From 2cfb3482740cb996c5993a8b85b2e9bfd83e6b16 Mon Sep 17 00:00:00 2001 From: Denis Merigoux Date: Wed, 30 Dec 2020 01:13:28 +0100 Subject: [PATCH] Debugged unification and typing --- src/catala/default_calculus/typing.ml | 33 +++++++++--------------- tests/test_array/fold_error.catala.A.out | 13 ++++++++++ 2 files changed, 25 insertions(+), 21 deletions(-) create mode 100644 tests/test_array/fold_error.catala.A.out diff --git a/src/catala/default_calculus/typing.ml b/src/catala/default_calculus/typing.ml index 3422f6c5..e16bb869 100644 --- a/src/catala/default_calculus/typing.ml +++ b/src/catala/default_calculus/typing.ml @@ -68,7 +68,7 @@ let rec format_typ (fmt : Format.formatter) (typ : typ Pos.marked UnionFind.elem (** Raises an error if unification cannot be performed *) let rec unify (t1 : typ Pos.marked UnionFind.elem) (t2 : typ Pos.marked UnionFind.elem) : unit = - Cli.debug_print (Format.asprintf "Unifying %a and %a" format_typ t1 format_typ t2); + (* Cli.debug_print (Format.asprintf "Unifying %a and %a" format_typ t1 format_typ t2); *) let t1_repr = UnionFind.get (UnionFind.find t1) in let t2_repr = UnionFind.get (UnionFind.find t2) in let repr = @@ -101,12 +101,7 @@ let rec unify (t1 : typ Pos.marked UnionFind.elem) (t2 : typ Pos.marked UnionFin ] in let t_union = UnionFind.union t1 t2 in - match repr with - | None -> () - | Some t_repr -> - Cli.debug_print - (Format.asprintf "Setting %a to %a" format_typ t_union format_typ (UnionFind.make t_repr)); - UnionFind.set t_union t_repr + match repr with None -> () | Some t_repr -> UnionFind.set t_union t_repr (** Operators have a single type, instead of being polymorphic with constraints. This allows us to have a simpler type system, while we argue the syntactic burden of operator annotations helps @@ -179,7 +174,7 @@ let rec typ_to_ast (ty : typ Pos.marked UnionFind.elem) : A.typ Pos.marked = (** {1 Double-directed typing} *) -type env = typ Pos.marked A.VarMap.t +type env = typ Pos.marked UnionFind.elem A.VarMap.t (** Infers the most permissive type from an expression *) let rec typecheck_expr_bottom_up (env : env) (e : A.expr Pos.marked) : typ Pos.marked UnionFind.elem @@ -188,7 +183,7 @@ let rec typecheck_expr_bottom_up (env : env) (e : A.expr Pos.marked) : typ Pos.m match Pos.unmark e with | EVar v -> ( match A.VarMap.find_opt (Pos.unmark v) env with - | Some t -> UnionFind.make t + | Some t -> t | None -> Errors.raise_spanned_error "Variable not found in the current context" (Pos.get_position e) ) @@ -252,13 +247,13 @@ let rec typecheck_expr_bottom_up (env : env) (e : A.expr Pos.marked) : typ Pos.m if Array.length xs = List.length taus then let xstaus = List.map2 - (fun x tau -> (x, (ast_to_typ (Pos.unmark tau), Pos.get_position tau))) + (fun x tau -> (x, UnionFind.make (ast_to_typ (Pos.unmark tau), Pos.get_position tau))) (Array.to_list xs) taus in let env = List.fold_left (fun env (x, tau) -> A.VarMap.add x tau env) env xstaus in List.fold_right (fun (_, t_arg) (acc : typ Pos.marked UnionFind.elem) -> - UnionFind.make (TArrow (UnionFind.make t_arg, acc), pos_binder)) + UnionFind.make (TArrow (t_arg, acc), pos_binder)) xstaus (typecheck_expr_bottom_up env body) else @@ -299,17 +294,17 @@ let rec typecheck_expr_bottom_up (env : env) (e : A.expr Pos.marked) : typ Pos.m es; UnionFind.make (Pos.same_pos_as (TArray cell_type) e) in - Cli.debug_print (Format.asprintf "Found type of %a: %a" Print.format_expr e format_typ out); + (* Cli.debug_print (Format.asprintf "Found type of %a: %a" Print.format_expr e format_typ out); *) out (** Checks whether the expression can be typed with the provided type *) and typecheck_expr_top_down (env : env) (e : A.expr Pos.marked) (tau : typ Pos.marked UnionFind.elem) : unit = - Cli.debug_print (Format.asprintf "Typechecking %a : %a" Print.format_expr e format_typ tau); + (* Cli.debug_print (Format.asprintf "Typechecking %a : %a" Print.format_expr e format_typ tau); *) match Pos.unmark e with | EVar v -> ( match A.VarMap.find_opt (Pos.unmark v) env with - | Some tau' -> ignore (unify tau (UnionFind.make tau')) + | Some tau' -> ignore (unify tau tau') | None -> Errors.raise_spanned_error "Variable not found in the current context" (Pos.get_position e) ) @@ -390,19 +385,15 @@ and typecheck_expr_top_down (env : env) (e : A.expr Pos.marked) if Array.length xs = List.length t_args then let xstaus = List.map2 - (fun x t_arg -> (x, Pos.map_under_mark ast_to_typ t_arg)) + (fun x t_arg -> (x, UnionFind.make (Pos.map_under_mark ast_to_typ t_arg))) (Array.to_list xs) t_args in let env = List.fold_left (fun env (x, t_arg) -> A.VarMap.add x t_arg env) env xstaus in let t_out = typecheck_expr_bottom_up env body in let t_func = List.fold_right - (fun t_arg acc -> - UnionFind.make - (Pos.same_pos_as - (TArrow (UnionFind.make (ast_to_typ (Pos.unmark t_arg), pos_binder), acc)) - e)) - t_args t_out + (fun (_, t_arg) acc -> UnionFind.make (Pos.same_pos_as (TArrow (t_arg, acc)) e)) + xstaus t_out in unify t_func tau else diff --git a/tests/test_array/fold_error.catala.A.out b/tests/test_array/fold_error.catala.A.out new file mode 100644 index 00000000..49bdd846 --- /dev/null +++ b/tests/test_array/fold_error.catala.A.out @@ -0,0 +1,13 @@ +[ERROR] Error during typechecking, types money and integer are incompatible +[ERROR] +[ERROR] Type money coming from expression: +[ERROR] --> test_array/fold_error.catala +[ERROR] | +[ERROR] 10 | def list_high_count := number for m in list of (m >=$ $7) +[ERROR] | ^^^ +[ERROR] +[ERROR] Type integer coming from expression: +[ERROR] --> test_array/fold_error.catala +[ERROR] | +[ERROR] 5 | param list content set int +[ERROR] | ^^^^^^^