The type signatures in Predef are no longer hard coded

This commit is contained in:
Krasimir Angelov
2024-02-06 08:36:43 +01:00
parent 9a6fc7fc9e
commit 9fd1c5da80
6 changed files with 20 additions and 114 deletions

View File

@@ -22,7 +22,6 @@ import GF.Grammar.Lookup (allOpers,allOpersTo)
import GF.Compile.Rename(renameSourceTerm)
import GF.Compile.Compute.Concrete(normalForm,Globals(..),stdPredef)
import GF.Compile.TypeCheck.Concrete as TC(inferLType,ppType)
import GF.Compile.TypeCheck.Primitives(predefMod)
import GF.Command.Abstract(Option(..),isOpt,listFlags,valueString,valStrOpts)
import GF.Command.CommandInfo
@@ -201,11 +200,8 @@ sourceCommands = Map.fromList [
| otherwise = unwords $ map prTerm ops
return $ fromString printed
show_operations os ts sgr0 = fmap fst $ runCheck $ do
let (sgr,mo) = case greatestResource sgr0 of
Nothing -> (mGrammar [predefMod], fst predefMod)
Just mo -> (sgr0,mo)
greps = map valueString (listFlags "grep" os)
show_operations os ts sgr = fmap fst $ runCheck $ do
let greps = map valueString (listFlags "grep" os)
ops <- case ts of
_:_ -> do let Right t = runP pExp (UTF8.fromString (unwords ts))
ty <- checkComputeTerm os sgr t
@@ -251,10 +247,10 @@ sourceCommands = Map.fromList [
P.putStrLn "wrote graph in file _gfdepgraph.dot"
return void
checkComputeTerm os sgr0 t =
do let (sgr,mo) = case greatestResource sgr0 of
Nothing -> (mGrammar [predefMod], fst predefMod)
Just mo -> (sgr0,mo)
checkComputeTerm os sgr t =
do mo <- case greatestResource sgr of
Nothing -> checkError (pp "No source grammar in scope")
Just mo -> return mo
t <- renameSourceTerm sgr mo t
(t,_) <- inferLType sgr [] t
fmap evalStr (normalForm (Gl sgr stdPredef) t)

View File

@@ -11,7 +11,6 @@ import GF.Grammar.Predef
import GF.Grammar.PatternMatch
import GF.Grammar.Lockfield (isLockLabel, lockRecType, unlockRecord)
import GF.Compile.Compute.Concrete(normalForm,Globals(..),stdPredef)
import GF.Compile.TypeCheck.Primitives
import Data.List
import Data.Maybe(fromMaybe,isJust,isNothing)
@@ -79,10 +78,6 @@ computeLType gr g0 t = comp (reverse [(b,x, Vr x) | (b,x,_) <- g0] ++ g0) t
inferLType :: SourceGrammar -> Context -> Term -> Check (Term, Type)
inferLType gr g trm = case trm of
Q (m,ident) | isPredef m -> termWith trm $ case typPredefined ident of
Just ty -> return ty
Nothing -> checkError ("unknown in Predef:" <+> ident)
Q ident -> checks [
termWith trm $ lookupResType gr ident >>= computeLType gr g
,
@@ -91,10 +86,6 @@ inferLType gr g trm = case trm of
checkError ("cannot infer type of constant" <+> ppTerm Unqualified 0 trm)
]
QC (m,ident) | isPredef m -> termWith trm $ case typPredefined ident of
Just ty -> return ty
Nothing -> checkError ("unknown in Predef:" <+> ident)
QC ident -> checks [
termWith trm $ lookupResType gr ident >>= computeLType gr g
,

View File

@@ -1,84 +0,0 @@
module GF.Compile.TypeCheck.Primitives(typPredefined,predefMod) where
import GF.Infra.Option
import GF.Grammar
import GF.Grammar.Predef
import qualified Data.Map as Map
typPredefined :: Ident -> Maybe Type
typPredefined f = case Map.lookup f primitives of
Just (ResOper (Just (L _ ty)) _) -> Just ty
Just (ResParam _ _) -> Just typePType
Just (ResValue (L _ ty) _) -> Just ty
_ -> Nothing
predefMod = (cPredef, modInfo)
where
modInfo = ModInfo {
mtype = MTResource,
mstatus = MSComplete,
mflags = noOptions,
mextend = [],
mwith = Nothing,
mopens = [],
mexdeps = [],
msrc = "Predef.gfo",
mseqs = Nothing,
jments = primitives
}
primitives = Map.fromList
[ (cErrorType, ResOper (Just (noLoc typeType)) Nothing)
, (cInt , ResOper (Just (noLoc typePType)) Nothing)
, (cFloat , ResOper (Just (noLoc typePType)) Nothing)
, (cInts , fun [typeInt] typePType)
, (cPBool , ResParam (Just (noLoc [(cPTrue,[]),(cPFalse,[])])) (Just ([QC (cPredef,cPTrue), QC (cPredef,cPFalse)],2)))
, (cPTrue , ResValue (noLoc typePBool) 0)
, (cPFalse , ResValue (noLoc typePBool) 1)
, (cError , fun [typeStr] typeError) -- non-can. of empty set
, (cLength , fun [typeTok] typeInt)
, (cDrop , fun [typeInt,typeTok] typeTok)
, (cTake , fun [typeInt,typeTok] typeTok)
, (cTk , fun [typeInt,typeTok] typeTok)
, (cDp , fun [typeInt,typeTok] typeTok)
, (cEqInt , fun [typeInt,typeInt] typePBool)
, (cLessInt , fun [typeInt,typeInt] typePBool)
, (cPlus , fun [typeInt,typeInt] typeInt)
, (cEqStr , fun [typeTok,typeTok] typePBool)
, (cOccur , fun [typeTok,typeTok] typePBool)
, (cOccurs , fun [typeTok,typeTok] typePBool)
, (cToUpper , fun [typeTok] typeTok)
, (cToLower , fun [typeTok] typeTok)
, (cIsUpper , fun [typeTok] typePBool)
---- "read" ->
, (cRead , ResOper (Just (noLoc (mkProd -- (P : Type) -> Tok -> P
[(Explicit,varP,typePType),(Explicit,identW,typeStr)] (Vr varP) []))) Nothing)
, (cShow , ResOper (Just (noLoc (mkProd -- (P : PType) -> P -> Tok
[(Explicit,varP,typePType),(Explicit,identW,Vr varP)] typeStr []))) Nothing)
, (cEqVal , ResOper (Just (noLoc (mkProd -- (P : PType) -> P -> P -> PBool
[(Explicit,varP,typePType),(Explicit,identW,Vr varP),(Explicit,identW,Vr varP)] typePBool []))) Nothing)
, (cToStr , ResOper (Just (noLoc (mkProd -- (L : Type) -> L -> Str
[(Explicit,varL,typeType),(Explicit,identW,Vr varL)] typeStr []))) Nothing)
, (cMapStr , ResOper (Just (noLoc (mkProd -- (L : Type) -> (Str -> Str) -> L -> L
[(Explicit,varL,typeType),(Explicit,identW,mkFunType [typeStr] typeStr),(Explicit,identW,Vr varL)] (Vr varL) []))) Nothing)
, (cNonExist , ResOper (Just (noLoc (mkProd -- Str
[] typeStr []))) Nothing)
, (cBIND , ResOper (Just (noLoc (mkProd -- Str
[] typeStr []))) Nothing)
, (cSOFT_BIND, ResOper (Just (noLoc (mkProd -- Str
[] typeStr []))) Nothing)
, (cSOFT_SPACE,ResOper (Just (noLoc (mkProd -- Str
[] typeStr []))) Nothing)
, (cCAPIT , ResOper (Just (noLoc (mkProd -- Str
[] typeStr []))) Nothing)
, (cALL_CAPIT, ResOper (Just (noLoc (mkProd -- Str
[] typeStr []))) Nothing)
]
where
fun from to = oper (mkFunType from to)
oper ty = ResOper (Just (noLoc ty)) Nothing
varL = identS "L"
varP = identS "P"

View File

@@ -18,6 +18,7 @@ module GF.Grammar
module GF.Grammar.Macros,
module GF.Grammar.Parser,
module GF.Grammar.Printer,
module GF.Grammar.Predef,
module GF.Infra.Ident
) where
@@ -26,4 +27,5 @@ import GF.Grammar.Values
import GF.Grammar.Macros
import GF.Grammar.Parser
import GF.Grammar.Printer
import GF.Grammar.Predef
import GF.Infra.Ident

View File

@@ -14,7 +14,6 @@ import GF.Command.Abstract
import GF.Command.Parse(readCommandLine,pCommand,readTransactionCommand)
import GF.Compile.Rename(renameSourceTerm)
import GF.Compile.TypeCheck.Concrete(inferLType)
import GF.Compile.TypeCheck.Primitives(predefMod)
import GF.Compile.GeneratePMCFG(pmcfgForm,type2fields)
import GF.Data.Operations (Err(..))
import GF.Data.Utilities(whenM,repeatM)
@@ -284,10 +283,10 @@ transactionCommand (CreateConcrete opts name) pgf mb_txnid = do
lift $ updatePGF pgf mb_txnid (createConcrete name (return ()))
return ()
transactionCommand (CreateLin opts f t is_alter) pgf mb_txnid = do
sgr0 <- getGrammar
let (sgr,mo) = case greatestResource sgr0 of
Nothing -> (mGrammar [predefMod], fst predefMod)
Just mo -> (sgr0,mo)
sgr <- getGrammar
mo <- case greatestResource sgr of
Nothing -> fail "No source grammar in scope"
Just mo -> return mo
lang <- optLang pgf opts
lift $ updatePGF pgf mb_txnid $ do
mb_ty <- getFunctionType f
@@ -321,10 +320,10 @@ transactionCommand (CreateLin opts f t is_alter) pgf mb_txnid = do
mapToSequence m = Seq.fromList (map (Left . fst) (sortOn snd (Map.toList m)))
transactionCommand (CreateLincat opts c t) pgf mb_txnid = do
sgr0 <- getGrammar
let (sgr,mo) = case greatestResource sgr0 of
Nothing -> (mGrammar [predefMod], fst predefMod)
Just mo -> (sgr0,mo)
sgr <- getGrammar
mo <- case greatestResource sgr of
Nothing -> fail "No source grammar in scope"
Just mo -> return mo
lang <- optLang pgf opts
case runCheck (compileLincatTerm sgr mo t) of
Ok (fields,_)-> do lift $ updatePGF pgf mb_txnid (alterConcrete lang (createLincat c fields [] [] Seq.empty >> return ()))
@@ -383,6 +382,8 @@ moreCommands = [
exec = \ _ _ ->
do modify $ \ gfenv -> (emptyGFEnv (startOpts gfenv))
{ history=history gfenv }
opts <- gets startOpts
importInEnv readNGF opts []
return void
}),
("ph", emptyCommandInfo {
@@ -433,7 +434,8 @@ importInEnv readNGF opts files =
(RetainSource,mb_txn) -> do src <- lift $ importSource opts pgf0 files
modify $ \gfenv -> gfenv{pgfenv = (snd src,pgf0,mb_txn)}
(RetainCompiled,Nothing) -> do pgf <- lift $ importPGF pgf0
modify $ \gfenv -> gfenv{pgfenv = (emptyGrammar,pgf,Nothing)}
src <- lift $ importSource opts pgf ["prelude/Predef.gfo"]
modify $ \gfenv -> gfenv{pgfenv = (snd src,pgf,Nothing)}
_ -> fail "You must commit/rollback the transaction before loading a new grammar"
where
importPGF pgf0 =

View File

@@ -128,7 +128,6 @@ library
GF.Compile.TypeCheck.Abstract
GF.Compile.TypeCheck.Concrete
GF.Compile.TypeCheck.ConcreteNew
GF.Compile.TypeCheck.Primitives
GF.Compile.TypeCheck.TC
GF.Compile.Update
GF.Data.BacktrackM