idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-25 04:33:45 +03:00
Code Issues Projects Releases Wiki Activity

[ test ] clean_names to make test outputs neater (#3156)

Browse Source
This commit is contained in:
Steve Dunham 2023-12-08 06:10:37 -08:00 committed by GitHub
parent 319fa65570
commit 59e00c5210
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
16 changed files with 170 additions and 134 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
CHANGELOG.md
View File

@ -314,6 +314,7 @@
* Updates the docs for `envvars` to categorise when environment variables are * Updates the docs for `envvars` to categorise when environment variables are
used (runtime, build-time, or both). used (runtime, build-time, or both).
* Fixed build failure occuring when `make -j` is in effect. * Fixed build failure occuring when `make -j` is in effect.
* Add `clean_names` function to `testutils.sh` to normalise machine names
## v0.6.0 ## v0.6.0

2
src/TTImp/ProcessDef.idr
View File

@ -1145,7 +1145,7 @@ processDef opts nest env fc n_in cs_in
getPMDef fc (CompileTime mult) (Resolved n) ty covcs getPMDef fc (CompileTime mult) (Resolved n) ty covcs
logC "declare.def" 3 $ do pure $ "Working from " ++ show !(toFullNames ctree) logC "declare.def" 3 $ do pure $ "Working from " ++ show !(toFullNames ctree)
missCase <- if any catchAll covcs missCase <- if any catchAll covcs
then do log "declare.def" 3 $ "Catch all case in " ++ show n then do logC "declare.def" 3 $ do pure "Catch all case in \{show !(getFullName (Resolved n))}"
pure [] pure []
else getMissing fc (Resolved n) ctree else getMissing fc (Resolved n) ctree
logC "declare.def" 3 $ logC "declare.def" 3 $

4
tests/codegen/builtin001/expected
View File

@ -1,3 +1,3 @@
Dumping case trees to Main.cases Dumping case trees to Main.cases
Main.plus = [{arg:N}, {arg:N}]: (%case !{arg:N} [(%constcase 0 !{arg:N})] Just (%let {e:N} (-Integer [!{arg:N}, 1]) (+Integer [(Main.plus [!{e:N}, !{arg:N}]), 1]))) Main.plus = [{arg:1}, {arg:1}]: (%case !{arg:1} [(%constcase 0 !{arg:1})] Just (%let {e:0} (-Integer [!{arg:1}, 1]) (+Integer [(Main.plus [!{e:0}, !{arg:1}]), 1])))
Main.main = [{ext:N}]: (Main.plus [1, 2]) Main.main = [{ext:0}]: (Main.plus [1, 2])

2
tests/codegen/builtin001/run
View File

@ -3,4 +3,4 @@ rm Main.cases
idris2 --dumpcases Main.cases -o Main Main.idr idris2 --dumpcases Main.cases -o Main Main.idr
cat Main.cases | sed -E "s/[0-9]+}/N}/g" | sed -E "s/[0-9]+:[0-9]+/L:C/g" | grep 'Main.plus\|Main.bah' cat Main.cases | clean_names | grep 'Main.plus\|Main.bah'

2
tests/codegen/con001/run
View File

@ -3,4 +3,4 @@ rm Main.cases
idris2 --dumpcases Main.cases -o Main Main.idr idris2 --dumpcases Main.cases -o Main Main.idr
cat Main.cases | sed -E "s/[0-9]+}/N}/g" | sed -E "s/[0-9]+:[0-9]+/L:C/g" | sed '/Constructor/!d' cat Main.cases | sed '/Constructor/!d'

136
tests/idris2/basic/basic044/expected
View File

@ -21,11 +21,11 @@ LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term:L:C--L:C, Rig0)) LOG unify.meta:5: Adding new meta ({P:cut:1}, (Term:1, Rig0))
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term:L:C--L:C, Rig0)) LOG unify.meta:5: Adding new meta ({P:vars:1}, (Term:2, Rig0))
LOG unify.equal:10: Skipped unification (equal already): Type and Type LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term:L:C--L:C, Rig0)) LOG unify.meta:5: Adding new meta ({P:cut:2}, (Term:3, Rig0))
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term:L:C--L:C, Rig0)) LOG unify.meta:5: Adding new meta ({P:vars:2}, (Term:4, Rig0))
LOG unify.equal:10: Skipped unification (equal already): Type and Type LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG declare.data:1: Processing Term.Chk LOG declare.data:1: Processing Term.Chk
@ -33,14 +33,14 @@ LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term:L:C--L:C, Rig0)) LOG unify.meta:5: Adding new meta ({P:cut:3}, (Term:5, Rig0))
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term:L:C--L:C, Rig0)) LOG unify.meta:5: Adding new meta ({P:vars:3}, (Term:6, Rig0))
LOG unify.equal:10: Skipped unification (equal already): Type and Type LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term:L:C--L:C, Rig0)) LOG unify.meta:5: Adding new meta ({P:cut:4}, (Term:7, Rig0))
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term:L:C--L:C, Rig0)) LOG unify.meta:5: Adding new meta ({P:vars:4}, (Term:8, Rig0))
LOG unify.meta:5: Adding new meta ({P:n:N}, (Term:L:C--L:C, Rig0)) LOG unify.meta:5: Adding new meta ({P:n:1}, (Term:9, Rig0))
LOG unify.equal:10: Skipped unification (equal already): Type and Type LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG declare.data:1: Processing Term.Syn LOG declare.data:1: Processing Term.Syn
@ -48,25 +48,25 @@ LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term:L:C--L:C, Rig0)) LOG unify.meta:5: Adding new meta ({P:vars:5}, (Term:10, Rig0))
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term:L:C--L:C, Rig0)) LOG unify.meta:5: Adding new meta ({P:cut:5}, (Term:11, Rig0))
LOG unify.equal:10: Skipped unification (equal already): Type and Type LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.meta:5: Adding new meta ({P:cut:N}, (Term:L:C--L:C, Rig0)) LOG unify.meta:5: Adding new meta ({P:cut:6}, (Term:12, Rig0))
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term:L:C--L:C, Rig0)) LOG unify.meta:5: Adding new meta ({P:vars:6}, (Term:13, Rig0))
LOG unify.equal:10: Skipped unification (equal already): Type and Type LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.meta:5: Adding new meta ({P:vars:N}, (Term:L:C--L:C, Rig0)) LOG unify.meta:5: Adding new meta ({P:vars:7}, (Term:14, Rig0))
LOG unify.equal:10: Skipped unification (equal already): Type and Type LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG unify.equal:10: Skipped unification (equal already): Type and Type LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG declare.def.lhs:3: LHS term: Term.Typ LOG declare.def.lhs:3: LHS term: Term.Typ
LOG unify.equal:10: Skipped unification (equal already): (vars : $resolvedN) -> Type and (vars : $resolvedN) -> Type LOG unify.equal:10: Skipped unification (equal already): (vars : $resolved1) -> Type and (vars : $resolved1) -> Type
LOG declare.def.clause:3: RHS term: Term.Chk LOG declare.def.clause:3: RHS term: Term.Chk
LOG declare.def:2: Case tree for Term.Typ: [0] Term.Chk LOG declare.def:2: Case tree for Term.Typ: [0] Term.Chk
LOG declare.def:3: Working from [0] Term.Chk LOG declare.def:3: Working from [0] Term.Chk
LOG declare.def:3: Catch all case in N LOG declare.def:3: Catch all case in Term.Typ
LOG declare.def:3: Initially missing in Term.Typ: LOG declare.def:3: Initially missing in Term.Typ:
LOG declare.type:1: Processing Term.Term LOG declare.type:1: Processing Term.Term
@ -78,7 +78,7 @@ LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG declare.def.clause:3: RHS term: (Term.Chk Prelude.Basics.True) LOG declare.def.clause:3: RHS term: (Term.Chk Prelude.Basics.True)
LOG declare.def:2: Case tree for Term.Term: [0] (Term.Chk Prelude.Basics.True) LOG declare.def:2: Case tree for Term.Term: [0] (Term.Chk Prelude.Basics.True)
LOG declare.def:3: Working from [0] (Term.Chk Prelude.Basics.True) LOG declare.def:3: Working from [0] (Term.Chk Prelude.Basics.True)
LOG declare.def:3: Catch all case in N LOG declare.def:3: Catch all case in Term.Term
LOG declare.def:3: Initially missing in Term.Term: LOG declare.def:3: Initially missing in Term.Term:
LOG declare.type:1: Processing Term.NF LOG declare.type:1: Processing Term.NF
@ -90,69 +90,69 @@ LOG unify.equal:10: Skipped unification (equal already): Type and Type
LOG declare.def.clause:3: RHS term: (Term.Chk Prelude.Basics.False) LOG declare.def.clause:3: RHS term: (Term.Chk Prelude.Basics.False)
LOG declare.def:2: Case tree for Term.NF: [0] (Term.Chk Prelude.Basics.False) LOG declare.def:2: Case tree for Term.NF: [0] (Term.Chk Prelude.Basics.False)
LOG declare.def:3: Working from [0] (Term.Chk Prelude.Basics.False) LOG declare.def:3: Working from [0] (Term.Chk Prelude.Basics.False)
LOG declare.def:3: Catch all case in N LOG declare.def:3: Catch all case in Term.NF
LOG declare.def:3: Initially missing in Term.NF: LOG declare.def:3: Initially missing in Term.NF:
Term> Bye for now! Term> Bye for now!
1/1: Building Vec (Vec.idr) 1/1: Building Vec (Vec.idr)
LOG declare.type:1: Processing Vec.Vec LOG declare.type:1: Processing Vec.Vec
LOG declare.def:2: Case tree for Vec.Vec: [0] ({arg:N} : (Data.Fin.Fin {arg:N}[1])) -> {arg:N}[1] LOG declare.def:2: Case tree for Vec.Vec: [0] ({arg:1} : (Data.Fin.Fin {arg:2}[1])) -> {arg:2}[1]
LOG declare.type:1: Processing Vec.Nil LOG declare.type:1: Processing Vec.Nil
LOG declare.def:2: Case tree for Vec.Nil: [0] (Prelude.Uninhabited.absurd {arg:N}[0] (Data.Fin.Fin Prelude.Types.Z) Data.Fin.Uninhabited implementation at Data.Fin:L:C--L:C) LOG declare.def:2: Case tree for Vec.Nil: [0] (Prelude.Uninhabited.absurd {arg:2}[0] (Data.Fin.Fin Prelude.Types.Z) Data.Fin.Uninhabited implementation at Data.Fin:1)
LOG declare.type:1: Processing Vec.(::) LOG declare.type:1: Processing Vec.(::)
LOG declare.def:2: Case tree for Vec.(::): case {arg:N}[4] : (Data.Fin.Fin (Prelude.Types.S {arg:N}[0])) of LOG declare.def:2: Case tree for Vec.(::): case {arg:2}[4] : (Data.Fin.Fin (Prelude.Types.S {arg:2}[0])) of
{ Data.Fin.FZ {e:N} => [0] {arg:N}[3] { Data.Fin.FZ {e:0} => [0] {arg:2}[3]
| Data.Fin.FS {e:N} {e:N} => [1] ({arg:N}[5] {e:N}[1]) | Data.Fin.FS {e:1} {e:2} => [1] ({arg:2}[5] {e:2}[1])
} }
LOG declare.type:1: Processing Vec.test LOG declare.type:1: Processing Vec.test
LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C: LOG elab.ambiguous:5: Ambiguous elaboration at Vec:1:
($resolvedN 2) ($resolved1 2)
($resolvedN 2) ($resolved2 2)
With default. Target type : Prelude.Types.Nat With default. Target type : Prelude.Types.Nat
LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:L:C--L:C: LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:2:
(($resolvedN Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil)) (($resolved3 Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil))
(($resolvedN Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil)) (($resolved4 Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil))
(($resolvedN Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil)) (($resolved5 Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil))
Target type : ({arg:N} : (Data.Fin.Fin (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z)))) -> (Prelude.Basics.List Prelude.Types.Nat) Target type : ({arg:1} : (Data.Fin.Fin (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z)))) -> (Prelude.Basics.List Prelude.Types.Nat)
LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:L:C--L:C: LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:3:
$resolvedN $resolved6
$resolvedN $resolved7
Target type : ?Vec.{a:N}_[] Target type : ?Vec.{a:4574}_[]
LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:L:C--L:C: LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:4:
(($resolvedN ((:: (fromInteger 0)) Nil)) Nil) (($resolved3 ((:: (fromInteger 0)) Nil)) Nil)
(($resolvedN ((:: (fromInteger 0)) Nil)) Nil) (($resolved4 ((:: (fromInteger 0)) Nil)) Nil)
(($resolvedN ((:: (fromInteger 0)) Nil)) Nil) (($resolved5 ((:: (fromInteger 0)) Nil)) Nil)
Target type : (Vec.Vec ?Vec.{a:N}_[] ?Vec.{n:N}_[]) Target type : (Vec.Vec ?Vec.{a:4574}_[] ?Vec.{n:4573}_[])
LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:L:C--L:C: LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:5:
(($resolvedN (fromInteger 0)) Nil) (($resolved3 (fromInteger 0)) Nil)
(($resolvedN (fromInteger 0)) Nil) (($resolved4 (fromInteger 0)) Nil)
(($resolvedN (fromInteger 0)) Nil) (($resolved5 (fromInteger 0)) Nil)
Target type : ?Vec.{a:N}_[] Target type : ?Vec.{a:4577}_[]
LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C: LOG elab.ambiguous:5: Ambiguous elaboration at Vec:6:
($resolvedN 0) ($resolved1 0)
($resolvedN 0) ($resolved2 0)
With default. Target type : ?Vec.{a:N}_[] With default. Target type : ?Vec.{a:4579}_[]
LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:L:C--L:C: LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:7:
$resolvedN $resolved6
$resolvedN $resolved7
Target type : (Vec.Vec ?Vec.{a:N}_[] ?Vec.{n:N}_[]) Target type : (Vec.Vec ?Vec.{a:4579}_[] ?Vec.{n:4578}_[])
LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C: LOG elab.ambiguous:5: Ambiguous elaboration at Vec:6:
($resolvedN 0) ($resolved1 0)
($resolvedN 0) ($resolved2 0)
With default. Target type : ?Vec.{a:N}_[] With default. Target type : ?Vec.{a:4578}_[]
LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:L:C--L:C: LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:8:
$resolvedN $resolved6
$resolvedN $resolved7
Target type : (Vec.Vec ?Vec.{a:N}_[] ?Vec.{n:N}_[]) Target type : (Vec.Vec ?Vec.{a:4577}_[] ?Vec.{n:4576}_[])
LOG elab.ambiguous:5: Ambiguous elaboration (kept 1 out of 3 candidates) (delayed) at Vec:L:C--L:C: LOG elab.ambiguous:5: Ambiguous elaboration (kept 1 out of 3 candidates) (delayed) at Vec:5:
(($resolvedN (fromInteger 0)) Nil) (($resolved4 (fromInteger 0)) Nil)
Target type : (Prelude.Basics.List Prelude.Types.Nat) Target type : (Prelude.Basics.List Prelude.Types.Nat)
LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C: LOG elab.ambiguous:5: Ambiguous elaboration at Vec:6:
($resolvedN 0) ($resolved1 0)
($resolvedN 0) ($resolved2 0)
With default. Target type : Prelude.Types.Nat With default. Target type : Prelude.Types.Nat
LOG elab.ambiguous:5: Ambiguous elaboration (kept 1 out of 2 candidates) (delayed) at Vec:L:C--L:C: LOG elab.ambiguous:5: Ambiguous elaboration (kept 1 out of 2 candidates) (delayed) at Vec:3:
$resolvedN $resolved7
Target type : (Prelude.Basics.List Prelude.Types.Nat) Target type : (Prelude.Basics.List Prelude.Types.Nat)
LOG declare.def:2: Case tree for Vec.test: [0] (Vec.(::) (Prelude.Types.S Prelude.Types.Z) (Prelude.Basics.List Prelude.Types.Nat) (Prelude.Basics.Nil Prelude.Types.Nat) (Vec.(::) Prelude.Types.Z (Prelude.Basics.List Prelude.Types.Nat) (Prelude.Basics.(::) Prelude.Types.Nat Prelude.Types.Z (Prelude.Basics.Nil Prelude.Types.Nat)) (Vec.Nil (Prelude.Basics.List Prelude.Types.Nat)))) LOG declare.def:2: Case tree for Vec.test: [0] (Vec.(::) (Prelude.Types.S Prelude.Types.Z) (Prelude.Basics.List Prelude.Types.Nat) (Prelude.Basics.Nil Prelude.Types.Nat) (Vec.(::) Prelude.Types.Z (Prelude.Basics.List Prelude.Types.Nat) (Prelude.Basics.(::) Prelude.Types.Nat Prelude.Types.Z (Prelude.Basics.Nil Prelude.Types.Nat)) (Vec.Nil (Prelude.Basics.List Prelude.Types.Nat))))
Vec> Bye for now! Vec> Bye for now!

