Mercurial > urweb
changeset 15:1e645beb3f3b
Implicit constructor arguments
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Sun, 08 Jun 2008 13:00:12 -0400 |
| parents | f1c36df29ed7 |
| children | bc7b76ca57e0 |
| files | src/elaborate.sml src/lacweb.grm tests/impl.lac |
| diffstat | 3 files changed, 76 insertions(+), 25 deletions(-) [+] |
line wrap: on
line diff
--- a/src/elaborate.sml Sun Jun 08 12:27:08 2008 -0400 +++ b/src/elaborate.sml Sun Jun 08 13:00:12 2008 -0400 @@ -680,6 +680,43 @@ | E.Named _ => raise Fail ("Primitive type " ^ s ^ " bound at non-Type kind") end +fun typeof env (e, loc) = + case e of + L'.EPrim p => (primType env p, loc) + | L'.ERel n => #2 (E.lookupERel env n) + | L'.ENamed n => #2 (E.lookupENamed env n) + | L'.EApp (e1, _) => + (case #1 (typeof env e1) of + L'.TFun (_, c) => c + | _ => raise Fail "typeof: Bad EApp") + | L'.EAbs (x, t, e1) => (L'.TFun (t, typeof (E.pushERel env x t) e1), loc) + | L'.ECApp (e1, c) => + (case #1 (typeof env e1) of + L'.TCFun (_, _, _, c1) => subConInCon (0, c) c1 + | _ => raise Fail "typeof: Bad ECApp") + | L'.ECAbs (expl, x, k, e1) => (L'.TCFun (expl, x, k, typeof (E.pushCRel env x k) e1), loc) + + | L'.ERecord xes => (L'.TRecord (L'.CRecord (ktype, map (fn (x, e) => (x, typeof env e)) xes), loc), loc) + | L'.EField (_, _, {field, ...}) => field + + | L'.EError => cerror + +fun elabHead env (e as (_, loc)) t = + let + fun unravel (t, e) = + case hnormCon env t of + (L'.TCFun (L'.Implicit, x, k, t'), _) => + let + val u = cunif k + in + unravel (subConInCon (0, u) t', + (L'.ECApp (e, u), loc)) + end + | _ => (e, t) + in + unravel (t, e) + end + fun elabExp env (e, loc) = case e of L.EAnnot (e, t) => @@ -702,6 +739,7 @@ | L.EApp (e1, e2) => let val (e1', t1) = elabExp env e1 + val (e1', t1) = elabHead env e1' t1 val (e2', t2) = elabExp env e2 val dom = cunif ktype @@ -731,6 +769,7 @@ | L.ECApp (e, c) => let val (e', et) = elabExp env e + val (e', et) = elabHead env e' et val (c', ck) = elabCon env c in case #1 (hnormCon env et) of @@ -832,15 +871,19 @@ in checkKind env c' ck k'; - if kunifsInKind k' then - declError env (KunifsRemainKind (loc, k')) - else - (); + if ErrorMsg.anyErrors () then + () + else ( + if kunifsInKind k' then + declError env (KunifsRemainKind (loc, k')) + else + (); - if kunifsInCon c' then - declError env (KunifsRemainCon (loc, c')) - else - (); + if kunifsInCon c' then + declError env (KunifsRemainCon (loc, c')) + else + () + ); (env', (L'.DCon (x, n, k', c'), loc)) @@ -856,25 +899,28 @@ in checkCon env e' et c'; - if kunifsInCon c' then - declError env (KunifsRemainCon (loc, c')) - else - (); + if ErrorMsg.anyErrors () then + () + else ( + if kunifsInCon c' then + declError env (KunifsRemainCon (loc, c')) + else + (); - if cunifsInCon c' then - declError env (CunifsRemainCon (loc, c')) - else - (); + if cunifsInCon c' then + declError env (CunifsRemainCon (loc, c')) + else + (); - if kunifsInExp e' then - declError env (KunifsRemainExp (loc, e')) - else - (); + if kunifsInExp e' then + declError env (KunifsRemainExp (loc, e')) + else + (); - if cunifsInExp e' then - declError env (CunifsRemainExp (loc, e')) - else - (); + if cunifsInExp e' then + declError env (CunifsRemainExp (loc, e')) + else + ()); (env', (L'.DVal (x, n, c', e'), loc))
--- a/src/lacweb.grm Sun Jun 08 12:27:08 2008 -0400 +++ b/src/lacweb.grm Sun Jun 08 13:00:12 2008 -0400 @@ -108,7 +108,7 @@ 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)) + | SYMBOL kcolon kind ARROW cexp (TCFun (kcolon, SYMBOL, kind, cexp), s (SYMBOLleft, cexpright)) | cexp PLUSPLUS cexp (CConcat (cexp1, cexp2), s (cexp1left, cexp1right))