CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-11-09 01:35:56 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' into aides_logement

Browse Source
This commit is contained in:
Denis Merigoux 2022-10-17 16:42:46 +02:00
commit f037a39bf4
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
110 changed files with 12907 additions and 11265 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
.git-blame-ignore-revs
View File

@ -1,6 +1,12 @@
# Reformatting commits to be skipped when running 'git blame'
# Use `git config --global blame.ignoreRevsFile .git-blame-ignore-revs` to use it
# Add new reformatting commits at the top
14f1ebfd0ad65bdd3408bb6ba9c254df97a59ad9
fee64d6f6f4b13da7a63fae92b78d69fc4122cc1
bd17857e904fa7381c05461674d49594f770b87b
06dbab74d2e392229833d6f7d5ca7abe629e7bd6
ba620fca280338139e015e316894a7cf49c450d5
7485c7f2ce726f59f1ec66ddfe1d3f7d640201d8

6
.nix/unionfind.nix
View File

@ -2,7 +2,7 @@
buildDunePackage rec {
pname = "unionFind";
version = "20200320";
version = "20220122";
minimumOCamlVersion = "4.0.8";
@ -10,8 +10,8 @@ buildDunePackage rec {
src = fetchurl {
url =
"https://gitlab.inria.fr/fpottier/unionFind/-/archive/20200320/archive.tar.gz";
hash = "sha256-szIwK9QyAw6fIIWDOiiyfyrEFZaaErGPRLkGhIK9STI=";
"https://gitlab.inria.fr/fpottier/${pname}/-/archive/${version}/archive.tar.gz";
hash = "sha256-85+5KNYKXsNAH568qR8/AFC9UDviLJEO/Fztc9cRHZA=";
};
meta = with lib; {

11
Makefile
View File

@ -53,6 +53,9 @@ build_dev: parser-messages
$(BUILD_SYSTEM_DIR)/clerk.exe \
$(CATALA_LEGIFRANCE_DIR)/catala_legifrance.exe
# Just the base compiler as needed to run the tests
compiler: parser-messages
dune build $(COMPILER_DIR)/catala.exe $(COMPILER_DIR)/plugins/ $(BUILD_SYSTEM_DIR)/clerk.exe
#> build : Builds the Catala compiler
build: parser-messages format build_dev
@ -305,11 +308,11 @@ CLERK=$(CLERK_BIN) --exe $(CATALA_BIN) \
.FORCE:
test_suite: .FORCE
$(MAKE) -C tests pass_all_tests
test_suite: .FORCE compiler
@$(MAKE) -C tests pass_all_tests
test_examples: .FORCE
$(MAKE) -C examples pass_all_tests
test_examples: .FORCE compiler
@$(MAKE) -C examples pass_all_tests
#> tests : Run interpreter tests
tests: test_suite test_examples

106
build_system/clerk_driver.ml
View File

@ -314,6 +314,32 @@ let search_for_expected_outputs (file : string) : expected_output_descr list =
test_declarations)
[@ocamlformat "disable"]
(** Var references used in the Clerk file *)
module Var = struct
let tested_file = Nj.Expr.Var "tested_file"
let catala_cmd = Nj.Expr.Var "catala_cmd"
let expected_output = Nj.Expr.Var "expected_output"
let test_file_or_folder = Nj.Expr.Var "test_file_or_folder"
let name = function
| Nj.Expr.Var n -> n
| _ -> invalid_arg "Clerk_driver.Var.name"
end
let pipe_diff_cmd =
let open Nj.Expr in
let has_patdiff = Sys.command "type patdiff >/dev/null 2>&1" = 0 in
if has_patdiff then
Seq
[
Lit "|";
Lit "patdiff";
Seq [Lit "-alt-new"; Lit "current-output"];
Var.tested_file;
Lit "/dev/stdin";
]
else Seq [Lit "| colordiff -u -b"; Var.tested_file; Lit "-"]
let inline_test_rule catala_exe catala_opts =
let open Nj.Expr in
Nj.Rule.make "inline_tests"
@ -322,14 +348,16 @@ let inline_test_rule catala_exe catala_opts =
[
Lit Sys.argv.(0);
Lit "runtest";
Lit ("--exe=" ^ catala_exe);
Lit ("--catala-opts=" ^ catala_opts);
Var "tested_file";
Lit "| colordiff -u -b";
Var "tested_file";
Lit "-";
Seq [Lit "--exe"; Lit catala_exe];
Seq
[
Lit "--catala-opts";
Lit ("\"" ^ String.escaped catala_opts ^ "\"");
];
Var.tested_file;
pipe_diff_cmd;
])
~description:(Seq [Lit "INLINE TESTS of file"; Var "tested_file"])
~description:(Seq [Lit "INLINE TESTS of file"; Var.tested_file])
let inline_reset_rule catala_exe catala_opts =
let open Nj.Expr in
@ -342,9 +370,9 @@ let inline_reset_rule catala_exe catala_opts =
Lit ("--exe=" ^ catala_exe);
Lit ("--catala-opts=" ^ catala_opts);
Lit "--reset";
Var "tested_file";
Var.tested_file;
])
~description:(Seq [Lit "RESET INLINE TESTS of file"; Var "tested_file"])
~description:(Seq [Lit "RESET INLINE TESTS of file"; Var.tested_file])
let add_reset_rules_aux
~(redirect : string)
@ -354,12 +382,12 @@ let add_reset_rules_aux
let reset_common_cmd_exprs =
Nj.Expr.
[
Var "catala_cmd";
Var "tested_file";
Var.catala_cmd;
Var.tested_file;
Lit "--unstyled";
Lit "--output=-";
Lit redirect;
Var "expected_output";
Var.expected_output;
Lit "2>&1";
Lit "|| true";
]
@ -373,9 +401,9 @@ let add_reset_rules_aux
[
Lit "RESET";
Lit "file";
Var "tested_file";
Var.tested_file;
Lit "with the";
Var "catala_cmd";
Var.catala_cmd;
Lit "command";
])
in
@ -392,12 +420,12 @@ let add_test_rules_aux
Seq
(Lit catala_exe_opts
:: [
Var "catala_cmd";
Var "tested_file";
Var.catala_cmd;
Var.tested_file;
Lit "--unstyled";
Lit "--output=-";
Lit "2>&1 | colordiff -u -b";
Var "expected_output";
Var.expected_output;
Lit "-";
]))
~description:
@ -405,9 +433,9 @@ let add_test_rules_aux
Seq
[
Lit "TEST on file";
Var "tested_file";
Var.tested_file;
Lit "with the";
Var "catala_cmd";
Var.catala_cmd;
Lit "command";
])
in
@ -435,8 +463,7 @@ let ninja_start (catala_exe : string) (catala_opts : string) : ninja =
Nj.Rule.make "run_and_display_final_message"
~command:Nj.Expr.(Seq [Lit ":"])
~description:
Nj.Expr.(
Seq [Lit "All tests"; Var "test_file_or_folder"; Lit "passed!"])
Nj.Expr.(Seq [Lit "All tests"; Var.test_file_or_folder; Lit "passed!"])
in
{
rules =
@ -457,7 +484,7 @@ let collect_inline_ninja_builds
if not (has_inline_tests tested_file) then None
else
let ninja =
let vars = ["tested_file", Nj.Expr.Lit tested_file] in
let vars = [Var.(name tested_file), Nj.Expr.Lit tested_file] in
let rule_to_call =
if reset_test_outputs then "inline_tests_reset" else "inline_tests"
in
@ -513,9 +540,9 @@ let collect_all_ninja_build
in
let vars =
[
"catala_cmd", Nj.Expr.Lit expected_output.cmd;
"tested_file", Nj.Expr.Lit tested_file;
"expected_output", Nj.Expr.Lit expected_output_file;
Var.(name catala_cmd), Nj.Expr.Lit expected_output.cmd;
Var.(name tested_file), Nj.Expr.Lit tested_file;
Var.(name expected_output), Nj.Expr.Lit expected_output_file;
]
and rule_to_call =
if reset_test_outputs then "reset_rule" else "test_rule"
@ -580,7 +607,7 @@ let add_root_test_build
~inputs:[Nj.Expr.Lit all_test_builds]
~vars:
[
( "test_file_or_folder",
( Var.(name test_file_or_folder),
Nj.Expr.Lit ("in [ " ^ file_names_str ^ " ]") );
])
ninja.builds;
@ -588,7 +615,11 @@ let add_root_test_build
(** Directly runs the test (not using ninja, this will be called by ninja rules
through the "clerk runtest" command) *)
let run_inline_tests ~(reset : bool) (file : string) (catala_exe : string) =
let run_inline_tests
~(reset : bool)
(file : string)
(catala_exe : string)
(catala_opts : string list) =
match scan_for_inline_tests file with
| None -> Cli.warning_print "No inline tests found in %s" file
| Some file_tests ->
@ -600,10 +631,20 @@ let run_inline_tests ~(reset : bool) (file : string) (catala_exe : string) =
let ic = Unix.in_channel_of_descr cmd_out_rd in
let cmd =
Array.of_list
((catala_exe :: test.params) @ [file; "--unstyled"; "--output=-"])
((catala_exe :: catala_opts)
@ test.params
@ [file; "--unstyled"; "--output=-"])
in
let env =
Unix.environment ()
|> Array.to_seq
|> Seq.filter (fun s ->
not (String.starts_with ~prefix:"OCAMLRUNPARAM=" s))
|> Array.of_seq
in
let pid =
Unix.create_process catala_exe cmd Unix.stdin cmd_out_wr cmd_out_wr
Unix.create_process_env catala_exe cmd env Unix.stdin cmd_out_wr
cmd_out_wr
in
Unix.close cmd_out_wr;
let rec process_cmd_out () =
@ -742,7 +783,7 @@ let collect_in_folder
~inputs:[Nj.Expr.Lit test_file_names]
~vars:
[
( "test_file_or_folder",
( Var.(name test_file_or_folder),
Nj.Expr.Lit ("in folder '" ^ folder ^ "'") );
])
ninja.builds;
@ -885,7 +926,7 @@ let driver
(add_root_test_build ninja ctx.all_file_names
ctx.all_test_builds));
let ninja_cmd =
"ninja -f " ^ ninja_output ^ " " ^ ninja_flags ^ " test"
"ninja -k 0 -f " ^ ninja_output ^ " " ^ ninja_flags ^ " test"
in
Cli.debug_print "executing '%s'..." ninja_cmd;
let return = Sys.command ninja_cmd in
@ -909,7 +950,8 @@ let driver
| "runtest" -> (
match files_or_folders with
| [f] ->
run_inline_tests ~reset:reset_test_outputs f catala_exe;
run_inline_tests ~reset:reset_test_outputs f catala_exe
(List.filter (( <> ) "") (String.split_on_char ' ' catala_opts));
0
| _ ->
Cli.error_print "Please specify a single catala file to test";

33
compiler/dcalc/interpreter.ml
View File

@ -479,7 +479,7 @@ let interpret_program :
fun (ctx : decl_ctx) (e : 'm Ast.expr) :
(Uid.MarkedString.info * 'm Ast.expr) list ->
match evaluate_expr ctx e with
| EAbs (_, [((TStruct s_in, _) as targs)]), mark_e -> begin
| (EAbs (_, [((TStruct s_in, _) as _targs)]), mark_e) as e -> begin
(* At this point, the interpreter seeks to execute the scope but does not
have a way to retrieve input values from the command line. [taus] contain
the types of the scope arguments. For [context] arguments, we can provide
@ -491,8 +491,7 @@ let interpret_program :
(fun (_, ty) ->
match Marked.unmark ty with
| TArrow ((TLit TUnit, _), ty_in) ->
Expr.empty_thunked_term
(Expr.map_mark (fun pos -> pos) (fun _ -> ty_in) mark_e)
Expr.empty_thunked_term (Expr.with_ty mark_e ty_in)
| _ ->
Errors.raise_spanned_error (Marked.get_mark ty)
"This scope needs input arguments to be executed. But the Catala \
@ -503,31 +502,11 @@ let interpret_program :
taus
in
let to_interpret =
( EApp
( e,
[
( ETuple (application_term, Some s_in),
let pos =
match application_term with
| a :: _ -> Expr.pos a
| [] -> Pos.no_pos
in
Expr.map_mark (fun _ -> pos) (fun _ -> targs) mark_e );
] ),
Expr.map_mark
(fun pos -> pos)
(fun ty ->
match application_term, ty with
| [], t_out -> t_out
| _ :: _, (TArrow (_, t_out), _) -> t_out
| _ :: _, (_, bad_pos) ->
Errors.raise_spanned_error bad_pos
"@[<hv 2>(bug) Result of interpretation doesn't have the \
expected type:@ @[%a@]@]"
(Print.typ ctx) ty)
mark_e )
Expr.make_app (Bindlib.box e)
[Expr.make_tuple application_term (Some s_in) mark_e]
(Expr.pos e)
in
match Marked.unmark (evaluate_expr ctx to_interpret) with
match Marked.unmark (evaluate_expr ctx (Bindlib.unbox to_interpret)) with
| ETuple (args, Some s_out) ->
let s_out_fields =
List.map

55
compiler/dcalc/optimizations.ml
View File

@ -25,7 +25,7 @@ type partial_evaluation_ctx = {
let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : 'm expr) :
'm expr Bindlib.box =
let pos = Marked.get_mark e in
let mark = Marked.get_mark e in
let rec_helper = partial_evaluation ctx in
match Marked.unmark e with
| EApp
@ -35,9 +35,9 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : 'm expr) :
(* reduction of logical not *)
(Bindlib.box_apply (fun e1 ->
match e1 with
| ELit (LBool false), _ -> ELit (LBool true), pos
| ELit (LBool true), _ -> ELit (LBool false), pos
| _ -> EApp (op, [e1]), pos))
| ELit (LBool false), _ -> ELit (LBool true), mark
| ELit (LBool true), _ -> ELit (LBool false), mark
| _ -> EApp (op, [e1]), mark))
(rec_helper e1)
| EApp
( (( EOp (Binop Or), _
@ -49,8 +49,8 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : 'm expr) :
| (ELit (LBool false), _), new_e | new_e, (ELit (LBool false), _) ->
new_e
| (ELit (LBool true), _), _ | _, (ELit (LBool true), _) ->
ELit (LBool true), pos
| _ -> EApp (op, [e1; e2]), pos))
ELit (LBool true), mark
| _ -> EApp (op, [e1; e2]), mark))
(rec_helper e1) (rec_helper e2)
| EApp
( (( EOp (Binop And), _
@ -62,21 +62,21 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : 'm expr) :
| (ELit (LBool true), _), new_e | new_e, (ELit (LBool true), _) ->
new_e
| (ELit (LBool false), _), _ | _, (ELit (LBool false), _) ->
ELit (LBool false), pos
| _ -> EApp (op, [e1; e2]), pos))
ELit (LBool false), mark
| _ -> EApp (op, [e1; e2]), mark))
(rec_helper e1) (rec_helper e2)
| EVar x -> Bindlib.box_apply (fun x -> x, pos) (Bindlib.box_var x)
| EVar x -> Bindlib.box_apply (fun x -> x, mark) (Bindlib.box_var x)
| ETuple (args, s_name) ->
Bindlib.box_apply
(fun args -> ETuple (args, s_name), pos)
(fun args -> ETuple (args, s_name), mark)
(List.map rec_helper args |> Bindlib.box_list)
| ETupleAccess (arg, i, s_name, typs) ->
Bindlib.box_apply
(fun arg -> ETupleAccess (arg, i, s_name, typs), pos)
(fun arg -> ETupleAccess (arg, i, s_name, typs), mark)
(rec_helper arg)
| EInj (arg, i, e_name, typs) ->
Bindlib.box_apply
(fun arg -> EInj (arg, i, e_name, typs), pos)
(fun arg -> EInj (arg, i, e_name, typs), mark)
(rec_helper arg)
| EMatch (arg, arms, e_name) ->
Bindlib.box_apply2
@ -85,20 +85,20 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : 'm expr) :
| (EInj (e1, i, e_name', _ts), _), _
when EnumName.compare e_name e_name' = 0 ->
(* iota reduction *)
EApp (List.nth arms i, [e1]), pos
| _ -> EMatch (arg, arms, e_name), pos)
EApp (List.nth arms i, [e1]), mark
| _ -> EMatch (arg, arms, e_name), mark)
(rec_helper arg)
(List.map rec_helper arms |> Bindlib.box_list)
| EArray args ->
Bindlib.box_apply
(fun args -> EArray args, pos)
(fun args -> EArray args, mark)
(List.map rec_helper args |> Bindlib.box_list)
| ELit l -> Bindlib.box (ELit l, pos)
| ELit l -> Bindlib.box (ELit l, mark)
| EAbs (binder, typs) ->
let vars, body = Bindlib.unmbind binder in
let new_body = rec_helper body in
let new_binder = Bindlib.bind_mvar vars new_body in
Bindlib.box_apply (fun binder -> EAbs (binder, typs), pos) new_binder
Bindlib.box_apply (fun binder -> EAbs (binder, typs), mark) new_binder
| EApp (f, args) ->
Bindlib.box_apply2
(fun f args ->
@ -106,11 +106,11 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : 'm expr) :
| EAbs (binder, _ts) ->
(* beta reduction *)
Bindlib.msubst binder (List.map fst args |> Array.of_list)
| _ -> EApp (f, args), pos)
| _ -> EApp (f, args), mark)
(rec_helper f)
(List.map rec_helper args |> Bindlib.box_list)
| EAssert e1 -> Bindlib.box_apply (fun e1 -> EAssert e1, pos) (rec_helper e1)
| EOp op -> Bindlib.box (EOp op, pos)
| EAssert e1 -> Bindlib.box_apply (fun e1 -> EAssert e1, mark) (rec_helper e1)
| EOp op -> Bindlib.box (EOp op, mark)
| EDefault (exceptions, just, cons) ->
Bindlib.box_apply3
(fun exceptions just cons ->
@ -135,7 +135,7 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : 'm expr) :
feed the expression to the interpreter that will print the
beautiful right error message *)
Interpreter.evaluate_expr ctx.decl_ctx
(EDefault (exceptions, just, cons), pos)
(EDefault (exceptions, just, cons), mark)
| [except], _, _ when Expr.is_value except ->
(* if there is only one exception and it is a non-empty value it is
always chosen *)
@ -151,15 +151,15 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : 'm expr) :
| EApp ((EOp (Unop (Log _)), _), [(ELit (LBool false), _)]) ),
_ ),
_ ) ->
ELit LEmptyError, pos
ELit LEmptyError, mark
| [], just, cons when not !Cli.avoid_exceptions_flag ->
(* without exceptions, a default is just an [if then else] raising an
error in the else case. This exception is only valid in the context
of compilation_with_exceptions, so we desactivate with a global
flag to know if we will be compiling using exceptions or the option
monad. *)
EIfThenElse (just, cons, (ELit LEmptyError, pos)), pos
| exceptions, just, cons -> EDefault (exceptions, just, cons), pos)
EIfThenElse (just, cons, (ELit LEmptyError, mark)), mark
| exceptions, just, cons -> EDefault (exceptions, just, cons), mark)
(List.map rec_helper exceptions |> Bindlib.box_list)
(rec_helper just) (rec_helper cons)
| EIfThenElse (e1, e2, e3) ->
@ -179,10 +179,10 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : 'm expr) :
| EApp ((EOp (Unop (Log _)), _), [(ELit (LBool false), _)]) ) ) ->
e1
| _ when Expr.equal e2 e3 -> e2
| _ -> EIfThenElse (e1, e2, e3), pos)
| _ -> EIfThenElse (e1, e2, e3), mark)
(rec_helper e1) (rec_helper e2) (rec_helper e3)
| ErrorOnEmpty e1 ->
Bindlib.box_apply (fun e1 -> ErrorOnEmpty e1, pos) (rec_helper e1)
Bindlib.box_apply (fun e1 -> ErrorOnEmpty e1, mark) (rec_helper e1)
let optimize_expr (decl_ctx : decl_ctx) (e : 'm expr) =
partial_evaluation { var_values = Var.Map.empty; decl_ctx } e
@ -248,9 +248,8 @@ let program_map
(fun new_scopes -> { p with scopes = new_scopes })
(scopes_map t ctx p.scopes)
let optimize_program (p : 'm program) : untyped program =
let optimize_program (p : 'm program) : 'm program =
Bindlib.unbox
(program_map partial_evaluation
{ var_values = Var.Map.empty; decl_ctx = p.decl_ctx }
p)
|> Program.untype

2
compiler/dcalc/optimizations.mli
View File

@ -21,4 +21,4 @@ open Shared_ast
open Ast
val optimize_expr : decl_ctx -> 'm expr -> 'm expr Bindlib.box
val optimize_program : 'm program -> untyped program
val optimize_program : 'm program -> 'm program

31
compiler/dcalc/typing.mli
View File

@ -1,31 +0,0 @@
(* This file is part of the Catala compiler, a specification language for tax
and social benefits computation rules. Copyright (C) 2020 Inria, contributor:
Denis Merigoux <denis.merigoux@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. *)
(** Typing for the default calculus. Because of the error terms, we perform type
inference using the classical W algorithm with union-find unification. *)
open Shared_ast
val infer_types : decl_ctx -> untyped Ast.expr -> typed Ast.expr Bindlib.box
(** Infers types everywhere on the given expression, and adds (or replaces) type
annotations on each node *)
val infer_type : decl_ctx -> 'm Ast.expr -> typ
(** Gets the outer type of the given expression, using either the existing
annotations or inference *)
val check_type : decl_ctx -> 'm Ast.expr -> typ -> unit
val infer_types_program : untyped Ast.program -> typed Ast.program

27
compiler/desugared/ast.ml
View File

@ -40,7 +40,7 @@ module LabelSet : Set.S with type elt = LabelName.t = Set.Make (LabelName)
module ScopeDef = struct
type t =
| Var of ScopeVar.t * StateName.t option
| SubScopeVar of SubScopeName.t * ScopeVar.t
| SubScopeVar of SubScopeName.t * ScopeVar.t * Pos.t
(** In this case, the [ScopeVar.t] lives inside the context of the
subscope's original declaration *)
@ -49,13 +49,13 @@ module ScopeDef = struct
| Var (x, None), Var (y, None)
| Var (x, Some _), Var (y, None)
| Var (x, None), Var (y, Some _)
| Var (x, _), SubScopeVar (_, y)
| SubScopeVar (_, x), Var (y, _) ->
| Var (x, _), SubScopeVar (_, y, _)
| SubScopeVar (_, x, _), Var (y, _) ->
ScopeVar.compare x y
| Var (x, Some sx), Var (y, Some sy) ->
let cmp = ScopeVar.compare x y in
if cmp = 0 then StateName.compare sx sy else cmp
| SubScopeVar (x', x), SubScopeVar (y', y) ->
| SubScopeVar (x', x, _), SubScopeVar (y', y, _) ->
let cmp = SubScopeName.compare x' y' in
if cmp = 0 then ScopeVar.compare x y else cmp
@ -63,21 +63,22 @@ module ScopeDef = struct
match x with
| Var (x, None) -> Marked.get_mark (ScopeVar.get_info x)
| Var (_, Some sx) -> Marked.get_mark (StateName.get_info sx)
| SubScopeVar (x, _) -> Marked.get_mark (SubScopeName.get_info x)
| SubScopeVar (_, _, pos) -> pos
let format_t fmt x =
match x with
| Var (v, None) -> ScopeVar.format_t fmt v
| Var (v, Some sv) ->
Format.fprintf fmt "%a.%a" ScopeVar.format_t v StateName.format_t sv
| SubScopeVar (s, v) ->
| SubScopeVar (s, v, _) ->
Format.fprintf fmt "%a.%a" SubScopeName.format_t s ScopeVar.format_t v
let hash x =
match x with
| Var (v, None) -> ScopeVar.hash v
| Var (v, Some sv) -> Int.logxor (ScopeVar.hash v) (StateName.hash sv)
| SubScopeVar (w, v) -> Int.logxor (SubScopeName.hash w) (ScopeVar.hash v)
| SubScopeVar (w, v, _) ->
Int.logxor (SubScopeName.hash w) (ScopeVar.hash v)
end
module ScopeDefMap : Map.S with type key = ScopeDef.t = Map.Make (ScopeDef)
@ -198,17 +199,14 @@ type var_or_states = WholeVar | States of StateName.t list
type scope = {
scope_vars : var_or_states ScopeVarMap.t;
scope_sub_scopes : ScopeName.t Scopelang.Ast.SubScopeMap.t;
scope_sub_scopes : ScopeName.t SubScopeMap.t;
scope_uid : ScopeName.t;
scope_defs : scope_def ScopeDefMap.t;
scope_assertions : assertion list;
scope_meta_assertions : meta_assertion list;
}
type program = {
program_scopes : scope Scopelang.Ast.ScopeMap.t;
program_ctx : decl_ctx;
}
type program = { program_scopes : scope ScopeMap.t; program_ctx : decl_ctx }
let rec locations_used (e : expr) : LocationSet.t =
match Marked.unmark e with
@ -254,7 +252,10 @@ let free_variables (def : rule RuleMap.t) : Pos.t ScopeDefMap.t =
(match loc with
| DesugaredScopeVar (v, st) -> ScopeDef.Var (Marked.unmark v, st)
| SubScopeVar (_, sub_index, sub_var) ->
ScopeDef.SubScopeVar (Marked.unmark sub_index, Marked.unmark sub_var))
ScopeDef.SubScopeVar
( Marked.unmark sub_index,
Marked.unmark sub_var,
Marked.get_mark sub_index ))
loc_pos acc)
locs acc
in

9
compiler/desugared/ast.mli
View File

@ -34,7 +34,7 @@ module LabelSet : Set.S with type elt = LabelName.t
module ScopeDef : sig
type t =
| Var of ScopeVar.t * StateName.t option
| SubScopeVar of SubScopeName.t * ScopeVar.t
| SubScopeVar of SubScopeName.t * ScopeVar.t * Pos.t
val compare : t -> t -> int
val get_position : t -> Pos.t
@ -99,17 +99,14 @@ type var_or_states = WholeVar | States of StateName.t list
type scope = {
scope_vars : var_or_states ScopeVarMap.t;
scope_sub_scopes : ScopeName.t Scopelang.Ast.SubScopeMap.t;
scope_sub_scopes : ScopeName.t SubScopeMap.t;
scope_uid : ScopeName.t;
scope_defs : scope_def ScopeDefMap.t;
scope_assertions : assertion list;
scope_meta_assertions : meta_assertion list;
}
type program = {
program_scopes : scope Scopelang.Ast.ScopeMap.t;
program_ctx : decl_ctx;
}
type program = { program_scopes : scope ScopeMap.t; program_ctx : decl_ctx }
(** {1 Helpers} *)

10
compiler/desugared/dependency.ml
View File

@ -155,7 +155,7 @@ let build_scope_dependencies (scope : Ast.scope) : ScopeDependencies.t =
scope.scope_vars g
in
let g =
Scopelang.Ast.SubScopeMap.fold
SubScopeMap.fold
(fun (v : SubScopeName.t) _ g ->
ScopeDependencies.add_vertex g (Vertex.SubScope v))
scope.scope_sub_scopes g
@ -185,7 +185,7 @@ let build_scope_dependencies (scope : Ast.scope) : ScopeDependencies.t =
(Vertex.Var (v_defined, s_defined))
in
ScopeDependencies.add_edge_e g edge
| ( Ast.ScopeDef.SubScopeVar (defined, _),
| ( Ast.ScopeDef.SubScopeVar (defined, _, _),
Ast.ScopeDef.Var (v_used, s_used) ) ->
(* here we are defining the input of a subscope using a var of the
scope *)
@ -195,8 +195,8 @@ let build_scope_dependencies (scope : Ast.scope) : ScopeDependencies.t =
fv_def_pos (Vertex.SubScope defined)
in
ScopeDependencies.add_edge_e g edge
| ( Ast.ScopeDef.SubScopeVar (defined, _),
Ast.ScopeDef.SubScopeVar (used, _) ) ->
| ( Ast.ScopeDef.SubScopeVar (defined, _, _),
Ast.ScopeDef.SubScopeVar (used, _, _) ) ->
(* here we are defining the input of a scope with the output of
another subscope *)
if used = defined then
@ -212,7 +212,7 @@ let build_scope_dependencies (scope : Ast.scope) : ScopeDependencies.t =
in
ScopeDependencies.add_edge_e g edge
| ( Ast.ScopeDef.Var (v_defined, s_defined),
Ast.ScopeDef.SubScopeVar (used, _) ) ->
Ast.ScopeDef.SubScopeVar (used, _, _) ) ->
(* finally we define a scope var with the output of a subscope *)
let edge =
ScopeDependencies.E.create (Vertex.SubScope used) fv_def_pos

63
compiler/desugared/desugared_to_scope.ml
View File

@ -27,18 +27,18 @@ type target_scope_vars =
type ctx = {
scope_var_mapping : target_scope_vars ScopeVarMap.t;
var_mapping : (Ast.expr, Scopelang.Ast.expr Var.t) Var.Map.t;
var_mapping : (Ast.expr, untyped Scopelang.Ast.expr Var.t) Var.Map.t;
}
let tag_with_log_entry
(e : Scopelang.Ast.expr)
(e : untyped Scopelang.Ast.expr)
(l : log_entry)
(markings : Utils.Uid.MarkedString.info list) : Scopelang.Ast.expr =
(markings : Utils.Uid.MarkedString.info list) : untyped Scopelang.Ast.expr =
( EApp ((EOp (Unop (Log (l, markings))), Marked.get_mark e), [e]),
Marked.get_mark e )
let rec translate_expr (ctx : ctx) (e : Ast.expr) :
Scopelang.Ast.expr Bindlib.box =
untyped Scopelang.Ast.expr Bindlib.box =
let m = Marked.get_mark e in
match Marked.unmark e with
| ELocation (SubScopeVar (s_name, ss_name, s_var)) ->
@ -186,7 +186,7 @@ let rec rule_tree_to_expr
(ctx : ctx)
(def_pos : Pos.t)
(is_func : Ast.expr Var.t option)
(tree : rule_tree) : Scopelang.Ast.expr Bindlib.box =
(tree : rule_tree) : untyped Scopelang.Ast.expr Bindlib.box =
let emark = Untyped { pos = def_pos } in
let exceptions, base_rules =
match tree with Leaf r -> [], r | Node (exceptions, r) -> exceptions, r
@ -236,7 +236,7 @@ let rec rule_tree_to_expr
base_rules
in
let translate_and_unbox_list (list : Ast.expr Bindlib.box list) :
Scopelang.Ast.expr Bindlib.box list =
untyped Scopelang.Ast.expr Bindlib.box list =
List.map
(fun e ->
(* There are two levels of boxing here, the outermost is introduced by
@ -283,12 +283,13 @@ let rec rule_tree_to_expr
that the result returned by the function is not empty *)
let default =
Bindlib.box_apply
(fun (default : Scopelang.Ast.expr) -> ErrorOnEmpty default, emark)
(fun (default : untyped Scopelang.Ast.expr) ->
ErrorOnEmpty default, emark)
default
in
Expr.make_abs
[| Var.Map.find new_param ctx.var_mapping |]
default [typ] emark
default [typ] def_pos
else default
| _ -> (* should not happen *) assert false
@ -303,7 +304,7 @@ let translate_def
(typ : typ)
(io : Scopelang.Ast.io)
~(is_cond : bool)
~(is_subscope_var : bool) : Scopelang.Ast.expr =
~(is_subscope_var : bool) : untyped Scopelang.Ast.expr =
(* Here, we have to transform this list of rules into a default tree. *)
let is_def_func =
match Marked.unmark typ with TArrow (_, _) -> true | _ -> false
@ -411,7 +412,8 @@ let translate_def
[Ast.empty_rule (Marked.get_mark typ) is_def_func_param_typ] )))
(** Translates a scope *)
let translate_scope (ctx : ctx) (scope : Ast.scope) : Scopelang.Ast.scope_decl =
let translate_scope (ctx : ctx) (scope : Ast.scope) :
untyped Scopelang.Ast.scope_decl =
let scope_dependencies = Dependency.build_scope_dependencies scope in
Dependency.check_for_cycle scope scope_dependencies;
let scope_ordering =
@ -475,15 +477,14 @@ let translate_scope (ctx : ctx) (scope : Ast.scope) : Scopelang.Ast.scope_decl =
(* Before calling the sub_scope, we need to include all the
re-definitions of subscope parameters*)
let sub_scope =
Scopelang.Ast.SubScopeMap.find sub_scope_index
scope.scope_sub_scopes
SubScopeMap.find sub_scope_index scope.scope_sub_scopes
in
let sub_scope_vars_redefs_candidates =
Ast.ScopeDefMap.filter
(fun def_key scope_def ->
match def_key with
| Ast.ScopeDef.Var _ -> false
| Ast.ScopeDef.SubScopeVar (sub_scope_index', _) ->
| Ast.ScopeDef.SubScopeVar (sub_scope_index', _, _) ->
sub_scope_index = sub_scope_index'
(* We exclude subscope variables that have 0 re-definitions
and are not visible in the input of the subscope *)
@ -504,7 +505,7 @@ let translate_scope (ctx : ctx) (scope : Ast.scope) : Scopelang.Ast.scope_decl =
let is_cond = scope_def.scope_def_is_condition in
match def_key with
| Ast.ScopeDef.Var _ -> assert false (* should not happen *)
| Ast.ScopeDef.SubScopeVar (_, sub_scope_var) ->
| Ast.ScopeDef.SubScopeVar (sscope, sub_scope_var, pos) ->
(* This definition redefines a variable of the correct
subscope. But we have to check that this redefinition is
allowed with respect to the io parameters of that
@ -515,7 +516,7 @@ let translate_scope (ctx : ctx) (scope : Ast.scope) : Scopelang.Ast.scope_decl =
| Scopelang.Ast.NoInput ->
Errors.raise_multispanned_error
(( Some "Incriminated subscope:",
Ast.ScopeDef.get_position def_key )
Marked.get_mark (SubScopeName.get_info sscope) )
:: ( Some "Incriminated variable:",
Marked.get_mark (ScopeVar.get_info sub_scope_var)
)
@ -533,9 +534,8 @@ let translate_scope (ctx : ctx) (scope : Ast.scope) : Scopelang.Ast.scope_decl =
Errors.raise_multispanned_error
[
( Some "Incriminated subscope:",
Ast.ScopeDef.get_position def_key );
( Some "Incriminated variable:",
Marked.get_mark (ScopeVar.get_info sub_scope_var) );
Marked.get_mark (SubScopeName.get_info sscope) );
Some "Incriminated variable:", pos;
]
"This subscope variable is a mandatory input but no \
definition was provided."
@ -548,12 +548,9 @@ let translate_scope (ctx : ctx) (scope : Ast.scope) : Scopelang.Ast.scope_decl =
~is_subscope_var:true
in
let subscop_real_name =
Scopelang.Ast.SubScopeMap.find sub_scope_index
scope.scope_sub_scopes
in
let var_pos =
Marked.get_mark (ScopeVar.get_info sub_scope_var)
SubScopeMap.find sub_scope_index scope.scope_sub_scopes
in
let var_pos = Ast.ScopeDef.get_position def_key in
Scopelang.Ast.Definition
( ( SubScopeVar
( subscop_real_name,
@ -578,7 +575,17 @@ let translate_scope (ctx : ctx) (scope : Ast.scope) : Scopelang.Ast.scope_decl =
List.map snd (Ast.ScopeDefMap.bindings sub_scope_vars_redefs)
in
sub_scope_vars_redefs
@ [Scopelang.Ast.Call (sub_scope, sub_scope_index)])
@ [
Scopelang.Ast.Call
( sub_scope,
sub_scope_index,
Untyped
{
pos =
Marked.get_mark
(SubScopeName.get_info sub_scope_index);
} );
])
scope_ordering)
in
(* Then, after having computed all the scopes variables, we add the
@ -630,20 +637,22 @@ let translate_scope (ctx : ctx) (scope : Ast.scope) : Scopelang.Ast.scope_decl =
acc states)
scope.scope_vars ScopeVarMap.empty
in
let pos = Marked.get_mark (ScopeName.get_info scope.scope_uid) in
{
Scopelang.Ast.scope_decl_name = scope.scope_uid;
Scopelang.Ast.scope_decl_rules;
Scopelang.Ast.scope_sig;
Scopelang.Ast.scope_mark = Untyped { pos };
}
(** {1 API} *)
let translate_program (pgrm : Ast.program) : Scopelang.Ast.program =
let translate_program (pgrm : Ast.program) : untyped Scopelang.Ast.program =
(* First we give mappings to all the locations between Desugared and
Scopelang. This involves creating a new Scopelang scope variable for every
state of a Desugared variable. *)
let ctx =
Scopelang.Ast.ScopeMap.fold
ScopeMap.fold
(fun _scope scope_decl ctx ->
ScopeVarMap.fold
(fun scope_var (states : Ast.var_or_states) ctx ->
@ -682,6 +691,6 @@ let translate_program (pgrm : Ast.program) : Scopelang.Ast.program =
in
{
Scopelang.Ast.program_scopes =
Scopelang.Ast.ScopeMap.map (translate_scope ctx) pgrm.program_scopes;
ScopeMap.map (translate_scope ctx) pgrm.program_scopes;
Scopelang.Ast.program_ctx = pgrm.program_ctx;
}

2
compiler/desugared/desugared_to_scope.mli
View File

@ -16,4 +16,4 @@
(** Translation from {!module: Desugared.Ast} to {!module: Scopelang.Ast} *)
val translate_program : Ast.program -> Scopelang.Ast.program
val translate_program : Ast.program -> Shared_ast.untyped Scopelang.Ast.program

36
compiler/driver.ml
View File

@ -171,18 +171,21 @@ let driver source_file (options : Cli.options) : int =
if Option.is_some options.ex_scope then
Format.fprintf fmt "%a\n"
(Scopelang.Print.scope prgm.program_ctx ~debug:options.debug)
( scope_uid,
Scopelang.Ast.ScopeMap.find scope_uid prgm.program_scopes )
(scope_uid, Shared_ast.ScopeMap.find scope_uid prgm.program_scopes)
else
Format.fprintf fmt "%a\n"
(Scopelang.Print.program ~debug:options.debug)
prgm
| ( `Interpret | `Typecheck | `OCaml | `Python | `Scalc | `Lcalc | `Dcalc
| `Proof | `Plugin _ ) as backend -> (
Cli.debug_print "Translating to default calculus...";
let prgm, type_ordering =
Scopelang.Scope_to_dcalc.translate_program prgm
Cli.debug_print "Typechecking...";
let type_ordering =
Scopelang.Dependency.check_type_cycles prgm.program_ctx.ctx_structs
prgm.program_ctx.ctx_enums
in
let prgm = Scopelang.Ast.type_program prgm in
Cli.debug_print "Translating to default calculus...";
let prgm = Scopelang.Scope_to_dcalc.translate_program prgm in
let prgm =
if options.optimize then begin
Cli.debug_print "Optimizing default calculus...";
@ -191,6 +194,9 @@ let driver source_file (options : Cli.options) : int =
else prgm
in
match backend with
| `Typecheck ->
(* That's it! *)
Cli.result_print "Typechecking successful!"
| `Dcalc ->
let _output_file, with_output = get_output_format () in
with_output
@ -216,16 +222,22 @@ let driver source_file (options : Cli.options) : int =
Format.fprintf fmt "%a\n"
(Shared_ast.Expr.format prgm.decl_ctx)
prgrm_dcalc_expr
| ( `Interpret | `Typecheck | `OCaml | `Python | `Scalc | `Lcalc
| `Proof | `Plugin _ ) as backend -> (
Cli.debug_print "Typechecking...";
let prgm = Dcalc.Typing.infer_types_program prgm in
| (`Interpret | `OCaml | `Python | `Scalc | `Lcalc | `Proof | `Plugin _)
as backend -> (
Cli.debug_print "Typechecking again...";
let prgm =
try Shared_ast.Typing.program prgm
with Errors.StructuredError (msg, details) ->
let msg =
"Typing error occured during re-typing on the 'default \
calculus'. This is a bug in the Catala compiler.\n"
^ msg
in
raise (Errors.StructuredError (msg, details))
in
(* Cli.debug_print (Format.asprintf "Typechecking results :@\n%a"
(Print.typ prgm.decl_ctx) typ); *)
match backend with
| `Typecheck ->
(* That's it! *)
Cli.result_print "Typechecking successful!"
| `Proof ->
let vcs =
Verification.Conditions.generate_verification_conditions prgm

10
compiler/lcalc/ast.ml
View File

@ -39,9 +39,7 @@ let make_none m =
Bindlib.box
@@ mark
@@ EInj
( Marked.mark
(Expr.map_mark (fun pos -> pos) (fun _ -> tunit) m)
(ELit LUnit),
( Marked.mark (Expr.with_ty m tunit) (ELit LUnit),
0,
option_enum,
[TLit TUnit, Pos.no_pos; TAny, Pos.no_pos] )
@ -74,12 +72,12 @@ let make_matchopt_with_abs_arms arg e_none e_some =
[match arg with | None () -> e_none | Some v -> e_some]. It binds v to
e_some, permitting it to be used inside the expression. There is no
requirements on the form of both e_some and e_none. *)
let make_matchopt m v tau arg e_none e_some =
let make_matchopt pos v tau arg e_none e_some =
let x = Var.make "_" in
make_matchopt_with_abs_arms arg
(Expr.make_abs [| x |] e_none [TLit TUnit, Expr.mark_pos m] m)
(Expr.make_abs [| v |] e_some [tau] m)
(Expr.make_abs [| x |] e_none [TLit TUnit, pos] pos)
(Expr.make_abs [| v |] e_some [tau] pos)
let handle_default = Var.make "handle_default"
let handle_default_opt = Var.make "handle_default_opt"

2
compiler/lcalc/ast.mli
View File

@ -43,7 +43,7 @@ val make_matchopt_with_abs_arms :
'm expr Bindlib.box
val make_matchopt :
'm mark ->
Utils.Pos.t ->
'm expr Var.t ->
typ ->
'm expr Bindlib.box ->

2
compiler/lcalc/closure_conversion.ml
View File

@ -162,7 +162,7 @@ let closure_conversion_expr (type m) (ctx : m ctx) (e : m expr) :
(Array.concat [Array.make 1 inner_c_var; vars])
new_closure_body
((TAny, binder_pos) :: typs)
(Marked.get_mark e)
(Expr.pos e)
in
( Expr.make_let_in code_var
(TAny, Expr.pos e)

22
compiler/lcalc/compile_with_exceptions.ml
View File

@ -23,10 +23,11 @@ type 'm ctx = ('m D.expr, 'm A.expr Var.t) Var.Map.t
(** This environment contains a mapping between the variables in Dcalc and their
correspondance in Lcalc. *)
let thunk_expr (e : 'm A.expr Bindlib.box) (mark : 'm mark) :
'm A.expr Bindlib.box =
let thunk_expr (type m) (e : m A.expr Bindlib.box) : m A.expr Bindlib.box =
let dummy_var = Var.make "_" in
Expr.make_abs [| dummy_var |] e [TAny, Expr.mark_pos mark] mark
let pos = Expr.pos (Bindlib.unbox e) in
let arg_t = Marked.mark pos (TLit TUnit) in
Expr.make_abs [| dummy_var |] e [arg_t] pos
let rec translate_default
(ctx : 'm ctx)
@ -35,19 +36,20 @@ let rec translate_default
(cons : 'm D.expr)
(mark_default : 'm mark) : 'm A.expr Bindlib.box =
let exceptions =
List.map
(fun except -> thunk_expr (translate_expr ctx except) mark_default)
exceptions
List.map (fun except -> thunk_expr (translate_expr ctx except)) exceptions
in
let pos = Expr.mark_pos mark_default in
let exceptions =
Expr.make_app
(Expr.make_var (Var.translate A.handle_default, mark_default))
(Expr.make_var
( Var.translate A.handle_default,
Expr.with_ty mark_default (Utils.Marked.mark pos TAny) ))
[
Expr.earray exceptions mark_default;
thunk_expr (translate_expr ctx just) mark_default;
thunk_expr (translate_expr ctx cons) mark_default;
thunk_expr (translate_expr ctx just);
thunk_expr (translate_expr ctx cons);
]
mark_default
pos
in
exceptions

89
compiler/lcalc/compile_without_exceptions.ml
View File

@ -43,11 +43,10 @@ module A = Ast
open Shared_ast
type 'm hoists = ('m A.expr, 'm D.expr) Var.Map.t
(** Hoists definition. It represent bindings between [A.Var.t] and
[D.naked_expr]. *)
(** Hoists definition. It represent bindings between [A.Var.t] and [D.expr]. *)
type 'm info = {
naked_expr : 'm A.expr Bindlib.box;
expr : 'm A.expr Bindlib.box;
var : 'm A.expr Var.t;
is_pure : bool;
}
@ -104,7 +103,7 @@ let add_var
(is_pure : bool)
(ctx : 'm ctx) : 'm ctx =
let new_var = Var.make (Bindlib.name_of var) in
let naked_expr = Expr.make_var (new_var, mark) in
let expr = Expr.make_var (new_var, mark) in
(* Cli.debug_print @@ Format.asprintf "D.%a |-> A.%a" Print.var var Print.var
new_var; *)
@ -112,7 +111,7 @@ let add_var
ctx with
vars =
Var.Map.update var
(fun _ -> Some { naked_expr; var = new_var; is_pure })
(fun _ -> Some { expr; var = new_var; is_pure })
ctx.vars;
}
@ -158,7 +157,8 @@ let disjoint_union_maps (pos : Pos.t) (cs : ('e, 'a) Var.Map.t list) :
hoists, has the non-empty value in e_v. *)
let rec translate_and_hoist (ctx : 'm ctx) (e : 'm D.expr) :
'm A.expr Bindlib.box * 'm hoists =
let pos = Marked.get_mark e in
let mark = Marked.get_mark e in
let pos = Expr.mark_pos mark in
match Marked.unmark e with
(* empty-producing/using terms. We hoist those. (D.EVar in some cases,
EApp(D.EVar _, [ELit LUnit]), EDefault _, ELit LEmptyDefault) I'm unsure
@ -172,23 +172,23 @@ let rec translate_and_hoist (ctx : 'm ctx) (e : 'm D.expr) :
let v' = Var.make (Bindlib.name_of v) in
(* Cli.debug_print @@ Format.asprintf "Found an unpure variable %a,
created a variable %a to replace it" Print.var v Print.var v'; *)
Expr.make_var (v', pos), Var.Map.singleton v' e
else (find ~info:"should never happen" v ctx).naked_expr, Var.Map.empty
Expr.make_var (v', mark), Var.Map.singleton v' e
else (find ~info:"should never happen" v ctx).expr, Var.Map.empty
| EApp ((EVar v, p), [(ELit LUnit, _)]) ->
if not (find ~info:"search for a variable" v ctx).is_pure then
let v' = Var.make (Bindlib.name_of v) in
(* Cli.debug_print @@ Format.asprintf "Found an unpure variable %a,
created a variable %a to replace it" Print.var v Print.var v'; *)
Expr.make_var (v', pos), Var.Map.singleton v' (EVar v, p)
Expr.make_var (v', mark), Var.Map.singleton v' (EVar v, p)
else
Errors.raise_spanned_error (Expr.pos e)
"Internal error: an pure variable was found in an unpure environment."
| EDefault (_exceptions, _just, _cons) ->
let v' = Var.make "default_term" in
Expr.make_var (v', pos), Var.Map.singleton v' e
Expr.make_var (v', mark), Var.Map.singleton v' e
| ELit LEmptyError ->
let v' = Var.make "empty_litteral" in
Expr.make_var (v', pos), Var.Map.singleton v' e
Expr.make_var (v', mark), Var.Map.singleton v' e
(* This one is a very special case. It transform an unpure expression
environement to a pure expression. *)
| ErrorOnEmpty arg ->
@ -197,25 +197,25 @@ let rec translate_and_hoist (ctx : 'm ctx) (e : 'm D.expr) :
let x = Var.make "non_empty_argument" in
let arg' = translate_expr ctx arg in
let rty = Expr.maybe_ty mark in
( A.make_matchopt_with_abs_arms arg'
(Expr.make_abs [| silent_var |]
(Bindlib.box (ERaise NoValueProvided, pos))
[TAny, Expr.pos e]
pos)
(Expr.make_abs [| x |] (Expr.make_var (x, pos)) [TAny, Expr.pos e] pos),
(Bindlib.box (ERaise NoValueProvided, Expr.with_ty mark rty))
[rty] pos)
(Expr.make_abs [| x |] (Expr.make_var (x, mark)) [rty] pos),
Var.Map.empty )
(* pure terms *)
| ELit
((LBool _ | LInt _ | LRat _ | LMoney _ | LUnit | LDate _ | LDuration _) as
l) ->
Expr.elit l pos, Var.Map.empty
Expr.elit l mark, Var.Map.empty
| EIfThenElse (e1, e2, e3) ->
let e1', h1 = translate_and_hoist ctx e1 in
let e2', h2 = translate_and_hoist ctx e2 in
let e3', h3 = translate_and_hoist ctx e3 in
let e' = Expr.eifthenelse e1' e2' e3' pos in
let e' = Expr.eifthenelse e1' e2' e3' mark in
(*(* equivalent code : *) let e' = let+ e1' = e1' and+ e2' = e2' and+ e3' =
e3' in (A.EIfThenElse (e1', e2', e3'), pos) in *)
@ -224,7 +224,7 @@ let rec translate_and_hoist (ctx : 'm ctx) (e : 'm D.expr) :
(* same behavior as in the ICFP paper: if e1 is empty, then no error is
raised. *)
let e1', h1 = translate_and_hoist ctx e1 in
Expr.eassert e1' pos, h1
Expr.eassert e1' mark, h1
| EAbs (binder, ts) ->
let vars, body = Bindlib.unmbind binder in
let ctx, lc_vars =
@ -235,7 +235,7 @@ let rec translate_and_hoist (ctx : 'm ctx) (e : 'm D.expr) :
The code should behave correctly in the without this assumption if
we put here an is_pure=false, but the types are more compilcated.
(unimplemented for now) *)
let ctx = add_var pos var true ctx in
let ctx = add_var mark var true ctx in
let lc_var = (find var ctx).var in
ctx, lc_var :: lc_vars)
in
@ -247,7 +247,7 @@ let rec translate_and_hoist (ctx : 'm ctx) (e : 'm D.expr) :
let new_binder = Bindlib.bind_mvar lc_vars new_body in
( Bindlib.box_apply
(fun new_binder -> EAbs (new_binder, List.map translate_typ ts), pos)
(fun new_binder -> EAbs (new_binder, List.map translate_typ ts), mark)
new_binder,
hoists )
| EApp (e1, args) ->
@ -257,7 +257,7 @@ let rec translate_and_hoist (ctx : 'm ctx) (e : 'm D.expr) :
in
let hoists = disjoint_union_maps (Expr.pos e) (h1 :: h_args) in
let e' = Expr.eapp e1' args' pos in
let e' = Expr.eapp e1' args' mark in
e', hoists
| ETuple (args, s) ->
let args', h_args =
@ -265,14 +265,14 @@ let rec translate_and_hoist (ctx : 'm ctx) (e : 'm D.expr) :
in
let hoists = disjoint_union_maps (Expr.pos e) h_args in
Expr.etuple args' s pos, hoists
Expr.etuple args' s mark, hoists
| ETupleAccess (e1, i, s, ts) ->
let e1', hoists = translate_and_hoist ctx e1 in
let e1' = Expr.etupleaccess e1' i s ts pos in
let e1' = Expr.etupleaccess e1' i s ts mark in
e1', hoists
| EInj (e1, i, en, ts) ->
let e1', hoists = translate_and_hoist ctx e1 in
let e1' = Expr.einj e1' i en ts pos in
let e1' = Expr.einj e1' i en ts mark in
e1', hoists
| EMatch (e1, cases, en) ->
let e1', h1 = translate_and_hoist ctx e1 in
@ -281,13 +281,13 @@ let rec translate_and_hoist (ctx : 'm ctx) (e : 'm D.expr) :
in
let hoists = disjoint_union_maps (Expr.pos e) (h1 :: h_cases) in
let e' = Expr.ematch e1' cases' en pos in
let e' = Expr.ematch e1' cases' en mark in
e', hoists
| EArray es ->
let es', hoists = es |> List.map (translate_and_hoist ctx) |> List.split in
Expr.earray es' pos, disjoint_union_maps (Expr.pos e) hoists
| EOp op -> Bindlib.box (EOp op, pos), Var.Map.empty
Expr.earray es' mark, disjoint_union_maps (Expr.pos e) hoists
| EOp op -> Bindlib.box (EOp op, mark), Var.Map.empty
and translate_expr ?(append_esome = true) (ctx : 'm ctx) (e : 'm D.expr) :
'm A.expr Bindlib.box =
@ -303,11 +303,12 @@ and translate_expr ?(append_esome = true) (ctx : 'm ctx) (e : 'm D.expr) :
~init:(if append_esome then A.make_some e' else e')
~f:(fun acc (v, (hoist, mark_hoist)) ->
(* Cli.debug_print @@ Format.asprintf "hoist using A.%a" Print.var v; *)
let pos = Expr.mark_pos mark_hoist in
let c' : 'm A.expr Bindlib.box =
match hoist with
(* Here we have to handle only the cases appearing in hoists, as defined
the [translate_and_hoist] function. *)
| EVar v -> (find ~info:"should never happen" v ctx).naked_expr
| EVar v -> (find ~info:"should never happen" v ctx).expr
| EDefault (excep, just, cons) ->
let excep' = List.map (translate_expr ctx) excep in
let just' = translate_expr ctx just in
@ -322,7 +323,7 @@ and translate_expr ?(append_esome = true) (ctx : 'm ctx) (e : 'm D.expr) :
just';
cons';
]
mark_hoist
pos
| ELit LEmptyError -> A.make_none mark_hoist
| EAssert arg ->
let arg' = translate_expr ctx arg in
@ -336,13 +337,13 @@ and translate_expr ?(append_esome = true) (ctx : 'm ctx) (e : 'm D.expr) :
(Expr.make_abs [| silent_var |]
(Bindlib.box (ERaise NoValueProvided, mark_hoist))
[TAny, Expr.mark_pos mark_hoist]
mark_hoist)
pos)
(Expr.make_abs [| x |]
(Bindlib.box_apply
(fun arg -> EAssert arg, mark_hoist)
(Expr.make_var (x, mark_hoist)))
[TAny, Expr.mark_pos mark_hoist]
mark_hoist)
pos)
| _ ->
Errors.raise_spanned_error (Expr.mark_pos mark_hoist)
"Internal Error: An term was found in a position where it should \
@ -353,7 +354,7 @@ and translate_expr ?(append_esome = true) (ctx : 'm ctx) (e : 'm D.expr) :
] *)
(* Cli.debug_print @@ Format.asprintf "build matchopt using %a" Print.var
v; *)
A.make_matchopt mark_hoist v
A.make_matchopt pos v
(TAny, Expr.mark_pos mark_hoist)
c' (A.make_none mark_hoist) acc)
@ -374,12 +375,12 @@ let rec translate_scope_let (ctx : 'm ctx) (lets : 'm D.expr scope_body_expr) :
} ->
(* special case : the subscope variable is thunked (context i/o). We remove
this thunking. *)
let _, naked_expr = Bindlib.unmbind binder in
let _, expr = Bindlib.unmbind binder in
let var_is_pure = true in
let var, next = Bindlib.unbind next in
(* Cli.debug_print @@ Format.asprintf "unbinding %a" Print.var var; *)
let vmark = Expr.map_mark (fun _ -> pos) (fun _ -> typ) emark in
let vmark = Expr.with_ty emark ~pos typ in
let ctx' = add_var vmark var var_is_pure ctx in
let new_var = (find ~info:"variable that was just created" var ctx').var in
let new_next = translate_scope_let ctx' next in
@ -393,13 +394,13 @@ let rec translate_scope_let (ctx : 'm ctx) (lets : 'm D.expr scope_body_expr) :
scope_let_next = new_next;
scope_let_pos = pos;
})
(translate_expr ctx ~append_esome:false naked_expr)
(translate_expr ctx ~append_esome:false expr)
(Bindlib.bind_var new_var new_next)
| ScopeLet
{
scope_let_kind = SubScopeVarDefinition;
scope_let_typ = typ;
scope_let_expr = (ErrorOnEmpty _, emark) as naked_expr;
scope_let_expr = (ErrorOnEmpty _, emark) as expr;
scope_let_next = next;
scope_let_pos = pos;
} ->
@ -407,7 +408,7 @@ let rec translate_scope_let (ctx : 'm ctx) (lets : 'm D.expr scope_body_expr) :
let var_is_pure = true in
let var, next = Bindlib.unbind next in
(* Cli.debug_print @@ Format.asprintf "unbinding %a" Print.var var; *)
let vmark = Expr.map_mark (fun _ -> pos) (fun _ -> typ) emark in
let vmark = Expr.with_ty emark ~pos typ in
let ctx' = add_var vmark var var_is_pure ctx in
let new_var = (find ~info:"variable that was just created" var ctx').var in
Bindlib.box_apply2
@ -420,25 +421,25 @@ let rec translate_scope_let (ctx : 'm ctx) (lets : 'm D.expr scope_body_expr) :
scope_let_next = new_next;
scope_let_pos = pos;
})
(translate_expr ctx ~append_esome:false naked_expr)
(translate_expr ctx ~append_esome:false expr)
(Bindlib.bind_var new_var (translate_scope_let ctx' next))
| ScopeLet
{
scope_let_kind = SubScopeVarDefinition;
scope_let_pos = pos;
scope_let_expr = naked_expr;
scope_let_expr = expr;
_;
} ->
Errors.raise_spanned_error pos
"Internal Error: found an SubScopeVarDefinition that does not satisfy \
the invariants when translating Dcalc to Lcalc without exceptions: \
@[<hov 2>%a@]"
(Expr.format ctx.decl_ctx) naked_expr
(Expr.format ctx.decl_ctx) expr
| ScopeLet
{
scope_let_kind = kind;
scope_let_typ = typ;
scope_let_expr = naked_expr;
scope_let_expr = expr;
scope_let_next = next;
scope_let_pos = pos;
} ->
@ -458,9 +459,7 @@ let rec translate_scope_let (ctx : 'm ctx) (lets : 'm D.expr scope_body_expr) :
in
let var, next = Bindlib.unbind next in
(* Cli.debug_print @@ Format.asprintf "unbinding %a" Print.var var; *)
let vmark =
Expr.map_mark (fun _ -> pos) (fun _ -> typ) (Marked.get_mark naked_expr)
in
let vmark = Expr.with_ty (Marked.get_mark expr) ~pos typ in
let ctx' = add_var vmark var var_is_pure ctx in
let new_var = (find ~info:"variable that was just created" var ctx').var in
Bindlib.box_apply2
@ -473,7 +472,7 @@ let rec translate_scope_let (ctx : 'm ctx) (lets : 'm D.expr scope_body_expr) :
scope_let_next = new_next;
scope_let_pos = pos;
})
(translate_expr ctx ~append_esome:false naked_expr)
(translate_expr ctx ~append_esome:false expr)
(Bindlib.bind_var new_var (translate_scope_let ctx' next))
let translate_scope_body

79
compiler/scopelang/ast.ml
View File

@ -16,14 +16,6 @@
open Utils
open Shared_ast
module ScopeMap : Map.S with type key = ScopeName.t = Map.Make (ScopeName)
module SubScopeNameSet : Set.S with type elt = SubScopeName.t =
Set.Make (SubScopeName)
module SubScopeMap : Map.S with type key = SubScopeName.t =
Map.Make (SubScopeName)
module StructFieldMapLift = Bindlib.Lift (StructFieldMap)
module EnumConstructorMapLift = Bindlib.Lift (EnumConstructorMap)
@ -36,15 +28,9 @@ Set.Make (struct
let compare = Expr.compare_location
end)
type expr = (scopelang, untyped mark) gexpr
type 'm expr = (scopelang, 'm mark) gexpr
module ExprMap = Map.Make (struct
type t = expr
let compare = Expr.compare
end)
let rec locations_used (e : expr) : LocationSet.t =
let rec locations_used (e : 'm expr) : LocationSet.t =
match Marked.unmark e with
| ELocation l -> LocationSet.singleton (l, Expr.pos e)
| EVar _ | ELit _ | EOp _ -> LocationSet.empty
@ -82,18 +68,63 @@ let rec locations_used (e : expr) : LocationSet.t =
type io_input = NoInput | OnlyInput | Reentrant
type io = { io_output : bool Marked.pos; io_input : io_input Marked.pos }
type rule =
| Definition of location Marked.pos * typ * io * expr
| Assertion of expr
| Call of ScopeName.t * SubScopeName.t
type 'm rule =
| Definition of location Marked.pos * typ * io * 'm expr
| Assertion of 'm expr
| Call of ScopeName.t * SubScopeName.t * 'm mark
type scope_decl = {
type 'm scope_decl = {
scope_decl_name : ScopeName.t;
scope_sig : (typ * io) ScopeVarMap.t;
scope_decl_rules : rule list;
scope_decl_rules : 'm rule list;
scope_mark : 'm mark;
}
type program = {
program_scopes : scope_decl ScopeMap.t;
type 'm program = {
program_scopes : 'm scope_decl ScopeMap.t;
program_ctx : decl_ctx;
}
let type_rule decl_ctx env = function
| Definition (loc, typ, io, expr) ->
let expr' = Typing.expr decl_ctx ~env ~typ expr in
Definition (loc, typ, io, Bindlib.unbox expr')
| Assertion expr ->
let typ = Marked.mark (Expr.pos expr) (TLit TBool) in
let expr' = Typing.expr decl_ctx ~env ~typ expr in
Assertion (Bindlib.unbox expr')
| Call (sc_name, ssc_name, m) ->
let pos = Expr.mark_pos m in
Call (sc_name, ssc_name, Typed { pos; ty = Marked.mark pos TAny })
let type_program (prg : 'm program) : typed program =
let typing_env =
ScopeMap.fold
(fun scope_name scope_decl ->
Typing.Env.add_scope scope_name
(ScopeVarMap.map fst scope_decl.scope_sig))
prg.program_scopes Typing.Env.empty
in
let program_scopes =
ScopeMap.map
(fun scope_decl ->
let typing_env =
ScopeVarMap.fold
(fun svar (typ, _) env -> Typing.Env.add_scope_var svar typ env)
scope_decl.scope_sig typing_env
in
let scope_decl_rules =
List.map
(type_rule prg.program_ctx typing_env)
scope_decl.scope_decl_rules
in
let scope_mark =
let pos =
Marked.get_mark (ScopeName.get_info scope_decl.scope_decl_name)
in
Typed { pos; ty = Marked.mark pos TAny }
in
{ scope_decl with scope_decl_rules; scope_mark })
prg.program_scopes
in
{ prg with program_scopes }

29
compiler/scopelang/ast.mli
View File

@ -21,10 +21,6 @@ open Shared_ast
(** {1 Identifiers} *)
module ScopeMap : Map.S with type key = ScopeName.t
module SubScopeNameSet : Set.S with type elt = SubScopeName.t
module SubScopeMap : Map.S with type key = SubScopeName.t
module StructFieldMapLift : sig
val lift_box :
'a Bindlib.box StructFieldMap.t -> 'a StructFieldMap.t Bindlib.box
@ -41,11 +37,9 @@ module LocationSet : Set.S with type elt = location Marked.pos
(** {1 Abstract syntax tree} *)
type expr = (scopelang, untyped mark) gexpr
type 'm expr = (scopelang, 'm mark) gexpr
module ExprMap : Map.S with type key = expr
val locations_used : expr -> LocationSet.t
val locations_used : 'm expr -> LocationSet.t
(** This type characterizes the three levels of visibility for a given scope
variable with regards to the scope's input and possible redefinitions inside
@ -68,18 +62,21 @@ type io = {
}
(** Characterization of the input/output status of a scope variable. *)
type rule =
| Definition of location Marked.pos * typ * io * expr
| Assertion of expr
| Call of ScopeName.t * SubScopeName.t
type 'm rule =
| Definition of location Marked.pos * typ * io * 'm expr
| Assertion of 'm expr
| Call of ScopeName.t * SubScopeName.t * 'm mark
type scope_decl = {
type 'm scope_decl = {
scope_decl_name : ScopeName.t;
scope_sig : (typ * io) ScopeVarMap.t;
scope_decl_rules : rule list;
scope_decl_rules : 'm rule list;
scope_mark : 'm mark;
}
type program = {
program_scopes : scope_decl ScopeMap.t;
type 'm program = {
program_scopes : 'm scope_decl ScopeMap.t;
program_ctx : decl_ctx;
}
val type_program : 'm program -> typed program

14
compiler/scopelang/dependency.ml
View File

@ -45,21 +45,21 @@ module STopologicalTraversal = Graph.Topological.Make (SDependencies)
module SSCC = Graph.Components.Make (SDependencies)
(** Tarjan's stongly connected components algorithm, provided by OCamlGraph *)
let build_program_dep_graph (prgm : Ast.program) : SDependencies.t =
let build_program_dep_graph (prgm : 'm Ast.program) : SDependencies.t =
let g = SDependencies.empty in
let g =
Ast.ScopeMap.fold
ScopeMap.fold
(fun v _ g -> SDependencies.add_vertex g v)
prgm.program_scopes g
in
Ast.ScopeMap.fold
ScopeMap.fold
(fun scope_name scope g ->
let subscopes =
List.fold_left
(fun acc r ->
match r with
| Ast.Definition _ | Ast.Assertion _ -> acc
| Ast.Call (subscope, subindex) ->
| Ast.Call (subscope, subindex, _) ->
if subscope = scope_name then
Errors.raise_spanned_error
(Marked.get_mark
@ -68,12 +68,12 @@ let build_program_dep_graph (prgm : Ast.program) : SDependencies.t =
forbidden since Catala does not provide recursion"
ScopeName.format_t scope.Ast.scope_decl_name
else
Ast.ScopeMap.add subscope
ScopeMap.add subscope
(Marked.get_mark (SubScopeName.get_info subindex))
acc)
Ast.ScopeMap.empty scope.Ast.scope_decl_rules
ScopeMap.empty scope.Ast.scope_decl_rules
in
Ast.ScopeMap.fold
ScopeMap.fold
(fun subscope pos g ->
let edge = SDependencies.E.create subscope pos scope_name in
SDependencies.add_edge_e g edge)

2
compiler/scopelang/dependency.mli
View File

@ -27,7 +27,7 @@ open Shared_ast
module SDependencies :
Graph.Sig.P with type V.t = ScopeName.t and type E.label = Pos.t
val build_program_dep_graph : Ast.program -> SDependencies.t
val build_program_dep_graph : 'm Ast.program -> SDependencies.t
val check_for_cycle_in_scope : SDependencies.t -> unit
val get_scope_ordering : SDependencies.t -> ScopeName.t list

46
compiler/scopelang/print.ml
View File

@ -21,7 +21,8 @@ open Ast
let struc
ctx
(fmt : Format.formatter)
((name, fields) : StructName.t * (StructFieldName.t * typ) list) : unit =
(name : StructName.t)
(fields : (StructFieldName.t * typ) list) : unit =
Format.fprintf fmt "%a %a %a %a@\n@[<hov 2> %a@]@\n%a" Print.keyword "type"
StructName.format_t name Print.punctuation "=" Print.punctuation "{"
(Format.pp_print_list
@ -34,7 +35,8 @@ let struc
let enum
ctx
(fmt : Format.formatter)
((name, cases) : EnumName.t * (EnumConstructor.t * typ) list) : unit =
(name : EnumName.t)
(cases : (EnumConstructor.t * typ) list) : unit =
Format.fprintf fmt "%a %a %a @\n@[<hov 2> %a@]" Print.keyword "type"
EnumName.format_t name Print.punctuation "="
(Format.pp_print_list
@ -74,7 +76,7 @@ let scope ?(debug = false) ctx fmt (name, decl) =
(Print.typ ctx) typ Print.punctuation "="
(fun fmt e ->
match Marked.unmark loc with
| SubScopeVar _ -> Print.naked_expr ctx fmt e
| SubScopeVar _ -> Print.expr ctx fmt e
| ScopelangScopeVar v -> (
match
Marked.unmark
@ -83,36 +85,36 @@ let scope ?(debug = false) ctx fmt (name, decl) =
with
| Reentrant ->
Format.fprintf fmt "%a@ %a" Print.operator
"reentrant or by default"
(Print.naked_expr ~debug ctx)
e
| _ -> Format.fprintf fmt "%a" (Print.naked_expr ~debug ctx) e))
"reentrant or by default" (Print.expr ~debug ctx) e
| _ -> Format.fprintf fmt "%a" (Print.expr ~debug ctx) e))
e
| Assertion e ->
Format.fprintf fmt "%a %a" Print.keyword "assert"
(Print.naked_expr ~debug ctx)
e
| Call (scope_name, subscope_name) ->
(Print.expr ~debug ctx) e
| Call (scope_name, subscope_name, _) ->
Format.fprintf fmt "%a %a%a%a%a" Print.keyword "call"
ScopeName.format_t scope_name Print.punctuation "["
SubScopeName.format_t subscope_name Print.punctuation "]"))
decl.scope_decl_rules
let program ?(debug : bool = false) (fmt : Format.formatter) (p : program) :
let program ?(debug : bool = false) (fmt : Format.formatter) (p : 'm program) :
unit =
let ctx = p.program_ctx in
let pp_sep fmt () =
Format.pp_print_cut fmt ();
Format.pp_print_cut fmt ()
in
Format.fprintf fmt "@[<v>%a%a%a%a%a@]"
(Format.pp_print_list ~pp_sep (struc ctx))
(StructMap.bindings ctx.ctx_structs)
(if StructMap.is_empty ctx.ctx_structs then fun _ _ -> () else pp_sep)
()
(Format.pp_print_list ~pp_sep (enum ctx))
(EnumMap.bindings ctx.ctx_enums)
(if EnumMap.is_empty ctx.ctx_enums then fun _ _ -> () else pp_sep)
()
(Format.pp_print_list ~pp_sep (scope ~debug ctx))
(ScopeMap.bindings p.program_scopes)
Format.pp_open_vbox fmt 0;
StructMap.iter
(fun n s ->
struc ctx fmt n s;
pp_sep fmt ())
ctx.ctx_structs;
EnumMap.iter
(fun n e ->
enum ctx fmt n e;
pp_sep fmt ())
ctx.ctx_enums;
Format.pp_print_list ~pp_sep (scope ~debug ctx) fmt
(ScopeMap.bindings p.program_scopes);
Format.pp_close_box fmt ()

4
compiler/scopelang/print.mli
View File

@ -18,11 +18,11 @@ val scope :
?debug:bool (** [true] for debug printing *) ->
Shared_ast.decl_ctx ->
Format.formatter ->
Shared_ast.ScopeName.t * Ast.scope_decl ->
Shared_ast.ScopeName.t * 'm Ast.scope_decl ->
unit
val program :
?debug:bool (** [true] for debug printing *) ->
Format.formatter ->
Ast.program ->
'm Ast.program ->
unit

185
compiler/scopelang/scope_to_dcalc.ml
View File

@ -23,35 +23,33 @@ type scope_var_ctx = {
scope_var_io : Ast.io;
}
type scope_sig_ctx = {
type 'm scope_sig_ctx = {
scope_sig_local_vars : scope_var_ctx list; (** List of scope variables *)
scope_sig_scope_var : untyped Dcalc.Ast.expr Var.t;
scope_sig_scope_var : 'm Dcalc.Ast.expr Var.t;
(** Var representing the scope *)
scope_sig_input_var : untyped Dcalc.Ast.expr Var.t;
scope_sig_input_var : 'm Dcalc.Ast.expr Var.t;
(** Var representing the scope input inside the scope func *)
scope_sig_input_struct : StructName.t; (** Scope input *)
scope_sig_output_struct : StructName.t; (** Scope output *)
}
type scope_sigs_ctx = scope_sig_ctx Ast.ScopeMap.t
type 'm scope_sigs_ctx = 'm scope_sig_ctx ScopeMap.t
type ctx = {
type 'm ctx = {
structs : struct_ctx;
enums : enum_ctx;
scope_name : ScopeName.t;
scopes_parameters : scope_sigs_ctx;
scope_vars :
(untyped Dcalc.Ast.expr Var.t * naked_typ * Ast.io) ScopeVarMap.t;
scopes_parameters : 'm scope_sigs_ctx;
scope_vars : ('m Dcalc.Ast.expr Var.t * naked_typ * Ast.io) ScopeVarMap.t;
subscope_vars :
(untyped Dcalc.Ast.expr Var.t * naked_typ * Ast.io) ScopeVarMap.t
Ast.SubScopeMap.t;
local_vars : (Ast.expr, untyped Dcalc.Ast.expr Var.t) Var.Map.t;
('m Dcalc.Ast.expr Var.t * naked_typ * Ast.io) ScopeVarMap.t SubScopeMap.t;
local_vars : ('m Ast.expr, 'm Dcalc.Ast.expr Var.t) Var.Map.t;
}
let empty_ctx
(struct_ctx : struct_ctx)
(enum_ctx : enum_ctx)
(scopes_ctx : scope_sigs_ctx)
(scopes_ctx : 'm scope_sigs_ctx)
(scope_name : ScopeName.t) =
{
structs = struct_ctx;
@ -59,40 +57,55 @@ let empty_ctx
scope_name;
scopes_parameters = scopes_ctx;
scope_vars = ScopeVarMap.empty;
subscope_vars = Ast.SubScopeMap.empty;
subscope_vars = SubScopeMap.empty;
local_vars = Var.Map.empty;
}
let pos_mark (pos : Pos.t) : untyped mark = Untyped { pos }
let pos_mark_as e = pos_mark (Marked.get_mark e)
let mark_tany m pos = Expr.with_ty m (Marked.mark pos TAny) ~pos
(* Expression argument is used as a type witness, its type and positions aren't
used *)
let pos_mark_mk (type a m) (e : (a, m mark) gexpr) :
(Pos.t -> m mark) * ((_, Pos.t) Marked.t -> m mark) =
let pos_mark pos =
Expr.map_mark (fun _ -> pos) (fun _ -> TAny, pos) (Marked.get_mark e)
in
let pos_mark_as e = pos_mark (Marked.get_mark e) in
pos_mark, pos_mark_as
let merge_defaults
(caller : untyped Dcalc.Ast.expr Bindlib.box)
(callee : untyped Dcalc.Ast.expr Bindlib.box) :
untyped Dcalc.Ast.expr Bindlib.box =
(caller : 'a Dcalc.Ast.expr Bindlib.box)
(callee : 'a Dcalc.Ast.expr Bindlib.box) : 'a Dcalc.Ast.expr Bindlib.box =
let caller =
let m = Marked.get_mark (Bindlib.unbox caller) in
Expr.make_app caller [Bindlib.box (ELit LUnit, m)] m
let pos = Expr.mark_pos m in
Expr.make_app caller
[Bindlib.box (ELit LUnit, Expr.with_ty m (Marked.mark pos (TLit TUnit)))]
pos
in
let body =
Bindlib.box_apply2
(fun caller callee ->
let m = Marked.get_mark callee in
EDefault ([caller], (ELit (LBool true), m), callee), m)
let ltrue =
Marked.mark
(Expr.with_ty m (Marked.mark (Expr.mark_pos m) (TLit TBool)))
(ELit (LBool true))
in
Marked.mark m (EDefault ([caller], ltrue, callee)))
caller callee
in
body
let tag_with_log_entry
(e : untyped Dcalc.Ast.expr Bindlib.box)
(e : 'm Dcalc.Ast.expr Bindlib.box)
(l : log_entry)
(markings : Utils.Uid.MarkedString.info list) :
untyped Dcalc.Ast.expr Bindlib.box =
'm Dcalc.Ast.expr Bindlib.box =
Bindlib.box_apply
(fun e ->
Marked.same_mark_as
(EApp (Marked.same_mark_as (EOp (Unop (Log (l, markings)))) e, [e]))
e)
let m = mark_tany (Marked.get_mark e) (Expr.pos e) in
Marked.mark m (EApp (Marked.mark m (EOp (Unop (Log (l, markings)))), [e])))
e
(* In a list of exceptions, it is normally an error if more than a single one
@ -102,16 +115,22 @@ let tag_with_log_entry
NOTE: the choice of the exception that will be triggered and show in the
trace is arbitrary (but deterministic). *)
let collapse_similar_outcomes (excepts : Ast.expr list) : Ast.expr list =
let collapse_similar_outcomes (type m) (excepts : m Ast.expr list) :
m Ast.expr list =
let module ExprMap = Map.Make (struct
type t = m Ast.expr
let compare = Expr.compare
end) in
let cons_map =
List.fold_left
(fun map -> function
| (EDefault ([], _, cons), _) as e ->
Ast.ExprMap.update cons
ExprMap.update cons
(fun prev -> Some (e :: Option.value ~default:[] prev))
map
| _ -> map)
Ast.ExprMap.empty excepts
ExprMap.empty excepts
in
let _, excepts =
List.fold_right
@ -125,16 +144,16 @@ let collapse_similar_outcomes (excepts : Ast.expr list) : Ast.expr list =
[EDefault (acc, just, cons), pos]
| _ -> assert false)
[]
(Ast.ExprMap.find cons cons_map)
(ExprMap.find cons cons_map)
in
Ast.ExprMap.add cons [] cons_map, collapsed_exc @ excepts
ExprMap.add cons [] cons_map, collapsed_exc @ excepts
| e -> cons_map, e :: excepts)
excepts (cons_map, [])
in
excepts
let rec translate_expr (ctx : ctx) (e : Ast.expr) :
untyped Dcalc.Ast.expr Bindlib.box =
let rec translate_expr (ctx : 'm ctx) (e : 'm Ast.expr) :
'm Dcalc.Ast.expr Bindlib.box =
Bindlib.box_apply (fun x -> Marked.same_mark_as x e)
@@
match Marked.unmark e with
@ -214,7 +233,7 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr) :
in
if EnumConstructorMap.cardinal remaining_e_cases > 0 then
Errors.raise_spanned_error (Expr.pos e)
"Patter matching is incomplete for enum %a: missing cases %a"
"Pattern matching is incomplete for enum %a: missing cases %a"
EnumName.format_t enum_name
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ", ")
@ -260,7 +279,7 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr) :
retrieve_in_and_out_typ_or_any var ctx.scope_vars
| ELocation (SubScopeVar (_, sname, var)) ->
ctx.subscope_vars
|> Ast.SubScopeMap.find (Marked.unmark sname)
|> SubScopeMap.find (Marked.unmark sname)
|> retrieve_in_and_out_typ_or_any var
| _ -> TAny, TAny
in
@ -319,7 +338,7 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr) :
try
let v, _, _ =
ScopeVarMap.find (Marked.unmark a)
(Ast.SubScopeMap.find (Marked.unmark s) ctx.subscope_vars)
(SubScopeMap.find (Marked.unmark s) ctx.subscope_vars)
in
Bindlib.box_var v
with Not_found ->
@ -353,14 +372,15 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr) :
continuation yielding a [Dcalc.scope_body_expr] by giving it what should
come later in the chain of let-bindings. *)
let translate_rule
(ctx : ctx)
(rule : Ast.rule)
(ctx : 'm ctx)
(rule : 'm Ast.rule)
((sigma_name, pos_sigma) : Utils.Uid.MarkedString.info) :
(untyped Dcalc.Ast.expr scope_body_expr Bindlib.box ->
untyped Dcalc.Ast.expr scope_body_expr Bindlib.box)
* ctx =
('m Dcalc.Ast.expr scope_body_expr Bindlib.box ->
'm Dcalc.Ast.expr scope_body_expr Bindlib.box)
* 'm ctx =
match rule with
| Definition ((ScopelangScopeVar a, var_def_pos), tau, a_io, e) ->
let pos_mark, pos_mark_as = pos_mark_mk e in
let a_name = ScopeVar.get_info (Marked.unmark a) in
let a_var = Var.make (Marked.unmark a_name) in
let new_e = translate_expr ctx e in
@ -406,6 +426,7 @@ let translate_rule
tau,
a_io,
e ) ->
let _pos_mark, pos_mark_as = pos_mark_mk e in
let a_name =
Marked.map_under_mark
(fun str ->
@ -429,7 +450,7 @@ let translate_rule
| Reentrant ->
Expr.make_abs [| silent_var |] new_e
[TLit TUnit, var_def_pos]
(pos_mark var_def_pos)
var_def_pos
in
( (fun next ->
Bindlib.box_apply2
@ -452,7 +473,7 @@ let translate_rule
{
ctx with
subscope_vars =
Ast.SubScopeMap.update (Marked.unmark subs_index)
SubScopeMap.update (Marked.unmark subs_index)
(fun map ->
match map with
| Some map ->
@ -466,8 +487,8 @@ let translate_rule
(a_var, Marked.unmark tau, a_io)))
ctx.subscope_vars;
} )
| Call (subname, subindex) ->
let subscope_sig = Ast.ScopeMap.find subname ctx.scopes_parameters in
| Call (subname, subindex, m) ->
let subscope_sig = ScopeMap.find subname ctx.scopes_parameters in
let all_subscope_vars = subscope_sig.scope_sig_local_vars in
let all_subscope_input_vars =
List.filter
@ -486,7 +507,7 @@ let translate_rule
let called_scope_input_struct = subscope_sig.scope_sig_input_struct in
let called_scope_return_struct = subscope_sig.scope_sig_output_struct in
let subscope_vars_defined =
try Ast.SubScopeMap.find subindex ctx.subscope_vars
try SubScopeMap.find subindex ctx.subscope_vars
with Not_found -> ScopeVarMap.empty
in
let subscope_var_not_yet_defined subvar =
@ -501,19 +522,19 @@ let translate_rule
should have been defined (even an empty definition, if they're
not defined by any rule in the source code) by the translation
from desugared to the scope language. *)
Bindlib.box (Expr.empty_thunked_term (Untyped { pos = pos_call }))
Expr.empty_thunked_term m
else
let a_var, _, _ =
ScopeVarMap.find subvar.scope_var_name subscope_vars_defined
in
Expr.make_var (a_var, pos_mark pos_call))
Expr.make_var (a_var, mark_tany m pos_call))
all_subscope_input_vars
in
let subscope_struct_arg =
Bindlib.box_apply
(fun subscope_args ->
( ETuple (subscope_args, Some called_scope_input_struct),
pos_mark pos_call ))
mark_tany m pos_call ))
(Bindlib.box_list subscope_args)
in
let all_subscope_output_vars_dcalc =
@ -530,8 +551,7 @@ let translate_rule
in
let subscope_func =
tag_with_log_entry
(Expr.make_var
(scope_dcalc_var, pos_mark_as (SubScopeName.get_info subindex)))
(Expr.make_var (scope_dcalc_var, mark_tany m pos_call))
BeginCall
[
sigma_name, pos_sigma;
@ -542,7 +562,7 @@ let translate_rule
let call_expr =
tag_with_log_entry
(Bindlib.box_apply2
(fun e u -> EApp (e, [u]), pos_mark Pos.no_pos)
(fun e u -> EApp (e, [u]), mark_tany m pos_call)
subscope_func subscope_struct_arg)
EndCall
[
@ -587,10 +607,10 @@ let translate_rule
(fun (var_ctx, _) ->
var_ctx.scope_var_typ, pos_sigma)
all_subscope_output_vars_dcalc ),
pos_mark pos_sigma );
mark_tany m pos_sigma );
})
(Bindlib.bind_var v next)
(Expr.make_var (result_tuple_var, pos_mark pos_sigma)),
(Expr.make_var (result_tuple_var, mark_tany m pos_sigma)),
i - 1 ))
all_subscope_output_vars_dcalc
(next, List.length all_subscope_output_vars_dcalc - 1)
@ -599,7 +619,7 @@ let translate_rule
{
ctx with
subscope_vars =
Ast.SubScopeMap.add subindex
SubScopeMap.add subindex
(List.fold_left
(fun acc (var_ctx, dvar) ->
ScopeVarMap.add var_ctx.scope_var_name
@ -610,20 +630,22 @@ let translate_rule
} )
| Assertion e ->
let new_e = translate_expr ctx e in
let scope_let_pos = Expr.pos e in
let scope_let_typ = TLit TUnit, scope_let_pos in
( (fun next ->
Bindlib.box_apply2
(fun next new_e ->
ScopeLet
{
scope_let_next = next;
scope_let_pos = Expr.pos e;
scope_let_typ = TLit TUnit, Expr.pos e;
scope_let_pos;
scope_let_typ;
scope_let_expr =
(* To ensure that we throw an error if the value is not
defined, we add an check "ErrorOnEmpty" here. *)
Marked.same_mark_as
(EAssert (Marked.same_mark_as (ErrorOnEmpty new_e) e))
new_e;
Marked.mark
(Expr.map_ty (fun _ -> scope_let_typ) (Marked.get_mark e))
(EAssert (Marked.same_mark_as (ErrorOnEmpty new_e) e));
scope_let_kind = Assertion;
})
(Bindlib.bind_var (Var.make "_") next)
@ -631,11 +653,12 @@ let translate_rule
ctx )
let translate_rules
(ctx : ctx)
(rules : Ast.rule list)
(ctx : 'm ctx)
(rules : 'm Ast.rule list)
((sigma_name, pos_sigma) : Utils.Uid.MarkedString.info)
(mark : 'm mark)
(sigma_return_struct_name : StructName.t) :
untyped Dcalc.Ast.expr scope_body_expr Bindlib.box * ctx =
'm Dcalc.Ast.expr scope_body_expr Bindlib.box * 'm ctx =
let scope_lets, new_ctx =
List.fold_left
(fun (scope_lets, ctx) rule ->
@ -655,11 +678,11 @@ let translate_rules
let return_exp =
Bindlib.box_apply
(fun args ->
ETuple (args, Some sigma_return_struct_name), pos_mark pos_sigma)
ETuple (args, Some sigma_return_struct_name), mark_tany mark pos_sigma)
(Bindlib.box_list
(List.map
(fun (_, (dcalc_var, _, _)) ->
Expr.make_var (dcalc_var, pos_mark pos_sigma))
Expr.make_var (dcalc_var, mark_tany mark pos_sigma))
scope_output_variables))
in
( scope_lets
@ -669,12 +692,12 @@ let translate_rules
let translate_scope_decl
(struct_ctx : struct_ctx)
(enum_ctx : enum_ctx)
(sctx : scope_sigs_ctx)
(sctx : 'm scope_sigs_ctx)
(scope_name : ScopeName.t)
(sigma : Ast.scope_decl) :
untyped Dcalc.Ast.expr scope_body Bindlib.box * struct_ctx =
(sigma : 'm Ast.scope_decl) :
'm Dcalc.Ast.expr scope_body Bindlib.box * struct_ctx =
let sigma_info = ScopeName.get_info sigma.scope_decl_name in
let scope_sig = Ast.ScopeMap.find sigma.scope_decl_name sctx in
let scope_sig = ScopeMap.find sigma.scope_decl_name sctx in
let scope_variables = scope_sig.scope_sig_local_vars in
let ctx =
(* the context must be initialized for fresh variables for all only-input
@ -703,7 +726,7 @@ let translate_scope_decl
let scope_return_struct_name = scope_sig.scope_sig_output_struct in
let pos_sigma = Marked.get_mark sigma_info in
let rules_with_return_expr, ctx =
translate_rules ctx sigma.scope_decl_rules sigma_info
translate_rules ctx sigma.scope_decl_rules sigma_info sigma.scope_mark
scope_return_struct_name
in
let scope_variables =
@ -757,10 +780,11 @@ let translate_scope_decl
List.map
(fun (var_ctx, _) -> input_var_typ var_ctx)
scope_input_variables ),
pos_mark pos_sigma );
mark_tany sigma.scope_mark pos_sigma );
})
(Bindlib.bind_var v next)
(Expr.make_var (scope_input_var, pos_mark pos_sigma)),
(Expr.make_var
(scope_input_var, mark_tany sigma.scope_mark pos_sigma)),
i - 1 ))
scope_input_variables
(next, List.length scope_input_variables - 1))
@ -798,18 +822,13 @@ let translate_scope_decl
(input_destructurings rules_with_return_expr)),
new_struct_ctx )
let translate_program (prgm : Ast.program) :
untyped Dcalc.Ast.program * Dependency.TVertex.t list =
let translate_program (prgm : 'm Ast.program) : 'm Dcalc.Ast.program =
let scope_dependencies = Dependency.build_program_dep_graph prgm in
Dependency.check_for_cycle_in_scope scope_dependencies;
let types_ordering =
Dependency.check_type_cycles prgm.program_ctx.ctx_structs
prgm.program_ctx.ctx_enums
in
let scope_ordering = Dependency.get_scope_ordering scope_dependencies in
let decl_ctx = prgm.program_ctx in
let sctx : scope_sigs_ctx =
Ast.ScopeMap.mapi
let sctx : 'm scope_sigs_ctx =
ScopeMap.mapi
(fun scope_name scope ->
let scope_dvar =
Var.make
@ -849,15 +868,15 @@ let translate_program (prgm : Ast.program) :
in
(* the resulting expression is the list of definitions of all the scopes,
ending with the top-level scope. *)
let (scopes, decl_ctx) : untyped Dcalc.Ast.expr scopes Bindlib.box * _ =
let (scopes, decl_ctx) : 'm Dcalc.Ast.expr scopes Bindlib.box * _ =
List.fold_right
(fun scope_name (scopes, decl_ctx) ->
let scope = Ast.ScopeMap.find scope_name prgm.program_scopes in
let scope = ScopeMap.find scope_name prgm.program_scopes in
let scope_body, scope_out_struct =
translate_scope_decl decl_ctx.ctx_structs decl_ctx.ctx_enums sctx
scope_name scope
in
let dvar = (Ast.ScopeMap.find scope_name sctx).scope_sig_scope_var in
let dvar = (ScopeMap.find scope_name sctx).scope_sig_scope_var in
let decl_ctx =
{
decl_ctx with
@ -878,4 +897,4 @@ let translate_program (prgm : Ast.program) :
scope_ordering
(Bindlib.box Nil, decl_ctx)
in
{ scopes = Bindlib.unbox scopes; decl_ctx }, types_ordering
{ scopes = Bindlib.unbox scopes; decl_ctx }

8
compiler/scopelang/scope_to_dcalc.mli
View File

@ -16,10 +16,4 @@
(** Scope language to default calculus translator *)
val translate_program :
Ast.program ->
Shared_ast.untyped Dcalc.Ast.program * Dependency.TVertex.t list
(** Usage [translate_program p] returns a tuple [(new_program, types_list)]
where [new_program] is the map of translated scopes. Finally, [types_list]
is a list of all types (structs and enums) used in the program, correctly
ordered with respect to inter-types dependency. *)
val translate_program : 'm Ast.program -> 'm Dcalc.Ast.program

10
compiler/shared_ast/definitions.ml
View File

@ -26,6 +26,8 @@ module Runtime = Runtime_ocaml.Runtime
module ScopeName : Uid.Id with type info = Uid.MarkedString.info =
Uid.Make (Uid.MarkedString) ()
module ScopeMap : Map.S with type key = ScopeName.t = Map.Make (ScopeName)
module StructName : Uid.Id with type info = Uid.MarkedString.info =
Uid.Make (Uid.MarkedString) ()
@ -53,6 +55,12 @@ module ScopeVarMap : Map.S with type key = ScopeVar.t = Map.Make (ScopeVar)
module SubScopeName : Uid.Id with type info = Uid.MarkedString.info =
Uid.Make (Uid.MarkedString) ()
module SubScopeNameSet : Set.S with type elt = SubScopeName.t =
Set.Make (SubScopeName)
module SubScopeMap : Map.S with type key = SubScopeName.t =
Map.Make (SubScopeName)
module StructFieldMap : Map.S with type key = StructFieldName.t =
Map.Make (StructFieldName)
@ -264,7 +272,7 @@ type typed = { pos : Pos.t; ty : typ }
type _ mark = Untyped : untyped -> untyped mark | Typed : typed -> typed mark
(** Useful for errors and printing, for example *)
type any_expr = AnyExpr : (_ any, _ mark) gexpr -> any_expr
type any_expr = AnyExpr : (_, _ mark) gexpr -> any_expr
(** {2 Higher-level program structure} *)

198
compiler/shared_ast/expr.ml
View File

@ -98,7 +98,7 @@ let pos (type m) (x : ('a, m mark) Marked.t) : Pos.t =
let ty (_, m) : typ = match m with Typed { ty; _ } -> ty
let with_ty (type m) (ty : typ) (x : ('a, m mark) Marked.t) :
let set_ty (type m) (ty : typ) (x : ('a, m mark) Marked.t) :
('a, typed mark) Marked.t =
Marked.mark
(match Marked.get_mark x with
@ -138,6 +138,18 @@ let fold_marks
ty = ty_f (List.map (function Typed m -> m) ms);
}
let with_pos (type m) (pos : Pos.t) (m : m mark) : m mark =
map_mark (fun _ -> pos) (fun ty -> ty) m
let map_ty (type m) (ty_f : typ -> typ) (m : m mark) : m mark =
map_mark (fun pos -> pos) ty_f m
let with_ty (type m) (m : m mark) ?pos (ty : typ) : m mark =
map_mark (fun default -> Option.value pos ~default) (fun _ -> ty) m
let maybe_ty (type m) ?(typ = TAny) (m : m mark) : typ =
match m with Untyped { pos } -> Marked.mark pos typ | Typed { ty; _ } -> ty
(* - Traversal functions - *)
(* shallow map *)
@ -205,74 +217,6 @@ let box e =
let untype e = map_marks ~f:(fun m -> Untyped { pos = mark_pos m }) e
(* - Expression building helpers - *)
let make_var (x, mark) =
Bindlib.box_apply (fun x -> x, mark) (Bindlib.box_var x)
let make_abs xs e taus mark =
Bindlib.box_apply (fun b -> EAbs (b, taus), mark) (Bindlib.bind_mvar xs e)
let make_app e u mark =
Bindlib.box_apply2 (fun e u -> EApp (e, u), mark) e (Bindlib.box_list u)
let empty_thunked_term mark =
let silent = Var.make "_" in
let pos = mark_pos mark in
Bindlib.unbox
(make_abs [| silent |]
(Bindlib.box (ELit LEmptyError, mark))
[TLit TUnit, pos]
(map_mark
(fun pos -> pos)
(fun ty ->
Marked.mark pos (TArrow (Marked.mark pos (TLit TUnit), ty)))
mark))
let make_let_in x tau e1 e2 pos =
let m_e1 = Marked.get_mark (Bindlib.unbox e1) in
let m_e2 = Marked.get_mark (Bindlib.unbox e2) in
let m_abs =
map_mark2
(fun _ _ -> pos)
(fun m1 m2 -> Marked.mark pos (TArrow (m1.ty, m2.ty)))
m_e1 m_e2
in
make_app (make_abs [| x |] e2 [tau] m_abs) [e1] m_e2
let make_multiple_let_in xs taus e1s e2 pos =
(* let m_e1s = List.map (fun e -> Marked.get_mark (Bindlib.unbox e)) e1s in *)
let m_e1s =
fold_marks List.hd
(fun tys -> TTuple (List.map (fun t -> t.ty) tys), (List.hd tys).pos)
(List.map (fun e -> Marked.get_mark (Bindlib.unbox e)) e1s)
in
let m_e2 = Marked.get_mark (Bindlib.unbox e2) in
let m_abs =
map_mark2
(fun _ _ -> pos)
(fun m1 m2 -> Marked.mark pos (TArrow (m1.ty, m2.ty)))
m_e1s m_e2
in
make_app (make_abs xs e2 taus m_abs) e1s m_e2
let make_default exceptions just cons mark =
let rec bool_value = function
| ELit (LBool b), _ -> Some b
| EApp ((EOp (Unop (Log (l, _))), _), [e]), _
when l <> PosRecordIfTrueBool
(* we don't remove the log calls corresponding to source code
definitions !*) ->
bool_value e
| _ -> None
in
match exceptions, bool_value just, cons with
| [], Some true, cons -> cons
| exceptions, Some true, (EDefault ([], just, cons), mark) ->
EDefault (exceptions, just, cons), mark
| [except], Some false, _ -> except
| exceptions, _, cons -> EDefault (exceptions, just, cons), mark
(* Tests *)
let is_value (type a) (e : (a, _) gexpr) =
@ -301,6 +245,24 @@ let rec equal_typ ty1 ty2 =
and equal_typ_list tys1 tys2 =
try List.for_all2 equal_typ tys1 tys2 with Invalid_argument _ -> false
(* Similar to [equal_typ], but allows TAny holes *)
let rec unifiable ty1 ty2 =
match Marked.unmark ty1, Marked.unmark ty2 with
| TAny, _ | _, TAny -> true
| TLit l1, TLit l2 -> equal_tlit l1 l2
| TTuple tys1, TTuple tys2 -> unifiable_list tys1 tys2
| TStruct n1, TStruct n2 -> StructName.equal n1 n2
| TEnum n1, TEnum n2 -> EnumName.equal n1 n2
| TOption t1, TOption t2 -> unifiable t1 t2
| TArrow (t1, t1'), TArrow (t2, t2') -> unifiable t1 t2 && unifiable t1' t2'
| TArray t1, TArray t2 -> unifiable t1 t2
| ( (TLit _ | TTuple _ | TStruct _ | TEnum _ | TOption _ | TArrow _ | TArray _),
_ ) ->
false
and unifiable_list tys1 tys2 =
try List.for_all2 unifiable tys1 tys2 with Invalid_argument _ -> false
let rec compare_typ ty1 ty2 =
match Marked.unmark ty1, Marked.unmark ty2 with
| TLit l1, TLit l2 -> compare_tlit l1 l2
@ -722,7 +684,7 @@ let remove_logging_calls e =
in
f () e
let format ?debug decl_ctx ppf e = Print.naked_expr ?debug decl_ctx ppf e
let format ?debug decl_ctx ppf e = Print.expr ?debug decl_ctx ppf e
let rec size : type a. (a, 't) gexpr -> int =
fun e ->
@ -756,3 +718,99 @@ let rec size : type a. (a, 't) gexpr -> int =
| EEnumInj (e1, _, _) -> 1 + size e1
| EMatchS (e1, _, cases) ->
EnumConstructorMap.fold (fun _ e acc -> acc + 1 + size e) cases (size e1)
(* - Expression building helpers - *)
let make_var (x, mark) =
Bindlib.box_apply (fun x -> x, mark) (Bindlib.box_var x)
let make_abs xs e taus pos =
let mark =
map_mark
(fun _ -> pos)
(fun ety ->
List.fold_right
(fun tx acc -> Marked.mark pos (TArrow (tx, acc)))
taus ety)
(Marked.get_mark (Bindlib.unbox e))
in
Bindlib.box_apply (fun b -> EAbs (b, taus), mark) (Bindlib.bind_mvar xs e)
let make_app e u pos =
Bindlib.box_apply2
(fun e u ->
let mark =
fold_marks
(fun _ -> pos)
(function
| [] -> assert false
| fty :: argtys ->
List.fold_left
(fun tf tx ->
match Marked.unmark tf with
| TArrow (tx', tr) ->
assert (unifiable tx.ty tx');
(* wrong arg type *)
tr
| TAny -> tf
| _ ->
Format.eprintf
"Attempt to construct application of non-arrow type %a:@\n\
%a"
Print.typ_debug tf
(Print.expr_debug ~debug:false)
e;
assert false)
fty.ty argtys)
(List.map Marked.get_mark (e :: u))
in
EApp (e, u), mark)
e (Bindlib.box_list u)
let empty_thunked_term mark =
let silent = Var.make "_" in
let pos = mark_pos mark in
make_abs [| silent |]
(Bindlib.box (ELit LEmptyError, mark))
[TLit TUnit, pos]
pos
let make_let_in x tau e1 e2 mpos =
make_app (make_abs [| x |] e2 [tau] mpos) [e1] (pos (Bindlib.unbox e2))
let make_multiple_let_in xs taus e1s e2 mpos =
make_app (make_abs xs e2 taus mpos) e1s (pos (Bindlib.unbox e2))
let make_default exceptions just cons mark =
let rec bool_value = function
| ELit (LBool b), _ -> Some b
| EApp ((EOp (Unop (Log (l, _))), _), [e]), _
when l <> PosRecordIfTrueBool
(* we don't remove the log calls corresponding to source code
definitions !*) ->
bool_value e
| _ -> None
in
match exceptions, bool_value just, cons with
| [], Some true, cons -> cons
| exceptions, Some true, (EDefault ([], just, cons), mark) ->
EDefault (exceptions, just, cons), mark
| [except], Some false, _ -> except
| exceptions, _, cons -> EDefault (exceptions, just, cons), mark
let make_tuple el structname m0 =
match el with
| [] ->
etuple [] structname
(with_ty m0
(match structname with
| Some n -> TStruct n, mark_pos m0
| None -> TTuple [], mark_pos m0))
| el ->
let m =
fold_marks
(fun posl -> List.hd posl)
(fun ml -> TTuple (List.map (fun t -> t.ty) ml), (List.hd ml).pos)
(List.map (fun e -> Marked.get_mark (Bindlib.unbox e)) el)
in
etuple el structname m

43
compiler/shared_ast/expr.mli
View File

@ -103,9 +103,14 @@ val eraise : except -> 't -> (lcalc, 't) gexpr box
val no_mark : 'm mark -> 'm mark
val mark_pos : 'm mark -> Pos.t
val pos : ('e, _ mark) gexpr -> Pos.t
val ty : (_, typed mark) Marked.t -> typ
val with_ty : typ -> ('a, _ mark) Marked.t -> ('a, typed mark) Marked.t
val with_pos : Pos.t -> 'm mark -> 'm mark
val with_ty : 'm mark -> ?pos:Pos.t -> typ -> 'm mark
(** Adds the given type information only on typed marks *)
val map_ty : (typ -> typ) -> 'm mark -> 'm mark
(** Identity on untyped marks*)
val map_mark : (Pos.t -> Pos.t) -> (typ -> typ) -> 'm mark -> 'm mark
val map_mark2 :
@ -118,6 +123,15 @@ val map_mark2 :
val fold_marks :
(Pos.t list -> Pos.t) -> (typed list -> typ) -> 'm mark list -> 'm mark
val maybe_ty : ?typ:naked_typ -> 'm mark -> typ
(** Returns the corresponding type on a typed expr, or [typ] (defaulting to
[TAny]) at the current position on an untyped one *)
(** Manipulation of marked expressions *)
val pos : ('e, 'm mark) gexpr -> Pos.t
val ty : ('e, typed mark) Marked.t -> typ
val set_ty : typ -> ('a, 'm mark) Marked.t -> ('a, typed mark) Marked.t
val untype : ('a, 'm mark) gexpr -> ('a, untyped mark) gexpr box
(** {2 Traversal functions} *)
@ -161,27 +175,27 @@ val map_marks : f:('t1 -> 't2) -> ('a, 't1) gexpr -> ('a, 't2) gexpr box
val make_var : ('a, 't) gexpr Var.t * 'b -> (('a, 't) naked_gexpr * 'b) box
val make_abs :
('a, 't) gexpr Var.vars ->
('a, 't) gexpr box ->
('a, 'm mark) gexpr Var.vars ->
('a, 'm mark) gexpr box ->
typ list ->
't ->
('a, 't) gexpr box
Pos.t ->
('a, 'm mark) gexpr box
val make_app :
('a any, 'm mark) gexpr box ->
('a, 'm mark) gexpr box list ->
'm mark ->
Pos.t ->
('a, 'm mark) gexpr box
val empty_thunked_term :
'm mark -> ([< dcalc | desugared | scopelang ], 'm mark) gexpr
'm mark -> ([< dcalc | desugared | scopelang ], 'm mark) gexpr box
val make_let_in :
('a, 'm mark) gexpr Var.t ->
typ ->
('a, 'm mark) gexpr box ->
('a, 'm mark) gexpr box ->
Utils.Pos.t ->
Pos.t ->
('a, 'm mark) gexpr box
val make_multiple_let_in :
@ -211,6 +225,14 @@ val make_default :
exceptions, is collapsed into [<ex | def>]
- [<ex | false :- _>], when [ex] is a single exception, is rewritten as [ex] *)
val make_tuple :
(([< dcalc | lcalc ] as 'a), 'm mark) gexpr box list ->
StructName.t option ->
'm mark ->
('a, 'm mark) gexpr box
(** Builds a tuple; the mark argument is only used as witness and for position
when building 0-uples *)
(** {2 Transformations} *)
val remove_logging_calls : ('a any, 't) gexpr -> ('a, 't) gexpr box
@ -238,6 +260,7 @@ val compare : ('a, 't) gexpr -> ('a, 't) gexpr -> int
(** Standard comparison function, suitable for e.g. [Set.Make]. Ignores position
information *)
val equal_typ : typ -> typ -> bool
val compare_typ : typ -> typ -> int
val is_value : ('a any, 't) gexpr -> bool
val free_vars : ('a any, 't) gexpr -> ('a, 't) gexpr Var.Set.t

375
compiler/shared_ast/print.ml
View File

@ -74,7 +74,7 @@ let enum_constructor (fmt : Format.formatter) (c : EnumConstructor.t) : unit =
(Utils.Cli.format_with_style [ANSITerminal.magenta])
(Format.asprintf "%a" EnumConstructor.format_t c)
let rec typ (ctx : decl_ctx) (fmt : Format.formatter) (ty : typ) : unit =
let rec typ (ctx : decl_ctx option) (fmt : Format.formatter) (ty : typ) : unit =
let typ = typ ctx in
let typ_with_parens (fmt : Format.formatter) (t : typ) =
if typ_needs_parens t then Format.fprintf fmt "(%a)" typ t
@ -88,31 +88,39 @@ let rec typ (ctx : decl_ctx) (fmt : Format.formatter) (ty : typ) : unit =
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ %a@ " operator "*")
(fun fmt t -> Format.fprintf fmt "%a" typ t))
ts
| TStruct s ->
Format.fprintf fmt "@[<hov 2>%a%a%a%a@]" StructName.format_t s punctuation
"{"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "%a@ " punctuation ";")
(fun fmt (field, mty) ->
Format.fprintf fmt "%a%a%a%a@ %a" punctuation "\""
StructFieldName.format_t field punctuation "\"" punctuation ":" typ
mty))
(StructMap.find s ctx.ctx_structs)
punctuation "}"
| TEnum e ->
Format.fprintf fmt "@[<hov 2>%a%a%a%a@]" EnumName.format_t e punctuation "["
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ %a@ " punctuation "|")
(fun fmt (case, mty) ->
Format.fprintf fmt "%a%a@ %a" enum_constructor case punctuation ":"
typ mty))
(EnumMap.find e ctx.ctx_enums)
punctuation "]"
| TStruct s -> (
match ctx with
| None -> Format.fprintf fmt "@[<hov 2>%a@]" StructName.format_t s
| Some ctx ->
Format.fprintf fmt "@[<hov 2>%a%a%a%a@]" StructName.format_t s punctuation
"{"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "%a@ " punctuation ";")
(fun fmt (field, mty) ->
Format.fprintf fmt "%a%a%a%a@ %a" punctuation "\""
StructFieldName.format_t field punctuation "\"" punctuation ":"
typ mty))
(StructMap.find s ctx.ctx_structs)
punctuation "}")
| TEnum e -> (
match ctx with
| None -> Format.fprintf fmt "@[<hov 2>%a@]" EnumName.format_t e
| Some ctx ->
Format.fprintf fmt "@[<hov 2>%a%a%a%a@]" EnumName.format_t e punctuation
"["
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ %a@ " punctuation "|")
(fun fmt (case, mty) ->
Format.fprintf fmt "%a%a@ %a" enum_constructor case punctuation ":"
typ mty))
(EnumMap.find e ctx.ctx_enums)
punctuation "]")
| TOption t -> Format.fprintf fmt "@[<hov 2>%a@ %a@]" base_type "option" typ t
| TArrow (t1, t2) ->
Format.fprintf fmt "@[<hov 2>%a %a@ %a@]" typ_with_parens t1 operator "→"
typ t2
| TArray t1 -> Format.fprintf fmt "@[<hov 2>%a@ %a@]" base_type "array" typ t1
| TArray t1 ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" base_type "collection" typ t1
| TAny -> base_type fmt "any"
let lit (type a) (fmt : Format.formatter) (l : a glit) : unit =
@ -211,155 +219,176 @@ let var fmt v =
let needs_parens (type a) (e : (a, _) gexpr) : bool =
match Marked.unmark e with EAbs _ | ETuple (_, Some _) -> true | _ -> false
let rec naked_expr :
'a.
?debug:bool -> decl_ctx -> Format.formatter -> ('a, 't) gexpr -> unit
let rec expr :
type a.
?debug:bool -> decl_ctx option -> Format.formatter -> (a, 't) gexpr -> unit
=
fun (type a) ?(debug : bool = false) (ctx : decl_ctx) (fmt : Format.formatter)
(e : (a, 't) gexpr) ->
let naked_expr e = naked_expr ~debug ctx e in
let with_parens fmt e =
if needs_parens e then (
punctuation fmt "(";
naked_expr fmt e;
punctuation fmt ")")
else naked_expr fmt e
in
match Marked.unmark e with
| EVar v -> Format.fprintf fmt "%a" var v
| ETuple (es, None) ->
Format.fprintf fmt "@[<hov 2>%a%a%a@]" punctuation "("
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ")
(fun fmt e -> Format.fprintf fmt "%a" naked_expr e))
es punctuation ")"
| ETuple (es, Some s) ->
Format.fprintf fmt "@[<hov 2>%a@ @[<hov 2>%a%a%a@]@]" StructName.format_t s
punctuation "{"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "%a@ " punctuation ";")
(fun fmt (e, struct_field) ->
Format.fprintf fmt "%a%a%a%a@ %a" punctuation "\""
StructFieldName.format_t struct_field punctuation "\"" punctuation
"=" naked_expr e))
(List.combine es (List.map fst (StructMap.find s ctx.ctx_structs)))
punctuation "}"
| EArray es ->
Format.fprintf fmt "@[<hov 2>%a%a%a@]" punctuation "["
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ";@ ")
(fun fmt e -> Format.fprintf fmt "%a" naked_expr e))
es punctuation "]"
| ETupleAccess (e1, n, s, _ts) -> (
match s with
| None -> Format.fprintf fmt "%a%a%d" naked_expr e1 punctuation "." n
| Some s ->
Format.fprintf fmt "%a%a%a%a%a" naked_expr e1 operator "." punctuation
"\"" StructFieldName.format_t
(fst (List.nth (StructMap.find s ctx.ctx_structs) n))
punctuation "\"")
| EInj (e, n, en, _ts) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" enum_constructor
(fst (List.nth (EnumMap.find en ctx.ctx_enums) n))
naked_expr e
| EMatch (e, es, e_name) ->
Format.fprintf fmt "@[<hov 0>%a@ @[<hov 2>%a@]@ %a@ %a@]" keyword "match"
naked_expr e keyword "with"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n")
(fun fmt (e, c) ->
Format.fprintf fmt "@[<hov 2>%a %a%a@ %a@]" punctuation "|"
enum_constructor c punctuation ":" naked_expr e))
(List.combine es (List.map fst (EnumMap.find e_name ctx.ctx_enums)))
| ELit l -> lit fmt l
| EApp ((EAbs (binder, taus), _), args) ->
let xs, body = Bindlib.unmbind binder in
let xs_tau = List.mapi (fun i tau -> xs.(i), tau) taus in
let xs_tau_arg = List.map2 (fun (x, tau) arg -> x, tau, arg) xs_tau args in
Format.fprintf fmt "%a%a"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "")
(fun fmt (x, tau, arg) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@ %a@ %a@ %a@ %a@]@\n"
keyword "let" var x punctuation ":" (typ ctx) tau punctuation "="
naked_expr arg keyword "in"))
xs_tau_arg naked_expr body
| EAbs (binder, taus) ->
let xs, body = Bindlib.unmbind binder in
let xs_tau = List.mapi (fun i tau -> xs.(i), tau) taus in
Format.fprintf fmt "@[<hov 2>%a @[<hov 2>%a@] %a@ %a@]" punctuation "λ"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")
(fun fmt (x, tau) ->
Format.fprintf fmt "%a%a%a %a%a" punctuation "(" var x punctuation
":" (typ ctx) tau punctuation ")"))
xs_tau punctuation "→" naked_expr body
| EApp ((EOp (Binop ((Map | Filter) as op)), _), [arg1; arg2]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" binop op with_parens arg1
with_parens arg2
| EApp ((EOp (Binop op), _), [arg1; arg2]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" with_parens arg1 binop op
with_parens arg2
| EApp ((EOp (Unop (Log _)), _), [arg1]) when not debug ->
naked_expr fmt arg1
| EApp ((EOp (Unop op), _), [arg1]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" unop op with_parens arg1
| EApp (f, args) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" naked_expr f
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")
with_parens)
args
| EIfThenElse (e1, e2, e3) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@ %a@ %a@ %a@]" keyword "if"
naked_expr e1 keyword "then" naked_expr e2 keyword "else" naked_expr e3
| EOp (Ternop op) -> Format.fprintf fmt "%a" ternop op
| EOp (Binop op) -> Format.fprintf fmt "%a" binop op
| EOp (Unop op) -> Format.fprintf fmt "%a" unop op
| EDefault (exceptions, just, cons) ->
if List.length exceptions = 0 then
Format.fprintf fmt "@[<hov 2>%a%a@ %a@ %a%a@]" punctuation "⟨" naked_expr
just punctuation "⊢" naked_expr cons punctuation "⟩"
else
Format.fprintf fmt "@[<hov 2>%a%a@ %a@ %a@ %a@ %a%a@]" punctuation "⟨"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "%a@ " punctuation ",")
naked_expr)
exceptions punctuation "|" naked_expr just punctuation "⊢" naked_expr
cons punctuation "⟩"
| ErrorOnEmpty e' ->
Format.fprintf fmt "%a@ %a" operator "error_empty" with_parens e'
| EAssert e' ->
Format.fprintf fmt "@[<hov 2>%a@ %a%a%a@]" keyword "assert" punctuation "("
naked_expr e' punctuation ")"
| ECatch (e1, exn, e2) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@ %a ->@ %a@]" keyword "try"
with_parens e1 keyword "with" except exn with_parens e2
| ERaise exn ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" keyword "raise" except exn
| ELocation loc -> location fmt loc
| EStruct (name, fields) ->
Format.fprintf fmt " @[<hov 2>%a@ %a@ %a@ %a@]" StructName.format_t name
punctuation "{"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "%a@ " punctuation ";")
(fun fmt (field_name, field_expr) ->
Format.fprintf fmt "%a%a%a%a@ %a" punctuation "\""
StructFieldName.format_t field_name punctuation "\"" punctuation
"=" naked_expr field_expr))
(StructFieldMap.bindings fields)
punctuation "}"
| EStructAccess (e1, field, _) ->
Format.fprintf fmt "%a%a%a%a%a" naked_expr e1 punctuation "." punctuation
"\"" StructFieldName.format_t field punctuation "\""
| EEnumInj (e1, cons, _) ->
Format.fprintf fmt "%a@ %a" EnumConstructor.format_t cons naked_expr e1
| EMatchS (e1, _, cases) ->
Format.fprintf fmt "@[<hov 0>%a@ @[<hov 2>%a@]@ %a@ %a@]" keyword "match"
naked_expr e1 keyword "with"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n")
(fun fmt (cons_name, case_expr) ->
Format.fprintf fmt "@[<hov 2>%a %a@ %a@ %a@]" punctuation "|"
enum_constructor cons_name punctuation "→" naked_expr case_expr))
(EnumConstructorMap.bindings cases)
fun ?(debug = false) ctx fmt e ->
let expr e = expr ~debug ctx e in
let with_parens fmt e =
if needs_parens e then (
punctuation fmt "(";
expr fmt e;
punctuation fmt ")")
else expr fmt e
in
match Marked.unmark e with
| EVar v -> Format.fprintf fmt "%a" var v
| ETuple (es, None) ->
Format.fprintf fmt "@[<hov 2>%a%a%a@]" punctuation "("
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ")
(fun fmt e -> Format.fprintf fmt "%a" expr e))
es punctuation ")"
| ETuple (es, Some s) -> (
match ctx with
| None -> expr fmt (Marked.same_mark_as (ETuple (es, None)) e)
| Some ctx ->
Format.fprintf fmt "@[<hov 2>%a@ @[<hov 2>%a%a%a@]@]" StructName.format_t
s punctuation "{"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "%a@ " punctuation ";")
(fun fmt (e, struct_field) ->
Format.fprintf fmt "%a%a%a%a@ %a" punctuation "\""
StructFieldName.format_t struct_field punctuation "\""
punctuation "=" expr e))
(List.combine es (List.map fst (StructMap.find s ctx.ctx_structs)))
punctuation "}")
| EArray es ->
Format.fprintf fmt "@[<hov 2>%a%a%a@]" punctuation "["
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ";@ ")
(fun fmt e -> Format.fprintf fmt "%a" expr e))
es punctuation "]"
| ETupleAccess (e1, n, s, _ts) -> (
match s, ctx with
| None, _ | _, None -> Format.fprintf fmt "%a%a%d" expr e1 punctuation "." n
| Some s, Some ctx ->
Format.fprintf fmt "%a%a%a%a%a" expr e1 operator "." punctuation "\""
StructFieldName.format_t
(fst (List.nth (StructMap.find s ctx.ctx_structs) n))
punctuation "\"")
| EInj (e, n, en, _ts) -> (
match ctx with
| None ->
Format.fprintf fmt "@[<hov 2>%a[%d]@ %a@]" EnumName.format_t en n expr e
| Some ctx ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" enum_constructor
(fst (List.nth (EnumMap.find en ctx.ctx_enums) n))
expr e)
| EMatch (e, es, e_name) -> (
match ctx with
| None ->
Format.fprintf fmt "@[<hov 0>%a@ @[<hov 2>%a@]@ %a@ %a@]" keyword "match"
expr e keyword "with"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n")
(fun fmt (e, i) ->
Format.fprintf fmt "@[<hov 2>%a %a[%d]%a@ %a@]" punctuation "|"
EnumName.format_t e_name i punctuation ":" expr e))
(List.mapi (fun i e -> e, i) es)
| Some ctx ->
Format.fprintf fmt "@[<hov 0>%a@ @[<hov 2>%a@]@ %a@ %a@]" keyword "match"
expr e keyword "with"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n")
(fun fmt (e, c) ->
Format.fprintf fmt "@[<hov 2>%a %a%a@ %a@]" punctuation "|"
enum_constructor c punctuation ":" expr e))
(List.combine es (List.map fst (EnumMap.find e_name ctx.ctx_enums))))
| ELit l -> lit fmt l
| EApp ((EAbs (binder, taus), _), args) ->
let xs, body = Bindlib.unmbind binder in
let xs_tau = List.mapi (fun i tau -> xs.(i), tau) taus in
let xs_tau_arg = List.map2 (fun (x, tau) arg -> x, tau, arg) xs_tau args in
Format.fprintf fmt "%a%a"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "")
(fun fmt (x, tau, arg) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@ %a@ %a@ %a@ %a@]@\n" keyword
"let" var x punctuation ":" (typ ctx) tau punctuation "=" expr arg
keyword "in"))
xs_tau_arg expr body
| EAbs (binder, taus) ->
let xs, body = Bindlib.unmbind binder in
let xs_tau = List.mapi (fun i tau -> xs.(i), tau) taus in
Format.fprintf fmt "@[<hov 2>%a @[<hov 2>%a@] %a@ %a@]" punctuation "λ"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")
(fun fmt (x, tau) ->
Format.fprintf fmt "%a%a%a %a%a" punctuation "(" var x punctuation
":" (typ ctx) tau punctuation ")"))
xs_tau punctuation "→" expr body
| EApp ((EOp (Binop ((Map | Filter) as op)), _), [arg1; arg2]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" binop op with_parens arg1
with_parens arg2
| EApp ((EOp (Binop op), _), [arg1; arg2]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" with_parens arg1 binop op
with_parens arg2
| EApp ((EOp (Unop (Log _)), _), [arg1]) when not debug -> expr fmt arg1
| EApp ((EOp (Unop op), _), [arg1]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" unop op with_parens arg1
| EApp (f, args) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" expr f
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")
with_parens)
args
| EIfThenElse (e1, e2, e3) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@ %a@ %a@ %a@]" keyword "if" expr e1
keyword "then" expr e2 keyword "else" expr e3
| EOp (Ternop op) -> Format.fprintf fmt "%a" ternop op
| EOp (Binop op) -> Format.fprintf fmt "%a" binop op
| EOp (Unop op) -> Format.fprintf fmt "%a" unop op
| EDefault (exceptions, just, cons) ->
if List.length exceptions = 0 then
Format.fprintf fmt "@[<hov 2>%a%a@ %a@ %a%a@]" punctuation "⟨" expr just
punctuation "⊢" expr cons punctuation "⟩"
else
Format.fprintf fmt "@[<hov 2>%a%a@ %a@ %a@ %a@ %a%a@]" punctuation "⟨"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "%a@ " punctuation ",")
expr)
exceptions punctuation "|" expr just punctuation "⊢" expr cons
punctuation "⟩"
| ErrorOnEmpty e' ->
Format.fprintf fmt "%a@ %a" operator "error_empty" with_parens e'
| EAssert e' ->
Format.fprintf fmt "@[<hov 2>%a@ %a%a%a@]" keyword "assert" punctuation "("
expr e' punctuation ")"
| ECatch (e1, exn, e2) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@ %a ->@ %a@]" keyword "try"
with_parens e1 keyword "with" except exn with_parens e2
| ERaise exn ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" keyword "raise" except exn
| ELocation loc -> location fmt loc
| EStruct (name, fields) ->
Format.fprintf fmt " @[<hov 2>%a@ %a@ %a@ %a@]" StructName.format_t name
punctuation "{"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "%a@ " punctuation ";")
(fun fmt (field_name, field_expr) ->
Format.fprintf fmt "%a%a%a%a@ %a" punctuation "\""
StructFieldName.format_t field_name punctuation "\"" punctuation
"=" expr field_expr))
(StructFieldMap.bindings fields)
punctuation "}"
| EStructAccess (e1, field, _) ->
Format.fprintf fmt "%a%a%a%a%a" expr e1 punctuation "." punctuation "\""
StructFieldName.format_t field punctuation "\""
| EEnumInj (e1, cons, _) ->
Format.fprintf fmt "%a@ %a" EnumConstructor.format_t cons expr e1
| EMatchS (e1, _, cases) ->
Format.fprintf fmt "@[<hov 0>%a@ @[<hov 2>%a@]@ %a@ %a@]" keyword "match"
expr e1 keyword "with"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n")
(fun fmt (cons_name, case_expr) ->
Format.fprintf fmt "@[<hov 2>%a %a@ %a@ %a@]" punctuation "|"
enum_constructor cons_name punctuation "→" expr case_expr))
(EnumConstructorMap.bindings cases)
let typ_debug = typ None
let typ ctx = typ (Some ctx)
let expr_debug ?debug = expr ?debug None
let expr ?debug ctx = expr ?debug (Some ctx)

