From 3f497272d327fea2638006c751d812dbbc449c78 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sat, 1 Nov 2008 11:17:29 -0400 Subject: Elaborating 'let' --- src/elab_env.sig | 1 + 1 file changed, 1 insertion(+) (limited to 'src/elab_env.sig') diff --git a/src/elab_env.sig b/src/elab_env.sig index 363cbe26..727ee259 100644 --- a/src/elab_env.sig +++ b/src/elab_env.sig @@ -85,6 +85,7 @@ signature ELAB_ENV = sig val lookupStr : env -> string -> (int * Elab.sgn) option + val edeclBinds : env -> Elab.edecl -> env val declBinds : env -> Elab.decl -> env val sgiBinds : env -> Elab.sgn_item -> env -- cgit v1.2.3 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/compiler.sig | 2 + src/compiler.sml | 9 +- src/elab_env.sig | 4 + src/elab_env.sml | 29 +++++ src/elab_print.sml | 4 +- src/elab_util.sig | 25 ++++ src/elab_util.sml | 107 ++++++++++++++- src/sources | 3 + src/termination.sml | 2 + src/unnest.sig | 34 +++++ src/unnest.sml | 369 ++++++++++++++++++++++++++++++++++++++++++++++++++++ tests/nest.ur | 41 ++++++ tests/nest.urp | 3 + 13 files changed, 627 insertions(+), 5 deletions(-) create mode 100644 src/unnest.sig create mode 100644 src/unnest.sml create mode 100644 tests/nest.ur create mode 100644 tests/nest.urp (limited to 'src/elab_env.sig') diff --git a/src/compiler.sig b/src/compiler.sig index e26ec13c..bc1974a1 100644 --- a/src/compiler.sig +++ b/src/compiler.sig @@ -58,6 +58,7 @@ signature COMPILER = sig val parse : (job, Source.file) phase val elaborate : (Source.file, Elab.file) phase + val unnest : (Elab.file, Elab.file) phase val termination : (Elab.file, Elab.file) phase val explify : (Elab.file, Expl.file) phase val corify : (Expl.file, Core.file) phase @@ -80,6 +81,7 @@ signature COMPILER = sig val toParseJob : (string, job) transform val toParse : (string, Source.file) transform val toElaborate : (string, Elab.file) transform + val toUnnest : (string, Elab.file) transform val toTermination : (string, Elab.file) transform val toExplify : (string, Expl.file) transform val toCorify : (string, Core.file) transform diff --git a/src/compiler.sml b/src/compiler.sml index 4f1bce11..e92f86c3 100644 --- a/src/compiler.sml +++ b/src/compiler.sml @@ -383,12 +383,19 @@ val elaborate = { val toElaborate = transform elaborate "elaborate" o toParse +val unnest = { + func = Unnest.unnest, + print = ElabPrint.p_file ElabEnv.empty +} + +val toUnnest = transform unnest "unnest" o toElaborate + val termination = { func = (fn file => (Termination.check file; file)), print = ElabPrint.p_file ElabEnv.empty } -val toTermination = transform termination "termination" o toElaborate +val toTermination = transform termination "termination" o toUnnest val explify = { func = Explify.explify, diff --git a/src/elab_env.sig b/src/elab_env.sig index 727ee259..90cf8153 100644 --- a/src/elab_env.sig +++ b/src/elab_env.sig @@ -30,6 +30,10 @@ signature ELAB_ENV = sig exception SynUnif val liftConInCon : int -> Elab.con -> Elab.con + val liftExpInExp : int -> Elab.exp -> Elab.exp + + val subExpInExp : (int * Elab.exp) -> Elab.exp -> Elab.exp + type env val empty : env diff --git a/src/elab_env.sml b/src/elab_env.sml index f4f5d2cb..2732de13 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -61,6 +61,20 @@ val liftConInCon = val lift = liftConInCon 0 +val liftConInExp = + U.Exp.mapB {kind = fn k => k, + con = fn bound => fn c => + case c of + CRel xn => + if xn < bound then + c + else + CRel (xn + 1) + | _ => c, + exp = fn _ => fn e => e, + bind = fn (bound, U.Exp.RelC _) => bound + 1 + | (bound, _) => bound} + val liftExpInExp = U.Exp.mapB {kind = fn k => k, con = fn _ => fn c => c, @@ -78,6 +92,21 @@ val liftExpInExp = val liftExp = liftExpInExp 0 +val subExpInExp = + U.Exp.mapB {kind = fn k => k, + con = fn _ => fn c => c, + exp = fn (xn, rep) => fn e => + case e of + ERel xn' => + (case Int.compare (xn', xn) of + EQUAL => #1 rep + | GREATER=> ERel (xn' - 1) + | LESS => e) + | _ => e, + bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, liftExpInExp 0 rep) + | ((xn, rep), U.Exp.RelC _) => (xn, liftConInExp 0 rep) + | (ctx, _) => ctx} + (* Back to environments *) datatype 'a var' = diff --git a/src/elab_print.sml b/src/elab_print.sml index 3d7ce625..b236954e 100644 --- a/src/elab_print.sml +++ b/src/elab_print.sml @@ -198,7 +198,7 @@ fun p_patCon env pc = string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n) else string (#1 (E.lookupENamed env n))) - handle E.UnboundRel _ => string ("UNBOUND_NAMED" ^ Int.toString n)) + handle E.UnboundNamed _ => string ("UNBOUND_NAMED" ^ Int.toString n)) | PConProj (m1, ms, x) => let val m1x = #1 (E.lookupStrNamed env m1) @@ -247,7 +247,7 @@ fun p_exp' par env (e, _) = string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n) else string (#1 (E.lookupENamed env n))) - handle E.UnboundRel _ => string ("UNBOUND_NAMED" ^ Int.toString n)) + handle E.UnboundNamed _ => string ("UNBOUND_NAMED" ^ Int.toString n)) | EModProj (m1, ms, x) => let val m1x = #1 (E.lookupStrNamed env m1) diff --git a/src/elab_util.sig b/src/elab_util.sig index f4edd972..f9988981 100644 --- a/src/elab_util.sig +++ b/src/elab_util.sig @@ -57,6 +57,11 @@ structure Con : sig -> Elab.con -> Elab.con val exists : {kind : Elab.kind' -> bool, con : Elab.con' -> bool} -> Elab.con -> bool + + val foldB : {kind : Elab.kind' * 'state -> 'state, + con : 'context * Elab.con' * 'state -> 'state, + bind : 'context * binder -> 'context} + -> 'context -> 'state -> Elab.con -> 'state end structure Exp : sig @@ -83,6 +88,12 @@ structure Exp : sig val exists : {kind : Elab.kind' -> bool, con : Elab.con' -> bool, exp : Elab.exp' -> bool} -> Elab.exp -> bool + + val foldB : {kind : Elab.kind' * 'state -> 'state, + con : 'context * Elab.con' * 'state -> 'state, + exp : 'context * Elab.exp' * 'state -> 'state, + bind : 'context * binder -> 'context} + -> 'context -> 'state -> Elab.exp -> 'state end structure Sgn : sig @@ -156,6 +167,20 @@ structure Decl : sig str : Elab.str' -> 'a option, decl : Elab.decl' -> 'a option} -> Elab.decl -> 'a option + + val foldMapB : {kind : Elab.kind' * 'state -> Elab.kind' * 'state, + con : 'context * Elab.con' * 'state -> Elab.con' * 'state, + exp : 'context * Elab.exp' * 'state -> Elab.exp' * 'state, + sgn_item : 'context * Elab.sgn_item' * 'state -> Elab.sgn_item' * 'state, + sgn : 'context * Elab.sgn' * 'state -> Elab.sgn' * 'state, + str : 'context * Elab.str' * 'state -> Elab.str' * 'state, + decl : 'context * Elab.decl' * 'state -> Elab.decl' * 'state, + bind : 'context * binder -> 'context} + -> 'context -> 'state -> Elab.decl -> Elab.decl * 'state +end + +structure File : sig + val maxName : Elab.file -> int end end 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 diff --git a/src/sources b/src/sources index ebf71d9e..984b5e23 100644 --- a/src/sources +++ b/src/sources @@ -50,6 +50,9 @@ elab_err.sml elaborate.sig elaborate.sml +unnest.sig +unnest.sml + termination.sig termination.sml diff --git a/src/termination.sml b/src/termination.sml index b0716eca..6ed4d92f 100644 --- a/src/termination.sml +++ b/src/termination.sml @@ -292,6 +292,8 @@ fun declOk' env (d, loc) = | EError => (Rabble, calls) | EUnif (ref (SOME e)) => exp parent (penv, calls) e | EUnif (ref NONE) => (Rabble, calls) + + | ELet (_, e) => exp parent (penv, calls) e end fun doVali (i, (_, f, _, e), calls) = diff --git a/src/unnest.sig b/src/unnest.sig new file mode 100644 index 00000000..6508a781 --- /dev/null +++ b/src/unnest.sig @@ -0,0 +1,34 @@ +(* Copyright (c) 2008, Adam Chlipala + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * - Redistributions of source code must retain the above copyright notice, + * this list of conditions and the following disclaimer. + * - Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * - The names of contributors may not be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE + * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF + * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN + * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) + * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + *) + +(* Remove nested function definitions *) + +signature UNNEST = sig + + val unnest : Elab.file -> Elab.file + +end diff --git a/src/unnest.sml b/src/unnest.sml new file mode 100644 index 00000000..e5eddc42 --- /dev/null +++ b/src/unnest.sml @@ -0,0 +1,369 @@ +(* Copyright (c) 2008, Adam Chlipala + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * - Redistributions of source code must retain the above copyright notice, + * this list of conditions and the following disclaimer. + * - Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * - The names of contributors may not be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE + * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF + * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN + * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) + * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + *) + +(* Remove nested function definitions *) + +structure Unnest :> UNNEST = struct + +open Elab + +structure E = ElabEnv +structure U = ElabUtil + +structure IS = IntBinarySet + +val fvsCon = U.Con.foldB {kind = fn (_, st) => st, + con = fn (cb, c, cvs) => + case c of + CRel n => + if n >= cb then + IS.add (cvs, n - cb) + else + cvs + | _ => cvs, + bind = fn (cb, b) => + case b of + U.Con.Rel _ => cb + 1 + | _ => cb} + 0 IS.empty + +fun fvsExp nr = U.Exp.foldB {kind = fn (_, st) => st, + con = fn ((cb, eb), c, st as (cvs, evs)) => + case c of + CRel n => + if n >= cb then + (IS.add (cvs, n - cb), evs) + else + st + | _ => st, + exp = fn ((cb, eb), e, st as (cvs, evs)) => + case e of + ERel n => + if n >= eb then + (cvs, IS.add (evs, n - eb)) + else + st + | _ => st, + bind = fn (ctx as (cb, eb), b) => + case b of + U.Exp.RelC _ => (cb + 1, eb) + | U.Exp.RelE _ => (cb, eb + 1) + | _ => ctx} + (0, nr) (IS.empty, IS.empty) + +fun positionOf (x : int) ls = + let + fun po n ls = + case ls of + [] => raise Fail "Unnest.positionOf" + | x' :: ls' => + if x' = x then + n + else + po (n + 1) ls' + in + po 0 ls + handle Fail _ => raise Fail ("Unnset.positionOf(" + ^ Int.toString x + ^ ", " + ^ String.concatWith ";" (map Int.toString ls) + ^ ")") + end + +fun squishCon cfv = + U.Con.mapB {kind = fn k => k, + con = fn cb => fn c => + case c of + CRel n => + if n >= cb then + CRel (positionOf (n - cb) cfv + cb) + else + c + | _ => c, + bind = fn (cb, b) => + case b of + U.Con.Rel _ => cb + 1 + | _ => cb} + 0 + +fun squishExp (nr, cfv, efv) = + U.Exp.mapB {kind = fn k => k, + con = fn (cb, eb) => fn c => + case c of + CRel n => + if n >= cb then + CRel (positionOf (n - cb) cfv + cb) + else + c + | _ => c, + exp = fn (cb, eb) => fn e => + case e of + ERel n => + if n >= eb then + ERel (positionOf (n - eb) efv + eb) + else + e + | _ => e, + bind = fn (ctx as (cb, eb), b) => + case b of + U.Exp.RelC _ => (cb + 1, eb) + | U.Exp.RelE _ => (cb, eb + 1) + | _ => ctx} + (0, nr) + +type state = { + maxName : int, + decls : decl list +} + +fun kind (k, st) = (k, st) + +fun exp ((ks, ts), e, st : state) = + case e of + ELet (eds, e) => + let + val doSubst = foldl (fn (p, e) => E.subExpInExp p e) + + val (eds, (maxName, ds, subs)) = + ListUtil.foldlMapConcat + (fn (ed, (maxName, ds, subs)) => + case #1 ed of + EDVal _ => ([ed], (maxName, ds, map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs)) + | EDValRec vis => + let + val loc = #2 ed + + val nr = length vis + val (cfv, efv) = foldl (fn ((_, t, e), (cfv, efv)) => + let + val (cfv', efv') = fvsExp nr e + (*val () = Print.prefaces "fvsExp" + [("e", ElabPrint.p_exp E.empty e), + ("cfv", Print.PD.string + (Int.toString (IS.numItems cfv'))), + ("efv", Print.PD.string + (Int.toString (IS.numItems efv')))]*) + val cfv'' = fvsCon t + in + (IS.union (cfv, IS.union (cfv', cfv'')), + IS.union (efv, efv')) + end) + (IS.empty, IS.empty) vis + + (*val () = print ("A: " ^ Int.toString (length ts) ^ ", " ^ Int.toString (length ks) ^ "\n")*) + val cfv = IS.foldl (fn (x, cfv) => + let + (*val () = print (Int.toString x ^ "\n")*) + val (_, t) = List.nth (ts, x) + in + IS.union (cfv, fvsCon t) + end) + cfv efv + (*val () = print "B\n"*) + + val (vis, maxName) = + ListUtil.foldlMap (fn ((x, t, e), maxName) => + ((x, maxName, t, e), + maxName + 1)) + maxName vis + + fun apply e = + let + val e = IS.foldl (fn (x, e) => + (ECApp (e, (CRel x, loc)), loc)) + e cfv + in + IS.foldl (fn (x, e) => + (EApp (e, (ERel x, loc)), loc)) + e efv + end + + val subs = map (fn (n, e) => (n + nr, E.liftExpInExp nr e)) subs + + val subs' = ListUtil.mapi (fn (i, (_, n, _, _)) => + let + val e = apply (ENamed n, loc) + in + (0, E.liftExpInExp (nr - i - 1) e) + end) + vis + val subs' = rev subs' + + val cfv = IS.listItems cfv + val efv = IS.listItems efv + val efn = length efv + + (*val subsInner = subs + @ map (fn (i, e) => + (i + efn, + E.liftExpInExp efn e)) subs'*) + + val subs = subs @ subs' + + val vis = map (fn (x, n, t, e) => + let + (*val () = Print.prefaces "preSubst" + [("e", ElabPrint.p_exp E.empty e)]*) + val e = doSubst e subs(*Inner*) + + (*val () = Print.prefaces "squishCon" + [("t", ElabPrint.p_con E.empty t)]*) + val t = squishCon cfv t + (*val () = Print.prefaces "squishExp" + [("e", ElabPrint.p_exp E.empty e)]*) + val e = squishExp (nr, cfv, efv) e + + val (e, t) = foldr (fn (ex, (e, t)) => + let + val (name, t') = List.nth (ts, ex) + in + ((EAbs (name, + t', + t, + e), loc), + (TFun (t', + t), loc)) + end) + (e, t) efv + + val (e, t) = foldr (fn (cx, (e, t)) => + let + val (name, k) = List.nth (ks, cx) + in + ((ECAbs (Explicit, + name, + k, + e), loc), + (TCFun (Explicit, + name, + k, + t), loc)) + end) + (e, t) cfv + in + (x, n, t, e) + end) + vis + + val d = (DValRec vis, #2 ed) + in + ([], (maxName, d :: ds, subs)) + end) + (#maxName st, #decls st, []) eds + in + (ELet (eds, doSubst e subs), + {maxName = maxName, + decls = ds}) + end + + | _ => (e, st) + +fun default (ctx, d, st) = (d, st) + +fun bind ((ks, ts), b) = + case b of + U.Decl.RelC p => (p :: ks, map (fn (name, t) => (name, E.liftConInCon 0 t)) ts) + | U.Decl.RelE p => (ks, p :: ts) + | _ => (ks, ts) + +val unnestDecl = U.Decl.foldMapB {kind = kind, + con = default, + exp = exp, + sgn_item = default, + sgn = default, + str = default, + decl = default, + bind = bind} + ([], []) + +fun unnest file = + let + fun doDecl (all as (d, loc), st : state) = + let + fun default () = ([all], st) + fun explore () = + let + val (d, st) = unnestDecl st all + in + (rev (d :: #decls st), + {maxName = #maxName st, + decls = []}) + end + in + case d of + DCon _ => default () + | DDatatype _ => default () + | DDatatypeImp _ => default () + | DVal _ => explore () + | DValRec _ => explore () + | DSgn _ => default () + | DStr (x, n, sgn, str) => + let + val (str, st) = doStr (str, st) + in + ([(DStr (x, n, sgn, str), loc)], st) + end + | DFfiStr _ => default () + | DConstraint _ => default () + | DExport _ => default () + | DTable _ => default () + | DSequence _ => default () + | DClass _ => default () + | DDatabase _ => default () + end + + and doStr (all as (str, loc), st) = + let + fun default () = (all, st) + in + case str of + StrConst ds => + let + val (ds, st) = ListUtil.foldlMapConcat doDecl st ds + in + ((StrConst ds, loc), st) + end + | StrVar _ => default () + | StrProj _ => default () + | StrFun (x, n, dom, ran, str) => + let + val (str, st) = doStr (str, st) + in + ((StrFun (x, n, dom, ran, str), loc), st) + end + | StrApp _ => default () + | StrError => raise Fail "Unnest: StrError" + end + + val (ds, _) = ListUtil.foldlMapConcat doDecl + {maxName = U.File.maxName file + 1, + decls = []} file + in + ds + end + +end diff --git a/tests/nest.ur b/tests/nest.ur new file mode 100644 index 00000000..c136b1e6 --- /dev/null +++ b/tests/nest.ur @@ -0,0 +1,41 @@ +fun add x = + let + fun add' y = x + y + in + add' 1 + add' 2 + end + +fun f (x : int) = + let + fun page () = return + {[x]} + + in + page + end + +fun f (x : int) = + let + fun page1 () = return + {[x]} + + + and page2 () = + case Some True of + Some r => return {[r]} + | _ => return Error + in + page1 + end + +datatype list t = Nil | Cons of t * list t + +fun length (t ::: Type) (ls : list t) = + let + fun length' ls acc = + case ls of + Nil => acc + | Cons (_, ls') => length' ls' (acc + 1) + in + length' ls 0 + end diff --git a/tests/nest.urp b/tests/nest.urp new file mode 100644 index 00000000..7f8a473a --- /dev/null +++ b/tests/nest.urp @@ -0,0 +1,3 @@ +debug + +nest -- cgit v1.2.3 From 24b68e6d7408f50023272e765687eab777596363 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 6 Nov 2008 19:43:48 -0500 Subject: Tree demo working (and other assorted regressions fixed) --- demo/crud.ur | 8 ++++---- demo/prose | 4 ++++ demo/refFun.ur | 8 ++++---- demo/sql.ur | 4 ++-- demo/tree.ur | 22 ++++++++++++++++++++-- demo/tree.urp | 2 +- demo/treeFun.ur | 2 +- lib/top.ur | 4 ++-- src/cjr_print.sml | 37 +++++++++++++++++++++++++++++++++++++ src/elab_env.sig | 1 + src/elab_env.sml | 3 +++ src/elaborate.sml | 16 +++++++++++----- src/monoize.sml | 16 ++++++++++++++++ src/urweb.grm | 6 +++--- 14 files changed, 109 insertions(+), 24 deletions(-) (limited to 'src/elab_env.sig') diff --git a/demo/crud.ur b/demo/crud.ur index ee6a95f6..a120cb2a 100644 --- a/demo/crud.ur +++ b/demo/crud.ur @@ -102,7 +102,7 @@ functor Make(M : sig [[nm] ~ rest] => fn input col acc => acc ++ {nm = @sql_inject col.Inject (col.Parse input)}) {} [M.cols] inputs M.cols - ++ {Id = (SQL {id})})); + ++ {Id = (SQL {[id]})})); ls <- list (); return

Inserted with ID {[id]}.

@@ -122,7 +122,7 @@ functor Make(M : sig fn input col acc => acc ++ {nm = @sql_inject col.Inject (col.Parse input)}) {} [M.cols] inputs M.cols) - tab (WHERE T.Id = {id})); + tab (WHERE T.Id = {[id]})); ls <- list (); return

Saved!