8
tests/idris2/basic/basic044/run
View File

@ -1,8 +1,4 @@
. ../../../testutils.sh . ../../../testutils.sh
echo ":q" | idris2 --log unify.equal:10 --log unify:5 Term.idr \ echo ":q" | idris2 --log unify.equal:10 --log unify:5 Term.idr | clean_names
| sed -E "s/[0-9]+}/N}/g" | sed -E "s/resolved([0-9]+)/resolvedN/g" \ echo ":q" | idris2 --log unify:3 --log elab.ambiguous:5 Vec.idr | clean_names
| sed -E "s/case in ([0-9]+)/case in N/g" | sed -E "s/[0-9]+:[0-9]+/L:C/g"
echo ":q" | idris2 --log unify:3 --log elab.ambiguous:5 Vec.idr \
| sed -E "s/[0-9]+}/N}/g" | sed -E "s/resolved([0-9]+)/resolvedN/g" \
| sed -E "s/case in ([0-9]+)/case in N/g" | sed -E "s/[0-9]+:[0-9]+/L:C/g"

64
tests/idris2/evaluator/spec001/expected
View File

@ -1,12 +1,12 @@
1/1: Building Mult3 (Mult3.idr) 1/1: Building Mult3 (Mult3.idr)
LOG specialise.declare:5: Specialising Main.smult ($resolved2645) -> _PE.PE_smult_4e8901402355876e by (0, Static (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z)))), (1, Dynamic) LOG specialise.declare:5: Specialising Main.smult ($resolved1) -> _PE.PE_smult_4e8901402355876e by (0, Static (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z)))), (1, Dynamic)
LOG specialise:3: Specialised type _PE.PE_smult_4e8901402355876e: (n : Prelude.Types.Nat) -> Prelude.Types.Nat LOG specialise:3: Specialised type _PE.PE_smult_4e8901402355876e: (n : Prelude.Types.Nat) -> Prelude.Types.Nat
LOG specialise:5: Attempting to specialise: LOG specialise:5: Attempting to specialise:
((Main.smult Prelude.Types.Z) n) = Prelude.Types.Z ((Main.smult Prelude.Types.Z) n) = Prelude.Types.Z
((Main.smult (Prelude.Types.S Prelude.Types.Z)) n) = n ((Main.smult (Prelude.Types.S Prelude.Types.Z)) n) = n
((Main.smult (Prelude.Types.S m)) n) = ((((Prelude.Num.(+) [ty = Prelude.Types.Nat]) [__con = Prelude.Types.Num implementation at Prelude.Types:66:1--71:33]) n) ((Main.smult m) n)) ((Main.smult (Prelude.Types.S m)) n) = ((((Prelude.Num.(+) [ty = Prelude.Types.Nat]) [__con = Prelude.Types.Num implementation at Prelude.Types:1]) n) ((Main.smult m) n))
LOG specialise:5: New patterns for _PE.PE_smult_4e8901402355876e: LOG specialise:5: New patterns for _PE.PE_smult_4e8901402355876e:
(_PE.PE_smult_4e8901402355876e $_pe0) = (($resolved2645 (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z)))) _pe0) (_PE.PE_smult_4e8901402355876e $_pe0) = (($resolved1 (Prelude.Types.S (Prelude.Types.S (Prelude.Types.S Prelude.Types.Z)))) _pe0)
LOG specialise:5: New RHS: (Prelude.Types.plus _pe0[0] (Prelude.Types.plus _pe0[0] _pe0[0])) LOG specialise:5: New RHS: (Prelude.Types.plus _pe0[0] (Prelude.Types.plus _pe0[0] _pe0[0]))
LOG specialise:5: Already specialised _PE.PE_smult_4e8901402355876e LOG specialise:5: Already specialised _PE.PE_smult_4e8901402355876e
/* Main.main : IO () */ /* Main.main : IO () */
@ -16,29 +16,29 @@ function Main_main($0) {
return Prelude_IO_prim__putStr((Prelude_Show_show_Show_Nat(($4+($4+$4)))+'\n'), $0); return Prelude_IO_prim__putStr((Prelude_Show_show_Show_Nat(($4+($4+$4)))+'\n'), $0);
} }
1/1: Building Desc (Desc.idr) 1/1: Building Desc (Desc.idr)
LOG specialise.declare:5: Specialising Desc.fold ($resolved2758) -> _PE.PE_fold_3a845f1ca594c582 by (0, Dynamic), (1, Static (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))), (2, Dynamic) LOG specialise.declare:5: Specialising Desc.fold ($resolved2) -> _PE.PE_fold_3a845f1ca594c582 by (0, Dynamic), (1, Static (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))), (2, Dynamic)
LOG specialise:3: Specialised type _PE.PE_fold_3a845f1ca594c582: {0 a : Type} -> ({arg:936} : ({arg:938} : (Desc.Meaning (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec)) a[0])) -> a[1]) -> ({arg:943} : (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec)))) -> a[2] LOG specialise:3: Specialised type _PE.PE_fold_3a845f1ca594c582: {0 a : Type} -> ({arg:1} : ({arg:1} : (Desc.Meaning (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec)) a[0])) -> a[1]) -> ({arg:2} : (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec)))) -> a[2]
LOG specialise:5: Attempting to specialise: LOG specialise:5: Attempting to specialise:
((((Desc.fold [a = a]) [d = d]) alg) ((Desc.MkMu [d = d]) t)) = (alg (((((Desc.fmap [b = a]) [a = ?a]) d) ((Builtin.assert_total [a = ?a]) (((Desc.fold [a = a]) [d = d]) alg))) t)) ((((Desc.fold [a = a]) [d = d]) alg) ((Desc.MkMu [d = d]) t)) = (alg (((((Desc.fmap [b = a]) [a = ?a]) d) ((Builtin.assert_total [a = ?a]) (((Desc.fold [a = a]) [d = d]) alg))) t))
LOG specialise:5: New patterns for _PE.PE_fold_3a845f1ca594c582: LOG specialise:5: New patterns for _PE.PE_fold_3a845f1ca594c582:
(((_PE.PE_fold_3a845f1ca594c582 [a = a]) alg) ((Desc.MkMu [d = ((Desc.Sum Desc.Stop) ((Desc.Prod Desc.Rec) Desc.Rec))]) t)) = (alg (((((Desc.fmap [b = a]) [a = ?]) ((Desc.Sum Desc.Stop) ((Desc.Prod Desc.Rec) Desc.Rec))) ((Builtin.assert_total [a = ?]) (((Desc.fold [a = a]) [d = ((Desc.Sum Desc.Stop) ((Desc.Prod Desc.Rec) Desc.Rec))]) alg))) t)) (((_PE.PE_fold_3a845f1ca594c582 [a = a]) alg) ((Desc.MkMu [d = ((Desc.Sum Desc.Stop) ((Desc.Prod Desc.Rec) Desc.Rec))]) t)) = (alg (((((Desc.fmap [b = a]) [a = ?]) ((Desc.Sum Desc.Stop) ((Desc.Prod Desc.Rec) Desc.Rec))) ((Builtin.assert_total [a = ?]) (((Desc.fold [a = a]) [d = ((Desc.Sum Desc.Stop) ((Desc.Prod Desc.Rec) Desc.Rec))]) alg))) t))
LOG specialise:5: Already specialised _PE.PE_fold_3a845f1ca594c582 LOG specialise:5: Already specialised _PE.PE_fold_3a845f1ca594c582
LOG specialise:5: Already specialised _PE.PE_fold_3a845f1ca594c582 LOG specialise:5: Already specialised _PE.PE_fold_3a845f1ca594c582
LOG specialise:5: New RHS: (alg[0] (Prelude.Types.bimap (Builtin.Pair a[1] a[1]) (Builtin.Pair (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))) (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec)))) Builtin.Unit Builtin.Unit (Prelude.Basics.id Builtin.Unit) \({arg:2} : (Builtin.Pair (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))) (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))))) => (Prelude.Types.bimap a[2] (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))) a[2] (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))) (_PE.PE_fold_3a845f1ca594c582 a[2] alg[1]) (_PE.PE_fold_3a845f1ca594c582 a[2] alg[1]) {arg:2}[0]) t[2])) LOG specialise:5: New RHS: (alg[0] (Prelude.Types.bimap (Builtin.Pair a[1] a[1]) (Builtin.Pair (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))) (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec)))) Builtin.Unit Builtin.Unit (Prelude.Basics.id Builtin.Unit) \({arg:3} : (Builtin.Pair (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))) (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))))) => (Prelude.Types.bimap a[2] (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))) a[2] (Desc.Mu (Desc.Sum Desc.Stop (Desc.Prod Desc.Rec Desc.Rec))) (_PE.PE_fold_3a845f1ca594c582 a[2] alg[1]) (_PE.PE_fold_3a845f1ca594c582 a[2] alg[1]) {arg:3}[0]) t[2]))
LOG specialise:5: Already specialised _PE.PE_fold_3a845f1ca594c582 LOG specialise:5: Already specialised _PE.PE_fold_3a845f1ca594c582
1/1: Building Desc2 (Desc2.idr) 1/1: Building Desc2 (Desc2.idr)
LOG specialise.declare:5: Specialising Main.fold ($resolved2668) -> _PE.PE_fold_8abb50b713fe8e5e by (0, Static Prelude.Types.Nat), (1, Static Prelude.Basics.List), (2, Static (Prelude.Interfaces.MkFunctor Prelude.Basics.List \{0 b : Type} => \{0 a : Type} => \(func : ({arg:8742} : a[0]) -> b[2]) => \({arg:8747} : (Prelude.Basics.List a[1])) => (Prelude.Types.List.mapImpl b[3] a[2] func[1] {arg:8747}[0]))), (3, Dynamic) LOG specialise.declare:5: Specialising Main.fold ($resolved3) -> _PE.PE_fold_8abb50b713fe8e5e by (0, Static Prelude.Types.Nat), (1, Static Prelude.Basics.List), (2, Static (Prelude.Interfaces.MkFunctor Prelude.Basics.List \{0 b : Type} => \{0 a : Type} => \(func : ({arg:4} : a[0]) -> b[2]) => \({arg:4} : (Prelude.Basics.List a[1])) => (Prelude.Types.List.mapImpl b[3] a[2] func[1] {arg:4}[0]))), (3, Dynamic)
LOG specialise:3: Specialised type _PE.PE_fold_8abb50b713fe8e5e: ({arg:840} : ({arg:842} : (Prelude.Basics.List Prelude.Types.Nat)) -> Prelude.Types.Nat) -> ({arg:847} : (Main.Mu Prelude.Basics.List)) -> Prelude.Types.Nat LOG specialise:3: Specialised type _PE.PE_fold_8abb50b713fe8e5e: ({arg:5} : ({arg:5} : (Prelude.Basics.List Prelude.Types.Nat)) -> Prelude.Types.Nat) -> ({arg:5} : (Main.Mu Prelude.Basics.List)) -> Prelude.Types.Nat
LOG specialise:5: Attempting to specialise: LOG specialise:5: Attempting to specialise:
(((((Main.fold [a = a]) [f = f]) [fun = fun]) alg) ((Main.MkMu [f = f]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = a]) [a = (Main.Mu f)]) [f = f]) [{conArg:8796} = fun]) ((((Main.fold [a = a]) [f = f]) [fun = fun]) alg)) t)) (((((Main.fold [a = a]) [f = f]) [fun = fun]) alg) ((Main.MkMu [f = f]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = a]) [a = (Main.Mu f)]) [f = f]) [{conArg:1} = fun]) ((((Main.fold [a = a]) [f = f]) [fun = fun]) alg)) t))
LOG specialise:5: New patterns for _PE.PE_fold_8abb50b713fe8e5e: LOG specialise:5: New patterns for _PE.PE_fold_8abb50b713fe8e5e:
((_PE.PE_fold_8abb50b713fe8e5e alg) ((Main.MkMu [f = Prelude.Basics.List]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = Prelude.Types.Nat]) [a = (Main.Mu Prelude.Basics.List)]) [f = Prelude.Basics.List]) [{conArg:8796} = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8742}) a b) (%lam RigW Explicit (Just {arg:8747}) (Prelude.Basics.List a) ((((Prelude.Types.List.mapImpl [b = b]) [a = a]) func) {arg:8747}))))))]) ((((Main.fold [a = Prelude.Types.Nat]) [f = Prelude.Basics.List]) [fun = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8742}) a b) (%lam RigW Explicit (Just {arg:8747}) (Prelude.Basics.List a) ((((Prelude.Types.List.mapImpl [b = b]) [a = a]) func) {arg:8747}))))))]) alg)) t)) ((_PE.PE_fold_8abb50b713fe8e5e alg) ((Main.MkMu [f = Prelude.Basics.List]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = Prelude.Types.Nat]) [a = (Main.Mu Prelude.Basics.List)]) [f = Prelude.Basics.List]) [{conArg:1} = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:4}) a b) (%lam RigW Explicit (Just {arg:4}) (Prelude.Basics.List a) ((((Prelude.Types.List.mapImpl [b = b]) [a = a]) func) {arg:4}))))))]) ((((Main.fold [a = Prelude.Types.Nat]) [f = Prelude.Basics.List]) [fun = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:4}) a b) (%lam RigW Explicit (Just {arg:4}) (Prelude.Basics.List a) ((((Prelude.Types.List.mapImpl [b = b]) [a = a]) func) {arg:4}))))))]) alg)) t))
LOG specialise.declare:5: Specialising Main.fold ($resolved2668) -> _PE.PE_fold_a727631bc09e3761 by (0, Static Prelude.Types.Nat), (1, Static Prelude.Basics.List), (2, Static (Prelude.Interfaces.MkFunctor Prelude.Basics.List \{0 b : Type} => \{0 a : Type} => \(func : ({arg:8742} : a[0]) -> b[2]) => \({arg:8747} : (Prelude.Basics.List a[1])) => (Prelude.Types.List.mapAppend a[2] b[3] (Prelude.Basics.Lin b[3]) func[1] {arg:8747}[0]))), (3, Dynamic) LOG specialise.declare:5: Specialising Main.fold ($resolved3) -> _PE.PE_fold_a727631bc09e3761 by (0, Static Prelude.Types.Nat), (1, Static Prelude.Basics.List), (2, Static (Prelude.Interfaces.MkFunctor Prelude.Basics.List \{0 b : Type} => \{0 a : Type} => \(func : ({arg:4} : a[0]) -> b[2]) => \({arg:4} : (Prelude.Basics.List a[1])) => (Prelude.Types.List.mapAppend a[2] b[3] (Prelude.Basics.Lin b[3]) func[1] {arg:4}[0]))), (3, Dynamic)
LOG specialise:3: Specialised type _PE.PE_fold_a727631bc09e3761: ({arg:840} : ({arg:842} : (Prelude.Basics.List Prelude.Types.Nat)) -> Prelude.Types.Nat) -> ({arg:847} : (Main.Mu Prelude.Basics.List)) -> Prelude.Types.Nat LOG specialise:3: Specialised type _PE.PE_fold_a727631bc09e3761: ({arg:5} : ({arg:5} : (Prelude.Basics.List Prelude.Types.Nat)) -> Prelude.Types.Nat) -> ({arg:5} : (Main.Mu Prelude.Basics.List)) -> Prelude.Types.Nat
LOG specialise:5: Attempting to specialise: LOG specialise:5: Attempting to specialise:
(((((Main.fold [a = a]) [f = f]) [fun = fun]) alg) ((Main.MkMu [f = f]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = a]) [a = (Main.Mu f)]) [f = f]) [{conArg:8796} = fun]) ((((Main.fold [a = a]) [f = f]) [fun = fun]) alg)) t)) (((((Main.fold [a = a]) [f = f]) [fun = fun]) alg) ((Main.MkMu [f = f]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = a]) [a = (Main.Mu f)]) [f = f]) [{conArg:1} = fun]) ((((Main.fold [a = a]) [f = f]) [fun = fun]) alg)) t))
LOG specialise:5: New patterns for _PE.PE_fold_a727631bc09e3761: LOG specialise:5: New patterns for _PE.PE_fold_a727631bc09e3761:
((_PE.PE_fold_a727631bc09e3761 alg) ((Main.MkMu [f = Prelude.Basics.List]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = Prelude.Types.Nat]) [a = (Main.Mu Prelude.Basics.List)]) [f = Prelude.Basics.List]) [{conArg:8796} = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8742}) a b) (%lam RigW Explicit (Just {arg:8747}) (Prelude.Basics.List a) (((((Prelude.Types.List.mapAppend [a = a]) [b = b]) (Prelude.Basics.Lin [a = b])) func) {arg:8747}))))))]) ((((Main.fold [a = Prelude.Types.Nat]) [f = Prelude.Basics.List]) [fun = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:8742}) a b) (%lam RigW Explicit (Just {arg:8747}) (Prelude.Basics.List a) (((((Prelude.Types.List.mapAppend [a = a]) [b = b]) (Prelude.Basics.Lin [a = b])) func) {arg:8747}))))))]) alg)) t)) ((_PE.PE_fold_a727631bc09e3761 alg) ((Main.MkMu [f = Prelude.Basics.List]) t)) = (alg ((((((Prelude.Interfaces.(<$>) [b = Prelude.Types.Nat]) [a = (Main.Mu Prelude.Basics.List)]) [f = Prelude.Basics.List]) [{conArg:1} = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:4}) a b) (%lam RigW Explicit (Just {arg:4}) (Prelude.Basics.List a) (((((Prelude.Types.List.mapAppend [a = a]) [b = b]) (Prelude.Basics.Lin [a = b])) func) {arg:4}))))))]) ((((Main.fold [a = Prelude.Types.Nat]) [f = Prelude.Basics.List]) [fun = ((Prelude.Interfaces.MkFunctor [f = Prelude.Basics.List]) (%lam Rig0 Implicit (Just b) %type (%lam Rig0 Implicit (Just a) %type (%lam RigW Explicit (Just func) (%pi RigW Explicit (Just {arg:4}) a b) (%lam RigW Explicit (Just {arg:4}) (Prelude.Basics.List a) (((((Prelude.Types.List.mapAppend [a = a]) [b = b]) (Prelude.Basics.Lin [a = b])) func) {arg:4}))))))]) alg)) t))
LOG specialise:5: Already specialised _PE.PE_fold_a727631bc09e3761 LOG specialise:5: Already specialised _PE.PE_fold_a727631bc09e3761
LOG specialise:5: New RHS: (alg[0] (Prelude.Types.List.mapAppend (Main.Mu Prelude.Basics.List) Prelude.Types.Nat (Prelude.Basics.Lin Prelude.Types.Nat) (_PE.PE_fold_a727631bc09e3761 alg[0]) t[1])) LOG specialise:5: New RHS: (alg[0] (Prelude.Types.List.mapAppend (Main.Mu Prelude.Basics.List) Prelude.Types.Nat (Prelude.Basics.Lin Prelude.Types.Nat) (_PE.PE_fold_a727631bc09e3761 alg[0]) t[1]))
LOG specialise:5: Already specialised _PE.PE_fold_a727631bc09e3761 LOG specialise:5: Already specialised _PE.PE_fold_a727631bc09e3761
@ -47,8 +47,8 @@ LOG specialise:5: Already specialised _PE.PE_fold_8abb50b713fe8e5e
LOG specialise:5: New RHS: (alg[0] (Prelude.Types.List.mapAppend (Main.Mu Prelude.Basics.List) Prelude.Types.Nat (Prelude.Basics.Lin Prelude.Types.Nat) (_PE.PE_fold_a727631bc09e3761 alg[0]) t[1])) LOG specialise:5: New RHS: (alg[0] (Prelude.Types.List.mapAppend (Main.Mu Prelude.Basics.List) Prelude.Types.Nat (Prelude.Basics.Lin Prelude.Types.Nat) (_PE.PE_fold_a727631bc09e3761 alg[0]) t[1]))
LOG specialise:5: Already specialised _PE.PE_fold_8abb50b713fe8e5e LOG specialise:5: Already specialised _PE.PE_fold_8abb50b713fe8e5e
1/1: Building Identity (Identity.idr) 1/1: Building Identity (Identity.idr)
LOG specialise.declare:5: Specialising Main.identity ($resolved2645) -> _PE.PE_identity_3c7f5598e5c9b732 by (0, Static Prelude.Types.Nat), (1, Dynamic) LOG specialise.declare:5: Specialising Main.identity ($resolved1) -> _PE.PE_identity_3c7f5598e5c9b732 by (0, Static Prelude.Types.Nat), (1, Dynamic)
LOG specialise:3: Specialised type _PE.PE_identity_3c7f5598e5c9b732: ({arg:813} : (Prelude.Basics.List Prelude.Types.Nat)) -> (Prelude.Basics.List Prelude.Types.Nat) LOG specialise:3: Specialised type _PE.PE_identity_3c7f5598e5c9b732: ({arg:6} : (Prelude.Basics.List Prelude.Types.Nat)) -> (Prelude.Basics.List Prelude.Types.Nat)
LOG specialise:5: Attempting to specialise: LOG specialise:5: Attempting to specialise:
((Main.identity [a = a]) (Prelude.Basics.Nil [a = a])) = (Prelude.Basics.Nil [a = a]) ((Main.identity [a = a]) (Prelude.Basics.Nil [a = a])) = (Prelude.Basics.Nil [a = a])
((Main.identity [a = a]) (((Prelude.Basics.(::) [a = a]) x) xs)) = (((Prelude.Basics.(::) [a = a]) x) ((Main.identity [a = a]) xs)) ((Main.identity [a = a]) (((Prelude.Basics.(::) [a = a]) x) xs)) = (((Prelude.Basics.(::) [a = a]) x) ((Main.identity [a = a]) xs))
@ -60,26 +60,26 @@ LOG specialise:5: Already specialised _PE.PE_identity_3c7f5598e5c9b732
LOG specialise:5: New RHS: (Prelude.Basics.(::) Prelude.Types.Nat x[1] (_PE.PE_identity_3c7f5598e5c9b732 xs[0])) LOG specialise:5: New RHS: (Prelude.Basics.(::) Prelude.Types.Nat x[1] (_PE.PE_identity_3c7f5598e5c9b732 xs[0]))
LOG specialise:5: Already specialised _PE.PE_identity_3c7f5598e5c9b732 LOG specialise:5: Already specialised _PE.PE_identity_3c7f5598e5c9b732
LOG compiler.identity:5: found identity flag for: _PE.PE_identity_3c7f5598e5c9b732, 0 LOG compiler.identity:5: found identity flag for: _PE.PE_identity_3c7f5598e5c9b732, 0
old def: Just [{arg:0}]: (%case !{arg:0} [(%concase [nil] Prelude.Basics.Nil Just 0 [] (%con [nil] Prelude.Basics.Nil Just 0 [])), (%concase [cons] Prelude.Basics.(::) Just 1 [{e:2}, {e:3}] (%con [cons] Prelude.Basics.(::) Just 1 [!{e:2}, (_PE.PE_identity_3c7f5598e5c9b732 [!{e:3}])]))] Nothing) old def: Just [{arg:3}]: (%case !{arg:3} [(%concase [nil] Prelude.Basics.Nil Just 0 [] (%con [nil] Prelude.Basics.Nil Just 0 [])), (%concase [cons] Prelude.Basics.(::) Just 1 [{e:2}, {e:3}] (%con [cons] Prelude.Basics.(::) Just 1 [!{e:2}, (_PE.PE_identity_3c7f5598e5c9b732 [!{e:3}])]))] Nothing)
LOG compiler.identity:5: new def: [{arg:0}]: !{arg:0} LOG compiler.identity:5: new def: [{arg:3}]: !{arg:3}
LOG compiler.identity:5: found identity flag for: Main.identity, 0 LOG compiler.identity:5: found identity flag for: Main.identity, 0
old def: Just [{arg:1}]: (%case !{arg:1} [(%concase [nil] Prelude.Basics.Nil Just 0 [] (%con [nil] Prelude.Basics.Nil Just 0 [])), (%concase [cons] Prelude.Basics.(::) Just 1 [{e:2}, {e:3}] (%con [cons] Prelude.Basics.(::) Just 1 [!{e:2}, (Main.identity [!{e:3}])]))] Nothing) old def: Just [{arg:3}]: (%case !{arg:3} [(%concase [nil] Prelude.Basics.Nil Just 0 [] (%con [nil] Prelude.Basics.Nil Just 0 [])), (%concase [cons] Prelude.Basics.(::) Just 1 [{e:2}, {e:3}] (%con [cons] Prelude.Basics.(::) Just 1 [!{e:2}, (Main.identity [!{e:3}])]))] Nothing)
LOG compiler.identity:5: new def: [{arg:1}]: !{arg:1} LOG compiler.identity:5: new def: [{arg:3}]: !{arg:3}
LOG compiler.identity:5: found identity flag for: _PE.PE_identity_3c7f5598e5c9b732, 0 LOG compiler.identity:5: found identity flag for: _PE.PE_identity_3c7f5598e5c9b732, 0
old def: Just [{arg:0}]: !{arg:0} old def: Just [{arg:3}]: !{arg:3}
LOG compiler.identity:5: new def: [{arg:0}]: !{arg:0} LOG compiler.identity:5: new def: [{arg:3}]: !{arg:3}
LOG compiler.identity:5: found identity flag for: Main.identity, 0 LOG compiler.identity:5: found identity flag for: Main.identity, 0
old def: Just [{arg:1}]: !{arg:1} old def: Just [{arg:3}]: !{arg:3}
LOG compiler.identity:5: new def: [{arg:1}]: !{arg:1} LOG compiler.identity:5: new def: [{arg:3}]: !{arg:3}
LOG compiler.identity:5: found identity flag for: Main.test, 0 LOG compiler.identity:5: found identity flag for: Main.test, 0
old def: Just [{arg:0}]: !{arg:0} old def: Just [{arg:3}]: !{arg:3}
LOG compiler.identity:5: new def: [{arg:0}]: !{arg:0} LOG compiler.identity:5: new def: [{arg:3}]: !{arg:3}
LOG compiler.identity:5: found identity flag for: _PE.PE_identity_3c7f5598e5c9b732, 0 LOG compiler.identity:5: found identity flag for: _PE.PE_identity_3c7f5598e5c9b732, 0
old def: Just [{arg:0}]: !{arg:0} old def: Just [{arg:3}]: !{arg:3}
LOG compiler.identity:5: new def: [{arg:0}]: !{arg:0} LOG compiler.identity:5: new def: [{arg:3}]: !{arg:3}
LOG compiler.identity:5: found identity flag for: Main.identity, 0 LOG compiler.identity:5: found identity flag for: Main.identity, 0
old def: Just [{arg:1}]: !{arg:1} old def: Just [{arg:3}]: !{arg:3}
LOG compiler.identity:5: new def: [{arg:1}]: !{arg:1} LOG compiler.identity:5: new def: [{arg:3}]: !{arg:3}
LOG compiler.identity:5: found identity flag for: Main.test, 0 LOG compiler.identity:5: found identity flag for: Main.test, 0
old def: Just [{arg:0}]: !{arg:0} old def: Just [{arg:3}]: !{arg:3}
LOG compiler.identity:5: new def: [{arg:0}]: !{arg:0} LOG compiler.identity:5: new def: [{arg:3}]: !{arg:3}

