# HG changeset patch
# User nipkow
# Date 954438251 -7200
# Node ID 870a58dd0ddda346973ab45e3496df10fc6a31d7
# Parent  8ba0f90f6f35bb5f6e078266c3b2ab6fda8de514
the simplification rules returned from TFL are now paired with the row they
came from.

diff -r 8ba0f90f6f35 -r 870a58dd0ddd TFL/post.sml
--- a/TFL/post.sml	Thu Mar 30 15:13:59 2000 +0200
+++ b/TFL/post.sml	Thu Mar 30 19:44:11 2000 +0200
@@ -25,12 +25,12 @@
    val define_i : theory -> xstring -> term 
                   -> simpset * thm list (*allows special simplication*)
                   -> term list
-                  -> theory * {rules:thm list, induct:thm, tcs:term list}
+                  -> theory * {rules:(thm*int)list, induct:thm, tcs:term list}
 
    val define   : theory -> xstring -> string 
                   -> simpset * thm list 
                   -> string list 
-                  -> theory * {rules:thm list, induct:thm, tcs:term list}
+                  -> theory * {rules:(thm*int)list, induct:thm, tcs:term list}
 
    val defer_i : theory -> xstring
                   -> thm list (* congruence rules *)
@@ -39,11 +39,11 @@
    val defer : theory -> xstring
                   -> thm list 
                   -> string list -> theory * thm
-
+(*
    val simplify_defn : simpset * thm list 
                         -> theory * (string * Prim.pattern list)
                         -> {rules:thm list, induct:thm, tcs:term list}
-
+*)
   end;
 
 
@@ -194,7 +194,7 @@
 			 ("Recursive definition " ^ id ^ 
 			  " would clash with the theory of the same name!")
 	val def = freezeT(get_def thy id)   RS   meta_eq_to_obj_eq
-	val {theory,rules,TCs,full_pats_TCs,patterns} = 
+	val {theory,rules,rows,TCs,full_pats_TCs} = 
 		 Prim.post_definition (Prim.congs tflCongs)
 		    (thy, (def,pats))
 	val {lhs=f,rhs} = S.dest_eq(concl def)
