X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnCicElim.ml;h=a124b28388d3fa83d38ad6a6a8d444724d963215;hb=71d8526b03b2b7f415404074b4a0d51b71afb85a;hp=0c1a98ec342a9848406f925bc60056257afa1a59;hpb=65792c85896dab2d3c69e7eafd8ff5c628260773;p=helm.git

diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml
index 0c1a98ec3..a124b2838 100644
--- a/helm/software/components/ng_tactics/nCicElim.ml
+++ b/helm/software/components/ng_tactics/nCicElim.ml
@@ -66,7 +66,6 @@ let mk_elim uri leftno [it] (outsort,suffix) =
   [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 =
@@ -110,12 +109,14 @@ let mk_elim uri leftno [it] (outsort,suffix) =
        mk_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 bo = CicNotationPt.Case (rec_arg,Some (ind_name,None),None,branches) in
+ let recno = List.length final_params in
+ let where = recno - 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
@@ -146,17 +147,27 @@ let mk_elim uri leftno [it] (outsort,suffix) =
    (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
+      (try
+        if String.sub u 0 4 = "Type" then
+         `NType (String.sub u 4 (String.length u - 4)), "rect_" ^ u
+        else if String.sub u 0 5 = "CProp" then
+         `NCProp (String.sub u 5 (String.length u - 5)), "rect_" ^ u
+        else
+         (prerr_endline u;
+         assert false)
+       with Failure _ -> assert false)
+;;
+
 let mk_elims (uri,_,_,_,obj) =
- 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))
@@ -164,3 +175,83 @@ let mk_elims (uri,_,_,_,obj) =
          List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes ()))
    | _ -> []
 ;;
+
+(********************* Projections **********************)
+
+let mk_lambda =
+ function
+    [] -> assert false 
+  | [t] -> t
+  | l -> CicNotationPt.Appl l
+;;
+
+let rec count_prods = function NCic.Prod (_,_,t) -> 1 + count_prods t | _ -> 0;;
+
+let rec nth_prod projs n ty =
+ match ty with
+    NCic.Prod (_,s,_) when n=0 -> projs, s
+  | NCic.Prod (name,_,t) -> nth_prod (name::projs) (n-1) t
+  | _ -> assert false
+;;
+
+let rec pp rels =
+ function
+    NCic.Rel i -> List.nth rels (i - 1)
+  | NCic.Const _ as t ->
+     CicNotationPt.Ident
+      (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t,None)
+  | NCic.Sort s -> CicNotationPt.Sort (fst (ast_of_sort s))
+  | NCic.Appl l -> CicNotationPt.Appl (List.map (pp rels) l)
+  | NCic.Prod (n,s,t) ->
+     let n = mk_id n in
+      CicNotationPt.Binder (`Pi, (n,Some (pp rels s)), pp (n::rels) t)
+  | _ -> assert false (* not implemented yet *)
+;;
+
+let mk_projection leftno tyname consname consty (projname,_,_) i =
+ let argsno = count_prods consty - leftno in
+ let rec aux names ty leftno =
+  match leftno,ty with
+   | 0,_ ->
+     let arg = mk_id "xxx" in
+     let arg_ty = mk_appl (mk_id tyname :: List.rev names) in
+     let bvar = mk_id "yyy" in
+     let underscore = CicNotationPt.Ident ("_",None),None in
+     let bvars =
+      HExtlib.mk_list underscore i @ [bvar,None] @
+       HExtlib.mk_list underscore (argsno - i -1) in
+     let branch = CicNotationPt.Pattern (consname,None,bvars), bvar in
+     let projs,outtype = nth_prod [] i ty in
+     let rels =
+      List.map
+       (fun name -> mk_appl (mk_id name :: List.rev names @ [arg])) projs
+      @ names in
+     let outtype = pp rels outtype in
+     let outtype= CicNotationPt.Binder (`Lambda, (arg, Some arg_ty), outtype) in
+      CicNotationPt.Binder
+       (`Lambda, (arg,Some arg_ty),
+         CicNotationPt.Case (arg,None,Some outtype,[branch]))
+   | _,NCic.Prod (name,_,t) ->
+      let name = mk_id name in
+       CicNotationPt.Binder
+        (`Lambda, (name,None), aux (name::names) t (leftno - 1))
+   | _,_ -> assert false
+ in
+ let res = aux [] consty leftno 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)));*)
+  CicNotationPt.Theorem (`Definition,projname,CicNotationPt.Implicit,Some res)
+;;
+
+let mk_projections (_,_,_,_,obj) =
+ match obj with
+    NCic.Inductive
+     (true,leftno,[_,tyname,_,[_,consname,consty]],(_,`Record fields))
+    ->
+     HExtlib.list_mapi (mk_projection leftno tyname consname consty) fields
+  | _ -> []
+;;