content: --
  -- Parser AST.
  --
  -- Copyright (C) 2014, Galois, Inc.
  -- All rights reserved.
  --
  
  module Ivory.Language.Syntax.Concrete.ParseAST where
  
  import           Data.List                               (foldl')
  import           Prelude                                 ()
  import           Prelude.Compat                          hiding (init)
  
  import           Ivory.Language.Syntax.Concrete.Location
  
  --------------------------------------------------------------------------------
  
  type FnSym     = String
  type Var       = String
  type RefVar    = String
  type IxVar     = String
  type TypeVar   = String
  type FieldNm   = String
  type MacroVar  = String
  
  --------------------------------------------------------------------------------
  
  -- Top level symbols.
  data GlobalSym = GlobalProc       ProcDef
                 | GlobalInclProc   IncludeProc
                 | GlobalStruct     StructDef
                 | GlobalBitData    BitDataDef
                 | GlobalTypeDef    TypeDef
                 | GlobalConstDef   ConstDef
                 | GlobalInclude    IncludeDef
                 | GlobalExtern     Extern
                 | GlobalArea       AreaDef
                 | GlobalAreaImport AreaImportDef
    deriving (Show, Read, Eq, Ord)
  
  --------------------------------------------------------------------------------
  -- Mem Areas
  
  data AreaDef = AreaDef
    { areaConst  :: Bool
    , areaType   :: Type
    , areaInit   :: AllocRef
    , memAreaLoc :: SrcLoc
    } deriving (Show, Read, Eq, Ord)
  
  data AreaImportDef = AreaImportDef
    { aiSym   :: String
    , aiConst :: Bool
    , aiType  :: Type
    , aiFile  :: String
    , aiLoc   :: SrcLoc
    } deriving (Show, Read, Eq, Ord)
  
  --------------------------------------------------------------------------------
  -- Includes
  
  data IncludeDef = IncludeDef
    { inclModule :: String
    , inclDefLoc :: SrcLoc
    } deriving (Show, Read, Eq, Ord)
  
  --------------------------------------------------------------------------------
  -- Externs
  
  data Extern = Extern
    { externSym  :: String
    , externFile :: String
    , externType :: Type
    , externLoc  :: SrcLoc
    } deriving (Show, Read, Eq, Ord)
  
  --------------------------------------------------------------------------------
  -- Constant definition
  
  data ConstDef = ConstDef
    { constSym    :: String
    , constExp    :: Exp
    , constType   :: Maybe Type
    , constDefLoc :: SrcLoc
    } deriving (Show, Read, Eq, Ord)
  
  --------------------------------------------------------------------------------
  -- Type definition
  
  data TypeDef = TypeDef
    { tySym    :: String
    , tyDef    :: Type
    , tyDefLoc :: SrcLoc
    } deriving (Show, Read, Eq, Ord)
  
  --------------------------------------------------------------------------------
  -- Procs
  
  data ProcDef = ProcDef
    { procTy      :: Type         -- ^ Return type
    , procSym     :: FnSym        -- ^ Function name
    , procArgs    :: [(Type,Var)] -- ^ Argument types
    , procStmt    :: [Stmt]       -- ^ Body
    , procPrePost :: [PrePost]
    , procLoc     :: SrcLoc
    } deriving (Show, Read, Eq, Ord)
  
  -- | We distinguish the name used from the name imported so the same symbol can
  -- be used twice at different types. (E.g., @printf@).
  data IncludeProc = IncludeProc
    { procInclTy   :: Type         -- ^ Return type
    , procInclSym  :: FnSym        -- ^ Function name used
    , procInclArgs :: [(Type,Var)] -- ^ Argument types
  -- XXX add later
  --  , procInclPrePost :: [PrePost]
    , procIncl     :: (String, FnSym) -- ^ Header to import from and function
                                         -- name imported
    , procInclLoc  :: SrcLoc
    } deriving (Show, Read, Eq, Ord)
  
  -- Pre and post conditions
  data PrePost = PreCond  Exp
               | PostCond Exp
    deriving (Show, Read, Eq, Ord)
  
  --------------------------------------------------------------------------------
  -- Types
  
  type SzType = Either String Integer
  
  data Type
    = TyVoid                               -- ^ Unit type
    | TyInt IntSize                        -- ^ Signed ints
    | TyWord WordSize                      -- ^ Unsigned ints
    | TyBool                               -- ^ Booleans
    | TyChar                               -- ^ Characters
    | TyFloat                              -- ^ Floats
    | TyDouble                             -- ^ Doubles
    -- XXX
    -- | TyPtr Type                        -- ^ Pointers
    | TyIx Integer                         -- ^ Index type
    | TyString                             -- ^ Static strings
    | TyStored Type                        -- ^ References
    | TyStruct String                      -- ^ Structures
    | TyArray Type SzType                  -- ^ Arrays of fixed length (can be a macro or integer)
    | TyRef      Scope Type                -- ^ References
    | TyConstRef Scope Type                -- ^ Constant References
    | TySynonym String                     -- ^ Type synonym
    | LocTy (Located Type)
    deriving (Show, Read, Eq, Ord)
  
  -- Helper to put array type indexes in the right order.
  tyArray :: Type -> SzType -> [SzType] -> Type
  tyArray ty idx idxs =
    let idxs' = idxs ++ [idx] in
    let i = head idxs' in
    foldl' TyArray (TyArray ty i) (tail idxs')
  
  data Scope =
      Stack (Maybe TypeVar)
      -- ^ Stack allocated.  If no type variable is provided, a fresh one is
      -- constructed.
    | Global
    -- ^ Globally allocated
    | PolyMem (Maybe TypeVar)
    -- ^ Either allocation.  If no type variable is provided, a fresh one is
    -- constructed.
    deriving (Show, Read, Eq, Ord)
  
  data IntSize
    = Int8
    | Int16
    | Int32
    | Int64
    deriving (Show, Read, Eq, Ord)
  
  data WordSize
    = Word8
    | Word16
    | Word32
    | Word64
    deriving (Show, Read, Eq, Ord)
  
  --------------------------------------------------------------------------------
  -- Expressions
  
  data Literal
    = LitInteger Integer
    | LitFloat Double -- represents floats, too
    | LitString String
    deriving (Show, Read, Eq, Ord)
  
  data Exp
    = ExpLit Literal
    | ExpVar Var
    | ExpRet -- Used only in post-conditions
    | ExpOp ExpOp [Exp]
    | IvoryMacroExp (String,[Exp])
    | ExpDeref  Exp
    | ExpArray  Exp Exp
    | ExpStruct Exp Exp
    | ExpCall FnSym [Exp]
    | ExpAddrOf Var
    | LocExp (Located Exp)
    deriving (Show, Read, Eq, Ord)
  
  data ExpOp
    = EqOp
    | NeqOp
    | CondOp
  
    | GtOp Bool
    -- ^ True is >=, False is >
    | LtOp Bool
    -- ^ True is <=, False is <
  
    | NotOp
    | AndOp
    | OrOp
  
    | MulOp
    | AddOp
    | SubOp
    | NegateOp
    | AbsOp
    | SignumOp
  
    | DivOp
    | EucDivOp
    | ModOp
  
    | FExpOp
    | FSqrtOp
    | FLogOp
    | FPowOp
    | FSinOp
    | FTanOp
    | FCosOp
    | FAsinOp
    | FAtanOp
    | FAtan2Op
    | FAcosOp
    | FSinhOp
    | FTanhOp
    | FCoshOp
    | FAsinhOp
    | FAtanhOp
    | FAcoshOp
  
    | IsNanOp
    | IsInfOp
    | RoundFOp
    | CeilFOp
    | FloorFOp
  
    | BitAndOp
    | BitOrOp
    | BitXorOp
    | BitComplementOp
    | BitShiftLOp
    | BitShiftROp
  
    | ConstRefOp
  
    | SafeCast
    | BitCast
    | CastWith
    | TwosCompCast
    | TwosCompRep
  
    | ToIx
    | FromIx
    | IxSize
    | ArrayLen
    | SizeOf
    | NullPtr
    | RefToPtr
    | ToCArray
  
    deriving (Show, Read, Eq, Ord)
  
  data StructInit
    = Empty
    | MacroInit (String, [Exp])
    | FieldInits [(FieldNm, Exp)]
    deriving (Show, Read, Eq, Ord)
  
  data AllocRef
    = AllocBase    RefVar (Maybe Exp)
    | AllocArr     RefVar [Exp]
    | AllocStruct  RefVar StructInit
    deriving (Show, Read, Eq, Ord)
  
  allocRefVar :: AllocRef -> RefVar
  allocRefVar a =
    case a of
      AllocBase   v _ -> v
      AllocArr    v _ -> v
      AllocStruct v _ -> v
  
  -- | AST for parsing C-like statements.
  data Stmt
    = IfTE Exp [Stmt] [Stmt]
    | Assert Exp
    | Assume Exp
    | Return Exp
    | ReturnVoid
    -- Deref dereferencing is an expression in our language here.
    | Store Exp Exp
    | Assign Var Exp (Maybe Type)
    | NoBindCall Var [Exp]
    | RefCopy Exp Exp
  -- Local is AllocRef
    | AllocRef AllocRef
    | MapArr IxVar [Stmt]
    | UpTo Exp IxVar [Stmt]
    | UpFromTo Exp Exp IxVar [Stmt]
    | DownFrom Exp IxVar [Stmt]
    | DownFromTo Exp Exp IxVar [Stmt]
    | Forever [Stmt]
    | IvoryMacroStmt (Maybe Var) (String, [Exp])
    | Break
    | LocStmt (Located Stmt)
    deriving (Show, Read, Eq, Ord)
  
  --------------------------------------------------------------------------------
  -- Structs
  
  data StructDef
    = StructDef   String [Field]  SrcLoc
    | AbstractDef String FilePath SrcLoc
    | StringDef   String Integer  SrcLoc
      deriving (Show, Read, Eq, Ord)
  
  structSym :: StructDef -> String
  structSym s = case s of
    StructDef   sym _ _ -> sym
    AbstractDef sym _ _ -> sym
    StringDef   sym _ _ -> ivoryStringStructName sym
  
  ivoryStringStructName :: String -> String
  ivoryStringStructName = ("ivory_string_" ++)
  
  data Field = Field
    { fieldName :: FieldNm
    , fieldType :: Type
    , fieldLoc  :: SrcLoc
    } deriving (Show, Read, Eq, Ord)
  
  --------------------------------------------------------------------------------
  -- Bit-data
  
  -- | A "bitdata" definition.
  data BitDataDef = BitDataDef
    { defName    :: String
    , defType    :: BitTy
    , defConstrs :: [Constr]
    , bdLoc      :: SrcLoc
    } deriving (Show, Read, Eq, Ord)
  
  -- | Basic type representation allowed in bit definitions.
  data BitTy = Bit
             | Bits Integer
             | BitArray Integer BitTy
             | BitTySynonym String
             | LocBitTy (Located BitTy)
    deriving (Show, Read, Eq, Ord)
  
  -- | A constructor definition within a "bitdata".
  data Constr = Constr
    { constrName   :: String
    , constrFields :: [BitField]
    , constrLayout :: [LayoutItem]
    , constrLoc    :: SrcLoc
    } deriving (Show, Read, Eq, Ord)
  
  -- | One element of a bit data constructor layout.
  data LayoutItem = LayoutConst BitLiteral
                  | LayoutField String
    deriving (Show, Read, Eq, Ord)
  
  -- | A bit integer literal with a known or unknown size.
  data BitLiteral =
      BitLitKnown   { bitLitLen :: Integer , bitLitVal :: Integer }
    | BitLitUnknown { bitLitVal :: Integer }
   deriving (Show, Read, Eq, Ord)
  
  -- | A record-like field defined within a "bitdata" constructor.  If the name is
  -- an underscore, we name it with 'Nothing'.
  data BitField = BitField
    { bitFieldName :: Maybe String
    , bitFieldType :: BitTy
    , bitFieldLoc  :: SrcLoc
    } deriving (Show, Read, Eq, Ord)
  
  --------------------------------------------------------------------------------
  -- Instances
  
  instance HasLocation GlobalSym where
    getLoc = mempty
    stripLoc g = case g of
      GlobalProc p       -> GlobalProc       (stripLoc p)
      GlobalInclProc p   -> GlobalInclProc   (stripLoc p)
      GlobalStruct s     -> GlobalStruct     (stripLoc s)
      GlobalBitData b    -> GlobalBitData    (stripLoc b)
      GlobalTypeDef t    -> GlobalTypeDef    (stripLoc t)
      GlobalConstDef c   -> GlobalConstDef   (stripLoc c)
      GlobalInclude i    -> GlobalInclude    (stripLoc i)
      GlobalExtern e     -> GlobalExtern     (stripLoc e)
      GlobalArea   a     -> GlobalArea       (stripLoc a)
      GlobalAreaImport a -> GlobalAreaImport (stripLoc a)
  
  instance HasLocation IncludeDef where
    getLoc = inclDefLoc
    stripLoc incl = incl { inclDefLoc = mempty }
  
  instance HasLocation IncludeProc where
    getLoc = procInclLoc
    stripLoc incl = incl { procInclLoc = mempty }
  
  instance HasLocation Extern where
    getLoc = externLoc
    stripLoc e = e { externLoc = mempty }
  
  instance HasLocation ConstDef where
    getLoc = constDefLoc
    stripLoc c = c { constDefLoc = mempty }
  
  instance HasLocation TypeDef where
    getLoc = tyDefLoc
    stripLoc td = td { tyDefLoc = mempty }
  
  instance HasLocation ProcDef where
    getLoc = procLoc
    stripLoc p = p { procLoc = mempty }
  
  instance HasLocation PrePost where
    getLoc _ = mempty
    stripLoc pp = case pp of
      PreCond e  -> PreCond (stripLoc e)
      PostCond e -> PostCond (stripLoc e)
  
  instance HasLocation AreaDef where
    getLoc _ = mempty
    stripLoc p = p { memAreaLoc = mempty }
  
  instance HasLocation AreaImportDef where
      getLoc _ = mempty
      stripLoc p = p { aiLoc = mempty }
  
  instance HasLocation Type where
    getLoc ty = case ty of
                  LocTy t -> getLoc t
                  _       -> mempty
    stripLoc ty = case ty of
      TyVoid{}         -> ty
      TyInt{}          -> ty
      TyWord{}         -> ty
      TyBool{}         -> ty
      TyChar{}         -> ty
      TyFloat{}        -> ty
      TyDouble{}       -> ty
      TyString{}       -> ty
      TyIx{}           -> ty
      TyStored ty0     -> TyStored (stripLoc ty0)
      TyStruct{}       -> ty
      TyArray ty0 i    -> TyArray (stripLoc ty0) i
      TyRef s ty0      -> TyRef s (stripLoc ty0)
      TyConstRef s ty0 -> TyConstRef s (stripLoc ty0)
      TySynonym{}      -> ty
      LocTy ty0        -> unLoc ty0
  
  instance HasLocation Exp where
    getLoc e = case e of
                 LocExp le -> getLoc le
                 _         -> mempty
  
    stripLoc e = case e of
      ExpLit{}               -> e
      ExpVar{}               -> e
      ExpRet{}               -> e
      ExpOp op args          -> ExpOp op (stripLoc args)
      IvoryMacroExp (s,args) -> IvoryMacroExp (s, stripLoc args)
      ExpDeref e0            -> ExpDeref (stripLoc e0)
      ExpArray e0 e1         -> ExpArray (stripLoc e0) (stripLoc e1)
      ExpStruct e0 e1        -> ExpStruct (stripLoc e0) (stripLoc e1)
      ExpCall fn args        -> ExpCall fn (stripLoc args)
      ExpAddrOf{}            -> e
      LocExp le              -> unLoc le
  
  instance HasLocation AllocRef where
    getLoc _ = mempty
    stripLoc a = case a of
      AllocBase v e      -> AllocBase   v (stripLoc e)
      AllocArr v es      -> AllocArr    v (stripLoc es)
      AllocStruct v init -> AllocStruct v (stripLoc init)
  
  instance HasLocation StructInit where
    getLoc _ = mempty
    stripLoc init = case init of
      Empty             -> Empty
      MacroInit (fn,es) -> MacroInit (fn, map stripLoc es)
      FieldInits fs     -> FieldInits (map (\(n,e) -> (n, stripLoc e)) fs)
  
  instance HasLocation Stmt where
    getLoc s = case s of
                 LocStmt s0 -> getLoc s0
                 _          -> mempty
    stripLoc s = case s of
      IfTE e s0 s1             -> IfTE (stripLoc e) (stripLoc s0) (stripLoc s1)
      Assert e                 -> Assert (stripLoc e)
      Assume e                 -> Assume (stripLoc e)
      Return e                 -> Return (stripLoc e)
      ReturnVoid               -> ReturnVoid
      Break                    -> Break
      Store e0 e1              -> Store (stripLoc e0) (stripLoc e1)
      Assign v e t             -> Assign v (stripLoc e) (stripLoc t)
      NoBindCall v es          -> NoBindCall v (stripLoc es)
      RefCopy e0 e1            -> RefCopy (stripLoc e0) (stripLoc e1)
      AllocRef ar              -> AllocRef (stripLoc ar)
      MapArr v ss              -> MapArr v (stripLoc ss)
      UpTo e v ss              -> UpTo (stripLoc e) v (stripLoc ss)
      UpFromTo e0 e1 v ss      -> UpFromTo (stripLoc e0) (stripLoc e1) v (stripLoc ss)
      DownFrom e v ss          -> DownFrom (stripLoc e) v (stripLoc ss)
      DownFromTo e0 e1 v ss    -> DownFromTo (stripLoc e0) (stripLoc e1) v (stripLoc ss)
      Forever ss               -> Forever (stripLoc ss)
      IvoryMacroStmt v (s0,es) -> IvoryMacroStmt v (s0, stripLoc es)
      LocStmt s0               -> unLoc s0
  
  instance HasLocation StructDef where
    getLoc s = case s of
                 StructDef _ _   srcloc -> srcloc
                 AbstractDef _ _ srcloc -> srcloc
                 StringDef _ _   srcloc -> srcloc
    stripLoc s = case s of
      StructDef s0 fs _   -> StructDef s0 (stripLoc fs) mempty
      AbstractDef s0 fp _ -> AbstractDef s0 fp mempty
      StringDef s0 i _    -> StringDef s0 i mempty
  
  instance HasLocation Field where
    getLoc = fieldLoc
    stripLoc (Field n t _) = Field n (stripLoc t) mempty
  
  instance HasLocation BitDataDef where
    getLoc = bdLoc
    stripLoc (BitDataDef s t cs _) = BitDataDef s (stripLoc t) (stripLoc cs) mempty
  
  instance HasLocation BitTy where
    getLoc bt = case bt of
                  LocBitTy bt' -> getLoc bt'
                  _            -> mempty
    stripLoc bt = case bt of
      Bit            -> bt
      Bits{}         -> bt
      BitArray i bt0 -> BitArray i (stripLoc bt0)
      BitTySynonym{} -> bt
      LocBitTy bt0   -> unLoc bt0
  
  instance HasLocation Constr where
    getLoc = constrLoc
    stripLoc (Constr n fs l _) = Constr n (stripLoc fs) l mempty
  
  instance HasLocation BitField where
    getLoc = bitFieldLoc
    stripLoc (BitField n t _) = BitField n (stripLoc t) mempty
  