diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/checker_signature.rs | 8 | ||||
| -rw-r--r-- | src/checker_state.rs | 6 | ||||
| -rw-r--r-- | src/main.rs | 6 | ||||
| -rw-r--r-- | src/parser.rs | 14 |
4 files changed, 20 insertions, 14 deletions
diff --git a/src/checker_signature.rs b/src/checker_signature.rs index 36b11ca..15203b2 100644 --- a/src/checker_signature.rs +++ b/src/checker_signature.rs @@ -58,7 +58,11 @@ impl CheckerState { }); }; let set = Box::new(self.check_set(*set.clone())?); - Ok(Instance::SetCoerce(set)) + if let Set::ClaimedSet(inner) = *set { + Ok(inner) + } else { + Ok(Instance::SetCoerce(set)) + } } Instance::Var(ref v) => { // Exactly the same discipline as for Element::Var, see there @@ -158,7 +162,7 @@ impl CheckerState { Ok(sub_element) } _ => panic!( - "invariant violation: check_element returned neither a record or stuck computation for record set" + "invariant violation: check_instance returned neither a record or stuck computation for record set" ), } } diff --git a/src/checker_state.rs b/src/checker_state.rs index dc76a10..b710ac3 100644 --- a/src/checker_state.rs +++ b/src/checker_state.rs @@ -442,11 +442,9 @@ impl CheckerState { Instance::Var(canonical.clone()).into(), signature.clone(), )?; - // And lo, the special case: - // TODO: is this correct in the presence of de bruijn? + // And lo, the special case, our chosen canonical form if signature == Signature::Set { - self.add_set(canonical.clone(), SetValue::Hypothetical)?; - self.add_set(name, Set::Var(canonical).into())?; + self.add_set(name, Set::ClaimedSet(Instance::Var(canonical)).into())?; } self.binder_instance += 1; diff --git a/src/main.rs b/src/main.rs index a40eb87..94a9428 100644 --- a/src/main.rs +++ b/src/main.rs @@ -36,7 +36,7 @@ let signature OneSet = theory { F :: Set } let signature T = theory { A :: Set, B :: (x : set-of({ .F = A } .F)) -> Set, - C :: (x : set-of(A)) (b : set-of(B x)) -> Set + C :: (x : set-of(set-of(set-of(A) :: Set) :: Set)) (b : set-of(B x)) -> Set } let signature Graph = theory { @@ -45,8 +45,8 @@ let signature Graph = theory { } let instance natPoset :: Graph = { - .Node = Nat, - .Edge = for (s : Nat) (t : Nat), Bool + .Node = Nat :: Set, + .Edge = for (s : Nat) (t : Nat), Bool :: Set } let element node : set-of(natPoset .Node) = 7 diff --git a/src/parser.rs b/src/parser.rs index 65aa7f4..e917aac 100644 --- a/src/parser.rs +++ b/src/parser.rs @@ -179,9 +179,13 @@ parser! { = n:project_upper() _ "=" _ i:instance() { InstAssign { name: n, instance: i } } + rule explicit_set_coerce() -> Set + = _ s:set() _ "::" _ kw_Set() _ { s } + rule atom_inst() -> Instance - = s:set() { Instance::SetCoerce(Box::new(s)) } - / v:inst_var() { Instance::Var(v) } + = v:inst_var() { Instance::Var(v) } + / f:sig_var() { Instance::Var(f) } + / s:explicit_set_coerce() { Instance::SetCoerce(Box::new(s)) } / "{" fs:(inst_assign() ** ",") _ "}" { Instance::Record(fs) } / "(" _ i:instance() _ ")" { i } @@ -291,8 +295,8 @@ let set Maybe = variant [ } let instance natPoset :: Graph = { - .Node = Nat, - .Edge = for (s : Nat) (t : Nat), Bool + .Node = (Nat :: Set), + .Edge = for (s : Nat) (t : Nat), Bool::Set } let element node : set-of(natPoset .Node) = 7 @@ -300,7 +304,7 @@ let set Maybe = variant [ let set NatEdges = record { source: set-of(natPoset .Node), target: set-of(natPoset .Node), - connected: set-of(natPoset .Edge source target) + connected: set-of(set-of(natPoset .Edge source target) :: Set) } "#; |