Skip to content

Commit

Permalink
Replace earley by pacomb in examples.
Browse files Browse the repository at this point in the history
  • Loading branch information
craff authored and rlepigre committed May 1, 2024
1 parent 5b35600 commit 0a3fed2
Show file tree
Hide file tree
Showing 4 changed files with 27 additions and 25 deletions.
2 changes: 1 addition & 1 deletion bindlib.opam
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ depends: [
"ocaml" {>= "4.07.0"}
"dune" {>= "2.7" & build}
"timed" {>= "1.0" & with-test}
"earley" {= "3.0.0" & with-test}
"pacomb" {>= "1.1" & with-test}
"odoc" {with-doc}
]
build: [
Expand Down
2 changes: 1 addition & 1 deletion dune-project
Original file line number Diff line number Diff line change
Expand Up @@ -23,5 +23,5 @@
(ocaml (>= 4.07.0))
(dune :build)
(timed (and (>= 1.0) :with-test))
(earley (and (= 3.0.0) :with-test))
(pacomb (and (>= 1.1) :with-test))
(odoc :with-doc)))
4 changes: 2 additions & 2 deletions examples/metavar/dune
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
(test
(name main)
(preprocess (per_module ((action (run pa_ocaml %{input-file})) parser)))
(libraries bindlib earley.core timed)
(preprocess (per_module ((pps pacomb.ppx) parser)))
(libraries bindlib unix pacomb timed)
(action (with-stdin-from test.txt (run %{test}))))
44 changes: 23 additions & 21 deletions examples/metavar/parser.ml
Original file line number Diff line number Diff line change
@@ -1,30 +1,32 @@
open Earley_core
open Pacomb
open Ast

let parser ident = id:{#[a-z0-9][_a-zA-Z0-9]*[']*#}[group.(0)]
let%parser ident = (id::RE"[a-z0-9][_a-zA-Z0-9]*[']*") => id

let parser term_atom =
| id:ident -> PVar id
| '(' t:term_full ')' -> t
| '[' t:term_full ']' -> PNrm t
let%parser rec term_atom =
(id::ident) => PVar id
; '(' (t::term_full) ')' => t
; '[' (t::term_full) ']' => PNrm t

and parser term_appl =
| term_atom
| t:term_appl u:term_atom -> PApp(t,u)
and term_appl =
(t::term_atom) => t
; (t::term_appl) (u::term_atom) => PApp(t,u)

and parser term_full =
| term_appl
| {"λ"|"%"} ids:ident* '.' t:term_full -> many_PLam ids t
and term_full =
(t::term_appl) => t
; ("λ" => () ; "%" => ()) (ids:: ~* ident) '.' (t::term_full)
=> many_PLam ids t

let parser command =
| "$u" -> Undo
| "$g" -> Goal
| "$s" x:ident "=" t:term_full -> Decl(x,t)
| "$p" t:term_full -> Prnt(t)
let%parser command =
"$u" => Undo
; "$g" => Goal
; "$s" (x::ident) "=" (t::term_full) => Decl(x,t)
; "$p" (t::term_full) => Prnt(t)

let parser commands = {command ";"}*
let%parser commands = cs :: ~* ((c::command) ";" => c) => cs

let blank = Blank.line_comments "//"

let parse_channel : in_channel -> cmd list = fun ic ->
let blank = Blanks.line_comments "//" in
let parse = Earley.parse_buffer commands blank in
Earley.handle_exception parse (Input.from_channel ic)
let parse = Grammar.parse_channel commands blank in
Pos.handle_exception parse ic

0 comments on commit 0a3fed2

Please sign in to comment.