From bfa7a567c67854eb58c4aa2d8760f765b8093251 Mon Sep 17 00:00:00 2001 From: Gabriel Hondet <7418676+gabrielhdt@users.noreply.github.com> Date: Sun, 5 Nov 2023 19:23:04 +0100 Subject: [PATCH 1/3] Add upper bound on pratter (#1017) Pratter is going to be updated (see https://github.com/ocaml/opam-repository/pull/24746) and its interface will change. To avoid conflicts, make lambdapi depend on the current interface, that is, on pratter version 2. Co-authored-by: Gabriel Hondet --- dune-project | 2 +- lambdapi.opam | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/dune-project b/dune-project index f121ff6e5..efea963c7 100644 --- a/dune-project +++ b/dune-project @@ -57,7 +57,7 @@ the Why3 platform.") (dedukti (and :with-test (>= 2.7))) (bindlib (>= 5.0.1)) (timed (>= 1.0)) - (pratter (>= 2.0.0)) + (pratter (and (>= 2.0.0) (< 3))) (camlp-streams (>= 5.0)) (why3 (and (>= 1.6.0) (< 1.7~))) (yojson (>= 1.6.0)) diff --git a/lambdapi.opam b/lambdapi.opam index 3b8b24a96..0660699d7 100644 --- a/lambdapi.opam +++ b/lambdapi.opam @@ -55,7 +55,7 @@ depends: [ "dedukti" {with-test & >= "2.7"} "bindlib" {>= "6.0.0"} "timed" {>= "1.0"} - "pratter" {>= "2.0.0"} + "pratter" {>= "2.0.0" & < "3"} "camlp-streams" {>= "5.0"} "why3" {>= "1.6.0" & < "1.7~"} "yojson" {>= "1.6.0"} From 3067fafe2a7df5e7a97b91e285a39cabd1422bcd Mon Sep 17 00:00:00 2001 From: Gabriel Hondet <7418676+gabrielhdt@users.noreply.github.com> Date: Sat, 11 Nov 2023 07:07:44 +0100 Subject: [PATCH 2/3] Update Pratter from 2 to 3 (#1019) Co-authored-by: Gabriel Hondet --- dune-project | 2 +- lambdapi.opam | 2 +- src/parsing/pratt.ml | 64 ++++++++++++++++++++------------------------ 3 files changed, 31 insertions(+), 37 deletions(-) diff --git a/dune-project b/dune-project index efea963c7..6893c640a 100644 --- a/dune-project +++ b/dune-project @@ -57,7 +57,7 @@ the Why3 platform.") (dedukti (and :with-test (>= 2.7))) (bindlib (>= 5.0.1)) (timed (>= 1.0)) - (pratter (and (>= 2.0.0) (< 3))) + (pratter (and (>= 3.0.0) (< 4))) (camlp-streams (>= 5.0)) (why3 (and (>= 1.6.0) (< 1.7~))) (yojson (>= 1.6.0)) diff --git a/lambdapi.opam b/lambdapi.opam index 0660699d7..0ea169819 100644 --- a/lambdapi.opam +++ b/lambdapi.opam @@ -55,7 +55,7 @@ depends: [ "dedukti" {with-test & >= "2.7"} "bindlib" {>= "6.0.0"} "timed" {>= "1.0"} - "pratter" {>= "2.0.0" & < "3"} + "pratter" {>= "3.0.0" & < "4"} "camlp-streams" {>= "5.0"} "why3" {>= "1.6.0" & < "1.7~"} "yojson" {>= "1.6.0"} diff --git a/src/parsing/pratt.ml b/src/parsing/pratt.ml index 0ed83ee42..70b67e2ce 100644 --- a/src/parsing/pratt.ml +++ b/src/parsing/pratt.ml @@ -8,61 +8,55 @@ open Core open Syntax module Pratt : sig - val parse : ?find_sym:Core.Sig_state.find_sym -> Sig_state.t -> Env.t + val parse : ?find_sym:Sig_state.find_sym -> Sig_state.t -> Env.t -> p_term -> p_term (** [parse ~find_sym ss env t] Pratt parses term [t], unsugaring infix operators and prefix operators using signature state [ss] and environment [env] to determine which term is an operator, and to build - new terms. Note that it doesn't recurse into abstractions or - implications and alike. [~find_sym] is used to scope symbol + new terms. Note that it doesn't recurse into abstractions or + implications and alike. [~find_sym] is used to scope symbol identifiers. *) end = struct open Lplib open Pos - module Pratt_terms : Pratter.SUPPORT - with type term = p_term - and type table = Core.Sig_state.find_sym * Sig_state.t * Env.t - = struct - type term = p_term - type table = Core.Sig_state.find_sym * Sig_state.t * Env.t + let is_op : Sig_state.find_sym -> Sig_state.t -> Env.t -> p_term + -> (Pratter.fixity * float) option = + fun find_sym ss env t -> + match t.elt with + | P_Iden({elt=(mp, s); _} as id, false) -> + let open Option.Monad in + let* sym = + try (* Look if [id] is in [env]... *) + if mp <> [] then raise Not_found; + ignore (Env.find s env); None + with Not_found -> (* ... or look into the signature *) + Some(find_sym ~prt:true ~prv:true ss id) + in + (match Term.SymMap.find_opt sym ss.notations with + | Some(Infix(assoc, prio)) -> Some(Pratter.Infix assoc, prio) + | Some(Prefix(prio)) | Some(Succ(Some(Prefix(prio)))) -> + Some(Pratter.Prefix, prio) + | Some(Postfix(prio)) | Some(Succ(Some(Postfix(prio)))) -> + Some(Pratter.Postfix, prio) + | Some (Zero | Succ _ | Quant) | None -> None) + | _ -> None - (* Get properties of term [t] if its an operator. *) - let get ((find_sym : Core.Sig_state.find_sym), tbl, env) t = - match t.elt with - | P_Iden({elt=(mp, s); _} as id, false) -> - let open Option.Monad in - let* sym = - try (* Look if [id] is in [env]... *) - if mp <> [] then raise Not_found; - ignore (Env.find s env); None - with Not_found -> (* ... or look into the signature *) - Some(find_sym ~prt:true ~prv:true tbl id) - in - (match Term.SymMap.find_opt sym tbl.notations with - | Some(Infix(assoc, prio)) -> Some(Pratter.Infix assoc, prio) - | Some(Prefix(prio)) | Some(Succ(Some(Prefix(prio)))) -> - Some(Pratter.Prefix, prio) - | Some(Postfix(prio)) | Some(Succ(Some(Postfix(prio)))) -> - Some(Pratter.Postfix, prio) - | Some (Zero | Succ _ | Quant) | None -> None) - | _ -> None - - let make_appl t u = Pos.make (Pos.cat t.pos u.pos) (P_Appl(t, u)) - end + let appl : p_term -> p_term -> p_term = fun t u -> + Pos.make (Pos.cat t.pos u.pos) (P_Appl(t, u)) (* NOTE the term is converted from appl nodes to list in [Pratt.parse], rebuilt into appl nodes by [Pratt.parse], and then decomposed again into a list by [get_args]. We could make [Pratt.parse] return a list of terms instead. *) - let parse : ?find_sym:Core.Sig_state.find_sym -> + let parse : ?find_sym:Sig_state.find_sym -> Sig_state.t -> Env.t -> p_term -> p_term = fun ?(find_sym=Sig_state.find_sym) st env t -> let h, args = Syntax.p_get_args t in let strm = Stream.of_list (h :: args) in - let module Parse = Pratter.Make(Pratt_terms) in - match Parse.expression (find_sym, st, env) strm with + let is_op = is_op find_sym st env in + match Pratter.expression ~is_op ~appl strm with | Ok e -> e | Error `TooFewArguments -> Error.fatal t.pos "Malformed application in \"%a\"" Pretty.term t From b905e6d09bf369e5d759eae04dc7cb35b72bd7bd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Wed, 22 Nov 2023 11:50:01 +0100 Subject: [PATCH 3/3] release 2.4.1 (#1020) --- CHANGES.md | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index 0e0e30fa7..7bdf0fe81 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -3,6 +3,22 @@ All notable changes to this project will be documented in this file. The format is based on [Keep a Changelog](https://keepachangelog.com/), and this project adheres to [Semantic Versioning](https://semver.org/). +## 2.4.1 (2023-11-22) + +### Added + +- support for Pratter 3.0.0 +- printing of unification and coercion rules + +### Improved + +- unification + +### Fixed + +- Coq export +- matita.sh script + ## 2.4.0 (2023-07-28) ### Added