# HG changeset patch # User wenzelm # Date 1392934593 -3600 # Node ID e4e8cbd9d780183be74c8008288bd8a52283e653 # Parent 9b1805ff3aae4df5e68b4802450a0804e2e70aff tuned whitespace; diff -r 9b1805ff3aae -r e4e8cbd9d780 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Thu Feb 20 21:55:37 2014 +0100 +++ b/src/Pure/Isar/expression.ML Thu Feb 20 23:16:33 2014 +0100 @@ -19,10 +19,12 @@ Proof.context -> (term * term list) list list * Proof.context (* Declaring locales *) - val cert_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context_i list -> + 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 -> + 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*) @@ -39,13 +41,16 @@ (term list list * (string * morphism) list * morphism) * Proof.context val read_goal_expression: expression -> Proof.context -> (term list list * (string * morphism) list * morphism) * Proof.context - val permanent_interpretation: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state - val ephemeral_interpretation: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state + val permanent_interpretation: expression_i -> (Attrib.binding * term) list -> + local_theory -> Proof.state + val ephemeral_interpretation: expression_i -> (Attrib.binding * term) list -> + local_theory -> Proof.state val interpret: expression_i -> (Attrib.binding * term) list -> bool -> Proof.state -> Proof.state val interpret_cmd: expression -> (Attrib.binding * string) list -> bool -> Proof.state -> Proof.state val interpretation: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state - val interpretation_cmd: expression -> (Attrib.binding * string) list -> local_theory -> Proof.state + val interpretation_cmd: expression -> (Attrib.binding * string) list -> + local_theory -> Proof.state val sublocale: expression_i -> (Attrib.binding * term) list -> local_theory -> Proof.state val sublocale_cmd: expression -> (Attrib.binding * string) list -> local_theory -> Proof.state val sublocale_global: (local_theory -> local_theory) -> string -> expression_i -> @@ -138,8 +143,11 @@ val implicit'' = if strict then [] else - let val _ = reject_dups - "Parameter(s) declared simultaneously in expression and for clause: " (implicit' @ fixed') + 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; @@ -492,7 +500,8 @@ let val (asm, defs) = Locale.specification_of thy name; in - (case asm of NONE => defs | SOME asm => asm :: defs) |> map (Morphism.term morph) + (case asm of NONE => defs | SOME asm => asm :: defs) + |> map (Morphism.term morph) end; fun prep_goal_expression prep expression context = @@ -581,12 +590,13 @@ 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 [(Attrib.empty_binding, [(the asm', [])])]) + val text' = + text |> + (if is_some asm then + eval_text ctxt false (Assumes [(Attrib.empty_binding, [(the asm', [])])]) else I) |> - (if not (null defs) - then eval_text ctxt false (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs')) + (if not (null defs) then + eval_text ctxt false (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs')) else I) (* FIXME clone from locale.ML *) in text' end; @@ -618,7 +628,8 @@ val body = Object_Logic.atomize_term thy t; val bodyT = Term.fastype_of body; in - if bodyT = propT then (t, propT, Thm.reflexive (Thm.cterm_of thy t)) + if bodyT = propT + then (t, propT, Thm.reflexive (Thm.cterm_of thy t)) else (body, bodyT, Object_Logic.atomize (Proof_Context.init_global thy) (Thm.cterm_of thy t)) end; @@ -700,7 +711,8 @@ if null exts then (NONE, NONE, [], thy) else let - val abinding = if null ints then binding else Binding.suffix_name ("_" ^ axiomsN) binding; + 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'; @@ -761,7 +773,9 @@ val text as (((_, exts'), _), defs) = eval ctxt' deps body_elems; val extraTs = - subtract (op =) (fold Term.add_tfreesT (map snd parms) []) (fold Term.add_tfrees exts' []); + subtract (op =) + (fold Term.add_tfreesT (map snd parms) []) + (fold Term.add_tfrees exts' []); val _ = if null extraTs then () else warning ("Additional type variable(s) in locale specification " ^ @@ -790,14 +804,15 @@ [(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 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; @@ -836,7 +851,8 @@ let val ((propss, deps, export), expr_ctxt) = prep_expr expression initial_ctxt; val eqns = prep_with_extended_syntax prep_prop deps expr_ctxt raw_eqns; - val attrss = map (apsnd (map (prep_attr (Proof_Context.theory_of initial_ctxt))) o fst) raw_eqns; + val attrss = + map (apsnd (map (prep_attr (Proof_Context.theory_of initial_ctxt))) o fst) raw_eqns; val goal_ctxt = fold Variable.auto_fixes eqns expr_ctxt; val export' = Variable.export_morphism goal_ctxt expr_ctxt; in (((propss, deps, export, export'), (eqns, attrss)), goal_ctxt) end; @@ -918,8 +934,10 @@ fun subscribe_locale_only lthy = let - val _ = if Named_Target.is_theory lthy - then error "Not possible on level of global theory" else (); + val _ = + if Named_Target.is_theory lthy + then error "Not possible on level of global theory" + else (); in subscribe lthy end; @@ -929,7 +947,7 @@ before_exit raw_locale expression raw_eqns thy = thy |> Named_Target.init before_exit (prep_loc thy raw_locale) - |> gen_local_theory_interpretation prep_interpretation subscribe_locale_only expression raw_eqns + |> gen_local_theory_interpretation prep_interpretation subscribe_locale_only expression raw_eqns; in diff -r 9b1805ff3aae -r e4e8cbd9d780 src/Pure/Isar/rule_cases.ML --- a/src/Pure/Isar/rule_cases.ML Thu Feb 20 21:55:37 2014 +0100 +++ b/src/Pure/Isar/rule_cases.ML Thu Feb 20 23:16:33 2014 +0100 @@ -233,7 +233,8 @@ (case AList.lookup (op =) (Thm.get_tags th) consumes_tagN of NONE => NONE | SOME s => - (case Lexicon.read_nat s of SOME n => SOME n + (case Lexicon.read_nat s of + SOME n => SOME n | _ => raise THM ("Malformed 'consumes' tag of theorem", 0, [th]))); fun get_consumes th = the_default 0 (lookup_consumes th); @@ -262,7 +263,8 @@ (case AList.lookup (op =) (Thm.get_tags th) constraints_tagN of NONE => NONE | SOME s => - (case Lexicon.read_nat s of SOME n => SOME n + (case Lexicon.read_nat s of + SOME n => SOME n | _ => raise THM ("Malformed 'constraints' tag of theorem", 0, [th]))); fun get_constraints th = the_default 0 (lookup_constraints th); @@ -341,7 +343,8 @@ fun save_case_concls th = let val concls = Thm.get_tags th |> map_filter (fn (a, b) => - if a = case_concl_tagN then (case explode_args b of c :: cs => SOME (c, cs) | _ => NONE) + if a = case_concl_tagN + then (case explode_args b of c :: cs => SOME (c, cs) | _ => NONE) else NONE) in fold add_case_concl concls end; @@ -385,7 +388,8 @@ (case lookup_case_names th of NONE => map (rpair [] o Library.string_of_int) (1 upto (Thm.nprems_of th - n)) | SOME names => map (fn name => (name, get_case_concls th name)) names); - val cases_hyps = (case lookup_cases_hyp_names th of + val cases_hyps = + (case lookup_cases_hyp_names th of NONE => replicate (length cases) [] | SOME names => names); fun regroup ((name,concls),hyps) = ((name,hyps),concls) diff -r 9b1805ff3aae -r e4e8cbd9d780 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Thu Feb 20 21:55:37 2014 +0100 +++ b/src/Pure/Isar/specification.ML Thu Feb 20 23:16:33 2014 +0100 @@ -46,7 +46,8 @@ val abbreviation_cmd: Syntax.mode -> (binding * string option * mixfix) option * string -> bool -> local_theory -> local_theory val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory - val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory + val type_notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> + local_theory -> local_theory val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory val theorems: string -> @@ -90,7 +91,8 @@ (case duplicates (op =) commons of [] => () | dups => error ("Duplicate local variables " ^ commas_quote dups)); val frees = rev (fold (Variable.add_free_names ctxt) As (rev commons)); - val types = map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length frees)); + val types = + map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length frees)); val uniform_typing = the o AList.lookup (op =) (frees ~~ types); fun abs_body lev y (Abs (x, T, b)) = Abs (x, T, abs_body (lev + 1) y b)