diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-03 02:49:04 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-03-03 02:52:53 +0100 |
commit | a13e33bc6b4cf637f0e3b94be15907d50cf48eea (patch) | |
tree | 97cb1de091a69cbc616538dd3fe93212510bc9da | |
parent | 37f624d80e82d655021f2beb7d72794a120ff8b5 (diff) |
Removing Termdn, and putting the relevant code in Btermdn. The current Termdn
file was useless and duplicated code from Btermdn itself.
-rw-r--r-- | tactics/btermdn.ml | 175 | ||||
-rw-r--r-- | tactics/btermdn.mli | 12 | ||||
-rw-r--r-- | tactics/tactics.mllib | 1 | ||||
-rw-r--r-- | tactics/termdn.ml | 92 | ||||
-rw-r--r-- | tactics/termdn.mli | 44 |
5 files changed, 119 insertions, 205 deletions
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index 1751d4138..b93be6fc2 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -18,11 +18,117 @@ open Globnames let dnet_depth = ref 8 +type term_label = +| GRLabel of global_reference +| ProdLabel +| LambdaLabel +| SortLabel + +let compare_term_label t1 t2 = match t1, t2 with +| GRLabel gr1, GRLabel gr2 -> RefOrdered.compare gr1 gr2 +| _ -> Pervasives.compare t1 t2 (** OK *) + +type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything + +let decomp_pat = + let rec decrec acc = function + | PApp (f,args) -> decrec (Array.to_list args @ acc) f + | c -> (c,acc) + in + decrec [] + +let decomp = + let rec decrec acc c = match kind_of_term c with + | App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f + | Cast (c1,_,_) -> decrec acc c1 + | _ -> (c,acc) + in + decrec [] + +let constr_val_discr t = + let c, l = decomp t in + match kind_of_term c with + | Ind ind_sp -> Label(GRLabel (IndRef ind_sp),l) + | Construct cstr_sp -> Label(GRLabel (ConstructRef cstr_sp),l) + | Var id -> Label(GRLabel (VarRef id),l) + | Const _ -> Everything + | _ -> Nothing + +let constr_pat_discr t = + if not (Patternops.occur_meta_pattern t) then + None + else + match decomp_pat t with + | PRef ((IndRef _) as ref), args + | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args) + | PRef ((VarRef v) as ref), args -> Some(GRLabel ref,args) + | _ -> None + +let constr_val_discr_st (idpred,cpred) t = + let c, l = decomp t in + match kind_of_term c with + | Const c -> if Cpred.mem c cpred then Everything else Label(GRLabel (ConstRef c),l) + | Ind ind_sp -> Label(GRLabel (IndRef ind_sp),l) + | Construct cstr_sp -> Label(GRLabel (ConstructRef cstr_sp),l) + | Var id when not (Id.Pred.mem id idpred) -> Label(GRLabel (VarRef id),l) + | Prod (n, d, c) -> Label(ProdLabel, [d; c]) + | Lambda (n, d, c) -> Label(LambdaLabel, [d; c] @ l) + | Sort _ -> Label(SortLabel, []) + | Evar _ -> Everything + | _ -> Nothing + +let constr_pat_discr_st (idpred,cpred) t = + match decomp_pat t with + | PRef ((IndRef _) as ref), args + | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args) + | PRef ((VarRef v) as ref), args when not (Id.Pred.mem v idpred) -> + Some(GRLabel ref,args) + | PVar v, args when not (Id.Pred.mem v idpred) -> + Some(GRLabel (VarRef v),args) + | PRef ((ConstRef c) as ref), args when not (Cpred.mem c cpred) -> + Some (GRLabel ref, args) + | PProd (_, d, c), [] -> Some (ProdLabel, [d ; c]) + | PLambda (_, d, c), l -> Some (LambdaLabel, [d ; c] @ l) + | PSort s, [] -> Some (SortLabel, []) + | _ -> None + +let bounded_constr_pat_discr_st st (t,depth) = + if Int.equal depth 0 then + None + else + match constr_pat_discr_st st t with + | None -> None + | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l) + +let bounded_constr_val_discr_st st (t,depth) = + if Int.equal depth 0 then + Nothing + else + match constr_val_discr_st st t with + | Label (c,l) -> Label(c,List.map (fun c -> (c,depth-1)) l) + | Nothing -> Nothing + | Everything -> Everything + +let bounded_constr_pat_discr (t,depth) = + if Int.equal depth 0 then + None + else + match constr_pat_discr t with + | None -> None + | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l) + +let bounded_constr_val_discr (t,depth) = + if Int.equal depth 0 then + Nothing + else + match constr_val_discr t with + | Label (c,l) -> Label(c,List.map (fun c -> (c,depth-1)) l) + | Nothing -> Nothing + | Everything -> Everything module Make = functor (Z : Map.OrderedType) -> struct - open Termdn module X = struct type t = constr_pattern*int @@ -34,79 +140,12 @@ struct let compare = compare_term_label end - type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything - module Dn = Dn.Make(X)(Y)(Z) type t = Dn.t let create = Dn.create - let decomp = - let rec decrec acc c = match kind_of_term c with - | App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f - | Cast (c1,_,_) -> decrec acc c1 - | _ -> (c,acc) - in - decrec [] - - let constr_val_discr t = - let c, l = decomp t in - match kind_of_term c with - | Ind ind_sp -> Label(GRLabel (IndRef ind_sp),l) - | Construct cstr_sp -> Label(GRLabel (ConstructRef cstr_sp),l) - | Var id -> Label(GRLabel (VarRef id),l) - | Const _ -> Everything - | _ -> Nothing - - let constr_val_discr_st (idpred,cpred) t = - let c, l = decomp t in - match kind_of_term c with - | Const c -> if Cpred.mem c cpred then Everything else Label(GRLabel (ConstRef c),l) - | Ind ind_sp -> Label(GRLabel (IndRef ind_sp),l) - | Construct cstr_sp -> Label(GRLabel (ConstructRef cstr_sp),l) - | Var id when not (Id.Pred.mem id idpred) -> Label(GRLabel (VarRef id),l) - | Prod (n, d, c) -> Label(ProdLabel, [d; c]) - | Lambda (n, d, c) -> Label(LambdaLabel, [d; c] @ l) - | Sort _ -> Label(SortLabel, []) - | Evar _ -> Everything - | _ -> Nothing - - let bounded_constr_pat_discr_st st (t,depth) = - if Int.equal depth 0 then - None - else - match constr_pat_discr_st st t with - | None -> None - | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l) - - let bounded_constr_val_discr_st st (t,depth) = - if Int.equal depth 0 then - Nothing - else - match constr_val_discr_st st t with - | Label (c,l) -> Label(c,List.map (fun c -> (c,depth-1)) l) - | Nothing -> Nothing - | Everything -> Everything - - let bounded_constr_pat_discr (t,depth) = - if Int.equal depth 0 then - None - else - match constr_pat_discr t with - | None -> None - | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l) - - let bounded_constr_val_discr (t,depth) = - if Int.equal depth 0 then - Nothing - else - match constr_val_discr t with - | Label (c,l) -> Label(c,List.map (fun c -> (c,depth-1)) l) - | Nothing -> Nothing - | Everything -> Everything - - let add = function | None -> (fun dn (c,v) -> diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index fedc68047..575502026 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -11,6 +11,18 @@ open Pattern open Names (** Discrimination nets with bounded depth. *) + +(** This module registers actions (typically tactics) mapped to patterns *) + +(** Patterns are stocked linearly as the list of its node in prefix +order in such a way patterns having the same prefix have this common +prefix shared and the seek for the action associated to the patterns +that a term matches are found in time proportional to the maximal +number of nodes of the patterns matching the term. The [transparent_state] +indicates which constants and variables can be considered as rigid. +These dnets are able to cope with existential variables as well, which match +[Everything]. *) + module Make : functor (Z : Map.OrderedType) -> sig diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index a4de9e2b4..27ded2357 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -1,6 +1,5 @@ Geninterp Dn -Termdn Btermdn Tacticals Hipattern diff --git a/tactics/termdn.ml b/tactics/termdn.ml deleted file mode 100644 index 7eff2909f..000000000 --- a/tactics/termdn.ml +++ /dev/null @@ -1,92 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Util -open Names -open Term -open Pattern -open Patternops -open Globnames - -type term_label = -| GRLabel of global_reference -| ProdLabel -| LambdaLabel -| SortLabel - -let compare_term_label t1 t2 = match t1, t2 with -| GRLabel gr1, GRLabel gr2 -> RefOrdered.compare gr1 gr2 -| _ -> Pervasives.compare t1 t2 (** OK *) - -type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything - -(*If we have: f a b c ..., decomp gives: (f,[a;b;c;...])*) - -let decomp = - let rec decrec acc c = match kind_of_term c with - | App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f - | Cast (c1,_,_) -> decrec acc c1 - | _ -> (c,acc) - in - decrec [] - -let decomp_pat = - let rec decrec acc = function - | PApp (f,args) -> decrec (Array.to_list args @ acc) f - | c -> (c,acc) - in - decrec [] - -let constr_pat_discr t = - if not (occur_meta_pattern t) then - None - else - match decomp_pat t with - | PRef ((IndRef _) as ref), args - | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args) - | PRef ((VarRef v) as ref), args -> Some(GRLabel ref,args) - | _ -> None - -let constr_pat_discr_st (idpred,cpred) t = - match decomp_pat t with - | PRef ((IndRef _) as ref), args - | PRef ((ConstructRef _ ) as ref), args -> Some (GRLabel ref,args) - | PRef ((VarRef v) as ref), args when not (Id.Pred.mem v idpred) -> - Some(GRLabel ref,args) - | PVar v, args when not (Id.Pred.mem v idpred) -> - Some(GRLabel (VarRef v),args) - | PRef ((ConstRef c) as ref), args when not (Cpred.mem c cpred) -> - Some (GRLabel ref, args) - | PProd (_, d, c), [] -> Some (ProdLabel, [d ; c]) - | PLambda (_, d, c), l -> Some (LambdaLabel, [d ; c] @ l) - | PSort s, [] -> Some (SortLabel, []) - | _ -> None - -open Dn - -let constr_val_discr t = - let c, l = decomp t in - match kind_of_term c with - | Ind ind_sp -> Label(GRLabel (IndRef ind_sp),l) - | Construct cstr_sp -> Label(GRLabel (ConstructRef cstr_sp),l) - | Var id -> Label(GRLabel (VarRef id),l) - | Const _ -> Everything - | _ -> Nothing - -let constr_val_discr_st (idpred,cpred) t = - let c, l = decomp t in - match kind_of_term c with - | Const c -> if Cpred.mem c cpred then Everything else Label(GRLabel (ConstRef c),l) - | Ind ind_sp -> Label(GRLabel (IndRef ind_sp),l) - | Construct cstr_sp -> Label(GRLabel (ConstructRef cstr_sp),l) - | Var id when not (Id.Pred.mem id idpred) -> Label(GRLabel (VarRef id),l) - | Prod (n, d, c) -> Label(ProdLabel, [d; c]) - | Lambda (n, d, c) -> Label(LambdaLabel, [d; c] @ l) - | Sort _ -> Label (SortLabel, []) - | Evar _ -> Everything - | _ -> Nothing diff --git a/tactics/termdn.mli b/tactics/termdn.mli deleted file mode 100644 index 16be2e1c9..000000000 --- a/tactics/termdn.mli +++ /dev/null @@ -1,44 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Term -open Pattern -open Globnames -open Names - -type term_label = -| GRLabel of global_reference -| ProdLabel -| LambdaLabel -| SortLabel - -val compare_term_label : term_label -> term_label -> int - -(** Discrimination nets of terms. *) - -(** This module registers actions (typically tactics) mapped to patterns *) - -(** Patterns are stocked linearly as the list of its node in prefix -order in such a way patterns having the same prefix have this common -prefix shared and the seek for the action associated to the patterns -that a term matches are found in time proportional to the maximal -number of nodes of the patterns matching the term. The [transparent_state] -indicates which constants and variables can be considered as rigid. -These dnets are able to cope with existential variables as well, which match -[Everything]. *) - -(**/**) -(** These are for Nbtermdn *) - -val constr_pat_discr_st : transparent_state -> - constr_pattern -> (term_label * constr_pattern list) option -val constr_val_discr_st : transparent_state -> - constr -> (term_label * constr list) Dn.lookup_res - -val constr_pat_discr : constr_pattern -> (term_label * constr_pattern list) option -val constr_val_discr : constr -> (term_label * constr list) Dn.lookup_res |