{-| ISyntax abstract syntax. Properties: * Names are unique. * Equipped with position information. CITranslate translates CSyntax.CExpr into Exp -} module ISynType where import Data.Maybe(catMaybes) import Literal(Literal) import Id(Id,UId,dummyUId,toId,toDummyUId,dummyId,SymTab) import Position(Position,noPosition) import MetaVars(MetaVar,Visibility) import CITrans(CITrans) import Util(apSnd) import Data.Map ( Map ) import PluginType --import ClassEnv data Program = Program [LetDef] data LetDef = DSimple Def | DMutual [Def] deriving (Eq,Show) -- | DOpen Exp OpenArgs -- PJ 041015: Not all [EProp] combinations are allowed (private public ??) data Def = Def Bool Bool [EProp] UId FCVars Tel Exp Drhs -- ^ REMOVE --- ^ is recursive | UnTypedDef Bool Bool [EProp] UId FCVars Drhs | DOpen Exp OpenArgs deriving (Eq,Show) data Drhs = DExp Exp | PN | Native deriving (Eq,Show) data Exp = EMeta MetaVar Position Bool TransClass Int Visibility | EMetaV MetaVar Bool FCVars TransClass | EVar UId (Maybe TransClass) | EConst UId (Maybe TransClass) | EConstV UId FCVars | ESort Position Sort | EProd Bind Exp | EArrow Bool Exp Exp -- kept for nicer pretty printing and easier to -- automatically | EAbs Bind Exp | EApp Exp [(Bool,Exp)] | EBinOp Exp Exp Exp -- EBinOp e1 op e2 | EIf Exp Exp Exp -- kept for nicer pretty printing | EDef [LetDef] Exp | EOpen Exp OpenArgs Exp | ESig Position [ESigDef] | EStruct Position [LetDef] FCVars [(Id,UId)] [UId] -- pub and abs const | EPackageType | Epackage Position [LetDef] FCVars [(Id,UId)] [UId] -- pub and abs const | EProj Exp Id | EData [ConBind] | EIndData Tel [IndConBind] -- Tel is [] when used for 1. | ECon Id [(Bool,Exp)] | EConF Id Exp [(Bool,Exp)] | ECase Exp [(CaseBranch,Exp)] | PreMeta | EStop MetaVar Exp | EClos Environment Exp | ELiteral Position Literal | EExternal (Plugin Exp TransClass) --- | EClass Position [Id] [ESigDef] --- | EInstance Position [LetDef] FCVars [UId] [UId] -- pub and abs const --- | ETheory Position [LetDef] [UId] --- | ETheoryV Position [UId] [UId] deriving (Eq,Show) type Head = Exp data ESigDef = ESigAbs Decl | ESigDefn Def deriving (Eq,Show) type Bind = ([(Bool,UId)],Exp) type Decl = Bind type Tel = [Decl] type ConBind = (Id,Tel) type IndConBind = (ConBind,[(Bool,Exp)]) --- ^ substitution from cb to tel of EIndData data PatArg = PArgT UId Exp | PArg UId deriving (Eq,Show) data CaseBranch = CBConM Id [PatArg] {- constructor name, args -} (Maybe (UId,FCVars)) {- NOW NOT USED. just Nothing. see CITranslate.hs if the cased exp is a var, its uid as a constant in this branch, and its free vars (incl. patarg) -} | CBLit Position Literal -- defunct deriving (Eq,Show) data OpenArg = OpenConst [EProp] UId | OpenConstAs [EProp] Id UId | OpenConstT [EProp] UId Exp | OpenConstAsT [EProp] Id UId Exp deriving (Eq,Show) data OpenArgs = OpenArgs [OpenArg] FCVars deriving (Eq,Show) data Sort = Sort Int deriving (Show,Eq,Ord) data EProp = Eprivate | Epublic | Eabstract | Econcrete deriving (Eq, Ord, Show) mapLetDef :: (Def -> Def) -> LetDef -> LetDef mapLetDef f (DSimple d) = DSimple (f d) mapLetDef f (DMutual ds) = DMutual (map f ds) --mapLetDef _ d = d letDefToDefList :: LetDef -> [Def] letDefToDefList (DSimple d) = [d] letDefToDefList (DMutual ds) = ds flattenLetDef :: [LetDef] -> [Def] flattenLetDef = concatMap letDefToDefList updateRhsDef :: Def -> Drhs -> Def updateRhsDef (Def blocked rec p c xs tel a _) rhs = Def blocked rec p c xs tel a rhs updateRhsDef _ _ = error "updateRhsDef: " absRhs :: Tel -> Drhs -> Drhs absRhs tel (DExp e) = DExp (eAbs tel e) absRhs _ d = d -- absRhs _ PN = PN -- absRhs _ Native = Native mkDef :: Bool -> Bool -> [EProp] -> UId -> FCVars -> Tel -> Exp -> Drhs -> Def mkEDef :: Bool -> Bool -> [EProp] -> UId -> FCVars -> Tel -> Exp -> Exp -> Def mkDef blocked rec p c xs tel a rhs = Def blocked rec p c xs tel a rhs mkEDef blocked rec p c xs tel a e = Def blocked rec p c xs tel a (DExp e) mkAbstract :: Def -> Def mkAbstract (Def blocked rec ps c xs tel a (DExp e)) = Def blocked rec ps c xs tel a PN mkAbstract (UnTypedDef blocked rec ps c xs (DExp e)) = UnTypedDef blocked rec ps c xs PN mkAbstract d = d mkUnTyped :: Bool -> Bool -> [EProp] -> UId -> FCVars -> Exp -> Def mkUnTyped blocked rec p c xs e = UnTypedDef blocked rec p c xs (DExp e) unTypeDef :: Def -> Def unTypeDef (Def blocked rec ps c xs [] a (DExp e)) = mkUnTyped blocked rec ps c xs e unTypeDef d = d mkPN :: Bool -> Bool -> [EProp] -> UId -> FCVars -> Tel -> Exp -> Def mkPN blocked rec p c xs tel a = Def blocked False p c xs tel a PN mkNative :: Bool -> Bool -> [EProp] -> UId -> FCVars -> Tel -> Exp -> Def mkNative blocked rec p c xs tel a = Def blocked False p c xs tel a Native nameOfDef :: Def -> UId nameOfDef (Def _ _ _ c _ _ _ _) = c nameOfDef (UnTypedDef _ _ _ c _ _) = c rhsOfDef :: Def -> Drhs rhsOfDef (Def _ _ _ _ _ tel _ rhs) = absRhs tel rhs rhsOfDef (UnTypedDef _ _ _ _ _ rhs) = rhs -- | Eabstract `elem` ps = PN -- | otherwise = absRhs tel rhs typeOfDef :: Def -> Exp typeOfDef (Def _ _ _ _ _ tel a _) = eProd tel a typeOfDef _ = error "typeOfDef: " telOfDef :: Def -> Tel telOfDef (Def _ _ _ _ _ tel _ _) = tel telOfDef (UnTypedDef _ _ _ _ _ _) = [] telOfDef d = error ("telOfDef") varScopeDef :: Def -> FCVars varScopeDef (Def _ _ _ _ xs _ _ _) = xs varScopeDef (UnTypedDef _ _ _ _ xs _) = xs varScopeDef (DOpen _ (OpenArgs _ xs)) = xs isRecDef :: Def -> Bool isRecDef (Def _ rec _ _ _ _ _ _) = rec isRecDef (UnTypedDef _ rec _ _ _ _ ) = rec isRecDef _ = False isBlockedDef :: Def -> Bool isBlockedDef (Def blocked _ _ _ _ _ _ _) = blocked isBlockedDef (UnTypedDef blocked _ _ _ _ _ ) = blocked isBlockedDef _ = False mkVars :: [UId] -> [Exp] mkVars xs = [EVar x Nothing | x <- xs] isVar :: Exp -> Bool isVar (EVar x _) = True isVar _ = False eType :: Position -> Exp eType p = ESort p (Sort 1) eSet :: Position -> Exp eSet p = ESort p (Sort 0) eApp' :: Exp -> [(Bool,Exp)] -> Exp eApp' e [] = e eApp' e es = eApp e es where eApp :: Exp -> [(Bool,Exp)] -> Exp eApp (EApp e es) es' = eApp e (es ++ es') eApp (ECon c es) es' = ECon c (es ++ es') eApp (EConF c e es) es' = EConF c e (es++ es') eApp e es = EApp e es eArrow :: Bool -> Exp -> Exp -> Exp eArrow h a b = EProd ([(h,toDummyUId dummyId)],a) b eAbs :: [Bind] -> Exp -> Exp eAbs [] e = e eAbs (([],_):tel) e = eAbs tel e eAbs (b:bs) e = EAbs b (eAbs bs e) eProd :: Tel -> Exp -> Exp eProd [] e = e eProd (([],_):tel) e = eProd tel e eProd (b:tel) e = EProd b (eProd tel e) eLiteral :: Literal -> Exp eLiteral l = ELiteral noPosition l expToLiteral :: Exp -> Maybe Literal expToLiteral (ELiteral _ l) = Just l expToLiteral _ = Nothing isStopped :: Exp -> Bool isStopped (EStop _ e) = True isStopped _ = False stoppedBy:: [Exp] -> Maybe MetaVar stoppedBy [] = Nothing stoppedBy (EStop m _:_) = Just m stoppedBy (_:es) = stoppedBy es initEAbs :: Decl -> Exp -> Exp initEAbs d e = EAbs d e domESigDefs :: [ESigDef] -> [UId] domESigDefs [] = [] domESigDefs (ESigAbs (xs,_):sds) = (map snd xs) ++ domESigDefs sds domESigDefs (_:sds) = domESigDefs sds typeD :: Decl -> Exp typeD (_,a) = a domTel :: Tel -> [UId] domTel tel = concatMap getVarsBind tel addBindTel :: Tel -> Decl -> Tel addBindTel tel ([],_) = tel addBindTel tel b = b:tel getUIdPatt (PArgT x _) = x getUIdPatt (PArg x ) = x getIdBr (CBConM c _ _) = c getIdBr _ = error "getIdBr: CBLit is defunct." telCB :: ConBind -> Tel telCB (_,tel) = tel idCB :: ConBind -> Id idCB (i,_) = i lookupConstr :: Id -> [ConBind] -> Maybe Tel lookupConstr c cbs = lookup c cbs getVarsBind :: Bind -> [UId] getVarsBind (hxs,_) = map snd hxs getTypeBind :: Bind -> Exp getTypeBind (_,a) = a addToSort :: Int -> Sort -> Sort addToSort n (Sort k) = Sort (n+k) idOpenArg :: OpenArg -> UId idOpenArg (OpenConst _ c) = c idOpenArg (OpenConstAs _ _ c) = c idOpenArg (OpenConstT _ c _) = c idOpenArg (OpenConstAsT _ _ c _) = c propOpenArg :: OpenArg -> [EProp] propOpenArg (OpenConst ps _) = ps propOpenArg (OpenConstAs ps _ c) = ps propOpenArg (OpenConstT ps c _) = ps propOpenArg (OpenConstAsT ps _ c _) = ps isAbstract :: Def -> Bool isAbstract (Def _ _ ps _ _ _ _ _) = Eabstract `elem` ps isAbstract (UnTypedDef _ _ ps _ _ _) = Eabstract `elem` ps isAbstract _ = False abstractLetDef :: [LetDef] -> [UId] abstractLetDef [] = [] abstractLetDef (DSimple d : ds) = abstractDef d ++ abstractLetDef ds abstractLetDef (DMutual ds : ds') = concatMap abstractDef ds ++ abstractLetDef ds' abstractDef :: Def -> [UId] abstractDef (Def _ _ ps c _ _ _ _) | Eabstract `elem` ps = [c] | otherwise = [] abstractDef (UnTypedDef _ _ ps c _ _) | Eabstract `elem` ps = [c] | otherwise = [] abstractDef (DOpen _ (OpenArgs oas _)) = catMaybes (map visibleOpenArg oas) isPrivate :: Def -> Bool isPrivate (Def _ _ ps _ _ _ _ _) = Eprivate `elem` ps isPrivate (UnTypedDef _ _ ps _ _ _) = Eprivate `elem` ps isPrivate _ = False domVisibleLetDef :: [LetDef] -> [UId] domVisibleLetDef [] = [] domVisibleLetDef (DSimple d : ds) = domVisibleDef d ++ domVisibleLetDef ds domVisibleLetDef (DMutual ds : ds') = concatMap domVisibleDef ds ++ domVisibleLetDef ds' --domVisibleLetDef (DOpen _ oas : ds) = exportConsts oas++domVisibleLetDef ds domVisibleDef :: Def -> [UId] domVisibleDef (Def _ _ ps c _ _ _ _) | Eprivate `elem` ps = [] | otherwise = [c] domVisibleDef (UnTypedDef _ _ ps c _ _) | Eprivate `elem` ps = [] | otherwise = [c] domVisibleDef (DOpen _ (OpenArgs oas _)) = catMaybes (map visibleOpenArg oas) visibleOpenArg :: OpenArg -> Maybe UId visibleOpenArg (OpenConst ps c) | Eprivate `elem` ps = Nothing | otherwise = Just c visibleOpenArg (OpenConstAs ps i c) | Eprivate `elem` ps = Nothing | otherwise = Just c visibleOpenArg (OpenConstT ps c _) | Eprivate `elem` ps = Nothing | otherwise = Just c visibleOpenArg (OpenConstAsT ps i c _) | Eprivate `elem` ps = Nothing | otherwise = Just c abstractOpenArg :: OpenArg -> Maybe UId -- used in import. abstractOpenArg (OpenConst ps c) | Eabstract `elem` ps = Just c | otherwise = Nothing abstractOpenArg (OpenConstAs ps i c) | Eabstract `elem` ps = Just c | otherwise = Nothing abstractOpenArg (OpenConstT ps c _) | Eabstract `elem` ps = Just c | otherwise = Nothing abstractOpenArg (OpenConstAsT ps i c _) | Eabstract `elem` ps = Just c | otherwise = Nothing abstractOpenArgs :: OpenArgs -> [UId] abstractOpenArgs (OpenArgs os _) = catMaybes (map abstractOpenArg os) type OpenArgG = ([EProp], {- modifieres -} Id, {- label name, default toId of the next -} UId, {- UId as a const defed by this open -} Maybe Exp) {- possibly given type -} toOpenArgG:: OpenArg -> OpenArgG toOpenArgG oa = case oa of (OpenConst ps c ) -> (ps, toId c, c, Nothing) (OpenConstAs ps n c ) -> (ps, n, c, Nothing) (OpenConstT ps c a) -> (ps, toId c, c, Just a ) (OpenConstAsT ps n c a) -> (ps, n, c, Just a ) idsDef :: Def -> [UId] idsDef (Def _ _ _ c _ _ _ _) = [c] idsDef (UnTypedDef _ _ _ c _ _) = [c] idsDef _ = [] idsLetDef :: LetDef -> [UId] idsLetDef (DSimple d) = idsDef d idsLetDef (DMutual ds) = concatMap idsDef ds {- want to put it in ISynEnv ... -} type Value = Exp -- terms of this type should only be created with the operations in Eval, -- but this invariant has been broken on some places which needs to be fixed -- Possible values are (I need to think this through CC) -- v = EVar x | ECon i [(h1,v11),...,(hn,vn) | EConF i e [(h1,v1),...,(hn,vn) | -- | EApp v [(h1,v1),...,(hn,vn) ] (where v is not a lambda) -- | EProj v n (where v is not EStructV or Eackage) -- | ELiteral | EStop m v | ESort _ _ | EPackageType -- | EClos eclos env -- eclos = EConstV c xs | Eackage _ _ _ _ _ | EStructV _ _ _ _ _ | EMetaV _ _ _ -- | EAbs _ _ | EProd _ _ -- | EData _ _ | EIndData _ _ _ | ECase _ _ | ESig _ _ newtype Environment = E (Env,[UId]) deriving (Eq,Show) -- ^^^ accessibles ... type Env = [(UId,Value)] --FiniteMap UId Value {- ---- -} type FCVars = [UId] {- Instead of backtracking in the unfold, one could instead decorate all expressions that has name equality such as data, idata and sig (+ related metas) with appropiate information so that backtracking is not needed but it still behaves as equality on name. Makoto had started this, but I took it away to do a more complete revision later (CC). -- preparing for switching among -- 1. free+cased vars (as it is now; -- inefficient for Equals) -- 2. (free,free+cased) -- 3. free vars only (with cased var as consts) {- Static context info for an ocurrence of exps -} {- Will be used in 1. equality check 2. garbage collection (retrieveEnv) 3. printing 4. solve? -} {- all those 'isProbLam' things will be decorated by this in future. I'm starting with just EIndData. -} type CtxInfo = (UId, -- of this occurrence (strange for const?) [UId], -- free vars, for 1 (4?) [UId], -- free+cased vars, for 2 (UId, -- const in whose def this occurrence is and [UId])) -- def tel vars and lambda bound vars after them, for3 getCtxOcc :: CtxInfo -> UId getCtxOcc (ou,_,_,_) = ou getCtxFV :: CtxInfo -> [UId] getCtxFV (_,xs,_,_) = xs getCtxFCV :: CtxInfo -> [UId] getCtxFCV (_,_,ys,_) = ys getCtxCCPV :: CtxInfo -> (UId,[UId]) getCtxCCPV (_,_,_,ccpvs) = ccpvs {- --- -} -} appnormalized :: Value -> (Value,[(Bool,Value)]) appnormalized (EStop _ v) = appnormalized v appnormalized (EApp h vs) = apSnd (++ vs) (appnormalized h) appnormalized (EBinOp v1 op v2) = (op,[(False,v1),(False,v2)]) appnormalized h = (h,[]) transInfoExp :: Exp -> Maybe TransClass transInfoExp (EConst _ cit) = cit transInfoExp (EVar _ cit) = cit transInfoExp (EApp h es ) = transInfoExp h transInfoExp (EBinOp _ op _) = transInfoExp op transInfoExp (EProj h n) = transInfoExp h transInfoExp (EIf e _ _ ) = transInfoExp e transInfoExp (EMeta _ _ _ cit _ _) = Just cit transInfoExp (EMetaV _ _ _ cit) = Just cit transInfoExp (EStop m e ) = transInfoExp e transInfoExp (EClos _ e) = transInfoExp e transInfoExp _ = Nothing mkHiddenBind :: Bind -> Bind mkHiddenBind (hxs,a) = ([(True,x) | (_,x) <- hxs],a) mkVisibleBind :: Bind -> Bind mkVisibleBind (hxs,a) = ([(False,x) | (_,x) <- hxs],a) {- Class environment definition -} type ClassEnv = (ClassTable,InstanceTable) initClassEnv = (initSuperClasses,initInstTable) initSuperClasses = [] initInstTable = [] type SuperClass = (UId,UId) type SuperClasses = [SuperClass] type ClassTable = [(UId,SuperClasses)] -- list of superclasses together with the "path" projections to -- reach them type InstancePath = (UId,[UId]) type InstanceInfo = (UId,InstancePath) --- ^ Class name type InstanceTable = [(UId,[InstanceInfo])] -- type name and it's instances together with the name of -- the instance type TransClass = (CITrans,ClassEnv)