liquid-fixpoint 0.2.3.1 → 0.2.3.2
raw patch · 28 files changed
+2756/−1158 lines, 28 filesPVP: minor bump suggested
API additions: PVP suggests at least a minor version bump
API changes (from Hackage documentation)
+ Language.Fixpoint.Types: FFrac :: Sort
+ Language.Fixpoint.Types: instance Constructor C1_7Sort
Files
- external/fixpoint/ast.ml +504/−493
- external/fixpoint/ast.mli +1/−0
- external/fixpoint/fixLex.mll +1/−0
- external/fixpoint/fixParse.mly +2/−1
- external/fixpoint/fixpoint.native-i386-linux binary
- external/fixpoint/fixpoint.native-i686-w64-mingw32 too large to diff
- external/fixpoint/fixpoint.native-x86_64-darwin too large to diff
- external/fixpoint/fixpoint.native-x86_64-linux too large to diff
- external/fixpoint/predAbs.ml +0/−58
- external/ocamlgraph/src/dot_lexer.ml +386/−0
- external/ocamlgraph/src/dot_parser.ml +551/−0
- external/ocamlgraph/src/dot_parser.mli +21/−0
- external/ocamlgraph/src/gml.ml +670/−0
- external/ocamlgraph/src/version.ml +2/−0
- liquid-fixpoint.cabal +1/−1
- src/Language/Fixpoint/Bitvector.hs +15/−16
- src/Language/Fixpoint/Config.hs +30/−32
- src/Language/Fixpoint/Errors.hs +30/−31
- src/Language/Fixpoint/Files.hs +14/−14
- src/Language/Fixpoint/Interface.hs +48/−48
- src/Language/Fixpoint/Misc.hs +105/−102
- src/Language/Fixpoint/Names.hs +29/−29
- src/Language/Fixpoint/Parse.hs +135/−129
- src/Language/Fixpoint/PrettyPrint.hs +8/−8
- src/Language/Fixpoint/SmtLib2.hs +46/−45
- src/Language/Fixpoint/Sort.hs +75/−72
- src/Language/Fixpoint/Types.hs +54/−50
- src/Language/Fixpoint/Visitor.hs +28/−29
external/fixpoint/ast.ml view
@@ -1,30 +1,30 @@ (*- * Copyright © 2009 The Regents of the University of California. All rights reserved. + * Copyright © 2009 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 + * 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. * *) (**- * This module implements a DAG representation for expressions and + * This module implements a DAG representation for expressions and * predicates: each sub-predicate or sub-expression is paired with- * a unique int ID, which enables constant time hashing. + * a unique int ID, which enables constant time hashing. * However, one must take care when using DAGS: * (1) they can only be constructed using the appropriate functions * (2) when destructed via pattern-matching, one must discard the ID@@ -42,17 +42,17 @@ module Cone = struct type 'a t = Empty | Cone of ('a * 'a t) list - let rec map f = function + let rec map f = function | Empty -> Empty | Cone xcs -> Cone (List.map (f <**> map f) xcs)-end +end module Sort = struct- type loc = - | Loc of string + type loc =+ | Loc of string | Lvar of int- | LFun + | LFun type tycon = string @@ -63,25 +63,27 @@ | Obj | Var of int (* type-var *) | Ptr of loc (* c-pointer *)- | Func of int * t list (* type-var-arity, in-types @ [out-type] *)- | Num (* kind, for numeric tyvars -- ptr(loc(s)) -- *)+ | Func of int * t list (* type-var-arity, in-types @ [out-type] *)+ | Num (* kind, for numeric tyvars -- ptr(loc(s)) -- *)+ | Frac (* kind, for fractional tyvars -- ptr(loc(s)) -- *) | App of tycon * t list (* type constructors *) - type sub = { locs: (int * string) list; + type sub = { locs: (int * string) list; vars: (int * t) list; } - + let tycon_string x = x (*- let is_loc_string s = - let re = Str.regexp "[a-zA-Z]+[0-9]+" in + let is_loc_string s =+ let re = Str.regexp "[a-zA-Z]+[0-9]+" in Str.string_match re s 0- + let loc_of_string = fun s -> let _ = asserts (is_loc_string s) in Loc s let loc_of_index = fun i -> Lvar i *) - let t_num = Num + let t_num = Num+ let t_frac = Frac let t_obj = Obj let t_bool = Bool let t_int = Int@@ -89,17 +91,17 @@ let t_generic = fun i -> let _ = asserts (0 <= i) "t_generic: %d" i in Var i let t_ptr = fun l -> Ptr l let t_func = fun i ts -> Func (i, ts)- let tycon s = s + let tycon s = s let tc_app = "FAppTy" (* let tycon_re = Str.regexp "[A-Z][0-9 a-z A-Z '.']"- * function | s when Str.string_match tycon_re s 0 -> s - | s -> assertf "Error: Invalid tycon: %s" s + * function | s when Str.string_match tycon_re s 0 -> s+ | s -> assertf "Error: Invalid tycon: %s" s *) - let t_app c ts = if c = tc_app then App (c, ts) else + let t_app c ts = if c = tc_app then App (c, ts) else List.fold_left (fun t1 t2 -> App (tc_app, [t1; t2])) (App (c, [])) ts- (* let t_app c ts = List.fold_left (fun t1 t2 -> App ("FAppTy", [t1; t2])) (App (c, [])) ts *) + (* let t_app c ts = List.fold_left (fun t1 t2 -> App ("FAppTy", [t1; t2])) (App (c, [])) ts *) (* let t_app c ts = App (c, ts) *) let loc_to_string = function@@ -114,36 +116,37 @@ | Bool -> "bool" | Obj -> "obj" | Num -> "num"- | Ptr l -> loc_to_string l + | Frac -> "frac"+ | Ptr l -> loc_to_string l (* Printf.sprintf "ptr(%s)" (loc_to_string l) *)- | Func (n, ts) -> ts |> List.map to_string - |> String.concat " ; " - |> Printf.sprintf "func(%d, [%s])" n - | App (c, ts) -> ts |> List.map to_string_arg - |> String.concat " " - |> Printf.sprintf "%s %s" c - - and to_string_arg t = match t with + | Func (n, ts) -> ts |> List.map to_string+ |> String.concat " ; "+ |> Printf.sprintf "func(%d, [%s])" n+ | App (c, ts) -> ts |> List.map to_string_arg+ |> String.concat " "+ |> Printf.sprintf "%s %s" c++ and to_string_arg t = match t with | App (_, _) -> Printf.sprintf "(%s)" (to_string t) | _ -> to_string t let to_string_short = function | Func _ -> "func" (* | Ptr _ -> "ptr" *)- | t -> to_string t + | t -> to_string t - let print fmt t = - t |> to_string + let print fmt t =+ t |> to_string |> Format.fprintf fmt "%s" let sub_to_string {locs = ls; vars = vs} = let lts = fun (i, s) -> Printf.sprintf "(%d := %s)" i s in let vts = fun (i, t) -> Printf.sprintf "(%d := %s)" i (to_string t) in- Printf.sprintf "locs := %s, vars := %s \n" - (String.concat "" (List.map lts ls)) - (String.concat "" (List.map vts vs)) + Printf.sprintf "locs := %s, vars := %s \n"+ (String.concat "" (List.map lts ls))+ (String.concat "" (List.map vts vs)) - let rec map f = function + let rec map f = function | Func (n, ts) -> Func (n, List.map (map f) ts) | App (c, ts) -> App (c, List.map (map f) ts) | t -> f t@@ -152,8 +155,8 @@ | Func (n, ts) as t -> List.fold_left (fold f) (f b t) ts | t -> f b t - let subs_tvar ts = - map begin function + let subs_tvar ts =+ map begin function | Var i -> Misc.do_catchf "ERROR: subs_tvar" (List.nth ts) i | t -> t end@@ -165,7 +168,7 @@ let is_int = function | Int -> true | _ -> false- + let is_real = function | Real -> true | _ -> false@@ -179,19 +182,19 @@ | _ -> false let app_of_t = function- | App (c, ts) -> Some (c, ts) + | App (c, ts) -> Some (c, ts) | _ -> None (* (L t1 t2 t3) is now encoded as ---> (((L @ t1) @ t2) @ t3) ---> App(@, [App(@, [App(@, [L[]; t1]); t2]); t3])- The following decodes the above as + The following decodes the above as *)- let rec app_args_of_t acc = function - | App (c, [t1; t2]) when c = tc_app -> app_args_of_t (t2 :: acc) t1 + let rec app_args_of_t acc = function+ | App (c, [t1; t2]) when c = tc_app -> app_args_of_t (t2 :: acc) t1 | App (c, []) -> (c, acc) | t -> (tc_app, t :: acc)- + (* | Ptr (Loc s) -> (tycon s, acc) | t -> assertf "app_args_of_t: unexpected t1 = %s" (to_string t)@@ -200,10 +203,10 @@ let app_of_t = function | App (c, _) as t when c = tc_app -> Some (app_args_of_t [] t) | App (c, ts) -> Some (c, ts)- | _ -> None + | _ -> None let func_of_t = function- | Func (i, ts) -> let (xts, t) = ts |> Misc.list_snoc |> Misc.swap in + | Func (i, ts) -> let (xts, t) = ts |> Misc.list_snoc |> Misc.swap in Some (i, xts, t) | _ -> None @@ -218,57 +221,57 @@ | (Ptr _), Int -> true | _ -> t1 = t2 - (* {{{ - let concretize ts = function - | Func (n, ats) when n = List.length ts -> + (* {{{+ let concretize ts = function+ | Func (n, ats) when n = List.length ts -> Func (n, List.map (subs_tvar ts) ats)- | _ -> - assertf "ERROR: bad application" + | _ ->+ assertf "ERROR: bad application" - let is_monotype t = + let is_monotype t = fold (fun b t -> b && (match t with Var _ -> false | _ -> true)) true t }}} *) let lookup_var = fun s i -> try Some (List.assoc i s.vars) with Not_found -> None let lookup_loc = fun s j -> try Some (List.assoc j s.locs) with Not_found -> None- - let rec unifyt s = function ++ let rec unifyt s = function | Num,_ | _, Num -> None- | ct, (Var i) - | (Var i), ct - (* when ct != Bool *) -> - begin match lookup_var s i with + | ct, (Var i)+ | (Var i), ct+ (* when ct != Bool *) ->+ begin match lookup_var s i with | Some ct' when ct = ct' -> Some s | Some _ -> None | None -> Some {s with vars = (i,ct) :: s.vars} end - | Ptr LFun, Ptr _ + | Ptr LFun, Ptr _ | Ptr _, Ptr LFun -> Some s | Ptr (Loc cl), Ptr (Lvar j) | Ptr (Lvar j), Ptr (Loc cl) ->- begin match lookup_loc s j with + begin match lookup_loc s j with | Some cl' when cl' = cl -> Some s | Some _ -> None | None -> Some {s with locs = (j,cl) :: s.locs} end- - | App (c1, t1s), App (c2, t2s) ++ | App (c1, t1s), App (c2, t2s) when c1 = c2 && List.length t1s = List.length t2s -> Misc.maybe_fold unifyt s (List.combine t1s t2s)- - | (t1, t2) when t1 = t2 -> ++ | (t1, t2) when t1 = t2 -> Some s | _ -> None- + let empty_sub = {vars = []; locs = []}- + let unifyWith s ats cts = let _ = asserts (List.length ats = List.length cts) "ERROR: unify sorts" in- List.combine ats cts - |> Misc.maybe_fold unifyt s - (* >> (fun so -> Printf.printf "unify: [%s] ~ [%s] = %s \n" + List.combine ats cts+ |> Misc.maybe_fold unifyt s+ (* >> (fun so -> Printf.printf "unify: [%s] ~ [%s] = %s \n" (String.concat "; " (List.map to_string ats)) (String.concat "; " (List.map to_string cts)) (match so with None -> "NONE" | Some s -> sub_to_string s))@@ -276,7 +279,7 @@ let unify = unifyWith empty_sub - let apply s = + let apply s = map begin fun t -> match t with | Var i -> (match lookup_var s i with Some t' -> t' | _ -> t) | Ptr (Lvar j) -> (match lookup_loc s j with Some l -> Ptr (Loc l) | _ -> t)@@ -284,30 +287,30 @@ end let rec fold f acc t = match t with- | Var _ | Int | Real | Bool | Obj | Num | Ptr _ - -> f acc t - | Func (_, ts) | App (_, ts) - -> List.fold_left (fold f) (f acc t) ts - - let vars_of_t = fold begin fun acc -> function - | Var i -> i :: acc + | Var _ | Int | Real | Bool | Obj | Num | Ptr _+ -> f acc t+ | Func (_, ts) | App (_, ts)+ -> List.fold_left (fold f) (f acc t) ts++ let vars_of_t = fold begin fun acc -> function+ | Var i -> i :: acc | _ -> acc end []- - let locs_of_t = fold begin fun acc -> function - | Ptr (Loc l) -> l :: acc ++ let locs_of_t = fold begin fun acc -> function+ | Ptr (Loc l) -> l :: acc | _ -> acc end []- + let subst_locs_vars lim = map begin function | Ptr (Loc l) when SM.mem l lim -> Var (SM.find l lim) | t -> t end (* API *)- let generalize ts = + let generalize ts = let locs = ts |> Misc.flap locs_of_t |> Misc.sort_and_compact in- let idx = ts |> Misc.flap vars_of_t |> Misc.list_max (-1) |> (+) 1 in + let idx = ts |> Misc.flap vars_of_t |> Misc.list_max (-1) |> (+) 1 in let lim = Misc.index_from idx locs |>: Misc.swap |> SM.of_list in List.map (subst_locs_vars lim) ts @@ -320,42 +323,42 @@ end -module Symbol = - struct +module Symbol =+ struct type t = string- + let mk_wild = let t,_ = Misc.mk_int_factory () in t <+> string_of_int <+> (^) "~A"- + let is_wild_fresh s = s = "_" let is_wild_any s = s.[0] = '~' let is_wild_pre s = s.[0] = '@' let is_wild s = is_wild_fresh s || is_wild_any s || is_wild_pre s - let is_safe s = + let is_safe s = let re = Str.regexp "[A-Za-z '~' '_' '\'' '@' ][0-9 a-z A-Z '_' '@' '\'' '.' '#']*$" in Str.string_match re s 0- - let of_string, to_string = ++ let of_string, to_string = let of_t = Hashtbl.create 117 in let to_t = Hashtbl.create 117 in let bind = fun s sy -> Hashtbl.replace of_t s sy; Hashtbl.replace to_t sy s in let f,_ = Misc.mk_string_factory "FIXPOINTSYMBOL_" in- ((fun s -> + ((fun s -> if is_wild_fresh s then mk_wild () else if is_safe s then s else try Hashtbl.find of_t s with Not_found -> let sy = f () in let _ = bind s sy in sy), (fun sy -> try Hashtbl.find to_t sy with Not_found -> sy))- + let to_string = fun s -> s (* if is_safe s then s else "'" ^ s ^ "'" *) let suffix = fun s suff -> of_string ((to_string s) ^ suff) let print fmt s =- to_string s |> Format.fprintf fmt "%s" + to_string s |> Format.fprintf fmt "%s" let vvprefix = "VV_" let vvsuffix = function@@ -372,26 +375,26 @@ let is_value_variable = (=) vvprefix let value_variable _ = vvprefix - module SMap = Misc.EMap (struct type t = string - let compare i1 i2 = compare i1 i2 + module SMap = Misc.EMap (struct type t = string+ let compare i1 i2 = compare i1 i2 let print = print end) module SSet = Misc.ESet (struct type t = string let compare i1 i2 = compare i1 i2 end) - (* let sm_length m = + (* let sm_length m = SMap.fold (fun _ _ i -> i+1) m 0 - let sm_filter f sm = - SMap.fold begin fun x y sm -> - if f x y then SMap.add x y sm else sm - end sm SMap.empty + let sm_filter f sm =+ SMap.fold begin fun x y sm ->+ if f x y then SMap.add x y sm else sm+ end sm SMap.empty let sm_to_list sm = SMap.fold (fun x y acc -> (x,y)::acc) sm []- - let sm_of_list xs = - List.fold_left (fun sm (k,v) -> SMap.add k v sm) SMap.empty xs ++ let sm_of_list xs =+ List.fold_left (fun sm (k,v) -> SMap.add k v sm) SMap.empty xs *) end@@ -399,8 +402,8 @@ module Constant = struct - type t = Int of int - | Real of float + type t = Int of int+ | Real of float | Lit of string * Sort.t let to_string = function@@ -411,34 +414,34 @@ let print fmt s = to_string s |> Format.fprintf fmt "%s" end- + type tag = int type brel = Eq (* equal *) | Ne (* not-equal *)- | Gt (* greater than *) + | Gt (* greater than *) | Ge (* greater than or equal *) | Lt (* less than *) | Le (* less than or equal *)- | Ueq (* unsorted-equality *) + | Ueq (* unsorted-equality *) | Une (* unsorted-disequality *) type bop = Plus | Minus | Times | Div | Mod (* NOTE: For "Mod" 2nd expr should be a constant or a var *) -type expr = expr_int * tag - +type expr = expr_int * tag+ and expr_int = | Con of Constant.t | Var of Symbol.t | App of Symbol.t * expr list- | Bin of expr * bop * expr + | Bin of expr * bop * expr | Ite of pred * expr * expr- | Fld of Symbol.t * expr (* NOTE: Fld (s, e) == App ("field"^s,[e]) *) - | Cst of expr * Sort.t + | Fld of Symbol.t * expr (* NOTE: Fld (s, e) == App ("field"^s,[e]) *)+ | Cst of expr * Sort.t | Bot | MExp of expr list- | MBin of expr * bop list * expr + | MBin of expr * bop list * expr and pred = pred_int * tag @@ -451,15 +454,15 @@ | Imp of pred * pred | Iff of pred * pred | Bexp of expr- | Atom of expr * brel * expr + | Atom of expr * brel * expr | MAtom of expr * brel list * expr | Forall of ((Symbol.t * Sort.t) list) * pred -let list_hash b xs = +let list_hash b xs = List.fold_left (fun v (_,id) -> 2*v + id) b xs module Hashcons (X : sig type t- val sub_equal : t -> t -> bool + val sub_equal : t -> t -> bool val hash : t -> int end) = struct module HashStruct = struct@@ -469,11 +472,11 @@ end module Hash = Weak.Make(HashStruct)- - let wrap = ++ let wrap = let tab = Hash.create 251 in let ctr = ref 0 in- fun e -> + fun e -> let res = Hash.merge tab (e, !ctr) in let _ = if snd res = !ctr then incr ctr in res@@ -486,14 +489,14 @@ type t = expr_int let sub_equal e1 e2 = match e1, e2 with- | Con c1, Con c2 -> + | Con c1, Con c2 -> c1 = c2- | MExp es1, MExp es2 -> + | MExp es1, MExp es2 -> es1 = es2- | Var x1, Var x2 -> + | Var x1, Var x2 -> x1 = x2 | App (s1, e1s), App (s2, e2s) ->- (s1 = s2) && + (s1 = s2) && (try List.for_all2 (==) e1s e2s with _ -> false) | Bin (e1, op1, e1'), Bin (e2, op2, e2') -> op1 = op2 && e1 == e2 && e1' == e2'@@ -505,27 +508,27 @@ s1 = s2 && e1 == e2 | Cst (e1, s1), Cst (e2, s2) -> s1 = s2 && e1 == e2- | _ -> + | _ -> false- + let hash = function- | Con (Constant.Int x) -> + | Con (Constant.Int x) -> x- | Con (Constant.Real x) -> + | Con (Constant.Real x) -> 64 + int_of_float x- | Con (Constant.Lit (s,_)) -> + | Con (Constant.Lit (s,_)) -> 32 + Hashtbl.hash s | MExp es ->- list_hash 6 es - | Var x -> + list_hash 6 es+ | Var x -> Hashtbl.hash x- | App (s, es) -> - list_hash ((Hashtbl.hash s) + 1) es - | Bin ((_,id1), op, (_,id2)) -> - (Hashtbl.hash op) + 1 + (2 * id1) + id2 - | MBin ((_,id1), op::_ , (_,id2)) -> - (Hashtbl.hash op) + 1 + (2 * id1) + id2 - | Ite ((_,id1), (_,id2), (_,id3)) -> + | App (s, es) ->+ list_hash ((Hashtbl.hash s) + 1) es+ | Bin ((_,id1), op, (_,id2)) ->+ (Hashtbl.hash op) + 1 + (2 * id1) + id2+ | MBin ((_,id1), op::_ , (_,id2)) ->+ (Hashtbl.hash op) + 1 + (2 * id1) + id2+ | Ite ((_,id1), (_,id2), (_,id3)) -> 32 + (4 * id1) + (2 * id2) + id3 | Fld (s, (_,id)) -> (Hashtbl.hash s) + 12 + id@@ -536,47 +539,47 @@ | _ -> assertf "pattern error in A.pred hash" end- + module ExprHashcons = Hashcons(ExprHashconsStruct) module PredHashconsStruct = struct- + type t = pred_int- + let sub_equal p1 p2 = match p1, p2 with- | True, True | False, False -> + | True, True | False, False -> true- | And p1s, And p2s | Or p1s, Or p2s -> + | And p1s, And p2s | Or p1s, Or p2s -> (try List.for_all2 (==) p1s p2s with _ -> false)- | Not p1, Not p2 -> + | Not p1, Not p2 -> p1 == p2- | Imp (p1, p1'), Imp (p2, p2') -> + | Imp (p1, p1'), Imp (p2, p2') -> p1 == p2 && p1' == p2' | Iff (p1,p1'), Iff (p2,p2') -> p1 == p2 && p1' == p2'- | Bexp e1, Bexp e2 -> + | Bexp e1, Bexp e2 -> e1 == e2 | Atom (e1, r1, e1'), Atom (e2, r2, e2') -> r1 = r2 && e1 == e2 && e1' == e2' | MAtom (e1, r1, e1'), MAtom (e2, r2, e2') -> r1 = r2 && e1 == e2 && e1' == e2'- | Forall(q1s,p1), Forall(q2s,p2) -> + | Forall(q1s,p1), Forall(q2s,p2) -> q1s = q2s && p1 == p2- | _ -> + | _ -> false- + let hash = function- | True -> + | True -> 0- | False -> + | False -> 1- | And ps -> + | And ps -> list_hash 2 ps- | Or ps -> + | Or ps -> list_hash 3 ps- | Not (_,id) -> - 8 + id + | Not (_,id) ->+ 8 + id | Imp ((_,id1), (_,id2)) -> 20 + (2 * id1) + id2 | Iff ((_,id1), (_,id2)) ->@@ -587,15 +590,15 @@ 36 + (Hashtbl.hash r) + (2 * id1) + id2 | MAtom ((_,id1), r, (_,id2)) -> 42 + (Hashtbl.hash r) + (2 * id1) + id2- | Forall(qs,(_,id)) -> + | Forall(qs,(_,id)) -> 50 + (2 * (Hashtbl.hash qs)) + id end- + module PredHashcons = Hashcons(PredHashconsStruct) let ewr = ExprHashcons.wrap let euw = ExprHashcons.unwrap-let pwr = PredHashcons.wrap +let pwr = PredHashcons.wrap let puw = PredHashcons.unwrap (* Constructors: Expressions *)@@ -612,20 +615,20 @@ let eModExp = fun (e, m) -> ewr (Bin (e, Mod, m)) let eVar = fun s -> ewr (Var s) let eApp = fun (s, es) -> ewr (App (s, es))-let eBin = fun (e1, op, e2) -> ewr (Bin (e1, op, e2)) +let eBin = fun (e1, op, e2) -> ewr (Bin (e1, op, e2)) -let eMBin = fun (e1, ops, e2) -> ewr (MBin (e1, ops, e2)) +let eMBin = fun (e1, ops, e2) -> ewr (MBin (e1, ops, e2)) let eIte = fun (ip,te,ee) -> ewr (Ite(ip,te,ee)) let eFld = fun (s,e) -> ewr (Fld (s,e)) let eCst = fun (e,t) -> ewr (Cst (e, t)) -let eTim = function - | (Con (Constant.Int n1), _), (Con (Constant.Int n2), _) -> +let eTim = function+ | (Con (Constant.Int n1), _), (Con (Constant.Int n2), _) -> ewr (Con (Constant.Int (n1 * n2)))- | (Con (Constant.Int 1), _), e2 -> - e2 - | (Con (Constant.Int (-1)), _), e2 -> - eBin (zero, Minus, e2) + | (Con (Constant.Int 1), _), e2 ->+ e2+ | (Con (Constant.Int (-1)), _), e2 ->+ eBin (zero, Minus, e2) | (e1, e2) -> eBin (e1, Times, e2) @@ -650,8 +653,8 @@ let pUequal = fun (e1,e2) -> pAtom (e1, Ueq, e2) -let pAnd = fun ps -> match Misc.flap conjuncts ps with - | [] -> pTrue +let pAnd = fun ps -> match Misc.flap conjuncts ps with+ | [] -> pTrue | [p] -> p | ps -> pwr (And (Misc.flap conjuncts ps)) @@ -669,14 +672,14 @@ let hash (_,x) = x end) -let bop_to_string = function +let bop_to_string = function | Plus -> "+" | Minus -> "-" | Times -> "*" | Div -> "/"- | Mod -> "mod" + | Mod -> "mod" -let brel_to_string = function +let brel_to_string = function | Eq -> "=" | Ne -> "!=" | Gt -> ">"@@ -686,179 +689,179 @@ | Ueq -> "~~" | Une -> "!~" -let print_brel ppf r = +let print_brel ppf r = F.fprintf ppf "%s" (brel_to_string r) -let print_binding ppf (s,t) = +let print_binding ppf (s,t) = F.fprintf ppf "%a:%a" Symbol.print s Sort.print t -let bind_to_string (s,t) = +let bind_to_string (s,t) = Printf.sprintf "%s:%s" (Symbol.to_string s) (Sort.to_string t) let rec print_expr ppf e = match euw e with- | Con c -> - F.fprintf ppf "%a" Constant.print c - | MExp es -> + | Con c ->+ F.fprintf ppf "%a" Constant.print c+ | MExp es -> F.fprintf ppf "[%a]" (Misc.pprint_many false " ; " print_expr) es- | Var s -> + | Var s -> F.fprintf ppf "%a" Symbol.print s- | App (s, es) -> - F.fprintf ppf "%a([%a])" + | App (s, es) ->+ F.fprintf ppf "%a([%a])" Symbol.print s (Misc.pprint_many false "; " print_expr) es | Bin (e1, op, e2) ->- F.fprintf ppf "(%a %s %a)" - print_expr e1 - (bop_to_string op) + F.fprintf ppf "(%a %s %a)"+ print_expr e1+ (bop_to_string op) print_expr e2 | MBin (e1, ops, e2) ->- F.fprintf ppf "(%a [%s] %a)" - print_expr e1 + F.fprintf ppf "(%a [%s] %a)"+ print_expr e1 (ops |>: bop_to_string |> String.concat " ; ") print_expr e2- - | Ite (ip, te, ee) -> - F.fprintf ppf "if %a then %a else %a" - print_pred ip ++ | Ite (ip, te, ee) ->+ F.fprintf ppf "if %a then %a else %a"+ print_pred ip print_expr te print_expr ee- + (* DEPRECATED TO HELP HS Parser- | Ite(ip,te,ee) -> - F.fprintf ppf "(%a ? %a : %a)" - print_pred ip + | Ite(ip,te,ee) ->+ F.fprintf ppf "(%a ? %a : %a)"+ print_pred ip print_expr te print_expr ee- *) + *) - | Fld(s, e) -> - F.fprintf ppf "%a.%s" print_expr e s + | Fld(s, e) ->+ F.fprintf ppf "%a.%s" print_expr e s | Cst(e,t) ->- F.fprintf ppf "(%a : %a)" - print_expr e + F.fprintf ppf "(%a : %a)"+ print_expr e Sort.print t | Bot ->- F.fprintf ppf "_|_" + F.fprintf ppf "_|_" and print_pred ppf p = match puw p with- | True -> + | True -> F.fprintf ppf "true"- | False -> + | False -> F.fprintf ppf "false" | Bexp (App (s, es), _) -> F.fprintf ppf "%a(%a)" Symbol.print s (Misc.pprint_many false ", " print_expr) es | Bexp e -> F.fprintf ppf "(Bexp %a)" print_expr e- | Not p -> + | Not p -> F.fprintf ppf "(~ (%a))" print_pred p- | Imp (p1, p2) -> - F.fprintf ppf "(%a => %a)" print_pred p1 print_pred p2 + | Imp (p1, p2) ->+ F.fprintf ppf "(%a => %a)" print_pred p1 print_pred p2 | Iff (p1, p2) ->- F.fprintf ppf "(%a <=> %a)" print_pred p1 print_pred p2 + F.fprintf ppf "(%a <=> %a)" print_pred p1 print_pred p2 | And ps -> begin match ps with [] -> F.fprintf ppf "true" | _ -> F.fprintf ppf "&& %a" (Misc.pprint_many_brackets true print_pred) ps end- | Or ps -> begin match ps with [] -> F.fprintf ppf "false" | _ -> + | Or ps -> begin match ps with [] -> F.fprintf ppf "false" | _ -> F.fprintf ppf "|| %a" (Misc.pprint_many_brackets true print_pred) ps end | Atom (e1, r, e2) -> (* F.fprintf ppf "@[(%a %s %a)@]" *) F.fprintf ppf "(%a %s %a)"- print_expr e1 - (brel_to_string r) + print_expr e1+ (brel_to_string r) print_expr e2 | MAtom (e1, rs, e2) ->- F.fprintf ppf "(%a [%a] %a)" + F.fprintf ppf "(%a [%a] %a)" (* F.fprintf ppf "@[(%a [%a] %a)@]" *)- print_expr e1 + print_expr e1 (Misc.pprint_many false " ; " print_brel) rs print_expr e2- | Forall (qs, p) -> - F.fprintf ppf "forall [%a] . %a" + | Forall (qs, p) ->+ F.fprintf ppf "forall [%a] . %a" (Misc.pprint_many false "; " print_binding) qs print_pred p- -let rec expr_to_string e = ++let rec expr_to_string e = match euw e with- | Con c -> + | Con c -> Constant.to_string c- | MExp es -> + | MExp es -> Printf.sprintf "[%s]" (es |>: expr_to_string |> String.concat " ; ")- | Var s -> + | Var s -> Symbol.to_string s | App (s, es) ->- Printf.sprintf "%s([%s])" + Printf.sprintf "%s([%s])" (Symbol.to_string s) (es |> List.map expr_to_string |> String.concat "; ") | Bin (e1, op, e2) ->- Printf.sprintf "(%s %s %s)" + Printf.sprintf "(%s %s %s)" (expr_to_string e1) (bop_to_string op) (expr_to_string e2) | MBin (e1, ops, e2) ->- Printf.sprintf "(%s [%s] %s)" - (expr_to_string e1) + Printf.sprintf "(%s [%s] %s)"+ (expr_to_string e1) (ops |> List.map bop_to_string |> String.concat "; ") (expr_to_string e2)- | Ite(ip,te,ee) -> - Printf.sprintf "(%s ? %s : %s)" + | Ite(ip,te,ee) ->+ Printf.sprintf "(%s ? %s : %s)" (pred_to_string ip) (expr_to_string te) (expr_to_string ee)- | Fld(s,e) -> - Printf.sprintf "%s.%s" (expr_to_string e) s + | Fld(s,e) ->+ Printf.sprintf "%s.%s" (expr_to_string e) s | Cst(e,t) -> Printf.sprintf "(%s : %s)" (expr_to_string e) (Sort.to_string t) | Bot ->- Printf.sprintf "_|_" + Printf.sprintf "_|_" -and pred_to_string p = +and pred_to_string p = match puw p with- | True -> + | True -> "true"- | False -> + | False -> "false" | Bexp e -> Printf.sprintf "(Bexp %s)" (expr_to_string e)- | Not p -> - Printf.sprintf "(~ (%s))" (pred_to_string p) - | Imp (p1, p2) -> + | Not p ->+ Printf.sprintf "(~ (%s))" (pred_to_string p)+ | Imp (p1, p2) -> Printf.sprintf "(%s => %s)" (pred_to_string p1) (pred_to_string p2) | Iff (p1, p2) -> Printf.sprintf "(%s <=> %s)" (pred_to_string p1) (pred_to_string p2)- | And ps -> + | And ps -> Printf.sprintf "&& [%s]" (List.map pred_to_string ps |> String.concat " ; ")- | Or ps -> + | Or ps -> Printf.sprintf "|| [%s]" (List.map pred_to_string ps |> String.concat ";") | Atom (e1, r, e2) ->- Printf.sprintf "(%s %s %s)" + Printf.sprintf "(%s %s %s)" (expr_to_string e1) (brel_to_string r) (expr_to_string e2) | MAtom (e1, rs, e2) ->- Printf.sprintf "(%s [%s] %s)" + Printf.sprintf "(%s [%s] %s)" (expr_to_string e1)- (List.map brel_to_string rs |> String.concat " ; ") + (List.map brel_to_string rs |> String.concat " ; ") (expr_to_string e2)- | Forall (qs,p) -> - Printf.sprintf "forall [%s] . %s" + | Forall (qs,p) ->+ Printf.sprintf "forall [%s] . %s" (List.map bind_to_string qs |> String.concat "; ") (pred_to_string p) let rec pred_map hp he fp fe p = let rec pm p = try PredHash.find hp p with Not_found -> begin- let p' = + let p' = match puw p with- | True | False as p1 -> + | True | False as p1 -> p1- | And ps -> - And (List.map pm ps) - | Or ps -> - Or (List.map pm ps) - | Not p -> - Not (pm p) - | Imp (p1, p2) -> + | And ps ->+ And (List.map pm ps)+ | Or ps ->+ Or (List.map pm ps)+ | Not p ->+ Not (pm p)+ | Imp (p1, p2) -> Imp (pm p1, pm p2) | Iff (p1, p2) -> Iff (pm p1, pm p2) | Bexp e ->- Bexp (expr_map hp he fp fe e) + Bexp (expr_map hp he fp fe e) | Atom (e1, r, e2) -> Atom (expr_map hp he fp fe e1, r, expr_map hp he fp fe e2) | MAtom (e1, rs, e2) ->@@ -866,19 +869,19 @@ | Forall (qs, p) -> Forall (qs, pm p) in let rv = fp (pwr p') in- let _ = PredHash.add hp p rv in + let _ = PredHash.add hp p rv in rv- end in pm p + end in pm p and expr_map hp he fp fe e = let rec em e = try ExprHash.find he e with Not_found -> begin- let e' = + let e' = match euw e with- | Con _ | Var _ | Bot as e1 -> + | Con _ | Var _ | Bot as e1 -> e1 | MExp es ->- MExp (List.map em es) + MExp (List.map em es) | App (f, es) -> App (f, List.map em es) | Bin (e1, op, e2) ->@@ -886,11 +889,11 @@ | MBin (e1, ops, e2) -> MBin (em e1, ops, em e2) | Ite (ip, te, ee) ->- Ite (pred_map hp he fp fe ip, em te, em ee) - | Fld (s, e1) -> - Fld (s, em e1) - | Cst (e1, t) -> - Cst (em e1, t) + Ite (pred_map hp he fp fe ip, em te, em ee)+ | Fld (s, e1) ->+ Fld (s, em e1)+ | Cst (e1, t) ->+ Cst (em e1, t) in let rv = fe (ewr e') in let _ = ExprHash.add he e rv in@@ -913,50 +916,50 @@ and expr_iter fp fe ew = begin match puw ew with- | Con _ | Var _ | Bot -> + | Con _ | Var _ | Bot -> () | MExp es -> List.iter (expr_iter fp fe) es- | App (_, es) -> + | App (_, es) -> List.iter (expr_iter fp fe) es- | Bin (e1, _, e2) -> + | Bin (e1, _, e2) -> expr_iter fp fe e1; expr_iter fp fe e2- | MBin (e1, _, e2) -> + | MBin (e1, _, e2) -> expr_iter fp fe e1; expr_iter fp fe e2- | Ite (ip, te, ee) -> + | Ite (ip, te, ee) -> pred_iter fp fe ip; expr_iter fp fe te; expr_iter fp fe ee- | Fld (_, e1) | Cst (e1, _) -> + | Fld (_, e1) | Cst (e1, _) -> expr_iter fp fe e1 end; fe ew let esub x e = function | (Var y), _ when x = y -> e- | _ as e1 -> e1 + | _ as e1 -> e1 let expr_subst hp he e x e' =- expr_map hp he id (esub x e') e + expr_map hp he id (esub x e') e let pred_subst hp he p x e' =- pred_map hp he id (esub x e') p + pred_map hp he id (esub x e') p -module Expression = +module Expression = struct- - module Hash = ExprHash - ++ module Hash = ExprHash+ let to_string = expr_to_string (* let print = fun fmt e -> Format.pp_print_string fmt (to_string e) *) let print = print_expr- + let show = print Format.std_formatter let map fp fe e = let hp = PredHash.create 251 in- let he = ExprHash.create 251 in - expr_map hp he fp fe e + let he = ExprHash.create 251 in+ expr_map hp he fp fe e let iter fp fe e = expr_iter fp fe e@@ -969,8 +972,8 @@ let support e = let xs = ref Symbol.SSet.empty in- iter un begin function - | (Var x), _ + iter un begin function+ | (Var x), _ | (App (x,_)),_ -> xs := Symbol.SSet.add x !xs | _ -> () end e;@@ -980,26 +983,26 @@ let has_bot p = let r = ref false in- iter un begin function + iter un begin function | Bot, _ -> r := true | _ -> ()- end p; + end p; !r end- + module Predicate = struct- module Hash = PredHash - + module Hash = PredHash+ let to_string = pred_to_string let print = print_pred let show = print Format.std_formatter- + let map fp fe p = let hp = PredHash.create 251 in- let he = ExprHash.create 251 in + let he = ExprHash.create 251 in pred_map hp he fp fe p- + let iter fp fe p = pred_iter fp fe p @@ -1011,35 +1014,35 @@ let support p = let xs = ref Symbol.SSet.empty in- iter un begin function - | (Var x), _ + iter un begin function+ | (Var x), _ | (App (x,_)),_ -> xs := Symbol.SSet.add x !xs; | _ -> ()- end p; + end p; Symbol.SSet.elements !xs |> List.sort compare (* let size p = let c = ref 0 in let f = fun _ -> incr c in- let _ = iter f f p in + let _ = iter f f p in !c let size p = let c = ref 0 in- let _ = iter (fun _ -> incr c) p in + let _ = iter (fun _ -> incr c) p in !c *)- + let unwrap = puw - let is_contra = + let is_contra = let t = PredHash.create 17 in let _ = [pFalse; pNot pTrue; pAtom (zero, Eq, one); pAtom (one, Eq, zero)]- |> List.iter (fun p-> PredHash.replace t p ()) in - fun p -> PredHash.mem t p - + |> List.iter (fun p-> PredHash.replace t p ()) in+ fun p -> PredHash.mem t p + let rec is_tauto = function | Atom(e1, Eq, e2), _ -> snd e1 == snd e2 | Atom(e1, Ueq, e2), _ -> snd e1 == snd e2@@ -1051,15 +1054,15 @@ let has_bot p = let r = ref false in- iter un begin function + iter un begin function | Bot, _ -> r := true | _ -> ()- end p; + end p; !r end -let print_stats _ = +let print_stats _ = Printf.printf "Ast Stats. [none] \n" @@ -1071,30 +1074,30 @@ | Bin (_, Div, _), _ -> true | _ -> false -let pull_divisor = function - | Bin (_, Div, (Con (Constant.Int i),_)), _ -> i +let pull_divisor = function+ | Bin (_, Div, (Con (Constant.Int i),_)), _ -> i | _ -> 1 let calc_cm e1 e2 =- pull_divisor e1 * pull_divisor e2 + pull_divisor e1 * pull_divisor e2 -let rec apply_mult m = function +let rec apply_mult m = function | Bin (e, Div, (Con (Constant.Int d),_)), _ -> let _ = assert ((m/d) * d = m) in- eTim ((eCon (Constant.Int (m/d))), e) + eTim ((eCon (Constant.Int (m/d))), e) | Bin (e1, op, e2), _ -> eBin (apply_mult m e1, op, apply_mult m e2)- | Con (Constant.Int i), _ -> + | Con (Constant.Int i), _ -> eCon (Constant.Int (i*m))- | e -> + | e -> eTim (eCon (Constant.Int m), e) -let rec pred_isdiv = function - | True,_ | False,_ -> +let rec pred_isdiv = function+ | True,_ | False,_ -> false- | And ps,_ | Or ps,_ -> + | And ps,_ | Or ps,_ -> List.exists pred_isdiv ps- | Not p, _ | Forall (_, p), _ -> + | Not p, _ | Forall (_, p), _ -> pred_isdiv p | Imp (p1, p2), _ -> pred_isdiv p1 || pred_isdiv p2@@ -1102,29 +1105,29 @@ pred_isdiv p1 || pred_isdiv p2 | Bexp e, _ -> expr_isdiv e- | Atom (e1, _, e2), _ -> + | Atom (e1, _, e2), _ -> expr_isdiv e1 || expr_isdiv e2 | _ -> failwith "Unexpected: pred_isdiv" let bound m e e1 e2 = pAnd [pAtom (apply_mult m e, Gt, apply_mult m e2);- pAtom(apply_mult m e, Le, apply_mult m e1)] + pAtom(apply_mult m e, Le, apply_mult m e1)] let rec fixdiv = function- | p when not (pred_isdiv p) -> + | p when not (pred_isdiv p) -> p | Atom ((Var _,_) as e, Eq, e1), _ | Atom ((Con _, _) as e, Eq, e1), _ -> bound (calc_cm e e1) e e1 (eBin (e1, Minus, one)) | And ps, _ ->- pAnd (List.map fixdiv ps) + pAnd (List.map fixdiv ps) | Or ps, _ -> pOr (List.map fixdiv ps) | Imp (p1, p2), _ -> pImp (fixdiv p1, fixdiv p2) | Iff (p1, p2), _ -> pIff (fixdiv p1, fixdiv p2)- | Not p, _ -> - pNot (fixdiv p) + | Not p, _ ->+ pNot (fixdiv p) | p -> p (***************************************************************************)@@ -1139,66 +1142,66 @@ | 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,_,_) -> +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 + end | None -> None -let rec sortcheck_expr g f e = +let rec sortcheck_expr g f e = match euw e with- | Bot -> + | Bot -> None- | Con (Constant.Int _) -> - Some Sort.Int - | Con (Constant.Real _) -> - Some Sort.Real + | Con (Constant.Int _) ->+ Some Sort.Int+ | Con (Constant.Real _) ->+ Some Sort.Real | Con (Constant.Lit (_, t)) ->- Some t + Some t | Var s -> sortcheck_sym f s- | Bin (e1, op, e2) -> + | Bin (e1, op, e2) -> sortcheck_op g f (e1, op, e2)- | Ite (p, e1, e2) -> - if sortcheck_pred g f p then + | Ite (p, e1, e2) ->+ if sortcheck_pred g f p then match Misc.map_pair (sortcheck_expr g f) (e1, e2) with- | (Some t1, Some t2) when t1 = t2 -> Some t1 + | (Some t1, Some t2) when t1 = t2 -> Some t1 | _ -> None else None- + | Cst (e1, t) -> begin match euw e1 with | App (uf, es) -> sortcheck_app g f (Some t) uf es | _ -> match sortcheck_expr g f e1 with | Some t1 when Sort.compat t t1 -> Some t- | _ -> None + | _ -> None end | App (uf, es) -> sortcheck_app g f None uf es- + | _ -> assertf "Ast.sortcheck_expr: unhandled expr = %s" (Expression.to_string e) (* TODO: OMG! 5 levels of matching!!!!! *) and sortcheck_app_sub g f so_expected uf es = let yikes uf = F.printf "sortcheck_app_sub: unknown sym = %s \n" (Symbol.to_string uf) in sortcheck_sym f uf- |> function None -> (yikes uf; None) | Some t -> - Sort.func_of_t t - |> function None -> None | Some (tyArity, i_ts, o_t) -> - let _ = asserts (List.length es = List.length i_ts) + |> function None -> (yikes uf; None) | Some t ->+ Sort.func_of_t t+ |> function None -> None | Some (tyArity, i_ts, o_t) ->+ let _ = asserts (List.length es = List.length i_ts) "ERROR: uf arg-arity error: uf=%s" uf in let e_ts = es |> List.map (sortcheck_expr g f) |> Misc.map_partial id in- if List.length e_ts <> List.length i_ts then - None + if List.length e_ts <> List.length i_ts then+ None else match Sort.unify e_ts i_ts with | None -> None@@ -1211,10 +1214,10 @@ | None -> None | Some s' -> Some (s', Sort.apply s' t) -and sortcheck_app g f so_expected uf es = - sortcheck_app_sub g f so_expected uf es - |> Misc.maybe_map snd - (* >> begin function +and sortcheck_app g f so_expected uf es =+ sortcheck_app_sub g f so_expected uf es+ |> Misc.maybe_map snd+ (* >> begin function | Some t -> Format.printf "sortcheck_app: e = %s , t = %s \n" (expr_to_string (eApp (uf, es))) (Sort.to_string t) | None -> Format.printf "sortcheck_app: e = %s FAILS\n"@@ -1224,33 +1227,33 @@ and sortcheck_op g f (e1, op, e2) =-(* DEBUGGING - let (s1, s2) = Misc.map_pair (sortcheck_expr g f) (e1, e2) in - let _ = match (s1, s2) with - | (Some t1, Some t2) -> F.printf "sortcheck_op : \n%s - %s\n" (Sort.to_string t1) (Sort.to_string t2) - | (_, Some t2) -> F.printf "sortcheck_op1 : \n - %s\n" (Sort.to_string t2) - | (Some t1, _) -> F.printf "sortcheck_op2 : \n%s \n" (Sort.to_string t1) - | (_, _) -> F.printf "sortcheck_op3 : \n" +(* DEBUGGING+ let (s1, s2) = Misc.map_pair (sortcheck_expr g f) (e1, e2) in+ let _ = match (s1, s2) with+ | (Some t1, Some t2) -> F.printf "sortcheck_op : \n%s - %s\n" (Sort.to_string t1) (Sort.to_string t2)+ | (_, Some t2) -> F.printf "sortcheck_op1 : \n - %s\n" (Sort.to_string t2)+ | (Some t1, _) -> F.printf "sortcheck_op2 : \n%s \n" (Sort.to_string t1)+ | (_, _) -> F.printf "sortcheck_op3 : \n" in *) match Misc.map_pair (sortcheck_expr g f) (e1, e2) with- | (Some Sort.Int, Some Sort.Int) + | (Some Sort.Int, Some Sort.Int) -> Some Sort.Int - | (Some Sort.Real, Some Sort.Real) + | (Some Sort.Real, Some Sort.Real) -> Some Sort.Real- + (* only allow when language is Haskell *)- | (Some (Sort.Ptr l), Some (Sort.Ptr l')) + | (Some (Sort.Ptr l), Some (Sort.Ptr l')) when (l = l' && sortcheck_loc f l = Some Sort.Num) -> Some (Sort.Ptr l)- + (* only allow when language is C *)- | (Some (Sort.Ptr s), Some Sort.Int) - | (Some Sort.Int, Some (Sort.Ptr s)) + | (Some (Sort.Ptr s), Some Sort.Int)+ | (Some Sort.Int, Some (Sort.Ptr s)) -> Some (Sort.Ptr s) (* only allow when language is C *)- | (Some (Sort.Ptr s), Some (Sort.Ptr s')) + | (Some (Sort.Ptr s), Some (Sort.Ptr s')) when op = Minus && s = s' -> Some Sort.Int @@ -1266,15 +1269,20 @@ | _ , Some Sort.Int, Some (Sort.Ptr l) | _ , Some (Sort.Ptr l), Some Sort.Int -> (sortcheck_loc f l = Some Sort.Num)- | _ , Some (Sort.Ptr l1), Some (Sort.Ptr l2) - when (sortcheck_loc f l1 = Some Sort.Num) - && (sortcheck_loc f l2 = Some Sort.Num)- -> true+ | _ , Some (Sort.Ptr l1), Some (Sort.Ptr l2)+ when ((sortcheck_loc f l1 = Some Sort.Num)+ && (sortcheck_loc f l2 = Some Sort.Num))+ || ((sortcheck_loc f l1 = Some Sort.Frac)+ && (sortcheck_loc f l2 = Some Sort.Frac))+ -> true + | _ , Some Sort.Real, Some (Sort.Ptr l)+ | _ , Some (Sort.Ptr l), Some Sort.Real+ -> sortcheck_loc f l = Some Sort.Frac | Eq, Some t1, Some t2 | Ne, Some t1, Some t2 -> t1 = t2- | Ueq, Some (Sort.App (_,_)), Some (Sort.App (_,_)) - | Une, Some (Sort.App (_,_)), Some (Sort.App (_,_)) + | Ueq, Some (Sort.App (_,_)), Some (Sort.App (_,_))+ | Une, Some (Sort.App (_,_)), Some (Sort.App (_,_)) -> true | _ , Some (Sort.App (tc,_)), _ when (g tc) (* tc is an interpreted tycon *)@@ -1285,34 +1293,37 @@ and sortcheck_pred g f p = match puw p with- | True - | False -> - true - | Bexp e ->+ | True+ | False ->+ true+ | Bexp e -> sortcheck_expr g f e = Some Sort.Bool - | Not p -> + | Not p -> sortcheck_pred g f p- | Imp (p1, p2) | Iff (p1, p2) -> + | Imp (p1, p2) | Iff (p1, p2) -> List.for_all (sortcheck_pred g f) [p1; p2]- | And ps + | And ps | Or ps -> List.for_all (sortcheck_pred g f) ps- - | Atom (e1, Ueq, e2) - when !Constants.ueq_all_sorts - -> (not (None = sortcheck_expr g f e1)) && - (not (None = sortcheck_expr g f e2)) - - | Atom ((Con (Constant.Int(0)),_), _, e) - | Atom (e, _, (Con (Constant.Int(0)),_)) ++ | Atom (e1, Ueq, e2)+ when !Constants.ueq_all_sorts+ -> (not (None = sortcheck_expr g f e1)) &&+ (not (None = sortcheck_expr g f e2))++ | Atom ((Con (Constant.Int(0)),_), _, e)+ | Atom (e, _, (Con (Constant.Int(0)),_)) when not (!Constants.strictsortcheck) -> not (None = sortcheck_expr g f e)- - | Atom ((Var x, _) , Eq, (App (uf, es), _))- | Atom ((App (uf, es), _), Eq, (Var x, _))- -> begin match sortcheck_sym f x with - | None -> false - | Some tx -> not (None = sortcheck_app g f (Some tx) uf es)++ | Atom (((Con _, _) as e) , Eq, (App (uf, es), _))+ | Atom ((App (uf, es), _), Eq, ((Con _, _) as e))+ | Atom (((Var _, _) as e) , Eq, (App (uf, es), _))+ | Atom ((App (uf, es), _), Eq, ((Var _, _) as e))+ (* -> begin match sortcheck_sym f x with *)+ -> begin match sortcheck_expr g f e with+ | None -> false+ | Some t -> not (None = sortcheck_app g f (Some t) uf es) end | Atom (((App (uf1, e1s), _) as e1), Eq, ((App (uf2, e2s), _) as e2))@@ -1320,9 +1331,9 @@ 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, None) -> false | (None, Some t2) -> not (None = sortcheck_app g f (Some t2) uf1 e1s)- | (Some t1, None) -> not (None = sortcheck_app g f (Some t1) uf2 e2s) + | (Some t1, None) -> not (None = sortcheck_app g f (Some t1) uf2 e2s) end | Atom (e1, r, e2) ->@@ -1335,7 +1346,7 @@ (* and sortcheck_pred f p = sortcheck_pred' f p- >> (fun b -> if not b then F.eprintf "WARNING: Malformed Lhs Pred (%a)\n" Predicate.print p) + >> (fun b -> if not b then F.eprintf "WARNING: Malformed Lhs Pred (%a)\n" Predicate.print p) *) let opt_to_string p = function@@ -1344,11 +1355,11 @@ (* API *)-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) +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 (*@@ -1356,7 +1367,7 @@ (expr_to_string (eApp (uf, es))) n (Sort.sub_to_string s)- (Sort.to_string t) + (Sort.to_string t) (opt_to_string Sort.to_string tExp) in assertf "%s" msg@@ -1365,7 +1376,7 @@ (*-let sortcheck_pred f p = +let sortcheck_pred f p = sortcheck_pred f p >> (fun b -> ignore <| F.printf "sortcheck_pred: p = %a, res = %b\n" Predicate.print p b)@@ -1379,7 +1390,7 @@ let rec remove_bot pol ((p, _) as pred) = match p with- | Not p -> + | Not p -> pNot (remove_bot (not pol) p) | Imp (p, q) -> pImp (remove_bot (not pol) p, remove_bot pol q)@@ -1387,31 +1398,31 @@ pForall (qs, remove_bot pol p) | And ps -> ps |> List.map (remove_bot pol) |> pAnd- | Or ps -> + | Or ps -> ps |> List.map (remove_bot pol) |> pOr | Bexp e when Expression.has_bot e -> pred_of_bool pol- | Atom (e1, _, e2) when Expression.has_bot e1 || Expression.has_bot e2 -> + | Atom (e1, _, e2) when Expression.has_bot e1 || Expression.has_bot e2 -> pred_of_bool pol- | _ -> + | _ -> pred -let remove_bot p = - if Predicate.has_bot p - then remove_bot true p +let remove_bot p =+ if Predicate.has_bot p+ then remove_bot true p else p let symm_brel = function- | Eq -> Eq - | Ueq -> Ueq - | Ne -> Ne - | Une -> Une + | Eq -> Eq+ | Ueq -> Ueq+ | Ne -> Ne+ | Une -> Une | Gt -> Lt | Ge -> Le | Lt -> Gt | Le -> Ge -let neg_brel = function +let neg_brel = function | Eq -> Ne | Ueq -> Une | Ne -> Eq@@ -1423,30 +1434,30 @@ let rec push_neg ?(neg=false) ((p, _) as pred) = match p with- | True -> + | True -> if neg then pFalse else pred- | False -> + | False -> if neg then pTrue else pred- | Bexp _ -> + | Bexp _ -> if neg then pNot pred else pred- | Not p -> + | Not p -> push_neg ~neg:(not neg) p- | Imp (p, q) -> + | Imp (p, q) -> if neg then pAnd [push_neg p; push_neg ~neg:true q] else pImp (push_neg p, push_neg q) | Iff (p, q) -> if neg then pIff (p, push_neg ~neg:true q) else pIff (push_neg p, push_neg q)- | Forall (qs, p) -> + | Forall (qs, p) -> let pred' = pForall (qs, push_neg ~neg:false p) in if neg then pNot pred' else pred'- | And ps -> - List.map (push_neg ~neg:neg) ps + | And ps ->+ List.map (push_neg ~neg:neg) ps |> if neg then pOr else pAnd- | Or ps -> - List.map (push_neg ~neg:neg) ps + | Or ps ->+ List.map (push_neg ~neg:neg) ps |> if neg then pAnd else pOr- | Atom (e1, brel, e2) -> + | Atom (e1, brel, e2) -> if neg then pAtom (e1, neg_brel brel, e2) else pred | _ -> failwith "Unexpected: push_neg" @@ -1454,15 +1465,15 @@ let rec simplify_pred ((p, _) as pred) = match p with | Not p -> pNot (simplify_pred p)- | Imp (p, q) -> pImp (simplify_pred p, simplify_pred q) + | Imp (p, q) -> pImp (simplify_pred p, simplify_pred q) | Forall (qs, p) -> pForall (qs, simplify_pred p)- | And ps -> ps |> List.map simplify_pred - |> List.filter (not <.> Predicate.is_tauto) + | And ps -> ps |> List.map simplify_pred+ |> List.filter (not <.> Predicate.is_tauto) |> (function | [] -> pTrue | [p] -> p | _ when List.exists Predicate.is_contra ps -> pFalse | _ -> pAnd ps)- | Or ps -> ps |> List.map simplify_pred + | Or ps -> ps |> List.map simplify_pred |> List.filter (not <.> Predicate.is_contra) |> (function [] -> pFalse | [p] -> p@@ -1477,13 +1488,13 @@ module Subst = struct type t = expr Symbol.SMap.t- - let valid xes = - xes |> List.split ++ let valid xes =+ xes |> List.split |> Misc.app_snd (Misc.flap Expression.support) |> Misc.uncurry Misc.disjoint- - ++ let extend s (x, e) = let s = Symbol.SMap.map (esub x e) s in if Symbol.SMap.mem x s then@@ -1495,18 +1506,18 @@ let empty = Symbol.SMap.empty let is_empty = Symbol.SMap.is_empty- let to_list = Symbol.SMap.to_list + let to_list = Symbol.SMap.to_list let apply = Misc.flip Symbol.SMap.maybe_find let of_list = fun xes -> List.fold_left extend empty xes let simultaneous_of_list = Symbol.SMap.of_list- let compose s t = + let compose s t = let s' = Symbol.SMap.fold (fun x e s -> Symbol.SMap.map (esub x e) s) t s in Symbol.SMap.fold (fun x e s -> if Symbol.SMap.mem x s then s else Symbol.SMap.add x e s) t s' let print_sub = fun ppf (x,e) -> F.fprintf ppf "[%a:=%a]" Symbol.print x Expression.print e let print = fun ppf -> to_list <+> F.fprintf ppf "%a" (Misc.pprint_many false "" print_sub)- + (* fun s1 s2 -> Symbol.SMap.fold (fun x e s -> extend s (x, e)) s2 s1 *) (* let apply = Misc.flip Symbol.SMap.maybe_find *) @@ -1518,25 +1529,25 @@ (**************************************************************************) module Horn = struct- + type pr = string * string list type gd = C of pred | K of pr- type t = pr * gd list + type t = pr * gd list - let print_pr ppf (x, xs) = - Format.fprintf ppf "%s(%s)" x (String.concat "," xs) - - let print_gd ppf = function + let print_pr ppf (x, xs) =+ Format.fprintf ppf "%s(%s)" x (String.concat "," xs)++ let print_gd ppf = function | C p -> Predicate.print ppf p- | K x -> print_pr ppf x + | K x -> print_pr ppf x - let print ppf (hd, gds) = - Format.fprintf ppf "%a :- %a." - print_pr hd + let print ppf (hd, gds) =+ Format.fprintf ppf "%a :- %a."+ print_pr hd (Misc.pprint_many false "," print_gd) gds - let support_pr = snd - let support_gd = function K pr -> support_pr pr | C p -> p |> Predicate.support |> List.map Symbol.to_string + let support_pr = snd+ let support_gd = function K pr -> support_pr pr | C p -> p |> Predicate.support |> List.map Symbol.to_string let support = fun (hd, gds) -> (support_pr hd) ++ (Misc.flap support_gd gds) end @@ -1544,11 +1555,11 @@ let simplify_pred = remove_bot <+> simplify_pred -let esub_su su e = match e with +let esub_su su e = match e with | ((Var y), _) -> Misc.maybe_default (Subst.apply su y) e | _ -> e -(* ORIG +(* ORIG let substs_pred = fun p su -> su |> Subst.to_list |> Predicate.substs p |> simplify_pred *) @@ -1560,10 +1571,10 @@ (****************************************************************************) -exception DoesNotUnify +exception DoesNotUnify -let rec pUnify (p1, p2) = - let res = +let rec pUnify (p1, p2) =+ let res = match p1, p2 with | (Atom (e1, r1, e1'), _), (Atom (e2, r2, e2'), _) when r1 = r2 -> let s1 = eUnify (e1, e2) in@@ -1576,22 +1587,22 @@ pUnify (p1, p2) | (Imp (p1, p1'), _), (Imp (p2, p2'), _) -> psUnify ([p1; p1'], [p2; p2'])- - | (And p1s, _), (And p2s, _) - | (Or p1s, _), (Or p2s, _) ++ | (And p1s, _), (And p2s, _)+ | (Or p1s, _), (Or p2s, _) when List.length p1s = List.length p2s -> psUnify (p1s, p2s) | _, _ -> raise DoesNotUnify in- let _ = if mydebug then - (Format.printf "pUnify: p1 is %a, p2 is %a, subst = %a \n" + let _ = if mydebug then+ (Format.printf "pUnify: p1 is %a, p2 is %a, subst = %a \n" Predicate.print p1 Predicate.print p2 Subst.print (Subst.of_list res)) in res and psUnify (p1s, p2s) = let _ = asserts (List.length p1s = List.length p2s) "psUnify" in List.fold_left2 begin fun s p1 p2 ->- (p1, p2) + (p1, p2) |> Misc.map_pair (fun p -> Predicate.substs p s) |> pUnify |> (fun s' -> s' ++ s)@@ -1614,22 +1625,22 @@ esUnify (e1s, e2s) | e, (Var x, _) | (Var x, _), e when Symbol.is_wild x -> [(x, e)]- | _, _ -> raise DoesNotUnify + | _, _ -> raise DoesNotUnify and esUnify (e1s, e2s) = let _ = asserts (List.length e1s = List.length e2s) "esUnify" in List.fold_left2 begin fun s e1 e2 ->- (e1, e2) + (e1, e2) |> Misc.map_pair (fun e -> Expression.substs e s) |> eUnify |> (fun s' -> s' ++ s) end [] e1s e2s (* API *)-let unify_pred p1 p2 = try pUnify (p1, p2) |> Subst.of_list |> some with DoesNotUnify -> None +let unify_pred p1 p2 = try pUnify (p1, p2) |> Subst.of_list |> some with DoesNotUnify -> None let into_of_expr = function Con (Constant.Int i), _ -> Some i | _ -> None -let symm_pred = function +let symm_pred = function | Atom (e1, r, e2), _ -> pAtom (e2, symm_brel r, e1) | p -> p @@ -1637,11 +1648,11 @@ let rec expr_subst hp he e x e' = let rec esub e = try ExprHash.find he e with Not_found -> begin- let rv = + let rv = match euw e with | Var y when x = y ->- e' - | Con _ | Var _ -> + e'+ | Con _ | Var _ -> e | App (s, es) -> App (s, List.map esub es) |> ewr@@ -1652,7 +1663,7 @@ | Fld (s, e1) -> Fld (s, esub e1) |> ewr in let _ = ExprHash.add he e rv in- rv + rv end in esub e and pred_subst hp he e x e' =@@ -1671,7 +1682,7 @@ | Atom (_) -> e | Leq(x,y) -> pwr (Leq(expr_subst h he x v vv, expr_subst h he y v vv)) in s e-}}} *) +}}} *) (** {{{ let rec support pred = let h = Hash.create 251 in@@ -1687,14 +1698,14 @@ and s1 exp = match euw exp with Constant(_) -> ()- | Application (func, args) -> + | Application (func, args) -> add func; List.iter s args | Variable(sym) -> add sym | Sum(args) -> List.iter s args | Coeff(c,t) -> s t | Ite _ -> failwith "ite not supported" in s exp in- + let rec s exp = try Hash.find h exp with Not_found -> Hash.add h exp (); s1 exp@@ -1710,32 +1721,32 @@ | Leq (x,y) -> se x; se y | Atom (s) -> () in s pred; List.rev !res- + let h = PredHash.create 251 in let rec ip p = let _ = f p in if not (PredHash.mem h p) then begin let _ = PredHash.add h p () in match puw p with- | And ps | Or ps -> + | And ps | Or ps -> List.iter ip plist- | Not p | Forall (_,p) -> - ip p - | Imp (p1, p2) -> + | Not p | Forall (_,p) ->+ ip p+ | Imp (p1, p2) -> ip p1; ip p2 | _ -> () end in- ip p + ip p }}} *) (* {{{- + (* Translate predicate to a satisfiability-equivalent predicate without Ite *)- + let temp_ctr = ref 0 let new_temp () = let n = "$$$" ^ (string_of_int !temp_ctr) in (temp_ctr := !temp_ctr + 1; n)- + let elim_ite sp = let cnsts = ref [] in let he = Expression.Hash.create 251 in@@ -1746,7 +1757,7 @@ and te1 e = match euw e with Constant(c) -> e- | Application (func, args) -> + | Application (func, args) -> ewr (Application (func, List.map te args)) | Variable(v) -> ewr (Variable(v)) | Sum(args) -> ewr (Sum(List.map te args))@@ -1760,7 +1771,7 @@ cnsts := pwr (Or [i; pwr (Equality(temp,(ev)))]) :: (!cnsts); temp end- and tp p = + and tp p = try Hash.find hp p with Not_found -> (let foo = tp1 p in Hash.add hp p foo; foo) and tp1 p =
external/fixpoint/ast.mli view
@@ -53,6 +53,7 @@ val to_string : t -> string val print : Format.formatter -> t -> unit val t_num : t+ val t_frac : t val t_obj : t val t_bool : t val t_int : t
external/fixpoint/fixLex.mll view
@@ -131,6 +131,7 @@ | "mod" { MOD } | "obj" { OBJ } | "num" { NUM }+ | "frac" { FRAC } | "int" { INT } | "real" { REAL } | "ptr" { PTR }
external/fixpoint/fixParse.mly view
@@ -71,7 +71,7 @@ %token TIMES %token DIV %token QM DOT ASGN-%token OBJ REAL INT NUM PTR LFUN BOOL UNINT FUNC LIT+%token OBJ REAL INT NUM PTR LFUN BOOL UNINT FUNC LIT FRAC %token SRT AXM CON CST WF SOL QUL KUT BIND ADP DDP %token ENV GRD LHS RHS REF @@ -172,6 +172,7 @@ | PTR LPAREN Id RPAREN { So.t_ptr (So.Loc $3) } | OBJ { So.t_obj } | NUM { So.t_num } + | FRAC { So.t_frac } | TVAR LPAREN Num RPAREN { So.t_generic $3 } | FUNC LPAREN sorts RPAREN { So.t_func 0 $3 } | FUNC LPAREN Num COMMA sorts RPAREN { So.t_func $3 $5 }
external/fixpoint/fixpoint.native-i386-linux view
binary file changed (1688841 → 1693827 bytes)
external/fixpoint/fixpoint.native-i686-w64-mingw32 view
file too large to diff
external/fixpoint/fixpoint.native-x86_64-darwin view
file too large to diff
external/fixpoint/fixpoint.native-x86_64-linux view
file too large to diff
external/fixpoint/predAbs.ml view
@@ -690,64 +690,6 @@ let (ch, me) = refine me c in (ch, {me with seen = IS.add (C.id_of_t c) me.seen}) -(* LAZYINST -let refine me c =- let lps = lazy (get_lhs me c) in- let (_,_,ra2s) as r = C.rhs_of_t c in- let (ins, rcs) = BS.time "rhs_cands" (Misc.flap (rhs_cands me lps)) ra2s in- if rcs = [] then - let _ = me.stat_emptyRHS += 1 in- (false, me)- else if BS.time "lhs_contra" (List.exists P.is_contra) (Lazy.force lps) then - let _ = me.stat_unsatLHS += 1 in- let _ = me.stat_umatches += List.length rcs in- (ch, me)- else- let lps = Lazy.force lps in- let rcs = List.filter (fun (_,p) -> not (P.is_contra p)) rcs in- let lt = PH.create 17 in- let _ = List.iter (fun p -> PH.add lt p ()) lps in- let (x1,x2) = List.partition (fun (_,p) -> PH.mem lt p) rcs in- let _ = me.stat_matches += (List.length x1) in- let kqs1 = List.map fst x1 in- (if C.is_simple c - then (ignore(me.stat_simple_refines += 1); kqs1) - else let senv = C.senv_of_t c in- let vv = C.vv_of_t c in- let t = C.sort_of_t c in- kqs1 ++ (BS.time "check tp" (check_tp me senv vv t lps) x2))- |> p_update me (get_rhs_kvars c)- |> (fun (ch', z) -> (ch || ch', z))--let refine me c =- let (_,_,ra2s) as r2 = C.rhs_of_t c in- let k2s = r2 |> C.kvars_of_reft |> List.map snd in- let rcs = BS.time "rhs_cands" (Misc.flap (rhs_cands me c)) ra2s in- if rcs = [] then- let _ = me.stat_emptyRHS += 1 in- (false, me)- else- let lps = BS.time "preds_of_lhs" (C.preds_of_lhs (read me)) c in- if BS.time "lhs_contra" (List.exists P.is_contra) lps then - let _ = me.stat_unsatLHS += 1 in- let _ = me.stat_umatches += List.length rcs in- (false, me)- else - let rcs = List.filter (fun (_,p) -> not (P.is_contra p)) rcs in- let lt = PH.create 17 in- let _ = List.iter (fun p -> PH.add lt p ()) lps in- let (x1,x2) = List.partition (fun (_,p) -> PH.mem lt p) rcs in- let _ = me.stat_matches += (List.length x1) in- let kqs1 = List.map fst x1 in- (if C.is_simple c - then (ignore(me.stat_simple_refines += 1); kqs1) - else let senv = C.senv_of_t c in- let vv = C.vv_of_t c in- let t = C.sort_of_t c in- kqs1 ++ (BS.time "check tp" (check_tp me senv vv t lps) x2))- |> p_update me k2s-*)- let refine me c = let me = me |> (!Co.cex <?> cx_iter c) in let (b, me) = refine me c in
+ external/ocamlgraph/src/dot_lexer.ml view
@@ -0,0 +1,386 @@+# 20 "src/dot_lexer.mll"+ + open Lexing+ open Dot_ast+ open Dot_parser++ let string_buf = Buffer.create 1024++ let keyword =+ let h = Hashtbl.create 17 in+ List.iter + (fun (s,k) -> Hashtbl.add h s k)+ [+ "strict", STRICT;+ "graph", GRAPH;+ "digraph", DIGRAPH;+ "subgraph", SUBGRAPH;+ "node", NODE;+ "edge", EDGE;+ ];+ fun s -> let s = String.lowercase s in Hashtbl.find h s+++# 25 "src/dot_lexer.ml"+let __ocaml_lex_tables = {+ Lexing.lex_base = + "\000\000\238\255\239\255\240\255\241\255\078\000\088\000\098\000\+ \176\000\245\255\246\255\247\255\248\255\249\255\250\255\251\255\+ \252\255\114\000\001\000\005\000\254\255\002\000\253\255\191\000\+ \244\255\211\000\221\000\157\000\252\255\253\255\002\000\255\255\+ \254\255\032\000\252\255\253\255\254\255\255\255\054\000\253\255\+ \254\255\015\000\255\255";+ Lexing.lex_backtrk = + "\255\255\255\255\255\255\255\255\255\255\013\000\017\000\012\000\+ \017\000\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\017\000\017\000\000\000\255\255\255\255\255\255\255\255\+ \255\255\013\000\013\000\255\255\255\255\255\255\002\000\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\001\000\255\255";+ Lexing.lex_default = + "\001\000\000\000\000\000\000\000\000\000\255\255\255\255\255\255\+ \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\255\255\021\000\255\255\000\000\021\000\000\000\255\255\+ \000\000\255\255\255\255\029\000\000\000\000\000\255\255\000\000\+ \000\000\035\000\000\000\000\000\000\000\000\000\040\000\000\000\+ \000\000\255\255\000\000";+ Lexing.lex_trans = + "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\019\000\019\000\020\000\020\000\019\000\019\000\019\000\+ \000\000\000\000\019\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \019\000\000\000\004\000\018\000\032\000\019\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\015\000\008\000\006\000\017\000\+ \005\000\005\000\005\000\005\000\005\000\005\000\005\000\005\000\+ \005\000\005\000\016\000\014\000\003\000\013\000\042\000\000\000\+ \000\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\010\000\036\000\009\000\037\000\007\000\+ \041\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\012\000\026\000\011\000\005\000\005\000\+ \005\000\005\000\005\000\005\000\005\000\005\000\005\000\005\000\+ \025\000\025\000\025\000\025\000\025\000\025\000\025\000\025\000\+ \025\000\025\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\007\000\022\000\000\000\000\000\000\000\+ \000\000\021\000\000\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\007\000\007\000\000\000\000\000\031\000\+ \000\000\007\000\000\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\007\000\007\000\024\000\023\000\000\000\+ \005\000\005\000\005\000\005\000\005\000\005\000\005\000\005\000\+ \005\000\005\000\000\000\000\000\000\000\000\000\024\000\025\000\+ \025\000\025\000\025\000\025\000\025\000\025\000\025\000\025\000\+ \025\000\030\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \002\000\255\255\255\255\025\000\025\000\025\000\025\000\025\000\+ \025\000\025\000\025\000\025\000\025\000\026\000\026\000\026\000\+ \026\000\026\000\026\000\026\000\026\000\026\000\026\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \034\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\039\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\028\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000";+ Lexing.lex_check = + "\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\000\000\000\000\018\000\021\000\000\000\019\000\019\000\+ \255\255\255\255\019\000\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \000\000\255\255\000\000\000\000\030\000\019\000\255\255\255\255\+ \255\255\255\255\255\255\255\255\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\041\000\255\255\+ \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\033\000\000\000\033\000\000\000\+ \038\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\005\000\000\000\005\000\005\000\+ \005\000\005\000\005\000\005\000\005\000\005\000\005\000\005\000\+ \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\+ \006\000\006\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\007\000\017\000\255\255\255\255\255\255\+ \255\255\017\000\255\255\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\007\000\007\000\255\255\255\255\027\000\+ \255\255\007\000\255\255\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\007\000\007\000\008\000\008\000\255\255\+ \008\000\008\000\008\000\008\000\008\000\008\000\008\000\008\000\+ \008\000\008\000\255\255\255\255\255\255\255\255\008\000\023\000\+ \023\000\023\000\023\000\023\000\023\000\023\000\023\000\023\000\+ \023\000\027\000\255\255\255\255\255\255\255\255\255\255\255\255\+ \000\000\018\000\021\000\025\000\025\000\025\000\025\000\025\000\+ \025\000\025\000\025\000\025\000\025\000\026\000\026\000\026\000\+ \026\000\026\000\026\000\026\000\026\000\026\000\026\000\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \033\000\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\038\000\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\027\000\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255";+ Lexing.lex_base_code = + "";+ Lexing.lex_backtrk_code = + "";+ Lexing.lex_default_code = + "";+ Lexing.lex_trans_code = + "";+ Lexing.lex_check_code = + "";+ Lexing.lex_code = + "";+}++let rec token lexbuf =+ __ocaml_lex_token_rec lexbuf 0+and __ocaml_lex_token_rec lexbuf __ocaml_lex_state =+ match Lexing.engine __ocaml_lex_tables __ocaml_lex_state lexbuf with+ | 0 ->+# 52 "src/dot_lexer.mll"+ ( token lexbuf )+# 191 "src/dot_lexer.ml"++ | 1 ->+# 54 "src/dot_lexer.mll"+ ( token lexbuf )+# 196 "src/dot_lexer.ml"++ | 2 ->+# 56 "src/dot_lexer.mll"+ ( comment lexbuf; token lexbuf )+# 201 "src/dot_lexer.ml"++ | 3 ->+# 58 "src/dot_lexer.mll"+ ( COLON )+# 206 "src/dot_lexer.ml"++ | 4 ->+# 60 "src/dot_lexer.mll"+ ( COMMA )+# 211 "src/dot_lexer.ml"++ | 5 ->+# 62 "src/dot_lexer.mll"+ ( SEMICOLON )+# 216 "src/dot_lexer.ml"++ | 6 ->+# 64 "src/dot_lexer.mll"+ ( EQUAL )+# 221 "src/dot_lexer.ml"++ | 7 ->+# 66 "src/dot_lexer.mll"+ ( LBRA )+# 226 "src/dot_lexer.ml"++ | 8 ->+# 68 "src/dot_lexer.mll"+ ( RBRA )+# 231 "src/dot_lexer.ml"++ | 9 ->+# 70 "src/dot_lexer.mll"+ ( LSQ )+# 236 "src/dot_lexer.ml"++ | 10 ->+# 72 "src/dot_lexer.mll"+ ( RSQ )+# 241 "src/dot_lexer.ml"++ | 11 ->+# 74 "src/dot_lexer.mll"+ ( EDGEOP )+# 246 "src/dot_lexer.ml"++ | 12 ->+let+# 75 "src/dot_lexer.mll"+ s+# 252 "src/dot_lexer.ml"+= Lexing.sub_lexeme lexbuf lexbuf.Lexing.lex_start_pos lexbuf.Lexing.lex_curr_pos in+# 76 "src/dot_lexer.mll"+ ( try keyword s with Not_found -> ID (Ident s) )+# 256 "src/dot_lexer.ml"++ | 13 ->+let+# 77 "src/dot_lexer.mll"+ s+# 262 "src/dot_lexer.ml"+= Lexing.sub_lexeme lexbuf lexbuf.Lexing.lex_start_pos lexbuf.Lexing.lex_curr_pos in+# 78 "src/dot_lexer.mll"+ ( ID (Number s) )+# 266 "src/dot_lexer.ml"++ | 14 ->+# 80 "src/dot_lexer.mll"+ ( Buffer.clear string_buf; + let s = string lexbuf in+ ID (String s) )+# 273 "src/dot_lexer.ml"++ | 15 ->+# 84 "src/dot_lexer.mll"+ ( Buffer.clear string_buf; + html lexbuf; + ID (Html (Buffer.contents string_buf)) )+# 280 "src/dot_lexer.ml"++ | 16 ->+# 88 "src/dot_lexer.mll"+ ( EOF )+# 285 "src/dot_lexer.ml"++ | 17 ->+let+# 89 "src/dot_lexer.mll"+ c+# 291 "src/dot_lexer.ml"+= Lexing.sub_lexeme_char lexbuf lexbuf.Lexing.lex_start_pos in+# 90 "src/dot_lexer.mll"+ ( failwith ("Dot_lexer: invalid character " ^ String.make 1 c) )+# 295 "src/dot_lexer.ml"++ | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_token_rec lexbuf __ocaml_lex_state++and string lexbuf =+ __ocaml_lex_string_rec lexbuf 27+and __ocaml_lex_string_rec lexbuf __ocaml_lex_state =+ match Lexing.engine __ocaml_lex_tables __ocaml_lex_state lexbuf with+ | 0 ->+# 94 "src/dot_lexer.mll"+ ( Buffer.contents string_buf )+# 306 "src/dot_lexer.ml"++ | 1 ->+# 96 "src/dot_lexer.mll"+ ( Buffer.add_char string_buf '"';+ string lexbuf )+# 312 "src/dot_lexer.ml"++ | 2 ->+let+# 98 "src/dot_lexer.mll"+ c+# 318 "src/dot_lexer.ml"+= Lexing.sub_lexeme_char lexbuf lexbuf.Lexing.lex_start_pos in+# 99 "src/dot_lexer.mll"+ ( Buffer.add_char string_buf c;+ string lexbuf )+# 323 "src/dot_lexer.ml"++ | 3 ->+# 102 "src/dot_lexer.mll"+ ( failwith ("Dot_lexer: unterminated string literal") )+# 328 "src/dot_lexer.ml"++ | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_string_rec lexbuf __ocaml_lex_state++and html lexbuf =+ __ocaml_lex_html_rec lexbuf 33+and __ocaml_lex_html_rec lexbuf __ocaml_lex_state =+ match Lexing.engine __ocaml_lex_tables __ocaml_lex_state lexbuf with+ | 0 ->+# 106 "src/dot_lexer.mll"+ ( () )+# 339 "src/dot_lexer.ml"++ | 1 ->+# 108 "src/dot_lexer.mll"+ ( Buffer.add_char string_buf '<'; html lexbuf;+ Buffer.add_char string_buf '>'; html lexbuf )+# 345 "src/dot_lexer.ml"++ | 2 ->+let+# 110 "src/dot_lexer.mll"+ c+# 351 "src/dot_lexer.ml"+= Lexing.sub_lexeme_char lexbuf lexbuf.Lexing.lex_start_pos in+# 111 "src/dot_lexer.mll"+ ( Buffer.add_char string_buf c;+ html lexbuf )+# 356 "src/dot_lexer.ml"++ | 3 ->+# 114 "src/dot_lexer.mll"+ ( failwith ("Dot_lexer: unterminated html literal") )+# 361 "src/dot_lexer.ml"++ | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_html_rec lexbuf __ocaml_lex_state++and comment lexbuf =+ __ocaml_lex_comment_rec lexbuf 38+and __ocaml_lex_comment_rec lexbuf __ocaml_lex_state =+ match Lexing.engine __ocaml_lex_tables __ocaml_lex_state lexbuf with+ | 0 ->+# 118 "src/dot_lexer.mll"+ ( () )+# 372 "src/dot_lexer.ml"++ | 1 ->+# 120 "src/dot_lexer.mll"+ ( comment lexbuf )+# 377 "src/dot_lexer.ml"++ | 2 ->+# 122 "src/dot_lexer.mll"+ ( failwith "Dot_lexer: unterminated comment" )+# 382 "src/dot_lexer.ml"++ | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_comment_rec lexbuf __ocaml_lex_state++;;+
+ external/ocamlgraph/src/dot_parser.ml view
@@ -0,0 +1,551 @@+type token =+ | ID of (Dot_ast.id)+ | COLON+ | COMMA+ | EQUAL+ | SEMICOLON+ | EDGEOP+ | STRICT+ | GRAPH+ | DIGRAPH+ | LBRA+ | RBRA+ | LSQ+ | RSQ+ | NODE+ | EDGE+ | SUBGRAPH+ | EOF++open Parsing;;+# 23 "src/dot_parser.mly"+ open Dot_ast+ open Parsing++ let compass_pt = function+ | Ident "n" -> N+ | Ident "ne" -> Ne+ | Ident "e" -> E+ | Ident "se" -> Se+ | Ident "s" -> S+ | Ident "sw" -> Sw+ | Ident "w" -> W+ | Ident "nw" -> Nw+ | _ -> invalid_arg "compass_pt"++# 37 "src/dot_parser.ml"+let yytransl_const = [|+ 258 (* COLON *);+ 259 (* COMMA *);+ 260 (* EQUAL *);+ 261 (* SEMICOLON *);+ 262 (* EDGEOP *);+ 263 (* STRICT *);+ 264 (* GRAPH *);+ 265 (* DIGRAPH *);+ 266 (* LBRA *);+ 267 (* RBRA *);+ 268 (* LSQ *);+ 269 (* RSQ *);+ 270 (* NODE *);+ 271 (* EDGE *);+ 272 (* SUBGRAPH *);+ 0 (* EOF *);+ 0|]++let yytransl_block = [|+ 257 (* ID *);+ 0|]++let yylhs = "\255\255\+\001\000\002\000\002\000\003\000\003\000\005\000\005\000\006\000\+\006\000\008\000\008\000\007\000\007\000\007\000\007\000\007\000\+\009\000\010\000\011\000\011\000\011\000\016\000\018\000\018\000\+\015\000\015\000\013\000\019\000\019\000\020\000\020\000\014\000\+\014\000\017\000\017\000\004\000\004\000\021\000\021\000\022\000\+\022\000\023\000\023\000\012\000\012\000\012\000\012\000\000\000"++let yylen = "\002\000\+\007\000\000\000\001\000\001\000\001\000\000\000\001\000\002\000\+\003\000\000\000\001\000\001\000\001\000\001\000\003\000\001\000\+\002\000\003\000\002\000\002\000\002\000\003\000\000\000\003\000\+\001\000\001\000\002\000\000\000\001\000\002\000\004\000\000\000\+\001\000\003\000\004\000\000\000\001\000\002\000\003\000\001\000\+\003\000\000\000\001\000\002\000\005\000\004\000\003\000\002\000"++let yydefred = "\000\000\+\000\000\000\000\003\000\048\000\000\000\004\000\005\000\000\000\+\037\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+\000\000\000\000\007\000\000\000\012\000\013\000\014\000\000\000\+\000\000\000\000\000\000\000\000\027\000\029\000\000\000\019\000\+\000\000\020\000\021\000\000\000\000\000\000\000\011\000\000\000\+\017\000\033\000\000\000\000\000\000\000\015\000\000\000\000\000\+\000\000\047\000\000\000\000\000\001\000\009\000\000\000\026\000\+\025\000\000\000\018\000\000\000\000\000\000\000\043\000\000\000\+\000\000\046\000\000\000\022\000\031\000\041\000\035\000\039\000\+\045\000\000\000\024\000"++let yydgoto = "\002\000\+\004\000\005\000\008\000\010\000\018\000\019\000\020\000\040\000\+\021\000\022\000\023\000\024\000\025\000\041\000\026\000\044\000\+\042\000\068\000\029\000\030\000\048\000\049\000\064\000"++let yysindex = "\009\000\+\024\255\000\000\000\000\000\000\000\255\000\000\000\000\031\255\+\000\000\029\255\131\255\011\255\033\255\131\255\033\255\033\255\+\051\255\040\255\000\000\048\255\000\000\000\000\000\000\000\000\+\033\255\050\255\057\255\067\255\000\000\000\000\069\255\000\000\+\062\255\000\000\000\000\070\255\131\255\091\000\000\000\131\255\+\000\000\000\000\018\255\033\255\090\255\000\000\099\255\081\255\+\101\255\000\000\131\255\095\255\000\000\000\000\107\255\000\000\+\000\000\110\255\000\000\114\255\117\255\033\255\000\000\069\255\+\111\255\000\000\018\255\000\000\000\000\000\000\000\000\000\000\+\000\000\110\255\000\000"++let yyrindex = "\000\000\+\074\255\000\000\000\000\000\000\000\000\000\000\000\000\116\255\+\000\000\000\000\118\255\006\255\000\000\118\255\000\000\000\000\+\000\000\000\000\000\000\120\255\000\000\000\000\000\000\049\255\+\061\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+\000\000\000\000\000\000\073\255\118\255\000\000\000\000\122\255\+\000\000\000\000\000\000\097\255\032\255\000\000\023\255\000\000\+\022\255\000\000\118\255\000\000\000\000\000\000\006\255\000\000\+\000\000\085\255\000\000\000\000\000\000\109\255\000\000\124\255\+\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+\000\000\085\255\000\000"++let yygindex = "\000\000\+\000\000\000\000\000\000\000\000\246\255\087\000\000\000\000\000\+\000\000\000\000\000\000\214\255\218\255\094\000\219\255\000\000\+\243\255\066\000\000\000\000\000\078\000\000\000\000\000"++let yytablesize = 147+let yytable = "\032\000\+\056\000\034\000\035\000\033\000\057\000\058\000\028\000\006\000\+\007\000\001\000\028\000\028\000\027\000\028\000\028\000\028\000\+\028\000\028\000\055\000\028\000\028\000\028\000\042\000\040\000\+\056\000\040\000\052\000\014\000\057\000\074\000\003\000\009\000\+\030\000\017\000\042\000\040\000\030\000\030\000\011\000\030\000\+\065\000\030\000\030\000\030\000\031\000\030\000\030\000\030\000\+\071\000\016\000\038\000\036\000\039\000\016\000\026\000\043\000\+\016\000\045\000\016\000\016\000\037\000\032\000\016\000\016\000\+\016\000\032\000\025\000\046\000\032\000\047\000\032\000\032\000\+\050\000\044\000\032\000\032\000\032\000\044\000\044\000\051\000\+\044\000\002\000\002\000\044\000\044\000\023\000\044\000\044\000\+\044\000\023\000\053\000\060\000\023\000\062\000\023\000\023\000\+\023\000\032\000\023\000\023\000\023\000\032\000\061\000\063\000\+\032\000\066\000\032\000\032\000\027\000\034\000\032\000\032\000\+\032\000\034\000\069\000\067\000\034\000\070\000\034\000\034\000\+\010\000\073\000\034\000\034\000\034\000\036\000\054\000\010\000\+\006\000\010\000\010\000\012\000\008\000\010\000\010\000\010\000\+\038\000\059\000\013\000\075\000\014\000\072\000\000\000\000\000\+\015\000\016\000\017\000"++let yycheck = "\013\000\+\043\000\015\000\016\000\014\000\043\000\043\000\001\001\008\001\+\009\001\001\000\005\001\006\001\002\001\008\001\004\001\010\001\+\011\001\012\001\001\001\014\001\015\001\016\001\001\001\001\001\+\067\000\003\001\037\000\010\001\067\000\067\000\007\001\001\001\+\001\001\016\001\013\001\013\001\005\001\006\001\010\001\008\001\+\051\000\010\001\011\001\012\001\012\001\014\001\015\001\016\001\+\062\000\001\001\011\001\001\001\005\001\005\001\006\001\006\001\+\008\001\001\001\010\001\011\001\010\001\001\001\014\001\015\001\+\016\001\005\001\006\001\001\001\008\001\001\001\010\001\011\001\+\011\001\001\001\014\001\015\001\016\001\005\001\006\001\010\001\+\008\001\008\001\009\001\011\001\012\001\001\001\014\001\015\001\+\016\001\005\001\000\000\002\001\008\001\013\001\010\001\011\001\+\012\001\001\001\014\001\015\001\016\001\005\001\004\001\003\001\+\008\001\011\001\010\001\011\001\002\001\001\001\014\001\015\001\+\016\001\005\001\001\001\006\001\008\001\001\001\010\001\011\001\+\001\001\011\001\014\001\015\001\016\001\010\001\040\000\008\001\+\011\001\010\001\011\001\001\001\011\001\014\001\015\001\016\001\+\013\001\044\000\008\001\074\000\010\001\064\000\255\255\255\255\+\014\001\015\001\016\001"++let yynames_const = "\+ COLON\000\+ COMMA\000\+ EQUAL\000\+ SEMICOLON\000\+ EDGEOP\000\+ STRICT\000\+ GRAPH\000\+ DIGRAPH\000\+ LBRA\000\+ RBRA\000\+ LSQ\000\+ RSQ\000\+ NODE\000\+ EDGE\000\+ SUBGRAPH\000\+ EOF\000\+ "++let yynames_block = "\+ ID\000\+ "++let yyact = [|+ (fun _ -> failwith "parser")+; (fun __caml_parser_env ->+ let _1 = (Parsing.peek_val __caml_parser_env 6 : 'strict_opt) in+ let _2 = (Parsing.peek_val __caml_parser_env 5 : 'graph_or_digraph) in+ let _3 = (Parsing.peek_val __caml_parser_env 4 : 'id_opt) in+ let _5 = (Parsing.peek_val __caml_parser_env 2 : 'stmt_list) in+ Obj.repr(+# 49 "src/dot_parser.mly"+ ( { strict = _1; digraph = _2; id = _3; stmts = _5 } )+# 199 "src/dot_parser.ml"+ : Dot_ast.file))+; (fun __caml_parser_env ->+ Obj.repr(+# 53 "src/dot_parser.mly"+ ( false )+# 205 "src/dot_parser.ml"+ : 'strict_opt))+; (fun __caml_parser_env ->+ Obj.repr(+# 54 "src/dot_parser.mly"+ ( true )+# 211 "src/dot_parser.ml"+ : 'strict_opt))+; (fun __caml_parser_env ->+ Obj.repr(+# 58 "src/dot_parser.mly"+ ( false )+# 217 "src/dot_parser.ml"+ : 'graph_or_digraph))+; (fun __caml_parser_env ->+ Obj.repr(+# 59 "src/dot_parser.mly"+ ( true )+# 223 "src/dot_parser.ml"+ : 'graph_or_digraph))+; (fun __caml_parser_env ->+ Obj.repr(+# 63 "src/dot_parser.mly"+ ( [] )+# 229 "src/dot_parser.ml"+ : 'stmt_list))+; (fun __caml_parser_env ->+ let _1 = (Parsing.peek_val __caml_parser_env 0 : 'list1_stmt) in+ Obj.repr(+# 64 "src/dot_parser.mly"+ ( _1 )+# 236 "src/dot_parser.ml"+ : 'stmt_list))+; (fun __caml_parser_env ->+ let _1 = (Parsing.peek_val __caml_parser_env 1 : 'stmt) in+ let _2 = (Parsing.peek_val __caml_parser_env 0 : 'semicolon_opt) in+ Obj.repr(+# 68 "src/dot_parser.mly"+ ( [_1] )+# 244 "src/dot_parser.ml"+ : 'list1_stmt))+; (fun __caml_parser_env ->+ let _1 = (Parsing.peek_val __caml_parser_env 2 : 'stmt) in+ let _2 = (Parsing.peek_val __caml_parser_env 1 : 'semicolon_opt) in+ let _3 = (Parsing.peek_val __caml_parser_env 0 : 'list1_stmt) in+ Obj.repr(+# 69 "src/dot_parser.mly"+ ( _1 :: _3 )+# 253 "src/dot_parser.ml"+ : 'list1_stmt))+; (fun __caml_parser_env ->+ Obj.repr(+# 73 "src/dot_parser.mly"+ ( () )+# 259 "src/dot_parser.ml"+ : 'semicolon_opt))+; (fun __caml_parser_env ->+ Obj.repr(+# 74 "src/dot_parser.mly"+ ( () )+# 265 "src/dot_parser.ml"+ : 'semicolon_opt))+; (fun __caml_parser_env ->+ let _1 = (Parsing.peek_val __caml_parser_env 0 : 'node_stmt) in+ Obj.repr(+# 78 "src/dot_parser.mly"+ ( _1 )+# 272 "src/dot_parser.ml"+ : 'stmt))+; (fun __caml_parser_env ->+ let _1 = (Parsing.peek_val __caml_parser_env 0 : 'edge_stmt) in+ Obj.repr(+# 79 "src/dot_parser.mly"+ ( _1 )+# 279 "src/dot_parser.ml"+ : 'stmt))+; (fun __caml_parser_env ->+ let _1 = (Parsing.peek_val __caml_parser_env 0 : 'attr_stmt) in+ Obj.repr(+# 80 "src/dot_parser.mly"+ ( _1 )+# 286 "src/dot_parser.ml"+ : 'stmt))+; (fun __caml_parser_env ->+ let _1 = (Parsing.peek_val __caml_parser_env 2 : Dot_ast.id) in+ let _3 = (Parsing.peek_val __caml_parser_env 0 : Dot_ast.id) in+ Obj.repr(+# 81 "src/dot_parser.mly"+ ( Equal (_1, _3) )+# 294 "src/dot_parser.ml"+ : 'stmt))+; (fun __caml_parser_env ->+ let _1 = (Parsing.peek_val __caml_parser_env 0 : 'subgraph) in+ Obj.repr(+# 82 "src/dot_parser.mly"+ ( Subgraph _1 )+# 301 "src/dot_parser.ml"+ : 'stmt))+; (fun __caml_parser_env ->+ let _1 = (Parsing.peek_val __caml_parser_env 1 : 'node_id) in+ let _2 = (Parsing.peek_val __caml_parser_env 0 : 'attr_list_opt) in+ Obj.repr(+# 86 "src/dot_parser.mly"+ ( Node_stmt (_1, _2) )+# 309 "src/dot_parser.ml"+ : 'node_stmt))+; (fun __caml_parser_env ->+ let _1 = (Parsing.peek_val __caml_parser_env 2 : 'node) in+ let _2 = (Parsing.peek_val __caml_parser_env 1 : 'edge_rhs) in+ let _3 = (Parsing.peek_val __caml_parser_env 0 : 'attr_list_opt) in+ Obj.repr(+# 90 "src/dot_parser.mly"+ ( Edge_stmt (_1, _2, _3) )+# 318 "src/dot_parser.ml"+ : 'edge_stmt))+; (fun __caml_parser_env ->+ let _2 = (Parsing.peek_val __caml_parser_env 0 : 'attr_list) in+ Obj.repr(+# 94 "src/dot_parser.mly"+ ( Attr_graph _2 )+# 325 "src/dot_parser.ml"+ : 'attr_stmt))+; (fun __caml_parser_env ->+ let _2 = (Parsing.peek_val __caml_parser_env 0 : 'attr_list) in+ Obj.repr(+# 95 "src/dot_parser.mly"+ ( Attr_node _2 )+# 332 "src/dot_parser.ml"+ : 'attr_stmt))+; (fun __caml_parser_env ->+ let _2 = (Parsing.peek_val __caml_parser_env 0 : 'attr_list) in+ Obj.repr(+# 96 "src/dot_parser.mly"+ ( Attr_edge _2 )+# 339 "src/dot_parser.ml"+ : 'attr_stmt))+; (fun __caml_parser_env ->+ let _2 = (Parsing.peek_val __caml_parser_env 1 : 'node) in+ let _3 = (Parsing.peek_val __caml_parser_env 0 : 'edge_rhs_opt) in+ Obj.repr(+# 100 "src/dot_parser.mly"+ ( _2 :: _3 )+# 347 "src/dot_parser.ml"+ : 'edge_rhs))+; (fun __caml_parser_env ->+ Obj.repr(+# 104 "src/dot_parser.mly"+ ( [] )+# 353 "src/dot_parser.ml"+ : 'edge_rhs_opt))+; (fun __caml_parser_env ->+ let _2 = (Parsing.peek_val __caml_parser_env 1 : 'node) in+ let _3 = (Parsing.peek_val __caml_parser_env 0 : 'edge_rhs_opt) in+ Obj.repr(+# 105 "src/dot_parser.mly"+ ( _2 :: _3 )+# 361 "src/dot_parser.ml"+ : 'edge_rhs_opt))+; (fun __caml_parser_env ->+ let _1 = (Parsing.peek_val __caml_parser_env 0 : 'node_id) in+ Obj.repr(+# 109 "src/dot_parser.mly"+ ( NodeId _1 )+# 368 "src/dot_parser.ml"+ : 'node))+; (fun __caml_parser_env ->+ let _1 = (Parsing.peek_val __caml_parser_env 0 : 'subgraph) in+ Obj.repr(+# 110 "src/dot_parser.mly"+ ( NodeSub _1 )+# 375 "src/dot_parser.ml"+ : 'node))+; (fun __caml_parser_env ->+ let _1 = (Parsing.peek_val __caml_parser_env 1 : Dot_ast.id) in+ let _2 = (Parsing.peek_val __caml_parser_env 0 : 'port_opt) in+ Obj.repr(+# 114 "src/dot_parser.mly"+ ( _1, _2 )+# 383 "src/dot_parser.ml"+ : 'node_id))+; (fun __caml_parser_env ->+ Obj.repr(+# 118 "src/dot_parser.mly"+ ( None )+# 389 "src/dot_parser.ml"+ : 'port_opt))+; (fun __caml_parser_env ->+ let _1 = (Parsing.peek_val __caml_parser_env 0 : 'port) in+ Obj.repr(+# 119 "src/dot_parser.mly"+ ( Some _1 )+# 396 "src/dot_parser.ml"+ : 'port_opt))+; (fun __caml_parser_env ->+ let _2 = (Parsing.peek_val __caml_parser_env 0 : Dot_ast.id) in+ Obj.repr(+# 123 "src/dot_parser.mly"+ ( try PortC (compass_pt _2)+ with Invalid_argument _ -> PortId (_2, None) )+# 404 "src/dot_parser.ml"+ : 'port))+; (fun __caml_parser_env ->+ let _2 = (Parsing.peek_val __caml_parser_env 2 : Dot_ast.id) in+ let _4 = (Parsing.peek_val __caml_parser_env 0 : Dot_ast.id) in+ Obj.repr(+# 126 "src/dot_parser.mly"+ ( let cp = + try compass_pt _4 with Invalid_argument _ -> raise Parse_error + in+ PortId (_2, Some cp) )+# 415 "src/dot_parser.ml"+ : 'port))+; (fun __caml_parser_env ->+ Obj.repr(+# 133 "src/dot_parser.mly"+ ( [] )+# 421 "src/dot_parser.ml"+ : 'attr_list_opt))+; (fun __caml_parser_env ->+ let _1 = (Parsing.peek_val __caml_parser_env 0 : 'attr_list) in+ Obj.repr(+# 134 "src/dot_parser.mly"+ ( _1 )+# 428 "src/dot_parser.ml"+ : 'attr_list_opt))+; (fun __caml_parser_env ->+ let _2 = (Parsing.peek_val __caml_parser_env 1 : 'a_list) in+ Obj.repr(+# 138 "src/dot_parser.mly"+ ( [_2] )+# 435 "src/dot_parser.ml"+ : 'attr_list))+; (fun __caml_parser_env ->+ let _2 = (Parsing.peek_val __caml_parser_env 2 : 'a_list) in+ let _4 = (Parsing.peek_val __caml_parser_env 0 : 'attr_list) in+ Obj.repr(+# 139 "src/dot_parser.mly"+ ( _2 :: _4 )+# 443 "src/dot_parser.ml"+ : 'attr_list))+; (fun __caml_parser_env ->+ Obj.repr(+# 143 "src/dot_parser.mly"+ ( None )+# 449 "src/dot_parser.ml"+ : 'id_opt))+; (fun __caml_parser_env ->+ let _1 = (Parsing.peek_val __caml_parser_env 0 : Dot_ast.id) in+ Obj.repr(+# 144 "src/dot_parser.mly"+ ( Some _1 )+# 456 "src/dot_parser.ml"+ : 'id_opt))+; (fun __caml_parser_env ->+ let _1 = (Parsing.peek_val __caml_parser_env 1 : 'equality) in+ let _2 = (Parsing.peek_val __caml_parser_env 0 : 'comma_opt) in+ Obj.repr(+# 148 "src/dot_parser.mly"+ ( [_1] )+# 464 "src/dot_parser.ml"+ : 'a_list))+; (fun __caml_parser_env ->+ let _1 = (Parsing.peek_val __caml_parser_env 2 : 'equality) in+ let _2 = (Parsing.peek_val __caml_parser_env 1 : 'comma_opt) in+ let _3 = (Parsing.peek_val __caml_parser_env 0 : 'a_list) in+ Obj.repr(+# 149 "src/dot_parser.mly"+ ( _1 :: _3 )+# 473 "src/dot_parser.ml"+ : 'a_list))+; (fun __caml_parser_env ->+ let _1 = (Parsing.peek_val __caml_parser_env 0 : Dot_ast.id) in+ Obj.repr(+# 153 "src/dot_parser.mly"+ ( _1, None )+# 480 "src/dot_parser.ml"+ : 'equality))+; (fun __caml_parser_env ->+ let _1 = (Parsing.peek_val __caml_parser_env 2 : Dot_ast.id) in+ let _3 = (Parsing.peek_val __caml_parser_env 0 : Dot_ast.id) in+ Obj.repr(+# 154 "src/dot_parser.mly"+ ( _1, Some _3 )+# 488 "src/dot_parser.ml"+ : 'equality))+; (fun __caml_parser_env ->+ Obj.repr(+# 158 "src/dot_parser.mly"+ ( () )+# 494 "src/dot_parser.ml"+ : 'comma_opt))+; (fun __caml_parser_env ->+ Obj.repr(+# 159 "src/dot_parser.mly"+ ( () )+# 500 "src/dot_parser.ml"+ : 'comma_opt))+; (fun __caml_parser_env ->+ let _2 = (Parsing.peek_val __caml_parser_env 0 : Dot_ast.id) in+ Obj.repr(+# 164 "src/dot_parser.mly"+ ( SubgraphId _2 )+# 507 "src/dot_parser.ml"+ : 'subgraph))+; (fun __caml_parser_env ->+ let _2 = (Parsing.peek_val __caml_parser_env 3 : Dot_ast.id) in+ let _4 = (Parsing.peek_val __caml_parser_env 1 : 'stmt_list) in+ Obj.repr(+# 165 "src/dot_parser.mly"+ ( SubgraphDef (Some _2, _4) )+# 515 "src/dot_parser.ml"+ : 'subgraph))+; (fun __caml_parser_env ->+ let _3 = (Parsing.peek_val __caml_parser_env 1 : 'stmt_list) in+ Obj.repr(+# 166 "src/dot_parser.mly"+ ( SubgraphDef (None, _3) )+# 522 "src/dot_parser.ml"+ : 'subgraph))+; (fun __caml_parser_env ->+ let _2 = (Parsing.peek_val __caml_parser_env 1 : 'stmt_list) in+ Obj.repr(+# 167 "src/dot_parser.mly"+ ( SubgraphDef (None, _2) )+# 529 "src/dot_parser.ml"+ : 'subgraph))+(* Entry file *)+; (fun __caml_parser_env -> raise (Parsing.YYexit (Parsing.peek_val __caml_parser_env 0)))+|]+let yytables =+ { Parsing.actions=yyact;+ Parsing.transl_const=yytransl_const;+ Parsing.transl_block=yytransl_block;+ Parsing.lhs=yylhs;+ Parsing.len=yylen;+ Parsing.defred=yydefred;+ Parsing.dgoto=yydgoto;+ Parsing.sindex=yysindex;+ Parsing.rindex=yyrindex;+ Parsing.gindex=yygindex;+ Parsing.tablesize=yytablesize;+ Parsing.table=yytable;+ Parsing.check=yycheck;+ Parsing.error_function=parse_error;+ Parsing.names_const=yynames_const;+ Parsing.names_block=yynames_block }+let file (lexfun : Lexing.lexbuf -> token) (lexbuf : Lexing.lexbuf) =+ (Parsing.yyparse yytables 1 lexfun lexbuf : Dot_ast.file)
+ external/ocamlgraph/src/dot_parser.mli view
@@ -0,0 +1,21 @@+type token =+ | ID of (Dot_ast.id)+ | COLON+ | COMMA+ | EQUAL+ | SEMICOLON+ | EDGEOP+ | STRICT+ | GRAPH+ | DIGRAPH+ | LBRA+ | RBRA+ | LSQ+ | RSQ+ | NODE+ | EDGE+ | SUBGRAPH+ | EOF++val file :+ (Lexing.lexbuf -> token) -> Lexing.lexbuf -> Dot_ast.file
+ external/ocamlgraph/src/gml.ml view
@@ -0,0 +1,670 @@+# 20 "src/gml.mll"+ ++ open Lexing++ type value = + | Int of int + | Float of float+ | String of string+ | List of value_list++ and value_list = (string * value) list+++# 16 "src/gml.ml"+let __ocaml_lex_tables = {+ Lexing.lex_base = + "\000\000\252\255\253\255\114\000\002\000\007\000\228\000\086\001\+ \252\255\253\255\200\001\009\000\014\000\058\002\002\000\251\255\+ \252\255\001\000\080\000\102\000\194\000\216\000\052\001\071\001\+ \253\255\006\000";+ Lexing.lex_backtrk = + "\255\255\255\255\255\255\003\000\000\000\001\000\255\255\255\255\+ \255\255\255\255\003\000\000\000\001\000\255\255\255\255\255\255\+ \255\255\004\000\001\000\000\000\004\000\255\255\001\000\255\255\+ \255\255\255\255";+ Lexing.lex_default = + "\001\000\000\000\000\000\255\255\255\255\255\255\255\255\008\000\+ \000\000\000\000\255\255\255\255\255\255\255\255\015\000\000\000\+ \000\000\025\000\255\255\255\255\255\255\255\255\255\255\255\255\+ \000\000\025\000";+ Lexing.lex_trans = + "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\004\000\004\000\004\000\004\000\004\000\000\000\004\000\+ \005\000\005\000\011\000\011\000\005\000\000\000\011\000\012\000\+ \012\000\000\000\000\000\012\000\000\000\000\000\000\000\000\000\+ \004\000\000\000\004\000\024\000\017\000\000\000\000\000\005\000\+ \024\000\011\000\000\000\000\000\000\000\020\000\012\000\020\000\+ \018\000\000\000\019\000\019\000\019\000\019\000\019\000\019\000\+ \019\000\019\000\019\000\019\000\000\000\000\000\000\000\000\000\+ \000\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\+ \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\+ \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\+ \003\000\003\000\003\000\000\000\000\000\016\000\000\000\000\000\+ \000\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\+ \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\+ \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\+ \003\000\003\000\003\000\005\000\005\000\000\000\000\000\005\000\+ \018\000\018\000\018\000\018\000\018\000\018\000\018\000\018\000\+ \018\000\018\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\005\000\000\000\018\000\021\000\019\000\019\000\+ \019\000\019\000\019\000\019\000\019\000\019\000\019\000\019\000\+ \000\000\000\000\006\000\006\000\006\000\006\000\006\000\006\000\+ \006\000\006\000\006\000\006\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\006\000\006\000\006\000\006\000\006\000\+ \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\+ \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\+ \006\000\006\000\006\000\006\000\006\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\006\000\006\000\006\000\006\000\006\000\+ \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\+ \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\+ \006\000\006\000\006\000\006\000\006\000\005\000\005\000\000\000\+ \018\000\005\000\019\000\019\000\019\000\019\000\019\000\019\000\+ \019\000\019\000\019\000\019\000\000\000\000\000\000\000\000\000\+ \002\000\255\255\255\255\023\000\005\000\023\000\255\255\000\000\+ \022\000\022\000\022\000\022\000\022\000\022\000\022\000\022\000\+ \022\000\022\000\000\000\000\000\006\000\006\000\006\000\006\000\+ \006\000\006\000\006\000\006\000\006\000\006\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\006\000\006\000\006\000\+ \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\+ \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\+ \006\000\006\000\006\000\006\000\006\000\006\000\006\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\006\000\006\000\006\000\+ \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\+ \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\+ \006\000\006\000\006\000\006\000\006\000\006\000\006\000\011\000\+ \011\000\000\000\000\000\011\000\022\000\022\000\022\000\022\000\+ \022\000\022\000\022\000\022\000\022\000\022\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\011\000\022\000\+ \022\000\022\000\022\000\022\000\022\000\022\000\022\000\022\000\+ \022\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\010\000\+ \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\+ \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\+ \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\+ \010\000\000\000\000\000\009\000\000\000\000\000\000\000\010\000\+ \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\+ \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\+ \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\+ \010\000\012\000\012\000\000\000\000\000\012\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \012\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\+ \013\000\013\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\+ \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\+ \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\+ \013\000\013\000\013\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\+ \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\+ \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\+ \013\000\013\000\013\000\012\000\012\000\000\000\000\000\012\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\255\255\000\000\+ \000\000\000\000\012\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\013\000\013\000\013\000\013\000\013\000\013\000\+ \013\000\013\000\013\000\013\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\013\000\013\000\013\000\013\000\013\000\+ \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\+ \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\+ \013\000\013\000\013\000\013\000\013\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\013\000\013\000\013\000\013\000\013\000\+ \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\+ \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\+ \013\000\013\000\013\000\013\000\013\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000";+ Lexing.lex_check = + "\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\000\000\000\000\004\000\004\000\000\000\255\255\004\000\+ \005\000\005\000\011\000\011\000\005\000\255\255\011\000\012\000\+ \012\000\255\255\255\255\012\000\255\255\255\255\255\255\255\255\+ \000\000\255\255\004\000\017\000\014\000\255\255\255\255\005\000\+ \025\000\011\000\255\255\255\255\255\255\014\000\012\000\014\000\+ \014\000\255\255\014\000\014\000\014\000\014\000\014\000\014\000\+ \014\000\014\000\014\000\014\000\255\255\255\255\255\255\255\255\+ \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\255\255\255\255\014\000\255\255\255\255\+ \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\003\000\003\000\255\255\255\255\003\000\+ \018\000\018\000\018\000\018\000\018\000\018\000\018\000\018\000\+ \018\000\018\000\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\003\000\255\255\019\000\018\000\019\000\019\000\+ \019\000\019\000\019\000\019\000\019\000\019\000\019\000\019\000\+ \255\255\255\255\003\000\003\000\003\000\003\000\003\000\003\000\+ \003\000\003\000\003\000\003\000\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\003\000\003\000\003\000\003\000\003\000\+ \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\+ \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\+ \003\000\003\000\003\000\003\000\003\000\255\255\255\255\255\255\+ \255\255\255\255\255\255\003\000\003\000\003\000\003\000\003\000\+ \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\+ \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\+ \003\000\003\000\003\000\003\000\003\000\006\000\006\000\255\255\+ \020\000\006\000\020\000\020\000\020\000\020\000\020\000\020\000\+ \020\000\020\000\020\000\020\000\255\255\255\255\255\255\255\255\+ \000\000\017\000\014\000\021\000\006\000\021\000\025\000\255\255\+ \021\000\021\000\021\000\021\000\021\000\021\000\021\000\021\000\+ \021\000\021\000\255\255\255\255\006\000\006\000\006\000\006\000\+ \006\000\006\000\006\000\006\000\006\000\006\000\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\006\000\006\000\006\000\+ \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\+ \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\+ \006\000\006\000\006\000\006\000\006\000\006\000\006\000\255\255\+ \255\255\255\255\255\255\255\255\255\255\006\000\006\000\006\000\+ \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\+ \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\+ \006\000\006\000\006\000\006\000\006\000\006\000\006\000\007\000\+ \007\000\255\255\255\255\007\000\022\000\022\000\022\000\022\000\+ \022\000\022\000\022\000\022\000\022\000\022\000\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\007\000\023\000\+ \023\000\023\000\023\000\023\000\023\000\023\000\023\000\023\000\+ \023\000\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\007\000\+ \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\255\255\255\255\007\000\255\255\255\255\255\255\007\000\+ \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\010\000\010\000\255\255\255\255\010\000\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \010\000\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\+ \010\000\010\000\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\010\000\010\000\010\000\010\000\010\000\010\000\010\000\+ \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\+ \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\+ \010\000\010\000\010\000\255\255\255\255\255\255\255\255\255\255\+ \255\255\010\000\010\000\010\000\010\000\010\000\010\000\010\000\+ \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\+ \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\+ \010\000\010\000\010\000\013\000\013\000\255\255\255\255\013\000\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\007\000\255\255\+ \255\255\255\255\013\000\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\013\000\013\000\013\000\013\000\013\000\013\000\+ \013\000\013\000\013\000\013\000\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\013\000\013\000\013\000\013\000\013\000\+ \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\+ \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\+ \013\000\013\000\013\000\013\000\013\000\255\255\255\255\255\255\+ \255\255\255\255\255\255\013\000\013\000\013\000\013\000\013\000\+ \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\+ \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\+ \013\000\013\000\013\000\013\000\013\000\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255";+ Lexing.lex_base_code = + "\000\000\000\000\000\000\075\000\000\000\000\000\150\000\208\000\+ \000\000\000\000\027\001\000\000\000\000\102\001\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000";+ Lexing.lex_backtrk_code = + "\000\000\000\000\000\000\000\000\000\000\004\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\004\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000";+ Lexing.lex_default_code = + "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000";+ Lexing.lex_trans_code = + "\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\000\000\000\000\000\000\000\000\000\000\000\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\000\000\000\000\000\000\000\000\000\000\000\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\001\000\001\000\001\000\001\000\001\000\001\000\001\000\+ \001\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000";+ Lexing.lex_check_code = + "\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\255\255\255\255\255\255\255\255\255\255\+ \255\255\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\000\+ \000\000\000\000\000\000\003\000\003\000\003\000\003\000\003\000\+ \003\000\003\000\003\000\003\000\003\000\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\003\000\003\000\003\000\003\000\+ \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\+ \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\+ \003\000\003\000\003\000\003\000\003\000\003\000\255\255\255\255\+ \255\255\255\255\255\255\255\255\003\000\003\000\003\000\003\000\+ \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\+ \003\000\003\000\003\000\003\000\003\000\003\000\003\000\003\000\+ \003\000\003\000\003\000\003\000\003\000\003\000\006\000\006\000\+ \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\006\000\+ \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\+ \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\+ \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\+ \006\000\255\255\255\255\255\255\255\255\255\255\255\255\006\000\+ \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\+ \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\+ \006\000\006\000\006\000\006\000\006\000\006\000\006\000\006\000\+ \006\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\255\255\255\255\255\255\255\255\255\255\+ \255\255\007\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\007\000\007\000\007\000\007\000\007\000\+ \007\000\007\000\007\000\010\000\010\000\010\000\010\000\010\000\+ \010\000\010\000\010\000\010\000\010\000\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\010\000\010\000\010\000\010\000\+ \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\+ \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\+ \010\000\010\000\010\000\010\000\010\000\010\000\255\255\255\255\+ \255\255\255\255\255\255\255\255\010\000\010\000\010\000\010\000\+ \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\+ \010\000\010\000\010\000\010\000\010\000\010\000\010\000\010\000\+ \010\000\010\000\010\000\010\000\010\000\010\000\013\000\013\000\+ \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\013\000\+ \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\+ \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\+ \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\+ \013\000\255\255\255\255\255\255\255\255\255\255\255\255\013\000\+ \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\+ \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\+ \013\000\013\000\013\000\013\000\013\000\013\000\013\000\013\000\+ \013\000\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\255\+ \255\255\255\255\255\255\255\255\255\255\255\255\255\255";+ Lexing.lex_code = + "\255\001\255\255\000\001\255";+}++let rec file lexbuf =+ lexbuf.Lexing.lex_mem <- Array.create 2 (-1) ; __ocaml_lex_file_rec lexbuf 0+and __ocaml_lex_file_rec lexbuf __ocaml_lex_state =+ match Lexing.new_engine __ocaml_lex_tables __ocaml_lex_state lexbuf with+ | 0 ->+# 45 "src/gml.mll"+ ( file lexbuf )+# 425 "src/gml.ml"++ | 1 ->+let+# 46 "src/gml.mll"+ key+# 431 "src/gml.ml"+= Lexing.sub_lexeme lexbuf lexbuf.Lexing.lex_start_pos lexbuf.Lexing.lex_mem.(0) in+# 47 "src/gml.mll"+ ( let v = value lexbuf in+ (key, v) :: file lexbuf )+# 436 "src/gml.ml"++ | 2 ->+# 50 "src/gml.mll"+ ( [] )+# 441 "src/gml.ml"++ | 3 ->+let+# 51 "src/gml.mll"+ c+# 447 "src/gml.ml"+= Lexing.sub_lexeme_char lexbuf lexbuf.Lexing.lex_start_pos in+# 52 "src/gml.mll"+ ( failwith ("Gml: invalid character " ^ String.make 1 c) )+# 451 "src/gml.ml"++ | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_file_rec lexbuf __ocaml_lex_state++and value_list lexbuf =+ lexbuf.Lexing.lex_mem <- Array.create 2 (-1) ; __ocaml_lex_value_list_rec lexbuf 7+and __ocaml_lex_value_list_rec lexbuf __ocaml_lex_state =+ match Lexing.new_engine __ocaml_lex_tables __ocaml_lex_state lexbuf with+ | 0 ->+# 56 "src/gml.mll"+ ( value_list lexbuf )+# 462 "src/gml.ml"++ | 1 ->+let+# 57 "src/gml.mll"+ key+# 468 "src/gml.ml"+= Lexing.sub_lexeme lexbuf lexbuf.Lexing.lex_start_pos lexbuf.Lexing.lex_mem.(0) in+# 58 "src/gml.mll"+ ( let v = value lexbuf in+ (key, v) :: value_list lexbuf )+# 473 "src/gml.ml"++ | 2 ->+# 61 "src/gml.mll"+ ( [] )+# 478 "src/gml.ml"++ | 3 ->+let+# 62 "src/gml.mll"+ c+# 484 "src/gml.ml"+= Lexing.sub_lexeme_char lexbuf lexbuf.Lexing.lex_start_pos in+# 63 "src/gml.mll"+ ( failwith ("Gml: invalid character " ^ String.make 1 c) )+# 488 "src/gml.ml"++ | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_value_list_rec lexbuf __ocaml_lex_state++and value lexbuf =+ __ocaml_lex_value_rec lexbuf 14+and __ocaml_lex_value_rec lexbuf __ocaml_lex_state =+ match Lexing.engine __ocaml_lex_tables __ocaml_lex_state lexbuf with+ | 0 ->+let+# 66 "src/gml.mll"+ i+# 500 "src/gml.ml"+= Lexing.sub_lexeme lexbuf lexbuf.Lexing.lex_start_pos lexbuf.Lexing.lex_curr_pos in+# 67 "src/gml.mll"+ ( Int (int_of_string i) )+# 504 "src/gml.ml"++ | 1 ->+let+# 68 "src/gml.mll"+ r+# 510 "src/gml.ml"+= Lexing.sub_lexeme lexbuf lexbuf.Lexing.lex_start_pos lexbuf.Lexing.lex_curr_pos in+# 69 "src/gml.mll"+ ( Float (float_of_string r) )+# 514 "src/gml.ml"++ | 2 ->+let+# 70 "src/gml.mll"+ s+# 520 "src/gml.ml"+= Lexing.sub_lexeme lexbuf (lexbuf.Lexing.lex_start_pos + 1) (lexbuf.Lexing.lex_curr_pos + -1) in+# 71 "src/gml.mll"+ ( String s )+# 524 "src/gml.ml"++ | 3 ->+# 73 "src/gml.mll"+ ( let l = value_list lexbuf in List l )+# 529 "src/gml.ml"++ | 4 ->+let+# 74 "src/gml.mll"+ c+# 535 "src/gml.ml"+= Lexing.sub_lexeme_char lexbuf lexbuf.Lexing.lex_start_pos in+# 75 "src/gml.mll"+ ( failwith ("Gml: invalid character " ^ String.make 1 c) )+# 539 "src/gml.ml"++ | __ocaml_lex_state -> lexbuf.Lexing.refill_buff lexbuf; __ocaml_lex_value_rec lexbuf __ocaml_lex_state++;;++# 77 "src/gml.mll"+ ++ let parse f =+ let c = open_in f in+ let lb = from_channel c in+ let v = file lb in+ close_in c;+ v++ module Parse+ (B : Builder.S)+ (L : sig val node : value_list -> B.G.V.label+ val edge : value_list -> B.G.E.label end) = + struct++ let create_graph l =+ let nodes = Hashtbl.create 97 in+ let g = B.empty () in+ (* 1st pass: create the nodes *)+ let g =+ List.fold_left + (fun g v -> match v with+ | "node", List l ->+ let n = B.G.V.create (L.node l) in+ begin + try + let id = List.assoc "id" l in Hashtbl.add nodes id n+ with Not_found -> + ()+ end;+ B.add_vertex g n+ | _ -> + g)+ g l+ in+ (* 2nd pass: add the edges *)+ List.fold_left+ (fun g v -> match v with+ | "edge", List l ->+ begin try+ let source = List.assoc "source" l in+ let target = List.assoc "target" l in+ let nsource = Hashtbl.find nodes source in+ let ntarget = Hashtbl.find nodes target in+ let e = B.G.E.create nsource (L.edge l) ntarget in+ B.add_edge_e g e+ with Not_found ->+ g+ end+ | _ ->+ g)+ g l+ + let parse f =+ match parse f with+ | ["graph", List l] -> create_graph l+ | _ -> invalid_arg "Gml.Parse.parse: not a graph file"+ + end++ module Print+ (G : sig+ module V : sig+ type t+ val hash : t -> int+ val equal : t -> t -> bool+ type label+ val label : t -> label+ end+ module E : sig+ type t+ type label+ val src : t -> V.t+ val dst : t -> V.t+ val label : t -> label+ end+ type t+ val iter_vertex : (V.t -> unit) -> t -> unit+ val iter_edges_e : (E.t -> unit) -> t -> unit+ end)+ (L : sig+ val node : G.V.label -> value_list+ val edge : G.E.label -> value_list+ end) =+ struct++ open Format++ module H = Hashtbl.Make(G.V)++ let print fmt g =+ let nodes = H.create 97 in+ let cpt = ref 0 in+ let id n = + try H.find nodes n+ with Not_found -> incr cpt; let id = !cpt in H.add nodes n id; id+ in+ fprintf fmt "@[graph [@\n";+ let rec value fmt = function+ | Int n -> fprintf fmt "%d" n+ | Float f -> fprintf fmt "%f" f+ | String s -> fprintf fmt "\"%s\"" s+ | List l -> fprintf fmt "[@\n @[%a@]@\n]" value_list l+ and value_list fmt = function+ | [] -> ()+ | [s,v] -> fprintf fmt "%s %a" s value v+ | (s,v) :: l -> fprintf fmt "%s %a@\n" s value v; value_list fmt l+ in+ G.iter_vertex+ (fun v -> + fprintf fmt " @[node [@\n id %d@\n @[%a@]@\n]@]@\n" + (id v) value_list (L.node (G.V.label v)))+ g;+ G.iter_edges_e+ (fun e ->+ fprintf fmt + " @[edge [@\n source %d@\n target %d@\n @[%a@]@\n]@]@\n"+ (id (G.E.src e)) (id (G.E.dst e)) + value_list (L.edge (G.E.label e)))+ g;+ fprintf fmt "]@\n"++ end+++# 671 "src/gml.ml"
+ external/ocamlgraph/src/version.ml view
@@ -0,0 +1,2 @@+let version = "0.99b"+let date = "Fri Mar 27 20:20:48 UTC 2015"
liquid-fixpoint.cabal view
@@ -1,5 +1,5 @@ name: liquid-fixpoint-version: 0.2.3.1+version: 0.2.3.2 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
src/Language/Fixpoint/Bitvector.hs view
@@ -1,20 +1,20 @@-{-# LANGUAGE DeriveGeneric #-}-{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveGeneric #-} module Language.Fixpoint.Bitvector ( -- * Constructor Bv (..)- - -- * Sizes ++ -- * Sizes , BvSize (..) -- * Operators , BvOp (..) -- * BitVector Sort Constructor- , mkSort + , mkSort - -- * BitVector Expression Constructor + -- * BitVector Expression Constructor , eOp -- * BitVector Type Constructor@@ -22,14 +22,14 @@ ) where -import qualified Data.Text as T-import Language.Fixpoint.Types-import Language.Fixpoint.Names-import GHC.Generics (Generic)-import Data.Typeable (Typeable)-import Data.Generics (Data)+import Data.Generics (Data)+import qualified Data.Text as T+import Data.Typeable (Typeable)+import GHC.Generics (Generic)+import Language.Fixpoint.Names+import Language.Fixpoint.Types -data Bv = Bv BvSize String +data Bv = Bv BvSize String data BvSize = S32 | S64 deriving (Eq, Ord, Show, Data, Typeable, Generic)@@ -60,12 +60,11 @@ opName BvOr = dummyLoc bvOrName sizeSort = (`FApp` [fObj $ dummyLoc $ symbol "obj"]) . sizeTC-sizeTC = symbolFTycon . dummyLoc . sizeName +sizeTC = symbolFTycon . dummyLoc . sizeName sizeName S32 = size32Name sizeName S64 = size64Name bvTyCon = symbolFTycon $ dummyLoc bitVecName --- s32TyCon = symbolFTycon $ dummyLoc size32Name +-- s32TyCon = symbolFTycon $ dummyLoc size32Name -- s64TyCon = symbolFTycon $ dummyLoc size64Name-
src/Language/Fixpoint/Config.hs view
@@ -1,7 +1,7 @@-{-# LANGUAGE NoMonomorphismRestriction #-}-{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE UndecidableInstances #-} @@ -11,17 +11,17 @@ , SMTSolver (..) , GenQualifierSort (..) , UeqAllSorts (..)- , withTarget + , withTarget , withUEqAllSorts-) where - -import Language.Fixpoint.Files-import System.FilePath -import System.Console.CmdArgs.Default-import Data.Typeable (Typeable)-import Data.Generics (Data)+) where +import Data.Generics (Data)+import Data.Typeable (Typeable)+import Language.Fixpoint.Files+import System.Console.CmdArgs.Default+import System.FilePath + class Command a where command :: a -> String @@ -29,11 +29,11 @@ -- Configuration Options ----------------------------------------------- ------------------------------------------------------------------------ -withTarget :: Config -> FilePath -> Config +withTarget :: Config -> FilePath -> Config withTarget cfg fq = cfg { inFile = fq } { outFile = fq `withExt` Out } -data Config - = Config { +data Config+ = Config { inFile :: FilePath -- target fq-file , outFile :: FilePath -- output file , solver :: SMTSolver -- which SMT solver to use@@ -46,24 +46,24 @@ instance Default Config where def = Config "" def def def def def def -instance Command Config where - command c = command (genSorts c) - ++ command (ueqAllSorts c) - ++ command (solver c) - ++ " -out " +instance Command Config where+ command c = command (genSorts c)+ ++ command (ueqAllSorts c)+ ++ command (solver c)+ ++ " -out " ++ (outFile c) ++ " " ++ (inFile c) ------------------------------------------------------------------------------------------ newtype OFilePath = O FilePath +-- newtype OFilePath = O FilePath -- deriving (Eq, Data,Typeable,Show)--- --- instance Default OFilePath where +--+-- instance Default OFilePath where -- def = O "out"--- --- instance Command OFilePath where +--+-- instance Command OFilePath where -- command (O s) = " -out " ++ s -newtype GenQualifierSort = GQS Bool +newtype GenQualifierSort = GQS Bool deriving (Eq, Data,Typeable,Show) instance Default GenQualifierSort where@@ -71,9 +71,9 @@ instance Command GenQualifierSort where command (GQS True) = ""- command (GQS False) = "-no-gen-qual-sorts" + command (GQS False) = "-no-gen-qual-sorts" -newtype UeqAllSorts = UAS Bool +newtype UeqAllSorts = UAS Bool deriving (Eq, Data,Typeable,Show) instance Default UeqAllSorts where@@ -81,7 +81,7 @@ instance Command UeqAllSorts where command (UAS True) = " -ueq-all-sorts "- command (UAS False) = "" + command (UAS False) = "" withUEqAllSorts c b = c { ueqAllSorts = UAS b } @@ -90,13 +90,13 @@ data SMTSolver = Z3 | Cvc4 | Mathsat | Z3mem deriving (Eq,Data,Typeable) -instance Command SMTSolver where +instance Command SMTSolver where command s = " -smtsolver " ++ show s instance Default SMTSolver where def = Z3 -instance Show SMTSolver where +instance Show SMTSolver where show Z3 = "z3" show Cvc4 = "cvc4" show Mathsat = "mathsat"@@ -109,6 +109,4 @@ smtSolver other = error $ "ERROR: unsupported SMT Solver = " ++ other -- defaultSolver :: Maybe SMTSolver -> SMTSolver--- defaultSolver = fromMaybe Z3 --+-- defaultSolver = fromMaybe Z3
src/Language/Fixpoint/Errors.hs view
@@ -1,7 +1,7 @@-{-# LANGUAGE NoMonomorphismRestriction #-}-{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE NoMonomorphismRestriction #-} module Language.Fixpoint.Errors ( -- * Concrete Location Type@@ -29,52 +29,52 @@ ) where -import System.FilePath -import Text.PrettyPrint.HughesPJ-import Text.Parsec.Pos -import Data.Typeable-import Data.Generics (Data)-import Text.Printf -import Data.Hashable-import Control.Exception-import qualified Control.Monad.Error as E -import Language.Fixpoint.PrettyPrint-import Language.Fixpoint.Types-import GHC.Generics (Generic)+import Control.Exception+import qualified Control.Monad.Error as E+import Data.Generics (Data)+import Data.Hashable+import Data.Typeable+import GHC.Generics (Generic)+import Language.Fixpoint.PrettyPrint+import Language.Fixpoint.Types+import System.FilePath+import Text.Parsec.Pos+import Text.PrettyPrint.HughesPJ+import Text.Printf ----------------------------------------------------------------------- -- | A Reusable SrcSpan Type ------------------------------------------ ----------------------------------------------------------------------- -data SrcSpan = SS { sp_start :: !SourcePos, sp_stop :: !SourcePos} +data SrcSpan = SS { sp_start :: !SourcePos, sp_stop :: !SourcePos} deriving (Eq, Ord, Show, Data, Typeable, Generic) instance PPrint SrcSpan where pprint = ppSrcSpan -- ppSrcSpan_short z = parens--- $ text (printf "file %s: (%d, %d) - (%d, %d)" (takeFileName f) l c l' c') --- where +-- $ text (printf "file %s: (%d, %d) - (%d, %d)" (takeFileName f) l c l' c')+-- where -- (f,l ,c ) = sourcePosElts $ sp_start z -- (_,l',c') = sourcePosElts $ sp_stop z -ppSrcSpan z = text (printf "%s:%d:%d-%d:%d" f l c l' c') - -- parens $ text (printf "file %s: (%d, %d) - (%d, %d)" (takeFileName f) l c l' c') - where +ppSrcSpan z = text (printf "%s:%d:%d-%d:%d" f l c l' c')+ -- parens $ text (printf "file %s: (%d, %d) - (%d, %d)" (takeFileName f) l c l' c')+ where (f,l ,c ) = sourcePosElts $ sp_start z (_,l',c') = sourcePosElts $ sp_stop z sourcePosElts s = (src, line, col)- where - src = sourceName s + where+ src = sourceName s line = sourceLine s- col = sourceColumn s + col = sourceColumn s -instance Hashable SourcePos where +instance Hashable SourcePos where hashWithSalt i = hashWithSalt i . sourcePosElts -instance Hashable SrcSpan where +instance Hashable SrcSpan where hashWithSalt i z = hashWithSalt i (sp_start z, sp_stop z) @@ -94,8 +94,8 @@ instance PPrint Error where pprint (Error l msg) = ppSrcSpan l <> text (": Error: " ++ msg)- -- text $ printf "%s\n %s\n" (showpp l) msg - + -- text $ printf "%s\n %s\n" (showpp l) msg+ instance Fixpoint Error where toFix = pprint @@ -103,15 +103,15 @@ instance E.Error Error where strMsg = Error dummySpan- -dummySpan = SS l l ++dummySpan = SS l l where l = initialPos "" --------------------------------------------------------------------- catMessage :: Error -> String -> Error ----------------------------------------------------------------------catMessage err msg = err {errMsg = msg ++ errMsg err} +catMessage err msg = err {errMsg = msg ++ errMsg err} --------------------------------------------------------------------- catError :: Error -> Error -> Error@@ -129,4 +129,3 @@ die :: Error -> a --------------------------------------------------------------------- die = throw-
src/Language/Fixpoint/Files.hs view
@@ -29,11 +29,11 @@ ) where -import qualified Control.Exception as Ex-import Control.Monad -- .State-import Data.Functor ((<$>))-import Data.List hiding (find)-import Data.Maybe (fromMaybe)+import qualified Control.Exception as Ex+import Control.Monad+import Data.Functor ((<$>))+import Data.List hiding (find)+import Data.Maybe (fromMaybe) import System.Directory import System.Environment import System.FilePath@@ -63,11 +63,11 @@ data Ext = Cgi -- ^ Constraint Generation Information | Fq -- ^ Input to constraint solving (fixpoint) | Out -- ^ Output from constraint solving (fixpoint)- | Html -- ^ HTML file with inferred type annotations - | Annot -- ^ Text file with inferred types - | Vim -- ^ Vim annotation file - | Hs -- ^ Haskell source - | LHs -- ^ Literate Haskell source + | Html -- ^ HTML file with inferred type annotations+ | Annot -- ^ Text file with inferred types+ | Vim -- ^ Vim annotation file+ | Hs -- ^ Haskell source+ | LHs -- ^ Literate Haskell source | Js -- ^ JavaScript source | Ts -- ^ Typescript source | Spec -- ^ Spec file (e.g. include/Prelude.spec)@@ -108,7 +108,7 @@ go Saved = ".bak" go Cache = ".err" go Smt2 = ".smt2"- go _ = errorstar $ "extMap: Unknown extension " ++ show e+ -- go _ = errorstar $ "extMap: Unknown extension " ++ show e withExt :: FilePath -> Ext -> FilePath withExt f ext = replaceExtension f (extMap ext)@@ -121,8 +121,8 @@ ext = extMap e tempDirectory :: FilePath -> FilePath-tempDirectory f - | isTmp dir = dir +tempDirectory f+ | isTmp dir = dir | otherwise = dir </> tmpDirName where dir = takeDirectory f@@ -141,7 +141,7 @@ case explode modName of [] -> errorstar $ "malformed module name: " ++ modName ws -> extFileNameR ext $ foldr1 (</>) ws- where + where explode = words . map (\c -> if c == '.' then ' ' else c) copyFiles :: [FilePath] -> FilePath -> IO ()
src/Language/Fixpoint/Interface.hs view
@@ -1,72 +1,73 @@ module Language.Fixpoint.Interface (- + -- * Containing Constraints FInfo (..)- + -- * Invoke Solver on Set of Constraints , solve , solveFile -- * Function to determine outcome , resultExit- + -- * Validity Query- , checkValid + , checkValid ) where {- Interfacing with Fixpoint Binary -} -import Data.Hashable-import Data.Monoid-import Data.Functor-import Data.List-import qualified Data.HashMap.Strict as M-import System.IO (hPutStr, withFile, IOMode (..))-import System.Exit-import System.Directory (getTemporaryDirectory)-import System.FilePath ((</>))-import Text.Printf+import Data.Functor+import Data.Hashable+import qualified Data.HashMap.Strict as M+import Data.List+import Data.Monoid+import System.Directory (getTemporaryDirectory)+import System.Exit+import System.FilePath ((</>))+import System.IO (IOMode (..), hPutStr,+ withFile)+import Text.Printf -import Language.Fixpoint.Config-import Language.Fixpoint.Types hiding (kuts, lits)-import Language.Fixpoint.Misc-import Language.Fixpoint.Parse (rr)-import Language.Fixpoint.Files-import Text.PrettyPrint.HughesPJ-import System.Console.CmdArgs.Default-import System.Console.CmdArgs.Verbosity+import Language.Fixpoint.Config+import Language.Fixpoint.Files+import Language.Fixpoint.Misc+import Language.Fixpoint.Parse (rr)+import Language.Fixpoint.Types hiding (kuts, lits)+import System.Console.CmdArgs.Default+import System.Console.CmdArgs.Verbosity+import Text.PrettyPrint.HughesPJ --------------------------------------------------------------------------- -- | One Shot validity query ---------------------------------------------- --------------------------------------------------------------------------- ----------------------------------------------------------------------------checkValid :: (Hashable a) => a -> [(Symbol, Sort)] -> Pred -> IO (FixResult a) +checkValid :: (Hashable a) => a -> [(Symbol, Sort)] -> Pred -> IO (FixResult a) ----------------------------------------------------------------------------checkValid n xts p +checkValid n xts p = do file <- (</> show (hash n)) <$> getTemporaryDirectory (r, _) <- solve def file [] $ validFInfo n xts p- return (sinfo <$> r) + return (sinfo <$> r) validFInfo :: a -> [(Symbol, Sort)] -> Pred -> FInfo a validFInfo l xts p = FI constrm [] benv emptySEnv [] ksEmpty []- where - constrm = M.singleton 0 $ validSubc l ibenv p + where+ constrm = M.singleton 0 $ validSubc l ibenv p binds = [(x, trueSortedReft t) | (x, t) <- xts] ibenv = insertsIBindEnv bids emptyIBindEnv (bids, benv) = foldlMap (\e (x,t) -> insertBindEnv x t e) emptyBindEnv binds -validSubc :: a -> IBindEnv -> Pred -> SubC a +validSubc :: a -> IBindEnv -> Pred -> SubC a validSubc l env p = safeHead "Interface.validSubC" $ subC env PTrue lhs rhs i t l- where + where lhs = mempty rhs = RR mempty (predReft p) i = Just 0 t = [] -result :: a -> Bool -> FixResult a -result _ True = Safe +result :: a -> Bool -> FixResult a+result _ True = Safe result x False = Unsafe [x] @@ -75,25 +76,25 @@ --------------------------------------------------------------------------- ----------------------------------------------------------------------------solve :: Config -> FilePath -> [FilePath] -> FInfo a +solve :: Config -> FilePath -> [FilePath] -> FInfo a -> IO (FixResult (SubC a), M.HashMap Symbol Pred) --------------------------------------------------------------------------- solve cfg fn hqs fi = {-# SCC "Solve" #-} execFq cfg fn hqs fi- >>= {-# SCC "exitFq" #-} exitFq fn (cm fi) - + >>= {-# SCC "exitFq" #-} exitFq fn (cm fi)+ execFq cfg fn hqs fi = do copyFiles hqs fq- appendFile fq qstr + appendFile fq qstr withFile fq AppendMode (\h -> {-# SCC "HPrintDump" #-} hPutStr h (render d)) solveFile $ cfg `withTarget` fq- where + where fq = extFileName Fq fn- d = {-# SCC "FixPointify" #-} toFixpoint fi + d = {-# SCC "FixPointify" #-} toFixpoint fi qstr = render ((vcat $ toFix <$> (quals fi)) $$ text "\n") ----------------------------------------------------------------------------solveFile :: Config -> IO ExitCode +solveFile :: Config -> IO ExitCode --------------------------------------------------------------------------- solveFile cfg = do fp <- getFixpointPath@@ -101,33 +102,32 @@ v <- (\b -> if b then "-v 1" else "") <$> isLoud ec <- {-# SCC "sysCall:Fixpoint" #-} executeShellCommand "fixpoint" $ fixCommand cfg fp z3 v rf return ec- where realFlags = "-no-uif-multiply " + where realFlags = "-no-uif-multiply " ++ "-no-uif-divide " rf = if (real cfg) then realFlags else "" -fixCommand cfg fp z3 verbosity realFlags - = printf "LD_LIBRARY_PATH=%s %s %s %s -notruekvars -refinesort -nosimple -strictsortcheck -sortedquals %s" +fixCommand cfg fp z3 verbosity realFlags+ = printf "LD_LIBRARY_PATH=%s %s %s %s -notruekvars -refinesort -nosimple -strictsortcheck -sortedquals %s" z3 fp verbosity realFlags (command cfg) -exitFq _ _ (ExitFailure n) | (n /= 1) +exitFq _ _ (ExitFailure n) | (n /= 1) = return (Crash [] "Unknown Error", M.empty)-exitFq fn cm _ +exitFq fn cm _ = do str <- {-# SCC "readOut" #-} readFile (extFileName Out fn) let (x, y) = parseFixpointOutput str -- {-# SCC "parseFixOut" #-} rr ({-# SCC "sanitizeFixpointOutput" #-} sanitizeFixpointOutput str)- return $ (plugC cm x, y) + return $ (plugC cm x, y) parseFixpointOutput :: String -> (FixResult Integer, FixSolution) parseFixpointOutput str = {-# SCC "parseFixOut" #-} rr ({-# SCC "sanitizeFixpointOutput" #-} sanitizeFixpointOutput str) plugC = fmap . mlookup -sanitizeFixpointOutput - = unlines - . filter (not . ("//" `isPrefixOf`)) +sanitizeFixpointOutput+ = unlines+ . filter (not . ("//" `isPrefixOf`)) . chopAfter ("//QUALIFIERS" `isPrefixOf`) . lines resultExit Safe = ExitSuccess resultExit (Unsafe _) = ExitFailure 1 resultExit _ = ExitFailure 2-
src/Language/Fixpoint/Misc.hs view
@@ -1,55 +1,58 @@-{-# LANGUAGE DeriveDataTypeable, TupleSections, NoMonomorphismRestriction, ScopedTypeVariables #-}-{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TupleSections #-} module Language.Fixpoint.Misc where -import Data.Traversable (traverse)-import Data.Hashable-import qualified Control.Exception as Ex--- import qualified Data.HashSet as S -import qualified Data.HashMap.Strict as M-import qualified Data.List as L-import qualified Data.ByteString as B-import qualified Data.Text as T-import Data.ByteString.Char8 (pack, unpack)-import Control.Applicative ((<$>))-import Control.Monad (forM_, (>=>))-import Data.Maybe (fromJust)-import Data.Maybe (catMaybes, fromMaybe)+import qualified Control.Exception as Ex+import Data.Hashable+import Data.Traversable (traverse)+-- import qualified Data.HashSet as S+import Control.Applicative ((<$>))+import Control.Monad (forM_, (>=>))+import qualified Data.ByteString as B+import Data.ByteString.Char8 (pack, unpack)+import qualified Data.HashMap.Strict as M+import qualified Data.List as L+import Data.Maybe (fromJust)+import Data.Maybe (catMaybes, fromMaybe)+import qualified Data.Text as T -import System.Exit-import System.Process (system)-import Debug.Trace (trace)-import Data.Data-import System.Console.ANSI-import System.Console.CmdArgs.Verbosity (whenLoud)+import Data.Data+import Debug.Trace (trace)+import System.Console.ANSI+import System.Console.CmdArgs.Verbosity (whenLoud)+import System.Exit+import System.Process (system) -import Text.PrettyPrint.HughesPJ+import Text.PrettyPrint.HughesPJ ----------------------------------------------------------------------------------- ------------ Support for Colored Logging ------------------------------------------ ----------------------------------------------------------------------------------- -data Moods = Ok | Loud | Sad | Happy | Angry +data Moods = Ok | Loud | Sad | Happy | Angry moodColor Ok = Black-moodColor Loud = Blue -moodColor Sad = Magenta -moodColor Happy = Green -moodColor Angry = Red +moodColor Loud = Blue+moodColor Sad = Magenta+moodColor Happy = Green+moodColor Angry = Red wrapStars msg = "\n**** " ++ msg ++ " " ++ replicate (74 - length msg) '*' wrapStarsWithOptStars True msg = "\n**** " ++ msg ++ " " ++ replicate (74 - length msg) '*' wrapStarsWithOptStars False msg = wrapStars msg --- withColor _ act = act +-- withColor _ act = act withColor c act- = do setSGR [ SetConsoleIntensity BoldIntensity, SetColor Foreground Vivid c] + = do setSGR [ SetConsoleIntensity BoldIntensity, SetColor Foreground Vivid c] act setSGR [ Reset] -colorStrLn c = withColor (moodColor c) . putStrLn +colorStrLn c = withColor (moodColor c) . putStrLn colorPhaseLn c msg = colorStrLn c . wrapStars . (msg ++) startPhase c msg = colorPhaseLn c "START: " msg >> colorStrLn Ok " " doneLine c msg = colorPhaseLn c "DONE: " msg >> colorStrLn Ok " "@@ -58,13 +61,13 @@ startPhaseWithOptStars v c msg = colorPhaseLnWithOptStars v c "START: " msg >> colorStrLn Ok " " doneLineWithOptStars v c msg = colorPhaseLnWithOptStars v c "DONE: " msg >> colorStrLn Ok " " -donePhase c str - = case lines str of +donePhase c str+ = case lines str of (l:ls) -> doneLine c l >> forM_ ls (colorPhaseLn c "") _ -> return () -donePhaseWithOptStars v c str - = case lines str of +donePhaseWithOptStars v c str+ = case lines str of (l:ls) -> doneLineWithOptStars v c l >> forM_ ls (colorPhaseLnWithOptStars v c "") _ -> return () @@ -76,7 +79,7 @@ unIntersperse x ys = case L.elemIndex x ys of Nothing -> [ys]- Just i -> let (y, _:ys') = splitAt i ys + Just i -> let (y, _:ys') = splitAt i ys in (y : unIntersperse x ys') (=>>) m f = m >>= (\x -> f x >> return x)@@ -85,17 +88,17 @@ repeats n = concat . replicate n -errorstar = error . wrap (stars ++ "\n") (stars ++ "\n") - where +errorstar = error . wrap (stars ++ "\n") (stars ++ "\n")+ where stars = repeats 3 $ wrapStars "ERROR" -errortext = errorstar . render +errortext = errorstar . render putDocLn :: Doc -> IO ()-putDocLn = putStrLn . render +putDocLn = putStrLn . render assertstar _ True x = x-assertstar msg False x = errorstar msg +assertstar msg False x = errorstar msg findWithDefaultL f ls d = fromMaybe d (L.find f ls) @@ -124,21 +127,21 @@ mapPair f (x, y) = (f x, f y) -- mlookup :: (Show k, Hashable k) => M.HashMap k v -> k -> v-mlookup m k +mlookup m k = case M.lookup k m of Just v -> v Nothing -> errorstar $ "mlookup: unknown key " ++ show k mfromJust :: String -> Maybe a -> a-mfromJust _ (Just x) = x +mfromJust _ (Just x) = x mfromJust s Nothing = errorstar $ "mfromJust: Nothing " ++ s -boxStrCat :: String -> [String] -> String -boxStrCat sep = ("[" ++) . (++ "]") . L.intercalate sep +boxStrCat :: String -> [String] -> String+boxStrCat sep = ("[" ++) . (++ "]") . L.intercalate sep tryIgnore :: String -> IO () -> IO ()-tryIgnore s a = Ex.catch a $ \e -> +tryIgnore s a = Ex.catch a $ \e -> do let err = show (e :: Ex.IOException) whenLoud $ putStrLn ("Warning: Couldn't do " ++ s ++ ": " ++ err) return ()@@ -152,27 +155,27 @@ -- inserts :: Hashable k => k -> v -> M.HashMap k [v] -> M.HashMap k [v] inserts k v m = M.insert k (v : M.lookupDefault [] k m) m -concatMaps = fmap sortNub . L.foldl' (M.unionWith (++)) M.empty +concatMaps = fmap sortNub . L.foldl' (M.unionWith (++)) M.empty -- group :: Hashable k => [(k, v)] -> M.HashMap k [v]-group = L.foldl' (\m (k, v) -> inserts k v m) M.empty +group = L.foldl' (\m (k, v) -> inserts k v m) M.empty groupList = M.toList . group -- groupMap :: Hashable k => (a -> k) -> [a] -> M.HashMap k [a]-groupMap f xs = L.foldl' (\m x -> inserts (f x) x m) M.empty xs +groupMap f xs = L.foldl' (\m x -> inserts (f x) x m) M.empty xs sortNub :: (Ord a) => [a] -> [a] sortNub = nubOrd . L.sort- where nubOrd (x:t@(y:_)) - | x == y = nubOrd t + where nubOrd (x:t@(y:_))+ | x == y = nubOrd t | otherwise = x : nubOrd t nubOrd xs = xs sortDiff :: (Ord a) => [a] -> [a] -> [a] sortDiff x1s x2s = go (sortNub x1s) (sortNub x2s)- where go xs@(x:xs') ys@(y:ys') + where go xs@(x:xs') ys@(y:ys') | x < y = x : go xs' ys | x == y = go xs' ys' | otherwise = go xs ys'@@ -186,49 +189,49 @@ distinct xs = length xs == length (sortNub xs) tr_reverse :: [a] -> [a]-tr_reverse = L.foldl' (flip (:)) [] +tr_reverse = L.foldl' (flip (:)) [] tr_foldr' :: (a -> b -> b) -> b -> [a] -> b-tr_foldr' f b = L.foldl' (flip f) b . tr_reverse +tr_foldr' f b = L.foldl' (flip f) b . tr_reverse -safeZip msg xs ys - | nxs == nys +safeZip msg xs ys+ | nxs == nys = zip xs ys- | otherwise + | otherwise = errorstar $ "safeZip called on non-eq-sized lists (nxs = " ++ show nxs ++ ", nys = " ++ show nys ++ ") : " ++ msg where nxs = length xs nys = length ys --- eqLen = on (==) length +-- eqLen = on (==) length -safeZipWith msg f xs ys - | nxs == nys +safeZipWith msg f xs ys+ | nxs == nys = zipWith f xs ys- | otherwise + | otherwise = errorstar $ "safeZipWith called on non-eq-sized lists (nxs = " ++ show nxs ++ ", nys = " ++ show nys ++ ") : " ++ msg where nxs = length xs nys = length ys --- safe0ZipWith msg f xs ys --- | length xs == length ys +-- safe0ZipWith msg f xs ys+-- | length xs == length ys -- = zipWith f xs ys -- safe0ZipWith _ _ [] _ -- = [] -- safe0ZipWith _ _ _ [] -- = []--- safe0ZipWith msg _ xs ys +-- safe0ZipWith msg _ xs ys -- = errorstar $ "safeZipWith called on non-eq-sized lists (nxs = " ++ show nxs ++ ", nys = " ++ show nys ++ ") : " ++ msg -- where nxs = length xs -- nys = length ys -- safeFromList :: (Hashable k, Show k, Show a) => String -> [(k, a)] -> M.HashMap k a-safeFromList msg = L.foldl' safeAdd M.empty - where safeAdd m (k, v) +safeFromList msg = L.foldl' safeAdd M.empty+ where safeAdd m (k, v) | k `M.member` m = errorstar $ msg ++ "Duplicate key " ++ show k ++ "maps to: \n" ++ (show v) ++ "\n and \n" ++ show (m M.! k) | otherwise = M.insert k v m -safeUnion msg m1 m2 = +safeUnion msg m1 m2 = case L.find (`M.member` m1) (M.keys m2) of Just k -> errorstar $ "safeUnion with common key = " ++ show k ++ " " ++ msg Nothing -> M.union m1 m2@@ -244,57 +247,57 @@ -- memoIndex :: (Hashable b) => (a -> Maybe b) -> [a] -> [Maybe Int]-memoIndex f = snd . L.mapAccumL foo M.empty - where +memoIndex f = snd . L.mapAccumL foo M.empty+ where foo memo z =- case f z of + case f z of Nothing -> (memo, Nothing)- Just k -> case k `M.lookup` memo of + Just k -> case k `M.lookup` memo of Just i -> (memo, Just i) Nothing -> (M.insert k (M.size memo) memo, Just (M.size memo)) checkFail :: [Char] -> (a -> Bool) -> a -> a-checkFail msg f x +checkFail msg f x | f x = x | otherwise = errorstar $ "Check-Failure: " ++ msg chopAfter :: (a -> Bool) -> [a] -> [a]-chopAfter f xs +chopAfter f xs = case L.findIndex f xs of Just n -> take n xs Nothing -> xs -chopPrefix p xs +chopPrefix p xs | p `L.isPrefixOf` xs = Just $ drop (length p) xs- | otherwise + | otherwise = Nothing firstElem :: (Eq a) => [(a, t)] -> [a] -> Maybe Int-firstElem seps str - = case catMaybes [ L.elemIndex c str | (c, _) <- seps ] of +firstElem seps str+ = case catMaybes [ L.elemIndex c str | (c, _) <- seps ] of [] -> Nothing- is -> Just $ minimum is + is -> Just $ minimum is chopAlt :: (Eq a) => [(a, a)] -> [a] -> [[a]]-chopAlt seps = go +chopAlt seps = go where go s = maybe [s] (go' s) (firstElem seps s)- go' s i = let (s0, s1@(c:_)) = splitAt i s - (Just c') = lookup c seps + go' s i = let (s0, s1@(c:_)) = splitAt i s+ (Just c') = lookup c seps in case L.elemIndex c' s1 of Nothing -> [s1]- Just i' -> let (s2, s3) = splitAt (i' + 1) s1 in + Just i' -> let (s2, s3) = splitAt (i' + 1) s1 in s0 : s2 : go s3 firstElems :: [(B.ByteString, B.ByteString)] -> B.ByteString -> Maybe (Int, B.ByteString, (B.ByteString, B.ByteString))-firstElems seps str - = case splitters seps str of +firstElems seps str+ = case splitters seps str of [] -> Nothing- is -> Just $ L.minimumBy (\x y -> compare (fst3 x) (fst3 y)) is + is -> Just $ L.minimumBy (\x y -> compare (fst3 x) (fst3 y)) is -splitters seps str +splitters seps str = [(i, c', z) | (c, c') <- seps , let z = B.breakSubstring c str , let i = B.length (fst z)@@ -302,25 +305,25 @@ bchopAlts :: [(B.ByteString, B.ByteString)] -> B.ByteString -> [B.ByteString]-bchopAlts seps = go - where +bchopAlts seps = go+ where go s = maybe [s] (go' s) (firstElems seps s) go' s (i,c',(s0, s1)) = if (B.length s2 == B.length s1) then [B.concat [s0,s1]] else (s0 : s2' : go s3') where (s2, s3) = B.breakSubstring c' s1 s2' = B.append s2 c'- s3' = B.drop (B.length c') s3 + s3' = B.drop (B.length c') s3 chopAlts seps str = unpack <$> bchopAlts [(pack c, pack c') | (c, c') <- seps] (pack str) findFirst :: Monad m => (t -> m [a]) -> [t] -> m (Maybe a) findFirst _ [] = return Nothing findFirst f (x:xs) = do r <- f x- case r of + case r of y:_ -> return (Just y) [] -> findFirst f xs testM f x = do b <- f x- return $ if b then [x] else [] + return $ if b then [x] else [] -- unions :: (Hashable a) => [S.HashSet a] -> S.HashSet a -- unions = foldl' S.union S.empty@@ -332,35 +335,35 @@ strip = T.stripPrefix "(" >=> T.stripSuffix ")" ifM :: (Monad m) => m Bool -> m a -> m a -> m a-ifM bm xm ym +ifM bm xm ym = do b <- bm if b then xm else ym -executeShellCommand phase cmd - = do whenLoud $ putStrLn $ "EXEC: " ++ cmd +executeShellCommand phase cmd+ = do whenLoud $ putStrLn $ "EXEC: " ++ cmd Ex.bracket_ (startPhase Loud phase) (donePhase Loud phase) $ system cmd -executeShellCommandWithOptStars v phase cmd - = do whenLoud $ putStrLn $ "EXEC: " ++ cmd +executeShellCommandWithOptStars v phase cmd+ = do whenLoud $ putStrLn $ "EXEC: " ++ cmd Ex.bracket_ (startPhaseWithOptStars v Loud phase) (donePhaseWithOptStars v Loud phase) $ system cmd checkExitCode _ (ExitSuccess) = return ()-checkExitCode cmd (ExitFailure n) = errorstar $ "cmd: " ++ cmd ++ " failure code " ++ show n +checkExitCode cmd (ExitFailure n) = errorstar $ "cmd: " ++ cmd ++ " failure code " ++ show n hashMapToAscList :: Ord a => M.HashMap a b -> [(a, b)] hashMapToAscList = L.sortBy (\x y -> compare (fst x) (fst y)) . M.toList hashMapMapWithKey :: (k -> v1 -> v2) -> M.HashMap k v1 -> M.HashMap k v2-hashMapMapWithKey f = fromJust . M.traverseWithKey (\k v -> Just (f k v)) +hashMapMapWithKey f = fromJust . M.traverseWithKey (\k v -> Just (f k v)) hashMapMapKeys :: (Eq k, Hashable k) => (t -> k) -> M.HashMap t v -> M.HashMap k v-hashMapMapKeys f = M.fromList . fmap (mapFst f) . M.toList +hashMapMapKeys f = M.fromList . fmap (mapFst f) . M.toList applyNonNull def _ [] = def applyNonNull _ f xs = f xs -concatMapM f = fmap concat . mapM f +concatMapM f = fmap concat . mapM f @@ -374,13 +377,13 @@ foldlMap :: (a -> b -> (c, a)) -> a -> [b] -> ([c], a) foldlMap f b xs = (reverse zs, res)- where + where (zs, res) = L.foldl' ff ([], b) xs ff (ys, acc) x = let (y, acc') = f acc x in (y:ys, acc') mapEither :: (a -> Either b c) -> [a] -> ([b], [c])-mapEither f = go [] [] - where +mapEither f = go [] []+ where go ls rs [] = (reverse ls, reverse rs) go ls rs (x:xs) = case f x of Left l -> go (l:ls) rs xs
src/Language/Fixpoint/Names.hs view
@@ -1,12 +1,12 @@-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeSynonymInstances #-}-{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ViewPatterns #-}-{-# LANGUAGE GeneralizedNewtypeDeriving #-} -- | This module contains Haskell variables representing globally visible names. -- Rather than have strings floating around the system, all constant names@@ -32,7 +32,7 @@ , qualifySymbol , suffixSymbol - -- * Hardwired global names + -- * Hardwired global names , dummyName , preludeName , boolConName@@ -48,23 +48,23 @@ , prims ) where -import GHC.Generics (Generic)-import Data.Char-import Data.String-import Data.Typeable (Typeable)-import Data.Generics (Data)-import Data.Text (Text)-import qualified Data.Text as T-import Data.Monoid-import Data.Interned-import Data.Interned.Internal.Text-import Data.Interned.Text-import Data.Hashable-import qualified Data.HashSet as S-import Control.Applicative-import Control.DeepSeq+import Control.Applicative+import Control.DeepSeq+import Data.Char+import Data.Generics (Data)+import Data.Hashable+import qualified Data.HashSet as S+import Data.Interned+import Data.Interned.Internal.Text+import Data.Interned.Text+import Data.Monoid+import Data.String+import Data.Text (Text)+import qualified Data.Text as T+import Data.Typeable (Typeable)+import GHC.Generics (Generic) -import Language.Fixpoint.Misc (errorstar, stripParens, mapSnd)+import Language.Fixpoint.Misc (errorstar, mapSnd, stripParens) --------------------------------------------------------------- ---------------------------- Symbols --------------------------@@ -251,7 +251,7 @@ vvName = "VV" symSepName = '#' -size32Name = "Size32" :: Symbol +size32Name = "Size32" :: Symbol size64Name = "Size64" :: Symbol bitVecName = "BitVec" :: Symbol bvOrName = "bvor" :: Symbol@@ -278,17 +278,17 @@ , size32Name , size64Name , bitVecName- , bvOrName + , bvOrName , bvAndName- , "FAppTy" + , "FAppTy" ] -- dropModuleNames [] = []--- dropModuleNames s --- | s == tupConName = tupConName +-- dropModuleNames s+-- | s == tupConName = tupConName -- | otherwise = safeLast msg $ words $ dotWhite `fmap` stripParens s--- where --- msg = "dropModuleNames: " ++ s +-- where+-- msg = "dropModuleNames: " ++ s -- dotWhite '.' = ' ' -- dotWhite c = c
src/Language/Fixpoint/Parse.hs view
@@ -1,21 +1,26 @@-{-# LANGUAGE NoMonomorphismRestriction, FlexibleInstances, UndecidableInstances, TypeSynonymInstances, TupleSections #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE UndecidableInstances #-} module Language.Fixpoint.Parse (- - -- * Top Level Class for Parseable Values ++ -- * Top Level Class for Parseable Values Inputable (..)- - -- * Top Level Class for Parseable Values ++ -- * Top Level Class for Parseable Values , Parser -- * Lexer to add new tokens- , lexer + , lexer -- * Some Important keyword and parsers , reserved, reservedOp , parens , brackets, angles, braces- , semi , comma - , colon , dcolon + , semi , comma+ , colon , dcolon , whiteSpace , blanks @@ -49,35 +54,35 @@ , freshIntP -- * Parsing Function- , doParse' + , doParse' , parseFromFile- , remainderP + , remainderP ) where -import Control.Applicative ((<*>), (<$>), (<*))-import Control.Monad-import Text.Parsec-import Text.Parsec.Expr-import Text.Parsec.Pos-import Text.Parsec.Language-import Text.Parsec.String hiding (Parser, parseFromFile)-import Text.Printf (printf)-import qualified Text.Parsec.Token as Token-import qualified Data.HashMap.Strict as M-import qualified Data.HashSet as S-import Data.Text (Text)-import qualified Data.Text as T+import Control.Applicative ((<$>), (<*), (<*>))+import Control.Monad+import qualified Data.HashMap.Strict as M+import qualified Data.HashSet as S+import Data.Text (Text)+import qualified Data.Text as T+import Text.Parsec+import Text.Parsec.Expr+import Text.Parsec.Language+import Text.Parsec.Pos+import Text.Parsec.String hiding (Parser, parseFromFile)+import qualified Text.Parsec.Token as Token+import Text.Printf (printf) -import Data.Char (isLower, toUpper)-import Language.Fixpoint.Misc hiding (dcolon)-import Language.Fixpoint.Types-import Language.Fixpoint.Bitvector-import Language.Fixpoint.Errors-import Language.Fixpoint.SmtLib2+import Data.Char (isLower, toUpper)+import Language.Fixpoint.Bitvector+import Language.Fixpoint.Errors+import Language.Fixpoint.Misc hiding (dcolon)+import Language.Fixpoint.SmtLib2+import Language.Fixpoint.Types -import Data.Maybe(maybe, fromJust)+import Data.Maybe (fromJust, maybe) -import Data.Monoid (mempty)+import Data.Monoid (mempty) type Parser = Parsec String Integer @@ -87,7 +92,7 @@ emptyDef { Token.commentStart = "/* " , Token.commentEnd = " */" , Token.commentLine = "--"- , Token.identStart = satisfy (\_ -> False) + , Token.identStart = satisfy (\_ -> False) , Token.identLetter = satisfy (\_ -> False) , Token.reservedNames = [ "SAT" , "UNSAT"@@ -112,10 +117,10 @@ ] , Token.reservedOpNames = [ "+", "-", "*", "/", "\\" , "<", ">", "<=", ">=", "=", "!=" , "/="- , "mod", "and", "or" + , "mod", "and", "or" --, "is" , "&&", "||"- , "~", "=>", "<=>"+ , "~", "=>", "==>", "<=>" , "->" , ":=" , "&", "^", "<<", ">>", "--"@@ -143,14 +148,14 @@ blanks = many (satisfy (`elem` [' ', '\t'])) -integer = posInteger - +integer = posInteger+ -- try (char '-' >> (negate <$> posInteger)) -- <|> posInteger posInteger = toI <$> (many1 digit <* spaces) where- toI :: String -> Integer + toI :: String -> Integer toI = read ----------------------------------------------------------------@@ -163,7 +168,7 @@ -- FIXME: we (LH) rely on this parser being dumb and *not* consuming trailing -- whitespace, in order to avoid some parsers spanning multiple lines.. condIdP :: [Char] -> (String -> Bool) -> Parser Symbol-condIdP chars f +condIdP chars f = do c <- letter cs <- many (satisfy (`elem` chars)) blanks@@ -175,7 +180,7 @@ lowerIdP :: Parser Symbol lowerIdP = condIdP symChars (isLower . head) -locLowerIdP = locParserP lowerIdP +locLowerIdP = locParserP lowerIdP locUpperIdP = locParserP upperIdP symbolP :: Parser Symbol@@ -188,7 +193,7 @@ symconstP = SL . T.pack <$> stringLiteral expr0P :: Parser Expr-expr0P +expr0P = (fastIfP EIte exprP) <|> (ESym <$> symconstP) <|> (ECon <$> constantP)@@ -203,65 +208,65 @@ where t = symbolText cs -- <|> try (parens $ condP EIte exprP) -fastIfP f bodyP - = do reserved "if" +fastIfP f bodyP+ = do reserved "if" p <- predP reserved "then"- b1 <- bodyP + b1 <- bodyP reserved "else"- b2 <- bodyP + b2 <- bodyP return $ f p b1 b2 expr1P :: Parser Expr-expr1P - = try funAppP - <|> expr0P +expr1P+ = try funAppP+ <|> expr0P -exprP :: Parser Expr +exprP :: Parser Expr exprP = buildExpressionParser bops expr1P funAppP = (try litP) <|> (try exprFunSpacesP) <|> (try exprFunSemisP) <|> exprFunCommasP- where - exprFunSpacesP = liftM2 EApp funSymbolP (sepBy1 expr0P blanks) + where+ exprFunSpacesP = liftM2 EApp funSymbolP (sepBy1 expr0P blanks) exprFunCommasP = liftM2 EApp funSymbolP (parens $ sepBy exprP comma) exprFunSemisP = liftM2 EApp funSymbolP (parenBrackets $ sepBy exprP semi) funSymbolP = locParserP symbolP -- | BitVector literal: lit "#x00000001" (BitVec (Size32 obj))-litP = do reserved "lit" +litP = do reserved "lit" l <- stringLiteral s <- try (bvSortP "Size32" S32) <|> bvSortP "Size64" S64 return $ ECon $ L (T.pack l) (mkSort s)- where + where bvSortP ss s = do parens (reserved "BitVec" >> parens (reserved ss >> reserved "obj")) return s --- ORIG exprP :: Parser Expr +-- ORIG exprP :: Parser Expr -- ORIG exprP = expr2P <|> lexprP--- --- ORIG lexprP :: Parser Expr --- ORIG lexprP +--+-- ORIG lexprP :: Parser Expr+-- ORIG lexprP -- ORIG = try (parens exprP) -- ORIG <|> try (parens exprCastP) -- ORIG <|> try (parens $ condP EIte exprP) -- ORIG <|> try exprFunP -- ORIG <|> try (liftM (EVar . stringSymbol) upperIdP)--- ORIG <|> liftM expr symbolP +-- ORIG <|> liftM expr symbolP -- ORIG <|> liftM ECon constantP -- ORIG <|> liftM ESym symconstP -- ORIG <|> (reserved "_|_" >> return EBot)--- ORIG +-- ORIG -- ORIG exprFunP = (try exprFunSpacesP) <|> (try exprFunSemisP) <|> exprFunCommasP--- ORIG where --- ORIG exprFunSpacesP = parens $ liftM2 EApp funSymbolP (sepBy exprP spaces) +-- ORIG where+-- ORIG exprFunSpacesP = parens $ liftM2 EApp funSymbolP (sepBy exprP spaces) -- ORIG exprFunCommasP = liftM2 EApp funSymbolP (parens $ sepBy exprP comma) -- ORIG exprFunSemisP = liftM2 EApp funSymbolP (parenBrackets $ sepBy exprP semi) -- ORIG funSymbolP = locParserP symbolP -- liftM stringSymbol lowerIdP -parenBrackets = parens . brackets +parenBrackets = parens . brackets -- ORIG expr2P = buildExpressionParser bops lexprP @@ -275,11 +280,11 @@ , [ Infix (reservedOp "mod" >> return (EBin Mod )) AssocLeft] ] -eMinus = EBin Minus (expr (0 :: Integer)) +eMinus = EBin Minus (expr (0 :: Integer)) exprCastP- = do e <- exprP + = do e <- exprP ((try dcolon) <|> colon) so <- sortP return $ ECst e so@@ -305,10 +310,10 @@ falseP = reserved "false" >> return PFalse pred0P :: Parser Pred-pred0P = trueP - <|> falseP +pred0P = trueP+ <|> falseP <|> try (fastIfP pIte predP)- <|> try predrP + <|> try predrP <|> try (parens predP) <|> try (liftM PBexp funAppP) <|> try (reservedOp "&&" >> liftM PAnd predsP)@@ -327,11 +332,12 @@ , [Infix (reservedOp "&&" >> return (\x y -> PAnd [x,y])) AssocRight] , [Infix (reservedOp "||" >> return (\x y -> POr [x,y])) AssocRight] , [Infix (reservedOp "=>" >> return PImp) AssocRight]+ , [Infix (reservedOp "==>" >> return PImp) AssocRight] , [Infix (reservedOp "<=>" >> return PIff) AssocRight]]- + predrP = do e1 <- exprP r <- brelP- e2 <- exprP + e2 <- exprP return $ r e1 e2 brelP :: Parser (Expr -> Expr -> Pred)@@ -346,28 +352,28 @@ <|> (reservedOp ">" >> return (PAtom Gt)) <|> (reservedOp ">=" >> return (PAtom Ge)) -condP f bodyP +condP f bodyP = try (condIteP f bodyP) <|> (condQmP f bodyP) -condI = condIteP EIte +condI = condIteP EIte -condIteP f bodyP - = do reserved "if" +condIteP f bodyP+ = do reserved "if" p <- predP reserved "then"- b1 <- bodyP + b1 <- bodyP reserved "else"- b2 <- bodyP + b2 <- bodyP return $ f p b1 b2 -condQmP f bodyP - = do p <- predP +condQmP f bodyP+ = do p <- predP reserved "?"- b1 <- bodyP + b1 <- bodyP colon- b2 <- bodyP + b2 <- bodyP return $ f p b1 b2 ----------------------------------------------------------------------------------@@ -381,7 +387,7 @@ <|> (symbolFTycon <$> locUpperIdP) refasP :: Parser [Refa]-refasP = (try (brackets $ sepBy (RConc <$> predP) semi)) +refasP = (try (brackets $ sepBy (RConc <$> predP) semi)) <|> liftM ((:[]) . RConc) predP refBindP :: Parser Symbol -> Parser [Refa] -> Parser (Reft -> a) -> Parser a@@ -405,8 +411,8 @@ -- qualifierP = mkQual <$> upperIdP <*> parens $ sepBy1 sortBindP comma <*> predP -qualifierP = do pos <- getPosition - n <- upperIdP +qualifierP = do pos <- getPosition+ n <- upperIdP params <- parens $ sepBy1 sortBindP comma _ <- colon body <- predP@@ -415,13 +421,13 @@ sortBindP = (,) <$> symbolP <* colon <*> sortP mkQual n xts p pos = Q n ((vv, t) : yts) (subst su p) pos- where + where (vv,t):zts = xts yts = mapFst mkParam <$> zts- su = mkSubst $ zipWith (\(z,_) (y,_) -> (z, eVar y)) zts yts - + su = mkSubst $ zipWith (\(z,_) (y,_) -> (z, eVar y)) zts yts+ mkParam s = symbol ('~' `T.cons` toUpper c `T.cons` cs)- where + where Just (c,cs)= T.uncons $ symbolText s ---------------------------------------------------------------------@@ -442,7 +448,7 @@ <|> IBind <$> (reserved "bind" >> intP) <*> symbolP <*> (colon >> sortedReftP) sortedReftP :: Parser SortedReft-sortedReftP = refP (RR <$> (sortP <* spaces)) +sortedReftP = refP (RR <$> (sortP <* spaces)) wfCP :: Parser (WfC ()) wfCP = do reserved "env"@@ -452,25 +458,25 @@ return $ wfC env r Nothing () subCP :: Parser (SubC ())-subCP = do reserved "env" - env <- envP +subCP = do reserved "env"+ env <- envP reserved "grd" grd <- predP reserved "lhs"- lhs <- sortedReftP + lhs <- sortedReftP reserved "rhs"- rhs <- sortedReftP + rhs <- sortedReftP reserved "id" i <- (integer <* spaces) tag <- tagP- return $ safeHead "subCP" $ subC env grd lhs rhs (Just i) tag () + return $ safeHead "subCP" $ subC env grd lhs rhs (Just i) tag () tagP :: Parser [Int] tagP = try (reserved "tag" >> spaces >> (brackets $ sepBy intP semi)) <|> (return []) envP :: Parser IBindEnv-envP = do binds <- brackets $ sepBy (intP <* spaces) semi +envP = do binds <- brackets $ sepBy (intP <* spaces) semi return $ insertsIBindEnv binds emptyIBindEnv intP :: Parser Int@@ -478,24 +484,24 @@ defsFInfo :: [Def a] -> FInfo a defsFInfo defs = FI cm ws bs gs lts kts qs- where + where cm = M.fromList [(cid c, c) | Cst c <- defs] ws = [w | Wfc w <- defs] bs = rawBindEnv [(n, x, r) | IBind n x r <- defs] gs = fromListSEnv [(x, RR t mempty) | Con x t <- defs] lts = [(x, t) | Con x t <- defs, notFun t]- kts = KS $ S.fromList [k | Kut k <- defs] + kts = KS $ S.fromList [k | Kut k <- defs] qs = [q | Qul q <- defs] cid = fromJust . sid- notFun = not . isFunctionSortedReft . (`RR` trueReft) + notFun = not . isFunctionSortedReft . (`RR` trueReft) --------------------------------------------------------------------- -- | Interacting with Fixpoint -------------------------------------- --------------------------------------------------------------------- fixResultP :: Parser a -> Parser (FixResult a)-fixResultP pp +fixResultP pp = (reserved "SAT" >> return Safe)- <|> (reserved "UNSAT" >> Unsafe <$> (brackets $ sepBy pp comma)) + <|> (reserved "UNSAT" >> Unsafe <$> (brackets $ sepBy pp comma)) <|> (reserved "CRASH" >> crashP pp) crashP pp@@ -503,41 +509,41 @@ msg <- many anyChar return $ Crash [i] msg -predSolP - = parens $ (predP <* (comma >> iQualP)) - +predSolP+ = parens $ (predP <* (comma >> iQualP)) + iQualP = upperIdP >> (parens $ sepBy symbolP comma) solution1P- = do reserved "solution:" - k <- symbolP - reserved ":=" + = do reserved "solution:"+ k <- symbolP+ reserved ":=" ps <- brackets $ sepBy predSolP semi return (k, simplify $ PAnd ps) solutionP :: Parser (M.HashMap Symbol Pred)-solutionP +solutionP = M.fromList <$> sepBy solution1P whiteSpace -solutionFileP +solutionFileP = liftM2 (,) (fixResultP integer) solutionP ------------------------------------------------------------------------ -remainderP p +remainderP p = do res <- p str <- getInput- pos <- getPosition - return (res, str, pos) + pos <- getPosition+ return (res, str, pos) doParse' parser f s = case runParser (remainderP (whiteSpace >> parser)) 0 f s of- Left e -> die $ err (errorSpan e) $ printf "parseError %s\n when parsing from %s\n" (show e) f + Left e -> die $ err (errorSpan e) $ printf "parseError %s\n when parsing from %s\n" (show e) f Right (r, "", _) -> r Right (_, rem, l) -> die $ err (SS l l) $ printf "doParse has leftover when parsing: %s\nfrom file %s\n" rem f- + errorSpan e = SS l l where l = errorPos e parseFromFile :: Parser b -> SourceName -> IO b@@ -554,7 +560,7 @@ commandsP = sepBy commandP semi -commandP +commandP = (reserved "var" >> cmdVarP) <|> (reserved "push" >> return Push) <|> (reserved "pop" >> return Pop)@@ -562,8 +568,8 @@ <|> (reserved "assert" >> (Assert Nothing <$> predP)) <|> (reserved "distinct" >> (Distinct <$> (brackets $ sepBy exprP comma))) -cmdVarP - = do x <- bindP +cmdVarP+ = do x <- bindP t <- sortP return $ Declare x [] t @@ -576,19 +582,19 @@ rr :: String -> a rr' :: String -> String -> a rr' = \_ -> rr- rr = rr' "" + rr = rr' "" instance Inputable Symbol where rr' = doParse' symbolP instance Inputable Constant where- rr' = doParse' constantP + rr' = doParse' constantP instance Inputable Pred where- rr' = doParse' predP + rr' = doParse' predP instance Inputable Expr where- rr' = doParse' exprP + rr' = doParse' exprP instance Inputable [Refa] where rr' = doParse' refasP@@ -597,13 +603,13 @@ rr' = doParse' $ fixResultP integer instance Inputable (FixResult Integer, FixSolution) where- rr' = doParse' solutionFileP + rr' = doParse' solutionFileP instance Inputable (FInfo ()) where rr' = doParse' fInfoP instance Inputable Command where- rr' = doParse' commandP + rr' = doParse' commandP instance Inputable [Command] where rr' = doParse' commandsP@@ -615,7 +621,7 @@ -- A few tricky predicates for parsing -- myTest1 = "((((v >= 56320) && (v <= 57343)) => (((numchars a o ((i - o) + 1)) == (1 + (numchars a o ((i - o) - 1)))) && (((numchars a o (i - (o -1))) >= 0) && (((i - o) - 1) >= 0)))) && ((not (((v >= 56320) && (v <= 57343)))) => (((numchars a o ((i - o) + 1)) == (1 + (numchars a o (i - o)))) && ((numchars a o (i - o)) >= 0))))"--- +-- -- myTest2 = "len x = len y - 1" -- myTest3 = "len x y z = len a b c - 1" -- myTest4 = "len x y z = len a b (c - 1)"@@ -651,7 +657,7 @@ s9 = "v = x+y" s10 = "{v: Int | v = x + y}" -s11 = "x:{v:Int | true } -> {v:Int | true }" +s11 = "x:{v:Int | true } -> {v:Int | true }" s12 = "y : {v:Int | true } -> {v:Int | v = x }" s13 = "x:{v:Int | true } -> y:{v:Int | true} -> {v:Int | v = x + y}" s14 = "x:{v:a | true} -> y:{v:b | true } -> {v:a | (x < v && v < y) }"@@ -661,24 +667,24 @@ s18 = "x:a -> Bool" s20 = "forall a . x:Int -> Bool" -s21 = "x:{v : GHC.Prim.Int# | true } -> {v : Int | true }" +s21 = "x:{v : GHC.Prim.Int# | true } -> {v : Int | true }" r0 = (rr s0) :: Pred r0' = (rr s0) :: [Refa] r1 = (rr s1) :: [Refa] -e1, e2 :: Expr +e1, e2 :: Expr e1 = rr "(k_1 + k_2)"-e2 = rr "k_1" +e2 = rr "k_1" o1, o2, o3 :: FixResult Integer-o1 = rr "SAT " +o1 = rr "SAT " o2 = rr "UNSAT [1, 2, 9,10]"-o3 = rr "UNSAT []" +o3 = rr "UNSAT []" -- sol1 = doParse solution1P "solution: k_5 := [0 <= VV_int]"--- sol2 = doParse solution1P "solution: k_4 := [(0 <= VV_int)]" +-- sol2 = doParse solution1P "solution: k_4 := [(0 <= VV_int)]" b0, b1, b2, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13 :: BareType b0 = rr "Int"@@ -701,7 +707,7 @@ m1 = ["len :: [a] -> Int", "len (Nil) = 0", "len (Cons x xs) = 1 + len(xs)"] m2 = ["tog :: LL a -> Int", "tog (Nil) = 100", "tog (Cons y ys) = 200"] -me1, me2 :: Measure.Measure BareType Symbol -me1 = (rr $ intercalate "\n" m1) +me1, me2 :: Measure.Measure BareType Symbol+me1 = (rr $ intercalate "\n" m1) me2 = (rr $ intercalate "\n" m2) -}
src/Language/Fixpoint/PrettyPrint.hs view
@@ -1,15 +1,15 @@-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-} module Language.Fixpoint.PrettyPrint where -import Text.PrettyPrint.HughesPJ-import Language.Fixpoint.Types-import Language.Fixpoint.Misc-import Control.Applicative ((<$>))-import Text.Parsec-import qualified Data.Text as T+import Control.Applicative ((<$>))+import qualified Data.Text as T+import Language.Fixpoint.Misc+import Language.Fixpoint.Types+import Text.Parsec+import Text.PrettyPrint.HughesPJ class PPrint a where pprint :: a -> Doc
src/Language/Fixpoint/SmtLib2.hs view
@@ -1,12 +1,12 @@-{-# LANGUAGE NoMonomorphismRestriction #-}-{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE BangPatterns #-} {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE RecordWildCards #-}-{-# LANGUAGE BangPatterns #-} {-# LANGUAGE PatternGuards #-}+{-# LANGUAGE RecordWildCards #-}+{-# LANGUAGE UndecidableInstances #-} -- | This module contains an SMTLIB2 interface for -- 1. checking the validity, and,@@ -40,28 +40,29 @@ , smt_set_funs ) where -import Language.Fixpoint.Config (SMTSolver (..))-import Language.Fixpoint.Files-import Language.Fixpoint.Types+import Language.Fixpoint.Config (SMTSolver (..))+import Language.Fixpoint.Files+import Language.Fixpoint.Types -import Control.Monad-import Data.Char-import qualified Data.List as L-import qualified Data.HashMap.Strict as M-import Data.Monoid-import Data.Text.Format-import qualified Data.Text as T-import qualified Data.Text.IO as TIO-import qualified Data.Text.Lazy as LT-import qualified Data.Text.Lazy.IO as LTIO-import System.Directory-import System.Exit-import System.FilePath-import System.Process-import System.IO (openFile, IOMode (..), Handle, hFlush, hClose)-import Control.Applicative ((<$>), (<|>), (*>), (<*))+import Control.Applicative ((*>), (<$>), (<*), (<|>))+import Control.Monad+import Data.Char+import qualified Data.HashMap.Strict as M+import qualified Data.List as L+import Data.Monoid+import qualified Data.Text as T+import Data.Text.Format+import qualified Data.Text.IO as TIO+import qualified Data.Text.Lazy as LT+import qualified Data.Text.Lazy.IO as LTIO+import System.Directory+import System.Exit+import System.FilePath+import System.IO (Handle, IOMode (..), hClose, hFlush,+ openFile)+import System.Process -import qualified Data.Attoparsec.Text as A+import qualified Data.Attoparsec.Text as A {- Usage: runFile f@@ -104,10 +105,10 @@ deriving (Eq, Show) -- | Information about the external SMT process-data Context = Ctx { pId :: ProcessHandle- , cIn :: Handle- , cOut :: Handle- , cLog :: Maybe Handle+data Context = Ctx { pId :: ProcessHandle+ , cIn :: Handle+ , cOut :: Handle+ , cLog :: Maybe Handle , verbose :: Bool } @@ -123,7 +124,7 @@ -------------------------------------------------------------------------- command :: Context -> Command -> IO Response ---------------------------------------------------------------------------command me !cmd = {-# SCC command #-} say me cmd >> hear me cmd+command me !cmd = {-# SCC "command" #-} say me cmd >> hear me cmd where say me = smtWrite me . smt2 hear me CheckSat = smtRead me@@ -136,7 +137,7 @@ smtWrite me !s = smtWriteRaw me s smtRead :: Context -> IO Response-smtRead me = {-# SCC smtRead #-}+smtRead me = {-# SCC "smtRead" #-} do ln <- smtReadRaw me res <- A.parseWith (smtReadRaw me) responseP ln case A.eitherResult res of@@ -147,19 +148,19 @@ LTIO.putStrLn $ format "SMT Says: {}" (Only $ show r) return r -responseP = {-# SCC responseP #-} A.char '(' *> sexpP+responseP = {-# SCC "responseP" #-} A.char '(' *> sexpP <|> A.string "sat" *> return Sat <|> A.string "unsat" *> return Unsat <|> A.string "unknown" *> return Unknown -sexpP = {-# SCC sexpP #-} A.string "error" *> (Error <$> errorP)+sexpP = {-# SCC "sexpP" #-} A.string "error" *> (Error <$> errorP) <|> Values <$> valuesP errorP = A.skipSpace *> A.char '"' *> A.takeWhile1 (/='"') <* A.string "\")" valuesP = A.many1' pairP <* (A.char ')') -pairP = {-# SCC pairP #-}+pairP = {-# SCC "pairP" #-} do A.skipSpace A.char '(' !x <- symbolP@@ -168,9 +169,9 @@ A.char ')' return (x,v) -symbolP = {-# SCC symbolP #-} symbol <$> A.takeWhile1 (not . isSpace)+symbolP = {-# SCC "symbolP" #-} symbol <$> A.takeWhile1 (not . isSpace) -valueP = {-# SCC valueP #-} negativeP+valueP = {-# SCC "valueP" #-} negativeP <|> A.takeWhile1 (\c -> not (c == ')' || isSpace c)) negativeP@@ -184,12 +185,12 @@ ((x:y:[]),zs) -> (x,y) : pairs zs smtWriteRaw :: Context -> LT.Text -> IO ()-smtWriteRaw me !s = {-# SCC smtWriteRaw #-} do+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)+smtReadRaw me = {-# SCC "smtReadRaw" #-} TIO.hGetLine (cIn me) hPutStrLnNow h !s = LTIO.hPutStrLn h s >> hFlush h @@ -239,13 +240,13 @@ smtCmd Cvc4 = "cvc4 --incremental -L smtlib2" -- DON'T REMOVE THIS! z3 changed the names of options between 4.3.1 and 4.3.2...-smtPreamble Z3 me +smtPreamble Z3 me = do smtWrite me "(get-info :version)" r <- (!!1) . T.splitOn "\"" <$> smtReadRaw me case T.words r of "4.3.2" : _ -> return $ z3_432_options ++ z3Preamble _ -> return $ z3_options ++ z3Preamble-smtPreamble _ _ +smtPreamble _ _ = return smtlibPreamble smtFile :: FilePath@@ -281,8 +282,8 @@ bit = "BitVec" sz32 = "Size32" sz64 = "Size64"- + emp, add, cup, cap, mem, dif, sub, com :: Raw emp = "smt_set_emp" add = "smt_set_add"@@ -294,19 +295,19 @@ com = "smt_set_com" sel = "smt_map_sel" sto = "smt_map_sto"- + smt_set_funs :: M.HashMap Symbol Raw smt_set_funs = M.fromList [ ("Set_emp",emp),("Set_add",add),("Set_cup",cup) , ("Set_cap",cap),("Set_mem",mem),("Set_dif",dif) , ("Set_sub",sub),("Set_com",com)] -- DON'T REMOVE THIS! z3 changed the names of options between 4.3.1 and 4.3.2...-z3_432_options +z3_432_options = [ "(set-option :auto-config false)" , "(set-option :model true)" , "(set-option :model.partial false)" , "(set-option :smt.mbqi false)" ]-z3_options +z3_options = [ "(set-option :auto-config false)" , "(set-option :model true)" , "(set-option :model-partial false)"@@ -382,7 +383,7 @@ -- FIXME: this is probably too slow encode :: T.Text -> T.Text-encode t = {-# SCC encode #-}+encode t = {-# SCC "encode" #-} foldr (\(x,y) t -> T.replace x y t) t [("[", "ZM"), ("]", "ZN"), (":", "ZC") ,("(", "ZL"), (")", "ZR"), (",", "ZT") ,("|", "zb"), ("#", "zh"), ("\\","zr")
src/Language/Fixpoint/Sort.hs view
@@ -1,8 +1,9 @@+{-# LANGUAGE FlexibleContexts #-} -- | This module has the functions that perform sort-checking, and related -- operations on Fixpoint expressions and predicates. -module Language.Fixpoint.Sort ( +module Language.Fixpoint.Sort ( -- * Checking Well-Formedness checkSorted , checkSortedReft@@ -13,51 +14,51 @@ -import Language.Fixpoint.Types-import Language.Fixpoint.Misc-import Text.PrettyPrint.HughesPJ-import Text.Printf-import Control.Monad.Error (catchError, throwError)-import Control.Monad-import Control.Applicative-import Data.Maybe (fromMaybe, catMaybes)-import qualified Data.HashMap.Strict as M+import Control.Applicative+import Control.Monad+import Control.Monad.Error (catchError, throwError)+import qualified Data.HashMap.Strict as M+import Data.Maybe (catMaybes, fromMaybe)+import Language.Fixpoint.Misc+import Language.Fixpoint.Types+import Text.PrettyPrint.HughesPJ+import Text.Printf -import Debug.Trace (trace)+import Debug.Trace (trace) -- | Types used throughout checker type CheckM a = Either String a type Env = Symbol -> SESearch Sort-fProp = FApp boolFTyCon [] --- fProp = FApp propFTyCon [] +fProp = FApp boolFTyCon []+-- fProp = FApp propFTyCon [] ------------------------------------------------------------------------- -- | Checking Refinements ----------------------------------------------- ------------------------------------------------------------------------- checkSortedReft :: SEnv SortedReft -> [Symbol] -> SortedReft -> Maybe Doc-checkSortedReft env xs sr = applyNonNull Nothing error unknowns - where - error = Just . (text "Unknown symbols:" <+>) . toFix - unknowns = [ x | x <- syms sr, not (x `elem` v : xs), not (x `memberSEnv` env)] - Reft (v,_) = sr_reft sr +checkSortedReft env xs sr = applyNonNull Nothing error unknowns+ where+ error = Just . (text "Unknown symbols:" <+>) . toFix+ unknowns = [ x | x <- syms sr, not (x `elem` v : xs), not (x `memberSEnv` env)]+ Reft (v,_) = sr_reft sr checkSortedReftFull :: Checkable a => SEnv SortedReft -> a -> Maybe Doc checkSortedReftFull γ t = case check γ' t of Left err -> Just (text err) Right _ -> Nothing- where - γ' = mapSEnv sr_sort γ + where+ γ' = mapSEnv sr_sort γ checkSortFull :: Checkable a => SEnv SortedReft -> Sort -> a -> Maybe Doc checkSortFull γ s t = case checkSort γ' s t of Left err -> Just (text err) Right _ -> Nothing- where - γ' = mapSEnv sr_sort γ + where+ γ' = mapSEnv sr_sort γ checkSorted :: Checkable a => SEnv Sort -> a -> Maybe Doc checkSorted γ t@@ -67,8 +68,8 @@ pruneUnsortedReft :: SEnv Sort -> SortedReft -> SortedReft pruneUnsortedReft γ (RR s (Reft (v, ras)))- = RR s (Reft (v, catMaybes (go <$> ras))) - where + = RR s (Reft (v, catMaybes (go <$> ras)))+ where go r = case checkRefa f r of Left war -> trace (wmsg war r) $ Nothing Right _ -> Just r@@ -104,9 +105,9 @@ checkEqSort s t | s == t = return ()- | otherwise = throwError $ "Couldn't match expected type '" + | otherwise = throwError $ "Couldn't match expected type '" ++ show s ++ "'"- ++ "\n\t\t with actual type '" + ++ "\n\t\t with actual type '" ++ show t ++ "'" instance Checkable Pred where@@ -115,17 +116,17 @@ instance Checkable SortedReft where check γ (RR s (Reft (v, ras))) = mapM_ (check γ') ras- where γ' = insertSEnv v s γ + where γ' = insertSEnv v s γ ------------------------------------------------------------------------- -- | Checking Expressions ----------------------------------------------- ------------------------------------------------------------------------- -checkExpr :: Env -> Expr -> CheckM Sort +checkExpr :: Env -> Expr -> CheckM Sort checkExpr _ EBot = throwError "Type Error: Bot"-checkExpr _ (ECon (I _)) = return FInt -checkExpr _ (ECon (R _)) = return FReal +checkExpr _ (ECon (I _)) = return FInt+checkExpr _ (ECon (R _)) = return FReal checkExpr f (EVar x) = checkSym f x checkExpr f (ENeg e) = checkNeg f e checkExpr f (EBin o e1 e2) = checkOp f e1 o e2@@ -136,8 +137,8 @@ -- | Helper for checking symbol occurrences -checkSym f x - = case f x of +checkSym f x+ = case f x of Found s -> return s Alts xs -> throwError $ errUnboundAlts x xs -- $ traceFix ("checkSym: x = " ++ showFix x) (f x)@@ -146,17 +147,17 @@ -- | Helper for checking if-then-else expressions -checkIte f p e1 e2 +checkIte f p e1 e2 = do tp <- checkPred f p t1 <- checkExpr f e1 t2 <- checkExpr f e2 ((`apply` t1) <$> unify [t1] [t2]) `catchError` (\_ -> throwError $ errIte e1 e2 t1 t2) --- | Helper for checking cast expressions +-- | Helper for checking cast expressions -checkCst f t (EApp g es) +checkCst f t (EApp g es) = checkApp f (Just t) g es-checkCst f t e +checkCst f t e = do t' <- checkExpr f e ((`apply` t) <$> unify [t] [t']) `catchError` (\_ -> throwError $ errCast e t' t) @@ -164,7 +165,7 @@ = snd <$> checkApp' f to g es -- | Helper for checking uninterpreted function applications-checkApp' f to g es +checkApp' f to g es = do gt <- checkLocSym f g (n, its, ot) <- sortFunction gt unless (length its == length es) $ throwError (errArgArity g its es)@@ -188,15 +189,15 @@ _ -> throwError $ printf "Operand has non-numeric type %s in %s" (showFix t) (showFix e) -checkOp f e1 o e2 +checkOp f e1 o e2 = do t1 <- checkExpr f e1 t2 <- checkExpr f e2 checkOpTy f (EBin o e1 e2) t1 t2 -checkOpTy f _ FReal FReal +checkOpTy f _ FReal FReal = return FReal -checkOpTy f _ FInt FInt +checkOpTy f _ FInt FInt = return FInt checkOpTy f e t@(FObj l) t'@(FObj l')@@ -207,7 +208,9 @@ = throwError $ errOp e t t' checkFractional f l- = throwError $ errNonFractional l+ = do t <- checkSym f l+ unless (t == FFrac) (throwError $ errNonFractional l)+ return () checkNumeric f l = do t <- checkSym f l@@ -218,13 +221,13 @@ -- | Checking Predicates ------------------------------------------------ ------------------------------------------------------------------------- -checkPred :: Env -> Pred -> CheckM () +checkPred :: Env -> Pred -> CheckM () checkPred f PTrue = return () checkPred f PFalse = return ()-checkPred f (PBexp e) = checkPredBExp f e +checkPred f (PBexp e) = checkPredBExp f e checkPred f (PNot p) = checkPred f p-checkPred f (PImp p p') = mapM_ (checkPred f) [p, p'] +checkPred f (PImp p p') = mapM_ (checkPred f) [p, p'] checkPred f (PIff p p') = mapM_ (checkPred f) [p, p'] checkPred f (PAnd ps) = mapM_ (checkPred f) ps checkPred f (POr ps) = mapM_ (checkPred f) ps@@ -234,8 +237,8 @@ checkPredBExp f e = do t <- checkExpr f e unless (t == fProp) (throwError $ errBExp e t) return ()- + -- | Checking Relations checkRel f Eq (EVar x) (EApp g es) = checkRelEqVar f x g es@@ -245,12 +248,12 @@ checkRelTy f (PAtom r e1 e2) r t1 t2 checkRelTy :: (Fixpoint a) => Env -> a -> Brel -> Sort -> Sort -> CheckM ()-checkRelTy f _ _ (FObj l) (FObj l') | l /= l' - = (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) (FObj l') | l /= l'+ = (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 FReal = return ()-checkRelTy f _ _ FReal (FObj l) = (checkFractional f l) `catchError` (\_ -> throwError $ errNonFractional l) +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@@ -270,7 +273,7 @@ checkRelTy _ e _ t1 t2 = unless (t1 == t2) (throwError $ errRel e t1 t2) --- | Special case for polymorphic singleton variable equality e.g. (x = Set_emp) +-- | Special case for polymorphic singleton variable equality e.g. (x = Set_emp) checkRelEqVar f x g es = do tx <- checkSym f x _ <- checkApp f (Just tx) g es@@ -297,32 +300,32 @@ errUnify t1 t2 = printf "Cannot unify %s with %s" (showFix t1) (showFix t2) -errUnifyMany ts ts' = printf "Cannot unify types with different cardinalities %s and %s" +errUnifyMany ts ts' = printf "Cannot unify types with different cardinalities %s and %s" (showFix ts) (showFix ts') -errRel e t1 t2 = printf "Invalid Relation %s with operand types %s and %s" +errRel e t1 t2 = printf "Invalid Relation %s with operand types %s and %s" (showFix e) (showFix t1) (showFix t2) errBExp e t = printf "BExp %s with non-propositional type %s" (showFix e) (showFix t) -errOp e t t' - | t == t' = printf "Operands have non-numeric types %s in %s" +errOp e t t'+ | t == t' = printf "Operands have non-numeric types %s in %s" (showFix t) (showFix e)- | otherwise = printf "Operands have different types %s and %s in %s" + | otherwise = printf "Operands have different types %s and %s in %s" (showFix t) (showFix t') (showFix e) -errArgArity g its es = printf "Measure %s expects %d args but gets %d in %s" +errArgArity g its es = printf "Measure %s expects %d args but gets %d in %s" (showFix g) (length its) (length es) (showFix (EApp g es)) -errIte e1 e2 t1 t2 = printf "Mismatched branches in Ite: then %s : %s, else %s : %s" - (showFix e1) (showFix t1) (showFix e2) (showFix t2) +errIte e1 e2 t1 t2 = printf "Mismatched branches in Ite: then %s : %s, else %s : %s"+ (showFix e1) (showFix t1) (showFix e2) (showFix t2) -errCast e t' t = printf "Cannot cast %s of sort %s to incompatible sort %s" +errCast e t' t = printf "Cannot cast %s of sort %s to incompatible sort %s" (showFix e) (showFix t') (showFix t) errUnbound x = printf "Unbound Symbol %s" (showFix x)-errUnboundAlts x xs = printf "Unbound Symbol %s\n Perhaps you meant: %s" - (showFix x) +errUnboundAlts x xs = printf "Unbound Symbol %s\n Perhaps you meant: %s"+ (showFix x) (foldr1 (\w s -> w ++ ", " ++ s) (showFix <$> xs)) errNonFunction t = printf "Sort %s is not a function" (showFix t)@@ -342,26 +345,26 @@ unify = unifyMany (Th M.empty) -unifyMany θ ts ts' +unifyMany θ ts ts' | length ts == length ts' = foldM (uncurry . unify1) θ $ zip ts ts' | otherwise = throwError $ errUnifyMany ts ts' -- unify1 _ FNum _ = Nothing unify1 θ (FVar i) t = unifyVar θ i t unify1 θ t (FVar i) = unifyVar θ i t-unify1 θ (FApp c ts) (FApp c' ts') - | c == c' = unifyMany θ ts ts' -unify1 θ t1 t2 +unify1 θ (FApp c ts) (FApp c' ts')+ | c == c' = unifyMany θ ts ts'+unify1 θ t1 t2 | t1 == t2 = return θ | otherwise = throwError $ errUnify t1 t2 -unifyVar θ i t +unifyVar θ i t = case lookupVar i θ of- Just t' -> if t == t' then return θ else throwError (errUnify t t') - Nothing -> return $ updateVar i t θ + Just t' -> if t == t' then return θ else throwError (errUnify t t')+ Nothing -> return $ updateVar i t θ -- | Sort Substitutions-newtype TVSubst = Th (M.HashMap Int Sort) +newtype TVSubst = Th (M.HashMap Int Sort) -- | API for manipulating substitutions lookupVar i (Th m) = M.lookup i m@@ -384,10 +387,10 @@ -- | Deconstruct a function-sort --------------------------------------- ------------------------------------------------------------------------ -sortFunction (FFunc n ts') = return (n, ts, t) - where +sortFunction (FFunc n ts') = return (n, ts, t)+ where ts = take numArgs ts' t = last ts' numArgs = length ts' - 1 -sortFunction t = throwError $ errNonFunction t +sortFunction t = throwError $ errNonFunction t
src/Language/Fixpoint/Types.hs view
@@ -1,13 +1,14 @@-{-# LANGUAGE NoMonomorphismRestriction #-}-{-# LANGUAGE DeriveGeneric #-}-{-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE DeriveTraversable #-}-{-# LANGUAGE DeriveFoldable #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE OverloadedStrings #-}-{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE DeriveFoldable #-}+{-# LANGUAGE DeriveGeneric #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE UndecidableInstances #-} -- | This module contains the data types, operations and serialization functions@@ -56,7 +57,7 @@ -- * Expressions and Predicates , SymConst (..)- , Constant (..) + , Constant (..) , Bop (..), Brel (..) , Expr (..), Pred (..) , eVar@@ -156,38 +157,39 @@ , dummyLoc, dummyPos, dummyName, isDummy ) where -import Debug.Trace (trace)+import Debug.Trace (trace) -import GHC.Generics (Generic)-import Data.Typeable (Typeable)-import Data.Generics (Data)+import Data.Generics (Data)+import Data.Typeable (Typeable)+import GHC.Generics (Generic) -import Data.Monoid hiding ((<>))-import Data.Functor-import Data.Char (ord, chr, isAlpha, isUpper, toLower)-import Data.List (nub, foldl', sort, stripPrefix, intersect)-import Data.Hashable-import qualified Data.Foldable as F-import Data.Traversable-import Data.Interned-import Data.String-import Data.Text (Text)-import qualified Data.Text as T+import Data.Char (chr, isAlpha, isUpper, ord, toLower)+import qualified Data.Foldable as F+import Data.Functor+import Data.Hashable+import Data.Interned+import Data.List (foldl', intersect, nub, sort,+ stripPrefix)+import Data.Monoid hiding ((<>))+import Data.String+import Data.Text (Text)+import qualified Data.Text as T+import Data.Traversable -import Data.Maybe (fromMaybe)-import Text.Printf (printf)-import Control.DeepSeq-import Control.Arrow ((***))-import Control.Exception (assert)+import Control.Arrow ((***))+import Control.DeepSeq+import Control.Exception (assert)+import Data.Maybe (fromMaybe)+import Text.Printf (printf) -import Language.Fixpoint.Misc-import Text.PrettyPrint.HughesPJ-import Text.Parsec.Pos+import Language.Fixpoint.Misc+import Text.Parsec.Pos+import Text.PrettyPrint.HughesPJ -import qualified Data.HashMap.Strict as M-import qualified Data.HashSet as S-import Data.Array hiding (indices)-import Language.Fixpoint.Names+import Data.Array hiding (indices)+import qualified Data.HashMap.Strict as M+import qualified Data.HashSet as S+import Language.Fixpoint.Names class Fixpoint a where toFix :: a -> Doc@@ -340,7 +342,7 @@ fObj :: LocSymbol -> Sort fObj = fTyconSort . TC - + ---------------------------------------------------------------------- ------------------------------- Sorts -------------------------------- ----------------------------------------------------------------------@@ -348,11 +350,12 @@ data Sort = FInt | FReal | FNum -- ^ numeric kind for Num tyvars+ | FFrac -- ^ numeric kind for Fractional tyvars | FObj Symbol -- ^ uninterpreted type | FVar !Int -- ^ fixpoint type variable | FFunc !Int ![Sort] -- ^ type-var arity, in-ts ++ [out-t] | FApp FTycon [Sort] -- ^ constructed type- deriving (Eq, Ord, Show, Data, Typeable, Generic)+ deriving (Eq, Ord, Show, Data, Typeable, Generic) instance Hashable Sort @@ -364,6 +367,7 @@ toFix_sort (FVar i) = text "@" <> parens (toFix i) toFix_sort FInt = text "int" toFix_sort FReal = text "real"+toFix_sort FFrac = text "frac" toFix_sort (FObj x) = toFix x toFix_sort FNum = text "num" toFix_sort (FFunc n ts) = text "func" <> parens ((toFix n) <> (text ", ") <> (toFix ts))@@ -415,7 +419,7 @@ data Constant = I !Integer | R !Double- | L !Text !Sort + | L !Text !Sort deriving (Eq, Ord, Show, Data, Typeable, Generic) data Brel = Eq | Ne | Gt | Ge | Lt | Le | Ueq | Une@@ -423,7 +427,7 @@ data Bop = Plus | Minus | Times | Div | Mod deriving (Eq, Ord, Show, Data, Typeable, Generic)- -- NOTE: For "Mod" 2nd expr should be a constant or a var *)+ -- NOTE: For "Mod" 2nd expr should be a constant or a var *) data Expr = ESym !SymConst | ECon !Constant@@ -446,8 +450,8 @@ instance Fixpoint Constant where toFix (I i) = toFix i toFix (R i) = toFix i- toFix (L s t) = parens $ text "lit" <+> text "\"" <> toFix s <> text "\"" <+> toFix t - + toFix (L s t) = parens $ text "lit" <+> text "\"" <> toFix s <> text "\"" <+> toFix t+ instance Fixpoint SymConst where toFix = toFix . encodeSymConst @@ -609,7 +613,7 @@ -- | Generalizing Symbol, Expression, Predicate into Classes ----------- ------------------------------------------------------------------------ --- | Values that can be viewed as Constants +-- | Values that can be viewed as Constants -- | Values that can be viewed as Expressions @@ -683,7 +687,7 @@ instance Show Reft where show (Reft x) = render $ toFix x -data SortedReft = RR { sr_sort :: !Sort, sr_reft :: !Reft } +data SortedReft = RR { sr_sort :: !Sort, sr_reft :: !Reft } deriving (Eq, Show, Data, Typeable, Generic) isNonTrivialSortedReft (RR _ (Reft (_, ras)))@@ -785,7 +789,7 @@ instance (Fixpoint a) => Fixpoint (SEnv a) where toFix (SE e) = vcat $ map pprxt $ hashMapToAscList e- where pprxt (x, t) = toFix x <+> colon <> colon <+> toFix t+ where pprxt (x, t) = toFix x <+> colon <> colon <+> toFix t instance Fixpoint (SEnv a) => Show (SEnv a) where show = render . toFix@@ -827,7 +831,7 @@ data FixResult a = Crash [a] String | Safe | Unsafe ![a]- | UnknownError !String + | UnknownError !String deriving (Show, Generic) type FixSolution = M.HashMap Symbol Pred@@ -1151,7 +1155,7 @@ rnf (I x) = rnf x rnf (R x) = rnf x rnf (L s t) = rnf s `seq` rnf t- + instance NFData SymConst where rnf (SL x) = rnf x @@ -1286,7 +1290,7 @@ toFix = pprQual instance NFData Qualifier where- rnf (Q x1 x2 x3 _) = rnf x1 `seq` rnf x2 `seq` rnf x3 + rnf (Q x1 x2 x3 _) = rnf x1 `seq` rnf x2 `seq` rnf x3 pprQual (Q n xts p l) = text "qualif" <+> text (symbolString n) <> parens args <> colon <+> toFix p <+> text "//" <+> toFix l where args = intersperse comma (toFix <$> xts)@@ -1350,7 +1354,7 @@ toReft :: r -> Reft ofReft :: Reft -> r params :: r -> [Symbol] -- ^ parameters for Reft, vv + others- + instance Monoid Pred where mempty = PTrue mappend p q = pAnd [p, q]
src/Language/Fixpoint/Visitor.hs view
@@ -3,24 +3,24 @@ module Language.Fixpoint.Visitor ( -- * Visitor Visitor (..)- + -- * Default Visitor , defaultVisitor -- * Transformers , trans- + -- * Accumulators , fold ) where +import Control.Applicative (Applicative (), (<$>), (<*>))+import Control.Exception (throw)+import Control.Monad.Trans.State (State, modify, runState) 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 Data.Traversable (traverse)+import Language.Fixpoint.Misc (mapSnd) import Language.Fixpoint.Types @@ -31,14 +31,14 @@ , ctxPred :: ctx -> Pred -> ctx -- | Transforms can access current @ctx@- , txExpr :: ctx -> Expr -> Expr - , txPred :: ctx -> Pred -> Pred + , 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 ---------------------------------------------------------------------------------@@ -49,20 +49,20 @@ , txPred = \_ x -> x , accExpr = \_ _ -> mempty , accPred = \_ _ -> mempty- } + } ------------------------------------------------------------------------- +------------------------------------------------------------------------ -fold :: (Visitable t, Monoid a) => Visitor a ctx -> ctx -> a -> t -> a +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 +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 +type VisitM acc = State acc accum :: (Monoid a) => a -> VisitM a () accum = modify . mappend@@ -81,15 +81,15 @@ instance Visitable Refa where visit v c (RConc p) = RConc <$> visit v c p- visit _ _ r = return r + visit _ _ r = return r instance Visitable Reft where- visit v c (Reft (vv, ras)) = (Reft . (vv,)) <$> visitMany v c ras + 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 :: (Monoid a) => Visitor a ctx -> ctx -> Expr -> VisitM a Expr visitExpr v = vE where vP = visitPred v@@ -97,17 +97,17 @@ 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@(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 (EApp f es) = EApp f <$> (vE c <$$> es) step c (ENeg e) = ENeg <$> vE c e step c (EBin o e1 e2) = EBin o <$> vE c e1 <*> vE c e2 step c (EIte p e1 e2) = EIte <$> vP c p <*> vE c e1 <*> vE c e2 step c (ECst e t) = (`ECst` t) <$> vE c e- -visitPred :: (Monoid a) => Visitor a ctx -> ctx -> Pred -> VisitM a Pred ++visitPred :: (Monoid a) => Visitor a ctx -> ctx -> Pred -> VisitM a Pred visitPred v = vP where vE = visitExpr v@@ -115,14 +115,13 @@ 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 (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 (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 (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-