Add typing-based disambiguation pass after desugaring

Some typing errors are changed a little, because they get triggered during the
typing of the disambiguation pass, which does not specify the expected return
type (it's an expected invariant that it should not be needed for
disambiguation).

It would be possible to still specify these types during disambiguation just to
get the same errors, but since the newer ones don't appear to be clearly worse
at the moment, it has not been done.
This commit is contained in:
Louis Gesbert 2022-11-28 16:23:27 +01:00
parent b3ee503b12
commit 8960e5dbbc
16 changed files with 310 additions and 82 deletions

View File

@ -0,0 +1,78 @@
(* This file is part of the Catala compiler, a specification language for tax
and social benefits computation rules. Copyright (C) 2020 Inria, contributor:
Louis Gesbert <louis.gesbert@inria.fr>
Licensed under the Apache License, Version 2.0 (the "License"); you may not
use this file except in compliance with the License. You may obtain a copy of
the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
License for the specific language governing permissions and limitations under
the License. *)
open Shared_ast
open Ast
let expr ctx env e =
(* The typer takes care of disambiguating: this consists in: - ensuring
[EAbs.tys] doesn't contain any [TAny] - [EDStructAccess.name_opt] is always
[Some] *)
(* Intermediate unboxings are fine since the last [untype] will rebox in
depth *)
Typing.check_expr ctx ~env (Expr.unbox e)
let rule ctx env rule =
let env =
match rule.rule_parameter with
| None -> env
| Some (v, ty) -> Typing.Env.add_var v ty env
in
(* Note: we could use the known rule type here to direct typing. We choose not
to because it shouldn't be needed for disambiguation, and we prefer to
focus on local type errors first. *)
{
rule with
rule_just = expr ctx env rule.rule_just;
rule_cons = expr ctx env rule.rule_cons;
}
let scope ctx env scope =
let env = Typing.Env.open_scope scope.scope_uid env in
let scope_defs =
ScopeDefMap.map
(fun def ->
let scope_def_rules =
(* Note: ordering in file order might be better for error reporting ?
When we gather errors, the ordering could be done afterwards,
though *)
RuleName.Map.map (rule ctx env) def.scope_def_rules
in
{ def with scope_def_rules })
scope.scope_defs
in
let scope_assertions = List.map (expr ctx env) scope.scope_assertions in
{ scope with scope_defs; scope_assertions }
let program prg =
let env =
ScopeName.Map.fold
(fun scope_name scope env ->
let vars =
ScopeDefMap.fold
(fun var def vars ->
match var with
| Var (v, _states) -> ScopeVar.Map.add v def.scope_def_typ vars
| SubScopeVar _ -> vars)
scope.scope_defs ScopeVar.Map.empty
in
Typing.Env.add_scope scope_name ~vars env)
prg.program_scopes Typing.Env.empty
in
let program_scopes =
ScopeName.Map.map (scope prg.program_ctx env) prg.program_scopes
in
{ prg with program_scopes }

View File

@ -0,0 +1,24 @@
(* This file is part of the Catala compiler, a specification language for tax
and social benefits computation rules. Copyright (C) 2020 Inria, contributor:
Louis Gesbert <louis.gesbert@inria.fr>
Licensed under the Apache License, Version 2.0 (the "License"); you may not
use this file except in compliance with the License. You may obtain a copy of
the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
License for the specific language governing permissions and limitations under
the License. *)
(** This module does local typing in order to fill some missing type information
in the AST:
- it fills the types of arguments in [EAbs] nodes, (untyped ones are
inserted during desugaring, e.g. by `let-in` constructs),
- it resolves the structure names of [EDStructAccess] nodes. *)
val program : Ast.program -> Ast.program

View File

