Commit f6cd3dce authored by Leon Gondelman's avatar Leon Gondelman

adding new bench examples for coercions and adapting some examples for new_system

parent 07e25011
......@@ -9,5 +9,3 @@ meta coercion function f
function h c : a
meta coercion function h
type t 'a
function f (t int) : int
meta coercion function f
goal G: forall x: t bool. x = 42
type t 'a
function f int : t int
meta coercion function f
goal G: forall x: t bool. 42 = x
type t1 'a
type t2 'a
type t3 'a
function t2_of_t1 (t1 'a) : t2 ('a,'a)
meta coercion function t2_of_t1
function bool_of_int bool : int
meta coercion function bool_of_int
function h (x: t1 'a) (b: int) : t1 int
goal G: forall x: t1 (int,int), y: t2 int. h x true = y
type t
function f t : int
meta coercion function f
goal G: forall x: t. 42 = x
module Simple
type a
type b
type c
type t
function b_to_c b : c
meta coercion function b_to_c
function a_to_b a : b
meta coercion function a_to_b
function f t : int
meta coercion function f
predicate is_c c
goal G2: forall x: a. is_c x
goal G: forall x: t. x = 42
function is_zero int : bool
meta coercion function is_zero
end
goal G3: if 42 then 1=2 else 3=4
module SameOne
use import Simple
end
module Same
use import Simple
use import SameOne
goal G: forall x: t. x = 42
end
module SimplePolymorphic
type t 'a
function f (t 'a) : int
meta coercion function f
goal G: forall x: t (bool,bool). x = 42
end
module Transitivity
type a
type b
type c
function b_to_c b : c
meta coercion function b_to_c
function a_to_b a : b
meta coercion function a_to_b
predicate is_c c
goal G2: forall x: a. is_c x
end
module SameTransitivity
use import Transitivity
end
module SameTransitivityCheck
use import Transitivity
use import SameTransitivity
goal G2: forall x: a. is_c x
end
module CoercionIf
function is_zero int : bool
meta coercion function is_zero
goal G3: if 42 then 1=2 else 3=4
end
module TrickyPolymorphicAlpha
use import list.List
type t 'a
type t1 'a
type t2 'a
function f (t 'a) : t1 (list 'a)
meta coercion function f
function g (t1 'a) : t2 (list 'a)
meta coercion function g
goal a : forall x:t int, y:t2 (list (list int)). x = y
end
module TrickyPolymorphicBeta
use import list.List
type t 'a
type t1 'a
type t2 'a
function f (t 'a) : t1 (list 'b)
meta coercion function f
function g (t1 'a) : t2 (list 'a)
meta coercion function g
goal a : forall x:t int, y:t2 (list (list int)). x = y
end
module InTypeArgs
type t1 'a
type t2 'a
type t3 'a
function t2_of_t1 (t1 'a) : t2 'a
meta coercion function t2_of_t1
function bool_of_int bool : int
meta coercion function bool_of_int
function h (x: t1 'a) (b: int) : t1 int
goal G: forall x: t1 'a, y: t2 int. h x true = y
end
\ No newline at end of file
......@@ -12,7 +12,7 @@ module Heap
use import int.Int
type elt
predicate le elt elt
val predicate le elt elt
clone relations.TotalPreOrder with type t = elt, predicate rel = le
......@@ -161,7 +161,7 @@ module PairingHeap
use import list.List
use import list.Length
predicate le elt elt
val predicate le elt elt
clone import relations.TotalPreOrder with type t = elt, predicate rel = le
(* [e] is no greater than the root of [h], if any *)
......@@ -245,7 +245,7 @@ module PairingHeap
let is_empty (h: heap) : bool
ensures { result <-> size h = 0 }
= h = E
= match h with E -> true | _ -> false end
let merge (h1 h2: heap) : heap
requires { inv h1 && inv h2 }
......
......@@ -12,7 +12,7 @@ module Heap
use import int.Int
type elt
predicate le elt elt
val predicate le elt elt
clone relations.TotalPreOrder with type t = elt, predicate rel = le
......@@ -79,7 +79,7 @@ module Size
use import bintree.Tree
use import bintree.Size as T
function size (h: heap) : int = match h with
let function size (h: heap) : int = match h with
| E -> 0
| T _ r -> 1 + T.size r
end
......@@ -130,7 +130,7 @@ module PairingHeap
use import Size
use import Occ
predicate le elt elt
val predicate le elt elt
clone import relations.TotalPreOrder with type t = elt, predicate rel = le
predicate le_root (e: elt) (h: heap) = match h with
......@@ -195,7 +195,7 @@ module PairingHeap
let is_empty (h: heap) : bool
ensures { result <-> size h = 0 }
= h = E
= match h with E -> true | _ -> false end
let size (h: heap) : int
ensures { result = size h }
......
......@@ -255,8 +255,9 @@ module OptimalNumberOfRegisters
ensures { 2 <= result }
(** the minimal number of registers needed to evaluate e *)
let rec function n (e: expr) : int =
match e with
let rec function n (e: expr) : int
variant { e }
= match e with
| Evar _ -> 1
| Eneg e -> n e
| Eadd e1 e2 -> let n1 = n e1 in let n2 = n e2 in
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment