Skip to content

Commit 5e9a12f

Browse files
ajreynolajreynol
committed
More
1 parent 936dc85 commit 5e9a12f

7 files changed

Lines changed: 45 additions & 32 deletions

File tree

‎tests/Arith-theory.eo‎

Lines changed: 29 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -35,39 +35,51 @@
3535
)
3636

3737
; Must use integer nil terminators to avoid confusion with subtyping
38-
(declare-parameterized-const + ((T Type :implicit) (U Type :implicit)) (-> T U (arith_typeunion_nary T U)) :right-assoc-nil 0)
39-
(declare-parameterized-const - ((T Type :implicit) (U Type :implicit)) (-> T U (arith_typeunion T U)) :left-assoc)
40-
(declare-parameterized-const * ((T Type :implicit) (U Type :implicit)) (-> T U (arith_typeunion_nary T U)) :right-assoc-nil 1)
38+
(declare-parameterized-const + ((T Type :implicit) (U Type :implicit))
39+
(-> T U (arith_typeunion_nary T U)) :right-assoc-nil 0)
40+
(declare-parameterized-const - ((T Type :implicit) (U Type :implicit))
41+
(-> T U (arith_typeunion T U)) :left-assoc)
42+
(declare-parameterized-const * ((T Type :implicit) (U Type :implicit))
43+
(-> T U (arith_typeunion_nary T U)) :right-assoc-nil 1)
4144

