diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/Cps.ml | 262 |
1 files changed, 101 insertions, 161 deletions
diff --git a/compiler/Cps.ml b/compiler/Cps.ml index a3c8f1e1..3f2e2eaa 100644 --- a/compiler/Cps.ml +++ b/compiler/Cps.ml @@ -3,6 +3,7 @@ open Values open Contexts +open Errors (** TODO: change the name *) type eval_error = EPanic @@ -36,172 +37,111 @@ type statement_eval_res = type eval_result = SymbolicAst.expression option -(** Continuation function *) -type m_fun = eval_ctx -> eval_result - -(** Continuation taking another continuation as parameter *) -type cm_fun = m_fun -> m_fun - -(** Continuation taking a typed value as parameter - TODO: use more *) -type typed_value_m_fun = typed_value -> m_fun - -(** Continuation taking another continuation as parameter and a typed - value as parameter. - *) -type typed_value_cm_fun = typed_value -> cm_fun - -(** Type of a continuation used when evaluating a statement *) -type st_m_fun = statement_eval_res -> m_fun - -(** Type of a continuation used when evaluating a statement *) -type st_cm_fun = st_m_fun -> m_fun - -(** Convert a unit function to a cm function *) -let unit_to_cm_fun (f : eval_ctx -> unit) : cm_fun = - fun cf ctx -> - f ctx; - cf ctx - -(** *) -let update_to_cm_fun (f : eval_ctx -> eval_ctx) : cm_fun = - fun cf ctx -> - let ctx = f ctx in - cf ctx - -(** Composition of functions taking continuations as parameters. - We tried to make this as general as possible. *) -let comp (f : 'c -> 'd -> 'e) (g : ('a -> 'b) -> 'c) : ('a -> 'b) -> 'd -> 'e = - fun cf ctx -> f (g cf) ctx - -let comp_unit (f : cm_fun) (g : eval_ctx -> unit) : cm_fun = - comp f (unit_to_cm_fun g) - -let comp_update (f : cm_fun) (g : eval_ctx -> eval_ctx) : cm_fun = - comp f (update_to_cm_fun g) - -(** This is just a test, to check that {!comp} is general enough to handle a case - where a function must compute a value and give it to the continuation. - It happens for functions like {!val:InterpreterExpressions.eval_operand}. - - Keeping this here also makes it a good reference, when one wants to figure - out the signatures he should use for such a composition. - *) -let comp_ret_val (f : (typed_value -> m_fun) -> m_fun) - (g : m_fun -> typed_value -> m_fun) : cm_fun = - comp f g - -let apply (f : cm_fun) (g : m_fun) : m_fun = fun ctx -> f g ctx -let id_cm_fun : cm_fun = fun cf ctx -> cf ctx - -(** If we have a list of [inputs] of type ['a list] and a function [f] which - evaluates one element of type ['a] to compute a result of type ['b] before - giving it to a continuation, the following function performs a fold operation: - it evaluates all the inputs one by one by accumulating the results in a list, - and gives the list to a continuation. - - Note that we make sure that the results are listed in the order in - which they were computed (the first element of the list is the result - of applying [f] to the first element of the inputs). - - See the unit test below for an illustration. - *) -let fold_left_apply_continuation (f : 'a -> ('c -> 'd) -> 'c -> 'd) - (inputs : 'a list) (cf : 'c -> 'd) : 'c -> 'd = - let rec eval_list (inputs : 'a list) (cf : 'c -> 'd) : 'c -> 'd = +(** Function which takes a context as input, and evaluates to: + - a new context + - a continuation with which to build the execution trace, provided the + trace for the end of the execution. + *) +type cm_fun = eval_ctx -> eval_ctx * (eval_result -> eval_result) + +type st_cm_fun = + eval_ctx -> (eval_ctx * statement_eval_res) * (eval_result -> eval_result) + +(** Type of a function used when evaluating a statement *) +type stl_cm_fun = + eval_ctx -> + (eval_ctx * statement_eval_res) list + * (SymbolicAst.expression list option -> eval_result) + +(** Compose continuations that we use to compute execution traces *) +let cc_comp (f : 'b -> 'c) (g : 'a -> 'b) : 'a -> 'c = fun e -> f (g e) + +let comp (f : 'b -> 'c) (g : 'x * ('a -> 'b)) : 'x * ('a -> 'c) = + let x, g = g in + (x, cc_comp f g) + +let comp2 (f : 'b -> 'c) (g : 'x * 'y * ('a -> 'b)) : 'x * 'y * ('a -> 'c) = + let x, y, g = g in + (x, y, cc_comp f g) + +(** [fold] operation for functions which thread a context and return a continuation *) +let fold_left_apply_continuation (f : 'a -> 'c -> 'c * ('e -> 'e)) + (inputs : 'a list) (ctx : 'c) : 'c * ('e -> 'e) = + let rec eval_list (inputs : 'a list) : 'c -> 'b = fun ctx -> match inputs with - | [] -> cf ctx - | x :: inputs -> comp (f x) (fun cf -> eval_list inputs cf) cf ctx + | [] -> (ctx, fun x -> x) + | x :: inputs -> + let ctx, cc = f x ctx in + comp cc (eval_list inputs ctx) in - eval_list inputs cf - -(** Unit test/example for {!fold_left_apply_continuation} *) -let _ = - fold_left_apply_continuation - (fun x cf (ctx : int) -> cf (ctx + x)) - [ 1; 20; 300; 4000 ] - (fun (ctx : int) -> assert (ctx = 4321)) - 0 - -(** If we have a list of [inputs] of type ['a list] and a function [f] which - evaluates one element of type ['a] to compute a result of type ['b] before - giving it to a continuation, the following function performs a fold operation: - it evaluates all the inputs one by one by accumulating the results in a list, - and gives the list to a continuation. - - Note that we make sure that the results are listed in the order in - which they were computed (the first element of the list is the result - of applying [f] to the first element of the inputs). - - See the unit test below for an illustration. - *) -let fold_left_list_apply_continuation (f : 'a -> ('b -> 'c -> 'd) -> 'c -> 'd) - (inputs : 'a list) (cf : 'b list -> 'c -> 'd) : 'c -> 'd = - let rec eval_list (inputs : 'a list) (cf : 'b list -> 'c -> 'd) - (outputs : 'b list) : 'c -> 'd = - fun ctx -> + eval_list inputs ctx + +(** [map] operation for functions which thread a context and return a continuation *) +let map_apply_continuation (f : 'a -> 'c -> 'b * 'c * ('e -> 'e)) + (inputs : 'a list) (ctx : 'c) : 'b list * 'c * ('e -> 'e) = + let rec eval_list (inputs : 'a list) (ctx : 'c) : 'b list * 'c * ('e -> 'e) = match inputs with - | [] -> cf (List.rev outputs) ctx + | [] -> ([], ctx, fun e -> e) | x :: inputs -> - comp (f x) (fun cf v -> eval_list inputs cf (v :: outputs)) cf ctx + let v, ctx, cc1 = f x ctx in + let vl, ctx, cc2 = eval_list inputs ctx in + (v :: vl, ctx, cc_comp cc1 cc2) in - eval_list inputs cf [] - -(** Unit test/example for {!fold_left_list_apply_continuation} *) -let _ = - fold_left_list_apply_continuation - (fun x cf (ctx : unit) -> cf (10 + x) ctx) - [ 0; 1; 2; 3; 4 ] - (fun values _ctx -> assert (values = [ 10; 11; 12; 13; 14 ])) - () - -(** Composition of functions taking continuations as parameters. - - We sometimes have the following situation, where we want to compose three - functions [send], [transmit] and [receive] such that: - - those three functions take continuations as parameters - - [send] generates a value and gives it to its continuation - - [receive] expects a value (so we can compose [send] and [receive] like - so: [comp send receive]) - - [transmit] doesn't expect any value and needs to be called between [send] - and [receive] - - In this situation, we need to take the value given by [send] and "transmit" - it to [receive]. - - This is what this function does (see the unit test below for an illustration). - *) -let comp_transmit (f : ('v -> 'm) -> 'n) (g : 'm -> 'm) : ('v -> 'm) -> 'n = - fun cf -> f (fun v -> g (cf v)) - -(** Example of use of {!comp_transmit} - TODO: make "real" unit tests *) -let () = - let return3 (cf : int -> unit -> unit) (ctx : unit) = cf 3 ctx in - let do_nothing (cf : unit -> unit) (ctx : unit) = cf ctx in - let consume3 (x : int) (ctx : unit) : unit = - assert (x = 3); - ctx + eval_list inputs ctx + +let opt_list_to_list_opt (len : int) (el : 'a option list) : 'a list option = + let expr_list = + List.rev + (List.fold_left + (fun acc a -> match a with Some b -> b :: acc | None -> []) + [] el) in - let cc = comp_transmit return3 do_nothing in - let cc = cc consume3 in - cc () - -(** Sometimes, we want to compose a function with a continuation which checks - its computed value and its updated context, before transmitting them + let _ = assert (List.length expr_list = len) in + if Option.is_none (List.hd expr_list) then None else Some expr_list + +let cc_singleton file line meta cf el = + match el with + | Some [ e ] -> cf (Some e) + | Some _ -> internal_error file line meta + | _ -> None + +(** It happens that we need to concatenate lists of results, for + instance when evaluating the branches of a match. When applying + the continuations to build the symbolic expressions, we need + to decompose the list of expressions we get to give it to the + individual continuations for the branches. *) -let comp_check_value (f : ('v -> 'ctx -> 'a) -> 'ctx -> 'b) - (g : 'v -> 'ctx -> unit) : ('v -> 'ctx -> 'a) -> 'ctx -> 'b = - fun cf -> - f (fun v ctx -> - g v ctx; - cf v ctx) - -(** This case is similar to {!comp_check_value}, but even simpler (we only check - the context) - *) -let comp_check_ctx (f : ('ctx -> 'a) -> 'ctx -> 'b) (g : 'ctx -> unit) : - ('ctx -> 'a) -> 'ctx -> 'b = - fun cf -> - f (fun ctx -> - g ctx; - cf ctx) +let comp_seqs (file : string) (line : int) (meta : Meta.meta) + (ls : + ('a list + * (SymbolicAst.expression list option -> SymbolicAst.expression option)) + list) : + 'a list + * (SymbolicAst.expression list option -> SymbolicAst.expression list option) + = + (* Auxiliary function: given a list of expressions el, build the expressions + corresponding to the different branches *) + let rec cc_aux ls el = + match ls with + | [] -> + (* End of the list of branches: there shouldn't be any expression remaining *) + sanity_check file line (el = []) meta; + [] + | (resl, cf) :: ls -> + (* Split the list of expressions between: + - the expressions for the current branch + - the expressions for the remaining branches *) + let el0, el = Collections.List.split_at el (List.length resl) in + (* Compute the expression for the current branch *) + let e0 = cf (Some el0) in + let e0 = + match e0 with None -> internal_error file line meta | Some e -> e + in + (* Compute the expressions for the remaining branches *) + let e = cc_aux ls el in + (* Concatenate *) + e0 :: e + in + let cc el = match el with None -> None | Some el -> Some (cc_aux ls el) in + (List.flatten (fst (List.split ls)), cc) |