mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-23 03:32:51 -06:00
refactoring in GF.Grammar.Grammar
This commit is contained in:
@@ -72,7 +72,7 @@ computeAbsTermIn lookd xs e = errIn (render (text "computing" <+> ppTerm Unquali
|
|||||||
tracd (text "not defined" <+> ppTerm Unqualified 0 t2) $ return t2
|
tracd (text "not defined" <+> ppTerm Unqualified 0 t2) $ return t2
|
||||||
|
|
||||||
look t = case t of
|
look t = case t of
|
||||||
(Q m f) -> case lookd m f of
|
(Q (m,f)) -> case lookd m f of
|
||||||
Ok (_,md) -> md
|
Ok (_,md) -> md
|
||||||
_ -> Nothing
|
_ -> Nothing
|
||||||
_ -> Nothing
|
_ -> Nothing
|
||||||
@@ -114,11 +114,11 @@ tryMatch (p,t) = do
|
|||||||
(PString s, ([],K i,[])) | s==i -> return []
|
(PString s, ([],K i,[])) | s==i -> return []
|
||||||
(PInt s, ([],EInt i,[])) | s==i -> return []
|
(PInt s, ([],EInt i,[])) | s==i -> return []
|
||||||
(PFloat s,([],EFloat i,[])) | s==i -> return [] --- rounding?
|
(PFloat s,([],EFloat i,[])) | s==i -> return [] --- rounding?
|
||||||
(PP q p pp, ([], QC r f, tt)) |
|
(PP (q,p) pp, ([], QC (r,f), tt)) |
|
||||||
p `eqStrIdent` f && length pp == length tt -> do
|
p `eqStrIdent` f && length pp == length tt -> do
|
||||||
matches <- mapM tryMatch (zip pp tt)
|
matches <- mapM tryMatch (zip pp tt)
|
||||||
return (concat matches)
|
return (concat matches)
|
||||||
(PP q p pp, ([], Q r f, tt)) |
|
(PP (q,p) pp, ([], Q (r,f), tt)) |
|
||||||
p `eqStrIdent` f && length pp == length tt -> do
|
p `eqStrIdent` f && length pp == length tt -> do
|
||||||
matches <- mapM tryMatch (zip pp tt)
|
matches <- mapM tryMatch (zip pp tt)
|
||||||
return (concat matches)
|
return (concat matches)
|
||||||
|
|||||||
@@ -84,8 +84,8 @@ eval :: Env -> Exp -> Err Val
|
|||||||
eval env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $
|
eval env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $
|
||||||
case e of
|
case e of
|
||||||
Vr x -> lookupVar env x
|
Vr x -> lookupVar env x
|
||||||
Q m c -> return $ VCn (m,c)
|
Q c -> return $ VCn c
|
||||||
QC m c -> return $ VCn (m,c) ---- == Q ?
|
QC c -> return $ VCn c ---- == Q ?
|
||||||
Sort c -> return $ VType --- the only sort is Type
|
Sort c -> return $ VType --- the only sort is Type
|
||||||
App f a -> join $ liftM2 app (eval env f) (eval env a)
|
App f a -> join $ liftM2 app (eval env f) (eval env a)
|
||||||
RecType xs -> do xs <- mapM (\(l,e) -> eval env e >>= \e -> return (l,e)) xs
|
RecType xs -> do xs <- mapM (\(l,e) -> eval env e >>= \e -> return (l,e)) xs
|
||||||
@@ -161,10 +161,10 @@ checkInferExp th tenv@(k,_,_) e typ = do
|
|||||||
inferExp :: Theory -> TCEnv -> Exp -> Err (AExp, Val, [(Val,Val)])
|
inferExp :: Theory -> TCEnv -> Exp -> Err (AExp, Val, [(Val,Val)])
|
||||||
inferExp th tenv@(k,rho,gamma) e = case e of
|
inferExp th tenv@(k,rho,gamma) e = case e of
|
||||||
Vr x -> mkAnnot (AVr x) $ noConstr $ lookupVar gamma x
|
Vr x -> mkAnnot (AVr x) $ noConstr $ lookupVar gamma x
|
||||||
Q m c | m == cPredefAbs && isPredefCat c
|
Q (m,c) | m == cPredefAbs && isPredefCat c
|
||||||
-> return (ACn (m,c) vType, vType, [])
|
-> return (ACn (m,c) vType, vType, [])
|
||||||
| otherwise -> mkAnnot (ACn (m,c)) $ noConstr $ lookupConst th (m,c)
|
| otherwise -> mkAnnot (ACn (m,c)) $ noConstr $ lookupConst th (m,c)
|
||||||
QC m c -> mkAnnot (ACn (m,c)) $ noConstr $ lookupConst th (m,c) ----
|
QC c -> mkAnnot (ACn c) $ noConstr $ lookupConst th c ----
|
||||||
EInt i -> return (AInt i, valAbsInt, [])
|
EInt i -> return (AInt i, valAbsInt, [])
|
||||||
EFloat i -> return (AFloat i, valAbsFloat, [])
|
EFloat i -> return (AFloat i, valAbsFloat, [])
|
||||||
K i -> return (AStr i, valAbsString, [])
|
K i -> return (AStr i, valAbsString, [])
|
||||||
@@ -240,7 +240,7 @@ checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
|
|||||||
PString s -> (K s : ps, i, g, k)
|
PString s -> (K s : ps, i, g, k)
|
||||||
PInt n -> (EInt n : ps, i, g, k)
|
PInt n -> (EInt n : ps, i, g, k)
|
||||||
PFloat n -> (EFloat n : ps, i, g, k)
|
PFloat n -> (EFloat n : ps, i, g, k)
|
||||||
PP m c xs -> (mkApp (Q m c) xss : ps, j, g',k')
|
PP c xs -> (mkApp (Q c) xss : ps, j, g',k')
|
||||||
where (xss,j,g',k') = foldr p2t ([],i,g,k) xs
|
where (xss,j,g',k') = foldr p2t ([],i,g,k) xs
|
||||||
PImplArg p -> p2t p (ps,i,g,k)
|
PImplArg p -> p2t p (ps,i,g,k)
|
||||||
PTilde t -> (t : ps, i, g, k)
|
PTilde t -> (t : ps, i, g, k)
|
||||||
@@ -268,12 +268,12 @@ checkPatt th tenv exp val = do
|
|||||||
EFloat i -> return (AFloat i, valAbsFloat, [])
|
EFloat i -> return (AFloat i, valAbsFloat, [])
|
||||||
K s -> return (AStr s, valAbsString, [])
|
K s -> return (AStr s, valAbsString, [])
|
||||||
|
|
||||||
Q m c -> do
|
Q c -> do
|
||||||
typ <- lookupConst th (m,c)
|
typ <- lookupConst th c
|
||||||
return $ (ACn (m,c) typ, typ, [])
|
return $ (ACn c typ, typ, [])
|
||||||
QC m c -> do
|
QC c -> do
|
||||||
typ <- lookupConst th (m,c)
|
typ <- lookupConst th c
|
||||||
return $ (ACn (m,c) typ, typ, []) ----
|
return $ (ACn c typ, typ, []) ----
|
||||||
App f t -> do
|
App f t -> do
|
||||||
(f',w,csf) <- checkExpP tenv f val
|
(f',w,csf) <- checkExpP tenv f val
|
||||||
typ <- whnf w
|
typ <- whnf w
|
||||||
|
|||||||
@@ -99,7 +99,7 @@ checkCompleteGrammar gr (am,abs) (cm,cnc) = do
|
|||||||
let (cxt,(_,i),_) = typeForm ty
|
let (cxt,(_,i),_) = typeForm ty
|
||||||
info <- lookupIdent i js
|
info <- lookupIdent i js
|
||||||
info <- case info of
|
info <- case info of
|
||||||
(AnyInd _ m) -> do (m,info) <- lookupOrigInfo gr m i
|
(AnyInd _ m) -> do (m,info) <- lookupOrigInfo gr (m,i)
|
||||||
return info
|
return info
|
||||||
_ -> return info
|
_ -> return info
|
||||||
case info of
|
case info of
|
||||||
@@ -137,14 +137,14 @@ checkCompleteGrammar gr (am,abs) (cm,cnc) = do
|
|||||||
|
|
||||||
checkCnc js i@(c,info) =
|
checkCnc js i@(c,info) =
|
||||||
case info of
|
case info of
|
||||||
CncFun _ d pn -> case lookupOrigInfo gr am c of
|
CncFun _ d pn -> case lookupOrigInfo gr (am,c) of
|
||||||
Ok (_,AbsFun (Just (L _ ty)) _ _) ->
|
Ok (_,AbsFun (Just (L _ ty)) _ _) ->
|
||||||
do (cont,val) <- linTypeOfType gr cm ty
|
do (cont,val) <- linTypeOfType gr cm ty
|
||||||
let linty = (snd (valCat ty),cont,val)
|
let linty = (snd (valCat ty),cont,val)
|
||||||
return $ updateTree (c,CncFun (Just linty) d pn) js
|
return $ updateTree (c,CncFun (Just linty) d pn) js
|
||||||
_ -> do checkWarn $ text "function" <+> ppIdent c <+> text "is not in abstract"
|
_ -> do checkWarn $ text "function" <+> ppIdent c <+> text "is not in abstract"
|
||||||
return js
|
return js
|
||||||
CncCat _ _ _ -> case lookupOrigInfo gr am c of
|
CncCat _ _ _ -> case lookupOrigInfo gr (am,c) of
|
||||||
Ok _ -> return $ updateTree i js
|
Ok _ -> return $ updateTree i js
|
||||||
_ -> do checkWarn $ text "category" <+> ppIdent c <+> text "is not in abstract"
|
_ -> do checkWarn $ text "category" <+> ppIdent c <+> text "is not in abstract"
|
||||||
return js
|
return js
|
||||||
@@ -206,7 +206,7 @@ checkInfo ms (m,mo) c info = do
|
|||||||
|
|
||||||
ResOverload os tysts -> chIn (0,0) "overloading" $ do
|
ResOverload os tysts -> chIn (0,0) "overloading" $ do
|
||||||
tysts' <- mapM (uncurry $ flip (\(L loc1 t) (L loc2 ty) -> checkLType gr [] t ty >>= \(t,ty) -> return (L loc1 t, L loc2 ty))) tysts -- return explicit ones
|
tysts' <- mapM (uncurry $ flip (\(L loc1 t) (L loc2 ty) -> checkLType gr [] t ty >>= \(t,ty) -> return (L loc1 t, L loc2 ty))) tysts -- return explicit ones
|
||||||
tysts0 <- checkErr $ lookupOverload gr m c -- check against inherited ones too
|
tysts0 <- checkErr $ lookupOverload gr (m,c) -- check against inherited ones too
|
||||||
tysts1 <- mapM (uncurry $ flip (checkLType gr []))
|
tysts1 <- mapM (uncurry $ flip (checkLType gr []))
|
||||||
[(mkFunType args val,tr) | (args,(val,tr)) <- tysts0]
|
[(mkFunType args val,tr) | (args,(val,tr)) <- tysts0]
|
||||||
--- this can only be a partial guarantee, since matching
|
--- this can only be a partial guarantee, since matching
|
||||||
@@ -227,7 +227,7 @@ checkInfo ms (m,mo) c info = do
|
|||||||
mkPar (L loc (f,co)) =
|
mkPar (L loc (f,co)) =
|
||||||
chIn loc "parameter type" $ do
|
chIn loc "parameter type" $ do
|
||||||
vs <- checkErr $ liftM combinations $ mapM (\(_,_,ty) -> allParamValues gr ty) co
|
vs <- checkErr $ liftM combinations $ mapM (\(_,_,ty) -> allParamValues gr ty) co
|
||||||
return $ map (mkApp (QC m f)) vs
|
return $ map (mkApp (QC (m,f))) vs
|
||||||
|
|
||||||
checkUniq xss = case xss of
|
checkUniq xss = case xss of
|
||||||
x:y:xs
|
x:y:xs
|
||||||
|
|||||||
@@ -71,13 +71,13 @@ appPredefined t = case t of
|
|||||||
(x,_) <- appPredefined x0
|
(x,_) <- appPredefined x0
|
||||||
case f of
|
case f of
|
||||||
-- one-place functions
|
-- one-place functions
|
||||||
Q mod f | mod == cPredef ->
|
Q (mod,f) | mod == cPredef ->
|
||||||
case x of
|
case x of
|
||||||
(K s) | f == cLength -> retb $ EInt $ toInteger $ length s
|
(K s) | f == cLength -> retb $ EInt $ toInteger $ length s
|
||||||
_ -> retb t
|
_ -> retb t
|
||||||
|
|
||||||
-- two-place functions
|
-- two-place functions
|
||||||
App (Q mod f) z0 | mod == cPredef -> do
|
App (Q (mod,f)) z0 | mod == cPredef -> do
|
||||||
(z,_) <- appPredefined z0
|
(z,_) <- appPredefined z0
|
||||||
case (norm z, norm x) of
|
case (norm z, norm x) of
|
||||||
(EInt i, K s) | f == cDrop -> retb $ K (drop (fi i) s)
|
(EInt i, K s) | f == cDrop -> retb $ K (drop (fi i) s)
|
||||||
@@ -96,7 +96,7 @@ appPredefined t = case t of
|
|||||||
_ -> retb t ---- prtBad "cannot compute predefined" t
|
_ -> retb t ---- prtBad "cannot compute predefined" t
|
||||||
|
|
||||||
-- three-place functions
|
-- three-place functions
|
||||||
App (App (Q mod f) z0) y0 | mod == cPredef -> do
|
App (App (Q (mod,f)) z0) y0 | mod == cPredef -> do
|
||||||
(y,_) <- appPredefined y0
|
(y,_) <- appPredefined y0
|
||||||
(z,_) <- appPredefined z0
|
(z,_) <- appPredefined z0
|
||||||
case (z, y, x) of
|
case (z, y, x) of
|
||||||
@@ -123,8 +123,8 @@ appPredefined t = case t of
|
|||||||
|
|
||||||
-- read makes variables into constants
|
-- read makes variables into constants
|
||||||
|
|
||||||
predefTrue = QC cPredef cPTrue
|
predefTrue = QC (cPredef,cPTrue)
|
||||||
predefFalse = QC cPredef cPFalse
|
predefFalse = QC (cPredef,cPFalse)
|
||||||
|
|
||||||
substring :: String -> String -> Bool
|
substring :: String -> String -> Bool
|
||||||
substring s t = case (s,t) of
|
substring s t = case (s,t) of
|
||||||
|
|||||||
@@ -52,8 +52,8 @@ computeTermOpt rec gr = comput True where
|
|||||||
comput full g t = ---- errIn ("subterm" +++ prt t) $ --- for debugging
|
comput full g t = ---- errIn ("subterm" +++ prt t) $ --- for debugging
|
||||||
case t of
|
case t of
|
||||||
|
|
||||||
Q p c | p == cPredef -> return t
|
Q (p,c) | p == cPredef -> return t
|
||||||
| otherwise -> look p c
|
| otherwise -> look (p,c)
|
||||||
|
|
||||||
Vr x -> do
|
Vr x -> do
|
||||||
t' <- maybe (Bad (render (text "no value given to variable" <+> ppIdent x))) return $ lookup x g
|
t' <- maybe (Bad (render (text "no value given to variable" <+> ppIdent x))) return $ lookup x g
|
||||||
@@ -86,9 +86,9 @@ computeTermOpt rec gr = comput True where
|
|||||||
as' <- mapM (comp g) as
|
as' <- mapM (comp g) as
|
||||||
case h' of
|
case h' of
|
||||||
_ | not (null [() | FV _ <- as']) -> compApp g (mkApp h' as')
|
_ | not (null [() | FV _ <- as']) -> compApp g (mkApp h' as')
|
||||||
c@(QC _ _) -> do
|
c@(QC _) -> do
|
||||||
return $ mkApp c as'
|
return $ mkApp c as'
|
||||||
Q mod f | mod == cPredef -> do
|
Q (mod,f) | mod == cPredef -> do
|
||||||
(t',b) <- appPredefined (mkApp h' as')
|
(t',b) <- appPredefined (mkApp h' as')
|
||||||
if b then return t' else comp g t'
|
if b then return t' else comp g t'
|
||||||
|
|
||||||
@@ -163,11 +163,11 @@ computeTermOpt rec gr = comput True where
|
|||||||
(_,Empty) -> return x
|
(_,Empty) -> return x
|
||||||
(Empty,_) -> return y
|
(Empty,_) -> return y
|
||||||
(K a, K b) -> return $ K (a ++ b)
|
(K a, K b) -> return $ K (a ++ b)
|
||||||
(_, Alts (d,vs)) -> do
|
(_, Alts d vs) -> do
|
||||||
---- (K a, Alts (d,vs)) -> do
|
---- (K a, Alts (d,vs)) -> do
|
||||||
let glx = Glue x
|
let glx = Glue x
|
||||||
comp g $ Alts (glx d, [(glx v,c) | (v,c) <- vs])
|
comp g $ Alts (glx d) [(glx v,c) | (v,c) <- vs]
|
||||||
(Alts _, ka) -> checks [do
|
(Alts _ _, ka) -> checks [do
|
||||||
y' <- strsFromTerm ka
|
y' <- strsFromTerm ka
|
||||||
---- (Alts _, K a) -> checks [do
|
---- (Alts _, K a) -> checks [do
|
||||||
x' <- strsFromTerm x -- this may fail when compiling opers
|
x' <- strsFromTerm x -- this may fail when compiling opers
|
||||||
@@ -183,17 +183,17 @@ computeTermOpt rec gr = comput True where
|
|||||||
r <- composOp (comp g) t
|
r <- composOp (comp g) t
|
||||||
returnC r
|
returnC r
|
||||||
|
|
||||||
Alts (d,aa) -> do
|
Alts d aa -> do
|
||||||
d' <- comp g d
|
d' <- comp g d
|
||||||
aa' <- mapM (compInAlts g) aa
|
aa' <- mapM (compInAlts g) aa
|
||||||
returnC (Alts (d',aa'))
|
returnC (Alts d' aa')
|
||||||
|
|
||||||
-- remove empty
|
-- remove empty
|
||||||
C a b -> do
|
C a b -> do
|
||||||
a' <- comp g a
|
a' <- comp g a
|
||||||
b' <- comp g b
|
b' <- comp g b
|
||||||
case (a',b') of
|
case (a',b') of
|
||||||
(Alts _, K a) -> checks [do
|
(Alts _ _, K a) -> checks [do
|
||||||
as <- strsFromTerm a' -- this may fail when compiling opers
|
as <- strsFromTerm a' -- this may fail when compiling opers
|
||||||
return $ variants [
|
return $ variants [
|
||||||
foldr1 C (map K (str2strings (plusStr v (str a)))) | v <- as]
|
foldr1 C (map K (str2strings (plusStr v (str a)))) | v <- as]
|
||||||
@@ -238,7 +238,7 @@ computeTermOpt rec gr = comput True where
|
|||||||
(FV fs, _) -> mapM (\c -> comp g (App c a')) fs >>= 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'
|
(QC _,_) -> returnC $ App f' a'
|
||||||
|
|
||||||
(S (T i cs) e,_) -> prawitz g i (flip App a') cs e
|
(S (T i cs) e,_) -> prawitz g i (flip App a') cs e
|
||||||
(S (V i cs) e,_) -> prawitzV g i (flip App a') cs e
|
(S (V i cs) e,_) -> prawitzV g i (flip App a') cs e
|
||||||
@@ -250,9 +250,9 @@ computeTermOpt rec gr = comput True where
|
|||||||
hnf = comput False
|
hnf = comput False
|
||||||
comp = comput True
|
comp = comput True
|
||||||
|
|
||||||
look p c
|
look c
|
||||||
| rec = lookupResDef gr p c >>= comp []
|
| rec = lookupResDef gr c >>= comp []
|
||||||
| otherwise = lookupResDef gr p c
|
| otherwise = lookupResDef gr c
|
||||||
|
|
||||||
ext x a g = (x,a):g
|
ext x a g = (x,a):g
|
||||||
|
|
||||||
@@ -264,13 +264,13 @@ computeTermOpt rec gr = comput True where
|
|||||||
|
|
||||||
isCan v = case v of
|
isCan v = case v of
|
||||||
Con _ -> True
|
Con _ -> True
|
||||||
QC _ _ -> True
|
QC _ -> True
|
||||||
App f a -> isCan f && isCan a
|
App f a -> isCan f && isCan a
|
||||||
R rs -> all (isCan . snd . snd) rs
|
R rs -> all (isCan . snd . snd) rs
|
||||||
_ -> False
|
_ -> False
|
||||||
|
|
||||||
compPatternMacro p = case p of
|
compPatternMacro p = case p of
|
||||||
PM m c -> case look m c of
|
PM c -> case look c of
|
||||||
Ok (EPatt p') -> compPatternMacro p'
|
Ok (EPatt p') -> compPatternMacro p'
|
||||||
_ -> Bad (render (text "pattern expected as value of" $$ nest 2 (ppPatt Unqualified 0 p)))
|
_ -> Bad (render (text "pattern expected as value of" $$ nest 2 (ppPatt Unqualified 0 p)))
|
||||||
PAs x p -> do
|
PAs x p -> do
|
||||||
@@ -384,7 +384,7 @@ computeTermOpt rec gr = comput True where
|
|||||||
contP p = case p of
|
contP p = case p of
|
||||||
PV x -> [(x,Vr x)]
|
PV x -> [(x,Vr x)]
|
||||||
PC _ ps -> concatMap contP ps
|
PC _ ps -> concatMap contP ps
|
||||||
PP _ _ ps -> concatMap contP ps
|
PP _ ps -> concatMap contP ps
|
||||||
PT _ p -> contP p
|
PT _ p -> contP p
|
||||||
PR rs -> concatMap (contP . snd) rs
|
PR rs -> concatMap (contP . snd) rs
|
||||||
|
|
||||||
|
|||||||
@@ -23,8 +23,8 @@ computeLType gr g0 t = comp (reverse [(b,x, Vr x) | (b,x,_) <- g0] ++ g0) t
|
|||||||
_ | Just _ <- isTypeInts ty -> return ty ---- shouldn't be needed
|
_ | Just _ <- isTypeInts ty -> return ty ---- shouldn't be needed
|
||||||
| isPredefConstant ty -> return ty ---- shouldn't be needed
|
| isPredefConstant ty -> return ty ---- shouldn't be needed
|
||||||
|
|
||||||
Q m ident -> checkIn (text "module" <+> ppIdent m) $ do
|
Q (m,ident) -> checkIn (text "module" <+> ppIdent m) $ do
|
||||||
ty' <- checkErr (lookupResDef gr m ident)
|
ty' <- checkErr (lookupResDef gr (m,ident))
|
||||||
if ty' == ty then return ty else comp g ty' --- is this necessary to test?
|
if ty' == ty then return ty else comp g ty' --- is this necessary to test?
|
||||||
|
|
||||||
Vr ident -> checkLookup ident g -- never needed to compute!
|
Vr ident -> checkLookup ident g -- never needed to compute!
|
||||||
@@ -70,22 +70,22 @@ computeLType gr g0 t = comp (reverse [(b,x, Vr x) | (b,x,_) <- g0] ++ g0) t
|
|||||||
inferLType :: SourceGrammar -> Context -> Term -> Check (Term, Type)
|
inferLType :: SourceGrammar -> Context -> Term -> Check (Term, Type)
|
||||||
inferLType gr g trm = case trm of
|
inferLType gr g trm = case trm of
|
||||||
|
|
||||||
Q m ident | isPredef m -> termWith trm $ checkErr (typPredefined ident)
|
Q (m,ident) | isPredef m -> termWith trm $ checkErr (typPredefined ident)
|
||||||
|
|
||||||
Q m ident -> checks [
|
Q ident -> checks [
|
||||||
termWith trm $ checkErr (lookupResType gr m ident) >>= computeLType gr g
|
termWith trm $ checkErr (lookupResType gr ident) >>= computeLType gr g
|
||||||
,
|
,
|
||||||
checkErr (lookupResDef gr m ident) >>= inferLType gr g
|
checkErr (lookupResDef gr ident) >>= inferLType gr g
|
||||||
,
|
,
|
||||||
checkError (text "cannot infer type of constant" <+> ppTerm Unqualified 0 trm)
|
checkError (text "cannot infer type of constant" <+> ppTerm Unqualified 0 trm)
|
||||||
]
|
]
|
||||||
|
|
||||||
QC m ident | isPredef m -> termWith trm $ checkErr (typPredefined ident)
|
QC (m,ident) | isPredef m -> termWith trm $ checkErr (typPredefined ident)
|
||||||
|
|
||||||
QC m ident -> checks [
|
QC ident -> checks [
|
||||||
termWith trm $ checkErr (lookupResType gr m ident) >>= computeLType gr g
|
termWith trm $ checkErr (lookupResType gr ident) >>= computeLType gr g
|
||||||
,
|
,
|
||||||
checkErr (lookupResDef gr m ident) >>= inferLType gr g
|
checkErr (lookupResDef gr ident) >>= inferLType gr g
|
||||||
,
|
,
|
||||||
checkError (text "cannot infer type of canonical constant" <+> ppTerm Unqualified 0 trm)
|
checkError (text "cannot infer type of canonical constant" <+> ppTerm Unqualified 0 trm)
|
||||||
]
|
]
|
||||||
@@ -188,13 +188,13 @@ inferLType gr g trm = case trm of
|
|||||||
ts' <- mapM (\t -> justCheck g t typeStr) ts
|
ts' <- mapM (\t -> justCheck g t typeStr) ts
|
||||||
return (Strs ts', typeStrs)
|
return (Strs ts', typeStrs)
|
||||||
|
|
||||||
Alts (t,aa) -> do
|
Alts t aa -> do
|
||||||
t' <- justCheck g t typeStr
|
t' <- justCheck g t typeStr
|
||||||
aa' <- flip mapM aa (\ (c,v) -> do
|
aa' <- flip mapM aa (\ (c,v) -> do
|
||||||
c' <- justCheck g c typeStr
|
c' <- justCheck g c typeStr
|
||||||
v' <- checks $ map (justCheck g v) [typeStrs, EPattType typeStr]
|
v' <- checks $ map (justCheck g v) [typeStrs, EPattType typeStr]
|
||||||
return (c',v'))
|
return (c',v'))
|
||||||
return (Alts (t',aa'), typeStr)
|
return (Alts t' aa', typeStr)
|
||||||
|
|
||||||
RecType r -> do
|
RecType r -> do
|
||||||
let (ls,ts) = unzip r
|
let (ls,ts) = unzip r
|
||||||
@@ -267,7 +267,7 @@ inferLType gr g trm = case trm of
|
|||||||
return (arg,val)
|
return (arg,val)
|
||||||
isConstPatt p = case p of
|
isConstPatt p = case p of
|
||||||
PC _ ps -> True --- all isConstPatt ps
|
PC _ ps -> True --- all isConstPatt ps
|
||||||
PP _ _ ps -> True --- all isConstPatt ps
|
PP _ ps -> True --- all isConstPatt ps
|
||||||
PR ps -> all (isConstPatt . snd) ps
|
PR ps -> all (isConstPatt . snd) ps
|
||||||
PT _ p -> isConstPatt p
|
PT _ p -> isConstPatt p
|
||||||
PString _ -> True
|
PString _ -> True
|
||||||
@@ -283,7 +283,7 @@ inferLType gr g trm = case trm of
|
|||||||
_ -> False
|
_ -> False
|
||||||
|
|
||||||
inferPatt p = case p of
|
inferPatt p = case p of
|
||||||
PP q c ps | q /= cPredef -> checkErr $ liftM valTypeCnc (lookupResType gr q c)
|
PP (q,c) ps | q /= cPredef -> checkErr $ liftM valTypeCnc (lookupResType gr (q,c))
|
||||||
PAs _ p -> inferPatt p
|
PAs _ p -> inferPatt p
|
||||||
PNeg p -> inferPatt p
|
PNeg p -> inferPatt p
|
||||||
PAlt p q -> checks [inferPatt p, inferPatt q]
|
PAlt p q -> checks [inferPatt p, inferPatt q]
|
||||||
@@ -298,7 +298,7 @@ inferLType gr g trm = case trm of
|
|||||||
-- the latter permits matching with value type
|
-- the latter permits matching with value type
|
||||||
getOverload :: SourceGrammar -> Context -> Maybe Type -> Term -> Check (Maybe (Term,Type))
|
getOverload :: SourceGrammar -> Context -> Maybe Type -> Term -> Check (Maybe (Term,Type))
|
||||||
getOverload gr g mt ot = case appForm ot of
|
getOverload gr g mt ot = case appForm ot of
|
||||||
(f@(Q m c), ts) -> case lookupOverload gr m c of
|
(f@(Q c), ts) -> case lookupOverload gr c of
|
||||||
Ok typs -> do
|
Ok typs -> do
|
||||||
ttys <- mapM (inferLType gr g) ts
|
ttys <- mapM (inferLType gr g) ts
|
||||||
v <- matchOverload f typs ttys
|
v <- matchOverload f typs ttys
|
||||||
@@ -390,7 +390,7 @@ checkLType gr g trm typ0 = do
|
|||||||
(trm',ty') <- inferLType gr g trm
|
(trm',ty') <- inferLType gr g trm
|
||||||
termWith trm' $ checkEqLType gr g typ ty' trm'
|
termWith trm' $ checkEqLType gr g typ ty' trm'
|
||||||
|
|
||||||
Q _ _ -> do
|
Q _ -> do
|
||||||
over <- getOverload gr g (Just typ) trm
|
over <- getOverload gr g (Just typ) trm
|
||||||
case over of
|
case over of
|
||||||
Just trty -> return trty
|
Just trty -> return trty
|
||||||
@@ -522,8 +522,8 @@ checkLType gr g trm typ0 = do
|
|||||||
pattContext :: SourceGrammar -> Context -> Type -> Patt -> Check Context
|
pattContext :: SourceGrammar -> Context -> Type -> Patt -> Check Context
|
||||||
pattContext env g typ p = case p of
|
pattContext env g typ p = case p of
|
||||||
PV x -> return [(Explicit,x,typ)]
|
PV x -> return [(Explicit,x,typ)]
|
||||||
PP q c ps | q /= cPredef -> do ---- why this /=? AR 6/1/2006
|
PP (q,c) ps | q /= cPredef -> do ---- why this /=? AR 6/1/2006
|
||||||
t <- checkErr $ lookupResType env q c
|
t <- checkErr $ lookupResType env (q,c)
|
||||||
let (cont,v) = typeFormCnc t
|
let (cont,v) = typeFormCnc t
|
||||||
checkCond (text "wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p)
|
checkCond (text "wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p)
|
||||||
(length cont == length ps)
|
(length cont == length ps)
|
||||||
@@ -617,15 +617,15 @@ checkIfEqLType gr g t u trm = do
|
|||||||
| t == typeInt, Just _ <- isTypeInts u -> True ---- why this ???? AR 11/12/2005
|
| t == typeInt, Just _ <- isTypeInts u -> True ---- why this ???? AR 11/12/2005
|
||||||
|
|
||||||
---- this should be made in Rename
|
---- this should be made in Rename
|
||||||
(Q m a, Q n b) | a == b -> elem m (allExtendsPlus gr n)
|
(Q (m,a), Q (n,b)) | a == b -> elem m (allExtendsPlus gr n)
|
||||||
|| elem n (allExtendsPlus gr m)
|
|| elem n (allExtendsPlus gr m)
|
||||||
|| m == n --- for Predef
|
|| m == n --- for Predef
|
||||||
(QC m a, QC n b) | a == b -> elem m (allExtendsPlus gr n)
|
(QC (m,a), QC (n,b)) | a == b -> elem m (allExtendsPlus gr n)
|
||||||
|| elem n (allExtendsPlus gr m)
|
|| elem n (allExtendsPlus gr m)
|
||||||
(QC m a, Q n b) | a == b -> elem m (allExtendsPlus gr n)
|
(QC (m,a), Q (n,b)) | a == b -> elem m (allExtendsPlus gr n)
|
||||||
|| elem n (allExtendsPlus gr m)
|
|| elem n (allExtendsPlus gr m)
|
||||||
(Q m a, QC n b) | a == b -> elem m (allExtendsPlus gr n)
|
(Q (m,a), QC (n,b)) | a == b -> elem m (allExtendsPlus gr n)
|
||||||
|| elem n (allExtendsPlus gr m)
|
|| elem n (allExtendsPlus gr m)
|
||||||
|
|
||||||
(Table a b, Table c d) -> alpha g a c && alpha g b d
|
(Table a b, Table c d) -> alpha g a c && alpha g b d
|
||||||
(Vr x, Vr y) -> x == y || elem (x,y) g || elem (y,x) g
|
(Vr x, Vr y) -> x == y || elem (x,y) g || elem (y,x) g
|
||||||
|
|||||||
@@ -125,8 +125,8 @@ mkType scope t =
|
|||||||
mkExp :: [Ident] -> A.Term -> C.Expr
|
mkExp :: [Ident] -> A.Term -> C.Expr
|
||||||
mkExp scope t =
|
mkExp scope t =
|
||||||
case t of
|
case t of
|
||||||
Q _ c -> C.EFun (i2i c)
|
Q (_,c) -> C.EFun (i2i c)
|
||||||
QC _ c -> C.EFun (i2i c)
|
QC (_,c) -> C.EFun (i2i c)
|
||||||
Vr x -> case lookup x (zip scope [0..]) of
|
Vr x -> case lookup x (zip scope [0..]) of
|
||||||
Just i -> C.EVar i
|
Just i -> C.EVar i
|
||||||
Nothing -> C.EMeta 0
|
Nothing -> C.EMeta 0
|
||||||
@@ -140,7 +140,7 @@ mkExp scope t =
|
|||||||
|
|
||||||
mkPatt scope p =
|
mkPatt scope p =
|
||||||
case p of
|
case p of
|
||||||
A.PP _ c ps -> let (scope',ps') = mapAccumL mkPatt scope ps
|
A.PP (_,c) ps->let (scope',ps') = mapAccumL mkPatt scope ps
|
||||||
in (scope',C.PApp (i2i c) ps')
|
in (scope',C.PApp (i2i c) ps')
|
||||||
A.PV x -> (x:scope,C.PVar (i2i x))
|
A.PV x -> (x:scope,C.PVar (i2i x))
|
||||||
A.PAs x p -> let (scope',p') = mkPatt scope p
|
A.PAs x p -> let (scope',p') = mkPatt scope p
|
||||||
@@ -180,7 +180,7 @@ mkTerm tr = case tr of
|
|||||||
Empty -> C.S []
|
Empty -> C.S []
|
||||||
App _ _ -> prtTrace tr $ C.C 66661 ---- for debugging
|
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) ->
|
Alts td tvs ->
|
||||||
C.K (C.KP (strings td) [C.Alt (strings u) (strings v) | (u,v) <- 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
|
_ -> prtTrace tr $ C.S [C.K (C.KS (render (A.ppTerm Unqualified 0 tr <+> int 66662)))] ---- for debugging
|
||||||
where
|
where
|
||||||
@@ -363,7 +363,7 @@ paramValues cgr = (labels,untyps,typs) where
|
|||||||
(_,(_,CncCat (Just (L _ ty0)) _ _)) <- jments,
|
(_,(_,CncCat (Just (L _ ty0)) _ _)) <- jments,
|
||||||
ty <- typsFrom ty0
|
ty <- typsFrom ty0
|
||||||
] ++ [
|
] ++ [
|
||||||
Q m ty |
|
Q (m,ty) |
|
||||||
(m,(ty,ResParam _ _)) <- jments
|
(m,(ty,ResParam _ _)) <- jments
|
||||||
] ++ [ty |
|
] ++ [ty |
|
||||||
(_,(_,CncFun _ (Just (L _ tr)) _)) <- jments,
|
(_,(_,CncFun _ (Just (L _ tr)) _)) <- jments,
|
||||||
@@ -377,8 +377,8 @@ paramValues cgr = (labels,untyps,typs) where
|
|||||||
_ -> []
|
_ -> []
|
||||||
|
|
||||||
isParam ty = case ty of
|
isParam ty = case ty of
|
||||||
Q _ _ -> True
|
Q _ -> True
|
||||||
QC _ _ -> True
|
QC _ -> True
|
||||||
RecType rs -> all isParam (map snd rs)
|
RecType rs -> all isParam (map snd rs)
|
||||||
_ -> False
|
_ -> False
|
||||||
|
|
||||||
@@ -436,7 +436,7 @@ type2type cgr env@(labels,untyps,typs) ty = case ty of
|
|||||||
RecType rs ->
|
RecType rs ->
|
||||||
RecType [(mkLab i, t2t t) | (i,(l, t)) <- zip [0..] (unlockTyp rs)]
|
RecType [(mkLab i, t2t t) | (i,(l, t)) <- zip [0..] (unlockTyp rs)]
|
||||||
Table pt vt -> Table (t2t pt) (t2t vt)
|
Table pt vt -> Table (t2t pt) (t2t vt)
|
||||||
QC _ _ -> look ty
|
QC _ -> look ty
|
||||||
_ -> ty
|
_ -> ty
|
||||||
where
|
where
|
||||||
t2t = type2type cgr env
|
t2t = type2type cgr env
|
||||||
@@ -447,7 +447,7 @@ type2type cgr env@(labels,untyps,typs) ty = case ty of
|
|||||||
term2term :: Ident -> SourceGrammar -> ParamEnv -> Term -> Term
|
term2term :: Ident -> SourceGrammar -> ParamEnv -> Term -> Term
|
||||||
term2term fun cgr env@(labels,untyps,typs) tr = case tr of
|
term2term fun cgr env@(labels,untyps,typs) tr = case tr of
|
||||||
App _ _ -> mkValCase (unrec tr)
|
App _ _ -> mkValCase (unrec tr)
|
||||||
QC _ _ -> mkValCase tr
|
QC _ -> mkValCase tr
|
||||||
R rs -> R [(mkLab i, (Nothing, t2t t)) |
|
R rs -> R [(mkLab i, (Nothing, t2t t)) |
|
||||||
(i,(l,(_,t))) <- zip [0..] (GM.sortRec (unlock rs))]
|
(i,(l,(_,t))) <- zip [0..] (GM.sortRec (unlock rs))]
|
||||||
P t l -> r2r tr
|
P t l -> r2r tr
|
||||||
@@ -523,7 +523,7 @@ term2term fun cgr env@(labels,untyps,typs) tr = case tr of
|
|||||||
valNum tr = maybe (valNumFV $ tryFV tr) EInt $ Map.lookup tr untyps
|
valNum tr = maybe (valNumFV $ tryFV tr) EInt $ Map.lookup tr untyps
|
||||||
where
|
where
|
||||||
tryFV tr = case GM.appForm tr of
|
tryFV tr = case GM.appForm tr of
|
||||||
(c@(QC _ _), ts) -> [GM.mkApp c ts' | ts' <- combinations (map tryFV ts)]
|
(c@(QC _), ts) -> [GM.mkApp c ts' | ts' <- combinations (map tryFV ts)]
|
||||||
(FV ts,_) -> ts
|
(FV ts,_) -> ts
|
||||||
_ -> [tr]
|
_ -> [tr]
|
||||||
valNumFV ts = case ts of
|
valNumFV ts = case ts of
|
||||||
|
|||||||
@@ -146,10 +146,10 @@ mkLinDefault gr typ = liftM (Abs Explicit varStr) $ mkDefField typ
|
|||||||
let T _ cs = mkWildCases t'
|
let T _ cs = mkWildCases t'
|
||||||
return $ T (TWild p) cs
|
return $ T (TWild p) cs
|
||||||
Sort s | s == cStr -> return $ Vr varStr
|
Sort s | s == cStr -> return $ Vr varStr
|
||||||
QC q p -> do vs <- lookupParamValues gr q p
|
QC p -> do vs <- lookupParamValues gr p
|
||||||
case vs of
|
case vs of
|
||||||
v:_ -> return v
|
v:_ -> return v
|
||||||
_ -> Bad (render (text "no parameter values given to type" <+> ppIdent p))
|
_ -> Bad (render (text "no parameter values given to type" <+> ppQIdent Qualified p))
|
||||||
RecType r -> do
|
RecType r -> do
|
||||||
let (ls,ts) = unzip r
|
let (ls,ts) = unzip r
|
||||||
ts <- mapM mkDefField ts
|
ts <- mapM mkDefField ts
|
||||||
@@ -181,7 +181,7 @@ evalPrintname gr c ppr lin =
|
|||||||
C x y -> C (oneBranch x) (oneBranch y)
|
C x y -> C (oneBranch x) (oneBranch y)
|
||||||
S x _ -> oneBranch x
|
S x _ -> oneBranch x
|
||||||
P x _ -> oneBranch x
|
P x _ -> oneBranch x
|
||||||
Alts (d,_) -> oneBranch d
|
Alts d _ -> oneBranch d
|
||||||
_ -> t
|
_ -> t
|
||||||
|
|
||||||
--- very unclean cleaner
|
--- very unclean cleaner
|
||||||
@@ -222,7 +222,7 @@ replace :: Term -> Term -> Term -> Term
|
|||||||
replace old new trm =
|
replace old new trm =
|
||||||
case trm of
|
case trm of
|
||||||
-- these are the important cases, since they can correspond to patterns
|
-- these are the important cases, since they can correspond to patterns
|
||||||
QC _ _ | trm == old -> new
|
QC _ | trm == old -> new
|
||||||
App _ _ | trm == old -> new
|
App _ _ | trm == old -> new
|
||||||
R _ | trm == old -> new
|
R _ | trm == old -> new
|
||||||
App x y -> App (replace old new x) (replace old new y)
|
App x y -> App (replace old new x) (replace old new y)
|
||||||
|
|||||||
@@ -68,7 +68,7 @@ refreshCase (p,t) = liftM2 (,) (refreshPatt p) (refresh t)
|
|||||||
refreshPatt p = case p of
|
refreshPatt p = case p of
|
||||||
PV x -> liftM PV (refVar x)
|
PV x -> liftM PV (refVar x)
|
||||||
PC c ps -> liftM (PC c) (mapM refreshPatt ps)
|
PC c ps -> liftM (PC c) (mapM refreshPatt ps)
|
||||||
PP q c ps -> liftM (PP q c) (mapM refreshPatt ps)
|
PP c ps -> liftM (PP c) (mapM refreshPatt ps)
|
||||||
PR r -> liftM PR (mapPairsM refreshPatt r)
|
PR r -> liftM PR (mapPairsM refreshPatt r)
|
||||||
PT t p' -> liftM2 PT (refresh t) (refreshPatt p')
|
PT t p' -> liftM2 PT (refresh t) (refreshPatt p')
|
||||||
|
|
||||||
|
|||||||
@@ -69,13 +69,13 @@ renameIdentTerm env@(act,imps) t =
|
|||||||
case t of
|
case t of
|
||||||
Vr c -> ident predefAbs c
|
Vr c -> ident predefAbs c
|
||||||
Cn c -> ident (\_ s -> checkError s) c
|
Cn c -> ident (\_ s -> checkError s) c
|
||||||
Q m' c | m' == cPredef {- && isInPredefined c -} -> return t
|
Q (m',c) | m' == cPredef {- && isInPredefined c -} -> return t
|
||||||
Q m' c -> do
|
Q (m',c) -> do
|
||||||
m <- checkErr (lookupErr m' qualifs)
|
m <- checkErr (lookupErr m' qualifs)
|
||||||
f <- lookupTree showIdent c m
|
f <- lookupTree showIdent c m
|
||||||
return $ f c
|
return $ f c
|
||||||
QC m' c | m' == cPredef {- && isInPredefined c -} -> return t
|
QC (m',c) | m' == cPredef {- && isInPredefined c -} -> return t
|
||||||
QC m' c -> do
|
QC (m',c) -> do
|
||||||
m <- checkErr (lookupErr m' qualifs)
|
m <- checkErr (lookupErr m' qualifs)
|
||||||
f <- lookupTree showIdent c m
|
f <- lookupTree showIdent c m
|
||||||
return $ f c
|
return $ f c
|
||||||
@@ -87,7 +87,7 @@ renameIdentTerm env@(act,imps) t =
|
|||||||
|
|
||||||
-- this facility is mainly for BWC with GF1: you need not import PredefAbs
|
-- this facility is mainly for BWC with GF1: you need not import PredefAbs
|
||||||
predefAbs c s
|
predefAbs c s
|
||||||
| isPredefCat c = return $ Q cPredefAbs c
|
| isPredefCat c = return $ Q (cPredefAbs,c)
|
||||||
| otherwise = checkError s
|
| otherwise = checkError s
|
||||||
|
|
||||||
ident alt c = case lookupTree showIdent c act of
|
ident alt c = case lookupTree showIdent c act of
|
||||||
@@ -105,12 +105,12 @@ renameIdentTerm env@(act,imps) t =
|
|||||||
|
|
||||||
info2status :: Maybe Ident -> (Ident,Info) -> StatusInfo
|
info2status :: Maybe Ident -> (Ident,Info) -> StatusInfo
|
||||||
info2status mq (c,i) = case i of
|
info2status mq (c,i) = case i of
|
||||||
AbsFun _ _ Nothing -> maybe Con QC mq
|
AbsFun _ _ Nothing -> maybe Con (curry QC) mq
|
||||||
ResValue _ -> maybe Con QC mq
|
ResValue _ -> maybe Con (curry QC) mq
|
||||||
ResParam _ _ -> maybe Con QC mq
|
ResParam _ _ -> maybe Con (curry QC) mq
|
||||||
AnyInd True m -> maybe Con (const (QC m)) mq
|
AnyInd True m -> maybe Con (const (curry QC m)) mq
|
||||||
AnyInd False m -> maybe Cn (const (Q m)) mq
|
AnyInd False m -> maybe Cn (const (curry Q m)) mq
|
||||||
_ -> maybe Cn Q mq
|
_ -> maybe Cn (curry Q) mq
|
||||||
|
|
||||||
tree2status :: OpenSpec -> BinTree Ident Info -> BinTree Ident StatusInfo
|
tree2status :: OpenSpec -> BinTree Ident Info -> BinTree Ident StatusInfo
|
||||||
tree2status o = case o of
|
tree2status o = case o of
|
||||||
@@ -192,8 +192,8 @@ renameTerm env vars = ren vars where
|
|||||||
| otherwise -> renid trm
|
| otherwise -> renid trm
|
||||||
Cn _ -> renid trm
|
Cn _ -> renid trm
|
||||||
Con _ -> renid trm
|
Con _ -> renid trm
|
||||||
Q _ _ -> renid trm
|
Q _ -> renid trm
|
||||||
QC _ _ -> renid trm
|
QC _ -> renid trm
|
||||||
T i cs -> do
|
T i cs -> do
|
||||||
i' <- case i of
|
i' <- case i of
|
||||||
TTyped ty -> liftM TTyped $ ren vs ty -- the only annotation in source
|
TTyped ty -> liftM TTyped $ ren vs ty -- the only annotation in source
|
||||||
@@ -211,7 +211,7 @@ renameTerm env vars = ren vars where
|
|||||||
P t@(Vr r) l -- Here we have $r.l$ and this is ambiguous it could be either
|
P t@(Vr r) l -- Here we have $r.l$ and this is ambiguous it could be either
|
||||||
-- record projection from variable or constant $r$ or qualified expression with module $r$
|
-- record projection from variable or constant $r$ or qualified expression with module $r$
|
||||||
| elem r vs -> return trm -- try var proj first ..
|
| elem r vs -> return trm -- try var proj first ..
|
||||||
| otherwise -> checks [ renid (Q r (label2ident l)) -- .. and qualified expression second.
|
| otherwise -> checks [ renid (Q (r,label2ident l)) -- .. and qualified expression second.
|
||||||
, renid t >>= \t -> return (P t l) -- try as a constant at the end
|
, renid t >>= \t -> return (P t l) -- try as a constant at the end
|
||||||
, checkError (text "unknown qualified constant" <+> ppTerm Unqualified 0 trm)
|
, checkError (text "unknown qualified constant" <+> ppTerm Unqualified 0 trm)
|
||||||
]
|
]
|
||||||
@@ -236,34 +236,34 @@ renamePattern env patt = case patt of
|
|||||||
PMacro c -> do
|
PMacro c -> do
|
||||||
c' <- renid $ Vr c
|
c' <- renid $ Vr c
|
||||||
case c' of
|
case c' of
|
||||||
Q p d -> renp $ PM p d
|
Q d -> renp $ PM d
|
||||||
_ -> checkError (text "unresolved pattern" <+> ppPatt Unqualified 0 patt)
|
_ -> checkError (text "unresolved pattern" <+> ppPatt Unqualified 0 patt)
|
||||||
|
|
||||||
PC c ps -> do
|
PC c ps -> do
|
||||||
c' <- renid $ Cn c
|
c' <- renid $ Cn c
|
||||||
case c' of
|
case c' of
|
||||||
QC m c -> do psvss <- mapM renp ps
|
QC c -> do psvss <- mapM renp ps
|
||||||
let (ps,vs) = unzip psvss
|
let (ps,vs) = unzip psvss
|
||||||
return (PP m c ps, concat vs)
|
return (PP c ps, concat vs)
|
||||||
Q _ _ -> checkError (text "data constructor expected but" <+> ppTerm Qualified 0 c' <+> text "is found instead")
|
Q _ -> checkError (text "data constructor expected but" <+> ppTerm Qualified 0 c' <+> text "is found instead")
|
||||||
_ -> checkError (text "unresolved data constructor" <+> ppTerm Qualified 0 c')
|
_ -> checkError (text "unresolved data constructor" <+> ppTerm Qualified 0 c')
|
||||||
|
|
||||||
PP p c ps -> do
|
PP c ps -> do
|
||||||
(QC p' c') <- renid (QC p c)
|
(QC c') <- renid (QC c)
|
||||||
psvss <- mapM renp ps
|
psvss <- mapM renp ps
|
||||||
let (ps',vs) = unzip psvss
|
let (ps',vs) = unzip psvss
|
||||||
return (PP p' c' ps', concat vs)
|
return (PP c' ps', concat vs)
|
||||||
|
|
||||||
PM p c -> do
|
PM c -> do
|
||||||
x <- renid (Q p c)
|
x <- renid (Q c)
|
||||||
(p',c') <- case x of
|
c' <- case x of
|
||||||
(Q p' c') -> return (p',c')
|
(Q c') -> return c'
|
||||||
_ -> checkError (text "not a pattern macro" <+> ppPatt Qualified 0 patt)
|
_ -> checkError (text "not a pattern macro" <+> ppPatt Qualified 0 patt)
|
||||||
return (PM p' c', [])
|
return (PM c', [])
|
||||||
|
|
||||||
PV x -> checks [ renid (Vr x) >>= \t' -> case t' of
|
PV x -> checks [ renid (Vr x) >>= \t' -> case t' of
|
||||||
QC m c -> return (PP m c [],[])
|
QC c -> return (PP c [],[])
|
||||||
_ -> checkError (text "not a constructor")
|
_ -> checkError (text "not a constructor")
|
||||||
, return (patt, [x])
|
, return (patt, [x])
|
||||||
]
|
]
|
||||||
|
|
||||||
|
|||||||
@@ -58,8 +58,8 @@ unsubexpModule sm@(i,mo)
|
|||||||
ResOper pty (Just (L loc t)) -> [(c, ResOper pty (Just (L loc (unparTerm t))))]
|
ResOper pty (Just (L loc t)) -> [(c, ResOper pty (Just (L loc (unparTerm t))))]
|
||||||
_ -> [(c,info)]
|
_ -> [(c,info)]
|
||||||
unparTerm t = case t of
|
unparTerm t = case t of
|
||||||
Q m c | isOperIdent c -> --- name convention of subexp opers
|
Q (m,c) | isOperIdent c -> --- name convention of subexp opers
|
||||||
errVal t $ liftM unparTerm $ lookupResDef gr m c
|
errVal t $ liftM unparTerm $ lookupResDef gr (m,c)
|
||||||
_ -> C.composSafeOp unparTerm t
|
_ -> C.composSafeOp unparTerm t
|
||||||
gr = M.MGrammar [sm]
|
gr = M.MGrammar [sm]
|
||||||
rebuild = buildTree . concat
|
rebuild = buildTree . concat
|
||||||
@@ -84,7 +84,7 @@ addSubexpConsts mo tree lins = do
|
|||||||
return (f,ResOper ty (Just (L loc trm')))
|
return (f,ResOper ty (Just (L loc trm')))
|
||||||
_ -> return (f,def)
|
_ -> return (f,def)
|
||||||
recomp f t = case Map.lookup t tree of
|
recomp f t = case Map.lookup t tree of
|
||||||
Just (_,id) | operIdent id /= f -> return $ Q mo (operIdent id)
|
Just (_,id) | operIdent id /= f -> return $ Q (mo, operIdent id)
|
||||||
_ -> C.composOp (recomp f) t
|
_ -> C.composOp (recomp f) t
|
||||||
|
|
||||||
list = Map.toList tree
|
list = Map.toList tree
|
||||||
|
|||||||
@@ -142,10 +142,10 @@ extendMod gr isCompl (name,cond) base old new = foldM try new $ Map.toList old
|
|||||||
Just j -> case unifyAnyInfo name i j of
|
Just j -> case unifyAnyInfo name i j of
|
||||||
Ok k -> return $ updateTree (c,k) new
|
Ok k -> return $ updateTree (c,k) new
|
||||||
Bad _ -> do (base,j) <- case j of
|
Bad _ -> do (base,j) <- case j of
|
||||||
AnyInd _ m -> lookupOrigInfo gr m c
|
AnyInd _ m -> lookupOrigInfo gr (m,c)
|
||||||
_ -> return (base,j)
|
_ -> return (base,j)
|
||||||
(name,i) <- case i of
|
(name,i) <- case i of
|
||||||
AnyInd _ m -> lookupOrigInfo gr m c
|
AnyInd _ m -> lookupOrigInfo gr (m,c)
|
||||||
_ -> return (name,i)
|
_ -> return (name,i)
|
||||||
fail $ render (text "cannot unify the information" $$
|
fail $ render (text "cannot unify the information" $$
|
||||||
nest 4 (ppJudgement Qualified (c,i)) $$
|
nest 4 (ppJudgement Qualified (c,i)) $$
|
||||||
|
|||||||
@@ -146,14 +146,14 @@ instance Binary Term where
|
|||||||
put (V x y) = putWord8 20 >> put (x,y)
|
put (V x y) = putWord8 20 >> put (x,y)
|
||||||
put (S x y) = putWord8 21 >> put (x,y)
|
put (S x y) = putWord8 21 >> put (x,y)
|
||||||
put (Let x y) = putWord8 22 >> put (x,y)
|
put (Let x y) = putWord8 22 >> put (x,y)
|
||||||
put (Q x y) = putWord8 23 >> put (x,y)
|
put (Q x) = putWord8 23 >> put x
|
||||||
put (QC x y) = putWord8 24 >> put (x,y)
|
put (QC x) = putWord8 24 >> put x
|
||||||
put (C x y) = putWord8 25 >> put (x,y)
|
put (C x y) = putWord8 25 >> put (x,y)
|
||||||
put (Glue x y) = putWord8 26 >> put (x,y)
|
put (Glue x y) = putWord8 26 >> put (x,y)
|
||||||
put (EPatt x) = putWord8 27 >> put x
|
put (EPatt x) = putWord8 27 >> put x
|
||||||
put (EPattType x) = putWord8 28 >> put x
|
put (EPattType x) = putWord8 28 >> put x
|
||||||
put (FV x) = putWord8 29 >> put x
|
put (FV x) = putWord8 29 >> put x
|
||||||
put (Alts x) = putWord8 30 >> put x
|
put (Alts x y) = putWord8 30 >> put (x,y)
|
||||||
put (Strs x) = putWord8 31 >> put x
|
put (Strs x) = putWord8 31 >> put x
|
||||||
put (ELin x y) = putWord8 32 >> put (x,y)
|
put (ELin x y) = putWord8 32 >> put (x,y)
|
||||||
|
|
||||||
@@ -182,21 +182,21 @@ instance Binary Term where
|
|||||||
20 -> get >>= \(x,y) -> return (V x y)
|
20 -> get >>= \(x,y) -> return (V x y)
|
||||||
21 -> get >>= \(x,y) -> return (S x y)
|
21 -> get >>= \(x,y) -> return (S x y)
|
||||||
22 -> get >>= \(x,y) -> return (Let x y)
|
22 -> get >>= \(x,y) -> return (Let x y)
|
||||||
23 -> get >>= \(x,y) -> return (Q x y)
|
23 -> get >>= \x -> return (Q x)
|
||||||
24 -> get >>= \(x,y) -> return (QC x y)
|
24 -> get >>= \x -> return (QC x)
|
||||||
25 -> get >>= \(x,y) -> return (C x y)
|
25 -> get >>= \(x,y) -> return (C x y)
|
||||||
26 -> get >>= \(x,y) -> return (Glue x y)
|
26 -> get >>= \(x,y) -> return (Glue x y)
|
||||||
27 -> get >>= \x -> return (EPatt x)
|
27 -> get >>= \x -> return (EPatt x)
|
||||||
28 -> get >>= \x -> return (EPattType x)
|
28 -> get >>= \x -> return (EPattType x)
|
||||||
29 -> get >>= \x -> return (FV x)
|
29 -> get >>= \x -> return (FV x)
|
||||||
30 -> get >>= \x -> return (Alts x)
|
30 -> get >>= \(x,y) -> return (Alts x y)
|
||||||
31 -> get >>= \x -> return (Strs x)
|
31 -> get >>= \x -> return (Strs x)
|
||||||
32 -> get >>= \(x,y) -> return (ELin x y)
|
32 -> get >>= \(x,y) -> return (ELin x y)
|
||||||
_ -> decodingError
|
_ -> decodingError
|
||||||
|
|
||||||
instance Binary Patt where
|
instance Binary Patt where
|
||||||
put (PC x y) = putWord8 0 >> put (x,y)
|
put (PC x y) = putWord8 0 >> put (x,y)
|
||||||
put (PP x y z) = putWord8 1 >> put (x,y,z)
|
put (PP x y) = putWord8 1 >> put (x,y)
|
||||||
put (PV x) = putWord8 2 >> put x
|
put (PV x) = putWord8 2 >> put x
|
||||||
put (PW) = putWord8 3
|
put (PW) = putWord8 3
|
||||||
put (PR x) = putWord8 4 >> put x
|
put (PR x) = putWord8 4 >> put x
|
||||||
@@ -212,12 +212,12 @@ instance Binary Patt where
|
|||||||
put (PChar) = putWord8 15
|
put (PChar) = putWord8 15
|
||||||
put (PChars x) = putWord8 16 >> put x
|
put (PChars x) = putWord8 16 >> put x
|
||||||
put (PMacro x) = putWord8 17 >> put x
|
put (PMacro x) = putWord8 17 >> put x
|
||||||
put (PM x y) = putWord8 18 >> put (x,y)
|
put (PM x) = putWord8 18 >> put x
|
||||||
put (PTilde x) = putWord8 19 >> put x
|
put (PTilde x) = putWord8 19 >> put x
|
||||||
get = do tag <- getWord8
|
get = do tag <- getWord8
|
||||||
case tag of
|
case tag of
|
||||||
0 -> get >>= \(x,y) -> return (PC x y)
|
0 -> get >>= \(x,y) -> return (PC x y)
|
||||||
1 -> get >>= \(x,y,z) -> return (PP x y z)
|
1 -> get >>= \(x,y) -> return (PP x y)
|
||||||
2 -> get >>= \x -> return (PV x)
|
2 -> get >>= \x -> return (PV x)
|
||||||
3 -> return (PW)
|
3 -> return (PW)
|
||||||
4 -> get >>= \x -> return (PR x)
|
4 -> get >>= \x -> return (PR x)
|
||||||
@@ -233,7 +233,7 @@ instance Binary Patt where
|
|||||||
15 -> return (PChar)
|
15 -> return (PChar)
|
||||||
16 -> get >>= \x -> return (PChars x)
|
16 -> get >>= \x -> return (PChars x)
|
||||||
17 -> get >>= \x -> return (PMacro x)
|
17 -> get >>= \x -> return (PMacro x)
|
||||||
18 -> get >>= \(x,y) -> return (PM x y)
|
18 -> get >>= \x -> return (PM x)
|
||||||
19 -> get >>= \x -> return (PTilde x)
|
19 -> get >>= \x -> return (PTilde x)
|
||||||
_ -> decodingError
|
_ -> decodingError
|
||||||
|
|
||||||
|
|||||||
@@ -145,8 +145,8 @@ data Term =
|
|||||||
|
|
||||||
| Let LocalDef Term -- ^ local definition: @let {t : T = a} in b@
|
| Let LocalDef Term -- ^ local definition: @let {t : T = a} in b@
|
||||||
|
|
||||||
| Q Ident Ident -- ^ qualified constant from a package
|
| Q QIdent -- ^ qualified constant from a package
|
||||||
| QC Ident Ident -- ^ qualified constructor from a package
|
| QC QIdent -- ^ qualified constructor from a package
|
||||||
|
|
||||||
| C Term Term -- ^ concatenation: @s ++ t@
|
| C Term Term -- ^ concatenation: @s ++ t@
|
||||||
| Glue Term Term -- ^ agglutination: @s + t@
|
| Glue Term Term -- ^ agglutination: @s + t@
|
||||||
@@ -159,14 +159,14 @@ data Term =
|
|||||||
|
|
||||||
| 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 ; ...}@
|
| Alts Term [(Term, Term)] -- ^ alternatives by prefix: @pre {t ; s\/c ; ...}@
|
||||||
| Strs [Term] -- ^ conditioning prefix strings: @strs {s ; ...}@
|
| Strs [Term] -- ^ conditioning prefix strings: @strs {s ; ...}@
|
||||||
|
|
||||||
deriving (Show, Eq, Ord)
|
deriving (Show, Eq, Ord)
|
||||||
|
|
||||||
data Patt =
|
data Patt =
|
||||||
PC Ident [Patt] -- ^ constructor pattern: @C p1 ... pn@ @C@
|
PC Ident [Patt] -- ^ constructor pattern: @C p1 ... pn@ @C@
|
||||||
| PP Ident Ident [Patt] -- ^ package constructor pattern: @P.C p1 ... pn@ @P.C@
|
| PP QIdent [Patt] -- ^ package constructor pattern: @P.C p1 ... pn@ @P.C@
|
||||||
| PV Ident -- ^ variable pattern: @x@
|
| PV Ident -- ^ variable pattern: @x@
|
||||||
| PW -- ^ wild card pattern: @_@
|
| PW -- ^ wild card pattern: @_@
|
||||||
| PR [(Label,Patt)] -- ^ record pattern: @{r = p ; ...}@ -- only concrete
|
| PR [(Label,Patt)] -- ^ record pattern: @{r = p ; ...}@ -- only concrete
|
||||||
@@ -188,7 +188,7 @@ data Patt =
|
|||||||
| PChar -- ^ string of length one: ?
|
| PChar -- ^ string of length one: ?
|
||||||
| PChars [Char] -- ^ character list: ["aeiou"]
|
| PChars [Char] -- ^ character list: ["aeiou"]
|
||||||
| PMacro Ident -- #p
|
| PMacro Ident -- #p
|
||||||
| PM Ident Ident -- #m.p
|
| PM QIdent -- #m.p
|
||||||
|
|
||||||
deriving (Show, Eq, Ord)
|
deriving (Show, Eq, Ord)
|
||||||
|
|
||||||
|
|||||||
@@ -21,14 +21,14 @@ module GF.Grammar.Lookup (
|
|||||||
lookupOrigInfo,
|
lookupOrigInfo,
|
||||||
allOrigInfos,
|
allOrigInfos,
|
||||||
lookupResDef,
|
lookupResDef,
|
||||||
lookupResType,
|
lookupResType,
|
||||||
lookupOverload,
|
lookupOverload,
|
||||||
lookupParamValues,
|
lookupParamValues,
|
||||||
allParamValues,
|
allParamValues,
|
||||||
lookupAbsDef,
|
lookupAbsDef,
|
||||||
lookupLincat,
|
lookupLincat,
|
||||||
lookupFunType,
|
lookupFunType,
|
||||||
lookupCatContext
|
lookupCatContext
|
||||||
) where
|
) where
|
||||||
|
|
||||||
import GF.Data.Operations
|
import GF.Data.Operations
|
||||||
@@ -58,8 +58,8 @@ lookupIdent c t =
|
|||||||
lookupIdentInfo :: ModInfo a -> Ident -> Err a
|
lookupIdentInfo :: ModInfo a -> Ident -> Err a
|
||||||
lookupIdentInfo mo i = lookupIdent i (jments mo)
|
lookupIdentInfo mo i = lookupIdent i (jments mo)
|
||||||
|
|
||||||
lookupResDef :: SourceGrammar -> Ident -> Ident -> Err Term
|
lookupResDef :: SourceGrammar -> QIdent -> Err Term
|
||||||
lookupResDef gr m c
|
lookupResDef gr (m,c)
|
||||||
| isPredefCat c = lock c defLinType
|
| isPredefCat c = lock c defLinType
|
||||||
| otherwise = look m c
|
| otherwise = look m c
|
||||||
where
|
where
|
||||||
@@ -68,7 +68,7 @@ lookupResDef gr m c
|
|||||||
info <- lookupIdentInfo mo c
|
info <- lookupIdentInfo mo c
|
||||||
case info of
|
case info of
|
||||||
ResOper _ (Just (L _ t)) -> return t
|
ResOper _ (Just (L _ t)) -> return t
|
||||||
ResOper _ Nothing -> return (Q m c)
|
ResOper _ Nothing -> return (Q (m,c))
|
||||||
CncCat (Just (L _ ty)) _ _ -> lock c ty
|
CncCat (Just (L _ ty)) _ _ -> lock c ty
|
||||||
CncCat _ _ _ -> lock c defLinType
|
CncCat _ _ _ -> lock c defLinType
|
||||||
|
|
||||||
@@ -76,12 +76,12 @@ lookupResDef gr m c
|
|||||||
CncFun _ (Just (L _ tr)) _ -> return tr
|
CncFun _ (Just (L _ tr)) _ -> return tr
|
||||||
|
|
||||||
AnyInd _ n -> look n c
|
AnyInd _ n -> look n c
|
||||||
ResParam _ _ -> return (QC m c)
|
ResParam _ _ -> return (QC (m,c))
|
||||||
ResValue _ -> return (QC m c)
|
ResValue _ -> return (QC (m,c))
|
||||||
_ -> Bad $ render (ppIdent c <+> text "is not defined in resource" <+> ppIdent m)
|
_ -> Bad $ render (ppIdent c <+> text "is not defined in resource" <+> ppIdent m)
|
||||||
|
|
||||||
lookupResType :: SourceGrammar -> Ident -> Ident -> Err Type
|
lookupResType :: SourceGrammar -> QIdent -> Err Type
|
||||||
lookupResType gr m c = do
|
lookupResType gr (m,c) = do
|
||||||
mo <- lookupModule gr m
|
mo <- lookupModule gr m
|
||||||
info <- lookupIdentInfo mo c
|
info <- lookupIdentInfo mo c
|
||||||
case info of
|
case info of
|
||||||
@@ -92,53 +92,51 @@ lookupResType gr m c = do
|
|||||||
CncFun (Just (cat,cont,val)) _ _ -> do
|
CncFun (Just (cat,cont,val)) _ _ -> do
|
||||||
val' <- lock cat val
|
val' <- lock cat val
|
||||||
return $ mkProd cont val' []
|
return $ mkProd cont val' []
|
||||||
AnyInd _ n -> lookupResType gr n c
|
AnyInd _ n -> lookupResType gr (n,c)
|
||||||
ResParam _ _ -> return typePType
|
ResParam _ _ -> return typePType
|
||||||
ResValue (L _ t) -> return t
|
ResValue (L _ t) -> return t
|
||||||
_ -> Bad $ render (ppIdent c <+> text "has no type defined in resource" <+> ppIdent m)
|
_ -> Bad $ render (ppIdent c <+> text "has no type defined in resource" <+> ppIdent m)
|
||||||
|
|
||||||
lookupOverload :: SourceGrammar -> Ident -> Ident -> Err [([Type],(Type,Term))]
|
lookupOverload :: SourceGrammar -> QIdent -> Err [([Type],(Type,Term))]
|
||||||
lookupOverload gr m c = do
|
lookupOverload gr (m,c) = do
|
||||||
mo <- lookupModule gr m
|
mo <- lookupModule gr m
|
||||||
info <- lookupIdentInfo mo c
|
info <- lookupIdentInfo mo c
|
||||||
case info of
|
case info of
|
||||||
ResOverload os tysts -> do
|
ResOverload os tysts -> do
|
||||||
tss <- mapM (\x -> lookupOverload gr x c) os
|
tss <- mapM (\x -> lookupOverload gr (x,c)) os
|
||||||
return $ [let (args,val) = typeFormCnc ty in (map (\(b,x,t) -> t) args,(val,tr)) |
|
return $ [let (args,val) = typeFormCnc ty in (map (\(b,x,t) -> t) args,(val,tr)) |
|
||||||
(L _ ty,L _ tr) <- tysts] ++
|
(L _ ty,L _ tr) <- tysts] ++
|
||||||
concat tss
|
concat tss
|
||||||
|
|
||||||
AnyInd _ n -> lookupOverload gr n c
|
AnyInd _ n -> lookupOverload gr (n,c)
|
||||||
_ -> Bad $ render (ppIdent c <+> text "is not an overloaded operation")
|
_ -> Bad $ render (ppIdent c <+> text "is not an overloaded operation")
|
||||||
|
|
||||||
-- | returns the original 'Info' and the module where it was found
|
-- | returns the original 'Info' and the module where it was found
|
||||||
lookupOrigInfo :: SourceGrammar -> Ident -> Ident -> Err (Ident,Info)
|
lookupOrigInfo :: SourceGrammar -> QIdent -> Err (Ident,Info)
|
||||||
lookupOrigInfo gr m c = do
|
lookupOrigInfo gr (m,c) = do
|
||||||
mo <- lookupModule gr m
|
mo <- lookupModule gr m
|
||||||
info <- lookupIdentInfo mo c
|
info <- lookupIdentInfo mo c
|
||||||
case info of
|
case info of
|
||||||
AnyInd _ n -> lookupOrigInfo gr n c
|
AnyInd _ n -> lookupOrigInfo gr (n,c)
|
||||||
i -> return (m,i)
|
i -> return (m,i)
|
||||||
|
|
||||||
allOrigInfos :: SourceGrammar -> Ident -> [(Ident,Info)]
|
allOrigInfos :: SourceGrammar -> Ident -> [(Ident,Info)]
|
||||||
allOrigInfos gr m = errVal [] $ do
|
allOrigInfos gr m = errVal [] $ do
|
||||||
mo <- lookupModule gr m
|
mo <- lookupModule gr m
|
||||||
return [(c,i) | (c,_) <- tree2list (jments mo), Ok (_,i) <- [look c]]
|
return [(c,i) | (c,_) <- tree2list (jments mo), Ok (_,i) <- [lookupOrigInfo gr (m,c)]]
|
||||||
where
|
|
||||||
look = lookupOrigInfo gr m
|
|
||||||
|
|
||||||
lookupParamValues :: SourceGrammar -> Ident -> Ident -> Err [Term]
|
lookupParamValues :: SourceGrammar -> QIdent -> Err [Term]
|
||||||
lookupParamValues gr m c = do
|
lookupParamValues gr c = do
|
||||||
(_,info) <- lookupOrigInfo gr m c
|
(_,info) <- lookupOrigInfo gr c
|
||||||
case info of
|
case info of
|
||||||
ResParam _ (Just pvs) -> return pvs
|
ResParam _ (Just pvs) -> return pvs
|
||||||
_ -> Bad $ render (ppIdent c <+> text "has no parameter values defined in resource" <+> ppIdent m)
|
_ -> Bad $ render (ppQIdent Qualified c <+> text "has no parameter values defined")
|
||||||
|
|
||||||
allParamValues :: SourceGrammar -> Type -> Err [Term]
|
allParamValues :: SourceGrammar -> Type -> Err [Term]
|
||||||
allParamValues cnc ptyp = case ptyp of
|
allParamValues cnc ptyp = case ptyp of
|
||||||
_ | Just n <- isTypeInts ptyp -> return [EInt i | i <- [0..n]]
|
_ | Just n <- isTypeInts ptyp -> return [EInt i | i <- [0..n]]
|
||||||
QC p c -> lookupParamValues cnc p c
|
QC c -> lookupParamValues cnc c
|
||||||
Q p c -> lookupResDef cnc p c >>= allParamValues cnc
|
Q c -> lookupResDef cnc c >>= allParamValues cnc
|
||||||
RecType r -> do
|
RecType r -> do
|
||||||
let (ls,tys) = unzip $ sortByFst r
|
let (ls,tys) = unzip $ sortByFst r
|
||||||
tss <- mapM (allParamValues cnc) tys
|
tss <- mapM (allParamValues cnc) tys
|
||||||
|
|||||||
@@ -134,7 +134,7 @@ getMetaAtom a = case a of
|
|||||||
_ -> Bad "the active node is not meta"
|
_ -> Bad "the active node is not meta"
|
||||||
-}
|
-}
|
||||||
cat2val :: Context -> Cat -> Val
|
cat2val :: Context -> Cat -> Val
|
||||||
cat2val cont cat = vClos $ mkApp (uncurry Q cat) [Meta i | i <- [1..length cont]]
|
cat2val cont cat = vClos $ mkApp (Q cat) [Meta i | i <- [1..length cont]]
|
||||||
|
|
||||||
val2cat :: Val -> Err Cat
|
val2cat :: Val -> Err Cat
|
||||||
val2cat v = liftM valCat (val2exp v)
|
val2cat v = liftM valCat (val2exp v)
|
||||||
@@ -183,7 +183,7 @@ val2expP safe v = case v of
|
|||||||
else substVal g e
|
else substVal g e
|
||||||
VClos g e -> substVal g e
|
VClos g e -> substVal g e
|
||||||
VApp f c -> liftM2 App (val2expP safe f) (val2expP safe c)
|
VApp f c -> liftM2 App (val2expP safe f) (val2expP safe c)
|
||||||
VCn c -> return $ uncurry Q c
|
VCn c -> return $ Q c
|
||||||
VGen i x -> if safe
|
VGen i x -> if safe
|
||||||
then Bad (render (text "unsafe val2exp" <+> ppValue Unqualified 0 v))
|
then Bad (render (text "unsafe val2exp" <+> ppValue Unqualified 0 v))
|
||||||
else return $ Vr $ x --- in editing, no alpha conversions presentv
|
else return $ Vr $ x --- in editing, no alpha conversions presentv
|
||||||
@@ -234,9 +234,9 @@ qualifTerm m = qualif [] where
|
|||||||
qualif xs t = case t of
|
qualif xs t = case t of
|
||||||
Abs b x t -> let x' = chV x in Abs b x' $ qualif (x':xs) t
|
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
|
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)
|
Vr x -> let x' = chV x in if (elem x' xs) then (Vr x') else (Q (m,x))
|
||||||
Cn c -> Q m c
|
Cn c -> Q (m,c)
|
||||||
Con c -> QC m c
|
Con c -> QC (m,c)
|
||||||
_ -> composSafeOp (qualif xs) t
|
_ -> composSafeOp (qualif xs) t
|
||||||
chV x = string2var $ ident2bs x
|
chV x = string2var $ ident2bs x
|
||||||
|
|
||||||
|
|||||||
@@ -41,8 +41,8 @@ typeForm t =
|
|||||||
App c a ->
|
App c a ->
|
||||||
let (_, cat, args) = typeForm c
|
let (_, cat, args) = typeForm c
|
||||||
in ([],cat,args ++ [a])
|
in ([],cat,args ++ [a])
|
||||||
Q m c -> ([],(m,c),[])
|
Q c -> ([],c,[])
|
||||||
QC m c -> ([],(m,c),[])
|
QC c -> ([],c,[])
|
||||||
Sort c -> ([],(identW, c),[])
|
Sort c -> ([],(identW, c),[])
|
||||||
_ -> error (render (text "no normal form of type" <+> ppTerm Unqualified 0 t))
|
_ -> error (render (text "no normal form of type" <+> ppTerm Unqualified 0 t))
|
||||||
|
|
||||||
@@ -61,7 +61,7 @@ valCat typ =
|
|||||||
valType :: Type -> Type
|
valType :: Type -> Type
|
||||||
valType typ =
|
valType typ =
|
||||||
let (_,cat,xx) = typeForm typ --- not optimal to do in this way
|
let (_,cat,xx) = typeForm typ --- not optimal to do in this way
|
||||||
in mkApp (uncurry Q cat) xx
|
in mkApp (Q cat) xx
|
||||||
|
|
||||||
valTypeCnc :: Type -> Type
|
valTypeCnc :: Type -> Type
|
||||||
valTypeCnc typ = snd (typeFormCnc typ)
|
valTypeCnc typ = snd (typeFormCnc typ)
|
||||||
@@ -216,11 +216,11 @@ isTypeInts _ = Nothing
|
|||||||
|
|
||||||
isPredefConstant :: Term -> Bool
|
isPredefConstant :: Term -> Bool
|
||||||
isPredefConstant t = case t of
|
isPredefConstant t = case t of
|
||||||
Q mod _ | mod == cPredef || mod == cPredefAbs -> True
|
Q (mod,_) | mod == cPredef || mod == cPredefAbs -> True
|
||||||
_ -> False
|
_ -> False
|
||||||
|
|
||||||
cnPredef :: Ident -> Term
|
cnPredef :: Ident -> Term
|
||||||
cnPredef f = Q cPredef f
|
cnPredef f = Q (cPredef,f)
|
||||||
|
|
||||||
mkSelects :: Term -> [Term] -> Term
|
mkSelects :: Term -> [Term] -> Term
|
||||||
mkSelects t tt = foldl S t tt
|
mkSelects t tt = foldl S t tt
|
||||||
@@ -333,12 +333,12 @@ term2patt trm = case termForm trm of
|
|||||||
Ok ([], Con c, aa) -> do
|
Ok ([], Con c, aa) -> do
|
||||||
aa' <- mapM term2patt aa
|
aa' <- mapM term2patt aa
|
||||||
return (PC c aa')
|
return (PC c aa')
|
||||||
Ok ([], QC p c, aa) -> do
|
Ok ([], QC c, aa) -> do
|
||||||
aa' <- mapM term2patt aa
|
aa' <- mapM term2patt aa
|
||||||
return (PP p c aa')
|
return (PP c aa')
|
||||||
|
|
||||||
Ok ([], Q p c, []) -> do
|
Ok ([], Q c, []) -> do
|
||||||
return (PM p c)
|
return (PM c)
|
||||||
|
|
||||||
Ok ([], R r, []) -> do
|
Ok ([], R r, []) -> do
|
||||||
let (ll,aa) = unzipR r
|
let (ll,aa) = unzipR r
|
||||||
@@ -381,10 +381,10 @@ patt2term pt = case pt of
|
|||||||
PV x -> Vr x
|
PV x -> Vr x
|
||||||
PW -> Vr identW --- not parsable, should not occur
|
PW -> Vr identW --- not parsable, should not occur
|
||||||
PMacro c -> Cn c
|
PMacro c -> Cn c
|
||||||
PM p c -> Q p c
|
PM c -> Q c
|
||||||
|
|
||||||
PC c pp -> mkApp (Con c) (map patt2term pp)
|
PC c pp -> mkApp (Con c) (map patt2term pp)
|
||||||
PP p c pp -> mkApp (QC p c) (map patt2term pp)
|
PP c pp -> mkApp (QC c) (map patt2term pp)
|
||||||
|
|
||||||
PR r -> R [assign l (patt2term p) | (l,p) <- r]
|
PR r -> R [assign l (patt2term p) | (l,p) <- r]
|
||||||
PT _ p -> patt2term p
|
PT _ p -> patt2term p
|
||||||
@@ -403,8 +403,8 @@ patt2term pt = case pt of
|
|||||||
|
|
||||||
redirectTerm :: Ident -> Term -> Term
|
redirectTerm :: Ident -> Term -> Term
|
||||||
redirectTerm n t = case t of
|
redirectTerm n t = case t of
|
||||||
QC _ f -> QC n f
|
QC (_,f) -> QC (n,f)
|
||||||
Q _ f -> Q n f
|
Q (_,f) -> Q (n,f)
|
||||||
_ -> composSafeOp (redirectTerm n) t
|
_ -> composSafeOp (redirectTerm n) t
|
||||||
|
|
||||||
-- | to gather ultimate cases in a table; preserves pattern list
|
-- | to gather ultimate cases in a table; preserves pattern list
|
||||||
@@ -426,7 +426,7 @@ strsFromTerm t = case t of
|
|||||||
s' <- strsFromTerm s
|
s' <- strsFromTerm s
|
||||||
t' <- strsFromTerm t
|
t' <- strsFromTerm t
|
||||||
return [glueStr x y | x <- s', y <- t']
|
return [glueStr x y | x <- s', y <- t']
|
||||||
Alts (d,vs) -> do
|
Alts d vs -> do
|
||||||
d0 <- strsFromTerm d
|
d0 <- strsFromTerm d
|
||||||
v0 <- mapM (strsFromTerm . fst) vs
|
v0 <- mapM (strsFromTerm . fst) vs
|
||||||
c0 <- mapM (strsFromTerm . snd) vs
|
c0 <- mapM (strsFromTerm . snd) vs
|
||||||
@@ -516,10 +516,10 @@ composOp co trm =
|
|||||||
do v1 <- co s1
|
do v1 <- co s1
|
||||||
v2 <- co s2
|
v2 <- co s2
|
||||||
return (Glue v1 v2)
|
return (Glue v1 v2)
|
||||||
Alts (t,aa) ->
|
Alts t aa ->
|
||||||
do t' <- co t
|
do t' <- co t
|
||||||
aa' <- mapM (pairM co) aa
|
aa' <- mapM (pairM co) aa
|
||||||
return (Alts (t',aa'))
|
return (Alts t' aa')
|
||||||
FV ts -> mapM co ts >>= return . FV
|
FV ts -> mapM co ts >>= return . FV
|
||||||
Strs tt -> mapM co tt >>= return . Strs
|
Strs tt -> mapM co tt >>= return . Strs
|
||||||
|
|
||||||
@@ -571,7 +571,7 @@ collectOp co trm = case trm of
|
|||||||
Let (x,(mt,a)) b -> maybe [] co mt ++ co a ++ co b
|
Let (x,(mt,a)) b -> maybe [] co mt ++ co a ++ co b
|
||||||
C s1 s2 -> co s1 ++ co s2
|
C s1 s2 -> co s1 ++ co s2
|
||||||
Glue 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)
|
Alts t aa -> let (x,y) = unzip aa in co t ++ concatMap co (x ++ y)
|
||||||
FV ts -> concatMap co ts
|
FV ts -> concatMap co ts
|
||||||
Strs tt -> concatMap co tt
|
Strs tt -> concatMap co tt
|
||||||
_ -> [] -- covers K, Vr, Cn, Sort
|
_ -> [] -- covers K, Vr, Cn, Sort
|
||||||
@@ -581,7 +581,7 @@ wordsInTerm :: Term -> [String]
|
|||||||
wordsInTerm trm = filter (not . null) $ case trm of
|
wordsInTerm trm = filter (not . null) $ case trm of
|
||||||
K s -> [s]
|
K s -> [s]
|
||||||
S c _ -> wo c
|
S c _ -> wo c
|
||||||
Alts (t,aa) -> wo t ++ concatMap (wo . fst) aa
|
Alts t aa -> wo t ++ concatMap (wo . fst) aa
|
||||||
_ -> collectOp wo trm
|
_ -> collectOp wo trm
|
||||||
where wo = wordsInTerm
|
where wo = wordsInTerm
|
||||||
|
|
||||||
@@ -608,8 +608,8 @@ allDependencies ism b =
|
|||||||
[(f, nub (concatMap opty (pts i))) | (f,i) <- tree2list b]
|
[(f, nub (concatMap opty (pts i))) | (f,i) <- tree2list b]
|
||||||
where
|
where
|
||||||
opersIn t = case t of
|
opersIn t = case t of
|
||||||
Q n c | ism n -> [c]
|
Q (n,c) | ism n -> [c]
|
||||||
QC n c | ism n -> [c]
|
QC (n,c) | ism n -> [c]
|
||||||
_ -> collectOp opersIn t
|
_ -> collectOp opersIn t
|
||||||
opty (Just (L _ ty)) = opersIn ty
|
opty (Just (L _ ty)) = opersIn ty
|
||||||
opty _ = []
|
opty _ = []
|
||||||
|
|||||||
@@ -417,8 +417,8 @@ Exp4
|
|||||||
in S (T annot $5) $2 }
|
in S (T annot $5) $2 }
|
||||||
| 'variants' '{' ListExp '}' { FV $3 }
|
| 'variants' '{' ListExp '}' { FV $3 }
|
||||||
| 'pre' '{' ListCase '}' {% mkAlts $3 }
|
| 'pre' '{' ListCase '}' {% mkAlts $3 }
|
||||||
| 'pre' '{' String ';' ListAltern '}' { Alts (K $3, $5) }
|
| 'pre' '{' String ';' ListAltern '}' { Alts (K $3) $5 }
|
||||||
| 'pre' '{' Ident ';' ListAltern '}' { Alts (Vr $3, $5) }
|
| 'pre' '{' Ident ';' ListAltern '}' { Alts (Vr $3) $5 }
|
||||||
| 'strs' '{' ListExp '}' { Strs $3 }
|
| 'strs' '{' ListExp '}' { Strs $3 }
|
||||||
| '#' Patt3 { EPatt $2 }
|
| '#' Patt3 { EPatt $2 }
|
||||||
| 'pattern' Exp5 { EPattType $2 }
|
| 'pattern' Exp5 { EPattType $2 }
|
||||||
@@ -468,7 +468,7 @@ Patt
|
|||||||
Patt1 :: { Patt }
|
Patt1 :: { Patt }
|
||||||
Patt1
|
Patt1
|
||||||
: Ident ListPatt { PC $1 $2 }
|
: Ident ListPatt { PC $1 $2 }
|
||||||
| Ident '.' Ident ListPatt { PP $1 $3 $4 }
|
| Ident '.' Ident ListPatt { PP ($1,$3) $4 }
|
||||||
| Patt3 '*' { PRep $1 }
|
| Patt3 '*' { PRep $1 }
|
||||||
| Patt2 { $1 }
|
| Patt2 { $1 }
|
||||||
|
|
||||||
@@ -484,10 +484,10 @@ Patt3
|
|||||||
: '?' { PChar }
|
: '?' { PChar }
|
||||||
| '[' String ']' { PChars $2 }
|
| '[' String ']' { PChars $2 }
|
||||||
| '#' Ident { PMacro $2 }
|
| '#' Ident { PMacro $2 }
|
||||||
| '#' Ident '.' Ident { PM $2 $4 }
|
| '#' Ident '.' Ident { PM ($2,$4) }
|
||||||
| '_' { PW }
|
| '_' { PW }
|
||||||
| Ident { PV $1 }
|
| Ident { PV $1 }
|
||||||
| Ident '.' Ident { PP $1 $3 [] }
|
| Ident '.' Ident { PP ($1,$3) [] }
|
||||||
| Integer { PInt $1 }
|
| Integer { PInt $1 }
|
||||||
| Double { PFloat $1 }
|
| Double { PFloat $1 }
|
||||||
| String { PString $1 }
|
| String { PString $1 }
|
||||||
@@ -705,7 +705,7 @@ mkAlts cs = case cs of
|
|||||||
_:_ -> do
|
_:_ -> do
|
||||||
def <- mkDef (last cs)
|
def <- mkDef (last cs)
|
||||||
alts <- mapM mkAlt (init cs)
|
alts <- mapM mkAlt (init cs)
|
||||||
return (Alts (def,alts))
|
return (Alts def alts)
|
||||||
_ -> fail "empty alts"
|
_ -> fail "empty alts"
|
||||||
where
|
where
|
||||||
mkDef (_,t) = return t
|
mkDef (_,t) = return t
|
||||||
@@ -720,10 +720,10 @@ mkAlts cs = case cs of
|
|||||||
PString s -> return $ Strs [K s]
|
PString s -> return $ Strs [K s]
|
||||||
PV x -> return (Vr x) --- for macros; not yet complete
|
PV x -> return (Vr x) --- for macros; not yet complete
|
||||||
PMacro x -> return (Vr x) --- for macros; not yet complete
|
PMacro x -> return (Vr x) --- for macros; not yet complete
|
||||||
PM m c -> return (Q m c) --- for macros; not yet complete
|
PM c -> return (Q c) --- for macros; not yet complete
|
||||||
_ -> fail "no strs from pattern"
|
_ -> fail "no strs from pattern"
|
||||||
|
|
||||||
mkL :: Posn -> Posn -> x -> L x
|
mkL :: Posn -> Posn -> x -> L x
|
||||||
mkL (Pn l1 _) (Pn l2 _) x = L (l1,l2) x
|
mkL (Pn l1 _) (Pn l2 _) x = L (l1,l2) x
|
||||||
|
|
||||||
}
|
}
|
||||||
|
|||||||
@@ -87,13 +87,13 @@ tryMatch (p,t) = do
|
|||||||
do matches <- mapM tryMatch (zip pp tt)
|
do matches <- mapM tryMatch (zip pp tt)
|
||||||
return (concat matches)
|
return (concat matches)
|
||||||
|
|
||||||
(PP q p pp, ([], QC r f, tt)) |
|
(PP (q,p) pp, ([], QC (r,f), tt)) |
|
||||||
-- q `eqStrIdent` r && --- not for inherited AR 10/10/2005
|
-- q `eqStrIdent` r && --- not for inherited AR 10/10/2005
|
||||||
p `eqStrIdent` f && length pp == length tt ->
|
p `eqStrIdent` f && length pp == length tt ->
|
||||||
do matches <- mapM tryMatch (zip pp tt)
|
do matches <- mapM tryMatch (zip pp tt)
|
||||||
return (concat matches)
|
return (concat matches)
|
||||||
---- hack for AppPredef bug
|
---- hack for AppPredef bug
|
||||||
(PP q p pp, ([], Q r f, tt)) |
|
(PP (q,p) pp, ([], Q (r,f), tt)) |
|
||||||
-- q `eqStrIdent` r && ---
|
-- q `eqStrIdent` r && ---
|
||||||
p `eqStrIdent` f && length pp == length tt ->
|
p `eqStrIdent` f && length pp == length tt ->
|
||||||
do matches <- mapM tryMatch (zip pp tt)
|
do matches <- mapM tryMatch (zip pp tt)
|
||||||
@@ -136,8 +136,8 @@ isInConstantForm :: Term -> Bool
|
|||||||
isInConstantForm trm = case trm of
|
isInConstantForm trm = case trm of
|
||||||
Cn _ -> True
|
Cn _ -> True
|
||||||
Con _ -> True
|
Con _ -> True
|
||||||
Q _ _ -> True
|
Q _ -> True
|
||||||
QC _ _ -> True
|
QC _ -> True
|
||||||
Abs _ _ _ -> True
|
Abs _ _ _ -> True
|
||||||
C c a -> isInConstantForm c && isInConstantForm a
|
C c a -> isInConstantForm c && isInConstantForm a
|
||||||
App c a -> isInConstantForm c && isInConstantForm a
|
App c a -> isInConstantForm c && isInConstantForm a
|
||||||
@@ -151,7 +151,7 @@ varsOfPatt :: Patt -> [Ident]
|
|||||||
varsOfPatt p = case p of
|
varsOfPatt p = case p of
|
||||||
PV x -> [x]
|
PV x -> [x]
|
||||||
PC _ ps -> concat $ map varsOfPatt ps
|
PC _ ps -> concat $ map varsOfPatt ps
|
||||||
PP _ _ ps -> concat $ map varsOfPatt ps
|
PP _ ps -> concat $ map varsOfPatt ps
|
||||||
PR r -> concat $ map (varsOfPatt . snd) r
|
PR r -> concat $ map (varsOfPatt . snd) r
|
||||||
PT _ q -> varsOfPatt q
|
PT _ q -> varsOfPatt q
|
||||||
_ -> []
|
_ -> []
|
||||||
|
|||||||
@@ -17,6 +17,7 @@ module GF.Grammar.Printer
|
|||||||
, ppValue
|
, ppValue
|
||||||
, ppConstrs
|
, ppConstrs
|
||||||
, ppPosition
|
, ppPosition
|
||||||
|
, ppQIdent
|
||||||
) where
|
) where
|
||||||
|
|
||||||
import GF.Infra.Ident
|
import GF.Infra.Ident
|
||||||
@@ -159,15 +160,15 @@ ppTerm q d (ExtR x y) = prec d 3 (ppTerm q 3 x <+> text "**" <+> ppTerm q 4 y)
|
|||||||
ppTerm q d (App x y) = prec d 4 (ppTerm q 4 x <+> ppTerm q 5 y)
|
ppTerm q d (App x y) = prec d 4 (ppTerm q 4 x <+> ppTerm q 5 y)
|
||||||
ppTerm q d (V e es) = text "table" <+> ppTerm q 6 e <+> brackets (fsep (punctuate semi (map (ppTerm q 0) es)))
|
ppTerm q d (V e es) = text "table" <+> ppTerm q 6 e <+> brackets (fsep (punctuate semi (map (ppTerm q 0) es)))
|
||||||
ppTerm q d (FV es) = text "variants" <+> braces (fsep (punctuate semi (map (ppTerm q 0) es)))
|
ppTerm q d (FV es) = text "variants" <+> braces (fsep (punctuate semi (map (ppTerm q 0) es)))
|
||||||
ppTerm q d (Alts (e,xs))=text "pre" <+> braces (ppTerm q 0 e <> semi <+> fsep (punctuate semi (map (ppAltern q) xs)))
|
ppTerm q d (Alts e xs) = text "pre" <+> braces (ppTerm q 0 e <> semi <+> fsep (punctuate semi (map (ppAltern q) xs)))
|
||||||
ppTerm q d (Strs es) = text "strs" <+> braces (fsep (punctuate semi (map (ppTerm q 0) es)))
|
ppTerm q d (Strs es) = text "strs" <+> braces (fsep (punctuate semi (map (ppTerm q 0) es)))
|
||||||
ppTerm q d (EPatt p) = prec d 4 (char '#' <+> ppPatt q 2 p)
|
ppTerm q d (EPatt p) = prec d 4 (char '#' <+> ppPatt q 2 p)
|
||||||
ppTerm q d (EPattType t)=prec d 4 (text "pattern" <+> ppTerm q 0 t)
|
ppTerm q d (EPattType t)=prec d 4 (text "pattern" <+> ppTerm q 0 t)
|
||||||
ppTerm q d (P t l) = prec d 5 (ppTerm q 5 t <> char '.' <> ppLabel l)
|
ppTerm q d (P t l) = prec d 5 (ppTerm q 5 t <> char '.' <> ppLabel l)
|
||||||
ppTerm q d (Cn id) = ppIdent id
|
ppTerm q d (Cn id) = ppIdent id
|
||||||
ppTerm q d (Vr id) = ppIdent id
|
ppTerm q d (Vr id) = ppIdent id
|
||||||
ppTerm q d (Q m id) = ppQIdent q m id
|
ppTerm q d (Q id) = ppQIdent q id
|
||||||
ppTerm q d (QC m id) = ppQIdent q m id
|
ppTerm q d (QC id) = char '!' <> ppQIdent q id <> char '!'
|
||||||
ppTerm q d (Sort id) = ppIdent id
|
ppTerm q d (Sort id) = ppIdent id
|
||||||
ppTerm q d (K s) = str s
|
ppTerm q d (K s) = str s
|
||||||
ppTerm q d (EInt n) = integer n
|
ppTerm q d (EInt n) = integer n
|
||||||
@@ -191,16 +192,16 @@ ppPatt q d (PSeq p1 p2) = prec d 0 (ppPatt q 0 p1 <+> char '+' <+> ppPatt q 1 p2
|
|||||||
ppPatt q d (PC f ps) = if null ps
|
ppPatt q d (PC f ps) = if null ps
|
||||||
then ppIdent f
|
then ppIdent f
|
||||||
else prec d 1 (ppIdent f <+> hsep (map (ppPatt q 3) ps))
|
else prec d 1 (ppIdent f <+> hsep (map (ppPatt q 3) ps))
|
||||||
ppPatt q d (PP f g ps) = if null ps
|
ppPatt q d (PP f ps) = if null ps
|
||||||
then ppQIdent q f g
|
then ppQIdent q f
|
||||||
else prec d 1 (ppQIdent q f g <+> hsep (map (ppPatt q 3) ps))
|
else prec d 1 (ppQIdent q f <+> hsep (map (ppPatt q 3) ps))
|
||||||
ppPatt q d (PRep p) = prec d 1 (ppPatt q 3 p <> char '*')
|
ppPatt q d (PRep p) = prec d 1 (ppPatt q 3 p <> char '*')
|
||||||
ppPatt q d (PAs f p) = prec d 2 (ppIdent f <> char '@' <> ppPatt q 3 p)
|
ppPatt q d (PAs f p) = prec d 2 (ppIdent f <> char '@' <> ppPatt q 3 p)
|
||||||
ppPatt q d (PNeg p) = prec d 2 (char '-' <> ppPatt q 3 p)
|
ppPatt q d (PNeg p) = prec d 2 (char '-' <> ppPatt q 3 p)
|
||||||
ppPatt q d (PChar) = char '?'
|
ppPatt q d (PChar) = char '?'
|
||||||
ppPatt q d (PChars s) = brackets (str s)
|
ppPatt q d (PChars s) = brackets (str s)
|
||||||
ppPatt q d (PMacro id) = char '#' <> ppIdent id
|
ppPatt q d (PMacro id) = char '#' <> ppIdent id
|
||||||
ppPatt q d (PM m id) = char '#' <> ppIdent m <> char '.' <> ppIdent id
|
ppPatt q d (PM id) = char '#' <> ppQIdent q id
|
||||||
ppPatt q d PW = char '_'
|
ppPatt q d PW = char '_'
|
||||||
ppPatt q d (PV id) = ppIdent id
|
ppPatt q d (PV id) = ppIdent id
|
||||||
ppPatt q d (PInt n) = integer n
|
ppPatt q d (PInt n) = integer n
|
||||||
@@ -236,7 +237,7 @@ ppDDecl q (_,id,typ)
|
|||||||
| id == identW = ppTerm q 6 typ
|
| id == identW = ppTerm q 6 typ
|
||||||
| otherwise = parens (ppIdent id <+> colon <+> ppTerm q 0 typ)
|
| otherwise = parens (ppIdent id <+> colon <+> ppTerm q 0 typ)
|
||||||
|
|
||||||
ppQIdent q m id =
|
ppQIdent q (m,id) =
|
||||||
case q of
|
case q of
|
||||||
Qualified -> ppIdent m <> char '.' <> ppIdent id
|
Qualified -> ppIdent m <> char '.' <> ppIdent id
|
||||||
Unqualified -> ppIdent id
|
Unqualified -> ppIdent id
|
||||||
|
|||||||
@@ -57,8 +57,8 @@ unify e1 e2 g =
|
|||||||
let sg = maybe e1 id (lookup s g)
|
let sg = maybe e1 id (lookup s g)
|
||||||
if (sg == Meta s) then extend g s tg else unify sg tg g
|
if (sg == Meta s) then extend g s tg else unify sg tg g
|
||||||
(t, Meta s) -> unify e2 e1 g
|
(t, Meta s) -> unify e2 e1 g
|
||||||
(Q _ a, Q _ b) | (a == b) -> return g ---- qualif?
|
(Q (_,a), Q (_,b)) | (a == b) -> return g ---- qualif?
|
||||||
(QC _ a, QC _ b) | (a == b) -> return g ----
|
(QC (_,a), QC (_,b)) | (a == b)-> return g ----
|
||||||
(Vr x, Vr y) | (x == y) -> 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
|
(Abs _ x b, Abs _ y c) -> do let c' = substTerm [x] [(y,Vr x)] c
|
||||||
unify b c' g
|
unify b c' g
|
||||||
|
|||||||
Reference in New Issue
Block a user