diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 8056b1419..d68c3a661 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -4,6 +4,8 @@ on: push: paths-ignore: - '**/*.md' + - '**/*.bnf' + - '**/*.rst' workflow_dispatch: jobs: lambdapi: diff --git a/CHANGES.md b/CHANGES.md index 5ad328c13..d6274c20d 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -16,6 +16,9 @@ and this project adheres to [Semantic Versioning](https://semver.org/). ### Changed - Replaced Bindlib by de Bruijn (Frédéric) and closures (Bruno). The performances are slightly better than with Bindlib, especially on rewriting intensive files (the new version is 3.7 times faster on `tests/OK/perf_rw_engine.lp`). Lambdapi is now 2 times faster than dkcheck on matita, and only 2 times slower than dkcheck on holide. +- Terms are not kept in AC-canonical form any more. This allows to handle AC symbols more efficiently. +- When declaring a symbol as associative commutative, the side left or right is now mandatory. +- The ordering used to compare terms now compare arguments from left to right. This may require to permute some arguments for every thing to work again. - Several improvements to use the search engine: * normalize queries in websearch/search * pre-load a file in websearch (e.g. to declare implicit args) diff --git a/doc/commands.rst b/doc/commands.rst index 1a313eac6..f06b23bbd 100644 --- a/doc/commands.rst +++ b/doc/commands.rst @@ -116,26 +116,36 @@ the system with additional information on its properties and behavior. - ``constant``: No rule or definition can be given to the symbol - ``injective``: The symbol can be considered as injective, that is, if ``f t1 .. tn`` ≡ ``f u1 .. un``, then ``t1``\ ≡\ ``u1``, …, ``tn``\ ≡\ ``un``. For the moment, the verification is left to the user. - - ``commutative``: Adds in the conversion the equation ``f t u ≡ f u t``. - - ``associative``: Adds in the conversion the equation ``f (f t u) v ≡ f t (f u v)`` (in conjonction with ``commutative`` only). - - For handling commutative and associative-commutative symbols, - terms are systemically put in some canonical form following a - technique described `here - `__. - - If a symbol ``f`` is ``commutative`` and not ``associative`` then, - for every canonical term of the form ``f t u``, we have ``t ≤ u``, - where ``≤`` is a total ordering on terms left unspecified. - - If a symbol ``f`` is ``commutative`` and ``associative left`` then - there is no canonical term of the form ``f t (f u v)`` and thus - every canonical term headed by ``f`` is of the form ``f … (f (f t₁ - t₂) t₃) … tₙ``. If a symbol ``f`` is ``commutative`` and - ``associative`` or ``associative right`` then there is no - canonical term of the form ``f (f t u) v`` and thus every - canonical term headed by ``f`` is of the form ``f t₁ (f t₂ (f t₃ … - tₙ) … )``. Moreover, in both cases, we have ``t₁ ≤ t₂ ≤ … ≤ tₙ``. + + - ``commutative``: If a symbol ``f`` is ``commutative`` but not + ``associative`` then the reduction relation is enriched with the + following conditional rewriting rule: + + * ``f t u ↪ f u t`` if ``t > u`` + + where ``≤`` is a total ordering on terms such that: + * ``f t₁ t₂ < g u`` iff ``f <ᶠ g``, where ``≤ᶠ`` is a total ordering on function symbols and term constructors left unspecified; + * ``f t₁ t₂ < f u₁ u₂`` iff ``t₁ < u₁`` or else ``t₁ = u₁`` and ``t₂ < u₂`` (arguments are compare lexicographically from left to right). + + - ``left associative commutative``: In this case, the reduction + relation is enriched with the following conditional rewriting + rules: + + * ``f t (f u v) ↪ f (f t u) v`` + * ``f t u ↪ f u t`` if ``t > u`` + * ``f (f t u) v ↪ f (f u t) v`` if ``t > u`` + + - ``right associative commutative``: In this case, the reduction + relation is enriched with the following conditional rewriting + rules: + + * ``f (f t u) v ↪ f t (f u v)`` + * ``f t u ↪ f u t`` if ``t > u`` + * ``f t (f u v) ↪ f u (f t v)`` if ``t > u`` + + This can be used to identify terms modulo the following theories: + - ACI = AC + Idempotence: `max-suc algebra ` in the representation of type universe levels + - AG = AC + Inverse + Neutral: `linear arithmetic ` - **Exposition modifiers** define how a symbol can be used outside the module where it is defined. By default, the symbol can be used diff --git a/doc/lambdapi.bnf b/doc/lambdapi.bnf index 01a32963d..e26bb49f6 100644 --- a/doc/lambdapi.bnf +++ b/doc/lambdapi.bnf @@ -57,7 +57,7 @@ QID ::= [UID "."]+ UID ::= UID | QID - ::= [] "associative" + ::= "associative" "commutative" | "commutative" | "constant" | "injective" diff --git a/libraries/matita.sh b/libraries/matita.sh index 1cf108ad4..5a3ef710c 100755 --- a/libraries/matita.sh +++ b/libraries/matita.sh @@ -74,5 +74,6 @@ fi # Checking the files. cd ${DIR} +rm -f *.lpo \time -f "Finished in %E at %P with %MKb of RAM" \ lambdapi check --lib-root . --no-warnings -c matita.dk diff --git a/src/common/logger.ml b/src/common/logger.ml index 13d48f521..fdebfb6b0 100644 --- a/src/common/logger.ml +++ b/src/common/logger.ml @@ -95,7 +95,6 @@ let get_activated_loggers () = Without the optional argument, use [!default_loggers] *) let reset_loggers ?(default=Stdlib.(! default_loggers)) () = let default_value = String.contains default in - let fn { logger_key; logger_enabled; _ } = logger_enabled := default_value logger_key in @@ -106,10 +105,17 @@ let reset_loggers ?(default=Stdlib.(! default_loggers)) () = let log_summary () = List.map (fun d -> (d.logger_key, d.logger_desc)) Stdlib.(!loggers) -(** [set_debug_in b c f x] sets [c] logger to [b] for evaluating [f x]. *) -let set_debug_in : bool -> char -> ('a -> 'b) -> 'a -> 'b = fun b c f x -> +(** [set_debug_in c b f] sets [c] logger to [b] for evaluating [f()]. *) +let set_debug_in : char -> bool -> (unit -> 'a) -> 'a = fun c b f -> let is_activated = String.contains (get_activated_loggers()) in let v = is_activated c in let s = String.make 1 c in set_debug b s; - try let r = f x in set_debug v s; r with e -> set_debug v s; raise e + try let r = f() in set_debug v s; r with e -> set_debug v s; raise e + +(** [set_debug_in c b f] sets the loggers in [c] to [b] to evaluate [f()]. *) +let set_debug_in : string -> bool -> (unit -> 'a) -> 'a = fun s b f -> + let default = get_activated_loggers() in + set_debug b s; + try let r = f() in reset_loggers ~default (); r + with e -> reset_loggers ~default (); raise e diff --git a/src/common/logger.mli b/src/common/logger.mli index 38367eb97..78ec81ac7 100644 --- a/src/common/logger.mli +++ b/src/common/logger.mli @@ -32,5 +32,5 @@ val reset_loggers : ?default:string -> unit -> unit (** [log_summary ()] gives the keys and descriptions for logging options. *) val log_summary : unit -> (char * string) list -(** [set_debug_in b c f x] sets [c] logger to [b] for evaluating [f x]. *) -val set_debug_in : bool -> char -> ('a -> 'b) -> 'a -> 'b +(** [set_debug_in s b f] sets the loggers in [s] to [b] to evaluate [f()]. *) +val set_debug_in : string -> bool -> (unit -> 'a) -> 'a diff --git a/src/core/coercion.ml b/src/core/coercion.ml index dd1e70df5..e5d8b25f0 100644 --- a/src/core/coercion.ml +++ b/src/core/coercion.ml @@ -3,16 +3,16 @@ open Term let coerce : sym = let id = Pos.none "coerce" in - Sign.add_symbol Ghost.sign Public Defin Eager false id None mk_Kind [] + Sign.add_symbol Ghost.sign Public Defin Eager false id None Kind [] -let apply a b t : term = add_args (mk_Symb coerce) [a; b; t] +let apply a b t : term = add_args (Symb coerce) [a; b; t] let _ = (* Add the rule [coerce $A $A $t ↪ $t] (but we don't have access to the parser here) *) let rule = - let a = mk_Patt (Some 0, "A", [||]) - and t = mk_Patt (Some 1, "t", [||]) in + let a = Patt (Some 0, "A", [||]) + and t = Patt (Some 1, "t", [||]) in let lhs = [a;a;t] and arities = [|0;0|] and names = [|"A";"t"|] in { lhs; names; rhs=t; arity=3; arities; vars_nb=2; xvars_nb = 0; rule_pos = None } diff --git a/src/core/ctxt.ml b/src/core/ctxt.ml index 03d57bb16..e8234f577 100644 --- a/src/core/ctxt.ml +++ b/src/core/ctxt.ml @@ -28,8 +28,8 @@ let to_prod : ctxt -> term -> term * int = fun ctx t -> let b = bind_var x t in let u = match d with - | None -> mk_Prod (a,b) - | Some d -> mk_LLet (a,d,b) + | None -> Prod (a,b) + | Some d -> LLet (a,d,b) in u, k+1 in @@ -38,14 +38,14 @@ let to_prod : ctxt -> term -> term * int = fun ctx t -> (** [to_abst ctx t] builds a sequence of abstractions over the context [ctx], in the term [t]. *) let to_abst : ctxt -> term -> term = fun ctx t -> - let f t (x, a, _) = mk_Abst (a, bind_var x t) in + let f t (x, a, _) = Abst (a, bind_var x t) in List.fold_left f t ctx (** [to_let ctx t] adds the defined variables of [ctx] on top of [t]. *) let to_let : ctxt -> term -> term = fun ctx t -> let f t = function | _, _, None -> t - | x, a, Some u -> mk_LLet (a, u, bind_var x t) + | x, a, Some u -> LLet (a, u, bind_var x t) in List.fold_left f t ctx diff --git a/src/core/env.ml b/src/core/env.ml index 24e32a1a9..fde75120b 100644 --- a/src/core/env.ml +++ b/src/core/env.ml @@ -46,8 +46,8 @@ let to_prod : env -> term -> term = fun env t -> let add_prod t (_,(x,a,d)) = let b = bind_var x t in match d with - | None -> mk_Prod (a, b) - | Some d -> mk_LLet (a, d, b) + | None -> Prod (a, b) + | Some d -> LLet (a, d, b) in List.fold_left add_prod t env @@ -60,8 +60,8 @@ let to_abst : env -> term -> term = fun env t -> let add_abst t (_,(x,a,d)) = let b = bind_var x t in match d with - | None -> mk_Abst (a, b) - | Some d -> mk_LLet (a, d, b) + | None -> Abst (a, b) + | Some d -> LLet (a, d, b) in List.fold_left add_abst t env @@ -72,14 +72,14 @@ let vars : env -> var array = fun env -> (** [appl t env] applies [t] to the variables of [env]. *) let appl : term -> env -> term = fun t env -> - List.fold_right (fun (_,(x,_,_)) t -> mk_Appl (t, mk_Vari x)) env t + List.fold_right (fun (_,(x,_,_)) t -> Appl (t, Vari x)) env t (** [to_terms env] extracts the array of the variables in [env] and injects them in [tbox]. This is the same as [Array.map _Vari (vars env)]. Note that the order is reversed: [to_tbox [(xn,an);..;(x1,a1)] = [|x1;..;xn|]]. *) let to_terms : env -> term array = fun env -> - Array.of_list (List.rev_map (fun (_,(x,_,_)) -> mk_Vari x) env) + Array.of_list (List.rev_map (fun (_,(x,_,_)) -> Vari x) env) (** [to_ctxt e] converts an environment into a context. *) let to_ctxt : env -> ctxt = List.map snd @@ -142,5 +142,5 @@ let of_prod_using : ctxt -> var array -> term -> env * term = fun c xs t -> let xi = xs.(i) in let name = base_name xi in let env = add name xi a d env in - build_env (i+1) env (subst b (mk_Vari xi))) + build_env (i+1) env (subst b (Vari xi))) in build_env 0 [] t diff --git a/src/core/eval.ml b/src/core/eval.ml index 61061fcbc..16ca9a6c1 100644 --- a/src/core/eval.ml +++ b/src/core/eval.ml @@ -1,6 +1,6 @@ (** Evaluation and conversion. *) -open Lplib open Extra +open Lplib open Base open Extra open Common open Error open Debug open Term open Print @@ -46,7 +46,7 @@ let steps : int Stdlib.ref = Stdlib.ref 0 let hnf : (term -> term) -> (term -> term) = fun whnf -> let rec hnf t = match whnf t with - | Abst(a,t) -> mk_Abst(a, let x,t = unbind t in bind_var x (hnf t)) + | Abst(a,t) -> Abst(a, let x,t = unbind t in bind_var x (hnf t)) | t -> t in hnf @@ -65,122 +65,91 @@ let snf : (term -> term) -> (term -> term) = fun whnf -> -> t | LLet(_,t,b) -> snf (subst b t) | Prod(a,b) -> - mk_Prod(snf a, let x,b = unbind b in bind_var x (snf b)) + Prod(snf a, let x,b = unbind b in bind_var x (snf b)) | Abst(a,b) -> - mk_Abst(snf a, let x,b = unbind b in bind_var x (snf b)) - | Appl(t,u) -> mk_Appl(snf t, snf u) - | Meta(m,ts) -> mk_Meta(m, Array.map snf ts) - | Patt(i,n,ts) -> mk_Patt(i,n,Array.map snf ts) - | Bvar _ -> assert false - | Wild -> assert false - | TRef _ -> assert false + Abst(snf a, let x,b = unbind b in bind_var x (snf b)) + | Appl(t,u) -> Appl(snf t, snf u) + | Meta(m,ts) -> Meta(m, Array.map snf ts) + | Patt(i,n,ts) -> Patt(i,n,Array.map snf ts) + | Bvar _ -> assert false + | Wild -> assert false + | TRef _ -> assert false in snf -type rw_tag = [ `NoBeta | `NoRw | `NoExpand ] - -(** Configuration of the reduction engine. *) -module Config = struct - - type t = - { varmap : term VarMap.t (** Variable definitions. *) - ; rewrite : bool (** Whether to apply user-defined rewriting rules. *) - ; expand_defs : bool (** Whether to expand definitions. *) - ; beta : bool (** Whether to beta-normalise *) - ; dtree : sym -> dtree (** Retrieves the dtree of a symbol *) } - - (** [make ?dtree ?rewrite c] creates a new configuration with - tags [?rewrite] (being empty if not provided), context [c] and - dtree map [?dtree] (defaulting to getting the dtree from the symbol). - By default, beta reduction and rewriting is enabled for all symbols. *) - let make : ?dtree:(sym -> dtree) -> ?tags:rw_tag list -> ctxt -> t = - fun ?(dtree=fun sym -> Timed.(!(sym.sym_dtree))) ?(tags=[]) context -> - let beta = not @@ List.mem `NoBeta tags in - let expand_defs = not @@ List.mem `NoExpand tags in - let rewrite = not @@ List.mem `NoRw tags in - {varmap = Ctxt.to_map context; rewrite; expand_defs; beta; dtree} - - (** [unfold cfg a] unfolds [a] if it's a variable defined in the - configuration [cfg]. *) - let rec unfold : t -> term -> term = fun cfg a -> - match Term.unfold a with - | Vari x as a -> - begin match VarMap.find_opt x cfg.varmap with - | None -> a - | Some v -> unfold cfg v - end - | a -> a - -end - -type config = Config.t - -(** [eq_modulo whnf a b] tests the convertibility of [a] and [b] using - [whnf]. *) -let eq_modulo : (config -> term -> term) -> config -> term -> term -> bool = - fun whnf -> - let rec eq : config -> (term * term) list -> unit = fun cfg l -> +(** [eq_modulo norm a b] tests the convertibility of [a] and [b] by comparing + their [norm] forms. *) +let eq_modulo : (term -> term) -> term eq = fun norm -> + let rec eq : (term * term) list -> unit = fun l -> match l with | [] -> () | (a,b)::l -> - if Logger.log_enabled () then log_conv "eq: %a ≡ %a" term a term b; - if LibTerm.eq_alpha a b then eq cfg l else - let a = Config.unfold cfg a and b = Config.unfold cfg b in + if Logger.log_enabled () then + log_conv "eq_modulo %a ≡ %a %a" + term a term b (D.list (D.pair term term)) l; + (* We first check equality modulo alpha. *) + if LibTerm.eq_alpha a b then eq l else + (* FIXME? Instead of computing the norm of each side right away, we could + perhaps do it more incrementally (the reduction of beta-redexes, let's + and local definitions as done in whnf could be integrated here) and, + when both heads are function symbols, use an heuristic like in Matita + to decide which side to unfold first. + + Note also that, when comparing two AC symbols, we could detect the + non-equivalence more quickly by testing the equality of the number of + aliens: + + | (Symb f,([_;_]as ts)), (Symb g,([_;_]as us)) when is_ac f && g == f -> + let ts = aliens f norm ts and us = aliens f norm us in + let a = comb f norm ts and b = comb f norm us in + let ts = comb_aliens f a and us = comb_aliens f b in + if List.length ts <> List.length us then raise Exit + else eq (List.rev_append2 ts us l) *) + let a = norm a and b = norm b in + if Logger.log_enabled () then + log_conv "eq_modulo after norm %a ≡ %a" term a term b; match a, b with - | LLet(_,t,u), _ -> - let x,u = unbind u in - eq {cfg with varmap = VarMap.add x t cfg.varmap} ((u,b)::l) - | _, LLet(_,t,u) -> - let x,u = unbind u in - eq {cfg with varmap = VarMap.add x t cfg.varmap} ((a,u)::l) | Patt(None,_,_), _ | _, Patt(None,_,_) -> assert false | Patt(Some i,_,ts), Patt(Some j,_,us) -> - if i=j then eq cfg (List.add_array2 ts us l) else raise Exit + if i=j then eq (List.add_array2 ts us l) else raise Exit | Kind, Kind - | Type, Type -> eq cfg l - | Vari x, Vari y -> if eq_vars x y then eq cfg l else raise Exit - | Symb f, Symb g when f == g -> eq cfg l + | Type, Type -> eq l + | Vari x, Vari y when eq_vars x y -> eq l + | Symb f, Symb g when f == g -> eq l | Prod(a1,b1), Prod(a2,b2) | Abst(a1,b1), Abst(a2,b2) -> - let _,b1,b2 = unbind2 b1 b2 in eq cfg ((a1,a2)::(b1,b2)::l) - | Abst _, (Type|Kind|Prod _) - | (Type|Kind|Prod _), Abst _ -> raise Exit + let _,b1,b2 = unbind2 b1 b2 in eq ((a1,a2)::(b1,b2)::l) | (Abst(_ ,b), t | t, Abst(_ ,b)) when Timed.(!eta_equality) -> - let x,b = unbind b in eq cfg ((b, mk_Appl(t, mk_Vari x))::l) + let x,b = unbind b in eq ((b, Appl(t, Vari x))::l) | Meta(m1,a1), Meta(m2,a2) when m1 == m2 -> - eq cfg (if a1 == a2 then l else List.add_array2 a1 a2 l) - (* cases of failure *) - | Kind, _ | _, Kind - | Type, _ | _, Type -> raise Exit - | ((Symb f, (Vari _|Meta _|Prod _|Abst _)) - | ((Vari _|Meta _|Prod _|Abst _), Symb f)) when is_constant f -> - raise Exit - | _ -> - let a = whnf cfg a and b = whnf cfg b in - if Logger.log_enabled () then log_conv "whnf: %a ≡ %a" term a term b; - match a, b with - | Patt(None,_,_), _ | _, Patt(None,_,_) -> assert false - | Patt(Some i,_,ts), Patt(Some j,_,us) -> - if i=j then eq cfg (List.add_array2 ts us l) else raise Exit - | Kind, Kind - | Type, Type -> eq cfg l - | Vari x, Vari y when eq_vars x y -> eq cfg l - | Symb f, Symb g when f == g -> eq cfg l - | Prod(a1,b1), Prod(a2,b2) - | Abst(a1,b1), Abst(a2,b2) -> - let _,b1,b2 = unbind2 b1 b2 in eq cfg ((a1,a2)::(b1,b2)::l) - | (Abst(_ ,b), t | t, Abst(_ ,b)) when Timed.(!eta_equality) -> - let x,b = unbind b in eq cfg ((b, mk_Appl(t, mk_Vari x))::l) - | Meta(m1,a1), Meta(m2,a2) when m1 == m2 -> - eq cfg (if a1 == a2 then l else List.add_array2 a1 a2 l) - | Appl(t1,u1), Appl(t2,u2) -> eq cfg ((u1,u2)::(t1,t2)::l) + eq (if a1 == a2 then l else List.add_array2 a1 a2 l) | Bvar _, _ | _, Bvar _ -> assert false + | Appl(t1,u1), Appl(t2,u2) -> eq ((u1,u2)::(t1,t2)::l) | _ -> raise Exit in - fun cfg a b -> - if Logger.log_enabled () then log_conv "eq_modulo: %a ≡ %a" term a term b; - try eq cfg [(a,b)]; true + fun a b -> + try eq [(a,b)]; true with Exit -> if Logger.log_enabled () then log_conv "failed"; false +(** Reduction permissions. *) +type rw_tag = [ `NoRw | `NoExpand ] + +(** Configuration of the reduction engine. *) +type config = + { varmap : term VarMap.t (** Variable definitions. *) + ; rewrite : bool (** Whether to apply user-defined rewriting rules. *) + ; expand_defs : bool (** Whether to expand definitions. *) + ; dtree : sym -> dtree (** Retrieves the dtree of a symbol *) } + +(** [make ?dtree ?rewrite c] creates a new configuration with tags [?rewrite] + (being empty if not provided), context [c] and dtree map [?dtree] + (defaulting to getting the dtree from the symbol). By default, beta + reduction and rewriting is enabled for all symbols. *) +let make : ?dtree:(sym -> dtree) -> ?tags:rw_tag list -> ctxt -> config = + fun ?(dtree=fun sym -> Timed.(!(sym.sym_dtree))) ?(tags=[]) context -> + let expand_defs = not @@ List.mem `NoExpand tags in + let rewrite = not @@ List.mem `NoRw tags in + {varmap = Ctxt.to_map context; rewrite; expand_defs; dtree} + (** Abstract machine stack. *) type stack = term list @@ -188,104 +157,27 @@ type stack = term list {!constructor:TRef}. *) let to_tref : term -> term = fun t -> match t with - | Appl _ -> mk_TRef(Timed.ref(Some t)) - | Symb s when s.sym_prop <> Const -> mk_TRef(Timed.ref(Some t)) + | Appl _ -> TRef(Timed.ref(Some t)) + | Symb s when s.sym_prop <> Const -> TRef(Timed.ref(Some t)) | t -> t (** {1 Define the main {!whnf} function that takes a {!config} as argument} *) let depth = Stdlib.ref 0 -(** [whnf cfg t] computes a whnf of the term [t] wrt configuration [c]. *) -let rec whnf : config -> term -> term = fun cfg t -> - let n = Stdlib.(!steps) in - let u, stk = whnf_stk cfg t [] in - let r = if Stdlib.(!steps) <> n then add_args u stk else unfold t in - r +let incr_depth f = incr depth; let v = f() in decr depth; v -(** [whnf_stk cfg t stk] computes a whnf of [add_args t stk] wrt - configuration [c]. *) -and whnf_stk : config -> term -> stack -> term * stack = fun cfg t stk -> - if Logger.log_enabled () then - log_whnf "%awhnf_stk %a %a" D.depth !depth term t (D.list term) stk; - let t = unfold t in - match t, stk with - | Appl(f,u), stk -> whnf_stk cfg f (to_tref u::stk) - (*| _ -> +(** [tree_walk norm dt stk] tries to apply a rewrite rule by matching the + stack [stk] against the decision tree [dt], possibly reducing stack + elements with [norm]. The resulting state of the abstract machine is + returned in case of success. Even if matching fails, the stack [stk] may + be imperatively updated since a reduction step taken in elements of the + stack is preserved (this is done using {!constructor:Term.term.TRef}). *) +let tree_walk : (term -> term) -> dtree -> stack -> (term * stack) option = + fun norm tree stk -> if Logger.log_enabled () then - log_whnf "%awhnf_stk %a%a %a" D.depth !depth term t (D.list term) stk; - match t, stk with*) - | Abst(_,f), u::stk when cfg.Config.beta -> - Stdlib.incr steps; whnf_stk cfg (subst f u) stk - | LLet(_,t,u), stk -> - Stdlib.incr steps; whnf_stk cfg (subst u t) stk - | (Symb s as h, stk) as r -> - begin match Timed.(!(s.sym_def)) with - (* The invariant that defined symbols are subject to no - rewriting rules is false during indexing for websearch; - that's the reason for the when in the next line *) - | Some t when Tree_type.is_empty (cfg.dtree s) -> - if Timed.(!(s.sym_opaq)) || not cfg.Config.expand_defs then r else - (Stdlib.incr steps; whnf_stk cfg t stk) - | None when not cfg.Config.rewrite -> r - | _ -> - (* If [s] is modulo C or AC, we put its arguments in whnf and reorder - them to have a term in AC-canonical form. *) - let stk = - if is_modulo s then - let n = Stdlib.(!steps) in - (* We put the arguments in whnf. *) - let stk' = List.map (whnf cfg) stk in - if Stdlib.(!steps) = n then (* No argument has been reduced. *) - stk - else (* At least one argument has been reduced. *) - (* We put the term in AC-canonical form. *) - snd (get_args (add_args h stk')) - else stk - in - match tree_walk cfg (cfg.dtree s) stk with - | None -> h, stk - | Some (t', stk') -> - if Logger.log_enabled () then - log_whnf "%aapply rewrite rule" D.depth !depth; - Stdlib.incr steps; whnf_stk cfg t' stk' - end - | (Vari x, stk) as r -> - begin match VarMap.find_opt x cfg.varmap with - | Some v -> Stdlib.incr steps; whnf_stk cfg v stk - | None -> r - end - | r -> r - -(** {b NOTE} that in {!val:tree_walk} matching with trees involves two - collections of terms. - 1. The argument stack [stk] of type {!type:stack} which contains the terms - that are matched against the decision tree. - 2. An array [vars] containing subterms of the argument stack [stk] that - are filtered by a pattern variable. These terms may be used for - non-linearity or free-variable checks, or may be bound in the RHS. - - The [bound] array is similar to the [vars] array except that it is used to - save terms with free variables. *) - -(** {b NOTE} in the {!val:tree_walk} function, bound variables involve three - elements: - 1. a {!constructor:Term.term.Abst} which introduces the bound variable in - the term; - 2. a {!constructor:Term.term.Vari} which is the bound variable previously - introduced; - 3. a {!constructor:Tree_type.TC.t.Vari} which is a simplified - representation of a variable for trees. *) - -(** [tree_walk cfg dt stk] tries to apply a rewrite rule by matching the stack - [stk] against the decision tree [dt]. The resulting state of the abstract - machine is returned in case of success. Even if matching fails, the stack - [stk] may be imperatively updated since a reduction step taken in elements - of the stack is preserved (this is done using - {!constructor:Term.term.TRef}). *) -and tree_walk : config -> dtree -> stack -> (term * stack) option = - fun cfg tree stk -> + log_whnf "%atree_walk %a" D.depth !depth (D.list term) stk; let (lazy capacity, lazy tree) = tree in - let vars = Array.make capacity mk_Kind in (* dummy terms *) + let vars = Array.make capacity Kind in (* dummy terms *) let bound = Array.make capacity None in (* [walk tree stk cursor vars_id id_vars] where [stk] is the stack of terms to match and [cursor] the cursor indicating where to write in the [vars] @@ -314,14 +206,15 @@ and tree_walk : config -> dtree -> stack -> (term * stack) option = List.iter f rhs_subst; (* Complete the array with fresh meta-variables if needed. *) for i = r.vars_nb to env_len - 1 do - env.(i) <- Some(bind_mvar [||] (mk_Plac false)) + env.(i) <- Some(bind_mvar [||] (Plac false)) done; Some (subst_patt env r.rhs, stk) | Cond({ok; cond; fail}) -> let next = match cond with | CondNL(i, j) -> - if eq_modulo whnf cfg vars.(i) vars.(j) then ok else fail + if incr_depth (fun () -> eq_modulo norm vars.(i) vars.(j)) + then ok else fail | CondFV(i,xs) -> let allowed = (* Variables that are allowed in the term. *) @@ -344,7 +237,7 @@ and tree_walk : config -> dtree -> stack -> (term * stack) option = if no_forbidden b then (bound.(i) <- Some b; ok) else (* As a last resort we try matching the SNF. *) - let b = bind_mvar allowed (snf (whnf cfg) vars.(i)) in + let b = bind_mvar allowed (snf norm vars.(i)) in if no_forbidden b then (bound.(i) <- Some b; ok) else fail @@ -371,11 +264,9 @@ and tree_walk : config -> dtree -> stack -> (term * stack) option = Option.bind default fn else let s = Stdlib.(!steps) in - incr depth; - let (t, args) = whnf_stk cfg examined [] in - decr depth; + let (t, args) = incr_depth (fun () -> get_args (norm examined)) in let args = if store then List.map to_tref args else args in - (* If some reduction has been performed by [whnf_stk] ([steps <> + (* If some reduction has been performed by [norm] ([steps <> 0]), update the value of [examined] which may be stored into [vars]. *) if Stdlib.(!steps) <> s then @@ -456,28 +347,321 @@ and tree_walk : config -> dtree -> stack -> (term * stack) option = | Meta(_, _) -> default () | Plac _ -> assert false (* Should not appear in typechecked terms. *) - | TRef(_) -> assert false (* Should be reduced by [whnf_stk]. *) - | Appl(_) -> assert false (* Should be reduced by [whnf_stk]. *) - | LLet(_) -> assert false (* Should be reduced by [whnf_stk]. *) + | TRef(_) -> assert false (* Should be reduced by [norm]. *) + | Appl(_) -> assert false (* Should be reduced by [norm]. *) + | LLet(_) -> assert false (* Should be reduced by [norm]. *) | Bvar _ -> assert false | Wild -> assert false (* Should not appear in terms. *) in walk tree stk 0 VarMap.empty IntMap.empty +(** {b NOTE} that in {!val:tree_walk} matching with trees involves two + collections of terms. + 1. The argument stack [stk] of type {!type:stack} which contains the terms + that are matched against the decision tree. + 2. An array [vars] containing subterms of the argument stack [stk] that + are filtered by a pattern variable. These terms may be used for + non-linearity or free-variable checks, or may be bound in the RHS. + + The [bound] array is similar to the [vars] array except that it is used to + save terms with free variables. *) + +(** {b NOTE} in the {!val:tree_walk} function, bound variables involve three + elements: + 1. a {!constructor:Term.term.Abst} which introduces the bound variable in + the term; + 2. a {!constructor:Term.term.Vari} which is the bound variable previously + introduced; + 3. a {!constructor:Tree_type.TC.t.Vari} which is a simplified + representation of a variable for trees. *) + +(** [insert t ts] inserts [t] in [ts] assuming that [ts] is in increasing + order wrt [Term.comp]. *) +let insert t = + let rec aux ts = + match ts with + | t1::ts when cmp t t1 > 0 -> t1::aux ts + | _ -> t::ts + in aux + +(** [aliens f norm ts] computes the f-aliens of [ts]. f-aliens are normalized + wrt [norm] and ordered in increasing order wrt [Term.comp]. *) +let aliens f norm = + let rec aliens acc ts = + match ts with + | [] -> acc + | t::ts -> aux acc t ts + and aux acc t ts = + match get_args t with + | Symb g, [u1;u2] when g == f -> aux acc u1 (u2::ts) + | _ -> + let n = !steps in + let t' = norm t in + if !steps = n then aliens (insert t acc) ts + else aux acc t' ts + in aliens [] + +(* +(** [left_comb_aliens f t] computes the aliens of [t] assuming that [t] is a + left comb. *) +let left_comb_aliens f = + let rec aliens acc t = + match get_args t with + | Symb g, [t1;t2] when g == f -> aliens (t2::acc) t1 + | _ -> t::acc + in aliens [] + +(** [right_comb_aliens f t] computes the aliens of [t] assuming that [t] is a + right comb. *) +let right_comb_aliens f = + let rec aliens acc t = + match get_args t with + | Symb g, [t1;t2] when g == f -> aliens (t1::acc) t2 + | _ -> t::acc + in aliens [] + +(** [comb_aliens f t] computes the aliens of [t] assuming that [t] is a + comb. *) +let comb_aliens f = + match f.sym_prop with + | AC Left -> left_comb_aliens f + | AC Right -> right_comb_aliens f + | _ -> assert false +*) + +(** [app2 s t1 t2] builds the application of [s] to [t1] and [t2]. *) +let app2 s t1 t2 = Appl(Appl(Symb s, t1), t2) + +(** [left_comb norm (+) [t1;t2;t3]] computes [norm(norm(t1+t2)+t3)]. *) +let left_comb s norm = + let rec comb acc ts = + match ts with + | [] -> acc + | t::ts -> comb (norm (app2 s acc t)) ts + in + function + | [] | [_] -> assert false + | t::ts -> comb t ts + +(** [right_comb norm (+) [t1;t2;t3]] computes [norm(t1+norm(t2+t3))]. *) +let right_comb s norm = + let rec comb ts acc = + match ts with + | [] -> acc + | t::ts -> comb ts (norm (app2 s t acc)) + in + fun ts -> + match List.rev ts with + | [] | [_] -> assert false + | t::ts -> comb ts t + +(** [comb s norm ts] computes the [norm]-form of the comb obtained by applying + [s] to [ts]. *) +let comb s = + match s.sym_prop with + | AC Left -> left_comb s + | AC Right -> right_comb s + | _ -> assert false + +(** [sym_norm s t] computes the normal form of [t] wrt [s] rules. *) +let sym_norm s = + let rec norm ((h,ts) as v) = + match h with + | Symb s' when s' == s -> + begin + match tree_walk (fun t -> t) Timed.(!(s.sym_dtree)) ts with + | None -> v + | Some v -> + if Logger.log_enabled () then + log_whnf "%aapply rewrite rule" D.depth !depth; + Stdlib.incr steps; norm v + end + | _ -> v + in + fun t -> + if Logger.log_enabled() then + log_whnf "%asym_norm %a" D.depth !depth term t; + let h,ts = norm (get_args t) in add_args h ts + +(** [ac norm t] computes a head-AC [norm] form. *) +let ac norm t = + let t = norm t in + match get_args t with + | Symb f, ([t1;t2] as ts) -> + begin match f.sym_prop with + | AC _ -> comb f norm (aliens f norm ts) + | Commu when cmp t1 t2 > 0 -> app2 f t2 t1 + | _ -> t + end + | _ -> t + +(** If [t] is headed by an AC symbol, then [ac norm t] computes its head-AC + [norm] form. *) +let new_ac t = + match get_args t with + | Symb s, ([t1;t2] as ts) -> + begin match s.sym_prop with + | AC _ -> comb s (sym_norm s) (aliens s (fun t -> t) ts) + | Commu when cmp t1 t2 > 0 -> app2 s t2 t1 + | _ -> t + end + | _ -> t + +(** If [t] is headed by a sequential symbol, then [seq norm t] computes a + [norm] form of [t] so that each immediate subterm is also in [seq norm] + form. Otherwise, [seq norm t = norm t]. *) +let rec seq norm t = + match get_args t with + | Symb s, _ when s.sym_mstrat = Sequen -> + begin + let t = norm t in + let h, ts = get_args t in + match h with + | Symb _ -> add_args_map h (seq norm) ts + | _ -> t + end + | _ -> norm t + +(** [whnf cfg t] computes a whnf of the term [t] wrt configuration [cfg]. *) +let whnf : config -> term -> term = fun cfg -> + (* [whnf t] computes a whnf of [t]. *) + let rec whnf t = + let n = Stdlib.(!steps) in + let u, stk = whnf_stk t [] in + if Stdlib.(!steps) <> n then add_args u stk else unfold t + + (* [whnf_stk t stk] computes a whnf of [add_args t stk]. *) + and whnf_stk : term -> stack -> term * stack = fun t stk -> + if Logger.log_enabled () then + log_whnf "%awhnf_stk %a %a" D.depth !depth term t (D.list term) stk; + let t = unfold t in + match t with + | Appl(f,u) -> whnf_stk f (to_tref u::stk) + (*| _ -> + if Logger.log_enabled() then + log_whnf "%awhnf_stk %a %a" D.depth !depth term t (D.list term) stk; + match t, stk with*) + | Abst(_,f) -> + begin + match stk with + | u::stk -> Stdlib.incr steps; whnf_stk (subst f u) stk + | _ -> t, stk + end + | LLet(_,t,u) -> + (*FIXME? instead of doing a substitution now, add a local definition + instead to postpone the substitution when it will be necessary. But + the following makes tests/OK/725.lp fail: *) + (*let x,u = unbind u in + whnf_stk {cfg with varmap = VarMap.add x t cfg.varmap} u stk*) + Stdlib.incr steps; whnf_stk (subst u t) stk + | Symb s -> + begin match Timed.(!(s.sym_def)) with + (* The invariant that defined symbols are subject to no + rewriting rules is false during indexing for websearch; + that's the reason for the when in the next line *) + | Some u when Tree_type.is_empty (cfg.dtree s) -> + if Timed.(!(s.sym_opaq)) || not cfg.expand_defs then t, stk + else (Stdlib.incr steps; whnf_stk u stk) + | None when not cfg.rewrite -> t, stk + | _ -> + let norm = + if Timed.(!(s.sym_rstrat)) = Innermost then + fun t -> new_ac (seq whnf t) + else whnf + in + match tree_walk norm (cfg.dtree s) stk with + | None -> t, stk + | Some (t, stk) -> + if Logger.log_enabled () then + log_whnf "%aapply rewrite rule" D.depth !depth; + Stdlib.incr steps; whnf_stk t stk + end + | Vari x -> + begin match VarMap.find_opt x cfg.varmap with + | Some v -> Stdlib.incr steps; whnf_stk v stk + | None -> t, stk + end + | _ -> t, stk +(* + (* [snf t] computes snf of [t]. *) + and snf t = + let n = Stdlib.(!steps) in + let u, stk = snf_stk t [] in + if Stdlib.(!steps) <> n then add_args u stk else unfold t + + (* [snf_stk t stk] computes a snf of [add_args t stk]. *) + and snf_stk : term -> stack -> term * stack = fun t stk -> + if Logger.log_enabled () then + log_whnf "%asnf_stk %a %a" D.depth !depth term t (D.list term) stk; + let t = unfold t in + match t with + | Appl(f,u) -> snf_stk f (to_tref u::stk) + (*| _ -> + if Logger.log_enabled() then + log_snf "%asnf_stk %a %a" D.depth !depth term t (D.list term) stk; + match t, stk with*) + | Abst(a,b) -> + begin + match stk with + | u::stk when cfg.beta -> Stdlib.incr steps; snf_stk (subst b u) stk + | _ -> Abst(snf a, binder snf b), List.map snf stk + end + | LLet(_,t,u) -> + (*FIXME? instead of doing a substitution now, add a local definition + instead to postpone the substitution when it will be necessary. But + the following makes tests/OK/725.lp fail: *) + (*let x,u = unbind u in + snf_stk {cfg with varmap = VarMap.add x t cfg.varmap} u stk*) + Stdlib.incr steps; snf_stk (subst u t) stk + | Symb s -> + begin match Timed.(!(s.sym_def)) with + (* The invariant that defined symbols are subject to no + rewriting rules is false during indexing for websearch; + that's the reason for the when in the next line *) + | Some u when Tree_type.is_empty (cfg.dtree s) -> + if Timed.(!(s.sym_opaq)) || not cfg.expand_defs then + t, List.map snf stk + else (Stdlib.incr steps; snf_stk u stk) + | None when not cfg.rewrite -> t, List.map snf stk + | _ -> + match tree_walk whnf (cfg.dtree s) stk with + | None -> t, List.map snf stk + | Some (t', stk') -> + if Logger.log_enabled () then + log_snf "%aapply rewrite rule" D.depth !depth; + Stdlib.incr steps; snf_stk t' stk' + end + | Vari x -> + begin match VarMap.find_opt x cfg.varmap with + | Some v -> Stdlib.incr steps; snf_stk v stk + | None -> t, List.map snf stk + end + | Prod(a,b) -> Prod(snf a, binder snf b), stk + | Type -> t, stk + | Kind -> t, stk + | Plac _ -> t, stk (* may happen when reducing coercions *) + | Meta(m,ts) -> Meta(m,Array.map snf ts), List.map snf stk + | Patt(i,n,ts) -> Patt(i,n,Array.map snf ts), List.map snf stk + | Bvar _ -> assert false + | Wild -> assert false + | TRef _ -> assert false + *) + in fun t -> ac whnf (seq whnf t) + (** {1 Define exposed functions} that take optional arguments rather than a config. *) type reducer = ?tags:rw_tag list -> ctxt -> term -> term let time_reducer (f: reducer): reducer = - let open Stdlib in let r = ref mk_Kind in fun ?tags cfg t -> + let open Stdlib in let r = ref Kind in fun ?tags cfg t -> Debug.(record_time Rewriting (fun () -> r := f ?tags cfg t)); !r (** [snf ~dtree c t] computes a snf of [t], unfolding the variables defined in the context [c]. The function [dtree] maps symbols to dtrees. *) let snf : ?dtree:(sym -> dtree) -> reducer = fun ?dtree ?tags c t -> Stdlib.(steps := 0); - let u = snf (whnf (Config.make ?dtree ?tags c)) t in + let u = snf (whnf (make ?dtree ?tags c)) t in if Stdlib.(!steps = 0) then unfold t else u let snf ?dtree = time_reducer (snf ?dtree) @@ -486,7 +670,7 @@ let snf ?dtree = time_reducer (snf ?dtree) context [c], and using user-defined rewrite rules. *) let hnf : reducer = fun ?tags c t -> Stdlib.(steps := 0); - let u = hnf (whnf (Config.make ?tags c)) t in + let u = hnf (whnf (make ?tags c)) t in if Stdlib.(!steps = 0) then unfold t else u let hnf = time_reducer hnf @@ -494,7 +678,7 @@ let hnf = time_reducer hnf (** [eq_modulo c a b] tests the convertibility of [a] and [b] in context [c]. WARNING: may have side effects in TRef's introduced by whnf. *) let eq_modulo : ?tags:rw_tag list -> ctxt -> term -> term -> bool = - fun ?tags c -> eq_modulo whnf (Config.make ?tags c) + fun ?tags c -> eq_modulo (whnf (make ?tags c)) let eq_modulo = let open Stdlib in let r = ref false in fun ?tags c t u -> @@ -504,13 +688,16 @@ let eq_modulo = [c] with no side effects. *) let pure_eq_modulo : ?tags:rw_tag list -> ctxt -> term -> term -> bool = fun ?tags c a b -> - Timed.pure_test (fun (c,a,b) -> eq_modulo ?tags c a b) (c,a,b) + Timed.pure_test + (fun (c,a,b) -> + ((*Logger.set_debug_in "ce" false (fun () ->*) eq_modulo ?tags c a b)) + (c,a,b) (** [whnf c t] computes a whnf of [t], unfolding the variables defined in the context [c], and using user-defined rewrite rules if [~rewrite]. *) let whnf : reducer = fun ?tags c t -> Stdlib.(steps := 0); - let u = whnf (Config.make ?tags c) t in + let u = whnf (make ?tags c) t in if Stdlib.(!steps = 0) then unfold t else u let whnf = time_reducer whnf @@ -524,12 +711,12 @@ let beta_simplify : ctxt -> term -> term = fun c -> match get_args (whnf ~tags c t) with | Prod(a,b), _ -> let x, b = unbind b in - mk_Prod (simp a, bind_var x (simp b)) + Prod (simp a, bind_var x (simp b)) | h, ts -> add_args_map h (whnf ~tags c) ts in simp let beta_simplify = - let open Stdlib in let r = ref mk_Kind in fun c t -> + let open Stdlib in let r = ref Kind in fun c t -> Debug.(record_time Rewriting (fun () -> r := beta_simplify c t)); !r (** If [s] is a non-opaque symbol having a definition, [unfold_sym s t] @@ -545,11 +732,11 @@ let unfold_sym : sym -> term -> term = | _ -> let h = match h with - | Abst(a,b) -> mk_Abst(unfold_sym a, unfold_sym_binder b) - | Prod(a,b) -> mk_Prod(unfold_sym a, unfold_sym_binder b) - | Meta(m,ts) -> mk_Meta(m, Array.map unfold_sym ts) + | Abst(a,b) -> Abst(unfold_sym a, unfold_sym_binder b) + | Prod(a,b) -> Prod(unfold_sym a, unfold_sym_binder b) + | Meta(m,ts) -> Meta(m, Array.map unfold_sym ts) | LLet(a,t,u) -> - mk_LLet(unfold_sym a, unfold_sym t, unfold_sym_binder u) + LLet(unfold_sym a, unfold_sym t, unfold_sym_binder u) | _ -> h in add_args h args and unfold_sym_binder b = @@ -564,11 +751,10 @@ let unfold_sym : sym -> term -> term = match Timed.(!(s.sym_rules)) with | [] -> fun t -> t | _ -> - let cfg = Config.make [] and dt = Timed.(!(s.sym_dtree)) in let unfold_sym_app args = - match tree_walk cfg dt args with + match tree_walk (whnf []) Timed.(!(s.sym_dtree)) args with | Some(r,ts) -> add_args r ts - | None -> add_args (mk_Symb s) args + | None -> add_args (Symb s) args in unfold_sym s unfold_sym_app (** Dedukti evaluation strategies. *) @@ -582,8 +768,8 @@ type strat = { strategy : strategy (** Evaluation strategy. *) ; steps : int option (** Max number of steps if given. *) } -(** [eval cfg c t] evaluates the term [t] in the context [c] according to - evaluation configuration [cfg]. *) +(** [eval s c t] evaluates the term [t] in the context [c] according to + strategy [s]. *) let eval : strat -> ctxt -> term -> term = fun s c t -> match s.strategy, s.steps with | _, Some 0 diff --git a/src/core/eval.mli b/src/core/eval.mli index fec870f0d..f7bf7a2a6 100644 --- a/src/core/eval.mli +++ b/src/core/eval.mli @@ -23,8 +23,7 @@ val eta_equality : bool Timed.ref (** Tags for rewriting configuration. *) type rw_tag = - [ `NoBeta (** If true, no beta-reduction is performed. *) - | `NoRw (** If true, no user-defined rewrite rule is used. *) + [ `NoRw (** If true, no user-defined rewrite rule is used. *) | `NoExpand (** If true, definitions are not expanded. *) ] (** Functions that use the rewriting engine and accept an optional argument diff --git a/src/core/infer.ml b/src/core/infer.ml index 866636d84..f5a04c870 100644 --- a/src/core/infer.ml +++ b/src/core/infer.ml @@ -61,20 +61,20 @@ let rec reduce_coercions : ctxt -> term -> term option = fun c t -> | Type | Vari _ | Symb _ | Meta _ -> return t | Appl (t, u) -> let* t = reduce_coercions c t in let* u = reduce_coercions c u in - return (mk_Appl (t, u)) + return (Appl (t, u)) | Abst (a, b) -> let* a = reduce_coercions c a in let* b = reduce_coercions_binder b in - return (mk_Abst (a, b)) + return (Abst (a, b)) | Prod (a, b) -> let* a = reduce_coercions c a in let* b = reduce_coercions_binder b in - return (mk_Prod (a, b)) + return (Prod (a, b)) | LLet (a, e, b) -> let* a = reduce_coercions c a in let* e = reduce_coercions c e in let* b = reduce_coercions_binder b in - return (mk_LLet (a, e, b)) + return (LLet (a, e, b)) (** [coerce pb c t a b] coerces term [t] from type [a] to type [b] in context [c] and problem [pb]. *) @@ -105,9 +105,9 @@ and type_enforce : problem -> ctxt -> term -> term * term * bool = let a, s, cui = infer pb c a in let sort = match unfold s with - | Kind -> mk_Kind - | Type -> mk_Type - | _ -> mk_Type + | Kind -> Kind + | Type -> Type + | _ -> Type (* FIXME The algorithm should be able to backtrack on the choice of this sort, first trying [Type], and if it does not succeed, trying [Kind]. *) @@ -123,8 +123,8 @@ and force : problem -> ctxt -> term -> term -> term * bool = log "Force [%a] of [%a]" term te term ty; match unfold te with | Plac true -> - unif pb c ty mk_Type; - (LibMeta.make pb c mk_Type, true) + unif pb c ty Type; + (LibMeta.make pb c Type, true) | Plac false -> (LibMeta.make pb c ty, true) | _ -> @@ -140,16 +140,16 @@ and infer_aux : problem -> ctxt -> term -> term * term * bool = | Kind -> assert false | Wild -> assert false | TRef _ -> assert false - | Type -> (mk_Type, mk_Kind, false) + | Type -> (Type, Kind, false) | Vari x -> let a = try Ctxt.type_of x c with Not_found -> assert false in (t, a, false) | Symb s -> (t, !(s.sym_type), false) | Plac true -> - let m = LibMeta.make pb c mk_Type in - (m, mk_Type, true) + let m = LibMeta.make pb c Type in + (m, Type, true) | Plac false -> - let mt = LibMeta.make pb c mk_Type in + let mt = LibMeta.make pb c Type in let m = LibMeta.make pb c mt in (m, mt, true) (* All metavariables inserted are typed. *) @@ -192,34 +192,34 @@ and infer_aux : problem -> ctxt -> term -> term * term * bool = raise NotTypable | _ -> () ); let u_ty = bind_var x u_ty in - let top_ty = mk_LLet (t_ty, t, u_ty) in + let top_ty = LLet (t_ty, t, u_ty) in let cu = cu_t_ty || cu_t || cu_u in let top = if cu then let u = bind_var x u in - mk_LLet(t_ty, t, u) + LLet(t_ty, t, u) else top in (top, top_ty, cu) | Abst (dom, b) as top -> (* Domain must by of type Type (and not Kind) *) - let dom, cu_dom = force pb c dom mk_Type in + let dom, cu_dom = force pb c dom Type in let (x, b) = unbind b in let c = (x,dom,None)::c in let b, range, cu_b = infer pb c b in let range = bind_var x range in - let top_ty = mk_Prod (dom, range) in + let top_ty = Prod (dom, range) in let cu = cu_b || cu_dom in let top = if cu then let b = bind_var x b in - mk_Abst (dom, b) + Abst (dom, b) else top in (top, top_ty, cu) | Prod (dom, b) as top -> (* Domain must by of type Type (and not Kind) *) - let dom, cu_dom = force pb c dom mk_Type in + let dom, cu_dom = force pb c dom Type in let (x, b) = unbind b in let c = (x,dom,None)::c in let b, b_s, cu_b = type_enforce pb c b in @@ -227,7 +227,7 @@ and infer_aux : problem -> ctxt -> term -> term * term * bool = let top = if cu then let b = bind_var x b in - mk_Prod (dom, b) + Prod (dom, b) else top in (top, b_s, cu) @@ -235,7 +235,7 @@ and infer_aux : problem -> ctxt -> term -> term * term * bool = let t, t_ty, cu_t = infer pb c t in let return m t u range = let ty = subst range u and cu = cu_t || m in - if cu then (mk_Appl (t, u), ty, cu) else (top, ty, cu) + if cu then (Appl (t, u), ty, cu) else (top, ty, cu) in match Eval.whnf c t_ty with | Prod (dom, range) -> @@ -246,12 +246,12 @@ and infer_aux : problem -> ctxt -> term -> term * term * bool = | Meta (_, _) -> let u, u_ty, cu_u = infer pb c u in let range = LibMeta.make_codomain pb c u_ty in - unif pb c t_ty (mk_Prod (u_ty, range)); + unif pb c t_ty (Prod (u_ty, range)); return cu_u t u range | t_ty -> - let domain = LibMeta.make pb c mk_Type in + let domain = LibMeta.make pb c Type in let range = LibMeta.make_codomain pb c domain in - let t, cu_t' = coerce pb c t t_ty (mk_Prod (domain, range)) in + let t, cu_t' = coerce pb c t t_ty (Prod (domain, range)) in if Logger.log_enabled () then log "Appl-default arg [%a]" term u; let u, cu_u = force pb c u domain in diff --git a/src/core/inverse.ml b/src/core/inverse.ml index 3333e02a6..31ef0b629 100644 --- a/src/core/inverse.ml +++ b/src/core/inverse.ml @@ -81,7 +81,7 @@ let prod_graph : sym -> (sym * sym * sym * bool) list = fun s -> match get_args a with | Symb s1, [_] -> begin - match get_args (subst b mk_Kind) with + match get_args (subst b Kind) with | Symb(s2), [_] -> add (s0,s1,s2,binder_occur b) l | _ -> l end @@ -118,7 +118,7 @@ let rec inverse : sym -> term -> term = fun s v -> if Logger.log_enabled () then log "compute %a⁻¹(%a)" sym s term v; match get_args v with | Symb s', [t] when s' == s -> t - | Symb s', ts -> add_args (mk_Symb (inverse_const s s')) ts + | Symb s', ts -> add_args (Symb (inverse_const s s')) ts | Prod(a,b), _ -> let s0,s1,s2,occ = match get_args a with @@ -129,13 +129,13 @@ let rec inverse : sym -> term -> term = fun s v -> let t2 = let x, b = unbind b in let b = inverse s2 b in - if occ then mk_Abst (a, bind_var x b) else b + if occ then Abst (a, bind_var x b) else b in - add_args (mk_Symb s0) [t1;t2] + add_args (Symb s0) [t1;t2] | _ -> raise Not_found let inverse : sym -> term -> term = fun s v -> - let t = inverse s v in let v' = mk_Appl(mk_Symb s,t) in + let t = inverse s v in let v' = Appl(Symb s,t) in if Eval.eq_modulo [] v' v then t else (if Logger.log_enabled() then log "%a ≢ %a@" term v' term v; raise Not_found) diff --git a/src/core/libMeta.ml b/src/core/libMeta.ml index 0b942eafd..73851c036 100644 --- a/src/core/libMeta.ml +++ b/src/core/libMeta.ml @@ -29,7 +29,7 @@ let fresh : problem -> term -> int -> meta = fun p a n -> care. *) let set : problem -> meta -> mbinder -> unit = fun p m v -> m.meta_value := Some v; - m.meta_type := mk_Kind (* to save memory *); + m.meta_type := Kind (* to save memory *); p := {!p with metas = MetaSet.remove m !p.metas} (** [make p ctx a] creates a fresh metavariable term of type [a] in the @@ -37,14 +37,14 @@ let set : problem -> meta -> mbinder -> unit = fun p m v -> let make : problem -> ctxt -> term -> term = fun p ctx a -> let a,k = Ctxt.to_prod ctx a in let m = fresh p a k in - mk_Meta(m, Array.of_list (List.rev_map (fun (x,_,_) -> mk_Vari x) ctx)) + Meta(m, Array.of_list (List.rev_map (fun (x,_,_) -> mk_Vari x) ctx)) (** [make_codomain p ctx a] creates a fresh metavariable term of type [Type] in the context [ctx] extended with a fresh variable of type [a], and updates [p] with generated metavariables. *) let make_codomain : problem -> ctxt -> term -> binder = fun p ctx a -> let x = new_var "x" in - bind_var x (make p ((x, a, None) :: ctx) mk_Type) + bind_var x (make p ((x, a, None) :: ctx) Type) (** [iter b f c t] applies the function [f] to every metavariable of [t] and, if [x] is a variable of [t] mapped to [v] in the context [c], then to every @@ -76,10 +76,10 @@ let iter : bool -> (meta -> unit) -> ctxt -> term -> unit = fun b f c -> | None -> () end | Prod(a,b) - | Abst(a,b) -> iter a; iter (subst b mk_Kind) + | Abst(a,b) -> iter a; iter (subst b Kind) | Appl(t,u) -> iter t; iter u | Meta(m,ts) -> f m; Array.iter iter ts; if b then iter !(m.meta_type) - | LLet(a,t,u) -> iter a; iter t; iter (subst u mk_Kind) + | LLet(a,t,u) -> iter a; iter t; iter (subst u Kind) in iter (** [occurs m c t] tests whether the metavariable [m] occurs in the term [t] diff --git a/src/core/libTerm.ml b/src/core/libTerm.ml index b824e5123..2e437d066 100644 --- a/src/core/libTerm.ml +++ b/src/core/libTerm.ml @@ -7,7 +7,7 @@ open Lplib open Extra let rec is_kind : term -> bool = fun t -> match unfold t with | Type -> true - | Prod(_,b) -> is_kind (subst b mk_Kind) + | Prod(_,b) -> is_kind (subst b Kind) | _ -> false (** [to_var t] returns [x] if [t] is of the form [Vari x] and fails @@ -60,9 +60,9 @@ let iter : (term -> unit) -> term -> unit = fun action -> | Patt(_,_,ts) | Meta(_,ts) -> Array.iter iter ts | Prod(a,b) - | Abst(a,b) -> iter a; iter (subst b mk_Kind) + | Abst(a,b) -> iter a; iter (subst b Kind) | Appl(t,u) -> iter t; iter u - | LLet(a,t,u) -> iter a; iter t; iter (subst u mk_Kind) + | LLet(a,t,u) -> iter a; iter t; iter (subst u Kind) in iter (** [distinct_vars ctx ts] checks that the terms [ts] are distinct @@ -112,7 +112,7 @@ let nl_distinct_vars : term array -> (var array * var StrMap.t) option = let v = new_var f.sym_name in patt_vars := StrMap.add f.sym_name v !patt_vars; v - in to_var (mk_Vari v) + in to_var (Vari v) | _ -> raise Not_a_var in let replace_nl_var v = @@ -132,12 +132,12 @@ let nl_distinct_vars : term array -> (var array * var StrMap.t) option = let sym_to_var : var StrMap.t -> term -> term = fun map -> let rec to_var t = match unfold t with - | Symb f -> (try mk_Vari (StrMap.find f.sym_name map) with Not_found -> t) - | Prod(a,b) -> mk_Prod (to_var a, to_var_binder b) - | Abst(a,b) -> mk_Abst (to_var a, to_var_binder b) - | LLet(a,t,u) -> mk_LLet (to_var a, to_var t, to_var_binder u) - | Appl(a,b) -> mk_Appl(to_var a, to_var b) - | Meta(m,ts) -> mk_Meta(m, Array.map to_var ts) + | Symb f -> (try Vari (StrMap.find f.sym_name map) with Not_found -> t) + | Prod(a,b) -> Prod (to_var a, to_var_binder b) + | Abst(a,b) -> Abst (to_var a, to_var_binder b) + | LLet(a,t,u) -> LLet (to_var a, to_var t, to_var_binder u) + | Appl(a,b) -> Appl(to_var a, to_var b) + | Meta(m,ts) -> Meta(m, Array.map to_var ts) | Patt _ -> assert false | TRef _ -> assert false | _ -> t @@ -150,7 +150,7 @@ let sym_to_var : var StrMap.t -> term -> term = fun map -> let rec codom_binder : int -> term -> binder = fun n t -> match unfold t with | Prod(_,b) -> - if n <= 0 then b else codom_binder (n-1) (subst b mk_Kind) + if n <= 0 then b else codom_binder (n-1) (subst b Kind) | _ -> assert false (** [eq_alpha a b] tests the equality modulo alpha of [a] and [b]. *) @@ -178,17 +178,29 @@ let rec eq_alpha a b = [Bindlib.subst b t ≡ a]. *) let fold (x:var) (t:term): term -> term = let rec aux u = - if eq_alpha t u then mk_Vari x + if eq_alpha t u then Vari x else match unfold u with - | Appl(a,b) -> mk_Appl(aux a, aux b) + | Appl(a,b) -> Appl(aux a, aux b) | Abst(a,b) -> - let x,b = Term.unbind b in mk_Abst(aux a, Term.bind_var x b) + let x,b = Term.unbind b in Abst(aux a, Term.bind_var x b) | Prod(a,b) -> - let x,b = Term.unbind b in mk_Prod(aux a, Term.bind_var x b) + let x,b = Term.unbind b in Prod(aux a, Term.bind_var x b) | LLet(a,d,b) -> - let x,b = Term.unbind b in mk_LLet(aux a, aux d, Term.bind_var x b) - | Meta(m,us) -> mk_Meta(m,Array.map aux us) + let x,b = Term.unbind b in LLet(aux a, aux d, Term.bind_var x b) + | Meta(m,us) -> Meta(m,Array.map aux us) | _ -> u in aux + +(** [contains_ac_sym rs] tells whether the LHS's of [rs] contain an AC + symbol. *) +let contains_ac_sym : rule list -> bool = + let rec aux t = + match get_args t with + | Symb f, ts -> if is_ac f then raise Exit else List.iter aux ts + | Abst(a,b), _ | Prod(a,b), _ -> aux a; let _,b = unbind b in aux b + | _ -> () + in + let aux_rule r = List.iter aux r.lhs in + fun rs -> try List.iter aux_rule rs; false with Exit -> true diff --git a/src/core/print.ml b/src/core/print.ml index e781e34c3..dbba99ea2 100644 --- a/src/core/print.ml +++ b/src/core/print.ml @@ -55,12 +55,12 @@ let uid : string pp = string let path : Path.t pp = Path.pp +let side : side pp = fun ppf s -> + out ppf (match s with Left -> "left" | Right -> "right") + let prop : prop pp = fun ppf p -> match p with - | AC true -> out ppf "left associative commutative " - | AC false -> out ppf "associative commutative " - | Assoc true -> out ppf "left associative " - | Assoc false -> out ppf "associative " + | AC s -> out ppf "%a associative commutative " side s | Const -> out ppf "constant " | Commu -> out ppf "commutative " | Defin -> () diff --git a/src/core/sign.ml b/src/core/sign.ml index 89195dbb9..de06e0416 100644 --- a/src/core/sign.ml +++ b/src/core/sign.ml @@ -80,29 +80,25 @@ let link : t -> unit = fun sign -> try find (Path.Map.find s.sym_path !loaded) s.sym_name with Not_found -> assert false in - let link_term mk_Appl = - let rec link_term t = - match unfold t with - | Type - | Kind - | Vari _ -> t - | Symb s -> mk_Symb(link_symb s) - | Prod(a,b) -> mk_Prod(link_term a, binder link_term b) - | Abst(a,b) -> mk_Abst(link_term a, binder link_term b) - | LLet(a,t,b) -> mk_LLet(link_term a, link_term t, binder link_term b) - | Appl(a,b) -> mk_Appl(link_term a, link_term b) - | Patt(i,n,ts)-> mk_Patt(i, n, Array.map link_term ts) - | Bvar _ -> assert false - | Meta _ -> assert false - | Plac _ -> assert false - | Wild -> assert false - | TRef _ -> assert false - in link_term + let rec link_term t = + match unfold t with + | Type + | Kind + | Vari _ -> t + | Symb s -> Symb(link_symb s) + | Prod(a,b) -> Prod(link_term a, binder link_term b) + | Abst(a,b) -> Abst(link_term a, binder link_term b) + | LLet(a,t,b) -> LLet(link_term a, link_term t, binder link_term b) + | Appl(a,b) -> Appl(link_term a, link_term b) + | Patt(i,n,ts)-> Patt(i, n, Array.map link_term ts) + | Bvar _ -> assert false + | Meta _ -> assert false + | Plac _ -> assert false + | Wild -> assert false + | TRef _ -> assert false in - let link_lhs = link_term mk_Appl_not_canonical - and link_term = link_term mk_Appl in let link_rule r = - let lhs = List.map link_lhs r.lhs in + let lhs = List.map link_term r.lhs in let rhs = link_term r.rhs in {r with lhs ; rhs} in @@ -135,7 +131,7 @@ let link : t -> unit = fun sign -> let f s i m = SymMap.add (link_symb s) (link_ind_data i) m in sign.sign_ind := SymMap.fold f !(sign.sign_ind) SymMap.empty; let link_cp_pos (pos,l,r,p,l_p) = - pos, link_lhs l, link_term r, p, link_lhs l_p in + pos, link_term l, link_term r, p, link_term l_p in let f s cps m = SymMap.add (link_symb s) (List.map link_cp_pos cps) m in sign.sign_cp_pos := SymMap.fold f !(sign.sign_cp_pos) SymMap.empty @@ -150,7 +146,7 @@ let unlink : t -> unit = fun sign -> let unlink_sym s = s.sym_dtree := Tree_type.empty_dtree; if s.sym_path <> sign.sign_path then - (s.sym_type := mk_Kind; s.sym_rules := []) + (s.sym_type := Kind; s.sym_rules := []) in let rec unlink_term t = match unfold t with @@ -305,14 +301,18 @@ let read = pairs. *) let add_rule : t -> sym_rule -> unit = fun sign (sym,r) -> sym.sym_rules := !(sym.sym_rules) @ [r]; - if sym.sym_path <> sign.sign_path then - let sm = Path.Map.find sym.sym_path !(sign.sign_deps) in - let f = function - | None -> Some([r],None) - | Some(rs,n) -> Some(rs@[r],n) - in - let sm = StrMap.update sym.sym_name f sm in - sign.sign_deps := Path.Map.add sym.sym_path sm !(sign.sign_deps) + if Timed.(!(sym.sym_rstrat)) <> Innermost && LibTerm.contains_ac_sym [r] + then Timed.(sym.sym_rstrat := Innermost); + if sym.sym_path <> sign.sign_path then (* update dependencies *) + begin + let sm = Path.Map.find sym.sym_path !(sign.sign_deps) in + let f = function + | None -> Some([r],None) + | Some(rs,n) -> Some(rs@[r],n) + in + let sm = StrMap.update sym.sym_name f sm in + sign.sign_deps := Path.Map.add sym.sym_path sm !(sign.sign_deps) + end (** [add_rules sign sym rs] adds the new rules [rs] to the symbol [sym]. When the rules do not correspond to a symbol of signature [sign], they are @@ -320,14 +320,18 @@ let add_rule : t -> sym_rule -> unit = fun sign (sym,r) -> critical pairs. *) let add_rules : t -> sym -> rule list -> unit = fun sign sym rs -> sym.sym_rules := !(sym.sym_rules) @ rs; - if sym.sym_path <> sign.sign_path then - let sm = Path.Map.find sym.sym_path !(sign.sign_deps) in - let f = function - | None -> Some(rs,None) - | Some(rs',n) -> Some(rs'@rs,n) - in - let sm = StrMap.update sym.sym_name f sm in - sign.sign_deps := Path.Map.add sym.sym_path sm !(sign.sign_deps) + if Timed.(!(sym.sym_rstrat)) <> Innermost && LibTerm.contains_ac_sym rs + then Timed.(sym.sym_rstrat := Innermost); + if sym.sym_path <> sign.sign_path then (* update dependencies *) + begin + let sm = Path.Map.find sym.sym_path !(sign.sign_deps) in + let f = function + | None -> Some(rs,None) + | Some(rs',n) -> Some(rs'@rs,n) + in + let sm = StrMap.update sym.sym_name f sm in + sign.sign_deps := Path.Map.add sym.sym_path sm !(sign.sign_deps); + end (** [add_notation sign sym nota] changes the notation of [sym] to [nota] in the signature [sign]. *) diff --git a/src/core/term.ml b/src/core/term.ml index fa99a1cec..6f7242109 100644 --- a/src/core/term.ml +++ b/src/core/term.ml @@ -23,20 +23,30 @@ type match_strat = (** Any rule that filters a term can be applied (even if a rule defined earlier filters the term as well). This is the default. *) +(** Reduction strategy. *) +type red_strat = + | Innermost + (** Arguments are normalized before trying to apply a rewrite rule. Strategy + used for symbols with rules matching on AC symbols. *) + | Outermost + (** Arguments are reduced when trying to apply a rewrite rule. This is the + default. *) + (** Specify the visibility and usability of symbols outside their module. *) type expo = | Public (** Visible and usable everywhere. *) | Protec (** Visible everywhere but usable in LHS arguments only. *) | Privat (** Not visible and thus not usable. *) +type side = Left | Right + (** Symbol properties. *) type prop = | Defin (** Definable. *) | Const (** Constant. *) | Injec (** Injective. *) | Commu (** Commutative. *) - | Assoc of bool (** Associative left if [true], right if [false]. *) - | AC of bool (** Associative and commutative. *) + | AC of side (** Associative and commutative. *) (** Data of a binder. *) type binder_info = {binder_name : string; binder_bound : bool} @@ -176,6 +186,7 @@ and sym = ; sym_opaq : bool Timed.ref (** Opacity. *) ; sym_rules : rule list Timed.ref (** Rewriting rules. *) ; sym_mstrat: match_strat (** Matching strategy. *) + ; sym_rstrat: red_strat Timed.ref (** Reduction strategy. *) ; sym_dtree : dtree Timed.ref (** Decision tree used for matching. *) ; sym_pos : Pos.popt (** Position in source file of symbol name. *) ; sym_decl_pos : Pos.popt (** Position in source file of symbol declaration @@ -290,7 +301,7 @@ let create_sym : Path.t -> expo -> prop -> match_strat -> bool -> let open Timed in {sym_path; sym_name; sym_type = ref typ; sym_impl; sym_def = ref None; sym_opaq = ref sym_opaq; sym_rules = ref []; sym_not = ref NoNotation; - sym_dtree = ref Tree_type.empty_dtree; + sym_dtree = ref Tree_type.empty_dtree; sym_rstrat = ref Outermost; sym_mstrat; sym_prop; sym_expo; sym_pos ; sym_decl_pos } (** [is_constant s] tells whether [s] is a constant. *) @@ -306,7 +317,9 @@ let is_private : sym -> bool = fun s -> s.sym_expo = Privat (** [is_modulo s] tells whether the symbol [s] is modulo some equations. *) let is_modulo : sym -> bool = fun s -> - match s.sym_prop with Assoc _ | Commu | AC _ -> true | _ -> false + match s.sym_prop with Commu | AC _ -> true | _ -> false +let is_ac : sym -> bool = fun s -> + match s.sym_prop with AC _ -> true | _ -> false (** Sets and maps of symbols. *) module Sym = struct @@ -333,20 +346,16 @@ end module MetaSet = Set.Make(Meta) module MetaMap = Map.Make(Meta) -(** Dealing with AC-normalization of terms *) -let mk_bin s t1 t2 = Appl(Appl(Symb s, t1), t2) - -(** [mk_left_comb s t ts] builds a left comb of applications of [s] from - [t::ts] so that [mk_left_comb s t1 [t2; t3] = mk_bin s (mk_bin s t1 t2) - t3]. *) -let mk_left_comb : sym -> term -> term list -> term = fun s -> - List.fold_left (mk_bin s) +(** [add_args t args] builds the application of the {!type:term} [t] to a list + arguments [args]. When [args] is empty, the returned value is (physically) + equal to [t]. *) +let add_args : term -> term list -> term = + List.fold_left (fun t u -> Appl(t,u)) -(** [mk_right_comb s ts t] builds a right comb of applications of [s] to - [ts@[t]] so that [mk_right_comb s [t1; t2] t3 = mk_bin s t1 (mk_bin s t2 - t3)]. *) -let mk_right_comb : sym -> term list -> term -> term = fun s -> - List.fold_right (mk_bin s) +(** [add_args_map f t xs] is equivalent to [add_args t (List.map f xs)] but + more efficient. *) +let add_args_map : term -> ('a -> term) -> 'a list -> term = fun t f xs -> + List.fold_left (fun t x -> Appl(t, f x)) t xs (** Printing functions for debug. *) let rec term : term pp = fun ppf t -> @@ -384,17 +393,16 @@ and clos_env : term array pp = fun ppf env -> D.array term ppf env performed. {b NOTE} that {!val:unfold} must (almost) always be called before matching over a value of type {!type:term}. *) and unfold : term -> term = fun t -> - let open Timed in match t with | Meta(m, ts) -> begin - match !(m.meta_value) with + match Timed.(!(m.meta_value)) with | None -> t | Some(b) -> unfold (msubst b ts) end | TRef(r) -> begin - match !r with + match Timed.(!r) with | None -> t | Some(v) -> unfold v end @@ -407,12 +415,12 @@ and msubst : mbinder -> term array -> term = fun (bi,tm,env) vs -> let n = Array.length bi.mbinder_name in assert (Array.length vs = n); let rec msubst t = -(* if Logger.log_enabled() then + (*if Logger.log_enabled() then log "msubst %a %a" (D.array term) vs term t;*) match unfold t with | Bvar (InSub p) -> assert bi.mbinder_bound.(p); vs.(p) | Bvar (InEnv p) -> env.(p) - | Appl(a,b) -> mk_Appl(msubst a, msubst b) + | Appl(a,b) -> Appl(msubst a, msubst b) (* No need to substitute in the closure term: all bound variables appear in the closure environment *) | Abst(a,(n,u,e)) -> Abst(msubst a, (n, u, Array.map msubst e)) @@ -427,12 +435,32 @@ and msubst : mbinder -> term array -> term = fun (bi,tm,env) vs -> if Array.for_all ((=) false) bi.mbinder_bound && Array.length env = 0 then tm else msubst tm in - if Logger.log_enabled() then - log "msubst %a#%a %a = %a" clos_env env term tm (D.array term) vs term r; + (*if Logger.log_enabled() then + log "msubst %a#%a %a = %a" clos_env env term tm (D.array term) vs term r;*) r +(** [get_args t] decomposes the {!type:term} [t] into a pair [(h,args)], where + [h] is the head term of [t] and [args] is the list of arguments applied to + [h] in [t]. The returned [h] cannot be an [Appl] node. *) +let get_args : term -> term * term list = fun t -> + let rec get_args t acc = + match unfold t with + | Appl(t,u) -> get_args t (u::acc) + | t -> t, acc + in get_args t [] + +(** [get_args_len t] is similar to [get_args t] but it also returns the length + of the list of arguments. *) +let get_args_len : term -> term * term list * int = fun t -> + let rec get_args_len acc len t = + match unfold t with + | Appl(t, u) -> get_args_len (u::acc) (len + 1) t + | t -> (t, acc, len) + in + get_args_len [] 0 t + (** Total order on terms. *) -and cmp : term cmp = fun t t' -> +let rec cmp : term cmp = fun t t' -> match unfold t, unfold t' with | Vari x, Vari x' -> compare_vars x x' | Type, Type @@ -441,16 +469,14 @@ and cmp : term cmp = fun t t' -> | Symb s, Symb s' -> Sym.compare s s' | Prod(t,u), Prod(t',u') | Abst(t,u), Abst(t',u') -> lex cmp cmp_binder (t,u) (t',u') - | Appl(t,u), Appl(t',u') -> lex cmp cmp (u,t) (u',t') + | Appl(t,u), Appl(t',u') -> lex cmp cmp (t,u) (t',u') | Meta(m,ts), Meta(m',ts') -> - lex Meta.compare (Array.cmp cmp) (m,ts) (m',ts') + lex Meta.compare (Array.cmp cmp) (m,ts) (m',ts') | Patt(i,s,ts), Patt(i',s',ts') -> - lex3 Stdlib.compare Stdlib.compare (Array.cmp cmp) - (i,s,ts) (i',s',ts') + lex3 Stdlib.compare Stdlib.compare (Array.cmp cmp) (i,s,ts) (i',s',ts') | Bvar i, Bvar j -> Stdlib.compare i j | TRef r, TRef r' -> Stdlib.compare r r' - | LLet(a,t,u), LLet(a',t',u') -> - lex3 cmp cmp cmp_binder (a,t,u) (a',t',u') + | LLet(a,t,u), LLet(a',t',u') -> lex3 cmp cmp cmp_binder (a,t,u) (a',t',u') | t, t' -> cmp_tag t t' and cmp_binder : binder cmp = @@ -459,119 +485,12 @@ and cmp_binder : binder cmp = let var = Vari(new_var binder_name) in cmp (msubst (mbi,u,e)[|var|]) (msubst({mbi with mbinder_bound=[|bi'.binder_bound|]},u',e')[|var|])*) - fun (_,u,e) (_,u',e') -> - lex cmp (Array.cmp cmp) (u,e) (u',e') - -(** [get_args t] decomposes the {!type:term} [t] into a pair [(h,args)], where - [h] is the head term of [t] and [args] is the list of arguments applied to - [h] in [t]. The returned [h] cannot be an [Appl] node. *) -and get_args : term -> term * term list = fun t -> - let rec get_args t acc = - match unfold t with - | Appl(t,u) -> get_args t (u::acc) - | t -> t, acc - in get_args t [] - -(** [get_args_len t] is similar to [get_args t] but it also returns the length - of the list of arguments. *) -and get_args_len : term -> term * term list * int = fun t -> - let rec get_args_len acc len t = - match unfold t with - | Appl(t, u) -> get_args_len (u::acc) (len + 1) t - | t -> (t, acc, len) - in - get_args_len [] 0 t + fun (_,u,e) (_,u',e') -> lex cmp (Array.cmp cmp) (u,e) (u',e') (** [is_symb s t] tests whether [t] is of the form [Symb(s)]. *) -and is_symb : sym -> term -> bool = fun s t -> +let is_symb : sym -> term -> bool = fun s t -> match unfold t with Symb(r) -> r == s | _ -> false -(* We make the equality of terms modulo commutative and - associative-commutative symbols syntactic by always ordering arguments in - increasing order and by putting them in a comb form. - - The term [t1 + t2 + t3] is represented by the left comb [(t1 + t2) + t3] if - + is left associative and [t1 + (t2 + t3)] if + is right associative. *) - -(** [left_aliens s t] returns the list of the biggest subterms of [t] not - headed by [s], assuming that [s] is left associative and [t] is in - canonical form. This is the reverse of [mk_left_comb]. *) -and left_aliens : sym -> term -> term list = fun s -> - let rec aliens acc = function - | [] -> acc - | u::us -> - let h, ts = get_args u in - if is_symb s h then - match ts with - | t1 :: t2 :: _ -> aliens (t2 :: acc) (t1 :: us) - | _ -> aliens (u :: acc) us - else aliens (u :: acc) us - in fun t -> aliens [] [t] - -(** [right_aliens s t] returns the list of the biggest subterms of [t] not - headed by [s], assuming that [s] is right associative and [t] is in - canonical form. This is the reverse of [mk_right_comb]. *) -and right_aliens : sym -> term -> term list = fun s -> - let rec aliens acc = function - | [] -> acc - | u::us -> - let h, ts = get_args u in - if is_symb s h then - match ts with - | t1 :: t2 :: _ -> aliens (t1 :: acc) (t2 :: us) - | _ -> aliens (u :: acc) us - else aliens (u :: acc) us - in fun t -> let r = aliens [] [t] in - if Logger.log_enabled () then - log "right_aliens %a %a = %a" sym s term t (D.list term) r; - r - -(** [mk_Appl t u] puts the application of [t] to [u] in canonical form wrt C - or AC symbols. *) -and mk_Appl : term * term -> term = fun (t, u) -> - (* if Logger.log_enabled () then - log "mk_Appl(%a, %a)" term t term u; - let r = *) - match get_args t with - | Symb s, [t1] -> - begin - match s.sym_prop with - | Commu when cmp t1 u > 0 -> mk_bin s u t1 - | AC true -> (* left associative symbol *) - let ts = left_aliens s t1 and us = left_aliens s u in - begin - match List.sort cmp (ts @ us) with - | v::vs -> mk_left_comb s v vs - | _ -> assert false - end - | AC false -> (* right associative symbol *) - let ts = right_aliens s t1 and us = right_aliens s u in - let vs, v = List.split_last (List.sort cmp (ts @ us)) - in mk_right_comb s vs v - | _ -> Appl (t, u) - end - | _ -> Appl (t, u) - (* in - if Logger.log_enabled () then - log "mk_Appl(%a, %a) = %a" term t term u term r; - r *) - -(* unit test *) -let _ = - let s = - create_sym [] Privat (AC true) Eager false (Pos.none "+") None Kind [] in - let t1 = Vari (new_var "x1") in - let t2 = Vari (new_var "x2") in - let t3 = Vari (new_var "x3") in - let left = mk_bin s (mk_bin s t1 t2) t3 in - let right = mk_bin s t1 (mk_bin s t2 t3) in - let eq = eq_of_cmp cmp in - assert (eq (mk_left_comb s t1 [t2; t3]) left); - assert (eq (mk_right_comb s [t1; t2] t3) right); - let eq = eq_of_cmp (List.cmp cmp) in - assert (eq (left_aliens s left) [t1; t2; t3]); - assert (eq (right_aliens s right) [t3; t2; t1]) - (** [is_abst t] returns [true] iff [t] is of the form [Abst(_)]. *) let is_abst : term -> bool = fun t -> match unfold t with Abst(_) -> true | _ -> false @@ -670,7 +589,7 @@ let subst : binder -> term -> term = fun (bi,tm,env) v -> match unfold t with | Bvar (InSub _) -> assert bi.binder_bound; v | Bvar (InEnv p) -> env.(p) - | Appl(a,b) -> mk_Appl(subst a, subst b) + | Appl(a,b) -> Appl(subst a, subst b) | Abst(a,(n,u,e)) -> Abst(subst a, (n, u, Array.map subst e)) | Prod(a,(n,u,e)) -> Prod(subst a, (n ,u, Array.map subst e)) | LLet(a,t,(n,u,e)) -> LLet(subst a, subst t, (n, u, Array.map subst e)) @@ -720,7 +639,7 @@ let bind_var : var -> term -> binder = fun ((_,n) as x) t -> let a' = bind i a in let b' = bind i b in if a==a' && b==b' then t else Appl(a', b') - (* No need to call mk_Appl here as we only replace free variables by de + (* No need to call Appl here as we only replace free variables by de Bruijn indices. *) | Abst(a,b) -> let a' = bind i a in @@ -759,6 +678,14 @@ let bind_var : var -> term -> binder = fun ((_,n) as x) t -> log "bind_var %a %a = %a" var x term t term b; {binder_name=n; binder_bound= !bound}, b, [||] +(** Build a non-dependent product. *) +let mk_Arro (a,b) = let x = new_var "_" in Prod(a, bind_var x b) + +(** Curryfied versions of some constructors. *) +let mk_Vari v = Vari v +let mk_Abst (a,b) = Abst (a,b) +let mk_Prod (a,b) = Prod (a,b) + (** [binder f b] applies f inside [b]. *) let binder : (term -> term) -> binder -> binder = fun f b -> let x,t = unbind b in bind_var x (f t) @@ -788,7 +715,7 @@ let bind_mvar : var array -> term -> mbinder = let a' = bind fvar a in let b' = bind fvar b in if a==a' && b==b' then t else Appl(a', b') - (* No need to call mk_Appl here as we only replace free variables by de + (* No need to call Appl here as we only replace free variables by de Bruijn indices. *) | Abst(a,b) -> let a' = bind fvar a in @@ -839,52 +766,6 @@ let bind_mvar : var array -> term -> mbinder = bi, b, [||] end -(** Construction functions of the private type [term]. They ensure some - invariants: - -- In a commutative function symbol application, the first argument is smaller - than the second one wrt [cmp]. - -- In an associative and commutative function symbol application, the - application is built as a left or right comb depending on the associativity - of the symbol, and arguments are ordered in increasing order wrt [cmp]. - -- In [LLet(_,_,b)], [binder_occur b = true] (useless let's are erased). *) -let mk_Vari x = Vari x -let mk_Type = Type -let mk_Kind = Kind -let mk_Symb x = Symb x -let mk_Prod (a,b) = Prod (a,b) -let mk_Arro (a,b) = let x = new_var "_" in Prod(a, bind_var x b) -let mk_Abst (a,b) = Abst (a,b) -let mk_Meta (m,ts) = (*assert (m.meta_arity = Array.length ts);*) Meta (m,ts) -let mk_Patt (i,s,ts) = Patt (i,s,ts) -let mk_Wild = Wild -let mk_Plac b = Plac b -let mk_TRef x = TRef x -let mk_LLet (a,t,b) = LLet (a,t,b) - -(** [mk_Appl_not_canonical t u] builds the non-canonical (wrt. C and AC - symbols) application of [t] to [u]. WARNING: to use only in Sign.link. *) -let mk_Appl_not_canonical : term * term -> term = fun (t, u) -> Appl(t, u) - -(** [add_args t args] builds the application of the {!type:term} [t] to a list - arguments [args]. When [args] is empty, the returned value is (physically) - equal to [t]. *) -let add_args : term -> term list -> term = fun t ts -> - match get_args t with - | Symb s, _ when is_modulo s -> - List.fold_left (fun t u -> mk_Appl(t,u)) t ts - | _ -> List.fold_left (fun t u -> Appl(t,u)) t ts - -(** [add_args_map f t ts] is equivalent to [add_args t (List.map f ts)] but - more efficient. *) -let add_args_map : term -> (term -> term) -> term list -> term = fun t f ts -> - match get_args t with - | Symb s, _ when is_modulo s -> - List.fold_left (fun t u -> mk_Appl(t, f u)) t ts - | _ -> List.fold_left (fun t u -> Appl(t, f u)) t ts - (** Patt substitution. *) let subst_patt : mbinder option array -> term -> term = fun env -> let rec subst_patt t = @@ -892,17 +773,17 @@ let subst_patt : mbinder option array -> term -> term = fun env -> | Patt(Some i,n,ts) when 0 <= i && i < Array.length env -> begin match env.(i) with | Some b -> msubst b (Array.map subst_patt ts) - | None -> mk_Patt(Some i,n,Array.map subst_patt ts) + | None -> Patt(Some i,n,Array.map subst_patt ts) end - | Patt(i,n,ts) -> mk_Patt(i, n, Array.map subst_patt ts) + | Patt(i,n,ts) -> Patt(i, n, Array.map subst_patt ts) | Prod(a,(n,b,e)) -> - mk_Prod(subst_patt a, (n, subst_patt b, Array.map subst_patt e)) + Prod(subst_patt a, (n, subst_patt b, Array.map subst_patt e)) | Abst(a,(n,b,e)) -> - mk_Abst(subst_patt a, (n, subst_patt b, Array.map subst_patt e)) - | Appl(a,b) -> mk_Appl(subst_patt a, subst_patt b) - | Meta(m,ts) -> mk_Meta(m, Array.map subst_patt ts) + Abst(subst_patt a, (n, subst_patt b, Array.map subst_patt e)) + | Appl(a,b) -> Appl(subst_patt a, subst_patt b) + | Meta(m,ts) -> Meta(m, Array.map subst_patt ts) | LLet(a,t,(n,b,e)) -> - mk_LLet(subst_patt a, subst_patt t, + LLet(subst_patt a, subst_patt t, (n, subst_patt b, Array.map subst_patt e)) | Wild | Plac _ @@ -917,12 +798,12 @@ let subst_patt : mbinder option array -> term -> term = fun env -> (** [cleanup t] unfold all metas and TRef's in [t]. *) let rec cleanup : term -> term = fun t -> match unfold t with - | Patt(i,n,ts) -> mk_Patt(i, n, Array.map cleanup ts) - | Prod(a,b) -> mk_Prod(cleanup a, binder cleanup b) - | Abst(a,b) -> mk_Abst(cleanup a, binder cleanup b) - | Appl(a,b) -> mk_Appl(cleanup a, cleanup b) - | Meta(m,ts) -> mk_Meta(m, Array.map cleanup ts) - | LLet(a,t,b) -> mk_LLet(cleanup a, cleanup t, binder cleanup b) + | Patt(i,n,ts) -> Patt(i, n, Array.map cleanup ts) + | Prod(a,b) -> Prod(cleanup a, binder cleanup b) + | Abst(a,b) -> Abst(cleanup a, binder cleanup b) + | Appl(a,b) -> Appl(cleanup a, cleanup b) + | Meta(m,ts) -> Meta(m, Array.map cleanup ts) + | LLet(a,t,b) -> LLet(cleanup a, cleanup t, binder cleanup b) | Wild -> assert false | Plac _ -> assert false | TRef _ -> assert false @@ -935,7 +816,7 @@ let rec cleanup : term -> term = fun t -> (** Type of a symbol and a rule. *) type sym_rule = sym * rule -let lhs : sym_rule -> term = fun (s, r) -> add_args (mk_Symb s) r.lhs +let lhs : sym_rule -> term = fun (s, r) -> add_args (Symb s) r.lhs let rhs : sym_rule -> term = fun (_, r) -> r.rhs (** Positions in terms in reverse order. The i-th argument of a constructor diff --git a/src/core/term.mli b/src/core/term.mli index b265791d2..8142cb427 100644 --- a/src/core/term.mli +++ b/src/core/term.mli @@ -3,7 +3,6 @@ This module contains the definition of the internal representation of terms, together with smart constructors and low level operation. *) -open Timed open Lplib open Base open Common @@ -21,20 +20,30 @@ type match_strat = (** Any rule that filters a term can be applied (even if a rule defined earlier filters the term as well). This is the default. *) +(** Reduction strategy. *) +type red_strat = + | Innermost + (** Arguments are normalized before trying to apply a rewrite rule. Strategy + used for symbols with rules matching on AC symbols. *) + | Outermost + (** Arguments are reduced when trying to apply a rewrite rule. This is the + default. *) + (** Specify the visibility and usability of symbols outside their module. *) type expo = | Public (** Visible and usable everywhere. *) | Protec (** Visible everywhere but usable in LHS arguments only. *) | Privat (** Not visible and thus not usable. *) +type side = Left | Right + (** Symbol properties. *) type prop = | Defin (** Definable. *) | Const (** Constant. *) | Injec (** Injective. *) | Commu (** Commutative. *) - | Assoc of bool (** Associative left if [true], right if [false]. *) - | AC of bool (** Associative and commutative. *) + | AC of side (** Associative and commutative. *) (** Type for free variables. *) type var @@ -69,7 +78,7 @@ type 'a notation = are also used, for example, in the representation of patterns or rewriting rules. Specific constructors are included for such applications, and they are considered invalid in unrelated code. *) -type term = private +type term = | Vari of var (** Free variable. *) | Bvar of bvar (** Bound variables. Only used internally. *) | Type (** "TYPE" constant. *) @@ -85,7 +94,8 @@ type term = private | Plac of bool (** [Plac b] is a placeholder, or hole, for not given terms. Boolean [b] is true if the placeholder stands for a type. *) - | TRef of term option ref (** Reference cell (used in surface matching). *) + | TRef of term option Timed.ref + (** Reference cell (used in surface matching). *) | LLet of term * term * binder (** [LLet(a, t, u)] is [let x : a ≔ t in u] (with [x] bound in [u]). *) @@ -104,15 +114,16 @@ and sym = { sym_expo : expo (** Visibility. *) ; sym_path : Path.t (** Module in which the symbol is defined. *) ; sym_name : string (** Name. *) - ; sym_type : term ref (** Type. *) + ; sym_type : term Timed.ref (** Type. *) ; sym_impl : bool list (** Implicit arguments ([true] meaning implicit). *) ; sym_prop : prop (** Property. *) - ; sym_not : float notation ref (** Notation. *) - ; sym_def : term option ref (** Definition with ≔. *) - ; sym_opaq : bool ref (** Opacity. *) - ; sym_rules : rule list ref (** Rewriting rules. *) + ; sym_not : float notation Timed.ref (** Notation. *) + ; sym_def : term option Timed.ref (** Definition with ≔. *) + ; sym_opaq : bool Timed.ref (** Opacity. *) + ; sym_rules : rule list Timed.ref (** Rewriting rules. *) ; sym_mstrat: match_strat (** Matching strategy. *) - ; sym_dtree : dtree ref (** Decision tree used for matching. *) + ; sym_rstrat: red_strat Timed.ref (** Reduction strategy. *) + ; sym_dtree : dtree Timed.ref (** Decision tree used for matching. *) ; sym_pos : Pos.popt (** Position in source file of symbol name. *) ; sym_decl_pos : Pos.popt (** Position in source file of symbol declaration without its definition. *) } @@ -220,9 +231,9 @@ and rule = the form {!constructor:Meta}[(m,env)] can be unfolded. *) and meta = { meta_key : int (** Unique key. *) - ; meta_type : term ref (** Type. *) + ; meta_type : term Timed.ref (** Type. *) ; meta_arity : int (** Arity (environment size). *) - ; meta_value : mbinder option ref (** Definition. *) } + ; meta_value : mbinder option Timed.ref (** Definition. *) } (** [binder_name b] gives the name of the bound variable of [b]. *) val binder_name : binder -> string @@ -256,6 +267,7 @@ val is_private : sym -> bool (** [is_modulo s] tells whether the symbol [s] is modulo some equations. *) val is_modulo : sym -> bool +val is_ac : sym -> bool (** Sets and maps of symbols. *) module Sym : Map.OrderedType with type t = sym @@ -327,44 +339,22 @@ val get_args_len : term -> term * term list * int (** Total orders terms. *) val cmp : term cmp -(** Construction functions of the private type [term]. They ensure some - invariants: - -- In a commutative function symbol application, the first argument is smaller - than the second one wrt [cmp]. - -- In an associative and commutative function symbol application, the - application is built as a left or right comb depending on the associativity - of the symbol, and arguments are ordered in increasing order wrt [cmp]. +(** Build a non-dependent product. *) +val mk_Arro : term * term -> term -- In [LLet(_,_,b)], [binder_occur b = true] (useless let's are erased). *) +(** Curryfied versions of some constructors. *) val mk_Vari : var -> term -val mk_Type : term -val mk_Kind : term -val mk_Symb : sym -> term -val mk_Prod : term * binder -> term -val mk_Arro : term * term -> term val mk_Abst : term * binder -> term -val mk_Appl : term * term -> term -val mk_Meta : meta * term array -> term -val mk_Patt : int option * string * term array -> term -val mk_Wild : term -val mk_Plac : bool -> term -val mk_TRef : term option ref -> term -val mk_LLet : term * term * binder -> term - -(** [mk_Appl_not_canonical t u] builds the non-canonical (wrt. C and AC - symbols) application of [t] to [u]. WARNING: to use only in Sign.link. *) -val mk_Appl_not_canonical : term * term -> term +val mk_Prod : term * binder -> term (** [add_args t args] builds the application of the {!type:term} [t] to a list arguments [args]. When [args] is empty, the returned value is (physically) equal to [t]. *) val add_args : term -> term list -> term -(** [add_args_map f t ts] is equivalent to [add_args t (List.map f ts)] but +(** [add_args_map f t xs] is equivalent to [add_args t (List.map f xs)] but more efficient. *) -val add_args_map : term -> (term -> term) -> term list -> term +val add_args_map : term -> ('a -> term) -> 'a list -> term (** [subst b v] substitutes the variable bound by [b] with the value [v]. *) val subst : binder -> term -> term @@ -388,13 +378,13 @@ val unbind2 : ?name:string -> binder -> binder -> var * term * term create the fresh variables are based on those of the multiple binder. *) val unmbind : mbinder -> var array * term -(** [bind_var x b] binds the variable [x] in [b], producing a boxed binder. *) +(** [bind_var x b] binds the variable [x] in [b], producing a binder. *) val bind_var : var -> term -> binder (** [binder f b] applies f inside [b]. *) val binder : (term -> term) -> binder -> binder -(** [bind_mvar xs b] binds the variables of [xs] in [b] to get a boxed binder. +(** [bind_mvar xs b] binds the variables of [xs] in [b] to get a binder. It is the equivalent of [bind_var] for multiple variables. *) val bind_mvar : var array -> term -> mbinder @@ -406,7 +396,7 @@ val mbinder_occur : mbinder -> int -> bool val is_closed : term -> bool val is_closed_mbinder : mbinder -> bool -(** [occur x b] tells whether variable [x] occurs in the [box] [b]. *) +(** [occur x b] tells whether variable [x] occurs in [b]. *) val occur : var -> term -> bool val occur_mbinder : var -> mbinder -> bool @@ -436,7 +426,7 @@ type problem_aux = ; metas : MetaSet.t (** Set of unsolved metas. *) } -type problem = problem_aux ref +type problem = problem_aux Timed.ref (** Create a new empty problem. *) val new_problem : unit -> problem diff --git a/src/core/tree.ml b/src/core/tree.ml index 16b93962d..483ad93cd 100644 --- a/src/core/tree.ml +++ b/src/core/tree.ml @@ -451,13 +451,13 @@ module CM = struct let index_var : int VarMap.t -> term -> int = fun vi t -> VarMap.find (to_var t) vi - (** [mk_wildcard vs] creates a pattern variable that accepts anything and in + (** [wildcard vs] creates a pattern variable that accepts anything and in which variables [vs] can appear free. There is no order on [vs] because such created wildcard are not bound anywhere, so terms filtered by such wildcards are not kept. *) - let mk_wildcard : VarSet.t -> term = fun vs -> + let wildcard : VarSet.t -> term = fun vs -> let env = vs |> VarSet.to_seq |> Seq.map mk_Vari |> Array.of_seq in - mk_Patt (None, "", env) + Patt (None, "", env) (** [update_aux col mem clause] the condition pool and the substitution of clause [clause] assuming that column [col] is inspected and [mem] @@ -541,7 +541,7 @@ module CM = struct else None | _ , Patt(_) -> let arity = List.length pargs in - let e = Array.make arity (mk_wildcard free_vars) in + let e = Array.make arity (wildcard free_vars) in Some({ r with c_lhs = insert e }) | Symb(_), Vari(_) | Vari(_), Symb(_) @@ -600,15 +600,15 @@ module CM = struct let ph, pargs = get_args r.c_lhs.(col) in match ph with | Patt(_) -> - let domain = mk_wildcard free_vars in - let body = mk_wildcard (VarSet.add v free_vars) in + let domain = wildcard free_vars in + let body = wildcard (VarSet.add v free_vars) in Some{r with c_lhs = insert r [|domain; body|]} | Symb(_) | Vari(_) -> None | t -> let (a, b) = get t in assert (pargs = []) ; (* Patterns in β-normal form *) - let b = subst b (mk_Vari v) in + let b = subst b (Vari v) in Some({r with c_lhs = insert r [|a; b|]}) in diff --git a/src/core/unif.ml b/src/core/unif.ml index bbdda0f98..c06fde440 100644 --- a/src/core/unif.ml +++ b/src/core/unif.ml @@ -23,17 +23,17 @@ let set_to_prod : problem -> meta -> unit = fun p m -> let vs = Env.vars env in let xs = Array.map mk_Vari vs in (* domain *) - let u1 = Env.to_prod env mk_Type in + let u1 = Env.to_prod env Type in let m1 = LibMeta.fresh p u1 n in - let a = mk_Meta (m1, xs) in + let a = Meta (m1, xs) in (* codomain *) let y = new_var "y" in - let env' = Env.add "y" y (mk_Meta (m1, xs)) None env in + let env' = Env.add "y" y (Meta (m1, xs)) None env in let u2 = Env.to_prod env' s in let m2 = LibMeta.fresh p u2 (n+1) in - let b = bind_var y (mk_Meta (m2, Array.append xs [|mk_Vari y|])) in + let b = bind_var y (Meta (m2, Array.append xs [|Vari y|])) in (* result *) - let r = mk_Prod (a, b) in + let r = Prod (a, b) in if Logger.log_enabled () then log (red "%a ≔ %a") meta m term r; LibMeta.set p m (bind_mvar vs r) @@ -65,10 +65,10 @@ let try_unif_rules : problem -> ctxt -> term -> term -> bool = let open Unif_rule in try let rhs = - let start = add_args (mk_Symb equiv) [s;t] in + let start = add_args (Symb equiv) [s;t] in let reduced = Eval.whnf c start in if reduced != start then reduced else - let start = add_args (mk_Symb equiv) [t;s] in + let start = add_args (Symb equiv) [t;s] in let reduced = Eval.whnf c start in if reduced != start then reduced else raise No_match in @@ -195,12 +195,12 @@ let imitate_inj : -> bool = fun p c m vs us s ts -> if Logger.log_enabled () then - log "imitate_inj %a ≡ %a" term (add_args (mk_Meta(m,vs)) us) - term (add_args (mk_Symb s) ts); + log "imitate_inj %a ≡ %a" term (add_args (Meta(m,vs)) us) + term (add_args (Symb s) ts); let exception Cannot_imitate in try if us <> [] || not (is_injective s) - || LibMeta.occurs m c (add_args (mk_Symb s) ts) then + || LibMeta.occurs m c (add_args (Symb s) ts) then raise Cannot_imitate; let vars = match distinct_vars c vs with @@ -216,11 +216,11 @@ let imitate_inj : let k = Array.length vars in let t = let rec build i acc t = - if i <= 0 then add_args (mk_Symb s) (List.rev acc) else + if i <= 0 then add_args (Symb s) (List.rev acc) else match unfold t with | Prod(a,b) -> let m = LibMeta.fresh p (Env.to_prod env a) k in - let u = mk_Meta (m,vs) in + let u = Meta (m,vs) in build (i-1) (u::acc) (subst b u) | _ -> raise Cannot_imitate in build (List.length ts) [] !(s.sym_type) @@ -273,22 +273,22 @@ let imitate_lam : problem -> ctxt -> meta -> unit = fun p c m -> | _ -> assert false end | _ -> - let tm2 = Env.to_prod env mk_Type in + let tm2 = Env.to_prod env Type in let m2 = LibMeta.fresh p tm2 n in - let a = mk_Meta (m2, Env.to_terms env) in + let a = Meta (m2, Env.to_terms env) in let x = new_var "x" in let env' = Env.add "x" x a None env in - let tm3 = Env.to_prod env' mk_Type in + let tm3 = Env.to_prod env' Type in let m3 = LibMeta.fresh p tm3 (n+1) in - let b = mk_Meta (m3, Env.to_terms env') in - let u = mk_Prod (a, bind_var x b) in + let b = Meta (m3, Env.to_terms env') in + let u = Prod (a, bind_var x b) in add_constr p (Env.to_ctxt env, u, t); x, a, env', b in let tm1 = Env.to_prod env' b in let m1 = LibMeta.fresh p tm1 (n+1) in - let u1 = mk_Meta (m1, Env.to_terms env') in - let xu1 = mk_Abst (a, bind_var x u1) in + let u1 = Meta (m1, Env.to_terms env') in + let xu1 = Abst (a, bind_var x u1) in let v = bind_mvar (Env.vars env) xu1 in if Logger.log_enabled () then log (red "%a ≔ %a") meta m term xu1; LibMeta.set p m v diff --git a/src/core/unif_rule.ml b/src/core/unif_rule.ml index c95541e27..0fd41b4a7 100644 --- a/src/core/unif_rule.ml +++ b/src/core/unif_rule.ml @@ -11,7 +11,7 @@ open Term let equiv : sym = let id = Pos.none "≡" in let s = - Sign.add_symbol Ghost.sign Public Defin Eager false id None mk_Kind [] in + Sign.add_symbol Ghost.sign Public Defin Eager false id None Kind [] in Timed.(s.sym_not := Infix(Pratter.Neither, 2.0)); s @@ -19,7 +19,7 @@ let equiv : sym = let cons : sym = let id = Pos.none ";" in let s = - Sign.add_symbol Ghost.sign Public Const Eager true id None mk_Kind [] in + Sign.add_symbol Ghost.sign Public Const Eager true id None Kind [] in Timed.(s.sym_not := Infix(Pratter.Right, 1.0)); s diff --git a/src/export/dk.ml b/src/export/dk.ml index 11620a4a3..e663b7f48 100644 --- a/src/export/dk.ml +++ b/src/export/dk.ml @@ -157,7 +157,6 @@ let modifiers : sym -> string list = fun s -> | Injec -> add "injective" | AC _ -> add "defac" | Defin -> add "def" - | Assoc _ -> assert false | Commu -> assert false end; if s.sym_expo = Protec then add "private"; diff --git a/src/export/hrs.ml b/src/export/hrs.ml index e06a6dc2a..470cbd264 100644 --- a/src/export/hrs.ml +++ b/src/export/hrs.ml @@ -126,7 +126,7 @@ let sym_rule : sym -> rule pp = fun s ppf r -> (** Translate the rules of symbol [s]. *) let rules_of_sym : sym pp = fun ppf s -> match Timed.(!(s.sym_def)) with - | Some d -> rule ppf (mk_Symb s, d) + | Some d -> rule ppf (Symb s, d) | None -> List.iter (sym_rule s ppf) Timed.(!(s.sym_rules)) (** Translate the rules of a dependency except if it is a ghost signature. *) diff --git a/src/export/rawdk.ml b/src/export/rawdk.ml index b152e4736..e16e8ac59 100644 --- a/src/export/rawdk.ml +++ b/src/export/rawdk.ml @@ -163,17 +163,13 @@ let partition_modifiers (ms:p_modifier list) : modifiers = props, expos, mstrats, opaqs (* check Stdlib.compare on modifiers. *) -let _ = - assert (Stdlib.compare Commu (Assoc true) < 0) - ;assert (Stdlib.compare Commu (Assoc false) < 0) - let modifiers : p_term option -> p_modifier list pp = fun p_sym_typ ppf ms -> match partition_modifiers ms with | [], [], [], [] -> out ppf "def " | [], [], [], [P_opaq] when p_sym_typ <> None -> out ppf "thm " (*https://github.com/Deducteam/Dedukti/issues/319*) - | [Commu;Assoc _], [], [], [] -> out ppf "defac " - | [Commu;Assoc _], [Protec], [], [] -> out ppf "private defac " + | [AC _], [], [], [] -> out ppf "defac " + | [AC _], [Protec], [], [] -> out ppf "private defac " | [Injec], [Protec], [], [] -> out ppf "private injective " | [Injec], [], [], [] -> out ppf "injective " | [], [Protec], [], [] -> out ppf "private " @@ -187,7 +183,7 @@ let get_ac_typ : popt -> modifiers -> p_params list -> p_term option -> p_term option = fun pos ms p_sym_arg p_sym_typ -> match ms with - | ([Commu;Assoc _], _, _, _) -> + | ([AC _], _, _, _) -> begin match p_sym_arg, p_sym_typ with | [], Some {elt=P_Arro(a,{elt=P_Arro(b,_);_});_} when eq_p_term a b -> Some a diff --git a/src/export/xtc.ml b/src/export/xtc.ml index fe3c15399..be1f08e54 100644 --- a/src/export/xtc.ml +++ b/src/export/xtc.ml @@ -99,7 +99,7 @@ and head : term pp = fun ppf t -> let x, b = unbind b in add_bvar x; out ppf "%a%a%a" bvar x typ a term b | Prod _ -> assert false - | LLet(a,t,b) -> term ppf (mk_Appl(mk_Abst(a,b),t)) + | LLet(a,t,b) -> term ppf (Appl(Abst(a,b),t)) and pvar_app : (int * term array) pp = fun ppf (i,ts) -> let arity = Array.length ts in @@ -136,7 +136,7 @@ let add_pvars : sym -> rule -> unit = fun s r -> (* Generate n fresh variables and n fresh metas for their types. *) let var = Array.init n (new_var_ind "$") in let p = new_problem() in - type_of_pvar := Array.init n (fun _ -> LibMeta.make p [] mk_Type); + type_of_pvar := Array.init n (fun _ -> LibMeta.make p [] Type); (* Replace in lhs pattern variables by variables. *) let rec subst_patt t = match unfold t with @@ -156,17 +156,17 @@ let add_pvars : sym -> rule -> unit = fun s r -> match unfold a with | Patt(Some i,_,[||]) -> let x,b = unbind b in - mk_Abst(!type_of_pvar.(i), bind_var x (subst_patt b)) + Abst(!type_of_pvar.(i), bind_var x (subst_patt b)) | Patt(Some _,_,_) -> assert false (*FIXME*) | _ -> assert false end - | Appl(a,b) -> mk_Appl(subst_patt a, subst_patt b) + | Appl(a,b) -> Appl(subst_patt a, subst_patt b) | Patt(None, _, _) -> assert false | Patt(Some i, _, ts) -> - Array.fold_left (fun acc t -> mk_Appl(acc,t)) (mk_Vari var.(i)) ts + Array.fold_left (fun acc t -> Appl(acc,t)) (Vari var.(i)) ts in let lhs = - List.fold_left (fun h t -> mk_Appl(h, subst_patt t)) (mk_Symb s) r.lhs + List.fold_left (fun h t -> Appl(h, subst_patt t)) (Symb s) r.lhs in (* Create a typing context mapping every variable to its type. *) let ctx = @@ -203,7 +203,7 @@ let sym_rule : sym -> rule pp = fun s ppf r -> (** Translate the rules of symbol [s]. *) let rules_of_sym : sym pp = fun ppf s -> match Timed.(!(s.sym_def)) with - | Some d -> rule ppf (mk_Symb s, d) + | Some d -> rule ppf (Symb s, d) | None -> List.iter (sym_rule s ppf) Timed.(!(s.sym_rules)) (** Translate the rules of a dependency except if it is a ghost signature. *) diff --git a/src/handle/command.ml b/src/handle/command.ml index 3fcf7a204..e89dd0dd5 100644 --- a/src/handle/command.ml +++ b/src/handle/command.ml @@ -24,14 +24,14 @@ let _ = match !((StrMap.find "nat_succ" ss.builtins).sym_type) with | Prod(a,_) -> a | _ -> assert false - with Not_found -> mk_Meta (LibMeta.fresh (new_problem()) mk_Type 0, [||]) + with Not_found -> Meta (LibMeta.fresh (new_problem()) Type 0, [||]) in register "nat_zero" expected_zero_type; let expected_succ_type ss _pos = let typ_0 = try !((StrMap.find "nat_zero" ss.builtins).sym_type) with Not_found -> - mk_Meta (LibMeta.fresh (new_problem()) mk_Type 0, [||]) + Meta (LibMeta.fresh (new_problem()) Type 0, [||]) in mk_Arro (typ_0, typ_0) in @@ -99,12 +99,7 @@ let handle_modifiers : p_modifier list -> prop * expo * match_strat = let props, expos, strats = get_modifiers ([],[],[]) ms in let prop = match props with - | [{elt=P_prop (Assoc b);_};{elt=P_prop Commu;_}] - | [{elt=P_prop Commu;_};{elt=P_prop (Assoc b);_}] -> AC b | _::{pos;_}::_ -> fatal pos "Incompatible or duplicated properties." - | [{elt=P_prop (Assoc _);pos}] -> - fatal pos "Associativity alone is not allowed as \ - you can use a rewriting rule instead." | [{elt=P_prop p;_}] -> p | [] -> Defin | _ -> assert false @@ -256,8 +251,8 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output = (* Check that the notation is compatible with the theory. *) begin match s.sym_prop, n with - | (Assoc true | AC true), Infix (Pratter.Right,_) - | (Assoc false | AC false), Infix (Pratter.Left,_) + | AC Left, Infix (Pratter.Right,_) + | AC Right, Infix (Pratter.Left,_) -> fatal pos "notation incompatible with symbol property \ (e.g. infix right notation on left associative symbol)" @@ -512,7 +507,7 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output = (* Keep the definition only if the symbol is not opaque. *) let d = if opaq then None else - Option.map (fun m -> unfold (mk_Meta(m,[||]))) ps.proof_term + Option.map (fun m -> unfold (Meta(m,[||]))) ps.proof_term in (* Add the symbol in the signature. *) fst (Sig_state.add_symbol @@ -524,7 +519,7 @@ let get_proof_data : compiler -> sig_state -> p_command -> cmd_output = (* Keep the definition only if the symbol is not opaque. *) let d = if opaq then None else - Option.map (fun m -> unfold (mk_Meta(m,[||]))) ps.proof_term + Option.map (fun m -> unfold (Meta(m,[||]))) ps.proof_term in (* Add the symbol in the signature. *) Console.out 2 (Color.red "symbol %a : %a") uid id term a; diff --git a/src/handle/compile.ml b/src/handle/compile.ml index 79706c6cd..a611f5417 100644 --- a/src/handle/compile.ml +++ b/src/handle/compile.ml @@ -48,7 +48,7 @@ let rec compile_with : if force || Extra.more_recent src obj then begin let forced = if force then " (forced)" else "" in - Console.out 1 "Checking \"%s\"%s ..." src forced; + Console.out 1 "Check \"%s\"%s ..." src forced; loading := mp :: !loading; let sign = Sig_state.create_sign mp in let sig_st = Stdlib.ref (Sig_state.of_sign sign) in @@ -61,14 +61,20 @@ let rec compile_with : Debug.stream_iter consume (Parser.parse_file src); Sign.strip_private sign; if Stdlib.(!gen_obj) then begin - Console.out 1 "Writing \"%s\" ..." obj; Sign.write sign obj + Console.out 1 "Write \"%s\" ..." obj; Sign.write sign obj end; loading := List.tl !loading; + Console.out 2 "Checked \"%s\"" src; + begin + match !loading with + | p::_ -> Console.out 2 "Continue checking %a ..." Path.pp p + | [] -> () + end; sign end else begin - Console.out 1 "Loading \"%s\" ..." obj; + Console.out 1 "Load \"%s\" ..." obj; let sign = Sign.read obj in (* We recursively load every module [mp'] on which [mp] depends. *) let compile mp' _ = ignore (compile_with ~handle ~force:false mp') in diff --git a/src/handle/inductive.ml b/src/handle/inductive.ml index 7d8edd701..3ea5271a3 100644 --- a/src/handle/inductive.ml +++ b/src/handle/inductive.ml @@ -37,7 +37,7 @@ let get_config : Sig_state.t -> Pos.popt -> config = fun ss pos -> (** [prf_of p c ts t] returns the term [c.symb_prf (p t1 ... tn t)] where ts = [ts1;...;tsn]. *) let prf_of : config -> var -> term list -> term -> term = fun c p ts t -> - mk_Appl (mk_Symb c.symb_prf, mk_Appl (add_args (mk_Vari p) ts, t)) + Appl (Symb c.symb_prf, Appl (add_args (Vari p) ts, t)) (** compute safe prefixes for predicate and constructor argument variables. *) let gen_safe_prefixes : inductive -> string * string * string = @@ -88,7 +88,7 @@ let ind_typ_with_codom : | (Prod(a,b), _) -> let name = x_str ^ string_of_int k in let (x,b) = unbind ~name b in - mk_Prod (a, bind_var x (aux (x::xs) (k+1) b)) + Prod (a, bind_var x (aux (x::xs) (k+1) b)) | _ -> fatal pos "The type of %a is not supported" sym ind_sym in aux (List.map (fun (_,(v,_,_)) -> v) env) 0 a @@ -115,15 +115,15 @@ let create_ind_pred_map : let ind_var = new_var_ind p_str i in (* predicate type *) let codom ts = - mk_Arro (add_args (mk_Symb ind_sym) ts, mk_Symb c.symb_Prop) in + mk_Arro (add_args (Symb ind_sym) ts, Symb c.symb_Prop) in let a = snd (Env.of_prod_using [] vs !(ind_sym.sym_type)) in let ind_type = ind_typ_with_codom pos ind_sym env codom x_str a in (* predicate conclusion *) let codom ts = let x = new_var x_str in let t = bind_var x - (prf_of c ind_var (List.remove_heads arity ts) (mk_Vari x)) in - mk_Prod (add_args (mk_Symb ind_sym) ts, t) + (prf_of c ind_var (List.remove_heads arity ts) (Vari x)) in + Prod (add_args (Symb ind_sym) ts, t) in let ind_conclu = ind_typ_with_codom pos ind_sym env codom x_str a in (ind_sym, {ind_var; ind_type; ind_conclu}) @@ -246,19 +246,19 @@ let gen_rec_types : let init = () in (* aux computes the induction hypothesis *) let aux env _ p ts x = - let v = Env.appl (mk_Vari x) env in + let v = Env.appl (Vari x) env in let v = prf_of c p (List.remove_heads n ts) v in Env.to_prod env v in let acc_rec_dom _ _ _ = () in let rec_dom t x v next = - mk_Prod (t, bind_var x (mk_Arro (v, next))) + Prod (t, bind_var x (mk_Arro (v, next))) in let acc_nonrec_dom _ _ = () in - let nonrec_dom t x next = mk_Prod (t, bind_var x next) in + let nonrec_dom t x next = Prod (t, bind_var x next) in let codom xs _ p ts = prf_of c p (List.remove_heads n ts) - (add_args (mk_Symb cons_sym) (List.rev_map mk_Vari xs)) + (add_args (Symb cons_sym) (List.rev_map mk_Vari xs)) in fold_cons_type pos ind_pred_map x_str ind_sym vs cons_sym inj_var init aux acc_rec_dom rec_dom acc_nonrec_dom nonrec_dom codom @@ -274,7 +274,7 @@ let gen_rec_types : in let rec_typ = List.fold_right add_clauses_ind ind_list d.ind_conclu in let add_quantifier t (_,d) = - mk_Prod (d.ind_type, bind_var d.ind_var t) in + Prod (d.ind_type, bind_var d.ind_var t) in let rec_typ = List.fold_left add_quantifier rec_typ ind_pred_map in Env.to_prod env rec_typ in diff --git a/src/handle/proof.ml b/src/handle/proof.ml index 4d620de6e..2cf3f3cf3 100644 --- a/src/handle/proof.ml +++ b/src/handle/proof.ml @@ -34,7 +34,7 @@ module Goal = struct let env : goal -> Env.t = fun g -> match g with | Unif (c,_,_) -> - let t, n = Ctxt.to_prod c mk_Type in + let t, n = Ctxt.to_prod c Type in (try fst (Env.of_prod_nth c n t) with Invalid_argument _ -> assert false) | Typ gt -> gt.goal_hyps diff --git a/src/handle/query.ml b/src/handle/query.ml index 052de0d29..a15a42ba2 100644 --- a/src/handle/query.ml +++ b/src/handle/query.ml @@ -147,7 +147,7 @@ let handle : Sig_state.t -> proof_state option -> p_query -> result = | None -> fatal pos "Not in a proof" | Some ps -> match ps.proof_term with - | Some m -> return term (mk_Meta(m,[||])) + | Some m -> return term (Meta(m,[||])) | None -> fatal pos "Not in a definition") | _ -> let env = Proof.focus_env ps in diff --git a/src/handle/rewrite.ml b/src/handle/rewrite.ml index 0035282ca..514cc7cfe 100644 --- a/src/handle/rewrite.ml +++ b/src/handle/rewrite.ml @@ -32,7 +32,7 @@ let _ = let check_codomain_is_Type _ss pos sym = let valid = match Eval.whnf [] Timed.(!(sym.sym_type)) with - | Prod(_, b) -> Eval.eq_modulo [] (snd (unbind b)) mk_Type + | Prod(_, b) -> Eval.eq_modulo [] (snd (unbind b)) Type | _ -> false in if not valid then @@ -57,9 +57,9 @@ let _ = let term_U = get_domain_of_type symb_T in let term_Prop = get_domain_of_type symb_P in let a = new_var "a" in - let term_T_a = mk_Appl (mk_Symb symb_T, mk_Vari a) in + let term_T_a = Appl (Symb symb_T, Vari a) in let impls = mk_Arro (term_T_a, mk_Arro (term_T_a, term_Prop)) in - mk_Prod (term_U, bind_var a impls) + Prod (term_U, bind_var a impls) in register_builtin "eq" expected_eq_type; let expected_refl_type pos map = @@ -70,39 +70,39 @@ let _ = let term_U = get_domain_of_type symb_T in let a = new_var "a" in let x = new_var "x" in - let appl_eq = mk_Appl (mk_Symb symb_eq, mk_Vari a) in - let appl_eq = mk_Appl (mk_Appl (appl_eq, mk_Vari x), mk_Vari x) in - let appl = mk_Appl (mk_Symb symb_P, appl_eq) in - let term_T_a = mk_Appl (mk_Symb symb_T, mk_Vari a) in - let prod = mk_Prod (term_T_a, bind_var x appl) in - mk_Prod (term_U, bind_var a prod) + let appl_eq = Appl (Symb symb_eq, Vari a) in + let appl_eq = Appl (Appl (appl_eq, Vari x), Vari x) in + let appl = Appl (Symb symb_P, appl_eq) in + let term_T_a = Appl (Symb symb_T, Vari a) in + let prod = Prod (term_T_a, bind_var x appl) in + Prod (term_U, bind_var a prod) in register_builtin "refl" expected_refl_type; let expected_eqind_type pos map = (* [Π (a:U) (x y:T a), P (eq x y) → Π (p:T a→Prop), P (p y) → P (p x)] *) let symb_T = Builtin.get pos map "T" in - let term_T = mk_Symb symb_T in + let term_T = Symb symb_T in let symb_P = Builtin.get pos map "P" in - let term_P = mk_Symb symb_P in + let term_P = Symb symb_P in let symb_eq = Builtin.get pos map "eq" in - let term_eq = mk_Symb symb_eq in + let term_eq = Symb symb_eq in let term_U = get_domain_of_type symb_T in let term_Prop = get_domain_of_type symb_P in let a = new_var "a" in let x = new_var "x" in let y = new_var "y" in let p = new_var "p" in - let term_T_a = mk_Appl (term_T, mk_Vari a) in - let term_P_p_x = mk_Appl (term_P, mk_Appl (mk_Vari p, mk_Vari x)) in - let term_P_p_y = mk_Appl (term_P, mk_Appl (mk_Vari p, mk_Vari y)) in + let term_T_a = Appl (term_T, Vari a) in + let term_P_p_x = Appl (term_P, Appl (Vari p, Vari x)) in + let term_P_p_y = Appl (term_P, Appl (Vari p, Vari y)) in let impl = mk_Arro (term_P_p_y, term_P_p_x) in let prod = - mk_Prod (mk_Arro (term_T_a, term_Prop), bind_var p impl) in - let eq = add_args term_eq [mk_Vari a; mk_Vari x; mk_Vari y] in - let impl = mk_Arro (mk_Appl(term_P, eq), prod) in - let prod = mk_Prod (term_T_a, bind_var y impl) in - let prod = mk_Prod (term_T_a, bind_var x prod) in - mk_Prod (term_U, bind_var a prod) + Prod (mk_Arro (term_T_a, term_Prop), bind_var p impl) in + let eq = add_args term_eq [Vari a; Vari x; Vari y] in + let impl = mk_Arro (Appl(term_P, eq), prod) in + let prod = Prod (term_T_a, bind_var y impl) in + let prod = Prod (term_T_a, bind_var x prod) in + Prod (term_U, bind_var a prod) in register_builtin "eqind" expected_eqind_type @@ -221,7 +221,7 @@ let matches : term -> term -> bool = corresponding elements of [ts] in [p] yields [t]. *) let matching_subs : to_subst -> term -> term array option = fun (xs,p) t -> (* We replace [xs] by fresh [TRef]'s. *) - let ts = Array.map (fun _ -> mk_TRef(Timed.ref None)) xs in + let ts = Array.map (fun _ -> TRef(Timed.ref None)) xs in let p = msubst (bind_mvar xs p) ts in if matches p t then Some(Array.map unfold ts) else None @@ -284,19 +284,19 @@ let find_subterm_matching : term -> term -> bool = fun p t -> let bind_pattern : term -> term -> binder = fun p t -> let z = new_var "z" in let rec replace : term -> term = fun t -> - if matches p t then mk_Vari z else + if matches p t then Vari z else match unfold t with - | Appl(t,u) -> mk_Appl (replace t, replace u) + | Appl(t,u) -> Appl (replace t, replace u) | Prod(a,b) -> let x,b = unbind b in - mk_Prod (replace a, bind_var x (replace b)) + Prod (replace a, bind_var x (replace b)) | Abst(a,b) -> let x,b = unbind b in - mk_Abst (replace a, bind_var x (replace b)) + Abst (replace a, bind_var x (replace b)) | LLet(typ, def, body) -> let x, body = unbind body in - mk_LLet (replace typ, replace def, bind_var x (replace body)) - | Meta(m,ts) -> mk_Meta (m, Array.map replace ts) + LLet (replace typ, replace def, bind_var x (replace body)) + | Meta(m,ts) -> Meta (m, Array.map replace ts) | Bvar _ -> assert false | Wild -> assert false | TRef _ -> assert false @@ -313,32 +313,31 @@ let swap : eq_config -> term -> term -> term -> term -> term = (* We build the predicate “λx:T a, eq a l x”. *) let pred = let x = new_var "x" in - let pred = add_args (mk_Symb cfg.symb_eq) [a; l; mk_Vari x] in - mk_Abst(mk_Appl(mk_Symb cfg.symb_T, a), bind_var x pred) + let pred = add_args (Symb cfg.symb_eq) [a; l; Vari x] in + Abst(Appl(Symb cfg.symb_T, a), bind_var x pred) in (* We build the proof term. *) - let refl_a_l = add_args (mk_Symb cfg.symb_refl) [a; l] in - add_args (mk_Symb cfg.symb_eqind) [a; r; l; t; pred; refl_a_l] + let refl_a_l = add_args (Symb cfg.symb_refl) [a; l] in + add_args (Symb cfg.symb_eqind) [a; r; l; t; pred; refl_a_l] (** [replace_wild_by_tref t] substitutes every wildcard of [t] by a fresh [TRef]. *) let rec replace_wild_by_tref : term -> term = fun t -> match unfold t with - | Wild -> mk_TRef(Timed.ref None) - | Appl(t,u) -> - mk_Appl_not_canonical(replace_wild_by_tref t, replace_wild_by_tref u) + | Wild -> TRef(Timed.ref None) + | Appl(t,u) -> Appl(replace_wild_by_tref t, replace_wild_by_tref u) | _ -> t -(** [rewrite ss p pos gt l2r pat t] generates a term for the refine tactic +(** [rewrite ss p pos gt side pat t] generates a term for the refine tactic representing the application of the rewrite tactic to the goal type [gt]. Every occurrence of the first instance of the left-hand side is replaced by the right-hand side of the obtained proof (or the reverse if - l2r is false). [pat] is an optional SSReflect pattern. [t] is the + side=Left). [pat] is an optional SSReflect pattern. [t] is the equational lemma that is appied. It handles the full set of SSReflect patterns. *) -let rewrite : Sig_state.t -> problem -> popt -> goal_typ -> bool -> +let rewrite : Sig_state.t -> problem -> popt -> goal_typ -> side -> (term, binder) Parsing.Syntax.rw_patt option -> term -> term = - fun ss p pos {goal_hyps=g_env; goal_type=g_type; _} l2r pat t -> + fun ss p pos {goal_hyps=g_env; goal_type=g_type; _} side pat t -> (* Obtain the required symbols from the current signature. *) let cfg = get_eq_config ss pos in @@ -352,10 +351,10 @@ let rewrite : Sig_state.t -> problem -> popt -> goal_typ -> bool -> let vars = Array.of_list vars in (* Apply [t] to the variables of [vars] to get a witness of the equality. *) - let t = Array.fold_left (fun t x -> mk_Appl(t, mk_Vari x)) t vars in + let t = Array.fold_left (fun t x -> Appl(t, Vari x)) t vars in - (* Reverse the members of the equation if l2r is false. *) - let (t, l, r) = if l2r then (t, l, r) else (swap cfg a l r t, r, l) in + (* Reverse the members of the equation if side=Left. *) + let (t,l,r) = if side=Right then (t,l,r) else (swap cfg a l r t, r, l) in (* Bind the variables in this new witness. *) let bound = let bind = bind_mvar vars in bind t, bind l, bind r in @@ -661,14 +660,14 @@ let rewrite : Sig_state.t -> problem -> popt -> goal_typ -> bool -> in (* Construct the predicate (context). *) - let pred = mk_Abst(mk_Appl(mk_Symb cfg.symb_T, a), pred_bind) in + let pred = Abst(Appl(Symb cfg.symb_T, a), pred_bind) in (* Construct the new goal and its type. *) - let goal_type = mk_Appl(mk_Symb cfg.symb_P, new_term) in + let goal_type = Appl(Symb cfg.symb_P, new_term) in let goal_term = LibMeta.make p g_ctxt goal_type in (* Build the final term produced by the tactic. *) - let eqind = mk_Symb cfg.symb_eqind in + let eqind = Symb cfg.symb_eqind in let result = add_args eqind [a; l; r; t; pred; goal_term] in (* Debugging data to the log. *) diff --git a/src/handle/tactic.ml b/src/handle/tactic.ml index d5c585260..e5103979c 100644 --- a/src/handle/tactic.ml +++ b/src/handle/tactic.ml @@ -47,7 +47,7 @@ let add_axiom : Sig_state.t -> popt -> meta -> sym = metavariable. *) let meta_value = let vars = Array.init m.meta_arity (new_var_ind "x") in - let ax = add_args (mk_Symb sym) (List.map mk_Vari (Array.to_list vars)) in + let ax = add_args_map (Symb sym) mk_Vari (Array.to_list vars) in bind_mvar vars ax in LibMeta.set (new_problem()) m meta_value; sym @@ -166,13 +166,13 @@ let tac_induction : popt -> proof_state -> goal_typ -> goal list let p = new_problem () in let metas = let fresh_meta _ = - let mt = LibMeta.make p ctx mk_Type in + let mt = LibMeta.make p ctx Type in LibMeta.make p ctx mt in (* Reverse to have goals properly sorted. *) List.(rev (init (n - 1) fresh_meta)) in - let t = add_args (mk_Symb ind.ind_prop) metas in + let t = add_args (Symb ind.ind_prop) metas in tac_refine pos ps gt gs p t | _ -> fatal pos "[%a] is not a product." term goal_type @@ -181,7 +181,7 @@ let tac_induction : popt -> proof_state -> goal_typ -> goal list let count_products : ctxt -> term -> int = fun c -> let rec count acc t = match Eval.whnf c t with - | Prod(_,b) -> count (acc + 1) (subst b mk_Kind) + | Prod(_,b) -> count (acc + 1) (subst b Kind) | _ -> acc in count 0 @@ -350,9 +350,9 @@ let p_tactic (ss:Sig_state.t) (pos:popt) :term -> p_tactic = | T_remove, _ -> assert false | T_repeat, [t] -> P_tac_repeat(tac t) | T_repeat, _ -> assert false - | T_rewrite, [_;t] -> P_tac_rewrite(true,None,p_term pos t) + | T_rewrite, [_;t] -> P_tac_rewrite(Right,None,p_term pos t) | T_rewrite, _ -> assert false - | T_rewrite_left, [_;t] -> P_tac_rewrite(false,None,p_term pos t) + | T_rewrite_left, [_;t] -> P_tac_rewrite(Left,None,p_term pos t) | T_rewrite_left, _ -> assert false | T_set, [t1;_;t2] -> P_tac_set(p_ident_of_sym pos t1,p_term pos t2) @@ -448,9 +448,9 @@ let rec handle : let u = gt.goal_type in let q = Env.to_prod [x] (Env.to_prod e2 u) in let m = LibMeta.fresh p (Env.to_prod e1 q) (List.length e1) in - let me1 = mk_Meta (m, Env.to_terms e1) in + let me1 = Meta (m, Env.to_terms e1) in let t = - List.fold_left (fun t (_,(v,_,_)) -> mk_Appl(t, mk_Vari v)) + List.fold_left (fun t (_,(v,_,_)) -> Appl(t, Vari v)) me1 (x :: List.rev e2) in tac_refine pos ps gt gs p t @@ -465,7 +465,7 @@ let rec handle : (* Generate the constraints for [t] to be of type [Type]. *) let c = Env.to_ctxt env in begin - match Infer.check_noexn p c t mk_Type with + match Infer.check_noexn p c t Type with | None -> fatal pos "%a is not of type Type." term t | Some t -> (* Create a new goal of type [t]. *) @@ -476,7 +476,7 @@ let rec handle : let env' = Env.add id.elt v t None env in let m2 = LibMeta.fresh p (Env.to_prod env' gt.goal_type) (n+1) in let ts = Env.to_terms env in - let u = mk_Meta (m2, Array.append ts [|mk_Meta (m1, ts)|]) in + let u = Meta (m2, Array.append ts [|Meta (m1, ts)|]) in tac_refine pos ps gt gs p u end | P_tac_set(id,t) -> @@ -496,7 +496,7 @@ let rec handle : let v = LibTerm.fold x t gt.goal_type in let m = LibMeta.fresh p (Env.to_prod e' v) n in let ts = Env.to_terms env in - let u = mk_Meta (m, Array.append ts [|t|]) in + let u = Meta (m, Array.append ts [|t|]) in (*tac_refine pos ps gt gs p u*) LibMeta.set p gt.goal_meta (bind_mvar (Env.vars env) u); (*let g = Goal.of_meta m in*) @@ -517,7 +517,7 @@ let rec handle : | Typ gt::gs -> let cfg = Rewrite.get_eq_config ss pos in let (a,l,_),_ = Rewrite.get_eq_data cfg pos gt.goal_type in - let prf = add_args (mk_Symb cfg.symb_refl) [a; l] in + let prf = add_args (Symb cfg.symb_refl) [a; l] in tac_refine pos ps gt gs (new_problem()) prf end | P_tac_remove ids -> @@ -541,7 +541,7 @@ let rec handle : let a' = Env.to_prod env' gt.goal_type in let p = new_problem() in let m' = LibMeta.fresh p a' n in - let t = mk_Meta(m',Env.to_terms env') in + let t = Meta(m',Env.to_terms env') in LibMeta.set p m (bind_mvar (Env.vars env) t); Goal.of_meta m' in @@ -556,18 +556,18 @@ let rec handle : let ids = List.map fst (List.sort cmp (List.map id_pos ids)) in let g = List.fold_left remove g ids in {ps with proof_goals = g::gs} - | P_tac_rewrite(l2r,pat,eq) -> + | P_tac_rewrite(side,pat,eq) -> let pat = Option.map (Scope.scope_rw_patt ss env) pat in let p = new_problem() in tac_refine pos ps gt gs p - (Rewrite.rewrite ss p pos gt l2r pat (scope eq)) + (Rewrite.rewrite ss p pos gt side pat (scope eq)) | P_tac_sym -> let cfg = Rewrite.get_eq_config ss pos in let (a,l,r),_ = Rewrite.get_eq_data cfg pos gt.goal_type in let p = new_problem() in let prf = - let mt = mk_Appl(mk_Symb cfg.symb_P, - add_args (mk_Symb cfg.symb_eq) [a;r;l]) in + let mt = Appl(Symb cfg.symb_P, + add_args (Symb cfg.symb_eq) [a;r;l]) in let meta_term = LibMeta.make p (Env.to_ctxt env) mt in (* The proofterm is [eqind a r l M (λx,eq a l x) (refl a l)]. *) Rewrite.swap cfg a r l meta_term diff --git a/src/lplib/list.ml b/src/lplib/list.ml index 2fd3d9cfb..729323377 100644 --- a/src/lplib/list.ml +++ b/src/lplib/list.ml @@ -170,7 +170,7 @@ let destruct : 'a list -> int -> 'a list * 'a * 'a list = {!val:destruct} to insert a sublist [l] in the place of the element at the specified position in the specified list. *) let reconstruct : 'a list -> 'a list -> 'a list -> 'a list = fun l m r -> - L.rev_append l (m @ r) + rev_append l (m @ r) (** [init n f] creates a list with [f 0] up to [f n] as its elements. Note that [Invalid_argument] is raised if [n] is negative. *) @@ -194,7 +194,7 @@ let mem_sorted : 'a cmp -> 'a -> 'a list -> bool = fun cmp x -> let insert : 'a cmp -> 'a -> 'a list -> 'a list = fun cmp x -> let rec insert acc = function | y :: l' when cmp x y > 0 -> insert (y :: acc) l' - | l -> L.rev_append acc (x :: l) + | l -> rev_append acc (x :: l) in insert [] (* unit tests *) @@ -211,14 +211,14 @@ let insert_uniq : 'a cmp -> 'a -> 'a list -> 'a list = fun cmp x -> let exception Found in let rec insert acc l = match l with - | [] -> L.rev_append acc [x] + | [] -> rev_append acc [x] | y :: l' -> begin let n = cmp x y in match n with | 0 -> raise Found | _ when n > 0 -> insert (y :: acc) l' - | _ -> L.rev_append acc (x :: l) + | _ -> rev_append acc (x :: l) end in fun l -> try insert [] l with Found -> l @@ -309,3 +309,9 @@ let pos : ('a -> bool) -> 'a list -> int = fun f -> | [] -> raise Not_found | x::xs -> if f x then k else pos (k+1) xs in pos 0 + +(** [rev_append2 [x1;..;xm] [y1;..;yn] l] raises [Invalid_arg] if [m<>n], and + [(xn,yn)::..::(x1,y1)::l] otherwise. *) +let rev_append2 = + let combine acc xi yi = (xi,yi)::acc in + fun xs ys l -> fold_left2 combine l xs ys diff --git a/src/parsing/dkParser.mly b/src/parsing/dkParser.mly index 9eb887a37..b16fe4970 100644 --- a/src/parsing/dkParser.mly +++ b/src/parsing/dkParser.mly @@ -41,7 +41,7 @@ let defin lps = make_pos lps (P_prop Defin) let const lps = make_pos lps (P_prop Const) let inj lps = make_pos lps (P_prop Injec) - let ac lps = make_pos lps (P_prop (AC false)) + let ac lps = make_pos lps (P_prop (AC Right)) let opaq lps = make_pos lps P_opaq let protec lps = make_pos lps (P_expo Protec) diff --git a/src/parsing/lpLexer.ml b/src/parsing/lpLexer.ml index 3b039f992..46b24df48 100644 --- a/src/parsing/lpLexer.ml +++ b/src/parsing/lpLexer.ml @@ -97,7 +97,7 @@ type token = (* Tuple constructor (with parens) required by Menhir. *) | INT of string | FLOAT of string - | SIDE of Pratter.associativity + | SIDE of Core.Term.side | STRINGLIT of string | SWITCH of bool @@ -227,7 +227,7 @@ let rec token lb = | "inductive" -> INDUCTIVE | "infix" -> INFIX | "injective" -> INJECTIVE - | "left" -> SIDE(Pratter.Left) + | "left" -> SIDE(Core.Term.Left) | "let" -> LET | "notation" -> NOTATION | "off" -> SWITCH(false) @@ -250,7 +250,7 @@ let rec token lb = | "repeat" -> REPEAT | "require" -> REQUIRE | "rewrite" -> REWRITE - | "right" -> SIDE(Pratter.Right) + | "right" -> SIDE(Core.Term.Right) | "rule" -> RULE | "search" -> SEARCH | "sequential" -> SEQUENTIAL diff --git a/src/parsing/lpParser.mly b/src/parsing/lpParser.mly index b900e9297..a89c78c8c 100644 --- a/src/parsing/lpParser.mly +++ b/src/parsing/lpParser.mly @@ -15,6 +15,11 @@ let make_prod startpos ps t endpos = if ps = [] then t else make_pos (startpos,endpos) (P_Prod(ps,t)) + + let assoc_of_side_opt = function + | Some Core.Term.Left -> Pratter.Left + | Some Core.Term.Right -> Pratter.Right + | None -> Pratter.Neither %} // end of file @@ -90,7 +95,7 @@ %token DEBUG_FLAGS %token INT %token FLOAT -%token SIDE +%token SIDE %token STRINGLIT %token SWITCH @@ -224,9 +229,8 @@ path: | p=QID { make_pos $sloc (List.rev p) } modifier: - | d=ioption(SIDE) ASSOCIATIVE - { let b = match d with Some Pratter.Left -> true | _ -> false in - make_pos $sloc (P_prop (Term.Assoc b)) } + | s=SIDE ASSOCIATIVE COMMUTATIVE + { make_pos $sloc (P_prop (Term.AC s)) } | COMMUTATIVE { make_pos $sloc (P_prop Term.Commu) } | CONSTANT { make_pos $sloc (P_prop Term.Const) } | INJECTIVE { make_pos $sloc (P_prop Term.Injec) } @@ -341,9 +345,8 @@ tactic: | REFLEXIVITY { make_pos $sloc P_tac_refl } | REMOVE xs=uid+ { make_pos $sloc (P_tac_remove xs) } | REPEAT t=tactic { make_pos $sloc (P_tac_repeat t) } - | REWRITE d=SIDE? p=rw_patt_spec? t=term - { let b = match d with Some Pratter.Left -> false | _ -> true in - make_pos $sloc (P_tac_rewrite(b,p,t)) } + | REWRITE s=SIDE? p=rw_patt_spec? t=term + { make_pos $sloc (P_tac_rewrite(Option.get Core.Term.Right s,p,t)) } | SET i=uid ASSIGN t=term { make_pos $sloc (P_tac_set(i,t)) } | SIMPLIFY { make_pos $sloc (P_tac_simpl SimpAll) } | SIMPLIFY i=qid { make_pos $sloc (P_tac_simpl (SimpSym i)) } @@ -399,8 +402,8 @@ unif_rule: e=equation HOOK_ARROW equation: l=term EQUIV r=term { (l, r) } notation: - | INFIX a=SIDE? p=float_or_int - { Term.Infix(Option.get Pratter.Neither a, p) } + | INFIX s=SIDE? p=float_or_int + { Term.Infix(assoc_of_side_opt s, p) } | POSTFIX p=float_or_int { Term.Postfix(p) } | PREFIX p=float_or_int { Term.Prefix(p) } | QUANTIFIER { Term.Quant } diff --git a/src/parsing/pretty.ml b/src/parsing/pretty.ml index be2899d53..df1e9992d 100644 --- a/src/parsing/pretty.ml +++ b/src/parsing/pretty.ml @@ -43,7 +43,7 @@ let _ = let open LpLexer in ; "inductive", INDUCTIVE ; "infix", INFIX ; "injective", INJECTIVE - ; "left", SIDE(Pratter.Left) + ; "left", SIDE(Core.Term.Left) ; "let", LET ; "off", SWITCH(false) ; "on", SWITCH(true) @@ -62,7 +62,7 @@ let _ = let open LpLexer in ; "reflexivity", REFLEXIVITY ; "require", REQUIRE ; "rewrite", REWRITE - ; "right", SIDE(Pratter.Right) + ; "right", SIDE(Core.Term.Right) ; "rule", RULE ; "sequential", SEQUENTIAL ; "simplify", SIMPLIFY @@ -279,10 +279,10 @@ let rec tactic : p_tactic pp = fun ppf { elt; _ } -> | P_tac_remove ids -> out ppf "remove%a" (List.pp (unit " " |+ ident) "") ids | P_tac_repeat t -> out ppf "repeat %a" tactic t - | P_tac_rewrite(b,p,t) -> - let dir ppf b = if not b then out ppf " left" in + | P_tac_rewrite(s,p,t) -> + let dir ppf s = if s = Term.Left then out ppf " left" in let pat ppf p = out ppf " .[%a]" rw_patt p in - out ppf "rewrite%a%a %a" dir b (Option.pp pat) p term t + out ppf "rewrite%a%a %a" dir s (Option.pp pat) p term t | P_tac_set (id, t) -> out ppf "set %a ≔ %a" ident id term t | P_tac_simpl SimpAll -> out ppf "simplify" | P_tac_simpl SimpBetaOnly -> out ppf "simplify rule off" diff --git a/src/parsing/scope.ml b/src/parsing/scope.ml index 45b993d7b..0862859a7 100644 --- a/src/parsing/scope.ml +++ b/src/parsing/scope.ml @@ -31,10 +31,10 @@ let find_qid : (* Check for variables in the environment first. *) try if mp <> [] then raise Not_found; (* Variables cannot be qualified. *) - mk_Vari (Env.find s env) + Vari (Env.find s env) with Not_found -> (* Check for symbols. *) - mk_Symb (find_sym ~prt ~prv ss qid) + Symb (find_sym ~prt ~prv ss qid) (** Representation of the different scoping modes. Note that the constructors hold specific information for the given mode. *) @@ -125,10 +125,10 @@ let fresh_patt : lhs_data -> string option -> term array -> term = Hashtbl.add data.m_lhs_indices name i; Hashtbl.add data.m_lhs_names i name; i in - mk_Patt (Some i, name, ts) + Patt (Some i, name, ts) | None -> let i = fresh_index () in - mk_Patt (Some i, string_of_int i, ts) + Patt (Some i, string_of_int i, ts) (* used in desugaring decimal notations *) let strint = Array.init 11 string_of_int @@ -193,30 +193,26 @@ and scope_parsed : ?find_sym:find_sym -> and add_impl : ?find_sym:find_sym -> int -> mode -> sig_state -> Env.t -> popt -> term -> bool list -> p_term list -> term = fun ?find_sym k md ss env loc h impl args -> - let appl = - match md with - | M_LHS _ | M_SearchPatt _ -> mk_Appl_not_canonical - | _ -> mk_Appl in - let appl_p_term t u = appl(t, scope_parsed ?find_sym (k+1) md ss env u) in - let appl_meta t = appl(t, scope_head ?find_sym (k+1) md ss env P.wild) in + let app_term t u = Appl(t, scope_parsed ?find_sym (k+1) md ss env u) in + let app_meta t = Appl(t, scope_head ?find_sym (k+1) md ss env P.wild) in match impl, args with (* The remaining arguments are all explicit. *) - | [], _ -> List.fold_left appl_p_term h args + | [], _ -> List.fold_left app_term h args (* Only implicit arguments remain. *) - | true::impl, [] -> add_impl ?find_sym k md ss env loc (appl_meta h) impl [] + | true::impl, [] -> add_impl ?find_sym k md ss env loc (app_meta h) impl [] (* The first argument is implicit (could be [a] if made explicit). *) | true::impl, a::args -> begin match a.elt with | P_Expl b -> add_impl ?find_sym k md ss env loc - (appl_p_term h {a with elt = P_Wrap b}) impl args - | _ -> add_impl ?find_sym k md ss env loc (appl_meta h) impl (a::args) + (app_term h {a with elt = P_Wrap b}) impl args + | _ -> add_impl ?find_sym k md ss env loc (app_meta h) impl (a::args) end (* The first argument [a] is explicit. *) | false::impl, a::args -> begin match a.elt with | P_Expl _ -> fatal a.pos "Unexpected explicit argument." - | _ -> add_impl ?find_sym k md ss env loc (appl_p_term h a) impl args + | _ -> add_impl ?find_sym k md ss env loc (app_term h a) impl args end (* The application is too "partial" to insert all implicit arguments. *) | false::_, [] -> @@ -231,7 +227,7 @@ and scope_domain : ?find_sym:find_sym -> match a, md with | (Some {elt=P_Wild;_}|None), (M_LHS data | M_SearchPatt (_,data)) -> fresh_patt data None (Env.to_terms env) - | (Some {elt=P_Wild;_}|None), _ -> mk_Plac true + | (Some {elt=P_Wild;_}|None), _ -> Plac true | Some a, _ -> scope ?find_sym ~typ:true k md ss env a (** [scope_binder ~find_sym ~typ k md ss cons env params_list t] scopes [t], @@ -248,7 +244,7 @@ and scope_binder : begin match t with | Some t -> scope ?find_sym ~typ (k+1) md ss env t - | None -> mk_Plac true + | None -> Plac true end | (idopts,typopt,_implicit)::params_list -> let dom = scope_domain ?find_sym (k+1) md ss env typopt in @@ -275,7 +271,7 @@ and scope_head : ?find_sym:find_sym -> ?typ:bool -> int -> mode -> sig_state -> env -> p_term -> term = fun ?find_sym ?(typ=false) k md ss env ({elt;pos} as t) -> match elt, md with - | (P_Type, _) -> mk_Type + | (P_Type, _) -> Type | (P_Iden(qid,_), _) -> scope_iden ?find_sym md ss env qid @@ -286,11 +282,11 @@ and scope_head : ?find_sym:find_sym -> match StrMap.find_opt s Timed.(!(Ghost.sign.sign_symbols)) with | Some sym -> sym | None -> - let str = mk_Symb (Builtin.get ss pos "String") in + let str = Symb (Builtin.get ss pos "String") in Sign.add_symbol Ghost.sign Public Const Eager true {elt=s;pos} pos str [] in - mk_Symb sym + Symb sym end | (P_NLit s, _) -> @@ -299,7 +295,7 @@ and scope_head : ?find_sym:find_sym -> let s = if neg then String.sub s 1 (String.length s - 1) else s in neg, s in - let sym_of s = mk_Symb (Builtin.get ss pos s) in + let sym_of s = Symb (Builtin.get ss pos s) in let sym = Array.map sym_of strint in let digit = function | '0' -> sym.(0) | '1' -> sym.(1) | '2' -> sym.(2) | '3' -> sym.(3) @@ -307,24 +303,24 @@ and scope_head : ?find_sym:find_sym -> | '8' -> sym.(8) | '9' -> sym.(9) | _ -> assert false in let sym_add = sym_of "+" in - let add x y = mk_Appl(mk_Appl(sym_add,x),y) in + let add x y = Appl(Appl(sym_add,x),y) in let sym_mul = sym_of "*" in - let mul x y = mk_Appl(mk_Appl(sym_mul,x),y) in + let mul x y = Appl(Appl(sym_mul,x),y) in let rec unsugar i = if i <= 0 then digit s.[0] else add (digit s.[i]) (mul sym.(10) (unsugar (i-1))) in let n = unsugar (String.length s - 1) in - if neg then mk_Appl(sym_of "-",n) else n + if neg then Appl(sym_of "-",n) else n | (P_Wild, M_URHS(data)) -> let i = data.m_urhs_vars_nb in data.m_urhs_vars_nb <- data.m_urhs_vars_nb + 1; - mk_Patt (Some i, "_", Env.to_terms env) + Patt (Some i, "_", Env.to_terms env) | (P_Wild, (M_LHS data | M_SearchPatt (_,data))) -> fresh_patt data None (Env.to_terms env) - | (P_Wild, M_Patt) -> mk_Wild - | (P_Wild, (M_RHS _|M_Term _)) -> mk_Plac typ + | (P_Wild, M_Patt) -> Wild + | (P_Wild, (M_RHS _|M_Term _)) -> Plac typ | (P_Meta({elt;pos} as mk,ts), (M_Term {m_term_meta_of_key;_} | M_SearchPatt(m_term_meta_of_key,_))) -> ( @@ -333,7 +329,7 @@ and scope_head : ?find_sym:find_sym -> fatal pos "Metavariable %a not found among generated variables: \ metavariables can only be created by the system." Pretty.meta_ident mk - | Some m -> mk_Meta (m, Array.map (scope ?find_sym (k+1) md ss env) ts)) + | Some m -> Meta (m, Array.map (scope ?find_sym (k+1) md ss env) ts)) | (P_Meta(_), _) -> fatal pos "Metavariables are not allowed here." | (P_Patt(id,ts), (M_LHS(d) | M_SearchPatt(_,d))) -> @@ -399,7 +395,7 @@ and scope_head : ?find_sym:find_sym -> | Some ts -> Array.map (scope ?find_sym (k+1) md ss env) ts in let name = match id with Some {elt;_} -> elt | None -> assert false in - mk_Patt (Some i, name, ts) + Patt (Some i, name, ts) | (P_Patt(id,ts), M_RHS(r)) -> let i = match id with @@ -415,7 +411,7 @@ and scope_head : ?find_sym:find_sym -> | Some ts -> Array.map (scope ?find_sym (k+1) md ss env) ts in let name = match id with Some {elt;_} -> elt | None -> assert false in - mk_Patt (Some i, name, ts) + Patt (Some i, name, ts) | (P_Patt(_,_), _) -> fatal pos "Pattern variables are only allowed in rewriting rules." @@ -445,7 +441,7 @@ and scope_head : ?find_sym:find_sym -> scope ?find_sym ~typ (k+1) md ss (Env.add x.elt v a (Some t) env) u in if not (occur v u) then wrn x.pos "Useless let-binding (%s is not bound)." x.elt; - mk_LLet (a, t, bind_var v u) + LLet (a, t, bind_var v u) | (P_LLet(_), M_LHS(_)) -> fatal pos "Let-bindings are not allowed in a LHS." | (P_LLet(_), M_Patt) -> @@ -460,7 +456,7 @@ and scope_head : ?find_sym:find_sym -> let scope = let open Stdlib in - let r = ref mk_Kind in + let r = ref Kind in fun ?find_sym ?(typ=false) k md ss env t -> Debug.(record_time Scoping (fun () -> r := scope ?find_sym ~typ k md ss env t)); !r @@ -641,19 +637,19 @@ let scope_rw_patt : sig_state -> env -> p_rw_patt -> (term, binder) rw_patt = | Rw_InTerm(t) -> Rw_InTerm(scope_pattern ss env t) | Rw_InIdInTerm(x,t) -> let v = new_var x.elt in - let t = scope_pattern ss ((x.elt,(v, mk_Kind, None))::env) t in + let t = scope_pattern ss ((x.elt,(v, Kind, None))::env) t in Rw_InIdInTerm(bind_var v t) | Rw_IdInTerm(x,t) -> let v = new_var x.elt in - let t = scope_pattern ss ((x.elt,(v, mk_Kind, None))::env) t in + let t = scope_pattern ss ((x.elt,(v, Kind, None))::env) t in Rw_IdInTerm(bind_var v t) | Rw_TermInIdInTerm(u,(x,t)) -> let u = scope_pattern ss env u in let v = new_var x.elt in - let t = scope_pattern ss ((x.elt,(v, mk_Kind, None))::env) t in + let t = scope_pattern ss ((x.elt,(v, Kind, None))::env) t in Rw_TermInIdInTerm(u, bind_var v t) | Rw_TermAsIdInTerm(u,(x,t)) -> let u = scope_pattern ss env u in let v = new_var x.elt in - let t = scope_pattern ss ((x.elt,(v, mk_Kind, None))::env) t in + let t = scope_pattern ss ((x.elt,(v, Kind, None))::env) t in Rw_TermAsIdInTerm(u, bind_var v t) diff --git a/src/parsing/syntax.ml b/src/parsing/syntax.ml index 19b4cda52..d3e0a1df0 100644 --- a/src/parsing/syntax.ml +++ b/src/parsing/syntax.ml @@ -256,7 +256,7 @@ type p_tactic_aux = | P_tac_refl | P_tac_remove of p_ident list | P_tac_repeat of p_tactic - | P_tac_rewrite of bool * p_rw_patt option * p_term + | P_tac_rewrite of Term.side * p_rw_patt option * p_term (* The boolean indicates if the equation is applied from left to right. *) | P_tac_set of p_ident * p_term | P_tac_simpl of simp_flag diff --git a/src/tool/indexing.ml b/src/tool/indexing.ml index 01ee627c8..31d9fe595 100644 --- a/src/tool/indexing.ml +++ b/src/tool/indexing.ml @@ -343,7 +343,7 @@ module DB = struct Index.dump_to ~filename:dbpath (Lazy.force !db) let locate_name name = - let k = Term.mk_Wild (* dummy, unused *) in + let k = Term.Wild (* dummy, unused *) in set_of_list ~generalize:false k (Index.locate_name (Lazy.force !db) name) @@ -369,7 +369,7 @@ let find_sym ~prt ~prv sig_state ({elt=(mp,name); pos} as s) = with Common.Error.Fatal _ -> Core.Term.create_sym mp Core.Term.Public Core.Term.Defin Core.Term.Sequen - false (Common.Pos.make pos name) None Core.Term.mk_Type [] + false (Common.Pos.make pos name) None Core.Term.Type [] module QNameMap = Map.Make(struct type t = sym_name let compare = Stdlib.compare end) @@ -424,7 +424,7 @@ let normalize typ = let search_pterm ~generalize ~mok ss env pterm = let env = - ("V#",(new_var "V#",Term.mk_Type,None))::env in + ("V#",(new_var "V#",Term.Type,None))::env in let query = Parsing.Scope.scope_search_pattern ~find_sym ~mok ss env pterm in Dream.log "QUERY before: %a" Core.Print.term query ; @@ -475,7 +475,7 @@ let subterms_to_index ~is_spine t = | Prod(t,b) -> (match where with | Spine _ -> - let t2 = subst b (Core.Term.mk_Patt (None,"dummy",[||])) in + let t2 = subst b (Core.Term.Patt (None,"dummy",[||])) in aux ~where:(enter_pi_source where) t @ aux ~where:(enter_pi_target ~is_prod:(Core.Term.is_prod t2) where) t2 @@ -524,7 +524,7 @@ let index_rule sym ({Core.Term.lhs=lhsargs ; rule_pos ; _} as rule) = I leave the assert false to detect when it happens and let the team decide what to do *) | Some pos -> pos in - let lhs = Core.Term.add_args (Core.Term.mk_Symb sym) lhsargs in + let lhs = Core.Term.add_args (Core.Term.Symb sym) lhsargs in let rhs = rule.rhs in let get_inside = function | DB.Conclusion ins -> ins | _ -> assert false in let filename = Option.get rule_pos.fname in diff --git a/src/tool/lcr.ml b/src/tool/lcr.ml index 9e8e2d273..9996ae664 100644 --- a/src/tool/lcr.ml +++ b/src/tool/lcr.ml @@ -67,14 +67,14 @@ let replace : term -> subterm_pos -> term -> term = fun t p u -> | [] -> u | 0::p -> begin match unfold t with - | Appl(a,b) -> mk_Appl (replace a p, b) - | Abst(a,b) -> mk_Abst (replace a p, b) - | Prod(a,b) -> mk_Prod (replace a p, b) + | Appl(a,b) -> Appl (replace a p, b) + | Abst(a,b) -> Abst (replace a p, b) + | Prod(a,b) -> Prod (replace a p, b) | _ -> assert false end | 1::p -> begin match unfold t with - | Appl(a,b) -> mk_Appl (a, replace b p) + | Appl(a,b) -> Appl (a, replace b p) | _ -> assert false end | _ -> assert false @@ -109,14 +109,14 @@ let rec shift : term -> term = fun t -> | Wild | Plac _ | TRef _ -> t - | Prod(a,b) -> mk_Prod (shift a, shift_binder b) - | Abst(a,b) -> mk_Abst (shift a, shift_binder b) - | Appl(a,b) -> mk_Appl (shift a, shift b) - | Meta(m,ts) -> mk_Meta (m, Array.map shift ts) + | Prod(a,b) -> Prod (shift a, shift_binder b) + | Abst(a,b) -> Abst (shift a, shift_binder b) + | Appl(a,b) -> Appl (shift a, shift b) + | Meta(m,ts) -> Meta (m, Array.map shift ts) | Patt(None,_,_) -> assert false - | Patt(Some i,n,ts) -> mk_Patt (Some(-i-1), n ^ "'", Array.map shift ts) + | Patt(Some i,n,ts) -> Patt (Some(-i-1), n ^ "'", Array.map shift ts) | Bvar _ -> assert false - | LLet(a,t,b) -> mk_LLet (shift a, shift t, shift_binder b) + | LLet(a,t,b) -> LLet (shift a, shift t, shift_binder b) and shift_binder b = let x, t = unbind b in bind_var x (shift t) @@ -136,19 +136,19 @@ let apply_subs : subs -> term -> term = fun s t -> | Patt(None, _, _) -> assert false | Patt(Some i,_,[||]) -> begin try IntMap.find i s with Not_found -> t end - | Patt(i,n,ts) -> mk_Patt (i, n, Array.map apply_subs ts) + | Patt(i,n,ts) -> Patt (i, n, Array.map apply_subs ts) | Vari _ | Symb _ | Type | Kind -> t - | Appl(u,v) -> mk_Appl (apply_subs u, apply_subs v) + | Appl(u,v) -> Appl (apply_subs u, apply_subs v) | Abst(a,b) -> let x,b = unbind b in - mk_Abst (apply_subs a, bind_var x (apply_subs b)) + Abst (apply_subs a, bind_var x (apply_subs b)) | Prod(a,b) -> let x,b = unbind b in - mk_Prod (apply_subs a, bind_var x (apply_subs b)) + Prod (apply_subs a, bind_var x (apply_subs b)) | LLet(a,t,b) -> let x,b = unbind b in - mk_LLet (apply_subs a, apply_subs t, bind_var x (apply_subs b)) - | Meta(m,ts) -> mk_Meta (m, Array.map apply_subs ts) + LLet (apply_subs a, apply_subs t, bind_var x (apply_subs b)) + | Meta(m,ts) -> Meta (m, Array.map apply_subs ts) | Bvar _ -> assert false | TRef _ -> assert false | Wild -> assert false @@ -237,7 +237,7 @@ let unif : Pos.popt -> term -> term -> term IntMap.t option = | Abst(a,b), Abst(c,d) | Prod(a,b), Prod(c,d) -> let x,b = unbind b in - let d = subst d (mk_Vari x) in + let d = subst d (Vari x) in unif s ((a,c)::(b,d)::l) | Vari x, Vari y -> if eq_vars x y then unif s l else raise NotUnifiable @@ -266,17 +266,16 @@ let unif : Pos.popt -> term -> term -> term IntMap.t option = (* Unit tests. *) let _ = - let var i = mk_Patt (Some i, string_of_int i, [||]) in + let var i = Patt (Some i, string_of_int i, [||]) in let v0 = var 0 and v1 = var 1 in let sym name = - create_sym [] Public Defin Eager false (Pos.none name) None - mk_Type [] in + create_sym [] Public Defin Eager false (Pos.none name) None Type [] in let a_ = sym "a" and b_ = sym "b" and s_ = sym "s" and f_ = sym "f" in - let app s ts = add_args (mk_Symb s) ts in + let app s ts = add_args (Symb s) ts in let a = app a_ [] and b = app b_ [] and s t = app s_ [t] @@ -401,16 +400,16 @@ let typability_constraints : Pos.popt -> term -> subs option = fun pos t -> match IntMap.find_opt i !p2m with | Some m -> m | None -> - let m_typ = LibMeta.fresh p mk_Type 0 in - let typ = mk_Meta(m_typ,[||]) in + let m_typ = LibMeta.fresh p Type 0 in + let typ = Meta(m_typ,[||]) in let m = LibMeta.fresh p typ 0 in p2m := IntMap.add i m !p2m; m2p := MetaMap.add m (i,n) !m2p; m - in mk_Meta(m,[||]) - | Appl(a,b) -> mk_Appl_not_canonical(patt_to_meta a, patt_to_meta b) + in Meta(m,[||]) + | Appl(a,b) -> Appl(patt_to_meta a, patt_to_meta b) | Symb _ | Vari _ -> t | Abst(a,b) -> let x,b = unbind b in - mk_Abst(patt_to_meta a, bind_var x (patt_to_meta b)) + Abst(patt_to_meta a, bind_var x (patt_to_meta b)) | _ -> assert false in let t = patt_to_meta t in @@ -423,8 +422,8 @@ let typability_constraints : Pos.popt -> term -> subs option = fun pos t -> try let i,n = MetaMap.find m !m2p in let s = create_sym (Sign.current_path()) - Public Defin Eager false (Pos.none n) None mk_Kind [] in - let t = bind_mvar [||] (mk_Symb s) in + Public Defin Eager false (Pos.none n) None Kind [] in + let t = bind_mvar [||] (Symb s) in Timed.(m.meta_value := Some t); s2p := SymMap.add s i !s2p with Not_found -> () @@ -442,10 +441,10 @@ let typability_constraints : Pos.popt -> term -> subs option = fun pos t -> match unfold t with | Symb s -> begin match SymMap.find_opt s !s2p with - | Some i -> mk_Patt(Some i, s.sym_name, [||]) + | Some i -> Patt(Some i, s.sym_name, [||]) | None -> t end - | Appl(a,b) -> mk_Appl_not_canonical(sym_to_patt a, sym_to_patt b) + | Appl(a,b) -> Appl(sym_to_patt a, sym_to_patt b) | _ -> t in (* Function converting a pair of terms into a rule, if possible. *) @@ -564,7 +563,7 @@ let check_cps_subterms_eq : Pos.popt -> sym_rule -> unit = match !(s.sym_def) with | Some d -> let j = match s.sym_pos with Some p -> p | None -> assert false in - cp_cand_fun check_cp pos i l r p l_p j (mk_Symb s) d + cp_cand_fun check_cp pos i l r p l_p j (Symb s) d (*FIXME? what if s is applied to some arguments? *) | None -> let h y = diff --git a/src/tool/sr.ml b/src/tool/sr.ml index 7bdec9131..6e7cb719e 100644 --- a/src/tool/sr.ml +++ b/src/tool/sr.ml @@ -18,19 +18,19 @@ let build_meta_type : problem -> int -> term = fun p k -> let xs = Array.init k (new_var_ind "x") in let ts = Array.map mk_Vari xs in (* We create the types for the “Mi” metavariables. *) - let ty_m = Array.make (k+1) mk_Type in + let ty_m = Array.make (k+1) Type in for i = 0 to k do for j = (i-1) downto 0 do - ty_m.(i) <- mk_Prod (ty_m.(j), bind_var xs.(j) ty_m.(i)) + ty_m.(i) <- Prod (ty_m.(j), bind_var xs.(j) ty_m.(i)) done done; (* We create the “Ai” terms and the “Mi” metavariables. *) - let f i = mk_Meta (LibMeta.fresh p ty_m.(i) i, Array.sub ts 0 i) in + let f i = Meta (LibMeta.fresh p ty_m.(i) i, Array.sub ts 0 i) in let a = Array.init (k+1) f in (* We finally construct our type. *) let res = ref a.(k) in for i = k - 1 downto 0 do - res := mk_Prod (a.(i), bind_var xs.(i) !res) + res := Prod (a.(i), bind_var xs.(i) !res) done; !res @@ -54,24 +54,24 @@ let symb_to_patt : Pos.popt -> int option SymMap.t -> string array Please contact the developers." f.sym_name | Some(Some(i)) -> let (ts1, ts2) = List.cut ts arities.(i) in - (mk_Patt (Some i, names.(i), Array.of_list ts1), ts2) - | None -> (mk_Symb f, ts) + (Patt (Some i, names.(i), Array.of_list ts1), ts2) + | None -> (Symb f, ts) end - | Vari(x) -> (mk_Vari x, ts) - | Type -> (mk_Type , ts) - | Kind -> (mk_Kind , ts) + | Vari(x) -> (Vari x, ts) + | Type -> (Type , ts) + | Kind -> (Kind , ts) | Abst(a,b) -> let (x, t) = unbind b in let b = bind_var x (symb_to_patt t) in - (mk_Abst (symb_to_patt a, b), ts) + (Abst (symb_to_patt a, b), ts) | Prod(a,b) -> let (x, t) = unbind b in let b = bind_var x (symb_to_patt t) in - (mk_Prod (symb_to_patt a, b), ts) + (Prod (symb_to_patt a, b), ts) | LLet(a,t,b) -> let (x, u) = unbind b in let b = bind_var x (symb_to_patt u) in - (mk_LLet (symb_to_patt a, symb_to_patt t, b), ts) + (LLet (symb_to_patt a, symb_to_patt t, b), ts) | Meta(_,_) -> fatal pos "A metavariable could not be instantiated in the RHS." | Plac _ -> @@ -107,10 +107,10 @@ let check_rule : Pos.popt -> sym_rule -> sym_rule = let f m = let xs = Array.init m.meta_arity (new_var_ind "x") in let ts = Array.map mk_Vari xs in - Some(bind_mvar xs (mk_Meta (m, ts))) + Some(bind_mvar xs (Meta (m, ts))) in let su = Array.map f metas in - let lhs_with_metas = subst_patt su (add_args (mk_Symb s) lhs) + let lhs_with_metas = subst_patt su (add_args (Symb s) lhs) and rhs_with_metas = subst_patt su rhs in if Logger.log_enabled () then log_subj "replace pattern variables by metavariables:@ %a ↪ %a" @@ -144,8 +144,8 @@ let check_rule : Pos.popt -> sym_rule -> sym_rule = in Stdlib.(map := SymMap.add s None !map; m2s := MetaMap.add m s !m2s); let xs = Array.init m.meta_arity (new_var_ind "x") in - let s = mk_Symb s in - let def = Array.fold_left (fun t x -> mk_Appl (t, mk_Vari x)) s xs in + let s = Symb s in + let def = Array.fold_left (fun t x -> Appl (t, Vari x)) s xs in m.meta_value := Some(bind_mvar xs def) in MetaSet.iter instantiate !p.metas; @@ -195,7 +195,7 @@ let check_rule : Pos.popt -> sym_rule -> sym_rule = let is_inst ((_c1,t1,u1) as x1) ((_c2,t2,u2) as x2) = if Logger.log_enabled() then log_subj "is_inst [%a] [%a]" constr x1 constr x2; - let cons t u = add_args (mk_Symb Unif_rule.equiv) [t; u] in + let cons t u = add_args (Symb Unif_rule.equiv) [t; u] in matches (cons t1 u1) (cons t2 u2) || matches (cons t1 u1) (cons u2 t2) in let is_lhs_constr rc = List.exists (fun lc -> is_inst lc rc) lhs_constrs in diff --git a/tests/OK/1001.lp b/tests/OK/1001.lp index dba998acd..eb09d82eb 100644 --- a/tests/OK/1001.lp +++ b/tests/OK/1001.lp @@ -1,3 +1,3 @@ constant symbol A : TYPE; -associative commutative symbol * : A → A → A; +right associative commutative symbol * : A → A → A; diff --git a/tests/OK/991.lp b/tests/OK/991.lp index 1ad41d8e2..1a85f8292 100644 --- a/tests/OK/991.lp +++ b/tests/OK/991.lp @@ -1,6 +1,6 @@ symbol Prop:TYPE; symbol -:Prop → Prop; notation - prefix 10; -associative commutative symbol +: Prop → Prop → Prop; notation + infix right 5; +right associative commutative symbol +: Prop → Prop → Prop; notation + infix right 5; injective symbol π:Prop → TYPE; symbol resolution x a b : π (x + a) → π (- x + b) → π (a + b); opaque symbol test a b c d e : diff --git a/tests/OK/Comp.lp b/tests/OK/Comp.lp new file mode 100644 index 000000000..f832987ad --- /dev/null +++ b/tests/OK/Comp.lp @@ -0,0 +1,74 @@ +/* Comparison datatype + +By Quentin Garchery (May 2021). */ + +require open tests.OK.Set tests.OK.Prop tests.OK.FOL tests.OK.Eq tests.OK.Bool; + +inductive Comp : TYPE ≔ +| Eq : Comp +| Lt : Comp +| Gt : Comp; + +// set code for Comp + +constant symbol comp : Set; + +rule τ comp ↪ Comp; + +// Boolean functions for testing head constructor + +symbol isEq : Comp → 𝔹; + +rule isEq Eq ↪ true +with isEq Lt ↪ false +with isEq Gt ↪ false; + +symbol isLt : Comp → 𝔹; + +rule isLt Eq ↪ false +with isLt Lt ↪ true +with isLt Gt ↪ false; + +symbol isGt : Comp → 𝔹; + +rule isGt Eq ↪ false +with isGt Lt ↪ false +with isGt Gt ↪ true; + +// Discriminate constructors + +symbol Lt≠Eq : π (Lt ≠ Eq) ≔ +begin + assume h; refine ind_eq h (λ n, istrue(isEq n)) ⊤ᵢ +end; + +symbol Gt≠Eq : π (Gt ≠ Eq) ≔ +begin + assume h; refine ind_eq h (λ n, istrue(isEq n)) ⊤ᵢ +end; + +symbol Gt≠Lt : π (Gt ≠ Lt) ≔ +begin + assume h; refine ind_eq h (λ n, istrue(isLt n)) ⊤ᵢ +end; + +// Opposite of a Comp + +symbol opp : Comp → Comp; + +rule opp Eq ↪ Eq +with opp Lt ↪ Gt +with opp Gt ↪ Lt; + +symbol opp_idem c : π (opp (opp c) = c) ≔ +begin + induction { reflexivity; } { reflexivity; } { reflexivity; } +end; + +// Conditional + +symbol case_Comp [A] : Comp → τ A → τ A → τ A → τ A; + +rule case_Comp Eq $x _ _ ↪ $x +with case_Comp Lt _ $x _ ↪ $x +with case_Comp Gt _ _ $x ↪ $x; diff --git a/tests/OK/Pos.lp b/tests/OK/Pos.lp new file mode 100644 index 000000000..b42d95a44 --- /dev/null +++ b/tests/OK/Pos.lp @@ -0,0 +1,584 @@ +/* Positive binary integers + +by Quentin Garchery (May 2021). */ + +require open tests.OK.Set tests.OK.Prop tests.OK.FOL tests.OK.Eq + tests.OK.Nat tests.OK.Bool tests.OK.Comp; + +inductive ℙ : TYPE ≔ +| I : ℙ → ℙ +| O : ℙ → ℙ +| H : ℙ; + +// set code for ℙ + +constant symbol pos : Set; + +rule τ pos ↪ ℙ; + +// boolean functions for testing head constructor + +symbol isI : ℙ → 𝔹; + +rule isI (I _) ↪ true +with isI (O _) ↪ false +with isI H ↪ false; + +symbol isO : ℙ → 𝔹; + +rule isO (I _) ↪ false +with isO (O _) ↪ true +with isO H ↪ false; + +symbol isH : ℙ → 𝔹; + +rule isH (I _) ↪ false +with isH (O _) ↪ false +with isH H ↪ true; + +// Discriminate constructors + +symbol I≠H [x] : π (I x ≠ H) ≔ +begin + assume x h; refine ind_eq h (λ x, istrue(isH x)) ⊤ᵢ; +end; + +symbol O≠H [x] : π (O x ≠ H) ≔ +begin + assume x h; refine ind_eq h (λ x, istrue(isH x)) ⊤ᵢ; +end; + +symbol I≠O [x y] : π (I x ≠ O y) ≔ +begin + assume x y h; refine ind_eq h (λ x, istrue(isO x)) ⊤ᵢ; +end; + +opaque symbol caseH x : π(x = H ∨ x ≠ H) ≔ +begin + induction + { assume x h; apply ∨ᵢ₂; refine I≠H } + { assume x h; apply ∨ᵢ₂; refine O≠H } + { apply ∨ᵢ₁; reflexivity } +end; + +// Constructors are injective + +symbol projO : ℙ → ℙ; + +rule projO (O $x) ↪ $x +with projO (I $x) ↪ I $x +with projO H ↪ H; + +opaque symbol O_inj p q : π(O p = O q) → π(p = q) ≔ +begin + assume p q h; apply feq projO h +end; + +symbol projI : ℙ → ℙ; + +rule projI (I $x) ↪ $x +with projI (O $x) ↪ O $x +with projI H ↪ H; + +opaque symbol I_inj p q : π(I p = I q) → π(p = q) ≔ +begin + assume p q h; apply feq projI h +end; + +// Successor function + +symbol succ : ℙ → ℙ; + +rule succ (I $x) ↪ O (succ $x) +with succ (O $x) ↪ I $x +with succ H ↪ O H; + +// Interpretation of ℙ in ℕ + +symbol val : ℙ → ℕ; + +rule val H ↪ 1 +with val (O $x) ↪ 2 * val $x +with val (I $x) ↪ val (O $x) +1; + +assert ⊢ val (O (I H)) ≡ 6; + +opaque symbol valS x : π(val (succ x) = val x +1) ≔ +begin + induction + { assume x h; simplify; rewrite h; reflexivity } + { assume x h; reflexivity } + { reflexivity } +end; + +opaque symbol val_surj [n] : π(n ≠ 0 ⇒ `∃ x, val x = n) ≔ +begin + induction + { assume h; apply ⊥ₑ; apply h; reflexivity } + { assume n h i; apply ∨ₑ (casen n) + { assume j; apply ∃ᵢ H; rewrite j; reflexivity } + { assume j; apply ∃ₑ (h j); assume p k; apply ∃ᵢ (succ p); + rewrite left k; apply valS p /*FIXME*/ } + } +end; + +opaque symbol val≠0 x : π(val x ≠ 0) ≔ +begin + induction + { assume x h; refine s≠0 } + { assume x h; simplify; assume i; + apply h (∧ₑ₁ (∧ₑ₁ (addn_eq0 (val x) (val x)) i)) + } + { refine s≠0 } +end; + +opaque symbol 2*val≠0 x : π(val x + val x ≠ 0) ≔ +begin + assume x h; apply ⊥ₑ; apply val≠0 x; apply 2*=0; apply h +end; + +opaque symbol val_inj [x y] : π(val x = val y) → π(x = y) ≔ +begin + induction + { assume x h; induction + { simplify; assume y i j; rewrite h y _ + { apply 2*_inj; apply +1_inj; apply j } + { reflexivity } + } + { simplify; assume y i j; apply ⊥ₑ; apply odd≠even (val x) (val y) j } + { simplify; assume i; apply ⊥ₑ; apply 2*val≠0 x; apply +1_inj; apply i } + } + { assume x h; induction + { simplify; assume y i j; apply ⊥ₑ; + apply odd≠even (val y) (val x) (eq_sym j) } + { simplify; assume y i j; apply feq O; apply h; apply 2*_inj; apply j } + { assume i; apply ⊥ₑ; apply odd≠even 0 (val x); symmetry; apply i } + } + { induction + { simplify; assume x h i; apply ⊥ₑ; apply val≠0 x; apply 2*=0; apply +1_inj; + symmetry; apply i } + { simplify; assume x h i; apply ⊥ₑ; apply odd≠even 0 (val x); apply i } + { reflexivity } + } +end; + +// ℕ-like Induction Principle + +symbol ind_ℙeano p : π (p H) → (Π x, π (p x) → π (p (succ x))) → Π x, π (p x) ≔ +begin + assume p pH psucc; + have i: π(`∀ n, `∀ x, val x = n ⇒ p x) { + induction + { induction + { assume x h i; apply ⊥ₑ (s≠0 i) } + { assume x h i; apply ⊥ₑ (val≠0 (O x) i) } + { assume i; apply ⊥ₑ (s≠0 i) } + } + { assume n h x; apply ∨ₑ (casen n) + { assume i; rewrite i; assume j; + have k: π(x = H) { apply val_inj; apply j }; + rewrite k; apply pH + } + { assume i; apply ∃ₑ (val_surj i); assume y j; rewrite left j; + rewrite left valS; assume k; have l: π(x = succ y) { apply val_inj k }; + rewrite l; apply psucc y; apply h; apply j + } + } + }; + assume x; apply i (val x); reflexivity +end; + +// Addition of ℙ numbers with and without a carry + +symbol add : ℙ → ℙ → ℙ; +symbol add_carry : ℙ → ℙ → ℙ; + +rule add (I $x) (I $q) ↪ O (add_carry $x $q) +with add (I $x) (O $q) ↪ I (add $x $q) +with add (O $x) (I $q) ↪ I (add $x $q) +with add (O $x) (O $q) ↪ O (add $x $q) +with add $x H ↪ succ $x +with add H $y ↪ succ $y; + +rule add_carry (I $x) (I $q) ↪ I (add_carry $x $q) +with add_carry (I $x) (O $q) ↪ O (add_carry $x $q) +with add_carry (O $x) (I $q) ↪ O (add_carry $x $q) +with add_carry (O $x) (O $q) ↪ I (add $x $q) +with add_carry $x H ↪ add $x (O H) +with add_carry H $y ↪ add (O H) $y; +// for efficiency reasons last cases should not be 'succ (succ $x)' + +// Check that 7 + 5 = 12 +assert ⊢ add (I (I H)) (I (O H)) ≡ O (O (I H)); +// Check that 110101010 + 101101100 ≡ 1100010110 in base 2 (426 + 364 ≡ 790) +assert ⊢ add (O (I (O (I (O (I (O (I H)))))))) + (O (O (I (I (O (I (I (O H)))))))) + ≡ (O (I (I (O (I (O (O (O (I H))))))))); + +// Interaction of succ and add + +symbol succ_add x y : π (succ (add x y) = add_carry x y) ≔ +begin + induction + // case I + { assume p prec; + induction + { reflexivity } + { assume q h; simplify; rewrite prec; reflexivity } + { reflexivity } } + // case O + { assume p prec; + induction + { assume q h; simplify; rewrite prec; reflexivity } + { reflexivity } + { reflexivity } } + // case H + { induction { reflexivity } { reflexivity } { reflexivity } } +end; + +symbol add_succ x y : π (add (succ x) y = succ (add x y)) ≔ +begin + induction + // case I + { assume p prec; + induction + { assume q h; simplify; rewrite prec; rewrite succ_add; reflexivity } + { assume q h; simplify; rewrite prec; reflexivity } + { reflexivity } } + // case O + { assume p prec; + induction + { assume q h; simplify; rewrite succ_add; reflexivity } + { reflexivity } + { reflexivity } } + // case H + { induction { reflexivity } { reflexivity } { reflexivity } } +end; + +symbol add_succ_right x y : π (add x (succ y) = succ (add x y)) ≔ +begin + refine ind_ℙeano (λ x, `∀ y, add x (succ y) = succ (add x y)) _ _ + // case H + { reflexivity } + // case succ + { assume x xrec y; + rewrite add_succ; rewrite add_succ; rewrite xrec; reflexivity } +end; + +// Associativity of the addition + +symbol add_assoc x y z : π (add (add x y) z = add x (add y z)) ≔ +begin + refine ind_ℙeano (λ x, `∀ y, `∀ z, add (add x y) z = add x (add y z)) _ _ + // case H + { refine add_succ } + // case succ + { assume x xrec y z; + rewrite add_succ; rewrite add_succ; rewrite add_succ; + rewrite xrec; reflexivity } +end; + +// Commutativity of the addition + +symbol add_com x y : π (add x y = add y x) ≔ +begin + refine ind_ℙeano (λ x, `∀ y, add x y = add y x) _ _ + // case H + { reflexivity } + // case succ + { assume x xrec y; + rewrite add_succ; rewrite add_succ_right; rewrite xrec; reflexivity } +end; + +// function λ x, 2 * x - 1 + +symbol pos_pred_double : ℙ → ℙ; + +rule pos_pred_double (I $x) ↪ I (O $x) +with pos_pred_double (O $x) ↪ I (pos_pred_double $x) +with pos_pred_double H ↪ H; + +symbol pos_pred_double_succ x : π (pos_pred_double (succ x) = I x) ≔ +begin + induction + { assume x xrec; simplify; rewrite xrec; reflexivity } + { reflexivity } + { reflexivity } +end; + +symbol succ_pos_pred_double x : π (succ (pos_pred_double x) = O x) ≔ +begin + induction + { reflexivity } + { assume x xrec; simplify; rewrite xrec; reflexivity } + { reflexivity } +end; + +// Comparison of ℙ numbers + +symbol compare_acc : ℙ → Comp → ℙ → Comp; + +rule compare_acc (I $x) $c (I $q) ↪ compare_acc $x $c $q +with compare_acc (I $x) _ (O $q) ↪ compare_acc $x Gt $q +with compare_acc (I _) _ H ↪ Gt +with compare_acc (O $x) _ (I $q) ↪ compare_acc $x Lt $q +with compare_acc (O $x) $c (O $q) ↪ compare_acc $x $c $q +with compare_acc (O _) _ H ↪ Gt +with compare_acc H _ (I _) ↪ Lt +with compare_acc H _ (O _) ↪ Lt +with compare_acc H $c H ↪ $c; + +symbol compare x y ≔ compare_acc x Eq y; + +// Commutative property of compare + +symbol compare_acc_com x y c : + π (compare_acc y c x = opp (compare_acc x (opp c) y)) ≔ +begin + induction + // case I + { assume x xrec; + induction + { assume y h c; simplify; rewrite xrec; reflexivity } + { assume y h c; simplify; rewrite xrec; reflexivity } + { reflexivity } } + // case O + { assume x xrec; + induction + { assume y h c; simplify; rewrite xrec; reflexivity } + { assume y h c; simplify; rewrite xrec; reflexivity } + { reflexivity } } + // case H + { induction + { reflexivity } + { reflexivity } + { assume c; simplify; rewrite opp_idem; reflexivity } } +end; + +symbol compare_com x y : π (compare y x = opp (compare x y)) ≔ +begin + assume x y; refine compare_acc_com x y Eq; +end; + +// Compare decides the equality + +symbol compare_acc_nEq x y c : π (c ≠ Eq ⇒ compare_acc x c y ≠ Eq) ≔ +begin + induction + // case I + { assume x xrec; + induction + { assume y h c H; refine xrec y c H } + { assume y h c H; refine xrec y Gt _; refine Gt≠Eq } + { assume c h; refine Gt≠Eq } } + // case O + { assume x xrec; + induction + { assume y h c H; refine xrec y Lt _; refine Lt≠Eq } + { assume y h c H; refine xrec y c H } + { assume c h; refine Gt≠Eq } } + // case H + { induction + { assume y h c H; refine Lt≠Eq } + { assume y h c H; refine Lt≠Eq } + { assume c Hc; refine Hc } } +end; + +symbol compare_decides x y : π (compare x y = Eq ⇒ x = y) ≔ +begin + induction + // case I + { assume x xrec; + induction + { assume y h H; rewrite xrec y H; reflexivity } + { assume y h H; apply ⊥ₑ; refine compare_acc_nEq x y Gt _ H; refine Gt≠Eq } + { assume H; apply ⊥ₑ; refine Gt≠Eq H } } + // case O + { assume x xrec; + induction + { assume y h H; apply ⊥ₑ; refine compare_acc_nEq x y Lt _ H; refine Lt≠Eq } + { assume y h H; rewrite xrec y H; reflexivity } + { assume H; apply ⊥ₑ; refine Gt≠Eq H } } + // case H + { induction + { assume y h H; apply ⊥ₑ; refine Lt≠Eq H } + { assume y h H; apply ⊥ₑ; refine Lt≠Eq H } + { reflexivity } } +end; + +// Compare with Gt or Lt + +symbol compare_Lt x y : + π (compare_acc x Lt y = case_Comp (compare x y) Lt Lt Gt) ≔ +begin + induction + // case I + { assume x xrec; + induction + { assume y h; refine xrec y } + { assume y h; simplify; + refine ind_Comp (λ c, compare_acc x Gt y = c ⇒ c = case_Comp c Lt Lt Gt) _ _ _ (compare_acc x Gt y) _ + { assume H; apply ⊥ₑ; refine compare_acc_nEq x y Gt _ H } + { refine Gt≠Eq } + { reflexivity } + { reflexivity } } + { reflexivity; reflexivity } } + // case O + { assume x xrec; + induction + { assume y h; simplify; + refine ind_Comp (λ c, compare_acc x Lt y = c ⇒ c = case_Comp c Lt Lt Gt) _ _ _ (compare_acc x Lt y) _ + { assume H; apply ⊥ₑ; refine compare_acc_nEq x y Lt _ H } + { refine Lt≠Eq } + { reflexivity } + { reflexivity } } + { reflexivity } + { assume y h; refine xrec y; + reflexivity } } + // case H + { induction { reflexivity } { reflexivity } { reflexivity } } +end; + +symbol compare_Gt x y : + π (compare_acc x Gt y = case_Comp (compare x y) Gt Lt Gt) ≔ +begin + induction + // case I + { assume x xrec; + induction + { assume y h; refine xrec y } + { assume y h; simplify; + refine ind_Comp (λ c, compare_acc x Gt y = c ⇒ c = case_Comp c Gt Lt Gt) _ _ _ (compare_acc x Gt y) _ + { assume H; apply ⊥ₑ; refine compare_acc_nEq x y Gt _ H } + { refine Gt≠Eq } + { reflexivity } + { reflexivity } } + { reflexivity; reflexivity } } + // case O + { assume x xrec; + induction + { assume y h; simplify; + refine ind_Comp (λ c, compare_acc x Lt y = c ⇒ c = case_Comp c Gt Lt Gt) _ _ _ (compare_acc x Lt y) _ + { assume H; apply ⊥ₑ; refine compare_acc_nEq x y Lt _ H } + { refine Lt≠Eq } + { reflexivity } + { reflexivity } } + { reflexivity; assume y h; refine xrec y } + { reflexivity } } + // case H + { induction { reflexivity } { reflexivity } { reflexivity } } +end; + +// Compatibility of compare with the addition + +symbol compare_H_Lt y : π (compare_acc H Lt y = Lt) ≔ +begin + induction { reflexivity } { reflexivity } { reflexivity } +end; + +symbol compare_Gt_H x : π (compare_acc x Gt H = Gt) ≔ +begin + induction { reflexivity } { reflexivity } { reflexivity } +end; + +symbol compare_H_succ y c : π (compare_acc H c (succ y) = Lt) ≔ +begin + induction { reflexivity } { reflexivity } { reflexivity } +end; + +symbol compare_succ_H x c : π (compare_acc (succ x) c H = Gt) ≔ +begin + induction { reflexivity } { reflexivity } { reflexivity } +end; + +symbol compare_succ_Lt x y : + π (compare_acc (succ x) Lt y = compare_acc x Gt y) ≔ +begin + induction + // case I + { assume x xrec; + induction + { assume y h; refine xrec y } + { assume y h; refine xrec y } + { reflexivity } } + // case O + { assume x xrec; + induction { reflexivity } { reflexivity } { reflexivity } } + // case H + { induction + { assume y h; refine compare_H_Lt y } + { assume y h; refine compare_H_Lt y } + { reflexivity } } +end; + +symbol compare_Gt_succ x y : + π (compare_acc x Gt (succ y) = compare_acc x Lt y) ≔ +begin + assume x y; + rewrite compare_acc_com; rewrite .[u in _ = u] compare_acc_com; + simplify; rewrite compare_succ_Lt; reflexivity; +end; + +symbol compare_succ_succ x y c : + π (compare_acc (succ x) c (succ y) = compare_acc x c y) ≔ +begin + induction + // case I + { assume x xrec; + induction + { assume y h c; refine xrec y c } + { assume y h c; simplify; refine compare_succ_Lt x y } + { assume c; simplify; refine compare_succ_H x c } } + // case O + { assume x xrec; + induction + { assume y h c; simplify; refine compare_Gt_succ x y } + { assume y h c; reflexivity } + { assume c; simplify; refine compare_Gt_H x } } + // case H + { induction + { assume y h c; simplify; refine compare_H_succ y c } + { assume y h c; simplify; refine compare_H_Lt y } + { reflexivity } } +end; + +symbol compare_compat_add a x y : + π (compare (add x a) (add y a) = compare x y) ≔ +begin + refine ind_ℙeano (λ a, `∀ x, `∀ y, compare (add x a) (add y a) = compare x y) _ _ + // case H + { assume x y; refine compare_succ_succ x y Eq } + // case succ + { assume a arec x y; + rewrite add_succ_right; rewrite add_succ_right; rewrite left arec x y; + simplify; rewrite compare_succ_succ; reflexivity } +end; + +// Multiplication + +symbol mul : ℙ → ℙ → ℙ; + +rule mul (I $x) $y ↪ add $x (O (mul $x $y)) +with mul (O $x) $y ↪ O (mul $x $y) +with mul H $y ↪ $y; + +// shortcuts + +symbol _1 ≔ H; +symbol _2 ≔ O H; +symbol _3 ≔ I H; +symbol _4 ≔ O (O H); +symbol _5 ≔ I (O H); +symbol _6 ≔ O (I H); +symbol _7 ≔ I (I H); +symbol _8 ≔ O (O (O H)); +symbol _9 ≔ I (O (O H)); +symbol _10 ≔ O (I (O H)); + +// enable printing of natural numbers in decimal notation + +builtin "pos_one" ≔ H; +builtin "pos_double" ≔ O; +builtin "pos_succ_double" ≔ I; + +compute add _2 _2; diff --git a/tests/OK/Z.lp b/tests/OK/Z.lp new file mode 100644 index 000000000..171ddbc77 --- /dev/null +++ b/tests/OK/Z.lp @@ -0,0 +1,697 @@ +/* Binary integers + +by Quentin Garchery (May 2021). */ + +require open tests.OK.Set tests.OK.Prop tests.OK.FOL tests.OK.Eq tests.OK.Pos + tests.OK.Bool; + +inductive ℤ : TYPE ≔ // \BbbZ +| Z0 : ℤ +| Zpos : ℙ → ℤ +| Zneg : ℙ → ℤ; + +// set code for ℤ + +constant symbol int : Set; + +rule τ int ↪ ℤ; + +// boolean functions for testing head constructor + +symbol isZ0 : ℤ → 𝔹; + +rule isZ0 Z0 ↪ true +with isZ0 (Zpos _) ↪ false +with isZ0 (Zneg _) ↪ false; + +symbol isZpos : ℤ → 𝔹; + +rule isZpos Z0 ↪ false +with isZpos (Zpos _) ↪ true +with isZpos (Zneg _) ↪ false; + +symbol isZneg : ℤ → 𝔹; + +rule isZneg Z0 ↪ false +with isZneg (Zpos _) ↪ false +with isZneg (Zneg _) ↪ true; + +// Discriminate constructors + +symbol Zpos≠Z0 p : π (Zpos p ≠ Z0) ≔ +begin + assume n h; refine ind_eq h (λ n, istrue(isZ0 n)) ⊤ᵢ +end; + +symbol Zneg≠Z0 p : π (Zneg p ≠ Z0) ≔ +begin + assume n h; refine ind_eq h (λ n, istrue(isZ0 n)) ⊤ᵢ +end; + +symbol Zpos≠Zneg p q : π (Zpos p ≠ Zneg q) ≔ +begin + assume x y h; refine ind_eq h (λ n, istrue(isZneg n)) ⊤ᵢ +end; + +// Unary opposite + +symbol — : ℤ → ℤ; +notation — prefix 24; + +rule — Z0 ↪ Z0 +with — (Zpos $p) ↪ Zneg $p +with — (Zneg $p) ↪ Zpos $p; + +symbol —_idem z : π (— — z = z) ≔ +begin + induction { reflexivity } { reflexivity } { reflexivity } +end; + +// Doubling functions + +symbol double : ℤ → ℤ; + +rule double Z0 ↪ Z0 +with double (Zpos $p) ↪ Zpos (O $p) +with double (Zneg $p) ↪ Zneg (O $p); + +symbol succ_double : ℤ → ℤ; + +rule succ_double Z0 ↪ Zpos H +with succ_double (Zpos $p) ↪ Zpos (I $p) +with succ_double (Zneg $p) ↪ Zneg (pos_pred_double $p); + +symbol pred_double : ℤ → ℤ; + +rule pred_double Z0 ↪ Zneg H +with pred_double (Zpos $p) ↪ Zpos (pos_pred_double $p) +with pred_double (Zneg $p) ↪ Zneg (I $p); + +// Interaction of opp and doubling functions + +symbol double_opp z : π (double (— z) = — double z) ≔ +begin + induction { reflexivity } { reflexivity } { reflexivity } +end; + +symbol succ_double_opp z : π (succ_double (— z) = — pred_double z) ≔ +begin + induction { reflexivity } { reflexivity } { reflexivity } +end; + +symbol pred_double_opp z : π (pred_double (— z) = — succ_double z) ≔ +begin + induction { reflexivity } { reflexivity } { reflexivity } +end; + +// Binary negation on ℙ + +symbol sub : ℙ → ℙ → ℤ; + +rule sub (I $p) (I $q) ↪ double (sub $p $q) +with sub (I $p) (O $q) ↪ succ_double (sub $p $q) +with sub (I $p) H ↪ Zpos (O $p) +with sub (O $p) (I $q) ↪ pred_double (sub $p $q) +with sub (O $p) (O $q) ↪ double (sub $p $q) +with sub (O $p) H ↪ Zpos (pos_pred_double $p) +with sub H (I $q) ↪ Zneg (O $q) +with sub H (O $q) ↪ Zneg (pos_pred_double $q) +with sub H H ↪ Z0; + +symbol sub_same z : π (sub z z = Z0) ≔ +begin + induction + { assume x xrec; simplify; rewrite xrec; reflexivity } + { assume x xrec; simplify; rewrite xrec; reflexivity } + { reflexivity } +end; + +symbol sub_opp x y : π (— sub x y = sub y x) ≔ +begin + induction + // case I + { assume x xrec; + induction + { assume y h; simplify; rewrite left xrec y; rewrite double_opp; reflexivity } + { assume y h; simplify; rewrite left xrec y; rewrite pred_double_opp; reflexivity } + { reflexivity } } + // case O + { assume x xrec; + induction + { assume y h; simplify; rewrite left xrec y; rewrite succ_double_opp; reflexivity } + { assume y h; simplify; rewrite left xrec y; rewrite double_opp; reflexivity } + { reflexivity } } + // case H + { induction { reflexivity } { reflexivity } { reflexivity } } +end; + +// Addition of integers + +symbol + : ℤ → ℤ → ℤ; +notation + infix right 20; + +rule Z0 + $y ↪ $y +with $x + Z0 ↪ $x +with Zpos $x + Zpos $y ↪ Zpos (add $x $y) +with Zpos $x + Zneg $y ↪ sub $x $y +with Zneg $x + Zpos $y ↪ sub $y $x +with Zneg $x + Zneg $y ↪ Zneg (add $x $y); + +// Interaction of addition with opposite + +symbol distr_—_+ x y : π (— (x + y) = — x + — y) ≔ +begin + induction + // case Z0 + { reflexivity } + // case Zpos + { assume x; + induction + { reflexivity } + { reflexivity } + { assume y; simplify; rewrite sub_opp; reflexivity } } + // case Zneg + { assume x; + induction + { reflexivity } + { assume y; simplify; rewrite sub_opp; reflexivity } + { reflexivity } } +end; + +// Commutativity of addition + +symbol +_com x y : π (x + y = y + x) ≔ +begin + induction + // case Z0 + { induction { reflexivity } { reflexivity } { reflexivity } } + // case Zpos + { assume x; + induction + { reflexivity } + { assume y; simplify; rewrite add_com; reflexivity } + { reflexivity } } + // case Zneg + { assume x; + induction + { reflexivity } + { reflexivity } + { assume y; simplify; rewrite add_com; reflexivity } } +end; + +// Interaction of succ and doubling functions + +symbol pred_double_succ x : π (pred_double (x + Zpos H) = succ_double x) ≔ +begin + induction + { reflexivity } + { assume x; simplify; rewrite pos_pred_double_succ; reflexivity } + { induction { reflexivity } { reflexivity } { reflexivity } } +end; + +symbol succ_pred_double x : π (pred_double x + Zpos H = double x) ≔ +begin + induction + { reflexivity } + { assume x; simplify; rewrite succ_pos_pred_double; reflexivity } + { reflexivity } +end; + +symbol succ_double_carac x : π (succ_double x = double x + Zpos H) ≔ +begin + induction { reflexivity } { reflexivity } { reflexivity } +end; + +symbol double_succ x : π (double (x + Zpos H) = succ_double x + Zpos H) ≔ +begin + induction + { reflexivity } + { reflexivity } + { induction { reflexivity } { reflexivity } { reflexivity } } +end; + +// Negation + +symbol - x y ≔ x + — y; +notation - infix left 20; + +symbol -_same z : π (z + — z = Z0) ≔ +begin + induction + { reflexivity } + { simplify; refine sub_same } + { simplify; refine sub_same } +end; + +// Associativity + +symbol sub_succ x y : π (sub (succ x) y = sub x y + Zpos H) ≔ +begin + induction + // case I + { assume x xrec; + induction + { assume y h; simplify; rewrite xrec; rewrite pred_double_succ; + rewrite succ_double_carac; reflexivity } + { assume y h; simplify; rewrite xrec; rewrite double_succ; reflexivity } + { simplify; rewrite pos_pred_double_succ; reflexivity } } + // case O + { assume x xrec; + induction + { assume y h; simplify; rewrite left succ_pred_double; reflexivity } + { assume y h; simplify; rewrite succ_double_carac; reflexivity } + { simplify; rewrite succ_pos_pred_double; reflexivity } } + // case H + { induction + { induction { reflexivity } { reflexivity } { reflexivity } } + { induction { reflexivity } { reflexivity } { reflexivity } } + { reflexivity } } +end; + +symbol add_Zpos_succ x p : π (x + Zpos (succ p) = (x + Zpos p) + Zpos H) ≔ +begin + induction + { reflexivity } + { assume x p; simplify; rewrite add_succ_right; reflexivity } + { assume x p; simplify; rewrite sub_succ; reflexivity } +end; + +symbol sub_add_Zpos a b c : π (sub a b + Zpos c = sub (add a c) b) ≔ +begin + assume a b c; + refine ind_ℙeano (λ c, sub a b + Zpos c = sub (add a c) b) _ _ c + // case H + { simplify; rewrite sub_succ; reflexivity } + // case succ + { assume r rrec; rewrite add_Zpos_succ; rewrite rrec; + rewrite add_succ_right; rewrite sub_succ; reflexivity } +end; + +symbol sub_add_Zneg a b c : π (sub a b + Zneg c = sub a (add b c)) ≔ +begin + assume a b c; + rewrite left sub_opp (add b c) a; + rewrite left sub_add_Zpos; + rewrite distr_—_+; rewrite sub_opp; reflexivity; +end; + +symbol +_assoc x y z : π ((x + y) + z = x + (y + z)) ≔ +begin + induction + { reflexivity } + { assume x; + induction + { reflexivity } + { assume y; + induction + { reflexivity } + // case Zpos - Zpos - Zpos + { assume z; simplify; rewrite add_assoc; reflexivity } + // case Zpos - Zpos - Zneg + { assume z; simplify; rewrite +_com; rewrite sub_add_Zpos; + rewrite add_com; reflexivity } } + + { assume y; + induction + { reflexivity } + // case Zpos - Zneg - Zpos + { assume z; simplify; rewrite sub_add_Zpos; rewrite +_com; + rewrite sub_add_Zpos; rewrite add_com; reflexivity } + // case Zpos - Zneg - Zneg + { assume z; simplify; rewrite sub_add_Zneg; reflexivity } } } + + { assume x; + induction + { reflexivity } + { assume y; + induction + { reflexivity } + // case Zneg - Zpos - Zpos + { assume z; simplify; rewrite sub_add_Zpos; reflexivity } + // case Zneg - Zpos - Zneg + { assume z; simplify; rewrite sub_add_Zneg; rewrite +_com; + rewrite sub_add_Zneg; rewrite add_com; reflexivity } } + + { assume y; + induction + { reflexivity } + // case Zneg - Zneg - Zpos + { assume z; simplify; rewrite +_com; rewrite sub_add_Zneg; + rewrite add_com; reflexivity } + // case Zneg - Zneg - Zneg + { assume z; simplify; rewrite add_assoc; reflexivity } } } +end; + +// Comparison of integers + +require open tests.OK.Comp; + +symbol ≐ : ℤ → ℤ → Comp; notation ≐ infix 12; // \doteq + +rule Z0 ≐ Z0 ↪ Eq +with Z0 ≐ Zpos _ ↪ Lt +with Z0 ≐ Zneg _ ↪ Gt +with Zpos _ ≐ Z0 ↪ Gt +with Zpos $p ≐ Zpos $q ↪ compare $p $q +with Zpos _ ≐ Zneg _ ↪ Gt +with Zneg _ ≐ Z0 ↪ Lt +with Zneg _ ≐ Zpos _ ↪ Lt +with Zneg $p ≐ Zneg $q ↪ compare $q $p; + +// ≐ decides the equality of integers + +symbol ≐_decides x y : π (x ≐ y = Eq ⇒ x = y) ≔ +begin + induction + // case Z0 + { induction + { reflexivity } + { assume y H; apply ⊥ₑ; refine Lt≠Eq H } + { assume y H; apply ⊥ₑ; refine Gt≠Eq H } } + // case Zpos + { assume x; + induction + { assume H; apply ⊥ₑ; refine Gt≠Eq H } + { assume y H; rewrite compare_decides x y H; reflexivity } + { assume y H; apply ⊥ₑ; refine Gt≠Eq H } } + // case Zneg + { assume x; + induction + { assume H; apply ⊥ₑ; refine Lt≠Eq H } + { assume y H; apply ⊥ₑ; refine Lt≠Eq H } + { assume y H; rewrite compare_decides y x H; reflexivity } } +end; + +// Commutative properties of ≐ + +symbol ≐_com x y : π (x ≐ y = opp (y ≐ x)) ≔ +begin + induction + // case Z0 + { induction { reflexivity } { reflexivity } { reflexivity } } + // case Zpos + { assume x; + induction + { reflexivity } + { assume y; simplify; rewrite compare_acc_com; reflexivity } + { reflexivity } } + // case Zneg + { assume x; + induction + { reflexivity } + { reflexivity } + { assume y; simplify; rewrite compare_acc_com; reflexivity } } +end; + +symbol ≐_opp x y : π (— x ≐ — y = opp (x ≐ y)) ≔ +begin + induction + // case Z0 + { induction { reflexivity } { reflexivity } { reflexivity } } + // case Zpos + { assume x; + induction + { reflexivity } + { assume y; simplify; rewrite compare_acc_com; reflexivity } + { reflexivity } } + // case Zneg + { assume x; + induction + { reflexivity } + { reflexivity } + { assume y; simplify; rewrite compare_acc_com; reflexivity } } +end; + +// General results + +symbol simpl_right x a : π ((x + a) - a = x) ≔ +begin + assume x a; simplify; rewrite +_assoc; + rewrite -_same; reflexivity; +end; + +symbol simpl_inv_right x a : π ((x - a) + a = x) ≔ +begin + assume x a; simplify; rewrite +_assoc; + rewrite .[— a + a] +_com; rewrite -_same; reflexivity; +end; + +// ≐ with 0 + +symbol ≐_double x : π ((double x ≐ Z0) = (x ≐ Z0)) ≔ +begin + induction { reflexivity } { reflexivity } { reflexivity } +end; + +symbol ≐_pred_double x : + π (pred_double x ≐ Z0 = case_Comp (x ≐ Z0) Lt Lt Gt) ≔ +begin + induction { reflexivity } { reflexivity } { reflexivity } +end; + +symbol ≐_succ_double x : + π (succ_double x ≐ Z0 = case_Comp (x ≐ Z0) Gt Lt Gt) ≔ +begin + induction { reflexivity } { reflexivity } { reflexivity } +end; + +symbol ≐_pos_sub x y : π ((sub x y ≐ Z0) = compare x y) ≔ +begin + induction + // case I + { assume x xrec; + induction + { assume y h; simplify; rewrite ≐_double; refine xrec y } + { assume y h; simplify; rewrite ≐_succ_double; rewrite xrec; + rewrite compare_Gt; reflexivity } + { reflexivity } } + // case O + { assume x xrec; + induction + { assume y h; simplify; rewrite ≐_pred_double; rewrite xrec; + rewrite compare_Lt; reflexivity } + { assume y h; simplify; rewrite ≐_double; refine xrec y } + { reflexivity } } + // case H + { induction { reflexivity } { reflexivity } { reflexivity } } +end; + +symbol ≐_sub x y : π ((x ≐ y) = (x + — y ≐ Z0)) ≔ +begin + induction + // case Z0 + { induction { reflexivity } { reflexivity } { reflexivity } } + // case Zpos + { assume x; + induction + { reflexivity } + { assume y; simplify; rewrite ≐_pos_sub; reflexivity } + { reflexivity } } + // case Zneg + { assume x; + induction + { reflexivity } + { reflexivity } + { assume y; simplify; rewrite ≐_pos_sub; reflexivity } } +end; + +// Compatibility of comparison with the addition + +symbol ≐_compat_add x y z : π ((x ≐ y) = (x + z ≐ y + z)) ≔ +begin + assume x y z; + rewrite ≐_sub; rewrite .[x in _ = x] ≐_sub; + simplify; rewrite distr_—_+; rewrite .[— y + — z] +_com; + rewrite +_assoc; rewrite left +_assoc z (— z) (— y); + rewrite -_same z; reflexivity; +end; + +// Directional comparison operators + +symbol ≤ x y ≔ ¬ (istrue(isGt (x ≐ y))); +notation ≤ infix 10; + +symbol < x y ≔ istrue(isLt (x ≐ y)); +notation < infix 10; + +symbol ≥ x y ≔ ¬ (x < y); +notation ≥ infix 10; + +symbol > x y ≔ ¬ (x ≤ y); +notation > infix 10; + +symbol <_≤ x y : π (x < y ⇒ x ≤ y) ≔ +begin + assume x y; + refine ind_Comp (λ u, istrue(isLt u) ⇒ istrue(isGt u) ⇒ ⊥) _ _ _ (x ≐ y) + { refine (λ x _, x) } + { refine (λ _ y, y) } + { refine (λ x _, x) } +end; + +// Compatibility of directional comparison operators + +symbol ≤_compat_add x y a : π (x ≤ y ⇒ x + a ≤ y + a) ≔ +begin + assume x y a; simplify; + assume H; refine fold_⇒ _; rewrite ≐_sub; + simplify; refine fold_⇒ _; rewrite +_assoc; + rewrite .[y + a] +_com; rewrite distr_—_+; + rewrite left +_assoc a (— a) (— y); rewrite -_same; + rewrite left +_assoc x Z0 (— y); simplify; refine fold_⇒ _; + rewrite left ≐_sub x y; refine H; +end; + +symbol <_compat_add x y a : π (x < y ⇒ x + a < y + a) ≔ +begin + assume x y a; simplify; assume H; rewrite ≐_sub; + simplify; rewrite +_assoc; rewrite .[y + a] +_com; + rewrite distr_—_+; rewrite left +_assoc a (— a) (— y); + rewrite -_same; rewrite left +_assoc; + simplify; rewrite left ≐_sub; refine H; +end; + +symbol ≤_compat_≤ x y : π (Z0 ≤ x ⇒ Z0 ≤ y ⇒ Z0 ≤ x + y) ≔ +begin + induction + { assume y h H; refine H } + { assume x; + induction + { assume h1 h2; refine λ x, x; } + { assume y h h'; refine λ x, x } + { simplify; assume y h f; apply ⊥ₑ; refine f ⊤ᵢ } } + { assume x y f h; apply ⊥ₑ; refine f ⊤ᵢ } +end; + +symbol <_compat_≤ x y : π (Z0 < x ⇒ Z0 ≤ y ⇒ Z0 < x + y) ≔ +begin + induction + { assume y f h; apply ⊥ₑ; refine f } + { assume x; + induction + { assume h1 h2; refine ⊤ᵢ } + { assume y h h'; refine ⊤ᵢ } + { simplify; assume y h f; apply ⊥ₑ; refine f ⊤ᵢ } } + { assume x; assume y f h; apply ⊥ₑ; refine f } +end; + +// Reflexivity + +symbol ≤_refl x : π (x ≤ x) ≔ +begin + assume x; refine ≤_compat_add Z0 Z0 x _; refine (λ x, x); +end; + +// Antisymmetry + +symbol ≤_antisym x y : π (x ≤ y ⇒ y ≤ x ⇒ x = y) ≔ +begin + assume x y; + have e : π (¬ (istrue(isGt (x ≐ y))) ⇒ ¬ (istrue(isGt (y ≐ x))) ⇒ x = y) + { rewrite ≐_com } ; + refine ind_Comp (λ c, (y ≐ x) = c ⇒ ¬ (istrue(isGt (opp c))) ⇒ ¬ (istrue(isGt c)) ⇒ x = y) _ _ _ (y ≐ x) _ + { assume H h1 h2; symmetry; refine ≐_decides y x H } + { assume h1 f h2; apply ⊥ₑ; refine f ⊤ᵢ } + { assume h1 h2 f; apply ⊥ₑ; refine f ⊤ᵢ } + { reflexivity; refine e } +end; + +// Transitivity theorems + +symbol ≤_trans x y z : π (x ≤ y ⇒ y ≤ z ⇒ x ≤ z) ≔ +begin + assume x y z lxy lyz; + have H : π (Z0 ≤ (z + — y) + (y + — x)) + { refine ≤_compat_≤ (z - y) (y - x) _ _ + { rewrite left -_same y; refine ≤_compat_add y z (— y) _; refine lyz } + { rewrite left -_same x; refine ≤_compat_add x y (— x) _; refine lxy } } ; + generalize H; refine fold_⇒ _; + rewrite +_assoc; rewrite left +_assoc (— y) y (— x); + rewrite .[— y + y] +_com; rewrite -_same; + refine (λ p : π ((Z0 ≤ (z + — x)) ⇒ (x ≤ z)), p) _; + rewrite left .[in x ≤ z] simpl_inv_right z x; + refine ≤_compat_add Z0 (z - x) x; +end; + +symbol <_trans_1 x y z : π (x < y ⇒ y ≤ z ⇒ x < z) ≔ +begin + assume x y z lxy lyz; + have H : π (Z0 < (z + — y) + (y + — x)) + { rewrite +_com; apply <_compat_≤ (y - x) (z - y) + { rewrite left -_same x; refine <_compat_add x y (— x) _; refine lxy } + { rewrite left -_same y; refine ≤_compat_add y z (— y) _; refine lyz } } ; + generalize H; refine fold_⇒ _; + rewrite +_assoc; rewrite left +_assoc (— y) y (— x); + rewrite .[— y + y] +_com; rewrite -_same; + rewrite left .[in x < z] simpl_inv_right z x; + refine <_compat_add Z0 (z - x) x; +end; + +symbol <_trans_2 x y z : π (x ≤ y ⇒ y < z ⇒ x < z) ≔ +begin + assume x y z lxy lyz; + have H : π (Z0 < (z + — y) + (y + — x)) + { apply <_compat_≤ (z - y) (y - x) + { rewrite left -_same y; refine <_compat_add y z (— y) _; refine lyz } + { rewrite left -_same x; refine ≤_compat_add x y (— x) _; refine lxy } }; + generalize H; refine fold_⇒ _; + rewrite +_assoc; rewrite left +_assoc (— y) y (— x); + rewrite .[— y + y] +_com; rewrite -_same; + rewrite left .[in x < z] simpl_inv_right z x; + refine <_compat_add Z0 (z - x) x; +end; + +// Multiplication + +symbol * : ℤ → ℤ → ℤ; +notation * infix right 22; + +rule Z0 * _ ↪ Z0 +with _ * Z0 ↪ Z0 +with Zpos $x * Zpos $y ↪ Zpos (mul $x $y) +with Zpos $x * Zneg $y ↪ Zneg (mul $x $y) +with Zneg $x * Zpos $y ↪ Zneg (mul $x $y) +with Zneg $x * Zneg $y ↪ Zpos (mul $x $y); + +// TO BE CONTINUED (theorems about multiplication) + +// shortcuts + +symbol _1 ≔ Zpos _1; +symbol _2 ≔ Zpos _2; +symbol _3 ≔ Zpos _3; +symbol _4 ≔ Zpos _4; +symbol _5 ≔ Zpos _5; +symbol _6 ≔ Zpos _6; +symbol _7 ≔ Zpos _7; +symbol _8 ≔ Zpos _8; +symbol _9 ≔ Zpos _9; +symbol _10 ≔ Zpos _10; + +// enable printing of integers in decimal notation + +builtin "int_zero" ≔ Z0; +builtin "int_positive" ≔ Zpos; +builtin "int_negative" ≔ Zneg; + +compute _2 - _3; + +// enable parsing of integers in decimal notation + +builtin "0" ≔ Z0; +builtin "1" ≔ _1; +builtin "2" ≔ _2; +builtin "3" ≔ _3; +builtin "4" ≔ _4; +builtin "5" ≔ _5; +builtin "6" ≔ _6; +builtin "7" ≔ _7; +builtin "8" ≔ _8; +builtin "9" ≔ _9; +builtin "10" ≔ _10; + +builtin "+" ≔ +; +builtin "*" ≔ *; +builtin "-" ≔ —; + +type -42; diff --git a/tests/OK/ac.lp b/tests/OK/ac.lp index b0d546681..44a47dd5d 100644 --- a/tests/OK/ac.lp +++ b/tests/OK/ac.lp @@ -6,7 +6,7 @@ commutative symbol + : A → A → A; notation + infix 10; assert x y ⊢ x + y ≡ y + x; -associative commutative symbol * : A → A → A; +right associative commutative symbol * : A → A → A; notation * infix 10; assert x y ⊢ x * y ≡ y * x; assert x y z ⊢ (x * y) * z ≡ x * (y * z); @@ -38,7 +38,7 @@ symbol Max : Nat → LvlSet → Lvl; symbol Plus : Nat → Lvl → LvlSet; symbol mapPlus : Nat → LvlSet → LvlSet; -associative commutative symbol Union : LvlSet → LvlSet → LvlSet; +right associative commutative symbol Union : LvlSet → LvlSet → LvlSet; rule Max $i (Union (Plus $j (Max $k $l)) $tl) ↪ Max (plus_N $i (plus_N $j $k)) (Union (mapPlus $j $l) $tl); diff --git a/tests/OK/lia.lp b/tests/OK/lia.lp new file mode 100644 index 000000000..974092ae8 --- /dev/null +++ b/tests/OK/lia.lp @@ -0,0 +1,160 @@ +require open tests.OK.Z tests.OK.Pos; + +constant symbol R : TYPE; + +symbol var : ℤ → ℤ → R; +/* semantics: [var x k] = x * k +note that the first argument could be of any type that has a ring structure +(we then would take R : TYPE → TYPE) */ +constant symbol cst:ℤ → R; +symbol opp:R → R; +right associative commutative symbol add:R → R → R; + +rule var _ 0 ↪ cst 0; + +rule opp (var $x $k) ↪ var $x (— $k) +with opp (cst $k) ↪ cst (— $k) +with opp (opp $x) ↪ $x +with opp (add $x $y) ↪ add (opp $x) (opp $y); +// note that opp is totally defined on terms built with var, cst, opp and add, i.e. no normal form contains opp + +rule add (var $x $k) (var $x $l) ↪ var $x ($k + $l) +with add (var $x $k) (add (var $x $l) $y) ↪ add (var $x ($k + $l)) $y +with add (cst $k) (cst $l) ↪ cst ($k + $l) +with add (cst $k) (add (cst $l) $y) ↪ add (cst ($k + $l)) $y +with add (cst 0) $x ↪ $x +with add $x (cst 0) ↪ $x; + +// example: +compute λ x y z, add (add (var x 1) (add (opp (var y 1)) (var z 1))) (add (var y 1) (var x 1)); +assert x y z ⊢ add (add (var x 1) (add (opp (var y 1)) (var z 1))) (add (var y 1) (var x 1)) ≡ add (var x 2) (var z 1); + +// multiplication by a constant (optional) +symbol mul:ℤ → R → R; +rule mul $k (var $z $l) ↪ var $z ($k * $l) +with mul $k (opp $r) ↪ mul (— $k) $r +with mul $k (add $r $s) ↪ add (mul $k $r) (mul $k $s) +with mul $k (cst $z) ↪ cst ($k * $z) +with mul $k (mul $l $z) ↪ mul ($k * $l) $z; +// note that mul is totally defined on terms built from var, cst, opp, add and mul, i.e. no normal form contains mul + +// reification +// WARNING: this symbol is declared as sequential +// and the reduction relation is not stable by substitution +sequential symbol ⇧ : ℤ → R; + +rule ⇧ 0 ↪ cst 0 +with ⇧ (Zpos $x) ↪ cst (Zpos $x) +with ⇧ (Zneg $x) ↪ cst (Zneg $x) +with ⇧ (— $x) ↪ opp (⇧ $x) +with ⇧ ($x + $y) ↪ add (⇧ $x) (⇧ $y) + +with ⇧ (0 * $y) ↪ mul 0 (⇧ $y) +with ⇧ (Zpos $x * $y) ↪ mul (Zpos $x) (⇧ $y) +with ⇧ (Zneg $x * $y) ↪ mul (Zneg $x) (⇧ $y) +with ⇧ ($y * 0) ↪ mul 0 (⇧ $y) +with ⇧ ($y * Zpos $x) ↪ mul (Zpos $x) (⇧ $y) +with ⇧ ($y * Zneg $x) ↪ mul (Zneg $x) (⇧ $y) + +with ⇧ $x ↪ var $x 1; // must be the last rule for ⇧ + +// example: +compute λ x y z, ⇧ ((x + ((— y) + z)) + (y + x)); +compute λ x, ⇧ ((— x - — 5) + x + — 4); + +assert (x y z:ℤ) ⊢ ⇧ ((x + ((— y) + z)) + (y + x)) ≡ ⇧ (2 * x + z); +assert (x:ℤ) ⊢ ⇧ ((— x - — 5) + x + — 4) ≡ ⇧ 1; + +// eval function +symbol ⇓: R → ℤ; +rule ⇓ (var $k $x) ↪ $k * $x +with ⇓ (cst $k) ↪ $k +with ⇓ (opp $x) ↪ — (⇓ $x) +with ⇓ (add $x $y) ↪ ⇓ $x + ⇓ $y; + +require open tests.OK.Set; + +symbol T1: τ int; +symbol T2: τ int; +symbol T3: τ int; +symbol T4: τ int; +symbol T5: τ int; +symbol T6: τ int; +symbol T7: τ int; +symbol T8: τ int; +symbol T9: τ int; +symbol T10: τ int; +symbol T11: τ int; +symbol T12: τ int; +symbol T13: τ int; +symbol T14: τ int; +symbol T15: τ int; +symbol T16: τ int; +symbol T17: τ int; +symbol T18: τ int; +symbol T19: τ int; +symbol T20: τ int; +symbol T21: τ int; +symbol T22: τ int; +symbol T23: τ int; +symbol T24: τ int; +symbol T25: τ int; +symbol T26: τ int; +symbol T27: τ int; +symbol T28: τ int; +symbol T29: τ int; +symbol T30: τ int; +symbol T31: τ int; +symbol T32: τ int; +symbol T33: τ int; +symbol T34: τ int; +symbol T35: τ int; +symbol T36: τ int; +symbol T37: τ int; +symbol T38: τ int; +symbol T39: τ int; +symbol T40: τ int; + +symbol t1 ≔ (⇧ + ( + (T1 + T2 + T3 + T4 + T5 + T6 + T7 + T8 + T9 + T10 + T11 + T12 + T13 + T14 + T15 + T16 + T17 + T18 + T19 + T20) + + ( + (— 1) * (T20 + T19 + T18 + T17 + T16 + T15 + T14 + T13 + T12 + T11 + T10 + T9 + T8 + T7 + T6 + T5 + T4 + T3 + T2 + T1) + ) + ) +); +compute t1; +assert ⊢ t1 ≡ ⇧ 0; + +symbol t2 ≔ (⇧ + ( + (T1 + T2 + T3 + T4 + T5 + T6 + T7 + T8 + T9 + T10 + T11 + T12 + T13 + T14 + T15 + T16 + T17 + T18 + T19 + T20 + T21 + T22) + + ( + (— 1) * (T22 + T21 + T20 + T19 + T18 + T17 + T16 + T15 + T14 + T13 + T12 + T11 + T10 + T9 + T8 + T7 + T6 + T5 + T4 + T3 + T2 + T1) + ) + ) +); +compute t2; +assert ⊢ t2 ≡ ⇧ 0; + +symbol t3 ≔ (⇧ + ( + (T1 + T2 + T3 + T4 + T5 + T6 + T7 + T8 + T9 + T10 + T11 + T12 + T13 + T14 + T15 + T16 + T17 + T18 + T19 + T20 + T21 + T22 + T23) + + ( + (— 1) * (T23 + T22 + T21 + T20 + T19 + T18 + T17 + T16 + T15 + T14 + T13 + T12 + T11 + T10 + T9 + T8 + T7 + T6 + T5 + T4 + T3 + T2 + T1) + ) + ) +); +compute t3; +assert ⊢ t3 ≡ ⇧ 0; + +symbol t4 ≔ (⇧ + ( + (T1 + T2 + T3 + T4 + T5 + T6 + T7 + T8 + T9 + T10 + T11 + T12 + T13 + T14 + T15 + T16 + T17 + T18 + T19 + T20 + T21 + T22 + T23 + T24 + T25 + T26 + T27 + T28 + T29 + T30 + T31 + T32 + T33 + T34 + T35 + T36 + T37 + T38 + T39 + T40) + + ( + (— 1) * (T40 + T39 + T38 + T37 + T36 + T35 + T34 + T33 + T32 + T31 + T30 + T29 + T28 + T27 + T26 + T25 + T24 + T23 + T22 + T21 + T20 + T19 + T18 + T17 + T16 + T15 + T14 + T13 + T12 + T11 + T10 + T9 + T8 + T7 + T6 + T5 + T4 + T3 + T2 + T1) + ) + ) +); +compute t4; +assert ⊢ t4 ≡ ⇧ 0; diff --git a/tests/OK/max-suc-alg.lp b/tests/OK/max-suc-alg.lp index e7ce5d983..1c12c6a4b 100644 --- a/tests/OK/max-suc-alg.lp +++ b/tests/OK/max-suc-alg.lp @@ -28,23 +28,23 @@ with ($x + $y) + $z ↪ $x + ($y + $z); // s-max algebra: successor iterator and max operator on levels constant symbol z : L; -symbol s : ℕ → L → L; -associative commutative symbol ⊕ : L → L → L; // associative right by default +symbol s : L → ℕ → L; +right associative commutative symbol ⊕ : L → L → L; notation ⊕ infix right 10; // Translation of Agda's levels to the s-max algebra -rule Z ↪ s Oₙ z -with S $x ↪ s (sₙ Oₙ) $x +rule Z ↪ s z Oₙ +with S $x ↪ s $x (sₙ Oₙ) with $x ∪ $y ↪ $x ⊕ $y -with V $x ↪ s Oₙ ($x ⊕ z); +with V $x ↪ s ($x ⊕ z) Oₙ; // rules for deciding the s-max algebra -rule s $p (s $q $x) ↪ s ($p + $q) $x -with s $p ($x ⊕ $y) ↪ s $p $x ⊕ s $p $y; +rule s (s $x $p) $q ↪ s $x ($p + $q) +with s ($x ⊕ $y) $p ↪ s $x $p ⊕ s $y $p; -rule s $p $x ⊕ s $q $x ↪ s ($p ⊕ₙ $q) $x -with s $p $x ⊕ (s $q $x ⊕ $y) ↪ s ($p ⊕ₙ $q) $x ⊕ $y; +rule s $x $p ⊕ s $x $q ↪ s $x ($p ⊕ₙ $q) +with s $x $p ⊕ (s $x $q ⊕ $y) ↪ s $x ($p ⊕ₙ $q) ⊕ $y; // tests -assert x y ⊢ ((S (S (V x))) ∪ (S (V y))) ∪ Z ≡ s (sₙ Oₙ) y ⊕ (s (sₙ(sₙ Oₙ)) x ⊕ s (sₙ(sₙ Oₙ)) z); -assert a ⊢ s (sₙ Oₙ) (a ⊕ z) ⊕ s (sₙ(sₙ Oₙ)) (a ⊕ z) ≡ s (sₙ(sₙ Oₙ)) a ⊕ s (sₙ(sₙ Oₙ)) z; +assert x y ⊢ ((S (S (V x))) ∪ (S (V y))) ∪ Z ≡ s y (sₙ Oₙ) ⊕ (s x (sₙ(sₙ Oₙ)) ⊕ s z (sₙ(sₙ Oₙ))); +assert a ⊢ s (a ⊕ z) (sₙ Oₙ) ⊕ s (a ⊕ z) (sₙ(sₙ Oₙ)) ≡ s a (sₙ(sₙ Oₙ)) ⊕ s z (sₙ(sₙ Oₙ)); diff --git a/tests/OK/plus_ac.lp b/tests/OK/plus_ac.lp index 7f0ddc623..3034422a5 100644 --- a/tests/OK/plus_ac.lp +++ b/tests/OK/plus_ac.lp @@ -1,7 +1,7 @@ symbol N:TYPE; symbol O:N; symbol s:N → N; -associative commutative symbol +:N → N → N; +right associative commutative symbol +:N → N → N; notation + infix 10; assert x y z ⊢ (x + s y) + s(s z) ≡ s(s z) + (x + s y); compute λ x y z, (x + s y) + s(s z); diff --git a/tests/OK/xor.lp b/tests/OK/xor.lp index 95f2e24cd..b2961f98d 100644 --- a/tests/OK/xor.lp +++ b/tests/OK/xor.lp @@ -1,7 +1,8 @@ symbol B:TYPE; symbol O:B; -associative commutative symbol +:B → B → B; notation + infix right 20; +right associative commutative symbol +:B → B → B; +notation + infix right 20; rule O + $x ↪ $x with $x + O ↪ $x diff --git a/tests/export_raw_dk.sh b/tests/export_raw_dk.sh index 60d612f3d..475d4d4eb 100755 --- a/tests/export_raw_dk.sh +++ b/tests/export_raw_dk.sh @@ -60,7 +60,7 @@ do # proofs why3*|tutorial|try|tautologies|rewrite*|remove|natproofs|have|generalize|foo|comment_in_qid|apply|anonymous|admit);; # "open" - triangular|power-fact|postfix|perf_rw_*|not-eager|nonLeftLinear2|natural|Nat|lpparse2|logic|List|FOL|Eq|doc|Bool|arity_var|arity_diff|922|262_pair_ex_2|215|1141|Tactic|Option|String|HOL|Impred|PropExt|Classic|1217);; + triangular|power-fact|postfix|perf_rw_*|not-eager|nonLeftLinear2|natural|Nat|lpparse2|logic|List|FOL|Eq|doc|Bool|arity_var|arity_diff|922|262_pair_ex_2|215|1141|Tactic|Option|String|HOL|Impred|PropExt|Classic|1217|Comp|Pos|Z|lia);; # "inductive" strictly_positive_*|inductive|989|904|830|341);; # underscore in query diff --git a/tests/kernel.ml b/tests/kernel.ml index c67117382..76a9095a9 100644 --- a/tests/kernel.ml +++ b/tests/kernel.ml @@ -11,7 +11,7 @@ let open_sign_default () = let sign = Sig_state.create_sign [ "dummy" ] in let _ = Sign.add_symbol sign Term.Public Term.Defin Term.Eager false - (Pos.none "foo") None Term.mk_Type [] + (Pos.none "foo") None Term.Type [] in let ss = Sig_state.of_sign sign in Alcotest.(check unit) diff --git a/tests/rewriting.ml b/tests/rewriting.ml index c1064c02b..acd8f4286 100644 --- a/tests/rewriting.ml +++ b/tests/rewriting.ml @@ -15,7 +15,7 @@ let scope_term ss = Scope.scope_term true ss [] let add_sym ss id = Sig_state.add_symbol ss Public Defin Eager false (Pos.none id) None - Term.mk_Kind [] None + Term.Kind [] None (* Define a signature state and some symbols. *)