changing const type to pass along if typing annotations are necessary for disambigous terms
authorbulwahn
Wed Sep 07 13:51:30 2011 +0200 (2011-09-07)
changeset 447888b935f1b3cf8
parent 44778 18b1ba7cfcfe
child 44789 5a062c23c7db
changing const type to pass along if typing annotations are necessary for disambigous terms
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_ml.ML
src/Tools/Code/code_printer.ML
src/Tools/Code/code_scala.ML
src/Tools/Code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/Tools/Code/code_haskell.ML	Wed Sep 07 11:36:39 2011 +0200
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Wed Sep 07 13:51:30 2011 +0200
     1.3 @@ -75,7 +75,7 @@
     1.4                  then print_case tyvars some_thm vars fxy cases
     1.5                  else print_app tyvars some_thm vars fxy c_ts
     1.6              | NONE => print_case tyvars some_thm vars fxy cases)
     1.7 -    and print_app_expr tyvars some_thm vars ((c, (_, function_typs)), ts) = case contr_classparam_typs c
     1.8 +    and print_app_expr tyvars some_thm vars ((c, ((_, function_typs), _)), ts) = case contr_classparam_typs c
     1.9       of [] => (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
    1.10        | fingerprint => let
    1.11            val ts_fingerprint = ts ~~ take (length ts) fingerprint;
    1.12 @@ -230,14 +230,14 @@
    1.13                      ]
    1.14                  | SOME k =>
    1.15                      let
    1.16 -                      val (c, (_, tys)) = const;
    1.17 +                      val (c, ((_, tys), _)) = const; (* FIXME: pass around the need annotation flag here? *)
    1.18                        val (vs, rhs) = (apfst o map) fst
    1.19                          (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
    1.20                        val s = if (is_some o const_syntax) c
    1.21                          then NONE else (SOME o Long_Name.base_name o deresolve) c;
    1.22                        val vars = reserved
    1.23                          |> intro_vars (map_filter I (s :: vs));
    1.24 -                      val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs;
    1.25 +                      val lhs = IConst (classparam, ((([], []), tys), false (* FIXME *))) `$$ map IVar vs;
    1.26                          (*dictionaries are not relevant at this late stage*)
    1.27                      in
    1.28                        semicolon [
     2.1 --- a/src/Tools/Code/code_ml.ML	Wed Sep 07 11:36:39 2011 +0200
     2.2 +++ b/src/Tools/Code/code_ml.ML	Wed Sep 07 13:51:30 2011 +0200
     2.3 @@ -117,7 +117,7 @@
     2.4                  then print_case is_pseudo_fun some_thm vars fxy cases
     2.5                  else print_app is_pseudo_fun some_thm vars fxy c_ts
     2.6              | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
     2.7 -    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), function_typs)), ts)) =
     2.8 +    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), function_typs), _)), ts)) =
     2.9        if is_cons c then
    2.10          let val k = length function_typs in
    2.11            if k < 2 orelse length ts = k
    2.12 @@ -417,7 +417,7 @@
    2.13                  then print_case is_pseudo_fun some_thm vars fxy cases
    2.14                  else print_app is_pseudo_fun some_thm vars fxy c_ts
    2.15              | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
    2.16 -    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), tys)), ts)) =
    2.17 +    and print_app_expr is_pseudo_fun some_thm vars (app as ((c, (((_, iss), tys), _)), ts)) =
    2.18        if is_cons c then
    2.19          let val k = length tys in
    2.20            if length ts = k
     3.1 --- a/src/Tools/Code/code_printer.ML	Wed Sep 07 11:36:39 2011 +0200
     3.2 +++ b/src/Tools/Code/code_printer.ML	Wed Sep 07 13:51:30 2011 +0200
     3.3 @@ -315,7 +315,7 @@
     3.4        |-> (fn cs' => pair (Complex_const_syntax (n, f literals cs')));
     3.5  
     3.6  fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
     3.7 -    (app as ((c, (_, function_typs)), ts)) =
     3.8 +    (app as ((c, ((_, function_typs), _)), ts)) =
     3.9    case const_syntax c of
    3.10      NONE => brackify fxy (print_app_expr some_thm vars app)
    3.11    | SOME (Plain_const_syntax (_, s)) =>
     4.1 --- a/src/Tools/Code/code_scala.ML	Wed Sep 07 11:36:39 2011 +0200
     4.2 +++ b/src/Tools/Code/code_scala.ML	Wed Sep 07 13:51:30 2011 +0200
     4.3 @@ -72,7 +72,7 @@
     4.4                  else print_app tyvars is_pat some_thm vars fxy c_ts
     4.5              | NONE => print_case tyvars some_thm vars fxy cases)
     4.6      and print_app tyvars is_pat some_thm vars fxy
     4.7 -        (app as ((c, ((arg_typs, _), function_typs)), ts)) =
     4.8 +        (app as ((c, (((arg_typs, _), function_typs), _)), ts)) =
     4.9        let
    4.10          val k = length ts;
    4.11          val arg_typs' = if is_pat orelse
    4.12 @@ -265,7 +265,7 @@
    4.13            let
    4.14              val tyvars = intro_tyvars vs reserved;
    4.15              val classtyp = (class, tyco `%% map (ITyVar o fst) vs);
    4.16 -            fun print_classparam_instance ((classparam, const as (_, (_, tys))), (thm, _)) =
    4.17 +            fun print_classparam_instance ((classparam, const as (_, ((_, tys), _))), (thm, _)) =
    4.18                let
    4.19                  val aux_tys = Name.invent_names (snd reserved) "a" tys;
    4.20                  val auxs = map fst aux_tys;
     5.1 --- a/src/Tools/Code/code_thingol.ML	Wed Sep 07 11:36:39 2011 +0200
     5.2 +++ b/src/Tools/Code/code_thingol.ML	Wed Sep 07 13:51:30 2011 +0200
     5.3 @@ -22,7 +22,7 @@
     5.4    datatype itype =
     5.5        `%% of string * itype list
     5.6      | ITyVar of vname;
     5.7 -  type const = string * ((itype list * dict list list) * itype list)
     5.8 +  type const = string * (((itype list * dict list list) * itype list) * bool)
     5.9      (* f [T1..Tn] {dicts} (_::S1) .. (_..Sm) =^= (f, (([T1..Tn], dicts), [S1..Sm]) *)
    5.10    datatype iterm =
    5.11        IConst of const
    5.12 @@ -145,7 +145,8 @@
    5.13      `%% of string * itype list
    5.14    | ITyVar of vname;
    5.15  
    5.16 -type const = string * ((itype list * dict list list) * itype list (*types of arguments*))
    5.17 +type const = string * (((itype list * dict list list) * itype list (*types of arguments*))
    5.18 +  * bool (*requires type annotation*))
    5.19  
    5.20  datatype iterm =
    5.21      IConst of const
    5.22 @@ -198,7 +199,7 @@
    5.23  fun add_tycos (tyco `%% tys) = insert (op =) tyco #> fold add_tycos tys
    5.24    | add_tycos (ITyVar _) = I;
    5.25  
    5.26 -val add_tyconames = fold_constexprs (fn (_, ((tys, _), _)) => fold add_tycos tys);
    5.27 +val add_tyconames = fold_constexprs (fn (_, (((tys, _), _), _)) => fold add_tycos tys);
    5.28  
    5.29  fun fold_varnames f =
    5.30    let
    5.31 @@ -240,7 +241,7 @@
    5.32          val vs_tys = (map o apfst) SOME (Name.invent_names ctxt "a" tys);
    5.33        in (vs_tys, t `$$ map (IVar o fst) vs_tys) end;
    5.34  
    5.35 -fun eta_expand k (c as (name, (_, tys)), ts) =
    5.36 +fun eta_expand k (c as (name, ((_, tys), _)), ts) =
    5.37    let
    5.38      val j = length ts;
    5.39      val l = k - j;
    5.40 @@ -256,7 +257,7 @@
    5.41      fun cont_dict (Dict (_, d)) = cont_plain_dict d
    5.42      and cont_plain_dict (Dict_Const (_, dss)) = (exists o exists) cont_dict dss
    5.43        | cont_plain_dict (Dict_Var _) = true;
    5.44 -    fun cont_term (IConst (_, ((_, dss), _))) = (exists o exists) cont_dict dss
    5.45 +    fun cont_term (IConst (_, (((_, dss), _), _))) = (exists o exists) cont_dict dss
    5.46        | cont_term (IVar _) = false
    5.47        | cont_term (t1 `$ t2) = cont_term t1 orelse cont_term t2
    5.48        | cont_term (_ `|=> t) = cont_term t
    5.49 @@ -756,7 +757,8 @@
    5.50      ##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs
    5.51      ##>> fold_map (translate_dicts thy algbr eqngr permissive some_thm) (arg_typs ~~ sorts)
    5.52      ##>> fold_map (translate_typ thy algbr eqngr permissive) function_typs
    5.53 -    #>> (fn (((c, arg_typs), dss), function_typs) => IConst (c, ((arg_typs, dss), function_typs)))
    5.54 +    #>> (fn (((c, arg_typs), dss), function_typs) =>
    5.55 +      IConst (c, (((arg_typs, dss), function_typs), false))) (* FIXME *)
    5.56    end
    5.57  and translate_app_const thy algbr eqngr permissive some_thm ((c_ty, ts), some_abs) =
    5.58    translate_const thy algbr eqngr permissive some_thm (c_ty, some_abs)
    5.59 @@ -801,7 +803,7 @@
    5.60          val ts_clause = nth_drop t_pos ts;
    5.61          val clauses = if null case_pats
    5.62            then mk_clause (fn ([t], body) => (t, body)) [ty] (the_single ts_clause)
    5.63 -          else maps (fn ((constr as IConst (_, (_, tys)), n), t) =>
    5.64 +          else maps (fn ((constr as IConst (_, ((_, tys), _)), n), t) =>
    5.65              mk_clause (fn (ts, body) => (constr `$$ ts, body)) (take n tys) t)
    5.66                (constrs ~~ ts_clause);
    5.67        in ((t, ty), clauses) end;
     6.1 --- a/src/Tools/nbe.ML	Wed Sep 07 11:36:39 2011 +0200
     6.2 +++ b/src/Tools/nbe.ML	Wed Sep 07 13:51:30 2011 +0200
     6.3 @@ -315,7 +315,7 @@
     6.4            let
     6.5              val (t', ts) = Code_Thingol.unfold_app t
     6.6            in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end
     6.7 -        and of_iapp match_cont (IConst (c, ((_, dss), _))) ts = constapp c dss ts
     6.8 +        and of_iapp match_cont (IConst (c, (((_, dss), _), _))) ts = constapp c dss ts
     6.9            | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound_optional v) ts
    6.10            | of_iapp match_cont ((v, _) `|=> t) ts =
    6.11                nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts
    6.12 @@ -425,7 +425,7 @@
    6.13          val params = Name.invent Name.context "d" (length names);
    6.14          fun mk (k, name) =
    6.15            (name, ([(v, [])],
    6.16 -            [([IConst (class, (([], []), [])) `$$ map (IVar o SOME) params],
    6.17 +            [([IConst (class, ((([], []), []), false)) `$$ map (IVar o SOME) params],
    6.18                IVar (SOME (nth params k)))]));
    6.19        in map_index mk names end
    6.20    | eqns_of_stmt (_, Code_Thingol.Classrel _) =
    6.21 @@ -433,8 +433,8 @@
    6.22    | eqns_of_stmt (_, Code_Thingol.Classparam _) =
    6.23        []
    6.24    | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), (super_instances, (classparam_instances, _)))) =
    6.25 -      [(inst, (arity_args, [([], IConst (class, (([], []), [])) `$$
    6.26 -        map (fn (_, (_, (inst, dss))) => IConst (inst, (([], dss), []))) super_instances
    6.27 +      [(inst, (arity_args, [([], IConst (class, ((([], []), []), false)) `$$
    6.28 +        map (fn (_, (_, (inst, dss))) => IConst (inst, ((([], dss), []), false))) super_instances
    6.29          @ map (IConst o snd o fst) classparam_instances)]))];
    6.30  
    6.31