X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnCicElim.ml;h=359d93bbd5c72c48ff5700060fb82c4935ce0026;hb=5cfd68a5d9e73edb40e1cfe021a1426354767aa8;hp=79a22b07720fa9d5a3e7b2503324653a249becd7;hpb=3c17c53d6628c1863a33ab071266a0f5614bbce1;p=helm.git diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml index 79a22b077..359d93bbd 100644 --- a/helm/software/components/ng_tactics/nCicElim.ml +++ b/helm/software/components/ng_tactics/nCicElim.ml @@ -38,10 +38,11 @@ let mk_appl = function [] -> assert false | [x] -> x + | CicNotationPt.Appl l1 :: l2 -> CicNotationPt.Appl (l1 @ l2) | l -> CicNotationPt.Appl l ;; -let mk_elim uri leftno [it] (outsort,suffix) = +let mk_elim uri leftno it (outsort,suffix) pragma = let _,ind_name,ty,cl = it in let srec_name = ind_name ^ "_" ^ suffix in let rec_name = mk_id srec_name in @@ -52,30 +53,34 @@ let mk_elim uri leftno [it] (outsort,suffix) = let args,sort = NCicReduction.split_prods ~subst:[] [] (-1) ty in let args = List.rev_map (function name,_ -> mk_id name) args in let rec_arg = mk_id (fresh_name ()) in - let p_ty = + let mk_prods = List.fold_right - (fun name res -> CicNotationPt.Binder (`Forall,(name,None),res)) args + (fun name res -> CicNotationPt.Binder (`Forall,(name,None),res)) in + let p_ty = mk_prods args (CicNotationPt.Binder (`Forall, (rec_arg,Some (mk_appl (mk_id ind_name :: params @ args))), CicNotationPt.Sort outsort)) in + let mk_arrs n = mk_prods (HExtlib.mk_list (mk_id "_") n) in let args = args @ [rec_arg] in let k_names = List.map (function _,name,_ -> name_of_k name) cl in + (* let final_params = List.map (function name -> name, None) params @ [p_name,Some p_ty] @ List.map (function name -> name, None) k_names @ List.map (function name -> name, None) args in + *) let cty = mk_appl (p_name :: args) in let ty = Some cty in - let branches = + let branches_with_args = List.map (function (_,name,ty) -> let _,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in let cargs,ty= my_split_prods ~subst:[] [] (-1) ty in - let cargs_and_recursive_args = - List.rev_map - (function + let cargs_recargs_nih = + List.fold_left + (fun (acc,nih) -> function _,NCic.Def _ -> assert false | name,NCic.Decl ty -> let context,ty = my_split_prods ~subst:[] [] (-1) ty in @@ -88,7 +93,7 @@ let mk_elim uri leftno [it] (outsort,suffix) = -> let abs = List.rev_map (fun id,_ -> mk_id id) context in let name = mk_id name in - name, Some ( + (name, Some ( List.fold_right (fun id res -> CicNotationPt.Binder (`Lambda,(id,None),res)) @@ -100,16 +105,29 @@ let mk_elim uri leftno [it] (outsort,suffix) = k_names @ List.map (fun _ -> CicNotationPt.Implicit `JustOne) (List.tl args) @ - [mk_appl (name::abs)]))) - | _ -> mk_id name,None - ) cargs in + [mk_appl (name::abs)]))))::acc, nih + 1 + | _ -> (mk_id name,None)::acc,nih + ) ([],0) cargs in + let cargs_and_recursive_args, nih = cargs_recargs_nih in let cargs,recursive_args = List.split cargs_and_recursive_args in let recursive_args = HExtlib.filter_map (fun x -> x) recursive_args in - CicNotationPt.Pattern (name,None,List.map (fun x -> x,None) cargs), - mk_appl (name_of_k name :: cargs @ recursive_args) + (CicNotationPt.Pattern (name,None,List.map (fun x -> x,None) cargs), + mk_appl (name_of_k name :: cargs @ recursive_args)), (name,cargs, nih) ) cl in - let bo = CicNotationPt.Case (rec_arg,Some (ind_name,None),None,branches) in + let branches, branch_args = List.split branches_with_args in + let bo = CicNotationPt.Case (rec_arg,Some (ind_name,None),Some p_name,branches) in + let final_params = + List.map (function name -> name, None) params @ + [p_name,Some p_ty] @ + List.map (function name, cargs, nih -> + name_of_k name, + Some (mk_prods cargs (mk_arrs nih + (mk_appl + (p_name::HExtlib.mk_list (CicNotationPt.Implicit `JustOne) + (List.length args - 1) @ + [mk_appl (mk_id name :: params @ cargs)]))))) branch_args @ + List.map (function name -> name, None) args in let recno = List.length final_params in let where = recno - 1 in let res = @@ -149,29 +167,35 @@ let mk_elim uri leftno [it] (outsort,suffix) = (CicNotationPres.mpres_of_box boxml))); *) CicNotationPt.Theorem - (`Definition,srec_name,CicNotationPt.Implicit `JustOne,Some res) + (`Definition,srec_name, + CicNotationPt.Implicit `JustOne,Some res,pragma) ;; let ast_of_sort s = + let headrm prefix s = + try + let len_prefix = String.length prefix in + assert (String.sub s 0 len_prefix = prefix); + String.sub s len_prefix (String.length s - len_prefix) + with Invalid_argument _ -> assert false + in 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) + | NCic.Prop -> `Prop,"ind" + | NCic.Type [] -> `NType "", "rect_Type" + | NCic.Type ((`Type,u) :: _) -> + let name = NUri.name_of_uri u in + `NType (headrm "Type" name), "rect_" ^ name + | NCic.Type ((`CProp,u) :: _) -> + let name = NUri.name_of_uri u in + `NCProp (headrm "Type" name), + "rect_" ^ Str.replace_first (Str.regexp "Type") "CProp" name + | _ -> assert false ;; let mk_elims (uri,_,_,_,obj) = match obj with - NCic.Inductive (true,leftno,itl,_) -> - List.map (fun s -> mk_elim uri leftno itl (ast_of_sort s)) + NCic.Inductive (true,leftno,[itl],_) -> + List.map (fun s -> mk_elim uri leftno itl (ast_of_sort s) (`Elim s)) (NCic.Prop:: List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes ())) | _ -> [] @@ -284,7 +308,7 @@ let mk_projection leftno tyname consname consty (projname,_,_) i = 80 (CicNotationPres.render (fun _ -> None) (TermContentPres.pp_ast res)));*) CicNotationPt.Theorem - (`Definition,projname,CicNotationPt.Implicit `JustOne,Some res) + (`Definition,projname,CicNotationPt.Implicit `JustOne,Some res,`Projection) ;; let mk_projections (_,_,_,_,obj) =