diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 34 | ||||
| -rw-r--r-- | interp/constrintern.ml | 67 | ||||
| -rw-r--r-- | interp/constrintern.mli | 12 | ||||
| -rw-r--r-- | interp/implicit_quantifiers.ml | 2 | ||||
| -rw-r--r-- | interp/notation.ml | 6 | ||||
| -rw-r--r-- | interp/notation_ops.ml | 35 | ||||
| -rw-r--r-- | interp/topconstr.ml | 28 |
7 files changed, 81 insertions, 103 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 4c29fc8097..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 @@ -740,7 +742,7 @@ let rec extern inctx scopes vars r = | GCases (sty,rtntypopt,tml,eqns) -> let vars' = - List.fold_right (name_fold Id.Set.add) + List.fold_right (Name.fold_right Id.Set.add) (cases_predicate_names tml) vars in let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in let tml = List.map (fun (tm,(na,x)) -> @@ -790,12 +792,12 @@ let rec extern inctx scopes vars r = let (bl,ty,def) = blv.(i), tyv.(i), bv.(i) in let bl = List.map (extended_glob_local_binder_of_decl ?loc) bl in let (assums,ids,bl) = extern_local_binder scopes vars bl in - let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in - let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in + let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in + let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in let n = match fst nv.(i) with | None -> None - | Some x -> Some (Loc.tag @@ out_name (List.nth assums x)) + | Some x -> Some (Loc.tag @@ Name.get_id (List.nth assums x)) in let ro = extern_recursion_order scopes vars (snd nv.(i)) in ((Loc.tag fi), (n, ro), bl, extern_typ scopes vars0 ty, @@ -807,8 +809,8 @@ let rec extern inctx scopes vars r = Array.mapi (fun i fi -> let bl = List.map (extended_glob_local_binder_of_decl ?loc) blv.(i) in let (_,ids,bl) = extern_local_binder scopes vars bl in - let vars0 = List.fold_right (name_fold Id.Set.add) ids vars in - let vars1 = List.fold_right (name_fold Id.Set.add) ids vars' in + let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in + let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in ((Loc.tag fi),bl,extern_typ scopes vars0 tyv.(i), sub_extern false scopes vars1 bv.(i))) idv in @@ -852,14 +854,14 @@ and extern_local_binder scopes vars = function [] -> ([],[],[]) | { v = GLocalDef (na,bk,bd,ty)}::l -> let (assums,ids,l) = - extern_local_binder scopes (name_fold Id.Set.add na vars) l in + extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l in (assums,na::ids, CLocalDef((Loc.tag na), extern false scopes vars bd, Option.map (extern false scopes vars) ty) :: l) | { v = GLocalAssum (na,bk,ty)}::l -> let ty = extern_typ scopes vars ty in - (match extern_local_binder scopes (name_fold Id.Set.add na vars) l with + (match extern_local_binder scopes (Name.fold_right Id.Set.add na vars) l with (assums,ids,CLocalAssum(nal,k,ty')::l) when constr_expr_eq ty ty' && match na with Name id -> not (occur_var_constr_expr id ty') @@ -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 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 diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 644cafe575..a92e94d97b 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -38,7 +38,7 @@ open Misctypes of [env] *) 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 @@ -61,7 +61,7 @@ val empty_internalization_env : internalization_env val compute_internalization_data : env -> var_internalization_type -> types -> Impargs.manual_explicitation list -> var_internalization_data -val compute_internalization_env : env -> var_internalization_type -> +val compute_internalization_env : env -> ?impls:internalization_env -> var_internalization_type -> Id.t list -> types list -> Impargs.manual_explicitation list list -> internalization_env @@ -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 -> @@ -176,9 +176,9 @@ val interp_context_evars : val locate_reference : Libnames.qualid -> Globnames.global_reference val is_global : Id.t -> bool -val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> constr -val global_reference : Id.t -> constr -val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr +val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> Globnames.global_reference +val global_reference : Id.t -> Globnames.global_reference +val global_reference_in_absolute_module : DirPath.t -> Id.t -> Globnames.global_reference (** Interprets a term as the left-hand side of a notation. The returned map is guaranteed to have the same domain as the input one. *) diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index cfc6e6c2a6..ade524141a 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -264,7 +264,7 @@ let implicits_of_glob_constr ?(with_products=true) l = let () = match bk with | Implicit -> Feedback.msg_warning (strbrk "Ignoring implicit status of product binder " ++ - pr_name na ++ strbrk " and following binders") + Name.print na ++ strbrk " and following binders") | _ -> () in [] | GLambda (na, bk, t, b) -> abs na bk b 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 6f91009111..08b9fbe8ec 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -22,31 +22,6 @@ open Notation_term (**********************************************************************) (* Utilities *) -let on_true_do b f c = if b then (f c; b) else b - -let compare_glob_constr f add t1 t2 = match CAst.(t1.v,t2.v) with - | GRef (r1,_), GRef (r2,_) -> eq_gr r1 r2 - | GVar v1, GVar v2 -> on_true_do (Id.equal v1 v2) add (Name v1) - | GApp (f1,l1), GApp (f2,l2) -> f f1 f2 && List.for_all2eq f l1 l2 - | GLambda (na1,bk1,ty1,c1), GLambda (na2,bk2,ty2,c2) - when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 -> - on_true_do (f ty1 ty2 && f c1 c2) add na1 - | GProd (na1,bk1,ty1,c1), GProd (na2,bk2,ty2,c2) - when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 -> - on_true_do (f ty1 ty2 && f c1 c2) add na1 - | GHole _, GHole _ -> true - | GSort s1, GSort s2 -> Miscops.glob_sort_eq s1 s2 - | GLetIn (na1,b1,t1,c1), GLetIn (na2,b2,t2,c2) when Name.equal na1 na2 -> - on_true_do (f b1 b2 && f c1 c2) add na1 - | (GCases _ | GRec _ - | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_ - | _,(GCases _ | GRec _ - | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _) - -> user_err Pp.(str "Unsupported construction in recursive notations.") - | (GRef _ | GVar _ | GApp _ | GLambda _ | GProd _ - | GHole _ | GSort _ | GLetIn _), _ - -> false - let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with | NRef gr1, NRef gr2 -> eq_gr gr1 gr2 | NVar id1, NVar id2 -> Int.equal (List.index Id.equal id1 vars1) (List.index Id.equal id2 vars2) @@ -184,7 +159,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = e',Some (Loc.tag ?loc (ind,nal')) in let e',na' = g e' na in (e',(f e tm,(na',t'))::tml')) tml (e,[]) in - let fold (idl,e) na = let (e,na) = g e na in ((name_cons na idl,e),na) in + let fold (idl,e) na = let (e,na) = g e na in ((Name.cons na idl,e),na) in let eqnl' = List.map (fun (patl,rhs) -> let ((idl,e),patl) = List.fold_map (cases_pattern_fold_map ?loc fold) ([],e) patl in @@ -287,7 +262,7 @@ let compare_recursive_parts found f f' (iterator,subc) = | Some _ -> false end | GLambda (Name x,_,t_x,c), GLambda (Name y,_,t_y,term) - | GProd (Name x,_,t_x,c), GProd (Name y,_,t_y,term) -> + | GProd (Name x,_,t_x,c), GProd (Name y,_,t_y,term) when not (Id.equal x y) -> (* We found a binding position where it differs *) begin match !diff with | None -> @@ -296,7 +271,7 @@ let compare_recursive_parts found f f' (iterator,subc) = | Some _ -> false end | _ -> - compare_glob_constr aux (add_name found) c1 c2 in + mk_glob_constr_eq aux c1 c2 in if aux iterator subc then match !diff with | None -> @@ -715,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 *) @@ -855,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 diff --git a/interp/topconstr.ml b/interp/topconstr.ml index a79f10df6b..94bbc60eaf 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -83,13 +83,13 @@ let ids_of_cases_tomatch tms = (fun (_, ona, indnal) l -> Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t) indnal - (Option.fold_right (down_located (name_fold Id.Set.add)) ona l)) + (Option.fold_right (down_located (Name.fold_right Id.Set.add)) ona l)) tms Id.Set.empty let rec fold_constr_expr_binders g f n acc b = function | (nal,bk,t)::l -> let nal = snd (List.split nal) in - let n' = List.fold_right (name_fold g) nal n in + let n' = List.fold_right (Name.fold_right g) nal n in f n (fold_constr_expr_binders g f n' acc b l) t | [] -> f n acc b @@ -97,10 +97,10 @@ let rec fold_constr_expr_binders g f n acc b = function let rec fold_local_binders g f n acc b = function | CLocalAssum (nal,bk,t)::l -> let nal = snd (List.split nal) in - let n' = List.fold_right (name_fold g) nal n in + let n' = List.fold_right (Name.fold_right g) nal n in f n (fold_local_binders g f n' acc b l) t | CLocalDef ((_,na),c,t)::l -> - Option.fold_left (f n) (f n (fold_local_binders g f (name_fold g na n) acc b l) c) t + Option.fold_left (f n) (f n (fold_local_binders g f (Name.fold_right g na n) acc b l) c) t | CLocalPattern (_,(pat,t))::l -> let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in Option.fold_left (f n) acc t @@ -112,7 +112,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function | CApp ((_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l) | CProdN (l,b) | CLambdaN (l,b) -> fold_constr_expr_binders g f n acc b l | CLetIn (na,a,t,b) -> - f (name_fold g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b + f (Name.fold_right g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b | CCast (a,CastCoerce) -> f n acc a | CNotation (_,(l,ll,bll)) -> @@ -133,12 +133,12 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function let ids = ids_of_pattern_list patl in f (Id.Set.fold g ids n) acc rhs) bl acc | CLetTuple (nal,(ona,po),b,c) -> - let n' = List.fold_right (down_located (name_fold g)) nal n in - f (Option.fold_right (down_located (name_fold g)) ona n') (f n acc b) c + let n' = List.fold_right (down_located (Name.fold_right g)) nal n in + f (Option.fold_right (down_located (Name.fold_right g)) ona n') (f n acc b) c | CIf (c,(ona,po),b1,b2) -> let acc = f n (f n (f n acc b1) b2) c in Option.fold_left - (f (Option.fold_right (down_located (name_fold g)) ona n)) acc po + (f (Option.fold_right (down_located (Name.fold_right g)) ona n)) acc po | CFix (_,l) -> let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in List.fold_right (fun (_,(_,o),lb,t,c) acc -> @@ -198,7 +198,7 @@ let split_at_annot bl na = (* Used in correctness and interface *) -let map_binder g e nal = List.fold_right (down_located (name_fold g)) nal e +let map_binder g e nal = List.fold_right (down_located (Name.fold_right g)) nal e let map_binders f g e bl = (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) @@ -212,7 +212,7 @@ let map_local_binders f g e bl = CLocalAssum(nal,k,ty) -> (map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl) | CLocalDef((loc,na),c,ty) -> - (name_fold g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl) + (Name.fold_right g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl) | CLocalPattern (loc,(pat,t)) -> let ids = ids_of_pattern pat in (Id.Set.fold g ids e, CLocalPattern (loc,(pat,Option.map (f e) t))::bl) in @@ -228,7 +228,7 @@ let map_constr_expr_with_binders g f e = CAst.map (function | CLambdaN (bl,b) -> let (e,bl) = map_binders f g e bl in CLambdaN (bl,f e b) | CLetIn (na,a,t,b) -> - CLetIn (na,f e a,Option.map (f e) t,f (name_fold g (snd na) e) b) + CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (snd na) e) b) | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c) | CNotation (n,(l,ll,bll)) -> (* This is an approximation because we don't know what binds what *) @@ -247,11 +247,11 @@ let map_constr_expr_with_binders g f e = CAst.map (function let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in CCases (sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl) | CLetTuple (nal,(ona,po),b,c) -> - let e' = List.fold_right (down_located (name_fold g)) nal e in - let e'' = Option.fold_right (down_located (name_fold g)) ona e in + let e' = List.fold_right (down_located (Name.fold_right g)) nal e in + let e'' = Option.fold_right (down_located (Name.fold_right g)) ona e in CLetTuple (nal,(ona,Option.map (f e'') po),f e b,f e' c) | CIf (c,(ona,po),b1,b2) -> - let e' = Option.fold_right (down_located (name_fold g)) ona e in + let e' = Option.fold_right (down_located (Name.fold_right g)) ona e in CIf (f e c,(ona,Option.map (f e') po),f e b1,f e b2) | CFix (id,dl) -> CFix (id,List.map (fun (id,n,bl,t,d) -> |