adamc@16: (* Copyright (c) 2008, Adam Chlipala
adamc@16:  * All rights reserved.
adamc@16:  *
adamc@16:  * Redistribution and use in source and binary forms, with or without
adamc@16:  * modification, are permitted provided that the following conditions are met:
adamc@16:  *
adamc@16:  * - Redistributions of source code must retain the above copyright notice,
adamc@16:  *   this list of conditions and the following disclaimer.
adamc@16:  * - Redistributions in binary form must reproduce the above copyright notice,
adamc@16:  *   this list of conditions and the following disclaimer in the documentation
adamc@16:  *   and/or other materials provided with the distribution.
adamc@16:  * - The names of contributors may not be used to endorse or promote products
adamc@16:  *   derived from this software without specific prior written permission.
adamc@16:  *
adamc@16:  * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@16:  * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@16:  * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@16:  * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@16:  * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
adamc@16:  * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@16:  * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@16:  * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@16:  * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@16:  * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@16:  * POSSIBILITY OF SUCH DAMAGE.
adamc@16:  *)
adamc@16: 
adamc@16: structure CoreUtil :> CORE_UTIL = struct
adamc@16: 
adamc@16: open Core
adamc@16: 
adamc@16: structure S = Search
adamc@16: 
adamc@16: structure Kind = struct
adamc@16: 
adamc@193: open Order
adamc@193: 
adamc@193: fun compare ((k1, _), (k2, _)) =
adamc@193:     case (k1, k2) of
adamc@193:         (KType, KType) => EQUAL
adamc@193:       | (KType, _) => LESS
adamc@193:       | (_, KType) => GREATER
adamc@193: 
adamc@193:       | (KArrow (d1, r1), KArrow (d2, r2)) => join (compare (d1, d2), fn () => compare (r1, r2))
adamc@193:       | (KArrow _, _) => LESS
adamc@193:       | (_, KArrow _) => GREATER
adamc@193: 
adamc@193:       | (KName, KName) => EQUAL
adamc@193:       | (KName, _) => LESS
adamc@193:       | (_, KName) => GREATER
adamc@193: 
adamc@193:       | (KRecord k1, KRecord k2) => compare (k1, k2)
adamc@193:       | (KRecord _, _) => LESS
adamc@193:       | (_, KRecord _) => GREATER
adamc@193: 
adamc@193:       | (KUnit, KUnit) => EQUAL
adamc@214:       | (KUnit, _) => LESS
adamc@214:       | (_, KUnit) => GREATER
adamc@214: 
adamc@214:       | (KTuple ks1, KTuple ks2) => joinL compare (ks1, ks2)
adamc@193: 
adamc@16: fun mapfold f =
adamc@16:     let
adamc@16:         fun mfk k acc =
adamc@16:             S.bindP (mfk' k acc, f)
adamc@16: 
adamc@16:         and mfk' (kAll as (k, loc)) =
adamc@16:             case k of
adamc@16:                 KType => S.return2 kAll
adamc@16: 
adamc@16:               | KArrow (k1, k2) =>
adamc@16:                 S.bind2 (mfk k1,
adamc@16:                       fn k1' =>
adamc@16:                          S.map2 (mfk k2,
adamc@16:                               fn k2' =>
adamc@16:                                  (KArrow (k1', k2'), loc)))
adamc@16: 
adamc@16:               | KName => S.return2 kAll
adamc@16: 
adamc@16:               | KRecord k =>
adamc@16:                 S.map2 (mfk k,
adamc@16:                         fn k' =>
adamc@16:                            (KRecord k', loc))
adamc@87: 
adamc@87:               | KUnit => S.return2 kAll
adamc@214: 
adamc@214:               | KTuple ks =>
adamc@214:                 S.map2 (ListUtil.mapfold mfk ks,
adamc@214:                         fn ks' =>
adamc@214:                            (KTuple ks', loc))
adamc@16:     in
adamc@16:         mfk
adamc@16:     end
adamc@16: 
adamc@16: fun map f k =
adamc@16:     case mapfold (fn k => fn () => S.Continue (f k, ())) k () of
adamc@16:         S.Return () => raise Fail "Core_util.Kind.map"
adamc@16:       | S.Continue (k, ()) => k
adamc@16: 
adamc@16: fun exists f k =
adamc@16:     case mapfold (fn k => fn () =>
adamc@16:                              if f k then
adamc@16:                                  S.Return ()
adamc@16:                              else
adamc@16:                                  S.Continue (k, ())) k () of
adamc@16:         S.Return _ => true
adamc@16:       | S.Continue _ => false
adamc@16: 
adamc@16: end
adamc@16: 
adamc@16: structure Con = struct
adamc@16: 
adamc@193: open Order
adamc@193: 
adamc@193: fun compare ((c1, _), (c2, _)) =
adamc@193:     case (c1, c2) of
adamc@193:         (TFun (d1, r1), TFun (d2, r2)) => join (compare (d1, d2), fn () => compare (r1, r2))
adamc@193:       | (TFun _, _) => LESS
adamc@193:       | (_, TFun _) => GREATER
adamc@193: 
adamc@193:       | (TCFun (x1, k1, r1), TCFun (x2, k2, r2)) =>
adamc@193:         join (String.compare (x1, x2),
adamc@193:            fn () => join (Kind.compare (k1, k2),
adamc@193:                           fn () => compare (r1, r2)))
adamc@193:       | (TCFun _, _) => LESS
adamc@193:       | (_, TCFun _) => GREATER
adamc@193: 
adamc@193:       | (TRecord c1, TRecord c2) => compare (c1, c2)
adamc@193:       | (TRecord _, _) => LESS
adamc@193:       | (_, TRecord _) => GREATER
adamc@193: 
adamc@193:       | (CRel n1, CRel n2) => Int.compare (n1, n2)
adamc@193:       | (CRel _, _) => LESS
adamc@193:       | (_, CRel _) => GREATER
adamc@193: 
adamc@193:       | (CNamed n1, CNamed n2) => Int.compare (n1, n2)
adamc@193:       | (CNamed _, _) => LESS
adamc@193:       | (_, CNamed _) => GREATER
adamc@193: 
adamc@193:       | (CFfi (m1, s1), CFfi (m2, s2)) => join (String.compare (m1, m2),
adamc@193:                                                 fn () => String.compare (s1, s2))
adamc@193:       | (CFfi _, _) => LESS
adamc@193:       | (_, CFfi _) => GREATER
adamc@193: 
adamc@193:       | (CApp (f1, x1), CApp (f2, x2)) => join (compare (f1, f2),
adamc@193:                                                 fn () => compare (x1, x2))
adamc@193:       | (CApp _, _) => LESS
adamc@193:       | (_, CApp _) => GREATER
adamc@193: 
adamc@193:       | (CAbs (x1, k1, b1), CAbs (x2, k2, b2)) =>
adamc@193:         join (String.compare (x1, x2),
adamc@193:               fn () => join (Kind.compare (k1, k2),
adamc@193:                              fn () => compare (b1, b2)))
adamc@193:       | (CAbs _, _) => LESS
adamc@193:       | (_, CAbs _) => GREATER
adamc@193: 
adamc@193:       | (CName s1, CName s2) => String.compare (s1, s2)
adamc@193:       | (CName _, _) => LESS
adamc@193:       | (_, CName _) => GREATER
adamc@193: 
adamc@193:       | (CRecord (k1, xvs1), CRecord (k2, xvs2)) =>
adamc@193:         join (Kind.compare (k1, k2),
adamc@193:               fn () => joinL (fn ((x1, v1), (x2, v2)) =>
adamc@193:                                  join (compare (x1, x2),
adamc@193:                                        fn () => compare (v1, v2))) (xvs1, xvs2))
adamc@193:       | (CRecord _, _) => LESS
adamc@193:       | (_, CRecord _) => GREATER
adamc@193: 
adamc@193:       | (CConcat (f1, s1), CConcat (f2, s2)) =>
adamc@193:         join (compare (f1, f2),
adamc@193:               fn () => compare (s1, s2))
adamc@193:       | (CConcat _, _) => LESS
adamc@193:       | (_, CConcat _) => GREATER
adamc@193: 
adamc@193:       | (CFold (d1, r1), CFold (d2, r2)) =>
adamc@193:         join (Kind.compare (d1, r2),
adamc@193:               fn () => Kind.compare (r1, r2))
adamc@193:       | (CFold _, _) => LESS
adamc@193:       | (_, CFold _) => GREATER
adamc@193: 
adamc@193:       | (CUnit, CUnit) => EQUAL
adamc@214:       | (CUnit, _) => LESS
adamc@214:       | (_, CUnit) => GREATER
adamc@214: 
adamc@214:       | (CTuple cs1, CTuple cs2) => joinL compare (cs1, cs2)
adamc@214:       | (CTuple _, _) => LESS
adamc@214:       | (_, CTuple _) => GREATER
adamc@214: 
adamc@214:       | (CProj (c1, n1), CProj (c2, n2)) => join (Int.compare (n1, n2),
adamc@214:                                                   fn () => compare (c1, c2))
adamc@193: 
adamc@16: datatype binder =
adamc@16:          Rel of string * kind
adamc@20:        | Named of string * int * kind * con option
adamc@16: 
adamc@16: fun mapfoldB {kind = fk, con = fc, bind} =
adamc@16:     let
adamc@16:         val mfk = Kind.mapfold fk
adamc@16: 
adamc@16:         fun mfc ctx c acc =
adamc@16:             S.bindP (mfc' ctx c acc, fc ctx)
adamc@16: 
adamc@16:         and mfc' ctx (cAll as (c, loc)) =
adamc@16:             case c of
adamc@16:                 TFun (c1, c2) =>
adamc@16:                 S.bind2 (mfc ctx c1,
adamc@16:                       fn c1' =>
adamc@16:                          S.map2 (mfc ctx c2,
adamc@16:                               fn c2' =>
adamc@16:                                  (TFun (c1', c2'), loc)))
adamc@16:               | TCFun (x, k, c) =>
adamc@16:                 S.bind2 (mfk k,
adamc@16:                       fn k' =>
adamc@16:                          S.map2 (mfc (bind (ctx, Rel (x, k))) c,
adamc@16:                               fn c' =>
adamc@16:                                  (TCFun (x, k', c'), loc)))
adamc@16:               | TRecord c =>
adamc@16:                 S.map2 (mfc ctx c,
adamc@16:                         fn c' =>
adamc@16:                            (TRecord c', loc))
adamc@16: 
adamc@16:               | CRel _ => S.return2 cAll
adamc@16:               | CNamed _ => S.return2 cAll
adamc@48:               | CFfi _ => S.return2 cAll
adamc@16:               | CApp (c1, c2) =>
adamc@16:                 S.bind2 (mfc ctx c1,
adamc@16:                       fn c1' =>
adamc@16:                          S.map2 (mfc ctx c2,
adamc@16:                               fn c2' =>
adamc@16:                                  (CApp (c1', c2'), loc)))
adamc@16:               | CAbs (x, k, c) =>
adamc@16:                 S.bind2 (mfk k,
adamc@16:                       fn k' =>
adamc@16:                          S.map2 (mfc (bind (ctx, Rel (x, k))) c,
adamc@16:                               fn c' =>
adamc@16:                                  (CAbs (x, k', c'), loc)))
adamc@16: 
adamc@16:               | CName _ => S.return2 cAll
adamc@16: 
adamc@16:               | CRecord (k, xcs) =>
adamc@16:                 S.bind2 (mfk k,
adamc@16:                       fn k' =>
adamc@16:                          S.map2 (ListUtil.mapfold (fn (x, c) =>
adamc@16:                                                       S.bind2 (mfc ctx x,
adamc@16:                                                             fn x' =>
adamc@16:                                                                S.map2 (mfc ctx c,
adamc@16:                                                                     fn c' =>
adamc@16:                                                                        (x', c'))))
adamc@16:                                  xcs,
adamc@16:                               fn xcs' =>
adamc@16:                                  (CRecord (k', xcs'), loc)))
adamc@16:               | CConcat (c1, c2) =>
adamc@16:                 S.bind2 (mfc ctx c1,
adamc@16:                       fn c1' =>
adamc@16:                          S.map2 (mfc ctx c2,
adamc@16:                               fn c2' =>
adamc@16:                                  (CConcat (c1', c2'), loc)))
adamc@69:               | CFold (k1, k2) =>
adamc@69:                 S.bind2 (mfk k1,
adamc@69:                          fn k1' =>
adamc@69:                             S.map2 (mfk k2,
adamc@69:                                     fn k2' =>
adamc@69:                                        (CFold (k1', k2'), loc)))
adamc@87: 
adamc@87:               | CUnit => S.return2 cAll
adamc@214: 
adamc@214:               | CTuple cs =>
adamc@214:                 S.map2 (ListUtil.mapfold (mfc ctx) cs,
adamc@214:                         fn cs' =>
adamc@214:                            (CTuple cs', loc))
adamc@214: 
adamc@214:               | CProj (c, n) =>
adamc@214:                 S.map2 (mfc ctx c,
adamc@214:                         fn c' =>
adamc@214:                            (CProj (c', n), loc))
adamc@16:     in
adamc@16:         mfc
adamc@16:     end
adamc@16: 
adamc@16: fun mapfold {kind = fk, con = fc} =
adamc@16:     mapfoldB {kind = fk,
adamc@16:               con = fn () => fc,
adamc@16:               bind = fn ((), _) => ()} ()
adamc@16: 
adamc@16: fun map {kind, con} c =
adamc@16:     case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
adamc@16:                   con = fn c => fn () => S.Continue (con c, ())} c () of
adamc@16:         S.Return () => raise Fail "Core_util.Con.map"
adamc@16:       | S.Continue (c, ()) => c
adamc@16: 
adamc@16: fun mapB {kind, con, bind} ctx c =
adamc@16:     case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()),
adamc@16:                    con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
adamc@16:                    bind = bind} ctx c () of
adamc@16:         S.Continue (c, ()) => c
adamc@20:       | S.Return _ => raise Fail "CoreUtil.Con.mapB: Impossible"
adamc@16: 
adamc@23: fun fold {kind, con} s c =
adamc@23:     case mapfold {kind = fn k => fn s => S.Continue (k, kind (k, s)),
adamc@23:                   con = fn c => fn s => S.Continue (c, con (c, s))} c s of
adamc@23:         S.Continue (_, s) => s
adamc@23:       | S.Return _ => raise Fail "CoreUtil.Con.fold: Impossible"
adamc@23: 
adamc@16: fun exists {kind, con} k =
adamc@16:     case mapfold {kind = fn k => fn () =>
adamc@16:                                     if kind k then
adamc@16:                                         S.Return ()
adamc@16:                                     else
adamc@16:                                         S.Continue (k, ()),
adamc@16:                   con = fn c => fn () =>
adamc@16:                                     if con c then
adamc@16:                                         S.Return ()
adamc@16:                                     else
adamc@16:                                         S.Continue (c, ())} k () of
adamc@16:         S.Return _ => true
adamc@16:       | S.Continue _ => false
adamc@16: 
adamc@193: fun foldMap {kind, con} s c =
adamc@193:     case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)),
adamc@193:                   con = fn c => fn s => S.Continue (con (c, s))} c s of
adamc@193:         S.Continue v => v
adamc@193:       | S.Return _ => raise Fail "CoreUtil.Con.foldMap: Impossible"
adamc@193: 
adamc@16: end
adamc@16: 
adamc@16: structure Exp = struct
adamc@16: 
adamc@16: datatype binder =
adamc@16:          RelC of string * kind
adamc@20:        | NamedC of string * int * kind * con option
adamc@16:        | RelE of string * con
adamc@109:        | NamedE of string * int * con * exp option * string
adamc@16: 
adamc@16: fun mapfoldB {kind = fk, con = fc, exp = fe, bind} =
adamc@16:     let
adamc@16:         val mfk = Kind.mapfold fk
adamc@16: 
adamc@16:         fun bind' (ctx, b) =
adamc@16:             let
adamc@16:                 val b' = case b of
adamc@16:                              Con.Rel x => RelC x
adamc@16:                            | Con.Named x => NamedC x
adamc@16:             in
adamc@16:                 bind (ctx, b')
adamc@16:             end
adamc@16:         val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
adamc@16: 
adamc@16:         fun mfe ctx e acc =
adamc@16:             S.bindP (mfe' ctx e acc, fe ctx)
adamc@16: 
adamc@16:         and mfe' ctx (eAll as (e, loc)) =
adamc@16:             case e of
adamc@16:                 EPrim _ => S.return2 eAll
adamc@16:               | ERel _ => S.return2 eAll
adamc@16:               | ENamed _ => S.return2 eAll
adamc@192:               | ECon (dk, pc, cs, NONE) =>
adamc@192:                 S.map2 (ListUtil.mapfold (mfc ctx) cs,
adamc@192:                         fn cs' =>
adamc@192:                            (ECon (dk, pc, cs', NONE), loc))
adamc@192:               | ECon (dk, n, cs, SOME e) =>
adamc@192:                 S.bind2 (mfe ctx e,
adamc@192:                       fn e' =>
adamc@192:                          S.map2 (ListUtil.mapfold (mfc ctx) cs,
adamc@192:                                  fn cs' =>
adamc@192:                                     (ECon (dk, n, cs', SOME e'), loc)))
adamc@48:               | EFfi _ => S.return2 eAll
adamc@48:               | EFfiApp (m, x, es) =>
adamc@192:                 S.map2 (ListUtil.mapfold (mfe ctx) es,
adamc@48:                      fn es' =>
adamc@48:                         (EFfiApp (m, x, es'), loc))
adamc@16:               | EApp (e1, e2) =>
adamc@16:                 S.bind2 (mfe ctx e1,
adamc@16:                       fn e1' =>
adamc@16:                          S.map2 (mfe ctx e2,
adamc@16:                               fn e2' =>
adamc@16:                                  (EApp (e1', e2'), loc)))
adamc@26:               | EAbs (x, dom, ran, e) =>
adamc@26:                 S.bind2 (mfc ctx dom,
adamc@26:                       fn dom' =>
adamc@26:                          S.bind2 (mfc ctx ran,
adamc@26:                                fn ran' =>
adamc@26:                                   S.map2 (mfe (bind (ctx, RelE (x, dom'))) e,
adamc@26:                                        fn e' =>
adamc@26:                                           (EAbs (x, dom', ran', e'), loc))))
adamc@16: 
adamc@16:               | ECApp (e, c) =>
adamc@16:                 S.bind2 (mfe ctx e,
adamc@16:                       fn e' =>
adamc@16:                          S.map2 (mfc ctx c,
adamc@16:                               fn c' =>
adamc@16:                                  (ECApp (e', c'), loc)))
adamc@16:               | ECAbs (x, k, e) =>
adamc@16:                 S.bind2 (mfk k,
adamc@16:                       fn k' =>
adamc@16:                          S.map2 (mfe (bind (ctx, RelC (x, k))) e,
adamc@16:                               fn e' =>
adamc@16:                                  (ECAbs (x, k', e'), loc)))
adamc@16: 
adamc@16:               | ERecord xes =>
adamc@29:                 S.map2 (ListUtil.mapfold (fn (x, e, t) =>
adamc@16:                                              S.bind2 (mfc ctx x,
adamc@16:                                                    fn x' =>
adamc@29:                                                       S.bind2 (mfe ctx e,
adamc@29:                                                             fn e' =>
adamc@29:                                                                S.map2 (mfc ctx t,
adamc@29:                                                                     fn t' =>
adamc@29:                                                                        (x', e', t')))))
adamc@16:                                          xes,
adamc@16:                      fn xes' =>
adamc@16:                         (ERecord xes', loc))
adamc@16:               | EField (e, c, {field, rest}) =>
adamc@16:                 S.bind2 (mfe ctx e,
adamc@16:                       fn e' =>
adamc@16:                          S.bind2 (mfc ctx c,
adamc@16:                               fn c' =>
adamc@16:                                  S.bind2 (mfc ctx field,
adamc@16:                                           fn field' =>
adamc@16:                                              S.map2 (mfc ctx rest,
adamc@16:                                                   fn rest' =>
adamc@16:                                                      (EField (e', c', {field = field', rest = rest'}), loc)))))
adamc@149:               | ECut (e, c, {field, rest}) =>
adamc@149:                 S.bind2 (mfe ctx e,
adamc@149:                       fn e' =>
adamc@149:                          S.bind2 (mfc ctx c,
adamc@149:                               fn c' =>
adamc@149:                                  S.bind2 (mfc ctx field,
adamc@149:                                           fn field' =>
adamc@149:                                              S.map2 (mfc ctx rest,
adamc@149:                                                   fn rest' =>
adamc@149:                                                      (ECut (e', c', {field = field', rest = rest'}), loc)))))
adamc@73:               | EFold k =>
adamc@73:                 S.map2 (mfk k,
adamc@73:                          fn k' =>
adamc@73:                             (EFold k', loc))
adamc@102: 
adamc@182:               | ECase (e, pes, {disc, result}) =>
adamc@177:                 S.bind2 (mfe ctx e,
adamc@177:                          fn e' =>
adamc@177:                             S.bind2 (ListUtil.mapfold (fn (p, e) =>
adamc@193:                                                           let
adamc@193:                                                               fun pb ((p, _), ctx) =
adamc@193:                                                                   case p of
adamc@193:                                                                       PWild => ctx
adamc@193:                                                                     | PVar (x, t) => bind (ctx, RelE (x, t))
adamc@193:                                                                     | PPrim _ => ctx
adamc@193:                                                                     | PCon (_, _, _, NONE) => ctx
adamc@193:                                                                     | PCon (_, _, _, SOME p) => pb (p, ctx)
adamc@193:                                                                     | PRecord xps => foldl (fn ((_, p, _), ctx) =>
adamc@193:                                                                                                pb (p, ctx)) ctx xps
adamc@193:                                                           in
adamc@193:                                                               S.bind2 (mfp ctx p,
adamc@193:                                                                        fn p' =>
adamc@193:                                                                           S.map2 (mfe (pb (p', ctx)) e,
adamc@193:                                                                                fn e' => (p', e')))
adamc@193:                                                           end) pes,
adamc@177:                                     fn pes' =>
adamc@182:                                        S.bind2 (mfc ctx disc,
adamc@182:                                                 fn disc' =>
adamc@182:                                                    S.map2 (mfc ctx result,
adamc@182:                                                         fn result' =>
adamc@182:                                                            (ECase (e', pes', {disc = disc', result = result'}), loc)))))
adamc@177: 
adamc@102:               | EWrite e =>
adamc@102:                 S.map2 (mfe ctx e,
adamc@102:                      fn e' =>
adamc@102:                         (EWrite e', loc))
adamc@110: 
adamc@110:               | EClosure (n, es) =>
adamc@110:                 S.map2 (ListUtil.mapfold (mfe ctx) es,
adamc@110:                      fn es' =>
adamc@110:                         (EClosure (n, es'), loc))
adamc@193: 
adamc@193:         and mfp ctx (pAll as (p, loc)) =
adamc@193:             case p of
adamc@193:                 PWild => S.return2 pAll
adamc@193:               | PVar (x, t) =>
adamc@193:                 S.map2 (mfc ctx t,
adamc@193:                         fn t' =>
adamc@193:                            (PVar (x, t'), loc))
adamc@193:               | PPrim _ => S.return2 pAll
adamc@193:               | PCon (dk, pc, args, po) =>
adamc@193:                 S.bind2 (mfpc ctx pc,
adamc@193:                          fn pc' =>
adamc@193:                             S.bind2 (ListUtil.mapfold (mfc ctx) args,
adamc@193:                                      fn args' =>
adamc@193:                                         S.map2 ((case po of
adamc@193:                                                      NONE => S.return2 NONE
adamc@193:                                                    | SOME p => S.map2 (mfp ctx p, SOME)),
adamc@193:                                                 fn po' =>
adamc@193:                                                    (PCon (dk, pc', args', po'), loc))))
adamc@193:               | PRecord xps =>
adamc@193:                 S.map2 (ListUtil.mapfold (fn (x, p, c) =>
adamc@193:                                               S.bind2 (mfp ctx p,
adamc@193:                                                        fn p' =>
adamc@193:                                                           S.map2 (mfc ctx c,
adamc@193:                                                                   fn c' =>
adamc@193:                                                                      (x, p', c')))) xps,
adamc@193:                          fn xps' =>
adamc@193:                             (PRecord xps', loc))
adamc@193: 
adamc@193:         and mfpc ctx pc =
adamc@193:             case pc of
adamc@193:                 PConVar _ => S.return2 pc
adamc@193:               | PConFfi {mod = m, datatyp, params, con, arg, kind} =>
adamc@193:                 S.map2 ((case arg of
adamc@193:                              NONE => S.return2 NONE
adamc@193:                            | SOME c => S.map2 (mfc ctx c, SOME)),
adamc@193:                         fn arg' =>
adamc@193:                            PConFfi {mod = m, datatyp = datatyp, params = params,
adamc@193:                                     con = con, arg = arg', kind = kind})
adamc@16:     in
adamc@16:         mfe
adamc@16:     end
adamc@16: 
adamc@16: fun mapfold {kind = fk, con = fc, exp = fe} =
adamc@16:     mapfoldB {kind = fk,
adamc@16:               con = fn () => fc,
adamc@16:               exp = fn () => fe,
adamc@16:               bind = fn ((), _) => ()} ()
adamc@16: 
adamc@21: fun mapB {kind, con, exp, bind} ctx e =
adamc@21:     case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()),
adamc@21:                    con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
adamc@21:                    exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
adamc@21:                    bind = bind} ctx e () of
adamc@21:         S.Continue (e, ()) => e
adamc@21:       | S.Return _ => raise Fail "CoreUtil.Exp.mapB: Impossible"
adamc@21: 
adamc@16: fun map {kind, con, exp} e =
adamc@16:     case mapfold {kind = fn k => fn () => S.Continue (kind k, ()),
adamc@16:                   con = fn c => fn () => S.Continue (con c, ()),
adamc@16:                   exp = fn e => fn () => S.Continue (exp e, ())} e () of
adamc@16:         S.Return () => raise Fail "Core_util.Exp.map"
adamc@16:       | S.Continue (e, ()) => e
adamc@16: 
adamc@23: fun fold {kind, con, exp} s e =
adamc@23:     case mapfold {kind = fn k => fn s => S.Continue (k, kind (k, s)),
adamc@23:                   con = fn c => fn s => S.Continue (c, con (c, s)),
adamc@23:                   exp = fn e => fn s => S.Continue (e, exp (e, s))} e s of
adamc@23:         S.Continue (_, s) => s
adamc@23:       | S.Return _ => raise Fail "CoreUtil.Exp.fold: Impossible"
adamc@23: 
adamc@16: fun exists {kind, con, exp} k =
adamc@16:     case mapfold {kind = fn k => fn () =>
adamc@16:                                     if kind k then
adamc@16:                                         S.Return ()
adamc@16:                                     else
adamc@16:                                         S.Continue (k, ()),
adamc@16:                   con = fn c => fn () =>
adamc@16:                                     if con c then
adamc@16:                                         S.Return ()
adamc@16:                                     else
adamc@16:                                         S.Continue (c, ()),
adamc@16:                   exp = fn e => fn () =>
adamc@16:                                     if exp e then
adamc@16:                                         S.Return ()
adamc@16:                                     else
adamc@16:                                         S.Continue (e, ())} k () of
adamc@16:         S.Return _ => true
adamc@16:       | S.Continue _ => false
adamc@16: 
adamc@16: end
adamc@16: 
adamc@20: structure Decl = struct
adamc@20: 
adamc@20: datatype binder = datatype Exp.binder
adamc@20: 
adamc@20: fun mapfoldB {kind = fk, con = fc, exp = fe, decl = fd, bind} =
adamc@20:     let
adamc@20:         val mfk = Kind.mapfold fk
adamc@20: 
adamc@20:         fun bind' (ctx, b) =
adamc@20:             let
adamc@20:                 val b' = case b of
adamc@20:                              Con.Rel x => RelC x
adamc@20:                            | Con.Named x => NamedC x
adamc@20:             in
adamc@20:                 bind (ctx, b')
adamc@20:             end
adamc@20:         val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'}
adamc@20: 
adamc@20:         val mfe = Exp.mapfoldB {kind = fk, con = fc, exp = fe, bind = bind}
adamc@20: 
adamc@20:         fun mfd ctx d acc =
adamc@20:             S.bindP (mfd' ctx d acc, fd ctx)
adamc@20: 
adamc@20:         and mfd' ctx (dAll as (d, loc)) =
adamc@20:             case d of
adamc@20:                 DCon (x, n, k, c) =>
adamc@20:                 S.bind2 (mfk k,
adamc@20:                       fn k' =>
adamc@20:                          S.map2 (mfc ctx c,
adamc@20:                               fn c' =>
adamc@20:                                  (DCon (x, n, k', c'), loc)))
adamc@192:               | DDatatype (x, n, xs, xncs) =>
adamc@196:                 let
adamc@196:                     val k = (KType, loc)
adamc@196:                     val k' = foldl (fn (_, k') => (KArrow (k, k'), loc)) k xs
adamc@196:                     val ctx' = bind (ctx, NamedC (x, n, k', NONE))
adamc@196:                 in
adamc@196:                     S.map2 (ListUtil.mapfold (fn (x, n, c) =>
adamc@196:                                                  case c of
adamc@196:                                                      NONE => S.return2 (x, n, c)
adamc@196:                                                    | SOME c =>
adamc@196:                                                      S.map2 (mfc ctx' c,
adamc@196:                                                           fn c' => (x, n, SOME c'))) xncs,
adamc@196:                          fn xncs' =>
adamc@196:                             (DDatatype (x, n, xs, xncs'), loc))
adamc@196:                 end
adamc@125:               | DVal vi =>
adamc@125:                 S.map2 (mfvi ctx vi,
adamc@125:                      fn vi' =>
adamc@125:                         (DVal vi', loc))
adamc@125:               | DValRec vis =>
adamc@127:                 let
adamc@127:                     val ctx = foldl (fn ((x, n, t, e, s), ctx) => bind (ctx, NamedE (x, n, t, NONE, s)))
adamc@127:                                     ctx vis
adamc@127:                 in
adamc@127:                     S.map2 (ListUtil.mapfold (mfvi ctx) vis,
adamc@127:                          fn vis' =>
adamc@127:                             (DValRec vis', loc))
adamc@127:                 end
adamc@109:               | DExport _ => S.return2 dAll
adamc@125: 
adamc@125:         and mfvi ctx (x, n, t, e, s) =
adamc@125:             S.bind2 (mfc ctx t,
adamc@125:                   fn t' =>
adamc@125:                      S.map2 (mfe ctx e,
adamc@125:                           fn e' =>
adamc@125:                              (x, n, t', e', s)))
adamc@20:     in
adamc@20:         mfd
adamc@20:     end    
adamc@20: 
adamc@23: fun mapfold {kind = fk, con = fc, exp = fe, decl = fd} =
adamc@23:     mapfoldB {kind = fk,
adamc@23:               con = fn () => fc,
adamc@23:               exp = fn () => fe,
adamc@23:               decl = fn () => fd,
adamc@23:               bind = fn ((), _) => ()} ()
adamc@23: 
adamc@23: fun fold {kind, con, exp, decl} s d =
adamc@23:     case mapfold {kind = fn k => fn s => S.Continue (k, kind (k, s)),
adamc@23:                   con = fn c => fn s => S.Continue (c, con (c, s)),
adamc@23:                   exp = fn e => fn s => S.Continue (e, exp (e, s)),
adamc@23:                   decl = fn d => fn s => S.Continue (d, decl (d, s))} d s of
adamc@23:         S.Continue (_, s) => s
adamc@23:       | S.Return _ => raise Fail "CoreUtil.Decl.fold: Impossible"
adamc@23: 
adamc@110: fun foldMap {kind, con, exp, decl} s d =
adamc@110:     case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)),
adamc@110:                   con = fn c => fn s => S.Continue (con (c, s)),
adamc@110:                   exp = fn e => fn s => S.Continue (exp (e, s)),
adamc@110:                   decl = fn d => fn s => S.Continue (decl (d, s))} d s of
adamc@110:         S.Continue v => v
adamc@110:       | S.Return _ => raise Fail "CoreUtil.Decl.foldMap: Impossible"
adamc@110: 
adamc@16: end
adamc@20: 
adamc@20: structure File = struct
adamc@20: 
adamc@20: datatype binder = datatype Exp.binder
adamc@20: 
adamc@20: fun mapfoldB (all as {bind, ...}) =
adamc@20:     let
adamc@20:         val mfd = Decl.mapfoldB all
adamc@20: 
adamc@20:         fun mff ctx ds =
adamc@20:             case ds of
adamc@20:                 nil => S.return2 nil
adamc@20:               | d :: ds' =>
adamc@20:                 S.bind2 (mfd ctx d,
adamc@20:                          fn d' =>
adamc@20:                             let
adamc@100:                                 val ctx' =
adamc@20:                                     case #1 d' of
adamc@100:                                         DCon (x, n, k, c) => bind (ctx, NamedC (x, n, k, SOME c))
adamc@192:                                       | DDatatype (x, n, xs, xncs) =>
adamc@163:                                         let
adamc@192:                                             val loc = #2 d'
adamc@192:                                             val k = (KType, loc)
adamc@192:                                             val k' = foldl (fn (_, k') => (KArrow (k, k'), loc)) k xs
adamc@192: 
adamc@192:                                             val ctx = bind (ctx, NamedC (x, n, k', NONE))
adamc@163:                                             val t = (CNamed n, #2 d')
adamc@192:                                             val t = ListUtil.foldli (fn (i, _, t) => (CApp (t, (CRel i, loc)), loc))
adamc@192:                                                                     t xs
adamc@163:                                         in
adamc@163:                                             foldl (fn ((x, n, to), ctx) =>
adamc@163:                                                       let
adamc@163:                                                           val t = case to of
adamc@163:                                                                       NONE => t
adamc@163:                                                                     | SOME t' => (TFun (t', t), #2 d')
adamc@192:                                                           val t = foldr (fn (x, t) => (TCFun (x, k, t), loc))
adamc@192:                                                                         t xs
adamc@163:                                                       in
adamc@163:                                                           bind (ctx, NamedE (x, n, t, NONE, ""))
adamc@163:                                                       end)
adamc@163:                                             ctx xncs
adamc@163:                                         end
adamc@109:                                       | DVal (x, n, t, e, s) => bind (ctx, NamedE (x, n, t, SOME e, s))
adamc@125:                                       | DValRec vis =>
adamc@127:                                         foldl (fn ((x, n, t, e, s), ctx) => bind (ctx, NamedE (x, n, t, NONE, s)))
adamc@125:                                         ctx vis
adamc@109:                                       | DExport _ => ctx
adamc@20:                             in
adamc@20:                                 S.map2 (mff ctx' ds',
adamc@20:                                      fn ds' =>
adamc@20:                                         d' :: ds')
adamc@20:                             end)
adamc@20:     in
adamc@20:         mff
adamc@20:     end
adamc@20: 
adamc@23: fun mapfold {kind = fk, con = fc, exp = fe, decl = fd} =
adamc@23:     mapfoldB {kind = fk,
adamc@23:               con = fn () => fc,
adamc@23:               exp = fn () => fe,
adamc@23:               decl = fn () => fd,
adamc@23:               bind = fn ((), _) => ()} ()
adamc@23: 
adamc@20: fun mapB {kind, con, exp, decl, bind} ctx ds =
adamc@20:     case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()),
adamc@20:                    con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()),
adamc@20:                    exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()),
adamc@20:                    decl = fn ctx => fn d => fn () => S.Continue (decl ctx d, ()),
adamc@20:                    bind = bind} ctx ds () of
adamc@20:         S.Continue (ds, ()) => ds
adamc@20:       | S.Return _ => raise Fail "CoreUtil.File.mapB: Impossible"
adamc@20: 
adamc@23: fun fold {kind, con, exp, decl} s d =
adamc@23:     case mapfold {kind = fn k => fn s => S.Continue (k, kind (k, s)),
adamc@23:                   con = fn c => fn s => S.Continue (c, con (c, s)),
adamc@23:                   exp = fn e => fn s => S.Continue (e, exp (e, s)),
adamc@23:                   decl = fn d => fn s => S.Continue (d, decl (d, s))} d s of
adamc@23:         S.Continue (_, s) => s
adamc@23:       | S.Return _ => raise Fail "CoreUtil.File.fold: Impossible"
adamc@23: 
adamc@110: fun foldMap {kind, con, exp, decl} s d =
adamc@110:     case mapfold {kind = fn k => fn s => S.Continue (kind (k, s)),
adamc@110:                   con = fn c => fn s => S.Continue (con (c, s)),
adamc@110:                   exp = fn e => fn s => S.Continue (exp (e, s)),
adamc@110:                   decl = fn d => fn s => S.Continue (decl (d, s))} d s of
adamc@110:         S.Continue v => v
adamc@110:       | S.Return _ => raise Fail "CoreUtil.File.foldMap: Impossible"
adamc@110: 
adamc@179: val maxName = foldl (fn ((d, _) : decl, count) =>
adamc@179:                         case d of
adamc@179:                             DCon (_, n, _, _) => Int.max (n, count)
adamc@192:                           | DDatatype (_, n, _, _) => Int.max (n, count)
adamc@179:                           | DVal (_, n, _, _, _) => Int.max (n, count)
adamc@179:                           | DValRec vis => foldl (fn ((_, n, _, _, _), count) => Int.max (n, count)) count vis
adamc@179:                           | DExport _ => count) 0
adamc@179:               
adamc@20: end
adamc@20: 
adamc@20: end