1
1
use std:: collections:: HashMap ;
2
2
3
3
#[ derive( Clone ) ]
4
- pub enum Term {
4
+ pub enum Term < E > {
5
+ Num ( u64 ) ,
6
+ Str ( String ) ,
5
7
Var ( String ) ,
6
- Fun ( Environment , String , Box < Term > ) ,
7
- App ( Box < Term > , Box < Term > ) ,
8
+ Fun ( E , String , Type , Box < Term < E > > ) ,
9
+ App ( Box < Term < E > > , Box < Term < E > > ) ,
8
10
}
9
11
10
12
#[ derive( Clone ) ]
11
- pub struct Environment ( HashMap < String , Term > ) ;
13
+ pub struct Environment ( HashMap < String , Term < Environment > > ) ;
12
14
13
15
impl Environment {
14
16
pub fn init ( ) -> Self {
15
17
Self ( HashMap :: new ( ) )
16
18
}
17
- pub fn find ( & self , name : & String ) -> Option < Term > {
19
+ pub fn find ( & self , name : & String ) -> Option < Term < Environment > > {
18
20
match self . 0 . get ( name) {
19
21
Some ( term) => Some ( term. clone ( ) ) ,
20
22
None => None
21
23
}
22
24
}
23
- pub fn push ( & self , name : String , term : Term ) -> Self {
25
+ pub fn push ( & self , name : String , term : Term < Environment > ) -> Self {
24
26
let mut next_envt = self . 0 . clone ( ) ;
25
27
next_envt. insert ( name, term) ;
26
28
Self ( next_envt)
@@ -29,8 +31,22 @@ impl Environment {
29
31
30
32
#[ derive( Clone ) ]
31
33
pub enum Type {
32
- Atom ,
33
- Func ( Box < Type > , Box < Type > )
34
+ Num ,
35
+ Str ,
36
+ Fun ( Box < Type > , Box < Type > )
37
+ }
38
+
39
+ impl PartialEq for Type {
40
+ fn eq ( & self , other : & Self ) -> bool {
41
+ match ( self , other) {
42
+ ( Type :: Num , Type :: Num ) => true ,
43
+ ( Type :: Str , Type :: Str ) => true ,
44
+ ( Type :: Fun ( self_para, self_body) ,
45
+ Type :: Fun ( other_para, other_body) ) =>
46
+ self_para. eq ( other_para) && self_body. eq ( self_body) ,
47
+ _ => false
48
+ }
49
+ }
34
50
}
35
51
36
52
pub struct Context ( HashMap < String , Type > ) ;
@@ -42,4 +58,36 @@ impl Context {
42
58
None => None
43
59
}
44
60
}
61
+ pub fn push ( & self , name : String , ty : Type ) -> Self {
62
+ let mut new_ctx = self . 0 . clone ( ) ;
63
+ new_ctx. insert ( name, ty. clone ( ) ) ;
64
+ Self ( new_ctx)
65
+ }
66
+ }
67
+
68
+ fn synthesize ( ctx : & Context , term : & Term < Context > ) -> Option < Type > {
69
+ match term {
70
+ Term :: Num ( _) => Some ( Type :: Num ) ,
71
+ Term :: Str ( _) => Some ( Type :: Str ) ,
72
+ Term :: Var ( name) => ctx. find ( name) ,
73
+ Term :: Fun ( _, name, para_type, body) => {
74
+ let new_ctx = ctx. push ( name. clone ( ) , para_type. clone ( ) ) ;
75
+ let body_type = synthesize ( & new_ctx, & body) ?;
76
+ Some ( Type :: Fun ( Box :: new ( para_type. clone ( ) ) , Box :: new ( body_type) ) )
77
+ } ,
78
+ Term :: App ( lier, cant) => {
79
+ let lier = synthesize ( & ctx, & lier) ?;
80
+ let cant = synthesize ( & ctx, & cant) ?;
81
+ match lier {
82
+ Type :: Fun ( para_type, body_type) => {
83
+ if * para_type == cant {
84
+ Some ( * body_type)
85
+ } else {
86
+ None
87
+ }
88
+ } ,
89
+ _ => None
90
+ }
91
+ }
92
+ }
45
93
}
0 commit comments