adamc@38: (* Copyright (c) 2008, Adam Chlipala adamc@38: * All rights reserved. adamc@38: * adamc@38: * Redistribution and use in source and binary forms, with or without adamc@38: * modification, are permitted provided that the following conditions are met: adamc@38: * adamc@38: * - Redistributions of source code must retain the above copyright notice, adamc@38: * this list of conditions and the following disclaimer. adamc@38: * - Redistributions in binary form must reproduce the above copyright notice, adamc@38: * this list of conditions and the following disclaimer in the documentation adamc@38: * and/or other materials provided with the distribution. adamc@38: * - The names of contributors may not be used to endorse or promote products adamc@38: * derived from this software without specific prior written permission. adamc@38: * adamc@38: * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" adamc@38: * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE adamc@38: * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE adamc@38: * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE adamc@38: * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR adamc@38: * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF adamc@38: * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS adamc@38: * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN adamc@38: * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) adamc@38: * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE adamc@38: * POSSIBILITY OF SUCH DAMAGE. adamc@38: *) adamc@38: adamc@38: structure ExplUtil :> EXPL_UTIL = struct adamc@38: adamc@38: open Expl adamc@38: adamc@38: structure S = Search adamc@38: adamc@38: structure Kind = struct adamc@38: adamc@624: fun mapfoldB {kind, bind} = adamc@38: let adamc@624: fun mfk ctx k acc = adamc@624: S.bindP (mfk' ctx k acc, kind ctx) adamc@38: adamc@624: and mfk' ctx (kAll as (k, loc)) = adamc@38: case k of adamc@38: KType => S.return2 kAll adamc@38: adamc@38: | KArrow (k1, k2) => adamc@624: S.bind2 (mfk ctx k1, adamc@38: fn k1' => adamc@624: S.map2 (mfk ctx k2, adamc@38: fn k2' => adamc@38: (KArrow (k1', k2'), loc))) adamc@38: adamc@38: | KName => S.return2 kAll adamc@38: adamc@38: | KRecord k => adamc@624: S.map2 (mfk ctx k, adamc@38: fn k' => adamc@38: (KRecord k', loc)) adamc@87: adamc@87: | KUnit => S.return2 kAll adamc@213: adamc@213: | KTuple ks => adamc@624: S.map2 (ListUtil.mapfold (mfk ctx) ks, adamc@213: fn ks' => adamc@213: (KTuple ks', loc)) adamc@624: adamc@624: | KRel _ => S.return2 kAll adamc@624: | KFun (x, k) => adamc@624: S.map2 (mfk (bind (ctx, x)) k, adamc@624: fn k' => adamc@624: (KFun (x, k'), loc)) adamc@38: in adamc@38: mfk adamc@38: end adamc@38: adamc@624: fun mapfold fk = adamc@624: mapfoldB {kind = fn () => fk, adamc@624: bind = fn ((), _) => ()} () adamc@624: adamc@624: fun mapB {kind, bind} ctx k = adamc@624: case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()), adamc@624: bind = bind} ctx k () of adamc@624: S.Continue (k, ()) => k adamc@624: | S.Return _ => raise Fail "ExplUtil.Kind.mapB: Impossible" adamc@624: adamc@38: fun exists f k = adamc@38: case mapfold (fn k => fn () => adamc@38: if f k then adamc@38: S.Return () adamc@38: else adamc@38: S.Continue (k, ())) k () of adamc@38: S.Return _ => true adamc@38: | S.Continue _ => false adamc@38: adamc@38: end adamc@38: adamc@38: structure Con = struct adamc@38: adamc@38: datatype binder = adamc@624: RelK of string adamc@624: | RelC of string * Expl.kind adamc@624: | NamedC of string * Expl.kind adamc@38: adamc@38: fun mapfoldB {kind = fk, con = fc, bind} = adamc@38: let adamc@624: val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)} adamc@38: adamc@38: fun mfc ctx c acc = adamc@38: S.bindP (mfc' ctx c acc, fc ctx) adamc@38: adamc@38: and mfc' ctx (cAll as (c, loc)) = adamc@38: case c of adamc@38: TFun (c1, c2) => adamc@38: S.bind2 (mfc ctx c1, adamc@38: fn c1' => adamc@38: S.map2 (mfc ctx c2, adamc@38: fn c2' => adamc@38: (TFun (c1', c2'), loc))) adamc@38: | TCFun (x, k, c) => adamc@624: S.bind2 (mfk ctx k, adamc@38: fn k' => adamc@624: S.map2 (mfc (bind (ctx, RelC (x, k))) c, adamc@38: fn c' => adamc@38: (TCFun (x, k', c'), loc))) adamc@38: | TRecord c => adamc@38: S.map2 (mfc ctx c, adamc@38: fn c' => adamc@38: (TRecord c', loc)) adamc@38: adamc@38: | CRel _ => S.return2 cAll adamc@38: | CNamed _ => S.return2 cAll adamc@38: | CModProj _ => S.return2 cAll adamc@38: | CApp (c1, c2) => adamc@38: S.bind2 (mfc ctx c1, adamc@38: fn c1' => adamc@38: S.map2 (mfc ctx c2, adamc@38: fn c2' => adamc@38: (CApp (c1', c2'), loc))) adamc@38: | CAbs (x, k, c) => adamc@624: S.bind2 (mfk ctx k, adamc@38: fn k' => adamc@624: S.map2 (mfc (bind (ctx, RelC (x, k))) c, adamc@38: fn c' => adamc@38: (CAbs (x, k', c'), loc))) adamc@38: adamc@38: | CName _ => S.return2 cAll adamc@38: adamc@38: | CRecord (k, xcs) => adamc@624: S.bind2 (mfk ctx k, adamc@38: fn k' => adamc@38: S.map2 (ListUtil.mapfold (fn (x, c) => adamc@38: S.bind2 (mfc ctx x, adamc@38: fn x' => adamc@38: S.map2 (mfc ctx c, adamc@38: fn c' => adamc@38: (x', c')))) adamc@38: xcs, adamc@38: fn xcs' => adamc@38: (CRecord (k', xcs'), loc))) adamc@38: | CConcat (c1, c2) => adamc@38: S.bind2 (mfc ctx c1, adamc@38: fn c1' => adamc@38: S.map2 (mfc ctx c2, adamc@38: fn c2' => adamc@38: (CConcat (c1', c2'), loc))) adamc@621: | CMap (k1, k2) => adamc@624: S.bind2 (mfk ctx k1, adamc@68: fn k1' => adamc@624: S.map2 (mfk ctx k2, adamc@68: fn k2' => adamc@621: (CMap (k1', k2'), loc))) adamc@87: adamc@87: | CUnit => S.return2 cAll adamc@213: adamc@213: | CTuple cs => adamc@213: S.map2 (ListUtil.mapfold (mfc ctx) cs, adamc@213: fn cs' => adamc@213: (CTuple cs', loc)) adamc@213: adamc@213: | CProj (c, n) => adamc@213: S.map2 (mfc ctx c, adamc@213: fn c' => adamc@213: (CProj (c', n), loc)) adamc@624: adamc@624: | CKAbs (x, c) => adamc@624: S.map2 (mfc (bind (ctx, RelK x)) c, adamc@624: fn c' => adamc@624: (CKAbs (x, c'), loc)) adamc@624: | CKApp (c, k) => adamc@624: S.bind2 (mfc ctx c, adamc@624: fn c' => adamc@624: S.map2 (mfk ctx k, adamc@624: fn k' => adamc@624: (CKApp (c', k'), loc))) adamc@624: | TKFun (x, c) => adamc@624: S.map2 (mfc (bind (ctx, RelK x)) c, adamc@624: fn c' => adamc@624: (TKFun (x, c'), loc)) adamc@38: in adamc@38: mfc adamc@38: end adamc@38: adamc@38: fun mapfold {kind = fk, con = fc} = adamc@624: mapfoldB {kind = fn () => fk, adamc@38: con = fn () => fc, adamc@38: bind = fn ((), _) => ()} () adamc@38: adamc@38: fun mapB {kind, con, bind} ctx c = adamc@624: case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()), adamc@38: con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()), adamc@38: bind = bind} ctx c () of adamc@38: S.Continue (c, ()) => c adamc@38: | S.Return _ => raise Fail "ExplUtil.Con.mapB: Impossible" adamc@38: adamc@38: fun map {kind, con} s = adamc@38: case mapfold {kind = fn k => fn () => S.Continue (kind k, ()), adamc@38: con = fn c => fn () => S.Continue (con c, ())} s () of adamc@38: S.Return () => raise Fail "ExplUtil.Con.map: Impossible" adamc@38: | S.Continue (s, ()) => s adamc@38: adamc@38: fun exists {kind, con} k = adamc@38: case mapfold {kind = fn k => fn () => adamc@38: if kind k then adamc@38: S.Return () adamc@38: else adamc@38: S.Continue (k, ()), adamc@38: con = fn c => fn () => adamc@38: if con c then adamc@38: S.Return () adamc@38: else adamc@38: S.Continue (c, ())} k () of adamc@38: S.Return _ => true adamc@38: | S.Continue _ => false adamc@38: adamc@38: end adamc@38: adamc@38: structure Exp = struct adamc@38: adamc@38: datatype binder = adamc@624: RelK of string adamc@624: | RelC of string * Expl.kind adamc@38: | NamedC of string * Expl.kind adamc@38: | RelE of string * Expl.con adamc@38: | NamedE of string * Expl.con adamc@38: adamc@38: fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = adamc@38: let adamc@624: val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)} adamc@38: adamc@38: fun bind' (ctx, b) = adamc@38: let adamc@38: val b' = case b of adamc@624: Con.RelK x => RelK x adamc@624: | Con.RelC x => RelC x adamc@624: | Con.NamedC x => NamedC x adamc@38: in adamc@38: bind (ctx, b') adamc@38: end adamc@38: val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'} adamc@38: adamc@38: fun mfe ctx e acc = adamc@38: S.bindP (mfe' ctx e acc, fe ctx) adamc@38: adamc@38: and mfe' ctx (eAll as (e, loc)) = adamc@38: case e of adamc@38: EPrim _ => S.return2 eAll adamc@38: | ERel _ => S.return2 eAll adamc@38: | ENamed _ => S.return2 eAll adamc@38: | EModProj _ => S.return2 eAll adamc@38: | EApp (e1, e2) => adamc@38: S.bind2 (mfe ctx e1, adamc@38: fn e1' => adamc@38: S.map2 (mfe ctx e2, adamc@38: fn e2' => adamc@38: (EApp (e1', e2'), loc))) adamc@38: | EAbs (x, dom, ran, e) => adamc@38: S.bind2 (mfc ctx dom, adamc@38: fn dom' => adamc@38: S.bind2 (mfc ctx ran, adamc@38: fn ran' => adamc@38: S.map2 (mfe (bind (ctx, RelE (x, dom'))) e, adamc@38: fn e' => adamc@38: (EAbs (x, dom', ran', e'), loc)))) adamc@38: adamc@38: | ECApp (e, c) => adamc@38: S.bind2 (mfe ctx e, adamc@38: fn e' => adamc@38: S.map2 (mfc ctx c, adamc@38: fn c' => adamc@38: (ECApp (e', c'), loc))) adamc@38: | ECAbs (x, k, e) => adamc@624: S.bind2 (mfk ctx k, adamc@38: fn k' => adamc@38: S.map2 (mfe (bind (ctx, RelC (x, k))) e, adamc@38: fn e' => adamc@38: (ECAbs (x, k', e'), loc))) adamc@38: adamc@38: | ERecord xes => adamc@38: S.map2 (ListUtil.mapfold (fn (x, e, t) => adamc@38: S.bind2 (mfc ctx x, adamc@38: fn x' => adamc@38: S.bind2 (mfe ctx e, adamc@38: fn e' => adamc@38: S.map2 (mfc ctx t, adamc@38: fn t' => adamc@38: (x', e', t'))))) adamc@38: xes, adamc@38: fn xes' => adamc@38: (ERecord xes', loc)) adamc@38: | EField (e, c, {field, rest}) => adamc@38: S.bind2 (mfe ctx e, adamc@38: fn e' => adamc@38: S.bind2 (mfc ctx c, adamc@38: fn c' => adamc@38: S.bind2 (mfc ctx field, adamc@38: fn field' => adamc@38: S.map2 (mfc ctx rest, adamc@38: fn rest' => adamc@38: (EField (e', c', {field = field', rest = rest'}), loc))))) adamc@445: | EConcat (e1, c1, e2, c2) => adamc@339: S.bind2 (mfe ctx e1, adamc@339: fn e1' => adamc@445: S.bind2 (mfc ctx c1, adamc@445: fn c1' => adamc@339: S.bind2 (mfe ctx e2, adamc@339: fn e2' => adamc@445: S.map2 (mfc ctx c2, adamc@445: fn c2' => adamc@445: (EConcat (e1', c1', e2', c2'), adamc@445: 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@493: | ECutMulti (e, c, {rest}) => adamc@493: S.bind2 (mfe ctx e, adamc@493: fn e' => adamc@493: S.bind2 (mfc ctx c, adamc@493: fn c' => adamc@493: S.map2 (mfc ctx rest, adamc@493: fn rest' => adamc@493: (ECutMulti (e', c', {rest = rest'}), loc)))) adamc@109: adamc@109: | EWrite e => adamc@109: S.map2 (mfe ctx e, adamc@109: fn e' => adamc@109: (EWrite e', loc)) adamc@176: adamc@182: | ECase (e, pes, {disc, result}) => adamc@176: S.bind2 (mfe ctx e, adamc@176: fn e' => adamc@176: S.bind2 (ListUtil.mapfold (fn (p, e) => adamc@176: S.map2 (mfe ctx e, adamc@176: fn e' => (p, e'))) pes, adamc@176: 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@449: adamc@449: | ELet (x, t, e1, e2) => adamc@449: S.bind2 (mfc ctx t, adamc@449: fn t' => adamc@449: S.bind2 (mfe ctx e1, adamc@449: fn e1' => adamc@453: S.map2 (mfe (bind (ctx, RelE (x, t))) e2, adamc@449: fn e2' => adamc@449: (ELet (x, t', e1', e2'), loc)))) adamc@624: adamc@624: | EKAbs (x, e) => adamc@624: S.map2 (mfe (bind (ctx, RelK x)) e, adamc@624: fn e' => adamc@624: (EKAbs (x, e'), loc)) adamc@624: | EKApp (e, k) => adamc@624: S.bind2 (mfe ctx e, adamc@624: fn e' => adamc@624: S.map2 (mfk ctx k, adamc@624: fn k' => adamc@624: (EKApp (e', k'), loc))) adamc@38: in adamc@38: mfe adamc@38: end adamc@38: adamc@38: fun mapfold {kind = fk, con = fc, exp = fe} = adamc@624: mapfoldB {kind = fn () => fk, adamc@38: con = fn () => fc, adamc@38: exp = fn () => fe, adamc@38: bind = fn ((), _) => ()} () adamc@38: adamc@38: fun exists {kind, con, exp} k = adamc@38: case mapfold {kind = fn k => fn () => adamc@38: if kind k then adamc@38: S.Return () adamc@38: else adamc@38: S.Continue (k, ()), adamc@38: con = fn c => fn () => adamc@38: if con c then adamc@38: S.Return () adamc@38: else adamc@38: S.Continue (c, ()), adamc@38: exp = fn e => fn () => adamc@38: if exp e then adamc@38: S.Return () adamc@38: else adamc@38: S.Continue (e, ())} k () of adamc@38: S.Return _ => true adamc@38: | S.Continue _ => false adamc@38: adamc@38: end adamc@38: adamc@38: structure Sgn = struct adamc@38: adamc@38: datatype binder = adamc@624: RelK of string adamc@624: | RelC of string * Expl.kind adamc@38: | NamedC of string * Expl.kind adamc@38: | Str of string * Expl.sgn adamc@64: | Sgn of string * Expl.sgn adamc@38: adamc@38: fun mapfoldB {kind, con, sgn_item, sgn, bind} = adamc@38: let adamc@38: fun bind' (ctx, b) = adamc@38: let adamc@38: val b' = case b of adamc@624: Con.RelK x => RelK x adamc@624: | Con.RelC x => RelC x adamc@624: | Con.NamedC x => NamedC x adamc@38: in adamc@38: bind (ctx, b') adamc@38: end adamc@38: val con = Con.mapfoldB {kind = kind, con = con, bind = bind'} adamc@38: adamc@624: val kind = Kind.mapfoldB {kind = kind, bind = fn (ctx, x) => bind (ctx, RelK x)} adamc@38: adamc@38: fun sgi ctx si acc = adamc@38: S.bindP (sgi' ctx si acc, sgn_item ctx) adamc@38: adamc@162: and sgi' ctx (siAll as (si, loc)) = adamc@38: case si of adamc@38: SgiConAbs (x, n, k) => adamc@624: S.map2 (kind ctx k, adamc@38: fn k' => adamc@38: (SgiConAbs (x, n, k'), loc)) adamc@38: | SgiCon (x, n, k, c) => adamc@624: S.bind2 (kind ctx k, adamc@38: fn k' => adamc@38: S.map2 (con ctx c, adamc@38: fn c' => adamc@38: (SgiCon (x, n, k', c'), loc))) adamc@191: | SgiDatatype (x, n, xs, xncs) => adamc@162: S.map2 (ListUtil.mapfold (fn (x, n, c) => adamc@162: case c of adamc@162: NONE => S.return2 (x, n, c) adamc@162: | SOME c => adamc@162: S.map2 (con ctx c, adamc@162: fn c' => (x, n, SOME c'))) xncs, adamc@162: fn xncs' => adamc@191: (SgiDatatype (x, n, xs, xncs'), loc)) adamc@191: | SgiDatatypeImp (x, n, m1, ms, s, xs, xncs) => adamc@162: S.map2 (ListUtil.mapfold (fn (x, n, c) => adamc@162: case c of adamc@162: NONE => S.return2 (x, n, c) adamc@162: | SOME c => adamc@162: S.map2 (con ctx c, adamc@162: fn c' => (x, n, SOME c'))) xncs, adamc@162: fn xncs' => adamc@191: (SgiDatatypeImp (x, n, m1, ms, s, xs, xncs'), loc)) adamc@38: | SgiVal (x, n, c) => adamc@38: S.map2 (con ctx c, adamc@38: fn c' => adamc@38: (SgiVal (x, n, c'), loc)) adamc@38: | SgiStr (x, n, s) => adamc@38: S.map2 (sg ctx s, adamc@38: fn s' => adamc@38: (SgiStr (x, n, s'), loc)) adamc@64: | SgiSgn (x, n, s) => adamc@64: S.map2 (sg ctx s, adamc@64: fn s' => adamc@64: (SgiSgn (x, n, s'), loc)) adamc@38: adamc@38: and sg ctx s acc = adamc@38: S.bindP (sg' ctx s acc, sgn ctx) adamc@38: adamc@38: and sg' ctx (sAll as (s, loc)) = adamc@38: case s of adamc@38: SgnConst sgis => adamc@38: S.map2 (ListUtil.mapfoldB (fn (ctx, si) => adamc@38: (case #1 si of adamc@38: SgiConAbs (x, _, k) => adamc@38: bind (ctx, NamedC (x, k)) adamc@38: | SgiCon (x, _, k, _) => adamc@38: bind (ctx, NamedC (x, k)) adamc@191: | SgiDatatype (x, n, _, xncs) => adamc@162: bind (ctx, NamedC (x, (KType, loc))) adamc@191: | SgiDatatypeImp (x, _, _, _, _, _, _) => adamc@162: bind (ctx, NamedC (x, (KType, loc))) adamc@38: | SgiVal _ => ctx adamc@38: | SgiStr (x, _, sgn) => adamc@64: bind (ctx, Str (x, sgn)) adamc@64: | SgiSgn (x, _, sgn) => adamc@460: bind (ctx, Sgn (x, sgn)), adamc@38: sgi ctx si)) ctx sgis, adamc@38: fn sgis' => adamc@38: (SgnConst sgis', loc)) adamc@38: adamc@38: | SgnVar _ => S.return2 sAll adamc@45: adamc@45: | SgnFun (m, n, s1, s2) => adamc@45: S.bind2 (sg ctx s1, adamc@45: fn s1' => adamc@45: S.map2 (sg (bind (ctx, Str (m, s1'))) s2, adamc@45: fn s2' => adamc@45: (SgnFun (m, n, s1', s2'), loc))) adamc@45: | SgnWhere (sgn, x, c) => adamc@45: S.bind2 (sg ctx sgn, adamc@45: fn sgn' => adamc@45: S.map2 (con ctx c, adamc@45: fn c' => adamc@45: (SgnWhere (sgn', x, c'), loc))) adamc@64: | SgnProj _ => S.return2 sAll adamc@38: in adamc@38: sg adamc@38: end adamc@38: adamc@38: fun mapfold {kind, con, sgn_item, sgn} = adamc@624: mapfoldB {kind = fn () => kind, adamc@38: con = fn () => con, adamc@38: sgn_item = fn () => sgn_item, adamc@38: sgn = fn () => sgn, adamc@38: bind = fn ((), _) => ()} () adamc@38: adamc@38: fun map {kind, con, sgn_item, sgn} s = adamc@38: case mapfold {kind = fn k => fn () => S.Continue (kind k, ()), adamc@38: con = fn c => fn () => S.Continue (con c, ()), adamc@38: sgn_item = fn si => fn () => S.Continue (sgn_item si, ()), adamc@38: sgn = fn s => fn () => S.Continue (sgn s, ())} s () of adamc@38: S.Return () => raise Fail "Expl_util.Sgn.map" adamc@38: | S.Continue (s, ()) => s adamc@38: adamc@38: end adamc@38: adamc@38: end