1(* Title: Pure/theory.ML 2 Author: Lawrence C Paulson and Markus Wenzel 3 4Logical theory content: axioms, definitions, and begin/end wrappers. 5*) 6 7signature THEORY = 8sig 9 val parents_of: theory -> theory list 10 val ancestors_of: theory -> theory list 11 val nodes_of: theory -> theory list 12 val setup: (theory -> theory) -> unit 13 val local_setup: (Proof.context -> Proof.context) -> unit 14 val install_pure: theory -> unit 15 val get_pure: unit -> theory 16 val get_pure_bootstrap: unit -> theory 17 val get_markup: theory -> Markup.T 18 val check: {long: bool} -> Proof.context -> string * Position.T -> theory 19 val axiom_table: theory -> term Name_Space.table 20 val axiom_space: theory -> Name_Space.T 21 val all_axioms_of: theory -> (string * term) list 22 val defs_of: theory -> Defs.T 23 val at_begin: (theory -> theory option) -> theory -> theory 24 val at_end: (theory -> theory option) -> theory -> theory 25 val join_theory: theory list -> theory 26 val begin_theory: string * Position.T -> theory list -> theory 27 val end_theory: theory -> theory 28 val add_axiom: Proof.context -> binding * term -> theory -> theory 29 val const_dep: theory -> string * typ -> Defs.entry 30 val type_dep: string * typ list -> Defs.entry 31 val add_deps: Defs.context -> string -> Defs.entry -> Defs.entry list -> theory -> theory 32 val add_deps_global: string -> Defs.entry -> Defs.entry list -> theory -> theory 33 val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> theory 34 val specify_const: (binding * typ) * mixfix -> theory -> term * theory 35 val check_overloading: Proof.context -> bool -> string * typ -> unit 36end 37 38structure Theory: THEORY = 39struct 40 41 42(** theory context operations **) 43 44val parents_of = Context.parents_of; 45val ancestors_of = Context.ancestors_of; 46fun nodes_of thy = thy :: ancestors_of thy; 47 48fun setup f = Context.>> (Context.map_theory f); 49fun local_setup f = Context.>> (Context.map_proof f); 50 51 52(* implicit theory Pure *) 53 54val pure: theory Single_Assignment.var = Single_Assignment.var "pure"; 55 56fun install_pure thy = Single_Assignment.assign pure thy; 57 58fun get_pure () = 59 (case Single_Assignment.peek pure of 60 SOME thy => thy 61 | NONE => raise Fail "Theory Pure not present"); 62 63fun get_pure_bootstrap () = 64 (case Single_Assignment.peek pure of 65 SOME thy => thy 66 | NONE => Context.the_global_context ()); 67 68 69 70(** datatype thy **) 71 72type wrapper = (theory -> theory option) * stamp; 73 74fun apply_wrappers (wrappers: wrapper list) = 75 perhaps (perhaps_loop (perhaps_apply (map fst wrappers))); 76 77datatype thy = Thy of 78 {pos: Position.T, 79 id: serial, 80 axioms: term Name_Space.table, 81 defs: Defs.T, 82 wrappers: wrapper list * wrapper list}; 83 84fun make_thy (pos, id, axioms, defs, wrappers) = 85 Thy {pos = pos, id = id, axioms = axioms, defs = defs, wrappers = wrappers}; 86 87structure Thy = Theory_Data' 88( 89 type T = thy; 90 val empty = make_thy (Position.none, 0, Name_Space.empty_table "axiom", Defs.empty, ([], [])); 91 92 fun extend (Thy {pos = _, id = _, axioms, defs, wrappers}) = 93 make_thy (Position.none, 0, axioms, defs, wrappers); 94 95 fun merge old_thys (thy1, thy2) = 96 let 97 val Thy {pos = _, id = _, axioms = axioms1, defs = defs1, wrappers = (bgs1, ens1)} = thy1; 98 val Thy {pos = _, id = _, axioms = axioms2, defs = defs2, wrappers = (bgs2, ens2)} = thy2; 99 100 val axioms' = Name_Space.merge_tables (axioms1, axioms2); 101 val defs' = Defs.merge (Defs.global_context (fst old_thys)) (defs1, defs2); 102 val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2); 103 val ens' = Library.merge (eq_snd op =) (ens1, ens2); 104 in make_thy (Position.none, 0, axioms', defs', (bgs', ens')) end; 105); 106 107fun rep_theory thy = Thy.get thy |> (fn Thy args => args); 108 109fun map_thy f = Thy.map (fn (Thy {pos, id, axioms, defs, wrappers}) => 110 make_thy (f (pos, id, axioms, defs, wrappers))); 111 112fun map_axioms f = 113 map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, f axioms, defs, wrappers)); 114 115fun map_defs f = 116 map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, f defs, wrappers)); 117 118fun map_wrappers f = 119 map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, defs, f wrappers)); 120 121 122(* entity markup *) 123 124fun theory_markup def name id pos = 125 if id = 0 then Markup.empty 126 else 127 Markup.properties (Position.entity_properties_of def id pos) 128 (Markup.entity Markup.theoryN name); 129 130fun init_markup (name, pos) thy = 131 let 132 val id = serial (); 133 val _ = Position.report pos (theory_markup true name id pos); 134 in map_thy (fn (_, _, axioms, defs, wrappers) => (pos, id, axioms, defs, wrappers)) thy end; 135 136fun get_markup thy = 137 let val {pos, id, ...} = rep_theory thy 138 in theory_markup false (Context.theory_name thy) id pos end; 139 140fun check long ctxt (name, pos) = 141 let 142 val thy = Proof_Context.theory_of ctxt; 143 val thy' = 144 Context.get_theory long thy name 145 handle ERROR msg => 146 let 147 val completion_report = 148 Completion.make_report (name, pos) 149 (fn completed => 150 map (Context.theory_name' long) (ancestors_of thy) 151 |> filter (completed o Long_Name.base_name) 152 |> sort_strings 153 |> map (fn a => (a, (Markup.theoryN, a)))); 154 in error (msg ^ Position.here pos ^ completion_report) end; 155 val _ = Context_Position.report ctxt pos (get_markup thy'); 156 in thy' end; 157 158 159(* basic operations *) 160 161val axiom_table = #axioms o rep_theory; 162val axiom_space = Name_Space.space_of_table o axiom_table; 163 164val all_axioms_of = Name_Space.dest_table o axiom_table; 165 166val defs_of = #defs o rep_theory; 167 168 169(* join theory *) 170 171fun join_theory [] = raise List.Empty 172 | join_theory [thy] = thy 173 | join_theory thys = foldl1 Context.join_thys thys |> Sign.restore_naming (hd thys); 174 175 176(* begin/end theory *) 177 178val begin_wrappers = rev o #1 o #wrappers o rep_theory; 179val end_wrappers = rev o #2 o #wrappers o rep_theory; 180 181fun at_begin f = map_wrappers (apfst (cons (f, stamp ()))); 182fun at_end f = map_wrappers (apsnd (cons (f, stamp ()))); 183 184fun begin_theory (name, pos) imports = 185 if name = Context.PureN then 186 (case imports of 187 [thy] => init_markup (name, pos) thy 188 | _ => error "Bad bootstrapping of theory Pure") 189 else 190 let 191 val thy = Context.begin_thy name imports; 192 val wrappers = begin_wrappers thy; 193 in 194 thy 195 |> init_markup (name, pos) 196 |> Sign.local_path 197 |> Sign.theory_naming 198 |> apply_wrappers wrappers 199 |> tap (Syntax.force_syntax o Sign.syn_of) 200 end; 201 202fun end_theory thy = 203 thy 204 |> apply_wrappers (end_wrappers thy) 205 |> Sign.change_check 206 |> Context.finish_thy; 207 208 209 210(** primitive specifications **) 211 212(* raw axioms *) 213 214fun cert_axm ctxt (b, raw_tm) = 215 let 216 val thy = Proof_Context.theory_of ctxt; 217 val t = Sign.cert_prop thy raw_tm 218 handle TYPE (msg, _, _) => error msg 219 | TERM (msg, _) => error msg; 220 val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg; 221 222 val bad_sorts = 223 rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I | (T, _) => insert (op =) T) t []); 224 val _ = null bad_sorts orelse 225 error ("Illegal sort constraints in primitive specification: " ^ 226 commas (map (Syntax.string_of_typ (Config.put show_sorts true ctxt)) bad_sorts)); 227 in (b, Sign.no_vars ctxt t) end 228 handle ERROR msg => cat_error msg ("The error(s) above occurred in axiom " ^ Binding.print b); 229 230fun add_axiom ctxt raw_axm thy = thy |> map_axioms (fn axioms => 231 let 232 val axm = apsnd Logic.varify_global (cert_axm ctxt raw_axm); 233 val context = ctxt 234 |> Sign.inherit_naming thy 235 |> Context_Position.set_visible_generic false; 236 val (_, axioms') = Name_Space.define context true axm axioms; 237 in axioms' end); 238 239 240(* dependencies *) 241 242fun const_dep thy (c, T) = ((Defs.Const, c), Sign.const_typargs thy (c, T)); 243fun type_dep (c, args) = ((Defs.Type, c), args); 244 245fun dependencies (context as (ctxt, _)) unchecked def description lhs rhs = 246 let 247 fun prep (item, args) = 248 (case fold Term.add_tvarsT args [] of 249 [] => (item, map Logic.varifyT_global args) 250 | vs => raise TYPE ("Illegal schematic type variable(s)", map TVar vs, [])); 251 252 val lhs_vars = fold Term.add_tfreesT (snd lhs) []; 253 val rhs_extras = 254 fold (fn (_, args) => args |> (fold o Term.fold_atyps) (fn TFree v => 255 if member (op =) lhs_vars v then I else insert (op =) v)) rhs []; 256 val _ = 257 if null rhs_extras then () 258 else error ("Specification depends on extra type variables: " ^ 259 commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^ 260 "\nThe error(s) above occurred in " ^ quote description); 261 in Defs.define context unchecked def description (prep lhs) (map prep rhs) end; 262 263fun cert_entry thy ((Defs.Const, c), args) = 264 Sign.cert_term thy (Const (c, Sign.const_instance thy (c, args))) 265 |> dest_Const |> const_dep thy 266 | cert_entry thy ((Defs.Type, c), args) = 267 Sign.certify_typ thy (Type (c, args)) |> dest_Type |> type_dep; 268 269fun add_deps context a raw_lhs raw_rhs thy = 270 let 271 val (lhs as ((_, lhs_name), _)) :: rhs = map (cert_entry thy) (raw_lhs :: raw_rhs); 272 val description = if a = "" then lhs_name ^ " axiom" else a; 273 in thy |> map_defs (dependencies context false NONE description lhs rhs) end; 274 275fun add_deps_global a x y thy = 276 add_deps (Defs.global_context thy) a x y thy; 277 278fun specify_const decl thy = 279 let val (t, thy') = Sign.declare_const_global decl thy; 280 in (t, add_deps_global "" (const_dep thy' (dest_Const t)) [] thy') end; 281 282 283(* overloading *) 284 285fun check_overloading ctxt overloaded (c, T) = 286 let 287 val thy = Proof_Context.theory_of ctxt; 288 289 val declT = Sign.the_const_constraint thy c 290 handle TYPE (msg, _, _) => error msg; 291 val T' = Logic.varifyT_global T; 292 293 fun message sorts txt = 294 [Pretty.block [Pretty.str "Specification of constant ", 295 Pretty.str c, Pretty.str " ::", Pretty.brk 1, 296 Pretty.quote (Syntax.pretty_typ (Config.put show_sorts sorts ctxt) T)], 297 Pretty.str txt] |> Pretty.chunks |> Pretty.string_of; 298 in 299 if Sign.typ_instance thy (declT, T') then () 300 else if Type.raw_instance (declT, T') then 301 error (message true "imposes additional sort constraints on the constant declaration") 302 else if overloaded then () 303 else 304 error (message false "is strictly less general than the declared type (overloading required)") 305 end; 306 307 308(* definitional axioms *) 309 310local 311 312fun check_def (context as (ctxt, _)) thy unchecked overloaded (b, tm) defs = 313 let 314 val name = Sign.full_name thy b; 315 val ((lhs, rhs), _, _) = 316 Primitive_Defs.dest_def ctxt 317 {check_head = Term.is_Const, 318 check_free_lhs = K true, 319 check_free_rhs = K false, 320 check_tfree = K false} tm 321 handle TERM (msg, _) => error msg; 322 val lhs_const = Term.dest_Const (Term.head_of lhs); 323 324 val rhs_consts = 325 fold_aterms (fn Const const => insert (op =) (const_dep thy const) | _ => I) rhs []; 326 val rhs_types = 327 (fold_types o fold_subtypes) (fn Type t => insert (op =) (type_dep t) | _ => I) rhs []; 328 val rhs_deps = rhs_consts @ rhs_types; 329 330 val _ = check_overloading ctxt overloaded lhs_const; 331 in defs |> dependencies context unchecked (SOME name) name (const_dep thy lhs_const) rhs_deps end 332 handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block 333 [Pretty.str ("The error(s) above occurred in definition " ^ Binding.print b ^ ":"), 334 Pretty.fbrk, Pretty.quote (Syntax.pretty_term ctxt tm)])); 335 336in 337 338fun add_def (context as (ctxt, _)) unchecked overloaded raw_axm thy = 339 let val axm = cert_axm ctxt raw_axm in 340 thy 341 |> map_defs (check_def context thy unchecked overloaded axm) 342 |> add_axiom ctxt axm 343 end; 344 345end; 346 347end; 348