feat(proof): emit is-a terms properly

these occur in datatypes proofs.

src/base/Proof.ml

@@ -145,7 +145,14 @@ let rec emit_term_ (self:t) (t:Term.t) : term_id =
       | Term_cell.Not a ->
         PS.Step_view.Expr_not {PS.Expr_not.f=a}
 
+      | Term_cell.App_fun ({fun_view=Fun.Fun_is_a c;_}, args) ->
+        assert (IArray.length args=1);
+        let c = emit_fun_ self (Fun.cstor c) in
+        let arg = IArray.get args 0 in
+        PS.Step_view.Expr_isa {PS.Expr_isa.c; arg}
+
       | Term_cell.App_fun (f, arr) ->
+
         let f = emit_fun_ self f in
         PS.Step_view.Expr_app {PS.Expr_app.f; args=(arr:_ IArray.t:> _ array)}
 

src/base/Proof_quip.ml

@@ -56,6 +56,10 @@ end = struct
   (* id -> function symbol *)
   let funs: P.Fun.t Util.Int_tbl.t = Util.Int_tbl.create 32
 
+  let find_fun (f:PS.ID.t) : P.Fun.t =
+    try Util.Int_tbl.find funs (Int32.to_int f)
+    with Not_found -> Error.errorf "unknown function '%ld'" f
+
   (* list of toplevel steps, in the final proof order *)
   let top_steps_ : P.composite_step lazy_t list ref = ref []
   let add_top_step s = top_steps_ := s :: !top_steps_
@@ -149,14 +153,21 @@ end = struct
           let t = Lazy.from_val (P.T.bool b) in
           L_terms.add lid t
 
+        | PS.Step_view.Expr_isa {c; arg} ->
+          add_needed_step c;
+          add_needed_step arg;
+          let t = lazy (
+            let c = find_fun c in
+            let arg = L_terms.find arg in
+            P.T.is_a c arg
+          ) in
+          L_terms.add lid t
+
         | PS.Step_view.Expr_app { f; args } ->
           add_needed_step f;
           Array.iter add_needed_step args;
           let t = lazy (
-            let f =
-              try Util.Int_tbl.find funs (Int32.to_int f)
-              with Not_found -> Error.errorf "unknown function '%ld'" f
-            in
+            let f = find_fun f in
             let args = Array.map L_terms.find args in
             P.T.app_fun f args
           ) in

src/proof-trace/proof_ser.bare

@@ -105,6 +105,11 @@ type Expr_app {
   args: []ID
 }
 
+type Expr_isa {
+  c: ID
+  arg: ID
+}
+
 type Step_view
   ( Step_input
   | Step_unsat
@@ -123,6 +128,7 @@ type Step_view
   | Expr_bool
   | Expr_if
   | Expr_not
+  | Expr_isa
   | Expr_eq
   | Expr_app
   )

src/proof-trace/proof_ser.ml

@@ -879,6 +879,30 @@ module Expr_app = struct
 
 end
 
+module Expr_isa = struct
+  type t = {
+    c: ID.t;
+    arg: ID.t;
+  }
+  
+  (** @raise Bare.Decode.Error in case of error. *)
+  let decode (dec: Bare.Decode.t) : t =
+    let c = ID.decode dec in let arg = ID.decode dec in {c; arg; }
+  
+  let encode (enc: Bare.Encode.t) (self: t) : unit =
+    begin ID.encode enc self.c; ID.encode enc self.arg; end
+  
+  let pp out (self:t) : unit =
+    (fun out x ->
+     begin
+       Format.fprintf out "{ @[";
+       Format.fprintf out "c=%a;@ " ID.pp x.c;
+       Format.fprintf out "arg=%a;@ " ID.pp x.arg;
+       Format.fprintf out "@]}";
+     end) out self
+
+end
+
 module Step_view = struct
   type t =
     | Step_input of Step_input.t
