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

Some more fixes and improvements to the printer (#462)

Browse Source
This commit is contained in:
Louis Gesbert 2023-05-03 17:36:57 +02:00 committed by GitHub
commit 2a43929d59
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
42 changed files with 577 additions and 456 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
compiler/dcalc/invariants.ml
View File

@ -39,8 +39,7 @@ let check_invariant (inv : string * invariant_expr) (p : typed program) : bool =
| Fail ->
Cli.error_format "%s failed in %s.\n\n %a" name
(Pos.to_string_short (Expr.pos e))
(Print.expr ~debug:true p.decl_ctx)
e;
(Print.expr ()) e;
incr total;
false
| Pass ->

6
compiler/driver.ml
View File

@ -361,7 +361,7 @@ let driver source_file (options : Cli.options) : int =
Shared_ast.Expr.unbox (Shared_ast.Program.to_expr prgm scope_uid)
in
Format.fprintf fmt "%a\n"
(Shared_ast.Expr.format ~debug:options.debug prgm.decl_ctx)
(Shared_ast.Print.expr ~debug:options.debug ())
prgrm_dcalc_expr
| ( `Interpret | `OCaml | `Python | `Scalc | `Lcalc | `Proof | `Plugin _
| `Interpret_Lcalc ) as backend -> (
@ -408,7 +408,7 @@ let driver source_file (options : Cli.options) : int =
List.iter
(fun ((var, _), result) ->
Cli.result_format "@[<hov 2>%s@ =@ %a@]" var
(Shared_ast.Expr.format ~debug:options.debug prgm.decl_ctx)
(Shared_ast.Print.expr ~debug:options.debug ())
result)
results
| `Plugin (Plugin.Dcalc p) ->
@ -496,7 +496,7 @@ let driver source_file (options : Cli.options) : int =
List.iter
(fun ((var, _), result) ->
Cli.result_format "@[<hov 2>%s@ =@ %a@]" var
(Shared_ast.Expr.format ~debug:options.debug prgm.decl_ctx)
(Shared_ast.Print.expr ~debug:options.debug ())
result)
results
| (`OCaml | `Python | `Scalc | `Plugin _) as backend -> (

5
compiler/lcalc/compile_without_exceptions.ml
View File

@ -103,7 +103,7 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) :
let m = Marked.get_mark e in
let mark = m in
let pos = Expr.pos e in
(* Cli.debug_format "%a" (Print.expr_debug ~debug:true) e; *)
(* Cli.debug_format "%a" (Print.expr ~debug:true ()) e; *)
match Marked.unmark e with
| EVar x ->
if (Var.Map.find x ctx.ctx_vars).info_pure then
@ -342,7 +342,8 @@ let rec trans (ctx : typed ctx) (e : typed D.expr) :
Errors.raise_internal_error
"List operator %a was not fully determined: some partial evaluation was \
found while compiling."
Print.operator op
(Print.operator ~debug:false)
op
| EApp { f = EOp { op; tys }, opmark; args } ->
let res =
Ast.OptionMonad.mmap ~var_name:ctx.ctx_context_name

4
compiler/lcalc/to_ocaml.ml
View File

@ -340,9 +340,9 @@ let rec format_expr (ctx : decl_ctx) (fmt : Format.formatter) (e : 'm expr) :
args;
} ->
Format.fprintf fmt
"@[<hov 2>%a@ @[<hov 2>{filename = \"%s\";@ start_line=%d;@ \
"@[<hov 2>%s@ @[<hov 2>{filename = \"%s\";@ start_line=%d;@ \
start_column=%d;@ end_line=%d; end_column=%d;@ law_headings=%a}@]@ %a@]"
Print.operator op
(Print.operator_to_string op)
(Pos.get_file (Expr.mark_pos pos))
(Pos.get_start_line (Expr.mark_pos pos))
(Pos.get_start_column (Expr.mark_pos pos))

34
compiler/plugins/lazy_interp.ml
View File

@ -84,9 +84,9 @@ let rec lazy_eval :
let r, env1 = lazy_eval ctx env1 llevel e in
if not (Expr.equal e r) then (
log "@[<hv 2>{{%a =@ [%a]@ ==> [%a]}}@]" Print.var_debug v
(Print.expr ~debug:true ctx)
(Print.expr ~debug:true ())
e
(Print.expr ~debug:true ctx)
(Print.expr ~debug:true ())
r;
v_env := r, env1);
r, Env.join env env1
@ -105,12 +105,12 @@ let rec lazy_eval :
Seq.fold_left2
(fun env1 var e ->
log "@[<hov 2>LET %a = %a@]@ " Print.var_debug var
(Print.expr ~debug:true ctx)
(Print.expr ~debug:true ())
e;
Env.add var e env env1)
env (Array.to_seq vars) (List.to_seq args)
in
log "@]@[<hov 4>IN [%a]@]" (Print.expr ~debug:true ctx) body;
log "@]@[<hov 4>IN [%a]@]" (Print.expr ~debug:true ()) body;
let e, env = lazy_eval ctx env llevel body in
log "@]}";
e, env
@ -131,9 +131,9 @@ let rec lazy_eval :
renv := env;
e
in
Interpreter.evaluate_operator eval ctx op m args, !renv
Interpreter.evaluate_operator eval op m args, !renv
(* fixme: this forwards eempty *)
| e, _ -> error e "Invalid apply on %a" (Print.expr ctx) e)
| e, _ -> error e "Invalid apply on %a" Expr.format e)
| (EAbs _ | ELit _ | EOp _ | EEmptyError), _ -> e0, env (* these are values *)
| (EStruct _ | ETuple _ | EInj _ | EArray _), _ ->
if not llevel.eval_struct then e0, env
@ -152,14 +152,14 @@ let rec lazy_eval :
match eval_to_value env e with
| (EStruct { name = n; fields }, _), env when StructName.equal name n ->
lazy_eval ctx env llevel (StructField.Map.find field fields)
| e, _ -> error e "Invalid field access on %a" (Print.expr ctx) e)
| e, _ -> error e "Invalid field access on %a" Expr.format e)
| ETupleAccess { e; index; size }, _ -> (
if not llevel.eval_default then e0, env
else
match eval_to_value env e with
| (ETuple es, _), env when List.length es = size ->
lazy_eval ctx env llevel (List.nth es index)
| e, _ -> error e "Invalid tuple access on %a" (Print.expr ctx) e)
| e, _ -> error e "Invalid tuple access on %a" Expr.format e)
| EMatch { e; name; cases }, _ -> (
if not llevel.eval_default then e0, env
else
@ -167,7 +167,7 @@ let rec lazy_eval :
| (EInj { name = n; cons; e }, m), env when EnumName.equal name n ->
lazy_eval ctx env llevel
(EApp { f = EnumConstructor.Map.find cons cases; args = [e] }, m)
| e, _ -> error e "Invalid match argument %a" (Print.expr ctx) e)
| e, _ -> error e "Invalid match argument %a" Expr.format e)
| EDefault { excepts; just; cons }, m -> (
let excs =
List.filter_map
@ -182,9 +182,9 @@ let rec lazy_eval :
match eval_to_value env just with
| (ELit (LBool true), _), _ -> lazy_eval ctx env llevel cons
| (ELit (LBool false), _), _ -> (EEmptyError, m), env
| e, _ -> error e "Invalid exception justification %a" (Print.expr ctx) e)
| e, _ -> error e "Invalid exception justification %a" Expr.format e)
| [(e, env)] ->
log "@[<hov 5>EVAL %a@]" (Print.expr ctx) e;
log "@[<hov 5>EVAL %a@]" Expr.format e;
lazy_eval ctx env llevel e
| _ :: _ :: _ ->
Errors.raise_multispanned_error
@ -195,12 +195,12 @@ let rec lazy_eval :
match eval_to_value env cond with
| (ELit (LBool true), _), _ -> lazy_eval ctx env llevel etrue
| (ELit (LBool false), _), _ -> lazy_eval ctx env llevel efalse
| e, _ -> error e "Invalid condition %a" (Print.expr ctx) e)
| e, _ -> error e "Invalid condition %a" Expr.format e)
| EErrorOnEmpty e, _ -> (
match eval_to_value env e ~eval_default:false with
| ((EEmptyError, _) as e'), _ ->
(* This does _not_ match the eager semantics ! *)
error e' "This value is undefined %a" (Print.expr ctx) e
error e' "This value is undefined %a" Expr.format e
| e, env -> lazy_eval ctx env llevel e)
| EAssert e, m -> (
if noassert then (ELit LUnit, m), env
@ -208,8 +208,8 @@ let rec lazy_eval :
match eval_to_value env e with
| (ELit (LBool true), m), env -> (ELit LUnit, m), env
| (ELit (LBool false), _), _ ->
error e "Assert failure (%a)" (Print.expr ctx) e
| _ -> error e "Invalid assertion condition %a" (Print.expr ctx) e)
error e "Assert failure (%a)" Expr.format e
| _ -> error e "Invalid assertion condition %a" Expr.format e)
| _ -> .
let interpret_program
@ -230,7 +230,7 @@ let interpret_program
let { contents = e, env } = Env.find scope_v all_env in
let e = Expr.unbox (Expr.remove_logging_calls e) in
log "=====================";
log "%a" (Print.expr ~debug:true ctx) e;
log "%a" (Print.expr ~debug:true ()) e;
log "=====================";
let m = Marked.get_mark e in
let application_arg =
@ -268,6 +268,6 @@ let apply ~source_file ~output_file ~scope prg _type_ordering =
ignore output_file;
let fmt = Format.std_formatter in
let result_expr, _env = interpret_program prg scope in
Print.expr prg.decl_ctx fmt result_expr
Expr.format fmt result_expr
let () = Driver.Plugin.register_dcalc ~name ~extension apply

10
compiler/scalc/print.ml
View File

@ -68,16 +68,16 @@ let rec format_expr
format_expr e
| ELit l -> Print.lit fmt l
| EApp ((EOp ((Map | Filter) as op), _), [arg1; arg2]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" Print.operator op
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" (Print.operator ~debug) op
format_with_parens arg1 format_with_parens arg2
| EApp ((EOp op, _), [arg1; arg2]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" format_with_parens arg1
Print.operator op format_with_parens arg2
(Print.operator ~debug) op format_with_parens arg2
| EApp ((EOp (Log _), _), [arg1]) when not debug ->
Format.fprintf fmt "%a" format_with_parens arg1
| EApp ((EOp op, _), [arg1]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" Print.operator op format_with_parens
arg1
Format.fprintf fmt "@[<hov 2>%a@ %a@]" (Print.operator ~debug) op
format_with_parens arg1
| EApp (f, []) -> Format.fprintf fmt "@[<hov 2>%a@ ()@]" format_expr f
| EApp (f, args) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" format_expr f
@ -85,7 +85,7 @@ let rec format_expr
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")
format_with_parens)
args
| EOp op -> Format.fprintf fmt "%a" Print.operator op
| EOp op -> Print.operator ~debug fmt op
let rec format_statement
(decl_ctx : decl_ctx)

12
compiler/scopelang/print.ml
View File

@ -48,7 +48,7 @@ let enum
(Print.typ ctx) typ))
(EnumConstructor.Map.bindings cases)
let scope ?(debug = false) ctx fmt (name, decl) =
let scope ?debug ctx fmt (name, decl) =
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@ %a@ %a@]@\n@[<v 2> %a@]"
Print.keyword "let" Print.keyword "scope" ScopeName.format_t name
(Format.pp_print_list ~pp_sep:Format.pp_print_space
@ -77,7 +77,7 @@ let scope ?(debug = false) ctx fmt (name, decl) =
(Print.typ ctx) typ Print.punctuation "="
(fun fmt e ->
match Marked.unmark loc with
| SubScopeVar _ | ToplevelVar _ -> Print.expr ctx fmt e
| SubScopeVar _ | ToplevelVar _ -> Print.expr () fmt e
| ScopelangScopeVar v -> (
match
Marked.unmark
@ -86,12 +86,12 @@ let scope ?(debug = false) ctx fmt (name, decl) =
with
| Reentrant ->
Format.fprintf fmt "%a@ %a" Print.op_style
"reentrant or by default" (Print.expr ~debug ctx) e
| _ -> Format.fprintf fmt "%a" (Print.expr ~debug ctx) e))
"reentrant or by default" (Print.expr ?debug ()) e
| _ -> Format.fprintf fmt "%a" (Print.expr ?debug ()) e))
e
| Assertion e ->
Format.fprintf fmt "%a %a" Print.keyword "assert"
(Print.expr ~debug ctx) e
(Print.expr ?debug ()) e
| Call (scope_name, subscope_name, _) ->
Format.fprintf fmt "%a %a%a%a%a" Print.keyword "call"
ScopeName.format_t scope_name Print.punctuation "["
@ -113,7 +113,7 @@ let print_topdef ctx ppf name (e, ty) =
Format.pp_close_box ppf ()
in
Format.pp_print_cut ppf ();
Print.expr ctx ppf e;
Print.expr () ppf e;
Format.pp_close_box ppf ()
let program ?(debug : bool = false) (fmt : Format.formatter) (p : 'm program) :

23
compiler/shared_ast/expr.ml
View File

@ -536,11 +536,7 @@ and equal : type a. (a, 't) gexpr -> (a, 't) gexpr -> bool =
| EArray es1, EArray es2 -> equal_list es1 es2
| ELit l1, ELit l2 -> l1 = l2
| EAbs { binder = b1; tys = tys1 }, EAbs { binder = b2; tys = tys2 } ->
Type.equal_list tys1 tys2
&&
let vars1, body1 = Bindlib.unmbind b1 in
let body2 = Bindlib.msubst b2 (Array.map (fun x -> EVar x) vars1) in
equal body1 body2
Type.equal_list tys1 tys2 && Bindlib.eq_mbinder equal b1 b2
| EApp { f = e1; args = args1 }, EApp { f = e2; args = args2 } ->
equal e1 e2 && equal_list args1 args2
| EAssert e1, EAssert e2 -> equal e1 e2
@ -702,18 +698,27 @@ let rec free_vars : ('a, 't) gexpr -> ('a, 't) gexpr Var.Set.t = function
let rec skip_wrappers : type a. (a, 'm) gexpr -> (a, 'm) gexpr = function
| EApp { f = EOp { op = Log _; _ }, _; args = [e] }, _ -> skip_wrappers e
| EApp { f = EApp { f = EOp { op = Log _; _ }, _; args = [f] }, _; args }, m
->
skip_wrappers (EApp { f; args }, m)
| EErrorOnEmpty e, _ -> skip_wrappers e
| EDefault { excepts = []; just = ELit (LBool true), _; cons = e }, _ ->
skip_wrappers e
| e -> e
let remove_logging_calls e =
let rec f e =
match Marked.unmark e with
| EApp { f = EOp { op = Log _; _ }, _; args = [arg] } -> map ~f arg
| _ -> map ~f e
let e, m = map ~f e in
( Bindlib.box_apply
(function
| EApp { f = EOp { op = Log _; _ }, _; args = [(arg, _)] } -> arg
| e -> e)
e,
m )
in
f e
let format ?debug decl_ctx ppf e = Print.expr ?debug decl_ctx ppf e
let format ppf e = Print.expr ~debug:false () ppf e
let rec size : type a. (a, 't) gexpr -> int =
fun e ->

9
compiler/shared_ast/expr.mli
View File

@ -340,12 +340,9 @@ val remove_logging_calls :
(** Removes all calls to [Log] unary operators in the AST, replacing them by
their argument. *)
val format :
?debug:bool (** [true] for debug printing *) ->
decl_ctx ->
Format.formatter ->
(_, _ mark) gexpr ->
unit
val format : Format.formatter -> ('a, 'm mark) gexpr -> unit
(** Simple printing without debug, use [Print.expr ()] instead to follow the
command-line debug setting *)
(** {2 Analysis and tests} *)

40
compiler/shared_ast/interpreter.ml
View File

@ -49,7 +49,7 @@ let log_indent = ref 0
different backends: python, ocaml, javascript, and interpreter *)
(** {1 Evaluation} *)
let print_log ctx entry infos pos e =
let print_log entry infos pos e =
if !Cli.trace_flag then
match entry with
| VarDef _ ->
@ -60,9 +60,7 @@ let print_log ctx entry infos pos e =
(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 = Format.asprintf "%a" (Print.expr ()) e in
let expr_str =
Re.Pcre.substitute ~rex:(Re.Pcre.regexp "\n\\s*")
~subst:(fun _ -> " ")
@ -91,7 +89,7 @@ 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 handle_eq evaluate_operator pos e1 e2 =
let open Runtime.Oper in
match e1, e2 with
| ELit LUnit, ELit LUnit -> true
@ -105,7 +103,7 @@ let handle_eq evaluate_operator ctx pos e1 e2 =
try
List.for_all2
(fun e1 e2 ->
match Marked.unmark (evaluate_operator ctx Eq pos [e1; e2]) with
match Marked.unmark (evaluate_operator Eq pos [e1; e2]) with
| ELit (LBool b) -> b
| _ -> assert false
(* should not happen *))
@ -115,7 +113,7 @@ let handle_eq evaluate_operator ctx pos e1 e2 =
StructName.equal s1 s2
&& StructField.Map.equal
(fun e1 e2 ->
match Marked.unmark (evaluate_operator ctx Eq pos [e1; e2]) with
match Marked.unmark (evaluate_operator Eq pos [e1; e2]) with
| ELit (LBool b) -> b
| _ -> assert false
(* should not happen *))
@ -126,7 +124,7 @@ let handle_eq evaluate_operator ctx pos e1 e2 =
EnumName.equal en1 en2
&& EnumConstructor.equal i1 i2
&&
match Marked.unmark (evaluate_operator ctx Eq pos [e1; e2]) with
match Marked.unmark (evaluate_operator Eq pos [e1; e2]) with
| ELit (LBool b) -> b
| _ -> assert false
(* should not happen *)
@ -136,7 +134,6 @@ let handle_eq evaluate_operator ctx pos e1 e2 =
(* Call-by-value: the arguments are expected to be already evaluated here *)
let rec evaluate_operator
evaluate_expr
ctx
(op : < overloaded : no ; .. > operator)
m
args =
@ -167,8 +164,7 @@ let rec evaluate_operator
(fun i arg ->
( Some
(Format.asprintf "Argument n°%d, value %a" (i + 1)
(Expr.format ctx ~debug:true)
arg),
(Print.expr ()) arg),
Expr.pos arg ))
args)
"Operator applied to the wrong arguments\n\
@ -183,10 +179,10 @@ let rec evaluate_operator
| Length, [(EArray es, _)] ->
ELit (LInt (Runtime.integer_of_int (List.length es)))
| Log (entry, infos), [e'] ->
print_log ctx entry infos pos e';
print_log entry infos pos e';
Marked.unmark e'
| Eq, [(e1, _); (e2, _)] ->
ELit (LBool (handle_eq (evaluate_operator evaluate_expr) ctx m e1 e2))
ELit (LBool (handle_eq (evaluate_operator evaluate_expr) m e1 e2))
| Map, [f; (EArray es, _)] ->
EArray
(List.map
@ -422,7 +418,7 @@ let rec evaluate_expr :
"wrong function call, expected %d arguments, got %d"
(Bindlib.mbinder_arity binder)
(List.length args)
| EOp { op; _ } -> evaluate_operator (evaluate_expr ctx) ctx op m args
| EOp { 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 \
@ -462,8 +458,7 @@ let rec evaluate_expr :
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)
(Print.expr ()) 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
@ -472,8 +467,7 @@ let rec evaluate_expr :
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)
(Print.expr ()) e size)
| EInj { e; name; cons } ->
propagate_empty_error (evaluate_expr ctx e)
@@ fun e -> Marked.mark m (EInj { e; name; cons })
@ -526,13 +520,11 @@ let rec evaluate_expr :
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
"Assertion failed: %a %a %a" (Print.expr ()) e1
(Print.operator ~debug:!Cli.debug_flag)
op (Print.expr ()) e2
| _ ->
Cli.debug_format "%a" (Expr.format ctx) e';
Cli.debug_format "%a" (Print.expr ()) e';
Errors.raise_spanned_error (Expr.mark_pos m) "Assertion failed")
| _ ->
Errors.raise_spanned_error (Expr.pos e')

1
compiler/shared_ast/interpreter.mli
View File

@ -22,7 +22,6 @@ open Definitions
val evaluate_operator :
((((_, _) dcalc_lcalc as 'a), 'm mark) gexpr -> ('a, 'm mark) gexpr) ->
decl_ctx ->
'a operator ->
'm mark ->
('a, 'm mark) gexpr list ->

3
compiler/shared_ast/operator.ml
View File

@ -533,7 +533,8 @@ let resolve_overload ctx (op : overloaded t Marked.pos) (operands : typ list) :
(Print.typ ctx) ty),
Marked.get_mark ty ))
operands)
"I don't know how to apply operator %a on types %a" Print.operator
"I don't know how to apply operator %a on types %a"
(Print.operator ~debug:true)
(Marked.unmark op)
(Format.pp_print_list
~pp_sep:(fun ppf () -> Format.fprintf ppf " and@ ")

12
compiler/shared_ast/optimizations.ml
View File

@ -342,10 +342,8 @@ let test_iota_reduction_1 () =
\ | B → (λ (x: any) → D x)\n\
after=C\n\
x"
(Format.asprintf "before=%a\nafter=%a"
(Print.expr_debug ~debug:false)
(Expr.unbox matchA)
(Print.expr_debug ~debug:false)
(Format.asprintf "before=%a\nafter=%a" Expr.format (Expr.unbox matchA)
Expr.format
(Expr.unbox
(optimize_expr
{
@ -416,10 +414,8 @@ let test_iota_reduction_2 () =
\ with\n\
\ | A → (λ (x: any) → C 20)\n\
\ | B → (λ (x: any) → D B x)\n"
(Format.asprintf "before=@[%a@]@.after=%a@."
(Print.expr_debug ~debug:false)
(Expr.unbox matchA)
(Print.expr_debug ~debug:false)
(Format.asprintf "before=@[%a@]@.after=%a@." Expr.format
(Expr.unbox matchA) Expr.format
(Expr.unbox
(optimize_expr
{

328
compiler/shared_ast/print.ml
View File

@ -40,7 +40,7 @@ let base_type (fmt : Format.formatter) (s : string) : unit =
Cli.format_with_style [ANSITerminal.yellow] fmt s
let punctuation (fmt : Format.formatter) (s : string) : unit =
Cli.format_with_style [ANSITerminal.cyan] fmt s
Format.pp_print_as fmt 1 (Cli.with_style [ANSITerminal.cyan] "%s" s)
let op_style (fmt : Format.formatter) (s : string) : unit =
Cli.format_with_style [ANSITerminal.green] fmt s
@ -72,6 +72,10 @@ let enum_constructor (fmt : Format.formatter) (c : EnumConstructor.t) : unit =
Cli.format_with_style [ANSITerminal.magenta] fmt
(Format.asprintf "%a" EnumConstructor.format_t c)
let struct_field (fmt : Format.formatter) (c : StructField.t) : unit =
Cli.format_with_style [ANSITerminal.magenta] fmt
(Format.asprintf "%a" StructField.format_t c)
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) =
@ -82,11 +86,40 @@ let rec typ (ctx : decl_ctx option) (fmt : Format.formatter) (ty : typ) : unit =
| TTuple ts ->
Format.fprintf fmt "@[<hov 2>(%a)@]"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ %a@ " op_style "*")
~pp_sep:(fun fmt () -> Format.fprintf fmt " %a@ " op_style "*")
typ)
ts
| TStruct s -> Format.fprintf fmt "@[<hov 2>%a@]" StructName.format_t s
| TEnum e -> Format.fprintf fmt "@[<hov 2>%a@]" EnumName.format_t e
| TStruct s -> (
match ctx with
| None -> StructName.format_t fmt s
| Some ctx ->
let fields = StructName.Map.find s ctx.ctx_structs in
if StructField.Map.is_empty fields then StructName.format_t fmt s
else
Format.fprintf fmt "@[<hv 2>%a %a@,%a@;<0 -2>%a@]" StructName.format_t s
punctuation "{"
(Format.pp_print_list
~pp_sep:(fun fmt () ->
punctuation fmt ";";
Format.pp_print_space fmt ())
(fun fmt (field_name, field_typ) ->
Format.fprintf fmt "@[<hv 2>%a%a@ %a@]" struct_field field_name
punctuation ":" typ field_typ))
(StructField.Map.bindings fields)
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))
(EnumConstructor.Map.bindings (EnumName.Map.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 op_style "→"
@ -219,8 +252,50 @@ let operator_to_string : type a. a Op.t -> string =
| HandleDefault -> "handle_default"
| HandleDefaultOpt -> "handle_default_opt"
let operator : type a. Format.formatter -> a operator -> unit =
fun fmt op ->
let operator_to_shorter_string : type a. a Op.t -> string =
let open Op in
function
| Not -> "~"
| Length -> "length"
| GetDay -> "get_day"
| GetMonth -> "get_month"
| GetYear -> "get_year"
| FirstDayOfMonth -> "first_day_of_month"
| LastDayOfMonth -> "last_day_of_month"
| ToRat_int | ToRat_mon | ToRat -> "to_rat"
| ToMoney_rat | ToMoney -> "to_mon"
| Round_rat | Round_mon | Round -> "round"
| Log _ -> "Log"
| Minus_int | Minus_rat | Minus_mon | Minus_dur | Minus -> "-"
| And -> "&&"
| Or -> "||"
| Xor -> "xor"
| Eq_int_int | Eq_rat_rat | Eq_mon_mon | Eq_dur_dur | Eq_dat_dat | Eq -> "="
| Map -> "map"
| Reduce -> "reduce"
| Concat -> "++"
| Filter -> "filter"
| Add_int_int | Add_rat_rat | Add_mon_mon | Add_dat_dur _ | Add_dur_dur | Add
->
"+"
| Sub_int_int | Sub_rat_rat | Sub_mon_mon | Sub_dat_dat | Sub_dat_dur
| Sub_dur_dur | Sub ->
"-"
| Mult_int_int | Mult_rat_rat | Mult_mon_rat | Mult_dur_int | Mult -> "*"
| Div_int_int | Div_rat_rat | Div_mon_mon | Div_mon_rat | Div_dur_dur | Div ->
"/"
| Lt_int_int | Lt_rat_rat | Lt_mon_mon | Lt_dur_dur | Lt_dat_dat | Lt -> "<"
| Lte_int_int | Lte_rat_rat | Lte_mon_mon | Lte_dur_dur | Lte_dat_dat | Lte ->
"<="
| Gt_int_int | Gt_rat_rat | Gt_mon_mon | Gt_dur_dur | Gt_dat_dat | Gt -> ">"
| Gte_int_int | Gte_rat_rat | Gte_mon_mon | Gte_dur_dur | Gte_dat_dat | Gte ->
">="
| Fold -> "fold"
| HandleDefault -> "handle_default"
| HandleDefaultOpt -> "handle_default_opt"
let operator : type a. ?debug:bool -> Format.formatter -> a operator -> unit =
fun ?(debug = true) fmt op ->
let open Op in
match op with
| Log (entry, infos) ->
@ -235,7 +310,9 @@ let operator : type a. Format.formatter -> a operator -> unit =
infos
(Cli.format_with_style [ANSITerminal.blue])
"}"
| op -> Format.fprintf fmt "%a" op_style (operator_to_string op)
| op ->
op_style fmt
(if debug then operator_to_string op else operator_to_shorter_string op)
let except (fmt : Format.formatter) (exn : except) : unit =
op_style fmt
@ -326,7 +403,7 @@ module Precedence = struct
let needs_parens ~context ?(rhs = false) e =
match expr context, expr e with
| _, Contained -> false
| Dot, Dot -> not rhs
| Dot, Dot -> rhs
| _, Dot -> false
| Dot, _ -> true
| App, App -> not rhs
@ -347,22 +424,21 @@ module Precedence = struct
| (Mul | Div), (Add | Sub) -> true
| Mul, (Mul | Div) -> false
| Div, (Mul | Div) -> rhs)
| Op _, App -> false
| Op _, App -> not rhs
| Op _, _ -> true
| Contained, _ -> false
end
let rec expr_aux :
type a.
?debug:bool ->
decl_ctx option ->
debug:bool ->
Bindlib.ctxt ->
ANSITerminal.style list ->
Format.formatter ->
(a, 't) gexpr ->
unit =
fun ?(debug = false) ctx bnd_ctx colors fmt e ->
let exprb bnd_ctx colors e = expr_aux ~debug ctx bnd_ctx colors e in
fun ~debug bnd_ctx colors fmt e ->
let exprb bnd_ctx colors e = expr_aux ~debug bnd_ctx colors e in
let exprc colors e = exprb bnd_ctx colors e in
let expr e = exprc colors e in
let var = if debug then var_debug else var in
@ -402,55 +478,90 @@ let rec expr_aux :
punctuation fmt ".";
Format.pp_print_int fmt index
| ELit l -> lit fmt l
| EApp { f = EAbs { binder; tys }, _; args } ->
let xs, body, bnd_ctx = Bindlib.unmbind_in bnd_ctx binder in
let expr = exprb bnd_ctx in
let xs_tau = List.mapi (fun i tau -> xs.(i), tau) tys in
let xs_tau_arg = List.map2 (fun (x, tau) arg -> x, tau, arg) xs_tau args in
Format.fprintf fmt "@[<hv 0>%a%a@]"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "")
(fun fmt (x, tau, arg) ->
Format.fprintf fmt
"@[<hv 0>@[<hv 2>@[<hov 4>%a@ %a@ %a@ %a@ %a@]@ %a@]@ %a@]@\n"
keyword "let" var x punctuation ":" (typ ctx) tau punctuation "="
(expr colors) arg keyword "in"))
xs_tau_arg (rhs expr) body
| EApp { f = EAbs _, _; _ } ->
let rec pr bnd_ctx colors fmt = function
| EApp { f = EAbs { binder; tys }, _; args }, _ ->
let xs, body, bnd_ctx = Bindlib.unmbind_in bnd_ctx binder in
let xs_tau = List.mapi (fun i tau -> xs.(i), tau) tys in
let xs_tau_arg =
List.map2 (fun (x, tau) arg -> x, tau, arg) xs_tau args
in
Format.pp_print_list
(fun fmt (x, tau, arg) ->
Format.fprintf fmt
"@[<hv 2>@[<hov 4>%a %a %a@ %a@ %a@]@ %a@;<1 -2>%a@]" keyword
"let" var x punctuation ":" (typ None) tau punctuation "="
(exprc colors) arg keyword "in")
fmt xs_tau_arg;
Format.pp_print_cut fmt ();
rhs (pr bnd_ctx) fmt body
| e -> rhs (exprb bnd_ctx) fmt e
in
Format.pp_open_vbox fmt 0;
pr bnd_ctx colors fmt e;
Format.pp_close_box fmt ()
| EAbs { binder; tys } ->
let xs, body, bnd_ctx = Bindlib.unmbind_in bnd_ctx binder in
let expr = exprb bnd_ctx in
let xs_tau = List.mapi (fun i tau -> xs.(i), tau) tys 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 ")"))
Format.fprintf fmt "@[<hv 0>%a @[<hv 2>%a@]@ @]%a@ %a" punctuation "λ"
(Format.pp_print_list ~pp_sep:Format.pp_print_space (fun fmt (x, tau) ->
punctuation fmt "(";
Format.pp_open_hvbox fmt 2;
var fmt x;
punctuation fmt ":";
Format.pp_print_space fmt ();
typ None fmt tau;
Format.pp_close_box fmt ();
punctuation fmt ")"))
xs_tau punctuation "→" (rhs expr) body
| EApp { f = EOp { op = (Map | Filter) as op; _ }, _; args = [arg1; arg2] } ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" operator op (lhs exprc) arg1
(rhs exprc) arg2
| EApp { f = EOp { op = (And | Or) as op; _ }, _; args = [arg1; arg2] } ->
Format.fprintf fmt "%a@ %a %a" (lhs exprc) arg1 operator op (rhs exprc) arg2
| EApp { f = EOp { op; _ }, _; args = [arg1; arg2] } ->
Format.fprintf fmt "@[<hv 0>%a@ %a %a@]" (lhs exprc) arg1 operator op
(rhs exprc) arg2
Format.fprintf fmt "@[<hv 2>%a %a@ %a@]" (operator ~debug) op (lhs exprc)
arg1 (rhs exprc) arg2
| EApp { f = EOp { op = Log _ as op; _ }, _; args = [arg1] } ->
Format.fprintf fmt "@[<hv 0>%a@ %a@]" (operator ~debug) op (rhs exprc) arg1
| EApp { f = EOp { op = op0; _ }, _; args = [_; _] } ->
let prec = Precedence.expr e in
let rec pr colors fmt = function
(* Flatten sequences of the same associative op *)
| EApp { f = EOp { op; _ }, _; args = [arg1; arg2] }, _ when op = op0 -> (
(match prec with
| Op (And | Or | Mul | Add | Div | Sub) -> lhs pr fmt arg1
| _ -> lhs exprc fmt arg1);
Format.pp_print_space fmt ();
(operator ~debug) fmt op;
Format.pp_print_char fmt ' ';
match prec with
| Op (And | Or | Mul | Add) -> rhs pr fmt arg2
| _ -> rhs exprc fmt arg2)
| e -> exprc colors fmt e
in
Format.pp_open_hvbox fmt 0;
pr colors fmt e;
Format.pp_close_box fmt ()
| EApp { f = EOp { op; _ }, _; args = [arg1] } ->
Format.fprintf fmt "%a %a" operator op (rhs exprc) arg1
Format.fprintf fmt "@[<hv 2>%a@ %a@]" (operator ~debug) op (rhs exprc) arg1
| EApp { f; args } ->
Format.fprintf fmt "@[<hv 2>%a@ %a@]" (lhs exprc) f
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ")
(rhs exprc))
args
| EIfThenElse { cond; etrue; efalse } ->
Format.fprintf fmt
"@[<hv 0>@[<hv 2>%a@ %a@]@ @[<hv 2>%a@ %a@]@ @[<hv 2>%a@ %a@]@]" keyword
"if" expr cond keyword "then" expr etrue keyword "else" (rhs exprc) efalse
| EOp { op; _ } -> operator fmt op
| EIfThenElse _ ->
let rec pr els fmt = function
| EIfThenElse { cond; etrue; efalse }, _ ->
Format.fprintf fmt "@[<hv 2>%a@ %a@]@ @[<hv 2>%a@ %a@]@ %a" keyword
(if els then "else if" else "if")
expr cond keyword "then" expr etrue (pr true) efalse
| e -> Format.fprintf fmt "@[<hv 2>%a@ %a@]" keyword "else" (rhs exprc) e
in
Format.pp_open_hvbox fmt 0;
pr false fmt e;
Format.pp_close_box fmt ()
| EOp { op; _ } -> operator ~debug fmt op
| EDefault { excepts; just; cons } ->
if List.length excepts = 0 then
Format.fprintf fmt "@[<hov 2>%a%a@ %a@ %a%a@]" punctuation "⟨" expr just
Format.fprintf fmt "@[<hv 1>%a%a@ %a %a%a@]" punctuation "⟨" expr just
punctuation "⊢" expr cons punctuation "⟩"
else
Format.fprintf fmt
@ -473,32 +584,45 @@ let rec expr_aux :
Format.fprintf fmt "@[<hov 2>%a@ %a@]" keyword "raise" except exn
| ELocation loc -> location fmt loc
| EDStructAccess { e; field; _ } ->
Format.fprintf fmt "%a%a%a%a%a" (lhs exprc) e punctuation "." punctuation
"\"" IdentName.format_t field punctuation "\""
Format.fprintf fmt "@[<hv 2>%a%a@,%a%a%a@]" (lhs exprc) e punctuation "."
punctuation "\"" IdentName.format_t field punctuation "\""
| EStruct { name; fields } ->
Format.fprintf fmt "@[<hv 0>@[<hv 2>%a@,@[<hv 0>%a@]@]@,%a%a@]" punctuation
"{"
(Format.pp_print_list
~pp_sep:(fun fmt () -> punctuation fmt ";")
(fun fmt (field_name, field_expr) ->
Format.fprintf fmt "@ @[<hov 2>%a%a%a %a@ %a@]" punctuation "\""
StructField.format_t field_name punctuation "\"" punctuation "="
(lhs exprc) field_expr))
(StructField.Map.bindings fields)
punctuation "}_" StructName.format_t name
if StructField.Map.is_empty fields then (
punctuation fmt "{";
StructName.format_t fmt name;
punctuation fmt "}")
else
Format.fprintf fmt "@[<hv 2>%a %a@ %a@;<1 -2>%a@]" punctuation "{"
StructName.format_t name
(Format.pp_print_list ~pp_sep:Format.pp_print_space
(fun fmt (field_name, field_expr) ->
Format.fprintf fmt "@[<hv 2>%a %a@ %a%a@]" struct_field field_name
punctuation "=" (lhs exprc) field_expr punctuation ";"))
(StructField.Map.bindings fields)
punctuation "}"
| EStructAccess { e; field; _ } ->
Format.fprintf fmt "%a%a%a%a%a" (lhs exprc) e punctuation "." punctuation
"\"" StructField.format_t field punctuation "\""
Format.fprintf fmt "@[<hv 2>%a%a@,%a@]" (lhs exprc) e punctuation "."
struct_field field
| EInj { e; cons; _ } ->
Format.fprintf fmt "%a@ %a" EnumConstructor.format_t cons (rhs exprc) e
Format.fprintf fmt "@[<hv 2>%a@ %a@]" EnumConstructor.format_t cons
(rhs exprc) e
| EMatch { e; cases; _ } ->
Format.fprintf fmt "@[<v 0>@[<hov 2>%a@ %a@]@ %a@ %a@]" keyword "match"
Format.fprintf fmt "@[<v 0>@[<hv 2>%a@ %a@ %a@]@ %a@]" keyword "match"
(lhs exprc) e 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 "→" (rhs exprc) case_expr))
match case_expr with
| EAbs { binder; _ }, _ ->
let xs, body, bnd_ctx = Bindlib.unmbind_in bnd_ctx binder in
let expr = exprb bnd_ctx in
Format.fprintf fmt "@[<hov 2>%a %a@ %a@ %a@ %a@]" punctuation "|"
enum_constructor cons_name
(Format.pp_print_seq ~pp_sep:Format.pp_print_space var)
(Array.to_seq xs) punctuation "→" (rhs expr) body
| e ->
Format.fprintf fmt "@[<hov 2>%a %a@ %a@ %a@]" punctuation "|"
enum_constructor cons_name punctuation "→" (rhs exprc) e))
(EnumConstructor.Map.bindings cases)
| EScopeCall { scope; args } ->
Format.pp_open_hovbox fmt 2;
@ -530,8 +654,9 @@ let rec colors =
let typ_debug = typ None
let typ ctx = typ (Some ctx)
let expr_debug ?debug = expr_aux ?debug None Bindlib.empty_ctxt colors
let expr ?debug ctx = expr_aux ?debug (Some ctx) Bindlib.empty_ctxt colors
let expr ?(debug = !Cli.debug_flag) () ppf e =
expr_aux ~debug Bindlib.empty_ctxt colors ppf e
let scope_let_kind ?debug:(_debug = true) _ctx fmt k =
match k with
@ -542,9 +667,10 @@ let scope_let_kind ?debug:(_debug = true) _ctx fmt k =
| DestructuringSubScopeResults -> keyword fmt "sub_get"
| Assertion -> keyword fmt "assert"
let rec scope_body_expr ?(debug = false) ctx fmt b : unit =
let[@ocamlformat "disable"] rec
scope_body_expr ?(debug = false) ctx fmt b : unit =
match b with
| Result e -> Format.fprintf fmt "%a %a" keyword "return" (expr ~debug ctx) e
| Result e -> Format.fprintf fmt "%a %a" keyword "return" (expr ~debug ()) e
| ScopeLet
{
scope_let_kind = kind;
@ -554,14 +680,17 @@ let rec scope_body_expr ?(debug = false) ctx fmt b : unit =
_;
} ->
let x, next = Bindlib.unbind scope_let_next in
Format.fprintf fmt "@[<hov 2>%a %a %a %a %a %a@;%a@;%a @]@,%a" keyword "let"
(scope_let_kind ~debug ctx)
kind
(if debug then var_debug else var)
x punctuation ":" (typ ctx) scope_let_typ punctuation "="
(expr ~debug ctx) scope_let_expr keyword "in"
(scope_body_expr ~debug ctx)
next
Format.fprintf fmt
"@[<hv 2>@[<hov 4>%a %a %a %a@ %a@ %a@]@ %a@;<1 -2>%a@]@,%a"
keyword "let"
(scope_let_kind ~debug ctx) kind
(if debug then var_debug else var) x
punctuation ":"
(typ ctx) scope_let_typ
punctuation "="
(expr ~debug ()) scope_let_expr
keyword "in"
(scope_body_expr ~debug ctx) next
let scope_body ?(debug = false) ctx fmt (n, l) : unit =
let {
@ -577,23 +706,36 @@ let scope_body ?(debug = false) ctx fmt (n, l) : unit =
let x, body = Bindlib.unbind body in
let _ =
let () =
Format.pp_open_vbox fmt 2;
let _ =
Format.pp_open_hbox fmt ();
keyword fmt "let scope";
Format.pp_print_space fmt ();
ScopeName.format_t fmt n;
let () =
Format.pp_open_hvbox fmt 2;
let () =
Format.pp_open_hovbox fmt 4;
keyword fmt "let scope";
Format.pp_print_space fmt ();
ScopeName.format_t fmt n;
Format.pp_close_box fmt ()
in
Format.pp_print_space fmt ();
punctuation fmt "(";
(if debug then var_debug else var) fmt x;
let () =
Format.pp_open_hvbox fmt 2;
(if debug then var_debug else var) fmt x;
punctuation fmt ":";
Format.pp_print_space fmt ();
(if debug then typ_debug else typ ctx) fmt input_typ;
punctuation fmt ")";
Format.pp_close_box fmt ()
in
Format.pp_print_cut fmt ();
punctuation fmt ":";
Format.pp_print_space fmt ();
(if debug then typ_debug else typ ctx) fmt input_typ;
punctuation fmt ")";
punctuation fmt ":";
Format.pp_print_space fmt ();
(if debug then typ_debug else typ ctx) fmt output_typ;
Format.pp_print_string fmt " ";
let () =
Format.pp_open_hvbox fmt 2;
(if debug then typ_debug else typ ctx) fmt output_typ;
Format.pp_close_box fmt ()
in
Format.pp_print_space fmt ();
punctuation fmt "=";
Format.pp_close_box fmt ()
@ -652,7 +794,9 @@ let scope
(ctx : decl_ctx)
(fmt : Format.formatter)
((n, s) : ScopeName.t * 'm scope_body) : unit =
scope_body ~debug ctx fmt (n, s)
Format.pp_open_vbox fmt 0;
scope_body ~debug ctx fmt (n, s);
Format.pp_close_box fmt ()
let code_item ?(debug = false) decl_ctx fmt c =
match c with
@ -660,7 +804,7 @@ let code_item ?(debug = false) decl_ctx fmt c =
| Topdef (n, ty, e) ->
Format.fprintf fmt "@[%a %a %a %a %a %a @]" keyword "let topval"
TopdefName.format_t n op_style ":" (typ decl_ctx) ty op_style "="
(expr ~debug decl_ctx) e
(expr ~debug ()) e
let rec code_item_list ?(debug = false) decl_ctx fmt c =
match c with

25
compiler/shared_ast/print.mli
View File

@ -23,10 +23,20 @@ open Definitions
val base_type : Format.formatter -> string -> unit
val keyword : Format.formatter -> string -> unit
val punctuation : Format.formatter -> string -> unit
(** The argument is assumed to be 1-column wide (but can be a multi-char utf8
character) *)
val op_style : Format.formatter -> string -> unit
val lit_style : Format.formatter -> string -> unit
(** {1 Some basic stringifiers} *)
val operator_to_string : 'a operator -> string
(** Prints the operator symbols with kind suffixes, as expected by the OCaml
backend (e.g. "+^", "+$", etc.) *)
(** {1 Formatters} *)
val uid_list : Format.formatter -> Uid.MarkedString.info list -> unit
@ -35,27 +45,18 @@ val tlit : Format.formatter -> typ_lit -> unit
val location : Format.formatter -> 'a glocation -> unit
val typ : decl_ctx -> Format.formatter -> typ -> unit
val lit : Format.formatter -> lit -> unit
val operator : Format.formatter -> 'a operator -> unit
val operator : ?debug:bool -> Format.formatter -> 'a operator -> unit
val log_entry : Format.formatter -> log_entry -> unit
val except : Format.formatter -> except -> unit
val var : Format.formatter -> 'e Var.t -> unit
val var_debug : Format.formatter -> 'e Var.t -> unit
val expr :
?debug:bool (** [true] for debug printing *) ->
decl_ctx ->
Format.formatter ->
('a, 'm mark) gexpr ->
unit
?debug:bool -> unit -> Format.formatter -> ('a, 'm mark) gexpr -> unit
(** Same as [expr], but with a debug flag that defaults to [!Cli.debug_flag] *)
(** {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
val scope :

2
compiler/shared_ast/typing.ml
View File

@ -394,7 +394,7 @@ and typecheck_expr_top_down :
| Some ty -> ty
| None ->
Errors.raise_spanned_error pos_e "Reference to %a not found"
(Expr.format ctx) e
(Print.expr ()) e
in
Expr.elocation loc (mark_with_tau_and_unify (ast_to_typ ty))
| A.EStruct { name; fields } ->

9
compiler/verification/conditions.ml
View File

@ -139,8 +139,7 @@ let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : typed expr) :
"Internal error: this expression does not have the structure expected \
by the VC generator:\n\
%a"
(Expr.format ~debug:true ctx.decl)
e)
(Print.expr ()) e)
| EErrorOnEmpty d ->
d (* input subscope variables and non-input scope variable *)
| _ ->
@ -148,8 +147,7 @@ let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : typed expr) :
"Internal error: this expression does not have the structure expected by \
the VC generator:\n\
%a"
(Expr.format ~debug:true ctx.decl)
e
(Print.expr ()) e
(** {1 Verification conditions generator}*)
@ -334,8 +332,7 @@ let rec generate_verification_conditions_scope_body_expr
"Internal error: this assertion does not have the structure \
expected by the VC generator:\n\
%a"
(Expr.format ~debug:true ctx.decl)
e)
(Print.expr ()) e)
| DestructuringInputStruct ->
{ ctx with input_vars = scope_let_var :: ctx.input_vars }, [], []
| ScopeVarDefinition | SubScopeVarDefinition ->

4
compiler/verification/io.ml
View File

@ -138,7 +138,7 @@ module MakeBackendIO (B : Backend) = struct
| Some counterexample -> "\n" ^ counterexample
let encode_and_check_vc
(decl_ctx : decl_ctx)
(_decl_ctx : decl_ctx)
(vc : Conditions.verification_condition * vc_encoding_result) : bool =
let vc, z3_vc = vc in
@ -154,7 +154,7 @@ module MakeBackendIO (B : Backend) = struct
| Conditions.NoEmptyError ->
"the variable definition never to return an empty error"
| NoOverlappingExceptions -> "no two exceptions to ever overlap")
(Expr.format decl_ctx) vc.vc_guard (Expr.format decl_ctx) vc.vc_asserts;
(Print.expr ()) vc.vc_guard (Print.expr ()) vc.vc_asserts;
match z3_vc with
| Success (encoding, backend_ctx) -> (

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

@ -433,8 +433,7 @@ let rec translate_op :
fun ctx op args ->
let ill_formed () =
Format.kasprintf failwith
"[Z3 encoding] Ill-formed operator application: %a"
(Shared_ast.Expr.format ctx.ctx_decl)
"[Z3 encoding] Ill-formed operator application: %a" Shared_ast.Expr.format
(Shared_ast.Expr.eapp
(Shared_ast.Expr.eop op [] (Untyped { pos = Pos.no_pos }))
(List.map Shared_ast.Expr.untype args)

26
tests/test_array/good/aggregation_2.catala_en
View File

@ -33,31 +33,29 @@ scope B:
$ catala Interpret -s A
[RESULT] Computation successful! Results:
[RESULT] x =
[ { "id" = 0; "income" = $0.00}_S;
{ "id" = 1; "income" = $9.00}_S;
{ "id" = 2; "income" = $5.20}_S ]
[ { S id = 0; income = $0.00; };
{ S id = 1; income = $9.00; };
{ S id = 2; income = $5.20; } ]
```
```catala-test-inline
$ catala Interpret -s B
[RESULT] Computation successful! Results:
[RESULT] argmax = { "id" = 1; "income" = $9.00}_S
[RESULT] argmin = { "id" = 0; "income" = $0.00}_S
[RESULT] argmax = { S id = 1; income = $9.00; }
[RESULT] argmin = { S id = 0; income = $0.00; }
```
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] x = ESome
[ ESome
{ "id" = ESome 0; "income" = ESome $0.00}_S;
ESome
{ "id" = ESome 1; "income" = ESome $9.00}_S;
ESome
{ "id" = ESome 2; "income" = ESome $5.20}_S ]
[RESULT] x =
ESome
[ ESome { S id = ESome 0; income = ESome $0.00; };
ESome { S id = ESome 1; income = ESome $9.00; };
ESome { S id = ESome 2; income = ESome $5.20; } ]
```
```catala-test-inline
$ catala Interpret_Lcalc -s B --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] argmax = ESome { "id" = ESome 1; "income" = ESome $9.00}_S
[RESULT] argmin = ESome { "id" = ESome 0; "income" = ESome $0.00}_S
[RESULT] argmax = ESome { S id = ESome 1; income = ESome $9.00; }
[RESULT] argmin = ESome { S id = ESome 0; income = ESome $0.00; }
```

70
tests/test_array/good/aggregation_3.catala_en
View File

@ -35,47 +35,47 @@ scope S:
$ catala scopelang -s S
let scope S (x: integer|internal|output) =
let x : integer = ⟨true ⊢ 0⟩;
assert reduce
(λ (i_1: integer) (i_2: integer) →
if
let i : integer = i_1 in
to_rat_int ((2 -! i) *! (2 -! i))
<. let i : integer = i_2 in
to_rat_int ((2 -! i) *! (2 -! i))
then i_1
else i_2),
42,
[ 1; 2; 3 ]
assert (reduce
(λ (i_1: integer) (i_2: integer) →
if
(let i : integer = i_1 in
to_rat ((2 - i) * (2 - i)))
< let i : integer = i_2 in
to_rat ((2 - i) * (2 - i))
then i_1
else i_2),
42,
[ 1; 2; 3 ])
= 2;
assert reduce
(λ (max1: decimal) (max2: decimal) →
if max1 >. max2 then max1 else max2),
10.,
map (λ (i: integer) → to_rat_int i) [ 1; 2; 3 ]
assert (reduce
(λ (max1: decimal) (max2: decimal) →
if max1 > max2 then max1 else max2),
10.,
map (λ (i: integer) → to_rat i) [ 1; 2; 3 ])
= 3.;
assert reduce
(λ (max1: integer) (max2: integer) →
if max1 >! max2 then max1 else max2),
10,
[ 1; 2; 3 ]
assert (reduce
(λ (max1: integer) (max2: integer) →
if max1 > max2 then max1 else max2),
10,
[ 1; 2; 3 ])
= 3;
assert length filter (λ (i: integer) → i >=! 2) [ 1; 2; 3 ] = 2;
assert length [ 1; 2; 3 ] = 3;
assert reduce
(λ (sum1: integer) (sum2: integer) → sum1 +! sum2),
0,
map (λ (i: integer) → i +! 2) [ 1; 2; 3 ]
assert (length filter (λ (i: integer) → i >= 2) [ 1; 2; 3 ]) = 2;
assert (length [ 1; 2; 3 ]) = 3;
assert (reduce
(λ (sum1: integer) (sum2: integer) → sum1 + sum2),
0,
map (λ (i: integer) → i + 2) [ 1; 2; 3 ])
= 12;
assert reduce
(λ (sum1: integer) (sum2: integer) → sum1 +! sum2),
0,
[ 1; 2; 3 ]
assert (reduce
(λ (sum1: integer) (sum2: integer) → sum1 + sum2),
0,
[ 1; 2; 3 ])
= 6;
assert map (λ (i: integer) → i +! 2)
filter (λ (i: integer) → i >! 2) [ 1; 2; 3 ]
assert (map (λ (i: integer) → i + 2)
filter (λ (i: integer) → i > 2) [ 1; 2; 3 ])
= [ 5 ];
assert filter (λ (i: integer) → i >=! 2) [ 1; 2; 3 ] = [ 2; 3 ];
assert map (λ (i: integer) → i +! 2) [ 1; 2; 3 ] = [ 3; 4; 5 ]
assert (filter (λ (i: integer) → i >= 2) [ 1; 2; 3 ]) = [ 2; 3 ];
assert (map (λ (i: integer) → i + 2) [ 1; 2; 3 ]) = [ 3; 4; 5 ]
```
```catala-test-inline

41
tests/test_array/good/concatenation.catala_en
View File

@ -19,29 +19,20 @@ $ catala Interpret -s A
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] x = ESome
[ ESome 0; ESome 1; ESome 2; ESome 3; ESome 4; ESome 5; ESome 6 ]
[RESULT] y = ESome
[ ESome
0;
ESome
1;
ESome
2;
ESome
3;
ESome
4;
ESome
5;
ESome
6;
ESome
7;
ESome
8;
ESome
9;
ESome
10 ]
[RESULT] x =
ESome
[ ESome 0; ESome 1; ESome 2; ESome 3; ESome 4; ESome 5; ESome 6 ]
[RESULT] y =
ESome
[ ESome 0;
ESome 1;
ESome 2;
ESome 3;
ESome 4;
ESome 5;
ESome 6;
ESome 7;
ESome 8;
ESome 9;
ESome 10 ]
```

