diff --git a/src/Pure/Isar/expression.ML b/src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML +++ b/src/Pure/Isar/expression.ML @@ -1,881 +1,879 @@ (* Title: Pure/Isar/expression.ML Author: Clemens Ballarin, TU Muenchen Locale expressions and user interface layer of locales. *) signature EXPRESSION = sig (* Locale expressions *) datatype 'term map = Positional of 'term option list | Named of (string * 'term) list type 'term rewrites = (Attrib.binding * 'term) list type ('name, 'term) expr = ('name * ((string * bool) * ('term map * 'term rewrites))) list type expression_i = (string, term) expr * (binding * typ option * mixfix) list type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list (* Processing of context statements *) val cert_statement: Element.context_i list -> Element.statement_i -> Proof.context -> (Attrib.binding * (term * term list) list) list * Proof.context val read_statement: Element.context list -> Element.statement -> Proof.context -> (Attrib.binding * (term * term list) list) list * Proof.context (* Declaring locales *) val cert_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context_i list -> Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context) val cert_read_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context list -> Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context) (*FIXME*) val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list -> Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context) val add_locale: binding -> binding -> Bundle.name list -> expression_i -> Element.context_i list -> theory -> string * local_theory val add_locale_cmd: binding -> binding -> (xstring * Position.T) list -> expression -> Element.context list -> theory -> string * local_theory (* Processing of locale expressions *) val cert_goal_expression: expression_i -> Proof.context -> (term list list * term list list * (string * morphism) list * (Attrib.binding * term) list list * morphism) * Proof.context val read_goal_expression: expression -> Proof.context -> (term list list * term list list * (string * morphism) list * (Attrib.binding * term) list list * morphism) * Proof.context end; structure Expression : EXPRESSION = struct datatype ctxt = datatype Element.ctxt; (*** Expressions ***) datatype 'term map = Positional of 'term option list | Named of (string * 'term) list; type 'term rewrites = (Attrib.binding * 'term) list; type ('name, 'term) expr = ('name * ((string * bool) * ('term map * 'term rewrites))) list; type expression_i = (string, term) expr * (binding * typ option * mixfix) list; type expression = (xstring * Position.T, string) expr * (binding * string option * mixfix) list; (** Internalise locale names in expr **) fun check_expr thy instances = map (apfst (Locale.check thy)) instances; (** Parameters of expression **) (*Sanity check of instantiations and extraction of implicit parameters. The latter only occurs iff strict = false. Positional instantiations are extended to match full length of parameter list of instantiated locale.*) fun parameters_of thy strict (expr, fixed) = let val ctxt = Proof_Context.init_global thy; fun reject_dups message xs = (case duplicates (op =) xs of [] => () | dups => error (message ^ commas dups)); fun parm_eq ((p1, mx1), (p2, mx2)) = p1 = p2 andalso (Mixfix.equal (mx1, mx2) orelse error ("Conflicting syntax for parameter " ^ quote p1 ^ " in expression" ^ Position.here_list [Mixfix.pos_of mx1, Mixfix.pos_of mx2])); fun params_loc loc = Locale.params_of thy loc |> map (apfst #1); fun params_inst (loc, (prfx, (Positional insts, eqns))) = let val ps = params_loc loc; val d = length ps - length insts; val insts' = if d < 0 then error ("More arguments than parameters in instantiation of locale " ^ quote (Locale.markup_name ctxt loc)) else insts @ replicate d NONE; val ps' = (ps ~~ insts') |> map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE); in (ps', (loc, (prfx, (Positional insts', eqns)))) end | params_inst (loc, (prfx, (Named insts, eqns))) = let val _ = reject_dups "Duplicate instantiation of the following parameter(s): " (map fst insts); val ps' = (insts, params_loc loc) |-> fold (fn (p, _) => fn ps => if AList.defined (op =) ps p then AList.delete (op =) p ps else error (quote p ^ " not a parameter of instantiated expression")); in (ps', (loc, (prfx, (Named insts, eqns)))) end; fun params_expr is = let val (is', ps') = fold_map (fn i => fn ps => let val (ps', i') = params_inst i; val ps'' = distinct parm_eq (ps @ ps'); in (i', ps'') end) is [] in (ps', is') end; val (implicit, expr') = params_expr expr; val implicit' = map #1 implicit; val fixed' = map (Variable.check_name o #1) fixed; val _ = reject_dups "Duplicate fixed parameter(s): " fixed'; val implicit'' = if strict then [] else let val _ = reject_dups "Parameter(s) declared simultaneously in expression and for clause: " (implicit' @ fixed'); in map (fn (x, mx) => (Binding.name x, NONE, mx)) implicit end; in (expr', implicit'' @ fixed) end; (** Read instantiation **) (* Parse positional or named instantiation *) local fun prep_inst prep_term ctxt parms (Positional insts) = (insts ~~ parms) |> map (fn (NONE, p) => Free (p, dummyT) | (SOME t, _) => prep_term ctxt t) | prep_inst prep_term ctxt parms (Named insts) = parms |> map (fn p => (case AList.lookup (op =) insts p of SOME t => prep_term ctxt t | NONE => Free (p, dummyT))); in fun parse_inst x = prep_inst Syntax.parse_term x; fun make_inst x = prep_inst (K I) x; end; (* Instantiation morphism *) fun inst_morphism params ((prfx, mandatory), insts') ctxt = let (* parameters *) val parm_types = map #2 params; val type_parms = fold Term.add_tfreesT parm_types []; (* type inference *) val parm_types' = map (Type_Infer.paramify_vars o Logic.varifyT_global) parm_types; val type_parms' = fold Term.add_tvarsT parm_types' []; val checked = (map (Logic.mk_type o TVar) type_parms' @ map2 Type.constraint parm_types' insts') |> Syntax.check_terms (Config.put Type_Infer.object_logic false ctxt) val (type_parms'', insts'') = chop (length type_parms') checked; (* context *) val ctxt' = fold Proof_Context.augment checked ctxt; val certT = Thm.trim_context_ctyp o Thm.ctyp_of ctxt'; val cert = Thm.trim_context_cterm o Thm.cterm_of ctxt'; (* instantiation *) val instT = (type_parms ~~ map Logic.dest_type type_parms'') |> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (v, T)); val cert_inst = ((map #1 params ~~ map (Term_Subst.instantiateT_frees (TFrees.make instT)) parm_types) ~~ insts'') |> map_filter (fn (v, t) => if Free v = t then NONE else SOME (v, cert t)); in (Element.instantiate_normalize_morphism (map (apsnd certT) instT, cert_inst) $> Morphism.binding_morphism "Expression.inst" (Binding.prefix mandatory prfx), ctxt') end; (*** Locale processing ***) (** Parsing **) fun parse_elem prep_typ prep_term ctxt = Element.map_ctxt {binding = I, typ = prep_typ ctxt, term = prep_term (Proof_Context.set_mode Proof_Context.mode_schematic ctxt), pattern = prep_term (Proof_Context.set_mode Proof_Context.mode_pattern ctxt), fact = I, attrib = I}; fun prepare_stmt prep_prop prep_obtains ctxt stmt = (case stmt of Element.Shows raw_shows => raw_shows |> (map o apsnd o map) (fn (t, ps) => (prep_prop (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) t, map (prep_prop (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)) ps)) | Element.Obtains raw_obtains => let val ((_, thesis), thesis_ctxt) = Obtain.obtain_thesis ctxt; val obtains = prep_obtains thesis_ctxt thesis raw_obtains; in map (fn (b, t) => ((b, []), [(t, [])])) obtains end); (** Simultaneous type inference: instantiations + elements + statement **) local fun mk_type T = (Logic.mk_type T, []); fun mk_term t = (t, []); fun mk_propp (p, pats) = (Type.constraint propT p, pats); fun dest_type (T, []) = Logic.dest_type T; fun dest_term (t, []) = t; fun dest_propp (p, pats) = (p, pats); fun extract_inst (_, (_, ts)) = map mk_term ts; fun restore_inst ((l, (p, _)), cs) = (l, (p, map dest_term cs)); fun extract_eqns es = map (mk_term o snd) es; fun restore_eqns (es, cs) = map2 (fn (b, _) => fn c => (b, dest_term c)) es cs; fun extract_elem (Fixes fixes) = map (#2 #> the_list #> map mk_type) fixes | extract_elem (Constrains csts) = map (#2 #> single #> map mk_type) csts | extract_elem (Assumes asms) = map (#2 #> map mk_propp) asms | extract_elem (Defines defs) = map (fn (_, (t, ps)) => [mk_propp (t, ps)]) defs | extract_elem (Notes _) = [] | extract_elem (Lazy_Notes _) = []; fun restore_elem (Fixes fixes, css) = (fixes ~~ css) |> map (fn ((x, _, mx), cs) => (x, cs |> map dest_type |> try hd, mx)) |> Fixes | restore_elem (Constrains csts, css) = (csts ~~ css) |> map (fn ((x, _), cs) => (x, cs |> map dest_type |> hd)) |> Constrains | restore_elem (Assumes asms, css) = (asms ~~ css) |> map (fn ((b, _), cs) => (b, map dest_propp cs)) |> Assumes | restore_elem (Defines defs, css) = (defs ~~ css) |> map (fn ((b, _), [c]) => (b, dest_propp c)) |> Defines | restore_elem (elem as Notes _, _) = elem | restore_elem (elem as Lazy_Notes _, _) = elem; fun prep (_, pats) (ctxt, t :: ts) = let val ctxt' = Proof_Context.augment t ctxt in ((t, Syntax.check_props (Proof_Context.set_mode Proof_Context.mode_pattern ctxt') pats), (ctxt', ts)) end; fun check cs ctxt = let val (cs', (ctxt', _)) = fold_map prep cs (ctxt, Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) (map fst cs)); in (cs', ctxt') end; in fun check_autofix insts eqnss elems concl ctxt = let val inst_cs = map extract_inst insts; val eqns_cs = map extract_eqns eqnss; val elem_css = map extract_elem elems; val concl_cs = (map o map) mk_propp (map snd concl); (* Type inference *) val (inst_cs' :: eqns_cs' :: css', ctxt') = (fold_burrow o fold_burrow) check (inst_cs :: eqns_cs :: elem_css @ [concl_cs]) ctxt; val (elem_css', [concl_cs']) = chop (length elem_css) css'; in ((map restore_inst (insts ~~ inst_cs'), map restore_eqns (eqnss ~~ eqns_cs'), map restore_elem (elems ~~ elem_css'), map fst concl ~~ concl_cs'), ctxt') end; end; (** Prepare locale elements **) fun declare_elem prep_var (Fixes fixes) ctxt = let val (vars, _) = fold_map prep_var fixes ctxt in ctxt |> Proof_Context.add_fixes vars |> snd end | declare_elem prep_var (Constrains csts) ctxt = ctxt |> fold_map (fn (x, T) => prep_var (Binding.name x, SOME T, NoSyn)) csts |> snd | declare_elem _ (Assumes _) ctxt = ctxt | declare_elem _ (Defines _) ctxt = ctxt | declare_elem _ (Notes _) ctxt = ctxt | declare_elem _ (Lazy_Notes _) ctxt = ctxt; (** Finish locale elements **) fun finish_inst ctxt (loc, (prfx, inst)) = let val thy = Proof_Context.theory_of ctxt; val (morph, _) = inst_morphism (map #1 (Locale.params_of thy loc)) (prfx, inst) ctxt; in (loc, morph) end; fun finish_fixes (parms: (string * typ) list) = map (fn (binding, _, mx) => let val x = Binding.name_of binding in (binding, AList.lookup (op =) parms x, mx) end); local fun closeup _ _ false elem = elem | closeup (outer_ctxt, ctxt) parms true elem = let (* FIXME consider closing in syntactic phase -- before type checking *) fun close_frees t = let val rev_frees = Term.fold_aterms (fn Free (x, T) => if Variable.is_fixed outer_ctxt x orelse AList.defined (op =) parms x then I else insert (op =) (x, T) | _ => I) t []; in fold (Logic.all o Free) rev_frees t end; fun no_binds [] = [] | no_binds _ = error "Illegal term bindings in context element"; in (case elem of Assumes asms => Assumes (asms |> map (fn (a, propps) => (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps))) | Defines defs => Defines (defs |> map (fn ((name, atts), (t, ps)) => let val ((c, _), t') = Local_Defs.cert_def ctxt (K []) (close_frees t) in ((Thm.def_binding_optional (Binding.name c) name, atts), (t', no_binds ps)) end)) | e => e) end; in fun finish_elem _ parms _ (Fixes fixes) = Fixes (finish_fixes parms fixes) | finish_elem _ _ _ (Constrains _) = Constrains [] | finish_elem ctxts parms do_close (Assumes asms) = closeup ctxts parms do_close (Assumes asms) | finish_elem ctxts parms do_close (Defines defs) = closeup ctxts parms do_close (Defines defs) | finish_elem _ _ _ (elem as Notes _) = elem | finish_elem _ _ _ (elem as Lazy_Notes _) = elem; end; (** Process full context statement: instantiations + elements + statement **) (* Interleave incremental parsing and type inference over entire parsed stretch. *) local fun abs_def ctxt = Thm.cterm_of ctxt #> Assumption.assume ctxt #> Local_Defs.abs_def_rule ctxt #> Thm.prop_of; fun prep_full_context_statement parse_typ parse_prop prep_obtains prep_var_elem prep_inst prep_eqns prep_attr prep_var_inst prep_expr {strict, do_close, fixed_frees} raw_import init_body raw_elems raw_stmt ctxt1 = let val thy = Proof_Context.theory_of ctxt1; val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import); fun prep_insts_cumulative (loc, (prfx, (inst, eqns))) (i, insts, eqnss, ctxt) = let val params = map #1 (Locale.params_of thy loc); val inst' = prep_inst ctxt (map #1 params) inst; val parm_types' = params |> map (#2 #> Logic.varifyT_global #> Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) #> Type_Infer.paramify_vars); val inst'' = map2 Type.constraint parm_types' inst'; val insts' = insts @ [(loc, (prfx, inst''))]; val ((insts'', _, _, _), ctxt2) = check_autofix insts' [] [] [] ctxt; val inst''' = insts'' |> List.last |> snd |> snd; val (inst_morph, _) = inst_morphism params (prfx, inst''') ctxt; val ctxt' = Locale.activate_declarations (loc, inst_morph) ctxt2 handle ERROR msg => if null eqns then error msg else (Locale.tracing ctxt1 (msg ^ "\nFalling back to reading rewrites clause before activation."); ctxt2); val attrss = map (apsnd (map (prep_attr ctxt)) o fst) eqns; val eqns' = (prep_eqns ctxt' o map snd) eqns; val eqnss' = [attrss ~~ eqns']; val ((_, [eqns''], _, _), _) = check_autofix insts'' eqnss' [] [] ctxt'; val rewrite_morph = eqns' |> map (abs_def ctxt') |> Variable.export_terms ctxt' ctxt |> Element.eq_term_morphism (Proof_Context.theory_of ctxt) |> the_default Morphism.identity; val ctxt'' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt; val eqnss' = eqnss @ [attrss ~~ Variable.export_terms ctxt' ctxt eqns']; in (i + 1, insts', eqnss', ctxt'') end; fun prep_elem raw_elem ctxt = let val ctxt' = ctxt |> Context_Position.set_visible false |> declare_elem prep_var_elem raw_elem |> Context_Position.restore_visible ctxt; val elems' = parse_elem parse_typ parse_prop ctxt' raw_elem; in (elems', ctxt') end; val fors = fold_map prep_var_inst fixed ctxt1 |> fst; val ctxt2 = ctxt1 |> Proof_Context.add_fixes fors |> snd; val (_, insts', eqnss', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], [], ctxt2); fun prep_stmt elems ctxt = check_autofix insts' [] elems (prepare_stmt parse_prop prep_obtains ctxt raw_stmt) ctxt; val _ = if fixed_frees then () else (case fold (fold (Variable.add_frees ctxt3) o snd o snd) insts' [] of [] => () | frees => error ("Illegal free variables in expression: " ^ commas_quote (map (Syntax.string_of_term ctxt3 o Free) (rev frees)))); val ((insts, _, elems', concl), ctxt4) = ctxt3 |> init_body |> fold_map prep_elem raw_elems |-> prep_stmt; (* parameters from expression and elements *) val xs = maps (fn Fixes fixes => map (Variable.check_name o #1) fixes | _ => []) (Fixes fors :: elems'); val (parms, ctxt5) = fold_map Proof_Context.inferred_param xs ctxt4; val fors' = finish_fixes parms fors; val fixed = map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fors'; val deps = map (finish_inst ctxt5) insts; val elems'' = map (finish_elem (ctxt1, ctxt5) parms do_close) elems'; in ((fixed, deps, eqnss', elems'', concl), (parms, ctxt5)) end; in fun cert_full_context_statement x = prep_full_context_statement (K I) (K I) Obtain.cert_obtains Proof_Context.cert_var make_inst Syntax.check_props (K I) Proof_Context.cert_var (K I) x; fun cert_read_full_context_statement x = prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains Proof_Context.read_var make_inst Syntax.check_props (K I) Proof_Context.cert_var (K I) x; fun read_full_context_statement x = prep_full_context_statement Syntax.parse_typ Syntax.parse_prop Obtain.parse_obtains Proof_Context.read_var parse_inst Syntax.read_props Attrib.check_src Proof_Context.read_var check_expr x; end; (* Context statement: elements + statement *) local fun prep_statement prep activate raw_elems raw_stmt ctxt = let val ((_, _, _, elems, concl), _) = prep {strict = true, do_close = false, fixed_frees = true} ([], []) I raw_elems raw_stmt ctxt; val ctxt' = ctxt |> Proof_Context.set_stmt true |> fold_map activate elems |> #2 |> Proof_Context.restore_stmt ctxt; in (concl, ctxt') end; in fun cert_statement x = prep_statement cert_full_context_statement Element.activate_i x; fun read_statement x = prep_statement read_full_context_statement Element.activate x; end; (* Locale declaration: import + elements *) fun fix_params params = Proof_Context.add_fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params) #> snd; local fun prep_declaration prep activate raw_import init_body raw_elems ctxt = let val ((fixed, deps, eqnss, elems, _), (parms, ctxt0)) = prep {strict = false, do_close = true, fixed_frees = false} raw_import init_body raw_elems (Element.Shows []) ctxt; val _ = null (flat eqnss) orelse error "Illegal rewrites clause(s) in declaration of locale"; (* Declare parameters and imported facts *) val ctxt' = ctxt |> fix_params fixed |> fold (Context.proof_map o Locale.activate_facts NONE) deps; val (elems', ctxt'') = ctxt' |> Proof_Context.set_stmt true |> fold_map activate elems ||> Proof_Context.restore_stmt ctxt'; in ((fixed, deps, elems', ctxt''), (parms, ctxt0)) end; in fun cert_declaration x = prep_declaration cert_full_context_statement Element.activate_i x; fun cert_read_declaration x = prep_declaration cert_read_full_context_statement Element.activate x; fun read_declaration x = prep_declaration read_full_context_statement Element.activate x; end; (* Locale expression to set up a goal *) local fun props_of thy (name, morph) = let val (asm, defs) = Locale.specification_of thy name in map (Morphism.term morph) (the_list asm @ defs) end; fun prep_goal_expression prep expression ctxt = let val thy = Proof_Context.theory_of ctxt; val ((fixed, deps, eqnss, _, _), _) = prep {strict = true, do_close = true, fixed_frees = true} expression I [] (Element.Shows []) ctxt; (* proof obligations *) val propss = map (props_of thy) deps; val eq_propss = (map o map) snd eqnss; val goal_ctxt = ctxt |> fix_params fixed |> (fold o fold) Proof_Context.augment (propss @ eq_propss); val export = Proof_Context.export_morphism goal_ctxt ctxt; val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export; val exp_term = Term_Subst.zero_var_indexes o Morphism.term export; val exp_typ = Logic.type_map exp_term; val export' = Morphism.morphism "Expression.prep_goal" {binding = [], typ = [exp_typ], term = [exp_term], fact = [exp_fact]}; in ((propss, eq_propss, deps, eqnss, export'), goal_ctxt) end; in fun cert_goal_expression x = prep_goal_expression cert_full_context_statement x; fun read_goal_expression x = prep_goal_expression read_full_context_statement x; end; (*** Locale declarations ***) (* extract specification text *) val norm_term = Envir.beta_norm oo Term.subst_atomic; fun bind_def ctxt eq (env, eqs) = let val _ = Local_Defs.cert_def ctxt (K []) eq; val ((y, T), b) = Local_Defs.abs_def eq; val b' = norm_term env b; fun err msg = error (msg ^ ": " ^ quote y); in (case filter (fn (Free (y', _), _) => y = y' | _ => false) env of [] => ((Free (y, T), b') :: env, eq :: eqs) | dups => if forall (fn (_, b'') => b' aconv b'') dups then (env, eqs) else err "Attempt to redefine variable") end; (* text has the following structure: (((exts, exts'), (ints, ints')), (xs, env, defs)) where exts: external assumptions (terms in assumes elements) exts': dito, normalised wrt. env ints: internal assumptions (terms in assumptions from insts) ints': dito, normalised wrt. env xs: the free variables in exts' and ints' and rhss of definitions, this includes parameters except defined parameters env: list of term pairs encoding substitutions, where the first term is a free variable; substitutions represent defines elements and the rhs is normalised wrt. the previous env defs: the equations from the defines elements *) fun eval_text _ _ (Fixes _) text = text | eval_text _ _ (Constrains _) text = text | eval_text _ is_ext (Assumes asms) (((exts, exts'), (ints, ints')), (env, defs)) = let val ts = maps (map #1 o #2) asms; val ts' = map (norm_term env) ts; val spec' = if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints')) else ((exts, exts'), (ints @ ts, ints' @ ts')); in (spec', (env, defs)) end | eval_text ctxt _ (Defines defs) (spec, binds) = (spec, fold (bind_def ctxt o #1 o #2) defs binds) | eval_text _ _ (Notes _) text = text | eval_text _ _ (Lazy_Notes _) text = text; fun eval_inst ctxt (loc, morph) text = let val thy = Proof_Context.theory_of ctxt; val (asm, defs) = Locale.specification_of thy loc; val asm' = Option.map (Morphism.term morph) asm; val defs' = map (Morphism.term morph) defs; val text' = text |> (if is_some asm then eval_text ctxt false (Assumes [(Binding.empty_atts, [(the asm', [])])]) else I) |> (if not (null defs) then eval_text ctxt false (Defines (map (fn def => (Binding.empty_atts, (def, []))) defs')) else I) (* FIXME clone from locale.ML *) in text' end; fun eval_elem ctxt elem text = eval_text ctxt true elem text; fun eval ctxt deps elems = let val text' = fold (eval_inst ctxt) deps ((([], []), ([], [])), ([], [])); val ((spec, (_, defs))) = fold (eval_elem ctxt) elems text'; in (spec, defs) end; (* axiomsN: name of theorem set with destruct rules for locale predicates, also name suffix of delta predicates and assumptions. *) val axiomsN = "axioms"; local (* introN: name of theorems for introduction rules of locale and delta predicates *) val introN = "intro"; fun atomize_spec ctxt ts = let val t = Logic.mk_conjunction_balanced ts; val body = Object_Logic.atomize_term ctxt t; val bodyT = Term.fastype_of body; in if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of ctxt t)) else (body, bodyT, Object_Logic.atomize ctxt (Thm.cterm_of ctxt t)) end; (* achieve plain syntax for locale predicates (without "PROP") *) fun aprop_tr' n c = let val c' = Lexicon.mark_const c; fun tr' (_: Proof.context) T args = if T <> dummyT andalso length args = n then Syntax.const "_aprop" $ Term.list_comb (Syntax.const c', args) else raise Match; in (c', tr') end; (* define one predicate including its intro rule and axioms - binding: predicate name - parms: locale parameters - defs: thms representing substitutions from defines elements - ts: terms representing locale assumptions (not normalised wrt. defs) - norm_ts: terms representing locale assumptions (normalised wrt. defs) - thy: the theory *) fun def_pred binding parms defs ts norm_ts thy = let val name = Sign.full_name thy binding; val thy_ctxt = Proof_Context.init_global thy; val (body, bodyT, body_eq) = atomize_spec thy_ctxt norm_ts; val env = Names.build (Names.add_free_names body); val xs = filter (Names.defined env o #1) parms; val Ts = map #2 xs; val type_tfrees = TFrees.build (fold TFrees.add_tfreesT Ts); val extra_tfrees = - TFrees.build (body |> (Term.fold_types o Term.fold_atyps) - (fn TFree v => not (TFrees.defined type_tfrees v) ? TFrees.add_set v | _ => I)) + TFrees.build (TFrees.add_tfrees_unless (TFrees.defined type_tfrees) body) |> TFrees.list_set |> sort_by #1 |> map TFree; val predT = map Term.itselfT extra_tfrees ---> Ts ---> bodyT; val args = map Logic.mk_type extra_tfrees @ map Free xs; val head = Term.list_comb (Const (name, predT), args); val statement = Object_Logic.ensure_propT thy_ctxt head; val ([pred_def], defs_thy) = thy |> bodyT = propT ? Sign.typed_print_translation [aprop_tr' (length args) name] |> Sign.declare_const_global ((binding, predT), NoSyn) |> snd |> Global_Theory.add_defs false [((Thm.def_binding binding, Logic.mk_equals (head, body)), [])]; val defs_ctxt = Proof_Context.init_global defs_thy |> Variable.declare_term head; val intro = Goal.prove_global defs_thy [] norm_ts statement (fn {context = ctxt, ...} => rewrite_goals_tac ctxt [pred_def] THEN compose_tac defs_ctxt (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN compose_tac defs_ctxt (false, Conjunction.intr_balanced (map (Thm.assume o Thm.cterm_of defs_ctxt) norm_ts), 0) 1); val conjuncts = (Drule.equal_elim_rule2 OF [body_eq, rewrite_rule defs_ctxt [pred_def] (Thm.assume (Thm.cterm_of defs_ctxt statement))]) |> Conjunction.elim_balanced (length ts); val (_, axioms_ctxt) = defs_ctxt |> Assumption.add_assumes (maps Thm.chyps_of (defs @ conjuncts)); val axioms = ts ~~ conjuncts |> map (fn (t, ax) => Element.prove_witness axioms_ctxt t (rewrite_goals_tac axioms_ctxt defs THEN compose_tac axioms_ctxt (false, ax, 0) 1)); in ((statement, intro, axioms), defs_thy) end; in (* main predicate definition function *) fun define_preds binding parms (((exts, exts'), (ints, ints')), defs) thy = let val ctxt = Proof_Context.init_global thy; val defs' = map (Thm.cterm_of ctxt #> Assumption.assume ctxt #> Drule.abs_def) defs; val (a_pred, a_intro, a_axioms, thy'') = if null exts then (NONE, NONE, [], thy) else let val abinding = if null ints then binding else Binding.suffix_name ("_" ^ axiomsN) binding; val ((statement, intro, axioms), thy') = thy |> def_pred abinding parms defs' exts exts'; val ((_, [intro']), thy'') = thy' |> Sign.qualified_path true abinding |> Global_Theory.note_thms "" ((Binding.name introN, []), [([intro], [Locale.unfold_add])]) ||> Sign.restore_naming thy'; in (SOME statement, SOME intro', axioms, thy'') end; val (b_pred, b_intro, b_axioms, thy'''') = if null ints then (NONE, NONE, [], thy'') else let val ((statement, intro, axioms), thy''') = thy'' |> def_pred binding parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred); val ctxt''' = Proof_Context.init_global thy'''; val ([(_, [intro']), _], thy'''') = thy''' |> Sign.qualified_path true binding |> Global_Theory.note_thmss "" [((Binding.name introN, []), [([intro], [Locale.intro_add])]), ((Binding.name axiomsN, []), [(map (Drule.export_without_context o Element.conclude_witness ctxt''') axioms, [])])] ||> Sign.restore_naming thy'''; in (SOME statement, SOME intro', axioms, thy'''') end; in ((a_pred, a_intro, a_axioms), (b_pred, b_intro, b_axioms), thy'''') end; end; local fun assumes_to_notes (Assumes asms) axms = fold_map (fn (a, spec) => fn axs => let val (ps, qs) = chop (length spec) axs in ((a, [(ps, [])]), qs) end) asms axms |> apfst (curry Notes "") | assumes_to_notes e axms = (e, axms); fun defines_to_notes ctxt (Defines defs) = Notes ("", map (fn (a, (def, _)) => (a, [([Assumption.assume ctxt (Thm.cterm_of ctxt def)], [(Attrib.internal o K) Locale.witness_add])])) defs) | defines_to_notes _ e = e; val is_hyp = fn Assumes _ => true | Defines _ => true | _ => false; fun gen_add_locale prep_include prep_decl binding raw_predicate_binding raw_includes raw_import raw_body thy = let val name = Sign.full_name thy binding; val _ = Locale.defined thy name andalso error ("Duplicate definition of locale " ^ quote name); val ctxt = Proof_Context.init_global thy; val includes = map (prep_include ctxt) raw_includes; val ((fixed, deps, body_elems, _), (parms, ctxt')) = ctxt |> Bundle.includes includes |> prep_decl raw_import I raw_body; val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems; val type_tfrees = TFrees.build (fold (TFrees.add_tfreesT o #2) parms); val extra_tfrees = - TFrees.build (exts' |> (fold o Term.fold_types o Term.fold_atyps) - (fn TFree v => not (TFrees.defined type_tfrees v) ? TFrees.add_set v | _ => I)); + TFrees.build (fold (TFrees.add_tfrees_unless (TFrees.defined type_tfrees)) exts') val extraTs = TFrees.list_set_rev extra_tfrees; val _ = if null extraTs then () else warning ("Additional type variable(s) in locale specification " ^ Binding.print binding ^ ": " ^ commas (map (Syntax.string_of_typ ctxt' o TFree) (sort_by #1 extraTs))); val predicate_binding = if Binding.is_empty raw_predicate_binding then binding else raw_predicate_binding; val ((a_statement, a_intro, a_axioms), (b_statement, b_intro, b_axioms), thy') = define_preds predicate_binding parms text thy; val pred_ctxt = Proof_Context.init_global thy'; val a_satisfy = Element.satisfy_morphism a_axioms; val b_satisfy = Element.satisfy_morphism b_axioms; val params = fixed @ maps (fn Fixes fixes => map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fixes | _ => []) body_elems; val asm = if is_some b_statement then b_statement else a_statement; val hyp_spec = filter is_hyp body_elems; val notes = if is_some asm then [("", [((Binding.suffix_name ("_" ^ axiomsN) binding, []), [([Assumption.assume pred_ctxt (Thm.cterm_of pred_ctxt (the asm))], [(Attrib.internal o K) Locale.witness_add])])])] else []; val notes' = body_elems |> map (defines_to_notes pred_ctxt) |> map (Element.transform_ctxt a_satisfy) |> (fn elems => fold_map assumes_to_notes elems (map (Element.conclude_witness pred_ctxt) a_axioms)) |> fst |> map (Element.transform_ctxt b_satisfy) |> map_filter (fn Notes notes => SOME notes | _ => NONE); val deps' = map (fn (l, morph) => (l, morph $> b_satisfy)) deps; val axioms = map (Element.conclude_witness pred_ctxt) b_axioms; val loc_ctxt = thy' |> Locale.register_locale binding (extraTs, params) (asm, rev defs) (a_intro, b_intro) axioms hyp_spec [] (rev notes) (rev deps') |> Named_Target.init includes name |> fold (fn (kind, facts) => Local_Theory.notes_kind kind facts #> snd) notes'; in (name, loc_ctxt) end; in val add_locale = gen_add_locale (K I) cert_declaration; val add_locale_cmd = gen_add_locale Bundle.check read_declaration; end; end; diff --git a/src/Pure/Isar/generic_target.ML b/src/Pure/Isar/generic_target.ML --- a/src/Pure/Isar/generic_target.ML +++ b/src/Pure/Isar/generic_target.ML @@ -1,472 +1,472 @@ (* Title: Pure/Isar/generic_target.ML Author: Makarius Author: Florian Haftmann, TU Muenchen Common target infrastructure. *) signature GENERIC_TARGET = sig (*auxiliary*) val export_abbrev: Proof.context -> (term -> term) -> term -> term * ((string * sort) list * (term list * term list)) val check_mixfix: Proof.context -> binding * (string * sort) list -> mixfix -> mixfix val check_mixfix_global: binding * bool -> mixfix -> mixfix (*background primitives*) val background_foundation: ((binding * typ) * mixfix) * (binding * term) -> term list * term list -> local_theory -> (term * thm) * local_theory val background_declaration: declaration -> local_theory -> local_theory val background_abbrev: binding * term -> term list -> local_theory -> (term * term) * local_theory val add_foundation_interpretation: (binding * (term * term list) -> Context.generic -> Context.generic) -> theory -> theory (*nested local theories primitives*) val standard_facts: local_theory -> Proof.context -> Attrib.fact list -> Attrib.fact list val standard_notes: (int * int -> bool) -> string -> Attrib.fact list -> local_theory -> local_theory val standard_declaration: (int * int -> bool) -> (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory val local_interpretation: Locale.registration -> local_theory -> local_theory (*lifting target primitives to local theory operations*) val define: (((binding * typ) * mixfix) * (binding * term) -> term list * term list -> local_theory -> (term * thm) * local_theory) -> bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory -> (term * (string * thm)) * local_theory val notes: (string -> Attrib.fact list -> Attrib.fact list -> local_theory -> local_theory) -> string -> Attrib.fact list -> local_theory -> (string * thm list) list * local_theory val abbrev: (Syntax.mode -> binding * mixfix -> term -> term list * term list -> local_theory -> local_theory) -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory (*theory target primitives*) val theory_target_foundation: ((binding * typ) * mixfix) * (binding * term) -> term list * term list -> local_theory -> (term * thm) * local_theory val theory_target_notes: string -> Attrib.fact list -> Attrib.fact list -> local_theory -> local_theory val theory_target_abbrev: Syntax.mode -> (binding * mixfix) -> term -> term list * term list -> local_theory -> local_theory (*theory target operations*) val theory_abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory val theory_declaration: declaration -> local_theory -> local_theory val theory_registration: Locale.registration -> local_theory -> local_theory (*locale target primitives*) val locale_target_notes: string -> string -> Attrib.fact list -> Attrib.fact list -> local_theory -> local_theory val locale_target_abbrev: string -> Syntax.mode -> (binding * mixfix) -> term -> term list * term list -> local_theory -> local_theory val locale_target_declaration: string -> bool -> declaration -> local_theory -> local_theory val locale_target_const: string -> (morphism -> bool) -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory (*locale operations*) val locale_abbrev: string -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> (term * term) * local_theory val locale_declaration: string -> {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory val locale_const: string -> Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory val locale_dependency: string -> Locale.registration -> local_theory -> local_theory end structure Generic_Target: GENERIC_TARGET = struct (** consts **) fun export_abbrev lthy preprocess rhs = let val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy); val rhs' = rhs |> Assumption.export_term lthy (Local_Theory.target_of lthy) |> preprocess; val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) (Variable.add_fixed lthy rhs' [])); val u = fold_rev lambda term_params rhs'; val global_rhs = singleton (Variable.polymorphic thy_ctxt) u; val type_tfrees = TFrees.build (TFrees.add_tfreesT (Term.fastype_of u)); val extra_tfrees = - build_rev (u |> (Term.fold_types o Term.fold_atyps) - (fn TFree v => not (TFrees.defined type_tfrees v) ? insert (op =) v | _ => I)); + TFrees.build (TFrees.add_tfrees_unless (TFrees.defined type_tfrees) u) + |> TFrees.list_set; val type_params = map (Logic.mk_type o TFree) extra_tfrees; in (global_rhs, (extra_tfrees, (type_params, term_params))) end; fun check_mixfix ctxt (b, extra_tfrees) mx = if null extra_tfrees then mx else (if Context_Position.is_visible ctxt then warning ("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^ commas (map (Syntax.string_of_typ ctxt o TFree) (sort_by #1 extra_tfrees)) ^ (if Mixfix.is_empty mx then "" else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx))) else (); NoSyn); fun check_mixfix_global (b, no_params) mx = if no_params orelse Mixfix.is_empty mx then mx else (warning ("Dropping global mixfix syntax: " ^ Binding.print b ^ " " ^ Pretty.string_of (Mixfix.pretty_mixfix mx)); NoSyn); fun same_const (Const (c, _), Const (c', _)) = c = c' | same_const (t $ _, t' $ _) = same_const (t, t') | same_const (_, _) = false; fun const_decl phi_pred prmode ((b, mx), rhs) phi context = if phi_pred phi then let val b' = Morphism.binding phi b; val rhs' = Morphism.term phi rhs; val same_shape = Term.aconv_untyped (rhs, rhs'); val same_stem = same_shape orelse same_const (rhs, rhs'); val const_alias = if same_shape then (case rhs' of Const (c, T) => let val thy = Context.theory_of context; val ctxt = Context.proof_of context; in (case Type_Infer_Context.const_type ctxt c of SOME T' => if Sign.typ_equiv thy (T, T') then SOME c else NONE | NONE => NONE) end | _ => NONE) else NONE; in (case const_alias of SOME c => context |> Context.mapping (Sign.const_alias b' c) (Proof_Context.const_alias b' c) |> Morphism.form (Proof_Context.generic_notation true prmode [(rhs', mx)]) | NONE => context |> Proof_Context.generic_add_abbrev Print_Mode.internal (b', Term.close_schematic_term rhs') |-> (fn (const as Const (c, _), _) => same_stem ? (Proof_Context.generic_revert_abbrev (#1 prmode) c #> same_shape ? Morphism.form (Proof_Context.generic_notation true prmode [(const, mx)])))) end else context; (** background primitives **) structure Foundation_Interpretations = Theory_Data ( type T = (binding * (term * term list) -> Context.generic -> Context.generic) Inttab.table; val empty = Inttab.empty; val extend = I; val merge = Inttab.merge (K true); ); fun add_foundation_interpretation f = Foundation_Interpretations.map (Inttab.update_new (serial (), f)); fun foundation_interpretation binding_const_params lthy = let val interps = Foundation_Interpretations.get (Proof_Context.theory_of lthy); val interp = Inttab.fold (fn (_, f) => f binding_const_params) interps; in lthy |> Local_Theory.background_theory (Context.theory_map interp) |> Local_Theory.map_contexts (K (Context.proof_map interp)) end; fun background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) lthy = let val params = type_params @ term_params; val target_params = type_params @ take_prefix is_Free (Variable.export_terms lthy (Local_Theory.target_of lthy) term_params); val mx' = check_mixfix_global (b, null params) mx; val (const, lthy2) = lthy |> Local_Theory.background_theory_result (Sign.declare_const lthy ((b, U), mx')); val lhs = Term.list_comb (const, params); val ((_, def), lthy3) = lthy2 |> Local_Theory.background_theory_result (Thm.add_def (Proof_Context.defs_context lthy2) false false (Thm.def_binding_optional b b_def, Logic.mk_equals (lhs, rhs))) ||> foundation_interpretation (b, (const, target_params)); in ((lhs, def), lthy3) end; fun background_declaration decl lthy = let fun theory_decl context = Local_Theory.standard_form lthy (Proof_Context.init_global (Context.theory_of context)) decl context; in Local_Theory.background_theory (Context.theory_map theory_decl) lthy end; fun background_abbrev (b, global_rhs) params = Local_Theory.background_theory_result (Sign.add_abbrev Print_Mode.internal (b, global_rhs)) #>> apply2 (fn t => Term.list_comb (Logic.unvarify_global t, params)) (** nested local theories primitives **) fun standard_facts lthy ctxt = Attrib.transform_facts (Local_Theory.standard_morphism lthy ctxt); fun standard_notes pred kind facts lthy = Local_Theory.map_contexts (fn level => fn ctxt => if pred (Local_Theory.level lthy, level) then Attrib.local_notes kind (standard_facts lthy ctxt facts) ctxt |> snd else ctxt) lthy; fun standard_declaration pred decl lthy = Local_Theory.map_contexts (fn level => fn ctxt => if pred (Local_Theory.level lthy, level) then Context.proof_map (Local_Theory.standard_form lthy ctxt decl) ctxt else ctxt) lthy; fun standard_const pred prmode ((b, mx), rhs) = standard_declaration pred (const_decl (K true) prmode ((b, mx), rhs)); fun standard_registration pred registration lthy = Local_Theory.map_contexts (fn level => if pred (Local_Theory.level lthy, level) then Context.proof_map (Locale.add_registration registration) else I) lthy; val local_interpretation = standard_registration (fn (n, level) => level = n - 1); (** lifting target primitives to local theory operations **) (* define *) fun define foundation internal ((b, mx), ((b_def, atts), rhs)) lthy = let val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of lthy); (*term and type parameters*) val ((defs, _), rhs') = Thm.cterm_of lthy rhs |> Local_Defs.export_cterm lthy thy_ctxt ||> Thm.term_of; val xs = Variable.add_fixed lthy rhs' []; val T = Term.fastype_of rhs; val type_tfrees = TFrees.build (TFrees.add_tfreesT T #> fold (TFrees.add_tfreesT o #2) xs); val extra_tfrees = - build_rev (rhs |> (Term.fold_types o Term.fold_atyps) - (fn TFree v => not (TFrees.defined type_tfrees v) ? insert (op =) v | _ => I)); + TFrees.build (rhs |> TFrees.add_tfrees_unless (TFrees.defined type_tfrees)) + |> TFrees.list_set; val mx' = check_mixfix lthy (b, extra_tfrees) mx; val type_params = map (Logic.mk_type o TFree) extra_tfrees; val term_params = map Free (sort (Variable.fixed_ord lthy o apply2 #1) xs); val params = type_params @ term_params; val U = map Term.fastype_of params ---> T; (*foundation*) val ((lhs', global_def), lthy2) = lthy |> foundation (((b, U), mx'), (b_def, rhs')) (type_params, term_params); (*local definition*) val ([(lhs, (_, local_def))], lthy3) = lthy2 |> Context_Position.set_visible false |> Local_Defs.define [((b, NoSyn), (Binding.empty_atts, lhs'))] ||> Context_Position.restore_visible lthy2; (*result*) val def = Thm.transitive local_def global_def |> Local_Defs.contract lthy3 defs (Thm.cterm_of lthy3 (Logic.mk_equals (lhs, rhs))); val ([(res_name, [res])], lthy4) = lthy3 |> Local_Theory.notes [((if internal then Binding.empty else b_def, atts), [([def], [])])]; in ((lhs, (res_name, res)), lthy4) end; (* notes *) local fun import_export_proof ctxt (name, raw_th) = let val thy_ctxt = Proof_Context.init_global (Proof_Context.theory_of ctxt); (*export assumes/defines*) val th = Goal.norm_result ctxt raw_th; val ((defs, asms), th') = Local_Defs.export ctxt thy_ctxt th; val asms' = map (rewrite_rule ctxt (Drule.norm_hhf_eqs @ defs)) asms; (*export fixes*) val tfrees = map TFree (Thm.fold_terms {hyps = true} Term.add_tfrees th' []); val frees = map Free (Thm.fold_terms {hyps = true} Term.add_frees th' []); val (th'' :: vs) = (th' :: map (Drule.mk_term o Thm.cterm_of ctxt) (map Logic.mk_type tfrees @ frees)) |> Variable.export ctxt thy_ctxt |> Drule.zero_var_indexes_list; (*thm definition*) val result = Global_Theory.name_thm Global_Theory.official1 name th''; (*import fixes*) val (tvars, vars) = chop (length tfrees) (map (Thm.term_of o Drule.dest_term) vs) |>> map Logic.dest_type; val instT = TVars.build (fold2 (fn a => fn b => (case a of TVar v => TVars.add (v, b) | _ => I)) tvars tfrees); val cinstT = TVars.fold (fn (v, T) => cons (v, Thm.ctyp_of ctxt T)) instT []; val cinst = map_filter (fn (Var (xi, T), t) => SOME ((xi, Term_Subst.instantiateT instT T), Thm.cterm_of ctxt (Term.map_types (Term_Subst.instantiateT instT) t)) | _ => NONE) (vars ~~ frees); val result' = Thm.instantiate (cinstT, cinst) result; (*import assumes/defines*) val result'' = (fold (curry op COMP) asms' result' handle THM _ => raise THM ("Failed to re-import result", 0, result' :: asms')) |> Local_Defs.contract ctxt defs (Thm.cprop_of th) |> Goal.norm_result ctxt |> Global_Theory.name_thm Global_Theory.unofficial2 name; in (result'', result) end; fun bind_name lthy b = (Local_Theory.full_name lthy b, Binding.default_pos_of b); fun map_facts f = map (apsnd (map (apfst (map f)))); in fun notes target_notes kind facts lthy = let val facts' = facts |> map (fn (a, bs) => (a, Global_Theory.burrow_fact (Global_Theory.name_multi (bind_name lthy (fst a))) bs)) |> map_facts (import_export_proof lthy); val local_facts = map_facts #1 facts'; val global_facts = map_facts #2 facts'; in lthy |> target_notes kind global_facts (Attrib.partial_evaluation lthy local_facts) |> Attrib.local_notes kind local_facts end; end; (* abbrev *) fun abbrev target_abbrev prmode ((b, mx), rhs) lthy = let val (global_rhs, (extra_tfrees, (type_params, term_params))) = export_abbrev lthy I rhs; val mx' = check_mixfix lthy (b, extra_tfrees) mx; in lthy |> target_abbrev prmode (b, mx') global_rhs (type_params, term_params) |> Context_Position.set_visible false |> Proof_Context.add_abbrev Print_Mode.internal (b, rhs) |> snd |> Local_Defs.fixed_abbrev ((b, NoSyn), rhs) ||> Context_Position.restore_visible lthy end; (** theory target primitives **) fun theory_target_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) = background_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params) #-> (fn (lhs, def) => standard_const (op <>) Syntax.mode_default ((b, mx), lhs) #> pair (lhs, def)); fun theory_target_notes kind global_facts local_facts = Local_Theory.background_theory (Attrib.global_notes kind global_facts #> snd) #> standard_notes (op <>) kind local_facts; fun theory_target_abbrev prmode (b, mx) global_rhs params = Local_Theory.background_theory_result (Sign.add_abbrev (#1 prmode) (b, global_rhs) #-> (fn (lhs, _) => (* FIXME type_params!? *) Sign.notation true prmode [(lhs, check_mixfix_global (b, null (snd params)) mx)] #> pair lhs)) #-> (fn lhs => standard_const (op <>) prmode ((b, if null (snd params) then NoSyn else mx), Term.list_comb (Logic.unvarify_global lhs, snd params))); (** theory operations **) val theory_abbrev = abbrev theory_target_abbrev; fun theory_declaration decl = background_declaration decl #> standard_declaration (K true) decl; fun target_registration lthy {inst, mixin, export} = {inst = inst, mixin = mixin, export = export $> Proof_Context.export_morphism lthy (Local_Theory.target_of lthy)}; fun theory_registration registration lthy = lthy |> (Local_Theory.raw_theory o Context.theory_map) (Locale.add_registration (target_registration lthy registration)) |> standard_registration (K true) registration; (** locale target primitives **) fun locale_target_notes locale kind global_facts local_facts = Local_Theory.background_theory (Attrib.global_notes kind (Attrib.map_facts (K []) global_facts) #> snd) #> (fn lthy => lthy |> Local_Theory.target (fn ctxt => ctxt |> Locale.add_facts locale kind (standard_facts lthy ctxt local_facts))) #> standard_notes (fn (this, other) => other <> 0 andalso this <> other) kind local_facts; fun locale_target_declaration locale syntax decl lthy = lthy |> Local_Theory.target (fn ctxt => ctxt |> Locale.add_declaration locale syntax (Morphism.transform (Local_Theory.standard_morphism lthy ctxt) decl)); fun locale_target_const locale phi_pred prmode ((b, mx), rhs) = locale_target_declaration locale true (const_decl phi_pred prmode ((b, mx), rhs)) (** locale operations **) fun locale_declaration locale {syntax, pervasive} decl = pervasive ? background_declaration decl #> locale_target_declaration locale syntax decl #> standard_declaration (fn (_, other) => other <> 0) decl; fun locale_const locale prmode ((b, mx), rhs) = locale_target_const locale (K true) prmode ((b, mx), rhs) #> standard_const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs); fun locale_dependency loc registration lthy = lthy |> Local_Theory.raw_theory (Locale.add_dependency loc registration) |> standard_registration (K true) registration; (** locale abbreviations **) fun locale_target_abbrev locale prmode (b, mx) global_rhs params = background_abbrev (b, global_rhs) (snd params) #-> (fn (lhs, _) => locale_const locale prmode ((b, mx), lhs)); fun locale_abbrev locale = abbrev (locale_target_abbrev locale); end; diff --git a/src/Pure/primitive_defs.ML b/src/Pure/primitive_defs.ML --- a/src/Pure/primitive_defs.ML +++ b/src/Pure/primitive_defs.ML @@ -1,85 +1,86 @@ (* Title: Pure/primitive_defs.ML Author: Makarius Primitive definition forms. *) signature PRIMITIVE_DEFS = sig val dest_def: Proof.context -> {check_head: term -> bool, check_free_lhs: string -> bool, check_free_rhs: string -> bool, check_tfree: string -> bool} -> term -> (term * term) * term list * term val abs_def: term -> term * term end; structure Primitive_Defs: PRIMITIVE_DEFS = struct fun term_kind (Const _) = "existing constant " | term_kind (Free _) = "free variable " | term_kind (Bound _) = "bound variable " | term_kind _ = ""; (*c x \ t[x] to \x. c x \ t[x]*) fun dest_def ctxt {check_head, check_free_lhs, check_free_rhs, check_tfree} eq = let fun err msg = raise TERM (msg, [eq]); val eq_vars = Term.strip_all_vars eq; val eq_body = Term.strip_all_body eq; val display_terms = commas_quote o map (Syntax.string_of_term ctxt o Syntax_Trans.bound_vars eq_vars); val display_types = commas_quote o map (Syntax.string_of_typ ctxt); val (raw_lhs, rhs) = Logic.dest_equals eq_body handle TERM _ => err "Not a meta-equality (\)"; val lhs = Envir.beta_eta_contract raw_lhs; val (head, args) = Term.strip_comb lhs; val head_tfrees = TFrees.build (TFrees.add_tfrees head); fun check_arg (Bound _) = true | check_arg (Free (x, _)) = check_free_lhs x | check_arg (Const ("Pure.type", Type ("itself", [TFree _]))) = true | check_arg _ = false; fun close_arg (Bound _) t = t | close_arg x t = Logic.all x t; val lhs_bads = filter_out check_arg args; val lhs_dups = duplicates (op aconv) args; val rhs_extras = Term.fold_aterms (fn v as Free (x, _) => if check_free_rhs x orelse member (op aconv) args v then I else insert (op aconv) v | _ => I) rhs []; - val rhs_extrasT = Term.fold_aterms (Term.fold_types (fn v as TFree (a, S) => - if check_tfree a orelse TFrees.defined head_tfrees (a, S) then I - else insert (op =) v | _ => I)) rhs []; + val rhs_extrasT = + TFrees.build (rhs |> TFrees.add_tfrees_unless + (fn (a, S) => check_tfree a orelse TFrees.defined head_tfrees (a, S))) + |> TFrees.list_set_rev |> map TFree; in if not (check_head head) then err ("Bad head of lhs: " ^ term_kind head ^ display_terms [head]) else if not (null lhs_bads) then err ("Bad arguments on lhs: " ^ display_terms lhs_bads) else if not (null lhs_dups) then err ("Duplicate arguments on lhs: " ^ display_terms lhs_dups) else if not (null rhs_extras) then err ("Extra variables on rhs: " ^ display_terms rhs_extras) else if not (null rhs_extrasT) then err ("Extra type variables on rhs: " ^ display_types rhs_extrasT) else if exists_subterm (fn t => t aconv head) rhs then err "Entity to be defined occurs on rhs" else ((lhs, rhs), args, fold_rev close_arg args (Logic.list_all (eq_vars, (Logic.mk_equals (lhs, rhs))))) end; (*\x. c x \ t[x] to c \ \x. t[x]*) fun abs_def eq = let val body = Term.strip_all_body eq; val vars = map Free (Term.rename_wrt_term body (Term.strip_all_vars eq)); val (lhs, rhs) = Logic.dest_equals (Term.subst_bounds (vars, body)); val (lhs', args) = Term.strip_comb lhs; val rhs' = fold_rev (absfree o dest_Free) args rhs; in (lhs', rhs') end; end; diff --git a/src/Pure/term_items.ML b/src/Pure/term_items.ML --- a/src/Pure/term_items.ML +++ b/src/Pure/term_items.ML @@ -1,193 +1,198 @@ (* Title: Pure/term_items.ML Author: Makarius Scalable collections of term items: - table: e.g. for instantiation - set with order of addition, e.g. occurrences within term *) signature TERM_ITEMS = sig type key type 'a table val empty: 'a table val build: ('a table -> 'a table) -> 'a table val size: 'a table -> int val is_empty: 'a table -> bool val map: (key -> 'a -> 'b) -> 'a table -> 'b table val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a val dest: 'a table -> (key * 'a) list val keys: 'a table -> key list val exists: (key * 'a -> bool) -> 'a table -> bool val forall: (key * 'a -> bool) -> 'a table -> bool val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option val lookup: 'a table -> key -> 'a option val defined: 'a table -> key -> bool val add: key * 'a -> 'a table -> 'a table val make: (key * 'a) list -> 'a table type set = int table val add_set: key -> set -> set val make_set: key list -> set val list_set: set -> key list val list_set_rev: set -> key list val subset: set * set -> bool val eq_set: set * set -> bool end; functor Term_Items(Key: KEY): TERM_ITEMS = struct (* table with length *) structure Table = Table(Key); type key = Table.key; datatype 'a table = Items of int * 'a Table.table; fun size (Items (n, _)) = n; fun table (Items (_, tab)) = tab; val empty = Items (0, Table.empty); fun build (f: 'a table -> 'a table) = f empty; fun is_empty items = size items = 0; fun dest items = Table.dest (table items); fun keys items = Table.keys (table items); fun exists pred = Table.exists pred o table; fun forall pred = Table.forall pred o table; fun get_first get = Table.get_first get o table; fun lookup items = Table.lookup (table items); fun defined items = Table.defined (table items); fun add (key, x) (items as Items (n, tab)) = if Table.defined tab key then items else Items (n + 1, Table.update_new (key, x) tab); fun make entries = build (fold add entries); (* set with order of addition *) type set = int table; fun add_set x (items as Items (n, tab)) = if Table.defined tab x then items else Items (n + 1, Table.update_new (x, n) tab); fun make_set xs = build (fold add_set xs); fun subset (A: set, B: set) = forall (defined B o #1) A; fun eq_set (A: set, B: set) = size A = size B andalso subset (A, B); fun list_set_ord ord items = Table.dest (table items) |> sort (ord o apply2 #2) |> map #1 val list_set = list_set_ord int_ord; val list_set_rev = list_set_ord (rev_order o int_ord); fun map f (Items (n, tab)) = Items (n, Table.map f tab); fun fold f = Table.fold f o table; fun fold_rev f = Table.fold_rev f o table; end; structure TFrees: sig include TERM_ITEMS val add_tfreesT: typ -> set -> set val add_tfrees: term -> set -> set + val add_tfreesT_unless: (string * sort -> bool) -> typ -> set -> set + val add_tfrees_unless: (string * sort -> bool) -> term -> set -> set end = struct structure Items = Term_Items ( type key = string * sort; val ord = pointer_eq_ord (prod_ord fast_string_ord Term_Ord.sort_ord); ); open Items; val add_tfreesT = fold_atyps (fn TFree v => add_set v | _ => I); val add_tfrees = fold_types add_tfreesT; +fun add_tfreesT_unless pred = Term.fold_atyps (fn TFree v => not (pred v) ? add_set v | _ => I); +fun add_tfrees_unless pred = fold_types (add_tfreesT_unless pred); + end; structure TVars: sig include TERM_ITEMS val add_tvarsT: typ -> set -> set val add_tvars: term -> set -> set end = struct structure Term_Items = Term_Items( type key = indexname * sort; val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord Term_Ord.sort_ord); ); open Term_Items; val add_tvarsT = fold_atyps (fn TVar v => add_set v | _ => I); val add_tvars = fold_types add_tvarsT; end; structure Frees: sig include TERM_ITEMS val add_frees: term -> set -> set end = struct structure Term_Items = Term_Items ( type key = string * typ; val ord = pointer_eq_ord (prod_ord fast_string_ord Term_Ord.typ_ord); ); open Term_Items; val add_frees = fold_aterms (fn Free v => add_set v | _ => I); end; structure Vars: sig include TERM_ITEMS val add_vars: term -> set -> set end = struct structure Term_Items = Term_Items ( type key = indexname * typ; val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord Term_Ord.typ_ord) ); open Term_Items; val add_vars = fold_aterms (fn Var v => add_set v | _ => I); end; structure Names: sig include TERM_ITEMS val add_tfree_namesT: typ -> set -> set val add_tfree_names: term -> set -> set val add_free_names: term -> set -> set end = struct structure Term_Items = Term_Items ( type key = string; val ord = fast_string_ord ); open Term_Items; val add_tfree_namesT = fold_atyps (fn TFree (a, _) => add_set a | _ => I); val add_tfree_names = fold_types add_tfree_namesT; val add_free_names = fold_aterms (fn Free (x, _) => add_set x | _ => I); end; diff --git a/src/Pure/theory.ML b/src/Pure/theory.ML --- a/src/Pure/theory.ML +++ b/src/Pure/theory.ML @@ -1,342 +1,342 @@ (* Title: Pure/theory.ML Author: Lawrence C Paulson and Markus Wenzel Logical theory content: axioms, definitions, and begin/end wrappers. *) signature THEORY = sig val parents_of: theory -> theory list val ancestors_of: theory -> theory list val nodes_of: theory -> theory list val setup: (theory -> theory) -> unit val local_setup: (Proof.context -> Proof.context) -> unit val install_pure: theory -> unit val get_pure: unit -> theory val get_pure_bootstrap: unit -> theory val get_markup: theory -> Markup.T val check: {long: bool} -> Proof.context -> string * Position.T -> theory val axiom_table: theory -> term Name_Space.table val axiom_space: theory -> Name_Space.T val all_axioms_of: theory -> (string * term) list val defs_of: theory -> Defs.T val at_begin: (theory -> theory option) -> theory -> theory val at_end: (theory -> theory option) -> theory -> theory val join_theory: theory list -> theory val begin_theory: string * Position.T -> theory list -> theory val end_theory: theory -> theory val add_axiom: Proof.context -> binding * term -> theory -> theory val const_dep: theory -> string * typ -> Defs.entry val type_dep: string * typ list -> Defs.entry val add_deps: Defs.context -> string -> Defs.entry -> Defs.entry list -> theory -> theory val add_deps_global: string -> Defs.entry -> Defs.entry list -> theory -> theory val add_def: Defs.context -> bool -> bool -> binding * term -> theory -> theory val specify_const: (binding * typ) * mixfix -> theory -> term * theory val check_overloading: Proof.context -> bool -> string * typ -> unit end structure Theory: THEORY = struct (** theory context operations **) val parents_of = Context.parents_of; val ancestors_of = Context.ancestors_of; fun nodes_of thy = thy :: ancestors_of thy; fun setup f = Context.>> (Context.map_theory f); fun local_setup f = Context.>> (Context.map_proof f); (* implicit theory Pure *) val pure: theory Single_Assignment.var = Single_Assignment.var "pure"; fun install_pure thy = Single_Assignment.assign pure thy; fun get_pure () = (case Single_Assignment.peek pure of SOME thy => thy | NONE => raise Fail "Theory Pure not present"); fun get_pure_bootstrap () = (case Single_Assignment.peek pure of SOME thy => thy | NONE => Context.the_global_context ()); (** datatype thy **) type wrapper = (theory -> theory option) * stamp; fun apply_wrappers (wrappers: wrapper list) = perhaps (perhaps_loop (perhaps_apply (map fst wrappers))); datatype thy = Thy of {pos: Position.T, id: serial, axioms: term Name_Space.table, defs: Defs.T, wrappers: wrapper list * wrapper list}; fun make_thy (pos, id, axioms, defs, wrappers) = Thy {pos = pos, id = id, axioms = axioms, defs = defs, wrappers = wrappers}; structure Thy = Theory_Data' ( type T = thy; val extend = I; val empty = make_thy (Position.none, 0, Name_Space.empty_table Markup.axiomN, Defs.empty, ([], [])); fun merge old_thys (thy1, thy2) = let val Thy {pos, id, axioms = axioms1, defs = defs1, wrappers = (bgs1, ens1)} = thy1; val Thy {pos = _, id = _, axioms = axioms2, defs = defs2, wrappers = (bgs2, ens2)} = thy2; val axioms' = Name_Space.merge_tables (axioms1, axioms2); val defs' = Defs.merge (Defs.global_context (fst old_thys)) (defs1, defs2); val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2); val ens' = Library.merge (eq_snd op =) (ens1, ens2); in make_thy (pos, id, axioms', defs', (bgs', ens')) end; ); fun rep_theory thy = Thy.get thy |> (fn Thy args => args); fun map_thy f = Thy.map (fn (Thy {pos, id, axioms, defs, wrappers}) => make_thy (f (pos, id, axioms, defs, wrappers))); fun map_axioms f = map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, f axioms, defs, wrappers)); fun map_defs f = map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, f defs, wrappers)); fun map_wrappers f = map_thy (fn (pos, id, axioms, defs, wrappers) => (pos, id, axioms, defs, f wrappers)); (* entity markup *) fun theory_markup def name id pos = if id = 0 then Markup.empty else Position.make_entity_markup def id Markup.theoryN (name, pos); fun init_markup (name, pos) thy = let val id = serial (); val _ = Context_Position.reports_global thy [(pos, theory_markup {def = true} name id pos)]; in map_thy (fn (_, _, axioms, defs, wrappers) => (pos, id, axioms, defs, wrappers)) thy end; fun get_markup thy = let val {pos, id, ...} = rep_theory thy in theory_markup {def = false} (Context.theory_long_name thy) id pos end; fun check long ctxt (name, pos) = let val thy = Proof_Context.theory_of ctxt; val thy' = Context.get_theory long thy name handle ERROR msg => let val completion_report = Completion.make_report (name, pos) (fn completed => map (Context.theory_name' long) (ancestors_of thy) |> filter (completed o Long_Name.base_name) |> sort_strings |> map (fn a => (a, (Markup.theoryN, a)))); in error (msg ^ Position.here pos ^ completion_report) end; val _ = Context_Position.report ctxt pos (get_markup thy'); in thy' end; (* basic operations *) val axiom_table = #axioms o rep_theory; val axiom_space = Name_Space.space_of_table o axiom_table; val all_axioms_of = Name_Space.dest_table o axiom_table; val defs_of = #defs o rep_theory; (* join theory *) fun join_theory [] = raise List.Empty | join_theory [thy] = thy | join_theory thys = foldl1 Context.join_thys thys; (* begin/end theory *) val begin_wrappers = rev o #1 o #wrappers o rep_theory; val end_wrappers = rev o #2 o #wrappers o rep_theory; fun at_begin f = map_wrappers (apfst (cons (f, stamp ()))); fun at_end f = map_wrappers (apsnd (cons (f, stamp ()))); fun begin_theory (name, pos) imports = if name = Context.PureN then (case imports of [thy] => init_markup (name, pos) thy | _ => error "Bad bootstrapping of theory Pure") else let val thy = Context.begin_thy name imports; val wrappers = begin_wrappers thy; in thy |> init_markup (name, pos) |> Sign.init_naming |> Sign.local_path |> apply_wrappers wrappers |> tap (Syntax.force_syntax o Sign.syn_of) end; fun end_theory thy = thy |> apply_wrappers (end_wrappers thy) |> Sign.change_check |> Context.finish_thy; (** primitive specifications **) (* raw axioms *) fun cert_axm ctxt (b, raw_tm) = let val thy = Proof_Context.theory_of ctxt; val t = Sign.cert_prop thy raw_tm handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg; val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg; val bad_sorts = rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I | (T, _) => insert (op =) T) t []); val _ = null bad_sorts orelse error ("Illegal sort constraints in primitive specification: " ^ commas (map (Syntax.string_of_typ (Config.put show_sorts true ctxt)) bad_sorts)); in (b, Sign.no_vars ctxt t) end handle ERROR msg => cat_error msg ("The error(s) above occurred in axiom " ^ Binding.print b); fun add_axiom ctxt raw_axm thy = thy |> map_axioms (fn axioms => let val axm = apsnd Logic.varify_global (cert_axm ctxt raw_axm); val context = ctxt |> Sign.inherit_naming thy |> Context_Position.set_visible_generic false; val (_, axioms') = Name_Space.define context true axm axioms; in axioms' end); (* dependencies *) fun const_dep thy (c, T) = ((Defs.Const, c), Sign.const_typargs thy (c, T)); fun type_dep (c, args) = ((Defs.Type, c), args); fun dependencies (context as (ctxt, _)) unchecked def description lhs rhs = let fun prep (item, args) = (case fold Term.add_tvarsT args [] of [] => (item, map Logic.varifyT_global args) | vs => raise TYPE ("Illegal schematic type variable(s)", map TVar vs, [])); - val lhs_vars = TFrees.build (snd lhs |> fold TFrees.add_tfreesT); + val lhs_vars = TFrees.build (fold TFrees.add_tfreesT (snd lhs)); val rhs_extras = - build (rhs |> fold (#2 #> (fold o Term.fold_atyps) - (fn TFree v => not (TFrees.defined lhs_vars v) ? insert (op =) v | _ => I))); + TFrees.build (rhs |> fold (fold (TFrees.add_tfreesT_unless (TFrees.defined lhs_vars)) o snd)) + |> TFrees.list_set_rev; val _ = if null rhs_extras then () else error ("Specification depends on extra type variables: " ^ commas_quote (map (Syntax.string_of_typ ctxt o TFree) rhs_extras) ^ "\nThe error(s) above occurred in " ^ quote description); in Defs.define context unchecked def description (prep lhs) (map prep rhs) end; fun cert_entry thy ((Defs.Const, c), args) = Sign.cert_term thy (Const (c, Sign.const_instance thy (c, args))) |> dest_Const |> const_dep thy | cert_entry thy ((Defs.Type, c), args) = Sign.certify_typ thy (Type (c, args)) |> dest_Type |> type_dep; fun add_deps context a raw_lhs raw_rhs thy = let val (lhs as ((_, lhs_name), _)) :: rhs = map (cert_entry thy) (raw_lhs :: raw_rhs); val description = if a = "" then lhs_name ^ " axiom" else a; in thy |> map_defs (dependencies context false NONE description lhs rhs) end; fun add_deps_global a x y thy = add_deps (Defs.global_context thy) a x y thy; fun specify_const decl thy = let val (t, thy') = Sign.declare_const_global decl thy; in (t, add_deps_global "" (const_dep thy' (dest_Const t)) [] thy') end; (* overloading *) fun check_overloading ctxt overloaded (c, T) = let val thy = Proof_Context.theory_of ctxt; val declT = Sign.the_const_constraint thy c handle TYPE (msg, _, _) => error msg; val T' = Logic.varifyT_global T; fun message sorts txt = [Pretty.block [Pretty.str "Specification of constant ", Pretty.str c, Pretty.str " ::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ (Config.put show_sorts sorts ctxt) T)], Pretty.str txt] |> Pretty.chunks |> Pretty.string_of; in if Sign.typ_instance thy (declT, T') then () else if Type.raw_instance (declT, T') then error (message true "imposes additional sort constraints on the constant declaration") else if overloaded then () else error (message false "is strictly less general than the declared type (overloading required)") end; (* definitional axioms *) local fun check_def (context as (ctxt, _)) thy unchecked overloaded (b, tm) defs = let val name = Sign.full_name thy b; val ((lhs, rhs), _, _) = Primitive_Defs.dest_def ctxt {check_head = Term.is_Const, check_free_lhs = K true, check_free_rhs = K false, check_tfree = K false} tm handle TERM (msg, _) => error msg; val lhs_const = Term.dest_Const (Term.head_of lhs); val rhs_consts = fold_aterms (fn Const const => insert (op =) (const_dep thy const) | _ => I) rhs []; val rhs_types = (fold_types o fold_subtypes) (fn Type t => insert (op =) (type_dep t) | _ => I) rhs []; val rhs_deps = rhs_consts @ rhs_types; val _ = check_overloading ctxt overloaded lhs_const; in defs |> dependencies context unchecked (SOME name) name (const_dep thy lhs_const) rhs_deps end handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block [Pretty.str ("The error(s) above occurred in definition " ^ Binding.print b ^ ":"), Pretty.fbrk, Pretty.quote (Syntax.pretty_term ctxt tm)])); in fun add_def (context as (ctxt, _)) unchecked overloaded raw_axm thy = let val axm = cert_axm ctxt raw_axm in thy |> map_defs (check_def context thy unchecked overloaded axm) |> add_axiom ctxt axm end; end; end;