wip (not working yet)
authorSimon Huber <hubsim@gmail.com>
Sat, 18 Apr 2015 02:08:53 +0000 (04:08 +0200)
committerSimon Huber <hubsim@gmail.com>
Sat, 18 Apr 2015 02:08:53 +0000 (04:08 +0200)
CTT.hs
Connections.hs
Eval.hs
Exp.cf
Resolver.hs
TypeChecker.hs

diff --git a/CTT.hs b/CTT.hs
index e764036f9b0ad3acb3d2d107d819a8e20e144f59..0661d694fce1fc703f0447c05f0ba6c8b6dad810 100644 (file)
--- a/CTT.hs
+++ b/CTT.hs
@@ -23,13 +23,13 @@ type LIdent = String
 type Tele   = [(Ident,Ter)]
 
 data Label = OLabel LIdent Tele -- Object label
-           | PLabel LIdent Tele Ter Ter -- Path label
+           | PLabel LIdent Tele [Name] (System Ter) -- Path label
   deriving (Eq,Show)
 
 -- OBranch of the form: c x1 .. xn -> e
--- PBranch of the form: c x1 .. xn i -> e
+-- PBranch of the form: c x1 .. xn i1 .. im -> e
 data Branch = OBranch LIdent [Ident] Ter
-            | PBranch LIdent [Ident] Name Ter
+            | PBranch LIdent [Ident] [Name] Ter
   deriving (Eq,Show)
 
 -- Declarations: x : A = e
@@ -60,8 +60,8 @@ labelTeles = map labelTele
 lookupLabel :: LIdent -> [Label] -> Maybe Tele
 lookupLabel x xs = lookup x (labelTeles xs)
 
-lookupPLabel :: LIdent -> [Label] -> Maybe (Tele,Ter,Ter)
-lookupPLabel x xs = listToMaybe [ (ts,t0,t1) | PLabel y ts t0 t1 <- xs, x == y ]
+lookupPLabel :: LIdent -> [Label] -> Maybe (Tele,[Name],System Ter)
+lookupPLabel x xs = listToMaybe [ (ts,is,es) | PLabel y ts is es <- xs, x == y ]
 
 branchName :: Branch -> LIdent
 branchName (OBranch c _ _) = c
@@ -89,7 +89,7 @@ data Ter = App Ter Ter
          | Snd Ter
            -- constructor c Ms
          | Con LIdent [Ter]
-         | PCon LIdent Ter [Ter] Formula -- c A ts phi (A is the data type)
+         | PCon LIdent Ter [Ter] [Formula] -- c A ts phis (A is the data type)
            -- branches c1 xs1  -> M1,..., cn xsn -> Mn
          | Split Ident Loc Ter [Branch]
            -- labelled sum c1 A1s,..., cn Ans (assumes terms are constructors)
@@ -138,8 +138,7 @@ data Val = VU
          | VSigma Val Val
          | VPair Val Val
          | VCon LIdent [Val]
-           -- The Formula is the direction of the equality in VPCon
-         | VPCon LIdent Val [Val] Formula
+         | VPCon LIdent Val [Val] [Formula]
 
            -- Id values
          | VIdP Val Val Val
@@ -237,6 +236,9 @@ upds = foldl Upd
 updsTele :: Env -> Tele -> [Val] -> Env
 updsTele rho tele vs = upds rho (zip (map fst tele) vs)
 
+subs :: Env -> [(Name,Formula)] -> Env
+subs = foldl Sub
+
 mapEnv :: (Val -> Val) -> (Formula -> Formula) -> Env -> Env
 mapEnv f g e = case e of
   Empty         -> Empty
@@ -325,8 +327,9 @@ showTer v = case v of
   Where e d          -> showTer e <+> text "where" <+> showDecls d
   Var x              -> text x
   Con c es           -> text c <+> showTers es
-  PCon c a es phi    -> text c <+> char '{' <+> showTer a <+> char '}' <+>
-                          showTers es <+> showFormula phi
+  PCon c a es phis   -> text c <+> char '{' <+> showTer a <+> char '}'
+                        <+> showTers es
+                        <+> (hsep $ punctuate (char '@') (map showFormula phis))
   Split f _ _ _      -> text f
   Sum _ n _          -> text n
   Undef{}            -> text "undefined"
