GitHub/gf-core
1
0
Fork 1
mirror of https://github.com/GrammaticalFramework/gf-core.git synced 2026-04-23 19:42:50 -06:00
Code Issues Packages Projects Releases Wiki Activity

Merge pull request #179 from phantamanta44/majestic

Browse Source 
majestic: predef evaluation + option..of construct
This commit is contained in:
Krasimir Angelov
2025-04-06 17:25:16 +02:00
committed by GitHub
parent f0b42f4783 b29ec2a47a
commit aa3a03e7af
9 changed files with 634 additions and 314 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
src/compiler/api/GF/Compile/CheckGrammar.hs
View File

@@ -302,7 +302,7 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do
-- | for grammars obtained otherwise than by parsing ---- update!! -- | for grammars obtained otherwise than by parsing ---- update!!
checkReservedId :: Ident -> Check () checkReservedId :: Ident -> Check ()
checkReservedId x = checkReservedId x =
when (isReservedWord x) $ when (isReservedWord GF x) $
checkWarn ("reserved word used as identifier:" <+> x) checkWarn ("reserved word used as identifier:" <+> x)
-- auxiliaries -- auxiliaries

172
src/compiler/api/GF/Compile/Compute/Concrete.hs
View File

@@ -1,12 +1,12 @@
{-# LANGUAGE RankNTypes, BangPatterns, CPP, ExistentialQuantification, LambdaCase #-} {-# LANGUAGE RankNTypes, BangPatterns, CPP, ExistentialQuantification #-}
-- | Functions for computing the values of terms in the concrete syntax, in -- | Functions for computing the values of terms in the concrete syntax, in
-- | preparation for PMCFG generation. -- | preparation for PMCFG generation.
module GF.Compile.Compute.Concrete module GF.Compile.Compute.Concrete
( normalForm, normalFlatForm, normalStringForm ( normalForm, normalFlatForm, normalStringForm
, Value(..), Thunk, ThunkState(..), Env, Scope, showValue , Value(..), Thunk, ThunkState(..), Env, Scope, showValue, isCanonicalForm
, PredefImpl, Predef(..), PredefCombinator, ($\) , PredefImpl, Predef(..), PredefCombinator, ($\)
, pdForce, pdClosedArgs, pdArity, pdStandard , pdForce, pdCanonicalArgs, pdArity, pdStandard
, MetaThunks, Constraint, PredefTable, Globals(..), ConstValue(..) , MetaThunks, Constraint, PredefTable, Globals(..), ConstValue(..)
, EvalM(..), runEvalM, runEvalOneM, reset, try, evalError, evalWarn , EvalM(..), runEvalM, runEvalOneM, reset, try, evalError, evalWarn
, eval, apply, force, value2term, patternMatch, stdPredef , eval, apply, force, value2term, patternMatch, stdPredef
@@ -27,7 +27,7 @@ import GF.Grammar.Predef
import GF.Grammar.Lockfield(lockLabel) import GF.Grammar.Lockfield(lockLabel)
import GF.Grammar.Printer import GF.Grammar.Printer
import GF.Data.Operations(Err(..)) import GF.Data.Operations(Err(..))
import GF.Data.Utilities(splitAt',(<||>),anyM) import GF.Data.Utilities(splitAt')
import GF.Infra.CheckM import GF.Infra.CheckM
import GF.Infra.Option import GF.Infra.Option
import Data.STRef import Data.STRef
@@ -39,6 +39,7 @@ import Control.Monad.ST
import Control.Monad.ST.Unsafe import Control.Monad.ST.Unsafe
import Control.Applicative hiding (Const) import Control.Applicative hiding (Const)
import qualified Control.Monad.Fail as Fail import qualified Control.Monad.Fail as Fail
import Data.Functor ((<&>))
import qualified Data.Map as Map import qualified Data.Map as Map
import GF.Text.Pretty import GF.Text.Pretty
import PGF2.Transactions(LIndex) import PGF2.Transactions(LIndex)
@@ -143,36 +144,23 @@ showValue (VAlts _ _) = "VAlts"
showValue (VStrs _) = "VStrs" showValue (VStrs _) = "VStrs"
showValue (VSymCat _ _ _) = "VSymCat" showValue (VSymCat _ _ _) = "VSymCat"
isOpen :: [Ident] -> Term -> EvalM s Bool isCanonicalForm :: Value s -> Bool
isOpen bound (Vr x) = return $ x `notElem` bound isCanonicalForm (VClosure {}) = True
isOpen bound (App f x) = isOpen bound f <||> isOpen bound x isCanonicalForm (VProd b x d cod) = isCanonicalForm d && isCanonicalForm cod
isOpen bound (Abs b x t) = isOpen (x:bound) t isCanonicalForm (VRecType fs) = all (isCanonicalForm . snd) fs
isOpen bound (ImplArg t) = isOpen bound t isCanonicalForm (VR {}) = True
isOpen bound (Prod b x d cod) = isOpen bound d <||> isOpen (x:bound) cod isCanonicalForm (VTable d cod) = isCanonicalForm d && isCanonicalForm cod
isOpen bound (Typed t ty) = isOpen bound t isCanonicalForm (VT {}) = True
isOpen bound (Example t s) = isOpen bound t isCanonicalForm (VV {}) = True
isOpen bound (RecType fs) = anyM (isOpen bound . snd) fs isCanonicalForm (VSort {}) = True
isOpen bound (R fs) = anyM (isOpen bound . snd . snd) fs isCanonicalForm (VInt {}) = True
isOpen bound (P t f) = isOpen bound t isCanonicalForm (VFlt {}) = True
isOpen bound (ExtR t t') = isOpen bound t <||> isOpen bound t' isCanonicalForm (VStr {}) = True
isOpen bound (Table d cod) = isOpen bound d <||> isOpen bound cod isCanonicalForm VEmpty = True
isOpen bound (T (TTyped ty) cs) = isOpen bound ty <||> anyM (isOpen bound . snd) cs isCanonicalForm (VAlts d vs) = all (isCanonicalForm . snd) vs
isOpen bound (T (TWild ty) cs) = isOpen bound ty <||> anyM (isOpen bound . snd) cs isCanonicalForm (VStrs vs) = all isCanonicalForm vs
isOpen bound (T _ cs) = anyM (isOpen bound . snd) cs isCanonicalForm (VMarkup tag as vs) = all (isCanonicalForm . snd) as && all isCanonicalForm vs
isOpen bound (V ty cs) = isOpen bound ty <||> anyM (isOpen bound) cs isCanonicalForm _ = False
isOpen bound (S t x) = isOpen bound t <||> isOpen bound x
isOpen bound (Let (x,(ty,d)) t) = isOpen bound d <||> isOpen (x:bound) t
isOpen bound (C t t') = isOpen bound t <||> isOpen bound t'
isOpen bound (Glue t t') = isOpen bound t <||> isOpen bound t'
isOpen bound (EPattType ty) = isOpen bound ty
isOpen bound (ELincat c ty) = isOpen bound ty
isOpen bound (ELin c t) = isOpen bound t
isOpen bound (FV ts) = anyM (isOpen bound) ts
isOpen bound (Markup tag as ts) = anyM (isOpen bound) ts <||> anyM (isOpen bound . snd) as
isOpen bound (Reset c t) = isOpen bound t
isOpen bound (Alts d as) = isOpen bound d <||> anyM (\(x,y) -> isOpen bound x <||> isOpen bound y) as
isOpen bound (Strs ts) = anyM (isOpen bound) ts
isOpen _ _ = return False
eval env (Vr x) vs = do (tnk,depth) <- lookup x env eval env (Vr x) vs = do (tnk,depth) <- lookup x env
withVar depth $ do withVar depth $ do
@@ -238,12 +226,8 @@ eval env (S t1 t2) vs = do v1 <- eval env t1 []
v1 -> return v0 v1 -> return v0
eval env (Let (x,(_,t1)) t2) vs = do tnk <- newThunk env t1 eval env (Let (x,(_,t1)) t2) vs = do tnk <- newThunk env t1
eval ((x,tnk):env) t2 vs eval ((x,tnk):env) t2 vs
eval env t@(Q q@(m,id)) vs eval env (Q q@(m,id)) vs
| m == cPredef = do res <- evalPredef env t id vs | m == cPredef = evalPredef id vs
case res of
Const res -> return res
RunTime -> return (VApp q vs)
NonExist -> return (VApp (cPredef,cNonExist) [])
| otherwise = do t <- getResDef q | otherwise = do t <- getResDef q
eval env t vs eval env t vs
eval env (QC q) vs = return (VApp q vs) eval env (QC q) vs = return (VApp q vs)
@@ -313,39 +297,46 @@ eval env (TSymCat d r rs) []= do rs <- forM rs $ \(i,(pv,ty)) ->
Nothing -> evalError ("Variable" <+> pp pv <+> "is not in scope") Nothing -> evalError ("Variable" <+> pp pv <+> "is not in scope")
return (VSymCat d r rs) return (VSymCat d r rs)
eval env (TSymVar d r) [] = do return (VSymVar d r) eval env (TSymVar d r) [] = do return (VSymVar d r)
eval env t@(Opts n cs) vs = EvalM $ \gr k e mt b r msgs ->
case cs of
[] -> return $ Fail ("No options in expression:" $$ ppTerm Unqualified 0 t) msgs
((l,t):_) -> case eval env t vs of EvalM f -> f gr k e mt b r msgs
eval env t vs = evalError ("Cannot reduce term" <+> pp t) eval env t vs = evalError ("Cannot reduce term" <+> pp t)
apply v [] = return v
apply (VMeta m vs0) vs = return (VMeta m (vs0++vs)) apply (VMeta m vs0) vs = return (VMeta m (vs0++vs))
apply (VSusp m k vs0) vs = return (VSusp m k (vs0++vs)) apply (VSusp m k vs0) vs = return (VSusp m k (vs0++vs))
apply (VApp f vs0) vs = return (VApp f (vs0++vs)) apply (VApp f@(m,p) vs0) vs
| m == cPredef = evalPredef p (vs0++vs)
| otherwise = return (VApp f (vs0++vs))
apply (VGen i vs0) vs = return (VGen i (vs0++vs)) apply (VGen i vs0) vs = return (VGen i (vs0++vs))
apply (VClosure env (Abs b x t)) (v:vs) = eval ((x,v):env) t vs apply (VClosure env (Abs b x t)) (v:vs) = eval ((x,v):env) t vs
apply v [] = return v
stdPredef :: PredefTable s stdPredef :: PredefTable s
stdPredef = Map.fromList stdPredef = Map.fromList
[(cLength, pdStandard 1 $\ \[v] -> case value2string v of [(cLength, pd 1 $\ \[v] -> case value2string v of
Const s -> return (Const (VInt (genericLength s))) Const s -> return (Const (VInt (genericLength s)))
_ -> return RunTime) _ -> return RunTime)
,(cTake, pdStandard 2 $\ \[v1,v2] -> return (fmap string2value (liftA2 genericTake (value2int v1) (value2string v2)))) ,(cTake, pd 2 $\ \[v1,v2] -> return (fmap string2value (liftA2 genericTake (value2int v1) (value2string v2))))
,(cDrop, pdStandard 2 $\ \[v1,v2] -> return (fmap string2value (liftA2 genericDrop (value2int v1) (value2string v2)))) ,(cDrop, pd 2 $\ \[v1,v2] -> return (fmap string2value (liftA2 genericDrop (value2int v1) (value2string v2))))
,(cTk, pdStandard 2 $\ \[v1,v2] -> return (fmap string2value (liftA2 genericTk (value2int v1) (value2string v2)))) ,(cTk, pd 2 $\ \[v1,v2] -> return (fmap string2value (liftA2 genericTk (value2int v1) (value2string v2))))
,(cDp, pdStandard 2 $\ \[v1,v2] -> return (fmap string2value (liftA2 genericDp (value2int v1) (value2string v2)))) ,(cDp, pd 2 $\ \[v1,v2] -> return (fmap string2value (liftA2 genericDp (value2int v1) (value2string v2))))
,(cIsUpper,pdStandard 1 $\ \[v] -> return (fmap toPBool (liftA (all isUpper) (value2string v)))) ,(cIsUpper,pd 1 $\ \[v] -> return (fmap toPBool (liftA (all isUpper) (value2string v))))
,(cToUpper,pdStandard 1 $\ \[v] -> return (fmap string2value (liftA (map toUpper) (value2string v)))) ,(cToUpper,pd 1 $\ \[v] -> return (fmap string2value (liftA (map toUpper) (value2string v))))
,(cToLower,pdStandard 1 $\ \[v] -> return (fmap string2value (liftA (map toLower) (value2string v)))) ,(cToLower,pd 1 $\ \[v] -> return (fmap string2value (liftA (map toLower) (value2string v))))
,(cEqStr, pdStandard 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 (==) (value2string v1) (value2string v2)))) ,(cEqStr, pd 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 (==) (value2string v1) (value2string v2))))
,(cOccur, pdStandard 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 occur (value2string v1) (value2string v2)))) ,(cOccur, pd 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 occur (value2string v1) (value2string v2))))
,(cOccurs, pdStandard 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 occurs (value2string v1) (value2string v2)))) ,(cOccurs, pd 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 occurs (value2string v1) (value2string v2))))
,(cEqInt, pdStandard 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 (==) (value2int v1) (value2int v2)))) ,(cEqInt, pd 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 (==) (value2int v1) (value2int v2))))
,(cLessInt,pdStandard 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 (<) (value2int v1) (value2int v2)))) ,(cLessInt,pd 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 (<) (value2int v1) (value2int v2))))
,(cPlus, pdStandard 2 $\ \[v1,v2] -> return (fmap VInt (liftA2 (+) (value2int v1) (value2int v2)))) ,(cPlus, pd 2 $\ \[v1,v2] -> return (fmap VInt (liftA2 (+) (value2int v1) (value2int v2))))
,(cError, pdStandard 1 $\ \[v] -> case value2string v of ,(cError, pd 1 $\ \[v] -> case value2string v of
Const msg -> fail msg Const msg -> fail msg
_ -> fail "Indescribable error appeared") _ -> fail "Indescribable error appeared")
] ]
where where
pd n = pdArity n . pdForce
genericTk n = reverse . genericDrop n . reverse genericTk n = reverse . genericDrop n . reverse
genericDp n = reverse . genericTake n . reverse genericDp n = reverse . genericTake n . reverse
@@ -773,51 +764,33 @@ value2int _ = RunTime
-- * Global/built-in definitions -- * Global/built-in definitions
type PredefImpl a s = [a] -> EvalM s (ConstValue (Value s)) type PredefImpl a s = [a] -> EvalM s (ConstValue (Value s))
newtype Predef a s = Predef { runPredef :: Term -> Env s -> PredefImpl a s } newtype Predef a s = Predef { runPredef :: PredefImpl a s }
type PredefCombinator a b s = Predef a s -> Predef b s type PredefCombinator a b s = Predef a s -> Predef b s
infix 0 $\\ infix 1 $\\
($\) :: PredefCombinator a b s -> PredefImpl a s -> Predef b s ($\) :: PredefCombinator a b s -> PredefImpl a s -> Predef b s
k $\ f = k (Predef (\_ _ -> f)) k $\ f = k (Predef f)
pdForce :: PredefCombinator (Value s) (Thunk s) s pdForce :: PredefCombinator (Value s) (Thunk s) s
pdForce def = Predef $ \h env args -> do pdForce def = Predef $ \args -> do
argValues <- mapM force args argValues <- mapM force args
runPredef def h env argValues runPredef def argValues
pdClosedArgs :: PredefCombinator (Value s) (Value s) s pdCanonicalArgs :: PredefCombinator (Value s) (Value s) s
pdClosedArgs def = Predef $ \h env args -> do pdCanonicalArgs def = Predef $ \args ->
open <- anyM (value2term True [] >=> isOpen []) args if all isCanonicalForm args then runPredef def args else return RunTime
if open then return RunTime else runPredef def h env args
pdArity :: Int -> PredefCombinator (Thunk s) (Thunk s) s pdArity :: Int -> PredefCombinator (Thunk s) (Thunk s) s
pdArity n def = Predef $ \h env args -> pdArity n def = Predef $ \args ->
case splitAt' n args of case splitAt' n args of
Nothing -> do Nothing -> return RunTime
t <- papply env h args
let t' = abstract 0 (n - length args) t
Const <$> eval env t' []
Just (usedArgs, remArgs) -> do Just (usedArgs, remArgs) -> do
res <- runPredef def h env usedArgs res <- runPredef def usedArgs
forM res $ \v -> case remArgs of forM res $ \v -> apply v remArgs
[] -> return v
_ -> do
t <- value2term False (fst <$> env) v
eval env t remArgs
where
papply env t [] = return t
papply env t (arg:args) = do
arg <- tnk2term False (fst <$> env) arg
papply env (App t arg) args
abstract i n t
| n <= 0 = t
| otherwise = let x = identV (rawIdentS "a") i
in Abs Explicit x (abstract (i + 1) (n - 1) (App t (Vr x)))
pdStandard :: Int -> PredefCombinator (Value s) (Thunk s) s pdStandard :: Int -> PredefCombinator (Value s) (Thunk s) s
pdStandard n = pdArity n . pdForce . pdClosedArgs pdStandard n = pdArity n . pdForce . pdCanonicalArgs
----------------------------------------------------------------------- -----------------------------------------------------------------------
-- * Evaluation monad -- * Evaluation monad
@@ -884,11 +857,16 @@ evalError msg = EvalM (\gr k e _ _ r ws -> e msg ws)
evalWarn :: Message -> EvalM s () evalWarn :: Message -> EvalM s ()
evalWarn msg = EvalM (\gr k e mt d r msgs -> k () mt d r (msg:msgs)) evalWarn msg = EvalM (\gr k e mt d r msgs -> k () mt d r (msg:msgs))
evalPredef :: Env s -> Term -> Ident -> [Thunk s] -> EvalM s (ConstValue (Value s)) evalPredef :: Ident -> [Thunk s] -> EvalM s (Value s)
evalPredef env h id args = EvalM (\globals@(Gl _ predef) k e mt d r msgs -> evalPredef id args = do
case fmap (\def -> runPredef def h env args) (Map.lookup id predef) of res <- EvalM $ \globals@(Gl _ predef) k e mt d r msgs ->
Just (EvalM f) -> f globals k e mt d r msgs case Map.lookup id predef <&> \def -> runPredef def args of
Nothing -> k RunTime mt d r msgs) Just (EvalM f) -> f globals k e mt d r msgs
Nothing -> k RunTime mt d r msgs
case res of
Const res -> return res
RunTime -> return $ VApp (cPredef,id) args
NonExist -> return $ VApp (cPredef,cNonExist) []
getResDef :: QIdent -> EvalM s Term getResDef :: QIdent -> EvalM s Term
getResDef q = EvalM $ \(Gl gr _) k e mt d r msgs -> do getResDef q = EvalM $ \(Gl gr _) k e mt d r msgs -> do