@@ -208,7 +208,7 @@
 	val rules' = map (standard o normalize_thm [RSmp]) (R.CONJUNCTS rules)
     in  {induct = meta_outer
 		   (normalize_thm [RSspec,RSmp] (induction RS spec')), 
-	 rules = rules', 
+	 rules = ListPair.zip(rules', rows),
 	 tcs = (termination_goals rules') @ tcs}
     end
    handle Utils.ERR {mesg,func,module} => 
diff -r 8ba0f90f6f35 -r 870a58dd0ddd TFL/tfl.sig
--- a/TFL/tfl.sig	Thu Mar 30 15:13:59 2000 +0200
+++ b/TFL/tfl.sig	Thu Mar 30 19:44:11 2000 +0200
@@ -15,8 +15,7 @@
 
    val congs : thm list -> thm list  (*fn to make congruent rules*)
 
-   datatype pattern = GIVEN of term * int
-                    | OMITTED of term * int
+   type pattern
 
    val mk_functional : theory -> term list
                        -> {functional:term,
@@ -26,10 +25,10 @@
 
    val post_definition : thm list -> theory * (thm * pattern list)
 				  -> {theory : theory,
-				     rules  : thm, 
+				     rules  : thm,
+                                      rows  : int list,
 				       TCs  : term list list,
-			     full_pats_TCs  : (term * term list) list, 
-				  patterns  : pattern list}
+			     full_pats_TCs  : (term * term list) list}
 
    val wfrec_eqns : theory -> xstring
 	             -> thm list (* congruence rules *)
diff -r 8ba0f90f6f35 -r 870a58dd0ddd TFL/tfl.sml
--- a/TFL/tfl.sml	Thu Mar 30 15:13:59 2000 +0200
+++ b/TFL/tfl.sml	Thu Mar 30 19:44:11 2000 +0200
@@ -25,12 +25,7 @@
 
 val list_mk_type = U.end_itlist (curry(op -->));
 
-fun enumerate l = 
-     rev(#1(foldl (fn ((alist,i), x) => ((x,i)::alist, i+1)) (([],0), l)));
-
-fun stringize [] = ""
-  | stringize [i] = Int.toString i
-  | stringize (h::t) = (Int.toString h^", "^stringize t);
+fun enumerate xs = ListPair.zip(xs, 0 upto (length xs - 1));
 
 fun front_last [] = raise TFL_ERR {func="front_last", mesg="empty list"}
   | front_last [x] = ([],x)
@@ -115,19 +110,25 @@
  * This datatype carries some information about the origin of a
  * clause in a function definition.
  *---------------------------------------------------------------------------*)
+(*
 datatype pattern = GIVEN   of term * int
                  | OMITTED of term * int
+*)
+(* True means the pattern was given by the user
+   (or is an instantiation of a user supplied pattern)
+*)
+type pattern = term * (int * bool)
 
-fun pattern_map f (GIVEN (tm,i)) = GIVEN(f tm, i)
-  | pattern_map f (OMITTED (tm,i)) = OMITTED(f tm, i);
+fun pattern_map f (tm,x) = (f tm, x);
 
 fun pattern_subst theta = pattern_map (subst_free theta);
-
+(*
 fun dest_pattern (GIVEN (tm,i)) = ((GIVEN,i),tm)
   | dest_pattern (OMITTED (tm,i)) = ((OMITTED,i),tm);
-
-val pat_of = #2 o dest_pattern;
-val row_of_pat = #2 o #1 o dest_pattern;
+*)
+val pat_of = fst;
+val row_of_pat = fst o snd;
+val given = snd o snd;
 
 (*---------------------------------------------------------------------------
  * Produce an instance of a constructor, plus genvars for its arguments.
@@ -170,7 +171,7 @@
              val (in_group, not_in_group) = mk_group Name rows
              val in_group' =
                  if (null in_group)  (* Constructor not given *)
-                 then [((prfx, #2(fresh c)), OMITTED (S.ARB res_ty, ~1))]
+                 then [((prfx, #2(fresh c)), (S.ARB res_ty, (~1,false)))]
                  else in_group
          in 
          part{constrs = crst, 
@@ -225,10 +226,8 @@
             in map expnd (map fresh constructors)  end
        else [row]
  fun mk{rows=[],...} = mk_case_fail"no rows"
-   | mk{path=[], rows = ((prfx, []), rhs)::_} =  (* Done *)
-        let val (tag,tm) = dest_pattern rhs
-        in ([(prfx,tag,[])], tm)
-        end
+   | mk{path=[], rows = ((prfx, []), (tm,tag))::_} =  (* Done *)
+        ([(prfx,tag,[])], tm)
    | mk{path=[], rows = _::_} = mk_case_fail"blunder"
    | mk{path as u::rstp, rows as ((prfx, []), rhs)::rst} = 
         mk{path = path, 
@@ -327,7 +326,7 @@
      val (fname,ftype) = dest_atom atom
      val dummy = map (no_repeat_vars thy) pats
      val rows = ListPair.zip (map (fn x => ([]:term list,[x])) pats,
-                              map GIVEN (enumerate R))
+                              map (fn (t,i) => (t,(i,true))) (enumerate R))
      val names = foldr add_term_names (R,[])
      val atype = type_of(hd pats)
      and aname = variant names "a"
@@ -337,7 +336,7 @@
      val range_ty = type_of (hd R)
      val (patts, case_tm) = mk_case ty_info ty_match (aname::names) range_ty 
                                     {path=[a], rows=rows}
-     val patts1 = map (fn (_,(tag,i),[pat]) => tag (pat,i)) patts 
+     val patts1 = map (fn (_,tag,[pat]) => (pat,tag)) patts 
 	  handle _ => mk_functional_err "error in pattern-match translation"
      val patts2 = U.sort(fn p1=>fn p2=> row_of_pat p1 < row_of_pat p2) patts1
      val finals = map row_of_pat patts2
@@ -345,7 +344,7 @@
      val dummy = case (originals\\finals)
              of [] => ()
           | L => mk_functional_err ("The following rows are inaccessible: " ^
-                   stringize (map (fn i => i + 1) L))
+                   commas (map Int.toString L))
  in {functional = Abs(Sign.base_name fname, ftype,
 		      abstract_over (atom, 
 				     absfree(aname,atype, case_tm))),
@@ -424,16 +423,16 @@
 end;
 
 
-fun givens [] = []
-  | givens (GIVEN(tm,_)::pats) = tm :: givens pats
-  | givens (OMITTED _::pats)   = givens pats;
+fun givens pats = map pat_of (filter given pats);
 
 (*called only by Tfl.simplify_defn*)
 fun post_definition meta_tflCongs (theory, (def, pats)) =
  let val tych = Thry.typecheck theory 
      val f = #lhs(S.dest_eq(concl def))
      val corollary = R.MATCH_MP Thms.WFREC_COROLLARY def
-     val given_pats = givens pats
+     val pats' = filter given pats
+     val given_pats = map pat_of pats'
+     val rows = map row_of_pat pats'
      val WFR = #ant(S.dest_imp(concl corollary))
      val R = #Rand(S.dest_comb WFR)
      val corollary' = R.UNDISCH corollary  (* put WF R on assums *)
@@ -450,9 +449,9 @@
  in
  {theory = theory,   (* holds def, if it's needed *)
   rules = rules1,
+  rows = rows,
   full_pats_TCs = merge (map pat_of pats) (ListPair.zip (given_pats, TCs)), 
-  TCs = TCs, 
-  patterns = pats}
+  TCs = TCs}
  end;