@@ -372,9 +375,11 @@ showVal v = case v of
   Ter t@Split{} rho -> showTer t <+> showEnv False rho
   Ter t env         -> showTer1 t <+> showEnv True env
   VCon c us         -> text c <+> showVals us
-  VPCon c a us phi  -> text c <+> char '{' <+> showVal a <+> char '}' <+>
-                       showVals us <+> showFormula phi
-  VPi a l@(VLam x t b) | "_" `isPrefixOf` x -> showVal1 a <+> text "->" <+> showVal1 b
+  VPCon c a us phis -> text c <+> char '{' <+> showVal a <+> char '}'
+                       <+> showVals us
+                       <+> (hsep $ punctuate (char '@') (map showFormula phis))
+  VPi a l@(VLam x t b) | "_" `isPrefixOf` x -> showVal1 a <+> text "->"
+                                               <+> showVal1 b
                        | otherwise -> showVal l
   VPi a b           -> text "Pi" <+> showVals [a,b]
   VPair u v         -> parens (showVal u <> comma <> showVal v)
index fe2c10b48e7e41648ab810f5b2fe6fc55a3dac98..ba1234a4fd2250e4e44b9a9aa328e387703fcd84 100644 (file)
@@ -4,7 +4,7 @@ module Connections where
 
 import Control.Applicative
 import Data.List
-import Data.Map (Map,(!))
+import Data.Map (Map,(!),keys)
 import Data.Set (Set)
 import qualified Data.Map as Map
 import qualified Data.Set as Set
@@ -375,9 +375,6 @@ mkSystem = flip insertsSystem Map.empty
 unionSystem :: System a -> System a -> System a
 unionSystem us vs = insertsSystem (Map.assocs us) vs
 
--- could something like that work??
--- transposeSystem :: System [a] -> [System a]
--- transposeSystem as = Map.tranverseWithKey (const . id) as
 
 -- TODO: add some checks
 transposeSystemAndList :: System [a] -> [b] -> [(System a,b)]
@@ -445,3 +442,6 @@ proj us alpha | eps `Map.member` usalpha = usalpha ! eps
   error $ "proj: eps not in " ++ show usalpha ++ "\nwhich  is the "
     ++ show alpha ++ "\nface of " ++ show us
   where usalpha = us `face` alpha
+
+domain :: System a -> [Name]
+domain  = keys . Map.unions . keys
diff --git a/Eval.hs b/Eval.hs
index c2035a06403d877c2a2c6f7e761e454f9d1f78c3..967586575496111180a58bc0328f456ca567c2b6 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -59,7 +59,7 @@ instance Nominal Val where
     VFst u              -> support u
     VSnd u              -> support u
     VCon _ vs           -> support vs
-    VPCon _ a vs phi    -> support (a,vs,phi)
+    VPCon _ a vs phis   -> support (a,vs,phis)
     VVar _ v            -> support v
     VApp u v            -> support (u,v)
     VLam _ u v          -> support (u,v)
@@ -90,7 +90,7 @@ instance Nominal Val where
          VFst u              -> fstVal (acti u)
          VSnd u              -> sndVal (acti u)
          VCon c vs           -> VCon c (acti vs)
-         VPCon c a vs phi    -> pcon c (acti a) (acti vs) (acti phi)
+         VPCon c a vs phis   -> pcon c (acti a) (acti vs) (acti phis)
          VVar x v            -> VVar x (acti v)
          VAppFormula u psi   -> acti u @@ acti psi
          VApp u v            -> app (acti u) (acti v)
@@ -118,7 +118,7 @@ instance Nominal Val where
          VFst u              -> VFst (sw u)
          VSnd u              -> VSnd (sw u)
          VCon c vs           -> VCon c (sw vs)
-         VPCon c a vs phi    -> VPCon c (sw a) (sw vs) (sw phi)
+         VPCon c a vs phis   -> VPCon c (sw a) (sw vs) (sw phis)
          VVar x v            -> VVar x (sw v)
          VAppFormula u psi   -> VAppFormula (sw u) (sw psi)
          VApp u v            -> VApp (sw u) (sw v)
@@ -144,8 +144,8 @@ eval rho v = case v of
   Snd a               -> sndVal (eval rho a)
   Where t decls       -> eval (Def decls rho) t
   Con name ts         -> VCon name (map (eval rho) ts)