2
tests/idris2/evaluator/spec001/run
View File

@ -1,8 +1,10 @@
. ../../../testutils.sh . ../../../testutils.sh
{
idris2 --log specialise:5 -c Mult3.idr idris2 --log specialise:5 -c Mult3.idr
idris2 --cg node -o mult3.js -c Mult3.idr idris2 --cg node -o mult3.js -c Mult3.idr
awk -v RS= '/\/\* Main.main/' build/exec/mult3.js awk -v RS= '/\/\* Main.main/' build/exec/mult3.js
idris2 --log specialise:5 -c Desc.idr idris2 --log specialise:5 -c Desc.idr
idris2 --log specialise:5 -c Desc2.idr idris2 --log specialise:5 -c Desc2.idr
idris2 --log specialise:5 -c Identity.idr idris2 --log specialise:5 -c Identity.idr
} | clean_names

4
tests/idris2/reflection/reflection010/expected
View File

@ -1,10 +1,10 @@
1/1: Building Name (Name.idr) 1/1: Building Name (Name.idr)
LOG declare.data:1: Processing Main.Identity LOG declare.data:1: Processing Main.Identity
LOG declare.type:1: Processing Main.nested LOG declare.type:1: Processing Main.nested
LOG declare.type:1: Processing Main.N:N:foo LOG declare.type:1: Processing Main.1:foo
LOG declare.type:1: Processing Main.cased LOG declare.type:1: Processing Main.cased
LOG declare.type:1: Processing Main.test LOG declare.type:1: Processing Main.test
LOG 1: nested: ((Main.MkIdentity [a = Int]) Main.N:N:foo) LOG 1: nested: ((Main.MkIdentity [a = Int]) Main.1:foo)
LOG 1: True LOG 1: True
LOG 1: cased: (%lam RigW Explicit (Just {lamc:0}) (Main.Identity Int) (Main.case block in cased {lamc:0})) LOG 1: cased: (%lam RigW Explicit (Just {lamc:0}) (Main.Identity Int) (Main.case block in cased {lamc:0}))
LOG 1: 10 LOG 1: 10

