-
Notifications
You must be signed in to change notification settings - Fork 85
/
Copy pathunify.hs
108 lines (94 loc) · 3.16 KB
/
unify.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
module Unify where
import Data.Map as Map
import Data.List as List
import Ast as Ast
type Uvar = Integer
data Infer_t =
Infer_Tvar_db Integer
| Infer_Tapp [Infer_t] Ast.Tc
| Infer_Tuvar Uvar
data T_print_ctxt =
Pc_fn_left
| Pc_fn_right
| Pc_tup
| Pc_app
| Pc_top
deriving Eq
print_t ctxt (Infer_Tvar_db i) =
show i
print_t ctxt (Infer_Tapp [t1,t2] TC_fn) =
if ctxt == Pc_fn_right || ctxt == Pc_top then
print_t Pc_fn_left t1 ++ " -> " ++ print_t Pc_fn_right t2
else
"(" ++ print_t Pc_fn_left t1 ++ " -> " ++ print_t Pc_fn_right t2 ++ ")"
print_t ctxt (Infer_Tapp ts TC_tup) =
if ctxt == Pc_fn_left || ctxt == Pc_fn_right || ctxt == Pc_top then
List.intercalate "*" (List.map (print_t Pc_tup) ts)
else
"(" ++ List.intercalate "*" (List.map (print_t Pc_tup) ts) ++ ")"
print_t ctxt (Infer_Tapp [] tc) = show tc
print_t ctxt (Infer_Tapp [t] tc) = print_t Pc_app t ++ " " ++ show tc
print_t ctxt (Infer_Tapp ts tc) = "(" ++ List.intercalate "," (List.map (print_t Pc_top) ts) ++ ") " ++ show tc
print_t ctxt (Infer_Tuvar uv) = "'a" ++ show uv
instance Show Infer_t where
show t = print_t Pc_top t
type Subst = Map.Map Uvar Infer_t
t_vwalk :: Subst -> Uvar -> Infer_t
t_vwalk s v =
case Map.lookup v s of
Nothing -> Infer_Tuvar v
Just (Infer_Tuvar u) -> t_vwalk s u
Just (Infer_Tapp ts tc') -> Infer_Tapp ts tc'
Just (Infer_Tvar_db n) -> Infer_Tvar_db n
t_walk :: Subst -> Infer_t -> Infer_t
t_walk s (Infer_Tuvar v) = t_vwalk s v
t_walk s (Infer_Tapp ts tc) = Infer_Tapp ts tc
t_walk s (Infer_Tvar_db n) = Infer_Tvar_db n
t_oc :: Subst -> Infer_t -> Uvar -> Bool
t_oc s t v =
case t_walk s t of
Infer_Tuvar u -> v == u
Infer_Tapp ts tc' -> List.any (\t -> t_oc s t v) ts
Infer_Tvar_db n -> False
t_ext_s_check :: Subst -> Uvar -> Infer_t -> Maybe Subst
t_ext_s_check s v t = if t_oc s t v then Nothing else Just (Map.insert v t s)
t_unify :: Subst -> Infer_t -> Infer_t -> Maybe Subst
t_unify s t1 t2 =
case (t_walk s t1, t_walk s t2) of
(Infer_Tuvar v1, Infer_Tuvar v2) ->
Just (if v1 == v2 then s else Map.insert v1 (Infer_Tuvar v2) s)
(Infer_Tuvar v1, t2) -> t_ext_s_check s v1 t2
(t1, Infer_Tuvar v2) -> t_ext_s_check s v2 t1
(Infer_Tapp ts1 tc1, Infer_Tapp ts2 tc2) ->
if tc1 == tc2 then
ts_unify s ts1 ts2
else
Nothing
(Infer_Tvar_db n1, Infer_Tvar_db n2) ->
if n1 == n2 then
Just s
else
Nothing
_ -> Nothing
ts_unify :: Subst -> [Infer_t] -> [Infer_t] -> Maybe Subst
ts_unify s [] [] = Just s
ts_unify s (t1:ts1) (t2:ts2) =
case t_unify s t1 t2 of
Nothing -> Nothing
Just s' -> ts_unify s' ts1 ts2
ts_unify s _ _ = Nothing
apply_subst_t :: Subst -> Infer_t -> Infer_t
apply_subst_t s (Infer_Tuvar n) =
case Map.lookup n s of
Nothing -> Infer_Tuvar n
Just t -> t
apply_subst_t s (Infer_Tapp ts tc) =
Infer_Tapp (List.map (apply_subst_t s) ts) tc
apply_subst_t s (Infer_Tvar_db n) =
Infer_Tvar_db n
t_walkstar :: Subst -> Infer_t -> Infer_t
t_walkstar s t =
case t_walk s t of
Infer_Tuvar v -> Infer_Tuvar v
Infer_Tapp ts tc0 -> Infer_Tapp (List.map (t_walkstar s) ts) tc0
Infer_Tvar_db n -> Infer_Tvar_db n