PGF.Type.Hypo now can represent explicit and implicit arguments and argument without bound variable

4 files changed, 40 insertions, 14 deletions

diff --git a/src/PGF/Binary.hs b/src/PGF/Binary.hs
index b99296db5..bd896817f 100644
--- a/src/PGF/Binary.hs
+++ b/src/PGF/Binary.hs
@@ -146,8 +146,14 @@ instance Binary Type where
   get = liftM3 DTyp get get get

 

 instance Binary Hypo where

-  put (Hyp v t) = put (v,t)

-  get = liftM2 Hyp get get

+  put (Hyp    t) = putWord8 0 >> put t

+  put (HypV v t) = putWord8 1 >> put (v,t)

+  put (HypI v t) = putWord8 2 >> put (v,t)

+  get = do tag <- getWord8

+           case tag of

+             0 -> liftM  Hyp  get 

+             1 -> liftM2 HypV get get

+             2 -> liftM2 HypI get get

 

 instance Binary FFun where

   put (FFun fun prof lins) = put (fun,prof,lins)

diff --git a/src/PGF/Macros.hs b/src/PGF/Macros.hs
index fe00f4ff7..5d8600090 100644
--- a/src/PGF/Macros.hs
+++ b/src/PGF/Macros.hs
@@ -105,15 +105,20 @@ depth (Fun _ ts) = maximum (0:map depth ts) + 1
 depth _          = 1
 
 cftype :: [CId] -> CId -> Type
-cftype args val = DTyp [Hyp wildCId (cftype [] arg) | arg <- args] val []
+cftype args val = DTyp [Hyp (cftype [] arg) | arg <- args] val []
+
+typeOfHypo :: Hypo -> Type
+typeOfHypo (Hyp    ty) = ty
+typeOfHypo (HypV _ ty) = ty
+typeOfHypo (HypI _ ty) = ty
 
 catSkeleton :: Type -> ([CId],CId)
 catSkeleton ty = case ty of
-  DTyp hyps val _ -> ([valCat ty | Hyp _ ty <- hyps],val)
+  DTyp hyps val _ -> ([valCat (typeOfHypo h) | h <- hyps],val)
 
 typeSkeleton :: Type -> ([(Int,CId)],CId)
 typeSkeleton ty = case ty of
-  DTyp hyps val _ -> ([(contextLength ty, valCat ty) | Hyp _ ty <- hyps],val)
+  DTyp hyps val _ -> ([(contextLength ty, valCat ty) | h <- hyps, let ty = typeOfHypo h],val)
 
 valCat :: Type -> CId
 valCat ty = case ty of
diff --git a/src/PGF/Type.hs b/src/PGF/Type.hs
index 5b77c8085..f8b25202c 100644
--- a/src/PGF/Type.hs
+++ b/src/PGF/Type.hs
@@ -15,9 +15,12 @@ data Type =
    DTyp [Hypo] CId [Expr]

   deriving (Eq,Ord)

 

+-- | 'Hypo' represents a hypothesis in a type i.e. in the type A -> B, A is the hypothesis

 data Hypo =

-   Hyp CId Type

-  deriving (Eq,Ord,Show)

+    Hyp      Type      -- ^ hypothesis without bound variable like in A -> B

+  | HypV CId Type      -- ^ hypothesis with bound variable like in (x : A) -> B x

+  | HypI CId Type      -- ^ hypothesis with bound implicit variable like in {x : A} -> B x

+  deriving (Eq,Ord)

 

 -- | Reads a 'Type' from a 'String'.

 readType :: String -> Maybe Type

@@ -45,7 +48,7 @@ pType = do
   where

     pHypo =

       do (cat,args) <- pAtom

-         return (Hyp wildCId (DTyp [] cat args))

+         return (Hyp (DTyp [] cat args))

       RP.<++

       (RP.between (RP.char '(') (RP.char ')') $ do

          var <- RP.option wildCId $ do

@@ -54,7 +57,16 @@ pType = do
                      RP.string ":"

                      return v

          ty <- pType

-         return (Hyp var ty))

+         return (HypV var ty))

+      RP.<++

+      (RP.between (RP.char '{') (RP.char '}') $ do

+         var <- RP.option wildCId $ do

+                     v <- pCId

+                     RP.skipSpaces

+                     RP.string ":"

+                     return v

+         ty <- pType

+         return (HypI var ty))

 

     pAtom = do

       cat <- pCId

@@ -70,9 +82,9 @@ ppType d (DTyp ctxt cat args)
     ppCtxt hyp doc = ppHypo hyp PP.<+> PP.text "->" PP.<+> doc

     ppRes cat es = PP.text (prCId cat) PP.<+> PP.hsep (map (ppExpr 2) es)

 

-ppHypo (Hyp x typ)

-  | x == wildCId = ppType 1 typ

-  | otherwise    = PP.parens (PP.text (prCId x) PP.<+> PP.char ':' PP.<+> ppType 0 typ)

+ppHypo (Hyp    typ) = ppType 1 typ

+ppHypo (HypV x typ) = PP.parens (PP.text (prCId x) PP.<+> PP.char ':' PP.<+> ppType 0 typ)

+ppHypo (HypI x typ) = PP.braces (PP.text (prCId x) PP.<+> PP.char ':' PP.<+> ppType 0 typ)

 

 ppParens :: Bool -> PP.Doc -> PP.Doc

 ppParens True  = PP.parens

diff --git a/src/PGF/TypeCheck.hs b/src/PGF/TypeCheck.hs
index f2576bb6d..3fba99302 100644
--- a/src/PGF/TypeCheck.hs
+++ b/src/PGF/TypeCheck.hs
@@ -91,7 +91,10 @@ lookupEVar pgf (_,g,_) x = case Map.lookup x g of
 
 type2expr :: Type -> Expr
 type2expr (DTyp hyps cat es) = 
-  foldr (uncurry EPi) (foldl EApp (EVar cat) es) [(x, type2expr t) | Hyp x t <- hyps]
+  foldr (uncurry EPi) (foldl EApp (EVar cat) es) [toPair h | h <- hyps]
+  where
+    toPair (Hyp    t) = (wildCId, type2expr t)
+    toPair (HypV x t) = (x,       type2expr t)
 
 type TCEnv = (Int,Env,Env)
 
@@ -156,7 +159,7 @@ splitConstraints pgf = mkSplit . unifyAll [] . map reduce where
     (VMeta s _, t) -> do
       let tg = substMetas g t
       let sg = maybe e1 id (lookup s g)
-      if (sg == e1) then extend s tg g else unify sg tg g 
+      if null (eqValue (funs (abstract pgf)) 0 sg e1) then extend s tg g else unify sg tg g 
     (t, VMeta _ _) -> unify e2 e1 g
     (VApp c as, VApp d bs) | c == d -> 
        foldM (\ h (a,b) -> unify a b h) g (zip as bs)