Idris2/tests/idris2/reflection002/power.idr

import Language.Reflection

%language ElabReflection

powerFn : Nat -> TTImp
powerFn Z = `(const 1)
powerFn (S k) = `(\x => mult x (~(powerFn k) x))

powerFn' : Nat -> Elab (Nat -> Nat)
powerFn' Z = pure (const 1)
powerFn' (S k) = do powerk <- powerFn' k
                    pure (\x => mult (powerk x) x)

%macro
power : Nat -> Elab (Nat -> Nat)
power n = check (powerFn n)

%macro
power' : Nat -> Elab (Nat -> Nat)
power' n = powerFn' n

cube : Nat -> Nat
cube = power 3

cube' : Nat -> Nat
cube' = power' 3
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			`import Language.Reflection`

			`%language ElabReflection`

			`powerFn : Nat -> TTImp`
			powerFn Z = `(const 1)
			powerFn (S k) = `(\x => mult x (~(powerFn k) x))

Add alternative example to reflection002 A bit more typesafe... 2020-06-03 01:56:30 +03:00			`powerFn' : Nat -> Elab (Nat -> Nat)`
			`powerFn' Z = pure (const 1)`
			`powerFn' (S k) = do powerk <- powerFn' k`
			`pure (\x => mult (powerk x) x)`

Implement %macro flag A %macro must always be fully applied. Whenever the elaborator encounters a %macro application (except in a function LHS) it evaluates the application and sends the result to %runElab. So: %macro foo : args -> Elab TT ... def = foo a b c is equivalent to foo : args -> Elab TT ... def = %runElab foo a b c 2020-06-01 19:55:54 +03:00			`%macro`
In reflection, check now takes a concrete type So the type of Elab now gives the expected type that's being elaborated to, meaning that we can run 'check' in the middle of scripts and use the result. 2020-06-03 00:41:37 +03:00			`power : Nat -> Elab (Nat -> Nat)`
Implement %macro flag A %macro must always be fully applied. Whenever the elaborator encounters a %macro application (except in a function LHS) it evaluates the application and sends the result to %runElab. So: %macro foo : args -> Elab TT ... def = foo a b c is equivalent to foo : args -> Elab TT ... def = %runElab foo a b c 2020-06-01 19:55:54 +03:00			`power n = check (powerFn n)`

Add alternative example to reflection002 A bit more typesafe... 2020-06-03 01:56:30 +03:00			`%macro`
			`power' : Nat -> Elab (Nat -> Nat)`
			`power' n = powerFn' n`

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			`cube : Nat -> Nat`
Implement %macro flag A %macro must always be fully applied. Whenever the elaborator encounters a %macro application (except in a function LHS) it evaluates the application and sends the result to %runElab. So: %macro foo : args -> Elab TT ... def = foo a b c is equivalent to foo : args -> Elab TT ... def = %runElab foo a b c 2020-06-01 19:55:54 +03:00			`cube = power 3`
Add alternative example to reflection002 A bit more typesafe... 2020-06-03 01:56:30 +03:00
			`cube' : Nat -> Nat`
			`cube' = power' 3`