liquid-fixpoint 0.3.0.1 → 0.4.0.0

raw patch · 49 files changed

+3388/−1181 lines, 49 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Fixpoint.hs +6/−5
• external/fixpoint/ast.ml +54/−23
• external/fixpoint/ast.mli +3/−0
• external/fixpoint/fixLex.mll +5/−1
• external/fixpoint/fixParse.mly +8/−7
• external/fixpoint/fixpoint.native-i386-linux binary
• external/fixpoint/fixpoint.native-i686-w64-mingw32 too large to diff
• external/fixpoint/fixpoint.native-x86_64-darwin too large to diff
• external/fixpoint/fixpoint.native-x86_64-linux too large to diff
• external/fixpoint/smtZ3.ml +93/−0
• external/misc/fixMisc.ml +3/−1
• external/ocamlgraph/.depend +0/−128
• external/ocamlgraph/src/dot_lexer.ml +386/−0
• external/ocamlgraph/src/dot_parser.ml +551/−0
• external/ocamlgraph/src/dot_parser.mli +21/−0
• external/ocamlgraph/src/gml.ml +670/−0
• external/ocamlgraph/src/version.ml +2/−0
• liquid-fixpoint.cabal +20/−12
• src/Language/Fixpoint/Config.hs +18/−19
• src/Language/Fixpoint/Errors.hs +0/−2
• src/Language/Fixpoint/Files.hs +45/−43
• src/Language/Fixpoint/Interface.hs +82/−89
• src/Language/Fixpoint/Misc.hs +10/−7
• src/Language/Fixpoint/Names.hs +8/−4
• src/Language/Fixpoint/Parse.hs +62/−85
• src/Language/Fixpoint/Partition.hs +147/−0
• src/Language/Fixpoint/PrettyPrint.hs +3/−1
• src/Language/Fixpoint/Smt/Interface.hs +289/−0
• src/Language/Fixpoint/Smt/Serialize.hs +139/−0
• src/Language/Fixpoint/Smt/Theories.hs +139/−0
• src/Language/Fixpoint/Smt/Types.hs +102/−0
• src/Language/Fixpoint/SmtLib2.hs +0/−529
• src/Language/Fixpoint/Solver/Deps.hs +9/−9
• src/Language/Fixpoint/Solver/Eliminate.hs +50/−63
• src/Language/Fixpoint/Solver/Monad.hs +10/−2
• src/Language/Fixpoint/Solver/Solution.hs +2/−2
• src/Language/Fixpoint/Solver/Solve.hs +16/−14
• src/Language/Fixpoint/Solver/Uniqify.hs +117/−0
• src/Language/Fixpoint/Solver/Validate.hs +33/−2
• src/Language/Fixpoint/Sort.hs +13/−6
• src/Language/Fixpoint/Statistics.hs +81/−0
• src/Language/Fixpoint/Types.hs +131/−78
• src/Language/Fixpoint/Visitor.hs +19/−7
• tests/neg/float-literal.fq +7/−0
• tests/pos/cut-keyword.fq +3/−0
• tests/pos/func-arg.fq +1/−0
• tests/pos/overwrite-names.fq +9/−0
• tests/pos/unexpected-ge.fq +2/−0
• tests/test.hs +19/−42

@@ -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

@@ -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

@@ -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+

@@ -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 }

@@ -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 }

binary file changed (1695021 → 1699479 bytes)

file too large to diff

file too large to diff

file too large to diff

@@ -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

@@ -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)+  | _ -> []

@@ -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 :

@@ -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++;;+

@@ -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)

@@ -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

@@ -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"

@@ -0,0 +1,2 @@+let version = "0.99b"+let date = "Wed Aug 12 18:13:31 UTC 2015"

@@ -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 (<http://z3.codeplex.com>) or CVC4 (<http://cvc4.cs.nyu.edu>) 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

@@ -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"

@@ -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 ------------------------------------------

@@ -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

@@ -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 

@@ -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

@@ -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"

@@ -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

@@ -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

@@ -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))

@@ -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)" ]+

@@ -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)+-}+

@@ -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

@@ -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+

@@ -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)--}----------------------------------------------------------------------

@@ -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])

@@ -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))

@@ -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)+

@@ -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

@@ -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-

@@ -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))+

@@ -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

@@ -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 () 

@@ -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)

@@ -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) []

@@ -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)]

@@ -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]

@@ -0,0 +1,3 @@++cut $k__151+constant Prop : (func(0, [GHC.Types.Bool; bool]))

@@ -0,0 +1,1 @@+bind 0 foo : {VV : func(0, [func(0, [int])]) | []}

@@ -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]+ 

@@ -0,0 +1,2 @@++qualif Auto(v : int, x : int): (v = (if (x > 0) then 0 else 0))

@@ -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