diff options
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 48 |
1 files changed, 12 insertions, 36 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 6c0c28905..bcfa6b931 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -26,31 +26,6 @@ open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration -(* Some pretty printing function for debugging purpose *) - -let pr_binding prc = - function - | loc, NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) - | loc, AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) - -let pr_bindings prc prlc = function - | ImplicitBindings l -> - brk (1,1) ++ str "with" ++ brk (1,1) ++ - pr_sequence prc l - | ExplicitBindings l -> - brk (1,1) ++ str "with" ++ brk (1,1) ++ - pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l - | NoBindings -> mt () - - -let pr_with_bindings prc prlc (c,bl) = - prc c ++ hv 0 (pr_bindings prc prlc bl) - - - -let pr_constr_with_binding prc (c,bl) : Pp.std_ppcmds = - pr_with_bindings prc prc (c,bl) - (* The local debugging mechanism *) (* let msgnl = Pp.msgnl *) @@ -140,7 +115,7 @@ let generate_type evd g_to_f f graph i = let ctxt,_ = decompose_prod_assum !evd graph_arity in let fun_ctxt,res_type = match ctxt with - | [] | [_] -> anomaly (Pp.str "Not a valid context") + | [] | [_] -> anomaly (Pp.str "Not a valid context.") | decl :: fun_ctxt -> fun_ctxt, RelDecl.get_type decl in let rec args_from_decl i accu = function @@ -197,7 +172,7 @@ let generate_type evd g_to_f f graph i = let find_induction_principle evd f = let f_as_constant,u = match EConstr.kind !evd f with | Const c' -> c' - | _ -> error "Must be used with a function" + | _ -> user_err Pp.(str "Must be used with a function") in let infos = find_Function_infos f_as_constant in match infos.rect_lemma with @@ -273,7 +248,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes List.map (fun decl -> List.map - (fun id -> Loc.ghost, IntroNaming (IntroIdentifier id)) + (fun id -> Loc.tag @@ IntroNaming (IntroIdentifier id)) (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl))))) ) branches @@ -292,7 +267,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes (fun (_,pat) acc -> match pat with | IntroNaming (IntroIdentifier id) -> id::acc - | _ -> anomaly (Pp.str "Not an identifier") + | _ -> anomaly (Pp.str "Not an identifier.") ) (List.nth intro_pats (pred i)) [] @@ -401,7 +376,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes Array.map (fun ((_,(ctxt,concl))) -> match ctxt with - | [] | [_] | [_;_] -> anomaly (Pp.str "bad context") + | [] | [_] | [_;_] -> anomaly (Pp.str "bad context.") | hres::res::decl::ctxt -> let res = EConstr.it_mkLambda_or_LetIn (EConstr.it_mkProd_or_LetIn concl [hres;res]) @@ -421,7 +396,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes let params_bindings,avoid = List.fold_left2 (fun (bindings,avoid) decl p -> - let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in + let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) avoid in p::bindings,id::avoid ) ([],pf_ids_of_hyps g) @@ -431,7 +406,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes let lemmas_bindings = List.rev (fst (List.fold_left2 (fun (bindings,avoid) decl p -> - let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in + let id = Namegen.next_ident_away (Nameops.Name.get_id (RelDecl.get_name decl)) avoid in (nf_zeta p)::bindings,id::avoid) ([],avoid) princ_infos.predicates @@ -546,7 +521,7 @@ and intros_with_rewrite_aux : tactic = intros_with_rewrite ] g end - | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Coqlib.build_coq_False ())) -> + | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ())) -> Proofview.V82.of_tactic tauto g | Case(_,_,v,_) -> tclTHENSEQ[ @@ -701,14 +676,14 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = let graph_def = graphs.(j) in let infos = try find_Function_infos (fst (destConst (project g) funcs.(j))) - with Not_found -> error "No graph found" + with Not_found -> user_err Pp.(str "No graph found") in if infos.is_general || Rtree.is_infinite Declareops.eq_recarg graph_def.mind_recargs then let eq_lemma = try Option.get (infos).equation_lemma - with Option.IsNone -> anomaly (Pp.str "Cannot find equation lemma") + with Option.IsNone -> anomaly (Pp.str "Cannot find equation lemma.") in tclTHENSEQ[ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) ids; @@ -938,7 +913,7 @@ let revert_graph kn post_tac hid g = let info = try find_Function_of_graph ind' with Not_found -> (* The graphs are mutually recursive but we cannot find one of them !*) - anomaly (Pp.str "Cannot retrieve infos about a mutual block") + anomaly (Pp.str "Cannot retrieve infos about a mutual block.") in (* if we can find a completeness lemma for this function then we can come back to the functional form. If not, we do nothing @@ -1006,6 +981,7 @@ let functional_inversion kn hid fconst f_correct : tactic = | _ -> tclFAIL 1 (mt ()) g +let error msg = user_err Pp.(str msg) let invfun qhyp f = let f = |