GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-04-09 04:59:31 -06:00
Code Issues Packages Projects Releases Wiki Activity

syntax for implicit arguments in GF

Browse Source
This commit is contained in:
krasimir
2009-09-20 13:47:08 +00:00
parent 7c805b8ff7
commit c2ef7ed35d
20 changed files with 309 additions and 339 deletions
Download Patch File Download Diff File Expand all files Collapse all files

10
src/GF/Compile/AbsCompute.hs
View File

@@ -53,7 +53,7 @@ computeAbsTermIn lookd xs e = errIn (render (text "computing" <+> ppTerm Unquali
_ -> do
let t' = beta vv t
(yy,f,aa) <- termForm t'
let vv' = yy ++ vv
let vv' = map snd yy ++ vv
aa' <- mapM (compt vv') aa
case look f of
Just eqs -> tracd (text "\nmatching" <+> ppTerm Unqualified 0 f) $
@@ -84,10 +84,10 @@ beta vv c = case c of
App f a ->
let (a',f') = (beta vv a, beta vv f) in
case f' of
Abs x b -> beta vv $ substTerm vv [(x,a')] (beta (x:vv) b)
Abs _ x b -> beta vv $ substTerm vv [(x,a')] (beta (x:vv) b)
_ -> (if a'==a && f'==f then id else beta vv) $ App f' a'
Prod x a b -> Prod x (beta vv a) (beta (x:vv) b)
Abs x b -> Abs x (beta (x:vv) b)
Prod b x a t -> Prod b x (beta vv a) (beta (x:vv) t)
Abs b x t -> Abs b x (beta (x:vv) t)
_ -> c
-- special version of pattern matching, to deal with comp under lambda
@@ -133,7 +133,7 @@ tryMatch (p,t) = do
notMeta e = case e of
Meta _ -> False
App f a -> notMeta f && notMeta a
Abs _ b -> notMeta b
Abs _ _ b -> notMeta b
_ -> True
prtm p g =

84
src/GF/Compile/CheckGrammar.hs
View File

@@ -134,11 +134,11 @@ checkAbsInfo st m mo c info = do
Let (x,(_,a)) b -> do
a' <- compAbsTyp g a
compAbsTyp ((x, a'):g) b
Prod x a b -> do
Prod b x a t -> do
a' <- compAbsTyp g a
b' <- compAbsTyp ((x,Vr x):g) b
return $ Prod x a' b'
Abs _ _ -> return t
t' <- compAbsTyp ((x,Vr x):g) t
return $ Prod b x a' t'
Abs _ _ _ -> return t
_ -> composOp (compAbsTyp g) t
checkCompleteGrammar :: SourceGrammar -> SourceModInfo -> SourceModInfo -> Check (BinTree Ident Info)
@@ -170,7 +170,7 @@ checkCompleteGrammar gr abs cnc = do
return info
_ -> return info
case info of
CncCat (Just (RecType [])) _ _ -> return (foldr (\_ -> Abs identW) (R []) cxt)
CncCat (Just (RecType [])) _ _ -> return (foldr (\_ -> Abs Explicit identW) (R []) cxt)
_ -> Bad "no def lin"
case lookupIdent c js of
Ok (CncFun _ (Just _) _ ) -> return js
@@ -224,7 +224,7 @@ checkResInfo gr mo mm c info = do
--- this can only be a partial guarantee, since matching
--- with value type is only possible if expected type is given
checkUniq $
sort [t : map snd xs | (_,x) <- tysts1, Ok (xs,t) <- [typeFormCnc x]]
sort [t : map (\(b,x,t) -> t) xs | (_,x) <- tysts1, Ok (xs,t) <- [typeFormCnc x]]
return (ResOverload os [(y,x) | (x,y) <- tysts'])
ResParam (Just (pcs,_)) -> chIn "parameter type" $ do
@@ -257,7 +257,7 @@ checkCncInfo gr m mo (a,abs) c info = do
typ <- checkErr $ lookupFunType gr a c
cat0 <- checkErr $ valCat typ
(cont,val) <- linTypeOfType gr m typ -- creates arg vars
(trm',_) <- check trm (mkFunType (map snd cont) val) -- erases arg vars
(trm',_) <- check trm (mkFunType (map (\(_,_,ty) -> ty) cont) val) -- erases arg vars
checkPrintname gr mpr
cat <- return $ snd cat0
return (CncFun (Just (cat,(cont,val))) (Just trm') mpr)
@@ -286,7 +286,7 @@ checkCncInfo gr m mo (a,abs) c info = do
computeLType :: SourceGrammar -> Type -> Check Type
computeLType gr t = do
g0 <- checkGetContext
let g = [(x, Vr x) | (x,_) <- g0]
let g = [(b,x, Vr x) | (b,x,_) <- g0]
checkInContext g $ comp t
where
comp ty = case ty of
@@ -303,17 +303,17 @@ computeLType gr t = do
f' <- comp f
a' <- comp a
case f' of
Abs x b -> checkInContext [(x,a')] $ comp b
Abs b x t -> checkInContext [(b,x,a')] $ comp t
_ -> return $ App f' a'
Prod x a b -> do
Prod bt x a b -> do
a' <- comp a
b' <- checkInContext [(x,Vr x)] $ comp b
return $ Prod x a' b'
b' <- checkInContext [(bt,x,Vr x)] $ comp b
return $ Prod bt x a' b'
Abs x b -> do
b' <- checkInContext [(x,Vr x)] $ comp b
return $ Abs x b'
Abs bt x b -> do
b' <- checkInContext [(bt,x,Vr x)] $ comp b
return $ Abs bt x b'
ExtR r s -> do
r' <- comp r
@@ -387,11 +387,11 @@ inferLType gr trm = case trm of
(f',fty) <- infer f
fty' <- comp fty
case fty' of
Prod z arg val -> do
Prod bt z arg val -> do
a' <- justCheck a arg
ty <- if isWildIdent z
then return val
else substituteLType [(z,a')] val
else substituteLType [(bt,z,a')] val
return (App f' a',ty)
_ -> checkError (text "A function type is expected for" <+> ppTerm Unqualified 0 f <+> text "instead of type" <+> ppType env fty)
@@ -502,10 +502,10 @@ inferLType gr trm = case trm of
Sort _ ->
termWith trm $ return typeType
Prod x a b -> do
Prod bt x a b -> do
a' <- justCheck a typeType
b' <- checkInContext [(x,a')] $ justCheck b typeType
return (Prod x a' b', typeType)
b' <- checkInContext [(bt,x,a')] $ justCheck b typeType
return (Prod bt x a' b', typeType)
Table p t -> do
p' <- justCheck p typeType --- check p partype!
@@ -655,7 +655,7 @@ getOverload env@gr mt ot = case appForm ot of
noProds vfs = [(v,f) | (v,f) <- vfs, noProd v]
noProd ty = case ty of
Prod _ _ _ -> False
Prod _ _ _ _ -> False
_ -> True
checkLType :: SourceGrammar -> Term -> Type -> Check (Term, Type)
@@ -665,17 +665,17 @@ checkLType env trm typ0 = do
case trm of
Abs x c -> do
Abs bt x c -> do
case typ of
Prod z a b -> do
checkUpdate (x,a)
Prod bt' z a b -> do
checkUpdate (bt,x,a)
(c',b') <- if isWildIdent z
then check c b
else do
b' <- checkIn (text "abs") $ substituteLType [(z,Vr x)] b
b' <- checkIn (text "abs") $ substituteLType [(bt',z,Vr x)] b
check c b'
checkReset
return $ (Abs x c', Prod x a b')
return $ (Abs bt x c', Prod bt' x a b')
_ -> checkError $ text "function type expected instead of" <+> ppType env typ
App f a -> do
@@ -774,7 +774,7 @@ checkLType env trm typ0 = do
Let (x,(mty,def)) body -> case mty of
Just ty -> do
(def',ty') <- check def ty
checkUpdate (x,ty')
checkUpdate (Explicit,x,ty')
body' <- justCheck body typ
checkReset
return (Let (x,(Just ty',def')) body', typ)
@@ -827,14 +827,14 @@ checkLType env trm typ0 = do
pattContext :: LTEnv -> Type -> Patt -> Check Context
pattContext env typ p = case p of
PV x -> return [(x,typ)]
PV x -> return [(Explicit,x,typ)]
PP q c ps | q /= cPredef -> do ---- why this /=? AR 6/1/2006
t <- checkErr $ lookupResType cnc q c
(cont,v) <- checkErr $ typeFormCnc t
checkCond (text "wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p)
(length cont == length ps)
checkEqLType env typ v (patt2term p)
mapM (uncurry (pattContext env)) (zip (map snd cont) ps) >>= return . concat
mapM (\((_,_,ty),p) -> pattContext env ty p) (zip cont ps) >>= return . concat
PR r -> do
typ' <- computeLType env typ
case typ' of
@@ -849,12 +849,12 @@ pattContext env typ p = case p of
PAs x p -> do
g <- pattContext env typ p
return $ (x,typ):g
return $ (Explicit,x,typ):g
PAlt p' q -> do
g1 <- pattContext env typ p'
g2 <- pattContext env typ q
let pts = nub ([fst pt | pt <- g1, notElem pt g2] ++ [fst pt | pt <- g2, notElem pt g1])
let pts = nub ([x | pt@(_,x,_) <- g1, notElem pt g2] ++ [x | pt@(_,x,_) <- g2, notElem pt g1])
checkCond
(text "incompatible bindings of" <+>
fsep (map ppIdent pts) <+>
@@ -889,7 +889,7 @@ termWith t ct = do
-- | light-weight substitution for dep. types
substituteLType :: Context -> Type -> Check Type
substituteLType g t = case t of
Vr x -> return $ maybe t id $ lookup x g
Vr x -> return $ maybe t id $ lookup x [(x,t) | (_,x,t) <- g]
_ -> composOp (substituteLType g) t
-- | compositional check\/infer of binary operations
@@ -933,7 +933,7 @@ checkIfEqLType env t u trm = do
(_,u) | u == typeError -> True
-- contravariance
(Prod x a b, Prod y c d) -> alpha g c a && alpha ((x,y):g) b d
(Prod _ x a b, Prod _ y c d) -> alpha g c a && alpha ((x,y):g) b d
-- record subtyping
(RecType rs, RecType ts) -> all (\ (l,a) ->
@@ -975,7 +975,7 @@ checkIfEqLType env t u trm = do
_:_ -> Bad $ render (text "missing record fields:" <+> fsep (punctuate comma (map ppLabel others)))
_ -> return locks
-- contravariance
(Prod x a b, Prod y c d) -> do
(Prod _ x a b, Prod _ y c d) -> do
ls1 <- missingLock g c a
ls2 <- missingLock g b d
return $ ls1 ++ ls2
@@ -989,11 +989,11 @@ checkIfEqLType env t u trm = do
ppType :: LTEnv -> Type -> Doc
ppType env ty =
case ty of
RecType fs -> case filter isLockLabel $ map fst fs of
[lock] -> text (drop 5 (showIdent (label2ident lock)))
_ -> ppTerm Unqualified 0 ty
Prod x a b -> ppType env a <+> text "->" <+> ppType env b
_ -> ppTerm Unqualified 0 ty
RecType fs -> case filter isLockLabel $ map fst fs of
[lock] -> text (drop 5 (showIdent (label2ident lock)))
_ -> ppTerm Unqualified 0 ty
Prod _ x a b -> ppType env a <+> text "->" <+> ppType env b
_ -> ppTerm Unqualified 0 ty
-- | linearization types and defaults
linTypeOfType :: SourceGrammar -> Ident -> Type -> Check (Context,Type)
@@ -1013,7 +1013,7 @@ linTypeOfType cnc m typ = do
text "with" $$
nest 2 (ppTerm Unqualified 0 val))) $
plusRecType vars val
return (symb,rec)
return (Explicit,symb,rec)
lookLin (_,c) = checks [ --- rather: update with defLinType ?
checkErr (lookupLincat cnc m c) >>= computeLType cnc
,return defLinType
@@ -1036,11 +1036,11 @@ allDependencies ism b =
opty _ = []
pts i = case i of
ResOper pty pt -> [pty,pt]
ResParam (Just (ps,_)) -> [Just t | (_,cont) <- ps, (_,t) <- cont]
ResParam (Just (ps,_)) -> [Just t | (_,cont) <- ps, (_,_,t) <- cont]
CncCat pty _ _ -> [pty]
CncFun _ pt _ -> [pt] ---- (Maybe (Ident,(Context,Type))
AbsFun pty _ ptr -> [pty] --- ptr is def, which can be mutual
AbsCat (Just co) _ -> [Just ty | (_,ty) <- co]
AbsCat (Just co) _ -> [Just ty | (_,_,ty) <- co]
_ -> []
topoSortOpers :: [(Ident,[Ident])] -> Err [Ident]

20
src/GF/Compile/Compute.hs
View File

@@ -62,22 +62,22 @@ computeTermOpt rec gr = comput True where
_ -> comp g t'
-- Abs x@(IA _) b -> do
Abs x b | full -> do
Abs _ _ _ | full -> do
let (xs,b1) = termFormCnc t
b' <- comp ([(x,Vr x) | x <- xs] ++ g) b1
b' <- comp ([(x,Vr x) | (_,x) <- xs] ++ g) b1
return $ mkAbs xs b'
-- b' <- comp (ext x (Vr x) g) b
-- return $ Abs x b'
Abs _ _ -> return t -- hnf
Abs _ _ _ -> return t -- hnf
Let (x,(_,a)) b -> do
a' <- comp g a
comp (ext x a' g) b
Prod x a b -> do
Prod b x a t -> do
a' <- comp g a
b' <- comp (ext x (Vr x) g) b
return $ Prod x a' b'
t' <- comp (ext x (Vr x) g) t
return $ Prod b x a' t'
-- beta-convert
App f a -> case appForm t of
@@ -92,9 +92,9 @@ computeTermOpt rec gr = comput True where
(t',b) <- appPredefined (mkApp h' as')
if b then return t' else comp g t'
Abs _ _ -> do
Abs _ _ _ -> do
let (xs,b) = termFormCnc h'
let g' = (zip xs as') ++ g
let g' = (zip (map snd xs) as') ++ g
let as2 = drop (length xs) as'
let xs2 = drop (length as') xs
b' <- comp g' (mkAbs xs2 b)
@@ -234,11 +234,11 @@ computeTermOpt rec gr = comput True where
f' <- hnf g f
a' <- comp g a
case (f',a') of
(Abs x b, FV as) ->
(Abs _ x b, FV as) ->
mapM (\c -> comp (ext x c g) b) as >>= return . variants
(_, FV as) -> mapM (\c -> comp g (App f' c)) as >>= return . variants
(FV fs, _) -> mapM (\c -> comp g (App c a')) fs >>= return . variants
(Abs x b,_) -> comp (ext x a' g) b
(Abs _ x b,_) -> comp (ext x a' g) b
(QC _ _,_) -> returnC $ App f' a'

24
src/GF/Compile/GrammarToGFCC.hs
View File

@@ -119,6 +119,10 @@ canon2gfcc opts pars cgr@(M.MGrammar ((a,abm):cms)) =
i2i :: Ident -> CId
i2i = CId . ident2bs
b2b :: A.BindType -> C.BindType
b2b A.Explicit = C.Explicit
b2b A.Implicit = C.Implicit
mkType :: [Ident] -> A.Type -> C.Type
mkType scope t =
case GM.typeForm t of
@@ -127,9 +131,9 @@ mkType scope t =
mkExp :: [Ident] -> A.Term -> C.Expr
mkExp scope t = case GM.termForm t of
Ok (xs,c,args) -> mkAbs xs (mkApp (reverse xs++scope) c (map (mkExp scope) args))
Ok (xs,c,args) -> mkAbs xs (mkApp (map snd (reverse xs)++scope) c (map (mkExp scope) args))
where
mkAbs xs t = foldr (C.EAbs C.Explicit . i2i) t xs
mkAbs xs t = foldr (\(b,v) -> C.EAbs (b2b b) (i2i v)) t xs
mkApp scope c args = case c of
Q _ c -> foldl C.EApp (C.EFun (i2i c)) args
QC _ c -> foldl C.EApp (C.EFun (i2i c)) args
@@ -154,10 +158,10 @@ mkPatt scope p =
mkContext :: [Ident] -> A.Context -> ([Ident],[C.Hypo])
mkContext scope hyps = mapAccumL (\scope (x,ty) -> let ty' = mkType scope ty
in if x == identW
then ( scope,(C.Explicit,i2i x,ty'))
else (x:scope,(C.Explicit,i2i x,ty'))) scope hyps
mkContext scope hyps = mapAccumL (\scope (bt,x,ty) -> let ty' = mkType scope ty
in if x == identW
then ( scope,(b2b bt,i2i x,ty'))
else (x:scope,(b2b bt,i2i x,ty'))) scope hyps
mkTerm :: Term -> C.Term
mkTerm tr = case tr of
@@ -179,7 +183,7 @@ mkTerm tr = case tr of
----- K (KP ss _) -> C.K (C.KP ss []) ---- TODO: prefix variants
Empty -> C.S []
App _ _ -> prtTrace tr $ C.C 66661 ---- for debugging
Abs _ t -> mkTerm t ---- only on toplevel
Abs _ _ t -> mkTerm t ---- only on toplevel
Alts (td,tvs) ->
C.K (C.KP (strings td) [C.Alt (strings u) (strings v) | (u,v) <- tvs])
_ -> prtTrace tr $ C.S [C.K (C.KS (render (A.ppTerm Unqualified 0 tr <+> int 66662)))] ---- for debugging
@@ -309,9 +313,9 @@ canon2canon opts abs cg0 =
ResParam (Just (ps,v)) ->
ResParam (Just ([(c,concatMap unRec cont) | (c,cont) <- ps],Nothing))
_ -> j
unRec (x,ty) = case ty of
RecType fs -> [ity | (_,typ) <- fs, ity <- unRec (identW,typ)]
_ -> [(x,ty)]
unRec (bt,x,ty) = case ty of
RecType fs -> [ity | (_,typ) <- fs, ity <- unRec (Explicit,identW,typ)]
_ -> [(bt,x,ty)]
----
trs v = traceD (render (tr v)) v

14
src/GF/Compile/Optimize.hs
View File

@@ -117,9 +117,9 @@ evalCncInfo opts gr cnc abs (c,info) = do
CncCat ptyp pde ppr -> do
pde' <- case (ptyp,pde) of
(Just typ, Just de) ->
liftM Just $ pEval ([(varStr, typeStr)], typ) de
liftM Just $ pEval ([(Explicit, varStr, typeStr)], typ) de
(Just typ, Nothing) ->
liftM Just $ mkLinDefault gr typ >>= partEval noOptions gr ([(varStr, typeStr)],typ)
liftM Just $ mkLinDefault gr typ >>= partEval noOptions gr ([(Explicit, varStr, typeStr)],typ)
_ -> return pde -- indirection
ppr' <- liftM Just $ evalPrintname gr c ppr (Just $ K $ showIdent c)
@@ -142,7 +142,7 @@ evalCncInfo opts gr cnc abs (c,info) = do
-- | the main function for compiling linearizations
partEval :: Options -> SourceGrammar -> (Context,Type) -> Term -> Err Term
partEval opts gr (context, val) trm = errIn (render (text "parteval" <+> ppTerm Qualified 0 trm)) $ do
let vars = map fst context
let vars = map (\(bt,x,t) -> x) context
args = map Vr vars
subst = [(v, Vr v) | v <- vars]
trm1 = mkApp trm args
@@ -150,7 +150,7 @@ partEval opts gr (context, val) trm = errIn (render (text "parteval" <+> ppTerm
trm3 <- if rightType trm2
then computeTerm gr subst trm2
else recordExpand val trm2 >>= computeTerm gr subst
return $ mkAbs vars trm3
return $ mkAbs [(Explicit,v) | v <- vars] trm3
where
-- don't eta expand records of right length (correct by type checking)
rightType (R rs) = case val of
@@ -178,8 +178,8 @@ recordExpand typ trm = case typ of
mkLinDefault :: SourceGrammar -> Type -> Err Term
mkLinDefault gr typ = do
case typ of
RecType lts -> mapPairsM mkDefField lts >>= (return . Abs varStr . R . mkAssign)
_ -> liftM (Abs varStr) $ mkDefField typ
RecType lts -> mapPairsM mkDefField lts >>= (return . Abs Explicit varStr . R . mkAssign)
_ -> liftM (Abs Explicit varStr) $ mkDefField typ
---- _ -> prtBad "linearization type must be a record type, not" typ
where
mkDefField typ = case typ of
@@ -211,7 +211,7 @@ evalPrintname gr c ppr lin =
comp = computeConcrete gr
oneBranch t = case t of
Abs _ b -> oneBranch b
Abs _ _ b -> oneBranch b
R (r:_) -> oneBranch $ snd $ snd r
T _ (c:_) -> oneBranch $ snd c
V _ (c:_) -> oneBranch c

8
src/GF/Compile/Refresh.hs
View File

@@ -37,13 +37,13 @@ refresh :: Term -> STM IdState Term
refresh e = case e of
Vr x -> liftM Vr (lookVar x)
Abs x b -> liftM2 Abs (refVarPlus x) (refresh b)
Abs b x t -> liftM2 (Abs b) (refVarPlus x) (refresh t)
Prod x a b -> do
Prod b x a t -> do
a' <- refresh a
x' <- refVar x
b' <- refresh b
return $ Prod x' a' b'
t' <- refresh t
return $ Prod b x' a' t'
Let (x,(mt,a)) b -> do
a' <- refresh a

10
src/GF/Compile/Rename.hs
View File

@@ -178,8 +178,8 @@ renPerh ren Nothing = return Nothing
renameTerm :: Status -> [Ident] -> Term -> Err Term
renameTerm env vars = ren vars where
ren vs trm = case trm of
Abs x b -> liftM (Abs x) (ren (x:vs) b)
Prod x a b -> liftM2 (Prod x) (ren vs a) (ren (x:vs) b)
Abs b x t -> liftM (Abs b x) (ren (x:vs) t)
Prod bt x a b -> liftM2 (Prod bt x) (ren vs a) (ren (x:vs) b)
Typed a b -> liftM2 Typed (ren vs a) (ren vs b)
Vr x
| elem x vs -> return trm
@@ -301,16 +301,16 @@ renameParam env (c,co) = do
renameContext :: Status -> Context -> Err Context
renameContext b = renc [] where
renc vs cont = case cont of
(x,t) : xts
(bt,x,t) : xts
| isWildIdent x -> do
t' <- ren vs t
xts' <- renc vs xts
return $ (x,t') : xts'
return $ (bt,x,t') : xts'
| otherwise -> do
t' <- ren vs t
let vs' = x:vs
xts' <- renc vs' xts
return $ (x,t') : xts'
return $ (bt,x,t') : xts'
_ -> return cont
ren = renameTerm b

18
src/GF/Compile/TC.hs
View File

@@ -77,7 +77,7 @@ whnf v = ---- errIn ("whnf" +++ prt v) $ ---- debug
app :: Val -> Val -> Err Val
app u v = case u of
VClos env (Abs x e) -> eval ((x,v):env) e
VClos env (Abs _ x e) -> eval ((x,v):env) e
_ -> return $ VApp u v
eval :: Env -> Exp -> Err Val
@@ -100,9 +100,9 @@ eqVal k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2) $
let v = VGen k
case (w1,w2) of
(VApp f1 a1, VApp f2 a2) -> liftM2 (++) (eqVal k f1 f2) (eqVal k a1 a2)
(VClos env1 (Abs x1 e1), VClos env2 (Abs x2 e2)) ->
(VClos env1 (Abs _ x1 e1), VClos env2 (Abs _ x2 e2)) ->
eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2)
(VClos env1 (Prod x1 a1 e1), VClos env2 (Prod x2 a2 e2)) ->
(VClos env1 (Prod _ x1 a1 e1), VClos env2 (Prod _ x2 a2 e2)) ->
liftM2 (++)
(eqVal k (VClos env1 a1) (VClos env2 a2))
(eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2))
@@ -123,15 +123,15 @@ checkExp th tenv@(k,rho,gamma) e ty = do
case e of
Meta m -> return $ (AMeta m typ,[])
Abs x t -> case typ of
VClos env (Prod y a b) -> do
Abs _ x t -> case typ of
VClos env (Prod _ y a b) -> do
a' <- whnf $ VClos env a ---
(t',cs) <- checkExp th
(k+1,(x,v x):rho, (x,a'):gamma) t (VClos ((y,v x):env) b)
return (AAbs x a' t', cs)
_ -> Bad (render (text "function type expected for" <+> ppTerm Unqualified 0 e <+> text "instead of" <+> ppValue Unqualified 0 typ))
Prod x a b -> do
Prod _ x a b -> do
testErr (typ == vType) "expected Type"
(a',csa) <- checkType th tenv a
(b',csb) <- checkType th (k+1, (x,v x):rho, (x,VClos rho a):gamma) b
@@ -176,7 +176,7 @@ inferExp th tenv@(k,rho,gamma) e = case e of
(f',w,csf) <- inferExp th tenv f
typ <- whnf w
case typ of
VClos env (Prod x a b) -> do
VClos env (Prod _ x a b) -> do
(a',csa) <- checkExp th tenv t (VClos env a)
b' <- whnf $ VClos ((x,VClos rho t):env) b
return $ (AApp f' a' b', b', csf ++ csa)
@@ -217,7 +217,7 @@ checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
p:ps2 -> do
typ <- whnf ty
case typ of
VClos env (Prod y a b) -> do
VClos env (Prod _ y a b) -> do
a' <- whnf $ VClos env a
(p', sigma, binds, cs1) <- checkP tenv p y a'
let tenv' = (length binds, sigma ++ rho, binds ++ gamma)
@@ -275,7 +275,7 @@ checkPatt th tenv exp val = do
(f',w,csf) <- checkExpP tenv f val
typ <- whnf w
case typ of
VClos env (Prod x a b) -> do
VClos env (Prod _ x a b) -> do
(a',_,csa) <- checkExpP tenv t (VClos env a)
b' <- whnf $ VClos ((x,VClos rho t):env) b
return $ (AApp f' a' b', b', csf ++ csa)

6
src/GF/Grammar/AppPredefined.hs
View File

@@ -50,11 +50,11 @@ typPredefined f
| f == cPlus = return $ mkFunType [typeInt,typeInt] (typeInt)
---- "read" -> (P : Type) -> Tok -> P
| f == cShow = return $ mkProd -- (P : PType) -> P -> Tok
([(varP,typePType),(identW,Vr varP)],typeStr,[])
([(Explicit,varP,typePType),(Explicit,identW,Vr varP)],typeStr,[])
| f == cToStr = return $ mkProd -- (L : Type) -> L -> Str
([(varL,typeType),(identW,Vr varL)],typeStr,[])
([(Explicit,varL,typeType),(Explicit,identW,Vr varL)],typeStr,[])
| f == cMapStr = return $ mkProd -- (L : Type) -> (Str -> Str) -> L -> L
([(varL,typeType),(identW,mkFunType [typeStr] typeStr),(identW,Vr varL)],Vr varL,[])
([(Explicit,varL,typeType),(Explicit,identW,mkFunType [typeStr] typeStr),(Explicit,identW,Vr varL)],Vr varL,[])
| f == cTake = return $ mkFunType [typeInt,typeTok] typeTok
| f == cTk = return $ mkFunType [typeInt,typeTok] typeTok
| otherwise = Bad (render (text "unknown in Predef:" <+> ppIdent f))

17
src/GF/Grammar/Binary.hs
View File

@@ -109,6 +109,15 @@ instance Binary Info where
8 -> get >>= \(x,y) -> return (AnyInd x y)
_ -> decodingError
instance Binary BindType where
put Explicit = putWord8 0
put Implicit = putWord8 1
get = do tag <- getWord8
case tag of
0 -> return Explicit
1 -> return Implicit
_ -> decodingError
instance Binary Term where
put (Vr x) = putWord8 0 >> put x
put (Cn x) = putWord8 1 >> put x
@@ -119,9 +128,9 @@ instance Binary Term where
put (K x) = putWord8 7 >> put x
put (Empty) = putWord8 8
put (App x y) = putWord8 9 >> put (x,y)
put (Abs x y) = putWord8 10 >> put (x,y)
put (Abs x y z) = putWord8 10 >> put (x,y,z)
put (Meta x) = putWord8 11 >> put x
put (Prod x y z) = putWord8 12 >> put (x,y,z)
put (Prod w x y z)= putWord8 12 >> put (w,x,y,z)
put (Typed x y) = putWord8 14 >> put (x,y)
put (Example x y) = putWord8 15 >> put (x,y)
put (RecType x) = putWord8 16 >> put x
@@ -159,9 +168,9 @@ instance Binary Term where
7 -> get >>= \x -> return (K x)
8 -> return (Empty)
9 -> get >>= \(x,y) -> return (App x y)
10 -> get >>= \(x,y) -> return (Abs x y)
10 -> get >>= \(x,y,z) -> return (Abs x y z)
11 -> get >>= \x -> return (Meta x)
12 -> get >>= \(x,y,z) -> return (Prod x y z)
12 -> get >>= \(w,x,y,z)->return (Prod w x y z)
14 -> get >>= \(x,y) -> return (Typed x y)
15 -> get >>= \(x,y) -> return (Example x y)
16 -> get >>= \x -> return (RecType x)

4
src/GF/Grammar/CF.hs
View File

@@ -112,8 +112,8 @@ cf2rule (fun, (cat, items)) = (def,ldef) where
f = identS fun
def = (f, AbsFun (Just (mkProd (args', Cn (identS cat), []))) Nothing Nothing)
args0 = zip (map (identS . ("x" ++) . show) [0..]) items
args = [(v, Cn (identS c)) | (v, Left c) <- args0]
args' = [(identS "_", Cn (identS c)) | (_, Left c) <- args0]
args = [((Explicit,v), Cn (identS c)) | (v, Left c) <- args0]
args' = [(Explicit,identS "_", Cn (identS c)) | (_, Left c) <- args0]
ldef = (f, CncFun
Nothing
(Just (mkAbs (map fst args)

144
src/GF/Grammar/Grammar.hs
View File

@@ -15,35 +15,36 @@
-----------------------------------------------------------------------------
module GF.Grammar.Grammar (SourceGrammar,
emptySourceGrammar,
SourceModInfo,
SourceModule,
mapSourceModule,
Info(..),
PValues,
Type,
Cat,
Fun,
QIdent,
Term(..),
Patt(..),
TInfo(..),
Label(..),
MetaId,
Hypo,
Context,
Equation,
Labelling,
Assign,
Case,
Cases,
LocalDef,
Param,
Altern,
Substitution,
varLabel, tupleLabel, linLabel, theLinLabel,
ident2label, label2ident
) where
emptySourceGrammar,
SourceModInfo,
SourceModule,
mapSourceModule,
Info(..),
PValues,
Type,
Cat,
Fun,
QIdent,
BindType(..),
Term(..),
Patt(..),
TInfo(..),
Label(..),
MetaId,
Hypo,
Context,
Equation,
Labelling,
Assign,
Case,
Cases,
LocalDef,
Param,
Altern,
Substitution,
varLabel, tupleLabel, linLabel, theLinLabel,
ident2label, label2ident
) where
import GF.Infra.Ident
import GF.Infra.Option ---
@@ -103,57 +104,62 @@ type Fun = QIdent
type QIdent = (Ident,Ident)
data Term =
Vr Ident -- ^ variable
| Cn Ident -- ^ constant
| Con Ident -- ^ constructor
| Sort Ident -- ^ basic type
| EInt Integer -- ^ integer literal
| EFloat Double -- ^ floating point literal
| K String -- ^ string literal or token: @\"foo\"@
| Empty -- ^ the empty string @[]@
data BindType =
Explicit
| Implicit
deriving (Eq,Ord,Show)
| App Term Term -- ^ application: @f a@
| Abs Ident Term -- ^ abstraction: @\x -> b@
data Term =
Vr Ident -- ^ variable
| Cn Ident -- ^ constant
| Con Ident -- ^ constructor
| Sort Ident -- ^ basic type
| EInt Integer -- ^ integer literal
| EFloat Double -- ^ floating point literal
| K String -- ^ string literal or token: @\"foo\"@
| Empty -- ^ the empty string @[]@
| App Term Term -- ^ application: @f a@
| Abs BindType Ident Term -- ^ abstraction: @\x -> b@
| Meta {-# UNPACK #-} !MetaId -- ^ metavariable: @?i@ (only parsable: ? = ?0)
| Prod Ident Term Term -- ^ function type: @(x : A) -> B@
| Typed Term Term -- ^ type-annotated term
| Prod BindType Ident Term Term -- ^ function type: @(x : A) -> B@, @A -> B@, @({x} : A) -> B@
| Typed Term Term -- ^ type-annotated term
--
-- /below this, the constructors are only for concrete syntax/
| Example Term String -- ^ example-based term: @in M.C "foo"
| RecType [Labelling] -- ^ record type: @{ p : A ; ...}@
| R [Assign] -- ^ record: @{ p = a ; ...}@
| P Term Label -- ^ projection: @r.p@
| PI Term Label Int -- ^ index-annotated projection
| ExtR Term Term -- ^ extension: @R ** {x : A}@ (both types and terms)
| Example Term String -- ^ example-based term: @in M.C "foo"
| RecType [Labelling] -- ^ record type: @{ p : A ; ...}@
| R [Assign] -- ^ record: @{ p = a ; ...}@
| P Term Label -- ^ projection: @r.p@
| PI Term Label Int -- ^ index-annotated projection
| ExtR Term Term -- ^ extension: @R ** {x : A}@ (both types and terms)
| Table Term Term -- ^ table type: @P => A@
| T TInfo [Case] -- ^ table: @table {p => c ; ...}@
| TSh TInfo [Cases] -- ^ table with disjunctive patters (only back end opt)
| V Type [Term] -- ^ table given as course of values: @table T [c1 ; ... ; cn]@
| S Term Term -- ^ selection: @t ! p@
| Val Term Type Int -- ^ parameter value number: @T # i#
| Table Term Term -- ^ table type: @P => A@
| T TInfo [Case] -- ^ table: @table {p => c ; ...}@
| TSh TInfo [Cases] -- ^ table with disjunctive patters (only back end opt)
| V Type [Term] -- ^ table given as course of values: @table T [c1 ; ... ; cn]@
| S Term Term -- ^ selection: @t ! p@
| Val Term Type Int -- ^ parameter value number: @T # i#
| Let LocalDef Term -- ^ local definition: @let {t : T = a} in b@
| Let LocalDef Term -- ^ local definition: @let {t : T = a} in b@
| Alias Ident Type Term -- ^ constant and its definition, used in inlining
| Alias Ident Type Term -- ^ constant and its definition, used in inlining
| Q Ident Ident -- ^ qualified constant from a package
| QC Ident Ident -- ^ qualified constructor from a package
| Q Ident Ident -- ^ qualified constant from a package
| QC Ident Ident -- ^ qualified constructor from a package
| C Term Term -- ^ concatenation: @s ++ t@
| Glue Term Term -- ^ agglutination: @s + t@
| C Term Term -- ^ concatenation: @s ++ t@
| Glue Term Term -- ^ agglutination: @s + t@
| EPatt Patt -- ^ pattern (in macro definition): # p
| EPattType Term -- ^ pattern type: pattern T
| EPatt Patt -- ^ pattern (in macro definition): # p
| EPattType Term -- ^ pattern type: pattern T
| ELincat Ident Term -- ^ boxed linearization type of Ident
| ELin Ident Term -- ^ boxed linearization of type Ident
| ELincat Ident Term -- ^ boxed linearization type of Ident
| ELin Ident Term -- ^ boxed linearization of type Ident
| FV [Term] -- ^ alternatives in free variation: @variants { s ; ... }@
| FV [Term] -- ^ alternatives in free variation: @variants { s ; ... }@
| Alts (Term, [(Term, Term)]) -- ^ alternatives by prefix: @pre {t ; s\/c ; ...}@
| Strs [Term] -- ^ conditioning prefix strings: @strs {s ; ...}@
| Alts (Term, [(Term, Term)]) -- ^ alternatives by prefix: @pre {t ; s\/c ; ...}@
| Strs [Term] -- ^ conditioning prefix strings: @strs {s ; ...}@
deriving (Show, Eq, Ord)
@@ -200,8 +206,8 @@ data Label =
type MetaId = Int
type Hypo = (Ident,Term) -- (x:A) (_:A) A
type Context = [Hypo] -- (x:A)(y:B) (x,y:A) (_,_:A)
type Hypo = (BindType,Ident,Term) -- (x:A) (_:A) A ({x}:A)
type Context = [Hypo] -- (x:A)(y:B) (x,y:A) (_,_:A)
type Equation = ([Patt],Term)
type Labelling = (Label, Term)

4
src/GF/Grammar/Lookup.hs
View File

@@ -137,7 +137,7 @@ lookupOverload gr m c = do
case info of
ResOverload os tysts -> do
tss <- mapM (\x -> lookupOverload gr x c) os
return $ [(map snd args,(val,tr)) |
return $ [(map (\(b,x,t) -> t) args,(val,tr)) |
(ty,tr) <- tysts, Ok (args,val) <- [typeFormCnc ty]] ++
concat tss
@@ -173,7 +173,7 @@ lookupParamValues gr m c = do
_ -> liftM concat $ mapM mkPar ps
where
mkPar (f,co) = do
vs <- liftM combinations $ mapM (\ (_,ty) -> allParamValues gr ty) co
vs <- liftM combinations $ mapM (\(_,_,ty) -> allParamValues gr ty) co
return $ map (mkApp (QC m f)) vs
lookupFirstTag :: SourceGrammar -> Ident -> Ident -> Err Term

70
src/GF/Grammar/MMacros.hs
View File

@@ -143,10 +143,10 @@ substTerm :: [Ident] -> Substitution -> Term -> Term
substTerm ss g c = case c of
Vr x -> maybe c id $ lookup x g
App f a -> App (substTerm ss g f) (substTerm ss g a)
Abs x b -> let y = mkFreshVarX ss x in
Abs y (substTerm (y:ss) ((x, Vr y):g) b)
Prod x a b -> let y = mkFreshVarX ss x in
Prod y (substTerm ss g a) (substTerm (y:ss) ((x,Vr y):g) b)
Abs b x t -> let y = mkFreshVarX ss x in
Abs b y (substTerm (y:ss) ((x, Vr y):g) t)
Prod b x a t -> let y = mkFreshVarX ss x in
Prod b y (substTerm ss g a) (substTerm (y:ss) ((x,Vr y):g) t)
_ -> c
metaSubstExp :: MetaSubst -> [(MetaId,Exp)]
@@ -204,64 +204,16 @@ mkProdVal :: Binds -> Val -> Err Val ---
mkProdVal bs v = do
bs' <- mapPairsM val2exp bs
v' <- val2exp v
return $ vClos $ foldr (uncurry Prod) v' bs'
return $ vClos $ foldr (uncurry (Prod Explicit)) v' bs'
freeVarsExp :: Exp -> [Ident]
freeVarsExp e = case e of
Vr x -> [x]
App f c -> freeVarsExp f ++ freeVarsExp c
Abs x b -> filter (/=x) (freeVarsExp b)
Prod x a b -> freeVarsExp a ++ filter (/=x) (freeVarsExp b)
Abs _ x b -> filter (/=x) (freeVarsExp b)
Prod _ x a b -> freeVarsExp a ++ filter (/=x) (freeVarsExp b)
_ -> [] --- thus applies to abstract syntax only
ident2string :: Ident -> String
ident2string = showIdent
{-
tree :: (TrNode,[Tree]) -> Tree
tree = Tr
eqCat :: Cat -> Cat -> Bool
eqCat = (==)
addBinds :: Binds -> Tree -> Tree
addBinds b (Tr (N (b0,at,t,c,x),ts)) = Tr (N (b ++ b0,at,t,c,x),ts)
bodyTree :: Tree -> Tree
bodyTree (Tr (N (_,a,t,c,x),ts)) = Tr (N ([],a,t,c,x),ts)
-}
ref2exp :: [Var] -> Type -> Ref -> Err Exp
ref2exp bounds typ ref = do
cont <- contextOfType typ
xx0 <- mapM (typeSkeleton . snd) cont
let (xxs,cs) = unzip [(length hs, c) | (hs,c) <- xx0]
args = [mkAbs xs mExp | i <- xxs, let xs = mkFreshVars i bounds]
return $ mkApp ref args
-- no refreshment of metas
-- | invariant: only 'Con' or 'Var'
type Ref = Exp
fun2wrap :: [Var] -> ((Fun,Int),Type) -> Exp -> Err Exp
fun2wrap oldvars ((fun,i),typ) exp = do
cont <- contextOfType typ
args <- mapM mkArg (zip [0..] (map snd cont))
return $ mkApp (qq fun) args
where
mkArg (n,c) = do
cont <- contextOfType c
let vars = mkFreshVars (length cont) oldvars
return $ mkAbs vars $ if n==i then exp else mExp
-- | weak heuristics: sameness of value category
compatType :: Val -> Type -> Bool
compatType v t = errVal True $ do
cat1 <- val2cat v
cat2 <- valCat t
return $ cat1 == cat2
---
mkJustProd :: Context -> Term -> Term
mkJustProd cont typ = mkProd (cont,typ,[])
@@ -283,8 +235,8 @@ identVar _ = Bad "not a variable"
qualifTerm :: Ident -> Term -> Term
qualifTerm m = qualif [] where
qualif xs t = case t of
Abs x b -> let x' = chV x in Abs x' $ qualif (x':xs) b
Prod x a b -> Prod x (qualif xs a) $ qualif (x:xs) b
Abs b x t -> let x' = chV x in Abs b x' $ qualif (x':xs) t
Prod b x a t -> Prod b x (qualif xs a) $ qualif (x:xs) t
Vr x -> let x' = chV x in if (elem x' xs) then (Vr x') else (Q m x)
Cn c -> Q m c
Con c -> QC m c
@@ -300,8 +252,8 @@ string2var s = case BS.unpack s of
reindexTerm :: Term -> Term
reindexTerm = qualif (0,[]) where
qualif dg@(d,g) t = case t of
Abs x b -> let x' = ind x d in Abs x' $ qualif (d+1, (x,x'):g) b
Prod x a b -> let x' = ind x d in Prod x' (qualif dg a) $ qualif (d+1, (x,x'):g) b
Abs b x t -> let x' = ind x d in Abs b x' $ qualif (d+1, (x,x'):g) t
Prod b x a t -> let x' = ind x d in Prod b x' (qualif dg a) $ qualif (d+1, (x,x'):g) t
Vr x -> Vr $ look x g
_ -> composSafeOp (qualif dg) t
look x = maybe x id . lookup x --- if x is not in scope it is unchanged

125
src/GF/Grammar/Macros.hs
View File

@@ -33,16 +33,16 @@ import Text.PrettyPrint
firstTypeForm :: Type -> Err (Context, Type)
firstTypeForm t = case t of
Prod x a b -> do
(x', val) <- firstTypeForm b
return ((x,a):x',val)
Prod b x a t -> do
(x', val) <- firstTypeForm t
return ((b,x,a):x',val)
_ -> return ([],t)
qTypeForm :: Type -> Err (Context, Cat, [Term])
qTypeForm t = case t of
Prod x a b -> do
(x', cat, args) <- qTypeForm b
return ((x,a):x', cat, args)
Prod b x a t -> do
(x', cat, args) <- qTypeForm t
return ((b,x,a):x', cat, args)
App c a -> do
(_,cat, args) <- qTypeForm c
return ([],cat,args ++ [a])
@@ -61,9 +61,9 @@ typeForm = qTypeForm ---- no need to distinguish any more
typeFormCnc :: Type -> Err (Context, Type)
typeFormCnc t = case t of
Prod x a b -> do
(x', v) <- typeFormCnc b
return ((x,a):x',v)
Prod b x a t -> do
(x', v) <- typeFormCnc t
return ((b,x,a):x',v)
_ -> return ([],t)
valCat :: Type -> Err Cat
@@ -84,7 +84,7 @@ valTypeCnc typ =
typeRawSkeleton :: Type -> Err ([(Int,Type)],Type)
typeRawSkeleton typ =
do (cont,typ) <- typeFormCnc typ
args <- mapM (typeRawSkeleton . snd) cont
args <- mapM (\(b,x,t) -> typeRawSkeleton t) cont
return ([(length c, v) | (c,v) <- args], typ)
type MCat = (Ident,Ident)
@@ -117,9 +117,9 @@ funsToAndFrom t = errVal undefined $ do ---
typeFormConcrete :: Type -> Err (Context, Type)
typeFormConcrete t = case t of
Prod x a b -> do
(x', typ) <- typeFormConcrete b
return ((x,a):x', typ)
Prod b x a t -> do
(x', typ) <- typeFormConcrete t
return ((b,x,a):x', typ)
_ -> return ([],t)
isRecursiveType :: Type -> Bool
@@ -130,54 +130,49 @@ isRecursiveType t = errVal False $ do
isHigherOrderType :: Type -> Bool
isHigherOrderType t = errVal True $ do -- pessimistic choice
co <- contextOfType t
return $ not $ null [x | (x,Prod _ _ _) <- co]
return $ not $ null [x | (_,x,Prod _ _ _ _) <- co]
contextOfType :: Type -> Err Context
contextOfType typ = case typ of
Prod x a b -> liftM ((x,a):) $ contextOfType b
_ -> return []
Prod b x a t -> liftM ((b,x,a):) $ contextOfType t
_ -> return []
termForm :: Term -> Err ([(Ident)], Term, [Term])
termForm :: Term -> Err ([(BindType,Ident)], Term, [Term])
termForm t = case t of
Abs x b ->
do (x', fun, args) <- termForm b
return (x:x', fun, args)
Abs b x t ->
do (x', fun, args) <- termForm t
return ((b,x):x', fun, args)
App c a ->
do (_,fun, args) <- termForm c
return ([],fun,args ++ [a])
_ ->
return ([],t,[])
termFormCnc :: Term -> ([(Ident)], Term)
termFormCnc :: Term -> ([(BindType,Ident)], Term)
termFormCnc t = case t of
Abs x b -> (x:xs, t') where (xs,t') = termFormCnc b
_ -> ([],t)
Abs b x t -> ((b,x):xs, t') where (xs,t') = termFormCnc t
_ -> ([],t)
appForm :: Term -> (Term, [Term])
appForm t = case t of
App c a -> (fun, args ++ [a]) where (fun, args) = appForm c
_ -> (t,[])
varsOfType :: Type -> [Ident]
varsOfType t = case t of
Prod x _ b -> x : varsOfType b
_ -> []
mkProdSimple :: Context -> Term -> Term
mkProdSimple c t = mkProd (c,t,[])
mkProd :: (Context, Term, [Term]) -> Term
mkProd ([],typ,args) = mkApp typ args
mkProd ((x,a):dd, typ, args) = Prod x a (mkProd (dd, typ, args))
mkProd ([], typ, args) = mkApp typ args
mkProd ((b,x,a):dd, typ, args) = Prod b x a (mkProd (dd, typ, args))
mkTerm :: ([(Ident)], Term, [Term]) -> Term
mkTerm :: ([(BindType,Ident)], Term, [Term]) -> Term
mkTerm (xx,t,aa) = mkAbs xx (mkApp t aa)
mkApp :: Term -> [Term] -> Term
mkApp = foldl App
mkAbs :: [Ident] -> Term -> Term
mkAbs xx t = foldr Abs t xx
mkAbs :: [(BindType,Ident)] -> Term -> Term
mkAbs xx t = foldr (uncurry Abs) t xx
appCons :: Ident -> [Term] -> Term
appCons = mkApp . Cn
@@ -186,7 +181,7 @@ mkLet :: [LocalDef] -> Term -> Term
mkLet defs t = foldr Let t defs
mkLetUntyped :: Context -> Term -> Term
mkLetUntyped defs = mkLet [(x,(Nothing,t)) | (x,t) <- defs]
mkLetUntyped defs = mkLet [(x,(Nothing,t)) | (_,x,t) <- defs]
isVariable :: Term -> Bool
isVariable (Vr _ ) = True
@@ -272,12 +267,12 @@ mkSelects t tt = foldl S t tt
mkTable :: [Term] -> Term -> Term
mkTable tt t = foldr Table t tt
mkCTable :: [Ident] -> Term -> Term
mkCTable :: [(BindType,Ident)] -> Term -> Term
mkCTable ids v = foldr ccase v ids where
ccase x t = T TRaw [(PV x,t)]
ccase (_,x) t = T TRaw [(PV x,t)]
mkHypo :: Term -> Hypo
mkHypo typ = (identW, typ)
mkHypo typ = (Explicit,identW, typ)
eqStrIdent :: Ident -> Ident -> Bool
eqStrIdent = (==)
@@ -298,7 +293,7 @@ mkWildCases :: Term -> Term
mkWildCases = mkCases identW
mkFunType :: [Type] -> Type -> Type
mkFunType tt t = mkProd ([(identW, ty) | ty <- tt], t, []) -- nondep prod
mkFunType tt t = mkProd ([(Explicit,identW, ty) | ty <- tt], t, []) -- nondep prod
plusRecType :: Type -> Type -> Err Type
plusRecType t1 t2 = case (t1, t2) of
@@ -510,13 +505,13 @@ composOp co trm =
do c' <- co c
a' <- co a
return (App c' a')
Abs x b ->
do b' <- co b
return (Abs x b')
Prod x a b ->
Abs b x t ->
do t' <- co t
return (Abs b x t')
Prod b x a t ->
do a' <- co a
b' <- co b
return (Prod x a' b')
t' <- co t
return (Prod b x a' t')
S c a ->
do c' <- co c
a' <- co a
@@ -618,25 +613,25 @@ changeTableType co i = case i of
collectOp :: (Term -> [a]) -> Term -> [a]
collectOp co trm = case trm of
App c a -> co c ++ co a
Abs _ b -> co b
Prod _ a b -> co a ++ co b
S c a -> co c ++ co a
Table a c -> co a ++ co c
ExtR a c -> co a ++ co c
R r -> concatMap (\ (_,(mt,a)) -> maybe [] co mt ++ co a) r
RecType r -> concatMap (co . snd) r
P t i -> co t
T _ cc -> concatMap (co . snd) cc -- not from patterns --- nor from type annot
TSh _ cc -> concatMap (co . snd) cc -- not from patterns --- nor from type annot
V _ cc -> concatMap co cc --- nor from type annot
App c a -> co c ++ co a
Abs _ _ b -> co b
Prod _ _ a b -> co a ++ co b
S c a -> co c ++ co a
Table a c -> co a ++ co c
ExtR a c -> co a ++ co c
R r -> concatMap (\ (_,(mt,a)) -> maybe [] co mt ++ co a) r
RecType r -> concatMap (co . snd) r
P t i -> co t
T _ cc -> concatMap (co . snd) cc -- not from patterns --- nor from type annot
TSh _ cc -> concatMap (co . snd) cc -- not from patterns --- nor from type annot
V _ cc -> concatMap co cc --- nor from type annot
Let (x,(mt,a)) b -> maybe [] co mt ++ co a ++ co b
C s1 s2 -> co s1 ++ co s2
Glue s1 s2 -> co s1 ++ co s2
Alts (t,aa) -> let (x,y) = unzip aa in co t ++ concatMap co (x ++ y)
FV ts -> concatMap co ts
Strs tt -> concatMap co tt
_ -> [] -- covers K, Vr, Cn, Sort
C s1 s2 -> co s1 ++ co s2
Glue s1 s2 -> co s1 ++ co s2
Alts (t,aa) -> let (x,y) = unzip aa in co t ++ concatMap co (x ++ y)
FV ts -> concatMap co ts
Strs tt -> concatMap co tt
_ -> [] -- covers K, Vr, Cn, Sort
-- | to find the word items in a term
wordsInTerm :: Term -> [String]
@@ -653,12 +648,6 @@ noExist = FV []
defaultLinType :: Type
defaultLinType = mkRecType linLabel [typeStr]
-- | from GF1, 20\/9\/2003
isInOneType :: Type -> Bool
isInOneType t = case t of
Prod _ a b -> a == b
_ -> False
-- normalize records and record types; put s first
sortRec :: [(Label,a)] -> [(Label,a)]

48
src/GF/Grammar/Parser.y
View File

@@ -344,6 +344,11 @@ ListIdent
: Ident { [$1] }
| Ident ',' ListIdent { $1 : $3 }
ListIdent2 :: { [Ident] }
ListIdent2
: Ident { [$1] }
| Ident ListIdent2 { $1 : $2 }
Name :: { Ident }
Name
: Ident { $1 }
@@ -492,11 +497,6 @@ Patt2
| '<' ListPattTupleComp '>' { (PR . tuple2recordPatt) $2 }
| '(' Patt ')' { $2 }
Arg :: { Ident }
Arg
: '_' { identW }
| Ident { $1 }
PattAss :: { [(Label,Patt)] }
PattAss
: ListIdent '=' Patt { [(LIdent (ident2bs i),$3) | i <- $1] }
@@ -525,25 +525,32 @@ ListPatt
: Patt2 { [$1] }
| Patt2 ListPatt { $1 : $2 }
ListArg :: { [Ident] }
Arg :: { [(BindType,Ident)] }
Arg
: Ident { [(Explicit,$1 )] }
| '_' { [(Explicit,identW)] }
| '{' ListIdent2 '}' { [(Implicit,v) | v <- $2] }
ListArg :: { [(BindType,Ident)] }
ListArg
: Arg { [$1] }
| Arg ListArg { $1 : $2 }
: Arg { $1 }
| Arg ListArg { $1 ++ $2 }
Bind :: { Ident }
Bind :: { [(BindType,Ident)] }
Bind
: Ident { $1 }
| '_' { identW }
: Ident { [(Explicit,$1 )] }
| '_' { [(Explicit,identW)] }
| '{' ListIdent '}' { [(Implicit,v) | v <- $2] }
ListBind :: { [Ident] }
ListBind :: { [(BindType,Ident)] }
ListBind
: Bind { [$1] }
| Bind ',' ListBind { $1 : $3 }
: Bind { $1 }
| Bind ',' ListBind { $1 ++ $3 }
Decl :: { [Hypo] }
Decl
: '(' ListBind ':' Exp ')' { [(x,$4) | x <- $2] }
| Exp4 { [mkHypo $1] }
: '(' ListBind ':' Exp ')' { [(b,x,$4) | (b,x) <- $2] }
| Exp4 { [mkHypo $1] }
ListTupleComp :: { [Term] }
ListTupleComp
@@ -577,8 +584,8 @@ ListAltern
DDecl :: { [Hypo] }
DDecl
: '(' ListBind ':' Exp ')' { [(x,$4) | x <- $2] }
| Exp6 { [mkHypo $1] }
: '(' ListBind ':' Exp ')' { [(b,x,$4) | (b,x) <- $2] }
| Exp6 { [mkHypo $1] }
ListDDecl :: { [Hypo] }
ListDDecl
@@ -603,6 +610,7 @@ mkBaseId = prefixId (BS.pack "Base")
prefixId :: BS.ByteString -> Ident -> Ident
prefixId pref id = identC (BS.append pref (ident2bs id))
listCatDef :: Ident -> SrcSpan -> Context -> Int -> [(Ident,SrcSpan,Info)]
listCatDef id pos cont size = [catd,nilfund,consfund]
where
listId = mkListId id
@@ -613,8 +621,8 @@ listCatDef id pos cont size = [catd,nilfund,consfund]
nilfund = (baseId, pos, AbsFun (Just niltyp) Nothing Nothing)
consfund = (consId, pos, AbsFun (Just constyp) Nothing Nothing)
cont' = [(mkId x i,ty) | (i,(x,ty)) <- zip [0..] cont]
xs = map (Vr . fst) cont'
cont' = [(b,mkId x i,ty) | (i,(b,x,ty)) <- zip [0..] cont]
xs = map (\(b,x,t) -> Vr x) cont'
cd = mkHypo (mkApp (Vr id) xs)
lc = mkApp (Vr listId) xs

2
src/GF/Grammar/PatternMatch.hs
View File

@@ -146,7 +146,7 @@ isInConstantForm trm = case trm of
Con _ -> True
Q _ _ -> True
QC _ _ -> True
Abs _ _ -> True
Abs _ _ _ -> True
C c a -> isInConstantForm c && isInConstantForm a
App c a -> isInConstantForm c && isInConstantForm a
R r -> all (isInConstantForm . snd . snd) r

28
src/GF/Grammar/Printer.hs
View File

@@ -116,16 +116,16 @@ ppJudgement q (id, CncCat ptype pexp pprn) =
Nothing -> empty)
ppJudgement q (id, CncFun ptype pdef pprn) =
(case pdef of
Just e -> let (vs,e') = getAbs e
in text "lin" <+> ppIdent id <+> hsep (map ppIdent vs) <+> equals <+> ppTerm q 0 e' <+> semi
Just e -> let (xs,e') = getAbs e
in text "lin" <+> ppIdent id <+> hsep (map ppBind xs) <+> equals <+> ppTerm q 0 e' <+> semi
Nothing -> empty) $$
(case pprn of
Just prn -> text "printname" <+> text "fun" <+> ppIdent id <+> equals <+> ppTerm q 0 prn <+> semi
Nothing -> empty)
ppJudgement q (id, AnyInd cann mid) = text "ind" <+> ppIdent id <+> equals <+> (if cann then text "canonical" else empty) <+> ppIdent mid <+> semi
ppTerm q d (Abs v e) = let (vs,e') = getAbs e
in prec d 0 (char '\\' <> commaPunct ppIdent (v:vs) <+> text "->" <+> ppTerm q 0 e')
ppTerm q d (Abs b v e) = let (xs,e') = getAbs (Abs b v e)
in prec d 0 (char '\\' <> commaPunct ppBind xs <+> text "->" <+> ppTerm q 0 e')
ppTerm q d (T TRaw xs) = case getCTable (T TRaw xs) of
([],_) -> text "table" <+> lbrace $$
nest 2 (vcat (punctuate semi (map (ppCase q) xs))) $$
@@ -140,9 +140,9 @@ ppTerm q d (T (TComp t) xs) = text "table" <+> ppTerm q 0 t <+> lbrace $$
ppTerm q d (T (TWild t) xs) = text "table" <+> ppTerm q 0 t <+> lbrace $$
nest 2 (vcat (punctuate semi (map (ppCase q) xs))) $$
rbrace
ppTerm q d (Prod x a b)= if x == identW
then prec d 0 (ppTerm q 4 a <+> text "->" <+> ppTerm q 0 b)
else prec d 0 (parens (ppIdent x <+> colon <+> ppTerm q 0 a) <+> text "->" <+> ppTerm q 0 b)
ppTerm q d (Prod bt x a b)= if x == identW && bt == Explicit
then prec d 0 (ppTerm q 4 a <+> text "->" <+> ppTerm q 0 b)
else prec d 0 (parens (ppBind (bt,x) <+> colon <+> ppTerm q 0 a) <+> text "->" <+> ppTerm q 0 b)
ppTerm q d (Table kt vt)=prec d 0 (ppTerm q 3 kt <+> text "=>" <+> ppTerm q 0 vt)
ppTerm q d (Let l e) = let (ls,e') = getLet e
in prec d 0 (text "let" <+> vcat (map (ppLocDef q) (l:ls)) $$ text "in" <+> ppTerm q 0 e')
@@ -246,11 +246,11 @@ ppEnv e = hcat (map (\(x,t) -> braces (ppIdent x <> text ":=" <> ppValue Unquali
str s = doubleQuotes (text s)
ppDecl q (id,typ)
ppDecl q (_,id,typ)
| id == identW = ppTerm q 4 typ
| otherwise = parens (ppIdent id <+> colon <+> ppTerm q 0 typ)
ppDDecl q (id,typ)
ppDDecl q (_,id,typ)
| id == identW = ppTerm q 6 typ
| otherwise = parens (ppIdent id <+> colon <+> ppTerm q 0 typ)
@@ -272,6 +272,8 @@ ppLocDef q (id, (mbt, e)) =
ppIdent id <+>
(case mbt of {Just t -> colon <+> ppTerm q 0 t; Nothing -> empty} <+> equals <+> ppTerm q 0 e) <+> semi
ppBind (Explicit,v) = ppIdent v
ppBind (Implicit,v) = braces (ppIdent v)
ppAltern q (x,y) = ppTerm q 0 x <+> char '/' <+> ppTerm q 0 y
@@ -283,10 +285,10 @@ prec d1 d2 doc
| d1 > d2 = parens doc
| otherwise = doc
getAbs :: Term -> ([Ident], Term)
getAbs (Abs v e) = let (vs,e') = getAbs e
in (v:vs,e')
getAbs e = ([],e)
getAbs :: Term -> ([(BindType,Ident)], Term)
getAbs (Abs bt v e) = let (xs,e') = getAbs e
in ((bt,v):xs,e')
getAbs e = ([],e)
getCTable :: Term -> ([Ident], Term)
getCTable (T TRaw [(PV v,e)]) = let (vs,e') = getCTable e

6
src/GF/Grammar/Unify.hs
View File

@@ -60,8 +60,8 @@ unify e1 e2 g =
(Q _ a, Q _ b) | (a == b) -> return g ---- qualif?
(QC _ a, QC _ b) | (a == b) -> return g ----
(Vr x, Vr y) | (x == y) -> return g
(Abs x b, Abs y c) -> do let c' = substTerm [x] [(y,Vr x)] c
unify b c' g
(Abs _ x b, Abs _ y c) -> do let c' = substTerm [x] [(y,Vr x)] c
unify b c' g
(App c a, App d b) -> case unify c d g of
Ok g1 -> unify a b g1
_ -> Bad (render (text "fail unify" <+> ppTerm Unqualified 0 e1))
@@ -92,6 +92,6 @@ occCheck :: MetaId -> Term -> Bool
occCheck s u = case u of
Meta v -> s == v
App c a -> occCheck s c || occCheck s a
Abs x b -> occCheck s b
Abs _ x b -> occCheck s b
_ -> False

6
src/GF/Infra/CheckM.hs
View File

@@ -80,9 +80,9 @@ checkGetContext = Check (\ctxt msgs -> Success ctxt ctxt msgs)
checkLookup :: Ident -> Check Type
checkLookup x = do
co <- checkGetContext
case lookup x co of
Nothing -> checkError (text "unknown variable" <+> ppIdent x)
Just ty -> return ty
case [ty | (b,y,ty) <- co, x == y] of
[] -> checkError (text "unknown variable" <+> ppIdent x)
(ty:_) -> return ty
runCheck :: Check a -> Either [Message] (a,Context,[Message])
runCheck c =