Merge branch 'master' into add_opaque_cmd

Deducteam · Nov 23, 2023 · d5f8d48 · d5f8d48
2 parents 2d6ab39 + b905e6d
commit d5f8d48
Show file tree

Hide file tree

Showing 4 changed files with 47 additions and 37 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -7,6 +7,22 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 
 - Add the command `opaque` that opacifies a symbol already defined.
 
+## 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

diff --git 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 (>= 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
@@ -55,7 +55,7 @@ depends: [
   "dedukti" {with-test & >= "2.7"}
   "bindlib" {>= "6.0.0"}
   "timed" {>= "1.0"}
-  "pratter" {>= "2.0.0"}
+  "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
@@ -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