Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Open sidebar
CHARGUERAUD Arthur
cfml
Commits
421a8ce2
Commit
421a8ce2
authored
May 13, 2016
by
charguer
Browse files
normalization
parent
38d59aeb
Changes
1
Hide whitespace changes
Inline
Sidebyside
Showing
1 changed file
with
218 additions
and
0 deletions
+218
0
doc/normalization_pseudocode.ml
doc/normalization_pseudocode.ml
+218
0
No files found.
doc/normalization_pseudocode.ml
0 → 100644
View file @
421a8ce2
(*************************************************************)
(* Common constructs *)
type
var
=
string
and
vars
=
var
list
type
cstr
=
string
type
pat
=

Pvar
of
var
(* x *)

Pcst
of
int
(* n *)

Pconstr
of
cstr
*
pat
(* C(p1, .., pN) *)
(*************************************************************)
(* Source language *)
type
etrm
=

Evar
of
var
(* x *)

Ecst
of
int
(* n *)

Econstr
of
cstr
*
etrms
(* C(e1, ..., en) *)

Eapp
of
etrm
*
etrm
(* (e1 e2) *)

Elet
of
var
*
etrm
*
etrm
(* let(rec) x = e1 in e2 *)

Eif
of
etrm
*
etrm
*
etrm
(* if e1 then e2 else e3 *)

Ematch
of
etrm
*
ebranches
(* match e1 with bes *)

Efun
of
var
*
etrm
(* fun x > e1 *)
and
etrms
=
etrm
list
and
ebranch
=
pat
*
etrm
(* pi > ei *)
and
ebranches
=
ebranch
list
(* p1 > e1  ..  pn > en *)
(*************************************************************)
(* Target language *)
type
aval
=

Avar
of
var
(* x *)

Acst
of
int
(* n *)

Aconstr
of
cstr
*
avals
(* C(v1, ..., vn) *)
(* Note: at runtime, type aval also includes closures,
but there are no closures in the source code.
Same applies for program locations. *)
and
avals
=
aval
list
type
atrm
=

Aval
of
aval
(* v *)

Aapp
of
aval
*
aval
(* (v1 v2) *)

Alet
of
var
*
atrm
*
atrm
(* let x = t1 in t2 *)

Aletfun
of
var
*
var
*
atrm
*
atrm
(* let rec f x = t1 in t2 *)

Aif
of
aval
*
atrm
*
atrm
(* if v1 then t2 else t3 *)

Amatch
of
aval
*
abranches
(* match v with bas *)
and
atrms
=
atrm
list
and
abranch
=
pat
*
atrm
(* pi > ti *)
and
abranches
=
abranch
list
(* p1 > t1  ..  pn > tn *)
(*************************************************************)
(* Translation auxiliary definitions *)
(* Internally, the translation of a term of type [etrm]
produces a [res], which is either a value or a term. *)
type
res
=

ResVal
of
aval

ResTrm
of
atrm
(* A [res] can always be viewed as a term. *)
let
atrm_of_res
r
=
match
r
with

ResVal
v
>
Aval
v

ResTrm
t
>
t
(* Bindings, used internally by the translation. *)
type
binding
=

BindingTrm
of
var
*
atrm
(* let x = t *)

BindingFun
of
var
*
var
*
atrm
(* let rec f x = t *)
and
bindings
=
binding
list
(** [apply_binding b t0] computes, e.g.,
[let x = t t0]. *)
let
apply_binding
b
t0
=
match
b
with

TindingTrm
(
x
,
t
)
>
Alet
(
x
,
t
,
t0
)

