diff --git a/src/Language/Reflection/Compat.idr b/src/Language/Reflection/Compat.idr index e61b339e4..13aec7428 100644 --- a/src/Language/Reflection/Compat.idr +++ b/src/Language/Reflection/Compat.idr @@ -24,6 +24,11 @@ public export argName : Arg -> Name argName = stname . (.name) +cleanupNamedHoles : TTImp -> TTImp +cleanupNamedHoles = mapTTImp $ \case + IHole {} => implicitFalse + e => e + -------------------------------------------------------------------------------- -- General Types -------------------------------------------------------------------------------- @@ -40,7 +45,7 @@ record Con where export getCon : Elaboration m => Name -> m Con getCon n = do (n', tt) <- lookupName n - let (args, tpe) = unPi tt + let (args, tpe) = unPi $ cleanupNamedHoles tt pure $ MkCon n' args tpe ||| Information about a data type @@ -64,7 +69,7 @@ export getInfo' : Elaboration m => Name -> m TypeInfo getInfo' n = do (n',tt) <- lookupName n - let (args,IType _) = unPi tt + let (args,IType _) = unPi $ cleanupNamedHoles tt | (_,_) => fail "Type declaration does not end in IType" conNames <- getCons n' cons <- traverse getCon conNames diff --git a/tests/derivation/least-effort/print/regression/fin-inc/AlternativeCore.idr b/tests/derivation/least-effort/print/regression/fin-inc/AlternativeCore.idr new file mode 120000 index 000000000..6da8d83f9 --- /dev/null +++ b/tests/derivation/least-effort/print/regression/fin-inc/AlternativeCore.idr @@ -0,0 +1 @@ +../_common/AlternativeCore.idr \ No newline at end of file diff --git a/tests/derivation/least-effort/print/regression/fin-inc/DerivedGen.idr b/tests/derivation/least-effort/print/regression/fin-inc/DerivedGen.idr new file mode 100644 index 000000000..a06aa8d8c --- /dev/null +++ b/tests/derivation/least-effort/print/regression/fin-inc/DerivedGen.idr @@ -0,0 +1,15 @@ +module DerivedGen + +import AlternativeCore +import PrintDerivation + +%default total + +record FinInc n where + constructor MkFinInc + val : Nat + prf : LTE val n + +%language ElabReflection + +%runElab printDerived @{MainCoreDerivator @{LeastEffort}} $ Fuel -> Gen MaybeEmpty (n ** FinInc n) diff --git a/tests/derivation/least-effort/print/regression/fin-inc/PrintDerivation.idr b/tests/derivation/least-effort/print/regression/fin-inc/PrintDerivation.idr new file mode 120000 index 000000000..3724a195a --- /dev/null +++ b/tests/derivation/least-effort/print/regression/fin-inc/PrintDerivation.idr @@ -0,0 +1 @@ +../_common/PrintDerivation.idr \ No newline at end of file diff --git a/tests/derivation/least-effort/print/regression/fin-inc/RunDerivedGen.idr b/tests/derivation/least-effort/print/regression/fin-inc/RunDerivedGen.idr new file mode 120000 index 000000000..2b18cc56c --- /dev/null +++ b/tests/derivation/least-effort/print/regression/fin-inc/RunDerivedGen.idr @@ -0,0 +1 @@ +../_common/RunDerivedGen.idr \ No newline at end of file diff --git a/tests/derivation/least-effort/print/regression/fin-inc/derive.ipkg b/tests/derivation/least-effort/print/regression/fin-inc/derive.ipkg new file mode 120000 index 000000000..ff0da46fe --- /dev/null +++ b/tests/derivation/least-effort/print/regression/fin-inc/derive.ipkg @@ -0,0 +1 @@ +../_common/derive.ipkg \ No newline at end of file diff --git a/tests/derivation/least-effort/print/regression/fin-inc/expected b/tests/derivation/least-effort/print/regression/fin-inc/expected new file mode 100644 index 000000000..6704d9098 --- /dev/null +++ b/tests/derivation/least-effort/print/regression/fin-inc/expected @@ -0,0 +1,297 @@ +1/3: Building AlternativeCore (AlternativeCore.idr) +2/3: Building PrintDerivation (PrintDerivation.idr) +3/3: Building DerivedGen (DerivedGen.idr) +LOG gen.auto.derive.infra:0: type: (arg : Fuel) -> Gen MaybeEmpty (n : Nat ** FinInc n) +LOG gen.auto.derive.infra:0: + MkArg MW ExplicitArg (Just "^outmost-fuel^") (var "Data.Fuel.Fuel") +.=> local + { decls = + [ IClaim + emptyFC + MW + Export + [] + (mkTy + { name = "[]" + , type = + MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") + .-> var "Test.DepTyCheck.Gen.Gen" + .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" + .$ ( var "Builtin.DPair.DPair" + .$ implicitFalse + .$ (MkArg MW ExplicitArg (Just "n") implicitFalse .=> var "DerivedGen.FinInc" .$ var "n")) + }) + , IClaim + emptyFC + MW + Export + [] + (mkTy + { name = "[]" + , type = + MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") + .-> var "Test.DepTyCheck.Gen.Gen" + .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" + .$ ( var "Builtin.DPair.DPair" + .$ var "Prelude.Types.Nat" + .$ ( MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .=> var "Builtin.DPair.DPair" + .$ var "Prelude.Types.Nat" + .$ (MkArg MW ExplicitArg (Just "m") (var "Prelude.Types.Nat") .=> var "Data.Nat.LTE" .$ var "n" .$ var "m"))) + }) + , IClaim + emptyFC + MW + Export + [] + (mkTy + { name = "[]" + , type = + MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") + .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Prelude.Types.Nat" + }) + , IDef + emptyFC + "[]" + [ var "[]" .$ bindVar "^fuel_arg^" + .= local + { decls = + [ IClaim + emptyFC + MW + Export + [] + (mkTy + { name = "<>" + , type = + MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") + .-> var "Test.DepTyCheck.Gen.Gen" + .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" + .$ ( var "Builtin.DPair.DPair" + .$ implicitFalse + .$ (MkArg MW ExplicitArg (Just "n") implicitFalse .=> var "DerivedGen.FinInc" .$ var "n")) + }) + , IDef + emptyFC + "<>" + [ var "<>" .$ bindVar "^cons_fuel^" + .= var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "DerivedGen.MkFinInc (orders)")) + .$ ( var ">>=" + .$ (var "[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse + .=> iCase + { sc = var "{lamc:0}" + , ty = implicitFalse + , clauses = + [ var "Builtin.DPair.MkDPair" + .$ bindVar "val" + .$ (var "Builtin.DPair.MkDPair" .$ bindVar "n" .$ bindVar "prf") + .= var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ (var "DerivedGen.MkFinInc" .! ("n", var "n") .$ var "val" .$ var "prf")) + ] + })) + ] + ] + , scope = + var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "DerivedGen.FinInc[] (non-recursive)")) + .$ (var "<>" .$ var "^fuel_arg^") + } + ] + , IDef + emptyFC + "[]" + [ var "[]" .$ bindVar "^fuel_arg^" + .= local + { decls = + [ IClaim + emptyFC + MW + Export + [] + (mkTy + { name = "<>" + , type = + MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") + .-> var "Test.DepTyCheck.Gen.Gen" + .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" + .$ ( var "Builtin.DPair.DPair" + .$ var "Prelude.Types.Nat" + .$ ( MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .=> var "Builtin.DPair.DPair" + .$ var "Prelude.Types.Nat" + .$ ( MkArg MW ExplicitArg (Just "m") (var "Prelude.Types.Nat") + .=> var "Data.Nat.LTE" .$ var "n" .$ var "m"))) + }) + , IClaim + emptyFC + MW + Export + [] + (mkTy + { name = "<>" + , type = + MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") + .-> var "Test.DepTyCheck.Gen.Gen" + .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" + .$ ( var "Builtin.DPair.DPair" + .$ var "Prelude.Types.Nat" + .$ ( MkArg MW ExplicitArg (Just "n") (var "Prelude.Types.Nat") + .=> var "Builtin.DPair.DPair" + .$ var "Prelude.Types.Nat" + .$ ( MkArg MW ExplicitArg (Just "m") (var "Prelude.Types.Nat") + .=> var "Data.Nat.LTE" .$ var "n" .$ var "m"))) + }) + , IDef + emptyFC + "<>" + [ var "<>" .$ bindVar "^cons_fuel^" + .= var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "Data.Nat.LTEZero (orders)")) + .$ ( var ">>=" + .$ (var "[]" .$ var "^outmost-fuel^") + .$ ( MkArg MW ExplicitArg (Just "right") implicitFalse + .=> var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ (var "Data.Nat.LTEZero" .! ("right", var "right")))))) + ] + , IDef + emptyFC + "<>" + [ var "<>" .$ bindVar "^cons_fuel^" + .= var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "Data.Nat.LTESucc (orders)")) + .$ ( var ">>=" + .$ (var "[]" .$ var "^cons_fuel^") + .$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse + .=> iCase + { sc = var "{lamc:0}" + , ty = implicitFalse + , clauses = + [ var "Builtin.DPair.MkDPair" + .$ bindVar "left" + .$ (var "Builtin.DPair.MkDPair" .$ bindVar "right" .$ bindVar "^bnd^{arg:1}") + .= var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ ( var "Builtin.DPair.MkDPair" + .$ implicitTrue + .$ ( var "Data.Nat.LTESucc" + .! ("right", var "right") + .! ("left", var "left") + .$ var "^bnd^{arg:1}"))) + ] + })) + ] + ] + , scope = + iCase + { sc = var "^fuel_arg^" + , ty = var "Data.Fuel.Fuel" + , clauses = + [ var "Data.Fuel.Dry" + .= var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "Data.Nat.LTE[] (dry fuel)")) + .$ (var "<>" .$ var "Data.Fuel.Dry") + , var "Data.Fuel.More" .$ bindVar "^sub^fuel_arg^" + .= var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "Data.Nat.LTE[] (spend fuel)")) + .$ ( var "Test.DepTyCheck.Gen.frequency" + .$ ( var "::" + .$ (var "Builtin.MkPair" .$ var "Data.Nat1.one" .$ (var "<>" .$ var "^fuel_arg^")) + .$ ( var "::" + .$ ( var "Builtin.MkPair" + .$ (var "Deriving.DepTyCheck.Util.Reflection.leftDepth" .$ var "^sub^fuel_arg^") + .$ (var "<>" .$ var "^sub^fuel_arg^")) + .$ var "Nil"))) + ] + } + } + ] + , IDef + emptyFC + "[]" + [ var "[]" .$ bindVar "^fuel_arg^" + .= local + { decls = + [ IClaim + emptyFC + MW + Export + [] + (mkTy + { name = "<>" + , type = + MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") + .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Prelude.Types.Nat" + }) + , IClaim + emptyFC + MW + Export + [] + (mkTy + { name = "<>" + , type = + MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel") + .-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Prelude.Types.Nat" + }) + , IDef + emptyFC + "<>" + [ var "<>" .$ bindVar "^cons_fuel^" + .= var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "Prelude.Types.Z (orders)")) + .$ (var "Prelude.pure" .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) .$ var "Prelude.Types.Z") + ] + , IDef + emptyFC + "<>" + [ var "<>" .$ bindVar "^cons_fuel^" + .= var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "Prelude.Types.S (orders)")) + .$ ( var ">>=" + .$ (var "[]" .$ var "^cons_fuel^") + .$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:2}") implicitFalse + .=> var "Prelude.pure" + .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue) + .$ (var "Prelude.Types.S" .$ var "^bnd^{arg:2}"))) + ] + ] + , scope = + iCase + { sc = var "^fuel_arg^" + , ty = var "Data.Fuel.Fuel" + , clauses = + [ var "Data.Fuel.Dry" + .= var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "Prelude.Types.Nat[] (dry fuel)")) + .$ (var "<>" .$ var "Data.Fuel.Dry") + , var "Data.Fuel.More" .$ bindVar "^sub^fuel_arg^" + .= var "Test.DepTyCheck.Gen.label" + .$ (var "fromString" .$ primVal (Str "Prelude.Types.Nat[] (spend fuel)")) + .$ ( var "Test.DepTyCheck.Gen.frequency" + .$ ( var "::" + .$ (var "Builtin.MkPair" .$ var "Data.Nat1.one" .$ (var "<>" .$ var "^fuel_arg^")) + .$ ( var "::" + .$ ( var "Builtin.MkPair" + .$ (var "Deriving.DepTyCheck.Util.Reflection.leftDepth" .$ var "^sub^fuel_arg^") + .$ (var "<>" .$ var "^sub^fuel_arg^")) + .$ var "Nil"))) + ] + } + } + ] + ] + , scope = var "[]" .$ var "^outmost-fuel^" + } + diff --git a/tests/derivation/least-effort/print/regression/fin-inc/run b/tests/derivation/least-effort/print/regression/fin-inc/run new file mode 120000 index 000000000..805165988 --- /dev/null +++ b/tests/derivation/least-effort/print/regression/fin-inc/run @@ -0,0 +1 @@ +../_common/run \ No newline at end of file diff --git a/tests/derivation/least-effort/run/regression/fin-inc/DerivedGen.idr b/tests/derivation/least-effort/run/regression/fin-inc/DerivedGen.idr new file mode 100644 index 000000000..4d656ea01 --- /dev/null +++ b/tests/derivation/least-effort/run/regression/fin-inc/DerivedGen.idr @@ -0,0 +1,21 @@ +module DerivedGen + +import RunDerivedGen + +%default total + +record FinInc n where + constructor MkFinInc + val : Nat + prf : LTE val n + +Show (FinInc n) where + show (MkFinInc v p) = "MkFinInc \{show v} prf" + +checkedGen : Fuel -> Gen MaybeEmpty (n ** FinInc n) +checkedGen = deriveGen @{MainCoreDerivator @{LeastEffort}} + +main : IO () +main = runGs + [ G $ \fl => checkedGen fl + ] diff --git a/tests/derivation/least-effort/run/regression/fin-inc/RunDerivedGen.idr b/tests/derivation/least-effort/run/regression/fin-inc/RunDerivedGen.idr new file mode 120000 index 000000000..2b18cc56c --- /dev/null +++ b/tests/derivation/least-effort/run/regression/fin-inc/RunDerivedGen.idr @@ -0,0 +1 @@ +../_common/RunDerivedGen.idr \ No newline at end of file diff --git a/tests/derivation/least-effort/run/regression/fin-inc/derive.ipkg b/tests/derivation/least-effort/run/regression/fin-inc/derive.ipkg new file mode 120000 index 000000000..ff0da46fe --- /dev/null +++ b/tests/derivation/least-effort/run/regression/fin-inc/derive.ipkg @@ -0,0 +1 @@ +../_common/derive.ipkg \ No newline at end of file diff --git a/tests/derivation/least-effort/run/regression/fin-inc/expected b/tests/derivation/least-effort/run/regression/fin-inc/expected new file mode 100644 index 000000000..f7ab5c74a --- /dev/null +++ b/tests/derivation/least-effort/run/regression/fin-inc/expected @@ -0,0 +1,24 @@ +1/2: Building RunDerivedGen (RunDerivedGen.idr) +2/2: Building DerivedGen (DerivedGen.idr) +Generated values: +----- +----- +(20 ** MkFinInc 16 prf) +----- +(27 ** MkFinInc 17 prf) +----- +(27 ** MkFinInc 10 prf) +----- +(9 ** MkFinInc 5 prf) +----- +(23 ** MkFinInc 12 prf) +----- +(23 ** MkFinInc 8 prf) +----- +(18 ** MkFinInc 4 prf) +----- +(11 ** MkFinInc 7 prf) +----- +(11 ** MkFinInc 10 prf) +----- +(35 ** MkFinInc 15 prf) diff --git a/tests/derivation/least-effort/run/regression/fin-inc/run b/tests/derivation/least-effort/run/regression/fin-inc/run new file mode 120000 index 000000000..805165988 --- /dev/null +++ b/tests/derivation/least-effort/run/regression/fin-inc/run @@ -0,0 +1 @@ +../_common/run \ No newline at end of file