X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnCicElim.ml;h=79a22b07720fa9d5a3e7b2503324653a249becd7;hb=3c17c53d6628c1863a33ab071266a0f5614bbce1;hp=ae472ae38cbdaf37633b73fe2655342d589fa1bc;hpb=24c5f3d919918175b6380f47cf9613ee4bd7af80;p=helm.git diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml index ae472ae38..79a22b077 100644 --- a/helm/software/components/ng_tactics/nCicElim.ml +++ b/helm/software/components/ng_tactics/nCicElim.ml @@ -98,7 +98,7 @@ let mk_elim uri leftno [it] (outsort,suffix) = params @ [p_name] @ k_names @ - List.map (fun _ -> CicNotationPt.Implicit) + List.map (fun _ -> CicNotationPt.Implicit `JustOne) (List.tl args) @ [mk_appl (name::abs)]))) | _ -> mk_id name,None @@ -148,17 +148,27 @@ let mk_elim uri leftno [it] (outsort,suffix) = (function x::_ -> x | _ -> assert false) 80 (CicNotationPres.mpres_of_box boxml))); *) - CicNotationPt.Theorem (`Definition,srec_name,CicNotationPt.Implicit,Some res) + CicNotationPt.Theorem + (`Definition,srec_name,CicNotationPt.Implicit `JustOne,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)) @@ -166,3 +176,122 @@ 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 +;; + +(* this code should be unified with NTermCicContent.nast_of_cic0, + but the two contexts have different types *) +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.Meta _ + | NCic.Implicit _ -> assert false + | 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) + | NCic.Lambda (n,s,t) -> + let n = mk_id n in + CicNotationPt.Binder (`Lambda, (n,Some (pp rels s)), pp (n::rels) t) + | NCic.LetIn (n,s,ty,t) -> + let n = mk_id n in + CicNotationPt.LetIn ((n, Some (pp rels ty)), pp rels s, pp (n::rels) t) + | NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) -> + let name = NUri.name_of_uri uri in + let case_indty = Some (name, None) in + let constructors, leftno = + let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys r in + let _,_,_,cl = List.nth tys n in + cl,leftno + in + let rec eat_branch n rels ty pat = + match (ty, pat) with + | NCic.Prod (name, s, t), _ when n > 0 -> + eat_branch (pred n) rels t pat + | NCic.Prod (_, _, t), NCic.Lambda (name, s, t') -> + let cv, rhs = eat_branch 0 ((mk_id name)::rels) t t' in + (mk_id name, Some (pp rels s)) :: cv, rhs + | _, _ -> [], pp rels pat + in + let patterns = + try + List.map2 + (fun (_, name, ty) pat -> + let capture_variables,rhs = eat_branch leftno rels ty pat in + CicNotationPt.Pattern (name, None, capture_variables), rhs + ) constructors patterns + with Invalid_argument _ -> assert false + in + CicNotationPt.Case (pp rels te, case_indty, Some (pp rels outty), patterns) +;; + +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 + [arg, Some arg_ty], CicNotationPt.Case (arg,None,Some outtype,[branch]) + | _,NCic.Prod (name,_,t) -> + let name = mk_id name in + let params,body = aux (name::names) t (leftno - 1) in + (name,None)::params, body + | _,_ -> assert false + in + let params,bo = aux [] consty leftno in + let pprojname = mk_id projname in + let res = + CicNotationPt.LetRec (`Inductive, + [params, (pprojname,None), bo, leftno], pprojname) 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 `JustOne,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 + | _ -> [] +;;