From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 21 Jul 2009 20:20:18 +0000 (+0000)
Subject: Record projections are now automatically generated for NG.
X-Git-Tag: make_still_working~3642
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=72b4799ea220bc54dc27b34fdb863f1ee6fc9e08;p=helm.git

Record projections are now automatically generated for NG.

Note: I have implemented a partial function from NCic.term to
CicNotationPt.term. Is there already a similar function? Where should it be
moved?
---

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index 3976978f7..99414f63c 100644
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -968,6 +968,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) =
          (try
        (*prerr_endline (NCicPp.ppobj obj);*)
            let boxml = NCicElim.mk_elims obj in
+           let boxml = boxml @ NCicElim.mk_projections obj in
 (*
            let objs = [] in
            let timestamp,uris_rev =
diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml
index ef33ceeab..684874ce6 100644
--- 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
+  | _ -> []
+;;
diff --git a/helm/software/components/ng_tactics/nCicElim.mli b/helm/software/components/ng_tactics/nCicElim.mli
index 677454550..e8b4c7a8d 100644
--- a/helm/software/components/ng_tactics/nCicElim.mli
+++ b/helm/software/components/ng_tactics/nCicElim.mli
@@ -11,5 +11,5 @@
 
 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
 
-(* val mk_elims: NCic.obj -> NCic.obj list *)
 val mk_elims: NCic.obj -> CicNotationPt.term CicNotationPt.obj list
+val mk_projections: NCic.obj -> CicNotationPt.term CicNotationPt.obj list
diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma
index 40400378d..d74913988 100644
--- a/helm/software/matita/nlibrary/algebra/magmas.ma
+++ b/helm/software/matita/nlibrary/algebra/magmas.ma
@@ -18,54 +18,29 @@ nrecord pre_magma : Type[1] ≝
  { carr: Type;
    op: carr → carr → carr
  }.
-(* this is a projection *)
-ndefinition carr: pre_magma → Type
- ≝ λM: pre_magma. match M with [ mk_pre_magma carr _ ⇒ carr ].
 ncoercion carr: ∀M:pre_magma. Type ≝ carr on _M: pre_magma to Type.
-ndefinition op ≝
- λM: pre_magma. match M return λM:pre_magma. M → M → M with [ mk_pre_magma _ op ⇒ op ].
 
 nrecord magma (A: pre_magma) : Type[1] ≝
  { mcarr: Ω \sup A;
    op_closed: ∀x,y. x ∈ mcarr → y ∈ mcarr → op A x y ∈ mcarr
  }.
-(* this is a projection *)
-ndefinition mcarr ≝ λA.λM: magma A. match M with [ mk_magma mcarr _ ⇒ mcarr ].
 ncoercion mcarr: ∀A.∀M: magma A. Ω \sup A ≝ mcarr
  on _M: magma ? to Ω \sup ?.
-ndefinition op_closed ≝
- λA.λM: magma A.
-  match M return λM: magma A.∀x,y. x ∈ M → y ∈ M → op ? x y ∈ M with
-   [ mk_magma _ opc ⇒ opc ].
 
 nrecord pre_magma_morphism (A,B: pre_magma) : Type ≝
  { mmcarr: A → B;
    mmprop: ∀x,y. mmcarr (op ? x y) = op ? (mmcarr x) (mmcarr y)
  }.
-(* this is a projection *)
-ndefinition mmcarr ≝
- λA,B.λf: pre_magma_morphism A B. match f with [ mk_pre_magma_morphism f _ ⇒ f ].
 ncoercion mmcarr: ∀A,B.∀M: pre_magma_morphism A B. A → B ≝ mmcarr
  on _M: pre_magma_morphism ? ? to ∀_.?.
-ndefinition mmprop ≝
- λA,B,M.
-  match M return λM:pre_magma_morphism A B.∀x,y. M (op ? x y) = op ? (M x) (M y) with
-   [ mk_pre_magma_morphism _ p ⇒ p ].
 
 nrecord magma_morphism (A) (B) (Ma: magma A) (Mb: magma B) : Type ≝
  { mmmcarr: pre_magma_morphism A B;
    mmclosed: ∀x. x ∈ Ma → mmmcarr x ∈ Mb
  }.
-(* this is a projection *)
-ndefinition mmmcarr ≝
- λA,B,Ma,Mb.λf: magma_morphism A B Ma Mb. match f with [ mk_magma_morphism f _ ⇒ f ].
 ncoercion mmmcarr : ∀A,B,Ma,Mb.∀f: magma_morphism A B Ma Mb. pre_magma_morphism A B
  ≝ mmmcarr
  on _f: magma_morphism ???? to pre_magma_morphism ??.
-ndefinition mmclosed ≝
- λA,B,Ma,Mb.λf: magma_morphism A B Ma Mb.
-  match f return λf: magma_morphism A B Ma Mb.∀x. x ∈ Ma → f x ∈ Mb with
-   [ mk_magma_morphism _ p ⇒ p ].
  
 ndefinition sub_magma ≝
  λA.λM1,M2: magma A. M1 ⊆ M2.
@@ -86,4 +61,14 @@ ndefinition mm_image:
         | nrewrite < Hx1;
           nrewrite < Hy1;
           napply (mmprop ?? f ??)]##]
-nqed.
\ No newline at end of file
+nqed.
+
+ndefinition counter_image: ∀A,B. (A → B) → Ω \sup B → Ω \sup A ≝
+ λA,B,f,Sb. {x | ∃y. y ∈ Sb ∧ f x = y}.
+ 
+ndefinition mm_counter_image:
+ ∀A,B. ∀Ma: magma A. ∀Mb: magma B. magma_morphism ?? Ma Mb → magma A.
+  #A; #B; #Ma; #Mb; #f;
+  napply (mk_magma ???)
+   [ napply (counter_image ?? f Mb)
+   | #x; #y; nwhd in ⊢ (% → % → ?); *; #y0; *; #Hy0; #H