26
tests/test_array/good/fold.catala_en
View File

@ -33,31 +33,29 @@ scope B:
$ catala Interpret -s A
[RESULT] Computation successful! Results:
[RESULT] x =
[ { "id" = 0; "income" = $0.00}_S;
{ "id" = 1; "income" = $9.00}_S;
{ "id" = 2; "income" = $5.20}_S ]
[ { S id = 0; income = $0.00; };
{ S id = 1; income = $9.00; };
{ S id = 2; income = $5.20; } ]
```
```catala-test-inline
$ catala Interpret -s B
[RESULT] Computation successful! Results:
[RESULT] argmax = { "id" = 1; "income" = $9.00}_S
[RESULT] argmin = { "id" = 0; "income" = $0.00}_S
[RESULT] argmax = { S id = 1; income = $9.00; }
[RESULT] argmin = { S id = 0; income = $0.00; }
```
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] x = ESome
[ ESome
{ "id" = ESome 0; "income" = ESome $0.00}_S;
ESome
{ "id" = ESome 1; "income" = ESome $9.00}_S;
ESome
{ "id" = ESome 2; "income" = ESome $5.20}_S ]
[RESULT] x =
ESome
[ ESome { S id = ESome 0; income = ESome $0.00; };
ESome { S id = ESome 1; income = ESome $9.00; };
ESome { S id = ESome 2; income = ESome $5.20; } ]
```
```catala-test-inline
$ catala Interpret_Lcalc -s B --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] argmax = ESome { "id" = ESome 1; "income" = ESome $9.00}_S
[RESULT] argmin = ESome { "id" = ESome 0; "income" = ESome $0.00}_S
[RESULT] argmax = ESome { S id = ESome 1; income = ESome $9.00; }
[RESULT] argmin = ESome { S id = ESome 0; income = ESome $0.00; }
```

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

