From 1208744c6b7488dfe69630115ddaf19e5d786b82 Mon Sep 17 00:00:00 2001 From: Louis Gesbert Date: Thu, 30 Mar 2023 18:53:07 +0200 Subject: [PATCH] EmptyError is no longer a literal it's much simpler to handle it as an AST node, as that makes the literal identical across all AST passes. --- compiler/dcalc/ast.ml | 2 -- compiler/dcalc/ast.mli | 2 -- compiler/dcalc/from_scopelang.ml | 9 +++--- compiler/dcalc/interpreter.ml | 32 +++++++++---------- compiler/dcalc/optimizations.ml | 11 +++---- compiler/desugared/ast.ml | 2 +- compiler/lcalc/ast.ml | 2 -- compiler/lcalc/ast.mli | 2 -- compiler/lcalc/compile_with_exceptions.ml | 2 +- compiler/lcalc/compile_without_exceptions.ml | 4 +-- compiler/scalc/ast.ml | 2 +- compiler/scalc/to_python.ml | 2 +- compiler/scopelang/from_desugared.ml | 10 +++--- compiler/shared_ast/definitions.ml | 20 ++++++------ compiler/shared_ast/expr.ml | 33 +++++++++----------- compiler/shared_ast/expr.mli | 8 +++-- compiler/shared_ast/print.ml | 4 +-- compiler/shared_ast/print.mli | 2 +- compiler/shared_ast/typing.ml | 4 +-- compiler/verification/conditions.ml | 2 +- compiler/verification/z3backend.real.ml | 2 +- 21 files changed, 73 insertions(+), 84 deletions(-) diff --git a/compiler/dcalc/ast.ml b/compiler/dcalc/ast.ml index 89e74c32..3e73d09d 100644 --- a/compiler/dcalc/ast.ml +++ b/compiler/dcalc/ast.ml @@ -17,8 +17,6 @@ open Shared_ast -type lit = dcalc glit - type 'm naked_expr = (dcalc, 'm mark) naked_gexpr and 'm expr = (dcalc, 'm mark) gexpr diff --git a/compiler/dcalc/ast.mli b/compiler/dcalc/ast.mli index 277d78e9..0c0a776a 100644 --- a/compiler/dcalc/ast.mli +++ b/compiler/dcalc/ast.mli @@ -19,8 +19,6 @@ open Shared_ast -type lit = dcalc glit - type 'm naked_expr = (dcalc, 'm mark) naked_gexpr and 'm expr = (dcalc, 'm mark) gexpr diff --git a/compiler/dcalc/from_scopelang.ml b/compiler/dcalc/from_scopelang.ml index 508b0182..cdbd684c 100644 --- a/compiler/dcalc/from_scopelang.ml +++ b/compiler/dcalc/from_scopelang.ml @@ -201,8 +201,8 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) : match Marked.unmark e with | EVar v -> Expr.evar (Var.Map.find v ctx.local_vars) m | ELit - (( LBool _ | LEmptyError | LInt _ | LRat _ | LMoney _ | LUnit | LDate _ - | LDuration _ ) as l) -> + ((LBool _ | LInt _ | LRat _ | LMoney _ | LUnit | LDate _ | LDuration _) as + l) -> Expr.elit l m | EStruct { name; fields } -> let fields = StructField.Map.map (translate_expr ctx) fields in @@ -254,7 +254,7 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) : let expr = match str_field, expr with | Some { scope_input_io = Desugared.Ast.Reentrant, _; _ }, None -> - Some (Expr.unbox (Expr.elit LEmptyError (mark_tany m pos))) + Some (Expr.unbox (Expr.eemptyerror (mark_tany m pos))) | _ -> expr in match str_field, expr with @@ -410,7 +410,7 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) : (Marked.mark (Expr.with_ty m (TStruct sc_sig.scope_sig_output_struct, Expr.pos e)) - (ELit LEmptyError))) + EEmptyError)) (Expr.with_ty m (TStruct sc_sig.scope_sig_output_struct, Expr.pos e)) in (* let result_var = calling_expr in let result_eta_expanded_var = @@ -561,6 +561,7 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) : | EOp { op = Add_dat_dur _; tys } -> Expr.eop (Add_dat_dur ctx.date_rounding) tys m | EOp { op; tys } -> Expr.eop (Operator.translate op) tys m + | EEmptyError -> Expr.eemptyerror m | EErrorOnEmpty e' -> Expr.eerroronempty (translate_expr ctx e') m | EArray es -> Expr.earray (List.map (translate_expr ctx) es) m diff --git a/compiler/dcalc/interpreter.ml b/compiler/dcalc/interpreter.ml index 11de6426..7fe00ac3 100644 --- a/compiler/dcalc/interpreter.ml +++ b/compiler/dcalc/interpreter.ml @@ -23,7 +23,7 @@ module Runtime = Runtime_ocaml.Runtime (** {1 Helpers} *) let is_empty_error (e : 'm Ast.expr) : bool = - match Marked.unmark e with ELit LEmptyError -> true | _ -> false + match Marked.unmark e with EEmptyError -> true | _ -> false let log_indent = ref 0 @@ -150,8 +150,8 @@ and evaluate_operator : (should not happen if the term was well-typed)" in let open Runtime.Oper in - if List.exists (function ELit LEmptyError, _ -> true | _ -> false) args then - ELit LEmptyError + if List.exists (function EEmptyError, _ -> true | _ -> false) args then + EEmptyError else match op, args with | Length, [(EArray es, _)] -> @@ -350,7 +350,7 @@ and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr = (List.length args) | EOp { op; _ } -> Marked.same_mark_as (evaluate_operator ctx op (Expr.pos e) args) e - | ELit LEmptyError -> Marked.same_mark_as (ELit LEmptyError) 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 \ @@ -359,7 +359,7 @@ and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr = | 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 (ELit LEmptyError) e + 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 @@ -377,7 +377,7 @@ and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr = "Invalid field access %a in struct %a (should not happen if the term \ was well-typed)" StructField.format_t field StructName.format_t s) - | ELit LEmptyError -> Marked.same_mark_as (ELit LEmptyError) e + | 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 \ @@ -397,7 +397,7 @@ and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr = e size) | EInj { e = e1; name; cons } -> let e1' = evaluate_expr ctx e1 in - if is_empty_error e then Marked.same_mark_as (ELit LEmptyError) e + 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 @@ -418,7 +418,7 @@ and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr = in let new_e = Marked.same_mark_as (EApp { f = es_n; args = [e1] }) e in evaluate_expr ctx new_e - | ELit LEmptyError -> Marked.same_mark_as (ELit LEmptyError) 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 \ @@ -430,9 +430,9 @@ and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr = | 0 -> ( let just = evaluate_expr ctx just in match Marked.unmark just with - | ELit LEmptyError -> Marked.same_mark_as (ELit LEmptyError) e + | EEmptyError -> Marked.same_mark_as EEmptyError e | ELit (LBool true) -> evaluate_expr ctx cons - | ELit (LBool false) -> Marked.same_mark_as (ELit LEmptyError) e + | 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 \ @@ -450,19 +450,19 @@ and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr = match Marked.unmark (evaluate_expr ctx cond) with | ELit (LBool true) -> evaluate_expr ctx etrue | ELit (LBool false) -> evaluate_expr ctx efalse - | ELit LEmptyError -> Marked.same_mark_as (ELit LEmptyError) e + | 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 (ELit LEmptyError) e + 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' = ELit LEmptyError then + 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)" @@ -515,7 +515,7 @@ and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr = | _ -> Cli.debug_format "%a" (Expr.format ctx) e'; Errors.raise_spanned_error (Expr.pos e') "Assertion failed") - | ELit LEmptyError -> Marked.same_mark_as (ELit LEmptyError) e + | 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 \ @@ -543,7 +543,7 @@ let interpret_program : | TArrow (ty_in, ty_out) -> Expr.make_abs (Array.of_list @@ List.map (fun _ -> Var.make "_") ty_in) - (Bindlib.box (ELit LEmptyError), Expr.with_ty mark_e ty_out) + (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) diff --git a/compiler/dcalc/optimizations.ml b/compiler/dcalc/optimizations.ml index e5332b8e..b914db42 100644 --- a/compiler/dcalc/optimizations.ml +++ b/compiler/dcalc/optimizations.ml @@ -29,7 +29,7 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : 'm expr) : let e = Expr.map ~f:(partial_evaluation ctx) e in let mark = Marked.get_mark e in (* Then reduce the parent node *) - let reduce e = + let reduce (e : 'm expr) = (* Todo: improve the handling of eapp(log,elit) cases here, it obfuscates the matches and the log calls are not preserved, which would be a good property *) @@ -99,9 +99,7 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : 'm expr) : | EDefault { excepts; just; cons } -> ( (* TODO: mechanically prove each of these optimizations correct :) *) let excepts = - List.filter - (fun except -> Marked.unmark except <> ELit LEmptyError) - excepts + List.filter (fun except -> Marked.unmark except <> EEmptyError) excepts (* we can discard the exceptions that are always empty error *) in let value_except_count = @@ -137,7 +135,7 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : 'm expr) : args = [(ELit (LBool false), _)]; } ), _ ) ) -> - ELit LEmptyError + EEmptyError | [], just when not !Cli.avoid_exceptions_flag -> (* without exceptions, a default is just an [if then else] raising an error in the else case. This exception is only valid in the context @@ -145,8 +143,7 @@ let rec partial_evaluation (ctx : partial_evaluation_ctx) (e : 'm expr) : flag to know if we will be compiling using exceptions or the option monad. FIXME: move this optimisation somewhere else to avoid this check *) - EIfThenElse - { cond = just; etrue = cons; efalse = ELit LEmptyError, mark } + EIfThenElse { cond = just; etrue = cons; efalse = EEmptyError, mark } | excepts, just -> EDefault { excepts; just; cons }) | EIfThenElse { diff --git a/compiler/desugared/ast.ml b/compiler/desugared/ast.ml index a46f5a1a..0d5e370a 100644 --- a/compiler/desugared/ast.ml +++ b/compiler/desugared/ast.ml @@ -145,7 +145,7 @@ let empty_rule (parameters : (Uid.MarkedString.info * typ) list Marked.pos option) : rule = { rule_just = Expr.box (ELit (LBool false), Untyped { pos }); - rule_cons = Expr.box (ELit LEmptyError, Untyped { pos }); + rule_cons = Expr.box (EEmptyError, Untyped { pos }); rule_parameter = Option.map (Marked.map_under_mark diff --git a/compiler/lcalc/ast.ml b/compiler/lcalc/ast.ml index a94f73b9..25a8954b 100644 --- a/compiler/lcalc/ast.ml +++ b/compiler/lcalc/ast.ml @@ -17,8 +17,6 @@ open Catala_utils include Shared_ast -type lit = lcalc glit - type 'm naked_expr = (lcalc, 'm mark) naked_gexpr and 'm expr = (lcalc, 'm mark) gexpr diff --git a/compiler/lcalc/ast.mli b/compiler/lcalc/ast.mli index be417680..2f3a8053 100644 --- a/compiler/lcalc/ast.mli +++ b/compiler/lcalc/ast.mli @@ -21,8 +21,6 @@ open Shared_ast (** {1 Abstract syntax tree} *) -type lit = lcalc glit - type 'm naked_expr = (lcalc, 'm mark) naked_gexpr and 'm expr = (lcalc, 'm mark) gexpr diff --git a/compiler/lcalc/compile_with_exceptions.ml b/compiler/lcalc/compile_with_exceptions.ml index 0cc68b97..ac410a43 100644 --- a/compiler/lcalc/compile_with_exceptions.ml +++ b/compiler/lcalc/compile_with_exceptions.ml @@ -77,7 +77,7 @@ and translate_expr (ctx : 'm ctx) (e : 'm D.expr) : 'm A.expr boxed = ((LBool _ | LInt _ | LRat _ | LMoney _ | LUnit | LDate _ | LDuration _) as l) -> Expr.elit l m - | ELit LEmptyError -> Expr.eraise EmptyError m + | EEmptyError -> Expr.eraise EmptyError m | EOp { op; tys } -> Expr.eop (Operator.translate op) tys m | EIfThenElse { cond; etrue; efalse } -> Expr.eifthenelse (translate_expr ctx cond) (translate_expr ctx etrue) diff --git a/compiler/lcalc/compile_without_exceptions.ml b/compiler/lcalc/compile_without_exceptions.ml index 6ee04c66..c2a8b0bf 100644 --- a/compiler/lcalc/compile_without_exceptions.ml +++ b/compiler/lcalc/compile_without_exceptions.ml @@ -182,7 +182,7 @@ let rec translate_and_hoist (ctx : 'm ctx) (e : 'm D.expr) : | EDefault _ -> let v' = Var.make "default_term" in Expr.make_var v' mark, Var.Map.singleton v' e - | ELit LEmptyError -> + | EEmptyError -> let v' = Var.make "empty_litteral" in Expr.make_var v' mark, Var.Map.singleton v' e (* This one is a very special case. It transform an unpure expression @@ -333,7 +333,7 @@ and translate_expr ?(append_esome = true) (ctx : 'm ctx) (e : 'm D.expr) : (Expr.make_var (Var.translate A.handle_default_opt) mark_hoist) [Expr.earray excepts' mark_hoist; just'; cons'] pos - | ELit LEmptyError -> A.make_none mark_hoist + | EEmptyError -> A.make_none mark_hoist | EAssert arg -> let arg' = translate_expr ctx arg in diff --git a/compiler/scalc/ast.ml b/compiler/scalc/ast.ml index 938721ff..a7faed03 100644 --- a/compiler/scalc/ast.ml +++ b/compiler/scalc/ast.ml @@ -36,7 +36,7 @@ and naked_expr = | EStructFieldAccess : expr * StructField.t * StructName.t -> naked_expr | EInj : expr * EnumConstructor.t * EnumName.t -> naked_expr | EArray : expr list -> naked_expr - | ELit : L.lit -> naked_expr + | ELit : lit -> naked_expr | EApp : expr * expr list -> naked_expr | EOp : operator -> naked_expr diff --git a/compiler/scalc/to_python.ml b/compiler/scalc/to_python.ml index 70d3ba5f..78168a50 100644 --- a/compiler/scalc/to_python.ml +++ b/compiler/scalc/to_python.ml @@ -22,7 +22,7 @@ module Runtime = Runtime_ocaml.Runtime module D = Dcalc.Ast module L = Lcalc.Ast -let format_lit (fmt : Format.formatter) (l : L.lit Marked.pos) : unit = +let format_lit (fmt : Format.formatter) (l : lit Marked.pos) : unit = match Marked.unmark l with | LBool true -> Format.pp_print_string fmt "True" | LBool false -> Format.pp_print_string fmt "False" diff --git a/compiler/scopelang/from_desugared.ml b/compiler/scopelang/from_desugared.ml index 721ebf9e..e401c801 100644 --- a/compiler/scopelang/from_desugared.ml +++ b/compiler/scopelang/from_desugared.ml @@ -120,8 +120,8 @@ let rec translate_expr (ctx : ctx) (e : Desugared.Ast.expr) : args ScopeVar.Map.empty) m | ELit - (( LBool _ | LEmptyError | LInt _ | LRat _ | LMoney _ | LUnit | LDate _ - | LDuration _ ) as l) -> + ((LBool _ | LInt _ | LRat _ | LMoney _ | LUnit | LDate _ | LDuration _) as + l) -> Expr.elit l m | EAbs { binder; tys } -> let vars, body = Bindlib.unmbind binder in @@ -159,6 +159,7 @@ let rec translate_expr (ctx : ctx) (e : Desugared.Ast.expr) : (translate_expr ctx efalse) m | EArray args -> Expr.earray (List.map (translate_expr ctx) args) m + | EEmptyError -> Expr.eemptyerror m | EErrorOnEmpty e1 -> Expr.eerroronempty (translate_expr ctx e1) m (** {1 Rule tree construction} *) @@ -292,8 +293,7 @@ let rec rule_tree_to_expr (translate_and_unbox_list base_just_list) (translate_and_unbox_list base_cons_list)) (Expr.elit (LBool false) emark) - (Expr.elit LEmptyError emark) - emark + (Expr.eemptyerror emark) emark in let exceptions = List.map @@ -390,7 +390,7 @@ let translate_def caller. *) then let m = Untyped { pos = Desugared.Ast.ScopeDef.get_position def_info } in - let empty_error = Expr.elit LEmptyError m in + let empty_error = Expr.eemptyerror m in match params with | Some (ps, _) -> let labels, tys = List.split ps in diff --git a/compiler/shared_ast/definitions.ml b/compiler/shared_ast/definitions.ml index 6cb6c7f9..530bbcb9 100644 --- a/compiler/shared_ast/definitions.ml +++ b/compiler/shared_ast/definitions.ml @@ -267,15 +267,14 @@ type except = ConflictError | EmptyError | NoValueProvided | Crash (** Literals are the same throughout compilation except for the [LEmptyError] case which is eliminated midway through. *) -type _ glit = - | LBool : bool -> 'a glit - | LInt : Runtime.integer -> 'a glit - | LRat : Runtime.decimal -> 'a glit - | LMoney : Runtime.money -> 'a glit - | LUnit : 'a glit - | LDate : date -> 'a glit - | LDuration : duration -> 'a glit - | LEmptyError : [> `DefaultTerms ] glit +type lit = + | LBool of bool + | LInt of Runtime.integer + | LRat of Runtime.decimal + | LMoney of Runtime.money + | LUnit + | LDate of date + | LDuration of duration (** Locations are handled differently in [desugared] and [scopelang] *) type 'a glocation = @@ -306,7 +305,7 @@ type ('a, 't) gexpr = (('a, 't) naked_gexpr, 't) Marked.t and ('a, 't) naked_gexpr = (* Constructors common to all ASTs *) - | ELit : 'a glit -> (([< all ] as 'a), 't) naked_gexpr + | ELit : lit -> (([< all ] as 'a), 't) naked_gexpr | EApp : { f : ('a, 't) gexpr; args : ('a, 't) gexpr list; @@ -388,6 +387,7 @@ and ('a, 't) naked_gexpr = cons : ('a, 't) gexpr; } -> (([< all > `DefaultTerms ] as 'a), 't) naked_gexpr + | EEmptyError : (([< all > `DefaultTerms ] as 'a), 't) naked_gexpr | EErrorOnEmpty : ('a, 't) gexpr -> (([< all > `DefaultTerms ] as 'a), 't) naked_gexpr diff --git a/compiler/shared_ast/expr.ml b/compiler/shared_ast/expr.ml index d1e581ae..bc9191fd 100644 --- a/compiler/shared_ast/expr.ml +++ b/compiler/shared_ast/expr.ml @@ -101,6 +101,7 @@ let eifthenelse cond etrue efalse = @@ fun cond etrue efalse -> EIfThenElse { cond; etrue; efalse } let eerroronempty e1 = Box.app1 e1 @@ fun e1 -> EErrorOnEmpty e1 +let eemptyerror mark = Marked.mark mark (Bindlib.box EEmptyError) let eraise e1 = Box.app0 @@ ERaise e1 let ecatch body exn handler = @@ -228,6 +229,7 @@ let map | EAssert e1 -> eassert (f e1) m | EDefault { excepts; just; cons } -> edefault (List.map f excepts) (f just) (f cons) m + | EEmptyError -> eemptyerror m | EErrorOnEmpty e1 -> eerroronempty (f e1) m | ECatch { body; exn; handler } -> ecatch (f body) exn (f handler) m | ERaise exn -> eraise exn m @@ -259,7 +261,7 @@ let shallow_fold (acc : 'acc) : 'acc = let lfold x acc = List.fold_left (fun acc x -> f x acc) acc x in match Marked.unmark e with - | ELit _ | EOp _ | EVar _ | ERaise _ | ELocation _ -> acc + | ELit _ | EOp _ | EVar _ | ERaise _ | ELocation _ | EEmptyError -> acc | EApp { f = e; args } -> acc |> f e |> lfold args | EArray args -> acc |> lfold args | EAbs _ -> acc @@ -334,6 +336,7 @@ let map_gather let acc2, just = f just in let acc3, cons = f cons in join (join acc1 acc2) acc3, edefault excepts just cons m + | EEmptyError -> acc, eemptyerror m | EErrorOnEmpty e -> let acc, e = f e in acc, eerroronempty e m @@ -396,27 +399,23 @@ let is_value (type a) (e : (a, _) gexpr) = | ELit _ | EAbs _ | EOp _ | ERaise _ -> true | _ -> false -let equal_lit (type a) (l1 : a glit) (l2 : a glit) = +let equal_lit (l1 : lit) (l2 : lit) = let open Runtime.Oper in match l1, l2 with | LBool b1, LBool b2 -> not (o_xor b1 b2) - | LEmptyError, LEmptyError -> true | LInt n1, LInt n2 -> o_eq_int_int n1 n2 | LRat r1, LRat r2 -> o_eq_rat_rat r1 r2 | LMoney m1, LMoney m2 -> o_eq_mon_mon m1 m2 | LUnit, LUnit -> true | LDate d1, LDate d2 -> o_eq_dat_dat d1 d2 | LDuration d1, LDuration d2 -> o_eq_dur_dur d1 d2 - | ( ( LBool _ | LEmptyError | LInt _ | LRat _ | LMoney _ | LUnit | LDate _ - | LDuration _ ), - _ ) -> + | (LBool _ | LInt _ | LRat _ | LMoney _ | LUnit | LDate _ | LDuration _), _ -> false -let compare_lit (type a) (l1 : a glit) (l2 : a glit) = +let compare_lit (l1 : lit) (l2 : lit) = let open Runtime.Oper in match l1, l2 with | LBool b1, LBool b2 -> Bool.compare b1 b2 - | LEmptyError, LEmptyError -> 0 | LInt n1, LInt n2 -> if o_lt_int_int n1 n2 then -1 else if o_eq_int_int n1 n2 then 0 else 1 | LRat r1, LRat r2 -> @@ -436,8 +435,6 @@ let compare_lit (type a) (l1 : a glit) (l2 : a glit) = | n -> n) | LBool _, _ -> -1 | _, LBool _ -> 1 - | LEmptyError, _ -> -1 - | _, LEmptyError -> 1 | LInt _, _ -> -1 | _, LInt _ -> 1 | LRat _, _ -> -1 @@ -516,6 +513,7 @@ and equal : type a. (a, 't) gexpr -> (a, 't) gexpr -> bool = | ( EIfThenElse { cond = if1; etrue = then1; efalse = else1 }, EIfThenElse { cond = if2; etrue = then2; efalse = else2 } ) -> equal if1 if2 && equal then1 then2 && equal else1 else2 + | EEmptyError, EEmptyError -> true | EErrorOnEmpty e1, EErrorOnEmpty e2 -> equal e1 e2 | ERaise ex1, ERaise ex2 -> equal_except ex1 ex2 | ( ECatch { body = etry1; exn = ex1; handler = ewith1 }, @@ -544,9 +542,9 @@ and equal : type a. (a, 't) gexpr -> (a, 't) gexpr -> bool = EScopeCall { scope = s2; args = fields2 } ) -> ScopeName.equal s1 s2 && ScopeVar.Map.equal equal fields1 fields2 | ( ( EVar _ | ETuple _ | ETupleAccess _ | EArray _ | ELit _ | EAbs _ | EApp _ - | EAssert _ | EOp _ | EDefault _ | EIfThenElse _ | EErrorOnEmpty _ - | ERaise _ | ECatch _ | ELocation _ | EStruct _ | EDStructAccess _ - | EStructAccess _ | EInj _ | EMatch _ | EScopeCall _ ), + | EAssert _ | EOp _ | EDefault _ | EIfThenElse _ | EEmptyError + | EErrorOnEmpty _ | ERaise _ | ECatch _ | ELocation _ | EStruct _ + | EDStructAccess _ | EStructAccess _ | EInj _ | EMatch _ | EScopeCall _ ), _ ) -> false @@ -623,6 +621,7 @@ let rec compare : type a. (a, _) gexpr -> (a, _) gexpr -> int = compare just1 just2 @@< fun () -> compare cons1 cons2 @@< fun () -> List.compare compare exs1 exs2 + | EEmptyError, EEmptyError -> 0 | EErrorOnEmpty e1, EErrorOnEmpty e2 -> compare e1 e2 | ERaise ex1, ERaise ex2 -> @@ -650,6 +649,7 @@ let rec compare : type a. (a, _) gexpr -> (a, _) gexpr -> int = | EInj _, _ -> -1 | _, EInj _ -> 1 | EAssert _, _ -> -1 | _, EAssert _ -> 1 | EDefault _, _ -> -1 | _, EDefault _ -> 1 + | EEmptyError , _ -> -1 | _, EEmptyError -> 1 | EErrorOnEmpty _, _ -> -1 | _, EErrorOnEmpty _ -> 1 | ERaise _, _ -> -1 | _, ERaise _ -> 1 | ECatch _, _ -> . | _, ECatch _ -> . @@ -674,7 +674,7 @@ let format ?debug decl_ctx ppf e = Print.expr ?debug decl_ctx ppf e let rec size : type a. (a, 't) gexpr -> int = fun e -> match Marked.unmark e with - | EVar _ | ELit _ | EOp _ -> 1 + | EVar _ | ELit _ | EOp _ | EEmptyError -> 1 | ETuple args -> List.fold_left (fun acc arg -> acc + size arg) 1 args | EArray args -> List.fold_left (fun acc arg -> acc + size arg) 1 args | ETupleAccess { e; _ } -> size e + 1 @@ -738,10 +738,7 @@ let make_app e args pos = let empty_thunked_term mark = let silent = Var.make "_" in let pos = mark_pos mark in - make_abs [| silent |] - (Bindlib.box (ELit LEmptyError), mark) - [TLit TUnit, pos] - pos + make_abs [| silent |] (Bindlib.box EEmptyError, mark) [TLit TUnit, pos] pos let make_let_in x tau e1 e2 mpos = make_app (make_abs [| x |] e2 [tau] mpos) [e1] (pos e2) diff --git a/compiler/shared_ast/expr.mli b/compiler/shared_ast/expr.mli index 3ebff562..7b5de158 100644 --- a/compiler/shared_ast/expr.mli +++ b/compiler/shared_ast/expr.mli @@ -49,7 +49,7 @@ val etupleaccess : ('a, 't) boxed_gexpr -> int -> int -> 't -> ('a any, 't) boxed_gexpr val earray : ('a, 't) boxed_gexpr list -> 't -> ('a any, 't) boxed_gexpr -val elit : 'a glit -> 't -> ('a any, 't) boxed_gexpr +val elit : lit -> 't -> ('a any, 't) boxed_gexpr val eabs : (('a, 't) naked_gexpr, ('a, 't) gexpr) Bindlib.mbinder Bindlib.box -> @@ -82,6 +82,8 @@ val eifthenelse : 't -> ('a any, 't) boxed_gexpr +val eemptyerror : 't -> (([< all > `DefaultTerms ] as 'a), 't) boxed_gexpr + val eerroronempty : ('a, 't) boxed_gexpr -> 't -> @@ -324,8 +326,8 @@ val format : (** {2 Analysis and tests} *) -val equal_lit : 'a glit -> 'a glit -> bool -val compare_lit : 'a glit -> 'a glit -> int +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 diff --git a/compiler/shared_ast/print.ml b/compiler/shared_ast/print.ml index 8166d291..85f4f323 100644 --- a/compiler/shared_ast/print.ml +++ b/compiler/shared_ast/print.ml @@ -126,11 +126,10 @@ let rec typ (ctx : decl_ctx option) (fmt : Format.formatter) (ty : typ) : unit = Format.fprintf fmt "@[%a@ %a@]" base_type "collection" typ t1 | TAny -> base_type fmt "any" -let lit (type a) (fmt : Format.formatter) (l : a glit) : unit = +let lit (fmt : Format.formatter) (l : lit) : unit = match l with | LBool b -> lit_style fmt (string_of_bool b) | LInt i -> lit_style fmt (Runtime.integer_to_string i) - | LEmptyError -> lit_style fmt "∅ " | LUnit -> lit_style fmt "()" | LRat i -> lit_style fmt @@ -364,6 +363,7 @@ let rec expr_aux : expr) excepts punctuation "|" expr just punctuation "⊢" expr cons punctuation "⟩" + | EEmptyError -> lit_style fmt "∅ " | EErrorOnEmpty e' -> Format.fprintf fmt "%a@ %a" op_style "error_empty" with_parens e' | EAssert e' -> diff --git a/compiler/shared_ast/print.mli b/compiler/shared_ast/print.mli index 3b0babd1..cb3a9b3c 100644 --- a/compiler/shared_ast/print.mli +++ b/compiler/shared_ast/print.mli @@ -34,7 +34,7 @@ val enum_constructor : Format.formatter -> EnumConstructor.t -> unit 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 -> 'a glit -> unit +val lit : Format.formatter -> lit -> unit val operator : Format.formatter -> 'a operator -> unit val log_entry : Format.formatter -> log_entry -> unit val except : Format.formatter -> except -> unit diff --git a/compiler/shared_ast/typing.ml b/compiler/shared_ast/typing.ml index d197612e..300de4b2 100644 --- a/compiler/shared_ast/typing.ml +++ b/compiler/shared_ast/typing.ml @@ -221,7 +221,7 @@ let handle_type_error ctx e t1 t2 = (Cli.format_with_style [ANSITerminal.blue; ANSITerminal.Bold]) "-->" t2_s () -let lit_type (type a) (lit : a A.glit) : naked_typ = +let lit_type (lit : A.lit) : naked_typ = match lit with | LBool _ -> TLit TBool | LInt _ -> TLit TInt @@ -230,7 +230,6 @@ let lit_type (type a) (lit : a A.glit) : naked_typ = | LDate _ -> TLit TDate | LDuration _ -> TLit TDuration | LUnit -> TLit TUnit - | LEmptyError -> TAny (Any.fresh ()) (** [op_type] and [resolve_overload] are a bit similar, and work on disjoint sets of operators. However, their assumptions are different so we keep the @@ -742,6 +741,7 @@ and typecheck_expr_top_down : e1 in Expr.eassert e1' mark + | A.EEmptyError -> Expr.eemptyerror (ty_mark (TAny (Any.fresh ()))) | A.EErrorOnEmpty e1 -> let e1' = typecheck_expr_top_down ~leave_unresolved ctx env tau e1 in Expr.eerroronempty e1' context_mark diff --git a/compiler/verification/conditions.ml b/compiler/verification/conditions.ml index ec54aa48..754d1667 100644 --- a/compiler/verification/conditions.ml +++ b/compiler/verification/conditions.ml @@ -198,7 +198,7 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : typed expr) : (Marked.get_mark e); ]) (Marked.get_mark e) - | ELit LEmptyError -> Marked.same_mark_as (ELit (LBool false)) e + | EEmptyError -> Marked.same_mark_as (ELit (LBool false)) e | EVar _ (* Per default calculus semantics, you cannot call a function with an argument that evaluates to the empty error. Thus, all variable evaluate to diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml index 606bfe40..9bdde5e3 100644 --- a/compiler/verification/z3backend.real.ml +++ b/compiler/verification/z3backend.real.ml @@ -374,7 +374,6 @@ let translate_lit (ctx : context) (l : lit) : Expr.expr = match l with | LBool b -> if b then Boolean.mk_true ctx.ctx_z3 else Boolean.mk_false ctx.ctx_z3 - | LEmptyError -> failwith "[Z3 encoding] LEmptyError literals not supported" | LInt n -> Arithmetic.Integer.mk_numeral_i ctx.ctx_z3 (Runtime.integer_to_int n) | LRat r -> @@ -785,6 +784,7 @@ and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr = (Boolean.mk_not ctx.ctx_z3 z3_if) z3_else; ] ) + | 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