diff --git a/external/fixpoint/fixLex.mll b/external/fixpoint/fixLex.mll --- a/external/fixpoint/fixLex.mll +++ b/external/fixpoint/fixLex.mll @@ -161,12 +161,11 @@ | (digit)+ { Num (safe_int_of_string (Lexing.lexeme lexbuf)) } | (alphlet)letdig* { Id (Lexing.lexeme lexbuf) } | '''[^''']*''' { Id (snip_begin_end (Lexing.lexeme lexbuf)) } - | '"'[^''']*'"' { StringLit (snip_begin_end (Lexing.lexeme lexbuf)) } - | eof { EOF } - | _ { - begin + | '"'[^'"']*'"' { StringLit (snip_begin_end (Lexing.lexeme lexbuf)) } + | eof { EOF } + | _ { begin lexerror ("Illegal Character '" ^ (Lexing.lexeme lexbuf) ^ "'") lexbuf; - token lexbuf - end } + token lexbuf + end } diff --git a/external/fixpoint/fixParse.mly b/external/fixpoint/fixParse.mly --- a/external/fixpoint/fixParse.mly +++ b/external/fixpoint/fixParse.mly @@ -18,7 +18,7 @@ | Tycon { So.t_app (So.tycon $1) [] } | Tycon tyconargsne { So.t_app (So.tycon $1) $2 } *) - (* | Id { So.t_ptr (So.Loc $1) } + (* | Id { So.t_ptr (So.Loc $1) } (* pExprs: @@ -276,10 +276,8 @@ | con { A.eCon $1 } | exprs { A.eMExp $1 } | LPAREN expr MOD expr RPAREN { A.eMod ($2, $4) } - | expr PLUS expr { A.eBin ($1, A.Plus, $3) } - | expr MINUS expr { A.eBin ($1, A.Minus, $3) } - | expr TIMES expr { A.eBin ($1, A.Times, $3) } - | expr DIV expr { A.eBin ($1, A.Div, $3) } + | MINUS expr { A.eBin (A.zero, A.Minus, $2) } + | expr op expr { A.eBin ($1, $2, $3) } | expr ops expr { A.eMBin ($1, $2, $3) } | Id LPAREN exprs RPAREN { A.eApp ((Sy.of_string $1), $3) } | Id Id { A.eApp ((Sy.of_string $1), [A.eVar (Sy.of_string $2)]) } diff --git a/external/fixpoint/fixpoint.native-i386-linux b/external/fixpoint/fixpoint.native-i386-linux Binary files a/external/fixpoint/fixpoint.native-i386-linux and b/external/fixpoint/fixpoint.native-i386-linux differ diff --git a/external/fixpoint/fixpoint.native-i686-w64-mingw32 b/external/fixpoint/fixpoint.native-i686-w64-mingw32 # file too large to diff: external/fixpoint/fixpoint.native-i686-w64-mingw32 diff --git a/external/fixpoint/fixpoint.native-x86_64-darwin b/external/fixpoint/fixpoint.native-x86_64-darwin # file too large to diff: external/fixpoint/fixpoint.native-x86_64-darwin diff --git a/external/fixpoint/fixpoint.native-x86_64-linux b/external/fixpoint/fixpoint.native-x86_64-linux # file too large to diff: external/fixpoint/fixpoint.native-x86_64-linux diff --git a/external/fixpoint/foo.ml b/external/fixpoint/foo.ml deleted file mode 100644 --- a/external/fixpoint/foo.ml +++ /dev/null @@ -1,6 +0,0 @@ -let main () - = let co,ci = Unix.open_process "cvc4 --print-success --incremental" in - output_string ci "QUERY TRUE;\n"; - let r = input_line co in - print_endline r -let _ = main () diff --git a/external/ocamlgraph/src/dot_lexer.ml b/external/ocamlgraph/src/dot_lexer.ml deleted file mode 100644 --- a/external/ocamlgraph/src/dot_lexer.ml +++ /dev/null @@ -1,386 +0,0 @@ -# 20 "src/dot_lexer.mll" - - open Lexing - open Dot_ast - open Dot_parser - - let string_buf = Buffer.create 1024 - - let keyword = - let h = Hashtbl.create 17 in - List.iter - (fun (s,k) -> Hashtbl.add h s k) - [ - "strict", STRICT; - "graph", GRAPH; - "digraph", DIGRAPH; - "subgraph", SUBGRAPH; - "node", NODE; - "edge", EDGE; - ]; - fun s -> let s = String.lowercase s in Hashtbl.find h s - - -# 25 "src/dot_lexer.ml" -let __ocaml_lex_tables = { - Lexing.lex_base = - "\000\000\238\255\239\255\240\255\241\255\078\000\088\000\098\000\ - \176\000\245\255\246\255\247\255\248\255\249\255\250\255\251\255\ - \252\255\114\000\001\000\005\000\254\255\002\000\253\255\191\000\ - \244\255\211\000\221\000\157\000\252\255\253\255\002\000\255\255\ - \254\255\032\000\252\255\253\255\254\255\255\255\054\000\253\255\ - \254\255\015\000\255\255"; - Lexing.lex_backtrk = - "\255\255\255\255\255\255\255\255\255\255\013\000\017\000\012\000\ - \017\000\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\017\000\017\000\000\000\255\255\255\255\255\255\255\255\ - \255\255\013\000\013\000\255\255\255\255\255\255\002\000\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\001\000\255\255"; - Lexing.lex_default = - "\001\000\000\000\000\000\000\000\000\000\255\255\255\255\255\255\ - \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\255\255\021\000\255\255\000\000\021\000\000\000\255\255\ - \000\000\255\255\255\255\029\000\000\000\000\000\255\255\000\000\ - \000\000\035\000\000\000\000\000\000\000\000\000\040\000\000\000\ - \000\000\255\255\000\000"; - Lexing.lex_trans = - "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\019\000\019\000\020\000\020\000\019\000\019\000\019\000\ - \000\000\000\000\019\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \019\000\000\000\004\000\018\000\032\000\019\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\015\000\008\000\006\000\017\000\ - \005\000\005\000\005\000\005\000\005\000\005\000\005\000\005\000\ - \005\000\005\000\016\000\014\000\003\000\013\000\042\000\000\000\ - \000\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\010\000\036\000\009\000\037\000\007\000\ - \041\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\012\000\026\000\011\000\005\000\005\000\ - \005\000\005\000\005\000\005\000\005\000\005\000\005\000\005\000\ - \025\000\025\000\025\000\025\000\025\000\025\000\025\000\025\000\ - \025\000\025\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\007\000\022\000\000\000\000\000\000\000\ - \000\000\021\000\000\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\007\000\007\000\000\000\000\000\031\000\ - \000\000\007\000\000\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\007\000\007\000\024\000\023\000\000\000\ - \005\000\005\000\005\000\005\000\005\000\005\000\005\000\005\000\ - \005\000\005\000\000\000\000\000\000\000\000\000\024\000\025\000\ - \025\000\025\000\025\000\025\000\025\000\025\000\025\000\025\000\ - \025\000\030\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \002\000\255\255\255\255\025\000\025\000\025\000\025\000\025\000\ - \025\000\025\000\025\000\025\000\025\000\026\000\026\000\026\000\ - \026\000\026\000\026\000\026\000\026\000\026\000\026\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \034\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\039\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\028\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000"; - Lexing.lex_check = - "\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\000\000\000\000\018\000\021\000\000\000\019\000\019\000\ - \255\255\255\255\019\000\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \000\000\255\255\000\000\000\000\030\000\019\000\255\255\255\255\ - \255\255\255\255\255\255\255\255\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\041\000\255\255\ - \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\033\000\000\000\033\000\000\000\ - \038\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\005\000\000\000\005\000\005\000\ - \005\000\005\000\005\000\005\000\005\000\005\000\005\000\005\000\ - \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\ - \006\000\006\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\007\000\017\000\255\255\255\255\255\255\ - \255\255\017\000\255\255\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\007\000\007\000\255\255\255\255\027\000\ - \255\255\007\000\255\255\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\007\000\007\000\008\000\008\000\255\255\ - \008\000\008\000\008\000\008\000\008\000\008\000\008\000\008\000\ - \008\000\008\000\255\255\255\255\255\255\255\255\008\000\023\000\ - \023\000\023\000\023\000\023\000\023\000\023\000\023\000\023\000\ - \023\000\027\000\255\255\255\255\255\255\255\255\255\255\255\255\ - \000\000\018\000\021\000\025\000\025\000\025\000\025\000\025\000\ - \025\000\025\000\025\000\025\000\025\000\026\000\026\000\026\000\ - \026\000\026\000\026\000\026\000\026\000\026\000\026\000\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \033\000\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\038\000\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\027\000\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255"; - Lexing.lex_base_code = - ""; - Lexing.lex_backtrk_code = - ""; - Lexing.lex_default_code = - ""; - Lexing.lex_trans_code = - ""; - Lexing.lex_check_code = - ""; - Lexing.lex_code = - ""; -} - -let rec token lexbuf = - __ocaml_lex_token_rec lexbuf 0 -and __ocaml_lex_token_rec lexbuf __ocaml_lex_state = - match Lexing.engine __ocaml_lex_tables __ocaml_lex_state lexbuf with - | 0 -> -# 52 "src/dot_lexer.mll" - ( token lexbuf ) -# 191 "src/dot_lexer.ml" - - | 1 -> -# 54 "src/dot_lexer.mll" - ( token lexbuf ) -# 196 "src/dot_lexer.ml" - - | 2 -> -# 56 "src/dot_lexer.mll" - ( comment lexbuf; token lexbuf ) -# 201 "src/dot_lexer.ml" - - | 3 -> -# 58 "src/dot_lexer.mll" - ( COLON ) -# 206 "src/dot_lexer.ml" - - | 4 -> -# 60 "src/dot_lexer.mll" - ( COMMA ) -# 211 "src/dot_lexer.ml" - - | 5 -> -# 62 "src/dot_lexer.mll" - ( SEMICOLON ) -# 216 "src/dot_lexer.ml" - - | 6 -> -# 64 "src/dot_lexer.mll" - ( EQUAL ) -# 221 "src/dot_lexer.ml" - - | 7 -> -# 66 "src/dot_lexer.mll" - ( LBRA ) -# 226 "src/dot_lexer.ml" - - | 8 -> -# 68 "src/dot_lexer.mll" - ( RBRA ) -# 231 "src/dot_lexer.ml" - - | 9 -> -# 70 "src/dot_lexer.mll" - ( LSQ ) -# 236 "src/dot_lexer.ml" - - | 10 -> -# 72 "src/dot_lexer.mll" - ( RSQ ) -# 241 "src/dot_lexer.ml" - - | 11 -> -# 74 "src/dot_lexer.mll" - ( EDGEOP ) -# 246 "src/dot_lexer.ml" - - | 12 -> -let -# 75 "src/dot_lexer.mll" - s -# 252 "src/dot_lexer.ml" -= Lexing.sub_lexeme lexbuf lexbuf.Lexing.lex_start_pos lexbuf.Lexing.lex_curr_pos in -# 76 "src/dot_lexer.mll" - ( try keyword s with Not_found -> ID (Ident s) ) -# 256 "src/dot_lexer.ml" - - | 13 -> -let -# 77 "src/dot_lexer.mll" - s -# 262 "src/dot_lexer.ml" -= Lexing.sub_lexeme lexbuf lexbuf.Lexing.lex_start_pos lexbuf.Lexing.lex_curr_pos in -# 78 "src/dot_lexer.mll" - ( ID (Number s) ) -# 266 "src/dot_lexer.ml" - - | 14 -> -# 80 "src/dot_lexer.mll" - ( Buffer.clear string_buf; - let s = string lexbuf in - ID (String s) ) -# 273 "src/dot_lexer.ml" - - | 15 -> -# 84 "src/dot_lexer.mll" - ( Buffer.clear string_buf; - html lexbuf; - ID (Html (Buffer.contents string_buf)) ) -# 280 "src/dot_lexer.ml" - - | 16 -> -# 88 "src/dot_lexer.mll" - ( EOF ) -# 285 "src/dot_lexer.ml" - - | 17 -> -let -# 89 "src/dot_lexer.mll" - c -# 291 "src/dot_lexer.ml" -= Lexing.sub_lexeme_char lexbuf lexbuf.Lexing.lex_start_pos in -# 90 "src/dot_lexer.mll" - ( failwith ("Dot_lexer: invalid character " ^ String.make 1 c) ) -# 295 "src/dot_lexer.ml" - - | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_token_rec lexbuf __ocaml_lex_state - -and string lexbuf = - __ocaml_lex_string_rec lexbuf 27 -and __ocaml_lex_string_rec lexbuf __ocaml_lex_state = - match Lexing.engine __ocaml_lex_tables __ocaml_lex_state lexbuf with - | 0 -> -# 94 "src/dot_lexer.mll" - ( Buffer.contents string_buf ) -# 306 "src/dot_lexer.ml" - - | 1 -> -# 96 "src/dot_lexer.mll" - ( Buffer.add_char string_buf '"'; - string lexbuf ) -# 312 "src/dot_lexer.ml" - - | 2 -> -let -# 98 "src/dot_lexer.mll" - c -# 318 "src/dot_lexer.ml" -= Lexing.sub_lexeme_char lexbuf lexbuf.Lexing.lex_start_pos in -# 99 "src/dot_lexer.mll" - ( Buffer.add_char string_buf c; - string lexbuf ) -# 323 "src/dot_lexer.ml" - - | 3 -> -# 102 "src/dot_lexer.mll" - ( failwith ("Dot_lexer: unterminated string literal") ) -# 328 "src/dot_lexer.ml" - - | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_string_rec lexbuf __ocaml_lex_state - -and html lexbuf = - __ocaml_lex_html_rec lexbuf 33 -and __ocaml_lex_html_rec lexbuf __ocaml_lex_state = - match Lexing.engine __ocaml_lex_tables __ocaml_lex_state lexbuf with - | 0 -> -# 106 "src/dot_lexer.mll" - ( () ) -# 339 "src/dot_lexer.ml" - - | 1 -> -# 108 "src/dot_lexer.mll" - ( Buffer.add_char string_buf '<'; html lexbuf; - Buffer.add_char string_buf '>'; html lexbuf ) -# 345 "src/dot_lexer.ml" - - | 2 -> -let -# 110 "src/dot_lexer.mll" - c -# 351 "src/dot_lexer.ml" -= Lexing.sub_lexeme_char lexbuf lexbuf.Lexing.lex_start_pos in -# 111 "src/dot_lexer.mll" - ( Buffer.add_char string_buf c; - html lexbuf ) -# 356 "src/dot_lexer.ml" - - | 3 -> -# 114 "src/dot_lexer.mll" - ( failwith ("Dot_lexer: unterminated html literal") ) -# 361 "src/dot_lexer.ml" - - | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_html_rec lexbuf __ocaml_lex_state - -and comment lexbuf = - __ocaml_lex_comment_rec lexbuf 38 -and __ocaml_lex_comment_rec lexbuf __ocaml_lex_state = - match Lexing.engine __ocaml_lex_tables __ocaml_lex_state lexbuf with - | 0 -> -# 118 "src/dot_lexer.mll" - ( () ) -# 372 "src/dot_lexer.ml" - - | 1 -> -# 120 "src/dot_lexer.mll" - ( comment lexbuf ) -# 377 "src/dot_lexer.ml" - - | 2 -> -# 122 "src/dot_lexer.mll" - ( failwith "Dot_lexer: unterminated comment" ) -# 382 "src/dot_lexer.ml" - - | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_comment_rec lexbuf __ocaml_lex_state - -;; - diff --git a/external/ocamlgraph/src/dot_parser.ml b/external/ocamlgraph/src/dot_parser.ml deleted file mode 100644 --- a/external/ocamlgraph/src/dot_parser.ml +++ /dev/null @@ -1,551 +0,0 @@ -type token = - | ID of (Dot_ast.id) - | COLON - | COMMA - | EQUAL - | SEMICOLON - | EDGEOP - | STRICT - | GRAPH - | DIGRAPH - | LBRA - | RBRA - | LSQ - | RSQ - | NODE - | EDGE - | SUBGRAPH - | EOF - -open Parsing;; -# 23 "src/dot_parser.mly" - open Dot_ast - open Parsing - - let compass_pt = function - | Ident "n" -> N - | Ident "ne" -> Ne - | Ident "e" -> E - | Ident "se" -> Se - | Ident "s" -> S - | Ident "sw" -> Sw - | Ident "w" -> W - | Ident "nw" -> Nw - | _ -> invalid_arg "compass_pt" - -# 37 "src/dot_parser.ml" -let yytransl_const = [| - 258 (* COLON *); - 259 (* COMMA *); - 260 (* EQUAL *); - 261 (* SEMICOLON *); - 262 (* EDGEOP *); - 263 (* STRICT *); - 264 (* GRAPH *); - 265 (* DIGRAPH *); - 266 (* LBRA *); - 267 (* RBRA *); - 268 (* LSQ *); - 269 (* RSQ *); - 270 (* NODE *); - 271 (* EDGE *); - 272 (* SUBGRAPH *); - 0 (* EOF *); - 0|] - -let yytransl_block = [| - 257 (* ID *); - 0|] - -let yylhs = "\255\255\ -\001\000\002\000\002\000\003\000\003\000\005\000\005\000\006\000\ -\006\000\008\000\008\000\007\000\007\000\007\000\007\000\007\000\ -\009\000\010\000\011\000\011\000\011\000\016\000\018\000\018\000\ -\015\000\015\000\013\000\019\000\019\000\020\000\020\000\014\000\ -\014\000\017\000\017\000\004\000\004\000\021\000\021\000\022\000\ -\022\000\023\000\023\000\012\000\012\000\012\000\012\000\000\000" - -let yylen = "\002\000\ -\007\000\000\000\001\000\001\000\001\000\000\000\001\000\002\000\ -\003\000\000\000\001\000\001\000\001\000\001\000\003\000\001\000\ -\002\000\003\000\002\000\002\000\002\000\003\000\000\000\003\000\ -\001\000\001\000\002\000\000\000\001\000\002\000\004\000\000\000\ -\001\000\003\000\004\000\000\000\001\000\002\000\003\000\001\000\ -\003\000\000\000\001\000\002\000\005\000\004\000\003\000\002\000" - -let yydefred = "\000\000\ -\000\000\000\000\003\000\048\000\000\000\004\000\005\000\000\000\ -\037\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ -\000\000\000\000\007\000\000\000\012\000\013\000\014\000\000\000\ -\000\000\000\000\000\000\000\000\027\000\029\000\000\000\019\000\ -\000\000\020\000\021\000\000\000\000\000\000\000\011\000\000\000\ -\017\000\033\000\000\000\000\000\000\000\015\000\000\000\000\000\ -\000\000\047\000\000\000\000\000\001\000\009\000\000\000\026\000\ -\025\000\000\000\018\000\000\000\000\000\000\000\043\000\000\000\ -\000\000\046\000\000\000\022\000\031\000\041\000\035\000\039\000\ -\045\000\000\000\024\000" - -let yydgoto = "\002\000\ -\004\000\005\000\008\000\010\000\018\000\019\000\020\000\040\000\ -\021\000\022\000\023\000\024\000\025\000\041\000\026\000\044\000\ -\042\000\068\000\029\000\030\000\048\000\049\000\064\000" - -let yysindex = "\009\000\ -\024\255\000\000\000\000\000\000\000\255\000\000\000\000\031\255\ -\000\000\029\255\131\255\011\255\033\255\131\255\033\255\033\255\ -\051\255\040\255\000\000\048\255\000\000\000\000\000\000\000\000\ -\033\255\050\255\057\255\067\255\000\000\000\000\069\255\000\000\ -\062\255\000\000\000\000\070\255\131\255\091\000\000\000\131\255\ -\000\000\000\000\018\255\033\255\090\255\000\000\099\255\081\255\ -\101\255\000\000\131\255\095\255\000\000\000\000\107\255\000\000\ -\000\000\110\255\000\000\114\255\117\255\033\255\000\000\069\255\ -\111\255\000\000\018\255\000\000\000\000\000\000\000\000\000\000\ -\000\000\110\255\000\000" - -let yyrindex = "\000\000\ -\074\255\000\000\000\000\000\000\000\000\000\000\000\000\116\255\ -\000\000\000\000\118\255\006\255\000\000\118\255\000\000\000\000\ -\000\000\000\000\000\000\120\255\000\000\000\000\000\000\049\255\ -\061\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ -\000\000\000\000\000\000\073\255\118\255\000\000\000\000\122\255\ -\000\000\000\000\000\000\097\255\032\255\000\000\023\255\000\000\ -\022\255\000\000\118\255\000\000\000\000\000\000\006\255\000\000\ -\000\000\085\255\000\000\000\000\000\000\109\255\000\000\124\255\ -\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ -\000\000\085\255\000\000" - -let yygindex = "\000\000\ -\000\000\000\000\000\000\000\000\246\255\087\000\000\000\000\000\ -\000\000\000\000\000\000\214\255\218\255\094\000\219\255\000\000\ -\243\255\066\000\000\000\000\000\078\000\000\000\000\000" - -let yytablesize = 147 -let yytable = "\032\000\ -\056\000\034\000\035\000\033\000\057\000\058\000\028\000\006\000\ -\007\000\001\000\028\000\028\000\027\000\028\000\028\000\028\000\ -\028\000\028\000\055\000\028\000\028\000\028\000\042\000\040\000\ -\056\000\040\000\052\000\014\000\057\000\074\000\003\000\009\000\ -\030\000\017\000\042\000\040\000\030\000\030\000\011\000\030\000\ -\065\000\030\000\030\000\030\000\031\000\030\000\030\000\030\000\ -\071\000\016\000\038\000\036\000\039\000\016\000\026\000\043\000\ -\016\000\045\000\016\000\016\000\037\000\032\000\016\000\016\000\ -\016\000\032\000\025\000\046\000\032\000\047\000\032\000\032\000\ -\050\000\044\000\032\000\032\000\032\000\044\000\044\000\051\000\ -\044\000\002\000\002\000\044\000\044\000\023\000\044\000\044\000\ -\044\000\023\000\053\000\060\000\023\000\062\000\023\000\023\000\ -\023\000\032\000\023\000\023\000\023\000\032\000\061\000\063\000\ -\032\000\066\000\032\000\032\000\027\000\034\000\032\000\032\000\ -\032\000\034\000\069\000\067\000\034\000\070\000\034\000\034\000\ -\010\000\073\000\034\000\034\000\034\000\036\000\054\000\010\000\ -\006\000\010\000\010\000\012\000\008\000\010\000\010\000\010\000\ -\038\000\059\000\013\000\075\000\014\000\072\000\000\000\000\000\ -\015\000\016\000\017\000" - -let yycheck = "\013\000\ -\043\000\015\000\016\000\014\000\043\000\043\000\001\001\008\001\ -\009\001\001\000\005\001\006\001\002\001\008\001\004\001\010\001\ -\011\001\012\001\001\001\014\001\015\001\016\001\001\001\001\001\ -\067\000\003\001\037\000\010\001\067\000\067\000\007\001\001\001\ -\001\001\016\001\013\001\013\001\005\001\006\001\010\001\008\001\ -\051\000\010\001\011\001\012\001\012\001\014\001\015\001\016\001\ -\062\000\001\001\011\001\001\001\005\001\005\001\006\001\006\001\ -\008\001\001\001\010\001\011\001\010\001\001\001\014\001\015\001\ -\016\001\005\001\006\001\001\001\008\001\001\001\010\001\011\001\ -\011\001\001\001\014\001\015\001\016\001\005\001\006\001\010\001\ -\008\001\008\001\009\001\011\001\012\001\001\001\014\001\015\001\ -\016\001\005\001\000\000\002\001\008\001\013\001\010\001\011\001\ -\012\001\001\001\014\001\015\001\016\001\005\001\004\001\003\001\ -\008\001\011\001\010\001\011\001\002\001\001\001\014\001\015\001\ -\016\001\005\001\001\001\006\001\008\001\001\001\010\001\011\001\ -\001\001\011\001\014\001\015\001\016\001\010\001\040\000\008\001\ -\011\001\010\001\011\001\001\001\011\001\014\001\015\001\016\001\ -\013\001\044\000\008\001\074\000\010\001\064\000\255\255\255\255\ -\014\001\015\001\016\001" - -let yynames_const = "\ - COLON\000\ - COMMA\000\ - EQUAL\000\ - SEMICOLON\000\ - EDGEOP\000\ - STRICT\000\ - GRAPH\000\ - DIGRAPH\000\ - LBRA\000\ - RBRA\000\ - LSQ\000\ - RSQ\000\ - NODE\000\ - EDGE\000\ - SUBGRAPH\000\ - EOF\000\ - " - -let yynames_block = "\ - ID\000\ - " - -let yyact = [| - (fun _ -> failwith "parser") -; (fun __caml_parser_env -> - let _1 = (Parsing.peek_val __caml_parser_env 6 : 'strict_opt) in - let _2 = (Parsing.peek_val __caml_parser_env 5 : 'graph_or_digraph) in - let _3 = (Parsing.peek_val __caml_parser_env 4 : 'id_opt) in - let _5 = (Parsing.peek_val __caml_parser_env 2 : 'stmt_list) in - Obj.repr( -# 49 "src/dot_parser.mly" - ( { strict = _1; digraph = _2; id = _3; stmts = _5 } ) -# 199 "src/dot_parser.ml" - : Dot_ast.file)) -; (fun __caml_parser_env -> - Obj.repr( -# 53 "src/dot_parser.mly" - ( false ) -# 205 "src/dot_parser.ml" - : 'strict_opt)) -; (fun __caml_parser_env -> - Obj.repr( -# 54 "src/dot_parser.mly" - ( true ) -# 211 "src/dot_parser.ml" - : 'strict_opt)) -; (fun __caml_parser_env -> - Obj.repr( -# 58 "src/dot_parser.mly" - ( false ) -# 217 "src/dot_parser.ml" - : 'graph_or_digraph)) -; (fun __caml_parser_env -> - Obj.repr( -# 59 "src/dot_parser.mly" - ( true ) -# 223 "src/dot_parser.ml" - : 'graph_or_digraph)) -; (fun __caml_parser_env -> - Obj.repr( -# 63 "src/dot_parser.mly" - ( [] ) -# 229 "src/dot_parser.ml" - : 'stmt_list)) -; (fun __caml_parser_env -> - let _1 = (Parsing.peek_val __caml_parser_env 0 : 'list1_stmt) in - Obj.repr( -# 64 "src/dot_parser.mly" - ( _1 ) -# 236 "src/dot_parser.ml" - : 'stmt_list)) -; (fun __caml_parser_env -> - let _1 = (Parsing.peek_val __caml_parser_env 1 : 'stmt) in - let _2 = (Parsing.peek_val __caml_parser_env 0 : 'semicolon_opt) in - Obj.repr( -# 68 "src/dot_parser.mly" - ( [_1] ) -# 244 "src/dot_parser.ml" - : 'list1_stmt)) -; (fun __caml_parser_env -> - let _1 = (Parsing.peek_val __caml_parser_env 2 : 'stmt) in - let _2 = (Parsing.peek_val __caml_parser_env 1 : 'semicolon_opt) in - let _3 = (Parsing.peek_val __caml_parser_env 0 : 'list1_stmt) in - Obj.repr( -# 69 "src/dot_parser.mly" - ( _1 :: _3 ) -# 253 "src/dot_parser.ml" - : 'list1_stmt)) -; (fun __caml_parser_env -> - Obj.repr( -# 73 "src/dot_parser.mly" - ( () ) -# 259 "src/dot_parser.ml" - : 'semicolon_opt)) -; (fun __caml_parser_env -> - Obj.repr( -# 74 "src/dot_parser.mly" - ( () ) -# 265 "src/dot_parser.ml" - : 'semicolon_opt)) -; (fun __caml_parser_env -> - let _1 = (Parsing.peek_val __caml_parser_env 0 : 'node_stmt) in - Obj.repr( -# 78 "src/dot_parser.mly" - ( _1 ) -# 272 "src/dot_parser.ml" - : 'stmt)) -; (fun __caml_parser_env -> - let _1 = (Parsing.peek_val __caml_parser_env 0 : 'edge_stmt) in - Obj.repr( -# 79 "src/dot_parser.mly" - ( _1 ) -# 279 "src/dot_parser.ml" - : 'stmt)) -; (fun __caml_parser_env -> - let _1 = (Parsing.peek_val __caml_parser_env 0 : 'attr_stmt) in - Obj.repr( -# 80 "src/dot_parser.mly" - ( _1 ) -# 286 "src/dot_parser.ml" - : 'stmt)) -; (fun __caml_parser_env -> - let _1 = (Parsing.peek_val __caml_parser_env 2 : Dot_ast.id) in - let _3 = (Parsing.peek_val __caml_parser_env 0 : Dot_ast.id) in - Obj.repr( -# 81 "src/dot_parser.mly" - ( Equal (_1, _3) ) -# 294 "src/dot_parser.ml" - : 'stmt)) -; (fun __caml_parser_env -> - let _1 = (Parsing.peek_val __caml_parser_env 0 : 'subgraph) in - Obj.repr( -# 82 "src/dot_parser.mly" - ( Subgraph _1 ) -# 301 "src/dot_parser.ml" - : 'stmt)) -; (fun __caml_parser_env -> - let _1 = (Parsing.peek_val __caml_parser_env 1 : 'node_id) in - let _2 = (Parsing.peek_val __caml_parser_env 0 : 'attr_list_opt) in - Obj.repr( -# 86 "src/dot_parser.mly" - ( Node_stmt (_1, _2) ) -# 309 "src/dot_parser.ml" - : 'node_stmt)) -; (fun __caml_parser_env -> - let _1 = (Parsing.peek_val __caml_parser_env 2 : 'node) in - let _2 = (Parsing.peek_val __caml_parser_env 1 : 'edge_rhs) in - let _3 = (Parsing.peek_val __caml_parser_env 0 : 'attr_list_opt) in - Obj.repr( -# 90 "src/dot_parser.mly" - ( Edge_stmt (_1, _2, _3) ) -# 318 "src/dot_parser.ml" - : 'edge_stmt)) -; (fun __caml_parser_env -> - let _2 = (Parsing.peek_val __caml_parser_env 0 : 'attr_list) in - Obj.repr( -# 94 "src/dot_parser.mly" - ( Attr_graph _2 ) -# 325 "src/dot_parser.ml" - : 'attr_stmt)) -; (fun __caml_parser_env -> - let _2 = (Parsing.peek_val __caml_parser_env 0 : 'attr_list) in - Obj.repr( -# 95 "src/dot_parser.mly" - ( Attr_node _2 ) -# 332 "src/dot_parser.ml" - : 'attr_stmt)) -; (fun __caml_parser_env -> - let _2 = (Parsing.peek_val __caml_parser_env 0 : 'attr_list) in - Obj.repr( -# 96 "src/dot_parser.mly" - ( Attr_edge _2 ) -# 339 "src/dot_parser.ml" - : 'attr_stmt)) -; (fun __caml_parser_env -> - let _2 = (Parsing.peek_val __caml_parser_env 1 : 'node) in - let _3 = (Parsing.peek_val __caml_parser_env 0 : 'edge_rhs_opt) in - Obj.repr( -# 100 "src/dot_parser.mly" - ( _2 :: _3 ) -# 347 "src/dot_parser.ml" - : 'edge_rhs)) -; (fun __caml_parser_env -> - Obj.repr( -# 104 "src/dot_parser.mly" - ( [] ) -# 353 "src/dot_parser.ml" - : 'edge_rhs_opt)) -; (fun __caml_parser_env -> - let _2 = (Parsing.peek_val __caml_parser_env 1 : 'node) in - let _3 = (Parsing.peek_val __caml_parser_env 0 : 'edge_rhs_opt) in - Obj.repr( -# 105 "src/dot_parser.mly" - ( _2 :: _3 ) -# 361 "src/dot_parser.ml" - : 'edge_rhs_opt)) -; (fun __caml_parser_env -> - let _1 = (Parsing.peek_val __caml_parser_env 0 : 'node_id) in - Obj.repr( -# 109 "src/dot_parser.mly" - ( NodeId _1 ) -# 368 "src/dot_parser.ml" - : 'node)) -; (fun __caml_parser_env -> - let _1 = (Parsing.peek_val __caml_parser_env 0 : 'subgraph) in - Obj.repr( -# 110 "src/dot_parser.mly" - ( NodeSub _1 ) -# 375 "src/dot_parser.ml" - : 'node)) -; (fun __caml_parser_env -> - let _1 = (Parsing.peek_val __caml_parser_env 1 : Dot_ast.id) in - let _2 = (Parsing.peek_val __caml_parser_env 0 : 'port_opt) in - Obj.repr( -# 114 "src/dot_parser.mly" - ( _1, _2 ) -# 383 "src/dot_parser.ml" - : 'node_id)) -; (fun __caml_parser_env -> - Obj.repr( -# 118 "src/dot_parser.mly" - ( None ) -# 389 "src/dot_parser.ml" - : 'port_opt)) -; (fun __caml_parser_env -> - let _1 = (Parsing.peek_val __caml_parser_env 0 : 'port) in - Obj.repr( -# 119 "src/dot_parser.mly" - ( Some _1 ) -# 396 "src/dot_parser.ml" - : 'port_opt)) -; (fun __caml_parser_env -> - let _2 = (Parsing.peek_val __caml_parser_env 0 : Dot_ast.id) in - Obj.repr( -# 123 "src/dot_parser.mly" - ( try PortC (compass_pt _2) - with Invalid_argument _ -> PortId (_2, None) ) -# 404 "src/dot_parser.ml" - : 'port)) -; (fun __caml_parser_env -> - let _2 = (Parsing.peek_val __caml_parser_env 2 : Dot_ast.id) in - let _4 = (Parsing.peek_val __caml_parser_env 0 : Dot_ast.id) in - Obj.repr( -# 126 "src/dot_parser.mly" - ( let cp = - try compass_pt _4 with Invalid_argument _ -> raise Parse_error - in - PortId (_2, Some cp) ) -# 415 "src/dot_parser.ml" - : 'port)) -; (fun __caml_parser_env -> - Obj.repr( -# 133 "src/dot_parser.mly" - ( [] ) -# 421 "src/dot_parser.ml" - : 'attr_list_opt)) -; (fun __caml_parser_env -> - let _1 = (Parsing.peek_val __caml_parser_env 0 : 'attr_list) in - Obj.repr( -# 134 "src/dot_parser.mly" - ( _1 ) -# 428 "src/dot_parser.ml" - : 'attr_list_opt)) -; (fun __caml_parser_env -> - let _2 = (Parsing.peek_val __caml_parser_env 1 : 'a_list) in - Obj.repr( -# 138 "src/dot_parser.mly" - ( [_2] ) -# 435 "src/dot_parser.ml" - : 'attr_list)) -; (fun __caml_parser_env -> - let _2 = (Parsing.peek_val __caml_parser_env 2 : 'a_list) in - let _4 = (Parsing.peek_val __caml_parser_env 0 : 'attr_list) in - Obj.repr( -# 139 "src/dot_parser.mly" - ( _2 :: _4 ) -# 443 "src/dot_parser.ml" - : 'attr_list)) -; (fun __caml_parser_env -> - Obj.repr( -# 143 "src/dot_parser.mly" - ( None ) -# 449 "src/dot_parser.ml" - : 'id_opt)) -; (fun __caml_parser_env -> - let _1 = (Parsing.peek_val __caml_parser_env 0 : Dot_ast.id) in - Obj.repr( -# 144 "src/dot_parser.mly" - ( Some _1 ) -# 456 "src/dot_parser.ml" - : 'id_opt)) -; (fun __caml_parser_env -> - let _1 = (Parsing.peek_val __caml_parser_env 1 : 'equality) in - let _2 = (Parsing.peek_val __caml_parser_env 0 : 'comma_opt) in - Obj.repr( -# 148 "src/dot_parser.mly" - ( [_1] ) -# 464 "src/dot_parser.ml" - : 'a_list)) -; (fun __caml_parser_env -> - let _1 = (Parsing.peek_val __caml_parser_env 2 : 'equality) in - let _2 = (Parsing.peek_val __caml_parser_env 1 : 'comma_opt) in - let _3 = (Parsing.peek_val __caml_parser_env 0 : 'a_list) in - Obj.repr( -# 149 "src/dot_parser.mly" - ( _1 :: _3 ) -# 473 "src/dot_parser.ml" - : 'a_list)) -; (fun __caml_parser_env -> - let _1 = (Parsing.peek_val __caml_parser_env 0 : Dot_ast.id) in - Obj.repr( -# 153 "src/dot_parser.mly" - ( _1, None ) -# 480 "src/dot_parser.ml" - : 'equality)) -; (fun __caml_parser_env -> - let _1 = (Parsing.peek_val __caml_parser_env 2 : Dot_ast.id) in - let _3 = (Parsing.peek_val __caml_parser_env 0 : Dot_ast.id) in - Obj.repr( -# 154 "src/dot_parser.mly" - ( _1, Some _3 ) -# 488 "src/dot_parser.ml" - : 'equality)) -; (fun __caml_parser_env -> - Obj.repr( -# 158 "src/dot_parser.mly" - ( () ) -# 494 "src/dot_parser.ml" - : 'comma_opt)) -; (fun __caml_parser_env -> - Obj.repr( -# 159 "src/dot_parser.mly" - ( () ) -# 500 "src/dot_parser.ml" - : 'comma_opt)) -; (fun __caml_parser_env -> - let _2 = (Parsing.peek_val __caml_parser_env 0 : Dot_ast.id) in - Obj.repr( -# 164 "src/dot_parser.mly" - ( SubgraphId _2 ) -# 507 "src/dot_parser.ml" - : 'subgraph)) -; (fun __caml_parser_env -> - let _2 = (Parsing.peek_val __caml_parser_env 3 : Dot_ast.id) in - let _4 = (Parsing.peek_val __caml_parser_env 1 : 'stmt_list) in - Obj.repr( -# 165 "src/dot_parser.mly" - ( SubgraphDef (Some _2, _4) ) -# 515 "src/dot_parser.ml" - : 'subgraph)) -; (fun __caml_parser_env -> - let _3 = (Parsing.peek_val __caml_parser_env 1 : 'stmt_list) in - Obj.repr( -# 166 "src/dot_parser.mly" - ( SubgraphDef (None, _3) ) -# 522 "src/dot_parser.ml" - : 'subgraph)) -; (fun __caml_parser_env -> - let _2 = (Parsing.peek_val __caml_parser_env 1 : 'stmt_list) in - Obj.repr( -# 167 "src/dot_parser.mly" - ( SubgraphDef (None, _2) ) -# 529 "src/dot_parser.ml" - : 'subgraph)) -(* Entry file *) -; (fun __caml_parser_env -> raise (Parsing.YYexit (Parsing.peek_val __caml_parser_env 0))) -|] -let yytables = - { Parsing.actions=yyact; - Parsing.transl_const=yytransl_const; - Parsing.transl_block=yytransl_block; - Parsing.lhs=yylhs; - Parsing.len=yylen; - Parsing.defred=yydefred; - Parsing.dgoto=yydgoto; - Parsing.sindex=yysindex; - Parsing.rindex=yyrindex; - Parsing.gindex=yygindex; - Parsing.tablesize=yytablesize; - Parsing.table=yytable; - Parsing.check=yycheck; - Parsing.error_function=parse_error; - Parsing.names_const=yynames_const; - Parsing.names_block=yynames_block } -let file (lexfun : Lexing.lexbuf -> token) (lexbuf : Lexing.lexbuf) = - (Parsing.yyparse yytables 1 lexfun lexbuf : Dot_ast.file) diff --git a/external/ocamlgraph/src/dot_parser.mli b/external/ocamlgraph/src/dot_parser.mli deleted file mode 100644 --- a/external/ocamlgraph/src/dot_parser.mli +++ /dev/null @@ -1,21 +0,0 @@ -type token = - | ID of (Dot_ast.id) - | COLON - | COMMA - | EQUAL - | SEMICOLON - | EDGEOP - | STRICT - | GRAPH - | DIGRAPH - | LBRA - | RBRA - | LSQ - | RSQ - | NODE - | EDGE - | SUBGRAPH - | EOF - -val file : - (Lexing.lexbuf -> token) -> Lexing.lexbuf -> Dot_ast.file diff --git a/external/ocamlgraph/src/gml.ml b/external/ocamlgraph/src/gml.ml deleted file mode 100644 --- a/external/ocamlgraph/src/gml.ml +++ /dev/null @@ -1,670 +0,0 @@ -# 20 "src/gml.mll" - - - open Lexing - - type value = - | Int of int - | Float of float - | String of string - | List of value_list - - and value_list = (string * value) list - - -# 16 "src/gml.ml" -let __ocaml_lex_tables = { - Lexing.lex_base = - "\000\000\252\255\253\255\114\000\002\000\007\000\228\000\086\001\ - \252\255\253\255\200\001\009\000\014\000\058\002\002\000\251\255\ - \252\255\001\000\080\000\102\000\194\000\216\000\052\001\071\001\ - \253\255\006\000"; - Lexing.lex_backtrk = - "\255\255\255\255\255\255\003\000\000\000\001\000\255\255\255\255\ - \255\255\255\255\003\000\000\000\001\000\255\255\255\255\255\255\ - \255\255\004\000\001\000\000\000\004\000\255\255\001\000\255\255\ - \255\255\255\255"; - Lexing.lex_default = - "\001\000\000\000\000\000\255\255\255\255\255\255\255\255\008\000\ - \000\000\000\000\255\255\255\255\255\255\255\255\015\000\000\000\ - \000\000\025\000\255\255\255\255\255\255\255\255\255\255\255\255\ - \000\000\025\000"; - Lexing.lex_trans = - "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\004\000\004\000\004\000\004\000\004\000\000\000\004\000\ - \005\000\005\000\011\000\011\000\005\000\000\000\011\000\012\000\ - \012\000\000\000\000\000\012\000\000\000\000\000\000\000\000\000\ - \004\000\000\000\004\000\024\000\017\000\000\000\000\000\005\000\ - \024\000\011\000\000\000\000\000\000\000\020\000\012\000\020\000\ - \018\000\000\000\019\000\019\000\019\000\019\000\019\000\019\000\ - \019\000\019\000\019\000\019\000\000\000\000\000\000\000\000\000\ - \000\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\ - \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\ - \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\ - \003\000\003\000\003\000\000\000\000\000\016\000\000\000\000\000\ - \000\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\ - \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\ - \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\ - \003\000\003\000\003\000\005\000\005\000\000\000\000\000\005\000\ - \018\000\018\000\018\000\018\000\018\000\018\000\018\000\018\000\ - \018\000\018\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\005\000\000\000\018\000\021\000\019\000\019\000\ - \019\000\019\000\019\000\019\000\019\000\019\000\019\000\019\000\ - \000\000\000\000\006\000\006\000\006\000\006\000\006\000\006\000\ - \006\000\006\000\006\000\006\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\006\000\006\000\006\000\006\000\006\000\ - \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\ - \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\ - \006\000\006\000\006\000\006\000\006\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\006\000\006\000\006\000\006\000\006\000\ - \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\ - \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\ - \006\000\006\000\006\000\006\000\006\000\005\000\005\000\000\000\ - \018\000\005\000\019\000\019\000\019\000\019\000\019\000\019\000\ - \019\000\019\000\019\000\019\000\000\000\000\000\000\000\000\000\ - \002\000\255\255\255\255\023\000\005\000\023\000\255\255\000\000\ - \022\000\022\000\022\000\022\000\022\000\022\000\022\000\022\000\ - \022\000\022\000\000\000\000\000\006\000\006\000\006\000\006\000\ - \006\000\006\000\006\000\006\000\006\000\006\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\006\000\006\000\006\000\ - \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\ - \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\ - \006\000\006\000\006\000\006\000\006\000\006\000\006\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\006\000\006\000\006\000\ - \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\ - \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\ - \006\000\006\000\006\000\006\000\006\000\006\000\006\000\011\000\ - \011\000\000\000\000\000\011\000\022\000\022\000\022\000\022\000\ - \022\000\022\000\022\000\022\000\022\000\022\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\011\000\022\000\ - \022\000\022\000\022\000\022\000\022\000\022\000\022\000\022\000\ - \022\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\010\000\ - \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\ - \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\ - \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\ - \010\000\000\000\000\000\009\000\000\000\000\000\000\000\010\000\ - \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\ - \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\ - \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\ - \010\000\012\000\012\000\000\000\000\000\012\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \012\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\ - \013\000\013\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\ - \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\ - \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\ - \013\000\013\000\013\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\ - \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\ - \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\ - \013\000\013\000\013\000\012\000\012\000\000\000\000\000\012\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\255\255\000\000\ - \000\000\000\000\012\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\013\000\013\000\013\000\013\000\013\000\013\000\ - \013\000\013\000\013\000\013\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\013\000\013\000\013\000\013\000\013\000\ - \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\ - \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\ - \013\000\013\000\013\000\013\000\013\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\013\000\013\000\013\000\013\000\013\000\ - \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\ - \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\ - \013\000\013\000\013\000\013\000\013\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000"; - Lexing.lex_check = - "\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\000\000\000\000\004\000\004\000\000\000\255\255\004\000\ - \005\000\005\000\011\000\011\000\005\000\255\255\011\000\012\000\ - \012\000\255\255\255\255\012\000\255\255\255\255\255\255\255\255\ - \000\000\255\255\004\000\017\000\014\000\255\255\255\255\005\000\ - \025\000\011\000\255\255\255\255\255\255\014\000\012\000\014\000\ - \014\000\255\255\014\000\014\000\014\000\014\000\014\000\014\000\ - \014\000\014\000\014\000\014\000\255\255\255\255\255\255\255\255\ - \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\255\255\255\255\014\000\255\255\255\255\ - \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\003\000\003\000\255\255\255\255\003\000\ - \018\000\018\000\018\000\018\000\018\000\018\000\018\000\018\000\ - \018\000\018\000\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\003\000\255\255\019\000\018\000\019\000\019\000\ - \019\000\019\000\019\000\019\000\019\000\019\000\019\000\019\000\ - \255\255\255\255\003\000\003\000\003\000\003\000\003\000\003\000\ - \003\000\003\000\003\000\003\000\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\003\000\003\000\003\000\003\000\003\000\ - \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\ - \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\ - \003\000\003\000\003\000\003\000\003\000\255\255\255\255\255\255\ - \255\255\255\255\255\255\003\000\003\000\003\000\003\000\003\000\ - \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\ - \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\ - \003\000\003\000\003\000\003\000\003\000\006\000\006\000\255\255\ - \020\000\006\000\020\000\020\000\020\000\020\000\020\000\020\000\ - \020\000\020\000\020\000\020\000\255\255\255\255\255\255\255\255\ - \000\000\017\000\014\000\021\000\006\000\021\000\025\000\255\255\ - \021\000\021\000\021\000\021\000\021\000\021\000\021\000\021\000\ - \021\000\021\000\255\255\255\255\006\000\006\000\006\000\006\000\ - \006\000\006\000\006\000\006\000\006\000\006\000\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\006\000\006\000\006\000\ - \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\ - \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\ - \006\000\006\000\006\000\006\000\006\000\006\000\006\000\255\255\ - \255\255\255\255\255\255\255\255\255\255\006\000\006\000\006\000\ - \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\ - \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\ - \006\000\006\000\006\000\006\000\006\000\006\000\006\000\007\000\ - \007\000\255\255\255\255\007\000\022\000\022\000\022\000\022\000\ - \022\000\022\000\022\000\022\000\022\000\022\000\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\007\000\023\000\ - \023\000\023\000\023\000\023\000\023\000\023\000\023\000\023\000\ - \023\000\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\007\000\ - \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\255\255\255\255\007\000\255\255\255\255\255\255\007\000\ - \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\010\000\010\000\255\255\255\255\010\000\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \010\000\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\ - \010\000\010\000\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\010\000\010\000\010\000\010\000\010\000\010\000\010\000\ - \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\ - \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\ - \010\000\010\000\010\000\255\255\255\255\255\255\255\255\255\255\ - \255\255\010\000\010\000\010\000\010\000\010\000\010\000\010\000\ - \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\ - \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\ - \010\000\010\000\010\000\013\000\013\000\255\255\255\255\013\000\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\007\000\255\255\ - \255\255\255\255\013\000\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\013\000\013\000\013\000\013\000\013\000\013\000\ - \013\000\013\000\013\000\013\000\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\013\000\013\000\013\000\013\000\013\000\ - \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\ - \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\ - \013\000\013\000\013\000\013\000\013\000\255\255\255\255\255\255\ - \255\255\255\255\255\255\013\000\013\000\013\000\013\000\013\000\ - \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\ - \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\ - \013\000\013\000\013\000\013\000\013\000\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255"; - Lexing.lex_base_code = - "\000\000\000\000\000\000\075\000\000\000\000\000\150\000\208\000\ - \000\000\000\000\027\001\000\000\000\000\102\001\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000"; - Lexing.lex_backtrk_code = - "\000\000\000\000\000\000\000\000\000\000\004\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\004\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000"; - Lexing.lex_default_code = - "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000"; - Lexing.lex_trans_code = - "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\000\000\000\000\000\000\000\000\000\000\000\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\000\000\000\000\000\000\000\000\000\000\000\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\ - \001\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000"; - Lexing.lex_check_code = - "\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\255\255\255\255\255\255\255\255\255\255\ - \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\ - \000\000\000\000\000\000\003\000\003\000\003\000\003\000\003\000\ - \003\000\003\000\003\000\003\000\003\000\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\003\000\003\000\003\000\003\000\ - \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\ - \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\ - \003\000\003\000\003\000\003\000\003\000\003\000\255\255\255\255\ - \255\255\255\255\255\255\255\255\003\000\003\000\003\000\003\000\ - \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\ - \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\ - \003\000\003\000\003\000\003\000\003\000\003\000\006\000\006\000\ - \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\006\000\ - \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\ - \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\ - \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\ - \006\000\255\255\255\255\255\255\255\255\255\255\255\255\006\000\ - \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\ - \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\ - \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\ - \006\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\255\255\255\255\255\255\255\255\255\255\ - \255\255\007\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\ - \007\000\007\000\007\000\010\000\010\000\010\000\010\000\010\000\ - \010\000\010\000\010\000\010\000\010\000\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\010\000\010\000\010\000\010\000\ - \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\ - \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\ - \010\000\010\000\010\000\010\000\010\000\010\000\255\255\255\255\ - \255\255\255\255\255\255\255\255\010\000\010\000\010\000\010\000\ - \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\ - \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\ - \010\000\010\000\010\000\010\000\010\000\010\000\013\000\013\000\ - \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\013\000\ - \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\ - \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\ - \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\ - \013\000\255\255\255\255\255\255\255\255\255\255\255\255\013\000\ - \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\ - \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\ - \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\ - \013\000\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\ - \255\255\255\255\255\255\255\255\255\255\255\255\255\255"; - Lexing.lex_code = - "\255\001\255\255\000\001\255"; -} - -let rec file lexbuf = - lexbuf.Lexing.lex_mem <- Array.create 2 (-1) ; __ocaml_lex_file_rec lexbuf 0 -and __ocaml_lex_file_rec lexbuf __ocaml_lex_state = - match Lexing.new_engine __ocaml_lex_tables __ocaml_lex_state lexbuf with - | 0 -> -# 45 "src/gml.mll" - ( file lexbuf ) -# 425 "src/gml.ml" - - | 1 -> -let -# 46 "src/gml.mll" - key -# 431 "src/gml.ml" -= Lexing.sub_lexeme lexbuf lexbuf.Lexing.lex_start_pos lexbuf.Lexing.lex_mem.(0) in -# 47 "src/gml.mll" - ( let v = value lexbuf in - (key, v) :: file lexbuf ) -# 436 "src/gml.ml" - - | 2 -> -# 50 "src/gml.mll" - ( [] ) -# 441 "src/gml.ml" - - | 3 -> -let -# 51 "src/gml.mll" - c -# 447 "src/gml.ml" -= Lexing.sub_lexeme_char lexbuf lexbuf.Lexing.lex_start_pos in -# 52 "src/gml.mll" - ( failwith ("Gml: invalid character " ^ String.make 1 c) ) -# 451 "src/gml.ml" - - | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_file_rec lexbuf __ocaml_lex_state - -and value_list lexbuf = - lexbuf.Lexing.lex_mem <- Array.create 2 (-1) ; __ocaml_lex_value_list_rec lexbuf 7 -and __ocaml_lex_value_list_rec lexbuf __ocaml_lex_state = - match Lexing.new_engine __ocaml_lex_tables __ocaml_lex_state lexbuf with - | 0 -> -# 56 "src/gml.mll" - ( value_list lexbuf ) -# 462 "src/gml.ml" - - | 1 -> -let -# 57 "src/gml.mll" - key -# 468 "src/gml.ml" -= Lexing.sub_lexeme lexbuf lexbuf.Lexing.lex_start_pos lexbuf.Lexing.lex_mem.(0) in -# 58 "src/gml.mll" - ( let v = value lexbuf in - (key, v) :: value_list lexbuf ) -# 473 "src/gml.ml" - - | 2 -> -# 61 "src/gml.mll" - ( [] ) -# 478 "src/gml.ml" - - | 3 -> -let -# 62 "src/gml.mll" - c -# 484 "src/gml.ml" -= Lexing.sub_lexeme_char lexbuf lexbuf.Lexing.lex_start_pos in -# 63 "src/gml.mll" - ( failwith ("Gml: invalid character " ^ String.make 1 c) ) -# 488 "src/gml.ml" - - | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_value_list_rec lexbuf __ocaml_lex_state - -and value lexbuf = - __ocaml_lex_value_rec lexbuf 14 -and __ocaml_lex_value_rec lexbuf __ocaml_lex_state = - match Lexing.engine __ocaml_lex_tables __ocaml_lex_state lexbuf with - | 0 -> -let -# 66 "src/gml.mll" - i -# 500 "src/gml.ml" -= Lexing.sub_lexeme lexbuf lexbuf.Lexing.lex_start_pos lexbuf.Lexing.lex_curr_pos in -# 67 "src/gml.mll" - ( Int (int_of_string i) ) -# 504 "src/gml.ml" - - | 1 -> -let -# 68 "src/gml.mll" - r -# 510 "src/gml.ml" -= Lexing.sub_lexeme lexbuf lexbuf.Lexing.lex_start_pos lexbuf.Lexing.lex_curr_pos in -# 69 "src/gml.mll" - ( Float (float_of_string r) ) -# 514 "src/gml.ml" - - | 2 -> -let -# 70 "src/gml.mll" - s -# 520 "src/gml.ml" -= Lexing.sub_lexeme lexbuf (lexbuf.Lexing.lex_start_pos + 1) (lexbuf.Lexing.lex_curr_pos + -1) in -# 71 "src/gml.mll" - ( String s ) -# 524 "src/gml.ml" - - | 3 -> -# 73 "src/gml.mll" - ( let l = value_list lexbuf in List l ) -# 529 "src/gml.ml" - - | 4 -> -let -# 74 "src/gml.mll" - c -# 535 "src/gml.ml" -= Lexing.sub_lexeme_char lexbuf lexbuf.Lexing.lex_start_pos in -# 75 "src/gml.mll" - ( failwith ("Gml: invalid character " ^ String.make 1 c) ) -# 539 "src/gml.ml" - - | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_value_rec lexbuf __ocaml_lex_state - -;; - -# 77 "src/gml.mll" - - - let parse f = - let c = open_in f in - let lb = from_channel c in - let v = file lb in - close_in c; - v - - module Parse - (B : Builder.S) - (L : sig val node : value_list -> B.G.V.label - val edge : value_list -> B.G.E.label end) = - struct - - let create_graph l = - let nodes = Hashtbl.create 97 in - let g = B.empty () in - (* 1st pass: create the nodes *) - let g = - List.fold_left - (fun g v -> match v with - | "node", List l -> - let n = B.G.V.create (L.node l) in - begin - try - let id = List.assoc "id" l in Hashtbl.add nodes id n - with Not_found -> - () - end; - B.add_vertex g n - | _ -> - g) - g l - in - (* 2nd pass: add the edges *) - List.fold_left - (fun g v -> match v with - | "edge", List l -> - begin try - let source = List.assoc "source" l in - let target = List.assoc "target" l in - let nsource = Hashtbl.find nodes source in - let ntarget = Hashtbl.find nodes target in - let e = B.G.E.create nsource (L.edge l) ntarget in - B.add_edge_e g e - with Not_found -> - g - end - | _ -> - g) - g l - - let parse f = - match parse f with - | ["graph", List l] -> create_graph l - | _ -> invalid_arg "Gml.Parse.parse: not a graph file" - - end - - module Print - (G : sig - module V : sig - type t - val hash : t -> int - val equal : t -> t -> bool - type label - val label : t -> label - end - module E : sig - type t - type label - val src : t -> V.t - val dst : t -> V.t - val label : t -> label - end - type t - val iter_vertex : (V.t -> unit) -> t -> unit - val iter_edges_e : (E.t -> unit) -> t -> unit - end) - (L : sig - val node : G.V.label -> value_list - val edge : G.E.label -> value_list - end) = - struct - - open Format - - module H = Hashtbl.Make(G.V) - - let print fmt g = - let nodes = H.create 97 in - let cpt = ref 0 in - let id n = - try H.find nodes n - with Not_found -> incr cpt; let id = !cpt in H.add nodes n id; id - in - fprintf fmt "@[graph [@\n"; - let rec value fmt = function - | Int n -> fprintf fmt "%d" n - | Float f -> fprintf fmt "%f" f - | String s -> fprintf fmt "\"%s\"" s - | List l -> fprintf fmt "[@\n @[%a@]@\n]" value_list l - and value_list fmt = function - | [] -> () - | [s,v] -> fprintf fmt "%s %a" s value v - | (s,v) :: l -> fprintf fmt "%s %a@\n" s value v; value_list fmt l - in - G.iter_vertex - (fun v -> - fprintf fmt " @[node [@\n id %d@\n @[%a@]@\n]@]@\n" - (id v) value_list (L.node (G.V.label v))) - g; - G.iter_edges_e - (fun e -> - fprintf fmt - " @[edge [@\n source %d@\n target %d@\n @[%a@]@\n]@]@\n" - (id (G.E.src e)) (id (G.E.dst e)) - value_list (L.edge (G.E.label e))) - g; - fprintf fmt "]@\n" - - end - - -# 671 "src/gml.ml" diff --git a/external/ocamlgraph/src/version.ml b/external/ocamlgraph/src/version.ml deleted file mode 100644 --- a/external/ocamlgraph/src/version.ml +++ /dev/null @@ -1,2 +0,0 @@ -let version = "0.99b" -let date = "Fri Feb 6 22:49:24 UTC 2015" diff --git a/liquid-fixpoint.cabal b/liquid-fixpoint.cabal --- a/liquid-fixpoint.cabal +++ b/liquid-fixpoint.cabal @@ -1,5 +1,5 @@ name: liquid-fixpoint -version: 0.2.2.0 +version: 0.2.3.0 Copyright: 2010-15 Ranjit Jhala, University of California, San Diego. synopsis: Predicate Abstraction-based Horn-Clause/Implication Constraint Solver homepage: https://github.com/ucsd-progsys/liquid-fixpoint @@ -182,3 +182,22 @@ , hashable , unordered-containers , text-format + +test-suite test + default-language: Haskell98 + type: exitcode-stdio-1.0 + hs-source-dirs: tests + ghc-options: -O2 -threaded + main-is: test.hs + build-depends: base, + -- directory, + -- filepath, + -- process, + -- tagged, + liquid-fixpoint, + -- optparse-applicative == 0.11.*, + QuickCheck, + tasty >= 0.10, + tasty-quickcheck, + tasty-rerun >= 1.1, + text diff --git a/src/Language/Fixpoint/Bitvector.hs b/src/Language/Fixpoint/Bitvector.hs --- a/src/Language/Fixpoint/Bitvector.hs +++ b/src/Language/Fixpoint/Bitvector.hs @@ -2,8 +2,11 @@ {-# LANGUAGE DeriveDataTypeable #-} module Language.Fixpoint.Bitvector - ( -- * Sizes - BvSize (..) + ( -- * Constructor + Bv (..) + + -- * Sizes + , BvSize (..) -- * Operators , BvOp (..) @@ -14,6 +17,9 @@ -- * BitVector Expression Constructor , eOp + -- * BitVector Type Constructor + , bvTyCon + ) where import qualified Data.Text as T @@ -34,7 +40,8 @@ -- | Construct the bitvector `Sort` from its `BvSize` mkSort :: BvSize -> Sort -mkSort s = fApp (Left bvTyCon) [sizeSort s] +mkSort _ = fApp (Left $ symbolFTycon $ dummyLoc bitVecName) + [FApp (symbolFTycon $ dummyLoc size32Name) [fObj $ dummyLoc $ symbol "obj"]] -- | Construct an `Expr` using a raw string, e.g. (Bv S32 "#x02000000") instance Expression Bv where @@ -52,7 +59,7 @@ opName BvAnd = dummyLoc bvAndName opName BvOr = dummyLoc bvOrName -sizeSort = (`FApp` []) . sizeTC +sizeSort = (`FApp` [fObj $ dummyLoc $ symbol "obj"]) . sizeTC sizeTC = symbolFTycon . dummyLoc . sizeName sizeName S32 = size32Name sizeName S64 = size64Name diff --git a/src/Language/Fixpoint/Parse.hs b/src/Language/Fixpoint/Parse.hs --- a/src/Language/Fixpoint/Parse.hs +++ b/src/Language/Fixpoint/Parse.hs @@ -71,6 +71,7 @@ import Data.Char (isLower, toUpper) import Language.Fixpoint.Misc hiding (dcolon) import Language.Fixpoint.Types +import Language.Fixpoint.Bitvector import Language.Fixpoint.Errors import Language.Fixpoint.SmtLib2 @@ -159,6 +160,8 @@ locParserP :: Parser a -> Parser (Located a) locParserP p = liftM2 Loc getPosition p +-- FIXME: we (LH) rely on this parser being dumb and *not* consuming trailing +-- whitespace, in order to avoid some parsers spanning multiple lines.. condIdP :: [Char] -> (String -> Bool) -> Parser Symbol condIdP chars f = do c <- letter @@ -218,14 +221,22 @@ exprP :: Parser Expr exprP = buildExpressionParser bops expr1P -funAppP = (try exprFunSpacesP) <|> (try exprFunSemisP) <|> exprFunCommasP +funAppP = (try litP) <|> (try exprFunSpacesP) <|> (try exprFunSemisP) <|> exprFunCommasP where - exprFunSpacesP = liftM2 EApp funSymbolP (sepBy1 expr0P spaces) + exprFunSpacesP = liftM2 EApp funSymbolP (sepBy1 expr0P blanks) exprFunCommasP = liftM2 EApp funSymbolP (parens $ sepBy exprP comma) exprFunSemisP = liftM2 EApp funSymbolP (parenBrackets $ sepBy exprP semi) funSymbolP = locParserP symbolP +-- | BitVector literal: lit "#x00000001" (BitVec (Size32 obj)) +litP = do reserved "lit" + l <- stringLiteral + s <- try (bvSortP "Size32" S32) <|> bvSortP "Size64" S64 + return $ ECon $ L (T.pack l) (mkSort s) + where + bvSortP ss s = do parens (reserved "BitVec" >> parens (reserved ss >> reserved "obj")) + return s -- ORIG exprP :: Parser Expr @@ -254,14 +265,14 @@ -- ORIG expr2P = buildExpressionParser bops lexprP -bops = [ [ Prefix (reservedOp "-" >> return eMinus)] +bops = [ [ Prefix (reservedOp "-" >> return ENeg)] , [ Infix (reservedOp "*" >> return (EBin Times)) AssocLeft , Infix (reservedOp "/" >> return (EBin Div )) AssocLeft ] , [ Infix (reservedOp "-" >> return (EBin Minus)) AssocLeft , Infix (reservedOp "+" >> return (EBin Plus )) AssocLeft ] - , [Infix (reservedOp "mod" >> return (EBin Mod )) AssocLeft] + , [ Infix (reservedOp "mod" >> return (EBin Mod )) AssocLeft] ] eMinus = EBin Minus (expr (0 :: Integer)) diff --git a/src/Language/Fixpoint/PrettyPrint.hs b/src/Language/Fixpoint/PrettyPrint.hs --- a/src/Language/Fixpoint/PrettyPrint.hs +++ b/src/Language/Fixpoint/PrettyPrint.hs @@ -1,4 +1,4 @@ -{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} @@ -13,10 +13,15 @@ class PPrint a where pprint :: a -> Doc + pprint = pprintPrec 0 -showpp :: (PPrint a) => a -> String -showpp = render . pprint + -- | Pretty-print something with a specific precedence. + pprintPrec :: Int -> a -> Doc + pprintPrec _ = pprint +showpp :: (PPrint a) => a -> String +showpp = render . pprint + instance PPrint a => PPrint (Maybe a) where pprint = maybe (text "Nothing") ((text "Just" <+>) . pprint) @@ -24,20 +29,20 @@ pprint = brackets . intersperse comma . map pprint instance (PPrint a, PPrint b, PPrint c) => PPrint (a, b, c) where - pprint (x, y, z) = parens $ (pprint x) <> text "," <> (pprint y) <> text "," <> (pprint z) + pprint (x, y, z) = parens $ (pprint x) <> text "," <> (pprint y) <> text "," <> (pprint z) instance (PPrint a, PPrint b) => PPrint (a,b) where pprint (x, y) = (pprint x) <+> text ":" <+> (pprint y) instance PPrint SourcePos where - pprint = text . show + pprint = text . show instance PPrint () where - pprint = text . show + pprint = text . show -instance PPrint String where - pprint = text +instance PPrint String where + pprint = text instance PPrint Int where pprint = toFix @@ -54,71 +59,127 @@ pprint r = toFix r instance PPrint Bop where - pprint = toFix + pprint = toFix instance PPrint Sort where - pprint = toFix + pprint = toFix instance PPrint Symbol where - pprint = toFix + pprint = text . symbolString instance PPrint SymConst where pprint (SL x) = doubleQuotes $ text $ T.unpack x + +-- | Wrap the enclosed 'Doc' in parentheses only if the condition holds. +parensIf True = parens +parensIf False = id + +-- NOTE: The following Expr and Pred printers use pprintPrec to print +-- expressions with minimal parenthesization. The precedence rules are somewhat +-- fragile, and it would be nice to have them directly tied to the parser, but +-- the general idea is (from lowest to highest precedence): +-- +-- 1 - if-then-else +-- 2 - => and <=> +-- 3 - && and || +-- 4 - ==, !=, <, <=, >, >= +-- 5 - mod +-- 6 - + and - +-- 7 - * and / +-- 8 - function application +-- +-- Each printer `p` checks whether the precedence of the context is greater than +-- its own precedence. If so, the printer wraps itself in parentheses. Then it +-- sets the contextual precedence for recursive printer invocations to +-- (prec p + 1). + +opPrec Mod = 5 +opPrec Plus = 6 +opPrec Minus = 6 +opPrec Times = 7 +opPrec Div = 7 + instance PPrint Expr where - pprint (EApp f es) = parens $ intersperse empty $ (pprint f) : (pprint <$> es) - pprint (ESym c) = pprint c - pprint (ECon c) = pprint c - pprint (EVar s) = pprint s - pprint (ELit s _) = pprint s - pprint (EBin o e1 e2) = parens $ pprint e1 <+> pprint o <+> pprint e2 - pprint (EIte p e1 e2) = parens $ text "if" <+> pprint p <+> text "then" <+> pprint e1 <+> text "else" <+> pprint e2 - pprint (ECst e so) = parens $ pprint e <+> text " : " <+> pprint so - pprint (EBot) = text "_|_" + pprintPrec _ (ESym c) = pprint c + pprintPrec _ (ECon c) = pprint c + pprintPrec _ (EVar s) = pprint s + pprintPrec _ (ELit s _) = pprint s + pprintPrec _ (EBot) = text "_|_" + pprintPrec z (ENeg e) = parensIf (z > zn) $ + text "-" <> pprintPrec (zn+1) e + where zn = 2 + pprintPrec z (EApp f es) = parensIf (z > za) $ + intersperse empty $ + (pprint f) : (pprintPrec (za+1) <$> es) + where za = 8 + pprintPrec z (EBin o e1 e2) = parensIf (z > zo) $ + pprintPrec (zo+1) e1 <+> + pprint o <+> + pprintPrec (zo+1) e2 + where zo = opPrec o + pprintPrec z (EIte p e1 e2) = parensIf (z > zi) $ + text "if" <+> pprintPrec (zi+1) p <+> + text "then" <+> pprintPrec (zi+1) e1 <+> + text "else" <+> pprintPrec (zi+1) e2 + where zi = 1 + pprintPrec _ (ECst e so) = parens $ pprint e <+> text ":" <+> pprint so instance PPrint Pred where - pprint PTop = text "???" - pprint PTrue = trueD - pprint PFalse = falseD - pprint (PBexp e) = parens $ pprint e - pprint (PNot p) = parens $ text "not" <+> parens (pprint p) - pprint (PImp p1 p2) = parens $ (pprint p1) <+> text "=>" <+> (pprint p2) - pprint (PIff p1 p2) = parens $ (pprint p1) <+> text "<=>" <+> (pprint p2) - pprint (PAnd ps) = parens $ pprintBin trueD andD ps - pprint (POr ps) = parens $ pprintBin falseD orD ps - pprint (PAtom r e1 e2) = parens $ pprint e1 <+> pprint r <+> pprint e2 - pprint (PAll xts p) = text "forall" <+> toFix xts <+> text "." <+> pprint p + pprintPrec _ PTop = text "???" + pprintPrec _ PTrue = trueD + pprintPrec _ PFalse = falseD + pprintPrec z (PBexp e) = pprintPrec z e + pprintPrec z (PNot p) = parensIf (z > zn) $ + text "not" <+> pprintPrec (zn+1) p + where zn = 8 + pprintPrec z (PImp p1 p2) = parensIf (z > zi) $ + (pprintPrec (zi+1) p1) <+> + text "=>" <+> + (pprintPrec (zi+1) p2) + where zi = 2 + pprintPrec z (PIff p1 p2) = parensIf (z > zi) $ + (pprintPrec (zi+1) p1) <+> + text "<=>" <+> + (pprintPrec (zi+1) p2) + where zi = 2 + pprintPrec z (PAnd ps) = parensIf (z > za) $ + pprintBin (za+1) trueD andD ps + where za = 3 + pprintPrec z (POr ps) = parensIf (z > zo) $ + pprintBin (zo+1) falseD orD ps + where zo = 3 + pprintPrec z (PAtom r e1 e2) = parensIf (z > za) $ + pprintPrec (za+1) e1 <+> + pprint r <+> + pprintPrec (za+1) e2 + where za = 4 + pprintPrec _ (PAll xts p) = text "forall" <+> toFix xts <+> text "." <+> pprint p trueD = text "true" falseD = text "false" andD = text " &&" orD = text " ||" -pprintBin b _ [] = b -pprintBin _ o xs = intersperse o $ pprint <$> xs +pprintBin _ b _ [] = b +pprintBin z _ o xs = intersperse o $ pprintPrec z <$> xs instance PPrint Refa where - pprint (RConc p) = pprint p - pprint k = toFix k - -instance PPrint Reft where - pprint r@(Reft (_,ras)) - | isTauto r = text "true" - | otherwise = {- intersperse comma -} pprintBin trueD andD $ flattenRefas ras + pprintPrec z (RConc p) = pprintPrec z p + pprintPrec _ k = toFix k - +instance PPrint Reft where + pprint r@(Reft (_,ras)) + | isTauto r = text "true" + | otherwise = {- intersperse comma -} pprintBin z trueD andD flat + where + flat = flattenRefas ras + z = if length flat > 1 then 3 else 0 instance PPrint SortedReft where - pprint (RR so (Reft (v, ras))) - = braces + pprint (RR so (Reft (v, ras))) + = braces $ (pprint v) <+> (text ":") <+> (toFix so) <+> (text "|") <+> pprint ras instance PPrint a => PPrint (Located a) where pprint (Loc _ x) = pprint x - - - - - - - diff --git a/src/Language/Fixpoint/SmtLib2.hs b/src/Language/Fixpoint/SmtLib2.hs --- a/src/Language/Fixpoint/SmtLib2.hs +++ b/src/Language/Fixpoint/SmtLib2.hs @@ -424,6 +424,7 @@ smt2 (EApp f [e]) | val f == "Set_sng" = format "({} {} {})" (add, emp, smt2 e) smt2 (EApp f es) = format "({} {})" (smt2 f, smt2s es) + smt2 (ENeg e) = format "(- {})" (Only $ smt2 e) smt2 (EBin o e1 e2) = format "({} {} {})" (smt2 o, smt2 e1, smt2 e2) smt2 (EIte e1 e2 e3) = format "(ite {} {} {})" (smt2 e1, smt2 e2, smt2 e3) smt2 _ = error "TODO: SMTLIB2 Expr" diff --git a/src/Language/Fixpoint/Sort.hs b/src/Language/Fixpoint/Sort.hs --- a/src/Language/Fixpoint/Sort.hs +++ b/src/Language/Fixpoint/Sort.hs @@ -127,6 +127,7 @@ checkExpr _ (ECon (I _)) = return FInt checkExpr _ (ECon (R _)) = return FReal checkExpr f (EVar x) = checkSym f x +checkExpr f (ENeg e) = checkNeg f e checkExpr f (EBin o e1 e2) = checkOp f e1 o e2 checkExpr f (EIte p e1 e2) = checkIte f p e1 e2 checkExpr f (ECst e t) = checkCst f t e @@ -177,6 +178,15 @@ -- | Helper for checking binary (numeric) operations + +checkNeg f e = do + t <- checkExpr f e + case t of + FReal -> return FReal + FInt -> return FInt + (FObj l) -> checkNumeric f l >> return t + _ -> throwError $ printf "Operand has non-numeric type %s in %s" + (showFix t) (showFix e) checkOp f e1 o e2 = do t1 <- checkExpr f e1 diff --git a/src/Language/Fixpoint/Types.hs b/src/Language/Fixpoint/Types.hs --- a/src/Language/Fixpoint/Types.hs +++ b/src/Language/Fixpoint/Types.hs @@ -109,6 +109,7 @@ , notExprReft -- singleton: v /= e , uexprReft -- singleton: v ~~ e , symbolReft -- singleton: v == x + , usymbolReft -- singleton: v ~~ x , propReft -- singleton: Prop(v) <=> p , predReft -- any pred : p , isFunctionSortedReft @@ -130,6 +131,7 @@ , substfExcept , subst1Except , sortSubst + , targetSubstSyms -- * Visitors , reftKVars @@ -231,6 +233,7 @@ -- go (EDat x _) = [x] go (ELit x _) = [val x] go (EApp f es) = val f : concatMap go es + go (ENeg e) = go e go (EBin _ e1 e2) = go e1 ++ go e2 go (EIte p e1 e2) = predSymbols p ++ go e1 ++ go e2 go (ECst e _) = go e @@ -398,7 +401,9 @@ [] -> empty xys -> hcat $ map (\(x,y) -> brackets $ (toFix x) <> text ":=" <> (toFix y)) xys +targetSubstSyms (Su ms) = syms $ snd <$> ms + --------------------------------------------------------------- ------------------------- Expressions ------------------------- --------------------------------------------------------------- @@ -425,6 +430,7 @@ | EVar !Symbol | ELit !LocSymbol !Sort | EApp !LocSymbol ![Expr] + | ENeg !Expr | EBin !Bop !Expr !Expr | EIte !Pred !Expr !Expr | ECst !Expr !Sort @@ -440,7 +446,7 @@ instance Fixpoint Constant where toFix (I i) = toFix i toFix (R i) = toFix i - toFix (L s t) = parens $ text "lit" <+> toFix s <+> toFix t + toFix (L s t) = parens $ text "lit" <+> text "\"" <> toFix s <> text "\"" <+> toFix t instance Fixpoint SymConst where toFix = toFix . encodeSymConst @@ -475,6 +481,7 @@ toFix (EVar s) = toFix s toFix (ELit s _) = toFix s toFix (EApp f es) = (toFix f) <> (parens $ toFix es) + toFix (ENeg e) = parens $ text "-" <+> parens (toFix e) toFix (EBin o e1 e2) = parens $ toFix e1 <+> toFix o <+> toFix e2 toFix (EIte p e1 e2) = parens $ toFix p <+> text "?" <+> toFix e1 <+> text ":" <+> toFix e2 toFix (ECst e so) = parens $ toFix e <+> text " : " <+> toFix so @@ -944,6 +951,7 @@ syms = exprSymbols substa f = substf (EVar . f) substf f (EApp s es) = EApp (substf f s) $ map (substf f) es + substf f (ENeg e) = ENeg (substf f e) substf f (EBin op e1 e2) = EBin op (substf f e1) (substf f e2) substf f (EIte p e1 e2) = EIte (substf f p) (substf f e1) (substf f e2) substf f (ECst e so) = ECst (substf f e) so @@ -951,8 +959,9 @@ substf _ e = e subst su (EApp f es) = EApp (subst su f) $ map (subst su) es + subst su (ENeg e) = ENeg (subst su e) subst su (EBin op e1 e2) = EBin op (subst su e1) (subst su e2) - subst su (EIte p e1 e2) = EIte (subst su p) (subst su e1) (subst su e2) + subst su (EIte p e1 e2) = EIte (subst su p) (subst su e1) (subst su e2) subst su (ECst e so) = ECst (subst su e) so subst su (EVar x) = appSubst su x subst _ e = e @@ -1081,6 +1090,9 @@ symbolReft :: (Symbolic a) => a -> Reft symbolReft = exprReft . eVar +usymbolReft :: (Symbolic a) => a -> Reft +usymbolReft = uexprReft . eVar + vv_ = vv Nothing trueSortedReft :: Sort -> SortedReft @@ -1153,6 +1165,7 @@ -- rnf (EDat x1 x2) = rnf x1 `seq` rnf x2 rnf (ELit x1 x2) = rnf x1 `seq` rnf x2 rnf (EApp x1 x2) = rnf x1 `seq` rnf x2 + rnf (ENeg x1) = rnf x1 rnf (EBin x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 rnf (EIte x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 rnf (ECst x1 x2) = rnf x1 `seq` rnf x2 @@ -1275,7 +1288,7 @@ instance NFData Qualifier where rnf (Q x1 x2 x3 _) = rnf x1 `seq` rnf x2 `seq` rnf x3 -pprQual (Q n xts p _) = text "qualif" <+> text (symbolString n) <> parens args <> colon <+> toFix p +pprQual (Q n xts p l) = text "qualif" <+> text (symbolString n) <> parens args <> colon <+> toFix p <+> text "//" <+> toFix l where args = intersperse comma (toFix <$> xts) data FInfo a = FI { cm :: M.HashMap Integer (SubC a) @@ -1467,6 +1480,7 @@ instance SymConsts Expr where symConsts (ESym c) = [c] symConsts (EApp _ es) = concatMap symConsts es + symConsts (ENeg e) = symConsts e symConsts (EBin _ e e') = concatMap symConsts [e, e'] symConsts (EIte p e e') = symConsts p ++ concatMap symConsts [e, e'] symConsts (ECst e _) = symConsts e diff --git a/src/Language/Fixpoint/Visitor.hs b/src/Language/Fixpoint/Visitor.hs --- a/src/Language/Fixpoint/Visitor.hs +++ b/src/Language/Fixpoint/Visitor.hs @@ -102,6 +102,7 @@ step c e@(ELit _ _) = return e step c e@(EVar _) = return e step c (EApp f es) = EApp f <$> (vE c <$$> es) + step c (ENeg e) = ENeg <$> vE c e step c (EBin o e1 e2) = EBin o <$> vE c e1 <*> vE c e2 step c (EIte p e1 e2) = EIte <$> vP c p <*> vE c e1 <*> vE c e2 step c (ECst e t) = (`ECst` t) <$> vE c e diff --git a/tests/test.hs b/tests/test.hs new file mode 100644 --- /dev/null +++ b/tests/test.hs @@ -0,0 +1,145 @@ +{-# LANGUAGE OverloadedStrings #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} +module Main where + +import Language.Fixpoint.Names +import Language.Fixpoint.Parse +import Language.Fixpoint.PrettyPrint +import Language.Fixpoint.Types + +import Control.Monad +import Data.Proxy +import Data.Text (Text, cons, inits, pack) +import Test.QuickCheck +import Test.Tasty +import Test.Tasty.Ingredients.Rerun +import Test.Tasty.Options +import Test.Tasty.QuickCheck +import Test.Tasty.Runners + +main :: IO () +main = run tests + where + run = defaultMainWithIngredients [ + rerunningTests [ listingTests, consoleTestReporter ] + , includingOptions [ Option (Proxy :: Proxy QuickCheckTests) + ] + ] + + tests = testGroup "Tests" [ quickCheckTests ] + +quickCheckTests :: TestTree +quickCheckTests + = testGroup "Properties" + [ testProperty "prop_pprint_parse_inv_expr" prop_pprint_parse_inv_expr + , testProperty "prop_pprint_parse_inv_pred" prop_pprint_parse_inv_pred + ] + +prop_pprint_parse_inv_pred :: Pred -> Bool +prop_pprint_parse_inv_pred p = p == rr (showpp p) + +prop_pprint_parse_inv_expr :: Expr -> Bool +prop_pprint_parse_inv_expr p = simplify p == rr (showpp $ simplify p) + +instance Arbitrary Sort where + arbitrary = sized arbSort + +arbSort 0 = oneof [return FInt, return FReal, return FNum] +arbSort n = frequency + [(1, return FInt) + ,(1, return FReal) + ,(1, return FNum) + ,(2, fmap FObj arbitrary) + ] + + +instance Arbitrary Pred where + arbitrary = sized arbPred + shrink = filter valid . genericShrink + where + valid (PAnd []) = False + valid (PAnd [_]) = False + valid (POr []) = False + valid (POr [_]) = False + valid (PBexp (EBin _ _ _)) = True + valid (PBexp _) = False + valid _ = True + +arbPred 0 = elements [PTrue, PFalse] +arbPred n = frequency + [(1, return PTrue) + ,(1, return PFalse) + ,(2, fmap PAnd twoPreds) + ,(2, fmap POr twoPreds) + ,(2, fmap PNot (arbPred (n `div` 2))) + ,(2, liftM2 PImp (arbPred (n `div` 2)) (arbPred (n `div` 2))) + ,(2, liftM2 PIff (arbPred (n `div` 2)) (arbPred (n `div` 2))) + ,(2, fmap PBexp (arbExpr (n `div` 2))) + ,(2, liftM3 PAtom arbitrary (arbExpr (n `div` 2)) (arbExpr (n `div` 2))) + -- ,liftM2 PAll arbitrary arbitrary + -- ,return PTop + ] + where + twoPreds = do + x <- arbPred (n `div` 2) + y <- arbPred (n `div` 2) + return [x,y] + +instance Arbitrary Expr where + arbitrary = sized arbExpr + shrink = filter valid . genericShrink + where valid (EApp _ []) = False + valid _ = True + +arbExpr 0 = oneof [fmap ESym arbitrary, fmap ECon arbitrary, fmap EVar arbitrary, return EBot] +arbExpr n = frequency + [(1, fmap ESym arbitrary) + ,(1, fmap ECon arbitrary) + ,(1, fmap EVar arbitrary) + ,(1, return EBot) + -- ,liftM2 ELit arbitrary arbitrary -- restrict literals somehow + ,(2, choose (1,3) >>= \m -> liftM2 EApp arbitrary (vectorOf m (arbExpr (n `div` 2)))) + ,(2, liftM3 EBin arbitrary (arbExpr (n `div` 2)) (arbExpr (n `div` 2))) + ,(2, liftM3 EIte (arbPred (max 2 (n `div` 2)) `suchThat` isRel) + (arbExpr (n `div` 2)) + (arbExpr (n `div` 2))) + ,(2, liftM2 ECst (arbExpr (n `div` 2)) (arbSort (n `div` 2))) + ] + where + isRel (PAtom _ _ _) = True + isRel _ = False + +instance Arbitrary Brel where + arbitrary = oneof (map return [Eq, Ne, Gt, Ge, Lt, Le, Ueq, Une]) + +instance Arbitrary Bop where + arbitrary = oneof (map return [Plus, Minus, Times, Div, Mod]) + +instance Arbitrary SymConst where + arbitrary = fmap SL arbitrary + +instance Arbitrary Symbol where + arbitrary = fmap (symbol :: Text -> Symbol) arbitrary + +instance Arbitrary Text where + arbitrary = choose (1,4) >>= \n -> + fmap pack (vectorOf n char `suchThat` valid) + where + char = elements ['a'..'z'] + valid x = x `notElem` fixpointNames && not (isFixKey x) + +instance Arbitrary FTycon where + arbitrary = do + c <- elements ['A'..'Z'] + t <- arbitrary + return $ symbolFTycon $ dummyLoc $ symbol $ cons c t + +instance Arbitrary Constant where + arbitrary = oneof [fmap I (arbitrary `suchThat` (>=0)) + -- ,fmap R arbitrary + ] + shrink = genericShrink + +instance Arbitrary a => Arbitrary (Located a) where + arbitrary = fmap dummyLoc arbitrary + shrink = fmap dummyLoc . shrink . val