Commit 47be8555 authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Add a small parser for CSI^HO confluence counter-examples

parent 58842ac2
let main () =
Arg.parse [] (fun file ->
Base.labels := [];
let input = open_in file in
let lb = Lexing.from_channel input in
try
Parse_csiho.file Lex_csiho.token lb
with
| e ->
let start = lb.Lexing.lex_start_p in
let file = start.Lexing.pos_fname in
let line = start.Lexing.pos_lnum in
let cnum = start.Lexing.pos_cnum - start.Lexing.pos_bol in
let tok = Lexing.lexeme lb in
Format.eprintf "Error File: %s, line: %d, column: %d, Token \"%s\"@\n@."
file line cnum tok;
raise e)
"Please provide a file name."
let _ = main ()
{
open Parse_csiho
}
let num = [ '0' - '9' ]+
let id = [ 'a' - 'z' 'A' - 'Z' '_' '0' - '9' '\'' ]+
let unknown_meta = 'm' '_' '?' '_' num
rule token = parse
| [ ' ' '\t' ] { token lexbuf }
| '\n' { Lexing.new_line lexbuf; token lexbuf }
| "NO" { NO }
| "Problem:" { PROBLEM }
| "Proof:" { PROOF }
| "Higher-Order Church Rosser Processor:" { PROCESSOR }
| "Higher-Order Nonconfluence Processor:" { PROCESSOR }
| "non-joinable conversion:" { NONJOIN }
| "Qed" { QED }
| "critical peaks:" { CRITPEAKS }
| "<- . ->" { PEAK }
| "app (lam m_typ (\\v_x. m_F v_x)) m_B -> m_F m_B" {BETA}
| "->*" { ARRS }
| "*<-" { LARRS }
| "->" { ARR }
| "app" { APP }
| "lam" { LAM }
| "pi" { PI }
| '\\' { BACKSLASH }
| '.' { DOT }
| '(' { LPAREN }
| ')' { RPAREN }
| num as s { NUM (s)}
| "c_" (id as s) { CONST (s) }
| "m_?_" num { UNKNOWNMETA }
| "m_" (id as s) { META (s) }
| "v_?" { NOVAR }
| "v_" (id as s) { VAR (s) }
| "<-[" (num | ',')* "]->" { PEAK }
| _ as c { failwith (Printf.sprintf "Unexpected char: '%c'" c) }
| eof { raise End_of_file }
%{
type var = string
type term =
| Lam of (var * term * term)
| App of term * term list
| Var of var
| Pi of (var * term * term)
| Arr of (term * term)
let app t l = match t with
| App (t', l') -> App (t', List.append l l')
| t -> if l = [] then t else App (t, l)
let rec print_term out = function
| Lam (x, ty, t) ->
Printf.fprintf out "%s : %a => %a"
x
print_term_par ty
print_term t
| Pi (x, ty, t) ->
Printf.fprintf out "%s : %a -> %a"
x
print_term_par ty
print_term t
| Arr (ty, t) ->
Printf.fprintf out "%a -> %a"
print_term_par ty
print_term t
| App (t, l) ->
Printf.fprintf out "%a%a"
print_term_par t
(fun out -> List.iter (Printf.fprintf out " %a" print_term_par)) l
| Var x -> Printf.fprintf out "%s" x
and print_term_par out = function
| Var x -> Printf.fprintf out "%s" x
| t -> Printf.fprintf out "(%a)" print_term t
let print_file out (rules, rules', peaks, t1, t2, t3, t4) =
assert (rules = rules');
Printf.fprintf out "%s critical peaks\n" peaks;
if t1 = t2 then
Printf.fprintf out "%a\n" print_term t1
else
Printf.fprintf out "%a\n *<-\n%a\n" print_term t1 print_term t2;
Printf.fprintf out " ==\n";
if t3 = t4 then
Printf.fprintf out "%a\n" print_term t3
else
Printf.fprintf out "%a\n ->*\n%a\n" print_term t3 print_term t4
%}
%token NO PROBLEM PROOF PROCESSOR CRITPEAKS NONJOIN QED BETA
%token APP LAM PI LPAREN RPAREN ARR BACKSLASH DOT LARRS ARRS PEAK UNKNOWNMETA NOVAR
%token <string> VAR CONST META NUM
%start <unit> file
%%
file: NO PROBLEM BETA rules PROOF PROCESSOR BETA rules CRITPEAKS NUM peaks PROCESSOR NONJOIN term LARRS term PEAK term ARRS term QED
{ Printf.printf "%a" print_file ($4, $8, $10, $14, $16, $18, $20) }
rules: { [] }
| rule rules
{ $1 :: $2 }
rule: term ARR term { ($1, 3) }
term: APP term term { app $2 [$3] }
| LPAREN term RPAREN { $2 }
| LAM term LPAREN BACKSLASH VAR DOT term RPAREN { Lam ($5, $2, $7) }
| VAR { Var $1 }
| CONST { Var $1 }
| META { Var $1 }
| UNKNOWNMETA { Var "_" }
| NUM { Var "_" }
| PI term LPAREN BACKSLASH VAR DOT term RPAREN { Pi ($5, $2, $7) }
| PI term LPAREN BACKSLASH NOVAR DOT term RPAREN { Arr ($2, $7) }
peaks: { [] }
| peak peaks { $1 :: $2 }
peak: term PEAK term { ($1, $3) }
%%
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment