src/Tools/nbe.ML
author haftmann
Thu Sep 25 09:28:08 2008 +0200 (2008-09-25)
changeset 28350 715163ec93c0
parent 28337 93964076e7b8
child 28423 9fc3befd8191
permissions -rw-r--r--
non left-linear equations for nbe
     1 (*  Title:      Tools/nbe.ML
     2     ID:         $Id$
     3     Authors:    Klaus Aehlig, LMU Muenchen; Tobias Nipkow, Florian Haftmann, TU Muenchen
     4 
     5 Normalization by evaluation, based on generic code generator.
     6 *)
     7 
     8 signature NBE =
     9 sig
    10   val norm_conv: cterm -> thm
    11   val norm_term: theory -> term -> term
    12 
    13   datatype Univ =
    14       Const of int * Univ list               (*named (uninterpreted) constants*)
    15     | Free of string * Univ list             (*free (uninterpreted) variables*)
    16     | DFree of string * int                  (*free (uninterpreted) dictionary parameters*)
    17     | BVar of int * Univ list
    18     | Abs of (int * (Univ list -> Univ)) * Univ list
    19   val apps: Univ -> Univ list -> Univ        (*explicit applications*)
    20   val abss: int -> (Univ list -> Univ) -> Univ
    21                                              (*abstractions as closures*)
    22   val same: Univ -> Univ -> bool
    23 
    24   val univs_ref: (unit -> Univ list -> Univ list) option ref
    25   val trace: bool ref
    26 
    27   val setup: theory -> theory
    28 end;
    29 
    30 structure Nbe: NBE =
    31 struct
    32 
    33 (* generic non-sense *)
    34 
    35 val trace = ref false;
    36 fun tracing f x = if !trace then (Output.tracing (f x); x) else x;
    37 
    38 
    39 (** the semantical universe **)
    40 
    41 (*
    42    Functions are given by their semantical function value. To avoid
    43    trouble with the ML-type system, these functions have the most
    44    generic type, that is "Univ list -> Univ". The calling convention is
    45    that the arguments come as a list, the last argument first. In
    46    other words, a function call that usually would look like
    47 
    48    f x_1 x_2 ... x_n   or   f(x_1,x_2, ..., x_n)
    49 
    50    would be in our convention called as
    51 
    52               f [x_n,..,x_2,x_1]
    53 
    54    Moreover, to handle functions that are still waiting for some
    55    arguments we have additionally a list of arguments collected to far
    56    and the number of arguments we're still waiting for.
    57 *)
    58 
    59 datatype Univ =
    60     Const of int * Univ list           (*named (uninterpreted) constants*)
    61   | Free of string * Univ list         (*free variables*)
    62   | DFree of string * int              (*free (uninterpreted) dictionary parameters*)
    63   | BVar of int * Univ list            (*bound variables, named*)
    64   | Abs of (int * (Univ list -> Univ)) * Univ list
    65                                        (*abstractions as closures*);
    66 
    67 fun same (Const (k, xs)) (Const (l, ys)) = k = l andalso sames xs ys
    68   | same (Free (s, xs)) (Free (t, ys)) = s = t andalso sames xs ys
    69   | same (DFree (s, k)) (DFree (t, l)) = s = t andalso k = l
    70   | same (BVar (k, xs)) (BVar (l, ys)) = k = l andalso sames xs ys
    71   | same _ _ = false
    72 and sames xs ys = length xs = length ys andalso forall (uncurry same) (xs ~~ ys);
    73 
    74 (* constructor functions *)
    75 
    76 fun abss n f = Abs ((n, f), []);
    77 fun apps (Abs ((n, f), xs)) ys = let val k = n - length ys in
    78       case int_ord (k, 0)
    79        of EQUAL => f (ys @ xs)
    80         | LESS => let val (zs, ws) = chop (~ k) ys in apps (f (ws @ xs)) zs end
    81         | GREATER => Abs ((k, f), ys @ xs) (*note: reverse convention also for apps!*)
    82       end
    83   | apps (Const (name, xs)) ys = Const (name, ys @ xs)
    84   | apps (Free (name, xs)) ys = Free (name, ys @ xs)
    85   | apps (BVar (n, xs)) ys = BVar (n, ys @ xs);
    86 
    87 
    88 (** assembling and compiling ML code from terms **)
    89 
    90 (* abstract ML syntax *)
    91 
    92 infix 9 `$` `$$`;
    93 fun e1 `$` e2 = "(" ^ e1 ^ " " ^ e2 ^ ")";
    94 fun e `$$` [] = e
    95   | e `$$` es = "(" ^ e ^ " " ^ space_implode " " es ^ ")";
    96 fun ml_abs v e = "(fn " ^ v ^ " => " ^ e ^ ")";
    97 
    98 fun ml_cases t cs =
    99   "(case " ^ t ^ " of " ^ space_implode " | " (map (fn (p, t) => p ^ " => " ^ t) cs) ^ ")";
   100 fun ml_Let d e = "let\n" ^ d ^ " in " ^ e ^ " end";
   101 fun ml_as v t = "(" ^ v ^ " as " ^ t ^ ")";
   102 
   103 fun ml_and [] = "true"
   104   | ml_and [x] = x
   105   | ml_and xs = "(" ^ space_implode " andalso " xs ^ ")";
   106 fun ml_if b x y = "(if " ^ b ^ " then " ^ x ^ " else " ^ y ^ ")";
   107 
   108 fun ml_list es = "[" ^ commas es ^ "]";
   109 
   110 fun ml_fundefs ([(name, [([], e)])]) =
   111       "val " ^ name ^ " = " ^ e ^ "\n"
   112   | ml_fundefs (eqs :: eqss) =
   113       let
   114         fun fundef (name, eqs) =
   115           let
   116             fun eqn (es, e) = name ^ " " ^ space_implode " " es ^ " = " ^ e
   117           in space_implode "\n  | " (map eqn eqs) end;
   118       in
   119         (prefix "fun " o fundef) eqs :: map (prefix "and " o fundef) eqss
   120         |> cat_lines
   121         |> suffix "\n"
   122       end;
   123 
   124 (* nbe specific syntax and sandbox communication *)
   125 
   126 val univs_ref = ref (NONE : (unit -> Univ list -> Univ list) option);
   127 
   128 local
   129   val prefix =      "Nbe.";
   130   val name_ref =    prefix ^ "univs_ref";
   131   val name_const =  prefix ^ "Const";
   132   val name_abss =   prefix ^ "abss";
   133   val name_apps =   prefix ^ "apps";
   134   val name_same =   prefix ^ "same";
   135 in
   136 
   137 val univs_cookie = (name_ref, univs_ref);
   138 
   139 fun nbe_fun 0 "" = "nbe_value"
   140   | nbe_fun i c = "c_" ^ translate_string (fn "." => "_" | c => c) c ^ "_" ^ string_of_int i;
   141 fun nbe_dict v n = "d_" ^ v ^ "_" ^ string_of_int n;
   142 fun nbe_bound v = "v_" ^ v;
   143 fun nbe_default v = "w_" ^ v;
   144 
   145 (*note: these three are the "turning spots" where proper argument order is established!*)
   146 fun nbe_apps t [] = t
   147   | nbe_apps t ts = name_apps `$$` [t, ml_list (rev ts)];
   148 fun nbe_apps_local i c ts = nbe_fun i c `$` ml_list (rev ts);
   149 fun nbe_apps_constr idx_of c ts =
   150   let
   151     val c' = if !trace then string_of_int (idx_of c) ^ " (*" ^ c ^ "*)"
   152       else string_of_int (idx_of c);
   153   in name_const `$` ("(" ^ c' ^ ", " ^ ml_list (rev ts) ^ ")") end;
   154 
   155 fun nbe_abss 0 f = f `$` ml_list []
   156   | nbe_abss n f = name_abss `$$` [string_of_int n, f];
   157 
   158 fun nbe_same v1 v2 = "(" ^ name_same ^ " " ^ nbe_bound v1 ^ " " ^ nbe_bound v2 ^ ")";
   159 
   160 end;
   161 
   162 open Basic_Code_Thingol;
   163 
   164 (* code generation *)
   165 
   166 fun assemble_eqnss idx_of deps eqnss =
   167   let
   168     fun prep_eqns (c, (vs, eqns)) =
   169       let
   170         val dicts = maps (fn (v, sort) => map_index (nbe_dict v o fst) sort) vs;
   171         val num_args = length dicts + ((length o fst o hd) eqns);
   172       in (c, (num_args, (dicts, eqns))) end;
   173     val eqnss' = map prep_eqns eqnss;
   174 
   175     fun assemble_constapp c dss ts = 
   176       let
   177         val ts' = (maps o map) assemble_idict dss @ ts;
   178       in case AList.lookup (op =) eqnss' c
   179        of SOME (num_args, _) => if num_args <= length ts'
   180             then let val (ts1, ts2) = chop num_args ts'
   181             in nbe_apps (nbe_apps_local 0 c ts1) ts2
   182             end else nbe_apps (nbe_abss num_args (nbe_fun 0 c)) ts'
   183         | NONE => if member (op =) deps c
   184             then nbe_apps (nbe_fun 0 c) ts'
   185             else nbe_apps_constr idx_of c ts'
   186       end
   187     and assemble_idict (DictConst (inst, dss)) =
   188           assemble_constapp inst dss []
   189       | assemble_idict (DictVar (supers, (v, (n, _)))) =
   190           fold_rev (fn super => assemble_constapp super [] o single) supers (nbe_dict v n);
   191 
   192     fun assemble_iterm constapp =
   193       let
   194         fun of_iterm match_cont t =
   195           let
   196             val (t', ts) = Code_Thingol.unfold_app t
   197           in of_iapp match_cont t' (fold_rev (cons o of_iterm NONE) ts []) end
   198         and of_iapp match_cont (IConst (c, (dss, _))) ts = constapp c dss ts
   199           | of_iapp match_cont (IVar v) ts = nbe_apps (nbe_bound v) ts
   200           | of_iapp match_cont ((v, _) `|-> t) ts =
   201               nbe_apps (nbe_abss 1 (ml_abs (ml_list [nbe_bound v]) (of_iterm NONE t))) ts
   202           | of_iapp match_cont (ICase (((t, _), cs), t0)) ts =
   203               nbe_apps (ml_cases (of_iterm NONE t)
   204                 (map (fn (p, t) => (of_iterm NONE p, of_iterm match_cont t)) cs
   205                   @ [("_", case match_cont of SOME s => s | NONE => of_iterm NONE t0)])) ts
   206       in of_iterm end;
   207 
   208     fun subst_nonlin_vars args =
   209       let
   210         val vs = (fold o Code_Thingol.fold_varnames)
   211           (fn v => AList.map_default (op =) (v, 0) (curry (op +) 1)) args [];
   212         val names = Name.make_context (map fst vs);
   213         fun declare v k ctxt = let val vs = Name.invents ctxt v k
   214           in (vs, fold Name.declare vs ctxt) end;
   215         val (vs_renames, _) = fold_map (fn (v, k) => if k > 1
   216           then declare v (k - 1) #>> (fn vs => (v, vs))
   217           else pair (v, [])) vs names;
   218         val samepairs = maps (fn (v, vs) => map (pair v) vs) vs_renames;
   219         fun subst_vars (t as IConst _) samepairs = (t, samepairs)
   220           | subst_vars (t as IVar v) samepairs = (case AList.lookup (op =) samepairs v
   221              of SOME v' => (IVar v', AList.delete (op =) v samepairs)
   222               | NONE => (t, samepairs))
   223           | subst_vars (t1 `$ t2) samepairs = samepairs
   224               |> subst_vars t1
   225               ||>> subst_vars t2
   226               |>> (op `$)
   227           | subst_vars (ICase (_, t)) samepairs = subst_vars t samepairs;
   228         val (args', _) = fold_map subst_vars args samepairs;
   229       in (samepairs, args') end;
   230 
   231     fun assemble_eqn c dicts default_args (i, (args, rhs)) =
   232       let
   233         val is_eval = (c = "");
   234         val default_rhs = nbe_apps_local (i+1) c (dicts @ default_args);
   235         val match_cont = if is_eval then NONE else SOME default_rhs;
   236         val assemble_arg = assemble_iterm
   237           (fn c => fn _ => fn ts => nbe_apps_constr idx_of c ts) NONE;
   238         val assemble_rhs = assemble_iterm assemble_constapp match_cont ;
   239         val (samepairs, args') = subst_nonlin_vars args;
   240         val s_args = map assemble_arg args';
   241         val s_rhs = if null samepairs then assemble_rhs rhs
   242           else ml_if (ml_and (map (uncurry nbe_same) samepairs))
   243             (assemble_rhs rhs) default_rhs;
   244         val eqns = if is_eval then
   245             [([ml_list (rev (dicts @ s_args))], s_rhs)]
   246           else
   247             [([ml_list (rev (dicts @ map2 ml_as default_args s_args))], s_rhs),
   248               ([ml_list (rev (dicts @ default_args))], default_rhs)]
   249       in (nbe_fun i c, eqns) end;
   250 
   251     fun assemble_eqns (c, (num_args, (dicts, eqns))) =
   252       let
   253         val default_args = map nbe_default
   254           (Name.invent_list [] "a" (num_args - length dicts));
   255         val eqns' = map_index (assemble_eqn c dicts default_args) eqns
   256           @ (if c = "" then [] else [(nbe_fun (length eqns) c,
   257             [([ml_list (rev (dicts @ default_args))],
   258               nbe_apps_constr idx_of c (dicts @ default_args))])]);
   259       in (eqns', nbe_abss num_args (nbe_fun 0 c)) end;
   260 
   261     val (fun_vars, fun_vals) = map_split assemble_eqns eqnss';
   262     val deps_vars = ml_list (map (nbe_fun 0) deps);
   263   in ml_abs deps_vars (ml_Let (ml_fundefs (flat fun_vars)) (ml_list fun_vals)) end;
   264 
   265 (* code compilation *)
   266 
   267 fun compile_eqnss _ gr raw_deps [] = []
   268   | compile_eqnss ctxt gr raw_deps eqnss =
   269       let
   270         val (deps, deps_vals) = split_list (map_filter
   271           (fn dep => Option.map (fn univ => (dep, univ)) (fst ((Graph.get_node gr dep)))) raw_deps);
   272         val idx_of = raw_deps
   273           |> map (fn dep => (dep, snd (Graph.get_node gr dep)))
   274           |> AList.lookup (op =)
   275           |> (fn f => the o f);
   276         val s = assemble_eqnss idx_of deps eqnss;
   277         val cs = map fst eqnss;
   278       in
   279         s
   280         |> tracing (fn s => "\n--- code to be evaluated:\n" ^ s)
   281         |> ML_Context.evaluate ctxt
   282             (Output.tracing o enclose "\n---compiler echo:\n" "\n---\n",
   283             Output.tracing o enclose "\n--- compiler echo (with error):\n" "\n---\n")
   284             (!trace) univs_cookie
   285         |> (fn f => f deps_vals)
   286         |> (fn univs => cs ~~ univs)
   287       end;
   288 
   289 (* preparing function equations *)
   290 
   291 fun eqns_of_stmt (_, Code_Thingol.Fun (_, [])) =
   292       []
   293   | eqns_of_stmt (const, Code_Thingol.Fun ((vs, _), eqns)) =
   294       [(const, (vs, map fst eqns))]
   295   | eqns_of_stmt (_, Code_Thingol.Datatypecons _) =
   296       []
   297   | eqns_of_stmt (_, Code_Thingol.Datatype _) =
   298       []
   299   | eqns_of_stmt (class, Code_Thingol.Class (v, (superclasses, classops))) =
   300       let
   301         val names = map snd superclasses @ map fst classops;
   302         val params = Name.invent_list [] "d" (length names);
   303         fun mk (k, name) =
   304           (name, ([(v, [])],
   305             [([IConst (class, ([], [])) `$$ map IVar params], IVar (nth params k))]));
   306       in map_index mk names end
   307   | eqns_of_stmt (_, Code_Thingol.Classrel _) =
   308       []
   309   | eqns_of_stmt (_, Code_Thingol.Classparam _) =
   310       []
   311   | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arities)), (superinsts, instops))) =
   312       [(inst, (arities, [([], IConst (class, ([], [])) `$$
   313         map (fn (_, (_, (inst, dicts))) => IConst (inst, (dicts, []))) superinsts
   314         @ map (IConst o snd o fst) instops)]))];
   315 
   316 fun compile_stmts ctxt stmts_deps =
   317   let
   318     val names = map (fst o fst) stmts_deps;
   319     val names_deps = map (fn ((name, _), deps) => (name, deps)) stmts_deps;
   320     val eqnss = maps (eqns_of_stmt o fst) stmts_deps;
   321     val refl_deps = names_deps
   322       |> maps snd
   323       |> distinct (op =)
   324       |> fold (insert (op =)) names;
   325     fun new_node name (gr, (maxidx, idx_tab)) = if can (Graph.get_node gr) name
   326       then (gr, (maxidx, idx_tab))
   327       else (Graph.new_node (name, (NONE, maxidx)) gr,
   328         (maxidx + 1, Inttab.update_new (maxidx, name) idx_tab));
   329     fun compile gr = eqnss
   330       |> compile_eqnss ctxt gr refl_deps
   331       |> rpair gr;
   332   in
   333     fold new_node refl_deps
   334     #> apfst (fold (fn (name, deps) => fold (curry Graph.add_edge name) deps) names_deps
   335       #> compile
   336       #-> fold (fn (name, univ) => (Graph.map_node name o apfst) (K (SOME univ))))
   337   end;
   338 
   339 fun ensure_stmts ctxt program =
   340   let
   341     fun add_stmts names (gr, (maxidx, idx_tab)) = if exists ((can o Graph.get_node) gr) names
   342       then (gr, (maxidx, idx_tab))
   343       else (gr, (maxidx, idx_tab))
   344         |> compile_stmts ctxt (map (fn name => ((name, Graph.get_node program name),
   345           Graph.imm_succs program name)) names);
   346   in fold_rev add_stmts (Graph.strong_conn program) end;
   347 
   348 
   349 (** evaluation **)
   350 
   351 (* term evaluation *)
   352 
   353 fun eval_term ctxt gr deps ((vs, ty) : typscheme, t) =
   354   let 
   355     val frees = Code_Thingol.fold_unbound_varnames (insert (op =)) t []
   356     val frees' = map (fn v => Free (v, [])) frees;
   357     val dict_frees = maps (fn (v, sort) => map_index (curry DFree v o fst) sort) vs;
   358   in
   359     ("", (vs, [(map IVar frees, t)]))
   360     |> singleton (compile_eqnss ctxt gr deps)
   361     |> snd
   362     |> (fn t => apps t (rev (dict_frees @ frees')))
   363   end;
   364 
   365 (* reification *)
   366 
   367 fun term_of_univ thy idx_tab t =
   368   let
   369     fun take_until f [] = []
   370       | take_until f (x::xs) = if f x then [] else x :: take_until f xs;
   371     fun is_dict (Const (idx, _)) =
   372           let
   373             val c = the (Inttab.lookup idx_tab idx);
   374           in
   375             (is_some o Code_Name.class_rev thy) c
   376             orelse (is_some o Code_Name.classrel_rev thy) c
   377             orelse (is_some o Code_Name.instance_rev thy) c
   378           end
   379       | is_dict (DFree _) = true
   380       | is_dict _ = false;
   381     fun of_apps bounds (t, ts) =
   382       fold_map (of_univ bounds) ts
   383       #>> (fn ts' => list_comb (t, rev ts'))
   384     and of_univ bounds (Const (idx, ts)) typidx =
   385           let
   386             val ts' = take_until is_dict ts;
   387             val c = (the o Code_Name.const_rev thy o the o Inttab.lookup idx_tab) idx;
   388             val (_, T) = Code.default_typ thy c;
   389             val T' = map_type_tvar (fn ((v, i), S) => TypeInfer.param (typidx + i) (v, [])) T;
   390             val typidx' = typidx + maxidx_of_typ T' + 1;
   391           in of_apps bounds (Term.Const (c, T'), ts') typidx' end
   392       | of_univ bounds (Free (name, ts)) typidx =
   393           of_apps bounds (Term.Free (name, dummyT), ts) typidx
   394       | of_univ bounds (BVar (n, ts)) typidx =
   395           of_apps bounds (Bound (bounds - n - 1), ts) typidx
   396       | of_univ bounds (t as Abs _) typidx =
   397           typidx
   398           |> of_univ (bounds + 1) (apps t [BVar (bounds, [])])
   399           |-> (fn t' => pair (Term.Abs ("u", dummyT, t')))
   400   in of_univ 0 t 0 |> fst end;
   401 
   402 (* function store *)
   403 
   404 structure Nbe_Functions = CodeDataFun
   405 (
   406   type T = (Univ option * int) Graph.T * (int * string Inttab.table);
   407   val empty = (Graph.empty, (0, Inttab.empty));
   408   fun purge thy cs (gr, (maxidx, idx_tab)) =
   409     let
   410       val cs_exisiting =
   411         map_filter (Code_Name.const_rev thy) (Graph.keys gr);
   412       val dels = (Graph.all_preds gr
   413           o map (Code_Name.const thy)
   414           o filter (member (op =) cs_exisiting)
   415         ) cs;
   416     in (Graph.del_nodes dels gr, (maxidx, idx_tab)) end;
   417 );
   418 
   419 (* compilation, evaluation and reification *)
   420 
   421 fun compile_eval thy program vs_ty_t deps =
   422   let
   423     val ctxt = ProofContext.init thy;
   424     val (gr, (_, idx_tab)) = Nbe_Functions.change thy (ensure_stmts ctxt program);
   425   in
   426     vs_ty_t
   427     |> eval_term ctxt gr deps
   428     |> term_of_univ thy idx_tab
   429   end;
   430 
   431 (* evaluation with type reconstruction *)
   432 
   433 fun eval thy t program vs_ty_t deps =
   434   let
   435     fun subst_const f = map_aterms (fn t as Term.Const (c, ty) => Term.Const (f c, ty)
   436       | t => t);
   437     val subst_triv_consts = subst_const (Code_Unit.resubst_alias thy);
   438     val ty = type_of t;
   439     val type_free = AList.lookup (op =)
   440       (map (fn (s, T) => (s, Term.Free (s, T))) (Term.add_frees t []));
   441     val type_frees = Term.map_aterms
   442       (fn (t as Term.Free (s, _)) => the_default t (type_free s) | t => t);
   443     fun type_infer t =
   444       singleton (TypeInfer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
   445         (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0)
   446       (TypeInfer.constrain ty t);
   447     fun check_tvars t = if null (Term.term_tvars t) then t else
   448       error ("Illegal schematic type variables in normalized term: "
   449         ^ setmp show_types true (Syntax.string_of_term_global thy) t);
   450     val string_of_term = setmp show_types true (Syntax.string_of_term_global thy);
   451   in
   452     compile_eval thy program vs_ty_t deps
   453     |> tracing (fn t => "Normalized:\n" ^ string_of_term t)
   454     |> subst_triv_consts
   455     |> type_frees
   456     |> tracing (fn t => "Vars typed:\n" ^ string_of_term t)
   457     |> type_infer
   458     |> tracing (fn t => "Types inferred:\n" ^ string_of_term t)
   459     |> check_tvars
   460     |> tracing (fn t => "---\n")
   461   end;
   462 
   463 (* evaluation oracle *)
   464 
   465 val (_, norm_oracle) = Context.>>> (Context.map_theory_result
   466   (Thm.add_oracle ("norm", fn (thy, t, program, vs_ty_t, deps) =>
   467     Thm.cterm_of thy (Logic.mk_equals (t, eval thy t program vs_ty_t deps)))));
   468 
   469 fun add_triv_classes thy =
   470   let
   471     val inters = curry (Sorts.inter_sort (Sign.classes_of thy))
   472       (Code_Unit.triv_classes thy);
   473     fun map_sorts f = (map_types o map_atyps)
   474       (fn TVar (v, sort) => TVar (v, f sort)
   475         | TFree (v, sort) => TFree (v, f sort));
   476   in map_sorts inters end;
   477 
   478 fun norm_conv ct =
   479   let
   480     val thy = Thm.theory_of_cterm ct;
   481     fun evaluator' t program vs_ty_t deps = norm_oracle (thy, t, program, vs_ty_t, deps);
   482     fun evaluator t = (add_triv_classes thy t, evaluator' t);
   483   in Code_Thingol.eval_conv thy evaluator ct end;
   484 
   485 fun norm_term thy t =
   486   let
   487     fun evaluator' t program vs_ty_t deps = eval thy t program vs_ty_t deps;
   488     fun evaluator t = (add_triv_classes thy t, evaluator' t);
   489   in (Code.postprocess_term thy o Code_Thingol.eval_term thy evaluator) t end;
   490 
   491 (* evaluation command *)
   492 
   493 fun norm_print_term ctxt modes t =
   494   let
   495     val thy = ProofContext.theory_of ctxt;
   496     val t' = norm_term thy t;
   497     val ty' = Term.type_of t';
   498     val ctxt' = Variable.auto_fixes t ctxt;
   499     val p = PrintMode.with_modes modes (fn () =>
   500       Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t'), Pretty.fbrk,
   501         Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' ty')]) ();
   502   in Pretty.writeln p end;
   503 
   504 
   505 (** Isar setup **)
   506 
   507 fun norm_print_term_cmd (modes, s) state =
   508   let val ctxt = Toplevel.context_of state
   509   in norm_print_term ctxt modes (Syntax.read_term ctxt s) end;
   510 
   511 val setup =
   512   Value.add_evaluator ("nbe", norm_term o ProofContext.theory_of);
   513 
   514 local structure P = OuterParse and K = OuterKeyword in
   515 
   516 val opt_modes = Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.xname --| P.$$$ ")")) [];
   517 
   518 val _ =
   519   OuterSyntax.improper_command "normal_form" "normalize term by evaluation" K.diag
   520     (opt_modes -- P.term >> (Toplevel.keep o norm_print_term_cmd));
   521 
   522 end;
   523 
   524 end;
   525