idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-20 18:21:47 +03:00
Code Issues Projects Releases Wiki Activity
c54c1a6e97
Idris2/tests/idris2/literate006/expected

18 lines
513 B
Plaintext
Raw Normal View History

Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
1/1: Building Door (Door.lidr)
Add linear pair/dependent pair to the prelude I'm playing with some linear structures and finding these useful a lot, so good to have a consistent syntax for it. '#' is chosen because it's short, looks a bit like a cross if you look at it from the right angle (!) and so as not to clash with '@@' in preorder reasoning syntax.
2020-06-12 13:18:12 +03:00
Main> > (val # y) => ?now_4
Main> > (True # d) => ?now_4
> (False # d) => ?now_5
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
Main> 0 m : Type -> Type
1 d : Door Open
x : Integer
Look at intermediate results in program search This has involved quite a bit of reorganisation and some improvements in resugaring so that the results look nice. In summary: * Expression search now gives back a RawImp rather than a checked term, which allows it to include case expressions * Case with one pattern is resugared to a destructuring let * Some name generation issues address in function generation We look at intermediate results for local variables which are functions that return a concrete type, or recursive calls that return a single constructor type. In these cases, we: * let bind the local variable/recursive call * generate a new definition for the scope, as a 'case' function When we recursively generate the definition, it's a bit more restricted so as not to explode the search space. We only take the first result, we only look one constructor deep, and we go right to left on variable splitting so only deconstruct the name we've just added.
2020-08-04 14:51:57 +03:00
0 r : Res Bool (\r => Door (if r then Open else Closed))
Prettyprinting hole context
2020-08-18 15:36:34 +03:00
------------------------------
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
now_2 : Use Many m ()
Main> 0 m : Type -> Type
1 d : Door Closed
x : Integer
Look at intermediate results in program search This has involved quite a bit of reorganisation and some improvements in resugaring so that the results look nice. In summary: * Expression search now gives back a RawImp rather than a checked term, which allows it to include case expressions * Case with one pattern is resugared to a destructuring let * Some name generation issues address in function generation We look at intermediate results for local variables which are functions that return a concrete type, or recursive calls that return a single constructor type. In these cases, we: * let bind the local variable/recursive call * generate a new definition for the scope, as a 'case' function When we recursively generate the definition, it's a bit more restricted so as not to explode the search space. We only take the first result, we only look one constructor deep, and we go right to left on variable splitting so only deconstruct the name we've just added.
2020-08-04 14:51:57 +03:00
0 r : Res Bool (\r => Door (if r then Open else Closed))
Prettyprinting hole context
2020-08-18 15:36:34 +03:00
------------------------------
Add test script They don't all pass yet, for minor reasons. Coming shortly... Unfortunately the startup overhead for chez is really noticeable here!
2020-05-19 20:25:18 +03:00
now_3 : Use Many m ()
Main> Bye for now!
Reference in New Issue Copy Permalink