@ -317,6 +317,7 @@ let rec translate_expr
| LetIn (x, e1, e2) ->
let ctxt, v = Name_resolution.add_def_local_var ctxt (Marked.unmark x) in
let tau = TAny, Marked.get_mark x in
(* This type will be resolved in Scopelang.Desambiguation *)
let fn =
Expr.make_abs [| v |]
(translate_expr scope inside_definition_of ctxt e2)
@ -1250,6 +1251,7 @@ let translate_program
ScopeName.Map.add scope scope_out_struct acc
| _ -> acc)
ctxt.Name_resolution.typedefs ScopeName.Map.empty;
ctx_struct_fields = ctxt.Name_resolution.field_idmap;
};
Ast.program_scopes;
}

View File

@ -167,6 +167,8 @@ let driver source_file (options : Cli.options) : int =
in
Cli.debug_print "Desugaring...";
let prgm = Desugared.From_surface.translate_program ctxt prgm in
Cli.debug_print "Disambiguating...";
let prgm = Desugared.Disambiguate.program prgm in
Cli.debug_print "Collecting rules...";
let prgm = Scopelang.From_desugared.translate_program prgm in
match backend with

View File

@ -26,6 +26,7 @@ type target_scope_vars =
| States of (StateName.t * ScopeVar.t) list
type ctx = {
decl_ctx : decl_ctx;
scope_var_mapping : target_scope_vars ScopeVar.Map.t;
var_mapping : (Desugared.Ast.expr, untyped Ast.expr Var.t) Var.Map.t;
}
@ -73,10 +74,25 @@ let rec translate_expr (ctx : ctx) (e : Desugared.Ast.expr) :
| EVar v -> Expr.evar (Var.Map.find v ctx.var_mapping) m
| EStruct { name; fields } ->
Expr.estruct name (StructField.Map.map (translate_expr ctx) fields) m
| EDStructAccess { e; field; name_opt } ->
assert false
(* TODO: resolve!! *)
(* Expr.estructaccess (translate_expr ctx e) field name_opt m *)
| EDStructAccess { name_opt = None; _ } ->
(* Note: this could only happen if disambiguation was disabled. If we want
to support it, we should still allow this case when the field has only
one possible matching structure *)
Errors.raise_spanned_error (Expr.mark_pos m)
"Ambiguous structure field access"
| EDStructAccess { e; field; name_opt = Some name } ->
let e' = translate_expr ctx e in
let field =
try
StructName.Map.find name
(IdentName.Map.find field ctx.decl_ctx.ctx_struct_fields)
with Not_found ->
(* Should not happen after disambiguation *)
Errors.raise_spanned_error (Expr.mark_pos m)
"Field %s does not belong to structure %a" field StructName.format_t
name
in
Expr.estructaccess e' field name m
| EInj { e; cons; name } -> Expr.einj (translate_expr ctx e) cons name m
| EMatch { e; name; cases } ->
Expr.ematch (translate_expr ctx e) name
@ -653,7 +669,11 @@ let translate_program (pgrm : Desugared.Ast.program) : untyped Ast.program =
})
scope_decl.Desugared.Ast.scope_vars ctx)
pgrm.Desugared.Ast.program_scopes
{ scope_var_mapping = ScopeVar.Map.empty; var_mapping = Var.Map.empty }
{
scope_var_mapping = ScopeVar.Map.empty;
var_mapping = Var.Map.empty;
decl_ctx = pgrm.program_ctx;
}
in
let ctx_scopes =
ScopeName.Map.map

View File

@ -374,6 +374,8 @@ type scope_out_struct = {
type decl_ctx = {
ctx_enums : enum_ctx;
ctx_structs : struct_ctx;
ctx_struct_fields : StructField.t StructName.Map.t IdentName.Map.t;
(** needed for disambiguation (desugared -> scope) *)
ctx_scopes : scope_out_struct ScopeName.Map.t;
}

View File

@ -372,10 +372,10 @@ module Box : sig
a separate argument. *)
val app1 :
('a, 't) boxed_gexpr ->
(('a, 't) gexpr -> ('a, 't) naked_gexpr) ->
't ->
('a, 't) boxed_gexpr
('a, 't1) boxed_gexpr ->
(('a, 't1) gexpr -> ('a, 't2) naked_gexpr) ->
't2 ->
('a, 't2) boxed_gexpr
val app2 :
('a, 't) boxed_gexpr ->

