-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathecethesis.toc
90 lines (90 loc) · 6.66 KB
/
ecethesis.toc
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
\contentsline {chapter}{Chapter\ 1\hskip 1em\relax Introduction}{1}{chapter.1}
\contentsline {chapter}{Chapter\ 2\hskip 1em\relax Context Free Syntax}{3}{chapter.2}
\contentsline {section}{\numberline {2.1}K Explanation}{4}{section.2.1}
\contentsline {subsection}{\numberline {2.1.1}K Labels}{4}{subsection.2.1.1}
\contentsline {subsection}{\numberline {2.1.2}Strict}{4}{subsection.2.1.2}
\contentsline {section}{\numberline {2.2}Syntax Explanation}{4}{section.2.2}
\contentsline {section}{\numberline {2.3}Implementation of Section 10.2}{5}{section.2.3}
\contentsline {section}{\numberline {2.4}Implementation of Section 10.5}{6}{section.2.4}
\contentsline {subsection}{\numberline {2.4.1}Modules}{6}{subsection.2.4.1}
\contentsline {subsection}{\numberline {2.4.2}ImpDecls}{6}{subsection.2.4.2}
\contentsline {subsection}{\numberline {2.4.3}TopDecls}{8}{subsection.2.4.3}
\contentsline {subsection}{\numberline {2.4.4}Decls}{8}{subsection.2.4.4}
\contentsline {subsection}{\numberline {2.4.5}LExp}{10}{subsection.2.4.5}
\contentsline {subsection}{\numberline {2.4.6}AExp}{10}{subsection.2.4.6}
\contentsline {chapter}{Chapter\ 3\hskip 1em\relax Configuration}{12}{chapter.3}
\contentsline {section}{\numberline {3.1}Alpha}{13}{section.3.1}
\contentsline {section}{\numberline {3.2}Beta}{14}{section.3.2}
\contentsline {subsection}{\numberline {3.2.1}Example}{14}{subsection.3.2.1}
\contentsline {section}{\numberline {3.3}Delta}{15}{section.3.3}
\contentsline {subsection}{\numberline {3.3.1}Example}{15}{subsection.3.3.1}
\contentsline {section}{\numberline {3.4}Import Data Structure}{16}{section.3.4}
\contentsline {section}{\numberline {3.5}Modules}{16}{section.3.5}
\contentsline {chapter}{Chapter\ 4\hskip 1em\relax Context-Sensitive Checks}{17}{chapter.4}
\contentsline {section}{\numberline {4.1}Data Types}{17}{section.4.1}
\contentsline {subsection}{\numberline {4.1.1}Polymorphim}{17}{subsection.4.1.1}
\contentsline {section}{\numberline {4.2}Datatype Constructors}{18}{section.4.2}
\contentsline {subsection}{\numberline {4.2.1}Type}{18}{subsection.4.2.1}
\contentsline {subsection}{\numberline {4.2.2}Data}{18}{subsection.4.2.2}
\contentsline {subsection}{\numberline {4.2.3}Newtype}{19}{subsection.4.2.3}
\contentsline {subsection}{\numberline {4.2.4}Context}{19}{subsection.4.2.4}
\contentsline {section}{\numberline {4.3}Initial Data Structures}{19}{section.4.3}
\contentsline {subsection}{\numberline {4.3.1}Example T}{20}{subsection.4.3.1}
\contentsline {subsection}{\numberline {4.3.2}K Code}{21}{subsection.4.3.2}
\contentsline {section}{\numberline {4.4}context-sensitive Checks}{23}{section.4.4}
\contentsline {subsubsection}{K Code}{23}{section*.3}
\contentsline {subsection}{\numberline {4.4.1}Name Collision}{24}{subsection.4.4.1}
\contentsline {subsubsection}{K Code}{25}{section*.4}
\contentsline {subsection}{\numberline {4.4.2}Type Constructor Collision}{25}{subsection.4.4.2}
\contentsline {subsubsection}{K Code}{26}{section*.5}
\contentsline {subsection}{\numberline {4.4.3}Alpha Cycle Check}{26}{subsection.4.4.3}
\contentsline {subsubsection}{K Code}{27}{section*.6}
\contentsline {subsection}{\numberline {4.4.4}Argument Sort Check}{28}{subsection.4.4.4}
\contentsline {subsubsection}{K Code}{28}{section*.7}
\contentsline {subsection}{\numberline {4.4.5}Polymorphic Parameter Check}{29}{subsection.4.4.5}
\contentsline {subsubsection}{K Code}{30}{section*.8}
\contentsline {chapter}{Chapter\ 5\hskip 1em\relax Inferencing}{32}{chapter.5}
\contentsline {section}{\numberline {5.1}Type theory}{32}{section.5.1}
\contentsline {subsection}{\numberline {5.1.1}Simply Typed Lambda Calculus}{33}{subsection.5.1.1}
\contentsline {subsection}{\numberline {5.1.2}System F}{33}{subsection.5.1.2}
\contentsline {subsection}{\numberline {5.1.3}Hindley-Milner}{33}{subsection.5.1.3}
\contentsline {subsection}{\numberline {5.1.4}Meta Language}{33}{subsection.5.1.4}
\contentsline {section}{\numberline {5.2}Data Structures}{34}{section.5.2}
\contentsline {subsection}{\numberline {5.2.1}Transform T into Beta}{34}{subsection.5.2.1}
\contentsline {subsection}{\numberline {5.2.2}Construct Beta}{35}{subsection.5.2.2}
\contentsline {subsubsection}{Example}{35}{section*.9}
\contentsline {subsubsection}{K Code}{35}{section*.10}
\contentsline {subsection}{\numberline {5.2.3}Construct Delta}{37}{subsection.5.2.3}
\contentsline {subsubsection}{Example}{37}{section*.11}
\contentsline {section}{\numberline {5.3}Definition of Substitution}{38}{section.5.3}
\contentsline {section}{\numberline {5.4}Inference Algorithm}{38}{section.5.4}
\contentsline {subsection}{\numberline {5.4.1}Variable Rule}{40}{subsection.5.4.1}
\contentsline {subsection}{\numberline {5.4.2}Constant Rule}{41}{subsection.5.4.2}
\contentsline {subsection}{\numberline {5.4.3}Lambda Rule}{41}{subsection.5.4.3}
\contentsline {subsection}{\numberline {5.4.4}Application Rule}{43}{subsection.5.4.4}
\contentsline {subsection}{\numberline {5.4.5}IfThenElse Rule}{44}{subsection.5.4.5}
\contentsline {section}{\numberline {5.5}Mutual Recursion}{45}{section.5.5}
\contentsline {subsection}{\numberline {5.5.1}LetIn Rule}{46}{subsection.5.5.1}
\contentsline {subsubsection}{Module}{46}{section*.12}
\contentsline {subsubsection}{K Code}{47}{section*.13}
\contentsline {section}{\numberline {5.6}Helper Functions}{49}{section.5.6}
\contentsline {section}{\numberline {5.7}Fresh Instance}{50}{section.5.7}
\contentsline {section}{\numberline {5.8}GEN}{51}{section.5.8}
\contentsline {section}{\numberline {5.9}Unification Algorithm}{52}{section.5.9}
\contentsline {subsection}{\numberline {5.9.1}Identity}{52}{subsection.5.9.1}
\contentsline {subsection}{\numberline {5.9.2}Non-Identity}{53}{subsection.5.9.2}
\contentsline {subsubsection}{Delete}{53}{section*.14}
\contentsline {subsubsection}{Decompose}{53}{section*.15}
\contentsline {subsubsection}{Orient}{53}{section*.16}
\contentsline {subsubsection}{Eliminate}{53}{section*.17}
\contentsline {subsection}{\numberline {5.9.3}K Code}{54}{subsection.5.9.3}
\contentsline {section}{\numberline {5.10}Composition of Substitutions}{55}{section.5.10}
\contentsline {section}{\numberline {5.11}Example}{56}{section.5.11}
\contentsline {chapter}{Chapter\ 6\hskip 1em\relax Multiple Module Support}{59}{chapter.6}
\contentsline {section}{\numberline {6.1}Algorithm}{59}{section.6.1}
\contentsline {chapter}{Chapter\ 7\hskip 1em\relax Conclusion}{61}{chapter.7}
\contentsline {chapter}{Appendix\ A\hskip 1em\relax haskell-syntax.k}{62}{appendix.A}
\contentsline {chapter}{Appendix\ B\hskip 1em\relax haskell-configuration.k}{74}{appendix.B}
\contentsline {chapter}{Appendix\ C\hskip 1em\relax haskell-preprocessing.k}{76}{appendix.C}
\contentsline {chapter}{Appendix\ D\hskip 1em\relax haskell-type-inferencing.k}{97}{appendix.D}
\contentsline {chapter}{References}{112}{appendix*.18}