2
tests/idris2/reflection/reflection010/run
View File

@ -1,3 +1,3 @@
. ../../../testutils.sh . ../../../testutils.sh
check Name.idr | sed -E "s/\.[0-9]+:[0-9]+/\.N:N/" check Name.idr | clean_names

20
tests/idris2/reflection/reflection025/expected
View File

@ -4,7 +4,7 @@ LOG elab:0: - prim__sub_Integer
LOG elab:0: - prim__lte_Integer LOG elab:0: - prim__lte_Integer
LOG elab:0: - Prelude.Types.case block in "integerToNat" LOG elab:0: - Prelude.Types.case block in "integerToNat"
LOG elab:0: - Prelude.Types.fromInteger LOG elab:0: - Prelude.Types.fromInteger
LOG elab:0: - Prelude.Types.Num implementation at Prelude.Types:66:1--71:33 LOG elab:0: - Prelude.Types.Num implementation at Prelude.Types:1
LOG elab:0: - Prelude.Types.+ LOG elab:0: - Prelude.Types.+
LOG elab:0: - Prelude.Types.* LOG elab:0: - Prelude.Types.*
LOG elab:0: - Prelude.Types.plus LOG elab:0: - Prelude.Types.plus
@ -43,7 +43,7 @@ LOG elab:0: current fn: [< CurrFn.f]
LOG elab:0: current fn: [< CurrFn.f'] LOG elab:0: current fn: [< CurrFn.f']
LOG elab:0: current fn: [< CurrFn.f''] LOG elab:0: current fn: [< CurrFn.f'']
LOG elab:0: current fn: [< CurrFn.f''', CurrFn.case block in "f'''"] LOG elab:0: current fn: [< CurrFn.f''', CurrFn.case block in "f'''"]
LOG elab:0: current fn: [< CurrFn.n, CurrFn.<nums>:<nums>:f] LOG elab:0: current fn: [< CurrFn.n, CurrFn.1:f]
LOG elab:0: current fn: [< CurrFn.w, CurrFn.with block in "w"] LOG elab:0: current fn: [< CurrFn.w, CurrFn.with block in "w"]
LOG elab:0: current fn: [< CurrFn.w, CurrFn.with block in "w"] LOG elab:0: current fn: [< CurrFn.w, CurrFn.with block in "w"]
------------ ------------
@ -53,7 +53,7 @@ LOG elab:0: === current fn: [< RefDefsDeep.f] ===
LOG elab:0: === current fn: [< RefDefsDeep.f'] === LOG elab:0: === current fn: [< RefDefsDeep.f'] ===
LOG elab:0: === current fn: [< RefDefsDeep.f''] === LOG elab:0: === current fn: [< RefDefsDeep.f''] ===
LOG elab:0: === current fn: [< RefDefsDeep.f''', RefDefsDeep.case block in "f'''"] === LOG elab:0: === current fn: [< RefDefsDeep.f''', RefDefsDeep.case block in "f'''"] ===
LOG elab:0: === current fn: [< RefDefsDeep.n, RefDefsDeep.<nums>:<nums>:f] === LOG elab:0: === current fn: [< RefDefsDeep.n, RefDefsDeep.1:f] ===
LOG elab:0: === current fn: [< RefDefsDeep.w, RefDefsDeep.with block in "w"] === LOG elab:0: === current fn: [< RefDefsDeep.w, RefDefsDeep.with block in "w"] ===
LOG elab:0: === current fn: [< RefDefsDeep.w, RefDefsDeep.with block in "w"] === LOG elab:0: === current fn: [< RefDefsDeep.w, RefDefsDeep.with block in "w"] ===
LOG elab:0: Names `RefDefsDeep.f` refers to: LOG elab:0: Names `RefDefsDeep.f` refers to:
@ -61,7 +61,7 @@ LOG elab:0: - prim__sub_Integer
LOG elab:0: - prim__lte_Integer LOG elab:0: - prim__lte_Integer
LOG elab:0: - Prelude.Types.case block in "integerToNat" LOG elab:0: - Prelude.Types.case block in "integerToNat"
LOG elab:0: - Prelude.Types.fromInteger LOG elab:0: - Prelude.Types.fromInteger
LOG elab:0: - Prelude.Types.Num implementation at Prelude.Types:66:1--71:33 LOG elab:0: - Prelude.Types.Num implementation at Prelude.Types:1
LOG elab:0: - Prelude.Types.+ LOG elab:0: - Prelude.Types.+
LOG elab:0: - Prelude.Types.* LOG elab:0: - Prelude.Types.*
LOG elab:0: - Prelude.Types.plus LOG elab:0: - Prelude.Types.plus
@ -84,7 +84,7 @@ LOG elab:0: - prim__sub_Integer
LOG elab:0: - prim__lte_Integer LOG elab:0: - prim__lte_Integer
LOG elab:0: - Prelude.Types.case block in "integerToNat" LOG elab:0: - Prelude.Types.case block in "integerToNat"
LOG elab:0: - Prelude.Types.fromInteger LOG elab:0: - Prelude.Types.fromInteger
LOG elab:0: - Prelude.Types.Num implementation at Prelude.Types:66:1--71:33 LOG elab:0: - Prelude.Types.Num implementation at Prelude.Types:1
LOG elab:0: - Prelude.Types.+ LOG elab:0: - Prelude.Types.+
LOG elab:0: - Prelude.Types.* LOG elab:0: - Prelude.Types.*
LOG elab:0: - Prelude.Types.plus LOG elab:0: - Prelude.Types.plus
@ -107,7 +107,7 @@ LOG elab:0: - prim__sub_Integer
LOG elab:0: - prim__lte_Integer LOG elab:0: - prim__lte_Integer
LOG elab:0: - Prelude.Types.case block in "integerToNat" LOG elab:0: - Prelude.Types.case block in "integerToNat"
LOG elab:0: - Prelude.Types.fromInteger LOG elab:0: - Prelude.Types.fromInteger
LOG elab:0: - Prelude.Types.Num implementation at Prelude.Types:66:1--71:33 LOG elab:0: - Prelude.Types.Num implementation at Prelude.Types:1
LOG elab:0: - Prelude.Types.+ LOG elab:0: - Prelude.Types.+
LOG elab:0: - Prelude.Types.* LOG elab:0: - Prelude.Types.*
LOG elab:0: - Prelude.Types.plus LOG elab:0: - Prelude.Types.plus
@ -132,7 +132,7 @@ LOG elab:0: - prim__sub_Integer
LOG elab:0: - prim__lte_Integer LOG elab:0: - prim__lte_Integer
LOG elab:0: - Prelude.Types.case block in "integerToNat" LOG elab:0: - Prelude.Types.case block in "integerToNat"
LOG elab:0: - Prelude.Types.fromInteger LOG elab:0: - Prelude.Types.fromInteger
LOG elab:0: - Prelude.Types.Num implementation at Prelude.Types:66:1--71:33 LOG elab:0: - Prelude.Types.Num implementation at Prelude.Types:1
LOG elab:0: - Prelude.Types.+ LOG elab:0: - Prelude.Types.+
LOG elab:0: - Prelude.Types.* LOG elab:0: - Prelude.Types.*
LOG elab:0: - Prelude.Types.plus LOG elab:0: - Prelude.Types.plus
@ -158,7 +158,7 @@ LOG elab:0: - prim__sub_Integer
LOG elab:0: - prim__lte_Integer LOG elab:0: - prim__lte_Integer
LOG elab:0: - Prelude.Types.case block in "integerToNat" LOG elab:0: - Prelude.Types.case block in "integerToNat"
LOG elab:0: - Prelude.Types.fromInteger LOG elab:0: - Prelude.Types.fromInteger
LOG elab:0: - Prelude.Types.Num implementation at Prelude.Types:66:1--71:33 LOG elab:0: - Prelude.Types.Num implementation at Prelude.Types:1
LOG elab:0: - Prelude.Types.+ LOG elab:0: - Prelude.Types.+
LOG elab:0: - Prelude.Types.* LOG elab:0: - Prelude.Types.*
LOG elab:0: - Prelude.Types.plus LOG elab:0: - Prelude.Types.plus
@ -174,7 +174,7 @@ LOG elab:0: - Prelude.Basics.True
LOG elab:0: - Prelude.Basics.False LOG elab:0: - Prelude.Basics.False
LOG elab:0: - Builtin.assert_total LOG elab:0: - Builtin.assert_total
LOG elab:0: - Builtin.MkUnit LOG elab:0: - Builtin.MkUnit
LOG elab:0: - RefDefsDeep.<nums>:<nums>:f LOG elab:0: - RefDefsDeep.1:f
LOG elab:0: - RefDefsDeep.case block in "n,f" LOG elab:0: - RefDefsDeep.case block in "n,f"
LOG elab:0: LOG elab:0:
LOG elab:0: Names `RefDefsDeep.w` refers to: LOG elab:0: Names `RefDefsDeep.w` refers to:
@ -182,7 +182,7 @@ LOG elab:0: - prim__sub_Integer
LOG elab:0: - prim__lte_Integer LOG elab:0: - prim__lte_Integer
LOG elab:0: - Prelude.Types.case block in "integerToNat" LOG elab:0: - Prelude.Types.case block in "integerToNat"
LOG elab:0: - Prelude.Types.fromInteger LOG elab:0: - Prelude.Types.fromInteger
LOG elab:0: - Prelude.Types.Num implementation at Prelude.Types:66:1--71:33 LOG elab:0: - Prelude.Types.Num implementation at Prelude.Types:1
LOG elab:0: - Prelude.Types.+ LOG elab:0: - Prelude.Types.+
LOG elab:0: - Prelude.Types.* LOG elab:0: - Prelude.Types.*
LOG elab:0: - Prelude.Types.plus LOG elab:0: - Prelude.Types.plus

2
tests/idris2/reflection/reflection025/run
View File

@ -8,4 +8,4 @@ echo ------------
check RefDefsDeep.idr check RefDefsDeep.idr
echo ------------ echo ------------
check InspectRec.idr check InspectRec.idr
} | sed -e 's/\.[0-9]*:[0-9]*:/.<nums>:<nums>:/' } | clean_names

