# HG changeset patch # User haftmann # Date 1201776283 -3600 # Node ID ffe1a032d24b96f87cf86006466fdd4655f86b74 # Parent ecbfe264569446a2ea39dabf7834356eac352540 proper term_of functions diff -r ecbfe2645694 -r ffe1a032d24b src/HOL/Library/Eval.thy --- a/src/HOL/Library/Eval.thy Thu Jan 31 09:16:01 2008 +0100 +++ b/src/HOL/Library/Eval.thy Thu Jan 31 11:44:43 2008 +0100 @@ -21,39 +21,8 @@ Type message_string "typ list" | TFree vname sort -abbreviation - Fun :: "typ \ typ \ typ" where - "Fun ty1 ty2 \ Type (STR ''fun'') [ty1, ty2]" - -locale (open) pure_term_syntax = -- {* FIXME drop this *} - fixes pure_term_Type :: "message_string \ typ list \ typ" (infixl "{\}" 120) - and pure_term_TFree :: "vname \ sort \ typ" ("\_\_\" [118, 118] 117) - and pure_term_Fun :: "typ \ typ \ typ" (infixr "\" 114) - -parse_translation {* -let - fun Type_tr [tyco, tys] = Lexicon.const @{const_syntax Type} $ tyco $ tys - | Type_tr ts = raise TERM ("Type_tr", ts); - fun TFree_tr [v, sort] = Lexicon.const @{const_syntax TFree} $ v $ sort - | TFree_tr ts = raise TERM ("TFree_tr", ts); - fun Fun_tr [ty1, ty2] = Lexicon.const @{const_syntax Fun} $ ty1 $ ty2 - | Fun_tr ts = raise TERM("Fun_tr", ts); -in [ - ("\<^fixed>pure_term_Type", Type_tr), - ("\<^fixed>pure_term_TFree", TFree_tr), - ("\<^fixed>pure_term_Fun", Fun_tr) -] end -*} - -notation (output) - Type (infixl "{\}" 120) -and - TFree ("\_\_\" [118, 118] 117) -and - Fun (infixr "\" 114) - ML {* -structure Eval_Aux = +structure Eval = struct val mk_sort = HOLogic.mk_list @{typ class} o map Message_String.mk; @@ -74,81 +43,54 @@ fixes typ_of :: "'a\{} itself \ typ" ML {* -structure Eval_Aux = +structure Eval = struct -open Eval_Aux; +open Eval; fun mk_typ_of ty = Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ}) $ Logic.mk_type ty; +fun add_typ_of_def tyco thy = + let + val sorts = replicate (Sign.arity_number thy tyco) @{sort typ_of}; + val vs = Name.names Name.context "'a" sorts; + val ty = Type (tyco, map TFree vs); + val lhs = Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ}) + $ Free ("T", Term.itselfT ty); + val rhs = mk_typ (fn v => mk_typ_of (TFree v)) ty; + val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); + in + thy + |> TheoryTarget.instantiation ([tyco], vs, @{sort typ_of}) + |> `(fn lthy => Syntax.check_term lthy eq) + |-> (fn eq => Specification.definition (NONE, (("", []), eq))) + |> snd + |> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) + |> LocalTheory.exit + |> ProofContext.theory_of + end; + end *} -setup {* +(*setup {* let - open Eval_Aux; - fun define_typ_of ty lthy = - let - val lhs = Const (@{const_name typ_of}, Term.itselfT ty --> @{typ typ}) - $ Free ("T", Term.itselfT ty); - val rhs = mk_typ (fn v => mk_typ_of (TFree v)) ty; - val eq = Syntax.check_term lthy (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))) - in lthy |> Specification.definition (NONE, (("", []), eq)) end; - fun interpretator tyco thy = - let - val sorts = replicate (Sign.arity_number thy tyco) @{sort typ_of}; - val vs = Name.names Name.context "'a" sorts; - val ty = Type (tyco, map TFree vs); - in - thy - |> TheoryTarget.instantiation ([tyco], vs, @{sort typ_of}) - |> define_typ_of ty - |> snd - |> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) - |> LocalTheory.exit - |> ProofContext.theory_of - end; -in TypedefPackage.interpretation interpretator end -*} - -instantiation "prop" :: typ_of -begin - -definition - "typ_of (T\prop itself) = Type (STR ''prop'') []" - -instance .. - + open Eval; +in + Eval.add_typ_of_def @{type_name prop} + #> Eval.add_typ_of_def @{type_name itself} + #> Eval.add_typ_of_def @{type_name bool} + #> Eval.add_typ_of_def @{type_name set} + #> TypedefPackage.interpretation Eval.add_typ_of_def end - -instantiation itself :: (typ_of) typ_of -begin - -definition - "typ_of (T\'a itself itself) = Type (STR ''itself'') [typ_of TYPE('a\typ_of)]" - -instance .. - -end - -instantiation set :: (typ_of) typ_of -begin - -definition - "typ_of (T\'a set itself) = Type (STR ''set'') [typ_of TYPE('a\typ_of)]" - -instance .. - -end - +*}*) subsubsection {* Code generator setup *} lemma [code func]: - includes pure_term_syntax - shows "tyco1 {\} tys1 = tyco2 {\} tys2 \ tyco1 = tyco2 + "Type tyco1 tys1 = Type tyco2 tys2 \ tyco1 = tyco2 \ list_all2 (op =) tys1 tys2" by (auto simp add: list_all2_eq [symmetric]) @@ -161,32 +103,38 @@ code_reserved SML Term - subsection {* Term representation *} -subsubsection {* Definition *} +subsubsection {* Definitions *} + +datatype "term" = dummy_term -datatype "term" = - Const message_string "typ" (infix "\\" 112) - | Fix vname "typ" (infix ":\" 112) - | App "term" "term" (infixl "\" 110) - | Abs "vname \ typ" "term" (infixr "\" 111) - | Bnd nat +definition + Const :: "message_string \ typ \ term" +where + "Const _ _ = dummy_term" -code_datatype Const App Fix +definition + App :: "term \ term \ term" +where + "App _ _ = dummy_term" + +code_datatype Const App -abbreviation - Apps :: "term \ term list \ term" (infixl "{\}" 110) where - "t {\} ts \ foldl (op \) t ts" -abbreviation - Abss :: "(vname \ typ) list \ term \ term" (infixr "{\}" 111) where - "vs {\} t \ foldr (op \) vs t" +subsubsection {* Class @{term term_of} *} + +class term_of = typ_of + + constrains typ_of :: "'a\{} itself \ typ" + fixes term_of :: "'a \ term" + +lemma term_of_anything: "term_of x \ t" + by (rule eq_reflection) (cases "term_of x", cases t, simp) ML {* -structure Eval_Aux = +structure Eval = struct -open Eval_Aux; +open Eval; fun mk_term f g (Const (c, ty)) = @{term Const} $ Message_String.mk c $ g ty @@ -194,156 +142,102 @@ @{term App} $ mk_term f g t1 $ mk_term f g t2 | mk_term f g (Free v) = f v; -end; -*} - - -subsubsection {* Class @{text term_of} *} - -class term_of = typ_of + - constrains typ_of :: "'a\{} itself \ typ" - fixes term_of :: "'a \ term" - -ML {* -structure Eval_Aux = -struct - -open Eval_Aux; - -local - fun term_term_of ty = - Const (@{const_name term_of}, ty --> @{typ term}); -in - val class_term_of = Sign.intern_class @{theory} "term_of"; - fun mk_terms_of_defs vs (tyco, cs) = - let - val dty = Type (tyco, map TFree vs); - fun mk_eq c = - let - val lhs : term = term_term_of dty $ c; - val rhs : term = mk_term - (fn (v, ty) => term_term_of ty $ Free (v, ty)) - (mk_typ (fn (v, sort) => mk_typ_of (TFree (v, sort)))) c - in - HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)) - end; - in map mk_eq cs end; - fun mk_term_of t = - term_term_of (Term.fastype_of t) $ t; -end; +fun mk_term_of ty t = Const (@{const_name term_of}, ty --> @{typ term}) $ t; end; *} setup {* let - open Eval_Aux; - fun thy_note ((name, atts), thms) = - PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms)); - fun thy_def ((name, atts), t) = - PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm)); - fun prep_dtyp thy vs tyco = - let - val (_, cs) = DatatypePackage.the_datatype_spec thy tyco; - val prep_typ = map_atyps (fn TFree (v, sort) => - TFree (v, (the o AList.lookup (op =) vs) v)); - fun prep_c (c, tys) = list_comb (Const (c, tys ---> Type (tyco, map TFree vs)), - map Free (Name.names Name.context "a" tys)); - in (tyco, map (prep_c o (apsnd o map) prep_typ) cs) end; - fun prep thy tycos = + fun has_no_inst tyco sort thy = + not (can (Sorts.mg_domain (Sign.classes_of thy) tyco) + sort); + fun add_term_of_def ty vs tyco thy = let - val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of}; - val tyco = hd tycos; - val (vs_proto, _) = DatatypePackage.the_datatype_spec thy tyco; - val all_typs = maps (maps snd o snd o DatatypePackage.the_datatype_spec thy) tycos; - fun add_tycos (Type (tyco, tys)) = insert (op =) tyco #> - fold add_tycos tys - | add_tycos _ = I; - val dep_tycos = [] |> fold add_tycos all_typs |> subtract (op =) tycos; - val sorts = map (inter_sort o snd) vs_proto; - val vs = map fst vs_proto ~~ sorts; - val css = map (prep_dtyp thy vs) tycos; - val defs = map (mk_terms_of_defs vs) css; - in if forall (fn tyco => can (Sign.arity_sorts thy tyco) @{sort term_of}) dep_tycos - andalso not (tycos = [@{type_name typ}]) - then SOME (vs, defs) - else NONE - end; - fun prep' ctxt proto_eqs = - let - val eqs as eq :: _ = map (Syntax.check_term ctxt) proto_eqs; - val (Free (v, ty), _) = - (strip_comb o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) eq; - in ((v, SOME ty, NoSyn), map (pair ("", [])) eqs) end; - fun primrec primrecs ctxt = - let - val (fixes, eqnss) = split_list (map (prep' ctxt) primrecs); - in PrimrecPackage.add_primrec fixes (flat eqnss) ctxt end; - fun interpretator tycos thy = case prep thy tycos - of SOME (vs, defs) => + val lhs = Const (@{const_name term_of}, ty --> @{typ term}) + $ Free ("x", ty); + val rhs = @{term "undefined \ term"}; + val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)); + in thy - |> TheoryTarget.instantiation (tycos, vs, @{sort term_of}) - |> primrec defs + |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of}) + |> `(fn lthy => Syntax.check_term lthy eq) + |-> (fn eq => Specification.definition (NONE, (("", []), eq))) |> snd |> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) |> LocalTheory.exit |> ProofContext.theory_of - | NONE => thy; - in DatatypePackage.interpretation interpretator end + end; + fun interpretator (tyco, (raw_vs, _)) thy = + let + val constrain_sort = + curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of}; + val vs = (map o apsnd) constrain_sort raw_vs; + val ty = Type (tyco, map TFree vs); + in + thy + |> `(has_no_inst tyco @{sort typ_of}) + |-> (fn no_typ_of => no_typ_of ? Eval.add_typ_of_def tyco) + |> `(has_no_inst tyco @{sort term_of}) + |-> (fn no_term_of => no_term_of ? add_term_of_def ty vs tyco) + end; +in + Code.type_interpretation interpretator +end *} -abbreviation (in pure_term_syntax) (input) - intT :: "typ" -where - "intT \ Type (STR ''Int.int'') []" - -abbreviation (in pure_term_syntax) (input) - bitT :: "typ" -where - "bitT \ Type (STR ''Int.bit'') []" - -function (in pure_term_syntax) - mk_int :: "int \ term" -where - "mk_int k = (if k = 0 then STR ''Int.Pls'' \\ intT - else if k = -1 then STR ''Int.Min'' \\ intT - else let (l, m) = divAlg (k, 2) - in STR ''Int.Bit'' \\ intT \ bitT \ intT \ mk_int l \ - (if m = 0 then STR ''Int.bit.B0'' \\ bitT else STR ''Int.bit.B1'' \\ bitT))" -by pat_completeness auto -termination (in pure_term_syntax) -by (relation "measure (nat o abs)") (auto simp add: divAlg_mod_div) - -declare pure_term_syntax.mk_int.simps [code func] - -definition (in pure_term_syntax) - "term_of_int_aux k = STR ''Int.number_class.number_of'' \\ intT \ intT \ mk_int k" - -declare pure_term_syntax.term_of_int_aux_def [code func] - -instantiation int :: term_of -begin - -definition - "term_of = pure_term_syntax.term_of_int_aux" - -instance .. - +setup {* +let + fun mk_term_of_eq ty vs tyco (c, tys) = + let + val t = list_comb (Const (c, tys ---> ty), + map Free (Name.names Name.context "a" tys)); + in (map_aterms (fn Free (v, ty) => Var ((v, 0), ty) | t => t) t, Eval.mk_term + (fn (v, ty) => Eval.mk_term_of ty (Var ((v, 0), ty))) + (Eval.mk_typ (fn (v, sort) => Eval.mk_typ_of (TFree (v, sort)))) t) + end; + fun prove_term_of_eq ty eq thy = + let + val cty = Thm.ctyp_of thy ty; + val (arg, rhs) = pairself (Thm.cterm_of thy) eq; + val thm = @{thm term_of_anything} + |> Drule.instantiate' [SOME cty] [SOME arg, SOME rhs] + |> Thm.varifyT; + in + thy + |> Code.add_func thm + end; + fun interpretator (tyco, (raw_vs, raw_cs)) thy = + let + val constrain_sort = + curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of}; + val vs = (map o apsnd) constrain_sort raw_vs; + val cs = (map o apsnd o map o map_atyps) + (fn TFree (v, sort) => TFree (v, constrain_sort sort)) raw_cs; + val ty = Type (tyco, map TFree vs); + val eqs = map (mk_term_of_eq ty vs tyco) cs; + val const = AxClass.param_of_inst thy (@{const_name term_of}, tyco); + in + thy + |> Code.del_funcs const + |> fold (prove_term_of_eq ty) eqs + end; +in + Code.type_interpretation interpretator end - +*} subsubsection {* Code generator setup *} lemmas [code func del] = term.recs term.cases term.size -lemmas [code func del] = term_of_message_string.simps lemma [code func, code func del]: "(t1\term) = t2 \ t1 = t2" .. +lemma [code func, code func del]: "(term_of \ message_string \ term) = term_of" .. code_type "term" (SML "Term.term") -code_const Const and App and Fix - (SML "Term.Const/ (_, _)" and "Term.$/ (_, _)" and "Term.Free/ (_, _)") - +code_const Const and App + (SML "Term.Const/ (_, _)" and "Term.$/ (_, _)") subsection {* Evaluation setup *} @@ -354,18 +248,21 @@ val eval_term: theory -> term -> term val evaluate: Proof.context -> term -> unit val evaluate': string -> Proof.context -> term -> unit - val evaluate_cmd: string option -> Toplevel.state -> unit + val evaluate_cmd: string option -> string -> Toplevel.state -> unit end; -structure Eval = +structure Eval : EVAL = struct +open Eval; + val eval_ref = ref (NONE : (unit -> term) option); -fun eval_term thy = - Eval_Aux.mk_term_of - #> (fn t => CodePackage.eval_term ("Eval.eval_ref", eval_ref) thy t []) - #> Code.postprocess_term thy; +fun eval_term thy t = + t + |> Eval.mk_term_of (fastype_of t) + |> (fn t => CodePackage.eval_term ("Eval.eval_ref", eval_ref) thy t []) + |> Code.postprocess_term thy; val evaluators = [ ("code", eval_term), @@ -411,4 +308,6 @@ (Eval.evaluate_cmd some_name t))); *} +hide (open) const Type TFree Const App dummy_term typ_of term_of + end diff -r ecbfe2645694 -r ffe1a032d24b src/HOL/ex/Eval_Examples.thy --- a/src/HOL/ex/Eval_Examples.thy Thu Jan 31 09:16:01 2008 +0100 +++ b/src/HOL/ex/Eval_Examples.thy Thu Jan 31 11:44:43 2008 +0100 @@ -60,7 +60,7 @@ value ("normal_form") "max (2::int) 4" value "of_int 2 / of_int 4 * (1::rat)" -(*value (code) "of_int 2 / of_int 4 * (1::rat)"*) +value (code) "of_int 2 / of_int 4 * (1::rat)" value (SML) "of_int 2 / of_int 4 * (1::rat)" value ("normal_form") "of_int 2 / of_int 4 * (1::rat)"