From 889c68bd903b5201d659c963afc09482f33ba5b0 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <jahier@imag.fr>
Date: Fri, 22 Mar 2013 08:40:05 +0100
Subject: [PATCH] The -exec mode now supports enums.
---
src/lic2soc.ml | 2 +-
src/socExecEvalPredef.ml | 20 +++++++-------------
src/socExecValue.ml | 22 ++++++++++++++++------
src/socExecValue.mli | 4 ++--
src/socPredef.ml | 21 ++++++++-------------
src/socUtils.ml | 2 +-
6 files changed, 35 insertions(+), 36 deletions(-)
diff --git a/src/lic2soc.ml b/src/lic2soc.ml
index 0252c7cf..b8024c5a 100644
--- a/src/lic2soc.ml
+++ b/src/lic2soc.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 21/03/2013 (at 09:56) by Erwan Jahier> *)
+(** Time-stamp: <modified the 21/03/2013 (at 16:47) by Erwan Jahier> *)
open Lxm
open Lic
diff --git a/src/socExecEvalPredef.ml b/src/socExecEvalPredef.ml
index da5a1785..0bcab4ea 100644
--- a/src/socExecEvalPredef.ml
+++ b/src/socExecEvalPredef.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 21/03/2013 (at 11:34) by Erwan Jahier> *)
+(* Time-stamp: <modified the 21/03/2013 (at 17:04) by Erwan Jahier> *)
open SocExecValue
open Soc
@@ -61,10 +61,8 @@ let lustre_mod ctx =
let lustre_eq ctx =
let (vn,vv) =
match ([get_val "x" ctx; get_val "y" ctx]) with
- | [I x1; I x2] -> "z"::ctx.cpath,B(x1 = x2)
- | [F x1; F x2] -> "z"::ctx.cpath,B(x1 = x2)
- | [B x1; B x2] -> "z"::ctx.cpath,B(x1 = x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U
+ | [x1; x2] -> "z"::ctx.cpath,B(x1 = x2)
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
@@ -112,9 +110,8 @@ let lustre_not ctx =
let lustre_lt ctx =
let (vn,vv) =
match ([get_val "x" ctx; get_val "y" ctx]) with
- | [I x1; I x2] -> "z"::ctx.cpath,B(x1 < x2)
- | [F x1; F x2] -> "z"::ctx.cpath,B(x1 < x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U
+ | [x1; x2] -> "z"::ctx.cpath,B(x1 < x2)
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
@@ -122,9 +119,8 @@ let lustre_lt ctx =
let lustre_gt ctx =
let (vn,vv) =
match ([get_val "x" ctx; get_val "y" ctx]) with
- | [I x1; I x2] -> "z"::ctx.cpath,B(x1 > x2)
- | [F x1; F x2] -> "z"::ctx.cpath,B(x1 > x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U
+ | [x1; x2] -> "z"::ctx.cpath,B(x1 > x2)
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
@@ -132,9 +128,8 @@ let lustre_gt ctx =
let lustre_lte ctx =
let (vn,vv) =
match ([get_val "x" ctx; get_val "y" ctx]) with
- | [I x1; I x2] -> "z"::ctx.cpath,B(x1 <= x2)
- | [F x1; F x2] -> "z"::ctx.cpath,B(x1 <= x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U
+ | [x1; x2] -> "z"::ctx.cpath,B(x1 <= x2)
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
@@ -142,9 +137,8 @@ let lustre_lte ctx =
let lustre_gte ctx =
let (vn,vv) =
match ([get_val "x" ctx; get_val "y" ctx]) with
- | [I x1; I x2] -> "z"::ctx.cpath,B(x1 >= x2)
- | [F x1; F x2] -> "z"::ctx.cpath,B(x1 >= x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U
+ | [x1; x2] -> "z"::ctx.cpath,B(x1 >= x2)
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
@@ -162,8 +156,8 @@ let lustre_and ctx =
let lustre_neq ctx =
let (vn,vv) =
match ([get_val "x" ctx; get_val "y" ctx]) with
- | [B x1; B x2] -> "z"::ctx.cpath,B(x1 <> x2)
| [U; _] | [_;U] -> "z"::ctx.cpath,U
+ | [x1; x2] -> "z"::ctx.cpath,B(x1 <> x2)
| _ -> assert false
in
{ ctx with s = sadd ctx.s vn vv }
diff --git a/src/socExecValue.ml b/src/socExecValue.ml
index e1292af7..80e45acb 100644
--- a/src/socExecValue.ml
+++ b/src/socExecValue.ml
@@ -1,8 +1,8 @@
-(* Time-stamp: <modified the 21/03/2013 (at 11:22) by Erwan Jahier> *)
+(* Time-stamp: <modified the 22/03/2013 (at 08:35) by Erwan Jahier> *)
open Soc
-type t = I of int | F of float | B of bool | E of Soc.ident
+type t = I of int | F of float | B of bool | E of Soc.ident * int
| A of t array | S of (Soc.ident * t) list | U
(* Meant to represent paths in the call tree. Actually it both
@@ -173,7 +173,7 @@ let rec (to_string : t -> string) =
| F f -> string_of_float f
| B true -> "t"
| B false -> "f"
- | E e -> e
+ | E (e,_) -> e
| S fl -> String.concat " " (List.map (fun (fn,fv) -> to_string fv) fl)
| A a ->
let str = ref "" in
@@ -221,13 +221,22 @@ let rec (read_enum : ident list -> ident) =
let str = read_line () in
if List.mem str idl then str else (print_string "Bad enum; "; read_enum idl)
+let rec pos_in_list i x l =
+ match l with
+ | e::l -> if e=x then i else pos_in_list (i+1) x l
+ | [] -> assert false (* should not occur *)
+
+
let (read_value : var -> t) =
fun (_,t) ->
match t with
| Bool -> print_string "Enter a bool (t/f):";flush stdout; B(read_line () = "t")
| Int -> print_string "Enter an int:"; flush stdout; I(read_int())
| Real -> print_string "Enter a float:"; flush stdout; F(read_float())
- | Enum(_,idl) -> E(read_enum(idl))
+ | Enum(_,idl) ->
+ let e = read_enum(idl) in
+ let i = pos_in_list 0 e idl in
+ E(e,i)
| _ -> assert false (* finish me! *)
(* let (get_val : ident -> ctx -> t) = *)
@@ -261,7 +270,7 @@ let (get_val : ident -> ctx -> t) =
let (get_enum : ident -> ctx -> ident) =
fun id ctx ->
match get_val id ctx with
- | E e -> e
+ | E(e,_) -> e
| _ -> assert false (* should not fail *)
let rec (get_value : ctx -> var_expr -> t) =
@@ -271,7 +280,8 @@ let rec (get_value : ctx -> var_expr -> t) =
| Const("true",Bool) -> B true
| Const("false",Bool) -> B false
| Const(id_in,Int) -> I (int_of_string id_in)
- | Const(id_in,Real) -> F (float_of_string id_in)
+ | Const(id_in,Real) -> F (float_of_string id_in)
+ | Const(id,Enum(_,idl)) -> E(id, pos_in_list 0 id idl)
| Const(id,_) -> assert false (* finish me! *)
| Field(ve,fn,t) ->
let s = get_value ctx ve in
diff --git a/src/socExecValue.mli b/src/socExecValue.mli
index 14b8c38f..5f5da7ac 100644
--- a/src/socExecValue.mli
+++ b/src/socExecValue.mli
@@ -1,8 +1,8 @@
-(* Time-stamp: <modified the 20/03/2013 (at 18:36) by Erwan Jahier> *)
+(* Time-stamp: <modified the 22/03/2013 (at 08:35) by Erwan Jahier> *)
(** Manipulating data in the Soc interpreter *)
-type t = | I of int | F of float | B of bool | E of Soc.ident
+type t = | I of int | F of float | B of bool | E of Soc.ident * int
| A of t array
| S of (Soc.ident * t) list
| U (* to set uninitialized mem *)
diff --git a/src/socPredef.ml b/src/socPredef.ml
index b5df28ff..77cc3664 100644
--- a/src/socPredef.ml
+++ b/src/socPredef.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 21/03/2013 (at 10:48) by Erwan Jahier> *)
+(* Time-stamp: <modified the 21/03/2013 (at 17:06) by Erwan Jahier> *)
(** Synchronous Object Code for Predefined operators. *)
@@ -15,6 +15,7 @@ let r = Soc.Real
let aa t1 t2 = ["x", t1], ["z", t2]
let aaa t1 t2 t3 = ["x", t1; "y",t2], ["z", t3]
+let aab t1 t2 = ["x", t1; "y",t2], ["z", Bool]
(* if/then/else *)
let baaa t = ["c", b; "xt", t; "xe", t], ["z", t]
@@ -410,22 +411,16 @@ let soc_interface_of_predef:
| AstPredef.IUMINUS_n, [Int] -> of_soc_key (("Lustre::uminus"), types@[Int], None)
| AstPredef.UMINUS_n, [Real] -> of_soc_key (("Lustre::uminus"), types@[Real], None)
| AstPredef.RUMINUS_n, [Real] -> of_soc_key (("Lustre::uminus"), types@[Real], None)
- | AstPredef.LT_n, [Int; Int] -> of_soc_key (("Lustre::lt"), types@[Int], None)
- | AstPredef.LT_n, [Real; Real] -> of_soc_key (("Lustre::lt"), types@[Real], None)
- | AstPredef.GT_n, [Int; Int] -> of_soc_key (("Lustre::gt"), types@[Int], None)
- | AstPredef.GT_n, [Real; Real] -> of_soc_key (("Lustre::gt"), types@[Real], None)
- | AstPredef.LTE_n, [Int; Int] -> of_soc_key (("Lustre::lte"), types@[Int], None)
- | AstPredef.LTE_n, [Real; Real] -> of_soc_key (("Lustre::lte"), types@[Real], None)
- | AstPredef.GTE_n, [Int; Int] -> of_soc_key (("Lustre::gte"), types@[Int], None)
- | AstPredef.GTE_n, [Real; Real] -> of_soc_key (("Lustre::gte"), types@[Real], None)
+ | AstPredef.LT_n, [_; _] -> of_soc_key (("Lustre::lt"), types@[Bool], None)
+ | AstPredef.GT_n, [_; _] -> of_soc_key (("Lustre::gt"), types@[Bool], None)
+ | AstPredef.LTE_n, [_; _] -> of_soc_key (("Lustre::lte"), types@[Bool], None)
+ | AstPredef.GTE_n, [_; _] -> of_soc_key (("Lustre::gte"), types@[Bool], None)
| AstPredef.AND_n, [Bool; Bool] -> of_soc_key (("Lustre::and"), types@[Bool], None)
| AstPredef.OR_n, [Bool; Bool] -> of_soc_key (("Lustre::or"), types@[Bool], None)
| AstPredef.XOR_n, [Bool; Bool] -> of_soc_key (("Lustre::xor"), types@[Bool], None)
| AstPredef.IMPL_n, [Bool; Bool] -> of_soc_key (("Lustre::impl"), types@[Bool], None)
- | AstPredef.EQ_n, [Bool; Bool] -> of_soc_key (("Lustre::eq"), types@[Bool], None)
- | AstPredef.EQ_n, [Int; Int] -> of_soc_key (("Lustre::eq"), types@[Int], None)
- | AstPredef.EQ_n, [Real; Real] -> of_soc_key (("Lustre::eq"), types@[Real], None)
- | AstPredef.NEQ_n, [Bool; Bool] -> of_soc_key (("Lustre::neq"), types@[Bool], None)
+ | AstPredef.EQ_n , [_; _] -> of_soc_key (("Lustre::eq"), types@[Bool], None)
+ | AstPredef.NEQ_n, [_; _] -> of_soc_key (("Lustre::neq"), types@[Bool], None)
| AstPredef.NOT_n, [Bool] -> of_soc_key (("Lustre::not"), types@[Bool], None)
| AstPredef.TRUE_n, [] -> finish_me lxm ; assert false (* todo *)
diff --git a/src/socUtils.ml b/src/socUtils.ml
index 952af1bd..5336267f 100644
--- a/src/socUtils.ml
+++ b/src/socUtils.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 21/03/2013 (at 09:55) by Erwan Jahier> *)
+(** Time-stamp: <modified the 21/03/2013 (at 17:51) by Erwan Jahier> *)
open Soc
--
GitLab