From 4eea9bc50c1f151f1b47f2b78327ce2fd92af300 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 28 Jan 2022 00:21:55 +0100
Subject: Implement visitors for Pure.expression and make minor modifications
---
src/Pure.ml | 67 +++++++++++++++++++++++++++++++++++++++++++++++
src/PureMicroPasses.ml | 71 ++++++++++++++++++++++++++++++++++++++------------
2 files changed, 121 insertions(+), 17 deletions(-)
diff --git a/src/Pure.ml b/src/Pure.ml
index 7e5aca47..4e0768cd 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -203,6 +203,55 @@ type let_bindings =
(** Meta-information stored in the AST *)
type meta = Assignment of mplace * typed_rvalue
+(** Ancestor for [iter_expression] iter visitor *)
+class ['self] iter_expression_base =
+ object (_self : 'self)
+ inherit [_] VisitorsRuntime.iter
+
+ method visit_typed_rvalue : 'env -> typed_rvalue -> 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 _ _ -> ()
+
+ method visit_integer_type : 'env -> T.integer_type -> unit = fun _ _ -> ()
+
+ method visit_scalar_value : 'env -> scalar_value -> unit = fun _ _ -> ()
+
+ method visit_id : 'env -> VariantId.id -> unit = fun _ _ -> ()
+
+ method visit_var_or_dummy : 'env -> var_or_dummy -> unit = fun _ _ -> ()
+ end
+
+(** Ancestor for [map_expression] map visitor *)
+class ['self] map_expression_base =
+ object (_self : 'self)
+ inherit [_] VisitorsRuntime.map
+
+ method visit_typed_rvalue : 'env -> typed_rvalue -> typed_rvalue =
+ 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
+
+ method visit_integer_type : 'env -> T.integer_type -> T.integer_type =
+ fun _ x -> x
+
+ method visit_scalar_value : 'env -> scalar_value -> scalar_value =
+ fun _ x -> x
+
+ 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
+ end
+
(** **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.
@@ -230,6 +279,24 @@ and match_branch = {
vars : var_or_dummy list;
branch : expression;
}
+[@@deriving
+ visitors
+ {
+ name = "iter_expression";
+ variety = "iter";
+ ancestors = [ "iter_expression_base" ];
+ nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+ concrete = true;
+ },
+ visitors
+ {
+ name = "map_expression";
+ variety = "map";
+ ancestors = [ "map_expression_base" ];
+ nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+ concrete = true;
+ }]
+(** "Regular" typed value (we map variables to typed values) *)
type fun_sig = {
type_params : type_var list;
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index cd64a288..634537c2 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -1,5 +1,6 @@
(** The following module defines micro-passes which operate on the pure AST *)
+open Errors
open Pure
(** This function computes pretty names for the variables in the pure AST. It
@@ -13,6 +14,7 @@ open Pure
a name and an empty path, we consider we should use this name
For instance, the following situations happen:
+
- let's say we evaluate:
```
match (ls : List<T>) {
@@ -24,11 +26,11 @@ open Pure
Actually, in MIR, we get:
```
- tmp = discriminant(ls);
+ tmp := discriminant(ls);
switch tmp {
0 => {
- x = (ls as Cons).0;
- hd = (ls as Cons).1;
+ x := (ls as Cons).0;
+ hd := (ls as Cons).1;
...
}
}
@@ -44,19 +46,54 @@ open Pure
hd -> s2
```
- If at any moment we use `x` (as an operand to a function, to return,
- etc.) we ...
- TODO: finish explanations
- TODO: meta-information for:
- - unop
- - binop
- - assignments
- - discriminant
- - ...
-
- the subsequent assignments actually give us the naming information we
- were looking for.
- - TODO: temporaries for binops which can fail/have preconditions
- - TODO: reborrows just before calling functions.
+ When generating the symbolic AST, we save as meta-information that we
+ assign `s1` to the place `x` and `s2` to the place `hd`. This way,
+ we learn we can use the names `x` and `hd` for the variables which are
+ introduced by the match:
+ ```
+ match ls with
+ | Cons x hd -> ...
+ | ...
+ ```
+ - If we write the following in Rust:
+ ```
+ let x = y + z;
+ ```
+
+ We get the following MIR:
+ ```
+ let tmp = y + z;
+ ```
+ TODO: finish...
+ - If we write the following in Rust:
+ ```
+ let px = &mut x;
+ f(px);
+ ```
+
+ Rustc generates the following MIR:
+ ```
+ px := &mut x;
+ tmp := &mut ( *px ); // "tmp" is actually an anonymous variable
+ f(move tmp);
+ ```
+
+ As borrows and dereferencements are ignored in the pure paths we generate
+ (because they are extracted to the identity), we save as meta-data that
+ at some point we assign the value of `px` to `tmp`.
+
+ TODO: actually useless, because `tmp` later gets inlined.
+ - TODO: inputs and end abstraction...
*)
let compute_pretty_names () = ()
+
+(** Remove the meta-information *)
+let remove_meta (e : expression) : expression =
+ let obj =
+ object
+ inherit [_] map_expression as super
+
+ method! visit_Meta env meta e = super#visit_expression env e
+ end
+ in
+ obj#visit_expression () e
--
cgit v1.2.3