Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
verimag
synchrone
lutin
Commits
33183a6a
Commit
33183a6a
authored
Dec 08, 2010
by
Erwan Jahier
Browse files
Merge /home/raymond/git/lurette
parents
a9dff877
3a2d6f89
Changes
5
Hide whitespace changes
Inline
Side-by-side
examples/lutin/external_code/extern.lut
View file @
33183a6a
...
...
@@ -7,13 +7,14 @@ extern pi(): real
extern
rand_up_to
(
min
,
max
:
int
)
:
int
node
main
(
deg
:
real
-- deg: real
dummy
:
bool
;
)
returns
(
a
:
real
;
s
:
real
a
:
real
;
s
:
real
)
=
let
a1
=
((
deg
*
pi
())
/
180
.
0
)
in
exist
deg
:
real
[
0
.
0
;
360
.
0
]
=
0
.
0
in
let
a1
=
(((
pre
deg
)
*
pi
())
/
180
.
0
)
in
loop
{
(
a
=
a1
)
and
(
s
=
sin
(
a1
))
(
a
=
a1
)
and
(
s
=
sin
(
a1
))
}
source/Lutin/autoExplore.ml
View file @
33183a6a
...
...
@@ -215,6 +215,25 @@ Mode simu, gestion en dur :
- des compteurs de boucles
*)
let
rec
substitute_pre
pctx
ae
=
(
match
ae
.
ae_val
with
|
AE_pre
id
->
(
match
CoTraceExp
.
get_pre_ctx
pctx
id
with
|
Some
e
->
e
|
None
->
ae
)
|
AE_call
(
f
,
args
)
->
(
let
n
=
AE_call
(
f
,
List
.
map
(
substitute_pre
pctx
)
args
)
in
{
ae_type
=
ae
.
ae_type
;
ae_ctrl
=
ae
.
ae_ctrl
;
ae_val
=
n
}
)
|
AE_external_call
(
f
,
exti
,
prof
,
args
)
->
(
let
n
=
AE_external_call
(
f
,
exti
,
prof
,
List
.
map
(
substitute_pre
pctx
)
args
)
in
{
ae_type
=
ae
.
ae_type
;
ae_ctrl
=
ae
.
ae_ctrl
;
ae_val
=
n
}
)
|
other
->
ae
)
let
gentrans
(
xenv
:
Expand
.
t
)
(* le résultat de l'expansion *)
(
x
:
CoTraceExp
.
t
)
(* la trace à traiter *)
...
...
@@ -382,13 +401,14 @@ let gentrans
)
in
rec_gentrans
te
rec_goto_cb
vanish_cb
raise_cb
)
(**
Entry
On appèle avec un nouveau goto callback
:
goto(cl,n) -> goto(a::cl,n)
(**
init_pre
pre substitution is made HERE,
MAYBE not a good idea ???
*)
|
TE_init_
then
(
a
,
b
,
te
)
->
(
|
TE_init_
pre
(
pctx
,
te
)
->
(
let
rec_goto_cb
(
cl
,
n
)
=
(
goto_cb
(
a
::
cl
,
TE_assert
(
b
,
n
))
let
cl'
=
List
.
map
(
substitute_pre
pctx
)
cl
in
goto_cb
(
cl'
,
n
)
)
in
rec_gentrans
te
rec_goto_cb
vanish_cb
raise_cb
)
...
...
source/Lutin/coTraceExp.ml
View file @
33183a6a
...
...
@@ -36,6 +36,19 @@ let nb_loops () = !loop_cpt_number
(* type loop_weighter = int -> (int, int) *)
(* pre context for local variable scope :
list of (id * CoAlgExp.t)
WARNING : maybe use a table/set later ???
*)
type
pre_ctx
=
(
CoIdent
.
t
*
CoAlgExp
.
t
)
list
let
add_pre_ctx
pctx
(
i
,
v
)
=
(
i
,
v
)
::
pctx
let
new_pre_ctx
()
=
[]
let
get_pre_ctx
pctx
id
=
(
try
Some
(
List
.
assoc
id
pctx
)
with
Not_found
->
None
)
type
t
=
TE_eps
|
TE_ref
of
CoIdent
.
t
...
...
@@ -49,11 +62,8 @@ type t =
|
TE_loopi
of
int
*
CoAlgExp
.
t
*
CoAlgExp
.
t
*
t
|
TE_loopa
of
int
*
CoAlgExp
.
t
*
CoAlgExp
.
t
option
*
t
|
TE_assert
of
CoAlgExp
.
t
*
t
(* Takes two constraints:
- one for the first reaction
- one for all others
*)
|
TE_init_then
of
CoAlgExp
.
t
*
CoAlgExp
.
t
*
t
(* Takes a list (id,val) *)
|
TE_init_pre
of
pre_ctx
*
t
|
TE_raise
of
string
|
TE_try
of
t
*
t
option
|
TE_catch
of
string
*
t
*
t
option
...
...
@@ -73,7 +83,7 @@ let of_loopa moy ect e = (TE_loopa (new_loop_cpt (), moy,ect,e))
let
of_assert
c
e
=
(
TE_assert
(
c
,
e
))
let
of_init_
then
cinit
cother
e
=
(
TE_init_then
(
cinit
,
cother
,
e
))
let
of_init_
pre
pctx
e
=
(
TE_init_pre
(
pctx
,
e
))
let
of_raise
s
=
(
TE_raise
s
)
...
...
@@ -147,11 +157,16 @@ let rec _dump (pr: string -> unit) te = (
pr
" in "
;
_dump
pr
e
;
)
|
TE_init_
then
(
a
,
b
,
e
)
->
(
|
TE_init_
pre
(
pctx
,
e
)
->
(
pr
"init "
;
pr
(
CoAlgExp
.
lus_dumps
a
)
;
pr
" then "
;
pr
(
CoAlgExp
.
lus_dumps
b
)
;
let
pp
(
i
,
v
)
=
(
pr
"pre "
;
pr
(
CoIdent
.
to_string
i
);
pr
" = "
;
pr
(
CoAlgExp
.
lus_dumps
v
)
;
pr
";"
)
in
List
.
iter
pp
pctx
;
pr
" in "
;
_dump
pr
e
;
)
...
...
source/Lutin/coTraceExp.mli
View file @
33183a6a
...
...
@@ -17,6 +17,12 @@ N.B. les exceptions sont enti
(** On exporte la structure du type *)
type
pre_ctx
=
(
CoIdent
.
t
*
CoAlgExp
.
t
)
list
val
new_pre_ctx
:
unit
->
pre_ctx
val
add_pre_ctx
:
pre_ctx
->
(
CoIdent
.
t
*
CoAlgExp
.
t
)
->
pre_ctx
val
get_pre_ctx
:
pre_ctx
->
CoIdent
.
t
->
CoAlgExp
.
t
option
type
t
=
|
TE_eps
|
TE_ref
of
CoIdent
.
t
...
...
@@ -29,7 +35,7 @@ type t =
|
TE_loopi
of
int
*
CoAlgExp
.
t
*
CoAlgExp
.
t
*
t
|
TE_loopa
of
int
*
CoAlgExp
.
t
*
CoAlgExp
.
t
option
*
t
|
TE_assert
of
CoAlgExp
.
t
*
t
|
TE_init_
then
of
CoAlgExp
.
t
*
CoAlgExp
.
t
*
t
|
TE_init_
pre
of
pre_ctx
*
t
|
TE_raise
of
string
|
TE_try
of
t
*
t
option
|
TE_catch
of
string
*
t
*
t
option
...
...
@@ -66,7 +72,7 @@ val of_choice : (t * CoAlgExp.t option ) list -> t
val
of_assert
:
CoAlgExp
.
t
->
t
->
t
val
of_init_
then
:
CoAlgExp
.
t
->
CoAlgExp
.
t
->
t
->
t
val
of_init_
pre
:
pre_ctx
->
t
->
t
val
of_raise
:
string
->
t
...
...
source/Lutin/expand.ml
View file @
33183a6a
...
...
@@ -90,37 +90,29 @@ and support_info = {
(**************************************************************
LOCAL SCOPE HANDLING (see EXIST_n)
---------------------------------------------------------------
A scope contains mainly 2 constraints :
- the (re)init constraint
- the other constraint
For each variable X declared with an init value V :
- an extra var PX is created
- the constraint "PX = V" is added to init
- the constraint "PX = pre X" is added to other
N.B. init and other are filled by new_pre_handler
A scope contains a pre (re)init context
**************************************************************)
and
support_scope
=
{
sco_src
:
CoIdent
.
src_stack
;
mutable
sco_init
_other
:
(
Co
AlgExp
.
t
*
CoAlgExp
.
t
)
option
;
mutable
sco_init
:
Co
TraceExp
.
pre_ctx
option
;
}
let
new_support_scope
(
src
:
CoIdent
.
src_stack
)
=
(
let
res
=
{
sco_src
=
src
;
(* made on demand *)
sco_init
_other
=
None
;
sco_init
=
None
;
}
in
res
)
let
add_support_scope_constraint
scope
i
nitc
otherc
=
(
scope
.
sco_init_other
<-
Some
(
match
scope
.
sco_init_other
with
|
None
->
(
initc
,
otherc
)
|
Some
(
i
,
o
)
->
(
CoAlgExp
.
of_and
initc
i
,
CoAlgExp
.
of_and
otherc
o
)
)
let
add_support_scope_constraint
scope
i
d
va
=
(
let
oldp
=
match
scope
.
sco_init
with
|
None
->
CoTraceExp
.
new_pre_ctx
()
|
Some
p
->
p
in
scope
.
sco_init
<-
Some
(
CoTraceExp
.
add_pre_ctx
oldp
(
id
,
va
)
)
)
...
...
@@ -494,6 +486,18 @@ let new_pre_handler
(
id
:
CoIdent
.
t
)
(
id_info
:
support_info
)
=
(
let
te
=
id_info
.
si_type
in
let
pre_X
=
CoAlgExp
.
of_pre
id
te
in
(* Reinitializable LOCAL var ? *)
let
_
=
match
(
id_info
.
si_scope
,
id_info
.
si_init
)
with
|
(
Some
scope
,
Some
init
)
->
(
add_support_scope_constraint
scope
id
init
)
|
(
_
,_
)
->
(
(* NO: nothing to do ... *)
)
in
pre_X
(*
(* var preX inherit type and has no source *)
let preid = CoIdent.get ("pre"^(CoIdent.to_string id)) in
let te = id_info.si_type in
...
...
@@ -505,7 +509,8 @@ let new_pre_handler
let ze_right_ref = match (id_info.si_scope, id_info.si_init) with
| (Some scope, Some init) -> (
(* YES: NEW SUPPORT VAR, NEW scope CONSTRAINTS *)
let
eref
=
CoAlgExp
.
of_support
preid
te
true
in
(* let eref = CoAlgExp.of_support preid te true in *)
let eref = CoAlgExp.of_support preid te false in
Hashtbl.add _support_tab preid {
si_nature = Local;
si_type = te;
...
...
@@ -538,6 +543,7 @@ let new_pre_handler
eref
) in
ze_right_ref
*)
)
let
alg_exp_of_support_pre_ref
tgtid
=
(
...
...
@@ -808,6 +814,7 @@ and treat_exp_call
(* non contrôlable ? *)
let
check_unctl
esrc
eexp
=
(
if
(
CoAlgExp
.
is_controlable
eexp
)
then
(
Verbose
.
exe
~
level
:
3
(
fun
()
->
CoAlgExp
.
dumpf
stderr
eexp
);
raise
(
Compile_error
(
esrc
.
src
,
"extern. func. arguments must be uncontrollable"
))
)
else
()
...
...
@@ -1206,9 +1213,9 @@ and
(* on continu dans ce nouvel env ... *)
let
res
=
treat_trace
env
sstack
ee
in
(* un reinit a-il été associé au scope lors du traitement des id ? *)
match
zescope
.
sco_init
_other
with
match
zescope
.
sco_init
with
|
None
->
res
|
Some
(
i
,
o
)
->
CoTraceExp
.
of_init_
then
i
o
res
|
Some
p
->
CoTraceExp
.
of_init_
pre
p
res
)
(* traces *)
|
FBY_n
(
e1
,
e2
)
->
(
...
...
Write
Preview
Supports
Markdown
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