diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2014-07-30 10:52:36 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2014-07-30 14:24:40 +0200 |
commit | e1d69ae5106f69cc7e683402fd0125b40a7504e2 (patch) | |
tree | 1fce07f2ec432b772b3045e99d60907f31e2649e /tactics/btermdn.ml | |
parent | 1dfd513bd9c63893eb982ad43ab892f5f95ac9c7 (diff) |
Fix discrimination net which was not recognizing primitive projections.
Diffstat (limited to 'tactics/btermdn.ml')
-rw-r--r-- | tactics/btermdn.ml | 73 |
1 files changed, 2 insertions, 71 deletions
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index df8e98604..5fbc6f5b2 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -33,6 +33,7 @@ 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 + | PProj (p, c) -> (PRef (ConstRef p), c :: acc) | c -> (c,acc) in decrec [] @@ -40,6 +41,7 @@ let decomp_pat = 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 + | Proj (p, c) -> (mkConst p, c :: acc) | Cast (c1,_,_) -> decrec acc c1 | _ -> (c,acc) in @@ -141,77 +143,6 @@ struct let create = Dn.create -(* FIXME: MS: remove *) -(* 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 - | Proj (p,c) -> decrec (c :: acc) (mkConst p) - | 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,_) -> Dn.Label(Term_dn.GRLabel (IndRef ind_sp),l) - | Construct (cstr_sp,_) -> Dn.Label(Term_dn.GRLabel (ConstructRef cstr_sp),l) - | Var id -> Dn.Label(Term_dn.GRLabel (VarRef id),l) - | Const _ -> Dn.Everything - | Proj (p, c) -> Dn.Everything - | _ -> Dn.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 Dn.Everything else Dn.Label(Term_dn.GRLabel (ConstRef c),l) - | Ind (ind_sp,_) -> Dn.Label(Term_dn.GRLabel (IndRef ind_sp),l) - | Construct (cstr_sp,_) -> Dn.Label(Term_dn.GRLabel (ConstructRef cstr_sp),l) - | Proj (p,c) -> - if Cpred.mem p cpred then Dn.Everything else Dn.Label(Term_dn.GRLabel (ConstRef p), c::l) - | Var id when not (Id.Pred.mem id idpred) -> Dn.Label(Term_dn.GRLabel (VarRef id),l) - | Prod (n, d, c) -> Dn.Label(Term_dn.ProdLabel, [d; c]) - | Lambda (n, d, c) -> Dn.Label(Term_dn.LambdaLabel, [d; c] @ l) - | Sort _ -> Dn.Label(Term_dn.SortLabel, []) - | Evar _ -> Dn.Everything - | _ -> Dn.Nothing - - let bounded_constr_pat_discr_st st (t,depth) = - if Int.equal depth 0 then - None - else - match Term_dn.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 - Dn.Nothing - else - match constr_val_discr_st st t with - | Dn.Label (c,l) -> Dn.Label(c,List.map (fun c -> (c,depth-1)) l) - | Dn.Nothing -> Dn.Nothing - | Dn.Everything -> Dn.Everything - - let bounded_constr_pat_discr (t,depth) = - if Int.equal depth 0 then - None - else - match Term_dn.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 - Dn.Nothing - else - match constr_val_discr t with - | Dn.Label (c,l) -> Dn.Label(c,List.map (fun c -> (c,depth-1)) l) - | Dn.Nothing -> Dn.Nothing - | Dn.Everything -> Dn.Everything - -*) - let add = function | None -> (fun dn (c,v) -> |