Record projections are now automatically generated for NG.

[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 ef33ceeab20cf6c1d7c1fb3aab65091fe0fd11ed..684874ce62bbdc87e22d0c4213aaa4dd583290d2 100644 (file)
--- a/helm/software/components/ng_tactics/nCicElim.ml
+++ b/helm/software/components/ng_tactics/nCicElim.ml
@@ -151,22 +151,23 @@ let mk_elim uri leftno [it] (outsort,suffix) =
   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
-       (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)
- in
   match obj with
      NCic.Inductive (true,leftno,itl,_) ->
       List.map (fun s -> mk_elim uri leftno itl (ast_of_sort s))
@@ -174,3 +175,85 @@ 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
+prerr_endline ("outtype[" ^ string_of_int i ^ "]: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty);
+prerr_endline ("XXX[" ^ string_of_int i ^ "]: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] outtype);
+     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
+  | _ -> []
+;;