discontinued unflat in favour of burrow and burrow_split
authorhaftmann
Wed Dec 21 13:25:20 2005 +0100 (2005-12-21)
changeset 18450e57731ba01dd
parent 18449 e314fb38307d
child 18451 5ff0244e25e8
discontinued unflat in favour of burrow and burrow_split
NEWS
src/Pure/Isar/locale.ML
src/Pure/Isar/proof.ML
src/Pure/library.ML
     1.1 --- a/NEWS	Wed Dec 21 12:06:08 2005 +0100
     1.2 +++ b/NEWS	Wed Dec 21 13:25:20 2005 +0100
     1.3 @@ -163,6 +163,20 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Pure/library:
     1.8 +
     1.9 +  val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
    1.10 +  val burrow_split: ('a list -> 'c * 'b list) -> 'a list list -> 'c * 'b list list
    1.11 +
    1.12 +The semantics of "burrow" is: "take a function with *simulatanously* transforms
    1.13 +a list of value, and apply it *simulatanously* to a list of list of values of the
    1.14 +appropriate type". Confer this with "map" which would *not* apply its argument
    1.15 +function simulatanously but in sequence. "burrow_split" allows the transformator
    1.16 +function to yield an additional side result.
    1.17 +
    1.18 +Both actually avoid the usage of "unflat" since they hide away "unflat"
    1.19 +from the user.
    1.20 +
    1.21  * Pure/library: functions map2 and fold2 with curried syntax for
    1.22  simultanous mapping and folding:
    1.23  
     2.1 --- a/src/Pure/Isar/locale.ML	Wed Dec 21 12:06:08 2005 +0100
     2.2 +++ b/src/Pure/Isar/locale.ML	Wed Dec 21 13:25:20 2005 +0100
     2.3 @@ -1201,24 +1201,21 @@
     2.4         the fixes elements in raw_elemss,
     2.5         raw_proppss contains assumptions and definitions from the
     2.6         external elements in raw_elemss. *)
     2.7 -    val raw_propps = map List.concat raw_proppss;
     2.8 -    val raw_propp = List.concat raw_propps;
     2.9 +    fun prep_prop raw_ctxt raw_concl raw_propp =
    2.10 +      let
    2.11 +        (* CB: add type information from fixed_params to context (declare_term) *)
    2.12 +        (* CB: process patterns (conclusion and external elements only) *)
    2.13 +        val (ctxt, all_propp) =
    2.14 +          prepp (fold ProofContext.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
    2.15 +        (* CB: add type information from conclusion and external elements to context *)
    2.16 +        val ctxt = fold ProofContext.declare_term (List.concat (map (map fst) all_propp)) ctxt;
    2.17 +        (* CB: resolve schematic variables (patterns) in conclusion and external elements. *)
    2.18 +        val all_propp' = map2 (curry (op ~~))
    2.19 +          (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp);
    2.20 +        val (concl, propp) = splitAt (length raw_concl, all_propp')
    2.21 +      in ((ctxt, concl), propp) end
    2.22  
    2.23 -    (* CB: add type information from fixed_params to context (declare_term) *)
    2.24 -    (* CB: process patterns (conclusion and external elements only) *)
    2.25 -    val (ctxt, all_propp) =
    2.26 -      prepp (fold ProofContext.declare_term (map Free fixed_params) raw_ctxt, raw_concl @ raw_propp);
    2.27 -    (* CB: add type information from conclusion and external elements
    2.28 -       to context *)
    2.29 -    val ctxt = fold ProofContext.declare_term (List.concat (map (map fst) all_propp)) ctxt;
    2.30 -
    2.31 -    (* CB: resolve schematic variables (patterns) in conclusion and external
    2.32 -       elements. *)
    2.33 -    val all_propp' = map2 (curry (op ~~))
    2.34 -      (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp)))) (map (map snd) all_propp);
    2.35 -    val (concl, propp) = splitAt(length raw_concl, all_propp');
    2.36 -    val propps = unflat raw_propps propp;
    2.37 -    val proppss = map (uncurry unflat) (raw_proppss ~~ propps);
    2.38 +    val ((ctxt, concl), proppss) = (burrow_split o burrow_split) (prep_prop raw_ctxt raw_concl) raw_proppss;
    2.39  
    2.40      (* CB: obtain all parameters from identifier part of raw_elemss *)
    2.41      val xs = map #1 (params_of' raw_elemss);
     3.1 --- a/src/Pure/Isar/proof.ML	Wed Dec 21 12:06:08 2005 +0100
     3.2 +++ b/src/Pure/Isar/proof.ML	Wed Dec 21 13:25:20 2005 +0100
     3.3 @@ -801,12 +801,12 @@
     3.4      val outer_state = state |> close_block;
     3.5      val outer_ctxt = context_of outer_state;
     3.6  
     3.7 -    val raw_props = List.concat stmt;
     3.8 +    val raw_props = Library.flat stmt;
     3.9      val props = ProofContext.generalize goal_ctxt outer_ctxt raw_props;
    3.10      val results =
    3.11 -      conclude_goal state raw_props goal
    3.12 -      |> Seq.map_list (ProofContext.exports goal_ctxt outer_ctxt)
    3.13 -      |> Seq.map (Library.unflat stmt);
    3.14 +      stmt
    3.15 +      |> burrow (fn raw_props => conclude_goal state raw_props goal)
    3.16 +      |> (Seq.map_list o Seq.map_list) (ProofContext.exports goal_ctxt outer_ctxt);
    3.17    in
    3.18      outer_state
    3.19      |> map_context (ProofContext.auto_bind_facts props)
     4.1 --- a/src/Pure/library.ML	Wed Dec 21 12:06:08 2005 +0100
     4.2 +++ b/src/Pure/library.ML	Wed Dec 21 13:25:20 2005 +0100
     4.3 @@ -102,7 +102,7 @@
     4.4    val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
     4.5    val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
     4.6    val burrow: ('a list -> 'b list) -> 'a list list -> 'b list list
     4.7 -  val unflat: 'a list list -> 'b list -> 'b list list
     4.8 +  val burrow_split: ('a list -> 'c * 'b list) -> 'a list list -> 'c * 'b list list
     4.9    val splitAt: int * 'a list -> 'a list * 'a list
    4.10    val dropwhile: ('a -> bool) -> 'a list -> 'a list
    4.11    val nth: 'a list -> int -> 'a
    4.12 @@ -599,6 +599,8 @@
    4.13  fun burrow f xss =
    4.14    unflat xss ((f o flat) xss);
    4.15  
    4.16 +fun burrow_split f xss =
    4.17 +  apsnd (unflat xss) ((f o flat) xss);
    4.18  
    4.19  (*like Lisp's MAPC -- seq proc [x1, ..., xn] evaluates
    4.20    (proc x1; ...; proc xn) for side effects*)