1526

1 
(* Title: Pure/theory.ML


2 
ID: $Id$


3 
Author: Lawrence C Paulson and Markus Wenzel


4 
Copyright 1996 University of Cambridge


5 


6 
Theories


7 
*)


8 


9 
signature THEORY =


10 
sig


11 
type theory


12 
exception THEORY of string * theory list


13 
val rep_theory : theory >


14 
{sign: Sign.sg, new_axioms: term Symtab.table, parents: theory list}


15 
val sign_of : theory > Sign.sg


16 
val syn_of : theory > Syntax.syntax


17 
val stamps_of_thy : theory > string ref list


18 
val parents_of : theory > theory list


19 
val subthy : theory * theory > bool


20 
val eq_thy : theory * theory > bool


21 
val proto_pure_thy : theory


22 
val pure_thy : theory


23 
val cpure_thy : theory


24 
(*theory primitives*)


25 
val add_classes : (class * class list) list > theory > theory


26 
val add_classrel : (class * class) list > theory > theory


27 
val add_defsort : sort > theory > theory


28 
val add_types : (string * int * mixfix) list > theory > theory


29 
val add_tyabbrs : (string * string list * string * mixfix) list


30 
> theory > theory


31 
val add_tyabbrs_i : (string * string list * typ * mixfix) list


32 
> theory > theory


33 
val add_arities : (string * sort list * sort) list > theory > theory


34 
val add_consts : (string * string * mixfix) list > theory > theory


35 
val add_consts_i : (string * typ * mixfix) list > theory > theory


36 
val add_syntax : (string * string * mixfix) list > theory > theory


37 
val add_syntax_i : (string * typ * mixfix) list > theory > theory


38 
val add_trfuns :


39 
(string * (Syntax.ast list > Syntax.ast)) list *


40 
(string * (term list > term)) list *


41 
(string * (term list > term)) list *


42 
(string * (Syntax.ast list > Syntax.ast)) list > theory > theory


43 
val add_trrules : (string * string)Syntax.trrule list > theory > theory


44 
val add_trrules_i : Syntax.ast Syntax.trrule list > theory > theory


45 
val cert_axm : Sign.sg > string * term > string * term


46 
val read_axm : Sign.sg > string * string > string * term


47 
val inferT_axm : Sign.sg > string * term > string * term


48 
val add_axioms : (string * string) list > theory > theory


49 
val add_axioms_i : (string * term) list > theory > theory


50 
val add_thyname : string > theory > theory


51 


52 
val merge_theories : theory * theory > theory


53 
val merge_thy_list : bool > theory list > theory


54 
end;


55 


56 


57 
structure Theory : THEORY =


58 
struct


59 
(*** Theories ***)


60 


61 
datatype theory =


62 
Theory of {


63 
sign: Sign.sg,


64 
new_axioms: term Symtab.table,


65 
parents: theory list};


66 


67 
fun rep_theory (Theory args) = args;


68 


69 
(*errors involving theories*)


70 
exception THEORY of string * theory list;


71 


72 


73 
val sign_of = #sign o rep_theory;


74 
val syn_of = #syn o Sign.rep_sg o sign_of;


75 


76 
(*stamps associated with a theory*)


77 
val stamps_of_thy = #stamps o Sign.rep_sg o sign_of;


78 


79 
(*return the immediate ancestors*)


80 
val parents_of = #parents o rep_theory;


81 


82 


83 
(*compare theories*)


84 
val subthy = Sign.subsig o pairself sign_of;


85 
val eq_thy = Sign.eq_sg o pairself sign_of;


86 


87 


88 
(* the Pure theories *)


89 


90 
val proto_pure_thy =


91 
Theory {sign = Sign.proto_pure, new_axioms = Symtab.null, parents = []};


92 


93 
val pure_thy =


94 
Theory {sign = Sign.pure, new_axioms = Symtab.null, parents = []};


95 


96 
val cpure_thy =


97 
Theory {sign = Sign.cpure, new_axioms = Symtab.null, parents = []};


98 


99 


100 


101 
(** extend theory **)


102 


103 
fun err_dup_axms names =


104 
error ("Duplicate axiom name(s) " ^ commas_quote names);


105 


106 
fun ext_thy (thy as Theory {sign, new_axioms, parents}) sign1 new_axms =


107 
let


108 
val draft = Sign.is_draft sign;


109 
val new_axioms1 =


110 
Symtab.extend_new (if draft then new_axioms else Symtab.null, new_axms)


