explicit type arguments in constants
authorhaftmann
Wed May 06 16:01:06 2009 +0200 (2009-05-06)
changeset 31049396d4d6a1594
parent 31048 ac146fc38b51
child 31050 555b56b66fcf
explicit type arguments in constants
src/Tools/code/code_haskell.ML
src/Tools/code/code_ml.ML
src/Tools/code/code_thingol.ML
src/Tools/nbe.ML
     1.1 --- a/src/Tools/code/code_haskell.ML	Wed May 06 16:01:06 2009 +0200
     1.2 +++ b/src/Tools/code/code_haskell.ML	Wed May 06 16:01:06 2009 +0200
     1.3 @@ -261,7 +261,7 @@
     1.4                      val vars = init_syms
     1.5                        |> Code_Printer.intro_vars (the_list const)
     1.6                        |> Code_Printer.intro_vars vs;
     1.7 -                    val lhs = IConst (classparam, ([], tys)) `$$ map IVar vs;
     1.8 +                    val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs;
     1.9                        (*dictionaries are not relevant at this late stage*)
    1.10                    in
    1.11                      semicolon [
     2.1 --- a/src/Tools/code/code_ml.ML	Wed May 06 16:01:06 2009 +0200
     2.2 +++ b/src/Tools/code/code_ml.ML	Wed May 06 16:01:06 2009 +0200
     2.3 @@ -109,7 +109,7 @@
     2.4                  then pr_case is_closure thm vars fxy cases
     2.5                  else pr_app is_closure thm vars fxy c_ts
     2.6              | NONE => pr_case is_closure thm vars fxy cases)
     2.7 -    and pr_app' is_closure thm vars (app as ((c, (iss, tys)), ts)) =
     2.8 +    and pr_app' is_closure thm vars (app as ((c, ((_, iss), tys)), ts)) =
     2.9        if is_cons c then
    2.10          let
    2.11            val k = length tys
    2.12 @@ -414,7 +414,7 @@
    2.13                  then pr_case is_closure thm vars fxy cases
    2.14                  else pr_app is_closure thm vars fxy c_ts
    2.15              | NONE => pr_case is_closure thm vars fxy cases)
    2.16 -    and pr_app' is_closure thm vars (app as ((c, (iss, tys)), ts)) =
    2.17 +    and pr_app' is_closure thm vars (app as ((c, ((_, iss), tys)), ts)) =
    2.18        if is_cons c then
    2.19          if length tys = length ts
    2.20          then case ts
     3.1 --- a/src/Tools/code/code_thingol.ML	Wed May 06 16:01:06 2009 +0200
     3.2 +++ b/src/Tools/code/code_thingol.ML	Wed May 06 16:01:06 2009 +0200
     3.3 @@ -20,7 +20,7 @@
     3.4    datatype itype =
     3.5        `%% of string * itype list
     3.6      | ITyVar of vname;
     3.7 -  type const = string * (dict list list * itype list (*types of arguments*))
     3.8 +  type const = string * ((itype list * dict list list) * itype list (*types of arguments*))
     3.9    datatype iterm =
    3.10        IConst of const
    3.11      | IVar of vname
    3.12 @@ -44,11 +44,10 @@
    3.13    val unfold_abs: iterm -> ((vname * iterm option) * itype) list * iterm
    3.14    val split_let: iterm -> (((iterm * itype) * iterm) * iterm) option
    3.15    val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm
    3.16 -  val unfold_const_app: iterm ->
    3.17 -    ((string * (dict list list * itype list)) * iterm list) option
    3.18 +  val unfold_const_app: iterm -> (const * iterm list) option
    3.19    val collapse_let: ((vname * itype) * iterm) * iterm
    3.20      -> (iterm * itype) * (iterm * iterm) list
    3.21 -  val eta_expand: int -> (string * (dict list list * itype list)) * iterm list -> iterm
    3.22 +  val eta_expand: int -> const * iterm list -> iterm
    3.23    val contains_dictvar: iterm -> bool
    3.24    val locally_monomorphic: iterm -> bool
    3.25    val fold_constnames: (string -> 'a -> 'a) -> iterm -> 'a -> 'a
    3.26 @@ -122,7 +121,7 @@
    3.27      `%% of string * itype list
    3.28    | ITyVar of vname;
    3.29  
    3.30 -type const = string * (dict list list * itype list (*types of arguments*))
    3.31 +type const = string * ((itype list * dict list list) * itype list (*types of arguments*))
    3.32  
    3.33  datatype iterm =
    3.34      IConst of const
    3.35 @@ -212,7 +211,7 @@
    3.36        | contains (DictVar _) = K true;
    3.37    in
    3.38      fold_aiterms
    3.39 -      (fn IConst (_, (dss, _)) => (fold o fold) contains dss | _ => I) t false
    3.40 +      (fn IConst (_, ((_, dss), _)) => (fold o fold) contains dss | _ => I) t false
    3.41    end;
    3.42    
    3.43  fun locally_monomorphic (IConst _) = false
    3.44 @@ -602,9 +601,10 @@
    3.45      val tys_args = (fst o Term.strip_type) ty;
    3.46    in
    3.47      ensure_const thy algbr funcgr c
    3.48 +    ##>> fold_map (translate_typ thy algbr funcgr) tys
    3.49      ##>> fold_map (translate_dicts thy algbr funcgr thm) (tys ~~ sorts)
    3.50      ##>> fold_map (translate_typ thy algbr funcgr) tys_args
    3.51 -    #>> (fn ((c, iss), tys) => IConst (c, (iss, tys)))
    3.52 +    #>> (fn (((c, tys), iss), tys_args) => IConst (c, ((tys, iss), tys_args)))
    3.53    end
    3.54  and translate_app_const thy algbr funcgr thm (c_ty, ts) =
    3.55    translate_const thy algbr funcgr thm c_ty
     4.1 --- a/src/Tools/nbe.ML	Wed May 06 16:01:06 2009 +0200
     4.2 +++ b/src/Tools/nbe.ML	Wed May 06 16:01:06 2009 +0200
     4.3 @@ -194,7 +194,7 @@
     4.4            let
     4.5              val (t', ts) = Code_Thingol.unfold_app t
     4.6            in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end
     4.7 -        and of_iapp match_cont (IConst (c, (dss, _))) ts = constapp c dss ts
     4.8 +        and of_iapp match_cont (IConst (c, ((_, dss), _))) ts = constapp c dss ts
     4.9            | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound v) ts
    4.10            | of_iapp match_cont ((v, _) `|-> t) ts =
    4.11                nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound v]) (of_iterm NONE t))) ts
    4.12 @@ -299,15 +299,15 @@
    4.13          val params = Name.invent_list [] "d" (length names);
    4.14          fun mk (k, name) =
    4.15            (name, ([(v, [])],
    4.16 -            [([IConst (class, ([], [])) `$$ map IVar params], IVar (nth params k))]));
    4.17 +            [([IConst (class, (([], []), [])) `$$ map IVar params], IVar (nth params k))]));
    4.18        in map_index mk names end
    4.19    | eqns_of_stmt (_, Code_Thingol.Classrel _) =
    4.20        []
    4.21    | eqns_of_stmt (_, Code_Thingol.Classparam _) =
    4.22        []
    4.23    | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arities)), (superinsts, instops))) =
    4.24 -      [(inst, (arities, [([], IConst (class, ([], [])) `$$
    4.25 -        map (fn (_, (_, (inst, dicts))) => IConst (inst, (dicts, []))) superinsts
    4.26 +      [(inst, (arities, [([], IConst (class, (([], []), [])) `$$
    4.27 +        map (fn (_, (_, (inst, dicts))) => IConst (inst, (([], dicts), []))) superinsts
    4.28          @ map (IConst o snd o fst) instops)]))];
    4.29  
    4.30  fun compile_stmts ctxt stmts_deps =