tuned;
authorwenzelm
Wed Apr 27 10:03:35 2016 +0200 (2016-04-27 ago)
changeset 63063c9605a284fba
parent 63062 60406bf310f8
child 63064 2f18172214c8
tuned;
src/Pure/Isar/specification.ML
src/Pure/logic.ML
     1.1 --- a/src/Pure/Isar/specification.ML	Tue Apr 26 22:59:25 2016 +0200
     1.2 +++ b/src/Pure/Isar/specification.ML	Wed Apr 27 10:03:35 2016 +0200
     1.3 @@ -105,14 +105,15 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun close_forms ctxt i As =
     1.8 +fun close_forms ctxt auto_close i prems concls =
     1.9    let
    1.10 -    val xs = rev (fold (Variable.add_free_names ctxt) As []);
    1.11 +    val xs =
    1.12 +      if auto_close then rev (fold (Variable.add_free_names ctxt) (concls @ prems) [])
    1.13 +      else [];
    1.14      val types =
    1.15        map (Type_Infer.param i o rpair []) (Name.invent Name.context Name.aT (length xs));
    1.16      val uniform_typing = AList.lookup (op =) (xs ~~ types);
    1.17 -    val close = fold_rev (Logic.dependent_all_constraint uniform_typing) (xs ~~ xs);
    1.18 -  in map close As end;
    1.19 +  in map (Logic.close_prop_constraint uniform_typing (xs ~~ xs) prems) concls end;
    1.20  
    1.21  fun get_positions ctxt x =
    1.22    let
    1.23 @@ -127,7 +128,7 @@
    1.24        | get _ _ = [];
    1.25    in get [] end;
    1.26  
    1.27 -fun prepare prep_var parse_prop prep_att do_close raw_vars raw_specss ctxt =
    1.28 +fun prepare prep_var parse_prop prep_att auto_close raw_vars raw_specss ctxt =
    1.29    let
    1.30      val (vars, vars_ctxt) = ctxt |> fold_map prep_var raw_vars;
    1.31      val (xs, params_ctxt) = vars_ctxt
    1.32 @@ -139,20 +140,21 @@
    1.33          (map (Binding.pos_of o #1) vars ~~
    1.34            map (Variable.markup_entity_def params_ctxt ##> Properties.remove Markup.kindN) xs);
    1.35  
    1.36 -    val Asss =
    1.37 +    val Asss0 =
    1.38        (map o map) snd raw_specss
    1.39        |> (burrow o burrow) (grouped 10 Par_List.map_independent (parse_prop params_ctxt));
    1.40 -    val names = Variable.names_of (params_ctxt |> (fold o fold o fold) Variable.declare_term Asss)
    1.41 +    val names =
    1.42 +      Variable.names_of (params_ctxt |> (fold o fold o fold) Variable.declare_term Asss0)
    1.43        |> fold Name.declare xs;
    1.44 -    val Asss' = #1 ((fold_map o fold_map o fold_map) Term.free_dummy_patterns Asss names);
    1.45 -    val idx = (fold o fold o fold) Term.maxidx_term Asss' ~1 + 1;
    1.46  
    1.47 -    val specs =
    1.48 -      (if do_close then
    1.49 -        #1 (fold_map
    1.50 -            (fn Ass => fn i => (burrow (close_forms params_ctxt i) Ass, i + 1)) Asss' idx)
    1.51 -      else Asss')
    1.52 -      |> flat |> burrow (Syntax.check_props params_ctxt);
    1.53 +    val (Asss1, _) = (fold_map o fold_map o fold_map) Term.free_dummy_patterns Asss0 names;
    1.54 +    val idx = (fold o fold o fold) Term.maxidx_term Asss1 ~1 + 1;
    1.55 +
    1.56 +    val (Asss2, _) =
    1.57 +      fold_map (fn Ass => fn i => (burrow (close_forms params_ctxt auto_close i []) Ass, i + 1))
    1.58 +        Asss1 idx;
    1.59 +
    1.60 +    val specs = burrow (Syntax.check_props params_ctxt) (flat Asss2);
    1.61      val specs_ctxt = params_ctxt |> (fold o fold) Variable.declare_term specs;
    1.62  
    1.63      val ps = specs_ctxt |> fold_map Proof_Context.inferred_param xs |> fst;
    1.64 @@ -161,19 +163,17 @@
    1.65        map (fn ((name, atts), _) => (name, map (prep_att ctxt) atts)) (flat raw_specss);
    1.66  
    1.67      fun get_pos x =
    1.68 -      if do_close then Position.none
    1.69 -      else
    1.70 -        (case (maps o maps o maps) (get_positions specs_ctxt x) Asss' of
    1.71 -          [] => Position.none
    1.72 -        | pos :: _ => pos);
    1.73 +      (case (maps o maps o maps) (get_positions specs_ctxt x) Asss2 of
    1.74 +        [] => Position.none
    1.75 +      | pos :: _ => pos);
    1.76    in (((params, name_atts ~~ specs), get_pos), specs_ctxt) end;
    1.77  
    1.78  
    1.79  fun single_spec (a, prop) = [(a, [prop])];
    1.80  fun the_spec (a, [prop]) = (a, prop);
    1.81  
    1.82 -fun prep_spec prep_var parse_prop prep_att do_close vars specs =
    1.83 -  prepare prep_var parse_prop prep_att do_close
    1.84 +fun prep_spec prep_var parse_prop prep_att auto_close vars specs =
    1.85 +  prepare prep_var parse_prop prep_att auto_close
    1.86      vars (map single_spec specs) #>> (apfst o apsnd) (map the_spec);
    1.87  
    1.88  in
     2.1 --- a/src/Pure/logic.ML	Tue Apr 26 22:59:25 2016 +0200
     2.2 +++ b/src/Pure/logic.ML	Wed Apr 27 10:03:35 2016 +0200
     2.3 @@ -28,6 +28,8 @@
     2.4    val nth_prem: int * term -> term
     2.5    val close_term: (string * term) list -> term -> term
     2.6    val close_prop: (string * term) list -> term list -> term -> term
     2.7 +  val close_prop_constraint: (string -> typ option) ->
     2.8 +    (string * string) list -> term list -> term -> term
     2.9    val true_prop: term
    2.10    val conjunction: term
    2.11    val mk_conjunction: term * term -> term
    2.12 @@ -205,10 +207,15 @@
    2.13  fun strip_horn A = (strip_imp_prems A, strip_imp_concl A);
    2.14  
    2.15  
    2.16 -(* close *)
    2.17 +(* close -- omit vacuous quantifiers *)
    2.18  
    2.19  val close_term = fold_rev Term.dependent_lambda_name;
    2.20 -fun close_prop xs As B = fold_rev dependent_all_name xs (list_implies (As, B));
    2.21 +
    2.22 +fun close_prop xs As B =
    2.23 +  fold_rev dependent_all_name xs (list_implies (As, B));
    2.24 +
    2.25 +fun close_prop_constraint default_type xs As B =
    2.26 +  fold_rev (dependent_all_constraint default_type) xs (list_implies (As, B));
    2.27  
    2.28  
    2.29  (** conjunction **)