CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-11-08 07:51:43 +03:00
Code Issues Projects Releases Wiki Activity

Merge branch 'master' into adelaett-withoutexceptionsfix

Browse Source
This commit is contained in:
adelaett 2023-04-11 11:49:22 +02:00
commit 3e35d4b826
No known key found for this signature in database
GPG Key ID: 367A8C08F513BD65
17 changed files with 765 additions and 637 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
.nix/catala.nix
View File

@ -11,7 +11,6 @@
, js_of_ocaml-ppx
, menhir
, menhirLib
, ocaml-crunch
, ocamlgraph
, pkgs
, ppx_deriving
@ -24,6 +23,7 @@
, z3
, zarith
, zarith_stubs_js
, ocaml-crunch
, cohttp-lwt-unix
, ppx_expect
}:

10
compiler/catala_utils/cli.ml
View File

@ -30,7 +30,8 @@ type backend_option_builtin =
| `Dcalc
| `Scopelang
| `Proof
| `DcalcInvariants ]
| `DcalcInvariants
| `Interpret_Lcalc ]
type 'a backend_option = [ backend_option_builtin | `Plugin of 'a ]
@ -43,6 +44,7 @@ let language_code =
let backend_option_to_string = function
| `Interpret -> "Interpret"
| `Interpret_Lcalc -> "Interpret_Lcalc"
| `Makefile -> "Makefile"
| `OCaml -> "Ocaml"
| `Scopelang -> "Scopelang"
@ -60,6 +62,7 @@ let backend_option_to_string = function
let backend_option_of_string backend =
match String.lowercase_ascii backend with
| "interpret" -> `Interpret
| "interpret_lcalc" -> `Interpret_Lcalc
| "makefile" -> `Makefile
| "ocaml" -> `OCaml
| "scopelang" -> `Scopelang
@ -358,6 +361,11 @@ let info =
"Runs the interpreter on the Catala program, executing the scope \
specified by the $(b,-s) option assuming no additional external \
inputs." );
`I
( "$(b,Intepret_Lcalc)",
"Runs the interpreter on the lcalc pass on the Catala program, \
executing the scope specified by the $(b,-s) option assuming no \
additional external inputs." );
`I
( "$(b,Typecheck)",
"Parses and typechecks a Catala program, without interpreting it." );

1
compiler/catala_utils/cli.mli
View File

