-
Notifications
You must be signed in to change notification settings - Fork 0
/
types.ml
110 lines (96 loc) · 4.81 KB
/
types.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
let print_for_debug msg = ()
type variable_name = string
type source_type = source_type_main * Range.t
and source_type_main =
| TypeVariable of int
| IntType
| BoolType
| FuncType of source_type * source_type
| CircleType of source_type
| BoxType of source_type
type source_tree = source_tree_main * Range.t
and source_tree_main =
| SrcOrdContentOf of variable_name
| SrcPermContentOf of variable_name
| SrcApply of source_tree * source_tree
| SrcLambda of (variable_name * Range.t) * source_tree
| SrcFixPoint of (variable_name * Range.t) * source_tree
| SrcIfThenElse of source_tree * source_tree * source_tree
| SrcNext of source_tree
| SrcPrev of source_tree
| SrcBox of source_tree
| SrcUnbox of (variable_name * Range.t) * int * source_tree * source_tree
| SrcIntConst of int
| SrcBoolConst of bool
type abstract_tree = abstract_tree_main * int
and abstract_tree_main =
| OrdContentOf of variable_name
| PermContentOf of variable_name
| Apply of abstract_tree * abstract_tree
| Lambda of variable_name * abstract_tree
| FixPoint of variable_name * abstract_tree
| IfThenElse of abstract_tree * abstract_tree * abstract_tree
| Next of abstract_tree
| Prev of abstract_tree
| Box of abstract_tree
| Unbox of variable_name * int * abstract_tree * abstract_tree
| IntConst of int
| BoolConst of bool
let rec string_of_source_tree sast =
let iter = string_of_source_tree in
let (sastmain, _) = sast in
match sastmain with
| SrcOrdContentOf(varnm) -> varnm
| SrcPermContentOf(varnm) -> varnm
| SrcApply(sast1, sast2) -> "(" ^ (iter sast1) ^ " " ^ (iter sast2) ^ ")"
| SrcLambda((varnm, _), sast1) -> "(\\" ^ varnm ^ ". " ^ (iter sast1) ^ ")"
| SrcFixPoint((varnm, _), sast1) -> "(fix " ^ varnm ^ ". " ^ (iter sast1) ^ ")"
| SrcIfThenElse(sast0, sast1, sast2) -> "(if " ^ (iter sast0) ^ " then " ^ (iter sast1) ^ " else " ^ (iter sast2) ^ ")"
| SrcNext(sast1) -> "(next " ^ (iter sast1) ^ ")"
| SrcPrev(sast1) -> "(prev " ^ (iter sast1) ^ ")"
| SrcBox(sast1) -> "(box " ^ (iter sast1) ^ ")"
| SrcUnbox((varnm, _), i, sast1, sast2) -> "(unbox " ^ varnm ^ " =" ^ (string_of_int i)
^ " " ^ (iter sast1) ^ " in " ^ (iter sast2) ^ ")"
| SrcIntConst(nc) -> string_of_int nc
| SrcBoolConst(bc) -> string_of_bool bc
let rec string_of_source_type (srcty : source_type) =
let iter = string_of_source_type in
let iter_enclose srcty =
match srcty with
| (FuncType(_, _), _) -> "(" ^ (iter srcty) ^ ")"
| _ -> iter srcty
in
let (srctymain, _) = srcty in
match srctymain with
| TypeVariable(i) -> "'" ^ (string_of_int i)
| IntType -> "int"
| BoolType -> "bool"
| CircleType(tyin) -> "O" ^ (iter_enclose tyin)
| BoxType(tyin) -> "B" ^ (iter_enclose tyin)
| FuncType(tydom, tycod) -> (iter_enclose tydom) ^ " -> " ^ (iter tycod)
let rec string_of_abstract_tree (ast : abstract_tree) =
let iter = string_of_abstract_tree in
let (astmain, layer) = ast in
let strlayer s = "(" ^ (string_of_int layer) ^ "| " ^ s ^ ")" in
match astmain with
| OrdContentOf(ovnm) -> strlayer ovnm
| PermContentOf(pvnm) -> strlayer pvnm
| Apply(ast1, ast2) -> strlayer ((iter ast1) ^ " " ^ (iter ast2))
| Lambda(ovnm, ast1) -> strlayer ("\\" ^ ovnm ^ ". " ^ (iter ast1))
| FixPoint(ovnm, ast1) -> strlayer ("fix " ^ ovnm ^ ". " ^ (iter ast1))
| IfThenElse(ast0, ast1, ast2) -> strlayer ("if " ^ (iter ast0) ^ " then " ^ (iter ast1) ^ " else " ^ (iter ast2))
| Next(ast1) -> strlayer ("next " ^ (iter ast1))
| Prev(ast1) -> strlayer ("prev " ^ (iter ast1))
| Box(ast1) -> strlayer ("box " ^ (iter ast1))
| Unbox(pvnm, i, ast1, ast2) -> strlayer ("unbox " ^ pvnm ^ " =" ^ (string_of_int i) ^ " " ^ (iter ast1) ^ " in " ^ (iter ast2))
| IntConst(ic) -> strlayer (string_of_int ic)
| BoolConst(bc) -> strlayer (string_of_bool bc)
let rec erase_range_of_source_type (srcty : source_type) =
let (srctymain, _) = srcty in
let iter = erase_range_of_source_type in
let dr = Range.dummy "erased" in
match srctymain with
| FuncType(tydom, tycod) -> (FuncType(iter tydom, iter tycod), dr)
| CircleType(tyin) -> (CircleType(iter tyin), dr)
| BoxType(tyin) -> (BoxType(iter tyin), dr)
| _ -> (srctymain, dr)