-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
Showing
9 changed files
with
260 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,20 @@ | ||
data Exp | ||
= Let (List1 (PatExp, DataExp)) DataExp | ||
| If DataExp DataExp DataExp | ||
| Case DataExp (List1 (PatExp, DataExp)) | ||
| App DataExp (List1 DataExp) | ||
| Ref Name | ||
| Val Data | ||
|
||
data Pat | ||
= UndPat | ||
| AppPat ConstrName (List1 Pat) | ||
| TupPat (List2 Pat) | ||
| VarPat (Maybe Pat) | ||
| LitPat Lit | ||
|
||
data Lit | ||
= BoolLit Bool | ||
| IntLit Int | ||
| FloatLit Float | ||
| StrLit String |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,41 @@ | ||
Module = Definition* | ||
|
||
Definition | ||
= "type" TypeName "=" TypeExpr ;; type alias | ||
| "data" TypeName "=" ConstrName TypeExpr* ( "|" ConstrName TypeExpr* )* ;; datatype | ||
| DataName PatExpr* "=" DataExpr ;; function | ||
|
||
TypeExpr | ||
= "(" TypeExprNP ( "," TypeExprNP )+ ")" ;; tuple type | ||
| "(" TypeName TypeExpr+ ")" ;; type app in parens | ||
| "()" ;; unit type (note there are no 1-tuple, just 0 and 2+) | ||
|
||
TypeExprNP = TypeExpr | TypeName TypeExpr+ ;; type app w/o parens | ||
|
||
DataExpr | ||
= "let" ( Pat "=" DataExpr )+ "in" DataExpr ;; LET IN | ||
| "if" DataExpr "then" DataExpr "else" DataExpr ;; conditional | ||
| "case" DataExpr "of" ( PatExpr "->" DataExpr )+ ;; matching | ||
| "(" DataExpr ( "," DataExpr )+ ")" ;; tuple | ||
| "(" DataExpr ")" ;; just parenthesises expr (for simplicity) | ||
| ( ConstrName | DataName ) DataExpr* ;; application and reference (as 0-application) | ||
| Lit ;; literal | ||
|
||
|
||
PatExpr | ||
= "_" ;; anonymous | ||
| "(" ConstrName Pat+ ")" ;; destructor | ||
| "(" PatExpr ( "," PatExpr )+ ;; tuple | ||
| DataName "@" Pat ;; AS pattern | ||
| DataName ;; simple pattern | ||
| Lit ;; verbatim | ||
|
||
Lit = NUMBER | DOUBLE_STRING | ||
TypeName = UPCASE | ||
ConstrName = UPCASE | ||
DataName = LOCASE | ||
|
||
;; --------------- | ||
|
||
;; predefined types: OMap UMap OSet USet <tuples> | ||
;; library types: List0 List1 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,58 @@ | ||
type TypEnv = OMap TypeName TypeDef | ||
type DefEnv = OMap DataName Def | ||
type ValEnv = OMap DataName Val | ||
|
||
lookup_local defs name = ??? | ||
lookup_global env name = ??? | ||
|
||
type Def = List1 (List0 Pat,Exp) | ||
|
||
data Val | ||
= LitVal Lit | ||
| OMpVal (OMap Data Data) ??? | ||
| OStVal (OSet Data Data) ??? | ||
| AppVal ConstrName (List1 Data) | ||
| TupVal (List2 Data) | ||
|
||
eval (If v e2 e3) env = | ||
match v of | ||
Lit (BoolLit b) -> if b then eval e2 env else eval e3 env | ||
_ -> error "type error" | ||
|
||
eval a@(AppVal h aa) = | ||
case lookup_local env h of | ||
Some cc -> eval_cases cc aa env | ||
None -> | ||
case lookup_global h of | ||
Some cc -> eval_cases cc aa env | ||
None -> a | ||
|
||
eval (Let dd e) env = eval_defs dd env | ||
eval (Case e cc) env = eval_cases (l1to0 cc) e env | ||
|
||
eval_defs Nil env = env | ||
eval_defs (Cons (p,e) dd) env = | ||
case match p (eval e env) env of | ||
Some env' -> eval_defs dd env' | ||
None -> error "let pattern failed" | ||
|
||
eval_cases Nil e1 env = error "non exhaustive case operator" | ||
eval_cases (Cons (p,e2) cc) e1 env = | ||
case match p e1 env of | ||
Some env' -> eval e2 env' | ||
None -> eval_cases cc e1 env | ||
|
||
match UndPat _ env = Some env | ||
match (VarPat n None) v env = Some (extend env n v) | ||
match (VarPat n (Some p)) v env = match p v (extend env n v) | ||
match (AppPat ph pp) (AppVal vh vv) env = if eq ph vh then match_all pp vv env | ||
match (TupPat pp) (TupVal vv) env = match_all pp vv env | ||
match _ _ _ = None | ||
|
||
match_all Nil (Cons _ _) _ = None | ||
match_all (Cons _ _) Nil _ = None | ||
match_all Nil Nil env = Some env | ||
match_all (Cons p pp) (Cons v vv) env = | ||
case match p v env of | ||
Some env' -> match_all pp vv env' | ||
None -> None |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,60 @@ | ||
data BinInt = Pos (List1 Bit) | Zero | Neg (List1 Bit) | ||
|
||
neg (Pos m) = Neg m | ||
neg Zero = Zero | ||
neg (Neg m) = Pos m | ||
|
||
sub a b = add a (neg b) | ||
|
||
abs (Pos a) = Pos a | ||
abs Zero = Zero | ||
abs (Neg a) = Pos a | ||
|
||
add Zero b = b | ||
add a Zero = a | ||
add (Pos a) (Pos b) = Pos (add_magnitudes a b) | ||
add (Pos a) (Neg b) = ??? | ||
add (Neg a) (Pos b) = ??? | ||
add (Neg a) (Neg b) = Neg (add_magnitudes a b) | ||
|
||
sub_loop aa Nil borrow = ??? | ||
sub_loop Nil bb borrow = ??? | ||
sub_loop (Cons a aa) (Cons b bb) borrow = | ||
let | ||
(a_minus_b, borrow_1) = bit_sub a b | ||
(result, borrow_2) = bit_sub a_minus_b borrow | ||
tail = sub_loop aa bb (bit_or borrow_1 borrow_2) | ||
in | ||
Cons result tail | ||
|
||
add_magnitudes (List1 a aa) (List1 b bb) = | ||
let | ||
(a_plus_b, carry) = bit_add a b | ||
tail = add_loop aa bb carry | ||
in | ||
List1 a_plus_b tail | ||
|
||
add_loop aa Nil carry = ??? | ||
add_loop Nil bb carry = ??? | ||
add_loop (Cons a aa) (Cons b bb) carry = | ||
let | ||
(a_plus_b, carry_1) = bit_add a b | ||
(result, carry_2) = bit_add a_plus_b carry | ||
tail = add_loop aa bb (bit_or carry_1 carry_2) | ||
in | ||
Cons result tail | ||
|
||
mul a b = ??? | ||
|
||
mod a b = ??? | ||
|
||
trunc_div a b = ??? | ||
|
||
print_binary a = bin2s a | ||
|
||
bin2s (Pos aa) = strcat "+" ( bb2s (l1to0 aa) 1 0 ) | ||
bin2s Zero = " 0" | ||
bin2s (Neg aa) = strcat "-" ( bb2s (l1to0 aa) 1 0 ) | ||
|
||
bb2s (Cons a aa) !m !a = bb2s aa (int_mul m 2) (int_add a (int_mul m (b2i a))) | ||
bb2s Nil _ _ = 0 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,38 @@ | ||
data Bit = I | O | ||
|
||
bit_sub O O = (O, O) | ||
bit_sub O I = (I, I) | ||
bit_sub I O = (I, O) | ||
bit_sub I I = (O, O) | ||
|
||
bit_add O O = (O, O) | ||
bit_add O I = (I, O) | ||
bit_add I O = (I, O) | ||
bit_add I I = (O, I) | ||
|
||
bit_xor O O = O | ||
bit_xor O I = I | ||
bit_xor I O = I | ||
bit_xor I I = O | ||
|
||
bit_or O O = O | ||
bit_or I O = I | ||
bit_or O I = I | ||
bit_or I I = I | ||
|
||
bit_and O O = O | ||
bit_and I O = O | ||
bit_and O I = O | ||
bit_and I I = I | ||
|
||
bit_not O = I | ||
bit_not I = O | ||
|
||
bit_id O = O | ||
bit_id I = I | ||
|
||
b2b O = True | ||
b2b I = False | ||
|
||
b2i O = 0 | ||
b2i I = 1 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,19 @@ | ||
map2 f (List2 a1 a2 aa) = List2 (f a1) (f a2) (map0 f aa) | ||
map1 f (List1 a aa) = List1 (f a) (map0 f aa) | ||
map0 f (Cons a aa) = Cons (f a) (map0 f aa) | ||
map0 _ Nil = Nil | ||
|
||
l1to0 (List1 a aa) = Cons a aa | ||
l2to0 (List2 a1 a2 aa) = Cons a1 (Cons a2 aa) | ||
l2to1 (List2 a1 a2 aa) = List1 a1 (Cons a2 aa) | ||
|
||
reverse aa = reverse_to aa Nil | ||
|
||
reverse_to (Cons a aa) bb = reverse_to aa (Cons a bb) | ||
reverse_to Nil bb = bb | ||
|
||
concat Nil bb = bb | ||
concat (Cons a aa) bb = Cons a (concat aa bb) | ||
|
||
singleton0 a = Cons a Nil | ||
singleton1 a = List1 a Nil |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,6 @@ | ||
data List0 a = Cons a | Nil -- [!] embedded! | ||
data List1 a = List1 a (List0 a) -- [!] embedded! | ||
data List2 a = List2 a a (List0 a) -- [!] embedded! | ||
data Option a = Some a | None | ||
|
||
data OMap = ??? ??? ??? |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
apply_logical op1 op2 op3 (Cons a aa) (Cons b bb) = Cons (op1 a b) (apply_logical op1 op2 op3 aa bb) | ||
apply_logical op1 op2 op3 a@(Cons _ _) Nil = map0 op2 a | ||
apply_logical op1 op2 op3 Nil b@(Cons _ _) = map0 op3 b | ||
apply_logical op1 op2 op3 Nil Nil = Nil | ||
|
||
prepend2 a aa = (Cons a (Cons a aa)) | ||
prepend4 a aa = prepend2 a (prepend2 a aa) | ||
prepend8 a aa = prepend4 a (prepend4 a aa) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,10 @@ | ||
data Uint8 -- 0 1 2 3 4 5 6 7 | ||
= UInt8 Bit Bit Bit Bit Bit Bit Bit Bit | ||
|
||
uint8_to_bb (Uint8 b0 b1 b2 b3 b4 b5 b6 b7) = Cons b0 (Cons b1 (Cons b2 (Cons b3 (Cons b4 (Cons b5 (Cons b6 (Cons b7 Nil))))))) | ||
|
||
bb_to_uint8 aa = | ||
case apply_logical bit_or bit_id bit_id a zero8 of | ||
Cons b0 (Cons b1 (Cons b2 (Cons b3 (Cons b4 (Cons b5 (Cons b6 (Cons b7 bb))))))) -> (Uint8 b0 b1 b2 b3 b4 b5 b6 b7, bb) | ||
|
||
zero8 = prepend8 O Nil |