-
Notifications
You must be signed in to change notification settings - Fork 3
/
coresyntax.ml
176 lines (161 loc) · 6.88 KB
/
coresyntax.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
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
open Base
open Core.Std
open Vars
type astinfo = { astloc : srcloc; (* These first two should probably just be a srcloc *)
affineFrees : CS.t ref; (* Represent free instructions inserted right
before this one. Since we don't actually
perform transformations, this is easier. *)
}
with sexp, bin_io
(* TODO Remove this *)
let nullloc = Unknown
let nullinfo = { astloc = Unknown; affineFrees = ref CS.empty; }
(* constants for PicoML *)
type const = Int of int | Float of float | String of string with sexp, bin_io
let string_of_const c =
match c
with Int n -> string_of_int n
| Float f -> Float.to_string f
| String s -> "\"" ^ s ^ "\""
(* Infixed binary operators for PicoML *)
type binop = Add | Sub | Mul | Div | Exp | FAdd | FSub | FMul | FDiv
| Concat | Eq | Less
with sexp, bin_io
let string_of_binop = function
Add -> " + "
| Sub -> " - "
| Mul -> " * "
| Div -> " / "
| Exp -> " ** "
| FAdd -> " +. "
| FSub -> " -. "
| FMul -> " *. "
| FDiv -> " /. "
| Concat -> " ^ "
| Eq -> " = "
| Less -> " < "
(* Primitive unary operator in PicoML *)
type monop = Print | Neg | Assert | PrintStr | Flush | IToS | SexpToS | Sleep with sexp, bin_io
let string_of_monop m =
match m with
| Neg -> "~"
| Assert -> "assert"
| PrintStr -> "print_str"
| Print -> "print"
| Flush -> "flush"
| IToS -> "i2s"
| SexpToS -> "sexp2s"
| Sleep -> "sleep"
(* ASTInfo is not included in the descriptions *)
type exp =
| Var of astinfo * fvar (* variables *)
| Con of astinfo * const (* constants *)
| Sat of astinfo * string * exp list (* saturated constructor *)
| App of astinfo * exp * exp (* exp1 exp2 *)
| Bin of astinfo * binop * exp * exp (* exp1 % exp2
where % is a builtin binary operator *)
| Mon of astinfo * monop * exp (* % exp1
where % is a builtin monadic operator *)
| Fun of astinfo * fvar * exp (* fun x -> exp *)
| Let of astinfo * [`M of Fullsyntax.mtype | `P of Fullsyntax.ptype] * fvar * exp * exp (* let x = exp1 in exp2 *)
| Cas of astinfo * exp * ((fvar list * exp) SM.t)
| Monad of astinfo * cvar option * proc * cvar list * procType option (* c <-{P}<- cs *)
| Cast of astinfo * exp * Fullsyntax.mtype (* <e:t> *)
| Box of astinfo * exp * Fullsyntax.mtype (* [e:t] *)
| PolyApp of astinfo * fvar * Fullsyntax.stype list (* x<S,S,...> *)
and proc =
| Bind of astinfo * cvar * exp * cvar list * proc (* c <- e -< cs; P *)
| TailBind of astinfo * cvar * exp * cvar list (* c <- e -< cs *)
| Service of astinfo * cvar * fvar * proc (* c <- service Foo; P *)
| Register of astinfo * fvar * cvar * proc (* register Foo c; P *)
| InputD of astinfo * fvar * cvar * proc (* x <- input c; P *)
| OutputD of astinfo * cvar * exp * proc (* output c e; P *)
| InputC of astinfo * [`Tensor | `DwCastL | `UpCastR ] ref * cvar * cvar * proc (* c <- input d; P *)
| OutputC of astinfo * cvar * cvar * proc * proc (* output c (d <- P); Q *)
| Close of astinfo * cvar (* close c *)
| Exit of astinfo
| Wait of astinfo * cvar * proc (* wait c; P *)
| External of astinfo * cvar * proc LM.t (* case c of SM *)
| Internal of astinfo * cvar * label * proc (* select c.l; P *)
| Fwd of astinfo * cvar * cvar (* fwd c d *)
| InputTy of astinfo * tyvar * cvar * proc
| OutputTy of astinfo * cvar * Fullsyntax.stype * proc
| ShftUpL of astinfo * cvar * cvar * proc (* c1 <- send c2; P *)
| ShftDwR of astinfo * cvar * cvar * proc (* send c1 (c2 <- P) *)
(* Type for holding information need for our dynamic type checks.
In particular, every monadic value has a set of quantifiers, a map from expressions to
types, and a map from proc expressions to types. We use the maps to get the dynamic
type we either need to check or add as a tag. The set of quantifiers then is used at
run time to instantiate these local checks with new monomorphic variables that can be
safely unified against without destroying our overall types. An alternate approach
might have stored the checking information closer to its use, but I think this would
require walking the entire AST and duplicating most of it, which could be much more
expensive if there is a large amount of non-dynamically checked functional code. *)
and procType = ProcType of SS.t * (proc * Fullsyntax.mtype) list * (proc * Fullsyntax.stype) list
with sexp, bin_io (* TODO Do we use procType? *)
(* TODO check these for well-formedness *)
type toplvl = TopLet of fvar (* Name *)
* [`M of Fullsyntax.mtype | `P of Fullsyntax.ptype]
* exp (* let f : tau = ... ;; *)
| TopProc of cvar * proc
| MTypeDecl of fvar * [`M of string | `S of tyvar] list * Fullsyntax.mtype list SM.t
| STypeDecl of fvar * [`M of string | `S of tyvar] list * Fullsyntax.stype
| Pass
| ServDecl of fvar * Fullsyntax.stype
let getinfoE (e:exp) : astinfo =
match e with
| Var (i,_) -> i
| Con (i,_) -> i
| Sat (i,_,_) -> i
| App (i,_,_) -> i
| Bin (i,_,_,_) -> i
| Mon (i,_,_) -> i
| Fun (i,_,_) -> i
| Let (i,_,_,_,_) -> i
| Cas (i,_,_) -> i
| Monad (i,_,_,_,_) -> i
| Cast (i,_,_) -> i
| Box (i,_,_) -> i
| PolyApp (i,_,_) -> i
let getinfoP (p:proc) : astinfo =
match p with
| TailBind (i,_,_,_) -> i
| Bind (i,_,_,_,_) -> i
| InputD (i,_,_,_) -> i
| OutputD (i,_,_,_) -> i
| InputC (i,_,_,_,_) -> i
| OutputC (i,_,_,_,_) -> i
| Close (i,_) -> i
| Exit i -> i
| Wait (i,_,_) -> i
| External (i,_,_) -> i
| Internal (i,_,_,_) -> i
| Fwd (i,_,_) -> i
| OutputTy (i,_,_,_) -> i
| InputTy (i,_,_,_) -> i
| Service (i,_,_,_) -> i
| Register (i,_,_,_) -> i
| ShftUpL (i,_,_,_) -> i
| ShftDwR (i,_,_,_) -> i
let locE (e:exp) : srcloc = (getinfoE e).astloc
let locP (p:proc) : srcloc = (getinfoP p).astloc
(* Each process statement has at most one channel it communicates along. This returns it. *)
let focusedChan : proc -> cvar option = function
| TailBind _ -> None
| Bind _ -> None
| Fwd _ -> None (* TODO Might be wrong *)
| Service _ -> None (* TODO This is wrong *)
| Register _ -> None (* TODO This is wrong *)
| InputD (_,_,c,_) -> Some c
| OutputD (_,c,_,_) -> Some c
| InputC (_,_,_,c,_) -> Some c
| OutputC (_,c,_,_,_) -> Some c
| Close (_,c) -> Some c
| Wait (_,c,_) -> Some c
| Exit _ -> None
| External (_,c,_) -> Some c
| Internal (_,c,_,_) -> Some c
| OutputTy (_,c,_,_) -> Some c
| InputTy (_,_,c,_) -> Some c
| ShftUpL (_,_,c,_) -> Some c
| ShftDwR (_,c,_,_) -> Some c