# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1201386374 18000
# Node ID 14b533dbe6ccc969c92a7291fc922518f94b76a7
# Parent  a455a9f85cc3fa290628459f6f10f31ac6942ba4
Added simple expression constructors to Elab

diff -r a455a9f85cc3 -r 14b533dbe6cc src/elab.sml
--- a/src/elab.sml	Sat Jan 26 17:10:26 2008 -0500
+++ b/src/elab.sml	Sat Jan 26 17:26:14 2008 -0500
@@ -64,8 +64,21 @@
 
 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 -r a455a9f85cc3 -r 14b533dbe6cc src/elab_env.sig
--- a/src/elab_env.sig	Sat Jan 26 17:10:26 2008 -0500
+++ b/src/elab_env.sig	Sat Jan 26 17:26:14 2008 -0500
@@ -34,17 +34,27 @@
     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 -r a455a9f85cc3 -r 14b533dbe6cc src/elab_env.sml
--- a/src/elab_env.sml	Sat Jan 26 17:10:26 2008 -0500
+++ b/src/elab_env.sml	Sat Jan 26 17:26:14 2008 -0500
@@ -38,19 +38,23 @@
 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 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 @@
     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 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 -r a455a9f85cc3 -r 14b533dbe6cc src/elab_print.sml
--- a/src/elab_print.sml	Sat Jan 26 17:10:26 2008 -0500
+++ b/src/elab_print.sml	Sat Jan 26 17:26:14 2008 -0500
@@ -128,6 +128,45 @@
         
 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 @@
                                   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 -r a455a9f85cc3 -r 14b533dbe6cc src/elab_util.sml
--- a/src/elab_util.sml	Sat Jan 26 17:10:26 2008 -0500
+++ b/src/elab_util.sml	Sat Jan 26 17:26:14 2008 -0500
@@ -167,5 +167,6 @@
 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 -r a455a9f85cc3 -r 14b533dbe6cc src/elaborate.sml
--- a/src/elaborate.sml	Sat Jan 26 17:10:26 2008 -0500
+++ b/src/elaborate.sml	Sat Jan 26 17:26:14 2008 -0500
@@ -201,12 +201,12 @@
 
       | 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