diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 18 | ||||
| -rw-r--r-- | interp/constrintern.ml | 32 | ||||
| -rw-r--r-- | interp/constrintern.mli | 2 | ||||
| -rw-r--r-- | interp/notation.ml | 6 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 4 |
5 files changed, 32 insertions, 30 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index f6da10c961..19ca8d50b5 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -663,9 +663,11 @@ let rec extern inctx scopes vars r = | GEvar (n,l) -> extern_evar n (List.map (on_snd (extern false scopes vars)) l) - | GPatVar (b,n) -> + | GPatVar kind -> if !print_meta_as_hole then CHole (None, Misctypes.IntroAnonymous, None) else - if b then CPatVar n else CEvar (n,[]) + (match kind with + | Evar_kinds.SecondOrderPatVar n -> CPatVar n + | Evar_kinds.FirstOrderPatVar n -> CEvar (n,[])) | GApp (f,args) -> (match f with @@ -698,7 +700,7 @@ let rec extern inctx scopes vars r = | None :: q -> raise No_match | Some c :: q -> match locs with - | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern]") + | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].") | (_, false) :: locs' -> (* we don't want to print locals *) ip q locs' args acc @@ -1033,17 +1035,17 @@ let rec glob_of_pat env sigma pat = CAst.make @@ match pat with let id = try match lookup_name_of_rel n env with | Name id -> id | Anonymous -> - anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable") + anomaly ~label:"glob_constr_of_pattern" (Pp.str "index to an anonymous variable.") with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in GVar id | PMeta None -> GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None) - | PMeta (Some n) -> GPatVar (false,n) + | PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n) | PProj (p,c) -> GApp (CAst.make @@ GRef (ConstRef (Projection.constant p),None), [glob_of_pat env sigma c]) | PApp (f,args) -> GApp (glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args) | PSoApp (n,args) -> - GApp (CAst.make @@ GPatVar (true,n), + GApp (CAst.make @@ GPatVar (Evar_kinds.SecondOrderPatVar n), List.map (glob_of_pat env sigma) args) | PProd (na,t,c) -> GProd (na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c) @@ -1064,7 +1066,7 @@ let rec glob_of_pat env sigma pat = CAst.make @@ match pat with | _, Some ind -> let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat env sigma c)) bl in simple_cases_matrix_of_branches ind bl' - | _, None -> anomaly (Pp.str "PCase with some branches but unknown inductive") + | _, None -> anomaly (Pp.str "PCase with some branches but unknown inductive.") in let mat = if info.cip_extensible then mat @ [any_any_branch] else mat in @@ -1072,7 +1074,7 @@ let rec glob_of_pat env sigma pat = CAst.make @@ match pat with | PMeta None, _, _ -> (Anonymous,None),None | _, Some ind, Some nargs -> return_type_of_predicate ind nargs (glob_of_pat env sigma p) - | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive") + | _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.") in GCases (RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat) | PFix f -> (Detyping.detype_names false [] env (Global.env()) sigma (EConstr.of_constr (mkFix f))).v (** FIXME bad env *) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 190369e8fa..336cfac85c 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -616,7 +616,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = let env,bl' = List.fold_left (intern_local_binder_aux intern ntnvars) (env,[]) bl in terms_of_binders (if lassoc then bl' else List.rev bl'),(None,[]) with Not_found -> - anomaly (Pp.str "Inconsistent substitution of recursive notation") in + anomaly (Pp.str "Inconsistent substitution of recursive notation.") in let termin = aux (terms,None,None) subinfos terminator in let fold a t = let nterms = Id.Map.add y (a, (scopt, subscopes)) terms in @@ -659,7 +659,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = termin bl in make_letins letins res with Not_found -> - anomaly (Pp.str "Inconsistent substitution of recursive notation")) + anomaly (Pp.str "Inconsistent substitution of recursive notation.")) | NProd (Name id, NHole _, c') when option_mem_assoc id binderopt -> let a,letins = snd (Option.get binderopt) in let e = make_letins letins (aux subst' infos c') in @@ -1070,7 +1070,7 @@ let sort_fields ~complete loc fields completer = let global_record_id = ConstructRef record.Recordops.s_CONST in try Qualid (loc, shortest_qualid_of_global Id.Set.empty global_record_id) with Not_found -> - anomaly (str "Environment corruption for records") in + anomaly (str "Environment corruption for records.") in let () = check_duplicate loc fields in let (end_index, (* one past the last field index *) first_field_index, (* index of the first field of the record *) @@ -1085,7 +1085,7 @@ let sort_fields ~complete loc fields completer = let field_glob_ref = ConstRef field_glob_id in let first_field = eq_gr field_glob_ref first_field_glob_ref in begin match proj_kinds with - | [] -> anomaly (Pp.str "Number of projections mismatch") + | [] -> anomaly (Pp.str "Number of projections mismatch.") | (_, regular) :: proj_kinds -> (* "regular" is false when the field is defined by a let-in in the record declaration @@ -1218,7 +1218,7 @@ let drop_notations_pattern looked_for = | GHole (_,_,_) -> RCPatAtom (None) | GRef (g,_) -> RCPatCstr (g,[],[]) | GApp ({ v = GRef (g,_) }, l) -> RCPatCstr (g, List.map rcp_of_glob l,[]) - | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr "))) x + | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr."))) x in let rec drop_syndef top scopes re pats = let (loc,qid) = qualid_of_reference re in @@ -1345,7 +1345,7 @@ let drop_notations_pattern looked_for = in_pat top (scopt,subscopes@snd scopes) a with Not_found -> if Id.equal id ldots_var then CAst.make ?loc @@ RCPatAtom (Some id) else - anomaly (str "Unbound pattern notation variable: " ++ Id.print id) + anomaly (str "Unbound pattern notation variable: " ++ Id.print id ++ str ".") end | NRef g -> ensure_kind top loc g; @@ -1370,7 +1370,7 @@ let drop_notations_pattern looked_for = subst_pat_iterator ldots_var t u) (if lassoc then List.rev l else l) termin with Not_found -> - anomaly (Pp.str "Inconsistent substitution of recursive notation")) + anomaly (Pp.str "Inconsistent substitution of recursive notation.")) | NHole _ -> let () = assert (List.is_empty args) in CAst.make ?loc @@ RCPatAtom None @@ -1464,7 +1464,7 @@ let get_implicit_name n imps = let set_hole_implicit i b = function | {loc; v = GRef (r,_) } | { v = GApp ({loc; v = GRef (r,_)},_) } -> Loc.tag ?loc (Evar_kinds.ImplicitArg (r,i,b),Misctypes.IntroAnonymous,None) | {loc; v = GVar id } -> Loc.tag ?loc (Evar_kinds.ImplicitArg (VarRef id,i,b),Misctypes.IntroAnonymous,None) - | _ -> anomaly (Pp.str "Only refs have implicits") + | _ -> anomaly (Pp.str "Only refs have implicits.") let exists_implicit_name id = List.exists (fun imp -> is_status_implicit imp && Id.equal id (name_of_implicit imp)) @@ -1506,7 +1506,7 @@ let extract_explicit_arg imps args = (**********************************************************************) (* Main loop *) -let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = +let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let rec intern env = CAst.with_loc_val (fun ?loc -> function | CRef (ref,us) -> let (c,imp,subscopes,l),_ = @@ -1749,12 +1749,12 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = CAst.make ?loc @@ GHole (k, naming, solve) (* Parsing pattern variables *) - | CPatVar n when allow_patvar -> + | CPatVar n when pattern_mode -> CAst.make ?loc @@ - GPatVar (true,n) - | CEvar (n, []) when allow_patvar -> + GPatVar (Evar_kinds.SecondOrderPatVar n) + | CEvar (n, []) when pattern_mode -> CAst.make ?loc @@ - GPatVar (false,n) + GPatVar (Evar_kinds.FirstOrderPatVar n) (* end *) (* Parsing existential variables *) | CEvar (n, l) -> @@ -1944,13 +1944,13 @@ let empty_ltac_sign = { } let intern_gen kind env - ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=empty_ltac_sign) + ?(impls=empty_internalization_env) ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) c = let tmp_scope = scope_of_type_kind kind in internalize env {ids = extract_ids env; unb = false; tmp_scope = tmp_scope; scopes = []; impls = impls} - allow_patvar (ltacvars, Id.Map.empty) c + pattern_mode (ltacvars, Id.Map.empty) c let intern_constr env c = intern_gen WithoutTypeConstraint env c @@ -2023,7 +2023,7 @@ let interp_type_evars env evdref ?(impls=empty_internalization_env) c = let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c = let c = intern_gen (if as_type then IsType else WithoutTypeConstraint) - ~allow_patvar:true ~ltacvars env c in + ~pattern_mode:true ~ltacvars env c in pattern_of_glob_constr c let interp_notation_constr ?(impls=empty_internalization_env) nenv a = diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 644f60d850..324f7a3894 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -83,7 +83,7 @@ val intern_constr : env -> constr_expr -> glob_constr val intern_type : env -> constr_expr -> glob_constr val intern_gen : typing_constraint -> env -> - ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> + ?impls:internalization_env -> ?pattern_mode:bool -> ?ltacvars:ltac_sign -> constr_expr -> glob_constr val intern_pattern : env -> cases_pattern_expr -> diff --git a/interp/notation.ml b/interp/notation.ml index d19654b10b..23332f7c45 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -381,7 +381,7 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function let declare_notation_level ntn level = if String.Map.mem ntn !notation_level_map then - anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level"); + anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level."); notation_level_map := String.Map.add ntn level !notation_level_map let level_of_notation ntn = @@ -1004,13 +1004,13 @@ let declare_notation_rule ntn ~extra unpl gram = let find_notation_printing_rule ntn = try pi1 (String.Map.find ntn !notation_rules) - with Not_found -> anomaly (str "No printing rule found for " ++ str ntn) + with Not_found -> anomaly (str "No printing rule found for " ++ str ntn ++ str ".") let find_notation_extra_printing_rules ntn = try pi2 (String.Map.find ntn !notation_rules) with Not_found -> [] let find_notation_parsing_rules ntn = try pi3 (String.Map.find ntn !notation_rules) - with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn) + with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn ++ str ".") let get_defined_notations () = String.Set.elements @@ String.Map.domain !notation_rules diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 8e876ec16d..08b9fbe8ec 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -690,7 +690,7 @@ let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sig | { CAst.v = GVar id' } -> (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp), sigma - | _ -> anomaly (str "A term which can be a binder has to be a variable") + | _ -> anomaly (str "A term which can be a binder has to be a variable.") with Not_found -> (* The matching against a term allowing to find the instance has not been found yet *) (* If it will be a different name, we shall unfortunately fail *) @@ -830,7 +830,7 @@ let bind_bindinglist_as_term_env alp (terms,onlybinders,termlists,binderlists) v let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc var binderlists) in add_bindinglist_env sigma var bl with Not_found -> - anomaly (str "There should be a binder list bindings this list of terms") + anomaly (str "There should be a binder list bindings this list of terms.") let match_fix_kind fk1 fk2 = match (fk1,fk2) with |