@ -22,6 +22,7 @@ type backend_option_builtin =
| `Makefile
| `Html
| `Interpret
| `Interpret_Lcalc
| `Typecheck
| `OCaml
| `Python

576
compiler/dcalc/interpreter.ml
View File

@ -1,576 +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>, Emile Rolley <emile.rolley@tuta.io>
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. *)
(** Reference interpreter for the default calculus *)
open Catala_utils
open Shared_ast
module Runtime = Runtime_ocaml.Runtime
(** {1 Helpers} *)
let is_empty_error (e : 'm Ast.expr) : bool =
match Marked.unmark e with EEmptyError -> true | _ -> false
let log_indent = ref 0
(** {1 Evaluation} *)
let print_log ctx entry infos pos e =
if !Cli.trace_flag then
match entry with
| VarDef _ ->
(* TODO: this usage of Format is broken, Formatting requires that all is
formatted in one pass, without going through intermediate "%s" *)
Cli.log_format "%*s%a %a: %s" (!log_indent * 2) "" Print.log_entry entry
Print.uid_list infos
(match Marked.unmark e with
| EAbs _ -> Cli.with_style [ANSITerminal.green] "<function>"
| _ ->
let expr_str =
Format.asprintf "%a" (Expr.format ctx ~debug:false) e
in
let expr_str =
Re.Pcre.substitute ~rex:(Re.Pcre.regexp "\n\\s*")
~subst:(fun _ -> " ")
expr_str
in
Cli.with_style [ANSITerminal.green] "%s" expr_str)
| PosRecordIfTrueBool -> (
match pos <> Pos.no_pos, Marked.unmark e with
| true, ELit (LBool true) ->
Cli.log_format "%*s%a%s:\n%s" (!log_indent * 2) "" Print.log_entry entry
(Cli.with_style [ANSITerminal.green] "Definition applied")
(Cli.add_prefix_to_each_line (Pos.retrieve_loc_text pos) (fun _ ->
Format.asprintf "%*s" (!log_indent * 2) ""))
| _ -> ())
| BeginCall ->
Cli.log_format "%*s%a %a" (!log_indent * 2) "" Print.log_entry entry
Print.uid_list infos;
log_indent := !log_indent + 1
| EndCall ->
log_indent := !log_indent - 1;
Cli.log_format "%*s%a %a" (!log_indent * 2) "" Print.log_entry entry
Print.uid_list infos
(* Todo: this should be handled early when resolving overloads. Here we have
proper structural equality, but the OCaml backend for example uses the
builtin equality function instead of this. *)
let rec handle_eq ctx pos e1 e2 =
let open Runtime.Oper in
match e1, e2 with
| ELit LUnit, ELit LUnit -> true
| ELit (LBool b1), ELit (LBool b2) -> not (o_xor b1 b2)
| ELit (LInt x1), ELit (LInt x2) -> o_eq_int_int x1 x2
| ELit (LRat x1), ELit (LRat x2) -> o_eq_rat_rat x1 x2
| ELit (LMoney x1), ELit (LMoney x2) -> o_eq_mon_mon x1 x2
| ELit (LDuration x1), ELit (LDuration x2) -> o_eq_dur_dur x1 x2
| ELit (LDate x1), ELit (LDate x2) -> o_eq_dat_dat x1 x2
| EArray es1, EArray es2 -> (
try
List.for_all2
(fun e1 e2 ->
match evaluate_operator ctx Eq pos [e1; e2] with
| ELit (LBool b) -> b
| _ -> assert false
(* should not happen *))
es1 es2
with Invalid_argument _ -> false)
| EStruct { fields = es1; name = s1 }, EStruct { fields = es2; name = s2 } ->
StructName.equal s1 s2
&& StructField.Map.equal
(fun e1 e2 ->
match evaluate_operator ctx Eq pos [e1; e2] with
| ELit (LBool b) -> b
| _ -> assert false
(* should not happen *))
es1 es2
| ( EInj { e = e1; cons = i1; name = en1 },
EInj { e = e2; cons = i2; name = en2 } ) -> (
try
EnumName.equal en1 en2
&& EnumConstructor.equal i1 i2
&&
match evaluate_operator ctx Eq pos [e1; e2] with
| ELit (LBool b) -> b
| _ -> assert false
(* should not happen *)
with Invalid_argument _ -> false)
| _, _ -> false (* comparing anything else return false *)
(* Call-by-value: the arguments are expected to be already evaluated here *)
and evaluate_operator :
decl_ctx -> dcalc operator -> Pos.t -> 'm Ast.expr list -> 'm Ast.naked_expr
=
fun ctx op pos args ->
let protect f x y =
let get_binop_args_pos = function
| (arg0 :: arg1 :: _ : 'm Ast.expr list) ->
[None, Expr.pos arg0; None, Expr.pos arg1]
| _ -> assert false
in
try f x y with
| Division_by_zero ->
Errors.raise_multispanned_error
[
Some "The division operator:", pos;
Some "The null denominator:", Expr.pos (List.nth args 1);
]
"division by zero at runtime"
| Runtime.UncomparableDurations ->
Errors.raise_multispanned_error (get_binop_args_pos args)
"Cannot compare together durations that cannot be converted to a \
precise number of days"
in
let err () =
Errors.raise_multispanned_error
([Some "Operator:", pos]
@ List.mapi
(fun i arg ->
( Some
(Format.asprintf "Argument n°%d, value %a" (i + 1)
(Expr.format ctx ~debug:true)
arg),
Expr.pos arg ))
args)
"Operator applied to the wrong arguments\n\
(should not happen if the term was well-typed)"
in
let open Runtime.Oper in
if List.exists (function EEmptyError, _ -> true | _ -> false) args then
EEmptyError
else
match op, args with
| Length, [(EArray es, _)] ->
ELit (LInt (Runtime.integer_of_int (List.length es)))
| Log (entry, infos), [e'] ->
print_log ctx entry infos pos e';
Marked.unmark e'
| Eq, [(e1, _); (e2, _)] -> ELit (LBool (handle_eq ctx pos e1 e2))
| Map, [f; (EArray es, _)] ->
EArray
(List.map
(fun e' ->
evaluate_expr ctx
(Marked.same_mark_as (EApp { f; args = [e'] }) e'))
es)
| Reduce, [_; default; (EArray [], _)] -> Marked.unmark default
| Reduce, [f; _; (EArray (x0 :: xn), _)] ->
Marked.unmark
(List.fold_left
(fun acc x ->
evaluate_expr ctx
(Marked.same_mark_as (EApp { f; args = [acc; x] }) f))
x0 xn)
| Concat, [(EArray es1, _); (EArray es2, _)] -> EArray (es1 @ es2)
| Filter, [f; (EArray es, _)] ->
EArray
(List.filter
(fun e' ->
match
evaluate_expr ctx
(Marked.same_mark_as (EApp { f; args = [e'] }) e')
with
| ELit (LBool b), _ -> b
| _ ->
Errors.raise_spanned_error
(Expr.pos (List.nth args 0))
"This predicate evaluated to something else than a boolean \
(should not happen if the term was well-typed)")
es)
| Fold, [f; init; (EArray es, _)] ->
Marked.unmark
(List.fold_left
(fun acc e' ->
evaluate_expr ctx
(Marked.same_mark_as (EApp { f; args = [acc; e'] }) e'))
init es)
| (Length | Log _ | Eq | Map | Concat | Filter | Fold | Reduce), _ -> err ()
| Not, [(ELit (LBool b), _)] -> ELit (LBool (o_not b))
| GetDay, [(ELit (LDate d), _)] -> ELit (LInt (o_getDay d))
| GetMonth, [(ELit (LDate d), _)] -> ELit (LInt (o_getMonth d))
| GetYear, [(ELit (LDate d), _)] -> ELit (LInt (o_getYear d))
| FirstDayOfMonth, [(ELit (LDate d), _)] ->
ELit (LDate (o_firstDayOfMonth d))
| LastDayOfMonth, [(ELit (LDate d), _)] -> ELit (LDate (o_lastDayOfMonth d))
| And, [(ELit (LBool b1), _); (ELit (LBool b2), _)] ->
ELit (LBool (o_and b1 b2))
| Or, [(ELit (LBool b1), _); (ELit (LBool b2), _)] ->
ELit (LBool (o_or b1 b2))
| Xor, [(ELit (LBool b1), _); (ELit (LBool b2), _)] ->
ELit (LBool (o_xor b1 b2))
| ( ( Not | GetDay | GetMonth | GetYear | FirstDayOfMonth | LastDayOfMonth
| And | Or | Xor ),
_ ) ->
err ()
| Minus_int, [(ELit (LInt x), _)] -> ELit (LInt (o_minus_int x))
| Minus_rat, [(ELit (LRat x), _)] -> ELit (LRat (o_minus_rat x))
| Minus_mon, [(ELit (LMoney x), _)] -> ELit (LMoney (o_minus_mon x))
| Minus_dur, [(ELit (LDuration x), _)] -> ELit (LDuration (o_minus_dur x))
| ToRat_int, [(ELit (LInt i), _)] -> ELit (LRat (o_torat_int i))
| ToRat_mon, [(ELit (LMoney i), _)] -> ELit (LRat (o_torat_mon i))
| ToMoney_rat, [(ELit (LRat i), _)] -> ELit (LMoney (o_tomoney_rat i))
| Round_mon, [(ELit (LMoney m), _)] -> ELit (LMoney (o_round_mon m))
| Round_rat, [(ELit (LRat m), _)] -> ELit (LRat (o_round_rat m))
| Add_int_int, [(ELit (LInt x), _); (ELit (LInt y), _)] ->
ELit (LInt (o_add_int_int x y))
| Add_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LRat (o_add_rat_rat x y))
| Add_mon_mon, [(ELit (LMoney x), _); (ELit (LMoney y), _)] ->
ELit (LMoney (o_add_mon_mon x y))
| Add_dat_dur r, [(ELit (LDate x), _); (ELit (LDuration y), _)] ->
ELit (LDate (o_add_dat_dur r x y))
| Add_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LDuration (o_add_dur_dur x y))
| Sub_int_int, [(ELit (LInt x), _); (ELit (LInt y), _)] ->
ELit (LInt (o_sub_int_int x y))
| Sub_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LRat (o_sub_rat_rat x y))
| Sub_mon_mon, [(ELit (LMoney x), _); (ELit (LMoney y), _)] ->
ELit (LMoney (o_sub_mon_mon x y))
| Sub_dat_dat, [(ELit (LDate x), _); (ELit (LDate y), _)] ->
ELit (LDuration (o_sub_dat_dat x y))
| Sub_dat_dur, [(ELit (LDate x), _); (ELit (LDuration y), _)] ->
ELit (LDate (o_sub_dat_dur x y))
| Sub_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LDuration (o_sub_dur_dur x y))
| Mult_int_int, [(ELit (LInt x), _); (ELit (LInt y), _)] ->
ELit (LInt (o_mult_int_int x y))
| Mult_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LRat (o_mult_rat_rat x y))
| Mult_mon_rat, [(ELit (LMoney x), _); (ELit (LRat y), _)] ->
ELit (LMoney (o_mult_mon_rat x y))
| Mult_dur_int, [(ELit (LDuration x), _); (ELit (LInt y), _)] ->
ELit (LDuration (o_mult_dur_int x y))
| Div_int_int, [(ELit (LInt x), _); (ELit (LInt y), _)] ->
ELit (LRat (protect o_div_int_int x y))
| Div_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LRat (protect o_div_rat_rat x y))
| Div_mon_mon, [(ELit (LMoney x), _); (ELit (LMoney y), _)] ->
ELit (LRat (protect o_div_mon_mon x y))
| Div_mon_rat, [(ELit (LMoney x), _); (ELit (LRat y), _)] ->
ELit (LMoney (protect o_div_mon_rat x y))
| Div_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LRat (protect o_div_dur_dur x y))
| Lt_int_int, [(ELit (LInt x), _); (ELit (LInt y), _)] ->
ELit (LBool (o_lt_int_int x y))
| Lt_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LBool (o_lt_rat_rat x y))
| Lt_mon_mon, [(ELit (LMoney x), _); (ELit (LMoney y), _)] ->
ELit (LBool (o_lt_mon_mon x y))
| Lt_dat_dat, [(ELit (LDate x), _); (ELit (LDate y), _)] ->
ELit (LBool (o_lt_dat_dat x y))
| Lt_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LBool (protect o_lt_dur_dur x y))
| Lte_int_int, [(ELit (LInt x), _); (ELit (LInt y), _)] ->
ELit (LBool (o_lte_int_int x y))
| Lte_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LBool (o_lte_rat_rat x y))
| Lte_mon_mon, [(ELit (LMoney x), _); (ELit (LMoney y), _)] ->
ELit (LBool (o_lte_mon_mon x y))
| Lte_dat_dat, [(ELit (LDate x), _); (ELit (LDate y), _)] ->
ELit (LBool (o_lte_dat_dat x y))
| Lte_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LBool (protect o_lte_dur_dur x y))
| Gt_int_int, [(ELit (LInt x), _); (ELit (LInt y), _)] ->
ELit (LBool (o_gt_int_int x y))
| Gt_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LBool (o_gt_rat_rat x y))
| Gt_mon_mon, [(ELit (LMoney x), _); (ELit (LMoney y), _)] ->
ELit (LBool (o_gt_mon_mon x y))
| Gt_dat_dat, [(ELit (LDate x), _); (ELit (LDate y), _)] ->
ELit (LBool (o_gt_dat_dat x y))
| Gt_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LBool (protect o_gt_dur_dur x y))
| Gte_int_int, [(ELit (LInt x), _); (ELit (LInt y), _)] ->
ELit (LBool (o_gte_int_int x y))
| Gte_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LBool (o_gte_rat_rat x y))
| Gte_mon_mon, [(ELit (LMoney x), _); (ELit (LMoney y), _)] ->
ELit (LBool (o_gte_mon_mon x y))
| Gte_dat_dat, [(ELit (LDate x), _); (ELit (LDate y), _)] ->
ELit (LBool (o_gte_dat_dat x y))
| Gte_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LBool (protect o_gte_dur_dur x y))
| Eq_int_int, [(ELit (LInt x), _); (ELit (LInt y), _)] ->
ELit (LBool (o_eq_int_int x y))
| Eq_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LBool (o_eq_rat_rat x y))
| Eq_mon_mon, [(ELit (LMoney x), _); (ELit (LMoney y), _)] ->
ELit (LBool (o_eq_mon_mon x y))
| Eq_dat_dat, [(ELit (LDate x), _); (ELit (LDate y), _)] ->
ELit (LBool (o_eq_dat_dat x y))
| Eq_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LBool (protect o_eq_dur_dur x y))
| ( ( Minus_int | Minus_rat | Minus_mon | Minus_dur | ToRat_int | ToRat_mon
| ToMoney_rat | Round_rat | Round_mon | Add_int_int | Add_rat_rat
| Add_mon_mon | Add_dat_dur _ | Add_dur_dur | Sub_int_int | Sub_rat_rat
| Sub_mon_mon | Sub_dat_dat | Sub_dat_dur | Sub_dur_dur | Mult_int_int
| Mult_rat_rat | Mult_mon_rat | Mult_dur_int | Div_int_int | Div_rat_rat
| Div_mon_mon | Div_mon_rat | Div_dur_dur | Lt_int_int | Lt_rat_rat
| Lt_mon_mon | Lt_dat_dat | Lt_dur_dur | Lte_int_int | Lte_rat_rat
| Lte_mon_mon | Lte_dat_dat | Lte_dur_dur | Gt_int_int | Gt_rat_rat
| Gt_mon_mon | Gt_dat_dat | Gt_dur_dur | Gte_int_int | Gte_rat_rat
| Gte_mon_mon | Gte_dat_dat | Gte_dur_dur | Eq_int_int | Eq_rat_rat
| Eq_mon_mon | Eq_dat_dat | Eq_dur_dur | HandleDefault
| HandleDefaultOpt ),
_ ) ->
err ()
and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr =
match Marked.unmark e with
| EVar _ ->
Errors.raise_spanned_error (Expr.pos e)
"free variable found at evaluation (should not happen if term was \
well-typed)"
| EApp { f = e1; args } -> (
let e1 = evaluate_expr ctx e1 in
let args = List.map (evaluate_expr ctx) args in
match Marked.unmark e1 with
| EAbs { binder; _ } ->
if Bindlib.mbinder_arity binder = List.length args then
evaluate_expr ctx
(Bindlib.msubst binder (Array.of_list (List.map Marked.unmark args)))
else
Errors.raise_spanned_error (Expr.pos e)
"wrong function call, expected %d arguments, got %d"
(Bindlib.mbinder_arity binder)
(List.length args)
| EOp { op; _ } ->
Marked.same_mark_as (evaluate_operator ctx op (Expr.pos e) args) e
| EEmptyError -> Marked.same_mark_as EEmptyError e
| _ ->
Errors.raise_spanned_error (Expr.pos e)
"function has not been reduced to a lambda at evaluation (should not \
happen if the term was well-typed")
| EAbs _ | ELit _ | EOp _ -> e (* these are values *)
| EStruct { fields = es; name } ->
let new_es = StructField.Map.map (evaluate_expr ctx) es in
if StructField.Map.exists (fun _ e -> is_empty_error e) new_es then
Marked.same_mark_as EEmptyError e
else Marked.same_mark_as (EStruct { fields = new_es; name }) e
| EStructAccess { e = e1; name = s; field } -> (
let e1 = evaluate_expr ctx e1 in
match Marked.unmark e1 with
| EStruct { fields = es; name = s' } -> (
if not (StructName.equal s s') then
Errors.raise_multispanned_error
[None, Expr.pos e; None, Expr.pos e1]
"Error during struct access: not the same structs (should not happen \
if the term was well-typed)";
match StructField.Map.find_opt field es with
| Some e' -> e'
| None ->
Errors.raise_spanned_error (Expr.pos e1)
"Invalid field access %a in struct %a (should not happen if the term \
was well-typed)"
StructField.format_t field StructName.format_t s)
| EEmptyError -> Marked.same_mark_as EEmptyError e
| _ ->
Errors.raise_spanned_error (Expr.pos e1)
"The expression %a should be a struct %a but is not (should not happen \
if the term was well-typed)"
(Expr.format ctx ~debug:true)
e StructName.format_t s)
| ETuple es ->
Marked.same_mark_as (ETuple (List.map (evaluate_expr ctx) es)) e
| ETupleAccess { e = e1; index; size } -> (
match evaluate_expr ctx e1 with
| ETuple es, _ when List.length es = size -> List.nth es index
| e ->
Errors.raise_spanned_error (Expr.pos e)
"The expression %a was expected to be a tuple of size %d (should not \
happen if the term was well-typed)"
(Expr.format ctx ~debug:true)
e size)
| EInj { e = e1; name; cons } ->
let e1' = evaluate_expr ctx e1 in
if is_empty_error e then Marked.same_mark_as EEmptyError e
else Marked.same_mark_as (EInj { e = e1'; name; cons }) e
| EMatch { e = e1; cases = es; name } -> (
let e1 = evaluate_expr ctx e1 in
match Marked.unmark e1 with
| EInj { e = e1; cons; name = name' } ->
if not (EnumName.equal name name') then
Errors.raise_multispanned_error
[None, Expr.pos e; None, Expr.pos e1]
"Error during match: two different enums found (should not happen if \
the term was well-typed)";
let es_n =
match EnumConstructor.Map.find_opt cons es with
| Some es_n -> es_n
| None ->
Errors.raise_spanned_error (Expr.pos e)
"sum type index error (should not happen if the term was \
well-typed)"
in
let new_e = Marked.same_mark_as (EApp { f = es_n; args = [e1] }) e in
evaluate_expr ctx new_e
| EEmptyError -> Marked.same_mark_as EEmptyError e
| _ ->
Errors.raise_spanned_error (Expr.pos e1)
"Expected a term having a sum type as an argument to a match (should \
not happen if the term was well-typed")
| EDefault { excepts; just; cons } -> (
let excepts = List.map (evaluate_expr ctx) excepts in
let empty_count = List.length (List.filter is_empty_error excepts) in
match List.length excepts - empty_count with
| 0 -> (
let just = evaluate_expr ctx just in
match Marked.unmark just with
| EEmptyError -> Marked.same_mark_as EEmptyError e
| ELit (LBool true) -> evaluate_expr ctx cons
| ELit (LBool false) -> Marked.same_mark_as EEmptyError e
| _ ->
Errors.raise_spanned_error (Expr.pos e)
"Default justification has not been reduced to a boolean at \
evaluation (should not happen if the term was well-typed")
| 1 -> List.find (fun sub -> not (is_empty_error sub)) excepts
| _ ->
Errors.raise_multispanned_error
(List.map
(fun except ->
Some "This consequence has a valid justification:", Expr.pos except)
(List.filter (fun sub -> not (is_empty_error sub)) excepts))
"There is a conflict between multiple valid consequences for assigning \
the same variable.")
| EIfThenElse { cond; etrue; efalse } -> (
match Marked.unmark (evaluate_expr ctx cond) with
| ELit (LBool true) -> evaluate_expr ctx etrue
| ELit (LBool false) -> evaluate_expr ctx efalse
| EEmptyError -> Marked.same_mark_as EEmptyError e
| _ ->
Errors.raise_spanned_error (Expr.pos cond)
"Expected a boolean literal for the result of this condition (should \
not happen if the term was well-typed)")
| EArray es ->
let new_es = List.map (evaluate_expr ctx) es in
if List.exists is_empty_error new_es then Marked.same_mark_as EEmptyError e
else Marked.same_mark_as (EArray new_es) e
| EEmptyError -> Marked.same_mark_as EEmptyError e
| EErrorOnEmpty e' ->
let e' = evaluate_expr ctx e' in
if Marked.unmark e' = EEmptyError then
Errors.raise_spanned_error (Expr.pos e')
"This variable evaluated to an empty term (no rule that defined it \
applied in this situation)"
else e'
| EAssert e' -> (
match Marked.unmark (evaluate_expr ctx e') with
| ELit (LBool true) -> Marked.same_mark_as (ELit LUnit) e'
| ELit (LBool false) -> (
match Marked.unmark e' with
| EErrorOnEmpty
( EApp
{
f = EOp { op; _ }, _;
args = [((ELit _, _) as e1); ((ELit _, _) as e2)];
},
_ ) ->
Errors.raise_spanned_error (Expr.pos e') "Assertion failed: %a %a %a"
(Expr.format ctx ~debug:false)
e1 Print.operator op
(Expr.format ctx ~debug:false)
e2
| EApp
{
f = EOp { op = Log _; _ }, _;
args =
[
( EApp
{
f = EOp { op; _ }, _;
args = [((ELit _, _) as e1); ((ELit _, _) as e2)];
},
_ );
];
} ->
Errors.raise_spanned_error (Expr.pos e') "Assertion failed: %a %a %a"
(Expr.format ctx ~debug:false)
e1 Print.operator op
(Expr.format ctx ~debug:false)
e2
| EApp
{
f = EOp { op; _ }, _;
args = [((ELit _, _) as e1); ((ELit _, _) as e2)];
} ->
Errors.raise_spanned_error (Expr.pos e') "Assertion failed: %a %a %a"
(Expr.format ctx ~debug:false)
e1 Print.operator op
(Expr.format ctx ~debug:false)
e2
| _ ->
Cli.debug_format "%a" (Expr.format ctx) e';
Errors.raise_spanned_error (Expr.pos e') "Assertion failed")
| EEmptyError -> Marked.same_mark_as EEmptyError e
| _ ->
Errors.raise_spanned_error (Expr.pos e')
"Expected a boolean literal for the result of this assertion (should \
not happen if the term was well-typed)")
(** {1 API} *)
let interpret_program :
'm. decl_ctx -> 'm Ast.expr -> (Uid.MarkedString.info * 'm Ast.expr) list
=
fun (ctx : decl_ctx) (e : 'm Ast.expr) :
(Uid.MarkedString.info * 'm Ast.expr) list ->
match evaluate_expr ctx e with
| (EAbs { tys = [((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
an empty thunked term. But for [input] arguments of another type, we
cannot provide anything so we have to fail. *)
let taus = StructName.Map.find s_in ctx.ctx_structs in
let application_term =
StructField.Map.map
(fun ty ->
match Marked.unmark ty with
| TArrow (ty_in, ty_out) ->
Expr.make_abs
(Array.of_list @@ List.map (fun _ -> Var.make "_") ty_in)
(Bindlib.box EEmptyError, Expr.with_ty mark_e ty_out)
ty_in (Expr.mark_pos mark_e)
| _ ->
Errors.raise_spanned_error (Marked.get_mark ty)
"This scope needs input arguments to be executed. But the Catala \
built-in interpreter does not have a way to retrieve input \
values from the command line, so it cannot execute this scope. \
Please create another scope thatprovide the input arguments to \
this one and execute it instead. ")
taus
in
let to_interpret =
Expr.make_app (Expr.box e)
[Expr.estruct s_in application_term mark_e]
(Expr.pos e)
in
match Marked.unmark (evaluate_expr ctx (Expr.unbox to_interpret)) with
| EStruct { fields; _ } ->
List.map
(fun (fld, e) -> StructField.get_info fld, e)
(StructField.Map.bindings fields)
| _ ->
Errors.raise_spanned_error (Expr.pos e)
"The interpretation of a program should always yield a struct \
corresponding to the scope variables"
end
| _ ->
Errors.raise_spanned_error (Expr.pos e)
"The interpreter can only interpret terms starting with functions having \
thunked arguments"

41
compiler/driver.ml
View File

@ -139,8 +139,9 @@ let driver source_file (options : Cli.options) : int =
Literate.Html.wrap_html prgm.Surface.Ast.program_source_files
language fmt (fun fmt -> weave_output fmt prgm)
else weave_output fmt prgm)
| ( `Interpret | `Typecheck | `OCaml | `Python | `Scalc | `Lcalc | `Dcalc
| `Scopelang | `Proof | `DcalcInvariants | `Plugin _ ) as backend -> (
| ( `Interpret | `Interpret_Lcalc | `Typecheck | `OCaml | `Python | `Scalc
| `Lcalc | `Dcalc | `Scopelang | `Proof | `DcalcInvariants | `Plugin _ )
as backend -> (
Cli.debug_print "Name resolution...";
let ctxt = Desugared.Name_resolution.form_context prgm in
let scope_uid =
@ -189,8 +190,9 @@ let driver source_file (options : Cli.options) : int =
Format.fprintf fmt "%a\n"
(Scopelang.Print.program ~debug:options.debug)
prgm
| ( `Interpret | `Typecheck | `OCaml | `Python | `Scalc | `Lcalc | `Dcalc
| `Proof | `DcalcInvariants | `Plugin _ ) as backend -> (
| ( `Interpret | `Interpret_Lcalc | `Typecheck | `OCaml | `Python | `Scalc
| `Lcalc | `Dcalc | `Proof | `DcalcInvariants | `Plugin _ ) as backend
-> (
Cli.debug_print "Typechecking...";
let type_ordering =
Scopelang.Dependency.check_type_cycles prgm.program_ctx.ctx_structs
@ -247,8 +249,8 @@ let driver source_file (options : Cli.options) : int =
Format.fprintf fmt "%a\n"
(Shared_ast.Expr.format ~debug:options.debug prgm.decl_ctx)
prgrm_dcalc_expr
| ( `Interpret | `OCaml | `Python | `Scalc | `Lcalc | `Proof
| `DcalcInvariants | `Plugin _ ) as backend -> (
| ( `Interpret | `OCaml | `Python | `Scalc | `Lcalc | `Proof | `Plugin _
| `Interpret_Lcalc | `DcalcInvariants ) as backend -> (
Cli.debug_print "Typechecking again...";
let prgm =
try Shared_ast.Typing.program ~leave_unresolved:false prgm
@ -288,11 +290,8 @@ let driver source_file (options : Cli.options) : int =
else raise (Errors.raise_error "Invariant invalid")
| `Interpret ->
Cli.debug_print "Starting interpretation...";
let prgrm_dcalc_expr =
Shared_ast.Expr.unbox (Shared_ast.Program.to_expr prgm scope_uid)
in
let results =
Dcalc.Interpreter.interpret_program prgm.decl_ctx prgrm_dcalc_expr
Shared_ast.Interpreter.interpret_program_dcalc prgm scope_uid
in
let results =
List.sort
@ -308,7 +307,8 @@ let driver source_file (options : Cli.options) : int =
(Shared_ast.Expr.format ~debug:options.debug prgm.decl_ctx)
result)
results
| (`OCaml | `Python | `Lcalc | `Scalc | `Plugin _) as backend -> (
| (`OCaml | `Interpret_Lcalc | `Python | `Lcalc | `Scalc | `Plugin _)
as backend -> (
Cli.debug_print "Compiling program into lambda calculus...";
let prgm =
if options.avoid_exceptions then
@ -363,6 +363,25 @@ let driver source_file (options : Cli.options) : int =
Format.fprintf fmt "%a\n"
(Shared_ast.Print.program ~debug:options.debug)
prgm
| `Interpret_Lcalc ->
Cli.debug_print "Starting interpretation...";
let results =
Shared_ast.Interpreter.interpret_program_lcalc prgm scope_uid
in
let results =
List.sort
(fun ((v1, _), _) ((v2, _), _) -> String.compare v1 v2)
results
in
Cli.debug_print "End of interpretation";
Cli.result_print "Computation successful!%s"
(if List.length results > 0 then " Results:" else "");
List.iter
(fun ((var, _), result) ->
Cli.result_format "@[<hov 2>%s@ =@ %a@]" var
(Shared_ast.Expr.format ~debug:options.debug prgm.decl_ctx)
result)
results
| (`OCaml | `Python | `Scalc | `Plugin _) as backend -> (
match backend with
| `OCaml ->

2
compiler/lcalc/closure_conversion.ml
View File

@ -86,6 +86,7 @@ let rec hoist_context_free_closures :
[{ name = closure_var; closure = e }], Expr.make_var closure_var m
| EApp _ ->
Expr.map_gather ~acc:[] ~join:( @ ) ~f:(hoist_context_free_closures ctx) e
| _ -> .
[@@warning "-32"]
(** Returns the expression with closed closures and the set of free variables
@ -237,6 +238,7 @@ let rec transform_closures_expr :
Expr.make_let_in code_env_var
(TAny, Expr.pos e)
new_e1 call_expr (Expr.pos e) )
| _ -> .
(* Here I have to reimplement Scope.map_exprs_in_lets because I'm changing the
type *)

12
compiler/lcalc/compile_with_exceptions.ml
View File

@ -73,12 +73,12 @@ and translate_expr (ctx : 'm ctx) (e : 'm D.expr) : 'm A.expr boxed =
(Marked.get_mark e)
| EDefault { excepts; just; cons } ->
translate_default ctx excepts just cons (Marked.get_mark e)
| ( ELit _ | EApp _ | EOp _ | EArray _ | EVar _ | EAbs _ | EIfThenElse _
| ETuple _ | ETupleAccess _ | EInj _ | EAssert _ | EStruct _
| EStructAccess _ | EMatch _ ) as e ->
Expr.map_raw ~fop:Operator.translate
~floc:(function _ -> .)
~f:(translate_expr ctx) (Marked.mark m e)
| EOp { op; tys } -> Expr.eop (Operator.translate op) tys m
| ( ELit _ | EApp _ | EArray _ | EVar _ | EAbs _ | EIfThenElse _ | ETuple _
| ETupleAccess _ | EInj _ | EAssert _ | EStruct _ | EStructAccess _
| EMatch _ ) as e ->
Expr.map ~f:(translate_expr ctx) (Marked.mark m e)
| _ -> .
let rec translate_scope_lets
(decl_ctx : decl_ctx)

1
compiler/lcalc/to_ocaml.ml
View File

@ -388,6 +388,7 @@ let rec format_expr (ctx : decl_ctx) (fmt : Format.formatter) (e : 'm expr) :
format_with_parens body format_exception
(exn, Expr.pos e)
format_with_parens handler
| _ -> .
let format_struct_embedding
(fmt : Format.formatter)

8
compiler/shared_ast/definitions.ml
View File

@ -320,7 +320,11 @@ and ('a, 'b, 't) base_gexpr =
args : ('a, 't) gexpr list;
}
-> ('a, [< all ], 't) base_gexpr
| EOp : { op : 'a operator; tys : typ list } -> ('a, [< all ], 't) base_gexpr
| EOp : {
op : 'b operator;
tys : typ list;
}
-> ('a, ([< all ] as 'b), 't) base_gexpr
| EArray : ('a, 't) gexpr list -> ('a, [< all ], 't) base_gexpr
| EVar : ('a, 't) naked_gexpr Bindlib.var -> ('a, _, 't) base_gexpr
| EAbs : {
@ -359,7 +363,7 @@ and ('a, 'b, 't) base_gexpr =
}
-> ('a, [< all ], 't) base_gexpr
(* Early stages *)
| ELocation : 'a glocation -> ('a, [< all > `ExplicitScopes ], 't) base_gexpr
| ELocation : 'b glocation -> ('a, ([< all ] as 'b), 't) base_gexpr
| EScopeCall : {
scope : ScopeName.t;
args : ('a, 't) gexpr ScopeVar.Map.t;

14
compiler/shared_ast/expr.ml
View File

@ -209,17 +209,15 @@ let maybe_ty (type m) ?(typ = TAny) (m : m mark) : typ =
(* - Traversal functions - *)
(* shallow map *)
let map_raw
let map
(type a b)
~(f : (a, 'm1) gexpr -> (b, 'm2) boxed_gexpr)
~(fop : a Op.t -> b Op.t)
~(floc : a glocation -> b glocation)
(e : ((a, b, 'm1) base_gexpr, 'm2) Marked.t) : (b, 'm2) boxed_gexpr =
let m = Marked.get_mark e in
match Marked.unmark e with
| ELit l -> elit l m
| EApp { f = e1; args } -> eapp (f e1) (List.map f args) m
| EOp { op; tys } -> eop (fop op) tys m
| EOp { op; tys } -> eop op tys m
| EArray args -> earray (List.map f args) m
| EVar v -> evar (Var.translate v) m
| EAbs { binder; tys } ->
@ -239,7 +237,7 @@ let map_raw
| EErrorOnEmpty e1 -> eerroronempty (f e1) m
| ECatch { body; exn; handler } -> ecatch (f body) exn (f handler) m
| ERaise exn -> eraise exn m
| ELocation loc -> elocation (floc loc) m
| ELocation loc -> elocation loc m
| EStruct { name; fields } ->
let fields = StructField.Map.map f fields in
estruct name fields m
@ -253,7 +251,6 @@ let map_raw
let fields = ScopeVar.Map.map f args in
escopecall scope fields m
let map = map_raw ~fop:(fun op -> op) ~floc:(fun loc -> loc)
let rec map_top_down ~f e = map ~f:(map_top_down ~f) (f e)
let map_marks ~f e =
@ -670,6 +667,11 @@ let rec free_vars : ('a, 't) gexpr -> ('a, 't) gexpr Var.Set.t = function
Array.fold_right Var.Set.remove vs (free_vars body)
| e -> shallow_fold (fun e -> Var.Set.union (free_vars e)) e Var.Set.empty
let rec skip_wrappers : type a. (a, 'm) gexpr -> (a, 'm) gexpr = function
| EApp { f = EOp { op = Log _; _ }, _; args = [e] }, _ -> skip_wrappers e
| EErrorOnEmpty e, _ -> skip_wrappers e
| e -> e
let remove_logging_calls e =
let rec f e =
match Marked.unmark e with

45
compiler/shared_ast/expr.mli
View File

@ -97,9 +97,7 @@ val ecatch :
(([< all > `Exceptions ] as 'a), 't) boxed_gexpr
val eraise : except -> 't -> ([< all > `Exceptions ], 't) boxed_gexpr
val elocation :
'a glocation -> 't -> (([< all > `ExplicitScopes ] as 'a), 't) boxed_gexpr
val elocation : 'a glocation -> 't -> (([< all ] as 'a), 't) boxed_gexpr
val estruct :
StructName.t ->
@ -181,15 +179,14 @@ val untype : ('a, 'm mark) gexpr -> ('a, untyped mark) boxed_gexpr
(** {2 Traversal functions} *)
val map :
f:(('a, 't1) gexpr -> ('a, 't2) boxed_gexpr) ->
(('a, 't1) naked_gexpr, 't2) Marked.t ->
('a, 't2) boxed_gexpr
f:(('a, 'm1) gexpr -> ('b, 'm2) boxed_gexpr) ->
(('a, 'b, 'm1) base_gexpr, 'm2) Marked.t ->
('b, 'm2) boxed_gexpr
(** Shallow mapping on expressions (non recursive): applies the given function
to all sub-terms of the given expression, and rebuilds the node.
When applying a map transform to an expression, this avoids expliciting all
cases that remain unchanged. For instance, if you want to remove all errors
on empty, you can write
This function makes it very concise to transform only certain nodes of the
AST. For instance, if you want to remove all errors on empty, you can write
{[
let remove_error_empty e =
@ -199,30 +196,21 @@ val map :
| _ -> Expr.map ~f e
in
f e
]} *)
]}
val map_raw :
f:(('a, 'm1) gexpr -> ('b, 'm2) boxed_gexpr) ->
fop:('a Op.t -> 'b Op.t) ->
floc:('a glocation -> 'b glocation) ->
(('a, 'b, 'm1) base_gexpr, 'm2) Marked.t ->
('b, 'm2) boxed_gexpr
(** Lower-level version of shallow [map] that can be used for transforming the
type of the AST. See [Lcalc.Compile_without_exceptions] for an example. The
structure is like this:
This can even be used to translate between different kinds of ASTs: see
[Lcalc.Compile_without_exceptions] for an example. The structure is like
this:
{[
let rec translate = function
| SpecificCase e -> TargetCase (translate e)
| (All | Other | Common | Cases) as e -> map_raw ~f:translate e
| (All | Other | Common | Cases) as e -> Expr.map ~f:translate e
]}
This function makes it very concise to transform only certain nodes of the
AST.
The [e] parameter passed to [map_raw] here needs to have only the common
cases in its shallow type, but can still contain any node from the starting
AST deeper inside: this is where the second type parameter to [base_gexpr]
The [e] parameter passed to [map] here needs to have only the common cases
in its shallow type, but can still contain any node from the starting AST
deeper inside: this is where the second type parameter to [base_gexpr]
becomes useful. *)
val map_top_down :
@ -338,6 +326,9 @@ val make_tuple :
(** {2 Transformations} *)
val skip_wrappers : ('a, 'm) gexpr -> ('a, 'm) gexpr
(** Removes surface logging calls and [EErrorOnEmpty] nodes. Shallow function *)
val remove_logging_calls :
(([< all > `Polymorphic ] as 'a), 't) gexpr -> ('a, 't) boxed_gexpr
(** Removes all calls to [Log] unary operators in the AST, replacing them by
@ -356,6 +347,8 @@ val equal_lit : lit -> lit -> bool
val compare_lit : lit -> lit -> int
val equal_location : 'a glocation Marked.pos -> 'a glocation Marked.pos -> bool
val compare_location : 'a glocation Marked.pos -> 'a glocation Marked.pos -> int
val equal_except : except -> except -> bool
val compare_except : except -> except -> int
val equal : ('a, 't) gexpr -> ('a, 't) gexpr -> bool
(** Determines if two expressions are equal, omitting their position information *)

654
compiler/shared_ast/interpreter.ml Normal file
View File

@ -0,0 +1,654 @@
(* 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>, Emile Rolley
<emile.rolley@tuta.io>, Alain Delaët <alain.delaet--tixeuil@inria.Fr>, Louis
Gesbert <louis.gesbert@inria.fr>
Licensed under the Apache License, Version 2.0 (the "License"); you may not
use this file except in compliance with the License. You may obtain a copy of
the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
License for the specific language governing permissions and limitations under
the License. *)
(** Reference interpreter for the default calculus *)
open Catala_utils
open Definitions
open Op
module Runtime = Runtime_ocaml.Runtime
(** {1 Helpers} *)
let is_empty_error : type a. (a, 'm) gexpr -> bool =
fun e -> match Marked.unmark e with EEmptyError -> true | _ -> false
(** [e' = propagate_empty_error e f] return [EEmptyError] if [e] is
[EEmptyError], else it apply [f] on not-empty term [e]. *)
let propagate_empty_error :
type a. (a, 'm) gexpr -> ((a, 'm) gexpr -> (a, 'm) gexpr) -> (a, 'm) gexpr =
fun e f -> match e with (EEmptyError, _) as e -> e | e -> f e
(** [e' = propagate_empty_error_list elist f] return [EEmptyError] if one lement
of [es] is [EEmptyError], else it apply [f] on not-empty term list [elist]. *)
let propagate_empty_error_list elist f =
let rec aux acc = function
| [] -> f (List.rev acc)
| e :: r -> propagate_empty_error e (fun e -> aux (e :: acc) r)
in
aux [] elist
let log_indent = ref 0
(* TODO: we should provide a generic way to print logs, that work across the
different backends: python, ocaml, javascript, and interpreter *)
(** {1 Evaluation} *)
let print_log ctx entry infos pos e =
if !Cli.trace_flag then
match entry with
| VarDef _ ->
(* TODO: this usage of Format is broken, Formatting requires that all is
formatted in one pass, without going through intermediate "%s" *)
Cli.log_format "%*s%a %a: %s" (!log_indent * 2) "" Print.log_entry entry
Print.uid_list infos
(match Marked.unmark e with
| EAbs _ -> Cli.with_style [ANSITerminal.green] "<function>"
| _ ->
let expr_str =
Format.asprintf "%a" (Expr.format ctx ~debug:false) e
in
let expr_str =
Re.Pcre.substitute ~rex:(Re.Pcre.regexp "\n\\s*")
~subst:(fun _ -> " ")
expr_str
in
Cli.with_style [ANSITerminal.green] "%s" expr_str)
| PosRecordIfTrueBool -> (
match pos <> Pos.no_pos, Marked.unmark e with
| true, ELit (LBool true) ->
Cli.log_format "%*s%a%s:\n%s" (!log_indent * 2) "" Print.log_entry entry
(Cli.with_style [ANSITerminal.green] "Definition applied")
(Cli.add_prefix_to_each_line (Pos.retrieve_loc_text pos) (fun _ ->
Format.asprintf "%*s" (!log_indent * 2) ""))
| _ -> ())
| BeginCall ->
Cli.log_format "%*s%a %a" (!log_indent * 2) "" Print.log_entry entry
Print.uid_list infos;
log_indent := !log_indent + 1
| EndCall ->
log_indent := !log_indent - 1;
Cli.log_format "%*s%a %a" (!log_indent * 2) "" Print.log_entry entry
Print.uid_list infos
exception CatalaException of except
(* Todo: this should be handled early when resolving overloads. Here we have
proper structural equality, but the OCaml backend for example uses the
builtin equality function instead of this. *)
let handle_eq evaluate_operator ctx pos e1 e2 =
let open Runtime.Oper in
match e1, e2 with
| ELit LUnit, ELit LUnit -> true
| ELit (LBool b1), ELit (LBool b2) -> not (o_xor b1 b2)
| ELit (LInt x1), ELit (LInt x2) -> o_eq_int_int x1 x2
| ELit (LRat x1), ELit (LRat x2) -> o_eq_rat_rat x1 x2
| ELit (LMoney x1), ELit (LMoney x2) -> o_eq_mon_mon x1 x2
| ELit (LDuration x1), ELit (LDuration x2) -> o_eq_dur_dur x1 x2
| ELit (LDate x1), ELit (LDate x2) -> o_eq_dat_dat x1 x2
| EArray es1, EArray es2 -> (
try
List.for_all2
(fun e1 e2 ->
match Marked.unmark (evaluate_operator ctx Eq pos [e1; e2]) with
| ELit (LBool b) -> b
| _ -> assert false
(* should not happen *))
es1 es2
with Invalid_argument _ -> false)
| EStruct { fields = es1; name = s1 }, EStruct { fields = es2; name = s2 } ->
StructName.equal s1 s2
&& StructField.Map.equal
(fun e1 e2 ->
match Marked.unmark (evaluate_operator ctx Eq pos [e1; e2]) with
| ELit (LBool b) -> b
| _ -> assert false
(* should not happen *))
es1 es2
| ( EInj { e = e1; cons = i1; name = en1 },
EInj { e = e2; cons = i2; name = en2 } ) -> (
try
EnumName.equal en1 en2
&& EnumConstructor.equal i1 i2
&&
match Marked.unmark (evaluate_operator ctx Eq pos [e1; e2]) with
| ELit (LBool b) -> b
| _ -> assert false
(* should not happen *)
with Invalid_argument _ -> false)
| _, _ -> false (* comparing anything else return false *)
(* Call-by-value: the arguments are expected to be already evaluated here *)
let rec evaluate_operator
evaluate_expr
ctx
(op : [< dcalc | lcalc ] operator)
m
args =
let pos = Expr.mark_pos m in
let protect f x y =
let get_binop_args_pos = function
| (arg0 :: arg1 :: _ : ('t, 'm) gexpr list) ->
[None, Expr.pos arg0; None, Expr.pos arg1]
| _ -> assert false
in
try f x y with
| Division_by_zero ->
Errors.raise_multispanned_error
[
Some "The division operator:", pos;
Some "The null denominator:", Expr.pos (List.nth args 1);
]
"division by zero at runtime"
| Runtime.UncomparableDurations ->
Errors.raise_multispanned_error (get_binop_args_pos args)
"Cannot compare together durations that cannot be converted to a \
precise number of days"
in
let err () =
Errors.raise_multispanned_error
([Some "Operator:", pos]
@ List.mapi
(fun i arg ->
( Some
(Format.asprintf "Argument n°%d, value %a" (i + 1)
(Expr.format ctx ~debug:true)
arg),
Expr.pos arg ))
args)
"Operator applied to the wrong arguments\n\
(should not happen if the term was well-typed)"
in
propagate_empty_error_list args
@@ fun args ->
let open Runtime.Oper in
Marked.mark m
@@
match op, args with
| Length, [(EArray es, _)] ->
ELit (LInt (Runtime.integer_of_int (List.length es)))
| Log (entry, infos), [e'] ->
print_log ctx entry infos pos e';
Marked.unmark e'
| Eq, [(e1, _); (e2, _)] ->
ELit (LBool (handle_eq (evaluate_operator evaluate_expr) ctx m e1 e2))
| Map, [f; (EArray es, _)] ->
EArray
(List.map
(fun e' ->
evaluate_expr ctx (Marked.same_mark_as (EApp { f; args = [e'] }) e'))
es)
| Reduce, [_; default; (EArray [], _)] -> Marked.unmark default
| Reduce, [f; _; (EArray (x0 :: xn), _)] ->
Marked.unmark
(List.fold_left
(fun acc x ->
evaluate_expr ctx
(Marked.same_mark_as (EApp { f; args = [acc; x] }) f))
x0 xn)
| Concat, [(EArray es1, _); (EArray es2, _)] -> EArray (es1 @ es2)
| Filter, [f; (EArray es, _)] ->
EArray
(List.filter
(fun e' ->
match
evaluate_expr ctx
(Marked.same_mark_as (EApp { f; args = [e'] }) e')
with
| ELit (LBool b), _ -> b
| _ ->
Errors.raise_spanned_error
(Expr.pos (List.nth args 0))
"This predicate evaluated to something else than a boolean \
(should not happen if the term was well-typed)")
es)
| Fold, [f; init; (EArray es, _)] ->
Marked.unmark
(List.fold_left
(fun acc e' ->
evaluate_expr ctx
(Marked.same_mark_as (EApp { f; args = [acc; e'] }) e'))
init es)
| (Length | Log _ | Eq | Map | Concat | Filter | Fold | Reduce), _ -> err ()
| Not, [(ELit (LBool b), _)] -> ELit (LBool (o_not b))
| GetDay, [(ELit (LDate d), _)] -> ELit (LInt (o_getDay d))
| GetMonth, [(ELit (LDate d), _)] -> ELit (LInt (o_getMonth d))
| GetYear, [(ELit (LDate d), _)] -> ELit (LInt (o_getYear d))
| FirstDayOfMonth, [(ELit (LDate d), _)] -> ELit (LDate (o_firstDayOfMonth d))
| LastDayOfMonth, [(ELit (LDate d), _)] -> ELit (LDate (o_lastDayOfMonth d))
| And, [(ELit (LBool b1), _); (ELit (LBool b2), _)] ->
ELit (LBool (o_and b1 b2))
| Or, [(ELit (LBool b1), _); (ELit (LBool b2), _)] ->
ELit (LBool (o_or b1 b2))
| Xor, [(ELit (LBool b1), _); (ELit (LBool b2), _)] ->
ELit (LBool (o_xor b1 b2))
| ( ( Not | GetDay | GetMonth | GetYear | FirstDayOfMonth | LastDayOfMonth
| And | Or | Xor ),
_ ) ->
err ()
| Minus_int, [(ELit (LInt x), _)] -> ELit (LInt (o_minus_int x))
| Minus_rat, [(ELit (LRat x), _)] -> ELit (LRat (o_minus_rat x))
| Minus_mon, [(ELit (LMoney x), _)] -> ELit (LMoney (o_minus_mon x))
| Minus_dur, [(ELit (LDuration x), _)] -> ELit (LDuration (o_minus_dur x))
| ToRat_int, [(ELit (LInt i), _)] -> ELit (LRat (o_torat_int i))
| ToRat_mon, [(ELit (LMoney i), _)] -> ELit (LRat (o_torat_mon i))
| ToMoney_rat, [(ELit (LRat i), _)] -> ELit (LMoney (o_tomoney_rat i))
| Round_mon, [(ELit (LMoney m), _)] -> ELit (LMoney (o_round_mon m))
| Round_rat, [(ELit (LRat m), _)] -> ELit (LRat (o_round_rat m))
| Add_int_int, [(ELit (LInt x), _); (ELit (LInt y), _)] ->
ELit (LInt (o_add_int_int x y))
| Add_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LRat (o_add_rat_rat x y))
| Add_mon_mon, [(ELit (LMoney x), _); (ELit (LMoney y), _)] ->
ELit (LMoney (o_add_mon_mon x y))
| Add_dat_dur r, [(ELit (LDate x), _); (ELit (LDuration y), _)] ->
ELit (LDate (o_add_dat_dur r x y))
| Add_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LDuration (o_add_dur_dur x y))
| Sub_int_int, [(ELit (LInt x), _); (ELit (LInt y), _)] ->
ELit (LInt (o_sub_int_int x y))
| Sub_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LRat (o_sub_rat_rat x y))
| Sub_mon_mon, [(ELit (LMoney x), _); (ELit (LMoney y), _)] ->
ELit (LMoney (o_sub_mon_mon x y))
| Sub_dat_dat, [(ELit (LDate x), _); (ELit (LDate y), _)] ->
ELit (LDuration (o_sub_dat_dat x y))
| Sub_dat_dur, [(ELit (LDate x), _); (ELit (LDuration y), _)] ->
ELit (LDate (o_sub_dat_dur x y))
| Sub_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LDuration (o_sub_dur_dur x y))
| Mult_int_int, [(ELit (LInt x), _); (ELit (LInt y), _)] ->
ELit (LInt (o_mult_int_int x y))
| Mult_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LRat (o_mult_rat_rat x y))
| Mult_mon_rat, [(ELit (LMoney x), _); (ELit (LRat y), _)] ->
ELit (LMoney (o_mult_mon_rat x y))
| Mult_dur_int, [(ELit (LDuration x), _); (ELit (LInt y), _)] ->
ELit (LDuration (o_mult_dur_int x y))
| Div_int_int, [(ELit (LInt x), _); (ELit (LInt y), _)] ->
ELit (LRat (protect o_div_int_int x y))
| Div_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LRat (protect o_div_rat_rat x y))
| Div_mon_mon, [(ELit (LMoney x), _); (ELit (LMoney y), _)] ->
ELit (LRat (protect o_div_mon_mon x y))
| Div_mon_rat, [(ELit (LMoney x), _); (ELit (LRat y), _)] ->
ELit (LMoney (protect o_div_mon_rat x y))
| Div_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LRat (protect o_div_dur_dur x y))
| Lt_int_int, [(ELit (LInt x), _); (ELit (LInt y), _)] ->
ELit (LBool (o_lt_int_int x y))
| Lt_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LBool (o_lt_rat_rat x y))
| Lt_mon_mon, [(ELit (LMoney x), _); (ELit (LMoney y), _)] ->
ELit (LBool (o_lt_mon_mon x y))
| Lt_dat_dat, [(ELit (LDate x), _); (ELit (LDate y), _)] ->
ELit (LBool (o_lt_dat_dat x y))
| Lt_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LBool (protect o_lt_dur_dur x y))
| Lte_int_int, [(ELit (LInt x), _); (ELit (LInt y), _)] ->
ELit (LBool (o_lte_int_int x y))
| Lte_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LBool (o_lte_rat_rat x y))
| Lte_mon_mon, [(ELit (LMoney x), _); (ELit (LMoney y), _)] ->
ELit (LBool (o_lte_mon_mon x y))
| Lte_dat_dat, [(ELit (LDate x), _); (ELit (LDate y), _)] ->
ELit (LBool (o_lte_dat_dat x y))
| Lte_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LBool (protect o_lte_dur_dur x y))
| Gt_int_int, [(ELit (LInt x), _); (ELit (LInt y), _)] ->
ELit (LBool (o_gt_int_int x y))
| Gt_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LBool (o_gt_rat_rat x y))
| Gt_mon_mon, [(ELit (LMoney x), _); (ELit (LMoney y), _)] ->
ELit (LBool (o_gt_mon_mon x y))
| Gt_dat_dat, [(ELit (LDate x), _); (ELit (LDate y), _)] ->
ELit (LBool (o_gt_dat_dat x y))
| Gt_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LBool (protect o_gt_dur_dur x y))
| Gte_int_int, [(ELit (LInt x), _); (ELit (LInt y), _)] ->
ELit (LBool (o_gte_int_int x y))
| Gte_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LBool (o_gte_rat_rat x y))
| Gte_mon_mon, [(ELit (LMoney x), _); (ELit (LMoney y), _)] ->
ELit (LBool (o_gte_mon_mon x y))
| Gte_dat_dat, [(ELit (LDate x), _); (ELit (LDate y), _)] ->
ELit (LBool (o_gte_dat_dat x y))
| Gte_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LBool (protect o_gte_dur_dur x y))
| Eq_int_int, [(ELit (LInt x), _); (ELit (LInt y), _)] ->
ELit (LBool (o_eq_int_int x y))
| Eq_rat_rat, [(ELit (LRat x), _); (ELit (LRat y), _)] ->
ELit (LBool (o_eq_rat_rat x y))
| Eq_mon_mon, [(ELit (LMoney x), _); (ELit (LMoney y), _)] ->
ELit (LBool (o_eq_mon_mon x y))
| Eq_dat_dat, [(ELit (LDate x), _); (ELit (LDate y), _)] ->
ELit (LBool (o_eq_dat_dat x y))
| Eq_dur_dur, [(ELit (LDuration x), _); (ELit (LDuration y), _)] ->
ELit (LBool (protect o_eq_dur_dur x y))
| ( ( Minus_int | Minus_rat | Minus_mon | Minus_dur | ToRat_int | ToRat_mon
| ToMoney_rat | Round_rat | Round_mon | Add_int_int | Add_rat_rat
| Add_mon_mon | Add_dat_dur _ | Add_dur_dur | Sub_int_int | Sub_rat_rat
| Sub_mon_mon | Sub_dat_dat | Sub_dat_dur | Sub_dur_dur | Mult_int_int
| Mult_rat_rat | Mult_mon_rat | Mult_dur_int | Div_int_int | Div_rat_rat
| Div_mon_mon | Div_mon_rat | Div_dur_dur | Lt_int_int | Lt_rat_rat
| Lt_mon_mon | Lt_dat_dat | Lt_dur_dur | Lte_int_int | Lte_rat_rat
| Lte_mon_mon | Lte_dat_dat | Lte_dur_dur | Gt_int_int | Gt_rat_rat
| Gt_mon_mon | Gt_dat_dat | Gt_dur_dur | Gte_int_int | Gte_rat_rat
| Gte_mon_mon | Gte_dat_dat | Gte_dur_dur | Eq_int_int | Eq_rat_rat
| Eq_mon_mon | Eq_dat_dat | Eq_dur_dur ),
_ ) ->
err ()
(* typed with ['a] for simplicity, but only actually implemented on dcalc and
lcalc at the moment *)
let rec evaluate_expr :
type a. decl_ctx -> (a, 'm mark) gexpr -> (a, 'm mark) gexpr =
fun ctx e ->
let m = Marked.get_mark e in
let pos = Expr.mark_pos m in
match Marked.unmark e with
| ELocation _ | EScopeCall _ | EDStructAccess _ ->
(* These cases don't belong to dcalc or lcalc *)
assert false
| ERaise exn -> raise (CatalaException exn)
| ECatch { body; exn; handler } -> (
try evaluate_expr ctx body
with CatalaException caught when Expr.equal_except caught exn ->
evaluate_expr ctx handler)
| EVar _ ->
Errors.raise_spanned_error pos
"free variable found at evaluation (should not happen if term was \
well-typed)"
| EApp { f = e1; args } -> (
let e1 = evaluate_expr ctx e1 in
let args = List.map (evaluate_expr ctx) args in
propagate_empty_error e1
@@ fun e1 ->
match Marked.unmark e1 with
| EAbs { binder; _ } ->
if Bindlib.mbinder_arity binder = List.length args then
evaluate_expr ctx
(Bindlib.msubst binder (Array.of_list (List.map Marked.unmark args)))
else
Errors.raise_spanned_error pos
"wrong function call, expected %d arguments, got %d"
(Bindlib.mbinder_arity binder)
(List.length args)
| EOp
{
op =
( Not | GetDay | GetMonth | GetYear | FirstDayOfMonth
| LastDayOfMonth | And | Or | Xor | Log _ | Length | Eq | Map
| Concat | Filter | Reduce | Fold | Minus_int | Minus_rat
| Minus_mon | Minus_dur | ToRat_int | ToRat_mon | ToMoney_rat
| Round_rat | Round_mon | Add_int_int | Add_rat_rat | Add_mon_mon
| Add_dat_dur _ | Add_dur_dur | Sub_int_int | Sub_rat_rat
| Sub_mon_mon | Sub_dat_dat | Sub_dat_dur | Sub_dur_dur
| Mult_int_int | Mult_rat_rat | Mult_mon_rat | Mult_dur_int
| Div_int_int | Div_rat_rat | Div_mon_mon | Div_mon_rat
| Div_dur_dur | Lt_int_int | Lt_rat_rat | Lt_mon_mon | Lt_dat_dat
| Lt_dur_dur | Lte_int_int | Lte_rat_rat | Lte_mon_mon | Lte_dat_dat
| Lte_dur_dur | Gt_int_int | Gt_rat_rat | Gt_mon_mon | Gt_dat_dat
| Gt_dur_dur | Gte_int_int | Gte_rat_rat | Gte_mon_mon | Gte_dat_dat
| Gte_dur_dur | Eq_int_int | Eq_rat_rat | Eq_mon_mon | Eq_dat_dat
| Eq_dur_dur ) as op;
_;
} ->
evaluate_operator evaluate_expr ctx op m args
| _ ->
Errors.raise_spanned_error pos
"function has not been reduced to a lambda at evaluation (should not \
happen if the term was well-typed")
| EAbs _ | ELit _ | EOp _ -> e (* these are values *)
| EStruct { fields = es; name } ->
let fields, es = List.split (StructField.Map.bindings es) in
let es = List.map (evaluate_expr ctx) es in
propagate_empty_error_list es
@@ fun es ->
Marked.mark m
(EStruct
{
fields =
StructField.Map.of_seq
(Seq.zip (List.to_seq fields) (List.to_seq es));
name;
})
| EStructAccess { e; name = s; field } -> (
propagate_empty_error (evaluate_expr ctx e)
@@ fun e ->
match Marked.unmark e with
| EStruct { fields = es; name } -> (
if not (StructName.equal s name) then
Errors.raise_multispanned_error
[None, pos; None, Expr.pos e]
"Error during struct access: not the same structs (should not happen \
if the term was well-typed)";
match StructField.Map.find_opt field es with
| Some e' -> e'
| None ->
Errors.raise_spanned_error (Expr.pos e)
"Invalid field access %a in struct %a (should not happen if the term \
was well-typed)"
StructField.format_t field StructName.format_t s)
| _ ->
Errors.raise_spanned_error (Expr.pos e)
"The expression %a should be a struct %a but is not (should not happen \
if the term was well-typed)"
(Expr.format ctx ~debug:true)
e StructName.format_t s)
| ETuple es -> Marked.mark m (ETuple (List.map (evaluate_expr ctx) es))
| ETupleAccess { e = e1; index; size } -> (
match evaluate_expr ctx e1 with
| ETuple es, _ when List.length es = size -> List.nth es index
| e ->
Errors.raise_spanned_error (Expr.pos e)
"The expression %a was expected to be a tuple of size %d (should not \
happen if the term was well-typed)"
(Expr.format ctx ~debug:true)
e size)
| EInj { e; name; cons } ->
propagate_empty_error (evaluate_expr ctx e)
@@ fun e -> Marked.mark m (EInj { e; name; cons })
| EMatch { e; cases; name } -> (
propagate_empty_error (evaluate_expr ctx e)
@@ fun e ->
match Marked.unmark e with
| EInj { e = e1; cons; name = name' } ->
if not (EnumName.equal name name') then
Errors.raise_multispanned_error
[None, Expr.pos e; None, Expr.pos e1]
"Error during match: two different enums found (should not happen if \
the term was well-typed)";
let es_n =
match EnumConstructor.Map.find_opt cons cases with
| Some es_n -> es_n
| None ->
Errors.raise_spanned_error (Expr.pos e)
"sum type index error (should not happen if the term was \
well-typed)"
in
let new_e = Marked.mark m (EApp { f = es_n; args = [e1] }) in
evaluate_expr ctx new_e
| _ ->
Errors.raise_spanned_error (Expr.pos e)
"Expected a term having a sum type as an argument to a match (should \
not happen if the term was well-typed")
| EDefault { excepts; just; cons } -> (
let excepts = List.map (evaluate_expr ctx) excepts in
let empty_count = List.length (List.filter is_empty_error excepts) in
match List.length excepts - empty_count with
| 0 -> (
let just = evaluate_expr ctx just in
match Marked.unmark just with
| EEmptyError -> Marked.mark m EEmptyError
| ELit (LBool true) -> evaluate_expr ctx cons
| ELit (LBool false) -> Marked.same_mark_as EEmptyError e
| _ ->
Errors.raise_spanned_error (Expr.pos e)
"Default justification has not been reduced to a boolean at \
evaluation (should not happen if the term was well-typed")
| 1 -> List.find (fun sub -> not (is_empty_error sub)) excepts
| _ ->
Errors.raise_multispanned_error
(List.map
(fun except ->
Some "This consequence has a valid justification:", Expr.pos except)
(List.filter (fun sub -> not (is_empty_error sub)) excepts))
"There is a conflict between multiple valid consequences for assigning \
the same variable.")
| EIfThenElse { cond; etrue; efalse } -> (
propagate_empty_error (evaluate_expr ctx cond)
@@ fun cond ->
match Marked.unmark cond with
| ELit (LBool true) -> evaluate_expr ctx etrue
| ELit (LBool false) -> evaluate_expr ctx efalse
| _ ->
Errors.raise_spanned_error (Expr.pos cond)
"Expected a boolean literal for the result of this condition (should \
not happen if the term was well-typed)")
| EArray es ->
propagate_empty_error_list (List.map (evaluate_expr ctx) es)
@@ fun es -> Marked.mark m (EArray es)
| EEmptyError -> Marked.same_mark_as EEmptyError e
| EErrorOnEmpty e' -> (
match evaluate_expr ctx e' with
| EEmptyError, _ ->
Errors.raise_spanned_error (Expr.pos e')
"This variable evaluated to an empty term (no rule that defined it \
applied in this situation)"
| e -> e)
| EAssert e' ->
propagate_empty_error (evaluate_expr ctx e') (fun e ->
match Marked.unmark e with
| ELit (LBool true) -> Marked.mark m (ELit LUnit)
| ELit (LBool false) -> (
match Marked.unmark (Expr.skip_wrappers e') with
| EApp
{
f = EOp { op; _ }, _;
args = [((ELit _, _) as e1); ((ELit _, _) as e2)];
} ->
Errors.raise_spanned_error (Expr.pos e')
"Assertion failed: %a %a %a"
(Expr.format ctx ~debug:false)
e1 Print.operator op
(Expr.format ctx ~debug:false)
e2
| _ ->
Cli.debug_format "%a" (Expr.format ctx) e';
Errors.raise_spanned_error (Expr.mark_pos m) "Assertion failed")
| _ ->
Errors.raise_spanned_error (Expr.pos e')
"Expected a boolean literal for the result of this assertion \
(should not happen if the term was well-typed)")
let interpret_program_lcalc p s : (Uid.MarkedString.info * ('a, 'm) gexpr) list
=
let e = Expr.unbox @@ Program.to_expr p s in
let ctx = p.decl_ctx in
match evaluate_expr ctx e with
| (EAbs { tys = [((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
an empty thunked term. But for [input] arguments of another type, we
cannot provide anything so we have to fail. *)
let taus = StructName.Map.find s_in ctx.ctx_structs in
let application_term =
StructField.Map.map
(fun ty ->
match Marked.unmark ty with
| _ ->
Errors.raise_spanned_error (Marked.get_mark ty)
"This scope needs input arguments to be executed. But the Catala \
built-in interpreter does not have a way to retrieve input \
values from the command line, so it cannot execute this scope. \
Please create another scope thatprovide the input arguments to \
this one and execute it instead. ")
taus
in
let to_interpret =
Expr.make_app (Expr.box e)
[Expr.estruct s_in application_term mark_e]
(Expr.pos e)
in
match Marked.unmark (evaluate_expr ctx (Expr.unbox to_interpret)) with
| EStruct { fields; _ } ->
List.map
(fun (fld, e) -> StructField.get_info fld, e)
(StructField.Map.bindings fields)
| _ ->
Errors.raise_spanned_error (Expr.pos e)
"The interpretation of a program should always yield a struct \
corresponding to the scope variables"
end
| _ ->
Errors.raise_spanned_error (Expr.pos e)
"The interpreter can only interpret terms starting with functions having \
thunked arguments"
(** {1 API} *)
let interpret_program_dcalc p s : (Uid.MarkedString.info * ('a, 'm) gexpr) list
=
let ctx = p.decl_ctx in
let e = Expr.unbox (Program.to_expr p s) in
match evaluate_expr p.decl_ctx e with
| (EAbs { tys = [((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
an empty thunked term. But for [input] arguments of another type, we
cannot provide anything so we have to fail. *)
let taus = StructName.Map.find s_in ctx.ctx_structs in
let application_term =
StructField.Map.map
(fun ty ->
match Marked.unmark ty with
| TArrow (ty_in, ty_out) ->
Expr.make_abs
(Array.of_list @@ List.map (fun _ -> Var.make "_") ty_in)
(Bindlib.box EEmptyError, Expr.with_ty mark_e ty_out)
ty_in (Expr.mark_pos mark_e)
| _ ->
Errors.raise_spanned_error (Marked.get_mark ty)
"This scope needs input arguments to be executed. But the Catala \
built-in interpreter does not have a way to retrieve input \
values from the command line, so it cannot execute this scope. \
Please create another scope thatprovide the input arguments to \
this one and execute it instead. ")
taus
in
let to_interpret =
Expr.make_app (Expr.box e)
[Expr.estruct s_in application_term mark_e]
(Expr.pos e)
in
match Marked.unmark (evaluate_expr ctx (Expr.unbox to_interpret)) with
| EStruct { fields; _ } ->
List.map
(fun (fld, e) -> StructField.get_info fld, e)
(StructField.Map.bindings fields)
| _ ->
Errors.raise_spanned_error (Expr.pos e)
"The interpretation of a program should always yield a struct \
corresponding to the scope variables"
end
| _ ->
Errors.raise_spanned_error (Expr.pos e)
"The interpreter can only interpret terms starting with functions having \
thunked arguments"

23
compiler/dcalc/interpreter.mli → compiler/shared_ast/interpreter.mli
View File

@ -1,6 +1,7 @@
(* 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>
Denis Merigoux <denis.merigoux@inria.fr>, Alain Delaët
<alain.delaet--tixeuil@inria.Fr>, Louis Gesbert <louis.gesbert@inria.fr>
Licensed under the Apache License, Version 2.0 (the "License"); you may not
use this file except in compliance with the License. You may obtain a copy of
@ -17,13 +18,25 @@
(** Reference interpreter for the default calculus *)
open Catala_utils
open Shared_ast
open Definitions
val evaluate_expr : decl_ctx -> 'm Ast.expr -> 'm Ast.expr
val evaluate_expr :
decl_ctx -> (([< dcalc | lcalc ] as 'a), 'm mark) gexpr -> ('a, 'm mark) gexpr
(** Evaluates an expression according to the semantics of the default calculus. *)
val interpret_program :
decl_ctx -> 'm Ast.expr -> (Uid.MarkedString.info * 'm Ast.expr) list
val interpret_program_dcalc :
(dcalc, 'm mark) gexpr program ->
ScopeName.t ->
(Uid.MarkedString.info * (dcalc, 'm mark) gexpr) list
(** Interprets a program. This function expects an expression typed as a
function whose argument are all thunked. The function is executed by
providing for each argument a thunked empty default. Returns a list of all
the computed values for the scope variables of the executed scope. *)
val interpret_program_lcalc :
(lcalc, 'm mark) gexpr program ->
ScopeName.t ->
(Uid.MarkedString.info * (lcalc, 'm mark) gexpr) list
(** Interprets a program. This function expects an expression typed as a
function whose argument are all thunked. The function is executed by
providing for each argument a thunked empty default. Returns a list of all

6
compiler/shared_ast/operator.ml
View File

@ -337,8 +337,10 @@ let kind_dispatch :
| Eq_mon_mon | Eq_dat_dat | Eq_dur_dur ) as op ->
resolved op
let translate
(t : [< scopelang | dcalc | lcalc > `Monomorphic `Polymorphic `Resolved ] t)
type 'a no_overloads =
[< all_ast_features | `Monomorphic | `Polymorphic | `Resolved ] as 'a
let translate (t : [> `Monomorphic | `Polymorphic | `Resolved ] no_overloads t)
=
match t with
| ( Not | GetDay | GetMonth | GetYear | FirstDayOfMonth | LastDayOfMonth | And

5
compiler/shared_ast/operator.mli
View File

@ -50,8 +50,11 @@ val kind_dispatch :
'b
(** Calls one of the supplied functions depending on the kind of the operator *)
type 'a no_overloads =
[< all_ast_features | `Monomorphic | `Polymorphic | `Resolved ] as 'a
val translate :
[< scopelang | dcalc | lcalc > `Monomorphic `Polymorphic `Resolved ] t ->
[> `Monomorphic | `Polymorphic | `Resolved ] no_overloads t ->
[> `Monomorphic | `Polymorphic | `Resolved ] t
(** An identity function that allows translating an operator between different
passes that don't change operator types *)

1
compiler/shared_ast/shared_ast.ml
View File

@ -23,3 +23,4 @@ module Scope = Scope
module Program = Program
module Print = Print
module Typing = Typing
module Interpreter = Interpreter

1
compiler/verification/z3backend.real.ml
View File

@ -786,6 +786,7 @@ and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr =
] )
| EEmptyError -> failwith "[Z3 encoding] LEmptyError literals not supported"
| EErrorOnEmpty _ -> failwith "[Z3 encoding] ErrorOnEmpty unsupported"
| _ -> .
(** [create_z3unit] creates a Z3 sort and expression corresponding to the unit
type and value respectively. Concretely, we represent unit as a tuple with 0