split annotation is now the type not the family; typo in eval fixed

diff --git a/Eval.hs b/Eval.hs
index ec9dc3122295b2f4a35c17faf8a2000cbe419a20..f58f0579065b4b3409aeb84385911a962f22b8b6 100644 (file)
--- 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 30e9951540f18d40123a5f8257ff9338446eb6a3..8d37210af78448a7df1e1f42f9bb1547d4196821 100644 (file)
--- 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 83431da252c5f19518619e19a666fa186046afea..25bedd1dfc65698a89b4d266017d49cc39c05ea0 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -156,10 +156,10 @@ check a t = case (a,t) of
       localM (addTele tele) $ do\r
         check (Ter t rho) t0\r
         check (Ter t rho) t1\r
-  (VPi va@(Ter (Sum _ _ cas) nu) f,Split _ _ f' ces) -> do\r
-    checkFam f'\r
+  (VPi va@(Ter (Sum _ _ cas) nu) f,Split _ _ ty ces) -> do\r
+    check VU ty\r
     rho <- asks env\r
-    unlessM (f === eval rho f') $ throwError "check: split annotations"\r
+    unlessM (a === eval rho ty) $ throwError "check: split annotations"\r
     if map labelName cas == map branchName ces\r
        then sequence_ [ checkBranch (lbl,nu) f brc (Ter t rho) va\r
                       | (brc, lbl) <- zip ces cas ]\r
@@ -205,7 +205,7 @@ check a t = case (a,t) of
 -- Check a list of declarations\r
 checkDecls :: [Decl] -> Typing ()\r
 checkDecls d = do\r
-  let (idents, tele, ters) = (declIdents d, declTele d, declTers d)\r
+  let (idents,tele,ters) = (declIdents d,declTele d,declTers d)\r
   trace ("Checking: " ++ unwords idents)\r
   checkTele tele\r
   rho <- asks env\r