Skip to content

Commit b618e8f

Browse files
bobatkeybobatkey
committed
[ model_checker ] fol_formula and parser_utils no longer public
1 parent 7ff1b73 commit b618e8f

13 files changed

+60
-132
lines changed

‎dune-project

-6
Original file line numberDiff line numberDiff line change
@@ -24,12 +24,6 @@
2424
; (tags
2525
; (topics "to describe" your project)))
2626

27-
(package
28-
(name fol_formula))
29-
30-
(package
31-
(name parser_util))
32-
3327
(package
3428
(name site_gen))
3529

‎fol_formula.opam

-30
This file was deleted.

‎fol_formula/dune

+1-7
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,6 @@
11
(library
22
(name fol_formula)
3-
(public_name fol_formula)
4-
(libraries menhirLib parser_util sexplib0)
3+
(libraries menhirLib parser_util sexplib0 generalities)
54
(preprocess
65
(pps ppx_sexp_conv ppx_inline_test))
76
(inline_tests)
@@ -15,11 +14,6 @@
1514
(modules grammar parser)
1615
(merge_into parser))
1716

18-
(install
19-
(section lib)
20-
(package fol_formula)
21-
(files grammar.mly))
22-
2317
(rule
2418
(targets parser_messages.ml)
2519
(deps parser.mly grammar.mly parser.messages)

‎fol_formula/lexer.mll

+2-2
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,8 @@ let digit = ['0'-'9']
1111
rule token = parse
1212
| white { token lexbuf }
1313
| "->" | "→" { ARROW }
14-
| "/\\" | "∧" | "&&" { AND }
15-
| "\\/" | "∨" | "||" { OR }
14+
| "/\\" | "∧" | "&&" | "&" { AND }
15+
| "\\/" | "∨" | "||" | "|" { OR }
1616
| "!" | "~" | "¬" { NOT }
1717
| "(" { LPAREN }
1818
| ")" { RPAREN }

‎frontend.opam

-2
Original file line numberDiff line numberDiff line change
@@ -6,11 +6,9 @@ depends: [
66
"msat"
77
"menhir"
88
"ulmus"
9-
"parser_util"
109
"ppx_monoid"
1110
"ppx_deriving"
1211
"ppx_inline_test"
13-
"fol_formula"
1412
]
1513
pin-depends: [
1614
[ "ulmus.~dev"

‎model_checker/lib/dune

+6-6
Original file line numberDiff line numberDiff line change
@@ -7,12 +7,12 @@
77
(ocamllex lexer)
88

99
(menhir
10-
(modules grammar formula_grammar)
10+
(modules grammar)
1111
(flags --table --unused-token UNKNOWN)
1212
(merge_into parser))
1313

14-
(rule
15-
(targets formula_grammar.mly)
16-
(deps %{lib:fol_formula:grammar.mly})
17-
(action
18-
(copy %{lib:fol_formula:grammar.mly} formula_grammar.mly)))
14+
; (rule
15+
; (targets formula_grammar.mly)
16+
; (deps %{lib:fol_formula:grammar.mly})
17+
; (action
18+
; (copy %{lib:fol_formula:grammar.mly} formula_grammar.mly)))

‎model_checker/lib/grammar.mly

+4-6
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
11
%{
2-
open Fol_formula
32
open Structure
43

54
(* FIXME: locations *)
@@ -12,9 +11,8 @@ open Structure
1211
%token AXIOMATISATION SYNTH SIZE
1312
%token LBRACE RBRACE MODELS EQUALS LPAREN RPAREN COMMA SLASH COLON
1413

15-
%token AND OR NOT ARROW DOT FORALL EXISTS TRUE FALSE EQ NE
16-
17-
%token EOF UNKNOWN QUOTE
14+
%token EOF UNKNOWN
15+
%token <Fol_formula.formula> QUOTED
1816

1917
%start <Structure.item list> structure
2018

@@ -31,13 +29,13 @@ item:
3129
{ Model { name; vocab_name; defns } }
3230
| AXIOMATISATION; name=IDENT; FOR; vocab=IDENT; LBRACE; formulas=separated_list(COMMA,named_formula); RBRACE
3331
{ Axioms { name; vocab; formulas } }
34-
| CHECK; model_name=IDENT; MODELS; QUOTE; formula=formula; QUOTE
32+
| CHECK; model_name=IDENT; MODELS; formula=QUOTED
3533
{ Check { model_name; formula } }
3634
| SYNTH; axioms=IDENT; SIZE; cardinality=INTLIT
3735
{ Synth { axioms; cardinality } }
3836

3937
named_formula:
40-
| nm=IDENT; COLON; QUOTE; f=formula; QUOTE
38+
| nm=IDENT; COLON; f=QUOTED
4139
{ (nm, f) }
4240

4341
arity_defn:

‎model_checker/lib/lexer.mll

+27-23
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
{
22
open Parser
3+
open Fol_formula
34
}
45

56
let white = [' ' '\t']+
@@ -9,32 +10,34 @@ let digit = ['0'-'9']
910
rule structure_token = parse
1011
| white { structure_token lexbuf }
1112
| '/''/' [^'\n']* '\n' { Lexing.new_line lexbuf; structure_token lexbuf }
12-
| '/''/' [^'\n']* eof { EOF }
13+
| '/''/' [^'\n']* eof { Ok EOF }
1314
| '\n' { Lexing.new_line lexbuf; structure_token lexbuf }
14-
| "\"" { QUOTE }
15-
| "vocab" { VOCAB }
16-
| "for" { FOR }
17-
| "model" { MODEL }
18-
| "check" { CHECK }
19-
| "axioms" { AXIOMATISATION }
20-
| "synth" { SYNTH }
21-
| "size" { SIZE }
22-
| "{" { LBRACE }
23-
| "}" { RBRACE }
24-
| "|=" { MODELS }
25-
| "=" { EQUALS }
26-
| "(" { LPAREN }
27-
| ")" { RPAREN }
28-
| ":" { COLON }
29-
| "/" { SLASH }
30-
| "," { COMMA }
31-
| ident { IDENT (Lexing.lexeme lexbuf) }
15+
| "\"" ([^ '\"']* as quoted) "\""
16+
{ Result.bind (Formula.of_string quoted) (fun f -> Ok (QUOTED f)) }
17+
| "vocab" { Ok VOCAB }
18+
| "for" { Ok FOR }
19+
| "model" { Ok MODEL }
20+
| "check" { Ok CHECK }
21+
| "axioms" { Ok AXIOMATISATION }
22+
| "synth" { Ok SYNTH }
23+
| "size" { Ok SIZE }
24+
| "{" { Ok LBRACE }
25+
| "}" { Ok RBRACE }
26+
| "|=" { Ok MODELS }
27+
| "=" { Ok EQUALS }
28+
| "(" { Ok LPAREN }
29+
| ")" { Ok RPAREN }
30+
| ":" { Ok COLON }
31+
| "/" { Ok SLASH }
32+
| "," { Ok COMMA }
33+
| ident { Ok (IDENT (Lexing.lexeme lexbuf)) }
3234
| ('-'|'+'|"")digit+
33-
{ try (INTLIT (int_of_string (Lexing.lexeme lexbuf)))
34-
with Failure _ -> UNKNOWN }
35-
| eof { EOF }
36-
| _ { UNKNOWN }
35+
{ try (Ok (INTLIT (int_of_string (Lexing.lexeme lexbuf))))
36+
with Failure _ -> Ok UNKNOWN }
37+
| eof { Ok EOF }
38+
| _ { Ok UNKNOWN }
3739

40+
(*
3841
and formula_token = parse
3942
| white { formula_token lexbuf }
4043
| '\n' { Lexing.new_line lexbuf; formula_token lexbuf }
@@ -59,3 +62,4 @@ and formula_token = parse
5962
| ident { IDENT (Lexing.lexeme lexbuf) }
6063
| eof { EOF }
6164
| _ { UNKNOWN }
65+
*)

‎model_checker/lib/reader.ml

+16-20
Original file line numberDiff line numberDiff line change
@@ -1,37 +1,33 @@
1-
let token state lexbuf =
2-
let open Parser in
3-
match state with
4-
| `Structure -> (
5-
match Lexer.structure_token lexbuf with
6-
| QUOTE -> (`Formula, QUOTE (* or supress it?*))
7-
| token -> (`Structure, token))
8-
| `Formula -> (
9-
match Lexer.formula_token lexbuf with
10-
| QUOTE -> (`Structure, QUOTE)
11-
| token -> (`Formula, token))
12-
131
(* FIXME: error messages?? *)
142
let parse entrypoint lexbuf =
153
let module MI = Parser.MenhirInterpreter in
16-
let rec loop lex_state cp =
4+
let rec loop cp =
175
match cp with
186
| MI.Accepted a -> Ok a
197
| MI.InputNeeded _env ->
20-
let lex_state, tok = token lex_state lexbuf in
21-
let spos = Lexing.lexeme_start_p lexbuf in
22-
let epos = Lexing.lexeme_end_p lexbuf in
23-
loop lex_state (MI.offer cp (tok, spos, epos))
24-
| MI.Shifting _ | MI.AboutToReduce _ -> loop lex_state (MI.resume cp)
8+
(match Lexer.structure_token lexbuf with
9+
| Ok tok ->
10+
let spos = Lexing.lexeme_start_p lexbuf in
11+
let epos = Lexing.lexeme_end_p lexbuf in
12+
loop (MI.offer cp (tok, spos, epos))
13+
| Error (`Parse e) ->
14+
let pos = Parser_util.Location.of_lexbuf lexbuf in
15+
Error (fun fmt ->
16+
Format.fprintf fmt
17+
"Error in formula at %a: %s"
18+
Parser_util.Location.pp_without_filename pos
19+
(Parser_util.Driver.string_of_error e)))
20+
| MI.Shifting _ | MI.AboutToReduce _ -> loop (MI.resume cp)
2521
| MI.HandlingError _ ->
2622
let pos = Parser_util.Location.of_lexbuf lexbuf in
2723
let lexeme = Lexing.lexeme lexbuf in
2824
Error
2925
(fun fmt ->
3026
Format.fprintf fmt "Error at %a on input '%s'"
31-
Parser_util.Location.pp pos lexeme)
27+
Parser_util.Location.pp_without_filename pos lexeme)
3228
| MI.Rejected -> assert false
3329
in
3430
let init_pos = lexbuf.Lexing.lex_curr_p in
35-
loop `Structure (entrypoint init_pos)
31+
loop (entrypoint init_pos)
3632

3733
let parse = parse Parser.Incremental.structure

‎parser_util.opam

-26
This file was deleted.

‎parser_util/dune

-1
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,5 @@
11
(library
22
(name parser_util)
3-
(public_name parser_util)
43
(libraries menhirLib)
54
(flags
65
(:standard -w -49-9-27)))

‎site_gen.opam

+4-2
Original file line numberDiff line numberDiff line change
@@ -11,12 +11,14 @@ depends: [
1111
"ocaml"
1212
"dune" {>= "3.7"}
1313
"menhir"
14-
"fol_formula"
15-
"parser_util"
1614
"omd"
1715
"html_sig"
1816
"ctypes"
1917
"ctypes-foreign"
18+
"sexplib0"
19+
"ppx_sexp_conv"
20+
"ppx_inline_test"
21+
"sexplib"
2022
]
2123
pin-depends: [
2224
[ "html_sig.~dev"

‎slakemoth.opam

-1
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,6 @@ depends: [
1616
"odoc" {with-doc}
1717
"ulmus"
1818
"omd"
19-
"parser_util"
2019
"ppx_monoid"
2120
"ppx_deriving"
2221
"ppx_inline_test"

0 commit comments

Comments
 (0)