diff --git a/src/GF/Compile/GFCCtoProlog.hs b/src/GF/Compile/GFCCtoProlog.hs index 48c3e620d..dca6465fa 100644 --- a/src/GF/Compile/GFCCtoProlog.hs +++ b/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 diff --git a/src/GF/Compile/GeneratePMCFG.hs b/src/GF/Compile/GeneratePMCFG.hs index bb61a0461..8081495f7 100644 --- a/src/GF/Compile/GeneratePMCFG.hs +++ b/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} - , c <- fst (catSkeleton ty)] + , h <- case ty of {DTyp hyps val _ -> hyps} + , 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) = diff --git a/src/GF/Compile/GrammarToGFCC.hs b/src/GF/Compile/GrammarToGFCC.hs index c8bb1c606..d7e46df3e 100644 --- a/src/GF/Compile/GrammarToGFCC.hs +++ b/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 diff --git a/src/PGF.hs b/src/PGF.hs index 5fd98fa25..8ac936e70 100644 --- a/src/PGF.hs +++ b/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) [] 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)