--- a/src/Tools/nbe.ML Wed Sep 15 11:30:32 2010 +0200
+++ b/src/Tools/nbe.ML Wed Sep 15 12:11:11 2010 +0200
@@ -377,15 +377,16 @@
in ml_abs deps_vars (ml_Let (ml_fundefs (flat fun_vars)) (ml_list fun_vals)) end;
-(* code compilation *)
+(* compile equations *)
-fun compile_eqnss ctxt gr raw_deps [] = []
- | compile_eqnss ctxt gr raw_deps eqnss =
+fun compile_eqnss thy nbe_program raw_deps [] = []
+ | compile_eqnss thy nbe_program raw_deps eqnss =
let
+ val ctxt = ProofContext.init_global thy;
val (deps, deps_vals) = split_list (map_filter
- (fn dep => Option.map (fn univ => (dep, univ)) (fst ((Graph.get_node gr dep)))) raw_deps);
+ (fn dep => Option.map (fn univ => (dep, univ)) (fst ((Graph.get_node nbe_program dep)))) raw_deps);
val idx_of = raw_deps
- |> map (fn dep => (dep, snd (Graph.get_node gr dep)))
+ |> map (fn dep => (dep, snd (Graph.get_node nbe_program dep)))
|> AList.lookup (op =)
|> (fn f => the o f);
val s = assemble_eqnss idx_of deps eqnss;
@@ -400,7 +401,7 @@
end;
-(* preparing function equations *)
+(* extract equations from statements *)
fun eqns_of_stmt (_, Code_Thingol.Fun (_, ((_, []), _))) =
[]
@@ -428,7 +429,10 @@
map (fn (_, (_, (inst, dss))) => IConst (inst, (([], dss), []))) super_instances
@ map (IConst o snd o fst) classparam_instances)]))];
-fun compile_stmts ctxt stmts_deps =
+
+(* compile whole programs *)
+
+fun compile_stmts thy stmts_deps =
let
val names = map (fst o fst) stmts_deps;
val names_deps = map (fn ((name, _), deps) => (name, deps)) stmts_deps;
@@ -437,13 +441,13 @@
|> maps snd
|> distinct (op =)
|> fold (insert (op =)) names;
- fun new_node name (gr, (maxidx, idx_tab)) = if can (Graph.get_node gr) name
- then (gr, (maxidx, idx_tab))
- else (Graph.new_node (name, (NONE, maxidx)) gr,
+ fun new_node name (nbe_program, (maxidx, idx_tab)) = if can (Graph.get_node nbe_program) name
+ then (nbe_program, (maxidx, idx_tab))
+ else (Graph.new_node (name, (NONE, maxidx)) nbe_program,
(maxidx + 1, Inttab.update_new (maxidx, name) idx_tab));
- fun compile gr = eqnss
- |> compile_eqnss ctxt gr refl_deps
- |> rpair gr;
+ fun compile nbe_program = eqnss
+ |> compile_eqnss thy nbe_program refl_deps
+ |> rpair nbe_program;
in
fold new_node refl_deps
#> apfst (fold (fn (name, deps) => fold (curry Graph.add_edge name) deps) names_deps
@@ -451,12 +455,12 @@
#-> fold (fn (name, univ) => (Graph.map_node name o apfst) (K (SOME univ))))
end;
-fun ensure_stmts ctxt program =
+fun compile_program thy program =
let
- fun add_stmts names (gr, (maxidx, idx_tab)) = if exists ((can o Graph.get_node) gr) names
- then (gr, (maxidx, idx_tab))
- else (gr, (maxidx, idx_tab))
- |> compile_stmts ctxt (map (fn name => ((name, Graph.get_node program name),
+ fun add_stmts names (nbe_program, (maxidx, idx_tab)) = if exists ((can o Graph.get_node) nbe_program) names
+ then (nbe_program, (maxidx, idx_tab))
+ else (nbe_program, (maxidx, idx_tab))
+ |> compile_stmts thy (map (fn name => ((name, Graph.get_node program name),
Graph.imm_succs program name)) names);
in
fold_rev add_stmts (Graph.strong_conn program)
@@ -465,20 +469,20 @@
(** evaluation **)
-(* term evaluation *)
+(* term evaluation by compilation *)
-fun eval_term ctxt gr deps (vs : (string * sort) list, t) =
+fun compile_term thy nbe_program deps (vs : (string * sort) list, t) =
let
val dict_frees = maps (fn (v, sort) => map_index (curry DFree v o fst) sort) vs;
in
("", (vs, [([], t)]))
- |> singleton (compile_eqnss ctxt gr deps)
+ |> singleton (compile_eqnss thy nbe_program deps)
|> snd
|> (fn t => apps t (rev dict_frees))
end;
-(* reification *)
+(* reconstruction *)
fun typ_of_itype program vs (ityco `%% itys) =
let
@@ -525,6 +529,29 @@
in of_univ 0 t 0 |> fst end;
+(* evaluation with type reconstruction *)
+
+fun eval_term thy program (nbe_program, idx_tab) ((vs0, (vs, ty)), t) deps =
+ let
+ val ctxt = Syntax.init_pretty_global thy;
+ val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
+ val ty' = typ_of_itype program vs0 ty;
+ fun type_infer t = singleton
+ (Type_Infer.infer_types ctxt (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE))
+ (Type.constraint ty' t);
+ fun check_tvars t =
+ if null (Term.add_tvars t []) then t
+ else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t);
+ in
+ compile_term thy nbe_program deps (vs, t)
+ |> term_of_univ thy program idx_tab
+ |> traced (fn t => "Normalized:\n" ^ string_of_term t)
+ |> type_infer
+ |> traced (fn t => "Types inferred:\n" ^ string_of_term t)
+ |> check_tvars
+ |> traced (fn _ => "---\n")
+ end;
+
(* function store *)
structure Nbe_Functions = Code_Data
@@ -533,43 +560,11 @@
val empty = (Graph.empty, (0, Inttab.empty));
);
-
-(* compilation, evaluation and reification *)
-
-fun compile_eval thy program =
- let
- val ctxt = ProofContext.init_global thy;
- val (gr, (_, idx_tab)) =
- Nbe_Functions.change thy (ensure_stmts ctxt program);
- in fn vs_t => fn deps =>
- vs_t
- |> eval_term ctxt gr deps
- |> term_of_univ thy program idx_tab
- end;
-
-
-(* evaluation with type reconstruction *)
-
-fun normalize thy program ((vs0, (vs, ty)), t) deps =
+fun compile thy program =
let
- val ctxt = Syntax.init_pretty_global thy;
- val ty' = typ_of_itype program vs0 ty;
- fun type_infer t =
- singleton
- (Type_Infer.infer_types ctxt (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE))
- (Type.constraint ty' t);
- val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
- fun check_tvars t =
- if null (Term.add_tvars t []) then t
- else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t);
- in
- compile_eval thy program (vs, t) deps
- |> traced (fn t => "Normalized:\n" ^ string_of_term t)
- |> type_infer
- |> traced (fn t => "Types inferred:\n" ^ string_of_term t)
- |> check_tvars
- |> traced (fn _ => "---\n")
- end;
+ val (nbe_program, (_, idx_tab)) =
+ Nbe_Functions.change thy (compile_program thy program);
+ in (nbe_program, idx_tab) end;
(* evaluation oracle *)
@@ -583,7 +578,7 @@
val (_, raw_oracle) = Context.>>> (Context.map_theory_result
(Thm.add_oracle (Binding.name "norm", fn (thy, program, vsp_ty_t, deps, ct) =>
- mk_equals thy ct (normalize thy program vsp_ty_t deps))));
+ mk_equals thy ct (eval_term thy program (compile thy program) vsp_ty_t deps))));
fun oracle thy program vsp_ty_t deps ct = raw_oracle (thy, program, vsp_ty_t, deps, ct);
@@ -601,7 +596,8 @@
(fn thy => lift_triv_classes_conv thy (Code_Thingol.dynamic_eval_conv thy (K (oracle thy)))));
fun dynamic_eval_value thy = lift_triv_classes_rew thy
- (no_frees_rew (Code_Thingol.dynamic_eval_value thy I (K (normalize thy))));
+ (no_frees_rew (Code_Thingol.dynamic_eval_value thy I
+ (K (fn program => eval_term thy program (compile thy program)))));
(* evaluation command *)