diff options
| -rw-r--r-- | source/Checking.hs | 20 | ||||
| -rw-r--r-- | source/Render/Html.hs | 16 | ||||
| -rw-r--r-- | source/Test/Unit/Checking.hs | 33 | ||||
| -rw-r--r-- | test/examples/inductive.tex | 6 | ||||
| -rw-r--r-- | test/golden/inductive/encoding tasks.golden | 16 | ||||
| -rw-r--r-- | test/golden/inductive/generating tasks.golden | 1000 | ||||
| -rw-r--r-- | test/golden/inductive/glossing.golden | 42 | ||||
| -rw-r--r-- | test/golden/inductive/parsing.golden | 44 | ||||
| -rw-r--r-- | test/golden/inductive/scanning.golden | 5 | ||||
| -rw-r--r-- | test/golden/inductive/tokenizing.golden | 17 |
10 files changed, 540 insertions, 659 deletions
diff --git a/source/Checking.hs b/source/Checking.hs index f1f29c4..f80e164 100644 --- a/source/Checking.hs +++ b/source/Checking.hs @@ -1992,6 +1992,13 @@ inductiveConditionFormulaAt _ replacement = \case CheckedInductiveRecursiveCondition{checkedInductiveRecursiveTerm, checkedInductiveRecursiveCarrierTemplate} -> isElementOf checkedInductiveRecursiveTerm (instantiate1 replacement checkedInductiveRecursiveCarrierTemplate) +semanticSubsetFormula :: Set VarSymbol -> Expr -> Expr -> Formula +semanticSubsetFormula reserved left right = + makeForall [witnessVar] + (isElementOf (TermVar witnessVar) left `Implies` isElementOf (TermVar witnessVar) right) + where + witnessVar = freshGeneratedVar (reserved <> freeVars left <> freeVars right) "x" + inductiveSoundnessGoals :: CheckedInductive -> [Formula] inductiveSoundnessGoals checked = inductiveMonotonicityGoals checked <> inductiveDomainGoals checked @@ -1999,9 +2006,9 @@ inductiveSoundnessGoals checked = inductiveMonotonicityGoals :: CheckedInductive -> [Formula] inductiveMonotonicityGoals checked = [ forallIfNeeded [leftVar, rightVar] - ( IsSubsetOf Nowhere (TermVar leftVar) (TermVar rightVar) + ( semanticSubsetFormula usedVars (TermVar leftVar) (TermVar rightVar) `Implies` - IsSubsetOf Nowhere + semanticSubsetFormula usedVars (instantiate1 (TermVar leftVar) checkedInductiveRecursiveCarrierTemplate) (instantiate1 (TermVar rightVar) checkedInductiveRecursiveCarrierTemplate) ) @@ -2067,7 +2074,8 @@ inductiveIntroFormula checked intro = inductiveDomSubsetFormula :: CheckedInductive -> Formula inductiveDomSubsetFormula checked = - forallIfNeeded (checkedInductiveParams checked) (IsSubsetOf Nowhere (inductiveCarrierTerm checked) (checkedInductiveDomain checked)) + forallIfNeeded (checkedInductiveParams checked) + (semanticSubsetFormula (inductiveUsedVars checked) (inductiveCarrierTerm checked) (checkedInductiveDomain checked)) inductiveCasesFormula :: CheckedInductive -> Formula inductiveCasesFormula checked = @@ -2092,7 +2100,11 @@ inductiveInductFormula checked = where subsetVar = freshGeneratedVar (inductiveUsedVars checked) "S" closures = inductiveInductionClosure checked subsetVar <$> NonEmpty.toList (checkedInductiveIntros checked) - conclusion = IsSubsetOf Nowhere (inductiveCarrierTerm checked) (TermVar subsetVar) + conclusion = + semanticSubsetFormula + (Set.insert subsetVar (inductiveUsedVars checked)) + (inductiveCarrierTerm checked) + (TermVar subsetVar) inductiveInductionClosure :: CheckedInductive -> VarSymbol -> CheckedInductiveIntro -> Formula inductiveInductionClosure checked subsetVar intro = diff --git a/source/Render/Html.hs b/source/Render/Html.hs index 90bef42..a45f422 100644 --- a/source/Render/Html.hs +++ b/source/Render/Html.hs @@ -2112,6 +2112,15 @@ elementOfFormula :: Expr -> Expr -> Formula elementOfFormula left right = FormulaChain (ChainBase (left :| []) Positive (Relation Nowhere ElementSymbol []) (right :| [])) +semanticSubsetFormula :: Set VarSymbol -> Expr -> Expr -> Formula +semanticSubsetFormula reserved left right = + forallIfNeeded [witnessVar] + (impliesFormula + (elementOfFormula (ExprVar witnessVar) left) + (elementOfFormula (ExprVar witnessVar) right)) + where + witnessVar = freshDatatypeVar (reserved <> Set.fromList (exprVars left <> exprVars right)) "x" + equalsFormula :: Expr -> Expr -> Formula equalsFormula left right = FormulaChain (ChainBase (left :| []) Positive (Relation Nowhere EqSymbol []) (right :| [])) @@ -2331,7 +2340,7 @@ inductiveIntroFormula info clause = inductiveDomSubsetFormula :: InductiveRenderInfo -> Formula inductiveDomSubsetFormula info = forallIfNeeded (inductiveRenderParams info) - (FormulaChain (ChainBase (inductiveRenderCarrierExpr info :| []) Positive (Relation Nowhere SubseteqSymbol []) (inductiveRenderDomainExpr info :| []))) + (semanticSubsetFormula (inductiveUsedVars info) (inductiveRenderCarrierExpr info) (inductiveRenderDomainExpr info)) inductiveCasesFormula :: InductiveRenderInfo -> Formula inductiveCasesFormula info = @@ -2354,7 +2363,10 @@ inductiveInductFormula info = subsetVar = freshDatatypeVar (inductiveUsedVars info) "S" closures = inductiveInductionClosure subsetVar <$> NonEmpty.toList (inductiveRenderClauses info) conclusion = - FormulaChain (ChainBase (inductiveRenderCarrierExpr info :| []) Positive (Relation Nowhere SubseteqSymbol []) (ExprVar subsetVar :| [])) + semanticSubsetFormula + (Set.insert subsetVar (inductiveUsedVars info)) + (inductiveRenderCarrierExpr info) + (ExprVar subsetVar) inductiveInductionClosure :: VarSymbol -> InductiveRenderClause -> Formula inductiveInductionClosure subsetVar clause = diff --git a/source/Test/Unit/Checking.hs b/source/Test/Unit/Checking.hs index a5ee61a..cea5873 100644 --- a/source/Test/Unit/Checking.hs +++ b/source/Test/Unit/Checking.hs @@ -103,7 +103,9 @@ unitTests = testGroup "Checking" expectChecks inductiveInductReferenceBlocks , testCase "inductive generates monotonicity obligations for recursive carriers" do text <- encodedTasksText goodMonotoneInductiveBlocks - assertContains "monotonicity task for wrapped carrier" "subseteq(wrap(Xxa),wrap(Xxb))" text + assertContains "monotonicity antecedent expands subset" "elem(Xx1,Xxa)=>elem(Xx1,Xxb)" text + assertContains "monotonicity conclusion expands subset" "elem(Xx1,wrap(Xxa))=>elem(Xx1,wrap(Xxb))" text + assertNotContains "monotonicity task avoids subseteq" "subseteq(" text , testCase "inductive rejects recursive premises outside carrier positions" do expectCheckingError "carrier of a membership premise" [badRecursiveTermInductiveBlock] , testCase "inductive rejects malformed recursive premises" do @@ -463,8 +465,7 @@ goodInductiveBlock = goodInductiveBlocks :: [Block] goodInductiveBlocks = - [ subseteqDefinitionBlock - , goodInductiveBlock + [ goodInductiveBlock ] goodMonotoneInductiveBlock :: Block @@ -482,8 +483,7 @@ goodMonotoneInductiveBlock = goodMonotoneInductiveBlocks :: [Block] goodMonotoneInductiveBlocks = - [ subseteqDefinitionBlock - , wrapSignatureBlock + [ wrapSignatureBlock , goodMonotoneInductiveBlock ] @@ -504,7 +504,9 @@ inductiveIntroAndDomainReferenceBlocks = , BlockProof Nowhere Nowhere (Qed (Just Nowhere) (JustificationRef ("fin_intro_1" :| []))) , BlockLemma Nowhere "inductive_dom_subset_ref" - (Lemma [] (makeForall ["A"] (IsSubsetOf Nowhere (finTerm (var "A")) (powTerm (var "A"))))) + (Lemma [] $ + makeForall ["A"] $ + semanticSubsetFormula (Set.fromList ["A"]) (finTerm (var "A")) (powTerm (var "A"))) , BlockProof Nowhere Nowhere (Qed (Just Nowhere) (JustificationRef ("fin_dom_subset" :| []))) ] @@ -647,8 +649,7 @@ datatypeConstructorThenOperatorBlocks = frozenSymbolDefinitionBlocks :: [Block] frozenSymbolDefinitionBlocks = - [ subseteqDefinitionBlock - , laterSignatureBlock + [ laterSignatureBlock , freezingInductiveBlock , BlockDefn Nowhere "later_operator_definition" (DefnOp laterSym ["A"] emptySet) ] @@ -668,8 +669,7 @@ freezingInductiveBlock = canonicalizedDomainFreezeBlocks :: [Block] canonicalizedDomainFreezeBlocks = - [ subseteqDefinitionBlock - , laterSignatureBlock + [ laterSignatureBlock , BlockAbbr Nowhere "domain_alias_abbr" (Abbreviation (SymbolMixfix domainAliasSym) @@ -686,8 +686,7 @@ canonicalizedDomainFreezeBlocks = transitiveFrozenDefinitionBlocks :: [Block] transitiveFrozenDefinitionBlocks = - [ subseteqDefinitionBlock - , laterSignatureBlock + [ laterSignatureBlock , BlockDefn Nowhere "middle_later_alias_definition" (DefnOp middleLaterAliasSym ["A"] (laterTerm (var "A"))) , BlockDefn Nowhere "indirect_later_alias_definition" (DefnOp indirectLaterAliasSym ["A"] (middleLaterAliasTerm (var "A"))) , BlockInductive Nowhere "transitive_freeze_inductive" Inductive @@ -779,7 +778,10 @@ finInductFormula = (consTerm (var "a") (var "B") `isElementOf` var "S")) ] `Implies` - IsSubsetOf Nowhere (finTerm (var "A")) (var "S")) + semanticSubsetFormula + (Set.fromList ["A", "S"]) + (finTerm (var "A")) + (var "S")) goodDatatypeClauses :: NonEmpty DatatypeClause goodDatatypeClauses = @@ -874,11 +876,6 @@ propformSignatureFormula = makeForall ["z"] ((var "z" `eq` propformTerm) `Implies` (var "z" `eq` var "z")) -subseteqDefinitionBlock :: Block -subseteqDefinitionBlock = - BlockDefn Nowhere "subseteq_definition" - (DefnPredicate [] (PredicateRelation SubseteqSymbol) ("A" :| ["B"]) (var "A" `eq` var "B")) - wrapSignatureBlock :: Block wrapSignatureBlock = mixfixSignatureBlock "wrap_signature" wrapSym ["A"] diff --git a/test/examples/inductive.tex b/test/examples/inductive.tex index 30a259f..20c1aa7 100644 --- a/test/examples/inductive.tex +++ b/test/examples/inductive.tex @@ -1,8 +1,8 @@ % Compact inductive examples covering derived facts and soundness tasks -\begin{definition}\label{subseteq} - $A\subseteq B$ iff $A = B$. -\end{definition} +% Generated inductive subset facts are expanded elementwise by the checker. +% +% \begin{axiom}\label{pow} $\pow{A} = \emptyset$. diff --git a/test/golden/inductive/encoding tasks.golden b/test/golden/inductive/encoding tasks.golden index 07b8a35..7b43660 100644 --- a/test/golden/inductive/encoding tasks.golden +++ b/test/golden/inductive/encoding tasks.golden @@ -3,40 +3,36 @@ fof(everything_in_emptyset,axiom,![Xx]:elem(Xx,emptyset)). fof(wrap,axiom,![XA]:wrap(XA)=emptyset). fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). fof(pow,axiom,![XA]:pow(XA)=emptyset). -fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). ------------------ fof(fin,conjecture,![Xa,XA,XB]:((elem(Xa,XA)&elem(XB,pow(XA)))=>elem(cons(Xa,XB),pow(XA))),"test/examples/inductive.tex 23:1"). fof(everything_in_emptyset,axiom,![Xx]:elem(Xx,emptyset)). fof(wrap,axiom,![XA]:wrap(XA)=emptyset). fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). fof(pow,axiom,![XA]:pow(XA)=emptyset). -fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). ------------------ fof(fin_intro_ref,conjecture,elem(emptyset,fin(fA)),"test/examples/inductive.tex 35:5"). fof(fin_intro_1,axiom,![XA]:elem(emptyset,fin(XA))). ------------------ -fof(acc,conjecture,![Xxa,Xxb]:(subseteq(Xxa,Xxb)=>subseteq(wrap(Xxa),wrap(Xxb))),"test/examples/inductive.tex 38:1"). +fof(acc,conjecture,![Xxa,Xxb]:(![Xx1]:(elem(Xx1,Xxa)=>elem(Xx1,Xxb))=>![Xx1]:(elem(Xx1,wrap(Xxa))=>elem(Xx1,wrap(Xxb)))),"test/examples/inductive.tex 38:1"). fof(fin_intro_ref,axiom,![XA]:elem(emptyset,fin(XA))). fof(fin_intro_1,axiom,![XA]:elem(emptyset,fin(XA))). fof(fin_intro_2,axiom,![Xa,XA,XB]:((elem(Xa,XA)&elem(XB,fin(XA)))=>elem(cons(Xa,XB),fin(XA)))). -fof(fin_dom_subset,axiom,![XA]:subseteq(fin(XA),pow(XA))). +fof(fin_dom_subset,axiom,![XA]:![Xx]:(elem(Xx,fin(XA))=>elem(Xx,pow(XA)))). fof(fin_cases,axiom,![Xx,XA]:(elem(Xx,fin(XA))=>(Xx=emptyset|?[Xa,XB]:(elem(Xa,XA)&elem(XB,fin(XA))&Xx=cons(Xa,XB))))). -fof(fin_induct,axiom,![XS,XA]:((elem(emptyset,XS)&![Xa,XB]:((elem(Xa,XA)&elem(XB,XS))=>elem(cons(Xa,XB),XS)))=>subseteq(fin(XA),XS))). +fof(fin_induct,axiom,![XS,XA]:((elem(emptyset,XS)&![Xa,XB]:((elem(Xa,XA)&elem(XB,XS))=>elem(cons(Xa,XB),XS)))=>![Xx]:(elem(Xx,fin(XA))=>elem(Xx,XS)))). fof(everything_in_emptyset,axiom,![Xx]:elem(Xx,emptyset)). fof(wrap,axiom,![XA]:wrap(XA)=emptyset). fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). fof(pow,axiom,![XA]:pow(XA)=emptyset). -fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)). ------------------ fof(acc,conjecture,![Xx,XR]:(elem(Xx,wrap(wrap(XR)))=>elem(Xx,wrap(XR))),"test/examples/inductive.tex 38:1"). fof(fin_intro_ref,axiom,![XA]:elem(emptyset,fin(XA))). fof(fin_intro_1,axiom,![XA]:elem(emptyset,fin(XA))). fof(fin_intro_2,axiom,![Xa,XA,XB]:((elem(Xa,XA)&elem(XB,fin(XA)))=>elem(cons(Xa,XB),fin(XA)))). -fof(fin_dom_subset,axiom,![XA]:subseteq(fin(XA),pow(XA))). +fof(fin_dom_subset,axiom,![XA]:![Xx]:(elem(Xx,fin(XA))=>elem(Xx,pow(XA)))). fof(fin_cases,axiom,![Xx,XA]:(elem(Xx,fin(XA))=>(Xx=emptyset|?[Xa,XB]:(elem(Xa,XA)&elem(XB,fin(XA))&Xx=cons(Xa,XB))))). -fof(fin_induct,axiom,![XS,XA]:((elem(emptyset,XS)&![Xa,XB]:((elem(Xa,XA)&elem(XB,XS))=>elem(cons(Xa,XB),XS)))=>subseteq(fin(XA),XS))). +fof(fin_induct,axiom,![XS,XA]:((elem(emptyset,XS)&![Xa,XB]:((elem(Xa,XA)&elem(XB,XS))=>elem(cons(Xa,XB),XS)))=>![Xx]:(elem(Xx,fin(XA))=>elem(Xx,XS)))). fof(everything_in_emptyset,axiom,![Xx]:elem(Xx,emptyset)). fof(wrap,axiom,![XA]:wrap(XA)=emptyset). fof(cons,axiom,![Xa,XB]:cons(Xa,XB)=emptyset). -fof(pow,axiom,![XA]:pow(XA)=emptyset). -fof(subseteq,axiom,![XA,XB]:(subseteq(XA,XB)<=>XA=XB)).
\ No newline at end of file +fof(pow,axiom,![XA]:pow(XA)=emptyset).
\ No newline at end of file diff --git a/test/golden/inductive/generating tasks.golden b/test/golden/inductive/generating tasks.golden index a045cb7..754ae86 100644 --- a/test/golden/inductive/generating tasks.golden +++ b/test/golden/inductive/generating tasks.golden @@ -224,73 +224,6 @@ ] ) ) - , Hypothesis Marker "subseteq" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/inductive.tex" - , locLine = 3 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "subseteq" ) - ( Marker "subseteq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "A" ) - ) - , TermVar - ( B - ( NamedVar "B" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/inductive.tex" - , locLine = 4 - , locColumn = 27 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "A" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "B" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) ] , taskConjectureLabel = Marker "fin" , taskLocation = Location @@ -583,73 +516,6 @@ ] ) ) - , Hypothesis Marker "subseteq" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/inductive.tex" - , locLine = 3 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "subseteq" ) - ( Marker "subseteq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "A" ) - ) - , TermVar - ( B - ( NamedVar "B" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/inductive.tex" - , locLine = 4 - , locColumn = 27 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "A" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "B" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) ] , taskConjectureLabel = Marker "fin" , taskLocation = Location @@ -1198,68 +1064,107 @@ ) , Hypothesis Marker "fin_dom_subset" Quantified Universally ( Scope - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "subseteq" ) - ( Marker "subseteq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "fin" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ( Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( Location + { locFile = "<nowhere>" + , locLine = -1 + , locColumn = -1 + } + ) + ( SymbolPredicate + ( PredicateRelation + ( RelationSymbol + ( Command "in" ) + ( Marker "elem" ) + ) ) ) - ( Marker "fin" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "A" ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermSymbol + ( Location + { locFile = "<nowhere>" + , locLine = -1 + , locColumn = -1 + } + ) + ( SymbolMixfix + ( MixfixItem + ( TokenCons + ( Command "fin" ) + ( TokenCons InvisibleBraceL + ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ) + ) + ( Marker "fin" ) NonAssoc + ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + ] + ] ) - ] - , TermSymbol - ( Location - { locFile = "test/examples/inductive.tex" - , locLine = 24 - , locColumn = 29 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "pow" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ( TermSymbol + ( Location + { locFile = "<nowhere>" + , locLine = -1 + , locColumn = -1 + } + ) + ( SymbolPredicate + ( PredicateRelation + ( RelationSymbol + ( Command "in" ) + ( Marker "elem" ) + ) ) ) - ( Marker "pow" ) NonAssoc + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermSymbol + ( Location + { locFile = "test/examples/inductive.tex" + , locLine = 24 + , locColumn = 29 + } + ) + ( SymbolMixfix + ( MixfixItem + ( TokenCons + ( Command "pow" ) + ( TokenCons InvisibleBraceL + ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ) + ) + ( Marker "pow" ) NonAssoc + ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + ] + ] ) ) - [ TermVar - ( B - ( NamedVar "A" ) - ) - ] - ] + ) ) ) , Hypothesis Marker "fin_cases" Quantified Universally @@ -1657,49 +1562,88 @@ ) ) ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "subseteq" ) - ( Marker "subseteq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "fin" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ( Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( Location + { locFile = "<nowhere>" + , locLine = -1 + , locColumn = -1 + } + ) + ( SymbolPredicate + ( PredicateRelation + ( RelationSymbol + ( Command "in" ) + ( Marker "elem" ) + ) ) ) - ( Marker "fin" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "A" ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermSymbol + ( Location + { locFile = "<nowhere>" + , locLine = -1 + , locColumn = -1 + } + ) + ( SymbolMixfix + ( MixfixItem + ( TokenCons + ( Command "fin" ) + ( TokenCons InvisibleBraceL + ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ) + ) + ( Marker "fin" ) NonAssoc + ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + ] + ] + ) + ( TermSymbol + ( Location + { locFile = "<nowhere>" + , locLine = -1 + , locColumn = -1 + } + ) + ( SymbolPredicate + ( PredicateRelation + ( RelationSymbol + ( Command "in" ) + ( Marker "elem" ) + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "S" ) + ) + ) + ) + ] ) - ] - , TermVar - ( B - ( NamedVar "S" ) ) - ] + ) ) ) ) @@ -1926,64 +1870,72 @@ ] ) ) - , Hypothesis Marker "subseteq" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/inductive.tex" - , locLine = 3 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "subseteq" ) - ( Marker "subseteq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "A" ) - ) - , TermVar - ( B - ( NamedVar "B" ) - ) - ] - ) - ( Quantified Universally - ( Scope + ] + , taskConjectureLabel = Marker "acc" + , taskLocation = Location + { locFile = "test/examples/inductive.tex" + , locLine = 38 + , locColumn = 1 + } + , taskConjecture = Quantified Universally + ( Scope + ( Connected Implication + ( Quantified Universally + ( Scope + ( Connected Implication ( TermSymbol ( Location - { locFile = "test/examples/inductive.tex" - , locLine = 4 - , locColumn = 27 + { locFile = "<nowhere>" + , locLine = -1 + , locColumn = -1 } ) ( SymbolPredicate ( PredicateRelation ( RelationSymbol - ( Symbol "=" ) - ( Marker "eq" ) + ( Command "in" ) + ( Marker "elem" ) ) ) ) [ TermVar + ( B + ( NamedVar "x1" ) + ) + , TermVar ( F ( TermVar ( B - ( NamedVar "A" ) + ( NamedVar "xa" ) ) ) ) + ] + ) + ( TermSymbol + ( Location + { locFile = "<nowhere>" + , locLine = -1 + , locColumn = -1 + } + ) + ( SymbolPredicate + ( PredicateRelation + ( RelationSymbol + ( Command "in" ) + ( Marker "elem" ) + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x1" ) + ) , TermVar ( F ( TermVar ( B - ( NamedVar "B" ) + ( NamedVar "xb" ) ) ) ) @@ -1992,104 +1944,107 @@ ) ) ) - ) - ] - , taskConjectureLabel = Marker "acc" - , taskLocation = Location - { locFile = "test/examples/inductive.tex" - , locLine = 38 - , locColumn = 1 - } - , taskConjecture = Quantified Universally - ( Scope - ( Connected Implication - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "subseteq" ) - ( Marker "subseteq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "xa" ) - ) - , TermVar - ( B - ( NamedVar "xb" ) - ) - ] - ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "subseteq" ) - ( Marker "subseteq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "test/examples/inductive.tex" - , locLine = 41 - , locColumn = 23 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "wrap" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ( Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( Location + { locFile = "<nowhere>" + , locLine = -1 + , locColumn = -1 + } + ) + ( SymbolPredicate + ( PredicateRelation + ( RelationSymbol + ( Command "in" ) + ( Marker "elem" ) + ) ) ) - ( Marker "wrap" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "xa" ) + [ TermVar + ( B + ( NamedVar "x1" ) + ) + , TermSymbol + ( Location + { locFile = "test/examples/inductive.tex" + , locLine = 41 + , locColumn = 23 + } + ) + ( SymbolMixfix + ( MixfixItem + ( TokenCons + ( Command "wrap" ) + ( TokenCons InvisibleBraceL + ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ) + ) + ( Marker "wrap" ) NonAssoc + ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "xa" ) + ) + ) + ) + ] + ] ) - ] - , TermSymbol - ( Location - { locFile = "test/examples/inductive.tex" - , locLine = 41 - , locColumn = 23 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "wrap" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ( TermSymbol + ( Location + { locFile = "<nowhere>" + , locLine = -1 + , locColumn = -1 + } + ) + ( SymbolPredicate + ( PredicateRelation + ( RelationSymbol + ( Command "in" ) + ( Marker "elem" ) + ) ) ) - ( Marker "wrap" ) NonAssoc + [ TermVar + ( B + ( NamedVar "x1" ) + ) + , TermSymbol + ( Location + { locFile = "test/examples/inductive.tex" + , locLine = 41 + , locColumn = 23 + } + ) + ( SymbolMixfix + ( MixfixItem + ( TokenCons + ( Command "wrap" ) + ( TokenCons InvisibleBraceL + ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ) + ) + ( Marker "wrap" ) NonAssoc + ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "xb" ) + ) + ) + ) + ] + ] ) ) - [ TermVar - ( B - ( NamedVar "xb" ) - ) - ] - ] + ) ) ) ) @@ -2364,68 +2319,107 @@ ) , Hypothesis Marker "fin_dom_subset" Quantified Universally ( Scope - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "subseteq" ) - ( Marker "subseteq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "fin" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ( Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( Location + { locFile = "<nowhere>" + , locLine = -1 + , locColumn = -1 + } + ) + ( SymbolPredicate + ( PredicateRelation + ( RelationSymbol + ( Command "in" ) + ( Marker "elem" ) + ) ) ) - ( Marker "fin" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "A" ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermSymbol + ( Location + { locFile = "<nowhere>" + , locLine = -1 + , locColumn = -1 + } + ) + ( SymbolMixfix + ( MixfixItem + ( TokenCons + ( Command "fin" ) + ( TokenCons InvisibleBraceL + ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ) + ) + ( Marker "fin" ) NonAssoc + ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + ] + ] ) - ] - , TermSymbol - ( Location - { locFile = "test/examples/inductive.tex" - , locLine = 24 - , locColumn = 29 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "pow" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ( TermSymbol + ( Location + { locFile = "<nowhere>" + , locLine = -1 + , locColumn = -1 + } + ) + ( SymbolPredicate + ( PredicateRelation + ( RelationSymbol + ( Command "in" ) + ( Marker "elem" ) + ) ) ) - ( Marker "pow" ) NonAssoc + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermSymbol + ( Location + { locFile = "test/examples/inductive.tex" + , locLine = 24 + , locColumn = 29 + } + ) + ( SymbolMixfix + ( MixfixItem + ( TokenCons + ( Command "pow" ) + ( TokenCons InvisibleBraceL + ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ) + ) + ( Marker "pow" ) NonAssoc + ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + ] + ] ) ) - [ TermVar - ( B - ( NamedVar "A" ) - ) - ] - ] + ) ) ) , Hypothesis Marker "fin_cases" Quantified Universally @@ -2823,49 +2817,88 @@ ) ) ) - ( TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "subseteq" ) - ( Marker "subseteq" ) - ) - ) - ) - [ TermSymbol - ( Location - { locFile = "<nowhere>" - , locLine = -1 - , locColumn = -1 - } - ) - ( SymbolMixfix - ( MixfixItem - ( TokenCons - ( Command "fin" ) - ( TokenCons InvisibleBraceL - ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ( Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( Location + { locFile = "<nowhere>" + , locLine = -1 + , locColumn = -1 + } + ) + ( SymbolPredicate + ( PredicateRelation + ( RelationSymbol + ( Command "in" ) + ( Marker "elem" ) + ) ) ) - ( Marker "fin" ) NonAssoc - ) - ) - [ TermVar - ( B - ( NamedVar "A" ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermSymbol + ( Location + { locFile = "<nowhere>" + , locLine = -1 + , locColumn = -1 + } + ) + ( SymbolMixfix + ( MixfixItem + ( TokenCons + ( Command "fin" ) + ( TokenCons InvisibleBraceL + ( HoleCons ( TokenCons InvisibleBraceR End ) ) + ) + ) + ( Marker "fin" ) NonAssoc + ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + ] + ] + ) + ( TermSymbol + ( Location + { locFile = "<nowhere>" + , locLine = -1 + , locColumn = -1 + } + ) + ( SymbolPredicate + ( PredicateRelation + ( RelationSymbol + ( Command "in" ) + ( Marker "elem" ) + ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "S" ) + ) + ) + ) + ] ) - ] - , TermVar - ( B - ( NamedVar "S" ) ) - ] + ) ) ) ) @@ -3092,73 +3125,6 @@ ] ) ) - , Hypothesis Marker "subseteq" Quantified Universally - ( Scope - ( Connected Equivalence - ( TermSymbol - ( Location - { locFile = "test/examples/inductive.tex" - , locLine = 3 - , locColumn = 1 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Command "subseteq" ) - ( Marker "subseteq" ) - ) - ) - ) - [ TermVar - ( B - ( NamedVar "A" ) - ) - , TermVar - ( B - ( NamedVar "B" ) - ) - ] - ) - ( Quantified Universally - ( Scope - ( TermSymbol - ( Location - { locFile = "test/examples/inductive.tex" - , locLine = 4 - , locColumn = 27 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( F - ( TermVar - ( B - ( NamedVar "A" ) - ) - ) - ) - , TermVar - ( F - ( TermVar - ( B - ( NamedVar "B" ) - ) - ) - ) - ] - ) - ) - ) - ) - ) ] , taskConjectureLabel = Marker "acc" , taskLocation = Location diff --git a/test/golden/inductive/glossing.golden b/test/golden/inductive/glossing.golden index 5063187..7d3ee93 100644 --- a/test/golden/inductive/glossing.golden +++ b/test/golden/inductive/glossing.golden @@ -1,44 +1,4 @@ -[ BlockDefn - ( Location - { locFile = "test/examples/inductive.tex" - , locLine = 3 - , locColumn = 1 - } - ) - ( Marker "subseteq" ) - ( DefnPredicate [] - ( PredicateRelation - ( RelationSymbol - ( Command "subseteq" ) - ( Marker "subseteq" ) - ) - ) - ( NamedVar "A" :| - [ NamedVar "B" ] - ) - ( TermSymbol - ( Location - { locFile = "test/examples/inductive.tex" - , locLine = 4 - , locColumn = 27 - } - ) - ( SymbolPredicate - ( PredicateRelation - ( RelationSymbol - ( Symbol "=" ) - ( Marker "eq" ) - ) - ) - ) - [ TermVar - ( NamedVar "A" ) - , TermVar - ( NamedVar "B" ) - ] - ) - ) -, BlockAxiom +[ BlockAxiom ( Location { locFile = "test/examples/inductive.tex" , locLine = 7 diff --git a/test/golden/inductive/parsing.golden b/test/golden/inductive/parsing.golden index 2a9dc9d..b027d60 100644 --- a/test/golden/inductive/parsing.golden +++ b/test/golden/inductive/parsing.golden @@ -1,46 +1,4 @@ -[ BlockDefn - ( Location - { locFile = "test/examples/inductive.tex" - , locLine = 3 - , locColumn = 1 - } - ) Nothing - ( Marker "subseteq" ) - ( Defn [] - ( DefnRel - ( NamedVar "A" ) - ( RelationSymbol - ( Command "subseteq" ) - ( Marker "subseteq" ) - ) [] - ( NamedVar "B" ) - ) - ( StmtFormula - { formula = FormulaChain - ( ChainBase - ( ExprVar - ( NamedVar "A" ) :| [] - ) Positive - ( Relation - ( Location - { locFile = "test/examples/inductive.tex" - , locLine = 4 - , locColumn = 27 - } - ) - ( RelationSymbol - ( Symbol "=" ) - ( Marker "eq" ) - ) [] - ) - ( ExprVar - ( NamedVar "B" ) :| [] - ) - ) - } - ) - ) -, BlockAxiom +[ BlockAxiom ( Location { locFile = "test/examples/inductive.tex" , locLine = 7 diff --git a/test/golden/inductive/scanning.golden b/test/golden/inductive/scanning.golden index 603902f..28c82d8 100644 --- a/test/golden/inductive/scanning.golden +++ b/test/golden/inductive/scanning.golden @@ -1,7 +1,4 @@ -[ ScanRelationSymbol - ( Command "subseteq" ) - ( Marker "subseteq" ) -, ScanFunctionSymbol +[ ScanFunctionSymbol ( TokenCons ( Command "wrap" ) ( TokenCons InvisibleBraceL diff --git a/test/golden/inductive/tokenizing.golden b/test/golden/inductive/tokenizing.golden index 6549faa..28527ec 100644 --- a/test/golden/inductive/tokenizing.golden +++ b/test/golden/inductive/tokenizing.golden @@ -1,21 +1,4 @@ [ - [ BeginEnv "definition" - , Label "subseteq" - , BeginEnv "math" - , Variable "A" - , Command "subseteq" - , Variable "B" - , EndEnv "math" - , Word "iff" - , BeginEnv "math" - , Variable "A" - , Symbol "=" - , Variable "B" - , EndEnv "math" - , Symbol "." - , EndEnv "definition" - ] -, [ BeginEnv "axiom" , Label "pow" , BeginEnv "math" |