diff options
23 files changed, 159 insertions, 146 deletions
diff --git a/library/topology/urysohntwo.tex b/library/topology/urysohntwo.tex index eda3c32..7f69aa4 100644 --- a/library/topology/urysohntwo.tex +++ b/library/topology/urysohntwo.tex @@ -473,7 +473,7 @@ \begin{proof}[Proof by \in-induction on $n$] Assume $n \in \naturals$. Suppose $Y$ has cardinality $n$. - $X$ has cardinality $n$ by \cref{bijection_converse_is_bijection,bijection_circ,regularity,cardinality,foundation,empty_eq,emptyset}. + $X$ has cardinality $n$ by \cref{bijection_converse_is_bijection,bijection_circ,regularity,cardinality,foundation,emptyset}. \begin{byCase} \caseOf{$n = \zero$.} Follows by \cref{converse_converse_eq,injective_converse_is_function,converse_is_relation,dom_converse,id_is_function_to,id_ran,ran_circ_exact,circ,ran_converse,emptyset_is_function_on_emptyset,bijective_converse_are_funs,relext,function_member_elim,bijection_is_function,cardinality,bijections_dom,in_irrefl,codom_of_emptyset_can_be_anything,converse_emptyset,funs_elim,neq_witness,id}. diff --git a/source/Meaning.hs b/source/Meaning.hs index 3822221..61f1d7b 100644 --- a/source/Meaning.hs +++ b/source/Meaning.hs @@ -42,6 +42,7 @@ type Gloss = ExceptT GlossError (State GlossState) data GlossError = GlossDefnError DefnError String | GlossInductionError + | GlossRelationExprWithParams deriving (Show, Eq, Ord) @@ -189,36 +190,39 @@ glossChain :: Sem.Chain -> Gloss (Sem.ExprOf VarSymbol) glossChain ch = Sem.makeConjunction <$> makeRels (conjuncts (splat ch)) where -- | Separate each link of the chain into separate triples. - splat :: Raw.Chain -> [(NonEmpty Raw.Expr, Sign, Raw.Relation, NonEmpty Raw.Expr)] + splat :: Raw.Chain -> [(NonEmpty Raw.Expr, Sign, Raw.Relation, [Raw.Expr], NonEmpty Raw.Expr)] splat = \case - Raw.ChainBase es sign rel es' - -> [(es, sign, rel, es')] - Raw.ChainCons es sign rel ch'@(Raw.ChainBase es' _ _ _) - -> (es, sign, rel, es') : splat ch' - Raw.ChainCons es sign rel ch'@(Raw.ChainCons es' _ _ _) - -> (es, sign, rel, es') : splat ch' + Raw.ChainBase es sign rel params es' + -> [(es, sign, rel, params, es')] + Raw.ChainCons es sign rel params ch'@(Raw.ChainBase es' _ _ _ _) + -> (es, sign, rel, params, es') : splat ch' + Raw.ChainCons es sign rel params ch'@(Raw.ChainCons es' _ _ _ _) + -> (es, sign, rel, params, es') : splat ch' -- | Take each triple and combine the lhs/rhs to make all the conjuncts. - conjuncts :: [(NonEmpty Raw.Expr, Sign, Raw.Relation, NonEmpty Raw.Expr)] -> [(Sign, Raw.Relation, Raw.Expr, Raw.Expr)] + conjuncts :: [(NonEmpty Raw.Expr, Sign, Raw.Relation, [Raw.Expr], NonEmpty Raw.Expr)] -> [(Sign, Raw.Relation, [Raw.Expr], Raw.Expr, Raw.Expr)] conjuncts triples = do - (e1s, sign, rel, e2s) <- triples + (e1s, sign, rel, params, e2s) <- triples e1 <- toList e1s e2 <- toList e2s - pure (sign, rel, e1, e2) + pure (sign, rel, params, e1, e2) - makeRels :: [(Sign, Raw.Relation, Raw.Expr, Raw.Expr)] -> Gloss [Sem.Formula] + makeRels :: [(Sign, Raw.Relation, [Raw.Expr], Raw.Expr, Raw.Expr)] -> Gloss [Sem.Formula] makeRels triples = for triples makeRel - makeRel :: (Sign, Raw.Relation, Raw.Expr, Raw.Expr) -> Gloss Sem.Formula - makeRel (sign, rel, e1, e2) = do + makeRel :: (Sign, Raw.Relation, [Raw.Expr], Raw.Expr, Raw.Expr) -> Gloss Sem.Formula + makeRel (sign, rel, params, e1, e2) = do e1' <- glossExpr e1 e2' <- glossExpr e2 + params' <- glossExpr `each` params case rel of Raw.RelationSymbol tok -> - pure $ sign' $ Sem.Relation tok (e1' : [e2']) - Raw.RelationExpr e -> do - e' <- glossExpr e - pure $ sign' $ Sem.TermPair e1' e2' `Sem.IsElementOf` e' + pure $ sign' $ Sem.Relation tok (params' <> [e1',e2']) + Raw.RelationExpr e -> case params of + [] -> do + e' <- glossExpr e + pure (sign' (Sem.TermPair e1' e2' `Sem.IsElementOf` e')) + _ -> throwError GlossRelationExprWithParams where sign' = case sign of Positive -> id @@ -542,8 +546,12 @@ glossDefnHead = \case pure $ \asms f -> Sem.DefnPredicate asms (Sem.PredicateVerb verb) (v :| vs) f Raw.DefnNoun v (Raw.Noun noun vs) -> pure $ \asms f -> Sem.DefnPredicate asms (Sem.PredicateNoun noun) (v :| vs) f - Raw.DefnRel v1 rel v2 -> - pure $ \asms f -> Sem.DefnPredicate asms (Sem.PredicateRelation rel) (v1 :| [v2]) f + Raw.DefnRel v1 rel params v2 -> + pure \asms f -> + let args = case params of + p : ps -> p :| (ps <> [v1, v2]) + [] -> v1 :| [v2] + in Sem.DefnPredicate asms (Sem.PredicateRelation rel) args f Raw.DefnSymbolicPredicate (Raw.PrefixPredicate symb _ar) vs -> pure $ \asms f -> Sem.DefnPredicate asms (Sem.PredicateSymbol symb) vs f @@ -688,8 +696,8 @@ glossAbbreviation = \case makeAbbrStmt (Sem.SymbolPredicate (Sem.PredicateVerb verb)) (x : xs) stmt Raw.AbbreviationNoun x (Raw.Noun noun xs) stmt -> makeAbbrStmt (Sem.SymbolPredicate (Sem.PredicateNoun noun)) (x : xs) stmt - Raw.AbbreviationRel x rel y stmt -> - makeAbbrStmt (Sem.SymbolPredicate (Sem.PredicateRelation rel)) [x, y] stmt + Raw.AbbreviationRel x rel params y stmt -> + makeAbbrStmt (Sem.SymbolPredicate (Sem.PredicateRelation rel)) (params <> [x, y]) stmt Raw.AbbreviationFun (Raw.Fun fun xs) t -> makeAbbrTerm (Sem.SymbolFun fun) xs t Raw.AbbreviationEq (Raw.SymbolPattern op xs) e -> diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs index 23da652..31a1029 100644 --- a/source/Syntax/Abstract.hs +++ b/source/Syntax/Abstract.hs @@ -92,8 +92,8 @@ makeTuple = foldr1 ExprPair data Chain - = ChainBase (NonEmpty Expr) Sign Relation (NonEmpty Expr) - | ChainCons (NonEmpty Expr) Sign Relation Chain + = ChainBase (NonEmpty Expr) Sign Relation [Expr] (NonEmpty Expr) -- left arguments, possibly empty list of parameters, right arguments + | ChainCons (NonEmpty Expr) Sign Relation [Expr] Chain deriving (Show, Eq, Ord) data Relation @@ -319,7 +319,7 @@ data DefnHead | DefnVerb (Maybe (NounPhrase Maybe)) VarSymbol (VerbOf VarSymbol) | DefnNoun VarSymbol (NounOf VarSymbol) | DefnSymbolicPredicate PrefixPredicate (NonEmpty VarSymbol) - | DefnRel VarSymbol RelationSymbol VarSymbol + | DefnRel VarSymbol RelationSymbol [VarSymbol] VarSymbol -- ^ E.g.: /@$x \subseteq y$ iff [...@/ deriving (Show, Eq, Ord) @@ -411,7 +411,7 @@ data Abbreviation = AbbreviationAdj VarSymbol (AdjOf VarSymbol) Stmt | AbbreviationVerb VarSymbol (VerbOf VarSymbol) Stmt | AbbreviationNoun VarSymbol (NounOf VarSymbol) Stmt - | AbbreviationRel VarSymbol RelationSymbol VarSymbol Stmt + | AbbreviationRel VarSymbol RelationSymbol [VarSymbol] VarSymbol Stmt | AbbreviationFun (FunOf VarSymbol) Term | AbbreviationEq SymbolPattern Expr deriving (Show, Eq, Ord) diff --git a/source/Syntax/Adapt.hs b/source/Syntax/Adapt.hs index b338d47..1b5a237 100644 --- a/source/Syntax/Adapt.hs +++ b/source/Syntax/Adapt.hs @@ -124,7 +124,7 @@ head = ScanNoun <$> noun <|> ScanAdj <$> adj <|> ScanVerb <$> verb <|> ScanFun <$> fun - <|> ScanRelationSymbol <$> relationSymbol + <|> ScanRelationSymbol . fst <$> relationSymbol <|> ScanFunctionSymbol <$> functionSymbol <|> ScanPrefixPredicate <$> prefixPredicate @@ -184,14 +184,19 @@ verb = toLexicalPhrase <$> (var *> pat <* iff) fun :: RE Token LexicalPhrase fun = toLexicalPhrase <$> (the *> pat <* (is <|> comma)) -relationSymbol :: RE Token RelationSymbol -relationSymbol = math relator' <* iff +relationSymbol :: RE Token (RelationSymbol, Int) +relationSymbol = definiendum <* iff where - relator' = do + definiendum = math do varSymbol rel <- symbol + k <- params varSymbol - pure rel + pure (rel, k) + params :: RE Token Int + params = do + vars <- many (sym InvisibleBraceL *> var <* sym InvisibleBraceR) + pure (length vars) functionSymbol :: RE Token FunctionSymbol functionSymbol = do diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs index 383f348..3c6700b 100644 --- a/source/Syntax/Concrete.hs +++ b/source/Syntax/Concrete.hs @@ -84,8 +84,8 @@ grammar lexicon@Lexicon{..} = mdo relationSign <- rule $ pure Positive <|> (Negative <$ command "not") relationExpr <- rule $ RelationExpr <$> (command "mathrel" *> group expr) relation <- rule $ (RelationSymbol <$> relator) <|> relationExpr - chainBase <- rule $ ChainBase <$> exprs <*> relationSign <*> relation <*> exprs - chainCons <- rule $ ChainCons <$> exprs <*> relationSign <*> relation <*> chain + chainBase <- rule $ ChainBase <$> exprs <*> relationSign <*> relation <*> many (brace expr) <*> exprs + chainCons <- rule $ ChainCons <$> exprs <*> relationSign <*> relation <*> many (brace expr) <*> chain chain <- rule $ chainCons <|> chainBase formulaPredicate <- rule $ asum $ prefixPredicateOf FormulaPredicate expr <$> HM.keys lexiconPrefixPredicates @@ -250,7 +250,7 @@ grammar lexicon@Lexicon{..} = mdo defnAdj <- rule $ DefnAdj <$> optional (_an *> nounPhrase) <*> var <* _is <*> adjVar defnVerb <- rule $ DefnVerb <$> optional (_an *> nounPhrase) <*> var <*> verbVar defnNoun <- rule $ DefnNoun <$> var <* _is <* _an <*> nounVar - defnRel <- rule $ DefnRel <$> (beginMath *> varSymbol) <*> relator <*> varSymbol <* endMath + defnRel <- rule $ DefnRel <$> (beginMath *> varSymbol) <*> relator <*> many (group varSymbol) <*> varSymbol <* endMath defnSymbolicPredicate <- rule $ math $ asum $ prefixPredicateOf DefnSymbolicPredicate varSymbol <$> HM.keys lexiconPrefixPredicates defnHead <- rule $ optional _write *> asum [defnAdj, defnVerb, defnNoun, defnRel, defnSymbolicPredicate] @@ -269,7 +269,7 @@ grammar lexicon@Lexicon{..} = mdo abbreviationVerb <- rule $ AbbreviationVerb <$> var <*> verbVar <* (_iff <|> _if) <*> stmt <* _dot abbreviationAdj <- rule $ AbbreviationAdj <$> var <* _is <*> adjVar <* (_iff <|> _if) <*> stmt <* _dot abbreviationNoun <- rule $ AbbreviationNoun <$> var <* _is <* _an <*> nounVar <* (_iff <|> _if) <*> stmt <* _dot - abbreviationRel <- rule $ AbbreviationRel <$> (beginMath *> varSymbol) <*> relator <*> varSymbol <* endMath <* (_iff <|> _if) <*> stmt <* _dot + abbreviationRel <- rule $ AbbreviationRel <$> (beginMath *> varSymbol) <*> relator <*> many (brace varSymbol) <*> varSymbol <* endMath <* (_iff <|> _if) <*> stmt <* _dot abbreviationFun <- rule $ AbbreviationFun <$> (_the *> funVar) <* (_is <|> _denotes) <*> term <* _dot abbreviationEq <- rule $ uncurry AbbreviationEq <$> symbolicPatternEqTerm abbreviation <- rule $ (abbreviationVerb <|> abbreviationAdj <|> abbreviationNoun <|> abbreviationRel <|> abbreviationFun <|> abbreviationEq) diff --git a/source/Syntax/Lexicon.hs b/source/Syntax/Lexicon.hs index 4fe8730..7f79294 100644 --- a/source/Syntax/Lexicon.hs +++ b/source/Syntax/Lexicon.hs @@ -112,7 +112,7 @@ prefixOps = , ([Just (Command "pow"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "pow")) , ([Just (Command "neg"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "neg")) , ([Just (Command "inv"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "inv")) - , ([Just (Command "abs"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "abs")) + , ([Just (Command "abs"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "abs")) , (ConsSymbol, (NonAssoc, "cons")) , (PairSymbol, (NonAssoc, "pair")) -- NOTE Is now defined and hence no longer necessary , (ApplySymbol, (NonAssoc, "apply")) diff --git a/test/golden/abbr/parsing.golden b/test/golden/abbr/parsing.golden index 2bc8148..77a4c47 100644 --- a/test/golden/abbr/parsing.golden +++ b/test/golden/abbr/parsing.golden @@ -24,7 +24,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "x" ) :| [] ) @@ -105,7 +105,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "x" ) :| [] ) @@ -181,7 +181,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) @@ -240,7 +240,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) @@ -267,7 +267,7 @@ ) Positive ( RelationSymbol ( Command "notin" ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) @@ -282,7 +282,7 @@ ) Negative ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) @@ -340,7 +340,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) @@ -396,7 +396,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) diff --git a/test/golden/byRef/parsing.golden b/test/golden/byRef/parsing.golden index 3df8730..e7e3287 100644 --- a/test/golden/byRef/parsing.golden +++ b/test/golden/byRef/parsing.golden @@ -15,7 +15,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "a" ) :| [] ) @@ -40,7 +40,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "b" ) :| [] ) @@ -65,7 +65,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "c" ) :| [] ) @@ -102,7 +102,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "e" ) :| [] ) @@ -128,7 +128,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "d" ) :| [] ) @@ -157,7 +157,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "f" ) :| [] ) diff --git a/test/golden/calc/parsing.golden b/test/golden/calc/parsing.golden index b6f393a..89997b4 100644 --- a/test/golden/calc/parsing.golden +++ b/test/golden/calc/parsing.golden @@ -15,7 +15,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "x" ) :| [] ) @@ -40,7 +40,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "z" ) :| [] ) @@ -65,7 +65,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) @@ -117,7 +117,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) @@ -141,7 +141,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) @@ -159,7 +159,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) diff --git a/test/golden/coord/parsing.golden b/test/golden/coord/parsing.golden index 65fa82f..a2b6657 100644 --- a/test/golden/coord/parsing.golden +++ b/test/golden/coord/parsing.golden @@ -31,7 +31,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "x" ) :| [] ) @@ -64,7 +64,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "x" ) :| [] ) @@ -97,7 +97,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "x" ) :| [] ) @@ -140,7 +140,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "x" ) :| [] ) @@ -190,7 +190,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "x" ) :| [] ) @@ -265,7 +265,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "x" ) :| [] ) @@ -291,7 +291,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) diff --git a/test/golden/finite-set-terms/parsing.golden b/test/golden/finite-set-terms/parsing.golden index c30f70b..e255c8d 100644 --- a/test/golden/finite-set-terms/parsing.golden +++ b/test/golden/finite-set-terms/parsing.golden @@ -16,7 +16,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "cons" ) @@ -45,7 +45,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) @@ -60,7 +60,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "X" ) :| [] ) @@ -111,7 +111,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "unit" ) diff --git a/test/golden/formula/parsing.golden b/test/golden/formula/parsing.golden index 7de1fb7..4012bde 100644 --- a/test/golden/formula/parsing.golden +++ b/test/golden/formula/parsing.golden @@ -20,7 +20,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "x" ) :| [] ) @@ -33,7 +33,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) @@ -64,7 +64,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) @@ -95,7 +95,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) @@ -114,7 +114,7 @@ ) Positive ( RelationSymbol ( Command "neq" ) - ) + ) [] ( ExprVar ( NamedVar "x" ) :| [] ) diff --git a/test/golden/geometry/parsing.golden b/test/golden/geometry/parsing.golden index b57f76c..1d067d0 100644 --- a/test/golden/geometry/parsing.golden +++ b/test/golden/geometry/parsing.golden @@ -244,7 +244,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "b" ) :| [] ) @@ -516,7 +516,7 @@ ) Positive ( RelationSymbol ( Command "neq" ) - ) + ) [] ( ExprVar ( NamedVar "b" ) :| [] ) @@ -590,7 +590,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "b" ) :| [] ) @@ -798,7 +798,7 @@ ) Positive ( RelationSymbol ( Command "neq" ) - ) + ) [] ( ExprVar ( NamedVar "v" ) :| [] ) diff --git a/test/golden/inductive/parsing.golden b/test/golden/inductive/parsing.golden index 7438daa..6d5c0e3 100644 --- a/test/golden/inductive/parsing.golden +++ b/test/golden/inductive/parsing.golden @@ -9,7 +9,7 @@ ( Defn [] ( DefnRel ( NamedVar "A" ) - ( Command "subseteq" ) + ( Command "subseteq" ) [] ( NamedVar "B" ) ) ( StmtFormula @@ -20,7 +20,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "B" ) :| [] ) @@ -176,7 +176,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "emptyset" ) @@ -224,7 +224,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "fin" ) @@ -247,7 +247,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "A" ) :| [] ) @@ -259,7 +259,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "fin" ) @@ -293,7 +293,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "fin" ) @@ -345,7 +345,7 @@ ) Positive ( RelationSymbol ( Command "subseteq" ) - ) + ) [] ( ExprVar ( NamedVar "B" ) :| [] ) @@ -369,7 +369,7 @@ ) Positive ( RelationSymbol ( Command "subseteq" ) - ) + ) [] ( ExprOp [ Just ( Command "fin" ) @@ -438,7 +438,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "R" ) :| [] ) @@ -451,7 +451,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "tracl" ) @@ -487,7 +487,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "tracl" ) @@ -520,7 +520,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "R" ) :| [] ) @@ -546,7 +546,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "tracl" ) @@ -616,7 +616,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "fld" ) @@ -650,7 +650,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "qrefltracl" ) @@ -686,7 +686,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "qrefltracl" ) @@ -719,7 +719,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "R" ) :| [] ) @@ -745,7 +745,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "qrefltracl" ) @@ -804,7 +804,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "A" ) :| [] ) @@ -830,7 +830,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "refltracl" ) @@ -871,7 +871,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "refltracl" ) @@ -909,7 +909,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "R" ) :| [] ) @@ -935,7 +935,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "refltracl" ) @@ -993,7 +993,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "fld" ) @@ -1028,7 +1028,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "pow" ) @@ -1057,7 +1057,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "acc" ) diff --git a/test/golden/no-reflexive-set/parsing.golden b/test/golden/no-reflexive-set/parsing.golden index 3de5dcc..d81dabd 100644 --- a/test/golden/no-reflexive-set/parsing.golden +++ b/test/golden/no-reflexive-set/parsing.golden @@ -34,7 +34,7 @@ ) Negative ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "A" ) :| [] ) diff --git a/test/golden/proofassume/parsing.golden b/test/golden/proofassume/parsing.golden index 57e542c..bf249ed 100644 --- a/test/golden/proofassume/parsing.golden +++ b/test/golden/proofassume/parsing.golden @@ -16,7 +16,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) @@ -31,7 +31,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) @@ -56,7 +56,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) @@ -72,7 +72,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) @@ -100,7 +100,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) @@ -115,7 +115,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "b" ) :| [] ) @@ -131,7 +131,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) @@ -156,7 +156,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "b" ) :| [] ) @@ -172,7 +172,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) @@ -188,7 +188,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) diff --git a/test/golden/proofdefinefunction/parsing.golden b/test/golden/proofdefinefunction/parsing.golden index eba14ec..c1ba1d0 100644 --- a/test/golden/proofdefinefunction/parsing.golden +++ b/test/golden/proofdefinefunction/parsing.golden @@ -72,7 +72,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "f" ) :| [] ) @@ -113,7 +113,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "f" ) :| [] ) @@ -139,7 +139,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) @@ -154,7 +154,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) diff --git a/test/golden/prooffix/parsing.golden b/test/golden/prooffix/parsing.golden index 26b2b35..2702f25 100644 --- a/test/golden/prooffix/parsing.golden +++ b/test/golden/prooffix/parsing.golden @@ -17,7 +17,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "x" ) :| [] ) @@ -44,7 +44,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "x" ) :| [] ) diff --git a/test/golden/relation-notation/parsing.golden b/test/golden/relation-notation/parsing.golden index 33f2808..bccafe0 100644 --- a/test/golden/relation-notation/parsing.golden +++ b/test/golden/relation-notation/parsing.golden @@ -18,7 +18,7 @@ ( ExprVar ( NamedVar "R" ) ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) @@ -35,7 +35,7 @@ ( ExprVar ( NamedVar "R" ) ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) diff --git a/test/golden/replace/parsing.golden b/test/golden/replace/parsing.golden index c2cd815..241ca01 100644 --- a/test/golden/replace/parsing.golden +++ b/test/golden/replace/parsing.golden @@ -16,7 +16,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Just ( Command "cons" ) @@ -45,7 +45,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "y" ) :| [] ) @@ -60,7 +60,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "X" ) :| [] ) @@ -176,7 +176,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Nothing , Just @@ -229,7 +229,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprFiniteSet ( ExprVar ( NamedVar "x" ) :| [] @@ -266,7 +266,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprReplace ( ExprOp [ Just diff --git a/test/golden/russell/parsing.golden b/test/golden/russell/parsing.golden index f924229..9f5dc37 100644 --- a/test/golden/russell/parsing.golden +++ b/test/golden/russell/parsing.golden @@ -57,7 +57,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "V" ) :| [] ) @@ -147,7 +147,7 @@ ) Negative ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "x" ) :| [] ) @@ -165,7 +165,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "R" ) :| [] ) @@ -180,7 +180,7 @@ ) Negative ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "R" ) :| [] ) diff --git a/test/golden/separation/parsing.golden b/test/golden/separation/parsing.golden index 2a2110f..132f408 100644 --- a/test/golden/separation/parsing.golden +++ b/test/golden/separation/parsing.golden @@ -15,7 +15,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprSep ( NamedVar "x" ) ( ExprVar @@ -29,7 +29,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "x" ) :| [] ) diff --git a/test/golden/union/parsing.golden b/test/golden/union/parsing.golden index 391f039..3ccdc08 100644 --- a/test/golden/union/parsing.golden +++ b/test/golden/union/parsing.golden @@ -19,7 +19,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "A" ) :| [] ) @@ -34,7 +34,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "B" ) :| [] ) @@ -52,7 +52,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprVar ( NamedVar "B" ) :| [] ) @@ -96,7 +96,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Nothing , Just @@ -121,7 +121,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "A" ) :| [] ) @@ -136,7 +136,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprVar ( NamedVar "B" ) :| [] ) @@ -172,7 +172,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprOp [ Nothing , Just @@ -224,7 +224,7 @@ ) Positive ( RelationSymbol ( Symbol "=" ) - ) + ) [] ( ExprOp [ Nothing , Just @@ -269,7 +269,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Nothing , Just @@ -302,7 +302,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Nothing , Just @@ -341,7 +341,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Nothing , Just @@ -374,7 +374,7 @@ ) Positive ( RelationSymbol ( Command "in" ) - ) + ) [] ( ExprOp [ Nothing , Just |