8
tests/idris2/total/total012/expected
View File

@ -1,6 +1,6 @@
1/1: Building Issue1828 (Issue1828.idr) 1/1: Building Issue1828 (Issue1828.idr)
LOG totality.requirement:10: Checking totality requirement of Issue1828.idr (main file is Issue1828.idr) LOG totality.requirement:10: Checking totality requirement of Issue1828.idr (main file is Issue1828.idr)
LOG totality.requirement:20: Reading totalReq from build/ttc/Issue1828.ttc LOG totality.requirement:20: Reading totalReq from build/ttc/1/Issue1828.ttc
LOG totality.requirement:20: Got covering and expected total: we should rebuild LOG totality.requirement:20: Got covering and expected total: we should rebuild
1/1: Building Issue1828 (Issue1828.idr) 1/1: Building Issue1828 (Issue1828.idr)
Error: caseTest is not total, possibly not terminating due to call to Main.dummy Error: caseTest is not total, possibly not terminating due to call to Main.dummy
@ -39,12 +39,12 @@ Issue1828:6:3--6:14
1/1: Building Issue1828 (Issue1828.idr) 1/1: Building Issue1828 (Issue1828.idr)
LOG totality.requirement:10: Checking totality requirement of Issue1828.idr (main file is Issue1828.idr) LOG totality.requirement:10: Checking totality requirement of Issue1828.idr (main file is Issue1828.idr)
LOG totality.requirement:20: Reading totalReq from build/ttc/Issue1828.ttc LOG totality.requirement:20: Reading totalReq from build/ttc/1/Issue1828.ttc
LOG totality.requirement:20: Got covering and expected covering: we shouldn't rebuild LOG totality.requirement:20: Got covering and expected covering: we shouldn't rebuild
1/1: Building TotallyTotal (TotallyTotal.idr) 1/1: Building TotallyTotal (TotallyTotal.idr)
LOG totality.requirement:10: Checking totality requirement of TotallyTotal.idr (main file is TotallyTotal.idr) LOG totality.requirement:10: Checking totality requirement of TotallyTotal.idr (main file is TotallyTotal.idr)
LOG totality.requirement:20: Reading totalReq from build/ttc/TotallyTotal.ttc LOG totality.requirement:20: Reading totalReq from build/ttc/1/TotallyTotal.ttc
LOG totality.requirement:20: Got total and expected covering: we shouldn't rebuild LOG totality.requirement:20: Got total and expected covering: we shouldn't rebuild
LOG totality.requirement:10: Checking totality requirement of TotallyTotal.idr (main file is TotallyTotal.idr) LOG totality.requirement:10: Checking totality requirement of TotallyTotal.idr (main file is TotallyTotal.idr)
LOG totality.requirement:20: Reading totalReq from build/ttc/TotallyTotal.ttc LOG totality.requirement:20: Reading totalReq from build/ttc/1/TotallyTotal.ttc
LOG totality.requirement:20: Got total and expected total: we shouldn't rebuild LOG totality.requirement:20: Got total and expected total: we shouldn't rebuild

