Skip to content

Commit

Permalink
[ test ] Fix print golden values
Browse files Browse the repository at this point in the history
  • Loading branch information
@buzden
buzden committed Oct 31, 2023
1 parent a778212 commit 6edf3fc
Show file tree
Hide file tree
Showing 17 changed files with 1,898 additions and 1,898 deletions.
24 changes: 12 additions & 12 deletions tests/derivation/infra/ext print 004/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,34 +15,34 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel)
IClaim MW
Export
[]
(MkTy <Prelude.Types.Nat>[]
(MkTy <AlternativeCore.X'S>[0]
(IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel)
-> (MW ExplicitArg {arg:5277} : IVar Prelude.Types.Nat)
-> (IApp. IVar Test.DepTyCheck.Gen.Gen
$ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty
$ IVar Prelude.Types.Nat)))
$ (IApp. IVar AlternativeCore.X'S
$ IVar {arg:5277}))))
IClaim MW
Export
[]
(MkTy <AlternativeCore.X'S>[0]
(MkTy <Prelude.Types.Nat>[]
(IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel)
-> (MW ExplicitArg {arg:5277} : IVar Prelude.Types.Nat)
-> (IApp. IVar Test.DepTyCheck.Gen.Gen
$ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty
$ (IApp. IVar AlternativeCore.X'S
$ IVar {arg:5277}))))
IDef <Prelude.Types.Nat>[]
[ PatClause (IApp. IVar <Prelude.Types.Nat>[] $ IBindVar fuel)
$ IVar Prelude.Types.Nat)))
IDef <AlternativeCore.X'S>[0]
[ PatClause (IApp. IVar <AlternativeCore.X'S>[0]
$ IBindVar fuel
$ Implicit True)
(IApp. IVar <*>
$ (IApp. IVar <$>
$ IVar MkXSN
$ (IApp. IVar external^<^prim^.String>[]
$ IVar ^outmost-fuel^))
$ (IApp. IVar <Prelude.Types.Nat>[]
$ IVar fuel)) ]
IDef <AlternativeCore.X'S>[0]
[ PatClause (IApp. IVar <AlternativeCore.X'S>[0]
$ IBindVar fuel
$ Implicit True)
IDef <Prelude.Types.Nat>[]
[ PatClause (IApp. IVar <Prelude.Types.Nat>[] $ IBindVar fuel)
(IApp. IVar <*>
$ (IApp. IVar <$>
$ IVar MkXSN
Expand Down
124 changes: 62 additions & 62 deletions tests/derivation/least-effort/print/adt/004 noparam/expected
View file

Large diffs are not rendered by default.

92 changes: 46 additions & 46 deletions tests/derivation/least-effort/print/adt/006 param/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,14 +5,6 @@ LOG gen.auto.derive.infra:0: type: (arg : Fuel) -> Gen MaybeEmpty (n : Nat ** X
LOG gen.auto.derive.infra:0:
ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel)
=> ILocal (IApp. IVar <DerivedGen.X>[] $ IVar ^outmost-fuel^)
IClaim MW
Export
[]
(MkTy <Prelude.Types.Nat>[]
(IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel)
-> (IApp. IVar Test.DepTyCheck.Gen.Gen
$ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty
$ IVar Prelude.Types.Nat)))
IClaim MW
Export
[]
Expand All @@ -25,6 +17,52 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel)
$ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat)
=> (IApp. IVar DerivedGen.X
$ IVar {arg:3630}))))))
IClaim MW
Export
[]
(MkTy <Prelude.Types.Nat>[]
(IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel)
-> (IApp. IVar Test.DepTyCheck.Gen.Gen
$ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty
$ IVar Prelude.Types.Nat)))
IDef <DerivedGen.X>[]
[ PatClause (IApp. IVar <DerivedGen.X>[] $ IBindVar ^fuel_arg^)
(ILocal (IApp. IVar Test.DepTyCheck.Gen.label
$ (IApp. IVar fromString
$ IPrimVal DerivedGen.X[] (non-recursive))
$ (IApp. IVar <<DerivedGen.MkX>>
$ IVar ^fuel_arg^)))
IClaim MW
Export
[]
(MkTy <<DerivedGen.MkX>>
(IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel)
-> (IApp. IVar Test.DepTyCheck.Gen.Gen
$ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty
$ (IApp. IVar Builtin.DPair.DPair
$ IVar Prelude.Types.Nat
$ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat)
=> (IApp. IVar DerivedGen.X
$ IVar {arg:3630}))))))
IDef <<DerivedGen.MkX>>
[ PatClause (IApp. IVar <<DerivedGen.MkX>>
$ IBindVar ^cons_fuel^)
(IApp. IVar Test.DepTyCheck.Gen.label
$ (IApp. IVar fromString
$ IPrimVal DerivedGen.MkX (orders))
$ (IApp. IVar >>=
$ (IApp. IVar <Prelude.Types.Nat>[]
$ IVar ^outmost-fuel^)
$ (ILam. (MW ExplicitArg n : Implicit False)
=> (IApp. INamedApp (IVar Prelude.pure)
f
(IApp. IVar Test.DepTyCheck.Gen.Gen
$ Implicit True)
$ (IApp. IVar Builtin.DPair.MkDPair
$ Implicit True
$ INamedApp (IVar DerivedGen.MkX)
n
(IVar n)))))) ] ]
IDef <Prelude.Types.Nat>[]
[ PatClause (IApp. IVar <Prelude.Types.Nat>[]
$ IBindVar ^fuel_arg^)
Expand Down Expand Up @@ -97,41 +135,3 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel)
$ Implicit True)
$ (IApp. IVar Prelude.Types.S
$ IVar ^bnd^{arg:651}))))) ] ]
IDef <DerivedGen.X>[]
[ PatClause (IApp. IVar <DerivedGen.X>[] $ IBindVar ^fuel_arg^)
(ILocal (IApp. IVar Test.DepTyCheck.Gen.label
$ (IApp. IVar fromString
$ IPrimVal DerivedGen.X[] (non-recursive))
$ (IApp. IVar <<DerivedGen.MkX>>
$ IVar ^fuel_arg^)))
IClaim MW
Export
[]
(MkTy <<DerivedGen.MkX>>
(IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel)
-> (IApp. IVar Test.DepTyCheck.Gen.Gen
$ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty
$ (IApp. IVar Builtin.DPair.DPair
$ IVar Prelude.Types.Nat
$ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat)
=> (IApp. IVar DerivedGen.X
$ IVar {arg:3630}))))))
IDef <<DerivedGen.MkX>>
[ PatClause (IApp. IVar <<DerivedGen.MkX>>
$ IBindVar ^cons_fuel^)
(IApp. IVar Test.DepTyCheck.Gen.label
$ (IApp. IVar fromString
$ IPrimVal DerivedGen.MkX (orders))
$ (IApp. IVar >>=
$ (IApp. IVar <Prelude.Types.Nat>[]
$ IVar ^outmost-fuel^)
$ (ILam. (MW ExplicitArg n : Implicit False)
=> (IApp. INamedApp (IVar Prelude.pure)
f
(IApp. IVar Test.DepTyCheck.Gen.Gen
$ Implicit True)
$ (IApp. IVar Builtin.DPair.MkDPair
$ Implicit True
$ INamedApp (IVar DerivedGen.MkX)
n
(IVar n)))))) ] ]
Loading

0 comments on commit 6edf3fc

Please sign in to comment.