summaryrefslogtreecommitdiff
path: root/compiler/SynthesizeSymbolic.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/SynthesizeSymbolic.ml38
1 files changed, 20 insertions, 18 deletions
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index 857fea97..9dd65c84 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -64,7 +64,7 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value)
assert (otherwise_see = None);
(* Return *)
ExpandInt (int_ty, branches, otherwise)
- | T.Adt (_, _, _, _) ->
+ | T.Adt (_, _) ->
(* Branching: it is necessarily an enumeration expansion *)
let get_variant (see : V.symbolic_expansion option) :
T.VariantId.id option * V.symbolic_value list =
@@ -85,7 +85,9 @@ let synthesize_symbolic_expansion (sv : V.symbolic_value)
match ls with
| [ (Some see, exp) ] -> ExpandNoBranch (see, exp)
| _ -> raise (Failure "Ill-formed borrow expansion"))
- | T.TypeVar _ | T.Literal Char | Never ->
+ | T.TypeVar _
+ | T.Literal Char
+ | Never | T.TraitType _ | T.Arrow _ | T.RawPtr _ ->
raise (Failure "Ill-formed symbolic expansion")
in
Some (Expansion (place, sv, expansion))
@@ -97,10 +99,10 @@ let synthesize_symbolic_expansion_no_branching (sv : V.symbolic_value)
synthesize_symbolic_expansion sv place [ Some see ] el
let synthesize_function_call (call_id : call_id) (ctx : Contexts.eval_ctx)
- (abstractions : V.AbstractionId.id list) (type_params : T.ety list)
- (const_generic_params : T.const_generic list) (args : V.typed_value list)
- (args_places : mplace option list) (dest : V.symbolic_value)
- (dest_place : mplace option) (e : expression option) : expression option =
+ (abstractions : V.AbstractionId.id list) (generics : T.egeneric_args)
+ (args : V.typed_value list) (args_places : mplace option list)
+ (dest : V.symbolic_value) (dest_place : mplace option)
+ (e : expression option) : expression option =
Option.map
(fun e ->
let call =
@@ -108,8 +110,7 @@ let synthesize_function_call (call_id : call_id) (ctx : Contexts.eval_ctx)
call_id;
ctx;
abstractions;
- type_params;
- const_generic_params;
+ generics;
args;
dest;
args_places;
@@ -123,28 +124,29 @@ let synthesize_global_eval (gid : A.GlobalDeclId.id) (dest : V.symbolic_value)
(e : expression option) : expression option =
Option.map (fun e -> EvalGlobal (gid, dest, e)) e
-let synthesize_regular_function_call (fun_id : A.fun_id)
+let synthesize_regular_function_call (fun_id : A.fun_id_or_trait_method_ref)
(call_id : V.FunCallId.id) (ctx : Contexts.eval_ctx)
- (abstractions : V.AbstractionId.id list) (type_params : T.ety list)
- (const_generic_params : T.const_generic list) (args : V.typed_value list)
- (args_places : mplace option list) (dest : V.symbolic_value)
- (dest_place : mplace option) (e : expression option) : expression option =
+ (abstractions : V.AbstractionId.id list) (generics : T.egeneric_args)
+ (args : V.typed_value list) (args_places : mplace option list)
+ (dest : V.symbolic_value) (dest_place : mplace option)
+ (e : expression option) : expression option =
synthesize_function_call
(Fun (fun_id, call_id))
- ctx abstractions type_params const_generic_params args args_places dest
- dest_place e
+ ctx abstractions generics args args_places dest dest_place e
let synthesize_unary_op (ctx : Contexts.eval_ctx) (unop : E.unop)
(arg : V.typed_value) (arg_place : mplace option) (dest : V.symbolic_value)
(dest_place : mplace option) (e : expression option) : expression option =
- synthesize_function_call (Unop unop) ctx [] [] [] [ arg ] [ arg_place ] dest
- dest_place e
+ let generics = TypesUtils.mk_empty_generic_args in
+ synthesize_function_call (Unop unop) ctx [] generics [ arg ] [ arg_place ]
+ dest dest_place e
let synthesize_binary_op (ctx : Contexts.eval_ctx) (binop : E.binop)
(arg0 : V.typed_value) (arg0_place : mplace option) (arg1 : V.typed_value)
(arg1_place : mplace option) (dest : V.symbolic_value)
(dest_place : mplace option) (e : expression option) : expression option =
- synthesize_function_call (Binop binop) ctx [] [] [] [ arg0; arg1 ]
+ let generics = TypesUtils.mk_empty_generic_args in
+ synthesize_function_call (Binop binop) ctx [] generics [ arg0; arg1 ]
[ arg0_place; arg1_place ] dest dest_place e
let synthesize_end_abstraction (ctx : Contexts.eval_ctx) (abs : V.abs)