From 2c4f099ffd44ff86cfa22324e8f67de93fc56796 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 9 Jan 2025 16:42:37 +0100 Subject: [PATCH 1/2] ci: test ocaml 5.3.0 (#1175) --- .github/workflows/main.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 7b7d3a929..dc3b5f3b6 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -8,7 +8,7 @@ jobs: strategy: fail-fast: false matrix: - ocaml-version: [5.2.1, 5.1.1, 5.0.0, 4.14.2, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1, 4.08.1] + ocaml-version: [5.3.0, 5.2.1, 5.1.1, 5.0.0, 4.14.2, 4.13.1, 4.12.1, 4.11.2, 4.10.2, 4.09.1, 4.08.1] runs-on: ubuntu-latest steps: - name: checking out lambdapi repo ... From 3d1786b2e45da6e161cd6aff959e9ffcb3a57537 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Thu, 9 Jan 2025 18:34:12 +0100 Subject: [PATCH 2/2] Does not allow underscores in assume tactic (#1171) - tactic: does not allow _ in assume - sig_state, scope: fix comments lambdapi-stdlib <= 1.1.0 is not compatible with this change. The master branch of lambdapi-stdlib is compatible with this change (since fe8c1758d469df1c1eabe0a09690603791e819c2 on 31/12/24). --- src/core/sig_state.ml | 16 ++--- src/handle/tactic.ml | 3 + src/parsing/scope.ml | 119 +++++++++++++++------------------- tests/{OK => KO}/anonymous.lp | 0 4 files changed, 60 insertions(+), 78 deletions(-) rename tests/{OK => KO}/anonymous.lp (100%) diff --git a/src/core/sig_state.ml b/src/core/sig_state.ml index 5074eaf80..3e7f7bc67 100644 --- a/src/core/sig_state.ml +++ b/src/core/sig_state.ml @@ -98,16 +98,12 @@ let of_sign : Sign.t -> sig_state = fun signature -> corresponding to a qualified / non qualified name *) type find_sym = prt:bool -> prv:bool -> sig_state -> qident loc -> sym -(** [find_sym ~prt ~prv b st qid] returns the symbol - corresponding to the qualified identifier [qid]. If [fst qid.elt] is - empty, we search for the name [snd qid.elt] in the opened modules of [st]. - The boolean [b] only indicates if the error message should mention - variables, in the case where the module path is empty and the symbol is - unbound. This is reported using the [Fatal] exception. - {!constructor:Term.expo.Protec} symbols from other modules - are allowed in left-hand side of rewrite rules (only) iff [~prt] is true. - {!constructor:Term.expo.Privat} symbols are allowed iff [~prv] - is [true]. *) +(** [find_sym ~prt ~prv b st qid] returns the symbol corresponding to the + possibly qualified identifier [qid], or raises [Fatal]. The boolean [b] + indicates if the error message should mention variables when [qid] is + unqualified. [~prt] indicates whether {!constructor:Term.expo.Protec} + symbols from other modules are allowed. [~prv] indicates whether + {!constructor:Term.expo.Privat} symbols are allowed. *) let find_sym : find_sym = fun ~prt ~prv st {elt = (mp, s); pos} -> let s = diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index 69224f8bc..73d84ce1b 100644 --- a/src/handle/tactic.ml +++ b/src/handle/tactic.ml @@ -250,6 +250,9 @@ let rec handle : let p = new_problem () in tac_refine pos ps gt gs p t | P_tac_assume idopts -> + (* Check that no idopt is None. *) + if List.exists ((=) None) idopts then + fatal pos "underscores not allowed in assume"; (* Check that the given identifiers are not already used. *) List.iter (Option.iter check) idopts; (* Check that the given identifiers are pairwise distinct. *) diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml index e15f69a97..f0381dc9d 100644 --- a/src/parsing/scope.ml +++ b/src/parsing/scope.ml @@ -11,15 +11,15 @@ open Core open Term open Env open Sig_state open Print let log_scop = Logger.make 'o' "scop" "term scoping" let log_scop = log_scop.pp -(** [find_qid prt prv ss env qid] returns a boxed term corresponding to a - variable of the environment [env] (or to a symbol) which name corresponds - to [qid]. In the case where the module path [fst qid.elt] is empty, we - first search for the name [snd qid.elt] in the environment, and if it is - not mapped we also search in the opened modules. The exception [Fatal] is - raised if an error occurs (e.g., when the name cannot be found). If [prt] - is true, protected symbols from external modules are allowed (protected - symbols from current modules are always allowed). If [prv] is true, private - symbols are allowed. *) +(** [find_qid ~find_sym prt prv ss env qid] returns a boxed term corresponding + to a variable of the environment [env] or a symbol which name corresponds + to [qid]. In case of a qualified identifier, we search in symbols using + [find_sym]. In case of an unqualified identifier, we first search in [env] + and the in symbols using [find_sym]. The exception [Fatal] is raised if an + error occurs (e.g. when the name cannot be found). If [prt] is true, + protected symbols from external modules are allowed (protected symbols + from current modules are always allowed). If [prv] is true, private + symbols are allowed. *) let find_qid : ?find_sym:find_sym -> bool -> bool -> sig_state -> env -> p_qident -> tbox = @@ -89,7 +89,8 @@ type mode = (** Scoping mode for unification rule right-hand sides. During scoping, we always have [m_urhs_vars_nb = m_lhs_size + length m_urhs_xvars]. *) -(** [scope_iden md ss env qid] scopes [qid] as a symbol. *) +(** [scope_iden ~find_sym md ss env qid] calls [find_qid] with the [prt] and + [prv] flags set according to [md]. *) let scope_iden : ?find_sym:find_sym -> mode -> sig_state -> env -> p_qident -> tbox = fun ?find_sym md ss env qid -> @@ -164,15 +165,10 @@ let _ = assert (valid "case_ex02_intro1"); assert (valid "case_ex02_intro10") -(** [scope ~typ md ss env t] turns a parser-level term [t] into an actual - term. The variables of the environment [env] may appear in [t], - and the scoping mode [md] changes the behaviour related to certain - constructors. The signature state [ss] is used to convert identifiers - into symbols according to [find_qid]. If [typ] is true, then [t] - must be a type (defaults to false). *) +(** [scope ~find_sym ~typ k md ss env t] turns a parser-level term [t] into an + actual term. *) let rec scope : ?find_sym:find_sym -> - ?typ:bool -> int -> mode -> sig_state -> env -> p_term -> - tbox = + ?typ:bool -> int -> mode -> sig_state -> env -> p_term -> tbox = fun ?find_sym ?(typ=false) k md ss env t -> if Logger.log_enabled () then log_scop "%a before Pratt: %a" D.depth k Pretty.term t; @@ -181,8 +177,8 @@ let rec scope : ?find_sym:find_sym -> log_scop "%a after Pratt: %a" D.depth k Pretty.term u; scope_parsed ?find_sym ~typ k md ss env u -(** [scope_parsed ~typ md ss env t] turns a parser-level Pratt-parsed - term [t] into an actual term. *) +(** [scope_parsed ~find_sym ~typ k md ss env t] turns a parser-level + Pratt-parsed term [t] into an actual term. *) and scope_parsed : ?find_sym:find_sym -> ?typ:bool -> int -> mode -> sig_state -> env -> p_term -> tbox = fun ?find_sym ?(typ=false) k md ss env t -> @@ -228,10 +224,10 @@ and scope_parsed : ?find_sym:find_sym -> |> D.log_and_return (fun e -> log_scop "%agot %a" D.depth k Raw.term (Bindlib.unbox e)) -(** [add_impl md ss env loc h impl args] scopes [args] and returns the - application of [h] to the scoped arguments. [impl] is a boolean list - described the implicit arguments. Implicit arguments are added as - underscores before scoping. *) +(** [add_impl ~find_sym k md ss env loc h impl args] scopes [args] and returns + the application of [h] to the scoped arguments. [impl] is a boolean list + described the implicit arguments. Implicit arguments are added as + underscores before scoping. *) and add_impl : ?find_sym:find_sym -> int -> mode -> sig_state -> Env.t -> popt -> tbox -> bool list -> p_term list -> tbox = fun ?find_sym k md ss env loc h impl args -> @@ -265,8 +261,8 @@ and add_impl : ?find_sym:find_sym -> int -> mode -> sig_state -> (* NOTE this could be improved with more general implicits. *) fatal loc "More arguments are required to instantiate implicits." -(** [scope_domain md ss env t] scopes [t] as the domain of an abstraction or - product. *) +(** [scope_domain ~find_sym k md ss env t] scopes [t] as the domain of an + abstraction or product. *) and scope_domain : ?find_sym:find_sym -> int -> mode -> sig_state -> env -> p_term option -> tbox = fun ?find_sym k md ss env a -> @@ -276,19 +272,16 @@ and scope_domain : ?find_sym:find_sym -> | (Some {elt=P_Wild;_}|None), _ -> _Plac true | Some a, _ -> scope ?find_sym ~typ:true k md ss env a -(** [scope_binder ~typ mode ss cons env params_list t] scopes [t] in - mode [md], signature state [ss] and environment [env]. [params_list] is a - list of paramters to abstract on. For each parameter, a tbox is built using - [cons] (either [_Abst] or [_Prod]). If [warn] is true (the default), a - warning is printed when the variable that is bound by the binder does not - appear in the body. [typ] indicates if we scope a type (default is - false). *) -and scope_binder : ?find_sym:find_sym -> - ?typ:bool -> int -> mode -> sig_state -> - (tbox -> tbinder Bindlib.box -> tbox) -> Env.t -> p_params list -> - p_term option -> tbox = +(** [scope_binder ~find_sym ~typ k md ss cons env params_list t] scopes [t], + abstract [params_list] and returns a tbox using [cons] (either [_Abst] or + [_Prod]). *) +and scope_binder : + ?find_sym:find_sym -> ?typ:bool -> int -> mode -> sig_state -> + (tbox -> tbinder Bindlib.box -> tbox) -> Env.t -> p_params list -> + p_term option -> tbox = fun ?find_sym ?(typ=false) k md ss cons env params_list t -> - let rec scope_params_list env params_list = + (* [n] is used to give different names to parameters of the form "_" *) + let rec scope_params_list n env params_list = match params_list with | [] -> begin @@ -298,14 +291,14 @@ and scope_binder : ?find_sym:find_sym -> end | (idopts,typopt,_implicit)::params_list -> let dom = scope_domain ?find_sym (k+1) md ss env typopt in - scope_params env idopts dom params_list - and scope_params env idopts a params_list = - let rec aux env idopts = + scope_params n env idopts dom params_list + and scope_params n env idopts a params_list = + let rec aux n env idopts = match idopts with - | [] -> scope_params_list env params_list + | [] -> scope_params_list n env params_list | None::idopts -> - let v = new_tvar "_" in - let t = aux env idopts in + let v = if n = 0 then new_tvar "_" else new_tvar_ind "_" n in + let t = aux (n+1) env idopts in cons a (Bindlib.bind_var v t) | Some {elt=id;pos}::idopts -> if is_invalid_bindlib_id id then @@ -314,13 +307,13 @@ and scope_binder : ?find_sym:find_sym -> are not allowed for bound variable names." id; let v = new_tvar id in let env = Env.add v a None env in - let t = aux env idopts in + let t = aux n env idopts in cons a (Bindlib.bind_var v t) - in aux env idopts + in aux n env idopts in - scope_params_list env params_list + scope_params_list 0 env params_list -(** [scope_head ~typ md ss env t] scopes [t] as term head. *) +(** [scope_head ~find_sym ~typ k md ss env t] scopes [t] as term head. *) and scope_head : ?find_sym:find_sym -> ?typ:bool -> int -> mode -> sig_state -> env -> p_term -> tbox = fun ?find_sym ?(typ=false) k md ss env t -> @@ -496,14 +489,9 @@ let scope = Debug.(record_time Scoping (fun () -> r := scope ?find_sym ~typ k md ss env t)); !r -(** [scope_term ~find_sym ~typ ~mok prv ss env t] turns a pterm [t] into a - term in the signature state [ss] and environment [env] (for bound - variables). If [prv] is [true], then the term can - contain private symbols. If [~typ] is [true], then [t] must be - a type (defaults to [false]). No {b new} metavariables may appear in - [t], but metavariables in the image of [mok] may be used. The function - [mok] defaults to the function constant to [None]. The function - [~find_sym] is used to scope symbol identifiers. *) +(** [scope_term ~find_sym ~typ ~mok prv ss env t] scopes [t] in mode [M_Term] + with [m_term_prv] set to [prv], and [m_term_meta_of_key] set to [mok] + (which defaults to the constant function equal to [None]). *) let scope_term : ?find_sym:find_sym -> ?typ:bool -> ?mok:(int -> meta option) -> bool -> sig_state -> env -> p_term -> term = @@ -511,12 +499,9 @@ let scope_term : let md = M_Term {m_term_meta_of_key=mok; m_term_prv} in Bindlib.unbox (scope ?find_sym ~typ 0 md ss env t) -(** [scope_search_pattern ~find_sym ~typ prv ss env t] turns a pterm [t] meant - to be a search patter into a term in the signature state [ss] - and environment [env] (for bound variables). If [~typ] is [true], - then [t] must be a type (defaults to [false]). No {b new} metavariables - may appear in [t]. The function [~find_sym] is used to scope symbol - identifiers. *) +(** [scope_search_pattern ~find_sym ~typ prv ss env t] scopes [t] in mode + [M_SearchPatt] with [m_term_meta_of_key] set to [mok] (which defaults to + the constant function equal to [None]). *) let scope_search_pattern : ?find_sym:find_sym -> ?typ:bool -> ?mok:(int -> meta option) -> sig_state -> env -> p_term -> term = fun ?find_sym ?(typ=false) ?(mok=fun _ -> None) ss env t -> @@ -612,8 +597,7 @@ let rule_of_pre_rule : pre_rule loc -> rule = ; rule_pos } (** [scope_rule ~find_sym ur ss r] turns a parser-level rewriting rule [r], - or a unification rule if [ur] is true, into a pre-rewriting rule. - The function [~find_sym] is used to scope symbol identifiers. *) + or a unification rule if [ur] is true, into a pre-rewriting rule. *) let scope_rule : ?find_sym:find_sym -> bool -> sig_state -> p_rule -> pre_rule loc = fun ?(find_sym=Sig_state.find_sym) ur ss { elt = (p_lhs, p_rhs); pos } -> @@ -720,13 +704,12 @@ let scope_rule : Pos.make pos prerule (** [scope_pattern ss env t] turns a parser-level term [t] into an actual term - that will correspond to selection pattern (rewrite tactic). *) + in mode [M_Patt], i.e. as a selection pattern in a rewrite tactic. *) let scope_pattern : sig_state -> env -> p_term -> term = fun ss env t -> Bindlib.unbox (scope 0 M_Patt ss env t) -(** [scope_rw_patt ss env t] turns a parser-level rewrite tactic specification - [s] into an actual rewrite specification (possibly containing variables of - [env] and using [ss] for aliasing). *) +(** [scope_rw_patt ss env s] scopes the parser-level rewrite tactic + specification [s] into an actual rewrite specification. *) let scope_rw_patt : sig_state -> env -> p_rw_patt -> (term, tbinder) rw_patt = fun ss env s -> match s.elt with diff --git a/tests/OK/anonymous.lp b/tests/KO/anonymous.lp similarity index 100% rename from tests/OK/anonymous.lp rename to tests/KO/anonymous.lp