]> matita.cs.unibo.it Git - helm.git/commitdiff
DOOMSDAY 1.0:
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 31 May 2007 15:06:22 +0000 (15:06 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 31 May 2007 15:06:22 +0000 (15:06 +0000)
 this is the commit that (partially) allows Matita to understand its own
 output. I.e. the natural language generated is now the declarative language.
 This is probably still highly bugged in most cases.

components/content_pres/content2pres.ml

index a8b0bc6a039e78425fe942ce6464770ddbabba1e..e377706b7ddb69b49650306eb5a71180b0d9d6e6 100644 (file)
@@ -100,10 +100,10 @@ let make_args_for_apply term2pres args =
     | Con.Term t -> 
         if is_first then
           (term2pres t)::row
-        else (B.b_object (P.Mi([],"_")))::row
+        else (B.b_object (P.Mi([],"?")))::row
     | Con.ArgProof _ 
     | Con.ArgMethod _ -> 
-       (B.b_object (P.Mi([],"_")))::row
+       (B.b_object (P.Mi([],"?")))::row
   in
    if is_first then res else B.skip::res
  in
@@ -132,10 +132,10 @@ let rec justification term2pres p =
       (B.b_kw "by")::B.b_space::
       B.Text([],"(")::pres_args@[B.Text([],")")]), None 
   else (B.b_kw "by"),
-    Some (B.b_toggle [B.b_kw "proof";proof2pres term2pres p])
+    Some (B.b_toggle [B.b_kw "proof";proof2pres true term2pres p])
      
-and proof2pres term2pres p =
-  let rec proof2pres p =
+and proof2pres is_top_down term2pres p =
+  let rec proof2pres is_top_down p omit_dot =
     let indent = 
       let is_decl e = 
         (match e with 
@@ -150,10 +150,16 @@ and proof2pres term2pres p =
        | Some t -> Some (term2pres t)) in
     let body =
         let presconclude = 
-          conclude2pres p.Con.proof_conclude indent omit_conclusion in
+          conclude2pres is_top_down p.Con.proof_conclude indent omit_conclusion
+           omit_dot in
         let presacontext = 