@@ -131,7 +131,7 @@ functor Make(M : sig and upd (id : int) = - fso <- oneOrNoRows (SELECT tab.{{mapT2T fstTT M.cols}} FROM tab WHERE tab.Id = {id}); + fso <- oneOrNoRows (SELECT tab.{{mapT2T fstTT M.cols}} FROM tab WHERE tab.Id = {[id]}); case fso : (Basis.option {Tab : $(mapT2T fstTT M.cols)}) of None => return Not found! | Some fs => return
@@ -150,7 +150,7 @@ functor Make(M : sig
and delete (id : int) = - dml (DELETE FROM tab WHERE Id = {id}); + dml (DELETE FROM tab WHERE Id = {[id]}); ls <- list (); return

The deed is done.

diff --git a/demo/prose b/demo/prose index fad98e26..11661211 100644 --- a/demo/prose +++ b/demo/prose @@ -132,6 +132,10 @@ metaform2.urp

This example showcases code reuse by applying the same functor as in the last example. The Metaform2 module mixes pages from the functor with some new pages of its own.

+tree.urp + +

Here we see how we can abstract over common patterns of SQL queries. In particular, since standard SQL does not help much with queries over trees, we write a function for traversing an SQL tree, building an HTML representation, based on a user-provided function for rendering individual rows.

+ crud1.urp

This example pulls together much of what we have seen so far. It involves a generic "admin interface" builder. That is, we have the Crud.Make functor, which takes in a description of a table and outputs a sub-application for viewing and editing that table.

diff --git a/demo/refFun.ur b/demo/refFun.ur index d648f31e..e523bac7 100644 --- a/demo/refFun.ur +++ b/demo/refFun.ur @@ -10,19 +10,19 @@ functor Make(M : sig fun new d = id <- nextval s; - dml (INSERT INTO t (Id, Data) VALUES ({id}, {d})); + dml (INSERT INTO t (Id, Data) VALUES ({[id]}, {[d]})); return id fun read r = - o <- oneOrNoRows (SELECT t.Data FROM t WHERE t.Id = {r}); + o <- oneOrNoRows (SELECT t.Data FROM t WHERE t.Id = {[r]}); return (case o of None => error You already deleted that ref! | Some r => r.T.Data) fun write r d = - dml (UPDATE t SET Data = {d} WHERE Id = {r}) + dml (UPDATE t SET Data = {[d]} WHERE Id = {[r]}) fun delete r = - dml (DELETE FROM t WHERE Id = {r}) + dml (DELETE FROM t WHERE Id = {[r]}) end diff --git a/demo/sql.ur b/demo/sql.ur index 43a69573..44ff478f 100644 --- a/demo/sql.ur +++ b/demo/sql.ur @@ -27,7 +27,7 @@ fun list () = and add r = dml (INSERT INTO t (A, B, C, D) - VALUES ({readError r.A}, {readError r.B}, {r.C}, {r.D})); + VALUES ({[readError r.A]}, {[readError r.B]}, {[r.C]}, {[r.D]})); xml <- list (); return

Row added.

@@ -37,7 +37,7 @@ and add r = and delete a = dml (DELETE FROM t - WHERE t.A = {a}); + WHERE t.A = {[a]}); xml <- list (); return

Row deleted.

diff --git a/demo/tree.ur b/demo/tree.ur index 06a30cf9..27e9aa21 100644 --- a/demo/tree.ur +++ b/demo/tree.ur @@ -1,3 +1,4 @@ +sequence s table t : { Id : int, Parent : option int, Nam : string } open TreeFun.Make(struct @@ -5,11 +6,28 @@ open TreeFun.Make(struct end) fun row r = - #{[r.Id]}: {[r.Nam]} + #{[r.Id]}: {[r.Nam]} [Delete] + +
+ Add child: +
-fun main () = +and main () = xml <- tree row None; return {xml} + +
+ Add a top-level node: +
+ +and add parent r = + id <- nextval s; + dml (INSERT INTO t (Id, Parent, Nam) VALUES ({[id]}, {[parent]}, {[r.Nam]})); + main () + +and del id = + dml (DELETE FROM t WHERE Id = {[id]}); + main () diff --git a/demo/tree.urp b/demo/tree.urp index 2270dd06..880a7ab4 100644 --- a/demo/tree.urp +++ b/demo/tree.urp @@ -1,5 +1,5 @@ debug -database dbname=tree +database dbname=test sql tree.sql treeFun diff --git a/demo/treeFun.ur b/demo/treeFun.ur index 236f354c..15fe60f5 100644 --- a/demo/treeFun.ur +++ b/demo/treeFun.ur @@ -18,7 +18,7 @@ functor Make(M : sig (root : option M.key) = let fun recurse (root : option key) = - queryX' (SELECT * FROM tab WHERE {[eqNullable' (SQL tab.{parent}) root]}) + queryX' (SELECT * FROM tab WHERE {eqNullable' (SQL tab.{parent}) root}) (fn r => children <- recurse (Some r.Tab.id); return diff --git a/lib/top.ur b/lib/top.ur index 5d00282c..76fe73c1 100644 --- a/lib/top.ur +++ b/lib/top.ur @@ -230,12 +230,12 @@ fun eqNullable (tables ::: {{Type}}) (agg ::: {{Type}}) (exps ::: {Type}) (t ::: Type) (_ : sql_injectable (option t)) (e1 : sql_exp tables agg exps (option t)) (e2 : sql_exp tables agg exps (option t)) = - (SQL ({[e1]} IS NULL AND {[e2]} IS NULL) OR {[e1]} = {[e2]}) + (SQL ({e1} IS NULL AND {e2} IS NULL) OR {e1} = {e2}) fun eqNullable' (tables ::: {{Type}}) (agg ::: {{Type}}) (exps ::: {Type}) (t ::: Type) (inj : sql_injectable (option t)) (e1 : sql_exp tables agg exps (option t)) (e2 : option t) = case e2 of - None => (SQL {[e1]} IS NULL) + None => (SQL {e1} IS NULL) | Some _ => sql_comparison sql_eq e1 (@sql_inject inj e2) diff --git a/src/cjr_print.sml b/src/cjr_print.sml index 2485e317..3941fdd9 100644 --- a/src/cjr_print.sml +++ b/src/cjr_print.sml @@ -799,6 +799,43 @@ fun unurlify env (t, loc) = string "})"] end + | TOption t => + box [string "(request[0] == '/' ? ++request : request, ", + string "((!strncmp(request, \"None\", 4) ", + string "&& (request[4] == 0 || request[4] == '/')) ", + string "? (request += 4, NULL) ", + string ": ((!strncmp(request, \"Some\", 4) ", + string "&& request[4] == '/') ", + string "? (request += 5, ", + if isUnboxable t then + unurlify' rf (#1 t) + else + box [string "({", + newline, + p_typ env t, + space, + string "*tmp", + space, + string "=", + space, + string "uw_malloc(ctx, sizeof(", + p_typ env t, + string "));", + newline, + string "*tmp", + space, + string "=", + space, + unurlify' rf (#1 t), + string ";", + newline, + string "tmp;", + newline, + string "})"], + string ") :", + space, + string "(uw_error(ctx, FATAL, \"Error unurlifying option type\"), NULL))))"] + | _ => (ErrorMsg.errorAt loc "Unable to choose a URL decoding function"; space) in diff --git a/src/elab_env.sig b/src/elab_env.sig index 90cf8153..926837e1 100644 --- a/src/elab_env.sig +++ b/src/elab_env.sig @@ -74,6 +74,7 @@ signature ELAB_ENV = sig val pushENamed : env -> string -> Elab.con -> env * int val pushENamedAs : env -> string -> int -> Elab.con -> env val lookupENamed : env -> int -> string * Elab.con + val checkENamed : env -> int -> bool val lookupE : env -> string -> Elab.con var diff --git a/src/elab_env.sml b/src/elab_env.sml index 46f62727..05da56db 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -542,6 +542,9 @@ fun lookupENamed (env : env) n = NONE => raise UnboundNamed n | SOME x => x +fun checkENamed (env : env) n = + Option.isSome (IM.find (#namedE env, n)) + fun lookupE (env : env) x = case SM.find (#renameE env, x) of NONE => NotBound diff --git a/src/elaborate.sml b/src/elaborate.sml index f0beecdd..e84f5307 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -2282,9 +2282,15 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) = let val env = case #1 h of L'.SgiCon (x, n, k, c) => - E.pushCNamedAs env x n k (SOME c) + if E.checkENamed env n then + env + else + E.pushCNamedAs env x n k (SOME c) | L'.SgiConAbs (x, n, k) => - E.pushCNamedAs env x n k NONE + if E.checkENamed env n then + env + else + E.pushCNamedAs env x n k NONE | _ => env in seek (E.sgiBinds env h, sgiBindsD (env, denv) h) t @@ -2391,12 +2397,12 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) = fun good () = let - val env = E.sgiBinds env sgi2All + val env = E.sgiBinds env sgi1All val env = if n1 = n2 then env else - E.pushCNamedAs env x n1 k' - (SOME (L'.CNamed n2, loc)) + E.pushCNamedAs env x n2 k' + (SOME (L'.CNamed n1, loc)) in SOME (env, denv) end diff --git a/src/monoize.sml b/src/monoize.sml index 9e1a4d22..ee509f52 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -390,6 +390,22 @@ fun fooifyExp fk env = ((L'.EApp ((L'.ENamed n, loc), e), loc), fm) end + | L'.TOption t => + let + val (body, fm) = fooify fm ((L'.ERel 0, loc), t) + in + ((L'.ECase (e, + [((L'.PNone t, loc), + (L'.EPrim (Prim.String "None"), loc)), + + ((L'.PSome (t, (L'.PVar ("x", t), loc)), loc), + (L'.EStrcat ((L'.EPrim (Prim.String "Some/"), loc), + body), loc))], + {disc = tAll, + result = (L'.TFfi ("Basis", "string"), loc)}), loc), + fm) + end + | _ => (E.errorAt loc "Don't know how to encode attribute type"; Print.eprefaces' [("Type", MonoPrint.p_typ MonoEnv.empty tAll)]; (dummyExp, fm)) diff --git a/src/urweb.grm b/src/urweb.grm index 4ac14450..b49cd793 100644 --- a/src/urweb.grm +++ b/src/urweb.grm @@ -1236,7 +1236,7 @@ sqlexp : TRUE (sql_inject (EVar (["Basis"], "True", In end end) - | LBRACE LBRACK eexp RBRACK RBRACE (eexp) + | LBRACE eexp RBRACE (eexp) | sqlexp EQ sqlexp (sql_compare ("eq", sqlexp1, sqlexp2, s (sqlexp1left, sqlexp2right))) | sqlexp NE sqlexp (sql_compare ("ne", sqlexp1, sqlexp2, s (sqlexp1left, sqlexp2right))) @@ -1256,8 +1256,8 @@ sqlexp : TRUE (sql_inject (EVar (["Basis"], "True", In sqlexp), loc) end) - | LBRACE eexp RBRACE (sql_inject (#1 eexp, - s (LBRACEleft, RBRACEright))) + | LBRACE LBRACK eexp RBRACK RBRACE (sql_inject (#1 eexp, + s (LBRACEleft, RBRACEright))) | LPAREN sqlexp RPAREN (sqlexp) | NULL (sql_inject ((EVar (["Basis"], "None", Infer), -- cgit v1.2.3 From 5ca452a8576373895301be85a7dfc13746036cac Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 11 Nov 2008 11:49:51 -0500 Subject: Get threadedBlog to work --- src/core_print.sml | 2 +- src/elab_env.sig | 1 + src/especialize.sml | 21 +++++++-- src/unnest.sml | 129 ++++++++++++++++++++++++++++++++++++---------------- 4 files changed, 111 insertions(+), 42 deletions(-) (limited to 'src/elab_env.sig') diff --git a/src/core_print.sml b/src/core_print.sml index af43e401..f209b84f 100644 --- a/src/core_print.sml +++ b/src/core_print.sml @@ -227,7 +227,7 @@ fun p_exp' par env (e, _) = string "(", p_list (p_exp env) es, string "))"] - | EApp (e1, e2) => parenIf par (box [p_exp env e1, + | EApp (e1, e2) => parenIf par (box [p_exp' true env e1, space, p_exp' true env e2]) | EAbs (x, t, _, e) => parenIf par (box [string "fn", diff --git a/src/elab_env.sig b/src/elab_env.sig index 926837e1..0b436106 100644 --- a/src/elab_env.sig +++ b/src/elab_env.sig @@ -30,6 +30,7 @@ signature ELAB_ENV = sig exception SynUnif val liftConInCon : int -> Elab.con -> Elab.con + val liftConInExp : int -> Elab.exp -> Elab.exp val liftExpInExp : int -> Elab.exp -> Elab.exp val subExpInExp : (int * Elab.exp) -> Elab.exp -> Elab.exp diff --git a/src/especialize.sml b/src/especialize.sml index f9c7c388..ffd4745b 100644 --- a/src/especialize.sml +++ b/src/especialize.sml @@ -188,9 +188,14 @@ fun specialize' file = andalso List.exists (fn (ERecord [], _) => false | _ => true) xs' andalso not (IS.member (actionable, f)) andalso hasFunarg (typ, xs') then - (#1 (foldl (fn (arg, e) => (EApp (e, arg), ErrorMsg.dummySpan)) - body xs'), - st) + let + val e = foldl (fn (arg, e) => (EApp (e, arg), ErrorMsg.dummySpan)) + body xs' + in + (*Print.prefaces "Unfolded" + [("e", CorePrint.p_exp CoreEnv.empty e)];*) + (#1 e, st) + end else (e, st) end) @@ -221,6 +226,9 @@ fun specialize' file = NONE => (e, st) | SOME (body', typ') => let + (*val () = Print.prefaces "sub'd" + [("body'", CorePrint.p_exp CoreEnv.empty body')]*) + val f' = #maxName st val funcs = IM.insert (#funcs st, f, {name = name, args = KM.insert (args, @@ -234,7 +242,13 @@ fun specialize' file = decls = #decls st } + (*val () = print ("Created " ^ Int.toString f' ^ " from " + ^ Int.toString f ^ "\n") + val () = Print.prefaces "body'" + [("body'", CorePrint.p_exp CoreEnv.empty body')]*) val (body', st) = specExp st body' + (*val () = Print.prefaces "body''" + [("body'", CorePrint.p_exp CoreEnv.empty body')]*) val e' = foldl (fn (arg, e) => (EApp (e, arg), ErrorMsg.dummySpan)) (ENamed f', ErrorMsg.dummySpan) xs' in @@ -316,6 +330,7 @@ fun specialize' file = fun specialize file = let + (*val () = Print.prefaces "Intermediate" [("file", CorePrint.p_file CoreEnv.empty file)];*) val (changed, file) = specialize' file in if changed then diff --git a/src/unnest.sml b/src/unnest.sml index 6a37d484..fe63f9fe 100644 --- a/src/unnest.sml +++ b/src/unnest.sml @@ -36,6 +36,35 @@ structure U = ElabUtil structure IS = IntBinarySet +fun liftExpInExp by = + U.Exp.mapB {kind = fn k => k, + con = fn _ => fn c => c, + exp = fn bound => fn e => + case e of + ERel xn => + if xn < bound then + e + else + ERel (xn + by) + | _ => e, + bind = fn (bound, U.Exp.RelE _) => bound + 1 + | (bound, _) => bound} + +val subExpInExp = + U.Exp.mapB {kind = fn k => k, + con = fn _ => fn c => c, + exp = fn (xn, rep) => fn e => + case e of + ERel xn' => + if xn' = xn then + #1 rep + else + e + | _ => e, + bind = fn ((xn, rep), U.Exp.RelE _) => (xn+1, E.liftExpInExp 0 rep) + | ((xn, rep), U.Exp.RelC _) => (xn, E.liftConInExp 0 rep) + | (ctx, _) => ctx} + val fvsCon = U.Con.foldB {kind = fn (_, st) => st, con = fn (cb, c, cvs) => case c of @@ -87,7 +116,7 @@ fun positionOf (x : int) ls = po (n + 1) ls' in po 0 ls - handle Fail _ => raise Fail ("Unnset.positionOf(" + handle Fail _ => raise Fail ("Unnest.positionOf(" ^ Int.toString x ^ ", " ^ String.concatWith ";" (map Int.toString ls) @@ -124,7 +153,7 @@ fun squishExp (nr, cfv, efv) = case e of ERel n => if n >= eb then - ERel (positionOf (n - eb) efv + eb) + ERel (positionOf (n - eb) efv + eb - nr) else e | _ => e, @@ -146,17 +175,32 @@ fun exp ((ks, ts), e as old, st : state) = case e of ELet (eds, e) => let - (*val () = Print.prefaces "let" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*) + (*val () = Print.prefaces "Letto" [("e", ElabPrint.p_exp E.empty (old, ErrorMsg.dummySpan))]*) - val doSubst = foldl (fn (p, e) => E.subExpInExp p e) + fun doSubst' (e, subs) = foldl (fn (p, e) => subExpInExp p e) e subs - val (eds, (ts, maxName, ds, subs)) = + fun doSubst (e, subs, by) = + let + val e = doSubst' (e, subs) + in + liftExpInExp (~by) (length subs) e + end + + val (eds, (ts, maxName, ds, subs, by)) = ListUtil.foldlMapConcat - (fn (ed, (ts, maxName, ds, subs)) => + (fn (ed, (ts, maxName, ds, subs, by)) => case #1 ed of - EDVal (x, t, _) => ([ed], - ((x, t) :: ts, - maxName, ds, map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs)) + EDVal (x, t, e) => + let + val e = doSubst (e, subs, by) + in + ([(EDVal (x, t, e), #2 ed)], + ((x, t) :: ts, + maxName, ds, + ((0, (ERel 0, #2 ed)) + :: map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs), + by)) + end | EDValRec vis => let val loc = #2 ed @@ -182,6 +226,7 @@ fun exp ((ks, ts), e as old, st : state) = val () = app (fn (x, t) => Print.prefaces "Var" [("x", Print.PD.string x), ("t", ElabPrint.p_con E.empty t)]) ts*) + val cfv = IS.foldl (fn (x, cfv) => let (*val () = print (Int.toString x ^ "\n")*) @@ -198,56 +243,54 @@ fun exp ((ks, ts), e as old, st : state) = maxName + 1)) maxName vis - fun apply e = - let - val e = IS.foldr (fn (x, e) => - (ECApp (e, (CRel x, loc)), loc)) - e cfv - in - IS.foldr (fn (x, e) => - (EApp (e, (ERel x, loc)), loc)) - e efv - end - val subs = map (fn (n, e) => (n + nr, E.liftExpInExp nr e)) subs + + val subs = map (fn (n, e) => (n + nr, + case e of + (ERel _, _) => e + | _ => liftExpInExp nr 0 e)) + subs + val subs' = ListUtil.mapi (fn (i, (_, n, _, _)) => let - val dummy = (EError, ErrorMsg.dummySpan) - - fun repeatLift k = - if k = 0 then - apply (ENamed n, loc) - else - E.liftExpInExp 0 (repeatLift (k - 1)) + val e = (ENamed n, loc) + + val e = IS.foldr (fn (x, e) => + (ECApp (e, (CRel x, loc)), loc)) + e cfv + + val e = IS.foldr (fn (x, e) => + (EApp (e, (ERel (nr + x), loc)), + loc)) + e efv in - (0, repeatLift i) + (nr - i - 1, e) end) vis - val subs' = rev subs' - val cfv = IS.listItems cfv val efv = IS.listItems efv - val efn = length efv - val subs = subs @ subs' + val subs = subs' @ subs val vis = map (fn (x, n, t, e) => let (*val () = Print.prefaces "preSubst" [("e", ElabPrint.p_exp E.empty e)]*) - val e = doSubst e subs + val e = doSubst' (e, subs) (*val () = Print.prefaces "squishCon" [("t", ElabPrint.p_con E.empty t)]*) val t = squishCon cfv t (*val () = Print.prefaces "squishExp" [("e", ElabPrint.p_exp E.empty e)]*) - val e = squishExp (0(*nr*), cfv, efv) e + val e = squishExp (nr, cfv, efv) e + (*val () = print ("Avail: " ^ Int.toString (length ts) ^ "\n")*) val (e, t) = foldl (fn (ex, (e, t)) => let + (*val () = print (Int.toString ex ^ "\n")*) val (name, t') = List.nth (ts, ex) in ((EAbs (name, @@ -258,6 +301,7 @@ fun exp ((ks, ts), e as old, st : state) = t), loc)) end) (e, t) efv + (*val () = print "Done\n"*) val (e, t) = foldl (fn (cx, (e, t)) => let @@ -274,19 +318,28 @@ fun exp ((ks, ts), e as old, st : state) = end) (e, t) cfv in + (*Print.prefaces "Have a vi" + [("x", Print.PD.string x), + ("e", ElabPrint.p_exp ElabEnv.empty e)];*) (x, n, t, e) end) vis - val ts = map (fn (x, _, t, _) => (x, t)) vis @ ts + val ts = List.revAppend (map (fn (x, _, t, _) => (x, t)) vis, ts) in - ([], (ts, maxName, vis @ ds, subs)) + ([], (ts, maxName, vis @ ds, subs, by + nr)) end) - (ts, #maxName st, #decls st, []) eds + (ts, #maxName st, #decls st, [], 0) eds + + val e' = doSubst (e, subs, by) in - (ELet (eds, doSubst e subs), + (*Print.prefaces "Before" [("e", ElabPrint.p_exp ElabEnv.empty e), + ("se", ElabPrint.p_exp ElabEnv.empty (doSubst' (e, subs))), + ("e'", ElabPrint.p_exp ElabEnv.empty e')];*) + (ELet (eds, e'), {maxName = maxName, decls = ds}) + (*(ELet (eds, doSubst (liftExpInExp (~(length subs - numRemaining)) (length subs) e) subs),*) end | _ => (e, st) -- cgit v1.2.3 From 85cf99a95c910841f197ca911bb13d044456de7f Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 22 Feb 2009 16:10:25 -0500 Subject: Start of kind polymorphism, up to the point where demo/hello elaborates with updated Basis/Top --- lib/ur/top.ur | 171 ++++++++++-------------------------- lib/ur/top.urs | 112 +++++++----------------- src/core.sml | 1 - src/core_print.sml | 1 - src/core_util.sml | 8 -- src/corify.sml | 1 - src/elab.sml | 11 ++- src/elab_env.sig | 4 + src/elab_env.sml | 130 ++++++++++++++++++++++++--- src/elab_err.sig | 7 +- src/elab_err.sml | 61 +++++++------ src/elab_ops.sig | 6 ++ src/elab_ops.sml | 69 ++++++++++++++- src/elab_print.sig | 2 +- src/elab_print.sml | 95 +++++++++++++------- src/elab_util.sig | 38 +++++--- src/elab_util.sml | 154 ++++++++++++++++++++------------ src/elaborate.sml | 241 +++++++++++++++++++++++++++++++++------------------ src/expl.sml | 1 - src/expl_print.sml | 1 - src/expl_util.sml | 4 - src/explify.sml | 2 - src/monoize.sml | 1 - src/reduce.sml | 16 ---- src/reduce_local.sml | 2 - src/source.sml | 9 +- src/source_print.sml | 26 +++++- src/termination.sml | 9 +- src/unnest.sml | 18 ++-- src/urweb.grm | 23 +++-- src/urweb.lex | 3 +- 31 files changed, 736 insertions(+), 491 deletions(-) (limited to 'src/elab_env.sig') diff --git a/lib/ur/top.ur b/lib/ur/top.ur index 58e99f3c..9016fd27 100644 --- a/lib/ur/top.ur +++ b/lib/ur/top.ur @@ -1,3 +1,12 @@ +(** Row folding *) + +con folder = K ==> fn r :: {K} => + tf :: ({K} -> Type) + -> (nm :: Name -> v :: K -> r :: {K} -> tf r + -> fn [[nm] ~ r] => tf ([nm = v] ++ r)) + -> tf [] -> tf r + + fun not b = if b then False else True con idT (t :: Type) = t @@ -27,23 +36,23 @@ fun foldUR (tf :: Type) (tr :: {Unit} -> Type) (f : nm :: Name -> rest :: {Unit} -> fn [[nm] ~ rest] => tf -> tr rest -> tr ([nm] ++ rest)) - (i : tr []) = + (i : tr []) (r ::: {Unit}) (fold : folder r)= fold [fn r :: {Unit} => $(mapUT tf r) -> tr r] - (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc - [[nm] ~ rest] r => - f [nm] [rest] r.nm (acc (r -- nm))) - (fn _ => i) + (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc + [[nm] ~ rest] r => + f [nm] [rest] r.nm (acc (r -- nm))) + (fn _ => i) fun foldUR2 (tf1 :: Type) (tf2 :: Type) (tr :: {Unit} -> Type) (f : nm :: Name -> rest :: {Unit} -> fn [[nm] ~ rest] => tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest)) - (i : tr []) = + (i : tr []) (r ::: {Unit}) (fold : folder r) = fold [fn r :: {Unit} => $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r] - (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc - [[nm] ~ rest] r1 r2 => - f [nm] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) - (fn _ _ => i) + (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc + [[nm] ~ rest] r1 r2 => + f [nm] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) + (fn _ _ => i) fun foldURX2 (tf1 :: Type) (tf2 :: Type) (ctx :: {Unit}) (f : nm :: Name -> rest :: {Unit} @@ -54,134 +63,46 @@ fun foldURX2 (tf1 :: Type) (tf2 :: Type) (ctx :: {Unit}) {f [nm] [rest] v1 v2}{acc}) -fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type) - (f : nm :: Name -> t :: Type -> rest :: {Type} +fun foldR K (tf :: K -> Type) (tr :: {K} -> Type) + (f : nm :: Name -> t :: K -> rest :: {K} -> fn [[nm] ~ rest] => tf t -> tr rest -> tr ([nm = t] ++ rest)) - (i : tr []) = - fold [fn r :: {Type} => $(map tf r) -> tr r] - (fn (nm :: Name) (t :: Type) (rest :: {Type}) (acc : _ -> tr rest) + (i : tr []) (r ::: {K}) (fold : folder r) = + fold [fn r :: {K} => $(map tf r) -> tr r] + (fn (nm :: Name) (t :: K) (rest :: {K}) (acc : _ -> tr rest) [[nm] ~ rest] r => f [nm] [t] [rest] r.nm (acc (r -- nm))) (fn _ => i) -fun foldT2R (tf :: (Type * Type) -> Type) (tr :: {(Type * Type)} -> Type) - (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} - -> fn [[nm] ~ rest] => - tf t -> tr rest -> tr ([nm = t] ++ rest)) - (i : tr []) = - fold [fn r :: {(Type * Type)} => $(map tf r) -> tr r] - (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) - (acc : _ -> tr rest) [[nm] ~ rest] r => - f [nm] [t] [rest] r.nm (acc (r -- nm))) - (fn _ => i) - -fun foldT3R (tf :: (Type * Type * Type) -> Type) (tr :: {(Type * Type * Type)} -> Type) - (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} - -> fn [[nm] ~ rest] => - tf t -> tr rest -> tr ([nm = t] ++ rest)) - (i : tr []) = - fold [fn r :: {(Type * Type * Type)} => $(map tf r) -> tr r] - (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)}) - (acc : _ -> tr rest) [[nm] ~ rest] r => - f [nm] [t] [rest] r.nm (acc (r -- nm))) - (fn _ => i) - -fun foldTR2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (tr :: {Type} -> Type) - (f : nm :: Name -> t :: Type -> rest :: {Type} +fun foldR2 K (tf1 :: K -> Type) (tf2 :: K -> Type) (tr :: {K} -> Type) + (f : nm :: Name -> t :: K -> rest :: {K} -> fn [[nm] ~ rest] => tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) - (i : tr []) = - fold [fn r :: {Type} => $(map tf1 r) -> $(map tf2 r) -> tr r] - (fn (nm :: Name) (t :: Type) (rest :: {Type}) - (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 => - f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) - (fn _ _ => i) - -fun foldT2R2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) - (tr :: {(Type * Type)} -> Type) - (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) - (i : tr []) = - fold [fn r :: {(Type * Type)} => $(map tf1 r) -> $(map tf2 r) -> tr r] - (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) - (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 => - f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) - (fn _ _ => i) - -fun foldT3R2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type) -> Type) - (tr :: {(Type * Type * Type)} -> Type) - (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) - (i : tr []) = - fold [fn r :: {(Type * Type * Type)} => $(map tf1 r) -> $(map tf2 r) -> tr r] - (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)}) - (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 => - f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) - (fn _ _ => i) - -fun foldTRX (tf :: Type -> Type) (ctx :: {Unit}) - (f : nm :: Name -> t :: Type -> rest :: {Type} + (i : tr []) (r ::: {K}) (fold : folder r) = + fold [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> tr r] + (fn (nm :: Name) (t :: K) (rest :: {K}) + (acc : _ -> _ -> tr rest) [[nm] ~ rest] r1 r2 => + f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) + (fn _ _ => i) + +fun foldRX K (tf :: K -> Type) (ctx :: {Unit}) + (f : nm :: Name -> t :: K -> rest :: {K} -> fn [[nm] ~ rest] => tf t -> xml ctx [] []) = - foldTR [tf] [fn _ => xml ctx [] []] - (fn (nm :: Name) (t :: Type) (rest :: {Type}) [[nm] ~ rest] r acc => - {f [nm] [t] [rest] r}{acc}) - - -fun foldT2RX (tf :: (Type * Type) -> Type) (ctx :: {Unit}) - (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} - -> fn [[nm] ~ rest] => - tf t -> xml ctx [] []) = - foldT2R [tf] [fn _ => xml ctx [] []] - (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) - [[nm] ~ rest] r acc => - {f [nm] [t] [rest] r}{acc}) - - -fun foldT3RX (tf :: (Type * Type * Type) -> Type) (ctx :: {Unit}) - (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} - -> fn [[nm] ~ rest] => - tf t -> xml ctx [] []) = - foldT3R [tf] [fn _ => xml ctx [] []] - (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)}) - [[nm] ~ rest] r acc => - {f [nm] [t] [rest] r}{acc}) - + foldR [tf] [fn _ => xml ctx [] []] + (fn (nm :: Name) (t :: K) (rest :: {K}) [[nm] ~ rest] r acc => + {f [nm] [t] [rest] r}{acc}) + -fun foldTRX2 (tf1 :: Type -> Type) (tf2 :: Type -> Type) (ctx :: {Unit}) - (f : nm :: Name -> t :: Type -> rest :: {Type} +fun foldRX2 K (tf1 :: K -> Type) (tf2 :: K -> Type) (ctx :: {Unit}) + (f : nm :: Name -> t :: K -> rest :: {K} -> fn [[nm] ~ rest] => tf1 t -> tf2 t -> xml ctx [] []) = - foldTR2 [tf1] [tf2] [fn _ => xml ctx [] []] - (fn (nm :: Name) (t :: Type) (rest :: {Type}) [[nm] ~ rest] - r1 r2 acc => - {f [nm] [t] [rest] r1 r2}{acc}) - - -fun foldT2RX2 (tf1 :: (Type * Type) -> Type) (tf2 :: (Type * Type) -> Type) - (ctx :: {Unit}) - (f : nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> xml ctx [] []) = - foldT2R2 [tf1] [tf2] [fn _ => xml ctx [] []] - (fn (nm :: Name) (t :: (Type * Type)) (rest :: {(Type * Type)}) - [[nm] ~ rest] r1 r2 acc => - {f [nm] [t] [rest] r1 r2}{acc}) - - -fun foldT3RX2 (tf1 :: (Type * Type * Type) -> Type) (tf2 :: (Type * Type * Type) -> Type) - (ctx :: {Unit}) - (f : nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> xml ctx [] []) = - foldT3R2 [tf1] [tf2] [fn _ => xml ctx [] []] - (fn (nm :: Name) (t :: (Type * Type * Type)) (rest :: {(Type * Type * Type)}) - [[nm] ~ rest] r1 r2 acc => - {f [nm] [t] [rest] r1 r2}{acc}) - + foldR2 [tf1] [tf2] [fn _ => xml ctx [] []] + (fn (nm :: Name) (t :: K) (rest :: {K}) [[nm] ~ rest] + r1 r2 acc => + {f [nm] [t] [rest] r1 r2}{acc}) + fun queryX (tables ::: {{Type}}) (exps ::: {Type}) (ctx ::: {Unit}) (q : sql_query tables exps) [tables ~ exps] diff --git a/lib/ur/top.urs b/lib/ur/top.urs index 49aad50c..d891c80d 100644 --- a/lib/ur/top.urs +++ b/lib/ur/top.urs @@ -1,3 +1,12 @@ +(** Row folding *) + +con folder = K ==> fn r :: {K} => + tf :: ({K} -> Type) + -> (nm :: Name -> v :: K -> r :: {K} -> tf r + -> fn [[nm] ~ r] => tf ([nm = v] ++ r)) + -> tf [] -> tf r + + val not : bool -> bool con idT = fn t :: Type => t @@ -25,103 +34,46 @@ val foldUR : tf :: Type -> tr :: ({Unit} -> Type) -> (nm :: Name -> rest :: {Unit} -> fn [[nm] ~ rest] => tf -> tr rest -> tr ([nm] ++ rest)) - -> tr [] -> r :: {Unit} -> $(mapUT tf r) -> tr r + -> tr [] -> r ::: {Unit} -> folder r -> $(mapUT tf r) -> tr r val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type) -> (nm :: Name -> rest :: {Unit} -> fn [[nm] ~ rest] => tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest)) - -> tr [] -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r + -> tr [] -> r ::: {Unit} -> folder r -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r val foldURX2: tf1 :: Type -> tf2 :: Type -> ctx :: {Unit} -> (nm :: Name -> rest :: {Unit} -> fn [[nm] ~ rest] => tf1 -> tf2 -> xml ctx [] []) - -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> xml ctx [] [] + -> r ::: {Unit} -> folder r -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> xml ctx [] [] -val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type) - -> (nm :: Name -> t :: Type -> rest :: {Type} +val foldR : K --> tf :: (K -> Type) -> tr :: ({K} -> Type) + -> (nm :: Name -> t :: K -> rest :: {K} -> fn [[nm] ~ rest] => tf t -> tr rest -> tr ([nm = t] ++ rest)) - -> tr [] -> r :: {Type} -> $(map tf r) -> tr r + -> tr [] -> r ::: {K} -> folder r -> $(map tf r) -> tr r -val foldT2R : tf :: ((Type * Type) -> Type) -> tr :: ({(Type * Type)} -> Type) - -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} - -> fn [[nm] ~ rest] => - tf t -> tr rest -> tr ([nm = t] ++ rest)) - -> tr [] -> r :: {(Type * Type)} -> $(map tf r) -> tr r +val foldR2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) + -> tr :: ({K} -> Type) + -> (nm :: Name -> t :: K -> rest :: {K} + -> fn [[nm] ~ rest] => + tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) + -> tr [] + -> r ::: {K} -> folder r -> $(map tf1 r) -> $(map tf2 r) -> tr r -val foldT3R : tf :: ((Type * Type * Type) -> Type) -> tr :: ({(Type * Type * Type)} -> Type) - -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} - -> fn [[nm] ~ rest] => - tf t -> tr rest -> tr ([nm = t] ++ rest)) - -> tr [] -> r :: {(Type * Type * Type)} -> $(map tf r) -> tr r +val foldRX : K --> tf :: (K -> Type) -> ctx :: {Unit} + -> (nm :: Name -> t :: K -> rest :: {K} + -> fn [[nm] ~ rest] => + tf t -> xml ctx [] []) + -> r ::: {K} -> folder r -> $(map tf r) -> xml ctx [] [] -val foldTR2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) - -> tr :: ({Type} -> Type) - -> (nm :: Name -> t :: Type -> rest :: {Type} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) - -> tr [] - -> r :: {Type} -> $(map tf1 r) -> $(map tf2 r) -> tr r - -val foldT2R2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) - -> tr :: ({(Type * Type)} -> Type) - -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) - -> tr [] -> r :: {(Type * Type)} - -> $(map tf1 r) -> $(map tf2 r) -> tr r - -val foldT3R2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type) - -> tr :: ({(Type * Type * Type)} -> Type) - -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> tr rest -> tr ([nm = t] ++ rest)) - -> tr [] -> r :: {(Type * Type * Type)} - -> $(map tf1 r) -> $(map tf2 r) -> tr r - -val foldTRX : tf :: (Type -> Type) -> ctx :: {Unit} - -> (nm :: Name -> t :: Type -> rest :: {Type} +val foldRX2 : K --> tf1 :: (K -> Type) -> tf2 :: (K -> Type) -> ctx :: {Unit} + -> (nm :: Name -> t :: K -> rest :: {K} -> fn [[nm] ~ rest] => - tf t -> xml ctx [] []) - -> r :: {Type} -> $(map tf r) -> xml ctx [] [] - -val foldT2RX : tf :: ((Type * Type) -> Type) -> ctx :: {Unit} - -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} - -> fn [[nm] ~ rest] => - tf t -> xml ctx [] []) - -> r :: {(Type * Type)} -> $(map tf r) -> xml ctx [] [] - -val foldT3RX : tf :: ((Type * Type * Type) -> Type) -> ctx :: {Unit} - -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} - -> fn [[nm] ~ rest] => - tf t -> xml ctx [] []) - -> r :: {(Type * Type * Type)} -> $(map tf r) -> xml ctx [] [] - -val foldTRX2 : tf1 :: (Type -> Type) -> tf2 :: (Type -> Type) -> ctx :: {Unit} - -> (nm :: Name -> t :: Type -> rest :: {Type} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> xml ctx [] []) - -> r :: {Type} - -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] [] - -val foldT2RX2 : tf1 :: ((Type * Type) -> Type) -> tf2 :: ((Type * Type) -> Type) - -> ctx :: {Unit} - -> (nm :: Name -> t :: (Type * Type) -> rest :: {(Type * Type)} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> xml ctx [] []) - -> r :: {(Type * Type)} - -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] [] - - -val foldT3RX2 : tf1 :: ((Type * Type * Type) -> Type) -> tf2 :: ((Type * Type * Type) -> Type) - -> ctx :: {Unit} - -> (nm :: Name -> t :: (Type * Type * Type) -> rest :: {(Type * Type * Type)} - -> fn [[nm] ~ rest] => - tf1 t -> tf2 t -> xml ctx [] []) - -> r :: {(Type * Type * Type)} - -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] [] + tf1 t -> tf2 t -> xml ctx [] []) + -> r ::: {K} -> folder r + -> $(map tf1 r) -> $(map tf2 r) -> xml ctx [] [] val queryX : tables ::: {{Type}} -> exps ::: {Type} -> ctx ::: {Unit} -> sql_query tables exps diff --git a/src/core.sml b/src/core.sml index d7a57493..a28d93dd 100644 --- a/src/core.sml +++ b/src/core.sml @@ -96,7 +96,6 @@ datatype exp' = | EConcat of exp * con * exp * con | ECut of exp * con * { field : con, rest : con } | ECutMulti of exp * con * { rest : con } - | EFold of kind | ECase of exp * (pat * exp) list * { disc : con, result : con } diff --git a/src/core_print.sml b/src/core_print.sml index db8c3907..504773ab 100644 --- a/src/core_print.sml +++ b/src/core_print.sml @@ -342,7 +342,6 @@ fun p_exp' par env (e, _) = string "---", space, p_con' true env c]) - | EFold _ => string "fold" | ECase (e, pes, {disc, result}) => parenIf par (box [string "case", diff --git a/src/core_util.sml b/src/core_util.sml index e76da387..d5f8dd05 100644 --- a/src/core_util.sml +++ b/src/core_util.sml @@ -454,10 +454,6 @@ fun compare ((e1, _), (e2, _)) = | (ECutMulti _, _) => LESS | (_, ECutMulti _) => GREATER - | (EFold _, EFold _) => EQUAL - | (EFold _, _) => LESS - | (_, EFold _) => GREATER - | (ECase (e1, pes1, _), ECase (e2, pes2, _)) => join (compare (e1, e2), fn () => joinL (fn ((p1, e1), (p2, e2)) => @@ -609,10 +605,6 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = S.map2 (mfc ctx rest, fn rest' => (ECutMulti (e', c', {rest = rest'}), loc)))) - | EFold k => - S.map2 (mfk k, - fn k' => - (EFold k', loc)) | ECase (e, pes, {disc, result}) => S.bind2 (mfe ctx e, diff --git a/src/corify.sml b/src/corify.sml index c464e5a5..802baf66 100644 --- a/src/corify.sml +++ b/src/corify.sml @@ -592,7 +592,6 @@ fun corifyExp st (e, loc) = {field = corifyCon st field, rest = corifyCon st rest}), loc) | L.ECutMulti (e1, c, {rest}) => (L'.ECutMulti (corifyExp st e1, corifyCon st c, {rest = corifyCon st rest}), loc) - | L.EFold k => (L'.EFold (corifyKind k), loc) | L.ECase (e, pes, {disc, result}) => (L'.ECase (corifyExp st e, diff --git a/src/elab.sml b/src/elab.sml index ec8a910a..9ec3793e 100644 --- a/src/elab.sml +++ b/src/elab.sml @@ -40,6 +40,9 @@ datatype kind' = | KError | KUnif of ErrorMsg.span * string * kind option ref + | KRel of int + | KFun of string * kind + withtype kind = kind' located datatype explicitness = @@ -62,6 +65,10 @@ datatype con' = | CAbs of string * kind * con | CDisjoint of auto_instantiate * con * con * con + | CKAbs of string * con + | CKApp of con * kind + | TKFun of string * con + | CName of string | CRecord of kind * (con * con) list @@ -106,12 +113,14 @@ datatype exp' = | ECApp of exp * con | ECAbs of explicitness * string * kind * exp + | EKAbs of string * exp + | EKApp of exp * kind + | ERecord of (con * exp * con) list | EField of exp * con * { field : con, rest : con } | EConcat of exp * con * exp * con | ECut of exp * con * { field : con, rest : con } | ECutMulti of exp * con * { rest : con } - | EFold of kind | ECase of exp * (pat * exp) list * { disc : con, result : con } diff --git a/src/elab_env.sig b/src/elab_env.sig index 0b436106..10d11e3b 100644 --- a/src/elab_env.sig +++ b/src/elab_env.sig @@ -47,6 +47,10 @@ signature ELAB_ENV = sig | Rel of int * 'a | Named of int * 'a + val pushKRel : env -> string -> env + val lookupKRel : env -> int -> string + val lookupK : env -> string -> int option + val pushCRel : env -> string -> Elab.kind -> env val lookupCRel : env -> int -> string * Elab.kind diff --git a/src/elab_env.sml b/src/elab_env.sml index 53c934dd..083e7d55 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -45,8 +45,32 @@ exception UnboundNamed of int exception SynUnif +val liftKindInKind = + U.Kind.mapB {kind = fn bound => fn k => + case k of + KRel xn => + if xn < bound then + k + else + KRel (xn + 1) + | _ => k, + bind = fn (bound, _) => bound + 1} + +val liftKindInCon = + U.Con.mapB {kind = fn bound => fn k => + case k of + KRel xn => + if xn < bound then + k + else + KRel (xn + 1) + | _ => k, + con = fn _ => fn c => c, + bind = fn (bound, U.Con.RelK _) => bound + 1 + | (bound, _) => bound} + val liftConInCon = - U.Con.mapB {kind = fn k => k, + U.Con.mapB {kind = fn _ => fn k => k, con = fn bound => fn c => case c of CRel xn => @@ -56,13 +80,27 @@ val liftConInCon = CRel (xn + 1) (*| CUnif _ => raise SynUnif*) | _ => c, - bind = fn (bound, U.Con.Rel _) => bound + 1 + bind = fn (bound, U.Con.RelC _) => bound + 1 | (bound, _) => bound} val lift = liftConInCon 0 +val liftKindInExp = + U.Exp.mapB {kind = fn bound => fn k => + case k of + KRel xn => + if xn < bound then + k + else + KRel (xn + 1) + | _ => k, + con = fn _ => fn c => c, + exp = fn _ => fn e => e, + bind = fn (bound, U.Exp.RelK _) => bound + 1 + | (bound, _) => bound} + val liftConInExp = - U.Exp.mapB {kind = fn k => k, + U.Exp.mapB {kind = fn _ => fn k => k, con = fn bound => fn c => case c of CRel xn => @@ -76,7 +114,7 @@ val liftConInExp = | (bound, _) => bound} val liftExpInExp = - U.Exp.mapB {kind = fn k => k, + U.Exp.mapB {kind = fn _ => fn k => k, con = fn _ => fn c => c, exp = fn bound => fn e => case e of @@ -93,7 +131,7 @@ val liftExpInExp = val liftExp = liftExpInExp 0 val subExpInExp = - U.Exp.mapB {kind = fn k => k, + U.Exp.mapB {kind = fn _ => fn k => k, con = fn _ => fn c => c, exp = fn (xn, rep) => fn e => case e of @@ -203,6 +241,9 @@ fun printClasses cs = (print "Classes:\n"; print "\n")) cs) type env = { + renameK : int SM.map, + relK : string list, + renameC : kind var' SM.map, relC : (string * kind) list, namedC : (string * kind * con option) IM.map, @@ -234,6 +275,9 @@ fun newNamed () = end val empty = { + renameK = SM.empty, + relK = [], + renameC = SM.empty, relC = [], namedC = IM.empty, @@ -261,12 +305,51 @@ fun liftClassKey ck = | CkProj _ => ck | CkApp (ck1, ck2) => CkApp (liftClassKey ck1, liftClassKey ck2) +fun pushKRel (env : env) x = + let + val renameK = SM.map (fn n => n+1) (#renameK env) + in + {renameK = SM.insert (renameK, x, 0), + relK = x :: #relK env, + + renameC = SM.map (fn Rel' (n, k) => Rel' (n, liftKindInKind 0 k) + | x => x) (#renameC env), + relC = map (fn (x, k) => (x, liftKindInKind 0 k)) (#relC env), + namedC = #namedC env, + + datatypes = #datatypes env, + constructors = #constructors env, + + classes = #classes env, + + renameE = SM.map (fn Rel' (n, c) => Rel' (n, liftKindInCon 0 c) + | Named' (n, c) => Named' (n, c)) (#renameE env), + relE = map (fn (x, c) => (x, liftKindInCon 0 c)) (#relE env), + namedE = #namedE env, + + renameSgn = #renameSgn env, + sgn = #sgn env, + + renameStr = #renameStr env, + str = #str env + } + end + +fun lookupKRel (env : env) n = + (List.nth (#relK env, n)) + handle Subscript => raise UnboundRel n + +fun lookupK (env : env) x = SM.find (#renameK env, x) + fun pushCRel (env : env) x k = let val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k) | x => x) (#renameC env) in - {renameC = SM.insert (renameC, x, Rel' (0, k)), + {renameK = #renameK env, + relK = #relK env, + + renameC = SM.insert (renameC, x, Rel' (0, k)), relC = (x, k) :: #relC env, namedC = #namedC env, @@ -298,7 +381,10 @@ fun lookupCRel (env : env) n = handle Subscript => raise UnboundRel n fun pushCNamedAs (env : env) x n k co = - {renameC = SM.insert (#renameC env, x, Named' (n, k)), + {renameK = #renameK env, + relK = #relK env, + + renameC = SM.insert (#renameC env, x, Named' (n, k)), relC = #relC env, namedC = IM.insert (#namedC env, n, (x, k, co)), @@ -340,7 +426,10 @@ fun pushDatatype (env : env) n xs xncs = let val dk = U.classifyDatatype xncs in - {renameC = #renameC env, + {renameK = #renameK env, + relK = #relK env, + + renameC = #renameC env, relC = #relC env, namedC = #namedC env, @@ -380,7 +469,10 @@ fun datatypeArgs (xs, _) = xs fun constructors (_, dt) = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt fun pushClass (env : env) n = - {renameC = #renameC env, + {renameK = #renameK env, + relK = #relK env, + + renameC = #renameC env, relC = #relC env, namedC = #namedC env, @@ -468,7 +560,10 @@ fun pushERel (env : env) x t = CM.insert (classes, f, class) end in - {renameC = #renameC env, + {renameK = #renameK env, + relK = #relK env, + + renameC = #renameC env, relC = #relC env, namedC = #namedC env, @@ -509,7 +604,10 @@ fun pushENamedAs (env : env) x n t = CM.insert (classes, f, class) end in - {renameC = #renameC env, + {renameK = #renameK env, + relK = #relK env, + + renameC = #renameC env, relC = #relC env, namedC = #namedC env, @@ -552,7 +650,10 @@ fun lookupE (env : env) x = | SOME (Named' x) => Named x fun pushSgnNamedAs (env : env) x n sgis = - {renameC = #renameC env, + {renameK = #renameK env, + relK = #relK env, + + renameC = #renameC env, relC = #relC env, namedC = #namedC env, @@ -868,7 +969,10 @@ fun enrichClasses env classes (m1, ms) sgn = | _ => classes fun pushStrNamedAs (env : env) x n sgn = - {renameC = #renameC env, + {renameK = #renameK env, + relK = #relK env, + + renameC = #renameC env, relC = #relC env, namedC = #namedC env, diff --git a/src/elab_err.sig b/src/elab_err.sig index d757572f..3b14406b 100644 --- a/src/elab_err.sig +++ b/src/elab_err.sig @@ -27,11 +27,16 @@ signature ELAB_ERR = sig + datatype kind_error = + UnboundKind of ErrorMsg.span * string + + val kindError : ElabEnv.env -> kind_error -> unit + datatype kunify_error = KOccursCheckFailed of Elab.kind * Elab.kind | KIncompatible of Elab.kind * Elab.kind - val kunifyError : kunify_error -> unit + val kunifyError : ElabEnv.env -> kunify_error -> unit datatype con_error = UnboundCon of ErrorMsg.span * string diff --git a/src/elab_err.sml b/src/elab_err.sml index e8d7ff68..8892674c 100644 --- a/src/elab_err.sml +++ b/src/elab_err.sml @@ -36,7 +36,7 @@ structure U = ElabUtil open Print structure P = ElabPrint -val simplCon = U.Con.mapB {kind = fn k => k, +val simplCon = U.Con.mapB {kind = fn _ => fn k => k, con = fn env => fn c => let val c = (c, ErrorMsg.dummySpan) @@ -46,25 +46,34 @@ val simplCon = U.Con.mapB {kind = fn k => k, ("c'", P.p_con env c')];*) #1 c' end, - bind = fn (env, U.Con.Rel (x, k)) => E.pushCRel env x k - | (env, U.Con.Named (x, n, k)) => E.pushCNamedAs env x n k NONE} + bind = fn (env, U.Con.RelC (x, k)) => E.pushCRel env x k + | (env, U.Con.NamedC (x, n, k)) => E.pushCNamedAs env x n k NONE + | (env, _) => env} val p_kind = P.p_kind + +datatype kind_error = + UnboundKind of ErrorMsg.span * string + +fun kindError env err = + case err of + UnboundKind (loc, s) => + ErrorMsg.errorAt loc ("Unbound kind variable " ^ s) datatype kunify_error = KOccursCheckFailed of kind * kind | KIncompatible of kind * kind -fun kunifyError err = +fun kunifyError env err = case err of KOccursCheckFailed (k1, k2) => eprefaces "Kind occurs check failed" - [("Kind 1", p_kind k1), - ("Kind 2", p_kind k2)] + [("Kind 1", p_kind env k1), + ("Kind 2", p_kind env k2)] | KIncompatible (k1, k2) => eprefaces "Incompatible kinds" - [("Kind 1", p_kind k1), - ("Kind 2", p_kind k2)] + [("Kind 1", p_kind env k1), + ("Kind 2", p_kind env k2)] fun p_con env c = P.p_con env (simplCon env c) @@ -89,9 +98,9 @@ fun conError env err = | WrongKind (c, k1, k2, kerr) => (ErrorMsg.errorAt (#2 c) "Wrong kind"; eprefaces' [("Constructor", p_con env c), - ("Have kind", p_kind k1), - ("Need kind", p_kind k2)]; - kunifyError kerr) + ("Have kind", p_kind env k1), + ("Need kind", p_kind env k2)]; + kunifyError env kerr) | DuplicateField (loc, s) => ErrorMsg.errorAt loc ("Duplicate record field " ^ s) | ProjBounds (c, n) => @@ -101,7 +110,7 @@ fun conError env err = | ProjMismatch (c, k) => (ErrorMsg.errorAt (#2 c) "Projection from non-tuple constructor"; eprefaces' [("Constructor", p_con env c), - ("Kind", p_kind k)]) + ("Kind", p_kind env k)]) datatype cunify_error = @@ -116,9 +125,9 @@ fun cunifyError env err = case err of CKind (k1, k2, kerr) => (eprefaces "Kind unification failure" - [("Kind 1", p_kind k1), - ("Kind 2", p_kind k2)]; - kunifyError kerr) + [("Kind 1", p_kind env k1), + ("Kind 2", p_kind env k2)]; + kunifyError env kerr) | COccursCheckFailed (c1, c2) => eprefaces "Constructor occurs check failed" [("Con 1", p_con env c1), @@ -133,7 +142,7 @@ fun cunifyError env err = ("Con 2", p_con env c2)] | CKindof (k, c, expected) => eprefaces ("Unexpected kind for kindof calculation (expecting " ^ expected ^ ")") - [("Kind", p_kind k), + [("Kind", p_kind env k), ("Con", p_con env c)] | CRecordFailure (c1, c2) => eprefaces "Can't unify record constructors" @@ -267,9 +276,9 @@ fun sgnError env err = (ErrorMsg.errorAt (#2 sgi1) "Kind unification failure in signature matching:"; eprefaces' [("Have", p_sgn_item env sgi1), ("Need", p_sgn_item env sgi2), - ("Kind 1", p_kind k1), - ("Kind 2", p_kind k2)]; - kunifyError kerr) + ("Kind 1", p_kind env k1), + ("Kind 2", p_kind env k2)]; + kunifyError env kerr) | SgiWrongCon (sgi1, c1, sgi2, c2, cerr) => (ErrorMsg.errorAt (#2 sgi1) "Constructor unification failure in signature matching:"; eprefaces' [("Have", p_sgn_item env sgi1), @@ -296,9 +305,9 @@ fun sgnError env err = ("Field", PD.string x)]) | WhereWrongKind (k1, k2, kerr) => (ErrorMsg.errorAt (#2 k1) "Wrong kind for 'where'"; - eprefaces' [("Have", p_kind k1), - ("Need", p_kind k2)]; - kunifyError kerr) + eprefaces' [("Have", p_kind env k1), + ("Need", p_kind env k2)]; + kunifyError env kerr) | NotIncludable sgn => (ErrorMsg.errorAt (#2 sgn) "Invalid signature to 'include'"; eprefaces' [("Signature", p_sgn env sgn)]) @@ -337,10 +346,10 @@ fun strError env err = eprefaces' [("Signature", p_sgn env sgn)]) | NotType (k, (k1, k2, ue)) => (ErrorMsg.errorAt (#2 k) "'val' type kind is not 'Type'"; - eprefaces' [("Kind", p_kind k), - ("Subkind 1", p_kind k1), - ("Subkind 2", p_kind k2)]; - kunifyError ue) + eprefaces' [("Kind", p_kind env k), + ("Subkind 1", p_kind env k1), + ("Subkind 2", p_kind env k2)]; + kunifyError env ue) | DuplicateConstructor (x, loc) => ErrorMsg.errorAt loc ("Duplicate datatype constructor " ^ x) | NotDatatype loc => diff --git a/src/elab_ops.sig b/src/elab_ops.sig index 62af9638..7088bf06 100644 --- a/src/elab_ops.sig +++ b/src/elab_ops.sig @@ -27,6 +27,12 @@ signature ELAB_OPS = sig + val liftKindInKind : int -> Elab.kind -> Elab.kind + val subKindInKind : int * Elab.kind -> Elab.kind -> Elab.kind + + val liftKindInCon : int -> Elab.con -> Elab.con + val subKindInCon : int * Elab.kind -> Elab.con -> Elab.con + val liftConInCon : int -> Elab.con -> Elab.con val subConInCon : int * Elab.con -> Elab.con -> Elab.con val subStrInSgn : int * int -> Elab.sgn -> Elab.sgn diff --git a/src/elab_ops.sml b/src/elab_ops.sml index c3e9274c..60a7639d 100644 --- a/src/elab_ops.sml +++ b/src/elab_ops.sml @@ -32,8 +32,64 @@ open Elab structure E = ElabEnv structure U = ElabUtil +fun liftKindInKind' by = + U.Kind.mapB {kind = fn bound => fn k => + case k of + KRel xn => + if xn < bound then + k + else + KRel (xn + by) + | _ => k, + bind = fn (bound, _) => bound + 1} + +fun subKindInKind' rep = + U.Kind.mapB {kind = fn (by, xn) => fn k => + case k of + KRel xn' => + (case Int.compare (xn', xn) of + EQUAL => #1 (liftKindInKind' by 0 rep) + | GREATER => KRel (xn' - 1) + | LESS => k) + | _ => k, + bind = fn ((by, xn), _) => (by+1, xn+1)} + +val liftKindInKind = liftKindInKind' 1 + +fun subKindInKind (xn, rep) = subKindInKind' rep (0, xn) + +fun liftKindInCon by = + U.Con.mapB {kind = fn bound => fn k => + case k of + KRel xn => + if xn < bound then + k + else + KRel (xn + by) + | _ => k, + con = fn _ => fn c => c, + bind = fn (bound, U.Con.RelK _) => bound + 1 + | (bound, _) => bound} + +fun subKindInCon' rep = + U.Con.mapB {kind = fn (by, xn) => fn k => + case k of + KRel xn' => + (case Int.compare (xn', xn) of + EQUAL => #1 (liftKindInKind' by 0 rep) + | GREATER => KRel (xn' - 1) + | LESS => k) + | _ => k, + con = fn _ => fn c => c, + bind = fn ((by, xn), U.Con.RelK _) => (by+1, xn+1) + | (st, _) => st} + +val liftKindInCon = liftKindInCon 1 + +fun subKindInCon (xn, rep) = subKindInCon' rep (0, xn) + fun liftConInCon by = - U.Con.mapB {kind = fn k => k, + U.Con.mapB {kind = fn _ => fn k => k, con = fn bound => fn c => case c of CRel xn => @@ -43,11 +99,11 @@ fun liftConInCon by = CRel (xn + by) (*| CUnif _ => raise SynUnif*) | _ => c, - bind = fn (bound, U.Con.Rel _) => bound + 1 + bind = fn (bound, U.Con.RelC _) => bound + 1 | (bound, _) => bound} fun subConInCon' rep = - U.Con.mapB {kind = fn k => k, + U.Con.mapB {kind = fn _ => fn k => k, con = fn (by, xn) => fn c => case c of CRel xn' => @@ -57,7 +113,7 @@ fun subConInCon' rep = | LESS => c) (*| CUnif _ => raise SynUnif*) | _ => c, - bind = fn ((by, xn), U.Con.Rel _) => (by+1, xn+1) + bind = fn ((by, xn), U.Con.RelC _) => (by+1, xn+1) | (ctx, _) => ctx} val liftConInCon = liftConInCon 1 @@ -205,6 +261,11 @@ fun hnormCon env (cAll as (c, loc)) = | _ => default () end | c1' => (CApp ((c1', loc), hnormCon env c2), loc)) + + | CKApp (c1, k) => + (case hnormCon env c1 of + (CKAbs (_, body), _) => hnormCon env (subKindInCon (0, k) body) + | _ => cAll) | CConcat (c1, c2) => (case (hnormCon env c1, hnormCon env c2) of diff --git a/src/elab_print.sig b/src/elab_print.sig index 3d078576..41d72ca7 100644 --- a/src/elab_print.sig +++ b/src/elab_print.sig @@ -28,7 +28,7 @@ (* Pretty-printing Ur/Web *) signature ELAB_PRINT = sig - val p_kind : Elab.kind Print.printer + val p_kind : ElabEnv.env -> Elab.kind Print.printer val p_explicitness : Elab.explicitness Print.printer val p_con : ElabEnv.env -> Elab.con Print.printer val p_pat : ElabEnv.env -> Elab.pat Print.printer diff --git a/src/elab_print.sml b/src/elab_print.sml index 098c9259..a0e1a54a 100644 --- a/src/elab_print.sml +++ b/src/elab_print.sml @@ -38,25 +38,36 @@ structure E = ElabEnv val debug = ref false -fun p_kind' par (k, _) = +fun p_kind' par env (k, _) = case k of KType => string "Type" - | KArrow (k1, k2) => parenIf par (box [p_kind' true k1, + | KArrow (k1, k2) => parenIf par (box [p_kind' true env k1, space, string "->", space, - p_kind k2]) + p_kind env k2]) | KName => string "Name" - | KRecord k => box [string "{", p_kind k, string "}"] + | KRecord k => box [string "{", p_kind env k, string "}"] | KUnit => string "Unit" | KTuple ks => box [string "(", - p_list_sep (box [space, string "*", space]) p_kind ks, + p_list_sep (box [space, string "*", space]) (p_kind env) ks, string ")"] | KError => string "" - | KUnif (_, _, ref (SOME k)) => p_kind' par k + | KUnif (_, _, ref (SOME k)) => p_kind' par env k | KUnif (_, s, _) => string ("") + | KRel n => ((if !debug then + string (E.lookupKRel env n ^ "_" ^ Int.toString n) + else + string (E.lookupKRel env n)) + handle E.UnboundRel _ => string ("UNBOUND_REL" ^ Int.toString n)) + | KFun (x, k) => box [string x, + space, + string "-->", + space, + p_kind (E.pushKRel env x) k] + and p_kind k = p_kind' false k fun p_explicitness e = @@ -66,7 +77,7 @@ fun p_explicitness e = fun p_con' par env (c, _) = case c of - TFun (t1, t2) => parenIf par (box [p_con' true env t1, + TFun (t1, t2) => parenIf true (box [p_con' true env t1, space, string "->", space, @@ -75,20 +86,22 @@ fun p_con' par env (c, _) = space, p_explicitness e, space, - p_kind k, + p_kind env k, space, string "->", space, p_con (E.pushCRel env x k) c]) - | CDisjoint (_, c1, c2, c3) => parenIf par (box [p_con env c1, - space, - string "~", - space, - p_con env c2, - space, - string "=>", - space, - p_con env c3]) + | CDisjoint (ai, c1, c2, c3) => parenIf par (box [p_con env c1, + space, + string (case ai of + Instantiate => "~" + | LeaveAlone => "~~"), + space, + p_con env c2, + space, + string "=>", + space, + p_con env c3]) | TRecord (CRecord (_, xcs), _) => box [string "{", p_list (fn (x, c) => box [p_name env x, @@ -134,7 +147,7 @@ fun p_con' par env (c, _) = space, string "::", space, - p_kind k, + p_kind env k, space, string "=>", space, @@ -152,7 +165,7 @@ fun p_con' par env (c, _) = space, p_con env c]) xcs, string "]::", - p_kind k]) + p_kind env k]) else parenIf par (box [string "[", p_list (fn (x, c) => @@ -181,8 +194,24 @@ fun p_con' par env (c, _) = | CError => string "" | CUnif (_, _, _, ref (SOME c)) => p_con' par env c | CUnif (_, k, s, _) => box [string (""] + + | CKAbs (x, c) => box [string x, + space, + string "==>", + space, + p_con (E.pushKRel env x) c] + | CKApp (c, k) => box [p_con env c, + string "[[", + p_kind env k, + string "]]"] + | TKFun (x, c) => box [string x, + space, + string "-->", + space, + p_con (E.pushKRel env x) c] + and p_con env = p_con' false env @@ -286,7 +315,7 @@ fun p_exp' par env (e, _) = space, p_explicitness exp, space, - p_kind k, + p_kind env k, space, string "=>", space, @@ -377,8 +406,6 @@ fun p_exp' par env (e, _) = space, p_con' true env c]) - | EFold _ => string "fold" - | ECase (e, pes, _) => parenIf par (box [string "case", space, p_exp env e, @@ -415,6 +442,16 @@ fun p_exp' par env (e, _) = string "end"] end + | EKAbs (x, e) => box [string x, + space, + string "==>", + space, + p_exp (E.pushKRel env x) e] + | EKApp (e, k) => box [p_exp env e, + string "[[", + p_kind env k, + string "]]"] + and p_exp env = p_exp' false env and p_edecl env (dAll as (d, _)) = @@ -478,14 +515,14 @@ fun p_sgn_item env (sgi, _) = space, string "::", space, - p_kind k] + p_kind env k] | SgiCon (x, n, k, c) => box [string "con", space, p_named x n, space, string "::", space, - p_kind k, + p_kind env k, space, string "=", space, @@ -540,14 +577,14 @@ fun p_sgn_item env (sgi, _) = space, string "::", space, - p_kind k] + p_kind env k] | SgiClass (x, n, k, c) => box [string "class", space, p_named x n, space, string "::", space, - p_kind k, + p_kind env k, space, string "=", space, @@ -627,7 +664,7 @@ fun p_decl env (dAll as (d, _) : decl) = space, string "::", space, - p_kind k, + p_kind env k, space, string "=", space, @@ -719,7 +756,7 @@ fun p_decl env (dAll as (d, _) : decl) = space, string "::", space, - p_kind k, + p_kind env k, space, string "=", space, diff --git a/src/elab_util.sig b/src/elab_util.sig index f9988981..817f885f 100644 --- a/src/elab_util.sig +++ b/src/elab_util.sig @@ -30,17 +30,24 @@ signature ELAB_UTIL = sig val classifyDatatype : (string * int * 'a option) list -> Elab.datatype_kind structure Kind : sig + val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB, + bind : 'context * string -> 'context} + -> ('context, Elab.kind, 'state, 'abort) Search.mapfolderB val mapfold : (Elab.kind', 'state, 'abort) Search.mapfolder -> (Elab.kind, 'state, 'abort) Search.mapfolder val exists : (Elab.kind' -> bool) -> Elab.kind -> bool + val mapB : {kind : 'context -> Elab.kind' -> Elab.kind', + bind : 'context * string -> 'context} + -> 'context -> (Elab.kind -> Elab.kind) end structure Con : sig datatype binder = - Rel of string * Elab.kind - | Named of string * int * Elab.kind + RelK of string + | RelC of string * Elab.kind + | NamedC of string * int * Elab.kind - val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, + val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB, con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, bind : 'context * binder -> 'context} -> ('context, Elab.con, 'state, 'abort) Search.mapfolderB @@ -48,7 +55,7 @@ structure Con : sig con : (Elab.con', 'state, 'abort) Search.mapfolder} -> (Elab.con, 'state, 'abort) Search.mapfolder - val mapB : {kind : Elab.kind' -> Elab.kind', + val mapB : {kind : 'context -> Elab.kind' -> Elab.kind', con : 'context -> Elab.con' -> Elab.con', bind : 'context * binder -> 'context} -> 'context -> (Elab.con -> Elab.con) @@ -58,7 +65,7 @@ structure Con : sig val exists : {kind : Elab.kind' -> bool, con : Elab.con' -> bool} -> Elab.con -> bool - val foldB : {kind : Elab.kind' * 'state -> 'state, + val foldB : {kind : 'context * Elab.kind' * 'state -> 'state, con : 'context * Elab.con' * 'state -> 'state, bind : 'context * binder -> 'context} -> 'context -> 'state -> Elab.con -> 'state @@ -66,12 +73,13 @@ end structure Exp : sig datatype binder = - RelC of string * Elab.kind + RelK of string + | RelC of string * Elab.kind | NamedC of string * int * Elab.kind | RelE of string * Elab.con | NamedE of string * Elab.con - val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, + val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB, con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, exp : ('context, Elab.exp', 'state, 'abort) Search.mapfolderB, bind : 'context * binder -> 'context} @@ -80,7 +88,7 @@ structure Exp : sig con : (Elab.con', 'state, 'abort) Search.mapfolder, exp : (Elab.exp', 'state, 'abort) Search.mapfolder} -> (Elab.exp, 'state, 'abort) Search.mapfolder - val mapB : {kind : Elab.kind' -> Elab.kind', + val mapB : {kind : 'context -> Elab.kind' -> Elab.kind', con : 'context -> Elab.con' -> Elab.con', exp : 'context -> Elab.exp' -> Elab.exp', bind : 'context * binder -> 'context} @@ -89,7 +97,7 @@ structure Exp : sig con : Elab.con' -> bool, exp : Elab.exp' -> bool} -> Elab.exp -> bool - val foldB : {kind : Elab.kind' * 'state -> 'state, + val foldB : {kind : 'context * Elab.kind' * 'state -> 'state, con : 'context * Elab.con' * 'state -> 'state, exp : 'context * Elab.exp' * 'state -> 'state, bind : 'context * binder -> 'context} @@ -98,12 +106,13 @@ end structure Sgn : sig datatype binder = - RelC of string * Elab.kind + RelK of string + | RelC of string * Elab.kind | NamedC of string * int * Elab.kind | Str of string * Elab.sgn | Sgn of string * Elab.sgn - val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, + val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB, con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB, sgn : ('context, Elab.sgn', 'state, 'abort) Search.mapfolderB, @@ -127,14 +136,15 @@ end structure Decl : sig datatype binder = - RelC of string * Elab.kind + RelK of string + | RelC of string * Elab.kind | NamedC of string * int * Elab.kind | RelE of string * Elab.con | NamedE of string * Elab.con | Str of string * Elab.sgn | Sgn of string * Elab.sgn - val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, + val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB, con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, exp : ('context, Elab.exp', 'state, 'abort) Search.mapfolderB, sgn_item : ('context, Elab.sgn_item', 'state, 'abort) Search.mapfolderB, @@ -168,7 +178,7 @@ structure Decl : sig decl : Elab.decl' -> 'a option} -> Elab.decl -> 'a option - val foldMapB : {kind : Elab.kind' * 'state -> Elab.kind' * 'state, + val foldMapB : {kind : 'context * Elab.kind' * 'state -> Elab.kind' * 'state, con : 'context * Elab.con' * 'state -> Elab.con' * 'state, exp : 'context * Elab.exp' * 'state -> Elab.exp' * 'state, sgn_item : 'context * Elab.sgn_item' * 'state -> Elab.sgn_item' * 'state, diff --git a/src/elab_util.sml b/src/elab_util.sml index f052a06d..be1c9459 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -43,44 +43,60 @@ structure S = Search structure Kind = struct -fun mapfold f = +fun mapfoldB {kind, bind} = let - fun mfk k acc = - S.bindP (mfk' k acc, f) + fun mfk ctx k acc = + S.bindP (mfk' ctx k acc, kind ctx) - and mfk' (kAll as (k, loc)) = + and mfk' ctx (kAll as (k, loc)) = case k of KType => S.return2 kAll | KArrow (k1, k2) => - S.bind2 (mfk k1, + S.bind2 (mfk ctx k1, fn k1' => - S.map2 (mfk k2, + S.map2 (mfk ctx k2, fn k2' => (KArrow (k1', k2'), loc))) | KName => S.return2 kAll | KRecord k => - S.map2 (mfk k, + S.map2 (mfk ctx k, fn k' => (KRecord k', loc)) | KUnit => S.return2 kAll | KTuple ks => - S.map2 (ListUtil.mapfold mfk ks, + S.map2 (ListUtil.mapfold (mfk ctx) ks, fn ks' => (KTuple ks', loc)) | KError => S.return2 kAll - | KUnif (_, _, ref (SOME k)) => mfk' k + | KUnif (_, _, ref (SOME k)) => mfk' ctx k | KUnif _ => S.return2 kAll + + | KRel _ => S.return2 kAll + | KFun (x, k) => + S.map2 (mfk (bind (ctx, x)) k, + fn k' => + (KFun (x, k'), loc)) in mfk end +fun mapfold fk = + mapfoldB {kind = fn () => fk, + bind = fn ((), _) => ()} () + +fun mapB {kind, bind} ctx k = + case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()), + bind = bind} ctx k () of + S.Continue (k, ()) => k + | S.Return _ => raise Fail "ElabUtil.Kind.mapB: Impossible" + fun exists f k = case mapfold (fn k => fn () => if f k then @@ -95,12 +111,13 @@ end structure Con = struct datatype binder = - Rel of string * Elab.kind - | Named of string * int * Elab.kind + RelK of string + | RelC of string * Elab.kind + | NamedC of string * int * Elab.kind fun mapfoldB {kind = fk, con = fc, bind} = let - val mfk = Kind.mapfold fk + val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, s) => bind (ctx, RelK s)} fun mfc ctx c acc = S.bindP (mfc' ctx c acc, fc ctx) @@ -114,9 +131,9 @@ fun mapfoldB {kind = fk, con = fc, bind} = fn c2' => (TFun (c1', c2'), loc))) | TCFun (e, x, k, c) => - S.bind2 (mfk k, + S.bind2 (mfk ctx k, fn k' => - S.map2 (mfc (bind (ctx, Rel (x, k))) c, + S.map2 (mfc (bind (ctx, RelC (x, k))) c, fn c' => (TCFun (e, x, k', c'), loc))) | CDisjoint (ai, c1, c2, c3) => @@ -142,16 +159,16 @@ fun mapfoldB {kind = fk, con = fc, bind} = fn c2' => (CApp (c1', c2'), loc))) | CAbs (x, k, c) => - S.bind2 (mfk k, + S.bind2 (mfk ctx k, fn k' => - S.map2 (mfc (bind (ctx, Rel (x, k))) c, + S.map2 (mfc (bind (ctx, RelC (x, k))) c, fn c' => (CAbs (x, k', c'), loc))) | CName _ => S.return2 cAll | CRecord (k, xcs) => - S.bind2 (mfk k, + S.bind2 (mfk ctx k, fn k' => S.map2 (ListUtil.mapfold (fn (x, c) => S.bind2 (mfc ctx x, @@ -169,9 +186,9 @@ fun mapfoldB {kind = fk, con = fc, bind} = fn c2' => (CConcat (c1', c2'), loc))) | CMap (k1, k2) => - S.bind2 (mfk k1, + S.bind2 (mfk ctx k1, fn k1' => - S.map2 (mfk k2, + S.map2 (mfk ctx k2, fn k2' => (CMap (k1', k2'), loc))) @@ -190,17 +207,32 @@ fun mapfoldB {kind = fk, con = fc, bind} = | CError => S.return2 cAll | CUnif (_, _, _, ref (SOME c)) => mfc' ctx c | CUnif _ => S.return2 cAll + + | CKAbs (x, c) => + S.map2 (mfc (bind (ctx, RelK x)) c, + fn c' => + (CKAbs (x, c'), loc)) + | CKApp (c, k) => + S.bind2 (mfc ctx c, + fn c' => + S.map2 (mfk ctx k, + fn k' => + (CKApp (c', k'), loc))) + | TKFun (x, c) => + S.map2 (mfc (bind (ctx, RelK x)) c, + fn c' => + (TKFun (x, c'), loc)) in mfc end fun mapfold {kind = fk, con = fc} = - mapfoldB {kind = fk, + mapfoldB {kind = fn () => fk, con = fn () => fc, bind = fn ((), _) => ()} () fun mapB {kind, con, bind} ctx c = - case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()), + case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()), con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()), bind = bind} ctx c () of S.Continue (c, ()) => c @@ -227,7 +259,7 @@ fun exists {kind, con} k = | S.Continue _ => false fun foldB {kind, con, bind} ctx st c = - case mapfoldB {kind = fn k => fn st => S.Continue (k, kind (k, st)), + case mapfoldB {kind = fn ctx => fn k => fn st => S.Continue (k, kind (ctx, 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 @@ -238,20 +270,22 @@ end structure Exp = struct datatype binder = - RelC of string * Elab.kind + RelK of string + | RelC of string * Elab.kind | NamedC of string * int * Elab.kind | RelE of string * Elab.con | NamedE of string * Elab.con fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = let - val mfk = Kind.mapfold fk + val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)} fun bind' (ctx, b) = let val b' = case b of - Con.Rel x => RelC x - | Con.Named x => NamedC x + Con.RelK x => RelK x + | Con.RelC x => RelC x + | Con.NamedC x => NamedC x in bind (ctx, b') end @@ -288,7 +322,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = fn c' => (ECApp (e', c'), loc))) | ECAbs (expl, x, k, e) => - S.bind2 (mfk k, + S.bind2 (mfk ctx k, fn k' => S.map2 (mfe (bind (ctx, RelC (x, k))) e, fn e' => @@ -347,11 +381,6 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = fn rest' => (ECutMulti (e', c', {rest = rest'}), loc)))) - | EFold k => - S.map2 (mfk k, - fn k' => - (EFold k', loc)) - | ECase (e, pes, {disc, result}) => S.bind2 (mfe ctx e, fn e' => @@ -406,6 +435,17 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = (ELet (des', e'), loc))) end + | EKAbs (x, e) => + S.map2 (mfe (bind (ctx, RelK x)) e, + fn e' => + (EKAbs (x, e'), loc)) + | EKApp (e, k) => + S.bind2 (mfe ctx e, + fn e' => + S.map2 (mfk ctx k, + fn k' => + (EKApp (e', k'), loc))) + and mfed ctx (dAll as (d, loc)) = case d of EDVal vi => @@ -432,7 +472,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = end fun mapfold {kind = fk, con = fc, exp = fe} = - mapfoldB {kind = fk, + mapfoldB {kind = fn () => fk, con = fn () => fc, exp = fn () => fe, bind = fn ((), _) => ()} () @@ -457,7 +497,7 @@ fun exists {kind, con, exp} k = | S.Continue _ => false fun mapB {kind, con, exp, bind} ctx e = - case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()), + case mapfoldB {kind = fn ctx => fn k => fn () => S.Continue (kind ctx k, ()), con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()), exp = fn ctx => fn e => fn () => S.Continue (exp ctx e, ()), bind = bind} ctx e () of @@ -465,7 +505,7 @@ fun mapB {kind, con, exp, bind} ctx 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)), + case mapfoldB {kind = fn ctx => fn k => fn st => S.Continue (k, kind (ctx, 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 @@ -477,7 +517,8 @@ end structure Sgn = struct datatype binder = - RelC of string * Elab.kind + RelK of string + | RelC of string * Elab.kind | NamedC of string * int * Elab.kind | Str of string * Elab.sgn | Sgn of string * Elab.sgn @@ -487,14 +528,15 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} = fun bind' (ctx, b) = let val b' = case b of - Con.Rel x => RelC x - | Con.Named x => NamedC x + Con.RelK x => RelK x + | Con.RelC x => RelC x + | Con.NamedC x => NamedC x in bind (ctx, b') end val con = Con.mapfoldB {kind = kind, con = con, bind = bind'} - val kind = Kind.mapfold kind + val kind = Kind.mapfoldB {kind = kind, bind = fn (ctx, x) => bind (ctx, RelK x)} fun sgi ctx si acc = S.bindP (sgi' ctx si acc, sgn_item ctx) @@ -502,11 +544,11 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} = and sgi' ctx (siAll as (si, loc)) = case si of SgiConAbs (x, n, k) => - S.map2 (kind k, + S.map2 (kind ctx k, fn k' => (SgiConAbs (x, n, k'), loc)) | SgiCon (x, n, k, c) => - S.bind2 (kind k, + S.bind2 (kind ctx k, fn k' => S.map2 (con ctx c, fn c' => @@ -548,11 +590,11 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} = fn c2' => (SgiConstraint (c1', c2'), loc))) | SgiClassAbs (x, n, k) => - S.map2 (kind k, + S.map2 (kind ctx k, fn k' => (SgiClassAbs (x, n, k'), loc)) | SgiClass (x, n, k, c) => - S.bind2 (kind k, + S.bind2 (kind ctx k, fn k' => S.map2 (con ctx c, fn c' => @@ -608,7 +650,7 @@ fun mapfoldB {kind, con, sgn_item, sgn, bind} = end fun mapfold {kind, con, sgn_item, sgn} = - mapfoldB {kind = kind, + mapfoldB {kind = fn () => kind, con = fn () => con, sgn_item = fn () => sgn_item, sgn = fn () => sgn, @@ -627,7 +669,8 @@ end structure Decl = struct datatype binder = - RelC of string * Elab.kind + RelK of string + | RelC of string * Elab.kind | NamedC of string * int * Elab.kind | RelE of string * Elab.con | NamedE of string * Elab.con @@ -636,13 +679,14 @@ datatype binder = fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = fst, decl = fd, bind} = let - val mfk = Kind.mapfold fk + val mfk = Kind.mapfoldB {kind = fk, bind = fn (ctx, x) => bind (ctx, RelK x)} fun bind' (ctx, b) = let val b' = case b of - Con.Rel x => RelC x - | Con.Named x => NamedC x + Con.RelK x => RelK x + | Con.RelC x => RelC x + | Con.NamedC x => NamedC x in bind (ctx, b') end @@ -651,7 +695,8 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f fun bind' (ctx, b) = let val b' = case b of - Exp.RelC x => RelC x + Exp.RelK x => RelK x + | Exp.RelC x => RelC x | Exp.NamedC x => NamedC x | Exp.RelE x => RelE x | Exp.NamedE x => NamedE x @@ -663,7 +708,8 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f fun bind' (ctx, b) = let val b' = case b of - Sgn.RelC x => RelC x + Sgn.RelK x => RelK x + | Sgn.RelC x => RelC x | Sgn.NamedC x => NamedC x | Sgn.Sgn x => Sgn x | Sgn.Str x => Str x @@ -760,7 +806,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f and mfd' ctx (dAll as (d, loc)) = case d of DCon (x, n, k, c) => - S.bind2 (mfk k, + S.bind2 (mfk ctx k, fn k' => S.map2 (mfc ctx c, fn c' => @@ -825,7 +871,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f | DSequence _ => S.return2 dAll | DClass (x, n, k, c) => - S.bind2 (mfk k, + S.bind2 (mfk ctx k, fn k' => S.map2 (mfc ctx c, fn c' => @@ -849,7 +895,7 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, sgn_item = fsgi, sgn = fsg, str = f end fun mapfold {kind, con, exp, sgn_item, sgn, str, decl} = - mapfoldB {kind = kind, + mapfoldB {kind = fn () => kind, con = fn () => con, exp = fn () => exp, sgn_item = fn () => sgn_item, @@ -938,7 +984,7 @@ fun search {kind, con, exp, sgn_item, sgn, str, decl} k = | 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)), + case mapfoldB {kind = fn ctx => fn x => fn st => S.Continue (kind (ctx, 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)), diff --git a/src/elaborate.sml b/src/elaborate.sml index 0c335603..54543ae9 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -61,7 +61,7 @@ exception KUnify' of kunify_error - fun unifyKinds' (k1All as (k1, _)) (k2All as (k2, _)) = + fun unifyKinds' env (k1All as (k1, _)) (k2All as (k2, _)) = let fun err f = raise KUnify' (f (k1All, k2All)) in @@ -70,19 +70,27 @@ | (L'.KUnit, L'.KUnit) => () | (L'.KArrow (d1, r1), L'.KArrow (d2, r2)) => - (unifyKinds' d1 d2; - unifyKinds' r1 r2) + (unifyKinds' env d1 d2; + unifyKinds' env r1 r2) | (L'.KName, L'.KName) => () - | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' k1 k2 + | (L'.KRecord k1, L'.KRecord k2) => unifyKinds' env k1 k2 | (L'.KTuple ks1, L'.KTuple ks2) => - ((ListPair.appEq (fn (k1, k2) => unifyKinds' k1 k2) (ks1, ks2)) + ((ListPair.appEq (fn (k1, k2) => unifyKinds' env k1 k2) (ks1, ks2)) handle ListPair.UnequalLengths => err KIncompatible) + | (L'.KRel n1, L'.KRel n2) => + if n1 = n2 then + () + else + err KIncompatible + | (L'.KFun (x, k1), L'.KFun (_, k2)) => + unifyKinds' (E.pushKRel env x) k1 k2 + | (L'.KError, _) => () | (_, L'.KError) => () - | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' k1All k2All - | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' k1All k2All + | (L'.KUnif (_, _, ref (SOME k1All)), _) => unifyKinds' env k1All k2All + | (_, L'.KUnif (_, _, ref (SOME k2All))) => unifyKinds' env k1All k2All | (L'.KUnif (_, _, r1), L'.KUnif (_, _, r2)) => if r1 = r2 then @@ -106,12 +114,12 @@ exception KUnify of L'.kind * L'.kind * kunify_error - fun unifyKinds k1 k2 = - unifyKinds' k1 k2 + fun unifyKinds env k1 k2 = + unifyKinds' env k1 k2 handle KUnify' err => raise KUnify (k1, k2, err) fun checkKind env c k1 k2 = - unifyKinds k1 k2 + unifyKinds env k1 k2 handle KUnify (k1, k2, err) => conError env (WrongKind (c, k1, k2, err)) @@ -172,16 +180,23 @@ end - fun elabKind (k, loc) = + fun elabKind env (k, loc) = case k of L.KType => (L'.KType, loc) - | L.KArrow (k1, k2) => (L'.KArrow (elabKind k1, elabKind k2), loc) + | L.KArrow (k1, k2) => (L'.KArrow (elabKind env k1, elabKind env k2), loc) | L.KName => (L'.KName, loc) - | L.KRecord k => (L'.KRecord (elabKind k), loc) + | L.KRecord k => (L'.KRecord (elabKind env k), loc) | L.KUnit => (L'.KUnit, loc) - | L.KTuple ks => (L'.KTuple (map elabKind ks), loc) + | L.KTuple ks => (L'.KTuple (map (elabKind env) ks), loc) | L.KWild => kunif loc + | L.KVar s => (case E.lookupK env s of + NONE => + (kindError env (UnboundKind (loc, s)); + kerror) + | SOME n => (L'.KRel n, loc)) + | L.KFun (x, k) => (L'.KFun (x, elabKind (E.pushKRel env x) k), loc) + fun mapKind (dom, ran, loc)= (L'.KArrow ((L'.KArrow (dom, ran), loc), (L'.KArrow ((L'.KRecord dom, loc), @@ -192,11 +207,31 @@ L'.KUnif (_, _, ref (SOME k)) => hnormKind k | _ => kAll + open ElabOps + val hnormCon = D.hnormCon + + fun elabConHead (c as (_, loc)) k = + let + fun unravel (k, c) = + case hnormKind k of + (L'.KFun (x, k'), _) => + let + val u = kunif loc + + val k'' = subKindInKind (0, u) k' + in + unravel (k'', (L'.CKApp (c, u), loc)) + end + | _ => (c, k) + in + unravel (k, c) + end + fun elabCon (env, denv) (c, loc) = case c of L.CAnnot (c, k) => let - val k' = elabKind k + val k' = elabKind env k val (c', ck, gs) = elabCon (env, denv) c in checkKind env c' ck k'; @@ -215,13 +250,21 @@ | L.TCFun (e, x, k, t) => let val e' = elabExplicitness e - val k' = elabKind k + val k' = elabKind env k val env' = E.pushCRel env x k' val (t', tk, gs) = elabCon (env', D.enter denv) t in checkKind env t' tk ktype; ((L'.TCFun (e', x, k', t'), loc), ktype, gs) end + | L.TKFun (x, t) => + let + val env' = E.pushKRel env x + val (t', tk, gs) = elabCon (env', denv) t + in + checkKind env t' tk ktype; + ((L'.TKFun (x, t'), loc), ktype, gs) + end | L.CDisjoint (c1, c2, c) => let val (c1', k1, gs1) = elabCon (env, denv) c1 @@ -253,9 +296,17 @@ (conError env (UnboundCon (loc, s)); (cerror, kerror, [])) | E.Rel (n, k) => - ((L'.CRel n, loc), k, []) + let + val (c, k) = elabConHead (L'.CRel n, loc) k + in + (c, k, []) + end | E.Named (n, k) => - ((L'.CNamed n, loc), k, [])) + let + val (c, k) = elabConHead (L'.CNamed n, loc) k + in + (c, k, []) + end) | L.CVar (m1 :: ms, s) => (case E.lookupStr env m1 of NONE => (conError env (UnboundStrInCon (loc, m1)); @@ -292,7 +343,7 @@ let val k' = case ko of NONE => kunif loc - | SOME k => elabKind k + | SOME k => elabKind env k val env' = E.pushCRel env x k' val (t', tk, gs) = elabCon (env', D.enter denv) t in @@ -300,6 +351,15 @@ (L'.KArrow (k', tk), loc), gs) end + | L.CKAbs (x, t) => + let + val env' = E.pushKRel env x + val (t', tk, gs) = elabCon (env', denv) t + in + ((L'.CKAbs (x, t'), loc), + (L'.KFun (x, tk), loc), + gs) + end | L.CName s => ((L'.CName s, loc), kname, []) @@ -392,7 +452,7 @@ | L.CWild k => let - val k' = elabKind k + val k' = elabKind env k in (cunif (loc, k'), k', []) end @@ -431,8 +491,6 @@ exception SynUnif = E.SynUnif - open ElabOps - type record_summary = { fields : (L'.con * L'.con) list, unifs : (L'.con * L'.con option ref) list, @@ -499,7 +557,12 @@ | L'.CError => kerror | L'.CUnif (_, k, _, _) => k - val hnormCon = D.hnormCon + | L'.CKAbs (x, c) => (L'.KFun (x, kindof (E.pushKRel env x) c), loc) + | L'.CKApp (c, k) => + (case hnormKind (kindof env c) of + (L'.KFun (_, k'), _) => subKindInKind (0, k) k' + | k => raise CUnify' (CKindof (k, c, "kapp"))) + | L'.TKFun _ => ktype fun deConstraintCon (env, denv) c = let @@ -564,6 +627,10 @@ | L'.CError => false | L'.CUnif (_, k, _, _) => #1 k = L'.KUnit + | L'.CKAbs _ => false + | L'.CKApp _ => false + | L'.TKFun _ => false + fun unifyRecordCons (env, denv) (c1, c2) = let fun rkindof c = @@ -578,7 +645,7 @@ val (r1, gs1) = recordSummary (env, denv) c1 val (r2, gs2) = recordSummary (env, denv) c2 in - unifyKinds k1 k2; + unifyKinds env k1 k2; unifySummaries (env, denv) (k1, r1, r2); gs1 @ gs2 end @@ -848,12 +915,13 @@ val (c2, gs2) = hnormCon (env, denv) c2 in let + (*val () = prefaces "unifyCons'" [("old1", p_con env old1), + ("old2", p_con env old2), + ("c1", p_con env c1), + ("c2", p_con env c2)]*) + val gs3 = unifyCons'' (env, denv) c1 c2 in - (*prefaces "unifyCons'" [("c1", p_con env old1), - ("c2", p_con env old2), - ("t", PD.string (LargeReal.toString (Time.toReal - (Time.- (Time.now (), befor)))))];*) gs1 @ gs2 @ gs3 end handle ex => guessMap (env, denv) (c1, c2, gs1 @ gs2, ex) @@ -878,7 +946,7 @@ if expl1 <> expl2 then err CExplicitness else - (unifyKinds d1 d2; + (unifyKinds env d1 d2; let val denv' = D.enter denv (*val befor = Time.now ()*) @@ -906,7 +974,7 @@ (unifyCons' (env, denv) d1 d2; unifyCons' (env, denv) r1 r2) | (L'.CAbs (x1, k1, c1), L'.CAbs (_, k2, c2)) => - (unifyKinds k1 k2; + (unifyKinds env k1 k2; unifyCons' (E.pushCRel env x1 k1, D.enter denv) c1 c2) | (L'.CName n1, L'.CName n2) => @@ -954,6 +1022,19 @@ else err CIncompatible + | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) => + (unifyKinds env dom1 dom2; + unifyKinds env ran1 ran2; + []) + + | (L'.CKAbs (x, c1), L'.CKAbs (_, c2)) => + unifyCons' (E.pushKRel env x, denv) c1 c2 + | (L'.CKApp (c1, k1), L'.CKApp (c2, k2)) => + (unifyKinds env k1 k2; + unifyCons' (env, denv) c1 c2) + | (L'.TKFun (x, c1), L'.TKFun (_, c2)) => + unifyCons' (E.pushKRel env x, denv) c1 c2 + | (L'.CError, _) => [] | (_, L'.CError) => [] @@ -966,7 +1047,7 @@ if r1 = r2 then [] else - (unifyKinds k1 k2; + (unifyKinds env k1 k2; r1 := SOME c2All; []) @@ -983,11 +1064,6 @@ (r := SOME c1All; []) - | (L'.CMap (dom1, ran1), L'.CMap (dom2, ran2)) => - (unifyKinds dom1 dom2; - unifyKinds ran1 ran2; - []) - | _ => err CIncompatible end @@ -1013,36 +1089,7 @@ P.Int _ => !int | P.Float _ => !float | P.String _ => !string - - fun recCons (k, nm, v, rest, loc) = - (L'.CConcat ((L'.CRecord (k, [(nm, v)]), loc), - rest), loc) - - fun foldType (dom, loc) = - (L'.TCFun (L'.Explicit, "ran", (L'.KArrow ((L'.KRecord dom, loc), (L'.KType, loc)), loc), - (L'.TFun ((L'.TCFun (L'.Explicit, "nm", (L'.KName, loc), - (L'.TCFun (L'.Explicit, "v", dom, - (L'.TCFun (L'.Explicit, "rest", (L'.KRecord dom, loc), - (L'.TFun ((L'.CApp ((L'.CRel 3, loc), (L'.CRel 0, loc)), loc), - (L'.CDisjoint (L'.Instantiate, - (L'.CRecord - ((L'.KUnit, loc), - [((L'.CRel 2, loc), - (L'.CUnit, loc))]), loc), - (L'.CRel 0, loc), - (L'.CApp ((L'.CRel 3, loc), - recCons (dom, - (L'.CRel 2, loc), - (L'.CRel 1, loc), - (L'.CRel 0, loc), - loc)), loc)), - loc)), loc)), - loc)), loc)), loc), - (L'.TFun ((L'.CApp ((L'.CRel 0, loc), (L'.CRecord (dom, []), loc)), loc), - (L'.TCFun (L'.Explicit, "r", (L'.KRecord dom, loc), - (L'.CApp ((L'.CRel 1, loc), (L'.CRel 0, loc)), loc)), loc)), - loc)), loc)), loc) - + datatype constraint = Disjoint of D.goal | TypeClass of E.env * L'.con * L'.exp option ref * ErrorMsg.span @@ -1056,7 +1103,16 @@ val (t, gs) = hnormCon (env, denv) t in case t of - (L'.TCFun (L'.Implicit, x, k, t'), _) => + (L'.TKFun (x, t'), _) => + let + val u = kunif loc + + val t'' = subKindInCon (0, u) t' + val (e, t, gs') = unravel (t'', (L'.EKApp (e, u), loc)) + in + (e, t, enD gs @ gs') + end + | (L'.TCFun (L'.Implicit, x, k, t'), _) => let val u = cunif (loc, k) @@ -1575,7 +1631,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) = | L.ECAbs (expl, x, k, e) => let val expl' = elabExplicitness expl - val k' = elabKind k + val k' = elabKind env k val env' = E.pushCRel env x k' val (e', et, gs) = elabExp (env', D.enter denv) e @@ -1584,6 +1640,15 @@ fun elabExp (env, denv) (eAll as (e, loc)) = (L'.TCFun (expl', x, k', et), loc), gs) end + | L.EKAbs (x, e) => + let + val env' = E.pushKRel env x + val (e', et, gs) = elabExp (env', denv) e + in + ((L'.EKAbs (x, e'), loc), + (L'.TKFun (x, et), loc), + gs) + end | L.EDisjoint (c1, c2, e) => let @@ -1710,13 +1775,6 @@ fun elabExp (env, denv) (eAll as (e, loc)) = gs1 @ enD gs2 @ enD gs3 @ enD gs4) end - | L.EFold => - let - val dom = kunif loc - in - ((L'.EFold dom, loc), foldType (dom, loc), []) - end - | L.ECase (e, pes) => let val (e', et, gs1) = elabExp (env, denv) e @@ -1781,6 +1839,7 @@ and elabEdecl denv (dAll as (d, loc), (env, gs : constraint list)) = case e of L.EAbs _ => true | L.ECAbs (_, _, _, e) => allowable e + | L.EKAbs (_, e) => allowable e | L.EDisjoint (_, _, e) => allowable e | _ => false @@ -1859,7 +1918,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = case sgi of L.SgiConAbs (x, k) => let - val k' = elabKind k + val k' = elabKind env k val (env', n) = E.pushCNamed env x k' NONE in @@ -1870,7 +1929,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = let val k' = case ko of NONE => kunif loc - | SOME k => elabKind k + | SOME k => elabKind env k val (c', ck, gs') = elabCon (env, denv) c val (env', n) = E.pushCNamed env x k' (SOME c') @@ -1979,7 +2038,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = val (env', n) = E.pushENamed env x c' val c' = normClassConstraint env c' in - (unifyKinds ck ktype + (unifyKinds env ck ktype handle KUnify ue => strError env (NotType (ck, ue))); ([(L'.SgiVal (x, n, c'), loc)], (env', denv, gs' @ gs)) @@ -2027,7 +2086,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = | L.SgiClassAbs (x, k) => let - val k = elabKind k + val k = elabKind env k val k' = (L'.KArrow (k, (L'.KType, loc)), loc) val (env, n) = E.pushCNamed env x k' NONE val env = E.pushClass env n @@ -2037,7 +2096,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = | L.SgiClass (x, k, c) => let - val k = elabKind k + val k = elabKind env k val k' = (L'.KArrow (k, (L'.KType, loc)), loc) val (c', ck, gs) = elabCon (env, denv) c val (env, n) = E.pushCNamed env x k' (SOME c') @@ -2149,7 +2208,7 @@ and elabSgn (env, denv) (sgn, loc) = | L'.SgnConst sgis => if List.exists (fn (L'.SgiConAbs (x', _, k), _) => x' = x andalso - (unifyKinds k ck + (unifyKinds env k ck handle KUnify x => sgnError env (WhereWrongKind x); true) | _ => false) sgis then @@ -2355,7 +2414,7 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) = fun found (x', n1, k1, co1) = if x = x' then let - val () = unifyKinds k1 k2 + val () = unifyKinds env k1 k2 handle KUnify (k1, k2, err) => sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err)) val env = E.pushCNamedAs env x n1 k1 co1 @@ -2606,7 +2665,7 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) = fun found (x', n1, k1, co) = if x = x' then let - val () = unifyKinds k1 k2 + val () = unifyKinds env k1 k2 handle KUnify (k1, k2, err) => sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err)) @@ -2635,7 +2694,7 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) = fun found (x', n1, k1, c1) = if x = x' then let - val () = unifyKinds k1 k2 + val () = unifyKinds env k1 k2 handle KUnify (k1, k2, err) => sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err)) @@ -2702,6 +2761,9 @@ fun positive self = | CAbs _ => false | CDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3 + | CKAbs _ => false + | TKFun _ => false + | CName _ => true | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso none c2) xcs @@ -2728,6 +2790,9 @@ fun positive self = | CAbs _ => false | CDisjoint (c1, c2, c3) => none c1 andalso none c2 andalso none c3 + | CKAbs _ => false + | TKFun _ => false + | CName _ => true | CRecord xcs => List.all (fn (c1, c2) => none c1 andalso pos c2) xcs @@ -2777,6 +2842,9 @@ fun wildifyStr env (str, sgn) = | L'.KUnif (_, _, ref (SOME k)) => decompileKind k | L'.KUnif _ => NONE + | L'.KRel _ => NONE + | L'.KFun _ => NONE + fun decompileCon env (c, loc) = case c of L'.CRel i => @@ -2914,7 +2982,7 @@ fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) = let val k' = case ko of NONE => kunif loc - | SOME k => elabKind k + | SOME k => elabKind env k val (c', ck, gs') = elabCon (env, denv) c val (env', n) = E.pushCNamed env x k' (SOME c') @@ -3047,6 +3115,7 @@ fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) = case e of L.EAbs _ => true | L.ECAbs (_, _, _, e) => allowable e + | L.EKAbs (_, e) => allowable e | L.EDisjoint (_, _, e) => allowable e | _ => false @@ -3264,7 +3333,7 @@ fun elabDecl (dAll as (d, loc), (env, denv, gs : constraint list)) = | L.DClass (x, k, c) => let - val k = elabKind k + val k = elabKind env k val k' = (L'.KArrow (k, (L'.KType, loc)), loc) val (c', ck, gs') = elabCon (env, denv) c val (env, n) = E.pushCNamed env x k' (SOME c') diff --git a/src/expl.sml b/src/expl.sml index c0d291b5..0101dd1f 100644 --- a/src/expl.sml +++ b/src/expl.sml @@ -93,7 +93,6 @@ datatype exp' = | EConcat of exp * con * exp * con | ECut of exp * con * { field : con, rest : con } | ECutMulti of exp * con * { rest : con } - | EFold of kind | ECase of exp * (pat * exp) list * { disc : con, result : con } diff --git a/src/expl_print.sml b/src/expl_print.sml index 7044bfa2..313fef5c 100644 --- a/src/expl_print.sml +++ b/src/expl_print.sml @@ -351,7 +351,6 @@ fun p_exp' par env (e, loc) = string "---", space, p_con' true env c]) - | EFold _ => string "fold" | EWrite e => box [string "write(", p_exp env e, diff --git a/src/expl_util.sml b/src/expl_util.sml index a2b5f2f6..febf3586 100644 --- a/src/expl_util.sml +++ b/src/expl_util.sml @@ -311,10 +311,6 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = S.map2 (mfc ctx rest, fn rest' => (ECutMulti (e', c', {rest = rest'}), loc)))) - | EFold k => - S.map2 (mfk k, - fn k' => - (EFold k', loc)) | EWrite e => S.map2 (mfe ctx e, diff --git a/src/explify.sml b/src/explify.sml index a4eab0ba..5bce9268 100644 --- a/src/explify.sml +++ b/src/explify.sml @@ -107,8 +107,6 @@ fun explifyExp (e, loc) = {field = explifyCon field, rest = explifyCon rest}), loc) | L.ECutMulti (e1, c, {rest}) => (L'.ECutMulti (explifyExp e1, explifyCon c, {rest = explifyCon rest}), loc) - | L.EFold k => (L'.EFold (explifyKind k), loc) - | L.ECase (e, pes, {disc, result}) => (L'.ECase (explifyExp e, map (fn (p, e) => (explifyPat p, explifyExp e)) pes, diff --git a/src/monoize.sml b/src/monoize.sml index 898d3e61..96ef2c6a 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -2183,7 +2183,6 @@ fun monoExp (env, st, fm) (all as (e, loc)) = | L.EConcat _ => poly () | L.ECut _ => poly () | L.ECutMulti _ => poly () - | L.EFold _ => poly () | L.ECase (e, pes, {disc, result}) => let diff --git a/src/reduce.sml b/src/reduce.sml index 949b2a6d..77718b66 100644 --- a/src/reduce.sml +++ b/src/reduce.sml @@ -214,20 +214,6 @@ fun conAndExp (namedC, namedE) = in case #1 e of ECAbs (_, _, b) => exp (KnownC c :: deKnown env) b - - | EApp ((EApp ((ECApp ((EFold _, _), _), _), f), _), i) => - (case #1 c of - CRecord (_, []) => i - | CRecord (k, (nm, v) :: rest) => - let - val rest = (CRecord (k, rest), loc) - in - exp (deKnown env) - (EApp ((ECApp ((ECApp ((ECApp (f, nm), loc), v), loc), rest), loc), - (ECApp (e, rest), loc)), loc) - end - | _ => (ECApp (e, c), loc)) - | _ => (ECApp (e, c), loc) end @@ -334,8 +320,6 @@ fun conAndExp (namedC, namedE) = | _ => default () end - | EFold _ => all - | ECase (e, pes, {disc, result}) => let fun patBinds (p, _) = diff --git a/src/reduce_local.sml b/src/reduce_local.sml index 7de7d799..25b1023a 100644 --- a/src/reduce_local.sml +++ b/src/reduce_local.sml @@ -107,8 +107,6 @@ fun exp env (all as (e, loc)) = | ECut (e, c, others) => (ECut (exp env e, c, others), loc) | ECutMulti (e, c, others) => (ECutMulti (exp env e, c, others), loc) - | EFold _ => all - | ECase (e, pes, others) => let fun patBinds (p, _) = diff --git a/src/source.sml b/src/source.sml index d70d0f5d..e9531245 100644 --- a/src/source.sml +++ b/src/source.sml @@ -38,6 +38,9 @@ datatype kind' = | KTuple of kind list | KWild + | KFun of string * kind + | KVar of string + withtype kind = kind' located datatype explicitness = @@ -56,6 +59,9 @@ datatype con' = | CAbs of string * kind option * con | CDisjoint of con * con * con + | CKAbs of string * con + | TKFun of string * con + | CName of string | CRecord of (con * con) list @@ -119,12 +125,13 @@ datatype exp' = | ECAbs of explicitness * string * kind * exp | EDisjoint of con * con * exp + | EKAbs of string * exp + | ERecord of (con * exp) list | EField of exp * con | EConcat of exp * exp | ECut of exp * con | ECutMulti of exp * con - | EFold | EWild diff --git a/src/source_print.sml b/src/source_print.sml index 148157c2..f2420947 100644 --- a/src/source_print.sml +++ b/src/source_print.sml @@ -50,6 +50,13 @@ fun p_kind' par (k, _) = p_list_sep (box [space, string "*", space]) p_kind ks, string ")"] + | KVar x => string x + | KFun (x, k) => box [string x, + space, + string "-->", + space, + p_kind k] + and p_kind k = p_kind' false k fun p_explicitness e = @@ -156,6 +163,17 @@ fun p_con' par (c, _) = | CProj (c, n) => box [p_con c, string ".", string (Int.toString n)] + + | CKAbs (x, c) => box [string x, + space, + string "==>", + space, + p_con c] + | TKFun (x, c) => box [string x, + space, + string "-->", + space, + p_con c] and p_con c = p_con' false c @@ -273,8 +291,6 @@ fun p_exp' par (e, _) = string "---", space, p_con' true c]) - | EFold => string "fold" - | ECase (e, pes) => parenIf par (box [string "case", space, p_exp e, @@ -300,6 +316,12 @@ fun p_exp' par (e, _) = newline, string "end"] + | EKAbs (x, e) => box [string x, + space, + string "-->", + space, + p_exp e] + and p_exp e = p_exp' false e and p_edecl (d, _) = diff --git a/src/termination.sml b/src/termination.sml index e89f329e..5dd95f46 100644 --- a/src/termination.sml +++ b/src/termination.sml @@ -190,6 +190,7 @@ fun declOk' env (d, loc) = in (p, ps, calls) end + | EKApp (e, _) => combiner calls e | _ => let val (p, calls) = exp parent (penv, calls) e @@ -239,6 +240,13 @@ fun declOk' env (d, loc) = in (Rabble, calls) end + | EKApp _ => apps () + | EKAbs (_, e) => + let + val (_, calls) = exp parent (penv, calls) e + in + (Rabble, calls) + end | ERecord xets => let @@ -278,7 +286,6 @@ fun declOk' env (d, loc) = in (Rabble, calls) end - | EFold _ => (Rabble, calls) | ECase (e, pes, _) => let diff --git a/src/unnest.sml b/src/unnest.sml index 8e363301..1d0c2388 100644 --- a/src/unnest.sml +++ b/src/unnest.sml @@ -37,7 +37,7 @@ structure U = ElabUtil structure IS = IntBinarySet fun liftExpInExp by = - U.Exp.mapB {kind = fn k => k, + U.Exp.mapB {kind = fn _ => fn k => k, con = fn _ => fn c => c, exp = fn bound => fn e => case e of @@ -51,7 +51,7 @@ fun liftExpInExp by = | (bound, _) => bound} val subExpInExp = - U.Exp.mapB {kind = fn k => k, + U.Exp.mapB {kind = fn _ => fn k => k, con = fn _ => fn c => c, exp = fn (xn, rep) => fn e => case e of @@ -65,7 +65,7 @@ val subExpInExp = | ((xn, rep), U.Exp.RelC _) => (xn, E.liftConInExp 0 rep) | (ctx, _) => ctx} -val fvsCon = U.Con.foldB {kind = fn (_, st) => st, +val fvsCon = U.Con.foldB {kind = fn (_, _, st) => st, con = fn (cb, c, cvs) => case c of CRel n => @@ -76,11 +76,11 @@ val fvsCon = U.Con.foldB {kind = fn (_, st) => st, | _ => cvs, bind = fn (cb, b) => case b of - U.Con.Rel _ => cb + 1 + U.Con.RelC _ => cb + 1 | _ => cb} 0 IS.empty -fun fvsExp nr = U.Exp.foldB {kind = fn (_, st) => st, +fun fvsExp nr = U.Exp.foldB {kind = fn (_, _, st) => st, con = fn ((cb, eb), c, st as (cvs, evs)) => case c of CRel n => @@ -124,7 +124,7 @@ fun positionOf (x : int) ls = end fun squishCon cfv = - U.Con.mapB {kind = fn k => k, + U.Con.mapB {kind = fn _ => fn k => k, con = fn cb => fn c => case c of CRel n => @@ -135,12 +135,12 @@ fun squishCon cfv = | _ => c, bind = fn (cb, b) => case b of - U.Con.Rel _ => cb + 1 + U.Con.RelC _ => cb + 1 | _ => cb} 0 fun squishExp (nr, cfv, efv) = - U.Exp.mapB {kind = fn k => k, + U.Exp.mapB {kind = fn _ => fn k => k, con = fn (cb, eb) => fn c => case c of CRel n => @@ -169,7 +169,7 @@ type state = { decls : (string * int * con * exp) list } -fun kind (k, st) = (k, st) +fun kind (_, k, st) = (k, st) fun exp ((ks, ts), e as old, st : state) = case e of diff --git a/src/urweb.grm b/src/urweb.grm index d425caec..b6e4ce72 100644 --- a/src/urweb.grm +++ b/src/urweb.grm @@ -184,10 +184,10 @@ fun tagIn bt = | LPAREN | RPAREN | LBRACK | RBRACK | LBRACE | RBRACE | EQ | COMMA | COLON | DCOLON | TCOLON | DOT | HASH | UNDER | UNDERUNDER | BAR | PLUS | MINUS | DIVIDE | DOTDOTDOT | MOD | AT - | CON | LTYPE | VAL | REC | AND | FUN | MAP | FOLD | UNIT | KUNIT | CLASS + | CON | LTYPE | VAL | REC | AND | FUN | MAP | UNIT | KUNIT | CLASS | DATATYPE | OF | TYPE | NAME - | ARROW | LARROW | DARROW | STAR | SEMI + | ARROW | LARROW | DARROW | STAR | SEMI | KARROW | DKARROW | FN | PLUSPLUS | MINUSMINUS | MINUSMINUSMINUS | DOLLAR | TWIDDLE | LET | IN | STRUCTURE | SIGNATURE | STRUCT | SIG | END | FUNCTOR | WHERE | EXTERN | SQL @@ -327,6 +327,8 @@ fun tagIn bt = %name Urweb +%right KARROW +%nonassoc DKARROW %right SEMI %nonassoc LARROW %nonassoc IF THEN ELSE @@ -575,6 +577,8 @@ kind : TYPE (KType, s (TYPEleft, TYPEright)) | KUNIT (KUnit, s (KUNITleft, KUNITright)) | UNDERUNDER (KWild, s (UNDERUNDERleft, UNDERUNDERright)) | LPAREN ktuple RPAREN (KTuple ktuple, s (LPARENleft, RPARENright)) + | CSYMBOL (KVar CSYMBOL, s (CSYMBOLleft, CSYMBOLright)) + | CSYMBOL KARROW kind (KFun (CSYMBOL, kind), s (CSYMBOLleft, kindright)) ktuple : kind STAR kind ([kind1, kind2]) | kind STAR ktuple (kind :: ktuple) @@ -585,10 +589,12 @@ capps : cterm (cterm) cexp : capps (capps) | cexp ARROW cexp (TFun (cexp1, cexp2), s (cexp1left, cexp2right)) | SYMBOL kcolon kind ARROW cexp (TCFun (kcolon, SYMBOL, kind, cexp), s (SYMBOLleft, cexpright)) + | CSYMBOL KARROW cexp (TKFun (CSYMBOL, cexp), s (CSYMBOLleft, cexpright)) | cexp PLUSPLUS cexp (CConcat (cexp1, cexp2), s (cexp1left, cexp1right)) | FN cargs DARROW cexp (#1 (cargs (cexp, (KWild, s (FNleft, cexpright))))) + | CSYMBOL DKARROW cexp (CKAbs (CSYMBOL, cexp), s (CSYMBOLleft, cexpright)) | LPAREN cexp RPAREN DCOLON kind (CAnnot (cexp, kind), s (LPARENleft, kindright)) @@ -651,7 +657,7 @@ cargp : SYMBOL (fn (c, k) => ((CAbs (SYMBOL, SOME kind, c), loc), (KArrow (kind, k), loc)) end) - | LBRACK cexp TWIDDLE cexp RBRACK (fn (c, k) => + | LBRACK cexp TWIDDLE cexp RBRACK (fn (c, k) => let val loc = s (LBRACKleft, RBRACKright) in @@ -716,6 +722,7 @@ eexp : eapps (eapps) in #1 (eargs (eexp, (CWild (KType, loc), loc))) end) + | CSYMBOL DKARROW eexp (EKAbs (CSYMBOL, eexp), s (CSYMBOLleft, eexpright)) | eexp COLON cexp (EAnnot (eexp, cexp), s (eexpleft, cexpright)) | eexp MINUSMINUS cexp (ECut (eexp, cexp), s (eexpleft, cexpright)) | eexp MINUSMINUSMINUS cexp (ECutMulti (eexp, cexp), s (eexpleft, cexpright)) @@ -851,6 +858,13 @@ eargp : SYMBOL (fn (e, t) => ((EDisjoint (cexp1, cexp2, e), loc), (CDisjoint (cexp1, cexp2, t), loc)) end) + | CSYMBOL (fn (e, t) => + let + val loc = s (CSYMBOLleft, CSYMBOLright) + in + ((EKAbs (CSYMBOL, e), loc), + (TKFun (CSYMBOL, t), loc)) + end) eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright)) | LPAREN etuple RPAREN (let @@ -895,7 +909,6 @@ eterm : LPAREN eexp RPAREN (#1 eexp, s (LPARENleft, RPARENright)) (EField (e, ident), loc)) (EVar (#1 path, #2 path, DontInfer), s (pathleft, pathright)) idents end) - | FOLD (EFold, s (FOLDleft, FOLDright)) | XML_BEGIN xml XML_END (let val loc = s (XML_BEGINleft, XML_ENDright) @@ -1070,7 +1083,7 @@ xmlOne : NOTAGS (EApp ((EVar (["Basis"], "cdata", Infer) () else ErrorMsg.errorAt pos "Begin and end tags don't match."; - (EFold, pos)) + (EWild, pos)) end) | LBRACE eexp RBRACE (eexp) | LBRACE LBRACK eexp RBRACK RBRACE (let diff --git a/src/urweb.lex b/src/urweb.lex index 29e07194..bb57f03d 100644 --- a/src/urweb.lex +++ b/src/urweb.lex @@ -247,7 +247,9 @@ notags = [^<{\n]+; "}" => (exitBrace (); Tokens.RBRACE (pos yypos, pos yypos + size yytext)); + "-->" => (Tokens.KARROW (pos yypos, pos yypos + size yytext)); "->" => (Tokens.ARROW (pos yypos, pos yypos + size yytext)); + "==>" => (Tokens.DKARROW (pos yypos, pos yypos + size yytext)); "=>" => (Tokens.DARROW (pos yypos, pos yypos + size yytext)); "++" => (Tokens.PLUSPLUS (pos yypos, pos yypos + size yytext)); "--" => (Tokens.MINUSMINUS (pos yypos, pos yypos + size yytext)); @@ -291,7 +293,6 @@ notags = [^<{\n]+; "fun" => (Tokens.FUN (pos yypos, pos yypos + size yytext)); "fn" => (Tokens.FN (pos yypos, pos yypos + size yytext)); "map" => (Tokens.MAP (pos yypos, pos yypos + size yytext)); - "fold" => (Tokens.FOLD (pos yypos, pos yypos + size yytext)); "case" => (Tokens.CASE (pos yypos, pos yypos + size yytext)); "if" => (Tokens.IF (pos yypos, pos yypos + size yytext)); "then" => (Tokens.THEN (pos yypos, pos yypos + size yytext)); -- cgit v1.2.3 From a75aaa90b3b827f9ef002491bc081df36260f136 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 9 Apr 2009 12:31:56 -0400 Subject: Made type class system very general; demo compiles --- lib/ur/basis.urs | 2 +- src/elab_env.sig | 1 + src/elab_env.sml | 552 +++++++++++++++++++++--------------------------------- src/elab_err.sml | 12 +- src/elab_util.sig | 4 + src/elab_util.sml | 19 +- src/elaborate.sml | 45 ++--- src/urweb.grm | 3 +- 8 files changed, 264 insertions(+), 374 deletions(-) (limited to 'src/elab_env.sig') diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs index d69ddfcb..87f20d6b 100644 --- a/lib/ur/basis.urs +++ b/lib/ur/basis.urs @@ -71,7 +71,7 @@ val read_time : read time (** * Monads *) -class monad :: Type -> Type +class monad :: (Type -> Type) -> Type val return : m ::: (Type -> Type) -> t ::: Type -> monad m -> t -> m t diff --git a/src/elab_env.sig b/src/elab_env.sig index 10d11e3b..4b927a16 100644 --- a/src/elab_env.sig +++ b/src/elab_env.sig @@ -72,6 +72,7 @@ signature ELAB_ENV = sig val pushClass : env -> int -> env val isClass : env -> Elab.con -> bool val resolveClass : env -> Elab.con -> Elab.exp option + val listClasses : env -> (Elab.con * (Elab.con * Elab.exp) list) list val pushERel : env -> string -> Elab.con -> env val lookupERel : env -> int -> string * Elab.con diff --git a/src/elab_env.sml b/src/elab_env.sml index 8da78375..1c3eb62e 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -162,6 +162,11 @@ datatype class_name = ClNamed of int | ClProj of int * string list * string +fun class_name_out cn = + case cn of + ClNamed n => (CNamed n, ErrorMsg.dummySpan) + | ClProj x => (CModProj x, ErrorMsg.dummySpan) + fun cn2s cn = case cn of ClNamed n => "Named(" ^ Int.toString n ^ ")" @@ -185,71 +190,10 @@ end structure CS = BinarySetFn(CK) structure CM = BinaryMapFn(CK) -datatype class_key = - CkNamed of int - | CkRel of int - | CkProj of int * string list * string - | CkApp of class_key * class_key - | CkOther of con - -fun ck2s ck = - case ck of - CkNamed n => "Named(" ^ Int.toString n ^ ")" - | CkRel n => "Rel(" ^ Int.toString n ^ ")" - | CkProj (m, ms, x) => "Proj(" ^ Int.toString m ^ "," ^ String.concatWith "," ms ^ "," ^ x ^ ")" - | CkApp (ck1, ck2) => "App(" ^ ck2s ck1 ^ ", " ^ ck2s ck2 ^ ")" - | CkOther _ => "Other" - -type class_key_n = class_key * int - -fun ckn2s (ck, n) = ck2s ck ^ "[" ^ Int.toString n ^ "]" - -fun cp2s (cn, ck) = "(" ^ cn2s cn ^ "," ^ ck2s ck ^ ")" - -structure KK = struct -type ord_key = class_key_n -open Order -fun compare' x = - case x of - (CkNamed n1, CkNamed n2) => Int.compare (n1, n2) - | (CkNamed _, _) => LESS - | (_, CkNamed _) => GREATER - - | (CkRel n1, CkRel n2) => Int.compare (n1, n2) - | (CkRel _, _) => LESS - | (_, CkRel _) => GREATER - - | (CkProj (m1, ms1, x1), CkProj (m2, ms2, x2)) => - join (Int.compare (m1, m2), - fn () => join (joinL String.compare (ms1, ms2), - fn () => String.compare (x1, x2))) - | (CkProj _, _) => LESS - | (_, CkProj _) => GREATER - - | (CkApp (f1, x1), CkApp (f2, x2)) => - join (compare' (f1, f2), - fn () => compare' (x1, x2)) - | (CkApp _, _) => LESS - | (_, CkApp _) => GREATER - - | (CkOther _, CkOther _) => EQUAL -fun compare ((k1, n1), (k2, n2)) = - join (Int.compare (n1, n2), - fn () => compare' (k1, k2)) -end - -structure KM = BinaryMapFn(KK) - -type class = {ground : ((class_name * class_key) list * exp) KM.map, - inclusions : exp CM.map} -val empty_class = {ground = KM.empty, - inclusions = CM.empty} - -fun printClasses cs = (print "Classes:\n"; - CM.appi (fn (cn, {ground = km, ...} : class) => - (print (cn2s cn ^ ":"); - KM.appi (fn (ck, _) => print (" " ^ ckn2s ck)) km; - print "\n")) cs) +type class = {ground : (con * exp) list, + rules : (int * con list * con * exp) list} +val empty_class = {ground = [], + rules = []} type env = { renameK : int SM.map, @@ -309,16 +253,6 @@ val empty = { str = IM.empty } -fun liftClassKey' ck = - case ck of - CkNamed _ => ck - | CkRel n => CkRel (n + 1) - | CkProj _ => ck - | CkApp (ck1, ck2) => CkApp (liftClassKey' ck1, liftClassKey' ck2) - | CkOther c => CkOther (lift c) - -fun liftClassKey (ck, n) = (liftClassKey' ck, n) - fun pushKRel (env : env) x = let val renameK = SM.map (fn n => n+1) (#renameK env) @@ -334,7 +268,12 @@ fun pushKRel (env : env) x = datatypes = #datatypes env, constructors = #constructors env, - classes = #classes env, + classes = CM.map (fn cl => {ground = map (fn (c, e) => + (liftKindInCon 0 c, + e)) + (#ground cl), + rules = #rules cl}) + (#classes env), renameE = SM.map (fn Rel' (n, c) => Rel' (n, liftKindInCon 0 c) | Named' (n, c) => Named' (n, c)) (#renameE env), @@ -371,10 +310,11 @@ fun pushCRel (env : env) x k = constructors = #constructors env, classes = CM.map (fn class => - {ground = KM.foldli (fn (ck, e, km) => - KM.insert (km, liftClassKey ck, e)) - KM.empty (#ground class), - inclusions = #inclusions class}) + {ground = map (fn (c, e) => + (liftConInCon 0 c, + e)) + (#ground class), + rules = #rules class}) (#classes env), renameE = SM.map (fn Rel' (n, c) => Rel' (n, lift c) @@ -482,6 +422,23 @@ fun lookupConstructor (env : env) s = SM.find (#constructors env, s) fun datatypeArgs (xs, _) = xs fun constructors (_, dt) = IM.foldri (fn (n, (x, to), ls) => (x, n, to) :: ls) [] dt +fun listClasses (env : env) = + map (fn (cn, {ground, rules}) => + (class_name_out cn, + ground + @ map (fn (nvs, cs, c, e) => + let + val loc = #2 c + val c = foldr (fn (c', c) => (TFun (c', c), loc)) c cs + val c = ListUtil.foldli (fn (n, (), c) => (TCFun (Explicit, + "x" ^ Int.toString n, + (KError, loc), + c), loc)) + c (List.tabulate (nvs, fn _ => ())) + in + (c, e) + end) rules)) (CM.listItemsi (#classes env)) + fun pushClass (env : env) n = {renameK = #renameK env, relK = #relK env, @@ -520,133 +477,169 @@ fun isClass (env : env) c = find (class_name_in c) end -fun class_key_in (all as (c, _)) = - case c of - CRel n => CkRel n - | CNamed n => CkNamed n - | CModProj x => CkProj x - | CUnif (_, _, _, ref (SOME c)) => class_key_in c - | CApp (c1, c2) => CkApp (class_key_in c1, class_key_in c2) - | _ => CkOther all - -fun class_key_out loc = +fun class_head_in c = + case #1 c of + CApp (f, _) => class_head_in f + | CUnif (_, _, _, ref (SOME c)) => class_head_in c + | _ => class_name_in c + +exception Unify + +fun unifyKinds (k1, k2) = + case (#1 k1, #1 k2) of + (KType, KType) => () + | (KArrow (d1, r1), KArrow (d2, r2)) => (unifyKinds (d1, d2); unifyKinds (r1, r2)) + | (KName, KName) => () + | (KRecord k1, KRecord k2) => unifyKinds (k1, k2) + | (KUnit, KUnit) => () + | (KTuple ks1, KTuple ks2) => (ListPair.appEq unifyKinds (ks1, ks2) + handle ListPair.UnequalLengths => raise Unify) + | (KUnif (_, _, ref (SOME k1)), _) => unifyKinds (k1, k2) + | (_, KUnif (_, _, ref (SOME k2))) => unifyKinds (k1, k2) + | (KRel n1, KRel n2) => if n1 = n2 then () else raise Unify + | (KFun (_, k1), KFun (_, k2)) => unifyKinds (k1, k2) + | _ => raise Unify + +fun unifyCons rs = let - fun cko k = - case k of - CkRel n => (CRel n, loc) - | CkNamed n => (CNamed n, loc) - | CkProj x => (CModProj x, loc) - | CkApp (k1, k2) => (CApp (cko k1, cko k2), loc) - | CkOther c => c + fun unify d (c1, c2) = + case (#1 c1, #1 c2) of + (CUnif (_, _, _, ref (SOME c1)), _) => unify d (c1, c2) + | (_, CUnif (_, _, _, ref (SOME c2))) => unify d (c1, c2) + + | (c1', CRel n2) => + if n2 < d then + case c1' of + CRel n1 => if n1 = n2 then () else raise Unify + | _ => raise Unify + else if n2 - d >= length rs then + case c1' of + CRel n1 => if n1 = n2 - length rs then () else raise Unify + | _ => raise Unify + else + let + val r = List.nth (rs, n2 - d) + in + case !r of + NONE => r := SOME c1 + | SOME c2 => unify d (c1, c2) + end + + | (TFun (d1, r1), TFun (d2, r2)) => (unify d (d1, d2); unify d (r1, r2)) + | (TCFun (_, _, k1, r1), TCFun (_, _, k2, r2)) => (unifyKinds (k1, k2); unify (d + 1) (r1, r2)) + | (TRecord c1, TRecord c2) => unify d (c1, c2) + | (TDisjoint (a1, b1, c1), TDisjoint (a2, b2, c2)) => + (unify d (a1, a2); unify d (b1, b2); unify d (c1, c2)) + + | (CNamed n1, CNamed n2) => if n1 = n2 then () else raise Unify + | (CModProj (n1, ms1, x1), CModProj (n2, ms2, x2)) => + if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then () else raise Unify + | (CApp (f1, x1), CApp (f2, x2)) => (unify d (f1, f2); unify d (x1, x2)) + | (CAbs (_, k1, b1), CAbs (_, k2, b2)) => (unifyKinds (k1, k2); unify (d + 1) (b1, b2)) + + | (CKAbs (_, b1), CKAbs (_, b2)) => unify d (b1, b2) + | (CKApp (c1, k1), CKApp (c2, k2)) => (unify d (c1, c2); unifyKinds (k1, k2)) + | (TKFun (_, c1), TKFun (_, c2)) => unify d (c1, c2) + + | (CName s1, CName s2) => if s1 = s2 then () else raise Unify + + | (CRecord (k1, xcs1), CRecord (k2, xcs2)) => + (unifyKinds (k1, k2); + ListPair.appEq (fn ((x1, c1), (x2, c2)) => (unify d (x1, x2); unify d (c1, c2))) (xcs1, xcs2) + handle ListPair.UnequalLengths => raise Unify) + | (CConcat (f1, x1), CConcat (f2, x2)) => (unify d (f1, f2); unify d (x1, x2)) + | (CMap (d1, r1), CMap (d2, r2)) => (unifyKinds (d1, d2); unifyKinds (r1, r2)) + + | (CUnit, CUnit) => () + + | (CTuple cs1, CTuple cs2) => (ListPair.appEq (unify d) (cs1, cs2) + handle ListPair.UnequalLengths => raise Unify) + | (CProj (c1, n1), CProj (c2, n2)) => (unify d (c1, c2); + if n1 = n2 then () else raise Unify) + + | _ => raise Unify in - cko + unify end -fun class_pair_in (c, _) = - case c of - CApp (f, x) => - (case class_name_in f of - SOME f => SOME (f, class_key_in x) - | _ => NONE) - | CUnif (_, _, _, ref (SOME c)) => class_pair_in c - | _ => NONE - -fun sub_class_key (n, c) = +fun tryUnify nRs (c1, c2) = let - fun csk k = - case k of - CkRel n' => SOME (if n' = n then - c - else - k) - | CkNamed _ => SOME k - | CkProj _ => SOME k - | CkApp (k1, k2) => - (case (csk k1, csk k2) of - (SOME k1, SOME k2) => SOME (CkApp (k1, k2)) - | _ => NONE) - | CkOther _ => NONE + val rs = List.tabulate (nRs, fn _ => ref NONE) in - csk + (unifyCons rs 0 (c1, c2); + SOME (map (fn r => case !r of + NONE => raise Unify + | SOME c => c) rs)) + handle Unify => NONE end -fun resolveClass (env : env) c = +fun unifySubst (rs : con list) = + U.Con.mapB {kind = fn _ => fn k => k, + con = fn d => fn c => + case c of + CRel n => + if n < d then + c + else + #1 (List.nth (rs, n - d)) + | _ => c, + bind = fn (d, U.Con.RelC _) => d + 1 + | (d, _) => d} + 0 + +fun resolveClass (env : env) = let - fun doPair (f, x) = - case CM.find (#classes env, f) of - NONE => NONE - | SOME class => - let - val loc = #2 c - - fun tryIncs () = + fun resolve c = + let + fun doHead f = + case CM.find (#classes env, f) of + NONE => NONE + | SOME class => let - fun tryIncs fs = - case fs of + val loc = #2 c + + fun tryRules rules = + case rules of [] => NONE - | (f', e') :: fs => - case doPair (f', x) of - NONE => tryIncs fs - | SOME e => + | (nRs, cs, c', e) :: rules' => + case tryUnify nRs (c, c') of + NONE => tryRules rules' + | SOME rs => let - val e' = (ECApp (e', class_key_out loc x), loc) - val e' = (EApp (e', e), loc) + val eos = map (resolve o unifySubst rs) cs in - SOME e' + if List.exists (not o Option.isSome) eos then + tryRules rules' + else + let + val es = List.mapPartial (fn x => x) eos + + val e = foldr (fn (c, e) => (ECApp (e, c), loc)) e rs + val e = foldl (fn (e', e) => (EApp (e, e'), loc)) e es + in + SOME e + end end - in - tryIncs (CM.listItemsi (#inclusions class)) - end - fun tryRules (k, args) = - let - val len = length args - - fun tryNext () = - case k of - CkApp (k1, k2) => tryRules (k1, k2 :: args) - | _ => tryIncs () + fun rules () = tryRules (#rules class) + + fun tryGrounds ces = + case ces of + [] => rules () + | (c', e) :: ces' => + case tryUnify 0 (c, c') of + NONE => tryGrounds ces' + | SOME _ => SOME e in - case KM.find (#ground class, (k, length args)) of - SOME (cs, e) => - let - val es = map (fn (cn, ck) => - let - val ck = ListUtil.foldli (fn (i, arg, ck) => - case ck of - NONE => NONE - | SOME ck => - sub_class_key (len - i - 1, - arg) - ck) - (SOME ck) args - in - case ck of - NONE => NONE - | SOME ck => doPair (cn, ck) - end) cs - in - if List.exists (not o Option.isSome) es then - tryNext () - else - let - val e = foldl (fn (arg, e) => (ECApp (e, class_key_out loc arg), loc)) - e args - val e = foldr (fn (pf, e) => (EApp (e, pf), loc)) - e (List.mapPartial (fn x => x) es) - in - SOME e - end - end - | NONE => tryNext () + tryGrounds (#ground class) end - in - tryRules (x, []) - end + in + case class_head_in c of + SOME f => doHead f + | _ => NONE + end in - case class_pair_in c of - SOME p => doPair p - | _ => NONE + resolve end fun pushERel (env : env) x t = @@ -655,17 +648,17 @@ fun pushERel (env : env) x t = | x => x) (#renameE env) val classes = CM.map (fn class => - {ground = KM.map (fn (ps, e) => (ps, liftExp e)) (#ground class), - inclusions = #inclusions class}) (#classes env) - val classes = case class_pair_in t of + {ground = map (fn (c, e) => (c, liftExp e)) (#ground class), + rules = #rules class}) (#classes env) + val classes = case class_head_in t of NONE => classes - | SOME (f, x) => + | SOME f => case CM.find (classes, f) of NONE => classes | SOME class => let - val class = {ground = KM.insert (#ground class, (x, 0), ([], (ERel 0, #2 t))), - inclusions = #inclusions class} + val class = {ground = (t, (ERel 0, #2 t)) :: #ground class, + rules = #rules class} in CM.insert (classes, f, class) end @@ -697,16 +690,6 @@ fun lookupERel (env : env) n = (List.nth (#relE env, n)) handle Subscript => raise UnboundRel n -datatype rule = - Normal of int * (class_name * class_key) list * class_key - | Inclusion of class_name - -fun containsOther k = - case k of - CkOther _ => true - | CkApp (k1, k2) => containsOther k1 orelse containsOther k2 - | _ => false - fun rule_in c = let fun quantifiers (c, nvars) = @@ -717,68 +700,18 @@ fun rule_in c = fun clauses (c, hyps) = case #1 c of TFun (hyp, c) => - (case class_pair_in hyp of - SOME (p as (_, CkRel _)) => clauses (c, p :: hyps) - | _ => NONE) + (case class_head_in hyp of + SOME _ => clauses (c, hyp :: hyps) + | NONE => NONE) | _ => - case class_pair_in c of + case class_head_in c of NONE => NONE - | SOME (cn, ck) => - let - fun dearg (ck, i) = - if i >= nvars then - if containsOther ck - orelse List.exists (fn (_, k) => containsOther k) hyps then - NONE - else - SOME (cn, Normal (nvars, hyps, ck)) - else case ck of - CkApp (ck, CkRel i') => - if i' = i then - dearg (ck, i + 1) - else - NONE - | _ => NONE - in - dearg (ck, 0) - end + | SOME f => SOME (f, nvars, rev hyps, c) in clauses (c, []) end in - case #1 c of - TCFun (_, _, _, (TFun ((CApp (f1, (CRel 0, _)), _), - (CApp (f2, (CRel 0, _)), _)), _)) => - (case (class_name_in f1, class_name_in f2) of - (SOME f1, SOME f2) => SOME (f2, Inclusion f1) - | _ => NONE) - | _ => quantifiers (c, 0) - end - -fun inclusion (classes : class CM.map, init, inclusions, f, e : exp) = - let - fun search (f, fs) = - if f = init then - NONE - else if CS.member (fs, f) then - SOME fs - else - let - val fs = CS.add (fs, f) - in - case CM.find (classes, f) of - NONE => SOME fs - | SOME {inclusions = fs', ...} => - CM.foldli (fn (f', _, fs) => - case fs of - NONE => NONE - | SOME fs => search (f', fs)) (SOME fs) fs' - end - in - case search (f, CS.empty) of - SOME _ => CM.insert (inclusions, f, e) - | NONE => (ErrorMsg.errorAt (#2 e) "Type class inclusion would create a cycle"; - inclusions) + quantifiers (c, 0) end fun pushENamedAs (env : env) x n t = @@ -786,7 +719,7 @@ fun pushENamedAs (env : env) x n t = val classes = #classes env val classes = case rule_in t of NONE => classes - | SOME (f, rule) => + | SOME (f, nvs, cs, c) => case CM.find (classes, f) of NONE => classes | SOME class => @@ -794,13 +727,8 @@ fun pushENamedAs (env : env) x n t = val e = (ENamed n, #2 t) val class = - case rule of - Normal (nvars, hyps, x) => - {ground = KM.insert (#ground class, (x, nvars), (hyps, e)), - inclusions = #inclusions class} - | Inclusion f' => - {ground = #ground class, - inclusions = inclusion (classes, f, #inclusions class, f', e)} + {ground = #ground class, + rules = (nvs, cs, c, e) :: #rules class} in CM.insert (classes, f, class) end @@ -985,31 +913,6 @@ fun sgnS_con' (arg as (m1, ms', (sgns, strs, cons))) c = (sgnS_con' arg (#1 c2), #2 c2)) | _ => c -fun sgnS_class_name (arg as (m1, ms', (sgns, strs, cons))) nm = - case nm of - ClProj (m1, ms, x) => - (case IM.find (strs, m1) of - NONE => nm - | SOME m1x => ClProj (m1, ms' @ m1x :: ms, x)) - | ClNamed n => - (case IM.find (cons, n) of - NONE => nm - | SOME nx => ClProj (m1, ms', nx)) - -fun sgnS_class_key (arg as (m1, ms', (sgns, strs, cons))) k = - case k of - CkProj (m1, ms, x) => - (case IM.find (strs, m1) of - NONE => k - | SOME m1x => CkProj (m1, ms' @ m1x :: ms, x)) - | CkNamed n => - (case IM.find (cons, n) of - NONE => k - | SOME nx => CkProj (m1, ms', nx)) - | CkApp (k1, k2) => CkApp (sgnS_class_key arg k1, - sgnS_class_key arg k2) - | _ => k - fun sgnS_sgn (str, (sgns, strs, cons)) sgn = case sgn of SgnProj (m1, ms, x) => @@ -1120,22 +1023,10 @@ fun enrichClasses env classes (m1, ms) sgn = | SgiVal (x, n, c) => (case rule_in c of NONE => default () - | SOME (cn, rule) => + | SOME (cn, nvs, cs, c) => let - val globalizeN = sgnS_class_name (m1, ms, fmap) - val globalize = sgnS_class_key (m1, ms, fmap) - - fun unravel c = - case c of - ClNamed n => - ((case lookupCNamed env n of - (_, _, SOME c') => - (case class_name_in c' of - NONE => c - | SOME k => unravel k) - | _ => c) - handle UnboundNamed _ => c) - | _ => c + val loc = #2 c + fun globalize (c, loc) = (sgnS_con' (m1, ms, fmap) c, loc) val nc = case cn of @@ -1150,23 +1041,14 @@ fun enrichClasses env classes (m1, ms) sgn = NONE => classes | SOME class => let - val e = (EModProj (m1, ms, x), - #2 sgn) + val e = (EModProj (m1, ms, x), #2 sgn) val class = - case rule of - Normal (nvars, hyps, a) => - {ground = - KM.insert (#ground class, (globalize a, nvars), - (map (fn (n, k) => - (globalizeN n, - globalize k)) hyps, e)), - inclusions = #inclusions class} - | Inclusion f' => - {ground = #ground class, - inclusions = inclusion (classes, cn, - #inclusions class, - globalizeN f', e)} + {ground = #ground class, + rules = (nvs, + map globalize cs, + globalize c, + e) :: #rules class} in CM.insert (classes, cn, class) end @@ -1188,19 +1070,11 @@ fun enrichClasses env classes (m1, ms) sgn = val e = (EModProj (m1, ms, x), #2 sgn) val class = - case rule of - Normal (nvars, hyps, a) => - {ground = - KM.insert (#ground class, (globalize a, nvars), - (map (fn (n, k) => - (globalizeN n, - globalize k)) hyps, e)), - inclusions = #inclusions class} - | Inclusion f' => - {ground = #ground class, - inclusions = inclusion (classes, cn, - #inclusions class, - globalizeN f', e)} + {ground = #ground class, + rules = (nvs, + map globalize cs, + globalize c, + e) :: #rules class} in CM.insert (classes, cn, class) end @@ -1301,8 +1175,8 @@ fun sgiBinds env (sgi, loc) = | SgiSgn (x, n, sgn) => pushSgnNamedAs env x n sgn | SgiConstraint _ => env - | SgiClassAbs (x, n, k) => pushCNamedAs env x n (KArrow (k, (KType, loc)), loc) NONE - | SgiClass (x, n, k, c) => pushCNamedAs env x n (KArrow (k, (KType, loc)), loc) (SOME c) + | SgiClassAbs (x, n, k) => pushCNamedAs env x n k NONE + | SgiClass (x, n, k, c) => pushCNamedAs env x n k (SOME c) fun sgnSubCon x = ElabUtil.Con.map {kind = id, diff --git a/src/elab_err.sml b/src/elab_err.sml index 4f24e225..172f7d37 100644 --- a/src/elab_err.sml +++ b/src/elab_err.sml @@ -217,7 +217,17 @@ fun expError env err = ("Type", p_con env c)]) co) | Unresolvable (loc, c) => (ErrorMsg.errorAt loc "Can't resolve type class instance"; - eprefaces' [("Class constraint", p_con env c)]) + eprefaces' [("Class constraint", p_con env c), + ("Class database", p_list (fn (c, rules) => + box [P.p_con env c, + PD.string ":", + space, + p_list (fn (c, e) => + box [p_exp env e, + PD.string ":", + space, + P.p_con env c]) rules]) + (E.listClasses env))]) | IllegalRec (x, e) => (ErrorMsg.errorAt (#2 e) "Illegal 'val rec' righthand side (must be a function abstraction)"; eprefaces' [("Variable", PD.string x), diff --git a/src/elab_util.sig b/src/elab_util.sig index 817f885f..5b4bc46a 100644 --- a/src/elab_util.sig +++ b/src/elab_util.sig @@ -62,6 +62,10 @@ structure Con : sig val map : {kind : Elab.kind' -> Elab.kind', con : Elab.con' -> Elab.con'} -> Elab.con -> Elab.con + val existsB : {kind : 'context * Elab.kind' -> bool, + con : 'context * Elab.con' -> bool, + bind : 'context * binder -> 'context} + -> 'context -> Elab.con -> bool val exists : {kind : Elab.kind' -> bool, con : Elab.con' -> bool} -> Elab.con -> bool diff --git a/src/elab_util.sml b/src/elab_util.sml index ff4abbfb..17e67787 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -244,7 +244,22 @@ fun map {kind, con} s = S.Return () => raise Fail "ElabUtil.Con.map: Impossible" | S.Continue (s, ()) => s -fun exists {kind, con} k = +fun existsB {kind, con, bind} ctx c = + case mapfoldB {kind = fn ctx => fn k => fn () => + if kind (ctx, k) then + S.Return () + else + S.Continue (k, ()), + con = fn ctx => fn c => fn () => + if con (ctx, c) then + S.Return () + else + S.Continue (c, ()), + bind = bind} ctx c () of + S.Return _ => true + | S.Continue _ => false + +fun exists {kind, con} c = case mapfold {kind = fn k => fn () => if kind k then S.Return () @@ -254,7 +269,7 @@ fun exists {kind, con} k = if con c then S.Return () else - S.Continue (c, ())} k () of + S.Continue (c, ())} c () of S.Return _ => true | S.Continue _ => false diff --git a/src/elaborate.sml b/src/elaborate.sml index 874f6c82..1323086c 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -2021,8 +2021,8 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = let val (c', ck, gs') = elabCon (env, denv) c - val (env', n) = E.pushENamed env x c' val c' = normClassConstraint env c' + val (env', n) = E.pushENamed env x c' in (unifyKinds env ck ktype handle KUnify ue => strError env (NotType (loc, ck, ue))); @@ -2115,8 +2115,7 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = | L.SgiClassAbs (x, k) => let val k = elabKind env k - val k' = (L'.KArrow (k, (L'.KType, loc)), loc) - val (env, n) = E.pushCNamed env x k' NONE + val (env, n) = E.pushCNamed env x k NONE val env = E.pushClass env n in ([(L'.SgiClassAbs (x, n, k), loc)], (env, denv, [])) @@ -2125,12 +2124,11 @@ fun elabSgn_item ((sgi, loc), (env, denv, gs)) = | L.SgiClass (x, k, c) => let val k = elabKind env k - val k' = (L'.KArrow (k, (L'.KType, loc)), loc) val (c', ck, gs) = elabCon (env, denv) c - val (env, n) = E.pushCNamed env x k' (SOME c') + val (env, n) = E.pushCNamed env x k (SOME c') val env = E.pushClass env n in - checkKind env c' ck k'; + checkKind env c' ck k; ([(L'.SgiClass (x, n, k, c'), loc)], (env, denv, [])) end @@ -2341,17 +2339,15 @@ and dopen env {str, strs, sgn} = (L'.DConstraint (c1, c2), loc) | L'.SgiClassAbs (x, n, k) => let - val k' = (L'.KArrow (k, (L'.KType, loc)), loc) val c = (L'.CModProj (str, strs, x), loc) in - (L'.DCon (x, n, k', c), loc) + (L'.DCon (x, n, k, c), loc) end | L'.SgiClass (x, n, k, _) => let - val k' = (L'.KArrow (k, (L'.KType, loc)), loc) val c = (L'.CModProj (str, strs, x), loc) in - (L'.DCon (x, n, k', c), loc) + (L'.DCon (x, n, k, c), loc) end in (d, E.declBinds env' d) @@ -2466,14 +2462,8 @@ and subSgn env sgn1 (sgn2 as (_, loc2)) = in found (x', n1, k', SOME (L'.CModProj (m1, ms, s), loc)) end - | L'.SgiClassAbs (x', n1, k) => found (x', n1, - (L'.KArrow (k, - (L'.KType, loc)), loc), - NONE) - | L'.SgiClass (x', n1, k, c) => found (x', n1, - (L'.KArrow (k, - (L'.KType, loc)), loc), - SOME c) + | L'.SgiClassAbs (x', n1, k) => found (x', n1, k, NONE) + | L'.SgiClass (x', n1, k, c) => found (x', n1, k, SOME c) | _ => NONE end) @@ -2505,8 +2495,7 @@ and subSgn env sgn1 (sgn2 as (_, loc2)) = in case sgi1 of L'.SgiCon (x', n1, k1, c1) => found (x', n1, k1, c1) - | L'.SgiClass (x', n1, k1, c1) => - found (x', n1, (L'.KArrow (k1, (L'.KType, loc)), loc), c1) + | L'.SgiClass (x', n1, k1, c1) => found (x', n1, k1, c1) | _ => NONE end) @@ -2677,13 +2666,12 @@ and subSgn env sgn1 (sgn2 as (_, loc2)) = handle KUnify (k1, k2, err) => sgnError env (SgiWrongKind (sgi1All, k1, sgi2All, k2, err)) - val k = (L'.KArrow (k1, (L'.KType, loc)), loc) - val env = E.pushCNamedAs env x n1 k co + val env = E.pushCNamedAs env x n1 k1 co in SOME (if n1 = n2 then env else - E.pushCNamedAs env x n2 k (SOME (L'.CNamed n1, loc2))) + E.pushCNamedAs env x n2 k1 (SOME (L'.CNamed n1, loc2))) end else NONE @@ -2696,8 +2684,6 @@ and subSgn env sgn1 (sgn2 as (_, loc2)) = | L'.SgiClass (x, n2, k2, c2) => seek (fn (env, sgi1All as (sgi1, _)) => let - val k = (L'.KArrow (k2, (L'.KType, loc)), loc) - fun found (x', n1, k1, c1) = if x = x' then let @@ -2707,11 +2693,11 @@ and subSgn env sgn1 (sgn2 as (_, loc2)) = fun good () = let - val env = E.pushCNamedAs env x n2 k (SOME c2) + val env = E.pushCNamedAs env x n2 k2 (SOME c2) val env = if n1 = n2 then env else - E.pushCNamedAs env x n1 k (SOME c1) + E.pushCNamedAs env x n1 k2 (SOME c1) in SOME env end @@ -3361,12 +3347,11 @@ and elabDecl (dAll as (d, loc), (env, denv, gs)) = | L.DClass (x, k, c) => let val k = elabKind env k - val k' = (L'.KArrow (k, (L'.KType, loc)), loc) val (c', ck, gs') = elabCon (env, denv) c - val (env, n) = E.pushCNamed env x k' (SOME c') + val (env, n) = E.pushCNamed env x k (SOME c') val env = E.pushClass env n in - checkKind env c' ck k'; + checkKind env c' ck k; ([(L'.DClass (x, n, k, c'), loc)], (env, denv, enD gs' @ gs)) end diff --git a/src/urweb.grm b/src/urweb.grm index fb31bd18..16a77150 100644 --- a/src/urweb.grm +++ b/src/urweb.grm @@ -660,8 +660,9 @@ sgi : CON SYMBOL DCOLON kind ((SgiConAbs (SYMBOL, kind), s (CONleft, end) | CLASS SYMBOL (let val loc = s (CLASSleft, SYMBOLright) + val k = (KArrow ((KType, loc), (KType, loc)), loc) in - (SgiClassAbs (SYMBOL, (KWild, loc)), loc) + (SgiClassAbs (SYMBOL, k), loc) end) | CLASS SYMBOL DCOLON kind (let val loc = s (CLASSleft, kindright) -- cgit v1.2.3 From 008b594412606bbf78fff76daff219a102ce2daa Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 28 Apr 2009 11:05:28 -0400 Subject: LEFT JOIN --- lib/ur/basis.urs | 11 +++++++ src/elab_env.sig | 2 +- src/elab_env.sml | 87 +++++++++++++++++++++++++++++++++++++++++++++++++++---- src/elaborate.sml | 61 +++++++++++++++++++++----------------- src/monoize.sml | 37 +++++++++++++++++++++++ src/urweb.grm | 14 +++++++-- src/urweb.lex | 1 + tests/join.ur | 3 +- 8 files changed, 181 insertions(+), 35 deletions(-) (limited to 'src/elab_env.sig') diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs index a81ba30a..a67d007a 100644 --- a/lib/ur/basis.urs +++ b/lib/ur/basis.urs @@ -235,6 +235,17 @@ val sql_inner_join : tabs1 ::: {{Type}} -> tabs2 ::: {{Type}} -> sql_exp (tabs1 ++ tabs2) [] [] bool -> sql_from_items (tabs1 ++ tabs2) +class nullify :: Type -> Type -> Type +val nullify_option : t ::: Type -> nullify (option t) (option t) +val nullify_prim : t ::: Type -> sql_injectable_prim t -> nullify t (option t) + +val sql_left_join : tabs1 ::: {{Type}} -> tabs2 ::: {{(Type * Type)}} + -> [tabs1 ~ tabs2] + => $(map (fn r => $(map (fn p :: (Type * Type) => nullify p.1 p.2) r)) tabs2) + -> sql_from_items tabs1 -> sql_from_items (map (map (fn p :: (Type * Type) => p.1)) tabs2) + -> sql_exp (tabs1 ++ map (map (fn p :: (Type * Type) => p.1)) tabs2) [] [] bool + -> sql_from_items (tabs1 ++ map (map (fn p :: (Type * Type) => p.2)) tabs2) + val sql_query1 : tables ::: {{Type}} -> grouped ::: {{Type}} -> selectedFields ::: {{Type}} diff --git a/src/elab_env.sig b/src/elab_env.sig index 4b927a16..1621722f 100644 --- a/src/elab_env.sig +++ b/src/elab_env.sig @@ -71,7 +71,7 @@ signature ELAB_ENV = sig val pushClass : env -> int -> env val isClass : env -> Elab.con -> bool - val resolveClass : env -> Elab.con -> Elab.exp option + val resolveClass : (Elab.con -> Elab.con) -> env -> Elab.con -> Elab.exp option val listClasses : env -> (Elab.con * (Elab.con * Elab.exp) list) list val pushERel : env -> string -> Elab.con -> env diff --git a/src/elab_env.sml b/src/elab_env.sml index 62a310f2..7b20a700 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -507,6 +507,8 @@ fun unifyCons rs = (CUnif (_, _, _, ref (SOME c1)), _) => unify d (c1, c2) | (_, CUnif (_, _, _, ref (SOME c2))) => unify d (c1, c2) + | (CUnif _, _) => () + | (c1', CRel n2) => if n2 < d then case c1' of @@ -587,7 +589,56 @@ fun unifySubst (rs : con list) = | (d, _) => d} 0 -fun resolveClass (env : env) = +fun postUnify x = + let + fun unify (c1, c2) = + case (#1 c1, #1 c2) of + (CUnif (_, _, _, ref (SOME c1)), _) => unify (c1, c2) + | (_, CUnif (_, _, _, ref (SOME c2))) => unify (c1, c2) + + | (CUnif (_, _, _, r), _) => r := SOME c2 + + | (TFun (d1, r1), TFun (d2, r2)) => (unify (d1, d2); unify (r1, r2)) + | (TCFun (_, _, k1, r1), TCFun (_, _, k2, r2)) => (unifyKinds (k1, k2); unify (r1, r2)) + | (TRecord c1, TRecord c2) => unify (c1, c2) + | (TDisjoint (a1, b1, c1), TDisjoint (a2, b2, c2)) => + (unify (a1, a2); unify (b1, b2); unify (c1, c2)) + + | (CRel n1, CRel n2) => if n1 = n2 then () else raise Unify + | (CNamed n1, CNamed n2) => if n1 = n2 then () else raise Unify + | (CModProj (n1, ms1, x1), CModProj (n2, ms2, x2)) => + if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then () else raise Unify + | (CApp (f1, x1), CApp (f2, x2)) => (unify (f1, f2); unify (x1, x2)) + | (CAbs (_, k1, b1), CAbs (_, k2, b2)) => (unifyKinds (k1, k2); unify (b1, b2)) + + | (CKAbs (_, b1), CKAbs (_, b2)) => unify (b1, b2) + | (CKApp (c1, k1), CKApp (c2, k2)) => (unify (c1, c2); unifyKinds (k1, k2)) + | (TKFun (_, c1), TKFun (_, c2)) => unify (c1, c2) + + | (CName s1, CName s2) => if s1 = s2 then () else raise Unify + + | (CRecord (k1, xcs1), CRecord (k2, xcs2)) => + (unifyKinds (k1, k2); + ListPair.appEq (fn ((x1, c1), (x2, c2)) => (unify (x1, x2); unify (c1, c2))) (xcs1, xcs2) + handle ListPair.UnequalLengths => raise Unify) + | (CConcat (f1, x1), CConcat (f2, x2)) => (unify (f1, f2); unify (x1, x2)) + | (CMap (d1, r1), CMap (d2, r2)) => (unifyKinds (d1, d2); unifyKinds (r1, r2)) + + | (CUnit, CUnit) => () + + | (CTuple cs1, CTuple cs2) => (ListPair.appEq unify (cs1, cs2) + handle ListPair.UnequalLengths => raise Unify) + | (CProj (c1, n1), CProj (c2, n2)) => (unify (c1, c2); + if n1 = n2 then () else raise Unify) + + | _ => raise Unify + in + unify x + end + +fun postUnifies x = (postUnify x; true) handle Unify => false + +fun resolveClass (hnorm : con -> con) (env : env) = let fun resolve c = let @@ -608,7 +659,8 @@ fun resolveClass (env : env) = let val eos = map (resolve o unifySubst rs) cs in - if List.exists (not o Option.isSome) eos then + if List.exists (not o Option.isSome) eos + orelse not (postUnifies (c, unifySubst rs c')) then tryRules rules' else let @@ -634,9 +686,34 @@ fun resolveClass (env : env) = tryGrounds (#ground class) end in - case class_head_in c of - SOME f => doHead f - | _ => NONE + case #1 c of + TRecord c => + (case #1 (hnorm c) of + CRecord (_, xts) => + let + fun resolver (xts, acc) = + case xts of + [] => SOME (ERecord acc, #2 c) + | (x, t) :: xts => + let + val t = hnorm t + + val t = case t of + (CApp (f, x), loc) => (CApp (hnorm f, hnorm x), loc) + | _ => t + in + case resolve t of + NONE => NONE + | SOME e => resolver (xts, (x, e, t) :: acc) + end + in + resolver (xts, []) + end + | _ => NONE) + | _ => + case class_head_in c of + SOME f => doHead f + | _ => NONE end in resolve diff --git a/src/elaborate.sml b/src/elaborate.sml index ea4c28bd..709871da 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -1131,26 +1131,35 @@ | (L'.TFun (dom, ran), _) => let fun default () = (e, t, []) + + fun isInstance () = + if infer <> L.TypesOnly then + let + val r = ref NONE + val (e, t, gs) = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc)) + in + (e, t, TypeClass (env, dom, r, loc) :: gs) + end + else + default () + + fun hasInstance c = + case #1 (hnormCon env c) of + L'.CApp (cl, x) => + let + val cl = hnormCon env cl + in + isClassOrFolder env cl + end + | L'.TRecord c => U.Con.exists {kind = fn _ => false, + con = fn c => + E.isClass env (hnormCon env (c, loc))} c + | _ => false in - case #1 (hnormCon env dom) of - L'.CApp (cl, x) => - let - val cl = hnormCon env cl - in - if infer <> L.TypesOnly then - if isClassOrFolder env cl then - let - val r = ref NONE - val (e, t, gs) = unravel (ran, (L'.EApp (e, (L'.EUnif r, loc)), loc)) - in - (e, t, TypeClass (env, dom, r, loc) :: gs) - end - else - default () - else - default () - end - | _ => default () + if hasInstance dom then + isInstance () + else + default () end | (L'.TDisjoint (r1, r2, t'), loc) => if infer <> L.TypesOnly then @@ -3638,7 +3647,7 @@ fun elabFile basis topStr topSgn env file = let val c = normClassKey env c in - case E.resolveClass env c of + case E.resolveClass (hnormCon env) env c of SOME e => r := SOME e | NONE => expError env (Unresolvable (loc, c)) end) gs @@ -3685,11 +3694,6 @@ fun elabFile basis topStr topSgn env file = (!delayedUnifs); delayedUnifs := []; - if ErrorMsg.anyErrors () then - () - else - app (fn f => f ()) (!checks); - if ErrorMsg.anyErrors () then () else @@ -3708,7 +3712,7 @@ fun elabFile basis topStr topSgn env file = val c = normClassKey env c in - case E.resolveClass env c of + case E.resolveClass (hnormCon env) env c of SOME e => r := SOME e | NONE => case #1 (hnormCon env c) of @@ -3747,6 +3751,11 @@ fun elabFile basis topStr topSgn env file = | _ => default () end) gs; + if ErrorMsg.anyErrors () then + () + else + app (fn f => f ()) (!checks); + (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) :: ds @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan) diff --git a/src/monoize.sml b/src/monoize.sml index 98a32492..1a502e51 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -189,6 +189,8 @@ fun monoType env = (L'.TFun (mt env dtmap t, (L'.TFfi ("Basis", "string"), loc)), loc) | L.CApp ((L.CFfi ("Basis", "sql_injectable"), _), t) => (L'.TFun (mt env dtmap t, (L'.TFfi ("Basis", "string"), loc)), loc) + | L.CApp ((L.CApp ((L.CFfi ("Basis", "nullify"), _), _), _), _) => + (L'.TRecord [], loc) | L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_unary"), _), _), _), _) => (L'.TFfi ("Basis", "string"), loc) | L.CApp ((L.CApp ((L.CApp ((L.CFfi ("Basis", "sql_binary"), _), _), _), _), _), _) => @@ -581,6 +583,15 @@ fun monoExp (env, st, fm) (all as (e, loc)) = ((L'.ERecord [("Lt", lt, (L'.TFun (t, (L'.TFun (t, (L'.TFfi ("Basis", "bool"), loc)), loc)), loc)), ("Le", le, (L'.TFun (t, (L'.TFun (t, (L'.TFfi ("Basis", "bool"), loc)), loc)), loc))], loc), fm) + + fun outerRec xts = + (L'.TRecord (map (fn ((L.CName x, _), (L.CRecord (_, xts), _)) => + (x, (L'.TRecord (map (fn (x', _) => (x, (L'.TRecord [], loc))) xts), loc)) + | (x, all as (_, loc)) => + (E.errorAt loc "Unsupported record field constructor"; + Print.eprefaces' [("Name", CorePrint.p_con env x), + ("Constructor", CorePrint.p_con env all)]; + ("", dummyTyp))) xts), loc) in case e of L.EPrim p => ((L'.EPrim p, loc), fm) @@ -1702,6 +1713,13 @@ fun monoExp (env, st, fm) (all as (e, loc)) = fm) end + | L.ECApp ((L.EFfi ("Basis", "nullify_option"), _), _) => + ((L'.ERecord [], loc), fm) + | L.ECApp ((L.EFfi ("Basis", "nullify_prim"), _), _) => + ((L'.EAbs ("_", (L'.TRecord [], loc), (L'.TRecord [], loc), + (L'.ERecord [], loc)), loc), + fm) + | L.ECApp ((L.EFfi ("Basis", "sql_subset"), _), _) => ((L'.ERecord [], loc), fm) | L.ECApp ((L.EFfi ("Basis", "sql_subset_all"), _), _) => @@ -1744,6 +1762,25 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L'.EPrim (Prim.String ")"), loc)]), loc)), loc)), loc), fm) end + | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_left_join"), _), _), _), (L.CRecord (_, right), _)) => + let + val s = (L'.TFfi ("Basis", "string"), loc) + in + ((L'.EAbs ("_", outerRec right, + (L'.TFun (s, (L'.TFun (s, (L'.TFun (s, s), loc)), loc)), loc), + (L'.EAbs ("tab1", s, (L'.TFun (s, (L'.TFun (s, s), loc)), loc), + (L'.EAbs ("tab2", s, (L'.TFun (s, s), loc), + (L'.EAbs ("on", s, s, + strcat [(L'.EPrim (Prim.String "("), loc), + (L'.ERel 2, loc), + (L'.EPrim (Prim.String " LEFT JOIN "), loc), + (L'.ERel 1, loc), + (L'.EPrim (Prim.String " ON "), loc), + (L'.ERel 0, loc), + (L'.EPrim (Prim.String ")"), loc)]), + loc)), loc)), loc)), loc), + fm) + end | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_order_by_Nil"), _), _), _), _) => ((L'.EPrim (Prim.String ""), loc), fm) diff --git a/src/urweb.grm b/src/urweb.grm index 723ed8b1..c1f0b1ca 100644 --- a/src/urweb.grm +++ b/src/urweb.grm @@ -213,7 +213,7 @@ datatype attr = Class of exp | Normal of con * exp | CURRENT_TIMESTAMP | NE | LT | LE | GT | GE | CCONSTRAINT | UNIQUE | CHECK | PRIMARY | FOREIGN | KEY | ON | NO | ACTION | RESTRICT | CASCADE | REFERENCES - | JOIN | INNER | CROSS + | JOIN | INNER | CROSS | LEFT %nonterm file of decl list @@ -361,7 +361,7 @@ datatype attr = Class of exp | Normal of con * exp %nonassoc DCOLON TCOLON %left UNION INTERSECT EXCEPT %right COMMA -%right JOIN INNER CROSS +%right JOIN INNER CROSS LEFT %right OR %right CAND %nonassoc EQ NE LT LE GT GE IS @@ -1468,6 +1468,16 @@ fitem : table' ([#1 table'], #2 table') (#1 fitem1 @ #1 fitem2, (EApp (e, tru), loc)) end) + | fitem LEFT JOIN fitem ON sqlexp (let + val loc = s (fitem1left, sqlexpright) + + val e = (EVar (["Basis"], "sql_left_join", Infer), loc) + val e = (EApp (e, #2 fitem1), loc) + val e = (EApp (e, #2 fitem2), loc) + in + (#1 fitem1 @ #1 fitem2, + (EApp (e, sqlexp), loc)) + end) tname : CSYMBOL (CName CSYMBOL, s (CSYMBOLleft, CSYMBOLright)) | LBRACE cexp RBRACE (cexp) diff --git a/src/urweb.lex b/src/urweb.lex index c20e9206..517054b3 100644 --- a/src/urweb.lex +++ b/src/urweb.lex @@ -341,6 +341,7 @@ notags = [^<{\n]+; "JOIN" => (Tokens.JOIN (pos yypos, pos yypos + size yytext)); "INNER" => (Tokens.INNER (pos yypos, pos yypos + size yytext)); "CROSS" => (Tokens.CROSS (pos yypos, pos yypos + size yytext)); + "LEFT" => (Tokens.LEFT (pos yypos, pos yypos + size yytext)); "UNION" => (Tokens.UNION (pos yypos, pos yypos + size yytext)); "INTERSECT" => (Tokens.INTERSECT (pos yypos, pos yypos + size yytext)); diff --git a/tests/join.ur b/tests/join.ur index 30a0e744..74f49eec 100644 --- a/tests/join.ur +++ b/tests/join.ur @@ -1,8 +1,9 @@ -table t : { A : int } +table t : { A : int, B : string, C : option string } fun main () = r <- oneRow (SELECT * FROM t); r <- oneRow (SELECT * FROM t AS T1, t AS T2); r <- oneRow (SELECT * FROM t AS T1 CROSS JOIN t AS T2); r <- oneRow (SELECT * FROM t AS T1 JOIN t AS T2 ON T1.A = T2.A); + r <- oneRow (SELECT * FROM t AS T1 LEFT JOIN t AS T2 ON T1.A = T2.A); return -- cgit v1.2.3 From caf010bca085bea65037d194c3eb21ca8b83c23b Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Tue, 28 Apr 2009 14:02:23 -0400 Subject: Preparing to allow views in SELECT FROM clauses --- lib/ur/basis.urs | 13 +++- src/elab_env.sig | 5 +- src/elab_env.sml | 85 ++++++++++------------- src/elaborate.sml | 197 ++++++++++++++++++++++++++++++++++-------------------- src/monoize.sml | 11 ++- 5 files changed, 183 insertions(+), 128 deletions(-) (limited to 'src/elab_env.sig') diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs index c80dde7c..ec31e57f 100644 --- a/lib/ur/basis.urs +++ b/lib/ur/basis.urs @@ -124,6 +124,13 @@ val self : transaction client (** SQL *) con sql_table :: {Type} -> {{Unit}} -> Type +con sql_view :: {Type} -> Type + +class fieldsOf :: Type -> {Type} -> Type +val fieldsOf_table : fs ::: {Type} -> keys ::: {{Unit}} + -> fieldsOf (sql_table fs keys) fs +val fieldsOf_view : fs ::: {Type} + -> fieldsOf (sql_view fs) fs (*** Constraints *) @@ -222,9 +229,9 @@ val sql_subset_all : tables :: {{Type}} -> sql_subset tables tables con sql_from_items :: {{Type}} -> Type -val sql_from_table : cols ::: {Type} -> keys ::: {{Unit}} - -> name :: Name -> sql_table cols keys - -> sql_from_items [name = cols] +val sql_from_table : t ::: Type -> fs ::: {Type} + -> fieldsOf t fs -> name :: Name + -> t -> sql_from_items [name = fs] val sql_from_comma : tabs1 ::: {{Type}} -> tabs2 ::: {{Type}} -> [tabs1 ~ tabs2] => sql_from_items tabs1 -> sql_from_items tabs2 diff --git a/src/elab_env.sig b/src/elab_env.sig index 1621722f..a5b8751a 100644 --- a/src/elab_env.sig +++ b/src/elab_env.sig @@ -71,7 +71,8 @@ signature ELAB_ENV = sig val pushClass : env -> int -> env val isClass : env -> Elab.con -> bool - val resolveClass : (Elab.con -> Elab.con) -> env -> Elab.con -> Elab.exp option + val resolveClass : (Elab.con -> Elab.con) -> (Elab.con * Elab.con -> bool) + -> env -> Elab.con -> Elab.exp option val listClasses : env -> (Elab.con * (Elab.con * Elab.exp) list) list val pushERel : env -> string -> Elab.con -> env @@ -118,4 +119,6 @@ signature ELAB_ENV = sig val patBinds : env -> Elab.pat -> env + exception Bad of Elab.con * Elab.con + end diff --git a/src/elab_env.sml b/src/elab_env.sml index 7b20a700..0184d0b1 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -589,56 +589,9 @@ fun unifySubst (rs : con list) = | (d, _) => d} 0 -fun postUnify x = - let - fun unify (c1, c2) = - case (#1 c1, #1 c2) of - (CUnif (_, _, _, ref (SOME c1)), _) => unify (c1, c2) - | (_, CUnif (_, _, _, ref (SOME c2))) => unify (c1, c2) - - | (CUnif (_, _, _, r), _) => r := SOME c2 - - | (TFun (d1, r1), TFun (d2, r2)) => (unify (d1, d2); unify (r1, r2)) - | (TCFun (_, _, k1, r1), TCFun (_, _, k2, r2)) => (unifyKinds (k1, k2); unify (r1, r2)) - | (TRecord c1, TRecord c2) => unify (c1, c2) - | (TDisjoint (a1, b1, c1), TDisjoint (a2, b2, c2)) => - (unify (a1, a2); unify (b1, b2); unify (c1, c2)) - - | (CRel n1, CRel n2) => if n1 = n2 then () else raise Unify - | (CNamed n1, CNamed n2) => if n1 = n2 then () else raise Unify - | (CModProj (n1, ms1, x1), CModProj (n2, ms2, x2)) => - if n1 = n2 andalso ms1 = ms2 andalso x1 = x2 then () else raise Unify - | (CApp (f1, x1), CApp (f2, x2)) => (unify (f1, f2); unify (x1, x2)) - | (CAbs (_, k1, b1), CAbs (_, k2, b2)) => (unifyKinds (k1, k2); unify (b1, b2)) - - | (CKAbs (_, b1), CKAbs (_, b2)) => unify (b1, b2) - | (CKApp (c1, k1), CKApp (c2, k2)) => (unify (c1, c2); unifyKinds (k1, k2)) - | (TKFun (_, c1), TKFun (_, c2)) => unify (c1, c2) - - | (CName s1, CName s2) => if s1 = s2 then () else raise Unify - - | (CRecord (k1, xcs1), CRecord (k2, xcs2)) => - (unifyKinds (k1, k2); - ListPair.appEq (fn ((x1, c1), (x2, c2)) => (unify (x1, x2); unify (c1, c2))) (xcs1, xcs2) - handle ListPair.UnequalLengths => raise Unify) - | (CConcat (f1, x1), CConcat (f2, x2)) => (unify (f1, f2); unify (x1, x2)) - | (CMap (d1, r1), CMap (d2, r2)) => (unifyKinds (d1, d2); unifyKinds (r1, r2)) - - | (CUnit, CUnit) => () - - | (CTuple cs1, CTuple cs2) => (ListPair.appEq unify (cs1, cs2) - handle ListPair.UnequalLengths => raise Unify) - | (CProj (c1, n1), CProj (c2, n2)) => (unify (c1, c2); - if n1 = n2 then () else raise Unify) +exception Bad of con * con - | _ => raise Unify - in - unify x - end - -fun postUnifies x = (postUnify x; true) handle Unify => false - -fun resolveClass (hnorm : con -> con) (env : env) = +fun resolveClass (hnorm : con -> con) (consEq : con * con -> bool) (env : env) = let fun resolve c = let @@ -649,6 +602,37 @@ fun resolveClass (hnorm : con -> con) (env : env) = let val loc = #2 c + fun generalize (c as (_, loc)) = + case #1 c of + CApp (f, x) => + let + val (f, equate) = generalize f + + fun isRecord () = + let + val rk = ref NONE + val k = (KUnif (loc, "k", rk), loc) + val r = ref NONE + val rc = (CUnif (loc, k, "x", r), loc) + in + ((CApp (f, rc), loc), + fn () => (if consEq (rc, x) then + true + else + (raise Bad (rc, x); + false)) + andalso equate ()) + end + in + case #1 x of + CConcat _ => isRecord () + | CRecord _ => isRecord () + | _ => ((CApp (f, x), loc), equate) + end + | _ => (c, fn () => true) + + val (c, equate) = generalize c + fun tryRules rules = case rules of [] => NONE @@ -660,7 +644,8 @@ fun resolveClass (hnorm : con -> con) (env : env) = val eos = map (resolve o unifySubst rs) cs in if List.exists (not o Option.isSome) eos - orelse not (postUnifies (c, unifySubst rs c')) then + orelse not (equate ()) + orelse not (consEq (c, unifySubst rs c')) then tryRules rules' else let diff --git a/src/elaborate.sml b/src/elaborate.sml index 709871da..81fcbda1 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -647,6 +647,13 @@ case hnormKind (kindof env c) of (L'.KRecord k, _) => k | (L'.KError, _) => kerror + | (L'.KUnif (_, _, r), _) => + let + val k = kunif (#2 c) + in + r := SOME (L'.KRecord k, #2 c); + k + end | k => raise CUnify' (CKindof (k, c, "record")) val k1 = rkindof c1 @@ -786,20 +793,25 @@ (*val () = eprefaces "Summaries4" [("#1", p_summary env {fields = fs1, unifs = unifs1, others = others1}), ("#2", p_summary env {fields = fs2, unifs = unifs2, others = others2})]*) - fun isGuessable (other, fs) = - (guessMap env (other, (L'.CRecord (k, fs), loc), GuessFailure); - true) - handle GuessFailure => false + fun isGuessable (other, fs, unifs) = + let + val c = (L'.CRecord (k, fs), loc) + val c = foldl (fn ((c', _), c) => (L'.CConcat (c', c), loc)) c unifs + in + (guessMap env (other, c, GuessFailure); + true) + handle GuessFailure => false + end val (fs1, fs2, others1, others2) = - case (fs1, fs2, others1, others2) of - ([], _, [other1], []) => - if isGuessable (other1, fs2) then + case (fs1, fs2, others1, others2, unifs1, unifs2) of + ([], _, [other1], [], [], _) => + if isGuessable (other1, fs2, unifs2) then ([], [], [], []) else (fs1, fs2, others1, others2) - | (_, [], [], [other2]) => - if isGuessable (other2, fs1) then + | (_, [], [], [other2], _, []) => + if isGuessable (other2, fs1, unifs1) then ([], [], [], []) else (fs1, fs2, others1, others2) @@ -866,6 +878,13 @@ unfold (r2, c2'); unifyCons env r (L'.CConcat (r1, r2), loc) end + | L'.CUnif (_, _, _, ref (SOME c)) => unfold (r, c) + | L'.CUnif (_, _, _, ur as ref NONE) => + let + val ur' = cunif (loc, (L'.KRecord dom, loc)) + in + ur := SOME (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), loc), f), loc), ur'), loc) + end | _ => raise ex in unfold (r, c) @@ -1144,17 +1163,21 @@ default () fun hasInstance c = - case #1 (hnormCon env c) of - L'.CApp (cl, x) => + case hnormCon env c of + (L'.TRecord c, _) => U.Con.exists {kind = fn _ => false, + con = fn c => + E.isClass env (hnormCon env (c, loc))} c + | c => let - val cl = hnormCon env cl + fun findHead c = + case #1 c of + L'.CApp (f, _) => findHead f + | _ => c + + val cl = hnormCon env (findHead c) in isClassOrFolder env cl end - | L'.TRecord c => U.Con.exists {kind = fn _ => false, - con = fn c => - E.isClass env (hnormCon env (c, loc))} c - | _ => false in if hasInstance dom then isInstance () @@ -3647,7 +3670,7 @@ fun elabFile basis topStr topSgn env file = let val c = normClassKey env c in - case E.resolveClass (hnormCon env) env c of + case E.resolveClass (hnormCon env) (consEq env) env c of SOME e => r := SOME e | NONE => expError env (Unresolvable (loc, c)) end) gs @@ -3684,72 +3707,102 @@ fun elabFile basis topStr topSgn env file = end val (file, (_, gs)) = ListUtil.foldlMapConcat elabDecl' (env', []) file - in - mayDelay := false; - app (fn (env, k, s1, s2) => - unifySummaries env (k, normalizeRecordSummary env s1, normalizeRecordSummary env s2) - handle CUnify' err => (ErrorMsg.errorAt (#2 k) "Error in final record unification"; - cunifyError env err)) - (!delayedUnifs); + val delayed = !delayedUnifs + in delayedUnifs := []; + app (fn (env, k, s1, s2) => + unifySummaries env (k, normalizeRecordSummary env s1, normalizeRecordSummary env s2)) + delayed; if ErrorMsg.anyErrors () then () else - app (fn Disjoint (loc, env, denv, c1, c2) => - (case D.prove env denv (c1, c2, loc) of - [] => () - | _ => - (ErrorMsg.errorAt loc "Couldn't prove field name disjointness"; - eprefaces' [("Con 1", p_con env c1), - ("Con 2", p_con env c2), - ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)), - ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))])) - | TypeClass (env, c, r, loc) => + let + fun solver gs = let - fun default () = expError env (Unresolvable (loc, c)) + val (gs, solved) = + ListUtil.foldlMapPartial + (fn (g, solved) => + case g of + Disjoint (loc, env, denv, c1, c2) => + (case D.prove env denv (c1, c2, loc) of + [] => (NONE, true) + | _ => (SOME g, solved)) + | TypeClass (env, c, r, loc) => + let + fun default () = (SOME g, solved) - val c = normClassKey env c - in - case E.resolveClass (hnormCon env) env c of - SOME e => r := SOME e - | NONE => - case #1 (hnormCon env c) of - L'.CApp (f, x) => - (case (#1 (hnormCon env f), #1 (hnormCon env x)) of - (L'.CKApp (f, _), L'.CRecord (k, xcs)) => - (case #1 (hnormCon env f) of - L'.CModProj (top_n', [], "folder") => - if top_n' = top_n then - let - val e = (L'.EModProj (top_n, ["Folder"], "nil"), loc) - val e = (L'.EKApp (e, k), loc) - - val (folder, _) = foldr (fn ((x, c), (folder, xcs)) => - let - val e = (L'.EModProj (top_n, ["Folder"], - "cons"), loc) - val e = (L'.EKApp (e, k), loc) - val e = (L'.ECApp (e, - (L'.CRecord (k, xcs), - loc)), loc) - val e = (L'.ECApp (e, x), loc) - val e = (L'.ECApp (e, c), loc) - val e = (L'.EApp (e, folder), loc) - in - (e, (x, c) :: xcs) - end) - (e, []) xcs - in - r := SOME folder - end - else - default () + val c = normClassKey env c + in + case E.resolveClass (hnormCon env) (consEq env) env c of + SOME e => (r := SOME e; + (NONE, true)) + | NONE => + case #1 (hnormCon env c) of + L'.CApp (f, x) => + (case (#1 (hnormCon env f), #1 (hnormCon env x)) of + (L'.CKApp (f, _), L'.CRecord (k, xcs)) => + (case #1 (hnormCon env f) of + L'.CModProj (top_n', [], "folder") => + if top_n' = top_n then + let + val e = (L'.EModProj (top_n, ["Folder"], "nil"), loc) + val e = (L'.EKApp (e, k), loc) + + val (folder, _) = foldr (fn ((x, c), (folder, xcs)) => + let + val e = (L'.EModProj (top_n, ["Folder"], + "cons"), loc) + val e = (L'.EKApp (e, k), loc) + val e = (L'.ECApp (e, + (L'.CRecord (k, xcs), + loc)), loc) + val e = (L'.ECApp (e, x), loc) + val e = (L'.ECApp (e, c), loc) + val e = (L'.EApp (e, folder), loc) + in + (e, (x, c) :: xcs) + end) + (e, []) xcs + in + (r := SOME folder; + (NONE, true)) + end + else + default () | _ => default ()) | _ => default ()) | _ => default () - end) gs; + end) + false gs + in + case (gs, solved) of + ([], _) => () + | (_, true) => solver gs + | _ => + app (fn Disjoint (loc, env, denv, c1, c2) => + ((ErrorMsg.errorAt loc "Couldn't prove field name disjointness"; + eprefaces' [("Con 1", p_con env c1), + ("Con 2", p_con env c2), + ("Hnormed 1", p_con env (ElabOps.hnormCon env c1)), + ("Hnormed 2", p_con env (ElabOps.hnormCon env c2))])) + | TypeClass (env, c, r, loc) => + expError env (Unresolvable (loc, c))) + gs + end + in + solver gs + end; + + mayDelay := false; + + app (fn (env, k, s1, s2) => + unifySummaries env (k, normalizeRecordSummary env s1, normalizeRecordSummary env s2) + handle CUnify' err => (ErrorMsg.errorAt (#2 k) "Error in final record unification"; + cunifyError env err)) + (!delayedUnifs); + delayedUnifs := []; if ErrorMsg.anyErrors () then () diff --git a/src/monoize.sml b/src/monoize.sml index 16839cf9..ccc5a851 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -184,6 +184,8 @@ fun monoType env = (L'.TFfi ("Basis", "string"), loc) | L.CFfi ("Basis", "sql_offset") => (L'.TFfi ("Basis", "string"), loc) + | L.CApp ((L.CApp ((L.CFfi ("Basis", "fieldsOf"), _), _), _), _) => + (L'.TRecord [], loc) | L.CApp ((L.CFfi ("Basis", "sql_injectable_prim"), _), t) => (L'.TFun (mt env dtmap t, (L'.TFfi ("Basis", "string"), loc)), loc) @@ -1725,8 +1727,13 @@ fun monoExp (env, st, fm) (all as (e, loc)) = | L.ECApp ((L.EFfi ("Basis", "sql_subset_all"), _), _) => ((L'.ERecord [], loc), fm) - | L.ECApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_from_table"), _), _), _), _), _), - (L.CName name, _)) => + | L.ECApp ((L.ECApp ((L.EFfi ("Basis", "fieldsOf_table"), _), _), _), _) => + ((L'.ERecord [], loc), fm) + | L.ECApp ((L.EFfi ("Basis", "fieldsOf_view"), _), _) => + ((L'.ERecord [], loc), fm) + + | L.ECApp ((L.EApp ((L.ECApp ((L.ECApp ((L.EFfi ("Basis", "sql_from_table"), _), _), _), _), _), _), _), + (L.CName name, _)) => let val s = (L'.TFfi ("Basis", "string"), loc) in -- cgit v1.2.3 From b1d29df128dd1fa879e24f0eb3f5cdc1b74e16b7 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 3 Jun 2010 13:04:37 -0400 Subject: Some serious bug-fix work to get HTML example to compile; this includes fixing a bug with 'val' patterns in Unnest and the need for more local reduction in Especialize --- lib/ur/basis.urs | 2 +- lib/ur/string.ur | 10 ++- src/compiler.sig | 10 ++- src/compiler.sml | 6 +- src/core_print.sml | 11 +++- src/elab_env.sig | 1 + src/elab_env.sml | 9 +++ src/elab_print.sml | 11 +++- src/elab_util.sml | 32 ++++++++- src/especialize.sml | 7 +- src/expl_print.sml | 11 +++- src/monoize.sml | 7 +- src/reduce.sml | 32 +++++++++ src/reduce_local.sml | 179 +++++++++++++++++++++++++++++++++++++++++++-------- src/unnest.sml | 16 ++++- 15 files changed, 295 insertions(+), 49 deletions(-) (limited to 'src/elab_env.sig') diff --git a/lib/ur/basis.urs b/lib/ur/basis.urs index 19983cd2..f2dffd38 100644 --- a/lib/ur/basis.urs +++ b/lib/ur/basis.urs @@ -79,7 +79,7 @@ val strsub : string -> int -> char val strsuffix : string -> int -> string val strchr : string -> char -> option string val strindex : string -> char -> option int -val strcspn : string -> string -> option int +val strcspn : string -> string -> int val substring : string -> int -> int -> string val str1 : char -> string diff --git a/lib/ur/string.ur b/lib/ur/string.ur index f19ce174..f7781e01 100644 --- a/lib/ur/string.ur +++ b/lib/ur/string.ur @@ -11,7 +11,15 @@ val suffix = Basis.strsuffix val index = Basis.strindex val atFirst = Basis.strchr -fun mindex {Haystack = s, Needle = chs} = Basis.strcspn s chs +fun mindex {Haystack = s, Needle = chs} = + let + val n = Basis.strcspn s chs + in + if n >= length s then + None + else + Some n + end fun substring s {Start = start, Len = len} = Basis.substring s start len diff --git a/src/compiler.sig b/src/compiler.sig index 16207e8b..7e3e8ffc 100644 --- a/src/compiler.sig +++ b/src/compiler.sig @@ -129,10 +129,14 @@ signature COMPILER = sig val toTag : (string, Core.file) transform val toReduce : (string, Core.file) transform val toShakey : (string, Core.file) transform - val toUnpoly : (string, Core.file) transform - val toSpecialize : (string, Core.file) transform + val toUnpoly : (string, Core.file) transform + val toSpecialize : (string, Core.file) transform val toShake4 : (string, Core.file) transform - val toEspecialize2 : (string, Core.file) transform + val toEspecialize2 : (string, Core.file) transform + val toShake4' : (string, Core.file) transform + val toUnpoly2 : (string, Core.file) transform + val toShake4'' : (string, Core.file) transform + val toEspecialize3 : (string, Core.file) transform val toReduce2 : (string, Core.file) transform val toShake5 : (string, Core.file) transform val toMarshalcheck : (string, Core.file) transform diff --git a/src/compiler.sml b/src/compiler.sml index 1d15367f..dcc1e5b3 100644 --- a/src/compiler.sml +++ b/src/compiler.sml @@ -1013,8 +1013,12 @@ val toSpecialize = transform specialize "specialize" o toUnpoly val toShake4 = transform shake "shake4" o toSpecialize val toEspecialize2 = transform especialize "especialize2" o toShake4 +val toShake4' = transform shake "shake4'" o toEspecialize2 +val toUnpoly2 = transform unpoly "unpoly2" o toShake4' +val toShake4'' = transform shake "shake4'" o toUnpoly2 +val toEspecialize3 = transform especialize "especialize3" o toShake4'' -val toReduce2 = transform reduce "reduce2" o toEspecialize2 +val toReduce2 = transform reduce "reduce2" o toEspecialize3 val toShake5 = transform shake "shake5" o toReduce2 diff --git a/src/core_print.sml b/src/core_print.sml index fd0556e6..f18ea4b9 100644 --- a/src/core_print.sml +++ b/src/core_print.sml @@ -233,12 +233,19 @@ fun p_pat' par env (p, _) = p_pat' true env p]) | PRecord xps => box [string "{", - p_list_sep (box [string ",", space]) (fn (x, p, _) => + p_list_sep (box [string ",", space]) (fn (x, p, t) => box [string x, space, string "=", space, - p_pat env p]) xps, + p_pat env p, + if !debug then + box [space, + string ":", + space, + p_con env t] + else + box []]) xps, string "}"] and p_pat x = p_pat' false x diff --git a/src/elab_env.sig b/src/elab_env.sig index a5b8751a..769fea58 100644 --- a/src/elab_env.sig +++ b/src/elab_env.sig @@ -118,6 +118,7 @@ signature ELAB_ENV = sig val chaseMpath : env -> (int * string list) -> Elab.str * Elab.sgn val patBinds : env -> Elab.pat -> env + val patBindsN : Elab.pat -> int exception Bad of Elab.con * Elab.con diff --git a/src/elab_env.sml b/src/elab_env.sml index dd050c9e..bb34c345 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -1512,6 +1512,15 @@ fun patBinds env (p, loc) = | PCon (_, _, _, SOME p) => patBinds env p | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps +fun patBindsN (p, _) = + case p of + PWild => 0 + | PVar _ => 1 + | PPrim _ => 0 + | PCon (_, _, _, NONE) => 0 + | PCon (_, _, _, SOME p) => patBindsN p + | PRecord xps => foldl (fn ((_, p, _), n) => patBindsN p + n) 0 xps + fun edeclBinds env (d, loc) = case d of EDVal (p, _, _) => patBinds env p diff --git a/src/elab_print.sml b/src/elab_print.sml index 86448659..42a0a107 100644 --- a/src/elab_print.sml +++ b/src/elab_print.sml @@ -252,12 +252,19 @@ fun p_pat' par env (p, _) = p_pat' true env p]) | PRecord xps => box [string "{", - p_list_sep (box [string ",", space]) (fn (x, p, _) => + p_list_sep (box [string ",", space]) (fn (x, p, t) => box [string x, space, string "=", space, - p_pat env p]) xps, + p_pat env p, + if !debug then + box [space, + string ":", + space, + p_con env t] + else + box []]) xps, string "}"] and p_pat x = p_pat' false x diff --git a/src/elab_util.sml b/src/elab_util.sml index 8345e3f3..ec6c51ba 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -429,8 +429,10 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = | PRecord xps => foldl (fn ((_, p, _), ctx) => pb (p, ctx)) ctx xps in - S.map2 (mfe (pb (p, ctx)) e, - fn e' => (p, e')) + S.bind2 (mfp ctx p, + fn p' => + S.map2 (mfe (pb (p', ctx)) e, + fn e' => (p', e'))) end) pes, fn pes' => S.bind2 (mfc ctx disc, @@ -482,6 +484,32 @@ fun mapfoldB {kind = fk, con = fc, exp = fe, bind} = fn k' => (EKApp (e', k'), loc))) + and mfp ctx (pAll as (p, loc)) = + case p of + PWild => S.return2 pAll + | PVar (x, t) => + S.map2 (mfc ctx t, + fn t' => + (PVar (x, t'), loc)) + | PPrim _ => S.return2 pAll + | PCon (dk, pc, args, po) => + S.bind2 (ListUtil.mapfold (mfc ctx) args, + fn args' => + S.map2 ((case po of + NONE => S.return2 NONE + | SOME p => S.map2 (mfp ctx p, SOME)), + fn po' => + (PCon (dk, pc, args', po'), loc))) + | PRecord xps => + S.map2 (ListUtil.mapfold (fn (x, p, c) => + S.bind2 (mfp ctx p, + fn p' => + S.map2 (mfc ctx c, + fn c' => + (x, p', c')))) xps, + fn xps' => + (PRecord xps', loc)) + and mfed ctx (dAll as (d, loc)) = case d of EDVal (p, t, e) => diff --git a/src/especialize.sml b/src/especialize.sml index 7d129b8b..3fa3ea1d 100644 --- a/src/especialize.sml +++ b/src/especialize.sml @@ -1,4 +1,4 @@ -(* Copyright (c) 2008-2009, Adam Chlipala +(* Copyright (c) 2008-2010, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -278,7 +278,7 @@ fun specialize' (funcs, specialized) file = NONE => default () | SOME (f, xs) => case IM.find (#funcs st, f) of - NONE => default () + NONE => ((*print ("No find: " ^ Int.toString f ^ "\n");*) default ()) | SOME {name, args, body, typ, tag} => let val (xs, st) = ListUtil.foldlMap (fn (e, st) => exp (env, e, st)) st xs @@ -415,6 +415,8 @@ fun specialize' (funcs, specialized) file = (body', typ') fvs val mns = !mayNotSpec (*val () = mayNotSpec := SS.add (mns, name)*) + (*val () = print ("NEW: " ^ name ^ "__" ^ Int.toString f' ^ "\n");*) + val body' = ReduceLocal.reduceExp body' (*val () = Print.preface ("PRE", CorePrint.p_exp CoreEnv.empty body')*) val (body', st) = exp (env, body', st) val () = mayNotSpec := mns @@ -424,7 +426,6 @@ fun specialize' (funcs, specialized) file = e' fvs val e' = foldl (fn (arg, e) => (EApp (e, arg), loc)) e' xs - (*val () = print ("NEW: " ^ name ^ "__" ^ Int.toString f' ^ "\n");*) (*val () = Print.prefaces "Brand new" [("e'", CorePrint.p_exp CoreEnv.empty e'), ("e", CorePrint.p_exp CoreEnv.empty e), diff --git a/src/expl_print.sml b/src/expl_print.sml index 15838729..c953350c 100644 --- a/src/expl_print.sml +++ b/src/expl_print.sml @@ -234,12 +234,19 @@ fun p_pat' par env (p, _) = | PRecord xps => box [string "{", - p_list_sep (box [string ",", space]) (fn (x, p, _) => + p_list_sep (box [string ",", space]) (fn (x, p, t) => box [string x, space, string "=", space, - p_pat env p]) xps, + p_pat env p, + if !debug then + box [space, + string ":", + space, + p_con env t] + else + box []]) xps, string "}"] and p_pat x = p_pat' false x diff --git a/src/monoize.sml b/src/monoize.sml index e2377bae..d43002cb 100644 --- a/src/monoize.sml +++ b/src/monoize.sml @@ -2737,7 +2737,7 @@ fun monoExp (env, st, fm) (all as (e, loc)) = (L.ECApp ( (L.ECApp ( (L.EFfi ("Basis", "tag"), - _), _), _), _), _), _), _), _), _), _), _), _), _), _), _), _), _), + _), (L.CRecord (_, attrsGiven), _)), _), _), _), _), _), _), _), _), _), _), _), _), _), _), _), class), _), attrs), _), tag), _), @@ -2768,7 +2768,10 @@ fun monoExp (env, st, fm) (all as (e, loc)) = val (attrs, fm) = monoExp (env, st, fm) attrs val attrs = case #1 attrs of L'.ERecord xes => xes - | _ => raise Fail "Non-record attributes!" + | _ => map (fn ((L.CName x, _), t) => (x, (L'.EField (attrs, x), loc), monoType env t) + | (c, t) => (E.errorAt loc "Non-constant field name for HTML tag attribute"; + Print.eprefaces' [("Name", CorePrint.p_con env c)]; + ("", (L'.EField (attrs, ""), loc), monoType env t))) attrsGiven val attrs = if List.exists (fn ("Link", _, _) => true diff --git a/src/reduce.sml b/src/reduce.sml index b2911a5f..963863e8 100644 --- a/src/reduce.sml +++ b/src/reduce.sml @@ -65,6 +65,18 @@ val dangling = CoreUtil.Exp.RelE _ => n + 1 | _ => n} +val cdangling = + CoreUtil.Exp.existsB {kind = fn _ => false, + con = fn (n, c) => + case c of + CRel n' => n' >= n + | _ => false, + exp = fn _ => false, + bind = fn (n, b) => + case b of + CoreUtil.Exp.RelC _ => n + 1 + | _ => n} + datatype env_item = UnknownK | KnownK of kind @@ -86,6 +98,15 @@ val edepth' = foldl (fn (UnknownE, n) => n + 1 | (Lift (_, _, n'), n) => n + n' | (_, n) => n) 0 +val cdepth = foldl (fn (UnknownC, n) => n + 1 + | (KnownC _, n) => n + 1 + | (_, n) => n) 0 + +val cdepth' = foldl (fn (UnknownC, n) => n + 1 + | (KnownC _, n) => n + 1 + | (Lift (_, n', _), n) => n + n' + | (_, n) => n) 0 + type env = env_item list fun ei2s ei = @@ -344,6 +365,11 @@ fun kindConAndExp (namedC, namedE) = raise Fail "!") else ()*) + (*val () = if cdangling (cdepth env) all then + Print.prefaces "Bad exp" [("e", CorePrint.p_exp CoreEnv.empty all), + ("env", Print.PD.string (e2s env))] + else + ()*) val r = case e of EPrim _ => all @@ -636,6 +662,12 @@ fun kindConAndExp (namedC, namedE) = raise Fail "!!") else ();*) + (*if cdangling (cdepth' (deKnown env)) r then + (Print.prefaces "exp" [("e", CorePrint.p_exp CoreEnv.empty all), + ("r", CorePrint.p_exp CoreEnv.empty r)]; + raise Fail "!!") + else + ();*) r end in diff --git a/src/reduce_local.sml b/src/reduce_local.sml index 4c5ab52e..43317b9e 100644 --- a/src/reduce_local.sml +++ b/src/reduce_local.sml @@ -1,4 +1,4 @@ -(* Copyright (c) 2008, Adam Chlipala +(* Copyright (c) 2008-2010, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -43,11 +43,15 @@ datatype env_item = Unknown | Known of exp - | Lift of int + | UnknownC + | KnownC of con + + | Lift of int * int type env = env_item list val deKnown = List.filter (fn Known _ => false + | KnownC _ => false | _ => true) datatype result = Yes of env | No | Maybe @@ -120,39 +124,140 @@ fun match (env, p : pat, e : exp) = match (env, p, e) end +fun con env (all as (c, loc)) = + ((*Print.prefaces "con" [("c", CorePrint.p_con CoreEnv.empty all)];*) + case c of + TFun (c1, c2) => (TFun (con env c1, con env c2), loc) + | TCFun (x, k, c2) => (TCFun (x, k, con (UnknownC :: env) c2), loc) + | TKFun (x, c2) => (TKFun (x, con env c2), loc) + | TRecord c => (TRecord (con env c), loc) + + | CRel n => + let + fun find (n', env, nudge, liftC) = + case env of + [] => raise Fail "Reduce.con: CRel" + | Unknown :: rest => find (n', rest, nudge, liftC) + | Known _ :: rest => find (n', rest, nudge, liftC) + | Lift (liftC', _) :: rest => find (n', rest, nudge + liftC', + liftC + liftC') + | UnknownC :: rest => + if n' = 0 then + (CRel (n + nudge), loc) + else + find (n' - 1, rest, nudge, liftC + 1) + | KnownC c :: rest => + if n' = 0 then + con (Lift (liftC, 0) :: rest) c + else + find (n' - 1, rest, nudge - 1, liftC) + in + (*print (Int.toString n ^ ": " ^ e2s env ^ "\n");*) + find (n, env, 0, 0) + end + | CNamed _ => all + | CFfi _ => all + | CApp (c1, c2) => + let + val c1 = con env c1 + val c2 = con env c2 + in + case #1 c1 of + CAbs (_, _, b) => + con (KnownC c2 :: deKnown env) b + + | CApp ((CMap (dom, ran), _), f) => + (case #1 c2 of + CRecord (_, []) => (CRecord (ran, []), loc) + | CRecord (_, (x, c) :: rest) => + con (deKnown env) + (CConcat ((CRecord (ran, [(x, (CApp (f, c), loc))]), loc), + (CApp (c1, (CRecord (dom, rest), loc)), loc)), loc) + | _ => (CApp (c1, c2), loc)) + + | _ => (CApp (c1, c2), loc) + end + | CAbs (x, k, b) => (CAbs (x, k, con (UnknownC :: env) b), loc) + + | CKApp (c1, k) => + let + val c1 = con env c1 + in + case #1 c1 of + CKAbs (_, b) => + con (deKnown env) b + + | _ => (CKApp (c1, k), loc) + end + | CKAbs (x, b) => (CKAbs (x, con env b), loc) + + | CName _ => all + + | CRecord (k, xcs) => (CRecord (k, map (fn (x, c) => (con env x, con env c)) xcs), loc) + | CConcat (c1, c2) => + let + val c1 = con env c1 + val c2 = con env c2 + in + case (#1 c1, #1 c2) of + (CRecord (k, xcs1), CRecord (_, xcs2)) => + (CRecord (k, xcs1 @ xcs2), loc) + | (CRecord (_, []), _) => c2 + | (_, CRecord (_, [])) => c1 + | _ => (CConcat (c1, c2), loc) + end + | CMap _ => all + + | CUnit => all + + | CTuple cs => (CTuple (map (con env) cs), loc) + | CProj (c, n) => + let + val c = con env c + in + case #1 c of + CTuple cs => List.nth (cs, n - 1) + | _ => (CProj (c, n), loc) + end) + +fun patCon pc = + case pc of + PConVar _ => pc + | PConFfi {mod = m, datatyp, params, con = c, arg, kind} => + PConFfi {mod = m, datatyp = datatyp, params = params, con = c, + arg = Option.map (con (map (fn _ => UnknownC) params)) arg, + kind = kind} + fun exp env (all as (e, loc)) = case e of EPrim _ => all | ERel n => let - fun find (n', env, nudge, lift) = + fun find (n', env, nudge, liftC, liftE) = case env of [] => (ERel (n + nudge), loc) - | Lift lift' :: rest => find (n', rest, nudge + lift', lift + lift') + | Lift (liftC', liftE') :: rest => find (n', rest, nudge + liftE', liftC + liftC', liftE + liftE') + | UnknownC :: rest => find (n', rest, nudge, liftC + 1, liftE) + | KnownC _ :: rest => find (n', rest, nudge, liftC, liftE) | Unknown :: rest => if n' = 0 then (ERel (n + nudge), loc) else - find (n' - 1, rest, nudge, lift + 1) + find (n' - 1, rest, nudge, liftC, liftE + 1) | Known e :: rest => if n' = 0 then ((*print "SUBSTITUTING\n";*) - exp (Lift lift :: rest) e) + exp (Lift (liftC, liftE) :: rest) e) else - find (n' - 1, rest, nudge - 1, lift) + find (n' - 1, rest, nudge - 1, liftC, liftE) in - find (n, env, 0, 0) + find (n, env, 0, 0, 0) end | ENamed _ => all - | ECon (dk, pc, cs, eo) => (ECon (dk, pc, cs, Option.map (exp env) eo), loc) + | ECon (dk, pc, cs, eo) => (ECon (dk, patCon pc, map (con env) cs, Option.map (exp env) eo), loc) | EFfi _ => all | EFfiApp (m, f, es) => (EFfiApp (m, f, map (exp env) es), loc) - | EApp ((ECApp ((ECAbs (_, _, (EAbs (_, (CRel 0, _), _, - (ECon (dk, pc, [(CRel 0, loc)], SOME (ERel 0, _)), _)), _)), _), - t), _), e) => - (ECon (dk, pc, [t], SOME (exp env e)), loc) - | EApp (e1, e2) => let val e1 = exp env e1 @@ -163,21 +268,28 @@ fun exp env (all as (e, loc)) = | _ => (EApp (e1, e2), loc) end - | EAbs (x, dom, ran, e) => (EAbs (x, dom, ran, exp (Unknown :: env) e), loc) + | EAbs (x, dom, ran, e) => (EAbs (x, con env dom, con env ran, exp (Unknown :: env) e), loc) - | ECApp ((ECAbs (_, _, (ECon (dk, pc, [(CRel 0, loc)], NONE), _)), _), t) => - (ECon (dk, pc, [t], NONE), loc) + | ECApp (e, c) => + let + val e = exp env e + val c = con env c + in + case #1 e of + ECAbs (_, _, b) => exp (KnownC c :: deKnown env) b + | _ => (ECApp (e, c), loc) + end - | ECApp (e, c) => (ECApp (exp env e, c), loc) - | ECAbs (x, k, e) => (ECAbs (x, k, exp env e), loc) + | ECAbs (x, k, e) => (ECAbs (x, k, exp (UnknownC :: env) e), loc) | EKApp (e, k) => (EKApp (exp env e, k), loc) | EKAbs (x, e) => (EKAbs (x, exp env e), loc) - | ERecord xcs => (ERecord (map (fn (x, e, t) => (x, exp env e, t)) xcs), loc) + | ERecord xcs => (ERecord (map (fn (x, e, t) => (con env x, exp env e, con env t)) xcs), loc) | EField (e, c, others) => let val e = exp env e + val c = con env c fun default () = (EField (e, c, others), loc) in @@ -189,12 +301,16 @@ fun exp env (all as (e, loc)) = | _ => default () end - | EConcat (e1, c1, e2, c2) => (EConcat (exp env e1, c1, exp env e2, c2), loc) - | ECut (e, c, others) => (ECut (exp env e, c, others), loc) - | ECutMulti (e, c, others) => (ECutMulti (exp env e, c, others), loc) + | EConcat (e1, c1, e2, c2) => (EConcat (exp env e1, con env c1, exp env e2, con env c2), loc) + | ECut (e, c, {field = f, rest = r}) => (ECut (exp env e, + con env c, + {field = con env f, rest = con env r}), loc) + | ECutMulti (e, c, {rest = r}) => (ECutMulti (exp env e, con env c, {rest = con env r}), loc) - | ECase (e, pes, others) => + | ECase (e, pes, {disc = d, result = r}) => let + val others = {disc = con env d, result = con env r} + fun patBinds (p, _) = case p of PWild => 0 @@ -204,9 +320,18 @@ fun exp env (all as (e, loc)) = | PCon (_, _, _, SOME p) => patBinds p | PRecord xpts => foldl (fn ((_, p, _), n) => n + patBinds p) 0 xpts + fun pat (all as (p, loc)) = + case p of + PWild => all + | PVar (x, t) => (PVar (x, con env t), loc) + | PPrim _ => all + | PCon (dk, pc, cs, po) => + (PCon (dk, patCon pc, map (con env) cs, Option.map pat po), loc) + | PRecord xpts => (PRecord (map (fn (x, p, t) => (x, pat p, con env t)) xpts), loc) + fun push () = (ECase (exp env e, - map (fn (p, e) => (p, + map (fn (p, e) => (pat p, exp (List.tabulate (patBinds p, fn _ => Unknown) @ env) e)) pes, others), loc) @@ -226,9 +351,9 @@ fun exp env (all as (e, loc)) = | EWrite e => (EWrite (exp env e), loc) | EClosure (n, es) => (EClosure (n, map (exp env) es), loc) - | ELet (x, t, e1, e2) => (ELet (x, t, exp env e1, exp (Unknown :: env) e2), loc) + | ELet (x, t, e1, e2) => (ELet (x, con env t, exp env e1, exp (Unknown :: env) e2), loc) - | EServerCall (n, es, t) => (EServerCall (n, map (exp env) es, t), loc) + | EServerCall (n, es, t) => (EServerCall (n, map (exp env) es, con env t), loc) fun reduce file = let diff --git a/src/unnest.sml b/src/unnest.sml index 77589bfb..a2ec32b0 100644 --- a/src/unnest.sml +++ b/src/unnest.sml @@ -1,4 +1,4 @@ -(* Copyright (c) 2008, Adam Chlipala +(* Copyright (c) 2008-2010, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -204,12 +204,19 @@ fun exp ((ks, ts), e as old, st : state) = | PRecord xpcs => foldl (fn ((_, p, _), ts) => doVars (p, ts)) ts xpcs + + fun bindOne subs = ((0, (ERel 0, #2 ed)) + :: map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs) + + fun bindMany (n, subs) = + case n of + 0 => subs + | _ => bindMany (n - 1, bindOne subs) in ([(EDVal (p, t, e), #2 ed)], (doVars (p, ts), maxName, ds, - ((0, (ERel 0, #2 ed)) - :: map (fn (n, e) => (n + 1, E.liftExpInExp 0 e)) subs), + bindMany (E.patBindsN p, subs), by)) end | EDValRec vis => @@ -310,6 +317,7 @@ fun exp ((ks, ts), e as old, st : state) = let (*val () = print (Int.toString ex ^ "\n")*) val (name, t') = List.nth (ts, ex) + val t' = squishCon cfv t' in ((EAbs (name, t', @@ -354,6 +362,8 @@ fun exp ((ks, ts), e as old, st : state) = (*Print.prefaces "Before" [("e", ElabPrint.p_exp ElabEnv.empty e), ("se", ElabPrint.p_exp ElabEnv.empty (doSubst' (e, subs))), ("e'", ElabPrint.p_exp ElabEnv.empty e')];*) + (*Print.prefaces "Let" [("Before", ElabPrint.p_exp ElabEnv.empty (old, ErrorMsg.dummySpan)), + ("After", ElabPrint.p_exp ElabEnv.empty (ELet (eds, e', t), ErrorMsg.dummySpan))];*) (ELet (eds, e', t), {maxName = maxName, decls = ds}) -- cgit v1.2.3 From 948aa854af8ca5560a1eea5221c4a1f3a6901970 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 10 Oct 2010 14:41:03 -0400 Subject: Hopeful fix for the Great Unification Bug --- demo/crud.ur | 4 ++-- demo/crud3.ur | 2 +- demo/metaform.ur | 9 ++++---- demo/view.ur | 2 +- src/elab.sml | 2 +- src/elab_env.sig | 2 +- src/elab_env.sml | 40 +++++++++++++++++++++++++---------- src/elab_err.sig | 4 +++- src/elab_err.sml | 12 +++++++++-- src/elab_ops.sig | 2 ++ src/elab_ops.sml | 13 +++++++----- src/elab_print.sml | 11 ++++++---- src/elab_util.sig | 4 +++- src/elab_util.sml | 6 ++++-- src/elaborate.sml | 62 ++++++++++++++++++++++++++++++------------------------ src/explify.sml | 2 +- tests/concat.ur | 13 ++++++++++++ tests/concat.urp | 1 + 18 files changed, 125 insertions(+), 66 deletions(-) create mode 100644 tests/concat.ur create mode 100644 tests/concat.urp (limited to 'src/elab_env.sig') diff --git a/demo/crud.ur b/demo/crud.ur index 2fc82c1b..4d2753ea 100644 --- a/demo/crud.ur +++ b/demo/crud.ur @@ -78,7 +78,7 @@ functor Make(M : sig
{@foldR [colMeta] [fn cols => xml form [] (map snd cols)] - (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] (col : colMeta t) (acc : xml form [] (map snd rest)) => + (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] (col : colMeta t) acc =>
  • {cdata col.Nam}: {col.Widget [nm]}
    • {useMore acc}     ) @@ -128,7 +128,7 @@ functor Make(M : sig None => return Not found! | Some fs => return {@foldR2 [fst] [colMeta] [fn cols => xml form [] (map snd cols)] - (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] (v : t.1) (col : colMeta t) + (fn [nm :: Name] [t ::_] [rest ::_] [[nm] ~ rest] v (col : colMeta t) (acc : xml form [] (map snd rest)) =>
  • {cdata col.Nam}: {col.WidgetPopulated [nm] v}
    • diff --git a/demo/crud3.ur b/demo/crud3.ur index c336af30..5be035dd 100644 --- a/demo/crud3.ur +++ b/demo/crud3.ur @@ -20,7 +20,7 @@ open Crud.Make(struct     ), - Parse = (fn p => p.A ^ p.B), + Parse = (fn p : {A : string, B : string} => p.A ^ p.B), Inject = _ } } diff --git a/demo/metaform.ur b/demo/metaform.ur index 729b7d08..c6a6e54b 100644 --- a/demo/metaform.ur +++ b/demo/metaform.ur @@ -15,11 +15,10 @@ functor Make (M : sig fun main () = return {@foldUR [string] [fn cols => xml form [] (mapU string cols)] - (fn [nm :: Name] [rest ::_] [[nm] ~ rest] name - (acc : xml form [] (mapU string rest)) => -
  • {[name]}:
    • - {useMore acc} -     ) + (fn [nm :: Name] [rest ::_] [[nm] ~ rest] name acc => +
  • {[name]}:
    • + {useMore acc} +     ) M.fl M.names} diff --git a/demo/view.ur b/demo/view.ur index 84c179f4..0dcb42fa 100644 --- a/demo/view.ur +++ b/demo/view.ur @@ -1,7 +1,7 @@ table t : { A : int } view v = SELECT t.A AS A FROM t WHERE t.A > 7 -fun list [u] (_ : fieldsOf u [A = int]) (title : string) (x : u) = +fun list [u] (_ : fieldsOf u [A = int]) (title : string) (x : u) : transaction xbody = xml <- queryX (SELECT * FROM x) (fn r : {X : {A : int}} =>
  • {[r.X.A]}
    • ); return diff --git a/src/elab.sml b/src/elab.sml index dcb15502..97acec31 100644 --- a/src/elab.sml +++ b/src/elab.sml @@ -78,7 +78,7 @@ datatype con' = | CProj of con * int | CError - | CUnif of ErrorMsg.span * kind * string * con option ref + | CUnif of int * ErrorMsg.span * kind * string * con option ref withtype con = con' located diff --git a/src/elab_env.sig b/src/elab_env.sig index 769fea58..662d7071 100644 --- a/src/elab_env.sig +++ b/src/elab_env.sig @@ -27,8 +27,8 @@ signature ELAB_ENV = sig - exception SynUnif val liftConInCon : int -> Elab.con -> Elab.con + val mliftConInCon : int -> Elab.con -> Elab.con val liftConInExp : int -> Elab.exp -> Elab.exp val liftExpInExp : int -> Elab.exp -> Elab.exp diff --git a/src/elab_env.sml b/src/elab_env.sml index 16596622..bb731c08 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -43,8 +43,6 @@ exception UnboundNamed of int (* AST utility functions *) -exception SynUnif - val liftKindInKind = U.Kind.mapB {kind = fn bound => fn k => case k of @@ -78,13 +76,32 @@ val liftConInCon = c else CRel (xn + 1) - (*| CUnif _ => raise SynUnif*) + | CUnif (nl, loc, k, s, r) => CUnif (nl+1, loc, k, s, r) | _ => c, bind = fn (bound, U.Con.RelC _) => bound + 1 | (bound, _) => bound} val lift = liftConInCon 0 +fun mliftConInCon by c = + if by = 0 then + c + else + U.Con.mapB {kind = fn _ => fn k => k, + con = fn bound => fn c => + case c of + CRel xn => + if xn < bound then + c + else + CRel (xn + by) + | CUnif (nl, loc, k, s, r) => CUnif (nl+by, loc, k, s, r) + | _ => c, + bind = fn (bound, U.Con.RelC _) => bound + 1 + | (bound, _) => bound} 0 c + +val () = U.mliftConInCon := mliftConInCon + val liftKindInExp = U.Exp.mapB {kind = fn bound => fn k => case k of @@ -108,6 +125,7 @@ val liftConInExp = c else CRel (xn + 1) + | CUnif (nl, loc, k, s, r) => CUnif (nl+1, loc, k, s, r) | _ => c, exp = fn _ => fn e => e, bind = fn (bound, U.Exp.RelC _) => bound + 1 @@ -466,7 +484,7 @@ fun class_name_in (c, _) = case c of CNamed n => SOME (ClNamed n) | CModProj x => SOME (ClProj x) - | CUnif (_, _, _, ref (SOME c)) => class_name_in c + | CUnif (_, _, _, _, ref (SOME c)) => class_name_in c | _ => NONE fun isClass (env : env) c = @@ -480,7 +498,7 @@ fun isClass (env : env) c = fun class_head_in c = case #1 c of CApp (f, _) => class_head_in f - | CUnif (_, _, _, ref (SOME c)) => class_head_in c + | CUnif (_, _, _, _, ref (SOME c)) => class_head_in c | _ => class_name_in c exception Unify @@ -502,8 +520,8 @@ fun unifyKinds (k1, k2) = fun eqCons (c1, c2) = case (#1 c1, #1 c2) of - (CUnif (_, _, _, ref (SOME c1)), _) => eqCons (c1, c2) - | (_, CUnif (_, _, _, ref (SOME c2))) => eqCons (c1, c2) + (CUnif (nl, _, _, _, ref (SOME c1)), _) => eqCons (mliftConInCon nl c1, c2) + | (_, CUnif (nl, _, _, _, ref (SOME c2))) => eqCons (c1, mliftConInCon nl c2) | (CRel n1, CRel n2) => if n1 = n2 then () else raise Unify @@ -545,8 +563,8 @@ fun unifyCons rs = let fun unify d (c1, c2) = case (#1 c1, #1 c2) of - (CUnif (_, _, _, ref (SOME c1)), _) => unify d (c1, c2) - | (_, CUnif (_, _, _, ref (SOME c2))) => unify d (c1, c2) + (CUnif (nl, _, _, _, ref (SOME c1)), _) => unify d (mliftConInCon nl c1, c2) + | (_, CUnif (nl, _, _, _, ref (SOME c2))) => unify d (c1, mliftConInCon nl c2) | (CUnif _, _) => () @@ -633,7 +651,7 @@ fun unifySubst (rs : con list) = exception Bad of con * con val hasUnif = U.Con.exists {kind = fn _ => false, - con = fn CUnif (_, _, _, ref NONE) => true + con = fn CUnif (_, _, _, _, ref NONE) => true | _ => false} fun startsWithUnif c = @@ -670,7 +688,7 @@ fun resolveClass (hnorm : con -> con) (consEq : con * con -> bool) (env : env) = val rk = ref NONE val k = (KUnif (loc, "k", rk), loc) val r = ref NONE - val rc = (CUnif (loc, k, "x", r), loc) + val rc = (CUnif (0, loc, k, "x", r), loc) in ((CApp (f, rc), loc), fn () => (if consEq (rc, x) then diff --git a/src/elab_err.sig b/src/elab_err.sig index f6277488..fbe55a5b 100644 --- a/src/elab_err.sig +++ b/src/elab_err.sig @@ -1,4 +1,4 @@ -(* Copyright (c) 2008, Adam Chlipala +(* Copyright (c) 2008-2010, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -56,6 +56,8 @@ signature ELAB_ERR = sig | CExplicitness of Elab.con * Elab.con | CKindof of Elab.kind * Elab.con * string | CRecordFailure of Elab.con * Elab.con * (Elab.con * Elab.con * Elab.con) option + | TooLifty of ErrorMsg.span * ErrorMsg.span + | TooUnify of Elab.con * Elab.con val cunifyError : ElabEnv.env -> cunify_error -> unit diff --git a/src/elab_err.sml b/src/elab_err.sml index 80de9497..f8a16294 100644 --- a/src/elab_err.sml +++ b/src/elab_err.sml @@ -1,4 +1,4 @@ -(* Copyright (c) 2008, Adam Chlipala +(* Copyright (c) 2008-2010, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -112,7 +112,6 @@ fun conError env err = eprefaces' [("Constructor", p_con env c), ("Kind", p_kind env k)]) - datatype cunify_error = CKind of kind * kind * kunify_error | COccursCheckFailed of con * con @@ -120,6 +119,8 @@ datatype cunify_error = | CExplicitness of con * con | CKindof of kind * con * string | CRecordFailure of con * con * (con * con * con) option + | TooLifty of ErrorMsg.span * ErrorMsg.span + | TooUnify of con * con fun cunifyError env err = case err of @@ -154,6 +155,13 @@ fun cunifyError env err = [("Field", p_con env nm), ("Value 1", p_con env t1), ("Value 2", p_con env t2)])) + | TooLifty (loc1, loc2) => + (ErrorMsg.errorAt loc1 "Can't unify two unification variables that both have suspended liftings"; + eprefaces' [("Other location", Print.PD.string (ErrorMsg.spanToString loc2))]) + | TooUnify (c1, c2) => + (ErrorMsg.errorAt (#2 c1) "Substitution in constructor is blocked by a too-deep unification variable"; + eprefaces' [("Replacement", p_con env c1), + ("Body", p_con env c2)]) datatype exp_error = UnboundExp of ErrorMsg.span * string diff --git a/src/elab_ops.sig b/src/elab_ops.sig index adf69696..ed4c7d68 100644 --- a/src/elab_ops.sig +++ b/src/elab_ops.sig @@ -27,6 +27,8 @@ signature ELAB_OPS = sig + exception SubUnif + val liftKindInKind : int -> Elab.kind -> Elab.kind val subKindInKind : int * Elab.kind -> Elab.kind -> Elab.kind diff --git a/src/elab_ops.sml b/src/elab_ops.sml index 6465668f..15d8e106 100644 --- a/src/elab_ops.sml +++ b/src/elab_ops.sml @@ -97,11 +97,13 @@ fun liftConInCon by = c else CRel (xn + by) - (*| CUnif _ => raise SynUnif*) + | CUnif (nl, loc, k, s, r) => CUnif (nl+by, loc, k, s, r) | _ => c, bind = fn (bound, U.Con.RelC _) => bound + 1 | (bound, _) => bound} +exception SubUnif + fun subConInCon' rep = U.Con.mapB {kind = fn _ => fn k => k, con = fn (by, xn) => fn c => @@ -111,7 +113,8 @@ fun subConInCon' rep = EQUAL => #1 (liftConInCon by 0 rep) | GREATER => CRel (xn' - 1) | LESS => c) - (*| CUnif _ => raise SynUnif*) + | CUnif (0, _, _, _, _) => raise SubUnif + | CUnif (n, loc, k, s, r) => CUnif (n-1, loc, k, s, r) | _ => c, bind = fn ((by, xn), U.Con.RelC _) => (by+1, xn+1) | (ctx, _) => ctx} @@ -153,7 +156,7 @@ fun reset () = (identity := 0; fun hnormCon env (cAll as (c, loc)) = case c of - CUnif (_, _, _, ref (SOME c)) => hnormCon env c + CUnif (nl, _, _, _, ref (SOME c)) => hnormCon env (E.mliftConInCon nl c) | CNamed xn => (case E.lookupCNamed env xn of @@ -276,7 +279,7 @@ fun hnormCon env (cAll as (c, loc)) = let val r = ref NONE in - (r, (CUnif (loc, (KType, loc), "_", r), loc)) + (r, (CUnif (0, loc, (KType, loc), "_", r), loc)) end val (vR, v) = cunif () @@ -284,7 +287,7 @@ fun hnormCon env (cAll as (c, loc)) = val c = (CApp (f, v), loc) in case unconstraint c of - (CUnif (_, _, _, vR'), _) => + (CUnif (_, _, _, _, vR'), _) => if vR' = vR then (inc identity; hnormCon env c2) diff --git a/src/elab_print.sml b/src/elab_print.sml index 279c7231..2b8dc5f4 100644 --- a/src/elab_print.sml +++ b/src/elab_print.sml @@ -202,10 +202,13 @@ fun p_con' par env (c, _) = string (Int.toString n)] | CError => string "" - | CUnif (_, _, _, ref (SOME c)) => p_con' par env c - | CUnif (_, k, s, _) => box [string (""] + | CUnif (nl, _, _, _, ref (SOME c)) => p_con' par env (E.mliftConInCon nl c) + | CUnif (nl, _, k, s, _) => box [string (" box [] + | _ => string ("+" ^ Int.toString nl), + string ">"] | CKAbs (x, c) => box [string x, space, diff --git a/src/elab_util.sig b/src/elab_util.sig index 934779ff..dc0f25e8 100644 --- a/src/elab_util.sig +++ b/src/elab_util.sig @@ -1,4 +1,4 @@ -(* Copyright (c) 2008, Adam Chlipala +(* Copyright (c) 2008-2010, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -29,6 +29,8 @@ signature ELAB_UTIL = sig val classifyDatatype : (string * int * 'a option) list -> Elab.datatype_kind +val mliftConInCon : (int -> Elab.con -> Elab.con) ref + structure Kind : sig val mapfoldB : {kind : ('context, Elab.kind', 'state, 'abort) Search.mapfolderB, bind : 'context * string -> 'context} diff --git a/src/elab_util.sml b/src/elab_util.sml index 33ed599c..d297ccbc 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -1,4 +1,4 @@ -(* Copyright (c) 2008, Adam Chlipala +(* Copyright (c) 2008-2010, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -118,6 +118,8 @@ fun exists f k = end +val mliftConInCon = ref (fn n : int => fn c : con => (raise Fail "You didn't set ElabUtil.mliftConInCon!") : con) + structure Con = struct datatype binder = @@ -215,7 +217,7 @@ fun mapfoldB {kind = fk, con = fc, bind} = (CProj (c', n), loc)) | CError => S.return2 cAll - | CUnif (_, _, _, ref (SOME c)) => mfc' ctx c + | CUnif (nl, _, _, _, ref (SOME c)) => mfc' ctx (!mliftConInCon nl c) | CUnif _ => S.return2 cAll | CKAbs (x, c) => diff --git a/src/elaborate.sml b/src/elaborate.sml index 2cc01eda..37ca4b25 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -207,7 +207,7 @@ "U" ^ Int.toString (n - 26) in count := n + 1; - (L'.CUnif (loc, k, s, ref NONE), loc) + (L'.CUnif (0, loc, k, s, ref NONE), loc) end end @@ -495,7 +495,7 @@ | _ => false fun cunifsRemain c = case c of - L'.CUnif (loc, _, _, ref NONE) => SOME loc + L'.CUnif (_, loc, _, _, ref NONE) => SOME loc | _ => NONE val kunifsInDecl = U.Decl.exists {kind = kunifsRemain, @@ -516,13 +516,11 @@ fun occursCon r = U.Con.exists {kind = fn _ => false, - con = fn L'.CUnif (_, _, _, r') => r = r' + con = fn L'.CUnif (_, _, _, _, r') => r = r' | _ => false} exception CUnify' of cunify_error - exception SynUnif = E.SynUnif - type record_summary = { fields : (L'.con * L'.con) list, unifs : (L'.con * L'.con option ref) list, @@ -588,7 +586,7 @@ | k => raise CUnify' (CKindof (k, c, "tuple"))) | L'.CError => kerror - | L'.CUnif (_, k, _, _) => k + | L'.CUnif (_, _, k, _, _) => k | L'.CKAbs (x, c) => (L'.KFun (x, kindof (E.pushKRel env x) c), loc) | L'.CKApp (c, k) => @@ -644,7 +642,7 @@ | k => raise CUnify' (CKindof (k, c, "tuple")))*) | L'.CError => false - | L'.CUnif (_, k, _, _) => #1 k = L'.KUnit + | L'.CUnif (_, _, k, _, _) => #1 k = L'.KUnit | L'.CKAbs _ => false | L'.CKApp _ => false @@ -701,8 +699,8 @@ unifs = #unifs s1 @ #unifs s2, others = #others s1 @ #others s2} end - | (L'.CUnif (_, _, _, ref (SOME c)), _) => recordSummary env c - | c' as (L'.CUnif (_, _, _, r), _) => {fields = [], unifs = [(c', r)], others = []} + | (L'.CUnif (nl, _, _, _, ref (SOME c)), _) => recordSummary env (E.mliftConInCon nl c) + | c' as (L'.CUnif (0, _, _, _, r), _) => {fields = [], unifs = [(c', r)], others = []} | c' => {fields = [], unifs = [], others = [c']} in sum @@ -735,8 +733,8 @@ and unifySummaries env (loc, k, s1 : record_summary, s2 : record_summary) = let (*val () = eprefaces "Summaries" [("loc", PD.string (ErrorMsg.spanToString loc)), - ("#1", p_summary env s1), - ("#2", p_summary env s2)]*) + ("#1", p_summary env s1), + ("#2", p_summary env s2)]*) fun eatMatching p (ls1, ls2) = let @@ -922,7 +920,7 @@ unfold (r2, c2'); unifyCons env loc r (L'.CConcat (r1, r2), loc) end - | L'.CUnif (_, _, _, ur) => + | L'.CUnif (0, _, _, _, ur) => ur := SOME (L'.CApp ((L'.CApp ((L'.CMap (dom, ran), loc), f), loc), r), loc) | _ => raise ex in @@ -970,7 +968,7 @@ onFail () in case #1 (hnormCon env c2) of - L'.CUnif (_, k, _, r) => + L'.CUnif (0, _, k, _, r) => (case #1 (hnormKind k) of L'.KTuple ks => let @@ -986,7 +984,7 @@ | _ => onFail () in case #1 (hnormCon env c1) of - L'.CUnif (_, k, _, r) => + L'.CUnif (0, _, k, _, r) => (case #1 (hnormKind k) of L'.KTuple ks => let @@ -1002,7 +1000,7 @@ fun projSpecial2 (c2, n2, onFail) = case #1 (hnormCon env c2) of - L'.CUnif (_, k, _, r) => + L'.CUnif (0, _, k, _, r) => (case #1 (hnormKind k) of L'.KTuple ks => let @@ -1035,19 +1033,24 @@ | (L'.CConcat _, _) => isRecord () | (_, L'.CConcat _) => isRecord () - | (L'.CUnif (_, k1, _, r1), L'.CUnif (_, k2, _, r2)) => - if r1 = r2 then + | (L'.CUnif (nl1, loc1, k1, _, r1), L'.CUnif (nl2, loc2, k2, _, r2)) => + if r1 = r2 andalso nl1 = nl2 then () - else + else if nl1 = 0 then (unifyKinds env k1 k2; r1 := SOME c2All) + else if nl2 = 0 then + (unifyKinds env k1 k2; + r2 := SOME c2All) + else + err (fn _ => TooLifty (loc1, loc2)) - | (L'.CUnif (_, _, _, r), _) => + | (L'.CUnif (0, _, _, _, r), _) => if occursCon r c2All then err COccursCheckFailed else r := SOME c2All - | (_, L'.CUnif (_, _, _, r)) => + | (_, L'.CUnif (0, _, _, _, r)) => if occursCon r c1All then err COccursCheckFailed else @@ -1167,6 +1170,11 @@ | _ => false) | _ => false + fun subConInCon env x y = + ElabOps.subConInCon x y + handle SubUnif => (cunifyError env (TooUnify (#2 x, y)); + cerror) + fun elabHead (env, denv) infer (e as (_, loc)) t = let fun unravelKind (t, e) = @@ -1195,7 +1203,7 @@ let val u = cunif (loc, k) - val t'' = subConInCon (0, u) t' + val t'' = subConInCon env (0, u) t' in unravel (t'', (L'.ECApp (e, u), loc)) end @@ -1282,7 +1290,7 @@ fun elabPat (pAll as (p, loc), (env, bound)) = val k = (L'.KType, loc) val unifs = map (fn _ => cunif (loc, k)) xs val nxs = length unifs - 1 - val t = ListUtil.foldli (fn (i, u, t) => subConInCon (nxs - i, u) t) t unifs + val t = ListUtil.foldli (fn (i, u, t) => subConInCon env (nxs - i, u) t) t unifs val dn = foldl (fn (u, dn) => (L'.CApp (dn, u), loc)) dn unifs in ignore (checkPatCon env p' pt t); @@ -1469,7 +1477,7 @@ fun exhaustive (env, t, ps, loc) = val (t1, args) = unapp (hnormCon env q1, []) val t1 = hnormCon env t1 - fun doSub t = foldl (fn (arg, t) => subConInCon (0, arg) t) t args + fun doSub t = foldl (fn (arg, t) => subConInCon env (0, arg) t) t args fun dtype (dtO, names) = let @@ -1653,7 +1661,7 @@ fun normClassConstraint env (c, loc) = (L'.TFun (c1, c2), loc) end | L'.TCFun (expl, x, k, c1) => (L'.TCFun (expl, x, k, normClassConstraint env c1), loc) - | L'.CUnif (_, _, _, ref (SOME c)) => normClassConstraint env c + | L'.CUnif (nl, _, _, _, ref (SOME c)) => normClassConstraint env (E.mliftConInCon nl c) | _ => unmodCon env (c, loc) fun findHead e e' = @@ -1863,9 +1871,7 @@ fun elabExp (env, denv) (eAll as (e, loc)) = | L'.TCFun (_, x, k, eb) => let val () = checkKind env c' ck k - val eb' = subConInCon (0, c') eb - handle SynUnif => (expError env (Unif ("substitution", loc, eb)); - cerror) + val eb' = subConInCon env (0, c') eb val ef = (L'.ECApp (e', c'), loc) val (ef, eb', gs3) = @@ -3303,7 +3309,7 @@ and wildifyStr env (str, sgn) = (SOME c1, SOME c2) => SOME (L.CConcat (c1, c2), loc) | _ => NONE) | L'.CUnit => SOME (L.CUnit, loc) - | L'.CUnif (_, _, _, ref (SOME c)) => decompileCon env c + | L'.CUnif (nl, _, _, _, ref (SOME c)) => decompileCon env (E.mliftConInCon nl c) | _ => NONE diff --git a/src/explify.sml b/src/explify.sml index cf6c491c..5081d33b 100644 --- a/src/explify.sml +++ b/src/explify.sml @@ -76,7 +76,7 @@ fun explifyCon (c, loc) = | L.CProj (c, n) => (L'.CProj (explifyCon c, n), loc) | L.CError => raise Fail ("explifyCon: CError at " ^ EM.spanToString loc) - | L.CUnif (_, _, _, ref (SOME c)) => explifyCon c + | L.CUnif (nl, _, _, _, ref (SOME c)) => explifyCon (ElabEnv.mliftConInCon nl c) | L.CUnif _ => raise Fail ("explifyCon: CUnif at " ^ EM.spanToString loc) | L.CKAbs (x, c) => (L'.CKAbs (x, explifyCon c), loc) diff --git a/tests/concat.ur b/tests/concat.ur new file mode 100644 index 00000000..1330a21d --- /dev/null +++ b/tests/concat.ur @@ -0,0 +1,13 @@ +functor Make(M : sig + con ts :: {(Type * Type)} + val tab : sql_table (map fst ts) [] + val cols : $(map (fn p => p.2 -> string) ts) + end) = struct +end + +table t : {A : string} + +open Make(struct + val tab = t + val cols = {A = fn p : {B : string, C : string} => p.B ^ p.C} + end) diff --git a/tests/concat.urp b/tests/concat.urp new file mode 100644 index 00000000..442b05b4 --- /dev/null +++ b/tests/concat.urp @@ -0,0 +1 @@ +concat -- cgit v1.2.3 From 802fc606ff18c261eb591d7ae6dbb99fe9c48af9 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Fri, 4 May 2012 10:33:04 -0400 Subject: More diagnostic information about some type class resolution failures --- src/elab_env.sig | 1 + src/elab_env.sml | 26 ++++++++++++++++---------- src/elab_err.sml | 15 ++++----------- src/elaborate.sml | 8 +++++++- tests/classFail.ur | 3 +++ 5 files changed, 31 insertions(+), 22 deletions(-) create mode 100644 tests/classFail.ur (limited to 'src/elab_env.sig') diff --git a/src/elab_env.sig b/src/elab_env.sig index 662d7071..e0c589c4 100644 --- a/src/elab_env.sig +++ b/src/elab_env.sig @@ -73,6 +73,7 @@ signature ELAB_ENV = sig val isClass : env -> Elab.con -> bool val resolveClass : (Elab.con -> Elab.con) -> (Elab.con * Elab.con -> bool) -> env -> Elab.con -> Elab.exp option + val resolveFailureCause : unit -> Elab.con option val listClasses : env -> (Elab.con * (Elab.con * Elab.exp) list) list val pushERel : env -> string -> Elab.con -> env diff --git a/src/elab_env.sml b/src/elab_env.sml index ed96782e..bf0808f5 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -678,13 +678,18 @@ fun startsWithUnif c = | SOME x => hasUnif x end +val cause = ref (NONE : con option) +fun resolveFailureCause () = !cause + fun resolveClass (hnorm : con -> con) (consEq : con * con -> bool) (env : env) = let - fun resolve c = + fun resolve firstLevel c = let + fun notFound () = (if firstLevel then () else cause := SOME c; NONE) + fun doHead f = case CM.find (#classes env, f) of - NONE => NONE + NONE => notFound () | SOME class => let val loc = #2 c @@ -722,13 +727,13 @@ fun resolveClass (hnorm : con -> con) (consEq : con * con -> bool) (env : env) = fun tryRules rules = case rules of - [] => NONE + [] => notFound () | (nRs, cs, c', e) :: rules' => case tryUnify hnorm nRs (c, c') of NONE => tryRules rules' | SOME rs => let - val eos = map (resolve o unifySubst rs) cs + val eos = map (resolve false o unifySubst rs) cs in if List.exists (not o Option.isSome) eos orelse not (equate ()) @@ -759,7 +764,7 @@ fun resolveClass (hnorm : con -> con) (consEq : con * con -> bool) (env : env) = end in if startsWithUnif c then - NONE + notFound () else case #1 c of TRecord c => @@ -777,21 +782,22 @@ fun resolveClass (hnorm : con -> con) (consEq : con * con -> bool) (env : env) = (CApp (f, x), loc) => (CApp (hnorm f, hnorm x), loc) | _ => t in - case resolve t of - NONE => NONE + case resolve false t of + NONE => notFound () | SOME e => resolver (xts, (x, e, t) :: acc) end in resolver (xts, []) end - | _ => NONE) + | _ => notFound ()) | _ => case class_head_in c of SOME f => doHead f - | _ => NONE + | _ => notFound () end in - resolve + cause := NONE; + resolve true end fun pushERel (env : env) x t = diff --git a/src/elab_err.sml b/src/elab_err.sml index f21ddce0..0e04cf51 100644 --- a/src/elab_err.sml +++ b/src/elab_err.sml @@ -239,17 +239,10 @@ fun expError env err = ("Type", p_con env c)]) co) | Unresolvable (loc, c) => (ErrorMsg.errorAt loc "Can't resolve type class instance"; - eprefaces' [("Class constraint", p_con env c)(*, - ("Class database", p_list (fn (c, rules) => - box [P.p_con env c, - PD.string ":", - space, - p_list (fn (c, e) => - box [p_exp env e, - PD.string ":", - space, - P.p_con env c]) rules]) - (E.listClasses env))*)]) + eprefaces' ([("Class constraint", p_con env c)] + @ (case E.resolveFailureCause () of + NONE => [] + | SOME c' => [("Reduced to unresolvable", p_con env c')]))) | IllegalRec (x, e) => (ErrorMsg.errorAt (#2 e) "Illegal 'val rec' righthand side (must be a function abstraction)"; eprefaces' [("Variable", PD.string x), diff --git a/src/elaborate.sml b/src/elaborate.sml index f098b580..5799d6bb 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -4676,7 +4676,13 @@ fun elabFile basis basis_tm topStr topSgn top_tm env file = (!delayedUnifs);*) end | TypeClass (env, c, r, loc) => - expError env (Unresolvable (loc, c))) + let + val c = normClassKey env c + in + case resolveClass env c of + SOME _ => raise Fail "Type class resolution succeeded unexpectedly" + | NONE => expError env (Unresolvable (loc, c)) + end) gs) end in diff --git a/tests/classFail.ur b/tests/classFail.ur new file mode 100644 index 00000000..dd7b66e9 --- /dev/null +++ b/tests/classFail.ur @@ -0,0 +1,3 @@ +val x = show 7 +val y = show (8, 9) +val z : (show int * show unit) = _ -- cgit v1.2.3 From 4635acd2d4e4404b2b1a89909cd765ac310d62c5 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Fri, 27 Nov 2015 15:28:12 -0500 Subject: Fix tricky case of functor signature subsumption --- src/elab_env.sig | 2 ++ src/elab_env.sml | 4 ++++ src/elaborate.sml | 9 +++++++-- tests/subfunctor.ur | 6 ++++++ tests/subfunctor.urs | 3 +++ 5 files changed, 22 insertions(+), 2 deletions(-) create mode 100644 tests/subfunctor.ur create mode 100644 tests/subfunctor.urs (limited to 'src/elab_env.sig') diff --git a/src/elab_env.sig b/src/elab_env.sig index e0c589c4..cbc85cdd 100644 --- a/src/elab_env.sig +++ b/src/elab_env.sig @@ -37,6 +37,8 @@ signature ELAB_ENV = sig type env + val dump : env -> unit + val empty : env exception UnboundRel of int diff --git a/src/elab_env.sml b/src/elab_env.sml index 9c9cd14f..3523b576 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -239,6 +239,10 @@ type env = { str : (string * sgn) IM.map } +fun dump (env : env) = + (print "NamedC:\n"; + IM.appi (fn (n, (x, k, co)) => print (x ^ " [" ^ Int.toString n ^ "]\n")) (#namedC env)) + val namedCounter = ref 0 fun newNamed () = diff --git a/src/elaborate.sml b/src/elaborate.sml index 7671f597..25cce6bd 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -1359,7 +1359,9 @@ end and unifyCons env loc c1 c2 = - unifyCons' env loc c1 c2 + ((*Print.prefaces "uc" [("c1", p_con env c1), + ("c2", p_con env c2)];*) + unifyCons' env loc c1 c2) handle CUnify' (env', err) => raise CUnify (c1, c2, env', err) | KUnify (arg as {3 = env', ...}) => raise CUnify (c1, c2, env', CKind arg) @@ -3079,6 +3081,8 @@ and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) = fun cpart n = IM.find (!counterparts, n) fun cparts (n2, n1) = counterparts := IM.insert (!counterparts, n2, n1) + fun uncparts n2 = (counterparts := #1 (IM.remove (!counterparts, n2))) + handle NotFound => () val sub2 = U.Con.map {kind = fn k => k, con = fn c => @@ -3107,7 +3111,8 @@ and subSgn' counterparts env strLoc sgn1 (sgn2 as (_, loc2)) = if E.checkENamed env n then env else - E.pushCNamedAs env x n k (SOME c) + (uncparts n; + E.pushCNamedAs env x n k (SOME c)) | L'.SgiConAbs (x, n, k) => if E.checkENamed env n then env diff --git a/tests/subfunctor.ur b/tests/subfunctor.ur new file mode 100644 index 00000000..3c2aa83f --- /dev/null +++ b/tests/subfunctor.ur @@ -0,0 +1,6 @@ +functor F(M : sig con fs :: {Type} end) = struct + open M + + functor G(M : sig val x : $(map sql_injectable_prim fs) end) = struct + end +end diff --git a/tests/subfunctor.urs b/tests/subfunctor.urs new file mode 100644 index 00000000..db393d21 --- /dev/null +++ b/tests/subfunctor.urs @@ -0,0 +1,3 @@ +functor F(M : sig con fs :: {Type} end) : sig + functor G(M : sig val x : $(map sql_injectable_prim M.fs) end) : sig end +end -- cgit v1.2.3