diff --git a/.envrc b/.envrc new file mode 100644 index 00000000..a62ca0ac --- /dev/null +++ b/.envrc @@ -0,0 +1 @@ +eval $(opam env) diff --git a/.github/workflows/gh-pages.yml b/.github/workflows/gh-pages.yml index f0e07cbc..515f62ac 100644 --- a/.github/workflows/gh-pages.yml +++ b/.github/workflows/gh-pages.yml @@ -14,7 +14,7 @@ jobs: - name: Setup OCaml uses: ocaml/setup-ocaml@v3 with: - ocaml-compiler: 4.14.x + ocaml-compiler: 5.4.x - name: Install Opam packages run: opam pin add -n .; opam install eff --deps-only diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 0b4634e0..28770e95 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -13,7 +13,7 @@ jobs: - name: Setup OCaml uses: ocaml/setup-ocaml@v3 with: - ocaml-compiler: 4.14.x + ocaml-compiler: 5.4.x - name: Install Opam packages run: opam pin add -n .; opam install eff --deps-only @@ -22,4 +22,4 @@ jobs: run: opam exec -- make format - name: Test - run: opam exec -- make test \ No newline at end of file + run: opam exec -- make test diff --git a/.gitignore b/.gitignore index 96b67541..cb834822 100644 --- a/.gitignore +++ b/.gitignore @@ -1,4 +1,5 @@ _build +_opam # Executable eff.exe docs/try/jseff.bc.js @@ -6,6 +7,9 @@ docs/try/jseff.bc.js # Backup files *~ +# Direnv +.envrc + # Silly Mac OS X files .DS_Store @@ -17,4 +21,4 @@ docs/try/jseff.bc.js .merlin misc/code-generation-benchmarks/generate-graphs/tables/*.table -graphs.exe \ No newline at end of file +graphs.exe diff --git a/.ocamlformat b/.ocamlformat index e938c308..187e7dfc 100644 --- a/.ocamlformat +++ b/.ocamlformat @@ -1 +1 @@ -version=0.25.1 \ No newline at end of file +version=0.29.0 diff --git a/README.markdown b/README.markdown index 1b45ba79..d321d77d 100644 --- a/README.markdown +++ b/README.markdown @@ -44,7 +44,7 @@ on Windows, we just have not tested it yet. To install Eff, you need a standard Unix-style build environment as well as -1. [OCaml](https://ocaml.org/), version 4.14.1 or newer, +1. [OCaml](https://ocaml.org/), version 5.4.1 or newer, 2. [Js_of_ocaml](http://ocsigen.github.io/js_of_ocaml) compiler from OCaml bytecode to Javascript 3. its syntax extension `js_of_ocaml-ppx`, 4. [Menhir](http://gitlab.inria.fr/fpottier/menhir) LR(1) parser generator, diff --git a/dune-project b/dune-project index 057bac53..09c9cd0f 100644 --- a/dune-project +++ b/dune-project @@ -19,4 +19,4 @@ js_of_ocaml-ppx menhir (ocaml (>= 4.14.1)) - (ocamlformat (= 0.25.1)))) + (ocamlformat (= 0.29.0)))) diff --git a/eff.opam b/eff.opam index b857e368..898c4bc6 100644 --- a/eff.opam +++ b/eff.opam @@ -14,7 +14,7 @@ depends: [ "js_of_ocaml-ppx" "menhir" "ocaml" {>= "4.14.1"} - "ocamlformat" {= "0.25.1"} + "ocamlformat" {= "0.29.0"} "odoc" {with-doc} ] build: [ diff --git a/misc/code-generation-benchmarks/benchmark-suite/parserNative.ml b/misc/code-generation-benchmarks/benchmark-suite/parserNative.ml index 93885374..f62e7985 100644 --- a/misc/code-generation-benchmarks/benchmark-suite/parserNative.ml +++ b/misc/code-generation-benchmarks/benchmark-suite/parserNative.ml @@ -1,12 +1,12 @@ (*********************************** - *********** The Parser ************* - ***********************************) + *********** The Parser ************* + ***********************************) exception Fail (******************************** - * Handlers - ********************************) + * Handlers + ********************************) (* let parse = handler | val y -> (fun s -> @@ -55,8 +55,8 @@ let rec parseNum (l, v) = let rec toNum l = parseNum (l, 0) (******************************** - * Parser :: FAIL - ********************************) + * Parser :: FAIL + ********************************) (* | [] -> raise Fail | y :: ys -> @@ -83,8 +83,8 @@ let rec toNum l = parseNum (l, 0) ;; *) (******************************** - * Parser :: OPTION - ********************************) + * Parser :: OPTION + ********************************) let get_symbol c d = match d with @@ -176,8 +176,8 @@ let rec expr d = | (a2, b2) :: xs -> [ (a1 + a2, b2) ])))) (******************************** - * Example - ********************************) + * Example + ********************************) (* expr ["2"; "+"; "4"; "3"; "*"; "("; "3"; "+"; "3"; ")"];; expr ["4"; "5"; "+"];; *) diff --git a/misc/code-generation-benchmarks/benchmark-suite/partial_optimizations.ml b/misc/code-generation-benchmarks/benchmark-suite/partial_optimizations.ml index b6c87b9e..aa409b5f 100644 --- a/misc/code-generation-benchmarks/benchmark-suite/partial_optimizations.ml +++ b/misc/code-generation-benchmarks/benchmark-suite/partial_optimizations.ml @@ -120,8 +120,11 @@ let loop_incr__direct n = (let _y_60 = _x_59 in fun (_x_61 : int) -> _x_61)); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Incr -> fun () _l_64 -> @@ -159,8 +162,11 @@ let loop_incr__purity_aware n = (let _y_60 = _x_59 in fun (_x_61 : int) -> _x_61)); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Incr -> fun () _l_64 -> @@ -219,8 +225,11 @@ let loop_state__direct n = handler { effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Put -> fun (_s'_45 : int) _l_61 -> @@ -262,8 +271,11 @@ let loop_state__purity_aware n = handler { effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Put -> fun (_s'_45 : int) _l_61 -> diff --git a/misc/code-generation-benchmarks/benchmark-suite/treeOpt.ml b/misc/code-generation-benchmarks/benchmark-suite/treeOpt.ml index 133aebc9..d4f0181f 100644 --- a/misc/code-generation-benchmarks/benchmark-suite/treeOpt.ml +++ b/misc/code-generation-benchmarks/benchmark-suite/treeOpt.ml @@ -174,8 +174,11 @@ let _test_leaf_state_422 (_m_423 : int) = (fun (_x_584 : intlist) -> Value (fun (_ : intlist) -> _x_584)); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Get -> fun () _l_585 -> @@ -218,8 +221,10 @@ let _test_leaf_state_422 (_m_423 : int) = _op_173 (* @ *) _b_458 _b_594)); effect_clauses = (fun (type a b) - (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Get -> fun () _l_596 -> @@ -235,8 +240,11 @@ let _test_leaf_state_422 (_m_423 : int) = }) (_l_482 false)))); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Get -> fun () _l_495 -> @@ -309,8 +317,10 @@ let _test_leaf_state_loop_2631 (_m_2632 : int) = Value (fun (_ : intlist) -> _x_2843)); effect_clauses = (fun (type a b) - (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Get -> fun () _l_2844 -> @@ -357,14 +367,16 @@ let _test_leaf_state_loop_2631 (_m_2632 : int) = _b_2853)); effect_clauses = (fun (type a b) - (eff : - (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Get -> fun () _l_2855 -> Value - (fun (_s_2856 : intlist) -> + (fun (_s_2856 : intlist) + -> match _s_2856 with | Cons (_x_2858, _rest_2857) @@ -381,8 +393,11 @@ let _test_leaf_state_loop_2631 (_m_2632 : int) = }) (_l_2703 false)))); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) - : (a -> (b -> _) -> _) -> + (fun (type a b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Get -> fun () _l_2753 -> @@ -449,8 +464,11 @@ let _test_leaf_state_update_4890 (_m_4891 : int) = (fun (_x_5109 : intlist) -> Value (fun (_ : int) -> _x_5109)); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Get -> fun () _l_5110 -> @@ -495,8 +513,10 @@ let _test_leaf_state_update_4890 (_m_4891 : int) = _op_173 (* @ *) _b_5443 _b_5445)); effect_clauses = (fun (type a b) - (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Get -> fun () _l_5447 -> @@ -516,8 +536,11 @@ let _test_leaf_state_update_4890 (_m_4891 : int) = }) (_l_5442 false)))); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Get -> fun () _l_5453 -> @@ -591,8 +614,11 @@ let _test_leaf_state_update_loop_21688 (_m_21689 : int) = (fun (_x_21958 : intlist) -> Value (fun (_ : int) -> _x_21958)); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) - : (a -> (b -> _) -> _) -> + (fun (type a b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Get -> fun () _l_21959 -> @@ -640,9 +666,11 @@ let _test_leaf_state_update_loop_21688 (_m_21689 : int) = _b_22294)); effect_clauses = (fun (type a b) - (eff : - (a, b) eff_internal_effect) - : (a -> (b -> _) -> _) -> + (eff : + (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Get -> fun () _l_22296 -> @@ -664,8 +692,11 @@ let _test_leaf_state_update_loop_21688 (_m_21689 : int) = }) (_l_22291 false)))); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) - : (a -> (b -> _) -> _) -> + (fun (type a b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Get -> fun () _l_22302 -> diff --git a/src/00-utils/assoc.mli b/src/00-utils/assoc.mli index bf30a015..ce624505 100644 --- a/src/00-utils/assoc.mli +++ b/src/00-utils/assoc.mli @@ -15,13 +15,13 @@ val pop : ('k, 'v) t -> (('k * 'v) * ('k, 'v) t) option (** [pop assoc] returns the first element and the rest of [assoc]. *) val update : 'k -> 'v -> ('k, 'v) t -> ('k, 'v) t -(** [update k v assoc] overshadows the previous value for [k] with [v]. - If [remove k assoc] is used once, the previous value will be associated - with [k] again. *) +(** [update k v assoc] overshadows the previous value for [k] with [v]. If + [remove k assoc] is used once, the previous value will be associated with + [k] again. *) val replace : 'k -> 'v -> ('k, 'v) t -> ('k, 'v) t -(** [replace k v assoc] replaces the previous value for [k] with [v] if [k] - is associated with a value in [assoc]. *) +(** [replace k v assoc] replaces the previous value for [k] with [v] if [k] is + associated with a value in [assoc]. *) val remove : 'k -> ('k, 'v) t -> ('k, 'v) t (** [remove k assoc] removes the most recent association with [k]. *) @@ -36,8 +36,8 @@ val kmap : ('k * 'v -> 'h * 'w) -> ('k, 'v) t -> ('h, 'w) t (** [kmap f assoc] transforms each [(k, v)] in [assoc] into [f (k, v)]. *) val map_of_list : ('a -> 'k * 'v) -> 'a list -> ('k, 'v) t -(** [map_of_list f lst] transforms each element of [lst] in a pair [(k, v)] - with the function [f] and builds an association list from it. *) +(** [map_of_list f lst] transforms each element of [lst] in a pair [(k, v)] with + the function [f] and builds an association list from it. *) val fold_left : ('acc -> 'k * 'v -> 'acc) -> 'acc -> ('k, 'v) t -> 'acc (** [fold_left f acc assoc] folds [f] over [assoc] from left to right. *) @@ -47,15 +47,16 @@ val fold_right : ('k * 'v -> 'acc -> 'acc) -> ('k, 'v) t -> 'acc -> 'acc val fold_map : ('acc -> 'v -> 'acc * 'w) -> 'acc -> ('k, 'v) t -> 'acc * ('k, 'w) t -(** [fold_map f state assoc] folds from left to right ON VALUES and also maps - at the same time. *) +(** [fold_map f state assoc] folds from left to right ON VALUES and also maps at + the same time. *) val kfold_map : ('acc -> 'k * 'v -> 'acc * ('h * 'w)) -> 'acc -> ('k, 'v) t -> 'acc * ('h, 'w) t -(** [kfold_map f state assoc] folds from left to right and also maps at the same time. *) +(** [kfold_map f state assoc] folds from left to right and also maps at the same + time. *) val length : ('k, 'v) t -> int (** [length assoc] returns the length of the association list. *) @@ -65,15 +66,15 @@ val values_of : ('k, 'v) t -> 'v list order. *) val keys_of : ('k, 'v) t -> 'k list -(** [keys_of assoc] constructs a list of all keys in [assoc] in the same - order. *) +(** [keys_of assoc] constructs a list of all keys in [assoc] in the same order. +*) val rev : ('k, 'v) t -> ('k, 'v) t (** [rev assoc] reverses the order of elements in [assoc]. *) val concat : ('k, 'v) t -> ('k, 'v) t -> ('k, 'v) t -(** [concat assoc1 assoc2] joins two association lists. If keys are - repeated, the values in [assoc1] overshadow those of [assoc2]. *) +(** [concat assoc1 assoc2] joins two association lists. If keys are repeated, + the values in [assoc1] overshadow those of [assoc2]. *) val of_list : ('k * 'v) list -> ('k, 'v) t (** Switch to lists and back. *) diff --git a/src/00-utils/config.ml b/src/00-utils/config.ml index 6e02bc7e..2e99d2da 100644 --- a/src/00-utils/config.ml +++ b/src/00-utils/config.ml @@ -3,7 +3,7 @@ let version = "5.1" let use_stdlib = ref true -type backend = Runtime | Multicore | Ocaml +type backend = Runtime | Handlers | Ocaml let backend = ref Runtime let ascii = ref false diff --git a/src/00-utils/config.mli b/src/00-utils/config.mli index 0550f2d3..b6d829c0 100644 --- a/src/00-utils/config.mli +++ b/src/00-utils/config.mli @@ -6,7 +6,7 @@ val version : string val use_stdlib : bool ref (** Should we load the standard library? *) -type backend = Runtime | Multicore | Ocaml +type backend = Runtime | Handlers | Ocaml val backend : backend ref diff --git a/src/00-utils/error.mli b/src/00-utils/error.mli index 544ee44b..a2af553f 100644 --- a/src/00-utils/error.mli +++ b/src/00-utils/error.mli @@ -18,8 +18,8 @@ exception Error of t (** Exception representing all possible Eff errors. *) val fatal : ?loc:Location.t -> ('a, Format.formatter, unit, 'b) format4 -> 'a -(** Fatal errors are errors over which Eff has no control, for example when - a file cannot be opened. *) +(** Fatal errors are errors over which Eff has no control, for example when a + file cannot be opened. *) val syntax : loc:Location.t -> ('a, Format.formatter, unit, 'b) format4 -> 'a (** Syntax errors occur during lexing, parsing, or desugaring into Eff's core diff --git a/src/00-utils/graph.ml b/src/00-utils/graph.ml index 0450c626..1330340d 100644 --- a/src/00-utils/graph.ml +++ b/src/00-utils/graph.ml @@ -13,7 +13,8 @@ module MakeEdges (Vertex : Symbol.S) = struct end module Make - (Vertex : Symbol.S) (Edge : sig + (Vertex : Symbol.S) + (Edge : sig type t val print : ?safe:bool -> t -> Format.formatter -> unit @@ -80,7 +81,7 @@ struct List.iter (fun cmp -> assert (Vertex.Set.cardinal cmp >= 1)) components; let all = List.fold_right Vertex.Set.union components Vertex.Set.empty in assert (Vertex.Set.equal all (vertices graph)); - (* *) + (* *) components let toposort graph = diff --git a/src/00-utils/list.mli b/src/00-utils/list.mli index 0cea294a..559eaafe 100644 --- a/src/00-utils/list.mli +++ b/src/00-utils/list.mli @@ -20,13 +20,9 @@ val list_diff : 'a list -> 'a list -> 'a list val concat_map : ('a -> 'b list) -> 'a list -> 'b list val equal : ('a -> 'a -> bool) -> 'a list -> 'a list -> bool -(** [equal eq [a1; ...; an] [b1; ..; bm]] holds when - the two input lists have the same length, and for each - pair of elements [ai], [bi] at the same position we have - [eq ai bi]. - Note: the [eq] function may be called even if the - lists have different length. If you know your equality - function is costly, you may want to check {!compare_lengths} - first. - Natively available in: 4.12.0 -*) +(** [equal eq [a1; ...; an] [b1; ..; bm]] holds when the two input lists have + the same length, and for each pair of elements [ai], [bi] at the same + position we have [eq ai bi]. Note: the [eq] function may be called even if + the lists have different length. If you know your equality function is + costly, you may want to check {!compare_lengths} first. Natively available + in: 4.12.0 *) diff --git a/src/00-utils/print.mli b/src/00-utils/print.mli index b7f0755a..8371862d 100644 --- a/src/00-utils/print.mli +++ b/src/00-utils/print.mli @@ -31,31 +31,29 @@ val print : As an example, let us look at untyped lambda calculus, naively defined as {[ - type term = - | Var of string - | App of term * term - | Abs of string * term + type term = Var of string | App of term * term | Abs of string * term ]} - Variables are atomic constructs so we print them at the lowest level. - - Application is left associative, so we print [App (App (e1, e2), e3)] - as ["e1 e2 e3"], but [App (e1, App (e2, e3))] as ["e1 (e2 e3)"]. - We achieve this by printing [App (e1, e2)] at level 1 and limiting the - maximum level of [e1] to 1 and of [e2] to 0. + - Application is left associative, so we print [App (App (e1, e2), e3)] as + ["e1 e2 e3"], but [App (e1, App (e2, e3))] as ["e1 (e2 e3)"]. We achieve + this by printing [App (e1, e2)] at level 1 and limiting the maximum level + of [e1] to 1 and of [e2] to 0. - Lambda abstraction has the lowest precedence, so we print it at level 2. The abstraction binds everything that follows it, so the level of its body is unlimited. The most convenient way to express this is as follows. {[ - let rec print_term ?max_level e ppf = - let print ?at_level = Print.print ?max_level ?at_level ppf in - match e with - | Var x -> print "%s" x - | App (e1, e2) -> + let rec print_term ?max_level e ppf = + let print ?at_level = Print.print ?max_level ?at_level ppf in + match e with + | Var x -> print "%s" x + | App (e1, e2) -> print ~at_level:1 "%t %t" - (print_term ~max_level:1 e1) (print_term ~max_level:0 e2) - | Abs (x, e) -> print ~at_level:2 "lam %s. %t" x (print_term e) + (print_term ~max_level:1 e1) + (print_term ~max_level:0 e2) + | Abs (x, e) -> print ~at_level:2 "lam %s. %t" x (print_term e) ]} We define a recursive function [print_term ?max_level e ppf] that prints [e] at [max_level] to the pretty-printer [ppf]. Since each case will be printed @@ -85,15 +83,15 @@ val sequence : val printer_sequence : string -> (Format.formatter -> unit) list -> Format.formatter -> unit -(** [printer_sequence sep pps ppf] calls pretty-printers [pps] which have already - received all their inputs apart from the formatter and applies them to the - formatter [ppf]. This is useful for printing heterogeneous sequences, such as - substitutions, constraints, ... *) +(** [printer_sequence sep pps ppf] calls pretty-printers [pps] which have + already received all their inputs apart from the formatter and applies them + to the formatter [ppf]. This is useful for printing heterogeneous sequences, + such as substitutions, constraints, ... *) val tuple : ('a -> Format.formatter -> unit) -> 'a list -> Format.formatter -> unit -(** [tuple pp lst ppf] prints a tuple given by a list of elements [lst] using - a pretty-printer [pp] to the formatter [ppf]. *) +(** [tuple pp lst ppf] prints a tuple given by a list of elements [lst] using a + pretty-printer [pp] to the formatter [ppf]. *) val record : ('f -> Format.formatter -> unit) -> @@ -101,6 +99,6 @@ val record : ('f * 'v) list -> Format.formatter -> unit -(** [record fpp vpp lst ppf] prints a record given by an associative list of elements - [lst] using a pretty-printer [fpp] for fields and [vpp] for values to the formatter - [ppf]. *) +(** [record fpp vpp lst ppf] prints a record given by an associative list of + elements [lst] using a pretty-printer [fpp] for fields and [vpp] for values + to the formatter [ppf]. *) diff --git a/src/01-language/backend.ml b/src/01-language/backend.ml index 1c0efceb..31ab8593 100644 --- a/src/01-language/backend.ml +++ b/src/01-language/backend.ml @@ -9,7 +9,7 @@ module type S = sig val process_type_of : state -> Type.Params.t * Term.computation * Constraints.t -> state - val process_def_effect : state -> Term.effect -> state + val process_def_effect : state -> Term.eff -> state val process_top_let : state -> @@ -22,7 +22,7 @@ module type S = sig state -> Term.variable -> Primitives.primitive_value -> state val load_primitive_effect : - state -> Term.effect -> Primitives.primitive_effect -> state + state -> Term.eff -> Primitives.primitive_effect -> state val process_tydef : state -> (TyName.t, Type.type_data) Utils.Assoc.t -> state val finalize : state -> unit diff --git a/src/01-language/coercion.ml b/src/01-language/coercion.ml index ce25855c..12c41783 100644 --- a/src/01-language/coercion.ml +++ b/src/01-language/coercion.ml @@ -53,8 +53,8 @@ let applyCoercion (ty_name, tcoers) = let tys, tys' = TyParam.Map.bindings tcoers |> List.map (fun (p, (tcoer, variance)) -> - let t1, t2 = tcoer.ty in - ((p, (t1, variance)), (p, (t2, variance)))) + let t1, t2 = tcoer.ty in + ((p, (t1, variance)), (p, (t2, variance)))) |> List.split in { diff --git a/src/01-language/substitution.ml b/src/01-language/substitution.ml index 02dc7ec2..49c97e68 100644 --- a/src/01-language/substitution.ml +++ b/src/01-language/substitution.ml @@ -184,9 +184,9 @@ let of_tydef_parameters (params : Type.tydef_params) = let ty_params' = Type.TyParam.Map.bindings params.type_params |> List.map (fun (p, (skel, variance)) -> - ( p, - ( TyParam.refresh p, - (apply_substitutions_to_skeleton subst skel, variance) ) )) + ( p, + ( TyParam.refresh p, + (apply_substitutions_to_skeleton subst skel, variance) ) )) in let params' = { @@ -235,9 +235,7 @@ let of_parameters (params : Type.Params.t) = let ty_params' = Type.TyParam.Map.bindings params.ty_params |> List.map (fun (p, skel) -> - ( p, - (Type.TyParam.refresh p, apply_substitutions_to_skeleton subst skel) - )) + (p, (Type.TyParam.refresh p, apply_substitutions_to_skeleton subst skel))) in let params' = { diff --git a/src/01-language/term.ml b/src/01-language/term.ml index d1a180cd..a0858cfb 100644 --- a/src/01-language/term.ml +++ b/src/01-language/term.ml @@ -10,7 +10,7 @@ type poly_variable = (Variable.t, TyScheme.t) typed module EffectFingerprint = Symbol.Make (Symbol.Anonymous) type effect_fingerprint = EffectFingerprint.t -type effect = (Effect.t, Type.ty * Type.ty) typed +type eff = (Effect.t, Type.ty * Type.ty) typed type pattern = (pattern', Type.ty) typed @@ -81,7 +81,7 @@ and computation' = | Match of expression * abstraction list | Apply of expression * expression | Handle of expression * computation - | Call of effect * expression * abstraction + | Call of eff * expression * abstraction | Bind of computation * abstraction | CastComp of computation * Coercion.dirty_coercion | Check of Location.t * computation @@ -95,7 +95,7 @@ and handler_clauses' = { } and effect_clauses = { - effect_part : (effect, abstraction2) Assoc.t; + effect_part : (eff, abstraction2) Assoc.t; fingerprint : effect_fingerprint; } @@ -379,8 +379,8 @@ and print_let_rec_abstraction (f, abs) ppf = (Type.print_ty (Type.arrow abs.ty)) (print_let_abstraction abs) -let apply_sub_effect sub effect = - { term = effect.term; ty = Substitution.apply_sub_eff_ty sub effect.ty } +let apply_sub_effect sub eff = + { term = eff.term; ty = Substitution.apply_sub_eff_ty sub eff.ty } let rec apply_sub_comp sub computation = { @@ -398,11 +398,9 @@ and apply_sub_comp' sub computation = Match (apply_sub_exp sub e, List.map (apply_sub_abs sub) alist) | Apply (e1, e2) -> Apply (apply_sub_exp sub e1, apply_sub_exp sub e2) | Handle (e1, c1) -> Handle (apply_sub_exp sub e1, apply_sub_comp sub c1) - | Call (effect, e1, abs) -> + | Call (eff, e1, abs) -> Call - ( apply_sub_effect sub effect, - apply_sub_exp sub e1, - apply_sub_abs sub abs ) + (apply_sub_effect sub eff, apply_sub_exp sub e1, apply_sub_abs sub abs) | Bind (c1, a1) -> Bind (apply_sub_comp sub c1, apply_sub_abs sub a1) | CastComp (c1, dc1) -> CastComp (apply_sub_comp sub c1, Substitution.apply_sub_dirtycoer sub dc1) diff --git a/src/01-language/untypedSyntax.ml b/src/01-language/untypedSyntax.ml index b3f0fb20..dd963a2c 100644 --- a/src/01-language/untypedSyntax.ml +++ b/src/01-language/untypedSyntax.ml @@ -3,7 +3,7 @@ open Utils (** Syntax of the core language. *) type variable = Term.Variable.t -type effect = Effect.t +type eff = Effect.t type label = Type.Label.t type field = Type.Field.t @@ -30,7 +30,7 @@ and plain_expression = | Record of expression Type.Field.Map.t | Variant of label * expression option | Lambda of abstraction - | Effect of effect + | Effect of eff | Handler of handler and computation = plain_computation located @@ -46,7 +46,7 @@ and plain_computation = | Check of computation and handler = { - effect_clauses : (effect, abstraction2) Assoc.t; + effect_clauses : (eff, abstraction2) Assoc.t; value_clause : abstraction; finally_clause : abstraction; } @@ -127,10 +127,10 @@ and print_expression ?max_level e ppf = print ~at_level:1 "%t @[%t@]" (Type.Label.print lbl) (print_expression e) | Lambda a -> print "fun %t" (abstraction a) - | Handler h -> - print "{effect_clauses = %t; value_clause = (%t)}" - (Print.sequence " | " effect_clause (Assoc.to_list h.effect_clauses)) - (abstraction h.value_clause) + | Handler { effect_clauses = e; value_clause = v; finally_clause = f } -> + print "handler @[%t@ | %t@ | finally %t@]" + (Print.sequence "" effect_clause (Assoc.to_list e)) + (abstraction v) (abstraction f) | Effect eff -> print "%t" (Effect.print eff) and abstraction (p, c) ppf = @@ -146,7 +146,7 @@ and letrec_abstraction (v, (p, c)) ppf = and case a ppf = Format.fprintf ppf "%t" (abstraction a) and effect_clause (eff, a2) ppf = - Format.fprintf ppf "| %t -> %t" (Effect.print eff) (abstraction2 a2) + Format.fprintf ppf "| effect %t %t" (Effect.print eff) (abstraction2 a2) and abstraction2 (p1, p2, c) ppf = Format.fprintf ppf "%t %t -> %t" (print_pattern p1) (print_pattern p2) diff --git a/src/01-language/untypedSyntax.mli b/src/01-language/untypedSyntax.mli index e2217287..66f0ef47 100644 --- a/src/01-language/untypedSyntax.mli +++ b/src/01-language/untypedSyntax.mli @@ -3,7 +3,7 @@ open Utils (** Syntax of the core language. *) type variable = Term.Variable.t -type effect = Effect.t +type eff = Effect.t type label = Type.Label.t type field = Type.Field.t @@ -30,7 +30,7 @@ and plain_expression = | Record of expression Type.Field.Map.t | Variant of label * expression option | Lambda of abstraction - | Effect of effect + | Effect of eff | Handler of handler and computation = plain_computation located @@ -46,7 +46,7 @@ and plain_computation = | Check of computation and handler = { - effect_clauses : (effect, abstraction2) Assoc.t; + effect_clauses : (eff, abstraction2) Assoc.t; value_clause : abstraction; finally_clause : abstraction; } diff --git a/src/02-parser/commands.ml b/src/02-parser/commands.ml index 7cfdadde..5fb083fb 100644 --- a/src/02-parser/commands.ml +++ b/src/02-parser/commands.ml @@ -13,7 +13,7 @@ and plain_command = (** [let p1 = t1 and ... and pn = tn] *) | TopLetRec of (Sugared.variable * Sugared.term) list (** [let rec f1 p1 = t1 and ... and fn pn = tn] *) - | DefEffect of (Sugared.effect * (Sugared.ty * Sugared.ty)) + | DefEffect of (Sugared.eff * (Sugared.ty * Sugared.ty)) (** [effect Eff : ty1 -> t2] *) | Term of Sugared.term | Use of string (** [#use "filename.eff"] *) diff --git a/src/02-parser/desugarer.ml b/src/02-parser/desugarer.ml index c017518c..e8aaf94b 100644 --- a/src/02-parser/desugarer.ml +++ b/src/02-parser/desugarer.ml @@ -168,13 +168,13 @@ let syntax_to_core_params ts = let core_params = ts |> List.map (fun (p, variance) -> - let param, ty = fresh_ty_param () in - (p, (param, ty, variance))) + let param, ty = fresh_ty_param () in + (p, (param, ty, variance))) in core_params |> List.to_seq |> StringMap.of_seq -(** [desugar_tydef state params def] desugars the type definition with parameters - [params] and definition [def]. *) +(** [desugar_tydef state params def] desugars the type definition with + parameters [params] and definition [def]. *) let desugar_tydef ~loc state (ty_sbst : (T.TyParam.t * T.ty * variance) StringMap.t) ty_name def = let state', def' = @@ -259,8 +259,8 @@ let desugar_tydefs ~loc (state : state) sugared_defs = let ty_param_subs = params |> List.map (fun (pname, _) -> - ty_sbst |> StringMap.find pname |> fun (_, ty, variance) -> - (force_param ty, variance)) + ty_sbst |> StringMap.find pname |> fun (_, ty, variance) -> + (force_param ty, variance)) in ( add_unique ~loc "Type" name (sym, ty_param_subs) tyname_symbols, (name, (ty_sbst, tydef)) ) diff --git a/src/02-parser/desugarer.mli b/src/02-parser/desugarer.mli index 3df6b207..5f434bda 100644 --- a/src/02-parser/desugarer.mli +++ b/src/02-parser/desugarer.mli @@ -17,7 +17,7 @@ val desugar_computation : val desugar_def_effect : loc:Location.t -> state -> - SugaredSyntax.effect * (SugaredSyntax.ty * SugaredSyntax.ty) -> + SugaredSyntax.eff * (SugaredSyntax.ty * SugaredSyntax.ty) -> state * (Effect.t * (Type.ty * Type.ty)) val desugar_top_let : diff --git a/src/02-parser/grammar.mly b/src/02-parser/grammar.mly index 0072dce4..a3afdc38 100644 --- a/src/02-parser/grammar.mly +++ b/src/02-parser/grammar.mly @@ -4,7 +4,7 @@ open Language type handler_clause = - | EffectClause of effect * abstraction2 + | EffectClause of eff * abstraction2 | ReturnClause of abstraction | FinallyClause of abstraction @@ -106,9 +106,9 @@ plain_topdef: { Commands.TopLet defs } | LET REC defs = separated_nonempty_list(AND, let_rec_def) { Commands.TopLetRec defs } - | EFFECT eff = effect COLON t1 = prod_ty ARROW t2 = ty + | EFFECT eff = effect_sym COLON t1 = prod_ty ARROW t2 = ty { Commands.DefEffect (eff, (t1, t2))} - | EFFECT eff = effect COLON t = prod_ty + | EFFECT eff = effect_sym COLON t = prod_ty { let unit_loc = Location.make $startpos(t) $endpos(t) in Commands.DefEffect (eff, ({it= TyTuple []; at= unit_loc}, t))} @@ -218,9 +218,9 @@ plain_simple_term: { Variant (lbl, None) } | cst = const_term { Const cst } - | PERFORM LPAREN eff = effect t = term RPAREN + | PERFORM LPAREN eff = effect_sym t = term RPAREN { Effect (eff, t)} - | PERFORM eff = effect + | PERFORM eff = effect_sym { let unit_loc = Location.make $startpos(eff) $endpos(eff) in Effect (eff, {it= Tuple []; at= unit_loc})} | LBRACK ts = separated_list(SEMI, comma_term) RBRACK @@ -263,9 +263,9 @@ function_case: match_case: | p = pattern ARROW t = term { Val_match (p, t) } - | EFFECT LPAREN eff = effect p = simple_pattern RPAREN k = simple_pattern ARROW t = term + | EFFECT LPAREN eff = effect_sym p = simple_pattern RPAREN k = simple_pattern ARROW t = term { Eff_match (eff, (p, k, t)) } - | EFFECT eff = effect k = simple_pattern ARROW t = term + | EFFECT eff = effect_sym k = simple_pattern ARROW t = term { let unit_loc = Location.make $startpos(eff) $endpos(eff) in Eff_match (eff, ({it= PTuple []; at= unit_loc}, k, t)) } @@ -295,9 +295,9 @@ let_rec_def: handler_clause: mark_position(plain_handler_clause) { $1 } plain_handler_clause: - | EFFECT LPAREN eff = effect p = simple_pattern RPAREN k = simple_pattern ARROW t = term + | EFFECT LPAREN eff = effect_sym p = simple_pattern RPAREN k = simple_pattern ARROW t = term { EffectClause (eff, (p, k, t)) } - | EFFECT eff = effect k = simple_pattern ARROW t = term + | EFFECT eff = effect_sym k = simple_pattern ARROW t = term { let unit_loc = Location.make $startpos(eff) $endpos(eff) in EffectClause (eff, ({it= PTuple []; at= unit_loc}, k, t)) } | c = function_case @@ -524,7 +524,7 @@ sum_case: | lbl = UNAME OF t = ty { (lbl, Some t) } -effect: +effect_sym: | eff = UNAME { eff } diff --git a/src/02-parser/sugaredSyntax.ml b/src/02-parser/sugaredSyntax.ml index 104fef9a..572ff650 100644 --- a/src/02-parser/sugaredSyntax.ml +++ b/src/02-parser/sugaredSyntax.ml @@ -6,7 +6,7 @@ open Language type variable = string (** Terms *) -type effect = string +type eff = string type label = string type field = string type tyname = string @@ -26,7 +26,8 @@ type tydef = | TyRecord of (field, ty) Assoc.t (** [{ field1 : ty1; field2 : ty2; ...; fieldn : tyn }] *) | TySum of (label, ty option) Assoc.t - (** [Label1 of ty1 | Label2 of ty2 | ... | Labeln of tyn | Label' | Label''] *) + (** [Label1 of ty1 | Label2 of ty2 | ... | Labeln of tyn | Label' | + Label''] *) | TyInline of ty (** [ty] *) type pattern = plain_pattern located @@ -56,7 +57,7 @@ and plain_term = | Variant of label * term option (** [Label] or [Label t] *) | Lambda of abstraction (** [fun p1 p2 ... pn -> t] *) | Function of abstraction list (** [function p1 -> t1 | ... | pn -> tn] *) - | Effect of effect * term (** [eff], where [eff] is an effect symbol. *) + | Effect of eff * term (** [eff], where [eff] is an effect symbol. *) | Handler of handler (** [handler clauses], where [clauses] are described below. *) | Let of (pattern * term) list * term @@ -71,16 +72,13 @@ and plain_term = | Check of term (** [check t] *) and handler = { - effect_clauses : (effect, abstraction2) Assoc.t; + effect_clauses : (eff, abstraction2) Assoc.t; (** [t1#op1 p1 k1 -> t1' | ... | tn#opn pn kn -> tn'] *) value_clause : abstraction list; (** [val p -> t] *) finally_clause : abstraction list; (** [finally p -> t] *) } -and match_case = - | Val_match of abstraction - | Eff_match of (effect * abstraction2) - +and match_case = Val_match of abstraction | Eff_match of (eff * abstraction2) and abstraction = pattern * term and abstraction2 = pattern * pattern * term diff --git a/src/03-typechecker/exhaust.mli b/src/03-typechecker/exhaust.mli index dcf29e77..6236be05 100644 --- a/src/03-typechecker/exhaust.mli +++ b/src/03-typechecker/exhaust.mli @@ -1,9 +1,8 @@ (** Pattern matching exhaustiveness checking as described by Maranget [1]. These - functions assume that patterns are type correct, so they should be run only - after types are inferred. + functions assume that patterns are type correct, so they should be run only + after types are inferred. - [1] http://pauillac.inria.fr/~maranget/papers/warn/index.html -*) + [1] http://pauillac.inria.fr/~maranget/papers/warn/index.html *) val is_irrefutable : TypeDefinitionContext.state -> Language.UntypedSyntax.pattern -> unit @@ -14,4 +13,5 @@ val check_computation : val check_expression : TypeDefinitionContext.state -> Language.UntypedSyntax.expression -> unit -(** Check for refutable patterns in let statements and non-exhaustive match statements. *) +(** Check for refutable patterns in let statements and non-exhaustive match + statements. *) diff --git a/src/03-typechecker/infer.ml b/src/03-typechecker/infer.ml index be57c7fb..5bd4ee67 100644 --- a/src/03-typechecker/infer.ml +++ b/src/03-typechecker/infer.ml @@ -64,7 +64,7 @@ let fresh_instantiation (params : Type.Params.t) (constraints : Constraints.t) = type state = { variables : TyScheme.t Term.Variable.Map.t; - effects : Term.effect Effect.Map.t; + effects : Term.eff Effect.Map.t; type_definitions : TypeDefinitionContext.state; } diff --git a/src/03-typechecker/typeDefinitionContext.ml b/src/03-typechecker/typeDefinitionContext.ml index a3ad7c84..c1a8cc99 100644 --- a/src/03-typechecker/typeDefinitionContext.ml +++ b/src/03-typechecker/typeDefinitionContext.ml @@ -53,8 +53,8 @@ let rec find_some f = function | [] -> None | hd :: tl -> ( match f hd with Some y -> Some y | None -> find_some f tl) -(** [find_variant lbl] returns the information about the variant type that defines the - label [lbl]. *) +(** [find_variant lbl] returns the information about the variant type that + defines the label [lbl]. *) let find_variant lbl st = let construct = function | ty_name, { params; type_def = Sum vs } -> ( @@ -65,8 +65,8 @@ let find_variant lbl st = in find_some construct (Assoc.to_list st) -(** [find_field fld] returns the information about the record type that defines the field - [fld]. *) +(** [find_field fld] returns the information about the record type that defines + the field [fld]. *) let find_field fld (st : state) = let construct = function @@ -83,12 +83,12 @@ let apply_to_tydef_params tyname (ps : tydef_params) p_map = ( tyname, p_map |> TyParam.Map.map (fun p -> - let skel, variance = TyParam.Map.find p ps.type_params in - (tyParam p skel, variance)) ) + let skel, variance = TyParam.Map.find p ps.type_params in + (tyParam p skel, variance)) ) -(** [infer_variant lbl] finds a variant type that defines the label [lbl] and returns it - with refreshed type parameters and additional information needed for type - inference. *) +(** [infer_variant lbl] finds a variant type that defines the label [lbl] and + returns it with refreshed type parameters and additional information needed + for type inference. *) let infer_variant lbl st = match find_variant lbl st with | None -> assert false @@ -101,8 +101,9 @@ let infer_variant lbl st = in (u', apply_to_tydef_params ty_name ps' p_map) -(** [infer_field fld] finds a record type that defines the field [fld] and returns it with - refreshed type parameters and additional information needed for type inference. *) +(** [infer_field fld] finds a record type that defines the field [fld] and + returns it with refreshed type parameters and additional information needed + for type inference. *) let infer_field fld st = match find_field fld st with | None -> assert false @@ -115,8 +116,9 @@ let infer_field fld st = in (apply_to_tydef_params ty_name ps' p_map, (ty_name, us')) -(** [extend_type_definitions tydefs state] checks that the simulatenous type definitions [tydefs] are - well-formed and returns the extended type context. *) +(** [extend_type_definitions tydefs state] checks that the simulatenous type + definitions [tydefs] are well-formed and returns the extended type context. +*) let extend_type_definitions tydefs st = (* We wish we wrote this in eff, where we could have transactional memory. *) let extend_tydef name { params; type_def } st' = diff --git a/src/04-optimizer/optimizer.ml b/src/04-optimizer/optimizer.ml index f6069343..70900e82 100644 --- a/src/04-optimizer/optimizer.ml +++ b/src/04-optimizer/optimizer.ml @@ -470,8 +470,7 @@ and reduce_computation' state comp = Type.Tuple [ _; - ({ term = Type.Arrow (ty_in, _); _ } as - ty_cont); + ({ term = Type.Arrow (ty_in, _); _ } as ty_cont); ]; _; }, diff --git a/src/05-backends/multicore-ocaml/dune b/src/05-backends/ocaml-handlers/dune similarity index 87% rename from src/05-backends/multicore-ocaml/dune rename to src/05-backends/ocaml-handlers/dune index 89fd856d..d9ecf078 100644 --- a/src/05-backends/multicore-ocaml/dune +++ b/src/05-backends/ocaml-handlers/dune @@ -1,5 +1,5 @@ (library - (name multicoreOCaml) + (name ocamlHandlers) (libraries language typechecker)) (rule diff --git a/src/05-backends/multicore-ocaml/multicoreOCaml.ml b/src/05-backends/ocaml-handlers/ocamlHandlers.ml similarity index 92% rename from src/05-backends/multicore-ocaml/multicoreOCaml.ml rename to src/05-backends/ocaml-handlers/ocamlHandlers.ml index be33d483..e10d9700 100644 --- a/src/05-backends/multicore-ocaml/multicoreOCaml.ml +++ b/src/05-backends/ocaml-handlers/ocamlHandlers.ml @@ -1,4 +1,4 @@ -(* Compilation to multicore ocaml *) +(* Compilation to ocaml handlers *) open Utils @@ -9,8 +9,7 @@ module Backend : Language.Backend.S = struct type state = { prog : Syntax.cmd list; primitive_effects : - (Syntax.effect * (Syntax.ty * Syntax.ty) * (string * string * string)) - list; + (Syntax.eff * (Syntax.ty * Syntax.ty) * (string * string * string)) list; } let initial_state = { prog = []; primitive_effects = [] } @@ -42,7 +41,7 @@ module Backend : Language.Backend.S = struct let process_type_of state _ = Print.warning - "[#typeof] commands are ignored when compiling to Multicore OCaml."; + "[#typeof] commands are ignored when compiling to OCaml Handlers."; state let process_def_effect state eff = diff --git a/src/05-backends/multicore-ocaml/multicoreOCaml.mli b/src/05-backends/ocaml-handlers/ocamlHandlers.mli similarity index 100% rename from src/05-backends/multicore-ocaml/multicoreOCaml.mli rename to src/05-backends/ocaml-handlers/ocamlHandlers.mli diff --git a/src/05-backends/multicore-ocaml/primitives.ml b/src/05-backends/ocaml-handlers/primitives.ml similarity index 100% rename from src/05-backends/multicore-ocaml/primitives.ml rename to src/05-backends/ocaml-handlers/primitives.ml diff --git a/src/05-backends/multicore-ocaml/stdlib.eff b/src/05-backends/ocaml-handlers/stdlib.eff similarity index 100% rename from src/05-backends/multicore-ocaml/stdlib.eff rename to src/05-backends/ocaml-handlers/stdlib.eff diff --git a/src/05-backends/multicore-ocaml/symbol.ml b/src/05-backends/ocaml-handlers/symbol.ml similarity index 100% rename from src/05-backends/multicore-ocaml/symbol.ml rename to src/05-backends/ocaml-handlers/symbol.ml diff --git a/src/05-backends/multicore-ocaml/syntax.ml b/src/05-backends/ocaml-handlers/syntax.ml similarity index 79% rename from src/05-backends/multicore-ocaml/syntax.ml rename to src/05-backends/ocaml-handlers/syntax.ml index dafdb6f8..e2f270ee 100644 --- a/src/05-backends/multicore-ocaml/syntax.ml +++ b/src/05-backends/ocaml-handlers/syntax.ml @@ -5,11 +5,11 @@ module Print = Utils.Print type variable = Term.Variable.t (** Syntax of the core language. *) -type effect = Effect.t +type eff = Effect.t type label = Type.Label.t type field = Type.Field.t -(** Types used by MulticoreOcaml. *) +(** Types used by OcamlHandlers. *) type ty = | TyApply of TyName.t * ty list | TyParam of Type.TyParam.t @@ -43,7 +43,7 @@ type term = | Variant of label * term option | Lambda of abstraction | Function of match_case list - | Effect of effect + | Effect of eff | Let of (pattern * term) list * term | LetRec of (variable * abstraction) list * term | Match of term * match_case list @@ -52,7 +52,7 @@ type term = and match_case = | ValueClause of abstraction - | EffectClause of effect * abstraction2 + | EffectClause of eff * abstraction2 and abstraction = pattern * term (** Abstractions that take one argument. *) @@ -62,7 +62,7 @@ and abstraction2 = pattern * pattern * term type cmd = | Term of term - | DefEffect of effect * (ty * ty) + | DefEffect of eff * (ty * ty) | TopLet of (pattern * term) list | TopLetRec of (variable * abstraction) list | RawSource of (variable * string) @@ -96,43 +96,50 @@ let print_record pp sep assoc ppf = let lst = Type.Field.Map.bindings assoc in print ppf "{@[%t@]}" (print_sequence "; " (print_field pp sep) lst) -let rec print_term t ppf = +let rec print_term ?max_level t ppf = + let print ?at_level = Print.print ?max_level ?at_level ppf in match t with - | Var x -> print ppf "%t" (Symbol.print_variable x) - | Const c -> print ppf "%t" (Const.print c) - | Annotated (t, ty) -> print ppf "(%t : %t)" (print_term t) (print_type ty) - | Tuple lst -> print ppf "%t" (print_tuple print_term lst) - | Record assoc -> print ppf "%t" (print_record print_term "=" assoc) - | Variant (lbl, None) when lbl = Type.nil -> print ppf "[]" - | Variant (lbl, None) -> print ppf "%t" (Symbol.print_label lbl) + | Var x -> print "%t" (Symbol.print_variable x) + | Const c -> print "%t" (Const.print c) + | Annotated (t, ty) -> + print ~at_level:1 "%t : %t" (print_term ~max_level:0 t) (print_type ty) + | Tuple lst -> print "%t" (print_tuple print_term lst) + | Record assoc -> print "%t" (print_record print_term "=" assoc) + | Variant (lbl, None) when lbl = Type.nil -> print "[]" + | Variant (lbl, None) -> print "%t" (Symbol.print_label lbl) | Variant (lbl, Some (Tuple [ hd; tl ])) when lbl = Type.cons -> - print ppf "@[(%t::%t)@]" (print_term hd) (print_term tl) + print "@[(%t::%t)@]" (print_term ~max_level:0 hd) (print_term tl) | Variant (lbl, Some t) -> - print ppf "(%t @[%t@])" (Symbol.print_label lbl) (print_term t) - | Lambda a -> print ppf "@[fun %t@]" (print_abstraction a) + print ~at_level:1 "%t @[%t@]" (Symbol.print_label lbl) + (print_term ~max_level:0 t) + | Lambda a -> print ~at_level:1 "@[fun %t@]" (print_abstraction a) | Function lst -> - print ppf "@[(function @, | %t)@]" + print ~at_level:1 "@[function @, | %t@]" (print_sequence "@, | " print_case lst) - | Effect eff -> print ppf "%t" (Symbol.print_effect eff) + | Effect eff -> print "%t" (Symbol.print_effect eff) | Let (lst, t) -> - print ppf "@[@[%tin@] @,%t@]" (print_let lst) (print_term t) + print ~at_level:1 "@[@[%tin@] @,%t@]" (print_let lst) + (print_term t) | LetRec (lst, t) -> - print ppf "@[@[%tin@] @,%t@]" (print_let_rec lst) (print_term t) + print ~at_level:1 "@[@[%tin@] @,%t@]" (print_let_rec lst) + (print_term t) | Match (t, []) -> (* Absurd case *) - print ppf "@[(match %t with | _ -> assert false)@]" (print_term t) + print ~at_level:1 "@[match %t with | _ -> assert false@]" + (print_term t) | Match (t, lst) -> - print ppf "@[(match %t with@, | %t)@]" (print_term t) + print ~at_level:1 "@[match %t with@, | %t@]" (print_term t) (print_sequence "@, | " print_case lst) - | Apply (Effect eff, (Lambda _ as t2)) -> - print ppf "perform (%t (%t))" (Symbol.print_effect eff) (print_term t2) | Apply (Effect eff, t2) -> - print ppf "perform (%t %t)" (Symbol.print_effect eff) (print_term t2) + print ~at_level:1 "perform (%t %t)" (Symbol.print_effect eff) + (print_term ~max_level:0 t2) | Apply (t1, t2) -> - print ppf "@[(%t) @,(%t)@]" (print_term t1) (print_term t2) + print ~at_level:1 "@[%t @,%t@]" + (print_term ~max_level:0 t1) + (print_term ~max_level:0 t2) | Check _t -> Print.warning - "[#check] commands are ignored when compiling to Multicore OCaml." + "[#check] commands are ignored when compiling to OCaml Handlers." and print_pattern p ppf = match p with @@ -191,8 +198,8 @@ and print_tydef (name, (params, tydef)) ppf = (Symbol.print_tyname name) (print_def tydef) and print_def_effect (eff, (ty1, ty2)) ppf = - print ppf "@[effect %t : %t ->@ %t@]@." (Symbol.print_effect eff) - (print_type ty1) (print_type ty2) + print ppf "@[type _ Effect.t += %t : %t ->@ %t Effect.t@]@." + (Symbol.print_effect eff) (print_type ty1) (print_type ty2) and print_top_let defs ppf = print ppf "@[%t@]@." (print_let defs) and print_top_let_rec defs ppf = print ppf "@[%t@]@." (print_let_rec defs) @@ -255,19 +262,20 @@ and print_case case ppf = | ValueClause abs -> print ppf "@[%t@]" (print_abstraction abs) | EffectClause (eff, (p1, p2, t)) -> if p2 = PNonbinding then - print ppf "@[effect (%t %t) %t -> @,%t@]" + print ppf "@[effect (%t %t), %t -> @,%t@]" (Symbol.print_effect eff) (print_pattern p1) (print_pattern p2) (print_term t) else print ppf - ("@[effect (%t %t) %t ->@," - ^^ "(let %t x = continue (Obj.clone_continuation %t) x in @,%t)@]") + ("@[effect (%t %t), %t ->@," + ^^ "(let %t x = continue (Multicont.Deep.clone_continuation %t) x in @,\ + %t)@]") (Symbol.print_effect eff) (print_pattern p1) (print_pattern p2) (print_pattern p2) (print_pattern p2) (print_term t) let print_top_handler cases ppf = let print_top_handler_case (eff, _, (x, k, t)) ppf = - print ppf " | effect (%t %s) %s -> %s" (Symbol.print_effect eff) x k t + print ppf " | effect (%t %s), %s -> %s" (Symbol.print_effect eff) x k t in print ppf "let _ocaml_tophandler c =\n match c () with\n%t\n | x -> x\n" (Print.sequence "" print_top_handler_case cases) @@ -283,7 +291,7 @@ let print_cmd cmd ppf = match cmd with | Term t -> print ppf "let _ = @.@[(_ocaml_tophandler) (fun _ -> @,%t@,)@];;@." - (print_term t) + (print_term ~max_level:1 t) | DefEffect (eff, (ty1, ty2)) -> print_def_effect (eff, (ty1, ty2)) ppf | TopLet defs -> print_top_let defs ppf | TopLetRec defs -> print_top_let_rec defs ppf diff --git a/src/05-backends/multicore-ocaml/syntax.mli b/src/05-backends/ocaml-handlers/syntax.mli similarity index 87% rename from src/05-backends/multicore-ocaml/syntax.mli rename to src/05-backends/ocaml-handlers/syntax.mli index 45c6bedb..eb5e3fbe 100644 --- a/src/05-backends/multicore-ocaml/syntax.mli +++ b/src/05-backends/ocaml-handlers/syntax.mli @@ -1,11 +1,11 @@ open Language type variable = Term.Variable.t -type effect = Effect.t +type eff = Effect.t type label = Type.Label.t type field = Type.Field.t -(** Types used by MulticoreOcaml. *) +(** Types used by OcamlHandlers. *) type ty = | TyApply of TyName.t * ty list | TyParam of Type.TyParam.t @@ -39,7 +39,7 @@ type term = | Variant of label * term option | Lambda of abstraction | Function of match_case list - | Effect of effect + | Effect of eff | Let of (pattern * term) list * term | LetRec of (variable * abstraction) list * term | Match of term * match_case list @@ -48,7 +48,7 @@ type term = and match_case = | ValueClause of abstraction - | EffectClause of effect * abstraction2 + | EffectClause of eff * abstraction2 and abstraction = pattern * term (** Abstractions that take one argument. *) @@ -58,14 +58,14 @@ and abstraction2 = pattern * pattern * term type cmd = | Term of term - | DefEffect of effect * (ty * ty) + | DefEffect of eff * (ty * ty) | TopLet of (pattern * term) list | TopLetRec of (variable * abstraction) list | RawSource of (variable * string) | TyDef of (label * (Type.TyParam.t list * tydef)) list val print_header : - (effect * (ty * ty) * (string * string * string)) list -> + (eff * (ty * ty) * (string * string * string)) list -> Format.formatter -> unit diff --git a/src/05-backends/multicore-ocaml/translate.ml b/src/05-backends/ocaml-handlers/translate.ml similarity index 100% rename from src/05-backends/multicore-ocaml/translate.ml rename to src/05-backends/ocaml-handlers/translate.ml diff --git a/src/05-backends/multicore-ocaml/translate.mli b/src/05-backends/ocaml-handlers/translate.mli similarity index 100% rename from src/05-backends/multicore-ocaml/translate.mli rename to src/05-backends/ocaml-handlers/translate.mli diff --git a/src/05-backends/plain-ocaml/noEffOptimizer.ml b/src/05-backends/plain-ocaml/noEffOptimizer.ml index fded5596..7a7db87d 100644 --- a/src/05-backends/plain-ocaml/noEffOptimizer.ml +++ b/src/05-backends/plain-ocaml/noEffOptimizer.ml @@ -113,9 +113,9 @@ let naive_lambda_lift state e = let subs = leafs |> List.filter_map (fun (x, _) -> - Option.map - (fun x -> (x, NoEff.NVar { variable = v; coercions = [] })) - x) + Option.map + (fun x -> (x, NoEff.NVar { variable = v; coercions = [] })) + x) |> Assoc.of_list in NoEff.NFun (p, ty, sub_leafs subs e)) diff --git a/src/05-backends/plain-ocaml/plainOCaml.ml b/src/05-backends/plain-ocaml/plainOCaml.ml index 6c40b77f..26f962b8 100644 --- a/src/05-backends/plain-ocaml/plainOCaml.ml +++ b/src/05-backends/plain-ocaml/plainOCaml.ml @@ -1,4 +1,4 @@ -(* Compilation to multicore ocaml *) +(* Compilation to plain ocaml *) open Utils module Term = Language.Term module Type = Language.Type @@ -26,7 +26,7 @@ module Backend : Language.Backend.S = struct no_eff_optimizer_state : NoEffOptimizer.state; primitive_values : (Language.Term.Variable.t, Language.Primitives.primitive_value) Assoc.t; - primitive_effects : Term.effect list; + primitive_effects : Term.eff list; } let initial_state = diff --git a/src/05-backends/runtime/eval.mli b/src/05-backends/runtime/eval.mli index 65ae52fb..336eead6 100644 --- a/src/05-backends/runtime/eval.mli +++ b/src/05-backends/runtime/eval.mli @@ -10,4 +10,4 @@ val eval_expression : state -> Term.expression -> Value.value val run : state -> Term.computation -> Value.value val update : Language.Term.Variable.t -> Value.value -> state -> state val lookup : Term.variable -> state -> Value.value option -val add_runner : Term.effect -> (Value.value -> Value.value) -> state -> state +val add_runner : Term.eff -> (Value.value -> Value.value) -> state -> state diff --git a/src/05-backends/runtime/primitives.ml b/src/05-backends/runtime/primitives.ml index ec9928e1..004f5938 100644 --- a/src/05-backends/runtime/primitives.ml +++ b/src/05-backends/runtime/primitives.ml @@ -17,8 +17,8 @@ let value_fun f = V.Value (from_fun f) nested closures. *) let binary_closure f = from_fun (fun v1 -> value_fun (fun v2 -> f v1 v2)) -(** [ternary_closure f] converts a function [f] that takes three values into three - nested closures. *) +(** [ternary_closure f] converts a function [f] that takes three values into + three nested closures. *) let ternary_closure f = from_fun (fun v1 -> value_fun (fun v2 -> value_fun (fun v3 -> f v1 v2 v3))) @@ -28,12 +28,12 @@ let int_int_to_int f = let int_f v1 v2 = value_int (f (V.to_int v1) (V.to_int v2)) in binary_closure int_f -(** [int_to_int f] takes a unary integer function f and transforms it into - a closure that takes two values and evaluates to a value. *) +(** [int_to_int f] takes a unary integer function f and transforms it into a + closure that takes two values and evaluates to a value. *) let int_to_int f = from_fun (fun v -> value_int (f (V.to_int v))) -(** [float_to_float f] takes a unary float function f and transforms it into - a closure that takes two values and evaluates to a value. *) +(** [float_to_float f] takes a unary float function f and transforms it into a + closure that takes two values and evaluates to a value. *) let float_to_float f = from_fun (fun v -> value_float (f (V.to_float v))) (** [float_float_to_float f] takes a binary float function f and transforms it diff --git a/src/eff/dune b/src/eff/dune index ad9261c0..012e763c 100644 --- a/src/eff/dune +++ b/src/eff/dune @@ -1,7 +1,7 @@ (executable (name eff) (public_name eff) - (libraries utils language runtime multicoreOCaml plainOCaml loader unix) + (libraries utils language runtime ocamlHandlers plainOCaml loader unix) (promote (until-clean) (into ../../))) diff --git a/src/eff/eff.ml b/src/eff/eff.ml index f0206483..350fe2d8 100644 --- a/src/eff/eff.ml +++ b/src/eff/eff.ml @@ -34,9 +34,9 @@ let options = ( "--no-header", Arg.Clear Config.include_header_open, " Do not include open OcamlHeader in generated files" ); - ( "--compile-multicore-ocaml", - Arg.Unit (fun () -> Config.backend := Multicore), - " Compile the Eff code into a Multicore OCaml (sent to standard output)" + ( "--compile-ocaml-handlers", + Arg.Unit (fun () -> Config.backend := Handlers), + " Compile the Eff code into OCaml 5 handlers (sent to standard output)" ); ( "--compile-plain-ocaml", Arg.Unit (fun () -> Config.backend := Ocaml), @@ -188,7 +188,7 @@ let main = let (module Backend : Language.Backend.S) = match !Config.backend with | Config.Runtime -> (module Runtime.Backend) - | Config.Multicore -> (module MulticoreOCaml.Backend) + | Config.Handlers -> (module OcamlHandlers.Backend) | Config.Ocaml -> (module PlainOCaml.Backend) in let (module Shell) = @@ -206,7 +206,7 @@ let main = let stdlib = match !Config.backend with | Config.Runtime | Config.Ocaml -> Loader.Stdlib_eff.source - | Config.Multicore -> MulticoreOCaml.stdlib + | Config.Handlers -> OcamlHandlers.stdlib in Shell.load_source stdlib state else state diff --git a/src/jseff/jseff.ml b/src/jseff/jseff.ml index 2dc3e3e6..bdfe983e 100644 --- a/src/jseff/jseff.ml +++ b/src/jseff/jseff.ml @@ -15,25 +15,25 @@ module Shell = Loader.Shell.Make (Runtime.Backend) (* Export the interface to Javascript. *) let _ = Js.export "jseff" - (object%js - method initialize echo = - Config.output_formatter := js_formatter "[;#00a8ff;#192a56]" echo; - Config.error_formatter := js_formatter "[b;#e84118;#192a56]" echo; - let state = Shell.initialize () in - let state = Shell.load_source Loader.Stdlib_eff.source state in - Format.fprintf !Config.output_formatter "eff %s@." Config.version; - Format.fprintf !Config.output_formatter "[Type #help for help.]@."; - state + object%js + method initialize echo = + Config.output_formatter := js_formatter "[;#00a8ff;#192a56]" echo; + Config.error_formatter := js_formatter "[b;#e84118;#192a56]" echo; + let state = Shell.initialize () in + let state = Shell.load_source Loader.Stdlib_eff.source state in + Format.fprintf !Config.output_formatter "eff %s@." Config.version; + Format.fprintf !Config.output_formatter "[Type #help for help.]@."; + state - method executeSource state source = - try Shell.execute_source (Js.to_string source) state - with Error.Error err -> - Error.print err; - state + method executeSource state source = + try Shell.execute_source (Js.to_string source) state + with Error.Error err -> + Error.print err; + state - method loadSource state source = - try Shell.load_source (Js.to_string source) state - with Error.Error err -> - Error.print err; - state - end) + method loadSource state source = + try Shell.load_source (Js.to_string source) state + with Error.Error err -> + Error.print err; + state + end diff --git a/tests/format_generated_code.t b/tests/format_generated_code.t index ebd07791..7882345f 100644 --- a/tests/format_generated_code.t +++ b/tests/format_generated_code.t @@ -66,7 +66,12 @@ { value_clause = (fun (_x : int) -> Value _x); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Decide -> fun (() : unit) _k -> @@ -118,89 +123,96 @@ let rec _op (* @ *) _x = Value (fun (_ys : triple_int_list) -> - match _x with + begin match _x with | TripleNil -> Value _ys | TripleCons (_x, _xs) -> _op (* @ *) _xs >>= fun _b -> - _b _ys >>= fun _b -> Value (TripleCons (_x, _b))) + _b _ys >>= fun _b -> Value (TripleCons (_x, _b)) + end) let _op (* @ *) = _op (* @ *) - let _testTriple (_n : int) (_s : int) = - let rec _choice _x = - coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( < ) _x) - >>= fun _b -> - _b 1 >>= fun _b -> - if _b then - Call - (TripleFail, (), fun (_y : empty) -> match _y with _ -> assert false) - else - Call - ( TripleFlip, - (), - fun (_y : bool) -> - if _y then Value _x - else - coer_return - (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) - (( - ) _x) - >>= fun _b -> - _b 1 >>= fun _b -> _choice _b ) - in - (handler - { - value_clause = (fun (_id : triple_int_list) -> Value _id); - effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> - match eff with - | TripleFail -> fun (_ : unit) _k -> Value TripleNil - | TripleFlip -> - fun (() : unit) _k -> - _k true >>= fun _xs -> - _k false >>= fun _ys -> - _op (* @ *) _xs >>= fun _b -> _b _ys - | eff' -> fun arg k -> Call (eff', arg, k)); - } - (fun (_x : triple_int_list) -> Value _x)) - ( _choice _n >>= fun _i -> - coer_return - (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) - (( - ) _i) - >>= fun _b -> - _b 1 >>= fun _b -> - _choice _b >>= fun _j -> - coer_return - (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) - (( - ) _j) - >>= fun _b -> - _b 1 >>= fun _b -> - _choice _b >>= fun _k -> - coer_return - (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) - (( + ) _i) - >>= fun _b -> - _b _j >>= fun _b -> - coer_return - (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) - (( + ) _b) - >>= fun _b -> - _b _k >>= fun _b -> - coer_return - (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) - (( = ) _b) - >>= fun _b -> - _b _s >>= fun _b -> - (if _b then Value (_i, _j, _k) - else - Call - ( TripleFail, - (), - fun (_y : empty) -> match _y with _ -> assert false )) - >>= fun _r -> Value (TripleCons (_r, TripleNil)) ) + let _testTriple = + fun (_n : int) -> + fun (_s : int) -> + let rec _choice _x = + coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( < ) _x) + >>= fun _b -> + _b 1 >>= fun _b -> + if _b then + Call + (TripleFail, (), fun (_y : empty) -> match _y with _ -> assert false) + else + Call + ( TripleFlip, + (), + fun (_y : bool) -> + if _y then Value _x + else + coer_return + (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) + (( - ) _x) + >>= fun _b -> + _b 1 >>= fun _b -> _choice _b ) + in + (handler + { + value_clause = (fun (_id : triple_int_list) -> Value _id); + effect_clauses = + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> + match eff with + | TripleFail -> fun (_ : unit) _k -> Value TripleNil + | TripleFlip -> + fun (() : unit) _k -> + _k true >>= fun _xs -> + _k false >>= fun _ys -> + _op (* @ *) _xs >>= fun _b -> _b _ys + | eff' -> fun arg k -> Call (eff', arg, k)); + } + (fun (_x : triple_int_list) -> Value _x)) + ( _choice _n >>= fun _i -> + coer_return + (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) + (( - ) _i) + >>= fun _b -> + _b 1 >>= fun _b -> + _choice _b >>= fun _j -> + coer_return + (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) + (( - ) _j) + >>= fun _b -> + _b 1 >>= fun _b -> + _choice _b >>= fun _k -> + coer_return + (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) + (( + ) _i) + >>= fun _b -> + _b _j >>= fun _b -> + coer_return + (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) + (( + ) _b) + >>= fun _b -> + _b _k >>= fun _b -> + coer_return + (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) + (( = ) _b) + >>= fun _b -> + _b _s >>= fun _b -> + (if _b then Value (_i, _j, _k) + else + Call + ( TripleFail, + (), + fun (_y : empty) -> match _y with _ -> assert false )) + >>= fun _r -> Value (TripleCons (_r, TripleNil)) ) let testTriple = _testTriple - let _handleTripleWrap ((_x, _y) : int * int) = _testTriple _x _y + let _handleTripleWrap = fun ((_x, _y) : int * int) -> _testTriple _x _y let handleTripleWrap = _handleTripleWrap type queen = int * int @@ -213,82 +225,99 @@ let rec _filter _x = Value (fun (_x : intlist) -> - match _x with + begin match _x with | End -> Value End | Lst (_x, _xs) -> _x _x >>= fun _b -> if _b then _filter _x >>= fun _b -> _b _xs >>= fun _b -> Value (Lst (_x, _b)) - else _filter _x >>= fun _b -> _b _xs) + else _filter _x >>= fun _b -> _b _xs + end) let filter = _filter let rec _forall _x = Value (fun (_x : queen_list) -> - match _x with + begin match _x with | Nil -> Value true | Cons (_x, _xs) -> _x _x >>= fun _b -> - if _b then _forall _x >>= fun _b -> _b _xs else Value false) + if _b then _forall _x >>= fun _b -> _b _xs else Value false + end) let forall = _forall - let _no_attack ((_x, _y) : int * int) ((_x', _y') : int * int) = - coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( <> ) _x) - >>= fun _b -> - _b _x' >>= fun _b -> - if _b then - coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( <> ) _y) - >>= fun _b -> - _b _y' >>= fun _b -> - if _b then - coer_return - (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) - (( - ) _x) - >>= fun _b -> - _b _x' >>= fun _b -> - coer_return - (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) - (( <> ) (abs _b)) - >>= fun _b -> - coer_return - (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) - (( - ) _y) - >>= fun _b -> - _b _y' >>= fun _b -> _b (abs _b) - else Value false - else Value false + let _no_attack = + fun ((_x, _y) : int * int) -> + fun ((_x', _y') : int * int) -> + coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( <> ) _x) + >>= fun _b -> + _b _x' >>= fun _b -> + if _b then + coer_return + (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) + (( <> ) _y) + >>= fun _b -> + _b _y' >>= fun _b -> + if _b then + coer_return + (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) + (( - ) _x) + >>= fun _b -> + _b _x' >>= fun _b -> + coer_return + (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) + (( <> ) (abs _b)) + >>= fun _b -> + coer_return + (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) + (( - ) _y) + >>= fun _b -> + _b _y' >>= fun _b -> _b (abs _b) + else Value false + else Value false let no_attack = _no_attack - let _available (_x : int) (_qs : queen_list) (_l : intlist) = - _filter (fun (_y : int) -> _forall (_no_attack (_x, _y)) >>= fun _b -> _b _qs) - >>= fun _b -> _b _l + let _available = + fun (_x : int) -> + fun (_qs : queen_list) -> + fun (_l : intlist) -> + _filter (fun (_y : int) -> + _forall (_no_attack (_x, _y)) >>= fun _b -> _b _qs) + >>= fun _b -> _b _l let available = _available - let _find_solution (_n : int) = + let _find_solution = + fun (_n : int) -> (handler { value_clause = (fun (_id : option) -> Value _id); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Select -> fun (_lst : intlist) _k -> let rec _loop _x = Value (fun (_x : intlist) -> - match _x with + begin match _x with | End -> Value None - | Lst (_x, _xs) -> ( + | Lst (_x, _xs) -> _x _x >>= fun _b -> - match _b with + begin match _b with | None -> _loop _x >>= fun _b -> _b _xs - | Some _x -> Value (Some _x))) + | Some _x -> Value (Some _x) + end + end) in _loop _k >>= fun _b -> _b _lst | eff' -> fun arg k -> Call (eff', arg, k)); @@ -345,7 +374,10 @@ _place (1, Nil)) let find_solution = _find_solution - let _queens_all (_number_of_queens : int) = _find_solution _number_of_queens + + let _queens_all = + fun (_number_of_queens : int) -> _find_solution _number_of_queens + let queens_all = _queens_all type (_, _) eff_internal_effect += CountPut : (int, unit) eff_internal_effect @@ -372,7 +404,8 @@ let count = _count - let _testCount (_m : int) = + let _testCount = + fun (_m : int) -> (handler { value_clause = @@ -381,8 +414,12 @@ (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (fun (_x : int) -> _x)); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | CountGet -> fun (() : unit) _k -> @@ -407,7 +444,8 @@ type (_, _) eff_internal_effect += | GeneratorYield : (int, unit) eff_internal_effect - let _testGenerator (_n : int) = + let _testGenerator = + fun (_n : int) -> let rec _generateFromTo (_l, _u) = coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( > ) _l) >>= fun _b -> @@ -432,8 +470,12 @@ (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (fun (_s : int) -> _s)); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | GeneratorPut -> fun (_s' : int) _k -> @@ -448,8 +490,12 @@ { value_clause = (fun (_id : unit) -> Value _id); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | GeneratorYield -> fun (_e : int) _k -> @@ -493,11 +539,12 @@ type (_, _) eff_internal_effect += | Write : (string * string, unit) eff_internal_effect - let _compose _tycoer _tycoer _tycoer _tycoer _tycoer - (_f : 'ty12 -> 'ty13 computation) (_g : 'ty10 -> 'ty11 computation) - (_x : 'ty6) = - coer_computation _tycoer (coer_computation _tycoer (_g (_tycoer _x))) - >>= fun _b -> coer_computation _tycoer (_f (_tycoer _b)) + let _compose _tycoer _tycoer _tycoer _tycoer _tycoer = + fun (_f : 'ty12 -> 'ty13 computation) -> + fun (_g : 'ty10 -> 'ty11 computation) -> + fun (_x : 'ty6) -> + coer_computation _tycoer (coer_computation _tycoer (_g (_tycoer _x))) + >>= fun _b -> coer_computation _tycoer (_f (_tycoer _b)) let compose = _compose ====================================================================== @@ -525,11 +572,16 @@ type a = Nil | Cons of (int * a) - let _f (_x : int) = match _x with 1 -> Value 0 | _ -> Value 4 + let _f = + fun (_x : int) -> + begin match _x with 1 -> Value 0 | _ -> Value 4 + end + let f = _f - let _g (_a : a) = - (match _a with + let _g = + fun (_a : a) -> + begin match _a with | Nil -> Value 0 | Cons (_x, Nil) -> coer_return @@ -537,7 +589,8 @@ (( + ) _x) >>= fun _b -> _b 4 | Cons (4, _x) -> Value 7 - | _x -> Value 13) + | _x -> Value 13 + end >>= fun _a0 -> coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( + ) 3) >>= fun _b -> @@ -569,7 +622,8 @@ type int_list = Nil | Cons of (int * int_list) - let _f (_y : int_list) = + let _f = + fun (_y : int_list) -> (handler { value_clause = @@ -579,16 +633,20 @@ (( + ) _x) >>= fun _b -> _b 10); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> - match eff with eff' -> fun arg k -> Call (eff', arg, k)); + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with eff' -> fun arg k -> Call (eff', arg, k)); } (fun (_x : int) -> Value _x)) - (match _y with + begin match _y with | Nil -> Value 1 | Cons (_x, Nil) -> Value _x | Cons (_, Cons (_y, Nil)) -> Value _y - | Cons (_x, _) -> Value _x) + | Cons (_x, _) -> Value _x + end let f = _f;; @@ -601,8 +659,12 @@ (( + ) _x) >>= fun _b -> _b 10); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : (a -> (b -> _) -> _) -> - match eff with eff' -> fun arg k -> Call (eff', arg, k)); + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with eff' -> fun arg k -> Call (eff', arg, k)); } (fun (_x : int) -> Value _x)) (Value 4) @@ -651,7 +713,12 @@ { value_clause = (fun (_id : int) -> Value _id); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Eff -> fun (() : unit) _k -> @@ -680,7 +747,12 @@ { value_clause = (fun (_id : int) -> Value _id); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Eff -> fun (() : unit) _k -> @@ -727,7 +799,12 @@ (( + ) _x) >>= fun _b -> _b 4); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Eff -> fun (_x : int) _k -> @@ -807,7 +884,7 @@ let addCase = _addCase let rec _createZeroCase _x = - match _x with + begin match _x with | 0 -> Value (Sub (_addCase, _addCase)) | _n -> coer_return @@ -822,11 +899,12 @@ >>= fun _b -> _b 1 >>= fun _b -> _createZeroCase _b >>= fun _b -> Value (Sub (_b, _b)) + end let createZeroCase = _createZeroCase let rec _createCase _x = - match _x with + begin match _x with | 1 -> _createZeroCase 3 >>= fun _b -> Value (Div (Num 100, _b)) | _ -> coer_return @@ -835,12 +913,14 @@ >>= fun _b -> _b 1 >>= fun _b -> _createCase _b >>= fun _b -> Value (Add (_addCase, _b)) + end let createCase = _createCase - let _bigTest (_num : int) = + let _bigTest = + fun (_num : int) -> let rec _interp _x = - match _x with + begin match _x with | Num _b -> Value _b | Add (_l, _r) -> _interp _l >>= fun _x -> @@ -863,24 +943,30 @@ (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( - ) _x) >>= fun _b -> _b _y - | Div (_l, _r) -> ( + | Div (_l, _r) -> _interp _r >>= fun _y -> _interp _l >>= fun _x -> - match _y with + begin match _y with | 0 -> Call (DivByZero, (), fun (_y : int) -> Value _y) | _ -> coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( / ) _x) - >>= fun _b -> _b _y) + >>= fun _b -> _b _y + end + end in _createCase _num >>= fun _finalCase -> (handler { value_clause = (fun (_id : int) -> Value _id); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | DivByZero -> fun (() : unit) _k -> Value (( ~- ) 1) | eff' -> fun arg k -> Call (eff', arg, k)); @@ -890,9 +976,10 @@ let bigTest = _bigTest - let _bigTestLoop (_num : int) = + let _bigTestLoop = + fun (_num : int) -> let rec _interp _x = - match _x with + begin match _x with | Num _b -> Value _b | Add (_l, _r) -> _interp _l >>= fun _x -> @@ -915,16 +1002,18 @@ (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( - ) _x) >>= fun _b -> _b _y - | Div (_l, _r) -> ( + | Div (_l, _r) -> _interp _r >>= fun _y -> _interp _l >>= fun _x -> - match _y with + begin match _y with | 0 -> Call (DivByZero, (), fun (_y : int) -> Value _y) | _ -> coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( / ) _x) - >>= fun _b -> _b _y) + >>= fun _b -> _b _y + end + end in _createCase _num >>= fun ____finalCase -> let rec _looper _x = @@ -951,8 +1040,12 @@ { value_clause = (fun (_id : int) -> Value _id); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | DivByZero -> fun (() : unit) _k -> Value (( ~- ) 1) | eff' -> fun arg k -> Call (eff', arg, k)); @@ -969,9 +1062,10 @@ type (_, _) eff_internal_effect += Get : (unit, int) eff_internal_effect type (_, _) eff_internal_effect += Set : (int, unit) eff_internal_effect - let _testState (_n : int) = + let _testState = + fun (_n : int) -> let rec _interp _x = - match _x with + begin match _x with | Num _b -> coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) @@ -999,16 +1093,18 @@ (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( - ) _x) >>= fun _b -> _b _y - | Div (_l, _r) -> ( + | Div (_l, _r) -> _interp _r >>= fun _y -> _interp _l >>= fun _x -> - match _y with + begin match _y with | 0 -> Call (Get, (), fun (_y : int) -> Value _y) | _ -> coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( / ) _x) - >>= fun _b -> _b _y) + >>= fun _b -> _b _y + end + end in _createCase _n >>= fun _finalCase -> (handler @@ -1019,8 +1115,12 @@ (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (fun (_ : int) -> _x)); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Get -> fun (() : unit) _k -> @@ -1036,14 +1136,15 @@ let testState = _testState - let _testStateLoop (_n : int) = + let _testStateLoop = + fun (_n : int) -> let _addCase = Add ( Add (Add (Num 20, Num 2), Mul (Num 1, Num 2)), Sub (Add (Num 2, Num 2), Div (Num 1, Num 10)) ) in let rec _createZeroCase _x = - match _x with + begin match _x with | 0 -> Value (Sub (_addCase, _addCase)) | _n -> coer_return @@ -1058,9 +1159,10 @@ >>= fun _b -> _b 1 >>= fun _b -> _createZeroCase _b >>= fun _b -> Value (Sub (_b, _b)) + end in let rec _createCase _x = - match _x with + begin match _x with | 1 -> _createZeroCase 3 >>= fun _b -> Value (Div (Num 100, _b)) | _ -> coer_return @@ -1069,9 +1171,10 @@ >>= fun _b -> _b 1 >>= fun _b -> _createCase _b >>= fun _b -> Value (Add (_addCase, _b)) + end in let rec _interp _x = - match _x with + begin match _x with | Num _b -> coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) @@ -1099,16 +1202,18 @@ (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( - ) _x) >>= fun _b -> _b _y - | Div (_l, _r) -> ( + | Div (_l, _r) -> _interp _r >>= fun _y -> _interp _l >>= fun _x -> - match _y with + begin match _y with | 0 -> Call (Get, (), fun (_y : int) -> Value _y) | _ -> coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( / ) _x) - >>= fun _b -> _b _y) + >>= fun _b -> _b _y + end + end in _createCase _n >>= fun ____finalCase -> let rec _looper _x = @@ -1129,8 +1234,12 @@ (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (fun (_ : int) -> _x)); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Get -> fun (() : unit) _k -> @@ -1189,7 +1298,12 @@ { value_clause = (fun (_x : unit) -> Value _x); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Op2 -> fun (_n : int) _k -> _k () | eff' -> fun arg k -> Call (eff', arg, k)); @@ -1256,7 +1370,7 @@ _b 1 >>= fun _b -> _loop_pure _b let loop_pure = _loop_pure - let _test_pure (_n : int) = _loop_pure _n + let _test_pure = fun (_n : int) -> _loop_pure _n let test_pure = _test_pure type (_, _) eff_internal_effect += Fail : (unit, empty) eff_internal_effect @@ -1280,7 +1394,7 @@ _b 1 >>= fun _b -> _loop_latent _b let loop_latent = _loop_latent - let _test_latent (_n : int) = _loop_latent _n + let _test_latent = fun (_n : int) -> _loop_latent _n let test_latent = _test_latent type (_, _) eff_internal_effect += Incr : (unit, unit) eff_internal_effect @@ -1303,7 +1417,8 @@ let loop_incr = _loop_incr - let _test_incr (_n : int) = + let _test_incr = + fun (_n : int) -> (handler { value_clause = @@ -1312,8 +1427,12 @@ (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (fun (_x : int) -> _x)); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Incr -> fun (() : unit) _k -> @@ -1346,7 +1465,8 @@ let loop_incr' = _loop_incr' - let _test_incr' (_n : int) = + let _test_incr' = + fun (_n : int) -> (handler { value_clause = @@ -1355,8 +1475,12 @@ (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (fun (_x : int) -> _x)); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Incr -> fun (() : unit) _k -> @@ -1406,7 +1530,8 @@ let loop_state = _loop_state - let _test_state (_n : int) = + let _test_state = + fun (_n : int) -> (handler { value_clause = @@ -1415,8 +1540,12 @@ (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (fun (_x : int) -> _x)); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Get -> fun (() : unit) _k -> @@ -1457,7 +1586,7 @@ let rec _map _tycoer _tycoer _tycoer _tycoer _tycoer _x = Value (fun (_x : 'ty21 list) -> - match _x with + begin match _x with | [] -> coer_return (coer_list _tycoer) [] | _x :: _xs -> coer_computation _tycoer (coer_computation _tycoer (_x (_tycoer _x))) @@ -1466,7 +1595,8 @@ _b _xs >>= fun _b -> Value ((fun (x, xs) -> x :: xs) - (coer_tuple (_tycoer, coer_refl_ty) (_b, _b)))) + (coer_tuple (_tycoer, coer_refl_ty) (_b, _b))) + end) let map = _map ====================================================================== @@ -1521,14 +1651,19 @@ type (_, _) eff_internal_effect += Fail : (unit, unit) eff_internal_effect type (_, _) eff_internal_effect += Decide : (unit, bool) eff_internal_effect - let _test_nested (_m : int) = + let _test_nested = + fun (_m : int) -> let rec _simple _x = Call (Get, (), fun (_y : int) -> Value _y) in (handler { value_clause = (fun (_id : int) -> Value _id); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Get -> fun (() : unit) _k -> _k _m | eff' -> fun arg k -> Call (eff', arg, k)); @@ -1538,16 +1673,20 @@ { value_clause = (fun (_x : int) -> Value _x); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> - match eff with eff' -> fun arg k -> Call (eff', arg, k)); + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with eff' -> fun arg k -> Call (eff', arg, k)); } (fun (_x : int) -> Value _x)) (_simple ())) let test_nested = _test_nested - let _test_nested (_m : int) = + let _test_nested = + fun (_m : int) -> let rec _go _x = coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( = ) _x) >>= fun _b -> @@ -1575,8 +1714,12 @@ { value_clause = (fun (_id : unit) -> Value _id); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Decide -> fun (() : unit) _k -> @@ -1584,8 +1727,12 @@ { value_clause = (fun (_id : unit) -> Value _id); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Fail -> fun (() : unit) __k -> _k false | eff' -> fun arg k -> Call (eff', arg, k)); @@ -1621,7 +1768,7 @@ type (_, _) eff_internal_effect += | Write : (string * string, unit) eff_internal_effect - let _f (_x : 'ty4) = () + let _f = fun (_x : 'ty4) -> () let f = _f ====================================================================== codegen/not-found.eff @@ -1652,7 +1799,12 @@ { value_clause = (fun (_x : int) -> Value _x); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Op1 -> fun (_x : int) _k -> _k 11 | eff' -> fun arg k -> Call (eff', arg, k)); @@ -1688,7 +1840,12 @@ { value_clause = (fun (_x : int) -> Value _x); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Decide -> fun (() : unit) _k -> @@ -1725,7 +1882,8 @@ type (_, _) eff_internal_effect += | Write : (string * string, unit) eff_internal_effect - let _k (_b : int) = + let _k = + fun (_b : int) -> let rec _a (_x, _y) = Value (fun (_z : int) -> @@ -1770,7 +1928,9 @@ type (_, _) eff_internal_effect += | Write : (string * string, unit) eff_internal_effect - let _a (_b : bool) (_c : bool) = if _b then Value _c else Value false + let _a = + fun (_b : bool) -> fun (_c : bool) -> if _b then Value _c else Value false + let a = _a ====================================================================== codegen/original.eff @@ -1836,7 +1996,12 @@ { value_clause = (fun (_x : unit) -> Value 0); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | WriteInt -> fun (_n : int) _k -> @@ -1890,22 +2055,23 @@ type (_, _) eff_internal_effect += | Write : (string * string, unit) eff_internal_effect - let _absurd _tycoer (_void : 'ty4) = - match _tycoer _void with _ -> assert false + let _absurd _tycoer = + fun (_void : 'ty4) -> match _tycoer _void with _ -> assert false let absurd = _absurd let rec _op (* @ *) _tycoer _tycoer _x = Value (fun (_ys : 'ty31 list) -> - match _x with + begin match _x with | [] -> coer_return (coer_list _tycoer) _ys | _x :: _xs -> _op (* @ *) _tycoer _tycoer _xs >>= fun _b -> _b _ys >>= fun _b -> Value ((fun (x, xs) -> x :: xs) - (coer_tuple (_tycoer, coer_refl_ty) (_x, _b)))) + (coer_tuple (_tycoer, coer_refl_ty) (_x, _b))) + end) let _op (* @ *) = _op (* @ *) @@ -1913,13 +2079,15 @@ type (_, _) eff_internal_effect += Fail : (unit, empty) eff_internal_effect type (_, _) eff_internal_effect += Decide : (unit, bool) eff_internal_effect - let _fail (() : unit) = + let _fail = + fun (() : unit) -> Call (Fail, (), fun (_y : empty) -> match _y with _ -> assert false) let fail = _fail let _parse _tycoer _tycoer _tycoer _tycoer _tycoer _tycoer _tycoer _tycoer - _tycoer _tycoer _tycoer _tycoer _cmd = + _tycoer _tycoer _tycoer _tycoer = + fun _cmd -> handler { value_clause = @@ -1929,20 +2097,25 @@ (coer_return (coer_arrow coer_refl_ty (coer_computation _tycoer)) (fun (_s : string list) -> - match _s with + begin match _s with | [] -> coer_return _tycoer (_tycoer _x) | _ -> coer_computation _tycoer - (coer_computation _tycoer (_fail ()))))); + (coer_computation _tycoer (_fail ())) + end))); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Symbol -> fun (_c : string) _k -> Value (fun (_s : string list) -> - match _s with + begin match _s with | [] -> coer_computation _tycoer (coer_computation _tycoer (_fail ())) @@ -1955,7 +2128,8 @@ if _b then _k _x >>= fun _b -> _b _xs else coer_computation _tycoer - (coer_computation _tycoer (_fail ()))) + (coer_computation _tycoer (_fail ())) + end) | eff' -> fun arg k -> Call (eff', arg, k)); } (fun (_x : string list -> 'ty73 computation) -> @@ -1966,8 +2140,8 @@ let parse = _parse - let _allsols _tycoer _tycoer _tycoer _tycoer _tycoer _tycoer _tycoer _tycoer - _cmd = + let _allsols _tycoer _tycoer _tycoer _tycoer _tycoer _tycoer _tycoer _tycoer = + fun _cmd -> handler { value_clause = @@ -1977,8 +2151,12 @@ ((fun (x, xs) -> x :: xs) (coer_tuple (_tycoer, coer_list _tycoer) (_tycoer _x, []))))); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Decide -> fun (_ : unit) _k -> @@ -1994,13 +2172,18 @@ let allsols = _allsols - let _backtrack _tycoer _tycoer _tycoer _cmd = + let _backtrack _tycoer _tycoer _tycoer = + fun _cmd -> handler { value_clause = (fun (_id : 'ty152) -> coer_return _tycoer _id); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Decide -> fun (_ : unit) _k -> @@ -2008,8 +2191,12 @@ { value_clause = (fun (_id : 'ty155) -> Value _id); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Fail -> fun (_ : unit) _ -> _k false | eff' -> fun arg k -> Call (eff', arg, k)); @@ -2023,7 +2210,8 @@ let backtrack = _backtrack - let _createNumber ((_prev, _num) : int * int) = + let _createNumber = + fun ((_prev, _num) : int * int) -> coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( * ) _prev) >>= fun _b -> _b 10 >>= fun _b -> @@ -2033,10 +2221,10 @@ let createNumber = _createNumber let rec _parseNum (_l, _v) = - match _l with + begin match _l with | [] -> Value _v - | _x :: _xs -> ( - match _x with + | _x :: _xs -> + begin match _x with | "0" -> _createNumber (_v, 0) >>= fun _b -> _parseNum (_xs, _b) | "1" -> _createNumber (_v, 1) >>= fun _b -> _parseNum (_xs, _b) | "2" -> _createNumber (_v, 2) >>= fun _b -> _parseNum (_xs, _b) @@ -2047,15 +2235,18 @@ | "7" -> _createNumber (_v, 7) >>= fun _b -> _parseNum (_xs, _b) | "8" -> _createNumber (_v, 8) >>= fun _b -> _parseNum (_xs, _b) | "9" -> _createNumber (_v, 9) >>= fun _b -> _parseNum (_xs, _b) - | _ -> _fail ()) + | _ -> _fail () + end + end let parseNum = _parseNum let rec _toNum _x = _parseNum (_x, 0) let toNum = _toNum - let _digit (() : unit) = + let _digit = + fun (() : unit) -> let rec _checkNums _x = - match _x with + begin match _x with | [] -> _fail () | _x :: _xs -> Call @@ -2064,6 +2255,7 @@ fun (_y : bool) -> if _y then Call (Symbol, _x, fun (_y : string) -> Value _y) else _checkNums _xs ) + end in _checkNums [ "0"; "1"; "2"; "3"; "4"; "5"; "6"; "7"; "8"; "9" ] @@ -2143,7 +2335,8 @@ let expr = _expr - let _parseTest (() : unit) = + let _parseTest = + fun (() : unit) -> _allsols coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty ( _parse coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty @@ -2187,7 +2380,7 @@ type intlist = IntNil | IntCons of (int * intlist);; (let rec _concat _x = - match _x with + begin match _x with | IntNil -> coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) @@ -2197,12 +2390,18 @@ (fun (_ys : intlist) -> _concat _zs >>= fun _b -> _b _ys >>= fun _b -> Value (IntCons (_z, _b))) + end in handler { value_clause = (fun (_x : int) -> Value (IntCons (_x, IntNil))); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Decide -> fun (() : unit) _k -> @@ -2249,7 +2448,7 @@ type intlist = IntNil | IntCons of (int * intlist);; let rec _concat _x = - match _x with + begin match _x with | IntNil -> coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) @@ -2259,12 +2458,18 @@ (fun (_ys : intlist) -> _concat _zs >>= fun _b -> _b _ys >>= fun _b -> Value (IntCons (_z, _b))) + end in (handler { value_clause = (fun (_x : int) -> Value (IntCons (_x, IntNil))); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Decide -> fun (() : unit) _k -> @@ -2305,7 +2510,7 @@ type intlist = IntNil | IntCons of (int * intlist);; let rec _concat _x = - match _x with + begin match _x with | IntNil -> coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) @@ -2315,12 +2520,18 @@ (fun (_ys : intlist) -> _concat _zs >>= fun _b -> _b _ys >>= fun _b -> Value (IntCons (_z, _b))) + end in (handler { value_clause = (fun (_x : int) -> Value (IntCons (_x, IntNil))); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Decide -> fun (() : unit) _k -> @@ -2367,14 +2578,18 @@ type (_, _) eff_internal_effect += | Write : (string * string, unit) eff_internal_effect - let _f (_ : 'ty4) = + let _f = + fun (_ : 'ty4) -> (handler { value_clause = (fun (_x : int) -> Value 5); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> - match eff with eff' -> fun arg k -> Call (eff', arg, k)); + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with eff' -> fun arg k -> Call (eff', arg, k)); } (fun (_x : int) -> Value _x)) ( coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( + ) 1) @@ -2413,97 +2628,110 @@ type optional_solution = None | Some of solution type void = Void - let _absurd _tycoer (_void : 'ty4) = - match _tycoer _void with _ -> assert false + let _absurd _tycoer = + fun (_void : 'ty4) -> match _tycoer _void with _ -> assert false let absurd = _absurd let rec _op (* @ *) _x = Value (fun (_ys : solutions) -> - match _x with + begin match _x with | SolutionsNil -> Value _ys | SolutionsCons (_x, _xs) -> _op (* @ *) _xs >>= fun _b -> - _b _ys >>= fun _b -> Value (SolutionsCons (_x, _b))) + _b _ys >>= fun _b -> Value (SolutionsCons (_x, _b)) + end) let _op (* @ *) = _op (* @ *) - let _no_attack ((_x, _y) : int * int) ((_x', _y') : int * int) = - coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( <> ) _x) - >>= fun _b -> - _b _x' >>= fun _b -> - if _b then - coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( <> ) _y) - >>= fun _b -> - _b _y' >>= fun _b -> - if _b then - coer_return - (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) - (( - ) _x) - >>= fun _b -> - _b _x' >>= fun _b -> - coer_return - (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) - (( <> ) (abs _b)) - >>= fun _b -> - coer_return - (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) - (( - ) _y) - >>= fun _b -> - _b _y' >>= fun _b -> _b (abs _b) - else Value false - else Value false + let _no_attack = + fun ((_x, _y) : int * int) -> + fun ((_x', _y') : int * int) -> + coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( <> ) _x) + >>= fun _b -> + _b _x' >>= fun _b -> + if _b then + coer_return + (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) + (( <> ) _y) + >>= fun _b -> + _b _y' >>= fun _b -> + if _b then + coer_return + (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) + (( - ) _x) + >>= fun _b -> + _b _x' >>= fun _b -> + coer_return + (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) + (( <> ) (abs _b)) + >>= fun _b -> + coer_return + (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) + (( - ) _y) + >>= fun _b -> + _b _y' >>= fun _b -> _b (abs _b) + else Value false + else Value false let no_attack = _no_attack let rec _not_attacked _x = Value (fun (_qs : solution) -> - match _qs with + begin match _qs with | SolutionEmpty -> Value true | SolutionPlace (_x, _xs) -> _no_attack _x _x >>= fun _b -> - if _b then _not_attacked _x >>= fun _b -> _b _xs else Value false) + if _b then _not_attacked _x >>= fun _b -> _b _xs else Value false + end) let not_attacked = _not_attacked - let _available (_number_of_queens : int) (_x : int) (_qs : solution) = - let rec _loop (_possible, _y) = - coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( < ) _y) - >>= fun _b -> - _b 1 >>= fun _b -> - if _b then Value _possible - else - _not_attacked (_x, _y) >>= fun _b -> - _b _qs >>= fun _b -> - if _b then - coer_return - (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) - (( - ) _y) - >>= fun _b -> - _b 1 >>= fun _b -> _loop (RowsCons (_y, _possible), _b) + let _available = + fun (_number_of_queens : int) -> + fun (_x : int) -> + fun (_qs : solution) -> + let rec _loop (_possible, _y) = + coer_return + (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) + (( < ) _y) + >>= fun _b -> + _b 1 >>= fun _b -> + if _b then Value _possible else - coer_return - (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) - (( - ) _y) - >>= fun _b -> - _b 1 >>= fun _b -> _loop (_possible, _b) - in - _loop (RowsEmpty, _number_of_queens) + _not_attacked (_x, _y) >>= fun _b -> + _b _qs >>= fun _b -> + if _b then + coer_return + (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) + (( - ) _y) + >>= fun _b -> + _b 1 >>= fun _b -> _loop (RowsCons (_y, _possible), _b) + else + coer_return + (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) + (( - ) _y) + >>= fun _b -> + _b 1 >>= fun _b -> _loop (_possible, _b) + in + _loop (RowsEmpty, _number_of_queens) let available = _available let rec _choose _x = - match _x with + begin match _x with | RowsEmpty -> Call (Fail, (), fun (_y : empty) -> match _y with _ -> assert false) | RowsCons (_x, _xs') -> Call (Decide, (), fun (_y : bool) -> if _y then Value _x else _choose _xs') + end let choose = _choose - let _queens (_number_of_queens : int) = + let _queens = + fun (_number_of_queens : int) -> let rec _place (_x, _qs) = coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( > ) _x) >>= fun _b -> @@ -2527,18 +2755,26 @@ let queens = _queens - let _queens_one_option (_number_of_queens : int) = + let _queens_one_option = + fun (_number_of_queens : int) -> (handler { value_clause = (fun (_x : solution) -> Value (Some _x)); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with - | Decide -> ( + | Decide -> fun (_ : unit) _k -> _k true >>= fun _b -> - match _b with Some _x -> Value (Some _x) | None -> _k false) + begin match _b with + | Some _x -> Value (Some _x) + | None -> _k false + end | Fail -> fun (_ : unit) __k -> Value None | eff' -> fun arg k -> Call (eff', arg, k)); } @@ -2547,14 +2783,19 @@ let queens_one_option = _queens_one_option - let _queens_all (_number_of_queens : int) = + let _queens_all = + fun (_number_of_queens : int) -> (handler { value_clause = (fun (_x : solution) -> Value (SolutionsCons (_x, SolutionsNil))); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Decide -> fun (_ : unit) _k -> @@ -2569,7 +2810,8 @@ let queens_all = _queens_all - let _queens_one_cps (_number_of_queens : int) = + let _queens_one_cps = + fun (_number_of_queens : int) -> (handler { value_clause = @@ -2578,8 +2820,12 @@ (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (fun (_ : unit -> solution computation) -> _x)); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Decide -> fun (_ : unit) _k -> @@ -2626,9 +2872,10 @@ type (_, _) eff_internal_effect += Fetch : (unit, int) eff_internal_effect type int_list = Nil | Cons of (int * int_list) - let _test (_n : int) = + let _test = + fun (_n : int) -> let rec _range _x = - match _x with + begin match _x with | 0 -> Value Nil | _ -> Call @@ -2641,13 +2888,18 @@ >>= fun _b -> _b 1 >>= fun _b -> _range _b >>= fun _b -> Value (Cons (_y, _b)) ) + end in (handler { value_clause = (fun (_x : int_list) -> Value _x); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Fetch -> fun (_ : unit) _k -> _k 42 | eff' -> fun arg k -> Call (eff', arg, k)); @@ -2666,7 +2918,8 @@ type (_, _) eff_internal_effect += | GeneratorProduce : (int, int) eff_internal_effect - let _testGenerator (_m : int) = + let _testGenerator = + fun (_m : int) -> let rec _sum _x = coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( = ) _x) >>= fun _b -> @@ -2704,8 +2957,12 @@ (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (fun (_ : int) -> _x)); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | GeneratorGet -> fun (() : unit) _k -> @@ -2720,8 +2977,12 @@ { value_clause = (fun (_id : int) -> Value _id); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | GeneratorProduce -> fun (_i : int) _k -> @@ -2813,13 +3074,18 @@ type (_, _) eff_internal_effect += Ping : (unit, unit) eff_internal_effect - let _test_simple (_x : 'ty4) = + let _test_simple = + fun (_x : 'ty4) -> (handler { value_clause = (fun (_id : unit * int) -> Value _id); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Ping -> fun (() : unit) _k -> _k () | eff' -> fun arg k -> Call (eff', arg, k)); @@ -2829,13 +3095,18 @@ let test_simple = _test_simple - let _test_simple2 (() : unit) = + let _test_simple2 = + fun (() : unit) -> (handler { value_clause = (fun (_id : unit) -> Value _id); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Ping -> fun (() : unit) _k -> _k () | eff' -> fun arg k -> Call (eff', arg, k)); @@ -2867,16 +3138,20 @@ type (_, _) eff_internal_effect += | Write : (string * string, unit) eff_internal_effect - let _h _tycoer _tycoer _tycoer _tycoer _tycoer _cmd = + let _h _tycoer _tycoer _tycoer _tycoer _tycoer = + fun _cmd -> handler { value_clause = (fun (_x : 'ty6) -> coer_computation _tycoer (coer_return _tycoer (_tycoer _x))); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> - match eff with eff' -> fun arg k -> Call (eff', arg, k)); + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with eff' -> fun arg k -> Call (eff', arg, k)); } (fun (_x : 'ty4) -> coer_return _tycoer (_tycoer _x)) _cmd @@ -2915,7 +3190,7 @@ type (_, _) eff_internal_effect += | Write : (string * string, unit) eff_internal_effect - let _decide_func (_bl : bool) = if _bl then Value 10 else Value 20 + let _decide_func = fun (_bl : bool) -> if _bl then Value 10 else Value 20 let decide_func = _decide_func ====================================================================== codegen/test-handle_effect_skip.eff @@ -2945,8 +3220,12 @@ { value_clause = (fun (_x : unit) -> Value 42); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : (a -> (b -> _) -> _) -> - match eff with eff' -> fun arg k -> Call (eff', arg, k)); + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with eff' -> fun arg k -> Call (eff', arg, k)); } (fun (_x : int) -> Value _x)) (Call (Print, "hello\n", fun (_y : unit) -> Value _y)) @@ -3053,7 +3332,12 @@ { value_clause = (fun (_x : int) -> Value _x); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Op1 -> fun (_n : int) _k -> Value 1 | Op2 -> fun (_n : int) _k -> Value 2 @@ -3090,7 +3374,12 @@ { value_clause = (fun (_x : int) -> Value _x); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Op1 -> fun (_n : int) _k -> Value 1 | Op2 -> fun (_n : int) _k -> Value 2 @@ -3241,8 +3530,12 @@ (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (fun (_ : int) -> _x)); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Get -> fun (_ : unit) _k -> @@ -3309,11 +3602,12 @@ let rec _add _x = Value (fun (_x : nat) -> - match _x with + begin match _x with | Zero -> Value _x | Succ _n -> _add _x >>= fun _b -> - _b _n >>= fun _b -> Value (Succ _b)) + _b _n >>= fun _b -> Value (Succ _b) + end) in _add ====================================================================== @@ -3343,12 +3637,14 @@ Value (coer_arrow coer_refl_ty (coer_return coer_refl_ty) - (fun ((_w, _k, _num) : nat * nat * int) (_x : nat * nat * int) -> - match _x with - | Zero, Zero, 0 -> Value (_w, _k, Zero, 0, 0) - | Zero, _z, _n -> Value (Zero, _z, Zero, _num, _n) - | _x, Zero, _n -> Value (Zero, _w, _x, 1, _n) - | _, _, _ -> Value (Zero, Zero, Zero, 0, 0))) + (fun ((_w, _k, _num) : nat * nat * int) -> + fun (_x : nat * nat * int) -> + begin match _x with + | Zero, Zero, 0 -> Value (_w, _k, Zero, 0, 0) + | Zero, _z, _n -> Value (Zero, _z, Zero, _num, _n) + | _x, Zero, _n -> Value (Zero, _w, _x, 1, _n) + | _, _, _ -> Value (Zero, Zero, Zero, 0, 0) + end)) ====================================================================== codegen/test2.eff ---------------------------------------------------------------------- @@ -3473,9 +3769,12 @@ (fun (_x : 'ty5) -> coer_computation _tycoer (coer_return _tycoer (_tycoer _x))); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> - match eff with eff' -> fun arg k -> Call (eff', arg, k)); + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with eff' -> fun arg k -> Call (eff', arg, k)); } (fun (_x : 'ty3) -> coer_return _tycoer (_tycoer _x)) ====================================================================== @@ -3506,8 +3805,12 @@ { value_clause = (fun (_x : int) -> Value _x); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : (a -> (b -> _) -> _) -> - match eff with eff' -> fun arg k -> Call (eff', arg, k)); + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with eff' -> fun arg k -> Call (eff', arg, k)); } (fun (_x : int) -> Value _x)) (Value 1) @@ -3540,7 +3843,12 @@ { value_clause = (fun (_id : int) -> Value _id); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Op -> fun (_n : int) _k -> Value 2 | eff' -> fun arg k -> Call (eff', arg, k)); @@ -3575,7 +3883,12 @@ { value_clause = (fun (_x : int) -> Value _x); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Op -> fun (_n : int) _k -> Value 2 | eff' -> fun arg k -> Call (eff', arg, k)); @@ -3611,7 +3924,12 @@ { value_clause = (fun (_x : int) -> Value _x); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Op -> fun (_n : int) _k -> Value 2 | eff' -> fun arg k -> Call (eff', arg, k)); @@ -3647,7 +3965,12 @@ { value_clause = (fun (_x : int) -> Value _x); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Op -> fun (_n : int) _k -> _k 2 | eff' -> fun arg k -> Call (eff', arg, k)); @@ -3683,7 +4006,12 @@ { value_clause = (fun (_x : int) -> Value _x); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Op -> fun (_n : int) _k -> _k _n | eff' -> fun arg k -> Call (eff', arg, k)); @@ -3717,7 +4045,7 @@ type intlist = IntNil | IntCons of (int * intlist) let rec _concat _x = - match _x with + begin match _x with | IntNil -> coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) @@ -3727,6 +4055,7 @@ (fun (_ys : intlist) -> _concat _zs >>= fun _b -> _b _ys >>= fun _b -> Value (IntCons (_z, _b))) + end let concat = _concat;; @@ -3734,8 +4063,12 @@ { value_clause = (fun (_x : int) -> Value IntNil); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : (a -> (b -> _) -> _) -> - match eff with eff' -> fun arg k -> Call (eff', arg, k)); + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with eff' -> fun arg k -> Call (eff', arg, k)); } (fun (_x : intlist) -> Value _x)) (Value 1) @@ -3765,23 +4098,25 @@ type tree = Empty | Node of (tree * int * tree) type (_, _) eff_internal_effect += Choose : (unit, bool) eff_internal_effect - let _tester (_k : int) = - let _leaf (_a : int) = + let _tester = + fun (_k : int) -> + let _leaf = + fun (_a : int) -> coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( * ) _a) >>= fun _b -> _b _k >>= fun _b -> Value (Node (Empty, _b, Empty)) in let _bot = - coer_arrow coer_refl_ty (coer_return coer_refl_ty) - (fun (_t : tree) (_t2 : tree) -> - _leaf 13 >>= fun _b -> - _leaf 9 >>= fun _b -> - _leaf 3 >>= fun _b -> - Value - (Node - ( Node (Node (_t, 0, _t2), 2, _b), - 5, - Node (_b, 7, Node (_t2, 3, Node (_b, 5, _t2))) ))) + coer_arrow coer_refl_ty (coer_return coer_refl_ty) (fun (_t : tree) -> + fun (_t2 : tree) -> + _leaf 13 >>= fun _b -> + _leaf 9 >>= fun _b -> + _leaf 3 >>= fun _b -> + Value + (Node + ( Node (Node (_t, 0, _t2), 2, _b), + 5, + Node (_b, 7, Node (_t2, 3, Node (_b, 5, _t2))) ))) in _leaf 3 >>= fun _b -> _bot _b >>= fun _b -> @@ -3806,22 +4141,24 @@ let tester = _tester - let _max _tycoer _tycoer _tycoer _tycoer _tycoer _tycoer (_a : 'ty97) - (_b : 'ty98) = - coer_computation - (coer_arrow _tycoer coer_refl_ty) - (coer_return - (coer_arrow _tycoer (coer_return coer_refl_ty)) - (( > ) (_tycoer _a))) - >>= fun _b -> - _b (_tycoer _b) >>= fun _b -> - if _b then coer_return _tycoer _a else coer_return _tycoer _b + let _max _tycoer _tycoer _tycoer _tycoer _tycoer _tycoer = + fun (_a : 'ty97) -> + fun (_b : 'ty98) -> + coer_computation + (coer_arrow _tycoer coer_refl_ty) + (coer_return + (coer_arrow _tycoer (coer_return coer_refl_ty)) + (( > ) (_tycoer _a))) + >>= fun _b -> + _b (_tycoer _b) >>= fun _b -> + if _b then coer_return _tycoer _a else coer_return _tycoer _b let max = _max - let _effect_max (_m : int) = + let _effect_max = + fun (_m : int) -> let rec _find_max _x = - match _x with + begin match _x with | Empty -> Value 0 | Node (Empty, _x, Empty) -> Value _x | Node (_left, _x, _right) -> @@ -3835,14 +4172,19 @@ (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( + ) _x) >>= fun _b -> _b _next ) + end in _tester _m >>= fun _t -> (handler { value_clause = (fun (_x : int) -> Value _x); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Choose -> fun (() : unit) _k -> @@ -3856,28 +4198,31 @@ (_find_max _t) let effect_max = _effect_max - let _test_max (_m : int) = _effect_max _m + let _test_max = fun (_m : int) -> _effect_max _m let test_max = _test_max - let _op (_x : int) (_y : int) = - coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( - ) _x) - >>= fun _b -> - coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( * ) 3) - >>= fun _b -> - _b _y >>= fun _b -> _b _b + let _op = + fun (_x : int) -> + fun (_y : int) -> + coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( - ) _x) + >>= fun _b -> + coer_return (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (( * ) 3) + >>= fun _b -> + _b _y >>= fun _b -> _b _b let op = _op - let _max _tycoer _tycoer _tycoer _tycoer _tycoer _tycoer (_a : 'ty189) - (_b : 'ty190) = - coer_computation - (coer_arrow _tycoer coer_refl_ty) - (coer_return - (coer_arrow _tycoer (coer_return coer_refl_ty)) - (( > ) (_tycoer _a))) - >>= fun _b -> - _b (_tycoer _b) >>= fun _b -> - if _b then coer_return _tycoer _a else coer_return _tycoer _b + let _max _tycoer _tycoer _tycoer _tycoer _tycoer _tycoer = + fun (_a : 'ty189) -> + fun (_b : 'ty190) -> + coer_computation + (coer_arrow _tycoer coer_refl_ty) + (coer_return + (coer_arrow _tycoer (coer_return coer_refl_ty)) + (( > ) (_tycoer _a))) + >>= fun _b -> + _b (_tycoer _b) >>= fun _b -> + if _b then coer_return _tycoer _a else coer_return _tycoer _b let max = _max @@ -3886,29 +4231,32 @@ let rec _op (* @ *) _x = Value (fun (_ys : intlist) -> - match _x with + begin match _x with | Nil -> Value _ys | Cons (_x, _xs) -> _op (* @ *) _xs >>= fun _b -> - _b _ys >>= fun _b -> Value (Cons (_x, _b))) + _b _ys >>= fun _b -> Value (Cons (_x, _b)) + end) let _op (* @ *) = _op (* @ *) - let _test_general (_m : int) = + let _test_general = + fun (_m : int) -> let rec _maxl _x = Value (fun (_x : intlist) -> - match _x with + begin match _x with | Nil -> Value _x | Cons (_x, _xs) -> _max coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty _x _x >>= fun _b -> - _maxl _b >>= fun _b -> _b _xs) + _maxl _b >>= fun _b -> _b _xs + end) in _tester _m >>= fun _t -> let rec _explore _x = - match _x with + begin match _x with | Empty -> Value 0 | Node (_left, _x, _right) -> Call @@ -3918,14 +4266,19 @@ (if _y then _explore _left >>= fun _b -> _op _x _b else _explore _right >>= fun _b -> _op _x _b) >>= fun _next -> Value _next ) + end in _maxl 0 >>= fun _b -> (handler { value_clause = (fun (_x : int) -> Value (Cons (_x, Nil))); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Choose -> fun (() : unit) _k -> @@ -3940,21 +4293,23 @@ let test_general = _test_general - let _test_general_loop (_m : int) = + let _test_general_loop = + fun (_m : int) -> let rec _maxl _x = Value (fun (_x : intlist) -> - match _x with + begin match _x with | Nil -> Value _x | Cons (_x, _xs) -> _max coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty _x _x >>= fun _b -> - _maxl _b >>= fun _b -> _b _xs) + _maxl _b >>= fun _b -> _b _xs + end) in _tester _m >>= fun ____t -> let rec _explore _x = - match _x with + begin match _x with | Empty -> Value 0 | Node (_left, _x, _right) -> Call @@ -3964,6 +4319,7 @@ (if _y then _explore _left >>= fun _b -> _op _x _b else _explore _right >>= fun _b -> _op _x _b) >>= fun _next -> Value _next ) + end in let rec _looper _x = Value @@ -3990,8 +4346,12 @@ { value_clause = (fun (_x : int) -> Value (Cons (_x, Nil))); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Choose -> fun (() : unit) _k -> @@ -4012,22 +4372,24 @@ type (_, _) eff_internal_effect += Get : (unit, int) eff_internal_effect - let _absurd _tycoer (_void : 'ty465) = - match _tycoer _void with _ -> assert false + let _absurd _tycoer = + fun (_void : 'ty465) -> match _tycoer _void with _ -> assert false let absurd = _absurd - let _test_leaf_state (_m : int) = + let _test_leaf_state = + fun (_m : int) -> let rec _maxl _x = Value (fun (_x : intlist) -> - match _x with + begin match _x with | Nil -> Value _x | Cons (_x, _xs) -> _max coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty _x _x >>= fun _b -> - _maxl _b >>= fun _b -> _b _xs) + _maxl _b >>= fun _b -> _b _xs + end) in let rec _populate_leafs _x = Value @@ -4056,7 +4418,7 @@ _b 154 >>= fun _leafs -> _tester _m >>= fun _t -> let rec _explore _x = - match _x with + begin match _x with | Empty -> Call (Get, (), fun (_y : int) -> Value _y) | Node (_left, _x, _right) -> Call @@ -4065,6 +4427,7 @@ fun (_y : bool) -> (if _y then Value _left else Value _right) >>= fun _next -> _explore _next >>= fun _b -> _op _x _b ) + end in _maxl 0 >>= fun _b -> (handler @@ -4075,16 +4438,21 @@ (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (fun (_ : intlist) -> _x)); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Get -> fun (() : unit) _k -> Value (fun (_s : intlist) -> - match _s with + begin match _s with | Cons (_x, _rest) -> _k _x >>= fun _b -> _b _rest - | Nil -> Value Nil) + | Nil -> Value Nil + end) | eff' -> fun arg k -> Call (eff', arg, k)); } (fun (_x : intlist -> intlist computation) -> Value _x)) @@ -4092,8 +4460,12 @@ { value_clause = (fun (_x : int) -> Value (Cons (_x, Nil))); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Choose -> fun (() : unit) _k -> @@ -4109,17 +4481,19 @@ let test_leaf_state = _test_leaf_state - let _test_leaf_state_loop (_m : int) = + let _test_leaf_state_loop = + fun (_m : int) -> let rec _maxl _x = Value (fun (_x : intlist) -> - match _x with + begin match _x with | Nil -> Value _x | Cons (_x, _xs) -> _max coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty _x _x >>= fun _b -> - _maxl _b >>= fun _b -> _b _xs) + _maxl _b >>= fun _b -> _b _xs + end) in let rec _populate_leafs _x = Value @@ -4148,7 +4522,7 @@ _b 154 >>= fun ____leafs -> _tester _m >>= fun ____t -> let rec _explore _x = - match _x with + begin match _x with | Empty -> Call (Get, (), fun (_y : int) -> Value _y) | Node (_left, _x, _right) -> Call @@ -4157,6 +4531,7 @@ fun (_y : bool) -> (if _y then Value _left else Value _right) >>= fun _next -> _explore _next >>= fun _b -> _op _x _b ) + end in let rec _looper _x = Value @@ -4187,16 +4562,21 @@ (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (fun (_ : intlist) -> _x)); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Get -> fun (() : unit) _k -> Value (fun (_s : intlist) -> - match _s with + begin match _s with | Cons (_x, _rest) -> _k _x >>= fun _b -> _b _rest - | Nil -> Value Nil) + | Nil -> Value Nil + end) | eff' -> fun arg k -> Call (eff', arg, k)); } (fun (_x : intlist -> intlist computation) -> Value _x)) @@ -4204,8 +4584,12 @@ { value_clause = (fun (_x : int) -> Value (Cons (_x, Nil))); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Choose -> fun (() : unit) _k -> @@ -4227,21 +4611,23 @@ type (_, _) eff_internal_effect += Set : (int, unit) eff_internal_effect - let _test_leaf_state_update (_m : int) = + let _test_leaf_state_update = + fun (_m : int) -> let rec _maxl _x = Value (fun (_x : intlist) -> - match _x with + begin match _x with | Nil -> Value _x | Cons (_x, _xs) -> _max coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty _x _x >>= fun _b -> - _maxl _b >>= fun _b -> _b _xs) + _maxl _b >>= fun _b -> _b _xs + end) in _tester _m >>= fun _t -> let rec _explore _x = - match _x with + begin match _x with | Empty -> Call (Get, (), fun (_y : int) -> Value _y) | Node (_left, _x, _right) -> coer_return @@ -4259,6 +4645,7 @@ fun (_y : bool) -> (if _y then Value _left else Value _right) >>= fun _next -> _explore _next >>= fun _b -> _op _x _b ) ) + end in _maxl 0 >>= fun _b -> (handler @@ -4269,8 +4656,12 @@ (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (fun (_ : int) -> _x)); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Get -> fun (() : unit) _k -> @@ -4285,8 +4676,12 @@ { value_clause = (fun (_x : int) -> Value (Cons (_x, Nil))); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Choose -> fun (() : unit) _k -> @@ -4302,21 +4697,23 @@ let test_leaf_state_update = _test_leaf_state_update - let _test_leaf_state_update_loop (_m : int) = + let _test_leaf_state_update_loop = + fun (_m : int) -> let rec _maxl _x = Value (fun (_x : intlist) -> - match _x with + begin match _x with | Nil -> Value _x | Cons (_x, _xs) -> _max coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty _x _x >>= fun _b -> - _maxl _b >>= fun _b -> _b _xs) + _maxl _b >>= fun _b -> _b _xs + end) in _tester _m >>= fun ____t -> let rec _explore _x = - match _x with + begin match _x with | Empty -> Call (Get, (), fun (_y : int) -> Value _y) | Node (_left, _x, _right) -> coer_return @@ -4334,6 +4731,7 @@ fun (_y : bool) -> (if _y then Value _left else Value _right) >>= fun _next -> _explore _next >>= fun _b -> _op _x _b ) ) + end in let rec _looper _x = Value @@ -4364,8 +4762,12 @@ (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (fun (_ : int) -> _x)); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Get -> fun (() : unit) _k -> @@ -4380,8 +4782,12 @@ { value_clause = (fun (_x : int) -> Value (Cons (_x, Nil))); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Choose -> fun (() : unit) _k -> @@ -4401,21 +4807,23 @@ let test_leaf_state_update_loop = _test_leaf_state_update_loop - let _test_leaf_state_update_merged_handler (_m : int) = + let _test_leaf_state_update_merged_handler = + fun (_m : int) -> let rec _maxl _x = Value (fun (_x : intlist) -> - match _x with + begin match _x with | Nil -> Value _x | Cons (_x, _xs) -> _max coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty _x _x >>= fun _b -> - _maxl _b >>= fun _b -> _b _xs) + _maxl _b >>= fun _b -> _b _xs + end) in _tester _m >>= fun _t -> let rec _explore _x = - match _x with + begin match _x with | Empty -> Call (Get, (), fun (_y : int) -> Value _y) | Node (_left, _x, _right) -> coer_return @@ -4433,6 +4841,7 @@ fun (_y : bool) -> (if _y then Value _left else Value _right) >>= fun _next -> _explore _next >>= fun _b -> _op _x _b ) ) + end in _maxl 0 >>= fun _b -> (handler @@ -4443,8 +4852,12 @@ (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (fun (_ : int) -> Cons (_x, Nil))); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Get -> fun (() : unit) _k -> @@ -4471,21 +4884,23 @@ let test_leaf_state_update_merged_handler = _test_leaf_state_update_merged_handler - let _test_leaf_state_update_merged_handler_loop (_m : int) = + let _test_leaf_state_update_merged_handler_loop = + fun (_m : int) -> let rec _maxl _x = Value (fun (_x : intlist) -> - match _x with + begin match _x with | Nil -> Value _x | Cons (_x, _xs) -> _max coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty coer_refl_ty _x _x >>= fun _b -> - _maxl _b >>= fun _b -> _b _xs) + _maxl _b >>= fun _b -> _b _xs + end) in _tester _m >>= fun ____t -> let rec _explore _x = - match _x with + begin match _x with | Empty -> Call (Get, (), fun (_y : int) -> Value _y) | Node (_left, _x, _right) -> coer_return @@ -4503,6 +4918,7 @@ fun (_y : bool) -> (if _y then Value _left else Value _right) >>= fun _next -> _explore _next >>= fun _b -> _op _x _b ) ) + end in let rec _looper _x = Value @@ -4533,8 +4949,12 @@ (coer_arrow coer_refl_ty (coer_return coer_refl_ty)) (fun (_ : int) -> Cons (_x, Nil))); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : - (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Get -> fun (() : unit) _k -> @@ -4593,17 +5013,23 @@ let rec _op (* @ *) _x = Value (fun (_ys : int_list) -> - match _x with + begin match _x with | Nil -> Value _ys | Cons (_x, _xs) -> _op (* @ *) _xs >>= fun _b -> - _b _ys >>= fun _b -> Value (Cons (_x, _b))) + _b _ys >>= fun _b -> Value (Cons (_x, _b)) + end) in (handler { value_clause = (fun (_x : int) -> Value (Cons (_x, Nil))); effect_clauses = - (fun (type a b) (eff : (a, b) eff_internal_effect) : (a -> (b -> _) -> _) -> + (fun (type a) + (type b) + (eff : (a, b) eff_internal_effect) + : + (a -> (b -> _) -> _) + -> match eff with | Decide -> fun (() : unit) _k ->