src/Tools/nbe.ML
changeset 39399 267235a14938
parent 39396 e9cad160aa0f
child 39436 4a7d09da2b9c
     1.1 --- a/src/Tools/nbe.ML	Wed Sep 15 15:11:39 2010 +0200
     1.2 +++ b/src/Tools/nbe.ML	Wed Sep 15 15:11:40 2010 +0200
     1.3 @@ -8,6 +8,7 @@
     1.4  sig
     1.5    val dynamic_eval_conv: conv
     1.6    val dynamic_eval_value: theory -> term -> term
     1.7 +  val static_eval_conv: theory -> string list -> conv
     1.8  
     1.9    datatype Univ =
    1.10        Const of int * Univ list               (*named (uninterpreted) constants*)
    1.11 @@ -228,9 +229,9 @@
    1.12  
    1.13  (* nbe specific syntax and sandbox communication *)
    1.14  
    1.15 -structure Univs = Proof_Data(
    1.16 +structure Univs = Proof_Data (
    1.17    type T = unit -> Univ list -> Univ list
    1.18 -  fun init thy () = error "Univs"
    1.19 +  fun init _ () = error "Univs"
    1.20  );
    1.21  val put_result = Univs.put;
    1.22  
    1.23 @@ -432,6 +433,12 @@
    1.24  
    1.25  (* compile whole programs *)
    1.26  
    1.27 +fun ensure_const_idx name (nbe_program, (maxidx, idx_tab)) =
    1.28 +  if can (Graph.get_node nbe_program) name
    1.29 +  then (nbe_program, (maxidx, idx_tab))
    1.30 +  else (Graph.new_node (name, (NONE, maxidx)) nbe_program,
    1.31 +    (maxidx + 1, Inttab.update_new (maxidx, name) idx_tab));
    1.32 +
    1.33  fun compile_stmts thy stmts_deps =
    1.34    let
    1.35      val names = map (fst o fst) stmts_deps;
    1.36 @@ -441,15 +448,11 @@
    1.37        |> maps snd
    1.38        |> distinct (op =)
    1.39        |> fold (insert (op =)) names;
    1.40 -    fun new_node name (nbe_program, (maxidx, idx_tab)) = if can (Graph.get_node nbe_program) name
    1.41 -      then (nbe_program, (maxidx, idx_tab))
    1.42 -      else (Graph.new_node (name, (NONE, maxidx)) nbe_program,
    1.43 -        (maxidx + 1, Inttab.update_new (maxidx, name) idx_tab));
    1.44      fun compile nbe_program = eqnss
    1.45        |> compile_eqnss thy nbe_program refl_deps
    1.46        |> rpair nbe_program;
    1.47    in
    1.48 -    fold new_node refl_deps
    1.49 +    fold ensure_const_idx refl_deps
    1.50      #> apfst (fold (fn (name, deps) => fold (curry Graph.add_edge name) deps) names_deps
    1.51        #> compile
    1.52        #-> fold (fn (name, univ) => (Graph.map_node name o apfst) (K (SOME univ))))
    1.53 @@ -560,10 +563,11 @@
    1.54    val empty = (Graph.empty, (0, Inttab.empty));
    1.55  );
    1.56  
    1.57 -fun compile thy program =
    1.58 +fun compile ignore_cache thy program =
    1.59    let
    1.60      val (nbe_program, (_, idx_tab)) =
    1.61 -      Nbe_Functions.change thy (compile_program thy program);
    1.62 +      Nbe_Functions.change (if ignore_cache then NONE else SOME thy)
    1.63 +        (compile_program thy program);
    1.64    in (nbe_program, idx_tab) end;
    1.65  
    1.66  
    1.67 @@ -577,10 +581,12 @@
    1.68    in Thm.mk_binop eq lhs rhs end;
    1.69  
    1.70  val (_, raw_oracle) = Context.>>> (Context.map_theory_result
    1.71 -  (Thm.add_oracle (Binding.name "norm", fn (thy, program, vsp_ty_t, deps, ct) =>
    1.72 -    mk_equals thy ct (eval_term thy program (compile thy program) vsp_ty_t deps))));
    1.73 +  (Thm.add_oracle (Binding.name "normalization_by_evaluation",
    1.74 +    fn (thy, program, nbe_program_idx_tab, vsp_ty_t, deps, ct) =>
    1.75 +      mk_equals thy ct (eval_term thy program nbe_program_idx_tab vsp_ty_t deps))));
    1.76  
    1.77 -fun oracle thy program vsp_ty_t deps ct = raw_oracle (thy, program, vsp_ty_t, deps, ct);
    1.78 +fun oracle thy program nbe_program_idx_tab vsp_ty_t deps ct =
    1.79 +  raw_oracle (thy, program, nbe_program_idx_tab, vsp_ty_t, deps, ct);
    1.80  
    1.81  fun no_frees_rew rew t =
    1.82    let
    1.83 @@ -592,12 +598,17 @@
    1.84      |> curry (Term.betapplys o swap) frees
    1.85    end;
    1.86  
    1.87 -val dynamic_eval_conv = Code_Simp.no_frees_conv (Conv.tap_thy
    1.88 -  (fn thy => lift_triv_classes_conv thy (Code_Thingol.dynamic_eval_conv thy (K (oracle thy)))));
    1.89 +val dynamic_eval_conv = Conv.tap_thy (fn thy => Code_Simp.no_frees_conv
    1.90 +  (lift_triv_classes_conv thy (Code_Thingol.dynamic_eval_conv thy
    1.91 +    (K (fn program => oracle thy program (compile false thy program))))));
    1.92  
    1.93  fun dynamic_eval_value thy = lift_triv_classes_rew thy
    1.94    (no_frees_rew (Code_Thingol.dynamic_eval_value thy I
    1.95 -    (K (fn program => eval_term thy program (compile thy program)))));
    1.96 +    (K (fn program => eval_term thy program (compile false thy program)))));
    1.97 +
    1.98 +fun static_eval_conv thy consts = Code_Simp.no_frees_conv
    1.99 +  (lift_triv_classes_conv thy (Code_Thingol.static_eval_conv thy consts
   1.100 +    (K (fn program => oracle thy program (compile true thy program)))));
   1.101  
   1.102  
   1.103  (** setup **)