1-- | 2-- Module : Cryptol.TypeCheck.AST 3-- Copyright : (c) 2013-2016 Galois, Inc. 4-- License : BSD3 5-- Maintainer : cryptol@galois.com 6-- Stability : provisional 7-- Portability : portable 8 9{-# LANGUAGE Safe #-} 10 11{-# LANGUAGE RecordWildCards #-} 12{-# LANGUAGE PatternGuards #-} 13{-# LANGUAGE FlexibleInstances, FlexibleContexts #-} 14{-# LANGUAGE DeriveAnyClass, DeriveGeneric #-} 15{-# LANGUAGE OverloadedStrings #-} 16module Cryptol.TypeCheck.AST 17 ( module Cryptol.TypeCheck.AST 18 , Name() 19 , TFun(..) 20 , Selector(..) 21 , Import(..) 22 , ImportSpec(..) 23 , ExportType(..) 24 , ExportSpec(..), isExportedBind, isExportedType 25 , Pragma(..) 26 , Fixity(..) 27 , PrimMap(..) 28 , module Cryptol.TypeCheck.Type 29 ) where 30 31import Cryptol.Parser.Position(Located,Range,HasLoc(..)) 32import Cryptol.ModuleSystem.Name 33import Cryptol.ModuleSystem.Exports(ExportSpec(..) 34 , isExportedBind, isExportedType) 35import Cryptol.Parser.AST ( Selector(..),Pragma(..) 36 , Import(..), ImportSpec(..), ExportType(..) 37 , Fixity(..)) 38import Cryptol.Utils.Ident (Ident,isInfixIdent,ModName,PrimIdent,prelPrim) 39import Cryptol.Utils.RecordMap 40import Cryptol.TypeCheck.PP 41import Cryptol.TypeCheck.Type 42 43import GHC.Generics (Generic) 44import Control.DeepSeq 45 46import Data.Map (Map) 47import qualified Data.Map as Map 48import qualified Data.IntMap as IntMap 49import Data.Text (Text) 50 51 52-- | A Cryptol module. 53data Module = Module { mName :: !ModName 54 , mExports :: ExportSpec Name 55 , mImports :: [Import] 56 57 , mTySyns :: Map Name TySyn 58 -- ^ This is just the type-level type synonyms 59 -- of a module. 60 61 , mNewtypes :: Map Name Newtype 62 , mPrimTypes :: Map Name AbstractType 63 , mParamTypes :: Map Name ModTParam 64 , mParamConstraints :: [Located Prop] 65 , mParamFuns :: Map Name ModVParam 66 , mDecls :: [DeclGroup] 67 } deriving (Show, Generic, NFData) 68 69-- | Is this a parameterized module? 70isParametrizedModule :: Module -> Bool 71isParametrizedModule m = not (null (mParamTypes m) && 72 null (mParamConstraints m) && 73 null (mParamFuns m)) 74 75-- | A type parameter of a module. 76data ModTParam = ModTParam 77 { mtpName :: Name 78 , mtpKind :: Kind 79 , mtpNumber :: !Int -- ^ The number of the parameter in the module 80 -- This is used when we move parameters from the module 81 -- level to individual declarations 82 -- (type synonyms in particular) 83 , mtpDoc :: Maybe Text 84 } deriving (Show,Generic,NFData) 85 86mtpParam :: ModTParam -> TParam 87mtpParam mtp = TParam { tpUnique = nameUnique (mtpName mtp) 88 , tpKind = mtpKind mtp 89 , tpFlav = TPModParam (mtpName mtp) 90 , tpInfo = desc 91 } 92 where desc = TVarInfo { tvarDesc = TVFromModParam (mtpName mtp) 93 , tvarSource = nameLoc (mtpName mtp) 94 } 95 96-- | A value parameter of a module. 97data ModVParam = ModVParam 98 { mvpName :: Name 99 , mvpType :: Schema 100 , mvpDoc :: Maybe Text 101 , mvpFixity :: Maybe Fixity 102 } deriving (Show,Generic,NFData) 103 104 105data Expr = EList [Expr] Type -- ^ List value (with type of elements) 106 | ETuple [Expr] -- ^ Tuple value 107 | ERec (RecordMap Ident Expr) -- ^ Record value 108 | ESel Expr Selector -- ^ Elimination for tuple/record/list 109 | ESet Type Expr Selector Expr -- ^ Change the value of a field. 110 -- The included type gives the type of the record being updated 111 112 | EIf Expr Expr Expr -- ^ If-then-else 113 | EComp Type Type Expr [[Match]] 114 -- ^ List comprehensions 115 -- The types cache the length of the 116 -- sequence and its element type. 117 118 | EVar Name -- ^ Use of a bound variable 119 120 | ETAbs TParam Expr -- ^ Function Value 121 | ETApp Expr Type -- ^ Type application 122 123 | EApp Expr Expr -- ^ Function application 124 | EAbs Name Type Expr -- ^ Function value 125 126 127 | ELocated Range Expr -- ^ Source location information 128 129 {- | Proof abstraction. Because we don't keep proofs around 130 we don't need to name the assumption, but we still need to 131 record the assumption. The assumption is the 'Type' term, 132 which should be of kind 'KProp'. 133 -} 134 | EProofAbs {- x -} Prop Expr 135 136 {- | If @e : p => t@, then @EProofApp e : t@, 137 as long as we can prove @p@. 138 139 We don't record the actual proofs, as they are not 140 used for anything. It may be nice to keep them around 141 for sanity checking. 142 -} 143 144 | EProofApp Expr {- proof -} 145 146 | EWhere Expr [DeclGroup] 147 148 deriving (Show, Generic, NFData) 149 150 151data Match = From Name Type Type Expr 152 -- ^ Type arguments are the length and element 153 -- type of the sequence expression 154 | Let Decl 155 deriving (Show, Generic, NFData) 156 157data DeclGroup = Recursive [Decl] -- ^ Mutually recursive declarations 158 | NonRecursive Decl -- ^ Non-recursive declaration 159 deriving (Show, Generic, NFData) 160 161groupDecls :: DeclGroup -> [Decl] 162groupDecls dg = case dg of 163 Recursive ds -> ds 164 NonRecursive d -> [d] 165 166 167data Decl = Decl { dName :: !Name 168 , dSignature :: Schema 169 , dDefinition :: DeclDef 170 , dPragmas :: [Pragma] 171 , dInfix :: !Bool 172 , dFixity :: Maybe Fixity 173 , dDoc :: Maybe Text 174 } deriving (Generic, NFData, Show) 175 176data DeclDef = DPrim 177 | DExpr Expr 178 deriving (Show, Generic, NFData) 179 180 181-------------------------------------------------------------------------------- 182 183-- | Construct a primitive, given a map to the unique primitive name. 184ePrim :: PrimMap -> PrimIdent -> Expr 185ePrim pm n = EVar (lookupPrimDecl n pm) 186 187-- | Make an expression that is @error@ pre-applied to a type and a message. 188eError :: PrimMap -> Type -> String -> Expr 189eError prims t str = 190 EApp (ETApp (ETApp (ePrim prims (prelPrim "error")) t) 191 (tNum (length str))) (eString prims str) 192 193eString :: PrimMap -> String -> Expr 194eString prims str = EList (map (eChar prims) str) tChar 195 196eChar :: PrimMap -> Char -> Expr 197eChar prims c = ETApp (ETApp (ePrim prims (prelPrim "number")) (tNum v)) (tWord (tNum w)) 198 where v = fromEnum c 199 w = 8 :: Int 200 201 202instance PP (WithNames Expr) where 203 ppPrec prec (WithNames expr nm) = 204 case expr of 205 ELocated _ t -> ppWP prec t 206 207 EList [] t -> optParens (prec > 0) 208 $ text "[]" <+> colon <+> ppWP prec t 209 210 EList es _ -> brackets $ sep $ punctuate comma $ map ppW es 211 212 ETuple es -> parens $ sep $ punctuate comma $ map ppW es 213 214 ERec fs -> braces $ sep $ punctuate comma 215 [ pp f <+> text "=" <+> ppW e | (f,e) <- displayFields fs ] 216 217 ESel e sel -> ppWP 4 e <+> text "." <.> pp sel 218 219 ESet _ty e sel v -> braces (pp e <+> "|" <+> pp sel <+> "=" <+> pp v) 220 221 EIf e1 e2 e3 -> optParens (prec > 0) 222 $ sep [ text "if" <+> ppW e1 223 , text "then" <+> ppW e2 224 , text "else" <+> ppW e3 ] 225 226 EComp _ _ e mss -> let arm ms = text "|" <+> commaSep (map ppW ms) 227 in brackets $ ppW e <+> vcat (map arm mss) 228 229 EVar x -> ppPrefixName x 230 231 EAbs {} -> let (xs,e) = splitWhile splitAbs expr 232 in ppLam nm prec [] [] xs e 233 234 EProofAbs {} -> let (ps,e1) = splitWhile splitProofAbs expr 235 (xs,e2) = splitWhile splitAbs e1 236 in ppLam nm prec [] ps xs e2 237 238 ETAbs {} -> let (ts,e1) = splitWhile splitTAbs expr 239 (ps,e2) = splitWhile splitProofAbs e1 240 (xs,e3) = splitWhile splitAbs e2 241 in ppLam nm prec ts ps xs e3 242 243 -- infix applications 244 EApp (EApp (EVar o) a) b 245 | isInfixIdent (nameIdent o) -> 246 ppPrec 3 a <+> ppInfixName o <+> ppPrec 3 b 247 248 | otherwise -> 249 ppPrefixName o <+> ppPrec 3 a <+> ppPrec 3 b 250 251 EApp e1 e2 -> optParens (prec > 3) 252 $ ppWP 3 e1 <+> ppWP 4 e2 253 254 EProofApp e -> optParens (prec > 3) 255 $ ppWP 3 e <+> text "<>" 256 257 ETApp e t -> optParens (prec > 3) 258 $ ppWP 3 e <+> ppWP 5 t 259 260 EWhere e ds -> optParens (prec > 0) 261 ( ppW e $$ text "where" 262 $$ nest 2 (vcat (map ppW ds)) 263 $$ text "" ) 264 265 where 266 ppW x = ppWithNames nm x 267 ppWP x = ppWithNamesPrec nm x 268 269ppLam :: NameMap -> Int -> [TParam] -> [Prop] -> [(Name,Type)] -> Expr -> Doc 270ppLam nm prec [] [] [] e = ppWithNamesPrec nm prec e 271ppLam nm prec ts ps xs e = 272 optParens (prec > 0) $ 273 sep [ text "\\" <.> tsD <+> psD <+> xsD <+> text "->" 274 , ppWithNames ns1 e 275 ] 276 where 277 ns1 = addTNames ts nm 278 279 tsD = if null ts then empty else braces $ sep $ punctuate comma $ map ppT ts 280 psD = if null ps then empty else parens $ sep $ punctuate comma $ map ppP ps 281 xsD = if null xs then empty else sep $ map ppArg xs 282 283 ppT = ppWithNames ns1 284 ppP = ppWithNames ns1 285 ppArg (x,t) = parens (pp x <+> text ":" <+> ppWithNames ns1 t) 286 287 288splitWhile :: (a -> Maybe (b,a)) -> a -> ([b],a) 289splitWhile f e = case f e of 290 Nothing -> ([], e) 291 Just (x,e1) -> let (xs,e2) = splitWhile f e1 292 in (x:xs,e2) 293 294splitAbs :: Expr -> Maybe ((Name,Type), Expr) 295splitAbs (EAbs x t e) = Just ((x,t), e) 296splitAbs _ = Nothing 297 298splitTAbs :: Expr -> Maybe (TParam, Expr) 299splitTAbs (ETAbs t e) = Just (t, e) 300splitTAbs _ = Nothing 301 302splitProofAbs :: Expr -> Maybe (Prop, Expr) 303splitProofAbs (EProofAbs p e) = Just (p,e) 304splitProofAbs _ = Nothing 305 306splitTApp :: Expr -> Maybe (Type,Expr) 307splitTApp (ETApp e t) = Just (t, e) 308splitTApp _ = Nothing 309 310splitProofApp :: Expr -> Maybe ((), Expr) 311splitProofApp (EProofApp e) = Just ((), e) 312splitProofApp _ = Nothing 313 314-- | Deconstruct an expression, typically polymorphic, into 315-- the types and proofs to which it is applied. 316-- Since we don't store the proofs, we just return 317-- the number of proof applications. 318-- The first type is the one closest to the expr. 319splitExprInst :: Expr -> (Expr, [Type], Int) 320splitExprInst e = (e2, reverse ts, length ps) 321 where 322 (ps,e1) = splitWhile splitProofApp e 323 (ts,e2) = splitWhile splitTApp e1 324 325 326instance HasLoc Expr where 327 getLoc (ELocated r _) = Just r 328 getLoc _ = Nothing 329 330instance PP Expr where 331 ppPrec n t = ppWithNamesPrec IntMap.empty n t 332 333 334instance PP (WithNames Match) where 335 ppPrec _ (WithNames mat nm) = 336 case mat of 337 From x _ _ e -> pp x <+> text "<-" <+> ppWithNames nm e 338 Let d -> text "let" <+> ppWithNames nm d 339 340instance PP Match where 341 ppPrec = ppWithNamesPrec IntMap.empty 342 343instance PP (WithNames DeclGroup) where 344 ppPrec _ (WithNames dg nm) = 345 case dg of 346 Recursive ds -> text "/* Recursive */" 347 $$ vcat (map (ppWithNames nm) ds) 348 $$ text "" 349 NonRecursive d -> text "/* Not recursive */" 350 $$ ppWithNames nm d 351 $$ text "" 352 353instance PP DeclGroup where 354 ppPrec = ppWithNamesPrec IntMap.empty 355 356instance PP (WithNames Decl) where 357 ppPrec _ (WithNames Decl { .. } nm) = 358 pp dName <+> text ":" <+> ppWithNames nm dSignature $$ 359 (if null dPragmas 360 then empty 361 else text "pragmas" <+> pp dName <+> sep (map pp dPragmas) 362 ) $$ 363 pp dName <+> text "=" <+> ppWithNames nm dDefinition 364 365instance PP (WithNames DeclDef) where 366 ppPrec _ (WithNames DPrim _) = text "<primitive>" 367 ppPrec _ (WithNames (DExpr e) nm) = ppWithNames nm e 368 369instance PP Decl where 370 ppPrec = ppWithNamesPrec IntMap.empty 371 372instance PP Module where 373 ppPrec = ppWithNamesPrec IntMap.empty 374 375instance PP (WithNames Module) where 376 ppPrec _ (WithNames Module { .. } nm) = 377 text "module" <+> pp mName $$ 378 -- XXX: Print exports? 379 vcat (map pp mImports) $$ 380 -- XXX: Print tysyns 381 -- XXX: Print abstarct types/functions 382 vcat (map (ppWithNames (addTNames mps nm)) mDecls) 383 where mps = map mtpParam (Map.elems mParamTypes) 384