diff options
Diffstat (limited to 'test/golden/replace')
| -rw-r--r-- | test/golden/replace/encoding tasks.golden | 17 | ||||
| -rw-r--r-- | test/golden/replace/generating tasks.golden | 1378 | ||||
| -rw-r--r-- | test/golden/replace/glossing.golden | 350 | ||||
| -rw-r--r-- | test/golden/replace/parsing.golden | 304 | ||||
| -rw-r--r-- | test/golden/replace/scanning.golden | 21 | ||||
| -rw-r--r-- | test/golden/replace/tokenizing.golden | 129 | ||||
| -rw-r--r-- | test/golden/replace/verification.golden | 1 |
7 files changed, 2200 insertions, 0 deletions
diff --git a/test/golden/replace/encoding tasks.golden b/test/golden/replace/encoding tasks.golden new file mode 100644 index 0000000..a939ff9 --- /dev/null +++ b/test/golden/replace/encoding tasks.golden @@ -0,0 +1,17 @@ +fof(pair_emptyset_in_times_unit,conjecture,elem(pair(emptyset,emptyset),times(unit,unit))). +fof(unit,axiom,![Xany]:(elem(Xany,unit)<=>(elem(Xany,emptyset)|Xany=emptyset))). +fof(times,axiom,![XA,XB]:![Xfrv]:(elem(Xfrv,times(XA,XB))<=>?[Xa,Xb]:(elem(Xa,XA)&elem(Xb,XB)&pair(Xa,Xb)=Xfrv))). +fof(cons,axiom,![Xx,Xy,XX]:(elem(Xx,cons(Xy,XX))<=>(Xx=Xy|elem(Xx,XX)))). +------------------ +fof(suc,conjecture,![X0]:(elem(X0,fa)=>![X1,X2]:((X1=cons(X0,emptyset)&X2=cons(X0,emptyset))=>X1=X2))). +fof(pair_emptyset_in_times_unit,axiom,elem(pair(emptyset,emptyset),times(unit,unit))). +fof(unit,axiom,![Xany]:(elem(Xany,unit)<=>(elem(Xany,emptyset)|Xany=emptyset))). +fof(times,axiom,![XA,XB]:![Xfrv]:(elem(Xfrv,times(XA,XB))<=>?[Xa,Xb]:(elem(Xa,XA)&elem(Xb,XB)&pair(Xa,Xb)=Xfrv))). +fof(cons,axiom,![Xx,Xy,XX]:(elem(Xx,cons(Xy,XX))<=>(Xx=Xy|elem(Xx,XX)))). +------------------ +fof(times_replacement_test,conjecture,![Xfrv]:(elem(Xfrv,times(fA,fB))<=>?[Xa,Xb]:(elem(Xa,fA)&elem(Xb,fB)&pair(Xa,Xb)=Xfrv))). +fof(suc,axiom,![X1,Xa]:(elem(X1,suc(Xa))<=>?[X0]:(elem(X0,Xa)&X1=cons(X0,emptyset)))). +fof(pair_emptyset_in_times_unit,axiom,elem(pair(emptyset,emptyset),times(unit,unit))). +fof(unit,axiom,![Xany]:(elem(Xany,unit)<=>(elem(Xany,emptyset)|Xany=emptyset))). +fof(times,axiom,![XA,XB]:![Xfrv]:(elem(Xfrv,times(XA,XB))<=>?[Xa,Xb]:(elem(Xa,XA)&elem(Xb,XB)&pair(Xa,Xb)=Xfrv))). +fof(cons,axiom,![Xx,Xy,XX]:(elem(Xx,cons(Xy,XX))<=>(Xx=Xy|elem(Xx,XX)))).
\ No newline at end of file diff --git a/test/golden/replace/generating tasks.golden b/test/golden/replace/generating tasks.golden new file mode 100644 index 0000000..2d8fc5d --- /dev/null +++ b/test/golden/replace/generating tasks.golden @@ -0,0 +1,1378 @@ +[ Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "unit" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "any" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "unit" ) + ] + ) [] + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "any" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "any" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + ) + ) + , + ( Marker "times" + , Quantified Universally + ( Scope + ( Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "frv" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "B" ) + ) + ) + ) + ] + ] + ) + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( F + ( TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( F + ( TermVar + ( F + ( TermVar + ( B + ( NamedVar "B" ) + ) + ) + ) + ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "frv" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "cons" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "X" ) + ) + ] + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "X" ) + ) + ] + ) + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "pair_emptyset_in_times_unit" + , taskConjecture = TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "unit" ) + ] + ) [] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "unit" ) + ] + ) [] + ] + ] + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "pair_emptyset_in_times_unit" + , TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "unit" ) + ] + ) [] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "unit" ) + ] + ) [] + ] + ] + ) + , + ( Marker "unit" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "any" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "unit" ) + ] + ) [] + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "any" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "any" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + ) + ) + , + ( Marker "times" + , Quantified Universally + ( Scope + ( Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "frv" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "B" ) + ) + ) + ) + ] + ] + ) + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( F + ( TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( F + ( TermVar + ( F + ( TermVar + ( B + ( NamedVar "B" ) + ) + ) + ) + ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "frv" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "cons" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "X" ) + ) + ] + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "X" ) + ) + ] + ) + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "suc" + , taskConjecture = Quantified Universally + ( Scope + ( Connected Implication + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( FreshVar 0 ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "a" ) + ) + ) + ] + ) + ( Quantified Universally + ( Scope + ( Connected Implication + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( FreshVar 1 ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( F + ( TermVar + ( B + ( FreshVar 0 ) + ) + ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( FreshVar 2 ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( F + ( TermVar + ( B + ( FreshVar 0 ) + ) + ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( FreshVar 1 ) + ) + , TermVar + ( B + ( FreshVar 2 ) + ) + ] + ) + ) + ) + ) + ) + ) + } +, Task + { taskDirectness = Direct + , taskHypotheses = + [ + ( Marker "suc" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( FreshVar 1 ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "suc" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + ] + ] + ) + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( FreshVar 0 ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "a" ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( F + ( TermVar + ( B + ( FreshVar 1 ) + ) + ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( FreshVar 0 ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ] + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "pair_emptyset_in_times_unit" + , TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "unit" ) + ] + ) [] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "unit" ) + ] + ) [] + ] + ] + ) + , + ( Marker "unit" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "any" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "unit" ) + ] + ) [] + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "any" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "any" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) + ) + ) + ) + , + ( Marker "times" + , Quantified Universally + ( Scope + ( Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "frv" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "B" ) + ) + ) + ) + ] + ] + ) + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( F + ( TermVar + ( F + ( TermVar + ( B + ( NamedVar "A" ) + ) + ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( F + ( TermVar + ( F + ( TermVar + ( B + ( NamedVar "B" ) + ) + ) + ) + ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "frv" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + ) + ) + ) + , + ( Marker "cons" + , Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "y" ) + ) + , TermVar + ( B + ( NamedVar "X" ) + ) + ] + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "y" ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "x" ) + ) + , TermVar + ( B + ( NamedVar "X" ) + ) + ] + ) + ) + ) + ) + ) + ] + , taskConjectureLabel = Marker "times_replacement_test" + , taskConjecture = Quantified Universally + ( Scope + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "frv" ) + ) + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + , TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + ] + ] + ) + ( Quantified Existentially + ( Scope + ( Connected Conjunction + ( Connected Conjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( F + ( TermVar + ( F + ( TermVar + ( NamedVar "A" ) + ) + ) + ) + ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( B + ( NamedVar "b" ) + ) + , TermVar + ( F + ( TermVar + ( F + ( TermVar + ( NamedVar "B" ) + ) + ) + ) + ) + ] + ) + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + , TermVar + ( F + ( TermVar + ( B + ( NamedVar "frv" ) + ) + ) + ) + ] + ) + ) + ) + ) + ) + ) + } +]
\ No newline at end of file diff --git a/test/golden/replace/glossing.golden b/test/golden/replace/glossing.golden new file mode 100644 index 0000000..d6219fe --- /dev/null +++ b/test/golden/replace/glossing.golden @@ -0,0 +1,350 @@ +[ BlockAxiom + ( SourcePos + { sourceName = "test/examples/replace.tex" + , sourceLine = Pos 1 + , sourceColumn = Pos 1 + } + ) + ( Marker "cons" ) + ( Axiom [] + ( Connected Equivalence + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( NamedVar "y" ) + , TermVar + ( NamedVar "X" ) + ] + ] + ) + ( Connected Disjunction + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "y" ) + ] + ) + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermVar + ( NamedVar "x" ) + , TermVar + ( NamedVar "X" ) + ] + ) + ) + ) + ) +, BlockDefn + ( SourcePos + { sourceName = "test/examples/replace.tex" + , sourceLine = Pos 5 + , sourceColumn = Pos 1 + } + ) + ( Marker "times" ) + ( DefnOp + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + [ NamedVar "A" + , NamedVar "B" + ] + ( ReplaceFun + ( + ( NamedVar "a" + , TermVar + ( NamedVar "A" ) + ) :| + [ + ( NamedVar "b" + , TermVar + ( NamedVar "B" ) + ) + ] + ) + ( Scope + ( TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( Scope ( PropositionalConstant IsTop ) ) + ) + ) +, BlockDefn + ( SourcePos + { sourceName = "test/examples/replace.tex" + , sourceLine = Pos 9 + , sourceColumn = Pos 1 + } + ) + ( Marker "unit" ) + ( DefnOp + [ Just + ( Command "unit" ) + ] [] + ( TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/replace.tex" + , sourceLine = Pos 13 + , sourceColumn = Pos 1 + } + ) + ( Marker "pair_emptyset_in_times_unit" ) + ( Lemma [] + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Command "in" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + , TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermSymbol + ( SymbolMixfix + [ Just + ( Command "unit" ) + ] + ) [] + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "unit" ) + ] + ) [] + ] + ] + ) + ) +, BlockDefn + ( SourcePos + { sourceName = "test/examples/replace.tex" + , sourceLine = Pos 19 + , sourceColumn = Pos 1 + } + ) + ( Marker "suc" ) + ( DefnOp + [ Just + ( Command "suc" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ NamedVar "a" ] + ( ReplacePred + ( NamedVar "y" ) + ( NamedVar "x" ) + ( TermVar + ( NamedVar "a" ) + ) + ( Scope + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermVar ( B ReplacementRangeVar ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar ( B ReplacementDomVar ) + , TermSymbol + ( SymbolMixfix + [ Just + ( Command "emptyset" ) + ] + ) [] + ] + ] + ) + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/replace.tex" + , sourceLine = Pos 25 + , sourceColumn = Pos 1 + } + ) + ( Marker "times_replacement_test" ) + ( Lemma [] + ( TermSymbol + ( SymbolPredicate + ( PredicateRelation + ( Symbol "=" ) + ) + ) + [ TermSymbol + ( SymbolMixfix + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ) + [ TermVar + ( NamedVar "A" ) + , TermVar + ( NamedVar "B" ) + ] + , ReplaceFun + ( + ( NamedVar "a" + , TermVar + ( NamedVar "A" ) + ) :| + [ + ( NamedVar "b" + , TermVar + ( NamedVar "B" ) + ) + ] + ) + ( Scope + ( TermSymbol + ( SymbolMixfix + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ) + [ TermVar + ( B + ( NamedVar "a" ) + ) + , TermVar + ( B + ( NamedVar "b" ) + ) + ] + ) + ) + ( Scope ( PropositionalConstant IsTop ) ) + ] + ) + ) +]
\ No newline at end of file diff --git a/test/golden/replace/parsing.golden b/test/golden/replace/parsing.golden new file mode 100644 index 0000000..c2cd815 --- /dev/null +++ b/test/golden/replace/parsing.golden @@ -0,0 +1,304 @@ +[ BlockAxiom + ( SourcePos + { sourceName = "test/examples/replace.tex" + , sourceLine = Pos 1 + , sourceColumn = Pos 1 + } + ) + ( Marker "cons" ) + ( Axiom [] + ( StmtConnected Equivalence + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "x" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Just + ( Command "cons" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "y" ) + , ExprVar + ( NamedVar "X" ) + ] :| [] + ) + ) + ) + ) + ( StmtConnected Disjunction + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "x" ) :| [] + ) Positive + ( RelationSymbol + ( Symbol "=" ) + ) + ( ExprVar + ( NamedVar "y" ) :| [] + ) + ) + ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "x" ) :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprVar + ( NamedVar "X" ) :| [] + ) + ) + ) + ) + ) + ) + ) +, BlockDefn + ( SourcePos + { sourceName = "test/examples/replace.tex" + , sourceLine = Pos 5 + , sourceColumn = Pos 1 + } + ) + ( Marker "times" ) + ( DefnOp + ( SymbolPattern + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + [ NamedVar "A" + , NamedVar "B" + ] + ) + ( ExprReplace + ( ExprOp + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "a" ) + , ExprVar + ( NamedVar "b" ) + ] + ) + ( + ( NamedVar "a" + , ExprVar + ( NamedVar "A" ) + ) :| + [ + ( NamedVar "b" + , ExprVar + ( NamedVar "B" ) + ) + ] + ) Nothing + ) + ) +, BlockDefn + ( SourcePos + { sourceName = "test/examples/replace.tex" + , sourceLine = Pos 9 + , sourceColumn = Pos 1 + } + ) + ( Marker "unit" ) + ( DefnOp + ( SymbolPattern + [ Just + ( Command "unit" ) + ] [] + ) + ( ExprFiniteSet + ( ExprOp + [ Just + ( Command "emptyset" ) + ] [] :| [] + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/replace.tex" + , sourceLine = Pos 13 + , sourceColumn = Pos 1 + } + ) + ( Marker "pair_emptyset_in_times_unit" ) + ( Lemma [] + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprOp + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprOp + [ Just + ( Command "emptyset" ) + ] [] + , ExprOp + [ Just + ( Command "emptyset" ) + ] [] + ] :| [] + ) Positive + ( RelationSymbol + ( Command "in" ) + ) + ( ExprOp + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + [ ExprOp + [ Just + ( Command "unit" ) + ] [] + , ExprOp + [ Just + ( Command "unit" ) + ] [] + ] :| [] + ) + ) + ) + ) + ) +, BlockDefn + ( SourcePos + { sourceName = "test/examples/replace.tex" + , sourceLine = Pos 19 + , sourceColumn = Pos 1 + } + ) + ( Marker "suc" ) + ( DefnOp + ( SymbolPattern + [ Just + ( Command "suc" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ NamedVar "a" ] + ) + ( ExprReplacePred + ( NamedVar "y" ) + ( NamedVar "x" ) + ( ExprVar + ( NamedVar "a" ) + ) + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprVar + ( NamedVar "y" ) :| [] + ) Positive + ( RelationSymbol + ( Symbol "=" ) + ) + ( ExprFiniteSet + ( ExprVar + ( NamedVar "x" ) :| [] + ) :| [] + ) + ) + ) + ) + ) + ) +, BlockLemma + ( SourcePos + { sourceName = "test/examples/replace.tex" + , sourceLine = Pos 25 + , sourceColumn = Pos 1 + } + ) + ( Marker "times_replacement_test" ) + ( Lemma [] + ( StmtFormula + ( FormulaChain + ( ChainBase + ( ExprOp + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + [ ExprVar + ( NamedVar "A" ) + , ExprVar + ( NamedVar "B" ) + ] :| [] + ) Positive + ( RelationSymbol + ( Symbol "=" ) + ) + ( ExprReplace + ( ExprOp + [ Just + ( Command "pair" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + [ ExprVar + ( NamedVar "a" ) + , ExprVar + ( NamedVar "b" ) + ] + ) + ( + ( NamedVar "a" + , ExprVar + ( NamedVar "A" ) + ) :| + [ + ( NamedVar "b" + , ExprVar + ( NamedVar "B" ) + ) + ] + ) Nothing :| [] + ) + ) + ) + ) + ) +]
\ No newline at end of file diff --git a/test/golden/replace/scanning.golden b/test/golden/replace/scanning.golden new file mode 100644 index 0000000..050e544 --- /dev/null +++ b/test/golden/replace/scanning.golden @@ -0,0 +1,21 @@ +[ ScanFunctionSymbol + [ Nothing + , Just + ( Command "times" ) + , Nothing + ] + ( Marker "times" ) +, ScanFunctionSymbol + [ Just + ( Command "unit" ) + ] + ( Marker "unit" ) +, ScanFunctionSymbol + [ Just + ( Command "suc" ) + , Just InvisibleBraceL + , Nothing + , Just InvisibleBraceR + ] + ( Marker "suc" ) +]
\ No newline at end of file diff --git a/test/golden/replace/tokenizing.golden b/test/golden/replace/tokenizing.golden new file mode 100644 index 0000000..3b9f65c --- /dev/null +++ b/test/golden/replace/tokenizing.golden @@ -0,0 +1,129 @@ +[ BeginEnv "axiom" +, Label "cons" +, BeginEnv "math" +, Variable "x" +, Command "in" +, Command "cons" +, InvisibleBraceL +, Variable "y" +, InvisibleBraceR +, InvisibleBraceL +, Variable "X" +, InvisibleBraceR +, EndEnv "math" +, Word "iff" +, BeginEnv "math" +, Variable "x" +, Symbol "=" +, Variable "y" +, EndEnv "math" +, Word "or" +, BeginEnv "math" +, Variable "x" +, Command "in" +, Variable "X" +, EndEnv "math" +, Symbol "." +, EndEnv "axiom" +, BeginEnv "definition" +, Label "times" +, BeginEnv "math" +, Variable "A" +, Command "times" +, Variable "B" +, Symbol "=" +, VisibleBraceL +, ParenL +, Variable "a" +, Symbol "," +, Variable "b" +, ParenR +, Command "mid" +, Variable "a" +, Command "in" +, Variable "A" +, Symbol "," +, Variable "b" +, Command "in" +, Variable "B" +, VisibleBraceR +, EndEnv "math" +, Symbol "." +, EndEnv "definition" +, BeginEnv "definition" +, Label "unit" +, BeginEnv "math" +, Command "unit" +, Symbol "=" +, VisibleBraceL +, Command "emptyset" +, VisibleBraceR +, EndEnv "math" +, Symbol "." +, EndEnv "definition" +, BeginEnv "proposition" +, Label "pair_emptyset_in_times_unit" +, BeginEnv "math" +, ParenL +, Command "emptyset" +, Symbol "," +, Command "emptyset" +, ParenR +, Command "in" +, Command "unit" +, Command "times" +, Command "unit" +, EndEnv "math" +, Symbol "." +, EndEnv "proposition" +, BeginEnv "definition" +, Label "suc" +, BeginEnv "math" +, Command "suc" +, InvisibleBraceL +, Variable "a" +, InvisibleBraceR +, Symbol "=" +, VisibleBraceL +, Variable "y" +, Command "mid" +, Command "exists" +, Variable "x" +, Command "in" +, Variable "a" +, Symbol "." +, Variable "y" +, Symbol "=" +, VisibleBraceL +, Variable "x" +, VisibleBraceR +, VisibleBraceR +, EndEnv "math" +, Symbol "." +, EndEnv "definition" +, BeginEnv "proposition" +, Label "times_replacement_test" +, BeginEnv "math" +, Variable "A" +, Command "times" +, Variable "B" +, Symbol "=" +, VisibleBraceL +, ParenL +, Variable "a" +, Symbol "," +, Variable "b" +, ParenR +, Command "mid" +, Variable "a" +, Command "in" +, Variable "A" +, Symbol "," +, Variable "b" +, Command "in" +, Variable "B" +, VisibleBraceR +, EndEnv "math" +, Symbol "." +, EndEnv "proposition" +]
\ No newline at end of file diff --git a/test/golden/replace/verification.golden b/test/golden/replace/verification.golden new file mode 100644 index 0000000..69b9873 --- /dev/null +++ b/test/golden/replace/verification.golden @@ -0,0 +1 @@ +VerificationSuccess
\ No newline at end of file |