From 5209cea7012cfa3b39a5a289e65e2ea5e166d730 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Thu, 21 Mar 2024 12:34:40 +0100 Subject: WIP: translate.ml and extract.ml do not compile. Some assert left to do and we need to see how translate_crate can give meta to the functions it calls --- compiler/InterpreterExpansion.mli | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'compiler/InterpreterExpansion.mli') diff --git a/compiler/InterpreterExpansion.mli b/compiler/InterpreterExpansion.mli index b545f979..3540d04c 100644 --- a/compiler/InterpreterExpansion.mli +++ b/compiler/InterpreterExpansion.mli @@ -12,11 +12,11 @@ type proj_kind = LoanProj | BorrowProj This function does *not* update the synthesis. *) val apply_symbolic_expansion_non_borrow : - config -> symbolic_value -> symbolic_expansion -> eval_ctx -> eval_ctx + Meta.meta -> config -> symbolic_value -> symbolic_expansion -> eval_ctx -> eval_ctx (** Expand a symhbolic value, without branching *) val expand_symbolic_value_no_branching : - config -> symbolic_value -> SA.mplace option -> cm_fun + Meta.meta -> config -> symbolic_value -> SA.mplace option -> cm_fun (** Expand a symbolic enumeration (leads to branching if the enumeration has more than one variant). @@ -32,7 +32,7 @@ val expand_symbolic_value_no_branching : then call it). *) val expand_symbolic_adt : - config -> symbolic_value -> SA.mplace option -> st_cm_fun -> st_m_fun -> m_fun + Meta.meta -> config -> symbolic_value -> SA.mplace option -> st_cm_fun -> st_m_fun -> m_fun (** Expand a symbolic boolean. @@ -41,6 +41,7 @@ val expand_symbolic_adt : parameter (here, there are exactly two branches). *) val expand_symbolic_bool : + Meta.meta -> config -> symbolic_value -> SA.mplace option -> @@ -69,6 +70,7 @@ val expand_symbolic_bool : switch. The continuation is thus for the execution *after* the switch. *) val expand_symbolic_int : + Meta.meta -> config -> symbolic_value -> SA.mplace option -> @@ -81,4 +83,4 @@ val expand_symbolic_int : (** If this mode is activated through the [config], greedily expand the symbolic values which need to be expanded. See {!type:Contexts.config} for more information. *) -val greedy_expand_symbolic_values : config -> cm_fun +val greedy_expand_symbolic_values : Meta.meta -> config -> cm_fun -- cgit v1.2.3 From d6ea35868e30bbc7542bfa09bb04d5b6cbe93b22 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Mon, 25 Mar 2024 12:06:05 +0100 Subject: Inverted meta and config argument orders (from meta -> config to config -> meta) --- compiler/InterpreterExpansion.mli | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'compiler/InterpreterExpansion.mli') diff --git a/compiler/InterpreterExpansion.mli b/compiler/InterpreterExpansion.mli index 3540d04c..8b0b386a 100644 --- a/compiler/InterpreterExpansion.mli +++ b/compiler/InterpreterExpansion.mli @@ -12,11 +12,11 @@ type proj_kind = LoanProj | BorrowProj This function does *not* update the synthesis. *) val apply_symbolic_expansion_non_borrow : - Meta.meta -> config -> symbolic_value -> symbolic_expansion -> eval_ctx -> eval_ctx + config -> Meta.meta -> symbolic_value -> symbolic_expansion -> eval_ctx -> eval_ctx (** Expand a symhbolic value, without branching *) val expand_symbolic_value_no_branching : - Meta.meta -> config -> symbolic_value -> SA.mplace option -> cm_fun + config -> Meta.meta -> symbolic_value -> SA.mplace option -> cm_fun (** Expand a symbolic enumeration (leads to branching if the enumeration has more than one variant). @@ -32,7 +32,7 @@ val expand_symbolic_value_no_branching : then call it). *) val expand_symbolic_adt : - Meta.meta -> config -> symbolic_value -> SA.mplace option -> st_cm_fun -> st_m_fun -> m_fun + config -> Meta.meta -> symbolic_value -> SA.mplace option -> st_cm_fun -> st_m_fun -> m_fun (** Expand a symbolic boolean. @@ -41,8 +41,8 @@ val expand_symbolic_adt : parameter (here, there are exactly two branches). *) val expand_symbolic_bool : - Meta.meta -> - config -> + config -> + Meta.meta -> symbolic_value -> SA.mplace option -> st_cm_fun -> @@ -70,8 +70,8 @@ val expand_symbolic_bool : switch. The continuation is thus for the execution *after* the switch. *) val expand_symbolic_int : - Meta.meta -> - config -> + config -> + Meta.meta -> symbolic_value -> SA.mplace option -> integer_type -> @@ -83,4 +83,4 @@ val expand_symbolic_int : (** If this mode is activated through the [config], greedily expand the symbolic values which need to be expanded. See {!type:Contexts.config} for more information. *) -val greedy_expand_symbolic_values : Meta.meta -> config -> cm_fun +val greedy_expand_symbolic_values : config -> Meta.meta -> cm_fun -- cgit v1.2.3 From 64666edb3c10cd42e15937ac4038b83def630e35 Mon Sep 17 00:00:00 2001 From: Escherichia Date: Thu, 28 Mar 2024 17:14:27 +0100 Subject: formatting --- compiler/InterpreterExpansion.mli | 19 +++++++++++++++---- 1 file changed, 15 insertions(+), 4 deletions(-) (limited to 'compiler/InterpreterExpansion.mli') diff --git a/compiler/InterpreterExpansion.mli b/compiler/InterpreterExpansion.mli index 8b0b386a..2ea27ea6 100644 --- a/compiler/InterpreterExpansion.mli +++ b/compiler/InterpreterExpansion.mli @@ -12,7 +12,12 @@ type proj_kind = LoanProj | BorrowProj This function does *not* update the synthesis. *) val apply_symbolic_expansion_non_borrow : - config -> Meta.meta -> symbolic_value -> symbolic_expansion -> eval_ctx -> eval_ctx + config -> + Meta.meta -> + symbolic_value -> + symbolic_expansion -> + eval_ctx -> + eval_ctx (** Expand a symhbolic value, without branching *) val expand_symbolic_value_no_branching : @@ -32,7 +37,13 @@ val expand_symbolic_value_no_branching : then call it). *) val expand_symbolic_adt : - config -> Meta.meta -> symbolic_value -> SA.mplace option -> st_cm_fun -> st_m_fun -> m_fun + config -> + Meta.meta -> + symbolic_value -> + SA.mplace option -> + st_cm_fun -> + st_m_fun -> + m_fun (** Expand a symbolic boolean. @@ -41,7 +52,7 @@ val expand_symbolic_adt : parameter (here, there are exactly two branches). *) val expand_symbolic_bool : - config -> + config -> Meta.meta -> symbolic_value -> SA.mplace option -> @@ -70,7 +81,7 @@ val expand_symbolic_bool : switch. The continuation is thus for the execution *after* the switch. *) val expand_symbolic_int : - config -> + config -> Meta.meta -> symbolic_value -> SA.mplace option -> -- cgit v1.2.3