From cfb8ffaf94885d8dc1b492a050830a9b4ffc3d04 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 1 Nov 2008 15:58:55 -0400 Subject: First Unnest tests working --- src/elab_util.sml | 107 +++++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 105 insertions(+), 2 deletions(-) (limited to 'src/elab_util.sml') diff --git a/src/elab_util.sml b/src/elab_util.sml index 28fe8f22..2e190d1e 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -226,6 +226,13 @@ fun exists {kind, con} k = S.Return _ => true | S.Continue _ => false +fun foldB {kind, con, bind} ctx st c = + case mapfoldB {kind = fn k => fn st => S.Continue (k, kind (k, st)), + con = fn ctx => fn c => fn st => S.Continue (c, con (ctx, c, st)), + bind = bind} ctx c st of + S.Continue (_, st) => st + | S.Return _ => raise Fail "ElabUtil.Con.foldB: Impossible" + end structure Exp = struct @@ -340,8 +347,20 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = S.bind2 (mfe ctx e, fn e' => S.bind2 (ListUtil.mapfold (fn (p, e) => - S.map2 (mfe ctx e, - fn e' => (p, e'))) pes, + let + fun pb ((p, _), ctx) = + case p of + PWild => ctx + | PVar (x, t) => bind (ctx, RelE (x, t)) + | PPrim _ => ctx + | PCon (_, _, _, NONE) => ctx + | PCon (_, _, _, SOME p) => pb (p, ctx) + | PRecord xps => foldl (fn ((_, p, _), ctx) => + pb (p, ctx)) ctx xps + in + S.map2 (mfe (pb (p, ctx)) e, + fn e' => (p, e')) + end) pes, fn pes' => S.bind2 (mfc ctx disc, fn disc' => @@ -431,6 +450,14 @@ fun mapB {kind, con, exp, bind} ctx e = S.Continue (e, ()) => e | S.Return _ => raise Fail "ElabUtil.Exp.mapB: Impossible" +fun foldB {kind, con, exp, bind} ctx st e = + case mapfoldB {kind = fn k => fn st => S.Continue (k, kind (k, st)), + con = fn ctx => fn c => fn st => S.Continue (c, con (ctx, c, st)), + exp = fn ctx => fn e => fn st => S.Continue (e, exp (ctx, e, st)), + bind = bind} ctx e st of + S.Continue (_, st) => st + | S.Return _ => raise Fail "ElabUtil.Exp.foldB: Impossible" + end structure Sgn = struct @@ -888,6 +915,82 @@ fun search {kind, con, exp, sgn_item, sgn, str, decl} k = S.Return x => SOME x | S.Continue _ => NONE +fun foldMapB {kind, con, exp, sgn_item, sgn, str, decl, bind} ctx st d = + case mapfoldB {kind = fn x => fn st => S.Continue (kind (x, st)), + con = fn ctx => fn x => fn st => S.Continue (con (ctx, x, st)), + exp = fn ctx => fn x => fn st => S.Continue (exp (ctx, x, st)), + sgn_item = fn ctx => fn x => fn st => S.Continue (sgn_item (ctx, x, st)), + sgn = fn ctx => fn x => fn st => S.Continue (sgn (ctx, x, st)), + str = fn ctx => fn x => fn st => S.Continue (str (ctx, x, st)), + decl = fn ctx => fn x => fn st => S.Continue (decl (ctx, x, st)), + bind = bind} ctx d st of + S.Continue x => x + | S.Return _ => raise Fail "ElabUtil.Decl.foldMapB: Impossible" + +end + +structure File = struct + +fun maxName ds = foldl (fn (d, count) => Int.max (maxNameDecl d, count)) 0 ds + +and maxNameDecl (d, _) = + case d of + DCon (_, n, _, _) => n + | DDatatype (_, n, _, ns) => + foldl (fn ((_, n', _), m) => Int.max (n', m)) + n ns + | DDatatypeImp (_, n1, n2, _, _, _, ns) => + foldl (fn ((_, n', _), m) => Int.max (n', m)) + (Int.max (n1, n2)) ns + | DVal (_, n, _, _) => n + | DValRec vis => foldl (fn ((_, n, _, _), count) => Int.max (n, count)) 0 vis + | DStr (_, n, sgn, str) => Int.max (n, Int.max (maxNameSgn sgn, maxNameStr str)) + | DSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn) + | DFfiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn) + | DConstraint _ => 0 + | DClass (_, n, _) => n + | DExport _ => 0 + | DTable (n, _, _, _) => n + | DSequence (n, _, _) => n + | DDatabase _ => 0 + +and maxNameStr (str, _) = + case str of + StrConst ds => maxName ds + | StrVar n => n + | StrProj (str, _) => maxNameStr str + | StrFun (_, n, dom, ran, str) => foldl Int.max n [maxNameSgn dom, maxNameSgn ran, maxNameStr str] + | StrApp (str1, str2) => Int.max (maxNameStr str1, maxNameStr str2) + | StrError => 0 + +and maxNameSgn (sgn, _) = + case sgn of + SgnConst sgis => foldl (fn (sgi, count) => Int.max (maxNameSgi sgi, count)) 0 sgis + | SgnVar n => n + | SgnFun (_, n, dom, ran) => Int.max (n, Int.max (maxNameSgn dom, maxNameSgn ran)) + | SgnWhere (sgn, _, _) => maxNameSgn sgn + | SgnProj (n, _, _) => n + | SgnError => 0 + +and maxNameSgi (sgi, _) = + case sgi of + SgiConAbs (_, n, _) => n + | SgiCon (_, n, _, _) => n + | SgiDatatype (_, n, _, ns) => + foldl (fn ((_, n', _), m) => Int.max (n', m)) + n ns + | SgiDatatypeImp (_, n1, n2, _, _, _, ns) => + foldl (fn ((_, n', _), m) => Int.max (n', m)) + (Int.max (n1, n2)) ns + | SgiVal (_, n, _) => n + | SgiStr (_, n, sgn) => Int.max (n, maxNameSgn sgn) + | SgiSgn (_, n, sgn) => Int.max (n, maxNameSgn sgn) + | SgiConstraint _ => 0 + | SgiTable (n, _, _, _) => n + | SgiSequence (n, _, _) => n + | SgiClassAbs (_, n) => n + | SgiClass (_, n, _) => n + end end -- cgit v1.2.3