content: -- |
  -- Module      : Minigent.Syntax
  -- Copyright   : (c) Data61 2018-2019
  --                   Commonwealth Science and Research Organisation (CSIRO)
  --                   ABN 41 687 119 230
  -- License     : BSD3
  --
  -- Contains type definitions for all the syntax used in the compiler:
  -- for types, expressions, constraints and so on.
  --
  -- It expects to be imported unqualified.
  {-# LANGUAGE PatternSynonyms #-}
  module Minigent.Syntax
    ( -- * Names
      -- | All names in the syntax tree are represented with 'String'.
      VarName
    , FunName
    , ConName
    , RecParName
    , AbsTypeName
    , FieldName
    , -- * Types
      Type (..)
    , Sigil (..)
    , RecContext
    , RecPar (..)
    , PrimType (..)
    , -- ** Entries and Rows
      Row (..)
    , Entry (..)
    , Taken
    , -- * Constraints
      Constraint (..)
    , pattern (:>)
    , -- * Assertions
      Assertion (..)
    , -- * Expressions
      Expr (..)
    , Op (..)
    , PrimValue (..)
    , -- * Toplevels and Polytypes
      RawTopLevel (..)
    , PolyType (..)
    ) where
  
  
  import qualified Data.Map as M
  
  -- | Binary and Unary Operators
  data Op
    = Plus | Times | Minus | Divide | Mod
    | Less | Greater | LessEqual | GreaterEqual
    | Equal | NotEqual
    | And | Or | Not
    deriving (Show, Eq)
  
  type FieldName = String
  type VarName = String
  type ConName = String
  type FunName = String
  type RecParName = String
  type AbsTypeName = String
  
  -- | A field or alternative is marked /taken/ if it is unpacked with a 'Take' expression
  --   or matched on with a 'Case' expression. 
  type Taken = Bool
  -- | An entry is either a record field or a variant alternative, consisting of a field or
  --   constructor name, a type, and whether or not the field or alternative is taken.
  data Entry = Entry String Type Taken -- Used for both Record and Variant
       deriving (Show, Eq)
  
  -- | Primitive types are represented using machine word types.
  data PrimType = Unit | Bool | U8 | U16 | U32 | U64
       deriving (Show, Eq)
  
  -- | Sigils, used in boxed records and abstract types, indicate whether a type is an
  --   unboxed data structure, a boxed read-only data structure, or a boxed read/write
  --   data structure which must be linearly typed.
  --
  --   Unification variables may also stand for sigils during type inference.
  data Sigil
    = Unboxed | ReadOnly | Writable
    | UnknownSigil VarName -- ^ Used only for type inference.
    deriving (Show, Eq)
  
  
  -- | A row is the contents of either a record or variant type. Each 'Entry' in the
  --   row corresponds to a field or alternative in the type. In addition, during type
  --   inference a row may also contain a unification variable to stand for further
  --   entries that are not yet known.
  data Row
    = Row
      { rowEntries :: M.Map FieldName Entry
      , rowVar :: Maybe VarName -- ^ Used only in type inference.
      } deriving (Show, Eq)
  
  -- | A recursive context.
  --   Maps a recursive parameter name to the record type which binds it
  --   Recursive parameters that exist within the context should have 'Nothing' as their
  --   context, to prevent infinite unrolling of the context.
  type RecContext = Maybe (M.Map RecParName Type)
  
  -- | A recursive parameter type, for embedding in front of records.
  --   Uses of the parameter inside the embedded record can be treated as recursively
  --   referencing the record
  data RecPar
    = None           -- ^ A regular non-recursive record
    | Rec RecParName -- ^ A recursive record
    | UnknownParameter RecParName -- ^ Used only in type inference (a unification variable)
    deriving (Show, Eq)
  
  -- | A type, which may contain unification variables or type operators.
  data Type
    = PrimType PrimType
    | Record RecPar Row Sigil -- ^ A recursive parameter, field entry row and sigil
    | AbsType AbsTypeName Sigil [Type]
    | Variant Row
    | TypeVar VarName -- ^ Refers to a rigid type variable bound with a forall.
    | TypeVarBang VarName -- ^ A 'TypeVar' with 'Bang' applied.
    -- ^ Refers to a recursive parameter, with the context of it's recursive references for Unrolling
    | RecPar VarName RecContext     -- ^ A recursive parameter.
    | RecParBang VarName RecContext -- ^ A 'RecPar' with 'Bang' applied.
    | Function Type Type
    -- used in type inference:
    | UnifVar VarName -- ^ Stands for an unknown type
    | Bang Type -- ^ Eliminated by type normalisation.
    deriving (Show, Eq)
  
  -- | Used for literals.
  data PrimValue = BoolV Bool | IntV Integer | UnitV
       deriving (Show, Eq)
  
  -- | Basic minicogent expressions.
  data Expr
    = PrimOp Op [Expr]  -- ^ Primitive operators with one or two arguments.
    | Literal PrimValue -- ^ Basic primitive type literals.
    | Var VarName       -- ^ Variables, identified by name. Shadowing is allowed.
    | Con ConName Expr  -- ^ A variant constructor applied to an argument.
    | TypeApp FunName [Type] -- ^ A function applied to zero or more type arguments.
    | Sig Expr Type     -- ^ An explicit type annotation. Added to all expressions by type inference.
    | Apply Expr Expr   -- ^ Function application.
    | Struct [(FieldName, Expr)] -- ^ Unboxed record literals.
    | If Expr Expr Expr -- ^ Ordinary conditionals. Condition, then, else.
    | Let VarName Expr Expr -- ^ A let expression. Not that @let@ doesn't imply type generalisation.
    | LetBang [VarName] VarName Expr Expr -- ^ Like let, but allows for observers to be made of the
                                          --   given variables.
    | Take VarName FieldName VarName Expr Expr -- ^ A take expression, the first 'VarName' denotes
                                               --   the name of the remaining record, the second
                                               --   is the name for the contents of the taken field.
                                               --   The first expression is the record to take from,
                                               --   and the second expression is the scope of the
                                               --   two new variables.
    | Put Expr FieldName Expr -- ^ A put expression. The first expression is the incomplete record
                              --   with the given field taken. The second expression evaluates to
                              --   a compatible value that can be placed inside the incomplete
                              --   record and then returned.
    | Member Expr FieldName -- ^ Extracting a field from a (non-linear) record.
    | Case Expr ConName VarName Expr VarName Expr
      -- ^ A refutable case expression where the first expression is
      --   the scrutinee to match on. After that, the first 'VarName' and 'Expr' denote the variable
      --   name bound and expression to run if the given scrutinee matches the given constructor.
      --   The second 'VarName' and 'Expr' are likewise for the default, fallback case. In this
      --   case, the variable bound will have the same type as the scrutinee, only with the constructor
      --   marked as 'Taken'.
    | Esac Expr ConName VarName Expr
      -- ^ An irrefutable pattern match expression. Here, the scrutinee must provably
      --   match the provided constructor.
    deriving (Show, Eq)
  
  infixr 0 :&:
  
  -- | Constraints used for type inference.
  data Constraint
    = Constraint :&: Constraint -- ^ Conjunction.
    | Type :< Type -- ^ Subtyping. Antisymmetry gives type equality constraints.
    | Type :=: Type -- ^ Type equality.
    | Integer :<=: Type -- ^ The 'fits in' relation, that says a given literal fits in the given
                        --   type. Only satisfiable if the type is a numeric type.
    | Share Type                    -- ^ The given type can be duplicated or shared freely
    | Drop Type                     -- ^ The given type can go out of scope without being used
    | Escape Type                   -- ^ The given type can be safely bound in a 'LetBang' expression
    | Exhausted Type                -- ^ The given type is a variant type where all entries are 'Taken'.
    | Solved Type                   -- ^ Constraint is satisfied when the type has no unification variables.
    | UnboxedNoRecurse RecPar Sigil -- ^ Satisfied when either Sigil is boxed, or is unboxed and RecPar is None
    | Sat            -- ^ Trivially true.
    | Unsat          -- ^ Trivially false.
    deriving (Show, Eq)
  
  infixr 0 :<:
  
  -- | Termination assertions used for detecting termination
  data Assertion = 
      VarName :<: VarName  -- ^ Structurally less than
    | VarName :~: VarName  -- ^ Structurally equal to 
    deriving (Eq, Ord, Show)
  
  
  pattern (:>) t1 t2 = t2 :< t1
  
  -- | A polymorphic type, used for top-level bindings only.
  --   Given a list of type variable names, constraints on those type variables (right now,
  --   only 'Share', 'Drop' and 'Escape' constraints are supported).
  data PolyType = Forall [VarName] [Constraint] Type
       deriving (Show, Eq)
  
  -- | A top level declaration is either a type signature for a function
  --   or a definition for a function.
  data RawTopLevel
    = TypeSig FunName PolyType -- ^ @f : t@
    | Equation FunName VarName Expr -- ^ @f x = e@
    deriving (Show, Eq)