src/HOL/Code_Eval.thy
changeset 28335 25326092cf9a
parent 28313 1742947952f8
child 28346 b8390cd56b8f
equal deleted inserted replaced
28334:7c693bb76366 28335:25326092cf9a
    14 subsubsection {* Terms and class @{text term_of} *}
    14 subsubsection {* Terms and class @{text term_of} *}
    15 
    15 
    16 datatype "term" = dummy_term
    16 datatype "term" = dummy_term
    17 
    17 
    18 definition
    18 definition
    19   Const :: "message_string \<Rightarrow> rtype \<Rightarrow> term"
    19   Const :: "message_string \<Rightarrow> typerep \<Rightarrow> term"
    20 where
    20 where
    21   "Const _ _ = dummy_term"
    21   "Const _ _ = dummy_term"
    22 
    22 
    23 definition
    23 definition
    24   App :: "term \<Rightarrow> term \<Rightarrow> term"
    24   App :: "term \<Rightarrow> term \<Rightarrow> term"
    25 where
    25 where
    26   "App _ _ = dummy_term"
    26   "App _ _ = dummy_term"
    27 
    27 
    28 code_datatype Const App
    28 code_datatype Const App
    29 
    29 
    30 class term_of = rtype +
    30 class term_of = typerep +
    31   fixes term_of :: "'a \<Rightarrow> term"
    31   fixes term_of :: "'a \<Rightarrow> term"
    32 
    32 
    33 lemma term_of_anything: "term_of x \<equiv> t"
    33 lemma term_of_anything: "term_of x \<equiv> t"
    34   by (rule eq_reflection) (cases "term_of x", cases t, simp)
    34   by (rule eq_reflection) (cases "term_of x", cases t, simp)
    35 
    35 
    80         curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of};
    80         curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort term_of};
    81       val vs = (map o apsnd) constrain_sort raw_vs;
    81       val vs = (map o apsnd) constrain_sort raw_vs;
    82       val ty = Type (tyco, map TFree vs);
    82       val ty = Type (tyco, map TFree vs);
    83     in
    83     in
    84       thy
    84       thy
    85       |> RType.perhaps_add_def tyco
    85       |> Typerep.perhaps_add_def tyco
    86       |> not has_inst ? add_term_of_def ty vs tyco
    86       |> not has_inst ? add_term_of_def ty vs tyco
    87     end;
    87     end;
    88 in
    88 in
    89   Code.type_interpretation interpretator
    89   Code.type_interpretation interpretator
    90 end
    90 end
    96     let
    96     let
    97       val t = list_comb (Const (c, tys ---> ty),
    97       val t = list_comb (Const (c, tys ---> ty),
    98         map Free (Name.names Name.context "a" tys));
    98         map Free (Name.names Name.context "a" tys));
    99     in (map_aterms (fn Free (v, ty) => Var ((v, 0), ty) | t => t) t, Eval.mk_term
    99     in (map_aterms (fn Free (v, ty) => Var ((v, 0), ty) | t => t) t, Eval.mk_term
   100       (fn (v, ty) => Eval.mk_term_of ty (Var ((v, 0), ty)))
   100       (fn (v, ty) => Eval.mk_term_of ty (Var ((v, 0), ty)))
   101       (RType.mk (fn (v, sort) => RType.rtype (TFree (v, sort)))) t)
   101       (Typerep.mk (fn (v, sort) => Typerep.typerep (TFree (v, sort)))) t)
   102     end;
   102     end;
   103   fun prove_term_of_eq ty eq thy =
   103   fun prove_term_of_eq ty eq thy =
   104     let
   104     let
   105       val cty = Thm.ctyp_of thy ty;
   105       val cty = Thm.ctyp_of thy ty;
   106       val (arg, rhs) = pairself (Thm.cterm_of thy) eq;
   106       val (arg, rhs) = pairself (Thm.cterm_of thy) eq;
   135 subsubsection {* Code generator setup *}
   135 subsubsection {* Code generator setup *}
   136 
   136 
   137 lemmas [code func del] = term.recs term.cases term.size
   137 lemmas [code func del] = term.recs term.cases term.size
   138 lemma [code func, code func del]: "(t1\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" ..
   138 lemma [code func, code func del]: "(t1\<Colon>term) = t2 \<longleftrightarrow> t1 = t2" ..
   139 
   139 
   140 lemma [code func, code func del]: "(term_of \<Colon> rtype \<Rightarrow> term) = term_of" ..
   140 lemma [code func, code func del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
   141 lemma [code func, code func del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
   141 lemma [code func, code func del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..
   142 lemma [code func, code func del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" ..
   142 lemma [code func, code func del]: "(term_of \<Colon> message_string \<Rightarrow> term) = term_of" ..
   143 
   143 
   144 lemma term_of_char [unfolded rtype_fun_def rtype_char_def rtype_nibble_def, code func]: "Code_Eval.term_of c =
   144 lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_nibble_def, code func]: "Code_Eval.term_of c =
   145     (let (n, m) = nibble_pair_of_char c
   145     (let (n, m) = nibble_pair_of_char c
   146   in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''Pair'') (RTYPE(nibble \<Rightarrow> nibble \<Rightarrow> char)))
   146   in Code_Eval.App (Code_Eval.App (Code_Eval.Const (STR ''Pair'') (TYPEREP(nibble \<Rightarrow> nibble \<Rightarrow> char)))
   147     (Code_Eval.term_of n)) (Code_Eval.term_of m))"
   147     (Code_Eval.term_of n)) (Code_Eval.term_of m))"
   148   by (subst term_of_anything) rule 
   148   by (subst term_of_anything) rule 
   149 
   149 
   150 code_type "term"
   150 code_type "term"
   151   (SML "Term.term")
   151   (SML "Term.term")