14
compiler/shared_ast/print.mli
View File

@ -43,9 +43,19 @@ val unop : Format.formatter -> unop -> unit
val except : Format.formatter -> except -> unit
val var : Format.formatter -> 'e Var.t -> unit
val naked_expr :
val expr :
?debug:bool (** [true] for debug printing *) ->
decl_ctx ->
Format.formatter ->
('a, 't) gexpr ->
('a, 'm mark) gexpr ->
unit
(** {1 Debugging versions that don't require a context} *)
val expr_debug :
?debug:bool (** [true] for debug printing *) ->
Format.formatter ->
('a, 'm mark) gexpr ->
unit
val typ_debug : Format.formatter -> typ -> unit

16
compiler/shared_ast/scope.ml
View File

@ -92,9 +92,19 @@ let map_exprs ~f ~varf scopes =
new_body_expr new_next)
~init:(Bindlib.box Nil) scopes
(* TODO: compute the expected body expr arrow type manually instead of [TAny]
for double-checking types ? *)
let rec get_body_expr_mark = function
| ScopeLet sl ->
let _, e = Bindlib.unbind sl.scope_let_next in
get_body_expr_mark e
| Result e ->
let m = Marked.get_mark e in
Expr.with_ty m (Utils.Marked.mark (Expr.mark_pos m) TAny)
let get_body_mark scope_body =
match snd (Bindlib.unbind scope_body.scope_body_expr) with
| Result e | ScopeLet { scope_let_expr = e; _ } -> Marked.get_mark e
let _, e = Bindlib.unbind scope_body.scope_body_expr in
get_body_expr_mark e
let rec unfold_body_expr (ctx : decl_ctx) (scope_let : 'e scope_body_expr) :
'e box =
@ -130,7 +140,7 @@ let to_expr (ctx : decl_ctx) (body : 'e scope_body) (mark_scope : 'm mark) :
let body_expr = unfold_body_expr ctx body_expr in
Expr.make_abs [| var |] body_expr
[TStruct body.scope_body_input_struct, Expr.mark_pos mark_scope]
mark_scope
(Expr.mark_pos mark_scope)
let format
?(debug : bool = false)

1
compiler/shared_ast/shared_ast.ml
View File

@ -20,3 +20,4 @@ module Expr = Expr
module Scope = Scope
module Program = Program
module Print = Print
module Typing = Typing

712
compiler/dcalc/typing.ml → compiler/shared_ast/typing.ml
View File

@ -18,7 +18,7 @@
inference using the classical W algorithm with union-find unification. *)
open Utils
module A = Shared_ast
module A = Definitions
module Any =
Utils.Uid.Make
@ -33,8 +33,8 @@ module Any =
()
type unionfind_typ = naked_typ Marked.pos UnionFind.elem
(** We do not reuse {!type: Dcalc.Ast.naked_typ} because we have to include a
new [TAny] variant. Indeed, error terms can have any type and this has to be
(** We do not reuse {!type: Shared_ast.typ} because we have to include a new
[TAny] variant. Indeed, error terms can have any type and this has to be
captured by the type sytem. *)
and naked_typ =
@ -90,7 +90,7 @@ let rec format_typ
in
let naked_typ = UnionFind.get (UnionFind.find naked_typ) in
match Marked.unmark naked_typ with
| TLit l -> Format.fprintf fmt "%a" A.Print.tlit l
| TLit l -> Format.fprintf fmt "%a" Print.tlit l
| TTuple ts ->
Format.fprintf fmt "@[<hov 2>(%a)]"
(Format.pp_print_list
@ -104,14 +104,18 @@ let rec format_typ
| TArrow (t1, t2) ->
Format.fprintf fmt "@[<hov 2>%a →@ %a@]" format_typ_with_parens t1
format_typ t2
| TArray t1 -> Format.fprintf fmt "@[%a@ array@]" format_typ t1
| TAny d -> Format.fprintf fmt "any[%d]" (Any.hash d)
| TArray t1 -> (
match Marked.unmark (UnionFind.get (UnionFind.find t1)) with
| TAny _ -> Format.pp_print_string fmt "collection"
| _ -> Format.fprintf fmt "@[collection@ %a@]" format_typ t1)
| TAny _ -> Format.pp_print_string fmt "<any>"
exception Type_error of A.any_expr * unionfind_typ * unionfind_typ
type mark = { pos : Pos.t; uf : unionfind_typ }
(** Raises an error if unification cannot be performed *)
(** Raises an error if unification cannot be performed. The position annotation
of the second [unionfind_typ] argument is propagated (unless it is [TAny]). *)
let rec unify
(ctx : A.decl_ctx)
(e : ('a, 'm A.mark) A.gexpr) (* used for error context *)
@ -123,39 +127,31 @@ let rec unify
let t1_repr = UnionFind.get (UnionFind.find t1) in
let t2_repr = UnionFind.get (UnionFind.find t2) in
let raise_type_error () = raise (Type_error (A.AnyExpr e, t1, t2)) in
let repr =
let () =
match Marked.unmark t1_repr, Marked.unmark t2_repr with
| TLit tl1, TLit tl2 when tl1 = tl2 -> None
| TLit tl1, TLit tl2 -> if tl1 <> tl2 then raise_type_error ()
| TArrow (t11, t12), TArrow (t21, t22) ->
unify e t11 t21;
unify e t12 t22;
None
unify e t11 t21
| TTuple ts1, TTuple ts2 ->
if List.length ts1 = List.length ts2 then begin
List.iter2 (unify e) ts1 ts2;
None
end
if List.length ts1 = List.length ts2 then List.iter2 (unify e) ts1 ts2
else raise_type_error ()
| TStruct s1, TStruct s2 ->
if A.StructName.equal s1 s2 then None else raise_type_error ()
if not (A.StructName.equal s1 s2) then raise_type_error ()
| TEnum e1, TEnum e2 ->
if A.EnumName.equal e1 e2 then None else raise_type_error ()
| TOption t1, TOption t2 ->
unify e t1 t2;
None
| TArray t1', TArray t2' ->
unify e t1' t2';
None
| TAny _, TAny _ -> None
| TAny _, _ -> Some t2_repr
| _, TAny _ -> Some t1_repr
if not (A.EnumName.equal e1 e2) then raise_type_error ()
| TOption t1, TOption t2 -> unify e t1 t2
| TArray t1', TArray t2' -> unify e t1' t2'
| TAny _, _ | _, TAny _ -> ()
| ( ( TLit _ | TArrow _ | TTuple _ | TStruct _ | TEnum _ | TOption _
| TArray _ ),
_ ) ->
raise_type_error ()
in
let t_union = UnionFind.union t1 t2 in
match repr with None -> () | Some t_repr -> UnionFind.set t_union t_repr
ignore
@@ UnionFind.merge
(fun t1 t2 -> match Marked.unmark t2 with TAny _ -> t1 | _ -> t2)
t1 t2
let handle_type_error ctx e t1 t2 =
(* TODO: if we get weird error messages, then it means that we should use the
@ -199,6 +195,17 @@ let handle_type_error ctx e t1 t2 =
(Cli.format_with_style [ANSITerminal.blue; ANSITerminal.Bold])
"-->" t2_s ()
let lit_type (type a) (lit : a A.glit) : naked_typ =
match lit with
| LBool _ -> TLit TBool
| LInt _ -> TLit TInt
| LRat _ -> TLit TRat
| LMoney _ -> TLit TMoney
| LDate _ -> TLit TDate
| LDuration _ -> TLit TDuration
| LUnit -> TLit TUnit
| LEmptyError -> TAny (Any.fresh ())
(** 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 the programmer visualize the type flow
@ -269,9 +276,38 @@ let op_type (op : A.operator Marked.pos) : unionfind_typ =
(** {1 Double-directed typing} *)
type 'e env = ('e, unionfind_typ) A.Var.Map.t
module Env = struct
type 'e t = {
vars : ('e, unionfind_typ) Var.Map.t;
scope_vars : A.typ A.ScopeVarMap.t;
scopes : A.typ A.ScopeVarMap.t A.ScopeMap.t;
}
let add_pos e ty = Marked.mark (A.Expr.pos e) ty
let empty =
{
vars = Var.Map.empty;
scope_vars = A.ScopeVarMap.empty;
scopes = A.ScopeMap.empty;
}
let get t v = Var.Map.find_opt v t.vars
let get_scope_var t sv = A.ScopeVarMap.find_opt sv t.scope_vars
let get_subscope_var t scope var =
Option.bind (A.ScopeMap.find_opt scope t.scopes) (fun vmap ->
A.ScopeVarMap.find_opt var vmap)
let add v tau t = { t with vars = Var.Map.add v tau t.vars }
let add_var v typ t = add v (ast_to_typ typ) t
let add_scope_var v typ t =
{ t with scope_vars = A.ScopeVarMap.add v typ t.scope_vars }
let add_scope scope_name vmap t =
{ t with scopes = A.ScopeMap.add scope_name vmap t.scopes }
end
let add_pos e ty = Marked.mark (Expr.pos e) ty
let ty (_, { uf; _ }) = uf
let ( let+ ) x f = Bindlib.box_apply f x
let ( and+ ) x1 x2 = Bindlib.box_pair x1 x2
@ -297,41 +333,107 @@ let bmap2 (f : 'a -> 'b -> 'c Bindlib.box) (es : 'a list) (xs : 'b list) :
let box_ty e = Bindlib.unbox (Bindlib.box_apply ty e)
(** Infers the most permissive type from an expression *)
let rec typecheck_expr_bottom_up
(ctx : A.decl_ctx)
(env : 'm Ast.expr env)
(e : 'm Ast.expr) : (A.dcalc, mark) A.gexpr Bindlib.box =
let rec typecheck_expr_bottom_up :
type a m.
A.decl_ctx ->
(a, m A.mark) A.gexpr Env.t ->
(a, m A.mark) A.gexpr ->
(a, mark) A.gexpr A.box =
fun ctx env e ->
(* Cli.debug_format "Looking for type of %a" (Expr.format ~debug:true ctx)
e; *)
let pos_e = A.Expr.pos e in
let mark (e : (A.dcalc, mark) A.naked_gexpr) uf =
Marked.mark { uf; pos = pos_e } e
let pos_e = Expr.pos e in
let mark e1 uf =
let () =
(* If the expression already has a type annotation, validate it before
rewrite *)
match Marked.get_mark e with
| A.Untyped _ | A.Typed { A.ty = A.TAny, _; _ } -> ()
| A.Typed { A.ty; _ } -> unify ctx e uf (ast_to_typ ty)
in
Marked.mark { uf; pos = pos_e } e1
in
let unionfind_make ?(pos = e) t = UnionFind.make (add_pos pos t) in
let mark_with_uf e1 ?pos ty = mark e1 (unionfind_make ?pos ty) in
match Marked.unmark e with
| A.ELocation loc as e1 -> (
let ty =
match loc with
| DesugaredScopeVar (v, _) | ScopelangScopeVar v ->
Env.get_scope_var env (Marked.unmark v)
| SubScopeVar (scope_name, _, v) ->
Env.get_subscope_var env scope_name (Marked.unmark v)
in
match ty with
| Some ty -> Bindlib.box (mark e1 (ast_to_typ ty))
| None ->
Errors.raise_spanned_error pos_e "Reference to %a not found"
(Expr.format ctx) e)
| A.EStruct (s_name, fmap) ->
let+ fmap' =
(* This assumes that the fields in fmap and the struct type are already
ensured to be the same *)
List.fold_left
(fun fmap' (f_name, f_ty) ->
let f_e = A.StructFieldMap.find f_name fmap in
let+ fmap'
and+ f_e' = typecheck_expr_top_down ctx env (ast_to_typ f_ty) f_e in
A.StructFieldMap.add f_name f_e' fmap')
(Bindlib.box A.StructFieldMap.empty)
(A.StructMap.find s_name ctx.A.ctx_structs)
in
mark_with_uf (A.EStruct (s_name, fmap')) (TStruct s_name)
| A.EStructAccess (e_struct, f_name, s_name) ->
let f_ty =
ast_to_typ (List.assoc f_name (A.StructMap.find s_name ctx.A.ctx_structs))
in
let+ e_struct' =
typecheck_expr_top_down ctx env (unionfind_make (TStruct s_name)) e_struct
in
mark (A.EStructAccess (e_struct', f_name, s_name)) f_ty
| A.EEnumInj (e_enum, c_name, e_name) ->
let c_ty =
ast_to_typ (List.assoc c_name (A.EnumMap.find e_name ctx.A.ctx_enums))
in
let+ e_enum' = typecheck_expr_top_down ctx env c_ty e_enum in
mark (A.EEnumInj (e_enum', c_name, e_name)) (unionfind_make (TEnum e_name))
| A.EMatchS (e1, e_name, cases) ->
let cases_ty = A.EnumMap.find e_name ctx.A.ctx_enums in
let t_ret = unionfind_make ~pos:e1 (TAny (Any.fresh ())) in
let+ e1' =
typecheck_expr_top_down ctx env (unionfind_make (TEnum e_name)) e1
and+ cases' =
A.EnumConstructorMap.fold
(fun c_name e cases' ->
let c_ty = List.assoc c_name cases_ty in
let e_ty = unionfind_make ~pos:e (TArrow (ast_to_typ c_ty, t_ret)) in
let+ cases' and+ e' = typecheck_expr_top_down ctx env e_ty e in
A.EnumConstructorMap.add c_name e' cases')
cases
(Bindlib.box A.EnumConstructorMap.empty)
in
mark (A.EMatchS (e1', e_name, cases')) t_ret
| A.ERaise ex ->
Bindlib.box (mark_with_uf (A.ERaise ex) (TAny (Any.fresh ())))
| A.ECatch (e1, ex, e2) ->
let+ e1' = typecheck_expr_bottom_up ctx env e1
and+ e2' = typecheck_expr_bottom_up ctx env e2 in
let e_ty = ty e1' in
unify ctx e e_ty (ty e2');
mark (A.ECatch (e1', ex, e2')) e_ty
| A.EVar v -> begin
match A.Var.Map.find_opt v env with
match Env.get env v with
| Some t ->
let+ v' = Bindlib.box_var (A.Var.translate v) in
let+ v' = Bindlib.box_var (Var.translate v) in
mark v' t
| None ->
Errors.raise_spanned_error (A.Expr.pos e)
Errors.raise_spanned_error (Expr.pos e)
"Variable %s not found in the current context." (Bindlib.name_of v)
end
| A.ELit (LBool _) as e1 -> Bindlib.box @@ mark_with_uf e1 (TLit TBool)
| A.ELit (LInt _) as e1 -> Bindlib.box @@ mark_with_uf e1 (TLit TInt)
| A.ELit (LRat _) as e1 -> Bindlib.box @@ mark_with_uf e1 (TLit TRat)
| A.ELit (LMoney _) as e1 -> Bindlib.box @@ mark_with_uf e1 (TLit TMoney)
| A.ELit (LDate _) as e1 -> Bindlib.box @@ mark_with_uf e1 (TLit TDate)
| A.ELit (LDuration _) as e1 ->
Bindlib.box @@ mark_with_uf e1 (TLit TDuration)
| A.ELit LUnit as e1 -> Bindlib.box @@ mark_with_uf e1 (TLit TUnit)
| A.ELit LEmptyError as e1 ->
Bindlib.box @@ mark_with_uf e1 (TAny (Any.fresh ()))
| A.ELit lit as e1 -> Bindlib.box @@ mark_with_uf e1 (lit_type lit)
| A.ETuple (es, None) ->
let+ es = bmap (typecheck_expr_bottom_up ctx env) es in
mark_with_uf (ETuple (es, None)) (TTuple (List.map ty es))
mark_with_uf (A.ETuple (es, None)) (TTuple (List.map ty es))
| A.ETuple (es, Some s_name) ->
let tys =
List.map
@ -339,13 +441,13 @@ let rec typecheck_expr_bottom_up
(A.StructMap.find s_name ctx.A.ctx_structs)
in
let+ es = bmap2 (typecheck_expr_top_down ctx env) tys es in
mark_with_uf (ETuple (es, Some s_name)) (TStruct s_name)
mark_with_uf (A.ETuple (es, Some s_name)) (TStruct s_name)
| A.ETupleAccess (e1, n, s, typs) -> begin
let utyps = List.map ast_to_typ typs in
let tuple_ty = match s with None -> TTuple utyps | Some s -> TStruct s in
let+ e1 = typecheck_expr_top_down ctx env (unionfind_make tuple_ty) e1 in
match List.nth_opt utyps n with
| Some t' -> mark (ETupleAccess (e1, n, s, typs)) t'
| Some t' -> mark (A.ETupleAccess (e1, n, s, typs)) t'
| None ->
Errors.raise_spanned_error (Marked.get_mark e1).pos
"Expression should have a tuple type with at least %d elements but \
@ -358,7 +460,7 @@ let rec typecheck_expr_bottom_up
match List.nth_opt ts' n with
| Some ts_n -> ts_n
| None ->
Errors.raise_spanned_error (A.Expr.pos e)
Errors.raise_spanned_error (Expr.pos e)
"Expression should have a sum type with at least %d cases but only \
has %d"
n (List.length ts')
@ -380,19 +482,19 @@ let rec typecheck_expr_bottom_up
es')
es enum_cases
in
mark (EMatch (e1', es', e_name)) t_ret
mark (A.EMatch (e1', es', e_name)) t_ret
| A.EAbs (binder, taus) ->
if Bindlib.mbinder_arity binder <> List.length taus then
Errors.raise_spanned_error (A.Expr.pos e)
Errors.raise_spanned_error (Expr.pos e)
"function has %d variables but was supplied %d types"
(Bindlib.mbinder_arity binder)
(List.length taus)
else
let xs, body = Bindlib.unmbind binder in
let xs' = Array.map A.Var.translate xs in
let xs' = Array.map Var.translate xs in
let xstaus = List.mapi (fun i tau -> xs.(i), ast_to_typ tau) taus in
let env =
List.fold_left (fun env (x, tau) -> A.Var.Map.add x tau env) env xstaus
List.fold_left (fun env (x, tau) -> Env.add x tau env) env xstaus
in
let body' = typecheck_expr_bottom_up ctx env body in
let t_func =
@ -401,7 +503,7 @@ let rec typecheck_expr_bottom_up
xstaus (box_ty body')
in
let+ binder' = Bindlib.bind_mvar xs' body' in
mark (EAbs (binder', taus)) t_func
mark (A.EAbs (binder', taus)) t_func
| A.EApp (e1, args) ->
let args' = bmap (typecheck_expr_bottom_up ctx env) args in
let t_ret = unionfind_make (TAny (Any.fresh ())) in
@ -413,7 +515,7 @@ let rec typecheck_expr_bottom_up
in
let+ e1' = typecheck_expr_bottom_up ctx env e1 and+ args' in
unify ctx e (ty e1') t_func;
mark (EApp (e1', args')) t_ret
mark (A.EApp (e1', args')) t_ret
| A.EOp op as e1 -> Bindlib.box @@ mark e1 (op_type (Marked.mark pos_e op))
| A.EDefault (excepts, just, cons) ->
let just' =
@ -443,7 +545,7 @@ let rec typecheck_expr_bottom_up
let+ e1' =
typecheck_expr_top_down ctx env (unionfind_make ~pos:e1 (TLit TBool)) e1
in
mark_with_uf (A.EAssert e1') ~pos:e1 (TLit TUnit)
mark_with_uf (A.EAssert e1') (TLit TUnit)
| A.ErrorOnEmpty e1 ->
let+ e1' = typecheck_expr_bottom_up ctx env e1 in
mark (A.ErrorOnEmpty e1') (ty e1')
@ -460,184 +562,250 @@ let rec typecheck_expr_bottom_up
mark_with_uf (A.EArray es') (TArray cell_type)
(** Checks whether the expression can be typed with the provided type *)
and typecheck_expr_top_down
(ctx : A.decl_ctx)
(env : 'm Ast.expr env)
(tau : unionfind_typ)
(e : 'm Ast.expr) : (A.dcalc, mark) A.gexpr Bindlib.box =
and typecheck_expr_top_down :
type a m.
A.decl_ctx ->
(a, m A.mark) A.gexpr Env.t ->
unionfind_typ ->
(a, m A.mark) A.gexpr ->
(a, mark) A.gexpr Bindlib.box =
fun ctx env tau e ->
(* Cli.debug_format "Propagating type %a for naked_expr %a" (format_typ ctx)
tau (Expr.format ctx) e; *)
let pos_e = A.Expr.pos e in
let pos_e = Expr.pos e in
let () =
(* If there already is a type annotation on the given expr, ensure it
matches *)
match Marked.get_mark e with
| A.Untyped _ | A.Typed { A.ty = A.TAny, _; _ } -> ()
| A.Typed { A.ty; _ } -> unify ctx e tau (ast_to_typ ty)
in
let mark e = Marked.mark { uf = tau; pos = pos_e } e in
let unify_and_mark (e' : (A.dcalc, mark) A.naked_gexpr) tau' =
(* This try...with was added because of
[tests/test_bool/bad/bad_assert.catala_en] but we shouldn't need it.
TODO: debug why it is needed here. *)
(try unify ctx e tau tau'
with Type_error (e', t1, t2) -> handle_type_error ctx e' t1 t2);
Marked.mark { uf = tau; pos = pos_e } e'
let unify_and_mark tau' f_e =
unify ctx e tau' tau;
Bindlib.box_apply (Marked.mark { uf = tau; pos = pos_e }) (f_e ())
in
let unionfind_make ?(pos = e) t = UnionFind.make (add_pos pos t) in
match Marked.unmark e with
| A.EVar v -> begin
match A.Var.Map.find_opt v env with
| Some tau' ->
let+ v' = Bindlib.box_var (A.Var.translate v) in
unify_and_mark v' tau'
| A.ELocation loc as e1 -> (
let ty =
match loc with
| DesugaredScopeVar (v, _) | ScopelangScopeVar v ->
Env.get_scope_var env (Marked.unmark v)
| SubScopeVar (scope, _, v) ->
Env.get_subscope_var env scope (Marked.unmark v)
in
match ty with
| Some ty -> unify_and_mark (ast_to_typ ty) (fun () -> Bindlib.box e1)
| None ->
Errors.raise_spanned_error pos_e
"Variable %s not found in the current context" (Bindlib.name_of v)
end
| A.ELit (LBool _) as e1 ->
Bindlib.box @@ unify_and_mark e1 (unionfind_make (TLit TBool))
| A.ELit (LInt _) as e1 ->
Bindlib.box @@ unify_and_mark e1 (unionfind_make (TLit TInt))
| A.ELit (LRat _) as e1 ->
Bindlib.box @@ unify_and_mark e1 (unionfind_make (TLit TRat))
| A.ELit (LMoney _) as e1 ->
Bindlib.box @@ unify_and_mark e1 (unionfind_make (TLit TMoney))
| A.ELit (LDate _) as e1 ->
Bindlib.box @@ unify_and_mark e1 (unionfind_make (TLit TDate))
| A.ELit (LDuration _) as e1 ->
Bindlib.box @@ unify_and_mark e1 (unionfind_make (TLit TDuration))
| A.ELit LUnit as e1 ->
Bindlib.box @@ unify_and_mark e1 (unionfind_make (TLit TUnit))
| A.ELit LEmptyError as e1 ->
Bindlib.box @@ unify_and_mark e1 (unionfind_make (TAny (Any.fresh ())))
| A.ETuple (es, None) ->
let+ es' = bmap (typecheck_expr_bottom_up ctx env) es in
Errors.raise_spanned_error pos_e "Reference to %a not found"
(Expr.format ctx) e)
| A.EStruct (s_name, fmap) ->
unify_and_mark (unionfind_make (TStruct s_name))
@@ fun () ->
let+ fmap' =
(* This assumes that the fields in fmap and the struct type are already
ensured to be the same *)
List.fold_left
(fun fmap' (f_name, f_ty) ->
let f_e = A.StructFieldMap.find f_name fmap in
let+ fmap'
and+ f_e' = typecheck_expr_top_down ctx env (ast_to_typ f_ty) f_e in
A.StructFieldMap.add f_name f_e' fmap')
(Bindlib.box A.StructFieldMap.empty)
(A.StructMap.find s_name ctx.A.ctx_structs)
in
A.EStruct (s_name, fmap')
| A.EStructAccess (e_struct, f_name, s_name) ->
unify_and_mark
(A.ETuple (es', None))
(unionfind_make (TTuple (List.map ty es')))
(ast_to_typ
(List.assoc f_name (A.StructMap.find s_name ctx.A.ctx_structs)))
@@ fun () ->
let+ e_struct' =
typecheck_expr_top_down ctx env (unionfind_make (TStruct s_name)) e_struct
in
A.EStructAccess (e_struct', f_name, s_name)
| A.EEnumInj (e_enum, c_name, e_name) ->
unify_and_mark (unionfind_make (TEnum e_name))
@@ fun () ->
let+ e_enum' =
typecheck_expr_top_down ctx env
(ast_to_typ (List.assoc c_name (A.EnumMap.find e_name ctx.A.ctx_enums)))
e_enum
in
A.EEnumInj (e_enum', c_name, e_name)
| A.EMatchS (e1, e_name, cases) ->
let cases_ty = A.EnumMap.find e_name ctx.A.ctx_enums in
let t_ret = unionfind_make ~pos:e1 (TAny (Any.fresh ())) in
unify_and_mark t_ret
@@ fun () ->
let+ e1' =
typecheck_expr_top_down ctx env (unionfind_make (TEnum e_name)) e1
and+ cases' =
A.EnumConstructorMap.fold
(fun c_name e cases' ->
let c_ty = List.assoc c_name cases_ty in
let e_ty = unionfind_make ~pos:e (TArrow (ast_to_typ c_ty, t_ret)) in
let+ cases' and+ e' = typecheck_expr_top_down ctx env e_ty e in
A.EnumConstructorMap.add c_name e' cases')
cases
(Bindlib.box A.EnumConstructorMap.empty)
in
A.EMatchS (e1', e_name, cases')
| A.ERaise _ as e1 -> Bindlib.box (mark e1)
| A.ECatch (e1, ex, e2) ->
let+ e1' = typecheck_expr_top_down ctx env tau e1
and+ e2' = typecheck_expr_top_down ctx env tau e2 in
mark (A.ECatch (e1', ex, e2'))
| A.EVar v ->
let tau' =
match Env.get env v with
| Some t -> t
| None ->
Errors.raise_spanned_error pos_e
"Variable %s not found in the current context" (Bindlib.name_of v)
in
unify_and_mark tau' @@ fun () -> Bindlib.box_var (Var.translate v)
| A.ELit lit as e1 ->
unify_and_mark (unionfind_make (lit_type lit))
@@ fun () -> Bindlib.box @@ e1
| A.ETuple (es, None) ->
let tys = List.map (fun _ -> unionfind_make (TAny (Any.fresh ()))) es in
unify_and_mark (unionfind_make (TTuple tys))
@@ fun () ->
let+ es' = bmap2 (typecheck_expr_top_down ctx env) tys es in
A.ETuple (es', None)
| A.ETuple (es, Some s_name) ->
let tys =
List.map
(fun (_, ty) -> ast_to_typ ty)
(A.StructMap.find s_name ctx.A.ctx_structs)
in
unify_and_mark (unionfind_make (TStruct s_name))
@@ fun () ->
let+ es' = bmap2 (typecheck_expr_top_down ctx env) tys es in
unify_and_mark
(A.ETuple (es', Some s_name))
(unionfind_make (TStruct s_name))
| A.ETupleAccess (e1, n, s, typs) -> begin
A.ETuple (es', Some s_name)
| A.ETupleAccess (e1, n, s, typs) ->
let typs' = List.map ast_to_typ typs in
let tuple_ty = match s with None -> TTuple typs' | Some s -> TStruct s in
let t1n =
try List.nth typs' n
with Not_found ->
Errors.raise_spanned_error (Expr.pos e1)
"Expression should have a tuple type with at least %d elements but \
only has %d"
n (List.length typs)
in
unify_and_mark t1n
@@ fun () ->
let+ e1' = typecheck_expr_top_down ctx env (unionfind_make tuple_ty) e1 in
match List.nth_opt typs' n with
| Some t1n -> unify_and_mark (A.ETupleAccess (e1', n, s, typs)) t1n
| None ->
Errors.raise_spanned_error (A.Expr.pos e1)
"Expression should have a tuple type with at least %d elements but \
only has %d"
n (List.length typs)
end
A.ETupleAccess (e1', n, s, typs)
| A.EInj (e1, n, e_name, ts) ->
let ts' = List.map ast_to_typ ts in
let ts_n =
match List.nth_opt ts' n with
| Some ts_n -> ts_n
| None ->
Errors.raise_spanned_error (A.Expr.pos e)
try List.nth ts' n
with Not_found ->
Errors.raise_spanned_error (Expr.pos e)
"Expression should have a sum type with at least %d cases but only \
has %d"
n (List.length ts)
in
unify_and_mark (unionfind_make (TEnum e_name))
@@ fun () ->
let+ e1' = typecheck_expr_top_down ctx env ts_n e1 in
unify_and_mark (A.EInj (e1', n, e_name, ts)) (unionfind_make (TEnum e_name))
A.EInj (e1', n, e_name, ts)
| A.EMatch (e1, es, e_name) ->
let enum_cases =
List.map (fun e' -> unionfind_make ~pos:e' (TAny (Any.fresh ()))) es
in
let e1' =
let+ es' =
bmap2
(fun es' (_, c_ty) ->
typecheck_expr_top_down ctx env
(unionfind_make ~pos:es' (TArrow (ast_to_typ c_ty, tau)))
es')
es
(A.EnumMap.find e_name ctx.ctx_enums)
and+ e1' =
typecheck_expr_top_down ctx env (unionfind_make ~pos:e1 (TEnum e_name)) e1
in
let t_ret = unionfind_make ~pos:e (TAny (Any.fresh ())) in
let+ e1'
and+ es' =
bmap2
(fun es' enum_t ->
typecheck_expr_top_down ctx env
(unionfind_make ~pos:es' (TArrow (enum_t, t_ret)))
es')
es enum_cases
in
unify_and_mark (EMatch (e1', es', e_name)) t_ret
mark (A.EMatch (e1', es', e_name))
| A.EAbs (binder, t_args) ->
if Bindlib.mbinder_arity binder <> List.length t_args then
Errors.raise_spanned_error (A.Expr.pos e)
Errors.raise_spanned_error (Expr.pos e)
"function has %d variables but was supplied %d types"
(Bindlib.mbinder_arity binder)
(List.length t_args)
else
let xs, body = Bindlib.unmbind binder in
let xs' = Array.map A.Var.translate xs in
let xstaus =
List.map2 (fun x t_arg -> x, ast_to_typ t_arg) (Array.to_list xs) t_args
in
let env =
List.fold_left
(fun env (x, t_arg) -> A.Var.Map.add x t_arg env)
env xstaus
in
let body' = typecheck_expr_bottom_up ctx env body in
let tau_args = List.map ast_to_typ t_args in
let t_ret = unionfind_make (TAny (Any.fresh ())) in
let t_func =
List.fold_right
(fun (_, t_arg) acc -> unionfind_make (TArrow (t_arg, acc)))
xstaus (box_ty body')
(fun t_arg acc -> unionfind_make (TArrow (t_arg, acc)))
tau_args t_ret
in
unify_and_mark t_func
@@ fun () ->
let xs, body = Bindlib.unmbind binder in
let xs' = Array.map Var.translate xs in
let env =
List.fold_left2
(fun env x tau_arg -> Env.add x tau_arg env)
env (Array.to_list xs) tau_args
in
let body' = typecheck_expr_top_down ctx env t_ret body in
let+ binder' = Bindlib.bind_mvar xs' body' in
unify_and_mark (EAbs (binder', t_args)) t_func
A.EAbs (binder', t_args)
| A.EApp (e1, args) ->
let+ args' = bmap (typecheck_expr_bottom_up ctx env) args
and+ e1' = typecheck_expr_bottom_up ctx env e1 in
let t_args =
List.map (fun _ -> unionfind_make (TAny (Any.fresh ()))) args
in
let t_func =
List.fold_right
(fun arg acc -> unionfind_make (TArrow (ty arg, acc)))
args' tau
(fun t_arg acc -> unionfind_make (TArrow (t_arg, acc)))
t_args tau
in
unify ctx e (ty e1') t_func;
unify_and_mark (EApp (e1', args')) tau
let+ e1' = typecheck_expr_top_down ctx env t_func e1
and+ args' = bmap2 (typecheck_expr_top_down ctx env) t_args args in
mark (A.EApp (e1', args'))
| A.EOp op as e1 ->
let op_typ = op_type (add_pos e op) in
Bindlib.box (unify_and_mark e1 op_typ)
unify_and_mark (op_type (add_pos e op)) @@ fun () -> Bindlib.box e1
| A.EDefault (excepts, just, cons) ->
let+ just' =
let+ cons' = typecheck_expr_top_down ctx env tau cons
and+ just' =
typecheck_expr_top_down ctx env
(unionfind_make ~pos:just (TLit TBool))
just
and+ cons' = typecheck_expr_top_down ctx env tau cons
and+ excepts' = bmap (typecheck_expr_top_down ctx env tau) excepts in
mark (A.EDefault (excepts', just', cons'))
| A.EIfThenElse (cond, et, ef) ->
let+ cond' =
let+ et' = typecheck_expr_top_down ctx env tau et
and+ ef' = typecheck_expr_top_down ctx env tau ef
and+ cond' =
typecheck_expr_top_down ctx env
(unionfind_make ~pos:cond (TLit TBool))
cond
and+ et' = typecheck_expr_top_down ctx env tau et
and+ ef' = typecheck_expr_top_down ctx env tau ef in
in
mark (A.EIfThenElse (cond', et', ef'))
| A.EAssert e1 ->
unify_and_mark (unionfind_make (TLit TUnit))
@@ fun () ->
let+ e1' =
typecheck_expr_top_down ctx env (unionfind_make ~pos:e1 (TLit TBool)) e1
in
unify_and_mark (EAssert e1') (unionfind_make ~pos:e1 (TLit TUnit))
A.EAssert e1'
| A.ErrorOnEmpty e1 ->
let+ e1' = typecheck_expr_top_down ctx env tau e1 in
mark (A.ErrorOnEmpty e1')
| A.EArray es ->
let cell_type = unionfind_make (TAny (Any.fresh ())) in
let+ es' =
bmap
(fun e1 ->
let e1' = typecheck_expr_bottom_up ctx env e1 in
unify ctx e cell_type (box_ty e1');
e1')
es
in
unify_and_mark (A.EArray es') (unionfind_make (TArray cell_type))
unify_and_mark (unionfind_make (TArray cell_type))
@@ fun () ->
let+ es' = bmap (typecheck_expr_top_down ctx env cell_type) es in
A.EArray es'
let wrap ctx f e =
try f e
try
Bindlib.unbox (f e)
(* We need to unbox here, because the typing may otherwise be stored in
Bindlib closures and not yet applied, and would escape the `try..with` *)
with Type_error (e, ty1, ty2) -> (
let bt = Printexc.get_raw_backtrace () in
try handle_type_error ctx e ty1 ty2
@ -648,111 +816,95 @@ let wrap ctx f e =
let get_ty_mark { uf; pos } = A.Typed { ty = typ_to_ast uf; pos }
(* Infer the type of an expression *)
let infer_types (ctx : A.decl_ctx) (e : 'm Ast.expr) :
A.typed Ast.expr Bindlib.box =
A.Expr.map_marks ~f:get_ty_mark
@@ Bindlib.unbox
@@ wrap ctx (typecheck_expr_bottom_up ctx A.Var.Map.empty) e
let infer_type (type m) ctx (e : m Ast.expr) =
match Marked.get_mark e with
| A.Typed { ty; _ } -> ty
| A.Untyped _ -> A.Expr.ty (Bindlib.unbox (infer_types ctx e))
(** Typechecks an expression given an expected type *)
let check_type (ctx : A.decl_ctx) (e : 'm Ast.expr) (tau : A.typ) =
(* todo: consider using the already inferred type if ['m] = [typed] *)
ignore
@@ wrap ctx (typecheck_expr_top_down ctx A.Var.Map.empty (ast_to_typ tau)) e
let infer_types_program prg =
let ctx = prg.A.decl_ctx in
let rec process_scopes env = function
| A.Nil -> Bindlib.box A.Nil
| A.ScopeDef
{
scope_next;
scope_name;
scope_body =
{
scope_body_input_struct = s_in;
scope_body_output_struct = s_out;
scope_body_expr = body;
};
} ->
let scope_pos = Marked.get_mark (A.ScopeName.get_info scope_name) in
let struct_ty struct_name =
UnionFind.make (Marked.mark scope_pos (TStruct struct_name))
in
let ty_in = struct_ty s_in in
let ty_out = struct_ty s_out in
let ty_scope =
UnionFind.make (Marked.mark scope_pos (TArrow (ty_in, ty_out)))
in
let rec process_scope_body_expr env = function
| A.Result e ->
let e' = wrap ctx (typecheck_expr_bottom_up ctx env) e in
Bindlib.box_apply
(fun e1 ->
wrap ctx (unify ctx e (ty e1)) ty_out;
let e1 = A.Expr.map_marks ~f:get_ty_mark e1 in
A.Result (Bindlib.unbox e1))
e'
| A.ScopeLet
{
scope_let_kind;
scope_let_typ;
scope_let_expr = e0;
scope_let_next;
scope_let_pos;
} ->
let ty_e = ast_to_typ scope_let_typ in
let e = wrap ctx (typecheck_expr_bottom_up ctx env) e0 in
let var, next = Bindlib.unbind scope_let_next in
let env = A.Var.Map.add var ty_e env in
let next = process_scope_body_expr env next in
let scope_let_next = Bindlib.bind_var (A.Var.translate var) next in
Bindlib.box_apply2
(fun e scope_let_next ->
wrap ctx (unify ctx e0 (ty e)) ty_e;
let e = A.Expr.map_marks ~f:get_ty_mark e in
A.ScopeLet
{
scope_let_kind;
scope_let_typ;
scope_let_expr = Bindlib.unbox e;
scope_let_next;
scope_let_pos;
})
e scope_let_next
in
let scope_body_expr =
let var, e = Bindlib.unbind body in
let env = A.Var.Map.add var ty_in env in
let e' = process_scope_body_expr env e in
Bindlib.bind_var (A.Var.translate var) e'
in
let scope_next =
let scope_var, next = Bindlib.unbind scope_next in
let env = A.Var.Map.add scope_var ty_scope env in
let next' = process_scopes env next in
Bindlib.bind_var (A.Var.translate scope_var) next'
in
Bindlib.box_apply2
(fun scope_body_expr scope_next ->
A.ScopeDef
{
scope_next;
scope_name;
scope_body =
{
scope_body_input_struct = s_in;
scope_body_output_struct = s_out;
scope_body_expr;
};
})
scope_body_expr scope_next
let expr
(type a)
(ctx : A.decl_ctx)
?(env = Env.empty)
?(typ : A.typ option)
(e : (a, 'm) A.gexpr) : (a, A.typed A.mark) A.gexpr A.box =
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
let scopes = wrap ctx (process_scopes A.Var.Map.empty) prg.scopes in
Bindlib.box_apply (fun scopes -> { A.decl_ctx = ctx; scopes }) scopes
|> Bindlib.unbox
Expr.map_marks ~f:get_ty_mark (wrap ctx fty e)
let rec scope_body_expr ctx env ty_out body_expr =
match body_expr with
| A.Result e ->
let e' = wrap ctx (typecheck_expr_top_down ctx env ty_out) e in
let e' = Expr.map_marks ~f:get_ty_mark e' in
Bindlib.box_apply (fun e -> A.Result e) e'
| A.ScopeLet
{
scope_let_kind;
scope_let_typ;
scope_let_expr = e0;
scope_let_next;
scope_let_pos;
} ->
let ty_e = ast_to_typ scope_let_typ in
let e = wrap ctx (typecheck_expr_bottom_up ctx env) e0 in
wrap ctx (fun t -> Bindlib.box (unify ctx e0 (ty e) t)) ty_e;
(* We could use [typecheck_expr_top_down] rather than this manual
unification, but we get better messages with this order of the [unify]
parameters, which keeps location of the type as defined instead of as
inferred. *)
let var, next = Bindlib.unbind scope_let_next in
let env = Env.add var ty_e env in
let next = scope_body_expr ctx env ty_out next in
let scope_let_next = Bindlib.bind_var (Var.translate var) next in
Bindlib.box_apply2
(fun scope_let_expr scope_let_next ->
A.ScopeLet
{
scope_let_kind;
scope_let_typ;
scope_let_expr;
scope_let_next;
scope_let_pos;
})
(Expr.map_marks ~f:get_ty_mark e)
scope_let_next
let scope_body ctx env body =
let get_pos struct_name =
Marked.get_mark (A.StructName.get_info struct_name)
in
let struct_ty struct_name =
UnionFind.make (Marked.mark (get_pos struct_name) (TStruct struct_name))
in
let ty_in = struct_ty body.A.scope_body_input_struct in
let ty_out = struct_ty body.A.scope_body_output_struct in
let var, e = Bindlib.unbind body.A.scope_body_expr in
let env = Env.add var ty_in env in
let e' = scope_body_expr ctx env ty_out e in
( Bindlib.bind_var (Var.translate var) e',
UnionFind.make
(Marked.mark
(get_pos body.A.scope_body_output_struct)
(TArrow (ty_in, ty_out))) )
let rec scopes ctx env = function
| A.Nil -> Bindlib.box A.Nil
| A.ScopeDef def ->
let body_e, ty_scope = scope_body ctx env def.scope_body in
let scope_next =
let scope_var, next = Bindlib.unbind def.scope_next in
let env = Env.add scope_var ty_scope env in
let next' = scopes ctx env next in
Bindlib.bind_var (Var.translate scope_var) next'
in
Bindlib.box_apply2
(fun scope_body_expr scope_next ->
A.ScopeDef
{
def with
scope_body = { def.scope_body with scope_body_expr };
scope_next;
})
body_e scope_next
let program prg =
let scopes = Bindlib.unbox (scopes prg.A.decl_ctx Env.empty prg.A.scopes) in
{ prg with scopes }

52
compiler/shared_ast/typing.mli Normal file
View File

@ -0,0 +1,52 @@
(* This file is part of the Catala compiler, a specification language for tax
and social benefits computation rules. Copyright (C) 2020 Inria, contributor:
Denis Merigoux <denis.merigoux@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. *)
(** Typing for the default calculus. Because of the error terms, we perform type
inference using the classical W algorithm with union-find unification. *)
open Definitions
module Env : sig
type 'e t
val empty : 'e t
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 -> typ ScopeVarMap.t -> 'e t -> 'e t
end
val expr :
decl_ctx ->
?env:'e Env.t ->
?typ:typ ->
(('a, 'm mark) gexpr as 'e) ->
('a, typed mark) gexpr box
(** Infers and marks the types for the given expression. If [typ] is provided,
it is assumed to be the outer type and used for inference top-down.
If the input expression already has type annotations, the full inference is
still done, but with unification with the existing annotations at every
step. This can be used for double-checking after AST transformations and
filling the gaps ([TAny]) if any. Use [Expr.untype] first if this is not
what you want. *)
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.
Any existing type annotations are checked for unification. Use
[Program.untype] to remove them beforehand if this is not the desired
behaviour. *)

51
compiler/surface/desugaring.ml
View File

@ -125,7 +125,7 @@ let rec translate_expr
(inside_definition_of : Desugared.Ast.ScopeDef.t Marked.pos option)
(ctxt : Name_resolution.context)
(expr : Ast.expression Marked.pos) : Desugared.Ast.expr Bindlib.box =
let scope_ctxt = Scopelang.Ast.ScopeMap.find scope ctxt.scopes in
let scope_ctxt = ScopeMap.find scope ctxt.scopes in
let rec_helper = translate_expr scope inside_definition_of ctxt in
let pos = Marked.get_mark expr in
let emark = Untyped { pos } in
@ -148,13 +148,13 @@ let rec translate_expr
Bindlib.unbox
(Expr.make_abs [| nop_var |]
(Bindlib.box (ELit (LBool false), emark))
[tau] emark)
[tau] pos)
else
let ctxt, binding_var =
Name_resolution.add_def_local_var ctxt (Marked.unmark binding)
in
let e2 = translate_expr scope inside_definition_of ctxt e2 in
Bindlib.unbox (Expr.make_abs [| binding_var |] e2 [tau] emark))
Bindlib.unbox (Expr.make_abs [| binding_var |] e2 [tau] pos))
(EnumMap.find enum_uid ctxt.enums)
in
Bindlib.box_apply
@ -284,7 +284,7 @@ let rec translate_expr
Name_resolution.get_subscope_uid scope ctxt (Marked.same_mark_as y e)
in
let subscope_real_uid : ScopeName.t =
Scopelang.Ast.SubScopeMap.find subscope_uid scope_ctxt.sub_scopes
SubScopeMap.find subscope_uid scope_ctxt.sub_scopes
in
let subscope_var_uid =
Name_resolution.get_var_uid subscope_real_uid ctxt x
@ -344,7 +344,7 @@ let rec translate_expr
let fn =
Expr.make_abs [| v |]
(translate_expr scope inside_definition_of ctxt e2)
[tau] emark
[tau] pos
in
Bindlib.box_apply2
(fun fn arg -> EApp (fn, [arg]), emark)
@ -491,7 +491,7 @@ let rec translate_expr
(Bindlib.box
( ELit (LBool (EnumConstructor.compare c_uid c_uid' = 0)),
emark ))
[tau] emark))
[tau] pos))
(EnumMap.find enum_uid ctxt.enums)
in
Bindlib.box_apply
@ -514,7 +514,7 @@ let rec translate_expr
Expr.make_abs [| param |]
(translate_expr scope inside_definition_of ctxt predicate)
[TAny, pos]
emark
pos
in
Bindlib.box_apply2
(fun f_pred collection ->
@ -557,7 +557,7 @@ let rec translate_expr
Expr.make_abs [| param |]
(translate_expr scope inside_definition_of ctxt predicate)
[TAny, pos]
emark
pos
in
let f_pred_var = Var.make "predicate" in
let f_pred_var_e =
@ -586,9 +586,7 @@ let rec translate_expr
acc_var_e item_var_e f_pred_var_e
in
let fold_f =
Expr.make_abs [| acc_var; item_var |] fold_body
[TAny, pos; TAny, pos]
emark
Expr.make_abs [| acc_var; item_var |] fold_body [TAny, pos; TAny, pos] pos
in
let fold =
Bindlib.box_apply3
@ -680,7 +678,7 @@ let rec translate_expr
| Ast.Date -> KDate, (TLit TDate, pos)
| _ ->
Errors.raise_spanned_error pos
"ssible to compute the %s of two values of type %a"
"It is impossible to compute the %s of two values of type %a"
(if max_or_min then "max" else "min")
SurfacePrint.format_primitive_typ t
in
@ -995,14 +993,14 @@ let process_def
(prgm : Desugared.Ast.program)
(def : Ast.definition) : Desugared.Ast.program =
let scope : Desugared.Ast.scope =
Scopelang.Ast.ScopeMap.find scope_uid prgm.program_scopes
ScopeMap.find scope_uid prgm.program_scopes
in
let scope_ctxt = Scopelang.Ast.ScopeMap.find scope_uid ctxt.scopes in
let scope_ctxt = ScopeMap.find scope_uid ctxt.scopes in
let def_key =
Name_resolution.get_def_key
(Marked.unmark def.definition_name)
def.definition_state scope_uid ctxt
(Marked.get_mark def.definition_expr)
(Marked.get_mark def.definition_name)
in
let scope_def_ctxt =
Desugared.Ast.ScopeDefMap.find def_key scope_ctxt.scope_defs_contexts
@ -1072,8 +1070,7 @@ let process_def
in
{
prgm with
program_scopes =
Scopelang.Ast.ScopeMap.add scope_uid scope_updated prgm.program_scopes;
program_scopes = ScopeMap.add scope_uid scope_updated prgm.program_scopes;
}
(** Translates a {!type: Surface.Ast.rule} from the surface language *)
@ -1094,7 +1091,7 @@ let process_assert
(prgm : Desugared.Ast.program)
(ass : Ast.assertion) : Desugared.Ast.program =
let scope : Desugared.Ast.scope =
Scopelang.Ast.ScopeMap.find scope_uid prgm.program_scopes
ScopeMap.find scope_uid prgm.program_scopes
in
let ass =
translate_expr scope_uid None ctxt
@ -1123,8 +1120,7 @@ let process_assert
in
{
prgm with
program_scopes =
Scopelang.Ast.ScopeMap.add scope_uid new_scope prgm.program_scopes;
program_scopes = ScopeMap.add scope_uid new_scope prgm.program_scopes;
}
(** Translates a surface definition, rule or assertion *)
@ -1149,7 +1145,7 @@ let check_unlabeled_exception
(scope : ScopeName.t)
(ctxt : Name_resolution.context)
(item : Ast.scope_use_item Marked.pos) : unit =
let scope_ctxt = Scopelang.Ast.ScopeMap.find scope ctxt.scopes in
let scope_ctxt = ScopeMap.find scope ctxt.scopes in
match Marked.unmark item with
| Ast.Rule _ | Ast.Definition _ -> (
let def_key, exception_to =
@ -1199,7 +1195,7 @@ let process_scope_use
let scope_uid = Desugared.Ast.IdentMap.find name ctxt.scope_idmap in
(* Make sure the scope exists *)
let prgm =
match Scopelang.Ast.ScopeMap.find_opt scope_uid prgm.program_scopes with
match ScopeMap.find_opt scope_uid prgm.program_scopes with
| Some _ -> prgm
| None -> assert false
(* should not happen *)
@ -1236,7 +1232,7 @@ let desugar_program (ctxt : Name_resolution.context) (prgm : Ast.program) :
EnumMap.map EnumConstructorMap.bindings ctxt.Name_resolution.enums;
};
Desugared.Ast.program_scopes =
Scopelang.Ast.ScopeMap.mapi
ScopeMap.mapi
(fun s_uid s_context ->
{
Desugared.Ast.scope_vars =
@ -1322,7 +1318,7 @@ let desugar_program (ctxt : Name_resolution.context) (prgm : Ast.program) :
Desugared.Ast.ScopeDefMap.empty
in
let scope_and_subscope_vars_defs =
Scopelang.Ast.SubScopeMap.fold
SubScopeMap.fold
(fun subscope_name subscope_uid acc ->
Desugared.Ast.IdentMap.fold
(fun _ v acc ->
@ -1331,7 +1327,9 @@ let desugar_program (ctxt : Name_resolution.context) (prgm : Ast.program) :
in
let def_key =
Desugared.Ast.ScopeDef.SubScopeVar
(subscope_name, v)
( subscope_name,
v,
Marked.get_mark (ScopeVar.get_info v) )
in
Desugared.Ast.ScopeDefMap.add def_key
{
@ -1344,8 +1342,7 @@ let desugar_program (ctxt : Name_resolution.context) (prgm : Ast.program) :
attribute_to_io v_sig.var_sig_io;
}
acc)
(Scopelang.Ast.ScopeMap.find subscope_uid
ctxt.Name_resolution.scopes)
(ScopeMap.find subscope_uid ctxt.Name_resolution.scopes)
.Name_resolution.var_idmap acc)
s_context.sub_scopes scope_vars_defs
in

50
compiler/surface/name_resolution.ml
View File

@ -40,7 +40,7 @@ type scope_context = {
(** What is the default rule to refer to for unnamed exceptions, if any *)
sub_scopes_idmap : SubScopeName.t Desugared.Ast.IdentMap.t;
(** Sub-scopes variables *)
sub_scopes : ScopeName.t Scopelang.Ast.SubScopeMap.t;
sub_scopes : ScopeName.t SubScopeMap.t;
(** To what scope sub-scopes refer to? *)
}
(** Inside a scope, we distinguish between the variables and the subscopes. *)
@ -75,8 +75,7 @@ type context = {
constructor_idmap : EnumConstructor.t EnumMap.t Desugared.Ast.IdentMap.t;
(** The names of the enum constructors. Constructor names can be shared
between different enums *)
scopes : scope_context Scopelang.Ast.ScopeMap.t;
(** For each scope, its context *)
scopes : scope_context ScopeMap.t; (** For each scope, its context *)
structs : struct_context StructMap.t; (** For each struct, its context *)
enums : enum_context EnumMap.t; (** For each enum, its context *)
var_typs : var_sig ScopeVarMap.t;
@ -114,7 +113,7 @@ let get_var_uid
(scope_uid : ScopeName.t)
(ctxt : context)
((x, pos) : ident Marked.pos) : ScopeVar.t =
let scope = Scopelang.Ast.ScopeMap.find scope_uid ctxt.scopes in
let scope = ScopeMap.find scope_uid ctxt.scopes in
match Desugared.Ast.IdentMap.find_opt x scope.var_idmap with
| None ->
raise_unknown_identifier
@ -127,7 +126,7 @@ let get_subscope_uid
(scope_uid : ScopeName.t)
(ctxt : context)
((y, pos) : ident Marked.pos) : SubScopeName.t =
let scope = Scopelang.Ast.ScopeMap.find scope_uid ctxt.scopes in
let scope = ScopeMap.find scope_uid ctxt.scopes in
match Desugared.Ast.IdentMap.find_opt y scope.sub_scopes_idmap with
| None -> raise_unknown_identifier "for a subscope of this scope" (y, pos)
| Some sub_uid -> sub_uid
@ -136,13 +135,13 @@ let get_subscope_uid
subscopes of [scope_uid]. *)
let is_subscope_uid (scope_uid : ScopeName.t) (ctxt : context) (y : ident) :
bool =
let scope = Scopelang.Ast.ScopeMap.find scope_uid ctxt.scopes in
let scope = ScopeMap.find scope_uid ctxt.scopes in
Desugared.Ast.IdentMap.mem y scope.sub_scopes_idmap
(** Checks if the var_uid belongs to the scope scope_uid *)
let belongs_to (ctxt : context) (uid : ScopeVar.t) (scope_uid : ScopeName.t) :
bool =
let scope = Scopelang.Ast.ScopeMap.find scope_uid ctxt.scopes in
let scope = ScopeMap.find scope_uid ctxt.scopes in
Desugared.Ast.IdentMap.exists
(fun _ var_uid -> ScopeVar.compare uid var_uid = 0)
scope.var_idmap
@ -150,7 +149,7 @@ let belongs_to (ctxt : context) (uid : ScopeVar.t) (scope_uid : ScopeName.t) :
(** Retrieves the type of a scope definition from the context *)
let get_def_typ (ctxt : context) (def : Desugared.Ast.ScopeDef.t) : typ =
match def with
| Desugared.Ast.ScopeDef.SubScopeVar (_, x)
| Desugared.Ast.ScopeDef.SubScopeVar (_, x, _)
(* we don't need to look at the subscope prefix because [x] is already the uid
referring back to the original subscope *)
| Desugared.Ast.ScopeDef.Var (x, _) ->
@ -158,7 +157,7 @@ let get_def_typ (ctxt : context) (def : Desugared.Ast.ScopeDef.t) : typ =
let is_def_cond (ctxt : context) (def : Desugared.Ast.ScopeDef.t) : bool =
match def with
| Desugared.Ast.ScopeDef.SubScopeVar (_, x)
| Desugared.Ast.ScopeDef.SubScopeVar (_, x, _)
(* we don't need to look at the subscope prefix because [x] is already the uid
referring back to the original subscope *)
| Desugared.Ast.ScopeDef.Var (x, _) ->
@ -173,7 +172,7 @@ let process_subscope_decl
(decl : Ast.scope_decl_context_scope) : context =
let name, name_pos = decl.scope_decl_context_scope_name in
let subscope, s_pos = decl.scope_decl_context_scope_sub_scope in
let scope_ctxt = Scopelang.Ast.ScopeMap.find scope ctxt.scopes in
let scope_ctxt = ScopeMap.find scope ctxt.scopes in
match
Desugared.Ast.IdentMap.find_opt subscope scope_ctxt.sub_scopes_idmap
with
@ -200,14 +199,11 @@ let process_subscope_decl
Desugared.Ast.IdentMap.add name sub_scope_uid
scope_ctxt.sub_scopes_idmap;
sub_scopes =
Scopelang.Ast.SubScopeMap.add sub_scope_uid original_subscope_uid
SubScopeMap.add sub_scope_uid original_subscope_uid
scope_ctxt.sub_scopes;
}
in
{
ctxt with
scopes = Scopelang.Ast.ScopeMap.add scope scope_ctxt ctxt.scopes;
}
{ ctxt with scopes = ScopeMap.add scope scope_ctxt ctxt.scopes }
let is_type_cond ((typ, _) : Ast.typ) =
match typ with
@ -264,7 +260,7 @@ let process_data_decl
let data_typ = process_type ctxt decl.scope_decl_context_item_typ in
let is_cond = is_type_cond decl.scope_decl_context_item_typ in
let name, pos = decl.scope_decl_context_item_name in
let scope_ctxt = Scopelang.Ast.ScopeMap.find scope ctxt.scopes in
let scope_ctxt = ScopeMap.find scope ctxt.scopes in
match Desugared.Ast.IdentMap.find_opt name scope_ctxt.var_idmap with
| Some use ->
Errors.raise_multispanned_error
@ -295,7 +291,7 @@ let process_data_decl
in
{
ctxt with
scopes = Scopelang.Ast.ScopeMap.add scope scope_ctxt ctxt.scopes;
scopes = ScopeMap.add scope scope_ctxt ctxt.scopes;
var_typs =
ScopeVarMap.add uid
{
@ -454,12 +450,12 @@ let process_name_item (ctxt : context) (item : Ast.code_item Marked.pos) :
ctxt with
scope_idmap = Desugared.Ast.IdentMap.add name scope_uid ctxt.scope_idmap;
scopes =
Scopelang.Ast.ScopeMap.add scope_uid
ScopeMap.add scope_uid
{
var_idmap = Desugared.Ast.IdentMap.empty;
scope_defs_contexts = Desugared.Ast.ScopeDefMap.empty;
sub_scopes_idmap = Desugared.Ast.IdentMap.empty;
sub_scopes = Scopelang.Ast.SubScopeMap.empty;
sub_scopes = SubScopeMap.empty;
}
ctxt.scopes;
})
@ -530,8 +526,8 @@ let get_def_key
(state : Ast.ident Marked.pos option)
(scope_uid : ScopeName.t)
(ctxt : context)
(default_pos : Pos.t) : Desugared.Ast.ScopeDef.t =
let scope_ctxt = Scopelang.Ast.ScopeMap.find scope_uid ctxt.scopes in
(pos : Pos.t) : Desugared.Ast.ScopeDef.t =
let scope_ctxt = ScopeMap.find scope_uid ctxt.scopes in
match name with
| [x] ->
let x_uid = get_var_uid scope_uid ctxt x in
@ -569,12 +565,12 @@ let get_def_key
| [y; x] ->
let subscope_uid : SubScopeName.t = get_subscope_uid scope_uid ctxt y in
let subscope_real_uid : ScopeName.t =
Scopelang.Ast.SubScopeMap.find subscope_uid scope_ctxt.sub_scopes
SubScopeMap.find subscope_uid scope_ctxt.sub_scopes
in
let x_uid = get_var_uid subscope_real_uid ctxt x in
Desugared.Ast.ScopeDef.SubScopeVar (subscope_uid, x_uid)
Desugared.Ast.ScopeDef.SubScopeVar (subscope_uid, x_uid, pos)
| _ ->
Errors.raise_spanned_error default_pos
Errors.raise_spanned_error pos
"This line is defining a quantity that is neither a scope variable nor a \
subscope variable. In particular, it is not possible to define struct \
fields individually in Catala."
@ -587,13 +583,13 @@ let process_definition
{
ctxt with
scopes =
Scopelang.Ast.ScopeMap.update s_name
ScopeMap.update s_name
(fun (s_ctxt : scope_context option) ->
let def_key =
get_def_key
(Marked.unmark d.definition_name)
d.definition_state s_name ctxt
(Marked.get_mark d.definition_expr)
(Marked.get_mark d.definition_name)
in
match s_ctxt with
| None -> assert false (* should not happen *)
@ -727,7 +723,7 @@ let form_context (prgm : Ast.program) : context =
{
local_var_idmap = Desugared.Ast.IdentMap.empty;
scope_idmap = Desugared.Ast.IdentMap.empty;
scopes = Scopelang.Ast.ScopeMap.empty;
scopes = ScopeMap.empty;
var_typs = ScopeVarMap.empty;
structs = StructMap.empty;
struct_idmap = Desugared.Ast.IdentMap.empty;

5
compiler/surface/name_resolution.mli
View File

@ -40,7 +40,7 @@ type scope_context = {
(** What is the default rule to refer to for unnamed exceptions, if any *)
sub_scopes_idmap : SubScopeName.t Desugared.Ast.IdentMap.t;
(** Sub-scopes variables *)
sub_scopes : ScopeName.t Scopelang.Ast.SubScopeMap.t;
sub_scopes : ScopeName.t SubScopeMap.t;
(** To what scope sub-scopes refer to? *)
}
(** Inside a scope, we distinguish between the variables and the subscopes. *)
@ -75,8 +75,7 @@ type context = {
constructor_idmap : EnumConstructor.t EnumMap.t Desugared.Ast.IdentMap.t;
(** The names of the enum constructors. Constructor names can be shared
between different enums *)
scopes : scope_context Scopelang.Ast.ScopeMap.t;
(** For each scope, its context *)
scopes : scope_context ScopeMap.t; (** For each scope, its context *)
structs : struct_context StructMap.t; (** For each struct, its context *)
enums : enum_context EnumMap.t; (** For each enum, its context *)
var_typs : var_sig ScopeVarMap.t;

2
compiler/surface/parser.messages
View File

@ -1741,7 +1741,7 @@ source_file: BEGIN_CODE SCOPE CONSTRUCTOR UNDER_CONDITION TRUE YEAR
## small_expression
##
expected an enum constructor to test if the expression on the left
expected the function application operator

2
examples/aides_logement/code_construction_reglementaire.catala_fr
View File

@ -409,7 +409,7 @@ champ d'application RessourcesAidesPersonnelleLogement:
définition abattement_r_822_7 égal à
si demandeur_exerce_activité_rémunérée et
conjoint_exerce_activité_rémunérée et
(ressources_conjoint +€ ressources_conjoint) >=€
(ressources_demandeur +€ ressources_conjoint) >=€
base_mensuelle_allocations_familiales.montant *€ 12,0
alors
montant_forfaitaire_r_822_7

6
flake.lock
View File

@ -17,11 +17,11 @@
},
"nixpkgs": {
"locked": {
"lastModified": 1664017330,
"narHash": "sha256-919WZKBTxFdTkzIK6uJXE7hwSPQb7e/ekybxxWaotR4=",
"lastModified": 1665848363,
"narHash": "sha256-3Jow1YxzPtQnck1bAAvbVxgRH4gNnkIdw871Vm6UtAU=",
"owner": "NixOS",
"repo": "nixpkgs",
"rev": "fde244a8c7655bc28616864e2290ad9c95409c2c",
"rev": "83b198a2083774844962c854f811538323f9f7b1",
"type": "github"
},
"original": {

10306
french_law/js/french_law.js generated
View File

File diff suppressed because one or more lines are too long

6698
french_law/ocaml/law_source/aides_logement.ml generated
View File

File diff suppressed because it is too large Load Diff

1066
french_law/ocaml/law_source/allocations_familiales.ml generated
View File

File diff suppressed because it is too large Load Diff

2749
french_law/python/src/aides_logement.py generated
View File

File diff suppressed because it is too large Load Diff

372
french_law/python/src/allocations_familiales.py generated
View File

@ -545,11 +545,11 @@ def smic(smic_in:SmicIn):
date_courante = smic_in.date_courante_in
residence = smic_in.residence_in
try:
def temp_brut_horaire(_:Any):
def temp_brut_horaire(_:Unit):
raise EmptyError
def temp_brut_horaire_1(_:Any):
def temp_brut_horaire_1(_:Unit):
return False
def temp_brut_horaire_2(_:Any):
def temp_brut_horaire_2(_:Unit):
if ((date_courante >= date_of_numbers(2022,5,1)) and
((date_courante <= date_of_numbers(2022,12,31)) and
(residence == Collectivite(Collectivite_Code.Mayotte,
@ -557,7 +557,7 @@ def smic(smic_in:SmicIn):
return money_of_cents_string("819")
else:
raise EmptyError
def temp_brut_horaire_3(_:Any):
def temp_brut_horaire_3(_:Unit):
if ((date_courante >= date_of_numbers(2022,5,1)) and
((date_courante <= date_of_numbers(2022,12,31)) and
((residence == Collectivite(Collectivite_Code.Metropole,
@ -576,7 +576,7 @@ def smic(smic_in:SmicIn):
return money_of_cents_string("1085")
else:
raise EmptyError
def temp_brut_horaire_4(_:Any):
def temp_brut_horaire_4(_:Unit):
if ((date_courante >= date_of_numbers(2022,1,1)) and
((date_courante <= date_of_numbers(2022,4,30)) and
(residence == Collectivite(Collectivite_Code.Mayotte,
@ -584,7 +584,7 @@ def smic(smic_in:SmicIn):
return money_of_cents_string("798")
else:
raise EmptyError
def temp_brut_horaire_5(_:Any):
def temp_brut_horaire_5(_:Unit):
if ((date_courante >= date_of_numbers(2022,1,1)) and
((date_courante <= date_of_numbers(2022,4,30)) and
((residence == Collectivite(Collectivite_Code.Metropole,
@ -603,7 +603,7 @@ def smic(smic_in:SmicIn):
return money_of_cents_string("1057")
else:
raise EmptyError
def temp_brut_horaire_6(_:Any):
def temp_brut_horaire_6(_:Unit):
if ((date_courante >= date_of_numbers(2021,1,1)) and
((date_courante <= date_of_numbers(2021,12,31)) and
(residence == Collectivite(Collectivite_Code.Mayotte,
@ -611,7 +611,7 @@ def smic(smic_in:SmicIn):
return money_of_cents_string("774")
else:
raise EmptyError
def temp_brut_horaire_7(_:Any):
def temp_brut_horaire_7(_:Unit):
if ((date_courante >= date_of_numbers(2021,1,1)) and
((date_courante <= date_of_numbers(2021,12,31)) and
((residence == Collectivite(Collectivite_Code.Metropole,
@ -630,7 +630,7 @@ def smic(smic_in:SmicIn):
return money_of_cents_string("1025")
else:
raise EmptyError
def temp_brut_horaire_8(_:Any):
def temp_brut_horaire_8(_:Unit):
if ((date_courante >= date_of_numbers(2020,1,1)) and
((date_courante <= date_of_numbers(2020,12,31)) and
(residence == Collectivite(Collectivite_Code.Mayotte,
@ -638,7 +638,7 @@ def smic(smic_in:SmicIn):
return money_of_cents_string("766")
else:
raise EmptyError
def temp_brut_horaire_9(_:Any):
def temp_brut_horaire_9(_:Unit):
if ((date_courante >= date_of_numbers(2020,1,1)) and
((date_courante <= date_of_numbers(2020,12,31)) and
((residence == Collectivite(Collectivite_Code.Metropole,
@ -657,7 +657,7 @@ def smic(smic_in:SmicIn):
return money_of_cents_string("1015")
else:
raise EmptyError
def temp_brut_horaire_10(_:Any):
def temp_brut_horaire_10(_:Unit):
if ((date_courante >= date_of_numbers(2019,1,1)) and
((date_courante <= date_of_numbers(2019,12,31)) and
(residence == Collectivite(Collectivite_Code.Mayotte,
@ -665,7 +665,7 @@ def smic(smic_in:SmicIn):
return money_of_cents_string("757")
else:
raise EmptyError
def temp_brut_horaire_11(_:Any):
def temp_brut_horaire_11(_:Unit):
if ((date_courante >= date_of_numbers(2019,1,1)) and
((date_courante <= date_of_numbers(2019,12,31)) and
((residence == Collectivite(Collectivite_Code.Metropole,
@ -713,32 +713,32 @@ def smic(smic_in:SmicIn):
def base_mensuelle_allocations_familiales(base_mensuelle_allocations_familiales_in:BaseMensuelleAllocationsFamilialesIn):
date_courante_1 = base_mensuelle_allocations_familiales_in.date_courante_in
try:
def temp_montant(_:Any):
def temp_montant(_:Unit):
raise EmptyError
def temp_montant_1(_:Any):
def temp_montant_1(_:Unit):
return False
def temp_montant_2(_:Any):
def temp_montant_2(_:Unit):
if ((date_courante_1 >= date_of_numbers(2022,4,1)) and
(date_courante_1 <
date_of_numbers(2023,4,1))):
return money_of_cents_string("42228")
else:
raise EmptyError
def temp_montant_3(_:Any):
def temp_montant_3(_:Unit):
if ((date_courante_1 >= date_of_numbers(2021,4,1)) and
(date_courante_1 <
date_of_numbers(2022,4,1))):
return money_of_cents_string("41481")
else:
raise EmptyError
def temp_montant_4(_:Any):
def temp_montant_4(_:Unit):
if ((date_courante_1 >= date_of_numbers(2020,4,1)) and
(date_courante_1 <
date_of_numbers(2021,4,1))):
return money_of_cents_string("41440")
else:
raise EmptyError
def temp_montant_5(_:Any):
def temp_montant_5(_:Unit):
if ((date_courante_1 >= date_of_numbers(2019,4,1)) and
(date_courante_1 <
date_of_numbers(2020,4,1))):
@ -780,21 +780,23 @@ def prestations_familiales(prestations_familiales_in:PrestationsFamilialesIn):
temp_smic_dot_date_courante = date_courante_2
except EmptyError:
temp_smic_dot_date_courante = dead_value
raise NoValueProvided(SourcePosition(filename="examples/allocations_familiales/../smic/smic.catala_fr",
start_line=9, start_column=10,
end_line=9, end_column=23,
law_headings=["Prologue",
"Montant du salaire minimum de croissance"]))
raise NoValueProvided(SourcePosition(filename="examples/allocations_familiales/prologue.catala_fr",
start_line=69, start_column=14,
end_line=69, end_column=32,
law_headings=["Prestations familiales",
"Champs d'applications",
"Prologue"]))
smic_dot_date_courante = temp_smic_dot_date_courante
try:
temp_smic_dot_residence = residence_1
except EmptyError:
temp_smic_dot_residence = dead_value
raise NoValueProvided(SourcePosition(filename="examples/allocations_familiales/../smic/smic.catala_fr",
start_line=10, start_column=10,
end_line=10, end_column=19,
law_headings=["Prologue",
"Montant du salaire minimum de croissance"]))
raise NoValueProvided(SourcePosition(filename="examples/allocations_familiales/prologue.catala_fr",
start_line=68, start_column=14,
end_line=68, end_column=28,
law_headings=["Prestations familiales",
"Champs d'applications",
"Prologue"]))
smic_dot_residence = temp_smic_dot_residence
result = smic(SmicIn(date_courante_in = smic_dot_date_courante,
residence_in = smic_dot_residence))
@ -999,11 +1001,11 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
try:
def temp_prise_en_compte(param_2:Enfant):
try:
def temp_prise_en_compte_1(_:Any):
def temp_prise_en_compte_1(_:Unit):
raise EmptyError
def temp_prise_en_compte_2(_:Any):
def temp_prise_en_compte_2(_:Unit):
return False
def temp_prise_en_compte_3(_:Any):
def temp_prise_en_compte_3(_:Unit):
try:
try:
match_arg_6 = param_2.prise_en_charge
@ -1071,7 +1073,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
Unit())
else:
raise EmptyError
def temp_prise_en_compte_7(_:Any):
def temp_prise_en_compte_7(_:Unit):
match_arg_9 = param_2.prise_en_charge
if match_arg_9.code == PriseEnCharge_Code.GardeAlterneePartageAllocations:
_ = match_arg_9.value
@ -1092,7 +1094,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return PriseEnCompte(PriseEnCompte_Code.Zero, Unit())
else:
raise EmptyError
def temp_prise_en_compte_9(_:Any):
def temp_prise_en_compte_9(_:Unit):
match_arg_10 = param_2.prise_en_charge
if match_arg_10.code == PriseEnCharge_Code.GardeAlterneePartageAllocations:
_ = match_arg_10.value
@ -1145,11 +1147,11 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
try:
def temp_versement(param_3:Enfant):
try:
def temp_versement_1(_:Any):
def temp_versement_1(_:Unit):
raise EmptyError
def temp_versement_2(_:Any):
def temp_versement_2(_:Unit):
return False
def temp_versement_3(_:Any):
def temp_versement_3(_:Unit):
try:
try:
try:
@ -1240,7 +1242,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
Unit())
else:
raise EmptyError
def temp_versement_8(_:Any):
def temp_versement_8(_:Unit):
match_arg_15 = param_3.prise_en_charge
if match_arg_15.code == PriseEnCharge_Code.GardeAlterneePartageAllocations:
_ = match_arg_15.value
@ -1316,10 +1318,12 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
temp_bmaf_dot_date_courante = date_courante_3
except EmptyError:
temp_bmaf_dot_date_courante = dead_value
raise NoValueProvided(SourcePosition(filename="examples/allocations_familiales/../base_mensuelle_allocations_familiales/bmaf.catala_fr",
start_line=5, start_column=10,
end_line=5, end_column=23,
law_headings=["Montant de la base mensuelle des allocations familiales"]))
raise NoValueProvided(SourcePosition(filename="examples/allocations_familiales/prologue.catala_fr",
start_line=159, start_column=14,
end_line=159, end_column=32,
law_headings=["Allocations familiales",
"Champs d'applications",
"Prologue"]))
bmaf_dot_date_courante = temp_bmaf_dot_date_courante
result_2 = base_mensuelle_allocations_familiales(BaseMensuelleAllocationsFamilialesIn(date_courante_in = bmaf_dot_date_courante))
bmaf_dot_montant = result_2.montant_out
@ -1328,9 +1332,9 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
except EmptyError:
temp_prestations_familiales_dot_date_courante = dead_value
raise NoValueProvided(SourcePosition(filename="examples/allocations_familiales/prologue.catala_fr",
start_line=62, start_column=10,
end_line=62, end_column=23,
law_headings=["Prestations familiales",
start_line=155, start_column=14,
end_line=155, end_column=50,
law_headings=["Allocations familiales",
"Champs d'applications",
"Prologue"]))
prestations_familiales_dot_date_courante = temp_prestations_familiales_dot_date_courante
@ -1340,9 +1344,9 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
except EmptyError:
temp_prestations_familiales_dot_prestation_courante = dead_value
raise NoValueProvided(SourcePosition(filename="examples/allocations_familiales/prologue.catala_fr",
start_line=63, start_column=10,
end_line=63, end_column=29,
law_headings=["Prestations familiales",
start_line=153, start_column=14,
end_line=153, end_column=56,
law_headings=["Allocations familiales",
"Champs d'applications",
"Prologue"]))
prestations_familiales_dot_prestation_courante = temp_prestations_familiales_dot_prestation_courante
@ -1351,9 +1355,9 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
except EmptyError:
temp_prestations_familiales_dot_residence = dead_value
raise NoValueProvided(SourcePosition(filename="examples/allocations_familiales/prologue.catala_fr",
start_line=64, start_column=10,
end_line=64, end_column=19,
law_headings=["Prestations familiales",
start_line=157, start_column=14,
end_line=157, end_column=46,
law_headings=["Allocations familiales",
"Champs d'applications",
"Prologue"]))
prestations_familiales_dot_residence = temp_prestations_familiales_dot_residence
@ -1368,12 +1372,11 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
temp_enfant_le_plus_age_dot_enfants = enfants_a_charge
except EmptyError:
temp_enfant_le_plus_age_dot_enfants = dead_value
raise NoValueProvided(SourcePosition(filename="examples/allocations_familiales/prologue.catala_fr",
start_line=79, start_column=10,
end_line=79, end_column=17,
law_headings=["Allocations familiales",
"Champs d'applications",
"Prologue"]))
raise NoValueProvided(SourcePosition(filename="examples/allocations_familiales/epilogue.catala_fr",
start_line=32, start_column=14,
end_line=32, end_column=40,
law_headings=["Règles diverses",
"Épilogue"]))
enfant_le_plus_age_dot_enfants = temp_enfant_le_plus_age_dot_enfants
result_4 = enfant_le_plus_age(EnfantLePlusAgeIn(enfants_in = enfant_le_plus_age_dot_enfants))
enfant_le_plus_age_dot_le_plus_age = result_4.le_plus_age_out
@ -1445,11 +1448,11 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
est_enfant_le_plus_age = temp_est_enfant_le_plus_age
try:
try:
def temp_plafond__i_i_d521_3(_:Any):
def temp_plafond__i_i_d521_3(_:Unit):
raise EmptyError
def temp_plafond__i_i_d521_3_1(_:Any):
def temp_plafond__i_i_d521_3_1(_:Unit):
return False
def temp_plafond__i_i_d521_3_2(_:Any):
def temp_plafond__i_i_d521_3_2(_:Unit):
if ((date_courante_3 >= date_of_numbers(2021,1,1)) and
(date_courante_3 <=
date_of_numbers(2021,12,31))):
@ -1458,7 +1461,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
decimal_of_integer(list_length(enfants_a_charge_droit_ouvert_prestation_familiale))))
else:
raise EmptyError
def temp_plafond__i_i_d521_3_3(_:Any):
def temp_plafond__i_i_d521_3_3(_:Unit):
if ((date_courante_3 >= date_of_numbers(2020,1,1)) and
(date_courante_3 <=
date_of_numbers(2020,12,31))):
@ -1467,7 +1470,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
decimal_of_integer(list_length(enfants_a_charge_droit_ouvert_prestation_familiale))))
else:
raise EmptyError
def temp_plafond__i_i_d521_3_4(_:Any):
def temp_plafond__i_i_d521_3_4(_:Unit):
if ((date_courante_3 >= date_of_numbers(2019,1,1)) and
(date_courante_3 <=
date_of_numbers(2019,12,31))):
@ -1476,7 +1479,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
decimal_of_integer(list_length(enfants_a_charge_droit_ouvert_prestation_familiale))))
else:
raise EmptyError
def temp_plafond__i_i_d521_3_5(_:Any):
def temp_plafond__i_i_d521_3_5(_:Unit):
if ((date_courante_3 >= date_of_numbers(2018,1,1)) and
(date_courante_3 <=
date_of_numbers(2018,12,31))):
@ -1512,11 +1515,11 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
plafond__i_i_d521_3 = temp_plafond__i_i_d521_3_6
try:
try:
def temp_plafond__i_d521_3(_:Any):
def temp_plafond__i_d521_3(_:Unit):
raise EmptyError
def temp_plafond__i_d521_3_1(_:Any):
def temp_plafond__i_d521_3_1(_:Unit):
return False
def temp_plafond__i_d521_3_2(_:Any):
def temp_plafond__i_d521_3_2(_:Unit):
if ((date_courante_3 >= date_of_numbers(2021,1,1)) and
(date_courante_3 <=
date_of_numbers(2021,12,31))):
@ -1525,7 +1528,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
decimal_of_integer(list_length(enfants_a_charge_droit_ouvert_prestation_familiale))))
else:
raise EmptyError
def temp_plafond__i_d521_3_3(_:Any):
def temp_plafond__i_d521_3_3(_:Unit):
if ((date_courante_3 >= date_of_numbers(2020,1,1)) and
(date_courante_3 <=
date_of_numbers(2020,12,31))):
@ -1534,7 +1537,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
decimal_of_integer(list_length(enfants_a_charge_droit_ouvert_prestation_familiale))))
else:
raise EmptyError
def temp_plafond__i_d521_3_4(_:Any):
def temp_plafond__i_d521_3_4(_:Unit):
if ((date_courante_3 >= date_of_numbers(2019,1,1)) and
(date_courante_3 <=
date_of_numbers(2019,12,31))):
@ -1543,7 +1546,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
decimal_of_integer(list_length(enfants_a_charge_droit_ouvert_prestation_familiale))))
else:
raise EmptyError
def temp_plafond__i_d521_3_5(_:Any):
def temp_plafond__i_d521_3_5(_:Unit):
if ((date_courante_3 >= date_of_numbers(2018,1,1)) and
(date_courante_3 <=
date_of_numbers(2018,12,31))):
@ -1664,11 +1667,11 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
montant_initial_base_quatrieme_enfant_et_plus_mayotte = temp_montant_initial_base_quatrieme_enfant_et_plus_mayotte
try:
try:
def temp_montant_initial_base_troisieme_enfant_mayotte(_:Any):
def temp_montant_initial_base_troisieme_enfant_mayotte(_:Unit):
raise EmptyError
def temp_montant_initial_base_troisieme_enfant_mayotte_1(_:Any):
def temp_montant_initial_base_troisieme_enfant_mayotte_1(_:Unit):
return False
def temp_montant_initial_base_troisieme_enfant_mayotte_2(_:Any):
def temp_montant_initial_base_troisieme_enfant_mayotte_2(_:Unit):
if ((residence_2 == Collectivite(Collectivite_Code.Mayotte,
Unit())) and ((date_courante_3 >=
date_of_numbers(2020,1,1)) and (date_courante_3 <=
@ -1681,7 +1684,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_troisieme_enfant_mayotte_3(_:Any):
def temp_montant_initial_base_troisieme_enfant_mayotte_3(_:Unit):
if ((residence_2 == Collectivite(Collectivite_Code.Mayotte,
Unit())) and ((date_courante_3 >=
date_of_numbers(2019,1,1)) and (date_courante_3 <=
@ -1694,7 +1697,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_troisieme_enfant_mayotte_4(_:Any):
def temp_montant_initial_base_troisieme_enfant_mayotte_4(_:Unit):
if ((residence_2 == Collectivite(Collectivite_Code.Mayotte,
Unit())) and ((date_courante_3 >=
date_of_numbers(2018,1,1)) and (date_courante_3 <=
@ -1707,7 +1710,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_troisieme_enfant_mayotte_5(_:Any):
def temp_montant_initial_base_troisieme_enfant_mayotte_5(_:Unit):
if ((residence_2 == Collectivite(Collectivite_Code.Mayotte,
Unit())) and ((date_courante_3 >=
date_of_numbers(2017,1,1)) and (date_courante_3 <=
@ -1720,7 +1723,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_troisieme_enfant_mayotte_6(_:Any):
def temp_montant_initial_base_troisieme_enfant_mayotte_6(_:Unit):
if ((residence_2 == Collectivite(Collectivite_Code.Mayotte,
Unit())) and ((date_courante_3 >=
date_of_numbers(2016,1,1)) and (date_courante_3 <=
@ -1733,7 +1736,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_troisieme_enfant_mayotte_7(_:Any):
def temp_montant_initial_base_troisieme_enfant_mayotte_7(_:Unit):
if ((residence_2 == Collectivite(Collectivite_Code.Mayotte,
Unit())) and ((date_courante_3 >=
date_of_numbers(2015,1,1)) and (date_courante_3 <=
@ -1746,7 +1749,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_troisieme_enfant_mayotte_8(_:Any):
def temp_montant_initial_base_troisieme_enfant_mayotte_8(_:Unit):
if ((residence_2 == Collectivite(Collectivite_Code.Mayotte,
Unit())) and ((date_courante_3 >=
date_of_numbers(2014,1,1)) and (date_courante_3 <=
@ -1759,7 +1762,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_troisieme_enfant_mayotte_9(_:Any):
def temp_montant_initial_base_troisieme_enfant_mayotte_9(_:Unit):
if ((residence_2 == Collectivite(Collectivite_Code.Mayotte,
Unit())) and ((date_courante_3 >=
date_of_numbers(2013,1,1)) and (date_courante_3 <=
@ -1772,7 +1775,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_troisieme_enfant_mayotte_10(_:Any):
def temp_montant_initial_base_troisieme_enfant_mayotte_10(_:Unit):
if ((residence_2 == Collectivite(Collectivite_Code.Mayotte,
Unit())) and ((date_courante_3 >=
date_of_numbers(2012,1,1)) and (date_courante_3 <=
@ -1785,7 +1788,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_troisieme_enfant_mayotte_11(_:Any):
def temp_montant_initial_base_troisieme_enfant_mayotte_11(_:Unit):
if ((residence_2 == Collectivite(Collectivite_Code.Mayotte,
Unit())) and ((date_courante_3 >=
date_of_numbers(2011,1,1)) and (date_courante_3 <=
@ -1868,24 +1871,24 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
"Prologue"]))
nombre_moyen_enfants = temp_nombre_moyen_enfants_2
try:
def temp_montant_initial_base_premier_enfant(_:Any):
def temp_montant_initial_base_premier_enfant(_:Unit):
return money_of_cents_string("0")
def temp_montant_initial_base_premier_enfant_1(_:Any):
def temp_montant_initial_base_premier_enfant_1(_:Unit):
return True
def temp_montant_initial_base_premier_enfant_2(_:Any):
def temp_montant_initial_base_premier_enfant_2(_:Unit):
if (prestations_familiales_dot_regime_outre_mer_l751_1 and
(list_length(enfants_a_charge_droit_ouvert_prestation_familiale) ==
integer_of_string("1"))):
return (bmaf_dot_montant * decimal_of_string("0.0588"))
else:
raise EmptyError
def temp_montant_initial_base_premier_enfant_3(_:Any):
def temp_montant_initial_base_premier_enfant_3(_:Unit):
try:
def temp_montant_initial_base_premier_enfant_4(_:Any):
def temp_montant_initial_base_premier_enfant_4(_:Unit):
raise EmptyError
def temp_montant_initial_base_premier_enfant_5(_:Any):
def temp_montant_initial_base_premier_enfant_5(_:Unit):
return False
def temp_montant_initial_base_premier_enfant_6(_:Any):
def temp_montant_initial_base_premier_enfant_6(_:Unit):
if ((residence_2 ==
Collectivite(Collectivite_Code.Mayotte, Unit())) and
avait_enfant_a_charge_avant_1er_janvier_2012):
@ -1896,7 +1899,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_premier_enfant_7(_:Any):
def temp_montant_initial_base_premier_enfant_7(_:Unit):
if ((residence_2 ==
Collectivite(Collectivite_Code.Mayotte, Unit())) and
((date_courante_3 >= date_of_numbers(2020,1,1)) and
@ -1910,7 +1913,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_premier_enfant_8(_:Any):
def temp_montant_initial_base_premier_enfant_8(_:Unit):
if ((residence_2 ==
Collectivite(Collectivite_Code.Mayotte, Unit())) and
((date_courante_3 >= date_of_numbers(2019,1,1)) and
@ -1924,7 +1927,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_premier_enfant_9(_:Any):
def temp_montant_initial_base_premier_enfant_9(_:Unit):
if ((residence_2 ==
Collectivite(Collectivite_Code.Mayotte, Unit())) and
((date_courante_3 >= date_of_numbers(2018,1,1)) and
@ -1938,7 +1941,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_premier_enfant_10(_:Any):
def temp_montant_initial_base_premier_enfant_10(_:Unit):
if ((residence_2 ==
Collectivite(Collectivite_Code.Mayotte, Unit())) and
((date_courante_3 >= date_of_numbers(2017,1,1)) and
@ -1952,7 +1955,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_premier_enfant_11(_:Any):
def temp_montant_initial_base_premier_enfant_11(_:Unit):
if ((residence_2 ==
Collectivite(Collectivite_Code.Mayotte, Unit())) and
((date_courante_3 >= date_of_numbers(2016,1,1)) and
@ -1966,7 +1969,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_premier_enfant_12(_:Any):
def temp_montant_initial_base_premier_enfant_12(_:Unit):
if ((residence_2 ==
Collectivite(Collectivite_Code.Mayotte, Unit())) and
((date_courante_3 >= date_of_numbers(2015,1,1)) and
@ -1980,7 +1983,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_premier_enfant_13(_:Any):
def temp_montant_initial_base_premier_enfant_13(_:Unit):
if ((residence_2 ==
Collectivite(Collectivite_Code.Mayotte, Unit())) and
((date_courante_3 >= date_of_numbers(2014,1,1)) and
@ -1994,7 +1997,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_premier_enfant_14(_:Any):
def temp_montant_initial_base_premier_enfant_14(_:Unit):
if ((residence_2 ==
Collectivite(Collectivite_Code.Mayotte, Unit())) and
((date_courante_3 >= date_of_numbers(2013,1,1)) and
@ -2008,7 +2011,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_premier_enfant_15(_:Any):
def temp_montant_initial_base_premier_enfant_15(_:Unit):
if ((residence_2 ==
Collectivite(Collectivite_Code.Mayotte, Unit())) and
((date_courante_3 >= date_of_numbers(2012,1,1)) and
@ -2022,7 +2025,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_premier_enfant_16(_:Any):
def temp_montant_initial_base_premier_enfant_16(_:Unit):
if ((residence_2 ==
Collectivite(Collectivite_Code.Mayotte, Unit())) and
((date_courante_3 >= date_of_numbers(2011,1,1)) and
@ -2165,11 +2168,11 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
def temp_complement_degressif(param_8:Money):
try:
try:
def temp_complement_degressif_1(_:Any):
def temp_complement_degressif_1(_:Unit):
raise EmptyError
def temp_complement_degressif_2(_:Any):
def temp_complement_degressif_2(_:Unit):
return False
def temp_complement_degressif_3(_:Any):
def temp_complement_degressif_3(_:Unit):
if ((ressources_menage > plafond__i_i_d521_3) and
(ressources_menage <= (plafond__i_i_d521_3 +
(param_8 *
@ -2181,7 +2184,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
decimal_of_string("12.")))
else:
raise EmptyError
def temp_complement_degressif_4(_:Any):
def temp_complement_degressif_4(_:Unit):
if ((ressources_menage > plafond__i_d521_3) and
(ressources_menage <= (plafond__i_d521_3 +
(param_8 *
@ -2223,24 +2226,24 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
"Prologue"]))
complement_degressif = temp_complement_degressif
try:
def temp_montant_verse_forfaitaire_par_enfant(_:Any):
def temp_montant_verse_forfaitaire_par_enfant(_:Unit):
raise EmptyError
def temp_montant_verse_forfaitaire_par_enfant_1(_:Any):
def temp_montant_verse_forfaitaire_par_enfant_1(_:Unit):
return False
def temp_montant_verse_forfaitaire_par_enfant_2(_:Any):
def temp_montant_verse_forfaitaire_par_enfant_2(_:Unit):
if (ressources_menage >
plafond__i_i_d521_3):
return (bmaf_dot_montant * decimal_of_string("0.05059"))
else:
raise EmptyError
def temp_montant_verse_forfaitaire_par_enfant_3(_:Any):
def temp_montant_verse_forfaitaire_par_enfant_3(_:Unit):
if ((ressources_menage > plafond__i_d521_3) and
(ressources_menage <=
plafond__i_i_d521_3)):
return (bmaf_dot_montant * decimal_of_string("0.10117"))
else:
raise EmptyError
def temp_montant_verse_forfaitaire_par_enfant_4(_:Any):
def temp_montant_verse_forfaitaire_par_enfant_4(_:Unit):
if (ressources_menage <=
plafond__i_d521_3):
return (bmaf_dot_montant * decimal_of_string("0.20234"))
@ -2265,11 +2268,11 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
"Prologue"]))
montant_verse_forfaitaire_par_enfant = temp_montant_verse_forfaitaire_par_enfant_5
try:
def temp_montant_initial_base_troisieme_enfant_et_plus(_:Any):
def temp_montant_initial_base_troisieme_enfant_et_plus(_:Unit):
raise EmptyError
def temp_montant_initial_base_troisieme_enfant_et_plus_1(_:Any):
def temp_montant_initial_base_troisieme_enfant_et_plus_1(_:Unit):
return False
def temp_montant_initial_base_troisieme_enfant_et_plus_2(_:Any):
def temp_montant_initial_base_troisieme_enfant_et_plus_2(_:Unit):
if (ressources_menage >
plafond__i_i_d521_3):
if (list_length(enfants_a_charge_droit_ouvert_prestation_familiale) >
@ -2282,7 +2285,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_troisieme_enfant_et_plus_3(_:Any):
def temp_montant_initial_base_troisieme_enfant_et_plus_3(_:Unit):
if ((ressources_menage > plafond__i_d521_3) and
(ressources_menage <=
plafond__i_i_d521_3)):
@ -2295,7 +2298,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_troisieme_enfant_et_plus_4(_:Any):
def temp_montant_initial_base_troisieme_enfant_et_plus_4(_:Unit):
if (ressources_menage <=
plafond__i_d521_3):
if (list_length(enfants_a_charge_droit_ouvert_prestation_familiale) >
@ -2328,11 +2331,11 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
try:
try:
try:
def temp_montant_initial_base_deuxieme_enfant(_:Any):
def temp_montant_initial_base_deuxieme_enfant(_:Unit):
raise EmptyError
def temp_montant_initial_base_deuxieme_enfant_1(_:Any):
def temp_montant_initial_base_deuxieme_enfant_1(_:Unit):
return False
def temp_montant_initial_base_deuxieme_enfant_2(_:Any):
def temp_montant_initial_base_deuxieme_enfant_2(_:Unit):
if ((residence_2 ==
Collectivite(Collectivite_Code.Mayotte, Unit())) and
((date_courante_3 >= date_of_numbers(2020,1,1)) and
@ -2346,7 +2349,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_deuxieme_enfant_3(_:Any):
def temp_montant_initial_base_deuxieme_enfant_3(_:Unit):
if ((residence_2 ==
Collectivite(Collectivite_Code.Mayotte, Unit())) and
((date_courante_3 >= date_of_numbers(2019,1,1)) and
@ -2360,7 +2363,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_deuxieme_enfant_4(_:Any):
def temp_montant_initial_base_deuxieme_enfant_4(_:Unit):
if ((residence_2 ==
Collectivite(Collectivite_Code.Mayotte, Unit())) and
((date_courante_3 >= date_of_numbers(2018,1,1)) and
@ -2374,7 +2377,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_deuxieme_enfant_5(_:Any):
def temp_montant_initial_base_deuxieme_enfant_5(_:Unit):
if ((residence_2 ==
Collectivite(Collectivite_Code.Mayotte, Unit())) and
((date_courante_3 >= date_of_numbers(2017,1,1)) and
@ -2388,7 +2391,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_deuxieme_enfant_6(_:Any):
def temp_montant_initial_base_deuxieme_enfant_6(_:Unit):
if ((residence_2 ==
Collectivite(Collectivite_Code.Mayotte, Unit())) and
((date_courante_3 >= date_of_numbers(2016,1,1)) and
@ -2402,7 +2405,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_deuxieme_enfant_7(_:Any):
def temp_montant_initial_base_deuxieme_enfant_7(_:Unit):
if ((residence_2 ==
Collectivite(Collectivite_Code.Mayotte, Unit())) and
((date_courante_3 >= date_of_numbers(2015,1,1)) and
@ -2416,7 +2419,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_deuxieme_enfant_8(_:Any):
def temp_montant_initial_base_deuxieme_enfant_8(_:Unit):
if ((residence_2 ==
Collectivite(Collectivite_Code.Mayotte, Unit())) and
((date_courante_3 >= date_of_numbers(2014,1,1)) and
@ -2430,7 +2433,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_deuxieme_enfant_9(_:Any):
def temp_montant_initial_base_deuxieme_enfant_9(_:Unit):
if ((residence_2 ==
Collectivite(Collectivite_Code.Mayotte, Unit())) and
((date_courante_3 >= date_of_numbers(2013,1,1)) and
@ -2444,7 +2447,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_deuxieme_enfant_10(_:Any):
def temp_montant_initial_base_deuxieme_enfant_10(_:Unit):
if ((residence_2 ==
Collectivite(Collectivite_Code.Mayotte, Unit())) and
((date_courante_3 >= date_of_numbers(2012,1,1)) and
@ -2458,7 +2461,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_deuxieme_enfant_11(_:Any):
def temp_montant_initial_base_deuxieme_enfant_11(_:Unit):
if ((residence_2 ==
Collectivite(Collectivite_Code.Mayotte, Unit())) and
((date_courante_3 >= date_of_numbers(2011,1,1)) and
@ -2503,11 +2506,11 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
temp_montant_initial_base_deuxieme_enfant_12 = dead_value
raise EmptyError
except EmptyError:
def temp_montant_initial_base_deuxieme_enfant_13(_:Any):
def temp_montant_initial_base_deuxieme_enfant_13(_:Unit):
raise EmptyError
def temp_montant_initial_base_deuxieme_enfant_14(_:Any):
def temp_montant_initial_base_deuxieme_enfant_14(_:Unit):
return False
def temp_montant_initial_base_deuxieme_enfant_15(_:Any):
def temp_montant_initial_base_deuxieme_enfant_15(_:Unit):
if (ressources_menage >
plafond__i_i_d521_3):
if (list_length(enfants_a_charge_droit_ouvert_prestation_familiale) >
@ -2517,7 +2520,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_deuxieme_enfant_16(_:Any):
def temp_montant_initial_base_deuxieme_enfant_16(_:Unit):
if ((ressources_menage > plafond__i_d521_3) and
(ressources_menage <=
plafond__i_i_d521_3)):
@ -2528,7 +2531,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_base_deuxieme_enfant_17(_:Any):
def temp_montant_initial_base_deuxieme_enfant_17(_:Unit):
if (ressources_menage <=
plafond__i_d521_3):
if (list_length(enfants_a_charge_droit_ouvert_prestation_familiale) >
@ -2576,29 +2579,29 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
try:
def temp_montant_initial_metropole_majoration(param_9:Enfant):
try:
def temp_montant_initial_metropole_majoration_1(_:Any):
def temp_montant_initial_metropole_majoration_1(_:Unit):
raise EmptyError
def temp_montant_initial_metropole_majoration_2(_:Any):
def temp_montant_initial_metropole_majoration_2(_:Unit):
return False
def temp_montant_initial_metropole_majoration_3(_:Any):
def temp_montant_initial_metropole_majoration_3(_:Unit):
if not droit_ouvert_majoration(param_9):
return money_of_cents_string("0")
else:
raise EmptyError
def temp_montant_initial_metropole_majoration_4(_:Any):
def temp_montant_initial_metropole_majoration_4(_:Unit):
if ((ressources_menage > plafond__i_i_d521_3) and
droit_ouvert_majoration(param_9)):
return (bmaf_dot_montant * decimal_of_string("0.04"))
else:
raise EmptyError
def temp_montant_initial_metropole_majoration_5(_:Any):
def temp_montant_initial_metropole_majoration_5(_:Unit):
if (((ressources_menage > plafond__i_d521_3) and
(ressources_menage <= plafond__i_i_d521_3)) and
droit_ouvert_majoration(param_9)):
return (bmaf_dot_montant * decimal_of_string("0.08"))
else:
raise EmptyError
def temp_montant_initial_metropole_majoration_6(_:Any):
def temp_montant_initial_metropole_majoration_6(_:Unit):
if ((ressources_menage <= plafond__i_d521_3) and
droit_ouvert_majoration(param_9)):
return (bmaf_dot_montant * decimal_of_string("0.16"))
@ -2654,11 +2657,11 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
montant_verse_forfaitaire = temp_montant_verse_forfaitaire_1
try:
try:
def temp_montant_initial_base(_:Any):
def temp_montant_initial_base(_:Unit):
raise EmptyError
def temp_montant_initial_base_1(_:Any):
def temp_montant_initial_base_1(_:Unit):
return False
def temp_montant_initial_base_2(_:Any):
def temp_montant_initial_base_2(_:Unit):
if (residence_2 == Collectivite(Collectivite_Code.Mayotte,
Unit())):
return (((montant_initial_base_premier_enfant +
@ -2667,7 +2670,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
montant_initial_base_quatrieme_enfant_et_plus_mayotte)
else:
raise EmptyError
def temp_montant_initial_base_3(_:Any):
def temp_montant_initial_base_3(_:Unit):
if (prestations_familiales_dot_regime_outre_mer_l751_1 and
(list_length(enfants_a_charge_droit_ouvert_prestation_familiale) ==
integer_of_string("1"))):
@ -2700,11 +2703,11 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
def temp_montant_initial_majoration(param_10:Enfant):
try:
try:
def temp_montant_initial_majoration_1(_:Any):
def temp_montant_initial_majoration_1(_:Unit):
raise EmptyError
def temp_montant_initial_majoration_2(_:Any):
def temp_montant_initial_majoration_2(_:Unit):
return False
def temp_montant_initial_majoration_3(_:Any):
def temp_montant_initial_majoration_3(_:Unit):
if (droit_ouvert_majoration(param_10) and
(prestations_familiales_dot_regime_outre_mer_l751_1 and
((list_length(enfants_a_charge_droit_ouvert_prestation_familiale) ==
@ -2716,7 +2719,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
decimal_of_string("0.0567"))
else:
raise EmptyError
def temp_montant_initial_majoration_4(_:Any):
def temp_montant_initial_majoration_4(_:Unit):
if (droit_ouvert_majoration(param_10) and
(prestations_familiales_dot_regime_outre_mer_l751_1 and
((list_length(enfants_a_charge_droit_ouvert_prestation_familiale) ==
@ -2762,11 +2765,11 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
montant_initial_majoration = temp_montant_initial_majoration
try:
try:
def temp_montant_verse_complement_pour_forfaitaire(_:Any):
def temp_montant_verse_complement_pour_forfaitaire(_:Unit):
raise EmptyError
def temp_montant_verse_complement_pour_forfaitaire_1(_:Any):
def temp_montant_verse_complement_pour_forfaitaire_1(_:Unit):
return False
def temp_montant_verse_complement_pour_forfaitaire_2(_:Any):
def temp_montant_verse_complement_pour_forfaitaire_2(_:Unit):
if ((ressources_menage > plafond__i_i_d521_3) and
(ressources_menage <= (plafond__i_i_d521_3 +
(montant_verse_forfaitaire *
@ -2777,7 +2780,7 @@ def allocations_familiales(allocations_familiales_in:AllocationsFamilialesIn):
(decimal_of_string("1.") / decimal_of_string("12.")))
else:
raise EmptyError
def temp_montant_verse_complement_pour_forfaitaire_3(_:Any):
def temp_montant_verse_complement_pour_forfaitaire_3(_:Unit):
if ((ressources_menage > plafond__i_d521_3) and
(ressources_menage <= (plafond__i_d521_3 +
(montant_verse_forfaitaire *
@ -3009,12 +3012,11 @@ def interface_allocations_familiales(interface_allocations_familiales_in:Interfa
temp_allocations_familiales_dot_personne_charge_effective_permanente_est_parent_1 = temp_allocations_familiales_dot_personne_charge_effective_permanente_est_parent
except EmptyError:
temp_allocations_familiales_dot_personne_charge_effective_permanente_est_parent_1 = dead_value
raise NoValueProvided(SourcePosition(filename="examples/allocations_familiales/prologue.catala_fr",
start_line=85, start_column=10,
end_line=85, end_column=57,
law_headings=["Allocations familiales",
"Champs d'applications",
"Prologue"]))
raise NoValueProvided(SourcePosition(filename="examples/allocations_familiales/epilogue.catala_fr",
start_line=91, start_column=5,
end_line=91, end_column=75,
law_headings=["Interface du programme",
"Épilogue"]))
allocations_familiales_dot_personne_charge_effective_permanente_est_parent = temp_allocations_familiales_dot_personne_charge_effective_permanente_est_parent_1
try:
try:
@ -3028,56 +3030,51 @@ def interface_allocations_familiales(interface_allocations_familiales_in:Interfa
temp_allocations_familiales_dot_personne_charge_effective_permanente_remplit_titre__i_1 = temp_allocations_familiales_dot_personne_charge_effective_permanente_remplit_titre__i
except EmptyError:
temp_allocations_familiales_dot_personne_charge_effective_permanente_remplit_titre__i_1 = dead_value
raise NoValueProvided(SourcePosition(filename="examples/allocations_familiales/prologue.catala_fr",
start_line=86, start_column=10,
end_line=86, end_column=62,
law_headings=["Allocations familiales",
"Champs d'applications",
"Prologue"]))
raise NoValueProvided(SourcePosition(filename="examples/allocations_familiales/epilogue.catala_fr",
start_line=95, start_column=5,
end_line=95, end_column=80,
law_headings=["Interface du programme",
"Épilogue"]))
allocations_familiales_dot_personne_charge_effective_permanente_remplit_titre__i = temp_allocations_familiales_dot_personne_charge_effective_permanente_remplit_titre__i_1
try:
temp_allocations_familiales_dot_ressources_menage = i_ressources_menage
except EmptyError:
temp_allocations_familiales_dot_ressources_menage = dead_value
raise NoValueProvided(SourcePosition(filename="examples/allocations_familiales/prologue.catala_fr",
start_line=87, start_column=10,
end_line=87, end_column=27,
law_headings=["Allocations familiales",
"Champs d'applications",
"Prologue"]))
raise NoValueProvided(SourcePosition(filename="examples/allocations_familiales/epilogue.catala_fr",
start_line=87, start_column=14,
end_line=87, end_column=54,
law_headings=["Interface du programme",
"Épilogue"]))
allocations_familiales_dot_ressources_menage = temp_allocations_familiales_dot_ressources_menage
try:
temp_allocations_familiales_dot_residence = i_residence
except EmptyError:
temp_allocations_familiales_dot_residence = dead_value
raise NoValueProvided(SourcePosition(filename="examples/allocations_familiales/prologue.catala_fr",
start_line=88, start_column=10,
end_line=88, end_column=19,
law_headings=["Allocations familiales",
"Champs d'applications",
"Prologue"]))
raise NoValueProvided(SourcePosition(filename="examples/allocations_familiales/epilogue.catala_fr",
start_line=88, start_column=14,
end_line=88, end_column=46,
law_headings=["Interface du programme",
"Épilogue"]))
allocations_familiales_dot_residence = temp_allocations_familiales_dot_residence
try:
temp_allocations_familiales_dot_date_courante = i_date_courante
except EmptyError:
temp_allocations_familiales_dot_date_courante = dead_value
raise NoValueProvided(SourcePosition(filename="examples/allocations_familiales/prologue.catala_fr",
start_line=91, start_column=10,
end_line=91, end_column=23,
law_headings=["Allocations familiales",
"Champs d'applications",
"Prologue"]))
raise NoValueProvided(SourcePosition(filename="examples/allocations_familiales/epilogue.catala_fr",
start_line=85, start_column=14,
end_line=85, end_column=50,
law_headings=["Interface du programme",
"Épilogue"]))
allocations_familiales_dot_date_courante = temp_allocations_familiales_dot_date_courante
try:
temp_allocations_familiales_dot_enfants_a_charge = enfants_a_charge_1
except EmptyError:
temp_allocations_familiales_dot_enfants_a_charge = dead_value
raise NoValueProvided(SourcePosition(filename="examples/allocations_familiales/prologue.catala_fr",
start_line=94, start_column=10,
end_line=94, end_column=26,
law_headings=["Allocations familiales",
"Champs d'applications",
"Prologue"]))
raise NoValueProvided(SourcePosition(filename="examples/allocations_familiales/epilogue.catala_fr",
start_line=86, start_column=14,
end_line=86, end_column=53,
law_headings=["Interface du programme",
"Épilogue"]))
allocations_familiales_dot_enfants_a_charge = temp_allocations_familiales_dot_enfants_a_charge
try:
try:
@ -3091,12 +3088,11 @@ def interface_allocations_familiales(interface_allocations_familiales_in:Interfa
temp_allocations_familiales_dot_avait_enfant_a_charge_avant_1er_janvier_2012_1 = temp_allocations_familiales_dot_avait_enfant_a_charge_avant_1er_janvier_2012
except EmptyError:
temp_allocations_familiales_dot_avait_enfant_a_charge_avant_1er_janvier_2012_1 = dead_value
raise NoValueProvided(SourcePosition(filename="examples/allocations_familiales/prologue.catala_fr",
start_line=115, start_column=10,
end_line=115, end_column=54,
law_headings=["Allocations familiales",
"Champs d'applications",
"Prologue"]))
raise NoValueProvided(SourcePosition(filename="examples/allocations_familiales/epilogue.catala_fr",
start_line=99, start_column=5,
end_line=99, end_column=72,
law_headings=["Interface du programme",
"Épilogue"]))
allocations_familiales_dot_avait_enfant_a_charge_avant_1er_janvier_2012 = temp_allocations_familiales_dot_avait_enfant_a_charge_avant_1er_janvier_2012_1
result_5 = allocations_familiales(AllocationsFamilialesIn(personne_charge_effective_permanente_est_parent_in = allocations_familiales_dot_personne_charge_effective_permanente_est_parent,
personne_charge_effective_permanente_remplit_titre_I_in = allocations_familiales_dot_personne_charge_effective_permanente_remplit_titre__i,

8
tests/README.md
View File

@ -49,3 +49,11 @@ for instance), you can mass-reset the expected outputs with
`make test_suite CLERK_OPTS=--reset`.
`git diff` will then allow to check all the changes at once.
**Caution**: It's your responsability to check all the changes before committing them.
## Tips
* Running a single test-file just to check changes when tweaking either the compiler or the test file itself, but without updating or diffing with the reference can be useful when debugging. The following command outputs the result to `stdout` and can be used from within text editors:
clerk runtest test-file.catala_en
# Or, to use the current build artefacts, wrap with `dune exec`:
dune exec --display=quiet --no-build -- clerk runtest -e dune -c "exec --display=quiet --no-build -- catala" test-file.catala_en

18
tests/test_array/bad/fold_error.catala_en
View File

@ -13,21 +13,14 @@ scope A:
```catala-test-inline
$ catala Interpret -s A
[ERROR] Error during typechecking, incompatible types:
--> money
--> integer
--> money
Error coming from typechecking the following expression:
--> tests/test_array/bad/fold_error.catala_en
|
10 | definition list_high_count equals number for m in list of (m >=$ $7)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ Article
Type money coming from expression:
--> tests/test_array/bad/fold_error.catala_en
|
10 | definition list_high_count equals number for m in list of (m >=$ $7)
| ^^^
| ^
+ Article
Type integer coming from expression:
@ -36,5 +29,12 @@ Type integer coming from expression:
5 | context list content collection integer
| ^^^^^^^
+ Article
Type money coming from expression:
--> tests/test_array/bad/fold_error.catala_en
|
10 | definition list_high_count equals number for m in list of (m >=$ $7)
| ^^^
+ Article
#return code 255#
```

20
tests/test_bool/bad/bad_assert.catala_en
View File

@ -13,8 +13,8 @@ scope Foo:
```catala-test-inline
$ catala Interpret -s Foo
[ERROR] Error during typechecking, incompatible types:
--> bool
--> integer
--> bool
Error coming from typechecking the following expression:
--> tests/test_bool/bad/bad_assert.catala_en
@ -23,18 +23,18 @@ Error coming from typechecking the following expression:
| ^
+ Test
Type bool coming from expression:
--> tests/test_bool/bad/bad_assert.catala_en
|
9 | assertion x
| ^
+ Test
Type integer coming from expression:
--> tests/test_bool/bad/bad_assert.catala_en
|
8 | definition x equals 0
| ^
5 | internal x content integer
| ^^^^^^^
+ Test
Type bool coming from expression:
--> tests/test_bool/bad/bad_assert.catala_en
|
9 | assertion x
| ^
+ Test
#return code 255#
```

6
tests/test_bool/bad/test_xor_with_int.catala_en
View File

@ -18,7 +18,7 @@ Error coming from typechecking the following expression:
--> tests/test_bool/bad/test_xor_with_int.catala_en
|
8 | definition test_var equals 10 xor 20
| ^^^^^^^^^
| ^^^
+ 'xor' should be a boolean operator
Type bool coming from expression:
@ -31,8 +31,8 @@ Type bool coming from expression:
Type integer coming from expression:
--> tests/test_bool/bad/test_xor_with_int.catala_en
|
8 | definition test_var equals 10 xor 20
| ^^
5 | context test_var content integer
| ^^^^^^^
+ 'xor' should be a boolean operator
#return code 255#
```

22
tests/test_bool/good/test_bool.catala_en
View File

@ -13,21 +13,21 @@ scope TestBool:
```catala-test-inline
$ catala Dcalc
let TestBool_14 :
let TestBool_22 :
TestBool_in{"foo_in": unit → bool; "bar_in": unit → integer} →
TestBool_out{"foo_out": bool; "bar_out": integer} =
λ (TestBool_in_15: TestBool_in{"foo_in": unit → bool; "bar_in":
λ (TestBool_in_23: TestBool_in{"foo_in": unit → bool; "bar_in":
unit → integer}) →
let foo_16 : unit → bool = TestBool_in_15."foo_in" in
let bar_17 : unit → integer = TestBool_in_15."bar_in" in
let bar_18 : integer = error_empty
⟨bar_17 () | true ⊢ ⟨true ⊢ 1⟩⟩ in
let foo_19 : bool = error_empty
⟨foo_16 () | true ⊢
⟨⟨bar_18 >= 0 ⊢ true⟩, ⟨bar_18 < 0 ⊢ false⟩ | false ⊢
let foo_24 : unit → bool = TestBool_in_23."foo_in" in
let bar_25 : unit → integer = TestBool_in_23."bar_in" in
let bar_26 : integer = error_empty
⟨bar_25 () | true ⊢ ⟨true ⊢ 1⟩⟩ in
let foo_27 : bool = error_empty
⟨foo_24 () | true ⊢
⟨⟨bar_26 >= 0 ⊢ true⟩, ⟨bar_26 < 0 ⊢ false⟩ | false ⊢
∅ ⟩⟩ in
TestBool_out {"foo_out"= foo_19; "bar_out"= bar_18} in
TestBool_14
TestBool_out {"foo_out"= foo_27; "bar_out"= bar_26} in
TestBool_22
```
```catala-test-inline

16
tests/test_enum/bad/quick_pattern_2.catala_en
View File

@ -31,8 +31,8 @@ scope B:
```catala-test-inline
$ catala Interpret -s A
[ERROR] Error during typechecking, incompatible types:
--> F
--> E
--> F
Error coming from typechecking the following expression:
--> tests/test_enum/bad/quick_pattern_2.catala_en
@ -41,18 +41,18 @@ Error coming from typechecking the following expression:
| ^
+ Article
Type F coming from expression:
--> tests/test_enum/bad/quick_pattern_2.catala_en
|
28 | definition y equals x with pattern Case3
| ^
+ Article
Type E coming from expression:
--> tests/test_enum/bad/quick_pattern_2.catala_en
|
17 | context x content E
| ^
+ Article
Type F coming from expression:
--> tests/test_enum/bad/quick_pattern_2.catala_en
|
28 | definition y equals x with pattern Case3
| ^^^^^^^^^^^^^^^^^^^^
+ Article
#return code 255#
```

16
tests/test_enum/bad/quick_pattern_3.catala_en
View File

@ -21,8 +21,8 @@ definition y equals x with pattern Case3
```catala-test-inline
$ catala Interpret -s A
[ERROR] Error during typechecking, incompatible types:
--> F
--> E
--> F
Error coming from typechecking the following expression:
--> tests/test_enum/bad/quick_pattern_3.catala_en
@ -31,18 +31,18 @@ Error coming from typechecking the following expression:
| ^
+ Article
Type F coming from expression:
--> tests/test_enum/bad/quick_pattern_3.catala_en
|
18 | definition y equals x with pattern Case3
| ^
+ Article
Type E coming from expression:
--> tests/test_enum/bad/quick_pattern_3.catala_en
|
13 | context x content E
| ^
+ Article
Type F coming from expression:
--> tests/test_enum/bad/quick_pattern_3.catala_en
|
18 | definition y equals x with pattern Case3
| ^^^^^^^^^^^^^^^^^^^^
+ Article
#return code 255#
```

16
tests/test_enum/bad/quick_pattern_4.catala_en
View File

@ -20,8 +20,8 @@ definition y equals x with pattern Case3
```catala-test-inline
$ catala Interpret -s A
[ERROR] Error during typechecking, incompatible types:
--> F
--> E
--> F
Error coming from typechecking the following expression:
--> tests/test_enum/bad/quick_pattern_4.catala_en
@ -30,18 +30,18 @@ Error coming from typechecking the following expression:
| ^
+ Test
Type F coming from expression:
--> tests/test_enum/bad/quick_pattern_4.catala_en
|
17 | definition y equals x with pattern Case3
| ^
+ Test
Type E coming from expression:
--> tests/test_enum/bad/quick_pattern_4.catala_en
|
12 | context x content E
| ^
+ Test
Type F coming from expression:
--> tests/test_enum/bad/quick_pattern_4.catala_en
|
17 | definition y equals x with pattern Case3
| ^^^^^^^^^^^^^^^^^^^^
+ Test
#return code 255#
```

2
tests/test_io/bad/using_non_output.catala_en
View File

@ -14,7 +14,7 @@ scope B:
assertion a.a = 0
```
```catala-test-inline
$ catala Typecheck
$ catala Typecheck
[ERROR] The variable a.a cannot be used here, as it is not part subscope a's results. Maybe you forgot to qualify it as an output?
Incriminated variable usage:

24
tests/test_io/good/all_io.catala_en
View File

@ -20,19 +20,19 @@ scope A:
```catala-test-inline
$ catala Dcalc -s A
let A =
λ (A_in_21: A_in{"c_in": integer; "d_in": integer; "e_in":
λ (A_in_29: A_in{"c_in": integer; "d_in": integer; "e_in":
unit → integer; "f_in": unit → integer}) →
let c_22 : integer = A_in_21."c_in" in
let d_23 : integer = A_in_21."d_in" in
let e_24 : unit → integer = A_in_21."e_in" in
let f_25 : unit → integer = A_in_21."f_in" in
let a_26 : integer = error_empty ⟨true ⊢ 0⟩ in
let b_27 : integer = error_empty ⟨true ⊢ a_26 + 1⟩ in
let e_28 : integer = error_empty
⟨e_24 () | true ⊢ ⟨true ⊢ b_27 + c_22 + d_23 + 1⟩⟩ in
let f_29 : integer = error_empty
⟨f_25 () | true ⊢ ⟨true ⊢ e_28 + 1⟩⟩ in
A_out {"b_out"= b_27; "d_out"= d_23; "f_out"= f_29}
let c_30 : integer = A_in_29."c_in" in
let d_31 : integer = A_in_29."d_in" in
let e_32 : unit → integer = A_in_29."e_in" in
let f_33 : unit → integer = A_in_29."f_in" in
let a_34 : integer = error_empty ⟨true ⊢ 0⟩ in
let b_35 : integer = error_empty ⟨true ⊢ a_34 + 1⟩ in
let e_36 : integer = error_empty
⟨e_32 () | true ⊢ ⟨true ⊢ b_35 + c_30 + d_31 + 1⟩⟩ in
let f_37 : integer = error_empty
⟨f_33 () | true ⊢ ⟨true ⊢ e_36 + 1⟩⟩ in
A_out {"b_out"= b_35; "d_out"= d_31; "f_out"= f_37}
```
```catala-test-inline

10
tests/test_io/good/condition_only_input.catala_en
View File

@ -17,11 +17,11 @@ scope B:
```catala-test-inline
$ catala Dcalc -s B
let B =
λ (B_in_21: B_in{}) →
let a.x_22 : bool = error_empty ⟨true ⊢ false⟩ in
let result_23 : A_out{"y_out": integer} = A_13 (A_in {"x_in"= a.x_22}) in
let a.y_24 : integer = result_23."y_out" in
let __25 : unit = assert (error_empty a.y_24 = 1) in
λ (B_in_25: B_in{}) →
let a.x_26 : bool = error_empty ⟨true ⊢ false⟩ in
let result_27 : A_out{"y_out": integer} = A_13 (A_in {"x_in"= a.x_26}) in
let a.y_28 : integer = result_27."y_out" in
let __29 : unit = assert (error_empty a.y_28 = 1) in
B_out {}
```

14
tests/test_io/good/subscope.catala_en
View File

@ -23,13 +23,13 @@ scope B:
```catala-test-inline
$ catala Dcalc -s B
let B =
λ (B_in_27: B_in{}) →
let a.a_28 : unit → integer = λ (__29: unit) → ∅ in
let a.b_30 : integer = error_empty ⟨true ⊢ 2⟩ in
let result_31 : A_out{"c_out": integer} =
A_17 (A_in {"a_in"= a.a_28; "b_in"= a.b_30}) in
let a.c_32 : integer = result_31."c_out" in
let __33 : unit = assert (error_empty a.c_32 = 1) in
λ (B_in_32: B_in{}) →
let a.a_33 : unit → integer = λ (__34: unit) → ∅ in
let a.b_35 : integer = error_empty ⟨true ⊢ 2⟩ in
let result_36 : A_out{"c_out": integer} =
A_17 (A_in {"a_in"= a.a_33; "b_in"= a.b_35}) in
let a.c_37 : integer = result_36."c_out" in
let __38 : unit = assert (error_empty a.c_37 = 1) in
B_out {}
```

18
tests/test_money/bad/no_mingle.catala_en
View File

@ -15,21 +15,14 @@ scope A:
```catala-test-inline
$ catala Interpret -s A
[ERROR] Error during typechecking, incompatible types:
--> decimal
--> money
--> decimal
Error coming from typechecking the following expression:
--> tests/test_money/bad/no_mingle.catala_en
|
12 | definition z equals (x *$ y)
| ^^^^^^
+ Article
Type decimal coming from expression:
--> tests/test_money/bad/no_mingle.catala_en
|
12 | definition z equals (x *$ y)
| ^^
| ^
+ Article
Type money coming from expression:
@ -38,5 +31,12 @@ Type money coming from expression:
6 | context y content money
| ^^^^^
+ Article
Type decimal coming from expression:
--> tests/test_money/bad/no_mingle.catala_en
|
12 | definition z equals (x *$ y)
| ^^
+ Article
#return code 255#
```

2
tests/test_proof/bad/array_length-empty.catala_en
View File

@ -14,7 +14,7 @@ scope A:
$ catala Proof --disable_counterexamples
[ERROR] [A.y] This variable might return an empty error:
--> tests/test_proof/bad/array_length-empty.catala_en
|
|
6 | context y content boolean
| ^
+ Test

2
tests/test_proof/bad/array_length-overlap.catala_en
View File

@ -15,7 +15,7 @@ scope A:
$ catala Proof --disable_counterexamples
[ERROR] [A.y] At least two exceptions overlap for this variable:
--> tests/test_proof/bad/array_length-overlap.catala_en
|
|
6 | context y content boolean
| ^
+ Test

2
tests/test_proof/bad/dates_get_year-empty.catala_en
View File

@ -17,7 +17,7 @@ scope A:
$ catala Proof --disable_counterexamples
[ERROR] [A.y] This variable might return an empty error:
--> tests/test_proof/bad/dates_get_year-empty.catala_en
|
|
6 | context y content boolean
| ^
+ Test

2
tests/test_proof/bad/dates_get_year-overlap.catala_en
View File

@ -17,7 +17,7 @@ scope A:
$ catala Proof --disable_counterexamples
[ERROR] [A.y] At least two exceptions overlap for this variable:
--> tests/test_proof/bad/dates_get_year-overlap.catala_en
|
|
6 | context y content boolean
| ^
+ Test

2
tests/test_proof/bad/dates_simple-empty.catala_en
View File

@ -16,7 +16,7 @@ scope A:
$ catala Proof --disable_counterexamples
[ERROR] [A.y] This variable might return an empty error:
--> tests/test_proof/bad/dates_simple-empty.catala_en
|
|
6 | context y content boolean
| ^
+ Test

2
tests/test_proof/bad/dates_simple-overlap.catala_en
View File

@ -17,7 +17,7 @@ scope A:
$ catala Proof --disable_counterexamples
[ERROR] [A.y] At least two exceptions overlap for this variable:
--> tests/test_proof/bad/dates_simple-overlap.catala_en
|
|
6 | context y content boolean
| ^
+ Test

2
tests/test_proof/bad/duration-empty.catala_en
View File

@ -14,7 +14,7 @@ scope A:
$ catala Proof --disable_counterexamples
[ERROR] [A.y] This variable might return an empty error:
--> tests/test_proof/bad/duration-empty.catala_en
|
|
6 | context y content boolean
| ^
+ Test

2
tests/test_proof/bad/duration-overlap.catala_en
View File

@ -15,7 +15,7 @@ scope A:
$ catala Proof --disable_counterexamples
[ERROR] [A.y] At least two exceptions overlap for this variable:
--> tests/test_proof/bad/duration-overlap.catala_en
|
|
6 | context y content boolean
| ^
+ Test

2
tests/test_proof/bad/enums-empty.catala_en
View File

@ -25,7 +25,7 @@ scope A:
$ catala Proof --disable_counterexamples
[ERROR] [A.x] This variable might return an empty error:
--> tests/test_proof/bad/enums-empty.catala_en
|
|
15 | context x content integer
| ^
+ Test

2
tests/test_proof/bad/enums-nonbool-empty.catala_en
View File

@ -23,7 +23,7 @@ scope A:
$ catala Proof --disable_counterexamples
[ERROR] [A.x] This variable might return an empty error:
--> tests/test_proof/bad/enums-nonbool-empty.catala_en
|
|
13 | context x content integer
| ^
+ Test

2
tests/test_proof/bad/enums-nonbool-overlap.catala_en
View File

@ -23,7 +23,7 @@ scope A:
$ catala Proof --disable_counterexamples
[ERROR] [A.x] At least two exceptions overlap for this variable:
--> tests/test_proof/bad/enums-nonbool-overlap.catala_en
|
|
13 | context x content integer
| ^
+ Test

2
tests/test_proof/bad/enums-overlap.catala_en
View File

@ -25,7 +25,7 @@ scope A:
$ catala Proof --disable_counterexamples
[ERROR] [A.x] At least two exceptions overlap for this variable:
--> tests/test_proof/bad/enums-overlap.catala_en
|
|
15 | context x content integer
| ^
+ Test

2
tests/test_proof/bad/enums_inj-empty.catala_en
View File

@ -18,7 +18,7 @@ scope A:
$ catala Proof --disable_counterexamples
[ERROR] [A.y] This variable might return an empty error:
--> tests/test_proof/bad/enums_inj-empty.catala_en
|
|
10 | context y content integer
| ^
+ Article

2
tests/test_proof/bad/enums_inj-overlap.catala_en
View File

@ -20,7 +20,7 @@ scope A:
$ catala Proof --disable_counterexamples
[ERROR] [A.y] At least two exceptions overlap for this variable:
--> tests/test_proof/bad/enums_inj-overlap.catala_en
|
|
10 | context y content integer
| ^
+ Article

2
tests/test_proof/bad/enums_unit-empty.catala_en
View File

@ -23,7 +23,7 @@ scope A:
$ catala Proof --disable_counterexamples
[ERROR] [A.y] This variable might return an empty error:
--> tests/test_proof/bad/enums_unit-empty.catala_en
|
|
10 | context y content integer
| ^
+ Article

2
tests/test_proof/bad/enums_unit-overlap.catala_en
View File

@ -23,7 +23,7 @@ scope A:
$ catala Proof --disable_counterexamples
[ERROR] [A.y] At least two exceptions overlap for this variable:
--> tests/test_proof/bad/enums_unit-overlap.catala_en
|
|
10 | context y content integer
| ^
+ Article

2
tests/test_proof/bad/money-empty.catala_en
View File

@ -18,7 +18,7 @@ scope A:
$ catala Proof --disable_counterexamples
[ERROR] [A.y] This variable might return an empty error:
--> tests/test_proof/bad/money-empty.catala_en
|
|
8 | context y content boolean
| ^
+ Test

2
tests/test_proof/bad/money-overlap.catala_en
View File

@ -19,7 +19,7 @@ scope A:
$ catala Proof --disable_counterexamples
[ERROR] [A.y] At least two exceptions overlap for this variable:
--> tests/test_proof/bad/money-overlap.catala_en
|
|
8 | context y content boolean
| ^
+ Test

2
tests/test_proof/bad/no_vars-conflict.catala_en
View File

@ -19,7 +19,7 @@ scope A:
$ catala Proof --disable_counterexamples
[ERROR] [A.y] At least two exceptions overlap for this variable:
--> tests/test_proof/bad/no_vars-conflict.catala_en
|
|
8 | context y content integer
| ^
+ Test

2
tests/test_proof/bad/no_vars-empty.catala_en
View File

@ -18,7 +18,7 @@ scope A:
$ catala Proof --disable_counterexamples
[ERROR] [A.y] This variable might return an empty error:
--> tests/test_proof/bad/no_vars-empty.catala_en
|
|
7 | context y content integer
| ^
+ Test

6
tests/test_proof/bad/prolala_motivating_example.catala_en
View File

@ -125,7 +125,7 @@ scope Amount:
$ catala Proof --disable_counterexamples
[ERROR] [Amount.amount] This variable might return an empty error:
--> tests/test_proof/bad/prolala_motivating_example.catala_en
|
|
60 | context amount content integer
| ^^^^^^
+ ProLaLa 2022 Super Cash Bonus
@ -133,7 +133,7 @@ $ catala Proof --disable_counterexamples
Counterexample generation is disabled so none was generated.
[ERROR] [Eligibility.is_eligible] This variable might return an empty error:
--> tests/test_proof/bad/prolala_motivating_example.catala_en
|
|
11 | output is_eligible content boolean
| ^^^^^^^^^^^
+ ProLaLa 2022 Super Cash Bonus
@ -141,7 +141,7 @@ Counterexample generation is disabled so none was generated.
Counterexample generation is disabled so none was generated.
[ERROR] [Eligibility.is_eligible] At least two exceptions overlap for this variable:
--> tests/test_proof/bad/prolala_motivating_example.catala_en
|
|
11 | output is_eligible content boolean
| ^^^^^^^^^^^
+ ProLaLa 2022 Super Cash Bonus

2
tests/test_proof/bad/rationals-empty.catala_en
View File

@ -14,7 +14,7 @@ scope A:
$ catala Proof --disable_counterexamples
[ERROR] [A.y] This variable might return an empty error:
--> tests/test_proof/bad/rationals-empty.catala_en
|
|
6 | context y content boolean
| ^
+ Test

2
tests/test_proof/bad/rationals-overlap.catala_en
View File

@ -15,7 +15,7 @@ scope A:
$ catala Proof --disable_counterexamples
[ERROR] [A.y] At least two exceptions overlap for this variable:
--> tests/test_proof/bad/rationals-overlap.catala_en
|
|
6 | context y content boolean
| ^
+ Test

2
tests/test_proof/bad/sat_solving.catala_en
View File

@ -42,7 +42,7 @@ scope A:
$ catala Proof --disable_counterexamples
[ERROR] [A.x10] This variable might return an empty error:
--> tests/test_proof/bad/sat_solving.catala_en
|
|
15 | context x10 content boolean
| ^^^
+ Test

2
tests/test_proof/bad/structs-empty.catala_en
View File

@ -23,7 +23,7 @@ scope A:
$ catala Proof --disable_counterexamples
[ERROR] [A.x] This variable might return an empty error:
--> tests/test_proof/bad/structs-empty.catala_en
|
|
13 | context x content integer
| ^
+ Test

2
tests/test_proof/bad/structs-overlap.catala_en
View File

@ -23,7 +23,7 @@ scope A:
$ catala Proof --disable_counterexamples
[ERROR] [A.x] At least two exceptions overlap for this variable:
--> tests/test_proof/bad/structs-overlap.catala_en
|
|
13 | context x content integer
| ^
+ Test

12
tests/test_scope/bad/cycle_in_scope.catala_en
View File

@ -20,42 +20,42 @@ $ catala Interpret -s A
Cycle variable z, declared:
--> tests/test_scope/bad/cycle_in_scope.catala_en
|
|
7 | context z content integer
| ^
+ Article
Used here in the definition of another cycle variable x:
--> tests/test_scope/bad/cycle_in_scope.catala_en
|
|
14 | definition x equals z
| ^
+ Article
Cycle variable y, declared:
--> tests/test_scope/bad/cycle_in_scope.catala_en
|
|
6 | context y content integer
| ^
+ Article
Used here in the definition of another cycle variable z:
--> tests/test_scope/bad/cycle_in_scope.catala_en
|
|
13 | definition z under condition y < 1 consequence equals y
| ^
+ Article
Cycle variable x, declared:
--> tests/test_scope/bad/cycle_in_scope.catala_en
|
|
5 | context x content integer
| ^
+ Article
Used here in the definition of another cycle variable y:
--> tests/test_scope/bad/cycle_in_scope.catala_en
|
|
11 | definition y under condition x >= 0 consequence equals x
| ^
+ Article

8
tests/test_scope/bad/cyclic_scopes.catala_en
View File

@ -22,28 +22,28 @@ $ catala Interpret -s A
Cycle variable B, declared:
--> tests/test_scope/bad/cyclic_scopes.catala_en
|
|
8 | declaration scope B:
| ^
+ Article
Used here in the definition of another cycle variable A:
--> tests/test_scope/bad/cyclic_scopes.catala_en
|
|
5 | b scope B
| ^
+ Article
Cycle variable A, declared:
--> tests/test_scope/bad/cyclic_scopes.catala_en
|
|
4 | declaration scope A:
| ^
+ Article
Used here in the definition of another cycle variable B:
--> tests/test_scope/bad/cyclic_scopes.catala_en
|
|
9 | a scope A
| ^
+ Article

4
tests/test_scope/bad/scope.catala_en
View File

@ -20,14 +20,14 @@ $ catala Interpret -s A
This consequence has a valid justification:
--> tests/test_scope/bad/scope.catala_en
|
|
13 | definition b under condition not c consequence equals 1337
| ^^^^
+ Article
This consequence has a valid justification:
--> tests/test_scope/bad/scope.catala_en
|
|
14 | definition b under condition not c consequence equals 0
| ^
+ Article

2
tests/test_scope/bad/sub_vars_in_sub_var.catala_en
View File

@ -18,7 +18,7 @@ $ catala Interpret -s A
[ERROR] The subscope a is used when defining one of its inputs, but recursion is forbidden in Catala
--> tests/test_scope/bad/sub_vars_in_sub_var.catala_en
|
|
13 | definition a.y equals if a.x then 0 else 1
| ^^^
+ Article

20
tests/test_scope/good/191_fix_record_name_confusion.catala_en
View File

@ -48,14 +48,14 @@ let scope_a (scope_a_in: ScopeAIn.t) : ScopeAOut.t =
(handle_default
{filename = "tests/test_scope/good/191_fix_record_name_confusion.catala_en";
start_line=5; start_column=18; end_line=5; end_column=19;
law_headings=["Article"]} ([|(fun (_: _) -> a_ ())|])
(fun (_: _) -> true)
(fun (_: _) ->
law_headings=["Article"]} ([|(fun (_: unit) -> a_ ())|])
(fun (_: unit) -> true)
(fun (_: unit) ->
handle_default
{filename = "tests/test_scope/good/191_fix_record_name_confusion.catala_en";
start_line=5; start_column=18; end_line=5; end_column=19;
law_headings=["Article"]} ([||]) (fun (_: _) -> true)
(fun (_: _) -> true)))
law_headings=["Article"]} ([||]) (fun (_: unit) -> true)
(fun (_: unit) -> true)))
with
EmptyError -> (raise (NoValueProvided
{filename = "tests/test_scope/good/191_fix_record_name_confusion.catala_en";
@ -73,14 +73,14 @@ let scope_b (scope_b_in: ScopeBIn.t) : ScopeBOut.t =
(handle_default
{filename = "tests/test_scope/good/191_fix_record_name_confusion.catala_en";
start_line=8; start_column=11; end_line=8; end_column=12;
law_headings=["Article"]} ([|(fun (_: _) -> a_ ())|])
(fun (_: _) -> true)
(fun (_: _) ->
law_headings=["Article"]} ([|(fun (_: unit) -> a_ ())|])
(fun (_: unit) -> true)
(fun (_: unit) ->
handle_default
{filename = "tests/test_scope/good/191_fix_record_name_confusion.catala_en";
start_line=8; start_column=11; end_line=8; end_column=12;
law_headings=["Article"]} ([||]) (fun (_: _) -> true)
(fun (_: _) -> scope_a_dot_a_)))
law_headings=["Article"]} ([||]) (fun (_: unit) -> true)
(fun (_: unit) -> scope_a_dot_a_)))
with
EmptyError -> (raise (NoValueProvided
{filename = "tests/test_scope/good/191_fix_record_name_confusion.catala_en";

10
tests/test_scope/good/simple.catala_en
View File

@ -11,10 +11,10 @@ scope Foo:
```catala-test-inline
$ catala Lcalc -s Foo
let Foo =
λ (Foo_in_27: Foo_in{}) →
let bar_28 : integer =
λ (Foo_in_28: Foo_in{}) →
let bar_29 : integer =
try
handle_default_0 [] (λ (__29: any) → true) (λ (__30: any) → 0)
with EmptyError -> raise NoValueProvided in
Foo_out {"bar_out"= bar_28}
handle_default_0 [] (λ (__30: unit) → true)
(λ (__31: unit) → 0) with EmptyError -> raise NoValueProvided in
Foo_out {"bar_out"= bar_29}
```

2
tests/test_struct/bad/ambiguous_fields.catala_en
View File

@ -21,7 +21,7 @@ $ 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 | definition y equals x.f
| ^
+ Article

4
tests/test_struct/bad/bug_107.catala_en
View File

@ -22,14 +22,14 @@ $ catala Interpret -s A
First definition:
--> tests/test_struct/bad/bug_107.catala_en
|
|
4 | declaration structure S:
| ^
+ https://github.com/CatalaLang/catala/issues/107
Second definition:
--> tests/test_struct/bad/bug_107.catala_en
|
|
8 | declaration structure S:
| ^
+ https://github.com/CatalaLang/catala/issues/107

2
tests/test_struct/bad/empty_struct.catala_en
View File

@ -12,7 +12,7 @@ $ catala Typecheck
[ERROR] The struct Foo does not have any fields; give it some for Catala to be able to accept it.
--> tests/test_struct/bad/empty_struct.catala_en
|
|
4 | declaration structure Foo:
| ^^^
+ Test

15
tests/test_struct/bad/nested.catala_en
View File

@ -1,23 +1,24 @@
## Article
```catala
declaration structure S:
data x content S
declaration enumeration E:
-- Empty
-- Rec content E
declaration scope A:
context y content S
context y content E
scope A:
definition y equals S { -- x: 1 }
definition y equals E.Empty
```
```catala-test-inline
$ catala Interpret -s A
[ERROR] The type S is defined using itself, which is forbidden since Catala does not provide recursive types
[ERROR] The type E is defined using itself, which is forbidden since Catala does not provide recursive types
--> tests/test_struct/bad/nested.catala_en
|
5 | data x content S
|
6 | -- Rec content E
| ^
+ Article
#return code 255#

8
tests/test_struct/bad/nested2.catala_en
View File

@ -19,28 +19,28 @@ $ catala Interpret -s A
Cycle type S, declared:
--> tests/test_struct/bad/nested2.catala_en
|
|
4 | declaration structure S:
| ^
+ Article
Used here in the definition of another cycle type E:
--> tests/test_struct/bad/nested2.catala_en
|
|
10 | -- Case2 content S
| ^
+ Article
Cycle type E, declared:
--> tests/test_struct/bad/nested2.catala_en
|
|
8 | declaration enumeration E:
| ^
+ Article
Used here in the definition of another cycle type S:
--> tests/test_struct/bad/nested2.catala_en
|
|
5 | data x content E
| ^
+ Article

2
tests/test_struct/bad/nonexisting_struct.catala_en
View File

@ -18,7 +18,7 @@ $ catala Interpret -s A
[ERROR] Struct Fo has not been defined before
--> tests/test_struct/bad/nonexisting_struct.catala_en
|
|
13 | definition y equals x.Fo.f
| ^^
+ Article

2
tests/test_struct/bad/wrong_qualified_field.catala_en
View File

@ -22,7 +22,7 @@ $ catala Interpret -s A
[ERROR] Struct Foo does not contain field g
--> tests/test_struct/bad/wrong_qualified_field.catala_en
|
|
17 | definition y equals x.Foo.g
| ^^^^^^^
+ Article

24
tests/test_typing/bad/err1.catala_en
View File

@ -13,28 +13,28 @@ scope S:
```catala-test-inline
$ catala Typecheck
[ERROR] Error during typechecking, incompatible types:
--> integer
--> decimal
--> integer
Error coming from typechecking the following expression:
--> tests/test_typing/bad/err1.catala_en
|
|
7 | Structure { -- i: 4.1 -- e: y };
| ^^^
+
Type integer coming from expression:
--> tests/test_typing/bad/common.catala_en
|
8 | data i content integer
| ^^^^^^^
+
+
Type decimal coming from expression:
--> tests/test_typing/bad/err1.catala_en
|
|
7 | Structure { -- i: 4.1 -- e: y };
| ^^^
+
+
Type integer coming from expression:
--> tests/test_typing/bad/common.catala_en
|
8 | data i content integer
| ^^^^^^^
+
#return code 255#
```

Some files were not shown because too many files have changed in this diff Show More