let rec map2(f: ('a # 'b) -> 'c, l: 'a list, m: 'b list): 'c list =
  if null(l) then if null(m) then [] else failwith `map2`
  else if null(m) then failwith `map2`
  else f(hd l,hd m) :: map2(f,tl l,tl m);

let rec appendlist(l: 'a list list): 'a list =
  if null(l) then [] else append(hd l, appendlist(tl l));

let rec type tile <=> [| all; tuple: tile list; variant: int # tile;
                         constant: [|int: int; real: real;
                                     string: string|] list |];
let alltile = abstile[|all|];

let trimcount = ref 0
and exhausted = `exhasted`
ins

%AM: type checking should have stopped the failures from occurring%
   tupleise(t: tile, size: int): tile list =
  case reptile t of
  [| all. let rec f(n) = if n=0 then [] else alltile::f(n-1)
          in f(size);
     tuple=l. if length(l)=size then l else failwith `exhaustion`;
     variant=(n,t'). failwith `exhaustion`;
     constant=_. failwith `exhaustion`
  |]

and variantise(t: tile, maxcase: int): (int # tile) list =
  case reptile t of
  [| all.  %RJG HACK - all exte. datatypes call with maxcase = MaxInt %
	   %so return a pair which won't be matched%
     	let rec f(i) = if i=0 then [] else (i-1,alltile)::f(i-1)
          in if maxcase=MaxInt then [(MaxInt-1,alltile)] else f(maxcase);
     tuple=l. failwith `exhaustion`;
     variant=(n,t'). if n<maxcase then [(n,t')] else failwith `exhaustion`;
     constant=_. failwith `exhaustion`
  |]

and constantise(t: tile, thing: SynConst'): tile =
  case reptile t of
  [| all. abstile[|constant=[thing]|];
     tuple=l. failwith `exhaustion`;
     variant=(n,t'). failwith `exhaustion`;
     constant=x. abstile[|constant=thing::x|]
  |]

and rec tileprod(a: tile list, b: tile list list): tile list list =
  if null(a) then if null(b) then [] else failwith `tileproduct`
  else if null(b) then failwith `tileproduct`
  else let ha::ta = a and hb::tb = b in
       let rest = tileprod(ta,tb) in
       append(map (\q.q::ta) hb,
              map (\q.ha::q) rest)

ins rec trimtile(b: SynBind', c: tile): tile list =
  let _ = trimcount := (!trimcount) - 1
  in
  if (!trimcount) <=0 then failwith exhausted
  else
  case repSynBind' b of
  [| SynBindIde=(|Ide; Binder; PreBinder|). case !PreBinder of
       [| absent.[];
          present=b.
         let (_,n,max,_) = !(b.Constructor as yes)
         enc c' = variantise(c, max)
         enc f(i,t) = let g(t') = abstile[|variant=(i,t')|] in
                      if i=n then map g (trimtile(
                                        absSynBind'[|SynBindTuple=[]|],t))
                      else [g(t)]
         in appendlist(map f c')
      |];
     SynBindAny.   [];
     SynBindConst=k. [constantise(c,k)];
     SynBindBoth=(x,y).  trimtile(y,c);    %AM: ML restriction on x used%
     SynBindTuple=x.
         %AM: let Bi be a subset of Ai (i=1,2). We calculate
              A1#A2-B1#B2 as the union of A1#(A2-B2) and (A1-B1)#A2. %
         let c' = tupleise(c,length(x))
         enc coverlist = map2(trimtile, x, c')
         in map (\q.abstile[|tuple=q|]) (tileprod(c',coverlist));
     SynBindRecord=(x,y).
         let x = case y of
                 [|solid. x;
                   flexi=f. let x' = (!f)() in
                            (f := \().x'; x')
                 |]
         enc c' = tupleise(c,length(x))
         enc coverlist = map2((\(e,c'').trimtile(e.RecField,c'')), x, c')
         in map (\q.abstile[|tuple=q|]) (tileprod(c',coverlist));
     SynBindAppl=x.
         let (_,n,max,_) = !((!x.Binder).Constructor as yes)
         enc c' = variantise(c, max)
         enc f(i,t) = let g(t') = abstile[|variant=(i,t')|] in
                      if i=n then map g (trimtile(x.Arg,t)) else [g(t)]
         in appendlist(map f c');
     SynBindVariant=x.
         let (n,max) = (!x.VarPos)(x.VarKey)
         enc c' = variantise(c, max)
         enc f(i,t) = let g(t') = abstile[|variant=(i,t')|] in
                      if i=n then map g (trimtile(x.VarField,t)) else [g(t)]
         in appendlist(map f c');
     SynBindForce=x. trimtile(x.ForceBind,c)
  |]

ins rec check(l: SynRule' list, left: tile list): tile list =
   if null(l) then left
   else let (bind,body)::rest = l
        in check(rest, appendlist(map (\t.trimtile(bind,t)) left))

ins CheckMatch(l: SynMatch'): bool =
  let _ = trimcount := (!Debug.CheckMatchLimit)
  in
  (if null(check(l,[alltile])) then true
  else (outstring(`***Warning:  Patterns in Match not exhaustive:  `);
        SynMatchPrint(l,5);  PrintLn();
        false))
  ?? [exhausted]
     (outstring(`***Warning: limit on Match checking exceeded`); PrintLn();
      outstring(`Patterns in match may not be exhaustive: `);
      SynMatchPrint(l,5);  PrintLn();
        false);
