mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-24 03:52:50 -06:00
extend behaviour for interface and incomplete
This commit is contained in:
@@ -89,7 +89,7 @@ factor c i t = case t of
|
|||||||
|
|
||||||
--- we hope this will be fresh and don't check...
|
--- 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
|
-- we need to replace subterms
|
||||||
|
|||||||
@@ -54,7 +54,7 @@ refresh e = case e of
|
|||||||
|
|
||||||
Prod x a b -> do
|
Prod x a b -> do
|
||||||
a' <- refresh a
|
a' <- refresh a
|
||||||
x' <- refVar x
|
x' <- refVarPlus x
|
||||||
b' <- refresh b
|
b' <- refresh b
|
||||||
return $ Prod x' a' 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)
|
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 (refVarPlus 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 q c ps -> liftM (PP q c) (mapM refreshPatt ps)
|
||||||
PR r -> liftM PR (mapPairsM refreshPatt r)
|
PR r -> liftM PR (mapPairsM refreshPatt r)
|
||||||
|
|||||||
@@ -47,12 +47,15 @@ renameSourceTerm g m t = do
|
|||||||
-}
|
-}
|
||||||
|
|
||||||
renameModule :: GF -> SourceModule -> Err SourceModule
|
renameModule :: GF -> SourceModule -> Err SourceModule
|
||||||
renameModule gf sm@(name,mo) = errIn ("renaming module" +++ prt name) $ do
|
renameModule gf sm@(name,mo) = case mtype mo of
|
||||||
let gf1 = gf {gfmodules = Map.insert name mo (gfmodules gf)}
|
MTInterface -> return sm
|
||||||
let rename = renameTerm (gf1,sm) []
|
_ | not (isCompleteModule mo) -> return sm
|
||||||
mo1 <- termOpModule rename mo
|
_ -> errIn ("renaming module" +++ prt name) $ do
|
||||||
let mo2 = mo1 {mopens = [(i,i) | (_,i) <- mopens mo1]}
|
let gf1 = gf {gfmodules = Map.insert name mo (gfmodules gf)}
|
||||||
return (name,mo2)
|
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)
|
type RenameEnv = (GF,SourceModule)
|
||||||
|
|
||||||
|
|||||||
@@ -504,6 +504,7 @@ transSort x = case x of
|
|||||||
transPatt :: Patt -> Err G.Patt
|
transPatt :: Patt -> Err G.Patt
|
||||||
transPatt x = case x of
|
transPatt x = case x of
|
||||||
PW -> return wildPatt
|
PW -> return wildPatt
|
||||||
|
PV (PIdent (_,"_")) -> return wildPatt
|
||||||
PV id -> liftM G.PV $ transIdent id
|
PV id -> liftM G.PV $ transIdent id
|
||||||
PC id patts -> liftM2 G.PC (transIdent id) (mapM transPatt patts)
|
PC id patts -> liftM2 G.PC (transIdent id) (mapM transPatt patts)
|
||||||
PCon id -> liftM2 G.PC (transIdent id) (return [])
|
PCon id -> liftM2 G.PC (transIdent id) (return [])
|
||||||
@@ -529,6 +530,7 @@ transPatt x = case x of
|
|||||||
|
|
||||||
transBind :: Bind -> Err Ident
|
transBind :: Bind -> Err Ident
|
||||||
transBind x = case x of
|
transBind x = case x of
|
||||||
|
BPIdent (PIdent (_,"_")) -> return identW
|
||||||
BPIdent id -> transIdent id
|
BPIdent id -> transIdent id
|
||||||
BWild -> return identW
|
BWild -> return identW
|
||||||
|
|
||||||
|
|||||||
@@ -146,6 +146,7 @@ trt trm = case trm of
|
|||||||
T _ cc -> P.ETable (map trCase cc)
|
T _ cc -> P.ETable (map trCase cc)
|
||||||
V ty cc -> P.EVTable (trt ty) (map trt 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)
|
Table x v -> P.ETType (trt x) (trt v)
|
||||||
S f x -> P.ESelect (trt f) (trt x)
|
S f x -> P.ESelect (trt f) (trt x)
|
||||||
Let (x,(ma,b)) t ->
|
Let (x,(ma,b)) t ->
|
||||||
|
|||||||
Reference in New Issue
Block a user