moved term_of syntax to separate theory
authorhaftmann
Tue Sep 16 16:13:06 2008 +0200 (2008-09-16)
changeset 2824384d90ec67059
parent 28242 f978c8e75118
child 28244 f433e544a855
moved term_of syntax to separate theory
src/HOL/Code_Eval.thy
src/HOL/IsaMakefile
src/HOL/ex/ROOT.ML
     1.1 --- a/src/HOL/Code_Eval.thy	Tue Sep 16 15:37:33 2008 +0200
     1.2 +++ b/src/HOL/Code_Eval.thy	Tue Sep 16 16:13:06 2008 +0200
     1.3 @@ -61,11 +61,13 @@
     1.4          $ Free ("x", ty);
     1.5        val rhs = @{term "undefined \<Colon> term"};
     1.6        val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs));
     1.7 +      fun triv_name_of t = (fst o dest_Free o fst o strip_comb o fst
     1.8 +        o HOLogic.dest_eq o HOLogic.dest_Trueprop) t ^ "_triv";
     1.9      in
    1.10        thy
    1.11        |> TheoryTarget.instantiation ([tyco], vs, @{sort term_of})
    1.12        |> `(fn lthy => Syntax.check_term lthy eq)
    1.13 -      |-> (fn eq => Specification.definition (NONE, (Attrib.no_binding, eq)))
    1.14 +      |-> (fn eq => Specification.definition (NONE, ((Name.binding (triv_name_of eq), []), eq)))
    1.15        |> snd
    1.16        |> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
    1.17        |> LocalTheory.exit
    1.18 @@ -139,6 +141,12 @@
    1.19  lemma [code func, code func del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
    1.20  lemma [code func, code func del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" ..
    1.21  
    1.22 +lemma term_of_char [unfolded rtype_fun_def rtype_char_def rtype_nibble_def, code func]: "Code_Eval.term_of c =
    1.23 +    (let (n, m) = nibble_pair_of_char c
    1.24 +  in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''Pair'') (RTYPE(nibble \<Rightarrow> nibble \<Rightarrow> char)))
    1.25 +    (Code_Eval.term_of n)) (Code_Eval.term_of m))"
    1.26 +  by (subst term_of_anything) rule 
    1.27 +
    1.28  code_type "term"
    1.29    (SML "Term.term")
    1.30  
    1.31 @@ -149,72 +157,6 @@
    1.32    (SML "Message'_String.mk")
    1.33  
    1.34  
    1.35 -subsubsection {* Syntax *}
    1.36 -
    1.37 -print_translation {*
    1.38 -let
    1.39 -  val term = Const ("<TERM>", dummyT);
    1.40 -  fun tr1' [_, _] = term;
    1.41 -  fun tr2' [] = term;
    1.42 -in
    1.43 -  [(@{const_syntax Const}, tr1'),
    1.44 -    (@{const_syntax App}, tr1'),
    1.45 -    (@{const_syntax dummy_term}, tr2')]
    1.46 -end
    1.47 -*}
    1.48 -setup {*
    1.49 -  Sign.declare_const [] ((Name.binding "rterm_of", @{typ "'a \<Rightarrow> 'b"}), NoSyn)
    1.50 -  #> snd
    1.51 -*}
    1.52 -
    1.53 -notation (output)
    1.54 -  rterm_of ("\<guillemotleft>_\<guillemotright>")
    1.55 -
    1.56 -locale rterm_syntax =
    1.57 -  fixes rterm_of_syntax :: "'a \<Rightarrow> 'b" ("\<guillemotleft>_\<guillemotright>")
    1.58 -
    1.59 -parse_translation {*
    1.60 -let
    1.61 -  fun rterm_of_tr [t] = Lexicon.const @{const_name rterm_of} $ t
    1.62 -    | rterm_of_tr ts = raise TERM ("rterm_of_tr", ts);
    1.63 -in
    1.64 -  [(Syntax.fixedN ^ "rterm_of_syntax", rterm_of_tr)]
    1.65 -end
    1.66 -*}
    1.67 -
    1.68 -setup {*
    1.69 -let
    1.70 -  val subst_rterm_of = Eval.mk_term
    1.71 -    (fn (v, _) => error ("illegal free variable in term quotation: " ^ quote v))
    1.72 -    (RType.mk (fn (v, sort) => RType.rtype (TFree (v, sort))));
    1.73 -  fun subst_rterm_of' (Const (@{const_name rterm_of}, _), [t]) = subst_rterm_of t
    1.74 -    | subst_rterm_of' (Const (@{const_name rterm_of}, _), _) =
    1.75 -        error ("illegal number of arguments for " ^ quote @{const_name rterm_of})
    1.76 -    | subst_rterm_of' (t, ts) = list_comb (t, map (subst_rterm_of' o strip_comb) ts);
    1.77 -  fun subst_rterm_of'' t = 
    1.78 -    let
    1.79 -      val t' = subst_rterm_of' (strip_comb t);
    1.80 -    in if t aconv t'
    1.81 -      then NONE
    1.82 -      else SOME t'
    1.83 -    end;
    1.84 -  fun check_rterm_of ts ctxt =
    1.85 -    let
    1.86 -      val ts' = map subst_rterm_of'' ts;
    1.87 -    in if exists is_some ts'
    1.88 -      then SOME (map2 the_default ts ts', ctxt)
    1.89 -      else NONE
    1.90 -    end;
    1.91 -in
    1.92 -  Context.theory_map (Syntax.add_term_check 0 "rterm_of" check_rterm_of)
    1.93 -end;
    1.94 -*}
    1.95 -
    1.96 -hide const dummy_term
    1.97 -hide (open) const Const App
    1.98 -hide (open) const term_of
    1.99 -
   1.100 -
   1.101  subsection {* Evaluation setup *}
   1.102  
   1.103  ML {*
   1.104 @@ -245,4 +187,23 @@
   1.105    Value.add_evaluator ("code", Eval.eval_term o ProofContext.theory_of)
   1.106  *}
   1.107  
   1.108 +
   1.109 +subsubsection {* Syntax *}
   1.110 +
   1.111 +print_translation {*
   1.112 +let
   1.113 +  val term = Const ("<TERM>", dummyT);
   1.114 +  fun tr1' [_, _] = term;
   1.115 +  fun tr2' [] = term;
   1.116 +in
   1.117 +  [(@{const_syntax Const}, tr1'),
   1.118 +    (@{const_syntax App}, tr1'),
   1.119 +    (@{const_syntax dummy_term}, tr2')]
   1.120  end
   1.121 +*}
   1.122 +
   1.123 +hide const dummy_term
   1.124 +hide (open) const Const App
   1.125 +hide (open) const term_of
   1.126 +
   1.127 +end
     2.1 --- a/src/HOL/IsaMakefile	Tue Sep 16 15:37:33 2008 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Tue Sep 16 16:13:06 2008 +0200
     2.3 @@ -779,7 +779,8 @@
     2.4    ex/ReflectionEx.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy		\
     2.5    ex/Reflected_Presburger.thy ex/coopertac.ML				\
     2.6    ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy		\
     2.7 -  ex/Sudoku.thy ex/Tarski.thy ex/Unification.thy ex/document/root.bib	\
     2.8 +  ex/Sudoku.thy ex/Tarski.thy ex/Term_Of_Syntax.thy			\
     2.9 +  ex/Unification.thy ex/document/root.bib			\
    2.10    ex/document/root.tex ex/Meson_Test.thy ex/reflection.ML ex/set.thy	\
    2.11    ex/svc_funcs.ML ex/svc_test.thy	\
    2.12    ex/ImperativeQuicksort.thy	\
     3.1 --- a/src/HOL/ex/ROOT.ML	Tue Sep 16 15:37:33 2008 +0200
     3.2 +++ b/src/HOL/ex/ROOT.ML	Tue Sep 16 16:13:06 2008 +0200
     3.3 @@ -13,7 +13,8 @@
     3.4    "FuncSet",
     3.5    "Word",
     3.6    "Eval_Examples",
     3.7 -  "Quickcheck"
     3.8 +  "Quickcheck",
     3.9 +  "Term_Of_Syntax"
    3.10  ];
    3.11  
    3.12  no_document use_thy "Codegenerator";