diff options
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/ccalgo.ml | 20 | ||||
| -rw-r--r-- | plugins/cc/cctac.ml | 15 | ||||
| -rw-r--r-- | plugins/cc/g_congruence.mlg (renamed from plugins/cc/g_congruence.ml4) | 14 |
3 files changed, 28 insertions, 21 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 8e53a044..f26ec0f4 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -26,6 +26,10 @@ let init_size=5 let cc_verbose=ref false +let print_constr t = + let sigma, env = Pfedit.get_current_context () in + Printer.pr_econstr_env env sigma t + let debug x = if !cc_verbose then Feedback.msg_debug (x ()) @@ -130,8 +134,8 @@ type cinfo= ci_nhyps: int} (* # projectable args *) let family_eq f1 f2 = match f1, f2 with - | Prop Pos, Prop Pos - | Prop Null, Prop Null + | Set, Set + | Prop, Prop | Type _, Type _ -> true | _ -> false @@ -457,10 +461,10 @@ let rec canonize_name sigma c = | LetIn (na,b,t,ct) -> mkLetIn (na, func b,func t,func ct) | App (ct,l) -> - mkApp (func ct,Array.smartmap func l) + mkApp (func ct,Array.Smart.map func l) | Proj(p,c) -> let p' = Projection.map (fun kn -> - Constant.make1 (Constant.canonical kn)) p in + MutInd.make1 (MutInd.canonical kn)) p in (mkProj (p', func c)) | _ -> c @@ -483,10 +487,10 @@ let rec inst_pattern subst = function args t let pr_idx_term uf i = str "[" ++ int i ++ str ":=" ++ - Termops.print_constr (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]" + print_constr (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]" let pr_term t = str "[" ++ - Termops.print_constr (EConstr.of_constr (constr_of_term t)) ++ str "]" + print_constr (EConstr.of_constr (constr_of_term t)) ++ str "]" let rec add_term state t= let uf=state.uf in @@ -601,7 +605,7 @@ let add_inst state (inst,int_subst) = begin debug (fun () -> (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++ - (str " [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++ + (str " [" ++ print_constr (EConstr.of_constr prf) ++ str " : " ++ pr_term s ++ str " == " ++ pr_term t ++ str "]")); add_equality state prf s t end @@ -609,7 +613,7 @@ let add_inst state (inst,int_subst) = begin debug (fun () -> (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++ - (str " [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++ + (str " [" ++ print_constr (EConstr.of_constr prf) ++ str " : " ++ pr_term s ++ str " <> " ++ pr_term t ++ str "]")); add_disequality state (Hyp prf) s t end diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index d19817e7..2eaa6146 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -49,7 +49,7 @@ let whd_delta env sigma t = (* decompose member of equality in an applicative format *) (** FIXME: evar leak *) -let sf_of env sigma c = e_sort_of env (ref sigma) c +let sf_of env sigma c = snd (sort_of env sigma c) let rec decompose_term env sigma t= match EConstr.kind sigma (whd env sigma t) with @@ -84,13 +84,13 @@ let rec decompose_term env sigma t= let canon_const = Constant.make1 (Constant.canonical c) in (Symb (Constr.mkConstU (canon_const,u))) | Proj (p, c) -> - let canon_const kn = Constant.make1 (Constant.canonical kn) in - let p' = Projection.map canon_const p in + let canon_mind kn = MutInd.make1 (MutInd.canonical kn) in + let p' = Projection.map canon_mind p in let c = Retyping.expand_projection env sigma p' c [] in decompose_term env sigma c | _ -> let t = Termops.strip_outer_cast sigma t in - if closed0 sigma t then Symb (EConstr.to_constr sigma t) else raise Not_found + if closed0 sigma t then Symb (EConstr.to_constr ~abort_on_undefined_evars:false sigma t) else raise Not_found (* decompose equality in members and type *) open Termops @@ -264,9 +264,8 @@ let app_global_with_holes f args n = let ans = mkApp (fc, args) in let (sigma, holes) = gen_holes env sigma t n [] in let ans = applist (ans, holes) in - let evdref = ref sigma in - let () = Typing.e_check env evdref ans concl in - (!evdref, ans) + let sigma = Typing.check env sigma ans concl in + (sigma, ans) end end @@ -444,7 +443,7 @@ let cc_tactic depth additionnal_terms = let open Glob_term in let env = Proofview.Goal.env gl in let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) in - let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None) in + let hole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) in let pr_missing (c, missing) = let c = Detyping.detype Detyping.Now ~lax:true false Id.Set.empty env sigma c in let holes = List.init missing (fun _ -> hole) in diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.mlg index fb013ac1..68505929 100644 --- a/plugins/cc/g_congruence.ml4 +++ b/plugins/cc/g_congruence.mlg @@ -8,22 +8,26 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +{ + open Ltac_plugin open Cctac open Stdarg +} + DECLARE PLUGIN "cc_plugin" (* Tactic registration *) TACTIC EXTEND cc - [ "congruence" ] -> [ congruence_tac 1000 [] ] - |[ "congruence" integer(n) ] -> [ congruence_tac n [] ] - |[ "congruence" "with" ne_constr_list(l) ] -> [ congruence_tac 1000 l ] +| [ "congruence" ] -> { congruence_tac 1000 [] } +| [ "congruence" integer(n) ] -> { congruence_tac n [] } +| [ "congruence" "with" ne_constr_list(l) ] -> { congruence_tac 1000 l } |[ "congruence" integer(n) "with" ne_constr_list(l) ] -> - [ congruence_tac n l ] + { congruence_tac n l } END TACTIC EXTEND f_equal - [ "f_equal" ] -> [ f_equal ] +| [ "f_equal" ] -> { f_equal } END |