0 | module Compiler.ES.Ast
  1 |
  2 | import Core.CompileExpr
  3 | import Core.Context
  4 | import Data.List1
  5 | import Data.Vect
  6 |
  7 | %default total
  8 |
  9 | public export
 10 | data Tag : Type where
 11 |   ||| A data constructor. Use the tag to dispatch / construct.
 12 |   ||| Here the Name is only for documentation purposes and should not
 13 |   ||| be used.
 14 |   DataCon : (tag : Int) -> (name : Name) -> Tag
 15 |   ||| A type constructor. We do not have a unique tag associated to types
 16 |   ||| and so we match on names instead.
 17 |   TypeCon : (name : Name) -> Tag
 18 |
 19 | ||| A variable in a toplevel function definition
 20 | |||
 21 | ||| When generating the syntax tree of imperative
 22 | ||| statements and expressions, we decide - based on
 23 | ||| codegen directives - which Idris names to keep
 24 | ||| and which names to convert to short, mangled
 25 | ||| versions.
 26 | public export
 27 | data Var =
 28 |     ||| An unaltered name - usually a toplevel function
 29 |     ||| or a function argument with an explicitly given
 30 |     ||| name
 31 |     VName Name |
 32 |
 33 |     ||| Index of a local variables
 34 |     VLoc  Int  |
 35 |
 36 |     ||| Index of a mangled toplevel function
 37 |     VRef  Int
 38 |
 39 | ||| A minimal expression.
 40 | public export
 41 | data Minimal =
 42 |   ||| A variable
 43 |   MVar Var |
 44 |
 45 |   ||| A projection targeting the field of a data type.
 46 |   ||| We include these here since it allows us to
 47 |   ||| conveniently carry around a `SortedMap Name Minimal`
 48 |   ||| for name resolution during the generation of the
 49 |   ||| imperative syntax tree.
 50 |   MProjection Nat Minimal
 51 |
 52 | --------------------------------------------------------------------------------
 53 | --          Expressions
 54 | --------------------------------------------------------------------------------
 55 |
 56 | ||| The effect of a statement or a block of statements.
 57 | ||| `Returns` means the
 58 | ||| result of the final expression will be returned as
 59 | ||| the current function's result, while `ErrorWithout v`
 60 | ||| is a reminder, that the block of code will eventually
 61 | ||| assign a value to `v` and will fail to do so if
 62 | ||| `v` hasn't previously been declared.
 63 | |||
 64 | ||| This is used as a typelevel index to prevent us from
 65 | ||| making some common stupid errors like declaring a variable
 66 | ||| twice, or having several `return` statements in the same
 67 | ||| block of code.
 68 | public export
 69 | data Effect = Returns | ErrorWithout Var
 70 |
 71 | mutual
 72 |   ||| An expression in a function definition.
 73 |   public export
 74 |   data Exp : Type where
 75 |     ||| A variable or projection. Minimal expressions
 76 |     ||| will always be inlined unless explicitly bound
 77 |     ||| in an Idris2 `let` expression.
 78 |     EMinimal  : Minimal -> Exp
 79 |
 80 |     ||| Lambda expression
 81 |     |||
 82 |     ||| An empty argument list represents a delayed computation
 83 |     ELam      : List Var -> Stmt (Just Returns) -> Exp
 84 |
 85 |     ||| Function application.
 86 |     |||
 87 |     ||| In case of a zero-argument list, we might also be
 88 |     ||| dealing with forcing a delayed computation.
 89 |     EApp      : Exp -> List Exp -> Exp
 90 |
 91 |     ||| Saturated construtor application.
 92 |     |||
 93 |     ||| The tag either represents the name of a type constructor
 94 |     ||| (when we are pattern matching on types) or the index
 95 |     ||| of a data constructor.
 96 |     ECon      : (tag : Tag) -> ConInfo -> List Exp -> Exp
 97 |
 98 |     ||| Primitive operation
 99 |     EOp       : {0 arity : Nat} -> PrimFn arity -> Vect arity Exp -> Exp