@@ -898,6 +922,7 @@ module Step_view = struct
     | Expr_bool of Expr_bool.t
     | Expr_if of Expr_if.t
     | Expr_not of Expr_not.t
+    | Expr_isa of Expr_isa.t
     | Expr_eq of Expr_eq.t
     | Expr_app of Expr_app.t
     
@@ -923,8 +948,9 @@ module Step_view = struct
     | 14L -> Expr_bool (Expr_bool.decode dec)
     | 15L -> Expr_if (Expr_if.decode dec)
     | 16L -> Expr_not (Expr_not.decode dec)
-    | 17L -> Expr_eq (Expr_eq.decode dec)
-    | 18L -> Expr_app (Expr_app.decode dec)
+    | 17L -> Expr_isa (Expr_isa.decode dec)
+    | 18L -> Expr_eq (Expr_eq.decode dec)
+    | 19L -> Expr_app (Expr_app.decode dec)
     | _ -> raise (Bare.Decode.Error(Printf.sprintf "unknown union tag Step_view.t: %Ld" tag))
     
   
@@ -981,11 +1007,14 @@ module Step_view = struct
     | Expr_not x ->
       Bare.Encode.uint enc 16L;
       Expr_not.encode enc x
-    | Expr_eq x ->
+    | Expr_isa x ->
       Bare.Encode.uint enc 17L;
+      Expr_isa.encode enc x
+    | Expr_eq x ->
+      Bare.Encode.uint enc 18L;
       Expr_eq.encode enc x
     | Expr_app x ->
-      Bare.Encode.uint enc 18L;
+      Bare.Encode.uint enc 19L;
       Expr_app.encode enc x
     
     
@@ -1025,6 +1054,8 @@ module Step_view = struct
         Format.fprintf out "(@[Expr_if@ %a@])" Expr_if.pp x
       | Expr_not x ->
         Format.fprintf out "(@[Expr_not@ %a@])" Expr_not.pp x
+      | Expr_isa x ->
+        Format.fprintf out "(@[Expr_isa@ %a@])" Expr_isa.pp x
       | Expr_eq x ->
         Format.fprintf out "(@[Expr_eq@ %a@])" Expr_eq.pp x
       | Expr_app x ->

src/quip/Proof.ml

@@ -40,6 +40,7 @@ module T = struct
     | Bool of bool
     | App_fun of Fun.t * t array
     | App_ho of t * t
+    | Is_a of Fun.t * t
     | Ite of t * t * t
     | Not of t
     | Eq of t * t
@@ -59,6 +60,7 @@ module T = struct
   let const c = app_fun c [||]
   let app_ho a b : t = App_ho (a,b)
   let ite a b c : t = Ite (a,b,c)
+  let is_a f t : t = Is_a (f,t)
 
   let rec pp out = function
     | Bool b -> Fmt.bool out b
@@ -70,6 +72,7 @@ module T = struct
     | Not a -> Fmt.fprintf out "(@[not@ %a@])" pp a
     | Eq (a,b) -> Fmt.fprintf out "(@[=@ %a@ %a@])" pp a pp b
     | Ref name -> Fmt.fprintf out "(@@ %s)" name
+    | Is_a (c,t) -> Fmt.fprintf out "(@[(_ is %a)@ %a@])" Fun.pp c pp t
 end
 
 type term = T.t

src/quip/Sidekick_quip.ml

@@ -28,6 +28,7 @@ module Make_printer(Out : OUT) = struct
     | T.App_fun (c, [||]) -> a c
     | T.App_fun (c, args) ->
       l(a c :: Util.array_to_list_map pp_t args)
+    | T.Is_a(c,u) -> l[l[a"_";a"is";a c];pp_t u] (* ((_ is c) t) *)
     | T.Ref name -> l[a"@"; a name]
     | T.App_ho(f,a) -> l[pp_t f;pp_t a]
     | T.Eq (t,u) -> l[a"=";pp_t t;pp_t u]