TindingFun
(
f
,
x
,
t
)
>
Aletfun
(
f
,
x
,
t
,
t0
)
(** [apply_bindings bs t0] computes, e.g.,
[let x1 = t1 in .. let xn = tn in t0],
where [bs = (x1,t1)::...::(xn,tn)]. *)
let
apply_bindings
bs
t0
=
fold_right
apply_binding
bs
t0
(*************************************************************)
(* Translation *)
(* There are five mutually recursive functions
 [tr_any e] produces a pair (r, bs), made
of a result of type [res] (a value or a term),
and a list of bindings.
 [tr_val e] produces a pair (v, bs), made of a
value of type [aval] and a list of bindings.
 [tr_trm e] produces a term t of type [atrm]
 [tr_anys es] produces a (rs, bs) made of a list of
results of type [res], and a list of bindings.
 [tr_vals es] produces a (vs, bs) made of a list of
results of type [aval], and a list of bindings.
*)
let
rec
tr_val
e
=
let
(
r
,
bs
)
=
tr_any
e
in
match
r
with

ResVal
v
>
(
v
,
bs
)

ResTrm
t
>
let
x
=
fresh_var
()
in
let
v
=
Avar
x
in
let
bs2
=
bs
@
BindingTrm
(
x
,
t
)
in
(
v
,
bs2
)
and
tr_trm
e
=
let
(
r
,
bs
)
=
tr_any
e
in
let
t0
=
atrm_of_res
r
in
apply_bindings
bs
t0
and
tr_any
e
=
match
t
with

Evar
x
>
(
ResVal
(
Avar
x
)
,
[]
)

Ecst
n
>
(
ResVal
(
Acst
n
)
,
[]
)

Econstr
(
c
,
es
)
>
let
(
vs
,
bs
)
=
tr_vals
es
in
(
ResVal
(
Aconstr
(
c
,
vs
))
,
bs
)

Eapp
(
e1
,
e2
)
>
let
([
v1
;
v2
]
,
bs
)
=
tr_vals
[
e1
;
e2
]
in
(
ResTrm
(
Aapp
(
v1
,
v2
))
,
bs
)

Elet
(
f
,
Efun
(
x
,
e1
)
,
e2
)
>
let
t1
=
tr_trm
e1
in
let
t2
=
tr_trm
e2
in
(
ResTrm
(
Aletfun
(
f
,
x
,
t1
,
t2
))
,
[]
)

Efun
(
x
,
e1
)
>
(* only for anonymous functions *)
let
f
=
fresh_var
()
in
let
t1
=
tr_trm
e1
in
(
ResVal
(
Avar
f
)
,
[
BindingFun
(
f
,
x
,
t1
)])

Elet
(
x
,
e1
,
e2
)
>
let
(
r1
,
bs1
)
=
tr_any
e1
in
let
t1
=
atrm_of_res
r1
in
let
t2
=
tr_trm
e2
in
(
ResTrm
(
Alet
(
x
,
t1
,
t2
))
,
bs1
)

Eif
(
e1
,
e2
,
e3
)
>
let
(
v1
,
bs1
)
=
tr_val
e1
in
let
t2
=
tr_trm
e2
in
let
t3
=
tr_trm
e3
in
(
ResTrm
(
Aif
(
v1
,
t2
,
t3
))
,
bs1
)

Ematch
(
e1
,
bes
)
>
let
(
v1
,
bs1
)
=
tr_val
e1
in
let
bas
=
List
.
map
(
fun
(
p
,
e
)
>
(
p
,
tr_trm
e
))
bes
in
(
ResTrm
(
Amatch
(
v1
,
bas
))
,
bs1
)
and
tr_anys
es
=
(* assume here righttoleft evaluation order, as in OCaml;
otherwise, replace [bs @ bs2] with [bs2 @ bs]. *)
List
.
fold_right
(
fun
(
rs
,
bs
)
e
>
let
(
r
,
bs2
)
=
tr_any
e
in
(
r
::
rs
,
bs
@
bs2
)
)
es
([]
,
[]
)
and
tr_vals
es
=
(* idem. *)
List
.
fold_right
(
fun
(
vs
,
bs
)
e
>
let
(
v
,
bs2
)
=
tr_val
e
in
(
v
::
vs
,
bs
@
bs2
)
)
es
([]
,
[]
)
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment