-
Notifications
You must be signed in to change notification settings - Fork 1
/
CheckHub.hs
103 lines (90 loc) · 3.57 KB
/
CheckHub.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
-- | Tying scope checking and type checking together by using checking problems
module CheckHub where
import Surface
import Core
import ScopeChecking
import Derivation
import ElabSpec
import Internal
import Types
import LatexPrint
import Data.List
import Control.Applicative
import Prelude hiding (log)
-- Wrapping a type checking problem
-- the expressions of the tuple list are turned into
-- constants (in order) and have to be fully type checked
data ChkProb = ChkProb {constants :: [(Name,SExpr)], term :: SExpr, typ :: SExpr}
-- So this is what we want to have: a set of postulates, an expression and a type in Surface,
-- and a set of optional postulate-replacements in Internal, providing the ability to instantiate things manually
-- the type in Surface should also be replaceable eventually
data OptChkProb = OCP {posts :: [((Name,SExpr), Maybe Type)],
termS :: SExpr,
typeS :: (SExpr,Maybe Type)}
printDerivation :: [Rule] -> IO ()
printDerivation rs = do
let log = unlines (intersperse "\\\\" $ map (show . lP) (aggregate . compact $ rs))
writeFile "/home/jesper/dev/masterthesisproject/report/problems/derivlog.tex" log
-- Don't look at it right now
process :: ChkProb -> IO ()
process prob = do
let result = processProb prob
either (\err -> putStrLn "A scope checking error occured" >> putStrLn err) handle result
where handle (log,xi,expr,result) = do
-- printDerivation log
either (\err -> putStrLn "An elaboration error occured" >> putStrLn err) (handle' expr) result
putStrLn ""
putStrLn "==========================="
putStrLn "== Metas and constraints =="
putStrLn "==========================="
putStrLn ""
print xi
handle' expr (posts',typ',trm) = do
printSurface (constants prob) (typ prob) (term prob)
printCore expr
putStrLn ""
putStrLn "=============="
putStrLn "== Internal =="
putStrLn "=============="
putStrLn ""
putStrLn "== Postulates =="
putStrLn $ concatMap printPost' posts'
putStrLn "== Type =="
putStrLn . showTerm $ typ'
putStrLn "== Term =="
putStrLn . showTerm $ trm
putStrLn ""
printPost (n,typ') = n ++ " : " ++ show typ' ++ "\n"
printPost' (n,typ') = n ++ " : " ++ showTerm typ' ++ "\n"
-- ++ n ++ " : " ++ show typ' ++ "\n"
printLPost (n,typ') = n ++ " : " ++ latexTerm typ' ++ "\n"
printSurface psts typ' trm = do
putStrLn ""
putStrLn "============="
putStrLn "== Surface =="
putStrLn "============="
putStrLn ""
putStrLn "== Postulates =="
putStrLn $ concatMap printPost psts
putStrLn "== Type =="
print typ'
putStrLn "== Term =="
print trm
putStrLn ""
printCore (psts,typ',trm) = do
putStrLn ""
putStrLn "=========="
putStrLn "== Core =="
putStrLn "=========="
putStrLn ""
putStrLn "== Postulates =="
putStrLn $ concatMap printPost psts
putStrLn "== Type =="
print typ'
putStrLn "== Term =="
print trm
putStrLn ""
processProb :: ChkProb -> Either Error ([Rule], Xi, ([(Name,CExpr)], CExpr,CExpr), Either Error ([(Name,Type)],Type,Term))
processProb prob = go (unzip (constants prob)) (typ prob) (term prob)
where go (ns,pstS) typS trmS = ccurr ns elabProblem <$> snd (scopecheckProb pstS typS trmS)
ccurr ns f (a,b,c) = f (zip ns a) b c