From e24cc96a07f8513782d3bc7c2ec2739aa85c04e5 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 17 Jul 2009 13:31:13 +0000 Subject: [PATCH] New suffixes for elimination principles: _ind (towards Prop) _rect_UNIVERSENAME (towards Type) --- .../components/ng_tactics/nCicElim.ml | 231 +++++++++--------- 1 file changed, 121 insertions(+), 110 deletions(-) diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml index 2a02b7d17..350144f9e 100644 --- a/helm/software/components/ng_tactics/nCicElim.ml +++ b/helm/software/components/ng_tactics/nCicElim.ml @@ -41,115 +41,126 @@ let mk_appl = | l -> CicNotationPt.Appl l ;; +let mk_elim uri leftno [it] (outsort,suffix) = + let _,ind_name,ty,cl = it in + let srec_name = ind_name ^ "_" ^ suffix in + let rec_name = mk_id srec_name in + let name_of_k id = mk_id ("H_" ^ id) in + let p_name = mk_id "Q_" in + let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in + let params = List.rev_map (function name,_ -> mk_id name) params in + 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 = + List.fold_right + (fun name res -> CicNotationPt.Binder (`Forall,(name,None),res)) args + (CicNotationPt.Binder + (`Forall, + (rec_arg,Some (mk_appl (mk_id ind_name :: params @ args))), + CicNotationPt.Sort outsort)) 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 recno = List.length final_params in + let cty = mk_appl (p_name :: args) in + let ty = Some cty in + let branches = + 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 + _,NCic.Def _ -> assert false + | name,NCic.Decl ty -> + let context,ty = my_split_prods ~subst:[] [] (-1) ty in + match ty with + | NCic.Const nref + | NCic.Appl (NCic.Const nref::_) + when + let NReference.Ref (uri',_) = nref in + NUri.eq uri uri' + -> + let abs = List.rev_map (fun id,_ -> mk_id id) context in + let name = mk_id name in + name, Some ( + List.fold_right + (fun id res -> + CicNotationPt.Binder (`Lambda,(id,None),res)) + abs + (CicNotationPt.Appl + (rec_name :: + params @ + [p_name] @ + k_names @ + List.map (fun _ -> CicNotationPt.Implicit) + (List.tl args) @ + [mk_appl (name::abs)]))) + | _ -> mk_id name,None + ) cargs 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), + CicNotationPt.Appl (name_of_k name :: cargs @ recursive_args) + ) cl + in + let bo = CicNotationPt.Case (rec_arg,None,None,branches) in + let where = List.length final_params - 1 in + let res = + CicNotationPt.LetRec (`Inductive, + [final_params, (rec_name,ty), bo, where], rec_name) + 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))); + prerr_endline "#####"; + let cobj = ("xxx", [], None, `Joint { + Content.joint_id = "yyy"; + joint_kind = `Recursive [recno]; + joint_defs = + [ `Definition { + Content.def_name = Some srec_name; + def_id = "zzz"; + def_aref = "www"; + def_term = bo; + def_type = + List.fold_right + (fun x t -> CicNotationPt.Binder(`Forall,x,t)) + final_params cty + } + ]; + }) + in + let ids_to_nrefs = Hashtbl.create 1 in + let boxml = Content2pres.ncontent2pres ~ids_to_nrefs cobj in + prerr_endline ( + (BoxPp.render_to_string ~map_unicode_to_tex:false + (function x::_ -> x | _ -> assert false) 80 + (CicNotationPres.mpres_of_box boxml))); + CicNotationPt.Theorem (`Definition,srec_name,CicNotationPt.Implicit,Some res) +;; + let mk_elims (uri,_,_,_,obj) = - match obj with - NCic.Inductive (true,leftno,[it],_) -> - let _,ind_name,ty,cl = it in - let srec_name = ind_name ^ "_rect" in - let rec_name = mk_id srec_name in - let name_of_k id = mk_id ("H_" ^ id) in - let p_name = mk_id "Q_" in - let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in - let params = List.rev_map (function name,_ -> mk_id name) params in - 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 = - List.fold_right - (fun name res -> CicNotationPt.Binder (`Forall,(name,None),res)) args - (CicNotationPt.Binder - (`Forall, - (rec_arg,Some (mk_appl (mk_id ind_name :: params @ args))), - CicNotationPt.Sort (`Type (CicUniv.fresh ())))) 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 recno = List.length final_params in - let cty = mk_appl (p_name :: args) in - let ty = Some cty in - let branches = - 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 - _,NCic.Def _ -> assert false - | name,NCic.Decl ty -> - let context,ty = my_split_prods ~subst:[] [] (-1) ty in - match ty with - | NCic.Const nref - | NCic.Appl (NCic.Const nref::_) - when - let NReference.Ref (uri',_) = nref in - NUri.eq uri uri' - -> - let abs = List.rev_map (fun id,_ -> mk_id id) context in - let name = mk_id name in - name, Some ( - List.fold_right - (fun id res -> - CicNotationPt.Binder (`Lambda,(id,None),res)) - abs - (CicNotationPt.Appl - (rec_name :: - params @ - [p_name] @ - k_names @ - List.map (fun _ -> CicNotationPt.Implicit) - (List.tl args) @ - [mk_appl (name::abs)]))) - | _ -> mk_id name,None - ) cargs 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), - CicNotationPt.Appl (name_of_k name :: cargs @ recursive_args) - ) cl - in - let bo = CicNotationPt.Case (rec_arg,None,None,branches) in - let where = List.length final_params - 1 in - let res = - CicNotationPt.LetRec (`Inductive, - [final_params, (rec_name,ty), bo, where], rec_name) - in - prerr_endline (CicNotationPp.pp_term res); - prerr_endline "#####"; - 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))); - prerr_endline "#####"; - let cobj = ("xxx", [], None, `Joint { - Content.joint_id = "yyy"; - joint_kind = `Recursive [recno]; - joint_defs = - [ `Definition { - Content.def_name = Some srec_name; - def_id = "zzz"; - def_aref = "www"; - def_term = bo; - def_type = - List.fold_right - (fun x t -> CicNotationPt.Binder(`Forall,x,t)) - final_params cty - } - ]; - }) - in - let ids_to_nrefs = Hashtbl.create 1 in - let boxml = Content2pres.ncontent2pres ~ids_to_nrefs cobj in - prerr_endline ( - (BoxPp.render_to_string ~map_unicode_to_tex:false - (function x::_ -> x | _ -> assert false) 80 - (CicNotationPres.mpres_of_box boxml))); - [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 + `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)) + (NCic.Prop:: + List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes ())) + | _ -> [] ;; -- 2.39.2