Field lock in MkResource.

Field lock in MkResource.
Terrible bug fixed in Check Grammar.
This commit is contained in:
aarne
2003-11-13 08:17:28 +00:00
parent eb24522848
commit 25c8690586
8 changed files with 57 additions and 28 deletions

View File

@@ -608,7 +608,8 @@ checkEqLType env t u trm = do
": expected" +++ prt t' ++ ", inferred" +++ prt u')
where
alpha g t u = case (t,u) of --- quick hack version of TC.eqVal
(Prod x a b, Prod y c d) -> alpha g a c && alpha ((x,y):g) b d
(Prod x a b, Prod y c d) -> alpha g c a && alpha ((x,y):g) b d
-- contravariance!
---- this should be made in Rename
(Q m a, Q n b) | a == b -> elem m (allExtendsPlus env n)
@@ -620,11 +621,11 @@ checkEqLType env t u trm = do
(Q m a, QC n b) | a == b -> elem m (allExtendsPlus env n)
|| elem n (allExtendsPlus env m)
(RecType rs, RecType ts) -> and [alpha g a b && l == k --- too strong req
| ((l,a),(k,b)) <- zip rs ts]
|| -- if fails, try subtyping:
(RecType rs, RecType ts) -> -- and [alpha g a b && l == k --- too strong req
-- | ((l,a),(k,b)) <- zip rs ts]
-- || -- if fails, try subtyping:
all (\ (l,a) ->
any (\ (k,b) -> alpha g a b && l == k) ts) rs
any (\ (k,b) -> alpha g a b && l == k) ts) rs
(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

View File

@@ -78,25 +78,27 @@ perhIndir n p = case p of
extendAnyInfo :: Bool -> Ident -> Info -> Info -> Err Info
extendAnyInfo isc n i j = errIn ("building extension for" +++ prt n) $ case (i,j) of
(AbsCat mc1 mf1, AbsCat mc2 mf2) ->
liftM2 AbsCat (updn mc1 mc2) (updn mf1 mf2) --- add cstrs
liftM2 AbsCat (updn isc n mc1 mc2) (updn isc n mf1 mf2) --- add cstrs
(AbsFun mt1 md1, AbsFun mt2 md2) ->
liftM2 AbsFun (updn mt1 mt2) (updn md1 md2) --- add defs
liftM2 AbsFun (updn isc n mt1 mt2) (updn isc n md1 md2) --- add defs
(ResParam mt1, ResParam mt2) ->
liftM ResParam $ updn mt1 mt2
liftM ResParam $ updn isc n mt1 mt2
(ResValue mt1, ResValue mt2) ->
liftM ResValue $ updn mt1 mt2
liftM ResValue $ updn isc n mt1 mt2
(ResOper mt1 m1, ResOper mt2 m2) -> ---- extendResOper n mt1 m1 mt2 m2
liftM2 ResOper (updn mt1 mt2) (updn m1 m2)
liftM2 ResOper (updn isc n mt1 mt2) (updn isc n m1 m2)
(CncCat mc1 mf1 mp1, CncCat mc2 mf2 mp2) ->
liftM3 CncCat (updn mc1 mc2) (updn mf1 mf2) (updn mp1 mp2)
liftM3 CncCat (updn isc n mc1 mc2) (updn isc n mf1 mf2) (updn isc n mp1 mp2)
(CncFun m mt1 md1, CncFun _ mt2 md2) ->
liftM2 (CncFun m) (updn mt1 mt2) (updn md1 md2)
liftM2 (CncFun m) (updn isc n mt1 mt2) (updn isc n md1 md2)
---- (AnyInd _ _, ResOper _ _) -> return j ----
_ -> Bad $ "cannot unify information in" ++++ show i ++++ "and" ++++ show j
where
updn = if isc then (updatePerhaps n) else (updatePerhapsHard n)
--- where
updn isc n = if isc then (updatePerhaps n) else (updatePerhapsHard n)

View File

@@ -38,7 +38,7 @@ redModInfo (c,info) = do
c' <- redIdent c
info' <- case info of
ModMod m -> do
let isIncompl = mstatus m == MSIncomplete
let isIncompl = not $ isCompleteModule m
(e,os) <- if isIncompl then return (Nothing,[]) else redExtOpen m ----
flags <- mapM redFlag $ flags m
(a,mt) <- case mtype m of
@@ -185,6 +185,7 @@ redCTerm t = case t of
ls' = map redLabel ls
ts <- mapM (redCTerm . snd) tts
return $ G.R $ map (uncurry G.Ass) $ zip ls' ts
RecType [] -> return $ G.R [] --- comes out in parsing
P tr l -> do
tr' <- redCTerm tr
return $ G.P tr' (redLabel l)

View File

@@ -39,12 +39,17 @@ mkResDefs r a mext maext abs cnc = mapMTree mkOne abs where
mkOne (f,info) = case info of
AbsCat _ _ -> do
typ <- err (const (return defLinType)) return $ look f
return (f, ResOper (Yes typeType) (Yes typ))
typ <- err (const (return defLinType)) return $ look f
typ' <- lockRecType f typ
return (f, ResOper (Yes typeType) (Yes typ'))
AbsFun (Yes typ0) _ -> do
trm <- look f
typ <- redirTyp typ0 --- if isHardType typ0 then compute typ0 else ...
return (f, ResOper (Yes typ) (Yes trm))
testErr (not (isHardType typ0))
("cannot build reuse for function" +++ prt f +++ ":" +++ prt typ0)
typ <- redirTyp typ0
cat <- valCat typ
trm' <- unlockRecord (snd cat) trm
return (f, ResOper (Yes typ) (Yes trm'))
AnyInd b _ -> case mext of
Just ext -> return (f,AnyInd b ext)
_ -> prtBad "no indirection possible in" r
@@ -65,11 +70,24 @@ mkResDefs r a mext maext abs cnc = mapMTree mkOne abs where
_ -> prtBad "no indirection of type possible in" r
_ -> composOp redirTyp ty
{-
-- for nicer printing of type signatures: preserves synonyms if not HO/dep type
lockRecType :: Ident -> Type -> Err Type
lockRecType c t = plusRecType t $ RecType [(lockLabel c, RecType [])]
unlockRecord :: Ident -> Term -> Err Term
unlockRecord c ft = do
let (xs,t) = termFormCnc ft
t' <- plusRecord t $ R [(lockLabel c, (Just (RecType []),R []))]
return $ mkAbs xs t'
lockLabel :: Ident -> Label
lockLabel c = LIdent $ "lock_" ++ prt c ----
-- no reuse for functions of HO/dep types
isHardType t = case t of
Prod x a b -> not (isWildIdent x) || isHardType a || isHardType b
Prod x a b -> not (isWild x) || isHardType a || isHardType b
App _ _ -> True
_ -> False
-}
where
isWild x = isWildIdent x || prt x == "h_" --- produced by transl from canon

View File

@@ -154,14 +154,14 @@ mapP f p = case p of
Nope -> Nope
-- this is what happens when matching two values in the same module
unifPerhaps :: Perhaps a b -> Perhaps a b -> Err (Perhaps a b)
unifPerhaps :: (Eq a, Eq b) => Perhaps a b -> Perhaps a b -> Err (Perhaps a b)
unifPerhaps p1 p2 = case (p1,p2) of
(Nope, _) -> return p2
(_, Nope) -> return p1
_ -> Bad "update conflict"
_ -> if p1==p2 then return p1 else Bad "update conflict"
-- this is what happens when updating a module extension
updatePerhaps :: b -> Perhaps a b -> Perhaps a b -> Err (Perhaps a b)
updatePerhaps :: (Eq a,Eq b) => b -> Perhaps a b -> Perhaps a b -> Err (Perhaps a b)
updatePerhaps old p1 p2 = case (p1,p2) of
(Yes a, Nope) -> return $ may old
(May older,Nope) -> return $ may older
@@ -169,7 +169,8 @@ updatePerhaps old p1 p2 = case (p1,p2) of
_ -> unifPerhaps p1 p2
-- here the value is copied instead of referred to; used for oper types
updatePerhapsHard :: b -> Perhaps a b -> Perhaps a b -> Err (Perhaps a b)
updatePerhapsHard :: (Eq a, Eq b) => b ->
Perhaps a b -> Perhaps a b -> Err (Perhaps a b)
updatePerhapsHard old p1 p2 = case (p1,p2) of
(Yes a, Nope) -> return $ yes a
(May older,Nope) -> return $ may older

View File

@@ -135,6 +135,11 @@ termForm t = case t of
_ ->
return ([],t,[])
termFormCnc :: Term -> ([(Ident)], Term)
termFormCnc t = case t of
Abs x b -> (x:xs, t') where (xs,t') = termFormCnc b
_ -> ([],t)
appForm :: Term -> (Term, [Term])
appForm t = case t of
App c a -> (fun, args ++ [a]) where (fun, args) = appForm c

View File

@@ -118,6 +118,7 @@ trt trm = case trm of
Prod x a b | isWildIdent x -> P.EProd (P.DExp (trt a)) (trt b)
Prod x a b -> P.EProd (P.DDec [trb x] (trt a)) (trt b)
R [] -> P.ETuple [] --- to get correct parsing when read back
R r -> P.ERecord $ map trAssign r
RecType r -> P.ERecord $ map trLabelling r
ExtR x y -> P.EExtend (trt x) (trt y)

View File

@@ -1 +1 @@
module Today where today = "Tue Nov 11 17:15:59 CET 2003"
module Today where today = "Wed Nov 12 13:30:08 CET 2003"