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