ncopy partially implemented and fixed (a ?) chain to print elimintaors

[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 6dee8f04066b2a1023cb006fad016f480b0a7719..63eec5e351a21dec9d50b7c2aedffc1ef580b433 100644 (file)
--- a/helm/software/components/content_pres/content2pres.ml
+++ b/helm/software/components/content_pres/content2pres.ml
@@ -908,6 +908,7 @@ let recursion_kind2pres params kind =
         "Co-Inductive definition with "^string_of_int i^" fixed parameter(s)"
   in
   B.b_h [] (B.b_kw kind :: params2pres params)
+;;
 
 let inductive2pres term2pres ind =
   let constructor2pres decl =
@@ -924,10 +925,84 @@ let inductive2pres term2pres ind =
       term2pres ind.Content.inductive_type ]
     :: List.map constructor2pres ind.Content.inductive_constructors)
 
-let joint_def2pres term2pres def =
+let definition2pres ?recno term2pres d =
+  let name = match d.Content.def_name with Some x -> x|_->assert false in
+  let rno = match recno with None -> assert false | Some x -> x in
+  let ty = d.Content.def_type in
+  let module P = CicNotationPt in
+  let rec split_pi i t = 
+    if i <= 1 then 
+      match t with 
+      | P.Binder ((`Pi|`Forall),(var,_ as v),t) -> [v], var, t 
+      | _ -> assert false
+    else
+      match t with
+      | P.Binder ((`Pi|`Forall), var ,ty) ->
+           let l, r, t = split_pi (i-1) ty in
+           var :: l, r, t
+      | _ -> assert false
+  in 
+  let params, rec_param, ty = split_pi rno ty in
+  let body = d.Content.def_term in
+  let params = 
+    List.map 
+      (function 
+      | (name,Some ty) -> 
+          B.b_h [] [B.b_text [] "("; term2pres name; B.b_text [] " : ";
+                    B.b_space; term2pres ty; B.b_text [] ")"; B.b_space]
+      | (name,None) -> B.b_h [] [term2pres name;B.b_space]) 
+      params
+  in
+  B.b_hv [] 
+   [B.b_hv [] 
+    ([ B.b_space; B.b_text [] name ] @ params @
+       [B.b_kw "on" ; B.b_space; term2pres rec_param ; B.b_space;
+       B.b_text [] ":"; B.b_space; term2pres ty]); 
+   B.b_text [] ":=";
+   B.b_h [] [B.b_space;term2pres body] ]
+;;
+
+let joint_def2pres ?recno term2pres def =
   match def with
   | `Inductive ind -> inductive2pres term2pres ind
-  | _ -> assert false (* ZACK or raise ToDo? *)
+  | _ -> assert false
+;;
+
+let njoint_def2pres ?recno term2pres def =
+  match def with
+  | `Inductive ind -> inductive2pres term2pres ind
+  | `Definition def -> definition2pres ?recno term2pres def 
+  | _ -> assert false
+;;
+
+let njoint_def2pres term2pres joint_kind defs =
+  match joint_kind with
+  | `Recursive recnos ->
+      B.b_hv [] (B.b_kw "nlet rec " ::
+        List.flatten
+         (HExtlib.list_mapi (fun x i -> 
+            if i > 0 then [B.b_kw " and ";x] else [x])
+          (List.map2 (fun a b -> njoint_def2pres ~recno:a term2pres b) 
+            recnos defs)))
+  | `CoRecursive ->
+      B.b_hv [] (B.b_kw "nlet corec " ::
+        List.flatten
+         (HExtlib.list_mapi (fun x i -> 
+            if i > 0 then [B.b_kw " and ";x] else [x])
+          (List.map (njoint_def2pres term2pres) defs)))
+  | `Inductive _ -> 
+      B.b_hv [] (B.b_kw "ninductive " ::
+        List.flatten
+         (HExtlib.list_mapi (fun x i -> 
+            if i > 0 then [B.b_kw " and ";x] else [x])
+          (List.map (njoint_def2pres term2pres) defs)))
+  | `CoInductive _ -> 
+      B.b_hv [] (B.b_kw "ncoinductive " ::
+        List.flatten
+         (HExtlib.list_mapi (fun x i -> 
+            if i > 0 then [B.b_kw " and ";x] else [x])
+          (List.map (njoint_def2pres term2pres) defs)))
+;;
 
 let content2pres0
   ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres 
@@ -988,7 +1063,7 @@ let content2pres
 
 let ncontent2pres0
   ?skip_initial_lambdas ?(skip_thm_and_qed=false) term2pres 
-  (id,params,metasenv,obj) 
+  (id,params,metasenv,obj : CicNotationPt.term Content.cobj) 
 =
   match obj with
   | `Def (Content.Const, thesis, `Proof p) ->
@@ -1025,9 +1100,9 @@ let ncontent2pres0
           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)
+      B.b_v [] 
+        [njoint_def2pres term2pres 
+          joint.Content.joint_kind joint.Content.joint_defs]
   | _ -> raise ToDo
 
 let ncontent2pres ?skip_initial_lambdas ?skip_thm_and_qed ~ids_to_nrefs =