@ -15,20 +15,16 @@ scope TestBool:
$ catala Dcalc
let TestBool : TestBool_in → TestBool =
λ (TestBool_in: TestBool_in) →
let foo : unit → bool = TestBool_in."foo_in" in
let bar : unit → integer = TestBool_in."bar_in" in
let bar1 : integer =
error_empty ⟨ bar () | true ⊢ ⟨true ⊢ 1⟩ ⟩
in
let foo1 : bool =
error_empty
⟨ foo ()
| true
⊢ ⟨true ⊢
⟨ ⟨bar1 >=! 0 ⊢ true⟩, ⟨bar1 <! 0 ⊢ false⟩
| false ⊢ ∅ ⟩⟩ ⟩
in
{ "foo" = foo1; "bar" = bar1}_TestBool
let foo : unit → bool = TestBool_in.foo_in in
let bar : unit → integer = TestBool_in.bar_in in
let bar1 : integer = error_empty ⟨ bar () | true ⊢ ⟨true ⊢ 1⟩ ⟩ in
let foo1 : bool =
error_empty
⟨ foo ()
| true
⊢ ⟨true ⊢ ⟨ ⟨bar1 >= 0 ⊢ true⟩, ⟨bar1 < 0 ⊢ false⟩ | false ⊢ ∅ ⟩⟩ ⟩
in
{ TestBool foo = foo1; bar = bar1; }
in
TestBool
```
@ -50,9 +46,7 @@ struct TestBool = {
let scope TestBool (foo: bool|context|output) (bar: integer|context|output) =
let bar : integer = reentrant or by default ⟨true ⊢ 1⟩;
let foo : bool = reentrant or by default
⟨true ⊢
⟨ ⟨bar >=! 0 ⊢ true⟩, ⟨bar <! 0 ⊢ false⟩
| false ⊢ ∅ ⟩⟩
⟨true ⊢ ⟨ ⟨bar >= 0 ⊢ true⟩, ⟨bar < 0 ⊢ false⟩ | false ⊢ ∅ ⟩⟩
```
```catala-test-inline
$ catala Interpret_Lcalc -s TestBool --avoid_exceptions --optimize

5
tests/test_dec/good/infinite_precision.catala_en
View File

@ -26,8 +26,9 @@ $ catala Interpret -s A
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] a = ESome
-0.000000000000000000000000000000000000000000000000000000000078695580959228473468…
[RESULT] a =
ESome
-0.000000000000000000000000000000000000000000000000000000000078695580959228473468…
[RESULT] x = ESome 84.64866565265689623
[RESULT] y = ESome -4.3682977870532065498
[RESULT] z = ESome 654265429805103220650980650.570540510654

4
tests/test_exception/good/grouped_exceptions.catala_en
View File

@ -50,11 +50,11 @@ scope Benefit:
$ catala Interpret -s Benefit
[RESULT] Computation successful! Results:
[RESULT] benefit = $2000.00
[RESULT] person = { "age" = 26; "disabled" = true}_Person
[RESULT] person = { Person age = 26; disabled = true; }
```
```catala-test-inline
$ catala Interpret_Lcalc -s Benefit --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] benefit = ESome $2000.00
[RESULT] person = ESome { "age" = ESome 26; "disabled" = ESome true}_Person
[RESULT] person = ESome { Person age = ESome 26; disabled = ESome true; }
```

