content: ------------------------------------------------------------------------------
  -- Copyright 2012-2021, Microsoft Research, Daan Leijen.
  --
  -- This is free software; you can redistribute it and/or modify it under the
  -- terms of the Apache License, Version 2.0. A copy of the License can be
  -- found in the LICENSE file at the root of this distribution.
  -----------------------------------------------------------------------------
  {-
      Definition of the concrete syntax.
  -}
  -----------------------------------------------------------------------------
  module Syntax.Syntax where
  
  import Common.NamePrim( nameTrue, nameSystemCore )
  import Common.Name
  import Common.Range
  import Common.Failure( failure )
  import Common.ResumeKind
  import Common.Syntax
  import qualified Common.NameSet as S
  import Syntax.Lexeme
  
  
  
  -- | A program
  data Program t k
    = Program{ programSource :: !Source
             , programName   :: !Name
             , programNameRange :: !Range
             , programTypeDefs :: ![TypeDefGroup t k]
             , programDefs      :: !(DefGroups t)
             , programImports  :: !Imports
             , programExternals :: !Externals
             , programFixDefs :: !FixDefs
             , programDoc :: !String
             }
    deriving (Show)
  
  {--------------------------------------------------------------------------
    Some instantiations
  --------------------------------------------------------------------------}
  
  type UserProgram = Program UserType UserKind
  type UserExpr    = Expr UserType
  type UserDef     = Def UserType
  type UserDefGroup = DefGroup UserType
  type UserTypeDef = TypeDef UserType UserType UserKind
  type UserTypeDefGroup = TypeDefGroup UserType UserKind
  type UserUserCon = UserCon UserType UserType UserKind
  type UserPattern = Pattern UserType
  type UserBranch  = Branch UserType
  type UserGuard   = Guard UserType
  type UserHandlerBranch = HandlerBranch UserType
  type UserValueBinder = ValueBinder () -- (Maybe UserType)
  type UserTypeBinder = TypeBinder UserKind
  
  {--------------------------------------------------------------------------
    External definitions
  --------------------------------------------------------------------------}
  type Externals
    = [External]
  
  data External
    = External{ extName :: !Name
              , extType :: !UserType
              , extParams :: ![ParamInfo]
              , extNameRange :: !Range
              , extRange :: !Range
              , extInline :: ![(Target,ExternalCall)]  -- map: target inline
              , extVis  :: !Visibility
              , extFip  :: !Fip
              , extDoc :: !String
              }
    | ExternalImport{ extImport :: ![(Target,[(String,String)])]
                    , extRange :: !Range }
    deriving (Show)
  
  
  
  
  data ExternalCall
    = ExternalInline !String  -- inline everywhere
    | ExternalCall !String    -- create a function call
    deriving (Show)
  
  type FixDefs
    = [FixDef]
  
  data FixDef
    = FixDef{ fixName   :: !Name
            , fixFixity :: !Fixity
            , fixRange  :: !Range
            , fixVis    :: !Visibility
            }
    deriving (Show)
  
  {---------------------------------------------------------------
    Import definitions
  ---------------------------------------------------------------}
  type Imports  = [Import]
  
  -- | Import declaration
  data Import
    = Import{ importName ::  !Name        -- ^ module name
            , importFullName :: !Name     -- ^ fully qualified module name
            , importNameRange :: !Range
            , importFullNameRange :: !Range
            , importRange :: !Range       -- ^ range of the full import declaration
            , importVis   :: !Visibility  -- ^ visibility of the module
            , importOpen  :: !Bool        -- used in the IDE to make all definitions visible
            }
      deriving (Show)
  
  
  {--------------------------------------------------------------------------
    type definitions
  --------------------------------------------------------------------------}
  -- | Recursive type definition groups
  type TypeDefGroups t k
    = [TypeDefGroup t k]
  
  -- | A recursive type definition group
  data TypeDefGroup t k
    = TypeDefRec [TypeDef t t k]
    | TypeDefNonRec (TypeDef t t k)
    deriving (Show)
  
  -- | type definitions.
  data TypeDef t u k
    = Synonym { typeDefBinder :: !(TypeBinder k)
              , typeDefParams :: ![TypeBinder k]
              , typeDefSynonym :: !t
              , typeDefRange :: !Range
              , typeDefVis :: !Visibility
              , typeDefDoc :: !String
              }
    | DataType{ typeDefBinder :: !(TypeBinder k)
              , typeDefParams :: ![TypeBinder k]
              , typeDefConstrs :: ![UserCon t u k]
              , typeDefRange :: !Range
              , typeDefVis :: !Visibility
              , typeDefSort :: !DataKind
              , typeDefDef  :: !DataDef
              , typeDefEffect :: !DataEffect
              , typeDefDoc  :: !String
              }
    deriving (Show)
  
  data TypeBinder k
    = TypeBinder{ tbinderName :: !Name -- ^ name
                , tbinderKind :: !k  -- ^ kind
                , tbinderNameRange :: !Range -- ^ name range
                , tbinderRange :: !Range -- ^ total range
                }
    deriving (Show)
  
  -- | Constructor: name, existentials, type parameters, name range, total range, and visibility
  data UserCon t u k
    = UserCon { userconName :: !Name
              , userconExists :: ![TypeBinder k] -- ^ existentials
              , userconParams :: ![(Visibility,ValueBinder t (Maybe (Expr u)))]            -- ^ parameters
              , userconResult :: !(Maybe t) -- ^ used internally for limited GADT's (for now)
              , userConLazy :: !(Maybe (Fip,Expr u)) -- lazy constructor?
              , userconNameRange :: !Range       --  ^ name range
              , userconRange :: !Range           --  ^ total range
              , userconVis :: !Visibility     -- ^  visibility
              , userconDoc :: !String
              }
    deriving (Show)
  
  data UserConLazy
  
  {--------------------------------------------------------------------------
    Definitions
  --------------------------------------------------------------------------}
  -- | A list of a list of value definitions. Each element is (recursive) binding group
  type DefGroups t
    = [DefGroup t]
  
  -- | Value definitions, either recursive or a single non-recursive binding
  data DefGroup t
    = DefRec    [Def t]
    | DefNonRec (Def t)
    deriving (Show)
  
  type Defs t
    = [Def t]
  
  data ValueBinder t e
    = ValueBinder{ binderName :: !Name    -- ^ name
                 , binderType :: !t       -- ^ Type. Always present for constructors.
                 , binderExpr  :: !e      -- ^ Expression: always present for definitions as 'Expr t'
                                         -- functions and constructor parameters use 'Maybe (Expr t)' for default values.
                                         -- Pattern bindings ('PatVar') use unit '()'.
                 , binderNameRange :: !Range  -- ^ name range
                 , binderRange :: !Range      -- ^ full range
                 }
    deriving (Show)
  
  
  --  | A value or function definition
  data Def t
    = Def{ defBinder :: !(ValueBinder () (Expr t))  -- a type on the definition goes into an outer Ann node on the expression
         , defRange  :: !Range
         , defVis    :: !Visibility
         , defSort   :: !DefSort
         , defInline :: !DefInline
         , defDoc    :: !String
         }
    deriving (Show)
  
  
  defIsVal def
    = not (isDefFun (defSort def))
  
  
  guardTrue
    = Var nameTrue False rangeNull
  
  {--------------------------------------------------------------------------
    Expression
  --------------------------------------------------------------------------}
  
  -- | Expressions
  data Expr t
    = Lam    ![ValueBinder (Maybe t) (Maybe (Expr t))] !(Expr t) !Bool {-toplevel?-} !Range
    | Let    !(DefGroup t) !(Expr t)    !Range
    | Bind   !(Def t) !(Expr t)         !Range
    | App    !(Expr t) ![(Maybe (Name,Range),Expr t)] !Range
    | Var    !Name !Bool !Range -- True if the var is an op
    | Lit    !Lit
    | Ann    !(Expr t) !t !Range
    | Case   !(Expr t) ![Branch t] !Bool !Range
    | Parens !(Expr t)             !Name !String !Range  --  name and string are used for the range map
    | Inject !t !(Expr t) !Bool {-behind?-} !Range
    | Handler{ hndlrSort         :: !HandlerSort,
               hndlrScope        :: !HandlerScope,
               hndlrOverride     :: !HandlerOverride,
               hndlrAllowMask    :: !(Maybe Bool),
               hndlrEffect       :: !(Maybe t),
               hndlrLocalPars    :: ![ValueBinder (Maybe t) ()],
               hndlrInitially    :: !(Maybe (Expr t)),
               hndlrReturn       :: !(Maybe (Expr t)),
               hndlrFinally      :: !(Maybe (Expr t)),
               hndlrBranches     :: ![HandlerBranch t],
               hndlrDeclRange    :: !Range,
               hndlrRange        :: !Range
              }
    deriving (Show)
  
  data HandlerOverride
    = HandlerNoOverride | HandlerOverride
    deriving (Eq,Show)
  
  data HandlerScope
    = HandlerNoScope | HandlerScoped
    deriving (Eq, Show)
  
  data HandlerBranch t
    = HandlerBranch{ hbranchName :: !Name
                   , hbranchPars :: ![ValueBinder (Maybe t) ()]
                   , hbranchExpr :: !(Expr t)
                   , hbranchSort :: !OperationSort
                   , hbranchNameRange :: !Range
                   , hbranchPatRange  :: !Range
                   }
    deriving (Show)
  
  data Branch t
    = Branch{ branchPattern :: !(Pattern t), branchGuards :: ![Guard t] }
    deriving (Show)
  
  data Guard t
    = Guard { guardTest :: !(Expr t), guardExpr :: !(Expr t) }
    deriving (Show)
  
  -- | Patterns
  data Pattern t
    = PatWild   !Range
    | PatVar    !(ValueBinder (Maybe t) (Pattern t)) -- the binderExpr is a potential other pattern (used for "as x" bindings)
    | PatAnn    !(Pattern t) !t !Range
    | PatCon    !Name    ![(Maybe (Name,Range), Pattern t)] !Range !Range  -- name range and full range
    | PatParens !(Pattern t) !Range
    | PatLit    !Lit
    deriving (Show)
  
  -- | Literals
  data Lit
    = LitInt      !Integer   !Range
    | LitFloat    !Double  !Range
    | LitChar     !Char     !Range
    | LitString   !String !Range
    deriving (Show)
  
  litRange :: Lit -> Range
  litRange lit
    = case lit of
        LitInt _ range    -> range
        LitFloat _ range  -> range
        LitChar _ range   -> range
        LitString _ range -> range
  
  stripExpr :: Expr t -> Expr t
  stripExpr (Parens e _ _ _) = stripExpr e
  stripExpr (Ann e _ _)      = stripExpr e
  stripExpr e                = e
  
  
  
  
  {--------------------------------------------------------------------------
    types and Kinds
  --------------------------------------------------------------------------}
  type KUserTypes k
    = [KUserType k]
  
  data UserQuantifier  = QSome | QForall | QExists
  
  -- (Higher ranked) types
  data KUserType k
    = TpQuan     !UserQuantifier !(TypeBinder k) !(KUserType k) !Range
    | TpFun      ![(Name,KUserType k)] !(KUserType k) !(KUserType k) !Range
    | TpApp      !(KUserType k)  ![KUserType k] !Range
    | TpVar      !Name                  !Range
    | TpCon      !Name                  !Range
    | TpParens   !(KUserType k)         !Range
    | TpAnn      !(KUserType k)  !k
    deriving (Show)
  
  type UserType
    = KUserType UserKind
  
  
  -- | A kind
  data UserKind
    = KindCon    !Name !Range
    | KindArrow  !UserKind !UserKind
    | KindParens !UserKind !Range
    | KindNone  -- flags that there is no explicit kind annotation
    deriving (Show)
  
  
  {--------------------------------------------------------------------------
    The range of expressions/types etc. can be retrieved via "getRange"
  --------------------------------------------------------------------------}
  instance Ranged (TypeDef t u k) where
    getRange typeDef
      = typeDefRange typeDef
  
  instance Ranged t => Ranged (Def t) where
    getRange def
      = getRange (defBinder def)
  
  instance Ranged (ValueBinder t e) where
    getRange vb = binderRange vb
  
  
  instance Ranged k => Ranged (KUserType k) where
    getRange tp
      = case tp of
         TpQuan     quant tname userType range -> range
         TpFun      args effect tp r-> r
         TpApp      tp tps rng      -> rng
         TpVar      name range      -> range
         TpCon      name range      -> range
         TpParens   userTp range    -> range
         TpAnn      userTp kind -> combineRange (getRange userTp) (getRange kind)
  
  instance Ranged (TypeBinder k) where
    getRange (TypeBinder _ _ _ range) = range
  
  instance Ranged (UserCon t u k) where
    getRange (UserCon _ _ _ _ _ _ range _ _) = range
  
  instance Ranged a => Ranged [a] where
    getRange rs
      = if null rs then rangeNull else combineRange (getRange (head rs)) (getRange (last rs))
  
  instance Ranged UserKind where
    getRange kind
      = case kind of
          KindCon    name range -> range
          KindArrow  k1 k2      -> combineRange (getRange k1) (getRange k2)
          KindParens knd range  -> range
          KindNone              -> rangeNull
  
  
  instance Ranged (Expr t) where
    getRange expr
      = case expr of
          Lam    pat expr _ range -> range
          Let    defs expr range -> range
          Bind   def expr range  -> range
          App    fun exprs range -> range
          Var    name isop range -> range
          Lit    lit             -> getRange lit
          Ann    expr tp range   -> range
          Case   exprs branches _ range -> range
          Parens expr name pre range  -> range
          Handler shallow scoped override _ eff pars reinit ret final ops hrng range -> range
          Inject tp expr behind range -> range
  
  instance Ranged Lit where
    getRange lit
      = case lit of
          LitInt   num range -> range
          LitFloat num range -> range
          LitChar  chr range -> range
          LitString s range  -> range
  
  instance Ranged (Pattern t) where
    getRange pat
      = case pat of
          PatWild range           -> range
          PatVar  binder          -> getRange binder
          PatAnn  pat tp range    -> range
          PatCon  name args nameRng range -> range
          PatParens pat range     -> range
          PatLit lit              -> getRange lit
  
  instance Ranged (Branch t) where
    getRange (Branch patterns guards)
      = combineRange (getRange patterns) (getRange guards)
  
  instance Ranged (Guard t) where
    getRange (Guard guard body)
      = combineRange (getRange guard) (getRange body)
  
  instance Ranged (HandlerBranch t) where
    getRange (HandlerBranch{ hbranchPatRange=rng, hbranchExpr=expr })
      = combineRange rng (getRange expr)
  
  ---------------------------------------------------------------------------
  -- Get Name
  ---------------------------------------------------------------------------
  
  type NameRange = (Name,Range)
  
  class HasName a where
    getName :: a -> Name
    getNameRange :: a -> Range
    getRName :: a -> NameRange
  
    getRName x       = (getName x, getNameRange x)
    getNameRange x   = snd (getRName x)
    getName x        = fst (getRName x)
  
  instance HasName (Program t k) where
    getName (Program _ name _ _ _ _ _ _ _) = name
    getNameRange (Program _ _ range _ _ _ _ _ _) = range
  
  instance HasName (TypeBinder k) where
    getName (TypeBinder name kind nameRange range) = name
    getNameRange (TypeBinder name kind nameRange range) = nameRange
  
  instance HasName (UserCon t u k) where
    getName (UserCon name exist params result mbLazyExpr nameRange range _ _) = name
    getNameRange (UserCon name exist params result mbLazyExpr nameRange range _ _) = nameRange
  
  instance HasName (TypeDef t u k) where
    getRName typeDef
      = getRName (typeDefBinder typeDef)
  
  instance HasName (ValueBinder t e) where
    getRName vb = (binderName vb,binderNameRange vb)
  
  instance HasName (Def t) where
    getRName def = getRName (defBinder def)
  
  
  
  
  ---------------------------------------------------------------------------
  -- Free type variables
  ---------------------------------------------------------------------------
  class HasFreeTypeVar a where
    freeTypeVars :: a -> S.NameSet
  
  instance HasFreeTypeVar a => HasFreeTypeVar (Maybe a) where
    freeTypeVars Nothing = S.empty
    freeTypeVars (Just x) = freeTypeVars x
  
  instance HasFreeTypeVar a => HasFreeTypeVar [a] where
    freeTypeVars xs = S.unions (map freeTypeVars xs)
  
  instance HasFreeTypeVar (KUserType k) where
    freeTypeVars tp
      = case tp of
         TpQuan quant (TypeBinder name k _ _) tp _
                                        -> S.delete name (freeTypeVars tp)
         TpFun      args effect tp rng  -> freeTypeVars (tp:effect:map snd args)
         TpApp      tp args range       -> S.union (freeTypeVars tp) (freeTypeVars args)
         TpVar      name range          -> S.singleton name
         TpCon      name range          -> S.empty
         TpParens   tp range            -> freeTypeVars tp
         TpAnn      tp kind             -> freeTypeVars tp
  
  instance HasFreeTypeVar a => HasFreeTypeVar (Either a b) where
    freeTypeVars (Left x) = freeTypeVars x
    freeTypeVars (Right y) = S.empty
  
  {--------------------------------------------------------------------------
    Access definitions
  --------------------------------------------------------------------------}
  defBody :: Def t -> Expr t
  defBody def  = binderExpr (defBinder def)
  
  defName :: Def t -> Name
  defName def  = binderName (defBinder def)
  
  defType :: Def t -> Maybe t
  defType def
    = case binderExpr (defBinder def) of
        Ann _ tp _ -> Just tp
        _          -> Nothing
  
  
  typeDefName typeDef
    = tbinderName (typeDefBinder typeDef)
  
  typeDefNameRange typeDef
    = getRange (typeDefBinder typeDef)
  
  
  programNull :: Name -> Program t k
  programNull name = Program sourceNull name rangeNull [] [] [preludeImport] [] [] ""
  
  -- | Import declaration for the standard prelude
  preludeImport :: Import
  preludeImport
    = Import nameSystemCore nameSystemCore rangeNull rangeNull rangeNull Private False
  
  makeProgram :: Name -> [TypeDef t t k] -> (Defs t) -> Program t k
  makeProgram name typedefs defs
    = Program sourceNull name rangeNull [TypeDefRec typedefs] [DefRec defs] [] [] [] ""
  
  programAddImports :: Program t k -> [Import] -> Program t k
  programAddImports program imports
    = program{ programImports = (programImports program) ++ imports }
  
  programAddDefs :: Program t k -> [TypeDef t t k] -> (Defs t) -> Program t k
  programAddDefs (Program source modName nameRange tdefs defs imports externals fixDefs doc) ts1 ds1
    = Program source modName nameRange
      (case tdefs of
         []                -> [TypeDefRec (ts1)]
         [TypeDefRec ts]   -> [TypeDefRec (removeTDefs ts ts1 ++ ts1)]
         _                 -> failure "Syntax.Syntax: can not add type definitions to processed tree")
      (case defs of
         []          -> [DefRec (ds1)]
         [DefRec ds] -> [DefRec (removeDefs ds ds1 ++ ds1)]
         _           -> failure "Syntax.Syntax: can not add definitions to processed tree")
      imports
      externals
      fixDefs
      doc
    where
      removeTDefs tdefs ts
        = foldl removeTDef tdefs ts
  
      removeTDef tdefs tdef
        = filter (\t -> typeDefName tdef /= typeDefName t) tdefs
  
      removeDefs defs ds
        = foldl removeDef defs ds
  
      removeDef defs def
        = filter (\d -> defName def /= defName d) defs
  
  
  programRemoveAllDefs :: Program t k -> Program t k
  programRemoveAllDefs program
    = program{ programDefs = [] }
  
  programRemoveDef :: Name -> Program t k -> Program t k
  programRemoveDef name (Program source modName nameRange tdefs defs imports ext fixDefs doc)
    = Program source modName nameRange (map filterTDef tdefs) (map filterDef defs) imports ext fixDefs doc
    where
      filterTDef  (TypeDefRec ts)    = TypeDefRec (filter (neqName . typeDefName) ts)
      filterTDef  (TypeDefNonRec t)  = if (neqName (typeDefName t)) then TypeDefNonRec t else TypeDefRec []
  
      filterDef   (DefRec ds)        = DefRec (filter (neqName . defName) ds)
      filterDef   (DefNonRec d)      = if neqName (defName d)
                                        then DefNonRec d
                                        else DefRec []
  
      neqName n  = (n /= name)
  
  
  programFind :: Ranged t => Name -> Program t k -> Maybe Range
  programFind name (Program source modName nameRange tdefs defs imports ext fixDefs doc)
    = lookup name (concatMap trange tdefs ++ concatMap drange defs)
    where
      trange (TypeDefRec ts)    = [(typeDefName t, getRange t) | t <- ts]
      trange (TypeDefNonRec td) = [(typeDefName t, getRange t) | t <- [td]]
  
      drange (DefRec ds)        = [(defName d, getRange d) | d <- ds]
      drange (DefNonRec def)    = [(defName d, getRange d) | d <- [def]]
  
  
  instance Show UserQuantifier where
    show QSome
      = "some"
    show QForall
      = "forall"
    show QExists
      = "exists"
  