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
open Ppxlib
open Ttypes
module Ident = Identifier.Ident
type vsymbol = { vs_name : Ident.t; vs_ty : ty } [@@deriving show]
let create_vsymbol pid ty = { vs_name = Ident.of_preid pid; vs_ty = ty }
module Vs = struct
type t = vsymbol
let compare = Stdlib.compare
end
module Svs = Set.Make (Vs)
module Mvs = Map.Make (Vs)
type lsymbol = {
ls_name : Ident.t;
ls_args : ty list;
ls_value : ty option;
ls_constr : bool;
ls_field : bool;
}
[@@deriving show]
let ls_equal l r = Ident.equal l.ls_name r.ls_name
module LS = struct
type t = lsymbol
let compare = Stdlib.compare
let equal = ls_equal
let hash = (Hashtbl.hash : lsymbol -> int)
end
module Sls = Set.Make (LS)
module Mls = Map.Make (LS)
let lsymbol ?(constr = false) ~field ls_name ls_args ls_value =
{ ls_name; ls_args; ls_value; ls_constr = constr; ls_field = field }
let fsymbol ?(constr = false) ~field nm tyl ty =
lsymbol ~constr ~field nm tyl (Some ty)
let psymbol nm ty = lsymbol ~field:false nm ty None
let ls_subst_ts old_ts new_ts ({ ls_name; ls_constr; ls_field; _ } as ls) =
let ls_args = List.map (ty_subst_ts old_ts new_ts) ls.ls_args in
let ls_value = Option.map (ty_subst_ts old_ts new_ts) ls.ls_value in
lsymbol ls_name ls_args ls_value ~constr:ls_constr ~field:ls_field
let ls_subst_ty old_ts new_ts new_ty ls =
let subst ty = ty_subst_ty old_ts new_ts new_ty ty in
let ls_args = List.map subst ls.ls_args in
let ls_value = Option.map subst ls.ls_value in
lsymbol ls.ls_name ls_args ls_value ~constr:ls.ls_constr ~field:ls.ls_field
(** buil-in lsymbols *)
let ps_equ =
let tv = fresh_ty_var "a" in
psymbol Identifier.eq [ tv; tv ]
let fs_unit =
fsymbol ~constr:true ~field:false
(Ident.create ~loc:Location.none "()")
[] ty_unit
let fs_bool_true =
fsymbol ~constr:true ~field:false
(Ident.create ~loc:Location.none "true")
[] ty_bool
let fs_bool_false =
fsymbol ~constr:true ~field:false
(Ident.create ~loc:Location.none "false")
[] ty_bool
let fs_apply =
let ty_a, ty_b = (fresh_ty_var "a", fresh_ty_var "b") in
let ty_a_to_b = ty_app ts_arrow [ ty_a; ty_b ] in
fsymbol ~field:false
(Ident.create ~loc:Location.none "apply")
[ ty_a_to_b; ty_a ] ty_b
let tvo = ts_option.ts_args |> function [ v ] -> v.tv_name | _ -> assert false
let tvl = ts_list.ts_args |> function [ v ] -> v.tv_name | _ -> assert false
let tv_option = { Ttypes.ty_node = Ttypes.Tyvar { Ttypes.tv_name = tvo } }
let tv_list = { Ttypes.ty_node = Ttypes.Tyvar { Ttypes.tv_name = tvl } }
let fs_option_none =
fsymbol ~constr:true ~field:false Identifier.none [] (ty_option tv_option)
let fs_option_some =
fsymbol ~constr:true ~field:false Identifier.some [ tv_option ]
(ty_option tv_option)
let fs_list_nil =
fsymbol ~constr:true ~field:false Identifier.nil [] (ty_list tv_list)
let fs_list_cons =
fsymbol ~constr:true ~field:false Identifier.cons
[ tv_list; ty_list tv_list ]
(ty_list tv_list)
let fs_tuple_ids = Hashtbl.create 17
let fs_tuple =
let ls_tuples = Hashtbl.create 17 in
fun n ->
try Hashtbl.find ls_tuples n
with Not_found ->
let id = Ident.create ~loc:Location.none ("tuple" ^ string_of_int n) in
let ts = ts_tuple n in
let tyl = List.map ty_of_var ts.ts_args in
let ty = ty_app (ts_tuple n) tyl in
let ls = fsymbol ~constr:true ~field:false id tyl ty in
Hashtbl.add fs_tuple_ids id ls;
Hashtbl.add ls_tuples n ls;
ls
let is_fs_tuple fs = fs.ls_constr && Hashtbl.mem fs_tuple_ids fs.ls_name