6
tests/test_exception/good/groups_of_exceptions.catala_en
View File

@ -39,10 +39,8 @@ struct Foo = {
let scope Foo (y: integer|input) (x: integer|internal|output) =
let x : integer =
⟨ ⟨ ⟨true ⊢
⟨ ⟨y = 4 ⊢ 4⟩, ⟨y = 5 ⊢ 5⟩ | false ⊢ ∅ ⟩⟩
| true
⊢ ⟨ ⟨y = 2 ⊢ 2⟩, ⟨y = 3 ⊢ 3⟩ | false ⊢ ∅ ⟩ ⟩
⟨ ⟨ ⟨true ⊢ ⟨ ⟨y = 4 ⊢ 4⟩, ⟨y = 5 ⊢ 5⟩ | false ⊢ ∅ ⟩⟩
| true ⊢ ⟨ ⟨y = 2 ⊢ 2⟩, ⟨y = 3 ⊢ 3⟩ | false ⊢ ∅ ⟩ ⟩
| true ⊢ ⟨ ⟨y = 0 ⊢ 0⟩, ⟨y = 1 ⊢ 1⟩ | false ⊢ ∅ ⟩ ⟩
```

24
tests/test_func/good/context_func.catala_en
View File

@ -25,8 +25,7 @@ $ catala Scopelang -s B
│ ‾
└─ Test
let scope B (b: bool|input) =
let a.f : integer → integer =
λ (x: integer) → ⟨b && x >! 0 ⊢ x -! 1⟩;
let a.f : integer → integer = λ (x: integer) → ⟨b && x > 0 ⊢ x - 1⟩;
call A[a]
```
@ -39,12 +38,13 @@ $ catala Dcalc -s A
5 │ context f content integer depends on x content integer
│ ‾
└─ Test
let scope A (A_in: A_in): A =
let get f : integer → integer = A_in."f_in" in
let scope A (A_in: A_in {f_in: integer → integer}): A =
let get f : integer → integer = A_in.f_in in
let set f : integer → integer =
λ (x: integer) →
error_empty ⟨ f x | true ⊢ ⟨true ⊢ x +! 1⟩ ⟩ in
return {}_A
error_empty ⟨ f x | true ⊢ ⟨true ⊢ x + 1⟩ ⟩
in
return {A}
```
```catala-test-inline
@ -56,10 +56,12 @@ $ catala Dcalc -s B
5 │ context f content integer depends on x content integer
│ ‾
└─ Test
let scope B (B_in: B_in): B =
let get b : bool = B_in."b_in" in
let scope B (B_in: B_in {b_in: bool}): B =
let get b : bool = B_in.b_in in
let sub_set a.f : integer → integer =
λ (x: integer) → ⟨b && x >! 0 ⊢ x -! 1⟩ in
let call result : A = A { "f_in" = a.f}_A_in in
return {}_B
λ (x: integer) →
⟨b && x > 0 ⊢ x - 1⟩
in
let call result : A = A { A_in f_in = a.f; } in
return {B}
```

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

@ -19,18 +19,27 @@ scope A:
```catala-test-inline
$ catala Dcalc -s A
let scope A (A_in: A_in): A =
let get c : integer = A_in."c_in" in
let get d : integer = A_in."d_in" in
let get e : unit → integer = A_in."e_in" in
let get f : unit → integer = A_in."f_in" in
let scope A
(A_in:
A_in {
c_in: integer;
d_in: integer;
e_in: unit → integer;
f_in: unit → integer
})
: A {b: integer; d: integer; f: integer}
=
let get c : integer = A_in.c_in in
let get d : integer = A_in.d_in in
let get e : unit → integer = A_in.e_in in
let get f : unit → integer = A_in.f_in in
let set a : integer = error_empty ⟨true ⊢ 0⟩ in
let set b : integer = error_empty ⟨true ⊢ a +! 1⟩ in
let set b : integer = error_empty ⟨true ⊢ a + 1⟩ in
let set e : integer =
error_empty ⟨ e () | true ⊢ ⟨true ⊢ b +! c +! d +! 1⟩ ⟩ in
let set f : integer =
error_empty ⟨ f () | true ⊢ ⟨true ⊢ e +! 1⟩ ⟩ in
return { "b" = b; "d" = d; "f" = f}_A
error_empty ⟨ e () | true ⊢ ⟨true ⊢ b + c + d + 1⟩ ⟩
in
let set f : integer = error_empty ⟨ f () | true ⊢ ⟨true ⊢ e + 1⟩ ⟩ in
return { A b = b; d = d; f = f; }
```
```catala-test-inline

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

@ -18,10 +18,10 @@ scope B:
$ catala Dcalc -s B
let scope B (B_in: B_in): B =
let sub_set a.x : bool = error_empty ⟨true ⊢ false⟩ in
let call result : A = A { "x_in" = a.x}_A_in in
let sub_get a.y : integer = result."y" in
let call result : A {y: integer} = A { A_in x_in = a.x; } in
let sub_get a.y : integer = result.y in
let assert _ : unit = assert (error_empty (a.y = 1)) in
return {}_B
return {B}
```
```catala-test-inline

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

@ -25,10 +25,10 @@ $ catala Dcalc -s B
let scope B (B_in: B_in): B =
let sub_set a.a : unit → integer = λ (_: unit) → ∅ in
let sub_set a.b : integer = error_empty ⟨true ⊢ 2⟩ in
let call result : A = A { "a_in" = a.a; "b_in" = a.b}_A_in in
let sub_get a.c : integer = result."c" in
let call result : A {c: integer} = A { A_in a_in = a.a; b_in = a.b; } in
let sub_get a.c : integer = result.c in
let assert _ : unit = assert (error_empty (a.c = 1)) in
return {}_B
return {B}
```
```catala-test-inline

18
tests/test_name_resolution/good/let_in.catala_en
View File

@ -28,8 +28,8 @@ scope S:
```catala-test-inline
$ catala Interpret -s S
[RESULT] Computation successful! Results:
[RESULT] a = { "x" = -2.; "y" = { "y" = false; "z" = -1.}_B}_A
[RESULT] b = { "y" = true; "z" = 42.}_B
[RESULT] a = { A x = -2.; y = { B y = false; z = -1.; }; }
[RESULT] b = { B y = true; z = 42.; }
```
## Check scope of let-in vs scope variable
@ -53,13 +53,13 @@ $ catala Interpret -s S2
```catala-test-inline
$ catala Interpret_Lcalc -s S --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] a = ESome
{
"x" = ESome -2.;
"y" = ESome { "y" = ESome false; "z" = ESome -1.}_B
}_A
[RESULT] b = ESome { "y" = ESome true; "z" = ESome 42.}_B
[RESULT] a =
ESome
{ A
x = ESome -2.;
y = ESome { B y = ESome false; z = ESome -1.; };
}
[RESULT] b = ESome { B y = ESome true; z = ESome 42.; }
```
```catala-test-inline
$ catala Interpret_Lcalc -s S2 --avoid_exceptions --optimize

15
tests/test_name_resolution/good/out_of_order.catala_en
View File

@ -21,14 +21,17 @@ scope S:
```catala-test-inline
$ catala Interpret -s S
[RESULT] Computation successful! Results:
[RESULT] a = { "x" = 0; "y" = { "y" = true; "z" = 0.}_B}_A
[RESULT] b = { "y" = true; "z" = 0.}_B
[RESULT] a = { A x = 0; y = { B y = true; z = 0.; }; }
[RESULT] b = { B y = true; z = 0.; }
```
```catala-test-inline
$ catala Interpret_Lcalc -s S --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] a = ESome
{ "x" = ESome 0; "y" = ESome { "y" = ESome true; "z" = ESome 0.}_B
}_A
[RESULT] b = ESome { "y" = ESome true; "z" = ESome 0.}_B
[RESULT] a =
ESome
{ A
x = ESome 0;
y = ESome { B y = ESome true; z = ESome 0.; };
}
[RESULT] b = ESome { B y = ESome true; z = ESome 0.; }
```

24
tests/test_name_resolution/good/toplevel_defs.catala_en
View File

@ -23,7 +23,7 @@ scope S:
$ catala Interpret -s S
[RESULT] Computation successful! Results:
[RESULT] a = 1946.5744
[RESULT] b = { "y" = true; "z" = 2091.}_A
[RESULT] b = { A y = true; z = 2091.; }
```
## Test toplevel function defs
@ -93,28 +93,28 @@ $ catala Interpret -s S4
$ catala scalc
let glob1_2 = 44.12
let glob3_3 (x_3: money) = return to_rat_mon x_3 +. 10.
let glob3_3 (x_3: money) = return to_rat x_3 + 10.
let glob4_4 (x_4: money) (y_5: decimal) = return to_rat_mon x_4 *. y_5 +. 10.
let glob4_4 (x_4: money) (y_5: decimal) = return to_rat x_4 * y_5 + 10.
let glob5_aux_5 =
decl glob5_7 : any;
let glob5_7 (x_8 : decimal) =
decl y_9 : decimal;
y_9 = 1000.;
return x_8 *. y_9;
return glob5_7 to_rat_int 2 *. 3.
return x_8 * y_9;
return glob5_7 to_rat 2 * 3.
let glob5_6 = glob5_aux_5 ()
let glob2_10 = A {"y": glob1_2 >=. 30., "z": 123. *. 17.}
let glob2_10 = A {"y": glob1_2 >= 30., "z": 123. * 17.}
let S2_6 (S2_in_11: S2_in) =
decl temp_a_13 : any;
try:
decl temp_a_16 : any;
let temp_a_16 (__17 : unit) =
return glob3_3 $44.00 +. 100.;
return glob3_3 $44.00 + 100.;
decl temp_a_14 : any;
let temp_a_14 (__15 : unit) =
return true;
@ -131,7 +131,7 @@ let S3_7 (S3_in_18: S3_in) =
try:
decl temp_a_23 : any;
let temp_a_23 (__24 : unit) =
return 50. +. glob4_4 $44.00 55.;
return 50. + glob4_4 $44.00 55.;
decl temp_a_21 : any;
let temp_a_21 (__22 : unit) =
return true;
@ -148,7 +148,7 @@ let S4_8 (S4_in_25: S4_in) =
try:
decl temp_a_30 : any;
let temp_a_30 (__31 : unit) =
return glob5_6 +. 1.;
return glob5_6 + 1.;
decl temp_a_28 : any;
let temp_a_28 (__29 : unit) =
return true;
@ -165,7 +165,7 @@ let S_9 (S_in_32: S_in) =
try:
decl temp_a_43 : any;
let temp_a_43 (__44 : unit) =
return glob1_2 *. glob1_2;
return glob1_2 * glob1_2;
decl temp_a_41 : any;
let temp_a_41 (__42 : unit) =
return true;
@ -187,7 +187,7 @@ let S_9 (S_in_32: S_in) =
with EmptyError:
temp_b_35 = dead_value_1;
raise NoValueProvided;
decl b_34 : A;
decl b_34 : A {y: bool; z: decimal};
b_34 = temp_b_35;
return S {"a": a_33, "b": b_34}
```
@ -466,7 +466,7 @@ def s(s_in:SIn):
$ catala Interpret_Lcalc -s S --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] a = ESome 1946.5744
[RESULT] b = ESome { "y" = ESome true; "z" = ESome 2091.}_A
[RESULT] b = ESome { A y = ESome true; z = ESome 2091.; }
```
```catala-test-inline
$ catala Interpret_Lcalc -s S2 --avoid_exceptions --optimize

8
tests/test_scope/good/scope_call2.catala_en
View File

@ -21,12 +21,12 @@ scope Titi:
```catala-test-inline
$ catala Interpret -s Titi
[RESULT] Computation successful! Results:
[RESULT] fizz = { "foo" = 1213}_Toto
[RESULT] fuzz = { "foo" = 1323}_Toto
[RESULT] fizz = { Toto foo = 1213; }
[RESULT] fuzz = { Toto foo = 1323; }
```
```catala-test-inline
$ catala Interpret_Lcalc -s Titi --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] fizz = ESome { "foo" = ESome 1213}_Toto
[RESULT] fuzz = ESome { "foo" = ESome 1323}_Toto
[RESULT] fizz = ESome { Toto foo = ESome 1213; }
[RESULT] fuzz = ESome { Toto foo = ESome 1323; }
```

51
tests/test_scope/good/scope_call3.catala_en
View File

@ -34,7 +34,7 @@ $ catala Interpret -t -s HousingComputation
│ ‾
[LOG] → RentComputation.direct
[LOG] ≔ RentComputation.direct.input: {}_RentComputation_in
[LOG] ≔ RentComputation.direct.input: {RentComputation_in}
[LOG] ≔ RentComputation.g: <function>
[LOG] ≔ RentComputation.f: <function>
[LOG] ☛ Definition applied:
@ -43,7 +43,7 @@ $ catala Interpret -t -s HousingComputation
7 │ definition f of x equals (output of RentComputation).f of x
│ ‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾‾
[LOG] ≔ RentComputation.direct.output: { "f" = λ (param0: integer) → { "f" = λ (x: integer) → error_empty ⟨true ⊢ (λ (x1: integer) → error_empty ⟨true ⊢ x1 +! 1⟩) (x +! 1)⟩ }_RentComputation."f" param0 }_RentComputation
[LOG] ≔ RentComputation.direct.output: { RentComputation f = λ (param0: integer) → { RentComputation f = λ (x: integer) → error_empty ⟨true ⊢ (λ (x1: integer) → error_empty ⟨true ⊢ x1 + 1⟩) (x + 1)⟩; }. f param0; }
[LOG] ← RentComputation.direct
[LOG] → RentComputation.f
[LOG] ≔ RentComputation.f.input0: 1
@ -69,28 +69,29 @@ $ catala Interpret -t -s HousingComputation
[LOG] ← HousingComputation.f
[LOG] ≔ HousingComputation.result: 3
[RESULT] Computation successful! Results:
[RESULT] f =
λ (x: integer) →
error_empty
⟨true ⊢
(let result : RentComputation =
(λ (RentComputation_in: RentComputation_in) →
let g : integer → integer =
λ (x1: integer) →
error_empty ⟨true ⊢ x1 +! 1⟩
in
let f : integer → integer =
λ (x1: integer) →
error_empty ⟨true ⊢ g (x1 +! 1)⟩
in
{ "f" = f}_RentComputation)
{}_RentComputation_in
in
let result1 : RentComputation =
{ "f" = λ (param0: integer) → result."f" param0
}_RentComputation
in
if true then result1 else result1)."f"
x⟩
[RESULT] f = λ (x: integer) →
error_empty
⟨true
⊢ (let result : RentComputation =
(λ (RentComputation_in: RentComputation_in) →
let g : integer → integer =
λ (x1: integer) →
error_empty ⟨true ⊢ x1 + 1⟩
in
let f : integer → integer =
λ (x1: integer) →
error_empty ⟨true ⊢ g (x1 + 1)⟩
in
{ RentComputation f = f; })
{RentComputation_in}
in
let result1 : RentComputation =
{ RentComputation
f = λ (param0: integer) → result.f param0;
}
in
if true then result1 else result1).
f
x⟩
[RESULT] result = 3
```

