From 6cbbe1c1e907935bdc57190d3f610b88c5ccefc8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lelio.brun@isae-supaero.fr>
Date: Thu, 3 Jun 2021 16:44:53 +0200
Subject: [PATCH] start again with spec representation
---
include/arrow.h | 2 +-
src/clock_calculus.ml | 74 ++++++++++++------------
src/clocks.ml | 9 ++-
src/corelang.ml | 8 ++-
src/machine_code.ml | 99 ++++++++++++++++++++-----------
src/machine_code_common.ml | 115 +++++++++++++++++++++----------------
src/machine_code_types.ml | 4 +-
src/spec_types.ml | 2 +-
src/types.ml | 2 +-
src/typing.ml | 70 +++++++++++-----------
10 files changed, 219 insertions(+), 166 deletions(-)
diff --git a/include/arrow.h b/include/arrow.h
index 802057da..d2956d8b 100644
--- a/include/arrow.h
+++ b/include/arrow.h
@@ -23,7 +23,7 @@ extern void _arrow_dealloc (struct _arrow_mem *);
#define _arrow_clear(self) {}
-#define _arrow_step(x,y,output,self) ((self)->_reg._first?((self)->_reg._first=0,(*output = x)):(*output = y))
+/* #define _arrow_step(x,y,output,self) ((self)->_reg._first?((self)->_reg._first=0,(*output = x)):(*output = y)) */
#define _arrow_reset(self) {(self)->_reg._first = 1;}
diff --git a/src/clock_calculus.ml b/src/clock_calculus.ml
index 0913fbc0..0be47af0 100644
--- a/src/clock_calculus.ml
+++ b/src/clock_calculus.ml
@@ -49,37 +49,38 @@ let rec generalize_carrier cr =
match cr.carrier_desc with
| Carry_const _
| Carry_name ->
- if cr.carrier_scoped then
- raise (Scope_carrier cr);
- cr.carrier_desc <- Carry_var
+ if cr.carrier_scoped then
+ raise (Scope_carrier cr);
+ cr.carrier_desc <- Carry_var
| Carry_var -> ()
| Carry_link cr' -> generalize_carrier cr'
(** Promote monomorphic clock variables to polymorphic clock variables. *)
(* Generalize by side-effects *)
let rec generalize ck =
- match ck.cdesc with
- | Carrow (ck1,ck2) ->
- generalize ck1; generalize ck2
- | Ctuple clist ->
- List.iter generalize clist
- | Con (ck',cr,_) -> generalize ck'; generalize_carrier cr
- | Cvar ->
- if ck.cscoped then
- raise (Scope_clock ck);
- ck.cdesc <- Cunivar
- | Cunivar -> ()
- | Clink ck' ->
- generalize ck'
- | Ccarrying (cr,ck') ->
- generalize_carrier cr; generalize ck'
+ match ck.cdesc with
+ | Carrow (ck1,ck2) ->
+ generalize ck1; generalize ck2
+ | Ctuple clist ->
+ List.iter generalize clist
+ | Con (ck',cr,_) -> generalize ck'; generalize_carrier cr
+ | Cvar ->
+ if ck.cscoped then
+ raise (Scope_clock ck);
+ ck.cdesc <- Cunivar
+ | Cunivar -> ()
+ | Clink ck' ->
+ generalize ck'
+ | Ccarrying (cr,ck') ->
+ generalize_carrier cr; generalize ck'
let try_generalize ck_node loc =
try
generalize ck_node
- with (Scope_carrier cr) ->
+ with
+ | Scope_carrier cr ->
raise (Error (loc, Carrier_extrusion (ck_node, cr)))
- | (Scope_clock ck) ->
+ | Scope_clock ck ->
raise (Error (loc, Clock_extrusion (ck_node, ck)))
(* Clocks instanciation *)
@@ -414,20 +415,20 @@ let unify_imported_clock ref_ck_opt ck loc =
let rec aux ck =
match (repr ck).cdesc with
| Cvar ->
- begin
- match !ck_var with
- | None ->
- ck_var:=Some ck
- | Some v ->
- (* cannot fail *)
- try_unify ck v loc
- end
+ begin
+ match !ck_var with
+ | None ->
+ ck_var := Some ck
+ | Some v ->
+ (* cannot fail *)
+ try_unify ck v loc
+ end
| Ctuple cl ->
- List.iter aux cl
+ List.iter aux cl
| Carrow (ck1,ck2) ->
- aux ck1; aux ck2
+ aux ck1; aux ck2
| Ccarrying (_, ck1) ->
- aux ck1
+ aux ck1
| Con (ck1, _, _) -> aux ck1
| _ -> ()
in
@@ -611,7 +612,8 @@ let clock_of_vlist vars =
(** [clock_eq env eq] performs the clock-calculus for equation [eq] in
environment [env] *)
let clock_eq env eq =
- let expr_lhs = expr_of_expr_list eq.eq_loc (List.map (fun v -> expr_of_ident v eq.eq_loc) eq.eq_lhs) in
+ let expr_lhs = expr_of_expr_list eq.eq_loc
+ (List.map (fun v -> expr_of_ident v eq.eq_loc) eq.eq_lhs) in
let ck_rhs = clock_expr env eq.eq_rhs in
clock_subtyping_arg env expr_lhs ck_rhs
@@ -649,7 +651,7 @@ let clock_var_decl scoped env vdecl =
else
*)
if Types.get_clock_base_type vdecl.var_type <> None
- then new_ck (Ccarrying ((new_carrier Carry_name scoped),ck)) scoped
+ then new_ck (Ccarrying (new_carrier Carry_name scoped, ck)) scoped
else ck in
(if vdecl.var_dec_const
then match vdecl.var_dec_value with
@@ -685,9 +687,9 @@ let clock_node env loc nd =
List.iter (clock_eq new_env) eqs;
let ck_ins = clock_of_vlist nd.node_inputs in
let ck_outs = clock_of_vlist nd.node_outputs in
- let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in
+ let ck_node = new_ck (Carrow (ck_ins, ck_outs)) false in
unify_imported_clock None ck_node loc;
- Log.report ~level:3 (fun fmt -> Format.fprintf fmt "%a@ " print_ck ck_node);
+ Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Clock of %s: %a@ " nd.node_id print_ck ck_node);
(* Local variables may contain first-order carrier variables that should be generalized.
That's not the case for types. *)
try_generalize ck_node loc;
@@ -699,7 +701,7 @@ let clock_node env loc nd =
(* if (is_main && is_polymorphic ck_node) then
raise (Error (loc,(Cannot_be_polymorphic ck_node)));
*)
- Log.report ~level:3 (fun fmt -> Format.fprintf fmt "%a@ " print_ck ck_node);
+ Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Generalized clock of %s: %a@ @ " nd.node_id print_ck ck_node);
nd.node_clock <- ck_node;
Env.add_value env nd.node_id ck_node
diff --git a/src/clocks.ml b/src/clocks.ml
index aa37d0ba..9a4cfe7a 100644
--- a/src/clocks.ml
+++ b/src/clocks.ml
@@ -191,7 +191,10 @@ let clock_on ck cr l =
clock_of_clock_list (List.map (fun ck -> new_ck (Con (ck,cr,l)) true) (clock_list_of_clock ck))
let clock_current ck =
- clock_of_clock_list (List.map (fun ck -> match (repr ck).cdesc with Con(ck',_,_) -> ck' | _ -> assert false) (clock_list_of_clock ck))
+ clock_of_clock_list (List.map (fun ck -> match (repr ck).cdesc with
+ | Con(ck',_,_) -> ck'
+ | _ -> Format.eprintf "internal error: Clocks.clock_current %a@." print_ck_long (repr ck);
+ assert false) (clock_list_of_clock ck))
let clock_of_impnode_clock ck =
let ck = repr ck in
@@ -394,11 +397,11 @@ let pp_error fmt = function
| Factor_zero ->
fprintf fmt "Cannot apply clock transformation with factor 0@."
| Carrier_extrusion (ck,cr) ->
- fprintf fmt "This node has clock@.%a@.It is invalid as %a escapes its scope@."
+ fprintf fmt "This node has clock@.%a@.It is invalid as the carrier %a escapes its scope@."
print_ck ck
print_carrier cr
| Clock_extrusion (ck_node,ck) ->
- fprintf fmt "This node has clock@.%a@.It is invalid as %a escapes its scope@."
+ fprintf fmt "This node has clock@.%a@.It is invalid as the clock %a escapes its scope@."
print_ck ck_node
print_ck ck
diff --git a/src/corelang.ml b/src/corelang.ml
index 8f89123c..32e57bda 100644
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -1009,15 +1009,17 @@ let pp_decl_type fmt tdecl =
| Node nd ->
fprintf fmt "%s: " nd.node_id;
Utils.reset_names ();
- fprintf fmt "%a@ " Types.print_ty nd.node_type
+ fprintf fmt "%a" Types.print_ty nd.node_type
| ImportedNode ind ->
fprintf fmt "%s: " ind.nodei_id;
Utils.reset_names ();
- fprintf fmt "%a@ " Types.print_ty ind.nodei_type
+ fprintf fmt "%a" Types.print_ty ind.nodei_type
| Const _ | Include _ | Open _ | TypeDef _ -> ()
let pp_prog_type fmt tdecl_list =
- Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list
+ Utils.Format.(pp_print_list
+ ~pp_open_box:pp_open_vbox0
+ pp_decl_type fmt tdecl_list)
let pp_decl_clock fmt cdecl =
match cdecl.top_decl_desc with
diff --git a/src/machine_code.ml b/src/machine_code.ml
index 16fe106f..abc36a7e 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -165,6 +165,8 @@ let rec translate_act env (y, expr) =
(* Datastructure updated while visiting equations *)
type machine_ctx = {
+ (* machine name *)
+ id: ident;
(* Memories *)
m: VSet.t;
(* Reset instructions *)
@@ -181,7 +183,8 @@ type machine_ctx = {
t: mc_formula_t list;
}
-let ctx_init = {
+let ctx_init id = {
+ id;
m = VSet.empty;
si = [];
j = IMap.empty;
@@ -191,18 +194,21 @@ let ctx_init = {
t = []
}
+let ctx_dummy = ctx_init ""
+
(****************************************************************)
(* Main function to translate equations into this machine context we
are building *)
(****************************************************************)
-let mk_control id vs v l inst =
+let mk_control v l inst =
mkinstr
- (Imply (mk_clocked_on id vs, inst.instr_spec))
+ True
+ (* (Imply (mk_clocked_on id vs, inst.instr_spec)) *)
(MBranch (v, [l, [inst]]))
-let control_on_clock env ctx ck inst =
- let rec aux (ck_ids, vs, ctx, inst as acc) ck =
+let control_on_clock env ctx ck spec inst =
+ let rec aux (ck_ids, vs, ctx, spec, inst as acc) ck =
match (Clocks.repr ck).cdesc with
| Con (ck, cr, l) ->
let id = Clocks.const_of_carrier cr in
@@ -212,66 +218,79 @@ let control_on_clock env ctx ck inst =
let ck_spec = mk_condition v l in
aux (id :: ck_ids,
v :: vs,
- { ctx
- with c = IMap.add id ck_spec
- (IMap.add id'
- (And [ck_spec; mk_clocked_on ck_ids' vs]) ctx.c)
+ { ctx with
+ c = IMap.add id ck_spec
+ (IMap.add id' (And [ck_spec; mk_clocked_on ck_ids' vs]) ctx.c)
},
- mk_control id' (v :: vs) v l inst) ck
+ Imply (mk_clocked_on id' (v :: vs), spec),
+ mk_control v l inst) ck
| _ -> acc
in
- let _, _, ctx, inst = aux ([], [], ctx, inst) ck in
- ctx, inst
+ let _, _, ctx, spec, inst = aux ([], [], ctx, spec, inst) ck in
+ ctx, spec, inst
let reset_instance env i r c =
match r with
| Some r ->
- [snd (control_on_clock env ctx_init c
- (mk_conditional
- (translate_guard env r)
- [mkinstr True (MReset i)]
- [mkinstr True (MNoReset i)]))]
+ let _, _, inst = control_on_clock env ctx_dummy c True
+ (mk_conditional
+ (translate_guard env r)
+ [mkinstr True (MReset i)]
+ [mkinstr True (MNoReset i)]) in
+ [ inst ]
| None -> []
-let translate_eq env ctx eq =
+let translate_eq env ctx i eq =
let translate_expr = translate_expr env in
let translate_act = translate_act env in
- let control_on_clock ck inst =
- let ctx, ins = control_on_clock env ctx ck inst in
- { ctx with s = ins :: ctx.s }
+ let control_on_clock ck spec inst =
+ let ctx, _spec, inst = control_on_clock env ctx ck spec inst in
+ { ctx with
+ s = { inst with
+ instr_spec = mk_transition ~i ctx.id [] } :: ctx.s }
in
let reset_instance = reset_instance env in
let mkinstr' = mkinstr ~lustre_eq:eq True in
- let ctl ?(ck=eq.eq_rhs.expr_clock) instr =
- control_on_clock ck (mkinstr' instr) in
+ let ctl ?(ck=eq.eq_rhs.expr_clock) spec instr =
+ control_on_clock ck spec (mkinstr' instr) in
(* Format.eprintf "translate_eq %a with clock %a@."
Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock; *)
match eq.eq_lhs, eq.eq_rhs.expr_desc with
| [x], Expr_arrow (e1, e2) ->
let var_x = env.get_var x in
- let o = new_instance (Arrow.arrow_top_decl ()) eq.eq_rhs.expr_tag in
+ let td = Arrow.arrow_top_decl () in
+ let o = new_instance td eq.eq_rhs.expr_tag in
let c1 = translate_expr e1 in
let c2 = translate_expr e2 in
- let ctx = ctl (MStep ([var_x], o, [c1;c2])) in
+ let ctx = ctl
+ (mk_transition (node_name td) [])
+ (MStep ([var_x], o, [c1;c2])) in
{ ctx with
si = mkinstr True (MReset o) :: ctx.si;
- j = IMap.add o (Arrow.arrow_top_decl (), []) ctx.j;
+ j = IMap.add o (td, []) ctx.j;
}
+
| [x], Expr_pre e1 when env.is_local x ->
let var_x = env.get_var x in
- let ctx = ctl (MStateAssign (var_x, translate_expr e1)) in
+ let ctx = ctl
+ True
+ (MStateAssign (var_x, translate_expr e1)) in
{ ctx with
m = VSet.add var_x ctx.m;
}
+
| [x], Expr_fby (e1, e2) when env.is_local x ->
let var_x = env.get_var x in
- let ctx = ctl (MStateAssign (var_x, translate_expr e2)) in
+ let ctx = ctl
+ True
+ (MStateAssign (var_x, translate_expr e2)) in
{ ctx with
m = VSet.add var_x ctx.m;
si = mkinstr' (MStateAssign (var_x, translate_expr e1)) :: ctx.si;
}
+
| p, Expr_appl (f, arg, r)
when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
let var_p = List.map (fun v -> env.get_var v) p in
@@ -284,7 +303,10 @@ let translate_eq env ctx eq =
el [eq.eq_rhs.expr_clock] in
let call_ck = Clock_calculus.compute_root_clock
(Clock_predef.ck_tuple env_cks) in
- let ctx = ctl ~ck:call_ck (MStep (var_p, o, vl)) in
+ let ctx = ctl
+ ~ck:call_ck
+ True
+ (MStep (var_p, o, vl)) in
(*Clocks.new_var true in
Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;
Format.eprintf "call %a: %a: %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple env_cks) Clocks.print_ck call_ck;*)
@@ -297,9 +319,11 @@ let translate_eq env ctx eq =
else reset_instance o r call_ck)
@ ctx.s
}
+
| [x], _ ->
let var_x = env.get_var x in
- control_on_clock eq.eq_rhs.expr_clock (translate_act (var_x, eq.eq_rhs))
+ control_on_clock eq.eq_rhs.expr_clock True (translate_act (var_x, eq.eq_rhs))
+
| _ ->
Format.eprintf "internal error: Machine_code.translate_eq %a@?"
Printers.pp_node_eq eq;
@@ -317,7 +341,11 @@ let constant_equations locals =
locals []
let translate_eqs env ctx eqs =
- List.fold_right (fun eq ctx -> translate_eq env ctx eq) eqs ctx
+ List.fold_right (fun eq (ctx, i) ->
+ let ctx = translate_eq env ctx i eq in
+ ctx, i - 1)
+ eqs (ctx, List.length eqs)
+ |> fst
(****************************************************************)
@@ -357,19 +385,19 @@ let process_asserts nd =
in
vars, eql, assertl
-let translate_core sorted_eqs locals other_vars =
+let translate_core nid sorted_eqs locals other_vars =
let constant_eqs = constant_equations locals in
let env = build_env locals other_vars in
(* Compute constants' instructions *)
- let ctx0 = translate_eqs env ctx_init constant_eqs in
+ let ctx0 = translate_eqs env (ctx_init nid) constant_eqs in
assert (VSet.is_empty ctx0.m);
assert (ctx0.si = []);
assert (IMap.is_empty ctx0.j);
(* Compute ctx for all eqs *)
- let ctx = translate_eqs env ctx_init sorted_eqs in
+ let ctx = translate_eqs env (ctx_init nid) sorted_eqs in
ctx, ctx0.s
@@ -402,7 +430,8 @@ let translate_decl nd sch =
* VSet.pp inout_vars
* ; *)
- let ctx, ctx0_s = translate_core (assert_instrs@sorted_eqs) locals inout_vars in
+ let ctx, ctx0_s = translate_core
+ nd.node_id (assert_instrs@sorted_eqs) locals inout_vars in
(* Format.eprintf "ok4@.@?"; *)
diff --git a/src/machine_code_common.ml b/src/machine_code_common.ml
index b47810af..35512053 100644
--- a/src/machine_code_common.ml
+++ b/src/machine_code_common.ml
@@ -3,7 +3,8 @@ open Machine_code_types
open Spec_types
open Spec_common
open Corelang
-
+open Utils.Format
+
let print_statelocaltag = true
let is_memory m id =
@@ -16,55 +17,64 @@ let rec pp_val m fmt v =
| Var v ->
if is_memory m v then
if print_statelocaltag then
- Format.fprintf fmt "%s(S)" v.var_id
+ fprintf fmt "{%s}" v.var_id
else
- Format.pp_print_string fmt v.var_id
+ pp_print_string fmt v.var_id
else
if print_statelocaltag then
- Format.fprintf fmt "%s(L)" v.var_id
+ fprintf fmt "%s" v.var_id
else
- Format.pp_print_string fmt v.var_id
- | Array vl -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val) vl
- | Access (t, i) -> Format.fprintf fmt "%a[%a]" pp_val t pp_val i
- | Power (v, n) -> Format.fprintf fmt "(%a^%a)" pp_val v pp_val n
- | Fun (n, vl) -> Format.fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val) vl
+ pp_print_string fmt v.var_id
+ | Array vl -> fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val) vl
+ | Access (t, i) -> fprintf fmt "%a[%a]" pp_val t pp_val i
+ | Power (v, n) -> fprintf fmt "(%a^%a)" pp_val v pp_val n
+ | Fun (n, vl) -> fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val) vl
+
+module PrintSpec = PrintSpec(struct
+ type t = value_t
+ type ctx = machine_t
+ let pp_val = pp_val
+ end)
let rec pp_instr m fmt i =
let pp_val = pp_val m and
pp_branch = pp_branch m in
let _ =
match i.instr_desc with
- | MLocalAssign (i,v) -> Format.fprintf fmt "%s<-l- %a" i.var_id pp_val v
- | MStateAssign (i,v) -> Format.fprintf fmt "%s<-s- %a" i.var_id pp_val v
- | MReset i -> Format.fprintf fmt "reset %s" i
- | MNoReset i -> Format.fprintf fmt "noreset %s" i
+ | MLocalAssign (i,v) -> fprintf fmt "%s := %a" i.var_id pp_val v
+ | MStateAssign (i,v) -> fprintf fmt "{%s} := %a" i.var_id pp_val v
+ | MReset i -> fprintf fmt "reset %s" i
+ | MNoReset i -> fprintf fmt "noreset %s" i
| MStep (il, i, vl) ->
- Format.fprintf fmt "%a = %s (%a)"
- (Utils.fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) il
+ fprintf fmt "%a = %s (%a)"
+ (Utils.fprintf_list ~sep:", " (fun fmt v -> pp_print_string fmt v.var_id)) il
i
(Utils.fprintf_list ~sep:", " pp_val) vl
| MBranch (g,hl) ->
- Format.fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]"
+ fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]"
pp_val g
(Utils.fprintf_list ~sep:"@," pp_branch) hl
- | MComment s -> Format.pp_print_string fmt s
- | MSpec s -> Format.pp_print_string fmt ("@" ^ s)
+ | MComment s -> pp_print_string fmt s
+ | MSpec s -> pp_print_string fmt ("@" ^ s)
in
(* Annotation *)
(* let _ = *)
- (* match i.lustre_expr with None -> () | Some e -> Format.fprintf fmt " -- original expr: %a" Printers.pp_expr e *)
+ (* match i.lustre_expr with None -> () | Some e -> fprintf fmt " -- original expr: %a" Printers.pp_expr e *)
(* in *)
- let _ =
- match i.lustre_eq with None -> () | Some eq -> Format.fprintf fmt " -- original eq: %a" Printers.pp_node_eq eq
- in
- ()
-
+ begin match i.lustre_eq with
+ | None -> ()
+ | Some eq -> fprintf fmt " -- original eq: %a" Printers.pp_node_eq eq
+ end;
+ fprintf fmt "@ --%@ %a" (PrintSpec.pp_spec m) i.instr_spec
+
+
and pp_branch m fmt (t, h) =
- Format.fprintf fmt "@[<v 2>%s:@,%a@]" t (Utils.fprintf_list ~sep:"@," (pp_instr m)) h
+ fprintf fmt "@[<v 2>%s:@,%a@]" t
+ (pp_print_list ~pp_open_box:pp_open_vbox0 (pp_instr m)) h
-and pp_instrs m fmt il =
- Format.fprintf fmt "@[<v 2>%a@]" (Utils.fprintf_list ~sep:"@," (pp_instr m)) il
+let pp_instrs m =
+ pp_print_list ~pp_open_box:pp_open_vbox0 (pp_instr m)
(* merge log: get_node_def was in c0f8 *)
@@ -74,9 +84,9 @@ let get_node_def id m =
let (decl, _) = List.assoc id m.mcalls in
Corelang.node_of_top decl
with Not_found -> (
- (* Format.eprintf "Unable to find node %s in list [%a]@.@?" *)
+ (* eprintf "Unable to find node %s in list [%a]@.@?" *)
(* id *)
- (* (Utils.fprintf_list ~sep:", " (fun fmt (n,_) -> Format.fprintf fmt "%s" n)) m.mcalls *)
+ (* (Utils.fprintf_list ~sep:", " (fun fmt (n,_) -> fprintf fmt "%s" n)) m.mcalls *)
(* ; *)
raise Not_found
)
@@ -85,22 +95,24 @@ let get_node_def id m =
let machine_vars m = m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory
let pp_step m fmt s =
- Format.fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ asserts : @[%a@]@]@ "
- (Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_inputs
- (Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_outputs
- (Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_locals
- (Utils.fprintf_list ~sep:", " (fun fmt (_, c) -> pp_val m fmt c)) s.step_checks
- (Utils.fprintf_list ~sep:"@ " (pp_instr m)) s.step_instrs
- (Utils.fprintf_list ~sep:", " (pp_val m)) s.step_asserts
+ let pp_list = pp_print_list ~pp_sep:pp_print_comma in
+ fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ asserts : @[%a@]@]@ "
+ (pp_list Printers.pp_var) s.step_inputs
+ (pp_list Printers.pp_var) s.step_outputs
+ (pp_list Printers.pp_var) s.step_locals
+ (pp_list (fun fmt (_, c) -> pp_val m fmt c))
+ s.step_checks
+ (pp_instrs m) s.step_instrs
+ (pp_list (pp_val m)) s.step_asserts
let pp_static_call fmt (node, args) =
- Format.fprintf fmt "%s<%a>"
+ fprintf fmt "%s<%a>"
(node_name node)
(Utils.fprintf_list ~sep:", " Dimension.pp_dimension) args
let pp_machine fmt m =
- Format.fprintf fmt
+ fprintf fmt
"@[<v 2>machine %s@ \
mem : %a@ \
instances: %a@ \
@@ -112,18 +124,18 @@ let pp_machine fmt m =
annot : @[%a@]@]@ "
m.mname.node_id
(Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory
- (Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) -> Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances
+ (Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) -> fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances
(Utils.fprintf_list ~sep:"@ " (pp_instr m)) m.minit
(Utils.fprintf_list ~sep:"@ " (pp_instr m)) m.mconst
(pp_step m) m.mstep
(fun fmt -> match m.mspec.mnode_spec with
| None -> ()
- | Some (NodeSpec id) -> Format.fprintf fmt "cocospec: %s" id
+ | Some (NodeSpec id) -> fprintf fmt "cocospec: %s" id
| Some (Contract spec) -> Printers.pp_spec fmt spec)
(Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot
let pp_machines fmt ml =
- Format.fprintf fmt "@[<v 0>%a@]" (Utils.fprintf_list ~sep:"@," pp_machine) ml
+ fprintf fmt "@[<v 0>%a@]" (Utils.fprintf_list ~sep:"@," pp_machine) ml
let rec is_const_value v =
@@ -159,23 +171,26 @@ let get_instr_spec i = i.instr_spec
let mk_conditional ?lustre_eq c t e =
mkinstr ?lustre_eq
- (Ternary (Val c,
- And (List.map get_instr_spec t),
- And (List.map get_instr_spec e)))
+ (* (Ternary (Val c,
+ * And (List.map get_instr_spec t),
+ * And (List.map get_instr_spec e))) *)
+ True
(MBranch(c, [
(tag_true, t);
(tag_false, e) ]))
let mk_branch ?lustre_eq c br =
mkinstr ?lustre_eq
- (And (List.map (fun (l, instrs) ->
- Imply (Equal (Val c, Tag l), And (List.map get_instr_spec instrs)))
- br))
+ (* (And (List.map (fun (l, instrs) ->
+ * Imply (Equal (Val c, Tag l), And (List.map get_instr_spec instrs)))
+ * br)) *)
+ True
(MBranch (c, br))
let mk_assign ?lustre_eq x v =
mkinstr ?lustre_eq
- (Equal (Var x, Val v))
+ (* (Equal (Var x, Val v)) *)
+ True
(MLocalAssign (x, v))
let mk_val v t =
@@ -290,9 +305,9 @@ let get_machine machines node_name =
try
Utils.desome (get_machine_opt machines node_name)
with Utils.DeSome ->
- Format.eprintf "Unable to find machine %s in machines %a@.@?"
+ eprintf "Unable to find machine %s in machines %a@.@?"
node_name
- (Utils.fprintf_list ~sep:", " (fun fmt m -> Format.pp_print_string fmt m.mname.node_id)) machines
+ (Utils.fprintf_list ~sep:", " (fun fmt m -> pp_print_string fmt m.mname.node_id)) machines
; assert false
let get_const_assign m id =
diff --git a/src/machine_code_types.ml b/src/machine_code_types.ml
index 283c6ea1..9403b67b 100644
--- a/src/machine_code_types.ml
+++ b/src/machine_code_types.ml
@@ -46,9 +46,11 @@ type step_t = {
type static_call = top_decl * (Dimension.dim_expr list)
+type mc_transition_t = value_t transition_t
+
type machine_spec = {
mnode_spec: node_spec_t option;
- mtransitions: value_t transition_t list
+ mtransitions: mc_transition_t list
}
type machine_t = {
diff --git a/src/spec_types.ml b/src/spec_types.ml
index d9136f7b..a96d0a44 100644
--- a/src/spec_types.ml
+++ b/src/spec_types.ml
@@ -14,7 +14,7 @@ type 'a expression_t =
type predicate_t =
(* | Memory_pack *)
| Clocked_on of ident
- | Transition
+ | Transition of ident * int option
| Initialization
type 'a formula_t =
diff --git a/src/types.ml b/src/types.ml
index be2fe4ac..8313081c 100644
--- a/src/types.ml
+++ b/src/types.ml
@@ -187,7 +187,7 @@ and print_ty_param pp_basic fmt ty =
| Tarray (e, ty) ->
fprintf fmt "%a^%a" print_ty ty Dimension.pp_dimension e
| Tlink ty ->
- print_ty fmt ty
+ print_ty fmt ty
| Tunivar ->
fprintf fmt "'%s" (name_of_type ty.tid)
diff --git a/src/typing.ml b/src/typing.ml
index 3a747ab8..1e5ea9a1 100644
--- a/src/typing.ml
+++ b/src/typing.ml
@@ -208,63 +208,63 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
let rec unif t1 t2 =
let t1 = repr t1 in
let t2 = repr t2 in
- if t1==t2 then
+ if t1 == t2 then
()
else
match t1.tdesc,t2.tdesc with
(* strictly subtyping cases first *)
| _ , Tclock t2 when sub && (get_clock_base_type t1 = None) ->
- unif t1 t2
+ unif t1 t2
| _ , Tstatic (_, t2) when sub && (get_static_value t1 = None) ->
- unif t1 t2
+ unif t1 t2
(* This case is not mandatory but will keep "older" types *)
| Tvar, Tvar ->
- if t1.tid < t2.tid then
- t2.tdesc <- Tlink t1
- else
- t1.tdesc <- Tlink t2
+ if t1.tid < t2.tid then
+ t2.tdesc <- Tlink t1
+ else
+ t1.tdesc <- Tlink t2
| Tvar, _ when (not semi) && (not (occurs t1 t2)) ->
- t1.tdesc <- Tlink t2
+ t1.tdesc <- Tlink t2
| _, Tvar when (not (occurs t2 t1)) ->
- t2.tdesc <- Tlink t1
+ t2.tdesc <- Tlink t1
| Tarrow (t1,t2), Tarrow (t1',t2') ->
- begin
- unif t2 t2';
- unif t1' t1
- end
+ begin
+ unif t2 t2';
+ unif t1' t1
+ end
| Ttuple tl, Ttuple tl' when List.length tl = List.length tl' ->
- List.iter2 unif tl tl'
+ List.iter2 unif tl tl'
| Ttuple [t1] , _ -> unif t1 t2
| _ , Ttuple [t2] -> unif t1 t2
| Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' ->
- List.iter2 (fun (_, t) (_, t') -> unif t t') fl fl'
+ List.iter2 (fun (_, t) (_, t') -> unif t t') fl fl'
| Tclock _, Tstatic _
- | Tstatic _, Tclock _ -> raise (Unify (t1, t2))
+ | Tstatic _, Tclock _ -> raise (Unify (t1, t2))
| Tclock t1', Tclock t2' -> unif t1' t2'
- | Tbasic t1, Tbasic t2 when t1 == t2 -> ()
+ (* | Tbasic t1, Tbasic t2 when t1 == t2 -> () *)
| Tunivar, _ | _, Tunivar -> ()
| (Tconst t, _) ->
- let def_t = get_type_definition t in
- unif def_t t2
+ let def_t = get_type_definition t in
+ unif def_t t2
| (_, Tconst t) ->
- let def_t = get_type_definition t in
- unif t1 def_t
+ let def_t = get_type_definition t in
+ unif t1 def_t
| Tenum tl, Tenum tl' when tl == tl' -> ()
| Tstatic (e1, t1'), Tstatic (e2, t2')
- | Tarray (e1, t1'), Tarray (e2, t2') ->
- let eval_const =
- if semi
- then (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c))
- else (fun _ -> None) in
- begin
- unif t1' t2';
- Dimension.eval Basic_library.eval_dim_env eval_const e1;
- Dimension.eval Basic_library.eval_dim_env eval_const e2;
- Dimension.unify ~semi:semi e1 e2;
- end
+ | Tarray (e1, t1'), Tarray (e2, t2') ->
+ let eval_const =
+ if semi
+ then (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c))
+ else (fun _ -> None) in
+ begin
+ unif t1' t2';
+ Dimension.eval Basic_library.eval_dim_env eval_const e1;
+ Dimension.eval Basic_library.eval_dim_env eval_const e2;
+ Dimension.unify ~semi:semi e1 e2;
+ end
(* Special cases for machine_types. Rules to unify static types infered
- for numerical constants with non static ones for variables with
- possible machine types *)
+ for numerical constants with non static ones for variables with
+ possible machine types *)
| Tbasic bt1, Tbasic bt2 when BasicT.is_unifiable bt1 bt2 -> BasicT.unify bt1 bt2
| _,_ -> raise (Unify (t1, t2))
in unif t1 t2
@@ -274,7 +274,7 @@ module Make (T: Types.S) (Expr_type_hub: EXPR_TYPE_HUB with type type_expr = T.t
try
unify ~sub:sub ~semi:semi ty1 ty2
with
- | Unify _ ->
+ | Unify (t1', t2') ->
raise (Error (loc, Type_clash (ty1,ty2)))
| Dimension.Unify _ ->
raise (Error (loc, Type_clash (ty1,ty2)))
--
GitLab