@ -7,45 +7,20 @@
(* * Terms *)
(* * Representation of Arithmetic terms *)
module rec Arith0 :
( Arithmetic . REPRESENTATION
with type var := Trm . Var1 . t
with type trm := Trm . t ) =
Arithmetic . Representation
( Trm . Var1 )
( struct
include Trm
include Comparer . Make ( Trm )
end )
(* * Arithmetic terms *)
and Arith : ( Arithmetic . S with type trm := Trm . t with type t = Arith0 . t ) =
struct
include Arith0
include Make ( struct
let to_trm = Trm . _Arith
(* Define term type using polymorphic arithmetic type, with derived compare,
equal , and sexp_of functions * )
module Trm1 = struct
type compare [ @@ deriving compare , equal , sexp ]
let get_arith ( e : Trm . t ) =
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
type arith = ( t , compare ) Arithmetic . t
(* * Terms, built from variables and applications of function symbols from
various theories . Denote functions from structures to values . * )
and Trm : sig
type t = private
and t =
(* variables *)
| Var of { id : int ; name : string }
| Var of { id : int ; name : string [ @ ignore ] }
(* arithmetic *)
| Z of Z . t
| Q of Q . t
| Arith of Arith . t
| Arith of arith
(* sequences ( of flexible size ) *)
| Splat of t
| Sized of { seq : t ; siz : t }
@ -54,50 +29,20 @@ and Trm : sig
(* uninterpreted *)
| Apply of Funsym . t * t array
[ @@ deriving compare , equal , sexp ]
end
(* * Variable terms, represented as a subtype of general terms *)
module Var1 : sig
type trm := t
include Var_intf . S with type t = private trm
val of_ : trm -> t
val of_trm : trm -> t option
(* Add comparer, needed to instantiate arithmetic and containers *)
module Trm2 = struct
include Comparer . Counterfeit ( Trm1 )
include Trm1
end
val ppx : Var1 . strength -> t pp
val pp : t pp
include Invariant . S with type t := t
val _ Var : int -> string -> t
val _ Z : Z . t -> t
val _ Q : Q . t -> t
val _ Arith : Arith . t -> t
val _ Splat : t -> t
val _ Sized : seq : t -> siz : t -> t
val _ Extract : seq : t -> off : t -> len : t -> t
val _ Concat : t array -> t
val _ Apply : Funsym . t -> t array -> t
val add : t -> t -> t
val sub : t -> t -> t
val seq_size_exn : t -> t
val seq_size : t -> t option
val get_z : t -> Z . t option
val get_q : t -> Q . t option
val vars : t -> Var1 . t iter
end = struct
type t =
| Var of { id : int ; name : string [ @ ignore ] }
| Z of Z . t
| Q of Q . t
| Arith of Arith . t
| Splat of t
| Sized of { seq : t ; siz : t }
| Extract of { seq : t ; off : t ; len : t }
| Concat of t array
| Apply of Funsym . t * t array
[ @@ deriving compare , equal , sexp ]
(* Specialize arithmetic type and define operations using comparer *)
module Arith0 = Arithmetic . Make ( Trm2 )
(* Add ppx, defined recursively with Arith0.ppx *)
module Trm3 = struct
include Trm2
(* nul-terminated string value represented by a concatenation *)
let string_of_concat xs =
@ -136,7 +81,7 @@ end = struct
| Some ` Anonymous -> Trace . pp_styled ` Cyan " _ " fs )
| 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 ( ppx strength ) fs a
| Arith a -> Arith 0 . ppx ( 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
@ -157,19 +102,31 @@ end = struct
pp fs trm
let pp = ppx ( fun _ -> None )
let pp_diff fs ( x , y ) = Format . fprintf fs " -- %a ++ %a " pp x pp y
end
(* Define containers over terms *)
module Set = struct
include Set . Make ( Trm3 )
include Provide_of_sexp ( Trm3 )
include Provide_pp ( Trm3 )
end
module Map = struct
include Map . Make ( Trm3 )
include Provide_of_sexp ( Trm3 )
end
(* Define variables as a subtype of terms *)
module Var1 = struct
module Var = struct
open Trm3
module V = struct
module T = struct
type nonrec t = t [ @@ deriving compare , equal , sexp ]
type strength = t -> [ ` Universal | ` Existential | ` Anonymous ] option
let pp = pp
let ppx = ppx
end
include T
let invariant x =
let @ () = Invariant . invariant [ % here ] x [ % sexp_of : t ] in
@ -182,22 +139,16 @@ end = struct
let name = function Var v -> v . name | x -> violates invariant x
module Set = struct
module S = NS . Set . Make ( T )
include S
include Provide_of_sexp ( T )
include Provide_pp ( T )
include Set
let ppx strength vs = S . pp_full ( ppx strength ) vs
let ppx strength vs = pp_full ( ppx strength ) vs
let pp_xs fs xs =
if not ( is_empty xs ) then
Format . fprintf fs " @<2>∃ @[%a@] .@;<1 2> " pp xs
end
module Map = struct
include NS . Map . Make ( T )
include Provide_of_sexp ( T )
end
module Map = Map
let fresh name ~ wrt =
let max =
@ -221,24 +172,42 @@ end = struct
module Subst = Subst . Make ( V )
end
(* Add definitions needed for arithmetic embedding into terms *)
module Trm = struct
include Trm3
(* * Invariant *)
let invariant e =
let @ () = Invariant . invariant [ % here ] e [ % sexp_of : t ] in
match e with
| Q q -> assert ( not ( Z . equal Z . one ( Q . den q ) ) )
| Arith a -> (
match Arith . classify a with
match Arith 0 . classify a with
| Trm _ | Const _ -> assert false
| _ -> () )
| _ -> ()
(* * Destruct *)
(* * Traverse *)
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
let rec iter_vars e ~ f =
match e with
| Var _ as v -> f ( Var . of_ v )
| Z _ | Q _ -> ()
| Splat x -> iter_vars ~ f x
| Sized { seq = x ; siz = 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 | Apply ( _ , xs ) -> Array . iter ~ f : ( iter_vars ~ f ) xs
| Arith a -> Iter . iter ~ f : ( iter_vars ~ f ) ( Arith0 . trms a )
(* * Construct *)
let vars e = Iter . from_labelled_iter ( iter_vars e
let _ Var id name = Var { id ; name } | > check invariant
(* * Construct *)
(* statically allocated since they are tested with == *)
let zero = Z Z . zero | > check invariant
@ -253,16 +222,59 @@ end = struct
| > check invariant
let _ Arith a =
( match Arith . classify a with
( match Arith 0 . classify a with
| Trm e -> e
| Const q -> _ Q q
| _ -> Arith a )
| > check invariant
end
include Trm
(* Instantiate arithmetic with embedding into terms, yielding full
Arithmetic interface * )
module Arith =
Arith0 . Embed ( Var ) ( Trm )
( struct
let to_trm = _ Arith
let get_arith e =
match e with
| Z z -> Some ( Arith0 . const ( Q . of_z z ) )
| Q q -> Some ( Arith0 . const q )
| Arith a -> Some a
| _ -> None
end )
(* Full Trm definition, using full arithmetic interface *)
(* * Destruct *)
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
(* * Construct *)
(* variables *)
let var v = ( v : Var . t :> t )
(* arithmetic *)
let integer z = _ Z z
let rational q = _ Q q
let neg x = _ Arith Arith . ( neg ( trm x ) )
let add x y = _ Arith Arith . ( add ( trm x ) ( trm y ) )
let sub x y = _ Arith Arith . ( sub ( trm x ) ( trm y ) )
let mulq q x = _ Arith Arith . ( mulc q ( trm x ) )
let mul x y = _ Arith ( Arith . mul x y )
let div x y = _ Arith ( Arith . div x y )
let pow x i = _ Arith ( Arith . pow x i )
let arith = _ Arith
(* sequences *)
let _ Splat x =
let s x =
(* 0^ ==> 0 *)
( if x = = zero then x else Splat x ) | > check invariant
@ -276,10 +288,9 @@ end = struct
in
seq_size_exn
let seq_size e =
try Some ( seq_size_exn e ) with Invalid_argument _ -> None
let seq_size e = try Some ( seq_size_exn e ) with Invalid_argument _ -> None
let _ S ized ~ seq ~ siz =
let s ~ seq ~ siz =
( match seq_size seq with
(* ⟨n,α⟩ ==> α α *)
| Some n when equal siz n -> seq
@ -297,7 +308,7 @@ end = struct
let empty_seq = Concat [| |]
let rec _ E xtract ~ seq ~ off ~ len =
let rec e ~ seq ~ off ~ len =
[ % trace ]
~ call : ( fun { pf } -> pf " @ %a " pp ( Extract { seq ; off ; len } ) )
~ retn : ( fun { pf } -> pf " %a " pp )
@ -309,13 +320,13 @@ end = struct
match seq with
(* α ) [o,l ) ==> α ) when k ≥ o+l *)
| Extract { seq = a ; off = m ; len = k } when partial_ge k o_l ->
_ E xtract ~ seq : a ~ off : ( add m off ) ~ len
e ~ seq : a ~ off : ( add m off ) ~ len
(* ⟨n,0⟩[o,l ) ==> ⟨l,0⟩ when n ≥ o+l *)
| Sized { siz = n ; seq } when seq = = zero && partial_ge n o_l ->
_ S ized ~ seq ~ siz : len
s ~ seq ~ siz : len
(* ⟨n,E^⟩[o,l ) ==> ⟨l,E^⟩ when n ≥ o+l *)
| Sized { siz = n ; seq = Splat _ as e } when partial_ge n o_l ->
_ S ized ~ seq : e ~ siz : len
s ~ seq : e ~ siz : len
(* ⟨n,a⟩[0,n ) ==> ⟨n,a⟩ *)
| Sized { siz = n } when equal off zero && equal n len -> seq
(* For ( α₀^α₁ ) [o,l ) there are 3 cases:
@ -344,7 +355,7 @@ end = struct
Array . fold_map_until na1N ( l , off )
~ f : ( fun naI ( l , oI ) ->
if Z . equal Z . zero l then
` Continue ( _ E xtract ~ seq : naI ~ off : oI ~ len : zero , ( l , oI ) )
` Continue ( e ~ seq : naI ~ off : oI ~ len : zero , ( l , oI ) )
else
let nI = seq_size_exn naI in
let oI_nI = sub oI nI in
@ -354,15 +365,15 @@ end = struct
let lI = Z . ( max zero ( min l ( neg z ) ) ) in
let l = Z . ( l - lI ) in
` Continue
( _ E xtract ~ seq : naI ~ off : oI ~ len : ( _ Z lI ) , ( l , oJ ) )
( e ~ seq : naI ~ off : oI ~ len : ( _ Z lI ) , ( l , oJ ) )
| _ -> ` Stop ( Extract { seq ; off ; len } ) )
~ finish : ( fun ( e1N , _ ) -> _ C e1N )
~ finish : ( fun ( e1N , _ ) -> c e1N )
| _ -> Extract { seq ; off ; len } )
(* α ) *)
| _ -> Extract { seq ; off ; len } )
| > check invariant
and _ C oncat xs =
and c xs =
[ % trace ]
~ call : ( fun { pf } -> pf " @ %a " pp ( Concat xs ) )
~ retn : ( fun { pf } -> pf " %a " pp )
@ -380,22 +391,24 @@ end = struct
, Extract { seq = na' ; off = o_k ; len = l } )
when equal na na' && equal o_k ( add o k ) && partial_ge n ( add o_k l )
->
Some ( _ E xtract ~ seq : na ~ off : o ~ len : ( add k l ) )
Some ( e ~ seq : na ~ off : o ~ len : ( add k l ) )
(* ⟨m,0⟩^⟨n,0⟩ ==> ⟨m+n,0⟩ *)
| Sized { siz = m ; seq = a } , Sized { siz = n ; seq = a' }
when a = = zero && a' = = zero ->
Some ( _ S ized ~ seq : a ~ siz : ( add m n ) )
Some ( s ~ seq : a ~ siz : ( add m n ) )
(* ⟨m,E^⟩^⟨n,E^⟩ ==> ⟨m+n,E^⟩ *)
| Sized { siz = m ; seq = Splat _ as a } , Sized { siz = n ; seq = a' }
when equal a a' ->
Some ( _ S ized ~ seq : a ~ siz : ( add m n ) )
Some ( s ~ seq : a ~ siz : ( 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 _ Apply f es =
(* uninterpreted *)
let apply f es =
( match Funsym . eval ~ equal ~ get_z ~ ret_z : _ Z ~ get_q ~ ret_q : _ Q f es with
| Some c -> c
| None -> Apply ( f , es ) )
@ -403,81 +416,6 @@ end = struct
(* * Traverse *)
let rec iter_vars e ~ f =
match e with
| Var _ as v -> f ( Var1 . of_ v )
| Z _ | Q _ -> ()
| Splat x -> iter_vars ~ f x
| Sized { seq = x ; siz = 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 | Apply ( _ , xs ) -> Array . iter ~ f : ( iter_vars ~ f ) xs
| Arith a -> Iter . iter ~ f : ( iter_vars ~ f ) ( Arith . trms a )
let vars e = Iter . from_labelled_iter ( iter_vars e )
end
include Trm
module Var = Var1
module Set = struct
include Set . Make ( Trm )
include Provide_of_sexp ( Trm )
include Provide_pp ( Trm )
let of_vars : Var . Set . t -> t =
fun vs ->
of_iter
( Iter . map ~ f : ( fun v -> ( v : Var . t :> Trm . t ) ) ( Var . Set . to_iter vs ) )
end
module Map = struct
include Map . Make ( Trm )
include Provide_of_sexp ( Trm )
end
type arith = Arith . t
let pp_diff fs ( x , y ) = Format . fprintf fs " -- %a ++ %a " pp x pp y
(* * Construct *)
(* variables *)
let var v = ( v : Var . t :> t )
(* arithmetic *)
let zero = _ Z Z . zero
let one = _ Z Z . one
let integer z = _ Z z
let rational q = _ Q q
let neg x = _ Arith Arith . ( neg ( trm x ) )
let add = Trm . add
let sub = Trm . sub
let mulq q x = _ Arith Arith . ( mulc q ( trm x ) )
let mul x y = _ Arith ( Arith . mul x y )
let div x y = _ Arith ( Arith . div x y )
let pow x i = _ Arith ( Arith . pow x i )
let arith = _ Arith
(* sequences *)
let splat = _ Splat
let sized = _ Sized
let extract = _ Extract
let concat elts = _ Concat elts
(* uninterpreted *)
let apply sym args = _ Apply sym args
(* * Traverse *)
let trms = function
| Var _ | Z _ | Q _ -> Iter . empty
| Arith a -> Arith . trms a
@ -505,25 +443,25 @@ let rec map_vars e ~f =
| Var _ as v -> ( f ( Var . of_ v ) : Var . t :> t )
| Z _ | Q _ -> e
| Arith a -> map1 ( Arith . map ~ f : ( map_vars ~ f ) ) e _ Arith a
| Splat x -> map1 ( map_vars ~ f ) e _ S x
| Splat x -> map1 ( map_vars ~ f ) e s x
| Sized { seq ; siz } ->
map2 ( map_vars ~ f ) e ( fun seq siz -> _ S ~ seq ~ siz ) seq siz
map2 ( map_vars ~ f ) e ( fun seq siz -> s ~ seq ~ siz ) seq siz
| Extract { seq ; off ; len } ->
map3 ( map_vars ~ f ) e
( fun seq off len -> _ E ~ seq ~ off ~ len )
( fun seq off len -> e ~ seq ~ off ~ len )
seq off len
| Concat xs -> mapN ( map_vars ~ f ) e _ C xs
| Apply ( g , xs ) -> mapN ( map_vars ~ f ) e ( _ A g ) xs
| Concat xs -> mapN ( map_vars ~ f ) e c xs
| Apply ( g , xs ) -> mapN ( map_vars ~ f ) e ( a g ) xs
let map e ~ f =
match e with
| Var _ | Z _ | Q _ -> e
| Arith a -> map1 ( Arith . map ~ f ) e _ Arith a
| Splat x -> map1 f e _ S x
| Sized { seq ; siz } -> map2 f e ( fun seq siz -> _ S ~ seq ~ siz ) seq siz
| Splat x -> map1 f e s x
| Sized { seq ; siz } -> map2 f e ( fun seq siz -> s ~ seq ~ siz ) seq siz
| Extract { seq ; off ; len } ->
map3 f e ( fun seq off len -> _ E ~ seq ~ off ~ len ) seq off len
| Concat xs -> mapN f e _ C xs
| Apply ( g , xs ) -> mapN f e ( _ A g ) xs
map3 f e ( fun seq off len -> e ~ seq ~ off ~ len ) seq off len
| Concat xs -> mapN f e c xs
| Apply ( g , xs ) -> mapN f e ( a g ) xs
let fold_map e = fold_map_from_map map e
Josh Berdine
4 years ago
committed by
Facebook GitHub Bot