Improve a bit the display of Coq scripts.

src/printer/coq.ml

@@ -215,7 +215,7 @@ let rec print_pat info fmt p = match p.pat_node with
       end
 
 let print_vsty_nopar info fmt v =
-  fprintf fmt "%a:%a" print_vs v (print_ty info) v.vs_ty
+  fprintf fmt "@[<hov>%a:@,%a@]" print_vs v (print_ty info) v.vs_ty
 
 let print_vsty info fmt v =
   fprintf fmt "(%a)" (print_vsty_nopar info) v
@@ -287,9 +287,9 @@ and print_tnode _opl opr info fmt t = match t.t_node with
         print_vs v (print_term info) t1 (print_opl_term info) t2;
       forget_var v
   | Tcase (t,bl) ->
-      fprintf fmt "@[<hov>match %a with@\n@[<hov>%a@]@\nend@]"
+      fprintf fmt "@[<v>match %a with@,%a@,end@]"
         (print_term info) t
-        (print_list newline (print_tbranch info)) bl
+        (print_list pp_print_cut (print_tbranch info)) bl
   | Teps fb ->
       let vl,_,t0 = t_open_lambda t in
       if vl = [] then begin
@@ -318,7 +318,7 @@ and print_tnode _opl opr info fmt t = match t.t_node with
       | _ -> if unambig_fs fs
           then
             if tl = [] then fprintf fmt "%a" (print_ls_real info) fs
-            else fprintf fmt "@[<hov>(@[<hov 1>%a %a@])@]"
+            else fprintf fmt "@[<hov 1>(%a@ %a)@]"
               (print_ls_real info) fs
               (print_list space (print_opr_term info)) tl
           else fprintf fmt "@[<hov>(%a %a: %a)@]"
@@ -330,7 +330,7 @@ and print_tnode _opl opr info fmt t = match t.t_node with
 and print_fnode opl opr info fmt f = match f.t_node with
   | Tquant (Tforall,fq) ->
       let vl,_tl,f = t_open_quant fq in
-      fprintf fmt (protect_on opr "@[<hov 1>forall @[<hov>%a@],@ @[<hov>%a@]@]")
+      fprintf fmt (protect_on opr "@[<hov>forall @[<hov>%a@],@ @[<hov>%a@]@]")
         (print_list space (print_vsty info)) vl
         (* (print_tl info) tl *) (print_fmla info) f;
       List.iter forget_var vl
@@ -340,8 +340,7 @@ and print_fnode opl opr info fmt f = match f.t_node with
         match vl with
           | [] -> print_fmla info fmt f
           | v::vr ->
-              fprintf fmt (protect_on opr
-                              "@[<hov 1>exists @[<hov>%a@],@ @[<hov>%a@]@]")
+              fprintf fmt (protect_on opr "@[<hov>exists @[<hov>%a@],@ @[<hov>%a@]@]")
                 (print_vsty_nopar info) v
                 aux vr
       in
@@ -354,7 +353,7 @@ and print_fnode opl opr info fmt f = match f.t_node with
   | Tbinop (b,f1,f2) ->
      (match b with
      | Tand | Tor ->
-       fprintf fmt (protect_on (opl || opr) "@[<hov>%a@ %a %a@]")
+       fprintf fmt (protect_on (opl || opr) "@[<hov>%a %a@ %a@]")
                (print_opr_fmla info) f1 print_binop b (print_opl_fmla info) f2
      | Timplies | Tiff ->
          fprintf fmt (protect_on (opl || opr) "@[<hov>%a %a@ %a@]")
@@ -363,7 +362,7 @@ and print_fnode opl opr info fmt f = match f.t_node with
       fprintf fmt (protect_on opr "@[<hov>~ %a@]") (print_opl_fmla info) f
   | Tlet (t,f) ->
       let v,f = t_open_bound f in
-      fprintf fmt (protect_on opr "@[<hov>let %a :=@[<hov 1>@ %a@] in@ %a@]")
+      fprintf fmt (protect_on opr "@[<hov>let %a :=@ @[<hov>%a@] in@ %a@]")
         print_vs v (print_term info) t (print_opl_fmla info) f;
       forget_var v
   | Tcase (t,bl) ->
@@ -372,7 +371,7 @@ and print_fnode opl opr info fmt f = match f.t_node with
         (print_list newline (print_fbranch info)) bl
   | Tif (f1,f2,f3) ->
       fprintf fmt (protect_on opr
-        "@[<hov>if @[<hov 1>%a@]@ then@[@ <hov 1>%a@]@ else@[@ <hov 1>%a@]@]")
+        "@[<hov>if @[<hov>%a@] then@ [@<hov>%a@]@ else@ [@<hov>%a@]@]")
         (print_fmla info) f1 (print_fmla info) f2 (print_opl_fmla info) f3
   | Tapp (ps, tl) ->
     begin match query_syntax info.info_syn ps.ls_name with
@@ -694,19 +693,19 @@ let print_type_decl ~prev info fmt ts =
         | Some (Query (_,Notation,c)) ->
           fprintf fmt "(* Why3 goal *)@\n%s@\n" c
         | Some (Axiom _) ->
