X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fcomponents%2Fng_tactics%2FnCicElim.ml;h=582f7353b01a5f08441f175c94acb1a907587ee2;hb=53b8e2af661ad4165aa0b1deccd0a7522d96ce2e;hp=bae10cc5630c8b93c905b42de42e88d901232b94;hpb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;p=helm.git diff --git a/matita/components/ng_tactics/nCicElim.ml b/matita/components/ng_tactics/nCicElim.ml index bae10cc56..582f7353b 100644 --- a/matita/components/ng_tactics/nCicElim.ml +++ b/matita/components/ng_tactics/nCicElim.ml @@ -53,30 +53,34 @@ let mk_elim status uri leftno it (outsort,suffix) pragma = let args,sort = NCicReduction.split_prods status ~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 -> NotationPt.Binder (`Forall,(name,None),res)) args + (fun name res -> NotationPt.Binder (`Forall,(name,None),res)) in + let p_ty = mk_prods args (NotationPt.Binder (`Forall, (rec_arg,Some (mk_appl (mk_id ind_name :: params @ args))), NotationPt.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 status ~subst:[] [] leftno ty in let cargs,ty= my_split_prods status ~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 status ~subst:[] [] (-1) ty in @@ -89,7 +93,7 @@ let mk_elim status uri leftno it (outsort,suffix) pragma = -> 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 -> NotationPt.Binder (`Lambda,(id,None),res)) @@ -101,21 +105,35 @@ let mk_elim status uri leftno it (outsort,suffix) pragma = k_names @ List.map (fun _ -> NotationPt.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 - NotationPt.Pattern (name,None,List.map (fun x -> x,None) cargs), - mk_appl (name_of_k name :: cargs @ recursive_args) + (NotationPt.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 = NotationPt.Case (rec_arg,Some (ind_name,None),None,branches) in + let branches, branch_args = List.split branches_with_args in + let bo = NotationPt.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 (NotationPt.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 attrs = `Generated, `Definition, pragma in let res = NotationPt.LetRec (`Inductive, - [final_params, (rec_name,ty), bo, where], rec_name) + [final_params, (rec_name,ty), bo, where], attrs) in (* prerr_endline @@ -149,9 +167,7 @@ let mk_elim status uri leftno it (outsort,suffix) pragma = (function x::_ -> x | _ -> assert false) 80 (NotationPres.mpres_of_box boxml))); *) - NotationPt.Theorem - (`Definition,srec_name, - NotationPt.Implicit `JustOne,Some res,pragma) + res ;; let ast_of_sort s = @@ -208,9 +224,7 @@ let pp (status: #NCic.status) = let rec pp rels = function NCic.Rel i -> List.nth rels (i - 1) - | NCic.Const _ as t -> - NotationPt.Ident - (status#ppterm ~metasenv:[] ~subst:[] ~context:[] t,None) + | NCic.Const _ as t -> NotationPt.NCic t | NCic.Sort s -> NotationPt.Sort (fst (ast_of_sort s)) | NCic.Meta _ | NCic.Implicit _ -> assert false @@ -221,7 +235,7 @@ let pp (status: #NCic.status) = | NCic.Lambda (n,s,t) -> let n = mk_id n in NotationPt.Binder (`Lambda, (n,Some (pp rels s)), pp (n::rels) t) - | NCic.LetIn (n,s,ty,t) -> + | NCic.LetIn (n,ty,s,t) -> let n = mk_id n in NotationPt.LetIn ((n, Some (pp rels ty)), pp rels s, pp (n::rels) t) | NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) -> @@ -284,17 +298,17 @@ let mk_projection status leftno tyname consname consty (projname,_,_) i = in let params,bo = aux [] consty leftno in let pprojname = mk_id projname in + let attrs = `Generated, `Definition, `Projection in let res = NotationPt.LetRec (`Inductive, - [params, (pprojname,None), bo, leftno], pprojname) in + [params, (pprojname,None), bo, leftno], attrs) in (* prerr_endline (BoxPp.render_to_string ~map_unicode_to_tex:false (function x::_ -> x | _ -> assert false) 80 (NotationPres.render (fun _ -> None) (TermContentPres.pp_ast res)));*) - NotationPt.Theorem - (`Definition,projname,NotationPt.Implicit `JustOne,Some res,`Projection) + res ;; let mk_projections status (_,_,_,_,obj) =