adamc@2: (* Copyright (c) 2008, Adam Chlipala adamc@2: * All rights reserved. adamc@2: * adamc@2: * Redistribution and use in source and binary forms, with or without adamc@2: * modification, are permitted provided that the following conditions are met: adamc@2: * adamc@2: * - Redistributions of source code must retain the above copyright notice, adamc@2: * this list of conditions and the following disclaimer. adamc@2: * - Redistributions in binary form must reproduce the above copyright notice, adamc@2: * this list of conditions and the following disclaimer in the documentation adamc@2: * and/or other materials provided with the distribution. adamc@2: * - The names of contributors may not be used to endorse or promote products adamc@2: * derived from this software without specific prior written permission. adamc@2: * adamc@2: * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" adamc@2: * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE adamc@2: * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE adamc@2: * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE adamc@2: * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR adamc@2: * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF adamc@2: * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS adamc@2: * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN adamc@2: * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) adamc@2: * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE adamc@2: * POSSIBILITY OF SUCH DAMAGE. adamc@2: *) adamc@2: adamc@2: structure ElabUtil :> ELAB_UTIL = struct adamc@2: adamc@2: open Elab adamc@2: adamc@188: fun classifyDatatype xncs = adamc@198: case xncs of adamc@198: [(_, _, NONE), (_, _, SOME _)] => Option adamc@198: | [(_, _, SOME _), (_, _, NONE)] => Option adamc@198: | _ => adamc@198: if List.all (fn (_, _, NONE) => true | _ => false) xncs then adamc@198: Enum adamc@198: else adamc@198: Default adamc@188: adamc@2: structure S = Search adamc@2: adamc@2: structure Kind = struct adamc@2: adamc@6: fun mapfold f = adamc@2: let adamc@2: fun mfk k acc = adamc@2: S.bindP (mfk' k acc, f) adamc@2: adamc@2: and mfk' (kAll as (k, loc)) = adamc@2: case k of adamc@2: KType => S.return2 kAll adamc@2: adamc@2: | KArrow (k1, k2) => adamc@2: S.bind2 (mfk k1, adamc@2: fn k1' => adamc@2: S.map2 (mfk k2, adamc@2: fn k2' => adamc@2: (KArrow (k1', k2'), loc))) adamc@2: adamc@2: | KName => S.return2 kAll adamc@2: adamc@2: | KRecord k => adamc@2: S.map2 (mfk k, adamc@2: fn k' => adamc@2: (KRecord k', loc)) adamc@2: adamc@82: | KUnit => S.return2 kAll adamc@82: adamc@207: | KTuple ks => adamc@207: S.map2 (ListUtil.mapfold mfk ks, adamc@207: fn ks' => adamc@207: (KTuple ks', loc)) adamc@207: adamc@2: | KError => S.return2 kAll adamc@2: adamc@76: | KUnif (_, _, ref (SOME k)) => mfk' k adamc@2: | KUnif _ => S.return2 kAll adamc@2: in adamc@2: mfk adamc@2: end adamc@2: adamc@2: fun exists f k = adamc@6: case mapfold (fn k => fn () => adamc@6: if f k then adamc@6: S.Return () adamc@6: else adamc@6: S.Continue (k, ())) k () of adamc@6: S.Return _ => true adamc@6: | S.Continue _ => false adamc@6: adamc@6: end adamc@6: adamc@6: structure Con = struct adamc@6: adamc@11: datatype binder = adamc@11: Rel of string * Elab.kind adamc@329: | Named of string * int * Elab.kind adamc@11: adamc@11: fun mapfoldB {kind = fk, con = fc, bind} = adamc@6: let adamc@6: val mfk = Kind.mapfold fk adamc@6: adamc@11: fun mfc ctx c acc = adamc@11: S.bindP (mfc' ctx c acc, fc ctx) adamc@6: adamc@11: and mfc' ctx (cAll as (c, loc)) = adamc@6: case c of adamc@6: TFun (c1, c2) => adamc@11: S.bind2 (mfc ctx c1, adamc@6: fn c1' => adamc@11: S.map2 (mfc ctx c2, adamc@6: fn c2' => adamc@6: (TFun (c1', c2'), loc))) adamc@6: | TCFun (e, x, k, c) => adamc@6: S.bind2 (mfk k, adamc@6: fn k' => adamc@11: S.map2 (mfc (bind (ctx, Rel (x, k))) c, adamc@6: fn c' => adamc@6: (TCFun (e, x, k', c'), loc))) adamc@345: | CDisjoint (ai, c1, c2, c3) => adamc@85: S.bind2 (mfc ctx c1, adamc@85: fn c1' => adamc@85: S.bind2 (mfc ctx c2, adamc@85: fn c2' => adamc@85: S.map2 (mfc ctx c3, adamc@85: fn c3' => adamc@345: (CDisjoint (ai, c1', c2', c3'), loc)))) adamc@6: | TRecord c => adamc@11: S.map2 (mfc ctx c, adamc@6: fn c' => adamc@6: (TRecord c', loc)) adamc@6: adamc@6: | CRel _ => S.return2 cAll adamc@6: | CNamed _ => S.return2 cAll adamc@34: | CModProj _ => S.return2 cAll adamc@6: | CApp (c1, c2) => adamc@11: S.bind2 (mfc ctx c1, adamc@6: fn c1' => adamc@11: S.map2 (mfc ctx c2, adamc@6: fn c2' => adamc@6: (CApp (c1', c2'), loc))) adamc@8: | CAbs (x, k, c) => adamc@6: S.bind2 (mfk k, adamc@6: fn k' => adamc@11: S.map2 (mfc (bind (ctx, Rel (x, k))) c, adamc@6: fn c' => adamc@8: (CAbs (x, k', c'), loc))) adamc@6: adamc@6: | CName _ => S.return2 cAll adamc@6: adamc@6: | CRecord (k, xcs) => adamc@6: S.bind2 (mfk k, adamc@6: fn k' => adamc@6: S.map2 (ListUtil.mapfold (fn (x, c) => adamc@11: S.bind2 (mfc ctx x, adamc@6: fn x' => adamc@11: S.map2 (mfc ctx c, adamc@6: fn c' => adamc@6: (x', c')))) adamc@6: xcs, adamc@6: fn xcs' => adamc@6: (CRecord (k', xcs'), loc))) adamc@6: | CConcat (c1, c2) => adamc@11: S.bind2 (mfc ctx c1, adamc@6: fn c1' => adamc@11: S.map2 (mfc ctx c2, adamc@6: fn c2' => adamc@6: (CConcat (c1', c2'), loc))) adamc@621: | CMap (k1, k2) => adamc@67: S.bind2 (mfk k1, adamc@67: fn k1' => adamc@67: S.map2 (mfk k2, adamc@67: fn k2' => adamc@621: (CMap (k1', k2'), loc))) adamc@6: adamc@82: | CUnit => S.return2 cAll adamc@82: adamc@207: | CTuple cs => adamc@207: S.map2 (ListUtil.mapfold (mfc ctx) cs, adamc@207: fn cs' => adamc@207: (CTuple cs', loc)) adamc@207: adamc@207: | CProj (c, n) => adamc@207: S.map2 (mfc ctx c, adamc@207: fn c' => adamc@207: (CProj (c', n), loc)) adamc@207: adamc@6: | CError => S.return2 cAll adamc@76: | CUnif (_, _, _, ref (SOME c)) => mfc' ctx c adamc@6: | CUnif _ => S.return2 cAll adamc@6: in adamc@6: mfc adamc@6: end adamc@6: adamc@11: fun mapfold {kind = fk, con = fc} = adamc@11: mapfoldB {kind = fk, adamc@11: con = fn () => fc, adamc@11: bind = fn ((), _) => ()} () adamc@11: adamc@11: fun mapB {kind, con, bind} ctx c = adamc@11: case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()), adamc@11: con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()), adamc@11: bind = bind} ctx c () of adamc@11: S.Continue (c, ()) => c adamc@34: | S.Return _ => raise Fail "ElabUtil.Con.mapB: Impossible" adamc@34: adamc@34: fun map {kind, con} s = adamc@34: case mapfold {kind = fn k => fn () => S.Continue (kind k, ()), adamc@34: con = fn c => fn () => S.Continue (con c, ())} s () of adamc@34: S.Return () => raise Fail "ElabUtil.Con.map: Impossible" adamc@34: | S.Continue (s, ()) => s adamc@11: adamc@6: fun exists {kind, con} k = adamc@6: case mapfold {kind = fn k => fn () => adamc@6: if kind k then adamc@6: S.Return () adamc@6: else adamc@6: S.Continue (k, ()), adamc@6: con = fn c => fn () => adamc@6: if con c then adamc@6: S.Return () adamc@6: else adamc@6: S.Continue (c, ())} k () of adamc@2: S.Return _ => true adamc@2: | S.Continue _ => false adamc@2: adamc@448: fun foldB {kind, con, bind} ctx st c = adamc@448: case mapfoldB {kind = fn k => fn st => S.Continue (k, kind (k, st)), adamc@448: con = fn ctx => fn c => fn st => S.Continue (c, con (ctx, c, st)), adamc@448: bind = bind} ctx c st of adamc@448: S.Continue (_, st) => st adamc@448: | S.Return _ => raise Fail "ElabUtil.Con.foldB: Impossible" adamc@448: adamc@2: end adamc@2: adamc@10: structure Exp = struct adamc@10: adamc@11: datatype binder = adamc@11: RelC of string * Elab.kind adamc@329: | NamedC of string * int * Elab.kind adamc@11: | RelE of string * Elab.con adamc@11: | NamedE of string * Elab.con adamc@11: adamc@11: fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = adamc@10: let adamc@10: val mfk = Kind.mapfold fk adamc@10: adamc@11: fun bind' (ctx, b) = adamc@11: let adamc@11: val b' = case b of adamc@11: Con.Rel x => RelC x adamc@11: | Con.Named x => NamedC x adamc@11: in adamc@11: bind (ctx, b') adamc@11: end adamc@11: val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'} adamc@10: adamc@11: fun mfe ctx e acc = adamc@11: S.bindP (mfe' ctx e acc, fe ctx) adamc@11: adamc@11: and mfe' ctx (eAll as (e, loc)) = adamc@10: case e of adamc@14: EPrim _ => S.return2 eAll adamc@14: | ERel _ => S.return2 eAll adamc@10: | ENamed _ => S.return2 eAll adamc@34: | EModProj _ => S.return2 eAll adamc@10: | EApp (e1, e2) => adamc@11: S.bind2 (mfe ctx e1, adamc@10: fn e1' => adamc@11: S.map2 (mfe ctx e2, adamc@10: fn e2' => adamc@10: (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@26: adamc@10: | ECApp (e, c) => adamc@11: S.bind2 (mfe ctx e, adamc@10: fn e' => adamc@11: S.map2 (mfc ctx c, adamc@10: fn c' => adamc@10: (ECApp (e', c'), loc))) adamc@10: | ECAbs (expl, x, k, e) => adamc@10: S.bind2 (mfk k, adamc@10: fn k' => adamc@11: S.map2 (mfe (bind (ctx, RelC (x, k))) e, adamc@10: fn e' => adamc@10: (ECAbs (expl, x, k', e'), loc))) adamc@10: adamc@12: | ERecord xes => adamc@29: S.map2 (ListUtil.mapfold (fn (x, e, t) => adamc@12: S.bind2 (mfc ctx x, adamc@12: fn x' => adamc@29: S.bind2 (mfe ctx e, adamc@12: fn e' => adamc@29: S.map2 (mfc ctx t, adamc@29: fn t' => adamc@29: (x', e', t'))))) adamc@12: xes, adamc@12: fn xes' => adamc@12: (ERecord xes', loc)) adamc@12: | EField (e, c, {field, rest}) => adamc@12: S.bind2 (mfe ctx e, adamc@12: fn e' => adamc@12: S.bind2 (mfc ctx c, adamc@12: fn c' => adamc@12: S.bind2 (mfc ctx field, adamc@12: fn field' => adamc@12: S.map2 (mfc ctx rest, adamc@12: fn rest' => adamc@12: (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@12: 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@493: adamc@71: | EFold k => adamc@71: S.map2 (mfk k, adamc@71: fn k' => adamc@71: (EFold k', loc)) adamc@71: adamc@182: | ECase (e, pes, {disc, result}) => adamc@171: S.bind2 (mfe ctx e, adamc@171: fn e' => adamc@171: S.bind2 (ListUtil.mapfold (fn (p, e) => adamc@448: let adamc@448: fun pb ((p, _), ctx) = adamc@448: case p of adamc@448: PWild => ctx adamc@448: | PVar (x, t) => bind (ctx, RelE (x, t)) adamc@448: | PPrim _ => ctx adamc@448: | PCon (_, _, _, NONE) => ctx adamc@448: | PCon (_, _, _, SOME p) => pb (p, ctx) adamc@448: | PRecord xps => foldl (fn ((_, p, _), ctx) => adamc@448: pb (p, ctx)) ctx xps adamc@448: in adamc@448: S.map2 (mfe (pb (p, ctx)) e, adamc@448: fn e' => (p, e')) adamc@448: end) pes, adamc@171: 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@171: adamc@10: | EError => S.return2 eAll adamc@228: | EUnif (ref (SOME e)) => mfe ctx e adamc@228: | EUnif _ => S.return2 eAll adamc@447: adamc@447: | ELet (des, e) => adamc@447: let adamc@447: val (des, ctx) = foldl (fn (ed, (des, ctx)) => adamc@453: let adamc@453: val ctx' = adamc@453: case #1 ed of adamc@453: EDVal (x, t, _) => bind (ctx, RelE (x, t)) adamc@453: | EDValRec vis => adamc@453: foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t))) ctx vis adamc@453: in adamc@453: (S.bind2 (des, adamc@453: fn des' => adamc@453: S.map2 (mfed ctx ed, adamc@447: fn ed' => des' @ [ed'])), adamc@453: ctx') adamc@453: end) adamc@447: (S.return2 [], ctx) des adamc@447: in adamc@447: S.bind2 (des, adamc@447: fn des' => adamc@447: S.map2 (mfe ctx e, adamc@447: fn e' => adamc@447: (ELet (des', e'), loc))) adamc@447: end adamc@447: adamc@447: and mfed ctx (dAll as (d, loc)) = adamc@447: case d of adamc@447: EDVal vi => adamc@447: S.map2 (mfvi ctx vi, adamc@447: fn vi' => adamc@447: (EDVal vi', loc)) adamc@447: | EDValRec vis => adamc@447: let adamc@453: val ctx = foldl (fn ((x, t, _), ctx) => bind (ctx, RelE (x, t))) ctx vis adamc@447: in adamc@447: S.map2 (ListUtil.mapfold (mfvi ctx) vis, adamc@447: fn vis' => adamc@447: (EDValRec vis', loc)) adamc@447: end adamc@447: adamc@447: and mfvi ctx (x, c, e) = adamc@447: S.bind2 (mfc ctx c, adamc@447: fn c' => adamc@447: S.map2 (mfe ctx e, adamc@447: fn e' => adamc@447: (x, c', e'))) adamc@10: in adamc@10: mfe adamc@10: end adamc@10: adamc@11: fun mapfold {kind = fk, con = fc, exp = fe} = adamc@11: mapfoldB {kind = fk, adamc@11: con = fn () => fc, adamc@11: exp = fn () => fe, adamc@11: bind = fn ((), _) => ()} () adamc@11: adamc@10: fun exists {kind, con, exp} k = adamc@10: case mapfold {kind = fn k => fn () => adamc@10: if kind k then adamc@10: S.Return () adamc@10: else adamc@10: S.Continue (k, ()), adamc@10: con = fn c => fn () => adamc@10: if con c then adamc@10: S.Return () adamc@10: else adamc@10: S.Continue (c, ()), adamc@10: exp = fn e => fn () => adamc@10: if exp e then adamc@10: S.Return () adamc@10: else adamc@10: S.Continue (e, ())} k () of adamc@10: S.Return _ => true adamc@10: | S.Continue _ => false adamc@10: adamc@211: fun mapB {kind, con, exp, bind} ctx e = adamc@211: case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()), adamc@211: con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()), adamc@211: exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()), adamc@211: bind = bind} ctx e () of adamc@211: S.Continue (e, ()) => e adamc@211: | S.Return _ => raise Fail "ElabUtil.Exp.mapB: Impossible" adamc@211: adamc@448: fun foldB {kind, con, exp, bind} ctx st e = adamc@448: case mapfoldB {kind = fn k => fn st => S.Continue (k, kind (k, st)), adamc@448: con = fn ctx => fn c => fn st => S.Continue (c, con (ctx, c, st)), adamc@448: exp = fn ctx => fn e => fn st => S.Continue (e, exp (ctx, e, st)), adamc@448: bind = bind} ctx e st of adamc@448: S.Continue (_, st) => st adamc@448: | S.Return _ => raise Fail "ElabUtil.Exp.foldB: Impossible" adamc@448: adamc@10: end adamc@10: adamc@34: structure Sgn = struct adamc@34: adamc@34: datatype binder = adamc@34: RelC of string * Elab.kind adamc@329: | NamedC of string * int * Elab.kind adamc@34: | Str of string * Elab.sgn adamc@59: | Sgn of string * Elab.sgn adamc@34: adamc@34: fun mapfoldB {kind, con, sgn_item, sgn, bind} = adamc@34: let adamc@34: fun bind' (ctx, b) = adamc@34: let adamc@34: val b' = case b of adamc@34: Con.Rel x => RelC x adamc@34: | Con.Named x => NamedC x adamc@34: in adamc@34: bind (ctx, b') adamc@34: end adamc@34: val con = Con.mapfoldB {kind = kind, con = con, bind = bind'} adamc@34: adamc@34: val kind = Kind.mapfold kind adamc@34: adamc@34: fun sgi ctx si acc = adamc@34: S.bindP (sgi' ctx si acc, sgn_item ctx) adamc@34: adamc@156: and sgi' ctx (siAll as (si, loc)) = adamc@34: case si of adamc@34: SgiConAbs (x, n, k) => adamc@34: S.map2 (kind k, adamc@34: fn k' => adamc@34: (SgiConAbs (x, n, k'), loc)) adamc@34: | SgiCon (x, n, k, c) => adamc@34: S.bind2 (kind k, adamc@34: fn k' => adamc@34: S.map2 (con ctx c, adamc@34: fn c' => adamc@34: (SgiCon (x, n, k', c'), loc))) adamc@191: | SgiDatatype (x, n, xs, xncs) => adamc@156: S.map2 (ListUtil.mapfold (fn (x, n, c) => adamc@156: case c of adamc@156: NONE => S.return2 (x, n, c) adamc@156: | SOME c => adamc@156: S.map2 (con ctx c, adamc@156: fn c' => (x, n, SOME c'))) xncs, adamc@156: 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@34: | SgiVal (x, n, c) => adamc@34: S.map2 (con ctx c, adamc@34: fn c' => adamc@34: (SgiVal (x, n, c'), loc)) adamc@34: | SgiStr (x, n, s) => adamc@34: S.map2 (sg ctx s, adamc@34: fn s' => adamc@34: (SgiStr (x, n, s'), loc)) adamc@59: | SgiSgn (x, n, s) => adamc@59: S.map2 (sg ctx s, adamc@59: fn s' => adamc@59: (SgiSgn (x, n, s'), loc)) adamc@88: | SgiConstraint (c1, c2) => adamc@88: S.bind2 (con ctx c1, adamc@88: fn c1' => adamc@88: S.map2 (con ctx c2, adamc@88: fn c2' => adamc@88: (SgiConstraint (c1', c2'), loc))) adamc@563: | SgiClassAbs (x, n, k) => adamc@563: S.map2 (kind k, adamc@563: fn k' => adamc@563: (SgiClassAbs (x, n, k'), loc)) adamc@563: | SgiClass (x, n, k, c) => adamc@563: S.bind2 (kind k, adamc@563: fn k' => adamc@563: S.map2 (con ctx c, adamc@563: fn c' => adamc@563: (SgiClass (x, n, k', c'), loc))) adamc@34: adamc@34: and sg ctx s acc = adamc@34: S.bindP (sg' ctx s acc, sgn ctx) adamc@34: adamc@34: and sg' ctx (sAll as (s, loc)) = adamc@34: case s of adamc@34: SgnConst sgis => adamc@34: S.map2 (ListUtil.mapfoldB (fn (ctx, si) => adamc@34: (case #1 si of adamc@329: SgiConAbs (x, n, k) => adamc@329: bind (ctx, NamedC (x, n, k)) adamc@329: | SgiCon (x, n, k, _) => adamc@329: bind (ctx, NamedC (x, n, k)) adamc@191: | SgiDatatype (x, n, _, xncs) => adamc@329: bind (ctx, NamedC (x, n, (KType, loc))) adamc@329: | SgiDatatypeImp (x, n, _, _, _, _, _) => adamc@329: bind (ctx, NamedC (x, n, (KType, loc))) adamc@34: | SgiVal _ => ctx adamc@34: | SgiStr (x, _, sgn) => adamc@59: bind (ctx, Str (x, sgn)) adamc@59: | SgiSgn (x, _, sgn) => adamc@88: bind (ctx, Sgn (x, sgn)) adamc@203: | SgiConstraint _ => ctx adamc@563: | SgiClassAbs (x, n, k) => adamc@563: bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc))) adamc@563: | SgiClass (x, n, k, _) => adamc@563: bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc))), adamc@34: sgi ctx si)) ctx sgis, adamc@34: fn sgis' => adamc@34: (SgnConst sgis', loc)) adamc@34: adamc@34: | SgnVar _ => S.return2 sAll adamc@41: | SgnFun (m, n, s1, s2) => adamc@41: S.bind2 (sg ctx s1, adamc@41: fn s1' => adamc@41: S.map2 (sg (bind (ctx, Str (m, s1'))) s2, adamc@41: fn s2' => adamc@41: (SgnFun (m, n, s1', s2'), loc))) adamc@59: | SgnProj _ => S.return2 sAll adamc@42: | SgnWhere (sgn, x, c) => adamc@42: S.bind2 (sg ctx sgn, adamc@42: fn sgn' => adamc@42: S.map2 (con ctx c, adamc@42: fn c' => adamc@42: (SgnWhere (sgn', x, c'), loc))) adamc@34: | SgnError => S.return2 sAll adamc@34: in adamc@34: sg adamc@34: end adamc@34: adamc@34: fun mapfold {kind, con, sgn_item, sgn} = adamc@34: mapfoldB {kind = kind, adamc@34: con = fn () => con, adamc@34: sgn_item = fn () => sgn_item, adamc@34: sgn = fn () => sgn, adamc@34: bind = fn ((), _) => ()} () adamc@34: adamc@34: fun map {kind, con, sgn_item, sgn} s = adamc@34: case mapfold {kind = fn k => fn () => S.Continue (kind k, ()), adamc@34: con = fn c => fn () => S.Continue (con c, ()), adamc@34: sgn_item = fn si => fn () => S.Continue (sgn_item si, ()), adamc@34: sgn = fn s => fn () => S.Continue (sgn s, ())} s () of adamc@34: S.Return () => raise Fail "Elab_util.Sgn.map" adamc@34: | S.Continue (s, ()) => s adamc@34: adamc@2: end adamc@34: adamc@76: structure Decl = struct adamc@76: adamc@76: datatype binder = adamc@76: RelC of string * Elab.kind adamc@329: | NamedC of string * int * Elab.kind adamc@76: | RelE of string * Elab.con adamc@76: | NamedE of string * Elab.con adamc@76: | Str of string * Elab.sgn adamc@76: | Sgn of string * Elab.sgn adamc@76: adamc@76: fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = fst, decl = fd, bind} = adamc@76: let adamc@76: val mfk = Kind.mapfold fk adamc@76: adamc@76: fun bind' (ctx, b) = adamc@76: let adamc@76: val b' = case b of adamc@76: Con.Rel x => RelC x adamc@76: | Con.Named x => NamedC x adamc@76: in adamc@76: bind (ctx, b') adamc@76: end adamc@76: val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'} adamc@76: adamc@76: fun bind' (ctx, b) = adamc@76: let adamc@76: val b' = case b of adamc@76: Exp.RelC x => RelC x adamc@76: | Exp.NamedC x => NamedC x adamc@76: | Exp.RelE x => RelE x adamc@76: | Exp.NamedE x => NamedE x adamc@76: in adamc@76: bind (ctx, b') adamc@76: end adamc@76: val mfe = Exp.mapfoldB {kind = fk, con = fc, exp = fe, bind = bind'} adamc@76: adamc@76: fun bind' (ctx, b) = adamc@76: let adamc@76: val b' = case b of adamc@76: Sgn.RelC x => RelC x adamc@76: | Sgn.NamedC x => NamedC x adamc@76: | Sgn.Sgn x => Sgn x adamc@76: | Sgn.Str x => Str x adamc@76: in adamc@76: bind (ctx, b') adamc@76: end adamc@76: val mfsg = Sgn.mapfoldB {kind = fk, con = fc, sgn_item = fsgi, sgn = fsg, bind = bind'} adamc@76: adamc@76: fun mfst ctx str acc = adamc@76: S.bindP (mfst' ctx str acc, fst ctx) adamc@76: adamc@76: and mfst' ctx (strAll as (str, loc)) = adamc@76: case str of adamc@76: StrConst ds => adamc@76: S.map2 (ListUtil.mapfoldB (fn (ctx, d) => adamc@76: (case #1 d of adamc@329: DCon (x, n, k, _) => adamc@329: bind (ctx, NamedC (x, n, k)) adamc@191: | DDatatype (x, n, xs, xncs) => adamc@156: let adamc@329: val ctx = bind (ctx, NamedC (x, n, (KType, loc))) adamc@156: in adamc@156: foldl (fn ((x, _, co), ctx) => adamc@156: let adamc@156: val t = adamc@156: case co of adamc@156: NONE => CNamed n adamc@156: | SOME t => TFun (t, (CNamed n, loc)) adamc@191: adamc@191: val k = (KType, loc) adamc@191: val t = (t, loc) adamc@191: val t = foldr (fn (x, t) => adamc@191: (TCFun (Explicit, adamc@191: x, adamc@191: k, adamc@191: t), loc)) adamc@191: t xs adamc@156: in adamc@191: bind (ctx, NamedE (x, t)) adamc@156: end) adamc@156: ctx xncs adamc@156: end adamc@191: | DDatatypeImp (x, n, m, ms, x', _, _) => adamc@329: bind (ctx, NamedC (x, n, (KType, loc))) adamc@76: | DVal (x, _, c, _) => adamc@76: bind (ctx, NamedE (x, c)) adamc@123: | DValRec vis => adamc@123: foldl (fn ((x, _, c, _), ctx) => bind (ctx, NamedE (x, c))) ctx vis adamc@76: | DSgn (x, _, sgn) => adamc@76: bind (ctx, Sgn (x, sgn)) adamc@76: | DStr (x, _, sgn, _) => adamc@76: bind (ctx, Str (x, sgn)) adamc@76: | DFfiStr (x, _, sgn) => adamc@88: bind (ctx, Str (x, sgn)) adamc@100: | DConstraint _ => ctx adamc@203: | DExport _ => ctx adamc@205: | DTable (tn, x, n, c) => adamc@338: bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "sql_table"), loc), adamc@213: c), loc))) adamc@338: | DSequence (tn, x, n) => adamc@338: bind (ctx, NamedE (x, (CModProj (n, [], "sql_sequence"), loc))) adamc@563: | DClass (x, n, k, _) => adamc@563: bind (ctx, NamedC (x, n, (KArrow (k, (KType, loc)), loc))) adamc@459: | DDatabase _ => ctx adamc@459: | DCookie (tn, x, n, c) => adamc@459: bind (ctx, NamedE (x, (CApp ((CModProj (n, [], "cookie"), loc), adamc@459: c), loc))), adamc@76: mfd ctx d)) ctx ds, adamc@76: fn ds' => (StrConst ds', loc)) adamc@76: | StrVar _ => S.return2 strAll adamc@76: | StrProj (str, x) => adamc@76: S.map2 (mfst ctx str, adamc@76: fn str' => adamc@76: (StrProj (str', x), loc)) adamc@76: | StrFun (x, n, sgn1, sgn2, str) => adamc@76: S.bind2 (mfsg ctx sgn1, adamc@76: fn sgn1' => adamc@76: S.bind2 (mfsg ctx sgn2, adamc@76: fn sgn2' => adamc@76: S.map2 (mfst ctx str, adamc@76: fn str' => adamc@76: (StrFun (x, n, sgn1', sgn2', str'), loc)))) adamc@76: | StrApp (str1, str2) => adamc@76: S.bind2 (mfst ctx str1, adamc@76: fn str1' => adamc@76: S.map2 (mfst ctx str2, adamc@76: fn str2' => adamc@76: (StrApp (str1', str2'), loc))) adamc@76: | StrError => S.return2 strAll adamc@76: adamc@76: and mfd ctx d acc = adamc@76: S.bindP (mfd' ctx d acc, fd ctx) adamc@76: adamc@76: and mfd' ctx (dAll as (d, loc)) = adamc@76: case d of adamc@76: DCon (x, n, k, c) => adamc@76: S.bind2 (mfk k, adamc@76: fn k' => adamc@76: S.map2 (mfc ctx c, adamc@76: fn c' => adamc@76: (DCon (x, n, k', c'), loc))) adamc@191: | DDatatype (x, n, xs, xncs) => adamc@156: S.map2 (ListUtil.mapfold (fn (x, n, c) => adamc@156: case c of adamc@156: NONE => S.return2 (x, n, c) adamc@156: | SOME c => adamc@156: S.map2 (mfc ctx c, adamc@156: fn c' => (x, n, SOME c'))) xncs, adamc@156: fn xncs' => adamc@191: (DDatatype (x, n, xs, xncs'), loc)) adamc@191: | DDatatypeImp (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 (mfc ctx c, adamc@162: fn c' => (x, n, SOME c'))) xncs, adamc@162: fn xncs' => adamc@191: (DDatatypeImp (x, n, m1, ms, s, xs, xncs'), loc)) adamc@123: | DVal vi => adamc@123: S.map2 (mfvi ctx vi, adamc@123: fn vi' => adamc@123: (DVal vi', loc)) adamc@123: | DValRec vis => adamc@123: S.map2 (ListUtil.mapfold (mfvi ctx) vis, adamc@123: fn vis' => adamc@123: (DValRec vis', loc)) adamc@76: | DSgn (x, n, sgn) => adamc@76: S.map2 (mfsg ctx sgn, adamc@76: fn sgn' => adamc@76: (DSgn (x, n, sgn'), loc)) adamc@76: | DStr (x, n, sgn, str) => adamc@76: S.bind2 (mfsg ctx sgn, adamc@76: fn sgn' => adamc@76: S.map2 (mfst ctx str, adamc@76: fn str' => adamc@76: (DStr (x, n, sgn', str'), loc))) adamc@76: | DFfiStr (x, n, sgn) => adamc@76: S.map2 (mfsg ctx sgn, adamc@76: fn sgn' => adamc@76: (DFfiStr (x, n, sgn'), loc)) adamc@88: | DConstraint (c1, c2) => adamc@88: S.bind2 (mfc ctx c1, adamc@88: fn c1' => adamc@88: S.map2 (mfc ctx c2, adamc@88: fn c2' => adamc@88: (DConstraint (c1', c2'), loc))) adamc@109: | DExport (en, sgn, str) => adamc@109: S.bind2 (mfsg ctx sgn, adamc@109: fn sgn' => adamc@109: S.map2 (mfst ctx str, adamc@109: fn str' => adamc@109: (DExport (en, sgn', str'), loc))) adamc@123: adamc@205: | DTable (tn, x, n, c) => adamc@203: S.map2 (mfc ctx c, adamc@203: fn c' => adamc@205: (DTable (tn, x, n, c'), loc)) adamc@338: | DSequence _ => S.return2 dAll adamc@203: adamc@563: | DClass (x, n, k, c) => adamc@563: S.bind2 (mfk k, adamc@563: fn k' => adamc@563: S.map2 (mfc ctx c, adamc@563: fn c' => adamc@563: (DClass (x, n, k', c'), loc))) adamc@213: adamc@338: | DDatabase _ => S.return2 dAll adamc@271: adamc@459: | DCookie (tn, x, n, c) => adamc@459: S.map2 (mfc ctx c, adamc@459: fn c' => adamc@459: (DCookie (tn, x, n, c'), loc)) adamc@459: adamc@123: and mfvi ctx (x, n, c, e) = adamc@123: S.bind2 (mfc ctx c, adamc@123: fn c' => adamc@123: S.map2 (mfe ctx e, adamc@123: fn e' => adamc@123: (x, n, c', e'))) adamc@76: in adamc@76: mfd adamc@76: end adamc@76: adamc@76: fun mapfold {kind, con, exp, sgn_item, sgn, str, decl} = adamc@76: mapfoldB {kind = kind, adamc@76: con = fn () => con, adamc@76: exp = fn () => exp, adamc@76: sgn_item = fn () => sgn_item, adamc@76: sgn = fn () => sgn, adamc@76: str = fn () => str, adamc@76: decl = fn () => decl, adamc@76: bind = fn ((), _) => ()} () adamc@76: adamc@76: fun exists {kind, con, exp, sgn_item, sgn, str, decl} k = adamc@76: case mapfold {kind = fn k => fn () => adamc@76: if kind k then adamc@76: S.Return () adamc@76: else adamc@76: S.Continue (k, ()), adamc@76: con = fn c => fn () => adamc@76: if con c then adamc@76: S.Return () adamc@76: else adamc@76: S.Continue (c, ()), adamc@76: exp = fn e => fn () => adamc@76: if exp e then adamc@76: S.Return () adamc@76: else adamc@76: S.Continue (e, ()), adamc@76: sgn_item = fn sgi => fn () => adamc@76: if sgn_item sgi then adamc@76: S.Return () adamc@76: else adamc@76: S.Continue (sgi, ()), adamc@76: sgn = fn x => fn () => adamc@76: if sgn x then adamc@76: S.Return () adamc@76: else adamc@76: S.Continue (x, ()), adamc@76: str = fn x => fn () => adamc@76: if str x then adamc@76: S.Return () adamc@76: else adamc@76: S.Continue (x, ()), adamc@76: decl = fn x => fn () => adamc@76: if decl x then adamc@76: S.Return () adamc@76: else adamc@76: S.Continue (x, ())} k () of adamc@76: S.Return _ => true adamc@76: | S.Continue _ => false adamc@76: adamc@76: fun search {kind, con, exp, sgn_item, sgn, str, decl} k = adamc@76: case mapfold {kind = fn x => fn () => adamc@76: case kind x of adamc@76: NONE => S.Continue (x, ()) adamc@76: | SOME v => S.Return v, adamc@76: adamc@76: con = fn x => fn () => adamc@76: case con x of adamc@76: NONE => S.Continue (x, ()) adamc@76: | SOME v => S.Return v, adamc@76: adamc@76: exp = fn x => fn () => adamc@76: case exp x of adamc@76: NONE => S.Continue (x, ()) adamc@76: | SOME v => S.Return v, adamc@76: adamc@76: sgn_item = fn x => fn () => adamc@76: case sgn_item x of adamc@76: NONE => S.Continue (x, ()) adamc@76: | SOME v => S.Return v, adamc@76: adamc@76: sgn = fn x => fn () => adamc@76: case sgn x of adamc@76: NONE => S.Continue (x, ()) adamc@76: | SOME v => S.Return v, adamc@76: adamc@76: str = fn x => fn () => adamc@76: case str x of adamc@76: NONE => S.Continue (x, ()) adamc@76: | SOME v => S.Return v, adamc@76: adamc@76: decl = fn x => fn () => adamc@76: case decl x of adamc@76: NONE => S.Continue (x, ()) adamc@76: | SOME v => S.Return v adamc@76: adamc@76: } k () of adamc@76: S.Return x => SOME x adamc@76: | S.Continue _ => NONE adamc@76: adamc@448: fun foldMapB {kind, con, exp, sgn_item, sgn, str, decl, bind} ctx st d = adamc@448: case mapfoldB {kind = fn x => fn st => S.Continue (kind (x, st)), adamc@448: con = fn ctx => fn x => fn st => S.Continue (con (ctx, x, st)), adamc@448: exp = fn ctx => fn x => fn st => S.Continue (exp (ctx, x, st)), adamc@448: sgn_item = fn ctx => fn x => fn st => S.Continue (sgn_item (ctx, x, st)), adamc@448: sgn = fn ctx => fn x => fn st => S.Continue (sgn (ctx, x, st)), adamc@448: str = fn ctx => fn x => fn st => S.Continue (str (ctx, x, st)), adamc@448: decl = fn ctx => fn x => fn st => S.Continue (decl (ctx, x, st)), adamc@448: bind = bind} ctx d st of adamc@448: S.Continue x => x adamc@448: | S.Return _ => raise Fail "ElabUtil.Decl.foldMapB: Impossible" adamc@448: adamc@448: end adamc@448: adamc@448: structure File = struct adamc@448: adamc@448: fun maxName ds = foldl (fn (d, count) => Int.max (maxNameDecl d, count)) 0 ds adamc@448: adamc@448: and maxNameDecl (d, _) = adamc@448: case d of adamc@448: DCon (_, n, _, _) => n adamc@448: | DDatatype (_, n, _, ns) => adamc@448: foldl (fn ((_, n', _), m) => Int.max (n', m)) adamc@448: n ns adamc@448: | DDatatypeImp (_, n1, n2, _, _, _, ns) => adamc@448: foldl (fn ((_, n', _), m) => Int.max (n', m)) adamc@448: (Int.max (n1, n2)) ns adamc@448: | DVal (_, n, _, _) => n adamc@448: | DValRec vis => foldl (fn ((_, n, _, _), count) => Int.max (n, count)) 0 vis adamc@448: | DStr (_, n, sgn, str) => Int.max (n, Int.max (maxNameSgn sgn, maxNameStr str)) adamc@448: | DSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn) adamc@448: | DFfiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn) adamc@448: | DConstraint _ => 0 adamc@563: | DClass (_, n, _, _) => n adamc@448: | DExport _ => 0 adamc@459: | DTable (n1, _, n2, _) => Int.max (n1, n2) adamc@459: | DSequence (n1, _, n2) => Int.max (n1, n2) adamc@448: | DDatabase _ => 0 adamc@459: | DCookie (n1, _, n2, _) => Int.max (n1, n2) adamc@448: adamc@448: and maxNameStr (str, _) = adamc@448: case str of adamc@448: StrConst ds => maxName ds adamc@448: | StrVar n => n adamc@448: | StrProj (str, _) => maxNameStr str adamc@448: | StrFun (_, n, dom, ran, str) => foldl Int.max n [maxNameSgn dom, maxNameSgn ran, maxNameStr str] adamc@448: | StrApp (str1, str2) => Int.max (maxNameStr str1, maxNameStr str2) adamc@448: | StrError => 0 adamc@448: adamc@448: and maxNameSgn (sgn, _) = adamc@448: case sgn of adamc@448: SgnConst sgis => foldl (fn (sgi, count) => Int.max (maxNameSgi sgi, count)) 0 sgis adamc@448: | SgnVar n => n adamc@448: | SgnFun (_, n, dom, ran) => Int.max (n, Int.max (maxNameSgn dom, maxNameSgn ran)) adamc@448: | SgnWhere (sgn, _, _) => maxNameSgn sgn adamc@448: | SgnProj (n, _, _) => n adamc@448: | SgnError => 0 adamc@448: adamc@448: and maxNameSgi (sgi, _) = adamc@448: case sgi of adamc@448: SgiConAbs (_, n, _) => n adamc@448: | SgiCon (_, n, _, _) => n adamc@448: | SgiDatatype (_, n, _, ns) => adamc@448: foldl (fn ((_, n', _), m) => Int.max (n', m)) adamc@448: n ns adamc@448: | SgiDatatypeImp (_, n1, n2, _, _, _, ns) => adamc@448: foldl (fn ((_, n', _), m) => Int.max (n', m)) adamc@448: (Int.max (n1, n2)) ns adamc@448: | SgiVal (_, n, _) => n adamc@448: | SgiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn) adamc@448: | SgiSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn) adamc@448: | SgiConstraint _ => 0 adamc@563: | SgiClassAbs (_, n, _) => n adamc@563: | SgiClass (_, n, _, _) => n adamc@448: adamc@34: end adamc@76: adamc@76: end