-          acontext2pres p.Con.proof_apply_context presconclude indent in
-        context2pres p.Con.proof_context presacontext in
+          acontext2pres
+           (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion")
+           p.Con.proof_apply_context presconclude indent
+           (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion")
+        in
+         context2pres p.Con.proof_context presacontext
+  in
     match p.Con.proof_name with
       None -> body
     | Some name ->
@@ -166,9 +172,7 @@ and proof2pres term2pres p =
                  "proof of" ac in
              B.b_toggle [ concl; body ]
         in
-        B.V ([],
-          [B.Text ([],"(" ^ name ^ ")");
-           B.indent action])
+         B.indent action
 
   and context2pres c continuation =
     (* we generate a subtable for each context element, for selection
@@ -202,82 +206,93 @@ and proof2pres term2pres p =
   and ce2pres_in_proof_context_element = function 
     | `Joint ho -> 
       B.H ([],(List.map ce2pres_in_joint_context_element ho.Content.joint_defs))
-    | (`Declaration _) as x -> ce2pres x
-    | (`Hypothesis _) as x  -> ce2pres x
+    | (`Declaration _) as x -> ce2pres x 
+    | (`Hypothesis _) as x  -> ce2pres x 
     | (`Proof _) as x       -> ce2pres x
-    | (`Definition _) as x  -> ce2pres x
+    | (`Definition _) as x  -> ce2pres x 
   
-  and ce2pres = 
+  and ce2pres =
     function 
         `Declaration d -> 
          let ty = term2pres d.Con.dec_type in
          B.H ([],
-           [(B.b_kw "Assume");
+           [(B.b_kw "assume");
             B.b_space;
             B.Object ([], P.Mi([],get_name d.Con.dec_name));
             B.Text([],":");
-            ty])
+            ty;
+            B.Text([],".")])
       | `Hypothesis h ->
           let ty = term2pres h.Con.dec_type in
           B.H ([],
-            [(B.b_kw "Suppose");
+            [(B.b_kw "suppose");
+             B.b_space;
+             ty;
              B.b_space;
              B.Text([],"(");
              B.Object ([], P.Mi ([],get_name h.Con.dec_name));
              B.Text([],")");
-             B.b_space;
-             ty])
+             B.Text([],".")])
       | `Proof p -> 
-           proof2pres 
+           proof2pres false p false
       | `Definition d -> 
           let term = term2pres d.Con.def_term in
           B.H ([],
-            [ B.b_kw "Let"; B.b_space;
+            [ B.b_kw "let"; B.b_space;
               B.Object ([], P.Mi([],get_name d.Con.def_name));
-              B.Text([]," = ");
+              B.Text([],Utf8Macro.unicode_of_tex "\\def");
               term])
 
-  and acontext2pres ac continuation indent =
+  and acontext2pres is_top_down ac continuation indent in_bu_conversion =
     List.fold_right
       (fun p continuation ->
-         let hd = 
-           if indent then
-             B.indent (proof2pres p)
-           else 
-             proof2pres p in
+        let hd = 
+          if indent then
+            B.indent (proof2pres is_top_down p in_bu_conversion)
+          else 
+            proof2pres is_top_down p in_bu_conversion
+        in
          B.V([Some "helm","xref",p.Con.proof_id],
            [B.H([Some "helm","xref","ace_"^p.Con.proof_id],[hd]);
             continuation])) ac continuation 
 
-  and conclude2pres conclude indent omit_conclusion =
+  and conclude2pres is_top_down conclude indent omit_conclusion omit_dot =
     let tconclude_body = 
       match conclude.Con.conclude_conclusion with
-        Some t when
-         not omit_conclusion or
+        Some t (*when not omit_conclusion or
          (* CSC: I ignore the omit_conclusion flag in this case.   *)
          (* CSC: Is this the correct behaviour? In the stylesheets *)
          (* CSC: we simply generated nothing (i.e. the output type *)
          (* CSC: of the function should become an option.          *)
-         conclude.Con.conclude_method = "BU_Conversion" ->
-          let concl = (term2pres t) in 
+         conclude.Con.conclude_method = "BU_Conversion" *) ->
+          let concl = term2pres t in 
           if conclude.Con.conclude_method = "BU_Conversion" then
-            make_concl "that is equivalent to" concl
+            B.b_hv []
+             (make_concl "that is equivalent to" concl ::
+              if is_top_down then [B.b_space ; B.Text([],"done.")] else [])
           else if conclude.Con.conclude_method = "FalseInd" then
            (* false ind is in charge to add the conclusion *)
            falseind conclude
           else  
             let conclude_body = conclude_aux conclude in
             let ann_concl = 
-              if conclude.Con.conclude_method = "TD_Conversion" then
-                 make_concl "that is equivalent to" concl 
-              else make_concl "we conclude" concl in
-            B.V ([], [conclude_body; ann_concl])
-      | _ -> conclude_aux conclude in
-    if indent then 
-      B.indent (B.H ([Some "helm", "xref", conclude.Con.conclude_id],
-                    [tconclude_body]))
-    else 
-      B.H ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body])
+              if  conclude.Con.conclude_method = "Intros+LetTac"
+               || conclude.Con.conclude_method = "ByInduction"
+               || conclude.Con.conclude_method = "TD_Conversion"
+              then
+               B.Text([],"")
+              else if omit_conclusion then B.Text([],"done.")
+              else B.b_hv []
+               ((if not is_top_down || omit_dot then [make_concl "we proved" concl; B.Text([],if not is_top_down then "(previous)" else "")] else [B.Text([],"done")]) @ if not omit_dot then [B.Text([],".")] else [])
+            in
+             B.V ([], [conclude_body; ann_concl])
+      | _ -> conclude_aux conclude
+    in
+     if indent then 
+       B.indent (B.H ([Some "helm", "xref", conclude.Con.conclude_id],
+                     [tconclude_body]))
+     else 
+       B.H ([Some "helm", "xref", conclude.Con.conclude_id],[tconclude_body])
 
   and conclude_aux conclude =
     if conclude.Con.conclude_method = "TD_Conversion" then
@@ -295,9 +310,10 @@ and proof2pres term2pres p =
          | Some c -> (term2pres c)) in
       B.V 
         ([],
-        [make_concl "we must prove" expected;
+        [make_concl "we need to  prove" expected;
          make_concl "or equivalently" synth;
-         proof2pres subproof])
+         B.Text([],".");
+         proof2pres true subproof false])
     else if conclude.Con.conclude_method = "BU_Conversion" then
       assert false
     else if conclude.Con.conclude_method = "Exact" then
