diff options
Diffstat (limited to 'tactics/term_dnet.ml')
| -rw-r--r-- | tactics/term_dnet.ml | 57 |
1 files changed, 42 insertions, 15 deletions
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index e4b45489..753c608a 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -1,14 +1,16 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (*i*) open Util -open Term +open Constr open Names open Globnames open Mod_subst @@ -49,7 +51,7 @@ struct | DNil (* debug *) - let pr_dconstr f : 'a t -> std_ppcmds = function + let _pr_dconstr f : 'a t -> Pp.t = function | DRel -> str "*" | DSort -> str "Sort" | DRef _ -> str "Ref" @@ -95,13 +97,20 @@ struct let compare cmp t1 t2 = match t1, t2 with | DRel, DRel -> 0 + | DRel, _ -> -1 | _, DRel -> 1 | DSort, DSort -> 0 + | DSort, _ -> -1 | _, DSort -> 1 | DRef gr1, DRef gr2 -> RefOrdered.compare gr1 gr2 + | DRef _, _ -> -1 | _, DRef _ -> 1 + | DCtx (tl1, tr1), DCtx (tl2, tr2) | DLambda (tl1, tr1), DLambda (tl2, tr2) | DApp (tl1, tr1), DApp (tl2, tr2) -> let c = cmp tl1 tl2 in if c = 0 then cmp tr1 tr2 else c + | DCtx _, _ -> -1 | _, DCtx _ -> 1 + | DLambda _, _ -> -1 | _, DLambda _ -> 1 + | DApp _, _ -> -1 | _, DApp _ -> 1 | DCase (ci1, c1, t1, p1), DCase (ci2, c2, t2, p2) -> let c = cmp c1 c2 in @@ -113,6 +122,7 @@ struct else c else c else c + | DCase _, _ -> -1 | _, DCase _ -> 1 | DFix (i1, j1, tl1, pl1), DFix (i2, j2, tl2, pl2) -> let c = Int.compare j1 j2 in @@ -124,6 +134,8 @@ struct else c else c else c + | DFix _, _ -> -1 | _, DFix _ -> 1 + | DCoFix (i1, tl1, pl1), DCoFix (i2, tl2, pl2) -> let c = Int.compare i1 i2 in if c = 0 then @@ -131,7 +143,18 @@ struct if c = 0 then Array.compare cmp pl1 pl2 else c else c - | _ -> Pervasives.compare t1 t2 (** OK **) + | DCoFix _, _ -> -1 | _, DCoFix _ -> 1 + + | DCons ((t1, ot1), u1), DCons ((t2, ot2), u2) -> + let c = cmp t1 t2 in + if Int.equal c 0 then + let c = Option.compare cmp ot1 ot2 in + if Int.equal c 0 then cmp u1 u2 + else c + else c + | DCons _, _ -> -1 | _, DCons _ -> 1 + + | DNil, DNil -> 0 let fold f acc = function | (DRel | DNil | DSort | DRef _) -> acc @@ -174,7 +197,8 @@ struct Array.fold_left2 f (Array.fold_left2 f acc ta1 ta2) ca1 ca2 | DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) -> f (Option.fold_left2 f (f acc t1 t2) topt1 topt2) u1 u2 - | _ -> assert false + | (DRel | DNil | DSort | DRef _ | DCtx _ | DApp _ | DLambda _ | DCase _ + | DFix _ | DCoFix _ | DCons _), _ -> assert false let map2 (f:'a -> 'b -> 'c) (c1:'a t) (c2:'b t) : 'c t = let head w = map (fun _ -> ()) w in @@ -194,11 +218,13 @@ struct DCoFix (i,Array.map2 f ta1 ta2,Array.map2 f ca1 ca2) | DCons ((t1,topt1),u1), DCons ((t2,topt2),u2) -> DCons ((f t1 t2,Option.lift2 f topt1 topt2), f u1 u2) - | _ -> assert false + | (DRel | DNil | DSort | DRef _ | DCtx _ | DApp _ | DLambda _ | DCase _ + | DFix _ | DCoFix _ | DCons _), _ -> assert false let terminal = function | (DRel | DSort | DNil | DRef _) -> true - | _ -> false + | DLambda _ | DApp _ | DCase _ | DFix _ | DCoFix _ | DCtx _ | DCons _ -> + false let compare t1 t2 = compare dummy_cmp t1 t2 @@ -257,7 +283,7 @@ struct let pat_of_constr c : term_pattern = (** To each evar we associate a unique identifier. *) let metas = ref Evar.Map.empty in - let rec pat_of_constr c = match kind_of_term c with + let rec pat_of_constr c = match Constr.kind c with | Rel _ -> Term DRel | Sort _ -> Term DSort | Var i -> Term (DRef (VarRef i)) @@ -290,7 +316,7 @@ struct | Proj (p,c) -> Term (DApp (Term (DRef (ConstRef (Projection.constant p))), pat_of_constr c)) - and ctx_of_constr ctx c = match kind_of_term c with + and ctx_of_constr ctx c = match Constr.kind c with | Prod (_,t,c) -> ctx_of_constr (Term(DCons((pat_of_constr t,None),ctx))) c | LetIn(_,d,t,c) -> ctx_of_constr (Term(DCons((pat_of_constr t, Some (pat_of_constr d)),ctx))) c | _ -> ctx,pat_of_constr c @@ -344,18 +370,19 @@ struct ) (pr_dconstr pr_term_pattern) p*) let search_pat cpat dpat dn = - let whole_c = cpat in + let whole_c = EConstr.of_constr cpat in (* if we are at the root, add an empty context *) let dpat = under_prod (empty_ctx dpat) in TDnet.Idset.fold (fun id acc -> let c_id = Opt.reduce (Ident.constr_of id) in + let c_id = EConstr.of_constr c_id in let (ctx,wc) = - try Termops.align_prod_letin whole_c c_id + try Termops.align_prod_letin Evd.empty whole_c c_id (** FIXME *) with Invalid_argument _ -> [],c_id in let wc,whole_c = if Opt.direction then whole_c,wc else wc,whole_c in try - let _ = Termops.filtering ctx Reduction.CUMUL wc whole_c in + let _ = Termops.filtering Evd.empty ctx Reduction.CUMUL wc whole_c in id :: acc with Termops.CannotFilter -> (* msgnl(str"recon "++Termops.print_constr_env (Global.env()) wc); *) acc ) (TDnet.find_match dpat dn) [] |