version 0.7.1

[helm.git] / helm / ocaml / cic_transformations / content2pres.ml

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index 29da14591e9fd6946f1e0062412ece9457985288..1429826479f0cd5f87f6f715ca931eeab8e09aa9 100644 (file)
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -186,6 +186,10 @@ let make_args_for_apply term2pres args =
   | _ -> assert false
 ;;
 
+let get_name = function
+  | Some s -> s
+  | None -> "_"
+
 let rec justification term2pres p = 
   let module Con = Content in
   let module P = Mpresentation in
@@ -250,17 +254,33 @@ and proof2pres term2pres p =
             (fun ce continuation ->
               let xref = get_xref ce in
               B.V([Some "helm", "xref", xref ],
-                [B.H([Some "helm", "xref", "ce_"^xref],[ce2pres ce]);
+                [B.H([Some "helm", "xref", "ce_"^xref],
+                     [ce2pres_in_proof_context_element ce]);
                  continuation])) tl continuation in
          let hd_xref= get_xref hd in
          B.V([],
              [B.H([Some "helm", "xref", "ce_"^hd_xref],
-               [ce2pres hd]);
+               [ce2pres_in_proof_context_element hd]);
              continuation'])
-         
-  and ce2pres =
+        
+  and ce2pres_in_joint_context_element = function
+    | `Inductive _ -> assert false (* TODO *)
+    | (`Declaration _) as x -> ce2pres x
+    | (`Hypothesis _) as x  -> ce2pres x
+    | (`Proof _) as x       -> ce2pres x
+    | (`Definition _) as x  -> ce2pres x
+  
+  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
+    | (`Proof _) as x       -> ce2pres x
+    | (`Definition _) as x  -> ce2pres x
+  
+  and ce2pres = 
     let module Con = Content in
-      function
+    function 
         `Declaration d -> 
           (match d.Con.dec_name with
               Some s ->
@@ -300,8 +320,6 @@ and proof2pres term2pres p =
                    term])
             | None -> 
                 prerr_endline "NO NAME!!"; assert false) 
