Commit 01674849 authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

corrected a bug in process printing, term printing and type checking

parent c0bd5a28
Pipeline #1658 failed with stage
in 38 seconds
......@@ -14,7 +14,6 @@ exception Process_badly_formed of string
let parse_problem input_channel =
let lexbuf = Lexing.from_channel input_channel in
(* print_tokens lexbuf; *)
try
let (decl_list,(p_left,p_right)) =
Term_parser.problem Term_lexer.token lexbuf in
......@@ -84,12 +83,12 @@ let main_interactive () =
let _ = debug (fun () ->
let open Fmt in
pf stderr "Parsed process %d declarations:\n@.@[<v 0>%a@]\n"
pf stderr "@[<v 0>Parsed process %d declarations:@;@[<v 0>%a@]@;@]"
(List.length declarations)
(list (fun ppf process ->
print_process_decl ppf process))
declarations;
pf stderr "Left process:@[%a@]\nRight process:@[%a@]\n@.%!"
pf stderr "@[<v 0>Left process:@[%a@]@;Right process:@[%a@]@]@.%!"
(print_concrete_process env) p_l
(print_concrete_process env) p_r) in
......
......@@ -146,17 +146,21 @@ let rec print_process env proc_call_printer ppf process =
(Fmt.list ~sep:(fun ppf () -> pf ppf "@ ") (print_term_par env)) l
| New (s,p) ->
let env' = rebind_type env s TName in
pf ppf "@[<hov>%a %a.@,@[%a@]@]"
(kw `Red) "new"
(kw `Magenta) s
(print_process env proc_call_printer) p
(print_process env' proc_call_printer) p
| In (Public c, s, p) ->
let env' = rebind_type env s TVar in
pf ppf "@[<hov>%a(%a,@,%a).@,%a@]"
(kw `Bold) "in"
(kw `None) c
(styled `Magenta (styled `Bold ident)) s
(print_process env proc_call_printer) p
(print_process env' proc_call_printer) p
| Out (Public c, t, p) ->
pf ppf "@[<hov>%a(%a,@,%a).@,%a@]"
......@@ -190,12 +194,14 @@ let rec print_process env proc_call_printer ppf process =
(print_process env proc_call_printer) p2
| Let (s,t,p) ->
let env' = rebind_type env s TVar in
pf ppf "@[<v>@[<2>%a %a =@ @[%a@] %a@]@ %a@]"
(kw `Bold) "let"
(styled `Magenta (styled `Bold ident)) s
(print_term env) t
(print_term env') t
(styled `Bold ident) "in"
(print_process env proc_call_printer) p
(print_process env' proc_call_printer) p
let print_concrete_process env ppf process =
print_process env print_concrete ppf process
......
......@@ -195,6 +195,9 @@ let string_type_to_string v = match v with
| TName -> "Nonce"
| BTName -> "Boolean Nonce";;
exception Not_type_checking of string
let is_binded env s = StringMap.mem s env.string_types
let term_is_binded : type a. env -> a term -> bool =
fun env t -> match get_sort t with
......@@ -233,12 +236,12 @@ let get_bindings : type a. env -> a sort
| Msg -> StringMap.fold (fun var u acc -> (var,u) :: acc) env.t_bindings []
| Bool -> StringMap.fold (fun var u acc -> (var,u) :: acc) env.bt_bindings []
let debug_print_string_types ht =
let debug_print_string_types env =
Debug.debug (fun () ->
Printf.eprintf "Type-checking error, dumping the current type table:\n";
StringMap.iter (fun s mtype ->
Printf.eprintf "%s -> %s\n" s (string_type_to_string mtype))
ht);
env.string_types);
Printf.eprintf "%!";;
exception No_such_binding of variable_string
......@@ -311,22 +314,24 @@ let rec print_term : type a. env -> Format.formatter -> a term -> unit =
else
match t.content with
| Name (s,Bool) ->
if term_is_binded env t then
if is_binded env s then
let s_type = StringMap.find s env.string_types in
if s_type = BTVar then
(styled `Bold (styled `Magenta ident)) ppf s
else
(kw `Magenta) ppf s
else begin
assert (s_type = BTName);
(kw `Magenta) ppf s end
else
(kw `Magenta) ppf s
| Name (s,Msg) ->
if term_is_binded env t then
if is_binded env s then
let s_type = StringMap.find s env.string_types in
if s_type = TVar then
(styled `Bold (styled `Magenta ident)) ppf s
else
(kw `Magenta) ppf s
else begin
assert (s_type = TName);
(kw `Magenta) ppf s end
else
(kw `Magenta) ppf s
......@@ -482,10 +487,6 @@ let bindings_to_print env =
(* Variable typing *)
(*******************)
exception Not_type_checking of string
let is_binded env s = StringMap.mem s env.string_types
(* fresh_name env pre : Return a string s such that pre is a preffix of s, and
s is fresh in env. *)
let fresh_name env pre =
......@@ -508,9 +509,14 @@ let typing_err env s mtype =
(string_type_to_string mtype)
(string_type_to_string (StringMap.find s env.string_types)) in
let _ = debug_print_string_types env.string_types in
let _ = debug_print_string_types env in
raise (Not_type_checking error_message)
(* rebind_type env s mtype: Add a new binding between s and mtype. If such a
binding already exists, it is replaced. *)
let rebind_type env s mtype =
{env with string_types = StringMap.add s mtype env.string_types }
(* bind_type env s mtype: Add a new binding between s and mtype if it does
not already exists. *)
let bind_type env s mtype =
......@@ -538,7 +544,7 @@ let rec type_check : type a. a term -> env -> env =
| Name (s,Msg) ->
if is_binded env s then
let s_type = StringMap.find s env.string_types in
if (s_type <> TVar) || (s_type <> TName) then
if (s_type <> TVar) && (s_type <> TName) then
typing_err env s TVar
else
env
......@@ -548,7 +554,7 @@ let rec type_check : type a. a term -> env -> env =
| Name (s,Bool) ->
if is_binded env s then
let s_type = StringMap.find s env.string_types in
if (s_type <> BTVar) || (s_type <> BTName) then
if (s_type <> BTVar) && (s_type <> BTName) then
typing_err env s BTVar
else
env
......
......@@ -145,6 +145,10 @@ val term_is_binded : env -> 'a term -> bool
s is fresh in env. *)
val fresh_name : env -> string -> string
(* rebind_type env s mtype: Add a new binding between s and mtype. If such a
binding already exists, it is replaced. *)
val rebind_type : env -> string -> string_type -> env
(* bind_type env s mtype: Add a new binding between s and mtype if it
does not already exists. *)
val bind_type : env -> string -> string_type -> env
......
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