TFL/tfl.sml

--- a/TFL/tfl.sml	Mon Oct 04 21:39:36 1999 +0200
+++ b/TFL/tfl.sml	Mon Oct 04 21:41:09 1999 +0200
@@ -11,6 +11,8 @@
 
 val trace = ref false;
 
+open BasisLibrary; (*restore original structures*)
+
 (* Abbreviations *)
 structure R = Rules;
 structure S = USyntax;
@@ -146,11 +148,11 @@
  * pattern with constructor = Name.
  *---------------------------------------------------------------------------*)
 fun mk_group Name rows =
-  U.itlist (fn (row as ((prefix, p::rst), rhs)) =>
+  U.itlist (fn (row as ((prfx, p::rst), rhs)) =>
             fn (in_group,not_in_group) =>
                let val (pc,args) = S.strip_comb p
                in if ((#1(dest_Const pc) = Name) handle _ => false)
-                  then (((prefix,args@rst), rhs)::in_group, not_in_group)
+                  then (((prfx,args@rst), rhs)::in_group, not_in_group)
                   else (in_group, row::not_in_group) end)
       rows ([],[]);
 
@@ -159,7 +161,7 @@
  *---------------------------------------------------------------------------*)
 fun partition _ _ (_,_,_,[]) = raise TFL_ERR{func="partition", mesg="no rows"}
   | partition gv ty_match
-              (constructors, colty, res_ty, rows as (((prefix,_),_)::_)) =
+              (constructors, colty, res_ty, rows as (((prfx,_),_)::_)) =
 let val fresh = fresh_constr ty_match colty gv
      fun part {constrs = [],      rows, A} = rev A
        | part {constrs = c::crst, rows, A} =
@@ -168,7 +170,7 @@
              val (in_group, not_in_group) = mk_group Name rows
              val in_group' =
                  if (null in_group)  (* Constructor not given *)
-                 then [((prefix, #2(fresh c)), OMITTED (S.ARB res_ty, ~1))]
+                 then [((prfx, #2(fresh c)), OMITTED (S.ARB res_ty, ~1))]
                  else in_group
          in 
          part{constrs = crst, 
@@ -186,16 +188,16 @@
 
 fun mk_pat (c,l) =
   let val L = length (binder_types (type_of c))
-      fun build (prefix,tag,plist) =
+      fun build (prfx,tag,plist) =
           let val args   = take (L,plist)
               and plist' = drop(L,plist)
-          in (prefix,tag,list_comb(c,args)::plist') end
+          in (prfx,tag,list_comb(c,args)::plist') end
   in map build l end;
 
-fun v_to_prefix (prefix, v::pats) = (v::prefix,pats)
-  | v_to_prefix _ = raise TFL_ERR{func="mk_case", mesg="v_to_prefix"};
+fun v_to_prfx (prfx, v::pats) = (v::prfx,pats)
+  | v_to_prfx _ = raise TFL_ERR{func="mk_case", mesg="v_to_prfx"};
 
-fun v_to_pats (v::prefix,tag, pats) = (prefix, tag, v::pats)
+fun v_to_pats (v::prfx,tag, pats) = (prfx, tag, v::pats)
   | v_to_pats _ = raise TFL_ERR{func="mk_case", mesg="v_to_pats"};
  
 
@@ -213,24 +215,24 @@
  val fresh_var = gvvariant usednames 
  val divide = partition fresh_var ty_match
  fun expand constructors ty ((_,[]), _) = mk_case_fail"expand_var_row"
-   | expand constructors ty (row as ((prefix, p::rst), rhs)) = 
+   | expand constructors ty (row as ((prfx, p::rst), rhs)) = 
        if (is_Free p) 
        then let val fresh = fresh_constr ty_match ty fresh_var
                 fun expnd (c,gvs) = 
                   let val capp = list_comb(c,gvs)
-                  in ((prefix, capp::rst), pattern_subst[(p,capp)] rhs)
+                  in ((prfx, capp::rst), pattern_subst[(p,capp)] rhs)
                   end
             in map expnd (map fresh constructors)  end
        else [row]
  fun mk{rows=[],...} = mk_case_fail"no rows"
-   | mk{path=[], rows = ((prefix, []), rhs)::_} =  (* Done *)
+   | mk{path=[], rows = ((prfx, []), rhs)::_} =  (* Done *)
         let val (tag,tm) = dest_pattern rhs
-        in ([(prefix,tag,[])], tm)
+        in ([(prfx,tag,[])], tm)
         end
    | mk{path=[], rows = _::_} = mk_case_fail"blunder"
-   | mk{path as u::rstp, rows as ((prefix, []), rhs)::rst} = 
+   | mk{path as u::rstp, rows as ((prfx, []), rhs)::rst} = 
         mk{path = path, 
-           rows = ((prefix, [fresh_var(type_of u)]), rhs)::rst}
+           rows = ((prfx, [fresh_var(type_of u)]), rhs)::rst}
    | mk{path = u::rstp, rows as ((_, p::_), _)::_} =
      let val (pat_rectangle,rights) = ListPair.unzip rows
          val col0 = map(hd o #2) pat_rectangle
@@ -238,7 +240,7 @@
      if (forall is_Free col0) 
      then let val rights' = map (fn(v,e) => pattern_subst[(v,u)] e)
                                 (ListPair.zip (col0, rights))
-              val pat_rectangle' = map v_to_prefix pat_rectangle
+              val pat_rectangle' = map v_to_prfx pat_rectangle
               val (pref_patl,tm) = mk{path = rstp,
                                       rows = ListPair.zip (pat_rectangle',
                                                            rights')}
@@ -250,7 +252,7 @@
      case (ty_info ty_name)
      of None => mk_case_fail("Not a known datatype: "^ty_name)
       | Some{case_const,constructors} =>
-        let open BasisLibrary (*restore original List*)
+        let
 	    val case_const_name = #1(dest_Const case_const)
             val nrows = List.concat (map (expand constructors pty) rows)
             val subproblems = divide(constructors, pty, range_ty, nrows)