View File

@ -47,7 +47,8 @@ and naked_typ =
| TArray of unionfind_typ
| TAny of Any.t
let rec typ_to_ast (ty : unionfind_typ) : A.typ =
let rec typ_to_ast ?(unsafe = false) (ty : unionfind_typ) : A.typ =
let typ_to_ast = typ_to_ast ~unsafe in
let ty, pos = UnionFind.get (UnionFind.find ty) in
match ty with
| TLit l -> A.TLit l, pos
@ -58,11 +59,22 @@ let rec typ_to_ast (ty : unionfind_typ) : A.typ =
| TArrow (t1, t2) -> A.TArrow (typ_to_ast t1, typ_to_ast t2), pos
| TArray t1 -> A.TArray (typ_to_ast t1), pos
| TAny _ ->
(* No polymorphism in Catala: type inference should return full types
without wildcards, and this function is used to recover the types after
typing. *)
Errors.raise_spanned_error pos
"Internal error: typing at this point could not be resolved"
if unsafe then A.TAny, pos
else
(* No polymorphism in Catala: type inference should return full types
without wildcards, and this function is used to recover the types after
typing. *)
Errors.raise_spanned_error pos
"Internal error: typing at this point could not be resolved"
(* Checks that there are no type variables remaining *)
let rec all_resolved ty =
match Marked.unmark (UnionFind.get (UnionFind.find ty)) with
| TAny _ -> false
| TLit _ | TStruct _ | TEnum _ -> true
| TOption t1 | TArray t1 -> all_resolved t1
| TArrow (t1, t2) -> all_resolved t1 && all_resolved t2
| TTuple ts -> List.for_all all_resolved ts
let rec ast_to_typ (ty : A.typ) : unionfind_typ =
let ty' =
@ -111,9 +123,11 @@ let rec format_typ
format_typ t2
| TArray t1 -> (
match Marked.unmark (UnionFind.get (UnionFind.find t1)) with
| TAny _ -> Format.pp_print_string fmt "collection"
| TAny _ when not !Cli.debug_flag -> Format.pp_print_string fmt "collection"
| _ -> Format.fprintf fmt "@[collection@ %a@]" format_typ t1)
| TAny _ -> Format.pp_print_string fmt "<any>"
| TAny v ->
if !Cli.debug_flag then Format.fprintf fmt "<a%d>" (Any.hash v)
else Format.pp_print_string fmt "<any>"
exception Type_error of A.any_expr * unionfind_typ * unionfind_typ
@ -310,6 +324,15 @@ module Env = struct
let add_scope scope_name ~vars t =
{ t with scopes = A.ScopeName.Map.add scope_name vars t.scopes }
let open_scope scope_name t =
let scope_vars =
A.ScopeVar.Map.union
(fun _ _ -> assert false)
t.scope_vars
(A.ScopeName.Map.find scope_name t.scopes)
in
{ t with scope_vars }
end
let add_pos e ty = Marked.mark (Expr.pos e) ty
@ -413,7 +436,46 @@ and typecheck_expr_top_down :
fields
in
Expr.estruct name fields' mark
| A.EDStructAccess { e = e_struct; name_opt; field } -> assert false
| A.EDStructAccess { e = e_struct; name_opt; field } ->
let t_struct =
match name_opt with
| Some name -> TStruct name
| None -> TAny (Any.fresh ())
in
let e_struct' =
typecheck_expr_top_down ctx env (unionfind t_struct) e_struct
in
let name =
match UnionFind.get (ty e_struct') with
| TStruct name, _ -> name
| TAny _, _ ->
Printf.ksprintf failwith
"Disambiguation failed before reaching field %s" field
| _ ->
Errors.raise_spanned_error (Expr.pos e)
"This is not a structure, cannot access field %s (%a)" field
(format_typ ctx) (ty e_struct')
in
let fld_ty =
let str =
try A.StructName.Map.find name ctx.A.ctx_structs
with Not_found ->
Errors.raise_spanned_error pos_e "No structure %a found"
A.StructName.format_t name
in
let field =
try
A.StructName.Map.find name
(A.IdentName.Map.find field ctx.ctx_struct_fields)
with Not_found ->
Errors.raise_spanned_error context_mark.pos
"Field %s does not belong to structure %a" field
A.StructName.format_t name
in
A.StructField.Map.find field str
in
let mark = uf_mark (ast_to_typ fld_ty) in
Expr.edstructaccess e_struct' field (Some name) mark
| A.EStructAccess { e = e_struct; name; field } ->
let fld_ty =
let str =
@ -522,6 +584,7 @@ and typecheck_expr_top_down :
tau_args t_ret
in
let mark = uf_mark t_func in
assert (List.for_all all_resolved tau_args);
let xs, body = Bindlib.unmbind binder in
let xs' = Array.map Var.translate xs in
let env =
@ -532,7 +595,13 @@ and typecheck_expr_top_down :
let body' = typecheck_expr_top_down ctx env t_ret body in
let binder' = Bindlib.bind_mvar xs' (Expr.Box.lift body') in
Expr.eabs binder' (List.map typ_to_ast tau_args) mark
| A.EApp { f = e1; args } ->
| A.EApp { f = (EOp _, _) as e1; args } ->
(* Same as EApp, but the typing order is different to help with
disambiguation: - type of the operator is extracted first (to figure
linked type vars between arguments) - arguments are typed right-to-left,
because our operators with function args always have the functions first,
and the argument types of those functions can always be inferred from the
later operator arguments *)
let t_args = List.map (fun _ -> unionfind (TAny (Any.fresh ()))) args in
let t_func =
List.fold_right
@ -540,7 +609,24 @@ and typecheck_expr_top_down :
t_args tau
in
let e1' = typecheck_expr_top_down ctx env t_func e1 in
let args' =
List.rev_map2
(typecheck_expr_top_down ctx env)
(List.rev t_args) (List.rev args)
in
Expr.eapp e1' args' context_mark
| A.EApp { f = e1; args } ->
(* Here we type the arguments first (in order), to ensure we know the types
of the arguments if [f] is [EAbs] before disambiguation. This is also the
right order for the [let-in] form. *)
let t_args = List.map (fun _ -> unionfind (TAny (Any.fresh ()))) args in
let t_func =
List.fold_right
(fun t_arg acc -> unionfind (TArrow (t_arg, acc)))
t_args tau
in
let args' = List.map2 (typecheck_expr_top_down ctx env) t_args args in
let e1' = typecheck_expr_top_down ctx env t_func e1 in
Expr.eapp e1' args' context_mark
| A.EOp op -> Expr.eop op (uf_mark (op_type (Marked.mark pos_e op)))
| A.EDefault { excepts; just; cons } ->
@ -588,19 +674,27 @@ let wrap_expr ctx f e =
let get_ty_mark { uf; pos } = A.Typed { ty = typ_to_ast uf; pos }
(* Infer the type of an expression *)
let expr
let expr_raw
(type a)
(ctx : A.decl_ctx)
?(env = Env.empty)
?(typ : A.typ option)
(e : (a, 'm) A.gexpr) : (a, A.typed A.mark) A.boxed_gexpr =
(e : (a, 'm) A.gexpr) : (a, mark) A.gexpr =
let fty =
match typ with
| None -> typecheck_expr_bottom_up ctx env
| Some typ -> typecheck_expr_top_down ctx env (ast_to_typ typ)
in
Expr.map_marks ~f:get_ty_mark (wrap_expr ctx fty e)
wrap_expr ctx fty e
let check_expr ctx ?env ?typ e =
Expr.map_marks
~f:(fun { pos; _ } -> A.Untyped { pos })
(expr_raw ctx ?env ?typ e)
(* Infer the type of an expression *)
let expr ctx ?env ?typ e =
Expr.map_marks ~f:get_ty_mark (expr_raw ctx ?env ?typ e)
let rec scope_body_expr ctx env ty_out body_expr =
match body_expr with

View File

@ -26,6 +26,7 @@ module Env : sig
val add_var : 'e Var.t -> typ -> 'e t -> 'e t
val add_scope_var : ScopeVar.t -> typ -> 'e t -> 'e t
val add_scope : ScopeName.t -> vars:typ ScopeVar.Map.t -> 'e t -> 'e t
val open_scope : ScopeName.t -> 'e t -> 'e t
end
val expr :
@ -43,6 +44,17 @@ val expr :
filling the gaps ([TAny]) if any. Use [Expr.untype] first if this is not
what you want. *)
val check_expr :
decl_ctx ->
?env:'e Env.t ->
?typ:typ ->
(('a, 'm mark) gexpr as 'e) ->
('a, untyped mark) boxed_gexpr
(** Same as [expr], but doesn't annotate the returned expression. Equivalent to
[Typing.expr |> Expr.untype], but more efficient. This can be useful for
type-checking and disambiguation (some AST nodes are updated with missing
information, e.g. any [TAny] appearing in the AST is replaced) *)
val program : ('a, 'm mark) gexpr program -> ('a, typed mark) gexpr program
(** Typing on whole programs (as defined in Shared_ast.program, i.e. for the
later dcalc/lcalc stages.

View File

@ -403,27 +403,28 @@ let enfant_le_plus_age (enfant_le_plus_age_in: EnfantLePlusAgeIn.t) : EnfantLePl
start_line=12; start_column=14; end_line=12; end_column=25;
law_headings=["Règles diverses"; "Épilogue"]} true))
(fun (_: unit) ->
(let predicate_ : Enfant.t -> date =
(fun (potentiel_plus_age_: Enfant.t) ->
potentiel_plus_age_.Enfant.date_de_naissance)
in
(Array.fold_left
(fun (acc_: Enfant.t) (item_: Enfant.t) ->
if ((predicate_ acc_) <@ (predicate_ item_)) then
acc_ else item_)
({Enfant.identifiant = (integer_of_string "-1");
Enfant.obligation_scolaire =
(SituationObligationScolaire.Pendant ());
Enfant.remuneration_mensuelle = (money_of_cents_string
"0");
Enfant.date_de_naissance =
(date_of_numbers (2999) (12) (31));
Enfant.prise_en_charge =
(PriseEnCharge.EffectiveEtPermanente ());
Enfant.a_deja_ouvert_droit_aux_allocations_familiales =
false;
Enfant.beneficie_titre_personnel_aide_personnelle_logement =
false}) enfants_))))
Array.fold_left
(fun (acc_: Enfant.t) (item_: Enfant.t) ->
if
((let potentiel_plus_age_ : Enfant.t = acc_
in
(potentiel_plus_age_.Enfant.date_de_naissance)) <@
(let potentiel_plus_age_ : Enfant.t = item_
in
(potentiel_plus_age_.Enfant.date_de_naissance))) then
acc_ else item_)
({Enfant.identifiant = (integer_of_string "-1");
Enfant.obligation_scolaire =
(SituationObligationScolaire.Pendant ());
Enfant.remuneration_mensuelle = (money_of_cents_string "0");
Enfant.date_de_naissance =
(date_of_numbers (2999) (12) (31));
Enfant.prise_en_charge =
(PriseEnCharge.EffectiveEtPermanente ());
Enfant.a_deja_ouvert_droit_aux_allocations_familiales =
false;
Enfant.beneficie_titre_personnel_aide_personnelle_logement =
false}) enfants_))
with
EmptyError -> (raise (NoValueProvided
{filename = "examples/allocations_familiales/prologue.catala_fr";

View File

@ -17,10 +17,10 @@ $ catala Interpret -s A
--> money
Error coming from typechecking the following expression:
┌─⯈ tests/test_array/bad/fold_error.catala_en:10.52-56:
┌─⯈ tests/test_array/bad/fold_error.catala_en:10.61-62:
└──┐
10 │ definition list_high_count equals number for m in list of (m >=$ $7)
‾‾‾
└─ Article
Type integer coming from expression:

View File

@ -11,14 +11,21 @@ scope TestXorWithInt:
```catala-test-inline
$ catala Typecheck
[ERROR] Error during typechecking, incompatible types:
--> bool
--> integer
--> bool
Error coming from typechecking the following expression:
┌─⯈ tests/test_bool/bad/test_xor_with_int.catala_en:8.32-35:
┌─⯈ tests/test_bool/bad/test_xor_with_int.catala_en:8.36-38:
└─┐
8 │ definition test_var equals 10 xor 20
│ ‾‾‾
│ ‾‾
└─ 'xor' should be a boolean operator
Type integer coming from expression:
┌─⯈ tests/test_bool/bad/test_xor_with_int.catala_en:8.36-38:
└─┐
8 │ definition test_var equals 10 xor 20
│ ‾‾
└─ 'xor' should be a boolean operator
Type bool coming from expression:
@ -27,12 +34,5 @@ Type bool coming from expression:
8 │ definition test_var equals 10 xor 20
│ ‾‾‾
└─ 'xor' should be a boolean operator
Type integer coming from expression:
┌─⯈ tests/test_bool/bad/test_xor_with_int.catala_en:5.27-34:
└─┐
5 │ context test_var content integer
│ ‾‾‾‾‾‾‾
└─ 'xor' should be a boolean operator
#return code 255#
```

View File

@ -19,7 +19,7 @@ scope A:
```catala-test-inline
$ catala Interpret -s A
[ERROR] Struct Foo does not contain field g
[ERROR] Field g does not belong to structure Foo
┌─⯈ tests/test_struct/bad/wrong_qualified_field.catala_en:17.22-29:
└──┐

View File

@ -18,12 +18,5 @@ scope A:
```catala-test-inline
$ catala Interpret -s A
[ERROR] This struct field name is ambiguous, it can belong to Foo or Bar. Disambiguate it by prefixing it with the struct name.
┌─⯈ tests/test_struct/bad/ambiguous_fields.catala_en:16.24-25:
└──┐
16 │ definition y equals x.f
│ ‾
└─ Article
#return code 255#
[RESULT] Computation successful!
```

View File

@ -13,28 +13,28 @@ scope S:
```catala-test-inline
$ catala Typecheck
[ERROR] Error during typechecking, incompatible types:
--> integer
--> decimal
--> collection
Error coming from typechecking the following expression:
┌─⯈ tests/test_typing/bad/err2.catala_en:10.43-44:
┌─⯈ tests/test_typing/bad/err2.catala_en:10.38-41:
└──┐
10 │ definition a equals number of (z ++ 1.1) / 2
│ ‾
Type integer coming from expression:
┌─⯈ tests/test_typing/bad/err2.catala_en:10.43-44:
└──┐
10 │ definition a equals number of (z ++ 1.1) / 2
│ ‾
│ ‾‾‾
Type decimal coming from expression:
┌─⯈ tests/test_typing/bad/common.catala_en:15.19-26:
┌─⯈ tests/test_typing/bad/err2.catala_en:10.38-41:
└──┐
15 │ output a content decimal
│ ‾‾‾‾‾‾‾
10 │ definition a equals number of (z ++ 1.1) / 2
│ ‾‾‾
Type collection coming from expression:
┌─⯈ tests/test_typing/bad/err2.catala_en:10.22-28:
└──┐
10 │ definition a equals number of (z ++ 1.1) / 2
│ ‾‾‾‾‾‾
#return code 255#
```

View File

@ -31,10 +31,10 @@ Type integer coming from expression:
Type Structure coming from expression:
┌─⯈ tests/test_typing/bad/common.catala_en:14.30-39:
└─
14 │ output z content collection Structure
‾‾‾‾‾‾‾‾‾
┌─⯈ tests/test_typing/bad/err5.catala_en:6.4-45:
└─┐
6 │ Structure { -- i: 3 -- e: Int content x };
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
#return code 255#
```