diff options
| author | adelon <22380201+adelon@users.noreply.github.com> | 2026-07-03 02:13:21 +0200 |
|---|---|---|
| committer | adelon <22380201+adelon@users.noreply.github.com> | 2026-07-03 02:13:21 +0200 |
| commit | 40bc466d6a996e731cba21f24a58be08b1f22689 (patch) | |
| tree | b1266521dd2241c55342297bc5628156480a7c7f /source/Syntax/Internal.hs | |
| parent | 63756b371e363f3f771429920360ecff89ab502d (diff) | |
Track ownership of top-level symbols
Require every ownable top-level symbol to be introduced by a dedicated owner before it can appear in facts. Reject duplicate ownership and prevent symbols used by inductive definitions from being defined later.
Use the ownership/dependency information to reject hidden recursive inductive definitions and to generate referenceable inductive principles.
BREAKING CHANGE: Top-level facts no longer introduce symbols implicitly.
Diffstat (limited to 'source/Syntax/Internal.hs')
| -rw-r--r-- | source/Syntax/Internal.hs | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs index 782d52a..78e6b91 100644 --- a/source/Syntax/Internal.hs +++ b/source/Syntax/Internal.hs @@ -34,6 +34,7 @@ import Syntax.Abstract , LexicalItem , LexicalItemSgPl , RelationSymbol(..) + , PrefixPredicate(..) , StructSymbol (..) , Relation , PropositionalConstant(..) @@ -600,7 +601,12 @@ data DatatypeClause = DatatypeClause data Signature = SignaturePredicate Predicate (NonEmpty VarSymbol) - | SignatureFormula Formula -- TODO: Reconsider, this is pretty lossy. + | SignatureFormula Formula + -- TODO: This is a lossy encoding of a symbolic signature declaration. + -- The checker currently recovers the declared mixfix symbol heuristically + -- from the generated formula in order to assign ownership. Replace this + -- with a precise signature representation that carries the declared symbol + -- directly. deriving instance Show Signature deriving instance Eq Signature |