extend behaviour for interface and incomplete

This commit is contained in:
aarne
2007-12-09 10:52:19 +00:00
parent b693ba103c
commit 6a4218e9ef
5 changed files with 15 additions and 9 deletions

View File

@@ -89,7 +89,7 @@ factor c i t = case t of
--- we hope this will be fresh and don't check...
qqIdent c i = identC ("_q" ++ prt c ++ "__" ++ show i)
qqIdent c i = identC ("_q_" ++ prt c ++ "__" ++ show i)
-- we need to replace subterms

View File

@@ -54,7 +54,7 @@ refresh e = case e of
Prod x a b -> do
a' <- refresh a
x' <- refVar x
x' <- refVarPlus x
b' <- refresh b
return $ Prod x' a' b'
@@ -79,7 +79,7 @@ refreshCase :: (Patt,Term) -> STM IdState (Patt,Term)
refreshCase (p,t) = liftM2 (,) (refreshPatt p) (refresh t)
refreshPatt p = case p of
PV x -> liftM PV (refVar x)
PV x -> liftM PV (refVarPlus x)
PC c ps -> liftM (PC c) (mapM refreshPatt ps)
PP q c ps -> liftM (PP q c) (mapM refreshPatt ps)
PR r -> liftM PR (mapPairsM refreshPatt r)

View File

@@ -47,12 +47,15 @@ renameSourceTerm g m t = do
-}
renameModule :: GF -> SourceModule -> Err SourceModule
renameModule gf sm@(name,mo) = errIn ("renaming module" +++ prt name) $ do
let gf1 = gf {gfmodules = Map.insert name mo (gfmodules gf)}
let rename = renameTerm (gf1,sm) []
mo1 <- termOpModule rename mo
let mo2 = mo1 {mopens = [(i,i) | (_,i) <- mopens mo1]}
return (name,mo2)
renameModule gf sm@(name,mo) = case mtype mo of
MTInterface -> return sm
_ | not (isCompleteModule mo) -> return sm
_ -> errIn ("renaming module" +++ prt name) $ do
let gf1 = gf {gfmodules = Map.insert name mo (gfmodules gf)}
let rename = renameTerm (gf1,sm) []
mo1 <- termOpModule rename mo
let mo2 = mo1 {mopens = nub [(i,i) | (_,i) <- mopens mo1]}
return (name,mo2)
type RenameEnv = (GF,SourceModule)

View File

@@ -504,6 +504,7 @@ transSort x = case x of
transPatt :: Patt -> Err G.Patt
transPatt x = case x of
PW -> return wildPatt
PV (PIdent (_,"_")) -> return wildPatt
PV id -> liftM G.PV $ transIdent id
PC id patts -> liftM2 G.PC (transIdent id) (mapM transPatt patts)
PCon id -> liftM2 G.PC (transIdent id) (return [])
@@ -529,6 +530,7 @@ transPatt x = case x of
transBind :: Bind -> Err Ident
transBind x = case x of
BPIdent (PIdent (_,"_")) -> return identW
BPIdent id -> transIdent id
BWild -> return identW

View File

@@ -146,6 +146,7 @@ trt trm = case trm of
T _ cc -> P.ETable (map trCase cc)
V ty cc -> P.EVTable (trt ty) (map trt cc)
Typed tr ty -> P.ETyped (trt tr) (trt ty)
Table x v -> P.ETType (trt x) (trt v)
S f x -> P.ESelect (trt f) (trt x)
Let (x,(ma,b)) t ->