-
Notifications
You must be signed in to change notification settings - Fork 0
/
dmlpat.ml
139 lines (127 loc) · 5.08 KB
/
dmlpat.ml
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
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
(*********************************************************************)
(* *)
(* Dependent ML *)
(* *)
(* (c) Hongwei Xi *)
(* July 2000 *)
(* *)
(* University of Cincinnati *)
(* *)
(* Distributed by permission only. *)
(* *)
(*********************************************************************)
(* dmlpat: type-checking pattern matching clauses *)
open Dmlsyn
module L = Dmlloc
module G = Dmlglo
module D = Dmldeb
module C = Dmlcop
module S = Dmlsim
let dt_tv_ins dt =
match dt.dt_dsc with
DTlam(tctx, dt) ->
let _ = C.bind_tctx tctx in
let dt = C.cp_dt dt in
let _ = C.unbind_tctx tctx in dt
| _ -> dt
let dt_iv_ope dt = (* for constructors in patterns *)
match dt.dt_dsc with
DT_uni (ictx, dt) ->
let newictx = C.cp_ictx ictx in
let newdt = C.cp_dt dt in
let _ = C.unbind_ictx ictx in (newictx, newdt)
| DTlam _ -> G.abort ("dt_iv_ope: DTlam: " ^ (D.dt_pr dt))
| _ -> ([], dt)
let rec ictx_of_ind ictx (ind, ind') =
IDprop (IPeq (ind, ind')) :: ictx
and ictx_of_ind_list ictx = function
[], [] -> ictx
| (ind :: rest, ind' :: rest') ->
let ictx = ictx_of_ind ictx (ind, ind')
in ictx_of_ind_list ictx (rest, rest')
| _ -> G.abort ("ictx_of_ind_list: unequal length")
let rec dt_list_link = function
[], [] -> ()
| (dt :: rest, dt' :: rest') -> begin
match dt.dt_dsc with
DT_e ({ btv_dtlink = DTnolink } as btv) ->
btv.btv_dtlink <- DTlinkto dt'; dt_list_link (rest, rest')
| _ -> G.abort ("dt_list_link: " ^ (D.dt_pr dt))
end
| _ -> G.abort ("dt_list_link: unequal length")
let rec ictx_of_dt ictx ({ dt_dsc = tdsc }, { dt_dsc = tdsc' }) =
(*
let _ = print_string ("ictx_of_dt: " ^ (D.dt_dsc_pr tdsc) ^ ", " ^ (D.dt_dsc_pr tdsc') ^ "\n") in
*)
match tdsc, tdsc' with
DT_nam(dtlist, tcon, indlist), DT_nam(dtlist', tcon', indlist') ->
if tcon = tcon' then
let _ = dt_list_link (dtlist, dtlist')
in ictx_of_ind_list ictx (indlist, indlist')
else G.abort ("ictx_of_dt: " ^ (D.dt_dsc_pr tdsc) ^
" <> " ^ (D.dt_dsc_pr tdsc'))
| _ -> G.abort ("ictx_of_dt: " ^ (D.dt_dsc_pr tdsc) ^
" <> " ^ (D.dt_dsc_pr tdsc'))
let rec bat_of_pat bat dt pat =
match dt.dt_dsc with
DT_e btv -> begin
match btv.btv_dtlink with
DTnolink -> G.abort("bat_of_pat: DT_e: no link")
| DTlinkto dt -> bat_of_pat bat dt pat
end
| DT_exi (ictx, dt) ->
let newictx = C.cp_ictx ictx in
let newdt = C.cp_dt dt in
let _ = C.unbind_ictx ictx in
let _ = bat.bat_ictx <- newictx @ bat.bat_ictx in
let _ =
bat.bat_ubivlist <- ubivlist_of_ictx bat.bat_ubivlist newictx
in bat_of_pat bat newdt pat
| _ -> bat_of_pat_dsc bat dt pat.pat_dsc
and bat_of_pat_dsc bat dt = function
P_var vd ->
let (ictx, dt) = (C.open_dt [] dt) in
let _ = bat.bat_ictx <- ictx @ bat.bat_ictx in
let _ =
bat.bat_ubivlist <- ubivlist_of_ictx bat.bat_ubivlist ictx
in vd.var_typ <- Some dt
| Pany -> ()
| Pcst c ->
let ictx = ictx_of_dt [] (G.dt_const c, dt) in
let _ = bat.bat_ictx <- ictx @ bat.bat_ictx
in bat.bat_ubivlist <- ubivlist_of_ictx bat.bat_ubivlist ictx
| P_cstr_0 cd ->
let (ictx, cdt) = dt_iv_ope (dt_tv_ins cd.con_typ) in
let ictx = ictx_of_dt ictx (cdt, dt) in
let _ = bat.bat_ictx <- ictx @ bat.bat_ictx
in bat.bat_ubivlist <- ubivlist_of_ictx bat.bat_ubivlist ictx
| P_cstr_1 (cd, pat) ->
let (ictx, cdt) = dt_iv_ope (dt_tv_ins cd.con_typ)
in begin
match cdt.dt_dsc with
DTfun (arg_dt, res_dt) ->
let ictx = ictx_of_dt ictx (res_dt, dt) in
let _ = bat.bat_ictx <- ictx @ bat.bat_ictx in
let _ =
bat.bat_ubivlist <- ubivlist_of_ictx bat.bat_ubivlist ictx
in bat_of_pat bat arg_dt pat
| _ -> G.abort ("bat_of_pat_dsc: constructor type: " ^ (D.dt_pr cdt))
end
| Ptup (patlist) -> begin
match dt.dt_dsc with
DTtup dtlist -> bat_of_pat_list bat (dtlist, patlist)
| _ -> G.abort ("bat_of_pat_dsc: tuple type: " ^ (D.dt_pr dt))
end
| P_as (vd, pat) ->
let (ictx, dt) = (C.open_dt [] dt) in
let _ = bat.bat_ictx <- ictx @ bat.bat_ictx in
let _ =
bat.bat_ubivlist <- ubivlist_of_ictx bat.bat_ubivlist ictx
in (vd.var_typ <- Some dt; bat_of_pat bat dt pat)
| pdsc -> G.abort ("bat_of_pat: pdsc: " ^ (D.pat_dsc_pr pdsc))
and bat_of_pat_list bat = function
[], [] -> ()
| (dt :: dtlist, pat :: patlist) ->
let ictx = bat_of_pat bat dt pat
in bat_of_pat_list bat (dtlist, patlist)
| _ -> G.abort ("bat_of_pat_list: unequal length")