src/Tools/nbe.ML
changeset 48072 ace701efe203
parent 47609 b3dab1892cda
child 51685 385ef6706252
     1.1 --- a/src/Tools/nbe.ML	Mon Jun 04 12:55:54 2012 +0200
     1.2 +++ b/src/Tools/nbe.ML	Tue Jun 05 07:05:56 2012 +0200
     1.3 @@ -314,13 +314,13 @@
     1.4            let
     1.5              val (t', ts) = Code_Thingol.unfold_app t
     1.6            in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end
     1.7 -        and of_iapp match_cont (IConst (c, (((_, dss), _), _))) ts = constapp c dss ts
     1.8 +        and of_iapp match_cont (IConst { name = c, dicts = dss, ... }) ts = constapp c dss ts
     1.9            | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound_optional v) ts
    1.10            | of_iapp match_cont ((v, _) `|=> t) ts =
    1.11                nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound_optional v]) (of_iterm NONE t))) ts
    1.12 -          | of_iapp match_cont (ICase (((t, _), cs), t0)) ts =
    1.13 +          | of_iapp match_cont (ICase { term = t, clauses = clauses, primitive = t0, ... }) ts =
    1.14                nbe_apps (ml_cases (of_iterm NONE t)
    1.15 -                (map (fn (p, t) => (of_iterm NONE p, of_iterm match_cont t)) cs
    1.16 +                (map (fn (p, t) => (of_iterm NONE p, of_iterm match_cont t)) clauses
    1.17                    @ [("_", case match_cont of SOME s => s | NONE => of_iterm NONE t0)])) ts
    1.18        in of_iterm end;
    1.19  
    1.20 @@ -345,7 +345,7 @@
    1.21                |> subst_vars t1
    1.22                ||>> subst_vars t2
    1.23                |>> (op `$)
    1.24 -          | subst_vars (ICase (_, t)) samepairs = subst_vars t samepairs;
    1.25 +          | subst_vars (ICase { primitive = t, ... }) samepairs = subst_vars t samepairs;
    1.26          val (args', _) = fold_map subst_vars args samepairs;
    1.27        in (samepairs, args') end;
    1.28  
    1.29 @@ -410,6 +410,10 @@
    1.30  
    1.31  (* extract equations from statements *)
    1.32  
    1.33 +fun dummy_const c dss =
    1.34 +  IConst { name = c, typargs = [], dicts = dss,
    1.35 +    dom = [], range = ITyVar "", annotate = false };
    1.36 +
    1.37  fun eqns_of_stmt (_, Code_Thingol.Fun (_, ((_, []), _))) =
    1.38        []
    1.39    | eqns_of_stmt (const, Code_Thingol.Fun (_, (((vs, _), eqns), _))) =
    1.40 @@ -424,17 +428,17 @@
    1.41          val params = Name.invent Name.context "d" (length names);
    1.42          fun mk (k, name) =
    1.43            (name, ([(v, [])],
    1.44 -            [([IConst (class, ((([], []), ([], ITyVar "")), false)) `$$ map (IVar o SOME) params],
    1.45 +            [([dummy_const class [] `$$ map (IVar o SOME) params],
    1.46                IVar (SOME (nth params k)))]));
    1.47        in map_index mk names end
    1.48    | eqns_of_stmt (_, Code_Thingol.Classrel _) =
    1.49        []
    1.50    | eqns_of_stmt (_, Code_Thingol.Classparam _) =
    1.51        []
    1.52 -  | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arity_args)), (super_instances, (classparam_instances, _)))) =
    1.53 -      [(inst, (arity_args, [([], IConst (class, ((([], []), ([], ITyVar "")), false)) `$$
    1.54 -        map (fn (_, (_, (inst, dss))) => IConst (inst, ((([], dss), ([], ITyVar "")), false))) super_instances
    1.55 -        @ map (IConst o snd o fst) classparam_instances)]))];
    1.56 +  | eqns_of_stmt (inst, Code_Thingol.Classinst { class, vs, superinsts, inst_params, ... }) =
    1.57 +      [(inst, (vs, [([], dummy_const class [] `$$
    1.58 +        map (fn (_, (_, (inst, dss))) => dummy_const inst dss) superinsts
    1.59 +        @ map (IConst o snd o fst) inst_params)]))];
    1.60  
    1.61  
    1.62  (* compile whole programs *)