diff options
Diffstat (limited to 'compiler/SynthesizeSymbolic.ml')
| -rw-r--r-- | compiler/SynthesizeSymbolic.ml | 38 |
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) |