diff options
Diffstat (limited to 'tactics/termdn.ml')
| -rw-r--r-- | tactics/termdn.ml | 36 |
1 files changed, 19 insertions, 17 deletions
diff --git a/tactics/termdn.ml b/tactics/termdn.ml index fda033f268..957543e16d 100644 --- a/tactics/termdn.ml +++ b/tactics/termdn.ml @@ -3,18 +3,15 @@ open Util open Generic +open Names open Term +open Rawterm (* Discrimination nets of terms. See the module dn.ml for further explanations. Eduardo (5/8/97) *) -type lbl = - | TERM of constr - | DOPER of sorts oper - | DLAMBDA - -type 'a t = (lbl,constr,'a) Dn.t +type 'a t = (constr_label,constr_pattern,'a) Dn.t (*If we have: f a b c ..., decomp gives: (f,[a;b;c;...])*) @@ -24,26 +21,31 @@ let decomp = | DOP2(Cast,c1,_) -> decrec acc c1 | c -> (c,acc) in - decrec [] + 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 t) then + if not (occur_meta_pattern t) then None else - match decomp t with - (* | DOPN(Const _,_) as c,l -> Some(TERM c,l) *) - | DOPN(MutInd _,_) as c,l -> Some(TERM c,l) - | DOPN(MutConstruct _,_) as c,l -> Some(TERM c,l) - | VAR _ as c,l -> Some(TERM c,l) - | c -> None + match decomp_pat t with + | PRef (RInd (ind_sp,_)), args -> Some(IndNode ind_sp,args) + | PRef (RConstruct (cstr_sp,_)), args -> Some(CstrNode cstr_sp,args) + | PRef (RVar id), args -> Some(VarNode id,args) + | _ -> None let constr_val_discr t = match decomp t with (* DOPN(Const _,_) as c,l -> Some(TERM c,l) *) - | DOPN(MutInd _,_) as c,l -> Some(TERM c,l) - | DOPN(MutConstruct _,_) as c,l -> Some(TERM c,l) - | VAR _ as c,l -> Some(TERM c,l) + | DOPN(MutInd ind_sp,_) as c,l -> Some(IndNode ind_sp,l) + | DOPN(MutConstruct cstr_sp,_) as c,l -> Some(CstrNode cstr_sp,l) + | VAR id as c,l -> Some(VarNode id,l) | c -> None (* Les deux fonctions suivantes ecrasaient les precedentes, |