package pratter

  1. Overview
  2. Docs
An extended Pratt parser

Install

Dune Dependency

Authors

Maintainers

Sources

pratter-1.2.1.tbz
sha256=7dd9a7b970d3f660a957a54ae257ac2228f8203a133f8ceb7a73ce61f0663833
sha512=040a36c6d61761701d7f93d620f5a466caa0d578f6dfb0a93028fd8f693b4abef8b22c9b7695971e21ce347865dfc84f26cc032f1c4bfc070ee6e87cd9a72318

Description

Pratter is a library that provides a parser that transforms streams of terms to applied terms. Terms may contain infix or prefix operators and native applications. The parser is based on the Pratt parsing algorithm and extended to handle term application and non associative operators.

Published: 10 May 2022

README

Pratter: A parser for terms with operators and applications

Pratter is a library that provides a parser that transforms streams of terms to applied terms. Terms may contain infix or prefix operators and applications. The parser is an extension of the Pratt parsing algorithm.

Examples can be seen in the tests inside the t/ folder.

Example: simple terms

The idea is that terms are made of symbols and applications and some symbol can be declared to be infix or prefix operators.

Start by defining the terms,

type term = Appl of term * term | Symb of string

and the data structure that maps symbols identifiers to operators properties,

type table = {
    unary  : (string * Pratter.priority) list
  ; binary : (string * (Pratter.priority * Pratter.associativity)) list
}
let empty : table = { unary = [] ; binary = [] }

Next, define a module to pack these two types, and two functions:

  • get that is able to retrieve the properties of a symbol if it is declared as an operator,

  • make_appl that creates an application out of two terms.

module Terms : Pratter.SUPPORT with type term = term and type table = table =
struct
  type nonrec term = term
  type nonrec table = table
  let get { unary; binary } (t: term) =
  match t with
  | Symb id -> (
      try Some (Pratter.Una, List.assoc id unary)
      with Not_found -> (
        try
          let bp, assoc = List.assoc id binary in
          Some (Bin assoc, bp)
        with Not_found -> None ) )
  | _ -> None

  let make_appl t u = Appl (t, u)
end

module Parser = Pratter.Make (Terms)

Then that's it, we can parse streams of terms with operators. For instance, assume that we want to parse x + y * -z where

  • + and * are infix operators, with * having a higher binding power than +;

  • - is a unary operator having a higher binding power than + and *.

Create a table holding these operators:

let tbl =
  { unary = [ "-", 1.0 ]
  ; binary = [ ("+", (0.5, Pratter.Left)) ; ("*", (0.6, Pratter.Left)) ] }

Priority (also called binding power) can be any float, and associativity may be Pratter.Left, Pratter.Right or Pratter.Neither.

Finally parse the input using Parser.expression:

let input = [ Symb "x"; Symb "+"; Symb "y"; Symb "*"; Symb "-"; Symb "z"]
Parser.expression tbl (Stream.of_list input)

we obtain the term x + (y * (-z)) representend by

Appl (Appl (Symb "+", Symb "x"),
 Appl (Appl (Symb "*", Symb "y"), Appl (Symb "-", Symb "z")))

Dependencies (2)

  1. camlp-streams
  2. dune >= "2.7"

Dev Dependencies (5)

  1. odoc with-doc
  2. qcheck-alcotest with-test
  3. qcheck with-test
  4. alcotest with-test
  5. ocaml >= "4.02" | with-test & >= "4.03"

Used by (1)

  1. lambdapi >= "2.0.0" & < "2.2.1"

Conflicts

None