359
src/compiler/api/GF/Compile/Compute/Concrete2.hs
View File

@@ -1,18 +1,22 @@
{-# LANGUAGE RankNTypes, BangPatterns, GeneralizedNewtypeDeriving #-} {-# LANGUAGE RankNTypes, BangPatterns, GeneralizedNewtypeDeriving, TupleSections #-}
module GF.Compile.Compute.Concrete2 module GF.Compile.Compute.Concrete2
(Env, Scope, Value(..), Constraint, ConstValue(..), Globals(..), PredefTable, EvalM, (Env, Scope, Value(..), Variants(..), Constraint, OptionInfo(..), ChoiceMap, cleanOptions,
runEvalM, stdPredef, globals, pdArity, ConstValue(..), ConstVariants(..), Globals(..), PredefTable, EvalM,
mapVariants, unvariants, variants2consts, consts2variants,
runEvalM, runEvalMWithOpts, stdPredef, globals,
PredefImpl, Predef(..), ($\),
pdCanonicalArgs, pdArity,
normalForm, normalFlatForm, normalForm, normalFlatForm,
eval, apply, value2term, value2termM, bubble, patternMatch, vtableSelect, eval, apply, value2term, value2termM, bubble, patternMatch, vtableSelect,
newResiduation, getMeta, setMeta, MetaState(..), variants, try, newResiduation, getMeta, setMeta, MetaState(..), variants, try,
evalError, evalWarn, ppValue, Choice, unit, split, split4, mapC, mapCM) where evalError, evalWarn, ppValue, Choice(..), unit, poison, split, split3, split4, mapC, mapCM) where
import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
import GF.Infra.Ident import GF.Infra.Ident
import GF.Infra.CheckM import GF.Infra.CheckM
import GF.Data.Operations(Err(..)) import GF.Data.Operations(Err(..))
import GF.Data.Utilities(splitAt',(<||>),anyM) import GF.Data.Utilities(maybeAt,splitAt',(<||>),anyM)
import GF.Grammar.Lookup(lookupResDef,lookupOrigInfo) import GF.Grammar.Lookup(lookupResDef,lookupOrigInfo)
import GF.Grammar.Grammar import GF.Grammar.Grammar
import GF.Grammar.Macros import GF.Grammar.Macros
@@ -24,19 +28,38 @@ import Control.Monad
import Control.Applicative hiding (Const) import Control.Applicative hiding (Const)
import qualified Control.Applicative as A import qualified Control.Applicative as A
import qualified Data.Map as Map import qualified Data.Map as Map
import Data.Bifunctor (second)
import Data.Functor ((<&>))
import Data.Maybe (fromMaybe,fromJust) import Data.Maybe (fromMaybe,fromJust)
import Data.List import Data.List
import Data.Char import Data.Char
type PredefImpl = Globals -> Choice -> [Value] -> ConstValue Value
newtype Predef = Predef { runPredef :: PredefImpl }
infix 1 $\
($\) :: (Predef -> Predef) -> PredefImpl -> Predef
k $\ f = k (Predef f)
pdCanonicalArgs :: Bool -> Predef -> Predef
pdCanonicalArgs flat def = Predef $ \g c args ->
if all (isCanonicalForm flat) args then runPredef def g c args else RunTime
pdArity :: Int -> Predef -> Predef
pdArity n def = Predef $ \g c args ->
case splitAt' n args of
Nothing -> RunTime
Just (usedArgs, remArgs) ->
runPredef def g c usedArgs <&> \v -> apply g v remArgs
type Env = [(Ident,Value)] type Env = [(Ident,Value)]
type Scope = [(Ident,Value)] type Scope = [(Ident,Value)]
type Predef a = Globals -> Choice -> [Value] -> ConstValue a type PredefTable = Map.Map Ident Predef
type PredefCombinator a = Predef a -> Predef a
type PredefTable = Map.Map Ident (Predef Value)
data Globals = Gl Grammar PredefTable data Globals = Gl Grammar PredefTable
data Value data Value
= VApp QIdent [Value] = VApp Choice QIdent [Value]
| VMeta {-# UNPACK #-} !MetaId [Value] | VMeta {-# UNPACK #-} !MetaId [Value]
| VSusp {-# UNPACK #-} !MetaId (Value -> Value) [Value] | VSusp {-# UNPACK #-} !MetaId (Value -> Value) [Value]
| VGen {-# UNPACK #-} !Int [Value] | VGen {-# UNPACK #-} !Int [Value]
@@ -59,7 +82,7 @@ data Value
| VGlue Value Value | VGlue Value Value
| VPatt Int (Maybe Int) Patt | VPatt Int (Maybe Int) Patt
| VPattType Value | VPattType Value
| VFV Choice [Value] | VFV Choice Variants
| VAlts Value [(Value, Value)] | VAlts Value [(Value, Value)]
| VStrs [Value] | VStrs [Value]
| VMarkup Ident [(Ident,Value)] [Value] | VMarkup Ident [(Ident,Value)] [Value]
@@ -71,16 +94,61 @@ data Value
| VCRecType [(Label, Bool, Value)] | VCRecType [(Label, Bool, Value)]
| VCInts (Maybe Integer) (Maybe Integer) | VCInts (Maybe Integer) (Maybe Integer)
data Variants
= VarFree [Value]
| VarOpts Value [(Value, Value)]
mapVariants :: (Value -> Value) -> Variants -> Variants
mapVariants f (VarFree vs) = VarFree (f <$> vs)
mapVariants f (VarOpts n cs) = VarOpts n (second f <$> cs)
unvariants :: Variants -> [Value]
unvariants (VarFree vs) = vs
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 (VR {}) = True
isCanonicalForm flat (VTable d cod) = isCanonicalForm flat d && isCanonicalForm flat cod
isCanonicalForm flat (VT {}) = True
isCanonicalForm flat (VV {}) = True
isCanonicalForm flat (VSort {}) = True
isCanonicalForm flat (VInt {}) = True
isCanonicalForm flat (VFlt {}) = True
isCanonicalForm flat (VStr {}) = True
isCanonicalForm flat VEmpty = True
isCanonicalForm True (VFV {}) = False
isCanonicalForm False (VFV c vs) = all (isCanonicalForm False) (unvariants vs)
isCanonicalForm flat (VAlts d vs) = all (isCanonicalForm flat . snd) vs
isCanonicalForm flat (VStrs vs) = all (isCanonicalForm flat) vs
isCanonicalForm flat (VMarkup tag as vs) = all (isCanonicalForm flat . snd) as && all (isCanonicalForm flat) vs
isCanonicalForm flat (VReset ctl v) = isCanonicalForm flat v
isCanonicalForm flat _ = False
data ConstValue a data ConstValue a
= Const a = Const a
| CSusp MetaId (Value -> ConstValue a) | CSusp MetaId (Value -> ConstValue a)
| CFV Choice [ConstValue a] | CFV Choice (ConstVariants a)
| RunTime | RunTime
| NonExist | NonExist
data ConstVariants a
= ConstFree [ConstValue a]
| ConstOpts Value [(Value, ConstValue a)]
mapConstVs :: (ConstValue a -> ConstValue b) -> ConstVariants a -> ConstVariants b
mapConstVs f (ConstFree vs) = ConstFree (f <$> vs)
mapConstVs f (ConstOpts n cs) = ConstOpts n (second f <$> cs)
unconstVs :: ConstVariants a -> [ConstValue a]
unconstVs (ConstFree vs) = vs
unconstVs (ConstOpts n cs) = snd <$> cs
instance Functor ConstValue where instance Functor ConstValue where
fmap f (Const c) = Const (f c) fmap f (Const c) = Const (f c)
fmap f (CFV i vs) = CFV i (map (fmap f) vs) fmap f (CFV i vs) = CFV i (mapConstVs (fmap f) vs)
fmap f (CSusp i k) = CSusp i (fmap f . k) fmap f (CSusp i k) = CSusp i (fmap f . k)
fmap f RunTime = RunTime fmap f RunTime = RunTime
fmap f NonExist = NonExist fmap f NonExist = NonExist
@@ -89,8 +157,8 @@ instance Applicative ConstValue where
pure = Const pure = Const
(Const f) <*> (Const x) = Const (f x) (Const f) <*> (Const x) = Const (f x)
(CFV s vs) <*> v2 = CFV s [v1 <*> v2 | v1 <- vs] (CFV s vs) <*> v2 = CFV s (mapConstVs (<*> v2) vs)
v1 <*> (CFV s vs) = CFV s [v1 <*> v2 | v2 <- vs] v1 <*> (CFV s vs) = CFV s (mapConstVs (v1 <*>) vs)
(CSusp i k) <*> v2 = CSusp i (\v -> k v <*> v2) (CSusp i k) <*> v2 = CSusp i (\v -> k v <*> v2)
v1 <*> (CSusp i k) = CSusp i (\v -> v1 <*> k v) v1 <*> (CSusp i k) = CSusp i (\v -> v1 <*> k v)
NonExist <*> _ = NonExist NonExist <*> _ = NonExist
@@ -98,6 +166,14 @@ instance Applicative ConstValue where
RunTime <*> _ = RunTime RunTime <*> _ = RunTime
_ <*> RunTime = RunTime _ <*> RunTime = RunTime
variants2consts :: (Value -> ConstValue a) -> Variants -> ConstVariants a
variants2consts f (VarFree vs) = ConstFree (f <$> vs)
variants2consts f (VarOpts n os) = ConstOpts n (second f <$> os)
consts2variants :: (ConstValue a -> Value) -> ConstVariants a -> Variants
consts2variants f (ConstFree vs) = VarFree (f <$> vs)
consts2variants f (ConstOpts n os) = VarOpts n (second f <$> os)
normalForm :: Globals -> Term -> Check Term normalForm :: Globals -> Term -> Check Term
normalForm g t = value2term g [] (bubble (eval g [] unit t [])) normalForm g t = value2term g [] (bubble (eval g [] unit t []))
@@ -130,7 +206,7 @@ eval g env s (P t lbl) vs = let project (VR as) = case lookup lbl a
Nothing -> VError ("Missing value for label" <+> pp lbl $$ Nothing -> VError ("Missing value for label" <+> pp lbl $$
"in" <+> pp (P t lbl)) "in" <+> pp (P t lbl))
Just v -> apply g v vs Just v -> apply g v vs
project (VFV s fvs) = VFV s (map project fvs) project (VFV s fvs) = VFV s (mapVariants project fvs)
project (VMeta i vs) = VSusp i (\v -> project (apply g v vs)) [] project (VMeta i vs) = VSusp i (\v -> project (apply g v vs)) []
project (VSusp i k vs) = VSusp i (\v -> project (apply g (k v) vs)) [] project (VSusp i k vs) = VSusp i (\v -> project (apply g (k v) vs)) []
project v = VP v lbl vs project v = VP v lbl vs
@@ -139,8 +215,8 @@ 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 (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,v) -> update lbl v as) as1 as2)
extend (VFV i fvs) v2 = VFV i [extend v1 v2 | v1 <- fvs] extend (VFV i fvs) v2 = VFV i (mapVariants (`extend` v2) fvs)
extend v1 (VFV i fvs) = VFV i [extend v1 v2 | 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) [] extend (VMeta i vs) v2 = VSusp i (\v -> extend (apply g v vs) v2) []
extend v1 (VMeta i vs) = VSusp i (\v -> extend v1 (apply g v vs)) [] extend v1 (VMeta i vs) = VSusp i (\v -> extend v1 (apply g v vs)) []
extend (VSusp i k vs) v2 = VSusp i (\v -> extend (apply g (k v) vs) v2) [] extend (VSusp i k vs) v2 = VSusp i (\v -> extend (apply g (k v) vs) v2) []
@@ -168,37 +244,31 @@ eval g env s (S t1 t2) vs = let (!s1,!s2) = split s
Success tys ws -> case tys of Success tys ws -> case tys of
[ty] -> vtableSelect g v0 ty tvs v2 vs [ty] -> vtableSelect g v0 ty tvs v2 vs
tys -> vtableSelect g v0 (FV (reverse tys)) tvs v2 vs tys -> vtableSelect g v0 (FV (reverse tys)) tvs v2 vs
select (VFV i fvs) = VFV i [select v1 | v1 <- fvs] select (VFV i fvs) = VFV i (mapVariants select fvs)
select (VMeta i vs) = VSusp i (\v -> select (apply g v vs)) [] select (VMeta i vs) = VSusp i (\v -> select (apply g v vs)) []
select (VSusp i k vs) = VSusp i (\v -> select (apply g (k v) vs)) [] select (VSusp i k vs) = VSusp i (\v -> select (apply g (k v) vs)) []
select v1 = v0 select v1 = v0
empty = State Map.empty Map.empty -- FIXME: options=[] is definitely not correct and this shouldn't be using value2termM at all
empty = State Map.empty Map.empty []
in select v1 in select v1
eval g env s (Let (x,(_,t1)) t2) vs = let (!s1,!s2) = split s eval g env s (Let (x,(_,t1)) t2) vs = let (!s1,!s2) = split s
in eval g ((x,eval g env s1 t1 []):env) s2 t2 vs in eval g ((x,eval g env s1 t1 []):env) s2 t2 vs
eval g env c (Q q@(m,id)) vs eval g env c (Q q@(m,id)) vs
| m == cPredef = case Map.lookup id predef of | m == cPredef = evalPredef g c id vs
Nothing -> VApp q vs
Just fn -> let valueOf (Const res) = res
valueOf (CFV i vs) = VFV i (map valueOf vs)
valueOf (CSusp i k) = VSusp i (valueOf . k) []
valueOf RunTime = VApp q vs
valueOf NonExist = VApp (cPredef,cNonExist) []
in valueOf (fn g c vs)
| otherwise = case lookupResDef gr q of | otherwise = case lookupResDef gr q of
Ok t -> eval g env c t vs Ok t -> eval g env c t vs
Bad msg -> error msg Bad msg -> error msg
where where
Gl gr predef = g Gl gr predef = g
eval g env s (QC q) vs = VApp q vs eval g env s (QC q) vs = VApp s q vs
eval g env s (C t1 t2) [] = let (!s1,!s2) = split s eval g env s (C t1 t2) [] = let (!s1,!s2) = split s
concat v1 VEmpty = v1 concat v1 VEmpty = v1
concat VEmpty v2 = v2 concat VEmpty v2 = v2
concat (VFV i fvs) v2 = VFV i [concat v1 v2 | v1 <- fvs] concat (VFV i fvs) v2 = VFV i (mapVariants (`concat` v2) fvs)
concat v1 (VFV i fvs) = VFV i [concat v1 v2 | v2 <- fvs] concat v1 (VFV i fvs) = VFV i (mapVariants (v1 `concat`) fvs)
concat (VMeta i vs) v2 = VSusp i (\v -> concat (apply g v vs) v2) [] concat (VMeta i vs) v2 = VSusp i (\v -> concat (apply g v vs) v2) []
concat v1 (VMeta i vs) = VSusp i (\v -> concat v1 (apply g v vs)) [] concat v1 (VMeta i vs) = VSusp i (\v -> concat v1 (apply g v vs)) []
concat (VSusp i k vs) v2 = VSusp i (\v -> concat (apply g (k v) vs) v2) [] concat (VSusp i k vs) v2 = VSusp i (\v -> concat (apply g (k v) vs) v2) []
@@ -210,18 +280,18 @@ eval g env s (Glue t1 t2) [] = let (!s1,!s2) = split s
glue VEmpty v = v glue VEmpty v = v
glue (VC v1 v2) v = VC v1 (glue v2 v) glue (VC v1 v2) v = VC v1 (glue v2 v)
glue (VApp q []) v glue (VApp c q []) v
| q == (cPredef,cNonExist) = VApp q [] | q == (cPredef,cNonExist) = VApp c q []
glue v VEmpty = v glue v VEmpty = v
glue v (VC v1 v2) = VC (glue v v1) v2 glue v (VC v1 v2) = VC (glue v v1) v2
glue v (VApp q []) glue v (VApp c q [])
| q == (cPredef,cNonExist) = VApp q [] | q == (cPredef,cNonExist) = VApp c q []
glue (VStr s1) (VStr s2) = VStr (s1++s2) glue (VStr s1) (VStr s2) = VStr (s1++s2)
glue v (VAlts d vas) = VAlts (glue v d) [(glue v v',ss) | (v',ss) <- vas] glue v (VAlts d vas) = VAlts (glue v d) [(glue v v',ss) | (v',ss) <- vas]
glue (VAlts d vas) (VStr s) = pre d vas s glue (VAlts d vas) (VStr s) = pre d vas s
glue (VAlts d vas) v = glue d v glue (VAlts d vas) v = glue d v
glue (VFV i fvs) v2 = VFV i [glue v1 v2 | v1 <- fvs] glue (VFV i fvs) v2 = VFV i (mapVariants (`glue` v2) fvs)
glue v1 (VFV i fvs) = VFV i [glue v1 v2 | v2 <- fvs] glue v1 (VFV i fvs) = VFV i (mapVariants (v1 `glue`) fvs)
glue (VMeta i vs) v2 = VSusp i (\v -> glue (apply g v vs) v2) [] glue (VMeta i vs) v2 = VSusp i (\v -> glue (apply g v vs) v2) []
glue v1 (VMeta i vs) = VSusp i (\v -> glue v1 (apply g v vs)) [] glue v1 (VMeta i vs) = VSusp i (\v -> glue v1 (apply g v vs)) []
glue (VSusp i k vs) v2 = VSusp i (\v -> glue (apply g (k v) vs) v2) [] glue (VSusp i k vs) v2 = VSusp i (\v -> glue (apply g (k v) vs) v2) []
@@ -242,7 +312,7 @@ eval g env s (ELincat c ty) [] = let lbl = lockLabel c
eval g env s (ELin c t) [] = let lbl = lockLabel c eval g env s (ELin c t) [] = let lbl = lockLabel c
lt = R [] lt = R []
in eval g env s (ExtR t (R [(lbl,(Nothing,lt))])) [] in eval g env s (ExtR t (R [(lbl,(Nothing,lt))])) []
eval g env s (FV ts) vs = VFV s (mapC (\s t -> eval g env s t vs) s ts) eval g env s (FV ts) vs = VFV s (VarFree (mapC (\s t -> eval g env s t vs) s ts))
eval g env s (Alts d as) [] = let (!s1,!s2) = split s eval g env s (Alts d as) [] = let (!s1,!s2) = split s
vd = eval g env s1 d [] vd = eval g env s1 d []
vas = mapC (\s (t1,t2) -> let (!s1,!s2) = split s vas = mapC (\s (t1,t2) -> let (!s1,!s2) = split s
@@ -256,25 +326,43 @@ eval g env c (Markup tag as ts) [] =
in (VMarkup tag vas vs) in (VMarkup tag vas vs)
eval g env c (Reset ctl t) [] = VReset ctl (eval g env c t []) eval g env c (Reset ctl t) [] = VReset ctl (eval g env c t [])
eval g env c (TSymCat d r rs) []= VSymCat d r [(i,(fromJust (lookup pv env),ty)) | (i,(pv,ty)) <- rs] eval g env c (TSymCat d r rs) []= VSymCat d r [(i,(fromJust (lookup pv env),ty)) | (i,(pv,ty)) <- rs]
eval g env c t@(Opts n cs) vs = if null cs
then VError ("No options in expression:" $$ ppTerm Unqualified 0 t)
else let (c1,c2,c3) = split3 c
vn = eval g env c1 n []
vcs = mapC evalOpt c cs
in VFV c3 (VarOpts vn vcs)
where evalOpt c' (l,t) = let (c1,c2) = split c' in (eval g env c1 l [], eval g env c2 t vs)
eval g env c t vs = VError ("Cannot reduce term" <+> pp t) eval g env c t vs = VError ("Cannot reduce term" <+> pp t)
evalPredef :: Globals -> Choice -> Ident -> [Value] -> Value
evalPredef g@(Gl gr pds) c n args =
case Map.lookup n pds of
Nothing -> VApp c (cPredef,n) args
Just def -> let valueOf (Const res) = res
valueOf (CFV i vs) = VFV i (consts2variants valueOf vs)
valueOf (CSusp i k) = VSusp i (valueOf . k) []
valueOf RunTime = VApp c (cPredef,n) args
valueOf NonExist = VApp c (cPredef,cNonExist) []
in valueOf (runPredef def g c args)
stdPredef :: Globals -> PredefTable stdPredef :: Globals -> PredefTable
stdPredef g = Map.fromList stdPredef g = Map.fromList
[(cLength, pdArity 1 $ \g c [v] -> fmap (VInt . genericLength) (value2string g v)) [(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))) ,(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))) ,(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))) ,(cTk, pdArity 2 $\ \g c [v1,v2] -> fmap string2value (liftA2 genericTk (value2int g v1) (value2string g v2)))
,(cDp, pdArity 2 $ \g c [v1,v2] -> fmap string2value (liftA2 genericDp (value2int g v1) (value2string g v2))) ,(cDp, pdArity 2 $\ \g c [v1,v2] -> fmap string2value (liftA2 genericDp (value2int g v1) (value2string g v2)))
,(cIsUpper,pdArity 1 $ \g c [v] -> fmap toPBool (liftA (all isUpper) (value2string g v))) ,(cIsUpper,pdArity 1 $\ \g c [v] -> fmap toPBool (liftA (all isUpper) (value2string g v)))
,(cToUpper,pdArity 1 $ \g c [v] -> fmap string2value (liftA (map toUpper) (value2string g v))) ,(cToUpper,pdArity 1 $\ \g c [v] -> fmap string2value (liftA (map toUpper) (value2string g v)))
,(cToLower,pdArity 1 $ \g c [v] -> fmap string2value (liftA (map toLower) (value2string g v))) ,(cToLower,pdArity 1 $\ \g c [v] -> fmap string2value (liftA (map toLower) (value2string g v)))
,(cEqStr, pdArity 2 $ \g c [v1,v2] -> fmap toPBool (liftA2 (==) (value2string g v1) (value2string g v2))) ,(cEqStr, pdArity 2 $\ \g c [v1,v2] -> fmap toPBool (liftA2 (==) (value2string g v1) (value2string g v2)))
,(cOccur, pdArity 2 $ \g c [v1,v2] -> fmap toPBool (liftA2 occur (value2string g v1) (value2string g v2))) ,(cOccur, pdArity 2 $\ \g c [v1,v2] -> fmap toPBool (liftA2 occur (value2string g v1) (value2string g v2)))
,(cOccurs, pdArity 2 $ \g c [v1,v2] -> fmap toPBool (liftA2 occurs (value2string g v1) (value2string g v2))) ,(cOccurs, pdArity 2 $\ \g c [v1,v2] -> fmap toPBool (liftA2 occurs (value2string g v1) (value2string g v2)))
,(cEqInt, pdArity 2 $ \g c [v1,v2] -> fmap toPBool (liftA2 (==) (value2int g v1) (value2int g v2))) ,(cEqInt, pdArity 2 $\ \g c [v1,v2] -> fmap toPBool (liftA2 (==) (value2int g v1) (value2int g v2)))
,(cLessInt,pdArity 2 $ \g c [v1,v2] -> fmap toPBool (liftA2 (<) (value2int g v1) (value2int g v2))) ,(cLessInt,pdArity 2 $\ \g c [v1,v2] -> fmap toPBool (liftA2 (<) (value2int g v1) (value2int g v2)))
,(cPlus, pdArity 2 $ \g c [v1,v2] -> fmap VInt (liftA2 (+) (value2int g v1) (value2int g v2))) ,(cPlus, pdArity 2 $\ \g c [v1,v2] -> fmap VInt (liftA2 (+) (value2int g v1) (value2int g v2)))
,(cError, pdArity 1 $ \g c [v] -> fmap (VError . pp) (value2string g v)) ,(cError, pdArity 1 $\ \g c [v] -> fmap (VError . pp) (value2string g v))
] ]
where where
genericTk n = reverse . genericDrop n . reverse genericTk n = reverse . genericDrop n . reverse
@@ -282,16 +370,22 @@ stdPredef g = Map.fromList
apply g (VMeta i vs0) vs = VMeta i (vs0++vs) apply g (VMeta i vs0) vs = VMeta i (vs0++vs)
apply g (VSusp i k vs0) vs = VSusp i k (vs0++vs) apply g (VSusp i k vs0) vs = VSusp i k (vs0++vs)
apply g (VApp f vs0) vs = VApp f (vs0++vs) apply g (VApp c f@(m,n) vs0) vs
| m == cPredef = evalPredef g c n (vs0++vs)
| otherwise = VApp c f (vs0++vs)
apply g (VGen i vs0) vs = VGen i (vs0++vs) apply g (VGen i vs0) vs = VGen i (vs0++vs)
apply g (VFV i fvs) vs = VFV i [apply g v vs | v <- fvs] apply g (VFV i fvs) vs = VFV i (mapVariants (\v -> apply g v vs) fvs)
apply g (VS v1 v2 vs') vs = VS v1 v2 (vs'++vs) apply g (VS v1 v2 vs') vs = VS v1 v2 (vs'++vs)
apply g (VClosure env s (Abs b x t)) (v:vs) = eval g ((x,v):env) s t vs apply g (VClosure env s (Abs b x t)) (v:vs) = eval g ((x,v):env) s t vs
apply g v [] = v apply g v [] = v
data BubbleVariants
= BubbleFree Int
| BubbleOpts Value [Value]
bubble v = snd (bubble v) bubble v = snd (bubble v)
where where
bubble (VApp f vs) = liftL (VApp f) vs bubble (VApp c f vs) = liftL (VApp c f) vs
bubble (VMeta metaid vs) = liftL (VMeta metaid) vs bubble (VMeta metaid vs) = liftL (VMeta metaid) vs
bubble (VSusp metaid k vs) = liftL (VSusp metaid k) vs bubble (VSusp metaid k vs) = liftL (VSusp metaid k) vs
bubble (VGen i vs) = liftL (VGen i) vs bubble (VGen i vs) = liftL (VGen i) vs
@@ -314,9 +408,12 @@ bubble v = snd (bubble v)
bubble (VGlue v1 v2) = lift2 VGlue v1 v2 bubble (VGlue v1 v2) = lift2 VGlue v1 v2
bubble v@(VPatt _ _ _) = lift0 v bubble v@(VPatt _ _ _) = lift0 v
bubble (VPattType v) = lift1 VPattType v bubble (VPattType v) = lift1 VPattType v
bubble (VFV c vs) = bubble (VFV c (VarFree vs)) =
let (union,vs') = mapAccumL descend Map.empty vs let (union,vs') = mapAccumL descend Map.empty vs
in (Map.insert c (length vs,1) union, addVariants (VFV c vs') union) in (Map.insert c (BubbleFree (length vs),1) union, addVariants (VFV c (VarFree vs')) union)
bubble (VFV c (VarOpts n os)) =
let (union,os') = mapAccumL (\acc (k,v) -> second (k,) $ descend acc v) Map.empty os
in (Map.insert c (BubbleOpts n (fst <$> os),1) union, addVariants (VFV c (VarOpts n os')) union)
bubble (VAlts v vs) = lift1L2 VAlts v vs bubble (VAlts v vs) = lift1L2 VAlts v vs
bubble (VStrs vs) = liftL VStrs vs bubble (VStrs vs) = liftL VStrs vs
bubble (VMarkup tag attrs vs) = bubble (VMarkup tag attrs vs) =
@@ -379,7 +476,7 @@ bubble v = snd (bubble v)
let (choices,v') = bubble v let (choices,v') = bubble v
in (mergeChoices1 union choices,v') in (mergeChoices1 union choices,v')
descend' :: Map.Map Choice (Int,Int) -> (a,Value) -> (Map.Map Choice (Int,Int),(a,Value)) descend' :: Map.Map Choice (BubbleVariants,Int) -> (a,Value) -> (Map.Map Choice (BubbleVariants,Int),(a,Value))
descend' union (x,v) = descend' union (x,v) =
let (choices,v') = bubble v let (choices,v') = bubble v
in (mergeChoices1 union choices,(x,v')) in (mergeChoices1 union choices,(x,v'))
@@ -399,16 +496,18 @@ bubble v = snd (bubble v)
addVariants v = Map.foldrWithKey addVariant v addVariants v = Map.foldrWithKey addVariant v
where where
addVariant c (n,cnt) v addVariant c (bvs,cnt) v
| cnt > 1 = VFV c (replicate n v) | cnt > 1 = VFV c $ case bvs of
BubbleFree k -> VarFree (replicate k v)
BubbleOpts n os -> VarOpts n ((,v) <$> os)
| otherwise = v | otherwise = v
unitfy = fmap (\(n,_) -> (n,1)) unitfy = fmap (\(n,_) -> (n,1))
mergeChoices1 = Map.mergeWithKey (\c (n,cnt) _ -> Just (n,cnt+1)) id unitfy mergeChoices1 = Map.mergeWithKey (\c (n,cnt) _ -> Just (n,cnt+1)) id unitfy
mergeChoices2 = Map.mergeWithKey (\c (n,cnt) _ -> Just (n,2)) unitfy unitfy mergeChoices2 = Map.mergeWithKey (\c (n,cnt) _ -> Just (n,2)) unitfy unitfy
toPBool True = VApp (cPredef,cPTrue) [] toPBool True = VApp poison (cPredef,cPTrue) []
toPBool False = VApp (cPredef,cPFalse) [] toPBool False = VApp poison (cPredef,cPFalse) []
occur s1 [] = False occur s1 [] = False
occur s1 s2@(_:tail) = check s1 s2 occur s1 s2@(_:tail) = check s1 s2
@@ -451,8 +550,8 @@ patternMatch g s v0 ((env0,ps,args0,t):eqs) = match env0 ps eqs args0
(p, VMeta i vs) -> VSusp i (\v -> match' env p ps eqs (apply g v vs) args) [] (p, VMeta i vs) -> VSusp i (\v -> match' env p ps eqs (apply g v vs) args) []
(p, VGen i vs) -> v0 (p, VGen i vs) -> v0
(p, VSusp i k vs) -> VSusp i (\v -> match' env p ps eqs (apply g (k v) vs) args) [] (p, VSusp i k vs) -> VSusp i (\v -> match' env p ps eqs (apply g (k v) vs) args) []
(p, VFV s vs) -> VFV s [match' env p ps eqs arg args | arg <- vs] (p, VFV s vs) -> VFV s (mapVariants (\arg -> match' env p ps eqs arg args) vs)
(PP q qs, VApp r vs) (PP q qs, VApp c r vs)
| q == r -> match env (qs++ps) eqs (vs++args) | q == r -> match env (qs++ps) eqs (vs++args)
(PR pas, VR as) -> matchRec env (reverse pas) as ps eqs args (PR pas, VR as) -> matchRec env (reverse pas) as ps eqs args
(PString s1, VStr s2) (PString s1, VStr s2)
@@ -510,7 +609,7 @@ vtableSelect g v0 ty cs v2 vs =
where where
select (Const (i,_)) = cs !! i select (Const (i,_)) = cs !! i
select (CSusp i k) = VSusp i (\v -> select (k v)) [] select (CSusp i k) = VSusp i (\v -> select (k v)) []
select (CFV s vs) = VFV s (map select vs) select (CFV s vs) = VFV s (consts2variants select vs)
select _ = v0 select _ = v0
value2index (VMeta i vs) ty = CSusp i (\v -> value2index (apply g v vs) ty) value2index (VMeta i vs) ty = CSusp i (\v -> value2index (apply g v vs) ty)
@@ -525,9 +624,9 @@ vtableSelect g v0 ty cs v2 vs =
(compute lbls) (compute lbls)
Nothing -> error (show ("Missing value for label" <+> pp lbl $$ Nothing -> error (show ("Missing value for label" <+> pp lbl $$
"among" <+> hsep (punctuate (pp ',') (map fst as)))) "among" <+> hsep (punctuate (pp ',') (map fst as))))
value2index (VApp q tnks) ty = value2index (VApp c q args) ty =
let (r ,ctxt,cnt ) = getIdxCnt q let (r ,ctxt,cnt ) = getIdxCnt q
in fmap (\(r', cnt') -> (r+r',cnt)) (compute ctxt tnks) in fmap (\(r', cnt') -> (r+r',cnt)) (compute ctxt args)
where where
getIdxCnt q = getIdxCnt q =
let (_,ResValue (L _ ty) idx) = getInfo q let (_,ResValue (L _ ty) idx) = getInfo q
@@ -550,7 +649,7 @@ vtableSelect g v0 ty cs v2 vs =
Gl gr _ = g Gl gr _ = g
value2index (VInt n) ty value2index (VInt n) ty
| Just max <- isTypeInts ty = Const (fromIntegral n,fromIntegral max+1) | Just max <- isTypeInts ty = Const (fromIntegral n,fromIntegral max+1)
value2index (VFV i vs) ty = CFV i [value2index v ty | v <- vs] value2index (VFV i vs) ty = CFV i (variants2consts (\v -> value2index v ty) vs)
value2index v ty = RunTime value2index v ty = RunTime
@@ -566,11 +665,23 @@ data MetaState
= Bound Scope Value = Bound Scope Value
| Narrowing Type | Narrowing Type
| Residuation Scope (Maybe Constraint) | Residuation Scope (Maybe Constraint)
data State data OptionInfo
= State = OptionInfo
{ choices :: Map.Map Choice Int { optChoice :: Choice
, metaVars :: Map.Map MetaId MetaState , optLabel :: Value
, optChoices :: [Value]
} }
type ChoiceMap = Map.Map Choice Int
data State
= State
{ choices :: ChoiceMap
, metaVars :: Map.Map MetaId MetaState
, options :: [OptionInfo]
}
cleanOptions :: [OptionInfo] -> ChoiceMap -> ChoiceMap
cleanOptions opts = Map.filterWithKey (\k _ -> any (\opt -> k == optChoice opt) opts)
type Cont r = State -> r -> [Message] -> CheckResult r [Message] type Cont r = State -> r -> [Message] -> CheckResult r [Message]
newtype EvalM a = EvalM (forall r . Globals -> (a -> Cont r) -> Cont r) newtype EvalM a = EvalM (forall r . Globals -> (a -> Cont r) -> Cont r)
@@ -606,46 +717,52 @@ runEvalM g (EvalM f) = Check $ \(es,ws) ->
Fail msg ws -> Fail msg (es,ws) Fail msg ws -> Fail msg (es,ws)
Success xs ws -> Success (reverse xs) (es,ws) Success xs ws -> Success (reverse xs) (es,ws)
where where
empty = State Map.empty Map.empty empty = State Map.empty Map.empty []
runEvalMWithOpts :: Globals -> ChoiceMap -> EvalM a -> Check [(a, ChoiceMap, [OptionInfo])]
runEvalMWithOpts g cs (EvalM f) = Check $ \(es,ws) ->
case f g (\x (State cs mvs os) xs ws -> Success ((x,cs,reverse os):xs) ws) init [] ws of
Fail msg ws -> Fail msg (es,ws)
Success xs ws -> Success (reverse xs) (es,ws)
where
init = State cs Map.empty []
reset :: EvalM a -> EvalM [a] reset :: EvalM a -> EvalM [a]
reset (EvalM f) = EvalM $ \g k state r ws -> reset (EvalM f) = EvalM $ \g k state r ws ->
case f g (\x state xs ws -> Success (x:xs) ws) state [] ws of case f g (\x state xs ws -> Success (x:xs) ws) state [] ws of
Fail msg ws -> Fail msg ws Fail msg ws -> Fail msg ws
Success xs ws -> k (reverse xs) state r ws Success xs ws -> k (reverse xs) state r ws
where
empty = State Map.empty Map.empty
globals :: EvalM Globals globals :: EvalM Globals
globals = EvalM (\g k -> k g) globals = EvalM (\g k -> k g)
variants :: Choice -> [a] -> EvalM a variants :: Choice -> [a] -> EvalM a
variants c xs = EvalM (\g k state@(State choices metas) r msgs -> variants c xs = EvalM (\g k state@(State choices metas opts) r msgs ->
case Map.lookup c choices of case Map.lookup c choices of
Just j -> k (xs !! j) state r msgs Just j -> k (xs !! j) state r msgs
Nothing -> backtrack 0 xs k choices metas r msgs) Nothing -> backtrack 0 xs k choices metas opts r msgs)
where where
backtrack j [] k choices metas r msgs = Success r msgs backtrack j [] k choices metas opts r msgs = Success r msgs
backtrack j (x:xs) k choices metas r msgs = backtrack j (x:xs) k choices metas opts r msgs =
case k x (State (Map.insert c j choices) metas) r msgs of case k x (State (Map.insert c j choices) metas opts) r msgs of
Fail msg msgs -> Fail msg msgs Fail msg msgs -> Fail msg msgs
Success r msgs -> backtrack (j+1) xs k choices metas r msgs Success r msgs -> backtrack (j+1) xs k choices metas opts r msgs
variants' :: Choice -> (a -> EvalM Term) -> [a] -> EvalM Term variants' :: Choice -> (a -> EvalM Term) -> [a] -> EvalM Term
variants' c f xs = EvalM (\g k state@(State choices metas) r msgs -> variants' c f xs = EvalM (\g k state@(State choices metas opts) r msgs ->
case Map.lookup c choices of case Map.lookup c choices of
Just j -> case f (xs !! j) of Just j -> case f (xs !! j) of
EvalM f -> f g k state r msgs EvalM f -> f g k state r msgs
Nothing -> case backtrack g 0 xs choices metas [] msgs of Nothing -> case backtrack g 0 xs choices metas opts [] msgs of
Fail msg msgs -> Fail msg msgs Fail msg msgs -> Fail msg msgs
Success ts msgs -> k (FV (reverse ts)) state r msgs) Success ts msgs -> k (FV (reverse ts)) state r msgs)
where where
backtrack g j [] choices metas ts msgs = Success ts msgs backtrack g j [] choices metas opts ts msgs = Success ts msgs
backtrack g j (x:xs) choices metas ts msgs = backtrack g j (x:xs) choices metas opts ts msgs =
case f x of case f x of
EvalM f -> case f g (\t st ts msgs -> Success (t:ts) msgs) (State (Map.insert c j choices) metas) ts msgs of EvalM f -> case f g (\t st ts msgs -> Success (t:ts) msgs) (State (Map.insert c j choices) metas opts) ts msgs of
Fail msg msgs -> Fail msg msgs Fail msg msgs -> Fail msg msgs
Success ts msgs -> backtrack g (j+1) xs choices metas ts msgs Success ts msgs -> backtrack g (j+1) xs choices metas opts ts msgs
try :: (a -> EvalM b) -> [a] -> Message -> EvalM b try :: (a -> EvalM b) -> [a] -> Message -> EvalM b
try f xs msg = EvalM (\g k state r msgs -> try f xs msg = EvalM (\g k state r msgs ->
@@ -668,9 +785,9 @@ try f xs msg = EvalM (\g k state r msgs ->
Success r msgs -> continue g k res r msgs Success r msgs -> continue g k res r msgs
newResiduation :: Scope -> EvalM MetaId newResiduation :: Scope -> EvalM MetaId
newResiduation scope = EvalM (\g k (State choices metas) r msgs -> newResiduation scope = EvalM (\g k (State choices metas opts) r msgs ->
let meta_id = Map.size metas+1 let meta_id = Map.size metas+1
in k meta_id (State choices (Map.insert meta_id (Residuation scope Nothing) metas)) r msgs) in k meta_id (State choices (Map.insert meta_id (Residuation scope Nothing) metas) opts) r msgs)
getMeta :: MetaId -> EvalM MetaState getMeta :: MetaId -> EvalM MetaState
getMeta i = EvalM (\g k state r msgs -> getMeta i = EvalM (\g k state r msgs ->
@@ -679,12 +796,12 @@ getMeta i = EvalM (\g k state r msgs ->
Nothing -> Fail ("Metavariable ?"<>pp i<+>"is not defined") msgs) Nothing -> Fail ("Metavariable ?"<>pp i<+>"is not defined") msgs)
setMeta :: MetaId -> MetaState -> EvalM () setMeta :: MetaId -> MetaState -> EvalM ()
setMeta i ms = EvalM (\g k (State choices metas) r msgs -> setMeta i ms = EvalM (\g k (State choices metas opts) r msgs ->
let state' = State choices (Map.insert i ms metas) let state' = State choices (Map.insert i ms metas) opts
in k () state' r msgs) in k () state' r msgs)
value2termM :: Bool -> [Ident] -> Value -> EvalM Term value2termM :: Bool -> [Ident] -> Value -> EvalM Term
value2termM flat xs (VApp q vs) = value2termM flat xs (VApp c q vs) =
foldM (\t v -> fmap (App t) (value2termM flat xs v)) (if fst q == cPredef then Q q else QC q) vs foldM (\t v -> fmap (App t) (value2termM flat xs v)) (if fst q == cPredef then Q q else QC q) vs
value2termM flat xs (VMeta i vs) = do value2termM flat xs (VMeta i vs) = do
mv <- getMeta i mv <- getMeta i
@@ -788,11 +905,18 @@ value2termM flat xs (VGlue v1 v2) = do
t1 <- value2termM flat xs v1 t1 <- value2termM flat xs v1
t2 <- value2termM flat xs v2 t2 <- value2termM flat xs v2
return (Glue t1 t2) return (Glue t1 t2)
value2termM flat xs (VFV i vs) = value2termM True xs (VFV i (VarFree vs)) = do
case flat of v <- variants i vs
True -> do v <- variants i vs value2termM True xs v
value2termM True xs v value2termM False xs (VFV i (VarFree vs)) = variants' i (value2termM False xs) vs
False -> variants' i (value2termM False xs) vs value2termM flat xs (VFV i (VarOpts n os)) =
EvalM $ \g k (State choices metas opts) r msgs ->
let j = fromMaybe 0 (Map.lookup i choices)
in case os `maybeAt` j of
Just (l,t) -> case value2termM flat xs t of
EvalM f -> let oi = OptionInfo i n (fst <$> os)
in f g k (State choices metas (oi:opts)) r msgs
Nothing -> Fail ("Index" <+> j <+> "out of bounds for option:" $$ ppValue Unqualified 0 n) msgs
value2termM flat xs (VPatt min max p) = return (EPatt min max p) value2termM flat xs (VPatt min max p) = return (EPatt min max p)
value2termM flat xs (VPattType v) = do t <- value2termM flat xs v value2termM flat xs (VPattType v) = do t <- value2termM flat xs v
return (EPattType t) return (EPattType t)
@@ -855,7 +979,7 @@ pattVars st (PSeq _ _ p1 _ _ p2) = pattVars (pattVars st p1) p2
pattVars st _ = st pattVars st _ = st
ppValue q d (VApp c vs) = prec d 4 (hsep (ppQIdent q c : map (ppValue q 5) vs)) ppValue q d (VApp c f vs) = prec d 4 (hsep (ppQIdent q f : map (ppValue q 5) vs))
ppValue q d (VMeta i vs) = prec d 4 (hsep ((if i > 0 then pp "?" <> pp i else pp "?") : map (ppValue q 5) vs)) ppValue q d (VMeta i vs) = prec d 4 (hsep ((if i > 0 then pp "?" <> pp i else pp "?") : map (ppValue q 5) vs))
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 (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 (VGen _ _) = pp "VGen"
@@ -882,7 +1006,7 @@ ppValue q d (VC v1 v2) = prec d 1 (hang (ppValue q 2 v1) 2 ("++" <+> ppValue q 1
ppValue q d (VGlue v1 v2) = prec d 2 (ppValue q 3 v1 <+> '+' <+> ppValue q 2 v2) ppValue q d (VGlue v1 v2) = prec d 2 (ppValue q 3 v1 <+> '+' <+> ppValue q 2 v2)
ppValue q d (VPatt _ _ _) = pp "VPatt" ppValue q d (VPatt _ _ _) = pp "VPatt"
ppValue q d (VPattType _) = pp "VPattType" ppValue q d (VPattType _) = pp "VPattType"
ppValue q d (VFV i vs) = prec d 4 ("variants" <+> pp i <+> braces (fsep (punctuate ';' (map (ppValue q 0) vs)))) ppValue q d (VFV i vs) = prec d 4 ("variants" <+> pp i <+> braces (fsep (punctuate ';' (map (ppValue q 0) (unvariants vs)))))
ppValue q d (VAlts e xs) = prec d 4 ("pre" <+> braces (ppValue q 0 e <> ';' <+> fsep (punctuate ';' (map (ppAltern q) xs)))) ppValue q d (VAlts e xs) = prec d 4 ("pre" <+> braces (ppValue q 0 e <> ';' <+> fsep (punctuate ';' (map (ppAltern q) xs))))
ppValue q d (VStrs _) = pp "VStrs" ppValue q d (VStrs _) = pp "VStrs"
ppValue q d (VMarkup _ _ _) = pp "VMarkup" ppValue q d (VMarkup _ _ _) = pp "VMarkup"
@@ -912,26 +1036,26 @@ value2string' g VEmpty b ws qs = Const (b,ws,qs)
value2string' g (VC v1 v2) b ws qs = concat v1 (value2string' g v2 b ws qs) value2string' g (VC v1 v2) b ws qs = concat v1 (value2string' g v2 b ws qs)
where where
concat v1 (Const (b,ws,qs)) = value2string' g v1 b ws qs concat v1 (Const (b,ws,qs)) = value2string' g v1 b ws qs
concat v1 (CFV i vs) = CFV i [concat v1 v2 | v2 <- vs] concat v1 (CFV i vs) = CFV i (mapConstVs (concat v1) vs)
concat v1 res = res concat v1 res = res
value2string' g (VApp q []) b ws qs value2string' g (VApp c q []) b ws qs
| q == (cPredef,cNonExist) = NonExist | q == (cPredef,cNonExist) = NonExist
value2string' g (VApp q []) b ws qs value2string' g (VApp c q []) b ws qs
| q == (cPredef,cSOFT_SPACE) = if null ws | q == (cPredef,cSOFT_SPACE) = if null ws
then Const (b,ws,q:qs) then Const (b,ws,q:qs)
else Const (b,ws,qs) else Const (b,ws,qs)
value2string' g (VApp q []) b ws qs value2string' g (VApp c q []) b ws qs
| q == (cPredef,cBIND) || q == (cPredef,cSOFT_BIND) | q == (cPredef,cBIND) || q == (cPredef,cSOFT_BIND)
= if null ws = if null ws
then Const (True,ws,q:qs) then Const (True,ws,q:qs)
else Const (True,ws,qs) else Const (True,ws,qs)
value2string' g (VApp q []) b ws qs value2string' g (VApp c q []) b ws qs
| q == (cPredef,cCAPIT) = capit ws | q == (cPredef,cCAPIT) = capit ws
where where
capit [] = Const (b,[],q:qs) capit [] = Const (b,[],q:qs)
capit ((c:cs) : ws) = Const (b,(toUpper c : cs) : ws,qs) capit ((c:cs) : ws) = Const (b,(toUpper c : cs) : ws,qs)
capit ws = Const (b,ws,qs) capit ws = Const (b,ws,qs)
value2string' g (VApp q []) b ws qs value2string' g (VApp c q []) b ws qs
| q == (cPredef,cALL_CAPIT) = all_capit ws | q == (cPredef,cALL_CAPIT) = all_capit ws
where where
all_capit [] = Const (b,[],q:qs) all_capit [] = Const (b,[],q:qs)
@@ -946,7 +1070,7 @@ value2string' g (VAlts vd vas) b ws qs =
| or [startsWith s w | VStr s <- ss] = value2string' g v | or [startsWith s w | VStr s <- ss] = value2string' g v
| otherwise = pre vd vas w | otherwise = pre vd vas w
value2string' g (VFV s vs) b ws qs = value2string' g (VFV s vs) b ws qs =
CFV s [value2string' g v b ws qs | v <- vs] CFV s (variants2consts (\v -> value2string' g v b ws qs) vs)
value2string' _ _ _ _ _ = RunTime value2string' _ _ _ _ _ = RunTime
startsWith [] _ = True startsWith [] _ = True
@@ -963,17 +1087,24 @@ string2value' (w:ws) = VC (VStr w) (string2value' ws)
value2int g (VMeta i vs) = CSusp i (\v -> value2int g (apply g v vs)) value2int g (VMeta i vs) = CSusp i (\v -> value2int g (apply g v vs))
value2int g (VSusp i k vs) = CSusp i (\v -> value2int g (apply g (k v) vs)) value2int g (VSusp i k vs) = CSusp i (\v -> value2int g (apply g (k v) vs))
value2int g (VInt n) = Const n value2int g (VInt n) = Const n
value2int g (VFV s vs) = CFV s (map (value2int g) vs) value2int g (VFV s vs) = CFV s (variants2consts (value2int g) vs)
value2int g _ = RunTime value2int g _ = RunTime
newtype Choice = Choice Integer deriving (Eq,Ord,Pretty,Show) newtype Choice = Choice { unchoice :: Integer }
deriving (Eq,Ord,Pretty,Show)
unit :: Choice unit :: Choice
unit = Choice 1 unit = Choice 1
poison :: Choice
poison = Choice (-1)
split :: Choice -> (Choice,Choice) split :: Choice -> (Choice,Choice)
split (Choice c) = (Choice (2*c), Choice (2*c+1)) split (Choice c) = (Choice (2*c), Choice (2*c+1))
split3 :: Choice -> (Choice,Choice,Choice)
split3 (Choice c) = (Choice (4*c), Choice (4*c+1), Choice (2*c+1))
split4 :: Choice -> (Choice,Choice,Choice,Choice) split4 :: Choice -> (Choice,Choice,Choice,Choice)
split4 (Choice c) = (Choice (4*c), Choice (4*c+1), Choice (4*c+2), Choice (4*c+3)) split4 (Choice c) = (Choice (4*c), Choice (4*c+1), Choice (4*c+2), Choice (4*c+3))
@@ -993,15 +1124,3 @@ mapCM f c (x:xs) = do
y <- f c1 x y <- f c1 x
ys <- mapCM f c2 xs ys <- mapCM f c2 xs
return (y:ys) return (y:ys)
pdArity :: Int -> PredefCombinator Value
pdArity n def = \g c args ->
case splitAt' n args of
Nothing -> RunTime
Just (usedArgs, remArgs) ->
fmap (\v -> apply g v remArgs) (def g c usedArgs)
where
abstract i n t
| n <= 0 = t
| otherwise = let x = identV (rawIdentS "a") i
in Abs Explicit x (abstract (i + 1) (n - 1) (App t (Vr x)))

243
src/compiler/api/GF/Compile/Repl.hs
View File

@@ -1,24 +1,40 @@
{-# LANGUAGE LambdaCase #-} {-# LANGUAGE LambdaCase, TupleSections, NamedFieldPuns #-}
module GF.Compile.Repl (ReplOpts(..), defaultReplOpts, replOptDescrs, getReplOpts, runRepl, runRepl') where module GF.Compile.Repl (ReplOpts(..), defaultReplOpts, replOptDescrs, getReplOpts, runRepl, runRepl') where
import Control.Monad (unless, forM_, foldM) import Control.Monad (join, when, unless, forM_, foldM)
import Control.Monad.IO.Class (MonadIO) import Control.Monad.IO.Class (MonadIO)
import qualified Data.ByteString.Char8 as BS import qualified Data.ByteString.Char8 as BS
import Data.Char (isSpace) import Data.Char (isSpace)
import Data.Function ((&)) import Data.Function ((&))
import Data.Functor ((<&>)) import Data.Functor ((<&>))
import Data.List (find)
import qualified Data.Map as Map import qualified Data.Map as Map
import Data.Maybe (fromMaybe)
import Text.Read (readMaybe)
import System.Console.GetOpt (ArgOrder(RequireOrder), OptDescr(..), ArgDescr(..), getOpt, usageInfo) import System.Console.GetOpt (ArgOrder(RequireOrder), OptDescr(..), ArgDescr(..), getOpt, usageInfo)
import System.Console.Haskeline (InputT, Settings(..), noCompletion, runInputT, getInputLine, outputStrLn) import System.Console.Haskeline (InputT, Settings(..), noCompletion, runInputT, getInputLine, outputStrLn)
import System.Directory (getAppUserDataDirectory) import System.Directory (getAppUserDataDirectory)
import GF.Compile (batchCompile) import GF.Compile (batchCompile)
import GF.Compile.Compute.Concrete2 (Globals(Gl), stdPredef, normalFlatForm) import GF.Compile.Compute.Concrete2
( Choice(..)
, ChoiceMap
, Globals(Gl)
, OptionInfo(..)
, stdPredef
, unit
, eval
, cleanOptions
, runEvalMWithOpts
, value2termM
, ppValue
)
import GF.Compile.Rename (renameSourceTerm) import GF.Compile.Rename (renameSourceTerm)
import GF.Compile.TypeCheck.ConcreteNew (inferLType) import GF.Compile.TypeCheck.ConcreteNew (inferLType)
import GF.Data.ErrM (Err(..)) import GF.Data.ErrM (Err(..))
import GF.Data.Utilities (maybeAt, orLeft)
import GF.Grammar.Grammar import GF.Grammar.Grammar
( Grammar ( Grammar
, mGrammar , mGrammar
@@ -33,7 +49,7 @@ import GF.Grammar.Grammar
, Term(Typed) , Term(Typed)
, prependModule , prependModule
) )
import GF.Grammar.Lexer (Posn(..), Lang(GF), runLangP) import GF.Grammar.Lexer (Posn(..), Lang(..), runLangP)
import GF.Grammar.Parser (pTerm) import GF.Grammar.Parser (pTerm)
import GF.Grammar.Printer (TermPrintQual(Unqualified), ppTerm) import GF.Grammar.Printer (TermPrintQual(Unqualified), ppTerm)
import GF.Infra.CheckM (Check, runCheck) import GF.Infra.CheckM (Check, runCheck)
@@ -41,14 +57,22 @@ import GF.Infra.Ident (moduleNameS)
import GF.Infra.Option (noOptions) import GF.Infra.Option (noOptions)
import GF.Infra.UseIO (justModuleName) import GF.Infra.UseIO (justModuleName)
import GF.Text.Pretty (render) import GF.Text.Pretty (render)
import Debug.Trace
data ReplOpts = ReplOpts data ReplOpts = ReplOpts
{ noPrelude :: Bool { lang :: Lang
, noPrelude :: Bool
, inputFiles :: [String] , inputFiles :: [String]
, evalToFlat :: Bool
} }
defaultReplOpts :: ReplOpts defaultReplOpts :: ReplOpts
defaultReplOpts = ReplOpts False [] defaultReplOpts = ReplOpts
{ lang = GF
, noPrelude = False
, inputFiles = []
, evalToFlat = True
}
type Errs a = Either [String] a type Errs a = Either [String] a
type ReplOptsOp = ReplOpts -> Errs ReplOpts type ReplOptsOp = ReplOpts -> Errs ReplOpts
@@ -57,6 +81,14 @@ replOptDescrs :: [OptDescr ReplOptsOp]
replOptDescrs = replOptDescrs =
[ Option ['h'] ["help"] (NoArg $ \o -> Left [usageInfo "gfci" replOptDescrs]) "Display help." [ Option ['h'] ["help"] (NoArg $ \o -> Left [usageInfo "gfci" replOptDescrs]) "Display help."
, Option [] ["no-prelude"] (flag $ \o -> o { noPrelude = True }) "Don't load the prelude." , Option [] ["no-prelude"] (flag $ \o -> o { noPrelude = True }) "Don't load the prelude."
, Option [] ["lang"] (ReqArg (\s o -> case s of
"gf" -> Right (o { lang = GF })
"bnfc" -> Right (o { lang = BNFC })
"nlg" -> Right (o { lang = NLG })
_ -> Left ["Unknown language variant: " ++ s])
"{gf,bnfc,nlg}")
"Set the active language variant."
, Option [] ["no-flat"] (flag $ \o -> o { evalToFlat = False }) "Do not evaluate to flat form."
] ]
where where
flag f = NoArg $ \o -> pure (f o) flag f = NoArg $ \o -> pure (f o)
@@ -68,12 +100,14 @@ getReplOpts args = case errs of
where where
(flags, inputFiles, errs) = getOpt RequireOrder replOptDescrs args (flags, inputFiles, errs) = getOpt RequireOrder replOptDescrs args
execCheck :: MonadIO m => Check a -> (a -> InputT m ()) -> InputT m () execCheck :: MonadIO m => Check a -> (a -> InputT m b) -> InputT m (Maybe b)
execCheck c k = case runCheck c of execCheck c k = case runCheck c of
Ok (a, warn) -> do Ok (a, warn) -> do
unless (null warn) $ outputStrLn warn unless (null warn) $ outputStrLn warn
k a Just <$> k a
Bad err -> outputStrLn err Bad err -> do
outputStrLn err
return Nothing
replModNameStr :: String replModNameStr :: String
replModNameStr = "<repl>" replModNameStr = "<repl>"
@@ -81,47 +115,182 @@ replModNameStr = "<repl>"
replModName :: ModuleName replModName :: ModuleName
replModName = moduleNameS replModNameStr replModName = moduleNameS replModNameStr
parseThen :: MonadIO m => Grammar -> String -> (Term -> InputT m ()) -> InputT m () parseThen :: MonadIO m => Lang -> Grammar -> String -> (Term -> InputT m b) -> InputT m (Maybe b)
parseThen g s k = case runLangP GF pTerm (BS.pack s) of parseThen l g s k = case runLangP l pTerm (BS.pack s) of
Left (Pn l c, err) -> outputStrLn $ err ++ " (" ++ show l ++ ":" ++ show c ++ ")" Left (Pn l c, err) -> do
outputStrLn $ err ++ " (" ++ show l ++ ":" ++ show c ++ ")"
return Nothing
Right t -> execCheck (renameSourceTerm g replModName t) $ \t -> k t Right t -> execCheck (renameSourceTerm g replModName t) $ \t -> k t
runRepl' :: Globals -> IO () data ResultState = ResultState
runRepl' gl@(Gl g _) = do { srsResult :: Term
historyFile <- getAppUserDataDirectory "gfci_history" , srsChoices :: ChoiceMap
runInputT (Settings noCompletion (Just historyFile) True) repl -- TODO tab completion , srsOptInfo :: [OptionInfo]
where , srsOpts :: ChoiceMap
repl = do }
getInputLine "gfci> " >>= \case data OptionState = OptionState
Nothing -> repl { osTerm :: Term
Just (':' : l) -> let (cmd, arg) = break isSpace l in command cmd (dropWhile isSpace arg) , osResults :: [ResultState]
Just code -> evalPrintLoop code , osSelected :: Maybe ResultState
}
newtype ReplState = ReplState
{ rsOpts :: Maybe OptionState
}
command "t" arg = do initState :: ReplState
parseThen g arg $ \main -> initState = ReplState Nothing
runRepl' :: ReplOpts -> Globals -> IO ()
runRepl' opts@ReplOpts { lang, evalToFlat } gl@(Gl g _) = do
historyFile <- getAppUserDataDirectory "gfci_history"
runInputT (Settings noCompletion (Just historyFile) True) (repl initState) -- TODO tab completion
where
repl st = do
getInputLine "gfci> " >>= \case
Nothing -> repl st
Just (':' : l) -> let (cmd, arg) = break isSpace l in command st cmd (dropWhile isSpace arg)
Just code -> evalPrintLoop st code
nlrepl st = outputStrLn "" >> repl st
-- Show help text
command st "?" arg = do
outputStrLn ":? -- show help text."
outputStrLn ":t <expr> -- show the inferred type of <expr>."
outputStrLn ":r -- show the results of the last eval."
outputStrLn ":s <index> -- select the result at <index>."
outputStrLn ":c -- show the current selected result."
outputStrLn ":o <choice> <value> -- set option <choice> to <value>."
outputStrLn ":q -- quit the REPL."
nlrepl st
-- Show the inferred type of an expression
command st "t" arg = do
parseThen lang g arg $ \main ->
execCheck (inferLType gl main) $ \res -> execCheck (inferLType gl main) $ \res ->
forM_ res $ \(t, ty) -> forM_ res $ \(t, ty) ->
let t' = case t of let t' = case t of
Typed _ _ -> t Typed _ _ -> t
t -> Typed t ty t -> Typed t ty
in outputStrLn $ render (ppTerm Unqualified 0 t') in outputStrLn $ render (ppTerm Unqualified 0 t')
outputStrLn "" >> repl nlrepl st
command "q" _ = outputStrLn "Bye!" -- Show the results of the last evaluated expression
command st "r" arg = do
case rsOpts st of
Nothing -> do
outputStrLn "No results to show!"
Just (OptionState t rs _) -> do
outputStrLn $ "> " ++ render (ppTerm Unqualified 0 t)
outputResults rs
nlrepl st
command cmd _ = do -- Select a result to "focus" by its index
outputStrLn $ "Unknown REPL command: " ++ cmd command st "s" arg = do
outputStrLn "" >> repl let e = do (OptionState t rs _) <- orLeft "No results to select!" $ rsOpts st
s <- orLeft "Could not parse result index!" $ readMaybe arg
(ResultState r cs ois os) <- orLeft "Result index out of bounds!" $ rs `maybeAt` (s - 1)
return (t, rs, r, cs, ois, os)
case e of
Left err -> do
outputStrLn err
nlrepl st
Right (t, rs, r, cs, ois, os) -> do
outputStrLn $ render (ppTerm Unqualified 0 r)
outputOptions ois os
nlrepl (st { rsOpts = Just (OptionState t rs (Just (ResultState r cs ois os))) })
evalPrintLoop code = do -- TODO bindings -- Show the current selected result
parseThen g code $ \main -> command st "c" arg = do
execCheck (inferLType gl main >>= \((t, _):_) -> normalFlatForm gl t) $ \nfs -> let e = do (OptionState t _ sel) <- orLeft "No results to select!" $ rsOpts st
forM_ (zip [1..] nfs) $ \(i, nf) -> (ResultState r _ ois os) <- orLeft "No result selected!" sel
outputStrLn $ show i ++ ". " ++ render (ppTerm Unqualified 0 nf) return (t, r, ois, os)
outputStrLn "" >> repl case e of
Left err -> outputStrLn err
Right (t, r, ois, os) -> do
outputStrLn $ "> " ++ render (ppTerm Unqualified 0 t)
outputStrLn $ render (ppTerm Unqualified 0 r)
outputOptions ois os
nlrepl st
-- Set an option for the selected result
command st "o" arg = do
let e = do (OptionState t _ sel) <- orLeft "No results to select!" $ rsOpts st
(ResultState _ cs ois os) <- orLeft "No result selected!" sel
(c, i) <- case words arg of
[argc, argi] -> do
c <- orLeft "Could not parse option choice!" $ readMaybe argc
i <- orLeft "Could not parse option value!" $ readMaybe argi
return (c, i)
_ -> Left "Expected two arguments!"
when (i < 1) $ Left "Option value must be positive!"
oi <- orLeft "No such option!" $ find (\oi -> unchoice (optChoice oi) == c) ois
when (i > length (optChoices oi)) $ Left "Option value out of bounds!"
return (t, cs, ois, os, c, i)
case e of
Left err -> do
outputStrLn err
nlrepl st
Right (t, cs, ois, os, c, i) -> do
let os' = Map.insert (Choice c) (i - 1) os
nfs <- execCheck (doEval st t (Map.union os' cs)) pure
case nfs of
Nothing -> nlrepl st
Just [] -> do
outputStrLn "No results!"
nlrepl st
Just [(r, cs, ois')] -> do
outputStrLn $ render (ppTerm Unqualified 0 r)
let os'' = cleanOptions ois' os'
outputOptions ois' os''
let rst = ResultState r (Map.difference cs os') ois' os''
nlrepl (st { rsOpts = Just (OptionState t [rst] (Just rst)) })
Just rs -> do
let rsts = rs <&> \(r, cs, ois') ->
ResultState r (Map.difference cs os') ois' (cleanOptions ois' os')
outputResults rsts
nlrepl (st { rsOpts = Just (OptionState t rsts Nothing) })
-- Quit the REPL
command _ "q" _ = outputStrLn "Bye!"
command st cmd _ = do
outputStrLn $ "Unknown REPL command \"" ++ cmd ++ "\"! Use :? for help."
nlrepl st
evalPrintLoop st code = do -- TODO bindings
c <- parseThen lang g code $ \main -> do
rsts <- execCheck (doEval st main Map.empty) $ \nfs -> do
if null nfs then do
outputStrLn "No results!"
return Nothing
else do
let rsts = nfs <&> \(r, cs, ois) -> ResultState r cs ois Map.empty
outputResults rsts
return $ Just rsts
return $ (main,) <$> join rsts
case join c of
Just (t, rs) -> nlrepl (ReplState (Just (OptionState t rs Nothing)))
Nothing -> nlrepl st
doEval st t opts = inferLType gl t >>= \case
[] -> fail $ "No result while checking type: " ++ render (ppTerm Unqualified 0 t)
((t', _):_) -> runEvalMWithOpts gl opts (value2termM evalToFlat [] (eval gl [] unit t' []))
outputResults rs =
forM_ (zip [1..] rs) $ \(i, ResultState r _ opts _) ->
outputStrLn $ show i ++ (if null opts then ". " else "*. ") ++ render (ppTerm Unqualified 0 r)
outputOptions ois os =
forM_ ois $ \(OptionInfo c n ls) -> do
outputStrLn ""
outputStrLn $ show (unchoice c) ++ ") " ++ render (ppValue Unqualified 0 n)
let sel = fromMaybe 0 (Map.lookup c os) + 1
forM_ (zip [1..] ls) $ \(i, l) ->
outputStrLn $ (if i == sel then "->" else " ") ++ show i ++ ". " ++ render (ppValue Unqualified 0 l)
runRepl :: ReplOpts -> IO () runRepl :: ReplOpts -> IO ()
runRepl (ReplOpts noPrelude inputFiles) = do runRepl opts@ReplOpts { noPrelude, inputFiles } = do
-- TODO accept an ngf grammar -- TODO accept an ngf grammar
let toLoad = if noPrelude then inputFiles else "prelude/Predef.gfo" : inputFiles let toLoad = if noPrelude then inputFiles else "prelude/Predef.gfo" : inputFiles
(g0, opens) <- case toLoad of (g0, opens) <- case toLoad of
@@ -143,4 +312,4 @@ runRepl (ReplOpts noPrelude inputFiles) = do
, jments = Map.empty , jments = Map.empty
} }
g = Gl (prependModule g0 (replModName, modInfo)) (if noPrelude then Map.empty else stdPredef g) g = Gl (prependModule g0 (replModName, modInfo)) (if noPrelude then Map.empty else stdPredef g)
runRepl' g runRepl' opts g

116
src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs
View File

@@ -21,6 +21,7 @@ import Data.STRef
import Data.List (nub, (\\), tails) import Data.List (nub, (\\), tails)
import qualified Data.Map as Map import qualified Data.Map as Map
import Data.Maybe(fromMaybe,isNothing,mapMaybe) import Data.Maybe(fromMaybe,isNothing,mapMaybe)
import Data.Bifunctor(second)
import Data.Functor((<&>)) import Data.Functor((<&>))
import qualified Control.Monad.Fail as Fail import qualified Control.Monad.Fail as Fail
@@ -57,14 +58,14 @@ inferSigma scope s t = do -- GEN1
let forall_tvs = res_tvs \\ env_tvs let forall_tvs = res_tvs \\ env_tvs
quantify scope t forall_tvs ty quantify scope t forall_tvs ty
vtypeInt = VApp (cPredef,cInt) [] vtypeInt = VApp poison (cPredef,cInt) []
vtypeFloat = VApp (cPredef,cFloat) [] vtypeFloat = VApp poison (cPredef,cFloat) []
vtypeInts i= VApp (cPredef,cInts) [VInt i] vtypeInts i= VApp poison (cPredef,cInts) [VInt i]
vtypeStr = VSort cStr vtypeStr = VSort cStr
vtypeStrs = VSort cStrs vtypeStrs = VSort cStrs
vtypeType = VSort cType vtypeType = VSort cType
vtypePType = VSort cPType vtypePType = VSort cPType
vtypeMarkup= VApp (cPredef,cMarkup) [] vtypeMarkup= VApp poison (cPredef,cMarkup) []
tcRho :: Scope -> Choice -> Term -> Maybe Rho -> EvalM (Term, Rho) tcRho :: Scope -> Choice -> Term -> Maybe Rho -> EvalM (Term, Rho)
tcRho scope s t@(EInt i) mb_ty = instSigma scope s t (vtypeInts i) mb_ty -- INT tcRho scope s t@(EInt i) mb_ty = instSigma scope s t (vtypeInts i) mb_ty -- INT
@@ -90,7 +91,7 @@ tcRho scope c (Abs bt var body) Nothing = do -- ABS1
in return (Abs bt var body, (VProd bt v arg_ty body_ty)) in return (Abs bt var body, (VProd bt v arg_ty body_ty))
else return (Abs bt var body, (VProd bt identW arg_ty body_ty)) else return (Abs bt var body, (VProd bt identW arg_ty body_ty))
where where
check m n st (VApp f vs) = foldM (check m n) st vs check m n st (VApp c f vs) = foldM (check m n) st vs
check m n st (VMeta i vs) = do check m n st (VMeta i vs) = do
state <- getMeta i state <- getMeta i
case state of case state of
@@ -98,8 +99,8 @@ tcRho scope c (Abs bt var body) Nothing = do -- ABS1
check m n st (apply g v vs) check m n st (apply g v vs)
_ -> foldM (check m n) st vs _ -> foldM (check m n) st vs
check m n st@(b,xs) (VGen i vs) check m n st@(b,xs) (VGen i vs)
| i == m = return (True, xs) | i == m = return (True, xs)
| otherwise = return st | otherwise = return st
check m n st (VClosure env c (Abs bt x t)) = do check m n st (VClosure env c (Abs bt x t)) = do
g <- globals g <- globals
check m (n+1) st (eval g ((x,VGen n []):env) c t []) check m (n+1) st (eval g ((x,VGen n []):env) c t [])
@@ -118,7 +119,7 @@ tcRho scope c (Abs bt var body) Nothing = do -- ABS1
check m n st v1 >>= \st -> check m n st v2 check m n st v1 >>= \st -> check m n st v2
check m n st (VTable v1 v2) = check m n st (VTable v1 v2) =
check m n st v1 >>= \st -> check m n st v2 check m n st v1 >>= \st -> check m n st v2
check m n st (VT ty env c cs) = check m n st (VT ty env c cs) =
check m n st ty -- Traverse cs as well check m n st ty -- Traverse cs as well
check m n st (VV ty cs) = check m n st (VV ty cs) =
check m n st ty >>= \st -> foldM (check m n) st cs check m n st ty >>= \st -> foldM (check m n) st cs
@@ -186,17 +187,7 @@ tcRho scope c (Typed body ann_ty) mb_ty = do -- ANNOT
(body,_) <- tcRho scope c3 body (Just v_ann_ty) (body,_) <- tcRho scope c3 body (Just v_ann_ty)
instSigma scope c4 (Typed body ann_ty) v_ann_ty mb_ty instSigma scope c4 (Typed body ann_ty) v_ann_ty mb_ty
tcRho scope c (FV ts) mb_ty = do tcRho scope c (FV ts) mb_ty = do
(ty,subsume) <- (ts,ty) <- tcUnifying scope c ts mb_ty
case mb_ty of
Just ty -> do return (ty, \t ty' -> return t)
Nothing -> do i <- newResiduation scope
let ty = VMeta i []
return (ty, \t ty' -> subsCheckRho scope t ty' ty)
let go c t = do (t, ty) <- tcRho scope c t mb_ty
subsume t ty
ts <- mapCM go c ts
return (FV ts, ty) return (FV ts, ty)
tcRho scope s t@(Sort _) mb_ty = do tcRho scope s t@(Sort _) mb_ty = do
instSigma scope s t vtypeType mb_ty instSigma scope s t vtypeType mb_ty
@@ -389,11 +380,17 @@ tcRho scope c (Reset ctl t) mb_ty =
Limit n -> do (t,_) <- tcRho scope c1 t Nothing Limit n -> do (t,_) <- tcRho scope c1 t Nothing
instSigma scope c2 (Reset ctl t) vtypeMarkup mb_ty instSigma scope c2 (Reset ctl t) vtypeMarkup mb_ty
Coordination mb_mn@(Just mn) conj _ Coordination mb_mn@(Just mn) conj _
-> do tcRho scope c1 (QC (mn,conj)) (Just (VApp (mn,identS "Conj") [])) -> do tcRho scope c1 (QC (mn,conj)) (Just (VApp poison (mn,identS "Conj") []))
(t,ty) <- tcRho scope c2 t mb_ty (t,ty) <- tcRho scope c2 t mb_ty
case ty of case ty of
VApp id [] -> return (Reset (Coordination mb_mn conj (snd id)) t, ty) VApp c id [] -> return (Reset (Coordination mb_mn conj (snd id)) t, ty)
_ -> evalError (pp "Needs atomic type"<+>ppValue Unqualified 0 ty) _ -> evalError (pp "Needs atomic type"<+>ppValue Unqualified 0 ty)
tcRho scope s (Opts n cs) mb_ty = do
let (s1,s2,s3) = split3 s
(n,_) <- tcRho scope s1 n Nothing
(ls,_) <- tcUnifying scope s2 (fst <$> cs) Nothing
(ts,ty) <- tcUnifying scope s3 (snd <$> cs) mb_ty
return (Opts n (zip ls ts), ty)
tcRho scope s t _ = unimplemented ("tcRho "++show t) tcRho scope s t _ = unimplemented ("tcRho "++show t)
evalCodomain :: Scope -> Ident -> Value -> EvalM Value evalCodomain :: Scope -> Ident -> Value -> EvalM Value
@@ -402,6 +399,21 @@ evalCodomain scope x (VClosure env c t) = do
return (eval g ((x,VGen (length scope) []):env) c t []) return (eval g ((x,VGen (length scope) []):env) c t [])
evalCodomain scope x t = return t evalCodomain scope x t = return t
tcUnifying :: Scope -> Choice -> [Term] -> Maybe Rho -> EvalM ([Term], Constraint)
tcUnifying scope c ts mb_ty = do
(ty,subsume) <-
case mb_ty of
Just ty -> do return (ty, \t ty' -> return t)
Nothing -> do i <- newResiduation scope
let ty = VMeta i []
return (ty, \t ty' -> subsCheckRho scope t ty' ty)
let go c t = do (t, ty) <- tcRho scope c t mb_ty
subsume t ty
ts <- mapCM go c ts
return (ts,ty)
tcCases scope c [] p_ty res_ty = return [] tcCases scope c [] p_ty res_ty = return []
tcCases scope c ((p,t):cs) p_ty res_ty = do tcCases scope c ((p,t):cs) p_ty res_ty = do
let (c1,c2,c3,c4) = split4 c let (c1,c2,c3,c4) = split4 c
@@ -690,9 +702,9 @@ subsCheckRho scope t (VTable p1 r1) rho2 = do -- Rule TABLE
subsCheckTbl scope t p1 r1 p2 r2 subsCheckTbl scope t p1 r1 p2 r2
subsCheckRho scope t (VSort s1) (VSort s2) -- Rule PTYPE subsCheckRho scope t (VSort s1) (VSort s2) -- Rule PTYPE
| s1 == cPType && s2 == cType = return t | s1 == cPType && s2 == cType = return t
subsCheckRho scope t (VApp p1 _) (VApp p2 _) -- Rule INT1 subsCheckRho scope t (VApp _ p1 _) (VApp _ p2 _) -- Rule INT1
| p1 == (cPredef,cInts) && p2 == (cPredef,cInt) = return t | p1 == (cPredef,cInts) && p2 == (cPredef,cInt) = return t
subsCheckRho scope t (VApp p1 [VInt i]) (VApp p2 [VInt j]) -- Rule INT2 subsCheckRho scope t (VApp _ p1 [VInt i]) (VApp _ p2 [VInt j]) -- Rule INT2
| p1 == (cPredef,cInts) && p2 == (cPredef,cInts) = do | p1 == (cPredef,cInts) && p2 == (cPredef,cInts) = do
if i <= j if i <= j
then return t then return t
@@ -736,10 +748,10 @@ subsCheckRho scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do -- Rule REC
"there are no values for fields:" <+> hsep missing) "there are no values for fields:" <+> hsep missing)
rs <- sequence [mkField scope l t ty1 ty2 | (l,ty2,Just ty1) <- fields, Just t <- [mkProj l]] rs <- sequence [mkField scope l t ty1 ty2 | (l,ty2,Just ty1) <- fields, Just t <- [mkProj l]]
return (mkWrap (R rs)) return (mkWrap (R rs))
subsCheckRho scope t tau1 (VFV c vs) = do subsCheckRho scope t tau1 (VFV c (VarFree vs)) = do
tau2 <- variants c vs tau2 <- variants c vs
subsCheckRho scope t tau1 tau2 subsCheckRho scope t tau1 tau2
subsCheckRho scope t (VFV c vs) tau2 = do subsCheckRho scope t (VFV c (VarFree vs)) tau2 = do
tau1 <- variants c vs tau1 <- variants c vs
subsCheckRho scope t tau1 tau2 subsCheckRho scope t tau1 tau2
subsCheckRho scope t tau1 tau2 = do -- Rule EQ subsCheckRho scope t tau1 tau2 = do -- Rule EQ
@@ -751,13 +763,13 @@ subsCheckFun scope t a1 r1 a2 r2 = do
let v = newVar scope let v = newVar scope
vt <- subsCheckRho ((v,a2):scope) (Vr v) a2 a1 vt <- subsCheckRho ((v,a2):scope) (Vr v) a2 a1
g <- globals g <- globals
let r1 = case r1 of let r1' = case r1 of
VClosure env c r1 -> eval g ((v,(VGen (length scope) [])):env) c r1 [] VClosure env c r1 -> eval g ((v,(VGen (length scope) [])):env) c r1 []
r1 -> r1 r1 -> r1
let r2 = case r2 of r2' = case r2 of
VClosure env c r2 -> eval g ((v,(VGen (length scope) [])):env) c r2 [] VClosure env c r2 -> eval g ((v,(VGen (length scope) [])):env) c r2 []
r2 -> r2 r2 -> r2
t <- subsCheckRho ((v,vtypeType):scope) (App t vt) r1 r2 t <- subsCheckRho ((v,vtypeType):scope) (App t vt) r1' r2'
return (Abs Explicit v t) return (Abs Explicit v t)
subsCheckTbl :: Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> EvalM Term subsCheckTbl :: Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> EvalM Term
@@ -768,10 +780,10 @@ subsCheckTbl scope t p1 r1 p2 r2 = do
p2 <- value2termM True (scopeVars scope) p2 p2 <- value2termM True (scopeVars scope) p2
return (T (TTyped p2) [(PV x,t)]) return (T (TTyped p2) [(PV x,t)])
subtype scope Nothing (VApp p [VInt i]) subtype scope Nothing (VApp c p [VInt i])
| p == (cPredef,cInts) = do | p == (cPredef,cInts) = do
return (VCInts Nothing (Just i)) return (VCInts Nothing (Just i))
subtype scope (Just (VCInts i j)) (VApp p [VInt k]) subtype scope (Just (VCInts i j)) (VApp c p [VInt k])
| p == (cPredef,cInts) = do | p == (cPredef,cInts) = do
return (VCInts j (Just (maybe k (min k) i))) return (VCInts j (Just (maybe k (min k) i)))
subtype scope Nothing (VRecType ltys) = do subtype scope Nothing (VRecType ltys) = do
@@ -793,10 +805,10 @@ subtype scope (Just ctr) ty = do
unify scope ctr ty unify scope ctr ty
return ty return ty
supertype scope Nothing (VApp p [VInt i]) supertype scope Nothing (VApp c p [VInt i])
| p == (cPredef,cInts) = do | p == (cPredef,cInts) = do
return (VCInts (Just i) Nothing) return (VCInts (Just i) Nothing)
supertype scope (Just (VCInts i j)) (VApp p [VInt k]) supertype scope (Just (VCInts i j)) (VApp c p [VInt k])
| p == (cPredef,cInts) = do | p == (cPredef,cInts) = do
return (VCInts (Just (maybe k (max k) i)) j) return (VCInts (Just (maybe k (max k) i)) j)
supertype scope Nothing (VRecType ltys) = do supertype scope Nothing (VRecType ltys) = do
@@ -823,9 +835,14 @@ supertype scope (Just ctr) ty = do
unifyFun :: Scope -> Rho -> EvalM (BindType, Ident, Sigma, Rho) unifyFun :: Scope -> Rho -> EvalM (BindType, Ident, Sigma, Rho)
unifyFun scope (VProd bt x arg res) = unifyFun scope (VProd bt x arg res) =
return (bt,x,arg,res) return (bt,x,arg,res)
unifyFun scope (VFV c vs) = do unifyFun scope (VFV c (VarFree vs)) = do
res <- mapM (unifyFun scope) vs res <- mapM (unifyFun scope) vs
return (Explicit, identW, VFV c [sigma | (_,_,sigma,rho) <- res], VFV c [rho | (_,_,sigma,rho) <- res]) return
( Explicit
, identW
, VFV c (VarFree [sigma | (_,_,sigma,rho) <- res])
, VFV c (VarFree [rho | (_,_,sigma,rho) <- res])
)
unifyFun scope tau = do unifyFun scope tau = do
let mk_val i = VMeta i [] let mk_val i = VMeta i []
arg <- fmap mk_val $ newResiduation scope arg <- fmap mk_val $ newResiduation scope
@@ -844,7 +861,7 @@ unifyTbl scope tau = do
unify scope tau (VTable arg res) unify scope tau (VTable arg res)
return (arg,res) return (arg,res)
unify scope (VApp f1 vs1) (VApp f2 vs2) unify scope (VApp c1 f1 vs1) (VApp c2 f2 vs2)
| f1 == f2 = sequence_ (zipWith (unify scope) vs1 vs2) | f1 == f2 = sequence_ (zipWith (unify scope) vs1 vs2)
unify scope (VMeta i vs1) (VMeta j vs2) unify scope (VMeta i vs1) (VMeta j vs2)
| i == j = sequence_ (zipWith (unify scope) vs1 vs2) | i == j = sequence_ (zipWith (unify scope) vs1 vs2)
@@ -910,7 +927,7 @@ occursCheck scope' i0 scope v =
n = length scope n = length scope
in check m n v in check m n v
where where
check m n (VApp f vs) = mapM_ (check m n) vs check m n (VApp c f vs) = mapM_ (check m n) vs
check m n (VMeta i vs) check m n (VMeta i vs)
| i0 == i = do ty1 <- value2termM False (scopeVars scope) (VMeta i vs) | i0 == i = do ty1 <- value2termM False (scopeVars scope) (VMeta i vs)
ty2 <- value2termM False (scopeVars scope) v ty2 <- value2termM False (scopeVars scope) v
@@ -964,7 +981,7 @@ occursCheck scope' i0 scope v =
check m n (VPattType v) = check m n (VPattType v) =
check m n v check m n v
check m n (VFV c vs) = check m n (VFV c vs) =
mapM_ (check m n) vs mapM_ (check m n) (unvariants vs)
check m n (VAlts v vs) = check m n (VAlts v vs) =
check m n v >> mapM_ (\(v1,v2) -> check m n v1 >> check m n v2) vs check m n v >> mapM_ (\(v1,v2) -> check m n v1 >> check m n v2) vs
check m n (VStrs vs) = check m n (VStrs vs) =
@@ -1019,9 +1036,9 @@ quantify scope t tvs ty = do
where where
bind scope (i, meta_id, name) = setMeta meta_id (Bound scope (VGen i [])) bind scope (i, meta_id, name) = setMeta meta_id (Bound scope (VGen i []))
check m n xs (VApp f vs) = do check m n xs (VApp c f vs) = do
(xs,vs) <- mapAccumM (check m n) xs vs (xs,vs) <- mapAccumM (check m n) xs vs
return (xs,VApp f vs) return (xs,VApp c f vs)
check m n xs (VMeta i vs) = do check m n xs (VMeta i vs) = do
s <- getMeta i s <- getMeta i
case s of case s of
@@ -1090,9 +1107,12 @@ quantify scope t tvs ty = do
check m n xs (VPattType v) = do check m n xs (VPattType v) = do
(xs,v) <- check m n xs v (xs,v) <- check m n xs v
return (xs,VPattType v) return (xs,VPattType v)
check m n xs (VFV c vs) = do check m n xs (VFV c (VarFree vs)) = do
(xs,vs) <- mapAccumM (check m n) xs vs (xs,vs) <- mapAccumM (check m n) xs vs
return (xs,VFV c vs) return (xs,VFV c (VarFree vs))
check m n xs (VFV c (VarOpts name os)) = do
(xs,os) <- mapAccumM (\acc (l,v) -> second (l,) <$> check m n acc v) xs os
return (xs,VFV c (VarOpts name os))
check m n xs (VAlts v vs) = do check m n xs (VAlts v vs) = do
(xs,v) <- check m n xs v (xs,v) <- check m n xs v
(xs,vs) <- mapAccumM (\xs (v1,v2) -> do (xs,v1) <- check m n xs v1 (xs,vs) <- mapAccumM (\xs (v1,v2) -> do (xs,v1) <- check m n xs v1
@@ -1159,8 +1179,8 @@ getMetaVars sc_tys = foldM (\acc (scope,ty) -> go acc ty) [] sc_tys
Residuation _ Nothing -> foldM go (m:acc) args Residuation _ Nothing -> foldM go (m:acc) args
Residuation _ (Just v) -> go acc v Residuation _ (Just v) -> go acc v
_ -> return acc _ -> return acc
go acc (VApp f args) = foldM go acc args go acc (VApp c f args) = foldM go acc args
go acc (VFV c vs) = foldM go acc vs go acc (VFV c vs) = foldM go acc (unvariants vs)
go acc (VCRecType vs) = foldM (\acc (lbl,b,v) -> go acc v) acc vs go acc (VCRecType vs) = foldM (\acc (lbl,b,v) -> go acc v) acc vs
go acc (VCInts _ _) = return acc go acc (VCInts _ _) = return acc
go acc v = unimplemented ("go "++show (ppValue Unqualified 5 v)) go acc v = unimplemented ("go "++show (ppValue Unqualified 5 v))

10
src/compiler/api/GF/Data/Utilities.hs
View File

@@ -32,6 +32,11 @@ notLongerThan, longerThan :: Int -> [a] -> Bool
notLongerThan n = null . snd . splitAt n notLongerThan n = null . snd . splitAt n
longerThan n = not . notLongerThan n longerThan n = not . notLongerThan n
maybeAt :: [a] -> Int -> Maybe a
maybeAt xs i
| i >= 0 && i < length xs = Just (xs !! i)
| otherwise = Nothing
lookupList :: Eq a => a -> [(a, b)] -> [b] lookupList :: Eq a => a -> [(a, b)] -> [b]
lookupList a [] = [] lookupList a [] = []
lookupList a (p:ps) | a == fst p = snd p : lookupList a ps lookupList a (p:ps) | a == fst p = snd p : lookupList a ps
@@ -171,6 +176,11 @@ anyM p = foldM (\b x -> if b then return True else p x) False
-- * functions on Maybes -- * functions on Maybes
-- | Returns the argument on the right, or a default value on the left.
orLeft :: a -> Maybe b -> Either a b
orLeft a (Just b) = Right b
orLeft a Nothing = Left a
-- | Returns true if the argument is Nothing or Just [] -- | Returns true if the argument is Nothing or Just []
nothingOrNull :: Maybe [a] -> Bool nothingOrNull :: Maybe [a] -> Bool
nothingOrNull = maybe True null nothingOrNull = maybe True null

6
src/compiler/api/GF/Grammar/Grammar.hs
View File

@@ -54,6 +54,7 @@ module GF.Grammar.Grammar (
Equation, Equation,
Labelling, Labelling,
Assign, Assign,
Option,
Case, Case,
LocalDef, LocalDef,
Param, Param,
@@ -372,7 +373,9 @@ data Term =
| R [Assign] -- ^ record: @{ p = a ; ...}@ | R [Assign] -- ^ record: @{ p = a ; ...}@
| P Term Label -- ^ projection: @r.p@ | P Term Label -- ^ projection: @r.p@
| ExtR Term Term -- ^ extension: @R ** {x : A}@ (both types and terms) | ExtR Term Term -- ^ extension: @R ** {x : A}@ (both types and terms)
| Opts Term [Option] -- ^ options: @options s in { e => x ; ... }@
| Table Term Term -- ^ table type: @P => A@ | Table Term Term -- ^ table type: @P => A@
| T TInfo [Case] -- ^ table: @table {p => c ; ...}@ | T TInfo [Case] -- ^ table: @table {p => c ; ...}@
| V Type [Term] -- ^ table given as course of values: @table T [c1 ; ... ; cn]@ | V Type [Term] -- ^ table given as course of values: @table T [c1 ; ... ; cn]@
@@ -471,6 +474,7 @@ type Equation = ([Patt],Term)
type Labelling = (Label, Type) type Labelling = (Label, Type)
type Assign = (Label, (Maybe Type, Term)) type Assign = (Label, (Maybe Type, Term))
type Option = (Term, Term)
type Case = (Patt, Term) type Case = (Patt, Term)
--type Cases = ([Patt], Term) --type Cases = ([Patt], Term)
type LocalDef = (Ident, (Maybe Type, Term)) type LocalDef = (Ident, (Maybe Type, Term))

29
src/compiler/api/GF/Grammar/Lexer.x
View File

@@ -41,7 +41,7 @@ $u = [.\n] -- universal: any character
"{-" ([$u # \-] | \- [$u # \}])* ("-")+ "}" ; "{-" ([$u # \-] | \- [$u # \}])* ("-")+ "}" ;
$white+ ; $white+ ;
@rsyms { tok ident } @rsyms { \lang -> tok (ident lang) lang }
\< $white* @ident $white* (\/ | \>) \< $white* @ident $white* (\/ | \>)
{ \lang inp@(AI pos s) inp' _ -> { \lang inp@(AI pos s) inp' _ ->
let inp0 = AI (alexMove pos '<') (BS.tail s) let inp0 = AI (alexMove pos '<') (BS.tail s)
@@ -74,7 +74,7 @@ $white+ ;
in POk (inp,inp0) T_less in POk (inp,inp0) T_less
} } } }
\' ([. # [\' \\ \n]] | (\\ (\' | \\)))+ \' { tok (T_Ident . identS . unescapeInitTail . unpack) } \' ([. # [\' \\ \n]] | (\\ (\' | \\)))+ \' { tok (T_Ident . identS . unescapeInitTail . unpack) }
@ident { tok ident } @ident { \lang -> tok (ident lang) lang }
\" ([$u # [\" \\ \n]] | (\\ (\" | \\ | \' | n | t | $d+)))* \" { tok (T_String . unescapeInitTail . unpack) } \" ([$u # [\" \\ \n]] | (\\ (\" | \\ | \' | n | t | $d+)))* \" { tok (T_String . unescapeInitTail . unpack) }
@@ -85,7 +85,7 @@ $white+ ;
{ {
unpack = UTF8.toString unpack = UTF8.toString
ident = res T_Ident . identC . rawIdentC ident lang = res lang T_Ident . identC . rawIdentC
tok f _ inp@(AI _ s) inp' len = POk (inp,inp') (f (UTF8.take len s)) tok f _ inp@(AI _ s) inp' len = POk (inp,inp') (f (UTF8.take len s))
@@ -149,6 +149,7 @@ data Token
| T_of | T_of
| T_open | T_open
| T_oper | T_oper
| T_option
| T_param | T_param
| T_pattern | T_pattern
| T_pre | T_pre
@@ -174,16 +175,20 @@ data Token
deriving Show -- debug deriving Show -- debug
res = eitherResIdent res = eitherResIdent
eitherResIdent :: (Ident -> Token) -> Ident -> Token eitherResIdent :: Lang -> (Ident -> Token) -> Ident -> Token
eitherResIdent tv s = eitherResIdent lang tv s =
case Map.lookup s resWords of case Map.lookup s (resWords lang) of
Just t -> t Just t -> t
Nothing -> tv s Nothing -> tv s
isReservedWord :: Ident -> Bool isReservedWord :: Lang -> Ident -> Bool
isReservedWord ident = Map.member ident resWords isReservedWord lang ident = Map.member ident (resWords lang)
resWords = Map.fromList resWords :: Lang -> Map.Map Ident Token
resWords NLG = nlgResWords
resWords _ = coreResWords
coreResWords = Map.fromList
[ b "!" T_exclmark [ b "!" T_exclmark
, b "#" T_patt , b "#" T_patt
, b "$" T_int_label , b "$" T_int_label
@@ -255,13 +260,17 @@ resWords = Map.fromList
, b "variants" T_variants , b "variants" T_variants
, b "where" T_where , b "where" T_where
, b "with" T_with , b "with" T_with
, b "coercions" T_coercions , b "coercions" T_coercions -- FIXME ..
, b "terminator" T_terminator , b "terminator" T_terminator
, b "separator" T_separator , b "separator" T_separator
, b "nonempty" T_nonempty , b "nonempty" T_nonempty
] ]
where b s t = (identS s, t) where b s t = (identS s, t)
-- bnfcResWords = _
nlgResWords = Map.insert (identS "option") T_option coreResWords
unescapeInitTail :: String -> String unescapeInitTail :: String -> String
unescapeInitTail = unesc . tail where unescapeInitTail = unesc . tail where
unesc s = case s of unesc s = case s of

11
src/compiler/api/GF/Grammar/Parser.y
View File

@@ -101,6 +101,7 @@ import qualified Data.Map as Map
'of' { T_of } 'of' { T_of }
'open' { T_open } 'open' { T_open }
'oper' { T_oper } 'oper' { T_oper }
'option' { T_option }
'param' { T_param } 'param' { T_param }
'pattern' { T_pattern } 'pattern' { T_pattern }
'pre' { T_pre } 'pre' { T_pre }
@@ -452,6 +453,7 @@ Exp4 :: { Term }
Exp4 Exp4
: Exp4 Exp5 { App $1 $2 } : Exp4 Exp5 { App $1 $2 }
| Exp4 '{' Exp '}' { App $1 (ImplArg $3) } | Exp4 '{' Exp '}' { App $1 (ImplArg $3) }
| 'option' Exp 'of' '{' ListOpt '}' { Opts $2 $5 }
| 'case' Exp 'of' '{' ListCase '}' { let annot = case $2 of | 'case' Exp 'of' '{' ListCase '}' { let annot = case $2 of
Typed _ t -> TTyped t Typed _ t -> TTyped t
_ -> TRaw _ -> TRaw
@@ -608,6 +610,15 @@ ListPattTupleComp
| Patt { [$1] } | Patt { [$1] }
| Patt ',' ListPattTupleComp { $1 : $3 } | Patt ',' ListPattTupleComp { $1 : $3 }
Opt :: { Option }
Opt
: '(' Exp ')' '=>' Exp { ($2,$5) }
ListOpt :: { [Option] }
ListOpt
: Opt { [$1] }
| Opt ';' ListOpt { $1 : $3 }
Case :: { Case } Case :: { Case }
Case Case
: Patt '=>' Exp { ($1,$3) } : Patt '=>' Exp { ($1,$3) }