Idris2/tests/idris2/reflection002/expected

1/1: Building power (power.idr)
Main> Main.cube : Nat -> Nat
cube = \x => mult x (mult x (mult x (const (fromInteger 1) x)))
Main> 27
Main> Main.cube' : Nat -> Nat
cube' = \x => mult (mult (plus x 0) x) x
Main> 27
Main> Bye for now!
Progress on elaborator reflection Add %runElab and start on scripts, although all they can do so far is check a term. This does gives us, sort of, "template Idris" (as demonstrated in test reflection002) 2020-05-31 03:36:54 +03:00			`1/1: Building power (power.idr)`
			`Main> Main.cube : Nat -> Nat`
Reduce amount of normalisation in elab scripts We don't want to unfold definitions in 'pure' or 'check' or 'bind' since we want the exact expression that the script author has used. 2020-06-03 02:22:03 +03:00			`cube = \x => mult x (mult x (mult x (const (fromInteger 1) x)))`
Progress on elaborator reflection Add %runElab and start on scripts, although all they can do so far is check a term. This does gives us, sort of, "template Idris" (as demonstrated in test reflection002) 2020-05-31 03:36:54 +03:00			`Main> 27`
Add alternative example to reflection002 A bit more typesafe... 2020-06-03 01:56:30 +03:00			`Main> Main.cube' : Nat -> Nat`
Improve elaborator reflection performance In a 'Bind', normalise the result of the first action, rather than quoting the HNF. This improves performance since the HNF could be quite big when quoted back. Ideally, we wouldn't have to quote and unquote here, and we can probably achieve this by tinkering with the evaluator. This has an unfortunate effect on the reflection002 test, in that the "typed template Idris" example now evaluates too much. But, I think the overall performance is too important for the primary motivation behind elaborator reflection. I will return to this! 2020-07-17 17:18:23 +03:00			`cube' = \x => mult (mult (plus x 0) x) x`
Add alternative example to reflection002 A bit more typesafe... 2020-06-03 01:56:30 +03:00			`Main> 27`
Progress on elaborator reflection Add %runElab and start on scripts, although all they can do so far is check a term. This does gives us, sort of, "template Idris" (as demonstrated in test reflection002) 2020-05-31 03:36:54 +03:00			`Main> Bye for now!`