Commit 52de3095 authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

modified process types to have a (maybe) cleaner code

parent a5f83a17
Pipeline #1638 passed with stage
in 1 minute and 56 seconds
......@@ -27,10 +27,10 @@ let parse_problem input_channel =
Fmt.pf Fmt.stderr "@.")
decl_list;
Printf.eprintf "Left process:\n";
print_process Fmt.stderr p_left;
print_concrete_process Fmt.stderr p_left;
Fmt.pf Fmt.stderr "@.";
Printf.eprintf "Right process:\n";
print_process Fmt.stderr p_right;
print_concrete_process Fmt.stderr p_right;
Fmt.pf Fmt.stderr "@.";) in
(decl_list,(p_left,p_right))
with
......
This diff is collapsed.
open Term
open Side
(* We only support public channels. *)
type channel = Public of string
type p_name_string = string
type proc_name = string
type concrete =
| Simple of proc_name
| Loop of proc_name * int
type p_name =
| Simple_proc of p_name_string
| Rec_proc of p_name_string * int
type abstract =
| ASimple of proc_name
| ALoop of proc_name * int
| ARec
(* Type of processes. Mind the fact that in an Apply (s, l) the name s must be
binded to a process whose free variables are all bounded by the application
(i.e. after application the resulting process has no free variables). *)
type process =
type 'a process =
| Nil
| Apply of p_name * msg term list
| New of string * process
| In of channel * string * process
| Out of channel * msg term * process
| Parallel of process * process
| IfThenElse of boole term * process * process
| Let of string * msg term * process
| Apply of 'a * msg term list
| New of string * 'a process
| In of channel * string * 'a process
| Out of channel * msg term * 'a process
| Parallel of 'a process * 'a process
| IfThenElse of boole term * 'a process * 'a process
| Let of string * msg term * 'a process
(* Declaration of a parametrized process.
- PProcess (name, args_name, p) is the declaration of the process 'p',
......@@ -32,29 +37,41 @@ type process =
name{i-1} as a sub-process; and name{0} is 'p0'.
The free variable of 'pi' and 'p0' must be a subset of args_name. *)
type declaration =
| PProcess of p_name_string * string list * process
| PRec of p_name_string * string list * process * process
| PProcess of proc_name * string list * concrete process
| PRec of proc_name * string list * abstract process * concrete process
(* A recursive process declaration was badly done *)
exception Bad_rec_declaration of string
(* Apply (s,l) called on undefined parametrized process. *)
exception Undefined_process of p_name
exception Undefined_process of concrete
(* Apply (s,l) called on with the wrong number of arguments. *)
exception Bad_arity of p_name * int * int
exception Bad_arity of concrete * int * int
(* Remark: The folding algorithm used is only sound for action-deterministic
processes. We use an sound but cot complete algorithm to check whether the
input processes are action-deterministic. *)
exception Not_deterministic of string
exception Bad_injection
(*****************)
(* Miscellaneous *)
(*****************)
(* inject p : Return a concrete process from an abstract one. p should not
contain any ARec. *)
val inject : abstract process -> concrete process
(***************************)
(* Process Pretty Printers *)
(***************************)
val print_process : Format.formatter -> process -> unit
val print_concrete_process : Format.formatter -> concrete process -> unit
val print_abstract_process : string -> Format.formatter -> abstract process
-> unit
val print_process_decl : Format.formatter -> declaration -> unit
......@@ -71,5 +88,5 @@ val add_declarations : declaration list -> unit
(********************)
val fold_protocol :
environement -> process -> process ->
environement -> concrete process -> concrete process ->
((msg term * msg term) list * environement) list
......@@ -14,26 +14,22 @@
%start term_list bterm_list problem
%type <Term.msg Term.term list> term_list
%type <Term.boole Term.term list> bterm_list
%type <Process.declaration list * (Process.process * Process.process)> problem
%type <Process.declaration list * (Process.concrete Process.process * Process.concrete Process.process)> problem
%left PARALLEL
%right ELSE
%%
(* Process Name *)
p_name_aux:
| i = NAME MINUS ONE
{ -2 }
| i = NAME
{ -1 }
| j = INT
{ j }
process_name:
abstract:
| n = NAME
{ Process.Simple_proc(n) }
| n = NAME LCURLY j = p_name_aux RCURLY
{ Process.Rec_proc(n,j) }
{ Process.ASimple(n) }
| n = NAME LCURLY j = INT RCURLY
{ Process.ALoop(n,j) }
| n = NAME LCURLY ONE RCURLY
{ Process.ALoop(n,1) }
| n = NAME LCURLY NAME MINUS ONE RCURLY
{ Process.ARec }
(* Terms *)
term_list:
......@@ -91,7 +87,7 @@ apply_arg:
process:
| LPAREN p = process RPAREN
{ p }
| id = process_name args = apply_arg
| id = abstract args = apply_arg
{ Process.Apply (id, args) }
| NEW s = NAME DOT p = process
{ Process.New (s, p) }%prec PARALLEL
......@@ -120,22 +116,20 @@ arg_list:
declaration:
| LET s = NAME l = arg_list p = process SEMICOLON
{ Process.PProcess (s, l, p) }
| LET s1 = NAME LCURLY i1 = p_name_aux RCURLY
{ Process.PProcess (s, l, Process.inject p) }
| LET s1 = NAME LCURLY i1 = NAME RCURLY
l1 = arg_list p1 = process SEMICOLON
LET s2 = NAME LCURLY i2 = p_name_aux RCURLY
LET s2 = NAME LCURLY i2 = INT RCURLY
l2 = arg_list p2 = process SEMICOLON
{ if (s1 <> s2) || (l1 <> l2) then
raise (Process.Bad_rec_declaration
(Printf.sprintf "%s %s %d %d"
s1 s2 (List.length l1) (List.length l2)))
else if (i1 = -1) && (i2 = 0) then
Process.PRec (s1, l1, p1,p2)
else if (i1 = 0) && (i2 = -1) then
Process.PRec (s1, l2, p2,p1)
else if (i1 = "i") && (i2 = 0) then
Process.PRec (s1, l1, p1, Process.inject p2)
else
raise (Process.Bad_rec_declaration
(Printf.sprintf "%s %d %d"
(Printf.sprintf "%s %s %d"
s1 i1 i2))}
declaration_list:
......@@ -146,4 +140,4 @@ declaration_list:
problem:
| l = declaration_list GOAL p1 = process SIM p2 = process EOF
{ (l, (p1,p2))}
{ (l, (Process.inject p1,Process.inject p2))}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment