From bf12eb93f3f6a6a824a10878878fadd59745aae0 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 29 Dec 2012 10:57:43 +0100 Subject: Imported Upstream version 8.4pl1dfsg --- pretyping/glob_term.ml | 34 ++++++++++++++++++++++++++++++++-- 1 file changed, 32 insertions(+), 2 deletions(-) (limited to 'pretyping/glob_term.ml') diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 24c5ba5b..8e4b211f 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -346,8 +346,38 @@ let rec cases_pattern_of_glob_constr na = function | GHole (loc,_) -> PatVar (loc,na) | GRef (loc,ConstructRef cstr) -> PatCstr (loc,cstr,[],na) - | GApp (loc,GRef (_,ConstructRef cstr),l) -> - PatCstr (loc,cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na) + | GApp (loc,GRef (_,ConstructRef (ind,_ as cstr)),args) -> + let mib,_ = Global.lookup_inductive ind in + let nparams = mib.Declarations.mind_nparams in + if nparams > List.length args then + user_err_loc (loc,"",Pp.str "Invalid notation for pattern."); + let params,args = list_chop nparams args in + List.iter (function GHole _ -> () + | _ -> user_err_loc (loc,"",Pp.str"Invalid notation for pattern.")) + params; + let args = List.map (cases_pattern_of_glob_constr Anonymous) args in + PatCstr (loc,cstr,args,na) + | _ -> raise Not_found + +let rec cases_pattern_of_glob_constr na = function + | GVar (loc,id) when na<>Anonymous -> + (* Unable to manage the presence of both an alias and a variable *) + raise Not_found + | GVar (loc,id) -> PatVar (loc,Name id) + | GHole (loc,_) -> PatVar (loc,na) + | GRef (loc,ConstructRef cstr) -> + PatCstr (loc,cstr,[],na) + | GApp (loc,GRef (_,ConstructRef (ind,_ as cstr)),args) -> + let mib,_ = Global.lookup_inductive ind in + let nparams = mib.Declarations.mind_nparams in + if nparams > List.length args then + user_err_loc (loc,"",Pp.str "Invalid notation for pattern."); + let params,args = list_chop nparams args in + List.iter (function GHole _ -> () + | _ -> user_err_loc (loc,"",Pp.str"Invalid notation for pattern.")) + params; + let args = List.map (cases_pattern_of_glob_constr Anonymous) args in + PatCstr (loc,cstr,args,na) | _ -> raise Not_found (* Turn a closed cases pattern into a glob_constr *) -- cgit v1.2.3