Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[ test ] Fix spec001 test #3156

Merged
merged 4 commits into from
Dec 8, 2023
Merged

[ test ] Fix spec001 test #3156

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
e6612b6
[ test ] make spec001 test less fragile
dunhamsteve Dec 2, 2023
f0b8437
[ text ] Replace arg/conArg/$resolved with consistent numbers in spec001
dunhamsteve Dec 3, 2023
f66ee2c
[ test ] Move clean_names into testutils.sh
dunhamsteve Dec 5, 2023
9b71197
[ tests ] Use clean_names where possible
dunhamsteve Dec 7, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -314,6 +314,7 @@
* Updates the docs for `envvars` to categorise when environment variables are
used (runtime, build-time, or both).
* Fixed build failure occuring when `make -j` is in effect.
* Add `clean_names` function to `testutils.sh` to normalise machine names

## v0.6.0

Expand Down
2 changes: 1 addition & 1 deletion src/TTImp/ProcessDef.idr
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1145,7 +1145,7 @@ processDef opts nest env fc n_in cs_in
getPMDef fc (CompileTime mult) (Resolved n) ty covcs
logC "declare.def" 3 $ do pure $ "Working from " ++ show !(toFullNames ctree)
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 []
else getMissing fc (Resolved n) ctree
logC "declare.def" 3 $
Expand Down
4 changes: 2 additions & 2 deletions tests/codegen/builtin001/expected
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
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.main = [{ext:N}]: (Main.plus [1, 2])
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:0}]: (Main.plus [1, 2])
2 changes: 1 addition & 1 deletion tests/codegen/builtin001/run
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,4 @@ rm Main.cases

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 changes: 1 addition & 1 deletion tests/codegen/con001/run
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,4 @@ rm Main.cases

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 changes: 68 additions & 68 deletions tests/idris2/basic/basic044/expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,52 +21,52 @@ 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:vars: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:1}, (Term:2, Rig0))
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:vars: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: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 declare.data:1: Processing Term.Chk
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:vars: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: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.meta:5: Adding new meta ({P:cut:N}, (Term:L:C--L:C, 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:n: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:4}, (Term:8, 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 declare.data:1: Processing Term.Syn
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:cut: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: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.meta:5: Adding new meta ({P:cut:N}, (Term:L:C--L:C, 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:cut:6}, (Term:12, 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.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 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:2: Case tree for Term.Typ: [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.type:1: Processing Term.Term
Expand All @@ -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: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: 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.type:1: Processing Term.NF
Expand All @@ -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: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: Catch all case in N
LOG declare.def:3: Catch all case in Term.NF
LOG declare.def:3: Initially missing in Term.NF:

Term> Bye for now!
1/1: Building Vec (Vec.idr)
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.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.def:2: Case tree for Vec.(::): case {arg:N}[4] : (Data.Fin.Fin (Prelude.Types.S {arg:N}[0])) of
{ Data.Fin.FZ {e:N} => [0] {arg:N}[3]
| Data.Fin.FS {e:N} {e:N} => [1] ({arg:N}[5] {e:N}[1])
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:0} => [0] {arg:2}[3]
| Data.Fin.FS {e:1} {e:2} => [1] ({arg:2}[5] {e:2}[1])
}
LOG declare.type:1: Processing Vec.test
LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C:
($resolvedN 2)
($resolvedN 2)
LOG elab.ambiguous:5: Ambiguous elaboration at Vec:1:
($resolved1 2)
($resolved2 2)
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:
(($resolvedN Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil))
(($resolvedN Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil))
(($resolvedN 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)
LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:L:C--L:C:
$resolvedN
$resolvedN
Target type : ?Vec.{a:N}_[]
LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:L:C--L:C:
(($resolvedN ((:: (fromInteger 0)) Nil)) Nil)
(($resolvedN ((:: (fromInteger 0)) Nil)) Nil)
(($resolvedN ((:: (fromInteger 0)) Nil)) Nil)
Target type : (Vec.Vec ?Vec.{a:N}_[] ?Vec.{n:N}_[])
LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:L:C--L:C:
(($resolvedN (fromInteger 0)) Nil)
(($resolvedN (fromInteger 0)) Nil)
(($resolvedN (fromInteger 0)) Nil)
Target type : ?Vec.{a:N}_[]
LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C:
($resolvedN 0)
($resolvedN 0)
With default. Target type : ?Vec.{a:N}_[]
LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:L:C--L:C:
$resolvedN
$resolvedN
Target type : (Vec.Vec ?Vec.{a:N}_[] ?Vec.{n:N}_[])
LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C:
($resolvedN 0)
($resolvedN 0)
With default. Target type : ?Vec.{a:N}_[]
LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:L:C--L:C:
$resolvedN
$resolvedN
Target type : (Vec.Vec ?Vec.{a:N}_[] ?Vec.{n:N}_[])
LOG elab.ambiguous:5: Ambiguous elaboration (kept 1 out of 3 candidates) (delayed) at Vec:L:C--L:C:
(($resolvedN (fromInteger 0)) Nil)
LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:2:
(($resolved3 Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil))
(($resolved4 Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil))
(($resolved5 Nil) ((:: ((:: (fromInteger 0)) Nil)) Nil))
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:3:
$resolved6
$resolved7
Target type : ?Vec.{a:4574}_[]
LOG elab.ambiguous:5: Ambiguous elaboration (kept 3 out of 3 candidates) (not delayed) at Vec:4:
(($resolved3 ((:: (fromInteger 0)) Nil)) Nil)
(($resolved4 ((:: (fromInteger 0)) Nil)) Nil)
(($resolved5 ((:: (fromInteger 0)) Nil)) Nil)
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:5:
(($resolved3 (fromInteger 0)) Nil)
(($resolved4 (fromInteger 0)) Nil)
(($resolved5 (fromInteger 0)) Nil)
Target type : ?Vec.{a:4577}_[]
LOG elab.ambiguous:5: Ambiguous elaboration at Vec:6:
($resolved1 0)
($resolved2 0)
With default. Target type : ?Vec.{a:4579}_[]
LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:7:
$resolved6
$resolved7
Target type : (Vec.Vec ?Vec.{a:4579}_[] ?Vec.{n:4578}_[])
LOG elab.ambiguous:5: Ambiguous elaboration at Vec:6:
($resolved1 0)
($resolved2 0)
With default. Target type : ?Vec.{a:4578}_[]
LOG elab.ambiguous:5: Ambiguous elaboration (kept 2 out of 2 candidates) (not delayed) at Vec:8:
$resolved6
$resolved7
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:5:
(($resolved4 (fromInteger 0)) Nil)
Target type : (Prelude.Basics.List Prelude.Types.Nat)
LOG elab.ambiguous:5: Ambiguous elaboration at Vec:L:C--L:C:
($resolvedN 0)
($resolvedN 0)
LOG elab.ambiguous:5: Ambiguous elaboration at Vec:6:
($resolved1 0)
($resolved2 0)
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:
$resolvedN
LOG elab.ambiguous:5: Ambiguous elaboration (kept 1 out of 2 candidates) (delayed) at Vec:3:
$resolved7
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))))
Vec> Bye for now!
8 changes: 2 additions & 6 deletions tests/idris2/basic/basic044/run
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,8 +1,4 @@
. ../../../testutils.sh

echo ":q" | idris2 --log unify.equal:10 --log unify:5 Term.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"
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"
echo ":q" | idris2 --log unify.equal:10 --log unify:5 Term.idr | clean_names
echo ":q" | idris2 --log unify:3 --log elab.ambiguous:5 Vec.idr | clean_names
Loading
Loading