111 
handle Symtab.DUPS names => err_dup_axms names;


112 
val parents1 = if draft then parents else [thy];


113 
in


114 
Theory {sign = sign1, new_axioms = new_axioms1, parents = parents1}


115 
end;


116 


117 


118 
(* extend signature of a theory *)


119 


120 
fun ext_sg extfun decls (thy as Theory {sign, ...}) =


121 
ext_thy thy (extfun decls sign) [];


122 


123 
val add_classes = ext_sg Sign.add_classes;


124 
val add_classrel = ext_sg Sign.add_classrel;


125 
val add_defsort = ext_sg Sign.add_defsort;


126 
val add_types = ext_sg Sign.add_types;


127 
val add_tyabbrs = ext_sg Sign.add_tyabbrs;


128 
val add_tyabbrs_i = ext_sg Sign.add_tyabbrs_i;


129 
val add_arities = ext_sg Sign.add_arities;


130 
val add_consts = ext_sg Sign.add_consts;


131 
val add_consts_i = ext_sg Sign.add_consts_i;


132 
val add_syntax = ext_sg Sign.add_syntax;


133 
val add_syntax_i = ext_sg Sign.add_syntax_i;


134 
val add_trfuns = ext_sg Sign.add_trfuns;


135 
val add_trrules = ext_sg Sign.add_trrules;


136 
val add_trrules_i = ext_sg Sign.add_trrules_i;


137 
val add_thyname = ext_sg Sign.add_name;


138 


139 


140 
(* prepare axioms *)


141 


142 
fun err_in_axm name =


143 
error ("The error(s) above occurred in axiom " ^ quote name);


144 


145 
fun no_vars tm =


146 
if null (term_vars tm) andalso null (term_tvars tm) then tm


147 
else error "Illegal schematic variable(s) in term";


148 


149 
fun cert_axm sg (name, raw_tm) =


150 
let


151 
val (t, T, _) = Sign.certify_term sg raw_tm


152 
handle TYPE arg => error (Sign.exn_type_msg sg arg)


153 
 TERM (msg, _) => error msg;


154 
in


155 
assert (T = propT) "Term not of type prop";


156 
(name, no_vars t)


157 
end


158 
handle ERROR => err_in_axm name;


159 


160 
(*Some duplication of code with read_def_cterm*)


161 
fun read_axm sg (name, str) =


162 
let val ts = Syntax.read (#syn (Sign.rep_sg sg)) propT str;


163 
val (_, t, _) =


164 
Sign.infer_types sg (K None) (K None) [] true (ts,propT);


165 
in cert_axm sg (name,t) end;


166 


167 
fun inferT_axm sg (name, pre_tm) =


168 
let val t = #2(Sign.infer_types sg (K None) (K None) [] true


169 
([pre_tm], propT))


170 
in (name, no_vars t) end


171 
handle ERROR => err_in_axm name;


172 


173 


174 
(* extend axioms of a theory *)


175 


176 
fun ext_axms prep_axm axms (thy as Theory {sign, ...}) =


177 
let


178 
val sign1 = Sign.make_draft sign;


179 
val axioms = map (apsnd (Term.compress_term o Logic.varify) o


180 
prep_axm sign)


181 
axms;


182 
in


183 
ext_thy thy sign1 axioms


184 
end;


185 


186 
val add_axioms = ext_axms read_axm;


187 
val add_axioms_i = ext_axms cert_axm;


188 


189 


190 


191 
(** merge theories **)


192 


193 
fun merge_thy_list mk_draft thys =


194 
let


195 
fun is_union thy = forall (fn t => subthy (t, thy)) thys;


196 
val is_draft = Sign.is_draft o sign_of;


197 


198 
fun add_sign (sg, Theory {sign, ...}) =


199 
Sign.merge (sg, sign) handle TERM (msg, _) => error msg;


200 
in


201 
(case (find_first is_union thys, exists is_draft thys) of


202 
(Some thy, _) => thy


203 
 (None, true) => raise THEORY ("Illegal merge of draft theories", thys)


204 
 (None, false) => Theory {


205 
sign =


206 
(if mk_draft then Sign.make_draft else I)


207 
(foldl add_sign (Sign.proto_pure, thys)),


208 
new_axioms = Symtab.null,


209 
parents = thys})


210 
end;


211 


212 
fun merge_theories (thy1, thy2) = merge_thy_list false [thy1, thy2];


213 


214 


215 
end;


216 


217 
open Theory;
