From 72b4799ea220bc54dc27b34fdb863f1ee6fc9e08 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 21 Jul 2009 20:20:18 +0000 Subject: [PATCH] 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? --- .../grafite_engine/grafiteEngine.ml | 1 + .../components/ng_tactics/nCicElim.ml | 113 +++++++++++++++--- .../components/ng_tactics/nCicElim.mli | 2 +- .../matita/nlibrary/algebra/magmas.ma | 37 ++---- 4 files changed, 111 insertions(+), 42 deletions(-) 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 -- 2.39.2