25 type cterm |
25 type cterm |
26 val rep_cterm : cterm -> {sign: Sign.sg, t: term, T: typ, maxidx: int} |
26 val rep_cterm : cterm -> {sign: Sign.sg, t: term, T: typ, maxidx: int} |
27 val term_of : cterm -> term |
27 val term_of : cterm -> term |
28 val cterm_of : Sign.sg -> term -> cterm |
28 val cterm_of : Sign.sg -> term -> cterm |
29 val read_cterm : Sign.sg -> string * typ -> cterm |
29 val read_cterm : Sign.sg -> string * typ -> cterm |
|
30 val read_cterms : Sign.sg -> string list * typ list -> cterm list |
30 val cterm_fun : (term -> term) -> (cterm -> cterm) |
31 val cterm_fun : (term -> term) -> (cterm -> cterm) |
31 val dest_cimplies : cterm -> cterm * cterm |
32 val dest_cimplies : cterm -> cterm * cterm |
32 val read_def_cterm : |
33 val read_def_cterm : |
33 Sign.sg * (indexname -> typ option) * (indexname -> sort option) -> |
34 Sign.sg * (indexname -> typ option) * (indexname -> sort option) -> |
34 string list -> bool -> string * typ -> cterm * (indexname * typ) list |
35 string list -> bool -> string * typ -> cterm * (indexname * typ) list |
189 fun term_of (Cterm {t, ...}) = t; |
190 fun term_of (Cterm {t, ...}) = t; |
190 |
191 |
191 (*create a cterm by checking a "raw" term with respect to a signature*) |
192 (*create a cterm by checking a "raw" term with respect to a signature*) |
192 fun cterm_of sign tm = |
193 fun cterm_of sign tm = |
193 let val (t, T, maxidx) = Sign.certify_term sign tm |
194 let val (t, T, maxidx) = Sign.certify_term sign tm |
194 in Cterm {sign = sign, t = t, T = T, maxidx = maxidx} |
195 in Cterm {sign = sign, t = t, T = T, maxidx = maxidx} |
195 end handle TYPE (msg, _, _) |
196 end; |
196 => raise TERM ("Term not in signature\n" ^ msg, [tm]); |
|
197 |
197 |
198 fun cterm_fun f (Cterm {sign, t, ...}) = cterm_of sign (f t); |
198 fun cterm_fun f (Cterm {sign, t, ...}) = cterm_of sign (f t); |
199 |
199 |
200 |
200 |
201 (*dest_implies for cterms. Note T=prop below*) |
201 (*dest_implies for cterms. Note T=prop below*) |
215 handle TYPE (msg, _, _) => error msg; |
215 handle TYPE (msg, _, _) => error msg; |
216 val ts = Syntax.read (#syn (Sign.rep_sg sign)) T' a; |
216 val ts = Syntax.read (#syn (Sign.rep_sg sign)) T' a; |
217 val (_, t', tye) = |
217 val (_, t', tye) = |
218 Sign.infer_types sign types sorts used freeze (ts, T'); |
218 Sign.infer_types sign types sorts used freeze (ts, T'); |
219 val ct = cterm_of sign t' |
219 val ct = cterm_of sign t' |
220 handle TERM (msg, _) => error msg; |
220 handle TYPE arg => error (Sign.exn_type_msg sign arg) |
|
221 | TERM (msg, _) => error msg; |
221 in (ct, tye) end; |
222 in (ct, tye) end; |
222 |
223 |
223 fun read_cterm sign = #1 o read_def_cterm (sign, K None, K None) [] true; |
224 fun read_cterm sign = #1 o read_def_cterm (sign, K None, K None) [] true; |
|
225 |
|
226 (*read a list of terms, matching them against a list of expected types. |
|
227 NO disambiguation of alternative parses via type-checking -- it is just |
|
228 not practical.*) |
|
229 fun read_cterms sign (bs, Ts) = |
|
230 let |
|
231 val {tsig, syn, ...} = Sign.rep_sg sign |
|
232 fun read (b,T) = |
|
233 case Syntax.read syn T b of |
|
234 [t] => t |
|
235 | _ => error("Error or ambiguity in parsing of " ^ b) |
|
236 val (us,_) = Type.infer_types(tsig, Sign.const_type sign, |
|
237 K None, K None, |
|
238 [], true, |
|
239 map (Sign.certify_typ sign) Ts, |
|
240 map read (bs~~Ts)) |
|
241 in map (cterm_of sign) us end |
|
242 handle TYPE arg => error (Sign.exn_type_msg sign arg) |
|
243 | TERM (msg, _) => error msg; |
224 |
244 |
225 |
245 |
226 |
246 |
227 (*** Meta theorems ***) |
247 (*** Meta theorems ***) |
228 |
248 |
482 else error "Illegal schematic variable(s) in term"; |
502 else error "Illegal schematic variable(s) in term"; |
483 |
503 |
484 fun cert_axm sg (name, raw_tm) = |
504 fun cert_axm sg (name, raw_tm) = |
485 let |
505 let |
486 val Cterm {t, T, ...} = cterm_of sg raw_tm |
506 val Cterm {t, T, ...} = cterm_of sg raw_tm |
487 handle TERM (msg, _) => error msg; |
507 handle TYPE arg => error (Sign.exn_type_msg sg arg) |
|
508 | TERM (msg, _) => error msg; |
488 in |
509 in |
489 assert (T = propT) "Term not of type prop"; |
510 assert (T = propT) "Term not of type prop"; |
490 (name, no_vars t) |
511 (name, no_vars t) |
491 end |
512 end |
492 handle ERROR => err_in_axm name; |
513 handle ERROR => err_in_axm name; |