62
tests/test_scope/good/scope_call4.catala_en
View File

@ -25,41 +25,39 @@ scope RentComputation:
```catala-test-inline
$ catala Interpret -s RentComputation
[RESULT] Computation successful! Results:
[RESULT] f1 =
λ (x: integer) →
error_empty
⟨true ⊢
let x1 : integer = x +! 1 in
error_empty ⟨true ⊢ x1 +! 1⟩⟩
[RESULT] f2 =
λ (x: integer) →
error_empty
⟨true ⊢
let x1 : integer = x +! 1 in
error_empty ⟨true ⊢ x1 +! 1⟩⟩
[RESULT] f1 = λ (x: integer) →
error_empty
⟨true ⊢ let x1 : integer = x + 1 in
error_empty ⟨true ⊢ x1 + 1⟩⟩
[RESULT] f2 = λ (x: integer) →
error_empty
⟨true ⊢ let x1 : integer = x + 1 in
error_empty ⟨true ⊢ x1 + 1⟩⟩
```
```catala-test-inline
$ catala Interpret_Lcalc -s RentComputation --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] f1 = ESome
(λ (x: integer) → ESome
match
(match (ESome (λ (x1: integer) → ESome (x1 +! 1)))
with
| ENone → (λ (_: unit) → ENone _)
| ESome → (λ (f1: any) → f1 (x +! 1)))
with
| ENone → (λ (f1: any) → raise NoValueProvided)
| ESome → (λ (x1: any) → x1))
[RESULT] f2 = ESome
(λ (x: integer) → ESome
match
(match (ESome (λ (x1: integer) → ESome (x1 +! 1)))
with
| ENone → (λ (_: unit) → ENone _)
| ESome → (λ (f2: any) → f2 (x +! 1)))
with
| ENone → (λ (f2: any) → raise NoValueProvided)
| ESome → (λ (x1: any) → x1))
[RESULT] f1 =
ESome
(λ (x: integer) →
ESome
match
(match (ESome (λ (x1: integer) → ESome (x1 + 1))) with
| ENone _ → ENone _
| ESome f1 → f1 (x + 1))
with
| ENone f1 → raise NoValueProvided
| ESome x1 → x1)
[RESULT] f2 =
ESome
(λ (x: integer) →
ESome
match
(match (ESome (λ (x1: integer) → ESome (x1 + 1))) with
| ENone _ → ENone _
| ESome f2 → f2 (x + 1))
with
| ENone f2 → raise NoValueProvided
| ESome x1 → x1)
```

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

