mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-09-12 05:16:01 -06:00
fix partial evaluations and frozen applications
This commit is contained in:
@@ -5,12 +5,11 @@ module GF.Compile.Compute
|
|||||||
ConstValue(..), Globals(..), PredefTable, EvalM,
|
ConstValue(..), Globals(..), PredefTable, EvalM,
|
||||||
mapVariantsC, unvariants,
|
mapVariantsC, unvariants,
|
||||||
runEvalM, runEvalMWithInput, stdPredef, noPredef, globals,
|
runEvalM, runEvalMWithInput, stdPredef, noPredef, globals,
|
||||||
PredefImpl, Predef(..), ($\),
|
PredefImpl, Predef, pdArity,
|
||||||
pdCanonicalArgs, pdArity,
|
|
||||||
normalForm, normalFlatForm,
|
normalForm, normalFlatForm,
|
||||||
eval, apply, value2term, value2termM, value2string, value2int, value2float, value2expr, string2value, bubble, patternMatch, vtableSelect, State(..),
|
eval, apply, value2term, value2termM, value2string, value2int, value2float, value2expr, string2value, bubble, patternMatch, vtableSelect, State(..),
|
||||||
newResiduation, checkpoint, getMeta, setMeta, MetaState(..), variants, try,
|
newResiduation, checkpoint, getMeta, setMeta, MetaState(..), variants, try,
|
||||||
evalError, evalWarn, ppValue, Choice(..), unit, poison, split, split3, split4, mapC, mapCM) where
|
evalError, evalWarn, ppValue, Choice(..), unit, 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
|
||||||
@@ -37,23 +36,10 @@ import Data.Char
|
|||||||
import PGF2(Expr(..),Literal(..))
|
import PGF2(Expr(..),Literal(..))
|
||||||
|
|
||||||
type PredefImpl = Globals -> Choice -> [Value] -> ConstValue Value
|
type PredefImpl = Globals -> Choice -> [Value] -> ConstValue Value
|
||||||
newtype Predef = Predef { runPredef :: PredefImpl }
|
data Predef = Predef { predefArity :: Int, predefRun :: PredefImpl }
|
||||||
|
|
||||||
infix 1 $\
|
pdArity :: Int -> PredefImpl -> Predef
|
||||||
|
pdArity n def = Predef n def
|
||||||
($\) :: (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)]
|
||||||
@@ -61,7 +47,9 @@ type PredefTable = Map.Map Ident Predef
|
|||||||
data Globals = Gl Grammar PredefTable Bool {- True for abstract, False for concrete -}
|
data Globals = Gl Grammar PredefTable Bool {- True for abstract, False for concrete -}
|
||||||
|
|
||||||
data Value
|
data Value
|
||||||
= VApp Choice QIdent [Value]
|
= VApp QIdent [Value] -- application of a constructor
|
||||||
|
| VPAP Choice QIdent [Value] -- partially applied function
|
||||||
|
| VConst QIdent [Value] -- function application that cannot be evaluated
|
||||||
| 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]
|
||||||
@@ -245,18 +233,13 @@ 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 = evalPredef g c id vs
|
| m == cPredef = evalPredef g c id vs
|
||||||
| isAbstract = let v0 = VApp c q vs
|
| isAbstract = evalAbsDef g c q vs
|
||||||
in case lookupAbsDef gr q of
|
|
||||||
Ok (Just arity,Just eqs)
|
|
||||||
| length vs < arity -> v0
|
|
||||||
| otherwise -> patternMatch g c v0 (map (\(ps,t) -> (env,ps,vs,t)) eqs)
|
|
||||||
Bad msg -> error msg
|
|
||||||
| otherwise = case lookupResDef gr q of
|
| otherwise = case lookupResDef gr q of
|
||||||
Ok t -> eval g env c t vs
|
Ok t -> eval g [] c t vs
|
||||||
Bad msg -> error msg
|
Bad msg -> error msg
|
||||||
where
|
where
|
||||||
Gl gr predef isAbstract = g
|
Gl gr predef isAbstract = g
|
||||||
eval g env s (QC q) vs = VApp s q vs
|
eval g env c (QC q) vs = VApp 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
|
||||||
@@ -274,12 +257,12 @@ 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 c q []) v
|
glue (VApp q []) v
|
||||||
| q == (cPredef,cNonExist) = VApp c q []
|
| q == (cPredef,cNonExist) = VApp 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 c q [])
|
glue v (VApp q [])
|
||||||
| q == (cPredef,cNonExist) = VApp c q []
|
| q == (cPredef,cNonExist) = VApp 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
|
||||||
@@ -333,45 +316,60 @@ eval g env c t vs = VError ("Cannot reduce term" <+> pp t)
|
|||||||
evalPredef :: Globals -> Choice -> Ident -> [Value] -> Value
|
evalPredef :: Globals -> Choice -> Ident -> [Value] -> Value
|
||||||
evalPredef g@(Gl gr pds _) c n args =
|
evalPredef g@(Gl gr pds _) c n args =
|
||||||
case Map.lookup n pds of
|
case Map.lookup n pds of
|
||||||
Nothing -> VApp c (cPredef,n) args
|
Nothing -> VApp (cPredef,n) args
|
||||||
Just def -> let valueOf (Const res) = res
|
Just (Predef k def) -> case splitAt' k args of
|
||||||
valueOf (CFV i vs) = VFV i (fmap valueOf vs)
|
Nothing -> VPAP c (cPredef,n) args
|
||||||
valueOf (CSusp i k) = VSusp i (valueOf . k) []
|
Just (usedArgs, remArgs) ->
|
||||||
valueOf RunTime = VApp c (cPredef,n) args
|
apply g (valueOf (def g c usedArgs)) remArgs
|
||||||
valueOf NonExist = VApp c (cPredef,cNonExist) []
|
where
|
||||||
in valueOf (runPredef def g c args)
|
valueOf (Const res) = res
|
||||||
|
valueOf (CFV i vs) = VFV i (fmap valueOf vs)
|
||||||
|
valueOf (CSusp i k) = VSusp i (valueOf . k) []
|
||||||
|
valueOf RunTime = VConst (cPredef,n) args
|
||||||
|
valueOf NonExist = VApp (cPredef,cNonExist) []
|
||||||
|
|
||||||
noPredef :: PredefTable
|
noPredef :: PredefTable
|
||||||
noPredef = Map.empty
|
noPredef = Map.empty
|
||||||
|
|
||||||
stdPredef :: Globals -> PredefTable
|
stdPredef :: Globals -> PredefTable
|
||||||
stdPredef g = Map.fromList
|
stdPredef g = Map.fromList
|
||||||
[(cInts, pdArity 1 $\ \g c vs -> Const (case vs of {[VInt i] -> VInts i False; vs -> VApp c (cPredef,cInts) vs}))
|
[(cInts, pdArity 1 $ \g c vs -> Const (case vs of {[VInt i] -> VInts i False; vs -> VApp (cPredef,cInts) vs}))
|
||||||
,(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
|
||||||
genericDp n = reverse . genericTake n . reverse
|
genericDp n = reverse . genericTake n . reverse
|
||||||
|
|
||||||
|
evalAbsDef :: Globals -> Choice -> QIdent -> [Value] -> Value
|
||||||
|
evalAbsDef g@(Gl gr pds _) c q args =
|
||||||
|
case lookupAbsDef gr q of
|
||||||
|
Ok (Just arity,Just eqs) ->
|
||||||
|
case splitAt' arity args of
|
||||||
|
Nothing -> VPAP c q args
|
||||||
|
Just (_,_) -> patternMatch g c (VConst q args) (map (\(ps,t) -> ([],ps,args,t)) eqs)
|
||||||
|
Bad msg -> error msg
|
||||||
|
|
||||||
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 c f@(m,n) vs0) vs
|
apply g (VApp f vs0) vs = VApp f (vs0++vs)
|
||||||
|
apply g (VPAP c q@(m,n) vs0) vs
|
||||||
| m == cPredef = evalPredef g c n (vs0++vs)
|
| m == cPredef = evalPredef g c n (vs0++vs)
|
||||||
| otherwise = VApp c f (vs0++vs)
|
| otherwise = evalAbsDef g c q (vs0++vs)
|
||||||
|
apply g (VConst f vs0) vs = VConst 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 (fmap (\v -> apply g v vs) fvs)
|
apply g (VFV i fvs) vs = VFV i (fmap (\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)
|
||||||
@@ -384,7 +382,9 @@ data BubbleVariants
|
|||||||
|
|
||||||
bubble v = snd (bubble v)
|
bubble v = snd (bubble v)
|
||||||
where
|
where
|
||||||
bubble (VApp c f vs) = liftL (VApp c f) vs
|
bubble (VApp f vs) = liftL (VApp f) vs
|
||||||
|
bubble (VPAP c f vs) = liftL (VPAP c f) vs
|
||||||
|
bubble (VConst f vs) = liftL (VConst 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
|
||||||
@@ -512,8 +512,8 @@ bubble v = snd (bubble v)
|
|||||||
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 poison (cPredef,cPTrue) []
|
toPBool True = VApp (cPredef,cPTrue) []
|
||||||
toPBool False = VApp poison (cPredef,cPFalse) []
|
toPBool False = VApp (cPredef,cPFalse) []
|
||||||
|
|
||||||
occur s1 [] = False
|
occur s1 [] = False
|
||||||
occur s1 s2@(_:tail) = check s1 s2
|
occur s1 s2@(_:tail) = check s1 s2
|
||||||
@@ -558,11 +558,12 @@ patternMatch g s v0 ((env0,ps,args0,t):eqs) = match env0 ps eqs args0
|
|||||||
|
|
||||||
match' env p ps eqs arg args =
|
match' env p ps eqs arg args =
|
||||||
case (p,arg) of
|
case (p,arg) of
|
||||||
|
(p, VConst q vs) -> v0
|
||||||
(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 (fmap (\arg -> match' env p ps eqs arg args) vs)
|
(p, VFV s vs) -> VFV s (fmap (\arg -> match' env p ps eqs arg args) vs)
|
||||||
(PP q qs, VApp c r vs)
|
(PP q qs, VApp 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)
|
||||||
@@ -638,7 +639,7 @@ 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 c q args) vty =
|
value2index (VApp q args) vty =
|
||||||
let (r ,ctxt,cnt ) = getIdxCnt q
|
let (r ,ctxt,cnt ) = getIdxCnt q
|
||||||
in fmap (\(r', cnt') -> (r+r',cnt)) (compute ctxt args)
|
in fmap (\(r', cnt') -> (r+r',cnt)) (compute ctxt args)
|
||||||
where
|
where
|
||||||
@@ -661,7 +662,7 @@ vtableSelect g v0 ty cs v2 vs =
|
|||||||
Bad msg -> error msg
|
Bad msg -> error msg
|
||||||
|
|
||||||
Gl gr _ _ = g
|
Gl gr _ _ = g
|
||||||
value2index (VInt n) (VApp _ c [VInt max])
|
value2index (VInt n) (VApp c [VInt max])
|
||||||
| Q c == cnPredef cInts = Const (fromIntegral n,fromIntegral max+1)
|
| Q c == cnPredef cInts = Const (fromIntegral n,fromIntegral max+1)
|
||||||
value2index (VFV c vs) vty = CFV c (fmap (\v -> value2index v vty) vs)
|
value2index (VFV c vs) vty = CFV c (fmap (\v -> value2index v vty) vs)
|
||||||
value2index v vty = RunTime
|
value2index v vty = RunTime
|
||||||
@@ -823,8 +824,12 @@ setMeta i ms = EvalM (\g k (State input choices metas opts) r msgs ->
|
|||||||
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 c q vs) =
|
value2termM flat xs (VApp 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)) (QC q) vs
|
||||||
|
value2termM flat xs (VPAP _ q vs) =
|
||||||
|
foldM (\t v -> fmap (App t) (value2termM flat xs v)) (Q q) vs
|
||||||
|
value2termM flat xs (VConst q vs) =
|
||||||
|
foldM (\t v -> fmap (App t) (value2termM flat xs v)) (Q q) vs
|
||||||
value2termM flat xs (VMeta i vs) = do
|
value2termM flat xs (VMeta i vs) = do
|
||||||
mv <- getMeta i
|
mv <- getMeta i
|
||||||
case mv of
|
case mv of
|
||||||
@@ -1068,8 +1073,21 @@ pattVars st _ = st
|
|||||||
|
|
||||||
|
|
||||||
|
|
||||||
ppValue q d (VApp c f vs) = prec d 4 (hsep (ppQIdent q f : map (ppValue q 5) vs))
|
ppValue q d (VApp f 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))
|
| null vs = ppQIdent q f
|
||||||
|
| otherwise = prec d 4 (hsep (ppQIdent q f : map (ppValue q 5) vs))
|
||||||
|
ppValue q d (VPAP _ f vs)
|
||||||
|
| null vs = ppQIdent q f
|
||||||
|
| otherwise = prec d 4 (hsep (ppQIdent q f : map (ppValue q 5) vs))
|
||||||
|
ppValue q d (VConst f vs)
|
||||||
|
| null vs = ppQIdent q f
|
||||||
|
| otherwise = prec d 4 (hsep (ppQIdent q f : map (ppValue q 5) vs))
|
||||||
|
ppValue q d (VMeta i vs)
|
||||||
|
| null vs = meta
|
||||||
|
| otherwise = prec d 4 (hsep (meta : map (ppValue q 5) vs))
|
||||||
|
where
|
||||||
|
meta | i > 0 = pp "?" <> pp i
|
||||||
|
| otherwise = 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 (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 i vs) = prec d 4 (hsep (pp "#gen" : pp i : map (ppValue q 5) vs))
|
ppValue q d (VGen i vs) = prec d 4 (hsep (pp "#gen" : pp i : map (ppValue q 5) vs))
|
||||||
ppValue q d (VClosure env c t) = pp "[|" <> ppTerm q 4 t <> pp "|]"
|
ppValue q d (VClosure env c t) = pp "[|" <> ppTerm q 4 t <> pp "|]"
|
||||||
@@ -1137,24 +1155,24 @@ value2string' g (VC v1 v2) b ws qs = concat v1 (value2string' g v2 b
|
|||||||
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 c vs) = CFV c (fmap (concat v1) vs)
|
concat v1 (CFV c vs) = CFV c (fmap (concat v1) vs)
|
||||||
concat v1 res = res
|
concat v1 res = res
|
||||||
value2string' g (VApp c q []) b ws qs
|
value2string' g (VApp q []) b ws qs
|
||||||
| q == (cPredef,cNonExist) = NonExist
|
| q == (cPredef,cNonExist) = NonExist
|
||||||
value2string' g (VApp c q []) b ws qs
|
value2string' g (VApp 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 c q []) b ws qs
|
value2string' g (VApp 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 c q []) b ws qs
|
value2string' g (VApp 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 c q []) b ws qs
|
value2string' g (VApp 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)
|
||||||
@@ -1195,7 +1213,7 @@ value2float g (VFlt f) = Const f
|
|||||||
value2float g (VFV s vs) = CFV s (fmap (value2float g) vs)
|
value2float g (VFV s vs) = CFV s (fmap (value2float g) vs)
|
||||||
value2float g _ = RunTime
|
value2float g _ = RunTime
|
||||||
|
|
||||||
value2expr g xs (VApp _ (m,f) vs)
|
value2expr g xs (VApp (m,f) vs)
|
||||||
| m /= cPredef = foldl (\e v -> fmap EApp e <*> value2expr g xs v) (pure (EFun (showIdent f))) vs
|
| m /= cPredef = foldl (\e v -> fmap EApp e <*> value2expr g xs v) (pure (EFun (showIdent f))) vs
|
||||||
value2expr g xs (VMeta i vs) = CSusp i (\v -> value2expr g xs (apply g v vs))
|
value2expr g xs (VMeta i vs) = CSusp i (\v -> value2expr g xs (apply g v vs))
|
||||||
value2expr g xs (VSusp i k vs) = CSusp i (\v -> value2expr g xs (apply g (k v) vs))
|
value2expr g xs (VSusp i k vs) = CSusp i (\v -> value2expr g xs (apply g (k v) vs))
|
||||||
@@ -1215,9 +1233,6 @@ newtype Choice = Choice { unchoice :: Integer }
|
|||||||
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))
|
||||||
|
|
||||||
|
|||||||
@@ -255,9 +255,9 @@ force (VSymCat d r rs) = do
|
|||||||
force_ (factor, (v, ty)) = do
|
force_ (factor, (v, ty)) = do
|
||||||
v <- force v
|
v <- force v
|
||||||
return (factor, (v, ty))
|
return (factor, (v, ty))
|
||||||
force (VApp c q vs) = do
|
force (VApp q vs) = do
|
||||||
vs <- mapM force vs
|
vs <- mapM force vs
|
||||||
return (VApp c q vs)
|
return (VApp q vs)
|
||||||
force (VAlts def alts) = do
|
force (VAlts def alts) = do
|
||||||
def <- force def
|
def <- force def
|
||||||
alts <- mapM force_ alts
|
alts <- mapM force_ alts
|
||||||
@@ -302,7 +302,7 @@ flatten subst (VStr s) = return (subst,[SymKS s])
|
|||||||
flatten subst (VSymCat d r rs) = do
|
flatten subst (VSymCat d r rs) = do
|
||||||
(subst,lin_index) <- params2int' subst r rs
|
(subst,lin_index) <- params2int' subst r rs
|
||||||
return (subst,[SymCat d lin_index])
|
return (subst,[SymCat d lin_index])
|
||||||
flatten subst (VApp _ (m,id) [])
|
flatten subst (VApp (m,id) [])
|
||||||
| m == cPredef && id == cBIND = return (subst,[SymBIND])
|
| m == cPredef && id == cBIND = return (subst,[SymBIND])
|
||||||
| m == cPredef && id == cSOFT_BIND = return (subst,[SymSOFT_BIND])
|
| m == cPredef && id == cSOFT_BIND = return (subst,[SymSOFT_BIND])
|
||||||
| m == cPredef && id == cSOFT_SPACE = return (subst,[SymSOFT_SPACE])
|
| m == cPredef && id == cSOFT_SPACE = return (subst,[SymSOFT_SPACE])
|
||||||
@@ -383,7 +383,7 @@ param2int subst (VR as) (RecType lbls) = compute subst lbls
|
|||||||
return (subst,r*cnt'+r',combine' cnt rs cnt' rs',cnt*cnt')
|
return (subst,r*cnt'+r',combine' cnt rs cnt' rs',cnt*cnt')
|
||||||
Nothing -> compileError ("Missing value for label" <+> pp lbl $$
|
Nothing -> compileError ("Missing value for label" <+> pp lbl $$
|
||||||
"among" <+> hsep (punctuate (pp ',') (map fst as)))
|
"among" <+> hsep (punctuate (pp ',') (map fst as)))
|
||||||
param2int subst (VApp _ q vs) ty = do
|
param2int subst (VApp q vs) ty = do
|
||||||
( r , ctxt,cnt ) <- getIdxCnt q
|
( r , ctxt,cnt ) <- getIdxCnt q
|
||||||
(subst,r',rs', cnt') <- compute subst ctxt vs
|
(subst,r',rs', cnt') <- compute subst ctxt vs
|
||||||
return (subst,r+r',rs',cnt)
|
return (subst,r+r',rs',cnt)
|
||||||
@@ -509,7 +509,7 @@ chooseMetaValue s ptyp = GenM $ \g@(Gl gr _ _) k svs ms r ->
|
|||||||
mkValue mod k svs ms r idx [] = return r
|
mkValue mod k svs ms r idx [] = return r
|
||||||
mkValue mod k svs ms r idx ((id,ctxt):ps) = do
|
mkValue mod k svs ms r idx ((id,ctxt):ps) = do
|
||||||
let (ms',args) = mkVars ms s ctxt
|
let (ms',args) = mkVars ms s ctxt
|
||||||
r <- k (VApp poison (mod,id) args) (Map.insert s idx svs) ms' r
|
r <- k (VApp (mod,id) args) (Map.insert s idx svs) ms' r
|
||||||
mkValue mod k svs ms r (idx+1) ps
|
mkValue mod k svs ms r (idx+1) ps
|
||||||
|
|
||||||
mkVars ms c [] = (ms,[])
|
mkVars ms c [] = (ms,[])
|
||||||
|
|||||||
@@ -108,13 +108,13 @@ 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 poison (cPredef,cInt) []
|
vtypeInt = VApp (cPredef,cInt) []
|
||||||
vtypeFloat = VApp poison (cPredef,cFloat) []
|
vtypeFloat = VApp (cPredef,cFloat) []
|
||||||
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 poison (cPredef,cMarkup) []
|
vtypeMarkup= VApp (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 (VInts i True) mb_ty -- INT
|
tcRho scope s t@(EInt i) mb_ty = instSigma scope s t (VInts i True) mb_ty -- INT
|
||||||
@@ -140,7 +140,9 @@ 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 c f vs) = foldM (check m n) st vs
|
check m n st (VApp f vs) = foldM (check m n) st vs
|
||||||
|
check m n st (VPAP c f vs) = foldM (check m n) st vs
|
||||||
|
check m n st (VConst 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
|
||||||
@@ -535,7 +537,7 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty
|
|||||||
Nothing -> do i <- newResiduation scope
|
Nothing -> do i <- newResiduation scope
|
||||||
return (VMeta i [])
|
return (VMeta i [])
|
||||||
let rec_ty = VRecType [ (ident2label cp1, True, ty)
|
let rec_ty = VRecType [ (ident2label cp1, True, ty)
|
||||||
, (ident2label cp2, True, VApp poison (cPredef,cBool) [])
|
, (ident2label cp2, True, VApp (cPredef,cBool) [])
|
||||||
] False
|
] False
|
||||||
case mb_ct of
|
case mb_ct of
|
||||||
Just ct -> evalError (pp "[filter | ..] cannot take an argument")
|
Just ct -> evalError (pp "[filter | ..] cannot take an argument")
|
||||||
@@ -558,8 +560,8 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty
|
|||||||
Nothing -> evalError (pp "[list: .. | ..] requires an argument")
|
Nothing -> evalError (pp "[list: .. | ..] requires an argument")
|
||||||
(t,ty) <- tcRho scope c2 t mb_ty
|
(t,ty) <- tcRho scope c2 t mb_ty
|
||||||
case ty of
|
case ty of
|
||||||
VApp c qid [] -> return (Reset ctl mb_ct t (Just qid), ty)
|
VApp qid [] -> return (Reset ctl mb_ct t (Just qid), ty)
|
||||||
_ -> evalError (pp "Needs atomic type"<+>ppValue Unqualified 0 ty)
|
_ -> evalError (pp "Needs atomic type"<+>ppValue Unqualified 0 ty)
|
||||||
| ctl == cLen = concreteOnly "Control operators" $ do
|
| ctl == cLen = concreteOnly "Control operators" $ do
|
||||||
do let (c1,c2) = split c
|
do let (c1,c2) = split c
|
||||||
(t,_) <- tcRho scope c1 t Nothing
|
(t,_) <- tcRho scope c1 t Nothing
|
||||||
@@ -676,11 +678,11 @@ resolveOverloads scope c t0 q args mb_ty = do
|
|||||||
g@(Gl gr _ isAbstract) <- globals
|
g@(Gl gr _ isAbstract) <- globals
|
||||||
if isAbstract
|
if isAbstract
|
||||||
then case lookupAbsType gr q of
|
then case lookupAbsType gr q of
|
||||||
Bad msg -> evalError (pp msg)
|
Bad msg -> evalError (pp msg)
|
||||||
Ok ty -> do let (c1,c23) = split c
|
Ok (t,ty) -> do let (c1,c23) = split c
|
||||||
(c2,c3) = split c23
|
(c2,c3) = split c23
|
||||||
(t,ty) <- reapply1 scope c1 t0 (eval g [] c2 ty []) args
|
(t,ty) <- reapply1 scope c1 t (eval g [] c2 ty []) args
|
||||||
instSigma scope c3 t ty mb_ty
|
instSigma scope c3 t ty mb_ty
|
||||||
else case lookupOverloadTypes gr q of
|
else case lookupOverloadTypes gr q of
|
||||||
Bad msg -> evalError (pp msg)
|
Bad msg -> evalError (pp msg)
|
||||||
Ok [(t,ty)] -> do let (c1,c23) = split c
|
Ok [(t,ty)] -> do let (c1,c23) = split c
|
||||||
@@ -1034,9 +1036,9 @@ instSigma scope s t ty1 (Just ty2) = do -- INST2
|
|||||||
|
|
||||||
-- | Invariant: the second argument is in weak-prenex form
|
-- | Invariant: the second argument is in weak-prenex form
|
||||||
subsCheckRho :: Scope -> Term -> Sigma -> Rho -> EvalM (Term,Sigma,Rho)
|
subsCheckRho :: Scope -> Term -> Sigma -> Rho -> EvalM (Term,Sigma,Rho)
|
||||||
subsCheckRho scope t ty1@(VApp _ p1 []) ty2 -- for backwards compatibility
|
subsCheckRho scope t ty1@(VApp p1 []) ty2 -- for backwards compatibility
|
||||||
| p1 == (cPredef,cErrorType) = return (t,ty1,ty2)
|
| p1 == (cPredef,cErrorType) = return (t,ty1,ty2)
|
||||||
subsCheckRho scope t ty1 ty2@(VApp _ p2 []) -- for backwards compatibility
|
subsCheckRho scope t ty1 ty2@(VApp p2 []) -- for backwards compatibility
|
||||||
| p2 == (cPredef,cErrorType) = return (t,ty1,ty2)
|
| p2 == (cPredef,cErrorType) = return (t,ty1,ty2)
|
||||||
subsCheckRho scope t ty1@(VMeta i vs1) ty2@(VMeta j vs2)
|
subsCheckRho scope t ty1@(VMeta i vs1) ty2@(VMeta j vs2)
|
||||||
| i == j = do sequence_ (zipWith (unify scope) vs1 vs2)
|
| i == j = do sequence_ (zipWith (unify scope) vs1 vs2)
|
||||||
@@ -1113,9 +1115,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 ty1@(VSort s1) ty2@(VSort s2) -- Rule PTYPE
|
subsCheckRho scope t ty1@(VSort s1) ty2@(VSort s2) -- Rule PTYPE
|
||||||
| s1 == cPType && s2 == cType = return (t,ty1,ty2)
|
| s1 == cPType && s2 == cType = return (t,ty1,ty2)
|
||||||
subsCheckRho scope t ty1@(VApp _ p _) ty2@(VInts _ _) -- This is not correct but nextPrec in the RGL relies on it.
|
subsCheckRho scope t ty1@(VApp p _) ty2@(VInts _ _) -- This is not correct but nextPrec in the RGL relies on it.
|
||||||
| p == (cPredef,cInt) = return (t,ty1,ty2) -- Should be only a temporary hack.
|
| p == (cPredef,cInt) = return (t,ty1,ty2) -- Should be only a temporary hack.
|
||||||
subsCheckRho scope t ty1@(VInts _ _) ty2@(VApp _ p _) -- Rule INT1
|
subsCheckRho scope t ty1@(VInts _ _) ty2@(VApp p _) -- Rule INT1
|
||||||
| p == (cPredef,cInt) = return (t,ty1,ty2)
|
| p == (cPredef,cInt) = return (t,ty1,ty2)
|
||||||
subsCheckRho scope t ty1@(VInts n1 ext1) ty2@(VInts n2 ext2) -- Rule INT2
|
subsCheckRho scope t ty1@(VInts n1 ext1) ty2@(VInts n2 ext2) -- Rule INT2
|
||||||
| n1 <= n2 = return (t,ty1,ty2)
|
| n1 <= n2 = return (t,ty1,ty2)
|
||||||
@@ -1277,9 +1279,9 @@ subtype scope (Just (VProd Explicit x a1 r1)) (VProd Explicit y a2 r2)
|
|||||||
a <- supertype scope (Just a1) a2
|
a <- supertype scope (Just a1) a2
|
||||||
r <- subtype scope (Just r1) r2
|
r <- subtype scope (Just r1) r2
|
||||||
return (VProd Explicit identW a r)
|
return (VProd Explicit identW a r)
|
||||||
subtype scope (Just (VApp _ p1 [])) ty2 -- for backwards compatibility
|
subtype scope (Just (VApp p1 [])) ty2 -- for backwards compatibility
|
||||||
| p1 == (cPredef,cErrorType) = return ty2
|
| p1 == (cPredef,cErrorType) = return ty2
|
||||||
subtype scope (Just ty1) (VApp _ p2 []) -- for backwards compatibility
|
subtype scope (Just ty1) (VApp p2 []) -- for backwards compatibility
|
||||||
| p2 == (cPredef,cErrorType) = return ty1
|
| p2 == (cPredef,cErrorType) = return ty1
|
||||||
subtype scope Nothing ty = return ty
|
subtype scope Nothing ty = return ty
|
||||||
subtype scope (Just ctr) ty = do
|
subtype scope (Just ctr) ty = do
|
||||||
@@ -1311,9 +1313,9 @@ supertype scope (Just (VProd Explicit x a1 r1)) (VProd Explicit y a2 r2)
|
|||||||
a <- subtype scope (Just a1) a2
|
a <- subtype scope (Just a1) a2
|
||||||
r <- supertype scope (Just r1) r2
|
r <- supertype scope (Just r1) r2
|
||||||
return (VProd Explicit identW a r)
|
return (VProd Explicit identW a r)
|
||||||
supertype scope (Just (VApp _ p1 [])) ty2 -- for backwards compatibility
|
supertype scope (Just (VApp p1 [])) ty2 -- for backwards compatibility
|
||||||
| p1 == (cPredef,cErrorType) = return ty2
|
| p1 == (cPredef,cErrorType) = return ty2
|
||||||
supertype scope (Just ty1) (VApp _ p2 []) -- for backwards compatibility
|
supertype scope (Just ty1) (VApp p2 []) -- for backwards compatibility
|
||||||
| p2 == (cPredef,cErrorType) = return ty1
|
| p2 == (cPredef,cErrorType) = return ty1
|
||||||
supertype scope Nothing ty = return ty
|
supertype scope Nothing ty = return ty
|
||||||
supertype scope (Just ctr) ty = do
|
supertype scope (Just ctr) ty = do
|
||||||
@@ -1353,7 +1355,11 @@ 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 c1 f1 vs1) (VApp c2 f2 vs2)
|
unify scope (VApp f1 vs1) (VApp f2 vs2)
|
||||||
|
| f1 == f2 = sequence_ (zipWith (unify scope) vs1 vs2)
|
||||||
|
unify scope (VPAP c1 f1 vs1) (VPAP c2 f2 vs2)
|
||||||
|
| f1 == f2 = sequence_ (zipWith (unify scope) vs1 vs2)
|
||||||
|
unify scope (VConst f1 vs1) (VConst 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)
|
||||||
@@ -1417,7 +1423,9 @@ 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 c f vs) = mapM_ (check m n) vs
|
check m n (VApp f vs) = mapM_ (check m n) vs
|
||||||
|
check m n (VPAP c f vs) = mapM_ (check m n) vs
|
||||||
|
check m n (VConst 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
|
||||||
@@ -1526,9 +1534,15 @@ 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 c f vs) = do
|
check m n xs (VApp f vs) = do
|
||||||
(xs,vs) <- mapAccumM (check m n) xs vs
|
(xs,vs) <- mapAccumM (check m n) xs vs
|
||||||
return (xs,VApp c f vs)
|
return (xs,VApp f vs)
|
||||||
|
check m n xs (VPAP c f vs) = do
|
||||||
|
(xs,vs) <- mapAccumM (check m n) xs vs
|
||||||
|
return (xs,VPAP c f vs)
|
||||||
|
check m n xs (VConst f vs) = do
|
||||||
|
(xs,vs) <- mapAccumM (check m n) xs vs
|
||||||
|
return (xs,VConst 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
|
||||||
@@ -1678,7 +1692,9 @@ getMetaVars sc_tys = foldM (\acc (scope,ty) -> go acc ty) [] sc_tys
|
|||||||
case res of
|
case res of
|
||||||
Bound _ v -> go acc v
|
Bound _ v -> go acc v
|
||||||
_ -> foldM go (m:acc) args
|
_ -> foldM go (m:acc) args
|
||||||
go acc (VApp c f args) = foldM go acc args
|
go acc (VApp f args) = foldM go acc args
|
||||||
|
go acc (VPAP c f args) = foldM go acc args
|
||||||
|
go acc (VConst f args) = foldM go acc args
|
||||||
go acc (VFV c vs) = foldM go acc (unvariants vs)
|
go acc (VFV c vs) = foldM go acc (unvariants vs)
|
||||||
go acc (VInts _ _) = return acc
|
go acc (VInts _ _) = return acc
|
||||||
go acc (VPattType v) = go acc v
|
go acc (VPattType v) = go acc v
|
||||||
|
|||||||
@@ -244,19 +244,20 @@ lookupLincat gr m c = do
|
|||||||
_ -> raise (render (c <+> "has no linearization type in" <+> m))
|
_ -> raise (render (c <+> "has no linearization type in" <+> m))
|
||||||
|
|
||||||
-- | this is needed at compile time
|
-- | this is needed at compile time
|
||||||
lookupAbsType :: ErrorMonad m => Grammar -> QIdent -> m Type
|
lookupAbsType :: ErrorMonad m => Grammar -> QIdent -> m (Term,Type)
|
||||||
lookupAbsType gr q@(m,c)
|
lookupAbsType gr q@(m,c)
|
||||||
| m == cPredefAbs =
|
| m == cPredefAbs =
|
||||||
if elem c [cInt,cFloat,cString]
|
if elem c [cInt,cFloat,cString]
|
||||||
then return typeType
|
then return (QC q,typeType)
|
||||||
else no_type
|
else no_type
|
||||||
| otherwise = do
|
| otherwise = do
|
||||||
info <- lookupQIdentInfo gr q
|
info <- lookupQIdentInfo gr q
|
||||||
case info of
|
case info of
|
||||||
AbsCat (Just (L _ co)) -> return (mkProd co typeType [])
|
AbsCat (Just (L _ co)) -> return (QC q,mkProd co typeType [])
|
||||||
AbsFun (Just (L _ t)) _ _ _ -> return t
|
AbsFun (Just (L _ t)) _ Nothing _ -> return (QC q,t)
|
||||||
AnyInd _ n -> lookupAbsType gr (n,c)
|
AbsFun (Just (L _ t)) _ (Just _) _ -> return (Q q,t)
|
||||||
_ -> no_type
|
AnyInd _ n -> lookupAbsType gr (n,c)
|
||||||
|
_ -> no_type
|
||||||
where
|
where
|
||||||
no_type = raise (render ("cannot find type of" <+> c))
|
no_type = raise (render ("cannot find type of" <+> c))
|
||||||
|
|
||||||
|
|||||||
Reference in New Issue
Block a user