liquid-fixpoint-0.2.3.2: external/fixpoint/ast.ml
(*
* 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
* TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.
*
*)
(**
* 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.
* 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
*)
(* random touch *)
module F = Format
module Misc = FixMisc
open Misc.Ops
module SM = Misc.StringMap
let mydebug = false
module Cone = struct
type 'a t = Empty | Cone of ('a * 'a t) list
let rec map f = function
| Empty -> Empty
| Cone xcs -> Cone (List.map (f <**> map f) xcs)
end
module Sort =
struct
type loc =
| Loc of string
| Lvar of int
| LFun
type tycon = string
type t =
| Int
| Real
| Bool
| 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)) -- *)
| Frac (* kind, for fractional tyvars -- ptr(loc(s)) -- *)
| App of tycon * t list (* type constructors *)
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
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_frac = Frac
let t_obj = Obj
let t_bool = Bool
let t_int = Int
let t_real = Real
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 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
*)
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 = App (c, ts) *)
let loc_to_string = function
| Loc s -> s
| Lvar i -> string_of_int i
| LFun -> "<fun>"
let rec to_string = function
| Var i -> Printf.sprintf "@(%d)" i
| Int -> "int"
| Real -> "real"
| Bool -> "bool"
| Obj -> "obj"
| Num -> "num"
| 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
| App (_, _) -> Printf.sprintf "(%s)" (to_string t)
| _ -> to_string t
let to_string_short = function
| Func _ -> "func"
(* | Ptr _ -> "ptr" *)
| t -> to_string t
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))
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
let rec fold f b = function
| 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
| Var i -> Misc.do_catchf "ERROR: subs_tvar" (List.nth ts) i
| t -> t
end
let is_bool = function
| Bool -> true
| _ -> false
let is_int = function
| Int -> true
| _ -> false
let is_real = function
| Real -> true
| _ -> false
let is_func = function
| Func _ -> true
| _ -> false
let is_kind = function
| Num -> true
| _ -> false
let app_of_t = function
| 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
*)
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)
*)
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
let func_of_t = function
| Func (i, ts) -> let (xts, t) = ts |> Misc.list_snoc |> Misc.swap in
Some (i, xts, t)
| _ -> None
let ptr_of_t = function
| Ptr l -> Some l
| _ -> None
(* Sleazy Hack for C pointers. Make this go away... *)
let compat t1 t2 = match t1, t2 with
| Int, (Ptr _) -> true
| (Ptr _), Int -> true
| _ -> t1 = t2
(* {{{
let concretize ts = function
| Func (n, ats) when n = List.length ts ->
Func (n, List.map (subs_tvar ts) ats)
| _ ->
assertf "ERROR: bad application"
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
| Num,_ | _, Num -> None
| 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 _, Ptr LFun -> Some s
| Ptr (Loc cl), Ptr (Lvar j)
| Ptr (Lvar j), Ptr (Loc cl) ->
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)
when c1 = c2 && List.length t1s = List.length t2s ->
Misc.maybe_fold unifyt s (List.combine t1s t2s)
| (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"
(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))
*)
let unify = unifyWith empty_sub
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)
| _ -> t
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
| _ -> acc
end []
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 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 lim = Misc.index_from idx locs |>: Misc.swap |> SM.of_list in
List.map (subst_locs_vars lim) ts
(* API *)
let sub_args s = List.sort compare s.vars
(* API *)
let check_arity n s = s.vars |>: fst |> Misc.sort_and_compact |> List.length |> (=) n
(* if ... then s else assertf "Type Inst. With Wrong Arity!" *)
end
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 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_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 ->
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"
let vvprefix = "VV_"
let vvsuffix = function
| Sort.Ptr l -> Sort.loc_to_string l
| t -> Sort.to_string_short t
let is_value_variable = Misc.is_prefix vvprefix
let value_variable t = vvprefix ^ (vvsuffix t)
(* DEBUG *)
let vvprefix = "VV"
let is_value_variable = (=) vvprefix
let value_variable _ = vvprefix
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 =
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_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
*)
end
module Constant =
struct
type t = Int of int
| Real of float
| Lit of string * Sort.t
let to_string = function
| Int i -> string_of_int i
| Real i -> string_of_float i ^ "0"
| Lit (s,t) -> Printf.sprintf "(lit \"%s\" %s)" s (Sort.to_string t)
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 *)
| Ge (* greater than or equal *)
| Lt (* less than *)
| Le (* less than or equal *)
| 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
and expr_int =
| Con of Constant.t
| Var of Symbol.t
| App of Symbol.t * expr list
| 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
| Bot
| MExp of expr list
| MBin of expr * bop list * expr
and pred = pred_int * tag
and pred_int =
| True
| False
| And of pred list
| Or of pred list
| Not of pred
| Imp of pred * pred
| Iff of pred * pred
| Bexp of 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 =
List.fold_left (fun v (_,id) -> 2*v + id) b xs
module Hashcons (X : sig type t
val sub_equal : t -> t -> bool
val hash : t -> int end) = struct
module HashStruct = struct
type t = X.t * int
let equal (x,_) (y,_) = X.sub_equal x y
let hash (x,_) = X.hash x
end
module Hash = Weak.Make(HashStruct)
let wrap =
let tab = Hash.create 251 in
let ctr = ref 0 in
fun e ->
let res = Hash.merge tab (e, !ctr) in
let _ = if snd res = !ctr then incr ctr in
res
let unwrap (e,_) = e
end
module ExprHashconsStruct = struct
type t = expr_int
let sub_equal e1 e2 =
match e1, e2 with
| Con c1, Con c2 ->
c1 = c2
| MExp es1, MExp es2 ->
es1 = es2
| Var x1, Var x2 ->
x1 = x2
| App (s1, e1s), App (s2, e2s) ->
(s1 = s2) &&
(try List.for_all2 (==) e1s e2s with _ -> false)
| Bin (e1, op1, e1'), Bin (e2, op2, e2') ->
op1 = op2 && e1 == e2 && e1' == e2'
| MBin (e1, ops1, e1'), MBin (e2, ops2, e2') ->
ops1 = ops2 && e1 == e2 && e1' == e2'
| Ite (ip1,te1,ee1), Ite (ip2,te2,ee2) ->
ip1 == ip2 && te1 == te2 && ee1 == ee2
| Fld (s1, e1), Fld (s2, e2) ->
s1 = s2 && e1 == e2
| Cst (e1, s1), Cst (e2, s2) ->
s1 = s2 && e1 == e2
| _ ->
false
let hash = function
| Con (Constant.Int x) ->
x
| Con (Constant.Real x) ->
64 + int_of_float x
| Con (Constant.Lit (s,_)) ->
32 + Hashtbl.hash s
| MExp es ->
list_hash 6 es
| Var x ->
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)) ->
32 + (4 * id1) + (2 * id2) + id3
| Fld (s, (_,id)) ->
(Hashtbl.hash s) + 12 + id
| Cst ((_, id), t) ->
id + Hashtbl.hash (Sort.to_string t)
| Bot ->
0
| _ -> 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
| And p1s, And p2s | Or p1s, Or p2s ->
(try List.for_all2 (==) p1s p2s with _ -> false)
| Not p1, Not p2 ->
p1 == 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 ->
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) ->
q1s = q2s && p1 == p2
| _ ->
false
let hash = function
| True ->
0
| False ->
1
| And ps ->
list_hash 2 ps
| Or ps ->
list_hash 3 ps
| Not (_,id) ->
8 + id
| Imp ((_,id1), (_,id2)) ->
20 + (2 * id1) + id2
| Iff ((_,id1), (_,id2)) ->
28 + (2 * id1) + id2
| Bexp (_, id) ->
32 + id
| Atom ((_,id1), r, (_,id2)) ->
36 + (Hashtbl.hash r) + (2 * id1) + id2
| MAtom ((_,id1), r, (_,id2)) ->
42 + (Hashtbl.hash r) + (2 * id1) + id2
| 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 puw = PredHashcons.unwrap
(* Constructors: Expressions *)
let eCon = fun c -> ewr (Con c)
let eMExp = fun es -> ewr (MExp es)
let eInt = fun i -> eCon (Constant.Int i)
let zero = eInt 0
let one = eInt 1
let bot = ewr Bot
let eMod = fun (e, e') -> ewr (Bin (e, Mod, e'))
(* let eMod = fun (e, m) -> ewr (Bin (e, Mod, eInt m)) *)
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 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), _) ->
ewr (Con (Constant.Int (n1 * n2)))
| (Con (Constant.Int 1), _), e2 ->
e2
| (Con (Constant.Int (-1)), _), e2 ->
eBin (zero, Minus, e2)
| (e1, e2) -> eBin (e1, Times, e2)
let rec conjuncts = function
| And ps, _ -> Misc.flap conjuncts ps
| True, _ -> []
| p -> [p]
(* Constructors: Predicates *)
let pTrue = pwr True
let pFalse = pwr False
let pAtom = fun (e1, r, e2) -> pwr (Atom (e1, r, e2))
let pMAtom = fun (e1, r, e2) -> pwr (MAtom (e1, r, e2))
let pOr = fun ps -> pwr (Or ps)
let pNot = fun p -> pwr (Not p)
let pBexp = fun e -> pwr (Bexp e)
let pImp = fun (p1,p2) -> pwr (Imp (p1,p2))
let pIff = fun (p1,p2) -> pwr (Iff (p1,p2))
let pForall = fun (qs, p) -> pwr (Forall (qs, p))
let pEqual = fun (e1,e2) -> pAtom (e1, Eq, e2)
let pUequal = fun (e1,e2) -> pAtom (e1, Ueq, e2)
let pAnd = fun ps -> match Misc.flap conjuncts ps with
| [] -> pTrue
| [p] -> p
| ps -> pwr (And (Misc.flap conjuncts ps))
module ExprHash = Hashtbl.Make(struct
type t = expr
let equal (_,x) (_,y) = (x = y)
let hash (_,x) = x
end)
module PredHash = Hashtbl.Make(struct
type t = pred
let equal (_,x) (_,y) = (x = y)
let hash (_,x) = x
end)
let bop_to_string = function
| Plus -> "+"
| Minus -> "-"
| Times -> "*"
| Div -> "/"
| Mod -> "mod"
let brel_to_string = function
| Eq -> "="
| Ne -> "!="
| Gt -> ">"
| Ge -> ">="
| Lt -> "<"
| Le -> "<="
| Ueq -> "~~"
| Une -> "!~"
let print_brel ppf r =
F.fprintf ppf "%s" (brel_to_string r)
let print_binding ppf (s,t) =
F.fprintf ppf "%a:%a" Symbol.print s Sort.print 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 ->
F.fprintf ppf "[%a]" (Misc.pprint_many false " ; " print_expr) es
| Var s ->
F.fprintf ppf "%a" Symbol.print s
| 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)
print_expr e2
| MBin (e1, ops, e2) ->
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
print_expr te
print_expr ee
(* DEPRECATED TO HELP HS Parser
| 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
| Cst(e,t) ->
F.fprintf ppf "(%a : %a)"
print_expr e
Sort.print t
| Bot ->
F.fprintf ppf "_|_"
and print_pred ppf p = match puw p with
| True ->
F.fprintf ppf "true"
| 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 ->
F.fprintf ppf "(~ (%a))" print_pred p
| 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
| 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" | _ ->
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 e2
| MAtom (e1, rs, e2) ->
F.fprintf ppf "(%a [%a] %a)"
(* F.fprintf ppf "@[(%a [%a] %a)@]" *)
print_expr e1
(Misc.pprint_many false " ; " print_brel) rs
print_expr e2
| 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 =
match euw e with
| Con c ->
Constant.to_string c
| MExp es ->
Printf.sprintf "[%s]" (es |>: expr_to_string |> String.concat " ; ")
| Var s ->
Symbol.to_string s
| App (s, es) ->
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)"
(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)
(ops |> List.map bop_to_string |> String.concat "; ")
(expr_to_string e2)
| 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
| Cst(e,t) ->
Printf.sprintf "(%s : %s)" (expr_to_string e) (Sort.to_string t)
| Bot ->
Printf.sprintf "_|_"
and pred_to_string p =
match puw p with
| True ->
"true"
| False ->
"false"
| Bexp e ->
Printf.sprintf "(Bexp %s)" (expr_to_string e)
| 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 ->
Printf.sprintf "&& [%s]" (List.map pred_to_string ps |> String.concat " ; ")
| Or ps ->
Printf.sprintf "|| [%s]" (List.map pred_to_string ps |> String.concat ";")
| Atom (e1, r, e2) ->
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)"
(expr_to_string e1)
(List.map brel_to_string rs |> String.concat " ; ")
(expr_to_string e2)
| 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' =
match puw p with
| 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) ->
Imp (pm p1, pm p2)
| Iff (p1, p2) ->
Iff (pm p1, pm p2)
| Bexp 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) ->
MAtom (expr_map hp he fp fe e1, rs, expr_map hp he fp fe e2)
| Forall (qs, p) ->
Forall (qs, pm p) in
let rv = fp (pwr p') in
let _ = PredHash.add hp p rv in
rv
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' =
match euw e with
| Con _ | Var _ | Bot as e1 ->
e1
| MExp es ->
MExp (List.map em es)
| App (f, es) ->
App (f, List.map em es)
| Bin (e1, op, e2) ->
Bin (em e1, op, em e2)
| 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)
in
let rv = fe (ewr e') in
let _ = ExprHash.add he e rv in
rv
end in em e
let rec pred_iter fp fe pw =
begin match puw pw with
| True | False -> ()
| Bexp e -> expr_iter fp fe e
| Not p -> pred_iter fp fe p
| Imp (p1, p2) -> pred_iter fp fe p1; pred_iter fp fe p2
| Iff (p1, p2) -> pred_iter fp fe p1; pred_iter fp fe p2
| And ps | Or ps -> List.iter (pred_iter fp fe) ps
| Atom (e1, _, e2) -> expr_iter fp fe e1; expr_iter fp fe e2
| MAtom (e1, _, e2) -> expr_iter fp fe e1; expr_iter fp fe e2
| Forall (_, p) -> pred_iter fp fe p (* pmr: looks wrong, but so does pred_map *)
end;
fp pw
and expr_iter fp fe ew =
begin match puw ew with
| Con _ | Var _ | Bot ->
()
| MExp es ->
List.iter (expr_iter fp fe) es
| App (_, es) ->
List.iter (expr_iter fp fe) es
| Bin (e1, _, e2) ->
expr_iter fp fe e1; expr_iter fp fe e2
| MBin (e1, _, e2) ->
expr_iter fp fe e1; expr_iter fp fe e2
| Ite (ip, te, ee) ->
pred_iter fp fe ip; expr_iter fp fe te; expr_iter fp fe ee
| 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
let expr_subst hp he e x 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
module Expression =
struct
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 iter fp fe e =
expr_iter fp fe e
let subst e x e' =
map id (esub x e') e
let substs e xes =
map id (fun e -> List.fold_left (esub |> Misc.uncurry |> Misc.flip) e xes) e
let support e =
let xs = ref Symbol.SSet.empty in
iter un begin function
| (Var x), _
| (App (x,_)),_ -> xs := Symbol.SSet.add x !xs
| _ -> ()
end e;
Symbol.SSet.elements !xs |> List.sort compare
let unwrap = euw
let has_bot p =
let r = ref false in
iter un begin function
| Bot, _ -> r := true
| _ -> ()
end p;
!r
end
module Predicate = struct
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
pred_map hp he fp fe p
let iter fp fe p =
pred_iter fp fe p
let subst p x e' =
map id (esub x e') p
let substs p xes =
map id (fun e -> List.fold_left (esub |> Misc.uncurry |> Misc.flip) e xes) p
let support p =
let xs = ref Symbol.SSet.empty in
iter un begin function
| (Var x), _
| (App (x,_)),_ -> xs := Symbol.SSet.add x !xs;
| _ -> ()
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
!c
let size p =
let c = ref 0 in
let _ = iter (fun _ -> incr c) p in
!c
*)
let unwrap = puw
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
let rec is_tauto = function
| Atom(e1, Eq, e2), _ -> snd e1 == snd e2
| Atom(e1, Ueq, e2), _ -> snd e1 == snd e2
| Imp (p1, p2), _ -> snd p1 == snd p2
| And ps, _ -> List.for_all is_tauto ps
| Or ps, _ -> List.exists is_tauto ps
| True, _ -> true
| _ -> false
let has_bot p =
let r = ref false in
iter un begin function
| Bot, _ -> r := true
| _ -> ()
end p;
!r
end
let print_stats _ =
Printf.printf "Ast Stats. [none] \n"
(********************************************************************************)
(************************** Rationalizing Division ******************************)
(********************************************************************************)
let expr_isdiv = function
| Bin (_, Div, _), _ -> true
| _ -> false
let pull_divisor = function
| Bin (_, Div, (Con (Constant.Int i),_)), _ -> i
| _ -> 1
let calc_cm e1 e2 =
pull_divisor e1 * pull_divisor e2
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)
| Bin (e1, op, e2), _ ->
eBin (apply_mult m e1, op, apply_mult m e2)
| Con (Constant.Int i), _ ->
eCon (Constant.Int (i*m))
| e ->
eTim (eCon (Constant.Int m), e)
let rec pred_isdiv = function
| True,_ | False,_ ->
false
| And ps,_ | Or ps,_ ->
List.exists pred_isdiv ps
| Not p, _ | Forall (_, p), _ ->
pred_isdiv p
| Imp (p1, p2), _ ->
pred_isdiv p1 || pred_isdiv p2
| Iff (p1, p2), _ ->
pred_isdiv p1 || pred_isdiv p2
| Bexp e, _ ->
expr_isdiv e
| 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)]
let rec fixdiv = function
| 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)
| 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)
| p -> p
(***************************************************************************)
(************* Type Checking Expressions and Predicates ********************)
(***************************************************************************)
let sortcheck_sym f s = f s
(* try Some (f s) with _ -> None *)
let sortcheck_loc f = function
| Sort.Loc s -> sortcheck_sym f (Symbol.of_string s)
| Sort.Lvar _ -> None
| Sort.LFun -> None
let uf_arity f uf =
match sortcheck_sym f uf with None -> None | Some t ->
match Sort.func_of_t t with None -> None | Some (i,_,_) ->
Some i
let solved_app f uf = function
| Some (s, t) -> begin match uf_arity f uf with
| Some n -> if Sort.check_arity n s then Some t else None
| _ -> None
end
| None -> None
let rec sortcheck_expr g f e =
match euw e with
| Bot ->
None
| Con (Constant.Int _) ->
Some Sort.Int
| Con (Constant.Real _) ->
Some Sort.Real
| Con (Constant.Lit (_, t)) ->
Some t
| Var s ->
sortcheck_sym f s
| Bin (e1, op, e2) ->
sortcheck_op g f (e1, op, e2)
| Ite (p, e1, e2) ->
if sortcheck_pred g f p then
match Misc.map_pair (sortcheck_expr g f) (e1, e2) with
| (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
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)
"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
else
match Sort.unify e_ts i_ts with
| None -> None
| Some s ->
let t = Sort.apply s o_t in
match so_expected with
| None -> Some (s, t)
| Some t' ->
match Sort.unifyWith s [t] [t'] with
| 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
| 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"
(expr_to_string (eApp (uf, es)))
end
*)
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"
in *)
match Misc.map_pair (sortcheck_expr g f) (e1, e2) with
| (Some Sort.Int, Some Sort.Int)
-> Some Sort.Int
| (Some Sort.Real, Some Sort.Real)
-> Some Sort.Real
(* only allow when language is Haskell *)
| (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)
(* only allow when language is C *)
| (Some (Sort.Ptr s), Some (Sort.Ptr s'))
when op = Minus && s = s'
-> Some Sort.Int
| _ -> None
and sortcheck_rel g f (e1, r, e2) =
let t1o, t2o = (e1,e2) |> Misc.map_pair (sortcheck_expr g f) in
match r, t1o, t2o with
| _, Some (Sort.Ptr _) , Some (Sort.Ptr Sort.LFun)
| _, Some (Sort.Ptr Sort.LFun), Some (Sort.Ptr _)
-> true
| _ , 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))
|| ((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 (_,_))
-> true
| _ , Some (Sort.App (tc,_)), _
when (g tc) (* tc is an interpreted tycon *)
-> false
| _ , Some t1, Some t2
-> t1 = t2 && t1 != Sort.Bool
| _ -> false
and sortcheck_pred g f p =
match puw p with
| True
| False ->
true
| Bexp e ->
sortcheck_expr g f e = Some Sort.Bool
| Not p ->
sortcheck_pred g f p
| Imp (p1, p2) | Iff (p1, p2) ->
List.for_all (sortcheck_pred g f) [p1; p2]
| 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)),_))
when not (!Constants.strictsortcheck)
-> not (None = sortcheck_expr g f e)
| Atom (((Con _, _) as e) , Eq, (App (uf, es), _))
| Atom ((App (uf, es), _), Eq, ((Con _, _) as e))
| Atom (((Var _, _) as e) , Eq, (App (uf, es), _))
| Atom ((App (uf, es), _), Eq, ((Var _, _) as e))
(* -> begin match sortcheck_sym f x with *)
-> begin match sortcheck_expr g f e with
| 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))
-> let t1o = solved_app f uf1 <| sortcheck_app_sub g f None uf1 e1s in
let t2o = solved_app f uf2 <| sortcheck_app_sub g f None uf2 e2s in
begin match t1o, t2o with
| (Some t1, Some t2) -> t1 = t2
| (None, None) -> false
| (None, Some t2) -> not (None = sortcheck_app g f (Some t2) uf1 e1s)
| (Some t1, None) -> not (None = sortcheck_app g f (Some t1) uf2 e2s)
end
| Atom (e1, r, e2) ->
sortcheck_rel g f (e1, r, e2)
| Forall (qs,p) ->
(* let f' = fun x -> try List.assoc x qs with _ -> f x in *)
let f' = fun x -> match Misc.list_assoc_maybe x qs with None -> f x | y -> y
in sortcheck_pred g f' p
| _ -> failwith "Unexpected: sortcheck_pred"
(* 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)
*)
let opt_to_string p = function
| None -> "none"
| Some x -> p x
(* 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)
else
None
(*
let msg = Printf.sprintf "Ast.sortcheck_app: type params not instantiated %s: n = %d, s = %s, t = %s, tExp = %s"
(expr_to_string (eApp (uf, es)))
n
(Sort.sub_to_string s)
(Sort.to_string t)
(opt_to_string Sort.to_string tExp)
in
assertf "%s" msg
*)
| _ -> None
(*
let sortcheck_pred f p =
sortcheck_pred f p
>> (fun b -> ignore <| F.printf "sortcheck_pred: p = %a, res = %b\n"
Predicate.print p b)
*)
(***************************************************************************)
(************* Simplifying Expressions and Predicates **********************)
(***************************************************************************)
let pred_of_bool = function true -> pTrue | false -> pFalse
let rec remove_bot pol ((p, _) as pred) =
match p with
| Not p ->
pNot (remove_bot (not pol) p)
| Imp (p, q) ->
pImp (remove_bot (not pol) p, remove_bot pol q)
| Forall (qs, p) ->
pForall (qs, remove_bot pol p)
| And ps ->
ps |> List.map (remove_bot pol) |> pAnd
| 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 ->
pred_of_bool pol
| _ ->
pred
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
| Gt -> Lt
| Ge -> Le
| Lt -> Gt
| Le -> Ge
let neg_brel = function
| Eq -> Ne
| Ueq -> Une
| Ne -> Eq
| Une -> Ueq
| Gt -> Le
| Ge -> Lt
| Lt -> Ge
| Le -> Gt
let rec push_neg ?(neg=false) ((p, _) as pred) =
match p with
| True ->
if neg then pFalse else pred
| False ->
if neg then pTrue else pred
| Bexp _ ->
if neg then pNot pred else pred
| Not p ->
push_neg ~neg:(not neg) p
| 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) ->
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
|> if neg then pOr else pAnd
| Or ps ->
List.map (push_neg ~neg:neg) ps
|> if neg then pAnd else pOr
| Atom (e1, brel, e2) ->
if neg then pAtom (e1, neg_brel brel, e2) else pred
| _ -> failwith "Unexpected: push_neg"
(* Andrey: TODO flatten nested conjunctions/disjunctions *)
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)
| Forall (qs, p) -> pForall (qs, simplify_pred p)
| 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
|> List.filter (not <.> Predicate.is_contra)
|> (function [] -> pFalse
| [p] -> p
| ps when List.exists Predicate.is_tauto ps -> pTrue
| ps -> pOr ps)
| _ -> pred
(**************************************************************************)
(*************************** Substitutions ********************************)
(**************************************************************************)
module Subst = struct
type t = expr Symbol.SMap.t
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
s
else
match e with
| Var x', _ when x = x' -> s
| _ -> Symbol.SMap.add x e s
let empty = Symbol.SMap.empty
let is_empty = Symbol.SMap.is_empty
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 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 *)
end
(**************************************************************************)
(******************* Horn Clauses: Parsing ARMC files *********************)
(**************************************************************************)
module Horn = struct
type pr = string * string list
type gd = C of pred | K of pr
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
| C p -> Predicate.print ppf p
| K x -> print_pr ppf x
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 = fun (hd, gds) -> (support_pr hd) ++ (Misc.flap support_gd gds)
end
(* API *)
let simplify_pred = remove_bot <+> simplify_pred
let esub_su su e = match e with
| ((Var y), _) -> Misc.maybe_default (Subst.apply su y) e
| _ -> e
(* ORIG
let substs_pred = fun p su -> su |> Subst.to_list |> Predicate.substs p |> simplify_pred
*)
let substs_pred p su = Predicate.map id (esub_su su) p
let substs_expr e su = Expression.map id (esub_su su) e
(****************************************************************************)
(******************** Unification of Predicates *****************************)
(****************************************************************************)
exception DoesNotUnify
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
let e1', e2' = Misc.map_pair ((Misc.flip Expression.substs) s1) (e1', e2') in
let s2 = eUnify (e1', e2') in
s1 ++ s2
| (Bexp e1, _), (Bexp e2, _) ->
eUnify (e1, e2)
| (Not p1, _), (Not p2, _) ->
pUnify (p1, p2)
| (Imp (p1, p1'), _), (Imp (p2, p2'), _) ->
psUnify ([p1; p1'], [p2; p2'])
| (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"
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)
|> Misc.map_pair (fun p -> Predicate.substs p s)
|> pUnify
|> (fun s' -> s' ++ s)
end [] p1s p2s
and eUnify = function
| (Con c1, _), (Con c2, _) when c1 = c2 ->
[]
| (Var x1, _), (Var x2, _) when x1 = x2 ->
[]
| (Bin (e1, op1, e1'),_), (Bin (e2, op2, e2'), _) when op1 = op2 ->
esUnify ([e1; e1'], [e2; e2'])
| (Ite (p1, e1, e1'),_), (Ite (p2, e2, e2'), _) ->
let s = pUnify (p1, p2) in
let [e1; e1'; e2; e2'] = List.map ((Misc.flip Expression.substs) s) [e1; e1'; e2; e2'] in
esUnify ([e1; e1'], [e2; e2'])
| (Cst (e1, t1),_), (Cst (e2, t2),_) when t1 = t2 ->
eUnify (e1, e2)
| (App (uf1, e1s), _), (App (uf2, e2s),_) when uf1 = uf2 ->
esUnify (e1s, e2s)
| e, (Var x, _) | (Var x, _), e when Symbol.is_wild x ->
[(x, e)]
| _, _ -> 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)
|> 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 into_of_expr = function Con (Constant.Int i), _ -> Some i | _ -> None
let symm_pred = function
| Atom (e1, r, e2), _ -> pAtom (e2, symm_brel r, e1)
| p -> p
(* {{{
let rec expr_subst hp he e x e' =
let rec esub e =
try ExprHash.find he e with Not_found -> begin
let rv =
match euw e with
| Var y when x = y ->
e'
| Con _ | Var _ ->
e
| App (s, es) ->
App (s, List.map esub es) |> ewr
| Bin (e1, op, e2) ->
Bin (esub e1, op, esub e2) |> ewr
| Ite (ip, te, ee) ->
Ite (pred_subst hp he ip x e', esub te, esub ee) |> ewr
| Fld (s, e1) ->
Fld (s, esub e1) |> ewr in
let _ = ExprHash.add he e rv in
rv
end in esub e
and pred_subst hp he e x e' =
let rec s e =
try PredHash.find h e with
Not_found -> (let foo = s1 e in PredHash.add h e foo; foo)
and s1 e =
match puw e with
True -> e
| False -> e
| And plist -> pwr (And(List.map s plist))
| Or plist -> pwr (Or(List.map s plist))
| Not p -> pwr (Not(s p))
| Implies (p1, p2) -> pwr (Implies (s p1, s p2))
| Equality (x,y) -> pwr (Equality(expr_subst h he x v vv,expr_subst h he y v vv))
| 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
let eh = Expression.Hash.create 251 in
let sh = Hashtbl.create 251 in
let res = ref [] in
let add s = if not(Hashtbl.mem sh s) then Hashtbl.add sh s (); res := s :: !res in
let se exp =
let rec s exp =
try Expression.Hash.find eh exp with
Not_found -> Expression.Hash.add eh exp (); s1 exp
and s1 exp =
match euw exp with
Constant(_) -> ()
| 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
and s1 pred =
match puw pred with
True -> ()
| False -> ()
| And plist -> List.iter s plist
| Or plist -> List.iter s plist
| Not p -> s p
| Implies (p1, p2) -> s p1; s p2
| Equality (x,y) -> se x; se y
| 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 ->
List.iter ip plist
| Not p | Forall (_,p) ->
ip p
| Imp (p1, p2) ->
ip p1; ip p2
| _ -> ()
end in
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
let hp = Hash.create 251 in
let rec te e =
try Expression.Hash.find he e
with Not_found -> (let foo = te1 e in Expression.Hash.add he e foo; foo)
and te1 e =
match euw e with
Constant(c) -> e
| Application (func, args) ->
ewr (Application (func, List.map te args))
| Variable(v) -> ewr (Variable(v))
| Sum(args) -> ewr (Sum(List.map te args))
| Coeff(c,t) -> ewr (Coeff(c,te t))
| Ite(si,st,se) ->
let temp = ewr (Variable(new_temp())) in
let i = tp si in
let tv = te st and ev = te se in
begin
cnsts := pwr (Or [pwr (Not i); pwr (Equality(temp,(tv)))]) :: (!cnsts);
cnsts := pwr (Or [i; pwr (Equality(temp,(ev)))]) :: (!cnsts);
temp
end
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 =
match puw p with
True -> p
| False -> p
| And plist -> pwr (And (List.map tp plist))
| Or plist -> pwr (Or (List.map tp plist))
| Not p -> pwr (Not (tp p))
| Implies (p1, p2) -> pwr (Implies((tp p1),(tp p2)))
| Equality (x,y) -> pwr(Equality((te x),(te y)))
| Leq (x,y) -> pwr(Leq((te x),(te y)))
| Atom (s) -> p
in
let foo = tp sp in
pwr (And(foo :: !cnsts))
}}} *)