Skip to content
GitLab
Explore
Sign in
Primary navigation
Search or go to…
Project
J
jsexplain
Manage
Activity
Members
Code
Repository
Branches
Commits
Tags
Repository graph
Compare revisions
Build
Pipelines
Jobs
Pipeline schedules
Artifacts
Deploy
Releases
Container Registry
Model registry
Operate
Environments
Analyze
Contributor analytics
CI/CD analytics
Repository analytics
Model experiments
Help
Help
Support
GitLab documentation
Compare GitLab plans
Community forum
Contribute to GitLab
Provide feedback
Keyboard shortcuts
?
Snippets
Groups
Projects
Show more breadcrumbs
Verified Software
jsexplain
Commits
747387a3
Commit
747387a3
authored
8 years ago
by
charguer
Committed by
Thomas Wood
8 years ago
Browse files
Options
Downloads
Patches
Plain Diff
monadic_notation
parent
28cb46e3
No related branches found
Branches containing commit
No related tags found
No related merge requests found
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
generator/TODO
+29
-0
29 additions, 0 deletions
generator/TODO
generator/js_of_ast.ml
+98
-13
98 additions, 13 deletions
generator/js_of_ast.ml
generator/tests/jsref/JsInterpreter.ml
+61
-38
61 additions, 38 deletions
generator/tests/jsref/JsInterpreter.ml
with
188 additions
and
51 deletions
generator/TODO
+
29
−
0
View file @
747387a3
pas forcément le bon affichage si dest_inline sur une monade
----
special display on "elseif"
---------
Cop_value_prim with value 2
Cop_value_prim with value 2
---
---
fix highlight using
enter run_expr / exit run_expr
enter run_expr / exit run_expr
----
----
...
@@ -14,6 +24,7 @@ inline let object_loc_comparable x y =
...
@@ -14,6 +24,7 @@ inline let object_loc_comparable x y =
-----
-----
let%if_spec (s,x) = expr in cont
let%if_spec (s,x) = expr in cont
becomes
becomes
if_spec expr (fun s x -> cont)
if_spec expr (fun s x -> cont)
...
@@ -21,6 +32,24 @@ and in pseudo:
...
@@ -21,6 +32,24 @@ and in pseudo:
Let%spec x = expr in
Let%spec x = expr in
cont
cont
[("run", "if_run");
("string", "if_string");
("object", "if_object");
("value", "if_value");
("prim", "if_prim");
("number", "if_number");
("some", "if_some");
("bool", "if_bool");
("void", "if_void");
("success", "if_success");
("not_throw", "if_not_throw");
("ter", "if_ter");
("break", "if_break");
let if_run w k = if_spec w k
if_string w k
let if_object w k =
------------
------------
...
...
This diff is collapsed.
Click to expand it.
generator/js_of_ast.ml
+
98
−
13
View file @
747387a3
...
@@ -135,6 +135,20 @@ let map_cstr_fields ?loc bind (cstr : constructor_description) elements =
...
@@ -135,6 +135,20 @@ let map_cstr_fields ?loc bind (cstr : constructor_description) elements =
error
?
loc
(
"Insufficient fieldnames for arguments to "
^
cstr
.
cstr_name
)
error
?
loc
(
"Insufficient fieldnames for arguments to "
^
cstr
.
cstr_name
)
(** Decomposition of functions *)
let
function_get_args_and_body
e
=
let
rec
aux
pats
body
=
match
body
.
exp_desc
with
|
Texp_function
(
_
,
c
::
[]
,
Total
)
->
let
(
p
,
body2
)
=
(
c
.
c_lhs
,
c
.
c_rhs
)
in
aux
(
p
::
pats
)
body2
|
_
->
List
.
rev
pats
,
body
in
aux
[]
e
(****************************************************************)
(****************************************************************)
(* === comparison *)
(* === comparison *)
...
@@ -180,6 +194,7 @@ let coercion_functions =
...
@@ -180,6 +194,7 @@ let coercion_functions =
"JsSyntax.res_normal"
;
"JsSyntax.res_normal"
;
"JsSyntax.res_ref"
;
"JsSyntax.res_ref"
;
"JsSyntax.res_val"
;
"JsSyntax.res_val"
;
"JsInterpreterMonads.res_spec"
;
"JsInterpreterMonads.res_out"
;
"JsInterpreterMonads.res_out"
;
"JsInterpreterMonads.res_ter"
;
"JsInterpreterMonads.res_ter"
;
"JsInterpreterMonads.result_out"
;
"JsInterpreterMonads.result_out"
;
...
@@ -233,6 +248,28 @@ let is_coercion_constructor lident =
...
@@ -233,6 +248,28 @@ let is_coercion_constructor lident =
b
b
(* Do not generate events for particular functions *)
let
is_monadic_function
f
=
match
f
.
exp_desc
with
|
Texp_ident
(
path
,
ident
,
_
)
->
let
x
=
Path
.
name
path
in
List
.
mem
x
[
"JsInterpreterMonads.if_run"
;
"JsInterpreterMonads.if_string"
;
"JsInterpreterMonads.if_object"
;
"JsInterpreterMonads.if_value"
;
"JsInterpreterMonads.if_prim"
;
"JsInterpreterMonads.if_number"
;
"JsInterpreterMonads.if_some"
;
"JsInterpreterMonads.if_bool"
;
"JsInterpreterMonads.if_void"
;
"JsInterpreterMonads.if_success"
;
"JsInterpreterMonads.if_not_throw"
;
"JsInterpreterMonads.if_ter"
;
"JsInterpreterMonads.if_break"
;]
|
_
->
false
(****************************************************************)
(****************************************************************)
...
@@ -821,14 +858,8 @@ and js_of_expression ctx dest e =
...
@@ -821,14 +858,8 @@ and js_of_expression ctx dest e =
sexp
sexp
|
Texp_function
(
_
,
c
::
[]
,
Total
)
->
|
Texp_function
(
_
,
c
::
[]
,
Total
)
->
let
rec
explore
pats
e
=
match
e
.
exp_desc
with
let
pats
,
body
=
function_get_args_and_body
e
|
Texp_function
(
_
,
c
::
[]
,
Total
)
->
(* DEPRECATED: function_get_args_and_body e [c.c_lhs] c.c_rhs *)
in
let
(
p
,
e
)
=
(
c
.
c_lhs
,
c
.
c_rhs
)
in
explore
(
p
::
pats
)
e
|
_
->
List
.
rev
pats
,
e
in
let
pats
,
body
=
explore
[
c
.
c_lhs
]
c
.
c_rhs
in
let
pats_clean
=
List
.
filter
(
fun
pat
->
is_mode_not_pseudo
()
||
not
(
is_hidden_type
pat
.
pat_type
))
pats
in
let
pats_clean
=
List
.
filter
(
fun
pat
->
is_mode_not_pseudo
()
||
not
(
is_hidden_type
pat
.
pat_type
))
pats
in
let
arg_ids
=
List
.
map
ident_of_pat
pats_clean
in
let
arg_ids
=
List
.
map
ident_of_pat
pats_clean
in
let
newctx
=
ctx_fresh
()
in
let
newctx
=
ctx_fresh
()
in
...
@@ -836,6 +867,64 @@ and js_of_expression ctx dest e =
...
@@ -836,6 +867,64 @@ and js_of_expression ctx dest e =
let
sexp
=
generate_logged_enter
body
.
exp_loc
arg_ids
ctx
newctx
sbody
in
let
sexp
=
generate_logged_enter
body
.
exp_loc
arg_ids
ctx
newctx
sbody
in
apply_dest'
ctx
dest
sexp
apply_dest'
ctx
dest
sexp
|
Texp_apply
(
f
,
exp_l
)
when
is_monadic_function
f
->
let
sl_clean
=
exp_l
|>
List
.
map
(
fun
(
_
,
eo
,
_
)
->
match
eo
with
|
None
->
out_of_scope
loc
"optional apply arguments"
|
Some
ei
->
ei
)
in
let
(
e1
,
e2
)
=
match
sl_clean
with
|
[
e1
;
e2
]
->
(
e1
,
e2
)
|
_
->
out_of_scope
loc
"not exactly two arguments provided to monad"
in
let
fname
=
match
f
.
exp_desc
with
|
Texp_ident
(
path
,
ident
,
_
)
->
Path
.
last
path
|
_
->
assert
false
in
let
monad_name
=
let
n
=
String
.
length
fname
in
if
n
<=
3
then
out_of_scope
loc
"monad name does not start with 'if_'"
;
String
.
sub
fname
3
(
n
-
3
)
in
let
sexp1
=
inline_of_wrap
e1
in
let
pats
,
body
=
function_get_args_and_body
e2
in
let
sbody
=
js_of_expression
ctx
Dest_return
body
in
let
pats_clean
=
List
.
filter
(
fun
pat
->
is_mode_not_pseudo
()
||
not
(
is_hidden_type
pat
.
pat_type
))
pats
in
let
arg_ids
=
List
.
map
ident_of_pat
pats_clean
in
let
(
token_start1
,
token_stop1
,
_token_loc
)
=
token_fresh
!
current_mode
loc
in
let
(
token_start2
,
token_stop2
,
_token_loc
)
=
token_fresh
!
current_mode
loc
in
(* token1 placed on sexp1
token2 placed on ids *)
if
is_mode_pseudo
()
then
begin
let
id
=
match
arg_ids
with
|
[]
->
"_"
(*deprecated: Printf.sprintf "@[<hov 2>%s%s;%s@]@,%s" token_start sexp1 token_stop sbody*)
|
[
id
]
->
id
|
_
->
out_of_scope
loc
"two argument bound by monad in pseudo-code mode"
in
(* e.g.: var%spec x = expr in cont *)
let
sexp
=
Printf
.
sprintf
"@[<hov 2>var%s%s %s%s%s = %s%s%s;@]@,%s"
"%%"
monad_name
token_start2
id
token_stop2
token_start1
sexp1
token_stop1
sbody
in
begin
match
dest
with
|
Dest_assign
_
->
apply_dest'
ctx
dest
(
ppf_lambda_wrap
sexp
)
|
Dest_ignore
->
sexp
|
Dest_return
->
(* do not display redundand return, but count it *)
let
(
token_start
,
token_stop
,
_token_loc
)
=
token_fresh
!
current_mode
loc
in
Printf
.
sprintf
"%s%s%s"
token_start
sexp
token_stop
|
Dest_inline
->
sexp
(* TODO: check if ok *)
end
end
else
begin
(* e.g.: if_spec(expr, (function(s, x) -> cont)) *)
let
sexp1_token
=
Printf
.
sprintf
"%s%s%s"
token_start1
sexp1
token_stop1
in
let
cont_token
=
Printf
.
sprintf
"function(%s%s%s) {@;<1 2>@[<v 0>%s@]@,}"
token_start2
(
String
.
concat
",@ "
arg_ids
)
token_stop2
sbody
in
let
sexp
=
ppf_apply
fname
(
String
.
concat
",@ "
[
sexp1_token
;
cont_token
])
in
apply_dest'
ctx
dest
sexp
end
|
Texp_apply
(
f
,
exp_l
)
->
|
Texp_apply
(
f
,
exp_l
)
->
(* first check not partial application *)
(* first check not partial application *)
...
@@ -848,10 +937,6 @@ and js_of_expression ctx dest e =
...
@@ -848,10 +937,6 @@ and js_of_expression ctx dest e =
in
in
if
is_result_arrow
then
out_of_scope
loc
"partial application"
;
if
is_result_arrow
then
out_of_scope
loc
"partial application"
;
let
sl'
=
exp_l
(* only used to know if infix *)
|>
List
.
map
(
fun
(
_
,
eo
,
_
)
->
match
eo
with
|
None
->
out_of_scope
loc
"optional apply arguments"
|
Some
ei
->
ei
)
in
let
sl_clean
=
exp_l
let
sl_clean
=
exp_l
|>
List
.
map
(
fun
(
_
,
eo
,
_
)
->
match
eo
with
|>
List
.
map
(
fun
(
_
,
eo
,
_
)
->
match
eo
with
|
None
->
out_of_scope
loc
"optional apply arguments"
|
None
->
out_of_scope
loc
"optional apply arguments"
...
@@ -877,7 +962,7 @@ and js_of_expression ctx dest e =
...
@@ -877,7 +962,7 @@ and js_of_expression ctx dest e =
let
stype
=
Str
.
global_replace
(
Str
.
regexp
"
\\
."
)
"_"
stype
in
let
stype
=
Str
.
global_replace
(
Str
.
regexp
"
\\
."
)
"_"
stype
in
ppf_apply
(
"_compare_"
^
stype
)
(
String
.
concat
",@ "
sl
)
ppf_apply
(
"_compare_"
^
stype
)
(
String
.
concat
",@ "
sl
)
end
end
end
else
if
is_infix
f
sl
'
&&
List
.
length
exp_l
=
2
then
begin
end
else
if
is_infix
f
sl
_clean
&&
List
.
length
exp_l
=
2
then
begin
ppf_apply_infix
se
(
List
.
hd
sl
)
(
List
.
hd
(
List
.
tl
sl
))
ppf_apply_infix
se
(
List
.
hd
sl
)
(
List
.
hd
(
List
.
tl
sl
))
end
else
begin
end
else
begin
ppf_apply
se
(
String
.
concat
",@ "
sl
)
ppf_apply
se
(
String
.
concat
",@ "
sl
)
...
...
This diff is collapsed.
Click to expand it.
generator/tests/jsref/JsInterpreter.ml
+
61
−
38
View file @
747387a3
...
@@ -2422,31 +2422,30 @@ and run_binary_op_arith mathop s c v1 v2 =
...
@@ -2422,31 +2422,30 @@ and run_binary_op_arith mathop s c v1 v2 =
res_out
(
Coq_out_ter
(
s1
,
(
res_val
(
Coq_value_prim
(
Coq_prim_number
(
mathop
n1
n2
))))))
res_out
(
Coq_out_ter
(
s1
,
(
res_val
(
Coq_value_prim
(
Coq_prim_number
(
mathop
n1
n2
))))))
and
run_binary_op_shift
b_unsigned
mathop
s
c
v1
v2
=
and
run_binary_op_shift
b_unsigned
mathop
s
c
v1
v2
=
let
%
run
(
s1
,
k1
)
=
((
if
b_unsigned
then
to_uint32
else
to_int32
)
s
c
v1
)
in
let
conv
=
(
if
b_unsigned
then
to_uint32
else
to_int32
)
in
let
%
run
(
s2
,
k2
)
=
(
to_uint32
s1
c
v2
)
in
let
%
run
(
s1
,
k1
)
=
(
conv
s
c
v1
)
in
let
k2_2
=
JsNumber
.
modulo_32
k2
in
let
%
run
(
s2
,
k2
)
=
(
to_uint32
s1
c
v2
)
in
res_ter
s2
(
res_val
(
Coq_value_prim
(
Coq_prim_number
(
mathop
k1
k2_2
))))
let
k2_2
=
JsNumber
.
modulo_32
k2
in
res_ter
s2
(
res_val
(
Coq_value_prim
(
Coq_prim_number
(
mathop
k1
k2_2
))))
and
run_binary_op_bitwise
mathop
s
c
v1
v2
=
and
run_binary_op_bitwise
mathop
s
c
v1
v2
=
let
%
run
(
s1
,
k1
)
=
(
to_int32
s
c
v1
)
in
let
%
run
(
s1
,
k1
)
=
(
to_int32
s
c
v1
)
in
let
%
run
(
s2
,
k2
)
=
(
to_int32
s1
c
v2
)
in
let
%
run
(
s2
,
k2
)
=
(
to_int32
s1
c
v2
)
in
res_ter
s2
(
res_val
(
Coq_value_prim
(
Coq_prim_number
(
mathop
k1
k2
))))
res_ter
s2
(
res_val
(
Coq_value_prim
(
Coq_prim_number
(
mathop
k1
k2
))))
and
run_binary_op_compare
b_swap
b_neg
s
c
v1
v2
=
and
run_binary_op_compare
b_swap
b_neg
s
c
v1
v2
=
let
%
run
(
s1
,
ww
)
=
convert_twice_primitive
s
c
v1
v2
in
let
%
run
(
s1
,
ww
)
=
convert_twice_primitive
s
c
v1
v2
in
let
(
w1
,
w2
)
=
ww
in
let
(
w1
,
w2
)
=
ww
in
let
p
=
if
b_swap
then
(
w2
,
w1
)
else
(
w1
,
w2
)
in
let
p
=
if
b_swap
then
(
w2
,
w1
)
else
(
w1
,
w2
)
in
let
(
wa
,
wb
)
=
p
in
let
(
wa
,
wb
)
=
p
in
let
wr
=
inequality_test_primitive
wa
wb
in
let
wr
=
inequality_test_primitive
wa
wb
in
let
v
=
if
prim_compare
wr
Coq_prim_undef
if
prim_compare
wr
Coq_prim_undef
then
res_out
(
Coq_out_ter
(
s1
,
res_val
(
Coq_value_prim
(
Coq_prim_bool
false
))))
then
res_val
(
Coq_value_prim
(
Coq_prim_bool
false
))
else
if
(
b_neg
)
&&
(
prim_compare
wr
(
Coq_prim_bool
true
))
else
if
(
b_neg
)
&&
(
prim_compare
wr
(
Coq_prim_bool
true
))
then
res_out
(
Coq_out_ter
(
s1
,
res_val
(
Coq_value_prim
(
Coq_prim_bool
false
))))
then
res_val
(
Coq_value_prim
(
Coq_prim_bool
false
))
else
if
(
b_neg
)
&&
(
prim_compare
wr
(
Coq_prim_bool
false
))
else
if
(
b_neg
)
&&
(
prim_compare
wr
(
Coq_prim_bool
false
))
then
res_out
(
Coq_out_ter
(
s1
,
res_val
(
Coq_value_prim
(
Coq_prim_bool
true
))))
then
res_val
(
Coq_value_prim
(
Coq_prim_bool
true
))
else
res_out
(
Coq_out_ter
(
s1
,
res_val
(
Coq_value_prim
wr
)))
else
res_val
(
Coq_value_prim
wr
)
in
res_out
(
Coq_out_ter
(
s1
,
v
))
and
run_binary_op_instanceof
s
c
v1
v2
=
and
run_binary_op_instanceof
s
c
v1
v2
=
match
v2
with
match
v2
with
...
@@ -2496,8 +2495,8 @@ and run_binary_op s c op v1 v2 =
...
@@ -2496,8 +2495,8 @@ and run_binary_op s c op v1 v2 =
|
Coq_binary_op_strict_disequal
->
|
Coq_binary_op_strict_disequal
->
result_out
(
Coq_out_ter
(
s
,
(
res_val
(
Coq_value_prim
(
Coq_prim_bool
(
not
(
strict_equality_test
v1
v2
)))))))
result_out
(
Coq_out_ter
(
s
,
(
res_val
(
Coq_value_prim
(
Coq_prim_bool
(
not
(
strict_equality_test
v1
v2
)))))))
|
Coq_binary_op_coma
->
result_out
(
Coq_out_ter
(
s
,
(
res_val
v2
)))
|
Coq_binary_op_coma
->
result_out
(
Coq_out_ter
(
s
,
(
res_val
v2
)))
|
Coq_binary_op_and
->
assert
fals
e
|
Coq_binary_op_and
->
Coq_result_impossibl
e
|
Coq_binary_op_or
->
assert
fals
e
|
Coq_binary_op_or
->
Coq_result_impossibl
e
(** val run_prepost_op : unary_op -> ((number -> number) * bool) option **)
(** val run_prepost_op : unary_op -> ((number -> number) * bool) option **)
...
@@ -3144,23 +3143,47 @@ and run_stat_switch_with_default_A s c found vi rv scs1 ts0 scs2 =
...
@@ -3144,23 +3143,47 @@ and run_stat_switch_with_default_A s c found vi rv scs1 ts0 scs2 =
state -> execution_ctx -> label_set -> expr -> switchbody ->
state -> execution_ctx -> label_set -> expr -> switchbody ->
result **)
result **)
(* ALTERNATIVE VERSION, WITH LESS FACTORIZATION
and run_stat_switch s c labs e sb =
and run_stat_switch s c labs e sb =
let%run (s1, vi) = run_expr_get_value s c e in
let%run (s1, vi) = run_expr_get_value s c e in
let
follow
=
(
fun
w
->
match sb with
let
%
success
(
s0
,
r
)
=
| Coq_switchbody_nodefault scs ->
let
%
break
(
s2
,
r
)
=
w
in
let%success (s0, r) = begin
if
res_label_in
r
labs
let%break (s2, r) =
then
result_out
(
Coq_out_ter
(
s2
,
(
res_normal
r
.
res_value
)))
run_stat_switch_no_default s1 c vi
else
result_out
(
Coq_out_ter
(
s2
,
r
))
in
Coq_resvalue_empty scs in
res_ter
s0
(
res_normal
r
))
in
if res_label_in r labs
match
sb
with
then result_out (Coq_out_ter (s2, (res_normal r.res_value)))
|
Coq_switchbody_nodefault
scs
->
else result_out (Coq_out_ter (s2, r))
follow
end in
(
run_stat_switch_no_default
s1
c
vi
Coq_resvalue_empty
scs
)
res_ter s0 (res_normal r)
|
Coq_switchbody_withdefault
(
scs1
,
ts
,
scs2
)
->
| Coq_switchbody_withdefault (scs1, ts, scs2) ->
follow
let%success (s0, r) = begin
(
run_stat_switch_with_default_A
s1
c
false
vi
let%break (s2, r) =
Coq_resvalue_empty
scs1
ts
scs2
)
run_stat_switch_with_default_A s1 c false vi
Coq_resvalue_empty scs1 ts scs2 in
if res_label_in r labs
then result_out (Coq_out_ter (s2, (res_normal r.res_value)))
else result_out (Coq_out_ter (s2, r)) end in
res_ter s0 (res_normal r)
*)
and
run_stat_switch
s
c
labs
e
sb
=
let
%
run
(
s1
,
vi
)
=
run_expr_get_value
s
c
e
in
let
follow
=
(
fun
w
->
let
%
success
(
s0
,
r
)
=
let
%
break
(
s2
,
r
)
=
w
in
if
res_label_in
r
labs
then
result_out
(
Coq_out_ter
(
s2
,
(
res_normal
r
.
res_value
)))
else
result_out
(
Coq_out_ter
(
s2
,
r
))
in
res_ter
s0
(
res_normal
r
))
in
match
sb
with
|
Coq_switchbody_nodefault
scs
->
follow
(
run_stat_switch_no_default
s1
c
vi
Coq_resvalue_empty
scs
)
|
Coq_switchbody_withdefault
(
scs1
,
ts
,
scs2
)
->
follow
(
run_stat_switch_with_default_A
s1
c
false
vi
Coq_resvalue_empty
scs1
ts
scs2
)
(** val run_stat_do_while :
(** val run_stat_do_while :
state -> execution_ctx -> resvalue -> label_set -> expr ->
state -> execution_ctx -> resvalue -> label_set -> expr ->
...
...
This diff is collapsed.
Click to expand it.
Preview
0%
Loading
Try again
or
attach a new file
.
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Save comment
Cancel
Please
register
or
sign in
to comment