-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathPreprocess.hs
144 lines (123 loc) · 6.47 KB
/
Preprocess.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
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
module Preprocess where
import DataTypes
import HelperFunctions
import Control.Monad.State
-- Type annotation
annotateType :: Term -> Env -> Env -> (Term, Sort)
annotateType (Var v) sortEnv env
| v `elem` (map fst sortEnv) = let s = (typeOf v sortEnv) in (TopVarSort v s, s)
| v `elem` (map fst env) = let s = (typeOf v env) in (VarSort v s, s)
| otherwise = error $ "The sort environments do not contain the variable " ++ v ++ "."
annotateType t@(Num n) sortEnv env = (t, IntSort)
annotateType (Add u v) sortEnv env = annotateTypeArithmeticExp u v Add sortEnv env
annotateType (Sub u v) sortEnv env = annotateTypeArithmeticExp u v Sub sortEnv env
annotateType (Sma u v) sortEnv env = annotateTypeFirstOrderFormula u v Sma sortEnv env
annotateType (SmaEq u v) sortEnv env = annotateTypeFirstOrderFormula u v SmaEq sortEnv env
annotateType (Eq u v) sortEnv env = annotateTypeFirstOrderFormula u v Eq sortEnv env
annotateType (Lar u v) sortEnv env = annotateTypeFirstOrderFormula u v Lar sortEnv env
annotateType (LarEq u v) sortEnv env = annotateTypeFirstOrderFormula u v LarEq sortEnv env
annotateType (And u v) sortEnv env = annotateTypeBoolFormula u v And sortEnv env
annotateType (Or u v) sortEnv env = annotateTypeBoolFormula u v Or sortEnv env
annotateType (App u v) sortEnv env = annotateTypeApp u v sortEnv env
annotateType (Exists v s b) sortEnv env = annotateTypeExists v s b sortEnv env
annotateType (Lambda v s b) sortEnv env = annotateTypeLambda v s b sortEnv env
annotateTypeBinaryOp :: (Sort, Sort) -> Term -> Term -> (Term -> Term -> Term) -> Env -> Env -> (Term, Sort)
annotateTypeBinaryOp (s1, s2) u v f sortEnv env
| s3 == s1 && s4 == s1 = (f t1 t2, s2)
| otherwise = error $ "Type mismatch in " ++ show (f u v)
where (t1, s3) = annotateType u sortEnv env
(t2, s4) = annotateType v sortEnv env
annotateTypeArithmeticExp :: Term -> Term -> (Term -> Term -> Term) -> Env -> Env -> (Term, Sort)
annotateTypeArithmeticExp = annotateTypeBinaryOp (IntSort, IntSort)
annotateTypeFirstOrderFormula :: Term -> Term -> (Term -> Term -> Term) -> Env -> Env -> (Term, Sort)
annotateTypeFirstOrderFormula = annotateTypeBinaryOp (IntSort, BoolSort)
annotateTypeBoolFormula :: Term -> Term -> (Term -> Term -> Term) -> Env -> Env -> (Term, Sort)
annotateTypeBoolFormula = annotateTypeBinaryOp (BoolSort, BoolSort)
annotateTypeExists :: String -> Sort -> Term -> Env -> Env -> (Term, Sort)
annotateTypeExists v s1 b sortEnv env
| s2 == BoolSort = (Exists v s1 t, BoolSort)
| otherwise = error $ "Type mismatch in " ++ show (Exists v s1 b)
where (t, s2) = annotateType b sortEnv ((v, s1): env)
annotateTypeApp :: Term -> Term -> Env -> Env -> (Term, Sort)
annotateTypeApp u v sortEnv env
| s2 == source = (AppSort t1 t2 target, target)
| otherwise = error $ "Type mismatch in " ++ show (App u v)
where (t1, s1) = annotateType u sortEnv env
(t2, s2) = annotateType v sortEnv env
(source, target) = sourceTargetType s1
annotateTypeLambda :: String -> Sort -> Term -> Env -> Env -> (Term, Sort)
annotateTypeLambda v s1 b sortEnv env = (LambdaSort v s1 t s2, Arrow s1 s2)
where (t, s2) = annotateType b sortEnv ((v, s1): env)
-- Eta expansion
etaExpansion :: Sort -> Term -> State [String] Term
etaExpansion IntSort t = return t
etaExpansion BoolSort t = return t
etaExpansion (Arrow source target) (LambdaSort v s1 b s2)
| s1 == source = (etaExpansion target b) >>= (\t -> return (LambdaSort v s1 t s2))
| otherwise = error "The sort of a quantified variable does not match the source sort."
etaExpansion s t = do
xs <- get
let
sorts = init (decomposeSort s)
(as, bs) = splitAt (length sorts) xs
vars = map (\s -> "x_" ++ s) as
apps = addApps t (zip vars sorts)
lambdas = addLambdas apps (zip vars sorts)
put bs
return lambdas
-- Eliminate anonymous functions
-- This eliminates anonymous functions whilst ignoring the outermost lambda abstractions.
elimAnonymIgnoreLambdas :: Term -> State [String] (Term, [Equation])
elimAnonymIgnoreLambdas (LambdaSort v s1 b s2) = elimAnonymIgnoreLambdas b >>= (\(u, eqs) -> return (LambdaSort v s1 u s2, eqs))
elimAnonymIgnoreLambdas t = elimAnonym t
elimAnonym :: Term -> State [String] (Term, [Equation])
elimAnonym (Exists v s b) = elimAnonym b >>= (\(u, eqs) -> return (Exists v s u, eqs))
elimAnonym t1@(LambdaSort v s1 b s2) = do
(t2, bs) <- elimAnonymIgnoreLambdas t1
(x:xs) <- get
let freeVars = extractFreeVars t1
newVar = "X_" ++ x
sortNewVar = concatSort ((map snd freeVars) ++ [Arrow s2 s1])
apps = addApps (VarSort newVar sortNewVar) freeVars
lambdas = addLambdas t2 freeVars
put xs
return (apps, (newVar, lambdas): bs)
elimAnonym (And u v) = do
(t1, as) <- elimAnonym u
(t2, bs) <- elimAnonym v
return (And t1 t2, as ++ bs)
elimAnonym (Or u v) = do
(t1, as) <- elimAnonym u
(t2, bs) <- elimAnonym v
return (Or t1 t2, as ++ bs)
elimAnonym (AppSort u v s) = do
(t1, as) <- elimAnonym u
(t2, bs) <- elimAnonym v
return (AppSort t1 t2 s, as ++ bs)
elimAnonym t = return (t, [])
extractFreeVars :: Term -> Env
extractFreeVars (TopVarSort v s) = []
extractFreeVars (VarSort v s) = [(v, s)]
extractFreeVars (Num n) = []
extractFreeVars (Add u v) = extractFreeVars u ++ (extractFreeVars v)
extractFreeVars (Sub u v) = extractFreeVars u ++ (extractFreeVars v)
extractFreeVars (Sma u v) = extractFreeVars u ++ (extractFreeVars v)
extractFreeVars (SmaEq u v) = extractFreeVars u ++ (extractFreeVars v)
extractFreeVars (Eq u v) = extractFreeVars u ++ (extractFreeVars v)
extractFreeVars (Lar u v) = extractFreeVars u ++ (extractFreeVars v)
extractFreeVars (LarEq u v) = extractFreeVars u ++ (extractFreeVars v)
extractFreeVars (And u v)= extractFreeVars u ++ (extractFreeVars v)
extractFreeVars (Or u v)= extractFreeVars u ++ (extractFreeVars v)
extractFreeVars (AppSort u v s)= extractFreeVars u ++ (extractFreeVars v)
extractFreeVars (Exists v s b) = filter (\(var,s) -> var /= v) (extractFreeVars b)
extractFreeVars (LambdaSort v s1 b s2) = filter (\(var, s) -> var /= v) (extractFreeVars b)
-- Testing
-- Sample Term
sample = Lambda "x" IntSort (App (Var "f") (Lambda "y" BoolSort (Num 1)))
-- Sort environtment for the variable f
sortEnv = [("f", Arrow (Arrow BoolSort IntSort) (Arrow BoolSort IntSort))]
-- Sort of the sample term
sampleSort = Arrow IntSort (Arrow BoolSort IntSort)
annotatedSample = fst $ annotateType sample sortEnv []
outputNoAnonym = fst $ runState (elimAnonymIgnoreLambdas annotatedSample) freshVars
outputEtaExpanded = fst $ runState (etaExpansion sampleSort (fst outputNoAnonym)) freshVars