GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-08-19 10:46:22 -06:00
Code Issues Packages Projects Releases Wiki Activity

Merge branch 'majestic' of github.com:krangelov/gf-core into majestic

Browse Source
This commit is contained in:
Krasimir Angelov
2025-06-06 16:55:22 +00:00
parent 04639d2c6b a0faa48537
commit 6664914b7e
11 changed files with 1445 additions and 2182 deletions
Download Patch File Download Diff File Expand all files Collapse all files
src/compiler/api/GF/Command/SourceCommands.hs
+1 -1
View File
@@ -20,7 +20,7 @@ import GF.Grammar.ShowTerm
import GF.Grammar.Lookup (allOpers,allOpersTo)
import GF.Compile.Rename(renameSourceTerm)
import GF.Compile.Compute.Concrete2(normalForm,normalFlatForm,Globals(..),stdPredef)
import GF.Compile.TypeCheck.ConcreteNew as TC(inferLType)
import GF.Compile.TypeCheck.Concrete as TC(inferLType)
import GF.Command.Abstract(Option(..),isOpt,listFlags,valueString,valStrOpts)
import GF.Command.CommandInfo
src/compiler/api/GF/Compile/CheckGrammar.hs
+2 -3
View File
@@ -27,8 +27,7 @@ import GF.Infra.Ident
import GF.Infra.Option
import GF.Compile.TypeCheck.Abstract
import GF.Compile.TypeCheck.Concrete(ppType)
import GF.Compile.TypeCheck.ConcreteNew(checkLType,inferLType)
import GF.Compile.TypeCheck.Concrete(checkLType,inferLType)
import GF.Compile.Compute.Concrete2(normalForm,Globals(..),stdPredef)
import GF.Grammar
@@ -265,7 +264,7 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do
checkUniq xss = case xss of
x:y:xs
| x == y -> checkError $ "ambiguous for type" <+>
ppType (mkFunType (tail x) (head x))
ppTerm Terse 0 (mkFunType (tail x) (head x))
| otherwise -> checkUniq $ y:xs
_ -> return ()
src/compiler/api/GF/Compile/Compute/Concrete2.hs
+55 -56
View File
@@ -1,7 +1,7 @@
{-# LANGUAGE RankNTypes, BangPatterns, GeneralizedNewtypeDeriving, TupleSections #-}
module GF.Compile.Compute.Concrete2
(Env, Scope, Value(..), Variants(..), Constraint, OptionInfo(..), ChoiceMap, cleanOptions,
(Env, Scope, Value(..), Variants(..), OptionInfo(..), ChoiceMap, cleanOptions,
ConstValue(..), ConstVariants(..), Globals(..), PredefTable, EvalM,
mapVariants, unvariants, variants2consts, consts2variants,
runEvalM, runEvalMWithOpts, stdPredef, globals,
@@ -65,7 +65,7 @@ data Value
| VGen {-# UNPACK #-} !Int [Value]
| VClosure Env Choice Term
| VProd BindType Ident Value Value
| VRecType [(Label, Value)]
| VRecType [(Label, Bool, Value)]
| VR [(Label, Value)]
| VP Value Label [Value]
| VExtR Value Value
@@ -89,10 +89,7 @@ data Value
| VReset Ident (Maybe Value) Value (Maybe QIdent)
| VSymCat Int LIndex [(LIndex, (Value, Type))]
| VError Doc
-- These two constructors are only used internally
-- in the type checker.
| VCRecType [(Label, Bool, Value)]
| VCInts (Maybe Integer) (Maybe Integer)
| VInts (Maybe Integer) (Maybe Integer)
data Variants
= VarFree [Value]
@@ -109,7 +106,7 @@ unvariants (VarOpts n cs) = snd <$> cs
isCanonicalForm :: Bool -> Value -> Bool
isCanonicalForm flat (VClosure {}) = True
isCanonicalForm flat (VProd b x d cod) = isCanonicalForm flat d && isCanonicalForm flat cod
isCanonicalForm flat (VRecType fs) = all (isCanonicalForm flat . snd) fs
isCanonicalForm flat (VRecType fs) = all (\(l,_,ty) -> isCanonicalForm flat ty) fs
isCanonicalForm flat (VR {}) = True
isCanonicalForm flat (VTable d cod) = isCanonicalForm flat d && isCanonicalForm flat cod
isCanonicalForm flat (VT {}) = True
@@ -197,10 +194,13 @@ eval g env s (Abs b x t) [] = VClosure env s (Abs b x t)
eval g env s (Abs b x t) (v:vs) = eval g ((x,v):env) s t vs
eval g env s (Meta i) vs = VMeta i vs
eval g env s (ImplArg t) [] = eval g env s t []
eval g env s (Prod b x t1 t2)[] = let (s1,s2) = split s
eval g env s (Prod b x t1 t2)[]
| x == identW = let (s1,s2) = split s
in VProd b x (eval g env s1 t1 []) (eval g env s2 t2 [])
| otherwise = let (s1,s2) = split s
in VProd b x (eval g env s1 t1 []) (VClosure env s2 t2)
eval g env s (Typed t ty) vs = eval g env s t vs
eval g env s (RecType lbls) [] = VRecType (mapC (\s (lbl,ty) -> (lbl, eval g env s ty [])) s lbls)
eval g env s (RecType lbls) [] = VRecType (mapC (\s (lbl,ty) -> (lbl, True, eval g env s ty [])) s lbls)
eval g env s (R as) [] = VR (mapC (\s (lbl,(ty,t)) -> (lbl, eval g env s t [])) s as)
eval g env s (P t lbl) vs = let project (VR as) = case lookup lbl as of
Nothing -> VError ("Missing value for label" <+> pp lbl $$
@@ -214,7 +214,7 @@ eval g env s (P t lbl) vs = let project (VR as) = case lookup lbl a
eval g env s (ExtR t1 t2) [] = let (s1,s2) = split s
extend (VR as1) (VR as2) = VR (foldl (\as (lbl,v) -> update lbl v as) as1 as2)
extend (VRecType as1) (VRecType as2) = VRecType (foldl (\as (lbl,v) -> update lbl v as) as1 as2)
extend (VRecType as1) (VRecType as2) = VRecType (foldl (\as (lbl,o,v) -> update3 lbl o v as) as1 as2)
extend (VFV i fvs) v2 = VFV i (mapVariants (`extend` v2) fvs)
extend v1 (VFV i fvs) = VFV i (mapVariants (v1 `extend`) fvs)
extend (VMeta i vs) v2 = VSusp i (\v -> extend (apply g v vs) v2) []
@@ -348,7 +348,8 @@ evalPredef g@(Gl gr pds) c n args =
stdPredef :: Globals -> PredefTable
stdPredef g = Map.fromList
[(cLength, pdArity 1 $\ \g c [v] -> fmap (VInt . genericLength) (value2string g v))
[(cInts, pdArity 1 $\ \g c vs -> Const (case vs of {[VInt i] -> VInts (Just i) (Just i); vs -> VApp c (cPredef,cInts) vs}))
,(cLength, pdArity 1 $\ \g c [v] -> fmap (VInt . genericLength) (value2string g v))
,(cTake, pdArity 2 $\ \g c [v1,v2] -> fmap string2value (liftA2 genericTake (value2int g v1) (value2string g v2)))
,(cDrop, pdArity 2 $\ \g c [v1,v2] -> fmap string2value (liftA2 genericDrop (value2int g v1) (value2string g v2)))
,(cTk, pdArity 2 $\ \g c [v1,v2] -> fmap string2value (liftA2 genericTk (value2int g v1) (value2string g v2)))
@@ -391,7 +392,9 @@ bubble v = snd (bubble v)
bubble (VGen i vs) = liftL (VGen i) vs
bubble (VClosure env c t) = liftL' (\env -> VClosure env c t) env
bubble (VProd bt x v1 v2) = lift2 (VProd bt x) v1 v2
bubble (VRecType as) = liftL' VRecType as
bubble v@(VRecType lbls) =
let (union,lbls') = mapAccumL descendR Map.empty lbls
in (union, addVariants (VRecType lbls') union)
bubble (VR as) = liftL' VR as
bubble (VP v l vs) = lift1L (\v vs -> VP v l vs) v vs
bubble (VExtR v1 v2) = lift2 VExtR v1 v2
@@ -427,10 +430,7 @@ bubble v = snd (bubble v)
let (union,vs') = mapAccumL descendC Map.empty vs
in (union, addVariants (VSymCat d i0 vs') union)
bubble v@(VError _) = lift0 v
bubble v@(VCRecType lbls) =
let (union,lbls') = mapAccumL descendR Map.empty lbls
in (union, addVariants (VCRecType lbls') union)
bubble v@(VCInts _ _) = lift0 v
bubble v@(VInts _ _) = lift0 v
lift0 v = (Map.empty, v)
@@ -527,6 +527,11 @@ update lbl v (a@(lbl',_):as)
| lbl==lbl' = (lbl,v) : as
| otherwise = a : update lbl v as
update3 lbl o v [] = [(lbl,o,v)]
update3 lbl o v (a@(lbl',o',_):as)
| lbl==lbl' = (lbl,o||o',v) : as
| otherwise = a : update3 lbl o v as
patternMatch g s v0 [] = v0
patternMatch g s v0 ((env0,ps,args0,t):eqs) = match env0 ps eqs args0
where
@@ -662,11 +667,10 @@ value2term g xs v = do
[t] -> return t
ts -> return (FV ts)
type Constraint = Value
data MetaState
= Bound Scope Value
| Narrowing Type
| Residuation Scope (Maybe Constraint)
| Residuation Scope
data OptionInfo
= OptionInfo
{ optChoice :: Choice
@@ -782,7 +786,7 @@ try f select xs = EvalM (\g k state r msgs ->
newResiduation :: Scope -> EvalM MetaId
newResiduation scope = EvalM (\g k (State choices metas opts) r msgs ->
let meta_id = Map.size metas+1
in k meta_id (State choices (Map.insert meta_id (Residuation scope Nothing) metas) opts) r msgs)
in k meta_id (State choices (Map.insert meta_id (Residuation scope) metas) opts) r msgs)
getMeta :: MetaId -> EvalM MetaState
getMeta i = EvalM (\g k state r msgs ->
@@ -803,11 +807,7 @@ value2termM flat xs (VMeta i vs) = do
case mv of
Bound scope v -> do g <- globals
value2termM flat (map fst scope) (apply g v vs)
Residuation _ mb_ctr ->
case mb_ctr of
Just ctr -> do g <- globals
value2termM flat xs (apply g ctr vs)
Nothing -> foldM (\t v -> fmap (App t) (value2termM flat xs v)) (Meta i) vs
Residuation _ -> foldM (\t v -> fmap (App t) (value2termM flat xs v)) (Meta i) vs
value2termM flat xs (VSusp j k vs) =
let v = k (VGen maxBound vs)
in value2termM flat xs v
@@ -819,23 +819,19 @@ value2termM flat xs (VClosure env s (Abs b x t)) = do
x' = mkFreshVar xs x
t <- value2termM flat (x':xs) v
return (Abs b x' t)
value2termM flat xs (VProd b x v1 v2)
| x == identW = do t1 <- value2termM flat xs v1
v2 <- case v2 of
VClosure env s t2 -> do g <- globals
return (eval g env s t2 [])
v2 -> return v2
t2 <- value2termM flat xs v2
return (Prod b x t1 t2)
| otherwise = do t1 <- value2termM flat xs v1
v2 <- case v2 of
VClosure env s t2 -> do g <- globals
return (eval g ((x,VGen (length xs) []):env) s t2 [])
v2 -> return v2
t2 <- value2termM flat (x:xs) v2
return (Prod b (mkFreshVar xs x) t1 t2)
value2termM flat xs (VClosure env s t) = do
return t
value2termM flat xs (VProd b x v1 (VClosure env c2 t2)) = do
g <- globals
t1 <- value2termM flat xs v1
t2 <- value2termM flat (x:xs) (eval g ((x,VGen (length xs) []):env) c2 t2 [])
return (Prod b (mkFreshVar xs x) t1 t2)
value2termM flat xs (VProd b x v1 v2) = do
t1 <- value2termM flat xs v1
t2 <- value2termM flat xs v2
return (Prod b x t1 t2)
value2termM flat xs (VRecType lbls) = do
lbls <- mapM (\(lbl,v) -> fmap ((,) lbl) (value2termM flat xs v)) lbls
lbls <- mapM (\(lbl,_,v) -> fmap ((,) lbl) (value2termM flat xs v)) lbls
return (RecType lbls)
value2termM flat xs (VR as) = do
as <- mapM (\(lbl,v) -> fmap (\t -> (lbl,(Nothing,t))) (value2termM flat xs v)) as
@@ -978,12 +974,9 @@ value2termM flat xs (VReset ctl mb_cv v mb_qid) = do
listify mn cat (t1:ts) = do t2 <- listify mn cat ts
return (App (App (QC (mn,identS ("Cons"++cat))) t1) t2)
value2termM flat xs (VError msg) = evalError msg
value2termM flat xs (VCRecType lbls) = do
lbls <- mapM (\(lbl,_,v) -> fmap ((,) lbl) (value2termM flat xs v)) lbls
return (RecType lbls)
value2termM flat xs (VCInts Nothing Nothing) = return (App (QC (cPredef,cInts)) (Meta 0))
value2termM flat xs (VCInts (Just min) Nothing) = return (App (QC (cPredef,cInts)) (EInt min))
value2termM flat xs (VCInts _ (Just max)) = return (App (QC (cPredef,cInts)) (EInt max))
value2termM flat xs (VInts Nothing Nothing) = return (App (Q (cPredef,cInts)) (Meta 0))
value2termM flat xs (VInts (Just min) Nothing) = return (App (Q (cPredef,cInts)) (EInt min))
value2termM flat xs (VInts _ (Just max)) = return (App (Q (cPredef,cInts)) (EInt max))
value2termM flat xs v = evalError ("value2termM" <+> ppValue Unqualified 5 v)
@@ -1004,12 +997,21 @@ ppValue q d (VMeta i vs) = prec d 4 (hsep ((if i > 0 then pp "?" <> pp i else pp
ppValue q d (VSusp i k vs) = prec d 4 (hsep (pp "#susp" : (if i > 0 then pp "?" <> pp i else pp "?") : map (ppValue q 5) vs))
ppValue q d (VGen _ _) = pp "VGen"
ppValue q d (VClosure env c t) = pp "[|" <> ppTerm q 4 t <> pp "|]"
ppValue q d (VProd _ _ _ _) = pp "VProd"
ppValue q d (VRecType _) = pp "VRecType"
ppValue q d (VProd bt x a b) =
if x == identW && bt == Explicit
then prec d 0 (ppValue q 4 a <+> "->" <+> ppValue q 0 b)
else prec d 0 (parens (ppBind (bt,x) <+> ':' <+> ppValue q 0 a) <+> "->" <+> ppValue q 0 b)
ppValue q d (VRecType xs)
| q == Terse = case [cat | (l,_,_) <- xs, let (p,cat) = splitAt 5 (showIdent (label2ident l)), p == "lock_"] of
[cat] -> pp cat
_ -> doc
| otherwise = doc
where
doc = braces (fsep (punctuate ';' [l <+> (if o then ":" else ":?") <+> ppValue q 0 v | (l,o,v) <- xs]))
ppValue q d (VR _) = pp "VR"
ppValue q d (VP v l vs) = prec d 5 (hsep (ppValue q 5 v <> '.' <> l : map (ppValue q 5) vs))
ppValue q d (VExtR _ _) = pp "VExtR"
ppValue q d (VTable _ _) = pp "VTable"
ppValue q d (VTable kt vt) = prec d 0 (ppValue q 3 kt <+> "=>" <+> ppValue q 0 vt)
ppValue q d (VT t _ _ cs) = "table" <+> ppValue q 0 t <+> '{' $$
nest 2 (vcat (punctuate ';' (map (ppCase q) cs))) $$
'}'
@@ -1032,13 +1034,10 @@ ppValue q d (VStrs _) = pp "VStrs"
ppValue q d (VMarkup _ _ _) = pp "VMarkup"
ppValue q d (VSymCat i r rs) = pp '<' <> pp i <> pp ',' <> pp r <> pp '>'
ppValue q d (VError msg) = prec d 4 (pp "error" <+> ppTerm q 5 (K (show msg)))
ppValue q d (VCRecType ass) = pp "VCRecType"
ppValue q d (VCInts Nothing Nothing) = prec d 4 (pp "Ints ?")
ppValue q d (VCInts (Just min) Nothing) = prec d 4 (pp "Ints" <+> brackets (pp min <> ".."))
ppValue q d (VCInts Nothing (Just max)) = prec d 4 (pp "Ints" <+> brackets (".." <> pp max))
ppValue q d (VCInts (Just min) (Just max))
| min == max = prec d 4 (pp "Ints" <+> min)
| otherwise = prec d 4 (pp "Ints" <+> brackets (pp min <> ".." <> pp max))
ppValue q d (VInts Nothing Nothing) = prec d 4 (pp "Ints ?")
ppValue q d (VInts (Just min) Nothing) = prec d 4 (pp "Ints" <+> brackets (pp min <> ".."))
ppValue q d (VInts Nothing (Just max)) = prec d 4 (pp "Ints" <+> brackets (".." <> pp max))
ppValue q d (VInts (Just min) (Just max)) = prec d 4 (pp "Ints" <+> brackets (pp min <> ".." <> pp max))
ppAltern q (x,y) = ppValue q 0 x <+> '/' <+> ppValue q 0 y
src/compiler/api/GF/Compile/Repl.hs
+1 -1
View File
@@ -32,7 +32,7 @@ import GF.Compile.Compute.Concrete2
, ppValue
)
import GF.Compile.Rename (renameSourceTerm)
import GF.Compile.TypeCheck.ConcreteNew (inferLType)
import GF.Compile.TypeCheck.Concrete (inferLType)
import GF.Data.ErrM (Err(..))
import GF.Data.Utilities (maybeAt, orLeft)
import GF.Grammar.Grammar
src/compiler/api/GF/Compile/TypeCheck/Concrete.hs
+1369 -817
View File
File diff suppressed because it is too large Load Diff
src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs
-1298
View File
File diff suppressed because it is too large Load Diff
src/compiler/api/GF/Grammar/Macros.hs
+8
View File
@@ -443,10 +443,14 @@ collectOp :: Monoid m => (Term -> m) -> Term -> m
collectOp co trm = case trm of
App c a -> co c <> co a
Abs _ _ b -> co b
ImplArg t -> co t
Prod _ _ a b -> co a <> co b
Typed a b -> co a <> co b
Example t _ -> co t
S c a -> co c <> co a
Table a c -> co a <> co c
ExtR a c -> co a <> co c
Opts t os -> co t <> mconcatMap (\(a,b) -> co a <> co b) os
R r -> mconcatMap (\ (_,(mt,a)) -> maybe mempty co mt <> co a) r
RecType r -> mconcatMap (co . snd) r
P t i -> co t
@@ -455,9 +459,13 @@ collectOp co trm = case trm of
Let (x,(mt,a)) b -> maybe mempty co mt <> co a <> co b
C s1 s2 -> co s1 <> co s2
Glue s1 s2 -> co s1 <> co s2
EPattType t -> co t
Alts t aa -> let (x,y) = unzip aa in co t <> mconcatMap co (x <> y)
FV ts -> mconcatMap co ts
Strs tt -> mconcatMap co tt
ELincat _ t -> co t
ELin _ t -> co t
AdHocOverload ts -> mconcatMap co ts
Markup t as cs -> mconcatMap (co.snd) as <> mconcatMap co cs
Reset _ ct t _-> maybe mempty co ct <> co t
_ -> mempty -- covers K, Vr, Cn, Sort
src/compiler/api/GF/Grammar/Printer.hs
+1
View File
@@ -17,6 +17,7 @@ module GF.Grammar.Printer
, ppTerm
, ppPatt
, ppValue
, ppBind
, ppConstrs
, ppQIdent
, ppMeta
src/compiler/api/GF/Interactive.hs
+7 -4
View File
@@ -14,7 +14,8 @@ 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.Compute.Concrete(normalForm,stdPredef,Globals(..))
import qualified GF.Compile.Compute.Concrete as O(normalForm,stdPredef,Globals(..))
import GF.Compile.Compute.Concrete2(stdPredef,Globals(..))
import GF.Compile.GeneratePMCFG(pmcfgForm,type2fields)
import GF.Data.Operations (Err(..))
import GF.Data.Utilities(whenM,repeatM)
@@ -317,11 +318,12 @@ transactionCommand (CreateLin opts f mb_t is_alter) pgf mb_txnid = do
compileLinTerm sgr mo f mb_t ty = do
(t,ty) <- case mb_t of
Just t -> do t <- renameSourceTerm sgr mo (Typed t ty)
(t,ty) <- inferLType sgr [] t
let g = Gl sgr (stdPredef g)
(t,ty) <- inferLType g t
return (t,ty)
Nothing -> case lookupResDef sgr (mo,identS f) of
Ok t -> do ty <- renameSourceTerm sgr mo ty
ty <- normalForm (Gl sgr stdPredef) ty
ty <- O.normalForm (O.Gl sgr O.stdPredef) ty
return (t,ty)
Bad msg -> fail msg
let (ctxt,res_ty) = typeFormCnc ty
@@ -344,7 +346,8 @@ transactionCommand (CreateLincat opts c mb_t) pgf mb_txnid = do
compileLincatTerm sgr mo mb_t = do
t <- case mb_t of
Just t -> do t <- renameSourceTerm sgr mo t
(t,_) <- inferLType sgr [] t
let g = Gl sgr (stdPredef g)
(t,_) <- inferLType g t
return t
Nothing -> case lookupResDef sgr (mo,identS c) of
Ok t -> return t
src/compiler/api/GF/Term.hs
+1 -1
View File
@@ -9,4 +9,4 @@ module GF.Term (renameSourceTerm,
import GF.Compile.Rename
import GF.Compile.Compute.Concrete
import GF.Compile.TypeCheck.ConcreteNew
import GF.Compile.TypeCheck.Concrete
src/compiler/gf.cabal
-1
View File
@@ -127,7 +127,6 @@ library
GF.Compile.ToAPI
GF.Compile.TypeCheck.Abstract
GF.Compile.TypeCheck.Concrete
GF.Compile.TypeCheck.ConcreteNew
GF.Compile.TypeCheck.TC
GF.Compile.Update
GF.Data.BacktrackM