improvements for nbe
authorhaftmann
Fri Mar 03 08:52:39 2006 +0100 (2006-03-03)
changeset 1917768c6824d8bb6
parent 19176 52b6ecd0433a
child 19178 9b295c37854f
improvements for nbe
src/HOL/ex/nbe.thy
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/nbe.ML
src/Pure/Tools/nbe_codegen.ML
src/Pure/Tools/nbe_eval.ML
     1.1 --- a/src/HOL/ex/nbe.thy	Thu Mar 02 18:51:11 2006 +0100
     1.2 +++ b/src/HOL/ex/nbe.thy	Fri Mar 03 08:52:39 2006 +0100
     1.3 @@ -19,5 +19,6 @@
     1.4  norm_by_eval "(%(xs, ys). xs @ ys) ([a, b, c], [d, e, f])"
     1.5  norm_by_eval "%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True"
     1.6  norm_by_eval "map (%x. case x of None \<Rightarrow> False | Some y \<Rightarrow> True) [None, Some ()]"
     1.7 +norm_by_eval "rev [a, b, c]"
     1.8  
     1.9  end
     2.1 --- a/src/Pure/Tools/codegen_package.ML	Thu Mar 02 18:51:11 2006 +0100
     2.2 +++ b/src/Pure/Tools/codegen_package.ML	Fri Mar 03 08:52:39 2006 +0100
     2.3 @@ -420,7 +420,7 @@
     2.4      | NONE => idf_of_name thy nsp_const c
     2.5    end;
     2.6  
     2.7 -fun recconst_of_idf thy ((deftab, _), (_, (_, overltab2), _)) idf =
     2.8 +fun recconst_of_idf thy (_, (_, (_, overltab2), _)) idf =
     2.9    case name_of_idf thy nsp_const idf
    2.10     of SOME c => SOME (c, Sign.the_const_type thy c)
    2.11      | NONE => (
    2.12 @@ -432,6 +432,16 @@
    2.13            | NONE => NONE
    2.14        );
    2.15  
    2.16 +fun const_of_idf thy (tabs as (_, (_, _, dtcontab))) idf =
    2.17 +  case recconst_of_idf thy tabs idf
    2.18 +   of SOME c_ty => SOME c_ty
    2.19 +    | NONE => case dest_nsp nsp_mem idf
    2.20 +       of SOME c => SOME (c, Sign.the_const_constraint thy c)
    2.21 +        | NONE => case name_of_idf thy nsp_dtcon idf
    2.22 +           of SOME idf' => let
    2.23 +                val c = (fst o DatatypeconsNameMangler.rev thy dtcontab) idf'
    2.24 +              in SOME (c, Sign.the_const_type thy c) end
    2.25 +            | NONE => NONE;
    2.26  
    2.27  (* further theory data accessors *)
    2.28  
    2.29 @@ -1163,13 +1173,13 @@
    2.30  
    2.31  fun codegen_term t thy =
    2.32    thy
    2.33 -  |> expand_module NONE exprsgen_term [t]
    2.34 +  |> expand_module NONE exprsgen_term [Codegen.preprocess_term thy t]
    2.35    |-> (fn [t] => pair t);
    2.36  
    2.37  val is_dtcon = has_nsp nsp_dtcon;
    2.38  
    2.39  fun consts_of_idfs thy =
    2.40 -  map (the o recconst_of_idf thy (mk_tabs thy));
    2.41 +  map (the o const_of_idf thy (mk_tabs thy));
    2.42  
    2.43  fun idfs_of_consts thy =
    2.44    map (idf_of_const thy (mk_tabs thy));
     3.1 --- a/src/Pure/Tools/nbe.ML	Thu Mar 02 18:51:11 2006 +0100
     3.2 +++ b/src/Pure/Tools/nbe.ML	Fri Mar 03 08:52:39 2006 +0100
     3.3 @@ -1,81 +1,71 @@
     3.4  (*  ID:         $Id$
     3.5      Author:     Tobias Nipkow, Florian Haftmann, TU Muenchen
     3.6  
     3.7 -Installing "normalization by evaluation"
     3.8 +Toplevel theory interface for "normalization by evaluation"
     3.9  *)
    3.10  
    3.11 -signature NORMBYEVAL =
    3.12 +signature NBE =
    3.13  sig
    3.14 -  val lookup: string -> NBE_Eval.Univ
    3.15 -  val update: string * NBE_Eval.Univ -> unit
    3.16 +  val norm_by_eval_i: term -> theory -> term * theory;
    3.17 +  val lookup: string -> NBE_Eval.Univ;
    3.18 +  val update: string * NBE_Eval.Univ -> unit;
    3.19  end;
    3.20  
    3.21 -structure NormByEval:NORMBYEVAL =
    3.22 +structure NBE: NBE =
    3.23  struct
    3.24  
    3.25  structure NBE_Data = TheoryDataFun
    3.26  (struct
    3.27 -  val name = "Pure/NormByEval";
    3.28 -  type T = NBE_Eval.Univ Symtab.table
    3.29 -  val empty = Symtab.empty
    3.30 +  val name = "Pure/NBE";
    3.31 +  type T = NBE_Eval.Univ Symtab.table;
    3.32 +  val empty = Symtab.empty;
    3.33    val copy = I;
    3.34    val extend = I;
    3.35 -  fun merge _ = Symtab.merge (K true)
    3.36 +  fun merge _ = Symtab.merge (K true);
    3.37    fun print _ _ = ();
    3.38  end);
    3.39  
    3.40  val _ = Context.add_setup NBE_Data.init;
    3.41  
    3.42 +val tab : NBE_Eval.Univ Symtab.table ref = ref Symtab.empty;
    3.43 +fun lookup s = (the o Symtab.lookup (!tab)) s;
    3.44 +fun update sx = (tab := Symtab.update sx (!tab));
    3.45 +fun defined s = Symtab.defined (!tab) s;
    3.46 +
    3.47  fun use_show s = (writeln ("\n---generated code:\n"^ s);
    3.48       use_text(writeln o enclose "\n---compiler echo:\n" "\n---\n",
    3.49                writeln o enclose "\n--- compiler echo (with error!):\n" 
    3.50                                  "\n---\n")
    3.51        true s);
    3.52  
    3.53 -val tab : NBE_Eval.Univ Symtab.table ref = ref Symtab.empty;
    3.54 -fun lookup s = the(Symtab.lookup (!tab) s);
    3.55 -fun update sx = (tab := Symtab.update sx (!tab));
    3.56 -fun defined s = Symtab.defined (!tab) s;
    3.57 -
    3.58 -fun top_nbe st thy =
    3.59 +fun norm_by_eval_i t thy =
    3.60    let
    3.61 -    val t = Sign.read_term thy st;
    3.62      val nbe_tab = NBE_Data.get thy;
    3.63      val modl_old = CodegenThingol.partof (Symtab.keys nbe_tab)
    3.64        (CodegenPackage.get_root_module thy);
    3.65 -    val (t', thy') = CodegenPackage.codegen_term t thy
    3.66 +    val (t', thy') = CodegenPackage.codegen_term t thy;
    3.67      val modl_new = CodegenPackage.get_root_module thy';
    3.68      val diff = CodegenThingol.diff_module (modl_new, modl_old);
    3.69      val _ = writeln ("new definitions: " ^ (commas o map fst) diff);
    3.70      val _ = (tab := nbe_tab;
    3.71 -             Library.seq (use_show o NBE_Codegen.generate defined) diff)
    3.72 -    val thy'' = NBE_Data.put (!tab) thy'
    3.73 -    val nt' = NBE_Eval.nbe (!tab) t'
    3.74 -    val _ = print nt'
    3.75 +             Library.seq (use_show o NBE_Codegen.generate defined) diff);
    3.76 +    val thy'' = NBE_Data.put (!tab) thy';
    3.77 +    val nt' = NBE_Eval.nbe (!tab) t';
    3.78 +    val t' = NBE_Codegen.nterm_to_term thy'' nt';
    3.79 +    val _ = print nt';
    3.80 +    val _ = (Pretty.writeln o Sign.pretty_term thy'') t';
    3.81    in
    3.82 -    thy''
    3.83 +    (t', thy'')
    3.84    end;
    3.85  
    3.86 +fun norm_by_eval raw_t thy = norm_by_eval_i (Sign.read_term thy raw_t) thy;
    3.87 +
    3.88  structure P = OuterParse and K = OuterKeyword;
    3.89  
    3.90  val nbeP =
    3.91 -  OuterSyntax.command "norm_by_eval" "norm by eval" K.thy_decl
    3.92 -    (P.term >> (Toplevel.theory o top_nbe));
    3.93 +  OuterSyntax.command "norm_by_eval" "normalization by evaluation" K.thy_decl
    3.94 +    (P.term >> (fn t => Toplevel.theory (snd o norm_by_eval t)));
    3.95  
    3.96  val _ = OuterSyntax.add_parsers [nbeP];
    3.97 -(*
    3.98 -ProofGeneral.write_keywords "nbe";
    3.99 -*)
   3.100 -(* isar-keywords-nbe.el -> isabelle/etc/
   3.101 -   Isabelle -k nbe *)
   3.102  
   3.103 -end
   3.104 -
   3.105 -
   3.106 -(*
   3.107 -fun to_term xs (C s) = Const(s,dummyT)
   3.108 -  | to_term xs (V s) = Free(s,dummyT)
   3.109 -  | to_term xs (B i) = Bound (find_index_eq i xs)
   3.110 -  | to_term xs (A(t1,t2)) = to_term xs t1 $ to_term xs t2
   3.111 -  | to_term xs (AbsN(i,t)) = Abs("u",dummyT,to_term (i::xs) t);
   3.112 -*)
   3.113 +end;
     4.1 --- a/src/Pure/Tools/nbe_codegen.ML	Thu Mar 02 18:51:11 2006 +0100
     4.2 +++ b/src/Pure/Tools/nbe_codegen.ML	Fri Mar 03 08:52:39 2006 +0100
     4.3 @@ -1,5 +1,7 @@
     4.4  (*  ID:         $Id$
     4.5 -    Author:     Klaus Aehlig, Tobias Nipkow
     4.6 +    Author:     Klaus Aehlig, LMU Muenchen; Tobias Nipkow, TU Muenchen
     4.7 +
     4.8 +Code generator for "normalization by evaluation".
     4.9  *)
    4.10  
    4.11  (* Global asssumptions:
    4.12 @@ -14,7 +16,8 @@
    4.13  
    4.14  signature NBE_CODEGEN =
    4.15  sig
    4.16 -  val generate: (string -> bool) -> string * CodegenThingol.def -> string
    4.17 +  val generate: (string -> bool) -> string * CodegenThingol.def -> string;
    4.18 +  val nterm_to_term: theory -> NBE_Eval.nterm -> term;
    4.19  end
    4.20  
    4.21  
    4.22 @@ -63,8 +66,8 @@
    4.23  
    4.24  end
    4.25  
    4.26 -val tab_lookup = S.app "NormByEval.lookup";
    4.27 -val tab_update = S.app "NormByEval.update";
    4.28 +val tab_lookup = S.app "NBE.lookup";
    4.29 +val tab_update = S.app "NBE.update";
    4.30  
    4.31  fun mk_nbeFUN(nm,e) =
    4.32    S.app Eval_Fun (S.tup [S.abs(S.list [MLvname nm])e,S.list [],"1",
    4.33 @@ -117,31 +120,52 @@
    4.34  fun mk_eqn defined nm ar (lhs,e) =
    4.35    ([S.list(map mk_lexpr (rev lhs))], mk_rexpr defined nm ar e);
    4.36  
    4.37 -fun funs_of_expr (IConst ((s, _), _)) = insert (op =) s
    4.38 -  | funs_of_expr (e1 `$ e2) =
    4.39 -      funs_of_expr e1 #> funs_of_expr e2
    4.40 -  | funs_of_expr (_ `|-> e) = funs_of_expr e
    4.41 -  | funs_of_expr (IAbs (_, e)) = funs_of_expr e
    4.42 -  | funs_of_expr (ICase (_, e)) = funs_of_expr e
    4.43 -  | funs_of_expr _ = I;
    4.44 +fun consts_of (IConst ((s, _), _)) = insert (op =) s
    4.45 +  | consts_of (e1 `$ e2) =
    4.46 +      consts_of e1 #> consts_of e2
    4.47 +  | consts_of (_ `|-> e) = consts_of e
    4.48 +  | consts_of (IAbs (_, e)) = consts_of e
    4.49 +  | consts_of (ICase (_, e)) = consts_of e
    4.50 +  | consts_of _ = I;
    4.51  
    4.52  fun lookup nm = S.Val (MLname nm) (tab_lookup (S.quote nm));
    4.53  
    4.54  fun generate defined (nm, CodegenThingol.Fun (eqns, _)) =
    4.55 +      let
    4.56 +        val ar = length(fst(hd eqns));
    4.57 +        val params = S.list (rev (MLparams ar));
    4.58 +        val funs = Library.flat(map (fn (_,e) => consts_of e []) eqns) \ nm;
    4.59 +        val globals = map lookup (filter defined funs);
    4.60 +        val default_eqn = ([params], S.app Eval_Constr (S.tup[S.quote nm,params]));
    4.61 +        val code = S.eqns (MLname nm)
    4.62 +                          (map (mk_eqn defined nm ar) eqns @ [default_eqn])
    4.63 +        val register = tab_update
    4.64 +            (S.app Eval_mk_Fun (S.tup[S.quote nm, MLname nm, string_of_int ar]))
    4.65 +      in
    4.66 +        S.Let (globals @ [code]) register
    4.67 +      end
    4.68 +  | generate _ _ = "";
    4.69 +
    4.70 +open NBE_Eval;
    4.71 +
    4.72 +fun nterm_to_term thy t =
    4.73    let
    4.74 -    val ar = length(fst(hd eqns));
    4.75 -    val params = S.list (rev (MLparams ar));
    4.76 -    val funs = Library.flat(map (fn (_,e) => funs_of_expr e []) eqns) \ nm;
    4.77 -    val globals = map lookup (filter defined funs);
    4.78 -    val default_eqn = ([params], S.app Eval_Constr (S.tup[S.quote nm,params]));
    4.79 -    val code = S.eqns (MLname nm)
    4.80 -                      (map (mk_eqn defined nm ar) eqns @ [default_eqn])
    4.81 -    val register = tab_update
    4.82 -        (S.app Eval_mk_Fun (S.tup[S.quote nm, MLname nm, string_of_int ar]))
    4.83 -  in
    4.84 -    S.Let (globals @ [code]) register
    4.85 -  end
    4.86 -  | generate _ _ = "";
    4.87 +    fun consts_of (C s) = insert (op =) s
    4.88 +      | consts_of (V _) = I
    4.89 +      | consts_of (B _) = I
    4.90 +      | consts_of (A (t1, t2)) = consts_of t1 #> consts_of t2
    4.91 +      | consts_of (AbsN (_, t)) = consts_of t;
    4.92 +    val consts = consts_of t [];
    4.93 +    val the_const = AList.lookup (op =)
    4.94 +      (consts ~~ CodegenPackage.consts_of_idfs thy consts)
    4.95 +      #> the_default ("", dummyT);
    4.96 +    fun to_term bounds (C s) = Const (the_const s)
    4.97 +      | to_term bounds (V s) = Free (s, dummyT)
    4.98 +      | to_term bounds (B i) = Bound (find_index (fn j => i = j) bounds)
    4.99 +      | to_term bounds (A (t1, t2)) = to_term bounds t1 $ to_term bounds t2
   4.100 +      | to_term bounds (AbsN (i, t)) =
   4.101 +          Abs("u", dummyT, to_term (i::bounds) t);
   4.102 +  in to_term [] t end;
   4.103  
   4.104  end;
   4.105  
     5.1 --- a/src/Pure/Tools/nbe_eval.ML	Thu Mar 02 18:51:11 2006 +0100
     5.2 +++ b/src/Pure/Tools/nbe_eval.ML	Fri Mar 03 08:52:39 2006 +0100
     5.3 @@ -1,9 +1,9 @@
     5.4  (*  ID:         $Id$
     5.5 -    Author:     Klaus Aehlig, Tobias Nipkow
     5.6 +    Author:     Klaus Aehlig, LMU Muenchen; Tobias Nipkow, TU Muenchen
     5.7 +
     5.8 +Evaluator infrastructure for "normalization by evaluation".
     5.9  *)
    5.10  
    5.11 -(* ------------------------------ Evaluator  ------------------------------ *)
    5.12 -
    5.13  (* Optimizations:
    5.14   int instead of string in Constr
    5.15   treat int via ML ints
    5.16 @@ -11,50 +11,42 @@
    5.17  
    5.18  signature NBE_EVAL =
    5.19  sig
    5.20 -(* named terms used for output only *)
    5.21 -datatype nterm =
    5.22 -    C of string (* Named Constants *)
    5.23 -  | V of string (* Free Variable *)
    5.24 -  | B of int (* Named(!!) Bound Variables *)
    5.25 -  | A of nterm*nterm (* Application *)
    5.26 -  | AbsN of int*nterm ; (* Binding of named Variables *)
    5.27 +  (*named terms used for output only*)
    5.28 +  datatype nterm =
    5.29 +      C of string         (*named constants*)
    5.30 +    | V of string         (*free variable*)
    5.31 +    | B of int            (*named(!!) bound variables*)
    5.32 +    | A of nterm * nterm  (*application*)
    5.33 +    | AbsN of int * nterm (*binding of named variables*);
    5.34 +  datatype Univ = 
    5.35 +      Constr of string*(Univ list)       (*named constructors*)
    5.36 +    | Var of string*(Univ list)          (*free variables*)
    5.37 +    | BVar of int*(Univ list)            (*bound named variables*)
    5.38 +    | Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm)
    5.39 +                                         (*functions*);
    5.40  
    5.41 -datatype Univ = 
    5.42 -    Constr of string*(Univ list)       (* Named Constructors *)
    5.43 -  | Var of string*(Univ list)          (* Free variables *)
    5.44 -  | BVar of int*(Univ list)            (* Bound named variables *)
    5.45 -  | Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm);
    5.46 -                                            (* Functions *)
    5.47 -val nbe: Univ Symtab.table -> CodegenThingol.iexpr -> nterm
    5.48 +  val nbe: Univ Symtab.table -> CodegenThingol.iexpr -> nterm;
    5.49 +  val apply: Univ -> Univ -> Univ;
    5.50 +
    5.51 +  val to_term: Univ -> nterm;
    5.52  
    5.53 -val apply: Univ -> Univ -> Univ;
    5.54 -val to_term: Univ -> nterm;
    5.55 +  val mk_Fun: string * (Univ list -> Univ) * int -> string * Univ;
    5.56 +  val new_name: unit -> int;
    5.57  
    5.58 -val mk_Fun: string * (Univ list -> Univ) * int -> string * Univ
    5.59 -val new_name: unit -> int;
    5.60 -
    5.61 -(* For testing
    5.62 -val eval: term -> (Univ list) -> Univ
    5.63 -*)
    5.64 -
    5.65 +  (* For testing
    5.66 +  val eval: (Univ list) -> term -> Univ
    5.67 +  *)
    5.68  end;
    5.69  
    5.70 -(* FIXME add_funs and relatives should NOT be exported. Eventually it
    5.71 -should work like for quickcheck: Eval generates code which leaves the
    5.72 -function values in a public reference variable, the code is executed,
    5.73 -and the value of the reference variable is added to the internal
    5.74 -tables, all in one go, w/o interruption. *)
    5.75 -
    5.76 -
    5.77 -structure NBE_Eval:NBE_EVAL =
    5.78 +structure NBE_Eval: NBE_EVAL =
    5.79  struct
    5.80  
    5.81  datatype nterm =
    5.82 -    C of string (* Named Constants *)
    5.83 -  | V of string (* Free Variable *)
    5.84 -  | B of int (* Named(!!) Variables *)
    5.85 -  | A of nterm * nterm (* Application *)
    5.86 -  | AbsN of int * nterm (* Binding of named Variables *);
    5.87 +    C of string
    5.88 +  | V of string
    5.89 +  | B of int
    5.90 +  | A of nterm * nterm
    5.91 +  | AbsN of int * nterm;
    5.92  
    5.93  fun apps t args = foldr (fn (y,x) => A(x,y)) t args;
    5.94  
    5.95 @@ -100,11 +92,11 @@
    5.96     reasonably we applied in a semantical way.
    5.97  *)
    5.98  
    5.99 -fun  apply (Fun(f,xs,1,name))  x = f (x::xs)
   5.100 -   | apply (Fun(f,xs,n,name))  x = Fun(f,x::xs,n-1,name)
   5.101 -   | apply (Constr(name,args)) x = Constr(name,x::args)
   5.102 -   | apply (Var(name,args))    x = Var(name,x::args)
   5.103 -   | apply (BVar(name,args))   x = BVar(name,x::args);
   5.104 +fun apply (Fun(f,xs,1,name))  x = f (x::xs)
   5.105 +  | apply (Fun(f,xs,n,name))  x = Fun(f,x::xs,n-1,name)
   5.106 +  | apply (Constr(name,args)) x = Constr(name,x::args)
   5.107 +  | apply (Var(name,args))    x = Var(name,x::args)
   5.108 +  | apply (BVar(name,args))   x = BVar(name,x::args);
   5.109  
   5.110  fun mk_Fun(name,v,0) = (name,v [])
   5.111    | mk_Fun(name,v,n) = (name,Fun(v,[],n, fn () => C name));
   5.112 @@ -123,7 +115,7 @@
   5.113  
   5.114  val counter = ref 0;
   5.115  
   5.116 -fun new_name() = (counter := !counter +1; !counter);
   5.117 +fun new_name () = (counter := !counter +1; !counter);
   5.118  
   5.119  (* greetings to Tarski *)
   5.120  
   5.121 @@ -142,7 +134,6 @@
   5.122    | eval xs (IAbs (_, t)) = eval xs t
   5.123    | eval xs (ICase (_, t)) = eval xs t;
   5.124  
   5.125 -
   5.126  (* finally... *)
   5.127  
   5.128  fun nbe tab t = (counter :=0; xfun_tab := tab; to_term(eval [] t));