From 297b0cb44bbe8ec7304ca635c566815167266d4a Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 24 Jun 2015 11:28:44 +0200 Subject: Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080 This reverts 18796b6aea453bdeef1ad12ce80eeb220bf01e67 (Slight change in the semantics of arguments scopes: scopes can no longer be bound to Funclass or Sortclass (this does not seem to be useful)). It is useful to have function_scope for, e.g., function composition. This allows users to, e.g., automatically interpret ∘ as morphism composition when expecting a morphism of categories, as functor composition when expecting a functor, and as function composition when expecting a function. Additionally, it is nicer to have fewer special cases in the OCaml code, and give more things a uniform syntax. (The scope type_scope should not be special-cased; this change is coming up next.) Also explicitly define [function_scope] in theories/Init/Notations.v. This closes bug #3080, Build a [function_scope] like [type_scope], or allow [Bind Scope ... with Sortclass] and [Bind Scope ... with Funclass] We now mention Funclass and Sortclass in the documentation of [Bind Scope] again. --- interp/notation.ml | 37 ++++++++++++------------------------- interp/notation.mli | 7 +++++-- 2 files changed, 17 insertions(+), 27 deletions(-) (limited to 'interp') diff --git a/interp/notation.ml b/interp/notation.ml index d18b804bfd..075e04cba0 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -556,23 +556,16 @@ let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false (**********************************************************************) (* Mapping classes to scopes *) -type scope_class = ScopeRef of global_reference | ScopeSort +open Classops -let scope_class_compare sc1 sc2 = match sc1, sc2 with -| ScopeRef gr1, ScopeRef gr2 -> RefOrdered.compare gr1 gr2 -| ScopeRef _, ScopeSort -> -1 -| ScopeSort, ScopeRef _ -> 1 -| ScopeSort, ScopeSort -> 0 +type scope_class = cl_typ -let scope_class_of_reference x = ScopeRef x +let scope_class_compare : scope_class -> scope_class -> int = + cl_typ_ord let compute_scope_class t = - let t', _ = decompose_appvect (Reductionops.whd_betaiotazeta Evd.empty t) in - match kind_of_term t' with - | Var _ | Const _ | Ind _ -> ScopeRef (global_of_constr t') - | Proj (p, c) -> ScopeRef (ConstRef (Projection.constant p)) - | Sort _ -> ScopeSort - | _ -> raise Not_found + let (cl,_,_) = find_class_type Evd.empty t in + cl module ScopeClassOrd = struct @@ -583,7 +576,7 @@ end module ScopeClassMap = Map.Make(ScopeClassOrd) let initial_scope_class_map : scope_name ScopeClassMap.t = - ScopeClassMap.add ScopeSort "type_scope" ScopeClassMap.empty + ScopeClassMap.add CL_SORT type_scope ScopeClassMap.empty let scope_class_map = ref initial_scope_class_map @@ -617,8 +610,8 @@ let compute_arguments_scope t = fst (compute_arguments_scope_full t) let compute_type_scope t = find_scope_class_opt (try Some (compute_scope_class t) with Not_found -> None) -let compute_scope_of_global ref = - find_scope_class_opt (Some (ScopeRef ref)) +let scope_class_of_class (x : cl_typ) : scope_class = + x (** Updating a scope list, thanks to a list of argument classes and the current Bind Scope base. When some current scope @@ -650,12 +643,8 @@ let load_arguments_scope _ (_,(_,r,scl,cls)) = let cache_arguments_scope o = load_arguments_scope 1 o -let subst_scope_class subst cs = match cs with - | ScopeSort -> Some cs - | ScopeRef t -> - let (t',c) = subst_global subst t in - if t == t' then Some cs - else try Some (compute_scope_class c) with Not_found -> None +let subst_scope_class subst cs = + try Some (subst_cl_typ subst cs) with Not_found -> None let subst_arguments_scope (subst,(req,r,scl,cls)) = let r' = fst (subst_global subst r) in @@ -788,9 +777,7 @@ let pr_delimiters_info = function let classes_of_scope sc = ScopeClassMap.fold (fun cl sc' l -> if String.equal sc sc' then cl::l else l) !scope_class_map [] -let pr_scope_class = function - | ScopeSort -> str "Sort" - | ScopeRef t -> pr_global_env Id.Set.empty t +let pr_scope_class = pr_class let pr_scope_classes sc = let l = classes_of_scope sc in diff --git a/interp/notation.mli b/interp/notation.mli index 38bd5fc7b8..85c4be4cc1 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -153,7 +153,9 @@ val find_arguments_scope : global_reference -> scope_name option list type scope_class -val scope_class_of_reference : global_reference -> scope_class +(** Comparison of scope_class *) +val scope_class_compare : scope_class -> scope_class -> int + val subst_scope_class : Mod_subst.substitution -> scope_class -> scope_class option @@ -162,7 +164,8 @@ val declare_ref_arguments_scope : global_reference -> unit val compute_arguments_scope : Term.types -> scope_name option list val compute_type_scope : Term.types -> scope_name option -val compute_scope_of_global : global_reference -> scope_name option + +val scope_class_of_class : Classops.cl_typ -> scope_class (** Building notation key *) -- cgit v1.2.3 From 6aa58955515dff338ea85d59073dfc0d0c7648ab Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 24 Jun 2015 15:41:11 +0200 Subject: Move type_scope into user space, fix some output logs --- interp/constrextern.ml | 2 +- interp/constrintern.ml | 17 ++++++++++------- interp/notation.ml | 9 +++++---- interp/notation.mli | 4 +++- 4 files changed, 19 insertions(+), 13 deletions(-) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index f57772ecb0..1c60d5c2f7 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -788,7 +788,7 @@ let rec extern inctx scopes vars r = Miscops.map_cast_type (extern_typ scopes vars) c') and extern_typ (_,scopes) = - extern true (Some Notation.type_scope,scopes) + extern true (Notation.current_type_scope_name (),scopes) and sub_extern inctx (_,scopes) = extern inctx (None,scopes) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8c56d0ccfe..d572508a15 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -298,7 +298,7 @@ let set_var_scope loc id istermvar env ntnvars = (* Not in a notation *) () -let set_type_scope env = {env with tmp_scope = Some Notation.type_scope} +let set_type_scope env = {env with tmp_scope = Notation.current_type_scope_name ()} let reset_tmp_scope env = {env with tmp_scope = None} @@ -449,12 +449,15 @@ let intern_generalization intern env lvar loc bk ak c = | Some AbsPi -> true | Some _ -> false | None -> - let is_type_scope = match env.tmp_scope with + match Notation.current_type_scope_name () with + | Some type_scope -> + let is_type_scope = match env.tmp_scope with + | None -> false + | Some sc -> String.equal sc type_scope + in + is_type_scope || + String.List.mem type_scope env.scopes | None -> false - | Some sc -> String.equal sc Notation.type_scope - in - is_type_scope || - String.List.mem Notation.type_scope env.scopes in if pi then (fun (id, loc') acc -> @@ -1755,7 +1758,7 @@ let extract_ids env = Id.Set.empty let scope_of_type_kind = function - | IsType -> Some Notation.type_scope + | IsType -> Notation.current_type_scope_name () | OfType typ -> compute_type_scope typ | WithoutTypeConstraint -> None diff --git a/interp/notation.ml b/interp/notation.ml index 075e04cba0..8395f7d9ad 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -65,11 +65,9 @@ let empty_scope = { } let default_scope = "" (* empty name, not available from outside *) -let type_scope = "type_scope" (* special scope used for interpreting types *) let init_scope_map () = - scope_map := String.Map.add default_scope empty_scope !scope_map; - scope_map := String.Map.add type_scope empty_scope !scope_map + scope_map := String.Map.add default_scope empty_scope !scope_map (**********************************************************************) (* Operations on scopes *) @@ -576,7 +574,7 @@ end module ScopeClassMap = Map.Make(ScopeClassOrd) let initial_scope_class_map : scope_name ScopeClassMap.t = - ScopeClassMap.add CL_SORT type_scope ScopeClassMap.empty + ScopeClassMap.empty let scope_class_map = ref initial_scope_class_map @@ -610,6 +608,9 @@ let compute_arguments_scope t = fst (compute_arguments_scope_full t) let compute_type_scope t = find_scope_class_opt (try Some (compute_scope_class t) with Not_found -> None) +let current_type_scope_name () = + find_scope_class_opt (Some CL_SORT) + let scope_class_of_class (x : cl_typ) : scope_class = x diff --git a/interp/notation.mli b/interp/notation.mli index 85c4be4cc1..2bfbb33c2d 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -29,7 +29,6 @@ type scopes (** = [scope_name list] *) type local_scopes = tmp_scope_name option * scope_name list -val type_scope : scope_name val declare_scope : scope_name -> unit val current_scopes : unit -> scopes @@ -165,6 +164,9 @@ val declare_ref_arguments_scope : global_reference -> unit val compute_arguments_scope : Term.types -> scope_name option list val compute_type_scope : Term.types -> scope_name option +(** Get the current scope bound to Sortclass, if it exists *) +val current_type_scope_name : unit -> scope_name option + val scope_class_of_class : Classops.cl_typ -> scope_class (** Building notation key *) -- cgit v1.2.3 From 6af9f644b64acf485c1628247f5435d09b990b79 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 16 Sep 2015 06:41:04 +0200 Subject: Properly handle {|...|} patterns when patterns are not asymmetric. (Fix bug #4268) --- interp/constrintern.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index ecaf2b8c13..c754f1910c 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1142,7 +1142,11 @@ let drop_notations_pattern looked_for = sort_fields false loc l (fun _ l -> (CPatAtom (loc, None))::l) in begin match sorted_fields with | None -> RCPatAtom (loc, None) - | Some (_, head, pl) -> + | Some (n, head, pl) -> + let pl = + if !oldfashion_patterns then pl else + let pars = List.make n (CPatAtom (loc, None)) in + List.rev_append pars pl in match drop_syndef top env head pl with |Some (a,b,c) -> RCPatCstr(loc, a, b, c) |None -> raise (InternalizationError (loc,NotAConstructor head)) -- cgit v1.2.3 From ed95f122f3c68becc09c653471dc2982b346d343 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 13 Oct 2015 18:30:47 +0200 Subject: Fix some typos. --- interp/implicit_quantifiers.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp') diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index a3721af660..eee9289892 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -28,7 +28,7 @@ val free_vars_of_binders : ?bound:Id.Set.t -> Id.t list -> local_binder list -> Id.Set.t * Id.t list (** Returns the generalizable free ids in left-to-right - order with the location of their first occurence *) + order with the location of their first occurrence *) val generalizable_vars_of_glob_constr : ?bound:Id.Set.t -> ?allowed:Id.Set.t -> glob_constr -> (Id.t * Loc.t) list -- cgit v1.2.3 From d1114c5f55fcb96a99a1a5562b014414ad8217ba Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 24 Oct 2015 18:10:24 +0200 Subject: Documenting a bit more interpretation functions in passing. --- interp/constrintern.mli | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 4d2c994679..b671c98815 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -95,7 +95,8 @@ val intern_context : bool -> env -> internalization_env -> local_binder list -> (** {6 Composing internalization with type inference (pretyping) } *) -(** Main interpretation functions expecting evars to be all resolved *) +(** Main interpretation functions, using type class inference, + expecting evars and pending problems to be all resolved *) val interp_constr : env -> evar_map -> ?impls:internalization_env -> constr_expr -> constr Evd.in_evar_universe_context @@ -106,9 +107,10 @@ val interp_casted_constr : env -> evar_map -> ?impls:internalization_env -> val interp_type : env -> evar_map -> ?impls:internalization_env -> constr_expr -> types Evd.in_evar_universe_context -(** Main interpretation function expecting evars to be all resolved *) +(** Main interpretation function expecting all postponed problems to + be resolved, but possibly leaving evars. *) -val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr +val interp_open_constr : env -> evar_map -> constr_expr -> evar_map * constr (** Accepting unresolved evars *) -- cgit v1.2.3 From 701a69732ef2abfc7384296e090a3e9bd7604bbd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 11 Nov 2015 18:45:32 +0100 Subject: Fixing bug #3554: Anomaly: Anonymous implicit argument. We just handle unnamed implicits using a dummy name. Note that the implicit argument logic should still output warnings whenever the user writes implicit arguments that won't be taken into account, but I'll leave that for another time. --- interp/constrintern.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c754f1910c..8afe630ec5 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -317,7 +317,7 @@ let rec it_mkGLambda loc2 env body = let build_impls = function |Implicit -> (function |Name id -> Some (id, Impargs.Manual, (true,true)) - |Anonymous -> anomaly (Pp.str "Anonymous implicit argument")) + |Anonymous -> Some (Id.of_string "_", Impargs.Manual, (true,true))) |Explicit -> fun _ -> None let impls_type_list ?(args = []) = -- cgit v1.2.3 From 11ccb7333c2a82d59736027838acaea2237e2402 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 26 Nov 2015 18:09:53 +0100 Subject: Make the pretty printer resilient to incomplete nametab (progress on #4363). The nametab in which the error message is printed is not the one in which the error message happens. This reveals a weakness in the fix_exn code: the fix_exn function should be pure, while in some cases (like this one) uses the global state (the nametab) to print a term in a pretty way (the shortest non-ambiguous name for constants). This patch makes the externalization phase (used by term printing) resilient to an incomplete nametab, so that printing a term in the wrong nametab does not mask the original error. --- interp/constrextern.ml | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index f57772ecb0..5160f07af0 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -147,8 +147,17 @@ let extern_evar loc n l = CEvar (loc,n,l) For instance, in the debugger the tables of global references may be inaccurate *) +let safe_shortest_qualid_of_global vars r = + try shortest_qualid_of_global vars r + with Not_found -> + match r with + | VarRef v -> make_qualid DirPath.empty v + | ConstRef c -> make_qualid DirPath.empty Names.(Label.to_id (con_label c)) + | IndRef (i,_) | ConstructRef ((i,_),_) -> + make_qualid DirPath.empty Names.(Label.to_id (mind_label i)) + let default_extern_reference loc vars r = - Qualid (loc,shortest_qualid_of_global vars r) + Qualid (loc,safe_shortest_qualid_of_global vars r) let my_extern_reference = ref default_extern_reference -- cgit v1.2.3 From 16504ad480a920e1800d52f5adbea8ddecefbeb0 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 2 Dec 2015 14:28:29 +0100 Subject: Fix a bug in externalisation which prevented printing of projections using dot notation. --- interp/constrextern.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 5160f07af0..ba20f9fa06 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -447,8 +447,8 @@ let is_projection nargs = function | Some r when not !Flags.in_debugger && not !Flags.raw_print && !print_projections -> (try let n = Recordops.find_projection_nparams r + 1 in - if n <= nargs then None - else Some n + if n <= nargs then Some n + else None with Not_found -> None) | _ -> None -- cgit v1.2.3 From 597e5dd737dd235222798153b2342ae609519348 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 16 Dec 2015 20:03:45 +0100 Subject: Getting rid of some hardwired generic arguments. --- interp/constrarg.ml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) (limited to 'interp') diff --git a/interp/constrarg.ml b/interp/constrarg.ml index a7241399e0..a67143b005 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -36,7 +36,7 @@ let wit_var = unsafe_of_type VarArgType let wit_ref = Genarg.make0 None "ref" -let wit_quant_hyp = unsafe_of_type QuantHypArgType +let wit_quant_hyp = Genarg.make0 None "quant_hyp" let wit_genarg = unsafe_of_type GenArgType @@ -51,14 +51,14 @@ let wit_uconstr = Genarg.make0 None "uconstr" let wit_open_constr = unsafe_of_type OpenConstrArgType -let wit_constr_with_bindings = unsafe_of_type ConstrWithBindingsArgType +let wit_constr_with_bindings = Genarg.make0 None "constr_with_bindings" -let wit_bindings = unsafe_of_type BindingsArgType +let wit_bindings = Genarg.make0 None "bindings" let wit_hyp_location_flag : 'a Genarg.uniform_genarg_type = Genarg.make0 None "hyp_location_flag" -let wit_red_expr = unsafe_of_type RedExprArgType +let wit_red_expr = Genarg.make0 None "redexpr" let wit_clause_dft_concl = Genarg.make0 None "clause_dft_concl" @@ -71,4 +71,8 @@ let () = register_name0 wit_tactic "Constrarg.wit_tactic"; register_name0 wit_sort "Constrarg.wit_sort"; register_name0 wit_uconstr "Constrarg.wit_uconstr"; + register_name0 wit_red_expr "Constrarg.wit_red_expr"; register_name0 wit_clause_dft_concl "Constrarg.wit_clause_dft_concl"; + register_name0 wit_quant_hyp "Constrarg.wit_quant_hyp"; + register_name0 wit_bindings "Constrarg.wit_bindings"; + register_name0 wit_constr_with_bindings "Constrarg.wit_constr_with_bindings"; -- cgit v1.2.3 From 1b5f85d38db7a0d7cb9a4b9491a5563461373182 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 17:31:25 +0100 Subject: CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified --- interp/constrexpr_ops.ml | 2 +- interp/constrextern.ml | 43 +++++++++++++++++++++++-------------------- interp/constrintern.ml | 8 ++++---- interp/topconstr.ml | 6 +++--- 4 files changed, 31 insertions(+), 28 deletions(-) (limited to 'interp') diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 2d48ea4d07..161fd1eb1d 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -178,7 +178,7 @@ and args_eq (a1,e1) (a2,e2) = Option.equal (eq_located explicitation_eq) e1 e2 && constr_expr_eq a1 a2 -and case_expr_eq (e1, (n1, p1)) (e2, (n2, p2)) = +and case_expr_eq (e1, n1, p1) (e2, n2, p2) = constr_expr_eq e1 e2 && Option.equal (eq_located Name.equal) n1 n2 && Option.equal cases_pattern_expr_eq p1 p2 diff --git a/interp/constrextern.ml b/interp/constrextern.ml index ba20f9fa06..ed85c38de0 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -721,26 +721,29 @@ let rec extern inctx scopes vars r = (cases_predicate_names tml) vars in let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in let tml = List.map (fun (tm,(na,x)) -> - let na' = match na,tm with - | Anonymous, GVar (_, id) -> - begin match rtntypopt with - | None -> None - | Some ntn -> - if occur_glob_constr id ntn then - Some (Loc.ghost, Anonymous) - else None - end - | Anonymous, _ -> None - | Name id, GVar (_,id') when Id.equal id id' -> None - | Name _, _ -> Some (Loc.ghost,na) in - (sub_extern false scopes vars tm, - (na',Option.map (fun (loc,ind,nal) -> - let args = List.map (fun x -> PatVar (Loc.ghost, x)) nal in - let fullargs = - if !Flags.in_debugger then args else - Notation_ops.add_patterns_for_params ind args in - extern_ind_pattern_in_scope scopes vars ind fullargs - ) x))) tml in + let na' = match na,tm with + | Anonymous, GVar (_, id) -> + begin match rtntypopt with + | None -> None + | Some ntn -> + if occur_glob_constr id ntn then + Some (Loc.ghost, Anonymous) + else None + end + | Anonymous, _ -> None + | Name id, GVar (_,id') when Id.equal id id' -> None + | Name _, _ -> Some (Loc.ghost,na) in + (sub_extern false scopes vars tm, + na', + Option.map (fun (loc,ind,nal) -> + let args = List.map (fun x -> PatVar (Loc.ghost, x)) nal in + let fullargs = + if !Flags.in_debugger then args else + Notation_ops.add_patterns_for_params ind args in + extern_ind_pattern_in_scope scopes vars ind fullargs + ) x)) + tml + in let eqns = List.map (extern_eqn inctx scopes vars) eqns in CCases (loc,sty,rtntypopt',tml,eqns) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8afe630ec5..8a86d30220 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1506,7 +1506,7 @@ let internalize globalenv env allow_patvar lvar c = intern env app end | CCases (loc, sty, rtnpo, tms, eqns) -> - let as_in_vars = List.fold_left (fun acc (_,(na,inb)) -> + let as_in_vars = List.fold_left (fun acc (_,na,inb) -> Option.fold_left (fun x tt -> List.fold_right Id.Set.add (ids_of_cases_indtype tt) x) (Option.fold_left (fun x (_,y) -> match y with | Name y' -> Id.Set.add y' x |_ -> x) acc na) inb) Id.Set.empty tms in @@ -1542,7 +1542,7 @@ let internalize globalenv env allow_patvar lvar c = | CLetTuple (loc, nal, (na,po), b, c) -> let env' = reset_tmp_scope env in (* "in" is None so no match to add *) - let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,(na,None)) in + let ((b',(na',_)),_,_) = intern_case_item env' Id.Set.empty (b,na,None) in let p' = Option.map (fun u -> let env'' = push_name_env lvar (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env') (Loc.ghost,na') in @@ -1551,7 +1551,7 @@ let internalize globalenv env allow_patvar lvar c = intern (List.fold_left (push_name_env lvar (Variable,[],[],[])) (reset_hidden_inductive_implicit_test env) nal) c) | CIf (loc, c, (na,po), b1, b2) -> let env' = reset_tmp_scope env in - let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,(na,None)) in (* no "in" no match to ad too *) + let ((c',(na',_)),_,_) = intern_case_item env' Id.Set.empty (c,na,None) in (* no "in" no match to ad too *) let p' = Option.map (fun p -> let env'' = push_name_env lvar (Variable,[],[],[]) (reset_hidden_inductive_implicit_test env) (Loc.ghost,na') in @@ -1628,7 +1628,7 @@ let internalize globalenv env allow_patvar lvar c = let rhs' = intern {env with ids = env_ids} rhs in (loc,eqn_ids,pl,rhs')) pll - and intern_case_item env forbidden_names_for_gen (tm,(na,t)) = + and intern_case_item env forbidden_names_for_gen (tm,na,t) = (*the "match" part *) let tm' = intern env tm in (* the "as" part *) diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 1231f11555..15ac46e29e 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -51,7 +51,7 @@ let ids_of_cases_indtype = let ids_of_cases_tomatch tms = List.fold_right - (fun (_,(ona,indnal)) l -> + (fun (_,ona,indnal) l -> Option.fold_right (fun t -> (@) (ids_of_cases_indtype t)) indnal (Option.fold_right (Loc.down_located name_cons) ona l)) tms [] @@ -120,7 +120,7 @@ let fold_constr_expr_with_binders g f n acc = function | CCases (loc,sty,rtnpo,al,bl) -> let ids = ids_of_cases_tomatch al in let acc = Option.fold_left (f (List.fold_right g ids n)) acc rtnpo in - let acc = List.fold_left (f n) acc (List.map fst al) in + let acc = List.fold_left (f n) acc (List.map (fun (fst,_,_) -> fst) al) in List.fold_right (fun (loc,patl,rhs) acc -> let ids = ids_of_pattern_list patl in f (Id.Set.fold g ids n) acc rhs) bl acc @@ -224,7 +224,7 @@ let map_constr_expr_with_binders g f e = function let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in let ids = ids_of_cases_tomatch a in let po = Option.map (f (List.fold_right g ids e)) rtnpo in - CCases (loc, sty, po, List.map (fun (tm,x) -> (f e tm,x)) a,bl) + CCases (loc, sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl) | CLetTuple (loc,nal,(ona,po),b,c) -> let e' = List.fold_right (Loc.down_located (name_fold g)) nal e in let e'' = Option.fold_right (Loc.down_located (name_fold g)) ona e in -- cgit v1.2.3 From 329b5b9ed526d572d7df066dc99486e1dcb9e4cc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 18 Dec 2015 17:18:06 +0100 Subject: Removing the now useless genarg generic argument. --- interp/constrarg.ml | 2 -- interp/constrarg.mli | 2 -- 2 files changed, 4 deletions(-) (limited to 'interp') diff --git a/interp/constrarg.ml b/interp/constrarg.ml index a67143b005..84b056ab68 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -38,8 +38,6 @@ let wit_ref = Genarg.make0 None "ref" let wit_quant_hyp = Genarg.make0 None "quant_hyp" -let wit_genarg = unsafe_of_type GenArgType - let wit_sort : (glob_sort, glob_sort, sorts) genarg_type = Genarg.make0 None "sort" diff --git a/interp/constrarg.mli b/interp/constrarg.mli index fdeddd66a1..ef1ef4aee4 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -38,8 +38,6 @@ val wit_ref : (reference, global_reference located or_var, global_reference) gen val wit_quant_hyp : quantified_hypothesis uniform_genarg_type -val wit_genarg : (raw_generic_argument, glob_generic_argument, typed_generic_argument) genarg_type - val wit_sort : (glob_sort, glob_sort, sorts) genarg_type val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type -- cgit v1.2.3 From 589130e87d68227d25800e7506666eaf1d47a25a Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 18 Dec 2015 17:30:09 +0100 Subject: Changing the toplevel type of the int_or_var generic type to int. --- interp/constrarg.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp') diff --git a/interp/constrarg.mli b/interp/constrarg.mli index ef1ef4aee4..f2f314eea0 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -26,7 +26,7 @@ val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t (** {5 Additional generic arguments} *) -val wit_int_or_var : int or_var uniform_genarg_type +val wit_int_or_var : (int or_var, int or_var, int) genarg_type val wit_intro_pattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type -- cgit v1.2.3 From 9b02ddf179b375cb09966b70dd3b119eda0d92c1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 18 Dec 2015 17:51:53 +0100 Subject: Sharing toplevel representation for several generic types. - int and int_or_var - ident and var - constr and constr_may_eval --- interp/stdarg.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'interp') diff --git a/interp/stdarg.ml b/interp/stdarg.ml index e155a5217d..5cfe3854a9 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -15,7 +15,9 @@ let wit_bool : bool uniform_genarg_type = make0 None "bool" let wit_int : int uniform_genarg_type = - make0 None "int" + make0 ~dyn:(val_tag (Obj.magic IntOrVarArgType)) None "int" +(** FIXME: IntOrVarArgType is hardwired, but that definition should be the other + way around. *) let wit_string : string uniform_genarg_type = make0 None "string" -- cgit v1.2.3 From 5835804bd69a193b9ea29b6d4c8d0cc03530ccdd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 18 Dec 2015 18:04:14 +0100 Subject: Removing ad-hoc interpretation rules for tactic notations and their genarg. Now that types can share the same dynamic representation, we do not have to transtype the topelvel values dynamically and just take advantage of the standard interpretation function. --- interp/constrarg.ml | 8 ++++++-- interp/stdarg.ml | 4 +--- 2 files changed, 7 insertions(+), 5 deletions(-) (limited to 'interp') diff --git a/interp/constrarg.ml b/interp/constrarg.ml index 84b056ab68..ab54b61977 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -22,7 +22,8 @@ let loc_of_or_by_notation f = function let unsafe_of_type (t : argument_type) : ('a, 'b, 'c) Genarg.genarg_type = Obj.magic t -let wit_int_or_var = unsafe_of_type IntOrVarArgType +let wit_int_or_var = + Genarg.make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) None "int_or_var" let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type = Genarg.make0 None "intropattern" @@ -43,7 +44,8 @@ let wit_sort : (glob_sort, glob_sort, sorts) genarg_type = let wit_constr = unsafe_of_type ConstrArgType -let wit_constr_may_eval = unsafe_of_type ConstrMayEvalArgType +let wit_constr_may_eval = + Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) None "constr_may_eval" let wit_uconstr = Genarg.make0 None "uconstr" @@ -64,11 +66,13 @@ let wit_clause_dft_concl = (** Register location *) let () = + register_name0 wit_int_or_var "Constrarg.wit_int_or_var"; register_name0 wit_ref "Constrarg.wit_ref"; register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern"; register_name0 wit_tactic "Constrarg.wit_tactic"; register_name0 wit_sort "Constrarg.wit_sort"; register_name0 wit_uconstr "Constrarg.wit_uconstr"; + register_name0 wit_constr_may_eval "Constrarg.wit_constr_may_eval"; register_name0 wit_red_expr "Constrarg.wit_red_expr"; register_name0 wit_clause_dft_concl "Constrarg.wit_clause_dft_concl"; register_name0 wit_quant_hyp "Constrarg.wit_quant_hyp"; diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 5cfe3854a9..e155a5217d 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -15,9 +15,7 @@ let wit_bool : bool uniform_genarg_type = make0 None "bool" let wit_int : int uniform_genarg_type = - make0 ~dyn:(val_tag (Obj.magic IntOrVarArgType)) None "int" -(** FIXME: IntOrVarArgType is hardwired, but that definition should be the other - way around. *) + make0 None "int" let wit_string : string uniform_genarg_type = make0 None "string" -- cgit v1.2.3 From 602badcad9deec9224b78cd1e1033af30358ef2e Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Dec 2015 22:35:09 +0100 Subject: Do not compose "str" and "to_string" whenever possible. For instance, calling only Id.print is faster than calling both str and Id.to_string, since the latter performs a copy. It also makes the code a bit simpler to read. --- interp/coqlib.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp') diff --git a/interp/coqlib.ml b/interp/coqlib.ml index 5ac718e3b0..b309f26cd6 100644 --- a/interp/coqlib.ml +++ b/interp/coqlib.ml @@ -87,7 +87,7 @@ let check_required_library d = *) (* or failing ...*) errorlabstrm "Coqlib.check_required_library" - (str "Library " ++ str (DirPath.to_string dir) ++ str " has to be required first.") + (str "Library " ++ pr_dirpath dir ++ str " has to be required first.") (************************************************************************) (* Specific Coq objects *) -- cgit v1.2.3 From 77e6eda6388aba117476f6c8445c4b61ebdbc33e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 27 Dec 2015 00:44:58 +0100 Subject: Tentative API fix for tactic arguments to be fed to tclWITHHOLES. The previous implementation was a source of evar leaks if misused, as it created values coming together with their current evar_map. This is dead wrong if the value is not used on the spot. To fix this, we rather return a ['a delayed_open] object. Two argument types were modified: bindings and constr_bindings. The open_constr argument should also be fixed, but it is more entangled and thus I leave it for another commit. --- interp/constrarg.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'interp') diff --git a/interp/constrarg.mli b/interp/constrarg.mli index f2f314eea0..052e4ec69b 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -55,12 +55,12 @@ val wit_open_constr : val wit_constr_with_bindings : (constr_expr with_bindings, glob_constr_and_expr with_bindings, - constr with_bindings Evd.sigma) genarg_type + constr with_bindings delayed_open) genarg_type val wit_bindings : (constr_expr bindings, glob_constr_and_expr bindings, - constr bindings Evd.sigma) genarg_type + constr bindings delayed_open) genarg_type val wit_hyp_location_flag : Locus.hyp_location_flag uniform_genarg_type -- cgit v1.2.3 From cb2f6a95ee72edb956f419a24f8385c8ae7f96f4 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 28 Dec 2015 02:08:42 +0100 Subject: Removing the special status of open_constr generic argument. We also intepret it at toplevel as a true constr and push the resulting evarmap in the current state. --- interp/constrarg.ml | 3 ++- interp/constrarg.mli | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) (limited to 'interp') diff --git a/interp/constrarg.ml b/interp/constrarg.ml index ab54b61977..44623f9c9a 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -49,7 +49,7 @@ let wit_constr_may_eval = let wit_uconstr = Genarg.make0 None "uconstr" -let wit_open_constr = unsafe_of_type OpenConstrArgType +let wit_open_constr = Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) None "open_constr" let wit_constr_with_bindings = Genarg.make0 None "constr_with_bindings" @@ -72,6 +72,7 @@ let () = register_name0 wit_tactic "Constrarg.wit_tactic"; register_name0 wit_sort "Constrarg.wit_sort"; register_name0 wit_uconstr "Constrarg.wit_uconstr"; + register_name0 wit_open_constr "Constrarg.wit_open_constr"; register_name0 wit_constr_may_eval "Constrarg.wit_constr_may_eval"; register_name0 wit_red_expr "Constrarg.wit_red_expr"; register_name0 wit_clause_dft_concl "Constrarg.wit_clause_dft_concl"; diff --git a/interp/constrarg.mli b/interp/constrarg.mli index 052e4ec69b..0cc111e617 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -50,7 +50,7 @@ val wit_constr_may_eval : val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type val wit_open_constr : - (open_constr_expr, open_glob_constr, Evd.open_constr) genarg_type + (constr_expr, glob_constr_and_expr, constr) genarg_type val wit_constr_with_bindings : (constr_expr with_bindings, -- cgit v1.2.3 From d3bc575c498ae09ad1003405d17a9d5cfbcf3cbf Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 31 Dec 2015 17:00:42 +0100 Subject: Do not dump a glob reference when its location is ghost. (Fix bug #4469) This patch also causes the code to finish a bit faster in the NoGlob case by not preparing a string for dump_string. It also optimizes Dumpglob.is_ghost by only checking whether the end position is zero. Note that no ghost locations were part of the glob files of the standard library before the patch. Note also that the html documentation of the standard library is bitwise identical before and after the patch. --- interp/dumpglob.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'interp') diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index c18ceecaba..c7d3da653c 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -139,12 +139,15 @@ let interval loc = loc1, loc2-1 let dump_ref loc filepath modpath ident ty = - if !glob_output = Feedback then + match !glob_output with + | Feedback -> Pp.feedback (Feedback.GlobRef (loc, filepath, modpath, ident, ty)) - else + | NoGlob -> () + | _ when not (Loc.is_ghost loc) -> let bl,el = interval loc in dump_string (Printf.sprintf "R%d:%d %s %s %s %s\n" bl el filepath modpath ident ty) + | _ -> () let dump_reference loc modpath ident ty = let filepath = Names.DirPath.to_string (Lib.library_dp ()) in -- cgit v1.2.3 From 1a157442dff4bfa127af467c49280e79889acde7 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 26 Dec 2015 10:07:19 +0100 Subject: Do not compose List.length with List.filter. --- interp/constrintern.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8a86d30220..d4cb797759 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1386,7 +1386,7 @@ let internalize globalenv env allow_patvar lvar c = let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in let ro = f (intern env') in - let n' = Option.map (fun _ -> List.length (List.filter (fun (_,(_,_,b,_)) -> (* remove let-ins *) b = None) rbefore)) n in + let n' = Option.map (fun _ -> List.count (fun (_,(_,_,b,_)) -> (* remove let-ins *) b = None) rbefore) n in n', ro, List.fold_left intern_local_binder (env',rbefore) after in let n, ro, (env',rbl) = -- cgit v1.2.3 From 80bbdf335be5657f5ab33b4aa02e21420d341de2 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 2 Jan 2016 17:11:03 +0100 Subject: Remove some unused functions. Note: they do not even seem to have a debugging purpose, so better remove them before they bitrot. --- interp/constrextern.ml | 9 --------- interp/constrintern.ml | 13 ------------- 2 files changed, 22 deletions(-) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index ed85c38de0..5c9e80df3d 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -462,15 +462,6 @@ let is_needed_for_correct_partial_application tail imp = exception Expl -let params_implicit n impl = - let rec aux n impl = - if n == 0 then true - else match impl with - | [] -> false - | imp :: impl when is_status_implicit imp -> aux (pred n) impl - | _ -> false - in aux n impl - (* Implicit args indexes are in ascending order *) (* inctx is useful only if there is a last argument to be deduced from ctxt *) let explicitize loc inctx impl (cf,f) args = diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d4cb797759..f9de8c4663 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -698,19 +698,6 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id = (* [id] a goal variable *) GVar (loc,id), [], [], [] -let proj_impls r impls = - let env = Global.env () in - let f (x, l) = x, projection_implicits env r l in - List.map f impls - -let proj_scopes n scopes = - List.skipn_at_least n scopes - -let proj_impls_scopes p impls scopes = - match p with - | Some (r, n) -> proj_impls r impls, proj_scopes n scopes - | None -> impls, scopes - let find_appl_head_data c = match c with | GRef (loc,ref,_) as x -> -- cgit v1.2.3 From 9d991d36c07efbb6428e277573bd43f6d56788fc Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 8 Jan 2016 10:00:21 +0100 Subject: CLEANUP: kernel/context.ml{,i} The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed. --- interp/constrextern.mli | 3 +-- interp/constrintern.ml | 4 ++-- interp/constrintern.mli | 5 ++--- 3 files changed, 5 insertions(+), 7 deletions(-) (limited to 'interp') diff --git a/interp/constrextern.mli b/interp/constrextern.mli index b797e455c0..ff8ca0b7cc 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Termops open Environ open Libnames @@ -42,7 +41,7 @@ val extern_reference : Loc.t -> Id.Set.t -> global_reference -> reference val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr val extern_sort : Evd.evar_map -> sorts -> glob_sort val extern_rel_context : constr option -> env -> Evd.evar_map -> - rel_context -> local_binder list + Context.Rel.t -> local_binder list (** Printing options *) val print_implicits : bool ref diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8a86d30220..918b75b0c1 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -101,7 +101,7 @@ let global_reference id = let construct_reference ctx id = try - Term.mkVar (let _ = Context.lookup_named id ctx in id) + Term.mkVar (let _ = Context.Named.lookup id ctx in id) with Not_found -> global_reference id @@ -685,7 +685,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id = str "variable " ++ pr_id id ++ str " should be bound to a term.") else (* Is [id] a goal or section variable *) - let _ = Context.lookup_named id namedctx in + let _ = Context.Named.lookup id namedctx in try (* [id] a section variable *) (* Redundant: could be done in intern_qualid *) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index b671c98815..c851fbb369 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -8,7 +8,6 @@ open Names open Term -open Context open Evd open Environ open Libnames @@ -161,7 +160,7 @@ val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> types val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int -> env -> evar_map ref -> local_binder list -> - internalization_env * ((env * rel_context) * Impargs.manual_implicits) + internalization_env * ((env * Context.Rel.t) * Impargs.manual_implicits) (* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *) (* (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *) @@ -178,7 +177,7 @@ val interp_context_evars : val locate_reference : Libnames.qualid -> Globnames.global_reference val is_global : Id.t -> bool -val construct_reference : named_context -> Id.t -> constr +val construct_reference : Context.Named.t -> Id.t -> constr val global_reference : Id.t -> constr val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr -- cgit v1.2.3 From a1aff01d16bad2f44392fd5cb804092e12e558ed Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Wed, 16 Dec 2015 16:19:51 +0100 Subject: CLEANUP: removing unused field I have removed the second field of the "Constrexpr.CRecord" variant because once it was set to "None" it never changed to anything else. It was just carried and copied around. --- interp/constrexpr_ops.ml | 5 ++--- interp/constrextern.ml | 2 +- interp/constrintern.ml | 2 +- interp/topconstr.ml | 4 ++-- 4 files changed, 6 insertions(+), 7 deletions(-) (limited to 'interp') diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 161fd1eb1d..a97e8e6db7 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -125,11 +125,10 @@ let rec constr_expr_eq e1 e2 = Option.equal Int.equal proj1 proj2 && constr_expr_eq e1 e2 && List.equal args_eq al1 al2 - | CRecord (_, e1, l1), CRecord (_, e2, l2) -> + | CRecord (_, l1), CRecord (_, l2) -> let field_eq (r1, e1) (r2, e2) = eq_reference r1 r2 && constr_expr_eq e1 e2 in - Option.equal constr_expr_eq e1 e2 && List.equal field_eq l1 l2 | CCases(_,_,r1,a1,brl1), CCases(_,_,r2,a2,brl2) -> (** Don't care about the case_style *) @@ -238,7 +237,7 @@ let constr_loc = function | CLetIn (loc,_,_,_) -> loc | CAppExpl (loc,_,_) -> loc | CApp (loc,_,_) -> loc - | CRecord (loc,_,_) -> loc + | CRecord (loc,_) -> loc | CCases (loc,_,_,_,_) -> loc | CLetTuple (loc,_,_,_,_) -> loc | CIf (loc,_,_,_,_) -> loc diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 5c9e80df3d..af2206d968 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -680,7 +680,7 @@ let rec extern inctx scopes vars r = | head :: tail -> ip q locs' tail ((extern_reference loc Id.Set.empty (ConstRef c), head) :: acc) in - CRecord (loc, None, List.rev (ip projs locals args [])) + CRecord (loc, List.rev (ip projs locals args [])) with | Not_found | No_match | Exit -> extern_app loc inctx diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 68bc0b1092..c0203b0666 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1479,7 +1479,7 @@ let internalize globalenv env allow_patvar lvar c = apply_impargs c env impargs args_scopes (merge_impargs l args) loc - | CRecord (loc, _, fs) -> + | CRecord (loc, fs) -> let cargs = sort_fields true loc fs (fun k l -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true)), Misctypes.IntroAnonymous, None) :: l) diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 15ac46e29e..837630183e 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -116,7 +116,7 @@ let fold_constr_expr_with_binders g f n acc = function | CDelimiters (loc,_,a) -> f n acc a | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CRef _ -> acc - | CRecord (loc,_,l) -> List.fold_left (fun acc (id, c) -> f n acc c) acc l + | CRecord (loc,l) -> List.fold_left (fun acc (id, c) -> f n acc c) acc l | CCases (loc,sty,rtnpo,al,bl) -> let ids = ids_of_cases_tomatch al in let acc = Option.fold_left (f (List.fold_right g ids n)) acc rtnpo in @@ -218,7 +218,7 @@ let map_constr_expr_with_binders g f e = function | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a) | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CRef _ as x -> x - | CRecord (loc,p,l) -> CRecord (loc,p,List.map (fun (id, c) -> (id, f e c)) l) + | CRecord (loc,l) -> CRecord (loc,List.map (fun (id, c) -> (id, f e c)) l) | CCases (loc,sty,rtnpo,a,bl) -> (* TODO: apply g on the binding variables in pat... *) let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in -- cgit v1.2.3 From 9f8ae1aa2678944888d80ce0867bfb2bba0c8c71 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 12 Jan 2016 22:12:40 +0100 Subject: Fixing #4467 (missing shadowing of variables in cases pattern). This fixes a TODO in map_constr_expr_with_binders, a bug in is_constructor, as well as a bug and TODOS in ids_of_cases_indtype. --- interp/topconstr.ml | 40 +++++++++++++++++----------------------- 1 file changed, 17 insertions(+), 23 deletions(-) (limited to 'interp') diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 1231f11555..560cd0277b 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -38,27 +38,9 @@ let error_invalid_pattern_notation loc = (**********************************************************************) (* Functions on constr_expr *) -let ids_of_cases_indtype = - let rec vars_of ids = function - (* We deal only with the regular cases *) - | (CPatCstr (_,_,l1,l2)|CPatNotation (_,_,(l1,[]),l2)) -> - List.fold_left vars_of (List.fold_left vars_of [] l2) l1 - (* assume the ntn is applicative and does not instantiate the head !! *) - | CPatDelimiters(_,_,c) -> vars_of ids c - | CPatAtom (_, Some (Libnames.Ident (_, x))) -> x::ids - | _ -> ids in - vars_of [] - -let ids_of_cases_tomatch tms = - List.fold_right - (fun (_,(ona,indnal)) l -> - Option.fold_right (fun t -> (@) (ids_of_cases_indtype t)) - indnal (Option.fold_right (Loc.down_located name_cons) ona l)) - tms [] - let is_constructor id = try ignore (Nametab.locate_extended (qualid_of_ident id)); true - with Not_found -> true + with Not_found -> false let rec cases_pattern_fold_names f a = function | CPatRecord (_, l) -> @@ -82,6 +64,17 @@ let ids_of_pattern_list = (List.fold_left (cases_pattern_fold_names Id.Set.add))) Id.Set.empty +let ids_of_cases_indtype p = + Id.Set.elements (cases_pattern_fold_names Id.Set.add Id.Set.empty p) + +let ids_of_cases_tomatch tms = + List.fold_right + (fun (_,(ona,indnal)) l -> + Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t) + indnal + (Option.fold_right (Loc.down_located (name_fold 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 @@ -119,7 +112,7 @@ let fold_constr_expr_with_binders g f n acc = function | CRecord (loc,_,l) -> List.fold_left (fun acc (id, c) -> f n acc c) acc l | CCases (loc,sty,rtnpo,al,bl) -> let ids = ids_of_cases_tomatch al in - let acc = Option.fold_left (f (List.fold_right g ids n)) acc rtnpo in + let acc = Option.fold_left (f (Id.Set.fold g ids n)) acc rtnpo in let acc = List.fold_left (f n) acc (List.map fst al) in List.fold_right (fun (loc,patl,rhs) acc -> let ids = ids_of_pattern_list patl in @@ -220,10 +213,11 @@ let map_constr_expr_with_binders g f e = function | CPrim _ | CRef _ as x -> x | CRecord (loc,p,l) -> CRecord (loc,p,List.map (fun (id, c) -> (id, f e c)) l) | CCases (loc,sty,rtnpo,a,bl) -> - (* TODO: apply g on the binding variables in pat... *) - let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in + let bl = List.map (fun (loc,patl,rhs) -> + let ids = ids_of_pattern_list patl in + (loc,patl,f (Id.Set.fold g ids e) rhs)) bl in let ids = ids_of_cases_tomatch a in - let po = Option.map (f (List.fold_right g ids e)) rtnpo in + let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in CCases (loc, sty, po, List.map (fun (tm,x) -> (f e tm,x)) a,bl) | CLetTuple (loc,nal,(ona,po),b,c) -> let e' = List.fold_right (Loc.down_located (name_fold g)) nal e in -- cgit v1.2.3 From 2d568a895d5c8a246f497c94c79811d3aad4269f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 13 Jan 2016 00:20:46 +0100 Subject: Fixing #4467 (continued). Function is_constructor was not properly fixed. Additionally, this fixes a problem with the 8.5 interpretation of in-pattern (see Cases.v). --- interp/interp.mllib | 2 +- interp/topconstr.ml | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) (limited to 'interp') diff --git a/interp/interp.mllib b/interp/interp.mllib index c9a0315267..96b52959a0 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -3,12 +3,12 @@ Constrarg Genintern Constrexpr_ops Notation_ops -Topconstr Ppextend Notation Dumpglob Syntax_def Smartlocate +Topconstr Reserve Impargs Implicit_quantifiers diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 560cd0277b..2cb2449b7d 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -39,7 +39,9 @@ let error_invalid_pattern_notation loc = (* Functions on constr_expr *) let is_constructor id = - try ignore (Nametab.locate_extended (qualid_of_ident id)); true + try Globnames.isConstructRef + (Smartlocate.global_of_extended_global + (Nametab.locate_extended (qualid_of_ident id))) with Not_found -> false let rec cases_pattern_fold_names f a = function -- cgit v1.2.3 From 67b9b34d409c793dc449104525684852353ee064 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 11 Jan 2016 21:40:23 +0100 Subject: Removing ident and var generic arguments. --- interp/constrarg.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'interp') diff --git a/interp/constrarg.ml b/interp/constrarg.ml index 44623f9c9a..94c13fe796 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -31,9 +31,11 @@ let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob let wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type = Genarg.make0 None "tactic" -let wit_ident = unsafe_of_type IdentArgType +let wit_ident = + Genarg.make0 None "ident" -let wit_var = unsafe_of_type VarArgType +let wit_var = + Genarg.make0 ~dyn:(val_tag (topwit wit_ident)) None "var" let wit_ref = Genarg.make0 None "ref" @@ -68,6 +70,8 @@ let wit_clause_dft_concl = let () = register_name0 wit_int_or_var "Constrarg.wit_int_or_var"; register_name0 wit_ref "Constrarg.wit_ref"; + register_name0 wit_ident "Constrarg.wit_ident"; + register_name0 wit_var "Constrarg.wit_var"; register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern"; register_name0 wit_tactic "Constrarg.wit_tactic"; register_name0 wit_sort "Constrarg.wit_sort"; -- cgit v1.2.3 From 448866f0ec5291d58677d8fccbefde493ade0ee2 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 11 Jan 2016 22:20:16 +0100 Subject: Removing constr generic argument. --- interp/constrarg.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'interp') diff --git a/interp/constrarg.ml b/interp/constrarg.ml index 94c13fe796..a8dfd02e1d 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -44,7 +44,8 @@ let wit_quant_hyp = Genarg.make0 None "quant_hyp" let wit_sort : (glob_sort, glob_sort, sorts) genarg_type = Genarg.make0 None "sort" -let wit_constr = unsafe_of_type ConstrArgType +let wit_constr = + Genarg.make0 None "constr" let wit_constr_may_eval = Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) None "constr_may_eval" @@ -75,6 +76,7 @@ let () = register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern"; register_name0 wit_tactic "Constrarg.wit_tactic"; register_name0 wit_sort "Constrarg.wit_sort"; + register_name0 wit_constr "Constrarg.wit_constr"; register_name0 wit_uconstr "Constrarg.wit_uconstr"; register_name0 wit_open_constr "Constrarg.wit_open_constr"; register_name0 wit_constr_may_eval "Constrarg.wit_constr_may_eval"; -- cgit v1.2.3 From 0d1345ea2423fc418a470786b0b33b80df3a67bc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 17 Jan 2016 01:08:21 +0100 Subject: Temporary commit getting rid of Obj.magic unsafety for Genarg. This will allow an easier landing of the rewriting of Genarg. --- interp/constrarg.ml | 3 --- 1 file changed, 3 deletions(-) (limited to 'interp') diff --git a/interp/constrarg.ml b/interp/constrarg.ml index a8dfd02e1d..f8957a24b8 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -19,9 +19,6 @@ let loc_of_or_by_notation f = function | AN c -> f c | ByNotation (loc,s,_) -> loc -let unsafe_of_type (t : argument_type) : ('a, 'b, 'c) Genarg.genarg_type = - Obj.magic t - let wit_int_or_var = Genarg.make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) None "int_or_var" -- cgit v1.2.3 From d3ee6b2fbcd0fbb666af7f1920446e809e8d6e1e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 17 Jan 2016 01:58:05 +0100 Subject: Getting rid of the awkward unpack mechanism from Genarg. --- interp/genintern.ml | 14 +++++--------- 1 file changed, 5 insertions(+), 9 deletions(-) (limited to 'interp') diff --git a/interp/genintern.ml b/interp/genintern.ml index 7795946d56..7a5f84704f 100644 --- a/interp/genintern.ml +++ b/interp/genintern.ml @@ -37,20 +37,16 @@ module Subst = Register (SubstObj) let intern = Intern.obj let register_intern0 = Intern.register0 -let generic_intern ist v = - let unpacker wit v = - let (ist, v) = intern wit ist (raw v) in - (ist, in_gen (glbwit wit) v) - in - unpack { unpacker; } v +let generic_intern ist (GenArg (Rawwit wit, v)) = + let (ist, v) = intern wit ist v in + (ist, in_gen (glbwit wit) v) (** Substitution functions *) let substitute = Subst.obj let register_subst0 = Subst.register0 -let generic_substitute subs v = - let unpacker wit v = in_gen (glbwit wit) (substitute wit subs (glb v)) in - unpack { unpacker; } v +let generic_substitute subs (GenArg (Glbwit wit, v)) = + in_gen (glbwit wit) (substitute wit subs v) let () = Hook.set Detyping.subst_genarg_hook generic_substitute -- cgit v1.2.3 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- interp/constrarg.ml | 2 +- interp/constrarg.mli | 2 +- interp/constrexpr_ops.ml | 2 +- interp/constrexpr_ops.mli | 2 +- interp/constrextern.ml | 2 +- interp/constrextern.mli | 2 +- interp/constrintern.ml | 2 +- interp/constrintern.mli | 2 +- interp/coqlib.ml | 2 +- interp/coqlib.mli | 2 +- interp/dumpglob.ml | 2 +- interp/dumpglob.mli | 2 +- interp/genintern.ml | 2 +- interp/genintern.mli | 2 +- interp/implicit_quantifiers.ml | 2 +- interp/implicit_quantifiers.mli | 2 +- interp/modintern.ml | 2 +- interp/modintern.mli | 2 +- interp/notation.ml | 2 +- interp/notation.mli | 2 +- interp/notation_ops.ml | 2 +- interp/notation_ops.mli | 2 +- interp/ppextend.ml | 2 +- interp/ppextend.mli | 2 +- interp/reserve.ml | 2 +- interp/reserve.mli | 2 +- interp/smartlocate.ml | 2 +- interp/smartlocate.mli | 2 +- interp/stdarg.ml | 2 +- interp/stdarg.mli | 2 +- interp/syntax_def.ml | 2 +- interp/syntax_def.mli | 2 +- interp/topconstr.ml | 2 +- interp/topconstr.mli | 2 +- 34 files changed, 34 insertions(+), 34 deletions(-) (limited to 'interp') diff --git a/interp/constrarg.ml b/interp/constrarg.ml index a7241399e0..d9c60a18bf 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* dump_definition (loc, id) sec ty | Names.Anonymous -> () -- cgit v1.2.3 From 34ef02fac1110673ae74c41c185c228ff7876de2 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Fri, 29 Jan 2016 10:13:12 +0100 Subject: CLEANUP: Context.{Rel,Named}.Declaration.t Originally, rel-context was represented as: Context.rel_context = Names.Name.t * Constr.t option * Constr.t Now it is represented as: Context.Rel.t = LocalAssum of Names.Name.t * Constr.t | LocalDef of Names.Name.t * Constr.t * Constr.t Originally, named-context was represented as: Context.named_context = Names.Id.t * Constr.t option * Constr.t Now it is represented as: Context.Named.t = LocalAssum of Names.Id.t * Constr.t | LocalDef of Names.Id.t * Constr.t * Constr.t Motivation: (1) In "tactics/hipattern.ml4" file we define "test_strict_disjunction" function which looked like this: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [_,None,c] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc Suppose that you do not know about rel-context and named-context. (that is the case of people who just started to read the source code) Merlin would tell you that the type of the value you are destructing by "match" is: 'a * 'b option * Constr.t (* worst-case scenario *) or Named.Name.t * Constr.t option * Constr.t (* best-case scenario (?) *) To me, this is akin to wearing an opaque veil. It is hard to figure out the meaning of the values you are looking at. In particular, it is hard to discover the connection between the value we are destructing above and the datatypes and functions defined in the "kernel/context.ml" file. In this case, the connection is there, but it is not visible (between the function above and the "Context" module). ------------------------------------------------------------------------ Now consider, what happens when the reader see the same function presented in the following form: let test_strict_disjunction n lc = Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc If the reader haven't seen "LocalAssum" before, (s)he can use Merlin to jump to the corresponding definition and learn more. In this case, the connection is there, and it is directly visible (between the function above and the "Context" module). (2) Also, if we already have the concepts such as: - local declaration - local assumption - local definition and we describe these notions meticulously in the Reference Manual, then it is a real pity not to reinforce the connection of the actual code with the abstract description we published. --- interp/constrextern.ml | 4 +++- interp/constrintern.ml | 9 +++++---- interp/implicit_quantifiers.ml | 19 ++++++++++--------- interp/implicit_quantifiers.mli | 4 ++-- 4 files changed, 20 insertions(+), 16 deletions(-) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 70a35c6132..3a8c506cba 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -29,6 +29,8 @@ open Notation open Detyping open Misctypes open Decl_kinds + +module NamedDecl = Context.Named.Declaration (*i*) (* Translation from glob_constr to front constr *) @@ -980,7 +982,7 @@ let rec glob_of_pat env sigma = function | PRef ref -> GRef (loc,ref,None) | PVar id -> GVar (loc,id) | PEvar (evk,l) -> - let test (id,_,_) = function PVar id' -> Id.equal id id' | _ -> false in + let test decl = function PVar id' -> Id.equal (NamedDecl.get_id decl) id' | _ -> false in let l = Evd.evar_instance_array test (Evd.find sigma evk) l in let id = Evd.evar_ident evk sigma in GEvar (loc,id,List.map (on_snd (glob_of_pat env sigma)) l) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 964ed05140..70802d5cba 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -29,6 +29,7 @@ open Nametab open Notation open Inductiveops open Decl_kinds +open Context.Rel.Declaration (** constr_expr -> glob_constr translation: - it adds holes for implicit arguments @@ -1645,14 +1646,14 @@ let internalize globalenv env allow_patvar lvar c = |loc,(Name y as x) -> (y,PatVar(loc,x)) :: l in match case_rel_ctxt,arg_pats with (* LetIn in the rel_context *) - |(_,Some _,_)::t, l when not with_letin -> + | LocalDef _ :: t, l when not with_letin -> canonize_args t l forbidden_names match_acc ((Loc.ghost,Anonymous)::var_acc) |[],[] -> (add_name match_acc na, var_acc) |_::t,PatVar (loc,x)::tt -> canonize_args t tt forbidden_names (add_name match_acc (loc,x)) ((loc,x)::var_acc) - |(cano_name,_,ty)::t,c::tt -> + | (LocalAssum (cano_name,ty) | LocalDef (cano_name,_,ty)) :: t, c::tt -> let fresh = Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names ty in canonize_args t tt (fresh::forbidden_names) @@ -1894,7 +1895,7 @@ let interp_rawcontext_evars env evdref k bl = let t' = locate_if_hole (loc_of_glob_constr t) na t in let t = understand_tcc_evars env evdref ~expected_type:IsType t' in - let d = (na,None,t) in + let d = LocalAssum (na,t) in let impls = if k == Implicit then let na = match na with Name n -> Some n | Anonymous -> None in @@ -1904,7 +1905,7 @@ let interp_rawcontext_evars env evdref k bl = (push_rel d env, d::params, succ n, impls) | Some b -> let c = understand_judgment_tcc env evdref b in - let d = (na, Some c.uj_val, c.uj_type) in + let d = LocalDef (na, c.uj_val, c.uj_type) in (push_rel d env, d::params, n, impls)) (env,[],k+1,[]) (List.rev bl) in (env, par), impls diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 391c600ed2..751b03a4a8 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -20,6 +20,7 @@ open Pp open Libobject open Nameops open Misctypes +open Context.Rel.Declaration (*i*) let generalizable_table = Summary.ref Id.Pred.empty ~name:"generalizable-ident" @@ -196,7 +197,7 @@ let combine_params avoid fn applied needed = List.partition (function (t, Some (loc, ExplByName id)) -> - let is_id (_, (na, _, _)) = match na with + let is_id (_, decl) = match get_name decl with | Name id' -> Id.equal id id' | Anonymous -> false in @@ -209,22 +210,22 @@ let combine_params avoid fn applied needed = (fun x -> match x with (t, Some (loc, ExplByName id)) -> id, t | _ -> assert false) named in - let is_unset (_, (_, b, _)) = match b with - | None -> true - | Some _ -> false + let is_unset (_, decl) = match decl with + | LocalAssum _ -> true + | LocalDef _ -> false in let needed = List.filter is_unset needed in let rec aux ids avoid app need = match app, need with [], [] -> List.rev ids, avoid - | app, (_, (Name id, _, _)) :: need when Id.List.mem_assoc id named -> + | app, (_, (LocalAssum (Name id, _) | LocalDef (Name id, _, _))) :: need when Id.List.mem_assoc id named -> aux (Id.List.assoc id named :: ids) avoid app need - | (x, None) :: app, (None, (Name id, _, _)) :: need -> + | (x, None) :: app, (None, (LocalAssum (Name id, _) | LocalDef (Name id, _, _))) :: need -> aux (x :: ids) avoid app need - | _, (Some cl, (_, _, _) as d) :: need -> + | _, (Some cl, _ as d) :: need -> let t', avoid' = fn avoid d in aux (t' :: ids) avoid' app need @@ -239,8 +240,8 @@ let combine_params avoid fn applied needed = in aux [] avoid applied needed let combine_params_freevar = - fun avoid (_, (na, _, _)) -> - let id' = next_name_away_from na avoid in + fun avoid (_, decl) -> + let id' = next_name_away_from (get_name decl) avoid in (CRef (Ident (Loc.ghost, id'),None), Id.Set.add id' avoid) let destClassApp cl = diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index b226bfa0af..d0327e5068 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -38,10 +38,10 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits val combine_params_freevar : - Id.Set.t -> (global_reference * bool) option * (Name.t * Term.constr option * Term.types) -> + Id.Set.t -> (global_reference * bool) option * Context.Rel.Declaration.t -> Constrexpr.constr_expr * Id.Set.t val implicit_application : Id.Set.t -> ?allow_partial:bool -> - (Id.Set.t -> (global_reference * bool) option * (Name.t * Term.constr option * Term.types) -> + (Id.Set.t -> (global_reference * bool) option * Context.Rel.Declaration.t -> Constrexpr.constr_expr * Id.Set.t) -> constr_expr -> constr_expr * Id.Set.t -- cgit v1.2.3 From f46a5686853353f8de733ae7fbd21a3a61977bc7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 3 Feb 2016 15:32:58 +0100 Subject: Do not give a name to anonymous evars anymore. See bug #4547. The current solution may not be totally ideal though. We generate names for anonymous evars on the fly at printing time, based on the Evar_kind data they are wearing. This means in particular that the printed name of an anonymous evar may change in the future because some unrelate evar has been solved or introduced. --- interp/constrextern.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 9df8f9c233..cc5d189e04 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -988,7 +988,10 @@ let rec glob_of_pat env sigma = function | PEvar (evk,l) -> let test (id,_,_) = function PVar id' -> Id.equal id id' | _ -> false in let l = Evd.evar_instance_array test (Evd.find sigma evk) l in - let id = Evd.evar_ident evk sigma in + let id = match Evd.evar_ident evk sigma with + | None -> Id.of_string "__" + | Some id -> id + in GEvar (loc,id,List.map (on_snd (glob_of_pat env sigma)) l) | PRel n -> let id = try match lookup_name_of_rel n env with -- cgit v1.2.3 From f358d7b4c962f5288ad9ce2dc35802666c882422 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 22 Feb 2016 10:32:57 +0100 Subject: The tactic generic argument now returns a value rather than a glob_expr. The glob_expr was actually always embedded as a VFun, so this patch should not change anything semantically. The only change occurs in the plugin API where one should use the Tacinterp.tactic_of_value function instead of Tacinterp.eval_tactic. Moreover, this patch allows to use tactics returning arguments from the ML side. --- interp/constrarg.ml | 2 +- interp/constrarg.mli | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'interp') diff --git a/interp/constrarg.ml b/interp/constrarg.ml index b093d92e73..a48d683754 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -25,7 +25,7 @@ let wit_int_or_var = let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type = Genarg.make0 None "intropattern" -let wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type = +let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type = Genarg.make0 None "tactic" let wit_ident = diff --git a/interp/constrarg.mli b/interp/constrarg.mli index e1a5f4d7c9..5c26af3c2a 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -69,6 +69,6 @@ val wit_red_expr : (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type -val wit_tactic : (raw_tactic_expr, glob_tactic_expr, glob_tactic_expr) genarg_type +val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type val wit_clause_dft_concl : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type -- cgit v1.2.3 From 4d25b224b91959b85fcd68c825a307ec684f0bac Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 28 Feb 2016 18:28:14 +0100 Subject: Printing notations: Cleaning in anticipation of fixing #4592. - Making a clear distinction between expressions of the notation which are associated to binding variables only (as in `Notation "'lam' x , P" := (fun x => P)" or `Notation "'exists2' x : t , p & q" := (ex2 (fun x:t => p) (fun x:t => q))') and those which are associated to at list one subterm (e.g. `Notation "x .+1" := (S x)' but also "Notation "{# x | P }" := (ex2 _ (fun y => x = F y) (fun x => P))' as in #4592). The former have type NtnTypeOnlyBinder. - Thus avoiding in particular encoding too early Anonymous as GHole and "Name id" as "GVar id". There is a non-trivial alpha-conversion work to do to get #4592 working. See comments in Notation_ops.add_env. --- interp/constrintern.ml | 10 +-- interp/constrintern.mli | 2 +- interp/notation.ml | 3 +- interp/notation_ops.ml | 183 ++++++++++++++++++++++++++++++++---------------- 4 files changed, 132 insertions(+), 66 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 70802d5cba..36f88fc3cc 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -275,7 +275,8 @@ let error_expect_binder_notation_type loc id = let set_var_scope loc id istermvar env ntnvars = try - let idscopes,typ = Id.Map.find id ntnvars in + let isonlybinding,idscopes,typ = Id.Map.find id ntnvars in + if istermvar then isonlybinding := false; let () = if istermvar then (* scopes have no effect on the interpretation of identifiers *) begin match !idscopes with @@ -629,7 +630,7 @@ let subst_aconstr_in_glob_constr loc intern (_,ntnvars as lvar) subst infos c = let split_by_type ids = List.fold_right (fun (x,(scl,typ)) (l1,l2,l3) -> match typ with - | NtnTypeConstr -> ((x,scl)::l1,l2,l3) + | NtnTypeConstr | NtnTypeOnlyBinder -> ((x,scl)::l1,l2,l3) | NtnTypeConstrList -> (l1,(x,scl)::l2,l3) | NtnTypeBinderList -> (l1,l2,(x,scl)::l3)) ids ([],[],[]) @@ -1845,7 +1846,7 @@ let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c = let interp_notation_constr ?(impls=empty_internalization_env) nenv a = let env = Global.env () in (* [vl] is intended to remember the scope of the free variables of [a] *) - let vl = Id.Map.map (fun typ -> (ref None, typ)) nenv.ninterp_var_type in + let vl = Id.Map.map (fun typ -> (ref true, ref None, typ)) nenv.ninterp_var_type in let c = internalize (Global.env()) {ids = extract_ids env; unb = false; tmp_scope = None; scopes = []; impls = impls} false (empty_ltac_sign, vl) a in @@ -1854,7 +1855,8 @@ let interp_notation_constr ?(impls=empty_internalization_env) nenv a = (* Splits variables into those that are binding, bound, or both *) (* binding and bound *) let out_scope = function None -> None,[] | Some (a,l) -> a,l in - let vars = Id.Map.map (fun (sc, typ) -> (out_scope !sc, typ)) vl in + let vars = Id.Map.map (fun (isonlybinding, sc, typ) -> + (!isonlybinding, out_scope !sc, typ)) vl in (* Returns [a] and the ordered list of variables with their scopes *) vars, a diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 73ecc437dd..eea76aa310 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -185,7 +185,7 @@ val global_reference_in_absolute_module : DirPath.t -> Id.t -> constr guaranteed to have the same domain as the input one. *) val interp_notation_constr : ?impls:internalization_env -> notation_interp_env -> constr_expr -> - (subscopes * notation_var_internalization_type) Id.Map.t * + (bool * subscopes * notation_var_internalization_type) Id.Map.t * notation_constr (** Globalization options *) diff --git a/interp/notation.ml b/interp/notation.ml index 5c10e0af71..04918bf7dd 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -529,9 +529,10 @@ let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2 let ntpe_eq t1 t2 = match t1, t2 with | NtnTypeConstr, NtnTypeConstr -> true +| NtnTypeOnlyBinder, NtnTypeOnlyBinder -> true | NtnTypeConstrList, NtnTypeConstrList -> true | NtnTypeBinderList, NtnTypeBinderList -> true -| (NtnTypeConstr | NtnTypeConstrList | NtnTypeBinderList), _ -> false +| (NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList), _ -> false let vars_eq (id1, (sc1, tp1)) (id2, (sc2, tp2)) = diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 51dfadac02..6561000c47 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -567,6 +567,18 @@ let abstract_return_type_context_notation_constr = abstract_return_type_context snd (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None),c)) +let is_term_meta id metas = + try match Id.List.assoc id metas with _,(NtnTypeConstr | NtnTypeConstrList) -> true | _ -> false + with Not_found -> false + +let is_onlybinding_meta id metas = + try match Id.List.assoc id metas with _,NtnTypeOnlyBinder -> true | _ -> false + with Not_found -> false + +let is_bindinglist_meta id metas = + try match Id.List.assoc id metas with _,NtnTypeBinderList -> true | _ -> false + with Not_found -> false + exception No_match let rec alpha_var id1 id2 = function @@ -575,26 +587,67 @@ let rec alpha_var id1 id2 = function | _::idl -> alpha_var id1 id2 idl | [] -> Id.equal id1 id2 -let add_env alp (sigma,sigmalist,sigmabinders) var v = +let add_env (alp,alpmetas) (terms,onlybinders,termlists,binderlists) var v = (* Check that no capture of binding variables occur *) + (* [alp] is used when matching a pattern "fun x => ... x ... ?var ... x ..." + with an actual term "fun z => ... z ..." when "x" is not bound in the + notation, as in "Notation "'twice_upto' y" := (fun x => x + x + y)". Then + we keep (z,x) in alp, and we have to check that what the [v] which is bound + to [var] does not contain z *) if List.exists (fun (id,_) ->occur_glob_constr id v) alp then raise No_match; + (* [alpmetas] is used when matching a pattern "fun x => ... x ... ?var ... x ..." + with an actual term "fun z => ... z ..." when "x" is bound in the + notation and the name "x" cannot be changed to "z", e.g. because + used at another occurrence, as in "Notation "'lam' y , P & Q" := + ((fun y => P),(fun y => Q))". Then, we keep (z,y) in alpmetas, and we + have to check that "fun z => ... z ..." denotes the same term as + "fun x => ... x ... ?var ... x" up to alpha-conversion when [var] + is instantiated by [v]; + Currently, we fail, but, eventually, [x] in [v] could be replaced by [x], + and, in match_, when finding "x" in subterm, failing because of a capture, + and, in match_, when finding "z" in subterm, replacing it with "x", + and, in an even further step, being even more robust, independent of the order, so + that e.g. the notation for ex2 works on "x y |- ex2 (fun x => y=x) (fun y => x=y)" + by giving, say, "exists2 x0, y=x0 & x=x0", but this would typically require the + glob_constr_eq in bind_term_env to be postponed in match_notation_constr, and the + choice of exact variable be done there; but again, this would be a non-trivial + refinement *) + if alpmetas != [] then raise No_match; + (* TODO: handle the case of multiple occs in different scopes *) + ((var,v)::terms,onlybinders,termlists,binderlists) + +let add_binding_env alp (terms,onlybinders,termlists,binderlists) var v = (* TODO: handle the case of multiple occs in different scopes *) - ((var,v)::sigma,sigmalist,sigmabinders) + (terms,(var,v)::onlybinders,termlists,binderlists) -let bind_env alp (sigma,sigmalist,sigmabinders as fullsigma) var v = +let add_bindinglist_env (terms,onlybinders,termlists,binderlists) x bl = + (terms,onlybinders,termlists,(x,List.rev bl)::binderlists) + +let bind_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var v = try - let v' = Id.List.assoc var sigma in + let v' = Id.List.assoc var terms in match v, v' with - | GHole _, _ -> fullsigma + | GHole _, _ -> sigma | _, GHole _ -> - add_env alp (Id.List.remove_assoc var sigma,sigmalist,sigmabinders) var v + let sigma = Id.List.remove_assoc var terms,onlybinders,termlists,binderlists in + add_env alp sigma var v | _, _ -> - if glob_constr_eq v v' then fullsigma + if glob_constr_eq v v' then sigma else raise No_match - with Not_found -> add_env alp fullsigma var v + with Not_found -> add_env alp sigma var v -let bind_binder (sigma,sigmalist,sigmabinders) x bl = - (sigma,sigmalist,(x,List.rev bl)::sigmabinders) +let bind_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var v = + try + let v' = Id.List.assoc var onlybinders in + match v, v' with + | Anonymous, _ -> alp, sigma + | _, Anonymous -> + let sigma = (terms,Id.List.remove_assoc var onlybinders,termlists,binderlists) in + alp, add_binding_env alp sigma var v + | Name id1, Name id2 -> + if Id.equal id1 id2 then alp,sigma + else (fst alp,(id1,id2)::snd alp),sigma + with Not_found -> alp, add_binding_env alp sigma var v let match_fix_kind fk1 fk2 = match (fk1,fk2) with @@ -615,12 +668,16 @@ let match_opt f sigma t1 t2 = match (t1,t2) with | _ -> raise No_match let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with - | (_,Name id2) when Id.List.mem id2 (fst metas) -> - let rhs = match na1 with - | Name id1 -> GVar (Loc.ghost,id1) - | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in - alp, bind_env alp sigma id2 rhs - | (Name id1,Name id2) -> (id1,id2)::alp,sigma + | (na1,Name id2) when is_onlybinding_meta id2 metas -> + bind_binding_env alp sigma id2 na1 + | (Name id1,Name id2) when is_term_meta id2 metas -> + (* We let the non-binding occurrence define the rhs and hence reason up to *) + (* alpha-conversion for the given occurrence of the name (see #)) *) + (fst alp,(id1,id2)::snd alp), sigma + | (Anonymous,Name id2) when is_term_meta id2 metas -> + (* We let the non-binding occurrence define the rhs *) + alp, sigma + | (Name id1,Name id2) -> ((id1,id2)::fst alp, snd alp),sigma | (Anonymous,Anonymous) -> alp,sigma | _ -> raise No_match @@ -645,36 +702,38 @@ let rec match_iterated_binders islambda decls = function ((na,Explicit (*?*), Some c,GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None))::decls) b | b -> (decls,b) -let remove_sigma x (sigmavar,sigmalist,sigmabinders) = - (Id.List.remove_assoc x sigmavar,sigmalist,sigmabinders) +let remove_sigma x (terms,onlybinders,termlists,binderlists) = + (Id.List.remove_assoc x terms,onlybinders,termlists,binderlists) + +let add_ldots_var metas = (ldots_var,((None,[]),NtnTypeConstr))::metas let match_abinderlist_with_app match_fun metas sigma rest x iter termin = let rec aux sigma acc rest = try - let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in - let rest = Id.List.assoc ldots_var (pi1 sigma) in + let (terms,_,_,binderlists as sigma) = match_fun (add_ldots_var metas) sigma rest iter in + let rest = Id.List.assoc ldots_var terms in let b = - match Id.List.assoc x (pi3 sigma) with [b] -> b | _ ->assert false + match Id.List.assoc x binderlists with [b] -> b | _ ->assert false in let sigma = remove_sigma x (remove_sigma ldots_var sigma) in aux sigma (b::acc) rest with No_match when not (List.is_empty acc) -> acc, match_fun metas sigma rest termin in let bl,sigma = aux sigma [] rest in - bind_binder sigma x bl + add_bindinglist_env sigma x bl let match_alist match_fun metas sigma rest x iter termin lassoc = let rec aux sigma acc rest = try - let sigma = match_fun (ldots_var::fst metas,snd metas) sigma rest iter in - let rest = Id.List.assoc ldots_var (pi1 sigma) in - let t = Id.List.assoc x (pi1 sigma) in + let (terms,_,_,_ as sigma) = match_fun (add_ldots_var metas) sigma rest iter in + let rest = Id.List.assoc ldots_var terms in + let t = Id.List.assoc x terms in let sigma = remove_sigma x (remove_sigma ldots_var sigma) in aux sigma (t::acc) rest with No_match when not (List.is_empty acc) -> acc, match_fun metas sigma rest termin in - let l,sigma = aux sigma [] rest in - (pi1 sigma, (x,if lassoc then l else List.rev l)::pi2 sigma, pi3 sigma) + let l,(terms,onlybinders,termlists,binderlists as sigma) = aux sigma [] rest in + (terms,onlybinders,(x,if lassoc then l else List.rev l)::termlists, binderlists) let does_not_come_from_already_eta_expanded_var = (* This is hack to avoid looping on a rule with rhs of the form *) @@ -688,11 +747,11 @@ let does_not_come_from_already_eta_expanded_var = (* checked). *) function GVar _ -> false | _ -> true -let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = +let rec match_ inner u alp metas sigma a1 a2 = match (a1,a2) with (* Matching notation variable *) - | r1, NVar id2 when Id.List.mem id2 tmetas -> bind_env alp sigma id2 r1 + | r1, NVar id2 when is_term_meta id2 metas -> bind_term_env alp sigma id2 r1 (* Matching recursive notations for terms *) | r1, NList (x,_,iter,termin,lassoc) -> @@ -702,25 +761,26 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = | GLambda (_,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name id2,_,b2),termin)-> let (decls,b) = match_iterated_binders true [(na1,bk,None,t1)] b1 in (* TODO: address the possibility that termin is a Lambda itself *) - match_in u alp metas (bind_binder sigma x decls) b termin + match_in u alp metas (add_bindinglist_env sigma x decls) b termin | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (Name id2,_,b2),termin) when na1 != Anonymous -> let (decls,b) = match_iterated_binders false [(na1,bk,None,t1)] b1 in (* TODO: address the possibility that termin is a Prod itself *) - match_in u alp metas (bind_binder sigma x decls) b termin + match_in u alp metas (add_bindinglist_env sigma x decls) b termin (* Matching recursive notations for binders: general case *) | r, NBinderList (x,_,iter,termin) -> match_abinderlist_with_app (match_hd u alp) metas sigma r x iter termin (* Matching individual binders as part of a recursive pattern *) - | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2) when Id.List.mem id blmetas -> - match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2 + | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2) + when is_bindinglist_meta id metas -> + match_in u alp metas (add_bindinglist_env sigma id [(na,bk,None,t)]) b1 b2 | GProd (_,na,bk,t,b1), NProd (Name id,_,b2) - when Id.List.mem id blmetas && na != Anonymous -> - match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2 + when is_bindinglist_meta id metas && na != Anonymous -> + match_in u alp metas (add_bindinglist_env sigma id [(na,bk,None,t)]) b1 b2 (* Matching compositionally *) - | GVar (_,id1), NVar id2 when alpha_var id1 id2 alp -> sigma + | GVar (_,id1), NVar id2 when alpha_var id1 id2 (fst alp) -> sigma | GRef (_,r1,_), NRef r2 when (eq_gr r1 r2) -> sigma | GPatVar (_,(_,n1)), NPatVar n2 when Id.equal n1 n2 -> sigma | GApp (loc,f1,l1), NApp (f2,l2) -> @@ -799,9 +859,9 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 = let t1 = GHole(Loc.ghost,Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in let sigma = match t2 with | NHole _ -> sigma - | NVar id2 -> bind_env alp sigma id2 t1 + | NVar id2 -> bind_term_env alp sigma id2 t1 | _ -> assert false in - match_in u alp metas (bind_binder sigma id [(Name id',Explicit,None,t1)]) + match_in u alp metas (add_bindinglist_env sigma id [(Name id',Explicit,None,t1)]) (mkGApp Loc.ghost b1 (GVar (Loc.ghost,id'))) b2 | (GRec _ | GEvar _), _ @@ -823,14 +883,16 @@ and match_equations u alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) = (alp,sigma) patl1 patl2 in match_in u alp metas sigma rhs1 rhs2 +let term_of_binder = function + | Name id -> GVar (Loc.ghost,id) + | Anonymous -> GHole (Loc.ghost,Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) + let match_notation_constr u c (metas,pat) = - let test (_, (_, x)) = match x with NtnTypeBinderList -> false | _ -> true in - let vars = List.partition test metas in - let vars = (List.map fst (fst vars), List.map fst (snd vars)) in - let terms,termlists,binders = match_ false u [] vars ([],[],[]) c pat in + let terms,binders,termlists,binderlists = + match_ false u ([],[]) metas ([],[],[],[]) c pat in (* Reorder canonically the substitution *) - let find x = - try Id.List.assoc x terms + let find_binder x = + try term_of_binder (Id.List.assoc x binders) with Not_found -> (* Happens for binders bound to Anonymous *) (* Find a better way to propagate Anonymous... *) @@ -838,11 +900,13 @@ let match_notation_constr u c (metas,pat) = List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') -> match typ with | NtnTypeConstr -> - ((find x, scl)::terms',termlists',binders') + ((Id.List.assoc x terms, scl)::terms',termlists',binders') + | NtnTypeOnlyBinder -> + ((find_binder x, scl)::terms',termlists',binders') | NtnTypeConstrList -> (terms',(Id.List.assoc x termlists,scl)::termlists',binders') | NtnTypeBinderList -> - (terms',termlists',(Id.List.assoc x binders,scl)::binders')) + (terms',termlists',(Id.List.assoc x binderlists,scl)::binders')) metas ([],[],[]) (* Matching cases pattern *) @@ -851,17 +915,17 @@ let add_patterns_for_params ind l = let nparams = mib.Declarations.mind_nparams in Util.List.addn nparams (PatVar (Loc.ghost,Anonymous)) l -let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v = +let bind_env_cases_pattern (terms,x,termlists,y as sigma) var v = try - let vvar = Id.List.assoc var sigma in - if cases_pattern_eq v vvar then fullsigma else raise No_match + let vvar = Id.List.assoc var terms in + if cases_pattern_eq v vvar then sigma else raise No_match with Not_found -> (* TODO: handle the case of multiple occs in different scopes *) - (var,v)::sigma,sigmalist,x + (var,v)::terms,x,termlists,y -let rec match_cases_pattern metas sigma a1 a2 = +let rec match_cases_pattern metas (terms,x,termlists,y as sigma) a1 a2 = match (a1,a2) with - | r1, NVar id2 when Id.List.mem id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[]) + | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 r1),(0,[]) | PatVar (_,Anonymous), NHole _ -> sigma,(0,[]) | PatCstr (loc,(ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 -> sigma,(0,add_patterns_for_params (fst r1) largs) @@ -876,14 +940,14 @@ let rec match_cases_pattern metas sigma a1 a2 = let l1',more_args = Util.List.chop le2 l1 in (List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),(le2,more_args) | r1, NList (x,_,iter,termin,lassoc) -> - (match_alist (fun (metas,_) -> match_cases_pattern_no_more_args metas) - (metas,[]) (pi1 sigma,pi2 sigma,()) r1 x iter termin lassoc),(0,[]) + (match_alist (match_cases_pattern_no_more_args) + metas (terms,(),termlists,()) r1 x iter termin lassoc),(0,[]) | _ -> raise No_match and match_cases_pattern_no_more_args metas sigma a1 a2 = match match_cases_pattern metas sigma a1 a2 with - |out,(_,[]) -> out - |_ -> raise No_match + | out,(_,[]) -> out + | _ -> raise No_match let match_ind_pattern metas sigma ind pats a2 = match a2 with @@ -904,16 +968,15 @@ let reorder_canonically_substitution terms termlists metas = List.fold_right (fun (x,(scl,typ)) (terms',termlists') -> match typ with | NtnTypeConstr -> ((Id.List.assoc x terms, scl)::terms',termlists') + | NtnTypeOnlyBinder -> assert false | NtnTypeConstrList -> (terms',(Id.List.assoc x termlists,scl)::termlists') | NtnTypeBinderList -> assert false) metas ([],[]) let match_notation_constr_cases_pattern c (metas,pat) = - let vars = List.map fst metas in - let (terms,termlists,()),more_args = match_cases_pattern vars ([],[],()) c pat in + let (terms,(),termlists,()),more_args = match_cases_pattern metas ([],(),[],()) c pat in reorder_canonically_substitution terms termlists metas, more_args let match_notation_constr_ind_pattern ind args (metas,pat) = - let vars = List.map fst metas in - let (terms,termlists,()),more_args = match_ind_pattern vars ([],[],()) ind args pat in + let (terms,(),termlists,()),more_args = match_ind_pattern metas ([],(),[],()) ind args pat in reorder_canonically_substitution terms termlists metas, more_args -- cgit v1.2.3 From 508d5a99101097948b6de342295eec0d5c8cbe72 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 3 Mar 2016 18:59:51 +0100 Subject: Fixing bug #4105: poor escaping in the protocol between CoqIDE and coqtop. Printing invalid UTF-8 string startled GTK too much, leading to CoqIDE dying improperly. We now check that all strings outputed by Coq are proper UTF-8. This is not perfect, as CoqIDE will sometimes truncate strings which contains the null character, but at least it should not crash. --- interp/notation.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'interp') diff --git a/interp/notation.ml b/interp/notation.ml index 5c10e0af71..c4addbf10f 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -314,7 +314,9 @@ let declare_prim_token_interpreter sc interp (patl,uninterp,b) = patl let mkNumeral n = Numeral n -let mkString s = String s +let mkString = function +| None -> None +| Some s -> if Unicode.is_utf8 s then Some (String s) else None let delay dir int loc x = (dir, (fun () -> int loc x)) @@ -326,7 +328,7 @@ let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) = let declare_string_interpreter sc dir interp (patl,uninterp,inpat) = declare_prim_token_interpreter sc (fun cont loc -> function String s -> delay dir interp loc s | p -> cont loc p) - (patl, (fun r -> Option.map mkString (uninterp r)), inpat) + (patl, (fun r -> mkString (uninterp r)), inpat) let check_required_module loc sc (sp,d) = try let _ = Nametab.global_of_path sp in () -- cgit v1.2.3 From 7478ad7cc600753ba2609254657c87cacc27e8fc Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 12 Mar 2016 08:03:05 +0100 Subject: A more explicit name to the asymmetric boolean flag. --- interp/constrextern.ml | 6 +++--- interp/constrintern.ml | 4 ++-- interp/topconstr.ml | 6 +++--- interp/topconstr.mli | 2 +- 4 files changed, 9 insertions(+), 9 deletions(-) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 3675441353..2da8e0f6f2 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -327,7 +327,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = with Not_found | No_match | Exit -> let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in - if !Topconstr.oldfashion_patterns then + if !Topconstr.asymmetric_patterns then if pattern_printable_in_both_syntax cstrsp then CPatCstr (loc, c, [], args) else CPatCstr (loc, c, add_patt_for_params (fst cstrsp) args, []) @@ -358,7 +358,7 @@ and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args)) List.map (extern_cases_pattern_in_scope subscope vars) c) substlist in let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in - let l2' = if !Topconstr.oldfashion_patterns || not (List.is_empty ll) then l2 + let l2' = if !Topconstr.asymmetric_patterns || not (List.is_empty ll) then l2 else match drop_implicits_in_patt gr nb_to_drop l2 with |Some true_args -> true_args @@ -374,7 +374,7 @@ and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args)) extern_cases_pattern_in_scope (scopt,scl@scopes) vars c) subst in let l2 = List.map (extern_cases_pattern_in_scope allscopes vars) more_args in - let l2' = if !Topconstr.oldfashion_patterns then l2 + let l2' = if !Topconstr.asymmetric_patterns then l2 else match drop_implicits_in_patt gr (nb_to_drop + List.length l1) l2 with |Some true_args -> true_args diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 36f88fc3cc..f46217dec6 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1133,7 +1133,7 @@ let drop_notations_pattern looked_for = | None -> RCPatAtom (loc, None) | Some (n, head, pl) -> let pl = - if !oldfashion_patterns then pl else + if !asymmetric_patterns then pl else let pars = List.make n (CPatAtom (loc, None)) in List.rev_append pars pl in match drop_syndef top env head pl with @@ -1238,7 +1238,7 @@ let rec intern_pat genv aliases pat = let aliases' = merge_aliases aliases id in intern_pat genv aliases' p | RCPatCstr (loc, head, expl_pl, pl) -> - if !oldfashion_patterns then + if !asymmetric_patterns then let len = if List.is_empty expl_pl then Some (List.length pl) else None in let c,idslpl1 = find_constructor loc len head in let with_letin = diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 8293f7f88d..cde72fd93d 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -19,14 +19,14 @@ open Constrexpr_ops (*i*) -let oldfashion_patterns = ref (false) +let asymmetric_patterns = ref (false) let _ = Goptions.declare_bool_option { Goptions.optsync = true; Goptions.optdepr = false; Goptions.optname = "Constructors in patterns require all their arguments but no parameters instead of explicit parameters and arguments"; Goptions.optkey = ["Asymmetric";"Patterns"]; - Goptions.optread = (fun () -> !oldfashion_patterns); - Goptions.optwrite = (fun a -> oldfashion_patterns:=a); + Goptions.optread = (fun () -> !asymmetric_patterns); + Goptions.optwrite = (fun a -> asymmetric_patterns:=a); } (**********************************************************************) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 1e867c19c6..0f30135f89 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -12,7 +12,7 @@ open Constrexpr (** Topconstr *) -val oldfashion_patterns : bool ref +val asymmetric_patterns : bool ref (** Utilities on constr_expr *) -- cgit v1.2.3 From d868820ad1f00b896c5f44f18678fac2f8e0f720 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 13 Mar 2016 13:18:10 +0100 Subject: Supporting "(@foo) args" in patterns, where "@foo" has no arguments. --- interp/constrexpr_ops.ml | 2 +- interp/constrextern.ml | 18 +++++++++--------- interp/constrintern.ml | 13 ++++++------- interp/topconstr.ml | 2 +- 4 files changed, 17 insertions(+), 18 deletions(-) (limited to 'interp') diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 9c577034e8..c5730e6261 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -66,7 +66,7 @@ let rec cases_pattern_expr_eq p1 p2 = Id.equal i1 i2 && cases_pattern_expr_eq a1 a2 | CPatCstr(_,c1,a1,b1), CPatCstr(_,c2,a2,b2) -> eq_reference c1 c2 && - List.equal cases_pattern_expr_eq a1 a2 && + Option.equal (List.equal cases_pattern_expr_eq) a1 a2 && List.equal cases_pattern_expr_eq b1 b2 | CPatAtom(_,r1), CPatAtom(_,r2) -> Option.equal eq_reference r1 r2 diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 2da8e0f6f2..49892bec49 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -266,7 +266,7 @@ let make_pat_notation loc ntn (terms,termlists as subst) args = let mkPat loc qid l = (* Normally irrelevant test with v8 syntax, but let's do it anyway *) - if List.is_empty l then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,[],l) + if List.is_empty l then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,None,l) let pattern_printable_in_both_syntax (ind,_ as c) = let impl_st = extract_impargs_data (implicits_of_global (ConstructRef c)) in @@ -286,7 +286,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = when !Flags.in_debugger||Inductiveops.constructor_has_local_defs cstrsp -> let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in - CPatCstr (loc, c, add_patt_for_params (fst cstrsp) args, []) + CPatCstr (loc, c, Some (add_patt_for_params (fst cstrsp) args), []) | _ -> try if !Flags.raw_print || !print_no_symbol then raise No_match; @@ -329,13 +329,13 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in if !Topconstr.asymmetric_patterns then if pattern_printable_in_both_syntax cstrsp - then CPatCstr (loc, c, [], args) - else CPatCstr (loc, c, add_patt_for_params (fst cstrsp) args, []) + then CPatCstr (loc, c, None, args) + else CPatCstr (loc, c, Some (add_patt_for_params (fst cstrsp) args), []) else let full_args = add_patt_for_params (fst cstrsp) args in match drop_implicits_in_patt (ConstructRef cstrsp) 0 full_args with - |Some true_args -> CPatCstr (loc, c, [], true_args) - |None -> CPatCstr (loc, c, full_args, []) + |Some true_args -> CPatCstr (loc, c, None, true_args) + |None -> CPatCstr (loc, c, Some full_args, []) in insert_pat_alias loc p na and apply_notation_to_pattern loc gr ((subst,substlist),(nb_to_drop,more_args)) (tmp_scope, scopes as allscopes) vars = @@ -413,7 +413,7 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then let c = extern_reference Loc.ghost vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in - CPatCstr (Loc.ghost, c, add_patt_for_params ind args, []) + CPatCstr (Loc.ghost, c, Some (add_patt_for_params ind args), []) else try if !Flags.raw_print || !print_no_symbol then raise No_match; @@ -431,8 +431,8 @@ let extern_ind_pattern_in_scope (scopes:local_scopes) vars ind args = let c = extern_reference Loc.ghost vars (IndRef ind) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in match drop_implicits_in_patt (IndRef ind) 0 args with - |Some true_args -> CPatCstr (Loc.ghost, c, [], true_args) - |None -> CPatCstr (Loc.ghost, c, args, []) + |Some true_args -> CPatCstr (Loc.ghost, c, None, true_args) + |None -> CPatCstr (Loc.ghost, c, Some args, []) let extern_cases_pattern vars p = extern_cases_pattern_in_scope (None,[]) vars p diff --git a/interp/constrintern.ml b/interp/constrintern.ml index f46217dec6..b62df8dfff 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1095,7 +1095,7 @@ let drop_notations_pattern looked_for = let (loc,qid) = qualid_of_reference re in try match locate_extended qid with - |SynDef sp -> + | SynDef sp -> let (vars,a) = Syntax_def.search_syntactic_definition sp in (match a with | NRef g -> @@ -1118,7 +1118,7 @@ let drop_notations_pattern looked_for = let (_,argscs) = find_remaining_scopes pats1 pats2 g in Some (g, idspl1, List.map2 (in_pat_sc env) argscs pats2) | _ -> raise Not_found) - |TrueGlobal g -> + | TrueGlobal g -> test_kind top g; Dumpglob.add_glob loc g; let (_,argscs) = find_remaining_scopes [] pats g in @@ -1140,16 +1140,15 @@ let drop_notations_pattern looked_for = |Some (a,b,c) -> RCPatCstr(loc, a, b, c) |None -> raise (InternalizationError (loc,NotAConstructor head)) end - | CPatCstr (loc, head, [], pl) -> + | CPatCstr (loc, head, None, pl) -> begin match drop_syndef top env head pl with | Some (a,b,c) -> RCPatCstr(loc, a, b, c) | None -> raise (InternalizationError (loc,NotAConstructor head)) end - | CPatCstr (loc, r, expl_pl, pl) -> - let g = try - (locate (snd (qualid_of_reference r))) - with Not_found -> + | CPatCstr (loc, r, Some expl_pl, pl) -> + let g = try locate (snd (qualid_of_reference r)) + with Not_found -> raise (InternalizationError (loc,NotAConstructor r)) in let (argscs1,argscs2) = find_remaining_scopes expl_pl pl g in RCPatCstr (loc, g, List.map2 (in_pat_sc env) argscs1 expl_pl, List.map2 (in_pat_sc env) argscs2 pl) diff --git a/interp/topconstr.ml b/interp/topconstr.ml index cde72fd93d..e569f543b5 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -52,7 +52,7 @@ let rec cases_pattern_fold_names f a = function List.fold_left (cases_pattern_fold_names f) a patl | CPatCstr (_,_,patl1,patl2) -> List.fold_left (cases_pattern_fold_names f) - (List.fold_left (cases_pattern_fold_names f) a patl1) patl2 + (Option.fold_left (List.fold_left (cases_pattern_fold_names f)) a patl1) patl2 | CPatNotation (_,_,(patl,patll),patl') -> List.fold_left (cases_pattern_fold_names f) (List.fold_left (cases_pattern_fold_names f) a (patl@List.flatten patll)) patl' -- cgit v1.2.3 From 3366f05ab09aa90dcc96d7432bff09617162c3e4 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 13 Mar 2016 17:49:25 +0100 Subject: Adopting the same rules for interpreting @, abbreviations and notations in patterns than in terms, wrt implicit arguments and scopes. See file Notations2.v for the conventions in use in terms. Somehow this could be put in 8.5 since it puts in agreement the interpretation of abbreviations and notations in "symmetric patterns" to what is done in terms (even though the interpretation rules for terms are a bit ad hoc). There is one exception: in terms, "(foo args) args'" deactivates the implicit arguments and scopes in args'. This is a bit complicated to implement in patterns so the syntax is not supported (and anyway, this convention is a bit questionable). --- interp/constrintern.ml | 33 ++++++++++++++++++++------------- 1 file changed, 20 insertions(+), 13 deletions(-) (limited to 'interp') diff --git a/interp/constrintern.ml b/interp/constrintern.ml index b62df8dfff..fa38695705 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -918,7 +918,7 @@ let chop_params_pattern loc ind args with_letin = args let find_constructor loc add_params ref = - let cstr = match ref with + let (ind,_ as cstr) = match ref with | ConstructRef cstr -> cstr | IndRef _ -> let error = str "There is an inductive name deep in a \"in\" clause." in @@ -927,15 +927,15 @@ let find_constructor loc add_params ref = let error = str "This reference is not a constructor." in user_err_loc (loc, "find_constructor", error) in - cstr, (function (ind,_ as c) -> match add_params with - |Some nb_args -> + cstr, match add_params with + | Some nb_args -> let nb = - if Int.equal nb_args (Inductiveops.constructor_nrealdecls c) + if Int.equal nb_args (Inductiveops.constructor_nrealdecls cstr) then Inductiveops.inductive_nparamdecls ind else Inductiveops.inductive_nparams ind in List.make nb ([], [(Id.Map.empty, PatVar(Loc.ghost,Anonymous))]) - |None -> []) cstr + | None -> [] let find_pattern_variable = function | Ident (loc,id) -> id @@ -1099,16 +1099,17 @@ let drop_notations_pattern looked_for = let (vars,a) = Syntax_def.search_syntactic_definition sp in (match a with | NRef g -> + (* Convention: do not deactivate implicit arguments and scopes for further arguments *) test_kind top g; let () = assert (List.is_empty vars) in let (_,argscs) = find_remaining_scopes [] pats g in Some (g, [], List.map2 (in_pat_sc env) argscs pats) - | NApp (NRef g,[]) -> (* special case : Syndef for @Cstr *) + | NApp (NRef g,[]) -> (* special case: Syndef for @Cstr, this deactivates *) test_kind top g; let () = assert (List.is_empty vars) in - let (argscs,_) = find_remaining_scopes pats [] g in - Some (g, List.map2 (in_pat_sc env) argscs pats, []) + Some (g, List.map (in_pat false env) pats, []) | NApp (NRef g,args) -> + (* Convention: do not deactivate implicit arguments and scopes for further arguments *) test_kind top g; let nvars = List.length vars in if List.length pats < nvars then error_not_enough_arguments loc; @@ -1146,12 +1147,18 @@ let drop_notations_pattern looked_for = | Some (a,b,c) -> RCPatCstr(loc, a, b, c) | None -> raise (InternalizationError (loc,NotAConstructor head)) end - | CPatCstr (loc, r, Some expl_pl, pl) -> + | CPatCstr (loc, r, Some expl_pl, pl) -> let g = try locate (snd (qualid_of_reference r)) with Not_found -> raise (InternalizationError (loc,NotAConstructor r)) in - let (argscs1,argscs2) = find_remaining_scopes expl_pl pl g in - RCPatCstr (loc, g, List.map2 (in_pat_sc env) argscs1 expl_pl, List.map2 (in_pat_sc env) argscs2 pl) + if expl_pl == [] then + (* Convention: (@r) deactivates all further implicit arguments and scopes *) + RCPatCstr (loc, g, List.map (in_pat false env) pl, []) + else + (* Convention: (@r expl_pl) deactivates implicit arguments in expl_pl and in pl *) + (* but not scopes in expl_pl *) + let (argscs1,_) = find_remaining_scopes expl_pl pl g in + RCPatCstr (loc, g, List.map2 (in_pat_sc env) argscs1 expl_pl @ List.map (in_pat false env) pl, []) | CPatNotation (loc,"- _",([CPatPrim(_,Numeral p)],[]),[]) when Bigint.is_strictly_pos p -> fst (Notation.interp_prim_token_cases_pattern_expr loc (ensure_kind false loc) (Numeral (Bigint.neg p)) @@ -1203,8 +1210,8 @@ let drop_notations_pattern looked_for = ensure_kind top loc g; let (argscs1,argscs2) = find_remaining_scopes pl args g in RCPatCstr (loc, g, - List.map2 (fun x -> in_not false loc {env with tmp_scope = x} fullsubst []) argscs1 pl, - List.map2 (in_pat_sc env) argscs2 args) + List.map2 (fun x -> in_not false loc {env with tmp_scope = x} fullsubst []) argscs1 pl @ + List.map (in_pat false env) args, []) | NList (x,_,iter,terminator,lassoc) -> if not (List.is_empty args) then user_err_loc (loc,"",strbrk "Application of arguments to a recursive notation not supported in patterns."); -- cgit v1.2.3 From 2537e84ba9fa92db6cfd3d7f5e400b1716c31246 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 17 Mar 2016 14:42:51 +0100 Subject: Removing the registering of default values for generic arguments. --- interp/constrarg.ml | 34 +++++++++++++++++----------------- interp/stdarg.ml | 10 +++++----- 2 files changed, 22 insertions(+), 22 deletions(-) (limited to 'interp') diff --git a/interp/constrarg.ml b/interp/constrarg.ml index a48d683754..ead4e39692 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -20,48 +20,48 @@ let loc_of_or_by_notation f = function | ByNotation (loc,s,_) -> loc let wit_int_or_var = - Genarg.make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) None "int_or_var" + Genarg.make0 ~dyn:(val_tag (topwit Stdarg.wit_int)) "int_or_var" let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type = - Genarg.make0 None "intropattern" + Genarg.make0 "intropattern" let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type = - Genarg.make0 None "tactic" + Genarg.make0 "tactic" let wit_ident = - Genarg.make0 None "ident" + Genarg.make0 "ident" let wit_var = - Genarg.make0 ~dyn:(val_tag (topwit wit_ident)) None "var" + Genarg.make0 ~dyn:(val_tag (topwit wit_ident)) "var" -let wit_ref = Genarg.make0 None "ref" +let wit_ref = Genarg.make0 "ref" -let wit_quant_hyp = Genarg.make0 None "quant_hyp" +let wit_quant_hyp = Genarg.make0 "quant_hyp" let wit_sort : (glob_sort, glob_sort, sorts) genarg_type = - Genarg.make0 None "sort" + Genarg.make0 "sort" let wit_constr = - Genarg.make0 None "constr" + Genarg.make0 "constr" let wit_constr_may_eval = - Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) None "constr_may_eval" + Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) "constr_may_eval" -let wit_uconstr = Genarg.make0 None "uconstr" +let wit_uconstr = Genarg.make0 "uconstr" -let wit_open_constr = Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) None "open_constr" +let wit_open_constr = Genarg.make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr" -let wit_constr_with_bindings = Genarg.make0 None "constr_with_bindings" +let wit_constr_with_bindings = Genarg.make0 "constr_with_bindings" -let wit_bindings = Genarg.make0 None "bindings" +let wit_bindings = Genarg.make0 "bindings" let wit_hyp_location_flag : 'a Genarg.uniform_genarg_type = - Genarg.make0 None "hyp_location_flag" + Genarg.make0 "hyp_location_flag" -let wit_red_expr = Genarg.make0 None "redexpr" +let wit_red_expr = Genarg.make0 "redexpr" let wit_clause_dft_concl = - Genarg.make0 None "clause_dft_concl" + Genarg.make0 "clause_dft_concl" (** Register location *) diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 9c3ed94130..56b995e537 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -9,19 +9,19 @@ open Genarg let wit_unit : unit uniform_genarg_type = - make0 None "unit" + make0 "unit" let wit_bool : bool uniform_genarg_type = - make0 None "bool" + make0 "bool" let wit_int : int uniform_genarg_type = - make0 None "int" + make0 "int" let wit_string : string uniform_genarg_type = - make0 None "string" + make0 "string" let wit_pre_ident : string uniform_genarg_type = - make0 None "preident" + make0 "preident" let () = register_name0 wit_unit "Stdarg.wit_unit" let () = register_name0 wit_bool "Stdarg.wit_bool" -- cgit v1.2.3 From 4b2cdf733df6dc23247b078679e71da98e54f5cc Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 17 Mar 2016 16:57:05 +0100 Subject: Removing the special status of generic entries defined by Coq itself. The ARGUMENT EXTEND macro was discriminating between parsing entries known statically, i.e. defined in Pcoq and unknown entires. Although simplifying a bit the life of the plugin writer, it made actual interpretation difficult to predict and complicated the code of the ARGUMENT EXTEND macro. After this patch, all parsing entries and generic arguments used in an ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding a few more "open Pcoq.X" and "open Constrarg" here and there. --- interp/constrarg.ml | 10 ++++++++++ interp/constrarg.mli | 12 ++++++++++++ interp/stdarg.ml | 5 +++++ interp/stdarg.mli | 5 +++++ 4 files changed, 32 insertions(+) (limited to 'interp') diff --git a/interp/constrarg.ml b/interp/constrarg.ml index ead4e39692..20ee7aa4fb 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -82,3 +82,13 @@ let () = register_name0 wit_quant_hyp "Constrarg.wit_quant_hyp"; register_name0 wit_bindings "Constrarg.wit_bindings"; register_name0 wit_constr_with_bindings "Constrarg.wit_constr_with_bindings"; + () + +(** Aliases *) + +let wit_reference = wit_ref +let wit_global = wit_ref +let wit_clause = wit_clause_dft_concl +let wit_quantified_hypothesis = wit_quant_hyp +let wit_intropattern = wit_intro_pattern +let wit_redexpr = wit_red_expr diff --git a/interp/constrarg.mli b/interp/constrarg.mli index 5c26af3c2a..1197b85a25 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -72,3 +72,15 @@ val wit_red_expr : val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type val wit_clause_dft_concl : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type + +(** Aliases for compatibility *) + +val wit_reference : (reference, global_reference located or_var, global_reference) genarg_type +val wit_global : (reference, global_reference located or_var, global_reference) genarg_type +val wit_clause : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type +val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type +val wit_intropattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type +val wit_redexpr : + ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, + (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, + (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type diff --git a/interp/stdarg.ml b/interp/stdarg.ml index 56b995e537..e497c996f7 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -28,3 +28,8 @@ let () = register_name0 wit_bool "Stdarg.wit_bool" let () = register_name0 wit_int "Stdarg.wit_int" let () = register_name0 wit_string "Stdarg.wit_string" let () = register_name0 wit_pre_ident "Stdarg.wit_pre_ident" + +(** Aliases for compatibility *) + +let wit_integer = wit_int +let wit_preident = wit_pre_ident diff --git a/interp/stdarg.mli b/interp/stdarg.mli index d8904dab87..e1f648d7fc 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -19,3 +19,8 @@ val wit_int : int uniform_genarg_type val wit_string : string uniform_genarg_type val wit_pre_ident : string uniform_genarg_type + +(** Aliases for compatibility *) + +val wit_integer : int uniform_genarg_type +val wit_preident : string uniform_genarg_type -- cgit v1.2.3 From 27d173f94a68367d91def90c6d287138c733054b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 19 Mar 2016 18:55:01 +0100 Subject: Removing dead code in Genarg. --- interp/constrarg.ml | 21 --------------------- interp/stdarg.ml | 6 ------ 2 files changed, 27 deletions(-) (limited to 'interp') diff --git a/interp/constrarg.ml b/interp/constrarg.ml index 20ee7aa4fb..81e942d828 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -63,27 +63,6 @@ let wit_red_expr = Genarg.make0 "redexpr" let wit_clause_dft_concl = Genarg.make0 "clause_dft_concl" -(** Register location *) - -let () = - register_name0 wit_int_or_var "Constrarg.wit_int_or_var"; - register_name0 wit_ref "Constrarg.wit_ref"; - register_name0 wit_ident "Constrarg.wit_ident"; - register_name0 wit_var "Constrarg.wit_var"; - register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern"; - register_name0 wit_tactic "Constrarg.wit_tactic"; - register_name0 wit_sort "Constrarg.wit_sort"; - register_name0 wit_constr "Constrarg.wit_constr"; - register_name0 wit_uconstr "Constrarg.wit_uconstr"; - register_name0 wit_open_constr "Constrarg.wit_open_constr"; - register_name0 wit_constr_may_eval "Constrarg.wit_constr_may_eval"; - register_name0 wit_red_expr "Constrarg.wit_red_expr"; - register_name0 wit_clause_dft_concl "Constrarg.wit_clause_dft_concl"; - register_name0 wit_quant_hyp "Constrarg.wit_quant_hyp"; - register_name0 wit_bindings "Constrarg.wit_bindings"; - register_name0 wit_constr_with_bindings "Constrarg.wit_constr_with_bindings"; - () - (** Aliases *) let wit_reference = wit_ref diff --git a/interp/stdarg.ml b/interp/stdarg.ml index e497c996f7..244cdd0a70 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -23,12 +23,6 @@ let wit_string : string uniform_genarg_type = let wit_pre_ident : string uniform_genarg_type = make0 "preident" -let () = register_name0 wit_unit "Stdarg.wit_unit" -let () = register_name0 wit_bool "Stdarg.wit_bool" -let () = register_name0 wit_int "Stdarg.wit_int" -let () = register_name0 wit_string "Stdarg.wit_string" -let () = register_name0 wit_pre_ident "Stdarg.wit_pre_ident" - (** Aliases for compatibility *) let wit_integer = wit_int -- cgit v1.2.3 From dc7b77f09fe5e59e6e48486d9a8c0bdc6acf83b7 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 20 Mar 2016 16:59:15 +0100 Subject: Adding a new Ltac generic argument for forced tactics returing unit. --- interp/constrarg.ml | 2 ++ interp/constrarg.mli | 5 +++++ 2 files changed, 7 insertions(+) (limited to 'interp') diff --git a/interp/constrarg.ml b/interp/constrarg.ml index 81e942d828..46be0b8a1f 100644 --- a/interp/constrarg.ml +++ b/interp/constrarg.ml @@ -28,6 +28,8 @@ let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type = Genarg.make0 "tactic" +let wit_ltac = Genarg.make0 ~dyn:(val_tag (topwit Stdarg.wit_unit)) "ltac" + let wit_ident = Genarg.make0 "ident" diff --git a/interp/constrarg.mli b/interp/constrarg.mli index 1197b85a25..d38b1183c5 100644 --- a/interp/constrarg.mli +++ b/interp/constrarg.mli @@ -71,6 +71,11 @@ val wit_red_expr : val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type +(** [wit_ltac] is subtly different from [wit_tactic]: they only change for their + toplevel interpretation. The one of [wit_ltac] forces the tactic and + discards the result. *) +val wit_ltac : (raw_tactic_expr, glob_tactic_expr, unit) genarg_type + val wit_clause_dft_concl : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) genarg_type (** Aliases for compatibility *) -- cgit v1.2.3