Simple elaboration working

10 files changed, 256 insertions, 74 deletions

diff --git a/src/elab_env.sig b/src/elab_env.sig
index f24206ee..075fe0dd 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -42,9 +42,9 @@ signature ELAB_ENV = sig
     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
 
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 2199ccbe..27ea1750 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -50,7 +50,7 @@ datatype 'a var =
 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 @@ fun lookupCRel (env : env) n =
     (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 =
diff --git a/src/elab_print.sig b/src/elab_print.sig
index b6ff2f27..66ae8d43 100644
--- a/src/elab_print.sig
+++ b/src/elab_print.sig
@@ -34,5 +34,7 @@ signature ELAB_PRINT = sig
     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
 
diff --git a/src/elab_print.sml b/src/elab_print.sml
index 451a9e5d..83e8f814 100644
--- a/src/elab_print.sml
+++ b/src/elab_print.sml
@@ -36,6 +36,8 @@ open Elab
 
 structure E = ElabEnv
 
+val debug = ref false
+
 fun p_kind' par (k, _) =
     case k of
         KType => string "Type"
@@ -85,8 +87,16 @@ fun p_con' par env (c, _) =
       | 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 @@ 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)
+        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 @@ 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",
-                                  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
diff --git a/src/elab_util.sig b/src/elab_util.sig
index 1f7ff2f9..4782d69d 100644
--- a/src/elab_util.sig
+++ b/src/elab_util.sig
@@ -34,14 +34,38 @@ structure Kind : sig
 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}
diff --git a/src/elab_util.sml b/src/elab_util.sml
index c07ff667..2550f638 100644
--- a/src/elab_util.sml
+++ b/src/elab_util.sml
@@ -77,44 +77,48 @@ end
 
 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 @@ fun mapfold {kind = fk, con = fc} =
                 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 @@ end
 
 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'}
+
+        fun mfe ctx e acc =
+            S.bindP (mfe' ctx e acc, fe ctx)
 
-        and mfe' (eAll as (e, loc)) =
+        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 @@ fun mapfold {kind = fk, con = fc, exp = fe} =
         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 @@ structure E = ElabEnv
 
 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
diff --git a/src/elaborate.sml b/src/elaborate.sml
index 5c81cec4..0b705fea 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -336,7 +336,21 @@ fun cunifyError env err =
                   [("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 @@ fun unifyCons env c1 c2 =
 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 @@ fun expError env err =
                      ("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 @@ fun elabExp env (e, loc) =
             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 (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
-      | L.ECAbs _ => raise Fail "ECAbs"
 
 datatype decl_error =
          KunifsRemainKind of ErrorMsg.span * L'.kind
@@ -532,7 +611,7 @@ fun elabDecl env (d, loc) =
                         | 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';
 
diff --git a/src/search.sig b/src/search.sig
index 102ef558..ac867146 100644
--- a/src/search.sig
+++ b/src/search.sig
@@ -34,7 +34,10 @@ signature SEARCH = sig
     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 @@ signature SEARCH = sig
     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
diff --git a/src/search.sml b/src/search.sml
index 6b78e9b2..563496fe 100644
--- a/src/search.sml
+++ b/src/search.sml
@@ -37,6 +37,9 @@ type ('data, 'state, 'abort) mapfold_arg =
 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) =
diff --git a/tests/stuff.lac b/tests/stuff.lac
index db29d5db..8348f5a1 100644
--- a/tests/stuff.lac
+++ b/tests/stuff.lac
@@ -15,4 +15,4 @@ con c9 = {}
 con c10 = ([]) :: {Type}
 
 val v1 = fn t :: Type => fn x : t => x
-val v2 = v1 [c1] (fn y => y)
+val v2 = v1 [t :: Type -> t -> t] v1