diff --git a/compiler/dcalc/from_scopelang.ml b/compiler/dcalc/from_scopelang.ml index 3fbe8e3b..ccc26855 100644 --- a/compiler/dcalc/from_scopelang.ml +++ b/compiler/dcalc/from_scopelang.ml @@ -97,7 +97,7 @@ let merge_defaults rewriting *) (Expr.with_ty m_body ~pos:(Expr.mark_pos m_body) ty)) (Array.to_list vars) tys) - pos + tys pos in let ltrue = Expr.elit (LBool true) @@ -119,6 +119,7 @@ let merge_defaults let pos = Expr.mark_pos m in Expr.make_app caller [Expr.elit LUnit (Expr.with_ty m (Mark.add pos (TLit TUnit)))] + [TLit TUnit, pos] pos in let body = @@ -140,7 +141,7 @@ let tag_with_log_entry let m = mark_tany (Mark.get e) (Expr.pos e) in if Cli.globals.trace then - Expr.eapp (Expr.eop (Log (l, markings)) [TAny, Expr.pos e] m) [e] m + Expr.eappop ~op:(Log (l, markings)) ~tys:[TAny, Expr.pos e] ~args:[e] m else e (* In a list of exceptions, it is normally an error if more than a single one @@ -342,7 +343,11 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) : ] in (* calling_expr = scope_function scope_input_struct *) - let calling_expr = Expr.eapp called_func [single_arg] m in + let calling_expr = + Expr.eapp ~f:called_func ~args:[single_arg] + ~tys:[TStruct sc_sig.scope_sig_input_struct, pos] + m + in (* For the purposes of log parsing explained in Runtime.EventParser, we need to wrap this function call in a flurry of log tags. Specifically, we are mascarading this scope call as a function call. In a normal function @@ -389,30 +394,30 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) : let f_markings = [ScopeName.get_info scope; StructField.get_info field] in + let args = + List.mapi + (fun i (param_var, t_in) -> + tag_with_log_entry + (Expr.make_var param_var (Expr.with_ty m t_in)) + (VarDef + { + log_typ = Mark.remove t_in; + log_io_output = false; + log_io_input = OnlyInput; + }) + (f_markings + @ [Mark.add (Expr.pos e) ("input" ^ string_of_int i)])) + (List.combine params_vars ts_in) + in Expr.make_abs (Array.of_list params_vars) (tag_with_log_entry (tag_with_log_entry (Expr.eapp - (tag_with_log_entry original_field_expr BeginCall - f_markings) - (ListLabels.mapi (List.combine params_vars ts_in) - ~f:(fun i (param_var, t_in) -> - tag_with_log_entry - (Expr.make_var param_var - (Expr.with_ty m t_in)) - (VarDef - { - log_typ = Mark.remove t_in; - log_io_output = false; - log_io_input = OnlyInput; - }) - (f_markings - @ [ - Mark.add (Expr.pos e) - ("input" ^ string_of_int i); - ]))) - (Expr.with_ty m t_out)) + ~f: + (tag_with_log_entry original_field_expr BeginCall + f_markings) + ~args ~tys:ts_in (Expr.with_ty m t_out)) (VarDef { log_typ = Mark.remove t_out; @@ -468,7 +473,7 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) : [ScopeName.get_info scope; Mark.add (Expr.pos e) "direct"]) (Expr.pos e)) (Expr.pos e) - | EApp { f; args } -> + | EApp { f; args; tys } -> (* We insert various log calls to record arguments and outputs of user-defined functions belonging to scopes *) let e1_func = translate_expr ctx f in @@ -489,37 +494,36 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) : | m -> tag_with_log_entry e1_func BeginCall m in let new_args = List.map (translate_expr ctx) args in - let input_typs, output_typ = + let input_typs = List.map Mark.remove tys in + let output_typ = (* NOTE: this is a temporary solution, it works because it's assumed that - all function calls are from scope variables. However, this will change - -- for more information see + all function have explicit types. However, this will change -- for more + information see https://github.com/CatalaLang/catala/pull/280#discussion_r898851693. *) - let retrieve_in_and_out_typ_or_any var vars = + let retrieve_out_typ_or_any var vars = let _, typ, _ = ScopeVar.Map.find (Mark.remove var) vars in match typ with - | TArrow (marked_input_typ, marked_output_typ) -> - List.map Mark.remove marked_input_typ, Mark.remove marked_output_typ - | _ -> ListLabels.map new_args ~f:(fun _ -> TAny), TAny + | TArrow (_, marked_output_typ) -> Mark.remove marked_output_typ + | _ -> TAny in match Mark.remove f with | ELocation (ScopelangScopeVar { name = var }) -> - retrieve_in_and_out_typ_or_any var ctx.scope_vars + retrieve_out_typ_or_any var ctx.scope_vars | ELocation (SubScopeVar { alias; var; _ }) -> ctx.subscope_vars |> SubScopeName.Map.find (Mark.remove alias) - |> retrieve_in_and_out_typ_or_any var + |> retrieve_out_typ_or_any var | ELocation (ToplevelVar { name }) -> ( let typ = TopdefName.Map.find (Mark.remove name) ctx.decl_ctx.ctx_topdefs in match Mark.remove typ with - | TArrow (tin, (tout, _)) -> List.map Mark.remove tin, tout + | TArrow (_, (tout, _)) -> tout | _ -> Message.raise_spanned_error (Expr.pos e) "Application of non-function toplevel variable") - | _ -> ListLabels.map new_args ~f:(fun _ -> TAny), TAny + | _ -> TAny in - (* Message.emit_debug "new_args %d, input_typs: %d, input_typs %a" (List.length new_args) (List.length input_typs) (Format.pp_print_list Print.typ_debug) (List.map (Mark.add Pos.no_pos) input_typs); *) @@ -538,8 +542,7 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) : (m @ [Mark.add (Expr.pos e) ("input" ^ string_of_int i)]) | _ -> new_arg) in - - let new_e = Expr.eapp e1_func new_args m in + let new_e = Expr.eapp ~f:e1_func ~args:new_args ~tys m in let new_e = match markings with | [] -> new_e @@ -591,9 +594,12 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm Scopelang.Ast.expr) : let v, _ = TopdefName.Map.find (Mark.remove name) ctx.toplevel_vars in Expr.evar v m else Expr.eexternal ~name:(Mark.map (fun n -> External_value n) name) m - | 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 + | EAppOp { op = Add_dat_dur _; args; tys } -> + let args = List.map (translate_expr ctx) args in + Expr.eappop ~op:(Add_dat_dur ctx.date_rounding) ~args ~tys m + | EAppOp { op; args; tys } -> + let args = List.map (translate_expr ctx) args in + Expr.eappop ~op:(Operator.translate op) ~args ~tys m | ( EVar _ | EAbs _ | ELit _ | EStruct _ | EStructAccess _ | ETuple _ | ETupleAccess _ | EInj _ | EEmptyError | EErrorOnEmpty _ | EArray _ | EIfThenElse _ ) as e -> @@ -818,7 +824,9 @@ let translate_rule in let call_expr = tag_with_log_entry - (Expr.eapp subscope_func [subscope_struct_arg] (mark_tany m pos_call)) + (Expr.eapp ~f:subscope_func ~args:[subscope_struct_arg] + ~tys:[TStruct called_scope_input_struct, Expr.mark_pos m] + (mark_tany m pos_call)) EndCall [ sigma_name, pos_sigma; diff --git a/compiler/dcalc/invariants.ml b/compiler/dcalc/invariants.ml index 36e82d66..2d96730b 100644 --- a/compiler/dcalc/invariants.ml +++ b/compiler/dcalc/invariants.ml @@ -57,7 +57,7 @@ let check_invariant (inv : string * invariant_expr) (p : typed program) : bool = (* Structural invariant: no default can have as type A -> B *) let invariant_default_no_arrow () : string * invariant_expr = - ( __FUNCTION__, + ( "default_no_arrow", fun _ctx e -> match Mark.remove e with | EDefault _ -> begin @@ -67,19 +67,18 @@ let invariant_default_no_arrow () : string * invariant_expr = (* Structural invariant: no partial evaluation *) let invariant_no_partial_evaluation () : string * invariant_expr = - ( __FUNCTION__, + ( "no_partial_evaluation", fun _ctx e -> match Mark.remove e with - | EApp { f = EOp { op = Op.Log _; _ }, _; _ } -> - (* logs are differents. *) Pass - | EApp _ -> begin - match Mark.remove (Expr.ty e) with TArrow _ -> Fail | _ -> Pass - end + | EApp { f; args; _ } -> ( + match Mark.remove (Expr.ty f) with + | TArrow (tl, _) when List.length args = List.length tl -> Pass + | _ -> Fail) | _ -> Ignore ) (* Structural invariant: no function can return an function *) let invariant_no_return_a_function () : string * invariant_expr = - ( __FUNCTION__, + ( "no_return_a_function", fun _ctx e -> match Mark.remove e with | EAbs _ -> begin @@ -90,16 +89,13 @@ let invariant_no_return_a_function () : string * invariant_expr = | _ -> Ignore ) let invariant_app_inversion () : string * invariant_expr = - ( __FUNCTION__, + ( "app_inversion", fun _ctx e -> match Mark.remove e with - | EApp { f = EOp _, _; _ } -> Pass - | EApp { f = EAbs { binder; _ }, _; args } -> + | EApp { f = EAbs { binder; _ }, _; args; _ } -> if Bindlib.mbinder_arity binder = 1 && List.length args = 1 then Pass else Fail | EApp { f = EVar _, _; _ } -> Pass - | EApp { f = EApp { f = EOp { op = Op.Log _; _ }, _; args = _ }, _; _ } -> - Pass | EApp { f = EStructAccess _, _; _ } -> Pass | EApp { f = EExternal _, _; _ } -> Pass | EApp _ -> Fail @@ -107,7 +103,7 @@ let invariant_app_inversion () : string * invariant_expr = (** the arity of constructors when matching is always one. *) let invariant_match_inversion () : string * invariant_expr = - ( __FUNCTION__, + ( "match_inversion", fun _ctx e -> match Mark.remove e with | EMatch { cases; _ } -> @@ -207,7 +203,7 @@ let check_type_root ctx ty = | _ -> false let invariant_typing_defaults () : string * invariant_expr = - ( __FUNCTION__, + ( "typing_defaults", fun ctx e -> if check_type_root ctx (Expr.ty e) then Pass else ( diff --git a/compiler/desugared/disambiguate.ml b/compiler/desugared/disambiguate.ml index 917d4dd5..7403e8be 100644 --- a/compiler/desugared/disambiguate.ml +++ b/compiler/desugared/disambiguate.ml @@ -21,7 +21,7 @@ let expr ctx env e = (* The typer takes care of disambiguating: this consists in: - ensuring [EAbs.tys] doesn't contain any [TAny] - [EDStructAccess.name_opt] is always [Some] *) - (* Intermediate unboxings are fine since the last [untype] will rebox in + (* Intermediate unboxings are fine since the [check_expr] will rebox in depth *) Typing.check_expr ~leave_unresolved:false ctx ~env (Expr.unbox e) diff --git a/compiler/desugared/disambiguate.mli b/compiler/desugared/disambiguate.mli index 95718ade..27ed62b0 100644 --- a/compiler/desugared/disambiguate.mli +++ b/compiler/desugared/disambiguate.mli @@ -18,7 +18,8 @@ in the AST: - it fills the types of arguments in [EAbs] nodes, (untyped ones are - inserted during desugaring, e.g. by `let-in` constructs), + inserted during desugaring, e.g. by `let-in` constructs), as well as + [EApp] and [EAppOp] nodes - it resolves the structure names of [EDStructAccess] nodes. *) val program : Ast.program -> Ast.program diff --git a/compiler/desugared/from_surface.ml b/compiler/desugared/from_surface.ml index ed89d7dc..a56f753c 100644 --- a/compiler/desugared/from_surface.ml +++ b/compiler/desugared/from_surface.ml @@ -34,10 +34,14 @@ module Runtime = Runtime_ocaml.Runtime the operator suffixes for explicit typing. See {!modules: Shared_ast.Operator} for detail. *) -let translate_binop : S.binop -> Pos.t -> Ast.expr boxed = - fun op pos -> +let translate_binop : + S.binop -> Pos.t -> Ast.expr boxed -> Ast.expr boxed -> Ast.expr boxed = + fun op pos lhs rhs -> let op_expr op tys = - Expr.eop op (List.map (Mark.add pos) tys) (Untyped { pos }) + Expr.eappop ~op + ~tys:(List.map (Mark.add pos) tys) + ~args:[lhs; rhs] + (Untyped { pos }) in match op with | S.And -> op_expr And [TLit TBool; TLit TBool] @@ -104,8 +108,10 @@ let translate_binop : S.binop -> Pos.t -> Ast.expr boxed = | S.Neq -> assert false (* desugared already *) | S.Concat -> op_expr Concat [TArray (TAny, pos); TArray (TAny, pos)] -let translate_unop (op : S.unop) pos : Ast.expr boxed = - let op_expr op ty = Expr.eop op [Mark.add pos ty] (Untyped { pos }) in +let translate_unop (op : S.unop) pos arg : Ast.expr boxed = + let op_expr op ty = + Expr.eappop ~op ~tys:[Mark.add pos ty] ~args:[arg] (Untyped { pos }) + in match op with | S.Not -> op_expr Not (TLit TBool) | S.Minus k -> @@ -251,8 +257,8 @@ let rec translate_expr | Binop ((((S.And | S.Or | S.Xor), _) as op), e1, e2) -> check_formula op e1; check_formula op e2; - let op_term = translate_binop (Mark.remove op) (Mark.get op) in - Expr.eapp op_term [rec_helper e1; rec_helper e2] emark + translate_binop (Mark.remove op) (Mark.get op) (rec_helper e1) + (rec_helper e2) | IfThenElse (e_if, e_then, e_else) -> Expr.eifthenelse (rec_helper e_if) (rec_helper e_then) (rec_helper e_else) emark @@ -260,11 +266,8 @@ let rec translate_expr (* Neq is just sugar *) rec_helper (Unop ((S.Not, posn), (Binop ((S.Eq, posn), e1, e2), posn)), pos) | Binop ((op, pos), e1, e2) -> - let op_term = translate_binop op pos in - Expr.eapp op_term [rec_helper e1; rec_helper e2] emark - | Unop ((op, pos), e) -> - let op_term = translate_unop op pos in - Expr.eapp op_term [rec_helper e] emark + translate_binop op pos (rec_helper e1) (rec_helper e2) + | Unop ((op, pos), e) -> translate_unop op pos (rec_helper e) | Literal l -> let lit = match l with @@ -416,8 +419,25 @@ let rec translate_expr in Expr.edstructaccess ~e ~field:(Mark.remove x) ~name_opt:(get_str ctxt path) emark) + | FunCall ((Builtin b, _), [arg]) -> + let op, ty = + match b with + | S.ToDecimal -> Op.ToRat, TAny + | S.ToMoney -> Op.ToMoney, TAny + | S.Round -> Op.Round, TAny + | S.Cardinal -> Op.Length, TArray (TAny, pos) + | S.GetDay -> Op.GetDay, TLit TDate + | S.GetMonth -> Op.GetMonth, TLit TDate + | S.GetYear -> Op.GetYear, TLit TDate + | S.FirstDayOfMonth -> Op.FirstDayOfMonth, TLit TDate + | S.LastDayOfMonth -> Op.LastDayOfMonth, TLit TDate + in + Expr.eappop ~op ~tys:[ty, pos] ~args:[rec_helper arg] emark + | S.Builtin _ -> + Message.raise_spanned_error pos "Invalid use of built-in: needs one operand" | FunCall (f, args) -> - Expr.eapp (rec_helper f) (List.map rec_helper args) emark + let args = List.map rec_helper args in + Expr.eapp ~f:(rec_helper f) ~args ~tys:[] emark | ScopeCall (((path, id), _), fields) -> if scope = None then Message.raise_spanned_error pos @@ -468,10 +488,10 @@ let rec translate_expr in let taus = List.map (fun x -> TAny, Mark.get x) xs in (* This type will be resolved in Scopelang.Desambiguation *) - let fn = + let f = Expr.make_abs (Array.of_list vs) (rec_helper ~local_vars e2) taus pos in - Expr.eapp fn [rec_helper e1] emark + Expr.eapp ~f ~args:[rec_helper e1] ~tys:[] emark | StructLit (((path, s_name), _), fields) -> let ctxt = Name_resolution.module_ctx ctxt path in let s_uid = @@ -606,15 +626,14 @@ let rec translate_expr [TAny, pos] pos in - Expr.eapp - (Expr.eop - (match op with - | S.Map _ -> Map - | S.Filter _ -> Filter - | _ -> assert false) - [TAny, pos; TAny, pos] - emark) - [f_pred; collection] emark + Expr.eappop + ~op: + (match op with + | S.Map _ -> Map + | S.Filter _ -> Filter + | _ -> assert false) + ~tys:[TAny, pos; TAny, pos] + ~args:[f_pred; collection] emark | CollectionOp ( S.AggregateArgExtremum { max; default; f = param_name, predicate }, collection ) -> @@ -640,19 +659,21 @@ let rec translate_expr rely on returning tuples here *) Expr.make_abs [| v1; v2 |] (Expr.eifthenelse - (Expr.eapp - (Expr.eop cmp_op - [TAny, pos_dft; TAny, pos_dft] - (Untyped { pos = pos_dft })) - [Expr.eapp f_pred [x1] emark; Expr.eapp f_pred [x2] emark] + (Expr.eappop ~op:cmp_op + ~tys:[TAny, pos_dft; TAny, pos_dft] + ~args: + [ + Expr.eapp ~f:f_pred ~args:[x1] ~tys:[] emark; + Expr.eapp ~f:f_pred ~args:[x2] ~tys:[] emark; + ] emark) x1 x2 emark) [TAny, pos; TAny, pos] pos in - Expr.eapp - (Expr.eop Reduce [TAny, pos; TAny, pos; TAny, pos] emark) - [reduce_f; default; collection] + Expr.eappop ~op:Reduce + ~tys:[TAny, pos; TAny, pos; TAny, pos] + ~args:[reduce_f; default; collection] emark | CollectionOp (((Exists { predicate } | Forall { predicate }) as op), collection) -> @@ -672,19 +693,17 @@ let rec translate_expr let acc = Expr.make_var acc_var (Untyped { pos = Mark.get param0 }) in Expr.eabs (Expr.bind [| acc_var; param |] - (Expr.eapp (translate_binop op pos) - [acc; rec_helper ~local_vars predicate] - emark)) + (translate_binop op pos acc (rec_helper ~local_vars predicate))) [TAny, pos; TAny, pos] emark in - Expr.eapp - (Expr.eop Fold [TAny, pos; TAny, pos; TAny, pos] emark) - [f; init; collection] emark + Expr.eappop ~op:Fold + ~tys:[TAny, pos; TAny, pos; TAny, pos] + ~args:[f; init; collection] emark | CollectionOp (AggregateExtremum { max; default }, collection) -> let collection = rec_helper collection in let default = rec_helper default in - let op = translate_binop (if max then S.Gt KPoly else S.Lt KPoly) pos in + let op = if max then S.Gt KPoly else S.Lt KPoly in let op_f = (* fun x1 x2 -> if op x1 x2 then x1 else x2 *) let vname = if max then "max" else "min" in @@ -692,13 +711,13 @@ let rec translate_expr let x1 = Expr.make_var v1 emark in let x2 = Expr.make_var v2 emark in Expr.make_abs [| v1; v2 |] - (Expr.eifthenelse (Expr.eapp op [x1; x2] emark) x1 x2 emark) + (Expr.eifthenelse (translate_binop op pos x1 x2) x1 x2 emark) [TAny, pos; TAny, pos] pos in - Expr.eapp - (Expr.eop Reduce [TAny, pos; TAny, pos; TAny, pos] emark) - [op_f; default; collection] + Expr.eappop ~op:Reduce + ~tys:[TAny, pos; TAny, pos; TAny, pos] + ~args:[op_f; default; collection] emark | CollectionOp (AggregateSum { typ }, collection) -> let collection = rec_helper collection in @@ -722,13 +741,13 @@ let rec translate_expr let x1 = Expr.make_var v1 emark in let x2 = Expr.make_var v2 emark in Expr.make_abs [| v1; v2 |] - (Expr.eapp (translate_binop (S.Add KPoly) pos) [x1; x2] emark) + (translate_binop (S.Add KPoly) pos x1 x2) [TAny, pos; TAny, pos] pos in - Expr.eapp - (Expr.eop Reduce [TAny, pos; TAny, pos; TAny, pos] emark) - [op_f; Expr.elit default_lit emark; collection] + Expr.eappop ~op:Reduce + ~tys:[TAny, pos; TAny, pos; TAny, pos] + ~args:[op_f; Expr.elit default_lit emark; collection] emark | MemCollection (member, collection) -> let param_var = Var.make "collection_member" in @@ -739,14 +758,15 @@ let rec translate_expr let acc = Expr.make_var acc_var emark in let f_body = let member = rec_helper member in - Expr.eapp - (Expr.eop Or [TLit TBool, pos; TLit TBool, pos] emark) - [ - Expr.eapp - (Expr.eop Eq [TAny, pos; TAny, pos] emark) - [member; param] emark; - acc; - ] + Expr.eappop ~op:Or + ~tys:[TLit TBool, pos; TLit TBool, pos] + ~args: + [ + Expr.eappop ~op:Eq + ~tys:[TAny, pos; TAny, pos] + ~args:[member; param] emark; + acc; + ] emark in let f = @@ -755,18 +775,9 @@ let rec translate_expr [TLit TBool, pos; TAny, pos] emark in - Expr.eapp - (Expr.eop Fold [TAny, pos; TAny, pos; TAny, pos] emark) - [f; init; collection] emark - | Builtin ToDecimal -> Expr.eop ToRat [TAny, pos] emark - | Builtin ToMoney -> Expr.eop ToMoney [TAny, pos] emark - | Builtin Round -> Expr.eop Round [TAny, pos] emark - | Builtin Cardinal -> Expr.eop Length [TArray (TAny, pos), pos] emark - | Builtin GetDay -> Expr.eop GetDay [TLit TDate, pos] emark - | Builtin GetMonth -> Expr.eop GetMonth [TLit TDate, pos] emark - | Builtin GetYear -> Expr.eop GetYear [TLit TDate, pos] emark - | Builtin FirstDayOfMonth -> Expr.eop FirstDayOfMonth [TLit TDate, pos] emark - | Builtin LastDayOfMonth -> Expr.eop LastDayOfMonth [TLit TDate, pos] emark + Expr.eappop ~op:Fold + ~tys:[TAny, pos; TAny, pos; TAny, pos] + ~args:[f; init; collection] emark and disambiguate_match_and_build_expression (scope : ScopeName.t option) @@ -913,12 +924,9 @@ let merge_conditions (default_pos : Pos.t) : Ast.expr boxed = match precond, cond with | Some precond, Some cond -> - let op_term = - Expr.eop And - [TLit TBool, default_pos; TLit TBool, default_pos] - (Mark.get cond) - in - Expr.eapp op_term [precond; cond] (Mark.get cond) + Expr.eappop ~op:And + ~tys:[TLit TBool, default_pos; TLit TBool, default_pos] + ~args:[precond; cond] (Mark.get cond) | Some precond, None -> Mark.remove precond, Untyped { pos = default_pos } | None, Some cond -> cond | None, None -> Expr.elit (LBool true) (Untyped { pos = default_pos }) @@ -1281,6 +1289,7 @@ let process_topdef let translate_typ t = Name_resolution.process_type ctxt t in let translate_tbase (tbase, m) = translate_typ (Base tbase, m) in let typ = translate_typ def.S.topdef_type in + Message.emit_debug "TTYP: %a@." Print.typ_debug typ; let expr_opt = match def.S.topdef_expr, def.S.topdef_args with | None, _ -> None @@ -1297,6 +1306,17 @@ let process_topdef in let body = translate_expr None None ctxt local_vars e in let args, tys = List.split args_tys in + let () = + match tys with + | [(Data (S.TTuple _), pos)] -> + Message.raise_spanned_error pos + "Defining arguments of a function as a tuple is not supported, \ + please name the individual arguments" + | _ -> () + in + Message.emit_debug "TTYPSS: %a@." + (Format.pp_print_list Print.typ_debug) + (List.map translate_tbase tys); let e = Expr.make_abs (Array.of_list (List.map Mark.remove args)) diff --git a/compiler/lcalc/ast.ml b/compiler/lcalc/ast.ml index 722eca0e..9e5b9f90 100644 --- a/compiler/lcalc/ast.ml +++ b/compiler/lcalc/ast.ml @@ -20,107 +20,3 @@ type 'm naked_expr = (lcalc, 'm) naked_gexpr and 'm expr = (lcalc, 'm) gexpr type 'm program = 'm expr Shared_ast.program - -module OptionMonad = struct - let return ~(mark : 'a mark) e = - Expr.einj ~e ~cons:Expr.some_constr ~name:Expr.option_enum mark - - let empty ~(mark : 'a mark) = - Expr.einj ~e:(Expr.elit LUnit mark) ~cons:Expr.none_constr - ~name:Expr.option_enum mark - - let bind_var ~(mark : 'a mark) f x arg = - let cases = - EnumConstructor.Map.of_list - [ - ( Expr.none_constr, - let x = Var.make "_" in - Expr.eabs - (Expr.bind [| x |] - (Expr.einj ~e:(Expr.evar x mark) ~cons:Expr.none_constr - ~name:Expr.option_enum mark)) - [TLit TUnit, Expr.mark_pos mark] - mark ); - (* | None x -> None x *) - ( Expr.some_constr, - Expr.eabs (Expr.bind [| x |] f) [TAny, Expr.mark_pos mark] mark ) - (*| Some x -> f (where f contains x as a free variable) *); - ] - in - Expr.ematch ~e:arg ~name:Expr.option_enum ~cases mark - - let bind ~(mark : 'a mark) ~(var_name : string) f arg = - let x = Var.make var_name in - (* todo modify*) - bind_var f x arg ~mark - - let bind_cont ~(mark : 'a mark) ~(var_name : string) f arg = - let x = Var.make var_name in - bind_var (f x) x arg ~mark - - let mbind_mvar ~(mark : 'a mark) f xs args = - (* match e1, ..., en with | Some e1', ..., Some en' -> f (e1, ..., en) | _ - -> None *) - ListLabels.fold_left2 xs args ~f:(bind_var ~mark) - ~init:(Expr.eapp f (List.map (fun v -> Expr.evar v mark) xs) mark) - - let mbind ~(mark : 'a mark) ~(var_name : string) f args = - (* match e1, ..., en with | Some e1', ..., Some en' -> f (e1, ..., en) | _ - -> None *) - let vars = - ListLabels.mapi args ~f:(fun i _ -> - Var.make (Format.sprintf "%s_%i" var_name i)) - in - mbind_mvar f vars args ~mark - - let mbind_cont ~(mark : 'a mark) ~(var_name : string) f args = - let vars = - ListLabels.mapi args ~f:(fun i _ -> - Var.make (Format.sprintf "%s_%i" var_name i)) - in - ListLabels.fold_left2 vars args ~f:(bind_var ~mark) ~init:(f vars) - (* mbind_mvar (f vars) vars args ~mark *) - - let mmap_mvar ~(mark : 'a mark) f xs args = - (* match e1, ..., en with | Some e1', ..., Some en' -> f (e1, ..., en) | _ - -> None *) - ListLabels.fold_left2 xs args ~f:(bind_var ~mark) - ~init: - (Expr.einj - ~e:(Expr.eapp f (List.map (fun v -> Expr.evar v mark) xs) mark) - ~cons:Expr.some_constr ~name:Expr.option_enum mark) - - let map_var ~(mark : 'a mark) f x arg = mmap_mvar f [x] [arg] ~mark - - let map ~(mark : 'a mark) ~(var_name : string) f arg = - let x = Var.make var_name in - map_var f x arg ~mark - - let mmap ~(mark : 'a mark) ~(var_name : string) f args = - let vars = - ListLabels.mapi args ~f:(fun i _ -> - Var.make (Format.sprintf "%s_%i" var_name i)) - in - mmap_mvar f vars args ~mark - - let error_on_empty - ~(mark : 'a mark) - ~(var_name : string) - ?(toplevel = false) - arg = - let cases = - EnumConstructor.Map.of_list - [ - ( Expr.none_constr, - let x = Var.make "_" in - Expr.eabs - (Expr.bind [| x |] (Expr.eraise NoValueProvided mark)) - [TAny, Expr.mark_pos mark] - mark ); - (* | None x -> raise NoValueProvided *) - Expr.some_constr, Expr.fun_id ~var_name mark (* | Some x -> x*); - ] - in - if toplevel then Expr.ematch ~e:arg ~name:Expr.option_enum ~cases mark - else Expr.ematch ~e:arg ~name:Expr.option_enum ~cases mark -end diff --git a/compiler/lcalc/ast.mli b/compiler/lcalc/ast.mli index 7129b7ed..f7006f66 100644 --- a/compiler/lcalc/ast.mli +++ b/compiler/lcalc/ast.mli @@ -24,82 +24,3 @@ type 'm naked_expr = (lcalc, 'm) naked_gexpr and 'm expr = (lcalc, 'm) gexpr type 'm program = 'm expr Shared_ast.program - -(** {1 Option-related management}*) - -(** {2 Term building and management for the [option] monad}*) - -module OptionMonad : sig - val return : mark:'m mark -> ('a any, 'm) boxed_gexpr -> ('a, 'm) boxed_gexpr - val empty : mark:'m mark -> ('a any, 'm) boxed_gexpr - - val bind_var : - mark:'m mark -> - ('a any, 'm) boxed_gexpr -> - ('a, 'm) gexpr Var.t -> - ('a, 'm) boxed_gexpr -> - ('a, 'm) boxed_gexpr - - val bind : - mark:'m mark -> - var_name:string -> - ('a any, 'm) boxed_gexpr -> - ('a, 'm) boxed_gexpr -> - ('a, 'm) boxed_gexpr - - val bind_cont : - mark:'m mark -> - var_name:string -> - (('a any, 'm) gexpr Var.t -> ('a, 'm) boxed_gexpr) -> - ('a, 'm) boxed_gexpr -> - ('a, 'm) boxed_gexpr - - val mbind_mvar : - mark:'m mark -> - ('a any, 'm) boxed_gexpr -> - ('a, 'm) gexpr Var.t list -> - ('a, 'm) boxed_gexpr list -> - ('a, 'm) boxed_gexpr - - val mbind : - mark:'m mark -> - var_name:string -> - ('a any, 'm) boxed_gexpr -> - ('a, 'm) boxed_gexpr list -> - ('a, 'm) boxed_gexpr - - val mbind_cont : - mark:'m mark -> - var_name:string -> - (('a any, 'm) gexpr Var.t list -> ('a, 'm) boxed_gexpr) -> - ('a, 'm) boxed_gexpr list -> - ('a, 'm) boxed_gexpr - - val error_on_empty : - mark:'m mark -> - var_name:string -> - ?toplevel:bool -> - ((< exceptions : yes ; .. > as 'a), 'm) boxed_gexpr -> - ('a, 'm) boxed_gexpr - - val map : - mark:'m mark -> - var_name:string -> - ((< exceptions : no ; .. > as 'a), 'm) boxed_gexpr -> - ('a, 'm) boxed_gexpr -> - ('a, 'm) boxed_gexpr - - val mmap_mvar : - mark:'m mark -> - ('a any, 'm) boxed_gexpr -> - ('a, 'm) gexpr Var.t list -> - ('a, 'm) boxed_gexpr list -> - ('a, 'm) boxed_gexpr - - val mmap : - mark:'m mark -> - var_name:string -> - ('a any, 'm) boxed_gexpr -> - ('a, 'm) boxed_gexpr list -> - ('a, 'm) boxed_gexpr -end diff --git a/compiler/lcalc/closure_conversion.ml b/compiler/lcalc/closure_conversion.ml index 89549ff4..f5e6192e 100644 --- a/compiler/lcalc/closure_conversion.ml +++ b/compiler/lcalc/closure_conversion.ml @@ -39,8 +39,7 @@ let rec transform_closures_expr : let m = Mark.get e in match Mark.remove e with | EStruct _ | EStructAccess _ | ETuple _ | ETupleAccess _ | EInj _ | EArray _ - | ELit _ | EExternal _ | EAssert _ | EOp _ | EIfThenElse _ | ERaise _ - | ECatch _ -> + | ELit _ | EExternal _ | EAssert _ | EIfThenElse _ | ERaise _ | ECatch _ -> Expr.map_gather ~acc:Var.Set.empty ~join:Var.Set.union ~f:(transform_closures_expr ctx) e @@ -59,7 +58,8 @@ let rec transform_closures_expr : let e = Expr.eabs (Expr.bind args - (Expr.eapp (Expr.rebox e) arg_vars (Expr.with_ty m tret))) + (Expr.eapp ~f:(Expr.rebox e) ~args:arg_vars ~tys:targs + (Expr.with_ty m tret))) targs m in let boxed = @@ -104,7 +104,7 @@ let rec transform_closures_expr : (free_vars, EnumConstructor.Map.empty) in free_vars, Expr.ematch ~e:new_e ~name ~cases:new_cases m - | EApp { f = EAbs { binder; tys }, e1_pos; args } -> + | EApp { f = EAbs { binder; tys }, e1_pos; args; _ } -> (* let-binding, we should not close these *) let vars, body = Bindlib.unmbind binder in let free_vars, new_body = (transform_closures_expr ctx) body in @@ -120,7 +120,9 @@ let rec transform_closures_expr : args (free_vars, []) in ( free_vars, - Expr.eapp (Expr.eabs new_binder (tys_as_tanys tys) e1_pos) new_args m ) + Expr.eapp + ~f:(Expr.eabs new_binder (tys_as_tanys tys) e1_pos) + ~args:new_args ~tys m ) | EAbs { binder; tys } -> (* λ x.t *) let binder_mark = m in @@ -143,11 +145,9 @@ let rec transform_closures_expr : (* let env = from_closure_env env in let arg0 = env.0 in ... *) let new_closure_body = Expr.make_let_in closure_env_var any_ty - (Expr.eapp - (Expr.eop Operator.FromClosureEnv - [TClosureEnv, binder_pos] - binder_mark) - [Expr.evar closure_env_arg_var binder_mark] + (Expr.eappop ~op:Operator.FromClosureEnv + ~tys:[TClosureEnv, binder_pos] + ~args:[Expr.evar closure_env_arg_var binder_mark] binder_mark) (Expr.make_multiple_let_in (Array.of_list extra_vars_list) @@ -155,9 +155,9 @@ let rec transform_closures_expr : (List.mapi (fun i _ -> Expr.etupleaccess - (Expr.evar closure_env_var binder_mark) - i - (List.length extra_vars_list) + ~e:(Expr.evar closure_env_var binder_mark) + ~index:i + ~size:(List.length extra_vars_list) binder_mark) extra_vars_list) new_body binder_pos) @@ -178,29 +178,27 @@ let rec transform_closures_expr : (Expr.etuple ((Bindlib.box_var code_var, binder_mark) :: [ - Expr.eapp - (Expr.eop Operator.ToClosureEnv - [TAny, Expr.pos e] - (Mark.get e)) - [ - (if extra_vars_list = [] then Expr.elit LUnit binder_mark - else - Expr.etuple - (List.map - (fun extra_var -> - Bindlib.box_var extra_var, binder_mark) - extra_vars_list) - m); - ] + Expr.eappop ~op:Operator.ToClosureEnv + ~tys:[TAny, Expr.pos e] + ~args: + [ + (if extra_vars_list = [] then Expr.elit LUnit binder_mark + else + Expr.etuple + (List.map + (fun extra_var -> + Bindlib.box_var extra_var, binder_mark) + extra_vars_list) + m); + ] (Mark.get e); ]) m) (Expr.pos e) ) - | EApp + | EAppOp { - f = - (EOp { op = HandleDefaultOpt | Fold | Map | Filter | Reduce; _ }, _) - as f; + op = (HandleDefaultOpt | Fold | Map | Filter | Reduce) as op; + tys; args; } -> (* Special case for some operators: its arguments shall remain thunks (which @@ -225,15 +223,16 @@ let rec transform_closures_expr : Var.Set.union free_vars new_free_vars, new_arg :: new_args) args (Var.Set.empty, []) in - free_vars, Expr.eapp (Expr.box f) new_args (Mark.get e) - | EApp { f = EOp _, _; _ } -> - (* This corresponds to an operator call, which we don't want to transform*) + free_vars, Expr.eappop ~op ~tys ~args:new_args (Mark.get e) + | EAppOp _ -> + (* This corresponds to an operator call, which we don't want to transform *) Expr.map_gather ~acc:Var.Set.empty ~join:Var.Set.union ~f:(transform_closures_expr ctx) e - | EApp { f = EVar v, f_m; args } when Var.Map.mem v ctx.globally_bound_vars -> + | EApp { f = EVar v, f_m; args; tys } + when Var.Map.mem v ctx.globally_bound_vars -> (* This corresponds to a scope or toplevel function call, which we don't - want to transform*) + want to transform *) let free_vars, new_args = List.fold_right (fun arg (free_vars, new_args) -> @@ -241,8 +240,8 @@ let rec transform_closures_expr : Var.Set.union free_vars new_free_vars, new_arg :: new_args) args (Var.Set.empty, []) in - free_vars, Expr.eapp (Expr.evar v f_m) new_args m - | EApp { f = e1; args } -> + free_vars, Expr.eapp ~f:(Expr.evar v f_m) ~args:new_args ~tys m + | EApp { f = e1; args; tys } -> let free_vars, new_e1 = (transform_closures_expr ctx) e1 in let code_env_var = Var.make "code_and_env" in let env_var = Var.make "env" in @@ -258,13 +257,18 @@ let rec transform_closures_expr : let m1 = Mark.get e1 in Expr.make_let_in code_var (TAny, Expr.pos e) - (Expr.etupleaccess (Bindlib.box_var code_env_var, m1) 0 2 m) + (Expr.etupleaccess + ~e:(Bindlib.box_var code_env_var, m1) + ~index:0 ~size:2 m) (Expr.make_let_in env_var (TAny, Expr.pos e) - (Expr.etupleaccess (Bindlib.box_var code_env_var, m1) 1 2 m) + (Expr.etupleaccess + ~e:(Bindlib.box_var code_env_var, m1) + ~index:1 ~size:2 m) (Expr.eapp - (Bindlib.box_var code_var, m1) - ((Bindlib.box_var env_var, m1) :: new_args) + ~f:(Bindlib.box_var code_var, m1) + ~args:((Bindlib.box_var env_var, m1) :: new_args) + ~tys:((TClosureEnv, Expr.pos e1) :: tys) m) (Expr.pos e)) (Expr.pos e) @@ -466,7 +470,7 @@ let rec hoist_closures_expr : (collected_closures, EnumConstructor.Map.empty) in collected_closures, Expr.ematch ~e:new_e ~name ~cases:new_cases m - | EApp { f = EAbs { binder; tys }, e1_pos; args } -> + | EApp { f = EAbs { binder; tys }, e1_pos; args; _ } -> (* let-binding, we should not close these *) let vars, body = Bindlib.unmbind binder in let collected_closures, new_body = @@ -483,12 +487,13 @@ let rec hoist_closures_expr : args (collected_closures, []) in ( collected_closures, - Expr.eapp (Expr.eabs new_binder (tys_as_tanys tys) e1_pos) new_args m ) - | EApp + Expr.eapp + ~f:(Expr.eabs new_binder (tys_as_tanys tys) e1_pos) + ~args:new_args ~tys m ) + | EAppOp { - f = - (EOp { op = HandleDefaultOpt | Fold | Map | Filter | Reduce; _ }, _) - as f; + op = (HandleDefaultOpt | Fold | Map | Filter | Reduce) as op; + tys; args; } -> (* Special case for some operators: its arguments closures thunks because if @@ -516,7 +521,7 @@ let rec hoist_closures_expr : new_collected_closures @ collected_closures, new_arg :: new_args) args ([], []) in - collected_closures, Expr.eapp (Expr.box f) new_args (Mark.get e) + collected_closures, Expr.eappop ~op ~args:new_args ~tys (Mark.get e) | EAbs { tys; _ } -> (* this is the closure we want to hoist*) let closure_var = Var.make ("closure_" ^ name_context) in @@ -534,8 +539,8 @@ let rec hoist_closures_expr : ], Expr.make_var closure_var m ) | EApp _ | EStruct _ | EStructAccess _ | ETuple _ | ETupleAccess _ | EInj _ - | EArray _ | ELit _ | EAssert _ | EOp _ | EIfThenElse _ | ERaise _ | ECatch _ - | EVar _ -> + | EArray _ | ELit _ | EAssert _ | EAppOp _ | EIfThenElse _ | ERaise _ + | ECatch _ | EVar _ -> Expr.map_gather ~acc:[] ~join:( @ ) ~f:(hoist_closures_expr name_context) e | EExternal _ -> failwith "unimplemented" | _ -> . diff --git a/compiler/lcalc/compile_with_exceptions.ml b/compiler/lcalc/compile_with_exceptions.ml index e13aacd3..96d60b87 100644 --- a/compiler/lcalc/compile_with_exceptions.ml +++ b/compiler/lcalc/compile_with_exceptions.ml @@ -33,16 +33,15 @@ let rec translate_default in let pos = Expr.mark_pos mark_default in let exceptions = - Expr.make_app - (Expr.eop Op.HandleDefault - [TAny, pos; TAny, pos; TAny, pos] - (Expr.no_mark mark_default)) - [ - Expr.earray exceptions mark_default; - Expr.thunk_term (translate_expr just) (Mark.get just); - Expr.thunk_term (translate_expr cons) (Mark.get cons); - ] - pos + Expr.eappop ~op:Op.HandleDefault + ~tys:[TAny, pos; TAny, pos; TAny, pos] + ~args: + [ + Expr.earray exceptions mark_default; + Expr.thunk_term (translate_expr just) (Mark.get just); + Expr.thunk_term (translate_expr cons) (Mark.get cons); + ] + mark_default in exceptions @@ -57,7 +56,10 @@ and translate_expr (e : 'm D.expr) : 'm A.expr boxed = | EDefault { excepts; just; cons } -> translate_default excepts just cons (Mark.get e) | EPureDefault e -> translate_expr e - | EOp { op; tys } -> Expr.eop (Operator.translate op) tys m + | EAppOp { op; args; tys } -> + Expr.eappop ~op:(Operator.translate op) + ~args:(List.map translate_expr args) + ~tys m | ( ELit _ | EApp _ | EArray _ | EVar _ | EExternal _ | EAbs _ | EIfThenElse _ | ETuple _ | ETupleAccess _ | EInj _ | EAssert _ | EStruct _ | EStructAccess _ | EMatch _ ) as e -> diff --git a/compiler/lcalc/compile_without_exceptions.ml b/compiler/lcalc/compile_without_exceptions.ml index 56176809..98e57ed8 100644 --- a/compiler/lcalc/compile_without_exceptions.ml +++ b/compiler/lcalc/compile_without_exceptions.ml @@ -59,36 +59,55 @@ let rec translate_default let exceptions = List.map translate_expr exceptions in let pos = Expr.mark_pos mark_default in let exceptions = - Expr.make_app - (Expr.eop Op.HandleDefaultOpt - [TAny, pos; TAny, pos; TAny, pos] - (Expr.no_mark mark_default)) - [ - Expr.earray exceptions mark_default; - (* In call-by-value programming languages, as lcalc, arguments are - evalulated before calling the function. Since we don't want to - execute the justification and conclusion while before checking every - exceptions, we need to thunk them. *) - Expr.thunk_term (translate_expr just) (Mark.get just); - Expr.thunk_term (translate_expr cons) (Mark.get cons); - ] - pos + Expr.eappop ~op:Op.HandleDefaultOpt + ~tys:[TAny, pos; TAny, pos; TAny, pos] + ~args: + [ + Expr.earray exceptions mark_default; + (* In call-by-value programming languages, as lcalc, arguments are + evalulated before calling the function. Since we don't want to + execute the justification and conclusion while before checking + every exceptions, we need to thunk them. *) + Expr.thunk_term (translate_expr just) (Mark.get just); + Expr.thunk_term (translate_expr cons) (Mark.get cons); + ] + mark_default in exceptions and translate_expr (e : 'm D.expr) : 'm A.expr boxed = let mark = Mark.get e in match Mark.remove e with - | EEmptyError -> Ast.OptionMonad.empty ~mark + | EEmptyError -> + Expr.einj ~e:(Expr.elit LUnit mark) ~cons:Expr.none_constr + ~name:Expr.option_enum mark | EErrorOnEmpty arg -> - Ast.OptionMonad.error_on_empty ~mark ~var_name:"arg" (translate_expr arg) + let cases = + EnumConstructor.Map.of_list + [ + ( Expr.none_constr, + let x = Var.make "_" in + Expr.eabs + (Expr.bind [| x |] (Expr.eraise NoValueProvided mark)) + [TAny, Expr.mark_pos mark] + mark ); + (* | None x -> raise NoValueProvided *) + Expr.some_constr, Expr.fun_id ~var_name:"arg" mark (* | Some x -> x*); + ] + in + Expr.ematch ~e:(translate_expr arg) ~name:Expr.option_enum ~cases mark | EDefault { excepts; just; cons } -> translate_default excepts just cons (Mark.get e) - | EPureDefault e -> Ast.OptionMonad.return ~mark (translate_expr e) + | EPureDefault e -> + Expr.einj ~e:(translate_expr e) ~cons:Expr.some_constr + ~name:Expr.option_enum mark (* As we need to translate types as well as terms, we cannot simply use [Expr.map] for terms that contains types. *) - | EOp { op; tys } -> - Expr.eop (Operator.translate op) (List.map translate_typ tys) mark + | EAppOp { op; tys; args } -> + Expr.eappop ~op:(Operator.translate op) + ~tys:(List.map translate_typ tys) + ~args:(List.map translate_expr args) + mark | EAbs { binder; tys } -> let vars, body = Bindlib.unmbind binder in let body = translate_expr body in diff --git a/compiler/lcalc/to_ocaml.ml b/compiler/lcalc/to_ocaml.ml index 1d408abb..e549bb1f 100644 --- a/compiler/lcalc/to_ocaml.ml +++ b/compiler/lcalc/to_ocaml.ml @@ -235,9 +235,7 @@ let format_var (fmt : Format.formatter) (v : 'm Var.t) : unit = let needs_parens (e : 'm expr) : bool = match Mark.remove e with - | EApp { f = EAbs _, _; _ } - | ELit (LBool _ | LUnit) - | EVar _ | ETuple _ | EOp _ -> + | EApp { f = EAbs _, _; _ } | ELit (LBool _ | LUnit) | EVar _ | ETuple _ -> false | _ -> true @@ -349,7 +347,7 @@ let rec format_expr (ctx : decl_ctx) (fmt : Format.formatter) (e : 'm expr) : e)) (EnumConstructor.Map.bindings cases) | ELit l -> Format.fprintf fmt "%a" format_lit (Mark.add (Expr.pos e) l) - | EApp { f = EAbs { binder; tys }, _; args } -> + | EApp { f = EAbs { binder; tys }, _; args; _ } -> let xs, body = Bindlib.unmbind binder in let xs_tau = List.map2 (fun x tau -> x, tau) (Array.to_list xs) tys in let xs_tau_arg = List.map2 (fun (x, tau) arg -> x, tau, arg) xs_tau args in @@ -371,14 +369,14 @@ let rec format_expr (ctx : decl_ctx) (fmt : Format.formatter) (e : 'm expr) : xs_tau format_expr body | EApp { - f = EApp { f = EOp { op = Log (BeginCall, info); _ }, _; args = [f] }, _; + f = EAppOp { op = Log (BeginCall, info); args = [f]; _ }, _; args = [arg]; + _; } when Cli.globals.trace -> Format.fprintf fmt "(log_begin_call@ %a@ %a)@ %a" format_uid_list info format_with_parens f format_with_parens arg - | EApp - { f = EOp { op = Log (VarDef var_def_info, info); _ }, _; args = [arg1] } + | EAppOp { op = Log (VarDef var_def_info, info); args = [arg1]; _ } when Cli.globals.trace -> Format.fprintf fmt "(log_variable_definition@ %a@ {io_input=%s;@ io_output=%b}@ (%a)@ %a)" @@ -390,42 +388,35 @@ let rec format_expr (ctx : decl_ctx) (fmt : Format.formatter) (e : 'm expr) : var_def_info.log_io_output typ_embedding_name (var_def_info.log_typ, Pos.no_pos) format_with_parens arg1 - | EApp { f = EOp { op = Log (PosRecordIfTrueBool, _); _ }, m; args = [arg1] } + | EAppOp { op = Log (PosRecordIfTrueBool, _); args = [arg1]; _ } when Cli.globals.trace -> - let pos = Expr.mark_pos m in + let pos = Expr.pos e in Format.fprintf fmt "(log_decision_taken@ @[{filename = \"%s\";@ start_line=%d;@ \ start_column=%d;@ end_line=%d; end_column=%d;@ law_headings=%a}@]@ %a)" (Pos.get_file pos) (Pos.get_start_line pos) (Pos.get_start_column pos) (Pos.get_end_line pos) (Pos.get_end_column pos) format_string_list (Pos.get_law_info pos) format_with_parens arg1 - | EApp { f = EOp { op = Log (EndCall, info); _ }, _; args = [arg1] } - when Cli.globals.trace -> + | EAppOp { op = Log (EndCall, info); args = [arg1]; _ } when Cli.globals.trace + -> Format.fprintf fmt "(log_end_call@ %a@ %a)" format_uid_list info format_with_parens arg1 - | EApp { f = EOp { op = Log _; _ }, _; args = [arg1] } -> + | EAppOp { op = Log _; args = [arg1]; _ } -> Format.fprintf fmt "%a" format_with_parens arg1 - | EApp - { - f = EOp { op = (HandleDefault | HandleDefaultOpt) as op; _ }, pos; - args; - } -> + | EAppOp { op = (HandleDefault | HandleDefaultOpt) as op; args; _ } -> + let pos = Expr.pos e in Format.fprintf fmt "@[%s@ @[{filename = \"%s\";@ start_line=%d;@ \ start_column=%d;@ end_line=%d; end_column=%d;@ law_headings=%a}@]@ %a@]" (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)) - (Pos.get_end_line (Expr.mark_pos pos)) - (Pos.get_end_column (Expr.mark_pos pos)) - format_string_list - (Pos.get_law_info (Expr.mark_pos pos)) + (Pos.get_file pos) (Pos.get_start_line pos) (Pos.get_start_column pos) + (Pos.get_end_line pos) (Pos.get_end_column pos) format_string_list + (Pos.get_law_info pos) (Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ") format_with_parens) args - | EApp { f; args } -> + | EApp { f; args; _ } -> Format.fprintf fmt "@[%a@ %a@]" format_with_parens f (Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ") @@ -435,7 +426,12 @@ let rec format_expr (ctx : decl_ctx) (fmt : Format.formatter) (e : 'm expr) : Format.fprintf fmt "@[ if@ @[%a@]@ then@ @[%a@]@ else@ @[%a@]@]" format_with_parens cond format_with_parens etrue format_with_parens efalse - | EOp { op; _ } -> Format.pp_print_string fmt (Operator.name op) + | EAppOp { op; args; _ } -> + Format.fprintf fmt "@[%s@ %a@]" (Operator.name op) + (Format.pp_print_list + ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ") + format_with_parens) + args | EAssert e' -> Format.fprintf fmt "@[if@ %a@ then@ ()@ else@ raise (AssertionFailed @[ ELit (LBool false), m | ELit (LBool false), m -> ELit (LBool true), m - | EApp { f = EOp { op = Op.Not; _ }, _; args = [(e, _)] }, m -> e, m - | (EApp { f = EOp { op; tys }, mop; args = [e1; e2] }, m) as e -> ( + | EAppOp { op = Op.Not; args = [(e, _)] }, m -> e, m + | (EAppOp { op; tys; args = [e1; e2] }, m) as e -> ( match op with | Op.And -> - ( EApp - { - f = EOp { op = Op.Or; tys }, mop; - args = [bool_negation e1; bool_negation e2]; - }, - m ) + EAppOp { op = Op.Or; tys; args = [bool_negation e1; bool_negation e2] }, m | Op.Or -> - ( EApp - { - f = EOp { op = Op.And; tys }, mop; - args = [bool_negation e1; bool_negation e2]; - }, + ( EAppOp { op = Op.And; tys; args = [bool_negation e1; bool_negation e2] }, m ) | op -> ( match neg_op op with - | Some op -> EApp { f = EOp { op; tys }, mop; args = [e1; e2] }, m + | Some op -> EAppOp { op; tys; args = [e1; e2] }, m | None -> - ( EApp - { - f = EOp { op = Op.Not; tys = [TLit TBool, Expr.mark_pos m] }, m; - args = [e]; - }, + ( EAppOp { op = Op.Not; tys = [TLit TBool, Expr.mark_pos m]; args = [e] }, m ))) | (_, m) as e -> - ( EApp - { - f = EOp { op = Op.Not; tys = [TLit TBool, Expr.mark_pos m] }, m; - args = [e]; - }, - m ) + EAppOp { op = Op.Not; tys = [TLit TBool, Expr.mark_pos m]; args = [e] }, m let rec lazy_eval : decl_ctx -> Env.t -> laziness_level -> expr -> expr * Env.t = @@ -187,35 +169,16 @@ let rec lazy_eval : decl_ctx -> Env.t -> laziness_level -> expr -> expr * Env.t let r, env1 = lazy_eval ctx env1 llevel e in env_elt.reduced <- r, env1; r, Env.join env env1 - | EApp { f; args }, m -> ( + | EAppOp { op; args; tys }, m -> ( if (not llevel.eval_default) && not (List.equal Expr.equal args [ELit LUnit, m]) (* Applications to () encode thunked default terms *) then e0, env else - match eval_to_value env f with - | (EAbs { binder; _ }, _), env -> - let vars, body = Bindlib.unmbind binder in - log "@[@[{"; - let env = - Seq.fold_left2 - (fun env1 var e -> - log "@[LET %a = %a@]@ " Print.var_debug var Expr.format e; - Env.add var e env env1) - env (Array.to_seq vars) (List.to_seq args) - in - log "@]@[IN [%a]@]" (Print.expr ~debug:true ()) body; - let e, env = lazy_eval ctx env llevel body in - log "@]}"; - e, env - | ( ( EOp - { - op = (Op.Map | Op.Filter | Op.Reduce | Op.Fold | Op.Length) as op; - tys; - }, - m ), - env (* when not llevel.eval_op *) ) -> ( + match op with + | (Op.Map | Op.Filter | Op.Reduce | Op.Fold | Op.Length) as op -> ( + (* when not llevel.eval_op *) (* Distribute collection operations to the terms rather than use their runtime implementations *) let arr = List.hd (List.rev args) in @@ -223,27 +186,17 @@ let rec lazy_eval : decl_ctx -> Env.t -> laziness_level -> expr -> expr * Env.t let aty = List.hd (List.rev tys) in match eval_to_value env arr with | (EArray elts, _), env -> - let eapp f e = EApp { f; args = [e] }, m in + let eapp f e = EApp { f; args = [e]; tys = [] }, m in let empty_condition () = (* Is the expression [length(arr) = 0] *) let pos = Expr.mark_pos m in - ( EApp + ( EAppOp { - f = - ( EOp - { - op = Op.Eq_int_int; - tys = [TLit TInt, pos; TLit TInt, pos]; - }, - m ); + op = Op.Eq_int_int; + tys = [TLit TInt, pos; TLit TInt, pos]; args = [ - ( EApp - { - f = EOp { op = Op.Length; tys = [aty] }, m; - args = [arr]; - }, - m ); + EAppOp { op = Op.Length; tys = [aty]; args = [arr] }, m; ELit (LInt (Runtime.integer_of_int 0)), m; ]; }, @@ -274,14 +227,14 @@ let rec lazy_eval : decl_ctx -> Env.t -> laziness_level -> expr -> expr * Env.t | Op.Reduce, [f; _; _], elt0 :: elts -> let e = List.fold_left - (fun acc elt -> EApp { f; args = [acc; elt] }, m) + (fun acc elt -> EApp { f; args = [acc; elt]; tys = [] }, m) elt0 elts in e, env | Op.Fold, [f; base; _], elts -> let e = List.fold_left - (fun acc elt -> EApp { f; args = [acc; elt] }, m) + (fun acc elt -> EApp { f; args = [acc; elt]; tys = [] }, m) base elts in e, env @@ -292,8 +245,8 @@ let rec lazy_eval : decl_ctx -> Env.t -> laziness_level -> expr -> expr * Env.t (* We did a transformation (removing the outer operator), but further evaluation may be needed to guarantee that [llevel] is reached *) lazy_eval ctx env { llevel with eval_match = true } e - | _ -> (EApp { f; args }, m), env) - | ((EOp { op; _ }, m) as f), env -> + | _ -> (EAppOp { op; args; tys }, m), env) + | _ -> let env, args = List.fold_left_map (fun env e -> @@ -301,7 +254,7 @@ let rec lazy_eval : decl_ctx -> Env.t -> laziness_level -> expr -> expr * Env.t env, e) env args in - if not llevel.eval_op then (EApp { f; args }, m), env + if not llevel.eval_op then (EAppOp { op; args; tys }, m), env else let renv = ref env in (* Dirty workaround returning env and conds from evaluate_operator *) @@ -316,10 +269,32 @@ let rec lazy_eval : decl_ctx -> Env.t -> laziness_level -> expr -> expr * Env.t messages so we don't care. *) args in - e, !renv - (* fixme: this forwards eempty *) + e, !renv) + (* fixme: this forwards eempty *) + | EApp { f; args }, m -> ( + if + (not llevel.eval_default) + && not (List.equal Expr.equal args [ELit LUnit, m]) + (* Applications to () encode thunked default terms *) + then e0, env + else + match eval_to_value env f with + | (EAbs { binder; _ }, _), env -> + let vars, body = Bindlib.unmbind binder in + log "@[@[{"; + let env = + Seq.fold_left2 + (fun env1 var e -> + log "@[LET %a = %a@]@ " Print.var_debug var Expr.format e; + Env.add var e env env1) + env (Array.to_seq vars) (List.to_seq args) + in + log "@]@[IN [%a]@]" (Print.expr ~debug:true ()) body; + let e, env = lazy_eval ctx env llevel body in + log "@]}"; + e, env | e, _ -> error e "Invalid apply on %a" Expr.format e) - | (EAbs _ | ELit _ | EOp _ | EEmptyError), _ -> e0, env (* these are values *) + | (EAbs _ | ELit _ | EEmptyError), _ -> e0, env (* these are values *) | (EStruct _ | ETuple _ | EInj _ | EArray _), _ -> if not llevel.eval_struct then e0, env else @@ -358,7 +333,13 @@ let rec lazy_eval : decl_ctx -> Env.t -> laziness_level -> expr -> expr * Env.t concise expression to express that *) let e1, env = lazy_eval ctx env llevel - (EApp { f = EnumConstructor.Map.find cons cases; args = [e1] }, m) + ( EApp + { + f = EnumConstructor.Map.find cons cases; + args = [e1]; + tys = []; + }, + m ) in add_condition ~condition e1, env | e, _ -> error e "Invalid match argument %a" Expr.format e) @@ -559,12 +540,7 @@ let to_graph ctx env expr = let rec aux env g e = (* lazy_eval ctx env (result_level base_vars) e *) match Expr.skip_wrappers e with - | ( EApp - { - f = EOp { op = ToRat_int | ToRat_mon | ToMoney_rat; _ }, _; - args = [arg]; - }, - _ ) -> + | EAppOp { op = ToRat_int | ToRat_mon | ToMoney_rat; args = [arg]; _ }, _ -> aux env g arg (* we skip conversions *) | ELit l, _ -> @@ -576,7 +552,7 @@ let to_graph ctx env expr = let child, env = (Env.find var env).base in let g, child_v = aux env g child in G.add_edge g v child_v, v - | EApp { f = EOp { op = _; _ }, _; args }, _ -> + | EAppOp { op = _; args; _ }, _ -> let v = G.V.create e in let g = G.add_vertex g v in let g, children = List.fold_left_map (aux env) g args in @@ -682,12 +658,8 @@ let program_to_graph in let e = Mark.set m (Expr.skip_wrappers e) in match e with - | ( EApp - { - f = EOp { op = ToRat_int | ToRat_mon | ToMoney_rat; _ }, _; - args = [arg]; - }, - _ ) -> + | EAppOp { op = ToRat_int | ToRat_mon | ToMoney_rat; args = [arg]; tys }, _ + -> aux parent (g, var_vertices, env0) (Mark.set m arg) (* we skip conversions *) | ELit l, _ -> @@ -725,12 +697,7 @@ let program_to_graph let v = G.V.create e in let g = G.add_vertex g v in (g, var_vertices, env), v)) - | ( EApp - { - f = EOp { op = Map | Filter | Reduce | Fold; _ }, _; - args = _ :: args; - }, - _ ) -> + | EAppOp { op = Map | Filter | Reduce | Fold; args = _ :: args; _ }, _ -> (* First argument (which is a function) is ignored *) let v = G.V.create e in let g = G.add_vertex g v in @@ -739,7 +706,7 @@ let program_to_graph in ( (List.fold_left (fun g -> G.add_edge g v) g children, var_vertices, env), v ) - | EApp { f = EOp { op; _ }, _; args = [lhs; rhs] }, _ -> + | EAppOp { op; args = [lhs; rhs]; _ }, _ -> let v = G.V.create e in let g = G.add_vertex g v in let (g, var_vertices, env), lhs = @@ -771,7 +738,7 @@ let program_to_graph (G.E.create v { side = rhs_label; condition = false } rhs) in (g, var_vertices, env), v - | EApp { f = EOp { op = _; _ }, _; args }, _ -> + | EAppOp { op = _; args; _ }, _ -> let v = G.V.create e in let g = G.add_vertex g v in let (g, var_vertices, env), children = @@ -907,8 +874,7 @@ let rec graph_cleanup options g base_vars = (fun v g -> let succ = G.succ g v in match G.V.label v, succ, List.map G.V.label succ with - | (EApp { f = EOp _, _; _ }, _), [v2], [(EApp { f = EOp _, _; _ }, _)] - -> + | (EAppOp _, _), [v2], [(EAppOp _, _)] -> let g = List.fold_left (fun g e -> @@ -965,8 +931,7 @@ let rec graph_cleanup options g base_vars = (fun v g -> let succ = G.succ g v in match G.V.label v, succ, List.map G.V.label succ with - | (EApp { f = EOp _, _; _ }, _), [v2], [(EApp { f = EOp _, _; _ }, _)] - -> + | (EAppOp _, _), [v2], [(EAppOp _, _)] -> let g = List.fold_left (fun g e -> @@ -1254,7 +1219,7 @@ let to_dot lang ppf ctx env base_vars g ~base_src_url = else (* Constants *) [`Style `Filled; `Fillcolor 0x77aaff; `Shape `Note] | EStruct _, _ | EArray _, _ -> [`Shape `Record] - | EApp { f = EOp { op; _ }, _; _ }, _ -> ( + | EAppOp { op; _ }, _ -> ( match op_kind op with | `Sum | `Product | _ -> [`Shape `Box] (* | _ -> [] *)) | _ -> []) diff --git a/compiler/plugins/lazy_interp.ml b/compiler/plugins/lazy_interp.ml index 4dad71f5..5a78dd0e 100644 --- a/compiler/plugins/lazy_interp.ml +++ b/compiler/plugins/lazy_interp.ml @@ -89,7 +89,35 @@ let rec lazy_eval : r; v_env := r, env1); r, Env.join env env1 - | EApp { f; args }, m -> ( + | EAppOp { op; args; tys }, m -> + if + (not llevel.eval_default) + && not (List.equal Expr.equal args [ELit LUnit, m]) + (* Applications to () encode thunked default terms *) + then e0, env + else + let env, args = + List.fold_left_map + (fun env e -> + let e, env = lazy_eval ctx env llevel e in + env, e) + env args + in + if not llevel.eval_op then (EAppOp { op; args; tys }, m), env + else + let renv = ref env in + (* Dirty workaround returning env from evaluate_operator *) + let eval e = + let e, env = lazy_eval ctx !renv llevel e in + renv := env; + e + in + ( Interpreter.evaluate_operator eval op m Cli.En + (* Default language to English but this should not raise any error + messages so we don't care. *) + args, + !renv ) (* fixme: this forwards eempty *) + | EApp { f; args; tys }, m -> ( if (not llevel.eval_default) && not (List.equal Expr.equal args [ELit LUnit, m]) @@ -113,31 +141,8 @@ let rec lazy_eval : let e, env = lazy_eval ctx env llevel body in log "@]}"; e, env - | ((EOp { op; _ }, m) as f), env -> - let env, args = - List.fold_left_map - (fun env e -> - let e, env = lazy_eval ctx env llevel e in - env, e) - env args - in - if not llevel.eval_op then (EApp { f; args }, m), env - else - let renv = ref env in - (* Dirty workaround returning env from evaluate_operator *) - let eval e = - let e, env = lazy_eval ctx !renv llevel e in - renv := env; - e - in - ( Interpreter.evaluate_operator eval op m Cli.En - (* Default language to English but this should not raise any error - messages so we don't care. *) - args, - !renv ) - (* fixme: this forwards eempty *) | e, _ -> error e "Invalid apply on %a" Expr.format e) - | (EAbs _ | ELit _ | EOp _ | EEmptyError), _ -> e0, env (* these are values *) + | (EAbs _ | ELit _ | EEmptyError), _ -> e0, env (* these are values *) | (EStruct _ | ETuple _ | EInj _ | EArray _), _ -> if not llevel.eval_struct then e0, env else @@ -169,7 +174,9 @@ let rec lazy_eval : match eval_to_value env e with | (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) + ( EApp + { f = EnumConstructor.Map.find cons cases; args = [e]; tys = [] }, + m ) | e, _ -> error e "Invalid match argument %a" Expr.format e) | EDefault { excepts; just; cons }, m -> ( let excs = @@ -251,7 +258,7 @@ let interpret_program (prg : ('dcalc, 'm) gexpr program) (scope : ScopeName.t) : (StructName.Map.find scope_arg_struct ctx.ctx_structs)) m in - let e_app = Expr.eapp (Expr.box e) [application_arg] m in + let e_app = Expr.eapp ~f:(Expr.box e) ~args:[application_arg] ~tys:[] m in lazy_eval ctx env { value_level with eval_struct = true; eval_op = false } (Expr.unbox e_app) diff --git a/compiler/scalc/ast.ml b/compiler/scalc/ast.ml index e75b2845..b77a364d 100644 --- a/compiler/scalc/ast.ml +++ b/compiler/scalc/ast.ml @@ -52,7 +52,7 @@ and naked_expr = | EArray : expr list -> naked_expr | ELit : lit -> naked_expr | EApp : expr * expr list -> naked_expr - | EOp : operator -> naked_expr + | EAppOp : operator * expr list -> naked_expr type stmt = | SInnerFuncDef of VarName.t Mark.pos * func diff --git a/compiler/scalc/from_lcalc.ml b/compiler/scalc/from_lcalc.ml index 1b231006..7ec6e25c 100644 --- a/compiler/scalc/from_lcalc.ml +++ b/compiler/scalc/from_lcalc.ml @@ -65,7 +65,7 @@ let rec translate_expr (ctxt : 'm ctxt) (expr : 'm L.expr) : A.block * A.expr = | EInj { e = e1; cons; name } -> let e1_stmts, new_e1 = translate_expr ctxt e1 in e1_stmts, (A.EInj (new_e1, cons, name), Expr.pos expr) - | EApp { f; args } -> + | EApp { f; args; _ } -> let f_stmts, new_f = translate_expr ctxt f in let args_stmts, new_args = List.fold_left @@ -74,8 +74,20 @@ let rec translate_expr (ctxt : 'm ctxt) (expr : 'm L.expr) : A.block * A.expr = arg_stmts @ args_stmts, new_arg :: new_args) ([], []) args in + (* FIXME: what happens if [arg] is not a tuple but reduces to one ? *) let new_args = List.rev new_args in f_stmts @ args_stmts, (A.EApp (new_f, new_args), Expr.pos expr) + | EAppOp { op; args; _ } -> + let op = Operator.translate op in + let args_stmts, new_args = + List.fold_left + (fun (args_stmts, new_args) arg -> + let arg_stmts, new_arg = translate_expr ctxt arg in + arg_stmts @ args_stmts, new_arg :: new_args) + ([], []) args + in + let new_args = List.rev new_args in + args_stmts, (A.EAppOp (op, new_args), Expr.pos expr) | EArray args -> let args_stmts, new_args = List.fold_left @@ -86,7 +98,6 @@ let rec translate_expr (ctxt : 'm ctxt) (expr : 'm L.expr) : A.block * A.expr = in let new_args = List.rev new_args in args_stmts, (A.EArray new_args, Expr.pos expr) - | EOp { op; _ } -> [], (A.EOp (Operator.translate op), Expr.pos expr) | ELit l -> [], (A.ELit l, Expr.pos expr) | _ -> let tmp_var = @@ -121,7 +132,7 @@ and translate_statements (ctxt : 'm ctxt) (block_expr : 'm L.expr) : A.block = (* Assertions are always encapsulated in a unit-typed let binding *) let e_stmts, new_e = translate_expr ctxt e in e_stmts @ [A.SAssert (Mark.remove new_e), Expr.pos block_expr] - | EApp { f = EAbs { binder; tys }, binder_mark; args } -> + | EApp { f = EAbs { binder; tys }, binder_mark; args; _ } -> (* This defines multiple local variables at the time *) let binder_pos = Expr.mark_pos binder_mark in let vars, body = Bindlib.unmbind binder in diff --git a/compiler/scalc/print.ml b/compiler/scalc/print.ml index 24ffdb39..23a2eae1 100644 --- a/compiler/scalc/print.ml +++ b/compiler/scalc/print.ml @@ -66,15 +66,15 @@ let rec format_expr Format.fprintf fmt "@[%a@ %a@]" EnumConstructor.format cons format_expr e | ELit l -> Print.lit fmt l - | EApp ((EOp ((Map | Filter) as op), _), [arg1; arg2]) -> + | EAppOp (((Map | Filter) as op), [arg1; arg2]) -> Format.fprintf fmt "@[%a@ %a@ %a@]" (Print.operator ~debug) op format_with_parens arg1 format_with_parens arg2 - | EApp ((EOp op, _), [arg1; arg2]) -> + | EAppOp (op, [arg1; arg2]) -> Format.fprintf fmt "@[%a@ %a@ %a@]" format_with_parens arg1 (Print.operator ~debug) op format_with_parens arg2 - | EApp ((EOp (Log _), _), [arg1]) when not debug -> + | EAppOp (Log _, [arg1]) when not debug -> Format.fprintf fmt "%a" format_with_parens arg1 - | EApp ((EOp op, _), [arg1]) -> + | EAppOp (op, [arg1]) -> Format.fprintf fmt "@[%a@ %a@]" (Print.operator ~debug) op format_with_parens arg1 | EApp (f, []) -> Format.fprintf fmt "@[%a@ ()@]" format_expr f @@ -84,7 +84,12 @@ let rec format_expr ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ") format_with_parens) args - | EOp op -> Print.operator ~debug fmt op + | EAppOp (op, args) -> + Format.fprintf fmt "@[%a@ %a@]" (Print.operator ~debug) op + (Format.pp_print_list + ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ") + format_with_parens) + args let rec format_statement (decl_ctx : decl_ctx) diff --git a/compiler/scalc/to_python.ml b/compiler/scalc/to_python.ml index 67de06d6..1ba14110 100644 --- a/compiler/scalc/to_python.ml +++ b/compiler/scalc/to_python.ml @@ -307,18 +307,17 @@ let rec format_expression (ctx : decl_ctx) (fmt : Format.formatter) (e : expr) : (fun fmt e -> Format.fprintf fmt "%a" (format_expression ctx) e)) es | ELit l -> Format.fprintf fmt "%a" format_lit (Mark.copy e l) - | EApp ((EOp ((Map | Filter) as op), _), [arg1; arg2]) -> + | EAppOp (((Map | Filter) as op), [arg1; arg2]) -> Format.fprintf fmt "%a(%a,@ %a)" format_op (op, Pos.no_pos) (format_expression ctx) arg1 (format_expression ctx) arg2 - | EApp ((EOp op, _), [arg1; arg2]) -> + | EAppOp (op, [arg1; arg2]) -> Format.fprintf fmt "(%a %a@ %a)" (format_expression ctx) arg1 format_op (op, Pos.no_pos) (format_expression ctx) arg2 - | EApp ((EApp ((EOp (Log (BeginCall, info)), _), [f]), _), [arg]) + | EApp ((EAppOp (Log (BeginCall, info), [f]), _), [arg]) when Cli.globals.trace -> Format.fprintf fmt "log_begin_call(%a,@ %a,@ %a)" format_uid_list info (format_expression ctx) f (format_expression ctx) arg - | EApp ((EOp (Log (VarDef var_def_info, info)), _), [arg1]) - when Cli.globals.trace -> + | EAppOp (Log (VarDef var_def_info, info), [arg1]) when Cli.globals.trace -> Format.fprintf fmt "log_variable_definition(%a,@ LogIO(input_io=InputIO.%s,@ \ output_io=%s),@ %a)" @@ -329,31 +328,30 @@ let rec format_expression (ctx : decl_ctx) (fmt : Format.formatter) (e : expr) : | Runtime.Reentrant -> "Reentrant") (if var_def_info.log_io_output then "True" else "False") (format_expression ctx) arg1 - | EApp ((EOp (Log (PosRecordIfTrueBool, _)), pos), [arg1]) - when Cli.globals.trace -> + | EAppOp (Log (PosRecordIfTrueBool, _), [arg1]) when Cli.globals.trace -> + let pos = Mark.get e in Format.fprintf fmt "log_decision_taken(SourcePosition(filename=\"%s\",@ start_line=%d,@ \ start_column=%d,@ end_line=%d, end_column=%d,@ law_headings=%a), %a)" (Pos.get_file pos) (Pos.get_start_line pos) (Pos.get_start_column pos) (Pos.get_end_line pos) (Pos.get_end_column pos) format_string_list (Pos.get_law_info pos) (format_expression ctx) arg1 - | EApp ((EOp (Log (EndCall, info)), _), [arg1]) when Cli.globals.trace -> + | EAppOp (Log (EndCall, info), [arg1]) when Cli.globals.trace -> Format.fprintf fmt "log_end_call(%a,@ %a)" format_uid_list info (format_expression ctx) arg1 - | EApp ((EOp (Log _), _), [arg1]) -> + | EAppOp (Log _, [arg1]) -> Format.fprintf fmt "%a" (format_expression ctx) arg1 - | EApp ((EOp Not, _), [arg1]) -> + | EAppOp (Not, [arg1]) -> Format.fprintf fmt "%a %a" format_op (Not, Pos.no_pos) (format_expression ctx) arg1 - | EApp - ((EOp ((Minus_int | Minus_rat | Minus_mon | Minus_dur) as op), _), [arg1]) - -> + | EAppOp (((Minus_int | Minus_rat | Minus_mon | Minus_dur) as op), [arg1]) -> Format.fprintf fmt "%a %a" format_op (op, Pos.no_pos) (format_expression ctx) arg1 - | EApp ((EOp op, _), [arg1]) -> + | EAppOp (op, [arg1]) -> Format.fprintf fmt "%a(%a)" format_op (op, Pos.no_pos) (format_expression ctx) arg1 - | EApp ((EOp ((HandleDefault | HandleDefaultOpt) as op), pos), args) -> + | EAppOp (((HandleDefault | HandleDefaultOpt) as op), args) -> + let pos = Mark.get e in Format.fprintf fmt "%a(@[SourcePosition(filename=\"%s\",@ start_line=%d,@ \ start_column=%d,@ end_line=%d, end_column=%d,@ law_headings=%a), %a)@]" @@ -383,7 +381,12 @@ let rec format_expression (ctx : decl_ctx) (fmt : Format.formatter) (e : expr) : ~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ") (format_expression ctx)) args - | EOp op -> Format.fprintf fmt "%a" format_op (op, Pos.no_pos) + | EAppOp (op, args) -> + Format.fprintf fmt "%a(@[%a)@]" format_op (op, Pos.no_pos) + (Format.pp_print_list + ~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ") + (format_expression ctx)) + args let rec format_statement (ctx : decl_ctx) diff --git a/compiler/scalc/to_r.ml b/compiler/scalc/to_r.ml index 9d0d65d5..ef6f8432 100644 --- a/compiler/scalc/to_r.ml +++ b/compiler/scalc/to_r.ml @@ -312,27 +312,26 @@ let rec format_expression (ctx : decl_ctx) (fmt : Format.formatter) (e : expr) : (fun fmt e -> Format.fprintf fmt "%a" (format_expression ctx) e)) es | ELit l -> Format.fprintf fmt "%a" format_lit (Mark.copy e l) - | EApp ((EOp ((Map | Filter) as op), _), [arg1; arg2]) -> + | EAppOp (((Map | Filter) as op), [arg1; arg2]) -> Format.fprintf fmt "%a(%a,@ %a)" format_op (op, Pos.no_pos) (format_expression ctx) arg1 (format_expression ctx) arg2 - | EApp ((EOp op, _), [arg1; arg2]) -> + | EAppOp (op, [arg1; arg2]) -> Format.fprintf fmt "(%a %a@ %a)" (format_expression ctx) arg1 format_op (op, Pos.no_pos) (format_expression ctx) arg2 - | EApp ((EOp Not, _), [arg1]) -> + | EAppOp (Not, [arg1]) -> Format.fprintf fmt "%a %a" format_op (Not, Pos.no_pos) (format_expression ctx) arg1 - | EApp - ((EOp ((Minus_int | Minus_rat | Minus_mon | Minus_dur) as op), _), [arg1]) - -> + | EAppOp (((Minus_int | Minus_rat | Minus_mon | Minus_dur) as op), [arg1]) -> Format.fprintf fmt "%a %a" format_op (op, Pos.no_pos) (format_expression ctx) arg1 - | EApp ((EOp op, _), [arg1]) -> + | EAppOp (op, [arg1]) -> Format.fprintf fmt "%a(%a)" format_op (op, Pos.no_pos) (format_expression ctx) arg1 - | EApp ((EOp HandleDefaultOpt, _), _) -> + | EAppOp (HandleDefaultOpt, _) -> Message.raise_internal_error "R compilation does not currently support the avoiding of exceptions" - | EApp ((EOp (HandleDefault as op), pos), args) -> + | EAppOp ((HandleDefault as op), args) -> + let pos = Mark.get e in Format.fprintf fmt "%a(@[catala_position(filename=\"%s\",@ start_line=%d,@ \ start_column=%d,@ end_line=%d, end_column=%d,@ law_headings=%a), %a)@]" @@ -362,7 +361,12 @@ let rec format_expression (ctx : decl_ctx) (fmt : Format.formatter) (e : expr) : ~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ") (format_expression ctx)) args - | EOp op -> Format.fprintf fmt "%a" format_op (op, Pos.no_pos) + | EAppOp (op, args) -> + Format.fprintf fmt "%a(@[%a)@]" format_op (op, Pos.no_pos) + (Format.pp_print_list + ~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ") + (format_expression ctx)) + args let rec format_statement (ctx : decl_ctx) diff --git a/compiler/scopelang/from_desugared.ml b/compiler/scopelang/from_desugared.ml index 2350e5b9..d454a1e9 100644 --- a/compiler/scopelang/from_desugared.ml +++ b/compiler/scopelang/from_desugared.ml @@ -38,9 +38,10 @@ let tag_with_log_entry (l : log_entry) (markings : Uid.MarkedString.info list) : untyped Ast.expr boxed = if Cli.globals.trace then - Expr.eapp - (Expr.eop (Log (l, markings)) [TAny, Expr.pos e] (Mark.get e)) - [e] (Mark.get e) + Expr.eappop + ~op:(Log (l, markings)) + ~tys:[TAny, Expr.pos e] + ~args:[e] (Mark.get e) else e let rec translate_expr (ctx : ctx) (e : D.expr) : untyped Ast.expr boxed = @@ -120,7 +121,7 @@ let rec translate_expr (ctx : ctx) (e : D.expr) : untyped Ast.expr boxed = (Expr.edefault ~excepts:[] ~just:(Expr.elit (LBool true) m) ~cons: (Expr.epuredefault - (Expr.make_app e' [Expr.evar arg m] pos) + (Expr.make_app e' [Expr.evar arg m] targs pos) m) m) targs pos @@ -130,22 +131,50 @@ let rec translate_expr (ctx : ctx) (e : D.expr) : untyped Ast.expr boxed = ScopeVar.Map.add v' e' args') args ScopeVar.Map.empty) m - | EApp { f = EOp { op; tys }, m1; args } -> + | EApp { f; tys; args } -> ( + (* Detuplification of function arguments *) + let pos = Expr.pos f in + let f = translate_expr ctx f in + match args, tys with + | [arg], [_] -> Expr.eapp ~f ~tys m ~args:[translate_expr ctx arg] + | [(ETuple args, _)], _ -> + assert (List.length args = List.length tys); + Expr.eapp ~f ~tys m ~args:(List.map (translate_expr ctx) args) + | [((EVar _, _) as arg)], ts -> + let size = List.length ts in + let args = + let e = translate_expr ctx arg in + List.init size (fun index -> Expr.etupleaccess ~e ~size ~index m) + in + Expr.eapp ~f ~tys m ~args + | [arg], ts -> + let size = List.length ts in + let v = Var.make "args" in + let e = Expr.evar v (Mark.get arg) in + let args = + List.init size (fun index -> Expr.etupleaccess ~e ~size ~index m) + in + Expr.make_let_in v (TTuple ts, pos) (translate_expr ctx arg) + (Expr.eapp ~f ~tys m ~args) + pos + | args, tys -> + assert (List.length args = List.length tys); + Expr.eapp ~f ~tys m ~args:(List.map (translate_expr ctx) args)) + | EAppOp { op; tys; args } -> let args = List.map (translate_expr ctx) args in Operator.kind_dispatch op - ~monomorphic:(fun op -> Expr.eapp (Expr.eop op tys m1) args m) - ~polymorphic:(fun op -> Expr.eapp (Expr.eop op tys m1) args m) + ~monomorphic:(fun op -> Expr.eappop ~op ~tys ~args m) + ~polymorphic:(fun op -> Expr.eappop ~op ~tys ~args m) ~overloaded:(fun op -> match Operator.resolve_overload ctx.decl_ctx (Mark.add (Expr.pos e) op) tys with - | op, `Straight -> Expr.eapp (Expr.eop op tys m1) args m + | op, `Straight -> Expr.eappop ~op ~tys ~args m | op, `Reversed -> - Expr.eapp (Expr.eop op (List.rev tys) m1) (List.rev args) m) - | EOp _ -> assert false (* Only allowed within [EApp] *) + Expr.eappop ~op ~tys:(List.rev tys) ~args:(List.rev args) m) | ( EStruct _ | EStructAccess _ | ETuple _ | ETupleAccess _ | EInj _ - | EMatch _ | ELit _ | EApp _ | EDefault _ | EPureDefault _ | EIfThenElse _ - | EArray _ | EEmptyError | EErrorOnEmpty _ ) as e -> + | EMatch _ | ELit _ | EDefault _ | EPureDefault _ | EIfThenElse _ | EArray _ + | EEmptyError | EErrorOnEmpty _ ) as e -> Expr.map ~f:(translate_expr ctx) (e, m) (** {1 Rule tree construction} *) diff --git a/compiler/shared_ast/definitions.ml b/compiler/shared_ast/definitions.ml index f18fdffe..3d0903ea 100644 --- a/compiler/shared_ast/definitions.ml +++ b/compiler/shared_ast/definitions.ml @@ -478,10 +478,14 @@ and ('a, 'b, 'm) base_gexpr = | EApp : { f : ('a, 'm) gexpr; args : ('a, 'm) gexpr list; + (** length may be 1 even if arity > 1 in desugared. scopelang performs + detuplification, so length = arity afterwards *) + tys : typ list; (** Set to [[]] before disambiguation *) } -> ('a, < .. >, 'm) base_gexpr - | EOp : { + | EAppOp : { op : 'b operator; + args : ('a, 'm) gexpr list; tys : typ list; } -> ('a, (< .. > as 'b), 'm) base_gexpr @@ -559,6 +563,7 @@ and ('a, 'b, 'm) base_gexpr = | EPureDefault : ('a, 'm) gexpr -> ('a, < defaultTerms : yes ; .. >, 'm) base_gexpr + (** "return" of a pure term, so that it can be typed as [default] *) | EEmptyError : ('a, < defaultTerms : yes ; .. >, 'm) base_gexpr | EErrorOnEmpty : ('a, 'm) gexpr diff --git a/compiler/shared_ast/expr.ml b/compiler/shared_ast/expr.ml index 9817f473..2b88c790 100644 --- a/compiler/shared_ast/expr.ml +++ b/compiler/shared_ast/expr.ml @@ -112,7 +112,7 @@ let evar v mark = Mark.add mark (Bindlib.box_var v) let eexternal ~name mark = Mark.add mark (Bindlib.box (EExternal { name })) let etuple args = Box.appn args @@ fun args -> ETuple args -let etupleaccess e index size = +let etupleaccess ~e ~index ~size = assert (index < size); Box.app1 e @@ fun e -> ETupleAccess { e; index; size } @@ -122,9 +122,11 @@ let elit l mark = Mark.add mark (Bindlib.box (ELit l)) let eabs binder tys mark = Bindlib.box_apply (fun binder -> EAbs { binder; tys }) binder, mark -let eapp f args = Box.app1n f args @@ fun f args -> EApp { f; args } +let eapp ~f ~args ~tys = Box.app1n f args @@ fun f args -> EApp { f; args; tys } let eassert e1 = Box.app1 e1 @@ fun e1 -> EAssert e1 -let eop op tys = Box.app0 @@ EOp { op; tys } + +let eappop ~op ~args ~tys = + Box.appn args @@ fun args -> EAppOp { op; args; tys } let edefault ~excepts ~just ~cons = Box.app2n just cons excepts @@ -273,8 +275,8 @@ let map let m = Mark.get e in match Mark.remove e with | ELit l -> elit l m - | EApp { f = e1; args } -> eapp (f e1) (List.map f args) m - | EOp { op; tys } -> eop op tys m + | EApp { f = e1; args; tys } -> eapp ~f:(f e1) ~args:(List.map f args) ~tys m + | EAppOp { op; tys; args } -> eappop ~op ~tys ~args:(List.map f args) m | EArray args -> earray (List.map f args) m | EVar v -> evar (Var.translate v) m | EExternal { name } -> eexternal ~name m @@ -286,7 +288,7 @@ let map | EIfThenElse { cond; etrue; efalse } -> eifthenelse (f cond) (f etrue) (f efalse) m | ETuple args -> etuple (List.map f args) m - | ETupleAccess { e; index; size } -> etupleaccess (f e) index size m + | ETupleAccess { e; index; size } -> etupleaccess ~e:(f e) ~index ~size m | EInj { name; cons; e } -> einj ~name ~cons ~e:(f e) m | EAssert e1 -> eassert (f e1) m | EDefault { excepts; just; cons } -> @@ -322,10 +324,9 @@ let shallow_fold (acc : 'acc) : 'acc = let lfold x acc = List.fold_left (fun acc x -> f x acc) acc x in match Mark.remove e with - | ELit _ | EOp _ | EVar _ | EExternal _ | ERaise _ | ELocation _ | EEmptyError - -> - acc - | EApp { f = e; args } -> acc |> f e |> lfold args + | ELit _ | EVar _ | EExternal _ | ERaise _ | ELocation _ | EEmptyError -> acc + | EApp { f = e; args; _ } -> acc |> f e |> lfold args + | EAppOp { args; _ } -> acc |> lfold args | EArray args -> acc |> lfold args | EAbs { binder; tys = _ } -> let _, body = Bindlib.unmbind binder in @@ -367,11 +368,13 @@ let map_gather in match Mark.remove e with | ELit l -> acc, elit l m - | EApp { f = e1; args } -> + | EApp { f = e1; args; tys } -> let acc1, f = f e1 in let acc2, args = lfoldmap args in - join acc1 acc2, eapp f args m - | EOp { op; tys } -> acc, eop op tys m + join acc1 acc2, eapp ~f ~args ~tys m + | EAppOp { op; args; tys } -> + let acc, args = lfoldmap args in + acc, eappop ~op ~args ~tys m | EArray args -> let acc, args = lfoldmap args in acc, earray args m @@ -392,7 +395,7 @@ let map_gather acc, etuple args m | ETupleAccess { e; index; size } -> let acc, e = f e in - acc, etupleaccess e index size m + acc, etupleaccess ~e ~index ~size m | EInj { name; cons; e } -> let acc, e = f e in acc, einj ~name ~cons ~e m @@ -473,7 +476,7 @@ let untype e = map_marks ~f:(fun m -> Untyped { pos = mark_pos m }) e let is_value (type a) (e : (a, _) gexpr) = match Mark.remove e with - | ELit _ | EAbs _ | EOp _ | ERaise _ -> true + | ELit _ | EAbs _ | ERaise _ | ECustom _ | EExternal _ -> true | _ -> false let equal_lit (l1 : lit) (l2 : lit) = @@ -596,11 +599,15 @@ and equal : type a. (a, 't) gexpr -> (a, 't) gexpr -> bool = | ELit l1, ELit l2 -> l1 = l2 | EAbs { binder = b1; tys = tys1 }, EAbs { binder = b2; tys = tys2 } -> 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 + | ( EApp { f = e1; args = args1; tys = tys1 }, + EApp { f = e2; args = args2; tys = tys2 } ) -> + equal e1 e2 && equal_list args1 args2 && Type.equal_list tys1 tys2 + | ( EAppOp { op = op1; args = args1; tys = tys1 }, + EAppOp { op = op2; args = args2; tys = tys2 } ) -> + Operator.equal op1 op2 + && equal_list args1 args2 + && Type.equal_list tys1 tys2 | EAssert e1, EAssert e2 -> equal e1 e2 - | EOp { op = op1; tys = tys1 }, EOp { op = op2; tys = tys2 } -> - Operator.equal op1 op2 && Type.equal_list tys1 tys2 | ( EDefault { excepts = exc1; just = def1; cons = cons1 }, EDefault { excepts = exc2; just = def2; cons = cons2 } ) -> equal def1 def2 && equal cons1 cons2 && equal_list exc1 exc2 @@ -640,7 +647,7 @@ and equal : type a. (a, 't) gexpr -> (a, 't) gexpr -> bool = ECustom { obj = obj2; targs = targs2; tret = tret2 } ) -> Type.equal_list targs1 targs2 && Type.equal tret1 tret2 && obj1 == obj2 | ( ( EVar _ | EExternal _ | ETuple _ | ETupleAccess _ | EArray _ | ELit _ - | EAbs _ | EApp _ | EAssert _ | EOp _ | EDefault _ | EPureDefault _ + | EAbs _ | EApp _ | EAppOp _ | EAssert _ | EDefault _ | EPureDefault _ | EIfThenElse _ | EEmptyError | EErrorOnEmpty _ | ERaise _ | ECatch _ | ELocation _ | EStruct _ | EDStructAccess _ | EStructAccess _ | EInj _ | EMatch _ | EScopeCall _ | ECustom _ ), @@ -656,11 +663,13 @@ let rec compare : type a. (a, _) gexpr -> (a, _) gexpr -> int = match[@ocamlformat "disable"] Mark.remove e1, Mark.remove e2 with | ELit l1, ELit l2 -> compare_lit l1 l2 - | EApp {f=f1; args=args1}, EApp {f=f2; args=args2} -> + | EApp {f=f1; args=args1; tys=tys1}, EApp {f=f2; args=args2; tys=tys2} -> compare f1 f2 @@< fun () -> - List.compare compare args1 args2 - | EOp {op=op1; tys=tys1}, EOp {op=op2; tys=tys2} -> + List.compare compare args1 args2 @@< fun () -> + List.compare Type.compare tys1 tys2 + | EAppOp {op=op1; args=args1; tys=tys1}, EAppOp {op=op2; args=args2; tys=tys2} -> Operator.compare op1 op2 @@< fun () -> + List.compare compare args1 args2 @@< fun () -> List.compare Type.compare tys1 tys2 | EArray a1, EArray a2 -> List.compare compare a1 a2 @@ -739,7 +748,7 @@ let rec compare : type a. (a, _) gexpr -> (a, _) gexpr -> int = invalid_arg "Custom block comparison" | ELit _, _ -> -1 | _, ELit _ -> 1 | EApp _, _ -> -1 | _, EApp _ -> 1 - | EOp _, _ -> -1 | _, EOp _ -> 1 + | EAppOp _, _ -> -1 | _, EAppOp _ -> 1 | EArray _, _ -> -1 | _, EArray _ -> 1 | EVar _, _ -> -1 | _, EVar _ -> 1 | EExternal _, _ -> -1 | _, EExternal _ -> 1 @@ -769,24 +778,14 @@ let rec free_vars : ('a, 't) gexpr -> ('a, 't) gexpr Var.Set.t = function Array.fold_right Var.Set.remove vs (free_vars body) | e -> shallow_fold (fun e -> Var.Set.union (free_vars e)) e Var.Set.empty -let rec skip_wrappers : type a. (a, 'm) gexpr -> (a, 'm) gexpr = function - | EApp { f = EOp { op = Log _; _ }, _; args = [e] }, _ -> skip_wrappers e - | 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 - | EPureDefault e, _ -> skip_wrappers e - | e -> e +(* This function is first defined in [Print], only for dependency reasons *) +let skip_wrappers : type a. (a, 'm) gexpr -> (a, 'm) gexpr = Print.skip_wrappers let remove_logging_calls e = let rec f e = let e, m = map ~f e in ( Bindlib.box_apply - (function - | EApp { f = EOp { op = Log _; _ }, _; args = [(arg, _)] } -> arg - | e -> e) + (function EAppOp { op = Log _; args = [(arg, _)]; _ } -> arg | e -> e) e, m ) in @@ -876,7 +875,7 @@ let format ppf e = Print.expr ~debug:false () ppf e let rec size : type a. (a, 't) gexpr -> int = fun e -> match Mark.remove e with - | EVar _ | EExternal _ | ELit _ | EOp _ | EEmptyError | ECustom _ -> 1 + | EVar _ | EExternal _ | ELit _ | EEmptyError | ECustom _ -> 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 @@ -884,8 +883,9 @@ let rec size : type a. (a, 't) gexpr -> int = | EAssert e -> size e + 1 | EErrorOnEmpty e -> size e + 1 | EPureDefault e -> size e + 1 - | EApp { f; args } -> + | EApp { f; args; _ } -> List.fold_left (fun acc arg -> acc + size arg) (1 + size f) args + | EAppOp { args; _ } -> List.fold_left (fun acc arg -> acc + size arg) 2 args | EAbs { binder; _ } -> let _, body = Bindlib.unmbind binder in 1 + size body @@ -921,7 +921,19 @@ let make_abs xs e taus pos = in eabs (bind xs e) taus mark -let make_app e args pos = +let make_tuple el m0 = + match el with + | [] -> etuple [] (with_ty m0 (TTuple [], mark_pos m0)) + | el -> + let m = + fold_marks + (fun posl -> List.hd posl) + (fun ml -> TTuple (List.map (fun t -> t.ty) ml), (List.hd ml).pos) + (List.map (fun e -> Mark.get e) el) + in + etuple el m + +let make_app f args tys pos = let mark = fold_marks (fun _ -> pos) @@ -937,9 +949,9 @@ let make_app e args pos = Message.raise_internal_error "wrong type: found %a while expecting either an Arrow or Any" Print.typ_debug fty.ty)) - (List.map Mark.get (e :: args)) + (List.map Mark.get (f :: args)) in - eapp e args mark + eapp ~f ~args ~tys mark let make_erroronempty e = let mark = @@ -964,28 +976,22 @@ let thunk_term term mark = let empty_thunked_term mark = thunk_term (Bindlib.box EEmptyError, mark) mark let unthunk_term_nobox term mark = - Mark.add mark (EApp { f = term; args = [ELit LUnit, mark] }) + Mark.add mark + (EApp + { + f = term; + args = [ELit LUnit, mark]; + tys = [TLit TUnit, mark_pos mark]; + }) let make_let_in x tau e1 e2 mpos = - make_app (make_abs [| x |] e2 [tau] mpos) [e1] (pos e2) + make_app (make_abs [| x |] e2 [tau] mpos) [e1] [tau] (pos e2) let make_multiple_let_in xs taus e1s e2 mpos = - make_app (make_abs xs e2 taus mpos) e1s (pos e2) + make_app (make_abs xs e2 taus mpos) e1s taus (pos e2) let make_puredefault e = let mark = map_mark (fun pos -> pos) (fun ty -> TDefault ty, Mark.get ty) (Mark.get e) in epuredefault e mark - -let make_tuple el m0 = - match el with - | [] -> etuple [] (with_ty m0 (TTuple [], mark_pos m0)) - | el -> - let m = - fold_marks - (fun posl -> List.hd posl) - (fun ml -> TTuple (List.map (fun t -> t.ty) ml), (List.hd ml).pos) - (List.map (fun e -> Mark.get e) el) - in - etuple el m diff --git a/compiler/shared_ast/expr.mli b/compiler/shared_ast/expr.mli index 0fd5654e..9cc7e0d7 100644 --- a/compiler/shared_ast/expr.mli +++ b/compiler/shared_ast/expr.mli @@ -55,7 +55,11 @@ val subst : val etuple : ('a, 'm) boxed_gexpr list -> 'm mark -> ('a any, 'm) boxed_gexpr val etupleaccess : - ('a, 'm) boxed_gexpr -> int -> int -> 'm mark -> ('a any, 'm) boxed_gexpr + e:('a, 'm) boxed_gexpr -> + index:int -> + size:int -> + 'm mark -> + ('a any, 'm) boxed_gexpr val earray : ('a, 'm) boxed_gexpr list -> 'm mark -> ('a any, 'm) boxed_gexpr val elit : lit -> 'm mark -> ('a any, 'm) boxed_gexpr @@ -67,8 +71,9 @@ val eabs : ('a any, 'm) boxed_gexpr val eapp : - ('a, 'm) boxed_gexpr -> - ('a, 'm) boxed_gexpr list -> + f:('a, 'm) boxed_gexpr -> + args:('a, 'm) boxed_gexpr list -> + tys:typ list -> 'm mark -> ('a any, 'm) boxed_gexpr @@ -77,7 +82,12 @@ val eassert : 'm mark -> ((< assertions : yes ; .. > as 'a), 'm) boxed_gexpr -val eop : 'a operator -> typ list -> 'm mark -> ('a any, 'm) boxed_gexpr +val eappop : + op:'a operator -> + args:('a, 'm) boxed_gexpr list -> + tys:typ list -> + 'm mark -> + ('a any, 'm) boxed_gexpr val edefault : excepts:('a, 'm) boxed_gexpr list -> @@ -319,6 +329,7 @@ val make_abs : val make_app : ('a any, 'm) boxed_gexpr -> ('a, 'm) boxed_gexpr list -> + typ list -> Pos.t -> ('a any, 'm) boxed_gexpr diff --git a/compiler/shared_ast/interpreter.ml b/compiler/shared_ast/interpreter.ml index 810b6b29..72099fe6 100644 --- a/compiler/shared_ast/interpreter.ml +++ b/compiler/shared_ast/interpreter.ml @@ -169,7 +169,7 @@ let rec evaluate_operator (should not happen if the term was well-typed)%a" (Print.operator ~debug:true) op Expr.format - (EApp { f = EOp { op; tys = [] }, m; args }, m) + (EAppOp { op; tys = []; args }, m) in propagate_empty_error_list args @@ fun args -> @@ -193,21 +193,38 @@ let rec evaluate_operator | Map, [f; (EArray es, _)] -> EArray (List.map - (fun e' -> evaluate_expr (Mark.copy e' (EApp { f; args = [e'] }))) + (fun e' -> + evaluate_expr + (Mark.copy e' + (EApp { f; args = [e']; tys = [Expr.maybe_ty (Mark.get e')] }))) es) | Reduce, [_; default; (EArray [], _)] -> Mark.remove default | Reduce, [f; _; (EArray (x0 :: xn), _)] -> Mark.remove (List.fold_left (fun acc x -> - evaluate_expr (Mark.copy f (EApp { f; args = [acc; x] }))) + evaluate_expr + (Mark.copy f + (EApp + { + f; + args = [acc; x]; + tys = + [ + Expr.maybe_ty (Mark.get acc); Expr.maybe_ty (Mark.get x); + ]; + }))) x0 xn) | Concat, [(EArray es1, _); (EArray es2, _)] -> EArray (es1 @ es2) | Filter, [f; (EArray es, _)] -> EArray (List.filter (fun e' -> - match evaluate_expr (Mark.copy e' (EApp { f; args = [e'] })) with + match + evaluate_expr + (Mark.copy e' + (EApp { f; args = [e']; tys = [Expr.maybe_ty (Mark.get e')] })) + with | ELit (LBool b), _ -> b | _ -> Message.raise_spanned_error @@ -219,7 +236,18 @@ let rec evaluate_operator Mark.remove (List.fold_left (fun acc e' -> - evaluate_expr (Mark.copy e' (EApp { f; args = [acc; e'] }))) + evaluate_expr + (Mark.copy e' + (EApp + { + f; + args = [acc; e']; + tys = + [ + Expr.maybe_ty (Mark.get acc); + Expr.maybe_ty (Mark.get e'); + ]; + }))) init es) | (Length | Log _ | Eq | Map | Concat | Filter | Fold | Reduce), _ -> err () | Not, [(ELit (LBool b), _)] -> ELit (LBool (o_not b)) @@ -536,8 +564,9 @@ and val_to_runtime : let rec curry acc = function | [] -> let args = List.rev acc in + let tys = List.map (fun a -> Expr.maybe_ty (Mark.get a)) args in val_to_runtime eval_expr ctx tret - (try eval_expr ctx (EApp { f = v; args }, m) + (try eval_expr ctx (EApp { f = v; args; tys }, m) with CatalaException EmptyError -> raise Runtime.EmptyError) | targ :: targs -> Obj.repr (fun x -> @@ -594,7 +623,7 @@ let rec evaluate_expr : in let o = Runtime.lookup_value runtime_path in runtime_to_val (fun ctx -> evaluate_expr ctx lang) ctx m ty o - | EApp { f = e1; args } -> ( + | EApp { f = e1; args; _ } -> ( let e1 = evaluate_expr ctx lang e1 in let args = List.map (evaluate_expr ctx lang) args in propagate_empty_error e1 @@ -609,7 +638,6 @@ 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 lang) op m lang args | ECustom { obj; targs; tret } -> (* Applies the arguments one by one to the curried form *) List.fold_left2 @@ -624,9 +652,11 @@ let rec evaluate_expr : Message.raise_spanned_error pos "function has not been reduced to a lambda at evaluation (should not \ happen if the term was well-typed") + | EAppOp { op; args; _ } -> + let args = List.map (evaluate_expr ctx lang) args in + evaluate_operator (evaluate_expr ctx lang) op m lang args | EAbs { binder; tys } -> Expr.unbox (Expr.eabs (Bindlib.box binder) tys m) | ELit _ as e -> Mark.add m e - | EOp { op; tys } -> Expr.unbox (Expr.eop (Operator.translate op) tys m) (* | EAbs _ as e -> Marked.mark m e (* these are values *) *) | EStruct { fields = es; name } -> let fields, es = List.split (StructField.Map.bindings es) in @@ -695,7 +725,10 @@ let rec evaluate_expr : "sum type index error (should not happen if the term was \ well-typed)" in - let new_e = Mark.add m (EApp { f = es_n; args = [e1] }) in + let ty = + EnumConstructor.Map.find cons (EnumName.Map.find name ctx.ctx_enums) + in + let new_e = Mark.add m (EApp { f = es_n; args = [e1]; tys = [ty] }) in evaluate_expr ctx lang new_e | _ -> Message.raise_spanned_error (Expr.pos e) @@ -780,19 +813,22 @@ and partially_evaluate_expr_for_assertion_failure_message : the AST while evaluating everything below. This makes for a good error message. *) match Mark.remove e with - | EApp { f = EOp ({ op = op_kind; _ } as op), m; args = [e1; e2] } - when match op_kind with - | And | Or | Xor | Eq | Lt_int_int | Lt_rat_rat | Lt_mon_mon - | Lt_dat_dat | Lt_dur_dur | Lte_int_int | Lte_rat_rat | Lte_mon_mon - | Lte_dat_dat | Lte_dur_dur | Gt_int_int | Gt_rat_rat | Gt_mon_mon - | Gt_dat_dat | Gt_dur_dur | Gte_int_int | Gte_rat_rat | Gte_mon_mon - | Gte_dat_dat | Gte_dur_dur | Eq_int_int | Eq_rat_rat | Eq_mon_mon - | Eq_dur_dur | Eq_dat_dat -> - true - | _ -> false -> - ( EApp + | EAppOp + { + args = [e1; e2]; + tys; + op = + ( And | Or | Xor | Eq | Lt_int_int | Lt_rat_rat | Lt_mon_mon + | Lt_dat_dat | Lt_dur_dur | Lte_int_int | Lte_rat_rat | Lte_mon_mon + | Lte_dat_dat | Lte_dur_dur | Gt_int_int | Gt_rat_rat | Gt_mon_mon + | Gt_dat_dat | Gt_dur_dur | Gte_int_int | Gte_rat_rat | Gte_mon_mon + | Gte_dat_dat | Gte_dur_dur | Eq_int_int | Eq_rat_rat | Eq_mon_mon + | Eq_dur_dur | Eq_dat_dat ) as op; + } -> + ( EAppOp { - f = EOp op, m; + op; + tys; args = [ partially_evaluate_expr_for_assertion_failure_message ctx lang e1; @@ -809,7 +845,8 @@ let addcustom e = ((d, e, c) interpr_kind, 't) gexpr -> ((d, e, yes) interpr_kind, 't) gexpr boxed = function | (ECustom _, _) as e -> Expr.map ~f e - | EOp { op; tys }, m -> Expr.eop (Operator.translate op) tys m + | EAppOp { op; tys; args }, m -> + Expr.eappop ~tys ~args:(List.map f args) ~op:(Operator.translate op) m | (EDefault _, _) as e -> Expr.map ~f e | (EPureDefault _, _) as e -> Expr.map ~f e | (EEmptyError, _) as e -> Expr.map ~f e @@ -840,7 +877,8 @@ let delcustom e = ((d, e, c) interpr_kind, 't) gexpr -> ((d, e, no) interpr_kind, 't) gexpr boxed = function | ECustom _, _ -> invalid_arg "Custom term remaining in evaluated term" - | EOp { op; tys }, m -> Expr.eop (Operator.translate op) tys m + | EAppOp { op; args; tys }, m -> + Expr.eappop ~tys ~args:(List.map f args) ~op:(Operator.translate op) m | (EDefault _, _) as e -> Expr.map ~f e | (EPureDefault _, _) as e -> Expr.map ~f e | (EEmptyError, _) as e -> Expr.map ~f e @@ -899,9 +937,9 @@ let interpret_program_lcalc p s : (Uid.MarkedString.info * ('a, 'm) gexpr) list (Expr.einj ~e:(Expr.elit LUnit mark_e) ~cons:Expr.none_constr ~name:Expr.option_enum mark_e) ty_in (Expr.mark_pos mark_e); - Expr.eapp - (Expr.eop Operator.ToClosureEnv [TClosureEnv, pos] mark_e) - [Expr.etuple [] mark_e] + Expr.eappop ~op:Operator.ToClosureEnv + ~args:[Expr.etuple [] mark_e] + ~tys:[TClosureEnv, pos] mark_e; ] mark_e @@ -918,6 +956,7 @@ let interpret_program_lcalc p s : (Uid.MarkedString.info * ('a, 'm) gexpr) list let to_interpret = Expr.make_app (Expr.box e) [Expr.estruct ~name:s_in ~fields:application_term mark_e] + [TStruct s_in, Expr.pos e] (Expr.pos e) in match Mark.remove (evaluate_expr ctx p.lang (Expr.unbox to_interpret)) with @@ -969,6 +1008,7 @@ let interpret_program_dcalc p s : (Uid.MarkedString.info * ('a, 'm) gexpr) list let to_interpret = Expr.make_app (Expr.box e) [Expr.estruct ~name:s_in ~fields:application_term mark_e] + [TStruct s_in, Expr.pos e] (Expr.pos e) in match Mark.remove (evaluate_expr ctx p.lang (Expr.unbox to_interpret)) with diff --git a/compiler/shared_ast/optimizations.ml b/compiler/shared_ast/optimizations.ml index a3c57756..0b7e86da 100644 --- a/compiler/shared_ast/optimizations.ml +++ b/compiler/shared_ast/optimizations.ml @@ -100,61 +100,17 @@ let rec optimize_expr : the matches and the log calls are not preserved, which would be a good property *) match Mark.remove e with - | EApp - { - f = - ( EOp { op = Not; _ }, _ - | ( EApp - { - f = EOp { op = Log _; _ }, _; - args = [(EOp { op = Not; _ }, _)]; - }, - _ ) ) as op; - args = [e1]; - } -> ( + | EAppOp { op = Not; args = [(ELit (LBool b), _)]; _ } -> (* reduction of logical not *) - match e1 with - | ELit (LBool false), _ -> ELit (LBool true) - | ELit (LBool true), _ -> ELit (LBool false) - | e1 -> EApp { f = op; args = [e1] }) - | EApp - { - f = - ( EOp { op = Or; _ }, _ - | ( EApp - { - f = EOp { op = Log _; _ }, _; - args = [(EOp { op = Or; _ }, _)]; - }, - _ ) ) as op; - args = [e1; e2]; - } -> ( + ELit (LBool (not b)) + | EAppOp { op = Or; args = [(ELit (LBool b), _); (e, _)]; _ } + | EAppOp { op = Or; args = [(e, _); (ELit (LBool b), _)]; _ } -> (* reduction of logical or *) - match e1, e2 with - | (ELit (LBool false), _), new_e | new_e, (ELit (LBool false), _) -> - Mark.remove new_e - | (ELit (LBool true), _), _ | _, (ELit (LBool true), _) -> - ELit (LBool true) - | _ -> EApp { f = op; args = [e1; e2] }) - | EApp - { - f = - ( EOp { op = And; _ }, _ - | ( EApp - { - f = EOp { op = Log _; _ }, _; - args = [(EOp { op = And; _ }, _)]; - }, - _ ) ) as op; - args = [e1; e2]; - } -> ( + if b then ELit (LBool true) else e + | EAppOp { op = And; args = [(ELit (LBool b), _); (e, _)]; _ } + | EAppOp { op = And; args = [(e, _); (ELit (LBool b), _)]; _ } -> (* reduction of logical and *) - match e1, e2 with - | (ELit (LBool true), _), new_e | new_e, (ELit (LBool true), _) -> - Mark.remove new_e - | (ELit (LBool false), _), _ | _, (ELit (LBool false), _) -> - ELit (LBool false) - | _ -> EApp { f = op; args = [e1; e2] }) + if b then e else ELit (LBool false) | EMatch { e = EInj { e = e'; cons; name = n' }, _; cases; name = n } (* iota-reduction *) when EnumName.equal n n' -> ( @@ -206,7 +162,7 @@ let rec optimize_expr : cases1 cases2 in EMatch { e = arg; cases; name = n1 } - | EApp { f = EAbs { binder; _ }, _; args } + | EApp { f = EAbs { binder; _ }, _; args; _ } when binder_vars_used_at_most_once binder || List.for_all (function EVar _, _ -> true | _ -> false) args -> (* beta reduction when variables not used, and for variable aliases *) @@ -270,11 +226,7 @@ let rec optimize_expr : dft | ( [], ( ( ELit (LBool false) - | EApp - { - f = EOp { op = Log _; _ }, _; - args = [(ELit (LBool false), _)]; - } ), + | EAppOp { op = Log _; args = [(ELit (LBool false), _)]; _ } ), _ ) ) -> (* No exceptions and condition false *) EEmptyError @@ -283,12 +235,7 @@ let rec optimize_expr : { cond = ( ELit (LBool true), _ - | ( EApp - { - f = EOp { op = Log _; _ }, _; - args = [(ELit (LBool true), _)]; - }, - _ ) ); + | EAppOp { op = Log _; args = [(ELit (LBool true), _)]; _ }, _ ); etrue; _; } -> @@ -297,11 +244,7 @@ let rec optimize_expr : { cond = ( ( ELit (LBool false) - | EApp - { - f = EOp { op = Log _; _ }, _; - args = [(ELit (LBool false), _)]; - } ), + | EAppOp { op = Log _; args = [(ELit (LBool false), _)]; _ } ), _ ); efalse; _; @@ -312,40 +255,31 @@ let rec optimize_expr : cond; etrue = ( ( ELit (LBool btrue) - | EApp - { - f = EOp { op = Log _; _ }, _; - args = [(ELit (LBool btrue), _)]; - } ), + | EAppOp { op = Log _; args = [(ELit (LBool btrue), _)]; _ } ), _ ); efalse = ( ( ELit (LBool bfalse) - | EApp - { - f = EOp { op = Log _; _ }, _; - args = [(ELit (LBool bfalse), _)]; - } ), + | EAppOp { op = Log _; args = [(ELit (LBool bfalse), _)]; _ } ), _ ); } -> if btrue && not bfalse then Mark.remove cond else if (not btrue) && bfalse then - EApp - { - f = EOp { op = Not; tys = [TLit TBool, Expr.mark_pos mark] }, mark; - args = [cond]; - } + EAppOp + { op = Not; tys = [TLit TBool, Expr.mark_pos mark]; args = [cond] } (* note: this last call eliminates the condition & might skip log calls as well *) else (* btrue = bfalse *) ELit (LBool btrue) - | EApp { f = EOp { op = Op.Fold; _ }, _; args = [_f; init; (EArray [], _)] } - -> + | EAppOp { op = Op.Fold; args = [_f; init; (EArray [], _)]; _ } -> (*reduces a fold with an empty list *) Mark.remove init - | EApp - { f = EOp { op = Op.Fold; _ }, _; args = [f; init; (EArray [e'], _)] } - -> + | EAppOp + { + op = Op.Fold; + args = [f; init; (EArray [e'], _)]; + tys = [_; tinit; (TArray tx, _)]; + } -> (* reduces a fold with one element *) - EApp { f; args = [init; e'] } + EApp { f; args = [init; e']; tys = [tinit; tx] } | ECatch { body; exn; handler } -> ( (* peephole exception catching reductions *) match Mark.remove body, Mark.remove handler with diff --git a/compiler/shared_ast/print.ml b/compiler/shared_ast/print.ml index 782a436c..047ef7f1 100644 --- a/compiler/shared_ast/print.ml +++ b/compiler/shared_ast/print.ml @@ -374,7 +374,7 @@ module Precedence = struct fun e -> match Mark.remove e with | ELit _ -> Contained (* Todo: unop if < 0 *) - | EApp { f = EOp { op; _ }, _; _ } -> ( + | EAppOp { op; _ } -> ( match op with | Not | GetDay | GetMonth | GetYear | FirstDayOfMonth | LastDayOfMonth | Length | Log _ | Minus | Minus_int | Minus_rat | Minus_mon | Minus_dur @@ -411,7 +411,6 @@ module Precedence = struct | ToClosureEnv | FromClosureEnv -> App) | EApp _ -> App - | EOp _ -> Contained | EArray _ -> Contained | EVar _ -> Contained | EExternal _ -> Contained @@ -527,7 +526,7 @@ module ExprGen (C : EXPR_PARAM) = struct | ELit l -> C.lit fmt l | EApp { f = EAbs _, _; _ } -> let rec pr bnd_ctx colors fmt = function - | EApp { f = EAbs { binder; tys }, _; args }, _ -> + | 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 = @@ -563,19 +562,16 @@ module ExprGen (C : EXPR_PARAM) = struct Format.pp_close_box fmt (); punctuation fmt ")")) xs_tau punctuation "→" (rhs expr) body - | EApp - { f = EOp { op = (Map | Filter) as op; _ }, _; args = [arg1; arg2] } - -> + | EAppOp { op = (Map | Filter) as op; args = [arg1; arg2]; _ } -> Format.fprintf fmt "@[%a %a@ %a@]" operator op (lhs exprc) arg1 (rhs exprc) arg2 - | EApp { f = EOp { op = Log _ as op; _ }, _; args = [arg1] } -> + | EAppOp { op = Log _ as op; args = [arg1]; _ } -> Format.fprintf fmt "@[%a@ %a@]" operator op (rhs exprc) arg1 - | EApp { f = EOp { op = op0; _ }, _; args = [_; _] } -> + | EAppOp { 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 - -> ( + | EAppOp { 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); @@ -590,9 +586,15 @@ module ExprGen (C : EXPR_PARAM) = struct Format.pp_open_hvbox fmt 0; pr colors fmt e; Format.pp_close_box fmt () - | EApp { f = EOp { op; _ }, _; args = [arg1] } -> + | EAppOp { op; args = [arg1]; _ } -> Format.fprintf fmt "@[%a@ %a@]" operator op (rhs exprc) arg1 - | EApp { f; args } -> + | EAppOp { op; args; _ } -> + Format.fprintf fmt "@[%a@ %a@]" operator op + (Format.pp_print_list + ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ") + (rhs exprc)) + args + | EApp { f; args; _ } -> Format.fprintf fmt "@[%a@ %a@]" (lhs exprc) f (Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ") @@ -611,7 +613,6 @@ module ExprGen (C : EXPR_PARAM) = struct Format.pp_open_hvbox fmt 0; pr false fmt e; Format.pp_close_box fmt () - | EOp { op; _ } -> operator fmt op | EDefault { excepts; just; cons } -> if List.length excepts = 0 then Format.fprintf fmt "@[%a%a@ %a %a%a@]" @@ -734,7 +735,7 @@ module ExprConciseParam = struct let lit = lit let rec pre_map : type a. (a, 't) gexpr -> (a, 't) gexpr = function - | EApp { f = EOp { op = Log _; _ }, _; args = [e] }, _ -> pre_map e + | EAppOp { op = Log _; args = [e]; _ }, _ -> pre_map e | e -> e end @@ -929,6 +930,18 @@ let program ?(debug = false) fmt p = (* - User-facing value printer - *) +(* This function is re-exported from module [Expr], but defined here where it's + first needed *) +let rec skip_wrappers : type a. (a, 'm) gexpr -> (a, 'm) gexpr = function + | EAppOp { op = Log _; args = [e]; tys = _ }, _ -> skip_wrappers e + | EApp { f = EAppOp { op = Log _; args = [f]; _ }, _; args; tys }, m -> + skip_wrappers (EApp { f; args; tys }, m) + | EErrorOnEmpty e, _ -> skip_wrappers e + | EDefault { excepts = []; just = ELit (LBool true), _; cons = e }, _ -> + skip_wrappers e + | EPureDefault e, _ -> skip_wrappers e + | e -> e + module UserFacing = struct (* Refs: https://en.wikipedia.org/wiki/Wikipedia:Manual_of_Style/Dates_and_numbers#Grouping_of_digits @@ -1092,24 +1105,12 @@ module UserFacing = struct | EEmptyError -> Format.pp_print_string ppf "ø" | EAbs _ -> Format.pp_print_string ppf "" | EExternal _ -> Format.pp_print_string ppf "" - | EApp _ | EOp _ | EVar _ | EIfThenElse _ | EMatch _ | ETupleAccess _ + | EApp _ | EAppOp _ | EVar _ | EIfThenElse _ | EMatch _ | ETupleAccess _ | EStructAccess _ | EAssert _ | EDefault _ | EPureDefault _ | EErrorOnEmpty _ | ERaise _ | ECatch _ | ELocation _ | EScopeCall _ | EDStructAccess _ | ECustom _ -> fallback ppf e - (* This function is already in module [Expr], but [Expr] depends on this - module *) - 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 expr : type a. Cli.backend_lang -> Format.formatter -> (a, 't) gexpr -> unit = fun lang -> diff --git a/compiler/shared_ast/print.mli b/compiler/shared_ast/print.mli index 3fd201e6..efdbe53d 100644 --- a/compiler/shared_ast/print.mli +++ b/compiler/shared_ast/print.mli @@ -125,3 +125,8 @@ module UserFacing : sig (** This combines the user-facing value printer and the generic expression printer to handle all AST nodes *) end + +(**/*) + +val skip_wrappers : ('a, 'm) gexpr -> ('a, 'm) gexpr +(** This is exported from [Expr], but first defined here for dependency reasons *) diff --git a/compiler/shared_ast/typing.ml b/compiler/shared_ast/typing.ml index edc82677..562790c8 100644 --- a/compiler/shared_ast/typing.ml +++ b/compiler/shared_ast/typing.ml @@ -327,7 +327,6 @@ let resolve_overload_ret_type Operator.overload_type ctx (Mark.add (Expr.pos e) op) (List.map (typ_to_ast ~leave_unresolved) tys) - (* We use [unsafe] because the error is caught below *) in ast_to_typ (Type.arrow_return op_ty) @@ -750,7 +749,7 @@ and typecheck_expr_top_down : (unionfind ~pos:e1 tuple_ty) e1 in - Expr.etupleaccess e1' index size context_mark + Expr.etupleaccess ~e:e1' ~index ~size context_mark | A.EAbs { binder; tys = t_args } -> if Bindlib.mbinder_arity binder <> List.length t_args then Message.raise_spanned_error (Expr.pos e) @@ -774,98 +773,72 @@ and typecheck_expr_top_down : in let binder' = Bindlib.bind_mvar xs' (Expr.Box.lift body') in Expr.eabs binder' (List.map (typ_to_ast ~leave_unresolved) tau_args) mark - | A.EApp { f = (EOp { op; tys }, _) as e1; args } -> + | A.EApp { f = e1; args; tys } -> + (* Here we type the arguments first (in order), to ensure we know the types + of the arguments if [f] is [EAbs] before disambiguation. This is also the + right order for the [let-in] form. *) + let t_args = + match tys with + | [] -> List.map (fun _ -> unionfind (TAny (Any.fresh ()))) args + | tys -> List.map ast_to_typ tys + in + let args' = + List.map2 (typecheck_expr_top_down ~leave_unresolved ctx env) t_args args + in + let t_args = + match t_args with + | [t] -> ( + match UnionFind.get t with TTuple tys, _ -> tys | _ -> t_args) + | _ -> t_args + in + let t_func = unionfind ~pos:e1 (TArrow (t_args, tau)) in + let e1' = typecheck_expr_top_down ~leave_unresolved ctx env t_func e1 in + Expr.eapp ~f:e1' ~args:args' + ~tys:(List.map (typ_to_ast ~leave_unresolved) t_args) + context_mark + | A.EAppOp { op; tys; args } -> let t_args = List.map ast_to_typ tys in let t_func = unionfind (TArrow (t_args, tau)) in - let e1', args' = + let args = Operator.kind_dispatch op - ~polymorphic:(fun _ -> + ~polymorphic:(fun op -> (* Type the operator first, then right-to-left: polymorphic operators are required to allow the resolution of all type variables this way *) - let e1' = - typecheck_expr_top_down ~leave_unresolved ctx env t_func e1 - in - let args' = - List.rev_map2 - (typecheck_expr_top_down ~leave_unresolved ctx env) - (List.rev t_args) (List.rev args) - in - e1', args') - ~overloaded:(fun _ -> + unify ctx e (polymorphic_op_type (Mark.add pos_e op)) t_func; + List.rev_map2 + (typecheck_expr_top_down ~leave_unresolved ctx env) + (List.rev t_args) (List.rev args)) + ~overloaded:(fun op -> (* Typing the arguments first is required to resolve the operator *) let args' = List.map2 (typecheck_expr_top_down ~leave_unresolved ctx env) t_args args in - let e1' = - typecheck_expr_top_down ~leave_unresolved ctx env t_func e1 - in - e1', args') - ~monomorphic:(fun _ -> - (* Here it doesn't matter but may affect the error messages *) - let e1' = - typecheck_expr_top_down ~leave_unresolved ctx env t_func e1 - in - let args' = - List.map2 - (typecheck_expr_top_down ~leave_unresolved ctx env) - t_args args - in - e1', args') - ~resolved:(fun _ -> - (* This case should not fail *) - let e1' = - typecheck_expr_top_down ~leave_unresolved ctx env t_func e1 - in - let args' = - List.map2 - (typecheck_expr_top_down ~leave_unresolved ctx env) - t_args args - in - e1', args') - in - Expr.eapp e1' args' context_mark - | A.EApp { f = e1; args } -> - (* Here we type the arguments first (in order), to ensure we know the types - of the arguments if [f] is [EAbs] before disambiguation. This is also the - right order for the [let-in] form. *) - let t_args = List.map (fun _ -> unionfind (TAny (Any.fresh ()))) args in - let t_func = unionfind (TArrow (t_args, tau)) in - let args' = - List.map2 (typecheck_expr_top_down ~leave_unresolved ctx env) t_args args - in - let e1' = typecheck_expr_top_down ~leave_unresolved ctx env t_func e1 in - Expr.eapp e1' args' context_mark - | A.EOp { op; tys } -> - let tys' = List.map ast_to_typ tys in - let t_ret = unionfind (TAny (Any.fresh ())) in - let t_func = unionfind (TArrow (tys', t_ret)) in - unify ctx e t_func tau; - let tys, mark = - Operator.kind_dispatch op - ~polymorphic:(fun op -> - tys, mark_with_tau_and_unify (polymorphic_op_type (Mark.add pos_e op))) + unify ctx e tau + (resolve_overload_ret_type ~leave_unresolved ctx e op t_args); + args') ~monomorphic:(fun op -> - let mark = - mark_with_tau_and_unify - (ast_to_typ (Operator.monomorphic_type (Mark.add pos_e op))) - in - List.map (typ_to_ast ~leave_unresolved) tys', mark) - ~overloaded:(fun op -> - unify ctx e t_ret - (resolve_overload_ret_type ~leave_unresolved ctx e op tys'); - ( List.map (typ_to_ast ~leave_unresolved) tys', - A.Custom { A.custom = t_func; pos = pos_e } )) + (* Here it doesn't matter but may affect the error messages *) + unify ctx e + (ast_to_typ (Operator.monomorphic_type (Mark.add pos_e op))) + t_func; + List.map2 + (typecheck_expr_top_down ~leave_unresolved ctx env) + t_args args) ~resolved:(fun op -> - let mark = - mark_with_tau_and_unify - (ast_to_typ (Operator.resolved_type (Mark.add pos_e op))) - in - List.map (typ_to_ast ~leave_unresolved) tys', mark) + (* This case should not fail *) + unify ctx e + (ast_to_typ (Operator.resolved_type (Mark.add pos_e op))) + t_func; + List.map2 + (typecheck_expr_top_down ~leave_unresolved ctx env) + t_args args) in - Expr.eop op tys mark + (* All operator applications are monomorphised at this point *) + let tys = List.map (typ_to_ast ~leave_unresolved) t_args in + Expr.eappop ~op ~args ~tys context_mark | A.EDefault { excepts; just; cons } -> let cons' = typecheck_expr_top_down ~leave_unresolved ctx env tau cons in let just' = diff --git a/compiler/shared_ast/typing.mli b/compiler/shared_ast/typing.mli index f540ca63..7fa6d885 100644 --- a/compiler/shared_ast/typing.mli +++ b/compiler/shared_ast/typing.mli @@ -61,9 +61,12 @@ val expr : filling the gaps ([TAny]) if any. Use [Expr.untype] first if this is not what you want. - Note that typing also transparently performs disambiguation of constructors: - [EDStructAccess] nodes are translated into [EStructAccess] with the suitable - structure and field idents (this only concerns [desugared] expressions). *) + Note that typing also transparently performs + - disambiguation of constructors: [EDStructAccess] nodes are translated into + [EStructAccess] with the suitable structure and field idents (this only + concerns [desugared] expressions). + - resolution of operator types, which are stored (monomorphised) back in the + AST nodes *) val check_expr : leave_unresolved:bool -> diff --git a/compiler/verification/conditions.ml b/compiler/verification/conditions.ml index d2269bd1..fabf5eb0 100644 --- a/compiler/verification/conditions.ml +++ b/compiler/verification/conditions.ml @@ -38,15 +38,10 @@ let rec conjunction_exprs (exprs : typed expr list) (mark : typed mark) : match exprs with | [] -> ELit (LBool true), mark | hd :: tl -> - ( EApp + ( EAppOp { - f = - ( EOp - { - op = And; - tys = [TLit TBool, Expr.pos hd; TLit TBool, Expr.pos hd]; - }, - mark ); + op = And; + tys = [TLit TBool, Expr.pos hd; TLit TBool, Expr.pos hd]; args = [hd; conjunction_exprs tl mark]; }, mark ) @@ -57,27 +52,17 @@ let conjunction (args : vc_return list) (mark : typed mark) : vc_return = in List.fold_left (fun acc arg -> - ( EApp + ( EAppOp { - f = - ( EOp - { - op = And; - tys = [TLit TBool, Expr.pos acc; TLit TBool, Expr.pos arg]; - }, - mark ); + op = And; + tys = [TLit TBool, Expr.pos acc; TLit TBool, Expr.pos arg]; args = [arg; acc]; }, mark )) acc list let negation (arg : vc_return) (mark : typed mark) : vc_return = - ( EApp - { - f = EOp { op = Not; tys = [TLit TBool, Expr.pos arg] }, mark; - args = [arg]; - }, - mark ) + EAppOp { op = Not; tys = [TLit TBool, Expr.pos arg]; args = [arg] }, mark let disjunction (args : vc_return list) (mark : typed mark) : vc_return = let acc, list = @@ -85,15 +70,10 @@ let disjunction (args : vc_return list) (mark : typed mark) : vc_return = in List.fold_left (fun (acc : vc_return) arg -> - ( EApp + ( EAppOp { - f = - ( EOp - { - op = Or; - tys = [TLit TBool, Expr.pos acc; TLit TBool, Expr.pos arg]; - }, - mark ); + op = Or; + tys = [TLit TBool, Expr.pos acc; TLit TBool, Expr.pos arg]; args = [arg; acc]; }, mark )) @@ -117,7 +97,7 @@ let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : typed expr) : | EErrorOnEmpty ( EDefault { - excepts = [(EApp { f = EVar x, _; args = [(ELit LUnit, _)] }, _)]; + excepts = [(EApp { f = EVar x, _; args = [(ELit LUnit, _)]; _ }, _)]; just = ELit (LBool true), _; cons; }, @@ -196,9 +176,9 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : typed expr) : (* Per default calculus semantics, you cannot call a function with an argument that evaluates to the empty error. Thus, all variable evaluate to non-empty-error terms. *) - | ELit _ | EOp _ -> + | ELit _ -> Mark.copy e (ELit (LBool true)) - | EApp { f; args } -> + | EApp { f; args; _ } -> (* Invariant: For the [EApp] case, we assume here that function calls never return empty error, which implies all functions have been checked never to return empty errors. *) @@ -250,7 +230,7 @@ let rec generate_vc_must_not_return_conflict (ctx : ctx) (e : typed expr) : | EAbs { binder; _ } -> let _vars, body = Bindlib.unmbind binder in (generate_vc_must_not_return_conflict ctx) body - | EVar _ | ELit _ | EOp _ -> Mark.copy e (ELit (LBool true)) + | EVar _ | ELit _ -> Mark.copy e (ELit (LBool true)) | EDefault { excepts; just; cons } -> (* never returns conflict if and only if: - neither e1 nor ... nor en nor ejust nor econs return conflict - there is diff --git a/compiler/verification/z3backend.real.ml b/compiler/verification/z3backend.real.ml index 2db4e0bc..f5c47fb3 100644 --- a/compiler/verification/z3backend.real.ml +++ b/compiler/verification/z3backend.real.ml @@ -437,9 +437,9 @@ let rec translate_op : let ill_formed () = Format.kasprintf failwith "[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) + (Shared_ast.Expr.eappop ~op + ~args:(List.map Shared_ast.Expr.untype args) + ~tys:[] (Untyped { pos = Pos.no_pos }) |> Shared_ast.Expr.unbox) in @@ -458,10 +458,7 @@ let rec translate_op : failwith "[Z3 encoding] ternary operator application not supported" (* Special case for GetYear comparisons *) | ( Lt_int_int, - [ - (EApp { f = EOp { op = GetYear; _ }, _; args = [e1] }, _); - (ELit (LInt n), _); - ] ) -> + [(EAppOp { op = GetYear; args = [e1]; _ }, _); (ELit (LInt n), _)] ) -> let n = Runtime.integer_to_int n in let ctx, e1 = translate_expr ctx e1 in let e2 = @@ -472,10 +469,7 @@ let rec translate_op : days *) ctx, Arithmetic.mk_lt ctx.ctx_z3 e1 e2 | ( Lte_int_int, - [ - (EApp { f = EOp { op = GetYear; _ }, _; args = [e1] }, _); - (ELit (LInt n), _); - ] ) -> + [(EAppOp { op = GetYear; args = [e1]; _ }, _); (ELit (LInt n), _)] ) -> let ctx, e1 = translate_expr ctx e1 in let nb_days = if is_leap_year n then 365 else 364 in let n = Runtime.integer_to_int n in @@ -489,10 +483,7 @@ let rec translate_op : in ctx, Arithmetic.mk_le ctx.ctx_z3 e1 e2 | ( Gt_int_int, - [ - (EApp { f = EOp { op = GetYear; _ }, _; args = [e1] }, _); - (ELit (LInt n), _); - ] ) -> + [(EAppOp { op = GetYear; args = [e1]; _ }, _); (ELit (LInt n), _)] ) -> let ctx, e1 = translate_expr ctx e1 in let nb_days = if is_leap_year n then 365 else 364 in let n = Runtime.integer_to_int n in @@ -506,10 +497,7 @@ let rec translate_op : in ctx, Arithmetic.mk_gt ctx.ctx_z3 e1 e2 | ( Gte_int_int, - [ - (EApp { f = EOp { op = GetYear; _ }, _; args = [e1] }, _); - (ELit (LInt n), _); - ] ) -> + [(EAppOp { op = GetYear; args = [e1]; _ }, _); (ELit (LInt n), _)] ) -> let n = Runtime.integer_to_int n in let ctx, e1 = translate_expr ctx e1 in let e2 = @@ -519,11 +507,7 @@ let rec translate_op : be directly translated as >= in the Z3 encoding using the number of days *) ctx, Arithmetic.mk_ge ctx.ctx_z3 e1 e2 - | ( Eq, - [ - (EApp { f = EOp { op = GetYear; _ }, _; args = [e1] }, _); - (ELit (LInt n), _); - ] ) -> + | Eq, [(EAppOp { op = GetYear; args = [e1]; _ }, _); (ELit (LInt n), _)] -> let n = Runtime.integer_to_int n in let ctx, e1 = translate_expr ctx e1 in let min_date = @@ -733,9 +717,9 @@ and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr = | EArray _ -> failwith "[Z3 encoding] EArray unsupported" | ELit l -> ctx, translate_lit ctx l | EAbs _ -> failwith "[Z3 encoding] EAbs unsupported" - | EApp { f = head; args } -> ( + | EAppOp { op; args; _ } -> translate_op ctx op args + | EApp { f = head; args; _ } -> ( match Mark.remove head with - | EOp { op; _ } -> translate_op ctx op args | EVar v -> let (Typed { ty = f_ty; _ }) = Mark.get head in let ctx, fd = find_or_create_funcdecl ctx v f_ty in @@ -762,7 +746,6 @@ and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr = "[Z3 encoding] EApp node: Catala function calls should only include \ operators or function names") | EAssert e -> translate_expr ctx e - | EOp _ -> failwith "[Z3 encoding] EOp unsupported" | EDefault _ -> failwith "[Z3 encoding] EDefault unsupported" | EPureDefault _ -> failwith "[Z3 encoding] EPureDefault unsupported" | EIfThenElse { cond = e_if; etrue = e_then; efalse = e_else } ->