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

src/GF/Compile/GFCCtoProlog.hs

@@ -69,11 +69,11 @@ plCat :: (CId, [Hypo]) -> String
 plCat (cat, hypos) = plFact "cat" (plTypeWithHypos typ) 
     where ((_,subst), hypos') = alphaConvert emptyEnv hypos
           args = reverse [EVar x | (_,x) <- subst]
-          typ = wildcardUnusedVars $ DTyp hypos' cat args
+          typ = DTyp hypos' cat args
 
 plFun :: (CId, (Type, Int, [Equation])) -> String
 plFun (fun, (typ,_,_)) = plFact "fun" (plp fun : plTypeWithHypos typ')
-    where typ' = wildcardUnusedVars $ snd $ alphaConvert emptyEnv typ
+    where typ' = snd $ alphaConvert emptyEnv typ
 
 plTypeWithHypos :: Type -> [String]
 plTypeWithHypos (DTyp hypos cat args) = [plTerm (plp cat) (map plp args), plp hypos]
@@ -114,7 +114,9 @@ instance PLPrint Type where
         where result = plTerm (plp cat) (map plp args)
 
 instance PLPrint Hypo where
-    plp (Hyp var typ) = plOper ":" (plp var) (plp typ)
+    plp (Hyp      typ) = plOper ":" (plp wildCId) (plp typ)
+    plp (HypI var typ) = plOper ":" (plp var) (plp typ)
+    plp (HypV var typ) = plOper ":" (plp var) (plp typ)
 
 instance PLPrint Expr where
     plp (EVar x)    = plp x
@@ -261,7 +263,12 @@ instance AlphaConvert Type where
               ((ctr,_), args') = alphaConvert env' args
 
 instance AlphaConvert Hypo where
-    alphaConvert env (Hyp x typ) = ((ctr+1,(x,x'):subst), Hyp x' typ')
+    alphaConvert env (Hyp typ) = ((ctr+1,subst), Hyp typ')
+        where ((ctr,subst), typ') = alphaConvert env typ
+    alphaConvert env (HypI x typ) = ((ctr+1,(x,x'):subst), HypI x' typ')
+        where ((ctr,subst), typ') = alphaConvert env typ
+              x' = createLogicalVariable ctr
+    alphaConvert env (HypV x typ) = ((ctr+1,(x,x'):subst), HypV x' typ')
         where ((ctr,subst), typ') = alphaConvert env typ
               x' = createLogicalVariable ctr
 
@@ -281,21 +288,3 @@ instance AlphaConvert Equation where
     alphaConvert env@(_,subst) (Equ patterns result)
         = ((ctr,subst), Equ patterns result')
         where ((ctr,_), result') = alphaConvert env result
-
-----------------------------------------------------------------------
--- translate unused variables to wildcards
-
-wildcardUnusedVars :: Type -> Type
-wildcardUnusedVars typ@(DTyp hypos cat args) = DTyp hypos' cat args
-    where hypos' = [Hyp x' (wildcardUnusedVars typ') | 
-                    Hyp x typ' <- hypos,
-                    let x' = if unusedInType x typ then wildCId else x]
-
-          unusedInType x (DTyp hypos _cat args) 
-              = and [unusedInType x typ | Hyp _ typ <- hypos] &&
-                and [unusedInExpr x exp | exp <- args]
-
-          unusedInExpr x (EAbs y e)  = unusedInExpr x e
-          unusedInExpr x (EApp e e') = unusedInExpr x e && unusedInExpr x e'
-          unusedInExpr x (EVar y)    = x/=y
-          unusedInExpr x expr        = True

src/GF/Compile/GeneratePMCFG.hs

@@ -371,8 +371,9 @@ expandHOAS abs_defs cnc_defs lincats env =
 
     hoCats :: [CId]
     hoCats = sortNub [c | (_,(ty,_,_)) <- abs_defs
-                        , Hyp _ ty <- case ty of {DTyp hyps val _ -> hyps}
+                        , h <- case ty of {DTyp hyps val _ -> hyps}
-                        , c   <- fst (catSkeleton ty)]
+                        , let ty = typeOfHypo h
+                        , c <- fst (catSkeleton ty)]
   
     -- add a range of PMCFG categories for each GF high-order category
     add_hoCat env@(GrammarEnv last_id catSet seqSet funSet crcSet prodSet) (n,cat) =

src/GF/Compile/GrammarToGFCC.hs

@@ -147,7 +147,7 @@ mkPatt p = case p of
 
 
 mkContext :: A.Context -> [C.Hypo]
-mkContext hyps = [C.Hyp (i2i x) (mkType ty) | (x,ty) <- hyps]
+mkContext hyps = [(if x == identW then C.Hyp else C.HypV (i2i x)) (mkType ty) | (x,ty) <- hyps]
 
 mkTerm :: Term -> C.Term
 mkTerm tr = case tr of

src/PGF.hs

@@ -279,7 +279,7 @@ languages pgf = cncnames pgf
 languageCode pgf lang = 
     fmap (replace '_' '-') $ lookConcrFlag pgf lang (mkCId "language")
 
-categories pgf = [DTyp [] c [EMeta i | (Hyp _ _,i) <- zip hs [0..]] | (c,hs) <- Map.toList (cats (abstract pgf))]
+categories pgf = [DTyp [] c (map EMeta [0..length hs]) | (c,hs) <- Map.toList (cats (abstract pgf))]
 
 startCat pgf = DTyp [] (lookStartCat pgf) []
 

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)
+  put (Hyp    t) = putWord8 0 >> put t
-  get = liftM2 Hyp get get
+  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)

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

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
+    Hyp      Type      -- ^ hypothesis without bound variable like in A -> B
-  deriving (Eq,Ord,Show)
+  | 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)
+ppHypo (Hyp    typ) = ppType 1 typ
-  | x == wildCId = ppType 1 typ
+ppHypo (HypV x typ) = PP.parens (PP.text (prCId x) PP.<+> PP.char ':' PP.<+> ppType 0 typ)
-  | otherwise    = 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

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)