@@ -311,15 +327,13 @@ and proof2pres term2pres p =
          | err -> assert false) in
       (match conclude.Con.conclude_conclusion with 
          None ->
-          B.b_h [] [B.b_kw "Consider"; B.b_space; arg]
+          B.b_h [] [B.b_kw "by"; B.b_space; arg]
        | Some c -> let conclusion = term2pres c in
-          make_row 
-            [arg; B.b_space; B.b_kw "proves"]
-            conclusion
+          B.b_h [] [B.b_kw "by"; B.b_space; arg]
        )
     else if conclude.Con.conclude_method = "Intros+LetTac" then
       (match conclude.Con.conclude_args with
-         [Con.ArgProof p] -> proof2pres p
+         [Con.ArgProof p] -> proof2pres true p false
        | _ -> assert false)
 (* OLD CODE 
       let conclusion = 
@@ -331,7 +345,7 @@ and proof2pres term2pres p =
            B.V 
             ([None,"align","baseline 1"; None,"equalrows","false";
               None,"columnalign","left"],
-              [B.H([],[B.Object([],proof2pres p)]);
+              [B.H([],[B.Object([],proof2pres p false)]);
                B.H([],[B.Object([],
                 (make_concl "we proved 1" conclusion))])]);
        | _ -> assert false)
@@ -359,6 +373,7 @@ and proof2pres term2pres p =
         (match List.nth conclude.Con.conclude_args 5 with
            Con.Term t -> term2pres t
          | _ -> assert false) in
+(*
       B.V ([], 
          B.H ([],[
           (B.b_kw "rewrite");
@@ -367,6 +382,7 @@ and proof2pres term2pres p =
           B.b_space; term2;
           B.b_space; justif1])::
            match justif2 with None -> [] | Some j -> [B.indent j])
+*) B.V([], [justif1 ; B.H([],[B.b_kw "we proved (" ; term2 ; B.b_kw "=" ; term1; B.b_kw ") (previous)."]); B.b_kw "by _"])
     else if conclude.Con.conclude_method = "Eq_chain" then
       let justification p =
        let j1,j2 = justification term2pres p in
@@ -406,7 +422,7 @@ and proof2pres term2pres p =
       | Con.Premise prem -> B.b_kw "premise"
       | Con.Lemma lemma -> B.b_kw "lemma"
       | Con.Term t -> term2pres t
-      | Con.ArgProof p -> proof2pres 
+      | Con.ArgProof p -> proof2pres true p false
       | Con.ArgMethod s -> B.b_kw "method"
  
    and case conclude =
@@ -466,7 +482,7 @@ and proof2pres term2pres p =
         (make_concl "we proceed by induction on" arg) in
      let to_prove =
         (make_concl "to prove" proof_conclusion) in
-     B.V ([], induction_on::to_prove:: (make_cases args_for_cases))
+     B.V ([], induction_on::to_prove:: B.Text([],".")::(make_cases args_for_cases))
 
     and make_cases l = List.map make_case l
 
@@ -491,16 +507,18 @@ and proof2pres term2pres p =
                      | `Hypothesis h -> 
                          let name = get_name h.Con.dec_name in
                          [B.b_space;
+                          B.Text([],"(");
                           B.Object ([], P.Mi ([],name));
                           B.Text([],":");
-                          (term2pres h.Con.dec_type)]
-                     | _ -> [B.Text ([],"???")]) in
+                          (term2pres h.Con.dec_type);
+                          B.Text([],")")]
+                     | _ -> assert false (*[B.Text ([],"???")]*)) in
                   dec@p) args [] in
           let pattern = 
             B.H ([],
-               (B.b_kw "Case"::B.b_space::name::pattern_aux)@
+               (B.b_kw "case"::B.b_space::name::pattern_aux)@
                 [B.b_space;
-                 B.Text([], Utf8Macro.unicode_of_tex "\\Rightarrow")]) in
+                 B.Text([], ".")]) in
           let subconcl = 
             (match p.Con.proof_conclude.Con.conclude_conclusion with
                None -> B.b_kw "No conclusion!!!"
@@ -516,20 +534,22 @@ and proof2pres term2pres p =
                    `Hypothesis h ->
                      let name = 
                        (match h.Con.dec_name with
-                          None -> "no name"
+                          None -> "useless"
                         | Some s -> s) in
                      B.indent (B.H ([],
-                       [B.Text([],"(");
+                       [term2pres h.Con.dec_type;
+                        B.b_space;
+                        B.Text([],"(");
                         B.Object ([], P.Mi ([],name));
                         B.Text([],")");
-                        B.b_space;
-                        term2pres h.Con.dec_type]))
+                        B.Text([],".")]))
                    | _ -> assert false in
                let hyps = List.map make_hyp indhyps in
                text::hyps) in          
           (* let acontext = 
                acontext2pres_old p.Con.proof_apply_context true in *)
