diff options
Diffstat (limited to 'interp/topconstr.ml')
| -rw-r--r-- | interp/topconstr.ml | 46 |
1 files changed, 21 insertions, 25 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 1231f115..cc8e697e 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -38,27 +38,11 @@ let error_invalid_pattern_notation loc = (**********************************************************************) (* Functions on constr_expr *) -let ids_of_cases_indtype = - let rec vars_of ids = function - (* We deal only with the regular cases *) - | (CPatCstr (_,_,l1,l2)|CPatNotation (_,_,(l1,[]),l2)) -> - List.fold_left vars_of (List.fold_left vars_of [] l2) l1 - (* assume the ntn is applicative and does not instantiate the head !! *) - | CPatDelimiters(_,_,c) -> vars_of ids c - | CPatAtom (_, Some (Libnames.Ident (_, x))) -> x::ids - | _ -> ids in - vars_of [] - -let ids_of_cases_tomatch tms = - List.fold_right - (fun (_,(ona,indnal)) l -> - Option.fold_right (fun t -> (@) (ids_of_cases_indtype t)) - indnal (Option.fold_right (Loc.down_located name_cons) ona l)) - tms [] - let is_constructor id = - try ignore (Nametab.locate_extended (qualid_of_ident id)); true - with Not_found -> true + try Globnames.isConstructRef + (Smartlocate.global_of_extended_global + (Nametab.locate_extended (qualid_of_ident id))) + with Not_found -> false let rec cases_pattern_fold_names f a = function | CPatRecord (_, l) -> @@ -82,6 +66,17 @@ let ids_of_pattern_list = (List.fold_left (cases_pattern_fold_names Id.Set.add))) Id.Set.empty +let ids_of_cases_indtype p = + Id.Set.elements (cases_pattern_fold_names Id.Set.add Id.Set.empty p) + +let ids_of_cases_tomatch tms = + List.fold_right + (fun (_,(ona,indnal)) l -> + Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t) + indnal + (Option.fold_right (Loc.down_located (name_fold Id.Set.add)) ona l)) + tms Id.Set.empty + let rec fold_constr_expr_binders g f n acc b = function | (nal,bk,t)::l -> let nal = snd (List.split nal) in @@ -119,7 +114,7 @@ let fold_constr_expr_with_binders g f n acc = function | CRecord (loc,_,l) -> List.fold_left (fun acc (id, c) -> f n acc c) acc l | CCases (loc,sty,rtnpo,al,bl) -> let ids = ids_of_cases_tomatch al in - let acc = Option.fold_left (f (List.fold_right g ids n)) acc rtnpo in + let acc = Option.fold_left (f (Id.Set.fold g ids n)) acc rtnpo in let acc = List.fold_left (f n) acc (List.map fst al) in List.fold_right (fun (loc,patl,rhs) acc -> let ids = ids_of_pattern_list patl in @@ -220,10 +215,11 @@ let map_constr_expr_with_binders g f e = function | CPrim _ | CRef _ as x -> x | CRecord (loc,p,l) -> CRecord (loc,p,List.map (fun (id, c) -> (id, f e c)) l) | CCases (loc,sty,rtnpo,a,bl) -> - (* TODO: apply g on the binding variables in pat... *) - let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in + let bl = List.map (fun (loc,patl,rhs) -> + let ids = ids_of_pattern_list patl in + (loc,patl,f (Id.Set.fold g ids e) rhs)) bl in let ids = ids_of_cases_tomatch a in - let po = Option.map (f (List.fold_right g ids e)) rtnpo in + let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in CCases (loc, sty, po, List.map (fun (tm,x) -> (f e tm,x)) a,bl) | CLetTuple (loc,nal,(ona,po),b,c) -> let e' = List.fold_right (Loc.down_located (name_fold g)) nal e in |