[ upstream ] Work around IHoles in type signatures

buzden · Aug 29, 2024 · 6e26d52 · 6e26d52
1 parent efce20f
commit 6e26d52
Show file tree

Hide file tree

Showing 13 changed files with 372 additions and 2 deletions.
diff --git 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
@@ -0,0 +1 @@
+../_common/AlternativeCore.idr
diff --git a/tests/derivation/least-effort/print/regression/fin-inc/DerivedGen.idr 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
@@ -0,0 +1 @@
+../_common/PrintDerivation.idr
diff --git a/tests/derivation/least-effort/print/regression/fin-inc/RunDerivedGen.idr b/tests/derivation/least-effort/print/regression/fin-inc/RunDerivedGen.idr
@@ -0,0 +1 @@
+../_common/RunDerivedGen.idr
diff --git a/tests/derivation/least-effort/print/regression/fin-inc/derive.ipkg b/tests/derivation/least-effort/print/regression/fin-inc/derive.ipkg
@@ -0,0 +1 @@
+../_common/derive.ipkg
diff --git a/tests/derivation/least-effort/print/regression/fin-inc/expected b/tests/derivation/least-effort/print/regression/fin-inc/expected
diff --git a/tests/derivation/least-effort/print/regression/fin-inc/run b/tests/derivation/least-effort/print/regression/fin-inc/run
@@ -0,0 +1 @@
+../_common/run
diff --git a/tests/derivation/least-effort/run/regression/fin-inc/DerivedGen.idr 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
@@ -0,0 +1 @@
+../_common/RunDerivedGen.idr
diff --git a/tests/derivation/least-effort/run/regression/fin-inc/derive.ipkg b/tests/derivation/least-effort/run/regression/fin-inc/derive.ipkg
@@ -0,0 +1 @@
+../_common/derive.ipkg
diff --git a/tests/derivation/least-effort/run/regression/fin-inc/expected 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
@@ -0,0 +1 @@
+../_common/run