-          let body = conclude2pres p.Con.proof_conclude true false in
+          let body =
+           conclude2pres true p.Con.proof_conclude true true false in
           let presacontext = 
            let acontext_id =
             match p.Con.proof_apply_context with
@@ -538,8 +558,12 @@ and proof2pres term2pres p =
            in
             B.Action([None,"type","toggle"],
               [ B.indent (add_xref acontext_id (B.b_kw "Proof"));
-                acontext2pres p.Con.proof_apply_context body true]) in
-          B.V ([], pattern::asubconcl::induction_hypothesis@[presacontext])
+                acontext2pres
+                 (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion")
+                 p.Con.proof_apply_context body true
+                 (p.Con.proof_conclude.Con.conclude_method = "BU_Conversion")
+              ]) in
+          B.V ([], pattern::induction_hypothesis@[asubconcl;B.Text([],".");presacontext])
        | _ -> assert false 
 
      and falseind conclude =
@@ -567,7 +591,7 @@ and proof2pres term2pres p =
                [ B.Object ([], P.Mi([],lemma.Con.lemma_name)); B.skip;
                  B.b_kw "is contradictory, hence" ]
            | _ -> assert false) in
-            (* let body = proof2pres {proof with Con.proof_context = tl} in *)
+            (* let body = proof2pres {proof with Con.proof_context = tl} false in *)
        make_row arg proof_conclusion
 
      and andind conclude =
@@ -605,10 +629,11 @@ and proof2pres term2pres p =
                 B.Text([],")");
                 B.skip;
                 term2pres hyp2.Con.dec_type]) in
-            (* let body = proof2pres {proof with Con.proof_context = tl} in *)
-            let body = conclude2pres proof.Con.proof_conclude false true in
+            (* let body = proof2pres {proof with Con.proof_context = tl} false in *)
+            let body= conclude2pres false proof.Con.proof_conclude false true false in
             let presacontext = 