@ -10,9 +10,10 @@ scope Foo:
```catala-test-inline
$ catala Lcalc -s Foo
let scope Foo (Foo_in: Foo_in): Foo =
let scope Foo (Foo_in: Foo_in): Foo {bar: integer} =
let set bar : integer =
try handle_default [ ], (λ (_: unit) → true), (λ (_: unit) → 0)
with EmptyError -> raise NoValueProvided in
return { "bar" = bar}_Foo
with EmptyError -> raise NoValueProvided
in
return { Foo bar = bar; }
```

32
tests/test_struct/good/nested3.catala_en
View File

@ -37,37 +37,33 @@ scope B:
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:
[RESULT] t =
{ "a" = { "x" = 0; "y" = false}_S; "b" = { "x" = 1; "y" = true}_S
}_T
[RESULT] t = { T a = { S x = 0; y = false; }; b = { S x = 1; y = true; }; }
```
```catala-test-inline
$ catala Interpret -s B
[RESULT] Computation successful! Results:
[RESULT] out = 1
[RESULT] t =
{ "a" = { "x" = 0; "y" = false}_S; "b" = { "x" = 1; "y" = true}_S
}_T
[RESULT] t = { T a = { S x = 0; y = false; }; b = { S x = 1; y = true; }; }
```
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] t = ESome
{
"a" = ESome { "x" = ESome 0; "y" = ESome false}_S;
"b" = ESome { "x" = ESome 1; "y" = ESome true}_S
}_T
[RESULT] t =
ESome
{ T
a = ESome { S x = ESome 0; y = ESome false; };
b = ESome { S x = ESome 1; y = ESome true; };
}
```
```catala-test-inline
$ catala Interpret_Lcalc -s B --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] out = ESome 1
[RESULT] t = ESome
{
"a" = ESome { "x" = ESome 0; "y" = ESome false}_S;
"b" = ESome { "x" = ESome 1; "y" = ESome true}_S
}_T
[RESULT] t =
ESome
{ T
a = ESome { S x = ESome 0; y = ESome false; };
b = ESome { S x = ESome 1; y = ESome true; };
}
```

