Mercurial > urweb
changeset 11:e97c6d335869
Simple elaboration working
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Fri, 28 Mar 2008 15:20:46 -0400 |
| parents | dde5c52e5e5e |
| children | d89477f07c1e |
| files | src/elab_env.sig src/elab_env.sml src/elab_print.sig src/elab_print.sml src/elab_util.sig src/elab_util.sml src/elaborate.sml src/search.sig src/search.sml tests/stuff.lac |
| diffstat | 10 files changed, 256 insertions(+), 74 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elab_env.sig Fri Mar 28 13:59:03 2008 -0400 +++ b/src/elab_env.sig Fri Mar 28 15:20:46 2008 -0400 @@ -42,9 +42,9 @@ val pushCRel : env -> string -> Elab.kind -> env val lookupCRel : env -> int -> string * Elab.kind - val pushCNamed : env -> string -> Elab.kind -> env * int - val pushCNamedAs : env -> string -> int -> Elab.kind -> env - val lookupCNamed : env -> int -> string * Elab.kind + val pushCNamed : env -> string -> Elab.kind -> Elab.con option -> env * int + val pushCNamedAs : env -> string -> int -> Elab.kind -> Elab.con option -> env + val lookupCNamed : env -> int -> string * Elab.kind * Elab.con option val lookupC : env -> string -> Elab.kind var
--- a/src/elab_env.sml Fri Mar 28 13:59:03 2008 -0400 +++ b/src/elab_env.sml Fri Mar 28 15:20:46 2008 -0400 @@ -50,7 +50,7 @@ type env = { renameC : kind var' SM.map, relC : (string * kind) list, - namedC : (string * kind) IM.map, + namedC : (string * kind * con option) IM.map, renameE : con var' SM.map, relE : (string * con) list, @@ -87,21 +87,21 @@ (List.nth (#relC env, n)) handle Subscript => raise UnboundRel n -fun pushCNamedAs (env : env) x n k = +fun pushCNamedAs (env : env) x n k co = {renameC = SM.insert (#renameC env, x, Named' (n, k)), relC = #relC env, - namedC = IM.insert (#namedC env, n, (x, k)), + namedC = IM.insert (#namedC env, n, (x, k, co)), renameE = #renameE env, relE = #relE env, namedE = #namedE env} -fun pushCNamed env x k = +fun pushCNamed env x k co = let val n = !namedCounter in namedCounter := n + 1; - (pushCNamedAs env x n k, n) + (pushCNamedAs env x n k co, n) end fun lookupCNamed (env : env) n =
--- a/src/elab_print.sig Fri Mar 28 13:59:03 2008 -0400 +++ b/src/elab_print.sig Fri Mar 28 15:20:46 2008 -0400 @@ -34,5 +34,7 @@ val p_exp : ElabEnv.env -> Elab.exp Print.printer val p_decl : ElabEnv.env -> Elab.decl Print.printer val p_file : ElabEnv.env -> Elab.file Print.printer + + val debug : bool ref end
--- a/src/elab_print.sml Fri Mar 28 13:59:03 2008 -0400 +++ b/src/elab_print.sml Fri Mar 28 15:20:46 2008 -0400 @@ -36,6 +36,8 @@ structure E = ElabEnv +val debug = ref false + fun p_kind' par (k, _) = case k of KType => string "Type" @@ -85,8 +87,16 @@ | TRecord c => box [string "$", p_con' true env c] - | CRel n => string (#1 (E.lookupCRel env n) ^ "_" ^ Int.toString n) - | CNamed n => string (#1 (E.lookupCNamed env n) ^ "__" ^ Int.toString n) + | CRel n => + if !debug then + string (#1 (E.lookupCRel env n) ^ "_" ^ Int.toString n) + else + string (#1 (E.lookupCRel env n)) + | CNamed n => + if !debug then + string (#1 (E.lookupCNamed env n) ^ "__" ^ Int.toString n) + else + string (#1 (E.lookupCNamed env n)) | CApp (c1, c2) => parenIf par (box [p_con env c1, space, @@ -130,8 +140,16 @@ fun p_exp' par env (e, _) = case e of - ERel n => string (#1 (E.lookupERel env n) ^ "_" ^ Int.toString n) - | ENamed n => string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n) + ERel n => + if !debug then + string (#1 (E.lookupERel env n) ^ "_" ^ Int.toString n) + else + string (#1 (E.lookupERel env n)) + | ENamed n => + if !debug then + string (#1 (E.lookupENamed env n) ^ "__" ^ Int.toString n) + else + string (#1 (E.lookupENamed env n)) | EApp (e1, e2) => parenIf par (box [p_exp env e1, space, p_exp' true env e2]) @@ -169,32 +187,48 @@ fun p_decl env ((d, _) : decl) = case d of - DCon (x, n, k, c) => box [string "con", - space, - string x, - string "__", - string (Int.toString n), - space, - string "::", - space, - p_kind k, - space, - string "=", - space, - p_con env c] - | DVal (x, n, t, e) => box [string "val", - space, - string x, - string "__", - string (Int.toString n), - space, - string ":", - space, - p_con env t, - space, - string "=", - space, - p_exp env e] + DCon (x, n, k, c) => + let + val xp = if !debug then + box [string x, + string "__", + string (Int.toString n)] + else + string x + in + box [string "con", + space, + xp, + space, + string "::", + space, + p_kind k, + space, + string "=", + space, + p_con env c] + end + | DVal (x, n, t, e) => + let + val xp = if !debug then + box [string x, + string "__", + string (Int.toString n)] + else + string x + in + box [string "val", + space, + xp, + space, + string ":", + space, + p_con env t, + space, + string "=", + space, + p_exp env e] + end fun p_file env file = let
--- a/src/elab_util.sig Fri Mar 28 13:59:03 2008 -0400 +++ b/src/elab_util.sig Fri Mar 28 15:20:46 2008 -0400 @@ -34,14 +34,38 @@ end structure Con : sig + datatype binder = + Rel of string * Elab.kind + | Named of string * Elab.kind + + val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, + con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, + bind : 'context * binder -> 'context} + -> ('context, Elab.con, 'state, 'abort) Search.mapfolderB val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, con : (Elab.con', 'state, 'abort) Search.mapfolder} -> (Elab.con, 'state, 'abort) Search.mapfolder + + val mapB : {kind : Elab.kind' -> Elab.kind', + con : 'context -> Elab.con' -> Elab.con', + bind : 'context * binder -> 'context} + -> 'context -> (Elab.con -> Elab.con) val exists : {kind : Elab.kind' -> bool, con : Elab.con' -> bool} -> Elab.con -> bool end structure Exp : sig + datatype binder = + RelC of string * Elab.kind + | NamedC of string * Elab.kind + | RelE of string * Elab.con + | NamedE of string * Elab.con + + val mapfoldB : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, + con : ('context, Elab.con', 'state, 'abort) Search.mapfolderB, + exp : ('context, Elab.exp', 'state, 'abort) Search.mapfolderB, + bind : 'context * binder -> 'context} + -> ('context, Elab.exp, 'state, 'abort) Search.mapfolderB val mapfold : {kind : (Elab.kind', 'state, 'abort) Search.mapfolder, con : (Elab.con', 'state, 'abort) Search.mapfolder, exp : (Elab.exp', 'state, 'abort) Search.mapfolder}
--- a/src/elab_util.sml Fri Mar 28 13:59:03 2008 -0400 +++ b/src/elab_util.sml Fri Mar 28 15:20:46 2008 -0400 @@ -77,44 +77,48 @@ structure Con = struct -fun mapfold {kind = fk, con = fc} = +datatype binder = + Rel of string * Elab.kind + | Named of string * Elab.kind + +fun mapfoldB {kind = fk, con = fc, bind} = let val mfk = Kind.mapfold fk - fun mfc c acc = - S.bindP (mfc' c acc, fc) + fun mfc ctx c acc = + S.bindP (mfc' ctx c acc, fc ctx) - and mfc' (cAll as (c, loc)) = + and mfc' ctx (cAll as (c, loc)) = case c of TFun (c1, c2) => - S.bind2 (mfc c1, + S.bind2 (mfc ctx c1, fn c1' => - S.map2 (mfc c2, + S.map2 (mfc ctx c2, fn c2' => (TFun (c1', c2'), loc))) | TCFun (e, x, k, c) => S.bind2 (mfk k, fn k' => - S.map2 (mfc c, + S.map2 (mfc (bind (ctx, Rel (x, k))) c, fn c' => (TCFun (e, x, k', c'), loc))) | TRecord c => - S.map2 (mfc c, + S.map2 (mfc ctx c, fn c' => (TRecord c', loc)) | CRel _ => S.return2 cAll | CNamed _ => S.return2 cAll | CApp (c1, c2) => - S.bind2 (mfc c1, + S.bind2 (mfc ctx c1, fn c1' => - S.map2 (mfc c2, + S.map2 (mfc ctx c2, fn c2' => (CApp (c1', c2'), loc))) | CAbs (x, k, c) => S.bind2 (mfk k, fn k' => - S.map2 (mfc c, + S.map2 (mfc (bind (ctx, Rel (x, k))) c, fn c' => (CAbs (x, k', c'), loc))) @@ -124,28 +128,40 @@ S.bind2 (mfk k, fn k' => S.map2 (ListUtil.mapfold (fn (x, c) => - S.bind2 (mfc x, + S.bind2 (mfc ctx x, fn x' => - S.map2 (mfc c, + S.map2 (mfc ctx c, fn c' => (x', c')))) xcs, fn xcs' => (CRecord (k', xcs'), loc))) | CConcat (c1, c2) => - S.bind2 (mfc c1, + S.bind2 (mfc ctx c1, fn c1' => - S.map2 (mfc c2, + S.map2 (mfc ctx c2, fn c2' => (CConcat (c1', c2'), loc))) | CError => S.return2 cAll - | CUnif (_, _, ref (SOME c)) => mfc' c + | CUnif (_, _, ref (SOME c)) => mfc' ctx c | CUnif _ => S.return2 cAll in mfc end +fun mapfold {kind = fk, con = fc} = + mapfoldB {kind = fk, + con = fn () => fc, + bind = fn ((), _) => ()} () + +fun mapB {kind, con, bind} ctx c = + case mapfoldB {kind = fn k => fn () => S.Continue (kind k, ()), + con = fn ctx => fn c => fn () => S.Continue (con ctx c, ()), + bind = bind} ctx c () of + S.Continue (c, ()) => c + | S.Return _ => raise Fail "Con.mapB: Impossible" + fun exists {kind, con} k = case mapfold {kind = fn k => fn () => if kind k then @@ -164,41 +180,56 @@ structure Exp = struct -fun mapfold {kind = fk, con = fc, exp = fe} = +datatype binder = + RelC of string * Elab.kind + | NamedC of string * 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 mfc = Con.mapfold {kind = fk, con = fc} - fun mfe e acc = - S.bindP (mfe' e acc, fe) + fun bind' (ctx, b) = + let + val b' = case b of + Con.Rel x => RelC x + | Con.Named x => NamedC x + in + bind (ctx, b') + end + val mfc = Con.mapfoldB {kind = fk, con = fc, bind = bind'} - and mfe' (eAll as (e, loc)) = + fun mfe ctx e acc = + S.bindP (mfe' ctx e acc, fe ctx) + + and mfe' ctx (eAll as (e, loc)) = case e of ERel _ => S.return2 eAll | ENamed _ => S.return2 eAll | EApp (e1, e2) => - S.bind2 (mfe e1, + S.bind2 (mfe ctx e1, fn e1' => - S.map2 (mfe e2, + S.map2 (mfe ctx e2, fn e2' => (EApp (e1', e2'), loc))) | EAbs (x, t, e) => - S.bind2 (mfc t, + S.bind2 (mfc ctx t, fn t' => - S.map2 (mfe e, + S.map2 (mfe (bind (ctx, RelE (x, t))) e, fn e' => (EAbs (x, t', e'), loc))) | ECApp (e, c) => - S.bind2 (mfe e, + S.bind2 (mfe ctx e, fn e' => - S.map2 (mfc c, + S.map2 (mfc ctx c, fn c' => (ECApp (e', c'), loc))) | ECAbs (expl, x, k, e) => S.bind2 (mfk k, fn k' => - S.map2 (mfe e, + S.map2 (mfe (bind (ctx, RelC (x, k))) e, fn e' => (ECAbs (expl, x, k', e'), loc))) @@ -207,6 +238,12 @@ mfe end +fun mapfold {kind = fk, con = fc, exp = fe} = + mapfoldB {kind = fk, + con = fn () => fc, + exp = fn () => fe, + bind = fn ((), _) => ()} () + fun exists {kind, con, exp} k = case mapfold {kind = fn k => fn () => if kind k then @@ -232,7 +269,7 @@ fun declBinds env (d, _) = case d of - DCon (x, n, k, _) => E.pushCNamedAs env x n k + DCon (x, n, k, c) => E.pushCNamedAs env x n k (SOME c) | DVal (x, n, t, _) => E.pushENamedAs env x n t end
--- a/src/elaborate.sml Fri Mar 28 13:59:03 2008 -0400 +++ b/src/elaborate.sml Fri Mar 28 15:20:46 2008 -0400 @@ -336,7 +336,21 @@ [("Con 1", p_con env c1), ("Con 2", p_con env c2)] -fun unifyCons' env (c1All as (c1, _)) (c2All as (c2, _)) = +fun hnormCon env (cAll as (c, _)) = + case c of + L'.CUnif (_, _, ref (SOME c)) => hnormCon env c + + | L'.CNamed xn => + (case E.lookupCNamed env xn of + (_, _, SOME c') => hnormCon env c' + | _ => cAll) + + | _ => cAll + +fun unifyCons' env c1 c2 = + unifyCons'' env (hnormCon env c1) (hnormCon env c2) + +and unifyCons'' env (c1All as (c1, _)) (c2All as (c2, _)) = let fun err f = raise CUnify' (f (c1All, c2All)) in @@ -424,6 +438,8 @@ datatype exp_error = UnboundExp of ErrorMsg.span * string | Unify of L'.exp * L'.con * L'.con * cunify_error + | Unif of string * L'.con + | WrongForm of string * L'.exp * L'.con fun expError env err = case err of @@ -435,12 +451,49 @@ ("Have con", p_con env c1), ("Need con", p_con env c2)]; cunifyError env uerr) + | Unif (action, c) => + (ErrorMsg.errorAt (#2 c) ("Unification variable blocks " ^ action); + eprefaces' [("Con", p_con env c)]) + | WrongForm (variety, e, t) => + (ErrorMsg.errorAt (#2 e) ("Expression is not a " ^ variety); + eprefaces' [("Expression", p_exp env e), + ("Type", p_con env t)]) fun checkCon env e c1 c2 = unifyCons env c1 c2 handle CUnify (c1, c2, err) => expError env (Unify (e, c1, c2, err)) +exception SynUnif + +val liftConInCon = + U.Con.mapB {kind = fn k => k, + con = fn bound => fn c => + case c of + L'.CRel xn => + if xn < bound then + c + else + L'.CRel (xn + 1) + | L'.CUnif _ => raise SynUnif + | _ => c, + bind = fn (bound, U.Con.Rel _) => bound + 1 + | (bound, _) => bound} + +val subConInCon = + U.Con.mapB {kind = fn k => k, + con = fn (xn, rep) => fn c => + case c of + L'.CRel xn' => + if xn = xn' then + #1 rep + else + c + | L'.CUnif _ => raise SynUnif + | _ => c, + bind = fn ((xn, rep), U.Con.Rel _) => (xn+1, liftConInCon 0 rep) + | (ctx, _) => ctx} + fun elabExp env (e, loc) = case e of L.EAnnot (e, t) => @@ -493,9 +546,35 @@ val (e', et) = elabExp env e val (c', ck) = elabCon env c in - raise Fail "ECApp" + case #1 (hnormCon env et) of + L'.CError => (eerror, cerror) + | L'.TCFun (_, _, k, eb) => + let + val () = checkKind env c' ck k + val eb' = subConInCon (0, c') eb + handle SynUnif => (expError env (Unif ("substitution", eb)); + cerror) + in + ((L'.ECApp (e', c'), loc), eb') + end + + | L'.CUnif _ => + (expError env (Unif ("application", et)); + (eerror, cerror)) + + | _ => + (expError env (WrongForm ("constructor function", e', et)); + (eerror, cerror)) end - | L.ECAbs _ => raise Fail "ECAbs" + | L.ECAbs (expl, x, k, e) => + let + val expl' = elabExplicitness expl + val k' = elabKind k + val (e', et) = elabExp (E.pushCRel env x k') e + in + ((L'.ECAbs (expl', x, k', e'), loc), + (L'.TCFun (expl', x, k', et), loc)) + end datatype decl_error = KunifsRemainKind of ErrorMsg.span * L'.kind @@ -532,7 +611,7 @@ | SOME k => elabKind k val (c', ck) = elabCon env c - val (env', n) = E.pushCNamed env x k' + val (env', n) = E.pushCNamed env x k' (SOME c') in checkKind env c' ck k';
--- a/src/search.sig Fri Mar 28 13:59:03 2008 -0400 +++ b/src/search.sig Fri Mar 28 15:20:46 2008 -0400 @@ -34,7 +34,10 @@ type ('data, 'state, 'abort) mapfolder = 'data -> 'state -> ('data * 'state, 'abort) result - val return2 : 'state1 -> 'state2 -> ('state1 * 'state2, 'abort) result + type ('context, 'data, 'state, 'abort) mapfolderB = + 'context -> 'data -> 'state -> ('data * 'state, 'abort) result + + val return2 : 'data -> 'state -> ('data * 'state, 'abort) result val map : ('state1, 'abort) result * ('state1 -> 'state2) @@ -43,7 +46,7 @@ val map2 : ('state2 -> ('state1 * 'state2, 'abort) result) * ('state1 -> 'state1') -> ('state2 -> ('state1' * 'state2, 'abort) result) - + val bind : ('state1, 'abort) result * ('state1 -> ('state2, 'abort) result) -> ('state2, 'abort) result
--- a/src/search.sml Fri Mar 28 13:59:03 2008 -0400 +++ b/src/search.sml Fri Mar 28 15:20:46 2008 -0400 @@ -37,6 +37,9 @@ type ('data, 'state, 'abort) mapfolder = 'data -> 'state -> ('data * 'state, 'abort) result +type ('context, 'data, 'state, 'abort) mapfolderB = + 'context -> 'data -> 'state -> ('data * 'state, 'abort) result + fun return2 v acc = Continue (v, acc) fun map (r, f) =