diff options
| -rw-r--r-- | src/elab.sml | 13 | ||||
| -rw-r--r-- | src/elab_env.sig | 20 | ||||
| -rw-r--r-- | src/elab_env.sml | 98 | ||||
| -rw-r--r-- | src/elab_print.sml | 52 | ||||
| -rw-r--r-- | src/elab_util.sml | 1 | ||||
| -rw-r--r-- | src/elaborate.sml | 6 |
6 files changed, 164 insertions, 26 deletions
diff --git a/src/elab.sml b/src/elab.sml index 5e1a3a9b..a289d633 100644 --- a/src/elab.sml +++ b/src/elab.sml @@ -64,8 +64,21 @@ datatype con' = withtype con = con' located +datatype exp' = + ERel of int + | ENamed of int + | EApp of exp * exp + | EAbs of string * con * exp + | ECApp of exp * con + | ECAbs of explicitness * string * kind * exp + + | EError + +withtype exp = exp' located + datatype decl' = DCon of string * int * kind * con + | DVal of string * int * con * exp withtype decl = decl' located diff --git a/src/elab_env.sig b/src/elab_env.sig index c4e5ae5a..f24206ee 100644 --- a/src/elab_env.sig +++ b/src/elab_env.sig @@ -34,17 +34,27 @@ signature ELAB_ENV = sig exception UnboundRel of int exception UnboundNamed of int + datatype 'a var = + NotBound + | Rel of int * 'a + | Named of int * 'a + 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 lookupC : env -> string -> Elab.kind var + + val pushERel : env -> string -> Elab.con -> env + val lookupERel : env -> int -> string * Elab.con + + val pushENamed : env -> string -> Elab.con -> env * int + val pushENamedAs : env -> string -> int -> Elab.con -> env + val lookupENamed : env -> int -> string * Elab.con - datatype var = - CNotBound - | CRel of int * Elab.kind - | CNamed of int * Elab.kind - val lookupC : env -> string -> var + val lookupE : env -> string -> Elab.con var end diff --git a/src/elab_env.sml b/src/elab_env.sml index 9a2655e4..2199ccbe 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -38,19 +38,23 @@ structure SM = BinaryMapFn(struct exception UnboundRel of int exception UnboundNamed of int -datatype var' = - CRel' of int * kind - | CNamed' of int * kind +datatype 'a var' = + Rel' of int * 'a + | Named' of int * 'a -datatype var = - CNotBound - | CRel of int * kind - | CNamed of int * kind +datatype 'a var = + NotBound + | Rel of int * 'a + | Named of int * 'a type env = { - renameC : var' SM.map, + renameC : kind var' SM.map, relC : (string * kind) list, - namedC : (string * kind) IM.map + namedC : (string * kind) IM.map, + + renameE : con var' SM.map, + relE : (string * con) list, + namedE : (string * con) IM.map } val namedCounter = ref 0 @@ -58,17 +62,25 @@ val namedCounter = ref 0 val empty = { renameC = SM.empty, relC = [], - namedC = IM.empty + namedC = IM.empty, + + renameE = SM.empty, + relE = [], + namedE = IM.empty } fun pushCRel (env : env) x k = let - val renameC = SM.map (fn CRel' (n, k) => CRel' (n+1, k) + val renameC = SM.map (fn Rel' (n, k) => Rel' (n+1, k) | x => x) (#renameC env) in - {renameC = SM.insert (renameC, x, CRel' (0, k)), + {renameC = SM.insert (renameC, x, Rel' (0, k)), relC = (x, k) :: #relC env, - namedC = #namedC env} + namedC = #namedC env, + + renameE = #renameE env, + relE = #relE env, + namedE = #namedE env} end fun lookupCRel (env : env) n = @@ -76,9 +88,13 @@ fun lookupCRel (env : env) n = handle Subscript => raise UnboundRel n fun pushCNamedAs (env : env) x n k = - {renameC = SM.insert (#renameC env, x, CNamed' (n, k)), + {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)), + + renameE = #renameE env, + relE = #relE env, + namedE = #namedE env} fun pushCNamed env x k = let @@ -95,8 +111,54 @@ fun lookupCNamed (env : env) n = fun lookupC (env : env) x = case SM.find (#renameC env, x) of - NONE => CNotBound - | SOME (CRel' x) => CRel x - | SOME (CNamed' x) => CNamed x + NONE => NotBound + | SOME (Rel' x) => Rel x + | SOME (Named' x) => Named x + +fun pushERel (env : env) x t = + let + val renameE = SM.map (fn Rel' (n, t) => Rel' (n+1, t) + | x => x) (#renameE env) + in + {renameC = #renameC env, + relC = #relC env, + namedC = #namedC env, + + renameE = SM.insert (renameE, x, Rel' (0, t)), + relE = (x, t) :: #relE env, + namedE = #namedE env} + end + +fun lookupERel (env : env) n = + (List.nth (#relE env, n)) + handle Subscript => raise UnboundRel n + +fun pushENamedAs (env : env) x n t = + {renameC = #renameC env, + relC = #relC env, + namedC = #namedC env, + + renameE = SM.insert (#renameE env, x, Named' (n, t)), + relE = #relE env, + namedE = IM.insert (#namedE env, n, (x, t))} + +fun pushENamed env x t = + let + val n = !namedCounter + in + namedCounter := n + 1; + (pushENamedAs env x n t, n) + end + +fun lookupENamed (env : env) n = + case IM.find (#namedE env, n) of + NONE => raise UnboundNamed n + | SOME x => x + +fun lookupE (env : env) x = + case SM.find (#renameE env, x) of + NONE => NotBound + | SOME (Rel' x) => Rel x + | SOME (Named' x) => Named x end diff --git a/src/elab_print.sml b/src/elab_print.sml index 98d9e196..451a9e5d 100644 --- a/src/elab_print.sml +++ b/src/elab_print.sml @@ -128,6 +128,45 @@ fun p_con' par env (c, _) = and p_con env = p_con' false env +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) + | EApp (e1, e2) => parenIf par (box [p_exp env e1, + space, + p_exp' true env e2]) + | EAbs (x, t, e) => parenIf par (box [string "fn", + space, + string x, + space, + string ":", + space, + p_con env t, + space, + string "=>", + space, + p_exp (E.pushERel env x t) e]) + | ECApp (e, c) => parenIf par (box [p_exp env e, + space, + string "[", + p_con env c, + string "]"]) + | ECAbs (exp, x, k, e) => parenIf par (box [string "fn", + space, + string x, + space, + p_explicitness exp, + space, + p_kind k, + space, + string "=>", + space, + p_exp (E.pushCRel env x k) e]) + + | EError => string "<ERROR>" + +and p_exp env = p_exp' false env + fun p_decl env ((d, _) : decl) = case d of DCon (x, n, k, c) => box [string "con", @@ -143,6 +182,19 @@ fun p_decl env ((d, _) : decl) = 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] fun p_file env file = let diff --git a/src/elab_util.sml b/src/elab_util.sml index 3b608710..ef0e740f 100644 --- a/src/elab_util.sml +++ b/src/elab_util.sml @@ -167,5 +167,6 @@ structure E = ElabEnv fun declBinds env (d, _) = case d of DCon (x, n, k, _) => E.pushCNamedAs env x n k + | DVal (x, n, t, _) => E.pushENamedAs env x n t end diff --git a/src/elaborate.sml b/src/elaborate.sml index 3e2cac1b..6fca31b1 100644 --- a/src/elaborate.sml +++ b/src/elaborate.sml @@ -201,12 +201,12 @@ fun elabCon env (c, loc) = | L.CVar s => (case E.lookupC env s of - E.CNotBound => + E.NotBound => (conError env (UnboundCon (loc, s)); (cerror, kerror)) - | E.CRel (n, k) => + | E.Rel (n, k) => ((L'.CRel n, loc), k) - | E.CNamed (n, k) => + | E.Named (n, k) => ((L'.CNamed n, loc), k)) | L.CApp (c1, c2) => let |