diff options
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 600 |
1 files changed, 300 insertions, 300 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 46da3a01d..7cce53c7c 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -7,13 +7,13 @@ open Libnames open Rawterm open Declarations -let is_rec_info scheme_info = - let test_branche min acc (_,_,br) = +let is_rec_info scheme_info = + let test_branche min acc (_,_,br) = acc || ( - let new_branche = - it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum br)) in - let free_rels_in_br = Termops.free_rels new_branche in - let max = min + scheme_info.Tactics.npredicates in + let new_branche = + it_mkProd_or_LetIn mkProp (fst (decompose_prod_assum br)) in + let free_rels_in_br = Termops.free_rels new_branche in + let max = min + scheme_info.Tactics.npredicates in Util.Intset.exists (fun i -> i >= min && i< max) free_rels_in_br ) in @@ -28,38 +28,38 @@ let choose_dest_or_ind scheme_info = let functional_induction with_clean c princl pat = Dumpglob.pause (); - let res = let f,args = decompose_app c in - fun g -> - let princ,bindings, princ_type = - match princl with + let res = let f,args = decompose_app c in + fun g -> + let princ,bindings, princ_type = + match princl with | None -> (* No principle is given let's find the good one *) begin match kind_of_term f with | Const c' -> - let princ_option = + let princ_option = let finfo = (* we first try to find out a graph on f *) - try find_Function_infos c' - with Not_found -> + try find_Function_infos c' + with Not_found -> errorlabstrm "" (str "Cannot find induction information on "++ Printer.pr_lconstr (mkConst c') ) in - match Tacticals.elimination_sort_of_goal g with + match Tacticals.elimination_sort_of_goal g with | InProp -> finfo.prop_lemma | InSet -> finfo.rec_lemma | InType -> finfo.rect_lemma in let princ = (* then we get the principle *) try mkConst (Option.get princ_option ) - with Option.IsNone -> - (*i If there is not default lemma defined then, - we cross our finger and try to find a lemma named f_ind + with Option.IsNone -> + (*i If there is not default lemma defined then, + we cross our finger and try to find a lemma named f_ind (or f_rec, f_rect) i*) - let princ_name = + let princ_name = Indrec.make_elimination_ident (id_of_label (con_label c')) (Tacticals.elimination_sort_of_goal g) in - try + try mkConst(const_of_id princ_name ) with Not_found -> (* This one is neither defined ! *) errorlabstrm "" (str "Cannot find induction principle for " @@ -67,57 +67,57 @@ let functional_induction with_clean c princl pat = in (princ,Rawterm.NoBindings, Tacmach.pf_type_of g princ) | _ -> raise (UserError("",str "functional induction must be used with a function" )) - + end - | Some ((princ,binding)) -> + | Some ((princ,binding)) -> princ,binding,Tacmach.pf_type_of g princ in - let princ_infos = Tactics.compute_elim_sig princ_type in + let princ_infos = Tactics.compute_elim_sig princ_type in let args_as_induction_constr = - let c_list = - if princ_infos.Tactics.farg_in_concl - then [c] else [] + let c_list = + if princ_infos.Tactics.farg_in_concl + then [c] else [] in - List.map (fun c -> Tacexpr.ElimOnConstr (c,NoBindings)) (args@c_list) - in - let princ' = Some (princ,bindings) in - let princ_vars = - List.fold_right - (fun a acc -> + List.map (fun c -> Tacexpr.ElimOnConstr (c,NoBindings)) (args@c_list) + in + let princ' = Some (princ,bindings) in + let princ_vars = + List.fold_right + (fun a acc -> try Idset.add (destVar a) acc with _ -> acc ) args Idset.empty in - let old_idl = List.fold_right Idset.add (Tacmach.pf_ids_of_hyps g) Idset.empty in - let old_idl = Idset.diff old_idl princ_vars in - let subst_and_reduce g = - if with_clean + let old_idl = List.fold_right Idset.add (Tacmach.pf_ids_of_hyps g) Idset.empty in + let old_idl = Idset.diff old_idl princ_vars in + let subst_and_reduce g = + if with_clean then - let idl = - map_succeed - (fun id -> + let idl = + map_succeed + (fun id -> if Idset.mem id old_idl then failwith "subst_and_reduce"; - id + id ) (Tacmach.pf_ids_of_hyps g) - in - let flag = + in + let flag = Rawterm.Cbv - {Rawterm.all_flags - with Rawterm.rDelta = false; + {Rawterm.all_flags + with Rawterm.rDelta = false; } in Tacticals.tclTHEN (Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Equality.subst [id])) idl ) - (Hiddentac.h_reduce flag Tacticals.allHypsAndConcl) + (Hiddentac.h_reduce flag Tacticals.allHypsAndConcl) g - else Tacticals.tclIDTAC g - + else Tacticals.tclIDTAC g + in Tacticals.tclTHEN - (choose_dest_or_ind + (choose_dest_or_ind princ_infos args_as_induction_constr princ' @@ -128,12 +128,12 @@ let functional_induction with_clean c princl pat = in Dumpglob.continue (); res - - -type annot = - Struct of identifier + + +type annot = + Struct of identifier | Wf of Topconstr.constr_expr * identifier option * Topconstr.constr_expr list | Mes of Topconstr.constr_expr * identifier option * Topconstr.constr_expr list @@ -150,12 +150,12 @@ let rec abstract_rawconstr c = function let interp_casted_constr_with_implicits sigma env impls c = (* Constrintern.interp_rawconstr_with_implicits sigma env [] impls c *) - Constrintern.intern_gen false sigma env ~impls:([],impls) + Constrintern.intern_gen false sigma env ~impls:([],impls) ~allow_patvar:false ~ltacvars:([],[]) c -(* - Construct a fixpoint as a Rawterm +(* + Construct a fixpoint as a Rawterm and not as a constr *) let build_newrecursive @@ -192,7 +192,7 @@ let build_newrecursive States.unfreeze fs; def in recdef,rec_impls - + let compute_annot (name,annot,args,types,body) = let names = List.map snd (Topconstr.names_of_local_assums args) in @@ -207,124 +207,124 @@ let compute_annot (name,annot,args,types,body) = | Some r -> (name,r,args,types,body) -(* Checks whether or not the mutual bloc is recursive *) -let rec is_rec names = - let names = List.fold_right Idset.add names Idset.empty in - let check_id id names = Idset.mem id names in - let rec lookup names = function +(* Checks whether or not the mutual bloc is recursive *) +let rec is_rec names = + let names = List.fold_right Idset.add names Idset.empty in + let check_id id names = Idset.mem id names in + let rec lookup names = function | RVar(_,id) -> check_id id names | RRef _ | REvar _ | RPatVar _ | RSort _ | RHole _ | RDynamic _ -> false | RCast(_,b,_) -> lookup names b | RRec _ -> error "RRec not handled" - | RIf(_,b,_,lhs,rhs) -> + | RIf(_,b,_,lhs,rhs) -> (lookup names b) || (lookup names lhs) || (lookup names rhs) - | RLetIn(_,na,t,b) | RLambda(_,na,_,t,b) | RProd(_,na,_,t,b) -> + | RLetIn(_,na,t,b) | RLambda(_,na,_,t,b) | RProd(_,na,_,t,b) -> lookup names t || lookup (Nameops.name_fold Idset.remove na names) b - | RLetTuple(_,nal,_,t,b) -> lookup names t || - lookup - (List.fold_left + | RLetTuple(_,nal,_,t,b) -> lookup names t || + lookup + (List.fold_left (fun acc na -> Nameops.name_fold Idset.remove na acc) names nal ) b | RApp(_,f,args) -> List.exists (lookup names) (f::args) - | RCases(_,_,_,el,brl) -> + | RCases(_,_,_,el,brl) -> List.exists (fun (e,_) -> lookup names e) el || List.exists (lookup_br names) brl - and lookup_br names (_,idl,_,rt) = - let new_names = List.fold_right Idset.remove idl names in + and lookup_br names (_,idl,_,rt) = + let new_names = List.fold_right Idset.remove idl names in lookup new_names rt in lookup names -let prepare_body (name,annot,args,types,body) rt = - let n = (Topconstr.local_binders_length args) in +let prepare_body (name,annot,args,types,body) rt = + let n = (Topconstr.local_binders_length args) in (* Pp.msgnl (str "nb lambda to chop : " ++ str (string_of_int n) ++ fnl () ++Printer.pr_rawconstr rt); *) let fun_args,rt' = chop_rlambda_n n rt in (fun_args,rt') let derive_inversion fix_names = - try + try (* we first transform the fix_names identifier into their corresponding constant *) - let fix_names_as_constant = - List.map (fun id -> destConst (Tacinterp.constr_of_id (Global.env ()) id)) fix_names - in - (* - Then we check that the graphs have been defined - If one of the graphs haven't been defined + let fix_names_as_constant = + List.map (fun id -> destConst (Tacinterp.constr_of_id (Global.env ()) id)) fix_names + in + (* + Then we check that the graphs have been defined + If one of the graphs haven't been defined we do nothing *) List.iter (fun c -> ignore (find_Function_infos c)) fix_names_as_constant ; try - Invfun.derive_correctness + Invfun.derive_correctness Functional_principles_types.make_scheme - functional_induction + functional_induction fix_names_as_constant - (*i The next call to mk_rel_id is valid since we have just construct the graph + (*i The next call to mk_rel_id is valid since we have just construct the graph Ensures by : register_built - i*) + i*) (List.map (fun id -> destInd (Tacinterp.constr_of_id (Global.env ()) (mk_rel_id id))) fix_names ) - with e -> - msg_warning - (str "Cannot built inversion information" ++ + with e -> + msg_warning + (str "Cannot built inversion information" ++ if do_observe () then Cerrors.explain_exn e else mt ()) with _ -> () -let warning_error names e = - let e_explain e = - match e with +let warning_error names e = + let e_explain e = + match e with | ToShow e -> spc () ++ Cerrors.explain_exn e | _ -> if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt () - in - match e with - | Building_graph e -> - Pp.msg_warning - (str "Cannot define graph(s) for " ++ + in + match e with + | Building_graph e -> + Pp.msg_warning + (str "Cannot define graph(s) for " ++ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ e_explain e) - | Defining_principle e -> + | Defining_principle e -> Pp.msg_warning - (str "Cannot define principle(s) for "++ + (str "Cannot define principle(s) for "++ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ e_explain e) | _ -> anomaly "" -let error_error names e = - let e_explain e = - match e with +let error_error names e = + let e_explain e = + match e with | ToShow e -> spc () ++ Cerrors.explain_exn e | _ -> if do_observe () then (spc () ++ Cerrors.explain_exn e) else mt () in - match e with - | Building_graph e -> - errorlabstrm "" - (str "Cannot define graph(s) for " ++ + match e with + | Building_graph e -> + errorlabstrm "" + (str "Cannot define graph(s) for " ++ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++ e_explain e) | _ -> anomaly "" let generate_principle on_error - is_general do_built fix_rec_l recdefs interactive_proof - (continue_proof : int -> Names.constant array -> Term.constr array -> int -> + is_general do_built fix_rec_l recdefs interactive_proof + (continue_proof : int -> Names.constant array -> Term.constr array -> int -> Tacmach.tactic) : unit = let names = List.map (function ((_, name),_,_,_,_) -> name) fix_rec_l in let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in let funs_args = List.map fst fun_bodies in let funs_types = List.map (function (_,_,_,types,_) -> types) fix_rec_l in - try + try (* We then register the Inductive graphs of the functions *) Rawterm_to_relation.build_inductive names funs_args funs_types recdefs; - if do_built + if do_built then begin - (*i The next call to mk_rel_id is valid since we have just construct the graph + (*i The next call to mk_rel_id is valid since we have just construct the graph Ensures by : do_built - i*) + i*) let f_R_mut = Ident (dummy_loc,mk_rel_id (List.nth names 0)) in let ind_kn = fst (locate_with_msg @@ -339,34 +339,34 @@ let generate_principle on_error locate_constant f_ref in - let funs_kn = Array.of_list (List.map fname_kn fix_rec_l) in - let _ = + let funs_kn = Array.of_list (List.map fname_kn fix_rec_l) in + let _ = list_map_i (fun i x -> - let princ = destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)) in + let princ = destConst (Indrec.lookup_eliminator (ind_kn,i) (InProp)) in let princ_type = Typeops.type_of_constant (Global.env()) princ in Functional_principles_types.generate_functional_principle - interactive_proof + interactive_proof princ_type None - None + None funs_kn i - (continue_proof 0 [|funs_kn.(i)|]) + (continue_proof 0 [|funs_kn.(i)|]) ) 0 fix_rec_l - in + in Array.iter (add_Function is_general) funs_kn; () end - with e -> - on_error names e + with e -> + on_error names e -let register_struct is_rec fixpoint_exprl = - match fixpoint_exprl with - | [((_,fname),_,bl,ret_type,body),_] when not is_rec -> +let register_struct is_rec fixpoint_exprl = + match fixpoint_exprl with + | [((_,fname),_,bl,ret_type,body),_] when not is_rec -> Command.declare_definition fname (Decl_kinds.Global,Flags.boxed_definitions (),Decl_kinds.Definition) @@ -375,65 +375,65 @@ let register_struct is_rec fixpoint_exprl = body (Some ret_type) (fun _ _ -> ()) - | _ -> + | _ -> Command.build_recursive fixpoint_exprl (Flags.boxed_definitions()) -let generate_correction_proof_wf f_ref tcc_lemma_ref +let generate_correction_proof_wf f_ref tcc_lemma_ref is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation - (_: int) (_:Names.constant array) (_:Term.constr array) (_:int) : Tacmach.tactic = + (_: int) (_:Names.constant array) (_:Term.constr array) (_:int) : Tacmach.tactic = Functional_principles_proofs.prove_principle_for_gen (f_ref,functional_ref,eq_ref) tcc_lemma_ref is_mes rec_arg_num rec_arg_type relation let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body - pre_hook - = - let type_of_f = Command.generalize_constr_expr ret_type args in - let rec_arg_num = - let names = + pre_hook + = + let type_of_f = Command.generalize_constr_expr ret_type args in + let rec_arg_num = + let names = List.map snd - (Topconstr.names_of_local_assums args) - in - match wf_arg with - | None -> + (Topconstr.names_of_local_assums args) + in + match wf_arg with + | None -> if List.length names = 1 then 1 else error "Recursive argument must be specified" - | Some wf_arg -> - list_index (Name wf_arg) names + | Some wf_arg -> + list_index (Name wf_arg) names in - let unbounded_eq = - let f_app_args = - Topconstr.CAppExpl - (dummy_loc, + let unbounded_eq = + let f_app_args = + Topconstr.CAppExpl + (dummy_loc, (None,(Ident (dummy_loc,fname))) , - (List.map + (List.map (function - | _,Anonymous -> assert false + | _,Anonymous -> assert false | _,Name e -> (Topconstr.mkIdentC e) - ) + ) (Topconstr.names_of_local_assums args) ) - ) + ) in Topconstr.CApp (dummy_loc,(None,Topconstr.mkRefC (Qualid (dummy_loc,(qualid_of_string "Logic.eq")))), [(f_app_args,None);(body,None)]) in - let eq = Command.generalize_constr_expr unbounded_eq args in + let eq = Command.generalize_constr_expr unbounded_eq args in let hook f_ref tcc_lemma_ref functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation = - try - pre_hook + try + pre_hook (generate_correction_proof_wf f_ref tcc_lemma_ref is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation ); derive_inversion [fname] - with e -> - (* No proof done *) + with e -> + (* No proof done *) () - in - Recdef.recursive_definition + in + Recdef.recursive_definition is_mes fname rec_impls type_of_f wf_rel_expr @@ -442,115 +442,115 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas hook using_lemmas - -let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type body = - let wf_arg_type,wf_arg = - match wf_arg with - | None -> + +let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type body = + let wf_arg_type,wf_arg = + match wf_arg with + | None -> begin - match args with - | [Topconstr.LocalRawAssum ([(_,Name x)],k,t)] -> t,x - | _ -> error "Recursive argument must be specified" + match args with + | [Topconstr.LocalRawAssum ([(_,Name x)],k,t)] -> t,x + | _ -> error "Recursive argument must be specified" end - | Some wf_args -> - try - match - List.find - (function - | Topconstr.LocalRawAssum(l,k,t) -> - List.exists - (function (_,Name id) -> id = wf_args | _ -> false) - l + | Some wf_args -> + try + match + List.find + (function + | Topconstr.LocalRawAssum(l,k,t) -> + List.exists + (function (_,Name id) -> id = wf_args | _ -> false) + l | _ -> false ) - args - with + args + with | Topconstr.LocalRawAssum(_,k,t) -> t,wf_args - | _ -> assert false - with Not_found -> assert false + | _ -> assert false + with Not_found -> assert false in - let ltof = - let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) in - Libnames.Qualid (dummy_loc,Libnames.qualid_of_path + let ltof = + let make_dir l = make_dirpath (List.map id_of_string (List.rev l)) in + Libnames.Qualid (dummy_loc,Libnames.qualid_of_path (Libnames.make_path (make_dir ["Arith";"Wf_nat"]) (id_of_string "ltof"))) in - let fun_from_mes = - let applied_mes = + let fun_from_mes = + let applied_mes = Topconstr.mkAppC(wf_mes_expr,[Topconstr.mkIdentC wf_arg]) in - Topconstr.mkLambdaC ([(dummy_loc,Name wf_arg)],Topconstr.default_binder_kind,wf_arg_type,applied_mes) + Topconstr.mkLambdaC ([(dummy_loc,Name wf_arg)],Topconstr.default_binder_kind,wf_arg_type,applied_mes) in - let wf_rel_from_mes = + let wf_rel_from_mes = Topconstr.mkAppC(Topconstr.mkRefC ltof,[wf_arg_type;fun_from_mes]) in - register_wf ~is_mes:true fname rec_impls wf_rel_from_mes (Some wf_arg) + register_wf ~is_mes:true fname rec_impls wf_rel_from_mes (Some wf_arg) using_lemmas args ret_type body - - -let do_generate_principle on_error register_built interactive_proof fixpoint_exprl = - let recdefs,rec_impls = build_newrecursive fixpoint_exprl in - let _is_struct = - match fixpoint_exprl with - | [(((_,name),Some (Wf (wf_rel,wf_x,using_lemmas)),args,types,body))] -> - let pre_hook = - generate_principle + + +let do_generate_principle on_error register_built interactive_proof fixpoint_exprl = + let recdefs,rec_impls = build_newrecursive fixpoint_exprl in + let _is_struct = + match fixpoint_exprl with + | [(((_,name),Some (Wf (wf_rel,wf_x,using_lemmas)),args,types,body))] -> + let pre_hook = + generate_principle on_error true register_built - fixpoint_exprl + fixpoint_exprl recdefs true - in - if register_built + in + if register_built then register_wf name rec_impls wf_rel wf_x using_lemmas args types body pre_hook; false - | [(((_,name),Some (Mes (wf_mes,wf_x,using_lemmas)),args,types,body))] -> - let pre_hook = - generate_principle + | [(((_,name),Some (Mes (wf_mes,wf_x,using_lemmas)),args,types,body))] -> + let pre_hook = + generate_principle on_error true register_built - fixpoint_exprl + fixpoint_exprl recdefs true - in - if register_built + in + if register_built then register_mes name rec_impls wf_mes wf_x using_lemmas args types body pre_hook; true - | _ -> - let fix_names = - List.map (function ((_,name),_,_,_,_) -> name) fixpoint_exprl + | _ -> + let fix_names = + List.map (function ((_,name),_,_,_,_) -> name) fixpoint_exprl in let is_one_rec = is_rec fix_names in - let old_fixpoint_exprl = + let old_fixpoint_exprl = List.map (function - | (name,Some (Struct id),args,types,body),_ -> - let annot = - try Some (dummy_loc, id), Topconstr.CStructRec - with Not_found -> - raise (UserError("",str "Cannot find argument " ++ - Ppconstr.pr_id id)) - in - (name,annot,args,types,body),(None:Vernacexpr.decl_notation) - | (name,None,args,types,body),recdef -> + | (name,Some (Struct id),args,types,body),_ -> + let annot = + try Some (dummy_loc, id), Topconstr.CStructRec + with Not_found -> + raise (UserError("",str "Cannot find argument " ++ + Ppconstr.pr_id id)) + in + (name,annot,args,types,body),(None:Vernacexpr.decl_notation) + | (name,None,args,types,body),recdef -> let names = (Topconstr.names_of_local_assums args) in if is_one_rec recdef && List.length names > 1 then user_err_loc (dummy_loc,"Function", Pp.str "the recursive argument needs to be specified in Function") - else + else let loc, na = List.hd names in (name,(Some (loc, Nameops.out_name na), Topconstr.CStructRec),args,types,body), (None:Vernacexpr.decl_notation) - | (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_-> - error + | (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_-> + error ("Cannot use mutual definition with well-founded recursion or measure") - ) + ) (List.combine fixpoint_exprl recdefs) in - (* ok all the expressions are structural *) - let fix_names = - List.map (function ((_,name),_,_,_,_) -> name) fixpoint_exprl + (* ok all the expressions are structural *) + let fix_names = + List.map (function ((_,name),_,_,_,_) -> name) fixpoint_exprl in let is_rec = List.exists (is_rec fix_names) recdefs in if register_built then register_struct is_rec old_fixpoint_exprl; @@ -559,7 +559,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp false register_built fixpoint_exprl - recdefs + recdefs interactive_proof (Functional_principles_proofs.prove_princ_for_struct interactive_proof); if register_built then derive_inversion fix_names; @@ -568,52 +568,52 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp () open Topconstr -let rec add_args id new_args b = - match b with - | CRef r -> - begin match r with - | Libnames.Ident(loc,fname) when fname = id -> +let rec add_args id new_args b = + match b with + | CRef r -> + begin match r with + | Libnames.Ident(loc,fname) when fname = id -> CAppExpl(dummy_loc,(None,r),new_args) | _ -> b end | CFix _ | CCoFix _ -> anomaly "add_args : todo" - | CArrow(loc,b1,b2) -> + | CArrow(loc,b1,b2) -> CArrow(loc,add_args id new_args b1, add_args id new_args b2) - | CProdN(loc,nal,b1) -> + | CProdN(loc,nal,b1) -> CProdN(loc, - List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, + List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, add_args id new_args b1) - | CLambdaN(loc,nal,b1) -> + | CLambdaN(loc,nal,b1) -> CLambdaN(loc, - List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, + List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, add_args id new_args b1) - | CLetIn(loc,na,b1,b2) -> + | CLetIn(loc,na,b1,b2) -> CLetIn(loc,na,add_args id new_args b1,add_args id new_args b2) - | CAppExpl(loc,(pf,r),exprl) -> - begin - match r with - | Libnames.Ident(loc,fname) when fname = id -> + | CAppExpl(loc,(pf,r),exprl) -> + begin + match r with + | Libnames.Ident(loc,fname) when fname = id -> CAppExpl(loc,(pf,r),new_args@(List.map (add_args id new_args) exprl)) | _ -> CAppExpl(loc,(pf,r),List.map (add_args id new_args) exprl) end - | CApp(loc,(pf,b),bl) -> - CApp(loc,(pf,add_args id new_args b), + | CApp(loc,(pf,b),bl) -> + CApp(loc,(pf,add_args id new_args b), List.map (fun (e,o) -> add_args id new_args e,o) bl) - | CCases(loc,sty,b_option,cel,cal) -> + | CCases(loc,sty,b_option,cel,cal) -> CCases(loc,sty,Option.map (add_args id new_args) b_option, - List.map (fun (b,(na,b_option)) -> + List.map (fun (b,(na,b_option)) -> add_args id new_args b, - (na,Option.map (add_args id new_args) b_option)) cel, + (na,Option.map (add_args id new_args) b_option)) cel, List.map (fun (loc,cpl,e) -> (loc,cpl,add_args id new_args e)) cal ) - | CLetTuple(loc,nal,(na,b_option),b1,b2) -> + | CLetTuple(loc,nal,(na,b_option),b1,b2) -> CLetTuple(loc,nal,(na,Option.map (add_args id new_args) b_option), add_args id new_args b1, add_args id new_args b2 ) - - | CIf(loc,b1,(na,b_option),b2,b3) -> - CIf(loc,add_args id new_args b1, + + | CIf(loc,b1,(na,b_option),b2,b3) -> + CIf(loc,add_args id new_args b1, (na,Option.map (add_args id new_args) b_option), add_args id new_args b2, add_args id new_args b3 @@ -622,7 +622,7 @@ let rec add_args id new_args b = | CPatVar _ -> b | CEvar _ -> b | CSort _ -> b - | CCast(loc,b1,CastConv(ck,b2)) -> + | CCast(loc,b1,CastConv(ck,b2)) -> CCast(loc,add_args id new_args b1,CastConv(ck,add_args id new_args b2)) | CCast(loc,b1,CastCoerce) -> CCast(loc,add_args id new_args b1,CastCoerce) @@ -635,70 +635,70 @@ let rec add_args id new_args b = exception Stop of Topconstr.constr_expr -(* [chop_n_arrow n t] chops the [n] first arrows in [t] - Acts on Topconstr.constr_expr +(* [chop_n_arrow n t] chops the [n] first arrows in [t] + Acts on Topconstr.constr_expr *) -let rec chop_n_arrow n t = - if n <= 0 +let rec chop_n_arrow n t = + if n <= 0 then t (* If we have already removed all the arrows then return the type *) - else (* If not we check the form of [t] *) - match t with + else (* If not we check the form of [t] *) + match t with | Topconstr.CArrow(_,_,t) -> (* If we have an arrow, we discard it and recall [chop_n_arrow] *) chop_n_arrow (n-1) t - | Topconstr.CProdN(_,nal_ta',t') -> (* If we have a forall, to result are possible : + | Topconstr.CProdN(_,nal_ta',t') -> (* If we have a forall, to result are possible : either we need to discard more than the number of arrows contained in this product declaration then we just recall [chop_n_arrow] on - the remaining number of arrow to chop and [t'] we discard it and - recall [chop_n_arrow], either this product contains more arrows + the remaining number of arrow to chop and [t'] we discard it and + recall [chop_n_arrow], either this product contains more arrows than the number we need to chop and then we return the new type *) - begin - try + begin + try let new_n = - let rec aux (n:int) = function + let rec aux (n:int) = function [] -> n - | (nal,k,t'')::nal_ta' -> - let nal_l = List.length nal in + | (nal,k,t'')::nal_ta' -> + let nal_l = List.length nal in if n >= nal_l - then + then aux (n - nal_l) nal_ta' - else - let new_t' = + else + let new_t' = Topconstr.CProdN(dummy_loc, ((snd (list_chop n nal)),k,t'')::nal_ta',t') - in + in raise (Stop new_t') in aux n nal_ta' - in + in chop_n_arrow new_n t' with Stop t -> t end | _ -> anomaly "Not enough products" - -let rec get_args b t : Topconstr.local_binder list * - Topconstr.constr_expr * Topconstr.constr_expr = - match b with - | Topconstr.CLambdaN (loc, (nal_ta), b') -> + +let rec get_args b t : Topconstr.local_binder list * + Topconstr.constr_expr * Topconstr.constr_expr = + match b with + | Topconstr.CLambdaN (loc, (nal_ta), b') -> begin - let n = - (List.fold_left (fun n (nal,_,_) -> + let n = + (List.fold_left (fun n (nal,_,_) -> n+List.length nal) 0 nal_ta ) in - let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in - (List.map (fun (nal,k,ta) -> - (Topconstr.LocalRawAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t'' + let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in + (List.map (fun (nal,k,ta) -> + (Topconstr.LocalRawAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t'' end | _ -> [],b,t let make_graph (f_ref:global_reference) = - let c,c_body = - match f_ref with - | ConstRef c -> - begin try c,Global.lookup_constant c - with Not_found -> + let c,c_body = + match f_ref with + | ConstRef c -> + begin try c,Global.lookup_constant c + with Not_found -> raise (UserError ("",str "Cannot find " ++ Printer.pr_lconstr (mkConst c)) ) end | _ -> raise (UserError ("", str "Not a function reference") ) @@ -710,10 +710,10 @@ let make_graph (f_ref:global_reference) = | Some b -> let env = Global.env () in let body = (force b) in - let extern_body,extern_type = - with_full_print - (fun () -> - (Constrextern.extern_constr false env body, + let extern_body,extern_type = + with_full_print + (fun () -> + (Constrextern.extern_constr false env body, Constrextern.extern_type false env (Typeops.type_of_constant_type env c_body.const_type) ) @@ -721,48 +721,48 @@ let make_graph (f_ref:global_reference) = () in let (nal_tas,b,t) = get_args extern_body extern_type in - let expr_list = - match b with - | Topconstr.CFix(loc,l_id,fixexprl) -> - let l = + let expr_list = + match b with + | Topconstr.CFix(loc,l_id,fixexprl) -> + let l = List.map - (fun (id,(n,recexp),bl,t,b) -> + (fun (id,(n,recexp),bl,t,b) -> let loc, rec_id = Option.get n in - let new_args = - List.flatten - (List.map + let new_args = + List.flatten + (List.map (function | Topconstr.LocalRawDef (na,_)-> [] - | Topconstr.LocalRawAssum (nal,_,_) -> - List.map - (fun (loc,n) -> - CRef(Libnames.Ident(loc, Nameops.out_name n))) + | Topconstr.LocalRawAssum (nal,_,_) -> + List.map + (fun (loc,n) -> + CRef(Libnames.Ident(loc, Nameops.out_name n))) nal ) nal_tas ) in - let b' = add_args (snd id) new_args b in + let b' = add_args (snd id) new_args b in (id, Some (Struct rec_id),nal_tas@bl,t,b') ) fixexprl in l - | _ -> - let id = id_of_label (con_label c) in + | _ -> + let id = id_of_label (con_label c) in [((dummy_loc,id),None,nal_tas,t,b)] in do_generate_principle error_error false false expr_list; (* We register the infos *) - let mp,dp,_ = repr_con c in - List.iter - (fun ((_,id),_,_,_,_) -> add_Function false (make_con mp dp (label_of_id id))) + let mp,dp,_ = repr_con c in + List.iter + (fun ((_,id),_,_,_,_) -> add_Function false (make_con mp dp (label_of_id id))) expr_list); Dumpglob.continue () - + (* let make_graph _ = assert false *) - -let do_generate_principle = do_generate_principle warning_error true + +let do_generate_principle = do_generate_principle warning_error true |