|
1 (* Title: HOL/Library/Pure_term.thy |
|
2 ID: $Id$ |
|
3 Author: Florian Haftmann, TU Muenchen |
|
4 *) |
|
5 |
|
6 header {* Embedding (a subset of) the Pure term algebra in HOL *} |
|
7 |
|
8 theory Pure_term |
|
9 imports MLString |
|
10 begin |
|
11 |
|
12 subsection {* Definitions *} |
|
13 |
|
14 types vname = ml_string; |
|
15 types "class" = ml_string; |
|
16 types sort = "class list" |
|
17 |
|
18 datatype "typ" = |
|
19 Type ml_string "typ list" (infix "{\<struct>}" 120) |
|
20 | TFix vname sort (infix "\<Colon>\<epsilon>" 117) |
|
21 |
|
22 abbreviation |
|
23 Fun :: "typ \<Rightarrow> typ \<Rightarrow> typ" (infixr "\<rightarrow>" 115) where |
|
24 "ty1 \<rightarrow> ty2 \<equiv> Type (STR ''fun'') [ty1, ty2]" |
|
25 abbreviation |
|
26 Funs :: "typ list \<Rightarrow> typ \<Rightarrow> typ" (infixr "{\<rightarrow>}" 115) where |
|
27 "tys {\<rightarrow>} ty \<equiv> foldr (op \<rightarrow>) tys ty" |
|
28 |
|
29 datatype "term" = |
|
30 Const ml_string "typ" (infix "\<Colon>\<subseteq>" 112) |
|
31 | Fix vname "typ" (infix ":\<epsilon>" 112) |
|
32 | App "term" "term" (infixl "\<bullet>" 110) |
|
33 | Abs "vname \<times> typ" "term" (infixr "\<mapsto>" 111) |
|
34 | Bnd nat |
|
35 |
|
36 abbreviation |
|
37 Apps :: "term \<Rightarrow> term list \<Rightarrow> term" (infixl "{\<bullet>}" 110) where |
|
38 "t {\<bullet>} ts \<equiv> foldl (op \<bullet>) t ts" |
|
39 abbreviation |
|
40 Abss :: "(vname \<times> typ) list \<Rightarrow> term \<Rightarrow> term" (infixr "{\<mapsto>}" 111) where |
|
41 "vs {\<mapsto>} t \<equiv> foldr (op \<mapsto>) vs t" |
|
42 |
|
43 |
|
44 subsection {* ML interface *} |
|
45 |
|
46 ML {* |
|
47 structure Pure_term = |
|
48 struct |
|
49 |
|
50 val mk_sort = HOLogic.mk_list @{typ class} o map MLString.mk; |
|
51 |
|
52 fun mk_typ f (Type (tyco, tys)) = |
|
53 @{term Type} $ MLString.mk tyco |
|
54 $ HOLogic.mk_list @{typ typ} (map (mk_typ f) tys) |
|
55 | mk_typ f (TFree v) = |
|
56 f v; |
|
57 |
|
58 fun mk_term f g (Const (c, ty)) = |
|
59 @{term Const} $ MLString.mk c $ g ty |
|
60 | mk_term f g (t1 $ t2) = |
|
61 @{term App} $ mk_term f g t1 $ mk_term f g t2 |
|
62 | mk_term f g (Free v) = f v; |
|
63 |
|
64 end; |
|
65 *} |
|
66 |
|
67 |
|
68 subsection {* Code generator setup *} |
|
69 |
|
70 definition |
|
71 Bound :: "int \<Rightarrow> term" |
|
72 where |
|
73 "Bound k = Bnd (nat k)" |
|
74 |
|
75 lemma Bnd_Bound [code inline, code func]: |
|
76 "Bnd n = Bound (int n)" |
|
77 unfolding Bound_def by auto |
|
78 |
|
79 definition |
|
80 Absp :: "vname \<Rightarrow> typ \<Rightarrow> term \<Rightarrow> term" |
|
81 where |
|
82 "Absp v ty t = (v, ty) \<mapsto> t" |
|
83 |
|
84 lemma Abs_Absp [code inline, code func]: |
|
85 "(op \<mapsto>) (v, ty) = Absp v ty" |
|
86 by rule (auto simp add: Absp_def) |
|
87 |
|
88 definition |
|
89 "term_case' f g h k l = term_case f g h (\<lambda>(v, ty). k v ty) (\<lambda>n. l (int n))" |
|
90 |
|
91 lemma term_case' [code inline, code func]: |
|
92 "term_case = (\<lambda>f g h k l. term_case' f g h (\<lambda>v ty. k (v, ty)) (\<lambda>v. l (nat v)))" |
|
93 unfolding term_case'_def by auto |
|
94 |
|
95 code_datatype Const App Fix Absp Bound |
|
96 lemmas [code func] = Bnd_Bound Abs_Absp |
|
97 |
|
98 code_type "typ" and "term" |
|
99 (SML "Term.typ" and "Term.term") |
|
100 |
|
101 code_const Type and TFix |
|
102 (SML "Term.Type/ (_, _)" and "Term.TFree/ (_, _)") |
|
103 |
|
104 code_const Const and App and Fix |
|
105 and Absp and Bound |
|
106 (SML "Term.Const/ (_, _)" and "Term.$/ (_, _)" and "Term.Free/ (_, _)" |
|
107 and "Term.Abs/ (_, _, _)" and "Term.Bound/ (IntInf.toInt/ _)") |
|
108 |
|
109 code_const term_rec and term_case and "size \<Colon> term \<Rightarrow> nat" |
|
110 (SML "!(_; _; _; _; _; raise Fail \"term'_rec\")" |
|
111 and "!(_; _; _; _; _; raise Fail \"term'_case\")" |
|
112 and "!(_; raise Fail \"size'_term\")") |
|
113 |
|
114 code_reserved SML Term |
|
115 |
|
116 end |