Skip to content

Commit

Permalink
[ derive, fix ] Support lets in types of constructors
Browse files Browse the repository at this point in the history
  • Loading branch information
@buzden
buzden authored Jan 21, 2025
2 parents 9052795 + f4bb0af commit 67f4a7c
Show file tree
Hide file tree
Showing 56 changed files with 1,795 additions and 1 deletion.
1 change: 1 addition & 0 deletions deptycheck.ipkg
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,7 @@ modules = Deriving.DepTyCheck
depends = ansi
, best-alternative
, collection-utils
, cozippable
, dependent-vect
, elab-pretty
, elab-util
Expand Down
3 changes: 2 additions & 1 deletion src/Deriving/DepTyCheck/Util/Reflection.idr
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ module Deriving.DepTyCheck.Util.Reflection
import public Control.Applicative.Const

import public Data.Alternative
import public Data.Cozippable

import public Data.Fin.Lists
import public Data.Fin.ToFin
Expand Down Expand Up @@ -74,7 +75,7 @@ normaliseCon orig@(MkCon n args ty) = do
| Nothing => pure orig -- didn't manage to normalise, e.g. due to private stuff
let (args', ty) = unPi whole
-- `quote` may corrupt names, workaround it:
let args = args `zip` args' <&> \(pre, normd) => {name := pre.name} normd
let args = cozipWith (these id id $ \pre => {name := pre.name}) args args'
pure $ MkCon n args ty

normaliseCons : Elaboration m => TypeInfo -> m TypeInfo
Expand Down
17 changes: 17 additions & 0 deletions tests/derivation/least-effort/print/adt/015 let function/DerivedGen.idr
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
module DerivedGen

import Deriving.DepTyCheck.Gen

%default total

%language ElabReflection

data X : String -> Nat -> Type where
MkX : (n : _) -> (m : _) -> X n m

data Y : Nat -> Type where
MkY : (u : Nat) -> forall n, m, k. let xx : Nat -> Nat; xx = S in X n (xx m) -> X n (xx k) -> Y (xx u)

%logging "deptycheck.derive.print" 5
%runElab deriveGenPrinter @{MainCoreDerivator @{LeastEffort}} $
Fuel -> (Fuel -> Gen MaybeEmpty String) => (Fuel -> Gen MaybeEmpty Nat) => (n : Nat) -> Gen MaybeEmpty $ Y n
1 change: 1 addition & 0 deletions tests/derivation/least-effort/print/adt/015 let function/derive.ipkg
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
../_common/derive.ipkg
227 changes: 227 additions & 0 deletions tests/derivation/least-effort/print/adt/015 let function/expected
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,227 @@
1/1: Building DerivedGen (DerivedGen.idr)
LOG deptycheck.derive.print:5: type: (arg : Fuel) -> {auto conArg : ((arg : Fuel) -> Gen MaybeEmpty String)} -> {auto conArg : ((arg : Fuel) -> Gen MaybeEmpty Nat)} -> (n : Nat) -> Gen MaybeEmpty (Y n)
MkArg MW ExplicitArg (Just "^outmost-fuel^") (var "Data.Fuel.Fuel")
.=> MkArg
MW
AutoImplicit
(Just "external^<^prim^.String>[]")
( MkArg MW ExplicitArg (Just "{arg:1}") (var "Data.Fuel.Fuel")
.-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ primVal (PrT StringType))
.=> MkArg
MW
AutoImplicit
(Just "external^<Prelude.Types.Nat>[]")
( MkArg MW ExplicitArg (Just "{arg:2}") (var "Data.Fuel.Fuel")
.-> var "Test.DepTyCheck.Gen.Gen" .$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty" .$ var "Prelude.Types.Nat")
.=> MkArg MW ExplicitArg (Just "outer^<n>") implicitTrue
.=> local
{ decls =
[ IClaim
(MkIClaimData
{ rig = MW
, vis = Export
, opts = []
, type =
mkTy
{ name = "<DerivedGen.Y>[0]"
, type =
MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel")
.-> MkArg MW ExplicitArg (Just "{arg:3}") (var "Prelude.Types.Nat")
.-> var "Test.DepTyCheck.Gen.Gen"
.$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty"
.$ (var "DerivedGen.Y" .$ var "{arg:3}")
}
})
, IClaim
(MkIClaimData
{ rig = MW
, vis = Export
, opts = []
, type =
mkTy
{ name = "<DerivedGen.X>[0, 1]"
, type =
MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel")
.-> MkArg MW ExplicitArg (Just "{arg:4}") (primVal (PrT StringType))
.-> MkArg MW ExplicitArg (Just "{arg:5}") (var "Prelude.Types.Nat")
.-> var "Test.DepTyCheck.Gen.Gen"
.$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty"
.$ (var "DerivedGen.X" .$ var "{arg:4}" .$ var "{arg:5}")
}
})
, IClaim
(MkIClaimData
{ rig = MW
, vis = Export
, opts = []
, type =
mkTy
{ name = "<DerivedGen.X>[1]"
, type =
MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel")
.-> MkArg MW ExplicitArg (Just "{arg:5}") (var "Prelude.Types.Nat")
.-> var "Test.DepTyCheck.Gen.Gen"
.$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty"
.$ ( var "Builtin.DPair.DPair"
.$ primVal (PrT StringType)
.$ ( MkArg MW ExplicitArg (Just "{arg:4}") (primVal (PrT StringType))
.=> var "DerivedGen.X" .$ var "{arg:4}" .$ var "{arg:5}"))
}
})
, IDef
emptyFC
"<DerivedGen.Y>[0]"
[ var "<DerivedGen.Y>[0]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^<{arg:3}>"
.= local
{ decls =
[ IClaim
(MkIClaimData
{ rig = MW
, vis = Export
, opts = []
, type =
mkTy
{ name = "<<DerivedGen.MkY>>"
, type =
MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel")
.-> MkArg MW ExplicitArg (Just "{arg:3}") (var "Prelude.Types.Nat")
.-> var "Test.DepTyCheck.Gen.Gen"
.$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty"
.$ (var "DerivedGen.Y" .$ var "{arg:3}")
}
})
, IDef
emptyFC
"<<DerivedGen.MkY>>"
[ var "<<DerivedGen.MkY>>" .$ bindVar "^cons_fuel^" .$ (var "Prelude.Types.S" .$ bindVar "u")
.= var "Test.DepTyCheck.Gen.label"
.$ (var "fromString" .$ primVal (Str "DerivedGen.MkY (orders)"))
.$ ( var ">>="
.$ (var "external^<Prelude.Types.Nat>[]" .$ var "^outmost-fuel^")
.$ ( MkArg MW ExplicitArg (Just "m") implicitFalse
.=> var ">>="
.$ (var "<DerivedGen.X>[1]" .$ var "^outmost-fuel^" .$ (var "Prelude.Types.S" .$ var "m"))
.$ ( MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse
.=> iCase
{ sc = var "{lamc:0}"
, ty = implicitFalse
, clauses =
[ var "Builtin.DPair.MkDPair" .$ bindVar "n" .$ bindVar "^bnd^{arg:6}"
.= var ">>="
.$ (var "external^<Prelude.Types.Nat>[]" .$ var "^outmost-fuel^")
.$ ( MkArg MW ExplicitArg (Just "k") implicitFalse
.=> var ">>="
.$ ( var "<DerivedGen.X>[0, 1]"
.$ var "^outmost-fuel^"
.$ var "n"
.$ (var "Prelude.Types.S" .$ var "k"))
.$ ( MkArg MW ExplicitArg (Just "^bnd^{arg:7}") implicitFalse
.=> var "Prelude.pure"
.! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue)
.$ ( var "DerivedGen.MkY"
.$ var "u"
.! ("n", implicitTrue)
.! ("m", implicitTrue)
.! ("k", implicitTrue)
.$ var "^bnd^{arg:6}"
.$ var "^bnd^{arg:7}")))
]
})))
, var "<<DerivedGen.MkY>>" .$ implicitTrue .$ implicitTrue .= var "empty"
]
]
, scope =
var "Test.DepTyCheck.Gen.label"
.$ (var "fromString" .$ primVal (Str "DerivedGen.Y[0] (non-recursive)"))
.$ (var "<<DerivedGen.MkY>>" .$ var "^fuel_arg^" .$ var "inter^<{arg:3}>")
}
]
, IDef
emptyFC
"<DerivedGen.X>[0, 1]"
[ var "<DerivedGen.X>[0, 1]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^<{arg:4}>" .$ bindVar "inter^<{arg:5}>"
.= local
{ decls =
[ IClaim
(MkIClaimData
{ rig = MW
, vis = Export
, opts = []
, type =
mkTy
{ name = "<<DerivedGen.MkX>>"
, type =
MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel")
.-> MkArg MW ExplicitArg (Just "{arg:4}") (primVal (PrT StringType))
.-> MkArg MW ExplicitArg (Just "{arg:5}") (var "Prelude.Types.Nat")
.-> var "Test.DepTyCheck.Gen.Gen"
.$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty"
.$ (var "DerivedGen.X" .$ var "{arg:4}" .$ var "{arg:5}")
}
})
, IDef
emptyFC
"<<DerivedGen.MkX>>"
[ var "<<DerivedGen.MkX>>" .$ bindVar "^cons_fuel^" .$ bindVar "n" .$ bindVar "m"
.= var "Test.DepTyCheck.Gen.label"
.$ (var "fromString" .$ primVal (Str "DerivedGen.MkX (orders)"))
.$ ( var "Prelude.pure"
.! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue)
.$ (var "DerivedGen.MkX" .$ var "n" .$ var "m"))
]
]
, scope =
var "Test.DepTyCheck.Gen.label"
.$ (var "fromString" .$ primVal (Str "DerivedGen.X[0, 1] (non-recursive)"))
.$ (var "<<DerivedGen.MkX>>" .$ var "^fuel_arg^" .$ var "inter^<{arg:4}>" .$ var "inter^<{arg:5}>")
}
]
, IDef
emptyFC
"<DerivedGen.X>[1]"
[ var "<DerivedGen.X>[1]" .$ bindVar "^fuel_arg^" .$ bindVar "inter^<{arg:5}>"
.= local
{ decls =
[ IClaim
(MkIClaimData
{ rig = MW
, vis = Export
, opts = []
, type =
mkTy
{ name = "<<DerivedGen.MkX>>"
, type =
MkArg MW ExplicitArg Nothing (var "Data.Fuel.Fuel")
.-> MkArg MW ExplicitArg (Just "{arg:5}") (var "Prelude.Types.Nat")
.-> var "Test.DepTyCheck.Gen.Gen"
.$ var "Test.DepTyCheck.Gen.Emptiness.MaybeEmpty"
.$ ( var "Builtin.DPair.DPair"
.$ primVal (PrT StringType)
.$ ( MkArg MW ExplicitArg (Just "{arg:4}") (primVal (PrT StringType))
.=> var "DerivedGen.X" .$ var "{arg:4}" .$ var "{arg:5}"))
}
})
, IDef
emptyFC
"<<DerivedGen.MkX>>"
[ var "<<DerivedGen.MkX>>" .$ bindVar "^cons_fuel^" .$ bindVar "m"
.= var "Test.DepTyCheck.Gen.label"
.$ (var "fromString" .$ primVal (Str "DerivedGen.MkX (orders)"))
.$ ( var ">>="
.$ (var "external^<^prim^.String>[]" .$ var "^outmost-fuel^")
.$ ( MkArg MW ExplicitArg (Just "n") implicitFalse
.=> var "Prelude.pure"
.! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue)
.$ (var "Builtin.DPair.MkDPair" .$ implicitTrue .$ (var "DerivedGen.MkX" .$ var "n" .$ var "m"))))
]
]
, scope =
var "Test.DepTyCheck.Gen.label"
.$ (var "fromString" .$ primVal (Str "DerivedGen.X[1] (non-recursive)"))
.$ (var "<<DerivedGen.MkX>>" .$ var "^fuel_arg^" .$ var "inter^<{arg:5}>")
}
]
]
, scope = var "<DerivedGen.Y>[0]" .$ var "^outmost-fuel^" .$ var "outer^<n>"
}

1 change: 1 addition & 0 deletions tests/derivation/least-effort/print/adt/015 let function/run
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
../_common/run
17 changes: 17 additions & 0 deletions tests/derivation/least-effort/print/adt/016 let function/DerivedGen.idr
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
module DerivedGen

import Deriving.DepTyCheck.Gen

%default total

%language ElabReflection

data X : String -> Nat -> Type where
MkX : (n : _) -> (m : _) -> X n m

data Y : Nat -> Type where
MkY : forall n, m, k. let xx : Nat -> Nat; xx = S in X n (xx m) -> X n (xx k) -> Y (xx m)

%logging "deptycheck.derive.print" 5
%runElab deriveGenPrinter @{MainCoreDerivator @{LeastEffort}} $
Fuel -> (Fuel -> Gen MaybeEmpty String) => (Fuel -> Gen MaybeEmpty Nat) => (n : Nat) -> Gen MaybeEmpty $ Y n
1 change: 1 addition & 0 deletions tests/derivation/least-effort/print/adt/016 let function/derive.ipkg
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
../_common/derive.ipkg
Loading

0 comments on commit 67f4a7c

Please sign in to comment.