delayed evaluation
authorhaftmann
Sat Sep 15 19:27:48 2007 +0200 (2007-09-15)
changeset 24590733120d04233
parent 24589 d3fca349736c
child 24591 6509626eb2c9
delayed evaluation
src/Tools/nbe.ML
     1.1 --- a/src/Tools/nbe.ML	Sat Sep 15 19:27:44 2007 +0200
     1.2 +++ b/src/Tools/nbe.ML	Sat Sep 15 19:27:48 2007 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      Tools/Nbe/Nbe_Eval.ML
     1.5 +(*  Title:      Tools/nbe.ML
     1.6      ID:         $Id$
     1.7      Authors:    Klaus Aehlig, LMU Muenchen; Tobias Nipkow, Florian Haftmann, TU Muenchen
     1.8  
     1.9 @@ -24,7 +24,7 @@
    1.10                                              (*abstractions as functions*)
    1.11    val app: Univ -> Univ -> Univ              (*explicit application*)
    1.12  
    1.13 -  val univs_ref: Univ list ref 
    1.14 +  val univs_ref: (unit -> Univ list) ref 
    1.15    val lookup_fun: string -> Univ
    1.16  
    1.17    val normalization_conv: cterm -> thm
    1.18 @@ -91,7 +91,7 @@
    1.19  
    1.20  (* sandbox communication *)
    1.21  
    1.22 -val univs_ref = ref [] : Univ list ref;
    1.23 +val univs_ref = ref (fn () => [] : Univ list);
    1.24  
    1.25  local
    1.26  
    1.27 @@ -106,7 +106,7 @@
    1.28  fun compile_univs tab ([], _) = []
    1.29    | compile_univs tab (cs, raw_s) =
    1.30        let
    1.31 -        val _ = univs_ref := [];
    1.32 +        val _ = univs_ref := (fn () => []);
    1.33          val s = "Nbe.univs_ref := " ^ raw_s;
    1.34          val _ = tracing (fn () => "\n--- generated code:\n" ^ s) ();
    1.35          val _ = tab_ref := SOME tab;
    1.36 @@ -114,7 +114,7 @@
    1.37            Output.tracing o enclose "\n--- compiler echo (with error):\n" "\n---\n")
    1.38            (!trace) s;
    1.39          val _ = tab_ref := NONE;
    1.40 -        val univs = case !univs_ref of [] => error "compile_univs" | univs => univs;
    1.41 +        val univs = case !univs_ref () of [] => error "compile_univs" | univs => univs;
    1.42        in cs ~~ univs end;
    1.43  
    1.44  end; (*local*)
    1.45 @@ -127,7 +127,7 @@
    1.46  infix 9 `$` `$$`;
    1.47  fun e1 `$` e2 = "(" ^ e1 ^ " " ^ e2 ^ ")";
    1.48  fun e `$$` es = "(" ^ e ^ " " ^ space_implode " " es ^ ")";
    1.49 -fun ml_abs v e = "(fn" ^ v ^ " => " ^ e ^ ")";
    1.50 +fun ml_abs v e = "(fn " ^ v ^ " => " ^ e ^ ")";
    1.51  
    1.52  fun ml_Val v s = "val " ^ v ^ " = " ^ s;
    1.53  fun ml_cases t cs =
    1.54 @@ -136,6 +136,8 @@
    1.55  
    1.56  fun ml_list es = "[" ^ commas es ^ "]";
    1.57  
    1.58 +val ml_delay = ml_abs "()"
    1.59 +
    1.60  fun ml_fundefs ([(name, [([], e)])]) =
    1.61        "val " ^ name ^ " = " ^ e ^ "\n"
    1.62    | ml_fundefs (eqs :: eqss) =
    1.63 @@ -225,7 +227,8 @@
    1.64          val bind_funs = map nbe_lookup (filter is_fun funs);
    1.65          val bind_locals = ml_fundefs (map nbe_fun cs ~~ map
    1.66            (assemble_fun thy is_fun (AList.lookup (op =) num_args)) eqnss);
    1.67 -        val result = ml_list (map (fn (c, n) => nbe_abss n (nbe_fun c)) num_args);
    1.68 +        val result = ml_list (map (fn (c, n) => nbe_abss n (nbe_fun c)) num_args)
    1.69 +          |> ml_delay;
    1.70        in (cs, ml_Let (bind_funs @ [bind_locals]) result) end;
    1.71  
    1.72  fun assemble_eval thy is_fun (((vs, ty), t), deps) =
    1.73 @@ -235,13 +238,14 @@
    1.74      val bind_funs = map nbe_lookup (filter is_fun funs);
    1.75      val bind_value = ml_fundefs [(nbe_value, [([ml_list (map nbe_bound frees)],
    1.76        assemble_iterm thy is_fun (K NONE) t)])];
    1.77 -    val result = ml_list [nbe_value `$` ml_list (map nbe_free frees)];
    1.78 +    val result = ml_list [nbe_value `$` ml_list (map nbe_free frees)]
    1.79 +      |> ml_delay;
    1.80    in ([nbe_value], ml_Let (bind_funs @ [bind_value]) result) end;
    1.81  
    1.82  fun eqns_of_stmt ((_, CodeThingol.Fun (_, [])), _) =
    1.83        NONE
    1.84    | eqns_of_stmt ((name, CodeThingol.Fun (_, eqns)), deps) =
    1.85 -      SOME ((name, eqns), deps)
    1.86 +      SOME ((name, map fst eqns), deps)
    1.87    | eqns_of_stmt ((_, CodeThingol.Datatypecons _), _) =
    1.88        NONE
    1.89    | eqns_of_stmt ((_, CodeThingol.Datatype _), _) =