blob: 3bc86a9c10e58e21a86cb2f2c1db540a64cc03fc (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
|
import Lean
import Lean.Meta.Tactic.Simp
import Mathlib.Tactic.Linarith
import Base.Primitives.Scalar
import Base.Arith
namespace Primitives
open Lean Meta Elab Term
/- Something strange happens here: when we solve the goal with scalar_tac, it
sometimes leaves meta-variables in place, which then causes issues when
type-checking functions. For instance, it happens when we have const-generics
in the translation: the constants contain meta-variables, which are then
used in the types, which cause issues later. An example is given below:
-/
macro:max x:term:max noWs "#isize" : term => `(Isize.ofInt $x (by first | decide | scalar_tac))
macro:max x:term:max noWs "#i8" : term => `(I8.ofInt $x (by first | decide | scalar_tac))
macro:max x:term:max noWs "#i16" : term => `(I16.ofInt $x (by first | decide | scalar_tac))
macro:max x:term:max noWs "#i32" : term => `(I32.ofInt $x (by first | decide | scalar_tac))
macro:max x:term:max noWs "#i64" : term => `(I64.ofInt $x (by first | decide | scalar_tac))
macro:max x:term:max noWs "#i128" : term => `(I128.ofInt $x (by first | decide | scalar_tac))
macro:max x:term:max noWs "#usize" : term => `(Usize.ofInt $x (by first | decide | scalar_tac))
macro:max x:term:max noWs "#u8" : term => `(U8.ofInt $x (by first | decide | scalar_tac))
macro:max x:term:max noWs "#u16" : term => `(U16.ofInt $x (by first | decide | scalar_tac))
macro:max x:term:max noWs "#u32" : term => `(U32.ofInt $x (by first | decide | scalar_tac))
macro:max x:term:max noWs "#u64" : term => `(U64.ofInt $x (by first | decide | scalar_tac))
macro:max x:term:max noWs "#u128" : term => `(U128.ofInt $x (by first | decide | scalar_tac))
-- Notation for pattern matching
-- We make the precedence looser than the negation.
notation:70 a:70 "#scalar" => Scalar.mk (a) _ _
/- Testing the notations -/
example := 0#u32
example := 1#u32
example := 1#i32
example := 0#isize
example := (-1)#isize
example := 1#u32
/-
-- This doesn't work anymore
example (x : U32) : Bool :=
match x with
| 0#u32 => true
| _ => false
example (x : U32) : Bool :=
match x with
| 1#u32 => true
| _ => false
example (x : I32) : Bool :=
match x with
| (-1)#i32 => true
| _ => false
-/
example (x : U32) : Bool :=
match x with
| 0#scalar => true
| _ => false
example (x : U32) : Bool :=
match x with
| 1#scalar => true
| _ => false
example (x : I32) : Bool :=
match x with
| (-1)#scalar => true
| _ => false
example {ty} (x : Scalar ty) : ℤ :=
match x with
| v#scalar => v
example {ty} (x : Scalar ty) : Bool :=
match x with
| 1#scalar => true
| _ => false
example {ty} (x : Scalar ty) : Bool :=
match x with
| -(1 : Int)#scalar => true
| _ => false
-- Testing the notations
example : Result Usize := 0#usize + 1#usize
-- More complex expressions
example (x y : Int) (h : 0 ≤ x + y ∧ x + y ≤ 1000) : U32 := (x + y)#u32
namespace Scalar.Examples
abbrev Array (a : Type) (len : U32) := { l : List a // l.length = len.val }
-- Checking the syntax
example : Array Int 0#u32 := ⟨ [], by simp ⟩
/- The example below fails if we don't use `decide` in the elaboration
of the scalar notation -/
example (a : Array (Array Int 32#u32) 32#u32) := a
end Scalar.Examples
end Primitives
|
