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
4bd8252e
Commit
4bd8252e
authored
May 13, 2016
by
charguer
Browse files
fixtypos
parent
421a8ce2
Changes
1
Hide whitespace changes
Inline
Sidebyside
Showing
1 changed file
with
17 additions
and
10 deletions
+17
10
doc/normalization_pseudocode.ml
doc/normalization_pseudocode.ml
+17
10
No files found.
doc/normalization_pseudocode.ml
View file @
4bd8252e
...
...
@@ 15,6 +15,10 @@ type pat =

Pconstr
of
cstr
*
pat
(* C(p1, .., pN) *)
let
fresh_var
=
let
r
=
ref
0
in
(
fun
()
>
incr
r
;
string_of_int
!
r
)
(*************************************************************)
(* Source language *)
...
...
@@ 65,7 +69,7 @@ and avals = aval list
type
atrm
=

Aval
of
aval
(* v *)
(* v *)

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

Alet
of
var
*
atrm
*
atrm
...
...
@@ 117,15 +121,15 @@ and bindings = binding list
let
apply_binding
b
t0
=
match
b
with

T
indingTrm
(
x
,
t
)
>
Alet
(
x
,
t
,
t0
)

T
indingFun
(
f
,
x
,
t
)
>
Aletfun
(
f
,
x
,
t
,
t0
)

B
indingTrm
(
x
,
t
)
>
Alet
(
x
,
t
,
t0
)

B
indingFun
(
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
List
.
fold_right
apply_binding
bs
t0
(*************************************************************)
...
...
@@ 157,7 +161,7 @@ let rec tr_val e =

ResTrm
t
>
let
x
=
fresh_var
()
in
let
v
=
Avar
x
in
let
bs2
=
bs
@
BindingTrm
(
x
,
t
)
in
let
bs2
=
bs
@
[
BindingTrm
(
x
,
t
)
]
in
(
v
,
bs2
)
and
tr_trm
e
=
...
...
@@ 166,7 +170,7 @@ and tr_trm e =
apply_bindings
bs
t0
and
tr_any
e
=
match
t
with
match
e
with

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

Ecst
n
>
...
...
@@ 175,8 +179,11 @@ and tr_any e =
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
)
let
(
vs
,
bs
)
=
tr_vals
[
e1
;
e2
]
in
begin
match
vs
with

[
v1
;
v2
]
>
(
ResTrm
(
Aapp
(
v1
,
v2
))
,
bs
)

_
>
assert
false
end

Elet
(
f
,
Efun
(
x
,
e1
)
,
e2
)
>
let
t1
=
tr_trm
e1
in
let
t2
=
tr_trm
e2
in
...
...
@@ 204,14 +211,14 @@ and tr_any e =
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
>
List
.
fold_right
(
fun
e
(
rs
,
bs
)
>
let
(
r
,
bs2
)
=
tr_any
e
in
(
r
::
rs
,
bs
@
bs2
)
)
es
([]
,
[]
)
and
tr_vals
es
=
(* idem. *)
List
.
fold_right
(
fun
(
vs
,
bs
)
e
>
List
.
fold_right
(
fun
e
(
vs
,
bs
)
>
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