diff options
author | Son Ho | 2022-01-28 11:06:13 +0100 |
---|---|---|
committer | Son Ho | 2022-01-28 11:06:13 +0100 |
commit | d00dd80b8b752a17c2027d6daccf74974ebf4292 (patch) | |
tree | 7d1b345a6d24dc6698c4040d8277f5eb5eea37fb /src/Pure.ml | |
parent | 7deb7a2bde6d6bcdf14aac4f68f336bc498b964b (diff) |
Simplify the let-bindings in the pure AST
Diffstat (limited to 'src/Pure.ml')
-rw-r--r-- | src/Pure.ml | 155 |
1 files changed, 94 insertions, 61 deletions
diff --git a/src/Pure.ml b/src/Pure.ml index 61d2d130..64851449 100644 --- a/src/Pure.ml +++ b/src/Pure.ml @@ -18,6 +18,20 @@ module SynthPhaseId = IdGen () module VarId = IdGen () (** Pay attention to the fact that we also define a [VarId] module in Values *) +(* TODO + (** The assumed types for the pure AST. + + In comparison with CFIM: + - we removed `Box` (because it is translated as the identity: `Box T == T`) + - we added `Result`, which is the type used in the error monad. This allows + us to have a unified treatment of expressions. + *) + type assumed_ty = unit + + type type_id = AdtId of TypeDefId.id | Tuple | Assumed of assumed_ty + [@@deriving show, ord] +*) + type ty = | Adt of T.type_id * ty list (** [Adt] encodes ADTs and tuples and assumed types. @@ -238,55 +252,6 @@ type fun_id = | Unop of unop | Binop of E.binop * T.integer_type -type call = { - func : fun_id; - type_params : ty list; - args : typed_rvalue list; - (** Note that at this point, some functions have no arguments. For instance: - ``` - fn f(); - ``` - - In the extracted code, we add a unit argument. This is unit argument is - added later, when going from the "pure" AST to the "extracted" AST. - *) - args_mplaces : mplace option list; (** Meta data *) -} - -(* TODO: we might want to merge Call and Assign *) -type let_bindings = - | Call of typed_lvalue * call - (** The called function and the tuple of returned values. *) - | Assign of typed_lvalue * typed_rvalue * mplace option - (** Variable assignment: the introduced pattern and the place we read. - - We are quite general for the left-value on purpose; this is used - in several situations: - - 1. When deconstructing a tuple: - ``` - let (x, y) = p in ... - ``` - (not all languages have syntax like `p.0`, `p.1`... and it is more - readable anyway). - - 2. When expanding an enumeration with one variant. - - In this case, [Deconstruct] has to be understood as: - ``` - let Cons x tl = ls in - ... - ``` - - Note that later, depending on the language we extract to, we can - eventually update it to something like this (for F*, for instance): - ``` - let x = Cons?.v ls in - let tl = Cons?.tl ls in - ... - ``` - *) - (** Meta-information stored in the AST *) type meta = Assignment of mplace * typed_rvalue @@ -295,12 +260,12 @@ class ['self] iter_expression_base = object (_self : 'self) inherit [_] VisitorsRuntime.iter + method visit_ty : 'env -> ty -> unit = fun _ _ -> () + method visit_typed_rvalue : 'env -> typed_rvalue -> unit = fun _ _ -> () method visit_typed_lvalue : 'env -> typed_lvalue -> unit = fun _ _ -> () - method visit_let_bindings : 'env -> let_bindings -> unit = fun _ _ -> () - method visit_mplace : 'env -> mplace -> unit = fun _ _ -> () method visit_meta : 'env -> meta -> unit = fun _ _ -> () @@ -311,7 +276,7 @@ class ['self] iter_expression_base = method visit_id : 'env -> VariantId.id -> unit = fun _ _ -> () - method visit_var_or_dummy : 'env -> var_or_dummy -> unit = fun _ _ -> () + method visit_fun_id : 'env -> fun_id -> unit = fun _ _ -> () end (** Ancestor for [map_expression] map visitor *) @@ -319,15 +284,14 @@ class ['self] map_expression_base = object (_self : 'self) inherit [_] VisitorsRuntime.map + method visit_ty : 'env -> ty -> ty = fun _ x -> x + method visit_typed_rvalue : 'env -> typed_rvalue -> typed_rvalue = fun _ x -> x method visit_typed_lvalue : 'env -> typed_lvalue -> typed_lvalue = fun _ x -> x - method visit_let_bindings : 'env -> let_bindings -> let_bindings = - fun _ x -> x - method visit_mplace : 'env -> mplace -> mplace = fun _ x -> x method visit_meta : 'env -> meta -> meta = fun _ x -> x @@ -340,10 +304,43 @@ class ['self] map_expression_base = method visit_id : 'env -> VariantId.id -> VariantId.id = fun _ x -> x - method visit_var_or_dummy : 'env -> var_or_dummy -> var_or_dummy = - fun _ x -> x + method visit_fun_id : 'env -> fun_id -> fun_id = fun _ x -> x end +type call = { + func : fun_id; + type_params : ty list; + args : typed_rvalue list; + (** Note that immediately after we converted the symbolic AST to a pure AST, + some functions may have no arguments. For instance: + ``` + fn f(); + ``` + We later add a unit argument. + + TODO: we should use expressions... + *) + args_mplaces : mplace option list; (** Meta data *) +} +[@@deriving + visitors + { + name = "iter_call"; + variety = "iter"; + ancestors = [ "iter_expression_base" ]; + nude = true (* Don't inherit [VisitorsRuntime.iter] *); + concrete = true; + }, + visitors + { + name = "map_call"; + variety = "map"; + ancestors = [ "map_expression_base" ]; + nude = true (* Don't inherit [VisitorsRuntime.iter] *); + concrete = true; + }] +(** "Regular" typed value (we map variables to typed values) *) + (** **Rk.:** here, [expression] is not at all equivalent to the expressions used in CFIM. They are lambda-calculus expressions, and are thus actually more general than the CFIM statements, in a sense. @@ -352,12 +349,48 @@ class ['self] map_expression_base = it is not a "textbook" lambda calculus expression (still quite constrained). As we want to do transformations on it, through micro-passes, it would be good to update it and make it more "regular". + + TODO: remove `Return` and `Fail` (they should be "normal" values, I think) *) type expression = | Return of typed_rvalue | Fail - | Let of let_bindings * expression - (** Let bindings include the let-bindings introduced because of function calls *) + | Value of typed_rvalue * mplace option + | Call of call + | Let of typed_lvalue * expression * expression + (** Let binding. + + TODO: add a boolean to control whether the let is monadic or not. + For instance, in F*: + - non-monadic: `let x = ... in ...` + - monadic: `x <-- ...; ...` + + Note that we are quite general for the left-value on purpose; this + is used in several situations: + + 1. When deconstructing a tuple: + ``` + let (x, y) = p in ... + ``` + (not all languages have syntax like `p.0`, `p.1`... and it is more + readable anyway). + + 2. When expanding an enumeration with one variant. + + In this case, [Deconstruct] has to be understood as: + ``` + let Cons x tl = ls in + ... + ``` + + Note that later, depending on the language we extract to, we can + eventually update it to something like this (for F*, for instance): + ``` + let x = Cons?.v ls in + let tl = Cons?.tl ls in + ... + ``` + *) | Switch of typed_rvalue * mplace option * switch_body | Meta of meta * expression (** Meta-information *) @@ -372,7 +405,7 @@ and match_branch = { pat : typed_lvalue; branch : expression } { name = "iter_expression"; variety = "iter"; - ancestors = [ "iter_expression_base" ]; + ancestors = [ "iter_call" ]; nude = true (* Don't inherit [VisitorsRuntime.iter] *); concrete = true; }, @@ -380,7 +413,7 @@ and match_branch = { pat : typed_lvalue; branch : expression } { name = "map_expression"; variety = "map"; - ancestors = [ "map_expression_base" ]; + ancestors = [ "map_call" ]; nude = true (* Don't inherit [VisitorsRuntime.iter] *); concrete = true; }] |