Skip to content

Commit 3b44350

Browse files
ajreynolajreynol
committed
Updates
1 parent 950bcfd commit 3b44350

10 files changed

Lines changed: 50 additions & 47 deletions

‎src/expr_parser.cpp‎

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1233,7 +1233,15 @@ void ExprParser::parseAttributeList(
12331233
}
12341234
break;
12351235
case Kind::NONE:
1236-
// nothing handled
1236+
handled = true;
1237+
switch (a)
1238+
{
1239+
case Attr::OPAQUE:
1240+
// requires no value
1241+
break;
1242+
case Attr::REQUIRES: val = parseExprPair(); break;
1243+
default: handled = false; break;
1244+
}
12371245
break;
12381246
default:
12391247
break;

‎tests/Arith-theory.eo‎

Lines changed: 26 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -39,35 +39,35 @@
3939
(declare-parameterized-const - ((T Type :implicit) (U Type :implicit)) (-> T U (arith_typeunion T U)) :left-assoc)
4040
(declare-parameterized-const * ((T Type :implicit) (U Type :implicit)) (-> T U (arith_typeunion_nary T U)) :right-assoc-nil 1)
4141

42-
(declare-parameterized-const < ((T Type :implicit) (U Type :implicit)
43-
(t T :requires ((is_arith_type T) true))
44-
(u U :requires ((is_arith_type U) true)))
45-
Bool :chainable and)
46-
(declare-parameterized-const <= ((T Type :implicit) (U Type :implicit)
47-
(t T :requires ((is_arith_type T) true))
48-
(u U :requires ((is_arith_type U) true)))
49-
Bool :chainable and)
50-
(declare-parameterized-const > ((T Type :implicit) (U Type :implicit)
51-
(t T :requires ((is_arith_type T) true))
52-
(u U :requires ((is_arith_type U) true)))
53-
Bool :chainable and)
54-
(declare-parameterized-const >= ((T Type :implicit) (U Type :implicit)
55-
(t T :requires ((is_arith_type T) true))
56-
(u U :requires ((is_arith_type U) true)))
57-
Bool :chainable and)
42+
(declare-parameterized-const < ((T Type :implicit) (U Type :implicit)) (-> (! T :requires ((is_arith_type T) true))
43+
(! U :requires ((is_arith_type U) true))
44+
Bool)
45+
:chainable and)
46+
(declare-parameterized-const <= ((T Type :implicit) (U Type :implicit)) (-> (! T :requires ((is_arith_type T) true))
47+
(! U :requires ((is_arith_type U) true))
48+
Bool)
49+
: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+
(! U :requires ((is_arith_type U) true))
56+
Bool)
57+
:chainable and)
5858

59-
(declare-parameterized-const to_real ((T Type :implicit) (t T :requires ((is_arith_type T) true)))
60-
Real)
61-
(declare-parameterized-const to_int ((T Type :implicit) (t T :requires ((is_arith_type T) true)))
62-
Int)
63-
(declare-parameterized-const is_int ((T Type :implicit) (t T :requires ((is_arith_type T) true)))
64-
Bool)
65-
(declare-parameterized-const abs ((T Type :implicit) (t T :requires ((is_arith_type T) true)))
66-
T)
59+
(declare-parameterized-const to_real ((T Type :implicit)) (-> (! T :requires ((is_arith_type T) true))
60+
Real))
61+
(declare-parameterized-const to_int ((T Type :implicit)) (-> (! T :requires ((is_arith_type T) true))
62+
Int))
63+
(declare-parameterized-const is_int ((T Type :implicit)) (-> (! T :requires ((is_arith_type T) true))
64+
Bool))
65+
(declare-parameterized-const abs ((T Type :implicit)) (-> (! T :requires ((is_arith_type T) true))
66+
T))
6767

6868
; power
6969
(declare-parameterized-const ^ ((T Type :implicit) (U Type :implicit)) (-> T U (arith_typeunion T U)))
7070

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

‎tests/bv-extract-smt3.eo‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -8,9 +8,9 @@
88
(declare-const +1 (-> Int Int))
99

1010
(declare-const BitVec (-> Int Type))
11-
(declare-const extract
12-
(-> (! Int :var m :syntax <numeral> :implicit :restrict (< 0 m))
13-
(! Int :var i :syntax <numeral> :restrict (< i m))
14-
(! Int :var j :syntax <numeral> :restrict (<= 0 j i))
15-
(! Int :var k :syntax <numeral> :implicit :restrict (= k (+1 (- i j))))
16-
(BitVec m) (BitVec k)))
11+
(declare-parameterized-const extract (
12+
(m Int :syntax <numeral> :implicit :restrict (< 0 m))
13+
(i Int :syntax <numeral> :restrict (< i m))
14+
(j Int :syntax <numeral> :restrict (<= 0 j i))
15+
(k Int :syntax <numeral> :implicit :restrict (= k (+1 (- i j)))))
16+
(-> (BitVec m) (BitVec k)))

‎tests/implicit-then-var.eo‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
11

2-
(declare-const = (-> (! Type :implicit :var T) T T Bool))
2+
(declare-parameterized-const = ((T Type :implicit)) (-> T T Bool))
33

44
(define d () (= true false) :type Bool)

‎tests/nested-requires.eo‎

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

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

‎tests/opaque-inst2.eo‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -13,10 +13,8 @@
1313
(declare-const select (-> (Array Int Int) Int Int))
1414

1515

16-
(declare-const @array_deq_diff
16+
(declare-parameterized-const @array_deq_diff ((T Type :implicit) (U Type :implicit))
1717
(->
18-
(! Type :implicit :var T)
19-
(! Type :implicit :var U)
2018
(! (Array T U) :opaque)
2119
(! (Array T U) :opaque)
2220
T

‎tests/param-dt-parse-amb-fun.eo‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
(declare-type Int ())
33
(declare-consts <numeral> Int)
44

5-
(declare-const @test (-> (! Type :opaque :var T) Int T))
5+
(declare-parameterized-const @test ((T Type :opaque)) (-> Int T))
66

77
(define t () (@test Bool 0) :type Bool)
88

‎tests/param-dt-parse.eo‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
(declare-type Int ())
33
(declare-consts <numeral> Int)
44

5-
(declare-const @test (-> (! Type :opaque :var T) Int T))
5+
(declare-parameterized-const @test ((T Type :opaque)) (-> Int T))
66

77
(define t () (@test Bool 0) :type Bool)
88

‎tests/quote-opaque.eo‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
(declare-type Int ())
22
(declare-consts <numeral> Int)
33

4-
(declare-const @const (-> (! Int :opaque) (! Type :var T :opaque) T))
4+
(declare-parameterized-const @const ((id Int :opaque) (T Type :opaque)) T)
55

66

77

‎tests/substitution-opaque.eo‎

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -29,12 +29,8 @@
2929
(declare-type Array (Type Type))
3030
(declare-type Int ())
3131

32-
(declare-const @array_deq_diff
33-
(->
34-
(! (Array Int Int) :opaque)
35-
(! (Array Int Int) :opaque)
36-
Int
37-
)
32+
(declare-parameterized-const @array_deq_diff ((a (Array Int Int) :opaque) (b (Array Int Int) :opaque))
33+
Int
3834
)
3935

4036
(declare-const n (Array Int Int))

0 commit comments

Comments
 (0)