Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Very basic example of using elaborator reflection to interactively fill in a hole in a function implementation.
-- Note that :elab does not automatically do :module Language.Reflection.Elab
-- for you. When you finish a proof, the same applies, so we have to also
-- add an import statement here, otherwise we'll get an error:
--
-- When checking right hand side of Main.shouldBeEmptyString:
-- No such variable Language.Reflection.Elab.Elab
import Language.Reflection.Elab
fillMeIn : List String -> String
fillMeIn strings =
case strings of
Nil =>
-- The ? creates a hole. This can be interactively filled using
-- :elab at the Idris REPL. On completion of the proof,
-- it writes out a definition that you can paste into the file.
?shouldBeEmptyString
string :: _ =>
string
-- This is the definition written out on :qed.
-- Try commenting this out and using :elab to fill the hole yourself.
-- Don't forget to run :module Language.Reflection.Elab first!
--
-- Once you have that working, try replacing the strings variable with an
-- unused variable (hint: look at `:doc intro`, then `:doc TTName`).
{-
Main.shouldBeEmptyString = %runElab (do intro $ UN "strings"
fill $ RConstant $ Str ""
solve)
-}
{-
*SimpleElaborationExample> :printdef fillMeIn
fillMeIn : List String -> String
fillMeIn strings = case strings of
[] => shouldBeEmptyString strings
(string :: _) => string
*SimpleElaborationExample> :printdef shouldBeEmptyString
shouldBeEmptyString : List String -> String
shouldBeEmptyString = let tacticExpr =
PE_>>=_585bb10e (intro (UN "strings"))
(\bindx =>
PE_>>=_585bb10e (fill (RConstant (Str "")))
(\bindx =>
solve))
in \strings => ""
*SimpleElaborationExample> fillMeIn []
"" : String
*SimpleElaborationExample> fillMeIn ["hi", "there"]
"hi" : String
-}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.