[WIP] 🔄 Cooltt Server 1.1

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: [

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
 

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

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))

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

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]

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)

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 <string list> IMPORT
@@ -307,6 +307,8 @@ plain_atomic_term_except_sq:
     { Hole (name, None) }
   | VISUALIZE
     { Visualize }
+  | EDIT
+    { Edit }
   | DIM
     { Dim }
   | COF

src/frontend/Lex.mll

@@ -23,6 +23,7 @@ let commands =
       ("#normalize", NORMALIZE);
       ("#print", PRINT);
       ("#viz", VISUALIZE);
+      ("#edit", EDIT);
       ("#quit", QUIT);
     ]
 

src/frontend/Server.ml

@@ -6,16 +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;
@@ -65,48 +71,90 @@ 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 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 serialize_boundary (ctx : (Ident.t * S.tp) list) (goal : S.tp) : J.t option =
+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 run dims env (id, tp) =
+    serialize_cube id dims @@ type_labels dims env tp
+  in List.map (run Emp env) ctx
+
+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 (_, _, bdry) ->
-          let dim_names = BwdLabels.to_list @@ BwdLabels.filter_map ~f:Fun.id dims in
-          let labels = boundary_labels dims env bdry in
-          let context = Format.asprintf "%a" (S.pp_sequent ~lbl:None ctx) goal in
-          let msg = `O [
-              ("dims", `A (List.map J.string dim_names));
-              ("labels", `A labels);
-              ("context", `String context)
-            ] 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 ->
@@ -115,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

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