liquid-fixpoint 0.2.1.1 → 0.2.2.0

raw patch · 29 files changed

+2307/−251 lines, 29 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• configure +1/−1
• external/fixpoint/Makefile +11/−3
• external/fixpoint/ast.ml +12/−4
• external/fixpoint/ast.mli +12/−13
• external/fixpoint/fixLex.mll +21/−8
• external/fixpoint/fixParse.mly +10/−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/proverArch.ml +20/−3
• external/fixpoint/smtLIB2.ml +37/−8
• external/fixpoint/smtZ3.mem.ml +6/−0
• external/fixpoint/smtZ3.ml +93/−0
• external/fixpoint/smtZ3.nomem.ml +9/−0
• external/fixpoint/theories.ml +178/−46
• external/fixpoint/tpGen.ml +19/−10
• external/misc/constants.ml +9/−1
• external/ocamlgraph/.depend +108/−108
• 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 +2/−1
• src/Language/Fixpoint/Bitvector.hs +64/−0
• src/Language/Fixpoint/Names.hs +15/−0
• src/Language/Fixpoint/SmtLib2.hs +24/−15
• src/Language/Fixpoint/Types.hs +26/−23

@@ -1,4 +1,4 @@-#!/bin/bash+#!/usr/bin/env bash  ROOTHOME=`pwd` GHCBIN=`which ghc`

@@ -3,7 +3,11 @@ DIRS=-I misc OFLAGS=$(DIRS) $(IFLAGS) $(LFLAGS) $(CFLAGS) -LIBS_=-libs unix,str,graph+OCAMLC=ocamlc+OCAMLOPT=ocamlopt+OCAMLBUILD=ocamlbuild -ocamlc $(OCAMLC) -ocamlopt $(OCAMLOPT)++LIBS_=-libs unix,str,graph,nums IFLAGS_=-lflags -I,$(OCAMLGRAPHHOME) LFLAGS_=-lflags -cclib,-L$(OCAMLLIB) @@ -38,10 +42,14 @@   SMTZ3SRC=smtZ3.nomem.ml endif +ifdef CCOPT+  CFLAGS+= -cflags -ccopt,-m32+endif+ all: smtz3 	ln -sf ../misc-	ocamlbuild -r $(LIBS) $(OFLAGS) -tags thread fixpoint.native-	ocamlbuild -r $(OFLAGS) fix.cmxa+	$(OCAMLBUILD) -r $(LIBS) $(OFLAGS) -tags thread fixpoint.native+	$(OCAMLBUILD) -r $(OFLAGS) fix.cmxa 	rm -f fixpoint.native 	cp _build/fixpoint.native . 

@@ -165,7 +165,7 @@     let is_int = function       | Int -> true       | _   -> false-+         let is_real = function       | Real -> true       | _    -> false@@ -398,11 +398,15 @@  module Constant =   struct-    type t = Int of int | Real of float +    type t = Int  of int +           | Real of float +           | Lit  of string * Sort.t+     let to_string = function-      | Int i -> string_of_int i-      | Real i -> string_of_float i ^ "0"+      | Int i     -> string_of_int i+      | Real i    -> string_of_float i ^ "0"+      | Lit (s,t) -> Printf.sprintf "(lit \"%s\" %s)" s (Sort.to_string t)      let print fmt s =       to_string s |> Format.fprintf fmt "%s"@@ -509,6 +513,8 @@         x     | Con (Constant.Real x) ->          64 + int_of_float x+    | Con (Constant.Lit (s,_)) -> +        32 + Hashtbl.hash s     | MExp es ->         list_hash 6 es      | Var x -> @@ -1154,6 +1160,8 @@       Some Sort.Int    | Con (Constant.Real _) ->        Some Sort.Real +  | Con (Constant.Lit (_, t)) ->+      Some t    | Var s ->       sortcheck_sym f s   | Bin (e1, op, e2) -> 