9
tests/idris2/total/total012/run
View File

@ -1,12 +1,11 @@
. ../../../testutils.sh . ../../../testutils.sh
check Issue1828.idr check Issue1828.idr
check Issue1828.idr --total --log totality.requirement:20 | sed -r "s/.([0-9]){10}//g" check Issue1828.idr --total --log totality.requirement:20 | clean_names
check Issue1828.idr check Issue1828.idr
check Issue1828.idr --log totality.requirement:20 | sed -r "s/.([0-9]){10}//g" check Issue1828.idr --log totality.requirement:20 | clean_names
check TotallyTotal.idr check TotallyTotal.idr
check TotallyTotal.idr --log totality.requirement:20 | sed -r "s/.([0-9]){10}//g" check TotallyTotal.idr --log totality.requirement:20 | clean_names
check TotallyTotal.idr --total --log totality.requirement:20 | sed -r "s/.([0-9]){10}//g" check TotallyTotal.idr --total --log totality.requirement:20 | clean_names

38
tests/testutils.sh
View File

@ -30,6 +30,44 @@ sed_literal() {
printf '%s\n' "$1" | sed -e 's/[]\/$*.^[]/\\&/g' printf '%s\n' "$1" | sed -e 's/[]\/$*.^[]/\\&/g'
} }
# used below to normalise machine names
# shellcheck disable=SC2016
_awk_clean_name='
#!/bin/awk -f
# consistently replace numbers to make golden tests more stable. Currently handles:
# arg:NNN
# conArg:NNN
# $resolvedNNN
# ttc/NNNNNNNNNN
# Foo.Bar:NN:NN--NN:NN
# P:xyz:NNNNN
{
out = ""
# the last one is FC
while (match($0, /(P:[A-z]+:|arg:|conArg:|ttc[\\\/][0-9]+|[$]resolved)[0-9]+|[A-z.]+:[0-9]+:[0-9]+--[0-9]+:[0-9]+|[A-z]+[.][0-9]+:[0-9]+/)) {
rs = RSTART
rl = RLENGTH
m = substr($0, rs, rl - 1)
pfx = "XXX"
if (match(m,/^(\$resolved|arg:|conArg:|ttc[\\\/]|P:[A-z]+:|[A-z.]+:|[A-z]+[.])/)) { pfx = substr(m, RSTART, RLENGTH) }
if (!(m in mapping)) {
# scope the count to the prefix so we can add more without breaking tests
if (!count[pfx]) { count[pfx] = 1}
mapping[m] = count[pfx]
count[pfx]++
}
out = out substr($0, 1, rs - 1) pfx mapping[m]
$0 = substr($0, rs + rl)
}
print out $0
}
'
# normalise machine names
clean_names() {
awk "$_awk_clean_name"
}
# Folder containing the currently running test # Folder containing the currently running test
if [ "$OS" = "windows" ]; then if [ "$OS" = "windows" ]; then
test_dir="$(cygpath -m "$(pwd)")" test_dir="$(cygpath -m "$(pwd)")"