@@ -1361,9 +1361,24 @@ rawBool False = Var (NS (UN "False") ["Bool", "Prelude"])
13611361rawNil :: Raw -> Raw
13621362rawNil ty = raw_apply (Var (NS (UN "Nil") ["List", "Prelude"])) [ty]
13631363
1364+rawCons :: Raw -> Raw -> Raw -> Raw
1365+rawCons ty hd tl = raw_apply (Var (NS (UN "::") ["List", "Prelude"])) [ty, hd, tl]
1366+
1367+rawList :: Raw -> [Raw] -> Raw
1368+rawList ty = foldr (rawCons ty) (rawNil ty)
1369+
13641370rawPairTy :: Raw -> Raw -> Raw
13651371rawPairTy t1 t2 = raw_apply (Var pairTy) [t1, t2]
13661372
1373+rawPair :: (Raw, Raw) -> (Raw, Raw) -> Raw
1374+rawPair (a, b) (x, y) = raw_apply (Var pairCon) [a, b, x, y]
1375+
1376+reflectCtxt :: [(Name, Type)] -> Raw
1377+reflectCtxt ctxt = rawList (rawPairTy (Var $ reflm "TTName") (Var $ reflm "TT"))
1378+ (map (\ (n, t) -> (rawPair (Var $ reflm "TTName", Var $ reflm "TT")
1379+ (reflectName n, reflect t)))
1380+ ctxt)
1381+
13671382reflectErr :: Err -> Raw
13681383reflectErr (Msg msg) = raw_apply (Var $ reflErrName "Msg") [RConstant (Str msg)]
13691384reflectErr (InternalMsg msg) = raw_apply (Var $ reflErrName "InternalMsg") [RConstant (Str msg)]
@@ -1373,8 +1388,71 @@ reflectErr (CantUnify b t1 t2 e ctxt i) =
13731388 , reflect t1
13741389 , reflect t2
13751390 , reflectErr e
1376− , rawNil $ rawPairTy (Var (reflm "TTName")) (Var (reflm "TT")) --FIXME
1391+ , reflectCtxt ctxt
13771392 , RConstant (I i)]
1393+reflectErr (InfiniteUnify n tm ctxt) =
1394+ raw_apply (Var $ reflErrName "InfiniteUnify")
1395+ [ reflectName n
1396+ , reflect tm
1397+ , reflectCtxt ctxt
1398+ ]
1399+reflectErr (CantConvert t t' ctxt) =
1400+ raw_apply (Var $ reflErrName "CantConvert")
1401+ [ reflect t
1402+ , reflect t'
1403+ , reflectCtxt ctxt
1404+ ]
1405+reflectErr (UnifyScope n n' t ctxt) =
1406+ raw_apply (Var $ reflErrName "UnifyScope")
1407+ [ reflectName n
1408+ , reflectName n'
1409+ , reflect t
1410+ , reflectCtxt ctxt
1411+ ]
1412+reflectErr (CantInferType str) =
1413+ raw_apply (Var $ reflErrName "CantInferType") [RConstant (Str str)]
1414+reflectErr (NonFunctionType t t') =
1415+ raw_apply (Var $ reflErrName "NonFunctionType") [reflect t, reflect t']
1416+reflectErr (NotEquality t t') =
1417+ raw_apply (Var $ reflErrName "NotEquality") [reflect t, reflect t']
1418+reflectErr (TooManyArguments n) = raw_apply (Var $ reflErrName "TooManyArguments") [reflectName n]
1419+reflectErr (CantIntroduce t) = raw_apply (Var $ reflErrName "CantIntroduce") [reflect t]
1420+reflectErr (NoSuchVariable n) = raw_apply (Var $ reflErrName "NoSuchVariable") [reflectName n]
1421+reflectErr (NoTypeDecl n) = raw_apply (Var $ reflErrName "NoTypeDecl") [reflectName n]
1422+reflectErr (NotInjective t1 t2 t3) =
1423+ raw_apply (Var $ reflErrName "NotInjective")
1424+ [ reflect t1
1425+ , reflect t2
1426+ , reflect t3
1427+ ]
1428+reflectErr (CantResolve t) = raw_apply (Var $ reflErrName "CantResolve") [reflect t]
1429+reflectErr (CantResolveAlts ss) =
1430+ raw_apply (Var $ reflErrName "CantResolve")
1431+ [rawList (Var $ (UN "String")) (map (RConstant . Str) ss)]
1432+reflectErr (IncompleteTerm t) = raw_apply (Var $ reflErrName "IncompleteTerm") [reflect t]
1433+reflectErr UniverseError = Var $ reflErrName "UniverseError"
1434+reflectErr ProgramLineComment = Var $ reflErrName "ProgramLineComment"
1435+reflectErr (Inaccessible n) = raw_apply (Var $ reflErrName "Inaccessible") [reflectName n]
1436+reflectErr (NonCollapsiblePostulate n) = raw_apply (Var $ reflErrName "NonCollabsiblePostulate") [reflectName n]
1437+reflectErr (AlreadyDefined n) = raw_apply (Var $ reflErrName "AlreadyDefined") [reflectName n]
1438+reflectErr (ProofSearchFail e) = raw_apply (Var $ reflErrName "ProofSearchFail") [reflectErr e]
1439+reflectErr (NoRewriting tm) = raw_apply (Var $ reflErrName "NoRewriting") [reflect tm]
1440+reflectErr (At fc err) = raw_apply (Var $ reflErrName "At") [reflectFC fc, reflectErr err]
1441+ where reflectFC (FC source line col) = raw_apply (Var $ reflErrName "FileLoc")
1442+ [ RConstant (Str source)
1443+ , RConstant (I line)
1444+ , RConstant (I col)
1445+ ]
1446+reflectErr (Elaborating str n e) =
1447+ raw_apply (Var $ reflErrName "Elaborating")
1448+ [ RConstant (Str str)
1449+ , reflectName n
1450+ , reflectErr e
1451+ ]
1452+reflectErr (ProviderError str) =
1453+ raw_apply (Var $ reflErrName "ProviderError") [RConstant (Str str)]
1454+reflectErr (LoadingFailed str err) =
1455+ raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]
13781456reflectErr x = raw_apply (Var (NS (UN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]
13791457
13801458withErrorReflection :: Idris a -> Idris a