liquid-fixpoint 0.2.0.0 → 0.2.1.0
raw patch · 31 files changed
+490/−2225 lines, 31 filessetup-changedbinary-added
Files
- Fixpoint.hs +2/−2
- LICENSE +1/−1
- Setup.hs +36/−24
- external/fixpoint/Makefile +1/−1
- external/fixpoint/ast.ml +46/−12
- external/fixpoint/fixParse.mly +7/−7
- external/fixpoint/fixpoint.native-i386-linux binary
- external/fixpoint/fixpoint.native-i686-w64-mingw32 binary
- external/fixpoint/fixpoint.native-x86_64-darwin too large to diff
- external/fixpoint/fixpoint.native-x86_64-linux too large to diff
- external/fixpoint/foo.ml +6/−0
- external/fixpoint/smtLIB2.ml +67/−6
- external/fixpoint/smtZ3.ml +0/−84
- external/fixpoint/theories.ml +16/−1
- external/fixpoint/tpGen.ml +49/−8
- external/ocamlgraph/META +0/−5
- external/ocamlgraph/Makefile +0/−386
- external/ocamlgraph/src/dot_lexer.ml +0/−386
- external/ocamlgraph/src/dot_parser.ml +0/−552
- external/ocamlgraph/src/dot_parser.mli +0/−21
- external/ocamlgraph/src/gml.ml +0/−670
- external/ocamlgraph/src/version.ml +0/−2
- liquid-fixpoint.cabal +18/−8
- src/Language/Fixpoint/Files.hs +19/−16
- src/Language/Fixpoint/Misc.hs +7/−5
- src/Language/Fixpoint/Names.hs +1/−0
- src/Language/Fixpoint/Parse.hs +2/−2
- src/Language/Fixpoint/SmtLib2.hs +42/−13
- src/Language/Fixpoint/Sort.hs +42/−12
- src/Language/Fixpoint/Types.hs +1/−1
- src/Language/Fixpoint/Visitor.hs +127/−0
Fixpoint.hs view
@@ -38,7 +38,7 @@ &= verbosity &= program "fixpoint" &= help "Predicate Abstraction Based Horn-Clause Solver" - &= summary "fixpoint © Copyright 2009-13 Regents of the University of California." + &= summary "fixpoint Copyright 2009-13 Regents of the University of California." &= details [ "Predicate Abstraction Based Horn-Clause Solver" , "" , "To check a file foo.fq type:"@@ -50,7 +50,7 @@ putStrLn $ banner md return md -banner args = "Liquid-Fixpoint © Copyright 2009-13 Regents of the University of California.\n" +banner args = "Liquid-Fixpoint Copyright 2009-13 Regents of the University of California.\n" ++ "All Rights Reserved.\n" ---------------------------------------------------------------------------------
LICENSE view
@@ -1,4 +1,4 @@-Copyright (c) 2013, Ranjit Jhala+Copyright (c) 2013-2014, Ranjit Jhala All rights reserved.
Setup.hs view
@@ -4,37 +4,49 @@ import Distribution.Simple import Distribution.Simple.LocalBuildInfo import Distribution.Simple.Setup-import System.Posix.Env-import System.Process+import Distribution.System+import System.Directory+import System.Environment import System.Exit+import System.FilePath+import System.Process -main = defaultMainWithHooks fixHooks+main = defaultMainWithHooks fixHooks where- fixHooks = simpleUserHooks { postBuild = buildFixpoint- , postCopy = copyFixpoint- , postInst = copyFixpoint- }+ fixHooks = simpleUserHooks { postBuild = buildFixpoint+ , postCopy = copyFixpoint+ , postInst = copyFixpoint+ } -buildFixpoint _ _ pkg lbi- = do setEnv "Z3MEM" (show z3mem) True- executeShellCommand "./configure"- executeShellCommand "./build.sh"- executeShellCommand "chmod a+x external/fixpoint/fixpoint.native "+copyFixpoint _ _ pkg lbi = do+ copyFile fixpoint bin where- allDirs = absoluteInstallDirs pkg lbi NoCopyDest- binDir = bindir allDirs ++ "/"- flags = configConfigurationsFlags $ configFlags lbi- z3mem = fromMaybe False $ lookup (FlagName "z3mem") flags+ allDirs = absoluteInstallDirs pkg lbi NoCopyDest+ bin = bindir allDirs </> "fixpoint.native"+ ++ if system == "i686-w64-mingw32" then ".exe" else ""+ fixpoint = "external" </> "fixpoint" </> "fixpoint.native"+ ++ if build then "" else "-" ++ system+ system = case hostPlatform lbi of+ Platform I386 Linux -> "i386-linux"+ Platform X86_64 Linux -> "x86_64-linux"+ Platform X86_64 OSX -> "x86_64-darwin"+ Platform _ Windows -> "i686-w64-mingw32"+ _ -> error "We don't have a prebuilt fixpoint.native for your system, please install with -fbuild-external (requires ocaml)"+ flags = configConfigurationsFlags $ configFlags lbi+ build = fromMaybe False $ lookup (FlagName "build-external") flags -copyFixpoint _ _ pkg lbi- = do executeShellCommand $ "cp external/fixpoint/fixpoint.native " ++ binDir- when z3mem $- executeShellCommand $ "cp external/z3/lib/libz3.* " ++ binDir++buildFixpoint _ _ pkg lbi = when build $ do+ setEnv "Z3MEM" (show z3mem)+ executeShellCommand "./configure"+ executeShellCommand "./build.sh"+ executeShellCommand "chmod a+x external/fixpoint/fixpoint.native " where- allDirs = absoluteInstallDirs pkg lbi NoCopyDest- binDir = bindir allDirs ++ "/"- flags = configConfigurationsFlags $ configFlags lbi- z3mem = fromMaybe False $ lookup (FlagName "z3mem") flags+ allDirs = absoluteInstallDirs pkg lbi NoCopyDest+ binDir = bindir allDirs ++ "/"+ flags = configConfigurationsFlags $ configFlags lbi+ z3mem = fromMaybe False $ lookup (FlagName "z3mem") flags+ build = fromMaybe False $ lookup (FlagName "build-external") flags executeShellCommand cmd = putStrLn ("EXEC: " ++ cmd) >> system cmd >>= check where
external/fixpoint/Makefile view
@@ -5,7 +5,7 @@ LIBS_=-libs unix,str,graph IFLAGS_=-lflags -I,$(OCAMLGRAPHHOME)-LFLAGS_=-lflags -cclib,-L$(OCAMLLIB) \+LFLAGS_=-lflags -cclib,-L$(OCAMLLIB) CFLAGS_=-cflags -dtypes,-annot \ -cflags -I,$(OCAMLGRAPHHOME) \
external/fixpoint/ast.ml view
@@ -1133,6 +1133,19 @@ | Sort.Lvar _ -> None | Sort.LFun -> None +let uf_arity f uf = + match sortcheck_sym f uf with None -> None | Some t -> + match Sort.func_of_t t with None -> None | Some (i,_,_) -> + Some i+ +let solved_app f uf = function+ | Some (s, t) -> begin match uf_arity f uf with+ | Some n -> if Sort.check_arity n s then Some t else None+ | _ -> None+ end + | None -> None++ let rec sortcheck_expr g f e = match euw e with | Bot -> @@ -1202,7 +1215,6 @@ *) - and sortcheck_op g f (e1, op, e2) = (* DEBUGGING let (s1, s2) = Misc.map_pair (sortcheck_expr g f) (e1, e2) in @@ -1295,6 +1307,16 @@ | Some tx -> not (None = sortcheck_app g f (Some tx) uf es) end + | Atom (((App (uf1, e1s), _) as e1), Eq, ((App (uf2, e2s), _) as e2))+ -> let t1o = solved_app f uf1 <| sortcheck_app_sub g f None uf1 e1s in+ let t2o = solved_app f uf2 <| sortcheck_app_sub g f None uf2 e2s in+ begin match t1o, t2o with+ | (Some t1, Some t2) -> t1 = t2+ | (None, None) -> false + | (None, Some t2) -> not (None = sortcheck_app g f (Some t2) uf1 e1s)+ | (Some t1, None) -> not (None = sortcheck_app g f (Some t1) uf2 e2s) + end+ | Atom (e1, r, e2) -> sortcheck_rel g f (e1, r, e2) | Forall (qs,p) ->@@ -1308,19 +1330,31 @@ >> (fun b -> if not b then F.eprintf "WARNING: Malformed Lhs Pred (%a)\n" Predicate.print p) *) -let uf_arity f uf = - match sortcheck_sym f uf with None -> None | Some t -> - match Sort.func_of_t t with None -> None | Some (i,_,_) -> - Some i- +let opt_to_string p = function+ | None -> "none"+ | Some x -> p x++ (* API *)-let sortcheck_app g f t uf es = - match uf_arity f uf, sortcheck_app_sub g f t uf es with - | (Some n , Some (s, t)) -> - if Sort.check_arity n s then Some (s, t) else- assertf "Ast.sortcheck_app: type args not fully instantiated %s" - (expr_to_string (eApp (uf, es)))+let sortcheck_app g f tExp uf es = + match uf_arity f uf, sortcheck_app_sub g f tExp uf es with + | (Some n, Some (s, t)) -> + if Sort.check_arity n s then + Some (s, t) + else+ None+ (*+ let msg = Printf.sprintf "Ast.sortcheck_app: type params not instantiated %s: n = %d, s = %s, t = %s, tExp = %s"+ (expr_to_string (eApp (uf, es)))+ n+ (Sort.sub_to_string s)+ (Sort.to_string t) + (opt_to_string Sort.to_string tExp)+ in+ assertf "%s" msg+ *) | _ -> None+ (* let sortcheck_pred f p =
external/fixpoint/fixParse.mly view
@@ -232,15 +232,15 @@ ; pred:- TRUE { A.pTrue }- | FALSE { A.pFalse }+ TRUE { A.pTrue }+ | FALSE { A.pFalse } | BEXP expr { A.pBexp $2 } | QM expr { A.pBexp $2 } | Id LPAREN argsne RPAREN { A.pBexp (A.eApp ((Sy.of_string $1), $3)) }- | AND preds { A.pAnd ($2) }- | OR preds { A.pOr ($2) }- | NOT pred { A.pNot ($2) }- | NOTWORD pred { A.pNot ($2) }+ | AND preds { A.pAnd ($2) }+ | OR preds { A.pOr ($2) }+ | NOT pred { A.pNot ($2) }+ | NOTWORD pred { A.pNot ($2) } | LPAREN pred AND pred RPAREN { A.pAnd [$2; $4] } | LPAREN pred OR pred RPAREN { A.pOr [$2; $4] } | expr rel expr { A.pAtom ($1, $2, $3) }@@ -249,7 +249,7 @@ | pred IMPL pred { A.pImp ($1, $3) } | pred IFF pred { A.pIff ($1, $3) } | pred IFFWORD pred { A.pIff ($1, $3) }- | LPAREN pred RPAREN { $2 }+ | LPAREN pred RPAREN { $2 } ; argsne:
+ external/fixpoint/fixpoint.native-i386-linux view
binary file changed (absent → 1567816 bytes)
+ external/fixpoint/fixpoint.native-i686-w64-mingw32 view
binary file changed (absent → 2072766 bytes)
+ external/fixpoint/fixpoint.native-x86_64-darwin view
file too large to diff
+ external/fixpoint/fixpoint.native-x86_64-linux view
file too large to diff
+ external/fixpoint/foo.ml view
@@ -0,0 +1,6 @@+let main ()+ = let co,ci = Unix.open_process "cvc4 --print-success --incremental" in+ output_string ci "QUERY TRUE;\n";+ let r = input_line co in+ print_endline r+let _ = main ()
external/fixpoint/smtLIB2.ml view
@@ -95,8 +95,8 @@ (*********************** Set Theory ********************************) (*******************************************************************) -let elt = "Elt"-let set = "Set"+let elt = "SMT_Elt"+let set = "SMT_Set" let emp = "smt_set_emp" let add = "smt_set_add" let cup = "smt_set_cup"@@ -117,9 +117,15 @@ (define-fun smt_set_sub ((s1 Set) (s2 Set)) Bool (= smt_set_emp (smt_set_dif s1 s2))) *) +let (++) = List.append+ (* z3 specific *) let z3_preamble _ - = if not !Co.set_theory then [] else+ = [ "(set-option :auto-config false)"+ ; "(set-option :model true)"+ ; "(set-option :model.partial false)"+ ; "(set-option :smt.mbqi false)"+ ] ++ if not !Co.set_theory then [] else [ spr "(define-sort %s () Int)" elt ; spr "(define-sort %s () (Array %s Bool))" @@ -142,6 +148,36 @@ sub set set emp dif ] +(* cvc4 specific *)+let cvc4_preamble _ + = if not !Co.set_theory then [] else+ [ spr "(set-logic QF_UFNIRAFS)"+ ; spr "(define-sort %s () Int)"+ elt+ ; spr "(define-sort %s () (Set %s))" + set elt+ ; spr "(define-fun %s () %s (as emptyset (Set %s)))"+ emp set elt+ ; spr "(define-fun %s ((x %s) (s %s)) Bool (member x s))"+ mem elt set+ ; spr "(define-fun %s ((s %s) (x %s)) %s (insert x s))"+ add set elt set+ ; spr "(define-fun %s ((s1 %s) (s2 %s)) %s (union s1 s2))"+ cup set set set+ ; spr "(define-fun %s ((s1 %s) (s2 %s)) %s (intersection s1 s2))"+ 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+ ] + let smtlib_preamble = [ spr "(set-logic QF_UFLIA)" ; spr "(define-sort %s () Int)" elt@@ -198,6 +234,7 @@ let smt_preamble = function | Z3 -> z3_preamble ()+ | Cvc4 -> cvc4_preamble () | _ -> smtlib_preamble @@ -205,8 +242,30 @@ output_now me.clog s; output_now me.cout s +(* copied from String.trim in ocaml-4.0 since mingw-ocaml uses 3.x *)+let trim s =+ let is_space = function+ | ' ' | '\012' | '\n' | '\r' | '\t' -> true+ | _ -> false in+ let len = String.length s in+ let i = ref 0 in+ while !i < len && is_space (String.get s !i) do+ incr i+ done;+ let j = ref (len - 1) in+ while !j >= !i && is_space (String.get s !j) do+ decr j+ done;+ if !i = 0 && !j = len - 1 then+ s+ else if !j >= !i then+ String.sub s !i (!j - !i + 1)+ else+ ""++(* strip off trailing whitespace, e.g. \r on windows.. *) let smt_read_raw me = - input_line me.cin+ trim (input_line me.cin) let smt_write me ?nl:(nl=true) ?tab:(tab=false) s = let pre = if tab then " " else "" in@@ -320,8 +379,10 @@ let mkRealSort _ = "Real" let mkBoolSort _ = "Bool" -let mkInt _ i _ = string_of_int i-let mkReal _ i _ = string_of_float i+let mkInt _ i _ = if i >= 0 then string_of_int i+ 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 mkTrue _ = "true" let mkFalse _ = "false"
− external/fixpoint/smtZ3.ml
@@ -1,84 +0,0 @@-(*- * 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 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 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 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
external/fixpoint/theories.ml view
@@ -33,6 +33,9 @@ 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)] )+ let emp = ( Sy.of_string "Set_emp" , So.t_func 1 [t_set (So.t_generic 0); So.t_bool] ) @@ -57,7 +60,7 @@ let interp_syms _ = if !Constants.set_theory - then [emp; sng; mem; cup; cap; dif; sub]+ then [emp0; emp; sng; mem; cup; cap; dif; sub] else [] module MakeTheory(SMT : SMTSOLVER): @@ -98,6 +101,17 @@ | _ -> assertf "Set_set: type mismatch" } ++let set_empty : appDef = + { sy_name = fst emp0+ ; sy_sort = snd emp0 + ; sy_emb = fun c ts es -> match ts, es with+ | [t], [_] -> SMT.mkEmptySet c t+ | _ -> assertf "Set_empty: type mismatch"+ }+++ let set_emp : appDef = { sy_name = fst emp ; sy_sort = snd emp @@ -189,6 +203,7 @@ (* API *) let theories = ([set_set], [set_emp; + set_empty; set_sng; set_mem; set_cup;
external/fixpoint/tpGen.ml view
@@ -187,9 +187,23 @@ (********************** Pred/Expr Transl ******************************) (**********************************************************************) +let opt_to_string p = function+ | None -> "none"+ | Some x -> p x exception Z3RelTypeError +let pred_sort env p = + A.sortcheck_pred Theories.is_interp (Misc.flip SM.maybe_find env) p ++let app_sort env tyo f es =+ A.sortcheck_app Theories.is_interp (Misc.flip SM.maybe_find env) tyo f es++let expr_sort env = function+ | A.App (f, es), _ -> Misc.maybe_map snd <| app_sort env None f es + | e -> A.sortcheck_expr Theories.is_interp (Misc.flip SM.maybe_find env) e++ let z3Bind me env x t = let vx = Vbl (x, varSort env x) in me.bnd <- me.bnd + 1; @@ -198,12 +212,15 @@ SMT.stringSymbol me.c (fresh "z3b") let rec z3Rel me env (e1, r, e2) =- let p = A.pAtom (e1, r, e2) in- let ok = A.sortcheck_pred Theories.is_interp (Misc.flip SM.maybe_find env) p in + let p = A.pAtom (e1, r, e2) in+ let ok = pred_sort env p in (* let _ = F.printf "z3Rel: e = %a, res = %b \n" P.print p ok in let _ = F.print_flush () in *)+ if ok then - SMT.mkRel me.c r (z3Exp me env e1) (z3Exp me env e2)+ z3Rel_cast me env (e1, r, e2)+ (* z3Rel_real me env (e1, r, e2) *)+ (* SMT.mkRel me.c r (z3Exp me env e1) (z3Exp me env e2) *) else begin SM.iter (fun s t -> F.printf "@[%a :: %a@]@." Sy.print s So.print t) env; F.printf "@[%a@]@.@." P.print (A.pAtom (e1, r, e2));@@ -211,13 +228,38 @@ raise Z3RelTypeError end ++++and z3Rel_cast me env = function+ | (e1, A.Eq, e2) -> begin+ let (t1o, t2o) = (expr_sort env e1, expr_sort env e2) in + (* let _ = F.printf "z3Rel_cast: t1o = %s, t2o = %s \n" + (opt_to_string So.to_string t1o) (opt_to_string So.to_string t2o) in+ *)+ match (t1o, t2o) with+ | (Some t , None ) -> z3Rel_real me env (e1, A.Eq, A.eCst (e2, t)) + | (None , Some t) -> z3Rel_real me env (A.eCst (e1, t), A.Eq, e2)+ | (_ , _ ) -> z3Rel_real me env (e1, A.Eq, e2) + end+ | (e1, r, e2) -> + z3Rel_real me env (e1, r, e2) ++and z3Rel_real me env (e1, r, e2) =+ (* let _ = F.printf "z3Rel_real: e1 = %s, e2 = %s \n"+ (E.to_string e1)+ (E.to_string e2) in+ *)+ SMT.mkRel me.c r (z3Exp me env e1) (z3Exp me env e2)+ and z3App me env p zes = let t = funSort env p in let cf = z3Fun me env p t (List.length zes) in SMT.mkApp me.c cf zes and z3AppThy me env def tyo f es = - match A.sortcheck_app Theories.is_interp (Misc.flip SM.maybe_find env) tyo f es with + (* match A.sortcheck_app Theories.is_interp (Misc.flip SM.maybe_find env) tyo f es with *)+ match app_sort env tyo f es with | Some (s, t) -> let zts = So.sub_args s |> List.map (snd <+> z3Type me) in let zes = es |> List.map (z3Exp me env) in@@ -299,10 +341,9 @@ | A.Bexp e, _ -> let a = z3Exp me env e in let s2 = E.to_string e in- let so = match A.sortcheck_expr Theories.is_interp (Misc.flip SM.maybe_find env) e with - | Some so -> so- | _ -> F.printf "No type for %s" (E.to_string e);- assert false in+ let so = match expr_sort env e with Some so -> so+ | _ -> F.printf "No type for %s" (E.to_string e);+ assert false in let sos = So.to_string so in (* let s1 = SMT.astString me.c a in let _ = asserts (SMT.isBool me.c a)
− external/ocamlgraph/META
@@ -1,5 +0,0 @@-version = "0.99b"-description = "Generic Graph Library"-requires=""-archive(byte) = "graph.cma"-archive(native) = "graph.cmxa"
− external/ocamlgraph/Makefile
@@ -1,386 +0,0 @@-##########################################################################-# #-# Ocamlgraph: a generic graph library for OCaml #-# Copyright (C) 2004-2007 #-# Sylvain Conchon, Jean-Christophe Filliatre and Julien Signoles #-# #-# This software is free software; you can redistribute it and/or #-# modify it under the terms of the GNU Library General Public #-# License version 2, with the special exception on linking #-# described in file LICENSE. #-# #-# This software is distributed in the hope that it will be useful, #-# but WITHOUT ANY WARRANTY; without even the implied warranty of #-# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. #-# #-##########################################################################--# Where to install the binaries-prefix=/usr/local-exec_prefix=${prefix}-BINDIR=${exec_prefix}/bin--# Where to install the man page-MANDIR=${prefix}/share/man--# Other variables set by ./configure-OCAMLC = ocamlc.opt-OCAMLOPT = ocamlopt.opt-OCAMLDEP = ocamldep-OCAMLDOC = ocamldoc.opt-OCAMLLEX = ocamllex.opt-OCAMLYACC= ocamlyacc-OCAMLLIB = /nix/store/547bsyhad0whqa62qkji1q0pfy5lm0qx-ocaml-4.01.0/lib/ocaml-OCAMLBEST= opt-OCAMLVERSION = 4.01.0-OCAMLWEB = true-OCAMLWIN32 = no-OCAMLFIND = -EXE = -LIBEXT = .a-OBJEXT = .o--# Others global variables-SRCDIR = src-LIBDIR = lib--INCLUDES= -I $(SRCDIR) -I $(LIBDIR) -BFLAGS = $(INCLUDES)-OFLAGS = $(INCLUDES) -for-pack Graph--# main target-#############--NAME=ocamlgraph--all: byte $(OCAMLBEST)-#all: byte $(OCAMLBEST) editor-no--# bytecode and native-code compilation-######################################--LIB= unionfind heap bitv-LIB:=$(patsubst %, $(LIBDIR)/%.cmo, $(LIB))--CMO = util blocks persistent imperative \- delaunay builder classic rand oper \- gpath traverse gcoloring topological components kruskal flow \- graphviz gml dot_parser dot_lexer dot pack \- gmap minsep cliquetree mcs_m md strat-CMO := $(LIB) $(patsubst %, $(SRCDIR)/%.cmo, $(CMO))--CMX = $(CMO:.cmo=.cmx)-CMA = graph.cma-CMXA = graph.cmxa--CMI = sig dot_ast sig_pack-CMI := $(patsubst %, src/%.cmi, $(CMI))--GENERATED = META \- src/gml.ml src/version.ml \- src/dot_parser.ml src/dot_parser.mli src/dot_lexer.ml--byte: $(CMA)-opt: $(CMXA)--graph.cma: graph.cmo- $(OCAMLC) $(INCLUDES) -a -o $@ $^--graph.cmxa: graph.cmx- $(OCAMLOPT) $(INCLUDES) -a -o $@ $^--graph.cmo: $(CMI) $(CMO)- $(OCAMLC) $(INCLUDES) -pack -o $@ $^--graph.cmx: $(CMI) $(CMX)- $(OCAMLOPT) $(INCLUDES) -pack -o $@ $^--EXAMPLESBIN=bin/demo.$(OCAMLBEST) bin/demo_planar.$(OCAMLBEST) \- bin/bench.$(OCAMLBEST) bin/color.$(OCAMLBEST) bin/sudoku.$(OCAMLBEST) \- bin/test.$(OCAMLBEST) --.PHONY: examples-examples: $(EXAMPLESBIN)--.PHONY: demo-demo: bin/demo.$(OCAMLBEST)--bin/demo.byte: $(CMA) examples/demo.cmo- $(OCAMLC) -o $@ $^--bin/demo.opt: $(CMXA) examples/demo.cmx- $(OCAMLOPT) -o $@ $^--bin/demo_planar.byte: $(CMA) examples/demo_planar.cmo- $(OCAMLC) -o $@ graphics.cma unix.cma $^--bin/demo_planar.opt: $(CMXA) examples/demo_planar.cmx- $(OCAMLOPT) -o $@ graphics.cmxa unix.cmxa $^--bin/color.byte: $(CMA) examples/color.cmo- $(OCAMLC) -o $@ graphics.cma unix.cma $^--bin/color.opt: $(CMXA) examples/color.cmx- $(OCAMLOPT) -o $@ graphics.cmxa unix.cmxa $^--bin/sudoku.byte: $(CMA) examples/sudoku.cmo- $(OCAMLC) -o $@ graphics.cma unix.cma $^--bin/sudoku.opt: $(CMXA) examples/sudoku.cmx- $(OCAMLOPT) -o $@ graphics.cmxa unix.cmxa $^--test: $(CMA) tests/test.ml- ocaml unix.cma graphics.cma $^--bin/test.byte: $(CMA) tests/test.cmo- $(OCAMLC) -g -unsafe -o $@ unix.cma graphics.cma $^--bin/test.opt: $(CMXA) tests/test.cmx- $(OCAMLOPT) -unsafe -inline 100 -o $@ unix.cmxa graphics.cmxa $^--bench: bin/bench.$(OCAMLBEST)- bin/bench.opt--bin/bench.opt: $(CMXA) tests/bench.ml- $(OCAMLOPT) -unsafe -inline 100 -o $@ unix.cmxa $^--check: $(CMA) tests/check.ml- ocaml $^--# gtk2 graph editor--ED_DIR=editor--editor-no:-editor-yes: $(ED_DIR)/editor.$(OCAMLBEST)--editor: $(ED_DIR)/editor.byte editor-yes--ED_CMO = ed_hyper ed_graph ed_draw ed_display ed_main-ED_CMO:= $(patsubst %, $(ED_DIR)/%.cmo, $(ED_CMO))-ED_CMX = $(ED_CMO:.cmo=.cmx)--ED_INCLUDES = -I +threads -I $(ED_DIR)--$(ED_CMO): BFLAGS+= $(ED_INCLUDES)-$(ED_CMX): OFLAGS+= $(ED_INCLUDES)--$(ED_DIR)/editor.byte: $(CMA) $(ED_CMO)- $(OCAMLC) -g -o $@ \- lablgtk.cma lablgnomecanvas.cma unix.cma $^--$(ED_DIR)/editor.opt: $(CMXA) $(ED_CMX)- $(OCAMLOPT) -o $@ \- lablgtk.cmxa lablgnomecanvas.cmxa unix.cmxa $^--VERSION=0.99b--src/version.ml: Makefile- echo "let version = \""$(VERSION)"\"" > $@- echo "let date = \""`date`"\"" >> $@--META: META.in Makefile- sed -e s/VERSION/$(VERSION)/ -e s/CMA/$(CMA)/ -e s/CMXA/$(CMXA)/ \- $@.in > $@--# Additional rules-##################--EXAMPLES = demo color demo_planar sudoku-EXAMPLES:= $(patsubst %, examples/%.ml, $(EXAMPLES))--TESTS = test check-TESTS := $(patsubst %, tests/%.ml, $(TESTS))--DPD_GRAPH_ML= $(TESTS) $(EXAMPLES)--$(DPD_GRAPH_ML:.ml=.cmo): $(CMA)-$(DPD_GRAPH_ML:.ml=.cmx): $(CMXA)--# installation-##############--install: install-$(OCAMLBEST) install-byte--install-byte: - cp -f graph.cmo graph.cmi $(CMA) "$(OCAMLLIB)"--install-opt: install-byte- cp -f graph$(LIBEXT) graph.cmx $(CMXA) "$(OCAMLLIB)"--install-findlib: META-ifdef OCAMLFIND- $(OCAMLFIND) install ocamlgraph META *.mli \- graph$(LIBEXT) graph.cmx graph.cmo graph.cmi $(CMA) $(CMXA)-endif--# documentation-###############--DOCFILES=$(NAME).ps $(NAME).html--NODOC = util blocks dot_parser dot_lexer-NODOC := $(patsubst %, $(SRCDIR)/%.cmo, $(NODOC))-DOC_CMO = $(filter-out $(NODOC) $(LIB), $(CMO))-DOC_SRC = $(CMI:.cmi=.mli) $(DOC_CMO:.cmo=.mli) $(DOC_CMO:.cmo=.ml)--.PHONY: doc-doc: $(DOC_CMO)- mkdir -p doc- rm -f doc/*- $(OCAMLDOC) -d doc -html $(INCLUDES) $(DOC_SRC)--# literate programming-$(NAME).tex: $(DOC_SRC)- $(OCAMLWEB) -o $@ $^--wc:- ocamlwc -p $(SRCDIRC)/*.mli $(SRCDIRC)/*.ml--# file headers-##############-headers:- headache -c misc/headache_config.txt -h misc/header.txt \- Makefile.in configure.in README \- $(LIBDIR)*.ml $(LIBDIR)*.ml[ily] \- $(SRCDIR)*.ml $(SRCDIR)*.ml[ily] \- $(ED_DIR)/*.ml $(ED_DIR)/*.mli \--# export-########--EXPORTDIR=$(NAME)-$(VERSION)-TAR=$(EXPORTDIR).tar--FTP = $$HOME/ftp/$(NAME)-WWW = $$HOME/WWW/$(NAME)--FILES = src/*.ml* lib/*.ml* Makefile.in configure configure.in META.in \- .depend editor/ed_*.ml* editor/Makefile \- editor/tests/*.dot editor/tests/*.gml \- examples/*.ml tests/*.ml \- .depend README FAQ CREDITS INSTALL COPYING LICENSE CHANGES--export: source export-doc export-web export-delaunay--source: - mkdir -p export- cd export; rm -rf $(EXPORTDIR)- mkdir -p export/$(EXPORTDIR)/bin- cp --parents $(FILES) export/$(EXPORTDIR)- cd export ; tar cf $(TAR) $(EXPORTDIR) ; gzip -f --best $(TAR)- cp export/$(TAR).gz $(FTP)- cp README FAQ CREDITS COPYING LICENSE CHANGES $(EXAMPLES) $(FTP)--www/version.prehtml: Makefile.in- echo "<#def version>$(VERSION)</#def>" > www/version.prehtml--export-web: www/version.prehtml- make -C www install--export-doc: $(DOC_CMO)- rm -f $(WWW)/doc/*- -$(OCAMLDOC) -d $(WWW)/doc -html $(INCLUDES) $(DOC_SRC)--MISCFTP = $(HOME)/WWW/ftp/ocaml/misc-DELAUNAY=delaunay.ml delaunay.mli-export-delaunay:- cd src; cp -f $(DELAUNAY) $(MISCFTP)- cd src; caml2html -d $(MISCFTP) $(DELAUNAY)--# generic rules-###############--.SUFFIXES: .mli .ml .cmi .cmo .cmx .mll .mly .tex .dvi .ps .html--.mli.cmi:- $(OCAMLC) -c $(BFLAGS) $<--.ml.cmo:- $(OCAMLC) -c $(BFLAGS) $<--.ml.o:- $(OCAMLOPT) -c $(OFLAGS) $<--.ml.cmx:- $(OCAMLOPT) -c $(OFLAGS) $<--.mll.ml:- $(OCAMLLEX) $<--.mly.ml:- $(OCAMLYACC) -v $<--.mly.mli:- $(OCAMLYACC) -v $<--.tex.dvi:- latex $< && latex $<--.dvi.ps:- dvips $< -o $@ --.tex.html:- hevea $<--# Emacs tags-############--otags:- otags -r src editor--tags:- find . -name "*.ml*" | sort -r | xargs \- etags "--regex=/let[ \t]+\([^ \t]+\)/\1/" \- "--regex=/let[ \t]+rec[ \t]+\([^ \t]+\)/\1/" \- "--regex=/and[ \t]+\([^ \t]+\)/\1/" \- "--regex=/type[ \t]+\([^ \t]+\)/\1/" \- "--regex=/exception[ \t]+\([^ \t]+\)/\1/" \- "--regex=/val[ \t]+\([^ \t]+\)/\1/" \- "--regex=/module[ \t]+\([^ \t]+\)/\1/"--# Makefile is rebuilt whenever Makefile.in or configure.in is modified-######################################################################--Makefile: Makefile.in config.status- if test -e $@; then chmod a+w $@; fi - ./config.status- chmod a-w $@--config.status: configure- ./config.status --recheck--configure: configure.in- autoconf --# clean-#######--clean:- rm -f *~- for d in $(SRCDIR) $(LIBDIR) $(ED_DIR) tests examples; do \- rm -f $$d/*.cm[iox] $$d/*$(OBJEXT) $$d/*~; \- done- rm -f $(GENERATED) $(SRCDIR)/dot_parser.output- rm -f graph.*a graph$(LIBEXT) bin/$(NAME).byte bin/$(NAME).opt- rm -f *.haux *.aux *.log $(NAME).tex $(NAME).dvi $(DOCFILES)- rm -f $(EXAMPLESBIN)--dist-clean distclean:: clean- rm -f Makefile config.cache config.log config.status *.byte *.opt--svnclean svn-clean:: dist-clean- rm -f config.* configure configure.lineno--# depend-########--.PHONY: depend-.depend depend: $(GENERATED)- rm -f .depend- $(OCAMLDEP) $(INCLUDES) \- $(LIBDIR)/*.ml $(LIBDIR)/*.mli \- $(SRCDIR)/*.ml $(SRCDIR)/*.mli \- $(ED_DIR)/*.mli $(ED_DIR)/*.ml > .depend--include .depend
− external/ocamlgraph/src/dot_lexer.ml
@@ -1,386 +0,0 @@-# 20 "src/dot_lexer.mll"- - open Lexing- open Dot_ast- open Dot_parser-- let string_buf = Buffer.create 1024-- let keyword =- let h = Hashtbl.create 17 in- List.iter - (fun (s,k) -> Hashtbl.add h s k)- [- "strict", STRICT;- "graph", GRAPH;- "digraph", DIGRAPH;- "subgraph", SUBGRAPH;- "node", NODE;- "edge", EDGE;- ];- fun s -> let s = String.lowercase s in Hashtbl.find h s---# 25 "src/dot_lexer.ml"-let __ocaml_lex_tables = {- Lexing.lex_base = - "\000\000\238\255\239\255\240\255\241\255\078\000\088\000\098\000\- \176\000\245\255\246\255\247\255\248\255\249\255\250\255\251\255\- \252\255\114\000\001\000\005\000\254\255\002\000\253\255\191\000\- \244\255\211\000\221\000\157\000\252\255\253\255\002\000\255\255\- \254\255\032\000\252\255\253\255\254\255\255\255\054\000\253\255\- \254\255\015\000\255\255";- Lexing.lex_backtrk = - "\255\255\255\255\255\255\255\255\255\255\013\000\017\000\012\000\- \017\000\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\017\000\017\000\000\000\255\255\255\255\255\255\255\255\- \255\255\013\000\013\000\255\255\255\255\255\255\002\000\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\001\000\255\255";- Lexing.lex_default = - "\001\000\000\000\000\000\000\000\000\000\255\255\255\255\255\255\- \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\255\255\021\000\255\255\000\000\021\000\000\000\255\255\- \000\000\255\255\255\255\029\000\000\000\000\000\255\255\000\000\- \000\000\035\000\000\000\000\000\000\000\000\000\040\000\000\000\- \000\000\255\255\000\000";- Lexing.lex_trans = - "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\019\000\019\000\020\000\020\000\019\000\019\000\019\000\- \000\000\000\000\019\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \019\000\000\000\004\000\018\000\032\000\019\000\000\000\000\000\- \000\000\000\000\000\000\000\000\015\000\008\000\006\000\017\000\- \005\000\005\000\005\000\005\000\005\000\005\000\005\000\005\000\- \005\000\005\000\016\000\014\000\003\000\013\000\042\000\000\000\- \000\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\010\000\036\000\009\000\037\000\007\000\- \041\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\012\000\026\000\011\000\005\000\005\000\- \005\000\005\000\005\000\005\000\005\000\005\000\005\000\005\000\- \025\000\025\000\025\000\025\000\025\000\025\000\025\000\025\000\- \025\000\025\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\007\000\022\000\000\000\000\000\000\000\- \000\000\021\000\000\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\007\000\007\000\000\000\000\000\031\000\- \000\000\007\000\000\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\007\000\007\000\024\000\023\000\000\000\- \005\000\005\000\005\000\005\000\005\000\005\000\005\000\005\000\- \005\000\005\000\000\000\000\000\000\000\000\000\024\000\025\000\- \025\000\025\000\025\000\025\000\025\000\025\000\025\000\025\000\- \025\000\030\000\000\000\000\000\000\000\000\000\000\000\000\000\- \002\000\255\255\255\255\025\000\025\000\025\000\025\000\025\000\- \025\000\025\000\025\000\025\000\025\000\026\000\026\000\026\000\- \026\000\026\000\026\000\026\000\026\000\026\000\026\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \034\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\039\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\028\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000";- Lexing.lex_check = - "\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\000\000\000\000\018\000\021\000\000\000\019\000\019\000\- \255\255\255\255\019\000\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \000\000\255\255\000\000\000\000\030\000\019\000\255\255\255\255\- \255\255\255\255\255\255\255\255\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\041\000\255\255\- \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\033\000\000\000\033\000\000\000\- \038\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\005\000\000\000\005\000\005\000\- \005\000\005\000\005\000\005\000\005\000\005\000\005\000\005\000\- \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\- \006\000\006\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\007\000\017\000\255\255\255\255\255\255\- \255\255\017\000\255\255\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\007\000\007\000\255\255\255\255\027\000\- \255\255\007\000\255\255\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\007\000\007\000\008\000\008\000\255\255\- \008\000\008\000\008\000\008\000\008\000\008\000\008\000\008\000\- \008\000\008\000\255\255\255\255\255\255\255\255\008\000\023\000\- \023\000\023\000\023\000\023\000\023\000\023\000\023\000\023\000\- \023\000\027\000\255\255\255\255\255\255\255\255\255\255\255\255\- \000\000\018\000\021\000\025\000\025\000\025\000\025\000\025\000\- \025\000\025\000\025\000\025\000\025\000\026\000\026\000\026\000\- \026\000\026\000\026\000\026\000\026\000\026\000\026\000\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \033\000\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\038\000\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\027\000\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255";- Lexing.lex_base_code = - "";- Lexing.lex_backtrk_code = - "";- Lexing.lex_default_code = - "";- Lexing.lex_trans_code = - "";- Lexing.lex_check_code = - "";- Lexing.lex_code = - "";-}--let rec token lexbuf =- __ocaml_lex_token_rec lexbuf 0-and __ocaml_lex_token_rec lexbuf __ocaml_lex_state =- match Lexing.engine __ocaml_lex_tables __ocaml_lex_state lexbuf with- | 0 ->-# 52 "src/dot_lexer.mll"- ( token lexbuf )-# 191 "src/dot_lexer.ml"-- | 1 ->-# 54 "src/dot_lexer.mll"- ( token lexbuf )-# 196 "src/dot_lexer.ml"-- | 2 ->-# 56 "src/dot_lexer.mll"- ( comment lexbuf; token lexbuf )-# 201 "src/dot_lexer.ml"-- | 3 ->-# 58 "src/dot_lexer.mll"- ( COLON )-# 206 "src/dot_lexer.ml"-- | 4 ->-# 60 "src/dot_lexer.mll"- ( COMMA )-# 211 "src/dot_lexer.ml"-- | 5 ->-# 62 "src/dot_lexer.mll"- ( SEMICOLON )-# 216 "src/dot_lexer.ml"-- | 6 ->-# 64 "src/dot_lexer.mll"- ( EQUAL )-# 221 "src/dot_lexer.ml"-- | 7 ->-# 66 "src/dot_lexer.mll"- ( LBRA )-# 226 "src/dot_lexer.ml"-- | 8 ->-# 68 "src/dot_lexer.mll"- ( RBRA )-# 231 "src/dot_lexer.ml"-- | 9 ->-# 70 "src/dot_lexer.mll"- ( LSQ )-# 236 "src/dot_lexer.ml"-- | 10 ->-# 72 "src/dot_lexer.mll"- ( RSQ )-# 241 "src/dot_lexer.ml"-- | 11 ->-# 74 "src/dot_lexer.mll"- ( EDGEOP )-# 246 "src/dot_lexer.ml"-- | 12 ->-let-# 75 "src/dot_lexer.mll"- s-# 252 "src/dot_lexer.ml"-= Lexing.sub_lexeme lexbuf lexbuf.Lexing.lex_start_pos lexbuf.Lexing.lex_curr_pos in-# 76 "src/dot_lexer.mll"- ( try keyword s with Not_found -> ID (Ident s) )-# 256 "src/dot_lexer.ml"-- | 13 ->-let-# 77 "src/dot_lexer.mll"- s-# 262 "src/dot_lexer.ml"-= Lexing.sub_lexeme lexbuf lexbuf.Lexing.lex_start_pos lexbuf.Lexing.lex_curr_pos in-# 78 "src/dot_lexer.mll"- ( ID (Number s) )-# 266 "src/dot_lexer.ml"-- | 14 ->-# 80 "src/dot_lexer.mll"- ( Buffer.clear string_buf; - let s = string lexbuf in- ID (String s) )-# 273 "src/dot_lexer.ml"-- | 15 ->-# 84 "src/dot_lexer.mll"- ( Buffer.clear string_buf; - html lexbuf; - ID (Html (Buffer.contents string_buf)) )-# 280 "src/dot_lexer.ml"-- | 16 ->-# 88 "src/dot_lexer.mll"- ( EOF )-# 285 "src/dot_lexer.ml"-- | 17 ->-let-# 89 "src/dot_lexer.mll"- c-# 291 "src/dot_lexer.ml"-= Lexing.sub_lexeme_char lexbuf lexbuf.Lexing.lex_start_pos in-# 90 "src/dot_lexer.mll"- ( failwith ("Dot_lexer: invalid character " ^ String.make 1 c) )-# 295 "src/dot_lexer.ml"-- | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_token_rec lexbuf __ocaml_lex_state--and string lexbuf =- __ocaml_lex_string_rec lexbuf 27-and __ocaml_lex_string_rec lexbuf __ocaml_lex_state =- match Lexing.engine __ocaml_lex_tables __ocaml_lex_state lexbuf with- | 0 ->-# 94 "src/dot_lexer.mll"- ( Buffer.contents string_buf )-# 306 "src/dot_lexer.ml"-- | 1 ->-# 96 "src/dot_lexer.mll"- ( Buffer.add_char string_buf '"';- string lexbuf )-# 312 "src/dot_lexer.ml"-- | 2 ->-let-# 98 "src/dot_lexer.mll"- c-# 318 "src/dot_lexer.ml"-= Lexing.sub_lexeme_char lexbuf lexbuf.Lexing.lex_start_pos in-# 99 "src/dot_lexer.mll"- ( Buffer.add_char string_buf c;- string lexbuf )-# 323 "src/dot_lexer.ml"-- | 3 ->-# 102 "src/dot_lexer.mll"- ( failwith ("Dot_lexer: unterminated string literal") )-# 328 "src/dot_lexer.ml"-- | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_string_rec lexbuf __ocaml_lex_state--and html lexbuf =- __ocaml_lex_html_rec lexbuf 33-and __ocaml_lex_html_rec lexbuf __ocaml_lex_state =- match Lexing.engine __ocaml_lex_tables __ocaml_lex_state lexbuf with- | 0 ->-# 106 "src/dot_lexer.mll"- ( () )-# 339 "src/dot_lexer.ml"-- | 1 ->-# 108 "src/dot_lexer.mll"- ( Buffer.add_char string_buf '<'; html lexbuf;- Buffer.add_char string_buf '>'; html lexbuf )-# 345 "src/dot_lexer.ml"-- | 2 ->-let-# 110 "src/dot_lexer.mll"- c-# 351 "src/dot_lexer.ml"-= Lexing.sub_lexeme_char lexbuf lexbuf.Lexing.lex_start_pos in-# 111 "src/dot_lexer.mll"- ( Buffer.add_char string_buf c;- html lexbuf )-# 356 "src/dot_lexer.ml"-- | 3 ->-# 114 "src/dot_lexer.mll"- ( failwith ("Dot_lexer: unterminated html literal") )-# 361 "src/dot_lexer.ml"-- | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_html_rec lexbuf __ocaml_lex_state--and comment lexbuf =- __ocaml_lex_comment_rec lexbuf 38-and __ocaml_lex_comment_rec lexbuf __ocaml_lex_state =- match Lexing.engine __ocaml_lex_tables __ocaml_lex_state lexbuf with- | 0 ->-# 118 "src/dot_lexer.mll"- ( () )-# 372 "src/dot_lexer.ml"-- | 1 ->-# 120 "src/dot_lexer.mll"- ( comment lexbuf )-# 377 "src/dot_lexer.ml"-- | 2 ->-# 122 "src/dot_lexer.mll"- ( failwith "Dot_lexer: unterminated comment" )-# 382 "src/dot_lexer.ml"-- | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_comment_rec lexbuf __ocaml_lex_state--;;-
− external/ocamlgraph/src/dot_parser.ml
@@ -1,552 +0,0 @@-type token =- | ID of (Dot_ast.id)- | COLON- | COMMA- | EQUAL- | SEMICOLON- | EDGEOP- | STRICT- | GRAPH- | DIGRAPH- | LBRA- | RBRA- | LSQ- | RSQ- | NODE- | EDGE- | SUBGRAPH- | EOF--open Parsing;;-let _ = parse_error;;-# 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"--# 38 "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 } )-# 200 "src/dot_parser.ml"- : Dot_ast.file))-; (fun __caml_parser_env ->- Obj.repr(-# 53 "src/dot_parser.mly"- ( false )-# 206 "src/dot_parser.ml"- : 'strict_opt))-; (fun __caml_parser_env ->- Obj.repr(-# 54 "src/dot_parser.mly"- ( true )-# 212 "src/dot_parser.ml"- : 'strict_opt))-; (fun __caml_parser_env ->- Obj.repr(-# 58 "src/dot_parser.mly"- ( false )-# 218 "src/dot_parser.ml"- : 'graph_or_digraph))-; (fun __caml_parser_env ->- Obj.repr(-# 59 "src/dot_parser.mly"- ( true )-# 224 "src/dot_parser.ml"- : 'graph_or_digraph))-; (fun __caml_parser_env ->- Obj.repr(-# 63 "src/dot_parser.mly"- ( [] )-# 230 "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 )-# 237 "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] )-# 245 "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 )-# 254 "src/dot_parser.ml"- : 'list1_stmt))-; (fun __caml_parser_env ->- Obj.repr(-# 73 "src/dot_parser.mly"- ( () )-# 260 "src/dot_parser.ml"- : 'semicolon_opt))-; (fun __caml_parser_env ->- Obj.repr(-# 74 "src/dot_parser.mly"- ( () )-# 266 "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 )-# 273 "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 )-# 280 "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 )-# 287 "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) )-# 295 "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 )-# 302 "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) )-# 310 "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) )-# 319 "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 )-# 326 "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 )-# 333 "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 )-# 340 "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 )-# 348 "src/dot_parser.ml"- : 'edge_rhs))-; (fun __caml_parser_env ->- Obj.repr(-# 104 "src/dot_parser.mly"- ( [] )-# 354 "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 )-# 362 "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 )-# 369 "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 )-# 376 "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 )-# 384 "src/dot_parser.ml"- : 'node_id))-; (fun __caml_parser_env ->- Obj.repr(-# 118 "src/dot_parser.mly"- ( None )-# 390 "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 )-# 397 "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) )-# 405 "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) )-# 416 "src/dot_parser.ml"- : 'port))-; (fun __caml_parser_env ->- Obj.repr(-# 133 "src/dot_parser.mly"- ( [] )-# 422 "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 )-# 429 "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] )-# 436 "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 )-# 444 "src/dot_parser.ml"- : 'attr_list))-; (fun __caml_parser_env ->- Obj.repr(-# 143 "src/dot_parser.mly"- ( None )-# 450 "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 )-# 457 "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] )-# 465 "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 )-# 474 "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 )-# 481 "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 )-# 489 "src/dot_parser.ml"- : 'equality))-; (fun __caml_parser_env ->- Obj.repr(-# 158 "src/dot_parser.mly"- ( () )-# 495 "src/dot_parser.ml"- : 'comma_opt))-; (fun __caml_parser_env ->- Obj.repr(-# 159 "src/dot_parser.mly"- ( () )-# 501 "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 )-# 508 "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) )-# 516 "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) )-# 523 "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) )-# 530 "src/dot_parser.ml"- : 'subgraph))-(* Entry file *)-; (fun __caml_parser_env -> raise (Parsing.YYexit (Parsing.peek_val __caml_parser_env 0)))-|]-let yytables =- { Parsing.actions=yyact;- Parsing.transl_const=yytransl_const;- Parsing.transl_block=yytransl_block;- Parsing.lhs=yylhs;- Parsing.len=yylen;- Parsing.defred=yydefred;- Parsing.dgoto=yydgoto;- Parsing.sindex=yysindex;- Parsing.rindex=yyrindex;- Parsing.gindex=yygindex;- Parsing.tablesize=yytablesize;- Parsing.table=yytable;- Parsing.check=yycheck;- Parsing.error_function=parse_error;- Parsing.names_const=yynames_const;- Parsing.names_block=yynames_block }-let file (lexfun : Lexing.lexbuf -> token) (lexbuf : Lexing.lexbuf) =- (Parsing.yyparse yytables 1 lexfun lexbuf : Dot_ast.file)
− external/ocamlgraph/src/dot_parser.mli
@@ -1,21 +0,0 @@-type token =- | ID of (Dot_ast.id)- | COLON- | COMMA- | EQUAL- | SEMICOLON- | EDGEOP- | STRICT- | GRAPH- | DIGRAPH- | LBRA- | RBRA- | LSQ- | RSQ- | NODE- | EDGE- | SUBGRAPH- | EOF--val file :- (Lexing.lexbuf -> token) -> Lexing.lexbuf -> Dot_ast.file
− external/ocamlgraph/src/gml.ml
@@ -1,670 +0,0 @@-# 20 "src/gml.mll"- -- open Lexing-- type value = - | Int of int - | Float of float- | String of string- | List of value_list-- and value_list = (string * value) list---# 16 "src/gml.ml"-let __ocaml_lex_tables = {- Lexing.lex_base = - "\000\000\252\255\253\255\114\000\002\000\007\000\228\000\086\001\- \252\255\253\255\200\001\009\000\014\000\058\002\002\000\251\255\- \252\255\001\000\080\000\102\000\194\000\216\000\052\001\071\001\- \253\255\006\000";- Lexing.lex_backtrk = - "\255\255\255\255\255\255\003\000\000\000\001\000\255\255\255\255\- \255\255\255\255\003\000\000\000\001\000\255\255\255\255\255\255\- \255\255\004\000\001\000\000\000\004\000\255\255\001\000\255\255\- \255\255\255\255";- Lexing.lex_default = - "\001\000\000\000\000\000\255\255\255\255\255\255\255\255\008\000\- \000\000\000\000\255\255\255\255\255\255\255\255\015\000\000\000\- \000\000\025\000\255\255\255\255\255\255\255\255\255\255\255\255\- \000\000\025\000";- Lexing.lex_trans = - "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\004\000\004\000\004\000\004\000\004\000\000\000\004\000\- \005\000\005\000\011\000\011\000\005\000\000\000\011\000\012\000\- \012\000\000\000\000\000\012\000\000\000\000\000\000\000\000\000\- \004\000\000\000\004\000\024\000\017\000\000\000\000\000\005\000\- \024\000\011\000\000\000\000\000\000\000\020\000\012\000\020\000\- \018\000\000\000\019\000\019\000\019\000\019\000\019\000\019\000\- \019\000\019\000\019\000\019\000\000\000\000\000\000\000\000\000\- \000\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\- \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\- \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\- \003\000\003\000\003\000\000\000\000\000\016\000\000\000\000\000\- \000\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\- \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\- \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\- \003\000\003\000\003\000\005\000\005\000\000\000\000\000\005\000\- \018\000\018\000\018\000\018\000\018\000\018\000\018\000\018\000\- \018\000\018\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\005\000\000\000\018\000\021\000\019\000\019\000\- \019\000\019\000\019\000\019\000\019\000\019\000\019\000\019\000\- \000\000\000\000\006\000\006\000\006\000\006\000\006\000\006\000\- \006\000\006\000\006\000\006\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\006\000\006\000\006\000\006\000\006\000\- \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\- \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\- \006\000\006\000\006\000\006\000\006\000\000\000\000\000\000\000\- \000\000\000\000\000\000\006\000\006\000\006\000\006\000\006\000\- \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\- \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\- \006\000\006\000\006\000\006\000\006\000\005\000\005\000\000\000\- \018\000\005\000\019\000\019\000\019\000\019\000\019\000\019\000\- \019\000\019\000\019\000\019\000\000\000\000\000\000\000\000\000\- \002\000\255\255\255\255\023\000\005\000\023\000\255\255\000\000\- \022\000\022\000\022\000\022\000\022\000\022\000\022\000\022\000\- \022\000\022\000\000\000\000\000\006\000\006\000\006\000\006\000\- \006\000\006\000\006\000\006\000\006\000\006\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\006\000\006\000\006\000\- \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\- \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\- \006\000\006\000\006\000\006\000\006\000\006\000\006\000\000\000\- \000\000\000\000\000\000\000\000\000\000\006\000\006\000\006\000\- \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\- \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\- \006\000\006\000\006\000\006\000\006\000\006\000\006\000\011\000\- \011\000\000\000\000\000\011\000\022\000\022\000\022\000\022\000\- \022\000\022\000\022\000\022\000\022\000\022\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\011\000\022\000\- \022\000\022\000\022\000\022\000\022\000\022\000\022\000\022\000\- \022\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\010\000\- \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\- \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\- \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\- \010\000\000\000\000\000\009\000\000\000\000\000\000\000\010\000\- \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\- \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\- \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\- \010\000\012\000\012\000\000\000\000\000\012\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \012\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\- \013\000\013\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\- \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\- \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\- \013\000\013\000\013\000\000\000\000\000\000\000\000\000\000\000\- \000\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\- \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\- \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\- \013\000\013\000\013\000\012\000\012\000\000\000\000\000\012\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\255\255\000\000\- \000\000\000\000\012\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\013\000\013\000\013\000\013\000\013\000\013\000\- \013\000\013\000\013\000\013\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\013\000\013\000\013\000\013\000\013\000\- \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\- \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\- \013\000\013\000\013\000\013\000\013\000\000\000\000\000\000\000\- \000\000\000\000\000\000\013\000\013\000\013\000\013\000\013\000\- \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\- \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\- \013\000\013\000\013\000\013\000\013\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000";- Lexing.lex_check = - "\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\000\000\000\000\004\000\004\000\000\000\255\255\004\000\- \005\000\005\000\011\000\011\000\005\000\255\255\011\000\012\000\- \012\000\255\255\255\255\012\000\255\255\255\255\255\255\255\255\- \000\000\255\255\004\000\017\000\014\000\255\255\255\255\005\000\- \025\000\011\000\255\255\255\255\255\255\014\000\012\000\014\000\- \014\000\255\255\014\000\014\000\014\000\014\000\014\000\014\000\- \014\000\014\000\014\000\014\000\255\255\255\255\255\255\255\255\- \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\255\255\255\255\014\000\255\255\255\255\- \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\003\000\003\000\255\255\255\255\003\000\- \018\000\018\000\018\000\018\000\018\000\018\000\018\000\018\000\- \018\000\018\000\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\003\000\255\255\019\000\018\000\019\000\019\000\- \019\000\019\000\019\000\019\000\019\000\019\000\019\000\019\000\- \255\255\255\255\003\000\003\000\003\000\003\000\003\000\003\000\- \003\000\003\000\003\000\003\000\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\003\000\003\000\003\000\003\000\003\000\- \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\- \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\- \003\000\003\000\003\000\003\000\003\000\255\255\255\255\255\255\- \255\255\255\255\255\255\003\000\003\000\003\000\003\000\003\000\- \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\- \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\- \003\000\003\000\003\000\003\000\003\000\006\000\006\000\255\255\- \020\000\006\000\020\000\020\000\020\000\020\000\020\000\020\000\- \020\000\020\000\020\000\020\000\255\255\255\255\255\255\255\255\- \000\000\017\000\014\000\021\000\006\000\021\000\025\000\255\255\- \021\000\021\000\021\000\021\000\021\000\021\000\021\000\021\000\- \021\000\021\000\255\255\255\255\006\000\006\000\006\000\006\000\- \006\000\006\000\006\000\006\000\006\000\006\000\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\006\000\006\000\006\000\- \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\- \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\- \006\000\006\000\006\000\006\000\006\000\006\000\006\000\255\255\- \255\255\255\255\255\255\255\255\255\255\006\000\006\000\006\000\- \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\- \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\- \006\000\006\000\006\000\006\000\006\000\006\000\006\000\007\000\- \007\000\255\255\255\255\007\000\022\000\022\000\022\000\022\000\- \022\000\022\000\022\000\022\000\022\000\022\000\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\007\000\023\000\- \023\000\023\000\023\000\023\000\023\000\023\000\023\000\023\000\- \023\000\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\007\000\- \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\255\255\255\255\007\000\255\255\255\255\255\255\007\000\- \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\010\000\010\000\255\255\255\255\010\000\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \010\000\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\- \010\000\010\000\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\010\000\010\000\010\000\010\000\010\000\010\000\010\000\- \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\- \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\- \010\000\010\000\010\000\255\255\255\255\255\255\255\255\255\255\- \255\255\010\000\010\000\010\000\010\000\010\000\010\000\010\000\- \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\- \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\- \010\000\010\000\010\000\013\000\013\000\255\255\255\255\013\000\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\007\000\255\255\- \255\255\255\255\013\000\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\013\000\013\000\013\000\013\000\013\000\013\000\- \013\000\013\000\013\000\013\000\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\013\000\013\000\013\000\013\000\013\000\- \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\- \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\- \013\000\013\000\013\000\013\000\013\000\255\255\255\255\255\255\- \255\255\255\255\255\255\013\000\013\000\013\000\013\000\013\000\- \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\- \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\- \013\000\013\000\013\000\013\000\013\000\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255";- Lexing.lex_base_code = - "\000\000\000\000\000\000\075\000\000\000\000\000\150\000\208\000\- \000\000\000\000\027\001\000\000\000\000\102\001\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000";- Lexing.lex_backtrk_code = - "\000\000\000\000\000\000\000\000\000\000\004\000\000\000\000\000\- \000\000\000\000\000\000\000\000\004\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000";- Lexing.lex_default_code = - "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000";- Lexing.lex_trans_code = - "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\000\000\000\000\000\000\000\000\000\000\- \000\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\000\000\000\000\- \000\000\000\000\000\000\000\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\000\000\000\000\000\000\000\000\000\000\000\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\000\000\000\000\000\000\000\000\000\000\- \000\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\000\000\000\000\- \000\000\000\000\000\000\000\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\000\000\000\000\000\000\000\000\000\000\000\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\- \001\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000";- Lexing.lex_check_code = - "\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\255\255\255\255\255\255\255\255\255\255\- \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\- \000\000\000\000\000\000\003\000\003\000\003\000\003\000\003\000\- \003\000\003\000\003\000\003\000\003\000\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\003\000\003\000\003\000\003\000\- \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\- \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\- \003\000\003\000\003\000\003\000\003\000\003\000\255\255\255\255\- \255\255\255\255\255\255\255\255\003\000\003\000\003\000\003\000\- \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\- \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\- \003\000\003\000\003\000\003\000\003\000\003\000\006\000\006\000\- \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\006\000\- \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\- \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\- \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\- \006\000\255\255\255\255\255\255\255\255\255\255\255\255\006\000\- \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\- \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\- \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\- \006\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\255\255\255\255\255\255\255\255\255\255\- \255\255\007\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\- \007\000\007\000\007\000\010\000\010\000\010\000\010\000\010\000\- \010\000\010\000\010\000\010\000\010\000\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\010\000\010\000\010\000\010\000\- \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\- \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\- \010\000\010\000\010\000\010\000\010\000\010\000\255\255\255\255\- \255\255\255\255\255\255\255\255\010\000\010\000\010\000\010\000\- \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\- \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\- \010\000\010\000\010\000\010\000\010\000\010\000\013\000\013\000\- \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\013\000\- \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\- \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\- \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\- \013\000\255\255\255\255\255\255\255\255\255\255\255\255\013\000\- \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\- \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\- \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\- \013\000\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\- \255\255\255\255\255\255\255\255\255\255\255\255\255\255";- Lexing.lex_code = - "\255\001\255\255\000\001\255";-}--let rec file lexbuf =- lexbuf.Lexing.lex_mem <- Array.create 2 (-1) ; __ocaml_lex_file_rec lexbuf 0-and __ocaml_lex_file_rec lexbuf __ocaml_lex_state =- match Lexing.new_engine __ocaml_lex_tables __ocaml_lex_state lexbuf with- | 0 ->-# 45 "src/gml.mll"- ( file lexbuf )-# 425 "src/gml.ml"-- | 1 ->-let-# 46 "src/gml.mll"- key-# 431 "src/gml.ml"-= Lexing.sub_lexeme lexbuf lexbuf.Lexing.lex_start_pos lexbuf.Lexing.lex_mem.(0) in-# 47 "src/gml.mll"- ( let v = value lexbuf in- (key, v) :: file lexbuf )-# 436 "src/gml.ml"-- | 2 ->-# 50 "src/gml.mll"- ( [] )-# 441 "src/gml.ml"-- | 3 ->-let-# 51 "src/gml.mll"- c-# 447 "src/gml.ml"-= Lexing.sub_lexeme_char lexbuf lexbuf.Lexing.lex_start_pos in-# 52 "src/gml.mll"- ( failwith ("Gml: invalid character " ^ String.make 1 c) )-# 451 "src/gml.ml"-- | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_file_rec lexbuf __ocaml_lex_state--and value_list lexbuf =- lexbuf.Lexing.lex_mem <- Array.create 2 (-1) ; __ocaml_lex_value_list_rec lexbuf 7-and __ocaml_lex_value_list_rec lexbuf __ocaml_lex_state =- match Lexing.new_engine __ocaml_lex_tables __ocaml_lex_state lexbuf with- | 0 ->-# 56 "src/gml.mll"- ( value_list lexbuf )-# 462 "src/gml.ml"-- | 1 ->-let-# 57 "src/gml.mll"- key-# 468 "src/gml.ml"-= Lexing.sub_lexeme lexbuf lexbuf.Lexing.lex_start_pos lexbuf.Lexing.lex_mem.(0) in-# 58 "src/gml.mll"- ( let v = value lexbuf in- (key, v) :: value_list lexbuf )-# 473 "src/gml.ml"-- | 2 ->-# 61 "src/gml.mll"- ( [] )-# 478 "src/gml.ml"-- | 3 ->-let-# 62 "src/gml.mll"- c-# 484 "src/gml.ml"-= Lexing.sub_lexeme_char lexbuf lexbuf.Lexing.lex_start_pos in-# 63 "src/gml.mll"- ( failwith ("Gml: invalid character " ^ String.make 1 c) )-# 488 "src/gml.ml"-- | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_value_list_rec lexbuf __ocaml_lex_state--and value lexbuf =- __ocaml_lex_value_rec lexbuf 14-and __ocaml_lex_value_rec lexbuf __ocaml_lex_state =- match Lexing.engine __ocaml_lex_tables __ocaml_lex_state lexbuf with- | 0 ->-let-# 66 "src/gml.mll"- i-# 500 "src/gml.ml"-= Lexing.sub_lexeme lexbuf lexbuf.Lexing.lex_start_pos lexbuf.Lexing.lex_curr_pos in-# 67 "src/gml.mll"- ( Int (int_of_string i) )-# 504 "src/gml.ml"-- | 1 ->-let-# 68 "src/gml.mll"- r-# 510 "src/gml.ml"-= Lexing.sub_lexeme lexbuf lexbuf.Lexing.lex_start_pos lexbuf.Lexing.lex_curr_pos in-# 69 "src/gml.mll"- ( Float (float_of_string r) )-# 514 "src/gml.ml"-- | 2 ->-let-# 70 "src/gml.mll"- s-# 520 "src/gml.ml"-= Lexing.sub_lexeme lexbuf (lexbuf.Lexing.lex_start_pos + 1) (lexbuf.Lexing.lex_curr_pos + -1) in-# 71 "src/gml.mll"- ( String s )-# 524 "src/gml.ml"-- | 3 ->-# 73 "src/gml.mll"- ( let l = value_list lexbuf in List l )-# 529 "src/gml.ml"-- | 4 ->-let-# 74 "src/gml.mll"- c-# 535 "src/gml.ml"-= Lexing.sub_lexeme_char lexbuf lexbuf.Lexing.lex_start_pos in-# 75 "src/gml.mll"- ( failwith ("Gml: invalid character " ^ String.make 1 c) )-# 539 "src/gml.ml"-- | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_value_rec lexbuf __ocaml_lex_state--;;--# 77 "src/gml.mll"- -- let parse f =- let c = open_in f in- let lb = from_channel c in- let v = file lb in- close_in c;- v-- module Parse- (B : Builder.S)- (L : sig val node : value_list -> B.G.V.label- val edge : value_list -> B.G.E.label end) = - struct-- let create_graph l =- let nodes = Hashtbl.create 97 in- let g = B.empty () in- (* 1st pass: create the nodes *)- let g =- List.fold_left - (fun g v -> match v with- | "node", List l ->- let n = B.G.V.create (L.node l) in- begin - try - let id = List.assoc "id" l in Hashtbl.add nodes id n- with Not_found -> - ()- end;- B.add_vertex g n- | _ -> - g)- g l- in- (* 2nd pass: add the edges *)- List.fold_left- (fun g v -> match v with- | "edge", List l ->- begin try- let source = List.assoc "source" l in- let target = List.assoc "target" l in- let nsource = Hashtbl.find nodes source in- let ntarget = Hashtbl.find nodes target in- let e = B.G.E.create nsource (L.edge l) ntarget in- B.add_edge_e g e- with Not_found ->- g- end- | _ ->- g)- g l- - let parse f =- match parse f with- | ["graph", List l] -> create_graph l- | _ -> invalid_arg "Gml.Parse.parse: not a graph file"- - end-- module Print- (G : sig- module V : sig- type t- val hash : t -> int- val equal : t -> t -> bool- type label- val label : t -> label- end- module E : sig- type t- type label- val src : t -> V.t- val dst : t -> V.t- val label : t -> label- end- type t- val iter_vertex : (V.t -> unit) -> t -> unit- val iter_edges_e : (E.t -> unit) -> t -> unit- end)- (L : sig- val node : G.V.label -> value_list- val edge : G.E.label -> value_list- end) =- struct-- open Format-- module H = Hashtbl.Make(G.V)-- let print fmt g =- let nodes = H.create 97 in- let cpt = ref 0 in- let id n = - try H.find nodes n- with Not_found -> incr cpt; let id = !cpt in H.add nodes n id; id- in- fprintf fmt "@[graph [@\n";- let rec value fmt = function- | Int n -> fprintf fmt "%d" n- | Float f -> fprintf fmt "%f" f- | String s -> fprintf fmt "\"%s\"" s- | List l -> fprintf fmt "[@\n @[%a@]@\n]" value_list l- and value_list fmt = function- | [] -> ()- | [s,v] -> fprintf fmt "%s %a" s value v- | (s,v) :: l -> fprintf fmt "%s %a@\n" s value v; value_list fmt l- in- G.iter_vertex- (fun v -> - fprintf fmt " @[node [@\n id %d@\n @[%a@]@\n]@]@\n" - (id v) value_list (L.node (G.V.label v)))- g;- G.iter_edges_e- (fun e ->- fprintf fmt - " @[edge [@\n source %d@\n target %d@\n @[%a@]@\n]@]@\n"- (id (G.E.src e)) (id (G.E.dst e)) - value_list (L.edge (G.E.label e)))- g;- fprintf fmt "]@\n"-- end---# 671 "src/gml.ml"
− external/ocamlgraph/src/version.ml
@@ -1,2 +0,0 @@-let version = "0.99b"-let date = "Tue Aug 12 13:29:08 PDT 2014"
liquid-fixpoint.cabal view
@@ -1,5 +1,6 @@ name: liquid-fixpoint-version: 0.2.0.0+version: 0.2.1.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 license: BSD3@@ -24,7 +25,7 @@ . 3. Code for parsing the results from the fixpoint.native binary .- 4. The Ocaml fixpoint code+ 4. The Ocaml fixpoint code and pre-compiled binaries . 5. (Deprecated) Z3 binaries if you want to link against the API. .@@ -32,9 +33,11 @@ . In addition to the .cabal dependencies you require .- - A Recent Ocaml compiler+ - A Z3 (<http://z3.codeplex.com>) or CVC4 (<http://cvc4.cs.nyu.edu>) binary.+ If on Windows, please make sure to place the binary and any associated DLLs+ in your "cabal/bin" folder, right next to the fixpoint.native.exe binary. .- - A Z3 Binary (<http://z3.codeplex.com>)+ - An ocaml compiler (if installing with -fbuild-external). Extra-Source-Files: configure , external/fixpoint/Makefile@@ -47,9 +50,7 @@ , external/misc/*.ml , external/misc/*.mli , external/ocamlgraph/.depend- , external/ocamlgraph/Makefile , external/ocamlgraph/Makefile.in- , external/ocamlgraph/META , external/ocamlgraph/META.in , external/ocamlgraph/configure , external/ocamlgraph/configure.in@@ -67,11 +68,19 @@ , external/z3/ocaml/build-lib.sh , external/z3/ocaml/z3.ml , external/z3/ocaml/*.c+ , external/fixpoint/fixpoint.native-i386-linux+ , external/fixpoint/fixpoint.native-i686-w64-mingw32+ , external/fixpoint/fixpoint.native-x86_64-darwin+ , external/fixpoint/fixpoint.native-x86_64-linux Flag z3mem Description: Link to Z3 Default: False +Flag build-external+ Description: Build fixpoint.native binary from source (requires ocaml)+ Default: False+ Source-Repository head Type: git Location: https://github.com/ucsd-progsys/liquid-fixpoint/@@ -93,7 +102,7 @@ , containers , deepseq , directory- , filemanip+ -- , filemanip , filepath , mtl , parsec@@ -119,7 +128,7 @@ , containers , deepseq , directory- , filemanip+ -- , filemanip , filepath , mtl , parsec@@ -139,6 +148,7 @@ Language.Fixpoint.Errors, Language.Fixpoint.Config, Language.Fixpoint.Types,+ Language.Fixpoint.Visitor, Language.Fixpoint.Sort, Language.Fixpoint.Interface, Language.Fixpoint.Parse,
src/Language/Fixpoint/Files.hs view
@@ -22,9 +22,9 @@ , getFixpointPath, getZ3LibPath -- * Various generic utility functions for finding and removing files- , getHsTargets+ -- , getHsTargets , getFileInDirs- , findFileInDirs+ -- , findFileInDirs , copyFiles ) where@@ -37,14 +37,17 @@ import System.Directory import System.Environment import System.FilePath-import System.FilePath.Find+-- import System.FilePath.Find import Language.Fixpoint.Misc ------------------------------------------------------------ -- | Hardwired Paths and Files ----------------------------- ------------------------------------------------------------ -getFixpointPath = fromMaybe msg <$> findExecutable "fixpoint.native"+getFixpointPath = fromMaybe msg . msum <$>+ sequence [ findExecutable "fixpoint.native"+ , findExecutable "fixpoint.native.exe"+ ] where msg = errorstar "Cannot find fixpoint binary [fixpoint.native]" getZ3LibPath = dropFileName <$> getFixpointPath@@ -149,15 +152,15 @@ ---------------------------------------------------------------------------------- -getHsTargets p = mapM canonicalizePath =<< files- where- files- | hasTrailingPathSeparator p = getHsSourceFiles p- | otherwise = return [p]+-- getHsTargets p = mapM canonicalizePath =<< files+-- where+-- files+-- | hasTrailingPathSeparator p = getHsSourceFiles p+-- | otherwise = return [p] -getHsSourceFiles = find dirs hs- where hs = extension ==? ".hs" ||? extension ==? ".lhs"- dirs = liftM (not . ("dist" `isSuffixOf`)) directory+-- getHsSourceFiles = find dirs hs+-- where hs = extension ==? ".hs" ||? extension ==? ".lhs"+-- dirs = liftM (not . ("dist" `isSuffixOf`)) directory --------------------------------------------------------------------------- @@ -165,7 +168,7 @@ getFileInDirs :: FilePath -> [FilePath] -> IO (Maybe FilePath) getFileInDirs name = findFirst (testM doesFileExist . (</> name)) -findFileInDirs :: FilePath -> [FilePath] -> IO FilePath-findFileInDirs file dirs- = liftM (fromMaybe err) (findFirst (find always (fileName ==? file)) dirs)- where err = errorstar $ "findFileInDirs: cannot find " ++ file ++ " in " ++ show dirs+-- findFileInDirs :: FilePath -> [FilePath] -> IO FilePath+-- findFileInDirs file dirs+-- = liftM (fromMaybe err) (findFirst (find always (fileName ==? file)) dirs)+-- where err = errorstar $ "findFileInDirs: cannot find " ++ file ++ " in " ++ show dirs
src/Language/Fixpoint/Misc.hs view
@@ -3,6 +3,7 @@ module Language.Fixpoint.Misc where +import Data.Traversable (traverse) import Data.Hashable import qualified Control.Exception as Ex -- import qualified Data.HashSet as S @@ -41,11 +42,12 @@ wrapStarsWithOptStars True msg = "\n**** " ++ msg ++ " " ++ replicate (74 - length msg) '*' wrapStarsWithOptStars False msg = wrapStars msg- ++-- withColor _ act = act withColor c act- = do setSGR [ SetConsoleIntensity BoldIntensity, SetColor Foreground Vivid c] - act- setSGR [ Reset]+ = do setSGR [ SetConsoleIntensity BoldIntensity, SetColor Foreground Vivid c] + act+ setSGR [ Reset] colorStrLn c = withColor (moodColor c) . putStrLn colorPhaseLn c msg = colorStrLn c . wrapStars . (msg ++)@@ -384,4 +386,4 @@ Left l -> go (l:ls) rs xs Right r -> go ls (r:rs) xs -+f <$$> x = traverse f x
src/Language/Fixpoint/Names.hs view
@@ -262,6 +262,7 @@ , "Set_cap" , "Set_dif" , "Set_emp"+ , "Set_empty" , "Set_mem" , "Set_sub" , "FAppTy"
src/Language/Fixpoint/Parse.hs view
@@ -517,7 +517,7 @@ remainderP p = do res <- p- str <- stateInput <$> getParserState+ str <- getInput pos <- getPosition return (res, str, pos) @@ -533,7 +533,7 @@ parseFromFile p f = doParse' p f <$> readFile f freshIntP :: Parser Integer-freshIntP = do n <- stateUser <$> getParserState+freshIntP = do n <- getState updateState (+ 1) return n
src/Language/Fixpoint/SmtLib2.hs view
@@ -30,6 +30,7 @@ -- * Creating and killing SMTLIB2 Process , Context (..) , makeContext+ , makeContextNoLog , cleanupContext -- * Execute Queries@@ -112,7 +113,7 @@ data Context = Ctx { pId :: ProcessHandle , cIn :: Handle , cOut :: Handle- , cLog :: Handle+ , cLog :: Maybe Handle , verbose :: Bool } @@ -147,7 +148,7 @@ case A.eitherResult res of Left e -> error e Right r -> do- hPutStrLnNow (cLog me) $ format "; SMT Says: {}" (Only $ show r)+ maybe (return ()) (\h -> hPutStrLnNow h $ format "; SMT Says: {}" (Only $ show r)) (cLog me) when (verbose me) $ LTIO.putStrLn $ format "SMT Says: {}" (Only $ show r) return r@@ -189,7 +190,9 @@ ((x:y:[]),zs) -> (x,y) : pairs zs smtWriteRaw :: Context -> LT.Text -> IO ()-smtWriteRaw me !s = {-# SCC smtWriteRaw #-} hPutStrLnNow (cOut me) s >> hPutStrLnNow (cLog me) s+smtWriteRaw me !s = {-# SCC smtWriteRaw #-} do+ hPutStrLnNow (cOut me) s+ maybe (return ()) (\h -> hPutStrLnNow h s) (cLog me) smtReadRaw :: Context -> IO Raw smtReadRaw me = {-# SCC smtReadRaw #-} TIO.hGetLine (cIn me)@@ -204,15 +207,23 @@ makeContext :: SMTSolver -> IO Context -------------------------------------------------------------------------- makeContext s+ = do me <- makeProcess s+ pre <- smtPreamble s me+ createDirectoryIfMissing True $ takeDirectory smtFile+ hLog <- openFile smtFile WriteMode+ let me' = me { cLog = Just hLog }+ mapM_ (smtWrite me') pre+ return me'++makeContextNoLog s = do me <- makeProcess s- mapM_ (smtWrite me) $ smtPreamble s+ pre <- smtPreamble s me+ mapM_ (smtWrite me) pre return me makeProcess s = do (hOut, hIn, _ ,pid) <- runInteractiveCommand $ smtCmd s- createDirectoryIfMissing True $ takeDirectory smtFile- hLog <- openFile smtFile WriteMode- return $ Ctx pid hIn hOut hLog False+ return $ Ctx pid hIn hOut Nothing False -------------------------------------------------------------------------- cleanupContext :: Context -> IO ExitCode@@ -222,20 +233,26 @@ code <- waitForProcess pId hClose cIn hClose cOut- hClose cLog+ maybe (return ()) hClose cLog return code {- "z3 -smt2 -in" -} {- "z3 -smtc SOFT_TIMEOUT=1000 -in" -} {- "z3 -smtc -in MBQI=false" -} --- ERIC: Do we really need to set mbqi to false? It seems useful for generating test data-smtCmd Z3 = "z3 -smt2 -in MODEL=true MODEL.PARTIAL=true auto-config=false"+smtCmd Z3 = "z3 -smt2 -in" smtCmd Mathsat = "mathsat -input=smt2" smtCmd Cvc4 = "cvc4 --incremental -L smtlib2" -smtPreamble Z3 = z3Preamble-smtPreamble _ = smtlibPreamble+-- DON'T REMOVE THIS! z3 changed the names of options between 4.3.1 and 4.3.2...+smtPreamble Z3 me + = do smtWrite me "(get-info :version)"+ r <- (!!1) . T.splitOn "\"" <$> smtReadRaw me+ case r of+ "4.3.2" -> return $ z3_432_options ++ z3Preamble+ _ -> return $ z3_options ++ z3Preamble+smtPreamble _ _ + = return smtlibPreamble smtFile :: FilePath smtFile = extFileName Smt2 "out"@@ -282,6 +299,18 @@ ,("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 + = [ "(set-option :auto-config false)"+ , "(set-option :model true)"+ , "(set-option :model.partial false)"+ , "(set-option :smt.mbqi false)" ]+z3_options + = [ "(set-option :auto-config false)"+ , "(set-option :model true)"+ , "(set-option :model-partial false)"+ , "(set-option :mbqi false)" ]+ z3Preamble = [ format "(define-sort {} () Int)" (Only elt)@@ -355,7 +384,7 @@ foldr (\(x,y) t -> T.replace x y t) t [("[", "ZM"), ("]", "ZN"), (":", "ZC") ,("(", "ZL"), (")", "ZR"), (",", "ZT") ,("|", "zb"), ("#", "zh"), ("\\","zr")- ,("z", "zz"), ("Z", "ZZ")]+ ,("z", "zz"), ("Z", "ZZ"), ("%","zv")] instance SMTLIB2 SymConst where smt2 (SL s) = LT.fromStrict s
src/Language/Fixpoint/Sort.hs view
@@ -94,10 +94,14 @@ check γ e = do {checkExpr f e; return ()} where f = (`lookupSEnvWithDistance` γ) - checkSort γ s e = do {t <- checkExpr f e; checkEqSort s t}- where f = (`lookupSEnvWithDistance` γ)+ checkSort γ s e = checkExpr f (ECst e s) >> return ()+ where+ f = (`lookupSEnvWithDistance` γ) + -- ORIG checkSort γ s e = do {t <- checkExpr f e; checkEqSort s t}+ -- ORIG where f = (`lookupSEnvWithDistance` γ) + checkEqSort s t | s == t = return () | otherwise = throwError $ "Couldn't match expected type '" @@ -159,8 +163,11 @@ then return t else throwError (errCast e t' t) --- | Helper for checking uninterpreted function applications +checkApp f to g es+ = snd <$> checkApp' f to g es++-- | Helper for checking uninterpreted function applications checkApp' f to g es = do gt <- checkLocSym f g (n, its, ot) <- sortFunction gt@@ -174,10 +181,6 @@ return (θ', apply θ' t) -checkApp f to g es- = snd <$> checkApp' f to g es-- -- | Helper for checking binary (numeric) operations checkOp f e1 o e2 @@ -198,6 +201,9 @@ checkOpTy f e t t' = throwError $ errOp e t t' +checkFractional f l+ = throwError $ errNonFractional l+ checkNumeric f l = do t <- checkSym f l unless (t == FNum) (throwError $ errNonNumeric l)@@ -238,10 +244,22 @@ = (checkNumeric f l >> checkNumeric f l') `catchError` (\_ -> throwError $ errNonNumerics l l') checkRelTy f _ _ FInt (FObj l) = (checkNumeric f l) `catchError` (\_ -> throwError $ errNonNumeric l) checkRelTy f _ _ (FObj l) FInt = (checkNumeric f l) `catchError` (\_ -> throwError $ errNonNumeric l)-checkRelTy f _ _ FReal (FObj l) = (checkNumeric f l) `catchError` (\_ -> throwError $ errNonNumeric l) -checkRelTy f _ _ (FObj l) FReal = (checkNumeric f l) `catchError` (\_ -> throwError $ errNonNumeric l)-checkRelTy _ e Eq t1 t2 = unless (t1 == t2 && t1 /= fProp) (throwError $ errRel e t1 t2)-checkRelTy _ e Ne t1 t2 = unless (t1 == t2 && t1 /= fProp) (throwError $ errRel e t1 t2)+checkRelTy f _ _ FReal FReal = return ()+checkRelTy f _ _ FReal (FObj l) = (checkFractional f l) `catchError` (\_ -> throwError $ errNonFractional l) +checkRelTy f _ _ (FObj l) FReal = (checkFractional f l) `catchError` (\_ -> throwError $ errNonFractional l)++checkRelTy _ e Eq t1 t2+ | t1 == fProp || t2 == fProp = throwError $ errRel e t1 t2+checkRelTy _ e Ne t1 t2+ | t1 == fProp || t2 == fProp = throwError $ errRel e t1 t2+checkRelTy _ e Eq t1 t2 = unify [t1] [t2] >> return ()+checkRelTy _ e Ne t1 t2 = unify [t1] [t2] >> return ()++-- ORIG checkRelTy _ e Eq t1 t2 = unless (t1 == t2 && t1 /= fProp) (throwError $ errRel e t1 t2)+-- ORIG checkRelTy _ e Ne t1 t2 = unless (t1 == t2 && t1 /= fProp) (throwError $ errRel e t1 t2)+++ checkRelTy _ e Ueq t1 t2 = unless (isAppTy t1 && isAppTy t2) (throwError $ errRel e t1 t2) checkRelTy _ e Une t1 t2 = unless (isAppTy t1 && isAppTy t2) (throwError $ errRel e t1 t2) checkRelTy _ e _ t1 t2 = unless (t1 == t2) (throwError $ errRel e t1 t2)@@ -258,6 +276,16 @@ isAppTy (FApp _ _) = True isAppTy _ = False ++isPoly :: Sort -> Bool+isPoly = not . null . fVars++fVars (FVar i) = [i]+fVars (FFunc _ ts) = concatMap fVars ts+fVars (FApp _ ts) = concatMap fVars ts+fVars _ = []++ ------------------------------------------------------------------------- -- | Error messages ----------------------------------------------------- -------------------------------------------------------------------------@@ -295,7 +323,9 @@ errNonFunction t = printf "Sort %s is not a function" (showFix t) errNonNumeric l = printf "FObj sort %s is not numeric" (showFix l)-errNonNumerics l l' = printf "FObj sort %s and %s are different and not numeric" (showFix l) (showFix l')+errNonNumerics l l' = printf "FObj sort %s and %s are different and not numeric" (showFix l) (showFix l')++errNonFractional l = printf "FObj sort %s is not fractional" (showFix l) errUnexpectedPred p = printf "Sort Checking: Unexpected Predicate %s" (showFix p)
src/Language/Fixpoint/Types.hs view
@@ -789,7 +789,7 @@ type BindId = Int type FEnv = SEnv SortedReft -newtype IBindEnv = FB (S.HashSet BindId)+newtype IBindEnv = FB (S.HashSet BindId) deriving (Data, Typeable) newtype SEnv a = SE { se_binds :: M.HashMap Symbol a } deriving (Eq, Data, Typeable, Generic, F.Foldable, Traversable) data BindEnv = BE { be_size :: Int , be_binds :: M.HashMap BindId (Symbol, SortedReft)
+ src/Language/Fixpoint/Visitor.hs view
@@ -0,0 +1,127 @@+{-# LANGUAGE TupleSections #-}++module Language.Fixpoint.Visitor (+ -- * Visitor+ Visitor (..)+ + -- * Default Visitor+ , defaultVisitor++ -- * Transformers+ , trans+ + -- * Accumulators+ , fold++ ) where++import Data.Monoid+import Data.Traversable (traverse)+import Control.Applicative (Applicative (), (<$>), (<*>))+import Control.Exception (throw)+import Control.Monad.Trans.State (modify, State, runState)+import Language.Fixpoint.Misc (mapSnd)+import Language.Fixpoint.Types++++data Visitor acc ctx = Visitor {+ -- | Context @ctx@ is built up in a "top-down" fashion but not across siblings+ ctxExpr :: ctx -> Expr -> ctx+ , ctxPred :: ctx -> Pred -> ctx++ -- | Transforms can access current @ctx@+ , txExpr :: ctx -> Expr -> Expr + , txPred :: ctx -> Pred -> Pred ++ -- | Accumulations can access current @ctx@; @acc@ value is monoidal+ , accExpr :: ctx -> Expr -> acc+ , accPred :: ctx -> Pred -> acc+ }+ +---------------------------------------------------------------------------------+defaultVisitor :: Monoid acc => Visitor acc ctx+---------------------------------------------------------------------------------+defaultVisitor = Visitor {+ ctxExpr = \c _ -> c+ , ctxPred = \c _ -> c+ , txExpr = \_ x -> x+ , txPred = \_ x -> x+ , accExpr = \_ _ -> mempty+ , accPred = \_ _ -> mempty+ } +++------------------------------------------------------------------------ ++fold :: (Visitable t, Monoid a) => Visitor a ctx -> ctx -> a -> t -> a +fold v c a t = snd $ execVisitM v c a visit t++trans :: (Visitable t, Monoid a) => Visitor a ctx -> ctx -> a -> t -> t +trans v c a z = fst $ execVisitM v c mempty visit z ++execVisitM v c a f x = runState (f v c x) a++type VisitM acc = State acc ++accum :: (Monoid a) => a -> VisitM a ()+accum = modify . mappend++f <$$> x = traverse f x++------------------------------------------------------------------------------+class Visitable t where+ visit :: (Monoid a) => Visitor a c -> c -> t -> VisitM a t++instance Visitable Expr where+ visit = visitExpr++instance Visitable Pred where+ visit = visitPred++instance Visitable Refa where+ visit v c (RConc p) = RConc <$> visit v c p+ visit _ _ r = return r ++instance Visitable Reft where+ visit v c (Reft (vv, ras)) = (Reft . (vv,)) <$> visitMany v c ras ++visitMany :: (Monoid a, Visitable t) => Visitor a ctx -> ctx -> [t] -> VisitM a [t]+visitMany v c xs = visit v c <$$> xs++visitExpr :: (Monoid a) => Visitor a ctx -> ctx -> Expr -> VisitM a Expr +visitExpr v = vE+ where+ vP = visitPred v+ vE c e = accum acc >> step c' e' where c' = ctxExpr v c e+ e' = txExpr v c' e+ acc = accExpr v c' e+ step c e@EBot = return e+ step c e@(ESym _) = return e + step c e@(ECon _) = return e + step c e@(ELit _ _) = return e + step c e@(EVar _) = return e+ step c (EApp f es) = EApp f <$> (vE c <$$> es) + step c (EBin o e1 e2) = EBin o <$> vE c e1 <*> vE c e2+ step c (EIte p e1 e2) = EIte <$> vP c p <*> vE c e1 <*> vE c e2+ step c (ECst e t) = (`ECst` t) <$> vE c e+ +visitPred :: (Monoid a) => Visitor a ctx -> ctx -> Pred -> VisitM a Pred +visitPred v = vP+ where+ vE = visitExpr v+ vP c p = accum acc >> step c' p' where c' = ctxPred v c p+ p' = txPred v c' p+ acc = accPred v c' p+ step c (PAnd ps) = PAnd <$> (vP c <$$> ps)+ step c (POr ps) = POr <$> (vP c <$$> ps) + step c (PNot p) = PNot <$> vP c p+ step c (PImp p1 p2) = PImp <$> vP c p1 <*> vP c p2 + step c (PIff p1 p2) = PIff <$> vP c p1 <*> vP c p2+ step c (PBexp e) = PBexp <$> vE c e+ step c (PAtom r e1 e2) = PAtom r <$> vE c e1 <*> vE c e2 + step c (PAll xts p) = PAll xts <$> vP c p+ step c p@PTrue = return p+ step c p@PFalse = return p+ step c p@PTop = return p+