-  PCon name a ts phi  ->
-    pcon name (eval rho a) (map (eval rho) ts) (evalFormula rho phi)
+  PCon name a ts phis  ->
+    pcon name (eval rho a) (map (eval rho) ts) (map (evalFormula rho) phis)
   Lam{}               -> Ter v rho
   Split{}             -> Ter v rho
   Sum{}               -> Ter v rho
@@ -190,8 +190,8 @@ app u v = case (u,v) of
   (Ter (Split _ _ _ nvs) e,VCon c vs) -> case lookupBranch c nvs of
     Just (OBranch _ xs t) -> eval (upds e (zip xs vs)) t
     _     -> error $ "app: missing case in split for " ++ c
-  (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
+  (Ter (Split _ _ _ nvs) e,VPCon c _ us phis) -> case lookupBranch c nvs of
+    Just (PBranch _ xs is t) -> eval (subs (upds e (zip xs us)) (zip is phis)) t
     _ -> error $ "app: missing case in split for " ++ c
   (Ter Split{} _,_) | isNeutral v         -> VSplit u v
   (Ter Split{} _,VCompElem _ _ w _)       -> app u w
@@ -267,11 +267,13 @@ v @@ phi | isNeutral v = case (inferType v,toFormula phi) of
 (VElimComp _ _ u) @@ phi   = u @@ phi
 v @@ phi = error $ "(@@): " ++ show v ++ " should be neutral."
 
-pcon :: LIdent -> Val -> [Val] -> Formula -> Val
-pcon c a@(Ter (Sum _ _ lbls) rho) us phi = case lookupPLabel c lbls of
-  Just (tele,t0,t1) | phi == Dir 0 -> eval (updsTele rho tele us) t0
-                    | phi == Dir 1 -> eval (updsTele rho tele us) t1
-                    | otherwise -> VPCon c a us phi
+pcon :: LIdent -> Val -> [Val] -> [Formula] -> Val
+pcon c a@(Ter (Sum _ _ lbls) rho) us phis = case lookupPLabel c lbls of
+  -- TODO: is this correct? Double check!
+  Just (tele,is,ts) | eps `Map.member` vs -> vs ! eps
+                    | otherwise -> VPCon c a us phis
+    where rho' = subs (updsTele rho tele us) (zip is phis)
+          vs   = evalSystem rho' ts
   Nothing           -> error "pcon"
 -- pcon c a us phi     = VPCon c a us phi
 
@@ -303,9 +305,9 @@ trans i v0 v1 = case (v0,v1) of
   (Ter (Sum _ _ nass) env,VCon c us) -> case lookupLabel c nass of
     Just as -> VCon c $ transps i as env us
     Nothing -> error $ "trans: missing constructor " ++ c ++ " in " ++ show v0
-  (Ter (Sum _ _ nass) env,VPCon c _ ws0 phi) -> case lookupLabel c nass of
+  (Ter (Sum _ _ nass) env,VPCon c _ ws0 phis) -> case lookupLabel c nass of
     -- v1 should be independent of i, so i # phi
-    Just as -> VPCon c (v0 `face` (i ~> 1)) (transps i as env ws0) phi
+    Just as -> VPCon c (v0 `face` (i ~> 1)) (transps i as env ws0) phis
     Nothing -> error $ "trans: missing path constructor " ++ c ++
                        " in " ++ show v0
   _ | isNeutral w -> w
@@ -709,19 +711,21 @@ instance Convertible Val where
         let w = mkVar k "X" u
         in conv k u u' && conv (k+1) (app v w) (app v' w)
       (VCon c us,VCon c' us')   -> (c == c') && conv k us us'
-      (VPair u v,VPair u' v') -> conv k u u' && conv k v v'
-      (VPair u v,w)            -> conv k u (fstVal w) && conv k v (sndVal w)
-      (w,VPair u v)            -> conv k (fstVal w) u && conv k (sndVal w) v
-      (VFst u,VFst u')          -> conv k u u'
-      (VSnd u,VSnd u')          -> conv k u u'
-      (VApp u v,VApp u' v')     -> conv k u u' && conv k v v'
-      (VSplit u v,VSplit u' v') -> conv k u u' && conv k v v'
-      (VVar x _, VVar x' _)     -> x == x'
+      (VPCon c v us phis,VPCon c' v' us' phis') ->
+        (c == c') && conv k (v,us,phis) (v',us',phis')
+      (VPair u v,VPair u' v')    -> conv k u u' && conv k v v'
+      (VPair u v,w)              -> conv k u (fstVal w) && conv k v (sndVal w)
+      (w,VPair u v)              -> conv k (fstVal w) u && conv k (sndVal w) v
+      (VFst u,VFst u')           -> conv k u u'
+      (VSnd u,VSnd u')           -> conv k u u'
+      (VApp u v,VApp u' v')      -> conv k u u' && conv k v v'
+      (VSplit u v,VSplit u' v')  -> conv k u u' && conv k v v'
+      (VVar x _, VVar x' _)      -> x == x'
       (VIdP a b c,VIdP a' b' c') -> conv k a a' && conv k b b' && conv k c c'
       (VPath i a,VPath i' a')    -> conv k (a `swap` (i,j)) (a' `swap` (i',j))
       (VPath i a,p')             -> conv k (a `swap` (i,j)) (p' @@ j)
       (p,VPath i' a')            -> conv k (p @@ j) (a' `swap` (i',j))
-      (VTrans p u,VTrans p' u') -> conv k p p' && conv k u u'
+      (VTrans p u,VTrans p' u')  -> conv k p p' && conv k u u'
       (VAppFormula u x,VAppFormula u' x') -> conv k (u,x) (u',x')
       (VComp a u ts,VComp a' u' ts') -> conv k (a,u,ts) (a',u',ts')
       (VGlue v hisos,VGlue v' hisos') -> conv k (v,hisos) (v',hisos')
@@ -794,7 +798,7 @@ instance Normal Val where
     VSigma u v          -> VSigma (normal k u) (normal k v)
     VPair u v           -> VPair (normal k u) (normal k v)
     VCon n us           -> VCon n (normal k us)
-    VPCon n u us phi    -> VPCon n (normal k u) (normal k us) phi
+    VPCon n u us phis   -> VPCon n (normal k u) (normal k us) phis
     VIdP a u0 u1        -> VIdP (normal k a) (normal k u0) (normal k u1)
     VPath i u           -> VPath i (normal k u)
     VComp u v vs        -> compLine (normal k u) (normal k v) (normal k vs)
diff --git a/Exp.cf b/Exp.cf
index b84064e1e663e994e9270a91b6c925e8b9908167..a22f225433e79de67100fbe801542834f3a57097 100644 (file)
--- a/Exp.cf
+++ b/Exp.cf
@@ -67,12 +67,13 @@ coercions Formula 2 ;
 
 -- Branches
 OBranch.   Branch ::= AIdent [AIdent] "->" ExpWhere ;
-PBranch.   Branch ::= AIdent [AIdent] "@" AIdent "->" ExpWhere ;
+-- TODO: better have ... @ i @ j @ k -> ... ?
+PBranch.   Branch ::= AIdent [AIdent] "@" [AIdent] "->" ExpWhere ;
 separator Branch ";" ;
 
 -- Labelled sum alternatives
 OLabel.   Label ::= AIdent [Tele] ;
-PLabel.   Label ::= AIdent [Tele] "@" Exp "~" Exp ;
+PLabel.   Label ::= AIdent [Tele] "<" [AIdent] ">" "@" System ;
 separator Label "|" ;
 
 -- Telescopes
index 8e4e9c7e25d2c9fde6fba03644e0e6dcee21f622..fd6b97e4ddfcc9bf09ca7e73a8f0265bf4040034 100644 (file)
@@ -45,6 +45,14 @@ unApps u         ws = (u, ws)
 appsToIdents :: Exp -> Maybe [Ident]
 appsToIdents = mapM unVar . uncurry (:) . flip unApps []
 
+-- Transform a sequence of applications
+-- (((u v1) .. vn) phi1) .. phim into (u,[v1,..,vn],[phi1,..,phim])
+unAppsFormulas :: Exp -> [Exp] -> [Formula]-> (Exp,[Exp],[Formula])
+unAppsFormulas (AppFormula u phi) ws phis = unAppsFormulas u ws (phi:phis)
+unAppsFormulas u ws phis = (x,xs++ws,phis)
+  where (x,xs) = unApps u ws
+
+
 -- Flatten a tele
 flattenTele :: [Tele] -> [(Ident,Exp)]
 flattenTele tele =
@@ -92,6 +100,9 @@ insertIdents = flip $ foldr insertIdent
 insertName :: AIdent -> Env -> Env
 insertName (AIdent (_,x)) = insertIdent (x,Name)
 
+insertNames :: [AIdent] -> Env -> Env
+insertNames = flip $ foldr insertName
+
 insertVar :: Ident -> Env -> Env
 insertVar x = insertIdent (x,Variable)
 
@@ -186,11 +197,11 @@ resolveExp e = case e of
   Path is e     -> paths is (resolveExp e)
   Hole (HoleIdent (l,_)) -> CTT.Hole <$> getLoc l
   AppFormula e phi ->
-    let (x,xs) = unApps e []
+    let (x,xs,phis) = unAppsFormulas e [] []
     in case x of
       PCon n a ->
         CTT.PCon (unAIdent n) <$> resolveExp a <*> mapM resolveExp xs
-                              <*> resolveFormula phi
+                              <*> mapM resolveFormula phis
       _ -> CTT.AppFormula <$> resolveExp e <*> resolveFormula phi
   Trans x y   -> CTT.Trans <$> resolveExp x <*> resolveExp y
   IdP x y z   -> CTT.IdP <$> resolveExp x <*> resolveExp y <*> resolveExp z
@@ -241,9 +252,10 @@ resolveBranch :: Branch -> Resolver CTT.Branch
 resolveBranch (OBranch (AIdent (_,lbl)) args e) = do
   re <- local (insertAIdents args) $ resolveWhere e
   return $ CTT.OBranch lbl (map unAIdent args) re
-resolveBranch (PBranch (AIdent (_,lbl)) args i e) = do
-  re <- local (insertName i . insertAIdents args) $ resolveWhere e
-  return $ CTT.PBranch lbl (map unAIdent args) (C.Name (unAIdent i)) re
+resolveBranch (PBranch (AIdent (_,lbl)) args is e) = do
+  re    <- local (insertNames is . insertAIdents args) $ resolveWhere e
+  names <- mapM resolveName is
+  return $ CTT.PBranch lbl (map unAIdent args) names re
 
 resolveTele :: [(Ident,Exp)] -> Resolver CTT.Tele
 resolveTele []        = return []
@@ -253,12 +265,13 @@ resolveTele ((i,d):t) =
 resolveLabel :: [(Ident,SymKind)] -> Label -> Resolver CTT.Label
 resolveLabel _ (OLabel n vdecl) =
   CTT.OLabel (unAIdent n) <$> resolveTele (flattenTele vdecl)
-resolveLabel cs (PLabel n vdecl t0 t1) = do
+resolveLabel cs (PLabel n vdecl is sys) = do
   let tele' = flattenTele vdecl
-      ts = map fst tele'
-  CTT.PLabel (unAIdent n) <$> resolveTele tele'
-                          <*> local (insertIdents cs . insertVars ts) (resolveExp t0)
-                          <*> local (insertIdents cs . insertVars ts) (resolveExp t1)
+      ts    = map fst tele'
+      names = map (C.Name . unAIdent) is
+  CTT.PLabel (unAIdent n) <$> resolveTele tele' <*> pure names
+    <*> local (insertNames is . insertIdents cs . insertVars ts)
+              (resolveSystem sys)
 
 -- Resolve Data or Def or Split declarations
 resolveDecl :: Decl -> Resolver (CTT.Decl,[(Ident,SymKind)])
index 89235b5b6bdafa7e2297b2eade467ee7bd858a05..dc5fb86c066b81c23facd7c8fe89982aca7de558 100644 (file)
@@ -68,6 +68,9 @@ addTypeVal (x,a) (TEnv k ind rho v) =
 addSub :: (Name,Formula) -> TEnv -> TEnv\r
 addSub iphi (TEnv k ind rho v) = TEnv k ind (Sub rho iphi) v\r
 \r
+addSubs :: [(Name,Formula)] -> TEnv -> TEnv\r
+addSubs = flip $ foldr addSub\r
+\r
 addType :: (Ident,Ter) -> TEnv -> Typing TEnv\r
 addType (x,a) tenv@(TEnv _ _ rho _) = return $ addTypeVal (x,eval rho a) tenv\r
 \r
@@ -129,7 +132,7 @@ mkSection vb vf vg =
         rho = Upd (Upd (Upd Empty ("b",vb)) ("f",vf)) ("g",vg)\r
 \r
 -- Test if two values are convertible\r
-(===) :: Val -> Val -> Typing Bool\r
+(===) :: Convertible a => a -> a -> Typing Bool\r
 u === v = conv <$> asks index <*> pure u <*> pure v\r
 \r
 -- eval in the typing monad\r
@@ -156,12 +159,20 @@ check a t = case (a,t) of
   (VU,Sigma f)    -> checkFam f\r
   (VU,Sum _ _ bs) -> forM_ bs $ \lbl -> case lbl of\r
     OLabel _ tele -> checkTele tele\r
-    PLabel _ tele t0 t1 -> do\r
+    PLabel _ tele is ts -> do\r
       checkTele tele\r
       rho <- asks env\r
-      localM (addTele tele) $ do\r
-        check (Ter t rho) t0\r
-        check (Ter t rho) t1\r
+      unless (all (`elem` is) (domain ts)) $\r
+        throwError $ "names in path label system" -- TODO\r
+      mapM_ checkFresh is\r
+      let iis = zip is (map Atom is)\r
+      local (addSubs iis) $ localM (addTele tele) $ do\r
+        checkSystemWith ts $ \alpha talpha ->\r
+          local (faceEnv alpha) $ do\r
+            rhoAlpha <- asks env\r
+            check (Ter t rhoAlpha) talpha\r
+        rho' <- asks env\r
+        checkCompSystem (evalSystem rho' ts)\r
   (VPi va@(Ter (Sum _ _ cas) nu) f,Split _ _ ty ces) -> do\r
     check VU ty\r
     rho <- asks env\r
@@ -292,21 +303,21 @@ checkBranch (OLabel _ tele,nu) f (OBranch c ns e) _ _ = do
   k <- asks index\r
   let us = map snd $ mkVars k tele nu\r
   local (addBranch (zip ns us) (tele,nu)) $ check (app f (VCon c us)) e\r
-checkBranch (PLabel _ tele t0 t1,nu) f (PBranch c ns i e) g va = do\r
+checkBranch (PLabel _ tele is ts,nu) f (PBranch c ns js e) g va = do\r
   k <- asks index\r
-  let us  = mkVars k tele nu\r
-      vus = map snd us\r
-      vt0 = eval (upds nu us) t0\r
-      vt1 = eval (upds nu us) t1\r
-  checkFresh i\r
+  mapM_ checkFresh is\r
+  let us   = mkVars k tele nu\r
+      vus  = map snd us\r
+      is'  = map Atom is\r
+      vts  = evalSystem (upds nu us) ts\r
+      vfts = intersectionWith app (border f ts) vts\r
   local (addBranch (zip ns vus) (tele,nu)) $ do\r
-    local (addSub (i,Atom i)) $\r
-      check (app f (VPCon c va vus (Atom i))) e\r
+    local (addSubs (zip is is')) $\r
+      check (app f (VPCon c va vus is')) e\r
     rho <- asks env\r
-    k'  <- asks index\r
-    unless (conv k' (eval (Sub rho (i,Dir 0)) e) (app g vt0) &&\r
-            conv k' (eval (Sub rho (i,Dir 1)) e) (app g vt1)) $\r
-      throwError "Endpoints of branch don't match"\r
+    ve  <- evalTyping e -- TODO: combine with next?\r
+    unlessM (border ve ts === vfts) $\r
+      throwError $ "Faces of branch don't match"\r
 \r
 checkFormula :: Formula -> Typing ()\r
 checkFormula phi = do\r
@@ -428,12 +439,13 @@ infer e = case e of
     let ves = evalSystem rho es\r
     check (compLine VU va ves) u\r
     return va\r
-  PCon c a es phi -> do\r
+  PCon c a es phis -> do\r
     check VU a\r
     va <- evalTyping a\r
-    (bs,nu) <- getLblType c va\r
-    checks (bs,nu) es\r
-    checkFormula phi\r
+--    (bs,nu) <- getLblType c va\r
+--    checks (bs,nu) es\r
+--    mapM_ checkFormula phis\r
+    trace $ "va = " ++ show va\r
     return va\r
   _ -> throwError ("infer " ++ show e)\r
 \r