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

[helm.git] / helm / software / components / ng_tactics / nCicElim.ml

diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml
index fba21753a53ce6ef8b749839b716020ca7b702e8..08c8b0f5609fddf3d17ef48a38c19d0571ad2914 100644 (file)
--- a/helm/software/components/ng_tactics/nCicElim.ml
+++ b/helm/software/components/ng_tactics/nCicElim.ml
@@ -38,8 +38,8 @@ let mk_elims (uri,_,_,_,obj) =
  match obj with
     NCic.Inductive (true,leftno,[it],_) ->
      let _,ind_name,ty,cl = it in
-     let rec_name = ind_name ^ "_rect" in
-     let rec_name = mk_id rec_name in
+     let srec_name = ind_name ^ "_rect" in
+     let rec_name = mk_id srec_name in
      let name_of_k id = mk_id ("H_" ^ id) in
      let p_name = mk_id "Q_" in
      let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in
@@ -61,7 +61,9 @@ let mk_elims (uri,_,_,_,obj) =
       [p_name,Some p_ty] @
       List.map (function name -> name, None) k_names @
       List.map (function name -> name, None) args in
-     let ty = Some (CicNotationPt.Appl (p_name :: args)) in
+     let recno = List.length final_params in
+     let cty = CicNotationPt.Appl (p_name :: args) in
+     let ty = Some cty in
      let branches =
       List.map
        (function (_,name,ty) ->
@@ -117,6 +119,30 @@ let mk_elims (uri,_,_,_,obj) =
          (function x::_ -> x | _ -> assert false)
          80 (CicNotationPres.render (fun _ -> None)
          (TermContentPres.pp_ast res)));
+      prerr_endline "#####";
+      let cobj = ("xxx", [], None, `Joint {
+          Content.joint_id = "yyy";
+          joint_kind = `Recursive [recno];
+          joint_defs =
+           [ `Definition {
+                Content.def_name = Some srec_name;
+                def_id = "zzz";
+                def_aref = "www";
+                def_term = bo;
+                def_type = 
+                  List.fold_right 
+                    (fun x t -> CicNotationPt.Binder(`Forall,x,t))
+                    final_params cty
+              }
+           ];
+        })
+      in
+      let ids_to_nrefs = Hashtbl.create 1 in
+      let boxml = Content2pres.ncontent2pres ~ids_to_nrefs cobj in
+      prerr_endline (
+       (BoxPp.render_to_string ~map_unicode_to_tex:false
+         (function x::_ -> x | _ -> assert false) 80 
+         (CicNotationPres.mpres_of_box boxml)));
       []
   | _ -> []
 ;;