42-
(declare-parameterized-const < ((T Type :implicit) (U Type :implicit)) (-> (! T :requires ((is_arith_type T) true))
45+
(declare-parameterized-const < ((T Type :implicit) (U Type :implicit)) (->
46+
(! T :requires ((is_arith_type T) true))
4347
(! U :requires ((is_arith_type U) true))
4448
Bool)
4549
:chainable and)
46-
(declare-parameterized-const <= ((T Type :implicit) (U Type :implicit)) (-> (! T :requires ((is_arith_type T) true))
50+
(declare-parameterized-const <= ((T Type :implicit) (U Type :implicit)) (->
51+
(! T :requires ((is_arith_type T) true))
4752
(! U :requires ((is_arith_type U) true))
4853
Bool)
4954
:chainable and)
50-
(declare-parameterized-const > ((T Type :implicit) (U Type :implicit)) (-> (! T :requires ((is_arith_type T) true))
51-
(! U :requires ((is_arith_type U) true))
52-
Bool)
53-
:chainable and)
54-
(declare-parameterized-const >= ((T Type :implicit) (U Type :implicit)) (-> (! T :requires ((is_arith_type T) true))
55+
(declare-parameterized-const > ((T Type :implicit) (U Type :implicit)) (->
56+
(! T :requires ((is_arith_type T) true))
57+
(! U :requires ((is_arith_type U) true))
58+
Bool)
59+
:chainable and)
60+
(declare-parameterized-const >= ((T Type :implicit) (U Type :implicit)) (->
61+
(! T :requires ((is_arith_type T) true))
5562
(! U :requires ((is_arith_type U) true))
5663
Bool)
5764
:chainable and)
5865

59-
(declare-parameterized-const to_real ((T Type :implicit)) (-> (! T :requires ((is_arith_type T) true))
66+
(declare-parameterized-const to_real ((T Type :implicit)) (->
67+
(! T :requires ((is_arith_type T) true))
6068
Real))
61-
(declare-parameterized-const to_int ((T Type :implicit)) (-> (! T :requires ((is_arith_type T) true))
69+
(declare-parameterized-const to_int ((T Type :implicit)) (->
70+
(! T :requires ((is_arith_type T) true))
6271
Int))
63-
(declare-parameterized-const is_int ((T Type :implicit)) (-> (! T :requires ((is_arith_type T) true))
72+
(declare-parameterized-const is_int ((T Type :implicit)) (->
73+
(! T :requires ((is_arith_type T) true))
6474
Bool))
65-
(declare-parameterized-const abs ((T Type :implicit)) (-> (! T :requires ((is_arith_type T) true))
75+
(declare-parameterized-const abs ((T Type :implicit)) (->
76+
(! T :requires ((is_arith_type T) true))
6677
T))
6778

6879
; power
69-
(declare-parameterized-const ^ ((T Type :implicit) (U Type :implicit)) (-> T U (arith_typeunion T U)))
80+
(declare-parameterized-const ^ ((T Type :implicit) (U Type :implicit))
81+
(-> T U (arith_typeunion T U)))
7082

7183
; currently unary negation cannot use overload
72-
(declare-parameterized-const u- ((T Type :implicit)) (-> (! T :requires ((is_arith_type T) true))
73-
T))
84+
(declare-parameterized-const u- ((T Type :implicit))
85+
(-> (! T :requires ((is_arith_type T) true)) T))

‎tests/bv-dep-type.eo‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,9 @@
22

33
(declare-type BitVec (Int))
44

5-
(declare-parameterized-const bvadd ((n Int)) (-> (BitVec n) (BitVec n)
5+
(declare-parameterized-const bvadd ((n Int)) (->
6+
(BitVec n)
7+
(BitVec n)
68
(BitVec n)))
79

810
(declare-const m Int)

‎tests/bv-eval.eo‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -37,8 +37,8 @@
3737
(BitVec (arith.eval (+ (- h l) 1))))))))
3838
)
3939

40-
(declare-parameterized-const bvconcat ((n Int :implicit) (m Int :implicit)) (-> (BitVec n) (BitVec m)
41-
(BitVec (arith.eval (+ n m)))))
40+
(declare-parameterized-const bvconcat ((n Int :implicit) (m Int :implicit))
41+
(-> (BitVec n) (BitVec m) (BitVec (arith.eval (+ n m)))))
4242

4343
(program bv.eval ((T Type) (U Type) (S Type) (a T) (b U) (z S) (h Int) (l Int))
4444
(S) S

‎tests/bv-extract.eo‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,8 @@
33
(declare-const BitVec (-> Int Type))
44

55

6-
(declare-parameterized-const extract ((n Int :implicit) (h Int) (l Int)) (-> (BitVec n) (!
7-
(BitVec (eo::add h (eo::add (eo::neg l) 1)))
8-
:requires ((eo::is_neg l) false)
9-
; TODO: more conditions
6+
(declare-parameterized-const extract ((n Int :implicit) (h Int) (l Int))
7+
(-> (BitVec n)
8+
(! (BitVec (eo::add h (eo::add (eo::neg l) 1))) :requires ((eo::is_neg l) false)
109
))
1110
)

‎tests/bv-type-strict.eo‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,8 +22,8 @@
2222

2323
(declare-parameterized-const BitVec ((w Int :requires ((run_evaluate (> w 0)) true))) Type)
2424

25-
(declare-parameterized-const bvadd ((n Int :implicit)) (-> (BitVec n) (BitVec n)
26-
(BitVec n)))
25+
(declare-parameterized-const bvadd ((n Int :implicit))
26+
(-> (BitVec n) (BitVec n) (BitVec n)))
2727

2828
(declare-const a (BitVec 4))
2929

‎tests/nested-requires.eo‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
(declare-type Int ())
22
(declare-consts <numeral> Int)
3-
(declare-parameterized-const C ((x Int) (y Int :requires ((eo::gt x y) true) :requires ((eo::gt x y) true)))
3+
(declare-parameterized-const C
4+
((x Int) (y Int :requires ((eo::gt x y) true) :requires ((eo::gt x y) true)))
45
Type)
56

67
(declare-const test (C 4 3))

‎tests/unstuck-eval-bv-example.eo‎

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -20,12 +20,11 @@
2020
(define @bv_empty () (eo::to_bin 0 0))
2121

2222
(declare-parameterized-const concat ((n Int :implicit) (m Int :implicit)) (-> (BitVec n) (BitVec m)
23-
(BitVec (eo::add n m))) :right-assoc-nil @bv_empty
24-
)
23+
(BitVec (eo::add n m))) :right-assoc-nil @bv_empty)
2524

26-
(declare-parameterized-const extract ((n Int :implicit) (h Int) (l Int)) (-> (BitVec n) (BitVec (eo::add h (eo::neg l) 1))
27-
)
28-
)
25+
(declare-parameterized-const extract ((n Int :implicit) (h Int) (l Int))
26+
(-> (BitVec n) (BitVec (eo::add h (eo::neg l) 1))))
27+
2928
(declare-rule bv-extract-concat-4 ((@n0 Int) (@n1 Int) (@n2 Int) (x1 (BitVec @n0)) (y1 (BitVec @n1)) (xs1 (BitVec @n2) :list) (i1 Int) (j1 Int))
3029
:premises ((= (< j1 (- (@bvsize (concat x1 xs1 y1)) (@bvsize x1))) true))
3130
:args (x1 y1 xs1 i1 j1)

0 commit comments

Comments
 (0)