@@ -16,9 +16,6 @@  * 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.- *  *)  (**@@ -55,7 +52,6 @@      val to_string   : t -> string     val print       : Format.formatter -> t -> unit-        val t_num       : t     val t_obj       : t     val t_bool      : t@@ -67,14 +63,14 @@     val t_app       : tycon -> t list -> t     (* val t_fptr      : t *)    -    val is_bool     : t -> bool-    val is_int      : t -> bool-    val is_real     : t -> bool-    val is_func     : t -> bool-    val is_kind     : t -> bool-    val app_of_t    : t -> (tycon * t list) option -    val func_of_t   : t -> (int * t list * t) option-    val ptr_of_t    : t -> loc option+    val is_bool      : t -> bool+    val is_int       : t -> bool+    val is_real      : t -> bool+    val is_func      : t -> bool+    val is_kind      : t -> bool+    val app_of_t     : t -> (tycon * t list) option +    val func_of_t    : t -> (int * t list * t) option+    val ptr_of_t     : t -> loc option       val compat      : t -> t -> bool     val empty_sub   : sub@@ -105,7 +101,10 @@  module Constant :   sig-    type t = Int of int | Real of float+    type t = Int  of int+           | Real of float+           | Lit  of string * Sort.t+     val to_string : t -> string     val print : Format.formatter -> t -> unit   end

@@ -47,13 +47,27 @@    *)   let safe_float_of_string s =      try float_of_string s with ex -> -      let _ = Printf.printf "safe_int_of_string crashes on: %s (error = %s)" s (Printexc.to_string ex) in+      let _ = Printf.printf "safe_float_of_string crashes on: %s (error = %s)" s (Printexc.to_string ex) in       raise ex    let safe_int_of_string s =      try int_of_string s with ex ->        let _ = Printf.printf "safe_int_of_string crashes on: %s (error = %s)" s (Printexc.to_string ex) in       raise ex++  let string_suffix_from s n = String.sub s n (String.length s - n)++  let snip_begin_end str =+    let len = String.length str in+		String.sub str 1 (len-2)+                            +  (* let safe_big_int_of_string s = +    try Big_int.big_int_of_string (string_suffix_from s 2) with ex -> +      let _ = Printf.printf "safe_big_int_of_string crashes on: %s (error = %s)" s (Printexc.to_string ex) in+      raise ex+   *)++ }  let digit    = ['0'-'9' '-']@@ -76,6 +90,7 @@ 			              token lexbuf                           end                          }+  | '_'                 { UNDERSCORE }   | '['                 { LB }   | ']'                 { RB }   | '('			        { LPAREN }@@ -121,6 +136,7 @@   | "ptr"               { PTR }   | "<fun>"             { LFUN }   (* | "fptr"           { FPTR } *)+  | "lit"               { LIT }   | "bool"              { BOOL }   | "uit"               { UNINT }   | "func"              { FUNC }@@ -142,13 +158,10 @@   | "reft"              { REF }   | "@"                 { TVAR }    | (digit)+'.'(digit)+	{ Real (safe_float_of_string (Lexing.lexeme lexbuf)) }-  | (digit)+	        { Num (safe_int_of_string (Lexing.lexeme lexbuf)) }-  | (alphlet)letdig*	{ Id    (Lexing.lexeme lexbuf) }-  | '''[^''']*'''       { let str = Lexing.lexeme lexbuf in-			              let len = String.length str in-			              Id (String.sub str 1 (len-2)) -                        }-  +  | (digit)+	          { Num  (safe_int_of_string (Lexing.lexeme lexbuf)) }+  | (alphlet)letdig*	  { Id    (Lexing.lexeme lexbuf) }+  | '''[^''']*'''       { Id (snip_begin_end (Lexing.lexeme lexbuf)) }+  | '"'[^''']*'"'       { StringLit (snip_begin_end (Lexing.lexeme lexbuf)) }   | eof			{ EOF }   | _			{                            begin

@@ -53,12 +53,14 @@ %}  %token <string> Id-%token <int> Num-%token <float> Real+%token <int>    Num+%token <float>  Real+%token <string> StringLit  %token TVAR  %token TAG ID  %token BEXP %token TRUE FALSE+%token UNDERSCORE  %token LPAREN  RPAREN LB RB LC RC %token EQ NE GT GE LT LE UEQ UNE %token AND OR NOT NOTWORD IMPL IFF IFFWORD FORALL SEMI COMMA COLON MID@@ -69,7 +71,7 @@ %token TIMES  %token DIV  %token QM DOT ASGN-%token OBJ REAL INT NUM PTR LFUN BOOL UNINT FUNC+%token OBJ REAL INT NUM PTR LFUN BOOL UNINT FUNC LIT %token SRT AXM CON CST WF SOL QUL KUT BIND ADP DDP %token ENV GRD LHS RHS REF @@ -311,6 +313,7 @@   | Num                                   { (A.Constant.Int $1) }   | MINUS Num                             { (A.Constant.Int (-1 * $2)) }   | MINUS Real                            { (A.Constant.Real (-. $2)) }+  | LIT StringLit sort                    { (A.Constant.Lit ($2, $3)) }   ;  cons:@@ -324,13 +327,13 @@   ;  wf:-    ENV env REF reft                              { C.make_wf $2 $4 None }-  | ENV env REF reft ID Num                       { C.make_wf $2 $4 (Some $6) }+    ENV env REF reft                      { C.make_wf $2 $4 None }+  | ENV env REF reft ID Num               { C.make_wf $2 $4 (Some $6) }   ;  tagsne:-  Num                                             { [$1] }-  | Num SEMI tagsne                               { $1 :: $3 }+  Num                                     { [$1] }+  | Num SEMI tagsne                       { $1 :: $3 }   ;  tag: 

binary file changed (1567816 → 1689979 bytes)

file too large to diff

file too large to diff

file too large to diff

@@ -34,7 +34,7 @@   val sort_name   : sortDef -> Ast.Sort.tycon   val mk_thy_sort : sortDef -> context -> sort list -> sort   val mk_thy_app  : appDef  -> context -> sort list -> ast list -> ast-  val theories    : sortDef list * appDef list+  val theories    : unit -> sortDef list * appDef list end  module type SMTSOLVER = sig@@ -64,6 +64,7 @@   val mkIte     : context -> ast -> ast -> ast -> ast   val mkInt     : context -> int -> sort -> ast   val mkReal    : context -> float -> sort -> ast+  val mkLit     : context -> string -> sort -> ast   val mkTrue    : context -> ast   val mkFalse   : context -> ast   val mkNot     : context -> ast -> ast@@ -74,8 +75,9 @@   val mkRel     : context -> Ast.brel   -> ast -> ast -> ast     (* Conversions *)-  val astString : context -> ast -> string-+  val astString     : context -> ast -> string+  val sortString    : context -> sort -> string+                                              (* Set Theory Operations *)   val mkSetSort     : context -> sort   -> sort   val mkEmptySet    : context -> sort -> ast@@ -85,6 +87,21 @@   val mkSetCap      : context -> ast -> ast -> ast   val mkSetDif      : context -> ast -> ast -> ast   val mkSetSub      : context -> ast -> ast -> ast++  (* Map Theory Operations *)++  val mkMapSort     : context -> sort -> sort -> sort+  val mkMapSelect   : context -> ast -> ast -> ast+  val mkMapStore    : context -> ast -> ast -> ast -> ast+++  (* BitVector Theory Operations *)+  val mkSizeSort    : context -> int  -> sort +  val mkBitSort     : context -> sort -> sort +  val mkBitAnd      : context -> ast  -> ast -> ast +  val mkBitOr       : context -> ast  -> ast -> ast++    (* Constructors *)   val mkContext      : (string * string) array -> context

@@ -106,6 +106,10 @@ let sub = "smt_set_sub" let com = "smt_set_com" +let map = "SMT_Map"+let sel = "smt_map_sel"+let sto = "smt_map_sto"+ (*     (define-fun smt_set_emp () Set ((as const Set) false))    (define-fun smt_set_mem ((x Elt) (s Set)) Bool (select s x))@@ -119,6 +123,18 @@  let (++) = List.append +(* array preamble *)+let array_preamble _ = +  if not !Co.map_theory then [] else+    [ spr "(define-sort %s () (Array %s %s))" +        map elt elt +    ; spr "(define-fun %s ((m %s) (k %s)) %s (select m k))"+        sel map elt elt +    ; spr "(define-fun %s ((m %s) (k %s) (v %s)) %s (store m k v))"+        sto map elt elt map+    ]++ (* z3 specific *) let z3_preamble _    =  [ "(set-option :auto-config false)"@@ -146,12 +162,13 @@         dif set set set cap com     ; spr "(define-fun %s ((s1 %s) (s2 %s)) Bool (= %s (%s s1 s2)))"         sub set set emp dif -    ] +    ] ++ array_preamble () + (* cvc4 specific *) let cvc4_preamble _    =  if not !Co.set_theory then [] else-    [ spr "(set-logic QF_UFNIRAFS)"+    [ spr "(set-logic QF_AUFNIRAFS)"     ; spr "(define-sort %s () Int)"         elt     ; spr "(define-sort %s () (Set %s))" @@ -168,15 +185,11 @@         cap set set set     ; spr "(declare-fun %s (%s) %s)"         com set set-    (* -    ; spr "(define-fun %s ((s %s)) %s ((_ map not) s))"-        com set set-     *)     ; spr "(define-fun %s ((s1 %s) (s2 %s)) %s (setminus s1 s2))"         dif set set set     ; spr "(define-fun %s ((s1 %s) (s2 %s)) Bool (subset s1 s2))"         sub set set-    ] +    ] ++ array_preamble ()  let smtlib_preamble    = [ spr "(set-logic QF_UFLIA)"@@ -189,7 +202,9 @@     ; spr "(declare-fun %s (%s %s) %s)"   dif set set set     ; spr "(declare-fun %s (%s %s) Bool)" sub set set      ; spr "(declare-fun %s (%s %s) Bool)" mem elt set -   +    ; spr "(declare-fun %s (%s %s) %s)"    sel map elt elt +    ; spr "(declare-fun %s (%s %s %s) %s)" sto map elt elt map +         (* HIDE?      ; spr "(assert (forall ((x %s)) (not (%s x %s))))"            elt mem emp@@ -218,6 +233,16 @@ let mkSetDif _ s t = spr "(%s %s %s)" dif s t let mkSetSub _ s t = spr "(%s %s %s)" sub s t +let mkMapSort c k v    = map +let mkMapSelect c m k  = spr "(%s %s %s)"    sel m k +let mkMapStore c m k v = spr "(%s %s %s %s)" sto m k v++let mkSizeSort _ n = spr "%d" n                          +let mkBitSort _ s  = spr "(_ BitVec %s)" s +let mkBitAnd _ x y = spr "(bvand %s %s)" x y+let mkBitOr  _ x y = spr "(bvor  %s %s)" x y++ (******************************************************************) (**************** SMT IO ******************************************) (** https://raw.github.com/ravichugh/djs/master/src/zzz.ml ********)@@ -364,6 +389,7 @@  let stringSymbol _ s = s let astString _ a    = a +let sortString _ s   = s  let isBool c a       = failwith "TODO:SMTLib2.isBool" let boundVar me i t  = failwith "TODO:SMTLib2.boundVar" @@ -383,6 +409,9 @@                      else spr "(- %d)" (abs i) let mkReal _ i _   = if i >= 0. then string_of_float i ^ "0" (* add trailing 0 for floats like 1. *)                      else spr "(- %s)" (string_of_float (i *. -1.0) ^ "0")++let mkLit _ l _    = l+                        let mkTrue _       = "true" let mkFalse _      = "false"  

@@ -113,6 +113,12 @@ let mkSetSub   = Z3.mk_set_subset  let mkContext  = Z3.mk_context_x  ++let mkMapSort   = fun _ _ _ -> failwith "TODO: smtZ3.mem : mkMapSort"+let mkMapSelect = fun _ _ _ -> failwith "TODO: smtZ3.mem : mkMapSelect"+let mkMapStore  = fun _ _ _ _ -> failwith "TODO: smtZ3.mem : mkMapStore"++ (*********************************************************)  let z3push me =

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

@@ -51,6 +51,7 @@ 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@@ -60,6 +61,7 @@ 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@@ -71,6 +73,13 @@ 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

@@ -26,13 +26,16 @@ open ProverArch open FixMisc.Ops +(***************************************************************************)+(********************* NAMES (independent of SMT) **************************)+(***************************************************************************)++(********************* Sets ************************************************)+ let set_tycon  = So.tycon "Set_Set" let t_set a    = So.t_app set_tycon [a]  (* API *)-let is_interp t = t = set_tycon--(* API *) let emp0 = ( Sy.of_string "Set_empty"            , So.t_func 1 [So.t_int; t_set (So.t_generic 0)] ) @@ -45,7 +48,6 @@ let mem = ( Sy.of_string "Set_mem"           , So.t_func 1 [So.t_generic 0; t_set (So.t_generic 0); So.t_bool] ) - let cup = ( Sy.of_string "Set_cup"           , So.t_func 1 [t_set (So.t_generic 0); t_set (So.t_generic 0); t_set (So.t_generic 0)]) @@ -58,11 +60,58 @@ let sub = ( Sy.of_string "Set_sub"            , So.t_func 1 [t_set (So.t_generic 0); t_set (So.t_generic 0); So.t_bool] ) +(********************* Maps ************************************************)++let map_tycon  = So.tycon "Map_t"++let t_map k v  = So.t_app map_tycon [k; v]++let select     = let k = So.t_generic 0 in+                 let v = So.t_generic 1 in+                 ( Sy.of_string "Map_select"+                 , So.t_func 2 [t_map k v; k; v] )++let store      = let k = So.t_generic 0 in+                 let v = So.t_generic 1 in+                 ( Sy.of_string "Map_store"+                 , So.t_func 2 [t_map k v; k; v; t_map k v] )++++(********************* Maps ************************************************)++let bv_tycon     = So.tycon "BitVec"+let sz32_tycon   = So.tycon "Size32"+let sz64_tycon   = So.tycon "Size64"+let t_bv a       = So.t_app bv_tycon [a]++let bv_binop op  = let k = So.t_generic 0 in+                   ( Sy.of_string op +                   , So.t_func 1 [t_bv k; t_bv k; t_bv k] ) ++let bvand        = bv_binop "bvand"+let bvor         = bv_binop "bvor"++                 +(********************* All Theories ****************************************)+(** WARNING: DO NOT PUT INSIDE MakeTheory; adds SMT dependency *************)+(***************************************************************************)++(* API *)+let is_interp t = List.mem t [set_tycon; map_tycon; sz32_tycon; sz64_tycon; bv_tycon]++(* API *) let interp_syms _ -  = if !Constants.set_theory -     then [emp0; emp; sng; mem; cup; cap; dif; sub]-     else []+  = []+    |> (!Constants.set_theory <?> (++) [emp0  ; emp; sng; mem; cup; cap; dif; sub])+    |> (!Constants.map_theory <?> (++) [select; store])+    |> (!Constants.bit_theory <?> (++) [bvand ; bvor]) ++(***************************************************************************)+(***************************************************************************)+(***************************************************************************)+ module MakeTheory(SMT : SMTSOLVER):    (THEORY with type context = SMT.context            and  type sort    = SMT.sort@@ -90,10 +139,41 @@ let sym_sort d  = d.sy_sort  (***************************************************************************)-(******************** Theory of Sets ***************************************)+(********* Wrappers Around Z3 Constructors For Last-Minute Checking ********) (***************************************************************************) -let set_set : sortDef = +let app_sort_arity def = match So.func_of_t def.sy_sort with+  | Some (n,_,_) -> n+  | None         -> assertf "Theories: app with non-function symbol %s" +                    (Sy.to_string def.sy_name)++let check_app_arities def tArgs eArgs = match So.func_of_t def.sy_sort with+  | Some (n, ts,_) +     -> asserts (n = List.length tArgs)  +          "Theories: app with mismatched sorts %s" (Sy.to_string def.sy_name);+        asserts (List.length ts = List.length eArgs) +          "Theories: app with mismatched args %s" (Sy.to_string def.sy_name) +  | None         +     -> assertf "Theories: app with non-function symbol %s" +          (Sy.to_string def.sy_name)+++(* API *)+let mk_thy_app def c ts es = +  check_app_arities def ts es;+  def.sy_emb c ts es++(* API *)+let mk_thy_sort def c ts = +  asserts (List.length ts = def.so_arity) +    "Theories: app with mismatched sorts %s" (So.tycon_string def.so_name);+  def.so_emb c ts +++(** Theory of Sets *********************************************************)+++let set_t : sortDef =    { so_name  = set_tycon    ; so_arity = 1    ; so_emb   = fun c -> function @@ -101,7 +181,6 @@                  | _ -> assertf "Set_set: type mismatch"   }   - let set_empty : appDef  =    { sy_name  = fst emp0   ; sy_sort  = snd emp0 @@ -110,8 +189,6 @@                  | _        -> assertf "Set_empty: type mismatch"   } -- let set_emp : appDef  =    { sy_name  = fst emp    ; sy_sort  = snd emp @@ -133,7 +210,7 @@   { sy_name = fst mem    ; sy_sort = snd mem   ; sy_emb  = fun c ts es -> match ts, es with-                 | [t], [e;es] -> SMT.mkSetMem c e es +                 | [_], [e;es] -> SMT.mkSetMem c e es                   | _           -> assertf "Set_mem: type mismatch"   } @@ -169,47 +246,102 @@                  | _            -> assertf "Set_dif: type mismatch"   } -(***************************************************************************)-(********* Wrappers Around Z3 Constructors For Last-Minute Checking ********)-(***************************************************************************)+(* API *)+let theory_set +  = ([ set_t ]+    ,[ set_emp +     ; set_empty +     ; set_sng +     ; set_mem +     ; set_cup +     ; set_cap +     ; set_dif +     ; set_sub ]) -let app_sort_arity def = match So.func_of_t def.sy_sort with-  | Some (n,_,_) -> n-  | None         -> assertf "Theories: app with non-function symbol %s" -                    (Sy.to_string def.sy_name)+(** Theory of Maps *********************************************************) -let check_app_arities def tArgs eArgs = match So.func_of_t def.sy_sort with-  | Some (n, ts,_) -     -> asserts (n = List.length tArgs)  -          "Theories: app with mismatched sorts %s" (Sy.to_string def.sy_name);-        asserts (List.length ts = List.length eArgs) -          "Theories: app with mismatched args %s" (Sy.to_string def.sy_name) -  | None         -     -> assertf "Theories: app with non-function symbol %s" -          (Sy.to_string def.sy_name)+let map_t : sortDef = +  { so_name  = map_tycon +  ; so_arity = 2 +  ; so_emb   = fun c -> function +                 | [k; v] -> SMT.mkMapSort c k v +                 | _      -> assertf "Map_t: type mismatch"+  }   +let map_select : appDef  = +  { sy_name = fst select +  ; sy_sort = snd select +  ; sy_emb  = fun c ts es -> match ts, es with+                 | [_; _], [m; k] -> SMT.mkMapSelect c m k +                 | _           -> assertf "Map_select: type mismatch"+  } +let map_store : appDef  = +  { sy_name = fst store +  ; sy_sort = snd store +  ; sy_emb  = fun c ts es -> match ts, es with+                 | [_; _], [m; k; v] -> SMT.mkMapStore c m k v +                 | _           -> assertf "Map_store: type mismatch"+  }+ (* API *)-let mk_thy_app def c ts es = -  check_app_arities def ts es;-  def.sy_emb c ts es+let theory_map+  = ([map_t], [map_select; map_store]) +(** Theory of Bitvectors ***************************************************)++let size32_t : sortDef =+  { so_name  = sz32_tycon +  ; so_arity = 1 +  ; so_emb   = fun c -> function +                 | [_] -> SMT.mkSizeSort c 32 +                 | _   -> assertf "Map_t: type mismatch"+  }  ++let size64_t : sortDef =+  { so_name  = sz64_tycon +  ; so_arity = 1 +  ; so_emb   = fun c   -> function +                 | [_] -> SMT.mkSizeSort c 64 +                 | _   -> assertf "Map_t: type mismatch"+  }  +    +let bit_t : sortDef =+  { so_name  = bv_tycon +  ; so_arity = 1 +  ; so_emb   = fun c -> function +                 | [n] -> SMT.mkBitSort c n +                 | _   -> assertf "BitVector: type mismatch"+  }  ++let bit_and : appDef  = +  { sy_name = fst bvand +  ; sy_sort = snd bvand  +  ; sy_emb  = fun c ts es -> match ts, es with+                 | [_], [x; y] -> SMT.mkBitAnd c x y +                 | _           -> assertf "bit_and: type mismatch"+  }++let bit_or : appDef  = +  { sy_name = fst bvor+  ; sy_sort = snd bvor+  ; sy_emb  = fun c ts es -> match ts, es with+                 | [_], [x; y] -> SMT.mkBitOr c x y +                 | _           -> assertf "bit_or: type mismatch"+  }+ (* API *)-let mk_thy_sort def c ts = -  asserts (List.length ts = def.so_arity) -    "Theories: app with mismatched sorts %s" (So.tycon_string def.so_name);-  def.so_emb c ts +let theory_bit+  = ([size32_t; size64_t; bit_t], [bit_and; bit_or])+    +(** Theory Composition *****************************************************)  (* API *)-let theories = -  ([set_set], [set_emp; -	       set_empty; -               set_sng; -               set_mem; -               set_cup; -               set_cap; -               set_dif; -               set_sub])+let theories () = +  let add_thy (t1,s1) (t2,s2) = (t1 ++ t2, s1 ++ s2) in+  ([], [])+  |> (!Constants.set_theory <?> add_thy theory_set)+  |> (!Constants.map_theory <?> add_thy theory_map)+  |> (!Constants.bit_theory <?> add_thy theory_bit) -   end

@@ -133,17 +133,20 @@     if So.is_bool t then me.tbool else       if So.is_int t then me.tint else         if So.is_real t then me.treal else-          match z3TypeThy me t with -            | Some t' -> t'-            | None    -> me.tint+          Misc.maybe_default (z3TypeThy me t) me.tint+          (* match z3TypeThy me t with +              | Some t' -> t'+              | None    -> me.tint *)    end t t -and z3TypeThy me t = match So.app_of_t t with- | Some (c, ts) when H.mem me.thy_sortm c -> +and z3TypeThy me t =+  match So.app_of_t t with+  | Some (c, ts) when H.mem me.thy_sortm c ->       let def = H.find me.thy_sortm c   in      let zts = List.map (z3Type me) ts in      Some (Th.mk_thy_sort def me.c zts)- | _ -> None +  | _ ->+     None    (***********************************************************************) (********************** Identifiers ************************************)@@ -284,11 +287,17 @@   | (e1, e2) ->        SMT.mkMul me.c (z3Exp me env e1) (z3Exp me env e2) -and z3Exp me env = function-  | A.Con (A.Constant.Int i), _ -> +and z3Con me env = function+  | A.Constant.Int i ->        SMT.mkInt me.c i me.tint -  | A.Con (A.Constant.Real i), _ -> +  | A.Constant.Real i ->        SMT.mkReal me.c i me.treal+  | A.Constant.Lit (l, t) ->+      SMT.mkLit me.c l (z3Type me t)+                +and z3Exp me env = function+  | A.Con c, _ ->+      z3Con me env c   | A.Var s, _ ->        z3Var me env s   | A.Cst ((A.App (f, es), _), t), _ when (H.mem me.thy_symm f) -> @@ -398,7 +407,7 @@ (************************************************************************)  let create_theories () =-  Th.theories +  Th.theories ()    |> (Misc.hashtbl_of_list_with Th.sort_name <**> Misc.hashtbl_of_list_with Th.sym_name)  let assert_distinct_constants me env = function [] -> () | cs -> 

@@ -80,7 +80,9 @@ let gen_qual_sorts              = ref true  (* -no-gen-qual-sorts  *) let web_demo                    = ref false (* -web-demo *) let simple                      = ref true  (* -simple  *) +let bit_theory                  = ref true  (* -bit-theory  *)  let set_theory                  = ref true  (* -set-theory  *) +let map_theory                  = ref true  (* -map-theory  *)  let ueq_all_sorts               = ref false (* -ueq-all-sorts *)  (* JHALA: what do these do ? *)@@ -244,9 +246,15 @@    ( "-nosimple"    , Arg.Clear simple    , " Directly propagate qualifiers for simple constraints (K1 <: K2) [true]");+   ( "-nobittheory"+   , Arg.Clear bit_theory+   , " Support for SMT bitvector theory [true]");    ( "-nosettheory"    , Arg.Clear set_theory-   , " Support for set theory on Z3 [true]");+   , " Support for SMT set theory [true]");+   ( "-nomaptheory"+   , Arg.Clear map_theory+   , " Support for SMT map theory [true]");    ("-psimple",      Arg.Set psimple,      " prioritize simple constraints [true]");

@@ -1,128 +1,128 @@-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 \+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/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/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.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/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/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/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/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/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/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.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.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/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 \+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 :+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 = "Fri Feb 6 22:49:24 UTC 2015"

@@ -1,5 +1,5 @@ name:                liquid-fixpoint-version:             0.2.1.1+version:             0.2.2.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@@ -148,6 +148,7 @@                    Language.Fixpoint.Errors,                    Language.Fixpoint.Config,                    Language.Fixpoint.Types,+                   Language.Fixpoint.Bitvector,                    Language.Fixpoint.Visitor,                    Language.Fixpoint.Sort,                    Language.Fixpoint.Interface, 

@@ -0,0 +1,64 @@+{-# LANGUAGE DeriveGeneric             #-}+{-# LANGUAGE DeriveDataTypeable        #-}++module Language.Fixpoint.Bitvector+       ( -- * Sizes +         BvSize (..)++         -- * Operators+       , BvOp (..)++         -- * BitVector Sort Constructor+       , mkSort ++         -- * BitVector Expression Constructor +       , eOp++       ) where++import qualified Data.Text as T+import Language.Fixpoint.Types+import Language.Fixpoint.Names+import GHC.Generics         (Generic)+import Data.Typeable        (Typeable)+import Data.Generics        (Data)++data Bv     = Bv BvSize String ++data BvSize = S32   | S64+              deriving (Eq, Ord, Show, Data, Typeable, Generic)++data BvOp   = BvAnd | BvOr+              deriving (Eq, Ord, Show, Data, Typeable, Generic)++-- | Construct the bitvector `Sort` from its `BvSize`++mkSort :: BvSize -> Sort+mkSort s = fApp (Left bvTyCon) [sizeSort s]++-- | Construct an `Expr` using a raw string, e.g. (Bv S32 "#x02000000")+instance Expression Bv where+  expr (Bv sz v) = ECon $ L (T.pack v) (mkSort sz)++-- | Apply some bitvector operator to a list of arguments++eOp :: BvOp -> [Expr] -> Expr+eOp o es = EApp (opName o) es+++--------------------------------------------------------------------++opName :: BvOp -> LocSymbol+opName BvAnd = dummyLoc bvAndName+opName BvOr  = dummyLoc bvOrName++sizeSort     = (`FApp` []) . sizeTC+sizeTC       = symbolFTycon . dummyLoc . sizeName +sizeName S32 = size32Name+sizeName S64 = size64Name++bvTyCon      = symbolFTycon $ dummyLoc bitVecName++-- s32TyCon     = symbolFTycon $ dummyLoc size32Name +-- s64TyCon     = symbolFTycon $ dummyLoc size64Name+

@@ -44,6 +44,7 @@   , strConName   , vvName   , symSepName+  , size32Name, size64Name, bitVecName, bvAndName, bvOrName   , prims ) where @@ -250,6 +251,12 @@ vvName       = "VV" symSepName   = '#' +size32Name   = "Size32" :: Symbol +size64Name   = "Size64" :: Symbol+bitVecName   = "BitVec" :: Symbol+bvOrName     = "bvor"   :: Symbol+bvAndName    = "bvAnd"  :: Symbol+ prims :: [Symbol] prims = [ propConName         , hpropConName@@ -265,6 +272,14 @@         , "Set_empty"         , "Set_mem"         , "Set_sub"+        , "Map_t"+        , "Map_select"+        , "Map_store"+        , size32Name+        , size64Name+        , bitVecName+        , bvOrName +        , bvAndName         , "FAppTy"          ] 

@@ -275,23 +275,30 @@ --------------------------------------------------------------------------  elt, set :: Raw-elt = "Elt"-set = "Set"+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"-+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"+         smt_set_funs :: M.HashMap Symbol Raw-smt_set_funs = M.fromList [("Set_emp",emp),("Set_add",add),("Set_cup",cup)-                          ,("Set_cap",cap),("Set_mem",mem),("Set_dif",dif)-                          ,("Set_sub",sub),("Set_com",com)]+smt_set_funs = M.fromList [ ("Set_emp",emp),("Set_add",add),("Set_cup",cup)+                          , ("Set_cap",cap),("Set_mem",mem),("Set_dif",dif)+                          , ("Set_sub",sub),("Set_com",com)]  -- DON'T REMOVE THIS! z3 changed the names of options between 4.3.1 and 4.3.2... z3_432_options @@ -328,6 +335,7 @@         (sub, set, set, emp, dif)     ] + smtlibPreamble   = [        "(set-logic QF_UFLIA)"     , format "(define-sort {} () Int)"       (Only elt)@@ -447,7 +455,8 @@   smt2 (Push)              = "(push 1)"   smt2 (Pop)               = "(pop 1)"   smt2 (CheckSat)          = "(check-sat)"-  smt2 (GetValue xs)       = LT.unwords $ ["(get-value ("] ++ map smt2 xs ++ ["))"]+  smt2 (GetValue xs)       = LT.unwords $ ["(get-value ("] ++ fmap smt2 xs ++ ["))"]+  smt2s = LT.intercalate " " . fmap smt2 

@@ -55,7 +55,8 @@   , fObj    -- * Expressions and Predicates-  , SymConst (..), Constant (..)+  , SymConst (..)+  , Constant (..)    , Bop (..), Brel (..)   , Expr (..), Pred (..)   , eVar@@ -153,11 +154,12 @@   , dummyLoc, dummyPos, dummyName, isDummy   ) where -import GHC.Generics         (Generic) import Debug.Trace          (trace) +import GHC.Generics         (Generic) import Data.Typeable        (Typeable) import Data.Generics        (Data)+ import Data.Monoid hiding   ((<>)) import Data.Functor import Data.Char            (ord, chr, isAlpha, isUpper, toLower)@@ -290,8 +292,6 @@ toFix_constant (c, so)   = text "constant" <+> toFix c <+> text ":" <+> toFix so -- ---------------------------------------------------------------------- ------------------------ Type Constructors --------------------------- ----------------------------------------------------------------------@@ -305,7 +305,6 @@ propFTyCon = TC $ dummyLoc propConName appFTyCon  = TC $ dummyLoc "FAppTy" - isListTC (TC (Loc _ c)) = c == listConName isTupTC  (TC (Loc _ c)) = c == tupConName isFAppTyTC = (== appFTyCon)@@ -337,6 +336,8 @@  fObj :: LocSymbol -> Sort fObj = fTyconSort . TC++  ---------------------------------------------------------------------- ------------------------------- Sorts -------------------------------- ----------------------------------------------------------------------@@ -379,9 +380,10 @@ instance Fixpoint FTycon where   toFix (TC s)       = toFix s --------------------------------------------------------------------------------------------++------------------------------------------------------------------------ sortSubst                  :: (M.HashMap Symbol Sort) -> Sort -> Sort--------------------------------------------------------------------------------------------+------------------------------------------------------------------------ sortSubst θ t@(FObj x)   = fromMaybe t (M.lookup x θ) sortSubst θ (FFunc n ts) = FFunc n (sortSubst θ <$> ts) sortSubst θ (FApp c ts)  = FApp c  (sortSubst θ <$> ts)@@ -406,7 +408,9 @@ data SymConst = SL !Text               deriving (Eq, Ord, Show, Data, Typeable, Generic) -data Constant = I  !Integer | R !Double+data Constant = I !Integer+              | R !Double+              | L !Text !Sort                deriving (Eq, Ord, Show, Data, Typeable, Generic)  data Brel = Eq | Ne | Gt | Ge | Lt | Le | Ueq | Une@@ -434,9 +438,10 @@   toFix = double  instance Fixpoint Constant where-  toFix (I i)  = toFix i-  toFix (R i)  = toFix i-+  toFix (I i)   = toFix i+  toFix (R i)   = toFix i+  toFix (L s t) = parens $ text "lit" <+> toFix s <+> toFix t   +                     instance Fixpoint SymConst where   toFix  = toFix . encodeSymConst @@ -597,6 +602,8 @@ -- | Generalizing Symbol, Expression, Predicate into Classes ----------- ------------------------------------------------------------------------ +-- | Values that can be viewed as Constants + -- | Values that can be viewed as Expressions  class Expression a where@@ -635,11 +642,11 @@   prop True  = PTrue   prop False = PFalse -eVar          ::  Symbolic a => a -> Expr-eVar          = EVar . symbol+eVar ::  Symbolic a => a -> Expr+eVar = EVar . symbol -eProp         ::  Symbolic a => a -> Pred-eProp         = mkProp . eVar+eProp ::  Symbolic a => a -> Pred+eProp = mkProp . eVar  relReft :: (Expression a) => Brel -> a -> Reft relReft r e   = Reft (vv_, [RConc $ PAtom r (eVar vv_)  (expr e)])@@ -649,11 +656,6 @@ notExprReft   = relReft Ne uexprReft     = relReft Ueq ---- exprReft e             = Reft (vv_, [RConc $ PAtom Eq (eVar vv_)  (expr e)])--- notExprReft e          = Reft (vv_, [RConc $ PAtom Ne (eVar vv_)  (expr e)])--- exprReft e             = Reft (vv_, [RConc $ PAtom Eq (eVar vv_)  (expr e)])- propReft      ::  (Predicate a) => a -> Reft propReft p    = Reft (vv_, [RConc $ PIff     (eProp vv_) (prop p)]) @@ -1134,9 +1136,10 @@   rnf (BE x m) = rnf x `seq` rnf m  instance NFData Constant where-  rnf (I x) = rnf x-  rnf (R x) = rnf x-+  rnf (I x)     = rnf x+  rnf (R x)     = rnf x+  rnf (L s t) = rnf s `seq` rnf t+   instance NFData SymConst where   rnf (SL x) = rnf x