-              acontext2pres proof.Con.proof_apply_context body false in
+              acontext2pres false proof.Con.proof_apply_context body false false
+            in
             B.V 
               ([],
                [B.H ([],arg@[B.skip; B.b_kw "we have"]);
@@ -644,10 +669,11 @@ and proof2pres term2pres p =
                 B.Text([],")");
                 B.skip;
                 term2pres hyp.Con.dec_type]) in
-            (* let body = proof2pres {proof with Con.proof_context = tl} in *)
-            let body = conclude2pres proof.Con.proof_conclude false true in
+            (* let body = proof2pres {proof with Con.proof_context = tl} false in *)
+            let body= conclude2pres false proof.Con.proof_conclude false true false in
             let presacontext = 
-              acontext2pres proof.Con.proof_apply_context body false in
+              acontext2pres false proof.Con.proof_apply_context body false false
+            in
             B.V 
               ([],
                [presdecl;
@@ -656,7 +682,7 @@ and proof2pres term2pres p =
          | _ -> assert false
 
     in
-    proof2pres p
+    proof2pres is_top_down p false
 
 exception ToDo
 
@@ -707,7 +733,7 @@ let conjecture2pres term2pres (id, n, context, ty) =
                                          None -> "_"
                                        | Some n -> n)) ;
                        B.b_text [] (Utf8Macro.unicode_of_tex "\\Assign");
-                       proof2pres term2pres p])
+                       proof2pres true term2pres p])
           (List.rev context)) ] ::
          [ B.b_h []
            [ B.b_text [] (Utf8Macro.unicode_of_tex "\\vdash");
@@ -778,20 +804,21 @@ let content2pres term2pres (id,params,metasenv,obj) =
       let name = get_name p.Content.proof_name in
       B.b_v
         [Some "helm","xref","id"]
-        ([ B.b_h [] (B.b_kw ("Proof " ^ name) :: params2pres params);
-           B.b_kw "Thesis:";
-           B.indent (term2pres thesis) ] @
+        ([ B.b_h [] (B.b_kw ("theorem " ^ name) :: params2pres params @ [B.b_kw ":"]);
+           B.indent (term2pres thesis) ; B.b_kw "." ] @
          metasenv2pres term2pres metasenv @
-         [proof2pres term2pres p])
+         [proof2pres true term2pres p ; B.b_kw "qed."])
   | `Def (_, ty, `Definition body) ->
       let name = get_name body.Content.def_name in
       B.b_v
         [Some "helm","xref","id"]
-        ([B.b_h [] (B.b_kw ("Definition " ^ name) :: params2pres params);
-          B.b_kw "Type:";
+        ([B.b_h []
+           (B.b_kw ("definition " ^ name) :: params2pres params @ [B.b_kw ":"]);
           B.indent (term2pres ty)] @
           metasenv2pres term2pres metasenv @
-          [B.b_kw "Body:"; term2pres body.Content.def_term])
+          [B.b_kw ":=";
+           B.indent (term2pres body.Content.def_term);
+           B.b_kw "."])
   | `Decl (_, `Declaration decl)
   | `Decl (_, `Hypothesis decl) ->
       let name = get_name decl.Content.dec_name in
@@ -809,11 +836,10 @@ let content2pres term2pres (id,params,metasenv,obj) =
 
 let content2pres ~ids_to_inner_sorts =
   content2pres
-    (fun annterm ->
+    (fun ?(prec=90) annterm ->
       let ast, ids_to_uris =
         TermAcicContent.ast_of_acic ids_to_inner_sorts annterm
       in
-      CicNotationPres.box_of_mpres
-        (CicNotationPres.render ids_to_uris
+       CicNotationPres.box_of_mpres
+        (CicNotationPres.render ids_to_uris ~prec
           (TermContentPres.pp_ast ast)))
-