@ -5,475 +5,11 @@
* LICENSE file in the root directory of this source tree .
* )
open Ses
let pp_boxed fs fmt =
Format . pp_open_box fs 2 ;
Format . kfprintf ( fun fs -> Format . pp_close_box fs () ) fs fmt
(*
* Terms
* )
(* * Variable terms, represented as a subtype of general terms *)
module rec Var : sig
include Var_intf . VAR with type t = private Trm . trm
val of_ : Trm . trm -> t
end = struct
module T = struct
type t = Trm . trm [ @@ deriving compare , equal , sexp ]
let invariant x =
let @ () = Invariant . invariant [ % here ] x [ % sexp_of : t ] in
match x with
| Var _ -> ()
| _ -> fail " non-var: %a " Sexp . pp_hum ( sexp_of_t x ) ()
let make ~ id ~ name = Trm . _Var id name | > check invariant
let id = function Trm . Var v -> v . id | x -> violates invariant x
let name = function Trm . Var v -> v . name | x -> violates invariant x
end
include Var0 . Make ( T )
let of_ v = v | > check T . invariant
end
and Arith0 :
( Arithmetic . REPRESENTATION
with type var := Var . t
with type trm := Trm . trm ) =
Arithmetic . Representation ( Trm )
and Arith :
( Arithmetic . S
with type var := Var . t
with type trm := Trm . trm
with type t = Arith0 . t ) = struct
include Arith0
include Make ( struct
let get_arith ( e : Trm . trm ) =
match e with
| Z z -> Some ( Arith . const ( Q . of_z z ) )
| Q q -> Some ( Arith . const q )
| Arith a -> Some a
| _ -> None
end )
end
(* * Terms, built from variables and applications of function symbols from
various theories . Denote functions from structures to values . * )
and Trm : sig
type var = Var . t
type trm = private
(* variables *)
| Var of { id : int ; name : string }
(* arithmetic *)
| Z of Z . t
| Q of Q . t
| Arith of Arith . t
(* sequences ( of flexible size ) *)
| Splat of trm
| Sized of { seq : trm ; siz : trm }
| Extract of { seq : trm ; off : trm ; len : trm }
| Concat of trm array
(* records ( with fixed indices ) *)
| Select of { idx : int ; rcd : trm }
| Update of { idx : int ; rcd : trm ; elt : trm }
| Record of trm array
| Ancestor of int
(* uninterpreted *)
| Apply of Funsym . t * trm array
[ @@ deriving compare , equal , sexp ]
val ppx : Var . t Var . strength -> trm pp
val _ Var : int -> string -> trm
val _ Z : Z . t -> trm
val _ Q : Q . t -> trm
val _ Arith : Arith . t -> trm
val _ Splat : trm -> trm
val _ Sized : trm -> trm -> trm
val _ Extract : trm -> trm -> trm -> trm
val _ Concat : trm array -> trm
val _ Select : int -> trm -> trm
val _ Update : int -> trm -> trm -> trm
val _ Record : trm array -> trm
val _ Ancestor : int -> trm
val _ Apply : Funsym . t -> trm array -> trm
val add : trm -> trm -> trm
val sub : trm -> trm -> trm
val seq_size_exn : trm -> trm
val vars : trm -> Var . t iter
end = struct
type var = Var . t
type trm =
| Var of { id : int ; name : string }
| Z of Z . t
| Q of Q . t
| Arith of Arith . t
| Splat of trm
| Sized of { seq : trm ; siz : trm }
| Extract of { seq : trm ; off : trm ; len : trm }
| Concat of trm array
| Select of { idx : int ; rcd : trm }
| Update of { idx : int ; rcd : trm ; elt : trm }
| Record of trm array
| Ancestor of int
| Apply of Funsym . t * trm array
[ @@ deriving compare , equal , sexp ]
let compare_trm x y =
if x = = y then 0
else
match ( x , y ) with
| Var { id = i ; name = _ } , Var { id = j ; name = _ } when i > 0 && j > 0 ->
Int . compare i j
| _ -> compare_trm x y
let equal_trm x y =
x = = y
| |
match ( x , y ) with
| Var { id = i ; name = _ } , Var { id = j ; name = _ } when i > 0 && j > 0 ->
Int . equal i j
| _ -> equal_trm x y
let rec ppx strength fs trm =
let rec pp fs trm =
let pf fmt = pp_boxed fs fmt in
match trm with
| Var _ as v -> Var . ppx strength fs ( Var . of_ v )
| Z z -> Trace . pp_styled ` Magenta " %a " fs Z . pp z
| Q q -> Trace . pp_styled ` Magenta " %a " fs Q . pp q
| Arith a -> Arith . ppx strength fs a
| Splat x -> pf " %a^ " pp x
| Sized { seq ; siz } -> pf " @<1>⟨%a,%a@<1>⟩ " pp siz pp seq
| Extract { seq ; off ; len } -> pf " %a[%a,%a) " pp seq pp off pp len
| Concat [| |] -> pf " @<2>⟨⟩ "
| Concat xs -> pf " (%a) " ( Array . pp " @,^ " pp ) xs
| Select { idx ; rcd } -> pf " %a[%i] " pp rcd idx
| Update { idx ; rcd ; elt } ->
pf " [%a@ @[| %i → %a@]] " pp rcd idx pp elt
| Record xs -> pf " {%a} " ( ppx_record strength ) xs
| Ancestor i -> pf " (ancestor %i) " i
| Apply ( f , [| |] ) -> pf " %a " Funsym . pp f
| Apply
( ( ( Rem | BitAnd | BitOr | BitXor | BitShl | BitLshr | BitAshr )
as f )
, [| x ; y |] ) ->
pf " (%a@ %a@ %a) " pp x Funsym . pp f pp y
| Apply ( f , es ) ->
pf " %a(%a) " Funsym . pp f ( Array . pp " ,@ " ( ppx strength ) ) es
in
pp fs trm
and ppx_record strength fs elts =
[ % Trace . fprintf
fs " %a "
( fun fs elts ->
let exception Not_a_string in
match
String . init ( Array . length elts ) ~ f : ( fun i ->
match elts . ( i ) with
| Z c -> Char . of_int_exn ( Z . to_int c )
| _ -> raise Not_a_string )
with
| s -> Format . fprintf fs " %S " s
| exception ( Not_a_string | Z . Overflow | Failure _ ) ->
Format . fprintf fs " @[<h>%a@] "
( Array . pp " ,@ " ( ppx strength ) )
elts )
elts ]
let pp = ppx ( fun _ -> None )
let invariant e =
let @ () = Invariant . invariant [ % here ] e [ % sexp_of : trm ] in
match e with
| Q q -> assert ( not ( Z . equal Z . one ( Q . den q ) ) )
| Arith a -> (
match Arith . classify a with
| Compound -> ()
| Trm _ | Const _ -> assert false )
| _ -> ()
(* destructors *)
let get_z = function Z z -> Some z | _ -> None
let get_q = function Q q -> Some q | Z z -> Some ( Q . of_z z ) | _ -> None
(* constructors *)
let _ Var id name = Var { id ; name } | > check invariant
(* statically allocated since they are tested with == *)
let zero = Z Z . zero | > check invariant
let one = Z Z . one | > check invariant
let _ Z z =
( if Z . equal Z . zero z then zero else if Z . equal Z . one z then one else Z z )
| > check invariant
let _ Q q =
( if Z . equal Z . one ( Q . den q ) then _ Z ( Q . num q ) else Q q )
| > check invariant
let _ Arith a =
( match Arith . classify a with
| Trm e -> e
| Const q -> _ Q q
| Compound -> Arith a )
| > check invariant
let add x y = _ Arith Arith . ( add ( trm x ) ( trm y ) )
let sub x y = _ Arith Arith . ( sub ( trm x ) ( trm y ) )
let _ Splat x = Splat x | > check invariant
let seq_size_exn =
let invalid = Invalid_argument " seq_size_exn " in
let rec seq_size_exn = function
| Sized { siz = n } | Extract { len = n } -> n
| Concat a0U ->
Array . fold ~ f : ( fun aJ a0I -> add a0I ( seq_size_exn aJ ) ) a0U zero
| _ -> raise invalid
in
seq_size_exn
let seq_size e =
try Some ( seq_size_exn e ) with Invalid_argument _ -> None
let _ Sized seq siz =
( match seq_size seq with
(* ⟨n,α⟩ ==> α α *)
| Some n when equal_trm siz n -> seq
| _ -> Sized { seq ; siz } )
| > check invariant
let partial_compare x y =
match sub x y with
| Z z -> Some ( Int . sign ( Z . sign z ) )
| Q q -> Some ( Int . sign ( Q . sign q ) )
| _ -> None
let partial_ge x y =
match partial_compare x y with Some ( Pos | Zero ) -> true | _ -> false
let empty_seq = Concat [| |]
let rec _ Extract seq off len =
[ % trace ]
~ call : ( fun { pf } -> pf " %a " pp ( Extract { seq ; off ; len } ) )
~ retn : ( fun { pf } -> pf " %a " pp )
@@ fun () ->
(* _[_,0 ) ==> ⟨⟩ *)
( if equal_trm len zero then empty_seq
else
let o_l = add off len in
match seq with
(* α ) [o,l ) ==> α ) when k ≥ o+l *)
| Extract { seq = a ; off = m ; len = k } when partial_ge k o_l ->
_ Extract a ( add m off ) len
(* ⟨n,E^⟩[o,l ) ==> ⟨l,E^⟩ when n ≥ o+l *)
| Sized { siz = n ; seq = Splat _ as e } when partial_ge n o_l ->
_ Sized e len
(* ⟨n,a⟩[0,n ) ==> ⟨n,a⟩ *)
| Sized { siz = n } when equal_trm off zero && equal_trm n len -> seq
(* For ( α₀^α₁ ) [o,l ) there are 3 cases:
*
* ⟨ .. . ⟩ ^ ⟨ .. . ⟩
* [ , )
* o < o + l ≤ | α ₀ | : ( α ₀ ^ α ₁ ) [ o , l ) = = > α ₀ [ o , l ) ^ α ₁ [ 0 , 0 )
*
* ⟨ .. . ⟩ ^ ⟨ .. . ⟩
* [ , )
* o ≤ | α ₀ | < o + l : ( α ₀ ^ α ₁ ) [ o , l ) = = > α ₀ [ o , | α ₀ | - o ) ^ α ₁ [ 0 , l - ( | α ₀ | - o ) )
*
* ⟨ .. . ⟩ ^ ⟨ .. . ⟩
* [ , )
* | α ₀ | ≤ o : ( α ₀ ^ α ₁ ) [ o , l ) = = > α ₀ [ o , 0 ) ^ α ₁ [ o - | α ₀ | , l )
*
* So in general :
*
* ( α ₀ ^ α ₁ ) [ o , l ) = = > α ₀ [ o , l ₀ ) ^ α ₁ [ o ₁ , l - l ₀ )
* where l ₀ = max 0 ( min l | α ₀ | - o )
* o ₁ = max 0 o - | α ₀ |
* )
| Concat na1N -> (
match len with
| Z l ->
Array . fold_map_until na1N ( l , off )
~ f : ( fun naI ( l , oI ) ->
if Z . equal Z . zero l then
` Continue ( _ Extract naI oI zero , ( l , oI ) )
else
let nI = seq_size_exn naI in
let oI_nI = sub oI nI in
match oI_nI with
| Z z ->
let oJ = if Z . sign z < = 0 then zero else oI_nI in
let lI = Z . ( max zero ( min l ( neg z ) ) ) in
let l = Z . ( l - lI ) in
` Continue ( _ Extract naI oI ( _ Z lI ) , ( l , oJ ) )
| _ -> ` Stop ( Extract { seq ; off ; len } ) )
~ finish : ( fun ( e1N , _ ) -> _ Concat e1N )
| _ -> Extract { seq ; off ; len } )
(* α ) *)
| _ -> Extract { seq ; off ; len } )
| > check invariant
and _ Concat xs =
[ % trace ]
~ call : ( fun { pf } -> pf " %a " pp ( Concat xs ) )
~ retn : ( fun { pf } -> pf " %a " pp )
@@ fun () ->
(* ( α ( β^γ ) ^δ ) ==> ( α γ ) *)
let flatten xs =
if Array . exists ~ f : ( function Concat _ -> true | _ -> false ) xs then
Array . flat_map ~ f : ( function Concat s -> s | e -> [| e |] ) xs
else xs
in
let simp_adjacent e f =
match ( e , f ) with
(* ⟨n,a⟩[o,k ) ^⟨n,a⟩[o+k,l ) ==> ⟨n,a⟩[o,k+l ) when n ≥ o+k+l *)
| ( Extract { seq = Sized { siz = n } as na ; off = o ; len = k }
, Extract { seq = na' ; off = o_k ; len = l } )
when equal_trm na na'
&& equal_trm o_k ( add o k )
&& partial_ge n ( add o_k l ) ->
Some ( _ Extract na o ( add k l ) )
(* ⟨m,E^⟩^⟨n,E^⟩ ==> ⟨m+n,E^⟩ *)
| Sized { siz = m ; seq = Splat _ as a } , Sized { siz = n ; seq = a' }
when equal_trm a a' ->
Some ( _ Sized a ( add m n ) )
| _ -> None
in
let xs = flatten xs in
let xs = Array . reduce_adjacent ~ f : simp_adjacent xs in
( if Array . length xs = 1 then xs . ( 0 ) else Concat xs ) | > check invariant
let _ Select idx rcd = Select { idx ; rcd } | > check invariant
let _ Update idx rcd elt = Update { idx ; rcd ; elt } | > check invariant
let _ Record es = Record es | > check invariant
let _ Ancestor i = Ancestor i | > check invariant
let _ Apply f es =
( match
Funsym . eval ~ equal : equal_trm ~ get_z ~ ret_z : _ Z ~ get_q ~ ret_q : _ Q f es
with
| Some c -> c
| None -> Apply ( f , es ) )
| > check invariant
let rec iter_vars e ~ f =
match e with
| Var _ as v -> f ( Var . of_ v )
| Z _ | Q _ | Ancestor _ -> ()
| Splat x | Select { rcd = x } -> iter_vars ~ f x
| Sized { seq = x ; siz = y } | Update { rcd = x ; elt = y } ->
iter_vars ~ f x ;
iter_vars ~ f y
| Extract { seq = x ; off = y ; len = z } ->
iter_vars ~ f x ;
iter_vars ~ f y ;
iter_vars ~ f z
| Concat xs | Record xs | Apply ( _ , xs ) ->
Array . iter ~ f : ( iter_vars ~ f ) xs
| Arith a -> Iter . iter ~ f : ( iter_vars ~ f ) ( Arith . iter a )
let vars e = Iter . from_labelled_iter ( iter_vars e )
end
open Trm
let zero = _ Z Z . zero
let one = _ Z Z . one
(*
* Formulas
* )
module Prop = Propositional . Make ( Trm )
module Fml = struct
include Prop . Fml
let tt = mk_Tt ()
let ff = _ Not tt
let bool b = if b then tt else ff
let _ Eq0 = function
| Z z -> bool ( Z . equal Z . zero z )
| Q q -> bool ( Q . equal Q . zero q )
| x -> _ Eq0 x
let _ Pos = function
| Z z -> bool ( Z . gt z Z . zero )
| Q q -> bool ( Q . gt q Q . zero )
| x -> _ Pos x
let _ Eq x y =
if x = = zero then _ Eq0 y
else if y = = zero then _ Eq0 x
else
let sort_eq x y =
match Sign . of_int ( compare_trm x y ) with
| Neg -> _ Eq x y
| Zero -> tt
| Pos -> _ Eq y x
in
match ( x , y ) with
(* x = y ==> 0 = x - y when x = y is an arithmetic equality *)
| ( Z _ | Q _ | Arith _ ) , _ | _ , ( Z _ | Q _ | Arith _ ) ->
_ Eq0 ( sub x y )
(* α α γ γ *)
| Concat a , Concat b ->
let m = Array . length a in
let n = Array . length b in
let l = min m n in
let length_common_prefix =
let rec find_lcp i =
if i < l && equal_trm a . ( i ) b . ( i ) then find_lcp ( i + 1 ) else i
in
find_lcp 0
in
if length_common_prefix = l then tt
else
let length_common_suffix =
let rec find_lcs i =
if equal_trm a . ( m - 1 - i ) b . ( n - 1 - i ) then
find_lcs ( i + 1 )
else i
in
find_lcs 0
in
let length_common =
length_common_prefix + length_common_suffix
in
if length_common = 0 then sort_eq x y
else
let pos = length_common_prefix in
let a = Array . sub ~ pos ~ len : ( m - length_common ) a in
let b = Array . sub ~ pos ~ len : ( n - length_common ) b in
_ Eq ( _ Concat a ) ( _ Concat b )
| ( Sized _ | Extract _ | Concat _ ) , ( Sized _ | Extract _ | Concat _ )
->
sort_eq x y
(* x = α α α *)
| x , ( ( Sized _ | Extract _ | Concat _ ) as a )
| ( ( Sized _ | Extract _ | Concat _ ) as a ) , x ->
_ Eq ( _ Sized x ( seq_size_exn a ) ) a
| _ -> sort_eq x y
let vars p = Iter . flat_map ~ f : Trm . vars ( trms p )
end
module Fmls = Prop . Fmls
open Fml
type var = Var . t
(*
* Conditional terms
* )
@ -498,6 +34,10 @@ type exp = [cnd | `Fml of fml] [@@deriving compare, equal, sexp]
(* * pp *)
let pp_boxed fs fmt =
Format . pp_open_box fs 2 ;
Format . kfprintf ( fun fs -> Format . pp_close_box fs () ) fs fmt
let ppx_f strength fs fml =
let pp_t = Trm . ppx strength in
let rec pp fs fml =
@ -529,7 +69,7 @@ let ppx_f strength fs fml =
| Iff ( x , y ) -> pf " (%a@ <=> %a) " pp x pp y
| Cond { cnd ; pos ; neg } ->
pf " @[<hv 1>(%a@ ? %a@ : %a)@] " pp cnd pp pos pp neg
| Lit ( p , xs ) -> pf " %a(%a) " . pp p ( Array . pp " ,@ " pp_t ) xs
| Lit ( p , xs ) -> pf " %a(%a) " Ses. Predsym. pp p ( Array . pp " ,@ " pp_t ) xs
in
pp fs fml
Josh Berdine
4 years ago
committed by
Facebook GitHub Bot