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 54d8d5df62cfd27e2d9a28e862943fd5e1553c10..08c8b0f5609fddf3d17ef48a38c19d0571ad2914 100644 (file)
--- a/helm/software/components/ng_tactics/nCicElim.ml
+++ b/helm/software/components/ng_tactics/nCicElim.ml
@@ -38,15 +38,15 @@ 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
      let params = List.rev_map (function name,_ -> mk_id name) params in
      let args,sort = NCicReduction.split_prods ~subst:[] [] (-1) ty in
-     let rec_arg = mk_id (fresh_name ()) in
      let args = List.rev_map (function name,_ -> mk_id name) args in
+     let rec_arg = mk_id (fresh_name ()) in
      let p_ty =
       List.fold_right
        (fun name res -> CicNotationPt.Binder (`Forall,(name,None),res)) args
@@ -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) ->
@@ -70,23 +72,32 @@ let mk_elims (uri,_,_,_,obj) =
          let cargs_and_recursive_args =
           List.rev_map
            (function
-               name,NCic.Def _ -> assert false
-             | name,NCic.Decl (NCic.Const nref)
-             | name,NCic.Decl (NCic.Appl (NCic.Const nref::_))
-               when
-                let NReference.Ref (uri',_) = nref in
-                 NUri.eq uri uri'
-               ->
-                let name = mk_id name in
-                 name, Some (
-                 CicNotationPt.Appl
-                  (rec_name ::
-                   params @
-                   [p_name] @
-                   k_names @
-                   List.map (fun _ -> CicNotationPt.Implicit) (List.tl args) @
-                   [name]))
-             | name,_ -> mk_id name,None
+               _,NCic.Def _ -> assert false
+             | name,NCic.Decl ty ->
+                let context,ty = my_split_prods ~subst:[] [] (-1) ty in
+                 match ty with
+                  | NCic.Const nref
+                  | NCic.Appl (NCic.Const nref::_)
+                     when
+                      let NReference.Ref (uri',_) = nref in
+                       NUri.eq uri uri'
+                     ->
+                      let abs = List.rev_map (fun id,_ -> mk_id id) context in
+                      let name = mk_id name in
+                       name, Some (
+                       List.fold_right
+                        (fun id res ->
+                          CicNotationPt.Binder (`Lambda,(id,None),res))
+                        abs
+                        (CicNotationPt.Appl
+                         (rec_name ::
+                          params @
+                          [p_name] @
+                          k_names @
+                          List.map (fun _ -> CicNotationPt.Implicit)
+                           (List.tl args) @
+                          [CicNotationPt.Appl (name::abs)])))
+                  | _ -> mk_id name,None
            ) cargs in
          let cargs,recursive_args = List.split cargs_and_recursive_args in
          let recursive_args = HExtlib.filter_map (fun x -> x) recursive_args in
@@ -106,9 +117,32 @@ let mk_elims (uri,_,_,_,obj) =
        (BoxPp.render_to_string
          ~map_unicode_to_tex:false
          (function x::_ -> x | _ -> assert false)
-         80 (CicNotationPres.render (Hashtbl.create 0)
+         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)));
       []
   | _ -> []
 ;;