4
tests/test_struct/good/same_name_fields.catala_en
View File

@ -26,7 +26,7 @@ $ catala Interpret -s A
│ ‾‾‾
└─ Article
[RESULT] Computation successful! Results:
[RESULT] x = { "f" = 1}_Foo
[RESULT] x = { Foo f = 1; }
[RESULT] y = 1
```
```catala-test-inline
@ -39,6 +39,6 @@ $ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
│ ‾‾‾
└─ Article
[RESULT] Computation successful! Results:
[RESULT] x = ESome { "f" = ESome 1}_Foo
[RESULT] x = ESome { Foo f = ESome 1; }
[RESULT] y = ESome 1
```

4
tests/test_struct/good/simple.catala_en
View File

@ -20,12 +20,12 @@ scope A:
```catala-test-inline
$ catala Interpret -s A
[RESULT] Computation successful! Results:
[RESULT] s = { "x" = 1; "y" = 2}_S
[RESULT] s = { S x = 1; y = 2; }
[RESULT] z = 3
```
```catala-test-inline
$ catala Interpret_Lcalc -s A --avoid_exceptions --optimize
[RESULT] Computation successful! Results:
[RESULT] s = ESome { "x" = ESome 1; "y" = ESome 2}_S
[RESULT] s = ESome { S x = ESome 1; y = ESome 2; }
[RESULT] z = ESome 3
```

4
tests/test_variable_state/good/subscope.catala_en
View File

@ -35,8 +35,8 @@ $ catala Scopelang -s A
let scope A (foo_bar: integer|context) (foo_baz: integer|internal)
(foo_fizz: integer|internal|output) =
let foo_bar : integer = reentrant or by default ⟨true ⊢ 1⟩;
let foo_baz : integer = ⟨true ⊢ foo_bar +! 1⟩;
let foo_fizz : integer = ⟨true ⊢ foo_baz +! 1⟩
let foo_baz : integer = ⟨true ⊢ foo_bar + 1⟩;
let foo_fizz : integer = ⟨true ⊢ foo_baz + 1⟩
```
```catala-test-inline