From ba51720d4d47b15ae3ec87ca60c3e83ee91ada13 Mon Sep 17 00:00:00 2001
From: Simon Huber <hubsim@gmail.com>
Date: Wed, 8 Apr 2015 22:14:55 +0200
Subject: [PATCH] split annotation is now the type not the family; typo in eval
 fixed

---
 Eval.hs        | 13 ++++++++-----
 Resolver.hs    | 13 +++----------
 TypeChecker.hs |  8 ++++----
 3 files changed, 15 insertions(+), 19 deletions(-)

diff --git a/Eval.hs b/Eval.hs
index ec9dc31..f58f057 100644
--- a/Eval.hs
+++ b/Eval.hs
@@ -145,7 +145,6 @@ eval rho v = case v of
     pcon name (eval rho a) (map (eval rho) ts) (evalFormula rho phi)
   Split{}             -> Ter v rho
   Sum{}               -> Ter v rho
-  Undef l             -> error $ "eval: undefined at " ++ show l
   IdP a e0 e1         -> VIdP (eval rho a) (eval rho e0) (eval rho e1)
   Path i t            ->
     let j = fresh rho
@@ -192,13 +191,14 @@ app (Ter (Split _ _ _ nvs) e) (VPCon c _ us phi) = case lookupBranch c nvs of
   Just (PBranch _ xs i t) -> eval (Sub (upds e (zip xs us)) (i,phi)) t
   _ -> error ("app: Split with insufficient arguments; " ++
               " missing case for " ++ c)
-app u@(Ter (Split _ _ f hbr) e) kan@(VComp v w ws) =
+app u@(Ter (Split _ _ ty hbr) e) kan@(VComp v w ws) =
   let j   = fresh (e,kan)
       wsj = Map.map (@@ j) ws
       ws' = mapWithKey (\alpha -> app (u `face` alpha)) wsj
       w'  = app u w
-      ffill = app (eval e f) (fill j v w wsj)
-  in genComp j ffill w' ws'
+  in case eval e ty of
+    VPi _ f -> genComp j (app f (fill j v w wsj)) w' ws'
+    _       -> error ("app: Split annotation not a Pi type " ++ show u)
 
 app kan@(VTrans (VPath i (VPi a f)) li0) ui1 =
     let j   = fresh (kan,ui1)
@@ -232,7 +232,10 @@ inferType v = case v of
     VSigma _ f -> app f (VFst t)
     ty         -> error $ "inferType: expected Sigma type for " ++ show v
                   ++ ", got " ++ show ty
-  VSplit (Ter (Split _ _ f _) rho) v1 -> app (eval rho f) v1
+  VSplit s@(Ter (Split _ _ t _) rho) v1 -> case eval rho t of
+    VPi _ f -> app f v1
+    ty      -> error $ "inferType: Pi type expected for split annotation in "
+               ++ show v ++ ", got " ++ show ty
   VApp t0 t1 -> case inferType t0 of
     VPi _ f -> app f t1
     ty      -> error $ "inferType: expected Pi type for " ++ show v
diff --git a/Resolver.hs b/Resolver.hs
index 30e9951..8d37210 100644
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -284,13 +284,6 @@ resolveLabel cs (PLabel n vdecl t0 t1) =
                           <*> local (insertIdents cs) (resolveExp t0)
                           <*> local (insertIdents cs) (resolveExp t1)
 
-piToFam :: ((Int,Int),String) -> Exp -> Resolver Ter
-piToFam _ (Fun a b)    = lam ("_",a) $ resolveExp b
-piToFam _ (Pi ptele b) = do
-  (x,a):tele <- flattenPTele ptele
-  lam (x,a) (binds CTT.Pi tele (resolveExp b))
-piToFam (l,n) _ = throwError $ "Pi type expected in " ++ n ++ " at " ++ show l
-
 -- Resolve Data or Def or Split declarations
 resolveDecl :: Decl -> Resolver (CTT.Decl,[(Ident,SymKind)])
 resolveDecl d = case d of
@@ -309,12 +302,12 @@ resolveDecl d = case d of
     return ((f,(a,d)),(f,Variable):cs ++ pcs)
   DeclSplit (AIdent (l,f)) tele t brs -> do
     let tele' = flattenTele tele
+        vars = map fst tele'
     loc  <- getLoc l
     a    <- binds CTT.Pi tele' (resolveExp t)
-    let vars = map fst tele'
-    fam  <- local (insertVars vars) $ piToFam (l,f) t
+    ty   <- local (insertVars vars) $ resolveExp t
     brs' <- local (insertVars (f:vars)) (mapM resolveBranch brs)
-    body <- lams tele' (return $ CTT.Split f loc fam brs')
+    body <- lams tele' (return $ CTT.Split f loc ty brs')
     return ((f,(a,body)),[(f,Variable)])
 
 resolveDecls :: [Decl] -> Resolver ([[CTT.Decl]],[(Ident,SymKind)])
diff --git a/TypeChecker.hs b/TypeChecker.hs
index 83431da..25bedd1 100644
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -156,10 +156,10 @@ check a t = case (a,t) of
       localM (addTele tele) $ do
         check (Ter t rho) t0
         check (Ter t rho) t1
-  (VPi va@(Ter (Sum _ _ cas) nu) f,Split _ _ f' ces) -> do
-    checkFam f'
+  (VPi va@(Ter (Sum _ _ cas) nu) f,Split _ _ ty ces) -> do
+    check VU ty
     rho <- asks env
-    unlessM (f === eval rho f') $ throwError "check: split annotations"
+    unlessM (a === eval rho ty) $ throwError "check: split annotations"
     if map labelName cas == map branchName ces
        then sequence_ [ checkBranch (lbl,nu) f brc (Ter t rho) va
                       | (brc, lbl) <- zip ces cas ]
@@ -205,7 +205,7 @@ check a t = case (a,t) of
 -- Check a list of declarations
 checkDecls :: [Decl] -> Typing ()
 checkDecls d = do
-  let (idents, tele, ters) = (declIdents d, declTele d, declTers d)
+  let (idents,tele,ters) = (declIdents d,declTele d,declTers d)
   trace ("Checking: " ++ unwords idents)
   checkTele tele
   rho <- asks env
-- 
2.34.1