src/Tools/nbe.ML
changeset 28350 715163ec93c0
parent 28337 93964076e7b8
child 28423 9fc3befd8191
     1.1 --- a/src/Tools/nbe.ML	Thu Sep 25 09:28:07 2008 +0200
     1.2 +++ b/src/Tools/nbe.ML	Thu Sep 25 09:28:08 2008 +0200
     1.3 @@ -15,10 +15,11 @@
     1.4      | Free of string * Univ list             (*free (uninterpreted) variables*)
     1.5      | DFree of string * int                  (*free (uninterpreted) dictionary parameters*)
     1.6      | BVar of int * Univ list
     1.7 -    | Abs of (int * (Univ list -> Univ)) * Univ list;
     1.8 +    | Abs of (int * (Univ list -> Univ)) * Univ list
     1.9    val apps: Univ -> Univ list -> Univ        (*explicit applications*)
    1.10    val abss: int -> (Univ list -> Univ) -> Univ
    1.11                                               (*abstractions as closures*)
    1.12 +  val same: Univ -> Univ -> bool
    1.13  
    1.14    val univs_ref: (unit -> Univ list -> Univ list) option ref
    1.15    val trace: bool ref
    1.16 @@ -63,6 +64,13 @@
    1.17    | Abs of (int * (Univ list -> Univ)) * Univ list
    1.18                                         (*abstractions as closures*);
    1.19  
    1.20 +fun same (Const (k, xs)) (Const (l, ys)) = k = l andalso sames xs ys
    1.21 +  | same (Free (s, xs)) (Free (t, ys)) = s = t andalso sames xs ys
    1.22 +  | same (DFree (s, k)) (DFree (t, l)) = s = t andalso k = l
    1.23 +  | same (BVar (k, xs)) (BVar (l, ys)) = k = l andalso sames xs ys
    1.24 +  | same _ _ = false
    1.25 +and sames xs ys = length xs = length ys andalso forall (uncurry same) (xs ~~ ys);
    1.26 +
    1.27  (* constructor functions *)
    1.28  
    1.29  fun abss n f = Abs ((n, f), []);
    1.30 @@ -92,6 +100,11 @@
    1.31  fun ml_Let d e = "let\n" ^ d ^ " in " ^ e ^ " end";
    1.32  fun ml_as v t = "(" ^ v ^ " as " ^ t ^ ")";
    1.33  
    1.34 +fun ml_and [] = "true"
    1.35 +  | ml_and [x] = x
    1.36 +  | ml_and xs = "(" ^ space_implode " andalso " xs ^ ")";
    1.37 +fun ml_if b x y = "(if " ^ b ^ " then " ^ x ^ " else " ^ y ^ ")";
    1.38 +
    1.39  fun ml_list es = "[" ^ commas es ^ "]";
    1.40  
    1.41  fun ml_fundefs ([(name, [([], e)])]) =
    1.42 @@ -113,11 +126,12 @@
    1.43  val univs_ref = ref (NONE : (unit -> Univ list -> Univ list) option);
    1.44  
    1.45  local
    1.46 -  val prefix =          "Nbe.";
    1.47 -  val name_ref =        prefix ^ "univs_ref";
    1.48 -  val name_const =      prefix ^ "Const";
    1.49 -  val name_abss =       prefix ^ "abss";
    1.50 -  val name_apps =       prefix ^ "apps";
    1.51 +  val prefix =      "Nbe.";
    1.52 +  val name_ref =    prefix ^ "univs_ref";
    1.53 +  val name_const =  prefix ^ "Const";
    1.54 +  val name_abss =   prefix ^ "abss";
    1.55 +  val name_apps =   prefix ^ "apps";
    1.56 +  val name_same =   prefix ^ "same";
    1.57  in
    1.58  
    1.59  val univs_cookie = (name_ref, univs_ref);
    1.60 @@ -141,6 +155,8 @@
    1.61  fun nbe_abss 0 f = f `$` ml_list []
    1.62    | nbe_abss n f = name_abss `$$` [string_of_int n, f];
    1.63  
    1.64 +fun nbe_same v1 v2 = "(" ^ name_same ^ " " ^ nbe_bound v1 ^ " " ^ nbe_bound v2 ^ ")";
    1.65 +
    1.66  end;
    1.67  
    1.68  open Basic_Code_Thingol;
    1.69 @@ -173,34 +189,62 @@
    1.70        | assemble_idict (DictVar (supers, (v, (n, _)))) =
    1.71            fold_rev (fn super => assemble_constapp super [] o single) supers (nbe_dict v n);
    1.72  
    1.73 -    fun assemble_iterm match_cont constapp =
    1.74 +    fun assemble_iterm constapp =
    1.75        let
    1.76 -        fun of_iterm t =
    1.77 +        fun of_iterm match_cont t =
    1.78            let
    1.79              val (t', ts) = Code_Thingol.unfold_app t
    1.80 -          in of_iapp t' (fold_rev (cons o of_iterm) ts []) end
    1.81 -        and of_iapp (IConst (c, (dss, _))) ts = constapp c dss ts
    1.82 -          | of_iapp (IVar v) ts = nbe_apps (nbe_bound v) ts
    1.83 -          | of_iapp ((v, _) `|-> t) ts =
    1.84 -              nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound v]) (of_iterm t))) ts
    1.85 -          | of_iapp (ICase (((t, _), cs), t0)) ts =
    1.86 -              nbe_apps (ml_cases (of_iterm t) (map (pairself of_iterm) cs
    1.87 -                @ [("_", case match_cont of SOME s => s | NONE => of_iterm t0)])) ts
    1.88 +          in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end
    1.89 +        and of_iapp match_cont (IConst (c, (dss, _))) ts = constapp c dss ts
    1.90 +          | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound v) ts
    1.91 +          | of_iapp match_cont ((v, _) `|-> t) ts =
    1.92 +              nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound v]) (of_iterm NONE t))) ts
    1.93 +          | of_iapp match_cont (ICase (((t, _), cs), t0)) ts =
    1.94 +              nbe_apps (ml_cases (of_iterm NONE t)
    1.95 +                (map (fn (p, t) => (of_iterm NONE p, of_iterm match_cont t)) cs
    1.96 +                  @ [("_", case match_cont of SOME s => s | NONE => of_iterm NONE t0)])) ts
    1.97        in of_iterm end;
    1.98  
    1.99 +    fun subst_nonlin_vars args =
   1.100 +      let
   1.101 +        val vs = (fold o Code_Thingol.fold_varnames)
   1.102 +          (fn v => AList.map_default (op =) (v, 0) (curry (op +) 1)) args [];
   1.103 +        val names = Name.make_context (map fst vs);
   1.104 +        fun declare v k ctxt = let val vs = Name.invents ctxt v k
   1.105 +          in (vs, fold Name.declare vs ctxt) end;
   1.106 +        val (vs_renames, _) = fold_map (fn (v, k) => if k > 1
   1.107 +          then declare v (k - 1) #>> (fn vs => (v, vs))
   1.108 +          else pair (v, [])) vs names;
   1.109 +        val samepairs = maps (fn (v, vs) => map (pair v) vs) vs_renames;
   1.110 +        fun subst_vars (t as IConst _) samepairs = (t, samepairs)
   1.111 +          | subst_vars (t as IVar v) samepairs = (case AList.lookup (op =) samepairs v
   1.112 +             of SOME v' => (IVar v', AList.delete (op =) v samepairs)
   1.113 +              | NONE => (t, samepairs))
   1.114 +          | subst_vars (t1 `$ t2) samepairs = samepairs
   1.115 +              |> subst_vars t1
   1.116 +              ||>> subst_vars t2
   1.117 +              |>> (op `$)
   1.118 +          | subst_vars (ICase (_, t)) samepairs = subst_vars t samepairs;
   1.119 +        val (args', _) = fold_map subst_vars args samepairs;
   1.120 +      in (samepairs, args') end;
   1.121 +
   1.122      fun assemble_eqn c dicts default_args (i, (args, rhs)) =
   1.123        let
   1.124          val is_eval = (c = "");
   1.125          val default_rhs = nbe_apps_local (i+1) c (dicts @ default_args);
   1.126          val match_cont = if is_eval then NONE else SOME default_rhs;
   1.127 -        val assemble_arg = assemble_iterm NONE
   1.128 -          (fn c => fn _ => fn ts => nbe_apps_constr idx_of c ts);
   1.129 -        val assemble_rhs = assemble_iterm match_cont assemble_constapp;
   1.130 +        val assemble_arg = assemble_iterm
   1.131 +          (fn c => fn _ => fn ts => nbe_apps_constr idx_of c ts) NONE;
   1.132 +        val assemble_rhs = assemble_iterm assemble_constapp match_cont ;
   1.133 +        val (samepairs, args') = subst_nonlin_vars args;
   1.134 +        val s_args = map assemble_arg args';
   1.135 +        val s_rhs = if null samepairs then assemble_rhs rhs
   1.136 +          else ml_if (ml_and (map (uncurry nbe_same) samepairs))
   1.137 +            (assemble_rhs rhs) default_rhs;
   1.138          val eqns = if is_eval then
   1.139 -            [([ml_list (rev (dicts @ map assemble_arg args))], assemble_rhs rhs)]
   1.140 +            [([ml_list (rev (dicts @ s_args))], s_rhs)]
   1.141            else
   1.142 -            [([ml_list (rev (dicts @ map2 ml_as default_args
   1.143 -                (map assemble_arg args)))], assemble_rhs rhs),
   1.144 +            [([ml_list (rev (dicts @ map2 ml_as default_args s_args))], s_rhs),
   1.145                ([ml_list (rev (dicts @ default_args))], default_rhs)]
   1.146        in (nbe_fun i c, eqns) end;
   1.147