summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/Pure.ml96
-rw-r--r--src/PureMicroPasses.ml52
-rw-r--r--src/SymbolicToPure.ml7
3 files changed, 121 insertions, 34 deletions
diff --git a/src/Pure.ml b/src/Pure.ml
index 375cdb0f..201ffd74 100644
--- a/src/Pure.ml
+++ b/src/Pure.ml
@@ -146,13 +146,17 @@ type mplace = { name : string option; projection : projection }
type place = { var : VarId.id; projection : projection }
-(** Ancestor for [iter_var_or_dummy] iter visitor *)
+(** Ancestor for [iter_var_or_dummy] visitor *)
class ['self] iter_value_base =
object (_self : 'self)
inherit [_] VisitorsRuntime.iter
+ method visit_constant_value : 'env -> constant_value -> unit = fun _ _ -> ()
+
method visit_var : 'env -> var -> unit = fun _ _ -> ()
+ method visit_place : 'env -> place -> unit = fun _ _ -> ()
+
method visit_mplace : 'env -> mplace -> unit = fun _ _ -> ()
method visit_ty : 'env -> ty -> unit = fun _ _ -> ()
@@ -163,8 +167,13 @@ class ['self] map_value_base =
object (_self : 'self)
inherit [_] VisitorsRuntime.map
+ method visit_constant_value : 'env -> constant_value -> constant_value =
+ fun _ x -> x
+
method visit_var : 'env -> var -> var = fun _ x -> x
+ method visit_place : 'env -> place -> place = fun _ x -> x
+
method visit_mplace : 'env -> mplace -> mplace = fun _ x -> x
method visit_ty : 'env -> ty -> ty = fun _ x -> x
@@ -175,8 +184,13 @@ class virtual ['self] reduce_value_base =
object (self : 'self)
inherit [_] VisitorsRuntime.reduce
+ method visit_constant_value : 'env -> constant_value -> 'a =
+ fun _ _ -> self#zero
+
method visit_var : 'env -> var -> 'a = fun _ _ -> self#zero
+ method visit_place : 'env -> place -> 'a = fun _ _ -> self#zero
+
method visit_mplace : 'env -> mplace -> 'a = fun _ _ -> self#zero
method visit_ty : 'env -> ty -> 'a = fun _ _ -> self#zero
@@ -261,10 +275,33 @@ and adt_rvalue = {
}
and typed_rvalue = { value : rvalue; ty : ty }
-(** In most situations we won't use the type in [typed_rvalue].
- Note that it is still necessary to have some useful informations
- about ADTs, though.
- *)
+[@@deriving
+ visitors
+ {
+ name = "iter_typed_rvalue";
+ variety = "iter";
+ ancestors = [ "iter_typed_lvalue" ];
+ nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+ concrete = true;
+ polymorphic = false;
+ },
+ visitors
+ {
+ name = "map_typed_rvalue";
+ variety = "map";
+ ancestors = [ "map_typed_lvalue" ];
+ nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+ concrete = true;
+ polymorphic = false;
+ },
+ visitors
+ {
+ name = "reduce_typed_rvalue";
+ variety = "reduce";
+ ancestors = [ "reduce_typed_lvalue" ];
+ nude = true (* Don't inherit [VisitorsRuntime.iter] *);
+ polymorphic = false;
+ }]
type unop = Not | Neg of T.integer_type
@@ -278,18 +315,10 @@ type fun_id =
(** Meta-information stored in the AST *)
type meta = Assignment of mplace * typed_rvalue
-(** Ancestor for [iter_expression] iter visitor *)
+(** Ancestor for [iter_expression] visitor *)
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_mplace : 'env -> mplace -> unit = fun _ _ -> ()
+ inherit [_] iter_typed_rvalue
method visit_meta : 'env -> meta -> unit = fun _ _ -> ()
@@ -302,20 +331,10 @@ class ['self] iter_expression_base =
method visit_fun_id : 'env -> fun_id -> unit = fun _ _ -> ()
end
-(** Ancestor for [map_expression] map visitor *)
+(** Ancestor for [map_expression] visitor *)
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_mplace : 'env -> mplace -> mplace = fun _ x -> x
+ inherit [_] map_typed_rvalue
method visit_meta : 'env -> meta -> meta = fun _ x -> x
@@ -330,6 +349,22 @@ class ['self] map_expression_base =
method visit_fun_id : 'env -> fun_id -> fun_id = fun _ x -> x
end
+(** Ancestor for [reduce_expression] visitor *)
+class virtual ['self] reduce_expression_base =
+ object (_self : 'self)
+ inherit [_] reduce_typed_rvalue
+
+ method visit_meta : 'env -> meta -> 'a = fun _ _ -> ()
+
+ method visit_integer_type : 'env -> T.integer_type -> 'a = fun _ _ -> ()
+
+ method visit_scalar_value : 'env -> scalar_value -> 'a = fun _ _ -> ()
+
+ method visit_id : 'env -> VariantId.id -> 'a = fun _ _ -> ()
+
+ method visit_fun_id : 'env -> fun_id -> 'a = fun _ _ -> ()
+ 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.
@@ -416,6 +451,13 @@ and match_branch = { pat : typed_lvalue; branch : expression }
ancestors = [ "map_expression_base" ];
nude = true (* Don't inherit [VisitorsRuntime.iter] *);
concrete = true;
+ },
+ visitors
+ {
+ name = "reduce_expression";
+ variety = "reduce";
+ ancestors = [ "reduce_expression_base" ];
+ nude = true (* Don't inherit [VisitorsRuntime.iter] *);
}]
type fun_sig = {
diff --git a/src/PureMicroPasses.ml b/src/PureMicroPasses.ml
index 9f261386..cb7f5b23 100644
--- a/src/PureMicroPasses.ml
+++ b/src/PureMicroPasses.ml
@@ -7,6 +7,17 @@ open TranslateCore
(** The local logger *)
let log = L.pure_micro_passes_log
+(** Small utility.
+
+ We sometimes have to insert new fresh variables in a function body, in which
+ case we need to make their indices greater than the indices of all the variables
+ in the body.
+ TODO: things would be simpler if we used a better representation of the
+ variables indices...
+ *)
+let get_expression_min_var_counter (e : expression) : VarId.generator =
+ raise Unimplemented
+
type pn_ctx = string VarId.Map.t
(** "pretty-name context": see [compute_pretty_names] *)
@@ -266,8 +277,34 @@ let filter_unused_assignments (def : fun_def) : fun_def =
(** Add unit arguments for functions with no arguments, and change their return type. *)
let to_monadic (def : fun_def) : fun_def =
- (* TODO *)
- def
+ (* Update the body *)
+ let obj =
+ object
+ inherit [_] map_expression as super
+
+ method! visit_call env call =
+ (* If no arguments, introduce unit *)
+ if call.args = [] then
+ let args = [ Value (SymbolicToPure.unit_rvalue, None) ] in
+ { call with args } (* Otherwise: nothing to do *)
+ else super#visit_call env call
+ end
+ in
+ let body = obj#visit_expression () def.body in
+ let def = { def with body } in
+
+ (* Update the signature *)
+ if def.inputs = [] then (
+ assert (def.signature.inputs = []);
+ let signature =
+ { def.signature with inputs = [ SymbolicToPure.unit_ty ] }
+ in
+ let var_cnt = get_expression_min_var_counter def.body in
+ let id, _ = VarId.fresh var_cnt in
+ let var = { id; basename = None; ty = SymbolicToPure.unit_ty } in
+ let inputs = [ var ] in
+ { def with signature; inputs })
+ else def
(** Apply all the micro-passes to a function.
@@ -296,6 +333,12 @@ let apply_passes_to_def (ctx : trans_ctx) (def : fun_def) : fun_def =
let def = remove_meta def in
log#ldebug (lazy ("remove_meta:\n" ^ fun_def_to_string ctx def));
+ (* Add unit arguments for functions with no arguments, and change their return type.
+ * **Rk.**: from now onwards, the types in the AST are correct (until now,
+ * functions had return type `t` where they should have return type `result t`) *)
+ (* let def = to_monadic def in
+ log#ldebug (lazy ("to_monadic:\n" ^ fun_def_to_string ctx def));*)
+
(* Inline the useless variable reassignments *)
let def = inline_useless_var_reassignments def in
log#ldebug
@@ -308,11 +351,6 @@ let apply_passes_to_def (ctx : trans_ctx) (def : fun_def) : fun_def =
(* TODO: deconstruct the monadic bindings into matches *)
- (* Add unit arguments for functions with no arguments, and change their return type.
- * TODO: move that at the beginning? *)
- let def = to_monadic def in
- log#ldebug (lazy ("to_monadic:\n" ^ fun_def_to_string ctx def));
-
(* We are done *)
def
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 2279dd06..30142639 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -27,6 +27,13 @@ let mk_place_from_var (v : var) : place = { var = v.id; projection = [] }
let mk_tuple_ty (tys : ty list) : ty = Adt (Tuple, tys)
+let unit_ty : ty = Adt (Tuple, [])
+
+let unit_rvalue : typed_rvalue =
+ let value = RvAdt { variant_id = None; field_values = [] } in
+ let ty = unit_ty in
+ { value; ty }
+
let mk_typed_rvalue_from_var (v : var) : typed_rvalue =
let value = RvPlace (mk_place_from_var v) in
let ty = v.ty in
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 14:43:06 +0000