# HG changeset patch # User wenzelm # Date 939066069 -7200 # Node ID cdaf7f18856dffe4166d5a52d490e0bf3623161b # Parent 8752253211ca1e8837d2854b1200a723fbe6a7c6 renamed 'prefix' to 'prfx' (avoids clash with infix); diff -r 8752253211ca -r cdaf7f18856d 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)