diff --git a/Fixpoint.hs b/Fixpoint.hs --- a/Fixpoint.hs +++ b/Fixpoint.hs @@ -4,8 +4,9 @@ import System.Console.CmdArgs.Verbosity (whenLoud) main :: IO ExitCode -main = do cfg <- getOpts - whenLoud $ putStrLn $ "Options: " ++ show cfg - e <- solveFQ cfg - putStrLn $ "EXIT: " ++ show e - exitWith e +main = do + cfg <- getOpts + whenLoud $ putStrLn $ "Options: " ++ show cfg + e <- solveFQ cfg + putStrLn $ "EXIT: " ++ show e + exitWith e diff --git a/external/fixpoint/ast.ml b/external/fixpoint/ast.ml --- a/external/fixpoint/ast.ml +++ b/external/fixpoint/ast.ml @@ -255,9 +255,9 @@ | (Var i), ct (* when ct != Bool *) -> begin match lookup_var s i with - | Some ct' when ct = ct' -> Some s - | Some _ -> None - | None -> Some {s with vars = (i,ct) :: s.vars} + | Some ct' when ct = ct' -> (*let _ = F.printf "\nUnify YES! %s \t - \t %s" (to_string ct) (to_string (Var i)) in *) Some s + | Some ct'' -> (*let _ = F.printf "\nUnify No! %s \t /= %s \t - \t %s" (to_string ct) (to_string ct'') (to_string (Var i)) in *) None + | None -> (*let _ = F.printf "\nUnify Add! %s \t - \t %s" (to_string ct) (to_string (Var i)) in *) Some {s with vars = (i,ct) :: s.vars} end | Ptr LFun, Ptr _ @@ -335,7 +335,26 @@ let n_vars = s.vars |>: fst |> Misc.sort_and_compact |> List.length in n == n_vars + let index = ref 0 + let makeFresh n = + let rec go i = + if i < n then (let x = !index in incr index; (i,x)::go (i+1)) else [] in + go 0 + + let rec refresh su = function + | Int -> Int + | Real -> Real + | Bool -> Bool + | Obj -> Obj + | Var i -> (try (Var (snd (List.find (fun (j, _) -> j == i) su))) + with Not_found -> Var i) + | Ptr l -> Ptr l + | Func(n, ts) -> let su' = List.filter (fun (i,_) -> i>= n) su in Func(n, List.map (refresh su') ts) + | Num -> Num + | Frac -> Frac + | App(tc, ts) -> App(tc, List.map (refresh su) ts) + end module Symbol = @@ -1200,7 +1219,7 @@ | None -> None end -let rec sortcheck_expr g f e = +let rec sortcheck_expr g f expected_t e = match euw e with | Bot -> None @@ -1216,7 +1235,7 @@ sortcheck_op g f (e1, op, e2) | Ite (p, e1, e2) -> if sortcheck_pred g f p then - match Misc.map_pair (sortcheck_expr g f) (e1, e2) with + match Misc.map_pair (sortcheck_expr g f None) (e1, e2) with | (Some t1, Some t2) -> begin match Sort.unify [t1] [t2] with @@ -1229,13 +1248,13 @@ begin match euw e1 with | App (uf, es) -> sortcheck_app g f (Some t) uf es | _ -> - match sortcheck_expr g f e1 with + match sortcheck_expr g f None e1 with | Some t1 when Sort.compat t t1 -> Some t | _ -> None end | App (uf, es) -> - sortcheck_app g f None uf es + sortcheck_app g f expected_t uf es | _ -> assertf "Ast.sortcheck_expr: unhandled expr = %s" (Expression.to_string e) @@ -1245,12 +1264,19 @@ sortcheck_sym f uf |> function None -> (* yikes uf; *) None | Some t -> Sort.func_of_t t - |> function None -> None | Some (tyArity, i_ts, o_t) -> + |> function None -> None | Some (tyArity, i_ts', o_t') -> + let freshMap = Sort.makeFresh tyArity in + let i_ts = List.map (Sort.refresh freshMap) i_ts' in + let o_t = Sort.refresh freshMap o_t' in let _ = asserts (List.length es = List.length i_ts) "ERROR: uf arg-arity error: uf=%s" uf in - let e_ts = es |> List.map (sortcheck_expr g f) |> Misc.map_partial id in + let e_ts = (List.map (fun x -> Some x) i_ts, es) |> Misc.zipWith (sortcheck_expr g f) |> Misc.map_partial id in if List.length e_ts <> List.length i_ts then - None + (* let _ = F.printf "OUT2 \n es = %s \n e_ts = %s \n i_ts = %s" + (String.concat "\t" (List.map Expression.to_string es)) + (String.concat "\t" (List.map Sort.to_string e_ts)) + (String.concat "\t" (List.map Sort.to_string i_ts)) + in*) None else match Sort.unify e_ts i_ts with | None -> None @@ -1260,7 +1286,8 @@ | None -> Some (s, t) | Some t' -> match Sort.unifyWith s [t] [t'] with - | None -> None + | None -> (*let _ = F.printf "\nOUT5 Cannot unify: %s \t\t with \t\t %s" (Sort.to_string t) (Sort.to_string t') in *) + None | Some s' -> Some (s', Sort.apply s' t) and sortcheck_app g f tExp uf es = @@ -1286,7 +1313,7 @@ | (Some t1, _) -> F.printf "sortcheck_op2 : \n%s \n" (Sort.to_string t1) | (_, _) -> F.printf "sortcheck_op3 : \n" in *) - match Misc.map_pair (sortcheck_expr g f) (e1, e2) with + match Misc.map_pair (sortcheck_expr g f None) (e1, e2) with | (Some Sort.Int, Some Sort.Int) -> Some Sort.Int @@ -1319,7 +1346,7 @@ and sortcheck_rel g f (e1, r, e2) = - let t1o, t2o = (e1,e2) |> Misc.map_pair (sortcheck_expr g f) in + let t1o, t2o = (e1,e2) |> Misc.map_pair (sortcheck_expr g f None) in match r, t1o, t2o with | Ueq, Some (_), Some (_) | Une, Some (_), Some (_) @@ -1355,7 +1382,7 @@ | False -> true | Bexp e -> - sortcheck_expr g f e = Some Sort.Bool + sortcheck_expr g f (Some Sort.Bool) e = Some Sort.Bool | Not p -> sortcheck_pred g f p | Imp (p1, p2) | Iff (p1, p2) -> @@ -1365,20 +1392,20 @@ List.for_all (sortcheck_pred g f) ps | Atom (e1, Ueq, e2) when !Constants.ueq_all_sorts - -> (not (None = sortcheck_expr g f e1)) && - (not (None = sortcheck_expr g f e2)) + -> (not (None = sortcheck_expr g f None e1)) && + (not (None = sortcheck_expr g f None e2)) | Atom ((Con (Constant.Int(0)),_), _, e) | Atom (e, _, (Con (Constant.Int(0)),_)) when not (!Constants.strictsortcheck) - -> not (None = sortcheck_expr g f e) + -> not (None = sortcheck_expr g f None e) | Atom (((Con _, _) as e), Eq, (App (uf, es), _)) | Atom ((App (uf, es), _), Eq, ((Con _, _) as e)) | Atom (((Var _, _) as e), Eq, (App (uf, es), _)) | Atom ((App (uf, es), _), Eq, ((Var _, _) as e)) (* -> begin match sortcheck_sym f x with *) - -> begin match sortcheck_expr g f e with + -> begin match sortcheck_expr g f None e with | None -> false | Some t -> not (None = sortcheck_app g f (Some t) uf es) end @@ -1387,10 +1414,12 @@ -> let t1o = solved_app f uf1 <| sortcheck_app_sub g f None uf1 e1s in let t2o = solved_app f uf2 <| sortcheck_app_sub g f None uf2 e2s in begin match t1o, t2o with - | (Some t1, Some t2) -> unifiable t1 t2 - | (None, None) -> false - | (None, Some t2) -> not (None = sortcheck_app g f (Some t2) uf1 e1s) - | (Some t1, None) -> not (None = sortcheck_app g f (Some t1) uf2 e2s) + | (Some t1, Some t2) -> (* let _ = F.printf "sortcheck Eq App1 %s" (Predicate.to_string p) in *) unifiable t1 t2 + | (None, None) -> (* let _ = F.printf "sortcheck Eq App2 %s" (Predicate.to_string p) in *) false + | (None, Some t2) -> (* let _ = F.printf "sortcheck Eq App3 %s" (Predicate.to_string p) in *) not (None = sortcheck_app g f (Some t2) uf1 e1s) + | (Some t1, None) -> (* let _ = F.printf "sortcheck Eq App4 %s :: %s" + (Predicate.to_string p) (Sort.to_string t1) in *) + not (None = sortcheck_app g f (Some t1) uf2 e2s) end | Atom (e1, r, e2) -> @@ -1414,7 +1443,9 @@ (* API *) let sortcheck_app g f tExp uf es = sortcheck_app_sub g f tExp uf es - |> checkArity f uf + |> checkArity f uf + +let sortcheck_expr g f e = sortcheck_expr g f None e (* match uf_arity f uf, sortcheck_app_sub g f tExp uf es with diff --git a/external/fixpoint/ast.mli b/external/fixpoint/ast.mli --- a/external/fixpoint/ast.mli +++ b/external/fixpoint/ast.mli @@ -81,6 +81,8 @@ val generalize : t list -> t list val sub_args : sub -> (int * t) list (* val check_arity : int -> sub -> bool *) + val makeFresh : int -> (int * int) list + val refresh : (int * int) list -> t -> t end module Symbol : @@ -250,3 +252,4 @@ val sortcheck_app : (Sort.tycon -> bool) -> (Symbol.t -> Sort.t option) -> Sort.t option -> Symbol.t -> expr list -> (Sort.sub * Sort.t) option val into_of_expr : expr -> int option + diff --git a/external/fixpoint/fixLex.mll b/external/fixpoint/fixLex.mll --- a/external/fixpoint/fixLex.mll +++ b/external/fixpoint/fixLex.mll @@ -109,6 +109,10 @@ | '?' { QM } | '$' { DOL } | '.' { DOT } + | "iff" { IFFWORD } + | "if" { IFWORD } + | "then" { THENWORD } + | "else" { ELSEWORD } | "not" { NOTWORD } | "tag" { TAG } | "id" { ID } @@ -118,8 +122,8 @@ | ":=" { ASGN } | "&&" { AND } | "||" { OR } + | "<=>" { IFF } - | "iff" { IFFWORD } | "=>" { IMPL } | "!=" { NE } | "=" { EQ } diff --git a/external/fixpoint/fixParse.mly b/external/fixpoint/fixParse.mly --- a/external/fixpoint/fixParse.mly +++ b/external/fixpoint/fixParse.mly @@ -74,7 +74,7 @@ %token OBJ REAL INT NUM PTR LFUN BOOL UNINT FUNC LIT FRAC %token SRT AXM CON CST WF SOL QUL KUT BIND ADP DDP %token ENV GRD LHS RHS REF - +%token IFWORD THENWORD ELSEWORD %right IFF IFFWORD %right IMPL %left PLUS @@ -235,15 +235,15 @@ ; pred: - TRUE { A.pTrue } - | FALSE { A.pFalse } + TRUE { A.pTrue } + | FALSE { A.pFalse } | BEXP expr { A.pBexp $2 } | QM expr { A.pBexp $2 } | Id LPAREN argsne RPAREN { A.pBexp (A.eApp ((Sy.of_string $1), $3)) } - | AND preds { A.pAnd ($2) } - | OR preds { A.pOr ($2) } - | NOT pred { A.pNot ($2) } - | NOTWORD pred { A.pNot ($2) } + | AND preds { A.pAnd ($2) } + | OR preds { A.pOr ($2) } + | NOT pred { A.pNot ($2) } + | NOTWORD pred { A.pNot ($2) } | LPAREN pred AND pred RPAREN { A.pAnd [$2; $4] } | LPAREN pred OR pred RPAREN { A.pOr [$2; $4] } | expr rel expr { A.pAtom ($1, $2, $3) } @@ -283,6 +283,7 @@ | 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)]) } | LPAREN pred QM expr COLON expr RPAREN { A.eIte ($2,$4,$6) } + | IFWORD pred THENWORD expr ELSEWORD expr { A.eIte ($2,$4,$6) } | expr DOT Id { A.eFld ((Sy.of_string $3), $1) } | LPAREN expr COLON sort RPAREN { A.eCst ($2, $4) } | LPAREN expr RPAREN { $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/smtZ3.ml b/external/fixpoint/smtZ3.ml new file mode 100644 --- /dev/null +++ b/external/fixpoint/smtZ3.ml @@ -0,0 +1,93 @@ +(* + * Copyright © 2008 The Regents of the University of California. All rights reserved. + * + * Permission is hereby granted, without written agreement and without + * license or royalty fees, to use, copy, modify, and distribute this + * software and its documentation for any purpose, provided that the + * above copyright notice and the following two paragraphs appear in + * all copies of this software. + * + * IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY + * FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES + * ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN + * IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY + * OF SUCH DAMAGE. + * + * THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, + * INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY + * AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS + * ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION + * TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS. + *) + +(********************************************************************************) +(** DUMMY SMT-Z3 Solver (for non Z3MEM builds) **********************************) +(********************************************************************************) + +let assertf = FixMisc.Ops.assertf +let msg = "This build is NOT linked against Z3. Please rebuild with Z3MEM=true. Only possible on linux" + +module SMTZ3 : ProverArch.SMTSOLVER = struct + +type context = () +type symbol = () +type sort = () +type ast = () +type fun_decl = () + +let var _ = failwith msg +let boundVar _ = failwith msg +let stringSymbol _ = failwith msg +let funcDecl _ = failwith msg +let isBool _ = failwith msg +let isInt _ = failwith msg +let mkAll _ = failwith msg +let mkRel _ = failwith msg +let mkApp _ = failwith msg +let mkMul _ = failwith msg +let mkDiv _ = failwith msg +let mkAdd _ = failwith msg +let mkSub _ = failwith msg +let mkMod _ = failwith msg +let mkIte _ = failwith msg +let mkInt _ = failwith msg +let mkLit _ = failwith msg +let mkReal _ = failwith msg +let mkTrue _ = failwith msg +let mkFalse _ = failwith msg +let mkNot _ = failwith msg +let mkAnd _ = failwith msg +let mkOr _ = failwith msg +let mkImp _ = failwith msg +let mkIff _ = failwith msg +let astString _ = failwith msg +let sortString _ = failwith msg +let mkIntSort _ = failwith msg +let mkRealSort _ = failwith msg +let mkBoolSort _ = failwith msg +let mkSetSort _ = failwith msg +let mkEmptySet _ = failwith msg +let mkSetAdd _ = failwith msg +let mkSetMem _ = failwith msg +let mkSetCup _ = failwith msg +let mkSetCap _ = failwith msg +let mkSetDif _ = failwith msg +let mkSetSub _ = failwith msg +let mkMapSort _ = failwith msg +let mkMapSelect _ = failwith msg +let mkMapStore _ = failwith msg +let mkSizeSort _ = failwith msg +let mkBitSort _ = failwith msg +let mkBitAnd _ = failwith msg +let mkBitOr _ = failwith msg +let mkContext _ = failwith msg +let unsat _ = failwith msg +let assertAxiom _ = failwith msg +let assertDistinct _ = failwith msg +let bracket _ = failwith msg +let assertPreds _ = failwith msg +let valid _ = failwith msg +let contra _ = failwith msg +let print_stats _ = failwith msg + +end diff --git a/external/misc/fixMisc.ml b/external/misc/fixMisc.ml --- a/external/misc/fixMisc.ml +++ b/external/misc/fixMisc.ml @@ -1360,4 +1360,6 @@ | s -> let c = s.[0] in c = Char.lowercase c - +let rec zipWith f = function + | (x::xs, y::ys) -> f x y::zipWith f (xs, ys) + | _ -> [] diff --git a/external/ocamlgraph/.depend b/external/ocamlgraph/.depend deleted file mode 100644 --- a/external/ocamlgraph/.depend +++ /dev/null @@ -1,128 +0,0 @@ -lib/bitv.cmo : lib/bitv.cmi -lib/bitv.cmx : lib/bitv.cmi -lib/heap.cmo : lib/heap.cmi -lib/heap.cmx : lib/heap.cmi -lib/unionfind.cmo : lib/unionfind.cmi -lib/unionfind.cmx : lib/unionfind.cmi -lib/bitv.cmi : -lib/heap.cmi : -lib/unionfind.cmi : -src/blocks.cmo : src/util.cmi src/sig.cmi -src/blocks.cmx : src/util.cmx src/sig.cmi -src/builder.cmo : src/sig.cmi src/builder.cmi -src/builder.cmx : src/sig.cmi src/builder.cmi -src/classic.cmo : src/sig.cmi src/builder.cmi src/classic.cmi -src/classic.cmx : src/sig.cmi src/builder.cmx src/classic.cmi -src/cliquetree.cmo : src/util.cmi src/sig.cmi src/persistent.cmi \ - src/oper.cmi src/gmap.cmi src/builder.cmi src/cliquetree.cmi -src/cliquetree.cmx : src/util.cmx src/sig.cmi src/persistent.cmx \ - src/oper.cmx src/gmap.cmx src/builder.cmx src/cliquetree.cmi -src/components.cmo : src/util.cmi src/sig.cmi src/components.cmi -src/components.cmx : src/util.cmx src/sig.cmi src/components.cmi -src/delaunay.cmo : src/delaunay.cmi -src/delaunay.cmx : src/delaunay.cmi -src/dot.cmo : src/dot_parser.cmi src/dot_lexer.cmo src/dot_ast.cmi \ - src/builder.cmi src/dot.cmi -src/dot.cmx : src/dot_parser.cmx src/dot_lexer.cmx src/dot_ast.cmi \ - src/builder.cmx src/dot.cmi -src/dot_lexer.cmo : src/dot_parser.cmi src/dot_ast.cmi -src/dot_lexer.cmx : src/dot_parser.cmx src/dot_ast.cmi -src/dot_parser.cmo : src/dot_ast.cmi src/dot_parser.cmi -src/dot_parser.cmx : src/dot_ast.cmi src/dot_parser.cmi -src/flow.cmo : src/util.cmi src/sig.cmi src/flow.cmi -src/flow.cmx : src/util.cmx src/sig.cmi src/flow.cmi -src/gcoloring.cmo : src/traverse.cmi src/sig.cmi src/gcoloring.cmi -src/gcoloring.cmx : src/traverse.cmx src/sig.cmi src/gcoloring.cmi -src/gmap.cmo : src/sig.cmi src/gmap.cmi -src/gmap.cmx : src/sig.cmi src/gmap.cmi -src/gml.cmo : src/builder.cmi src/gml.cmi -src/gml.cmx : src/builder.cmx src/gml.cmi -src/gpath.cmo : src/util.cmi src/sig.cmi lib/heap.cmi src/gpath.cmi -src/gpath.cmx : src/util.cmx src/sig.cmi lib/heap.cmx src/gpath.cmi -src/graphviz.cmo : src/graphviz.cmi -src/graphviz.cmx : src/graphviz.cmi -src/imperative.cmo : src/sig.cmi src/blocks.cmo lib/bitv.cmi \ - src/imperative.cmi -src/imperative.cmx : src/sig.cmi src/blocks.cmx lib/bitv.cmx \ - src/imperative.cmi -src/kruskal.cmo : src/util.cmi lib/unionfind.cmi src/sig.cmi src/kruskal.cmi -src/kruskal.cmx : src/util.cmx lib/unionfind.cmx src/sig.cmi src/kruskal.cmi -src/mcs_m.cmo : src/util.cmi src/sig.cmi src/persistent.cmi src/oper.cmi \ - src/imperative.cmi src/gmap.cmi src/builder.cmi src/mcs_m.cmi -src/mcs_m.cmx : src/util.cmx src/sig.cmi src/persistent.cmx src/oper.cmx \ - src/imperative.cmx src/gmap.cmx src/builder.cmx src/mcs_m.cmi -src/md.cmo : src/sig.cmi src/oper.cmi src/gmap.cmi src/cliquetree.cmi \ - src/builder.cmi src/md.cmi -src/md.cmx : src/sig.cmi src/oper.cmx src/gmap.cmx src/cliquetree.cmx \ - src/builder.cmx src/md.cmi -src/minsep.cmo : src/sig.cmi src/oper.cmi src/components.cmi src/minsep.cmi -src/minsep.cmx : src/sig.cmi src/oper.cmx src/components.cmx src/minsep.cmi -src/oper.cmo : src/sig.cmi src/builder.cmi src/oper.cmi -src/oper.cmx : src/sig.cmi src/builder.cmx src/oper.cmi -src/pack.cmo : src/traverse.cmi src/topological.cmi src/sig.cmi src/rand.cmi \ - src/oper.cmi src/kruskal.cmi src/imperative.cmi src/graphviz.cmi \ - src/gpath.cmi src/gml.cmi src/flow.cmi src/dot.cmi src/components.cmi \ - src/classic.cmi src/builder.cmi src/pack.cmi -src/pack.cmx : src/traverse.cmx src/topological.cmx src/sig.cmi src/rand.cmx \ - src/oper.cmx src/kruskal.cmx src/imperative.cmx src/graphviz.cmx \ - src/gpath.cmx src/gml.cmx src/flow.cmx src/dot.cmx src/components.cmx \ - src/classic.cmx src/builder.cmx src/pack.cmi -src/persistent.cmo : src/util.cmi src/sig.cmi src/blocks.cmo \ - src/persistent.cmi -src/persistent.cmx : src/util.cmx src/sig.cmi src/blocks.cmx \ - src/persistent.cmi -src/rand.cmo : src/sig.cmi src/delaunay.cmi src/builder.cmi src/rand.cmi -src/rand.cmx : src/sig.cmi src/delaunay.cmx src/builder.cmx src/rand.cmi -src/strat.cmo : src/sig.cmi src/strat.cmi -src/strat.cmx : src/sig.cmi src/strat.cmi -src/topological.cmo : src/sig.cmi src/topological.cmi -src/topological.cmx : src/sig.cmi src/topological.cmi -src/traverse.cmo : src/sig.cmi src/traverse.cmi -src/traverse.cmx : src/sig.cmi src/traverse.cmi -src/util.cmo : src/sig.cmi src/util.cmi -src/util.cmx : src/sig.cmi src/util.cmi -src/version.cmo : -src/version.cmx : -src/builder.cmi : src/sig.cmi -src/classic.cmi : src/sig.cmi -src/cliquetree.cmi : src/sig.cmi -src/components.cmi : src/util.cmi src/sig.cmi -src/delaunay.cmi : -src/dot.cmi : src/dot_ast.cmi src/builder.cmi -src/dot_ast.cmi : -src/dot_parser.cmi : src/dot_ast.cmi -src/flow.cmi : src/sig.cmi -src/gcoloring.cmi : src/sig.cmi -src/gmap.cmi : src/sig.cmi -src/gml.cmi : src/builder.cmi -src/gpath.cmi : src/sig.cmi -src/graphviz.cmi : -src/imperative.cmi : src/sig.cmi -src/kruskal.cmi : src/sig.cmi -src/mcs_m.cmi : src/sig.cmi -src/md.cmi : src/sig.cmi -src/minsep.cmi : src/sig.cmi -src/oper.cmi : src/sig.cmi src/builder.cmi -src/pack.cmi : src/sig_pack.cmi -src/persistent.cmi : src/sig.cmi -src/rand.cmi : src/sig.cmi src/builder.cmi -src/sig.cmi : -src/sig_pack.cmi : -src/strat.cmi : src/sig.cmi -src/topological.cmi : src/sig.cmi -src/traverse.cmi : src/sig.cmi -src/util.cmi : src/sig.cmi -editor/ed_display.cmo : -editor/ed_display.cmx : -editor/ed_draw.cmo : src/components.cmi -editor/ed_draw.cmx : src/components.cmx -editor/ed_graph.cmo : src/traverse.cmi src/imperative.cmi src/graphviz.cmi \ - src/gml.cmi src/dot_ast.cmi src/dot.cmi src/components.cmi \ - src/builder.cmi -editor/ed_graph.cmx : src/traverse.cmx src/imperative.cmx src/graphviz.cmx \ - src/gml.cmx src/dot_ast.cmi src/dot.cmx src/components.cmx \ - src/builder.cmx -editor/ed_hyper.cmo : -editor/ed_hyper.cmx : -editor/ed_main.cmo : -editor/ed_main.cmx : diff --git a/external/ocamlgraph/src/dot_lexer.ml b/external/ocamlgraph/src/dot_lexer.ml new file mode 100644 --- /dev/null +++ b/external/ocamlgraph/src/dot_lexer.ml @@ -0,0 +1,386 @@ +# 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 new file mode 100644 --- /dev/null +++ b/external/ocamlgraph/src/dot_parser.ml @@ -0,0 +1,551 @@ +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 new file mode 100644 --- /dev/null +++ b/external/ocamlgraph/src/dot_parser.mli @@ -0,0 +1,21 @@ +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 new file mode 100644 --- /dev/null +++ b/external/ocamlgraph/src/gml.ml @@ -0,0 +1,670 @@ +# 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 new file mode 100644 --- /dev/null +++ b/external/ocamlgraph/src/version.ml @@ -0,0 +1,2 @@ +let version = "0.99b" +let date = "Wed Aug 12 18:13:31 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.3.0.1 +version: 0.4.0.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 @@ -8,16 +8,16 @@ author: Ranjit Jhala, Niki Vazou, Eric Seidel maintainer: jhala@cs.ucsd.edu category: Language -build-type: Custom -cabal-version: >=1.8 +build-type: Custom +cabal-version: >=1.10 description: This package is a Haskell wrapper to the SMTLIB-based Horn-Clause/Logical Implication constraint solver used - for Liquid Types. + for Liquid Types. . - The solver itself is written in Ocaml. + The solver itself is written in Ocaml. . - The package includes: + The package includes: . 1. Types for Expressions, Predicates, Constraints, Solutions . @@ -31,7 +31,7 @@ . Requirements . - In addition to the .cabal dependencies you require + In addition to the .cabal dependencies you require . - A Z3 () or CVC4 () binary. If on Windows, please make sure to place the binary and any associated DLLs @@ -49,7 +49,6 @@ , external/fixpoint/*.mly , external/misc/*.ml , external/misc/*.mli - , external/ocamlgraph/.depend , external/ocamlgraph/Makefile.in , external/ocamlgraph/META.in , external/ocamlgraph/configure @@ -93,6 +92,7 @@ -- fixpoint.native as an executable, and properly symlink it when -- asked. Executable fixpoint.native + default-language: Haskell98 Main-is: Fixpoint.hs Build-Depends: base >= 4.7 && < 5 , array @@ -115,9 +115,10 @@ , unordered-containers , text-format , liquid-fixpoint - + Executable fixpoint + default-language: Haskell98 Main-is: Fixpoint.hs Build-Depends: base >= 4.7 && < 5 , array @@ -143,6 +144,7 @@ , liquid-fixpoint Library + default-language: Haskell98 hs-source-dirs: src Exposed-Modules: Language.Fixpoint.Names, Language.Fixpoint.Files, @@ -152,19 +154,25 @@ Language.Fixpoint.Bitvector, Language.Fixpoint.Visitor, Language.Fixpoint.Sort, - Language.Fixpoint.Interface, + Language.Fixpoint.Interface, Language.Fixpoint.Parse, Language.Fixpoint.PrettyPrint, - Language.Fixpoint.SmtLib2, + Language.Fixpoint.Smt.Types, + Language.Fixpoint.Smt.Theories, + Language.Fixpoint.Smt.Serialize, + Language.Fixpoint.Smt.Interface, Language.Fixpoint.Misc, Language.Fixpoint.Solver.Solution, Language.Fixpoint.Solver.Worklist, Language.Fixpoint.Solver.Monad, Language.Fixpoint.Solver.Deps, + Language.Fixpoint.Solver.Uniqify, Language.Fixpoint.Solver.Eliminate, Language.Fixpoint.Solver.Validate, + Language.Fixpoint.Partition, + Language.Fixpoint.Statistics, Language.Fixpoint.Solver.Solve - + Build-Depends: base >= 4.7 && < 5 , array , attoparsec diff --git a/src/Language/Fixpoint/Config.hs b/src/Language/Fixpoint/Config.hs --- a/src/Language/Fixpoint/Config.hs +++ b/src/Language/Fixpoint/Config.hs @@ -1,10 +1,8 @@ {-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE UndecidableInstances #-} - module Language.Fixpoint.Config ( Config (..) , getOpts @@ -13,16 +11,10 @@ , GenQualifierSort (..) , UeqAllSorts (..) , withTarget - , withUEqAllSorts ) where import System.Console.CmdArgs -import System.Console.CmdArgs.Verbosity (whenLoud) -import Data.Generics (Data) -import Data.Typeable (Typeable) import Language.Fixpoint.Files -import System.Console.CmdArgs.Default -import System.FilePath class Command a where @@ -35,6 +27,8 @@ withTarget :: Config -> FilePath -> Config withTarget cfg fq = cfg { inFile = fq } { outFile = fq `withExt` Out } + + data Config = Config { inFile :: FilePath -- ^ target fq-file @@ -46,17 +40,20 @@ , native :: Bool -- ^ use haskell solver , real :: Bool -- ^ interpret div and mul in SMT , eliminate :: Bool -- ^ eliminate non-cut KVars + , metadata :: Bool -- ^ print meta-data associated with constraints + , stats :: Bool -- ^ compute constraint statistics + , parts :: Bool -- ^ partition FInfo into separate fq files } deriving (Eq,Data,Typeable,Show) instance Default Config where - def = Config "" def def def def def def def def - + def = Config "" def def def def def def def def def def def + instance Command Config where command c = command (genSorts c) ++ command (ueqAllSorts c) ++ command (solver c) ++ " -out " - ++ (outFile c) ++ " " ++ (inFile c) + ++ outFile c ++ " " ++ inFile c --------------------------------------------------------------------------------------- -- newtype OFilePath = O FilePath @@ -88,7 +85,6 @@ command (UAS True) = " -ueq-all-sorts " command (UAS False) = "" -withUEqAllSorts c b = c { ueqAllSorts = UAS b } --------------------------------------------------------------------------------------- @@ -116,22 +112,25 @@ -- defaultSolver :: Maybe SMTSolver -> SMTSolver -- defaultSolver = fromMaybe Z3 - +config :: Config config = Config { inFile = def &= typ "TARGET" &= args &= typFile , outFile = "out" &= help "Output file" , srcFile = def &= help "Source File from which FQ is generated" , solver = def &= help "Name of SMT Solver" , genSorts = def &= help "Generalize qualifier sorts" - , ueqAllSorts = def &= help "use UEq on all sorts" + , ueqAllSorts = def &= help "Use UEq on all sorts" , native = False &= help "(alpha) Haskell Solver" , real = False &= help "(alpha) Theory of real numbers" , eliminate = False &= help "(alpha) Eliminate non-cut KVars" + , metadata = False &= help "Print meta-data associated with constraints" + , stats = False &= help "Compute constraint statistics" + , parts = False &= help "Partition constraints into indepdendent .fq files" } &= verbosity &= program "fixpoint" &= help "Predicate Abstraction Based Horn-Clause Solver" - &= summary "fixpoint Copyright 2009-13 Regents of the University of California." + &= summary "fixpoint Copyright 2009-15 Regents of the University of California." &= details [ "Predicate Abstraction Based Horn-Clause Solver" , "" , "To check a file foo.fq type:" @@ -140,9 +139,9 @@ getOpts :: IO Config getOpts = do md <- cmdArgs config - putStrLn $ banner md + putStrLn banner return md -banner args = "Liquid-Fixpoint Copyright 2009-13 Regents of the University of California.\n" - ++ "All Rights Reserved.\n" - +banner :: String +banner = "Liquid-Fixpoint Copyright 2009-13 Regents of the University of California.\n" + ++ "All Rights Reserved.\n" diff --git a/src/Language/Fixpoint/Errors.hs b/src/Language/Fixpoint/Errors.hs --- a/src/Language/Fixpoint/Errors.hs +++ b/src/Language/Fixpoint/Errors.hs @@ -37,11 +37,9 @@ import GHC.Generics (Generic) import Language.Fixpoint.PrettyPrint import Language.Fixpoint.Types -import System.FilePath import Text.Parsec.Pos import Text.PrettyPrint.HughesPJ import Text.Printf -import Control.Exception (catch) ----------------------------------------------------------------------- -- | A Reusable SrcSpan Type ------------------------------------------ diff --git a/src/Language/Fixpoint/Files.hs b/src/Language/Fixpoint/Files.hs --- a/src/Language/Fixpoint/Files.hs +++ b/src/Language/Fixpoint/Files.hs @@ -34,9 +34,7 @@ import Data.List hiding (find) import Data.Maybe (fromMaybe) import System.Directory -import System.Environment import System.FilePath --- import System.FilePath.Find import Language.Fixpoint.Misc ------------------------------------------------------------ @@ -60,26 +58,28 @@ if ex then return p else errorstar $ "Cannot find " ++ msg ++ " at :" ++ p ------------------------------------------------------------------------------------ + ----------------------------------------------------------------------------------- -data Ext = Cgi -- ^ Constraint Generation Information - | Fq -- ^ Input to constraint solving (fixpoint) - | Out -- ^ Output from constraint solving (fixpoint) - | Html -- ^ HTML file with inferred type annotations - | Annot -- ^ Text file with inferred types - | Vim -- ^ Vim annotation file - | Hs -- ^ Haskell source - | LHs -- ^ Literate Haskell source - | Js -- ^ JavaScript source - | Ts -- ^ Typescript source - | Spec -- ^ Spec file (e.g. include/Prelude.spec) - | Hquals -- ^ Qualifiers file (e.g. include/Prelude.hquals) - | Result -- ^ Final result: SAFE/UNSAFE - | Cst -- ^ HTML file with templates? - | Mkdn -- ^ Markdown file (temporarily generated from .Lhs + annots) - | Json -- ^ JSON file containing result (annots + errors) - | Saved -- ^ Previous source (for incremental checking) - | Cache -- ^ Previous output (for incremental checking) +data Ext = Cgi -- ^ Constraint Generation Information + | Fq -- ^ Input to constraint solving (fixpoint) + | Out -- ^ Output from constraint solving (fixpoint) + | Html -- ^ HTML file with inferred type annotations + | Annot -- ^ Text file with inferred types + | Vim -- ^ Vim annotation file + | Hs -- ^ Haskell source + | LHs -- ^ Literate Haskell source + | Js -- ^ JavaScript source + | Ts -- ^ Typescript source + | Spec -- ^ Spec file (e.g. include/Prelude.spec) + | Hquals -- ^ Qualifiers file (e.g. include/Prelude.hquals) + | Result -- ^ Final result: SAFE/UNSAFE + | Cst -- ^ HTML file with templates? + | Mkdn -- ^ Markdown file (temporarily generated from .Lhs + annots) + | Json -- ^ JSON file containing result (annots + errors) + | Saved -- ^ Previous source (for incremental checking) + | Cache -- ^ Previous output (for incremental checking) + | Dot -- ^ Constraint Graph + | Part Int -- ^ Partition | Pred | PAss | Dat @@ -88,28 +88,30 @@ extMap e = go e where - go Cgi = ".cgi" - go Pred = ".pred" - go PAss = ".pass" - go Dat = ".dat" - go Out = ".fqout" - go Fq = ".fq" - go Html = ".html" - go Cst = ".cst" - go Annot = ".annot" - go Vim = ".vim.annot" - go Hs = ".hs" - go LHs = ".lhs" - go Js = ".js" - go Ts = ".ts" - go Mkdn = ".markdown" - go Json = ".json" - go Spec = ".spec" - go Hquals = ".hquals" - go Result = ".out" - go Saved = ".bak" - go Cache = ".err" - go Smt2 = ".smt2" + go Cgi = ".cgi" + go Pred = ".pred" + go PAss = ".pass" + go Dat = ".dat" + go Out = ".fqout" + go Fq = ".fq" + go Html = ".html" + go Cst = ".cst" + go Annot = ".annot" + go Vim = ".vim.annot" + go Hs = ".hs" + go LHs = ".lhs" + go Js = ".js" + go Ts = ".ts" + go Mkdn = ".markdown" + go Json = ".json" + go Spec = ".spec" + go Hquals = ".hquals" + go Result = ".out" + go Saved = ".bak" + go Cache = ".err" + go Smt2 = ".smt2" + go Dot = ".dot" + go (Part n) = "." ++ show n -- go _ = errorstar $ "extMap: Unknown extension " ++ show e withExt :: FilePath -> Ext -> FilePath diff --git a/src/Language/Fixpoint/Interface.hs b/src/Language/Fixpoint/Interface.hs --- a/src/Language/Fixpoint/Interface.hs +++ b/src/Language/Fixpoint/Interface.hs @@ -1,6 +1,7 @@ -- | This module implements the top-level API for interfacing with Fixpoint -- In particular it exports the functions that solve constraints supplied -- either as .fq files or as FInfo. +{-# LANGUAGE CPP #-} module Language.Fixpoint.Interface ( @@ -20,123 +21,148 @@ , parseFInfo ) where -import Data.Functor --- import Data.Hashable +import Control.Monad (when) import qualified Data.HashMap.Strict as M -import Data.List +import Data.List hiding (partition) + +#if __GLASGOW_HASKELL__ < 710 +import Data.Functor import Data.Monoid (mconcat, mempty) --- import System.Directory (getTemporaryDirectory) +import Data.Hashable +import System.Directory (getTemporaryDirectory) +import System.FilePath (()) +#endif + + import System.Exit --- import System.FilePath (()) -import System.IO (IOMode (..), hPutStr, - withFile) +import System.IO (IOMode (..), hPutStr, withFile) import Text.Printf import Language.Fixpoint.Solver.Eliminate (eliminateAll) +import Language.Fixpoint.Solver.Uniqify (renameAll) import qualified Language.Fixpoint.Solver.Solve as S -import Language.Fixpoint.Config -import Language.Fixpoint.Files +import Language.Fixpoint.Config hiding (solver) +import Language.Fixpoint.Files hiding (Result) import Language.Fixpoint.Misc +import Language.Fixpoint.Statistics (statistics) +import Language.Fixpoint.Partition (partition) import Language.Fixpoint.Parse (rr, rr') import Language.Fixpoint.Types hiding (kuts, lits) import Language.Fixpoint.Errors (exit) import Language.Fixpoint.PrettyPrint (showpp) --- import System.Console.CmdArgs.Default -import System.Console.CmdArgs.Verbosity +import System.Console.CmdArgs.Verbosity hiding (Loud) import Text.PrettyPrint.HughesPJ - --------------------------------------------------------------------------- --- | Solve FInfo system of horn-clause constraints ------------------------ ---------------------------------------------------------------------------- -solve :: Config -> FInfo a -> IO (Result a) -solve cfg - | native cfg = S.solve cfg - | otherwise = solveExt cfg - ---------------------------------------------------------------------------- -- | Solve .fq File ------------------------------------------------------- --------------------------------------------------------------------------- solveFQ :: Config -> IO ExitCode --------------------------------------------------------------------------- solveFQ cfg - | native cfg = solveNative' cfg - | otherwise = solveFile cfg - + | native cfg = solveNative cfg (solve cfg) + | otherwise = solveFile cfg --------------------------------------------------------------------------- --- | Fake Dependencies Harness Solver +-- | Solve FInfo system of horn-clause constraints ------------------------ --------------------------------------------------------------------------- -solveNative :: Config -> IO ExitCode -solveNative cfg - = do let file = inFile cfg - str <- readFile file - let fi = rr' file str :: FInfo () - let res = eliminateAll fi - putStrLn $ "Result: \n" ++ (render $ toFixpoint res) - error "TODO: solveNative" + -- parts cfg = partition cfg x + -- stats cfg = statistics cfg x + -- native cfg = solveNativeWithFInfo cfg x + -- otherwise = solveExt cfg x +solve :: (Fixpoint a) => Config -> FInfo a -> IO (Result a) +solve cfg + | parts cfg = partition cfg + | stats cfg = statistics cfg + | native cfg = solveNativeWithFInfo cfg + | otherwise = solveExt cfg + --------------------------------------------------------------------------- -- | Native Haskell Solver --------------------------------------------------------------------------- -solveNative' :: Config -> IO ExitCode -solveNative' cfg = exit (ExitFailure 2) $ do +solveNative :: Config -> (FInfo () -> IO (Result ())) -> IO ExitCode +solveNative cfg s = exit (ExitFailure 2) $ do let file = inFile cfg str <- readFile file let fi = rr' file str :: FInfo () - let fi' = if eliminate cfg then eliminateAll fi else fi - (res, s) <- S.solve cfg fi' - let res' = sid <$> res - putStrLn $ "Solution:\n" ++ showpp s - putStrLn $ "Result: " ++ show res' - return $ resultExit res' + res <- s fi + return $ resultExit (resStatus res) +solveNativeWithFInfo :: (Fixpoint a) => Config -> FInfo a -> IO (Result a) +solveNativeWithFInfo cfg fi = do + whenLoud $ putStrLn $ "fq file in: \n" ++ render (toFixpoint cfg fi) + donePhase Loud "Read Constraints" + let fi' = renameAll fi + whenLoud $ putStrLn $ "fq file after uniqify: \n" ++ render (toFixpoint cfg fi') + donePhase Loud "Uniqify" + fi'' <- elim cfg fi' + donePhase Loud "Eliminate" + whenLoud $ putStrLn $ "fq file after eliminate: \n" ++ render (toFixpoint cfg fi') + Result stat soln <- S.solve cfg fi'' + donePhase Loud "Solve" + let stat' = sid <$> stat + putStrLn $ "Solution:\n" ++ showpp soln + putStrLn $ "Result: " ++ show stat' + return $ Result stat soln + + +elim :: (Fixpoint a) => Config -> FInfo a -> IO (FInfo a) +elim cfg fi + | eliminate cfg = do let fi' = eliminateAll fi + whenLoud $ putStrLn $ "fq file after eliminate: \n" ++ render (toFixpoint cfg fi') + return fi' + | otherwise = return fi + --------------------------------------------------------------------------- -- | External Ocaml Solver --------------------------------------------------------------------------- -solveExt :: Config -> FInfo a -> IO (Result a) +solveExt :: (Fixpoint a) => Config -> FInfo a -> IO (Result a) solveExt cfg fi = {-# SCC "Solve" #-} execFq cfg fn fi >>= {-# SCC "exitFq" #-} exitFq fn (cm fi) where fn = srcFile cfg +execFq :: (Fixpoint a) => Config -> FilePath -> FInfo a -> IO ExitCode execFq cfg fn fi = do writeFile fq qstr withFile fq AppendMode (\h -> {-# SCC "HPrintDump" #-} hPutStr h (render d)) solveFile $ cfg `withTarget` fq where fq = extFileName Fq fn - d = {-# SCC "FixPointify" #-} toFixpoint fi - qstr = render ((vcat $ toFix <$> quals fi) $$ text "\n") + d = {-# SCC "FixPointify" #-} toFixpoint cfg fi + qstr = render (vcat (toFix <$> quals fi) $$ text "\n") solveFile :: Config -> IO ExitCode solveFile cfg = do fp <- getFixpointPath z3 <- getZ3LibPath v <- (\b -> if b then "-v 1" else "") <$> isLoud - {-# SCC "sysCall:Fixpoint" #-} executeShellCommand "fixpoint" $ fixCommand cfg fp z3 v - -fixCommand cfg fp z3 verbosity - = printf "LD_LIBRARY_PATH=%s %s %s %s -notruekvars -refinesort -nosimple -strictsortcheck -sortedquals %s" - z3 fp verbosity rf (command cfg) - where - rf = if real cfg then realFlags else "" + {-# SCC "sysCall:Fixpoint" #-} executeShellCommand "fixpoint" $ fixCommand fp z3 v + where + fixCommand fp z3 verbosity + = printf "LD_LIBRARY_PATH=%s %s %s %s -notruekvars -refinesort -nosimple -strictsortcheck -sortedquals %s" + z3 fp verbosity rf (command cfg) + where + rf = if real cfg then realFlags else "" +realFlags :: String realFlags = "-no-uif-multiply " ++ "-no-uif-divide " + +exitFq :: FilePath -> M.HashMap Integer (SubC a) -> ExitCode -> IO (Result a) exitFq _ _ (ExitFailure n) | n /= 1 - = return (Crash [] "Unknown Error", M.empty) -exitFq fn cm _ + = return $ Result (Crash [] "Unknown Error") M.empty +exitFq fn z _ = do str <- {-# SCC "readOut" #-} readFile (extFileName Out fn) - let (x, y) = parseFixpointOutput str -- {-# SCC "parseFixOut" #-} rr ({-# SCC "sanitizeFixpointOutput" #-} sanitizeFixpointOutput str) - return $ (plugC cm x, y) - where - plugC = fmap . mlookup + let (x, y) = parseFixpointOutput str + let x' = fmap (mlookup z) x + return $ Result x' y parseFixpointOutput :: String -> (FixResult Integer, FixSolution) parseFixpointOutput str = {-# SCC "parseFixOut" #-} rr ({-# SCC "sanitizeFixpointOutput" #-} sanitizeFixpointOutput str) +sanitizeFixpointOutput :: String -> String sanitizeFixpointOutput = unlines . filter (not . ("//" `isPrefixOf`)) @@ -164,36 +190,3 @@ let fi = rr' f str :: FInfo () return $ mempty { quals = quals fi , gs = gs fi } - --- OLD CUT USE NEW SMTLIB INTERFACE --------------------------------------------------------------------------- --- OLD CUT USE NEW SMTLIB INTERFACE -- | One Shot validity query ---------------------------------------------- --- OLD CUT USE NEW SMTLIB INTERFACE --------------------------------------------------------------------------- --- OLD CUT USE NEW SMTLIB INTERFACE --- OLD CUT USE NEW SMTLIB INTERFACE --------------------------------------------------------------------------- --- OLD CUT USE NEW SMTLIB INTERFACE checkValid :: (Hashable a) => a -> [(Symbol, Sort)] -> Pred -> IO (FixResult a) --- OLD CUT USE NEW SMTLIB INTERFACE --------------------------------------------------------------------------- --- OLD CUT USE NEW SMTLIB INTERFACE checkValid n xts p --- OLD CUT USE NEW SMTLIB INTERFACE = do file <- ( show (hash n)) <$> getTemporaryDirectory --- OLD CUT USE NEW SMTLIB INTERFACE (r, _) <- solve def file [] $ validFInfo n xts p --- OLD CUT USE NEW SMTLIB INTERFACE return (sinfo <$> r) --- OLD CUT USE NEW SMTLIB INTERFACE --- OLD CUT USE NEW SMTLIB INTERFACE validFInfo :: a -> [(Symbol, Sort)] -> Pred -> FInfo a --- OLD CUT USE NEW SMTLIB INTERFACE validFInfo l xts p = FI constrm [] benv emptySEnv [] ksEmpty [] --- OLD CUT USE NEW SMTLIB INTERFACE where --- OLD CUT USE NEW SMTLIB INTERFACE constrm = M.singleton 0 $ validSubc l ibenv p --- OLD CUT USE NEW SMTLIB INTERFACE binds = [(x, trueSortedReft t) | (x, t) <- xts] --- OLD CUT USE NEW SMTLIB INTERFACE ibenv = insertsIBindEnv bids emptyIBindEnv --- OLD CUT USE NEW SMTLIB INTERFACE (bids, benv) = foldlMap (\e (x,t) -> insertBindEnv x t e) emptyBindEnv binds --- OLD CUT USE NEW SMTLIB INTERFACE --- OLD CUT USE NEW SMTLIB INTERFACE validSubc :: a -> IBindEnv -> Pred -> SubC a --- OLD CUT USE NEW SMTLIB INTERFACE validSubc l env p = safeHead "Interface.validSubC" $ subC env PTrue lhs rhs i t l --- OLD CUT USE NEW SMTLIB INTERFACE where --- OLD CUT USE NEW SMTLIB INTERFACE lhs = mempty --- OLD CUT USE NEW SMTLIB INTERFACE rhs = RR mempty (predReft p) --- OLD CUT USE NEW SMTLIB INTERFACE i = Just 0 --- OLD CUT USE NEW SMTLIB INTERFACE t = [] --- OLD CUT USE NEW SMTLIB INTERFACE --- OLD CUT USE NEW SMTLIB INTERFACE result :: a -> Bool -> FixResult a --- OLD CUT USE NEW SMTLIB INTERFACE result _ True = Safe --- OLD CUT USE NEW SMTLIB INTERFACE result x False = Unsafe [x] --- OLD CUT USE NEW SMTLIB INTERFACE diff --git a/src/Language/Fixpoint/Misc.hs b/src/Language/Fixpoint/Misc.hs --- a/src/Language/Fixpoint/Misc.hs +++ b/src/Language/Fixpoint/Misc.hs @@ -17,8 +17,7 @@ import qualified Data.HashMap.Strict as M import qualified Data.List as L import Data.Tuple (swap) -import Data.Maybe (fromJust) -import Data.Maybe (catMaybes, fromMaybe) +import Data.Maybe (fromJust, catMaybes, fromMaybe) import qualified Data.Text as T import Data.Data @@ -128,12 +127,12 @@ mapPair :: (a -> b) -> (a, a) -> (b, b) mapPair f (x, y) = (f x, f y) --- mlookup :: (Show k, Hashable k) => M.HashMap k v -> k -> v -mlookup m k - = case M.lookup k m of - Just v -> v - Nothing -> errorstar $ "mlookup: unknown key " ++ show k +mlookup :: (Eq k, Show k, Hashable k) => M.HashMap k v -> k -> v +mlookup m k = case M.lookup k m of + Just v -> v + Nothing -> errorstar $ "mlookup: unknown key " ++ show k +safeLookup :: (Eq k, Hashable k) => String -> k -> M.HashMap k v -> v safeLookup msg k m = fromMaybe (errorstar msg) (M.lookup k m) mfromJust :: String -> Maybe a -> a @@ -166,6 +165,9 @@ groupList = M.toList . group +groupFun :: (Eq k, Hashable k) => M.HashMap k Int -> k -> Int +groupFun m k = safeLookup "groupFun" k m + mkGraph :: (Eq a, Eq b, Hashable a, Hashable b) => [(a, b)] -> M.HashMap a (S.HashSet b) mkGraph = fmap S.fromList . group @@ -301,6 +303,7 @@ Just n -> take n xs Nothing -> xs +chopPrefix :: (Eq a) => [a] -> [a] -> Maybe [a] chopPrefix p xs | p `L.isPrefixOf` xs = Just $ drop (length p) xs diff --git a/src/Language/Fixpoint/Names.hs b/src/Language/Fixpoint/Names.hs --- a/src/Language/Fixpoint/Names.hs +++ b/src/Language/Fixpoint/Names.hs @@ -29,7 +29,7 @@ , takeModuleNames -- * Creating Symbols - , dummySymbol, intSymbol, tempSymbol, existSymbol + , dummySymbol, intSymbol, tempSymbol, existSymbol, renameSymbol , qualifySymbol , suffixSymbol @@ -59,7 +59,6 @@ import qualified Data.HashSet as S import Data.Interned import Data.Interned.Internal.Text -import Data.Interned.Text import Data.Monoid import Data.String import Data.Text (Text) @@ -69,6 +68,7 @@ import Language.Fixpoint.Misc (errorstar, mapSnd, stripParens) + --------------------------------------------------------------- ---------------------------- Symbols -------------------------- --------------------------------------------------------------- @@ -205,16 +205,20 @@ dummySymbol = dummyName intSymbol :: (Show a) => Symbol -> a -> Symbol -intSymbol x i = x `mappend` symbol (show i) +intSymbol x i = x `mappend` symbol ('_' : show i) tempSymbol, existSymbol :: Symbol -> Integer -> Symbol tempSymbol prefix n = intSymbol (tempPrefix `mappend` prefix) n existSymbol prefix n = intSymbol (existPrefix `mappend` prefix) n +renameSymbol :: Symbol -> Int -> Symbol +renameSymbol prefix n = intSymbol (renamePrefix `mappend` prefix) n + tempPrefix, anfPrefix, existPrefix :: Symbol tempPrefix = "lq_tmp_" anfPrefix = "lq_anf_" existPrefix = "lq_ext_" +renamePrefix = "lq_rnm_" nonSymbol :: Symbol nonSymbol = "" @@ -248,7 +252,7 @@ boolConName = "Bool" funConName = "->" listConName = "[]" -- "List" -tupConName = "()" -- "Tuple" +tupConName = "Tuple" propConName = "Prop" hpropConName = "HProp" strConName = "Str" 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 @@ -4,6 +4,7 @@ {-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE DeriveGeneric #-} module Language.Fixpoint.Parse ( @@ -25,22 +26,26 @@ , blanks -- * Parsing basic entities - , fTyConP -- Type constructors + + -- fTyConP -- Type constructors , lowerIdP -- Lower-case identifiers , upperIdP -- Upper-case identifiers , symbolP -- Arbitrary Symbols , constantP -- (Integer) Constants , integer -- Integer , bindP -- Binder (lowerIdP <* colon) + , mkQual -- constructing qualifiers -- * Parsing recursive entities , exprP -- Expressions , predP -- Refinement Predicates , funAppP -- Function Applications , qualifierP -- Qualifiers + , refaP -- Refa , refP -- (Sorted) Refinements , refDefP -- (Sorted) Refinements with default binder , refBindP -- (Sorted) Refinements with configurable sub-parsers + , bvSortP -- Bit-Vector Sort -- * Some Combinators , condIdP -- condIdP :: [Char] -> (Text -> Bool) -> Parser Text @@ -60,29 +65,26 @@ ) where import Control.Applicative ((<$>), (<*), (*>), (<*>)) --- import Control.Monad import qualified Data.HashMap.Strict as M import qualified Data.HashSet as S --- import Data.Text (Text) import qualified Data.Text as T import Text.Parsec import Text.Parsec.Expr import Text.Parsec.Language -import Text.Parsec.Pos -import Text.Parsec.String hiding (Parser, parseFromFile) import qualified Text.Parsec.Token as Token import Text.Printf (printf) +import GHC.Generics (Generic) import Data.Char (isLower, toUpper) import Language.Fixpoint.Bitvector import Language.Fixpoint.Errors import Language.Fixpoint.Misc hiding (dcolon) -import Language.Fixpoint.SmtLib2 +import Language.Fixpoint.Smt.Types + import Language.Fixpoint.Types -import Language.Fixpoint.Names (vv, nilName, consName) import Language.Fixpoint.Visitor (foldSort, mapSort) -import Data.Maybe (fromJust, maybe) +import Data.Maybe (fromJust, fromMaybe, maybe) import Data.Monoid (mempty,mconcat) @@ -196,15 +198,14 @@ constantP :: Parser Constant constantP = try (R <$> double) - <|> I <$>integer + <|> I <$> integer symconstP :: Parser SymConst symconstP = SL . T.pack <$> stringLiteral expr0P :: Parser Expr expr0P - = (brackets whiteSpace >> return eNil) - <|> (fastIfP EIte exprP) + = (fastIfP EIte exprP) <|> (ESym <$> symconstP) <|> (ECon <$> constantP) <|> (reserved "_|_" >> return EBot) @@ -227,7 +228,16 @@ b2 <- bodyP return $ f p b1 b2 +qmIfP f bodyP + = parens $ do + p <- predP + reserved "?" + b1 <- bodyP + colon + b2 <- bodyP + return $ f p b1 b2 + expr1P :: Parser Expr expr1P = try funAppP @@ -250,32 +260,8 @@ t <- sortP return $ ECon $ L (T.pack l) t --- ORIG exprP :: Parser Expr --- ORIG exprP = expr2P <|> lexprP --- --- ORIG lexprP :: Parser Expr --- ORIG lexprP --- ORIG = try (parens exprP) --- ORIG <|> try (parens exprCastP) --- ORIG <|> try (parens $ condP EIte exprP) --- ORIG <|> try exprFunP --- ORIG <|> try (liftM (EVar . stringSymbol) upperIdP) --- ORIG <|> liftM expr symbolP --- ORIG <|> liftM ECon constantP --- ORIG <|> liftM ESym symconstP --- ORIG <|> (reserved "_|_" >> return EBot) --- ORIG --- ORIG exprFunP = (try exprFunSpacesP) <|> (try exprFunSemisP) <|> exprFunCommasP --- ORIG where --- ORIG exprFunSpacesP = parens $ liftM2 EApp funSymbolP (sepBy exprP spaces) --- ORIG exprFunCommasP = liftM2 EApp funSymbolP (parens $ sepBy exprP comma) --- ORIG exprFunSemisP = liftM2 EApp funSymbolP (parenBrackets $ sepBy exprP semi) --- ORIG funSymbolP = locParserP symbolP -- liftM stringSymbol lowerIdP - parenBrackets = parens . brackets --- ORIG expr2P = buildExpressionParser bops lexprP - bops = [ [ Prefix (reservedOp "-" >> return ENeg)] , [ Infix (reservedOp "*" >> return (EBin Times)) AssocLeft , Infix (reservedOp "/" >> return (EBin Div )) AssocLeft @@ -284,12 +270,11 @@ , Infix (reservedOp "+" >> return (EBin Plus )) AssocLeft ] , [ Infix (reservedOp "mod" >> return (EBin Mod )) AssocLeft] - , [ Infix (reservedOp ":" >> return (eCons )) AssocLeft] ] eMinus = EBin Minus (expr (0 :: Integer)) -eCons x xs = EApp (dummyLoc consName) [x,xs] -eNil = EVar nilName +-- eCons x xs = EApp (dummyLoc consName) [x, xs] +-- eNil = EVar nilName exprCastP = do e <- exprP @@ -310,9 +295,19 @@ <|> try (string "func" >> funcSortP) <|> try (fApp (Left listFTyCon) . single <$> brackets sortP) <|> try bvSortP - <|> try (fApp <$> (Left <$> fTyConP) <*> sepBy sortP blanks) + <|> try (fApp <$> (Left <$> fTyConP) <*> sepBy sortP blanks) <|> (FObj . symbol <$> lowerIdP) +fTyConP :: Parser FTycon +fTyConP + = (reserved "int" >> return intFTyCon) + <|> (reserved "Integer" >> return intFTyCon) + <|> (reserved "Int" >> return intFTyCon) + <|> (reserved "int" >> return intFTyCon) + <|> (reserved "real" >> return realFTyCon) + <|> (reserved "bool" >> return boolFTyCon) + <|> (symbolFTycon <$> locUpperIdP) + bvSortP = mkSort <$> (bvSizeP "Size32" S32 <|> bvSizeP "Size64" S64) @@ -320,8 +315,6 @@ parens (reserved "BitVec" >> parens (reserved ss >> reserved "obj")) return s - - keyWordSyms = ["if", "then", "else", "mod"] --------------------------------------------------------------------- @@ -351,7 +344,7 @@ kvarPredP = PKVar <$> kvarP <*> substP kvarP :: Parser KVar -kvarP = KV <$> (char '$' *> symbolP) +kvarP = KV <$> (char '$' *> symbolP <* spaces) substP :: Parser Subst substP = mkSubst <$> many (brackets $ pairP symbolP aP exprP) @@ -390,47 +383,16 @@ <|> (reservedOp ">" >> return (PAtom Gt)) <|> (reservedOp ">=" >> return (PAtom Ge)) -condP f bodyP - = try (condIteP f bodyP) - <|> (condQmP f bodyP) - -condI = condIteP EIte - - -condIteP f bodyP - = do reserved "if" - p <- predP - reserved "then" - b1 <- bodyP - reserved "else" - b2 <- bodyP - return $ f p b1 b2 - -condQmP f bodyP - = do p <- predP - reserved "?" - b1 <- bodyP - colon - b2 <- bodyP - return $ f p b1 b2 - ---------------------------------------------------------------------------------- ------------------------------------ BareTypes ----------------------------------- ---------------------------------------------------------------------------------- -fTyConP - = (reserved "int" >> return intFTyCon) - <|> (reserved "Integer" >> return intFTyCon) - <|> (reserved "Int" >> return intFTyCon) - <|> (reserved "int" >> return intFTyCon) - <|> (reserved "real" >> return realFTyCon) - <|> (reserved "bool" >> return boolFTyCon) - <|> (symbolFTycon <$> locUpperIdP) - refaP :: Parser Refa refaP = try (refa <$> brackets (sepBy predP semi)) <|> (Refa <$> predP) + + refBindP :: Parser Symbol -> Parser Refa -> Parser (Reft -> a) -> Parser a refBindP bp rp kindP = braces $ do @@ -451,14 +413,15 @@ -- | Parsing Qualifiers --------------------------------------------- --------------------------------------------------------------------- -qualifierP = do pos <- getPosition - n <- upperIdP - params <- parens $ sepBy1 sortBindP comma - _ <- colon - body <- predP - return $ mkQual n params body pos +qualifierP tP = do + pos <- getPosition + n <- upperIdP + params <- parens $ sepBy1 (sortBindP tP) comma + _ <- colon + body <- predP + return $ mkQual n params body pos -sortBindP = (,) <$> symbolP <* colon <*> sortP +sortBindP tP = (,) <$> symbolP <* colon <*> tP pairP :: Parser a -> Parser z -> Parser b -> Parser (a, b) pairP xP sepP yP = (,) <$> xP <* sepP <*> yP @@ -497,6 +460,20 @@ -- | Parsing Constraints (.fq files) -------------------------------- --------------------------------------------------------------------- +-- Entities in Query File +data Def a + = Srt Sort + | Axm Pred + | Cst (SubC a) + | Wfc (WfC a) + | Con Symbol Sort + | Qul Qualifier + | Kut KVar + | IBind Int Symbol SortedReft + deriving (Show, Generic) + -- Sol of solbind + -- Dep of FixConstraint.dep + fInfoP :: Parser (FInfo ()) fInfoP = defsFInfo <$> many defP @@ -506,7 +483,7 @@ <|> Cst <$> (reserved "constraint" >> colon >> subCP) <|> Wfc <$> (reserved "wf" >> colon >> wfCP) <|> Con <$> (reserved "constant" >> symbolP) <*> (colon >> sortP) - <|> Qul <$> (reserved "qualif" >> qualifierP) + <|> Qul <$> (reserved "qualif" >> qualifierP sortP) <|> Kut <$> (reserved "cut" >> kvarP) <|> IBind <$> (reserved "bind" >> intP) <*> symbolP <*> (colon >> sortedReftP) @@ -554,7 +531,7 @@ intP = fromInteger <$> integer defsFInfo :: [Def a] -> FInfo a -defsFInfo defs = FI cm ws bs gs lts kts qs +defsFInfo defs = FI cm ws bs gs lts kts qs mempty where cm = M.fromList [(cid c, c) | Cst c <- defs] ws = [w | Wfc w <- defs] @@ -595,7 +572,7 @@ return (k, simplify $ PAnd ps) where kvP = try kvarP <|> (KV <$> symbolP) - + solutionP :: Parser (M.HashMap KVar Pred) solutionP = M.fromList <$> sepBy solution1P whiteSpace diff --git a/src/Language/Fixpoint/Partition.hs b/src/Language/Fixpoint/Partition.hs new file mode 100644 --- /dev/null +++ b/src/Language/Fixpoint/Partition.hs @@ -0,0 +1,147 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DeriveGeneric #-} + +-- | This module implements functions that print out +-- statistics about the constraints. + +module Language.Fixpoint.Partition (partition, partition') where + +import Control.Monad (forM_) +import GHC.Generics (Generic) +import Language.Fixpoint.Misc hiding (group)-- (fst3, safeLookup, mlookup, groupList) +import Language.Fixpoint.Solver.Deps +import Language.Fixpoint.Files +import Language.Fixpoint.Config +import Language.Fixpoint.PrettyPrint +import qualified Language.Fixpoint.Visitor as V +import qualified Language.Fixpoint.Types as F +import qualified Data.HashMap.Strict as M +import qualified Data.Graph as G +import qualified Data.Tree as T +import Data.Hashable +import Text.PrettyPrint.HughesPJ +import Debug.Trace + +#if __GLASGOW_HASKELL__ < 710 +import Data.Monoid (mempty) +import System.Console.CmdArgs.Verbosity (whenLoud) +import Control.Applicative ((<$>)) +import Control.Arrow ((&&&)) +import Data.List (sort,group) +import Data.Maybe (mapMaybe) +import System.FilePath -- (dropExtension) +#endif + +partition :: (F.Fixpoint a) => Config -> F.FInfo a -> IO (F.Result a) +partition cfg fi + = do dumpPartitions cfg fis + dumpEdges cfg es + -- whenLoud $ putStrLn $ render $ ppGraph es + return mempty + where + (es, fis) = partition' fi + +partition' :: F.FInfo a -> (KVGraph, [F.FInfo a]) +partition' fi = (g, partitionByConstraints fi css) + where + es = kvEdges fi + g = kvGraph es + css = decompose g + +------------------------------------------------------------------------------------- +dumpPartitions :: (F.Fixpoint a) => Config -> [F.FInfo a ] -> IO () +------------------------------------------------------------------------------------- +dumpPartitions cfg fis = + forM_ (zip [1..] fis) $ \(j, fi) -> + writeFile (partFile cfg j) (render $ F.toFixpoint cfg fi) + +partFile :: Config -> Int -> FilePath +partFile cfg j = {- trace ("partFile: " ++ fjq) -} fjq + where + fjq = extFileName (Part j) (inFile cfg) + +------------------------------------------------------------------------------------- +dumpEdges :: Config -> KVGraph -> IO () +------------------------------------------------------------------------------------- +dumpEdges cfg = writeFile f . render . ppGraph + where + f = extFileName Dot (inFile cfg) + +ppGraph :: KVGraph -> Doc +ppGraph g = ppEdges [ (v, v') | (v,_,vs) <- g, v' <- vs] + +ppEdges :: [CEdge] -> Doc +ppEdges es = vcat [pprint v <+> text "-->" <+> pprint v' | (v, v') <- es] + +------------------------------------------------------------------------------------- +partitionByConstraints :: F.FInfo a -> KVComps -> [F.FInfo a] +------------------------------------------------------------------------------------- +partitionByConstraints fi kvss = mkPartition fi icM iwM <$> js + where + js = fst <$> jkvs -- groups + gc = groupFun cM -- (i, ci) |-> j + gk = groupFun kM -- k |-> j + + iwM = groupMap (wfGroup gk) (F.ws fi) -- j |-> [w] + icM = groupMap (gc . fst) (M.toList (F.cm fi)) -- j |-> [(i, ci)] + + jkvs = zip [1..] kvss + kvI = [ (x, j) | (j, kvs) <- jkvs, x <- kvs ] + kM = M.fromList [ (k, i) | (KVar k, i) <- kvI ] + cM = M.fromList [ (c, i) | (Cstr c, i) <- kvI ] + +mkPartition fi icM iwM j + = fi { F.cm = M.fromList $ M.lookupDefault [] j icM + , F.ws = M.lookupDefault [] j iwM } + +wfGroup gk w = case sortNub [gk k | k <- wfKvars w ] of + [i] -> i + _ -> errorstar $ "PARTITION: wfGroup" ++ show (F.wid w) + +wfKvars :: F.WfC a -> [F.KVar] +wfKvars = V.kvars . F.sr_reft . F.wrft + +------------------------------------------------------------------------------------- +------------------------------------------------------------------------------------- +------------------------------------------------------------------------------------- + +data CVertex = KVar F.KVar + | Cstr Integer + deriving (Eq, Ord, Show, Generic) + +instance PPrint CVertex where + pprint (KVar k) = pprint k + pprint (Cstr i) = text "id:" <+> pprint i + +instance Hashable CVertex + +type CEdge = (CVertex, CVertex) +type KVGraph = [(CVertex, CVertex, [CVertex])] + +type Comps a = [[a]] +type KVComps = Comps CVertex + +------------------------------------------------------------------------------------- +------------------------------------------------------------------------------------- +decompose :: KVGraph -> KVComps +------------------------------------------------------------------------------------- +decompose kg = {- tracepp "flattened" $ -} map (fst3 . f) <$> vss + where + (g,f,_) = G.graphFromEdges kg + vss = T.flatten <$> G.components g + +kvGraph :: [CEdge] -> KVGraph +kvGraph es = [(v,v,vs) | (v, vs) <- groupList es ] + +kvEdges :: F.FInfo a -> [CEdge] +kvEdges fi = selfes ++ concatMap (subcEdges bs) cs + where + bs = F.bs fi + cs = M.elems (F.cm fi) + selfes = [(Cstr i, Cstr i) | c <- cs, let i = F.subcId c] + +subcEdges :: F.BindEnv -> F.SubC a -> [CEdge] +subcEdges bs c = [(KVar k, Cstr i ) | k <- lhsKVars bs c] + ++ [(Cstr i, KVar k') | k' <- rhsKVars c ] + where + i = F.subcId c 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 @@ -52,6 +52,9 @@ instance PPrint Bool where pprint = text . show +instance PPrint Float where + pprint = text . show + instance PPrint () where pprint = text . show @@ -183,7 +186,6 @@ instance PPrint Refa where pprintPrec z (Refa p) = pprintPrec z p - pprintPrec _ k = toFix k instance PPrint Reft where pprint r@(Reft (_,ra)) diff --git a/src/Language/Fixpoint/Smt/Interface.hs b/src/Language/Fixpoint/Smt/Interface.hs new file mode 100644 --- /dev/null +++ b/src/Language/Fixpoint/Smt/Interface.hs @@ -0,0 +1,289 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE UndecidableInstances #-} + +-- | This module contains an SMTLIB2 interface for +-- 1. checking the validity, and, +-- 2. computing satisfying assignments +-- for formulas. +-- By implementing a binary interface over the SMTLIB2 format defined at +-- http://www.smt-lib.org/ +-- http://www.grammatech.com/resource/smt/SMTLIBTutorial.pdf + +module Language.Fixpoint.Smt.Interface ( + + -- * Commands + Command (..) + + -- * Responses + , Response (..) + + -- * Typeclass for SMTLIB2 conversion + , SMTLIB2 (..) + + -- * Creating and killing SMTLIB2 Process + , Context (..) + , makeContext + , makeContextNoLog + , cleanupContext + + -- * Execute Queries + , command + , smtWrite + + -- * Query API + , smtDecl + , smtAssert + , smtCheckUnsat + , smtBracket + , smtDistinct + + -- * Theory Symbols + , theorySymbols + -- smt_set_funs + + ) where + +import Language.Fixpoint.Config (SMTSolver (..)) +import Language.Fixpoint.Errors +import Language.Fixpoint.Files +import Language.Fixpoint.Types +import Language.Fixpoint.Smt.Types +import Language.Fixpoint.Smt.Theories +import Language.Fixpoint.Smt.Serialize + + + +import Control.Applicative ((*>), (<$>), (<*), (<|>)) +import Control.Monad +import Data.Char +import qualified Data.HashMap.Strict as M +import qualified Data.List as L +import Data.Monoid +import qualified Data.Text as T +import Data.Text.Format +import qualified Data.Text.IO as TIO +import qualified Data.Text.Lazy as LT +import qualified Data.Text.Lazy.IO as LTIO +import System.Directory +import System.Exit hiding (die) +import System.FilePath +import System.IO (Handle, IOMode (..), hClose, hFlush, + openFile) +import System.Process +import qualified Data.Attoparsec.Text as A + +{- Usage: +runFile f + = readFile f >>= runString + +runString str + = runCommands $ rr str + +runCommands cmds + = do me <- makeContext Z3 + mapM_ (T.putStrLn . smt2) cmds + zs <- mapM (command me) cmds + return zs +-} + +-------------------------------------------------------------------------- +-- | SMT IO -------------------------------------------------------------- +-------------------------------------------------------------------------- + +-------------------------------------------------------------------------- +command :: Context -> Command -> IO Response +-------------------------------------------------------------------------- +command me !cmd = {-# SCC "command" #-} say me cmd >> hear me cmd + where + say me = smtWrite me . smt2 + hear me CheckSat = smtRead me + hear me (GetValue _) = smtRead me + hear me _ = return Ok + + + +smtWrite :: Context -> LT.Text -> IO () +smtWrite me !s = smtWriteRaw me s + +smtRead :: Context -> IO Response +smtRead me = {-# SCC "smtRead" #-} + do ln <- smtReadRaw me + res <- A.parseWith (smtReadRaw me) responseP ln + case A.eitherResult res of + Left e -> error e + Right r -> do + maybe (return ()) (\h -> hPutStrLnNow h $ format "; SMT Says: {}" (Only $ show r)) (cLog me) + when (verbose me) $ + LTIO.putStrLn $ format "SMT Says: {}" (Only $ show r) + return r + +responseP = {-# SCC "responseP" #-} A.char '(' *> sexpP + <|> A.string "sat" *> return Sat + <|> A.string "unsat" *> return Unsat + <|> A.string "unknown" *> return Unknown + +sexpP = {-# SCC "sexpP" #-} A.string "error" *> (Error <$> errorP) + <|> Values <$> valuesP + +errorP = A.skipSpace *> A.char '"' *> A.takeWhile1 (/='"') <* A.string "\")" + +valuesP = A.many1' pairP <* (A.char ')') + +pairP = {-# SCC "pairP" #-} + do A.skipSpace + A.char '(' + !x <- symbolP + A.skipSpace + !v <- valueP + A.char ')' + return (x,v) + +symbolP = {-# SCC "symbolP" #-} symbol <$> A.takeWhile1 (not . isSpace) + +valueP = {-# SCC "valueP" #-} negativeP + <|> A.takeWhile1 (\c -> not (c == ')' || isSpace c)) + +negativeP + = do v <- A.char '(' *> A.takeWhile1 (/=')') <* A.char ')' + return $ "(" <> v <> ")" + +{-@ pairs :: {v:[a] | (len v) mod 2 = 0} -> [(a,a)] @-} +pairs :: [a] -> [(a,a)] +pairs !xs = case L.splitAt 2 xs of + ([],b) -> [] + ([x,y], zs) -> (x,y) : pairs zs + +smtWriteRaw :: Context -> LT.Text -> IO () +smtWriteRaw me !s = {-# SCC "smtWriteRaw" #-} do + hPutStrLnNow (cOut me) s + maybe (return ()) (`hPutStrLnNow` s) (cLog me) + +smtReadRaw :: Context -> IO Raw +smtReadRaw me = {-# SCC "smtReadRaw" #-} TIO.hGetLine (cIn me) + +hPutStrLnNow h !s = LTIO.hPutStrLn h s >> hFlush h + +-------------------------------------------------------------------------- +-- | SMT Context --------------------------------------------------------- +-------------------------------------------------------------------------- + +-------------------------------------------------------------------------- +makeContext :: SMTSolver -> FilePath -> IO Context +-------------------------------------------------------------------------- +makeContext s f + = do me <- makeProcess s + pre <- smtPreamble s me + createDirectoryIfMissing True $ takeDirectory smtFile + hLog <- openFile smtFile WriteMode + let me' = me { cLog = Just hLog } + mapM_ (smtWrite me') pre + return me' + where + smtFile = extFileName Smt2 f + + +makeContextNoLog s + = do me <- makeProcess s + pre <- smtPreamble s me + mapM_ (smtWrite me) pre + return me + +makeProcess s + = do (hOut, hIn, _ ,pid) <- runInteractiveCommand $ smtCmd s + return $ Ctx pid hIn hOut Nothing False + +-------------------------------------------------------------------------- +cleanupContext :: Context -> IO ExitCode +-------------------------------------------------------------------------- +cleanupContext me@(Ctx {..}) + = do smtWrite me "(exit)" + code <- waitForProcess pId + hClose cIn + hClose cOut + maybe (return ()) hClose cLog + return code + +{- "z3 -smt2 -in" -} +{- "z3 -smtc SOFT_TIMEOUT=1000 -in" -} +{- "z3 -smtc -in MBQI=false" -} + +smtCmd Z3 = "z3 -smt2 -in" +smtCmd Mathsat = "mathsat -input=smt2" +smtCmd Cvc4 = "cvc4 --incremental -L smtlib2" + +-- DON'T REMOVE THIS! z3 changed the names of options between 4.3.1 and 4.3.2... +smtPreamble Z3 me + = do smtWrite me "(get-info :version)" + v:_ <- T.words . (!!1) . T.splitOn "\"" <$> smtReadRaw me + if T.splitOn "." v `versionGreater` ["4", "3", "2"] + then return $ z3_432_options ++ z3Preamble + else return $ z3_options ++ z3Preamble +smtPreamble _ _ + = return smtlibPreamble + +versionGreater (x:xs) (y:ys) + | x > y = True + | x == y = versionGreater xs ys + | x < y = False +versionGreater xs [] = True +versionGreater [] ys = False + +----------------------------------------------------------------------------- +-- | SMT Commands ----------------------------------------------------------- +----------------------------------------------------------------------------- + +smtPush, smtPop :: Context -> IO () +smtPush me = interact' me Push +smtPop me = interact' me Pop + + +smtDecl :: Context -> Symbol -> Sort -> IO () +smtDecl me x t = interact' me (Declare x ins out) + where + (ins, out) = deconSort t + +deconSort :: Sort -> ([Sort], Sort) +deconSort t = case functionSort t of + Just (_, ins, out) -> (ins, out) + Nothing -> ([] , t ) + +smtAssert :: Context -> Pred -> IO () +smtAssert me p = interact' me (Assert Nothing p) + +smtDistinct :: Context -> [Expr] -> IO () +smtDistinct me az = interact' me (Distinct az) + +smtCheckUnsat :: Context -> IO Bool +smtCheckUnsat me = respSat <$> command me CheckSat + +smtBracket :: Context -> IO a -> IO a +smtBracket me a = do smtPush me + r <- a + smtPop me + return r + +respSat Unsat = True +respSat Sat = False +respSat Unknown = False +respSat r = die $ err dummySpan $ "crash: SMTLIB2 respSat = " ++ show r + +interact' me cmd = void $ command me cmd + +-- DON'T REMOVE THIS! z3 changed the names of options between 4.3.1 and 4.3.2... +z3_432_options + = [ "(set-option :auto-config false)" + , "(set-option :model true)" + , "(set-option :model.partial false)" + , "(set-option :smt.mbqi false)" ] + +z3_options + = [ "(set-option :auto-config false)" + , "(set-option :model true)" + , "(set-option :model-partial false)" + , "(set-option :mbqi false)" ] + diff --git a/src/Language/Fixpoint/Smt/Serialize.hs b/src/Language/Fixpoint/Smt/Serialize.hs new file mode 100644 --- /dev/null +++ b/src/Language/Fixpoint/Smt/Serialize.hs @@ -0,0 +1,139 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE OverloadedStrings #-} + +-- | This module contains the code for serializing Haskell values +-- into SMTLIB2 format, that is, the instances for the @SMTLIB2@ +-- typeclass. We split it into a separate module as it depends on +-- Theories (see @smt2App@). + +module Language.Fixpoint.Smt.Serialize where + +import Language.Fixpoint.Types +import Language.Fixpoint.Smt.Types +import Language.Fixpoint.Smt.Theories +import qualified Data.Text as T +import Data.Text.Format +import qualified Data.Text.Lazy as LT + +instance SMTLIB2 Sort where + smt2 FInt = "Int" + smt2 t + | t == boolSort = "Bool" + -- smt2 (FApp t []) | t == intFTyCon = "Int" + -- smt2 (FApp t []) | t == boolFTyCon = "Bool" + smt2 (FApp t [FApp ts _,_]) | t == appFTyCon && fTyconSymbol ts == "Set_Set" = "Set" + -- smt2 (FObj s) = smt2 s + smt2 s@(FFunc _ _) = error $ "smt2 FFunc: " ++ show s + smt2 _ = "Int" + +instance SMTLIB2 Symbol where + smt2 s | Just t <- smt2Theory s -- M.lookup s smt_set_funs + = LT.fromStrict t + smt2 s = LT.fromStrict . encode . symbolText $ s + +-- FIXME: this is probably too slow +encode :: T.Text -> T.Text +encode t = {-# SCC "encode" #-} + foldr (\(x,y) -> T.replace x y) t [("[", "ZM"), ("]", "ZN"), (":", "ZC") + ,("(", "ZL"), (")", "ZR"), (",", "ZT") + ,("|", "zb"), ("#", "zh"), ("\\","zr") + ,("z", "zz"), ("Z", "ZZ"), ("%","zv")] + +instance SMTLIB2 SymConst where + smt2 (SL s) = LT.fromStrict s + +instance SMTLIB2 Constant where + smt2 (I n) = format "{}" (Only n) + smt2 (R d) = format "{}" (Only d) + -- smt2 (L t _) = t + +instance SMTLIB2 LocSymbol where + smt2 = smt2 . val + +instance SMTLIB2 Bop where + smt2 Plus = "+" + smt2 Minus = "-" + smt2 Times = "*" + smt2 Div = "/" + smt2 Mod = "mod" + +instance SMTLIB2 Brel where + smt2 Eq = "=" + smt2 Ueq = "=" + smt2 Gt = ">" + smt2 Ge = ">=" + smt2 Lt = "<" + smt2 Le = "<=" + smt2 _ = error "SMTLIB2 Brel" + +instance SMTLIB2 Expr where + smt2 (ESym z) = smt2 z + smt2 (ECon c) = smt2 c + smt2 (EVar x) = smt2 x + smt2 (ELit x _) = smt2 x + smt2 (EApp f es) = smt2App f 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 (ECst e _) = smt2 e + smt2 e = error $ "TODO: SMTLIB2 Expr: " ++ show e + +smt2App :: LocSymbol -> [Expr] -> LT.Text +smt2App f [] = smt2 f +smt2App f [e] + | val f == setEmp = format "(= {} {})" (emp, smt2 e) + | val f == setSng = format "({} {} {})" (add, emp, smt2 e) +smt2App f es = format "({} {})" (smt2 f, smt2s es) + + +instance SMTLIB2 Pred where + smt2 (PTrue) = "true" + smt2 (PFalse) = "false" + smt2 (PAnd []) = "true" + smt2 (PAnd ps) = format "(and {})" (Only $ smt2s ps) + smt2 (POr []) = "false" + smt2 (POr ps) = format "(or {})" (Only $ smt2s ps) + smt2 (PNot p) = format "(not {})" (Only $ smt2 p) + smt2 (PImp p q) = format "(=> {} {})" (smt2 p, smt2 q) + smt2 (PIff p q) = format "(= {} {})" (smt2 p, smt2 q) + smt2 (PBexp e) = smt2 e + smt2 (PAtom r e1 e2) = mkRel r e1 e2 + smt2 _ = error "smtlib2 Pred" + + +mkRel Ne e1 e2 = mkNe e1 e2 +mkRel Une e1 e2 = mkNe e1 e2 +mkRel r e1 e2 = format "({} {} {})" (smt2 r, smt2 e1, smt2 e2) +mkNe e1 e2 = format "(not (= {} {}))" (smt2 e1, smt2 e2) + +instance SMTLIB2 Command where + smt2 (Declare x ts t) = format "(declare-fun {} ({}) {})" (smt2 x, smt2s ts, smt2 t) + smt2 (Define t) = format "(declare-sort {})" (Only $ smt2 t) + smt2 (Assert Nothing p) = format "(assert {})" (Only $ smt2 p) + smt2 (Assert (Just i) p) = format "(assert (! {} :named p-{}))" (smt2 p, i) + smt2 (Distinct az) = format "(assert (distinct {}))" (Only $ smt2s az) + smt2 (Push) = "(push 1)" + smt2 (Pop) = "(pop 1)" + smt2 (CheckSat) = "(check-sat)" + smt2 (GetValue xs) = LT.unwords $ ["(get-value ("] ++ fmap smt2 xs ++ ["))"] + +smt2s :: SMTLIB2 a => [a] -> LT.Text +smt2s = LT.intercalate " " . fmap smt2 + + +{- +(declare-fun x () Int) +(declare-fun y () Int) +(assert (<= 0 x)) +(assert (< x y)) +(push 1) +(assert (not (<= 0 y))) +(check-sat) +(pop 1) +(push 1) +(assert (<= 0 y)) +(check-sat) +(pop 1) +-} + diff --git a/src/Language/Fixpoint/Smt/Theories.hs b/src/Language/Fixpoint/Smt/Theories.hs new file mode 100644 --- /dev/null +++ b/src/Language/Fixpoint/Smt/Theories.hs @@ -0,0 +1,139 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE UndecidableInstances #-} + +module Language.Fixpoint.Smt.Theories where + +import Language.Fixpoint.Types +import Language.Fixpoint.Smt.Types +import qualified Data.HashMap.Strict as M +-- import qualified Data.List as L +import qualified Data.Text as T +import Data.Text.Format +-- import Data.Monoid + + +--import Language.Fixpoint.Errors +--import Language.Fixpoint.Files +import Control.Applicative ((<$>)) +--import Control.Monad +--import Data.Char +--import qualified Data.Text.IO as TIO +import qualified Data.Text.Lazy as LT +--import qualified Data.Text.Lazy.IO as LTIO +--import System.Directory +--import System.Exit hiding (die) +--import System.FilePath +--import System.IO (Handle, IOMode (..), hClose, hFlush, openFile) +--import System.Process +--import qualified Data.Attoparsec.Text as A + + + +-------------------------------------------------------------------------- +-- | Set Theory ---------------------------------------------------------- +-------------------------------------------------------------------------- + +elt, set, map, bit, sz32, sz64 :: Raw +elt = "Elt" +set = "Set" +map = "Map" +bit = "BitVec" +sz32 = "Size32" +sz64 = "Size64" + +emp, add, cup, cap, mem, dif, sub, com, sel, sto :: Raw +emp = "smt_set_emp" +add = "smt_set_add" +cup = "smt_set_cup" +cap = "smt_set_cap" +mem = "smt_set_mem" +dif = "smt_set_dif" +sub = "smt_set_sub" +com = "smt_set_com" +sel = "smt_map_sel" +sto = "smt_map_sto" + + +setEmp, setCap, setSub, setAdd, setMem, setCom, setCup, setDif, setSng :: Symbol +setEmp = "Set_emp" +setCap = "Set_cap" +setSub = "Set_sub" +setAdd = "Set_add" +setMem = "Set_mem" +setCom = "Set_com" +setCup = "Set_cup" +setDif = "Set_dif" +setSng = "Set_sng" + +z3Preamble :: [LT.Text] +z3Preamble + = [ format "(define-sort {} () Int)" + (Only elt) + , format "(define-sort {} () (Array {} Bool))" + (set, elt) + , format "(define-fun {} () {} ((as const {}) false))" + (emp, set, set) + , format "(define-fun {} ((x {}) (s {})) Bool (select s x))" + (mem, elt, set) + , format "(define-fun {} ((s {}) (x {})) {} (store s x true))" + (add, set, elt, set) + , format "(define-fun {} ((s1 {}) (s2 {})) {} ((_ map or) s1 s2))" + (cup, set, set, set) + , format "(define-fun {} ((s1 {}) (s2 {})) {} ((_ map and) s1 s2))" + (cap, set, set, set) + , format "(define-fun {} ((s {})) {} ((_ map not) s))" + (com, set, set) + , format "(define-fun {} ((s1 {}) (s2 {})) {} ({} s1 ({} s2)))" + (dif, set, set, set, cap, com) + , format "(define-fun {} ((s1 {}) (s2 {})) Bool (= {} ({} s1 s2)))" + (sub, set, set, emp, dif) + ] + +smtlibPreamble :: [LT.Text] +smtlibPreamble + = [ "(set-logic QF_UFLIA)" + , format "(define-sort {} () Int)" (Only elt) + , format "(define-sort {} () Int)" (Only set) + , format "(declare-fun {} () {})" (emp, set) + , format "(declare-fun {} ({} {}) {})" (add, set, elt, set) + , format "(declare-fun {} ({} {}) {})" (cup, set, set, set) + , format "(declare-fun {} ({} {}) {})" (cap, set, set, set) + , format "(declare-fun {} ({} {}) {})" (dif, set, set, set) + , format "(declare-fun {} ({} {}) Bool)" (sub, set, set) + , format "(declare-fun {} ({} {}) Bool)" (mem, elt, set) + ] + +mkSetSort _ _ = set +mkEmptySet _ _ = emp +mkSetAdd _ s x = format "({} {} {})" (add, s, x) +mkSetMem _ x s = format "({} {} {})" (mem, x, s) +mkSetCup _ s t = format "({} {} {})" (cup, s, t) +mkSetCap _ s t = format "({} {} {})" (cap, s, t) +mkSetDif _ s t = format "({} {} {})" (dif, s, t) +mkSetSub _ s t = format "({} {} {})" (sub, s, t) + + +-- smt_set_funs :: M.HashMap Symbol Raw +-- smt_set_funs = M.fromList [ (setEmp, emp), (setAdd, add), (setCup, cup) +-- , (setCap, cap), (setMem, mem), (setDif, dif) +-- , (setSub, sub), (setCom, com)] + +theorySymbols :: M.HashMap Symbol TheorySymbol +theorySymbols = M.fromList + [ tSym setEmp emp undefined + , tSym setAdd add undefined + , tSym setCup cup undefined + , tSym setCap cap undefined + , tSym setMem mem undefined + , tSym setDif dif undefined + , tSym setSub sub undefined + , tSym setCom com undefined + ] + +tSym :: Symbol -> Raw -> Sort -> (Symbol, TheorySymbol) +tSym x n t = (x, Thy x n t) + +smt2Theory :: Symbol -> Maybe T.Text +smt2Theory x = tsRaw <$> M.lookup x theorySymbols diff --git a/src/Language/Fixpoint/Smt/Types.hs b/src/Language/Fixpoint/Smt/Types.hs new file mode 100644 --- /dev/null +++ b/src/Language/Fixpoint/Smt/Types.hs @@ -0,0 +1,102 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE NoMonomorphismRestriction #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE UndecidableInstances #-} + +-- | This module contains the types defining an SMTLIB2 interface. + +module Language.Fixpoint.Smt.Types ( + + -- * Serialized Representation + Raw + + -- * Commands + , Command (..) + + -- * Responses + , Response (..) + + -- * Typeclass for SMTLIB2 conversion + , SMTLIB2 (..) + + -- * SMTLIB2 Process Context + , Context (..) + + -- * Theory Symbol + , TheorySymbol (..) + + ) where + +import Language.Fixpoint.Config (SMTSolver (..)) +import Language.Fixpoint.Errors +import Language.Fixpoint.Files +import Language.Fixpoint.Types + +import Control.Applicative ((*>), (<$>), (<*), (<|>)) +import Control.Monad +import Data.Char +import qualified Data.HashMap.Strict as M +import qualified Data.List as L +import Data.Monoid +import qualified Data.Text as T +import Data.Text.Format +import qualified Data.Text.IO as TIO +import qualified Data.Text.Lazy as LT +import qualified Data.Text.Lazy.IO as LTIO +import System.Directory +import System.Exit hiding (die) +import System.FilePath +import System.IO (Handle, IOMode (..), hClose, hFlush, + openFile) +import System.Process +import qualified Data.Attoparsec.Text as A + +-------------------------------------------------------------------------- +-- | Types --------------------------------------------------------------- +-------------------------------------------------------------------------- + +type Raw = T.Text + +-- | Commands issued to SMT engine +data Command = Push + | Pop + | CheckSat + | Declare Symbol [Sort] Sort + | Define Sort + | Assert (Maybe Int) Pred + | Distinct [Expr] -- {v:[Expr] | 2 <= len v} + | GetValue [Symbol] + deriving (Eq, Show) + +-- | Responses received from SMT engine +data Response = Ok + | Sat + | Unsat + | Unknown + | Values [(Symbol, Raw)] + | Error Raw + deriving (Eq, Show) + +-- | Information about the external SMT process +data Context = Ctx { pId :: ProcessHandle + , cIn :: Handle + , cOut :: Handle + , cLog :: Maybe Handle + , verbose :: Bool + } + +-- | Theory Symbol +data TheorySymbol = Thy { tsSym :: Symbol + , tsRaw :: Raw + , tsSort :: Sort + } + deriving (Eq, Ord, Show) + +----------------------------------------------------------------------- +-- | AST Conversion: Types that can be serialized --------------------- +----------------------------------------------------------------------- + +-- | Types that can be serialized +class SMTLIB2 a where + smt2 :: a -> LT.Text + diff --git a/src/Language/Fixpoint/SmtLib2.hs b/src/Language/Fixpoint/SmtLib2.hs deleted file mode 100644 --- a/src/Language/Fixpoint/SmtLib2.hs +++ /dev/null @@ -1,529 +0,0 @@ -{-# LANGUAGE BangPatterns #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE NoMonomorphismRestriction #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE PatternGuards #-} -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE UndecidableInstances #-} - --- | This module contains an SMTLIB2 interface for --- 1. checking the validity, and, --- 2. computing satisfying assignments --- for formulas. --- By implementing a binary interface over the SMTLIB2 format defined at --- http://www.smt-lib.org/ --- http://www.grammatech.com/resource/smt/SMTLIBTutorial.pdf - -module Language.Fixpoint.SmtLib2 ( - - -- * Commands - Command (..) - - -- * Responses - , Response (..) - - -- * Typeclass for SMTLIB2 conversion - , SMTLIB2 (..) - - -- * Creating and killing SMTLIB2 Process - , Context (..) - , makeContext - , makeContextNoLog - , cleanupContext - - -- * Execute Queries - , command - , smtWrite - - -- * Query API - , smtDecl - , smtAssert - , smtCheckUnsat - , smtBracket - , smtDistinct - - -- * Theory Symbols - , smt_set_funs - - ) where - -import Language.Fixpoint.Config (SMTSolver (..)) -import Language.Fixpoint.Errors -import Language.Fixpoint.Files -import Language.Fixpoint.Types - -import Control.Applicative ((*>), (<$>), (<*), (<|>)) -import Control.Monad -import Data.Char -import qualified Data.HashMap.Strict as M -import qualified Data.List as L -import Data.Monoid -import qualified Data.Text as T -import Data.Text.Format -import qualified Data.Text.IO as TIO -import qualified Data.Text.Lazy as LT -import qualified Data.Text.Lazy.IO as LTIO -import Data.IORef -import System.Directory -import System.Exit hiding (die) -import System.FilePath -import System.IO (Handle, IOMode (..), hClose, hFlush, - openFile) -import System.Process -import Debug.Trace (trace) -import qualified Data.Attoparsec.Text as A - -{- Usage: -runFile f - = readFile f >>= runString - -runString str - = runCommands $ rr str - -runCommands cmds - = do me <- makeContext Z3 - mapM_ (T.putStrLn . smt2) cmds - zs <- mapM (command me) cmds - return zs --} - --------------------------------------------------------------------------- --- | Types --------------------------------------------------------------- --------------------------------------------------------------------------- - -type Raw = T.Text - --- | Commands issued to SMT engine -data Command = Push - | Pop - | CheckSat - | Declare Symbol [Sort] Sort - | Define Sort - | Assert (Maybe Int) Pred - | Distinct [Expr] -- {v:[Expr] | 2 <= len v} - | GetValue [Symbol] - deriving (Eq, Show) - --- | Responses received from SMT engine -data Response = Ok - | Sat - | Unsat - | Unknown - | Values [(Symbol, Raw)] - | Error Raw - deriving (Eq, Show) - --- | Information about the external SMT process -data Context = Ctx { pId :: ProcessHandle - , cIn :: Handle - , cOut :: Handle - , cLog :: Maybe Handle - , verbose :: Bool - } - --------------------------------------------------------------------------- --- | SMT IO -------------------------------------------------------------- --------------------------------------------------------------------------- - --------------------------------------------------------------------------- --- commands :: Context -> [Command] -> IO [Response] --- ----------------------------------------------------------------------- --- commands = mapM . command - --------------------------------------------------------------------------- -command :: Context -> Command -> IO Response --------------------------------------------------------------------------- -command me !cmd = {-# SCC "command" #-} say me cmd >> hear me cmd - where - say me = smtWrite me . smt2 - hear me CheckSat = smtRead me - hear me (GetValue _) = smtRead me - hear me _ = return Ok - - - -smtWrite :: Context -> LT.Text -> IO () -smtWrite me !s = smtWriteRaw me s - -smtRead :: Context -> IO Response -smtRead me = {-# SCC "smtRead" #-} - do ln <- smtReadRaw me - res <- A.parseWith (smtReadRaw me) responseP ln - case A.eitherResult res of - Left e -> error e - Right r -> do - maybe (return ()) (\h -> hPutStrLnNow h $ format "; SMT Says: {}" (Only $ show r)) (cLog me) - when (verbose me) $ - LTIO.putStrLn $ format "SMT Says: {}" (Only $ show r) - return r - -responseP = {-# SCC "responseP" #-} A.char '(' *> sexpP - <|> A.string "sat" *> return Sat - <|> A.string "unsat" *> return Unsat - <|> A.string "unknown" *> return Unknown - -sexpP = {-# SCC "sexpP" #-} A.string "error" *> (Error <$> errorP) - <|> Values <$> valuesP - -errorP = A.skipSpace *> A.char '"' *> A.takeWhile1 (/='"') <* A.string "\")" - -valuesP = A.many1' pairP <* (A.char ')') - -pairP = {-# SCC "pairP" #-} - do A.skipSpace - A.char '(' - !x <- symbolP - A.skipSpace - !v <- valueP - A.char ')' - return (x,v) - -symbolP = {-# SCC "symbolP" #-} symbol <$> A.takeWhile1 (not . isSpace) - -valueP = {-# SCC "valueP" #-} negativeP - <|> A.takeWhile1 (\c -> not (c == ')' || isSpace c)) - -negativeP - = do v <- A.char '(' *> A.takeWhile1 (/=')') <* A.char ')' - return $ "(" <> v <> ")" - -{-@ pairs :: {v:[a] | (len v) mod 2 = 0} -> [(a,a)] @-} -pairs :: [a] -> [(a,a)] -pairs !xs = case L.splitAt 2 xs of - ([],b) -> [] - ((x:y:[]),zs) -> (x,y) : pairs zs - -smtWriteRaw :: Context -> LT.Text -> IO () -smtWriteRaw me !s = {-# SCC "smtWriteRaw" #-} do - hPutStrLnNow (cOut me) s - maybe (return ()) (\h -> hPutStrLnNow h s) (cLog me) - -smtReadRaw :: Context -> IO Raw -smtReadRaw me = {-# SCC "smtReadRaw" #-} TIO.hGetLine (cIn me) - -hPutStrLnNow h !s = LTIO.hPutStrLn h s >> hFlush h - --------------------------------------------------------------------------- --- | SMT Context --------------------------------------------------------- --------------------------------------------------------------------------- - --------------------------------------------------------------------------- -makeContext :: SMTSolver -> FilePath -> IO Context --------------------------------------------------------------------------- -makeContext s f - = do me <- makeProcess s - pre <- smtPreamble s me - createDirectoryIfMissing True $ takeDirectory smtFile - hLog <- openFile smtFile WriteMode - let me' = me { cLog = Just hLog } - mapM_ (smtWrite me') pre - return me' - where - smtFile = extFileName Smt2 f - - -makeContextNoLog s - = do me <- makeProcess s - pre <- smtPreamble s me - mapM_ (smtWrite me) pre - return me - -makeProcess s - = do (hOut, hIn, _ ,pid) <- runInteractiveCommand $ smtCmd s - return $ Ctx pid hIn hOut Nothing False - --------------------------------------------------------------------------- -cleanupContext :: Context -> IO ExitCode --------------------------------------------------------------------------- -cleanupContext me@(Ctx {..}) - = do smtWrite me "(exit)" - code <- waitForProcess pId - hClose cIn - hClose cOut - maybe (return ()) hClose cLog - return code - -{- "z3 -smt2 -in" -} -{- "z3 -smtc SOFT_TIMEOUT=1000 -in" -} -{- "z3 -smtc -in MBQI=false" -} - -smtCmd Z3 = "z3 -smt2 -in" -smtCmd Mathsat = "mathsat -input=smt2" -smtCmd Cvc4 = "cvc4 --incremental -L smtlib2" - --- DON'T REMOVE THIS! z3 changed the names of options between 4.3.1 and 4.3.2... -smtPreamble Z3 me - = do smtWrite me "(get-info :version)" - r <- (!!1) . T.splitOn "\"" <$> smtReadRaw me - case T.words r of - "4.3.2" : _ -> return $ z3_432_options ++ z3Preamble - _ -> return $ z3_options ++ z3Preamble -smtPreamble _ _ - = return smtlibPreamble - ------------------------------------------------------------------------------ --- | SMT Commands ----------------------------------------------------------- ------------------------------------------------------------------------------ - -smtPush, smtPop :: Context -> IO () -smtPush me = interact' me Push -smtPop me = interact' me Pop - - -smtDecl :: Context -> Symbol -> Sort -> IO () -smtDecl me x t = interact' me (Declare x ins out) - where - (ins, out) = deconSort t - -deconSort :: Sort -> ([Sort], Sort) -deconSort t = case functionSort t of - Just (_, ins, out) -> (ins, out) - Nothing -> ([] , t ) - -smtAssert :: Context -> Pred -> IO () -smtAssert me p = interact' me (Assert Nothing p) - -smtDistinct :: Context -> [Expr] -> IO () -smtDistinct me az = interact' me (Distinct az) - -smtCheckUnsat :: Context -> IO Bool -smtCheckUnsat me = respSat <$> command me CheckSat - -smtBracket :: Context -> IO a -> IO a -smtBracket me a = do smtPush me - r <- a - smtPop me - return r - -respSat Unsat = True -respSat Sat = False -respSat Unknown = False -respSat r = die $ err dummySpan $ "crash: SMTLIB2 respSat = " ++ show r - -interact' me cmd = command me cmd >> return () - - --------------------------------------------------------------------------- --- | Set Theory ---------------------------------------------------------- --------------------------------------------------------------------------- - -elt, set :: Raw -elt = "Elt" -set = "Set" -map = "Map" -bit = "BitVec" -sz32 = "Size32" -sz64 = "Size64" - - -emp, add, cup, cap, mem, dif, sub, com :: Raw -emp = "smt_set_emp" -add = "smt_set_add" -cup = "smt_set_cup" -cap = "smt_set_cap" -mem = "smt_set_mem" -dif = "smt_set_dif" -sub = "smt_set_sub" -com = "smt_set_com" -sel = "smt_map_sel" -sto = "smt_map_sto" - -setEmp = "Set_emp" :: Symbol -setCap = "Set_cap" :: Symbol -setSub = "Set_sub" :: Symbol -setAdd = "Set_add" :: Symbol -setMem = "Set_mem" :: Symbol -setCom = "Set_com" :: Symbol -setCup = "Set_cup" :: Symbol -setDif = "Set_dif" :: Symbol -setSng = "Set_sng" :: Symbol - -smt_set_funs :: M.HashMap Symbol Raw -smt_set_funs = M.fromList [ (setEmp, emp), (setAdd, add), (setCup, cup) - , (setCap, cap), (setMem, mem), (setDif, dif) - , (setSub, sub), (setCom, com)] - --- DON'T REMOVE THIS! z3 changed the names of options between 4.3.1 and 4.3.2... -z3_432_options - = [ "(set-option :auto-config false)" - , "(set-option :model true)" - , "(set-option :model.partial false)" - , "(set-option :smt.mbqi false)" ] -z3_options - = [ "(set-option :auto-config false)" - , "(set-option :model true)" - , "(set-option :model-partial false)" - , "(set-option :mbqi false)" ] - -z3Preamble - = [ format "(define-sort {} () Int)" - (Only elt) - , format "(define-sort {} () (Array {} Bool))" - (set, elt) - , format "(define-fun {} () {} ((as const {}) false))" - (emp, set, set) - , format "(define-fun {} ((x {}) (s {})) Bool (select s x))" - (mem, elt, set) - , format "(define-fun {} ((s {}) (x {})) {} (store s x true))" - (add, set, elt, set) - , format "(define-fun {} ((s1 {}) (s2 {})) {} ((_ map or) s1 s2))" - (cup, set, set, set) - , format "(define-fun {} ((s1 {}) (s2 {})) {} ((_ map and) s1 s2))" - (cap, set, set, set) - , format "(define-fun {} ((s {})) {} ((_ map not) s))" - (com, set, set) - , format "(define-fun {} ((s1 {}) (s2 {})) {} ({} s1 ({} s2)))" - (dif, set, set, set, cap, com) - , format "(define-fun {} ((s1 {}) (s2 {})) Bool (= {} ({} s1 s2)))" - (sub, set, set, emp, dif) - ] - - -smtlibPreamble - = [ "(set-logic QF_UFLIA)" - , format "(define-sort {} () Int)" (Only elt) - , format "(define-sort {} () Int)" (Only set) - , format "(declare-fun {} () {})" (emp, set) - , format "(declare-fun {} ({} {}) {})" (add, set, elt, set) - , format "(declare-fun {} ({} {}) {})" (cup, set, set, set) - , format "(declare-fun {} ({} {}) {})" (cap, set, set, set) - , format "(declare-fun {} ({} {}) {})" (dif, set, set, set) - , format "(declare-fun {} ({} {}) Bool)" (sub, set, set) - , format "(declare-fun {} ({} {}) Bool)" (mem, elt, set) - ] - -mkSetSort _ _ = set -mkEmptySet _ _ = emp -mkSetAdd _ s x = format "({} {} {})" (add, s, x) -mkSetMem _ x s = format "({} {} {})" (mem, x, s) -mkSetCup _ s t = format "({} {} {})" (cup, s, t) -mkSetCap _ s t = format "({} {} {})" (cap, s, t) -mkSetDif _ s t = format "({} {} {})" (dif, s, t) -mkSetSub _ s t = format "({} {} {})" (sub, s, t) - ------------------------------------------------------------------------ --- | AST Conversion --------------------------------------------------- ------------------------------------------------------------------------ - --- | Types that can be serialized -class SMTLIB2 a where - smt2 :: a -> LT.Text - -instance SMTLIB2 Sort where - smt2 FInt = "Int" - smt2 (FApp t []) | t == intFTyCon = "Int" - smt2 (FApp t []) | t == boolFTyCon = "Bool" - smt2 (FApp t [FApp ts _,_]) | t == appFTyCon && fTyconSymbol ts == "Set_Set" = "Set" - -- smt2 (FObj s) = smt2 s - smt2 s@(FFunc _ _) = error $ "smt2 FFunc: " ++ show s - smt2 _ = "Int" - -instance SMTLIB2 Symbol where - smt2 s | Just t <- M.lookup s smt_set_funs - = LT.fromStrict t - smt2 s = LT.fromStrict . encode . symbolText $ s - --- FIXME: this is probably too slow -encode :: T.Text -> T.Text -encode t = {-# SCC "encode" #-} - foldr (\(x,y) t -> T.replace x y t) t [("[", "ZM"), ("]", "ZN"), (":", "ZC") - ,("(", "ZL"), (")", "ZR"), (",", "ZT") - ,("|", "zb"), ("#", "zh"), ("\\","zr") - ,("z", "zz"), ("Z", "ZZ"), ("%","zv")] - -instance SMTLIB2 SymConst where - smt2 (SL s) = LT.fromStrict s - -instance SMTLIB2 Constant where - smt2 (I n) = format "{}" (Only n) - -instance SMTLIB2 LocSymbol where - smt2 = smt2 . val - -instance SMTLIB2 Bop where - smt2 Plus = "+" - smt2 Minus = "-" - smt2 Times = "*" - smt2 Div = "/" - smt2 Mod = "mod" - -instance SMTLIB2 Brel where - smt2 Eq = "=" - smt2 Ueq = "=" - smt2 Gt = ">" - smt2 Ge = ">=" - smt2 Lt = "<" - smt2 Le = "<=" - smt2 _ = error "SMTLIB2 Brel" - -instance SMTLIB2 Expr where - smt2 (ESym z) = smt2 z - smt2 (ECon c) = smt2 c - smt2 (EVar x) = smt2 x - smt2 (ELit x _) = smt2 x - smt2 (EApp f es) = smt2App f 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 (ECst e _) = smt2 e - smt2 e = error $ "TODO: SMTLIB2 Expr: " ++ show e - -smt2App :: LocSymbol -> [Expr] -> LT.Text -smt2App f [] = smt2 f -smt2App f [e] - | val f == setEmp = format "(= {} {})" (emp, smt2 e) - | val f == setSng = format "({} {} {})" (add, emp, smt2 e) -smt2App f es = format "({} {})" (smt2 f, smt2s es) - - -instance SMTLIB2 Pred where - smt2 (PTrue) = "true" - smt2 (PFalse) = "false" - smt2 (PAnd []) = "true" - smt2 (PAnd ps) = format "(and {})" (Only $ smt2s ps) - smt2 (POr []) = "false" - smt2 (POr ps) = format "(or {})" (Only $ smt2s ps) - smt2 (PNot p) = format "(not {})" (Only $ smt2 p) - smt2 (PImp p q) = format "(=> {} {})" (smt2 p, smt2 q) - smt2 (PIff p q) = format "(= {} {})" (smt2 p, smt2 q) - smt2 (PBexp e) = smt2 e - smt2 (PAtom r e1 e2) = mkRel r e1 e2 - smt2 _ = error "smtlib2 Pred" - - -mkRel Ne e1 e2 = mkNe e1 e2 -mkRel Une e1 e2 = mkNe e1 e2 -mkRel r e1 e2 = format "({} {} {})" (smt2 r, smt2 e1, smt2 e2) -mkNe e1 e2 = format "(not (= {} {}))" (smt2 e1, smt2 e2) - -instance SMTLIB2 Command where - smt2 (Declare x ts t) = format "(declare-fun {} ({}) {})" (smt2 x, smt2s ts, smt2 t) - smt2 (Define t) = format "(declare-sort {})" (Only $ smt2 t) - smt2 (Assert Nothing p) = format "(assert {})" (Only $ smt2 p) - smt2 (Assert (Just i) p) = format "(assert (! {} :named p-{}))" (smt2 p, i) - smt2 (Distinct az) = format "(assert (distinct {}))" (Only $ smt2s az) - smt2 (Push) = "(push 1)" - smt2 (Pop) = "(pop 1)" - smt2 (CheckSat) = "(check-sat)" - smt2 (GetValue xs) = LT.unwords $ ["(get-value ("] ++ fmap smt2 xs ++ ["))"] - - -smt2s = LT.intercalate " " . fmap smt2 - -{- -(declare-fun x () Int) -(declare-fun y () Int) -(assert (<= 0 x)) -(assert (< x y)) -(push 1) -(assert (not (<= 0 y))) -(check-sat) -(pop 1) -(push 1) -(assert (<= 0 y)) -(check-sat) -(pop 1) --} - -------------------------------------------------------------------- - diff --git a/src/Language/Fixpoint/Solver/Deps.hs b/src/Language/Fixpoint/Solver/Deps.hs --- a/src/Language/Fixpoint/Solver/Deps.hs +++ b/src/Language/Fixpoint/Solver/Deps.hs @@ -58,16 +58,16 @@ graph = [(k,k,ks) | (k, ks) <- groupList edges] sccs = G.stronglyConnCompR graph -sccsToDeps :: [G.SCC (F.KVar, F.KVar,[F.KVar])] -> F.Kuts -> Deps +sccsToDeps :: [G.SCC (F.KVar, F.KVar, [F.KVar])] -> F.Kuts -> Deps sccsToDeps xs ks = execState (mapM_ (bar ks) xs) (Deps [] []) - -bar :: F.Kuts -> G.SCC (F.KVar, F.KVar,[F.KVar]) -> State Deps () -bar _ (G.AcyclicSCC (v,_,_)) = do ds <- get - put ds {depNonCuts = v : depNonCuts ds} -bar ks (G.CyclicSCC vs) = do let (v,vs') = chooseCut vs ks - ds <- get - put ds {depCuts = v : depCuts ds} - mapM_ (bar ks) (G.stronglyConnCompR vs') + where + bar :: F.Kuts -> G.SCC (F.KVar, F.KVar,[F.KVar]) -> State Deps () + bar _ (G.AcyclicSCC (v,_,_)) = do ds <- get + put ds {depNonCuts = v : depNonCuts ds} + bar ks (G.CyclicSCC vs) = do let (v,vs') = chooseCut vs ks + ds <- get + put ds {depCuts = v : depCuts ds} + mapM_ (bar ks) (G.stronglyConnCompR vs') chooseCut :: [(F.KVar, F.KVar, [F.KVar])] -> F.Kuts -> (F.KVar, [(F.KVar, F.KVar,[F.KVar])]) chooseCut vs (F.KS ks) = (v, [x | x@(u,_,_) <- vs, u /= v]) diff --git a/src/Language/Fixpoint/Solver/Eliminate.hs b/src/Language/Fixpoint/Solver/Eliminate.hs --- a/src/Language/Fixpoint/Solver/Eliminate.hs +++ b/src/Language/Fixpoint/Solver/Eliminate.hs @@ -1,10 +1,12 @@ +{-# LANGUAGE PatternGuards #-} {-# LANGUAGE FlexibleContexts #-} + module Language.Fixpoint.Solver.Eliminate - (eliminateAll) where + (eliminateAll, elimKVar, findWfC) where import Language.Fixpoint.Types import qualified Language.Fixpoint.Solver.Deps as D -import Language.Fixpoint.Visitor (kvars, mapKVars) +import Language.Fixpoint.Visitor (kvars, mapKVars') import Language.Fixpoint.Names (existSymbol) import Language.Fixpoint.Misc (errorstar) @@ -16,53 +18,48 @@ -------------------------------------------------------------- eliminateAll :: FInfo a -> FInfo a -eliminateAll fi = evalState (foldlM eliminate fi (D.depNonCuts ds)) 0 +eliminateAll fi = evalState (foldlM eliminate fi nonCuts) 0 where - ds = D.deps fi + nonCuts = D.depNonCuts $ D.deps fi -------------------------------------------------------------- class Elimable a where - elimKVar :: KVar -> Pred -> a -> a + elimKVar :: ((KVar, Subst) -> Maybe Pred) -> a -> a instance Elimable (SubC a) where - -- we don't bother editing srhs since if kv is on the rhs then the entire constraint should get eliminated - elimKVar kv pr x = x { slhs = elimKVar kv pr (slhs x) } + elimKVar f x = x { slhs = elimKVar f (slhs x) + , srhs = elimKVar f (srhs x) + } instance Elimable SortedReft where - elimKVar kv pr x = x { sr_reft = elimKVar kv pr (sr_reft x) } - -instance Elimable Reft where - elimKVar kv pr = mapKVars go - where - go k = if kv == k then Just pr else Nothing + elimKVar f x = x { sr_reft = mapKVars' f (sr_reft x) } instance Elimable (FInfo a) where - elimKVar kv pr x = x { cm = M.map (elimKVar kv pr) (cm x) - , bs = elimKVar kv pr (bs x) - } + elimKVar f x = x { cm = M.map (elimKVar f) (cm x) + , bs = elimKVar f (bs x) + } instance Elimable BindEnv where - elimKVar kv pr = mapBindEnv (\(sym, sr) -> (sym, elimKVar kv pr sr)) + elimKVar f = mapBindEnv (\(sym, sr) -> (sym, elimKVar f sr)) eliminate :: FInfo a -> KVar -> State Integer (FInfo a) -eliminate fInfo kv = do - n <- get - let relevantSubCs = M.filter ( elem kv . D.rhsKVars) (cm fInfo) - let remainingSubCs = M.filter (notElem kv . D.rhsKVars) (cm fInfo) - let (kvWfC, remainingWs) = findWfC kv (ws fInfo) - let (bindingsList, (n', orPred)) = runState (mapM (extractPred kvWfC (bs fInfo)) (M.elems relevantSubCs)) (n, POr []) - let bindings = concat bindingsList - - let be = bs fInfo - let (ids, be') = insertsBindEnv [(sym, trueSortedReft srt) | (sym, srt) <- bindings] be +eliminate fi kv = do + let relevantSubCs = M.filter ( elem kv . D.rhsKVars) (cm fi) + let remainingSubCs = M.filter (notElem kv . D.rhsKVars) (cm fi) + let (kvWfC, remainingWs) = findWfC kv (ws fi) + foo <- mapM (extractPred kvWfC (bs fi)) (M.elems relevantSubCs) + let orPred = POr $ map fst foo + let symSrtList = concatMap snd foo + let symSReftList = [(sym, trueSortedReft srt) | (sym, srt) <- symSrtList] + let (ids, be) = insertsBindEnv symSReftList $ bs fi let newSubCs = M.map (\s -> s { senv = insertsIBindEnv ids (senv s)}) remainingSubCs - put n' - return $ elimKVar kv orPred (fInfo { cm = newSubCs , ws = remainingWs , bs = be' }) + let go (k, _) = if kv == k then Just orPred else Nothing + return $ elimKVar go (fi { cm = newSubCs , ws = remainingWs , bs = be }) insertsBindEnv :: [(Symbol, SortedReft)] -> BindEnv -> ([BindId], BindEnv) -insertsBindEnv bs = runState (mapM go bs) +insertsBindEnv = runState . mapM go where go (sym, srft) = do be <- get let (id, be') = insertBindEnv sym srft be @@ -76,51 +73,41 @@ w' | [x] <- w = x | otherwise = errorstar $ (show kv) ++ " needs exactly one wf constraint" -extractPred :: WfC a -> BindEnv -> SubC a -> State (Integer, Pred) [(Symbol, Sort)] -extractPred wfc be subC = do (n, (POr preds)) <- get - let (bs, (n', pr')) = runState (mapM renameVar vars) (n, PAnd $ pr : [(blah (kVarVV, slhs subC))] ++ suPreds') - put (n', POr $ pr' : preds) - return bs +extractPred :: WfC a -> BindEnv -> SubC a -> State Integer (Pred, [(Symbol, Sort)]) +extractPred wfc be subC = do foo <- mapM renameVar vars + let (bs, subs) = unzip foo + return (subst (mkSubst subs) finalPred, bs) where wfcIBinds = elemsIBindEnv $ wenv wfc subcIBinds = elemsIBindEnv $ senv subC - unmatchedIBinds | wfcIBinds `subset` subcIBinds = subcIBinds \\ wfcIBinds - | otherwise = errorstar $ "kVar is not well formed (missing bindings)" ++ "kVar: " ++ (showFix wfc) ++ "constraint: " ++ (showFix subC) + unmatchedIBinds = subcIBinds \\ wfcIBinds unmatchedIBindEnv = insertsIBindEnv unmatchedIBinds emptyIBindEnv unmatchedBindings = envCs be unmatchedIBindEnv - - kvSreft = wrft wfc - kVarVV = reftBind $ sr_reft kvSreft + lhs = slhs subC + (vars, prList) = baz $ (reftBind $ sr_reft lhs, lhs) : unmatchedBindings - (vars, pr) = baz unmatchedBindings + suPreds = substPreds (domain be wfc) $ reftPred $ sr_reft $ srhs subC + finalPred = PAnd $ prList ++ suPreds - reft = sr_reft $ srhs subC - suPreds = substPreds $ reftPred reft - sub = ((reftBind reft), (eVar kVarVV)) - suPreds' = [subst1 p sub | p <- suPreds] +-- on rhs, $k0[v:=e1][x:=e2] -> [v = e1, x = e2] +substPreds :: [Symbol] -> Pred -> [Pred] +substPreds dom (PKVar _ (Su subs)) = [PAtom Eq (eVar sym) expr | (sym, expr) <- subs , sym `elem` dom] --- on rhs, k0[v:=z] -> [v = z] -substPreds :: Pred -> [Pred] -substPreds (PKVar _ (Su subs)) = map (\(sym, expr) -> PAtom Eq (eVar sym) expr) subs +domain :: BindEnv -> WfC a -> [Symbol] +domain be wfc = (reftBind $ sr_reft $ wrft wfc) : (map fst $ envCs be $ wenv wfc) -renameVar :: (Symbol, Sort) -> State (Integer, Pred) (Symbol, Sort) -renameVar (sym, srt) = do (n, pr) <- get +renameVar :: (Symbol, Sort) -> State Integer ((Symbol, Sort), (Symbol, Expr)) +renameVar (sym, srt) = do n <- get let sym' = existSymbol sym n - put ((n+1), subst1 pr (sym, eVar sym')) - return (sym', srt) - -subset :: (Eq a) => [a] -> [a] -> Bool -subset xs ys = (xs \\ ys) == [] + put (n+1) + return ((sym', srt), (sym, eVar sym')) --- [ x:{v:int|v=10} , y:{v:int|v=20} ] -> [x:int, y:int], (x=10) /\ (y=20) -baz :: [(Symbol, SortedReft)] -> ([(Symbol,Sort)],Pred) -baz bindings = (bs, PAnd $ map blah bindings) - where - bs = map (\(sym, sreft) -> (sym, sr_sort sreft)) bindings +-- [ x:{v:int|v=10} , y:{v:int|v=20} ] -> [x:int, y:int], [(x=10), (y=20)] +baz :: [(Symbol, SortedReft)] -> ([(Symbol,Sort)],[Pred]) +baz = unzip . map blah --- [ x:{v:int|v=10} ] -> (x=10) -blah :: (Symbol, SortedReft) -> Pred -blah (sym, sr) = subst1 (reftPred reft) sub +blah :: (Symbol, SortedReft) -> ((Symbol,Sort), Pred) +blah (sym, sr) = ((sym, sr_sort sr), subst1 (reftPred reft) sub) where reft = sr_reft sr sub = ((reftBind reft), (eVar sym)) diff --git a/src/Language/Fixpoint/Solver/Monad.hs b/src/Language/Fixpoint/Solver/Monad.hs --- a/src/Language/Fixpoint/Solver/Monad.hs +++ b/src/Language/Fixpoint/Solver/Monad.hs @@ -22,10 +22,11 @@ import Language.Fixpoint.Config (Config, inFile, solver) import qualified Language.Fixpoint.Types as F import qualified Language.Fixpoint.Errors as E -import Language.Fixpoint.SmtLib2 +import Language.Fixpoint.Smt.Interface import Language.Fixpoint.Solver.Validate import Language.Fixpoint.Solver.Solution import Data.Maybe (catMaybes) +import qualified Data.HashMap.Strict as M import Control.Applicative ((<$>)) import Control.Monad.State.Strict @@ -99,5 +100,12 @@ declare :: F.FInfo a -> SolveM () --------------------------------------------------------------------------- declare fi = withContext $ \me -> do - xts <- either E.die return $ symbolSorts fi + xts <- either E.die return $ declSymbols fi forM_ xts $ uncurry $ smtDecl me + +declSymbols :: F.FInfo a -> Either E.Error [(F.Symbol, F.Sort)] +declSymbols = fmap dropThy . symbolSorts + where + dropThy = filter (not . isThy . fst) + isThy = (`M.member` theorySymbols) + diff --git a/src/Language/Fixpoint/Solver/Solution.hs b/src/Language/Fixpoint/Solver/Solution.hs --- a/src/Language/Fixpoint/Solver/Solution.hs +++ b/src/Language/Fixpoint/Solver/Solution.hs @@ -58,7 +58,7 @@ instance PPrint EQual where pprint = pprint . eqPred -{-@ EQL :: q:_ -> p:_ -> ListX F.Expr {q_params q} -> _ @-} +{- EQL :: q:_ -> p:_ -> ListX F.Expr {q_params q} -> _ @-} eQual :: F.Qualifier -> [F.Symbol] -> EQual eQual q xs = EQL q p es @@ -176,7 +176,7 @@ wfKvar w@(F.WfC {F.wrft = sr}) | F.Reft (v, F.Refa (F.PKVar k su)) <- F.sr_reft sr , F.isEmptySubst su = (v, F.sr_sort sr, k) - | otherwise = errorstar $ "wfKvar: malformed wfC " ++ show w + | otherwise = errorstar $ "wfKvar: malformed wfC " ++ show (F.wid w) ----------------------------------------------------------------------- okInst :: F.SEnv F.SortedReft -> F.Symbol -> F.Sort -> EQual -> Bool diff --git a/src/Language/Fixpoint/Solver/Solve.hs b/src/Language/Fixpoint/Solver/Solve.hs --- a/src/Language/Fixpoint/Solver/Solve.hs +++ b/src/Language/Fixpoint/Solver/Solve.hs @@ -10,14 +10,16 @@ import qualified Data.HashMap.Strict as M import qualified Language.Fixpoint.Types as F import Language.Fixpoint.Config -import Language.Fixpoint.PrettyPrint import Language.Fixpoint.Solver.Validate import qualified Language.Fixpoint.Solver.Solution as S import qualified Language.Fixpoint.Solver.Worklist as W import Language.Fixpoint.Solver.Monad -import qualified Data.List as L -import Debug.Trace (trace) -import Text.Printf (printf) + +-- DEBUG +import Text.Printf +import Language.Fixpoint.PrettyPrint +import Debug.Trace + --------------------------------------------------------------------------- solve :: Config -> F.FInfo a -> IO (F.Result a) --------------------------------------------------------------------------- @@ -30,8 +32,8 @@ --------------------------------------------------------------------------- solve_ cfg fi = refine s0 wkl >>= result fi where - s0 = S.init cfg fi - wkl = W.init cfg fi + s0 = trace "DONE: S.init" $ S.init cfg fi + wkl = trace "DONE: W.init" $ W.init cfg fi --------------------------------------------------------------------------- refine :: S.Solution -> W.Worklist a -> SolveM S.Solution @@ -40,13 +42,13 @@ | Just (c, w') <- W.pop w = do i <- tickIter (b, s') <- refineC i s c let w'' = if b then W.push c w' else w' - refine s' w'' - -- $ trace (refineMsg i c b w'') w'' + refine s' $ trace (refineMsg i c b w'') + $ w'' | otherwise = return s -- DEBUG --- refineMsg i c b w = printf "REFINE: iter = %d cid = %s change = %s wkl = %s" --- i (show $ F.sid c) (show b) (showpp w) +refineMsg i c b w = printf "REFINE: iter = %d cid = %s change = %s wkl = %s" + i (show $ F.sid c) (show b) (showpp w) --------------------------------------------------------------------------- -- | Single Step Refinement ----------------------------------------------- @@ -87,9 +89,10 @@ --------------------------------------------------------------------------- result :: F.FInfo a -> S.Solution -> SolveM (F.Result a) --------------------------------------------------------------------------- -result fi s = (, sol) <$> result_ fi s - where - sol = M.map (F.pAnd . fmap S.eqPred) s +result fi s = do + let sol = M.map (F.pAnd . fmap S.eqPred) s + stat <- result_ fi s + return $ F.Result stat sol result_ :: F.FInfo a -> S.Solution -> SolveM (F.FixResult (F.SubC a)) result_ fi s = res <$> filterM (isUnsat s) cs @@ -111,4 +114,3 @@ rhsPred :: S.Solution -> F.SubC a -> F.Pred rhsPred s c = S.apply s $ F.rhsCs c - diff --git a/src/Language/Fixpoint/Solver/Uniqify.hs b/src/Language/Fixpoint/Solver/Uniqify.hs new file mode 100644 --- /dev/null +++ b/src/Language/Fixpoint/Solver/Uniqify.hs @@ -0,0 +1,117 @@ + +module Language.Fixpoint.Solver.Uniqify + (renameAll) where + +import Language.Fixpoint.Types +import Language.Fixpoint.Names (renameSymbol) +import Language.Fixpoint.Misc (errorstar) +import Language.Fixpoint.Solver.Eliminate (elimKVar, findWfC) + +import qualified Data.HashMap.Strict as M +import qualified Data.HashSet as S +import Data.List ((\\), sort) +import Data.Maybe (catMaybes) +import Data.Foldable (foldlM) +import Control.Monad.State (get, put, evalState, State) + + + + +-------------------------------------------------------------- +renameAll :: FInfo a -> FInfo a +renameAll fi = fi' + where + idMap = mkIdMap fi + fi' = renameVars fi (M.toList idMap) +-------------------------------------------------------------- + + +type IdMap = M.HashMap BindId (S.HashSet BindId, S.HashSet Integer) +type NameMap = M.HashMap Symbol BindId + +mkIdMap :: FInfo a -> IdMap +mkIdMap fi = M.foldlWithKey' (updateIdMap benv) (emptyIdMap benv) (cm fi) + where benv = bs fi + +emptyIdMap :: BindEnv -> IdMap +emptyIdMap benv = foldl go M.empty (M.keys $ beBinds benv) + where go m b = M.insert b (S.empty, S.empty) m + +updateIdMap :: BindEnv -> IdMap -> Integer -> SubC a -> IdMap +updateIdMap benv m subcId s = foldl (bar' subcId) m' refList + where + ids = sort $ elemsIBindEnv $ senv s + nameMap = mkNameMap benv ids + m' = foldl (bongo benv nameMap) m ids + + symList = (freeVars $ sr_reft $ slhs s) ++ (freeVars $ sr_reft $ srhs s) + refList = baz nameMap symList + +bongo :: BindEnv -> NameMap -> IdMap -> BindId -> IdMap +bongo benv nameMap idMap id = foldl (bar id) idMap refList + where + (_, sr) = lookupBindEnv id benv + symList = freeVars $ sr_reft sr + refList = baz nameMap symList + +bar :: BindId -> IdMap -> BindId -> IdMap +bar idOfReft m referencedId = M.insert referencedId (S.insert idOfReft bs, is) m + where (bs, is) = M.lookupDefault (errorstar "wat") referencedId m + +bar' :: Integer -> IdMap -> BindId -> IdMap +bar' idOfSubc m referencedId = M.insert referencedId (bs, S.insert idOfSubc is) m + where (bs, is) = M.lookupDefault (errorstar "wat") referencedId m + +baz :: NameMap -> [Symbol] -> [BindId] +baz m syms = catMaybes [M.lookup sym m | sym <- syms] --TODO why any Nothings? + +freeVars :: Reft -> [Symbol] +freeVars reft@(Reft (v, _)) = syms reft \\ [v] + +mkNameMap :: BindEnv -> [BindId] -> NameMap +mkNameMap benv ids = foldl (insertInverse benv) M.empty ids + +insertInverse :: BindEnv -> NameMap -> BindId -> NameMap +insertInverse benv m id = M.insert sym id m + where (sym, _) = lookupBindEnv id benv + + +renameVars :: FInfo a -> [(BindId, (S.HashSet BindId, S.HashSet Integer))] -> FInfo a +renameVars fi xs = evalState (foldlM potentiallyRenameVar fi xs) S.empty + +--lookupBindEnv :: BindId -> BindEnv -> (Symbol, SortedReft) + +potentiallyRenameVar :: FInfo a -> (BindId, (S.HashSet BindId, S.HashSet Integer)) -> State (S.HashSet Symbol) (FInfo a) +potentiallyRenameVar fi x@(id, _) = + do s <- get + let (sym, _) = lookupBindEnv id (bs fi) + let seen = sym `S.member` s + put (if seen then s else (S.insert sym s)) + return (if seen then (renameVar fi x) else fi) + +renameVar :: FInfo a -> (BindId, (S.HashSet BindId, S.HashSet Integer)) -> FInfo a +renameVar fi (id, stuff) = elimKVar (blarg fi id sym sym') fi''' --TODO: optimize? (elimKVar separately on every rename is expensive) + where + (sym, _) = lookupBindEnv id (bs fi) + sym' = renameSymbol sym id + sub = (sym, eVar sym') + go subst x = subst1 x subst + fi' = fi { bs = adjustBindEnv (go sub) id (bs fi) } + fi'' = S.foldl' (foo sub) fi' (fst stuff) + fi''' = S.foldl' (foo' sub) fi'' (snd stuff) + +foo :: (Symbol, Expr) -> FInfo a -> BindId -> FInfo a +foo sub fi id = fi { bs = adjustBindEnv (go sub) id (bs fi) } + where go sub (sym, sr) = (sym, subst1 sr sub) + +foo' :: (Symbol, Expr) -> FInfo a -> Integer -> FInfo a +foo' sub fi id = fi { cm = M.adjust (go sub) id (cm fi) } + where go sub c = c { slhs = subst1 (slhs c) sub , + srhs = subst1 (srhs c) sub } + +blarg :: FInfo a -> BindId -> Symbol -> Symbol -> (KVar, Subst) -> Maybe Pred +blarg fi id oldSym newSym (k, Su su) = if relevant then Just $ PKVar k $ mkSubst [(newSym, eVar oldSym)] else Nothing + where + wfc = fst $ findWfC k (ws fi) + relevant = (id `elem` (elemsIBindEnv $ wenv wfc)) && (oldSym `elem` (map fst su)) + diff --git a/src/Language/Fixpoint/Solver/Validate.hs b/src/Language/Fixpoint/Solver/Validate.hs --- a/src/Language/Fixpoint/Solver/Validate.hs +++ b/src/Language/Fixpoint/Solver/Validate.hs @@ -10,6 +10,7 @@ ) where +import Language.Fixpoint.Visitor (foldSort) import Language.Fixpoint.Config import Language.Fixpoint.PrettyPrint import qualified Language.Fixpoint.Misc as Misc @@ -19,13 +20,13 @@ import qualified Data.List as L -- import Control.Monad (filterM) -- import Control.Applicative ((<$>)) --- import Debug.Trace (trace) +--import Debug.Trace (trace) import Text.Printf --------------------------------------------------------------------------- validate :: Config -> F.FInfo a -> Either E.Error (F.FInfo a) --------------------------------------------------------------------------- -validate _ = Right . renameVV +validate _ = Right . dropHigherOrderBinders . renameVV --------------------------------------------------------------------------- -- | symbol |-> sort for EVERY variable in the FInfo @@ -76,6 +77,7 @@ binders :: F.BindEnv -> [(F.Symbol, (F.Sort, F.BindId))] binders be = [(x, (F.sr_sort t, i)) | (i, x, t) <- F.bindEnvToList be] + --------------------------------------------------------------------------- -- | Alpha Rename bindings to ensure each var appears in unique binder --------------------------------------------------------------------------- @@ -97,4 +99,33 @@ x = F.reftBind $ F.sr_reft sr +--------------------------------------------------------------------------- +-- | Drop Higher-Order Binders and Constants from Environment +--------------------------------------------------------------------------- +dropHigherOrderBinders :: F.FInfo a -> F.FInfo a +--------------------------------------------------------------------------- +dropHigherOrderBinders fi = fi { F.bs = bs' , F.cm = cm' , F.ws = ws' , F.gs = gs' } + where + (bs', discards) = dropHOBinders (F.bs fi) + cm' = M.map (foo discards) (F.cm fi) + ws' = map (bar discards) (F.ws fi) + gs' = F.filterSEnv (isFirstOrder . F.sr_sort) (F.gs fi) +foo :: [F.BindId] -> F.SubC a -> F.SubC a +foo discards sc = sc { F.senv = foldr F.deleteIBindEnv (F.senv sc) discards } +bar :: [F.BindId] -> F.WfC a -> F.WfC a +bar discards wf = wf { F.wenv = foldr F.deleteIBindEnv (F.wenv wf) discards } + +dropHOBinders :: F.BindEnv -> (F.BindEnv, [F.BindId]) +dropHOBinders = filterBindEnv (isFirstOrder . F.sr_sort . Misc.thd3) + +filterBindEnv f be = (F.bindEnvFromList keep, discard') + where + (keep, discard) = L.partition f $ F.bindEnvToList be + discard' = map Misc.fst3 discard + +isFirstOrder :: F.Sort -> Bool +isFirstOrder t = {- F.traceFix ("isFO: " ++ F.showFix t) -} (foldSort f 0 t <= 1) + where + f n (F.FFunc _ _) = n + 1 + f n _ = n 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 @@ -19,6 +19,10 @@ -- * Apply Substitution , apply + + -- * Exported Sorts + , boolSort + , strSort ) where @@ -32,15 +36,16 @@ import Text.PrettyPrint.HughesPJ import Text.Printf -import Debug.Trace (trace) +------------------------------------------------------------------------- +-- | Checking Refinements ----------------------------------------------- +------------------------------------------------------------------------- + -- | Types used throughout checker type CheckM a = Either String a type Env = Symbol -> SESearch Sort -fProp :: Sort -fProp = FApp boolFTyCon [] ------------------------------------------------------------------------- -- | Checking Refinements ----------------------------------------------- @@ -244,7 +249,7 @@ checkPredBExp :: Env -> Expr -> CheckM () checkPredBExp f e = do t <- checkExpr f e - unless (t == fProp) (throwError $ errBExp e t) + unless (t == boolSort) (throwError $ errBExp e t) return () @@ -266,9 +271,11 @@ checkRelTy f _ _ (FObj l) FReal = checkFractional f l `catchError` (\_ -> throwError $ errNonFractional l) checkRelTy _ e Eq t1 t2 - | t1 == fProp || t2 == fProp = throwError $ errRel e t1 t2 + | t1 == boolSort || + t2 == boolSort = throwError $ errRel e t1 t2 checkRelTy _ e Ne t1 t2 - | t1 == fProp || t2 == fProp = throwError $ errRel e t1 t2 + | t1 == boolSort || + t2 == boolSort = throwError $ errRel e t1 t2 checkRelTy _ e Eq t1 t2 = unifys [t1] [t2] >> return () checkRelTy _ e Ne t1 t2 = unifys [t1] [t2] >> return () diff --git a/src/Language/Fixpoint/Statistics.hs b/src/Language/Fixpoint/Statistics.hs new file mode 100644 --- /dev/null +++ b/src/Language/Fixpoint/Statistics.hs @@ -0,0 +1,81 @@ +-- | This module implements functions that print out +-- statistics about the constraints. +{-# LANGUAGE CPP #-} + +module Language.Fixpoint.Statistics (statistics) where + +import Control.Arrow ((&&&)) + +#if __GLASGOW_HASKELL__ < 710 +import Data.Monoid (mempty) +import Control.Applicative ((<$>)) +import GHC.Generics (Generic) +#endif + +import Language.Fixpoint.Misc (donePhase, Moods(..), applyNonNull) +import Language.Fixpoint.Config +import Language.Fixpoint.PrettyPrint +import Language.Fixpoint.Partition (partition') +import qualified Language.Fixpoint.Types as F +import qualified Data.HashMap.Strict as M +import Data.List (sort,group) +import Text.PrettyPrint.HughesPJ + +statistics :: Config -> F.FInfo a -> IO (F.Result a) +statistics _ fi = do + let (_, fis) = partition' fi + putStrLn $ render $ pprint $ partitionStats fis + donePhase Loud "Statistics" + return mempty + +partitionStats :: [F.FInfo a] -> Maybe Stats +partitionStats fis = info + where + css = [M.keys $ F.cm fi | fi <- fis] + sizes = fromIntegral . length <$> css + info = applyNonNull Nothing (Just . mkStats) sizes + +------------------------------------------------------------------------------------- +------------------------------------------------------------------------------------- +------------------------------------------------------------------------------------- + +data Stats = Stats { cSizes :: [Float] + , cFreq :: [(Float, Int)] + , cTotal :: Float + , cMean :: Float + , cMax :: Float + , cSpeed :: Float + } deriving (Show) + +instance PPrint Stats where + pprint s = vcat [ text "STAT: max/total = " <+> pprint (cMax s) <+> text "/" <+> pprint (cTotal s) + , text "STAT: freqs = " <+> pprint (cFreq s) + , text "STAT: average = " <+> pprint (cMean s) + , text "STAT: speed = " <+> pprint (cSpeed s) + ] + +mkStats :: [Float] -> Stats +mkStats ns = Stats { + cSizes = ns + , cFreq = frequency ns + , cTotal = total + , cMean = avg + , cMax = maxx + , cSpeed = total / maxx + } + where + maxx = maximum ns + total = sum ns + avg = mean ns + +frequency :: (Ord a) => [a] -> [(a, Int)] +frequency = map (head &&& length) . group . sort + +stdDev :: [Float] -> Float +stdDev xs = sqrt (sum [(x - μ)^2 | x <- xs] / n) + where + μ = mean xs + n = fromIntegral $ length xs + +mean :: [Float] -> Float +mean ns = sum ns / fromIntegral (length ns) 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 @@ -45,21 +45,17 @@ -- * Embedding to Fixpoint Types , Sort (..), FTycon, TCEmb - , intFTyCon - , boolFTyCon - , realFTyCon - , strFTyCon - , propFTyCon - , listFTyCon - , appFTyCon - , fTyconSymbol - , symbolFTycon + , sortFTycon + , intFTyCon, boolFTyCon, realFTyCon -- TODO: hide these + -- , strFTyCon + -- , propFTyCon - , strSort + , intSort, realSort, propSort, boolSort, strSort + , listFTyCon, appFTyCon + , isListTC, isFAppTyTC + , fTyconSymbol, symbolFTycon, fTyconSort , fApp , fObj - , isListTC - , isFAppTyTC -- * Expressions and Predicates , SymConst (..) @@ -79,7 +75,7 @@ -- * Constraints , WfC (..) - , SubC, sid, sgrd, senv, slhs, srhs, subC, lhsCs, rhsCs, wfC + , SubC, subcId, sid, sgrd, senv, slhs, srhs, subC, lhsCs, rhsCs, wfC , Tag -- * Accessing Constraints @@ -89,14 +85,13 @@ , removeLhsKvars -- * Solutions - , Result + , Result (..) , FixResult (..) , FixSolution -- * Environments , SEnv, SESearch(..) , emptySEnv, toListSEnv, fromListSEnv - -- , mapSEnv , mapSEnvWithKey , insertSEnv, deleteSEnv, memberSEnv, lookupSEnv , intersectWithSEnv @@ -107,13 +102,14 @@ , IBindEnv, BindId, BindMap , emptyIBindEnv, insertsIBindEnv, deleteIBindEnv, elemsIBindEnv - , BindEnv - , insertBindEnv, emptyBindEnv, lookupBindEnv, mapBindEnv + , BindEnv, beBinds + , insertBindEnv, emptyBindEnv, lookupBindEnv, mapBindEnv, adjustBindEnv , bindEnvFromList, bindEnvToList , unionIBindEnv -- * Refinements , Refa (..), SortedReft (..), Reft(..), Reftable(..) + , raConjuncts -- * Constructing Refinements , refa @@ -162,13 +158,10 @@ -- * Qualifiers , Qualifier (..) - -- * FQ Definitions - , Def (..) - -- * Located Values , Located (..) , LocSymbol, LocText - , dummyLoc, dummyPos, dummyName, isDummy + , locAt, dummyLoc, dummyPos, dummyName, isDummy ) where import Debug.Trace (trace) @@ -193,6 +186,7 @@ import Data.Maybe (isJust, mapMaybe, listToMaybe, fromMaybe) import Text.Printf (printf) +import Language.Fixpoint.Config import Language.Fixpoint.Misc import Text.Parsec.Pos import Text.PrettyPrint.HughesPJ @@ -209,25 +203,6 @@ simplify :: a -> a simplify = id ------------------------------------------------------------------------- --- | Entities in Query File -------------------------------------------- ------------------------------------------------------------------------- - -data Def a - = Srt Sort - | Axm Pred - | Cst (SubC a) - | Wfc (WfC a) - | Con Symbol Sort - | Qul Qualifier - | Kut KVar - | IBind Int Symbol SortedReft - deriving (Generic) - -- Sol of solbind - -- Dep of FixConstraint.dep - ------------------------------------------------------------------------- - showFix :: (Fixpoint a) => a -> String showFix = render . toFix @@ -309,6 +284,16 @@ toFix (x,y) = toFix x <+> text ":" <+> toFix y simplify (x,y) = (simplify x, simplify y) +instance (Fixpoint a, Fixpoint b, Fixpoint c) => Fixpoint (a,b,c) where + toFix (x,y,z) = toFix x <+> text ":" <+> toFix y <+> text ":" <+> toFix z + simplify (x,y,z) = (simplify x, simplify y,simplify z) + +instance Fixpoint Bool where + toFix True = text "True" + toFix False = text "False" + simplify z = z + + toFixGs :: SEnv SortedReft -> Doc toFixGs (SE e) = vcat $ map (toFixConstant . mapSnd sr_sort) $ hashMapToAscList e @@ -365,6 +350,11 @@ fObj :: LocSymbol -> Sort fObj = fTyconSort . TC +sortFTycon :: Sort -> Maybe FTycon +sortFTycon FInt = Just intFTyCon +sortFTycon FReal = Just realFTyCon +sortFTycon (FApp c _) = Just c +sortFTycon _ = Nothing ---------------------------------------------------------------------- ------------------------------- Sorts -------------------------------- @@ -513,10 +503,10 @@ 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 + 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 $ text "if" <+> toFix p <+> text "then" <+> toFix e1 <+> text "else" <+> toFix e2 + toFix (ECst e so) = parens $ toFix e <+> text " : " <+> toFix so toFix (EBot) = text "_|_" ---------------------------------------------------------- @@ -526,7 +516,7 @@ data Pred = PTrue | PFalse - | PAnd ![Pred] + | PAnd !(ListNE Pred) -- [Pred] | POr ![Pred] | PNot !Pred | PImp !Pred !Pred @@ -538,12 +528,8 @@ | PTop deriving (Eq, Ord, Show, Data, Typeable, Generic) -{-@ type ListNE a = {v:[a] | 0 < len v} @-} - {-@ PAnd :: ListNE Pred -> Pred @-} - - instance Hashable Brel instance Hashable Bop instance Hashable SymConst @@ -624,12 +610,15 @@ isEq r = r == Eq || r == Ueq isSingletonReft :: Reft -> Maybe Expr -isSingletonReft (Reft (v, ra)) = firstMaybe (isSingletonExpr v) $ conjuncts $ raPred ra +isSingletonReft (Reft (v, ra)) = firstMaybe (isSingletonExpr v) $ raConjuncts ra +raConjuncts :: Refa -> [Pred] +raConjuncts = conjuncts . raPred + firstMaybe :: (a -> Maybe b) -> [a] -> Maybe b firstMaybe f = listToMaybe . mapMaybe f --- where +-- where -- go (PAtom r e1 e2) | e1 == EVar v && isEq r = Just e2 -- | e2 == EVar v && isEq r = Just e1 -- go _ = Nothing @@ -849,6 +838,9 @@ unionIBindEnv :: IBindEnv -> IBindEnv -> IBindEnv unionIBindEnv (FB m1) (FB m2) = FB $ m1 `S.union` m2 +adjustBindEnv :: ((Symbol, SortedReft) -> (Symbol, SortedReft)) -> BindId -> BindEnv -> BindEnv +adjustBindEnv f id (BE n m) = BE n $ M.adjust f id m + instance Functor SEnv where fmap = mapSEnv @@ -923,14 +915,27 @@ } deriving (Generic) +subcId :: SubC a -> Integer +subcId = mfromJust "subCId" . sid --------------------------------------------------------------------------- -- | The output of the Solver --------------------------------------------------------------------------- -type Result a = (FixResult (SubC a), M.HashMap KVar Pred) +data Result a = Result { resStatus :: FixResult (SubC a) + , resSolution :: M.HashMap KVar Pred } + deriving (Show) --------------------------------------------------------------------------- +instance Monoid (Result a) where + mempty = Result mempty mempty + mappend r1 r2 = Result stat soln + where + stat = mappend (resStatus r1) (resStatus r2) + soln = mappend (resSolution r1) (resSolution r2) +-- instance Functor Result where +-- fmap f (Result x y) = Result (fmap (fmap f) x) y + data FixResult a = Crash [a] String | Safe | Unsafe ![a] @@ -977,21 +982,21 @@ resultDoc (Crash xs msg) = vcat $ text ("Crash!: " ++ msg) : (((text "CRASH:" <+>) . toFix) <$> xs) resultDoc (Unsafe xs) = vcat $ text "Unsafe:" : (((text "WARNING:" <+>) . toFix) <$> xs) - +colorResult :: FixResult a -> Moods colorResult (Safe) = Happy colorResult (Unsafe _) = Angry colorResult (_) = Sad -instance Show (WfC a) where +instance Fixpoint a => Show (WfC a) where show = showFix -instance Show (SubC a) where +instance Fixpoint a => Show (SubC a) where show = showFix instance Fixpoint (IBindEnv) where toFix (FB ids) = text "env" <+> toFix ids -instance Fixpoint (SubC a) where +instance Fixpoint a => Fixpoint (SubC a) where toFix c = hang (text "\n\nconstraint:") 2 bd where bd = -- text "env" <+> toFix (senv c) toFix (senv c) @@ -999,14 +1004,21 @@ $+$ text "lhs" <+> toFix (slhs c) $+$ text "rhs" <+> toFix (srhs c) $+$ (pprId (sid c) <+> pprTag (stag c)) + $+$ toFixMeta (text "constraint" <+> pprId (sid c)) (toFix (sinfo c)) -instance Fixpoint (WfC a) where + +instance Fixpoint a => Fixpoint (WfC a) where toFix w = hang (text "\n\nwf:") 2 bd where bd = -- text "env" <+> toFix (wenv w) toFix (wenv w) $+$ text "reft" <+> toFix (wrft w) $+$ pprId (wid w) + $+$ toFixMeta (text "wf" <+> pprId (wid w)) (toFix (winfo w)) +toFixMeta :: Doc -> Doc -> Doc +toFixMeta k v = text "// META" <+> k <+> text ":" <+> v + -- $+$ text "\n" + pprId (Just i) = text "id" <+> tshow i pprId _ = text "" @@ -1223,7 +1235,6 @@ flattenRefas = concatMap flatRa where flatRa (Refa p) = Refa <$> flatP p - flatRa ra = [ra] flatP (PAnd ps) = concatMap flatP ps flatP p = [p] @@ -1425,6 +1436,9 @@ instance Fixpoint Qualifier where toFix = pprQual +instance Fixpoint () where + toFix _ = text "()" + instance NFData Qualifier where rnf (Q x1 x2 x3 _) = rnf x1 `seq` rnf x2 `seq` rnf x3 @@ -1443,6 +1457,7 @@ , lits :: ![(Symbol, Sort)] , kuts :: Kuts , quals :: ![Qualifier] + , bindInfo :: M.HashMap BindId a } deriving (Show) @@ -1461,24 +1476,43 @@ mappend _ _ = errorstar "mappend on non-trivial BindEnvs" instance Monoid (FInfo a) where - mempty = FI M.empty mempty mempty mempty mempty mempty mempty - mappend i1 i2 = FI { cm = mappend (cm i1) (cm i2) - , ws = mappend (ws i1) (ws i2) - , bs = mappend (bs i1) (bs i2) - , gs = mappend (gs i1) (gs i2) - , lits = mappend (lits i1) (lits i2) - , kuts = mappend (kuts i1) (kuts i2) - , quals = mappend (quals i1) (quals i2) + mempty = FI M.empty mempty mempty mempty mempty mempty mempty mempty + mappend i1 i2 = FI { cm = mappend (cm i1) (cm i2) + , ws = mappend (ws i1) (ws i2) + , bs = mappend (bs i1) (bs i2) + , gs = mappend (gs i1) (gs i2) + , lits = mappend (lits i1) (lits i2) + , kuts = mappend (kuts i1) (kuts i2) + , quals = mappend (quals i1) (quals i2) + , bindInfo = mappend (bindInfo i1) (bindInfo i2) } -toFixpoint x' = kutsDoc x' $+$ gsDoc x' $+$ conDoc x' $+$ bindsDoc x' $+$ csDoc x' $+$ wsDoc x' +($++$) :: Doc -> Doc -> Doc +x $++$ y = x $+$ text "\n" $+$ y + +toFixpoint :: (Fixpoint a) => Config -> FInfo a -> Doc +toFixpoint cfg x' = qualsDoc x' + $++$ kutsDoc x' + $++$ gsDoc x' + $++$ conDoc x' + $++$ bindsDoc x' + $++$ csDoc x' + $++$ wsDoc x' + $++$ binfoDoc x' + $++$ text "\n" where - conDoc = vcat . map toFixConstant . lits - csDoc = vcat . map toFix . M.elems . cm - wsDoc = vcat . map toFix . ws - kutsDoc = toFix . kuts - bindsDoc = toFix . bs - gsDoc = toFixGs . gs + conDoc = vcat . map toFixConstant . lits + csDoc = vcat . map toFix . M.elems . cm + wsDoc = vcat . map toFix . ws + kutsDoc = toFix . kuts + bindsDoc = toFix . bs + gsDoc = toFixGs . gs + qualsDoc = vcat . map toFix . quals + metaDoc (i,d) = toFixMeta (text "bind" <+> toFix i) (toFix d) + mdata = metadata cfg + binfoDoc + | mdata = vcat . map metaDoc . M.toList . bindInfo + | otherwise = \_ -> text "\n" ------------------------------------------------------------------------- -- | A Class Predicates for Valid Refinements Types --------------------- @@ -1582,7 +1616,7 @@ isFalse (Refa p) = isFalse p instance Falseable Reft where - isFalse (Reft(_, (Refa p))) = isFalse p + isFalse (Reft (_, ra)) = isFalse $ raPred ra --------------------------------------------------------------- -- | String Constants ----------------------------------------- @@ -1610,9 +1644,6 @@ litPrefix :: Text litPrefix = "lit" `T.snoc` symSepName -strSort :: Sort -strSort = FInt - class SymConsts a where symConsts :: a -> [SymConst] @@ -1696,8 +1727,16 @@ type LocSymbol = Located Symbol type LocText = Located Text + +locAt :: String -> a -> Located a +locAt s = Loc l l + where + l = dummyPos s + dummyLoc :: a -> Located a -dummyLoc = Loc l l where l = dummyPos "Fixpoint.Types.dummyLoc" +dummyLoc = Loc l l + where + l = dummyPos "Fixpoint.Types.dummyLoc" dummyPos :: String -> SourcePos dummyPos s = newPos s 0 0 @@ -1747,3 +1786,17 @@ instance (NFData a) => NFData (Located a) where -- FIXME: no instance NFData SrcSpan rnf (Loc _ _ x) = rnf x + +------------------------------------------------------------------------- +-- | Exported Basic Sorts ----------------------------------------------- +------------------------------------------------------------------------- + +boolSort, intSort, propSort, realSort, strSort :: Sort +boolSort = fTyconSort boolFTyCon +strSort = fTyconSort strFTyCon +intSort = fTyconSort intFTyCon +realSort = fTyconSort realFTyCon +propSort = fTyconSort propFTyCon + +fTyConSort :: FTycon -> Sort +fTyConSort c = fApp (Left c) [] 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 @@ -1,4 +1,6 @@ {-# LANGUAGE TupleSections #-} +{-# LANGUAGE PatternGuards #-} +{-# LANGUAGE CPP #-} module Language.Fixpoint.Visitor ( -- * Visitor @@ -16,16 +18,19 @@ -- * Clients , kvars , envKVars - , mapKVars + , mapKVars, mapKVars' -- * Sorts , foldSort, mapSort ) where +#if __GLASGOW_HASKELL__ < 710 import Control.Applicative (Applicative, (<$>), (<*>)) -import Control.Monad.Trans.State (State, modify, runState) import Data.Monoid import Data.Traversable (Traversable, traverse) +#endif + +import Control.Monad.Trans.State (State, modify, runState) import Language.Fixpoint.Types import qualified Data.HashSet as S import qualified Data.List as L @@ -48,8 +53,8 @@ defaultVisitor :: Monoid acc => Visitor acc ctx --------------------------------------------------------------------------------- defaultVisitor = Visitor { - ctxExpr = \c _ -> c - , ctxPred = \c _ -> c + ctxExpr = const -- \c _ -> c + , ctxPred = const -- \c _ -> c , txExpr = \_ x -> x , txPred = \_ x -> x , accExpr = \_ _ -> mempty @@ -62,8 +67,9 @@ fold v c a t = snd $ execVisitM v c a visit t trans :: (Visitable t, Monoid a) => Visitor a ctx -> ctx -> a -> t -> t -trans v c a z = fst $ execVisitM v c mempty visit z +trans v c _ z = fst $ execVisitM v c mempty visit z +execVisitM :: Visitor a ctx -> ctx -> a -> (Visitor a ctx -> ctx -> t -> State a t) -> t -> (t, a) execVisitM v c a f x = runState (f v c x) a type VisitM acc = State acc @@ -142,11 +148,16 @@ -- predKVars :: Pred -> [Symbol] mapKVars :: Visitable t => (KVar -> Maybe Pred) -> t -> t -mapKVars f = trans kvVis () [] +mapKVars f = mapKVars' f' where + f' (kv, _) = f kv + +mapKVars' :: Visitable t => ((KVar, Subst) -> Maybe Pred) -> t -> t +mapKVars' f = trans kvVis () [] + where kvVis = defaultVisitor { txPred = txK } txK _ (PKVar k su) - | Just p' <- f k = subst su p' + | Just p' <- f (k, su) = subst su p' txK _ p = p kvars :: Visitable t => t -> [KVar] @@ -155,6 +166,7 @@ kvVis = defaultVisitor { accPred = kv } kv _ (PKVar k _) = [k] kv _ _ = [] + envKVars :: BindEnv -> SubC a -> [KVar] envKVars be c = squish [ kvs sr | (_, sr) <- envCs be (senv c)] diff --git a/tests/neg/float-literal.fq b/tests/neg/float-literal.fq new file mode 100644 --- /dev/null +++ b/tests/neg/float-literal.fq @@ -0,0 +1,7 @@ + +constraint: + env [] + grd true + lhs {VV#F2 : a_aZU | []} + rhs {VV#F2 : a_aZU | [(VV#F2 >= 1.0)]} + id 2 tag [2] diff --git a/tests/pos/cut-keyword.fq b/tests/pos/cut-keyword.fq new file mode 100644 --- /dev/null +++ b/tests/pos/cut-keyword.fq @@ -0,0 +1,3 @@ + +cut $k__151 +constant Prop : (func(0, [GHC.Types.Bool; bool])) diff --git a/tests/pos/func-arg.fq b/tests/pos/func-arg.fq new file mode 100644 --- /dev/null +++ b/tests/pos/func-arg.fq @@ -0,0 +1,1 @@ +bind 0 foo : {VV : func(0, [func(0, [int])]) | []} diff --git a/tests/pos/overwrite-names.fq b/tests/pos/overwrite-names.fq new file mode 100644 --- /dev/null +++ b/tests/pos/overwrite-names.fq @@ -0,0 +1,9 @@ +constant Set_mem : (func(1, [@(0); FAppTy Set_Set @(0); bool])) + +constraint: + env [] + grd true + lhs {VV#F1 : int | [(VV#F1 > 10)]} + rhs {VV#F1 : int | [(VV#F1 > 10)]} + id 1 tag [1] + diff --git a/tests/pos/unexpected-ge.fq b/tests/pos/unexpected-ge.fq new file mode 100644 --- /dev/null +++ b/tests/pos/unexpected-ge.fq @@ -0,0 +1,2 @@ + +qualif Auto(v : int, x : int): (v = (if (x > 0) then 0 else 0)) diff --git a/tests/test.hs b/tests/test.hs --- a/tests/test.hs +++ b/tests/test.hs @@ -3,71 +3,45 @@ module Main where --- import Language.Fixpoint.Config --- import Language.Fixpoint.Names --- import Language.Fixpoint.Parse --- import Language.Fixpoint.PrettyPrint --- import Language.Fixpoint.Types - import Control.Applicative --- import Data.Char --- import Data.Tagged --- import Data.Typeable --- import Options.Applicative import System.Directory import System.Exit import System.FilePath import System.IO import System.IO.Error --- import qualified System.Posix as Posix import System.Process - --- import Control.Monad --- import Data.Proxy --- import Data.Text (Text, cons, inits, pack) --- import Test.QuickCheck import Test.Tasty import Test.Tasty.HUnit --- import Test.Tasty.Ingredients.Rerun --- import Test.Tasty.Options --- import Test.Tasty.QuickCheck --- import Test.Tasty.Runners import Text.Printf main :: IO () -main = defaultMain =<< tests - where - tests = group "Tests" [unitTests] -- [ quickCheckTests ] - -- run = defaultMainWithIngredients [ - -- rerunningTests [ listingTests, consoleTestReporter ] - -- , includingOptions [ Option (Proxy :: Proxy QuickCheckTests) - -- ] - -- ] - +main = defaultMain =<< group "Tests" [unitTests] unitTests = group "Unit" [ - testGroup "pos" <$> dirTests "tests/pos" [] ExitSuccess - , testGroup "neg" <$> dirTests "tests/neg" [] (ExitFailure 1) + testGroup "native-pos" <$> dirTests nativeCmd "tests/pos" [] ExitSuccess + , testGroup "native-neg" <$> dirTests nativeCmd "tests/neg" [] (ExitFailure 1) + , testGroup "elim-pos1" <$> dirTests elimCmd "tests/pos" [] ExitSuccess + , testGroup "elim-pos2" <$> dirTests elimCmd "tests/elim" [] ExitSuccess + , testGroup "elim-neg" <$> dirTests elimCmd "tests/neg" [] (ExitFailure 1) ] --------------------------------------------------------------------------- -dirTests :: FilePath -> [FilePath] -> ExitCode -> IO [TestTree] +dirTests :: TestCmd -> FilePath -> [FilePath] -> ExitCode -> IO [TestTree] --------------------------------------------------------------------------- -dirTests root ignored code +dirTests testCmd root ignored code = do files <- walkDirectory root let tests = [ rel | f <- files, isTest f, let rel = makeRelative root f, rel `notElem` ignored ] - return $ mkTest code root <$> tests -- hs f code | f <- hs] + return $ mkTest testCmd code root <$> tests isTest :: FilePath -> Bool isTest f = takeExtension f `elem` [".fq"] --------------------------------------------------------------------------- -mkTest :: ExitCode -> FilePath -> FilePath -> TestTree +mkTest :: TestCmd -> ExitCode -> FilePath -> FilePath -> TestTree --------------------------------------------------------------------------- -mkTest code dir file - = -- askOption $ \(smt :: SMTSolver) -> - testCase file $ +mkTest testCmd code dir file + = testCase file $ if test `elem` knownToFail then do printf "%s is known to fail: SKIPPING" test @@ -85,11 +59,14 @@ log = let (d,f) = splitFileName file in dir d ".liquid" f <.> "log" knownToFail = [] - --------------------------------------------------------------------------- -testCmd :: FilePath -> FilePath -> FilePath -> String ---------------------------------------------------------------------------- -testCmd bin dir file = printf "cd %s && %s -n %s" dir bin file +type TestCmd = FilePath -> FilePath -> FilePath -> String + +nativeCmd :: TestCmd +nativeCmd bin dir file = printf "cd %s && %s -n %s" dir bin file + +elimCmd :: TestCmd +elimCmd bin dir file = printf "cd %s && %s -n -e %s" dir bin file