100 |
101 |     ||| Externally defined primitive operation.
102 |     EExtPrim  : Name -> List Exp -> Exp
103 |
104 |     ||| A constant primitive.
105 |     EPrimVal  : Constant -> Exp
106 |
107 |     ||| An erased value.
108 |     EErased   : Exp
109 |
110 |   ||| An imperative statement in a function definition.
111 |   |||
112 |   ||| This is indexed over the `Effect` the statement,
113 |   ||| will have.
114 |   ||| An `effect` of `Nothing` means that the result of
115 |   ||| the statement is `undefined`: The declaration of
116 |   ||| a constant or assignment of a previously declared
117 |   ||| variable. When we sequence statements in a block
118 |   ||| of code, all but the last one of them must have
119 |   ||| effect `Nothing`. This makes sure we properly declare variables
120 |   ||| exactly once before eventually assigning them.
121 |   ||| It makes also sure a block of code does not contain
122 |   ||| several `return` statements (until they are the
123 |   ||| results of the branches of a `switch` statement).
124 |   public export
125 |   data Stmt : (effect : Maybe Effect) -> Type where
126 |     ||| Returns the result of the given expression.
127 |     Return      : Exp -> Stmt (Just Returns)
128 |
129 |     ||| Introduces a new constant by assigning the result
130 |     ||| of a single expression to the given variable.
131 |     Const      : (v : Var) -> Exp -> Stmt Nothing
132 |
133 |     ||| Assigns the result of an expression to the given variable.
134 |     ||| This will result in an error, if the variable has not
135 |     ||| yet been declared.
136 |     Assign     : (v : Var) -> Exp -> Stmt (Just $ ErrorWithout v)
137 |
138 |     ||| Declares (but does not yet assign) a new mutable
139 |     ||| variable. This is the only way to "saturate"
140 |     ||| a `Stmt (Just $ ErrorWithout v)`.
141 |     Declare    : (v : Var) -> Stmt (Just $ ErrorWithout v) -> Stmt Nothing
142 |
143 |     ||| Switch statement from a pattern match on
144 |     ||| data or type constructors. The result of each branch
145 |     ||| will have the given `Effect`.
146 |     |||
147 |     ||| The scrutinee has already been lifted to
148 |     ||| the outer scope to make sure it is only
149 |     ||| evaluated once.
150 |     ConSwitch   :  (e         : Effect)
151 |                 -> (scrutinee : Minimal)
152 |                 -> (alts      : List $ EConAlt e)
153 |                 -> (def       : Maybe $ Stmt $ Just e)
154 |                 -> Stmt (Just e)
155 |
156 |     ||| Switch statement from a pattern on
157 |     ||| a constant. The result of each branch
158 |     ||| will have the given `Effect`.
159 |     ConstSwitch :  (e         : Effect)
160 |                 -> (scrutinee : Exp)
161 |                 -> (alts      : List $ EConstAlt e)
162 |                 -> (def       : Maybe $ Stmt $ Just e)
163 |                 -> Stmt (Just e)
164 |
165 |     ||| A runtime exception.
166 |     Error       : {0 any : _} -> String -> Stmt (Just any)
167 |
168 |     ||| A code block consisting of one or more
169 |     ||| imperative statements.
170 |     Block       :  List1 (Stmt Nothing) -> Stmt e -> Stmt e
171 |
172 |   ||| Single branch in a pattern match on a data or
173 |   ||| type constructor.
174 |   public export
175 |   record EConAlt (e : Effect) where
176 |     constructor MkEConAlt
177 |     tag     : Tag
178 |     conInfo : ConInfo
179 |     body    : Stmt (Just e)
180 |
181 |   ||| Single branch in a pattern match on a constant
182 |   public export
183 |   record EConstAlt (e : Effect) where
184 |     constructor MkEConstAlt
185 |     constant : Constant
186 |     body     : Stmt (Just e)
187 |
188 | export
189 | toMinimal : Exp -> Maybe Minimal
190 | toMinimal (EMinimal v) = Just v
191 | toMinimal _            = Nothing
192 |
193 | export
194 | prepend : List (Stmt Nothing) -> Stmt (Just e) -> Stmt (Just e)
195 | prepend []       s = s
196 | prepend (h :: t) s = Block (h ::: t) s
197 |
198 | export total
199 | declare : {v : _} -> Stmt (Just $ ErrorWithout v) -> Stmt Nothing
200 | declare (Assign v y)              = Const v y
201 | declare (Block ss s)              = Block ss $ declare s
202 | declare s                         = Declare v s
203 |