Created
February 6, 2014 17:46
-
-
Save david-christiansen/8849078 to your computer and use it in GitHub Desktop.
Idris has improved
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
%reflection | |
solveHasTable : Type -> Tactic | |
solveHasTable (HasTable (_::tl) name s) = | |
Try (Refine "Here" `Seq` Solve) | |
(Refine "There" `Seq` (Solve `Seq` solveHasTable (HasTable tl name s))) | |
solveHasTable (HasTable (a++b) _ _) = Refine "Here" `Seq` Solve | |
solveHasTable (HasTable _ name s) = Refine "Here" `Seq` Solve |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
hasTableHere : TTName | |
hasTableHere = (NS "Here" ["HasTable", "Database", "DB", "Providers"]) | |
hasTableThere : TTName | |
hasTableThere = (NS "There" ["HasTable", "Database", "DB", "Providers"]) | |
findHasTableProof : TT -> TT | |
findHasTableProof (App (App (App hasTable db) name) schema) = hasTableProof db name schema | |
where hasTableProof : TT -> TT -> TT -> TT | |
hasTableProof (App (App (P _ (NS (UN "::") ["Database", "DB", "Providers"]) _) hd) tl) name schema = | |
let (name', schema') = extractPair (unApply hd) in | |
if name' == name | |
then mkApp (P Ref hasTableHere Erased) [name, name', schema, tl, P Ref (UN "oh") Erased] | |
else mkApp (P Ref hasTableThere Erased) [tl, name, schema, name', schema', tl, hasTableProof tl name schema] | |
hasTableProof db name schema = (P Ref ("Failed to construct proof that " ++ show name ++ " is a table in " ++ show db ++ " with schema " ++ show schema) Erased) | |
findHasTableProof goal = P Ref ("Couldn't find HasTable proof for " ++ show goal) Erased | |
findHasTable : Nat -> List (TTName, Binder TT) -> TT -> Tactic | |
findHasTable _ ctxt goal = Exact $ findHasTableProof goal | |
findHasTable Z ctxt goal = seq [ Refine (NS (UN "Here") ["HasTable"]), Solve, Refine (UN "oh"), Solve] | |
findHasTable (S n) ctxt goal = Try (seq [ Refine (NS (UN "Here") ["HasTable"]) | |
, Refine (UN "oh") | |
, Solve | |
]) | |
(seq [ Refine (NS (UN "There") ["HasTable"]) | |
, Solve | |
, findHasTable n ctxt goal | |
]) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment