let rec iter(f,l) = if null l then () else (f(hd l); iter(f,tl l));
let as_present(x:'a opt) = x as present;

type path = int list;

let path_mkempty(): path = nil;
let path_get(p: path) = rev p;
let path_augment(p: path, i) = i::p;
let path_print(p: path) = listprint(p, printint, `,`);


type var = (| name: Atom'; path: path |);
let var_print(v: var) = let (|name; path|) = v in
      ( outstring `<`; PrintAtom name; outstring `,`; 
        path_print path; outstring `>`);

type vtable = var list array;

let vtable_mkempty(vsize): vtable = array(vsize,[]);

let vtable_insert(i, var, vtable: vtable) =
      update(vtable, i, var::(vtable sub i));

let vtable_print(vtable:vtable) =
      let vsize = LengthArray vtable
      enc rec vpr i = if i > vsize then vtable
                      else 
                        ( printint(i); outstring `) `;
                          listprint((vtable sub i), var_print, `,`);
                          if i = vsize then () else newline(1); vpr(i+1) )
       in vpr 1 end;

let vtable = ref (vtable_mkempty 0);
   
type rset = int list;

let rset_mkempty (): rset = nil;
let rset_init n = [n; n];
let rset_size (l:rset) = if null l then 0 else length(tl l);
let rset_get(l:rset) = if null l then [] else tl l;
let rset_isempty(set: rset) = null set;
let rset_issingleton (l:rset) = 
      if null l then false else if null(tl(tl l)) then true else false;
let rset_next(l:rset) = if null l then failwith `rset` else hd(tl(l));
let rset_isin(n, l:rset) = if null l then false
      else
      let rec isin l = if null l then false 
                       else if n = (hd l) then true
                       else if n < (hd l) then isin(tl l) else false
       in isin(tl l);
let rset_insert(n, l:rset): rset = if null l then [n;n] else (hd l)::n::(tl l);

let rset_intersect(l1:rset, l2:rset):rset = 
      if null l1 then [] else if null l2 then []
      else let (h1::t1) = l1 and (h2::t2) = l2
      enc rec inter(l1, l2, least, elements) =
            if null l1 Or null l2 
            then if null elements then nil else least::(rev elements)
            else let (h1'::t1') = l1 and (h2'::t2') = l2 in 
                if (h1':int) = h2' then inter(t1',t2',h1',h1'::elements)
                else if h1' > h2' then inter(t1',l2,least,elements)
                else inter(l1,t2',least,elements)
       in inter(t1,t2,0,[]);

let rset_count_intersect(l1:rset, l2:rset) = 
      if null l1 then 0 else if null l2 then 0
      else let (h1::t1) = l1 and (h2::t2) = l2
      enc rec inter(l1, l2, count) =
            if null l1 Or null l2 
            then count
            else let (h1'::t1') = l1 and (h2'::t2') = l2 in 
                if (h1':int) = h2' then inter(t1',t2',count+1)
                else if h1' > h2' then inter(t1',l2,count)
                else inter(l1,t2',count)
       in inter(t1,t2,0);

let rset_union(l1:rset, l2:rset):rset =
      if null l1 then l2 else if null l2 then l1 
      else let (h1::t1) = l1 and (h2::t2) = l2
      enc rec union(s1, s2, elements) =
                if null s1 Or null s2 
                then min(h1,h2)::(rev (s1@s2@elements))
                else let (h1'::t1') = s1 and (h2'::t2') = s2 in 
                  if (h1':int) = h2' then union(t1',t2',h1'::elements)
                  else if h1' > h2' then union(t1',l2,h1'::elements)
                  else union(l1,t2',h2'::elements)
         in union(t1,t2,[]);

let rset_equal(set1: rset, set2) = (set1 = set2);

let rset_least(l: rset) = if null l then ~1 else hd l;

let rset_least_singlet(l: rset) = if null l then []:rset else [hd(l);hd(l)];

let rec rset_least_p(l: rset, p) = 
      if null l then ~1 
      else if p(hd l) then hd l else rset_least_p(tl l,p);

let rec rules_least_p(l: int list, p) = 
      if null l then ~1 
      else let h::t = l
           enc result = rules_least_p(t,p)
       in if result >= 0 then result else if p(h) then h else ~1;

let rminus(set1: rset, set2: rset) = 
      if null set2 then set1 else if null set1 then [] 
      else let h1::t1 = set1 and h2::t2 = set2
           enc rec rmin(l1,l2,elements) =
                 if null l2 
                 then if null elements And null l1 then []
                      else if null l1 then (hd elements)::(rev elements)
                      else if null elements then h1::l1
                      else h1::((rev elements) @ l1)
                 else let h1::t1 = l1 and (h2::t2) = l2
                   in if h1 = h2 then rmin(t1,t2,elements)
                      else rmin(t1,l2,h1::elements)
       in rmin(t1,t2,[]);


%RJG 09-Feb-89 changes for new constructor type xcon%
type pconstr = 
     [| Constructor: [|variant;pointer;zero;ref;xcon:int ref|] # int # int # bool;
        Variant: int # int;
        Constant: SynConst'; DefConstants |];

let rec type 
     info <=> [| case_node: (| full: bool ref;
                               alts: node list ref;
                               defalts: node list ref |);
                 cons_node: (| constr: pconstr; arg: node opt |);
                 tuple_node:(| sons: node list |);
                 leaf
              |]

 and node <=> (| info: info ref;
                 rules: rset ref;
                 defaults: rset ref;
                 path: path |)
;

let case_node x = absinfo [|case_node=x|];
let repcase_node x = repinfo x as case_node;
let cons_node x = absinfo [|cons_node=x|];
let repcons_node x = repinfo x as cons_node;
let tuple_node x = absinfo [|tuple_node=x|];
let reptuple_node x = repinfo x as tuple_node;
let leaf = absinfo [|leaf|];
let node = absnode;

let rec lookup(l, found) =
      if null l then failwith `lookup_alt`
      else let constr = repcons_node(!(repnode(hd l).info)).constr
        in if found(constr) then hd l else lookup(tl l,found);

let lookup_alt(pcon, l) =
      varcase pcon of
      [|Constructor=(_,n,_,_). lookup(l, (\[|Constructor=(_,n',_,_)|]. n=n'));
        Variant=(n,_). lookup(l, (\[|Variant=(n',_)|]. n=n'));
        Constant = sc. 
          varcase sc of
          [|int=i. lookup(l, (\[|Constant=[|int=i'|]|]. i=i'));
            real=r. lookup(l, (\[|Constant=[|real=r'|]|]. r=r'));
            string=s. lookup(l, (\[|Constant=[|string=s'|]|]. s=s'))
          |];
        DefConstants. lookup(l, (\x. x is DefConstants))
      |];

let rec pconstr_of(pattern):pconstr =
      varcase repSynBind' pattern of
      [| SynBindIde=x.
           varcase !x.PreBinder of
           [| absent. failwith `pconstr_of`;
              present = x. [|Constructor= !(x.Constructor as yes)|]
           |];
         SynBindAppl=x.
           [|Constructor= !(((!(x.Binder)).Constructor) as yes)|];
         SynBindConst=x. [|Constant=x|];
         SynBindVariant=(|VarKey;VarField;VarPos|). 
           [|Variant=(!VarPos)(VarKey)|];
         SynBindForce=x. pconstr_of(x.ForceBind);
         SynBindRecord. failwith `pconstr_of`; 
         SynBindAny. failwith `pconstr_of`;
         SynBindBoth. failwith `pconstr_of`;
         SynBindTuple. failwith `pconstr_of`
      |];

let rec var_of(pattern): SynBindIde' opt =
      let rp = repSynBind' pattern in
       if rp is SynBindIde
       then if (!((rp as SynBindIde).PreBinder)) is absent
            then [|present=(rp as SynBindIde).Binder|] else [|absent|]
       else if rp is SynBindForce then var_of((rp as SynBindForce).ForceBind)
       else [|absent|];


let rec new_tree (bind: SynBind', rule, path) = 
      varcase var_of bind of
      [|absent.
          node (| info=ref (init_info(bind,rule,path)); path=path;
                  rules=ref (rset_init rule); defaults=ref (rset_mkempty()) |);
        present=v.
          node (| info=ref (init_info(bind,rule,path)); path=path;
                  rules=ref (rset_mkempty()); defaults=ref (rset_init rule) |)
      |]
and
    init_info(bind:SynBind', rule, path):info =
      varcase repSynBind' bind of
      [| SynBindIde = bi.
           varcase !bi.PreBinder of
           [| absent.
              ( vtable_insert(rule,(|name=bi.Ide; path=path|),!vtable);
                leaf );
              present = x. let x = x.Constructor as yes in
                case_node 
                  (| full=ref false; defalts=ref [];
                     alts=ref [node (| info=ref(cons_node
                                                  (|constr=[|Constructor= !x|];
                                                    arg=[|absent|]|));
                                       rules=ref (rset_init rule);
                                       defaults=ref (rset_mkempty());
                                       path=path |) ] |)
           |];
         SynBindAny. leaf;
         SynBindBoth = (id,y).
           ( vtable_insert(rule,(|name=(repSynBind'(id) as SynBindIde).Ide; 
                                  path=path|),!vtable);
             init_info(y, rule, path) );
         SynBindTuple = components.
           let rec mksons(l, i, sons) = 
              if null l then tuple_node (|sons=rev sons|)
              else let h::t = l in 
                mksons(t,i+1,new_tree(h,rule,path_augment(path,i))::sons)
            in mksons(components,1,[]);
         SynBindConst = c.
            case_node 
              (| full=ref false; defalts=ref [];
                 alts=ref [node (| info=ref(cons_node
                                              (|constr=[|Constant=c|];
                                                arg=[|absent|]|));
                                   rules=ref (rset_init rule);
                                   defaults=ref (rset_mkempty());
                                   path=path |) ] |);

         SynBindAppl = (|Ide; Binder; Arg; HowRead |).
            case_node 
              (| full=ref false; defalts=ref [];
                 alts=ref [node (| info=ref ( cons_node
                                        (|constr=[|Constructor=
                                                     !((!Binder).Constructor 
                                                       as yes) |];
                                          arg=[|present=
                                                (new_tree(Arg,rule,path))|]
                                        |) );
                                   rules=ref (rset_init rule);
                                   defaults=ref (rset_mkempty());
                                   path=path |) ] |);

         SynBindRecord = (x,y).
           let x': SynBindRecord' list =
              case y of [|solid. x; flexi=f. (!f)() |]
           enc rec mksons(l, i, sons) = 
              if null l then tuple_node (|sons=rev sons|)
              else let (|RecKey; RecField|)::t = l in 
                mksons(t,i+1,new_tree(RecField,rule,
                                      path_augment(path,i))::sons)
            in mksons(x',1,[]);

         SynBindVariant = (| VarKey; VarField; VarPos |).
            let (i,m) = (!VarPos)(VarKey) in
            case_node 
              (| full=ref false; defalts=ref [];
                 alts=ref [node (| info=ref ( cons_node
                                        (|constr=[|Variant= (i,m)|];
                                          arg=[|present=
                                           (new_tree(VarField,rule,path))|]
                                        |) );
                                   rules=ref (rset_init rule);
                                   defaults=ref (rset_mkempty());
                                   path=path |) ] |);

         SynBindForce = (|ForceBind; ForceType|) .
            init_info(ForceBind,rule,path)
      |];

let rec merge_pattern (pattern, rule, path, nd) = 
      let (| info; rules; defaults; path=path' |) = repnode nd in
      if repSynBind' pattern is SynBindAny
      then defaults := rset_insert(rule, !defaults)
      else if repSynBind' pattern is SynBindIde
         then let bi = (repSynBind' pattern as SynBindIde) in
              varcase !bi.PreBinder of
              [|absent.
                   ( defaults := rset_insert(rule, !defaults);
                     vtable_insert(rule,(|name=bi.Binder.Ide; 
                                          path=path|),!vtable) );
                present = _.
                   ( rules := rset_insert(rule, !rules);
                     update_info(pattern,rule,path,nd) )
              |]
      else if repSynBind' pattern is SynBindBoth
         then let (ide,patt) = (repSynBind' pattern as SynBindBoth)
              enc bi = (repSynBind' ide as SynBindIde).Binder in
              ( vtable_insert(rule,(|name=bi.Ide; path=path|),!vtable);
                merge_pattern (patt, rule, path, nd) )
      else if repSynBind' pattern is SynBindForce
         then merge_pattern ((repSynBind' pattern as SynBindForce).ForceBind, 
                             rule, path, nd)
      else 
        ( rules := rset_insert(rule, !rules);
          update_info(pattern,rule,path,nd) )
         
and
    update_info(pattern, rule, path, nd) =
      varcase repinfo(!((repnode nd).info)) of
      [|leaf. (repnode nd).info := init_info(pattern,rule,path);
        case_node = cn. 
          let constr = pconstr_of pattern
          enc alts = cn.alts enc al = !alts
           in (let nd' = lookup_alt(constr, al)
               enc rules = (repnode nd').rules enc info = (repnode nd').info
               enc carg = repcons_node(!info).arg
                in ( rules := rset_insert(rule, !rules);
                     let patt = repSynBind' pattern in
                     if patt is SynBindAppl
                     then merge_pattern((patt as SynBindAppl).Arg,
                                        rule,path,as_present carg)
                     else if patt is SynBindVariant
                     then merge_pattern((patt as SynBindVariant).VarField,
                                        rule,path,as_present carg)
                     else () )
              ) 
              ?? [`lookup_alt`]
                alts := node (|info= 
                                 ref (cons_node 
                                        (|constr= constr;
                                          arg= 
                                            let patt = repSynBind' pattern in
                                            if patt is SynBindAppl
                                            then [|present=(new_tree(
                                                   (patt as SynBindAppl).Arg,
                                                   rule,path))|]
                                            else if patt is SynBindVariant
                                            then [|present=(new_tree(
                                                   (patt as SynBindVariant).
                                                                   VarField,
                                                   rule,path))|]
                                            else [|absent|] |) );
                               rules=ref (rset_init rule);
                               defaults=ref (rset_mkempty()); path=path |)
                        :: al;

        cons_node = cn. failwith `Should never occur`;

        tuple_node = (| sons |).
          let components = 
              if repSynBind' pattern is SynBindTuple
              then repSynBind' pattern as SynBindTuple
              else let (x,y) = repSynBind' pattern as SynBindRecord
                   enc x' = case y of [|solid. x; flexi=f. (!f)() |]
                    in map (\(|RecKey; RecField|). RecField) x'
          enc rec mergesons(lc, ls, i) = 
              if null lc And null ls then ()
              else let (hc::tc) = lc and (hs::ts) = ls in
                ( merge_pattern(hc,rule,path_augment(path,i),hs);
                  mergesons(tc,ts,i+1) )
           in mergesons(components,sons,1)
      |];



let fill_case(nd) =
      let (| info; rules; defaults; path |) = repnode nd
      enc cn = repcase_node(!info)
      enc (|full; alts; defalts|) = cn
      enc constr = (repcons_node(!((repnode(hd (!alts))).info))).constr
       in if constr is Constant
          then (lookup_alt([|DefConstants|], !defalts); ())
               ?? [`lookup_alt`]
                 defalts := (node (|info=ref(cons_node
                                               (|constr=[|DefConstants|];
                                                 arg=[|absent|]|));
                                    rules=ref(!defaults);
                                    defaults=ref(!defaults);path|))
                            ::(!defalts) 

          else let rec proc_alts(n,max,genfn) =
                 if n = max then ()
                 else let pc = genfn n in
                  (lookup_alt(pc, !alts); proc_alts(n+1,max,genfn))
                  ?? [`lookup_alt`]
                    (defalts := (node (|info=ref(cons_node(|constr=pc;
                                                            arg=[|absent|]|));
                                        rules=ref(!defaults);
                                        defaults=ref(!defaults);path|))
                                ::(!defalts); proc_alts(n+1,max,genfn))
                in varcase constr of
                   [|Constructor=(rep,n,max,impappl).
                       proc_alts(0,max,
                                 (\n.[|Constructor=(rep,n,max,impappl)|]));
                     Variant=(n,max).
                       proc_alts(0,max,(\n.[|Variant=(n,max)|]));
                     Constant=_. (); DefConstants. ()
                   |];


fun propagate_defaults(nd, defs) =
      let (|info; rules; defaults; path|) = repnode nd in
      ( defaults := rset_union(!defaults, defs);
        rules := rset_union(!rules,!defaults);
        varcase repinfo(!info) of
        [|case_node = (|full; alts; defalts|).
            ( let info = !(repnode(hd(!alts)).info)
              enc constr = (repcons_node info).constr
               in varcase constr of
                  [|Constructor=(rep,n,max,impappl).
                      if length(!alts) = max
                      then full := true else fill_case nd;
                    Variant=(n,max).
                      if length(!alts) = max
                      then full := true else fill_case nd;
                    Constant=_. fill_case nd;
                    DefConstants. () |];
              iter((\ son_node. propagate_defaults(son_node, !defaults)),
                   !alts) );
          cons_node = (| constr; arg |) .
            ( varcase arg of 
              [|absent . ();
                present = a. propagate_defaults(a, !defaults) |] );
          tuple_node = (| sons |) .
            iter((\ son_node . propagate_defaults(son_node, !defaults)),
                 sons);
          leaf . ()
        |]
      );
         
let rec indent n = if n = 0 then () else (outstring ` `; indent(n-1));
                
let rec
    print_andor (nd, level) =
      let (|info; rules; defaults; path|) = repnode nd in
      ( outtok `node {`; print_info(!info,level+6);
        newline(1); indent(level+6); print_rules(!rules, level+6);
        newline(1); indent(level+6); print_defaults(!defaults,level+6);
        newline(1); indent(level+6); print_path(path,level+6);
        newline(1); indent(level+5); outtok `}`
      )
and print_info(info, level) =
      varcase repinfo info of
      [|case_node = (|full; alts; defalts|).
          ( outtok `case {`; outtok `full=`; printbool(!full);
            newline(1); indent(level+6); 
            outtok `alts=[`; print_nodelist(!alts, level+12); outtok `]`;
            newline(1); indent(level+6); 
            outtok `defalts=[`; print_nodelist(!defalts, level+15); outtok `]`;
            newline(1); indent(level+5); outtok `}`
          );
        cons_node = (|constr; arg|).
          ( outtok `cons {`; print_pconstr(constr, level+6);
            varcase arg of
            [|absent. ();
              present = a. 
                ( newline(1); indent(level+6); print_andor(a, level+6) ) |];
            outtok `}`
          );
        tuple_node = (|sons|). 
          ( outtok `tuple [`; print_nodelist(sons,level+7);
            newline(1); indent(level+6); outtok `]`
          );
        leaf. outtok `leaf`
      |]
and print_rules(r, level) =
      ( outtok `rules = (`; 
        if null r then () else listprint(tl(r):int list, printint, `,`); 
        outtok `)` )
and print_defaults(r, level) =
      ( outtok `defaults = (`; 
        if null r then () else listprint(tl(r):int list, printint, `,`); 
        outtok `)`)
and print_path(r, level) =
      ( outtok `path = (`; path_print r; outtok `)` )
and print_nodelist(l, level) = 
      if null l then () 
      else let (h::t) = l in
        ( print_andor(h,level); 
          if null t then ()
          else ( newline(1); indent(level); print_nodelist(t,level) )
        )
and print_pconstr( p: pconstr, level ) = 
      varcase p of
      [|Constructor=(rep,n,max,impappl).
          (outtok `con(`; printint n; outtok(`,`); printint max; outtok `)`);
        Variant=(n,max).
          (outtok `var(`; printint n; outtok(`,`); printint max; outtok `)`);
        Constant=sc.
          varcase sc of [|int=i. printint i;
                          real=r. printreal r; string=s. outtok s|];
        DefConstants. outtok `*`
      |];

let mktree l = 
      if null l then failwith `mktree`
      else let pattern::t = l in
      ( vtable := vtable_mkempty(length l);
        let aotree = new_tree(pattern,1,path_mkempty())
        enc redundant = array(length l, true)
        enc exhaustive = ref true
        enc rec process_pattlist(l,i) = 
                if null l then ()
                else let pattern::t = l in
                  ( merge_pattern(pattern,i,path_mkempty(),aotree);
                    process_pattlist(t,i+1) )
        enc _ = process_pattlist(t,2)
        enc _ = propagate_defaults(aotree, rset_mkempty())
        enc _ = print_andor(aotree,0)
%            val dtree = mkdispatch(aotree, (redundant, exhaustive))
            val _ = if !exhaustive then ""
                    else print "\nWarning --- Match not exhaustive\n"
            fun collect_red_pats(n,mx,rs) = 
                  if n = mx then rs 
                  else if redundant sub n 
                  then collect_red_pats(n+1,mx,rset_insert(n+1,rs))
                  else collect_red_pats(n+1,mx,rs)
            val red_pats = collect_red_pats(0,length l,rset_mkempty())
            val _ = if rset_isempty(red_pats) then ""
                    else (print "\nWarning --- The following rules are ";
                          print "redundant: ";
                          print_rules(red_pats, 0); print "\n")
         in (aotree, dtree) end );
%
         in ()
      );       
 



                



















