diff --git a/CHANGELOG.md b/CHANGELOG.md index 520781854a..2a4ea0157d 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr index 514fe2428f..b10a44b68f 100644 --- a/src/TTImp/ProcessDef.idr +++ b/src/TTImp/ProcessDef.idr @@ -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 $ diff --git a/tests/codegen/builtin001/expected b/tests/codegen/builtin001/expected index ed23a3ec55..5b15df7976 100644 --- a/tests/codegen/builtin001/expected +++ b/tests/codegen/builtin001/expected @@ -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]) diff --git a/tests/codegen/builtin001/run b/tests/codegen/builtin001/run index a971e6b98e..cd6dd35d9d 100755 --- a/tests/codegen/builtin001/run +++ b/tests/codegen/builtin001/run @@ -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' diff --git a/tests/codegen/con001/run b/tests/codegen/con001/run index 49ed047288..f1866a326c 100755 --- a/tests/codegen/con001/run +++ b/tests/codegen/con001/run @@ -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' diff --git a/tests/idris2/basic/basic044/expected b/tests/idris2/basic/basic044/expected index 2819e90571..d64b133646 100644 --- a/tests/idris2/basic/basic044/expected +++ b/tests/idris2/basic/basic044/expected @@ -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.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 @@ -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.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 @@ -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.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 @@ -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 @@ -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! diff --git a/tests/idris2/basic/basic044/run b/tests/idris2/basic/basic044/run index 0d793db537..5be403c02d 100644 --- a/tests/idris2/basic/basic044/run +++ b/tests/idris2/basic/basic044/run @@ -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 diff --git a/tests/idris2/evaluator/spec001/expected b/tests/idris2/evaluator/spec001/expected index 2caaca59cd..446d65ddae 100644 --- a/tests/idris2/evaluator/spec001/expected +++ b/tests/idris2/evaluator/spec001/expected @@ -1,12 +1,12 @@ 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:5: Attempting to specialise: ((Main.smult Prelude.Types.Z) n) = Prelude.Types.Z ((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: -(_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: Already specialised _PE.PE_smult_4e8901402355876e /* 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); } 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: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.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: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: ((((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: (((_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: 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 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: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.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: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: -(((((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: -((_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)) -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: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 +((_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 ($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: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: -(((((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: -((_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: 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 @@ -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: Already specialised _PE.PE_fold_8abb50b713fe8e5e 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:3: Specialised type _PE.PE_identity_3c7f5598e5c9b732: ({arg:813} : (Prelude.Basics.List Prelude.Types.Nat)) -> (Prelude.Basics.List Prelude.Types.Nat) +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:6} : (Prelude.Basics.List Prelude.Types.Nat)) -> (Prelude.Basics.List Prelude.Types.Nat) 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.(::) [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: Already specialised _PE.PE_identity_3c7f5598e5c9b732 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) -LOG compiler.identity:5: new def: [{arg:0}]: !{arg:0} + 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:3}]: !{arg:3} 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) -LOG compiler.identity:5: new def: [{arg:1}]: !{arg:1} + 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:3}]: !{arg:3} LOG compiler.identity:5: found identity flag for: _PE.PE_identity_3c7f5598e5c9b732, 0 - old def: Just [{arg:0}]: !{arg:0} -LOG compiler.identity:5: new def: [{arg:0}]: !{arg:0} + old def: Just [{arg:3}]: !{arg:3} +LOG compiler.identity:5: new def: [{arg:3}]: !{arg:3} LOG compiler.identity:5: found identity flag for: Main.identity, 0 - old def: Just [{arg:1}]: !{arg:1} -LOG compiler.identity:5: new def: [{arg:1}]: !{arg:1} + old def: Just [{arg:3}]: !{arg:3} +LOG compiler.identity:5: new def: [{arg:3}]: !{arg:3} LOG compiler.identity:5: found identity flag for: Main.test, 0 - old def: Just [{arg:0}]: !{arg:0} -LOG compiler.identity:5: new def: [{arg:0}]: !{arg:0} + old def: Just [{arg:3}]: !{arg:3} +LOG compiler.identity:5: new def: [{arg:3}]: !{arg:3} LOG compiler.identity:5: found identity flag for: _PE.PE_identity_3c7f5598e5c9b732, 0 - old def: Just [{arg:0}]: !{arg:0} -LOG compiler.identity:5: new def: [{arg:0}]: !{arg:0} + old def: Just [{arg:3}]: !{arg:3} +LOG compiler.identity:5: new def: [{arg:3}]: !{arg:3} LOG compiler.identity:5: found identity flag for: Main.identity, 0 - old def: Just [{arg:1}]: !{arg:1} -LOG compiler.identity:5: new def: [{arg:1}]: !{arg:1} + old def: Just [{arg:3}]: !{arg:3} +LOG compiler.identity:5: new def: [{arg:3}]: !{arg:3} LOG compiler.identity:5: found identity flag for: Main.test, 0 - old def: Just [{arg:0}]: !{arg:0} -LOG compiler.identity:5: new def: [{arg:0}]: !{arg:0} + old def: Just [{arg:3}]: !{arg:3} +LOG compiler.identity:5: new def: [{arg:3}]: !{arg:3} diff --git a/tests/idris2/evaluator/spec001/run b/tests/idris2/evaluator/spec001/run index 11aaa6a137..d49e5f3026 100644 --- a/tests/idris2/evaluator/spec001/run +++ b/tests/idris2/evaluator/spec001/run @@ -1,8 +1,10 @@ . ../../../testutils.sh +{ idris2 --log specialise:5 -c Mult3.idr idris2 --cg node -o mult3.js -c Mult3.idr awk -v RS= '/\/\* Main.main/' build/exec/mult3.js idris2 --log specialise:5 -c Desc.idr idris2 --log specialise:5 -c Desc2.idr idris2 --log specialise:5 -c Identity.idr +} | clean_names diff --git a/tests/idris2/reflection/reflection010/expected b/tests/idris2/reflection/reflection010/expected index e982beff47..baf441b0e2 100644 --- a/tests/idris2/reflection/reflection010/expected +++ b/tests/idris2/reflection/reflection010/expected @@ -1,10 +1,10 @@ 1/1: Building Name (Name.idr) LOG declare.data:1: Processing Main.Identity 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.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: cased: (%lam RigW Explicit (Just {lamc:0}) (Main.Identity Int) (Main.case block in cased {lamc:0})) LOG 1: 10 diff --git a/tests/idris2/reflection/reflection010/run b/tests/idris2/reflection/reflection010/run index bf1c8e5f8c..f3b0bc542a 100755 --- a/tests/idris2/reflection/reflection010/run +++ b/tests/idris2/reflection/reflection010/run @@ -1,3 +1,3 @@ . ../../../testutils.sh -check Name.idr | sed -E "s/\.[0-9]+:[0-9]+/\.N:N/" +check Name.idr | clean_names diff --git a/tests/idris2/reflection/reflection025/expected b/tests/idris2/reflection/reflection025/expected index d9a749ac36..f35d864a3d 100644 --- a/tests/idris2/reflection/reflection025/expected +++ b/tests/idris2/reflection/reflection025/expected @@ -4,7 +4,7 @@ LOG elab:0: - prim__sub_Integer LOG elab:0: - prim__lte_Integer LOG elab:0: - Prelude.Types.case block in "integerToNat" 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.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''', CurrFn.case block in "f'''"] -LOG elab:0: current fn: [< CurrFn.n, CurrFn.::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"] ------------ @@ -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''', RefDefsDeep.case block in "f'''"] === -LOG elab:0: === current fn: [< RefDefsDeep.n, RefDefsDeep.::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: Names `RefDefsDeep.f` refers to: @@ -61,7 +61,7 @@ LOG elab:0: - prim__sub_Integer LOG elab:0: - prim__lte_Integer LOG elab:0: - Prelude.Types.case block in "integerToNat" 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.plus @@ -84,7 +84,7 @@ LOG elab:0: - prim__sub_Integer LOG elab:0: - prim__lte_Integer LOG elab:0: - Prelude.Types.case block in "integerToNat" 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.plus @@ -107,7 +107,7 @@ LOG elab:0: - prim__sub_Integer LOG elab:0: - prim__lte_Integer LOG elab:0: - Prelude.Types.case block in "integerToNat" 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.plus @@ -132,7 +132,7 @@ LOG elab:0: - prim__sub_Integer LOG elab:0: - prim__lte_Integer LOG elab:0: - Prelude.Types.case block in "integerToNat" 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.plus @@ -158,7 +158,7 @@ LOG elab:0: - prim__sub_Integer LOG elab:0: - prim__lte_Integer LOG elab:0: - Prelude.Types.case block in "integerToNat" 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.plus @@ -174,7 +174,7 @@ LOG elab:0: - Prelude.Basics.True LOG elab:0: - Prelude.Basics.False LOG elab:0: - Builtin.assert_total LOG elab:0: - Builtin.MkUnit -LOG elab:0: - RefDefsDeep.::f +LOG elab:0: - RefDefsDeep.1:f LOG elab:0: - RefDefsDeep.case block in "n,f" LOG elab:0: 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: - Prelude.Types.case block in "integerToNat" 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.plus diff --git a/tests/idris2/reflection/reflection025/run b/tests/idris2/reflection/reflection025/run index 7bb7da8527..1c390d4cc1 100755 --- a/tests/idris2/reflection/reflection025/run +++ b/tests/idris2/reflection/reflection025/run @@ -8,4 +8,4 @@ echo ------------ check RefDefsDeep.idr echo ------------ check InspectRec.idr -} | sed -e 's/\.[0-9]*:[0-9]*:/.::/' +} | clean_names diff --git a/tests/idris2/total/total012/expected b/tests/idris2/total/total012/expected index c9459bd2c8..188710db15 100644 --- a/tests/idris2/total/total012/expected +++ b/tests/idris2/total/total012/expected @@ -1,6 +1,6 @@ 1/1: Building Issue1828 (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 1/1: Building Issue1828 (Issue1828.idr) 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) 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 1/1: Building TotallyTotal (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: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 diff --git a/tests/idris2/total/total012/run b/tests/idris2/total/total012/run index 5bb43bced0..67eb15849e 100755 --- a/tests/idris2/total/total012/run +++ b/tests/idris2/total/total012/run @@ -1,12 +1,11 @@ . ../../../testutils.sh 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 --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 --log totality.requirement:20 | sed -r "s/.([0-9]){10}//g" -check TotallyTotal.idr --total --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 | clean_names diff --git a/tests/testutils.sh b/tests/testutils.sh index 7f64eb64fc..397bca45a3 100755 --- a/tests/testutils.sh +++ b/tests/testutils.sh @@ -30,6 +30,44 @@ sed_literal() { 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 if [ "$OS" = "windows" ]; then test_dir="$(cygpath -m "$(pwd)")"