renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
authorwenzelm
Tue Mar 17 14:09:20 2009 +0100 (2009-03-17)
changeset 305582ef9892114fd
parent 30557 a28d83e903ce
child 30559 e5987a7ac5df
renamed Tactic.taglist/untaglist/orderlist to tag_list/untag_list/order_list (in library.ML);
src/Provers/blast.ML
src/Provers/classical.ML
src/Pure/library.ML
src/Pure/tactic.ML
     1.1 --- a/src/Provers/blast.ML	Tue Mar 17 13:33:21 2009 +0100
     1.2 +++ b/src/Provers/blast.ML	Tue Mar 17 14:09:20 2009 +0100
     1.3 @@ -564,11 +564,11 @@
     1.4        (Const ("*Goal*", _) $ G) =>
     1.5          let val pG = mk_Trueprop (toTerm 2 G)
     1.6              val intrs = maps (fn (inet,_) => Net.unify_term inet pG) nps
     1.7 -        in  map (fromIntrRule thy vars o #2) (Tactic.orderlist intrs)  end
     1.8 +        in  map (fromIntrRule thy vars o #2) (order_list intrs)  end
     1.9      | _ =>
    1.10          let val pP = mk_Trueprop (toTerm 3 P)
    1.11              val elims = maps (fn (_,enet) => Net.unify_term enet pP) nps
    1.12 -        in  map_filter (fromRule thy vars o #2) (Tactic.orderlist elims)  end;
    1.13 +        in  map_filter (fromRule thy vars o #2) (order_list elims)  end;
    1.14  
    1.15  
    1.16  (*Normalize a branch--for tracing*)
     2.1 --- a/src/Provers/classical.ML	Tue Mar 17 13:33:21 2009 +0100
     2.2 +++ b/src/Provers/classical.ML	Tue Mar 17 14:09:20 2009 +0100
     2.3 @@ -688,7 +688,7 @@
     2.4  (*version of bimatch_from_nets_tac that only applies rules that
     2.5    create precisely n subgoals.*)
     2.6  fun n_bimatch_from_nets_tac n =
     2.7 -    biresolution_from_nets_tac (Tactic.orderlist o List.filter (nsubgoalsP n)) true;
     2.8 +    biresolution_from_nets_tac (order_list o List.filter (nsubgoalsP n)) true;
     2.9  
    2.10  fun eq_contr_tac i = ematch_tac [not_elim] i  THEN  eq_assume_tac i;
    2.11  val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac;
     3.1 --- a/src/Pure/library.ML	Tue Mar 17 13:33:21 2009 +0100
     3.2 +++ b/src/Pure/library.ML	Tue Mar 17 14:09:20 2009 +0100
     3.3 @@ -211,6 +211,9 @@
     3.4    val sort_distinct: ('a * 'a -> order) -> 'a list -> 'a list
     3.5    val sort_strings: string list -> string list
     3.6    val sort_wrt: ('a -> string) -> 'a list -> 'a list
     3.7 +  val tag_list: int -> 'a list -> (int * 'a) list
     3.8 +  val untag_list: (int * 'a) list -> 'a list
     3.9 +  val order_list: (int * 'a) list -> 'a list
    3.10  
    3.11    (*random numbers*)
    3.12    exception RANDOM
    3.13 @@ -1015,6 +1018,23 @@
    3.14  fun sort_wrt sel xs = sort (string_ord o pairself sel) xs;
    3.15  
    3.16  
    3.17 +(* items tagged by integer index *)
    3.18 +
    3.19 +(*insert tags*)
    3.20 +fun tag_list k [] = []
    3.21 +  | tag_list k (x :: xs) = (k, x) :: tag_list (k + 1) xs;
    3.22 +
    3.23 +(*remove tags and suppress duplicates -- list is assumed sorted!*)
    3.24 +fun untag_list [] = []
    3.25 +  | untag_list [(k: int, x)] = [x]
    3.26 +  | untag_list ((k, x) :: (rest as (k', x') :: _)) =
    3.27 +      if k = k' then untag_list rest
    3.28 +      else x :: untag_list rest;
    3.29 +
    3.30 +(*return list elements in original order*)
    3.31 +fun order_list list = untag_list (sort (int_ord o pairself fst) list);
    3.32 +
    3.33 +
    3.34  
    3.35  (** random numbers **)
    3.36  
     4.1 --- a/src/Pure/tactic.ML	Tue Mar 17 13:33:21 2009 +0100
     4.2 +++ b/src/Pure/tactic.ML	Tue Mar 17 14:09:20 2009 +0100
     4.3 @@ -66,8 +66,6 @@
     4.4    val innermost_params: int -> thm -> (string * typ) list
     4.5    val term_lift_inst_rule:
     4.6      thm * int * ((indexname * sort) * typ) list * ((indexname * typ) * term) list * thm -> thm
     4.7 -  val untaglist: (int * 'a) list -> 'a list
     4.8 -  val orderlist: (int * 'a) list -> 'a list
     4.9    val insert_tagged_brl: 'a * (bool * thm) ->
    4.10      ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net ->
    4.11        ('a * (bool * thm)) Net.net * ('a * (bool * thm)) Net.net
    4.12 @@ -264,20 +262,6 @@
    4.13  
    4.14  (** To preserve the order of the rules, tag them with increasing integers **)
    4.15  
    4.16 -(*insert tags*)
    4.17 -fun taglist k [] = []
    4.18 -  | taglist k (x::xs) = (k,x) :: taglist (k+1) xs;
    4.19 -
    4.20 -(*remove tags and suppress duplicates -- list is assumed sorted!*)
    4.21 -fun untaglist [] = []
    4.22 -  | untaglist [(k:int,x)] = [x]
    4.23 -  | untaglist ((k,x) :: (rest as (k',x')::_)) =
    4.24 -      if k=k' then untaglist rest
    4.25 -      else    x :: untaglist rest;
    4.26 -
    4.27 -(*return list elements in original order*)
    4.28 -fun orderlist kbrls = untaglist (sort (int_ord o pairself fst) kbrls);
    4.29 -
    4.30  (*insert one tagged brl into the pair of nets*)
    4.31  fun insert_tagged_brl (kbrl as (k, (eres, th))) (inet, enet) =
    4.32    if eres then
    4.33 @@ -288,7 +272,7 @@
    4.34  
    4.35  (*build a pair of nets for biresolution*)
    4.36  fun build_netpair netpair brls =
    4.37 -    fold_rev insert_tagged_brl (taglist 1 brls) netpair;
    4.38 +    fold_rev insert_tagged_brl (tag_list 1 brls) netpair;
    4.39  
    4.40  (*delete one kbrl from the pair of nets*)
    4.41  fun eq_kbrl ((_, (_, th)), (_, (_, th'))) = Thm.eq_thm_prop (th, th')
    4.42 @@ -314,8 +298,8 @@
    4.43        in PRIMSEQ (biresolution match (order kbrls) i) end);
    4.44  
    4.45  (*versions taking pre-built nets.  No filtering of brls*)
    4.46 -val biresolve_from_nets_tac = biresolution_from_nets_tac orderlist false;
    4.47 -val bimatch_from_nets_tac   = biresolution_from_nets_tac orderlist true;
    4.48 +val biresolve_from_nets_tac = biresolution_from_nets_tac order_list false;
    4.49 +val bimatch_from_nets_tac   = biresolution_from_nets_tac order_list true;
    4.50  
    4.51  (*fast versions using nets internally*)
    4.52  val net_biresolve_tac =
    4.53 @@ -332,7 +316,7 @@
    4.54  
    4.55  (*build a net of rules for resolution*)
    4.56  fun build_net rls =
    4.57 -  fold_rev insert_krl (taglist 1 rls) Net.empty;
    4.58 +  fold_rev insert_krl (tag_list 1 rls) Net.empty;
    4.59  
    4.60  (*resolution using a net rather than rules; pred supports filt_resolve_tac*)
    4.61  fun filt_resolution_from_net_tac match pred net =
    4.62 @@ -342,7 +326,7 @@
    4.63        in
    4.64           if pred krls
    4.65           then PRIMSEQ
    4.66 -                (biresolution match (map (pair false) (orderlist krls)) i)
    4.67 +                (biresolution match (map (pair false) (order_list krls)) i)
    4.68           else no_tac
    4.69        end);
    4.70