Update printing function

plugin/src/library/coq/printing.ml

@@ -15,6 +15,7 @@ open Coqenvs
 open Printer
 open Utilities
 open Goptions
+open Collections
 
 module CRD = Context.Rel.Declaration
 
@@ -95,10 +96,38 @@ let rec term_as_string (env : env) (trm : types) =
      let ind_bodies = mutind_body.mind_packets in
      let name_id = (ind_bodies.(i_index)).mind_typename in
      string_of_id name_id
-  | Case (ci, ct, m, bs) -> (* TODO *)
-     Printf.sprintf "(%s)" (print_to_string print_constr trm)
-  | Fix ((is, i), (ns, ts, ds)) -> (* TODO *)
-     Printf.sprintf "(%s)" (print_to_string print_constr trm)
+  | Case (ci, ct, m, bs) ->
+     let (i, i_index) = ci.ci_ind in
+     let mutind_body = lookup_mind i env in
+     let ind_body = mutind_body.mind_packets.(i_index) in
+     Printf.sprintf
+       "(match %s : %s with %s)"
+       (term_as_string env m)
+       (term_as_string env ct)
+       (String.concat
+          " "
+          (Array.to_list
+             (Array.mapi
+                (fun c_i b ->
+                  Printf.sprintf
+                    "(case %s => %s)"
+                    (string_of_id (ind_body.mind_consnames.(c_i)))
+                    (term_as_string env b))
+                bs)))
+  | Fix ((is, i), (ns, ts, ds)) ->
+     let env_fix = push_rel_context (bindings_for_fix ns ds) env in
+     String.concat
+       " with "
+       (map3
+          (fun n t d ->
+            Printf.sprintf
+             "(Fix %s : %s := %s)"
+             (name_as_string n)
+             (term_as_string env t)
+             (term_as_string env_fix d))
+          (Array.to_list ns)
+          (Array.to_list ts)
+          (Array.to_list ds))
   | CoFix (i, (ns, ts, ds)) ->
      Printf.sprintf "TODO" (* TODO *)
   | Proj (p, c) ->

plugin/src/library/utilities/collections.ml

@@ -121,6 +121,14 @@ let flat_map (f : 'a -> 'b list) (l : 'a list) : 'b list =
 let flat_map2 (f : 'a -> 'b -> 'c list) (la : 'a list) (lb : 'b list) : 'c list =
   List.flatten (List.map2 f la lb)
 
+(* Map3 *)
+let rec map3 (f : 'a -> 'b -> 'c -> 'd) l1 l2 l3 : 'd list =
+  match (l1, l2, l3) with
+  | ([], [], []) ->
+     []
+  | (h1 :: t1, h2 :: t2, h3 :: t3) ->
+     let r = f h1 h2 h3 in r :: map3 f t1 t2 t3
+
 (*
  * Get the head of a transformation on a list,
  * defaulting to default if the original list is empty, or if the

plugin/src/library/utilities/collections.mli

@@ -83,6 +83,11 @@ val flat_map : ('a -> 'b list) -> 'a list -> 'b list
  *)
 val flat_map2 : ('a -> 'b -> 'c list) -> 'a list -> 'b list -> 'c list
 
+(*
+ * Map3
+ *)
+val map3 : ('a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list
+
 (*
  * Get the head of a transformation on a list,
  * defaulting to default if the list is empty