2112

1 
structure Thry : Thry_sig (* LThry_sig *) =


2 
struct


3 


4 
structure USyntax = USyntax;


5 
type Type = USyntax.Type


6 
type Preterm = USyntax.Preterm


7 
type Term = USyntax.Term


8 
type Thm = Thm.thm


9 
type Thry = theory;


10 


11 
open Mask;


12 
structure S = USyntax;


13 


14 


15 
fun THRY_ERR{func,mesg} = Utils.ERR{module = "Thry",func=func,mesg=mesg};


16 


17 
(*


18 
* Matching


19 
**)


20 


21 
local open Utils


22 
infix 3 >


23 
fun tybind (x,y) = TVar (x,["term"]) > y


24 
fun tmbind (x,y) = Var (x,type_of y) > y


25 
in


26 
fun match_term thry pat ob =


27 
let val tsig = #tsig(Sign.rep_sg(sign_of thry))


28 
val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob)


29 
in (map tmbind tm_theta, map tybind ty_theta)


30 
end


31 


32 
fun match_type thry pat ob =


33 
map tybind(Type.typ_match (#tsig(Sign.rep_sg(sign_of thry))) ([],(pat,ob)))


34 
end;


35 


36 


37 
(*


38 
* Typing


39 
**)


40 


41 
fun typecheck thry = cterm_of (sign_of thry);


42 


43 


44 


45 
(*


46 
* Making a definition. The argument "tm" looks like "f = WFREC R M". This


47 
* entrypoint is specialized for interactive use, since it closes the theory


48 
* after making the definition. This allows later interactive definitions to


49 
* refer to previous ones. The name for the new theory is automatically


50 
* generated from the name of the argument theory.


51 
**)


52 
local val (imp $ tprop $ (eeq $ _ $ _ )) = #prop(rep_thm(eq_reflection))


53 
val Const(eeq_name, ty) = eeq


54 
val prop = #2 (S.strip_type ty)


55 
in


56 
fun make_definition parent s tm =


57 
let val {lhs,rhs} = S.dest_eq tm


58 
val {Name,Ty} = S.dest_var lhs


59 
val lhs1 = S.mk_const{Name = Name, Ty = Ty}


60 
val eeq1 = S.mk_const{Name = eeq_name, Ty = Ty > Ty > prop}


61 
val dtm = S.list_mk_comb(eeq1,[lhs1,rhs]) (* Rename "=" to "==" *)


62 
val thry1 = add_consts_i [(Name,Ty,NoSyn)] parent


63 
val thry2 = add_defs_i [(s,dtm)] thry1


64 
val parent_names = map ! (stamps_of_thy parent)


65 
val newthy_name = variant parent_names (hd parent_names)


66 
val new_thy = add_thyname newthy_name thry2


67 
in


68 
((get_axiom new_thy s) RS meta_eq_to_obj_eq, new_thy)


69 
end


70 
end;


71 


72 


73 
(*


74 
* Utility routine. Insert into list ordered by the key (a string). If two


75 
* keys are equal, the new element replaces the old. A more efficient option


76 
* for the future is needed. In fact, having the list of datatype facts be


77 
* ordered is useless, since the lookup should never fail!


78 
**)


79 
fun insert (el as (x:string, _)) =


80 
let fun canfind[] = [el]


81 
 canfind(alist as ((y as (k,_))::rst)) =


82 
if (x<k) then el::alist


83 
else if (x=k) then el::rst


84 
else y::canfind rst


85 
in canfind


86 
end;


87 


88 


89 
(*


90 
* A collection of facts about datatypes


91 
**)


92 
val nat_record = Dtype.build_record (Nat.thy, ("nat",["0","Suc"]), nat_ind_tac)


93 
val prod_record =


94 
let val prod_case_thms = Dtype.case_thms (sign_of Prod.thy) [split]


95 
(fn s => res_inst_tac [("p",s)] PairE_lemma)


96 
fun const s = Const(s, the(Sign.const_type (sign_of Prod.thy) s))


97 
in ("*",


98 
{constructors = [const "Pair"],


99 
case_const = const "split",


100 
case_rewrites = [split RS eq_reflection],


101 
case_cong = #case_cong prod_case_thms,


102 
nchotomy = #nchotomy prod_case_thms})


103 
end;


104 


105 
(*


106 
* Hacks to make interactive mode work. Referring to "datatypes" directly


107 
* is temporary, I hope!


108 
**)


109 
val match_info = fn thy =>


110 
fn "*" => Utils.SOME({case_const = #case_const (#2 prod_record),


111 
constructors = #constructors (#2 prod_record)})


112 
 "nat" => Utils.SOME({case_const = #case_const (#2 nat_record),


113 
constructors = #constructors (#2 nat_record)})


114 
 ty => case assoc(!datatypes,ty)


115 
of None => Utils.NONE


116 
 Some{case_const,constructors, ...} =>


117 
Utils.SOME{case_const=case_const, constructors=constructors}


118 


119 
val induct_info = fn thy =>


120 
fn "*" => Utils.SOME({nchotomy = #nchotomy (#2 prod_record),


121 
constructors = #constructors (#2 prod_record)})


122 
 "nat" => Utils.SOME({nchotomy = #nchotomy (#2 nat_record),


123 
constructors = #constructors (#2 nat_record)})


124 
 ty => case assoc(!datatypes,ty)


125 
of None => Utils.NONE


126 
 Some{nchotomy,constructors, ...} =>


127 
Utils.SOME{nchotomy=nchotomy, constructors=constructors}


128 


129 
val extract_info = fn thy =>


130 
let val case_congs = map (#case_cong o #2) (!datatypes)


131 
val case_rewrites = flat(map (#case_rewrites o #2) (!datatypes))


132 
in {case_congs = #case_cong (#2 prod_record)::


133 
#case_cong (#2 nat_record)::case_congs,


134 
case_rewrites = #case_rewrites(#2 prod_record)@


135 
#case_rewrites(#2 nat_record)@case_rewrites}


136 
end;


137 


138 


139 
end; (* Thry *)
