diff --git a/examples/sorted-list/tests/gens/print/expected b/examples/sorted-list/tests/gens/print/expected index b70dd9866..b80c26316 100644 --- a/examples/sorted-list/tests/gens/print/expected +++ b/examples/sorted-list/tests/gens/print/expected @@ -39,32 +39,12 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty SortedList Export [] (mkTy - { name = "[0]" - , type = - MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> MkArg MW ExplicitArg (Just "{arg:1}") (var "Prelude.Types.Nat") - .-> var "Test.DepTyCheck.Gen.Gen" - .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ ( var "Builtin.DPair.DPair" - .$ var "Data.List.Sorted.SortedList" - .$ ( MkArg MW ExplicitArg (Just "{arg:2}") (var "Data.List.Sorted.SortedList") - .=> var "Data.List.Sorted.FirstGT" .$ var "{arg:1}" .$ var "{arg:2}")) - }) - , IClaim - emptyFC - MW - Export - [] - (mkTy - { name = "[0]" + { name = "[0, 1]" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> var "Test.DepTyCheck.Gen.Gen" - .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ ( var "Builtin.DPair.DPair" - .$ var "Prelude.Types.Nat" - .$ (MkArg MW ExplicitArg (Just "m") (var "Prelude.Types.Nat") .=> var "Data.Nat.LTE" .$ var "n" .$ var "m")) + .-> MkArg MW ExplicitArg (Just "m") (var "Prelude.Types.Nat") + .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ (var "Data.Nat.LTE" .$ var "n" .$ var "m") }) , IClaim emptyFC @@ -230,150 +210,36 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty SortedList .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "Data.List.Sorted.NE (orders)")) .$ ( var ">>=" - .$ (var "[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "n") implicitFalse - .=> var ">>=" - .$ (var "[0]" .$ var "^outmost-fuel^" .$ (var "Prelude.Types.S" .$ var "n")) - .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse - .=> iCase - { sc = var "{lamc:0}" - , ty = implicitFalse - , clauses = - [ var "Builtin.DPair.MkDPair" .$ bindVar "x" .$ bindVar "^bnd^{arg:3}" - .= var ">>=" - .$ (var "[0]" .$ var "^cons_fuel^" .$ var "x") - .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse - .=> iCase - { sc = var "{lamc:0}" - , ty = implicitFalse - , clauses = - [ var "Builtin.DPair.MkDPair" .$ bindVar "xs" .$ bindVar "prf" - .= var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ ( var "Builtin.DPair.MkDPair" - .$ implicitTrue - .$ ( var "Builtin.DPair.MkDPair" - .$ implicitTrue - .$ ( var "Data.List.Sorted.NE" - .! ("xs", implicitTrue) - .! ("x", implicitTrue) - .! ("prf", var "prf") - .! ("n", implicitTrue) - .$ var "^bnd^{arg:3}"))) - ] - }) - ] - }))) - ] - ] - , scope = - iCase - { sc = var "^fuel_arg^" - , ty = var "Data.Fuel.Fuel" - , clauses = - [ var "Data.Fuel.Dry" - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Data.List.Sorted.FirstGT[] (dry fuel)")) - .$ (var "<>" .$ var "Data.Fuel.Dry") - , var "Data.Fuel.More" .$ bindVar "^sub^fuel_arg^" - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Data.List.Sorted.FirstGT[] (spend fuel)")) - .$ ( var "Test.DepTyCheck.Gen.frequency" - .$ ( var "::" - .$ (var "Builtin.MkPair" .$ var "Data.Nat1.one" .$ (var "<>" .$ var "^fuel_arg^")) - .$ ( var "::" - .$ ( var "Builtin.MkPair" - .$ (var "Deriving.DepTyCheck.Util.Reflection.leftDepth" .$ var "^sub^fuel_arg^") - .$ (var "<>" .$ var "^sub^fuel_arg^")) - .$ var "Nil"))) - ] - } - } - ] - , IDef - emptyFC - "[0]" - [ var "[0]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^<{arg:1}>" - .= local - { decls = - [ IClaim - emptyFC - MW - Export - [] - (mkTy - { name = "<>" - , type = - MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> MkArg MW ExplicitArg (Just "{arg:1}") (var "Prelude.Types.Nat") - .-> var "Test.DepTyCheck.Gen.Gen" - .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ ( var "Builtin.DPair.DPair" - .$ var "Data.List.Sorted.SortedList" - .$ ( MkArg MW ExplicitArg (Just "{arg:2}") (var "Data.List.Sorted.SortedList") - .=> var "Data.List.Sorted.FirstGT" .$ var "{arg:1}" .$ var "{arg:2}")) - }) - , IClaim - emptyFC - MW - Export - [] - (mkTy - { name = "<>" - , type = - MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> MkArg MW ExplicitArg (Just "{arg:1}") (var "Prelude.Types.Nat") - .-> var "Test.DepTyCheck.Gen.Gen" - .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ ( var "Builtin.DPair.DPair" - .$ var "Data.List.Sorted.SortedList" - .$ ( MkArg MW ExplicitArg (Just "{arg:2}") (var "Data.List.Sorted.SortedList") - .=> var "Data.List.Sorted.FirstGT" .$ var "{arg:1}" .$ var "{arg:2}")) - }) - , IDef - emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" .$ bindVar "n" - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Data.List.Sorted.E (orders)")) - .$ ( var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ (var "Data.List.Sorted.E" .! ("n", var "n")))) - ] - , IDef - emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" .$ bindVar "n" - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Data.List.Sorted.NE (orders)")) - .$ ( var ">>=" - .$ (var "[0]" .$ var "^outmost-fuel^" .$ (var "Prelude.Types.S" .$ var "n")) + .$ (var "[]" .$ var "^cons_fuel^") .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse .=> iCase { sc = var "{lamc:0}" , ty = implicitFalse , clauses = - [ var "Builtin.DPair.MkDPair" .$ bindVar "x" .$ bindVar "^bnd^{arg:3}" + [ var "Builtin.DPair.MkDPair" + .$ bindVar "x" + .$ (var "Builtin.DPair.MkDPair" .$ bindVar "xs" .$ bindVar "prf") .= var ">>=" - .$ (var "[0]" .$ var "^cons_fuel^" .$ var "x") - .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse - .=> iCase - { sc = var "{lamc:0}" - , ty = implicitFalse - , clauses = - [ var "Builtin.DPair.MkDPair" .$ bindVar "xs" .$ bindVar "prf" - .= var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ ( var "Builtin.DPair.MkDPair" - .$ implicitTrue - .$ ( var "Data.List.Sorted.NE" - .! ("xs", implicitTrue) - .! ("x", implicitTrue) - .! ("prf", var "prf") - .! ("n", implicitTrue) - .$ var "^bnd^{arg:3}")) - ] - }) + .$ (var "[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "n") implicitFalse + .=> var ">>=" + .$ ( var "[0, 1]" + .$ var "^outmost-fuel^" + .$ (var "Prelude.Types.S" .$ var "n") + .$ var "x") + .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:3}") implicitFalse + .=> var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ ( var "Data.List.Sorted.NE" + .! ("xs", implicitTrue) + .! ("x", implicitTrue) + .! ("prf", var "prf") + .! ("n", implicitTrue) + .$ var "^bnd^{arg:3}"))))) ] })) ] @@ -385,20 +251,18 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty SortedList , clauses = [ var "Data.Fuel.Dry" .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Data.List.Sorted.FirstGT[0] (dry fuel)")) - .$ (var "<>" .$ var "Data.Fuel.Dry" .$ var "inter^<{arg:1}>") + .$ (var "fromString" .$ primVal (Str "Data.List.Sorted.FirstGT[] (dry fuel)")) + .$ (var "<>" .$ var "Data.Fuel.Dry") , var "Data.Fuel.More" .$ bindVar "^sub^fuel_arg^" .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Data.List.Sorted.FirstGT[0] (spend fuel)")) + .$ (var "fromString" .$ primVal (Str "Data.List.Sorted.FirstGT[] (spend fuel)")) .$ ( var "Test.DepTyCheck.Gen.frequency" .$ ( var "::" - .$ ( var "Builtin.MkPair" - .$ var "Data.Nat1.one" - .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^<{arg:1}>")) + .$ (var "Builtin.MkPair" .$ var "Data.Nat1.one" .$ (var "<>" .$ var "^fuel_arg^")) .$ ( var "::" .$ ( var "Builtin.MkPair" .$ (var "Deriving.DepTyCheck.Util.Reflection.leftDepth" .$ var "^sub^fuel_arg^") - .$ (var "<>" .$ var "^sub^fuel_arg^" .$ var "inter^<{arg:1}>")) + .$ (var "<>" .$ var "^sub^fuel_arg^")) .$ var "Nil"))) ] } @@ -406,8 +270,8 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty SortedList ] , IDef emptyFC - "[0]" - [ var "[0]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^" + "[0, 1]" + [ var "[0, 1]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^" .$ bindVar "inter^" .= local { decls = [ IClaim @@ -420,12 +284,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty SortedList , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .-> MkArg MW ExplicitArg (Just "m") (var "Prelude.Types.Nat") .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ ( var "Builtin.DPair.DPair" - .$ var "Prelude.Types.Nat" - .$ ( MkArg MW ExplicitArg (Just "m") (var "Prelude.Types.Nat") - .=> var "Data.Nat.LTE" .$ var "n" .$ var "m")) + .$ (var "Data.Nat.LTE" .$ var "n" .$ var "m") }) , IClaim emptyFC @@ -437,52 +299,41 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty SortedList , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .-> MkArg MW ExplicitArg (Just "m") (var "Prelude.Types.Nat") .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ ( var "Builtin.DPair.DPair" - .$ var "Prelude.Types.Nat" - .$ ( MkArg MW ExplicitArg (Just "m") (var "Prelude.Types.Nat") - .=> var "Data.Nat.LTE" .$ var "n" .$ var "m")) + .$ (var "Data.Nat.LTE" .$ var "n" .$ var "m") }) , IDef emptyFC "<>" - [ var "<>" .$ bindVar "^cons_fuel^" .$ var "Prelude.Types.Z" + [ var "<>" .$ bindVar "^cons_fuel^" .$ var "Prelude.Types.Z" .$ bindVar "right" .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "Data.Nat.LTEZero (orders)")) - .$ ( var ">>=" - .$ (var "[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "right") implicitFalse - .=> var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ (var "Data.Nat.LTEZero" .! ("right", var "right"))))) - , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" + .$ ( var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ (var "Data.Nat.LTEZero" .! ("right", var "right"))) + , var "<>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty" ] , IDef emptyFC "<>" - [ var "<>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ bindVar "left") + [ var "<>" + .$ bindVar "^cons_fuel^" + .$ (var "Prelude.Types.S" .$ bindVar "left") + .$ (var "Prelude.Types.S" .$ bindVar "right") .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "Data.Nat.LTESucc (orders)")) .$ ( var ">>=" - .$ (var "[0]" .$ var "^cons_fuel^" .$ var "left") - .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse - .=> iCase - { sc = var "{lamc:0}" - , ty = implicitFalse - , clauses = - [ var "Builtin.DPair.MkDPair" .$ bindVar "right" .$ bindVar "^bnd^{arg:4}" - .= var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ ( var "Builtin.DPair.MkDPair" - .$ implicitTrue - .$ ( var "Data.Nat.LTESucc" - .! ("right", implicitTrue) - .! ("left", implicitTrue) - .$ var "^bnd^{arg:4}")) - ] - })) - , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" + .$ (var "[0, 1]" .$ var "^cons_fuel^" .$ var "left" .$ var "right") + .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:4}") implicitFalse + .=> var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ ( var "Data.Nat.LTESucc" + .! ("right", implicitTrue) + .! ("left", implicitTrue) + .$ var "^bnd^{arg:4}"))) + , var "<>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty" ] ] , scope = @@ -492,20 +343,20 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty SortedList , clauses = [ var "Data.Fuel.Dry" .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Data.Nat.LTE[0] (dry fuel)")) - .$ (var "<>" .$ var "Data.Fuel.Dry" .$ var "inter^") + .$ (var "fromString" .$ primVal (Str "Data.Nat.LTE[0, 1] (dry fuel)")) + .$ (var "<>" .$ var "Data.Fuel.Dry" .$ var "inter^" .$ var "inter^") , var "Data.Fuel.More" .$ bindVar "^sub^fuel_arg^" .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Data.Nat.LTE[0] (spend fuel)")) + .$ (var "fromString" .$ primVal (Str "Data.Nat.LTE[0, 1] (spend fuel)")) .$ ( var "Test.DepTyCheck.Gen.frequency" .$ ( var "::" .$ ( var "Builtin.MkPair" .$ var "Data.Nat1.one" - .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^")) + .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^" .$ var "inter^")) .$ ( var "::" .$ ( var "Builtin.MkPair" .$ (var "Deriving.DepTyCheck.Util.Reflection.leftDepth" .$ var "^sub^fuel_arg^") - .$ (var "<>" .$ var "^sub^fuel_arg^" .$ var "inter^")) + .$ (var "<>" .$ var "^sub^fuel_arg^" .$ var "inter^" .$ var "inter^")) .$ var "Nil"))) ] } diff --git a/examples/sorted-tree-indexed/tests/gens/sorted/expected b/examples/sorted-tree-indexed/tests/gens/sorted/expected index c34e9cec8..a580c7c66 100644 --- a/examples/sorted-tree-indexed/tests/gens/sorted/expected +++ b/examples/sorted-tree-indexed/tests/gens/sorted/expected @@ -1,40 +1,40 @@ -------------- -min: 0, max: 1, length: 2 -as list: [0, 1] +min: 1, max: 4, length: 2 +as list: [1, 4] sorted: True -------------- -min: 1, max: 3, length: 3 -as list: [1, 2, 3] +min: 0, max: 4, length: 5 +as list: [0, 1, 2, 3, 4] sorted: True -------------- min: 0, max: 4, length: 5 as list: [0, 1, 2, 3, 4] sorted: True -------------- -min: 0, max: 1, length: 2 -as list: [0, 1] +min: 4, max: 4, length: 1 +as list: [4] sorted: True -------------- -min: 2, max: 2, length: 1 -as list: [2] +min: 2, max: 4, length: 3 +as list: [2, 3, 4] sorted: True -------------- min: 0, max: 4, length: 5 as list: [0, 1, 2, 3, 4] sorted: True -------------- -min: 3, max: 3, length: 1 -as list: [3] +min: 0, max: 4, length: 4 +as list: [0, 2, 3, 4] sorted: True -------------- -min: 4, max: 4, length: 1 -as list: [4] +min: 2, max: 4, length: 3 +as list: [2, 3, 4] sorted: True -------------- -min: 0, max: 4, length: 5 -as list: [0, 1, 2, 3, 4] +min: 2, max: 4, length: 3 +as list: [2, 3, 4] sorted: True -------------- -min: 0, max: 3, length: 4 -as list: [0, 1, 2, 3] +min: 2, max: 2, length: 1 +as list: [2] sorted: True diff --git a/examples/uniq-list/tests/gens/uniq-list/expected b/examples/uniq-list/tests/gens/uniq-list/expected index bb3fa34d6..39a5c765d 100644 --- a/examples/uniq-list/tests/gens/uniq-list/expected +++ b/examples/uniq-list/tests/gens/uniq-list/expected @@ -5,26 +5,26 @@ uniq: True list: ["g"] uniq: True ----------- -list: ["g", "b", "f"] +list: ["b", "f", "g"] uniq: True ----------- -list: ["f", "g", "a", "d"] +list: ["g", "a", "d", "f"] uniq: True ----------- -list: ["h", "c", "g"] +list: ["c", "g", "h"] uniq: True ----------- -list: ["h", "g", "b", "d", "c"] +list: ["g", "b", "d", "c", "h"] uniq: True ----------- -list: ["c", "b"] +list: ["b", "c"] uniq: True ----------- -list: ["d", "a", "h"] +list: ["a", "h", "d"] uniq: True ----------- -list: ["g", "a", "h", "c", "d", "b", "f"] +list: ["a", "h", "c", "d", "b", "f", "g"] uniq: True ----------- -list: ["g", "c", "b", "h", "d", "f", "a"] +list: ["c", "b", "h", "d", "f", "a", "g"] uniq: True diff --git a/examples/uniq-list/tests/gens/uniq-vect-spare/expected b/examples/uniq-list/tests/gens/uniq-vect-spare/expected index b14bad6f9..005e1e87e 100644 --- a/examples/uniq-list/tests/gens/uniq-vect-spare/expected +++ b/examples/uniq-list/tests/gens/uniq-vect-spare/expected @@ -1,31 +1,31 @@ prenty of spare strings to generate from (7 for vects of length 4) ----------- -vect: ["g", "c", "a", "b"] +vect: ["c", "a", "b", "g"] uniq: True ----------- -vect: ["b", "c", "g", "a"] +vect: ["c", "g", "a", "b"] uniq: True ----------- -vect: ["b", "c", "d", "h"] +vect: ["c", "d", "h", "b"] uniq: True ----------- -vect: ["h", "g", "d", "c"] +vect: ["g", "d", "c", "h"] uniq: True ----------- -vect: ["a", "b", "g", "c"] +vect: ["b", "g", "c", "a"] uniq: True ----------- -vect: ["f", "b", "h", "g"] +vect: ["b", "h", "g", "f"] uniq: True ----------- -vect: ["g", "f", "c", "a"] +vect: ["f", "c", "a", "g"] uniq: True ----------- -vect: ["a", "h", "d", "g"] +vect: ["h", "d", "g", "a"] uniq: True ----------- -vect: ["a", "c", "d", "f"] +vect: ["c", "d", "f", "a"] uniq: True ----------- -vect: ["c", "d", "f", "a"] +vect: ["d", "f", "a", "c"] uniq: True diff --git a/examples/uniq-list/tests/gens/uniq-vect-tight/expected b/examples/uniq-list/tests/gens/uniq-vect-tight/expected index c504454fa..8794ee8f6 100644 --- a/examples/uniq-list/tests/gens/uniq-vect-tight/expected +++ b/examples/uniq-list/tests/gens/uniq-vect-tight/expected @@ -1,31 +1,31 @@ no spare strings to generate from (4 for vects of length 4) ----------- -vect: ["b", "d", "a", "c"] +vect: ["d", "a", "c", "b"] uniq: True ----------- -vect: ["d", "c", "a", "b"] +vect: ["c", "a", "b", "d"] uniq: True ----------- -vect: ["d", "c", "a", "b"] +vect: ["c", "a", "b", "d"] uniq: True ----------- -vect: ["c", "b", "a", "d"] +vect: ["b", "a", "d", "c"] uniq: True ----------- -vect: ["d", "c", "b", "a"] +vect: ["c", "b", "a", "d"] uniq: True ----------- -vect: ["a", "b", "d", "c"] +vect: ["b", "d", "c", "a"] uniq: True ----------- -vect: ["b", "d", "c", "a"] +vect: ["d", "c", "a", "b"] uniq: True ----------- -vect: ["a", "b", "c", "d"] +vect: ["b", "c", "d", "a"] uniq: True ----------- -vect: ["b", "c", "a", "d"] +vect: ["c", "a", "d", "b"] uniq: True ----------- -vect: ["c", "b", "a", "d"] +vect: ["b", "a", "d", "c"] uniq: True diff --git a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr index 88e837b87..66a905b21 100644 --- a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr +++ b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr @@ -101,7 +101,7 @@ searchOrder determinable left = do -- It's important to do so, since after discharging one of the selected variable, set of available variants can extend -- (e.g. because of discharging of strong determination), and new alternative have more priority than current ones. -- TODO to determine the best among current variants taking into account which indices are more complex (transitively!) - let Just (curr, currDet) = last' notDetermined + let Just (curr, currDet) = head' notDetermined | Nothing => [] -- remove information about all currently chosen args diff --git a/tests/derivation/core/big record 11/expected b/tests/derivation/core/big record 11/expected index 2b16866f3..7cb77e0d7 100644 --- a/tests/derivation/core/big record 11/expected +++ b/tests/derivation/core/big record 11/expected @@ -3,22 +3,22 @@ Generated values: ----- ----- -MkX 15 8 11 12 4 5 17 10 10 17 4 16 +MkX 16 4 17 10 10 17 5 4 12 11 8 15 ----- -MkX 17 13 17 0 20 15 1 10 4 7 14 4 +MkX 4 14 7 4 10 1 15 20 0 17 13 17 ----- -MkX 3 1 11 16 16 14 10 13 18 2 12 17 +MkX 17 12 2 18 13 10 14 16 16 11 1 3 ----- -MkX 2 18 12 6 16 3 7 19 17 12 10 3 +MkX 3 10 12 17 19 7 3 16 6 12 18 2 ----- -MkX 19 3 19 15 5 0 7 1 15 18 1 8 +MkX 8 1 18 15 1 7 0 5 15 19 3 19 ----- -MkX 13 1 3 20 5 19 13 3 0 4 6 9 +MkX 9 6 4 0 3 13 19 5 20 3 1 13 ----- -MkX 5 4 6 3 16 6 7 4 7 0 5 9 +MkX 9 5 0 7 4 7 6 16 3 6 4 5 ----- -MkX 18 10 7 5 15 19 13 12 11 2 11 10 +MkX 10 11 2 11 12 13 19 15 5 7 10 18 ----- -MkX 20 6 7 17 10 3 13 20 7 9 14 2 +MkX 2 14 9 7 20 13 3 10 17 7 6 20 ----- -MkX 14 20 12 2 17 19 12 20 1 5 13 19 +MkX 19 13 5 1 20 12 19 17 2 12 20 14 diff --git a/tests/derivation/core/big record 4/expected b/tests/derivation/core/big record 4/expected index edbd7e11d..d0b44bca1 100644 --- a/tests/derivation/core/big record 4/expected +++ b/tests/derivation/core/big record 4/expected @@ -3,22 +3,22 @@ Generated values: ----- ----- -MkX 10 17 4 16 +MkX 16 4 17 10 ----- -MkX 4 5 17 10 +MkX 10 17 5 4 ----- -MkX 15 8 11 12 +MkX 12 11 8 15 ----- -MkX 4 7 14 4 +MkX 4 14 7 4 ----- -MkX 20 15 1 10 +MkX 10 1 15 20 ----- -MkX 17 13 17 0 +MkX 0 17 13 17 ----- -MkX 18 2 12 17 +MkX 17 12 2 18 ----- -MkX 16 14 10 13 +MkX 13 10 14 16 ----- -MkX 3 1 11 16 +MkX 16 11 1 3 ----- -MkX 17 12 10 3 +MkX 3 10 12 17 diff --git a/tests/derivation/core/big record 5/expected b/tests/derivation/core/big record 5/expected index 42b309fb3..284b16465 100644 --- a/tests/derivation/core/big record 5/expected +++ b/tests/derivation/core/big record 5/expected @@ -3,22 +3,22 @@ Generated values: ----- ----- -MkX 10 10 17 4 16 +MkX 16 4 17 10 10 ----- -MkX 11 12 4 5 17 +MkX 17 5 4 12 11 ----- -MkX 7 14 4 15 8 +MkX 8 15 4 14 7 ----- -MkX 20 15 1 10 4 +MkX 4 10 1 15 20 ----- -MkX 17 17 13 17 0 +MkX 0 17 13 17 17 ----- -MkX 10 13 18 2 12 +MkX 12 2 18 13 10 ----- -MkX 1 11 16 16 14 +MkX 14 16 16 11 1 ----- -MkX 17 12 10 3 3 +MkX 3 3 10 12 17 ----- -MkX 6 16 3 7 19 +MkX 19 7 3 16 6 ----- -MkX 1 8 2 18 12 +MkX 12 18 2 8 1 diff --git a/tests/derivation/core/big record 8/expected b/tests/derivation/core/big record 8/expected index 4cad1a7bd..699cbef9a 100644 --- a/tests/derivation/core/big record 8/expected +++ b/tests/derivation/core/big record 8/expected @@ -3,22 +3,22 @@ Generated values: ----- ----- -MkX 4 5 17 10 10 17 4 16 +MkX 16 4 17 10 10 17 5 4 ----- -MkX 4 7 14 4 15 8 11 12 +MkX 12 11 8 15 4 14 7 4 ----- -MkX 17 13 17 0 20 15 1 10 +MkX 10 1 15 20 0 17 13 17 ----- -MkX 16 14 10 13 18 2 12 17 +MkX 17 12 2 18 13 10 14 16 ----- -MkX 17 12 10 3 3 1 11 16 +MkX 16 11 1 3 3 10 12 17 ----- -MkX 2 18 12 6 16 3 7 19 +MkX 19 7 3 16 6 12 18 2 ----- -MkX 5 0 7 1 15 18 1 8 +MkX 8 1 18 15 1 7 0 5 ----- -MkX 0 4 6 9 19 3 19 15 +MkX 15 19 3 19 9 6 4 0 ----- -MkX 13 1 3 20 5 19 13 3 +MkX 3 13 19 5 20 3 1 13 ----- -MkX 16 6 7 4 7 0 5 9 +MkX 9 5 0 7 4 7 6 16 diff --git a/tests/derivation/core/norec nodep noext 002/expected b/tests/derivation/core/norec nodep noext 002/expected index e8002ea6f..f24349d0b 100644 --- a/tests/derivation/core/norec nodep noext 002/expected +++ b/tests/derivation/core/norec nodep noext 002/expected @@ -19,6 +19,6 @@ X0 ----- X1 True ----- -X2 True False +X2 False True ----- X0 diff --git a/tests/derivation/core/norec nodep w_ext 002/expected b/tests/derivation/core/norec nodep w_ext 002/expected index 3b1bbdba5..41f247885 100644 --- a/tests/derivation/core/norec nodep w_ext 002/expected +++ b/tests/derivation/core/norec nodep w_ext 002/expected @@ -3,22 +3,22 @@ Generated values: ----- ----- -MkX "" "a" +MkX "a" "" ----- MkX "" "" ----- -MkX "a" "" +MkX "" "a" ----- MkX "a" "a" ----- -MkX "a" "" +MkX "" "a" ----- -MkX "bc" "a" +MkX "a" "bc" ----- MkX "" "" ----- -MkX "a" "bc" +MkX "bc" "a" ----- MkX "a" "a" ----- -MkX "" "a" +MkX "a" "" diff --git a/tests/derivation/core/norec nodep w_ext 003/expected b/tests/derivation/core/norec nodep w_ext 003/expected index 283dfd585..bca5e2eb1 100644 --- a/tests/derivation/core/norec nodep w_ext 003/expected +++ b/tests/derivation/core/norec nodep w_ext 003/expected @@ -3,22 +3,22 @@ Generated values: ----- ----- -MkX "" 10 +MkX "a" 0 ----- MkX "" 0 ----- -MkX "a" 0 +MkX "" 10 ----- MkX "a" 10 ----- MkX "" 10 ----- -MkX "a" 10 ------ -MkX "" 0 +MkX "a" 0 ----- MkX "" 10 ----- -MkX "a" 0 +MkX "" 0 +----- +MkX "a" 10 ----- MkX "a" 10 diff --git a/tests/derivation/core/norec nodep w_ext 004/expected b/tests/derivation/core/norec nodep w_ext 004/expected index 6da06a116..a598ad771 100644 --- a/tests/derivation/core/norec nodep w_ext 004/expected +++ b/tests/derivation/core/norec nodep w_ext 004/expected @@ -15,7 +15,7 @@ X1 "a" 10 ----- X3 "" ----- -X1 "a" 0 +X1 "bc" 10 ----- X2 10 ----- diff --git a/tests/derivation/core/norec t-..->p. noext 001/expected b/tests/derivation/core/norec t-..->p. noext 001/expected index 424ef5e3c..f285def7a 100644 --- a/tests/derivation/core/norec t-..->p. noext 001/expected +++ b/tests/derivation/core/norec t-..->p. noext 001/expected @@ -3,22 +3,22 @@ Generated values: ----- ----- -(False ** (True ** MkX False True)) +(True ** (False ** MkX True False)) ----- (False ** (False ** MkX False False)) ----- -(True ** (False ** MkX True False)) +(False ** (True ** MkX False True)) ----- (True ** (True ** MkX True True)) ----- (True ** (True ** MkX True True)) ----- -(True ** (False ** MkX True False)) ------ (False ** (True ** MkX False True)) ----- (True ** (False ** MkX True False)) ----- +(False ** (True ** MkX False True)) +----- (False ** (False ** MkX False False)) ----- (True ** (True ** MkX True True)) diff --git a/tests/derivation/core/norec t-..->p. noext 002/expected b/tests/derivation/core/norec t-..->p. noext 002/expected index ea06853cc..7bb6de6e4 100644 --- a/tests/derivation/core/norec t-..->p. noext 002/expected +++ b/tests/derivation/core/norec t-..->p. noext 002/expected @@ -5,11 +5,11 @@ Generated values: ----- (False ** (False ** X1)) ----- -(True ** (False ** X0 True False)) +(False ** (True ** X0 False True)) ----- (True ** (True ** X1)) ----- -(False ** (True ** X1)) +(True ** (False ** X1)) ----- (False ** (False ** X1)) ----- @@ -17,8 +17,8 @@ Generated values: ----- (True ** (True ** X1)) ----- -(True ** (False ** X1)) +(False ** (True ** X1)) ----- -(True ** (False ** X0 True False)) +(False ** (True ** X0 False True)) ----- -(True ** (False ** X1)) +(False ** (True ** X1)) diff --git a/tests/derivation/core/typealias con 001/expected b/tests/derivation/core/typealias con 001/expected index e8002ea6f..f24349d0b 100644 --- a/tests/derivation/core/typealias con 001/expected +++ b/tests/derivation/core/typealias con 001/expected @@ -19,6 +19,6 @@ X0 ----- X1 True ----- -X2 True False +X2 False True ----- X0 diff --git a/tests/derivation/core/typealias con 002/expected b/tests/derivation/core/typealias con 002/expected index db1387033..cd7fee414 100644 --- a/tests/derivation/core/typealias con 002/expected +++ b/tests/derivation/core/typealias con 002/expected @@ -19,6 +19,6 @@ X0 ----- X1 True ----- -X2 False 6 +X2 False 5 ----- X0 diff --git a/tests/derivation/least-effort/print/adt/004 noparam/expected b/tests/derivation/least-effort/print/adt/004 noparam/expected index 7c87977bc..d1cf40ea6 100644 --- a/tests/derivation/least-effort/print/adt/004 noparam/expected +++ b/tests/derivation/least-effort/print/adt/004 noparam/expected @@ -68,14 +68,14 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty X .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.R (orders)")) .$ ( var ">>=" - .$ (var "[]" .$ var "^outmost-fuel^") + .$ (var "[]" .$ var "^cons_fuel^") .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:1}") implicitFalse .=> var ">>=" - .$ (var "[]" .$ var "^cons_fuel^") + .$ (var "[]" .$ var "^outmost-fuel^") .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:2}") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "DerivedGen.R" .$ var "^bnd^{arg:2}" .$ var "^bnd^{arg:1}")))) + .$ (var "DerivedGen.R" .$ var "^bnd^{arg:1}" .$ var "^bnd^{arg:2}")))) ] ] , scope = diff --git a/tests/derivation/least-effort/print/adt/010 right-to-left long-dpair/expected b/tests/derivation/least-effort/print/adt/010 right-to-left long-dpair/expected index 7fbedbd1e..6694c4b8e 100644 --- a/tests/derivation/least-effort/print/adt/010 right-to-left long-dpair/expected +++ b/tests/derivation/least-effort/print/adt/010 right-to-left long-dpair/expected @@ -126,10 +126,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y .$ (var "fromString" .$ primVal (Str "DerivedGen.MkX (orders)")) .$ ( var ">>=" .$ (var "[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "m") implicitFalse + .$ ( MkArg MW ExplicitArg (Just "n") implicitFalse .=> var ">>=" .$ (var "[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "n") implicitFalse + .$ ( MkArg MW ExplicitArg (Just "m") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "Builtin.DPair.MkDPair" diff --git a/tests/derivation/least-effort/print/adt/011 right-to-left long-dpair/expected b/tests/derivation/least-effort/print/adt/011 right-to-left long-dpair/expected index f67aeae1b..dbcf6c57f 100644 --- a/tests/derivation/least-effort/print/adt/011 right-to-left long-dpair/expected +++ b/tests/derivation/least-effort/print/adt/011 right-to-left long-dpair/expected @@ -39,10 +39,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y Export [] (mkTy - { name = "[]" + { name = "[]" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Prelude.Types.Nat" + .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Builtin.Unit" }) , IClaim emptyFC @@ -50,10 +50,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y Export [] (mkTy - { name = "[]" + { name = "[]" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Builtin.Unit" + .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Prelude.Types.Nat" }) , IDef emptyFC @@ -136,11 +136,11 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.MkX (orders)")) .$ ( var ">>=" - .$ (var "[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "m") implicitFalse + .$ (var "[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "n") implicitFalse .=> var ">>=" - .$ (var "[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "n") implicitFalse + .$ (var "[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "m") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "Builtin.DPair.MkDPair" @@ -156,6 +156,38 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y .$ (var "<>" .$ var "^fuel_arg^") } ] + , IDef + emptyFC + "[]" + [ var "[]" .$ bindVar "^fuel_arg^" + .= local + { decls = + [ IClaim + emptyFC + MW + Export + [] + (mkTy + { name = "<>" + , type = + MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") + .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Builtin.Unit" + }) + , IDef + emptyFC + "<>" + [ var "<>" .$ bindVar "^cons_fuel^" + .= var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "Builtin.MkUnit (orders)")) + .$ (var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ var "Builtin.MkUnit") + ] + ] + , scope = + var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "Builtin.Unit[] (non-recursive)")) + .$ (var "<>" .$ var "^fuel_arg^") + } + ] , IDef emptyFC "[]" @@ -230,38 +262,6 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y } } ] - , IDef - emptyFC - "[]" - [ var "[]" .$ bindVar "^fuel_arg^" - .= local - { decls = - [ IClaim - emptyFC - MW - Export - [] - (mkTy - { name = "<>" - , type = - MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Builtin.Unit" - }) - , IDef - emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Builtin.MkUnit (orders)")) - .$ (var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ var "Builtin.MkUnit") - ] - ] - , scope = - var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "Builtin.Unit[] (non-recursive)")) - .$ (var "<>" .$ var "^fuel_arg^") - } - ] ] , scope = var "[]" .$ var "^outmost-fuel^" } diff --git a/tests/derivation/least-effort/print/adt/013 right-to-left nondet/expected b/tests/derivation/least-effort/print/adt/013 right-to-left nondet/expected index 7acf3f758..52ac1a8a6 100644 --- a/tests/derivation/least-effort/print/adt/013 right-to-left nondet/expected +++ b/tests/derivation/least-effort/print/adt/013 right-to-left nondet/expected @@ -93,7 +93,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y , clauses = [ var "Builtin.DPair.MkDPair" .$ bindVar "n" - .$ (var "Builtin.DPair.MkDPair" .$ bindVar "k" .$ bindVar "^bnd^{arg:3}") + .$ (var "Builtin.DPair.MkDPair" .$ bindVar "m" .$ bindVar "^bnd^{arg:3}") .= var ">>=" .$ (var "[0]" .$ var "^outmost-fuel^" .$ var "n") .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse @@ -101,15 +101,15 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y { sc = var "{lamc:0}" , ty = implicitFalse , clauses = - [ var "Builtin.DPair.MkDPair" .$ bindVar "m" .$ bindVar "^bnd^{arg:4}" + [ var "Builtin.DPair.MkDPair" .$ bindVar "k" .$ bindVar "^bnd^{arg:4}" .= var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "DerivedGen.MkY" .! ("k", implicitTrue) .! ("m", implicitTrue) .! ("n", implicitTrue) - .$ var "^bnd^{arg:4}" - .$ var "^bnd^{arg:3}") + .$ var "^bnd^{arg:3}" + .$ var "^bnd^{arg:4}") ] }) ] @@ -200,10 +200,10 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y .$ (var "fromString" .$ primVal (Str "DerivedGen.MkX (orders)")) .$ ( var ">>=" .$ (var "[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "m") implicitFalse + .$ ( MkArg MW ExplicitArg (Just "n") implicitFalse .=> var ">>=" .$ (var "[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "n") implicitFalse + .$ ( MkArg MW ExplicitArg (Just "m") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "Builtin.DPair.MkDPair" diff --git a/tests/derivation/least-effort/print/adt/014 right-to-left nondet ext/expected b/tests/derivation/least-effort/print/adt/014 right-to-left nondet ext/expected index e8c2f9413..0e930b022 100644 --- a/tests/derivation/least-effort/print/adt/014 right-to-left nondet ext/expected +++ b/tests/derivation/least-effort/print/adt/014 right-to-left nondet ext/expected @@ -94,7 +94,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel , clauses = [ var "Builtin.DPair.MkDPair" .$ bindVar "n" - .$ (var "Builtin.DPair.MkDPair" .$ bindVar "k" .$ bindVar "^bnd^{arg:5}") + .$ (var "Builtin.DPair.MkDPair" .$ bindVar "m" .$ bindVar "^bnd^{arg:5}") .= var ">>=" .$ (var "[0]" .$ var "^outmost-fuel^" .$ var "n") .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse @@ -102,15 +102,15 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel { sc = var "{lamc:0}" , ty = implicitFalse , clauses = - [ var "Builtin.DPair.MkDPair" .$ bindVar "m" .$ bindVar "^bnd^{arg:6}" + [ var "Builtin.DPair.MkDPair" .$ bindVar "k" .$ bindVar "^bnd^{arg:6}" .= var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "DerivedGen.MkY" .! ("k", implicitTrue) .! ("m", implicitTrue) .! ("n", implicitTrue) - .$ var "^bnd^{arg:6}" - .$ var "^bnd^{arg:5}") + .$ var "^bnd^{arg:5}" + .$ var "^bnd^{arg:6}") ] }) ] @@ -198,11 +198,11 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.MkX (orders)")) .$ ( var ">>=" - .$ (var "external^[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "m") implicitFalse + .$ (var "external^<^prim^.String>[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "n") implicitFalse .=> var ">>=" - .$ (var "external^<^prim^.String>[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "n") implicitFalse + .$ (var "external^[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "m") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "Builtin.DPair.MkDPair" diff --git a/tests/derivation/least-effort/print/gadt/003 right-to-left nondet/expected b/tests/derivation/least-effort/print/gadt/003 right-to-left nondet/expected index 71ee4768c..80194f89f 100644 --- a/tests/derivation/least-effort/print/gadt/003 right-to-left nondet/expected +++ b/tests/derivation/least-effort/print/gadt/003 right-to-left nondet/expected @@ -121,7 +121,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y , clauses = [ var "Builtin.DPair.MkDPair" .$ bindVar "n" - .$ (var "Builtin.DPair.MkDPair" .$ bindVar "k" .$ bindVar "^bnd^{arg:3}") + .$ (var "Builtin.DPair.MkDPair" .$ bindVar "m" .$ bindVar "^bnd^{arg:3}") .= var ">>=" .$ (var "[0]" .$ var "^outmost-fuel^" .$ var "n") .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse @@ -129,15 +129,15 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y { sc = var "{lamc:0}" , ty = implicitFalse , clauses = - [ var "Builtin.DPair.MkDPair" .$ bindVar "m" .$ bindVar "^bnd^{arg:4}" + [ var "Builtin.DPair.MkDPair" .$ bindVar "k" .$ bindVar "^bnd^{arg:4}" .= var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "DerivedGen.MkY1" .! ("k", implicitTrue) .! ("m", implicitTrue) .! ("n", implicitTrue) - .$ var "^bnd^{arg:4}" - .$ var "^bnd^{arg:3}") + .$ var "^bnd^{arg:3}" + .$ var "^bnd^{arg:4}") ] }) ] @@ -157,7 +157,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y , ty = implicitFalse , clauses = [ var "Builtin.DPair.MkDPair" - .$ bindVar "k" + .$ bindVar "n" .$ (var "Builtin.DPair.MkDPair" .$ bindVar "m" .$ bindVar "^bnd^{arg:5}") .= var ">>=" .$ (var "[1]" .$ var "^outmost-fuel^" .$ var "m") @@ -166,15 +166,15 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y { sc = var "{lamc:0}" , ty = implicitFalse , clauses = - [ var "Builtin.DPair.MkDPair" .$ bindVar "n" .$ bindVar "^bnd^{arg:6}" + [ var "Builtin.DPair.MkDPair" .$ bindVar "k" .$ bindVar "^bnd^{arg:6}" .= var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "DerivedGen.MkY2" .! ("k", implicitTrue) .! ("m", implicitTrue) .! ("n", implicitTrue) - .$ var "^bnd^{arg:6}" - .$ var "^bnd^{arg:5}") + .$ var "^bnd^{arg:5}" + .$ var "^bnd^{arg:6}") ] }) ] diff --git a/tests/derivation/least-effort/print/gadt/004 right-to-left det/expected b/tests/derivation/least-effort/print/gadt/004 right-to-left det/expected index 70c288fef..07223e951 100644 --- a/tests/derivation/least-effort/print/gadt/004 right-to-left det/expected +++ b/tests/derivation/least-effort/print/gadt/004 right-to-left det/expected @@ -20,7 +20,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y Export [] (mkTy - { name = "[0]" + { name = "[0]" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") .-> MkArg MW ExplicitArg (Just "{arg:1}") (var "Prelude.Types.Nat") @@ -29,7 +29,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y .$ ( var "Builtin.DPair.DPair" .$ var "Prelude.Types.Nat" .$ ( MkArg MW ExplicitArg (Just "{arg:2}") (var "Prelude.Types.Nat") - .=> var "DerivedGen.X_ADT" .$ var "{arg:1}" .$ var "{arg:2}")) + .=> var "DerivedGen.X_GADT" .$ var "{arg:1}" .$ var "{arg:2}")) }) , IClaim emptyFC @@ -37,7 +37,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y Export [] (mkTy - { name = "[]" + { name = "[]" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") .-> var "Test.DepTyCheck.Gen.Gen" @@ -48,7 +48,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y .=> var "Builtin.DPair.DPair" .$ var "Prelude.Types.Nat" .$ ( MkArg MW ExplicitArg (Just "{arg:4}") (var "Prelude.Types.Nat") - .=> var "DerivedGen.X_GADT" .$ var "{arg:3}" .$ var "{arg:4}"))) + .=> var "DerivedGen.X_ADT" .$ var "{arg:3}" .$ var "{arg:4}"))) }) , IClaim emptyFC @@ -56,7 +56,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y Export [] (mkTy - { name = "[0]" + { name = "[0]" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") .-> MkArg MW ExplicitArg (Just "{arg:3}") (var "Prelude.Types.Nat") @@ -65,7 +65,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y .$ ( var "Builtin.DPair.DPair" .$ var "Prelude.Types.Nat" .$ ( MkArg MW ExplicitArg (Just "{arg:4}") (var "Prelude.Types.Nat") - .=> var "DerivedGen.X_GADT" .$ var "{arg:3}" .$ var "{arg:4}")) + .=> var "DerivedGen.X_ADT" .$ var "{arg:3}" .$ var "{arg:4}")) }) , IClaim emptyFC @@ -73,7 +73,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y Export [] (mkTy - { name = "[]" + { name = "[]" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") .-> var "Test.DepTyCheck.Gen.Gen" @@ -84,7 +84,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y .=> var "Builtin.DPair.DPair" .$ var "Prelude.Types.Nat" .$ ( MkArg MW ExplicitArg (Just "{arg:2}") (var "Prelude.Types.Nat") - .=> var "DerivedGen.X_ADT" .$ var "{arg:1}" .$ var "{arg:2}"))) + .=> var "DerivedGen.X_GADT" .$ var "{arg:1}" .$ var "{arg:2}"))) }) , IClaim emptyFC @@ -132,7 +132,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.MkY_LR (orders)")) .$ ( var ">>=" - .$ (var "[]" .$ var "^outmost-fuel^") + .$ (var "[]" .$ var "^outmost-fuel^") .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse .=> iCase { sc = var "{lamc:0}" @@ -140,23 +140,23 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y , clauses = [ var "Builtin.DPair.MkDPair" .$ bindVar "n" - .$ (var "Builtin.DPair.MkDPair" .$ bindVar "k" .$ bindVar "^bnd^{arg:5}") + .$ (var "Builtin.DPair.MkDPair" .$ bindVar "m" .$ bindVar "^bnd^{arg:5}") .= var ">>=" - .$ (var "[0]" .$ var "^outmost-fuel^" .$ var "n") + .$ (var "[0]" .$ var "^outmost-fuel^" .$ var "n") .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse .=> iCase { sc = var "{lamc:0}" , ty = implicitFalse , clauses = - [ var "Builtin.DPair.MkDPair" .$ bindVar "m" .$ bindVar "^bnd^{arg:6}" + [ var "Builtin.DPair.MkDPair" .$ bindVar "k" .$ bindVar "^bnd^{arg:6}" .= var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "DerivedGen.MkY_LR" .! ("k", implicitTrue) .! ("m", implicitTrue) .! ("n", implicitTrue) - .$ var "^bnd^{arg:6}" - .$ var "^bnd^{arg:5}") + .$ var "^bnd^{arg:5}" + .$ var "^bnd^{arg:6}") ] }) ] @@ -169,7 +169,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.MkY_RL (orders)")) .$ ( var ">>=" - .$ (var "[]" .$ var "^outmost-fuel^") + .$ (var "[]" .$ var "^outmost-fuel^") .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse .=> iCase { sc = var "{lamc:0}" @@ -177,23 +177,23 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y , clauses = [ var "Builtin.DPair.MkDPair" .$ bindVar "n" - .$ (var "Builtin.DPair.MkDPair" .$ bindVar "k" .$ bindVar "^bnd^{arg:7}") + .$ (var "Builtin.DPair.MkDPair" .$ bindVar "m" .$ bindVar "^bnd^{arg:7}") .= var ">>=" - .$ (var "[0]" .$ var "^outmost-fuel^" .$ var "n") + .$ (var "[0]" .$ var "^outmost-fuel^" .$ var "n") .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse .=> iCase { sc = var "{lamc:0}" , ty = implicitFalse , clauses = - [ var "Builtin.DPair.MkDPair" .$ bindVar "m" .$ bindVar "^bnd^{arg:8}" + [ var "Builtin.DPair.MkDPair" .$ bindVar "k" .$ bindVar "^bnd^{arg:8}" .= var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "DerivedGen.MkY_RL" .! ("k", implicitTrue) .! ("m", implicitTrue) .! ("n", implicitTrue) - .$ var "^bnd^{arg:8}" - .$ var "^bnd^{arg:7}") + .$ var "^bnd^{arg:7}" + .$ var "^bnd^{arg:8}") ] }) ] @@ -212,8 +212,8 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y ] , IDef emptyFC - "[0]" - [ var "[0]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^<{arg:1}>" + "[0]" + [ var "[0]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^<{arg:1}>" .= local { decls = [ IClaim @@ -222,7 +222,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y Export [] (mkTy - { name = "<>" + { name = "<>" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") .-> MkArg MW ExplicitArg (Just "{arg:1}") (var "Prelude.Types.Nat") @@ -231,32 +231,72 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y .$ ( var "Builtin.DPair.DPair" .$ var "Prelude.Types.Nat" .$ ( MkArg MW ExplicitArg (Just "{arg:2}") (var "Prelude.Types.Nat") - .=> var "DerivedGen.X_ADT" .$ var "{arg:1}" .$ var "{arg:2}")) + .=> var "DerivedGen.X_GADT" .$ var "{arg:1}" .$ var "{arg:2}")) + }) + , IClaim + emptyFC + MW + Export + [] + (mkTy + { name = "<>" + , type = + MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") + .-> MkArg MW ExplicitArg (Just "{arg:1}") (var "Prelude.Types.Nat") + .-> var "Test.DepTyCheck.Gen.Gen" + .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" + .$ ( var "Builtin.DPair.DPair" + .$ var "Prelude.Types.Nat" + .$ ( MkArg MW ExplicitArg (Just "{arg:2}") (var "Prelude.Types.Nat") + .=> var "DerivedGen.X_GADT" .$ var "{arg:1}" .$ var "{arg:2}")) }) , IDef emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" .$ bindVar "n" + "<>" + [ var "<>" + .$ bindVar "^cons_fuel^" + .$ ( var "Prelude.Types.S" + .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z")))) .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "DerivedGen.MkX (orders)")) + .$ (var "fromString" .$ primVal (Str "DerivedGen.MkXG_4 (orders)")) + .$ ( var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ var "DerivedGen.MkXG_4")) + , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" + ] + , IDef + emptyFC + "<>" + [ var "<>" + .$ bindVar "^cons_fuel^" + .$ ( var "Prelude.Types.S" + .$ ( var "Prelude.Types.S" + .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z"))))) + .= var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "DerivedGen.MkXG_5 (orders)")) .$ ( var ">>=" .$ (var "[]" .$ var "^outmost-fuel^") .$ ( MkArg MW ExplicitArg (Just "m") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ (var "DerivedGen.MkX" .$ var "n" .$ var "m")))) + .$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ (var "DerivedGen.MkXG_5" .! ("m", var "m"))))) + , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" ] ] , scope = var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "DerivedGen.X_ADT[0] (non-recursive)")) - .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^<{arg:1}>") + .$ (var "fromString" .$ primVal (Str "DerivedGen.X_GADT[0] (non-recursive)")) + .$ ( var "Test.DepTyCheck.Gen.oneOf" + .! ("em", var "MaybeEmpty") + .$ ( var "::" + .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^<{arg:1}>") + .$ (var "::" .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^<{arg:1}>") .$ var "Nil"))) } ] , IDef emptyFC - "[]" - [ var "[]" .$ bindVar "^fuel_arg^" + "[]" + [ var "[]" .$ bindVar "^fuel_arg^" .= local { decls = [ IClaim @@ -265,7 +305,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y Export [] (mkTy - { name = "<>" + { name = "<>" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") .-> var "Test.DepTyCheck.Gen.Gen" @@ -276,69 +316,82 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y .=> var "Builtin.DPair.DPair" .$ var "Prelude.Types.Nat" .$ ( MkArg MW ExplicitArg (Just "{arg:4}") (var "Prelude.Types.Nat") - .=> var "DerivedGen.X_GADT" .$ var "{arg:3}" .$ var "{arg:4}"))) + .=> var "DerivedGen.X_ADT" .$ var "{arg:3}" .$ var "{arg:4}"))) }) - , IClaim + , IDef + emptyFC + "<>" + [ var "<>" .$ bindVar "^cons_fuel^" + .= var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "DerivedGen.MkX (orders)")) + .$ ( var ">>=" + .$ (var "[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "n") implicitFalse + .=> var ">>=" + .$ (var "[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "m") implicitFalse + .=> var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ (var "DerivedGen.MkX" .$ var "n" .$ var "m")))))) + ] + ] + , scope = + var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "DerivedGen.X_ADT[] (non-recursive)")) + .$ (var "<>" .$ var "^fuel_arg^") + } + ] + , IDef + emptyFC + "[0]" + [ var "[0]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^<{arg:3}>" + .= local + { decls = + [ IClaim emptyFC MW Export [] (mkTy - { name = "<>" + { name = "<>" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") + .-> MkArg MW ExplicitArg (Just "{arg:3}") (var "Prelude.Types.Nat") .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ ( var "Builtin.DPair.DPair" .$ var "Prelude.Types.Nat" - .$ ( MkArg MW ExplicitArg (Just "{arg:3}") (var "Prelude.Types.Nat") - .=> var "Builtin.DPair.DPair" - .$ var "Prelude.Types.Nat" - .$ ( MkArg MW ExplicitArg (Just "{arg:4}") (var "Prelude.Types.Nat") - .=> var "DerivedGen.X_GADT" .$ var "{arg:3}" .$ var "{arg:4}"))) + .$ ( MkArg MW ExplicitArg (Just "{arg:4}") (var "Prelude.Types.Nat") + .=> var "DerivedGen.X_ADT" .$ var "{arg:3}" .$ var "{arg:4}")) }) , IDef emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "DerivedGen.MkXG_4 (orders)")) - .$ ( var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ ( var "Builtin.DPair.MkDPair" - .$ implicitTrue - .$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ var "DerivedGen.MkXG_4"))) - ] - , IDef - emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" + "<>" + [ var "<>" .$ bindVar "^cons_fuel^" .$ bindVar "n" .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "DerivedGen.MkXG_5 (orders)")) + .$ (var "fromString" .$ primVal (Str "DerivedGen.MkX (orders)")) .$ ( var ">>=" .$ (var "[]" .$ var "^outmost-fuel^") .$ ( MkArg MW ExplicitArg (Just "m") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ ( var "Builtin.DPair.MkDPair" - .$ implicitTrue - .$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ (var "DerivedGen.MkXG_5" .! ("m", var "m")))))) + .$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ (var "DerivedGen.MkX" .$ var "n" .$ var "m")))) ] ] , scope = var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "DerivedGen.X_GADT[] (non-recursive)")) - .$ ( var "Test.DepTyCheck.Gen.oneOf" - .! ("em", var "MaybeEmpty") - .$ ( var "::" - .$ (var "<>" .$ var "^fuel_arg^") - .$ (var "::" .$ (var "<>" .$ var "^fuel_arg^") .$ var "Nil"))) + .$ (var "fromString" .$ primVal (Str "DerivedGen.X_ADT[0] (non-recursive)")) + .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^<{arg:3}>") } ] , IDef emptyFC - "[0]" - [ var "[0]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^<{arg:3}>" + "[]" + [ var "[]" .$ bindVar "^fuel_arg^" .= local { decls = [ IClaim @@ -350,13 +403,15 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y { name = "<>" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> MkArg MW ExplicitArg (Just "{arg:3}") (var "Prelude.Types.Nat") .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ ( var "Builtin.DPair.DPair" .$ var "Prelude.Types.Nat" - .$ ( MkArg MW ExplicitArg (Just "{arg:4}") (var "Prelude.Types.Nat") - .=> var "DerivedGen.X_GADT" .$ var "{arg:3}" .$ var "{arg:4}")) + .$ ( MkArg MW ExplicitArg (Just "{arg:1}") (var "Prelude.Types.Nat") + .=> var "Builtin.DPair.DPair" + .$ var "Prelude.Types.Nat" + .$ ( MkArg MW ExplicitArg (Just "{arg:2}") (var "Prelude.Types.Nat") + .=> var "DerivedGen.X_GADT" .$ var "{arg:1}" .$ var "{arg:2}"))) }) , IClaim emptyFC @@ -367,36 +422,32 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y { name = "<>" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> MkArg MW ExplicitArg (Just "{arg:3}") (var "Prelude.Types.Nat") .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ ( var "Builtin.DPair.DPair" .$ var "Prelude.Types.Nat" - .$ ( MkArg MW ExplicitArg (Just "{arg:4}") (var "Prelude.Types.Nat") - .=> var "DerivedGen.X_GADT" .$ var "{arg:3}" .$ var "{arg:4}")) + .$ ( MkArg MW ExplicitArg (Just "{arg:1}") (var "Prelude.Types.Nat") + .=> var "Builtin.DPair.DPair" + .$ var "Prelude.Types.Nat" + .$ ( MkArg MW ExplicitArg (Just "{arg:2}") (var "Prelude.Types.Nat") + .=> var "DerivedGen.X_GADT" .$ var "{arg:1}" .$ var "{arg:2}"))) }) , IDef emptyFC "<>" - [ var "<>" - .$ bindVar "^cons_fuel^" - .$ ( var "Prelude.Types.S" - .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z")))) + [ var "<>" .$ bindVar "^cons_fuel^" .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.MkXG_4 (orders)")) .$ ( var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ var "DerivedGen.MkXG_4")) - , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ var "DerivedGen.MkXG_4"))) ] , IDef emptyFC "<>" - [ var "<>" - .$ bindVar "^cons_fuel^" - .$ ( var "Prelude.Types.S" - .$ ( var "Prelude.Types.S" - .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z"))))) + [ var "<>" .$ bindVar "^cons_fuel^" .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.MkXG_5 (orders)")) .$ ( var ">>=" @@ -404,70 +455,19 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Y .$ ( MkArg MW ExplicitArg (Just "m") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ (var "DerivedGen.MkXG_5" .! ("m", var "m"))))) - , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ (var "DerivedGen.MkXG_5" .! ("m", var "m")))))) ] ] , scope = var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "DerivedGen.X_GADT[0] (non-recursive)")) + .$ (var "fromString" .$ primVal (Str "DerivedGen.X_GADT[] (non-recursive)")) .$ ( var "Test.DepTyCheck.Gen.oneOf" .! ("em", var "MaybeEmpty") .$ ( var "::" - .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^<{arg:3}>") - .$ (var "::" .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^<{arg:3}>") .$ var "Nil"))) - } - ] - , IDef - emptyFC - "[]" - [ var "[]" .$ bindVar "^fuel_arg^" - .= local - { decls = - [ IClaim - emptyFC - MW - Export - [] - (mkTy - { name = "<>" - , type = - MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> var "Test.DepTyCheck.Gen.Gen" - .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ ( var "Builtin.DPair.DPair" - .$ var "Prelude.Types.Nat" - .$ ( MkArg MW ExplicitArg (Just "{arg:1}") (var "Prelude.Types.Nat") - .=> var "Builtin.DPair.DPair" - .$ var "Prelude.Types.Nat" - .$ ( MkArg MW ExplicitArg (Just "{arg:2}") (var "Prelude.Types.Nat") - .=> var "DerivedGen.X_ADT" .$ var "{arg:1}" .$ var "{arg:2}"))) - }) - , IDef - emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "DerivedGen.MkX (orders)")) - .$ ( var ">>=" - .$ (var "[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "m") implicitFalse - .=> var ">>=" - .$ (var "[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "n") implicitFalse - .=> var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ ( var "Builtin.DPair.MkDPair" - .$ implicitTrue - .$ ( var "Builtin.DPair.MkDPair" - .$ implicitTrue - .$ (var "DerivedGen.MkX" .$ var "n" .$ var "m")))))) - ] - ] - , scope = - var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "DerivedGen.X_ADT[] (non-recursive)")) - .$ (var "<>" .$ var "^fuel_arg^") + .$ (var "<>" .$ var "^fuel_arg^") + .$ (var "::" .$ (var "<>" .$ var "^fuel_arg^") .$ var "Nil"))) } ] , IDef diff --git a/tests/derivation/least-effort/print/gadt/005 gadt/expected b/tests/derivation/least-effort/print/gadt/005 gadt/expected index 726305725..db16989dd 100644 --- a/tests/derivation/least-effort/print/gadt/005 gadt/expected +++ b/tests/derivation/least-effort/print/gadt/005 gadt/expected @@ -118,22 +118,22 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.JJ (orders)")) .$ ( var ">>=" - .$ (var "external^[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:4}") implicitFalse + .$ (var "[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "b") implicitFalse .=> var ">>=" .$ (var "external^[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:5}") implicitFalse + .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:4}") implicitFalse .=> var ">>=" - .$ (var "[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "b") implicitFalse + .$ (var "external^[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:5}") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "Builtin.DPair.MkDPair" .$ implicitTrue .$ ( var "DerivedGen.JJ" .! ("b", var "b") - .$ var "^bnd^{arg:5}" - .$ var "^bnd^{arg:4}")))))) + .$ var "^bnd^{arg:4}" + .$ var "^bnd^{arg:5}")))))) ] , IDef emptyFC @@ -142,26 +142,26 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.FN (orders)")) .$ ( var ">>=" - .$ (var "[]" .$ var "^cons_fuel^") - .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse - .=> iCase - { sc = var "{lamc:0}" - , ty = implicitFalse - , clauses = - [ var "Builtin.DPair.MkDPair" .$ bindVar "b" .$ bindVar "^bnd^{arg:6}" - .= var ">>=" - .$ (var "external^[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:7}") implicitFalse - .=> var "Prelude.pure" + .$ (var "external^[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:6}") implicitFalse + .=> var ">>=" + .$ (var "[]" .$ var "^cons_fuel^") + .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse + .=> iCase + { sc = var "{lamc:0}" + , ty = implicitFalse + , clauses = + [ var "Builtin.DPair.MkDPair" .$ bindVar "b" .$ bindVar "^bnd^{arg:7}" + .= var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "Builtin.DPair.MkDPair" .$ implicitTrue .$ ( var "DerivedGen.FN" .! ("b", implicitTrue) - .$ var "^bnd^{arg:7}" - .$ var "^bnd^{arg:6}"))) - ] - })) + .$ var "^bnd^{arg:6}" + .$ var "^bnd^{arg:7}")) + ] + }))) ] , IDef emptyFC @@ -183,26 +183,26 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.TR (orders)")) .$ ( var ">>=" - .$ (var "[]" .$ var "^cons_fuel^") - .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse - .=> iCase - { sc = var "{lamc:0}" - , ty = implicitFalse - , clauses = - [ var "Builtin.DPair.MkDPair" .$ bindVar "b" .$ bindVar "^bnd^{arg:9}" - .= var ">>=" - .$ (var "external^<^prim^.String>[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:10}") implicitFalse - .=> var "Prelude.pure" + .$ (var "external^<^prim^.String>[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:9}") implicitFalse + .=> var ">>=" + .$ (var "[]" .$ var "^cons_fuel^") + .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse + .=> iCase + { sc = var "{lamc:0}" + , ty = implicitFalse + , clauses = + [ var "Builtin.DPair.MkDPair" .$ bindVar "b" .$ bindVar "^bnd^{arg:10}" + .= var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "Builtin.DPair.MkDPair" .$ implicitTrue .$ ( var "DerivedGen.TR" .! ("b", implicitTrue) - .$ var "^bnd^{arg:10}" - .$ var "^bnd^{arg:9}"))) - ] - })) + .$ var "^bnd^{arg:9}" + .$ var "^bnd^{arg:10}")) + ] + }))) ] ] , scope = diff --git a/tests/derivation/least-effort/print/gadt/006 gadt/expected b/tests/derivation/least-effort/print/gadt/006 gadt/expected index cf6b957f8..8f051a9fa 100644 --- a/tests/derivation/least-effort/print/gadt/006 gadt/expected +++ b/tests/derivation/least-effort/print/gadt/006 gadt/expected @@ -130,7 +130,7 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:5}") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "DerivedGen.JJ" .! ("b", var "b") .$ var "^bnd^{arg:5}" .$ var "^bnd^{arg:4}")))) + .$ (var "DerivedGen.JJ" .! ("b", var "b") .$ var "^bnd^{arg:4}" .$ var "^bnd^{arg:5}")))) ] , IDef emptyFC @@ -139,24 +139,24 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.FN (orders)")) .$ ( var ">>=" - .$ (var "[]" .$ var "^cons_fuel^") - .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse - .=> iCase - { sc = var "{lamc:0}" - , ty = implicitFalse - , clauses = - [ var "Builtin.DPair.MkDPair" .$ bindVar "b" .$ bindVar "^bnd^{arg:6}" - .= var ">>=" - .$ (var "external^[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:7}") implicitFalse - .=> var "Prelude.pure" + .$ (var "external^[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:6}") implicitFalse + .=> var ">>=" + .$ (var "[]" .$ var "^cons_fuel^") + .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse + .=> iCase + { sc = var "{lamc:0}" + , ty = implicitFalse + , clauses = + [ var "Builtin.DPair.MkDPair" .$ bindVar "b" .$ bindVar "^bnd^{arg:7}" + .= var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "DerivedGen.FN" .! ("b", implicitTrue) - .$ var "^bnd^{arg:7}" - .$ var "^bnd^{arg:6}")) - ] - })) + .$ var "^bnd^{arg:6}" + .$ var "^bnd^{arg:7}") + ] + }))) , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" ] , IDef @@ -180,24 +180,24 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.TR (orders)")) .$ ( var ">>=" - .$ (var "[]" .$ var "^cons_fuel^") - .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse - .=> iCase - { sc = var "{lamc:0}" - , ty = implicitFalse - , clauses = - [ var "Builtin.DPair.MkDPair" .$ bindVar "b" .$ bindVar "^bnd^{arg:9}" - .= var ">>=" - .$ (var "external^<^prim^.String>[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:10}") implicitFalse - .=> var "Prelude.pure" + .$ (var "external^<^prim^.String>[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:9}") implicitFalse + .=> var ">>=" + .$ (var "[]" .$ var "^cons_fuel^") + .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse + .=> iCase + { sc = var "{lamc:0}" + , ty = implicitFalse + , clauses = + [ var "Builtin.DPair.MkDPair" .$ bindVar "b" .$ bindVar "^bnd^{arg:10}" + .= var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "DerivedGen.TR" .! ("b", implicitTrue) - .$ var "^bnd^{arg:10}" - .$ var "^bnd^{arg:9}")) - ] - })) + .$ var "^bnd^{arg:9}" + .$ var "^bnd^{arg:10}") + ] + }))) , var "<>" .$ implicitTrue .$ implicitTrue .= var "empty" ] ] @@ -316,22 +316,22 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.JJ (orders)")) .$ ( var ">>=" - .$ (var "external^[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:4}") implicitFalse + .$ (var "[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "b") implicitFalse .=> var ">>=" .$ (var "external^[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:5}") implicitFalse + .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:4}") implicitFalse .=> var ">>=" - .$ (var "[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "b") implicitFalse + .$ (var "external^[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:5}") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "Builtin.DPair.MkDPair" .$ implicitTrue .$ ( var "DerivedGen.JJ" .! ("b", var "b") - .$ var "^bnd^{arg:5}" - .$ var "^bnd^{arg:4}")))))) + .$ var "^bnd^{arg:4}" + .$ var "^bnd^{arg:5}")))))) ] , IDef emptyFC @@ -340,26 +340,26 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.FN (orders)")) .$ ( var ">>=" - .$ (var "[]" .$ var "^cons_fuel^") - .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse - .=> iCase - { sc = var "{lamc:0}" - , ty = implicitFalse - , clauses = - [ var "Builtin.DPair.MkDPair" .$ bindVar "b" .$ bindVar "^bnd^{arg:6}" - .= var ">>=" - .$ (var "external^[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:7}") implicitFalse - .=> var "Prelude.pure" + .$ (var "external^[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:6}") implicitFalse + .=> var ">>=" + .$ (var "[]" .$ var "^cons_fuel^") + .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse + .=> iCase + { sc = var "{lamc:0}" + , ty = implicitFalse + , clauses = + [ var "Builtin.DPair.MkDPair" .$ bindVar "b" .$ bindVar "^bnd^{arg:7}" + .= var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "Builtin.DPair.MkDPair" .$ implicitTrue .$ ( var "DerivedGen.FN" .! ("b", implicitTrue) - .$ var "^bnd^{arg:7}" - .$ var "^bnd^{arg:6}"))) - ] - })) + .$ var "^bnd^{arg:6}" + .$ var "^bnd^{arg:7}")) + ] + }))) ] , IDef emptyFC @@ -381,26 +381,26 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.TR (orders)")) .$ ( var ">>=" - .$ (var "[]" .$ var "^cons_fuel^") - .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse - .=> iCase - { sc = var "{lamc:0}" - , ty = implicitFalse - , clauses = - [ var "Builtin.DPair.MkDPair" .$ bindVar "b" .$ bindVar "^bnd^{arg:9}" - .= var ">>=" - .$ (var "external^<^prim^.String>[]" .$ var "^outmost-fuel^") - .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:10}") implicitFalse - .=> var "Prelude.pure" + .$ (var "external^<^prim^.String>[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:9}") implicitFalse + .=> var ">>=" + .$ (var "[]" .$ var "^cons_fuel^") + .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse + .=> iCase + { sc = var "{lamc:0}" + , ty = implicitFalse + , clauses = + [ var "Builtin.DPair.MkDPair" .$ bindVar "b" .$ bindVar "^bnd^{arg:10}" + .= var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "Builtin.DPair.MkDPair" .$ implicitTrue .$ ( var "DerivedGen.TR" .! ("b", implicitTrue) - .$ var "^bnd^{arg:10}" - .$ var "^bnd^{arg:9}"))) - ] - })) + .$ var "^bnd^{arg:9}" + .$ var "^bnd^{arg:10}")) + ] + }))) ] ] , scope = diff --git a/tests/derivation/least-effort/print/order/002 complex order/expected b/tests/derivation/least-effort/print/order/002 complex order/expected index bd0401863..7e64a8999 100644 --- a/tests/derivation/least-effort/print/order/002 complex order/expected +++ b/tests/derivation/least-effort/print/order/002 complex order/expected @@ -57,11 +57,11 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Z Export [] (mkTy - { name = "[0]" + { name = "[0]" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ (var "DerivedGen.BS" .$ var "n") + .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ (var "Data.Fin.Fin" .$ var "n") }) , IClaim emptyFC @@ -69,11 +69,11 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Z Export [] (mkTy - { name = "[0]" + { name = "[0]" , type = MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ (var "Data.Fin.Fin" .$ var "n") + .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ (var "DerivedGen.BS" .$ var "n") }) , IDef emptyFC @@ -265,13 +265,11 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Z .= var "Test.DepTyCheck.Gen.label" .$ (var "fromString" .$ primVal (Str "DerivedGen.Y0 (orders)")) .$ ( var ">>=" - .$ (var "[0]" .$ var "^outmost-fuel^" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z")) - .$ ( MkArg MW ExplicitArg (Just "i") implicitFalse + .$ (var "[0]" .$ var "^outmost-fuel^" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z")) + .$ ( MkArg MW ExplicitArg (Just "bs") implicitFalse .=> var ">>=" - .$ ( var "[0]" - .$ var "^outmost-fuel^" - .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z")) - .$ ( MkArg MW ExplicitArg (Just "bs") implicitFalse + .$ (var "[0]" .$ var "^outmost-fuel^" .$ (var "Prelude.Types.S" .$ var "Prelude.Types.Z")) + .$ ( MkArg MW ExplicitArg (Just "i") implicitFalse .=> var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ ( var "Builtin.DPair.MkDPair" @@ -312,43 +310,6 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Z .$ (var "::" .$ (var "<>" .$ var "^fuel_arg^") .$ var "Nil"))) } ] - , IDef - emptyFC - "[0]" - [ var "[0]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^" - .= local - { decls = - [ IClaim - emptyFC - MW - Export - [] - (mkTy - { name = "<>" - , type = - MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") - .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") - .-> var "Test.DepTyCheck.Gen.Gen" - .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" - .$ (var "DerivedGen.BS" .$ var "n") - }) - , IDef - emptyFC - "<>" - [ var "<>" .$ bindVar "^cons_fuel^" .$ bindVar "n" - .= var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "DerivedGen.MkBS (orders)")) - .$ ( var "Prelude.pure" - .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) - .$ (var "DerivedGen.MkBS" .! ("n", var "n"))) - ] - ] - , scope = - var "Test.DepTyCheck.Gen.label" - .$ (var "fromString" .$ primVal (Str "DerivedGen.BS[0] (non-recursive)")) - .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^") - } - ] , IDef emptyFC "[0]" @@ -435,6 +396,43 @@ LOG deptycheck.derive.print:5: type: (arg : Fuel) -> Gen MaybeEmpty Z } } ] + , IDef + emptyFC + "[0]" + [ var "[0]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^" + .= local + { decls = + [ IClaim + emptyFC + MW + Export + [] + (mkTy + { name = "<>" + , type = + MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") + .-> MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .-> var "Test.DepTyCheck.Gen.Gen" + .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" + .$ (var "DerivedGen.BS" .$ var "n") + }) + , IDef + emptyFC + "<>" + [ var "<>" .$ bindVar "^cons_fuel^" .$ bindVar "n" + .= var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "DerivedGen.MkBS (orders)")) + .$ ( var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ (var "DerivedGen.MkBS" .! ("n", var "n"))) + ] + ] + , scope = + var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "DerivedGen.BS[0] (non-recursive)")) + .$ (var "<>" .$ var "^fuel_arg^" .$ var "inter^") + } + ] ] , scope = var "[]" .$ var "^outmost-fuel^" } diff --git a/tests/derivation/least-effort/run/adt/004 noparam/expected b/tests/derivation/least-effort/run/adt/004 noparam/expected index d995870d9..94044733a 100644 --- a/tests/derivation/least-effort/run/adt/004 noparam/expected +++ b/tests/derivation/least-effort/run/adt/004 noparam/expected @@ -3,22 +3,22 @@ Generated values: ----- ----- -R (R (R (R (R (R (R (R (R (R E 4) 10) 11) 12) 17) 8) 10) 17) 4) 16 +R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R E 4) 17) 10) 10) 17) 5) 4) 12) 11) 8) 15) 4) 14) 7) 4) 10 ----- -R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R E 16) 14) 9) 12) 19) 5) 20) 14) 20) 17) 17) 15) 0) 6) 1) 7) 14) 4) 14 +R E 15 ----- -R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R E 1) 15) 12) 6) 16) 3) 7) 19) 17) 12) 6) 2) 2) 0) 8) 16 +R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R E 0) 17) 13) 17) 17) 12) 2) 18) 13) 10) 14) 16) 16) 11) 1) 3) 3) 10) 12) 17 ----- -R (R (R (R E 15) 17) 0) 5 +R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R (R E 7) 3) 16) 6) 12) 18) 2) 8) 1) 18) 15) 1) 7) 0) 5) 15) 19) 3) 19 ----- -R E 6 +R (R (R (R (R (R (R (R (R E 6) 4) 0) 3) 13) 19) 5) 20) 3 ----- -R (R (R (R (R (R (R E 3) 14) 18) 1) 20) 1) 19 +R E 13 ----- -R (R (R (R (R (R (R (R (R E 4) 8) 13) 1) 3) 20) 15) 13) 2 +R (R (R (R (R (R (R (R (R E 5) 0) 7) 4) 7) 6) 16) 3) 6 ----- -R (R (R (R (R (R (R (R (R E 5) 2) 4) 2) 16) 5) 6) 3) 7 +R (R (R (R E 5) 10) 11) 2 ----- -R (R (R (R (R (R (R (R E 15) 19) 13) 11) 10) 1) 10) 4 +R (R (R (R (R (R (R (R (R (R (R E 12) 13) 19) 15) 5) 7) 10) 18) 2) 14) 9 ----- -R (R (R (R (R (R (R (R (R (R (R (R (R (R E 19) 6) 13) 17) 2) 13) 20) 6) 8) 13) 1) 17) 8) 12 +R (R (R (R (R (R (R E 20) 13) 3) 10) 17) 7) 6 diff --git a/tests/derivation/least-effort/run/adt/010 right-to-left long-dpair/expected b/tests/derivation/least-effort/run/adt/010 right-to-left long-dpair/expected index 00bda4bbf..c2745099d 100644 --- a/tests/derivation/least-effort/run/adt/010 right-to-left long-dpair/expected +++ b/tests/derivation/least-effort/run/adt/010 right-to-left long-dpair/expected @@ -3,22 +3,22 @@ Generated values: ----- ----- -MkY (MkX {n=4} {m=16}) ------ -MkY (MkX {n=10} {m=17}) +MkY (MkX {n=16} {m=4}) ----- MkY (MkX {n=17} {m=10}) ----- -MkY (MkX {n=4} {m=5}) +MkY (MkX {n=10} {m=17}) +----- +MkY (MkX {n=5} {m=4}) ----- -MkY (MkX {n=11} {m=12}) +MkY (MkX {n=12} {m=11}) ----- -MkY (MkX {n=15} {m=8}) +MkY (MkX {n=8} {m=15}) ----- -MkY (MkX {n=14} {m=4}) +MkY (MkX {n=4} {m=14}) ----- -MkY (MkX {n=4} {m=7}) +MkY (MkX {n=7} {m=4}) ----- -MkY (MkX {n=1} {m=10}) +MkY (MkX {n=10} {m=1}) ----- -MkY (MkX {n=20} {m=15}) +MkY (MkX {n=15} {m=20}) diff --git a/tests/derivation/least-effort/run/adt/013 right-to-left nondet/expected b/tests/derivation/least-effort/run/adt/013 right-to-left nondet/expected index ac9849693..3d40a969b 100644 --- a/tests/derivation/least-effort/run/adt/013 right-to-left nondet/expected +++ b/tests/derivation/least-effort/run/adt/013 right-to-left nondet/expected @@ -3,22 +3,22 @@ Generated values: ----- ----- -MkY (MkX {n=4} {m=17}) (MkX {n=4} {m=16}) +MkY (MkX {n=16} {m=4}) (MkX {n=16} {m=17}) ----- -MkY (MkX {n=10} {m=17}) (MkX {n=10} {m=10}) +MkY (MkX {n=10} {m=10}) (MkX {n=10} {m=17}) ----- -MkY (MkX {n=4} {m=12}) (MkX {n=4} {m=5}) +MkY (MkX {n=5} {m=4}) (MkX {n=5} {m=12}) ----- -MkY (MkX {n=8} {m=15}) (MkX {n=8} {m=11}) +MkY (MkX {n=11} {m=8}) (MkX {n=11} {m=15}) ----- -MkY (MkX {n=14} {m=7}) (MkX {n=14} {m=4}) +MkY (MkX {n=4} {m=14}) (MkX {n=4} {m=7}) ----- -MkY (MkX {n=10} {m=1}) (MkX {n=10} {m=4}) +MkY (MkX {n=4} {m=10}) (MkX {n=4} {m=1}) ----- -MkY (MkX {n=20} {m=0}) (MkX {n=20} {m=15}) +MkY (MkX {n=15} {m=20}) (MkX {n=15} {m=0}) ----- -MkY (MkX {n=13} {m=17}) (MkX {n=13} {m=17}) +MkY (MkX {n=17} {m=13}) (MkX {n=17} {m=17}) ----- -MkY (MkX {n=12} {m=2}) (MkX {n=12} {m=17}) +MkY (MkX {n=17} {m=12}) (MkX {n=17} {m=2}) ----- -MkY (MkX {n=13} {m=10}) (MkX {n=13} {m=18}) +MkY (MkX {n=18} {m=13}) (MkX {n=18} {m=10}) diff --git a/tests/derivation/least-effort/run/adt/014 right-to-left nondet ext/expected b/tests/derivation/least-effort/run/adt/014 right-to-left nondet ext/expected index 0a472f403..ad400ff85 100644 --- a/tests/derivation/least-effort/run/adt/014 right-to-left nondet ext/expected +++ b/tests/derivation/least-effort/run/adt/014 right-to-left nondet ext/expected @@ -3,9 +3,9 @@ Generated values: ----- ----- -MkY (MkX "" 0) (MkX "" 10) +MkY (MkX "a" 0) (MkX "a" 0) ----- -MkY (MkX "" 10) (MkX "" 0) +MkY (MkX "" 0) (MkX "" 10) ----- MkY (MkX "a" 10) (MkX "a" 10) ----- @@ -17,8 +17,8 @@ MkY (MkX "" 0) (MkX "" 10) ----- MkY (MkX "a" 10) (MkX "a" 10) ----- -MkY (MkX "a" 0) (MkX "a" 10) +MkY (MkX "a" 0) (MkX "a" 0) ----- -MkY (MkX "" 10) (MkX "" 0) +MkY (MkX "" 10) (MkX "" 10) ----- -MkY (MkX "a" 0) (MkX "a" 10) +MkY (MkX "a" 0) (MkX "a" 0) diff --git a/tests/derivation/least-effort/run/gadt/003 right-to-left nondet/expected b/tests/derivation/least-effort/run/gadt/003 right-to-left nondet/expected index 77cbe2710..e1e2f2ba8 100644 --- a/tests/derivation/least-effort/run/gadt/003 right-to-left nondet/expected +++ b/tests/derivation/least-effort/run/gadt/003 right-to-left nondet/expected @@ -9,16 +9,16 @@ MkY1 (MkXG_4) (MkXG_4) ----- MkY2 (MkXG_5 12) (MkXG_5 12) ----- -MkY1 (MkXG_5 17) (MkXG_5 2) +MkY1 (MkXG_5 2) (MkXG_5 17) ----- -MkY1 (MkXG_5 8) (MkXG_5 10) +MkY1 (MkXG_5 10) (MkXG_5 8) ----- MkY2 (MkXG_5 17) (MkXG_5 17) ----- -MkY1 (MkXG_5 12) (MkXG_5 10) +MkY1 (MkXG_5 10) (MkXG_5 12) ----- -MkY1 (MkXG_5 4) (MkXG_5 7) +MkY1 (MkXG_5 7) (MkXG_5 4) ----- -MkY1 (MkXG_5 4) (MkXG_5 14) +MkY1 (MkXG_5 14) (MkXG_5 4) ----- -MkY1 (MkXG_5 7) (MkXG_5 14) +MkY1 (MkXG_5 14) (MkXG_5 7) diff --git a/tests/derivation/least-effort/run/gadt/004 right-to-left det/expected b/tests/derivation/least-effort/run/gadt/004 right-to-left det/expected index 8ca257b11..2dfbc1a1a 100644 --- a/tests/derivation/least-effort/run/gadt/004 right-to-left det/expected +++ b/tests/derivation/least-effort/run/gadt/004 right-to-left det/expected @@ -3,22 +3,22 @@ Generated values: ----- ----- -MkY_RL (MkX 4 16) (MkXG_4) +MkY_RL (MkX 5 9) (MkXG_5) ----- -MkY_LR (MkXG_5) (MkX 5 4) +MkY_LR (MkXG_4) (MkX 4 17) ----- -MkY_LR (MkXG_5) (MkX 5 8) +MkY_LR (MkXG_5) (MkX 5 10) ----- -MkY_RL (MkX 4 11) (MkXG_4) +MkY_RL (MkX 5 11) (MkXG_5) ----- -MkY_RL (MkX 4 11) (MkXG_4) +MkY_RL (MkX 5 5) (MkXG_5) ----- -MkY_LR (MkXG_4) (MkX 4 10) ------ -MkY_RL (MkX 5 4) (MkXG_5) +MkY_LR (MkXG_5) (MkX 5 15) ----- MkY_LR (MkXG_5) (MkX 5 14) ----- -MkY_RL (MkX 4 6) (MkXG_4) +MkY_RL (MkX 5 4) (MkXG_5) +----- +MkY_RL (MkX 5 10) (MkXG_5) ----- -MkY_RL (MkX 5 15) (MkXG_5) +MkY_LR (MkXG_5) (MkX 5 13) diff --git a/tests/derivation/least-effort/run/gadt/005 gadt/expected b/tests/derivation/least-effort/run/gadt/005 gadt/expected index 3e012d742..bffc02658 100644 --- a/tests/derivation/least-effort/run/gadt/005 gadt/expected +++ b/tests/derivation/least-effort/run/gadt/005 gadt/expected @@ -3,22 +3,22 @@ Generated values: ----- ----- -(False ** FN 10 (FN 10 (TR "bc" (FN 10 (FN 0 (TR "a" (FN 10 (TR "bc" (FN 10 (FN 0 (TR "" (FN 0 (TR "a" (TR "a" (FN 0 (TR "" (TL ""))))))))))))))))) +(False ** FN 0 (TL "")) ----- -(False ** FN 10 (TR "a" (FN 0 (FN 0 (TR "a" (TR "" (FN 0 (FN 10 (FN 0 (FN 10 (FN 0 (TR "a" (TR "bc" (TR "bc" (TR "" (TL "bc")))))))))))))))) +(False ** FN 10 (FN 10 (TR "a" (FN 0 (FN 10 (TR "a" (FN 0 (FN 0 (FN 10 (TR "" (TR "bc" (FN 0 (TL "a"))))))))))))) ----- -(True ** JJ 10 10) +(True ** TR "bc" (FN 10 (TR "" (FN 10 (TR "bc" (FN 0 (FN 0 (FN 0 (TR "bc" (TR "a" (TR "" (TR "bc" (TR "a" (FN 10 (TR "bc" (FN 0 (TR "a" (FN 0 (TL "a"))))))))))))))))))) ----- -(True ** TR "bc" (FN 0 (TR "a" (FN 10 (FN 10 (FN 10 (FN 0 (FN 10 (TR "" (FN 0 (TR "a" (TR "a" (TL ""))))))))))))) +(True ** TR "" (FN 10 (TR "" (FN 10 (FN 0 (TR "a" (TR "a" (TR "a" (FN 10 (FN 10 (TR "a" (TR "bc" (JJ 0 10))))))))))))) ----- -(True ** TR "a" (FN 0 (FN 10 (TR "a" (FN 10 (TR "a" (JJ 0 10))))))) +(False ** FN 10 (FN 0 (TR "" (FN 0 (TR "bc" (TR "" (TL ""))))))) ----- -(True ** TR "bc" (FN 10 (TR "bc" (TR "bc" (TR "a" (FN 0 (FN 10 (FN 0 (FN 0 (JJ 10 0)))))))))) +(True ** TL "a") ----- -(False ** FN 0 (FN 10 (FN 0 (TR "a" (FN 10 (FN 0 (FN 10 (FN 0 (FN 0 (FN 10 (TR "a" (FN 10 (TR "a" (FN 0 (FN 10 (FN 0 (FN 10 (JJ 10 0)))))))))))))))))) +(False ** FN 10 (TR "bc" (FN 10 (TR "bc" (TR "bc" (FN 10 (FN 0 (JJ 10 10)))))))) ----- -(True ** TR "a" (TR "bc" (FN 0 (FN 10 (TR "" (FN 0 (FN 10 (TR "" (TR "bc" (FN 10 (JJ 10 10))))))))))) +(True ** TR "" (FN 10 (FN 0 (FN 0 (FN 0 (FN 0 (FN 0 (TR "bc" (TR "" (TR "bc" (FN 0 (FN 10 (FN 0 (FN 0 (TR "" (FN 0 (TR "bc" (TR "bc" (TR "a" (TL "a")))))))))))))))))))) ----- -(True ** TR "a" (FN 10 (TR "" (TR "bc" (TR "a" (FN 10 (FN 10 (FN 0 (FN 10 (TR "" (TR "" (FN 10 (FN 0 (JJ 10 10)))))))))))))) +(True ** TR "" (TR "" (TL "a"))) ----- -(True ** TR "bc" (TR "a" (FN 0 (TR "" (JJ 0 0))))) +(True ** TR "a" (TR "a" (FN 0 (TR "a" (TR "bc" (FN 0 (FN 10 (FN 10 (FN 10 (TR "a" (FN 0 (FN 10 (JJ 0 0))))))))))))) diff --git a/tests/derivation/least-effort/run/gadt/006 gadt/expected b/tests/derivation/least-effort/run/gadt/006 gadt/expected index 4badde148..33e8fa138 100644 --- a/tests/derivation/least-effort/run/gadt/006 gadt/expected +++ b/tests/derivation/least-effort/run/gadt/006 gadt/expected @@ -5,41 +5,41 @@ Generated values: ----- TL "" ----- -TR "a" (TR "bc" (FN 10 (FN 0 (FN 0 (FN 0 (FN 10 (FN 10 (FN 10 (FN 0 (FN 0 (TR "" (TL "a")))))))))))) +TR "" (FN 10 (FN 10 (TR "a" (FN 0 (FN 10 (TR "a" (FN 0 (FN 0 (FN 10 (TR "" (FN 10 (TL "a")))))))))))) ----- -TR "bc" (FN 0 (TR "" (FN 0 (FN 0 (TR "a" (FN 10 (TR "bc" (TR "bc" (FN 0 (FN 0 (TL "bc"))))))))))) +TR "bc" (FN 10 (TR "" (FN 10 (TR "bc" (FN 0 (FN 0 (FN 0 (TR "bc" (TR "a" (TR "" (TR "bc" (TR "a" (FN 10 (TR "bc" (FN 0 (TR "a" (FN 0 (TL "a")))))))))))))))))) ----- -TR "bc" (TL "") +TR "" (FN 10 (TR "" (FN 10 (FN 0 (TR "a" (TR "a" (TR "a" (FN 10 (FN 10 (TR "a" (TR "bc" (JJ 0 10)))))))))))) ----- -TR "" (FN 0 (FN 10 (TR "a" (JJ 10 10)))) +TR "a" (FN 0 (FN 0 (TR "bc" (TR "" (TR "a" (TR "a" (FN 0 (FN 10 (TR "bc" (TR "bc" (FN 10 (FN 0 (JJ 10 10))))))))))))) ----- -TR "a" (FN 0 (FN 10 (FN 0 (FN 0 (TR "a" (TR "a" (TR "" (FN 10 (TR "a" (TL "a")))))))))) +TR "" (FN 10 (FN 0 (FN 0 (FN 0 (FN 0 (FN 0 (TR "bc" (TR "" (TR "bc" (FN 0 (FN 10 (FN 0 (FN 0 (TR "" (FN 0 (TR "bc" (TR "bc" (TR "a" (TL "a"))))))))))))))))))) ----- -TR "bc" (TR "bc" (FN 10 (FN 10 (TR "a" (FN 0 (FN 10 (FN 10 (TR "a" (FN 10 (JJ 0 10)))))))))) +TR "a" (TR "" (TR "" (TR "a" (TR "" (TR "" (TR "bc" (TR "a" (FN 10 (TR "bc" (JJ 10 10)))))))))) ----- -TR "bc" (FN 10 (TR "" (FN 0 (JJ 10 0)))) +TR "bc" (TR "" (TR "" (TR "bc" (FN 10 (JJ 0 0))))) ----- -TR "bc" (FN 0 (FN 0 (FN 0 (TR "a" (TL ""))))) +TR "" (TR "a" (TR "" (TR "" (TR "" (FN 10 (TR "a" (FN 10 (FN 10 (TR "bc" (TR "" (FN 10 (FN 10 (TR "a" (FN 10 (JJ 0 10))))))))))))))) ----- -TR "" (TR "bc" (FN 0 (FN 10 (FN 0 (FN 10 (FN 0 (TR "a" (FN 10 (TR "" (FN 10 (TR "" (FN 0 (FN 10 (FN 10 (FN 10 (TR "a" (FN 0 (TR "a" (TL ""))))))))))))))))))) +TR "a" (TR "bc" (TR "bc" (TR "bc" (TR "a" (TR "a" (FN 0 (TR "a" (JJ 10 10)))))))) ----- ----- -FN 10 (FN 10 (TR "bc" (FN 10 (FN 0 (TR "a" (FN 10 (TR "bc" (FN 10 (FN 0 (TR "" (FN 0 (TR "a" (TR "a" (FN 0 (TR "" (TL "")))))))))))))))) +FN 0 (TL "") ----- -FN 10 (TR "a" (FN 0 (FN 0 (TR "a" (TR "" (FN 0 (FN 10 (FN 0 (FN 10 (FN 0 (TR "a" (TR "bc" (TR "bc" (TR "" (TL "bc"))))))))))))))) +FN 10 (FN 10 (TR "a" (FN 0 (FN 10 (TR "a" (FN 0 (FN 0 (FN 10 (TR "" (TR "bc" (FN 0 (TL "a")))))))))))) ----- -JJ 10 10 +FN 10 (FN 10 (TR "" (FN 10 (TR "bc" (FN 0 (FN 0 (FN 0 (TR "bc" (TR "a" (TR "" (TR "bc" (TR "a" (FN 10 (TR "bc" (FN 0 (TR "a" (FN 0 (TL "a")))))))))))))))))) ----- -FN 0 (FN 0 (TR "a" (FN 10 (FN 10 (FN 10 (FN 0 (FN 10 (TR "" (FN 0 (TR "a" (TR "a" (TL "")))))))))))) +FN 0 (FN 10 (TR "" (FN 10 (FN 0 (TR "a" (TR "a" (TR "a" (FN 10 (FN 10 (TR "a" (TR "bc" (JJ 0 10)))))))))))) ----- -FN 10 (FN 0 (FN 10 (TR "a" (FN 10 (TR "a" (JJ 0 10)))))) +FN 10 (FN 0 (TR "" (FN 0 (TR "bc" (TR "" (TL "")))))) ----- -FN 0 (FN 10 (TR "bc" (TR "bc" (TR "a" (FN 0 (FN 10 (FN 0 (FN 0 (JJ 10 0))))))))) +FN 10 (TR "bc" (FN 10 (TR "bc" (TR "bc" (FN 10 (FN 0 (JJ 10 10))))))) ----- -FN 0 (FN 10 (FN 0 (TR "a" (FN 10 (FN 0 (FN 10 (FN 0 (FN 0 (FN 10 (TR "a" (FN 10 (TR "a" (FN 0 (FN 10 (FN 0 (FN 10 (JJ 10 0))))))))))))))))) +FN 0 (FN 10 (FN 0 (FN 0 (FN 0 (FN 0 (FN 0 (TR "bc" (TR "" (TR "bc" (FN 0 (FN 10 (FN 0 (FN 0 (TR "" (FN 0 (TR "bc" (TR "bc" (TR "a" (TL "a"))))))))))))))))))) ----- -FN 10 (TR "bc" (FN 0 (FN 10 (TR "" (FN 0 (FN 10 (TR "" (TR "bc" (FN 10 (JJ 10 10)))))))))) +FN 10 (TR "" (TR "" (TR "a" (TR "" (TR "" (TR "bc" (TR "a" (FN 10 (TR "bc" (JJ 10 10)))))))))) ----- -JJ 0 10 +FN 0 (TR "" (TR "" (TR "bc" (FN 10 (JJ 0 0))))) ----- -FN 0 (FN 10 (FN 10 (FN 0 (JJ 10 0)))) +FN 0 (TR "a" (TR "" (TR "" (TR "" (FN 10 (TR "a" (FN 10 (FN 10 (TR "bc" (TR "" (FN 10 (FN 10 (TR "a" (FN 10 (JJ 0 10)))))))))))))))