From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 17 Jul 2009 13:31:13 +0000 (+0000)
Subject: New suffixes for elimination principles:
X-Git-Tag: make_still_working~3671
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e24cc96a07f8513782d3bc7c2ec2739aa85c04e5;p=helm.git

New suffixes for elimination principles:

_ind (towards Prop)
_rect_UNIVERSENAME (towards Type)
---

diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml
index 2a02b7d17..350144f9e 100644
--- a/helm/software/components/ng_tactics/nCicElim.ml
+++ b/helm/software/components/ng_tactics/nCicElim.ml
@@ -41,115 +41,126 @@ let mk_appl =
   | l -> CicNotationPt.Appl l
 ;;
 
+let mk_elim uri leftno [it] (outsort,suffix) =
+ let _,ind_name,ty,cl = it in
+ let srec_name = ind_name ^ "_" ^ suffix 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 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
+   (CicNotationPt.Binder
+    (`Forall,
+     (rec_arg,Some (mk_appl (mk_id ind_name :: params @ args))),
+     CicNotationPt.Sort outsort)) in
+ let args = args @ [rec_arg] in
+ let k_names = List.map (function _,name,_ -> name_of_k name) cl in
+ let final_params =
+  List.map (function name -> name, None) params @
+  [p_name,Some p_ty] @
+  List.map (function name -> name, None) k_names @
+  List.map (function name -> name, None) args in
+ let recno = List.length final_params in
+ let cty = mk_appl (p_name :: args) in
+ let ty = Some cty in
+ let branches =
+  List.map
+   (function (_,name,ty) ->
+     let _,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in
+     let cargs,ty= my_split_prods ~subst:[] [] (-1) ty in
+     let cargs_and_recursive_args =
+      List.rev_map
+       (function
+           _,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) @
+                      [mk_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
+      CicNotationPt.Pattern (name,None,List.map (fun x -> x,None) cargs),
+       CicNotationPt.Appl (name_of_k name :: cargs @ recursive_args)
+   ) cl
+ in
+ let bo = CicNotationPt.Case (rec_arg,None,None,branches) in
+ let where = List.length final_params - 1 in
+ let res =
+  CicNotationPt.LetRec (`Inductive,
+   [final_params, (rec_name,ty), bo, where], rec_name)
+ in
+  prerr_endline
+   (BoxPp.render_to_string
+     ~map_unicode_to_tex:false
+     (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)));
+  CicNotationPt.Theorem (`Definition,srec_name,CicNotationPt.Implicit,Some res)
+;;
+
 let mk_elims (uri,_,_,_,obj) =
- match obj with
-    NCic.Inductive (true,leftno,[it],_) ->
-     let _,ind_name,ty,cl = it 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 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
-       (CicNotationPt.Binder
-        (`Forall,
-         (rec_arg,Some (mk_appl (mk_id ind_name :: params @ args))),
-         CicNotationPt.Sort (`Type (CicUniv.fresh ())))) in
-     let args = args @ [rec_arg] in
-     let k_names = List.map (function _,name,_ -> name_of_k name) cl in
-     let final_params =
-      List.map (function name -> name, None) params @
-      [p_name,Some p_ty] @
-      List.map (function name -> name, None) k_names @
-      List.map (function name -> name, None) args in
-     let recno = List.length final_params in
-     let cty = mk_appl (p_name :: args) in
-     let ty = Some cty in
-     let branches =
-      List.map
-       (function (_,name,ty) ->
-         let _,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in
-         let cargs,ty= my_split_prods ~subst:[] [] (-1) ty in
-         let cargs_and_recursive_args =
-          List.rev_map
-           (function
-               _,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) @
-                          [mk_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
-          CicNotationPt.Pattern (name,None,List.map (fun x -> x,None) cargs),
-           CicNotationPt.Appl (name_of_k name :: cargs @ recursive_args)
-       ) cl
-     in
-     let bo = CicNotationPt.Case (rec_arg,None,None,branches) in
-     let where = List.length final_params - 1 in
-     let res =
-      CicNotationPt.LetRec (`Inductive,
-       [final_params, (rec_name,ty), bo, where], rec_name)
-     in
-      prerr_endline (CicNotationPp.pp_term res);
-      prerr_endline "#####";
-      prerr_endline
-       (BoxPp.render_to_string
-         ~map_unicode_to_tex:false
-         (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)));
-      [CicNotationPt.Theorem (`Definition,srec_name,CicNotationPt.Implicit,Some res)]
-  | _ -> []
+ let ast_of_sort s =
+   match s with
+      NCic.Prop -> `Prop,"ind"
+    | NCic.Type u ->
+       let u = NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] (NCic.Sort s) in
+       `NType u, "rect_" ^ u
+ in
+  match obj with
+     NCic.Inductive (true,leftno,itl,_) ->
+      List.map (fun s -> mk_elim uri leftno itl (ast_of_sort s))
+       (NCic.Prop::
+         List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes ()))
+   | _ -> []
 ;;