10 (*constants*) |
10 (*constants*) |
11 val check_const: theory -> term -> string |
11 val check_const: theory -> term -> string |
12 val read_bare_const: theory -> string -> string * typ |
12 val read_bare_const: theory -> string -> string * typ |
13 val read_const: theory -> string -> string |
13 val read_const: theory -> string -> string |
14 val string_of_const: theory -> string -> string |
14 val string_of_const: theory -> string -> string |
|
15 val cert_signature: theory -> typ -> typ |
|
16 val read_signature: theory -> string -> typ |
|
17 val const_typ: theory -> string -> typ |
|
18 val subst_signatures: theory -> term -> term |
15 val args_number: theory -> string -> int |
19 val args_number: theory -> string -> int |
16 |
20 |
17 (*constructor sets*) |
21 (*constructor sets*) |
18 val constrset_of_consts: theory -> (string * typ) list |
22 val constrset_of_consts: theory -> (string * typ) list |
19 -> string * ((string * sort) list * (string * typ list) list) |
23 -> string * ((string * sort) list * (string * typ list) list) |
29 val typscheme_eqn: theory -> thm -> (string * sort) list * typ |
33 val typscheme_eqn: theory -> thm -> (string * sort) list * typ |
30 val typscheme_eqns: theory -> string -> thm list -> (string * sort) list * typ |
34 val typscheme_eqns: theory -> string -> thm list -> (string * sort) list * typ |
31 val standard_typscheme: theory -> thm list -> thm list |
35 val standard_typscheme: theory -> thm list -> thm list |
32 |
36 |
33 (*executable code*) |
37 (*executable code*) |
|
38 val add_type: string -> theory -> theory |
|
39 val add_type_cmd: string -> theory -> theory |
|
40 val add_signature: string * typ -> theory -> theory |
|
41 val add_signature_cmd: string * string -> theory -> theory |
34 val add_datatype: (string * typ) list -> theory -> theory |
42 val add_datatype: (string * typ) list -> theory -> theory |
35 val add_datatype_cmd: string list -> theory -> theory |
43 val add_datatype_cmd: string list -> theory -> theory |
36 val type_interpretation: |
44 val type_interpretation: |
37 (string * ((string * sort) list * (string * typ list) list) |
45 (string * ((string * sort) list * (string * typ list) list) |
38 -> theory -> theory) -> theory -> theory |
46 -> theory -> theory) -> theory -> theory |
145 |
155 |
146 (* executable code data *) |
156 (* executable code data *) |
147 |
157 |
148 datatype spec = Spec of { |
158 datatype spec = Spec of { |
149 history_concluded: bool, |
159 history_concluded: bool, |
|
160 signatures: int Symtab.table * typ Symtab.table, |
150 eqns: ((bool * eqns) * (serial * eqns) list) Symtab.table |
161 eqns: ((bool * eqns) * (serial * eqns) list) Symtab.table |
151 (*with explicit history*), |
162 (*with explicit history*), |
152 dtyps: ((serial * ((string * sort) list * (string * typ list) list)) list) Symtab.table |
163 dtyps: ((serial * ((string * sort) list * (string * typ list) list)) list) Symtab.table |
153 (*with explicit history*), |
164 (*with explicit history*), |
154 cases: (int * (int * string list)) Symtab.table * unit Symtab.table |
165 cases: (int * (int * string list)) Symtab.table * unit Symtab.table |
155 }; |
166 }; |
156 |
167 |
157 fun make_spec (history_concluded, (eqns, (dtyps, cases))) = |
168 fun make_spec (history_concluded, ((signatures, eqns), (dtyps, cases))) = |
158 Spec { history_concluded = history_concluded, eqns = eqns, dtyps = dtyps, cases = cases }; |
169 Spec { history_concluded = history_concluded, |
159 fun map_spec f (Spec { history_concluded = history_concluded, eqns = eqns, |
170 signatures = signatures, eqns = eqns, dtyps = dtyps, cases = cases }; |
160 dtyps = dtyps, cases = cases }) = |
171 fun map_spec f (Spec { history_concluded = history_concluded, signatures = signatures, |
161 make_spec (f (history_concluded, (eqns, (dtyps, cases)))); |
172 eqns = eqns, dtyps = dtyps, cases = cases }) = |
162 fun merge_spec (Spec { history_concluded = _, eqns = eqns1, |
173 make_spec (f (history_concluded, ((signatures, eqns), (dtyps, cases)))); |
|
174 fun merge_spec (Spec { history_concluded = _, signatures = (tycos1, sigs1), eqns = eqns1, |
163 dtyps = dtyps1, cases = (cases1, undefs1) }, |
175 dtyps = dtyps1, cases = (cases1, undefs1) }, |
164 Spec { history_concluded = _, eqns = eqns2, |
176 Spec { history_concluded = _, signatures = (tycos2, sigs2), eqns = eqns2, |
165 dtyps = dtyps2, cases = (cases2, undefs2) }) = |
177 dtyps = dtyps2, cases = (cases2, undefs2) }) = |
166 let |
178 let |
|
179 val signatures = (Symtab.merge (op =) (tycos1, tycos2), |
|
180 Symtab.merge typ_equiv (sigs1, sigs2)); |
167 fun merge_eqns ((_, history1), (_, history2)) = |
181 fun merge_eqns ((_, history1), (_, history2)) = |
168 let |
182 let |
169 val raw_history = AList.merge (op = : serial * serial -> bool) |
183 val raw_history = AList.merge (op = : serial * serial -> bool) |
170 (K true) (history1, history2) |
184 (K true) (history1, history2) |
171 val filtered_history = filter_out (fst o snd) raw_history |
185 val filtered_history = filter_out (fst o snd) raw_history |
174 in ((false, (snd o hd) history), history) end; |
188 in ((false, (snd o hd) history), history) end; |
175 val eqns = Symtab.join (K merge_eqns) (eqns1, eqns2); |
189 val eqns = Symtab.join (K merge_eqns) (eqns1, eqns2); |
176 val dtyps = Symtab.join (K (AList.merge (op =) (K true))) (dtyps1, dtyps2); |
190 val dtyps = Symtab.join (K (AList.merge (op =) (K true))) (dtyps1, dtyps2); |
177 val cases = (Symtab.merge (K true) (cases1, cases2), |
191 val cases = (Symtab.merge (K true) (cases1, cases2), |
178 Symtab.merge (K true) (undefs1, undefs2)); |
192 Symtab.merge (K true) (undefs1, undefs2)); |
179 in make_spec (false, (eqns, (dtyps, cases))) end; |
193 in make_spec (false, ((signatures, eqns), (dtyps, cases))) end; |
180 |
194 |
181 fun history_concluded (Spec { history_concluded, ... }) = history_concluded; |
195 fun history_concluded (Spec { history_concluded, ... }) = history_concluded; |
|
196 fun the_signatures (Spec { signatures, ... }) = signatures; |
182 fun the_eqns (Spec { eqns, ... }) = eqns; |
197 fun the_eqns (Spec { eqns, ... }) = eqns; |
183 fun the_dtyps (Spec { dtyps, ... }) = dtyps; |
198 fun the_dtyps (Spec { dtyps, ... }) = dtyps; |
184 fun the_cases (Spec { cases, ... }) = cases; |
199 fun the_cases (Spec { cases, ... }) = cases; |
185 val map_history_concluded = map_spec o apfst; |
200 val map_history_concluded = map_spec o apfst; |
186 val map_eqns = map_spec o apsnd o apfst; |
201 val map_signatures = map_spec o apsnd o apfst o apfst; |
|
202 val map_eqns = map_spec o apsnd o apfst o apsnd; |
187 val map_dtyps = map_spec o apsnd o apsnd o apfst; |
203 val map_dtyps = map_spec o apsnd o apsnd o apfst; |
188 val map_cases = map_spec o apsnd o apsnd o apsnd; |
204 val map_cases = map_spec o apsnd o apsnd o apsnd; |
189 |
205 |
190 |
206 |
191 (* data slots dependent on executable code *) |
207 (* data slots dependent on executable code *) |
234 val empty_data = Datatab.empty : data; |
250 val empty_data = Datatab.empty : data; |
235 |
251 |
236 structure Code_Data = TheoryDataFun |
252 structure Code_Data = TheoryDataFun |
237 ( |
253 ( |
238 type T = spec * data Unsynchronized.ref; |
254 type T = spec * data Unsynchronized.ref; |
239 val empty = (make_spec (false, |
255 val empty = (make_spec (false, (((Symtab.empty, Symtab.empty), Symtab.empty), |
240 (Symtab.empty, (Symtab.empty, (Symtab.empty, Symtab.empty)))), Unsynchronized.ref empty_data); |
256 (Symtab.empty, (Symtab.empty, Symtab.empty)))), Unsynchronized.ref empty_data); |
241 fun copy (spec, data) = (spec, Unsynchronized.ref (! data)); |
257 fun copy (spec, data) = (spec, Unsynchronized.ref (! data)); |
242 val extend = copy; |
258 val extend = copy; |
243 fun merge pp ((spec1, data1), (spec2, data2)) = |
259 fun merge _ ((spec1, data1), (spec2, data2)) = |
244 (merge_spec (spec1, spec2), Unsynchronized.ref empty_data); |
260 (merge_spec (spec1, spec2), Unsynchronized.ref empty_data); |
245 ); |
261 ); |
246 |
262 |
247 fun thy_data f thy = f ((snd o Code_Data.get) thy); |
263 fun thy_data f thy = f ((snd o Code_Data.get) thy); |
248 |
264 |
332 |
348 |
333 (** foundation **) |
349 (** foundation **) |
334 |
350 |
335 (* constants *) |
351 (* constants *) |
336 |
352 |
337 fun args_number thy = length o fst o strip_type o Sign.the_const_type thy; |
353 fun arity_number thy tyco = case Symtab.lookup ((fst o the_signatures o the_exec) thy) tyco |
|
354 of SOME n => n |
|
355 | NONE => Sign.arity_number thy tyco; |
|
356 |
|
357 fun build_tsig thy = |
|
358 let |
|
359 val (tycos, _) = (the_signatures o the_exec) thy; |
|
360 val decls = (#types o Type.rep_tsig o Sign.tsig_of) thy |
|
361 |> apsnd (Symtab.fold (fn (tyco, n) => |
|
362 Symtab.update (tyco, Type.LogicalType n)) tycos); |
|
363 in Type.build_tsig ((Name_Space.empty "", Sorts.empty_algebra), [], decls) end; |
|
364 |
|
365 fun cert_signature thy = Logic.varifyT o Type.cert_typ (build_tsig thy) o Type.no_tvars; |
|
366 |
|
367 fun read_signature thy = cert_signature thy o Type.strip_sorts |
|
368 o Syntax.parse_typ (ProofContext.init thy); |
|
369 |
|
370 fun expand_signature thy = Type.cert_typ_mode Type.mode_syntax (Sign.tsig_of thy); |
|
371 |
|
372 fun lookup_typ thy = Symtab.lookup ((snd o the_signatures o the_exec) thy); |
|
373 |
|
374 fun const_typ thy c = case lookup_typ thy c |
|
375 of SOME ty => ty |
|
376 | NONE => (Type.strip_sorts o Sign.the_const_type thy) c; |
|
377 |
|
378 fun subst_signature thy c ty = |
|
379 let |
|
380 fun mk_subst (Type (tyco, tys1)) (ty2 as Type (tyco2, tys2)) = |
|
381 fold2 mk_subst tys1 tys2 |
|
382 | mk_subst ty (TVar (v, sort)) = Vartab.update (v, ([], ty)) |
|
383 in case lookup_typ thy c |
|
384 of SOME ty' => Envir.subst_type (mk_subst ty (expand_signature thy ty') Vartab.empty) ty' |
|
385 | NONE => ty |
|
386 end; |
|
387 |
|
388 fun subst_signatures thy = map_aterms (fn Const (c, ty) => Const (c, subst_signature thy c ty) | t => t); |
|
389 |
|
390 fun args_number thy = length o fst o strip_type o const_typ thy; |
338 |
391 |
339 |
392 |
340 (* datatypes *) |
393 (* datatypes *) |
341 |
394 |
342 fun constrset_of_consts thy cs = |
395 fun constrset_of_consts thy cs = |
353 val _ = if has_duplicates (eq_fst (op =)) vs |
406 val _ = if has_duplicates (eq_fst (op =)) vs |
354 then no_constr "duplicate type variables in datatype" c_ty else (); |
407 then no_constr "duplicate type variables in datatype" c_ty else (); |
355 val _ = if length tfrees <> length vs |
408 val _ = if length tfrees <> length vs |
356 then no_constr "type variables missing in datatype" c_ty else (); |
409 then no_constr "type variables missing in datatype" c_ty else (); |
357 in (tyco, vs) end; |
410 in (tyco, vs) end; |
358 fun ty_sorts (c, ty) = |
411 fun ty_sorts (c, raw_ty) = |
359 let |
412 let |
360 val ty_decl = (Logic.unvarifyT o Sign.the_const_type thy) c; |
413 val ty = subst_signature thy c raw_ty; |
|
414 val ty_decl = (Logic.unvarifyT o const_typ thy) c; |
361 val (tyco, _) = last_typ (c, ty) ty_decl; |
415 val (tyco, _) = last_typ (c, ty) ty_decl; |
362 val (_, vs) = last_typ (c, ty) ty; |
416 val (_, vs) = last_typ (c, ty) ty; |
363 in ((tyco, map snd vs), (c, (map fst vs, ty))) end; |
417 in ((tyco, map snd vs), (c, (map fst vs, ty))) end; |
364 fun add ((tyco', sorts'), c) ((tyco, sorts), cs) = |
418 fun add ((tyco', sorts'), c) ((tyco, sorts), cs) = |
365 let |
419 let |
380 in (tyco, (vs, rev cs''')) end; |
434 in (tyco, (vs, rev cs''')) end; |
381 |
435 |
382 fun get_datatype thy tyco = |
436 fun get_datatype thy tyco = |
383 case these (Symtab.lookup ((the_dtyps o the_exec) thy) tyco) |
437 case these (Symtab.lookup ((the_dtyps o the_exec) thy) tyco) |
384 of (_, spec) :: _ => spec |
438 of (_, spec) :: _ => spec |
385 | [] => Sign.arity_number thy tyco |
439 | [] => arity_number thy tyco |
386 |> Name.invents Name.context Name.aT |
440 |> Name.invents Name.context Name.aT |
387 |> map (rpair []) |
441 |> map (rpair []) |
388 |> rpair []; |
442 |> rpair []; |
389 |
443 |
390 fun get_datatype_of_constr thy c = |
444 fun get_datatype_of_constr thy c = |
391 case (snd o strip_type o Sign.the_const_type thy) c |
445 case (snd o strip_type o const_typ thy) c |
392 of Type (tyco, _) => if member (op =) ((map fst o snd o get_datatype thy) tyco) c |
446 of Type (tyco, _) => if member (op =) ((map fst o snd o get_datatype thy) tyco) c |
393 then SOME tyco else NONE |
447 then SOME tyco else NONE |
394 | _ => NONE; |
448 | _ => NONE; |
395 |
449 |
396 fun is_constr thy = is_some o get_datatype_of_constr thy; |
450 fun is_constr thy = is_some o get_datatype_of_constr thy; |
444 | check 0 (Var _) = () |
498 | check 0 (Var _) = () |
445 | check _ (Var _) = bad_thm |
499 | check _ (Var _) = bad_thm |
446 ("Variable with application on left hand side of equation\n" |
500 ("Variable with application on left hand side of equation\n" |
447 ^ Display.string_of_thm_global thy thm) |
501 ^ Display.string_of_thm_global thy thm) |
448 | check n (t1 $ t2) = (check (n+1) t1; check 0 t2) |
502 | check n (t1 $ t2) = (check (n+1) t1; check 0 t2) |
449 | check n (Const (c_ty as (c, ty))) = if n = (length o fst o strip_type) ty |
503 | check n (Const (c_ty as (_, ty))) = |
450 then if not proper orelse is_constr_pat (AxClass.unoverload_const thy c_ty) |
504 let |
451 then () |
505 val c' = AxClass.unoverload_const thy c_ty |
452 else bad_thm (quote c ^ " is not a constructor, on left hand side of equation\n" |
506 in if n = (length o fst o strip_type o subst_signature thy c') ty |
453 ^ Display.string_of_thm_global thy thm) |
507 then if not proper orelse is_constr_pat c' |
454 else bad_thm |
508 then () |
455 ("Partially applied constant " ^ quote c ^ " on left hand side of equation\n" |
509 else bad_thm (quote c ^ " is not a constructor, on left hand side of equation\n" |
456 ^ Display.string_of_thm_global thy thm); |
510 ^ Display.string_of_thm_global thy thm) |
|
511 else bad_thm |
|
512 ("Partially applied constant " ^ quote c ^ " on left hand side of equation\n" |
|
513 ^ Display.string_of_thm_global thy thm) |
|
514 end; |
457 val _ = map (check 0) args; |
515 val _ = map (check 0) args; |
458 val _ = if not proper orelse is_linear thm then () |
516 val _ = if not proper orelse is_linear thm then () |
459 else bad_thm ("Duplicate variables on left hand side of equation\n" |
517 else bad_thm ("Duplicate variables on left hand side of equation\n" |
460 ^ Display.string_of_thm_global thy thm); |
518 ^ Display.string_of_thm_global thy thm); |
461 val _ = if (is_none o AxClass.class_of_param thy) c |
519 val _ = if (is_none o AxClass.class_of_param thy) c |
462 then () |
520 then () |
463 else bad_thm ("Polymorphic constant as head in equation\n" |
521 else bad_thm ("Overloaded constant as head in equation\n" |
464 ^ Display.string_of_thm_global thy thm) |
522 ^ Display.string_of_thm_global thy thm) |
465 val _ = if not (is_constr thy c) |
523 val _ = if not (is_constr thy c) |
466 then () |
524 then () |
467 else bad_thm ("Constructor as head in equation\n" |
525 else bad_thm ("Constructor as head in equation\n" |
468 ^ Display.string_of_thm_global thy thm) |
526 ^ Display.string_of_thm_global thy thm) |
486 o warning_thm (gen_assert_eqn thy (K true)) o rpair false o meta_rewrite thy; |
544 o warning_thm (gen_assert_eqn thy (K true)) o rpair false o meta_rewrite thy; |
487 |
545 |
488 fun mk_eqn_liberal thy = Option.map (fn (thm, _) => (thm, is_linear thm)) |
546 fun mk_eqn_liberal thy = Option.map (fn (thm, _) => (thm, is_linear thm)) |
489 o try_thm (gen_assert_eqn thy (K true)) o rpair false o meta_rewrite thy; |
547 o try_thm (gen_assert_eqn thy (K true)) o rpair false o meta_rewrite thy; |
490 |
548 |
491 (*those following are permissive wrt. to overloaded constants!*) |
|
492 |
|
493 val head_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of; |
549 val head_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of; |
|
550 |
494 fun const_typ_eqn thy thm = |
551 fun const_typ_eqn thy thm = |
495 let |
552 let |
496 val (c, ty) = head_eqn thm; |
553 val (c, ty) = head_eqn thm; |
497 val c' = AxClass.unoverload_const thy (c, ty); |
554 val c' = AxClass.unoverload_const thy (c, ty); |
|
555 (*permissive wrt. to overloaded constants!*) |
498 in (c', ty) end; |
556 in (c', ty) end; |
|
557 |
499 fun const_eqn thy = fst o const_typ_eqn thy; |
558 fun const_eqn thy = fst o const_typ_eqn thy; |
500 |
559 |
501 fun typscheme thy (c, ty) = |
560 fun raw_typscheme thy (c, ty) = |
502 (map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty); |
561 (map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty); |
|
562 |
|
563 fun typscheme thy (c, ty) = raw_typscheme thy (c, subst_signature thy c ty); |
|
564 |
503 fun typscheme_eqn thy = typscheme thy o apsnd Logic.unvarifyT o const_typ_eqn thy; |
565 fun typscheme_eqn thy = typscheme thy o apsnd Logic.unvarifyT o const_typ_eqn thy; |
|
566 |
504 fun typscheme_eqns thy c [] = |
567 fun typscheme_eqns thy c [] = |
505 let |
568 let |
506 val raw_ty = Sign.the_const_type thy c; |
569 val raw_ty = const_typ thy c; |
507 val tvars = Term.add_tvar_namesT raw_ty []; |
570 val tvars = Term.add_tvar_namesT raw_ty []; |
508 val tvars' = case AxClass.class_of_param thy c |
571 val tvars' = case AxClass.class_of_param thy c |
509 of SOME class => [TFree (Name.aT, [class])] |
572 of SOME class => [TFree (Name.aT, [class])] |
510 | NONE => Name.invent_list [] Name.aT (length tvars) |
573 | NONE => Name.invent_list [] Name.aT (length tvars) |
511 |> map (fn v => TFree (v, [])); |
574 |> map (fn v => TFree (v, [])); |
512 val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty; |
575 val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty; |
513 in typscheme thy (c, ty) end |
576 in raw_typscheme thy (c, ty) end |
514 | typscheme_eqns thy c (thms as thm :: _) = typscheme_eqn thy thm; |
577 | typscheme_eqns thy c (thms as thm :: _) = typscheme_eqn thy thm; |
515 |
578 |
516 fun assert_eqns_const thy c eqns = |
579 fun assert_eqns_const thy c eqns = |
517 let |
580 let |
518 fun cert (eqn as (thm, _)) = if c = const_eqn thy thm |
581 fun cert (eqn as (thm, _)) = if c = const_eqn thy thm |
637 end; |
700 end; |
638 |
701 |
639 |
702 |
640 (** declaring executable ingredients **) |
703 (** declaring executable ingredients **) |
641 |
704 |
|
705 (* constant signatures *) |
|
706 |
|
707 fun add_type tyco thy = |
|
708 case Symtab.lookup ((snd o #types o Type.rep_tsig o Sign.tsig_of) thy) tyco |
|
709 of SOME (Type.Abbreviation (vs, _, _)) => |
|
710 (map_exec_purge NONE o map_signatures o apfst) |
|
711 (Symtab.update (tyco, length vs)) thy |
|
712 | _ => error ("No such type abbreviation: " ^ quote tyco); |
|
713 |
|
714 fun add_type_cmd s thy = add_type (Sign.intern_type thy s) thy; |
|
715 |
|
716 fun gen_add_signature prep_const prep_signature (raw_c, raw_ty) thy = |
|
717 let |
|
718 val c = prep_const thy raw_c; |
|
719 val ty = prep_signature thy raw_ty; |
|
720 val ty' = expand_signature thy ty; |
|
721 val ty'' = Sign.the_const_type thy c; |
|
722 val _ = if typ_equiv (ty', ty'') then () else |
|
723 error ("Illegal constant signature: " ^ Syntax.string_of_typ_global thy ty); |
|
724 in |
|
725 thy |
|
726 |> (map_exec_purge NONE o map_signatures o apsnd) (Symtab.update (c, ty)) |
|
727 end; |
|
728 |
|
729 val add_signature = gen_add_signature (K I) cert_signature; |
|
730 val add_signature_cmd = gen_add_signature read_const read_signature; |
|
731 |
|
732 |
642 (* datatypes *) |
733 (* datatypes *) |
643 |
734 |
644 structure Type_Interpretation = |
735 structure Type_Interpretation = |
645 Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool); |
736 Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool); |
646 |
737 |