mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-24 03:52:50 -06:00
More woek on interfaces
This commit is contained in:
@@ -54,7 +54,7 @@ checkModule ms (name,mod) = checkIn ("checking module" +++ prt name) $ case mod
|
|||||||
|
|
||||||
MTInstance a -> do
|
MTInstance a -> do
|
||||||
ModMod abs <- checkErr $ lookupModule gr a
|
ModMod abs <- checkErr $ lookupModule gr a
|
||||||
checkCompleteInstance abs mo
|
-- checkCompleteInstance abs mo -- this is done in Rebuild
|
||||||
mapMTree (checkResInfo gr) js
|
mapMTree (checkResInfo gr) js
|
||||||
|
|
||||||
return $ (name, ModMod (Module mt st fs me ops js')) : ms
|
return $ (name, ModMod (Module mt st fs me ops js')) : ms
|
||||||
@@ -91,18 +91,6 @@ checkCompleteGrammar abs cnc = mapM_ checkWarn $
|
|||||||
then id
|
then id
|
||||||
else (("Warning: no linearization of" +++ prt f):)
|
else (("Warning: no linearization of" +++ prt f):)
|
||||||
|
|
||||||
checkCompleteInstance :: SourceRes -> SourceRes -> Check ()
|
|
||||||
checkCompleteInstance abs cnc = mapM_ checkWarn $
|
|
||||||
checkComplete [f | (f, ResOper (Yes _) _) <- abs'] cnc'
|
|
||||||
where
|
|
||||||
abs' = tree2list $ jments abs
|
|
||||||
cnc' = mapTree fst $ jments cnc
|
|
||||||
checkComplete sought given = foldr ckOne [] sought
|
|
||||||
where
|
|
||||||
ckOne f = if isInBinTree f given
|
|
||||||
then id
|
|
||||||
else (("Warning: no definition given to" +++ prt f):)
|
|
||||||
|
|
||||||
-- General Principle: only Yes-values are checked.
|
-- General Principle: only Yes-values are checked.
|
||||||
-- A May-value has always been checked in its origin module.
|
-- A May-value has always been checked in its origin module.
|
||||||
|
|
||||||
@@ -623,14 +611,14 @@ checkEqLType env t u trm = do
|
|||||||
(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 a c && alpha ((x,y):g) b d
|
||||||
|
|
||||||
---- this should be made in Rename
|
---- this should be made in Rename
|
||||||
(Q m a, Q n b) | a == b -> elem m (allExtends env n)
|
(Q m a, Q n b) | a == b -> elem m (allExtendsPlus env n)
|
||||||
|| elem n (allExtends env m)
|
|| elem n (allExtendsPlus env m)
|
||||||
(QC m a, QC n b) | a == b -> elem m (allExtends env n)
|
(QC m a, QC n b) | a == b -> elem m (allExtendsPlus env n)
|
||||||
|| elem n (allExtends env m)
|
|| elem n (allExtendsPlus env m)
|
||||||
(QC m a, Q n b) | a == b -> elem m (allExtends env n)
|
(QC m a, Q n b) | a == b -> elem m (allExtendsPlus env n)
|
||||||
|| elem n (allExtends env m)
|
|| elem n (allExtendsPlus env m)
|
||||||
(Q m a, QC n b) | a == b -> elem m (allExtends env n)
|
(Q m a, QC n b) | a == b -> elem m (allExtendsPlus env n)
|
||||||
|| elem n (allExtends env m)
|
|| elem n (allExtendsPlus env m)
|
||||||
|
|
||||||
(RecType rs, RecType ts) -> and [alpha g a b && l == k --- too strong req
|
(RecType rs, RecType ts) -> and [alpha g a b && l == k --- too strong req
|
||||||
| ((l,a),(k,b)) <- zip rs ts]
|
| ((l,a),(k,b)) <- zip rs ts]
|
||||||
|
|||||||
@@ -7,13 +7,13 @@ import PrGrammar
|
|||||||
import Update
|
import Update
|
||||||
import Lookup
|
import Lookup
|
||||||
import Modules
|
import Modules
|
||||||
import ModDeps
|
|
||||||
import ReadFiles
|
import ReadFiles
|
||||||
import ShellState
|
import ShellState
|
||||||
import MkResource
|
import MkResource
|
||||||
|
|
||||||
-- the main compiler passes
|
-- the main compiler passes
|
||||||
import GetGrammar
|
import GetGrammar
|
||||||
|
import Rebuild
|
||||||
import Rename
|
import Rename
|
||||||
import Refresh
|
import Refresh
|
||||||
import CheckGrammar
|
import CheckGrammar
|
||||||
@@ -141,6 +141,7 @@ makeSourceModule opts env@(k,gr,can) mo@(i,mi) = case mi of
|
|||||||
putp " type checking reused" $ ioeErr $ showCheckModule mos mo2
|
putp " type checking reused" $ ioeErr $ showCheckModule mos mo2
|
||||||
return $ (k,mo2)
|
return $ (k,mo2)
|
||||||
_ -> compileSourceModule opts env mo
|
_ -> compileSourceModule opts env mo
|
||||||
|
_ -> compileSourceModule opts env mo
|
||||||
where
|
where
|
||||||
putp = putPointE opts
|
putp = putPointE opts
|
||||||
|
|
||||||
@@ -150,7 +151,9 @@ compileSourceModule opts env@(k,gr,can) mo@(i,mi) = do
|
|||||||
let putp = putPointE opts
|
let putp = putPointE opts
|
||||||
mos = modules gr
|
mos = modules gr
|
||||||
|
|
||||||
mo2:_ <- putp " renaming " $ ioeErr $ renameModule mos mo
|
mo1 <- ioeErr $ rebuildModule mos mo
|
||||||
|
|
||||||
|
mo2:_ <- putp " renaming " $ ioeErr $ renameModule mos mo1
|
||||||
|
|
||||||
(mo3:_,warnings) <- putp " type checking" $ ioeErr $ showCheckModule mos mo2
|
(mo3:_,warnings) <- putp " type checking" $ ioeErr $ showCheckModule mos mo2
|
||||||
putStrE warnings
|
putStrE warnings
|
||||||
|
|||||||
@@ -80,7 +80,7 @@ extendAnyInfo n i j = errIn ("building extension for" +++ prt n) $ case (i,j) of
|
|||||||
_ -> Bad $ "cannot unify information in" ++++ show i ++++ "and" ++++ show j
|
_ -> Bad $ "cannot unify information in" ++++ show i ++++ "and" ++++ show j
|
||||||
|
|
||||||
|
|
||||||
-- opers declared in one module and defined in an extension are a special case
|
-- opers declared in an interface and defined in an instance are a special case
|
||||||
|
|
||||||
extendResOper n mt1 m1 mt2 m2 = case (m1,m2) of
|
extendResOper n mt1 m1 mt2 m2 = case (m1,m2) of
|
||||||
(Nope,_) -> return $ ResOper (strip mt1) m2
|
(Nope,_) -> return $ ResOper (strip mt1) m2
|
||||||
|
|||||||
@@ -69,7 +69,7 @@ moduleDeps ms = mapM deps ms where
|
|||||||
_ -> return []
|
_ -> return []
|
||||||
testErr (all (compatMType ety) ests) "inappropriate extension module type"
|
testErr (all (compatMType ety) ests) "inappropriate extension module type"
|
||||||
osts <- mapM (lookupModuleType gr . openedModule) os
|
osts <- mapM (lookupModuleType gr . openedModule) os
|
||||||
testErr (all (==oty) osts) "inappropriate open module type"
|
testErr (all (compatOType oty) osts) "inappropriate open module type"
|
||||||
let ab = case it of
|
let ab = case it of
|
||||||
IdentM _ (MTConcrete a) -> [IdentM a MTAbstract]
|
IdentM _ (MTConcrete a) -> [IdentM a MTAbstract]
|
||||||
_ -> [] ----
|
_ -> [] ----
|
||||||
@@ -77,12 +77,41 @@ moduleDeps ms = mapM deps ms where
|
|||||||
[IdentM e ety | Just e <- [es]] ++
|
[IdentM e ety | Just e <- [es]] ++
|
||||||
[IdentM (openedModule o) oty | o <- os])
|
[IdentM (openedModule o) oty | o <- os])
|
||||||
|
|
||||||
-- check for superficial compatibility, not submodule relation etc
|
-- check for superficial compatibility, not submodule relation etc: what can be extended
|
||||||
compatMType mt0 mt = case (mt0,mt) of
|
compatMType mt0 mt = case (mt0,mt) of
|
||||||
(MTConcrete _, MTConcrete _) -> True
|
(MTConcrete _, MTConcrete _) -> True
|
||||||
(MTInstance _, MTInstance _) -> True
|
(MTInstance _, MTInstance _) -> True
|
||||||
(MTReuse _, MTReuse _) -> True
|
(MTReuse _, MTReuse _) -> True
|
||||||
---- some more
|
---- some more
|
||||||
_ -> mt0 == mt
|
_ -> mt0 == mt
|
||||||
|
-- in the same way; this defines what can be opened
|
||||||
|
compatOType mt0 mt = case mt0 of
|
||||||
|
MTAbstract -> mt == MTAbstract
|
||||||
|
MTTransfer _ _ -> mt == MTAbstract
|
||||||
|
_ -> case mt of
|
||||||
|
MTResource -> True
|
||||||
|
MTReuse _ -> True
|
||||||
|
MTInterface -> True
|
||||||
|
MTInstance _ -> True
|
||||||
|
_ -> False
|
||||||
|
|
||||||
gr = MGrammar ms --- hack
|
gr = MGrammar ms --- hack
|
||||||
|
|
||||||
|
openInterfaces :: Dependencies -> Ident -> Err [Ident]
|
||||||
|
openInterfaces ds m = do
|
||||||
|
let deps = [(i,ds) | (IdentM i _,ds) <- ds]
|
||||||
|
let more (c,_) = [(i,mt) | Just is <- [lookup c deps], IdentM i mt <- is]
|
||||||
|
let mods = iterFix (concatMap more) (more (m,undefined))
|
||||||
|
return $ [i | (i,MTInterface) <- mods]
|
||||||
|
|
||||||
|
{-
|
||||||
|
-- to test
|
||||||
|
exampleDeps = [
|
||||||
|
(ir "Nat",[ii "Gen", ir "Adj"]),
|
||||||
|
(ir "Adj",[ii "Num", ii "Gen", ir "Nou"]),
|
||||||
|
(ir "Nou",[ii "Cas"])
|
||||||
|
]
|
||||||
|
|
||||||
|
ii s = IdentM (IC s) MTInterface
|
||||||
|
ir s = IdentM (IC s) MTResource
|
||||||
|
-}
|
||||||
|
|||||||
94
src/GF/Compile/Rebuild.hs
Normal file
94
src/GF/Compile/Rebuild.hs
Normal file
@@ -0,0 +1,94 @@
|
|||||||
|
module Rebuild where
|
||||||
|
|
||||||
|
import Grammar
|
||||||
|
import ModDeps
|
||||||
|
import PrGrammar
|
||||||
|
import Lookup
|
||||||
|
import Extend
|
||||||
|
import Macros
|
||||||
|
|
||||||
|
import Ident
|
||||||
|
import Modules
|
||||||
|
import Operations
|
||||||
|
|
||||||
|
-- rebuilding instance + interface, and "with" modules, prior to renaming. AR 24/10/2003
|
||||||
|
|
||||||
|
rebuildModule :: [SourceModule] -> SourceModule -> Err SourceModule
|
||||||
|
rebuildModule ms mo@(i,mi) = do
|
||||||
|
let gr = MGrammar ms
|
||||||
|
deps <- moduleDeps ms
|
||||||
|
is <- openInterfaces deps i
|
||||||
|
mi' <- case mi of
|
||||||
|
|
||||||
|
-- add the interface type signatures into an instance module
|
||||||
|
ModMod m -> do
|
||||||
|
testErr (null is || mstatus m == MSIncomplete)
|
||||||
|
("module" +++ prt i +++ "must be declared incomplete")
|
||||||
|
mi' <- case mtype m of
|
||||||
|
MTInstance i0 -> do
|
||||||
|
m0 <- lookupModule gr i0
|
||||||
|
m' <- case m0 of
|
||||||
|
ModMod m1 | mtype m1 == MTInterface -> do
|
||||||
|
---- checkCompleteInstance m1 m -- do this later, in CheckGrammar
|
||||||
|
js' <- extendMod i (jments m1) (jments m)
|
||||||
|
return $ replaceJudgements m js'
|
||||||
|
_ -> prtBad "interface expected instead of" i0
|
||||||
|
return mi -----
|
||||||
|
_ -> return mi
|
||||||
|
return mi'
|
||||||
|
|
||||||
|
-- add the instance opens to an incomplete module "with" instances
|
||||||
|
ModWith mt stat ext ops -> do
|
||||||
|
let insts = [(inf,inst) |OQualif _ inf inst <- ops]
|
||||||
|
let infs = map fst insts
|
||||||
|
let stat' = ifNull MSComplete (const MSIncomplete) [i | i <- is, notElem i infs]
|
||||||
|
testErr (stat' == MSComplete || stat == MSIncomplete)
|
||||||
|
("module" +++ prt i +++ "remains incomplete")
|
||||||
|
Module mt0 stat0 fs me ops0 js <- do
|
||||||
|
mi <- lookupModule gr ext
|
||||||
|
case mi of
|
||||||
|
ModMod m -> return m --- check compatibility of module type
|
||||||
|
_ -> prtBad "expected regular module in 'with' clause, not" ext
|
||||||
|
let ops1 = ops ++ [o | o <- ops0, notElem (openedModule o) infs]
|
||||||
|
++ [oQualif i i | i <- map snd insts] ----
|
||||||
|
--- check if me is incomplete
|
||||||
|
return $ ModMod $ Module mt0 stat' fs me ops1 (mapTree (qualifInstanceInfo insts) js)
|
||||||
|
|
||||||
|
_ -> return mi
|
||||||
|
return (i,mi')
|
||||||
|
|
||||||
|
checkCompleteInstance :: SourceRes -> SourceRes -> Err ()
|
||||||
|
checkCompleteInstance abs cnc = ifNull (return ()) (Bad . unlines) $
|
||||||
|
checkComplete [f | (f, ResOper (Yes _) _) <- abs'] cnc'
|
||||||
|
where
|
||||||
|
abs' = tree2list $ jments abs
|
||||||
|
cnc' = mapTree fst $ jments cnc
|
||||||
|
checkComplete sought given = foldr ckOne [] sought
|
||||||
|
where
|
||||||
|
ckOne f = if isInBinTree f given
|
||||||
|
then id
|
||||||
|
else (("Error: no definition given to" +++ prt f):)
|
||||||
|
|
||||||
|
qualifInstanceInfo :: [(Ident,Ident)] -> (Ident,Info) -> (Ident,Info)
|
||||||
|
qualifInstanceInfo insts (c,i) = (c,qualInfo i) where
|
||||||
|
|
||||||
|
qualInfo i = case i of
|
||||||
|
ResOper pty pt -> ResOper (qualP pty) (qualP pt)
|
||||||
|
CncCat pty pt pp -> CncCat (qualP pty) (qualP pt) (qualP pp)
|
||||||
|
CncFun mp pt pp -> CncFun mp (qualP pt) (qualP pp) ---- mp
|
||||||
|
----- ResParam (Yes ps) -> ResParam (yes (map qualParam ps))
|
||||||
|
ResValue pty -> ResValue (qualP pty)
|
||||||
|
_ -> i
|
||||||
|
qualP pt = case pt of
|
||||||
|
Yes t -> yes $ qual t
|
||||||
|
May m -> may $ qualId m
|
||||||
|
_ -> pt
|
||||||
|
qualId x = maybe x id $ lookup x insts
|
||||||
|
qual t = case t of
|
||||||
|
Q m c -> Q (qualId m) c
|
||||||
|
QC m c -> QC (qualId m) c
|
||||||
|
_ -> composSafeOp qual t
|
||||||
|
|
||||||
|
-- NB constructor patterns never appear in interfaces so we need not rename them
|
||||||
|
|
||||||
|
|
||||||
@@ -60,6 +60,9 @@ updateModule :: Ord i => Module i f t -> i -> t -> Module i f t
|
|||||||
updateModule (Module mt ms fs me ops js) i t =
|
updateModule (Module mt ms fs me ops js) i t =
|
||||||
Module mt ms fs me ops (updateTree (i,t) js)
|
Module mt ms fs me ops (updateTree (i,t) js)
|
||||||
|
|
||||||
|
replaceJudgements :: Module i f t -> BinTree (i,t) -> Module i f t
|
||||||
|
replaceJudgements (Module mt ms fs me ops _) js = Module mt ms fs me ops js
|
||||||
|
|
||||||
data MainGrammar i = MainGrammar {
|
data MainGrammar i = MainGrammar {
|
||||||
mainAbstract :: i ,
|
mainAbstract :: i ,
|
||||||
mainConcretes :: [MainConcreteSpec i]
|
mainConcretes :: [MainConcreteSpec i]
|
||||||
@@ -119,6 +122,14 @@ allExtends gr i = case lookupModule gr i of
|
|||||||
_ -> [i]
|
_ -> [i]
|
||||||
_ -> []
|
_ -> []
|
||||||
|
|
||||||
|
-- this plus that an instance extends its interface
|
||||||
|
allExtendsPlus :: (Show i,Ord i) => MGrammar i f a -> i -> [i]
|
||||||
|
allExtendsPlus gr i = case lookupModule gr i of
|
||||||
|
Ok (ModMod m) -> i : concatMap (allExtendsPlus gr) (exts m)
|
||||||
|
_ -> []
|
||||||
|
where
|
||||||
|
exts m = [j | Just j <- [extends m]] ++ [j | MTInstance j <- [mtype m]]
|
||||||
|
|
||||||
-- initial search path: the nonqualified dependencies
|
-- initial search path: the nonqualified dependencies
|
||||||
searchPathModule :: Ord i => Module i f a -> [i]
|
searchPathModule :: Ord i => Module i f a -> [i]
|
||||||
searchPathModule m = [i | OSimple _ i <- depPathModule m]
|
searchPathModule m = [i | OSimple _ i <- depPathModule m]
|
||||||
|
|||||||
@@ -74,19 +74,21 @@ transModDef x = case x of
|
|||||||
id' <- transIdent id
|
id' <- transIdent id
|
||||||
open' <- transIdent open
|
open' <- transIdent open
|
||||||
return (transResDef, GM.MTInstance open', id')
|
return (transResDef, GM.MTInstance open', id')
|
||||||
|
|
||||||
(extends', opens', defs',flags') <- case body of
|
case body of
|
||||||
MBody extends opens defs -> do
|
MBody extends opens defs -> do
|
||||||
extends' <- transExtend extends
|
extends' <- transExtend extends
|
||||||
opens' <- transOpens opens
|
opens' <- transOpens opens
|
||||||
defs0 <- mapM trDef $ getTopDefs defs
|
defs0 <- mapM trDef $ getTopDefs defs
|
||||||
defs' <- U.buildAnyTree [d | Left ds <- defs0, d <- ds]
|
defs' <- U.buildAnyTree [d | Left ds <- defs0, d <- ds]
|
||||||
flags' <- return [f | Right fs <- defs0, f <- fs]
|
flags' <- return [f | Right fs <- defs0, f <- fs]
|
||||||
return $ (extends', opens', defs',flags')
|
return $ (id', GM.ModMod (GM.Module mtyp' mstat' flags' extends' opens' defs'))
|
||||||
MReuse _ ->
|
MReuse _ -> do
|
||||||
return (Nothing,[],NT,[])
|
return (id', GM.ModMod (GM.Module mtyp' mstat' [] Nothing [] NT))
|
||||||
|
MWith m opens -> do
|
||||||
return $ (id', GM.ModMod (GM.Module mtyp' mstat' flags' extends' opens' defs'))
|
m' <- transIdent m
|
||||||
|
opens' <- mapM transOpen opens
|
||||||
|
return (id', GM.ModWith mtyp' mstat' m' opens')
|
||||||
|
|
||||||
transComplMod :: ComplMod -> GM.ModuleStatus
|
transComplMod :: ComplMod -> GM.ModuleStatus
|
||||||
transComplMod x = case x of
|
transComplMod x = case x of
|
||||||
|
|||||||
@@ -1 +1 @@
|
|||||||
module Today where today = "Thu Oct 23 17:57:21 CEST 2003"
|
module Today where today = "Fri Oct 24 16:27:10 CEST 2003"
|
||||||
|
|||||||
Reference in New Issue
Block a user