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
|
mod ast;
mod checker;
mod checker_set;
mod checker_signature;
mod checker_state;
mod parser;
use tracing_subscriber::{layer::SubscriberExt, util::SubscriberInitExt};
use tracing_tree::HierarchicalLayer;
fn main() {
tracing_subscriber::registry()
.with(
HierarchicalLayer::new(2)
.with_targets(false)
.with_bracketed_fields(true),
)
.init();
let src = r#"
// let X be the set Y, call it Z
// let set X = record { b : Bool, n : Nat }
// let set Y = X
// let set Z = record { y : Y }
// make some elements
// let element x : X = { .b = true, .n = 41 }
// let element z : Z = { .y = x }
// exercise case matching
// let set Z_or_Float = variant [ z : Z | f : Float ]
// let element injected : Z_or_Float = z. z
// let element check_cases : Nat = case injected of [ z. myz => myz .y .n | f. myf => 2 ]
// let signature Graph = theory { Node :: Set, Edge :: (s : set-of(Node)) (t : set-of(Node)) -> Set }
// let instance natPoset :: Graph = { .Node = Nat :: Set , .Edge = for (s : Nat) (t : Nat), Bool :: Set }
// let element e : set-of(natPoset .Edge 3 5) = true
// this should be difficult unless we correctly handle various forms of alpha/beta
// let signature OneSet = theory { F :: Set }
// let signature T = theory {
// A :: Set,
// B :: (x : set-of({ .F = A } .F)) -> Set,
// C :: (x : set-of(set-of(set-of(A) :: Set) :: Set)) (b : set-of(B x)) -> Set
// }
let signature Graph = theory {
Node :: Set,
Edge :: (s : set-of(Node)) (t : set-of(Node)) -> Set
}
let instance natPoset :: Graph = {
.Node = Nat :: Set,
.Edge = for (s : Nat) (t : Nat), Bool :: Set
}
// let element node : set-of(natPoset .Node) = 7
// let set NatEdges = record {
// source: set-of(natPoset .Node),
// target: set-of(natPoset .Node),
// connected: set-of(natPoset .Edge source target)
// }
"#;
let programme = parser::debug_parse(src);
if let Err(e) = programme.check() {
println!("{}", e);
}
}
|
