diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 67 |
1 files changed, 34 insertions, 33 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 6514ad8be5..6f17324a19 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -46,7 +46,7 @@ open Context.Rel.Declaration types and recursive definitions and of projection names in records *) type var_internalization_type = - | Inductive of Id.t list (* list of params *) + | Inductive of Id.t list (* list of params *) * bool (* true = check for possible capture *) | Recursive | Method | Variable @@ -98,16 +98,16 @@ let global_reference_of_reference ref = locate_reference (snd (qualid_of_reference ref)) let global_reference id = - Universes.constr_of_global (locate_reference (qualid_of_ident id)) + locate_reference (qualid_of_ident id) let construct_reference ctx id = try - Term.mkVar (let _ = Context.Named.lookup id ctx in id) + VarRef (let _ = Context.Named.lookup id ctx in id) with Not_found -> global_reference id let global_reference_in_absolute_module dir id = - Universes.constr_of_global (Nametab.global_of_path (Libnames.make_path dir id)) + Nametab.global_of_path (Libnames.make_path dir id) (**********************************************************************) (* Internalization errors *) @@ -176,7 +176,7 @@ let parsing_explicit = ref false let empty_internalization_env = Id.Map.empty let compute_explicitable_implicit imps = function - | Inductive params -> + | Inductive (params,_) -> (* In inductive types, the parameters are fixed implicit arguments *) let sub_impl,_ = List.chop (List.length params) imps in let sub_impl' = List.filter is_status_implicit sub_impl in @@ -190,10 +190,10 @@ let compute_internalization_data env ty typ impl = let expls_impl = compute_explicitable_implicit impl ty in (ty, expls_impl, impl, compute_arguments_scope typ) -let compute_internalization_env env ty = +let compute_internalization_env env ?(impls=empty_internalization_env) ty = List.fold_left3 (fun map id typ impl -> Id.Map.add id (compute_internalization_data env ty typ impl) map) - empty_internalization_env + impls (**********************************************************************) (* Contracting "{ _ }" in notations *) @@ -358,16 +358,17 @@ let locate_if_hole ?loc na = function let reset_hidden_inductive_implicit_test env = { env with impls = Id.Map.map (function - | (Inductive _,b,c,d) -> (Inductive [],b,c,d) + | (Inductive (params,_),b,c,d) -> (Inductive (params,false),b,c,d) | x -> x) env.impls } -let check_hidden_implicit_parameters id impls = +let check_hidden_implicit_parameters ?loc id impls = if Id.Map.exists (fun _ -> function - | (Inductive indparams,_,_,_) -> Id.List.mem id indparams + | (Inductive (indparams,check),_,_,_) when check -> Id.List.mem id indparams | _ -> false) impls then - user_err (strbrk "A parameter of an inductive type " ++ - pr_id id ++ strbrk " is not allowed to be used as a bound variable in the type of its constructor.") + user_err ?loc (pr_id id ++ strbrk " is already used as name of " ++ + strbrk "a parameter of the inductive type; bound variables in " ++ + strbrk "the type of a constructor shall use a different name.") let push_name_env ?(global_level=false) ntnvars implargs env = function @@ -376,7 +377,7 @@ let push_name_env ?(global_level=false) ntnvars implargs env = user_err ?loc (str "Anonymous variables not allowed"); env | loc,Name id -> - check_hidden_implicit_parameters id env.impls ; + check_hidden_implicit_parameters ?loc id env.impls ; if Id.Map.is_empty ntnvars && Id.equal id ldots_var then error_ldots_var ?loc; set_var_scope ?loc id false env ntnvars; @@ -536,7 +537,7 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function try (* Binders bound in the notation are considered first-order objects *) let _,na = coerce_to_name (fst (Id.Map.find id terms)) in - (renaming,{env with ids = name_fold Id.Set.add na env.ids}), na + (renaming,{env with ids = Name.fold_right Id.Set.add na env.ids}), na with Not_found -> (* Binders not bound in the notation do not capture variables *) (* outside the notation (i.e. in the substitution) *) @@ -616,7 +617,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 +660,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 +1071,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 +1086,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 +1219,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 +1346,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 +1371,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 +1465,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 +1507,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),_ = @@ -1660,7 +1661,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = | CCases (sty, rtnpo, tms, eqns) -> let as_in_vars = List.fold_left (fun acc (_,na,inb) -> Option.fold_left (fun acc tt -> Id.Set.union (ids_of_cases_indtype tt) acc) - (Option.fold_left (fun acc (_,y) -> name_fold Id.Set.add y acc) acc na) + (Option.fold_left (fun acc (_,y) -> Name.fold_right Id.Set.add y acc) acc na) inb) Id.Set.empty tms in (* as, in & return vars *) let forbidden_vars = Option.cata free_vars_of_constr_expr as_in_vars rtnpo in @@ -1749,12 +1750,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 +1945,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 +2024,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 = @@ -2071,7 +2072,7 @@ let intern_context global_level env impl_env binders = with InternalizationError (loc,e) -> user_err ?loc ~hdr:"internalize" (explain_internalization_error e) -let interp_rawcontext_evars env evdref k bl = +let interp_glob_context_evars env evdref k bl = let open EConstr in let (env, par, _, impls) = List.fold_left @@ -2100,6 +2101,6 @@ let interp_rawcontext_evars env evdref k bl = let interp_context_evars ?(global_level=false) ?(impl_env=empty_internalization_env) ?(shift=0) env evdref params = let int_env,bl = intern_context global_level env impl_env params in - let x = interp_rawcontext_evars env evdref shift bl in + let x = interp_glob_context_evars env evdref shift bl in int_env, x |