-      | `Joint ho -> 
-            B.Text ([],"jointdef")
 
   and acontext2pres ac continuation indent =
     let module Con = Content in
@@ -376,7 +394,11 @@ and proof2pres term2pres p =
       let arg = 
         (match conclude.Con.conclude_args with 
            [Con.Term t] -> term2pres t
-         | _ -> assert false) in
+         | [Con.Premise p] -> 
+             (match p.Con.premise_binder with
+             | None -> assert false; (* unnamed hypothesis ??? *)
+             | Some s -> B.Text([],s))
+         | err -> assert false) in
       (match conclude.Con.conclude_conclusion with 
          None ->
           B.b_h [] [B.b_kw "Consider"; B.b_space; arg]
@@ -495,7 +517,7 @@ and proof2pres term2pres p =
                B.Text ([],"a proof???")
            | Con.ArgMethod s -> 
                B.Text ([],"a method???")) in
-        (make_concl "we proceede by cases on" case_arg) in
+        (make_concl "we proceed by cases on" case_arg) in
      let to_prove =
         (make_concl "to prove" proof_conclusion) in
      B.V 
@@ -531,7 +553,7 @@ and proof2pres term2pres p =
                B.Text ([],"a proof???")
            | Con.ArgMethod s -> 
                B.Text ([],"a method???")) in
-        (make_concl "we proceede by induction on" arg) in
+        (make_concl "we proceed by induction on" arg) in
      let to_prove =
         (make_concl "to prove" proof_conclusion) in
      B.V 
@@ -820,24 +842,59 @@ let metasenv2pres term2pres = function
              (let _ = incr counter; in (string_of_int !counter)))) ::
          (List.map (conjecture2pres term2pres) metasenv'))]
 
-let get_name = function
-  | Some s -> s
-  | None -> "_"
+let params2pres params =
+  let param2pres uri =
+    B.b_text [Some "xlink", "href", UriManager.string_of_uri uri]
+      (UriManager.name_of_uri uri)
+  in
+  let rec spatiate = function
+    | [] -> []
+    | hd :: [] -> [hd]
+    | hd :: tl -> hd :: B.b_text [] ", " :: spatiate tl
+  in
+  match params with
+  | [] -> []
+  | p ->
+      let params = spatiate (List.map param2pres p) in
+      [B.b_space;
+       B.b_h [] (B.b_text [] "[" :: params @ [ B.b_text [] "]" ])]
+
+let recursion_kind2pres params kind =
+  let kind =
+    match kind with
+    | `Recursive _ -> "Recursive definition"
+    | `CoRecursive -> "CoRecursive definition"
+    | `Inductive _ -> "Inductive definition"
+    | `CoInductive _ -> "CoInductive definition"
+  in
+  B.b_h [] (B.b_text [] kind :: params2pres params)
+
+let inductive2pres term2pres ind =
+  let constructor2pres decl =
+    B.b_h [] [
+      B.b_text [] ("| " ^ get_name decl.Content.dec_name ^ ":");
+      B.b_space;
+      term2pres decl.Content.dec_type
+    ]
+  in
+  B.b_v []
+    (B.b_h [] [
+      B.b_text [] (ind.Content.inductive_name ^ " of arity ");
+      term2pres ind.Content.inductive_type ]
+    :: List.map constructor2pres ind.Content.inductive_constructors)
 
-let pp_params = function
-  | [] -> ""
-  | params ->
-      " (" ^
-      String.concat " ; " (List.map UriManager.string_of_uri params) ^
-      ")"
+let joint_def2pres term2pres def =
+  match def with
+  | `Inductive ind -> inductive2pres term2pres ind
+  | _ -> assert false (* ZACK or raise ToDo? *)
 
 let content2pres term2pres (id,params,metasenv,obj) =
   match obj with
   | `Def (Content.Const, thesis, `Proof p) ->
       let name = get_name p.Content.proof_name in
       B.b_v
-        [None,"helm:xref","id"]
-        ([ B.b_text [] ("Proof " ^ name ^ pp_params params);
+        [Some "helm","xref","id"]
+        ([ B.b_h [] (B.b_text [] ("Proof " ^ name) :: params2pres params);
            B.b_text [] "Thesis:";
            B.indent (term2pres thesis) ] @
          metasenv2pres term2pres metasenv @
@@ -845,8 +902,8 @@ let content2pres term2pres (id,params,metasenv,obj) =
   | `Def (_, ty, `Definition body) ->
       let name = get_name body.Content.def_name in
       B.b_v
-        [None,"helm:xref","id"]
-        ([B.b_text [] ("Definition " ^ name ^ pp_params params);
+        [Some "helm","xref","id"]
+        ([B.b_h [] (B.b_text [] ("Definition " ^ name) :: params2pres params);
           B.b_text [] "Type:";
           B.indent (term2pres ty)] @
           metasenv2pres term2pres metasenv @
@@ -855,11 +912,15 @@ let content2pres term2pres (id,params,metasenv,obj) =
   | `Decl (_, `Hypothesis decl) ->
       let name = get_name decl.Content.dec_name in
       B.b_v
-        [None,"helm:xref","id"]
-        ([B.b_text [] ("Axiom " ^ name ^ pp_params params);
+        [Some "helm","xref","id"]
+        ([B.b_h [] (B.b_text [] ("Axiom " ^ name) :: params2pres params);
           B.b_text [] "Type:";
           B.indent (term2pres decl.Content.dec_type)] @
           metasenv2pres term2pres metasenv)
+  | `Joint joint ->
+      B.b_v []
+        (recursion_kind2pres params joint.Content.joint_kind
+        :: List.map (joint_def2pres term2pres) joint.Content.joint_defs)
   | _ -> raise ToDo
 ;;