programming-languages/hw5.ml at master · zhihaodev/programming-languages · GitHub

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
(* -------------------------------------------------------------------------------------------------- *)
(* HEADER: PLEASE FILL THIS IN                                                                        *)
(* -------------------------------------------------------------------------------------------------- *)

(*

  Name                        : Zhihao Cao
  List of team Members        : Jian Jin
  List of other collaborators :

*)


type label = Lab of string

type fbtype =
    TInt | TBool | TArrow of fbtype * fbtype | TRecord of (label * fbtype) list


let rec is_subtype t1 t2 =
    if t1 = t2 then
        true
    else
        match (t1, t2) with
        | (TRecord a, TRecord b) ->
            if (List.length a) < (List.length b) then
                false
            else
                scan_record a b
        | (TArrow (a, b), TArrow (c, d)) ->
            (is_subtype c a) && (is_subtype b d)
        | _ -> false

and

scan_record r1 r2 =
    match r2 with
    | [] -> true
    | hd :: tl ->
            if not (check_each_field r1 hd) then
                false
            else
                scan_record r1 tl

and

check_each_field r pair =
    match r with
    | [] -> false
    | hd :: tl ->
        let (l1, t1) = hd in
            let (l2, t2) = pair in
                if l1 = l2 then
                    is_subtype t1 t2
                else
                    check_each_field tl pair
;;


(*
# let r1 = TRecord [(Lab "x", TInt)] ;;
# let r2 = TRecord [(Lab "x", TInt); (Lab "y", TBool)] ;;
# let r3 = TRecord [(Lab "x", TInt); (Lab "y", TInt)] ;;
# let r4 = TRecord [] ;;
# let r5 = TRecord [(Lab "x", TInt); (Lab "y", TBool); (Lab "z", TRecord [(Lab "x", TInt)])] ;;
# let r6 = TArrow(r1, r2) ;;
# let r7 = TArrow(r4, r5) ;;
# is_subtype r2 r1 ;;
- : bool = true
# is_subtype r3 r2 ;;
- : bool = false
# is_subtype r7 r6 ;;
- : bool = true
*)


2.


τ ::= ... | [τ]


  Γ ⊢e_1 : τ,  ...,  Γ ⊢e_n : τ
---------------------------------
     Γ ⊢[e_1; ...; e_n] : [τ]


 Γ⊢e1 : τ,    Γ,[[ ]]:[τ] ⊢e2 : [τ]
-----------------------------------
         Γ⊢ e1 ++ e2 : [τ]


Γ ⊢e : [τ1],    Γ ⊢e1 : τ2,    Γ,h:τ1, t:[τ1] ⊢e2 : τ2
-----------------------------------------------------------
   Γ ⊢Match e With [[ ]] -> e1 | (h ++ t) -> e2 :  τ2