Huge commit with several changes:

[helm.git] / helm / software / components / content_pres / content2pres.ml

diff --git a/helm/software/components/content_pres/content2pres.ml b/helm/software/components/content_pres/content2pres.ml
index a99278dbcf137de171eff09cb3f5339fde9b8ab7..46f53d8860c85a00ac600373c36e63b5f74dbfa9 100644 (file)
--- a/helm/software/components/content_pres/content2pres.ml
+++ b/helm/software/components/content_pres/content2pres.ml
@@ -121,7 +121,7 @@ let add_xref id = function
   | B.Text (attrs, t) -> B.Text (((Some "helm", "xref", id) :: attrs), t)
   | _ -> assert false (* TODO, add_xref is meaningful for all boxes *)
 
-let rec justification ~ignore_atoms term2pres p = 
+let rec justification ~for_rewriting_step ~ignore_atoms term2pres p = 
   if p.Con.proof_conclude.Con.conclude_method = "Exact" &&
      ignore_atoms
   then
@@ -136,10 +136,16 @@ let rec justification ~ignore_atoms term2pres p =
       make_args_for_apply term2pres p.Con.proof_conclude.Con.conclude_args
     in
      [B.H([],
-       (B.b_kw "by")::B.b_space::
+       (if for_rewriting_step then (B.b_kw "exact") else (B.b_kw "by"))::
+       B.b_space::
        B.Text([],"(")::pres_args@[B.Text([],")")])], None 
   else
-   [B.H([],[B.b_kw "by"; B.b_space; B.b_kw "proof"])],
+   [B.H([],
+    if for_rewriting_step then
+     [B.b_kw "proof"]
+    else
+     [B.b_kw "by"; B.b_space; B.b_kw "proof"]
+    )],
     Some (B.b_toggle [B.b_kw "proof";B.indent (proof2pres true term2pres p)])
      
 and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
@@ -181,7 +187,9 @@ and proof2pres ?skip_initial_lambdas is_top_down term2pres p =
            | _ -> p.Con.proof_context)
           presacontext
     in
+(*
 let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ (if is_top_down then "(TD)" else "(NTD)") ^ "*)"); body; B.b_kw "(*>>*)"]) in
+*)
     match p.Con.proof_name with
       None -> body
     | Some name ->
@@ -439,7 +447,9 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ (
          || conclude.Con.conclude_method = "RewriteRL" then
       let justif1,justif2 = 
         (match (List.nth conclude.Con.conclude_args 6) with
-           Con.ArgProof p -> justification ~ignore_atoms:true term2pres p
+           Con.ArgProof p ->
+            justification ~for_rewriting_step:true ~ignore_atoms:true
+             term2pres p
          | _ -> assert false) in
       let justif =
        match justif2 with
@@ -447,9 +457,7 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ (
         | Some j -> [j]
       in
       let index_term1, index_term2 =
-       if  (conclude.Con.conclude_method = "RewriteLR" && is_top_down)
-        || (conclude.Con.conclude_method = "RewriteRL" && not is_top_down)
-       then 2,5 else 5,2
+       if conclude.Con.conclude_method = "RewriteLR" then 2,5 else 5,2
       in
       let term1 = 
         (match List.nth conclude.Con.conclude_args index_term1 with
@@ -483,7 +491,9 @@ let body = B.V([],[B.b_kw ("(*<<" ^ p.Con.proof_conclude.Con.conclude_method ^ (
       B.V([], justif @ [B.b_kw "by _"])
     else if conclude.Con.conclude_method = "Eq_chain" then
       let justification p =
-       let j1,j2 = justification ~ignore_atoms:false term2pres p in
+       let j1,j2 =
+        justification ~for_rewriting_step:true ~ignore_atoms:false term2pres p
+       in
         j1, match j2 with Some j -> [j] | None -> []
       in
       let rec aux args =
@@ -805,7 +815,9 @@ let conjecture2pres term2pres (id, n, context, ty) =
   (B.b_hv [Some "helm", "xref", id]
      ((B.b_toggle [
         B.b_h [] [B.b_text [] "{...}"; B.b_space];
-        B.b_hv [] (List.map
+        B.b_hv [] (HExtlib.list_concat ~sep:[B.b_text [] ";"; B.b_space] 
+         (List.map (fun x -> [x])
+         (List.map
           (function
              | None ->
                 B.b_h []
@@ -823,7 +835,7 @@ let conjecture2pres term2pres (id, n, context, ty) =
                            (match dec_name with
                                 None -> "_"
                               | Some n -> n));
-                       B.b_text [] ":";
+                       B.b_text [] ":"; B.b_space; 
                        term2pres ty ]
              | Some (`Definition d) ->
                  let
@@ -836,6 +848,7 @@ let conjecture2pres term2pres (id, n, context, ty) =
                                          None -> "_"
                                        | Some n -> n)) ;
                        B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign");
+                       B.b_space;
                        term2pres bo]
              | Some (`Proof p) ->
                  let proof_name = p.Content.proof_name in
@@ -845,12 +858,16 @@ let conjecture2pres term2pres (id, n, context, ty) =
                                          None -> "_"
                                        | Some n -> n)) ;
                        B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign");
+                       B.b_space;
                        proof2pres true term2pres p])
-          (List.rev context)) ] ::
+          (List.rev context)))) ] ::
          [ B.b_h []
-           [ B.b_text [] (Utf8Macro.unicode_of_tex "\\vdash");
+           [ B.b_space; 
+             B.b_text [] (Utf8Macro.unicode_of_tex "\\vdash");
+             B.b_space;
              B.b_object (p_mi [] (string_of_int n)) ;
              B.b_text [] ":" ;
+             B.b_space;
              term2pres ty ]])))
 
 let metasenv2pres term2pres = function
@@ -885,8 +902,10 @@ let recursion_kind2pres params kind =
     match kind with
     | `Recursive _ -> "Recursive definition"
     | `CoRecursive -> "CoRecursive definition"
-    | `Inductive _ -> "Inductive definition"
-    | `CoInductive _ -> "CoInductive definition"
+    | `Inductive i -> 
+        "Inductive definition with "^string_of_int i^" fixed parameter(s)"
+    | `CoInductive i -> 
+        "Co-Inductive definition with "^string_of_int i^" fixed parameter(s)"
   in
   B.b_h [] (B.b_kw kind :: params2pres params)
 
@@ -960,8 +979,9 @@ let content2pres
   content2pres ?skip_initial_lambdas ?skip_thm_and_qed
     (fun ?(prec=90) annterm ->
       let ast, ids_to_uris =
-        TermAcicContent.ast_of_acic ids_to_inner_sorts annterm
+       TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm
       in
        CicNotationPres.box_of_mpres
-        (CicNotationPres.render ids_to_uris ~prec
+        (CicNotationPres.render
+          ~lookup_uri:(CicNotationPres.lookup_uri ids_to_uris) ~prec
           (TermContentPres.pp_ast ast)))