From 6c0fab134e4d6e1d86c72b57cbbee96e7b163a16 Mon Sep 17 00:00:00 2001 From: Jack Feser Date: Fri, 1 Feb 2019 15:29:25 +0900 Subject: [PATCH] Reformat mli files. --- lib/combinat.mli | 8 +- lib/eval.mli | 8 +- lib/example.mli | 10 +- lib/example_deduction.mli | 3 +- lib/exprValue.mli | 8 ++ lib/hypothesis.mli | 224 +++++++++++++++++++++++--------------- lib/infer.mli | 64 ++++++++--- lib/library.mli | 18 +-- lib/status.mli | 7 +- lib/synthesis_common.mli | 55 +++++----- lib/v1_engine.mli | 23 ++-- lib/v1_solver_engine.mli | 11 +- 12 files changed, 272 insertions(+), 167 deletions(-) diff --git a/lib/combinat.mli b/lib/combinat.mli index 0421f3f..b76dc84 100644 --- a/lib/combinat.mli +++ b/lib/combinat.mli @@ -2,17 +2,17 @@ open Core (** Implementations of combinatorics routines. *) +val m_partition : int -> int -> Array.Int.t Sequence.t (** Compute the partitions of an integer {i n} into {i m} parts. See (Knuth 3b, pg. 2). *) -val m_partition : int -> int -> Array.Int.t Sequence.t +val m_partition_with_zeros : int -> int -> Array.Int.t Sequence.t (** Compute the partitions of an integer {i n} into {i m} parts, including partitions where some elements are zero. *) -val m_partition_with_zeros : int -> int -> Array.Int.t Sequence.t -(** Compute the unique permutations of an array. See (Knuth 2b, pg. 1). *) val permutations : Array.Int.t -> Array.Int.t Sequence.t +(** Compute the unique permutations of an array. See (Knuth 2b, pg. 1). *) val permutations_poly : 'a Array.t -> 'a Array.t Sequence.t - + val combinations_with_replacement : int -> 'a list -> 'a list list diff --git a/lib/eval.mli b/lib/eval.mli index c751433..4896223 100644 --- a/lib/eval.mli +++ b/lib/eval.mli @@ -2,12 +2,10 @@ open Core open Collections exception RuntimeError of Error.t + exception HitRecursionLimit val eval : ?recursion_limit:int -> Value.t Ctx.t -> Expr.t -> Value.t - + val partial_eval : - ?recursion_limit:int - -> ?ctx:ExprValue.t Ctx.t - -> ExprValue.t - -> ExprValue.t + ?recursion_limit:int -> ?ctx:ExprValue.t Ctx.t -> ExprValue.t -> ExprValue.t diff --git a/lib/example.mli b/lib/example.mli index 75e5344..a1e9518 100644 --- a/lib/example.mli +++ b/lib/example.mli @@ -1,5 +1,4 @@ open Core - open Collections type t = Expr.t * Expr.t @@ -7,12 +6,21 @@ type t = Expr.t * Expr.t include Sexpable.S with type t := t val compare : t -> t -> int + val of_string_exn : string -> t + val of_string : string -> t Or_error.t + val to_string : t -> string + val to_triple : t -> Ast.id * Ast.expr list * Expr.t + val name : t list -> Ast.id + val split : t list -> (string * t list) list + val signature : ?ctx:Infer.Type.t Ctx.t -> t list -> Infer.Type.t + val to_vctx : t -> string list -> Expr.t Ctx.t + val check : (t * Expr.t Ctx.t) list -> bool diff --git a/lib/example_deduction.mli b/lib/example_deduction.mli index 99b5044..996168d 100644 --- a/lib/example_deduction.mli +++ b/lib/example_deduction.mli @@ -1,12 +1,13 @@ open Core - open Synthesis_common open Collections type example = ExprValue.t list * ExprValue.t [@@deriving sexp] val examples_of_file : string -> example list + val examples_of_channel : In_channel.t -> example list val timer : Timer.t + val push_specs : Deduction.t diff --git a/lib/exprValue.mli b/lib/exprValue.mli index 6c1a071..03ce146 100644 --- a/lib/exprValue.mli +++ b/lib/exprValue.mli @@ -15,13 +15,21 @@ type t = | `Unit ] include Binable.S with type t := t + include Sexpable.S with type t := t + include Comparable.S with type t := t val compare : t -> t -> int + val to_string : t -> String.t + val of_expr : Expr.t -> t + val of_value : Value.t -> t + val to_expr_exn : t -> Expr.t + val to_value_exn : t -> Value.t + val to_value : t -> Value.t Or_error.t diff --git a/lib/hypothesis.mli b/lib/hypothesis.mli index 765e8e6..276a37f 100644 --- a/lib/hypothesis.mli +++ b/lib/hypothesis.mli @@ -1,7 +1,6 @@ open Core open Core_extended.Std open Collections - open Infer (** Modules for constructing hypotheses. *) @@ -16,33 +15,34 @@ module StaticDistance : sig include Map.S with type Key.t = t val increment_scope : 'a t -> 'a t + val to_string : ('a -> string) -> 'a t -> string end - + (* include Comparable.S with type t := t and module Map := Map *) - (** Increment the scope of a coordinate. *) val increment_scope : t -> t + (** Increment the scope of a coordinate. *) - (** Increment the scope of every coordinate in a Map.t. *) val map_increment_scope : 'a Map.t -> 'a Map.t + (** Increment the scope of every coordinate in a Map.t. *) + val create : distance:int -> index:int -> t (** Create a static distance coordinate. @param distance The distance of the coordinate from its binding site, in number of bindings. @param index The binding index. *) - val create : distance:int -> index:int -> t - (** Get the distance of a static distance coordinate. *) val distance : t -> int + (** Get the distance of a static distance coordinate. *) - (** Get the index of a static distance coordinate. *) val index : t -> int + (** Get the index of a static distance coordinate. *) - (** Generate an arguments list with {i n} arguments. *) val args : int -> t list + (** Generate an arguments list with {i n} arguments. *) - (** Convert static distance coordinate to string. *) val to_string : t -> string + (** Convert static distance coordinate to string. *) end (** Symbols are constant strings with a fast comparison function. Used @@ -51,11 +51,15 @@ module Symbol : sig type t include Sexpable.S with type t := t + include Comparable.S with type t := t - + val compare : t -> t -> int + val equal : t -> t -> bool + val to_string : t -> string + val create : string -> t end @@ -63,19 +67,19 @@ end type context, and a symbol which defines the set of expressions which can be used to fill the hole. *) module Hole : sig - type t = private { - id : int; - ctx : Type.t StaticDistance.Map.t; - type_ : Type.t; - symbol : Symbol.t; - } + type t = private + {id: int; ctx: Type.t StaticDistance.Map.t; type_: Type.t; symbol: Symbol.t} include Sexpable.S with type t := t - + val compare : t -> t -> int + val equal : t -> t -> bool + val to_string : t -> string + val create : ?ctx:Type.t StaticDistance.Map.t -> Type.t -> Symbol.t -> t + val apply_unifier : Unifier.t -> t -> t end @@ -83,143 +87,158 @@ end {!Specification}s. *) module Skeleton : sig module Id : sig - type t = - | StaticDistance of StaticDistance.t - | Name of string + type t = StaticDistance of StaticDistance.t | Name of string include Sexpable.S with type t := t + include Comparable.S with type t := t end type spec_data = .. type ast = private - | Num of int - | Bool of bool - | List of t list - | Tree of t Tree.t - | Id of Id.t - | Hole of Hole.t - | Let of { bound : t; body : t } - | Lambda of { num_args : int; body : t } - | Apply of { func : t; args : t list } - | Op of { op : Expr.Op.t; args : t list } - and spec = { - verify : Library.t -> t -> bool; - compare : spec -> int; - to_sexp : unit -> Sexp.t; - to_string : unit -> string; - data : spec_data; - } - and skel = { - spec : spec; - ast : ast; - } + | Num of int + | Bool of bool + | List of t list + | Tree of t Tree.t + | Id of Id.t + | Hole of Hole.t + | Let of {bound: t; body: t} + | Lambda of {num_args: int; body: t} + | Apply of {func: t; args: t list} + | Op of {op: Expr.Op.t; args: t list} + + and spec = + { verify: Library.t -> t -> bool + ; compare: spec -> int + ; to_sexp: unit -> Sexp.t + ; to_string: unit -> string + ; data: spec_data } + + and skel = {spec: spec; ast: ast} + and t = skel Hashcons.hash_consed - (** Accessor functions for record fields. *) val spec : t -> spec + (** Accessor functions for record fields. *) + val ast : t -> ast - (** Replacement functions for record fields. *) val replace_spec : t -> spec -> t + (** Replacement functions for record fields. *) - (** Constructors for variants. *) val num : int -> spec -> t + (** Constructors for variants. *) + val bool : bool -> spec -> t + val list : t list -> spec -> t + val tree : t Tree.t -> spec -> t + val id : Id.t -> spec -> t + val hole : Hole.t -> spec -> t + val let_ : t -> t -> spec -> t + val lambda : int -> t -> spec -> t + val apply : t -> t List.t -> spec -> t + val op : Expr.Op.t -> t List.t -> spec -> t - + include Sexpable.S with type t := t - + module Table : sig val counter : Counter.t end val equal : t -> t -> bool + val to_string_hum : t -> string + val to_pp : ?indent:int -> t -> Pp.t - (** Convert a skeleton to an {!Expr.t}. - @param ctx A mapping from static distance variables to expressions. All SD variables will be replaced according to this mapping. - @param fresh_name A function which generates a fresh name. - @param of_hole A function which converts a {!Hole.t} into an {!Expr.t}. All holes will be converted according to this function. *) val to_expr : - ?ctx:Expr.t StaticDistance.Map.t + ?ctx:Expr.t StaticDistance.Map.t -> ?fresh_name:(unit -> string) -> ?of_hole:(Hole.t -> Expr.t) -> t -> Expr.t - + (** Convert a skeleton to an {!Expr.t}. + @param ctx A mapping from static distance variables to expressions. All SD variables will be replaced according to this mapping. + @param fresh_name A function which generates a fresh name. + @param of_hole A function which converts a {!Hole.t} into an {!Expr.t}. All holes will be converted according to this function. *) + + val to_expr_exn : + ?ctx:Expr.t StaticDistance.Map.t -> ?fresh_name:(unit -> string) -> t -> Expr.t (** Convert a skeleton to an {!Expr.t}. Throws an exception if a {!Hole.t} is encountered. @param ctx A mapping from static distance variables to expressions. All SD variables will be replaced according to this mapping. @param fresh_name A function which generates a fresh name. *) - val to_expr_exn : - ?ctx:Expr.t StaticDistance.Map.t - -> ?fresh_name:(unit -> string) - -> t - -> Expr.t end (** A CostModel assigns a cost to each variant of a skeleton. The total cost is the sum of the costs of the nodes. *) module CostModel : sig - type t = { - num : int -> int; - bool : bool -> int; - hole : Hole.t -> int; - id : Skeleton.Id.t -> int; - list : 'a. 'a list -> int; - tree : 'a. 'a Tree.t -> int; - _let : 'a. 'a -> 'a -> int; - lambda : 'a. int -> 'a -> int; - apply : 'a. 'a -> 'a list -> int; - op : 'a. Expr.Op.t -> 'a list -> int; - } + type t = + { num: int -> int + ; bool: bool -> int + ; hole: Hole.t -> int + ; id: Skeleton.Id.t -> int + ; list: 'a. 'a list -> int + ; tree: 'a. 'a Tree.t -> int + ; _let: 'a. 'a -> 'a -> int + ; lambda: 'a. int -> 'a -> int + ; apply: 'a. 'a -> 'a list -> int + ; op: 'a. Expr.Op.t -> 'a list -> int } - (** A cost model where variant has a constant cost. *) val constant : int -> t + (** A cost model where variant has a constant cost. *) - (** A cost model where variant has a cost of zero. *) val zero : t + (** A cost model where variant has a cost of zero. *) - (** Compute the cost of a skeleton. *) val cost_of_skeleton : t -> Skeleton.t -> int + (** Compute the cost of a skeleton. *) end module PerFunctionCostModel : sig type t + val to_cost_model : t -> CostModel.t + val to_json : t -> Json.json + val of_json : Json.json -> t end module Specification : sig type data = Skeleton.spec_data = .. + type data += private Top | Bottom - type t = Skeleton.spec = { - verify : 'a. Library.t -> Skeleton.t -> bool; - compare : t -> int; - to_sexp : unit -> Sexp.t; - to_string : unit -> string; - data : data; - } + type t = Skeleton.spec = + { verify: 'a. Library.t -> Skeleton.t -> bool + ; compare: t -> int + ; to_sexp: unit -> Sexp.t + ; to_string: unit -> string + ; data: data } include Comparable.S with type t := t + include Sexpable.S with type t := t - + val to_string : t -> string + val verify : t -> ?library:Library.t -> Skeleton.t -> bool + val equal : t -> t -> bool + val data : t -> data + val top : t + val bottom : t val increment_scope : t -> t @@ -227,6 +246,7 @@ end module Examples : sig type t + type example = Value.t StaticDistance.Map.t * Value.t [@@deriving sexp] type Specification.data += private Examples of t @@ -234,8 +254,11 @@ module Examples : sig include Sexpable.S with type t := t val of_list : example list -> t Or_error.t + val of_list_exn : example list -> t + val to_list : t -> example list + val singleton : example -> t val context : t -> StaticDistance.t list @@ -245,19 +268,24 @@ end module FunctionExamples : sig type t - type example = (Value.t StaticDistance.Map.t * Value.t list) * Value.t [@@deriving sexp] + + type example = (Value.t StaticDistance.Map.t * Value.t list) * Value.t + [@@deriving sexp] type Specification.data += private FunctionExamples of t - + include Sexpable.S with type t := t val of_list : example list -> t Or_error.t + val of_list_exn : example list -> t val of_input_output_list : (Value.t list * Value.t) list -> t Or_error.t + val of_input_output_list_exn : (Value.t list * Value.t) list -> t val to_list : t -> example list + val singleton : example -> t val to_spec : t -> Specification.t @@ -267,10 +295,13 @@ module Inputs : sig type t type Specification.data += private Inputs of t + include Sexpable.S with type t := t val of_examples : Examples.t -> t + val signature : Library.t -> Skeleton.t -> t -> Value.t list option + val to_spec : t -> Specification.t end @@ -278,43 +309,60 @@ end additional information: cost, abstract/concrete state, and a list of holes. *) module Hypothesis : sig - type kind = - | Abstract - | Concrete + type kind = Abstract | Concrete type t include Sexpable.S with type t := t val skeleton : t -> Skeleton.t + val cost : t -> int + val kind : t -> kind + val holes : t -> (Hole.t * Specification.t) list + val spec : t -> Specification.t val to_expr : t -> Expr.t + val to_string : t -> string + val to_string_hum : t -> string - + val compare_cost : t -> t -> int + val compare_skeleton : t -> t -> int - + val apply_unifier : t -> Unifier.t -> t + val fill_hole : CostModel.t -> Hole.t -> parent:t -> child:t -> t + val verify : ?library:Library.t -> t -> bool val of_skeleton : CostModel.t -> Skeleton.t -> t - (** Constructors *) val num : CostModel.t -> int -> Specification.t -> t + (** Constructors *) + val bool : CostModel.t -> bool -> Specification.t -> t + val id_sd : CostModel.t -> StaticDistance.t -> Specification.t -> t + val id_name : CostModel.t -> string -> Specification.t -> t + val hole : CostModel.t -> Hole.t -> Specification.t -> t + val list : CostModel.t -> t list -> Specification.t -> t + val tree : CostModel.t -> t Tree.t -> Specification.t -> t + val _let : CostModel.t -> t -> t -> Specification.t -> t + val lambda : CostModel.t -> int -> t -> Specification.t -> t + val apply : CostModel.t -> t -> t list -> Specification.t -> t + val op : CostModel.t -> Expr.Op.t -> t list -> Specification.t -> t end diff --git a/lib/infer.mli b/lib/infer.mli index 086780f..5c2dd42 100644 --- a/lib/infer.mli +++ b/lib/infer.mli @@ -1,5 +1,4 @@ open Core - open Ast open Collections @@ -8,9 +7,7 @@ exception TypeError of Error.t val total_infer_time : Time.Span.t ref module Type : sig - type const = const_typ = - | Num_t - | Bool_t + type const = const_typ = Num_t | Bool_t type level = int @@ -20,33 +17,44 @@ module Type : sig | Arrow_t of typ list * typ | Var_t of var_typ ref - and var = var_typ = - | Free of int * level - | Link of typ - | Quant of string + and var = var_typ = Free of int * level | Link of typ | Quant of string include Sexpable.S with type t := t - + val compare : t -> t -> int + val equal : t -> t -> bool + val nesting_depth : t -> int + val normalize : t -> t + val are_unifiable : t -> t -> bool + val arity : t -> int val of_string_exn : string -> t + val of_string : string -> t Or_error.t + val to_string : t -> string - val of_expr : ?ctx:t String.Map.t -> Expr.t -> (t * t Int.Map.t) + val of_expr : ?ctx:t String.Map.t -> Expr.t -> t * t Int.Map.t val num : t + val bool : t + val list : t -> t + val tree : t -> t + val quant : id -> t + val free : int -> level -> t + val arrow1 : t -> t -> t + val arrow2 : t -> t -> t -> t end @@ -54,20 +62,28 @@ module Unifier : sig type t = Type.t Int.Map.t include Sexpable.S with type t := t - + val empty : t + val apply : t -> Type.t -> Type.t + val compose : outer:t -> inner:t -> t + val equal : t -> t -> bool + val relevant_to : t -> Type.t -> t + val of_types_exn : Type.t -> Type.t -> t + val of_types : Type.t -> Type.t -> t option + val to_alist : t -> (int * Type.t) list + val of_alist_exn : (int * Type.t) list -> t + val to_string : t -> string end - module ImmutableType : sig type t = | Const_i of const_typ @@ -77,12 +93,15 @@ module ImmutableType : sig | Free_i of int * level include Sexpable.S with type t := t - + module Table : Hashtbl.S with type key = t val compare : t -> t -> int + val hash : t -> int + val of_type : Type.t -> t + val to_type : t -> Type.t end @@ -99,27 +118,46 @@ module TypedExpr : sig | Op of (Expr.Op.t * t list) * Type.t include Comparable.S with type t := t + include Sexpable.S with type t := t val normalize : t -> t + val map : f:(Type.t -> Type.t) -> t -> t + val to_expr : t -> Expr.t + val to_type : t -> Type.t + val to_string : t -> string end val fresh_free : int -> Type.t + val normalize : Type.t -> Type.t + val occurs : int -> int -> Type.t -> unit + val generalize : int -> Type.t -> Type.t + val instantiate : ?ctx:Type.t Ctx.t -> int -> Type.t -> Type.t + val unify_exn : Type.t -> Type.t -> unit + val unify : Type.t -> Type.t -> Type.t option + val is_unifiable : Type.t -> Type.t -> bool + val typeof : Type.t Ctx.t -> int -> Expr.t -> TypedExpr.t + val stdlib_tctx : Type.t Ctx.t + val infer_exn : Type.t Ctx.t -> Expr.t -> TypedExpr.t + val infer : Type.t Ctx.t -> Expr.t -> TypedExpr.t Or_error.t + val typed_expr_of_string : string -> TypedExpr.t + val stdlib_names : String.Set.t + val free : ?bound:String.Set.t -> TypedExpr.t -> (string * Type.t) list diff --git a/lib/library.mli b/lib/library.mli index 9b5f95a..51e1a28 100644 --- a/lib/library.mli +++ b/lib/library.mli @@ -1,19 +1,21 @@ open Core -type t = { - exprs : (string * Expr.t) list; - expr_ctx : Expr.t String.Map.t; - value_ctx : Value.t String.Map.t; - exprvalue_ctx : ExprValue.t String.Map.t; - type_ctx : Infer.Type.t String.Map.t; - builtins : Expr.Op.t list; -} +type t = + { exprs: (string * Expr.t) list + ; expr_ctx: Expr.t String.Map.t + ; value_ctx: Value.t String.Map.t + ; exprvalue_ctx: ExprValue.t String.Map.t + ; type_ctx: Infer.Type.t String.Map.t + ; builtins: Expr.Op.t list } val empty : t val from_channel_exn : file:string -> In_channel.t -> t + val from_channel : file:string -> In_channel.t -> t Or_error.t + val from_file_exn : string -> t + val from_file : string -> t Or_error.t val filter_keys : t -> f:(string -> bool) -> t diff --git a/lib/status.mli b/lib/status.mli index 24098d7..8e71999 100644 --- a/lib/status.mli +++ b/lib/status.mli @@ -1,10 +1,9 @@ open Collections -type status = { - synthesis : Counter.t; - hashcons : Counter.t; -} +type status = {synthesis: Counter.t; hashcons: Counter.t} val enable : unit -> unit + val disable : unit -> unit + val print_status : status -> unit diff --git a/lib/synthesis_common.mli b/lib/synthesis_common.mli index cf7acb4..bf2e662 100644 --- a/lib/synthesis_common.mli +++ b/lib/synthesis_common.mli @@ -1,71 +1,74 @@ open Core - open Collections open Hypothesis open Infer module Generalizer : sig - type t = Type.t StaticDistance.Map.t -> Type.t -> Symbol.t -> Specification.t -> (Hypothesis.t * Unifier.t) list + type t = + Type.t StaticDistance.Map.t + -> Type.t + -> Symbol.t + -> Specification.t + -> (Hypothesis.t * Unifier.t) list - type params = { - cost_model : CostModel.t; - library : Library.t; - } + type params = {cost_model: CostModel.t; library: Library.t} val generalize_single : params -> t -> Hypothesis.t -> Hypothesis.t list + val generalize_all : params -> t -> Hypothesis.t -> Hypothesis.t list + val compose : t -> t -> t + val compose_all_exn : t list -> t end module Deduction : sig type t = Skeleton.t -> Skeleton.t Option.t + val no_op : t + val bottom : t + val compose : t -> t -> t end val counter : Counter.t + val timer : Timer.t + val sexp_log : SexpLog.t module Memoizer : sig type t module Config : sig - type t = { - generalize : Generalizer.t; - cost_model : CostModel.t; - deduction : Deduction.t; - library : Library.t; - search_space_out : Out_channel.t Option.t; - } + type t = + { generalize: Generalizer.t + ; cost_model: CostModel.t + ; deduction: Deduction.t + ; library: Library.t + ; search_space_out: Out_channel.t Option.t } end val create : Config.t -> t + val to_string : t -> string - + val fill_holes_in_hypothesis : - t - -> Hypothesis.t - -> int - -> (Hypothesis.t * Unifier.t) Sequence.t - + t -> Hypothesis.t -> int -> (Hypothesis.t * Unifier.t) Sequence.t + val get : - t - -> Hole.t - -> Specification.t - -> cost:int -> (Hypothesis.t * Unifier.t) list + t -> Hole.t -> Specification.t -> cost:int -> (Hypothesis.t * Unifier.t) list val to_sequence : - t + t -> ?min_cost:int -> ?max_cost:int -> Hypothesis.t -> (Hypothesis.t * Unifier.t) Sequence.t Sequence.t - + val to_flat_sequence : - t + t -> ?min_cost:int -> ?max_cost:int -> Hypothesis.t diff --git a/lib/v1_engine.mli b/lib/v1_engine.mli index 44eb995..ac17d4a 100644 --- a/lib/v1_engine.mli +++ b/lib/v1_engine.mli @@ -1,26 +1,25 @@ open Core - open Collections open Infer -type config = { - verbosity: int; - untyped: bool; - deduction: bool; - infer_base: bool; - max_exhaustive_depth: int; - flat_cost:bool; -} +type config = + { verbosity: int + ; untyped: bool + ; deduction: bool + ; infer_base: bool + ; max_exhaustive_depth: int + ; flat_cost: bool } val default_init : TypedExpr.t List.t + (* val extended_init : TypedExpr.t List.t *) (* val default_operators : Expr.Op.t List.t *) - + (* val timer : Timer.t *) (* val counter : Counter.t *) - + val solve : - ?config:config + ?config:config -> ?bk:(String.t * Expr.t) List.t -> ?init:TypedExpr.t List.t -> Example.t List.t diff --git a/lib/v1_solver_engine.mli b/lib/v1_solver_engine.mli index d5c1e6e..480d3b8 100644 --- a/lib/v1_solver_engine.mli +++ b/lib/v1_solver_engine.mli @@ -1,19 +1,20 @@ open Core - open Collections open Infer val default_init : TypedExpr.t List.t + val extended_init : TypedExpr.t List.t + val default_operators : Expr.Op.t List.t - + val timer : Timer.t + val counter : Counter.t - + val solve : - ?config:Config.t + ?config:Config.t -> ?bk:(String.t * Expr.t) List.t -> ?init:TypedExpr.t List.t -> Example.t List.t -> Expr.t Ctx.t -