liquid-fixpoint 0.2.2.0 → 0.2.3.0
raw patch · 21 files changed
+339/−1709 lines, 21 filesdep +QuickCheckdep +tastydep +tasty-quickcheckdep ~basePVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependencies added: QuickCheck, tasty, tasty-quickcheck, tasty-rerun
Dependency ranges changed: base
API changes (from Hackage documentation)
+ Language.Fixpoint.Bitvector: Bv :: BvSize -> String -> Bv
+ Language.Fixpoint.Bitvector: bvTyCon :: FTycon
+ Language.Fixpoint.Bitvector: data Bv
+ Language.Fixpoint.PrettyPrint: opPrec :: Num a => Bop -> a
+ Language.Fixpoint.PrettyPrint: parensIf :: Bool -> Doc -> Doc
+ Language.Fixpoint.PrettyPrint: pprintPrec :: PPrint a => Int -> a -> Doc
+ Language.Fixpoint.Types: ENeg :: !Expr -> Expr
+ Language.Fixpoint.Types: instance Constructor C1_9Expr
+ Language.Fixpoint.Types: targetSubstSyms :: Subst -> [Symbol]
+ Language.Fixpoint.Types: usymbolReft :: Symbolic a => a -> Reft
- Language.Fixpoint.PrettyPrint: class PPrint a
+ Language.Fixpoint.PrettyPrint: class PPrint a where pprint = pprintPrec 0 pprintPrec _ = pprint
- Language.Fixpoint.PrettyPrint: pprintBin :: PPrint a => Doc -> Doc -> [a] -> Doc
+ Language.Fixpoint.PrettyPrint: pprintBin :: PPrint a => Int -> Doc -> Doc -> [a] -> Doc
Files
- external/fixpoint/fixLex.mll +5/−6
- external/fixpoint/fixParse.mly +3/−5
- external/fixpoint/fixpoint.native-i386-linux binary
- external/fixpoint/fixpoint.native-i686-w64-mingw32 too large to diff
- external/fixpoint/fixpoint.native-x86_64-darwin too large to diff
- external/fixpoint/fixpoint.native-x86_64-linux too large to diff
- external/fixpoint/foo.ml +0/−6
- external/ocamlgraph/src/dot_lexer.ml +0/−386
- external/ocamlgraph/src/dot_parser.ml +0/−551
- external/ocamlgraph/src/dot_parser.mli +0/−21
- external/ocamlgraph/src/gml.ml +0/−670
- external/ocamlgraph/src/version.ml +0/−2
- liquid-fixpoint.cabal +20/−1
- src/Language/Fixpoint/Bitvector.hs +11/−4
- src/Language/Fixpoint/Parse.hs +15/−4
- src/Language/Fixpoint/PrettyPrint.hs +111/−50
- src/Language/Fixpoint/SmtLib2.hs +1/−0
- src/Language/Fixpoint/Sort.hs +10/−0
- src/Language/Fixpoint/Types.hs +17/−3
- src/Language/Fixpoint/Visitor.hs +1/−0
- tests/test.hs +145/−0
external/fixpoint/fixLex.mll view
@@ -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 }
external/fixpoint/fixParse.mly view
@@ -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)]) }
external/fixpoint/fixpoint.native-i386-linux view
binary file changed (1689979 → 1688841 bytes)
external/fixpoint/fixpoint.native-i686-w64-mingw32 view
file too large to diff
external/fixpoint/fixpoint.native-x86_64-darwin view
file too large to diff
external/fixpoint/fixpoint.native-x86_64-linux view
file too large to diff
− external/fixpoint/foo.ml
@@ -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 ()
− external/ocamlgraph/src/dot_lexer.ml
@@ -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--;;-
− external/ocamlgraph/src/dot_parser.ml
@@ -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)
− external/ocamlgraph/src/dot_parser.mli
@@ -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
− external/ocamlgraph/src/gml.ml
@@ -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"
− external/ocamlgraph/src/version.ml
@@ -1,2 +0,0 @@-let version = "0.99b"-let date = "Fri Feb 6 22:49:24 UTC 2015"
liquid-fixpoint.cabal view
@@ -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
src/Language/Fixpoint/Bitvector.hs view
@@ -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
src/Language/Fixpoint/Parse.hs view
@@ -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))
src/Language/Fixpoint/PrettyPrint.hs view
@@ -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-------
src/Language/Fixpoint/SmtLib2.hs view
@@ -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"
src/Language/Fixpoint/Sort.hs view
@@ -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
src/Language/Fixpoint/Types.hs view
@@ -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
src/Language/Fixpoint/Visitor.hs view
@@ -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
+ tests/test.hs view
@@ -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