|
1 (* |
|
2 ID: $Id$ |
|
3 Author: Tobias Mayr |
|
4 |
|
5 Additional theory file section for HOLCF: axioms |
|
6 There's an elaborate but german description of this program |
|
7 and a short english description of the new sections, |
|
8 write to mayrt@informatik.tu-muenchen.de. |
|
9 |
|
10 TODO: |
|
11 |
|
12 *) |
|
13 |
|
14 (*** new section of HOLCF : axioms |
|
15 since rules are already internally called axioms, |
|
16 the new section is internally called ext_axioms res. eaxms *) |
|
17 |
|
18 signature THY_AXIOMS = |
|
19 sig |
|
20 (* theory extenders : *) |
|
21 val add_ext_axioms : (string * string) list -> (string * string) list |
|
22 -> (string * string) list -> theory -> theory; |
|
23 val add_ext_axioms_i : (string * (typ option)) list -> |
|
24 (string * (typ option)) list -> |
|
25 (string * term) list -> theory -> theory; |
|
26 val axioms_keywords : string list; |
|
27 val axioms_sections : (string * (ThyParse.token list -> |
|
28 (string * string) * ThyParse.token list)) list; |
|
29 end; |
|
30 |
|
31 structure ThyAxioms : THY_AXIOMS = |
|
32 struct |
|
33 |
|
34 open HOLCFlogic; |
|
35 |
|
36 (** library ******************************************************) |
|
37 |
|
38 fun apsnd_of_three f = fn (a,b,c) => (a,f b,c); |
|
39 |
|
40 fun is_elem e list = exists (fn y => e=y) list |
|
41 |
|
42 fun without l1 l2 = (* l1 without the elements of l2 *) |
|
43 filter (fn x => (not (is_elem x l2))) l1; |
|
44 |
|
45 fun conc [e:string] = e |
|
46 | conc (head::tail) = head^", "^(conc tail) |
|
47 | conc [] = ""; |
|
48 |
|
49 fun appear varlist = (* all (x,_) for which (x,_) is in varlist *) |
|
50 filter (fn x => (exists (fn y => (fst x)=(fst y)) varlist)) |
|
51 |
|
52 |
|
53 (* all non unique elements of a list *) |
|
54 fun doubles (hd::tl) = if (is_elem hd tl) |
|
55 then (hd::(doubles tl)) |
|
56 else (doubles tl) |
|
57 | doubles _ = []; |
|
58 |
|
59 |
|
60 (* The main functions are the section parser ext_axiom_decls and the |
|
61 theory extender add_ext_axioms. *) |
|
62 |
|
63 (** theory extender : add_ext_axioms *) |
|
64 |
|
65 (* forms a function from constrained varnames to their constraints |
|
66 these constraints are then used local to each axiom, as an argument |
|
67 of read_def_cterm. Called by add_ext_axioms. *) |
|
68 fun get_constraints_of_str sign ((vname,vtyp)::tail) = |
|
69 if (vtyp <> "") |
|
70 then ((fn (x,_)=> if x=vname |
|
71 then Some (#T (rep_ctyp (read_ctyp sign vtyp))) |
|
72 else raise Match) |
|
73 orelf (get_constraints_of_str sign tail)) |
|
74 else (get_constraints_of_str sign tail) |
|
75 | get_constraints_of_str sign [] = K None; |
|
76 |
|
77 (* does the same job for allready parsed optional constraints. |
|
78 Called by add_ext_axioms_i. *) |
|
79 fun get_constraints_of_typ sign ((vname,vtyp)::tail) = |
|
80 if (is_some vtyp) |
|
81 then ((fn (x,_)=> if x=vname |
|
82 then vtyp |
|
83 else raise Match) |
|
84 orelf (get_constraints_of_typ sign tail)) |
|
85 else (get_constraints_of_typ sign tail) |
|
86 | get_constraints_of_typ sign [] = K None; |
|
87 |
|
88 |
|
89 (* applies mkNotEqUU_in on the axiom and every Free that appears in the list |
|
90 and in the axiom. Called by check_and_extend. *) |
|
91 fun add_prem axiom [] = axiom |
|
92 | add_prem axiom (vname::tl) = |
|
93 let val vterm = find_first (fn x => ((#1 o dest_Free) x = vname)) |
|
94 (term_frees axiom) |
|
95 in |
|
96 add_prem |
|
97 (if (is_some vterm) |
|
98 then mkNotEqUU_in (the vterm) axiom |
|
99 else axiom) |
|
100 tl |
|
101 end |
|
102 |
|
103 (* checks for uniqueness and completeness of var/defvar declarations, |
|
104 and enriches the axiom term with premises. Called by add_ext_axioms(_i).*) |
|
105 fun check_and_extend sign defvarl varl axiom = |
|
106 let |
|
107 val names_of_frees = map (fst o dest_Free) |
|
108 (term_frees axiom); |
|
109 val all_decl_varnames = (defvarl @ varl); |
|
110 val undeclared = without names_of_frees all_decl_varnames; |
|
111 val doubles = doubles all_decl_varnames |
|
112 in |
|
113 if (doubles <> []) |
|
114 then |
|
115 (error("Multiple declarations of one identifier in section axioms :\n" |
|
116 ^(conc doubles))) |
|
117 else (); |
|
118 if (undeclared <> []) |
|
119 then |
|
120 (error("Undeclared identifiers in section axioms : \n" |
|
121 ^(conc undeclared))) |
|
122 else (); |
|
123 add_prem axiom (rev defvarl) |
|
124 end; |
|
125 |
|
126 (* the next five only differ from the original add_axioms' subfunctions |
|
127 in the constraints argument for read_def_cterm *) |
|
128 local |
|
129 fun err_in_axm name = |
|
130 error ("The error(s) above occurred in axiom " ^ quote name); |
|
131 |
|
132 fun no_vars tm = |
|
133 if null (term_vars tm) andalso null (term_tvars tm) then tm |
|
134 else error "Illegal schematic variable(s) in term"; |
|
135 |
|
136 fun read_ext_cterm sign constraints = |
|
137 #1 o read_def_cterm (sign, constraints, K None) [] true; |
|
138 |
|
139 (* only for add_ext_axioms (working on strings) *) |
|
140 fun read_ext_axm sg constraints (name,str) = |
|
141 (name, no_vars (term_of (read_ext_cterm sg constraints (str, propT)))) |
|
142 handle ERROR => err_in_axm name; |
|
143 |
|
144 (* only for add_ext_axioms_i (working on terms) *) |
|
145 fun read_ext_axm_terms sg constraints (name,term) = |
|
146 (name, no_vars (#2(Sign.infer_types sg constraints (K None) [] true |
|
147 ([term], propT)))) |
|
148 handle ERROR => err_in_axm name; |
|
149 |
|
150 in |
|
151 |
|
152 (******* THE THEORY EXTENDERS THEMSELVES *****) |
|
153 fun add_ext_axioms varlist defvarlist axioms theory = |
|
154 let val {sign, ...} = rep_theory theory; |
|
155 val constraints = get_constraints_of_str sign (defvarlist@varlist) |
|
156 in |
|
157 add_axioms_i (map (apsnd |
|
158 (check_and_extend sign (map fst defvarlist) (map fst varlist)) o |
|
159 (read_ext_axm sign constraints)) axioms) theory |
|
160 end |
|
161 |
|
162 fun add_ext_axioms_i varlist defvarlist axiom_terms theory = |
|
163 let val {sign, ...} = rep_theory theory; |
|
164 val constraints = get_constraints_of_typ sign (defvarlist@varlist) |
|
165 in |
|
166 add_axioms_i (map (apsnd (check_and_extend sign |
|
167 (map fst defvarlist) (map fst varlist)) o |
|
168 (read_ext_axm_terms sign constraints)) axiom_terms) theory |
|
169 end |
|
170 end; |
|
171 |
|
172 |
|
173 (******** SECTION PARSER : ext_axiom_decls **********) |
|
174 local |
|
175 open ThyParse |
|
176 |
|
177 (* as in the pure section 'rules' : |
|
178 making the "val thmname = get_axiom thy thmname" list *) |
|
179 val mk_list_of_pairs = mk_big_list o map (mk_pair o apfst quote); |
|
180 fun mk_val ax = "val " ^ ax ^ " = get_axiom thy " ^ quote ax ^ ";"; |
|
181 val mk_vals = cat_lines o map mk_val; |
|
182 |
|
183 (* making the call for the theory extender *) |
|
184 fun mk_eaxms_decls ((vars,defvars),axms) = |
|
185 ( "|> ThyAxioms.add_ext_axioms \n " ^ |
|
186 (mk_list_of_pairs vars) ^ "\n " ^ |
|
187 (mk_list_of_pairs defvars) ^ "\n " ^ |
|
188 (mk_list_of_pairs axms), |
|
189 mk_vals (map fst axms)); |
|
190 |
|
191 (* parsing the concrete syntax *) |
|
192 |
|
193 val axiom_decls = (repeat1 (ident -- !! string)); |
|
194 |
|
195 val varlist = "vars" $$-- |
|
196 repeat1 (ident -- optional ("::" $$-- string) "\"\""); |
|
197 |
|
198 val defvarlist = "defvars" $$-- |
|
199 repeat1 (ident -- optional ("::" $$-- string) "\"\""); |
|
200 |
|
201 in |
|
202 |
|
203 val ext_axiom_decls = (optional varlist []) -- (optional defvarlist []) |
|
204 -- ("in" $$-- axiom_decls) >> mk_eaxms_decls; |
|
205 end; (* local *) |
|
206 |
|
207 |
|
208 (**** new keywords and sections ************************************) |
|
209 |
|
210 val axioms_keywords = ["vars", "defvars","in"]; |
|
211 (* "::" is already a pure keyword *) |
|
212 |
|
213 val axioms_sections = [("axioms" , ext_axiom_decls)] |
|
214 |
|
215 end; (* the structure *) |
|
216 |