# HG changeset patch # User wenzelm # Date 1461744215 -7200 # Node ID c9605a284fbad83283503938281ec45a159e3fc5 # Parent 60406bf310f8e9598bb08638d941a97036f5ecf3 tuned; diff -r 60406bf310f8 -r c9605a284fba src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Tue Apr 26 22:59:25 2016 +0200 +++ b/src/Pure/Isar/specification.ML Wed Apr 27 10:03:35 2016 +0200 @@ -105,14 +105,15 @@ local -fun close_forms ctxt i As = +fun close_forms ctxt auto_close i prems concls = let - val xs = rev (fold (Variable.add_free_names ctxt) As []); + val xs = + if auto_close then rev (fold (Variable.add_free_names ctxt) (concls @ prems) []) + else []; val types = map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length xs)); val uniform_typing = AList.lookup (op =) (xs ~~ types); - val close = fold_rev (Logic.dependent_all_constraint uniform_typing) (xs ~~ xs); - in map close As end; + in map (Logic.close_prop_constraint uniform_typing (xs ~~ xs) prems) concls end; fun get_positions ctxt x = let @@ -127,7 +128,7 @@ | get _ _ = []; in get [] end; -fun prepare prep_var parse_prop prep_att do_close raw_vars raw_specss ctxt = +fun prepare prep_var parse_prop prep_att auto_close raw_vars raw_specss ctxt = let val (vars, vars_ctxt) = ctxt |> fold_map prep_var raw_vars; val (xs, params_ctxt) = vars_ctxt @@ -139,20 +140,21 @@ (map (Binding.pos_of o #1) vars ~~ map (Variable.markup_entity_def params_ctxt ##> Properties.remove Markup.kindN) xs); - val Asss = + val Asss0 = (map o map) snd raw_specss |> (burrow o burrow) (grouped 10 Par_List.map_independent (parse_prop params_ctxt)); - val names = Variable.names_of (params_ctxt |> (fold o fold o fold) Variable.declare_term Asss) + val names = + Variable.names_of (params_ctxt |> (fold o fold o fold) Variable.declare_term Asss0) |> fold Name.declare xs; - val Asss' = #1 ((fold_map o fold_map o fold_map) Term.free_dummy_patterns Asss names); - val idx = (fold o fold o fold) Term.maxidx_term Asss' ~1 + 1; - val specs = - (if do_close then - #1 (fold_map - (fn Ass => fn i => (burrow (close_forms params_ctxt i) Ass, i + 1)) Asss' idx) - else Asss') - |> flat |> burrow (Syntax.check_props params_ctxt); + val (Asss1, _) = (fold_map o fold_map o fold_map) Term.free_dummy_patterns Asss0 names; + val idx = (fold o fold o fold) Term.maxidx_term Asss1 ~1 + 1; + + val (Asss2, _) = + fold_map (fn Ass => fn i => (burrow (close_forms params_ctxt auto_close i []) Ass, i + 1)) + Asss1 idx; + + val specs = burrow (Syntax.check_props params_ctxt) (flat Asss2); val specs_ctxt = params_ctxt |> (fold o fold) Variable.declare_term specs; val ps = specs_ctxt |> fold_map Proof_Context.inferred_param xs |> fst; @@ -161,19 +163,17 @@ map (fn ((name, atts), _) => (name, map (prep_att ctxt) atts)) (flat raw_specss); fun get_pos x = - if do_close then Position.none - else - (case (maps o maps o maps) (get_positions specs_ctxt x) Asss' of - [] => Position.none - | pos :: _ => pos); + (case (maps o maps o maps) (get_positions specs_ctxt x) Asss2 of + [] => Position.none + | pos :: _ => pos); in (((params, name_atts ~~ specs), get_pos), specs_ctxt) end; fun single_spec (a, prop) = [(a, [prop])]; fun the_spec (a, [prop]) = (a, prop); -fun prep_spec prep_var parse_prop prep_att do_close vars specs = - prepare prep_var parse_prop prep_att do_close +fun prep_spec prep_var parse_prop prep_att auto_close vars specs = + prepare prep_var parse_prop prep_att auto_close vars (map single_spec specs) #>> (apfst o apsnd) (map the_spec); in diff -r 60406bf310f8 -r c9605a284fba src/Pure/logic.ML --- a/src/Pure/logic.ML Tue Apr 26 22:59:25 2016 +0200 +++ b/src/Pure/logic.ML Wed Apr 27 10:03:35 2016 +0200 @@ -28,6 +28,8 @@ val nth_prem: int * term -> term val close_term: (string * term) list -> term -> term val close_prop: (string * term) list -> term list -> term -> term + val close_prop_constraint: (string -> typ option) -> + (string * string) list -> term list -> term -> term val true_prop: term val conjunction: term val mk_conjunction: term * term -> term @@ -205,10 +207,15 @@ fun strip_horn A = (strip_imp_prems A, strip_imp_concl A); -(* close *) +(* close -- omit vacuous quantifiers *) val close_term = fold_rev Term.dependent_lambda_name; -fun close_prop xs As B = fold_rev dependent_all_name xs (list_implies (As, B)); + +fun close_prop xs As B = + fold_rev dependent_all_name xs (list_implies (As, B)); + +fun close_prop_constraint default_type xs As B = + fold_rev (dependent_all_constraint default_type) xs (list_implies (As, B)); (** conjunction **)