diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 44 |
1 files changed, 27 insertions, 17 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index def8425ec3..848180743f 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -14,6 +14,7 @@ open Util open CAst open Names open Nameops +open Constr open Namegen open Libnames open Globnames @@ -525,7 +526,7 @@ let rec expand_binders ?loc mk bl c = let tm = DAst.make ?loc (GVar id) in (* Distribute the disjunctive patterns over the shared right-hand side *) let eqnl = List.map (fun pat -> CAst.make ?loc (ids,[pat],c)) disjpat in - let c = DAst.make ?loc @@ GCases (Misctypes.LetPatternStyle, None, [tm,(Anonymous,None)], eqnl) in + let c = DAst.make ?loc @@ GCases (LetPatternStyle, None, [tm,(Anonymous,None)], eqnl) in expand_binders ?loc mk bl (mk ?loc (Name id,Explicit,ty) c) (**********************************************************************) @@ -819,11 +820,11 @@ let split_by_type ids subst = | NtnTypeConstr -> let terms,terms' = bind id scl terms terms' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') - | NtnTypeBinder NtnBinderParsedAsConstr (Extend.AsIdentOrPattern | Extend.AsStrictPattern) -> + | NtnTypeBinder NtnBinderParsedAsConstr (AsIdentOrPattern | AsStrictPattern) -> let a,terms = match terms with a::terms -> a,terms | _ -> assert false in let binders' = Id.Map.add id (coerce_to_cases_pattern_expr a,(false,scl)) binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') - | NtnTypeBinder NtnBinderParsedAsConstr Extend.AsIdent -> + | NtnTypeBinder NtnBinderParsedAsConstr AsIdent -> let a,terms = match terms with a::terms -> a,terms | _ -> assert false in let binders' = Id.Map.add id (cases_pattern_of_name (coerce_to_name a),(true,scl)) binders' in (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists') @@ -980,17 +981,17 @@ let intern_reference ref = in Smartlocate.global_of_extended_global r -let sort_info_of_level_info (info: Misctypes.level_info) : (Libnames.reference * int) option = +let sort_info_of_level_info (info: level_info) : (Libnames.reference * int) option = match info with - | Misctypes.UAnonymous -> None - | Misctypes.UUnknown -> None - | Misctypes.UNamed id -> Some (id, 0) + | UAnonymous -> None + | UUnknown -> None + | UNamed id -> Some (id, 0) -let glob_sort_of_level (level: Misctypes.glob_level) : Misctypes.glob_sort = +let glob_sort_of_level (level: glob_level) : glob_sort = match level with - | Misctypes.GProp -> Misctypes.GProp - | Misctypes.GSet -> Misctypes.GSet - | Misctypes.GType info -> Misctypes.GType [sort_info_of_level_info info] + | GProp -> GProp + | GSet -> GSet + | GType info -> GType [sort_info_of_level_info info] (* Is it a global reference or a syntactic definition? *) let intern_qualid qid intern env ntnvars us args = @@ -998,7 +999,7 @@ let intern_qualid qid intern env ntnvars us args = match intern_extended_global_of_qualid qid with | TrueGlobal ref -> (DAst.make ?loc @@ GRef (ref, us)), true, args | SynDef sp -> - let (ids,c) = Syntax_def.search_syntactic_definition sp in + let (ids,c) = Syntax_def.search_syntactic_definition ?loc sp in let nids = List.length ids in if List.length args < nids then error_not_enough_arguments ?loc; let args1,args2 = List.chop nids args in @@ -1024,7 +1025,7 @@ let intern_qualid qid intern env ntnvars us args = DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg) | _ -> err () end - | Some [s], GSort (Misctypes.GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s) + | Some [s], GSort (GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s) | Some [_old_level], GSort _new_sort -> (* TODO: add old_level and new_sort to the error message *) user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid.v) @@ -1140,9 +1141,18 @@ let check_number_of_pattern loc n l = if not (Int.equal n p) then raise (InternalizationError (loc,BadPatternsNumber (n,p))) let check_or_pat_variables loc ids idsl = - if List.exists (fun ids' -> not (List.eq_set (fun {loc;v=id} {v=id'} -> Id.equal id id') ids ids')) idsl then - user_err ?loc (str - "The components of this disjunctive pattern must bind the same variables.") + let eq_id {v=id} {v=id'} = Id.equal id id' in + (* Collect remaining patterns which do not have the same variables as the first pattern *) + let idsl = List.filter (fun ids' -> not (List.eq_set eq_id ids ids')) idsl in + match idsl with + | ids'::_ -> + (* Look for an [id] which is either in [ids] and not in [ids'] or in [ids'] and not in [ids] *) + let ids'' = List.subtract eq_id ids ids' in + let ids'' = if ids'' = [] then List.subtract eq_id ids' ids else ids'' in + user_err ?loc + (strbrk "The components of this disjunctive pattern must bind the same variables (" ++ + Id.print (List.hd ids'').v ++ strbrk " is not bound in all patterns).") + | [] -> () (** Use only when params were NOT asked to the user. @return if letin are included *) @@ -1965,7 +1975,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = if List.for_all (irrefutable globalenv) thepats then [] else [CAst.make @@ ([],List.make (List.length thepats) (DAst.make @@ PatVar Anonymous), (* "|_,..,_" *) DAst.make @@ GHole(Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None))] (* "=> _" *) in - Some (DAst.make @@ GCases(Term.RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn)) + Some (DAst.make @@ GCases(RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn)) in let eqns' = List.map (intern_eqn (List.length tms) env) eqns in DAst.make ?loc @@ |