diff --git a/src/compiler/api/GF/Command/SourceCommands.hs b/src/compiler/api/GF/Command/SourceCommands.hs index f7f98308d..33badb3ea 100644 --- a/src/compiler/api/GF/Command/SourceCommands.hs +++ b/src/compiler/api/GF/Command/SourceCommands.hs @@ -20,7 +20,7 @@ import GF.Grammar.ShowTerm import GF.Grammar.Lookup (allOpers,allOpersTo) import GF.Compile.Rename(renameSourceTerm) import GF.Compile.Compute.Concrete2(normalForm,normalFlatForm,Globals(..),stdPredef) -import GF.Compile.TypeCheck.ConcreteNew as TC(inferLType) +import GF.Compile.TypeCheck.Concrete as TC(inferLType) import GF.Command.Abstract(Option(..),isOpt,listFlags,valueString,valStrOpts) import GF.Command.CommandInfo @@ -245,10 +245,10 @@ checkComputeTerm os sgr t = Nothing -> checkError (pp "No source grammar in scope") Just mo -> return mo t <- renameSourceTerm sgr mo t - ttys <- inferLType g t + (t,_) <- inferLType g t if isOpt "flat" os - then fmap concat (mapM (\(t,_) -> fmap (map evalStr) (normalFlatForm g t)) ttys) - else fmap concat (mapM (\(t,_) -> fmap (singleton . evalStr) (normalForm g t)) ttys) + then fmap (map evalStr) (normalFlatForm g t) + else fmap (singleton . evalStr) (normalForm g t) where -- ** Try to compute pre{...} tokens in token sequences singleton x = [x] diff --git a/src/compiler/api/GF/Compile/CheckGrammar.hs b/src/compiler/api/GF/Compile/CheckGrammar.hs index 14fa23f47..5f0deb696 100644 --- a/src/compiler/api/GF/Compile/CheckGrammar.hs +++ b/src/compiler/api/GF/Compile/CheckGrammar.hs @@ -27,9 +27,8 @@ import GF.Infra.Ident import GF.Infra.Option import GF.Compile.TypeCheck.Abstract -import GF.Compile.TypeCheck.Concrete(checkLType,inferLType,ppType) -import qualified GF.Compile.TypeCheck.ConcreteNew as CN(checkLType,inferLType) -import GF.Compile.Compute.Concrete(normalForm,Globals(..),stdPredef) +import GF.Compile.TypeCheck.Concrete(checkLType,inferLType) +import GF.Compile.Compute.Concrete2(normalForm,Globals(..),stdPredef) import GF.Grammar import GF.Grammar.Lexer @@ -173,26 +172,26 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do CncCat mty mdef mref mpr mpmcfg -> do mty <- case mty of Just (L loc typ) -> chIn loc "linearization type of" $ do - (typ,_) <- checkLType gr [] typ typeType - typ <- normalForm (Gl gr stdPredef) typ + (typ,_) <- checkLType g typ typeType + typ <- normalForm g typ return (Just (L loc typ)) Nothing -> return Nothing mdef <- case (mty,mdef) of (Just (L _ typ),Just (L loc def)) -> chIn loc "default linearization of" $ do - (def,_) <- checkLType gr [] def (mkFunType [typeStr] typ) + (def,_) <- checkLType g def (mkFunType [typeStr] typ) return (Just (L loc def)) _ -> return Nothing mref <- case (mty,mref) of (Just (L _ typ),Just (L loc ref)) -> chIn loc "reference linearization of" $ do - (ref,_) <- checkLType gr [] ref (mkFunType [typ] typeStr) + (ref,_) <- checkLType g ref (mkFunType [typ] typeStr) return (Just (L loc ref)) _ -> return Nothing mpr <- case mpr of (Just (L loc t)) -> chIn loc "print name of" $ do - (t,_) <- checkLType gr [] t typeStr + (t,_) <- checkLType g t typeStr return (Just (L loc t)) _ -> return Nothing update sm c (CncCat mty mdef mref mpr mpmcfg) @@ -201,13 +200,13 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do mt <- case (mty,mt) of (Just (_,cat,cont,val),Just (L loc trm)) -> chIn loc "linearization of" $ do - (trm,_) <- checkLType gr [] trm (mkFunType (map (\(_,_,ty) -> ty) cont) val) -- erases arg vars + (trm,_) <- checkLType g trm (mkFunType (map (\(_,_,ty) -> ty) cont) val) -- erases arg vars return (Just (L loc (etaExpand [] trm cont))) _ -> return mt mpr <- case mpr of (Just (L loc t)) -> chIn loc "print name of" $ do - (t,_) <- checkLType gr [] t typeStr + (t,_) <- checkLType g t typeStr return (Just (L loc t)) _ -> return Nothing update sm c (CncFun mty mt mpr mpmcfg) @@ -216,14 +215,14 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do (pty', pde') <- case (pty,pde) of (Just (L loct ty), Just (L locd de)) -> do ty' <- chIn loct "operation" $ do - (ty,_) <- checkLType gr [] ty typeType - normalForm (Gl gr stdPredef) ty + (ty,_) <- checkLType g ty typeType + normalForm g ty (de',_) <- chIn locd "operation" $ - checkLType gr [] de ty' + checkLType g de ty' return (Just (L loct ty'), Just (L locd de')) (Nothing , Just (L locd de)) -> do (de',ty') <- chIn locd "operation" $ - inferLType gr [] de + inferLType g de return (Just (L locd ty'), Just (L locd de')) (Just (L loct ty), Nothing) -> do chIn loct "operation" $ @@ -231,14 +230,14 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do update sm c (ResOper pty' pde') ResOverload os tysts -> chIn NoLoc "overloading" $ do - tysts' <- mapM (uncurry $ flip (\(L loc1 t) (L loc2 ty) -> checkLType gr [] t ty >>= \(t,ty) -> return (L loc1 t, L loc2 ty))) tysts -- return explicit ones + tysts' <- mapM (uncurry $ flip (\(L loc1 t) (L loc2 ty) -> checkLType g t ty >>= \(t,ty) -> return (L loc1 t, L loc2 ty))) tysts -- return explicit ones tysts0 <- lookupOverload gr (fst sm,c) -- check against inherited ones too - tysts1 <- mapM (uncurry $ flip (checkLType gr [])) - [(mkFunType args val,tr) | (args,(val,tr)) <- tysts0] + tysts1 <- sequence + [checkLType g tr (mkFunType args val) | (args,(val,tr)) <- tysts0] --- this can only be a partial guarantee, since matching --- with value type is only possible if expected type is given - checkUniq $ - sort [let (xs,t) = typeFormCnc x in t : map (\(b,x,t) -> t) xs | (_,x) <- tysts1] + --checkUniq $ + -- sort [let (xs,t) = typeFormCnc x in t : map (\(b,x,t) -> t) xs | (_,x) <- tysts1] update sm c (ResOverload os [(y,x) | (x,y) <- tysts']) ResParam (Just (L loc pcs)) _ -> do @@ -249,11 +248,12 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do _ -> return sm where gr = prependModule sgr sm + g = Gl gr (stdPredef g) chIn loc cat = checkInModule cwd (snd sm) loc ("Happened in" <+> cat <+> c) mkParamValues sm c cnt ts [] = return (sm,cnt,[],[]) mkParamValues sm@(mn,mi) c cnt ts ((p,co):pcs) = do - co <- mapM (\(b,v,ty) -> normalForm (Gl gr stdPredef) ty >>= \ty -> return (b,v,ty)) co + co <- mapM (\(b,v,ty) -> normalForm g ty >>= \ty -> return (b,v,ty)) co sm <- case lookupIdent p (jments mi) of Ok (ResValue (L loc _) _) -> update sm p (ResValue (L loc (mkProdSimple co (QC (mn,c)))) cnt) Bad msg -> checkError (pp msg) @@ -264,7 +264,7 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do checkUniq xss = case xss of x:y:xs | x == y -> checkError $ "ambiguous for type" <+> - ppType (mkFunType (tail x) (head x)) + ppTerm Terse 0 (mkFunType (tail x) (head x)) | otherwise -> checkUniq $ y:xs _ -> return () @@ -327,6 +327,7 @@ linTypeOfType cnc m (L loc typ) = do plusRecType vars val return ((Explicit,varX i,rec),cat) lookLin (_,c) = checks [ --- rather: update with defLinType ? - lookupLincat cnc m c >>= normalForm (Gl cnc stdPredef) + lookupLincat cnc m c >>= normalForm g ,return defLinType ] + g = Gl cnc (stdPredef g) diff --git a/src/compiler/api/GF/Compile/Compute/Concrete2.hs b/src/compiler/api/GF/Compile/Compute/Concrete2.hs index 394c4088d..8e80790e7 100644 --- a/src/compiler/api/GF/Compile/Compute/Concrete2.hs +++ b/src/compiler/api/GF/Compile/Compute/Concrete2.hs @@ -1,18 +1,16 @@ {-# LANGUAGE RankNTypes, BangPatterns, GeneralizedNewtypeDeriving, TupleSections #-} module GF.Compile.Compute.Concrete2 - (Env, Scope, Value(..), Variants(..), Constraint, OptionInfo(..), ChoiceMap, cleanOptions, - ConstValue(..), ConstVariants(..), Globals(..), PredefTable, EvalM, - mapVariants, mapVariantsC, unvariants, variants2consts, - mapConstVs, mapConstVsC, unconstVs, consts2variants, - runEvalM, runEvalMWithOpts, reset, reset1, stdPredef, globals, withState, + (Env, Scope, Value(..), Variants(..), OptionInfo(..), + ConstValue(..), Globals(..), PredefTable, EvalM, + mapVariantsC, unvariants, + runEvalM, runEvalMWithInput, stdPredef, globals, PredefImpl, Predef(..), ($\), pdCanonicalArgs, pdArity, normalForm, normalFlatForm, - eval, apply, value2term, value2termM, bubble, patternMatch, vtableSelect, State(..), - newResiduation, getMeta, setMeta, MetaState(..), variants, try, - evalError, evalWarn, ppValue, Choice(..), unit, poison, split, split3, split4, - mapC, forC, mapCM, forCM) where + eval, apply, value2term, value2termM, value2string, value2int, value2float, value2expr, string2value, bubble, patternMatch, vtableSelect, State(..), + newResiduation, checkpoint, getMeta, setMeta, MetaState(..), variants, try, + evalError, evalWarn, ppValue, Choice(..), unit, poison, split, split3, split4, mapC, mapCM) where import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint import GF.Infra.Ident @@ -26,6 +24,7 @@ import GF.Grammar.Predef import GF.Grammar.Printer hiding (ppValue) import GF.Grammar.Lockfield(lockLabel) import GF.Text.Pretty hiding (empty) +import qualified GF.Text.Pretty as PP import Control.Monad import Control.Applicative hiding (Const) import qualified Control.Applicative as A @@ -35,6 +34,7 @@ import Data.Functor ((<&>)) import Data.Maybe (fromMaybe,fromJust) import Data.List import Data.Char +import PGF2(Expr(..),Literal(..)) type PredefImpl = Globals -> Choice -> [Value] -> ConstValue Value newtype Predef = Predef { runPredef :: PredefImpl } @@ -67,7 +67,7 @@ data Value | VGen {-# UNPACK #-} !Int [Value] | VClosure Env Choice Term | VProd BindType Ident Value Value - | VRecType [(Label, Value)] + | VRecType [(Label, Bool, Value)] Bool | VR [(Label, Value)] | VP Value Label [Value] | VExtR Value Value @@ -84,40 +84,35 @@ data Value | VGlue Value Value | VPatt Int (Maybe Int) Patt | VPattType Value - | VFV Choice Variants + | VFV Choice (Variants Value) | VAlts Value [(Value, Value)] | VStrs [Value] | VMarkup Ident [(Ident,Value)] [Value] - | VReset Ident (Maybe Value) Value QIdent + | VReset Ident (Maybe Value) Value (Maybe QIdent) | VSymCat Int LIndex [(LIndex, (Value, Type))] | VError Doc - -- These two constructors are only used internally - -- in the type checker. - | VCRecType [(Label, Bool, Value)] - | VCInts (Maybe Integer) (Maybe Integer) + | VInts Integer Bool -third f (a,b,c) = (a, b, f c) +data Variants a + = VarFree [a] + | VarOpts Value [(Value, a)] -data Variants - = VarFree [Value] - | VarOpts Value Value [(Value, Value, Value)] +instance Functor Variants where + fmap f (VarFree vs) = VarFree (f <$> vs) + fmap f (VarOpts n cs) = VarOpts n (second f <$> cs) -mapVariants :: (Value -> Value) -> Variants -> Variants -mapVariants f (VarFree vs) = VarFree (f <$> vs) -mapVariants f (VarOpts nty n cs) = VarOpts nty n (third f <$> cs) +mapVariantsC :: (Choice -> a -> b) -> Choice -> Variants a -> Variants b +mapVariantsC f c (VarFree vs) = VarFree (mapC f c vs) +mapVariantsC f c (VarOpts n cs) = VarOpts n (mapC (\c (x,y) -> (x,f c y)) c cs) -mapVariantsC :: (Choice -> Value -> Value) -> Choice -> Variants -> Variants -mapVariantsC f c (VarFree vs) = VarFree (mapC f c vs) -mapVariantsC f c (VarOpts nty n cs) = VarOpts nty n (mapC (third . f) c cs) - -unvariants :: Variants -> [Value] -unvariants (VarFree vs) = vs -unvariants (VarOpts nty n cs) = cs <&> \(_,_,v) -> v +unvariants :: Variants a -> [a] +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 (VRecType fs _) = all (\(l,_,ty) -> isCanonicalForm flat ty) fs isCanonicalForm flat (VR {}) = True isCanonicalForm flat (VTable d cod) = isCanonicalForm flat d && isCanonicalForm flat cod isCanonicalForm flat (VT {}) = True @@ -138,29 +133,13 @@ isCanonicalForm flat _ = False data ConstValue a = Const a | CSusp MetaId (Value -> ConstValue a) - | CFV Choice (ConstVariants a) + | CFV Choice (Variants (ConstValue a)) | RunTime | NonExist -data ConstVariants a - = ConstFree [ConstValue a] - | ConstOpts Value Value [(Value, Value, ConstValue a)] - -mapConstVs :: (ConstValue a -> ConstValue b) -> ConstVariants a -> ConstVariants b -mapConstVs f (ConstFree vs) = ConstFree (f <$> vs) -mapConstVs f (ConstOpts nty n cs) = ConstOpts nty n (third f <$> cs) - -mapConstVsC :: (Choice -> ConstValue a -> ConstValue b) -> Choice -> ConstVariants a -> ConstVariants b -mapConstVsC f c (ConstFree vs) = ConstFree (mapC f c vs) -mapConstVsC f c (ConstOpts nty n cs) = ConstOpts nty n (mapC (third . f) c cs) - -unconstVs :: ConstVariants a -> [ConstValue a] -unconstVs (ConstFree vs) = vs -unconstVs (ConstOpts nty n cs) = cs <&> \(_,_,v) -> v - instance Functor ConstValue where fmap f (Const c) = Const (f c) - fmap f (CFV i vs) = CFV i (mapConstVs (fmap f) vs) + fmap f (CFV i vs) = CFV i (fmap (fmap f) vs) fmap f (CSusp i k) = CSusp i (fmap f . k) fmap f RunTime = RunTime fmap f NonExist = NonExist @@ -169,8 +148,8 @@ instance Applicative ConstValue where pure = Const (Const f) <*> (Const x) = Const (f x) - (CFV s vs) <*> v2 = CFV s (mapConstVs (<*> v2) vs) - v1 <*> (CFV s vs) = CFV s (mapConstVs (v1 <*>) vs) + (CFV s vs) <*> v2 = CFV s (fmap (<*> v2) vs) + v1 <*> (CFV s vs) = CFV s (fmap (v1 <*>) vs) (CSusp i k) <*> v2 = CSusp i (\v -> k v <*> v2) v1 <*> (CSusp i k) = CSusp i (\v -> v1 <*> k v) NonExist <*> _ = NonExist @@ -178,14 +157,6 @@ instance Applicative ConstValue where RunTime <*> _ = RunTime _ <*> RunTime = RunTime -variants2consts :: (Value -> ConstValue a) -> Variants -> ConstVariants a -variants2consts f (VarFree vs) = ConstFree (f <$> vs) -variants2consts f (VarOpts nty n os) = ConstOpts nty n (third f <$> os) - -consts2variants :: (ConstValue a -> Value) -> ConstVariants a -> Variants -consts2variants f (ConstFree vs) = VarFree (f <$> vs) -consts2variants f (ConstOpts nty n os) = VarOpts nty n (third f <$> os) - normalForm :: Globals -> Term -> Check Term normalForm g t = value2term g [] (bubble (eval g [] unit t [])) @@ -209,16 +180,19 @@ eval g env s (Abs b x t) [] = VClosure env s (Abs b x t) eval g env s (Abs b x t) (v:vs) = eval g ((x,v):env) s t vs eval g env s (Meta i) vs = VMeta i vs eval g env s (ImplArg t) [] = eval g env s t [] -eval g env s (Prod b x t1 t2)[] = let (s1,s2) = split s +eval g env s (Prod b x t1 t2)[] + | x == identW = let (s1,s2) = split s + in VProd b x (eval g env s1 t1 []) (eval g env s2 t2 []) + | otherwise = let (s1,s2) = split s in VProd b x (eval g env s1 t1 []) (VClosure env s2 t2) eval g env s (Typed t ty) vs = eval g env s t vs -eval g env s (RecType lbls) [] = VRecType (mapC (\s (lbl,ty) -> (lbl, eval g env s ty [])) s lbls) +eval g env s (RecType lbls) [] = VRecType (mapC (\s (lbl,ty) -> (lbl, True, eval g env s ty [])) s lbls) False eval g env s (R as) [] = VR (mapC (\s (lbl,(ty,t)) -> (lbl, eval g env s t [])) s as) eval g env s (P t lbl) vs = let project (VR as) = case lookup lbl as of Nothing -> VError ("Missing value for label" <+> pp lbl $$ "in" <+> pp (P t lbl)) Just v -> apply g v vs - project (VFV s fvs) = VFV s (mapVariants project fvs) + project (VFV s fvs) = VFV s (fmap project fvs) 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 v = VP v lbl vs @@ -226,9 +200,9 @@ eval g env s (P t lbl) vs = let project (VR as) = case lookup lbl a eval g env s (ExtR t1 t2) [] = let (s1,s2) = split s extend (VR as1) (VR as2) = VR (foldl (\as (lbl,v) -> update lbl v as) as1 as2) - extend (VRecType as1) (VRecType as2) = VRecType (foldl (\as (lbl,v) -> update lbl v as) as1 as2) - extend (VFV i fvs) v2 = VFV i (mapVariants (`extend` v2) fvs) - extend v1 (VFV i fvs) = VFV i (mapVariants (v1 `extend`) fvs) + extend (VRecType as1 e1) (VRecType as2 e2)=VRecType (foldl (\as (lbl,o,v) -> update3 lbl o v as) as1 as2) (e1 || e2) + extend (VFV i fvs) v2 = VFV i (fmap (`extend` v2) fvs) + extend v1 (VFV i fvs) = VFV i (fmap (v1 `extend`) fvs) 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 (VSusp i k vs) v2 = VSusp i (\v -> extend (apply g (k v) vs) v2) [] @@ -256,13 +230,13 @@ eval g env s (S t1 t2) vs = let (!s1,!s2) = split s Success tys ws -> case tys of [ty] -> vtableSelect g v0 ty tvs v2 vs tys -> vtableSelect g v0 (FV (reverse tys)) tvs v2 vs - select (VFV i fvs) = VFV i (mapVariants select fvs) + select (VFV i fvs) = VFV i (fmap select fvs) 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 v1 = v0 -- FIXME: options=[] is definitely not correct and this shouldn't be using value2termM at all - empty = State Map.empty Map.empty [] + empty = State [] Map.empty Map.empty [] in select v1 eval g env s (Let (x,(_,t1)) t2) vs = let (!s1,!s2) = split s @@ -279,8 +253,8 @@ eval g env s (C t1 t2) [] = let (!s1,!s2) = split s concat v1 VEmpty = v1 concat VEmpty v2 = v2 - concat (VFV i fvs) v2 = VFV i (mapVariants (`concat` v2) fvs) - concat v1 (VFV i fvs) = VFV i (mapVariants (v1 `concat`) fvs) + concat (VFV i fvs) v2 = VFV i (fmap (`concat` v2) fvs) + concat v1 (VFV i fvs) = VFV i (fmap (v1 `concat`) fvs) 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 (VSusp i k vs) v2 = VSusp i (\v -> concat (apply g (k v) vs) v2) [] @@ -302,8 +276,8 @@ eval g env s (Glue t1 t2) [] = let (!s1,!s2) = split s 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) v = glue d v - glue (VFV i fvs) v2 = VFV i (mapVariants (`glue` v2) fvs) - glue v1 (VFV i fvs) = VFV i (mapVariants (v1 `glue`) fvs) + glue (VFV i fvs) v2 = VFV i (fmap (`glue` v2) fvs) + glue v1 (VFV i fvs) = VFV i (fmap (v1 `glue`) fvs) 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 (VSusp i k vs) v2 = VSusp i (\v -> glue (apply g (k v) vs) v2) [] @@ -328,7 +302,7 @@ eval g env s (FV ts) vs = VFV s (VarFree (mapC (\s t -> eval g env s t v eval g env s (Alts d as) [] = let (!s1,!s2) = split s vd = eval g env s1 d [] vas = mapC (\s (t1,t2) -> let (!s1,!s2) = split s - in (eval g env s1 t1 [],eval g env s2 t2 [])) s2 as + in (eval g env s1 t1 [],eval g env s2 t2 [])) s2 as in VAlts vd vas eval g env c (Strs ts) [] = VStrs (mapC (\c t -> eval g env c t []) c ts) eval g env c (Markup tag as ts) [] = @@ -338,24 +312,22 @@ eval g env c (Markup tag as ts) [] = in (VMarkup tag vas vs) eval g env c (Reset ctl mb_ct t qid) [] = VReset ctl (fmap (\t -> eval g env c t []) mb_ct) (eval g env c t []) qid 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 (nty,n) cs) vs = if null cs - then VError ("No options in expression:" $$ ppTerm Unqualified 0 t) - else let (c1,c2,c3) = split3 c - (c1ty,c1t) = split c1 - vnty = eval g env c1ty (fromJust nty) [] - vn = eval g env c1t n [] - vcs = mapC evalOpt c2 cs - in VFV c3 (VarOpts vnty vn vcs) - where evalOpt c' ((lty,l),t) = let (c1,c2,c3) = split3 c' - in (eval g env c1 (fromJust lty) [], eval g env c2 l [], eval g env c3 t vs) -eval g env c t vs = VError ("Cannot reduce term" <+> pp t) +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' (Just l, t) = let (c1,c2) = split c' in (eval g env c1 l [], eval g env c2 t vs) + evalOpt c' (Nothing,t) = let v = eval g env c' t vs in (v, v) +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 (CFV i vs) = VFV i (fmap valueOf vs) valueOf (CSusp i k) = VSusp i (valueOf . k) [] valueOf RunTime = VApp c (cPredef,n) args valueOf NonExist = VApp c (cPredef,cNonExist) [] @@ -363,7 +335,8 @@ evalPredef g@(Gl gr pds) c n args = stdPredef :: Globals -> PredefTable stdPredef g = Map.fromList - [(cLength, pdArity 1 $\ \g c [v] -> fmap (VInt . genericLength) (value2string g v)) + [(cInts, pdArity 1 $\ \g c vs -> Const (case vs of {[VInt i] -> VInts i False; vs -> VApp c (cPredef,cInts) vs})) + ,(cLength, pdArity 1 $\ \g c [v] -> fmap (VInt . genericLength) (value2string g v)) ,(cTake, pdArity 2 $\ \g c [v1,v2] -> fmap string2value (liftA2 genericTake (value2int g v1) (value2string g v2))) ,(cDrop, pdArity 2 $\ \g c [v1,v2] -> fmap string2value (liftA2 genericDrop (value2int g v1) (value2string g v2))) ,(cTk, pdArity 2 $\ \g c [v1,v2] -> fmap string2value (liftA2 genericTk (value2int g v1) (value2string g v2))) @@ -389,14 +362,14 @@ 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 (VFV i fvs) vs = VFV i (mapVariants (\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 (VClosure env s (Abs b x t)) (v:vs) = eval g ((x,v):env) s t vs apply g v [] = v data BubbleVariants = BubbleFree Int - | BubbleOpts Value Value [(Value, Value)] + | BubbleOpts Value [Value] bubble v = snd (bubble v) where @@ -406,7 +379,9 @@ bubble v = snd (bubble v) bubble (VGen i vs) = liftL (VGen i) vs bubble (VClosure env c t) = liftL' (\env -> VClosure env c t) env bubble (VProd bt x v1 v2) = lift2 (VProd bt x) v1 v2 - bubble (VRecType as) = liftL' VRecType as + bubble v@(VRecType lbls ext) = + let (union,lbls') = mapAccumL descendR Map.empty lbls + in (union, addVariants (VRecType lbls' ext) union) bubble (VR as) = liftL' VR as bubble (VP v l vs) = lift1L (\v vs -> VP v l vs) v vs bubble (VExtR v1 v2) = lift2 VExtR v1 v2 @@ -426,30 +401,25 @@ bubble v = snd (bubble v) bubble v@(VFV c (VarFree vs)) | null vs = (Map.empty, v) | otherwise = let (union,vs') = mapAccumL descend Map.empty vs - b = BubbleFree (length vs) - v' = addVariants (VFV c (VarFree vs')) union - in (Map.insert c (b,1) union, v') - bubble v@(VFV c (VarOpts nty n os)) + in (Map.insert c (BubbleFree (length vs),1) union, VFV c (VarFree vs')) + bubble v@(VFV c (VarOpts n os)) | null os = (Map.empty, v) - | otherwise = let (union,os') = mapAccumL (\acc (lty,l,v) -> second (lty,l,) $ descend acc v) Map.empty os - b = BubbleOpts nty n (os <&> \(lty,l,_) -> (lty,l)) - v' = addVariants (VFV c (VarOpts nty n os')) union - in (Map.insert c (b,1) union, v') + | otherwise = let (union,os') = mapAccumL (\acc (k,v) -> second (k,) $ descend acc v) Map.empty os + in (Map.insert c (BubbleOpts n (map fst os),1) union, VFV c (VarOpts n os')) bubble (VAlts v vs) = lift1L2 VAlts v vs bubble (VStrs vs) = liftL VStrs vs bubble (VMarkup tag attrs vs) = let (union1,attrs') = mapAccumL descend' Map.empty attrs (union2,vs') = mapAccumL descend union1 vs in (union2, VMarkup tag attrs' vs') - bubble (VReset ctl mb_cv v id) = lift1 (\v -> VReset ctl mb_cv v id) v + bubble (VReset ctl mb_cv v id) = + let (union,v') = bubble v + in (Map.empty,VReset ctl mb_cv v' id) bubble (VSymCat d i0 vs) = let (union,vs') = mapAccumL descendC Map.empty vs in (union, addVariants (VSymCat d i0 vs') union) bubble v@(VError _) = lift0 v - bubble v@(VCRecType lbls) = - let (union,lbls') = mapAccumL descendR Map.empty lbls - in (union, addVariants (VCRecType lbls') union) - bubble v@(VCInts _ _) = lift0 v + bubble v@(VInts _ _) = lift0 v lift0 v = (Map.empty, v) @@ -519,8 +489,8 @@ bubble v = snd (bubble v) where addVariant c (bvs,cnt) v | cnt > 1 = VFV c $ case bvs of - BubbleFree k -> VarFree (replicate k v) - BubbleOpts nty n os -> VarOpts nty n (os <&> \(lty,l) -> (lty,l,v)) + BubbleFree k -> VarFree (replicate k v) + BubbleOpts n os -> VarOpts n (map (\l -> (l,v)) os) | otherwise = v unitfy = fmap (\(n,_) -> (n,1)) @@ -546,6 +516,11 @@ update lbl v (a@(lbl',_):as) | lbl==lbl' = (lbl,v) : as | otherwise = a : update lbl v as +update3 lbl o v [] = [(lbl,o,v)] +update3 lbl o v (a@(lbl',o',_):as) + | lbl==lbl' = (lbl,o||o',v) : as + | otherwise = a : update3 lbl o v as + patternMatch g s v0 [] = v0 patternMatch g s v0 ((env0,ps,args0,t):eqs) = match env0 ps eqs args0 where @@ -571,7 +546,7 @@ 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, VGen i vs) -> v0 (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 (mapVariants (\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) | q == r -> match env (qs++ps) eqs (vs++args) (PR pas, VR as) -> matchRec env (reverse pas) as ps eqs args @@ -630,7 +605,7 @@ vtableSelect g v0 ty cs v2 vs = where select (Const (i,_)) = cs !! i select (CSusp i k) = VSusp i (\v -> select (k v)) [] - select (CFV s vs) = VFV s (consts2variants select vs) + select (CFV c vs) = VFV c (fmap select vs) select _ = v0 value2index (VMeta i vs) ty = CSusp i (\v -> value2index (apply g v vs) ty) @@ -670,7 +645,7 @@ vtableSelect g v0 ty cs v2 vs = Gl gr _ = g value2index (VInt n) ty | Just max <- isTypeInts ty = Const (fromIntegral n,fromIntegral max+1) - value2index (VFV i vs) ty = CFV i (variants2consts (\v -> value2index v ty) vs) + value2index (VFV c vs) ty = CFV c (fmap (\v -> value2index v ty) vs) value2index v ty = RunTime @@ -681,29 +656,25 @@ value2term g xs v = do [t] -> return t ts -> return (FV ts) -type Constraint = Value data MetaState = Bound Scope Value | Narrowing Type - | Residuation Scope (Maybe Constraint) + | Residuation Scope data OptionInfo = OptionInfo - { optChoice :: Choice - , optLabelType :: Value - , optLabel :: Value - , optChoices :: [(Value, Value)] + { optChoice :: Choice + , optValue :: Int + , optLabel :: Value + , optChoices :: [Value] } -type ChoiceMap = Map.Map Choice Int data State = State - { choices :: ChoiceMap + { input :: [(Choice, Int)] + , choices :: Map.Map Choice Int , 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] newtype EvalM a = EvalM (forall r . Globals -> (a -> Cont r) -> Cont r) @@ -739,18 +710,15 @@ runEvalM g (EvalM f) = Check $ \(es,ws) -> Fail msg ws -> Fail msg (es,ws) Success xs ws -> Success (reverse xs) (es,ws) 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 +runEvalMWithInput :: Globals -> [(Choice,Int)] -> EvalM a -> Check [(a, [OptionInfo])] +runEvalMWithInput g input (EvalM f) = Check $ \(es,ws) -> + case f g (\x (State _ cs mvs os) xs ws -> Success ((x,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 [] - -withState :: State -> EvalM a -> EvalM a -withState state (EvalM f) = EvalM $ \g k _ r ws -> f g k state r ws + init = State input Map.empty Map.empty [] reset :: EvalM a -> EvalM [a] reset (EvalM f) = EvalM $ \g k state r ws -> @@ -768,50 +736,62 @@ globals :: EvalM Globals globals = EvalM (\g k -> k g) variants :: Choice -> [a] -> EvalM a -variants c xs = EvalM (\g k state@(State choices metas opts) r msgs -> +variants c xs = EvalM (\g k state@(State input choices metas opts) r msgs -> case Map.lookup c choices of Just j -> k (xs !! j) state r msgs - Nothing -> backtrack 0 xs k choices metas opts r msgs) + Nothing -> backtrack 0 xs k input choices metas opts r msgs) where - backtrack j [] k choices metas opts r msgs = Success r msgs - backtrack j (x:xs) k choices metas opts r msgs = - case k x (State (Map.insert c j choices) metas opts) r msgs of + backtrack j [] k input choices metas opts r msgs = Success r msgs + backtrack j (x:xs) k input choices metas opts r msgs = + case k x (State input (Map.insert c j choices) metas opts) r msgs of Fail msg msgs -> Fail msg msgs - Success r msgs -> backtrack (j+1) xs k choices metas opts r msgs + Success r msgs -> backtrack (j+1) xs k input choices metas opts r msgs variants' :: Choice -> (a -> EvalM Term) -> [a] -> EvalM Term -variants' c f xs = EvalM (\g k state@(State choices metas opts) r msgs -> +variants' c f xs = EvalM (\g k state@(State input choices metas opts) r msgs -> case Map.lookup c choices of Just j -> case f (xs !! j) of EvalM f -> f g k state r msgs - Nothing -> case backtrack g 0 xs choices metas opts [] msgs of + Nothing -> case backtrack g 0 xs input choices metas opts [] msgs of Fail msg msgs -> Fail msg msgs Success ts msgs -> k (FV (reverse ts)) state r msgs) where - backtrack g j [] choices metas opts ts msgs = Success ts msgs - backtrack g j (x:xs) choices metas opts ts msgs = + backtrack g j [] input choices metas opts ts msgs = Success ts msgs + backtrack g j (x:xs) input choices metas opts ts msgs = case f x 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 + EvalM f -> case f g (\t st ts msgs -> Success (t:ts) msgs) (State input (Map.insert c j choices) metas opts) ts msgs of Fail msg msgs -> Fail msg msgs - Success ts msgs -> backtrack g (j+1) xs choices metas opts ts msgs + Success ts msgs -> backtrack g (j+1) xs input choices metas opts ts msgs -try :: (a -> EvalM b) -> ([(b,State)] -> EvalM b) -> [a] -> EvalM b -try f select xs = EvalM (\g k state r msgs -> - let (res,msgs') = backtrack g xs state [] msgs +try :: Int -> (a -> EvalM b) -> ([b] -> EvalM b) -> [a] -> EvalM b +try sz f select xs = EvalM (\g k state r msgs -> + let (state',res,msgs') = backtrack sz g xs state [] msgs in case select res of - EvalM f' -> f' g k state r msgs') + EvalM f' -> f' g k state' r msgs') where - backtrack g [] state res msgs = (res,msgs) - backtrack g (x:xs) state res msgs = + backtrack sz g [] state res msgs = (state,res,msgs) + backtrack sz g (x:xs) state res msgs = case f x of - EvalM f -> case f g (\x state res msgs -> Success ((x,state):res) msgs) state res msgs of - Fail msg _ -> backtrack g xs state res msgs - Success res msgs -> backtrack g xs state res msgs + EvalM f -> case f g (\y state' (_,ys) msgs -> Success (cut sz state state',y:ys) msgs) state (state,res) msgs of + Fail msg _ -> backtrack sz g xs state res msgs + Success (state,res) msgs -> backtrack sz g xs state res msgs + + cut sz state state' = state'{metaVars=Map.mapWithKey select (metaVars state')} + where + select k ms + | k <= sz = ms + | otherwise = case Map.lookup k (metaVars state) of + Just ms -> ms + Nothing -> ms newResiduation :: Scope -> EvalM MetaId -newResiduation scope = EvalM (\g k (State choices metas opts) r msgs -> +newResiduation scope = EvalM (\g k (State input choices metas opts) r msgs -> let meta_id = Map.size metas+1 - in k meta_id (State choices (Map.insert meta_id (Residuation scope Nothing) metas) opts) r msgs) + in k meta_id (State input choices (Map.insert meta_id (Residuation scope) metas) opts) r msgs) + +checkpoint :: EvalM Int +checkpoint = EvalM (\g k state r msgs -> + k (Map.size (metaVars state)) state r msgs) getMeta :: MetaId -> EvalM MetaState getMeta i = EvalM (\g k state r msgs -> @@ -820,8 +800,8 @@ getMeta i = EvalM (\g k state r msgs -> Nothing -> Fail ("Metavariable ?"<>pp i<+>"is not defined") msgs) setMeta :: MetaId -> MetaState -> EvalM () -setMeta i ms = EvalM (\g k (State choices metas opts) r msgs -> - let state' = State choices (Map.insert i ms metas) opts +setMeta i ms = EvalM (\g k (State input choices metas opts) r msgs -> + let state' = State input choices (Map.insert i ms metas) opts in k () state' r msgs) value2termM :: Bool -> [Ident] -> Value -> EvalM Term @@ -832,11 +812,7 @@ value2termM flat xs (VMeta i vs) = do case mv of Bound scope v -> do g <- globals value2termM flat (map fst scope) (apply g v vs) - Residuation _ mb_ctr -> - case mb_ctr of - Just ctr -> do g <- globals - value2termM flat xs (apply g ctr vs) - Nothing -> foldM (\t v -> fmap (App t) (value2termM flat xs v)) (Meta i) vs + Residuation _ -> foldM (\t v -> fmap (App t) (value2termM flat xs v)) (Meta i) vs value2termM flat xs (VSusp j k vs) = let v = k (VGen maxBound vs) in value2termM flat xs v @@ -848,23 +824,19 @@ value2termM flat xs (VClosure env s (Abs b x t)) = do x' = mkFreshVar xs x t <- value2termM flat (x':xs) v return (Abs b x' t) -value2termM flat xs (VProd b x v1 v2) - | x == identW = do t1 <- value2termM flat xs v1 - v2 <- case v2 of - VClosure env s t2 -> do g <- globals - return (eval g env s t2 []) - v2 -> return v2 - t2 <- value2termM flat xs v2 - return (Prod b x t1 t2) - | otherwise = do t1 <- value2termM flat xs v1 - v2 <- case v2 of - VClosure env s t2 -> do g <- globals - return (eval g ((x,VGen (length xs) []):env) s t2 []) - v2 -> return v2 - t2 <- value2termM flat (x:xs) v2 - return (Prod b (mkFreshVar xs x) t1 t2) -value2termM flat xs (VRecType lbls) = do - lbls <- mapM (\(lbl,v) -> fmap ((,) lbl) (value2termM flat xs v)) lbls +value2termM flat xs (VClosure env s t) = do + return t +value2termM flat xs (VProd b x v1 (VClosure env c2 t2)) = do + g <- globals + t1 <- value2termM flat xs v1 + t2 <- value2termM flat (x:xs) (eval g ((x,VGen (length xs) []):env) c2 t2 []) + return (Prod b (mkFreshVar xs x) t1 t2) +value2termM flat xs (VProd b x v1 v2) = do + t1 <- value2termM flat xs v1 + t2 <- value2termM flat xs v2 + return (Prod b x t1 t2) +value2termM flat xs (VRecType lbls _) = do + lbls <- mapM (\(lbl,_,v) -> fmap ((,) lbl) (value2termM flat xs v)) lbls return (RecType lbls) value2termM flat xs (VR as) = do as <- mapM (\(lbl,v) -> fmap (\t -> (lbl,(Nothing,t))) (value2termM flat xs v)) as @@ -932,14 +904,20 @@ value2termM flat xs (VGlue v1 v2) = do value2termM True xs (VFV i (VarFree vs)) = do v <- variants i vs value2termM True xs v -value2termM False xs (VFV i (VarFree vs)) = variants' i (value2termM False xs) vs -value2termM flat xs (VFV i (VarOpts nty n os)) = - EvalM $ \g k (State choices metas opts) r msgs -> - let j = fromMaybe 0 (Map.lookup i choices) +value2termM False xs (VFV c (VarFree vs)) = variants' c (value2termM False xs) vs +value2termM flat xs (VFV c (VarOpts n os)) = + EvalM $ \g k (State input choices metas opts) r msgs -> + let (j,input',choices',opts') = + case Map.lookup c choices of + Just j -> (j,input,choices,opts) + Nothing -> case input of + (c',j):input | c == c' -> let oi = OptionInfo c j n (map fst os) + in (j,input,Map.insert c j choices,oi:opts) + _ -> let oi = OptionInfo c 0 n (map fst os) + in (0,[],Map.insert c 0 choices,oi:opts) in case os `maybeAt` j of - Just (lty,l,t) -> case value2termM flat xs t of - EvalM f -> let oi = OptionInfo i nty n (os <&> \(lty,l,_) -> (lty,l)) - in f g k (State choices metas (oi:opts)) r msgs + Just (l,t) -> case value2termM flat xs t of + EvalM f -> f g k (State input' choices' metas 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 (VPattType v) = do t <- value2termM flat xs v @@ -958,7 +936,7 @@ value2termM flat xs (VMarkup tag as vs) = do as <- mapM (\(id,v) -> value2termM flat xs v >>= \t -> return (id,t)) as ts <- mapM (value2termM flat xs) vs return (Markup tag as ts) -value2termM flat xs (VReset ctl mb_cv v qid) = do +value2termM flat xs (VReset ctl mb_cv v mb_qid) = do ts <- reset (value2termM True xs v) reduce ctl mb_cv ts where @@ -971,11 +949,36 @@ value2termM flat xs (VReset ctl mb_cv v qid) = do case ts of [t] -> return t ts -> return (Markup identW [] ts) + | ctl == cConcat' = do + ts <- case mb_cv of + Just (VInt n) -> return (genericTake n ts) + Nothing -> return ts + _ -> evalError (pp "[concat: .. | ..] requires an integer constant") + case ts of + [] -> mzero + [t] -> return t + ts -> return (Markup identW [] ts) | ctl == cOne = case (ts,mb_cv) of ([] ,Nothing) -> mzero ([] ,Just v) -> value2termM flat xs v (t:ts,_) -> return t + | ctl == cSelect = + case mb_cv of + Just (VInt n) | n >= 0 -> select n ts' + | otherwise -> select (-n-1) (reverse ts') + where + ts' = sortBy compareKey ts + + select _ [] = mzero + select 0 (t:ts) = + case t of + R rs -> case lookup (ident2label cp1) rs of + Just (_,t) -> return t + Nothing -> evalError (pp "Missing label p1") + _ -> evalError (pp "The term must be a record") + select n (t:ts) = select (n-1) ts + _ -> evalError (pp "[select: .. | ..] requires an integer constant") | ctl == cDefault = case (ts,mb_cv) of ([] ,Nothing) -> mzero @@ -986,24 +989,29 @@ value2termM flat xs (VReset ctl mb_cv v qid) = do ([], _) -> mzero ([t], _) -> return t (ts,Just cv) -> - do let cat = showIdent (snd qid) - mn = fst qid + do let Just (mn,id) = mb_qid + cat = showIdent id ct <- value2termM flat xs cv t <- listify mn cat ts return (App (App (QC (mn,identS ("Conj"++cat))) ct) t) _ -> evalError (pp "[list: .. | ..] requires an argument") + | ctl == cLen = + case mb_cv of + Just cv -> do g <- globals + value2termM True xs (apply g cv [VInt (genericLength ts)]) + Nothing -> return (EInt (genericLength ts)) | otherwise = evalError (pp "Operator" <+> pp ctl <+> pp "is not defined") listify mn cat [t1,t2] = do return (App (App (QC (mn,identS ("Base"++cat))) t1) t2) listify mn cat (t1:ts) = do t2 <- listify mn cat ts return (App (App (QC (mn,identS ("Cons"++cat))) t1) t2) + + compareKey (R rs1) (R rs2) = + case (lookup (ident2label cp2) rs1, lookup (ident2label cp2) rs2) of + (Just (_,K s1), Just (_,K s2)) -> compare s1 s2 + value2termM flat xs (VError msg) = evalError msg -value2termM flat xs (VCRecType lbls) = do - lbls <- mapM (\(lbl,_,v) -> fmap ((,) lbl) (value2termM flat xs v)) lbls - return (RecType lbls) -value2termM flat xs (VCInts Nothing Nothing) = return (App (QC (cPredef,cInts)) (Meta 0)) -value2termM flat xs (VCInts (Just min) Nothing) = return (App (QC (cPredef,cInts)) (EInt min)) -value2termM flat xs (VCInts _ (Just max)) = return (App (QC (cPredef,cInts)) (EInt max)) +value2termM flat xs (VInts n _) = return (App (Q (cPredef,cInts)) (EInt n)) value2termM flat xs v = evalError ("value2termM" <+> ppValue Unqualified 5 v) @@ -1019,17 +1027,27 @@ pattVars st (PSeq _ _ p1 _ _ p2) = pattVars (pattVars st p1) p2 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 (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 (VGen _ _) = pp "VGen" ppValue q d (VClosure env c t) = pp "[|" <> ppTerm q 4 t <> pp "|]" -ppValue q d (VProd _ _ _ _) = pp "VProd" -ppValue q d (VRecType _) = pp "VRecType" +ppValue q d (VProd bt x a b) = + if x == identW && bt == Explicit + then prec d 0 (ppValue q 4 a <+> "->" <+> ppValue q 0 b) + else prec d 0 (parens (ppBind (bt,x) <+> ':' <+> ppValue q 0 a) <+> "->" <+> ppValue q 0 b) +ppValue q d (VRecType xs ext) + | q == Terse = case [cat | (l,_,_) <- xs, let (p,cat) = splitAt 5 (showIdent (label2ident l)), p == "lock_"] of + [cat] -> pp cat + _ -> doc + | otherwise = doc + where + doc = braces (fsep (punctuate ';' ([l <+> (if o then ":" else ":?") <+> ppValue q 0 v | (l,o,v) <- xs] ++ [pp ".." | ext]))) ppValue q d (VR _) = pp "VR" ppValue q d (VP v l vs) = prec d 5 (hsep (ppValue q 5 v <> '.' <> l : map (ppValue q 5) vs)) ppValue q d (VExtR _ _) = pp "VExtR" -ppValue q d (VTable _ _) = pp "VTable" +ppValue q d (VTable kt vt) = prec d 0 (ppValue q 3 kt <+> "=>" <+> ppValue q 0 vt) ppValue q d (VT t _ _ cs) = "table" <+> ppValue q 0 t <+> '{' $$ nest 2 (vcat (punctuate ';' (map (ppCase q) cs))) $$ '}' @@ -1045,22 +1063,20 @@ ppValue q d VEmpty = pp "[]" ppValue q d (VC v1 v2) = prec d 1 (hang (ppValue q 2 v1) 2 ("++" <+> ppValue q 1 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 (VPattType _) = pp "VPattType" -ppValue q d (VFV i (VarFree vs)) = prec d 4 ("variants" <+> pp i <+> braces (fsep (punctuate ';' (map (ppValue q 0) vs)))) -ppValue q d (VFV i (VarOpts _ n os)) = prec d 4 ("option" <+> ppValue q 0 n <+> "of" <+> pp i <+> braces (fsep (punctuate ';' - (map (\(_,l,v) -> parens (ppValue q 0 l) <+> "=>" <+> ppValue q 0 v) os)))) +ppValue q d (VPattType v) = prec d 4 ("pattern" <+> ppValue q 0 v) +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 (VStrs _) = pp "VStrs" ppValue q d (VMarkup _ _ _) = pp "VMarkup" +ppValue q d (VReset ctl ct t _) = pp "[" <> pp ctl <> + maybe PP.empty (\v -> pp ':' <+> ppValue q 6 v) ct <> + pp "|" <> ppValue q 0 t <> + pp "]" ppValue q d (VSymCat i r rs) = pp '<' <> pp i <> pp ',' <> pp r <> pp '>' ppValue q d (VError msg) = prec d 4 (pp "error" <+> ppTerm q 5 (K (show msg))) -ppValue q d (VCRecType ass) = pp "VCRecType" -ppValue q d (VCInts Nothing Nothing) = prec d 4 (pp "Ints ?") -ppValue q d (VCInts (Just min) Nothing) = prec d 4 (pp "Ints" <+> brackets (pp min <> "..")) -ppValue q d (VCInts Nothing (Just max)) = prec d 4 (pp "Ints" <+> brackets (".." <> pp max)) -ppValue q d (VCInts (Just min) (Just max)) - | min == max = prec d 4 (pp "Ints" <+> min) - | otherwise = prec d 4 (pp "Ints" <+> brackets (pp min <> ".." <> pp max)) +ppValue q d (VInts n ext) + | ext = prec d 4 (pp "Ints" <+> brackets (pp n <> "..")) + | otherwise = prec d 4 (pp "Ints" <+> pp n) ppAltern q (x,y) = ppValue q 0 x <+> '/' <+> ppValue q 0 y @@ -1078,7 +1094,7 @@ 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) where concat v1 (Const (b,ws,qs)) = value2string' g v1 b ws qs - concat v1 (CFV i vs) = CFV i (mapConstVs (concat v1) vs) + concat v1 (CFV c vs) = CFV c (fmap (concat v1) vs) concat v1 res = res value2string' g (VApp c q []) b ws qs | q == (cPredef,cNonExist) = NonExist @@ -1112,7 +1128,7 @@ value2string' g (VAlts vd vas) b ws qs = | or [startsWith s w | VStr s <- ss] = value2string' g v | otherwise = pre vd vas w value2string' g (VFV s vs) b ws qs = - CFV s (variants2consts (\v -> value2string' g v b ws qs) vs) + CFV s (fmap (\v -> value2string' g v b ws qs) vs) value2string' _ _ _ _ _ = RunTime startsWith [] _ = True @@ -1129,9 +1145,29 @@ string2value' (w:ws) = VC (VStr w) (string2value' ws) 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 (VInt n) = Const n -value2int g (VFV s vs) = CFV s (variants2consts (value2int g) vs) +value2int g (VFV s vs) = CFV s (fmap (value2int g) vs) value2int g _ = RunTime +value2float g (VMeta i vs) = CSusp i (\v -> value2float g (apply g v vs)) +value2float g (VSusp i k vs) = CSusp i (\v -> value2float g (apply g (k v) vs)) +value2float g (VFlt f) = Const f +value2float g (VFV s vs) = CFV s (fmap (value2float g) vs) +value2float g _ = RunTime + +value2expr g xs (VApp _ (m,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 (VSusp i k vs) = CSusp i (\v -> value2expr g xs (apply g (k v) vs)) +value2expr g xs (VGen j vs) = foldl (\e v -> fmap EApp e <*> value2expr g xs v) (pure (EVar (length xs - j - 1))) vs +value2expr g xs (VClosure env s (Abs b x t)) = + let v = eval g ((x,VGen (length xs) []):env) s t [] + x' = mkFreshVar xs x + in fmap (EAbs b (showIdent x')) (value2expr g (x':xs) v) +value2expr g xs (VInt n) = pure (ELit (LInt n)) +value2expr g xs (VFlt f) = pure (ELit (LFlt f)) +value2expr g xs (VFV s vs) = CFV s (fmap (value2expr g xs) vs) +value2expr g xs v = fmap (ELit . LStr) (value2string g v) + newtype Choice = Choice { unchoice :: Integer } deriving (Eq,Ord,Pretty,Show) diff --git a/src/compiler/api/GF/Compile/GeneratePMCFG.hs b/src/compiler/api/GF/Compile/GeneratePMCFG.hs index b5861b350..383b11e41 100644 --- a/src/compiler/api/GF/Compile/GeneratePMCFG.hs +++ b/src/compiler/api/GF/Compile/GeneratePMCFG.hs @@ -131,13 +131,22 @@ type2metaTerm gr d ms r rs (RecType lbls) = do type2metaTerm gr d ms r rs (Table p q) | count == 1 = do (ms',r',t) <- type2metaTerm gr d ms r rs q return (ms',r+(r'-r),T (TTyped p) [(PW,t)]) - | otherwise = do let pv = varX (length rs+1) + | null (collectParams q) + = do let pv = varX (length rs+1) (ms',delta,t) <- fixST $ \(~(_,delta,_)) -> do (ms',r',t) <- type2metaTerm gr d ms r ((delta,(pv,p)):rs) q return (ms',r'-r,t) return (ms',r+delta*count,T (TTyped p) [(PV pv,t)]) + | otherwise = do ((ms',r'),ts) <- mapAccumM (\(ms,r) _ -> do (ms',r',t) <- type2metaTerm gr d ms r rs q + return ((ms',r'),t)) + (ms,r) [0..count-1] + return (ms',r+(r'-r),V p ts) where + collectParams (QC q) = [q] + collectParams (Table _ t) = collectParams t + collectParams t = collectOp collectParams t + count = case allParamValues gr p of Ok ts -> length ts Bad msg -> error msg @@ -214,11 +223,28 @@ str2lin (VSymCat d r rs) = do (r, rs) <- compute r rs str2lin (VSymVar d r) = return [SymVar d r] str2lin VEmpty = return [] str2lin (VC v1 v2) = liftM2 (++) (str2lin v1) (str2lin v2) -str2lin (VAlts def alts) = do def <- str2lin def - alts <- forM alts $ \(v,VStrs vs) -> do - lin <- str2lin v - return (lin,[s | VStr s <- vs]) +str2lin v0@(VAlts def alts) + = do def <- str2lin def + alts <- forM alts $ \(v1,v2) -> do + lin <- str2lin v1 + ss <- to_strs v2 + return (lin,ss) return [SymKP def alts] + where + to_strs (VStrs vs) = mapM to_str vs + to_strs (VPatt _ _ p) = from_patt p + to_strs v = fail + + to_str (VStr s) = return s + to_str _ = fail + + from_patt (PAlt p1 p2) = liftM2 (++) (from_patt p1) (from_patt p2) + from_patt (PSeq _ _ p1 _ _ p2) = liftM2 (liftM2 (++)) (from_patt p1) (from_patt p2) + from_patt (PString s) = return [s] + from_patt (PChars cs) = return (map (:[]) cs) + from_patt _ = fail + + fail = evalError ("Complex patterns are not supported in:" $$ nest 2 (pp (showValue v0))) str2lin v = do t <- value2term False [] v evalError ("the string:" <+> ppTerm Unqualified 0 t $$ "cannot be evaluated at compile time.") diff --git a/src/compiler/api/GF/Compile/Repl.hs b/src/compiler/api/GF/Compile/Repl.hs deleted file mode 100644 index 066ee1dc1..000000000 --- a/src/compiler/api/GF/Compile/Repl.hs +++ /dev/null @@ -1,315 +0,0 @@ -{-# LANGUAGE LambdaCase, TupleSections, NamedFieldPuns #-} - -module GF.Compile.Repl (ReplOpts(..), defaultReplOpts, replOptDescrs, getReplOpts, runRepl, runRepl') where - -import Control.Monad (join, when, unless, forM_, foldM) -import Control.Monad.IO.Class (MonadIO) -import qualified Data.ByteString.Char8 as BS -import Data.Char (isSpace) -import Data.Function ((&)) -import Data.Functor ((<&>)) -import Data.List (find) -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.Haskeline (InputT, Settings(..), noCompletion, runInputT, getInputLine, outputStrLn) -import System.Directory (getAppUserDataDirectory) - -import GF.Compile (batchCompile) -import GF.Compile.Compute.Concrete2 - ( Choice(..) - , ChoiceMap - , Globals(Gl) - , OptionInfo(..) - , bubble - , stdPredef - , unit - , eval - , cleanOptions - , runEvalMWithOpts - , value2termM - , ppValue - ) -import GF.Compile.Rename (renameSourceTerm) -import GF.Compile.TypeCheck.ConcreteNew (inferLType) -import GF.Data.ErrM (Err(..)) -import GF.Data.Utilities (maybeAt, orLeft) -import GF.Grammar.Grammar - ( Grammar - , mGrammar - , Info - , Module - , ModuleName - , ModuleInfo(..) - , ModuleType(MTResource) - , ModuleStatus(MSComplete) - , OpenSpec(OSimple) - , Location (NoLoc) - , Term(Typed) - , prependModule - ) -import GF.Grammar.Lexer (Posn(..), Lang(..), runLangP) -import GF.Grammar.Parser (pTerm) -import GF.Grammar.Printer (TermPrintQual(Unqualified), ppTerm) -import GF.Infra.CheckM (Check, runCheck) -import GF.Infra.Ident (moduleNameS) -import GF.Infra.Option (noOptions) -import GF.Infra.UseIO (justModuleName) -import GF.Text.Pretty (render) - -data ReplOpts = ReplOpts - { lang :: Lang - , noPrelude :: Bool - , inputFiles :: [String] - , evalToFlat :: Bool - } - -defaultReplOpts :: ReplOpts -defaultReplOpts = ReplOpts - { lang = GF - , noPrelude = False - , inputFiles = [] - , evalToFlat = True - } - -type Errs a = Either [String] a -type ReplOptsOp = ReplOpts -> Errs ReplOpts - -replOptDescrs :: [OptDescr ReplOptsOp] -replOptDescrs = - [ 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 [] ["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 - flag f = NoArg $ \o -> pure (f o) - -getReplOpts :: [String] -> Errs ReplOpts -getReplOpts args = case errs of - [] -> foldM (&) defaultReplOpts flags <&> \o -> o { inputFiles = inputFiles } - _ -> Left errs - where - (flags, inputFiles, errs) = getOpt RequireOrder replOptDescrs args - -execCheck :: MonadIO m => Check a -> (a -> InputT m b) -> InputT m (Maybe b) -execCheck c k = case runCheck c of - Ok (a, warn) -> do - unless (null warn) $ outputStrLn warn - Just <$> k a - Bad err -> do - outputStrLn err - return Nothing - -replModNameStr :: String -replModNameStr = "" - -replModName :: ModuleName -replModName = moduleNameS replModNameStr - -parseThen :: MonadIO m => Lang -> Grammar -> String -> (Term -> InputT m b) -> InputT m (Maybe b) -parseThen l g s k = case runLangP l pTerm (BS.pack s) of - Left (Pn l c, err) -> do - outputStrLn $ err ++ " (" ++ show l ++ ":" ++ show c ++ ")" - return Nothing - Right t -> execCheck (renameSourceTerm g replModName t) $ \t -> k t - -data ResultState = ResultState - { srsResult :: Term - , srsChoices :: ChoiceMap - , srsOptInfo :: [OptionInfo] - , srsOpts :: ChoiceMap - } -data OptionState = OptionState - { osTerm :: Term - , osResults :: [ResultState] - , osSelected :: Maybe ResultState - } -newtype ReplState = ReplState - { rsOpts :: Maybe OptionState - } - -initState :: ReplState -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 -- show the inferred type of ." - outputStrLn ":r -- show the results of the last eval." - outputStrLn ":s -- select the result at ." - outputStrLn ":c -- show the current selected result." - outputStrLn ":o -- set option to ." - 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 -> - forM_ res $ \(t, ty) -> - let t' = case t of - Typed _ _ -> t - t -> Typed t ty - in outputStrLn $ render (ppTerm Unqualified 0 t') - nlrepl st - - -- 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 - - -- Select a result to "focus" by its index - command st "s" arg = do - 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))) }) - - -- Show the current selected result - command st "c" arg = do - let e = do (OptionState t _ sel) <- orLeft "No results to select!" $ rsOpts st - (ResultState r _ ois os) <- orLeft "No result selected!" sel - return (t, r, ois, os) - 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 opts@ReplOpts { noPrelude, inputFiles } = do - -- TODO accept an ngf grammar - let toLoad = if noPrelude then inputFiles else "prelude/Predef.gfo" : inputFiles - (g0, opens) <- case toLoad of - [] -> pure (mGrammar [], []) - _ -> do - (_, g0) <- batchCompile noOptions Nothing toLoad - pure (g0, OSimple . moduleNameS . justModuleName <$> toLoad) - let - modInfo = ModInfo - { mtype = MTResource - , mstatus = MSComplete - , mflags = noOptions - , mextend = [] - , mwith = Nothing - , mopens = opens - , mexdeps = [] - , msrc = replModNameStr - , mseqs = Nothing - , jments = Map.empty - } - g = Gl (prependModule g0 (replModName, modInfo)) (if noPrelude then Map.empty else stdPredef g) - runRepl' opts g diff --git a/src/compiler/api/GF/Compile/TypeCheck/Concrete.hs b/src/compiler/api/GF/Compile/TypeCheck/Concrete.hs index 9c2f88443..d85972e95 100644 --- a/src/compiler/api/GF/Compile/TypeCheck/Concrete.hs +++ b/src/compiler/api/GF/Compile/TypeCheck/Concrete.hs @@ -1,341 +1,848 @@ -{-# LANGUAGE PatternGuards #-} -module GF.Compile.TypeCheck.Concrete( checkLType, inferLType, computeLType, ppType ) where -import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint +{-# LANGUAGE RankNTypes, CPP, TupleSections, LambdaCase #-} +module GF.Compile.TypeCheck.Concrete ( checkLType, checkLType', inferLType, inferLType' ) where -import GF.Infra.CheckM -import GF.Data.Operations +-- The code here is based on the paper: +-- Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich. +-- Practical type inference for arbitrary-rank types. +-- 14 September 2011 -import GF.Grammar +import GF.Grammar hiding (Env, VGen, VApp, VRecType, ppValue) import GF.Grammar.Lookup import GF.Grammar.Predef -import GF.Grammar.PatternMatch -import GF.Grammar.Lockfield (isLockLabel, lockRecType, unlockRecord) -import GF.Compile.Compute.Concrete(normalForm,Globals(..),stdPredef) - -import Data.List -import Data.Maybe(fromMaybe,isJust,isNothing) -import Control.Monad +import GF.Grammar.Lockfield +import GF.Compile.Compute.Concrete2 +import GF.Infra.CheckM +import GF.Data.ErrM ( Err(Ok, Bad) ) +import Control.Applicative(Applicative(..),(<|>)) +import Control.Monad(ap,liftM,liftM2,mplus,foldM,zipWithM,forM,filterM,unless) +import Control.Monad.ST import GF.Text.Pretty +import Data.STRef +import Data.List (nub, (\\), tails) +import qualified Data.Map as Map +import Data.Maybe(fromMaybe,isNothing,mapMaybe) +import Data.Bifunctor(second) +import Data.Functor((<&>)) +import qualified Control.Monad.Fail as Fail -computeLType :: SourceGrammar -> Context -> Type -> Check Type -computeLType gr g0 t = comp (reverse [(b,x, Vr x) | (b,x,_) <- g0] ++ g0) t - where - comp g ty = case ty of - _ | Just _ <- isTypeInts ty -> return ty ---- shouldn't be needed - | isPredefConstant ty -> return ty ---- shouldn't be needed +checkLType :: Globals -> Term -> Type -> Check (Term, Type) +checkLType globals t ty = do + res <- runEvalM globals $ do + let (c1,c2) = split unit + (t,vty) <- checkLType' c1 t (eval globals [] c2 ty []) + ty <- value2termM True [] vty + return (t,ty) + case res of + [tty] -> return tty + _ -> checkError (pp "Encountered variants while type checking") - Q (m,ident) -> checkIn ("module" <+> m) $ do - ty' <- lookupResDef gr (m,ident) - if ty' == ty then return ty else comp g ty' --- is this necessary to test? +checkLType' :: Choice -> Term -> Value -> EvalM (Term, Value) +checkLType' c t vty = do + (t,vty) <- tcRho [] c t (Just vty) + t <- zonkTerm [] t + return (t,vty) - AdHocOverload ts -> do - over <- getOverload gr g (Just typeType) t - case over of - Just (tr,_) -> return tr - _ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 t) +inferLType :: Globals -> Term -> Check (Term, Type) +inferLType globals t = do + res <- runEvalM globals $ do + (t,vty) <- inferLType' t + ty <- value2termM True [] vty + return (t,ty) + case res of + [tty] -> return tty + _ -> checkError (pp "Encountered variants while type checking") - Vr ident -> checkLookup ident g -- never needed to compute! +inferLType' :: Term -> EvalM (Term, Value) +inferLType' t = do + (t,vty) <- inferSigma [] unit t + t <- zonkTerm [] t + return (t,vty) - App f a -> do - f' <- comp g f - a' <- comp g a - case f' of - Abs b x t -> comp ((b,x,a'):g) t - _ -> return $ App f' a' +inferSigma :: Scope -> Choice -> Term -> EvalM (Term,Sigma) +inferSigma scope s t = do -- GEN1 + (t,ty) <- tcRho scope s t Nothing + env_tvs <- getMetaVars (scopeTypes scope) + res_tvs <- getMetaVars [(scope,ty)] + let forall_tvs = res_tvs \\ env_tvs + quantify scope t forall_tvs ty - Prod bt x a b -> do - a' <- comp g a - b' <- comp ((bt,x,Vr x) : g) b - return $ Prod bt x a' b' +vtypeInt = VApp poison (cPredef,cInt) [] +vtypeFloat = VApp poison (cPredef,cFloat) [] +vtypeStr = VSort cStr +vtypeStrs = VSort cStrs +vtypeType = VSort cType +vtypePType = VSort cPType +vtypeMarkup= VApp poison (cPredef,cMarkup) [] - Abs bt x b -> do - b' <- comp ((bt,x,Vr x):g) b - return $ Abs bt x b' +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@(EFloat _) mb_ty = instSigma scope s t vtypeFloat mb_ty -- FLOAT +tcRho scope s t@(K _) mb_ty = instSigma scope s t vtypeStr mb_ty -- STR +tcRho scope s t@(Empty) mb_ty = instSigma scope s t vtypeStr mb_ty +tcRho scope s t@(Vr v) mb_ty = do -- VAR + case lookup v scope of + Just v_sigma -> instSigma scope s t v_sigma mb_ty + Nothing -> evalError ("Unknown variable" <+> v) +tcRho scope c t@(Q id) mb_ty = tcApp scope c t t [] mb_ty +tcRho scope c t@(QC id) mb_ty = tcApp scope c t t [] mb_ty +tcRho scope c t@(App fun arg) mb_ty = tcApp scope c t t [] mb_ty +tcRho scope c (Abs bt var body) Nothing = do -- ABS1 + i <- newResiduation scope + let arg_ty = VMeta i [] + (body,body_ty) <- tcRho ((var,arg_ty):scope) c body Nothing + let m = length scope + n = m+1 + (b,used_bndrs) <- check m n (False,[]) body_ty + if b + then let v = head (allBinders \\ used_bndrs) + 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)) + where + check m n st (VApp c f vs) = foldM (check m n) st vs + check m n st (VMeta i vs) = do + state <- getMeta i + case state of + Bound _ v -> do g <- globals + check m n st (apply g v vs) + _ -> foldM (check m n) st vs + check m n st@(b,xs) (VGen i vs) + | i == m = return (True, xs) + | otherwise = return st + check m n st (VClosure env c (Abs bt x t)) = do + g <- globals + check m (n+1) st (eval g ((x,VGen n []):env) c t []) + check m n st (VProd _ x v1 v2) = do + st@(b,xs) <- check m n st v1 + case v2 of + VClosure env c t -> do g <- globals + check m (n+1) (b,x:xs) (eval g ((x,VGen n []):env) c t []) + v2 -> check m n st v2 + check m n st (VRecType as _) = foldM (\st (l,_,v) -> check m n st v) st as + check m n st (VR as) = + foldM (\st (lbl,tnk) -> check m n st tnk) st as + check m n st (VP v l vs) = + check m n st v >>= \st -> foldM (check m n) st vs + check m n st (VExtR v1 v2) = + check m n st v1 >>= \st -> check m n st v2 + check m n st (VTable v1 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 ty -- Traverse cs as well + check m n st (VV ty cs) = + check m n st ty >>= \st -> foldM (check m n) st cs + check m n st (VS v1 tnk vs) = do + st <- check m n st v1 + st <- check m n st tnk + foldM (check m n) st vs + check m n st (VSort _) = return st + check m n st (VInt _) = return st + check m n st (VFlt _) = return st + check m n st (VStr _) = return st + check m n st VEmpty = return st + check m n st (VC v1 v2) = + check m n st v1 >>= \st -> check m n st v2 + check m n st (VGlue v1 v2) = + check m n st v1 >>= \st -> check m n st v2 + check m n st (VPatt _ _ _) = return st + check m n st (VPattType v) = check m n st v + check m n st (VAlts v vs) = do + st <- check m n st v + foldM (\st (v1,v2) -> check m n st v1 >>= \st -> check m n st v2) st vs + check m n st (VStrs vs) = + foldM (check m n) st vs + check m n st (VInts _ _) = return st +tcRho scope c t@(Abs Implicit var body) (Just ty) = do -- ABS2 + (bt, x, var_ty, body_ty) <- unifyFun scope ty + if bt == Implicit + then return () + else evalError (ppTerm Unqualified 0 t <+> "is an implicit function, but no implicit function is expected") + body_ty <- evalCodomain x (VGen (length scope) []) body_ty + (body, body_ty) <- tcRho ((var,var_ty):scope) c body (Just body_ty) + return (Abs Implicit var body,ty) +tcRho scope c (Abs Explicit var body) (Just ty) = do -- ABS3 + (scope,f,ty') <- skolemise scope ty + (_,x,var_ty,body_ty) <- unifyFun scope ty' + body_ty <- evalCodomain x (VGen (length scope) []) body_ty + (body, body_ty) <- tcRho ((var,var_ty):scope) c body (Just body_ty) + return (f (Abs Explicit var body),ty) +tcRho scope c (Meta _) mb_ty = do + i <- newResiduation scope + ty <- case mb_ty of + Just ty -> return ty + Nothing -> do j <- newResiduation scope + return (VMeta j []) + return (Meta i, ty) +tcRho scope c (Let (var, (Nothing, rhs)) body) mb_ty = do -- LET + let (c1,c2) = split c + (rhs,var_ty) <- tcRho scope c1 rhs Nothing + (body, body_ty) <- tcRho ((var,var_ty):scope) c2 body mb_ty + var_ty <- value2termM True (scopeVars scope) var_ty + return (Let (var, (Just var_ty, rhs)) body, body_ty) +tcRho scope c (Let (var, (Just ann_ty, rhs)) body) mb_ty = do -- LET + let (c1,c2,c3,c4) = split4 c + (ann_ty, _) <- tcRho scope c1 ann_ty (Just vtypeType) + g <- globals + let v_ann_ty = eval g (scopeEnv scope) c2 ann_ty [] + (rhs,_) <- tcRho scope c3 rhs (Just v_ann_ty) + (body, body_ty) <- tcRho ((var,v_ann_ty):scope) c4 body mb_ty + var_ty <- value2termM True (scopeVars scope) v_ann_ty + return (Let (var, (Just var_ty, rhs)) body, body_ty) +tcRho scope c (Typed body ann_ty) mb_ty = do -- ANNOT + let (c1,c2,c3,c4) = split4 c + (ann_ty, _) <- tcRho scope c1 ann_ty (Just vtypeType) + g <- globals + let v_ann_ty = eval g (scopeEnv scope) c2 ann_ty [] + (body,_) <- tcRho scope c3 body (Just v_ann_ty) + instSigma scope c4 (Typed body ann_ty) v_ann_ty mb_ty +tcRho scope c (FV ts) mb_ty = do + (ts,ty) <- tcUnifying scope c ts mb_ty + return (FV ts, ty) +tcRho scope s t@(Sort _) mb_ty = do + instSigma scope s t vtypeType mb_ty +tcRho scope c t@(RecType rs) Nothing = do + (rs,mb_ty) <- tcRecTypeFields scope c [] rs Nothing + return (RecType rs,fromMaybe vtypePType mb_ty) +tcRho scope c t@(RecType rs) (Just ty) = do + (scope,f,ty') <- skolemise scope ty + case ty' of + VSort s + | s == cType -> return () + | s == cPType -> return () + VMeta i vs-> case rs of + [] -> unifyVar scope i vs vtypePType + _ -> return () + ty -> do ty <- value2termM False (scopeVars scope) ty + evalError ("The record type" <+> ppTerm Unqualified 0 t $$ + "cannot be of type" <+> ppTerm Unqualified 0 ty) + (rs,mb_ty) <- tcRecTypeFields scope c [] rs (Just ty') + return (f (RecType rs),ty) +tcRho scope s t@(Table p res) mb_ty = do + let (s1,s23) = split s + (s2,s3) = split s23 + (p, p_ty) <- tcRho scope s1 p (Just vtypePType) + (res,res_ty) <- tcRho scope s2 res (Just vtypeType) + instSigma scope s3 (Table p res) vtypeType mb_ty +tcRho scope c (Prod bt x ty1 ty2) mb_ty = do + let (c1,c2,c3,c4) = split4 c + (ty1,ty1_ty) <- tcRho scope c1 ty1 (Just vtypeType) + g <- globals + (ty2,ty2_ty) <- tcRho ((x,eval g (scopeEnv scope) c2 ty1 []):scope) c3 ty2 (Just vtypeType) + instSigma scope c4 (Prod bt x ty1 ty2) vtypeType mb_ty +tcRho scope c (S t p) mb_ty = do + let (c1,c2) = split c + let mk_val i = VMeta i [] + p_ty <- fmap mk_val $ newResiduation scope + res_ty <- case mb_ty of + Nothing -> fmap mk_val $ newResiduation scope + Just ty -> return ty + let t_ty = VTable p_ty res_ty + (t,t_ty) <- tcRho scope c1 t (Just t_ty) + (p,_) <- tcRho scope c2 p (Just p_ty) + return (S t p, res_ty) +tcRho scope c (T tt ps) Nothing = do -- ABS1/AABS1 for tables + let (c1,c2) = split c + mb_p_ty <- case tt of + TRaw -> return Nothing + TTyped ty -> do let (c3,c4) = split c1 + (ty, _) <- tcRho scope c3 ty (Just vtypeType) + g <- globals + return (Just (eval g (scopeEnv scope) c4 ty [])) + (ps,p_ty,res_ty) <- tcCases scope c2 ps mb_p_ty Nothing + p_ty_t <- value2termM True [] p_ty + return (T (TTyped p_ty_t) ps, VTable p_ty res_ty) +tcRho scope c (T tt ps) (Just ty) = do -- ABS2/AABS2 for tables + let (c12,c34) = split c + (c3,c4) = split c34 + (scope,f,ty') <- skolemise scope ty + (p_ty, res_ty) <- unifyTbl scope ty' + case tt of + TRaw -> return () + TTyped ty -> do let (c1,c2) = split c12 + (ty, _) <- tcRho scope c1 ty (Just vtypeType) + g <- globals + subsCheckRho scope (Meta 0) (eval g (scopeEnv scope) c2 ty []) p_ty + return () + (ps,p_ty,res_ty) <- tcCases scope c3 ps (Just p_ty) (Just res_ty) + p_ty_t <- value2termM True (scopeVars scope) p_ty + return (f (T (TTyped p_ty_t) ps), VTable p_ty res_ty) +tcRho scope c (V p_ty ts) Nothing = do + let (c1,c2,c3,c4) = split4 c + (p_ty, _) <- tcRho scope c1 p_ty (Just vtypeType) + i <- newResiduation scope + let res_ty = VMeta i [] - Let (x,(_,a)) b -> comp ((Explicit,x,a):g) b + let go c t = do (t, ty) <- tcRho scope c t Nothing + (t,_,_) <- subsCheckRho scope t ty res_ty + return t - ExtR r s -> do - r' <- comp g r - s' <- comp g s - case (r',s') of - (RecType rs, RecType ss) -> plusRecType r' s' >>= comp g - _ -> return $ ExtR r' s' + ts <- mapCM go c2 ts + g <- globals + return (V p_ty ts, VTable (eval g (scopeEnv scope) c3 p_ty []) res_ty) +tcRho scope c (V p_ty0 ts) (Just ty) = do + let (c1,c2,c3,c4) = split4 c + (scope,f,ty') <- skolemise scope ty + (p_ty, res_ty) <- unifyTbl scope ty' + (p_ty0, _) <- tcRho scope c1 p_ty0 (Just vtypeType) + g <- globals + let p_vty0 = eval g (scopeEnv scope) c2 p_ty0 [] + unify scope p_ty p_vty0 + ts <- mapCM (\c t -> fmap fst $ tcRho scope c t (Just res_ty)) c3 ts + return (V p_ty0 ts, VTable p_ty res_ty) +tcRho scope c (R rs) Nothing = do + lttys <- inferRecFields scope c [] rs + rs <- mapM (\(l,t,ty) -> value2termM True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys + return (R rs, + VRecType [(l,True,ty) | (l,t,ty) <- lttys] False + ) +tcRho scope c (R rs) (Just ty) = do + (scope,f,ty') <- skolemise scope ty + case ty' of + (VRecType ltys _)->do lttys <- checkRecFields scope c [] rs ltys + rs <- mapM (\(l,t,ty) -> value2termM True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys + return ((f . R) rs, + VRecType [(l,True,ty) | (l,t,ty) <- lttys] False + ) + ty -> do lttys <- inferRecFields scope c [] rs + t <- liftM (f . R) (mapM (\(l,t,ty) -> value2termM True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys) + let ty' = VRecType [(l,True,ty) | (l,t,ty) <- lttys] False + (t,_,_) <- subsCheckRho scope t ty' ty + return (t, ty') +tcRho scope c (P t l) mb_ty = do + l_ty <- case mb_ty of + Just ty -> return ty + Nothing -> do i <- newResiduation scope + return (VMeta i []) + (t,t_ty) <- tcRho scope c t (Just (VRecType [(l,True,l_ty)] True)) + return (P t l,l_ty) +tcRho scope c (C t1 t2) mb_ty = do + let (c1,c2,c3,c4) = split4 c + (t1,t1_ty) <- tcRho scope c1 t1 (Just vtypeStr) + (t2,t2_ty) <- tcRho scope c2 t2 (Just vtypeStr) + instSigma scope c3 (C t1 t2) vtypeStr mb_ty +tcRho scope c (Glue t1 t2) mb_ty = do + let (c1,c2,c3,c4) = split4 c + (t1,t1_ty) <- tcRho scope c1 t1 (Just vtypeStr) + (t2,t2_ty) <- tcRho scope c2 t2 (Just vtypeStr) + instSigma scope c3 (Glue t1 t2) vtypeStr mb_ty +tcRho scope c t@(ExtR t1 t2) mb_ty = + case (t2,mb_ty) of + (R rs,Just (VRecType ltys ext)) -> do + let ll2 = map fst rs + (c1,c2) = split c - RecType fs -> do - let fs' = sortRec fs - liftM RecType $ mapPairsM (comp g) fs' + (t1,ty1@(VRecType ltys1 ext)) <- tcRho scope c1 t1 (Just (VRecType [field | field@(l,_,_) <- ltys, not (elem l ll2)] ext)) + let (scope',proj1,wrap) = access scope t1 ty1 - ELincat c t -> do - t' <- comp g t - lockRecType c t' ---- locking to be removed AR 20/6/2009 + lttys2 <- checkRecFields scope' c2 [] rs [field | field@(l,_,_) <- ltys, elem l ll2] + let proj2 l = + case [(Nothing,t) | (l',t,_) <- lttys2, l'==l] of + [] -> Nothing + (x:_) -> Just x - _ | ty == typeTok -> return typeStr + return (wrap (R [(l,t) | (l,_,_) <- ltys, Just t <- [if elem l ll2 then proj2 l else proj1 l]]), + VRecType ltys False + ) + _ -> do + let (c1,c2,c3,c4) = split4 c + (t1,t1_ty) <- tcRho scope c1 t1 Nothing + (t2,t2_ty) <- tcRho scope c2 t2 Nothing + ty <- join t1_ty t2_ty + let (scope1,proj1,wrap1) = access scope t1 t1_ty + (scope2,proj2,wrap2) = access scope1 t2 t2_ty + let t = case (mb_ty,ty,t2_ty) of + (Just (VRecType ltys False), _, VRecType ltys2 False) -> + let ll2 = [l | (l,_,_) <- ltys2] + in (wrap1 . wrap2) (R [(l,t) | (l,_,_) <- ltys, Just t <- [if elem l ll2 then proj2 l else proj1 l]]) + (_, VRecType ltys False, VRecType ltys2 False) -> + let ll2 = [l | (l,_,_) <- ltys2] + in (wrap1 . wrap2) (R [(l,t) | (l,_,_) <- ltys, Just t <- [if elem l ll2 then proj2 l else proj1 l]]) + _ -> ExtR t1 t2 + return (t,ty) + where + access scope (R rs) ty = (scope + ,\l -> lookup l rs + ,id + ) + access scope (RecType rs) ty + = (scope + ,\l -> fmap ((,) Nothing) (lookup l rs) + ,id + ) + access scope t@(Vr x) ty + = (scope + ,\l -> return (Nothing,P t l) + ,id + ) + access scope t ty = let x = newVar scope + in (((x,ty):scope) + ,\l -> return (Nothing,P (Vr x) l) + ,Let (x, (Nothing, t)) + ) - _ -> composOp (comp g) ty + join (VMeta i vs) ty2 = do + mv <- getMeta i + case mv of + Bound _ v -> do + g <- globals + join (apply g v vs) ty2 + _ -> evalError (pp "Cannot type check record extensions when one of the types is a meta variable") + join ty1 (VMeta j vs) = do + mv <- getMeta j + case mv of + Bound _ v -> do + g <- globals + join ty1 (apply g v vs) + _ -> evalError (pp "Cannot type check record extensions when one of the types is a meta variable") + join (VSort s1) (VSort s2) + | (s1 == cType || s1 == cPType) && + (s2 == cType || s2 == cPType) = let sort | s1 == cPType && s2 == cPType = cPType + | otherwise = cType + in return (VSort sort) + join (VRecType rs1 ext1) (VRecType rs2 ext2) = do + rs <- foldM (\rs (l,o,ctr) -> extend l o ctr rs) rs1 rs2 + return (VRecType rs (ext1 || ext2)) + where + extend l o1 ty1 [] = do return [(l,o1,ty1)] + extend l o1 ty1 ((l',o2,ty2):rs) + | l == l' = do return ((l,o1,ty1):rs) + | otherwise = do rs <- extend l o1 ty1 rs + return ((l',o2,ty2):rs) + join ty1 ty2 = do ty1 <- value2termM False (scopeVars scope) ty1 + ty2 <- value2termM False (scopeVars scope) ty2 + evalError ("Cannot type check" <+> ppTerm Unqualified 0 t $$ + " with types" <+> (ppTerm Unqualified 0 ty1 $$ + ppTerm Unqualified 0 ty2)) +tcRho scope c (ELin cat t) mb_ty = do -- this could be done earlier, i.e. in the parser + tcRho scope c (ExtR t (R [(lockLabel cat,(Just (RecType []),R []))])) mb_ty +tcRho scope c (ELincat cat t) mb_ty = do -- this could be done earlier, i.e. in the parser + tcRho scope c (ExtR t (RecType [(lockLabel cat,RecType [])])) mb_ty +tcRho scope c (Alts t ss) mb_ty = do + let (c1,c2,c3,c4) = split4 c + (t,_) <- tcRho scope c1 t (Just vtypeStr) + ss <- mapCM (\c (t1,t2) -> do + let (c1,c2) = split c + (t1,_) <- tcRho scope c1 t1 (Just vtypeStr) + (t2,_) <- tcRho scope c2 t2 (Just vtypeStrs) + return (t1,t2)) + c2 ss + instSigma scope c3 (Alts t ss) vtypeStr mb_ty +tcRho scope c (Strs ss) mb_ty = do + let (c1,c2) = split c + ss <- mapCM (\c t -> do (t,_) <- tcRho scope c t (Just vtypeStr) + return t) + c1 ss + instSigma scope c2 (Strs ss) vtypeStrs mb_ty +tcRho scope c (EPattType ty) mb_ty = do + let (c1,c2) = split c + (ty, _) <- tcRho scope c1 ty (Just vtypeType) + instSigma scope c2 (EPattType ty) vtypeType mb_ty +tcRho scope c t@(EPatt _ _ p) mb_ty = do + (scope,f,mb_ty) <- case mb_ty of + Nothing -> return (scope,id,Nothing) + Just ty -> do (scope,f,ty) <- skolemise scope ty + case ty of + VPattType ty -> return (scope,f,Just ty) + _ -> evalError (ppTerm Unqualified 0 t <+> "must be of pattern type but" <+> ppTerm Unqualified 0 t <+> "is expected") + (_,ty) <- tcPatt scope c p mb_ty + (min,max,p) <- measurePatt p + return (f (EPatt min max p), VPattType ty) +tcRho scope c (Markup tag attrs children) mb_ty = do + let (c1,c2,c3,c4) = split4 c + attrs <- mapCM (\c (id,t) -> do + (t,_) <- tcRho scope c t Nothing + return (id,t)) + c1 attrs + res <- mapCM (\c child -> tcRho scope c child Nothing) c2 children + instSigma scope c3 (Markup tag attrs (map fst res)) vtypeMarkup mb_ty +tcRho scope c (Reset ctl mb_ct t qid) mb_ty + | ctl == cConcat || ctl == cConcat' = do + let (c1,c23) = split c + (c2,c3 ) = split c23 + (t,_) <- tcRho scope c1 t Nothing + mb_ct <- case mb_ct of + Just ct -> do (ct,_) <- tcRho scope c2 ct (Just vtypeInt) + return (Just ct) + Nothing -> return Nothing + instSigma scope c2 (Reset ctl mb_ct t qid) vtypeMarkup mb_ty + | ctl == cOne = do + let (c1,c2) = split c + (t,ty) <- tcRho scope c1 t mb_ty + (mb_ct,ty) <- case mb_ct of + Just ct -> do (ct,ty) <- tcRho scope c2 ct (Just ty) + return (Just ct,ty) + Nothing -> return (Nothing,ty) + return (Reset ctl mb_ct t qid,ty) + | ctl == cSelect = do + let (c1,c2) = split c + ty <- case mb_ty of + Just ty -> return ty + Nothing -> do i <- newResiduation scope + return (VMeta i []) + let rec_ty = VRecType [ (ident2label cp1, True, ty) + , (ident2label cp2, True, VSort cStr) + ] False + mb_ct <- case mb_ct of + Just ct -> do (ct,_) <- tcRho scope c2 ct (Just vtypeInt) + return (Just ct) + Nothing -> evalError (pp "[select: .. | ..] requires an integer argument") + (t,_) <- tcRho scope c1 t (Just rec_ty) + return (Reset ctl mb_ct t qid,ty) + | ctl == cDefault = do + let (c1,c2) = split c + (t,ty) <- tcRho scope c1 t mb_ty + (mb_ct,ty) <- case mb_ct of + Just ct -> do (ct,ty) <- tcRho scope c2 ct (Just ty) + return (Just ct,ty) + Nothing -> evalError (pp "[list: .. | ..] requires an argument") + return (Reset ctl mb_ct t qid,ty) + | ctl == cList = do + do let (c1,c2) = split c + mb_ct <- case mb_ct of + Just ct -> do (ct,ty) <- tcRho scope c1 ct Nothing + return (Just ct) + Nothing -> evalError (pp "[list: .. | ..] requires an argument") + (t,ty) <- tcRho scope c2 t mb_ty + case ty of + VApp c qid [] -> return (Reset ctl mb_ct t (Just qid), ty) + _ -> evalError (pp "Needs atomic type"<+>ppValue Unqualified 0 ty) + | ctl == cLen = do + do let (c1,c2) = split c + (t,_) <- tcRho scope c1 t Nothing + case mb_ct of + Just ct -> do res_ty <- case mb_ty of + Just ty -> return ty + Nothing -> do i <- newResiduation scope + return (VMeta i []) + (ct,_) <- tcRho scope c2 ct (Just (VProd Explicit identW vtypeInt res_ty)) + return (Reset ctl (Just ct) t Nothing, res_ty) + Nothing -> instSigma scope c2 (Reset ctl Nothing t Nothing) vtypeInt mb_ty + | otherwise = evalError (pp "Operator" <+> pp ctl <+> pp "is not defined") +tcRho scope s (Opts n cs) mb_ty = do + let (s1,s2,s3) = split3 s + (n,_) <- tcRho scope s1 n Nothing + (ls,_) <- tcUnifyingMaybe 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) --- the underlying algorithms +evalCodomain :: Ident -> Value -> Value -> EvalM Value +evalCodomain x v (VClosure env c ty) = do + g <- globals + return (eval g ((x,v):env) c ty []) +evalCodomain x _ ty = return ty -inferLType :: SourceGrammar -> Context -> Term -> Check (Term, Type) -inferLType gr g trm = case trm of +tcUnifying :: Scope -> Choice -> [Term] -> Maybe Rho -> EvalM ([Term], Value) +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 >>= \(t,_,_) -> return t) - Q ident -> checks [ - termWith trm $ lookupResType gr ident >>= computeLType gr g - , - lookupResDef gr ident >>= inferLType gr g - , - checkError ("cannot infer type of constant" <+> ppTerm Unqualified 0 trm) - ] + let go c t = do (t, ty) <- tcRho scope c t mb_ty + subsume t ty - QC ident -> checks [ - termWith trm $ lookupResType gr ident >>= computeLType gr g - , - lookupResDef gr ident >>= inferLType gr g - , - checkError ("cannot infer type of canonical constant" <+> ppTerm Unqualified 0 trm) - ] + ts <- mapCM go c ts + return (ts,ty) - Vr ident -> termWith trm $ checkLookup ident g +tcUnifyingMaybe :: Scope -> Choice -> [Maybe Term] -> Maybe Rho -> EvalM ([Maybe Term], Value) +tcUnifyingMaybe 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 >>= \(t,_,_) -> return t) - Typed e t -> do - t' <- computeLType gr g t - checkLType gr g e t' + let go c (Just t) = do (t, ty) <- tcRho scope c t mb_ty + fmap Just $ subsume t ty + go c Nothing = do return Nothing - AdHocOverload ts -> do - over <- getOverload gr g Nothing trm - case over of - Just trty -> return trty - _ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 trm) + ts <- mapCM go c ts + return (ts,ty) - App f a -> do - over <- getOverload gr g Nothing trm - case over of - Just trty -> return trty - _ -> do - (f',fty) <- inferLType gr g f - fty' <- computeLType gr g fty - case fty' of - Prod bt z arg val -> do - a' <- justCheck g a arg - ty <- if z == identW - then return val - else substituteLType [(bt,z,a')] val - return (App f' a',ty) - _ -> - let term = ppTerm Unqualified 0 f - funName = pp . head . words .render $ term - in checkError ("A function type is expected for" <+> term <+> "instead of type" <+> ppType fty $$ - "\n ** Maybe you gave too many arguments to" <+> funName <+> "\n") +tcCases scope c [] (Just p_ty) (Just res_ty) = return ([],p_ty,res_ty) +tcCases scope c ((p,t):cs) mb_p_ty mb_res_ty = do + let (c1,c2,c3,c4) = split4 c + (scope',p_ty) <- tcPatt scope c1 p mb_p_ty + (t,res_ty) <- tcRho scope' c2 t mb_res_ty + (cs,p_ty,res_ty) <- tcCases scope c3 cs (Just p_ty) (Just res_ty) + (_,_,p) <- measurePatt p + return ((p,t):cs,p_ty,res_ty) - S f x -> do - (f', fty) <- inferLType gr g f - case fty of - Table arg val -> do - x'<- justCheck g x arg - return (S f' x', val) - _ -> checkError ("table lintype expected for the table in" $$ nest 2 (ppTerm Unqualified 0 trm)) +tcApp scope c t0 (App fun arg) args mb_ty = tcApp scope c t0 fun (arg:args) mb_ty -- APP +tcApp scope c t0 t@(Q id) args mb_ty = resolveOverloads scope c t0 id args mb_ty -- VAR (global) +tcApp scope c t0 t@(QC id) args mb_ty = resolveOverloads scope c t0 id args mb_ty -- VAR (global) +tcApp scope c t0 t args mb_ty = do + let (c1,c23) = split c + let (c2,c3) = split c23 + (t,ty) <- tcRho scope c1 t Nothing + (t,ty) <- reapply1 scope c2 t ty args + instSigma scope c3 t ty mb_ty - P t i -> do - (t',ty) <- inferLType gr g t --- ?? - ty' <- computeLType gr g ty - let tr2 = P t' i - termWith tr2 $ case ty' of - RecType ts -> case lookup i ts of - Nothing -> checkError ("unknown label" <+> i <+> "in" $$ nest 2 (ppTerm Unqualified 0 ty')) - Just x -> return x - _ -> checkError ("record type expected for:" <+> ppTerm Unqualified 0 t $$ - " instead of the inferred:" <+> ppTerm Unqualified 0 ty') +reapply1 :: Scope -> Choice -> Term -> Value -> [Term] -> EvalM (Term,Rho) +reapply1 scope c fun fun_ty [] = return (fun,fun_ty) +reapply1 scope c fun fun_ty ((ImplArg arg):args) = do -- Implicit arg case + let (c1,c2,c3,c4) = split4 c + (bt, x, arg_ty, res_ty) <- unifyFun scope fun_ty + unless (bt == Implicit) $ + evalError (ppTerm Unqualified 0 (App fun (ImplArg arg)) <+> + "is an implicit argument application, but no implicit argument is expected") + (arg,_) <- tcRho scope c1 arg (Just arg_ty) + g <- globals + res_ty <- evalCodomain x (eval g (scopeEnv scope) c2 arg []) res_ty + reapply1 scope c3 (App fun (ImplArg arg)) res_ty args +reapply1 scope c fun fun_ty (arg:args) = do -- Explicit arg (fallthrough) case + let (c1,c2,c3,c4) = split4 c + (fun,fun_ty) <- instantiate scope fun fun_ty + (_, x, arg_ty, res_ty) <- unifyFun scope fun_ty + (arg,_) <- tcRho scope c1 arg (Just arg_ty) + g <- globals + res_ty <- evalCodomain x (eval g (scopeEnv scope) c2 arg []) res_ty + reapply1 scope c3 (App fun arg) res_ty args - R r -> do - let (ls,fs) = unzip r - fsts <- mapM inferM fs - let ts = [ty | (Just ty,_) <- fsts] - checkCond ("cannot infer type of record" $$ nest 2 (ppTerm Unqualified 0 trm)) (length ts == length fsts) - return $ (R (zip ls fsts), RecType (zip ls ts)) +resolveOverloads :: Scope -> Choice -> Term -> QIdent -> [Term] -> Maybe Rho -> EvalM (Term,Rho) +resolveOverloads scope c t0 q args mb_ty = do + g@(Gl gr _) <- globals + case lookupOverloadTypes gr q of + Bad msg -> evalError (pp msg) + Ok [(t,ty)] -> do let (c1,c23) = split c + (c2,c3) = split c23 + (t,ty) <- reapply1 scope c1 t (eval g [] c2 ty []) args + instSigma scope c3 t ty mb_ty + Ok ttys -> do let (c1,c23) = split c + (c2,c3) = split c23 + sz <- checkpoint + arg_tys <- mapCM (checkArg g) c1 args + let v_ttys = mapC (\c (t,ty) -> (t,eval g [] c ty [])) c2 ttys + try sz + (\(fun,fun_ty) -> reapply2 scope c3 fun fun_ty arg_tys mb_ty) + (\ttys -> fmap (\(ts,ty) -> (mkFV ts,ty)) (snd (minimum g ttys))) + v_ttys + where + checkArg g c (ImplArg arg) = do + let (c1,c2) = split c + (arg,arg_ty) <- tcRho scope c1 arg Nothing + let v = eval g (scopeEnv scope) c2 arg [] + return (ImplArg arg,v,arg_ty) + checkArg g c arg = do + let (c1,c2) = split c + (arg,arg_ty) <- tcRho scope c1 arg Nothing + let v = eval g (scopeEnv scope) c2 arg [] + return (arg,v,arg_ty) - T (TTyped arg) pts -> do - (_,val) <- checks $ map (inferCase (Just arg)) pts - checkLType gr g trm (Table arg val) - T (TComp arg) pts -> do - (_,val) <- checks $ map (inferCase (Just arg)) pts - checkLType gr g trm (Table arg val) - T ti pts -> do -- tries to guess: good in oper type inference - let pts' = [pt | pt@(p,_) <- pts, isConstPatt p] - case pts' of - [] -> checkError ("cannot infer table type of" <+> ppTerm Unqualified 0 trm) ----- PInt k : _ -> return $ Ints $ max [i | PInt i <- pts'] - _ -> do - (arg,val) <- checks $ map (inferCase Nothing) pts' - checkLType gr g trm (Table arg val) - V arg pts -> do - (_,val) <- checks $ map (inferLType gr g) pts --- return (trm, Table arg val) -- old, caused issue 68 - checkLType gr g trm (Table arg val) + mkFV [t] = t + mkFV ts = FV ts - K s -> - let trm' = case words s of - [] -> Empty - [w] -> K w - (w:ws) -> foldl (\t -> C t . K) (K w) ws - in return (trm', typeStr) + minimum g [] = (maxBound,err) + where + err = evalError (pp "Overload resolution failed") + minimum g (tty@(t,ty):ttys) = + let a = arity ty + (a',res) = minimum g ttys + in case compare a a' of + GT -> (a',res) + EQ -> (a',join t ty res) + LT -> (a ,one t ty) + where + arity :: Value -> Int + arity (VProd _ _ _ ty) = 1 + arity ty + arity _ = 0 - EInt i -> return (trm, typeInt) + one t ty = do + return ([t],ty) - EFloat i -> return (trm, typeFloat) + join t ty res = do + (ts,ty') <- res + ty <- supertype scope (Just ty) ty' + return (t:ts,ty) - Empty -> return (trm, typeStr) +reapply2 :: Scope -> Choice -> Term -> Value -> [(Term,Value,Value)] -> Maybe Rho -> EvalM (Term,Rho) +reapply2 scope c fun fun_ty [] mb_ty = do + (fun,fun_ty) <- instSigma scope c fun fun_ty mb_ty + fun <- zonkTerm (scopeVars scope) fun + return (fun,fun_ty) +reapply2 scope c fun fun_ty ((ImplArg arg,arg_v,arg_ty):args) mb_ty = do -- Implicit arg case + (bt, x, arg_ty', res_ty) <- unifyFun scope fun_ty + unless (bt == Implicit) $ + evalError (ppTerm Unqualified 0 (App fun (ImplArg arg)) <+> + "is an implicit argument application, but no implicit argument is expected") + (arg,_,_) <- subsCheckRho scope arg arg_ty' arg_ty + res_ty <- evalCodomain x arg_v res_ty + reapply2 scope c (App fun (ImplArg arg)) res_ty args mb_ty +reapply2 scope c fun fun_ty ((arg,arg_v,arg_ty):args) mb_ty = do -- Explicit arg (fallthrough) case + (fun,fun_ty) <- instantiate scope fun fun_ty + (_, x, arg_ty', res_ty) <- unifyFun scope fun_ty + (arg,_,_) <- subsCheckRho scope arg arg_ty arg_ty' + res_ty <- evalCodomain x arg_v res_ty + reapply2 scope c (App fun arg) res_ty args mb_ty - C s1 s2 -> - check2 (flip (justCheck g) typeStr) C s1 s2 typeStr +tcPatt scope c PW Nothing = do + i <- newResiduation scope + return (scope,VMeta i []) +tcPatt scope c PW (Just ty0) = + return (scope,ty0) +tcPatt scope c (PV x) Nothing = do + i <- newResiduation scope + let ty = VMeta i [] + return ((x,ty):scope,ty) +tcPatt scope c (PV x) (Just ty) = + return ((x,ty):scope,ty) +tcPatt scope c (PP q ps) mb_ty = do + g@(Gl gr _) <- globals + ty <- case lookupResType gr q of + Ok ty -> return ty + Bad msg -> evalError (pp msg) + let go scope c ty [] = return (scope,ty) + go scope c ty (p:ps) = do (_,_,arg_ty,res_ty) <- unifyFun scope ty + let (c1,c2) = split c + (scope,arg_ty) <- tcPatt scope c1 p (Just arg_ty) + go scope c2 res_ty ps + let (c1,c2) = split c + (scope,res_ty) <- go scope c1 (eval g [] c2 ty []) ps + case mb_ty of + Just ty -> unify scope ty res_ty + Nothing -> return () + return (scope,res_ty) +tcPatt scope c p@(PInt i) mb_ty = + case mb_ty of + Just ty0@(VInts n ext) + | i <= n -> return (scope,ty0) + | ext -> return (scope,VInts i ext) + | otherwise -> evalError ("Ints" <+> i <+> "is not a subtype of" <+> ppValue Unqualified 0 ty0) + Just ty0@(VMeta k vs) -> do + mv <- getMeta k + case mv of + Bound scope1 v -> do + g <- globals + (scope,ty) <- tcPatt scope c p (Just (apply g v vs)) + setMeta k (Bound scope1 ty) + return (scope,ty0) + Residuation scope1 -> do + setMeta k (Bound scope1 (VInts i True)) + return (scope,ty0) + Nothing -> return (scope,VInts i True) + _ -> evalError (pp "An integer must have an Int or Ints n type") +tcPatt scope c (PString s) mb_ty = do + case mb_ty of + Just ty -> unify scope ty vtypeStr + Nothing -> return () + return (scope,vtypeStr) +tcPatt scope c PChar mb_ty = do + case mb_ty of + Just ty -> unify scope ty vtypeStr + Nothing -> return () + return (scope,vtypeStr) +tcPatt scope c (PChars cs) mb_ty = do + case mb_ty of + Just ty -> unify scope ty vtypeStr + Nothing -> return () + return (scope,vtypeStr) +tcPatt scope c (PSeq _ _ p1 _ _ p2) mb_ty = do + case mb_ty of + Just ty -> unify scope ty vtypeStr + Nothing -> return () + let (c1,c2) = split c + (scope,_) <- tcPatt scope c1 p1 (Just vtypeStr) + (scope,_) <- tcPatt scope c2 p2 (Just vtypeStr) + return (scope,vtypeStr) +tcPatt scope c (PRep _ _ p) mb_ty = do + case mb_ty of + Just ty -> unify scope ty vtypeStr + Nothing -> return () + tcPatt scope c p (Just vtypeStr) +tcPatt scope c (PAs x p) mb_ty = do + ty <- case mb_ty of + Just ty -> return ty + Nothing -> do i <- newResiduation scope + return (VMeta i []) + tcPatt ((x,ty):scope) c p (Just ty) +tcPatt scope c p@(PR rs) mb_ty = + case mb_ty of + Just (VRecType ltys ext) -> check scope c rs ltys ext + Just ty0@(VMeta i vs) -> do + mv <- getMeta i + case mv of + Bound scope1 v -> + do g <- globals + (scope,ty) <- tcPatt scope c p (Just (apply g v vs)) + setMeta i (Bound scope1 ty) + return (scope,ty0) + Residuation scope1 -> + do (scope,ltys) <- infer scope c rs + setMeta i (Bound scope1 (VRecType ltys True)) + return (scope,ty0) + Nothing ->do (scope,ltys) <- infer scope c rs + return (scope,VRecType ltys True) + _ -> evalError (pp "An record must have an record type") + where + check scope c [] ltys ext = return (scope,VRecType ltys ext) + check scope c ((l,p):rs) ltys ext = + case lookup3 l ltys of + Just ty -> do let (c1,c2) = split c + (scope,ty) <- tcPatt scope c1 p (Just ty) + check scope c2 rs (update3 l True ty ltys) ext + Nothing + | ext -> do let (c1,c2) = split c + (scope,ty) <- tcPatt scope c1 p Nothing + check scope c2 rs (ltys++[(l,True,ty)]) ext + | otherwise + -> do ty <- value2termM False (scopeVars scope) (VRecType ltys ext) + evalError (pp "Label" <+> pp l <+> " is not defined in the type of the pattern:" $$ + nest 4 (ppTerm Unqualified 0 ty)) - Glue s1 s2 -> - check2 (flip (justCheck g) typeStr) Glue s1 s2 typeStr ---- typeTok + infer scope c [] = return (scope,[]) + infer scope c ((l,p):rs) = do + let (c1,c2) = split c + (scope,ty) <- tcPatt scope c1 p Nothing + (scope,ltys) <- infer scope c2 rs + return (scope,(l,True,ty):ltys) +tcPatt scope c (PNeg p) mb_ty = do + (_,ty) <- tcPatt scope c p mb_ty + return (scope, ty) +tcPatt scope c (PAlt p1 p2) mb_ty = do + let (c1,c2) = split c + (_,ty) <- tcPatt scope c1 p1 mb_ty + (_,ty) <- tcPatt scope c2 p2 (Just ty) + return (scope,ty) +tcPatt scope c (PM q) mb_ty = do + g@(Gl gr _) <- globals + ty <- case lookupResType gr q of + Ok ty -> return ty + Bad msg -> evalError (pp msg) + case ty of + EPattType ty + -> do let vty = eval g [] c ty [] + case mb_ty of + Just ty0 -> unify scope ty0 vty + Nothing -> return () + return (scope,vty) + ty -> evalError ("Pattern type expected but " <+> pp ty <+> " found.") +tcPatt scope c p ty = unimplemented ("tcPatt "++show p) ----- hack from Rename.identRenameTerm, to live with files with naming conflicts 18/6/2007 - Strs (Cn c : ts) | c == cConflict -> do - checkWarn ("unresolved constant, could be any of" <+> hcat (map (ppTerm Unqualified 0) ts)) - inferLType gr g (head ts) - - Strs ts -> do - ts' <- mapM (\t -> justCheck g t typeStr) ts - return (Strs ts', typeStrs) - - Alts t aa -> do - t' <- justCheck g t typeStr - aa' <- flip mapM aa (\ (c,v) -> do - c' <- justCheck g c typeStr - v' <- checks $ map (justCheck g v) [typeStrs, EPattType typeStr] - v' <- case v' of - Q q -> do t <- lookupResDef gr q - t <- normalForm (Gl gr stdPredef) t - case t of - EPatt _ _ p -> mkStrs p - _ -> return v' - _ -> return v' - return (c',v')) - return (Alts t' aa', typeStr) - - RecType r -> do - let (ls,ts) = unzip r - ts' <- mapM (flip (justCheck g) typeType) ts - return (RecType (zip ls ts'), typeType) - - ExtR r s -> do - (r',rT) <- inferLType gr g r - rT' <- computeLType gr g rT - - (s',sT) <- inferLType gr g s - sT' <- computeLType gr g sT - - let trm' = ExtR r' s' - case (rT', sT') of - (RecType rs, RecType ss) -> do - let rt = RecType ([field | field@(l,_) <- rs, notElem l (map fst ss)] ++ ss) -- select types of later fields - checkLType gr g trm' rt ---- return (trm', rt) - _ | rT' == typeType && sT' == typeType -> do - return (trm', typeType) - _ -> checkError ("records or record types expected in" <+> ppTerm Unqualified 0 trm) - - Sort _ -> - termWith trm $ return typeType - - Prod bt x a b -> do - a' <- justCheck g a typeType - b' <- justCheck ((bt,x,a'):g) b typeType - return (Prod bt x a' b', typeType) - - Table p t -> do - p' <- justCheck g p typeType --- check p partype! - t' <- justCheck g t typeType - return $ (Table p' t', typeType) - - FV vs -> do - (_,ty) <- checks $ map (inferLType gr g) vs ---- checkIfComplexVariantType trm ty - checkLType gr g trm ty - - EPattType ty -> do - ty' <- justCheck g ty typeType - return (EPattType ty',typeType) - EPatt _ _ p -> do - ty <- inferPatt p - (minp,maxp,p') <- measurePatt gr p - return (EPatt minp maxp p', EPattType ty) - - ELin c trm -> do - (trm',ty) <- inferLType gr g trm - ty' <- lockRecType c ty ---- lookup c; remove lock AR 20/6/2009 - return $ (ELin c trm', ty') - - _ -> checkError ("cannot infer lintype of" <+> ppTerm Unqualified 0 trm) - - where - isPredef m = elem m [cPredef,cPredefAbs] - - justCheck g ty te = checkLType gr g ty te >>= return . fst - - -- for record fields, which may be typed - inferM (mty, t) = do - (t', ty') <- case mty of - Just ty -> checkLType gr g t ty - _ -> inferLType gr g t - return (Just ty',t') - - inferCase mty (patt,term) = do - arg <- maybe (inferPatt patt) return mty - cont <- pattContext gr g arg patt - (term',val) <- inferLType gr (reverse cont ++ g) term - return (arg,val) - isConstPatt p = case p of - PC _ ps -> True --- all isConstPatt ps - PP _ ps -> True --- all isConstPatt ps - PR ps -> all (isConstPatt . snd) ps - PT _ p -> isConstPatt p - PString _ -> True - PInt _ -> True - PFloat _ -> True - PChar -> True - PChars _ -> True - PSeq _ _ p _ _ q -> isConstPatt p && isConstPatt q - PAlt p q -> isConstPatt p && isConstPatt q - PRep _ _ p -> isConstPatt p - PNeg p -> isConstPatt p - PAs _ p -> isConstPatt p - _ -> False - - inferPatt p = case p of - PP (q,c) ps | q /= cPredef -> liftM valTypeCnc (lookupResType gr (q,c)) - PAs _ p -> inferPatt p - PNeg p -> inferPatt p - PAlt p q -> checks [inferPatt p, inferPatt q] - PSeq _ _ _ _ _ _ -> return $ typeStr - PRep _ _ _ -> return $ typeStr - PChar -> return $ typeStr - PChars _ -> return $ typeStr - _ -> inferLType gr g (patt2term p) >>= return . snd - -measurePatt gr p = +measurePatt p = case p of - PM q -> do t <- lookupResDef gr q - t <- normalForm (Gl gr stdPredef) t - case t of - EPatt minp maxp _ -> return (minp,maxp,p) - _ -> checkError ("Expected pattern macro, but found:" $$ nest 2 (pp t)) - PR ass -> do ass <- mapM (\(lbl,p) -> measurePatt gr p >>= \(_,_,p') -> return (lbl,p')) ass + PM q -> do g <- globals + case eval g [] unit (Q q) [] of + VPatt minp maxp _ -> return (minp,maxp,p) + v -> evalError ("Expected pattern macro, but found:" $$ nest 2 (ppValue Unqualified 0 v)) + PR ass -> do ass <- mapM (\(lbl,p) -> measurePatt p >>= \(_,_,p') -> return (lbl,p')) ass return (0,Nothing,PR ass) PString s -> do let len=length s return (len,Just len,p) - PT t p -> do (min,max,p') <- measurePatt gr p + PT t p -> do (min,max,p') <- measurePatt p return (min,max,PT t p') - PAs x p -> do (min,max,p) <- measurePatt gr p + PAs x p -> do (min,max,p) <- measurePatt p case p of PW -> return (0,Nothing,PV x) _ -> return (min,max,PAs x p) - PImplArg p -> do (min,max,p') <- measurePatt gr p + PImplArg p -> do (min,max,p') <- measurePatt p return (min,max,PImplArg p') - PNeg p -> do (_,_,p') <- measurePatt gr p + PNeg p -> do (_,_,p') <- measurePatt p return (0,Nothing,PNeg p') - PAlt p1 p2 -> do (min1,max1,p1) <- measurePatt gr p1 - (min2,max2,p2) <- measurePatt gr p2 + PAlt p1 p2 -> do (min1,max1,p1) <- measurePatt p1 + (min2,max2,p2) <- measurePatt p2 case (p1,p2) of (PString [c1],PString [c2]) -> return (1,Just 1,PChars [c1,c2]) (PString [c], PChars cs) -> return (1,Just 1,PChars ([c]++cs)) @@ -343,13 +850,13 @@ measurePatt gr p = (PChars cs1, PChars cs2) -> return (1,Just 1,PChars (cs1++cs2)) _ -> return (min min1 min2,liftM2 max max1 max2,PAlt p1 p2) PSeq _ _ p1 _ _ p2 - -> do (min1,max1,p1) <- measurePatt gr p1 - (min2,max2,p2) <- measurePatt gr p2 + -> do (min1,max1,p1) <- measurePatt p1 + (min2,max2,p2) <- measurePatt p2 case (p1,p2) of (PW, PW ) -> return (0,Nothing,PW) (PString s1,PString s2) -> return (min1+min2,liftM2 (+) max1 max2,PString (s1++s2)) _ -> return (min1+min2,liftM2 (+) max1 max2,PSeq min1 max1 p1 min2 max2 p2) - PRep _ _ p -> do (minp,maxp,p) <- measurePatt gr p + PRep _ _ p -> do (minp,maxp,p) <- measurePatt p case p of PW -> return (0,Nothing,PW) PChar -> return (0,Nothing,PW) @@ -358,486 +865,746 @@ measurePatt gr p = PChars _ -> return (1,Just 1,p) _ -> return (0,Nothing,p) --- type inference: Nothing, type checking: Just t --- the latter permits matching with value type -getOverload :: SourceGrammar -> Context -> Maybe Type -> Term -> Check (Maybe (Term,Type)) -getOverload gr g mt ot = case appForm ot of - (f@(Q c), ts) -> case lookupOverload gr c of - Ok typs -> do - ttys <- mapM (inferLType gr g) ts - v <- matchOverload f typs ttys - return $ Just v - _ -> return Nothing - (AdHocOverload cs@(f:_), ts) -> do --- the function name f is only used in error messages - let typs = concatMap collectOverloads cs - ttys <- mapM (inferLType gr g) ts - v <- matchOverload f typs ttys - return $ Just v - _ -> return Nothing +inferRecFields scope c ls [] = return [] +inferRecFields scope c ls ((l,t):lts) + | elem l ls = evalError ("Repeated definition for field" <+> l) + | otherwise = do + let (c1,c2) = split c + lt <- tcRecField scope c1 l t Nothing + lts <- inferRecFields scope c2 (l:ls) lts + return (lt:lts) - where - collectOverloads tr@(Q c) = case lookupOverload gr c of - Ok typs -> typs - _ -> case lookupResType gr c of - Ok ty -> let (args,val) = typeFormCnc ty in [(map (\(b,x,t) -> t) args,(val,tr))] - _ -> [] - collectOverloads _ = [] --- constructors QC - - matchOverload f typs ttys = do - let (tts,tys) = unzip ttys - let vfs = lookupOverloadInstance tys typs - let matches = [vf | vf@((_,v,_),_) <- vfs, matchVal mt v] - let showTypes ty = hsep (map ppType ty) - - - let (stys,styps) = (showTypes tys, [showTypes ty | (ty,_) <- typs]) - - -- to avoid strange error msg e.g. in case of unmatch record extension, show whole types if needed AR 28/1/2013 - let (stysError,stypsError) = if elem (render stys) (map render styps) - then (hsep (map (ppTerm Unqualified 0) tys), [hsep (map (ppTerm Unqualified 0) ty) | (ty,_) <- typs]) - else (stys,styps) - - case ([vf | (vf,True) <- matches],[vf | (vf,False) <- matches]) of - ([(_,val,fun)],_) -> return (mkApp fun tts, val) - ([],[(pre,val,fun)]) -> do - checkWarn $ "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot $$ - "for" $$ - nest 2 (showTypes tys) $$ - "using" $$ - nest 2 (showTypes pre) - return (mkApp fun tts, val) - ([],[]) -> do - checkError $ "no overload instance of" <+> ppTerm Qualified 0 f $$ - maybe empty (\x -> "with value type" <+> ppType x) mt $$ - "for argument list" $$ - nest 2 stysError $$ - "among alternatives" $$ - nest 2 (vcat stypsError) - - - (vfs1,vfs2) -> case (noProds vfs1,noProds vfs2) of - ([(val,fun)],_) -> do - return (mkApp fun tts, val) - ([],[(val,fun)]) -> do - checkWarn ("ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot) - return (mkApp fun tts, val) - ------ unsafely exclude irritating warning AR 24/5/2008 ------ checkWarn $ "overloading of" +++ prt f +++ ------ "resolved by excluding partial applications:" ++++ ------ unlines [prtType env ty | (ty,_) <- vfs', not (noProd ty)] - ---- now forgiving ambiguity with a warning AR 1/2/2014 --- This gives ad hoc overloading the same behaviour as the choice of the first match in renaming did before. --- But it also gives a chance to ambiguous overloadings that were banned before. - (nps1,nps2) -> do - checkWarn $ "ambiguous overloading of" <+> ppTerm Unqualified 0 f <+> - ---- "with argument types" <+> hsep (map (ppTerm Qualified 0) tys) $$ - "resolved by selecting the first of the alternatives" $$ - nest 2 (vcat [ppTerm Qualified 0 fun | (_,ty,fun) <- vfs1 ++ if null vfs1 then vfs2 else []]) - case [(mkApp fun tts,val) | (val,fun) <- nps1 ++ nps2] of - [] -> checkError $ "no alternatives left when resolving" <+> ppTerm Unqualified 0 f - h:_ -> return h - - matchVal mt v = elem mt [Nothing,Just v,Just (unlocked v)] - - unlocked v = case v of - RecType fs -> RecType $ filter (not . isLockLabel . fst) (sortRec fs) - _ -> v - ---- TODO: accept subtypes - ---- TODO: use a trie - lookupOverloadInstance tys typs = - [((pre,mkFunType rest val, t),isExact) | - let lt = length tys, - (ty,(val,t)) <- typs, length ty >= lt, - let (pre,rest) = splitAt lt ty, - let isExact = pre == tys, - isExact || map unlocked pre == map unlocked tys - ] - - noProds vfs = [(v,f) | (_,v,f) <- vfs, noProd v] - - noProd ty = case ty of - Prod _ _ _ _ -> False - _ -> True - -checkLType :: SourceGrammar -> Context -> Term -> Type -> Check (Term, Type) -checkLType gr g trm typ0 = do - typ <- computeLType gr g typ0 - - case trm of - - Abs bt x c -> do - case typ of - Prod bt' z a b -> do - (c',b') <- if z == identW - then checkLType gr ((bt,x,a):g) c b - else do b' <- checkIn (pp "abs") $ substituteLType [(bt',z,Vr x)] b - checkLType gr ((bt,x,a):g) c b' - return $ (Abs bt x c', Prod bt' z a b') - _ -> checkError $ "function type expected instead of" <+> ppType typ $$ - "\n ** Double-check that the type signature of the operation" $$ - "matches the number of arguments given to it.\n" - - App f a -> do - over <- getOverload gr g (Just typ) trm - case over of - Just trty -> return trty - _ -> do - (trm',ty') <- inferLType gr g trm - termWith trm' $ checkEqLType gr g typ ty' trm' - - AdHocOverload ts -> do - over <- getOverload gr g Nothing trm - case over of - Just trty -> return trty - _ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 trm) - - Q _ -> do - over <- getOverload gr g (Just typ) trm - case over of - Just trty -> return trty - _ -> do - (trm',ty') <- inferLType gr g trm - termWith trm' $ checkEqLType gr g typ ty' trm' - - T _ [] -> - checkError ("found empty table in type" <+> ppTerm Unqualified 0 typ) - T _ cs -> case typ of - Table arg val -> do - case allParamValues gr arg of - Ok vs -> do - let ps0 = map fst cs - ps <- testOvershadow ps0 vs - if null ps - then return () - else checkWarn ("patterns never reached:" $$ - nest 2 (vcat (map (ppPatt Unqualified 0) ps))) - _ -> return () -- happens with variable types - cs' <- mapM (checkCase arg val) cs - return (T (TTyped arg) cs', typ) - _ -> checkError $ "table type expected for table instead of" $$ nest 2 (ppType typ) - V arg0 vs -> - case typ of - Table arg1 val -> - do arg' <- checkEqLType gr g arg0 arg1 trm - vs1 <- allParamValues gr arg1 - if length vs1 == length vs - then return () - else checkError $ "wrong number of values in table" <+> ppTerm Unqualified 0 trm - vs' <- map fst `fmap` sequence [checkLType gr g v val|v<-vs] - return (V arg' vs',typ) - - R r -> case typ of --- why needed? because inference may be too difficult - RecType rr -> do - --let (ls,_) = unzip rr -- labels of expected type - fsts <- mapM (checkM r) rr -- check that they are found in the record - return $ (R fsts, typ) -- normalize record - - _ -> checkError ("record type expected in type checking instead of" $$ nest 2 (ppTerm Unqualified 0 typ)) - - ExtR r s -> case typ of - _ | typ == typeType -> do - trm' <- computeLType gr g trm - case trm' of - RecType _ -> termWith trm' $ return typeType - ExtR (Vr _) (RecType _) -> termWith trm' $ return typeType - -- ext t = t ** ... - _ -> checkError ("invalid record type extension" <+> nest 2 (ppTerm Unqualified 0 trm)) - - RecType rr -> do - - (fields1,fields2) <- case s of - R ss -> return (partition (\(l,_) -> isNothing (lookup l ss)) rr) - _ -> do - (s',typ2) <- inferLType gr g s - case typ2 of - RecType ss -> return (partition (\(l,_) -> isNothing (lookup l ss)) rr) - _ -> checkError ("cannot get labels from" $$ nest 2 (ppTerm Unqualified 0 typ2)) - - (r',_) <- checkLType gr g r (RecType fields1) - (s',_) <- checkLType gr g s (RecType fields2) - - let withProjection t fields g f = - case t of - R rs -> f g (\l -> case lookup l rs of - Just (_,t) -> t - Nothing -> error (render ("no value for label" <+> l))) - QC _ -> f g (\l -> P t l) - Vr _ -> f g (\l -> P t l) - _ -> if length fields == 1 - then f g (\l -> P t l) - else let x = mkFreshVar (map (\(_,x,_) -> x) g) (identS "x") - in Let (x, (Nothing, t)) (f ((Explicit,x,RecType fields):g) (\l -> P (Vr x) l)) - - rec = withProjection r' fields1 g $ \g p_r' -> - withProjection s' fields2 g $ \g p_s' -> - R ([(l,(Nothing,p_r' l)) | (l,_) <- fields1] ++ [(l,(Nothing,p_s' l)) | (l,_) <- fields2]) - return (rec, typ) - - ExtR ty ex -> do - r' <- justCheck g r ty - s' <- justCheck g s ex - return $ (ExtR r' s', typ) --- is this all? it assumes the same division in trm and typ - - _ -> checkError ("record extension not meaningful for" <+> ppTerm Unqualified 0 typ) - - FV vs -> do - ttys <- mapM (flip (checkLType gr g) typ) vs ---- checkIfComplexVariantType trm typ - return (FV (map fst ttys), typ) --- typ' ? - - S tab arg -> checks [ do - (tab',ty) <- inferLType gr g tab - ty' <- computeLType gr g ty - case ty' of - Table p t -> do - (arg',val) <- checkLType gr g arg p - checkEqLType gr g typ t trm - return (S tab' arg', t) - _ -> checkError ("table type expected for applied table instead of" <+> ppType ty') - , do - (arg',ty) <- inferLType gr g arg - ty' <- computeLType gr g ty - (tab',_) <- checkLType gr g tab (Table ty' typ) - return (S tab' arg', typ) - ] - Let (x,(mty,def)) body -> case mty of - Just ty -> do - (ty0,_) <- checkLType gr g ty typeType - (def',ty') <- checkLType gr g def ty0 - body' <- justCheck ((Explicit,x,ty'):g) body typ - return (Let (x,(Just ty',def')) body', typ) - _ -> do - (def',ty) <- inferLType gr g def -- tries to infer type of local constant - checkLType gr g (Let (x,(Just ty,def')) body) typ - - ELin c tr -> do - tr1 <- unlockRecord c tr - checkLType gr g tr1 typ - - _ -> do - (trm',ty') <- inferLType gr g trm - termWith trm' $ checkEqLType gr g typ ty' trm' - where - justCheck g ty te = checkLType gr g ty te >>= return . fst -{- - recParts rr t = (RecType rr1,RecType rr2) where - (rr1,rr2) = partition (flip elem (map fst t) . fst) rr --} - checkM rms (l,ty) = case lookup l rms of - Just (Just ty0,t) -> do - checkEqLType gr g ty ty0 t - (t',ty') <- checkLType gr g t ty - return (l,(Just ty',t')) - Just (_,t) -> do - (t',ty') <- checkLType gr g t ty - return (l,(Just ty',t')) - _ -> checkError $ - if isLockLabel l - then let cat = drop 5 (showIdent (label2ident l)) - in ppTerm Unqualified 0 (R rms) <+> "is not in the lincat of" <+> cat <> - "; try wrapping it with lin" <+> cat - else "cannot find value for label" <+> l <+> "in" <+> ppTerm Unqualified 0 (R rms) - - checkCase arg val (p,t) = do - cont <- pattContext gr g arg p - t' <- justCheck (reverse cont ++ g) t val - (_,_,p') <- measurePatt gr p - return (p',t') - -pattContext :: SourceGrammar -> Context -> Type -> Patt -> Check Context -pattContext env g typ p = case p of - PV x -> return [(Explicit,x,typ)] - PP (q,c) ps | q /= cPredef -> do ---- why this /=? AR 6/1/2006 - t <- lookupResType env (q,c) - let (cont,v) = typeFormCnc t - checkCond ("wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p) - (length cont == length ps) - checkEqLType env g typ v (patt2term p) - mapM (\((_,_,ty),p) -> pattContext env g ty p) (zip cont ps) >>= return . concat - PR r -> do - typ' <- computeLType env g typ - case typ' of - RecType t -> do - let pts = [(ty,tr) | (l,tr) <- r, Just ty <- [lookup l t]] - ----- checkWarn $ prt p ++++ show pts ----- debug - mapM (uncurry (pattContext env g)) pts >>= return . concat - _ -> checkError ("record type expected for pattern instead of" <+> ppTerm Unqualified 0 typ') - PT t p' -> do - checkEqLType env g typ t (patt2term p') - pattContext env g typ p' - - PAs x p -> do - g' <- pattContext env g typ p - return ((Explicit,x,typ):g') - - PAlt p' q -> do - g1 <- pattContext env g typ p' - g2 <- pattContext env g typ q - let pts = nub ([x | pt@(_,x,_) <- g1, notElem pt g2] ++ [x | pt@(_,x,_) <- g2, notElem pt g1]) - checkCond - ("incompatible bindings of" <+> - fsep pts <+> - "in pattern alterantives" <+> ppPatt Unqualified 0 p) (null pts) - return g1 -- must be g1 == g2 - PSeq _ _ p _ _ q -> do - g1 <- pattContext env g typ p - g2 <- pattContext env g typ q - return $ g1 ++ g2 - PRep _ _ p' -> noBind typeStr p' - PNeg p' -> noBind typ p' - - _ -> return [] ---- check types! - where - noBind typ p' = do - co <- pattContext env g typ p' - if not (null co) - then checkWarn ("no variable bound inside pattern" <+> ppPatt Unqualified 0 p) - >> return [] - else return [] - -checkEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check Type -checkEqLType gr g t u trm = do - (b,t',u',s) <- checkIfEqLType gr g t u trm - case b of - True -> return t' - False -> - let inferredType = ppTerm Qualified 0 u - expectedType = ppTerm Qualified 0 t - term = ppTerm Unqualified 0 trm - funName = pp . head . words .render $ term - helpfulMsg = - case (arrows inferredType, arrows expectedType) of - (0,0) -> pp "" -- None of the types is a function - _ -> "\n **" <+> - if expectedType `isLessApplied` inferredType - then "Maybe you gave too few arguments to" <+> funName - else pp "Double-check that type signature and number of arguments match." - in checkError $ s <+> "type of" <+> term $$ - "expected:" <+> expectedType $$ -- ppqType t u $$ - "inferred:" <+> inferredType $$ -- ppqType u t - helpfulMsg +checkRecFields scope c ls [] ltys + | null ltys = return [] + | otherwise = evalError ("Missing fields:" <+> hsep [l | (l,_,_) <- ltys]) +checkRecFields scope c ls ((l,t):lts) ltys + | elem l ls = evalError ("Repeated definition for field" <+> l) + | otherwise = + case takeIt l ltys of + (Just ty,ltys) -> do let (c1,c2) = split c + ltty <- tcRecField scope c1 l t (Just ty) + lttys <- checkRecFields scope c2 ls lts ltys + return (ltty : lttys) + (Nothing,ltys) -> do evalWarn ("Discarded field:" <+> l) + lttys <- checkRecFields scope c ls lts ltys + return lttys -- ignore the field where - -- count the number of arrows in the prettyprinted term - arrows :: Doc -> Int - arrows = length . filter (=="->") . words . render + takeIt l1 [] = (Nothing, []) + takeIt l1 (lty@(l2,_,ty):ltys) + | l1 == l2 = (Just ty,ltys) + | otherwise = let (mb_ty,ltys') = takeIt l1 ltys + in (mb_ty,lty:ltys') - -- If prettyprinted type t has fewer arrows then prettyprinted type u, - -- then t is "less applied", and we can print out more helpful error msg. - isLessApplied :: Doc -> Doc -> Bool - isLessApplied t u = arrows t < arrows u +tcRecField scope c l (mb_ann_ty,t) mb_ty = do + (t,ty) <- case mb_ann_ty of + Just ann_ty -> do let (c1,c2,c3,c4) = split4 c + (ann_ty, _) <- tcRho scope c1 ann_ty (Just vtypeType) + g <- globals + let v_ann_ty = eval g (scopeEnv scope) c2 ann_ty [] + (t,_) <- tcRho scope c3 t (Just v_ann_ty) + instSigma scope c4 t v_ann_ty mb_ty + Nothing -> tcRho scope c t mb_ty + return (l,t,ty) -checkIfEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check (Bool,Type,Type,String) -checkIfEqLType gr g t u trm = do - t' <- computeLType gr g t - u' <- computeLType gr g u - case t' == u' || alpha [] t' u' of - True -> return (True,t',u',[]) - -- forgive missing lock fields by only generating a warning. - --- better: use a flag to forgive? (AR 31/1/2006) - _ -> case missingLock [] t' u' of - Ok lo -> do - checkWarn $ "missing lock field" <+> fsep lo - return (True,t',u',[]) - Bad s -> return (False,t',u',s) +tcRecTypeFields scope c ls [] mb_ty = return ([],mb_ty) +tcRecTypeFields scope c ls ((l,ty):rs) mb_ty + | elem l ls = evalError ("Repeated definition for field" <+> l) + | otherwise = do + let (c1,c2) = split c + (ty,sort) <- tcRho scope c1 ty mb_ty + mb_ty <- case sort of + VSort s + | s == cType -> return (Just sort) + | s == cPType -> return mb_ty + VMeta _ _ -> return mb_ty + _ -> do sort <- value2termM False (scopeVars scope) sort + evalError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$ + "cannot be of type" <+> ppTerm Unqualified 0 sort) + (rs,mb_ty) <- tcRecTypeFields scope c2 (l:ls) rs mb_ty + return ((l,ty):rs,mb_ty) +-- | Invariant: if the third argument is (Just rho), +-- then rho is in weak-prenex form +instSigma :: Scope -> Choice -> Term -> Sigma -> Maybe Rho -> EvalM (Term, Rho) +instSigma scope s t ty1 Nothing = return (t,ty1) -- INST1 +instSigma scope s t ty1 (Just ty2) = do -- INST2 + (t,ty1,ty2) <- subsCheckRho scope t ty1 ty2 + return (t,ty2) + +-- | Invariant: the second argument is in weak-prenex form +subsCheckRho :: Scope -> Term -> Sigma -> Rho -> EvalM (Term,Sigma,Rho) +subsCheckRho scope t ty1@(VApp _ p1 []) ty2 -- for backwards compatibility + | p1 == (cPredef,cErrorType) = return (t,ty1,ty2) +subsCheckRho scope t ty1 ty2@(VApp _ p2 []) -- for backwards compatibility + | p2 == (cPredef,cErrorType) = return (t,ty1,ty2) +subsCheckRho scope t ty1@(VMeta i vs1) ty2@(VMeta j vs2) + | i == j = do sequence_ (zipWith (unify scope) vs1 vs2) + return (t,ty1,ty2) + | otherwise = do + mv <- getMeta i + case mv of + Bound _ v1 -> do + g <- globals + subsCheckRho scope t (apply g v1 vs1) (VMeta j vs2) + Residuation scope1 -> do + mv <- getMeta j + case mv of + Bound _ v2 -> do + g <- globals + subsCheckRho scope t (VMeta i vs1) (apply g v2 vs2) + Residuation scope2 + | m > n -> do setMeta i (Bound scope1 (VMeta j vs2)) + return (t,VMeta j vs2,VMeta j vs2) + | otherwise -> do setMeta j (Bound scope2 (VMeta i vs1)) + return (t,VMeta i vs1,VMeta j vs1) + where + m = length scope1 + n = length scope2 +subsCheckRho scope t ty1@(VMeta i vs) ty2 = do + mv <- getMeta i + case mv of + Bound scope' ty1 -> do + g <- globals + (t,ty1,ty2) <- subsCheckRho scope t (apply g ty1 vs) ty2 + setMeta i (Bound scope' ty1) + return (t,ty1,ty2) + Residuation scope' -> do + occursCheck scope' i scope ty2 + ty1 <- subtype scope Nothing ty2 + setMeta i (Bound scope' ty1) + return (t,ty1,ty2) +subsCheckRho scope t ty1 ty2@(VMeta i vs) = do + mv <- getMeta i + case mv of + Bound scope' ty2 -> do + g <- globals + (t,ty1,ty2) <- subsCheckRho scope t ty1 (apply g ty2 vs) + setMeta i (Bound scope' ty2) + return (t,ty1,ty2) + Residuation scope' -> do + occursCheck scope' i scope ty1 + ty2 <- supertype scope Nothing ty1 + setMeta i (Bound scope' ty2) + return (t,ty1,ty2) +subsCheckRho scope t (VProd Implicit x ty1 ty2) rho2 = do -- Rule SPEC + i <- newResiduation scope + g <- globals + let ty2' = case ty2 of + VClosure env c ty2 -> eval g ((x,VMeta i []):env) c ty2 [] + ty2 -> ty2 + subsCheckRho scope (App t (ImplArg (Meta i))) ty2' rho2 +subsCheckRho scope t rho1 (VProd Implicit x ty1 ty2) = do -- Rule SKOL + let v = newVar scope + ty2 <- evalCodomain x (VGen (length scope) []) ty2 + (t,ty1,ty2) <- subsCheckRho ((v,ty1):scope) t rho1 ty2 + return (Abs Implicit v t,ty1,ty2) +subsCheckRho scope t rho1 (VProd Explicit _ a2 r2) = do -- Rule FUN + (_,_,a1,r1) <- unifyFun scope rho1 + subsCheckFun scope t a1 r1 a2 r2 +subsCheckRho scope t (VProd Explicit _ a1 r1) rho2 = do -- Rule FUN + (_,_,a2,r2) <- unifyFun scope rho2 + subsCheckFun scope t a1 r1 a2 r2 +subsCheckRho scope t rho1 (VTable p2 r2) = do -- Rule TABLE + (p1,r1) <- unifyTbl scope rho1 + subsCheckTbl scope t p1 r1 p2 r2 +subsCheckRho scope t (VTable p1 r1) rho2 = do -- Rule TABLE + (p2,r2) <- unifyTbl scope rho2 + subsCheckTbl scope t p1 r1 p2 r2 +subsCheckRho scope t ty1@(VSort s1) ty2@(VSort s2) -- Rule PTYPE + | 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. + | p == (cPredef,cInt) = return (t,ty1,ty2) -- Should be only a temporary hack. +subsCheckRho scope t ty1@(VInts _ _) ty2@(VApp _ p _) -- Rule INT1 + | p == (cPredef,cInt) = return (t,ty1,ty2) +subsCheckRho scope t ty1@(VInts n1 ext1) ty2@(VInts n2 ext2) -- Rule INT2 + | n1 <= n2 = return (t,ty1,ty2) + | ext2 = return (t,ty1,VInts n1 ext2) + | otherwise = evalError ("In the term" <+> ppTerm Unqualified 0 t $$ + ppValue Terse 0 ty1 <+> "is not a subtype of" <+> ppValue Terse 0 ty2) +subsCheckRho scope t ty1@(VRecType rs1 ext1) ty2@(VRecType rs2 ext2) = do -- Rule REC + let mkAccess scope t = + case t of + ExtR t1 (R rs) -> + do (scope,mkProj1,mkWrap1) <- mkAccess scope t1 + sequence_ [evalWarn ("Discarded field:" <+> l) | (l,_) <- rs, isNothing (lookup3 l rs2)] + return (scope + ,\l -> lookup l rs `mplus` mkProj1 l + ,mkWrap1 + ) + R rs -> do sequence_ [evalWarn ("Discarded field:" <+> l) | (l,_) <- rs, isNothing (lookup3 l rs2)] + return (scope + ,\l -> lookup l rs + ,id + ) + Vr x -> return (scope + ,\l -> return (Nothing,P t l) + ,\t' -> if is_trivial x t' then t else t' + ) + t -> let x = newVar scope + in return (((x,ty1):scope) + ,\l -> return (Nothing,P (Vr x) l) + ,\t' -> if is_trivial x t' then t else Let (x, (Nothing, t)) t' + ) + + is_trivial x (R rs) = all is_selection rs + where + is_selection (l, (_, P (Vr u) l')) + | l == l' && u == x = True + is_selection _ = False + is_trivial x _ = False + + mkField scope l (mb_ty,t) (Just ty1) ty2 = do + (t,ty1,ty2) <- subsCheckRho scope t ty1 ty2 + return ((l, (mb_ty,t)), (l, True, ty1)) + mkField scope l (mb_ty,t) Nothing ty2 + | isLockLabel l = return ((l, (Just (RecType []),R [])), (l, True, ty2)) + | otherwise = return ((l, (mb_ty,t)), (l, True, ty2)) + + (scope,mkProj,wrap) <- mkAccess scope t + + let fields = [(l,o2,ty2,lookup3 l rs1) | (l,o2,ty2) <- rs2] + case [l | (l,_,_,Nothing) <- fields, not ext1 && not (isLockLabel l)] of + [] -> return () + missing -> evalError ("In the term" <+> pp t $$ + "there are no values for fields:" <+> hsep missing) + rs <- sequence [mkField scope l t mb_ty1 ty2 | (l,_,ty2,mb_ty1) <- fields, Just t <- [mkProj l]] + return (wrap (R (map fst rs)),VRecType (foldl (\rs (_,(l,o,ty)) -> update3 l o ty rs) rs1 rs) ext2,ty2) +subsCheckRho scope t ty1 (VFV c (VarFree vs)) = do + ty2 <- variants c vs + subsCheckRho scope t ty1 ty2 +subsCheckRho scope t (VFV c (VarFree vs)) ty2 = do + ty1 <- variants c vs + subsCheckRho scope t ty1 ty2 +subsCheckRho scope t ty1@(VPattType (VSort s1)) ty2@(VSort s2) -- for backwards compatibility + | s1 == cStr && s2 == cStrs = return (t,ty1,ty2) +subsCheckRho scope t ty1 ty2 = do -- Rule EQ + unify scope ty1 ty2 -- Revert to ordinary unification + return (t,ty1,ty2) + +subsCheckFun :: Scope -> Term -> Sigma -> Value -> Sigma -> Value -> EvalM (Term,Value,Value) +subsCheckFun scope t a1 r1 a2 r2 = do + let x = newVar scope + (xt,a2,a1) <- subsCheckRho ((x,a2):scope) (Vr x) a2 a1 + g <- globals + let (x1',r1') = case r1 of + VClosure env c r1 -> (x,eval g ((x,(VGen (length scope) [])):env) c r1 []) + r1 -> (identW,r1) + (x2',r2') = case r2 of + VClosure env c r2 -> (x,eval g ((x,(VGen (length scope) [])):env) c r2 []) + r2 -> (identW,r2) + (t,r1,r2) <- subsCheckRho ((x,a2):scope) (App t xt) r1' r2' + case t of + App t (Vr u) | u == x -> return (t, VProd Explicit x1' a1 r1, VProd Explicit x2' a2 r2) + _ -> return (Abs Explicit x t, VProd Explicit x1' a1 r1, VProd Explicit x2' a2 r2) + +subsCheckTbl :: Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> EvalM (Term,Value,Value) +subsCheckTbl scope t p1 r1 p2 r2 = do + (scope,y,sel,wrap) <- + case t of + Vr x -> let y = newVar scope + in return ((y,p2):scope + ,y + ,\t -> S (Vr x) t + ,\p2 t' -> case t' of + S (Vr u) (Vr v) | u == x && v == y -> t + _ -> T (TTyped p2) [(PV y,t')] + ) + T _ [(PV x,t')] -> + let scope' = (x,p1):scope + y = newVar scope' + in return (((y,p2):scope') + ,y + ,\t -> Let (x, (Nothing, t)) t' + ,\p2 t -> case t of + Let (u, (Nothing, Vr v)) t | u == x && v == y -> T (TTyped p2) [(PV x,t)] + _ -> T (TTyped p2) [(PV y,t)] + ) + t -> let x = newVar scope + scope' = (x,VTable p1 r1):scope + y = newVar scope' + in return (((y,VTable p1 r1):scope') + ,y + ,\t -> S (Vr x) t + ,\p2 t' -> case t' of + S (Vr u) (Vr v) | u == x && v == y -> t + _ -> Let (x, (Nothing, t)) (T (TTyped p2) [(PV y,t')]) + ) + (yt,p2,p1) <- subsCheckRho scope (Vr y) p2 p1 + (t,r1,r2) <- subsCheckRho scope (sel yt) r1 r2 + p2_t <- value2termM True (scopeVars scope) p2 + return (wrap p2_t t,VTable p1 r1,VTable p2 r2) + + +subtype scope Nothing (VInts i2 _) = + return (VInts i2 True) +subtype scope (Just (VInts n1 _)) (VInts n2 _) = + return (VInts (min n1 n2) False) +subtype scope Nothing (VRecType ltys ext) = do + lctrs <- mapM (\(l,o,ty) -> subtype scope Nothing ty >>= \ctr -> return (l,o,ctr)) ltys + return (VRecType lctrs ext) +subtype scope (Just (VRecType lctrs1 ext1)) (VRecType lctrs2 ext2) = do + lctrs <- foldM (\lctrs (l,o,ctr) -> union l o ctr lctrs) lctrs1 lctrs2 + return (VRecType lctrs (ext1 || ext2)) where + union l o1 ctr1 [] = do ctr <- subtype scope Nothing ctr1 + return [(l,True,ctr)] + union l o1 ctr1 ((l',o2,ctr2):lctrs) + | l == l' = do ctr <- subtype scope (Just ctr1) ctr2 + return ((l,o1||o2,ctr):lctrs) + | otherwise = do lctrs <- union l o1 ctr1 lctrs + return ((l',o2,ctr2):lctrs) +subtype scope (Just (VTable a1 r1)) (VTable a2 r2) = do + a <- supertype scope (Just a1) a2 + r <- subtype scope (Just r1) r2 + return (VTable a r) +subtype scope (Just (VProd Explicit x a1 r1)) (VProd Explicit y a2 r2) + | x == identW && y == identW = do + a <- supertype scope (Just a1) a2 + r <- subtype scope (Just r1) r2 + return (VProd Explicit identW a r) +subtype scope (Just (VApp _ p1 [])) ty2 -- for backwards compatibility + | p1 == (cPredef,cErrorType) = return ty2 +subtype scope (Just ty1) (VApp _ p2 []) -- for backwards compatibility + | p2 == (cPredef,cErrorType) = return ty1 +subtype scope Nothing ty = return ty +subtype scope (Just ctr) ty = do + unify scope ctr ty + return ty - -- check that u is a subtype of t - --- quick hack version of TC.eqVal - alpha g t u = case (t,u) of +supertype scope Nothing (VInts n2 _) = + return (VInts n2 True) +supertype scope (Just (VInts n1 _)) (VInts n2 _) = + return (VInts (max n1 n2) True) +supertype scope Nothing (VRecType ltys ext) = do + lctrs <- mapM (\(l,o,ty) -> supertype scope Nothing ty >>= \ctr -> return (l,False,ctr)) ltys + return (VRecType lctrs ext) +supertype scope (Just (VRecType lctrs1 ext1)) (VRecType lctrs2 ext2) = do + lctrs <- foldM (\lctrs (l,o,ctr) -> intersect l o ctr lctrs lctrs2) [] lctrs1 + return (VRecType lctrs (ext1 || ext2)) + where + intersect l o1 ctr1 lctrs [] = return lctrs + intersect l o1 ctr1 lctrs ((l',o2,ctr2):lctrs2) + | l == l' = do ctr <- supertype scope (Just ctr1) ctr2 + return ((l,o1 && o2,ctr):lctrs) + | otherwise = do intersect l o1 ctr1 lctrs lctrs2 +supertype scope (Just (VTable a1 r1)) (VTable a2 r2) = do + a <- subtype scope (Just a1) a2 + r <- supertype scope (Just r1) r2 + return (VTable a r) +supertype scope (Just (VProd Explicit x a1 r1)) (VProd Explicit y a2 r2) + | x == identW && y == identW = do + a <- subtype scope (Just a1) a2 + r <- supertype scope (Just r1) r2 + return (VProd Explicit identW a r) +supertype scope (Just (VApp _ p1 [])) ty2 -- for backwards compatibility + | p1 == (cPredef,cErrorType) = return ty2 +supertype scope (Just ty1) (VApp _ p2 []) -- for backwards compatibility + | p2 == (cPredef,cErrorType) = return ty1 +supertype scope Nothing ty = return ty +supertype scope (Just ctr) ty = do + unify scope ctr ty + return ty - -- error (the empty type!) is subtype of any other type - (_,u) | u == typeError -> True +----------------------------------------------------------------------- +-- Unification +----------------------------------------------------------------------- - -- contravariance - (Prod _ x a b, Prod _ y c d) -> alpha g c a && alpha ((x,y):g) b d +unifyFun :: Scope -> Rho -> EvalM (BindType, Ident, Sigma, Rho) +unifyFun scope (VProd bt x arg res) = + return (bt,x,arg,res) +unifyFun scope (VFV c (VarFree vs)) = do + res <- mapM (unifyFun scope) vs + return + ( Explicit + , identW + , VFV c (VarFree [sigma | (_,_,sigma,rho) <- res]) + , VFV c (VarFree [rho | (_,_,sigma,rho) <- res]) + ) +unifyFun scope tau = do + let mk_val i = VMeta i [] + arg <- fmap mk_val $ newResiduation scope + res <- fmap mk_val $ newResiduation scope + let bt = Explicit + unify scope tau (VProd bt identW arg res) + return (bt,identW,arg,res) - -- record subtyping - (RecType rs, RecType ts) -> all (\ (l,a) -> - any (\ (k,b) -> l == k && alpha g a b) ts) rs - (ExtR r s, ExtR r' s') -> alpha g r r' && alpha g s s' - (ExtR r s, t) -> alpha g r t || alpha g s t +unifyTbl :: Scope -> Rho -> EvalM (Sigma, Rho) +unifyTbl scope (VTable arg res) = + return (arg,res) +unifyTbl scope tau = do + let mk_val i = VMeta i [] + arg <- fmap mk_val $ newResiduation scope + res <- fmap mk_val $ newResiduation scope + unify scope tau (VTable arg res) + return (arg,res) - -- the following say that Ints n is a subset of Int and of Ints m >= n - -- But why does it also allow Int as a subtype of Ints m? /TH 2014-04-04 - (t,u) | Just m <- isTypeInts t, Just n <- isTypeInts u -> m >= n - | Just _ <- isTypeInts t, u == typeInt -> True ---- check size! - | t == typeInt, Just _ <- isTypeInts u -> True ---- why this ???? AR 11/12/2005 +unify scope (VApp c1 f1 vs1) (VApp c2 f2 vs2) + | f1 == f2 = sequence_ (zipWith (unify scope) vs1 vs2) +unify scope (VMeta i vs1) (VMeta j vs2) + | i == j = sequence_ (zipWith (unify scope) vs1 vs2) + | otherwise = do + mv <- getMeta i + case mv of + Bound _ v1 -> do + g <- globals + unify scope (apply g v1 vs1) (VMeta j vs2) + Residuation scope1 -> do + mv <- getMeta j + case mv of + Bound _ v2 -> do + g <- globals + unify scope (VMeta i vs1) (apply g v2 vs2) + Residuation scope2 + | m > n -> setMeta i (Bound scope1 (VMeta j vs2)) + | otherwise -> setMeta j (Bound scope2 (VMeta i vs2)) + where + m = length scope1 + n = length scope2 +unify scope (VMeta i vs) v = unifyVar scope i vs v +unify scope v (VMeta i vs) = unifyVar scope i vs v +unify scope (VGen i vs1) (VGen j vs2) + | i == j = sequence_ (zipWith (unify scope) vs1 vs2) +unify scope (VProd b x d cod) (VProd b' x' d' cod') + | b == b' = do + unify scope d d' + cod <- evalCodomain x (VGen (length scope) []) cod + cod' <- evalCodomain x' (VGen (length scope) []) cod' + unify scope cod cod' +unify scope (VTable p1 res1) (VTable p2 res2) = do + unify scope p2 p1 + unify scope res1 res2 +unify scope (VSort s1) (VSort s2) + | s1 == s2 = return () +unify scope (VInt i) (VInt j) + | i == j = return () +unify scope (VFlt x) (VFlt y) + | x == y = return () +unify scope (VStr s1) (VStr s2) + | s1 == s2 = return () +unify scope VEmpty VEmpty = return () +unify scope v1 v2 = + evalError ("Cannot unify:" <+> ppValue Qualified 0 v1 $$ + " with:" <+> ppValue Qualified 0 v2) - ---- this should be made in Rename - (Q (m,a), Q (n,b)) | a == b -> elem m (allExtendsPlus gr n) - || elem n (allExtendsPlus gr m) - || m == n --- for Predef - (QC (m,a), QC (n,b)) | a == b -> elem m (allExtendsPlus gr n) - || elem n (allExtendsPlus gr m) - (QC (m,a), Q (n,b)) | a == b -> elem m (allExtendsPlus gr n) - || elem n (allExtendsPlus gr m) - (Q (m,a), QC (n,b)) | a == b -> elem m (allExtendsPlus gr n) - || elem n (allExtendsPlus gr m) - -- contravariance - (Table a b, Table c d) -> alpha g c a && alpha g b d - (Vr x, Vr y) -> x == y || elem (x,y) g || elem (y,x) g - _ -> t == u - --- the following should be one-way coercions only. AR 4/1/2001 - || elem t sTypes && elem u sTypes - || (t == typeType && u == typePType) - || (u == typeType && t == typePType) +-- | Invariant: tv1 is a flexible type variable +unifyVar :: Scope -> MetaId -> [Value] -> Tau -> EvalM () +unifyVar scope i vs ty2 = do -- Check whether i is bound + mv <- getMeta i + case mv of + Bound _ ty1 -> do g <- globals + unify scope (apply g ty1 vs) ty2 + Residuation scope' -> do occursCheck scope' i scope ty2 + setMeta i (Bound scope' ty2) - missingLock g t u = case (t,u) of - (RecType rs, RecType ts) -> - let - ls = [l | (l,a) <- rs, - not (any (\ (k,b) -> alpha g a b && l == k) ts)] - (locks,others) = partition isLockLabel ls - in case others of - _:_ -> Bad $ render ("missing record fields:" <+> fsep (punctuate ',' (others))) - _ -> return locks - -- contravariance - (Prod _ x a b, Prod _ y c d) -> do - ls1 <- missingLock g c a - ls2 <- missingLock g b d - return $ ls1 ++ ls2 +occursCheck scope' i0 scope v = + let m = length scope' + n = length scope + in check m n v + where + check m n (VApp c f vs) = mapM_ (check m n) vs + check m n (VMeta i vs) + | i0 == i = do ty1 <- value2termM False (scopeVars scope) (VMeta i vs) + ty2 <- value2termM False (scopeVars scope) v + evalError ("Occurs check for" <+> ppTerm Unqualified 0 ty1 <+> "in:" $$ + nest 2 (ppTerm Unqualified 0 ty2)) + | otherwise = do + s <- getMeta i + case s of + Bound _ v -> do g <- globals + check m n (apply g v vs) + _ -> mapM_ (check m n) vs + check m n (VGen i vs) + | i > m = let (v,_) = reverse scope !! i + in evalError ("Variable" <+> pp v <+> "has escaped") + | otherwise = mapM_ (check m n) vs + check m n (VClosure env c (Abs bt x t)) = do + g <- globals + check (m+1) (n+1) (eval g ((x,VGen n []):env) c t []) + check m n (VProd bt x ty1 ty2) = do + check m n ty1 + case ty2 of + VClosure env c t -> do g <- globals + check (m+1) (n+1) (eval g ((x,VGen n []):env) c t []) + _ -> check m n ty2 + check m n (VRecType as _) = + mapM_ (\(_,_,v) -> check m n v) as + check m n (VR as) = + mapM_ (\(lbl,v) -> check m n v) as + check m n (VP v l vs) = + check m n v >> mapM_ (check m n) vs + check m n (VExtR v1 v2) = + check m n v1 >> check m n v2 + check m n (VTable v1 v2) = + check m n v1 >> check m n v2 + check m n (VT ty env c cs) = + check m n ty -- Traverse cs as well + check m n (VV ty cs) = + check m n ty >> mapM_ (check m n) cs + check m n (VS v1 v2 vs) = + check m n v1 >> check m n v2 >> mapM_ (check m n) vs + check m n (VSort _) = return () + check m n (VInt _) = return () + check m n (VFlt _) = return () + check m n (VStr _) = return () + check m n VEmpty = return () + check m n (VC v1 v2) = + check m n v1 >> check m n v2 + check m n (VGlue v1 v2) = + check m n v1 >> check m n v2 + check m n (VPatt _ _ _) = return () + check m n (VPattType v) = + check m n v + check m n (VFV c vs) = + mapM_ (check m n) (unvariants 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 (VStrs vs) = + mapM_ (check m n) vs + check m n (VInts _ _) = return () - _ -> Bad "" +----------------------------------------------------------------------- +-- Instantiation and quantification +----------------------------------------------------------------------- - sTypes = [typeStr, typeTok, typeString] - --- auxiliaries - --- | light-weight substitution for dep. types -substituteLType :: Context -> Type -> Check Type -substituteLType g t = case t of - Vr x -> return $ maybe t id $ lookup x [(x,t) | (_,x,t) <- g] - _ -> composOp (substituteLType g) t - -termWith :: Term -> Check Type -> Check (Term, Type) -termWith t ct = do - ty <- ct +-- | Instantiate the topmost implicit arguments with metavariables +instantiate :: Scope -> Term -> Sigma -> EvalM (Term,Rho) +instantiate scope t (VProd Implicit x ty1 ty2) = do + i <- newResiduation scope + ty2 <- case ty2 of + VClosure env c ty2 -> do g <- globals + return (eval g ((x,VMeta i []):env) c ty2 []) + ty2 -> return ty2 + instantiate scope (App t (ImplArg (Meta i))) ty2 +instantiate scope t ty@(VMeta i args) = getMeta i >>= \case + Bound _ v -> instantiate scope t v + _ -> return (t,ty) -- We don't have enough information to try any instantiation +instantiate scope t ty = do return (t,ty) --- | compositional check\/infer of binary operations -check2 :: (Term -> Check Term) -> (Term -> Term -> Term) -> - Term -> Term -> Type -> Check (Term,Type) -check2 chk con a b t = do - a' <- chk a - b' <- chk b - return (con a' b', t) +-- | Build fresh lambda abstractions for the topmost implicit arguments +skolemise :: Scope -> Sigma -> EvalM (Scope, Term->Term, Rho) +skolemise scope ty@(VMeta i vs) = do + mv <- getMeta i + case mv of + Residuation _ -> return (scope,id,ty) -- guarded constant? + Bound _ ty -> do g <- globals + skolemise scope (apply g ty vs) +skolemise scope (VProd Implicit x ty1 ty2) = do + let v = newVar scope + ty2 <- evalCodomain x (VGen (length scope) []) ty2 + (scope,f,ty2) <- skolemise ((v,ty1):scope) ty2 + return (scope,Abs Implicit v . f,ty2) +skolemise scope ty = do + return (scope,id,ty) --- printing a type with a lock field lock_C as C -ppType :: Type -> Doc -ppType ty = - case ty of - RecType fs -> case filter isLockLabel $ map fst fs of - [lock] -> pp (drop 5 (showIdent (label2ident lock))) - _ -> ppTerm Unqualified 0 ty - Prod _ x a b -> ppType a <+> "->" <+> ppType b - _ -> ppTerm Unqualified 0 ty +-- | Quantify over the specified type variables (all flexible) +quantify :: Scope -> Term -> [MetaId] -> Rho -> EvalM (Term,Sigma) +quantify scope t tvs ty = do + let m = length tvs + n = length scope + (used_bndrs,ty) <- check m n [] ty + let new_bndrs = take m (allBinders \\ used_bndrs) + mapM_ (bind ([(var,VSort cType)|var <- new_bndrs]++scope)) (zip3 [0..] tvs new_bndrs) + let ty' = foldr (\ty -> VProd Implicit ty vtypeType) ty new_bndrs + return (foldr (Abs Implicit) t new_bndrs,ty') + where + bind scope (i, meta_id, name) = setMeta meta_id (Bound scope (VGen i [])) -checkLookup :: Ident -> Context -> Check Type -checkLookup x g = - case [ty | (b,y,ty) <- g, x == y] of - [] -> checkError ("unknown variable" <+> x) - (ty:_) -> return ty + check m n xs (VApp c f vs) = do + (xs,vs) <- mapAccumM (check m n) xs vs + return (xs,VApp c f vs) + check m n xs (VMeta i vs) = do + s <- getMeta i + case s of + Bound _ v -> do g <- globals + check m n xs (apply g v vs) + _ -> do (xs,vs) <- mapAccumM (check m n) xs vs + return (xs,VMeta i vs) + check m n st (VGen i vs)= do + (st,vs) <- mapAccumM (check m n) st vs + return (st, VGen (m+i) vs) + check m n st (VClosure env c (Abs bt x t)) = do + (st,env) <- mapAccumM (\st (x,v) -> check m n st v >>= \(st,v) -> return (st,(x,v))) st env + return (st,VClosure env c (Abs bt x t)) + check m n xs (VProd bt x v1 v2) = do + (xs,v1) <- check m n xs v1 + case v2 of + VClosure env c t -> do (st,env) <- mapAccumM (\xs (x,tnk) -> check m n xs tnk >>= \(xs,tnk) -> return (xs,(x,tnk))) xs env + return (x:xs,VProd bt x v1 (VClosure env c t)) + v2 -> do (xs,v2) <- check m (n+1) xs v2 + return (x:xs,VProd bt x v1 v2) + check m n xs (VRecType as ext) = do + (xs,as) <- mapAccumM (\xs (l,o,v) -> check m n xs v >>= \(xs,v) -> return (xs,(l,o,v))) xs as + return (xs,VRecType as ext) + check m n xs (VR as) = do + (xs,as) <- mapAccumM (\xs (lbl,tnk) -> check m n xs tnk >>= \(xs,tnk) -> return (xs,(lbl,tnk))) xs as + return (xs,VR as) + check m n xs (VP v l vs) = do + (xs,v) <- check m n xs v + (xs,vs) <- mapAccumM (check m n) xs vs + return (xs,VP v l vs) + check m n xs (VExtR v1 v2) = do + (xs,v1) <- check m n xs v1 + (xs,v2) <- check m n xs v2 + return (xs,VExtR v1 v2) + check m n xs (VTable v1 v2) = do + (xs,v1) <- check m n xs v1 + (xs,v2) <- check m n xs v2 + return (xs,VTable v1 v2) + check m n xs (VT ty env c cs) = do + (xs,ty) <- check m n xs ty + (xs,env) <- mapAccumM (\xs (x,tnk) -> check m n xs tnk >>= \(xs,tnk) -> return (xs,(x,tnk))) xs env + return (xs,VT ty env c cs) + check m n xs (VV ty cs) = do + (xs,ty) <- check m n xs ty + (xs,cs) <- mapAccumM (check m n) xs cs + return (xs,VV ty cs) + check m n xs (VS v1 tnk vs) = do + (xs,v1) <- check m n xs v1 + (xs,tnk) <- check m n xs tnk + (xs,vs) <- mapAccumM (check m n) xs vs + return (xs,VS v1 tnk vs) + check m n xs v@(VSort _) = return (xs,v) + check m n xs v@(VInt _) = return (xs,v) + check m n xs v@(VFlt _) = return (xs,v) + check m n xs v@(VStr _) = return (xs,v) + check m n xs v@VEmpty = return (xs,v) + check m n xs (VC v1 v2) = do + (xs,v1) <- check m n xs v1 + (xs,v2) <- check m n xs v2 + return (xs,VC v1 v2) + check m n xs (VGlue v1 v2) = do + (xs,v1) <- check m n xs v1 + (xs,v2) <- check m n xs v2 + return (xs,VGlue v1 v2) + check m n xs v@(VPatt _ _ _) = return (xs,v) + check m n xs (VPattType v) = do + (xs,v) <- check m n xs v + return (xs,VPattType v) + check m n xs (VFV c (VarFree vs)) = do + (xs,vs) <- mapAccumM (check m n) xs 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 + (xs,v) <- check m n xs v + (xs,vs) <- mapAccumM (\xs (v1,v2) -> do (xs,v1) <- check m n xs v1 + (xs,v2) <- check m n xs v2 + return (xs,(v1,v2))) + xs vs + return (xs,VAlts v vs) + check m n xs (VStrs vs) = do + (xs,vs) <- mapAccumM (check m n) xs vs + return (xs,VStrs vs) + check m n xs v@(VInts _ _) = return (xs,v) + check m n xs v = unimplemented ("check "++show (ppValue Unqualified 5 v)) + + mapAccumM :: Monad m => (a -> b -> m (a,c)) -> a -> [b] -> m (a,[c]) + mapAccumM f s [] = return (s,[]) + mapAccumM f s (x:xs) = do + (s,y) <- f s x + (s,ys) <- mapAccumM f s xs + return (s,y:ys) + +allBinders :: [Ident] -- a,b,..z, a1, b1,... z1, a2, b2,... +allBinders = [ identS [x] | x <- ['a'..'z'] ] ++ + [ identS (x : show i) | i <- [1 :: Integer ..], x <- ['a'..'z']] + +----------------------------------------------------------------------- +-- Helpers +----------------------------------------------------------------------- + +type Sigma = Value +type Rho = Value -- No top-level ForAll +type Tau = Value -- No ForAlls anywhere + +unimplemented str = fail ("Unimplemented: "++str) + +lookup3 l [] = Nothing +lookup3 l ((l',_,v):rs) + | l == l' = Just v + | otherwise = lookup3 l rs + +update3 l o v [] = [(l,o,v)] +update3 l o v (r@(l',_,_):rs) + | l == l' = (l,o,v) : rs + | otherwise = r : update3 l o v rs + +newVar :: Scope -> Ident +newVar scope = head [x | i <- [1..], + let x = identS ('v':show i), + isFree scope x] + where + isFree [] x = True + isFree ((y,_):scope) x = x /= y && isFree scope x + +scopeEnv scope = zipWith (\(x,ty) i -> (x,VGen i [])) (reverse scope) [0..] +scopeVars scope = map fst scope +scopeTypes scope = zipWith (\(_,ty) scope -> (scope,ty)) scope (tails scope) + +-- | This function takes account of zonking, and returns a set +-- (no duplicates) of unbound meta-type variables +getMetaVars :: [(Scope,Sigma)] -> EvalM [MetaId] +getMetaVars sc_tys = foldM (\acc (scope,ty) -> go acc ty) [] sc_tys + where + -- Get the MetaIds from a term; no duplicates in result + go acc (VGen i args) = foldM go acc args + go acc (VSort s) = return acc + go acc (VInt _) = return acc + go acc (VRecType vs _) = foldM (\acc (lbl,_,v) -> go acc v) acc vs + go acc (VClosure _ _ _) = return acc + go acc (VProd b x v1 v2) = go acc v2 >>= \acc -> go acc v1 + go acc (VTable v1 v2) = go acc v2 >>= \acc -> go acc v1 + go acc (VMeta m args) + | m `elem` acc = return acc + | otherwise = do res <- getMeta m + case res of + Bound _ v -> go acc v + _ -> foldM go (m:acc) args + go acc (VApp c f args) = foldM go acc args + go acc (VFV c vs) = foldM go acc (unvariants vs) + go acc (VInts _ _) = return acc + go acc (VPattType v) = go acc v + go acc v = unimplemented ("go "++show (ppValue Unqualified 5 v)) + +-- | Eliminate any substitutions in a term +zonkTerm :: [Ident] -> Term -> EvalM Term +zonkTerm xs (Abs b x t) = do + t <- zonkTerm (x:xs) t + return (Abs b x t) +zonkTerm xs (Prod b x t1 t2) = do + t1 <- zonkTerm xs t1 + t2 <- zonkTerm xs' t2 + return (Prod b x t1 t2) + where + xs' | x == identW = xs + | otherwise = x:xs +zonkTerm xs (Meta i) = do + st <- getMeta i + case st of + Bound _ v -> zonkTerm xs =<< value2termM False xs v + _ -> return (Meta i) +zonkTerm xs t = composOp (zonkTerm xs) t + +zonkValue :: Value -> EvalM Value +zonkValue (VProd bt x ty1 ty2) = do + ty1 <- zonkValue ty1 + ty2 <- zonkValue ty2 + return (VProd bt x ty1 ty2) +zonkValue (VMeta i vs) = do + g <- globals + st <- getMeta i + case st of + Bound _ v -> zonkValue (apply g v vs) + _ -> do vs <- mapM zonkValue vs + return (VMeta i vs) +zonkValue (VSusp i k vs) = do + g <- globals + st <- getMeta i + case st of + Bound _ v -> zonkValue (apply g (k v) vs) + _ -> do vs <- mapM zonkValue vs + return (VSusp i k vs) +zonkValue v = return v diff --git a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs deleted file mode 100644 index 2c03d866f..000000000 --- a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs +++ /dev/null @@ -1,1282 +0,0 @@ -{-# LANGUAGE RankNTypes, CPP, TupleSections, LambdaCase #-} -module GF.Compile.TypeCheck.ConcreteNew ( checkLType, checkLType', inferLType, inferLType' ) where - --- The code here is based on the paper: --- Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich. --- Practical type inference for arbitrary-rank types. --- 14 September 2011 - -import GF.Grammar hiding (Env, VGen, VApp, VRecType, ppValue) -import GF.Grammar.Lookup -import GF.Grammar.Predef -import GF.Grammar.Lockfield -import GF.Compile.Compute.Concrete2 -import GF.Infra.CheckM -import GF.Data.ErrM ( Err(Ok, Bad) ) -import Control.Applicative(Applicative(..)) -import Control.Monad(ap,liftM,mplus,foldM,zipWithM,forM,filterM,unless) -import Control.Monad.ST -import GF.Text.Pretty -import Data.STRef -import Data.List (nub, (\\), tails) -import qualified Data.Map as Map -import Data.Maybe(fromMaybe,isNothing,mapMaybe) -import Data.Bifunctor(second) -import Data.Functor((<&>)) -import qualified Control.Monad.Fail as Fail - -checkLType :: Globals -> Term -> Type -> Check [(Term, Type)] -checkLType globals t ty = runEvalM globals $ - do let (c1,c2) = split unit - (t,vty) <- checkLType' c1 t (eval globals [] c2 ty []) - ty <- value2termM True [] vty - return (t,ty) - -checkLType' :: Choice -> Term -> Constraint -> EvalM (Term, Constraint) -checkLType' c t vty = do - (t,vty) <- tcRho [] c t (Just vty) - t <- zonkTerm [] t - return (t,vty) - -inferLType :: Globals -> Term -> Check [(Term, Type)] -inferLType globals t = runEvalM globals $ do - (t,vty) <- inferLType' t - ty <- value2termM True [] vty - return (t,ty) - -inferLType' :: Term -> EvalM (Term, Constraint) -inferLType' t = do - (t,vty) <- inferSigma [] unit t - t <- zonkTerm [] t - return (t,vty) - -inferSigma :: Scope -> Choice -> Term -> EvalM (Term,Sigma) -inferSigma scope s t = do -- GEN1 - (t,ty) <- tcRho scope s t Nothing - env_tvs <- getMetaVars (scopeTypes scope) - res_tvs <- getMetaVars [(scope,ty)] - let forall_tvs = res_tvs \\ env_tvs - quantify scope t forall_tvs ty - -vtypeInt = VApp poison (cPredef,cInt) [] -vtypeFloat = VApp poison (cPredef,cFloat) [] -vtypeInts i= VApp poison (cPredef,cInts) [VInt i] -vtypeStr = VSort cStr -vtypeStrs = VSort cStrs -vtypeType = VSort cType -vtypePType = VSort cPType -vtypeMarkup= VApp poison (cPredef,cMarkup) [] - -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@(EFloat _) mb_ty = instSigma scope s t vtypeFloat mb_ty -- FLOAT -tcRho scope s t@(K _) mb_ty = instSigma scope s t vtypeStr mb_ty -- STR -tcRho scope s t@(Empty) mb_ty = instSigma scope s t vtypeStr mb_ty -tcRho scope s t@(Vr v) mb_ty = do -- VAR - case lookup v scope of - Just v_sigma -> instSigma scope s t v_sigma mb_ty - Nothing -> evalError ("Unknown variable" <+> v) -tcRho scope c t@(Q id) mb_ty = tcApp scope c t t [] mb_ty -tcRho scope c t@(QC id) mb_ty = tcApp scope c t t [] mb_ty -tcRho scope c t@(App fun arg) mb_ty = tcApp scope c t t [] mb_ty -tcRho scope c (Abs bt var body) Nothing = do -- ABS1 - i <- newResiduation scope - let arg_ty = VMeta i [] - (body,body_ty) <- tcRho ((var,arg_ty):scope) c body Nothing - let m = length scope - n = m+1 - (b,used_bndrs) <- check m n (False,[]) body_ty - if b - then let v = head (allBinders \\ used_bndrs) - 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)) - where - check m n st (VApp c f vs) = foldM (check m n) st vs - check m n st (VMeta i vs) = do - state <- getMeta i - case state of - Bound _ v -> do g <- globals - check m n st (apply g v vs) - _ -> foldM (check m n) st vs - check m n st@(b,xs) (VGen i vs) - | i == m = return (True, xs) - | otherwise = return st - check m n st (VClosure env c (Abs bt x t)) = do - g <- globals - check m (n+1) st (eval g ((x,VGen n []):env) c t []) - check m n st (VProd _ x v1 v2) = do - st@(b,xs) <- check m n st v1 - case v2 of - VClosure env c t -> do g <- globals - check m (n+1) (b,x:xs) (eval g ((x,VGen n []):env) c t []) - v2 -> check m n st v2 - check m n st (VRecType as) = foldM (\st (l,v) -> check m n st v) st as - check m n st (VR as) = - foldM (\st (lbl,tnk) -> check m n st tnk) st as - check m n st (VP v l vs) = - check m n st v >>= \st -> foldM (check m n) st vs - check m n st (VExtR v1 v2) = - check m n st v1 >>= \st -> check m n st v2 - check m n st (VTable v1 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 ty -- Traverse cs as well - check m n st (VV ty cs) = - check m n st ty >>= \st -> foldM (check m n) st cs - check m n st (VS v1 tnk vs) = do - st <- check m n st v1 - st <- check m n st tnk - foldM (check m n) st vs - check m n st (VSort _) = return st - check m n st (VInt _) = return st - check m n st (VFlt _) = return st - check m n st (VStr _) = return st - check m n st VEmpty = return st - check m n st (VC v1 v2) = - check m n st v1 >>= \st -> check m n st v2 - check m n st (VGlue v1 v2) = - check m n st v1 >>= \st -> check m n st v2 - check m n st (VPatt _ _ _) = return st - check m n st (VPattType v) = check m n st v - check m n st (VAlts v vs) = do - st <- check m n st v - foldM (\st (v1,v2) -> check m n st v1 >>= \st -> check m n st v2) st vs - check m n st (VStrs vs) = - foldM (check m n) st vs -tcRho scope c t@(Abs Implicit var body) (Just ty) = do -- ABS2 - (bt, x, var_ty, body_ty) <- unifyFun scope ty - if bt == Implicit - then return () - else evalError (ppTerm Unqualified 0 t <+> "is an implicit function, but no implicit function is expected") - body_ty <- evalCodomain scope x body_ty - (body, body_ty) <- tcRho ((var,var_ty):scope) c body (Just body_ty) - return (Abs Implicit var body,ty) -tcRho scope c (Abs Explicit var body) (Just ty) = do -- ABS3 - (scope,f,ty') <- skolemise scope ty - (_,x,var_ty,body_ty) <- unifyFun scope ty' - body_ty <- evalCodomain scope x body_ty - (body, body_ty) <- tcRho ((var,var_ty):scope) c body (Just body_ty) - return (f (Abs Explicit var body),ty) -tcRho scope c (Meta _) mb_ty = do - i <- newResiduation scope - ty <- case mb_ty of - Just ty -> return ty - Nothing -> do j <- newResiduation scope - return (VMeta j []) - return (Meta i, ty) -tcRho scope c (Let (var, (Nothing, rhs)) body) mb_ty = do -- LET - let (c1,c2) = split c - (rhs,var_ty) <- tcRho scope c1 rhs Nothing - (body, body_ty) <- tcRho ((var,var_ty):scope) c2 body mb_ty - var_ty <- value2termM True (scopeVars scope) var_ty - return (Let (var, (Just var_ty, rhs)) body, body_ty) -tcRho scope c (Let (var, (Just ann_ty, rhs)) body) mb_ty = do -- LET - let (c1,c2,c3,c4) = split4 c - (ann_ty, _) <- tcRho scope c1 ann_ty (Just vtypeType) - g <- globals - let v_ann_ty = eval g (scopeEnv scope) c2 ann_ty [] - (rhs,_) <- tcRho scope c3 rhs (Just v_ann_ty) - (body, body_ty) <- tcRho ((var,v_ann_ty):scope) c4 body mb_ty - var_ty <- value2termM True (scopeVars scope) v_ann_ty - return (Let (var, (Just var_ty, rhs)) body, body_ty) -tcRho scope c (Typed body ann_ty) mb_ty = do -- ANNOT - let (c1,c2,c3,c4) = split4 c - (ann_ty, _) <- tcRho scope c1 ann_ty (Just vtypeType) - g <- globals - let v_ann_ty = eval g (scopeEnv scope) c2 ann_ty [] - (body,_) <- tcRho scope c3 body (Just v_ann_ty) - instSigma scope c4 (Typed body ann_ty) v_ann_ty mb_ty -tcRho scope c (FV ts) mb_ty = do - (ts,ty) <- tcUnifying scope c ts mb_ty - return (FV ts, ty) -tcRho scope s t@(Sort _) mb_ty = do - instSigma scope s t vtypeType mb_ty -tcRho scope c t@(RecType rs) Nothing = do - (rs,mb_ty) <- tcRecTypeFields scope c rs Nothing - return (RecType rs,fromMaybe vtypePType mb_ty) -tcRho scope c t@(RecType rs) (Just ty) = do - (scope,f,ty') <- skolemise scope ty - case ty' of - VSort s - | s == cType -> return () - | s == cPType -> return () - VMeta i vs-> case rs of - [] -> unifyVar scope i vs vtypePType - _ -> return () - ty -> do ty <- value2termM False (scopeVars scope) ty - evalError ("The record type" <+> ppTerm Unqualified 0 t $$ - "cannot be of type" <+> ppTerm Unqualified 0 ty) - (rs,mb_ty) <- tcRecTypeFields scope c rs (Just ty') - return (f (RecType rs),ty) -tcRho scope s t@(Table p res) mb_ty = do - let (s1,s23) = split s - (s2,s3) = split s23 - (p, p_ty) <- tcRho scope s1 p (Just vtypePType) - (res,res_ty) <- tcRho scope s2 res (Just vtypeType) - instSigma scope s3 (Table p res) vtypeType mb_ty -tcRho scope c (Prod bt x ty1 ty2) mb_ty = do - let (c1,c2,c3,c4) = split4 c - (ty1,ty1_ty) <- tcRho scope c1 ty1 (Just vtypeType) - g <- globals - (ty2,ty2_ty) <- tcRho ((x,eval g (scopeEnv scope) c2 ty1 []):scope) c3 ty2 (Just vtypeType) - instSigma scope c4 (Prod bt x ty1 ty2) vtypeType mb_ty -tcRho scope c (S t p) mb_ty = do - let (c1,c2) = split c - let mk_val i = VMeta i [] - p_ty <- fmap mk_val $ newResiduation scope - res_ty <- case mb_ty of - Nothing -> fmap mk_val $ newResiduation scope - Just ty -> return ty - let t_ty = VTable p_ty res_ty - (t,t_ty) <- tcRho scope c1 t (Just t_ty) - (p,_) <- tcRho scope c2 p (Just p_ty) - return (S t p, res_ty) -tcRho scope c (T tt ps) Nothing = do -- ABS1/AABS1 for tables - let (c1,c2) = split c - let mk_val i = VMeta i [] - p_ty <- case tt of - TRaw -> fmap mk_val $ newResiduation scope - TTyped ty -> do let (c3,c4) = split c1 - (ty, _) <- tcRho scope c3 ty (Just vtypeType) - g <- globals - return (eval g (scopeEnv scope) c4 ty []) - res_ty <- fmap mk_val $ newResiduation scope - ps <- tcCases scope c2 ps p_ty res_ty - p_ty_t <- value2termM True [] p_ty - return (T (TTyped p_ty_t) ps, VTable p_ty res_ty) -tcRho scope c (T tt ps) (Just ty) = do -- ABS2/AABS2 for tables - let (c12,c34) = split c - (c3,c4) = split c34 - (scope,f,ty') <- skolemise scope ty - (p_ty, res_ty) <- unifyTbl scope ty' - case tt of - TRaw -> return () - TTyped ty -> do let (c1,c2) = split c12 - (ty, _) <- tcRho scope c1 ty (Just vtypeType) - g <- globals - unify scope (eval g (scopeEnv scope) c2 ty []) p_ty - ps <- tcCases scope c3 ps p_ty res_ty - p_ty_t <- value2termM True (scopeVars scope) p_ty - return (f (T (TTyped p_ty_t) ps), VTable p_ty res_ty) -tcRho scope c (V p_ty ts) Nothing = do - let (c1,c2,c3,c4) = split4 c - (p_ty, _) <- tcRho scope c1 p_ty (Just vtypeType) - i <- newResiduation scope - let res_ty = VMeta i [] - - let go c t = do (t, ty) <- tcRho scope c t Nothing - subsCheckRho scope t ty res_ty - - ts <- mapCM go c2 ts - g <- globals - return (V p_ty ts, VTable (eval g (scopeEnv scope) c3 p_ty []) res_ty) -tcRho scope c (V p_ty0 ts) (Just ty) = do - let (c1,c2,c3,c4) = split4 c - (scope,f,ty') <- skolemise scope ty - (p_ty, res_ty) <- unifyTbl scope ty' - (p_ty0, _) <- tcRho scope c1 p_ty0 (Just vtypeType) - g <- globals - let p_vty0 = eval g (scopeEnv scope) c2 p_ty0 [] - unify scope p_ty p_vty0 - ts <- mapCM (\c t -> fmap fst $ tcRho scope c t (Just res_ty)) c3 ts - return (V p_ty0 ts, VTable p_ty res_ty) -tcRho scope c (R rs) Nothing = do - lttys <- inferRecFields scope c rs - rs <- mapM (\(l,t,ty) -> value2termM True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys - return (R rs, - VRecType [(l, ty) | (l,t,ty) <- lttys] - ) -tcRho scope c (R rs) (Just ty) = do - (scope,f,ty') <- skolemise scope ty - case ty' of - (VRecType ltys) -> do lttys <- checkRecFields scope c rs ltys - rs <- mapM (\(l,t,ty) -> value2termM True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys - return ((f . R) rs, - VRecType [(l, ty) | (l,t,ty) <- lttys] - ) - ty -> do lttys <- inferRecFields scope c rs - t <- liftM (f . R) (mapM (\(l,t,ty) -> value2termM True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys) - let ty' = VRecType [(l, ty) | (l,t,ty) <- lttys] - t <- subsCheckRho scope t ty' ty - return (t, ty') -tcRho scope c (P t l) mb_ty = do - l_ty <- case mb_ty of - Just ty -> return ty - Nothing -> do i <- newResiduation scope - return (VMeta i []) - (t,t_ty) <- tcRho scope c t (Just (VRecType [(l,l_ty)])) - return (P t l,l_ty) -tcRho scope c (C t1 t2) mb_ty = do - let (c1,c2,c3,c4) = split4 c - (t1,t1_ty) <- tcRho scope c1 t1 (Just vtypeStr) - (t2,t2_ty) <- tcRho scope c2 t2 (Just vtypeStr) - instSigma scope c3 (C t1 t2) vtypeStr mb_ty -tcRho scope c (Glue t1 t2) mb_ty = do - let (c1,c2,c3,c4) = split4 c - (t1,t1_ty) <- tcRho scope c1 t1 (Just vtypeStr) - (t2,t2_ty) <- tcRho scope c2 t2 (Just vtypeStr) - instSigma scope c3 (Glue t1 t2) vtypeStr mb_ty -tcRho scope c t@(ExtR t1 t2) mb_ty = do - let (c1,c2,c3,c4) = split4 c - (t1,t1_ty) <- tcRho scope c1 t1 Nothing - (t2,t2_ty) <- tcRho scope c2 t2 Nothing - case (t1_ty,t2_ty) of - (VSort s1,VSort s2) - | (s1 == cType || s1 == cPType) && - (s2 == cType || s2 == cPType) -> let sort | s1 == cPType && s2 == cPType = cPType - | otherwise = cType - in instSigma scope c3 (ExtR t1 t2) (VSort sort) mb_ty - (VRecType rs1, VRecType rs2) -> instSigma scope c3 (ExtR t1 t2) (VRecType (rs2++rs1)) mb_ty - _ -> evalError ("Cannot type check" <+> ppTerm Unqualified 0 t) -tcRho scope c (ELin cat t) mb_ty = do -- this could be done earlier, i.e. in the parser - tcRho scope c (ExtR t (R [(lockLabel cat,(Just (RecType []),R []))])) mb_ty -tcRho scope c (ELincat cat t) mb_ty = do -- this could be done earlier, i.e. in the parser - tcRho scope c (ExtR t (RecType [(lockLabel cat,RecType [])])) mb_ty -tcRho scope c (Alts t ss) mb_ty = do - let (c1,c2,c3,c4) = split4 c - (t,_) <- tcRho scope c1 t (Just vtypeStr) - ss <- mapCM (\c (t1,t2) -> do - let (c1,c2) = split c - (t1,_) <- tcRho scope c1 t1 (Just vtypeStr) - (t2,_) <- tcRho scope c2 t2 (Just vtypeStrs) - return (t1,t2)) - c2 ss - instSigma scope c3 (Alts t ss) vtypeStr mb_ty -tcRho scope c (Strs ss) mb_ty = do - let (c1,c2) = split c - ss <- mapCM (\c t -> do (t,_) <- tcRho scope c t (Just vtypeStr) - return t) - c1 ss - instSigma scope c2 (Strs ss) vtypeStrs mb_ty -tcRho scope c (EPattType ty) mb_ty = do - let (c1,c2) = split c - (ty, _) <- tcRho scope c1 ty (Just vtypeType) - instSigma scope c2 (EPattType ty) vtypeType mb_ty -tcRho scope c t@(EPatt min max p) mb_ty = do - (scope,f,ty) <- case mb_ty of - Nothing -> do i <- newResiduation scope - return (scope,id,VMeta i []) - Just ty -> do (scope,f,ty) <- skolemise scope ty - case ty of - VPattType ty -> return (scope,f,ty) - _ -> evalError (ppTerm Unqualified 0 t <+> "must be of pattern type but" <+> ppTerm Unqualified 0 t <+> "is expected") - tcPatt scope c p ty - return (f (EPatt min max p), ty) -tcRho scope c (Markup tag attrs children) mb_ty = do - let (c1,c2,c3,c4) = split4 c - attrs <- mapCM (\c (id,t) -> do - (t,_) <- tcRho scope c t Nothing - return (id,t)) - c1 attrs - res <- mapCM (\c child -> tcRho scope c child Nothing) c2 children - instSigma scope c3 (Markup tag attrs (map fst res)) vtypeMarkup mb_ty -tcRho scope c (Reset ctl mb_ct t qid) mb_ty - | ctl == cConcat = do - let (c1,c23) = split c - (c2,c3 ) = split c23 - (t,_) <- tcRho scope c1 t Nothing - mb_ct <- case mb_ct of - Just ct -> do (ct,_) <- tcRho scope c2 ct (Just vtypeInt) - return (Just ct) - Nothing -> return Nothing - instSigma scope c2 (Reset ctl mb_ct t qid) vtypeMarkup mb_ty - | ctl == cOne = do - let (c1,c2) = split c - (t,ty) <- tcRho scope c1 t mb_ty - (mb_ct,ty) <- case mb_ct of - Just ct -> do (ct,ty) <- tcRho scope c2 ct (Just ty) - return (Just ct,ty) - Nothing -> return (Nothing,ty) - return (Reset ctl mb_ct t qid,ty) - | ctl == cDefault = do - let (c1,c2) = split c - (t,ty) <- tcRho scope c1 t mb_ty - (mb_ct,ty) <- case mb_ct of - Just ct -> do (ct,ty) <- tcRho scope c2 ct (Just ty) - return (Just ct,ty) - Nothing -> evalError (pp "[list: .. | ..] requires an argument") - return (Reset ctl mb_ct t qid,ty) - | ctl == cList = do - do let (c1,c2) = split c - mb_ct <- case mb_ct of - Just ct -> do (ct,ty) <- tcRho scope c1 ct Nothing - return (Just ct) - Nothing -> evalError (pp "[list: .. | ..] requires an argument") - (t,ty) <- tcRho scope c2 t mb_ty - case ty of - VApp c qid [] -> return (Reset ctl mb_ct t qid, ty) - _ -> evalError (pp "Needs atomic type"<+>ppValue Unqualified 0 ty) - | otherwise = evalError (pp "Operator" <+> pp ctl <+> pp "is not defined") -tcRho scope s (Opts (nty,n) cs) mb_ty = do - gl <- globals - let (s1,s2,s3) = split3 s - (n,nty) <- tcRho scope s1 n (nty <&> \ty -> eval gl [] poison ty []) - nty <- value2termM True [] nty - ls <- forCM s2 cs $ \s' ((lty,l),_) -> do - (l,lty) <- tcRho scope s' l (lty <&> \ty -> eval gl [] poison ty []) - lty <- value2termM True [] lty - return (Just lty, l) - (ts,ty) <- tcUnifying scope s3 (snd <$> cs) mb_ty - return (Opts (Just nty, n) (zip ls ts), ty) -tcRho scope s t _ = unimplemented ("tcRho "++show t) - -evalCodomain :: Scope -> Ident -> Value -> EvalM Value -evalCodomain scope x (VClosure env c t) = do - g <- globals - return (eval g ((x,VGen (length scope) []):env) c 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,t):cs) p_ty res_ty = do - let (c1,c2,c3,c4) = split4 c - scope' <- tcPatt scope c1 p p_ty - (t,_) <- tcRho scope' c2 t (Just res_ty) - cs <- tcCases scope c3 cs p_ty res_ty - return ((p,t):cs) - -tcApp scope c t0 (App fun arg) args mb_ty = tcApp scope c t0 fun (arg:args) mb_ty -- APP -tcApp scope c t0 t@(Q id) args mb_ty = resolveOverloads scope c t0 id args mb_ty -- VAR (global) -tcApp scope c t0 t@(QC id) args mb_ty = resolveOverloads scope c t0 id args mb_ty -- VAR (global) -tcApp scope c t0 t args mb_ty = do - let (c1,c23) = split c - let (c2,c3) = split c23 - (t,ty) <- tcRho scope c1 t Nothing - (t,ty) <- reapply1 scope c2 t ty args - instSigma scope c3 t ty mb_ty - -reapply1 :: Scope -> Choice -> Term -> Value -> [Term] -> EvalM (Term,Rho) -reapply1 scope c fun fun_ty [] = return (fun,fun_ty) -reapply1 scope c fun fun_ty ((ImplArg arg):args) = do -- Implicit arg case - let (c1,c2,c3,c4) = split4 c - (bt, x, arg_ty, res_ty) <- unifyFun scope fun_ty - unless (bt == Implicit) $ - evalError (ppTerm Unqualified 0 (App fun (ImplArg arg)) <+> - "is an implicit argument application, but no implicit argument is expected") - (arg,_) <- tcRho scope c1 arg (Just arg_ty) - res_ty <- case res_ty of - VClosure res_env res_c res_ty -> do g <- globals - return (eval g ((x,eval g (scopeEnv scope) c2 arg []):res_env) res_c res_ty []) - res_ty -> return res_ty - reapply1 scope c3 (App fun (ImplArg arg)) res_ty args -reapply1 scope c fun fun_ty (arg:args) = do -- Explicit arg (fallthrough) case - let (c1,c2,c3,c4) = split4 c - (fun,fun_ty) <- instantiate scope fun fun_ty - (_, x, arg_ty, res_ty) <- unifyFun scope fun_ty - (arg,_) <- tcRho scope c1 arg (Just arg_ty) - res_ty <- case res_ty of - VClosure res_env res_c res_ty -> do g <- globals - return (eval g ((x,eval g (scopeEnv scope) c2 arg []):res_env) res_c res_ty []) - res_ty -> return res_ty - reapply1 scope c3 (App fun arg) res_ty args - -resolveOverloads :: Scope -> Choice -> Term -> QIdent -> [Term] -> Maybe Rho -> EvalM (Term,Rho) -resolveOverloads scope c t0 q args mb_ty = do - g@(Gl gr _) <- globals - case lookupOverloadTypes gr q of - Bad msg -> evalError (pp msg) - Ok [(t,ty)] -> do let (c1,c23) = split c - (c2,c3) = split c23 - (t,ty) <- reapply1 scope c1 t (eval g [] c2 ty []) args - instSigma scope c3 t ty mb_ty - Ok ttys -> do let (c1,c23) = split c - (c2,c3) = split c23 - arg_tys <- mapCM (checkArg g) c1 args - let v_ttys = mapC (\c (t,ty) -> (t,eval g [] c ty [])) c2 ttys - try (\(fun,fun_ty) -> reapply2 scope c3 fun fun_ty arg_tys mb_ty) - (\ttys -> fmap (\(ts,ty) -> (FV ts,ty)) (snd (minimum g ttys))) - v_ttys - where - checkArg g c (ImplArg arg) = do - let (c1,c2) = split c - (arg,arg_ty) <- tcRho scope c1 arg Nothing - let v = eval g (scopeEnv scope) c2 arg [] - return (ImplArg arg,v,arg_ty) - checkArg g c arg = do - let (c1,c2) = split c - (arg,arg_ty) <- tcRho scope c1 arg Nothing - let v = eval g (scopeEnv scope) c2 arg [] - return (arg,v,arg_ty) - - minimum g [] = (maxBound,err) - where - err = evalError (pp "Overload resolution failed") - minimum g (tty@((t,ty),state):ttys) = - let ty' = zonk ty - a = arity ty' - (a',res) = minimum g ttys - in case compare a a' of - GT -> (a',res) - EQ -> (a',join t ty' state res) - LT -> (a ,one t ty' state) - where - arity :: Value -> Int - arity (VProd _ _ _ ty) = 1 + arity ty - arity _ = 0 - - zonk :: Value -> Value - zonk (VProd bt x ty1 ty2) = VProd bt x (zonk ty1) (zonk ty2) - zonk (VMeta i vs) = - case Map.lookup i (metaVars state) of - Just (Bound _ v) -> zonk (apply g v vs) - Just (Residuation _ (Just v)) -> zonk (apply g v vs) - _ -> VMeta i (map zonk vs) - zonk (VSusp i k vs) = - case Map.lookup i (metaVars state) of - Just (Bound _ v) -> zonk (apply g (k v) vs) - Just (Residuation _ (Just v)) -> zonk (apply g (k v) vs) - _ -> VSusp i k (map zonk vs) - zonk v = v - - one t ty state = do - t <- withState state (zonkTerm [] t) - return ([t],ty) - - join t ty state res = do - t <- withState state (zonkTerm [] t) - (ts,ty') <- res - unify scope ty ty' - return (t:ts,ty) - -reapply2 :: Scope -> Choice -> Term -> Value -> [(Term,Value,Value)] -> Maybe Rho -> EvalM (Term,Rho) -reapply2 scope c fun fun_ty [] mb_ty = instSigma scope c fun fun_ty mb_ty -reapply2 scope c fun fun_ty ((ImplArg arg,arg_v,arg_ty):args) mb_ty = do -- Implicit arg case - (bt, x, arg_ty', res_ty) <- unifyFun scope fun_ty - unless (bt == Implicit) $ - evalError (ppTerm Unqualified 0 (App fun (ImplArg arg)) <+> - "is an implicit argument application, but no implicit argument is expected") - arg <- subsCheckRho scope arg arg_ty' arg_ty - res_ty <- case res_ty of - VClosure res_env res_c res_ty -> do g <- globals - return (eval g ((x,arg_v):res_env) res_c res_ty []) - res_ty -> return res_ty - reapply2 scope c (App fun (ImplArg arg)) res_ty args mb_ty -reapply2 scope c fun fun_ty ((arg,arg_v,arg_ty):args) mb_ty = do -- Explicit arg (fallthrough) case - (fun,fun_ty) <- instantiate scope fun fun_ty - (_, x, arg_ty', res_ty) <- unifyFun scope fun_ty - arg <- subsCheckRho scope arg arg_ty arg_ty' - res_ty <- case res_ty of - VClosure res_env res_c res_ty -> do g <- globals - return (eval g ((x,arg_v):res_env) res_c res_ty []) - res_ty -> return res_ty - reapply2 scope c (App fun arg) res_ty args mb_ty - -tcPatt scope c PW ty0 = - return scope -tcPatt scope c (PV x) ty0 = - return ((x,ty0):scope) -tcPatt scope c (PP q ps) ty0 = do - g@(Gl gr _) <- globals - ty <- case lookupResType gr q of - Ok ty -> return ty - Bad msg -> evalError (pp msg) - let go scope c ty [] = return (scope,ty) - go scope c ty (p:ps) = do (_,_,arg_ty,res_ty) <- unifyFun scope ty - let (c1,c2) = split c - scope <- tcPatt scope c1 p arg_ty - go scope c2 res_ty ps - let (c1,c2) = split c - (scope,ty) <- go scope c1 (eval g [] c2 ty []) ps - unify scope ty0 ty - return scope -tcPatt scope c (PInt i) ty0 = do - unify scope (vtypeInts i) ty0 - return scope -tcPatt scope c (PString s) ty0 = do - unify scope ty0 vtypeStr - return scope -tcPatt scope c PChar ty0 = do - unify scope ty0 vtypeStr - return scope -tcPatt scope c (PSeq _ _ p1 _ _ p2) ty0 = do - unify scope ty0 vtypeStr - let (c1,c2) = split c - scope <- tcPatt scope c1 p1 vtypeStr - scope <- tcPatt scope c2 p2 vtypeStr - return scope -tcPatt scope c (PAs x p) ty0 = do - tcPatt ((x,ty0):scope) c p ty0 -tcPatt scope c (PR rs) ty0 = do - let mk_ltys [] = return [] - mk_ltys ((l,p):rs) = do i <- newResiduation scope - ltys <- mk_ltys rs - return ((l,p,VMeta i []) : ltys) - go scope c [] = return scope - go scope c ((l,p,ty):rs) = do let (c1,c2) = split c - scope <- tcPatt scope c1 p ty - go scope c2 rs - ltys <- mk_ltys rs - subsCheckRho scope (EPatt 0 Nothing (PR rs)) (VRecType [(l,ty) | (l,p,ty) <- ltys]) ty0 - go scope c ltys -tcPatt scope c (PAlt p1 p2) ty0 = do - let (c1,c2) = split c - tcPatt scope c1 p1 ty0 - tcPatt scope c2 p2 ty0 - return scope -tcPatt scope c (PM q) ty0 = do - g@(Gl gr _) <- globals - ty <- case lookupResType gr q of - Ok ty -> return ty - Bad msg -> evalError (pp msg) - case ty of - EPattType ty - -> do unify scope ty0 (eval g [] c ty []) - return scope - ty -> evalError ("Pattern type expected but " <+> pp ty <+> " found.") -tcPatt scope c p ty = unimplemented ("tcPatt "++show p) - -inferRecFields scope c rs = - mapCM (\c (l,r) -> tcRecField scope c l r Nothing) c rs - -checkRecFields scope c [] ltys - | null ltys = return [] - | otherwise = evalError ("Missing fields:" <+> hsep (map fst ltys)) -checkRecFields scope c ((l,t):lts) ltys = - case takeIt l ltys of - (Just ty,ltys) -> do let (c1,c2) = split c - ltty <- tcRecField scope c1 l t (Just ty) - lttys <- checkRecFields scope c2 lts ltys - return (ltty : lttys) - (Nothing,ltys) -> do evalWarn ("Discarded field:" <+> l) - let (c1,c2) = split c - ltty <- tcRecField scope c1 l t Nothing - lttys <- checkRecFields scope c2 lts ltys - return lttys -- ignore the field - where - takeIt l1 [] = (Nothing, []) - takeIt l1 (lty@(l2,ty):ltys) - | l1 == l2 = (Just ty,ltys) - | otherwise = let (mb_ty,ltys') = takeIt l1 ltys - in (mb_ty,lty:ltys') - -tcRecField scope c l (mb_ann_ty,t) mb_ty = do - (t,ty) <- case mb_ann_ty of - Just ann_ty -> do let (c1,c2,c3,c4) = split4 c - (ann_ty, _) <- tcRho scope c1 ann_ty (Just vtypeType) - g <- globals - let v_ann_ty = eval g (scopeEnv scope) c2 ann_ty [] - (t,_) <- tcRho scope c3 t (Just v_ann_ty) - instSigma scope c4 t v_ann_ty mb_ty - Nothing -> tcRho scope c t mb_ty - return (l,t,ty) - -tcRecTypeFields scope c [] mb_ty = return ([],mb_ty) -tcRecTypeFields scope c ((l,ty):rs) mb_ty = do - let (c1,c2) = split c - (ty,sort) <- tcRho scope c1 ty mb_ty - mb_ty <- case sort of - VSort s - | s == cType -> return (Just sort) - | s == cPType -> return mb_ty - VMeta _ _ -> return mb_ty - _ -> do sort <- value2termM False (scopeVars scope) sort - evalError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$ - "cannot be of type" <+> ppTerm Unqualified 0 sort) - (rs,mb_ty) <- tcRecTypeFields scope c2 rs mb_ty - return ((l,ty):rs,mb_ty) - --- | Invariant: if the third argument is (Just rho), --- then rho is in weak-prenex form -instSigma :: Scope -> Choice -> Term -> Sigma -> Maybe Rho -> EvalM (Term, Rho) -instSigma scope s t ty1 Nothing = return (t,ty1) -- INST1 -instSigma scope s t ty1 (Just ty2) = do -- INST2 - t <- subsCheckRho scope t ty1 ty2 - return (t,ty2) - --- | Invariant: the second argument is in weak-prenex form -subsCheckRho :: Scope -> Term -> Sigma -> Rho -> EvalM Term -subsCheckRho scope t (VMeta i vs1) (VMeta j vs2) - | i == j = do sequence_ (zipWith (unify scope) vs1 vs2) - return t - | otherwise = do - mv <- getMeta i - case mv of - Bound _ v1 -> do - g <- globals - subsCheckRho scope t (apply g v1 vs1) (VMeta j vs2) - Residuation scope1 (Just ctr1) -> do - g <- globals - subsCheckRho scope t (apply g ctr1 vs1) (VMeta j vs2) - Residuation scope1 Nothing -> do - mv <- getMeta j - case mv of - Bound _ v2 -> do - g <- globals - subsCheckRho scope t (VMeta i vs1) (apply g v2 vs2) - Residuation scope2 ctr2 - | m > n -> do setMeta i (Bound scope1 (VMeta j vs2)) - return t - | otherwise -> case ctr2 of - Nothing -> do setMeta j (Bound scope2 (VMeta i vs2)) - return t - Just ctr2 -> do g <- globals - subsCheckRho scope t (VMeta i vs1) (apply g ctr2 vs2) - where - m = length scope1 - n = length scope2 -subsCheckRho scope t ty1@(VMeta i vs) ty2 = do - mv <- getMeta i - case mv of - Bound _ ty1 -> do - g <- globals - subsCheckRho scope t (apply g ty1 vs) ty2 - Residuation scope' ctr -> do - occursCheck scope' i scope ty2 - ctr <- subtype scope ctr ty2 - setMeta i (Residuation scope' (Just ctr)) - return t -subsCheckRho scope t ty1 ty2@(VMeta i vs) = do - mv <- getMeta i - case mv of - Bound _ ty2 -> do - g <- globals - subsCheckRho scope t ty1 (apply g ty2 vs) - Residuation scope' ctr -> do - occursCheck scope' i scope ty1 - ctr <- supertype scope ctr ty1 - setMeta i (Residuation scope' (Just ctr)) - return t -subsCheckRho scope t (VProd Implicit x ty1 ty2) rho2 = do -- Rule SPEC - i <- newResiduation scope - g <- globals - let ty2' = case ty2 of - VClosure env c ty2 -> eval g ((x,VMeta i []):env) c ty2 [] - ty2 -> ty2 - subsCheckRho scope (App t (ImplArg (Meta i))) ty2' rho2 -subsCheckRho scope t rho1 (VProd Implicit x ty1 ty2) = do -- Rule SKOL - let v = newVar scope - ty2 <- evalCodomain scope x ty2 - t <- subsCheckRho ((v,ty1):scope) t rho1 ty2 - return (Abs Implicit v t) -subsCheckRho scope t rho1 (VProd Explicit _ a2 r2) = do -- Rule FUN - (_,_,a1,r1) <- unifyFun scope rho1 - subsCheckFun scope t a1 r1 a2 r2 -subsCheckRho scope t (VProd Explicit _ a1 r1) rho2 = do -- Rule FUN - (_,_,a2,r2) <- unifyFun scope rho2 - subsCheckFun scope t a1 r1 a2 r2 -subsCheckRho scope t rho1 (VTable p2 r2) = do -- Rule TABLE - (p1,r1) <- unifyTbl scope rho1 - subsCheckTbl scope t p1 r1 p2 r2 -subsCheckRho scope t (VTable p1 r1) rho2 = do -- Rule TABLE - (p2,r2) <- unifyTbl scope rho2 - subsCheckTbl scope t p1 r1 p2 r2 -subsCheckRho scope t (VSort s1) (VSort s2) -- Rule PTYPE - | s1 == cPType && s2 == cType = return t -subsCheckRho scope t (VApp _ p1 _) (VApp _ p2 _) -- Rule INT1 - | p1 == (cPredef,cInts) && p2 == (cPredef,cInt) = return t -subsCheckRho scope t (VApp _ p1 [VInt i]) (VApp _ p2 [VInt j]) -- Rule INT2 - | p1 == (cPredef,cInts) && p2 == (cPredef,cInts) = do - if i <= j - then return t - else evalError ("Ints" <+> i <+> "is not a subtype of" <+> "Ints" <+> j) -subsCheckRho scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do -- Rule REC - let mkAccess scope t = - case t of - ExtR t1 t2 -> do (scope,mkProj1,mkWrap1) <- mkAccess scope t1 - (scope,mkProj2,mkWrap2) <- mkAccess scope t2 - return (scope - ,\l -> mkProj2 l `mplus` mkProj1 l - ,mkWrap1 . mkWrap2 - ) - R rs -> do sequence_ [evalWarn ("Discarded field:" <+> l) | (l,_) <- rs, isNothing (lookup l rs2)] - return (scope - ,\l -> lookup l rs - ,id - ) - Vr x -> do return (scope - ,\l -> do VRecType rs <- lookup x scope - ty <- lookup l rs - return (Nothing,P t l) - ,id - ) - t -> let x = newVar scope - in return (((x,ty1):scope) - ,\l -> return (Nothing,P (Vr x) l) - ,Let (x, (Nothing, t)) - ) - - mkField scope l (mb_ty,t) ty1 ty2 = do - t <- subsCheckRho scope t ty1 ty2 - return (l, (mb_ty,t)) - - (scope,mkProj,mkWrap) <- mkAccess scope t - - let fields = [(l,ty2,lookup l rs1) | (l,ty2) <- rs2] - case [l | (l,_,Nothing) <- fields] of - [] -> return () - missing -> evalError ("In the term" <+> pp t $$ - "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]] - return (mkWrap (R rs)) -subsCheckRho scope t tau1 (VFV c (VarFree vs)) = do - tau2 <- variants c vs - subsCheckRho scope t tau1 tau2 -subsCheckRho scope t (VFV c (VarFree vs)) tau2 = do - tau1 <- variants c vs - subsCheckRho scope t tau1 tau2 -subsCheckRho scope t tau1 tau2 = do -- Rule EQ - unify scope tau1 tau2 -- Revert to ordinary unification - return t - -subsCheckFun :: Scope -> Term -> Sigma -> Value -> Sigma -> Value -> EvalM Term -subsCheckFun scope t a1 r1 a2 r2 = do - let v = newVar scope - vt <- subsCheckRho ((v,a2):scope) (Vr v) a2 a1 - g <- globals - let r1' = case r1 of - VClosure env c r1 -> eval g ((v,(VGen (length scope) [])):env) c r1 [] - r1 -> r1 - r2' = case r2 of - VClosure env c r2 -> eval g ((v,(VGen (length scope) [])):env) c r2 [] - r2 -> r2 - t <- subsCheckRho ((v,vtypeType):scope) (App t vt) r1' r2' - return (Abs Explicit v t) - -subsCheckTbl :: Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> EvalM Term -subsCheckTbl scope t p1 r1 p2 r2 = do - let x = newVar scope - xt <- subsCheckRho scope (Vr x) p2 p1 - t <- subsCheckRho ((x,vtypePType):scope) (S t xt) r1 r2 - p2 <- value2termM True (scopeVars scope) p2 - return (T (TTyped p2) [(PV x,t)]) - -subtype scope Nothing (VApp c p [VInt i]) - | p == (cPredef,cInts) = do - return (VCInts Nothing (Just i)) -subtype scope (Just (VCInts i j)) (VApp c p [VInt k]) - | p == (cPredef,cInts) = do - return (VCInts j (Just (maybe k (min k) i))) -subtype scope Nothing (VRecType ltys) = do - lctrs <- mapM (\(l,ty) -> supertype scope Nothing ty >>= \ctr -> return (l,True,ctr)) ltys - return (VCRecType lctrs) -subtype scope (Just (VCRecType lctrs)) (VRecType ltys) = do - lctrs <- foldM (\lctrs (l,ty) -> union l ty lctrs) lctrs ltys - return (VCRecType lctrs) - where - union l ty [] = do ctr <- subtype scope Nothing ty - return [(l,True,ctr)] - union l ty ((l',o,ctr):lctrs) - | l == l' = do ctr <- subtype scope (Just ctr) ty - return ((l,True,ctr):lctrs) - | otherwise = do lctrs <- union l ty lctrs - return ((l',o,ctr):lctrs) -subtype scope Nothing ty = return ty -subtype scope (Just ctr) ty = do - unify scope ctr ty - return ty - -supertype scope Nothing (VApp c p [VInt i]) - | p == (cPredef,cInts) = do - return (VCInts (Just i) Nothing) -supertype scope (Just (VCInts i j)) (VApp c p [VInt k]) - | p == (cPredef,cInts) = do - return (VCInts (Just (maybe k (max k) i)) j) -supertype scope Nothing (VRecType ltys) = do - lctrs <- mapM (\(l,ty) -> supertype scope Nothing ty >>= \ctr -> return (l,False,ctr)) ltys - return (VCRecType lctrs) -supertype scope (Just (VCRecType lctrs)) (VRecType ltys) = do - lctrs <- foldM (\lctrs (l,o,ctr) -> intersect l o ctr lctrs ltys) [] lctrs - return (VCRecType lctrs) - where - intersect l o ctr lctrs [] = return lctrs - intersect l o ctr lctrs ((l',ty):ltys2) - | l == l' = do ctr <- supertype scope (Just ctr) ty - return ((l,o,ctr):lctrs) - | otherwise = do intersect l o ctr lctrs ltys2 -supertype scope Nothing ty = return ty -supertype scope (Just ctr) ty = do - unify scope ctr ty - return ty - ------------------------------------------------------------------------ --- Unification ------------------------------------------------------------------------ - -unifyFun :: Scope -> Rho -> EvalM (BindType, Ident, Sigma, Rho) -unifyFun scope (VProd bt x arg res) = - return (bt,x,arg,res) -unifyFun scope (VFV c (VarFree vs)) = do - res <- mapM (unifyFun scope) vs - return - ( Explicit - , identW - , VFV c (VarFree [sigma | (_,_,sigma,rho) <- res]) - , VFV c (VarFree [rho | (_,_,sigma,rho) <- res]) - ) -unifyFun scope tau = do - let mk_val i = VMeta i [] - arg <- fmap mk_val $ newResiduation scope - res <- fmap mk_val $ newResiduation scope - let bt = Explicit - unify scope tau (VProd bt identW arg res) - return (bt,identW,arg,res) - -unifyTbl :: Scope -> Rho -> EvalM (Sigma, Rho) -unifyTbl scope (VTable arg res) = - return (arg,res) -unifyTbl scope tau = do - let mk_val i = VMeta i [] - arg <- fmap mk_val $ newResiduation scope - res <- fmap mk_val $ newResiduation scope - unify scope tau (VTable arg res) - return (arg,res) - -unify scope (VApp c1 f1 vs1) (VApp c2 f2 vs2) - | f1 == f2 = sequence_ (zipWith (unify scope) vs1 vs2) -unify scope (VMeta i vs1) (VMeta j vs2) - | i == j = sequence_ (zipWith (unify scope) vs1 vs2) - | otherwise = do - mv <- getMeta i - case mv of - Bound _ v1 -> do - g <- globals - unify scope (apply g v1 vs1) (VMeta j vs2) - Residuation scope1 _ -> do - mv <- getMeta j - case mv of - Bound _ v2 -> do - g <- globals - unify scope (VMeta i vs1) (apply g v2 vs2) - Residuation scope2 _ - | m > n -> setMeta i (Bound scope1 (VMeta j vs2)) - | otherwise -> setMeta j (Bound scope2 (VMeta i vs2)) - where - m = length scope1 - n = length scope2 -unify scope (VMeta i vs) v = unifyVar scope i vs v -unify scope v (VMeta i vs) = unifyVar scope i vs v -unify scope (VGen i vs1) (VGen j vs2) - | i == j = sequence_ (zipWith (unify scope) vs1 vs2) -unify scope (VProd b x d cod) (VProd b' x' d' cod') - | b == b' = do - unify scope d d' - cod <- evalCodomain scope x cod - cod' <- evalCodomain scope x' cod' - unify scope cod cod' -unify scope (VTable p1 res1) (VTable p2 res2) = do - unify scope p2 p1 - unify scope res1 res2 -unify scope (VSort s1) (VSort s2) - | s1 == s2 = return () -unify scope (VInt i) (VInt j) - | i == j = return () -unify scope (VFlt x) (VFlt y) - | x == y = return () -unify scope (VStr s1) (VStr s2) - | s1 == s2 = return () -unify scope VEmpty VEmpty = return () -unify scope v1 v2 = do - t1 <- value2termM False (scopeVars scope) v1 - t2 <- value2termM False (scopeVars scope) v2 - evalError ("Cannot unify terms:" <+> (ppTerm Unqualified 0 t1 $$ - ppTerm Unqualified 0 t2)) - - --- | Invariant: tv1 is a flexible type variable -unifyVar :: Scope -> MetaId -> [Value] -> Tau -> EvalM () -unifyVar scope metaid vs ty2 = do -- Check whether i is bound - mv <- getMeta metaid - case mv of - Bound _ ty1 -> do g <- globals - unify scope (apply g ty1 vs) ty2 - Residuation scope' _ -> do occursCheck scope' metaid scope ty2 - setMeta metaid (Bound scope' ty2) - -occursCheck scope' i0 scope v = - let m = length scope' - n = length scope - in check m n v - where - check m n (VApp c f vs) = mapM_ (check m n) vs - check m n (VMeta i vs) - | i0 == i = do ty1 <- value2termM False (scopeVars scope) (VMeta i vs) - ty2 <- value2termM False (scopeVars scope) v - evalError ("Occurs check for" <+> ppTerm Unqualified 0 ty1 <+> "in:" $$ - nest 2 (ppTerm Unqualified 0 ty2)) - | otherwise = do - s <- getMeta i - case s of - Bound _ v -> do g <- globals - check m n (apply g v vs) - _ -> mapM_ (check m n) vs - check m n (VGen i vs) - | i > m = let (v,_) = reverse scope !! i - in evalError ("Variable" <+> pp v <+> "has escaped") - | otherwise = mapM_ (check m n) vs - check m n (VClosure env c (Abs bt x t)) = do - g <- globals - check (m+1) (n+1) (eval g ((x,VGen n []):env) c t []) - check m n (VProd bt x ty1 ty2) = do - check m n ty1 - case ty2 of - VClosure env c t -> do g <- globals - check (m+1) (n+1) (eval g ((x,VGen n []):env) c t []) - _ -> check m n ty2 - check m n (VRecType as) = - mapM_ (\(lbl,v) -> check m n v) as - check m n (VR as) = - mapM_ (\(lbl,v) -> check m n v) as - check m n (VP v l vs) = - check m n v >> mapM_ (check m n) vs - check m n (VExtR v1 v2) = - check m n v1 >> check m n v2 - check m n (VTable v1 v2) = - check m n v1 >> check m n v2 - check m n (VT ty env c cs) = - check m n ty -- Traverse cs as well - check m n (VV ty cs) = - check m n ty >> mapM_ (check m n) cs - check m n (VS v1 v2 vs) = - check m n v1 >> check m n v2 >> mapM_ (check m n) vs - check m n (VSort _) = return () - check m n (VInt _) = return () - check m n (VFlt _) = return () - check m n (VStr _) = return () - check m n VEmpty = return () - check m n (VC v1 v2) = - check m n v1 >> check m n v2 - check m n (VGlue v1 v2) = - check m n v1 >> check m n v2 - check m n (VPatt _ _ _) = return () - check m n (VPattType v) = - check m n v - check m n (VFV c vs) = - mapM_ (check m n) (unvariants 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 (VStrs vs) = - mapM_ (check m n) vs - ------------------------------------------------------------------------ --- Instantiation and quantification ------------------------------------------------------------------------ - --- | Instantiate the topmost implicit arguments with metavariables -instantiate :: Scope -> Term -> Sigma -> EvalM (Term,Rho) -instantiate scope t (VProd Implicit x ty1 ty2) = do - i <- newResiduation scope - ty2 <- case ty2 of - VClosure env c ty2 -> do g <- globals - return (eval g ((x,VMeta i []):env) c ty2 []) - ty2 -> return ty2 - instantiate scope (App t (ImplArg (Meta i))) ty2 -instantiate scope t ty@(VMeta i args) = getMeta i >>= \case - Bound _ v -> instantiate scope t v - Residuation _ (Just v) -> instantiate scope t v - _ -> return (t,ty) -- We don't have enough information to try any instantiation -instantiate scope t ty = do - return (t,ty) - --- | Build fresh lambda abstractions for the topmost implicit arguments -skolemise :: Scope -> Sigma -> EvalM (Scope, Term->Term, Rho) -skolemise scope ty@(VMeta i vs) = do - mv <- getMeta i - case mv of - Residuation _ _ -> return (scope,id,ty) -- guarded constant? - Bound _ ty -> do g <- globals - skolemise scope (apply g ty vs) -skolemise scope (VProd Implicit x ty1 ty2) = do - let v = newVar scope - ty2 <- evalCodomain scope x ty2 - (scope,f,ty2) <- skolemise ((v,ty1):scope) ty2 - return (scope,Abs Implicit v . f,ty2) -skolemise scope ty = do - return (scope,id,ty) - --- | Quantify over the specified type variables (all flexible) -quantify :: Scope -> Term -> [MetaId] -> Rho -> EvalM (Term,Sigma) -quantify scope t tvs ty = do - let m = length tvs - n = length scope - (used_bndrs,ty) <- check m n [] ty - let new_bndrs = take m (allBinders \\ used_bndrs) - mapM_ (bind ([(var,VSort cType)|var <- new_bndrs]++scope)) (zip3 [0..] tvs new_bndrs) - let ty' = foldr (\ty -> VProd Implicit ty vtypeType) ty new_bndrs - return (foldr (Abs Implicit) t new_bndrs,ty') - where - bind scope (i, meta_id, name) = setMeta meta_id (Bound scope (VGen i [])) - - check m n xs (VApp c f vs) = do - (xs,vs) <- mapAccumM (check m n) xs vs - return (xs,VApp c f vs) - check m n xs (VMeta i vs) = do - s <- getMeta i - case s of - Bound _ v -> do g <- globals - check m n xs (apply g v vs) - _ -> do (xs,vs) <- mapAccumM (check m n) xs vs - return (xs,VMeta i vs) - check m n st (VGen i vs)= do - (st,vs) <- mapAccumM (check m n) st vs - return (st, VGen (m+i) vs) - check m n st (VClosure env c (Abs bt x t)) = do - (st,env) <- mapAccumM (\st (x,v) -> check m n st v >>= \(st,v) -> return (st,(x,v))) st env - return (st,VClosure env c (Abs bt x t)) - check m n xs (VProd bt x v1 v2) = do - (xs,v1) <- check m n xs v1 - case v2 of - VClosure env c t -> do (st,env) <- mapAccumM (\xs (x,tnk) -> check m n xs tnk >>= \(xs,tnk) -> return (xs,(x,tnk))) xs env - return (x:xs,VProd bt x v1 (VClosure env c t)) - v2 -> do (xs,v2) <- check m (n+1) xs v2 - return (x:xs,VProd bt x v1 v2) - check m n xs (VRecType as) = do - (xs,as) <- mapAccumM (\xs (l,v) -> check m n xs v >>= \(xs,v) -> return (xs,(l,v))) xs as - return (xs,VRecType as) - check m n xs (VR as) = do - (xs,as) <- mapAccumM (\xs (lbl,tnk) -> check m n xs tnk >>= \(xs,tnk) -> return (xs,(lbl,tnk))) xs as - return (xs,VR as) - check m n xs (VP v l vs) = do - (xs,v) <- check m n xs v - (xs,vs) <- mapAccumM (check m n) xs vs - return (xs,VP v l vs) - check m n xs (VExtR v1 v2) = do - (xs,v1) <- check m n xs v1 - (xs,v2) <- check m n xs v2 - return (xs,VExtR v1 v2) - check m n xs (VTable v1 v2) = do - (xs,v1) <- check m n xs v1 - (xs,v2) <- check m n xs v2 - return (xs,VTable v1 v2) - check m n xs (VT ty env c cs) = do - (xs,ty) <- check m n xs ty - (xs,env) <- mapAccumM (\xs (x,tnk) -> check m n xs tnk >>= \(xs,tnk) -> return (xs,(x,tnk))) xs env - return (xs,VT ty env c cs) - check m n xs (VV ty cs) = do - (xs,ty) <- check m n xs ty - (xs,cs) <- mapAccumM (check m n) xs cs - return (xs,VV ty cs) - check m n xs (VS v1 tnk vs) = do - (xs,v1) <- check m n xs v1 - (xs,tnk) <- check m n xs tnk - (xs,vs) <- mapAccumM (check m n) xs vs - return (xs,VS v1 tnk vs) - check m n xs v@(VSort _) = return (xs,v) - check m n xs v@(VInt _) = return (xs,v) - check m n xs v@(VFlt _) = return (xs,v) - check m n xs v@(VStr _) = return (xs,v) - check m n xs v@VEmpty = return (xs,v) - check m n xs (VC v1 v2) = do - (xs,v1) <- check m n xs v1 - (xs,v2) <- check m n xs v2 - return (xs,VC v1 v2) - check m n xs (VGlue v1 v2) = do - (xs,v1) <- check m n xs v1 - (xs,v2) <- check m n xs v2 - return (xs,VGlue v1 v2) - check m n xs v@(VPatt _ _ _) = return (xs,v) - check m n xs (VPattType v) = do - (xs,v) <- check m n xs v - return (xs,VPattType v) - check m n xs (VFV c (VarFree vs)) = do - (xs,vs) <- mapAccumM (check m n) xs vs - return (xs,VFV c (VarFree vs)) - check m n xs (VFV c (VarOpts nty name os)) = do - (xs,os) <- mapAccumM (\acc (lty,l,v) -> second (lty,l,) <$> check m n acc v) xs os - return (xs,VFV c (VarOpts nty name os)) - check m n xs (VAlts v vs) = do - (xs,v) <- check m n xs v - (xs,vs) <- mapAccumM (\xs (v1,v2) -> do (xs,v1) <- check m n xs v1 - (xs,v2) <- check m n xs v2 - return (xs,(v1,v2))) - xs vs - return (xs,VAlts v vs) - check m n xs (VStrs vs) = do - (xs,vs) <- mapAccumM (check m n) xs vs - return (xs,VStrs vs) - check m n xs v = unimplemented ("check "++show (ppValue Unqualified 5 v)) - - mapAccumM :: Monad m => (a -> b -> m (a,c)) -> a -> [b] -> m (a,[c]) - mapAccumM f s [] = return (s,[]) - mapAccumM f s (x:xs) = do - (s,y) <- f s x - (s,ys) <- mapAccumM f s xs - return (s,y:ys) - -allBinders :: [Ident] -- a,b,..z, a1, b1,... z1, a2, b2,... -allBinders = [ identS [x] | x <- ['a'..'z'] ] ++ - [ identS (x : show i) | i <- [1 :: Integer ..], x <- ['a'..'z']] - ------------------------------------------------------------------------ --- Helpers ------------------------------------------------------------------------ - -type Sigma = Value -type Rho = Value -- No top-level ForAll -type Tau = Value -- No ForAlls anywhere - -unimplemented str = fail ("Unimplemented: "++str) - -newVar :: Scope -> Ident -newVar scope = head [x | i <- [1..], - let x = identS ('v':show i), - isFree scope x] - where - isFree [] x = True - isFree ((y,_):scope) x = x /= y && isFree scope x - -scopeEnv scope = zipWith (\(x,ty) i -> (x,VGen i [])) (reverse scope) [0..] -scopeVars scope = map fst scope -scopeTypes scope = zipWith (\(_,ty) scope -> (scope,ty)) scope (tails scope) - --- | This function takes account of zonking, and returns a set --- (no duplicates) of unbound meta-type variables -getMetaVars :: [(Scope,Sigma)] -> EvalM [MetaId] -getMetaVars sc_tys = foldM (\acc (scope,ty) -> go acc ty) [] sc_tys - where - -- Get the MetaIds from a term; no duplicates in result - go acc (VGen i args) = foldM go acc args - go acc (VSort s) = return acc - go acc (VInt _) = return acc - go acc (VRecType as) = foldM (\acc (lbl,v) -> go acc v) acc as - go acc (VClosure _ _ _) = return acc - go acc (VProd b x v1 v2) = go acc v2 >>= \acc -> go acc v1 - go acc (VTable v1 v2) = go acc v2 >>= \acc -> go acc v1 - go acc (VMeta m args) - | m `elem` acc = return acc - | otherwise = do res <- getMeta m - case res of - Bound _ v -> go acc v - Residuation _ Nothing -> foldM go (m:acc) args - Residuation _ (Just v) -> go acc v - _ -> return acc - go acc (VApp c f args) = foldM go acc args - 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 (VCInts _ _) = return acc - go acc v = unimplemented ("go "++show (ppValue Unqualified 5 v)) - --- | Eliminate any substitutions in a term -zonkTerm :: [Ident] -> Term -> EvalM Term -zonkTerm xs (Abs b x t) = do - t <- zonkTerm (x:xs) t - return (Abs b x t) -zonkTerm xs (Prod b x t1 t2) = do - t1 <- zonkTerm xs t1 - t2 <- zonkTerm xs' t2 - return (Prod b x t1 t2) - where - xs' | x == identW = xs - | otherwise = x:xs -zonkTerm xs (Meta i) = do - st <- getMeta i - case st of - Bound _ v -> zonkTerm xs =<< value2termM False xs v - Residuation scope v -> case v of - Just v -> zonkTerm xs =<< value2termM False (map fst scope) v - Nothing -> return (Meta i) - Narrowing _ -> return (Meta i) -zonkTerm xs t = composOp (zonkTerm xs) t diff --git a/src/compiler/api/GF/Data/XML.hs b/src/compiler/api/GF/Data/XML.hs index 933dc243a..cd9b18339 100644 --- a/src/compiler/api/GF/Data/XML.hs +++ b/src/compiler/api/GF/Data/XML.hs @@ -1,11 +1,13 @@ ----------------------------------------------------------------------- + ---------------------------------------------------------------------- -- | -- Module : XML -- -- Utilities for creating XML documents. ---------------------------------------------------------------------- -module GF.Data.XML (XML(..), Attr, comments, showXMLDoc, showsXMLDoc, showsXML, bottomUpXML) where +module GF.Data.XML (XML(..), Attr, comments, showXMLDoc, showsXMLDoc, showsXML, bottomUpXML, parseXML) where +import Data.Char(isSpace) +import Numeric (readHex) import GF.Data.Utilities data XML = Data String | Tag String [Attr] [XML] | ETag String [Attr] | Comment String | Empty @@ -54,3 +56,229 @@ escape = concatMap escChar bottomUpXML :: (XML -> XML) -> XML -> XML bottomUpXML f (Tag n attrs cs) = f (Tag n attrs (map (bottomUpXML f) cs)) bottomUpXML f x = f x + + +-- Lexer ----------------------------------------------------------------------- + +type Line = Integer +type LChar = (Line,Char) +type LString = [LChar] +data Token = TokStart Line String [Attr] Bool -- is empty? + | TokEnd Line String + | TokCRef String + | TokText String + deriving Show + +tokens :: String -> [Token] +tokens = tokens' . linenumber 1 + +tokens' :: LString -> [Token] +tokens' ((_,'<') : c@(_,'!') : cs) = special c cs + +tokens' ((_,'<') : cs) = tag (dropSpace cs) -- we are being nice here +tokens' [] = [] +tokens' cs@((l,_):_) = let (as,bs) = breakn ('<' ==) cs + in map cvt (decode_text as) ++ tokens' bs + + -- XXX: Note, some of the lines might be a bit inacuarate + where cvt (TxtBit x) = TokText x + cvt (CRefBit x) = case cref_to_char x of + Just c -> TokText [c] + Nothing -> TokCRef x + + +special :: LChar -> LString -> [Token] +special _ ((_,'-') : (_,'-') : cs) = skip cs + where skip ((_,'-') : (_,'-') : (_,'>') : ds) = tokens' ds + skip (_ : ds) = skip ds + skip [] = [] -- unterminated comment + +special c ((_,'[') : (_,'C') : (_,'D') : (_,'A') : (_,'T') : (_,'A') : (_,'[') + : cs) = + let (xs,ts) = cdata cs + in TokText xs : tokens' ts + where cdata ((_,']') : (_,']') : (_,'>') : ds) = ([],ds) + cdata ((_,d) : ds) = let (xs,ys) = cdata ds in (d:xs,ys) + cdata [] = ([],[]) + +special c cs = + let (xs,ts) = munch "" 0 cs + in TokText ('<':'!':(reverse xs)) : tokens' ts + where munch acc nesting ((_,'>') : ds) + | nesting == (0::Int) = ('>':acc,ds) + | otherwise = munch ('>':acc) (nesting-1) ds + munch acc nesting ((_,'<') : ds) + = munch ('<':acc) (nesting+1) ds + munch acc n ((_,x) : ds) = munch (x:acc) n ds + munch acc _ [] = (acc,[]) -- unterminated DTD markup + +--special c cs = tag (c : cs) -- invalid specials are processed as tags + +linenumber :: Integer -> String -> LString +linenumber n s = + case s of + [] -> [] + ('\r':s') -> case s' of + ('\n':s'') -> next s'' + _ -> next s' + ('\n':s') -> next s' + (c :s') -> (n,c) : linenumber n s' + where + next s' = n' `seq` ((n,'\n'):linenumber n' s') where n' = n + 1 + + +qualName :: LString -> (String,LString) +qualName xs = breakn endName xs + where endName x = isSpace x || x == '=' || x == '>' || x == '/' + + + + + +tag :: LString -> [Token] +tag ((p,'/') : cs) = let (n,ds) = qualName (dropSpace cs) + in TokEnd p n : case (dropSpace ds) of + (_,'>') : es -> tokens' es + -- tag was not properly closed... + _ -> tokens' ds +tag [] = [] +tag cs = let (n,ds) = qualName cs + (as,b,ts) = attribs (dropSpace ds) + in TokStart (fst (head cs)) n as b : ts + +attribs :: LString -> ([Attr], Bool, [Token]) +attribs cs = case cs of + (_,'>') : ds -> ([], False, tokens' ds) + + (_,'/') : ds -> ([], True, case ds of + (_,'>') : es -> tokens' es + -- insert missing > ... + _ -> tokens' ds) + + (_,'?') : (_,'>') : ds -> ([], True, tokens' ds) + + -- doc ended within a tag.. + [] -> ([],False,[]) + + _ -> let (a,cs1) = attrib cs + (as,b,ts) = attribs cs1 + in (a:as,b,ts) + +attrib :: LString -> (Attr,LString) +attrib cs = let (ks,cs1) = qualName cs + (vs,cs2) = attr_val (dropSpace cs1) + in ((ks,decode_attr vs),dropSpace cs2) + +attr_val :: LString -> (String,LString) +attr_val ((_,'=') : cs) = string (dropSpace cs) +attr_val cs = ("",cs) + + +dropSpace :: LString -> LString +dropSpace = dropWhile (isSpace . snd) + +-- | Match the value for an attribute. For malformed XML we do +-- our best to guess the programmer's intention. +string :: LString -> (String,LString) +string ((_,'"') : cs) = break' ('"' ==) cs + +-- Allow attributes to be enclosed between ' '. +string ((_,'\'') : cs) = break' ('\'' ==) cs + +-- Allow attributes that are not enclosed by anything. +string cs = breakn eos cs + where eos x = isSpace x || x == '>' || x == '/' + + +break' :: (a -> Bool) -> [(b,a)] -> ([a],[(b,a)]) +break' p xs = let (as,bs) = breakn p xs + in (as, case bs of + [] -> [] + _ : cs -> cs) + +breakn :: (a -> Bool) -> [(b,a)] -> ([a],[(b,a)]) +breakn p l = (map snd as,bs) where (as,bs) = break (p . snd) l + + + +decode_attr :: String -> String +decode_attr cs = concatMap cvt (decode_text cs) + where cvt (TxtBit x) = x + cvt (CRefBit x) = case cref_to_char x of + Just c -> [c] + Nothing -> '&' : x ++ ";" + +data Txt = TxtBit String | CRefBit String deriving Show + +decode_text :: [Char] -> [Txt] +decode_text xs@('&' : cs) = case break (';' ==) cs of + (as,_:bs) -> CRefBit as : decode_text bs + _ -> [TxtBit xs] +decode_text [] = [] +decode_text cs = let (as,bs) = break ('&' ==) cs + in TxtBit as : decode_text bs + +cref_to_char :: [Char] -> Maybe Char +cref_to_char cs = case cs of + '#' : ds -> num_esc ds + "lt" -> Just '<' + "gt" -> Just '>' + "amp" -> Just '&' + "apos" -> Just '\'' + "quot" -> Just '"' + _ -> Nothing + +num_esc :: String -> Maybe Char +num_esc cs = case cs of + 'x' : ds -> check (readHex ds) + _ -> check (reads cs) + + where check [(n,"")] = cvt_char n + check _ = Nothing + +cvt_char :: Int -> Maybe Char +cvt_char x + | fromEnum (minBound :: Char) <= x && x <= fromEnum (maxBound::Char) + = Just (toEnum x) + | otherwise = Nothing + + +-- Parser -------------------------------------------------------------- + +-- | parseXML to a list of content chunks +parseXML :: String -> [XML] +parseXML = parse . tokens + +------------------------------------------------------------------------ + +parse :: [Token] -> [XML] +parse [] = [] +parse ts = let (es,_,ts1) = nodes [] ts + in es ++ parse ts1 + +nodes :: [String] -> [Token] -> ([XML], [String], [Token]) +nodes ps (TokCRef ref : ts) = + let (es,qs,ts1) = nodes ps ts + in (Data ref : es, qs, ts1) +nodes ps (TokText txt : ts) = + let (es,qs,ts1) = nodes ps ts + (more,es1) = case es of + Data cd : es1' -> (cd,es1') + _ -> ([],es) + in (Data (txt ++ more) : es1, qs, ts1) +nodes ps (TokStart p t as empty : ts) = (node : siblings, open, toks) + where + (node,(siblings,open,toks)) + | empty = (ETag t as, nodes ps ts) + | otherwise = let (es1,qs1,ts1) = nodes (t:ps) ts + in (Tag t as es1, + case qs1 of + [] -> nodes ps ts1 + _ : qs3 -> ([],qs3,ts1)) +nodes ps (TokEnd p t : ts) = case break (t ==) ps of + (as,_:_) -> ([],as,ts) + -- Unknown closing tag. Insert as text. + (_,[]) -> + let (es,qs,ts1) = nodes ps ts + in (Data "" : es,qs,ts1) +nodes ps [] = ([],ps,[]) diff --git a/src/compiler/api/GF/Grammar/Grammar.hs b/src/compiler/api/GF/Grammar/Grammar.hs index dda33193d..1a4f2ed3a 100644 --- a/src/compiler/api/GF/Grammar/Grammar.hs +++ b/src/compiler/api/GF/Grammar/Grammar.hs @@ -344,7 +344,6 @@ data Info = deriving Show type Type = Term -type MTyTerm = (Maybe Term, Term) type Cat = QIdent type Fun = QIdent @@ -374,7 +373,7 @@ data Term = | P Term Label -- ^ projection: @r.p@ | ExtR Term Term -- ^ extension: @R ** {x : A}@ (both types and terms) - | Opts MTyTerm [Option] -- ^ options: @options s in { e => x ; ... }@ + | Opts Term [Option] -- ^ options: @options s in { e => x ; ... }@ | Table Term Term -- ^ table type: @P => A@ | T TInfo [Case] -- ^ table: @table {p => c ; ...}@ @@ -395,12 +394,10 @@ data Term = | ELincat Ident Term -- ^ boxed linearization type of Ident | ELin Ident Term -- ^ boxed linearization of type Ident - | AdHocOverload [Term] -- ^ ad hoc overloading generated in Rename - | FV [Term] -- ^ alternatives in free variation: @variants { s ; ... }@ | Markup Ident [(Ident,Term)] [Term] - | Reset Ident (Maybe Term) Term QIdent + | Reset Ident (Maybe Term) Term (Maybe QIdent) | Alts Term [(Term, Term)] -- ^ alternatives by prefix: @pre {t ; s\/c ; ...}@ | Strs [Term] -- ^ conditioning prefix strings: @strs {s ; ...}@ @@ -467,7 +464,7 @@ type Equation = ([Patt],Term) type Labelling = (Label, Type) type Assign = (Label, (Maybe Type, Term)) -type Option = (MTyTerm, Term) +type Option = (Maybe Term, Term) type Case = (Patt, Term) --type Cases = ([Patt], Term) type LocalDef = (Ident, (Maybe Type, Term)) diff --git a/src/compiler/api/GF/Grammar/JSON.hs b/src/compiler/api/GF/Grammar/JSON.hs index ce24559bf..0ca49e15f 100644 --- a/src/compiler/api/GF/Grammar/JSON.hs +++ b/src/compiler/api/GF/Grammar/JSON.hs @@ -123,7 +123,6 @@ term2json (Glue t1 t2) = makeObj [("glue1",term2json t1),("glue2", term2json t2) term2json (EPattType t) = makeObj [("patttype",term2json t)] term2json (ELincat id t) = makeObj [("lincat",showJSON id), ("term",term2json t)] term2json (ELin id t) = makeObj [("lin",showJSON id), ("term",term2json t)] -term2json (AdHocOverload ts) = makeObj [("overloaded",showJSON (map term2json ts))] term2json (FV ts) = makeObj [("variants",showJSON (map term2json ts))] term2json (Markup tag attrs children) = makeObj [ ("tag",showJSON tag) , ("attrs",showJSON (map (\(attr,val) -> (showJSON attr,term2json val)) attrs)) @@ -175,7 +174,6 @@ json2term o = Vr <$> o!:"vr" <|> EPattType <$> o!<"patttype" <|> ELincat <$> o!:"lincat" <*> o!<"term" <|> ELin <$> o!:"lin" <*> o!<"term" - <|> AdHocOverload <$> (o!:"overloaded" >>= mapM json2term) <|> FV <$> (o!:"variants" >>= mapM json2term) <|> Markup <$> (o!:"tag") <*> (o!:"attrs" >>= mapM (\(attr,val) -> fmap ((,)attr) (json2term val))) <*> diff --git a/src/compiler/api/GF/Grammar/Lookup.hs b/src/compiler/api/GF/Grammar/Lookup.hs index c2eb5d6d1..30d581c72 100644 --- a/src/compiler/api/GF/Grammar/Lookup.hs +++ b/src/compiler/api/GF/Grammar/Lookup.hs @@ -68,7 +68,11 @@ lookupIdentInfo (m,ModPGF{mpgf=pgf}) i = Nothing -> notFound i where cnvType xs (PGF2.DTyp hypos cat es) = - appHypos hypos xs (QC (m,identS cat)) es + let t | cat == "String" = Sort cStr + | cat == "Int" = QC (cPredef,cInt) + | cat == "Float" = QC (cPredef,cFloat) + | otherwise = QC (m,identS cat) + in appHypos hypos xs t es appHypos [] xs t es = foldl (appExpr xs) t es diff --git a/src/compiler/api/GF/Grammar/Macros.hs b/src/compiler/api/GF/Grammar/Macros.hs index 526969b93..56b755178 100644 --- a/src/compiler/api/GF/Grammar/Macros.hs +++ b/src/compiler/api/GF/Grammar/Macros.hs @@ -404,6 +404,7 @@ composOp co trm = RecType r -> liftM RecType (mapPairsM co r) P t i -> liftM2 P (co t) (return i) ExtR a c -> liftM2 ExtR (co a) (co c) + Opts t os -> liftM2 Opts (co t) (mapM (\(t1,t2) -> liftM2 (,) (maybe (return Nothing) (liftM Just . co) t1) (co t2)) os) T i cc -> liftM2 (flip T) (mapPairsM co cc) (changeTableType co i) V ty vs -> liftM2 V (co ty) (mapM co vs) Let (x,(mt,a)) b -> liftM3 let' (co a) (T.mapM co mt) (co b) @@ -443,10 +444,14 @@ collectOp :: Monoid m => (Term -> m) -> Term -> m collectOp co trm = case trm of App c a -> co c <> co a Abs _ _ b -> co b + ImplArg t -> co t Prod _ _ a b -> co a <> co b + Typed a b -> co a <> co b + Example t _ -> co t S c a -> co c <> co a Table a c -> co a <> co c ExtR a c -> co a <> co c + Opts t os -> co t <> mconcatMap (\(a,b) -> maybe mempty co a <> co b) os R r -> mconcatMap (\ (_,(mt,a)) -> maybe mempty co mt <> co a) r RecType r -> mconcatMap (co . snd) r P t i -> co t @@ -455,9 +460,12 @@ collectOp co trm = case trm of Let (x,(mt,a)) b -> maybe mempty co mt <> co a <> co b C s1 s2 -> co s1 <> co s2 Glue s1 s2 -> co s1 <> co s2 + EPattType t -> co t Alts t aa -> let (x,y) = unzip aa in co t <> mconcatMap co (x <> y) FV ts -> mconcatMap co ts Strs tt -> mconcatMap co tt + ELincat _ t -> co t + ELin _ t -> co t Markup t as cs -> mconcatMap (co.snd) as <> mconcatMap co cs Reset _ ct t _-> maybe mempty co ct <> co t _ -> mempty -- covers K, Vr, Cn, Sort diff --git a/src/compiler/api/GF/Grammar/Parser.y b/src/compiler/api/GF/Grammar/Parser.y index 3e6cdfac3..b46b17a4f 100644 --- a/src/compiler/api/GF/Grammar/Parser.y +++ b/src/compiler/api/GF/Grammar/Parser.y @@ -275,10 +275,10 @@ ParamDef OperDef :: { [(Ident,Info)] } OperDef - : Posn LhsNames ':' Exp ';' Posn { [(i, info) | i <- $2, info <- mkOverload (Just (mkL $1 $6 $4)) Nothing ] } - | Posn LhsNames '=' Markup Posn { [(i, info) | i <- $2, info <- mkOverload Nothing (Just (mkL $1 $5 $4))] } - | Posn LhsName ListArg '=' Markup Posn { [(i, info) | i <- [$2], info <- mkOverload Nothing (Just (mkL $1 $6 (mkAbs $3 $5)))] } - | Posn LhsNames ':' Exp '=' Markup Posn { [(i, info) | i <- $2, info <- mkOverload (Just (mkL $1 $7 $4)) (Just (mkL $1 $7 $6))] } + : Posn LhsNames ':' Exp ';' Posn { [(i, info) | i <- $2, info <- mkOverload (Just (mkL $1 $6 $4)) Nothing ] } + | Posn LhsNames '=' Exp ';' Posn { [(i, info) | i <- $2, info <- mkOverload Nothing (Just (mkL $1 $6 $4))] } + | Posn LhsName ListArg '=' Exp ';' Posn { [(i, info) | i <- [$2], info <- mkOverload Nothing (Just (mkL $1 $7 (mkAbs $3 $5)))] } + | Posn LhsNames ':' Exp '=' Exp ';' Posn { [(i, info) | i <- $2, info <- mkOverload (Just (mkL $1 $8 $4)) (Just (mkL $1 $8 $6))] } LinDef :: { [(Ident,Info)] } LinDef @@ -452,7 +452,11 @@ Exp4 :: { Term } Exp4 : Exp4 Exp5 { App $1 $2 } | Exp4 '{' Exp '}' { App $1 (ImplArg $3) } - | 'option' Exp 'of' '{' ListOpt '}' { Opts (Nothing, $2) $5 } + | 'option' Exp 'of' '{' ListExp '}' { let toOption t = + case t of + Table x y -> (Just x, y) + y -> (Nothing, y) + in Opts $2 (map toOption $5) } | 'case' Exp 'of' '{' ListCase '}' { let annot = case $2 of Typed _ t -> TTyped t _ -> TRaw @@ -487,8 +491,7 @@ Exp6 | '{' ListLocDef '}' {% mkR $2 } | '<' ListTupleComp '>' { R (tuple2record $2) } | '<' Exp ':' Exp '>' { Typed $2 $4 } - | '[' Control '|' Tag ']' { Reset (fst $2) (snd $2) $4 undefined } - | '[' Control '|' Exp ']' { Reset (fst $2) (snd $2) $4 undefined } + | '[' Control '|' ListMarkup ']' { Reset (fst $2) (snd $2) (mkMarkup $4) Nothing } | '(' Exp ')' { $2 } ListExp :: { [Term] } @@ -609,15 +612,6 @@ ListPattTupleComp | Patt { [$1] } | Patt ',' ListPattTupleComp { $1 : $3 } -Opt :: { Option } -Opt - : '(' Exp ')' '=>' Exp { ((Nothing,$2),$5) } - -ListOpt :: { [Option] } -ListOpt - : Opt { [$1] } - | Opt ';' ListOpt { $1 : $3 } - Case :: { Case } Case : Patt '=>' Exp { ($1,$3) } @@ -720,14 +714,21 @@ ERHS3 :: { ERHS } | '(' ERHS0 ')' { $2 } NLG :: { Map.Map Ident Info } - : ListNLGDef { Map.fromList $1 } - | Posn Tag Posn { Map.singleton (identS "main") (ResOper Nothing (Just (mkL $1 $3 $2))) } - | Posn Exp Posn { Map.singleton (identS "main") (ResOper Nothing (Just (mkL $1 $3 $2))) } + : ListNLGDef { Map.fromList $1 } + | Posn Exp Posn { Map.singleton (identS "main") (ResOper Nothing (Just (mkL $1 $3 $2))) } + | Posn ListMarkup2 Posn { Map.singleton (identS "main") (ResOper Nothing (Just (mkL $1 $3 (mkMarkup $2)))) } ListNLGDef :: { [(Ident,Info)] } ListNLGDef - : {- empty -} { [] } - | 'oper' OperDef ListNLGDef { $2 ++ $3 } + : 'oper' NLGDef { $2 } + | 'oper' NLGDef ListNLGDef { $2 ++ $3 } + +NLGDef :: { [(Ident,Info)] } +NLGDef + : Posn LhsNames ':' Exp ';' Posn { [(i, info) | i <- $2, info <- mkOverload (Just (mkL $1 $6 $4)) Nothing ] } + | Posn LhsNames '=' ListMarkup2 Posn { [(i, info) | i <- $2, info <- mkOverload Nothing (Just (mkL $1 $5 (mkMarkup $4)))] } + | Posn LhsName ListArg '=' ListMarkup2 Posn { [(i, info) | i <- [$2], info <- mkOverload Nothing (Just (mkL $1 $6 (mkAbs $3 (mkMarkup $5))))] } + | Posn LhsNames ':' Exp '=' ListMarkup2 Posn { [(i, info) | i <- $2, info <- mkOverload (Just (mkL $1 $7 $4)) (Just (mkL $1 $7 (mkMarkup $6)))] } Markup :: { Term } Markup @@ -746,6 +747,10 @@ ListMarkup :: { [Term] } | Exp { [$1] } | Markup ListMarkup { $1 : $2 } +ListMarkup2 :: { [Term] } + : Markup { [$1] } + | Markup ListMarkup2 { $1 : $2 } + Control :: { (Ident,Maybe Term) } : Ident { ($1, Nothing) } | Ident ':' Exp6 { ($1, Just $3) } @@ -884,4 +889,7 @@ mkAlts cs = case cs of mkL :: Posn -> Posn -> x -> L x mkL (Pn l1 _) (Pn l2 _) x = L (Local l1 l2) x +mkMarkup [t] = t +mkMarkup ts = Markup identW [] ts + } diff --git a/src/compiler/api/GF/Grammar/PatternMatch.hs b/src/compiler/api/GF/Grammar/PatternMatch.hs deleted file mode 100644 index 53a99fe56..000000000 --- a/src/compiler/api/GF/Grammar/PatternMatch.hs +++ /dev/null @@ -1,183 +0,0 @@ ----------------------------------------------------------------------- --- | --- Module : PatternMatch --- Maintainer : AR --- Stability : (stable) --- Portability : (portable) --- --- > CVS $Date: 2005/10/12 12:38:29 $ --- > CVS $Author: aarne $ --- > CVS $Revision: 1.7 $ --- --- pattern matching for both concrete and abstract syntax. AR -- 16\/6\/2003 ------------------------------------------------------------------------------ - -module GF.Grammar.PatternMatch ( - matchPattern, - testOvershadow, - findMatch - ) where - -import GF.Data.Operations -import GF.Grammar.Grammar -import GF.Infra.Ident -import GF.Grammar.Macros ---import GF.Grammar.Printer - -import Data.Maybe(fromMaybe) -import Control.Monad -import GF.Text.Pretty ---import Debug.Trace - -matchPattern :: ErrorMonad m => [(Patt,rhs)] -> Term -> m (rhs, Substitution) -matchPattern pts term = - if not (isInConstantForm term) - then raise (render ("variables occur in" <+> pp term)) - else do - term' <- mkK term - errIn (render ("trying patterns" <+> hsep (punctuate ',' (map fst pts)))) $ - findMatch [([p],t) | (p,t) <- pts] [term'] - where - -- to capture all Str with string pattern matching - mkK s = case s of - C _ _ -> do - s' <- getS s - return (K (unwords s')) - _ -> return s - - getS s = case s of - K w -> return [w] - C v w -> liftM2 (++) (getS v) (getS w) - Empty -> return [] - _ -> raise (render ("cannot get string from" <+> s)) - -testOvershadow :: ErrorMonad m => [Patt] -> [Term] -> m [Patt] -testOvershadow pts vs = do - let numpts = zip pts [0..] - let cases = [(p,EInt i) | (p,i) <- numpts] - ts <- mapM (liftM fst . matchPattern cases) vs - return [p | (p,i) <- numpts, notElem i [i | EInt i <- ts] ] - -findMatch :: ErrorMonad m => [([Patt],rhs)] -> [Term] -> m (rhs, Substitution) -findMatch cases terms = case cases of - [] -> raise (render ("no applicable case for" <+> hsep (punctuate ',' terms))) - (patts,_):_ | length patts /= length terms -> - raise (render ("wrong number of args for patterns :" <+> hsep patts <+> - "cannot take" <+> hsep terms)) - (patts,val):cc -> case mapM tryMatch (zip patts terms) of - Ok substs -> return (val, concat substs) - _ -> findMatch cc terms - -tryMatch :: (Patt, Term) -> Err [(Ident, Term)] -tryMatch (p,t) = do - t' <- termForm t - trym p t' - where - trym p t' = - case (p,t') of --- (_,(x,Typed e ty,y)) -> trym p (x,e,y) -- Add this? /TH 2013-09-05 - (_,(x,Empty,y)) -> trym p (x,K [],y) -- because "" = [""] = [] - (PW, _) -> return [] -- optimization with wildcard - (PV x,([],K s,[])) -> return [(x,words2term (words s))] - (PV x, _) -> return [(x,t)] - (PString s, ([],K i,[])) | s==i -> return [] - (PInt s, ([],EInt i,[])) | s==i -> return [] - (PFloat s,([],EFloat i,[])) | s==i -> return [] --- rounding? - (PC p pp, ([], Con f, tt)) | - p `eqStrIdent` f && length pp == length tt -> - do matches <- mapM tryMatch (zip pp tt) - return (concat matches) - - (PP (q,p) pp, ([], QC (r,f), tt)) | - -- q `eqStrIdent` r && --- not for inherited AR 10/10/2005 - p `eqStrIdent` f && length pp == length tt -> - do matches <- mapM tryMatch (zip pp tt) - return (concat matches) - ---- hack for AppPredef bug - (PP (q,p) pp, ([], Q (r,f), tt)) | - -- q `eqStrIdent` r && --- - p `eqStrIdent` f && length pp == length tt -> - do matches <- mapM tryMatch (zip pp tt) - return (concat matches) - - (PR r, ([],R r',[])) | - all (`elem` map fst r') (map fst r) -> - do matches <- mapM tryMatch - [(p,snd a) | (l,p) <- r, let Just a = lookup l r'] - return (concat matches) - (PT _ p',_) -> trym p' t' - - (PAs x p',([],K s,[])) -> do - subst <- trym p' t' - return $ (x,words2term (words s)) : subst - - (PAs x p',_) -> do - subst <- trym p' t' - return $ (x,t) : subst - - (PAlt p1 p2,_) -> checks [trym p1 t', trym p2 t'] - - (PNeg p',_) -> case tryMatch (p',t) of - Bad _ -> return [] - _ -> raise (render ("no match with negative pattern" <+> p)) - - (PSeq min1 max1 p1 min2 max2 p2, ([],K s, [])) -> matchPSeq min1 max1 p1 min2 max2 p2 s - - (PRep _ _ p1, ([],K s, [])) -> checks [ - trym (foldr (const (PSeq 0 Nothing p1 0 Nothing)) (PString "") - [1..n]) t' | n <- [0 .. length s] - ] >> - return [] - - (PChar, ([],K [_], [])) -> return [] - (PChars cs, ([],K [c], [])) | elem c cs -> return [] - - _ -> raise (render ("no match in case expr for" <+> t)) - - words2term [] = Empty - words2term [w] = K w - words2term (w:ws) = C (K w) (words2term ws) - -matchPSeq min1 max1 p1 min2 max2 p2 s = - do let n = length s - lo = min1 `max` (n-fromMaybe n max2) - hi = (n-min2) `min` (fromMaybe n max1) - cuts = [splitAt i s | i <- [lo..hi]] - matches <- checks [mapM tryMatch [(p1,K s1),(p2,K s2)] | (s1,s2) <- cuts] - return (concat matches) - -isInConstantForm :: Term -> Bool -isInConstantForm trm = case trm of - Cn _ -> True - Con _ -> True - Q _ -> True - QC _ -> True - Abs _ _ _ -> True - C c a -> isInConstantForm c && isInConstantForm a - App c a -> isInConstantForm c && isInConstantForm a - R r -> all (isInConstantForm . snd . snd) r - K _ -> True - Empty -> True - EInt _ -> True - V ty ts -> isInConstantForm ty && all isInConstantForm ts -- TH 2013-09-05 --- Typed e t-> isInConstantForm e && isInConstantForm t -- Add this? TH 2013-09-05 - - _ -> False ---- isInArgVarForm trm -{- -- unused and suspicuous, see contP in GF.Compile.Compute.Concrete instead -varsOfPatt :: Patt -> [Ident] -varsOfPatt p = case p of - PV x -> [x] - PC _ ps -> concat $ map varsOfPatt ps - PP _ ps -> concat $ map varsOfPatt ps - PR r -> concat $ map (varsOfPatt . snd) r - PT _ q -> varsOfPatt q - _ -> [] - --- | to search matching parameter combinations in tables -isMatchingForms :: [Patt] -> [Term] -> Bool -isMatchingForms ps ts = all match (zip ps ts') where - match (PC c cs, (Cn d, ds)) = c == d && isMatchingForms cs ds - match _ = True - ts' = map appForm ts - --} diff --git a/src/compiler/api/GF/Grammar/Predef.hs b/src/compiler/api/GF/Grammar/Predef.hs index 4313042fa..f807d762a 100644 --- a/src/compiler/api/GF/Grammar/Predef.hs +++ b/src/compiler/api/GF/Grammar/Predef.hs @@ -63,9 +63,15 @@ cError = identS "error" -- * Used in the delimited continuations cConcat = identS "concat" +cConcat' = identS "concat'" cOne = identS "one" +cSelect = identS "select" cDefault = identS "default" cList = identS "list" +cLen = identS "len" + +cp1 = identS "p1" +cp2 = identS "p2" -- * Hacks: dummy identifiers used in various places. -- Not very nice! diff --git a/src/compiler/api/GF/Grammar/Printer.hs b/src/compiler/api/GF/Grammar/Printer.hs index d58f19e66..9a6283e49 100644 --- a/src/compiler/api/GF/Grammar/Printer.hs +++ b/src/compiler/api/GF/Grammar/Printer.hs @@ -17,6 +17,7 @@ module GF.Grammar.Printer , ppTerm , ppPatt , ppValue + , ppBind , ppConstrs , ppQIdent , ppMeta @@ -217,12 +218,12 @@ ppTerm q d (S x y) = case x of '}' _ -> prec d 3 (hang (ppTerm q 3 x) 2 ("!" <+> ppTerm q 4 y)) ppTerm q d (ExtR x y) = prec d 3 (ppTerm q 3 x <+> "**" <+> ppTerm q 4 y) +ppTerm q d (Opts t opts) = "option" <+> ppTerm q 0 t <+>"of" <+> '{' $$ + nest 2 (vcat (punctuate ';' (map (ppOpt q) opts))) $$ + '}' ppTerm q d (App x y) = prec d 4 (ppTerm q 4 x <+> ppTerm q 5 y) ppTerm q d (V e es) = hang "table" 2 (sep [ppTerm q 6 e,brackets (fsep (punctuate ';' (map (ppTerm q 0) es)))]) -ppTerm q d (Opts (_,n) cs) = prec d 4 ("option" <+> ppTerm q 0 n <+> "of" <+> braces (fsep (punctuate ';' - (map (\((_,l),t) -> parens (ppTerm q 0 l) <+> "=>" <+> ppTerm q 0 t) cs)))) ppTerm q d (FV es) = prec d 4 ("variants" <+> braces (fsep (punctuate ';' (map (ppTerm q 0) es)))) -ppTerm q d (AdHocOverload es) = "overload" <+> braces (fsep (punctuate ';' (map (ppTerm q 0) es))) ppTerm q d (Alts e xs) = prec d 4 ("pre" <+> braces (ppTerm q 0 e <> ';' <+> fsep (punctuate ';' (map (ppAltern q) xs)))) ppTerm q d (Strs es) = "strs" <+> braces (fsep (punctuate ';' (map (ppTerm q 0) es))) ppTerm q d (EPatt _ _ p)=prec d 4 ('#' <+> ppPatt q 2 p) @@ -270,6 +271,9 @@ ppEquation q (ps,e) = hcat (map (ppPatt q 2) ps) <+> "->" <+> ppTerm q 0 e ppCase q (p,e) = ppPatt q 0 p <+> "=>" <+> ppTerm q 0 e +ppOpt q (Just p, e) = ppTerm q 0 p <+> "=>" <+> ppTerm q 0 e +ppOpt q (Nothing,e) = ppTerm q 0 e + ppControl q (id,Nothing) = pp id ppControl q (id,Just t ) = pp id <> ':' <+> ppTerm q 6 t diff --git a/src/compiler/api/GF/Interactive.hs b/src/compiler/api/GF/Interactive.hs index 80e60ef8e..895229d94 100644 --- a/src/compiler/api/GF/Interactive.hs +++ b/src/compiler/api/GF/Interactive.hs @@ -14,7 +14,8 @@ import GF.Command.Abstract import GF.Command.Parse(readCommandLine,pCommand,readTransactionCommand) import GF.Compile.Rename(renameSourceTerm) import GF.Compile.TypeCheck.Concrete(inferLType) -import GF.Compile.Compute.Concrete(normalForm,stdPredef,Globals(..)) +import qualified GF.Compile.Compute.Concrete as O(normalForm,stdPredef,Globals(..)) +import GF.Compile.Compute.Concrete2(stdPredef,Globals(..)) import GF.Compile.GeneratePMCFG(pmcfgForm,type2fields) import GF.Data.Operations (Err(..)) import GF.Data.Utilities(whenM,repeatM) @@ -317,11 +318,12 @@ transactionCommand (CreateLin opts f mb_t is_alter) pgf mb_txnid = do compileLinTerm sgr mo f mb_t ty = do (t,ty) <- case mb_t of Just t -> do t <- renameSourceTerm sgr mo (Typed t ty) - (t,ty) <- inferLType sgr [] t + let g = Gl sgr (stdPredef g) + (t,ty) <- inferLType g t return (t,ty) Nothing -> case lookupResDef sgr (mo,identS f) of Ok t -> do ty <- renameSourceTerm sgr mo ty - ty <- normalForm (Gl sgr stdPredef) ty + ty <- O.normalForm (O.Gl sgr O.stdPredef) ty return (t,ty) Bad msg -> fail msg let (ctxt,res_ty) = typeFormCnc ty @@ -344,7 +346,8 @@ transactionCommand (CreateLincat opts c mb_t) pgf mb_txnid = do compileLincatTerm sgr mo mb_t = do t <- case mb_t of Just t -> do t <- renameSourceTerm sgr mo t - (t,_) <- inferLType sgr [] t + let g = Gl sgr (stdPredef g) + (t,_) <- inferLType g t return t Nothing -> case lookupResDef sgr (mo,identS c) of Ok t -> return t diff --git a/src/compiler/api/GF/Term.hs b/src/compiler/api/GF/Term.hs index 410360ea8..0b2bd2626 100644 --- a/src/compiler/api/GF/Term.hs +++ b/src/compiler/api/GF/Term.hs @@ -9,4 +9,4 @@ module GF.Term (renameSourceTerm, import GF.Compile.Rename import GF.Compile.Compute.Concrete -import GF.Compile.TypeCheck.ConcreteNew +import GF.Compile.TypeCheck.Concrete diff --git a/src/compiler/gf-repl.hs b/src/compiler/gf-repl.hs deleted file mode 100644 index 5b890fa9e..000000000 --- a/src/compiler/gf-repl.hs +++ /dev/null @@ -1,12 +0,0 @@ -import GHC.IO.Encoding (setLocaleEncoding, utf8) - -import System.Environment (getArgs) -import GF.Compile.Repl (getReplOpts, runRepl) - -main :: IO () -main = do - setLocaleEncoding utf8 - args <- getArgs - case getReplOpts args of - Left errs -> mapM_ putStrLn errs - Right opts -> runRepl opts diff --git a/src/compiler/gf.cabal b/src/compiler/gf.cabal index e0dc76ccb..e79a7fdad 100644 --- a/src/compiler/gf.cabal +++ b/src/compiler/gf.cabal @@ -121,13 +121,11 @@ library GF.Compile.GrammarToCanonical GF.Compile.ReadFiles GF.Compile.Rename - GF.Compile.Repl GF.Compile.SubExOpt GF.Compile.Tags GF.Compile.ToAPI GF.Compile.TypeCheck.Abstract GF.Compile.TypeCheck.Concrete - GF.Compile.TypeCheck.ConcreteNew GF.Compile.TypeCheck.TC GF.Compile.Update GF.Data.BacktrackM @@ -148,7 +146,6 @@ library GF.Grammar.Lookup GF.Grammar.Macros GF.Grammar.Parser - GF.Grammar.PatternMatch GF.Grammar.Predef GF.Grammar.Printer GF.Grammar.ShowTerm @@ -240,12 +237,6 @@ executable gf build-depends: base >= 4.6 && <5, directory>=1.2, gf ghc-options: -threaded -executable gfci - main-is: gf-repl.hs - default-language: Haskell2010 - build-depends: base >= 4.6 && < 5, gf - ghc-options: -threaded - test-suite gf-tests type: exitcode-stdio-1.0 main-is: run.hs diff --git a/src/runtime/c/pgf/vector.h b/src/runtime/c/pgf/vector.h index dd86869b6..edf0fc6e5 100644 --- a/src/runtime/c/pgf/vector.h +++ b/src/runtime/c/pgf/vector.h @@ -93,8 +93,8 @@ public: iterator begin() { return iterator(ref::from_ptr(&v()->data[0])); } iterator end() { return iterator(ref::from_ptr(&v()->data[v()->len])); } - bool operator ==(vector& other) const { return offset==other.as_object(); } - bool operator !=(vector& other) const { return offset!=other.as_object(); } + bool operator ==(vector& other) const { return offset==other.offset; } + bool operator !=(vector& other) const { return offset!=other.offset; } bool operator ==(object other_offset) const { return offset==other_offset; } bool operator !=(object other_offset) const { return offset!=other_offset; } diff --git a/src/runtime/python/pypgf.c b/src/runtime/python/pypgf.c index 7e90c51ad..44f42ff22 100644 --- a/src/runtime/python/pypgf.c +++ b/src/runtime/python/pypgf.c @@ -355,6 +355,59 @@ PgfLinearizationOutputIfaceVtbl pypgf_lin_out_iface_vtbl = (void*) pypgf_lin_out_flush }; +static PyObject* +Concr_tabularLinearize(ConcrObject* self, PyObject *args) +{ + ExprObject* pyexpr; + if (!PyArg_ParseTuple(args, "O!", &pgf_ExprType, &pyexpr)) + return NULL; + + PgfExn err; + PgfText **texts = + pgf_tabular_linearize(self->grammar->db, self->concr, (PgfExpr) pyexpr, NULL, + &marshaller, &err); + if (handleError(err) != PGF_EXN_NONE) { + return NULL; + } + + if (texts == NULL) { + Py_RETURN_NONE; + } + + PyObject *res = PyList_New(0); + if (!res) + goto fail; + + while (texts[0] != NULL && texts[1] != NULL) { + PyObject* pyfield = PyUnicode_FromStringAndSize(texts[0]->text, texts[0]->size); + free(texts[0]); texts++; + if (!pyfield) + goto fail; + + PyObject* pylin = PyUnicode_FromStringAndSize(texts[0]->text, texts[0]->size); + free(texts[0]); texts++; + if (!pylin) + goto fail; + + PyObject *tup = PyTuple_New(2); + PyTuple_SetItem(tup, 0, pyfield); + PyTuple_SetItem(tup, 1, pylin); + PyList_Append(res, tup); + Py_DECREF(tup); + } + + return res; + +fail: + Py_XDECREF(res); + + while (texts[0]) { + free(texts[0]); texts++; + } + + return NULL; +} + static PyObject* Concr_bracketedLinearize(ConcrObject* self, PyObject *args) { @@ -548,10 +601,10 @@ static PyMethodDef Concr_methods[] = { }, /*{"linearizeAll", (PyCFunction)Concr_linearizeAll, METH_VARARGS | METH_KEYWORDS, "Takes an abstract tree and linearizes with all variants" - }, + },*/ {"tabularLinearize", (PyCFunction)Concr_tabularLinearize, METH_VARARGS, "Takes an abstract tree and linearizes it to a table containing all fields" - },*/ + }, {"bracketedLinearize", (PyCFunction)Concr_bracketedLinearize, METH_VARARGS, "Takes an abstract tree and linearizes it to a bracketed string" }, @@ -806,8 +859,8 @@ _collect_cats(PgfItor *fn, PgfText *key, object value, PgfExn *err) if (PyList_Append((PyObject*) clo->collection, py_name) != 0) { err->type = PGF_EXN_OTHER_ERROR; - Py_DECREF(py_name); } + Py_DECREF(py_name); } static PyObject * @@ -892,8 +945,8 @@ _collect_funs(PgfItor *fn, PgfText *key, object value, PgfExn *err) if (PyList_Append((PyObject*) clo->collection, py_name) != 0) { err->type = PGF_EXN_OTHER_ERROR; - Py_DECREF(py_name); } + Py_DECREF(py_name); } static PyObject *