From c78e0c39834ba4e7936433c2f5d8f97a3309d7e0 Mon Sep 17 00:00:00 2001 From: hazel levine Date: Wed, 13 Jul 2022 11:00:52 -0500 Subject: [PATCH 1/2] [WIP] Serialize the labels of objects in the context Currently the pretty-printer env is broken on this --- src/frontend/Server.ml | 59 +++++++++++++++++++++++++++++++++++------- 1 file changed, 49 insertions(+), 10 deletions(-) diff --git a/src/frontend/Server.ml b/src/frontend/Server.ml index 88ed80e88..fb30ccff2 100644 --- a/src/frontend/Server.ml +++ b/src/frontend/Server.ml @@ -7,7 +7,6 @@ open Core open CodeUnit module S = Syntax - module J = Ezjsonm (* [NOTE: Cooltt Server] @@ -65,22 +64,60 @@ let rec dim_from_cof (dims : (string option) bwd) (cof : S.t) : (string * float) failwith @@ Format.asprintf "dim_from_cof: bad cof '%a'" S.dump cof (* Create our list of labels from a boundary constraint. *) -let boundary_labels (dims : (string option) bwd) (env : Pp.env) (tm : S.t) : J.value list = +let boundary_labels (dims : (string option) bwd) (env : Pp.env) (cof : S.t) (tm : S.t) : J.value list = let rec go env dims (bdry, cons) = match cons with | S.CofSplit branches -> - let (_x, envx) = ppenv_bind env `Anon in + let (_x, envx) = ppenv_bind env Ident.anon in List.concat_map (go envx (Snoc (dims, None))) branches | _ -> - let (_x, envx) = ppenv_bind env `Anon in + let (_x, envx) = ppenv_bind env Ident.anon in let lbl = Format.asprintf "%a" (S.pp envx) cons in List.map (serialize_label lbl) @@ dim_from_cof (Snoc (dims, None)) bdry in + let (_, envx) = ppenv_bind env Ident.anon in match tm with - | S.CofSplit branches -> - let (_x, envx) = ppenv_bind env `Anon in + | S.CofSplit branches -> List.concat_map (go envx dims) branches - | _ -> [] + | _ -> + let lbl = Format.asprintf "%a" (S.pp envx) tm in + List.map (serialize_label lbl) @@ dim_from_cof dims cof + + +let context_labels (ctx : (Ident.t * S.tp) list) (env : Pp.env) : J.value list = + let serialize_cube id dims labels = + let dim_names = BwdLabels.to_list @@ BwdLabels.filter_map ~f:Fun.id dims in + `O [ + ("id", `String (Ident.to_string id)); + ("dims", `A (List.map J.string dim_names)); + ("labels", `A labels) + ] + in + let rec unpack_bdry_lam tm env = + match tm with + | S.Lam (var, body) -> + let (_, envx) = ppenv_bind env var in + unpack_bdry_lam body envx + | _ -> tm, env + in + let rec type_labels dims env (id, tp) = + match tp with + | S.Sub (_, cof, tm) -> + let labels = boundary_labels dims env cof tm in + serialize_cube id dims labels + | S.El (S.CodeExt (_, cof, _, bdry_lam)) -> + let (tm, envx) = unpack_bdry_lam bdry_lam env in + let labels = boundary_labels dims envx cof tm in + serialize_cube id dims labels + | S.Pi (dom, var, cod) -> + let (dim_name, envx) = ppenv_bind env var in + begin + match dom with + | S.TpDim -> type_labels (Snoc (dims, Some dim_name)) envx (id, cod) + | _ -> type_labels (Snoc (dims, None)) envx (id, cod) + end + | _ -> serialize_cube id dims [] + in List.map (type_labels Emp env) ctx let serialize_boundary (ctx : (Ident.t * S.tp) list) (goal : S.tp) : J.t option = let rec go dims env = @@ -88,14 +125,16 @@ let serialize_boundary (ctx : (Ident.t * S.tp) list) (goal : S.tp) : J.t option | [] -> begin match goal with - | S.Sub (_, _, bdry) -> + | S.Sub (_, cof, tm) -> let dim_names = BwdLabels.to_list @@ BwdLabels.filter_map ~f:Fun.id dims in - let labels = boundary_labels dims env bdry in + let labels = boundary_labels dims env cof tm in let context = Format.asprintf "%a" (S.pp_sequent ~lbl:None ctx) goal in + let ctx_labels = context_labels ctx env in let msg = `O [ ("dims", `A (List.map J.string dim_names)); ("labels", `A labels); - ("context", `String context) + ("context", `String context); + ("cubes", `A ctx_labels) ] in Some (`O [("DisplayGoal", msg)]) | _ -> None From e085f93001217dfdca7c526872953fc2dfa4aa10 Mon Sep 17 00:00:00 2001 From: hazel levine Date: Mon, 18 Jul 2022 13:55:45 -0500 Subject: [PATCH 2/2] add rudimentary #edit to the elaborator super duper untested --- cooltt.opam | 4 +- src/core/Ident.ml | 3 + src/core/Ident.mli | 6 ++ src/core/dune | 4 +- src/frontend/ConcreteSyntax.mli | 10 +++ src/frontend/ConcreteSyntaxData.ml | 44 +++++++++- src/frontend/Elaborator.ml | 21 ++++- src/frontend/Grammar.mly | 4 +- src/frontend/Lex.mll | 1 + src/frontend/Server.ml | 136 +++++++++++++++++++---------- src/frontend/Server.mli | 10 ++- src/frontend/Tactics.ml | 16 ++-- src/frontend/Tactics.mli | 2 +- src/frontend/dune | 4 +- 14 files changed, 201 insertions(+), 64 deletions(-) diff --git a/cooltt.opam b/cooltt.opam index b572f19b9..37ecc5377 100644 --- a/cooltt.opam +++ b/cooltt.opam @@ -18,14 +18,16 @@ depends: [ "containers" {>= "3.4"} "ezjsonm" {>= "1.2.0"} "menhir" {>= "20180703"} + "ppx_yojson_conv" {>= "0.15.0"} "uuseg" {>= "12.0.0"} "uutf" {>= "1.0.2"} + "yojson" {>= "1.7" & < "2"} "yuujinchou" {>= "2.0.0" & < "3"} "odoc" {with-doc} "kado" ] pin-depends: [ - [ "kado.~dev" "git+https://github.com/RedPRL/kado" ] + [ "kado.~dev" "git+https://github.com/RedPRL/kado#main" ] [ "bantorra.0.1.0" "git+https://github.com/RedPRL/bantorra#1e78633d9a2ef7104552a24585bb8bea36d4117b" ] ] build: [ diff --git a/src/core/Ident.ml b/src/core/Ident.ml index fee37ce03..ec86767a0 100644 --- a/src/core/Ident.ml +++ b/src/core/Ident.ml @@ -1,6 +1,9 @@ +(* [NOTE: June; 2022-07-14] See ConcreteSyntaxData for Yojson stuff *) type t = [`Anon | `User of string list | `Machine of string | `Unfolder of t | `Blocked of t list] +[@@deriving yojson] type 'a some = 'a constraint 'a = [< t ] type user = [ `User of string list ] +[@@deriving yojson] module J = Ezjsonm diff --git a/src/core/Ident.mli b/src/core/Ident.mli index b9a4d1bae..166921e76 100644 --- a/src/core/Ident.mli +++ b/src/core/Ident.mli @@ -26,4 +26,10 @@ val json_to_ident : J.value -> t val json_of_user : [`User of string list ] -> [> `A of J.value list ] val json_to_user : J.value -> [`User of string list] +(* [HACK: June; 2022-07-14] derived *) +val yojson_of_t : t -> Yojson.Safe.t +val t_of_yojson : Yojson.Safe.t -> t +val yojson_of_user : user -> Yojson.Safe.t +val user_of_yojson : Yojson.Safe.t -> user + val equal : user -> user -> bool diff --git a/src/core/dune b/src/core/dune index 09a307b1c..51bfc81e9 100644 --- a/src/core/dune +++ b/src/core/dune @@ -1,8 +1,8 @@ (library (name Core) - (libraries kado bantorra cooltt.basis ezjsonm yuujinchou bwd) + (libraries kado bantorra cooltt.basis ezjsonm yuujinchou bwd yojson) (preprocess - (pps ppx_deriving.std)) + (pps ppx_deriving.std ppx_yojson_conv)) (flags (:standard -w -32-37-38 -warn-error -a+31)) (public_name cooltt.core)) diff --git a/src/frontend/ConcreteSyntax.mli b/src/frontend/ConcreteSyntax.mli index 80f998ae9..a8b33c526 100644 --- a/src/frontend/ConcreteSyntax.mli +++ b/src/frontend/ConcreteSyntax.mli @@ -2,3 +2,13 @@ include module type of ConcreteSyntaxData val show_con : con -> string val pp_con : Format.formatter -> con -> unit + +(* [HACK: June; 2022-07-14] See ConcreteSyntaxData *) +module J = Ezjsonm +module Y = Yojson.Safe + +val yojson_of_ezjsonm : J.value -> Y.t +val ezjsonm_of_yojson : Y.t -> J.value + +val con_of_yojson : Y.t -> con +val yojson_of_con : con -> Y.t diff --git a/src/frontend/ConcreteSyntaxData.ml b/src/frontend/ConcreteSyntaxData.ml index e92b903e5..40f933a84 100644 --- a/src/frontend/ConcreteSyntaxData.ml +++ b/src/frontend/ConcreteSyntaxData.ml @@ -1,6 +1,40 @@ open Basis open Core +(* [HACK: June; 2022-07-14] We are using Yojson to avoid having to write a serializer + for concrete syntax by hand. However, the rest of cooltt uses Ezjsonm. In my mind, this + is justification to dump Ezjsonm. But for now, we need a converter. + + Maybe this should go somewhere else. But considering that this is /the/ module that uses + Yojson, I put it here. *) + +module J = Ezjsonm +module Y = Yojson.Safe + +let rec yojson_of_ezjsonm (j : J.value) : Y.t = + match j with + | `A vals -> `List (List.map yojson_of_ezjsonm vals) + | `O vals -> `Assoc (List.map (fun (k, v) -> (k, yojson_of_ezjsonm v)) vals) + (* [HACK: June; 2022-07-14] Do we need more sophisticated float conversion? *) + | `Float f -> `Float f + | `Null -> `Null + | `Bool b -> `Bool b + | `String s -> `String s + +let rec ezjsonm_of_yojson (j : Y.t) : J.value = + match j with + | `List vals + | `Tuple vals -> `A (List.map ezjsonm_of_yojson vals) + | `Assoc vals -> `O (List.map (fun (k, v) -> (k, ezjsonm_of_yojson v)) vals) + | `Variant (label, Some x) -> `A [`String label; ezjsonm_of_yojson x] + | `Variant (label, None) -> `String label + | `Intlit i -> `String i + | `Null -> `Null + | `Float f -> `Float f + | `Bool b -> `Bool b + | `String s -> `String s + | `Int i -> `Float (float_of_int i) + type info = LexingUtil.span option let pp_info fmt = @@ -11,11 +45,12 @@ let pp_info fmt = type 'a node = {node : 'a; - info : info} -[@@deriving show] + info : (info [@yojson.opaque]) + } +[@@deriving show, yojson] type hole = {name: string option; silent: bool} -[@@deriving show] +[@@deriving show, yojson] let map_node ~f n = {n with node = f n.node} let get_info n = n.info @@ -50,6 +85,7 @@ and con_ = | Hole of hole * con option | BoundaryHole of con option | Visualize + | Edit | Underscore | Generalize of Ident.t * con | Unfold of Ident.t list * con @@ -88,7 +124,7 @@ and con_ = | ModUnion of con list | ModInSubtree of string list * con | ModPrint of hole -[@@deriving show] +[@@deriving show, yojson] and case = pat * con [@@deriving show] diff --git a/src/frontend/Elaborator.ml b/src/frontend/Elaborator.ml index 81e347924..880c23dc9 100644 --- a/src/frontend/Elaborator.ml +++ b/src/frontend/Elaborator.ml @@ -189,7 +189,26 @@ and chk_tm : CS.con -> T.Chk.tac = | CS.Generalize (ident, c) -> R.Structural.generalize ident (chk_tm c) - | CS.Visualize -> R.Probe.probe_goal_chk (fun ctx goal -> RM.ret @@ Server.dispatch_goal ctx goal) @@ R.Hole.unleash_hole None + | CS.Visualize -> + R.Probe.probe_goal_chk (fun ctx goal -> RM.ret @@ Server.dispatch_goal ctx goal) + @@ R.Hole.unleash_hole None + + | CS.Edit -> + Tactics.refine + (R.Probe.probe_goal_chk (fun ctx goal -> RM.ret @@ Server.dispatch_goal ctx goal) + @@ R.Hole.unleash_hole None) + @@ fun ctx goals err -> + begin + match err with + | Some exn -> + (* [TODO: June; 2022-07-15] Send message to the server, and undo the last action *) + raise exn + | None -> + let* tm = Server.send_faces ctx goals in + match tm with + | Some tm -> RM.ret @@ chk_tm tm + | None -> RM.ret @@ R.Hole.unleash_hole None + end | CS.HComChk (src, trg, tm) -> R.Univ.hcom_chk (chk_tm src) (chk_tm trg) (chk_tm tm) diff --git a/src/frontend/Grammar.mly b/src/frontend/Grammar.mly index c1acdd207..0973f78ee 100644 --- a/src/frontend/Grammar.mly +++ b/src/frontend/Grammar.mly @@ -54,7 +54,7 @@ %token SIG STRUCT AS INCLUDE RENAMING OPEN %token EXT %token COE COM HCOM HFILL -%token QUIT NORMALIZE PRINT DEF AXIOM ABSTRACT FAIL VISUALIZE +%token QUIT NORMALIZE PRINT DEF AXIOM ABSTRACT FAIL VISUALIZE EDIT %token UNFOLD %token IMPORT @@ -307,6 +307,8 @@ plain_atomic_term_except_sq: { Hole (name, None) } | VISUALIZE { Visualize } + | EDIT + { Edit } | DIM { Dim } | COF diff --git a/src/frontend/Lex.mll b/src/frontend/Lex.mll index 225a3a403..feae8a0d1 100644 --- a/src/frontend/Lex.mll +++ b/src/frontend/Lex.mll @@ -23,6 +23,7 @@ let commands = ("#normalize", NORMALIZE); ("#print", PRINT); ("#viz", VISUALIZE); + ("#edit", EDIT); ("#quit", QUIT); ] diff --git a/src/frontend/Server.ml b/src/frontend/Server.ml index fb30ccff2..9b2095060 100644 --- a/src/frontend/Server.ml +++ b/src/frontend/Server.ml @@ -6,15 +6,22 @@ module K = Kado.Syntax open Core open CodeUnit +module CS = ConcreteSyntax +module D = Domain module S = Syntax +module R = Refiner +module RM = RefineMonad module J = Ezjsonm +module Y = Yojson.Safe + +open Monad.Notation (RM) +module M = Monad.Util (RM) (* [NOTE: Cooltt Server] We use a 'ref' here to prevent having to thread down a server handle deep into the guts of the elaborator. *) let server : Unix.file_descr option ref = ref None - let init host_name port = try Format.eprintf "Initializing cooltt server connection on port %n...@." port; @@ -83,6 +90,28 @@ let boundary_labels (dims : (string option) bwd) (env : Pp.env) (cof : S.t) (tm let lbl = Format.asprintf "%a" (S.pp envx) tm in List.map (serialize_label lbl) @@ dim_from_cof dims cof +let rec type_labels dims env tp = + let rec unpack_bdry_lam tm env = + match tm with + | S.Lam (var, body) -> + let (_, envx) = ppenv_bind env var in + unpack_bdry_lam body envx + | _ -> tm, env + in + match tp with + | S.Sub (_, cof, tm) -> + boundary_labels dims env cof tm + | S.El (S.CodeExt (_, cof, _, bdry_lam)) -> + let (tm, envx) = unpack_bdry_lam bdry_lam env in + boundary_labels dims envx cof tm + | S.Pi (dom, var, cod) -> + let (dim_name, envx) = ppenv_bind env var in + begin + match dom with + | S.TpDim -> type_labels (Snoc (dims, Some dim_name)) envx cod + | _ -> type_labels (Snoc (dims, None)) envx cod + end + | _ -> [] let context_labels (ctx : (Ident.t * S.tp) list) (env : Pp.env) : J.value list = let serialize_cube id dims labels = @@ -93,59 +122,39 @@ let context_labels (ctx : (Ident.t * S.tp) list) (env : Pp.env) : J.value list = ("labels", `A labels) ] in - let rec unpack_bdry_lam tm env = - match tm with - | S.Lam (var, body) -> - let (_, envx) = ppenv_bind env var in - unpack_bdry_lam body envx - | _ -> tm, env - in - let rec type_labels dims env (id, tp) = - match tp with - | S.Sub (_, cof, tm) -> - let labels = boundary_labels dims env cof tm in - serialize_cube id dims labels - | S.El (S.CodeExt (_, cof, _, bdry_lam)) -> - let (tm, envx) = unpack_bdry_lam bdry_lam env in - let labels = boundary_labels dims envx cof tm in - serialize_cube id dims labels - | S.Pi (dom, var, cod) -> - let (dim_name, envx) = ppenv_bind env var in - begin - match dom with - | S.TpDim -> type_labels (Snoc (dims, Some dim_name)) envx (id, cod) - | _ -> type_labels (Snoc (dims, None)) envx (id, cod) - end - | _ -> serialize_cube id dims [] - in List.map (type_labels Emp env) ctx + let run dims env (id, tp) = + serialize_cube id dims @@ type_labels dims env tp + in List.map (run Emp env) ctx -let serialize_boundary (ctx : (Ident.t * S.tp) list) (goal : S.tp) : J.t option = +let ppenv_bind_ctx (ctx : (Ident.t * S.tp) list) (env : Pp.env) : string option bwd * Pp.env = let rec go dims env = function - | [] -> - begin - match goal with - | S.Sub (_, cof, tm) -> - let dim_names = BwdLabels.to_list @@ BwdLabels.filter_map ~f:Fun.id dims in - let labels = boundary_labels dims env cof tm in - let context = Format.asprintf "%a" (S.pp_sequent ~lbl:None ctx) goal in - let ctx_labels = context_labels ctx env in - let msg = `O [ - ("dims", `A (List.map J.string dim_names)); - ("labels", `A labels); - ("context", `String context); - ("cubes", `A ctx_labels) - ] in - Some (`O [("DisplayGoal", msg)]) - | _ -> None - end + | [] -> (dims, env) | (var, var_tp) :: ctx -> let (dim_name, envx) = ppenv_bind env var in match var_tp with | S.TpDim -> go (Snoc (dims, Some dim_name)) envx ctx | _ -> go (Snoc (dims, None)) envx ctx - in go Emp Pp.Env.emp ctx + in go Emp env ctx +let serialize_boundary (ctx : (Ident.t * S.tp) list) (goal : S.tp) : J.t option = + let (dims, env) = ppenv_bind_ctx ctx Pp.Env.emp in + match goal with + | S.Sub (_, cof, tm) -> + let dim_names = BwdLabels.to_list @@ BwdLabels.filter_map ~f:Fun.id dims in + let labels = boundary_labels dims env cof tm in + let context = Format.asprintf "%a" (S.pp_sequent ~lbl:None ctx) goal in + let ctx_labels = context_labels ctx env in + let msg = `O [ + ("dims", `A (List.map J.string dim_names)); + ("labels", `A labels); + ("context", `String context); + ("cubes", `A ctx_labels) + ] in + Some (`O [("DisplayGoal", msg)]) + | _ -> None + +(* Sends the current context and goal to the server. *) let dispatch_goal ctx goal = match !server, serialize_boundary ctx goal with | Some socket, Some msg -> @@ -154,10 +163,45 @@ let dispatch_goal ctx goal = let buf = Buffer.create 65536 in J.to_buffer ~minify:true buf msg; let nbytes = Unix.send socket (Buffer.to_bytes buf) 0 (Buffer.length buf) [] in - Debug.print "Sent %n bytes to Server.@." nbytes; + Debug.print "dispatch_goal: Sent %n bytes to Server.@." nbytes; () with Unix.Unix_error _ -> Format.eprintf "Cooltt server connection lost.@."; close () end | _, _ -> () + +let serialize_faces ctx goals = + let (dims, env) = ppenv_bind_ctx ctx Pp.Env.emp in + let serialize_goal (tp, phi, _) = + let* tp = RM.quote_tp tp in + let* phi = RM.quote_cof phi in + let lbl = Format.asprintf "%a" (S.pp_tp env) tp in + let pos = dim_from_cof dims phi in + RM.ret @@ `A (List.map (serialize_label lbl) pos) + in + let* ser = M.map serialize_goal goals in + RM.ret @@ `O [("EditGoal", `A ser)] + +(* Sends the faces of the cube (holes in the hcom) to the server, and blocks until the server + sends a ConcreteSyntax. This then gets elaborated. *) +let send_faces ctx goals = + let* msg = serialize_faces ctx goals in + match !server with + | Some socket -> + begin + try + let buf = Buffer.create 65536 in + J.to_buffer ~minify:true buf msg; + let nbytes = Unix.send socket (Buffer.to_bytes buf) 0 (Buffer.length buf) [] in + Debug.print "send_faces: Sent %n bytes to Server.@." nbytes; + Buffer.clear buf; + let nbytes = Unix.recv socket (Buffer.to_bytes buf) 0 (Buffer.length buf) [] in + Debug.print "send_faces: Received %n bytes from Server.@." nbytes; + RM.ret @@ Some (CS.con_of_yojson @@ Y.from_string @@ Buffer.contents buf) + with Unix.Unix_error _ -> + Format.eprintf "Cooltt server connection lost.@."; + close (); + RM.ret None + end + | _ -> RM.ret None diff --git a/src/frontend/Server.mli b/src/frontend/Server.mli index bc694a535..c29855655 100644 --- a/src/frontend/Server.mli +++ b/src/frontend/Server.mli @@ -1,7 +1,15 @@ open Core open CodeUnit +module CS := ConcreteSyntax +module D := Domain +module T := Tactic +module S := Syntax +module RM := RefineMonad + val init : string -> int -> unit val close : unit -> unit -val dispatch_goal : (Ident.t * Syntax.tp) list -> Syntax.tp -> unit +val dispatch_goal : (Ident.t * S.tp) list -> S.tp -> unit + +val send_faces : (Ident.t * S.tp) list -> (D.tp * D.cof * D.tm_clo) list -> CS.con option RM.m diff --git a/src/frontend/Tactics.ml b/src/frontend/Tactics.ml index 8e2becdaf..a2865ad4b 100644 --- a/src/frontend/Tactics.ml +++ b/src/frontend/Tactics.ml @@ -1,4 +1,5 @@ open Basis +open Bwd open Core open CodeUnit @@ -7,6 +8,7 @@ module T = Tactic module D = Domain module S = Syntax module R = Refiner +module Env = RefineEnv module CS = ConcreteSyntax module Sem = Semantics module TB = TermBuilder @@ -44,7 +46,7 @@ let match_goal (tac : _ -> T.Chk.tac RM.m) : T.Chk.tac = let* tac = tac goal in T.Chk.brun tac goal -let refine k = +let refine tac k = T.Chk.brule @@ fun (tp, phi, tm_clo) -> let rec go tac = (* [HACK: Hole State] @@ -64,17 +66,21 @@ let refine k = let* after_holes = RM.get_holes in let n_holes = List.length after_holes - List.length before_holes in let holes = CCList.take n_holes after_holes in + let* env = RM.read in + let cells = Env.locals env in + let* ctx = RM.destruct_cells @@ BwdLabels.to_list cells in match holes, r with | [], Ok tm -> RM.ret tm | holes, Ok _ -> let* () = RM.set st in - go (k holes None) + let* tac = k ctx holes None in + go tac | holes, Error exn -> let* () = RM.set st in - go (k holes (Some exn)) + let* tac = k ctx holes (Some exn) in + go tac in - (* [TODO: Reed M, 14/06/2022] Should we 'unleash_hole' here, or cof split? *) - go (R.Hole.unleash_hole None) + go tac let rec elim_implicit_connectives : T.Syn.tac -> T.Syn.tac = fun tac -> diff --git a/src/frontend/Tactics.mli b/src/frontend/Tactics.mli index 77c085746..858af85dd 100644 --- a/src/frontend/Tactics.mli +++ b/src/frontend/Tactics.mli @@ -31,7 +31,7 @@ val tac_nary_quantifier : ('a, 'b) R.quantifier -> (Ident.t * 'a) list -> 'b -> val match_goal : (D.tp * D.cof * D.tm_clo -> Chk.tac RM.m) -> Chk.tac -val refine : ((D.tp * D.cof * D.tm_clo) list -> exn option -> Chk.tac) -> Chk.tac +val refine : Chk.tac -> ((Ident.t * S.tp) list -> (D.tp * D.cof * D.tm_clo) list -> exn option -> Chk.tac RM.m) -> Chk.tac module Elim : sig type case_tac = CS.pat * Chk.tac diff --git a/src/frontend/dune b/src/frontend/dune index d58d873dd..f2b1fa87a 100644 --- a/src/frontend/dune +++ b/src/frontend/dune @@ -6,9 +6,9 @@ (library (name Frontend) - (libraries kado bantorra cooltt.basis cooltt.core ezjsonm menhirLib) + (libraries kado bantorra cooltt.basis cooltt.core ezjsonm menhirLib yojson) (preprocess - (pps ppx_deriving.std)) + (pps ppx_deriving.std ppx_yojson_conv)) (flags (:standard -w -32-37-38 -warn-error -a+31)) (public_name cooltt.frontend))