-          fprintf fmt "(* Why3 goal *)@\n@[<hov 2>Variable %a : %aType.@]@\n@[<hov 2>Hypothesis %a_WhyType : %aWhyType %a.@]@\nExisting Instance %a_WhyType.@\n@\n"
+          fprintf fmt "(* Why3 goal *)@\n@[<hv 2>Variable %a :@ @[<hov>%aType.@]@]@\n@[<hv 2>Hypothesis %a_WhyType :@ @[<hov>%aWhyType %a.@]@]@\nExisting Instance %a_WhyType.@\n@\n"
             print_ts ts (print_params_list info ~whytypes:false) ts.ts_args
             print_ts ts (print_params_list info ~whytypes:true)
               ts.ts_args (print_ts_tv info) ts print_ts ts
         | _ ->
-          fprintf fmt "(* Why3 goal *)@\n@[<hov 2>Definition %a : %aType.@]@\n%a@\n"
+          fprintf fmt "(* Why3 goal *)@\n@[<hv 2>Definition %a :@ @[<hov>%aType.@]@]@\n%a@\n"
             print_ts ts (print_params_list info ~whytypes:false) ts.ts_args
             (print_previous_proof None info) prev
       else begin
-        fprintf fmt "@[<hov 2>Axiom %a : %aType.@]@\n"
+        fprintf fmt "@[<hv 2>Axiom %a :@ @[<hov>%aType.@]@]@\n"
           print_ts ts (print_params_list info ~whytypes:false) ts.ts_args;
         if not info.ssreflect then begin
-          fprintf fmt "@[<hov 2>Parameter %a_WhyType : %aWhyType %a.@]@\n"
+          fprintf fmt "@[<hv 2>Parameter %a_WhyType :@ @[<hov>%aWhyType %a.@]@]@\n"
             print_ts ts (print_params_list info ~whytypes:true) ts.ts_args
             (print_ts_tv info) ts;
           fprintf fmt "Existing Instance %a_WhyType.@\n"
@@ -796,13 +795,13 @@ let print_param_decl ~prev info fmt ls =
         (print_expr info) e;
       List.iter forget_var vl
     | _ ->
-      fprintf fmt "(* Why3 goal *)@\n@[<hov 2>Definition %a: %a%a%a.@]@\n%a@\n"
+      fprintf fmt "(* Why3 goal *)@\n@[<hv 2>Definition %a :@ @[<hov>%a%a%a.@]@]@\n%a@\n"
         print_ls ls (print_params info ~whytypes:true) all_ty_params
         (print_arrow_list (print_ty info)) ls.ls_args
         (print_ls_type info) ls.ls_value
         (print_previous_proof None info) prev
   else
-    fprintf fmt "@[<hov 2>Parameter %a: %a%a%a.@]@\n@\n"
+    fprintf fmt "@[<hv 2>Parameter %a:@ @<hov>%a%a%a.@]@]@\n@\n"
       print_ls ls (print_params info ~whytypes:true) all_ty_params
       (print_arrow_list (print_ty info)) ls.ls_args
       (print_ls_type info) ls.ls_value
@@ -814,7 +813,7 @@ let print_param_decl ~prev info fmt ls =
 let print_logic_decl info fmt (ls,ld) =
   let _, _, all_ty_params = ls_ty_vars ls in
   let vl,e = open_ls_defn ld in
-  fprintf fmt "(* Why3 assumption *)@\n@[<hov 2>Definition %a%a%a: %a :=@ %a.@]@\n"
+  fprintf fmt "(* Why3 assumption *)@\n@[<hv 2>Definition @[<hov>%a%a%a :@ %a@] :=@ @[<hov>%a.@]@]@\n"
     print_ls ls
     (print_tv_binders info ~whytypes:true ~implicit:true) all_ty_params
     (print_list_pre space (print_vsty info)) vl
@@ -827,7 +826,7 @@ let print_equivalence_lemma ~prev info fmt name (ls,ld) =
   let _, _, all_ty_params = ls_ty_vars ls in
   let def_formula = ls_defn_axiom ld in
   fprintf fmt
-    "(* Why3 goal *)@\n@[<hov 2>Lemma %s :@ %a%a.@]@\n"
+    "(* Why3 goal *)@\n@[<hv 2>Lemma %s :@ @[<hov>%a%a.@]@]@\n"
     name
     (print_params info ~whytypes:true) all_ty_params
     (print_expr info) def_formula;
@@ -918,16 +917,16 @@ let print_prop_decl ~prev info fmt (k,pr,f) =
   if stt <> "" then
     match prev with
     | Some (Axiom _) when stt = "Lemma" ->
-      fprintf fmt "(* Why3 goal *)@\n@[<hov 2>Hypothesis %a :@.%a%a.@]@\n@\n"
+      fprintf fmt "(* Why3 goal *)@\n@[<hv 2>Hypothesis %a :@ @[<hov>%a%a.@]@]@\n@\n"
         print_pr pr (print_params info ~whytypes:true) params
         (print_fmla info) f
     | _ ->
-      fprintf fmt "(* Why3 goal *)@\n@[<hov 2>%s %a :@.%a%a.@]@\n%a@\n"
+      fprintf fmt "(* Why3 goal *)@\n@[<hv 2>%s %a :@ @[<hov>%a%a.@]@]@\n%a@\n"
         stt print_pr pr (print_params info ~whytypes:true) params
         (print_fmla info) f
         (print_previous_proof (Some (params,f)) info) prev
   else
-    fprintf fmt "@[<hov 2>Axiom %a :@.%a%a.@]@\n@\n"
+    fprintf fmt "@[<hv 2>Axiom %a :@ @[%a%a.@]@]@\n@\n"
       print_pr pr (print_params info ~whytypes:true) params
       (print_fmla info) f;
   forget_tvs ()