This commit is contained in:
aarne
2004-09-23 14:41:42 +00:00
parent 6c3c14dfcf
commit 22c849351f
31 changed files with 434 additions and 211 deletions

View File

@@ -233,6 +233,9 @@ computeLType gr t = do
where
comp ty = case ty of
App (Q (IC "Predef") (IC "Ints")) _ -> return ty ---- shouldn't be needed
Q (IC "Predef") (IC "Int") -> return ty ---- shouldn't be needed
Q m c | elem c [cPredef,cPredefAbs] -> return ty
Q m ident -> checkIn ("Q" +++ show m) $ do
@@ -664,6 +667,15 @@ checkEqLType env t u trm = do
all (\ (l,a) ->
any (\ (k,b) -> alpha g a b && l == k) ts) rs
-- the following say that Ints n is a subset of Int and of Ints m
(App (Q (IC "Predef") (IC "Ints")) (EInt n),
App (Q (IC "Predef") (IC "Ints")) (EInt m)) -> m >= n
(App (Q (IC "Predef") (IC "Ints")) (EInt n),
Q (IC "Predef") (IC "Int")) -> True ---- should check size
(Q (IC "Predef") (IC "Int"),
App (Q (IC "Predef") (IC "Ints")) (EInt n)) -> True
(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
_ -> t == u

View File

@@ -165,6 +165,9 @@ redCType t = case t of
Table p v -> liftM2 G.Table (redCType p) (redCType v)
Q m c -> liftM G.Cn $ redQIdent (m,c)
QC m c -> liftM G.Cn $ redQIdent (m,c)
App (Q (IC "Predef") (IC "Ints")) (EInt n) -> return $ G.TInts (toInteger n)
Sort "Str" -> return $ G.TStr
_ -> prtBad "cannot reduce to canonical the type" t
@@ -197,6 +200,7 @@ redCTerm t = case t of
return $ G.T ty' $ map (uncurry G.Cas) $ zip (map singleton ps') ts'
S u v -> liftM2 G.S (redCTerm u) (redCTerm v)
K s -> return $ G.K (G.KS s)
EInt i -> return $ G.EInt $ toInteger i
C u v -> liftM2 G.C (redCTerm u) (redCTerm v)
FV ts -> liftM G.FV $ mapM redCTerm ts
--- Ready ss -> return $ G.Ready [redStr ss] --- obsolete
@@ -224,6 +228,7 @@ redPatt p = case p of
ts <- mapM redPatt tts
return $ G.PR $ map (uncurry G.PAss) $ zip ls' ts
PT _ q -> redPatt q
PInt i -> return $ G.PI (toInteger i)
_ -> prtBad "cannot reduce pattern" p
redLabel :: Label -> G.Label