diff options
author | Stephane Glondu <steph@glondu.net> | 2012-12-29 10:57:43 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-12-29 10:57:43 +0100 |
commit | bf12eb93f3f6a6a824a10878878fadd59745aae0 (patch) | |
tree | 279f64f4b7e4804415ab5731cc7aaa8a4fcfe074 /pretyping/glob_term.ml | |
parent | e0d682ec25282a348d35c5b169abafec48555690 (diff) |
Imported Upstream version 8.4pl1dfsgupstream/8.4pl1dfsg
Diffstat (limited to 'pretyping/glob_term.ml')
-rw-r--r-- | pretyping/glob_term.ml | 34 |
1 files changed, 32 insertions, 2 deletions
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 *) |