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

AST change: more specific application

Browse Source 
As part of making tuples first-class citizens, expliciting the arity upon
function application was needed (so that a function of two args can
transparently -- in the surface language -- be applied to either two arguments
or a pair).

It was decided to actually explicit the whole type of arguments because the cost
is the same, and this is consistent with lambda definitions.

A related change done here is the replacement of the `EOp` node for operators by
an "operator application" `EAppOp` node, enforcing a pervasive invariant that
operators are always directly applied. This makes matches terser, and highlights
the fact that the treatment of operator application is almost always different
from function application in practice.
This commit is contained in:
Louis Gesbert 2023-12-18 10:25:00 +01:00
parent 94ebc1b65e
commit 2823795f9f
30 changed files with 771 additions and 942 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

90
compiler/dcalc/from_scopelang.ml
View File

@ -97,7 +97,7 @@ let merge_defaults
rewriting *) rewriting *)
(Expr.with_ty m_body ~pos:(Expr.mark_pos m_body) ty)) (Expr.with_ty m_body ~pos:(Expr.mark_pos m_body) ty))
(Array.to_list vars) tys) (Array.to_list vars) tys)
pos tys pos
in in
let ltrue = let ltrue =
Expr.elit (LBool true) Expr.elit (LBool true)
@ -119,6 +119,7 @@ let merge_defaults
let pos = Expr.mark_pos m in let pos = Expr.mark_pos m in
Expr.make_app caller Expr.make_app caller
[Expr.elit LUnit (Expr.with_ty m (Mark.add pos (TLit TUnit)))] [Expr.elit LUnit (Expr.with_ty m (Mark.add pos (TLit TUnit)))]
[TLit TUnit, pos]
pos pos
in in
let body = let body =
@ -140,7 +141,7 @@ let tag_with_log_entry
let m = mark_tany (Mark.get e) (Expr.pos e) in let m = mark_tany (Mark.get e) (Expr.pos e) in
if Cli.globals.trace then 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 else e
(* In a list of exceptions, it is normally an error if more than a single one (* 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 in
(* calling_expr = scope_function scope_input_struct *) (* 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 (* 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 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 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 = let f_markings =
[ScopeName.get_info scope; StructField.get_info field] [ScopeName.get_info scope; StructField.get_info field]
in 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 Expr.make_abs
(Array.of_list params_vars) (Array.of_list params_vars)
(tag_with_log_entry (tag_with_log_entry
(tag_with_log_entry (tag_with_log_entry
(Expr.eapp (Expr.eapp
(tag_with_log_entry original_field_expr BeginCall ~f:
f_markings) (tag_with_log_entry original_field_expr BeginCall
(ListLabels.mapi (List.combine params_vars ts_in) f_markings)
~f:(fun i (param_var, t_in) -> ~args ~tys:ts_in (Expr.with_ty m t_out))
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))
(VarDef (VarDef
{ {
log_typ = Mark.remove t_out; 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"]) [ScopeName.get_info scope; Mark.add (Expr.pos e) "direct"])
(Expr.pos e)) (Expr.pos e))
(Expr.pos e) (Expr.pos e)
| EApp { f; args } -> | EApp { f; args; tys } ->
(* We insert various log calls to record arguments and outputs of (* We insert various log calls to record arguments and outputs of
user-defined functions belonging to scopes *) user-defined functions belonging to scopes *)
let e1_func = translate_expr ctx f in 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 | m -> tag_with_log_entry e1_func BeginCall m
in in
let new_args = List.map (translate_expr ctx) args 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 (* NOTE: this is a temporary solution, it works because it's assumed that
all function calls are from scope variables. However, this will change all function have explicit types. However, this will change -- for more
-- for more information see information see
https://github.com/CatalaLang/catala/pull/280#discussion_r898851693. *) 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 let _, typ, _ = ScopeVar.Map.find (Mark.remove var) vars in
match typ with match typ with
| TArrow (marked_input_typ, marked_output_typ) -> | TArrow (_, marked_output_typ) -> Mark.remove marked_output_typ
List.map Mark.remove marked_input_typ, Mark.remove marked_output_typ | _ -> TAny
| _ -> ListLabels.map new_args ~f:(fun _ -> TAny), TAny
in in
match Mark.remove f with match Mark.remove f with
| ELocation (ScopelangScopeVar { name = var }) -> | 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; _ }) -> | ELocation (SubScopeVar { alias; var; _ }) ->
ctx.subscope_vars ctx.subscope_vars
|> SubScopeName.Map.find (Mark.remove alias) |> SubScopeName.Map.find (Mark.remove alias)
|> retrieve_in_and_out_typ_or_any var |> retrieve_out_typ_or_any var
| ELocation (ToplevelVar { name }) -> ( | ELocation (ToplevelVar { name }) -> (
let typ = let typ =
TopdefName.Map.find (Mark.remove name) ctx.decl_ctx.ctx_topdefs TopdefName.Map.find (Mark.remove name) ctx.decl_ctx.ctx_topdefs
in in
match Mark.remove typ with match Mark.remove typ with
| TArrow (tin, (tout, _)) -> List.map Mark.remove tin, tout | TArrow (_, (tout, _)) -> tout
| _ -> | _ ->
Message.raise_spanned_error (Expr.pos e) Message.raise_spanned_error (Expr.pos e)
"Application of non-function toplevel variable") "Application of non-function toplevel variable")
| _ -> ListLabels.map new_args ~f:(fun _ -> TAny), TAny | _ -> TAny
in in
(* Message.emit_debug "new_args %d, input_typs: %d, input_typs %a" (* Message.emit_debug "new_args %d, input_typs: %d, input_typs %a"
(List.length new_args) (List.length input_typs) (Format.pp_print_list (List.length new_args) (List.length input_typs) (Format.pp_print_list
Print.typ_debug) (List.map (Mark.add Pos.no_pos) input_typs); *) 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)]) (m @ [Mark.add (Expr.pos e) ("input" ^ string_of_int i)])
| _ -> new_arg) | _ -> new_arg)
in in
let new_e = Expr.eapp ~f:e1_func ~args:new_args ~tys m in
let new_e = Expr.eapp e1_func new_args m in
let new_e = let new_e =
match markings with match markings with
| [] -> new_e | [] -> 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 let v, _ = TopdefName.Map.find (Mark.remove name) ctx.toplevel_vars in
Expr.evar v m Expr.evar v m
else Expr.eexternal ~name:(Mark.map (fun n -> External_value n) name) m else Expr.eexternal ~name:(Mark.map (fun n -> External_value n) name) m
| EOp { op = Add_dat_dur _; tys } -> | EAppOp { op = Add_dat_dur _; args; tys } ->
Expr.eop (Add_dat_dur ctx.date_rounding) tys m let args = List.map (translate_expr ctx) args in
| EOp { op; tys } -> Expr.eop (Operator.translate op) tys m 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 _ | ( EVar _ | EAbs _ | ELit _ | EStruct _ | EStructAccess _ | ETuple _
| ETupleAccess _ | EInj _ | EEmptyError | EErrorOnEmpty _ | EArray _ | ETupleAccess _ | EInj _ | EEmptyError | EErrorOnEmpty _ | EArray _
| EIfThenElse _ ) as e -> | EIfThenElse _ ) as e ->
@ -818,7 +824,9 @@ let translate_rule
in in
let call_expr = let call_expr =
tag_with_log_entry 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 EndCall
[ [
sigma_name, pos_sigma; sigma_name, pos_sigma;

26
compiler/dcalc/invariants.ml
View File

@ -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 *) (* Structural invariant: no default can have as type A -> B *)
let invariant_default_no_arrow () : string * invariant_expr = let invariant_default_no_arrow () : string * invariant_expr =
( __FUNCTION__, ( "default_no_arrow",
fun _ctx e -> fun _ctx e ->
match Mark.remove e with match Mark.remove e with
| EDefault _ -> begin | EDefault _ -> begin
@ -67,19 +67,18 @@ let invariant_default_no_arrow () : string * invariant_expr =
(* Structural invariant: no partial evaluation *) (* Structural invariant: no partial evaluation *)
let invariant_no_partial_evaluation () : string * invariant_expr = let invariant_no_partial_evaluation () : string * invariant_expr =
( __FUNCTION__, ( "no_partial_evaluation",
fun _ctx e -> fun _ctx e ->
match Mark.remove e with match Mark.remove e with
| EApp { f = EOp { op = Op.Log _; _ }, _; _ } -> | EApp { f; args; _ } -> (
(* logs are differents. *) Pass match Mark.remove (Expr.ty f) with
| EApp _ -> begin | TArrow (tl, _) when List.length args = List.length tl -> Pass
match Mark.remove (Expr.ty e) with TArrow _ -> Fail | _ -> Pass | _ -> Fail)
end
| _ -> Ignore ) | _ -> Ignore )
(* Structural invariant: no function can return an function *) (* Structural invariant: no function can return an function *)
let invariant_no_return_a_function () : string * invariant_expr = let invariant_no_return_a_function () : string * invariant_expr =
( __FUNCTION__, ( "no_return_a_function",
fun _ctx e -> fun _ctx e ->
match Mark.remove e with match Mark.remove e with
| EAbs _ -> begin | EAbs _ -> begin
@ -90,16 +89,13 @@ let invariant_no_return_a_function () : string * invariant_expr =
| _ -> Ignore ) | _ -> Ignore )
let invariant_app_inversion () : string * invariant_expr = let invariant_app_inversion () : string * invariant_expr =
( __FUNCTION__, ( "app_inversion",
fun _ctx e -> fun _ctx e ->
match Mark.remove e with 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 if Bindlib.mbinder_arity binder = 1 && List.length args = 1 then Pass
else Fail else Fail
| EApp { f = EVar _, _; _ } -> Pass | EApp { f = EVar _, _; _ } -> Pass
| EApp { f = EApp { f = EOp { op = Op.Log _; _ }, _; args = _ }, _; _ } ->
Pass
| EApp { f = EStructAccess _, _; _ } -> Pass | EApp { f = EStructAccess _, _; _ } -> Pass
| EApp { f = EExternal _, _; _ } -> Pass | EApp { f = EExternal _, _; _ } -> Pass
| EApp _ -> Fail | EApp _ -> Fail
@ -107,7 +103,7 @@ let invariant_app_inversion () : string * invariant_expr =
(** the arity of constructors when matching is always one. *) (** the arity of constructors when matching is always one. *)
let invariant_match_inversion () : string * invariant_expr = let invariant_match_inversion () : string * invariant_expr =
( __FUNCTION__, ( "match_inversion",
fun _ctx e -> fun _ctx e ->
match Mark.remove e with match Mark.remove e with
| EMatch { cases; _ } -> | EMatch { cases; _ } ->
@ -207,7 +203,7 @@ let check_type_root ctx ty =
| _ -> false | _ -> false
let invariant_typing_defaults () : string * invariant_expr = let invariant_typing_defaults () : string * invariant_expr =
( __FUNCTION__, ( "typing_defaults",
fun ctx e -> fun ctx e ->
if check_type_root ctx (Expr.ty e) then Pass if check_type_root ctx (Expr.ty e) then Pass
else ( else (

2
compiler/desugared/disambiguate.ml
View File

@ -21,7 +21,7 @@ let expr ctx env e =
(* The typer takes care of disambiguating: this consists in: - ensuring (* The typer takes care of disambiguating: this consists in: - ensuring
[EAbs.tys] doesn't contain any [TAny] - [EDStructAccess.name_opt] is always [EAbs.tys] doesn't contain any [TAny] - [EDStructAccess.name_opt] is always
[Some] *) [Some] *)
(* Intermediate unboxings are fine since the last [untype] will rebox in (* Intermediate unboxings are fine since the [check_expr] will rebox in
depth *) depth *)
Typing.check_expr ~leave_unresolved:false ctx ~env (Expr.unbox e) Typing.check_expr ~leave_unresolved:false ctx ~env (Expr.unbox e)

3
compiler/desugared/disambiguate.mli
View File

@ -18,7 +18,8 @@
in the AST: in the AST:
- it fills the types of arguments in [EAbs] nodes, (untyped ones are - 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. *) - it resolves the structure names of [EDStructAccess] nodes. *)
val program : Ast.program -> Ast.program val program : Ast.program -> Ast.program

166
compiler/desugared/from_surface.ml
View File

@ -34,10 +34,14 @@ module Runtime = Runtime_ocaml.Runtime
the operator suffixes for explicit typing. See {!modules: the operator suffixes for explicit typing. See {!modules:
Shared_ast.Operator} for detail. *) Shared_ast.Operator} for detail. *)
let translate_binop : S.binop -> Pos.t -> Ast.expr boxed = let translate_binop :
fun op pos -> S.binop -> Pos.t -> Ast.expr boxed -> Ast.expr boxed -> Ast.expr boxed =
fun op pos lhs rhs ->
let op_expr op tys = 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 in
match op with match op with
| S.And -> op_expr And [TLit TBool; TLit TBool] | 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.Neq -> assert false (* desugared already *)
| S.Concat -> op_expr Concat [TArray (TAny, pos); TArray (TAny, pos)] | S.Concat -> op_expr Concat [TArray (TAny, pos); TArray (TAny, pos)]
let translate_unop (op : S.unop) pos : Ast.expr boxed = let translate_unop (op : S.unop) pos arg : Ast.expr boxed =
let op_expr op ty = Expr.eop op [Mark.add pos ty] (Untyped { pos }) in let op_expr op ty =
Expr.eappop ~op ~tys:[Mark.add pos ty] ~args:[arg] (Untyped { pos })
in
match op with match op with
| S.Not -> op_expr Not (TLit TBool) | S.Not -> op_expr Not (TLit TBool)
| S.Minus k -> | S.Minus k ->
@ -251,8 +257,8 @@ let rec translate_expr
| Binop ((((S.And | S.Or | S.Xor), _) as op), e1, e2) -> | Binop ((((S.And | S.Or | S.Xor), _) as op), e1, e2) ->
check_formula op e1; check_formula op e1;
check_formula op e2; check_formula op e2;
let op_term = translate_binop (Mark.remove op) (Mark.get op) in translate_binop (Mark.remove op) (Mark.get op) (rec_helper e1)
Expr.eapp op_term [rec_helper e1; rec_helper e2] emark (rec_helper e2)
| IfThenElse (e_if, e_then, e_else) -> | IfThenElse (e_if, e_then, e_else) ->
Expr.eifthenelse (rec_helper e_if) (rec_helper e_then) (rec_helper e_else) Expr.eifthenelse (rec_helper e_if) (rec_helper e_then) (rec_helper e_else)
emark emark
@ -260,11 +266,8 @@ let rec translate_expr
(* Neq is just sugar *) (* Neq is just sugar *)
rec_helper (Unop ((S.Not, posn), (Binop ((S.Eq, posn), e1, e2), posn)), pos) rec_helper (Unop ((S.Not, posn), (Binop ((S.Eq, posn), e1, e2), posn)), pos)
| Binop ((op, pos), e1, e2) -> | Binop ((op, pos), e1, e2) ->
let op_term = translate_binop op pos in translate_binop op pos (rec_helper e1) (rec_helper e2)
Expr.eapp op_term [rec_helper e1; rec_helper e2] emark | Unop ((op, pos), e) -> translate_unop op pos (rec_helper e)
| Unop ((op, pos), e) ->
let op_term = translate_unop op pos in
Expr.eapp op_term [rec_helper e] emark
| Literal l -> | Literal l ->
let lit = let lit =
match l with match l with
@ -416,8 +419,25 @@ let rec translate_expr
in in
Expr.edstructaccess ~e ~field:(Mark.remove x) Expr.edstructaccess ~e ~field:(Mark.remove x)
~name_opt:(get_str ctxt path) emark) ~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) -> | 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) -> | ScopeCall (((path, id), _), fields) ->
if scope = None then if scope = None then
Message.raise_spanned_error pos Message.raise_spanned_error pos
@ -468,10 +488,10 @@ let rec translate_expr
in in
let taus = List.map (fun x -> TAny, Mark.get x) xs in let taus = List.map (fun x -> TAny, Mark.get x) xs in
(* This type will be resolved in Scopelang.Desambiguation *) (* 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 Expr.make_abs (Array.of_list vs) (rec_helper ~local_vars e2) taus pos
in in
Expr.eapp fn [rec_helper e1] emark Expr.eapp ~f ~args:[rec_helper e1] ~tys:[] emark
| StructLit (((path, s_name), _), fields) -> | StructLit (((path, s_name), _), fields) ->
let ctxt = Name_resolution.module_ctx ctxt path in let ctxt = Name_resolution.module_ctx ctxt path in
let s_uid = let s_uid =
@ -606,15 +626,14 @@ let rec translate_expr
[TAny, pos] [TAny, pos]
pos pos
in in
Expr.eapp Expr.eappop
(Expr.eop ~op:
(match op with (match op with
| S.Map _ -> Map | S.Map _ -> Map
| S.Filter _ -> Filter | S.Filter _ -> Filter
| _ -> assert false) | _ -> assert false)
[TAny, pos; TAny, pos] ~tys:[TAny, pos; TAny, pos]
emark) ~args:[f_pred; collection] emark
[f_pred; collection] emark
| CollectionOp | CollectionOp
( S.AggregateArgExtremum { max; default; f = param_name, predicate }, ( S.AggregateArgExtremum { max; default; f = param_name, predicate },
collection ) -> collection ) ->
@ -640,19 +659,21 @@ let rec translate_expr
rely on returning tuples here *) rely on returning tuples here *)
Expr.make_abs [| v1; v2 |] Expr.make_abs [| v1; v2 |]
(Expr.eifthenelse (Expr.eifthenelse
(Expr.eapp (Expr.eappop ~op:cmp_op
(Expr.eop cmp_op ~tys:[TAny, pos_dft; TAny, pos_dft]
[TAny, pos_dft; TAny, pos_dft] ~args:
(Untyped { pos = pos_dft })) [
[Expr.eapp f_pred [x1] emark; Expr.eapp f_pred [x2] emark] Expr.eapp ~f:f_pred ~args:[x1] ~tys:[] emark;
Expr.eapp ~f:f_pred ~args:[x2] ~tys:[] emark;
]
emark) emark)
x1 x2 emark) x1 x2 emark)
[TAny, pos; TAny, pos] [TAny, pos; TAny, pos]
pos pos
in in
Expr.eapp Expr.eappop ~op:Reduce
(Expr.eop Reduce [TAny, pos; TAny, pos; TAny, pos] emark) ~tys:[TAny, pos; TAny, pos; TAny, pos]
[reduce_f; default; collection] ~args:[reduce_f; default; collection]
emark emark
| CollectionOp | CollectionOp
(((Exists { predicate } | Forall { predicate }) as op), collection) -> (((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 let acc = Expr.make_var acc_var (Untyped { pos = Mark.get param0 }) in
Expr.eabs Expr.eabs
(Expr.bind [| acc_var; param |] (Expr.bind [| acc_var; param |]
(Expr.eapp (translate_binop op pos) (translate_binop op pos acc (rec_helper ~local_vars predicate)))
[acc; rec_helper ~local_vars predicate]
emark))
[TAny, pos; TAny, pos] [TAny, pos; TAny, pos]
emark emark
in in
Expr.eapp Expr.eappop ~op:Fold
(Expr.eop Fold [TAny, pos; TAny, pos; TAny, pos] emark) ~tys:[TAny, pos; TAny, pos; TAny, pos]
[f; init; collection] emark ~args:[f; init; collection] emark
| CollectionOp (AggregateExtremum { max; default }, collection) -> | CollectionOp (AggregateExtremum { max; default }, collection) ->
let collection = rec_helper collection in let collection = rec_helper collection in
let default = rec_helper default 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 = let op_f =
(* fun x1 x2 -> if op x1 x2 then x1 else x2 *) (* fun x1 x2 -> if op x1 x2 then x1 else x2 *)
let vname = if max then "max" else "min" in 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 x1 = Expr.make_var v1 emark in
let x2 = Expr.make_var v2 emark in let x2 = Expr.make_var v2 emark in
Expr.make_abs [| v1; v2 |] 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] [TAny, pos; TAny, pos]
pos pos
in in
Expr.eapp Expr.eappop ~op:Reduce
(Expr.eop Reduce [TAny, pos; TAny, pos; TAny, pos] emark) ~tys:[TAny, pos; TAny, pos; TAny, pos]
[op_f; default; collection] ~args:[op_f; default; collection]
emark emark
| CollectionOp (AggregateSum { typ }, collection) -> | CollectionOp (AggregateSum { typ }, collection) ->
let collection = rec_helper collection in let collection = rec_helper collection in
@ -722,13 +741,13 @@ let rec translate_expr
let x1 = Expr.make_var v1 emark in let x1 = Expr.make_var v1 emark in
let x2 = Expr.make_var v2 emark in let x2 = Expr.make_var v2 emark in
Expr.make_abs [| v1; v2 |] 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] [TAny, pos; TAny, pos]
pos pos
in in
Expr.eapp Expr.eappop ~op:Reduce
(Expr.eop Reduce [TAny, pos; TAny, pos; TAny, pos] emark) ~tys:[TAny, pos; TAny, pos; TAny, pos]
[op_f; Expr.elit default_lit emark; collection] ~args:[op_f; Expr.elit default_lit emark; collection]
emark emark
| MemCollection (member, collection) -> | MemCollection (member, collection) ->
let param_var = Var.make "collection_member" in 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 acc = Expr.make_var acc_var emark in
let f_body = let f_body =
let member = rec_helper member in let member = rec_helper member in
Expr.eapp Expr.eappop ~op:Or
(Expr.eop Or [TLit TBool, pos; TLit TBool, pos] emark) ~tys:[TLit TBool, pos; TLit TBool, pos]
[ ~args:
Expr.eapp [
(Expr.eop Eq [TAny, pos; TAny, pos] emark) Expr.eappop ~op:Eq
[member; param] emark; ~tys:[TAny, pos; TAny, pos]
acc; ~args:[member; param] emark;
] acc;
]
emark emark
in in
let f = let f =
@ -755,18 +775,9 @@ let rec translate_expr
[TLit TBool, pos; TAny, pos] [TLit TBool, pos; TAny, pos]
emark emark
in in
Expr.eapp Expr.eappop ~op:Fold
(Expr.eop Fold [TAny, pos; TAny, pos; TAny, pos] emark) ~tys:[TAny, pos; TAny, pos; TAny, pos]
[f; init; collection] emark ~args:[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
and disambiguate_match_and_build_expression and disambiguate_match_and_build_expression
(scope : ScopeName.t option) (scope : ScopeName.t option)
@ -913,12 +924,9 @@ let merge_conditions
(default_pos : Pos.t) : Ast.expr boxed = (default_pos : Pos.t) : Ast.expr boxed =
match precond, cond with match precond, cond with
| Some precond, Some cond -> | Some precond, Some cond ->
let op_term = Expr.eappop ~op:And
Expr.eop And ~tys:[TLit TBool, default_pos; TLit TBool, default_pos]
[TLit TBool, default_pos; TLit TBool, default_pos] ~args:[precond; cond] (Mark.get cond)
(Mark.get cond)
in
Expr.eapp op_term [precond; cond] (Mark.get cond)
| Some precond, None -> Mark.remove precond, Untyped { pos = default_pos } | Some precond, None -> Mark.remove precond, Untyped { pos = default_pos }
| None, Some cond -> cond | None, Some cond -> cond
| None, None -> Expr.elit (LBool true) (Untyped { pos = default_pos }) | 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_typ t = Name_resolution.process_type ctxt t in
let translate_tbase (tbase, m) = translate_typ (Base tbase, m) in let translate_tbase (tbase, m) = translate_typ (Base tbase, m) in
let typ = translate_typ def.S.topdef_type in let typ = translate_typ def.S.topdef_type in
Message.emit_debug "TTYP: %a@." Print.typ_debug typ;
let expr_opt = let expr_opt =
match def.S.topdef_expr, def.S.topdef_args with match def.S.topdef_expr, def.S.topdef_args with
| None, _ -> None | None, _ -> None
@ -1297,6 +1306,17 @@ let process_topdef
in in
let body = translate_expr None None ctxt local_vars e in let body = translate_expr None None ctxt local_vars e in
let args, tys = List.split args_tys 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 = let e =
Expr.make_abs Expr.make_abs
(Array.of_list (List.map Mark.remove args)) (Array.of_list (List.map Mark.remove args))

104
compiler/lcalc/ast.ml
View File

@ -20,107 +20,3 @@ type 'm naked_expr = (lcalc, 'm) naked_gexpr
and 'm expr = (lcalc, 'm) gexpr and 'm expr = (lcalc, 'm) gexpr
type 'm program = 'm expr Shared_ast.program 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

79
compiler/lcalc/ast.mli
View File

@ -24,82 +24,3 @@ type 'm naked_expr = (lcalc, 'm) naked_gexpr
and 'm expr = (lcalc, 'm) gexpr and 'm expr = (lcalc, 'm) gexpr
type 'm program = 'm expr Shared_ast.program 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

107
compiler/lcalc/closure_conversion.ml
View File

@ -39,8 +39,7 @@ let rec transform_closures_expr :
let m = Mark.get e in let m = Mark.get e in
match Mark.remove e with match Mark.remove e with
| EStruct _ | EStructAccess _ | ETuple _ | ETupleAccess _ | EInj _ | EArray _ | EStruct _ | EStructAccess _ | ETuple _ | ETupleAccess _ | EInj _ | EArray _
| ELit _ | EExternal _ | EAssert _ | EOp _ | EIfThenElse _ | ERaise _ | ELit _ | EExternal _ | EAssert _ | EIfThenElse _ | ERaise _ | ECatch _ ->
| ECatch _ ->
Expr.map_gather ~acc:Var.Set.empty ~join:Var.Set.union Expr.map_gather ~acc:Var.Set.empty ~join:Var.Set.union
~f:(transform_closures_expr ctx) ~f:(transform_closures_expr ctx)
e e
@ -59,7 +58,8 @@ let rec transform_closures_expr :
let e = let e =
Expr.eabs Expr.eabs
(Expr.bind args (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 targs m
in in
let boxed = let boxed =
@ -104,7 +104,7 @@ let rec transform_closures_expr :
(free_vars, EnumConstructor.Map.empty) (free_vars, EnumConstructor.Map.empty)
in in
free_vars, Expr.ematch ~e:new_e ~name ~cases:new_cases m 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-binding, we should not close these *)
let vars, body = Bindlib.unmbind binder in let vars, body = Bindlib.unmbind binder in
let free_vars, new_body = (transform_closures_expr ctx) body in let free_vars, new_body = (transform_closures_expr ctx) body in
@ -120,7 +120,9 @@ let rec transform_closures_expr :
args (free_vars, []) args (free_vars, [])
in in
( free_vars, ( 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 } -> | EAbs { binder; tys } ->
(* λ x.t *) (* λ x.t *)
let binder_mark = m in 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 env = from_closure_env env in let arg0 = env.0 in ... *)
let new_closure_body = let new_closure_body =
Expr.make_let_in closure_env_var any_ty Expr.make_let_in closure_env_var any_ty
(Expr.eapp (Expr.eappop ~op:Operator.FromClosureEnv
(Expr.eop Operator.FromClosureEnv ~tys:[TClosureEnv, binder_pos]
[TClosureEnv, binder_pos] ~args:[Expr.evar closure_env_arg_var binder_mark]
binder_mark)
[Expr.evar closure_env_arg_var binder_mark]
binder_mark) binder_mark)
(Expr.make_multiple_let_in (Expr.make_multiple_let_in
(Array.of_list extra_vars_list) (Array.of_list extra_vars_list)
@ -155,9 +155,9 @@ let rec transform_closures_expr :
(List.mapi (List.mapi
(fun i _ -> (fun i _ ->
Expr.etupleaccess Expr.etupleaccess
(Expr.evar closure_env_var binder_mark) ~e:(Expr.evar closure_env_var binder_mark)
i ~index:i
(List.length extra_vars_list) ~size:(List.length extra_vars_list)
binder_mark) binder_mark)
extra_vars_list) extra_vars_list)
new_body binder_pos) new_body binder_pos)
@ -178,29 +178,27 @@ let rec transform_closures_expr :
(Expr.etuple (Expr.etuple
((Bindlib.box_var code_var, binder_mark) ((Bindlib.box_var code_var, binder_mark)
:: [ :: [
Expr.eapp Expr.eappop ~op:Operator.ToClosureEnv
(Expr.eop Operator.ToClosureEnv ~tys:[TAny, Expr.pos e]
[TAny, Expr.pos e] ~args:
(Mark.get e)) [
[ (if extra_vars_list = [] then Expr.elit LUnit binder_mark
(if extra_vars_list = [] then Expr.elit LUnit binder_mark else
else Expr.etuple
Expr.etuple (List.map
(List.map (fun extra_var ->
(fun extra_var -> Bindlib.box_var extra_var, binder_mark)
Bindlib.box_var extra_var, binder_mark) extra_vars_list)
extra_vars_list) m);
m); ]
]
(Mark.get e); (Mark.get e);
]) ])
m) m)
(Expr.pos e) ) (Expr.pos e) )
| EApp | EAppOp
{ {
f = op = (HandleDefaultOpt | Fold | Map | Filter | Reduce) as op;
(EOp { op = HandleDefaultOpt | Fold | Map | Filter | Reduce; _ }, _) tys;
as f;
args; args;
} -> } ->
(* Special case for some operators: its arguments shall remain thunks (which (* 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) Var.Set.union free_vars new_free_vars, new_arg :: new_args)
args (Var.Set.empty, []) args (Var.Set.empty, [])
in in
free_vars, Expr.eapp (Expr.box f) new_args (Mark.get e) free_vars, Expr.eappop ~op ~tys ~args:new_args (Mark.get e)
| EApp { f = EOp _, _; _ } -> | EAppOp _ ->
(* This corresponds to an operator call, which we don't want to transform*) (* This corresponds to an operator call, which we don't want to transform *)
Expr.map_gather ~acc:Var.Set.empty ~join:Var.Set.union Expr.map_gather ~acc:Var.Set.empty ~join:Var.Set.union
~f:(transform_closures_expr ctx) ~f:(transform_closures_expr ctx)
e 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 (* This corresponds to a scope or toplevel function call, which we don't
want to transform*) want to transform *)
let free_vars, new_args = let free_vars, new_args =
List.fold_right List.fold_right
(fun arg (free_vars, new_args) -> (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) Var.Set.union free_vars new_free_vars, new_arg :: new_args)
args (Var.Set.empty, []) args (Var.Set.empty, [])
in in
free_vars, Expr.eapp (Expr.evar v f_m) new_args m free_vars, Expr.eapp ~f:(Expr.evar v f_m) ~args:new_args ~tys m
| EApp { f = e1; args } -> | EApp { f = e1; args; tys } ->
let free_vars, new_e1 = (transform_closures_expr ctx) e1 in let free_vars, new_e1 = (transform_closures_expr ctx) e1 in
let code_env_var = Var.make "code_and_env" in let code_env_var = Var.make "code_and_env" in
let env_var = Var.make "env" in let env_var = Var.make "env" in
@ -258,13 +257,18 @@ let rec transform_closures_expr :
let m1 = Mark.get e1 in let m1 = Mark.get e1 in
Expr.make_let_in code_var Expr.make_let_in code_var
(TAny, Expr.pos e) (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 (Expr.make_let_in env_var
(TAny, Expr.pos e) (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 (Expr.eapp
(Bindlib.box_var code_var, m1) ~f:(Bindlib.box_var code_var, m1)
((Bindlib.box_var env_var, m1) :: new_args) ~args:((Bindlib.box_var env_var, m1) :: new_args)
~tys:((TClosureEnv, Expr.pos e1) :: tys)
m) m)
(Expr.pos e)) (Expr.pos e))
(Expr.pos e) (Expr.pos e)
@ -466,7 +470,7 @@ let rec hoist_closures_expr :
(collected_closures, EnumConstructor.Map.empty) (collected_closures, EnumConstructor.Map.empty)
in in
collected_closures, Expr.ematch ~e:new_e ~name ~cases:new_cases m 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-binding, we should not close these *)
let vars, body = Bindlib.unmbind binder in let vars, body = Bindlib.unmbind binder in
let collected_closures, new_body = let collected_closures, new_body =
@ -483,12 +487,13 @@ let rec hoist_closures_expr :
args (collected_closures, []) args (collected_closures, [])
in in
( collected_closures, ( collected_closures,
Expr.eapp (Expr.eabs new_binder (tys_as_tanys tys) e1_pos) new_args m ) Expr.eapp
| EApp ~f:(Expr.eabs new_binder (tys_as_tanys tys) e1_pos)
~args:new_args ~tys m )
| EAppOp
{ {
f = op = (HandleDefaultOpt | Fold | Map | Filter | Reduce) as op;
(EOp { op = HandleDefaultOpt | Fold | Map | Filter | Reduce; _ }, _) tys;
as f;
args; args;
} -> } ->
(* Special case for some operators: its arguments closures thunks because if (* 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) new_collected_closures @ collected_closures, new_arg :: new_args)
args ([], []) args ([], [])
in 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; _ } -> | EAbs { tys; _ } ->
(* this is the closure we want to hoist*) (* this is the closure we want to hoist*)
let closure_var = Var.make ("closure_" ^ name_context) in let closure_var = Var.make ("closure_" ^ name_context) in
@ -534,8 +539,8 @@ let rec hoist_closures_expr :
], ],
Expr.make_var closure_var m ) Expr.make_var closure_var m )
| EApp _ | EStruct _ | EStructAccess _ | ETuple _ | ETupleAccess _ | EInj _ | EApp _ | EStruct _ | EStructAccess _ | ETuple _ | ETupleAccess _ | EInj _
| EArray _ | ELit _ | EAssert _ | EOp _ | EIfThenElse _ | ERaise _ | ECatch _ | EArray _ | ELit _ | EAssert _ | EAppOp _ | EIfThenElse _ | ERaise _
| EVar _ -> | ECatch _ | EVar _ ->
Expr.map_gather ~acc:[] ~join:( @ ) ~f:(hoist_closures_expr name_context) e Expr.map_gather ~acc:[] ~join:( @ ) ~f:(hoist_closures_expr name_context) e
| EExternal _ -> failwith "unimplemented" | EExternal _ -> failwith "unimplemented"
| _ -> . | _ -> .

24
compiler/lcalc/compile_with_exceptions.ml
View File

@ -33,16 +33,15 @@ let rec translate_default
in in
let pos = Expr.mark_pos mark_default in let pos = Expr.mark_pos mark_default in
let exceptions = let exceptions =
Expr.make_app Expr.eappop ~op:Op.HandleDefault
(Expr.eop Op.HandleDefault ~tys:[TAny, pos; TAny, pos; TAny, pos]
[TAny, pos; TAny, pos; TAny, pos] ~args:
(Expr.no_mark mark_default)) [
[ Expr.earray exceptions mark_default;
Expr.earray exceptions mark_default; Expr.thunk_term (translate_expr just) (Mark.get just);
Expr.thunk_term (translate_expr just) (Mark.get just); Expr.thunk_term (translate_expr cons) (Mark.get cons);
Expr.thunk_term (translate_expr cons) (Mark.get cons); ]
] mark_default
pos
in in
exceptions exceptions
@ -57,7 +56,10 @@ and translate_expr (e : 'm D.expr) : 'm A.expr boxed =
| EDefault { excepts; just; cons } -> | EDefault { excepts; just; cons } ->
translate_default excepts just cons (Mark.get e) translate_default excepts just cons (Mark.get e)
| EPureDefault e -> translate_expr 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 _ | ( ELit _ | EApp _ | EArray _ | EVar _ | EExternal _ | EAbs _ | EIfThenElse _
| ETuple _ | ETupleAccess _ | EInj _ | EAssert _ | EStruct _ | ETuple _ | ETupleAccess _ | EInj _ | EAssert _ | EStruct _
| EStructAccess _ | EMatch _ ) as e -> | EStructAccess _ | EMatch _ ) as e ->

57
compiler/lcalc/compile_without_exceptions.ml
View File

@ -59,36 +59,55 @@ let rec translate_default
let exceptions = List.map translate_expr exceptions in let exceptions = List.map translate_expr exceptions in
let pos = Expr.mark_pos mark_default in let pos = Expr.mark_pos mark_default in
let exceptions = let exceptions =
Expr.make_app Expr.eappop ~op:Op.HandleDefaultOpt
(Expr.eop Op.HandleDefaultOpt ~tys:[TAny, pos; TAny, pos; TAny, pos]
[TAny, pos; TAny, pos; TAny, pos] ~args:
(Expr.no_mark mark_default)) [
[ Expr.earray exceptions mark_default;
Expr.earray exceptions mark_default; (* In call-by-value programming languages, as lcalc, arguments are
(* In call-by-value programming languages, as lcalc, arguments are evalulated before calling the function. Since we don't want to
evalulated before calling the function. Since we don't want to execute the justification and conclusion while before checking
execute the justification and conclusion while before checking every every exceptions, we need to thunk them. *)
exceptions, we need to thunk them. *) Expr.thunk_term (translate_expr just) (Mark.get just);
Expr.thunk_term (translate_expr just) (Mark.get just); Expr.thunk_term (translate_expr cons) (Mark.get cons);
Expr.thunk_term (translate_expr cons) (Mark.get cons); ]
] mark_default
pos
in in
exceptions exceptions
and translate_expr (e : 'm D.expr) : 'm A.expr boxed = and translate_expr (e : 'm D.expr) : 'm A.expr boxed =
let mark = Mark.get e in let mark = Mark.get e in
match Mark.remove e with 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 -> | 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 } -> | EDefault { excepts; just; cons } ->
translate_default excepts just cons (Mark.get e) 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 (* As we need to translate types as well as terms, we cannot simply use
[Expr.map] for terms that contains types. *) [Expr.map] for terms that contains types. *)
| EOp { op; tys } -> | EAppOp { op; tys; args } ->
Expr.eop (Operator.translate op) (List.map translate_typ tys) mark Expr.eappop ~op:(Operator.translate op)
~tys:(List.map translate_typ tys)
~args:(List.map translate_expr args)
mark
| EAbs { binder; tys } -> | EAbs { binder; tys } ->
let vars, body = Bindlib.unmbind binder in let vars, body = Bindlib.unmbind binder in
let body = translate_expr body in let body = translate_expr body in

48
compiler/lcalc/to_ocaml.ml
View File

@ -235,9 +235,7 @@ let format_var (fmt : Format.formatter) (v : 'm Var.t) : unit =
let needs_parens (e : 'm expr) : bool = let needs_parens (e : 'm expr) : bool =
match Mark.remove e with match Mark.remove e with
| EApp { f = EAbs _, _; _ } | EApp { f = EAbs _, _; _ } | ELit (LBool _ | LUnit) | EVar _ | ETuple _ ->
| ELit (LBool _ | LUnit)
| EVar _ | ETuple _ | EOp _ ->
false false
| _ -> true | _ -> true
@ -349,7 +347,7 @@ let rec format_expr (ctx : decl_ctx) (fmt : Format.formatter) (e : 'm expr) :
e)) e))
(EnumConstructor.Map.bindings cases) (EnumConstructor.Map.bindings cases)
| ELit l -> Format.fprintf fmt "%a" format_lit (Mark.add (Expr.pos e) l) | 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, body = Bindlib.unmbind binder in
let xs_tau = List.map2 (fun x tau -> x, tau) (Array.to_list xs) tys 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 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 xs_tau format_expr body
| EApp | EApp
{ {
f = EApp { f = EOp { op = Log (BeginCall, info); _ }, _; args = [f] }, _; f = EAppOp { op = Log (BeginCall, info); args = [f]; _ }, _;
args = [arg]; args = [arg];
_;
} }
when Cli.globals.trace -> when Cli.globals.trace ->
Format.fprintf fmt "(log_begin_call@ %a@ %a)@ %a" format_uid_list info Format.fprintf fmt "(log_begin_call@ %a@ %a)@ %a" format_uid_list info
format_with_parens f format_with_parens arg format_with_parens f format_with_parens arg
| EApp | EAppOp { op = Log (VarDef var_def_info, info); args = [arg1]; _ }
{ f = EOp { op = Log (VarDef var_def_info, info); _ }, _; args = [arg1] }
when Cli.globals.trace -> when Cli.globals.trace ->
Format.fprintf fmt Format.fprintf fmt
"(log_variable_definition@ %a@ {io_input=%s;@ io_output=%b}@ (%a)@ %a)" "(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_io_output typ_embedding_name
(var_def_info.log_typ, Pos.no_pos) (var_def_info.log_typ, Pos.no_pos)
format_with_parens arg1 format_with_parens arg1
| EApp { f = EOp { op = Log (PosRecordIfTrueBool, _); _ }, m; args = [arg1] } | EAppOp { op = Log (PosRecordIfTrueBool, _); args = [arg1]; _ }
when Cli.globals.trace -> when Cli.globals.trace ->
let pos = Expr.mark_pos m in let pos = Expr.pos e in
Format.fprintf fmt Format.fprintf fmt
"(log_decision_taken@ @[<hov 2>{filename = \"%s\";@ start_line=%d;@ \ "(log_decision_taken@ @[<hov 2>{filename = \"%s\";@ start_line=%d;@ \
start_column=%d;@ end_line=%d; end_column=%d;@ law_headings=%a}@]@ %a)" 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_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_end_line pos) (Pos.get_end_column pos) format_string_list
(Pos.get_law_info pos) format_with_parens arg1 (Pos.get_law_info pos) format_with_parens arg1
| EApp { f = EOp { op = Log (EndCall, info); _ }, _; args = [arg1] } | EAppOp { op = Log (EndCall, info); args = [arg1]; _ } when Cli.globals.trace
when Cli.globals.trace -> ->
Format.fprintf fmt "(log_end_call@ %a@ %a)" format_uid_list info Format.fprintf fmt "(log_end_call@ %a@ %a)" format_uid_list info
format_with_parens arg1 format_with_parens arg1
| EApp { f = EOp { op = Log _; _ }, _; args = [arg1] } -> | EAppOp { op = Log _; args = [arg1]; _ } ->
Format.fprintf fmt "%a" format_with_parens arg1 Format.fprintf fmt "%a" format_with_parens arg1
| EApp | EAppOp { op = (HandleDefault | HandleDefaultOpt) as op; args; _ } ->
{ let pos = Expr.pos e in
f = EOp { op = (HandleDefault | HandleDefaultOpt) as op; _ }, pos;
args;
} ->
Format.fprintf fmt Format.fprintf fmt
"@[<hov 2>%s@ @[<hov 2>{filename = \"%s\";@ start_line=%d;@ \ "@[<hov 2>%s@ @[<hov 2>{filename = \"%s\";@ start_line=%d;@ \
start_column=%d;@ end_line=%d; end_column=%d;@ law_headings=%a}@]@ %a@]" start_column=%d;@ end_line=%d; end_column=%d;@ law_headings=%a}@]@ %a@]"
(Print.operator_to_string op) (Print.operator_to_string op)
(Pos.get_file (Expr.mark_pos pos)) (Pos.get_file pos) (Pos.get_start_line pos) (Pos.get_start_column pos)
(Pos.get_start_line (Expr.mark_pos pos)) (Pos.get_end_line pos) (Pos.get_end_column pos) format_string_list
(Pos.get_start_column (Expr.mark_pos pos)) (Pos.get_law_info 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))
(Format.pp_print_list (Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ") ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")
format_with_parens) format_with_parens)
args args
| EApp { f; args } -> | EApp { f; args; _ } ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" format_with_parens f Format.fprintf fmt "@[<hov 2>%a@ %a@]" format_with_parens f
(Format.pp_print_list (Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ") ~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 Format.fprintf fmt
"@[<hov 2> if@ @[<hov 2>%a@]@ then@ @[<hov 2>%a@]@ else@ @[<hov 2>%a@]@]" "@[<hov 2> if@ @[<hov 2>%a@]@ then@ @[<hov 2>%a@]@ else@ @[<hov 2>%a@]@]"
format_with_parens cond format_with_parens etrue format_with_parens efalse 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 "@[<hov 2>%s@ %a@]" (Operator.name op)
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")
format_with_parens)
args
| EAssert e' -> | EAssert e' ->
Format.fprintf fmt Format.fprintf fmt
"@[<hov 2>if@ %a@ then@ ()@ else@ raise (AssertionFailed @[<hov \ "@[<hov 2>if@ %a@ then@ ()@ else@ raise (AssertionFailed @[<hov \

161
compiler/plugins/explain.ml
View File

@ -130,40 +130,22 @@ let rec bool_negation e =
match Expr.skip_wrappers e with match Expr.skip_wrappers e with
| ELit (LBool true), m -> ELit (LBool false), m | ELit (LBool true), m -> ELit (LBool false), m
| ELit (LBool false), m -> ELit (LBool true), m | ELit (LBool false), m -> ELit (LBool true), m
| EApp { f = EOp { op = Op.Not; _ }, _; args = [(e, _)] }, m -> e, m | EAppOp { op = Op.Not; args = [(e, _)] }, m -> e, m
| (EApp { f = EOp { op; tys }, mop; args = [e1; e2] }, m) as e -> ( | (EAppOp { op; tys; args = [e1; e2] }, m) as e -> (
match op with match op with
| Op.And -> | Op.And ->
( EApp EAppOp { op = Op.Or; tys; args = [bool_negation e1; bool_negation e2] }, m
{
f = EOp { op = Op.Or; tys }, mop;
args = [bool_negation e1; bool_negation e2];
},
m )
| Op.Or -> | Op.Or ->
( EApp ( EAppOp { op = Op.And; tys; args = [bool_negation e1; bool_negation e2] },
{
f = EOp { op = Op.And; tys }, mop;
args = [bool_negation e1; bool_negation e2];
},
m ) m )
| op -> ( | op -> (
match neg_op op with 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 -> | None ->
( EApp ( EAppOp { op = Op.Not; tys = [TLit TBool, Expr.mark_pos m]; args = [e] },
{
f = EOp { op = Op.Not; tys = [TLit TBool, Expr.mark_pos m] }, m;
args = [e];
},
m ))) m )))
| (_, m) as e -> | (_, m) as e ->
( EApp EAppOp { op = Op.Not; tys = [TLit TBool, Expr.mark_pos m]; args = [e] }, m
{
f = EOp { op = Op.Not; tys = [TLit TBool, Expr.mark_pos m] }, m;
args = [e];
},
m )
let rec lazy_eval : decl_ctx -> Env.t -> laziness_level -> expr -> expr * Env.t 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 let r, env1 = lazy_eval ctx env1 llevel e in
env_elt.reduced <- r, env1; env_elt.reduced <- r, env1;
r, Env.join env env1 r, Env.join env env1
| EApp { f; args }, m -> ( | EAppOp { op; args; tys }, m -> (
if if
(not llevel.eval_default) (not llevel.eval_default)
&& not (List.equal Expr.equal args [ELit LUnit, m]) && not (List.equal Expr.equal args [ELit LUnit, m])
(* Applications to () encode thunked default terms *) (* Applications to () encode thunked default terms *)
then e0, env then e0, env
else else
match eval_to_value env f with match op with
| (EAbs { binder; _ }, _), env -> | (Op.Map | Op.Filter | Op.Reduce | Op.Fold | Op.Length) as op -> (
let vars, body = Bindlib.unmbind binder in (* when not llevel.eval_op *)
log "@[<v 2>@[<hov 4>{";
let env =
Seq.fold_left2
(fun env1 var e ->
log "@[<hov 2>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 "@]@[<hov 4>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 *) ) -> (
(* Distribute collection operations to the terms rather than use their (* Distribute collection operations to the terms rather than use their
runtime implementations *) runtime implementations *)
let arr = List.hd (List.rev args) in 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 let aty = List.hd (List.rev tys) in
match eval_to_value env arr with match eval_to_value env arr with
| (EArray elts, _), env -> | (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 () = let empty_condition () =
(* Is the expression [length(arr) = 0] *) (* Is the expression [length(arr) = 0] *)
let pos = Expr.mark_pos m in let pos = Expr.mark_pos m in
( EApp ( EAppOp
{ {
f = op = Op.Eq_int_int;
( EOp tys = [TLit TInt, pos; TLit TInt, pos];
{
op = Op.Eq_int_int;
tys = [TLit TInt, pos; TLit TInt, pos];
},
m );
args = args =
[ [
( EApp EAppOp { op = Op.Length; tys = [aty]; args = [arr] }, m;
{
f = EOp { op = Op.Length; tys = [aty] }, m;
args = [arr];
},
m );
ELit (LInt (Runtime.integer_of_int 0)), 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 -> | Op.Reduce, [f; _; _], elt0 :: elts ->
let e = let e =
List.fold_left List.fold_left
(fun acc elt -> EApp { f; args = [acc; elt] }, m) (fun acc elt -> EApp { f; args = [acc; elt]; tys = [] }, m)
elt0 elts elt0 elts
in in
e, env e, env
| Op.Fold, [f; base; _], elts -> | Op.Fold, [f; base; _], elts ->
let e = let e =
List.fold_left List.fold_left
(fun acc elt -> EApp { f; args = [acc; elt] }, m) (fun acc elt -> EApp { f; args = [acc; elt]; tys = [] }, m)
base elts base elts
in in
e, env 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 (* We did a transformation (removing the outer operator), but further
evaluation may be needed to guarantee that [llevel] is reached *) evaluation may be needed to guarantee that [llevel] is reached *)
lazy_eval ctx env { llevel with eval_match = true } e lazy_eval ctx env { llevel with eval_match = true } e
| _ -> (EApp { f; args }, m), env) | _ -> (EAppOp { op; args; tys }, m), env)
| ((EOp { op; _ }, m) as f), env -> | _ ->
let env, args = let env, args =
List.fold_left_map List.fold_left_map
(fun env e -> (fun env e ->
@ -301,7 +254,7 @@ let rec lazy_eval : decl_ctx -> Env.t -> laziness_level -> expr -> expr * Env.t
env, e) env, e)
env args env args
in 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 else
let renv = ref env in let renv = ref env in
(* Dirty workaround returning env and conds from evaluate_operator *) (* 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. *) messages so we don't care. *)
args args
in in
e, !renv e, !renv)
(* fixme: this forwards eempty *) (* 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 "@[<v 2>@[<hov 4>{";
let env =
Seq.fold_left2
(fun env1 var e ->
log "@[<hov 2>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 "@]@[<hov 4>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) | 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 _), _ -> | (EStruct _ | ETuple _ | EInj _ | EArray _), _ ->
if not llevel.eval_struct then e0, env if not llevel.eval_struct then e0, env
else else
@ -358,7 +333,13 @@ let rec lazy_eval : decl_ctx -> Env.t -> laziness_level -> expr -> expr * Env.t
concise expression to express that *) concise expression to express that *)
let e1, env = let e1, env =
lazy_eval ctx env llevel 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 in
add_condition ~condition e1, env add_condition ~condition e1, env
| e, _ -> error e "Invalid match argument %a" Expr.format e) | 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 = let rec aux env g e =
(* lazy_eval ctx env (result_level base_vars) e *) (* lazy_eval ctx env (result_level base_vars) e *)
match Expr.skip_wrappers e with match Expr.skip_wrappers e with
| ( EApp | EAppOp { op = ToRat_int | ToRat_mon | ToMoney_rat; args = [arg]; _ }, _ ->
{
f = EOp { op = ToRat_int | ToRat_mon | ToMoney_rat; _ }, _;
args = [arg];
},
_ ) ->
aux env g arg aux env g arg
(* we skip conversions *) (* we skip conversions *)
| ELit l, _ -> | ELit l, _ ->
@ -576,7 +552,7 @@ let to_graph ctx env expr =
let child, env = (Env.find var env).base in let child, env = (Env.find var env).base in
let g, child_v = aux env g child in let g, child_v = aux env g child in
G.add_edge g v child_v, v G.add_edge g v child_v, v
| EApp { f = EOp { op = _; _ }, _; args }, _ -> | EAppOp { op = _; args; _ }, _ ->
let v = G.V.create e in let v = G.V.create e in
let g = G.add_vertex g v in let g = G.add_vertex g v in
let g, children = List.fold_left_map (aux env) g args in let g, children = List.fold_left_map (aux env) g args in
@ -682,12 +658,8 @@ let program_to_graph
in in
let e = Mark.set m (Expr.skip_wrappers e) in let e = Mark.set m (Expr.skip_wrappers e) in
match e with match e with
| ( EApp | EAppOp { op = ToRat_int | ToRat_mon | ToMoney_rat; args = [arg]; tys }, _
{ ->
f = EOp { op = ToRat_int | ToRat_mon | ToMoney_rat; _ }, _;
args = [arg];
},
_ ) ->
aux parent (g, var_vertices, env0) (Mark.set m arg) aux parent (g, var_vertices, env0) (Mark.set m arg)
(* we skip conversions *) (* we skip conversions *)
| ELit l, _ -> | ELit l, _ ->
@ -725,12 +697,7 @@ let program_to_graph
let v = G.V.create e in let v = G.V.create e in
let g = G.add_vertex g v in let g = G.add_vertex g v in
(g, var_vertices, env), v)) (g, var_vertices, env), v))
| ( EApp | EAppOp { op = Map | Filter | Reduce | Fold; args = _ :: args; _ }, _ ->
{
f = EOp { op = Map | Filter | Reduce | Fold; _ }, _;
args = _ :: args;
},
_ ) ->
(* First argument (which is a function) is ignored *) (* First argument (which is a function) is ignored *)
let v = G.V.create e in let v = G.V.create e in
let g = G.add_vertex g v in let g = G.add_vertex g v in
@ -739,7 +706,7 @@ let program_to_graph
in in
( (List.fold_left (fun g -> G.add_edge g v) g children, var_vertices, env), ( (List.fold_left (fun g -> G.add_edge g v) g children, var_vertices, env),
v ) v )
| EApp { f = EOp { op; _ }, _; args = [lhs; rhs] }, _ -> | EAppOp { op; args = [lhs; rhs]; _ }, _ ->
let v = G.V.create e in let v = G.V.create e in
let g = G.add_vertex g v in let g = G.add_vertex g v in
let (g, var_vertices, env), lhs = let (g, var_vertices, env), lhs =
@ -771,7 +738,7 @@ let program_to_graph
(G.E.create v { side = rhs_label; condition = false } rhs) (G.E.create v { side = rhs_label; condition = false } rhs)
in in
(g, var_vertices, env), v (g, var_vertices, env), v
| EApp { f = EOp { op = _; _ }, _; args }, _ -> | EAppOp { op = _; args; _ }, _ ->
let v = G.V.create e in let v = G.V.create e in
let g = G.add_vertex g v in let g = G.add_vertex g v in
let (g, var_vertices, env), children = let (g, var_vertices, env), children =
@ -907,8 +874,7 @@ let rec graph_cleanup options g base_vars =
(fun v g -> (fun v g ->
let succ = G.succ g v in let succ = G.succ g v in
match G.V.label v, succ, List.map G.V.label succ with 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 = let g =
List.fold_left List.fold_left
(fun g e -> (fun g e ->
@ -965,8 +931,7 @@ let rec graph_cleanup options g base_vars =
(fun v g -> (fun v g ->
let succ = G.succ g v in let succ = G.succ g v in
match G.V.label v, succ, List.map G.V.label succ with 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 = let g =
List.fold_left List.fold_left
(fun g e -> (fun g e ->
@ -1254,7 +1219,7 @@ let to_dot lang ppf ctx env base_vars g ~base_src_url =
else (* Constants *) else (* Constants *)
[`Style `Filled; `Fillcolor 0x77aaff; `Shape `Note] [`Style `Filled; `Fillcolor 0x77aaff; `Shape `Note]
| EStruct _, _ | EArray _, _ -> [`Shape `Record] | EStruct _, _ | EArray _, _ -> [`Shape `Record]
| EApp { f = EOp { op; _ }, _; _ }, _ -> ( | EAppOp { op; _ }, _ -> (
match op_kind op with match op_kind op with
| `Sum | `Product | _ -> [`Shape `Box] (* | _ -> [] *)) | `Sum | `Product | _ -> [`Shape `Box] (* | _ -> [] *))
| _ -> []) | _ -> [])

61
compiler/plugins/lazy_interp.ml
View File

@ -89,7 +89,35 @@ let rec lazy_eval :
r; r;
v_env := r, env1); v_env := r, env1);
r, Env.join env 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 if
(not llevel.eval_default) (not llevel.eval_default)
&& not (List.equal Expr.equal args [ELit LUnit, m]) && 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 let e, env = lazy_eval ctx env llevel body in
log "@]}"; log "@]}";
e, env 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) | 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 _), _ -> | (EStruct _ | ETuple _ | EInj _ | EArray _), _ ->
if not llevel.eval_struct then e0, env if not llevel.eval_struct then e0, env
else else
@ -169,7 +174,9 @@ let rec lazy_eval :
match eval_to_value env e with match eval_to_value env e with
| (EInj { name = n; cons; e }, m), env when EnumName.equal name n -> | (EInj { name = n; cons; e }, m), env when EnumName.equal name n ->
lazy_eval ctx env llevel 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) | e, _ -> error e "Invalid match argument %a" Expr.format e)
| EDefault { excepts; just; cons }, m -> ( | EDefault { excepts; just; cons }, m -> (
let excs = 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)) (StructName.Map.find scope_arg_struct ctx.ctx_structs))
m m
in 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 lazy_eval ctx env
{ value_level with eval_struct = true; eval_op = false } { value_level with eval_struct = true; eval_op = false }
(Expr.unbox e_app) (Expr.unbox e_app)

2
compiler/scalc/ast.ml
View File

@ -52,7 +52,7 @@ and naked_expr =
| EArray : expr list -> naked_expr | EArray : expr list -> naked_expr
| ELit : lit -> naked_expr | ELit : lit -> naked_expr
| EApp : expr * expr list -> naked_expr | EApp : expr * expr list -> naked_expr
| EOp : operator -> naked_expr | EAppOp : operator * expr list -> naked_expr
type stmt = type stmt =
| SInnerFuncDef of VarName.t Mark.pos * func | SInnerFuncDef of VarName.t Mark.pos * func

17
compiler/scalc/from_lcalc.ml
View File

@ -65,7 +65,7 @@ let rec translate_expr (ctxt : 'm ctxt) (expr : 'm L.expr) : A.block * A.expr =
| EInj { e = e1; cons; name } -> | EInj { e = e1; cons; name } ->
let e1_stmts, new_e1 = translate_expr ctxt e1 in let e1_stmts, new_e1 = translate_expr ctxt e1 in
e1_stmts, (A.EInj (new_e1, cons, name), Expr.pos expr) 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 f_stmts, new_f = translate_expr ctxt f in
let args_stmts, new_args = let args_stmts, new_args =
List.fold_left 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) arg_stmts @ args_stmts, new_arg :: new_args)
([], []) args ([], []) args
in in
(* FIXME: what happens if [arg] is not a tuple but reduces to one ? *)
let new_args = List.rev new_args in let new_args = List.rev new_args in
f_stmts @ args_stmts, (A.EApp (new_f, new_args), Expr.pos expr) 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 -> | EArray args ->
let args_stmts, new_args = let args_stmts, new_args =
List.fold_left List.fold_left
@ -86,7 +98,6 @@ let rec translate_expr (ctxt : 'm ctxt) (expr : 'm L.expr) : A.block * A.expr =
in in
let new_args = List.rev new_args in let new_args = List.rev new_args in
args_stmts, (A.EArray new_args, Expr.pos expr) 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) | ELit l -> [], (A.ELit l, Expr.pos expr)
| _ -> | _ ->
let tmp_var = 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 *) (* Assertions are always encapsulated in a unit-typed let binding *)
let e_stmts, new_e = translate_expr ctxt e in let e_stmts, new_e = translate_expr ctxt e in
e_stmts @ [A.SAssert (Mark.remove new_e), Expr.pos block_expr] 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 *) (* This defines multiple local variables at the time *)
let binder_pos = Expr.mark_pos binder_mark in let binder_pos = Expr.mark_pos binder_mark in
let vars, body = Bindlib.unmbind binder in let vars, body = Bindlib.unmbind binder in

15
compiler/scalc/print.ml
View File

@ -66,15 +66,15 @@ let rec format_expr
Format.fprintf fmt "@[<hov 2>%a@ %a@]" EnumConstructor.format cons Format.fprintf fmt "@[<hov 2>%a@ %a@]" EnumConstructor.format cons
format_expr e format_expr e
| ELit l -> Print.lit fmt l | ELit l -> Print.lit fmt l
| EApp ((EOp ((Map | Filter) as op), _), [arg1; arg2]) -> | EAppOp (((Map | Filter) as op), [arg1; arg2]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" (Print.operator ~debug) op Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" (Print.operator ~debug) op
format_with_parens arg1 format_with_parens arg2 format_with_parens arg1 format_with_parens arg2
| EApp ((EOp op, _), [arg1; arg2]) -> | EAppOp (op, [arg1; arg2]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" format_with_parens arg1 Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" format_with_parens arg1
(Print.operator ~debug) op format_with_parens arg2 (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 Format.fprintf fmt "%a" format_with_parens arg1
| EApp ((EOp op, _), [arg1]) -> | EAppOp (op, [arg1]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" (Print.operator ~debug) op Format.fprintf fmt "@[<hov 2>%a@ %a@]" (Print.operator ~debug) op
format_with_parens arg1 format_with_parens arg1
| EApp (f, []) -> Format.fprintf fmt "@[<hov 2>%a@ ()@]" format_expr f | EApp (f, []) -> Format.fprintf fmt "@[<hov 2>%a@ ()@]" format_expr f
@ -84,7 +84,12 @@ let rec format_expr
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ") ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")
format_with_parens) format_with_parens)
args args
| EOp op -> Print.operator ~debug fmt op | EAppOp (op, args) ->
Format.fprintf fmt "@[<hov 2>%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 let rec format_statement
(decl_ctx : decl_ctx) (decl_ctx : decl_ctx)

35
compiler/scalc/to_python.ml
View File

@ -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)) (fun fmt e -> Format.fprintf fmt "%a" (format_expression ctx) e))
es es
| ELit l -> Format.fprintf fmt "%a" format_lit (Mark.copy e l) | 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.fprintf fmt "%a(%a,@ %a)" format_op (op, Pos.no_pos)
(format_expression ctx) arg1 (format_expression ctx) arg2 (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 Format.fprintf fmt "(%a %a@ %a)" (format_expression ctx) arg1 format_op
(op, Pos.no_pos) (format_expression ctx) arg2 (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 -> when Cli.globals.trace ->
Format.fprintf fmt "log_begin_call(%a,@ %a,@ %a)" format_uid_list info Format.fprintf fmt "log_begin_call(%a,@ %a,@ %a)" format_uid_list info
(format_expression ctx) f (format_expression ctx) arg (format_expression ctx) f (format_expression ctx) arg
| EApp ((EOp (Log (VarDef var_def_info, info)), _), [arg1]) | EAppOp (Log (VarDef var_def_info, info), [arg1]) when Cli.globals.trace ->
when Cli.globals.trace ->
Format.fprintf fmt Format.fprintf fmt
"log_variable_definition(%a,@ LogIO(input_io=InputIO.%s,@ \ "log_variable_definition(%a,@ LogIO(input_io=InputIO.%s,@ \
output_io=%s),@ %a)" output_io=%s),@ %a)"
@ -329,31 +328,30 @@ let rec format_expression (ctx : decl_ctx) (fmt : Format.formatter) (e : expr) :
| Runtime.Reentrant -> "Reentrant") | Runtime.Reentrant -> "Reentrant")
(if var_def_info.log_io_output then "True" else "False") (if var_def_info.log_io_output then "True" else "False")
(format_expression ctx) arg1 (format_expression ctx) arg1
| EApp ((EOp (Log (PosRecordIfTrueBool, _)), pos), [arg1]) | EAppOp (Log (PosRecordIfTrueBool, _), [arg1]) when Cli.globals.trace ->
when Cli.globals.trace -> let pos = Mark.get e in
Format.fprintf fmt Format.fprintf fmt
"log_decision_taken(SourcePosition(filename=\"%s\",@ start_line=%d,@ \ "log_decision_taken(SourcePosition(filename=\"%s\",@ start_line=%d,@ \
start_column=%d,@ end_line=%d, end_column=%d,@ law_headings=%a), %a)" 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_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_end_line pos) (Pos.get_end_column pos) format_string_list
(Pos.get_law_info pos) (format_expression ctx) arg1 (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.fprintf fmt "log_end_call(%a,@ %a)" format_uid_list info
(format_expression ctx) arg1 (format_expression ctx) arg1
| EApp ((EOp (Log _), _), [arg1]) -> | EAppOp (Log _, [arg1]) ->
Format.fprintf fmt "%a" (format_expression ctx) 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.fprintf fmt "%a %a" format_op (Not, Pos.no_pos)
(format_expression ctx) arg1 (format_expression ctx) arg1
| EApp | EAppOp (((Minus_int | Minus_rat | Minus_mon | Minus_dur) as op), [arg1]) ->
((EOp ((Minus_int | Minus_rat | Minus_mon | Minus_dur) as op), _), [arg1])
->
Format.fprintf fmt "%a %a" format_op (op, Pos.no_pos) Format.fprintf fmt "%a %a" format_op (op, Pos.no_pos)
(format_expression ctx) arg1 (format_expression ctx) arg1
| EApp ((EOp op, _), [arg1]) -> | EAppOp (op, [arg1]) ->
Format.fprintf fmt "%a(%a)" format_op (op, Pos.no_pos) Format.fprintf fmt "%a(%a)" format_op (op, Pos.no_pos)
(format_expression ctx) arg1 (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 Format.fprintf fmt
"%a(@[<hov 0>SourcePosition(filename=\"%s\",@ start_line=%d,@ \ "%a(@[<hov 0>SourcePosition(filename=\"%s\",@ start_line=%d,@ \
start_column=%d,@ end_line=%d, end_column=%d,@ law_headings=%a), %a)@]" 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 ",@ ") ~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ")
(format_expression ctx)) (format_expression ctx))
args args
| EOp op -> Format.fprintf fmt "%a" format_op (op, Pos.no_pos) | EAppOp (op, args) ->
Format.fprintf fmt "%a(@[<hov 0>%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 let rec format_statement
(ctx : decl_ctx) (ctx : decl_ctx)

24
compiler/scalc/to_r.ml
View File

@ -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)) (fun fmt e -> Format.fprintf fmt "%a" (format_expression ctx) e))
es es
| ELit l -> Format.fprintf fmt "%a" format_lit (Mark.copy e l) | 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.fprintf fmt "%a(%a,@ %a)" format_op (op, Pos.no_pos)
(format_expression ctx) arg1 (format_expression ctx) arg2 (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 Format.fprintf fmt "(%a %a@ %a)" (format_expression ctx) arg1 format_op
(op, Pos.no_pos) (format_expression ctx) arg2 (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.fprintf fmt "%a %a" format_op (Not, Pos.no_pos)
(format_expression ctx) arg1 (format_expression ctx) arg1
| EApp | EAppOp (((Minus_int | Minus_rat | Minus_mon | Minus_dur) as op), [arg1]) ->
((EOp ((Minus_int | Minus_rat | Minus_mon | Minus_dur) as op), _), [arg1])
->
Format.fprintf fmt "%a %a" format_op (op, Pos.no_pos) Format.fprintf fmt "%a %a" format_op (op, Pos.no_pos)
(format_expression ctx) arg1 (format_expression ctx) arg1
| EApp ((EOp op, _), [arg1]) -> | EAppOp (op, [arg1]) ->
Format.fprintf fmt "%a(%a)" format_op (op, Pos.no_pos) Format.fprintf fmt "%a(%a)" format_op (op, Pos.no_pos)
(format_expression ctx) arg1 (format_expression ctx) arg1
| EApp ((EOp HandleDefaultOpt, _), _) -> | EAppOp (HandleDefaultOpt, _) ->
Message.raise_internal_error Message.raise_internal_error
"R compilation does not currently support the avoiding of exceptions" "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 Format.fprintf fmt
"%a(@[<hov 0>catala_position(filename=\"%s\",@ start_line=%d,@ \ "%a(@[<hov 0>catala_position(filename=\"%s\",@ start_line=%d,@ \
start_column=%d,@ end_line=%d, end_column=%d,@ law_headings=%a), %a)@]" 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 ",@ ") ~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ")
(format_expression ctx)) (format_expression ctx))
args args
| EOp op -> Format.fprintf fmt "%a" format_op (op, Pos.no_pos) | EAppOp (op, args) ->
Format.fprintf fmt "%a(@[<hov 0>%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 let rec format_statement
(ctx : decl_ctx) (ctx : decl_ctx)

53
compiler/scopelang/from_desugared.ml
View File

@ -38,9 +38,10 @@ let tag_with_log_entry
(l : log_entry) (l : log_entry)
(markings : Uid.MarkedString.info list) : untyped Ast.expr boxed = (markings : Uid.MarkedString.info list) : untyped Ast.expr boxed =
if Cli.globals.trace then if Cli.globals.trace then
Expr.eapp Expr.eappop
(Expr.eop (Log (l, markings)) [TAny, Expr.pos e] (Mark.get e)) ~op:(Log (l, markings))
[e] (Mark.get e) ~tys:[TAny, Expr.pos e]
~args:[e] (Mark.get e)
else e else e
let rec translate_expr (ctx : ctx) (e : D.expr) : untyped Ast.expr boxed = 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) (Expr.edefault ~excepts:[] ~just:(Expr.elit (LBool true) m)
~cons: ~cons:
(Expr.epuredefault (Expr.epuredefault
(Expr.make_app e' [Expr.evar arg m] pos) (Expr.make_app e' [Expr.evar arg m] targs pos)
m) m)
m) m)
targs pos 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') ScopeVar.Map.add v' e' args')
args ScopeVar.Map.empty) args ScopeVar.Map.empty)
m 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 let args = List.map (translate_expr ctx) args in
Operator.kind_dispatch op Operator.kind_dispatch op
~monomorphic:(fun op -> Expr.eapp (Expr.eop op tys m1) args m) ~monomorphic:(fun op -> Expr.eappop ~op ~tys ~args m)
~polymorphic:(fun op -> Expr.eapp (Expr.eop op tys m1) args m) ~polymorphic:(fun op -> Expr.eappop ~op ~tys ~args m)
~overloaded:(fun op -> ~overloaded:(fun op ->
match match
Operator.resolve_overload ctx.decl_ctx (Mark.add (Expr.pos e) op) tys Operator.resolve_overload ctx.decl_ctx (Mark.add (Expr.pos e) op) tys
with with
| op, `Straight -> Expr.eapp (Expr.eop op tys m1) args m | op, `Straight -> Expr.eappop ~op ~tys ~args m
| op, `Reversed -> | op, `Reversed ->
Expr.eapp (Expr.eop op (List.rev tys) m1) (List.rev args) m) Expr.eappop ~op ~tys:(List.rev tys) ~args:(List.rev args) m)
| EOp _ -> assert false (* Only allowed within [EApp] *)
| ( EStruct _ | EStructAccess _ | ETuple _ | ETupleAccess _ | EInj _ | ( EStruct _ | EStructAccess _ | ETuple _ | ETupleAccess _ | EInj _
| EMatch _ | ELit _ | EApp _ | EDefault _ | EPureDefault _ | EIfThenElse _ | EMatch _ | ELit _ | EDefault _ | EPureDefault _ | EIfThenElse _ | EArray _
| EArray _ | EEmptyError | EErrorOnEmpty _ ) as e -> | EEmptyError | EErrorOnEmpty _ ) as e ->
Expr.map ~f:(translate_expr ctx) (e, m) Expr.map ~f:(translate_expr ctx) (e, m)
(** {1 Rule tree construction} *) (** {1 Rule tree construction} *)

7
compiler/shared_ast/definitions.ml
View File

@ -478,10 +478,14 @@ and ('a, 'b, 'm) base_gexpr =
| EApp : { | EApp : {
f : ('a, 'm) gexpr; f : ('a, 'm) gexpr;
args : ('a, 'm) gexpr list; 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 -> ('a, < .. >, 'm) base_gexpr
| EOp : { | EAppOp : {
op : 'b operator; op : 'b operator;
args : ('a, 'm) gexpr list;
tys : typ list; tys : typ list;
} }
-> ('a, (< .. > as 'b), 'm) base_gexpr -> ('a, (< .. > as 'b), 'm) base_gexpr
@ -559,6 +563,7 @@ and ('a, 'b, 'm) base_gexpr =
| EPureDefault : | EPureDefault :
('a, 'm) gexpr ('a, 'm) gexpr
-> ('a, < defaultTerms : yes ; .. >, 'm) base_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 | EEmptyError : ('a, < defaultTerms : yes ; .. >, 'm) base_gexpr
| EErrorOnEmpty : | EErrorOnEmpty :
('a, 'm) gexpr ('a, 'm) gexpr

120
compiler/shared_ast/expr.ml
View File

@ -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 eexternal ~name mark = Mark.add mark (Bindlib.box (EExternal { name }))
let etuple args = Box.appn args @@ fun args -> ETuple args let etuple args = Box.appn args @@ fun args -> ETuple args
let etupleaccess e index size = let etupleaccess ~e ~index ~size =
assert (index < size); assert (index < size);
Box.app1 e @@ fun e -> ETupleAccess { e; 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 = let eabs binder tys mark =
Bindlib.box_apply (fun binder -> EAbs { binder; tys }) binder, 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 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 = let edefault ~excepts ~just ~cons =
Box.app2n just cons excepts Box.app2n just cons excepts
@ -273,8 +275,8 @@ let map
let m = Mark.get e in let m = Mark.get e in
match Mark.remove e with match Mark.remove e with
| ELit l -> elit l m | ELit l -> elit l m
| EApp { f = e1; args } -> eapp (f e1) (List.map f args) m | EApp { f = e1; args; tys } -> eapp ~f:(f e1) ~args:(List.map f args) ~tys m
| EOp { op; tys } -> eop op tys m | EAppOp { op; tys; args } -> eappop ~op ~tys ~args:(List.map f args) m
| EArray args -> earray (List.map f args) m | EArray args -> earray (List.map f args) m
| EVar v -> evar (Var.translate v) m | EVar v -> evar (Var.translate v) m
| EExternal { name } -> eexternal ~name m | EExternal { name } -> eexternal ~name m
@ -286,7 +288,7 @@ let map
| EIfThenElse { cond; etrue; efalse } -> | EIfThenElse { cond; etrue; efalse } ->
eifthenelse (f cond) (f etrue) (f efalse) m eifthenelse (f cond) (f etrue) (f efalse) m
| ETuple args -> etuple (List.map f args) 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 | EInj { name; cons; e } -> einj ~name ~cons ~e:(f e) m
| EAssert e1 -> eassert (f e1) m | EAssert e1 -> eassert (f e1) m
| EDefault { excepts; just; cons } -> | EDefault { excepts; just; cons } ->
@ -322,10 +324,9 @@ let shallow_fold
(acc : 'acc) : 'acc = (acc : 'acc) : 'acc =
let lfold x acc = List.fold_left (fun acc x -> f x acc) acc x in let lfold x acc = List.fold_left (fun acc x -> f x acc) acc x in
match Mark.remove e with match Mark.remove e with
| ELit _ | EOp _ | EVar _ | EExternal _ | ERaise _ | ELocation _ | EEmptyError | ELit _ | EVar _ | EExternal _ | ERaise _ | ELocation _ | EEmptyError -> acc
-> | EApp { f = e; args; _ } -> acc |> f e |> lfold args
acc | EAppOp { args; _ } -> acc |> lfold args
| EApp { f = e; args } -> acc |> f e |> lfold args
| EArray args -> acc |> lfold args | EArray args -> acc |> lfold args
| EAbs { binder; tys = _ } -> | EAbs { binder; tys = _ } ->
let _, body = Bindlib.unmbind binder in let _, body = Bindlib.unmbind binder in
@ -367,11 +368,13 @@ let map_gather
in in
match Mark.remove e with match Mark.remove e with
| ELit l -> acc, elit l m | ELit l -> acc, elit l m
| EApp { f = e1; args } -> | EApp { f = e1; args; tys } ->
let acc1, f = f e1 in let acc1, f = f e1 in
let acc2, args = lfoldmap args in let acc2, args = lfoldmap args in
join acc1 acc2, eapp f args m join acc1 acc2, eapp ~f ~args ~tys m
| EOp { op; tys } -> acc, eop op tys m | EAppOp { op; args; tys } ->
let acc, args = lfoldmap args in
acc, eappop ~op ~args ~tys m
| EArray args -> | EArray args ->
let acc, args = lfoldmap args in let acc, args = lfoldmap args in
acc, earray args m acc, earray args m
@ -392,7 +395,7 @@ let map_gather
acc, etuple args m acc, etuple args m
| ETupleAccess { e; index; size } -> | ETupleAccess { e; index; size } ->
let acc, e = f e in let acc, e = f e in
acc, etupleaccess e index size m acc, etupleaccess ~e ~index ~size m
| EInj { name; cons; e } -> | EInj { name; cons; e } ->
let acc, e = f e in let acc, e = f e in
acc, einj ~name ~cons ~e m 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) = let is_value (type a) (e : (a, _) gexpr) =
match Mark.remove e with match Mark.remove e with
| ELit _ | EAbs _ | EOp _ | ERaise _ -> true | ELit _ | EAbs _ | ERaise _ | ECustom _ | EExternal _ -> true
| _ -> false | _ -> false
let equal_lit (l1 : lit) (l2 : lit) = 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 | ELit l1, ELit l2 -> l1 = l2
| EAbs { binder = b1; tys = tys1 }, EAbs { binder = b2; tys = tys2 } -> | EAbs { binder = b1; tys = tys1 }, EAbs { binder = b2; tys = tys2 } ->
Type.equal_list tys1 tys2 && Bindlib.eq_mbinder equal b1 b2 Type.equal_list tys1 tys2 && Bindlib.eq_mbinder equal b1 b2
| EApp { f = e1; args = args1 }, EApp { f = e2; args = args2 } -> | ( EApp { f = e1; args = args1; tys = tys1 },
equal e1 e2 && equal_list args1 args2 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 | 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 = exc1; just = def1; cons = cons1 },
EDefault { excepts = exc2; just = def2; cons = cons2 } ) -> EDefault { excepts = exc2; just = def2; cons = cons2 } ) ->
equal def1 def2 && equal cons1 cons2 && equal_list exc1 exc2 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 } ) -> ECustom { obj = obj2; targs = targs2; tret = tret2 } ) ->
Type.equal_list targs1 targs2 && Type.equal tret1 tret2 && obj1 == obj2 Type.equal_list targs1 targs2 && Type.equal tret1 tret2 && obj1 == obj2
| ( ( EVar _ | EExternal _ | ETuple _ | ETupleAccess _ | EArray _ | ELit _ | ( ( EVar _ | EExternal _ | ETuple _ | ETupleAccess _ | EArray _ | ELit _
| EAbs _ | EApp _ | EAssert _ | EOp _ | EDefault _ | EPureDefault _ | EAbs _ | EApp _ | EAppOp _ | EAssert _ | EDefault _ | EPureDefault _
| EIfThenElse _ | EEmptyError | EErrorOnEmpty _ | ERaise _ | ECatch _ | EIfThenElse _ | EEmptyError | EErrorOnEmpty _ | ERaise _ | ECatch _
| ELocation _ | EStruct _ | EDStructAccess _ | EStructAccess _ | EInj _ | ELocation _ | EStruct _ | EDStructAccess _ | EStructAccess _ | EInj _
| EMatch _ | EScopeCall _ | ECustom _ ), | 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 match[@ocamlformat "disable"] Mark.remove e1, Mark.remove e2 with
| ELit l1, ELit l2 -> | ELit l1, ELit l2 ->
compare_lit l1 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 () -> compare f1 f2 @@< fun () ->
List.compare compare args1 args2 List.compare compare args1 args2 @@< fun () ->
| EOp {op=op1; tys=tys1}, EOp {op=op2; tys=tys2} -> 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 () -> Operator.compare op1 op2 @@< fun () ->
List.compare compare args1 args2 @@< fun () ->
List.compare Type.compare tys1 tys2 List.compare Type.compare tys1 tys2
| EArray a1, EArray a2 -> | EArray a1, EArray a2 ->
List.compare compare a1 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" invalid_arg "Custom block comparison"
| ELit _, _ -> -1 | _, ELit _ -> 1 | ELit _, _ -> -1 | _, ELit _ -> 1
| EApp _, _ -> -1 | _, EApp _ -> 1 | EApp _, _ -> -1 | _, EApp _ -> 1
| EOp _, _ -> -1 | _, EOp _ -> 1 | EAppOp _, _ -> -1 | _, EAppOp _ -> 1
| EArray _, _ -> -1 | _, EArray _ -> 1 | EArray _, _ -> -1 | _, EArray _ -> 1
| EVar _, _ -> -1 | _, EVar _ -> 1 | EVar _, _ -> -1 | _, EVar _ -> 1
| EExternal _, _ -> -1 | _, EExternal _ -> 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) 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 | 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 (* This function is first defined in [Print], only for dependency reasons *)
| EApp { f = EOp { op = Log _; _ }, _; args = [e] }, _ -> skip_wrappers e let skip_wrappers : type a. (a, 'm) gexpr -> (a, 'm) gexpr = Print.skip_wrappers
| 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
let remove_logging_calls e = let remove_logging_calls e =
let rec f e = let rec f e =
let e, m = map ~f e in let e, m = map ~f e in
( Bindlib.box_apply ( Bindlib.box_apply
(function (function EAppOp { op = Log _; args = [(arg, _)]; _ } -> arg | e -> e)
| EApp { f = EOp { op = Log _; _ }, _; args = [(arg, _)] } -> arg
| e -> e)
e, e,
m ) m )
in in
@ -876,7 +875,7 @@ let format ppf e = Print.expr ~debug:false () ppf e
let rec size : type a. (a, 't) gexpr -> int = let rec size : type a. (a, 't) gexpr -> int =
fun e -> fun e ->
match Mark.remove e with 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 | 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 | EArray args -> List.fold_left (fun acc arg -> acc + size arg) 1 args
| ETupleAccess { e; _ } -> size e + 1 | ETupleAccess { e; _ } -> size e + 1
@ -884,8 +883,9 @@ let rec size : type a. (a, 't) gexpr -> int =
| EAssert e -> size e + 1 | EAssert e -> size e + 1
| EErrorOnEmpty e -> size e + 1 | EErrorOnEmpty e -> size e + 1
| EPureDefault 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 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; _ } -> | EAbs { binder; _ } ->
let _, body = Bindlib.unmbind binder in let _, body = Bindlib.unmbind binder in
1 + size body 1 + size body
@ -921,7 +921,19 @@ let make_abs xs e taus pos =
in in
eabs (bind xs e) taus mark 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 = let mark =
fold_marks fold_marks
(fun _ -> pos) (fun _ -> pos)
@ -937,9 +949,9 @@ let make_app e args pos =
Message.raise_internal_error Message.raise_internal_error
"wrong type: found %a while expecting either an Arrow or Any" "wrong type: found %a while expecting either an Arrow or Any"
Print.typ_debug fty.ty)) Print.typ_debug fty.ty))
(List.map Mark.get (e :: args)) (List.map Mark.get (f :: args))
in in
eapp e args mark eapp ~f ~args ~tys mark
let make_erroronempty e = let make_erroronempty e =
let mark = let mark =
@ -964,28 +976,22 @@ let thunk_term term mark =
let empty_thunked_term mark = thunk_term (Bindlib.box EEmptyError, mark) mark let empty_thunked_term mark = thunk_term (Bindlib.box EEmptyError, mark) mark
let unthunk_term_nobox term 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 = 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 = 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 make_puredefault e =
let mark = let mark =
map_mark (fun pos -> pos) (fun ty -> TDefault ty, Mark.get ty) (Mark.get e) map_mark (fun pos -> pos) (fun ty -> TDefault ty, Mark.get ty) (Mark.get e)
in in
epuredefault e mark 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

19
compiler/shared_ast/expr.mli
View File

@ -55,7 +55,11 @@ val subst :
val etuple : ('a, 'm) boxed_gexpr list -> 'm mark -> ('a any, 'm) boxed_gexpr val etuple : ('a, 'm) boxed_gexpr list -> 'm mark -> ('a any, 'm) boxed_gexpr
val etupleaccess : 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 earray : ('a, 'm) boxed_gexpr list -> 'm mark -> ('a any, 'm) boxed_gexpr
val elit : lit -> '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 ('a any, 'm) boxed_gexpr
val eapp : val eapp :
('a, 'm) boxed_gexpr -> f:('a, 'm) boxed_gexpr ->
('a, 'm) boxed_gexpr list -> args:('a, 'm) boxed_gexpr list ->
tys:typ list ->
'm mark -> 'm mark ->
('a any, 'm) boxed_gexpr ('a any, 'm) boxed_gexpr
@ -77,7 +82,12 @@ val eassert :
'm mark -> 'm mark ->
((< assertions : yes ; .. > as 'a), 'm) boxed_gexpr ((< 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 : val edefault :
excepts:('a, 'm) boxed_gexpr list -> excepts:('a, 'm) boxed_gexpr list ->
@ -319,6 +329,7 @@ val make_abs :
val make_app : val make_app :
('a any, 'm) boxed_gexpr -> ('a any, 'm) boxed_gexpr ->
('a, 'm) boxed_gexpr list -> ('a, 'm) boxed_gexpr list ->
typ list ->
Pos.t -> Pos.t ->
('a any, 'm) boxed_gexpr ('a any, 'm) boxed_gexpr

94
compiler/shared_ast/interpreter.ml
View File

@ -169,7 +169,7 @@ let rec evaluate_operator
(should not happen if the term was well-typed)%a" (should not happen if the term was well-typed)%a"
(Print.operator ~debug:true) (Print.operator ~debug:true)
op Expr.format op Expr.format
(EApp { f = EOp { op; tys = [] }, m; args }, m) (EAppOp { op; tys = []; args }, m)
in in
propagate_empty_error_list args propagate_empty_error_list args
@@ fun args -> @@ fun args ->
@ -193,21 +193,38 @@ let rec evaluate_operator
| Map, [f; (EArray es, _)] -> | Map, [f; (EArray es, _)] ->
EArray EArray
(List.map (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) es)
| Reduce, [_; default; (EArray [], _)] -> Mark.remove default | Reduce, [_; default; (EArray [], _)] -> Mark.remove default
| Reduce, [f; _; (EArray (x0 :: xn), _)] -> | Reduce, [f; _; (EArray (x0 :: xn), _)] ->
Mark.remove Mark.remove
(List.fold_left (List.fold_left
(fun acc x -> (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) x0 xn)
| Concat, [(EArray es1, _); (EArray es2, _)] -> EArray (es1 @ es2) | Concat, [(EArray es1, _); (EArray es2, _)] -> EArray (es1 @ es2)
| Filter, [f; (EArray es, _)] -> | Filter, [f; (EArray es, _)] ->
EArray EArray
(List.filter (List.filter
(fun e' -> (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 | ELit (LBool b), _ -> b
| _ -> | _ ->
Message.raise_spanned_error Message.raise_spanned_error
@ -219,7 +236,18 @@ let rec evaluate_operator
Mark.remove Mark.remove
(List.fold_left (List.fold_left
(fun acc e' -> (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) init es)
| (Length | Log _ | Eq | Map | Concat | Filter | Fold | Reduce), _ -> err () | (Length | Log _ | Eq | Map | Concat | Filter | Fold | Reduce), _ -> err ()
| Not, [(ELit (LBool b), _)] -> ELit (LBool (o_not b)) | Not, [(ELit (LBool b), _)] -> ELit (LBool (o_not b))
@ -536,8 +564,9 @@ and val_to_runtime :
let rec curry acc = function let rec curry acc = function
| [] -> | [] ->
let args = List.rev acc in 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 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) with CatalaException EmptyError -> raise Runtime.EmptyError)
| targ :: targs -> | targ :: targs ->
Obj.repr (fun x -> Obj.repr (fun x ->
@ -594,7 +623,7 @@ let rec evaluate_expr :
in in
let o = Runtime.lookup_value runtime_path in let o = Runtime.lookup_value runtime_path in
runtime_to_val (fun ctx -> evaluate_expr ctx lang) ctx m ty o 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 e1 = evaluate_expr ctx lang e1 in
let args = List.map (evaluate_expr ctx lang) args in let args = List.map (evaluate_expr ctx lang) args in
propagate_empty_error e1 propagate_empty_error e1
@ -609,7 +638,6 @@ let rec evaluate_expr :
"wrong function call, expected %d arguments, got %d" "wrong function call, expected %d arguments, got %d"
(Bindlib.mbinder_arity binder) (Bindlib.mbinder_arity binder)
(List.length args) (List.length args)
| EOp { op; _ } -> evaluate_operator (evaluate_expr ctx lang) op m lang args
| ECustom { obj; targs; tret } -> | ECustom { obj; targs; tret } ->
(* Applies the arguments one by one to the curried form *) (* Applies the arguments one by one to the curried form *)
List.fold_left2 List.fold_left2
@ -624,9 +652,11 @@ let rec evaluate_expr :
Message.raise_spanned_error pos Message.raise_spanned_error pos
"function has not been reduced to a lambda at evaluation (should not \ "function has not been reduced to a lambda at evaluation (should not \
happen if the term was well-typed") 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) | EAbs { binder; tys } -> Expr.unbox (Expr.eabs (Bindlib.box binder) tys m)
| ELit _ as e -> Mark.add m e | 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 *) *) (* | EAbs _ as e -> Marked.mark m e (* these are values *) *)
| EStruct { fields = es; name } -> | EStruct { fields = es; name } ->
let fields, es = List.split (StructField.Map.bindings es) in 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 \ "sum type index error (should not happen if the term was \
well-typed)" well-typed)"
in 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 evaluate_expr ctx lang new_e
| _ -> | _ ->
Message.raise_spanned_error (Expr.pos 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 the AST while evaluating everything below. This makes for a good error
message. *) message. *)
match Mark.remove e with match Mark.remove e with
| EApp { f = EOp ({ op = op_kind; _ } as op), m; args = [e1; e2] } | EAppOp
when match op_kind with {
| And | Or | Xor | Eq | Lt_int_int | Lt_rat_rat | Lt_mon_mon args = [e1; e2];
| Lt_dat_dat | Lt_dur_dur | Lte_int_int | Lte_rat_rat | Lte_mon_mon tys;
| Lte_dat_dat | Lte_dur_dur | Gt_int_int | Gt_rat_rat | Gt_mon_mon op =
| Gt_dat_dat | Gt_dur_dur | Gte_int_int | Gte_rat_rat | Gte_mon_mon ( And | Or | Xor | Eq | Lt_int_int | Lt_rat_rat | Lt_mon_mon
| Gte_dat_dat | Gte_dur_dur | Eq_int_int | Eq_rat_rat | Eq_mon_mon | Lt_dat_dat | Lt_dur_dur | Lte_int_int | Lte_rat_rat | Lte_mon_mon
| Eq_dur_dur | Eq_dat_dat -> | Lte_dat_dat | Lte_dur_dur | Gt_int_int | Gt_rat_rat | Gt_mon_mon
true | Gt_dat_dat | Gt_dur_dur | Gte_int_int | Gte_rat_rat | Gte_mon_mon
| _ -> false -> | Gte_dat_dat | Gte_dur_dur | Eq_int_int | Eq_rat_rat | Eq_mon_mon
( EApp | Eq_dur_dur | Eq_dat_dat ) as op;
} ->
( EAppOp
{ {
f = EOp op, m; op;
tys;
args = args =
[ [
partially_evaluate_expr_for_assertion_failure_message ctx lang e1; 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, c) interpr_kind, 't) gexpr ->
((d, e, yes) interpr_kind, 't) gexpr boxed = function ((d, e, yes) interpr_kind, 't) gexpr boxed = function
| (ECustom _, _) as e -> Expr.map ~f e | (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 | (EDefault _, _) as e -> Expr.map ~f e
| (EPureDefault _, _) as e -> Expr.map ~f e | (EPureDefault _, _) as e -> Expr.map ~f e
| (EEmptyError, _) 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, c) interpr_kind, 't) gexpr ->
((d, e, no) interpr_kind, 't) gexpr boxed = function ((d, e, no) interpr_kind, 't) gexpr boxed = function
| ECustom _, _ -> invalid_arg "Custom term remaining in evaluated term" | 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 | (EDefault _, _) as e -> Expr.map ~f e
| (EPureDefault _, _) as e -> Expr.map ~f e | (EPureDefault _, _) as e -> Expr.map ~f e
| (EEmptyError, _) 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 (Expr.einj ~e:(Expr.elit LUnit mark_e) ~cons:Expr.none_constr
~name:Expr.option_enum mark_e) ~name:Expr.option_enum mark_e)
ty_in (Expr.mark_pos mark_e); ty_in (Expr.mark_pos mark_e);
Expr.eapp Expr.eappop ~op:Operator.ToClosureEnv
(Expr.eop Operator.ToClosureEnv [TClosureEnv, pos] mark_e) ~args:[Expr.etuple [] mark_e]
[Expr.etuple [] mark_e] ~tys:[TClosureEnv, pos]
mark_e; mark_e;
] ]
mark_e mark_e
@ -918,6 +956,7 @@ let interpret_program_lcalc p s : (Uid.MarkedString.info * ('a, 'm) gexpr) list
let to_interpret = let to_interpret =
Expr.make_app (Expr.box e) Expr.make_app (Expr.box e)
[Expr.estruct ~name:s_in ~fields:application_term mark_e] [Expr.estruct ~name:s_in ~fields:application_term mark_e]
[TStruct s_in, Expr.pos e]
(Expr.pos e) (Expr.pos e)
in in
match Mark.remove (evaluate_expr ctx p.lang (Expr.unbox to_interpret)) with 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 = let to_interpret =
Expr.make_app (Expr.box e) Expr.make_app (Expr.box e)
[Expr.estruct ~name:s_in ~fields:application_term mark_e] [Expr.estruct ~name:s_in ~fields:application_term mark_e]
[TStruct s_in, Expr.pos e]
(Expr.pos e) (Expr.pos e)
in in
match Mark.remove (evaluate_expr ctx p.lang (Expr.unbox to_interpret)) with match Mark.remove (evaluate_expr ctx p.lang (Expr.unbox to_interpret)) with

114
compiler/shared_ast/optimizations.ml
View File

@ -100,61 +100,17 @@ let rec optimize_expr :
the matches and the log calls are not preserved, which would be a good the matches and the log calls are not preserved, which would be a good
property *) property *)
match Mark.remove e with match Mark.remove e with
| EApp | EAppOp { op = Not; args = [(ELit (LBool b), _)]; _ } ->
{
f =
( EOp { op = Not; _ }, _
| ( EApp
{
f = EOp { op = Log _; _ }, _;
args = [(EOp { op = Not; _ }, _)];
},
_ ) ) as op;
args = [e1];
} -> (
(* reduction of logical not *) (* reduction of logical not *)
match e1 with ELit (LBool (not b))
| ELit (LBool false), _ -> ELit (LBool true) | EAppOp { op = Or; args = [(ELit (LBool b), _); (e, _)]; _ }
| ELit (LBool true), _ -> ELit (LBool false) | EAppOp { op = Or; args = [(e, _); (ELit (LBool b), _)]; _ } ->
| 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];
} -> (
(* reduction of logical or *) (* reduction of logical or *)
match e1, e2 with if b then ELit (LBool true) else e
| (ELit (LBool false), _), new_e | new_e, (ELit (LBool false), _) -> | EAppOp { op = And; args = [(ELit (LBool b), _); (e, _)]; _ }
Mark.remove new_e | EAppOp { op = And; args = [(e, _); (ELit (LBool b), _)]; _ } ->
| (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];
} -> (
(* reduction of logical and *) (* reduction of logical and *)
match e1, e2 with if b then e else ELit (LBool false)
| (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] })
| EMatch { e = EInj { e = e'; cons; name = n' }, _; cases; name = n } | EMatch { e = EInj { e = e'; cons; name = n' }, _; cases; name = n }
(* iota-reduction *) (* iota-reduction *)
when EnumName.equal n n' -> ( when EnumName.equal n n' -> (
@ -206,7 +162,7 @@ let rec optimize_expr :
cases1 cases2 cases1 cases2
in in
EMatch { e = arg; cases; name = n1 } EMatch { e = arg; cases; name = n1 }
| EApp { f = EAbs { binder; _ }, _; args } | EApp { f = EAbs { binder; _ }, _; args; _ }
when binder_vars_used_at_most_once binder when binder_vars_used_at_most_once binder
|| List.for_all (function EVar _, _ -> true | _ -> false) args -> || List.for_all (function EVar _, _ -> true | _ -> false) args ->
(* beta reduction when variables not used, and for variable aliases *) (* beta reduction when variables not used, and for variable aliases *)
@ -270,11 +226,7 @@ let rec optimize_expr :
dft dft
| ( [], | ( [],
( ( ELit (LBool false) ( ( ELit (LBool false)
| EApp | EAppOp { op = Log _; args = [(ELit (LBool false), _)]; _ } ),
{
f = EOp { op = Log _; _ }, _;
args = [(ELit (LBool false), _)];
} ),
_ ) ) -> _ ) ) ->
(* No exceptions and condition false *) (* No exceptions and condition false *)
EEmptyError EEmptyError
@ -283,12 +235,7 @@ let rec optimize_expr :
{ {
cond = cond =
( ELit (LBool true), _ ( ELit (LBool true), _
| ( EApp | EAppOp { op = Log _; args = [(ELit (LBool true), _)]; _ }, _ );
{
f = EOp { op = Log _; _ }, _;
args = [(ELit (LBool true), _)];
},
_ ) );
etrue; etrue;
_; _;
} -> } ->
@ -297,11 +244,7 @@ let rec optimize_expr :
{ {
cond = cond =
( ( ELit (LBool false) ( ( ELit (LBool false)
| EApp | EAppOp { op = Log _; args = [(ELit (LBool false), _)]; _ } ),
{
f = EOp { op = Log _; _ }, _;
args = [(ELit (LBool false), _)];
} ),
_ ); _ );
efalse; efalse;
_; _;
@ -312,40 +255,31 @@ let rec optimize_expr :
cond; cond;
etrue = etrue =
( ( ELit (LBool btrue) ( ( ELit (LBool btrue)
| EApp | EAppOp { op = Log _; args = [(ELit (LBool btrue), _)]; _ } ),
{
f = EOp { op = Log _; _ }, _;
args = [(ELit (LBool btrue), _)];
} ),
_ ); _ );
efalse = efalse =
( ( ELit (LBool bfalse) ( ( ELit (LBool bfalse)
| EApp | EAppOp { op = Log _; args = [(ELit (LBool bfalse), _)]; _ } ),
{
f = EOp { op = Log _; _ }, _;
args = [(ELit (LBool bfalse), _)];
} ),
_ ); _ );
} -> } ->
if btrue && not bfalse then Mark.remove cond if btrue && not bfalse then Mark.remove cond
else if (not btrue) && bfalse then else if (not btrue) && bfalse then
EApp EAppOp
{ { op = Not; tys = [TLit TBool, Expr.mark_pos mark]; args = [cond] }
f = EOp { op = Not; tys = [TLit TBool, Expr.mark_pos mark] }, mark;
args = [cond];
}
(* note: this last call eliminates the condition & might skip log calls (* note: this last call eliminates the condition & might skip log calls
as well *) as well *)
else (* btrue = bfalse *) ELit (LBool btrue) 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 *) (*reduces a fold with an empty list *)
Mark.remove init Mark.remove init
| EApp | EAppOp
{ f = EOp { op = Op.Fold; _ }, _; args = [f; init; (EArray [e'], _)] } {
-> op = Op.Fold;
args = [f; init; (EArray [e'], _)];
tys = [_; tinit; (TArray tx, _)];
} ->
(* reduces a fold with one element *) (* reduces a fold with one element *)
EApp { f; args = [init; e'] } EApp { f; args = [init; e']; tys = [tinit; tx] }
| ECatch { body; exn; handler } -> ( | ECatch { body; exn; handler } -> (
(* peephole exception catching reductions *) (* peephole exception catching reductions *)
match Mark.remove body, Mark.remove handler with match Mark.remove body, Mark.remove handler with

55
compiler/shared_ast/print.ml
View File

@ -374,7 +374,7 @@ module Precedence = struct
fun e -> fun e ->
match Mark.remove e with match Mark.remove e with
| ELit _ -> Contained (* Todo: unop if < 0 *) | ELit _ -> Contained (* Todo: unop if < 0 *)
| EApp { f = EOp { op; _ }, _; _ } -> ( | EAppOp { op; _ } -> (
match op with match op with
| Not | GetDay | GetMonth | GetYear | FirstDayOfMonth | LastDayOfMonth | Not | GetDay | GetMonth | GetYear | FirstDayOfMonth | LastDayOfMonth
| Length | Log _ | Minus | Minus_int | Minus_rat | Minus_mon | Minus_dur | Length | Log _ | Minus | Minus_int | Minus_rat | Minus_mon | Minus_dur
@ -411,7 +411,6 @@ module Precedence = struct
| ToClosureEnv | FromClosureEnv -> | ToClosureEnv | FromClosureEnv ->
App) App)
| EApp _ -> App | EApp _ -> App
| EOp _ -> Contained
| EArray _ -> Contained | EArray _ -> Contained
| EVar _ -> Contained | EVar _ -> Contained
| EExternal _ -> Contained | EExternal _ -> Contained
@ -527,7 +526,7 @@ module ExprGen (C : EXPR_PARAM) = struct
| ELit l -> C.lit fmt l | ELit l -> C.lit fmt l
| EApp { f = EAbs _, _; _ } -> | EApp { f = EAbs _, _; _ } ->
let rec pr bnd_ctx colors fmt = function 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, 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 = List.mapi (fun i tau -> xs.(i), tau) tys in
let xs_tau_arg = let xs_tau_arg =
@ -563,19 +562,16 @@ module ExprGen (C : EXPR_PARAM) = struct
Format.pp_close_box fmt (); Format.pp_close_box fmt ();
punctuation fmt ")")) punctuation fmt ")"))
xs_tau punctuation "→" (rhs expr) body xs_tau punctuation "→" (rhs expr) body
| EApp | EAppOp { op = (Map | Filter) as op; args = [arg1; arg2]; _ } ->
{ f = EOp { op = (Map | Filter) as op; _ }, _; args = [arg1; arg2] }
->
Format.fprintf fmt "@[<hv 2>%a %a@ %a@]" operator op (lhs exprc) arg1 Format.fprintf fmt "@[<hv 2>%a %a@ %a@]" operator op (lhs exprc) arg1
(rhs exprc) arg2 (rhs exprc) arg2
| EApp { f = EOp { op = Log _ as op; _ }, _; args = [arg1] } -> | EAppOp { op = Log _ as op; args = [arg1]; _ } ->
Format.fprintf fmt "@[<hv 0>%a@ %a@]" operator op (rhs exprc) arg1 Format.fprintf fmt "@[<hv 0>%a@ %a@]" operator op (rhs exprc) arg1
| EApp { f = EOp { op = op0; _ }, _; args = [_; _] } -> | EAppOp { op = op0; args = [_; _]; _ } ->
let prec = Precedence.expr e in let prec = Precedence.expr e in
let rec pr colors fmt = function let rec pr colors fmt = function
(* Flatten sequences of the same associative op *) (* 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 (match prec with
| Op (And | Or | Mul | Add | Div | Sub) -> lhs pr fmt arg1 | Op (And | Or | Mul | Add | Div | Sub) -> lhs pr fmt arg1
| _ -> lhs exprc fmt arg1); | _ -> lhs exprc fmt arg1);
@ -590,9 +586,15 @@ module ExprGen (C : EXPR_PARAM) = struct
Format.pp_open_hvbox fmt 0; Format.pp_open_hvbox fmt 0;
pr colors fmt e; pr colors fmt e;
Format.pp_close_box fmt () Format.pp_close_box fmt ()
| EApp { f = EOp { op; _ }, _; args = [arg1] } -> | EAppOp { op; args = [arg1]; _ } ->
Format.fprintf fmt "@[<hv 2>%a@ %a@]" operator op (rhs exprc) arg1 Format.fprintf fmt "@[<hv 2>%a@ %a@]" operator op (rhs exprc) arg1
| EApp { f; args } -> | EAppOp { op; args; _ } ->
Format.fprintf fmt "@[<hv 2>%a@ %a@]" operator op
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")
(rhs exprc))
args
| EApp { f; args; _ } ->
Format.fprintf fmt "@[<hv 2>%a@ %a@]" (lhs exprc) f Format.fprintf fmt "@[<hv 2>%a@ %a@]" (lhs exprc) f
(Format.pp_print_list (Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ") ~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")
@ -611,7 +613,6 @@ module ExprGen (C : EXPR_PARAM) = struct
Format.pp_open_hvbox fmt 0; Format.pp_open_hvbox fmt 0;
pr false fmt e; pr false fmt e;
Format.pp_close_box fmt () Format.pp_close_box fmt ()
| EOp { op; _ } -> operator fmt op
| EDefault { excepts; just; cons } -> | EDefault { excepts; just; cons } ->
if List.length excepts = 0 then if List.length excepts = 0 then
Format.fprintf fmt "@[<hv 1>%a%a@ %a %a%a@]" Format.fprintf fmt "@[<hv 1>%a%a@ %a %a%a@]"
@ -734,7 +735,7 @@ module ExprConciseParam = struct
let lit = lit let lit = lit
let rec pre_map : type a. (a, 't) gexpr -> (a, 't) gexpr = function 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 | e -> e
end end
@ -929,6 +930,18 @@ let program ?(debug = false) fmt p =
(* - User-facing value printer - *) (* - 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 module UserFacing = struct
(* Refs: (* Refs:
https://en.wikipedia.org/wiki/Wikipedia:Manual_of_Style/Dates_and_numbers#Grouping_of_digits 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 "ø" | EEmptyError -> Format.pp_print_string ppf "ø"
| EAbs _ -> Format.pp_print_string ppf "<function>" | EAbs _ -> Format.pp_print_string ppf "<function>"
| EExternal _ -> Format.pp_print_string ppf "<external>" | EExternal _ -> Format.pp_print_string ppf "<external>"
| EApp _ | EOp _ | EVar _ | EIfThenElse _ | EMatch _ | ETupleAccess _ | EApp _ | EAppOp _ | EVar _ | EIfThenElse _ | EMatch _ | ETupleAccess _
| EStructAccess _ | EAssert _ | EDefault _ | EPureDefault _ | EStructAccess _ | EAssert _ | EDefault _ | EPureDefault _
| EErrorOnEmpty _ | ERaise _ | ECatch _ | ELocation _ | EScopeCall _ | EErrorOnEmpty _ | ERaise _ | ECatch _ | ELocation _ | EScopeCall _
| EDStructAccess _ | ECustom _ -> | EDStructAccess _ | ECustom _ ->
fallback ppf e 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 : let expr :
type a. Cli.backend_lang -> Format.formatter -> (a, 't) gexpr -> unit = type a. Cli.backend_lang -> Format.formatter -> (a, 't) gexpr -> unit =
fun lang -> fun lang ->

5
compiler/shared_ast/print.mli
View File

@ -125,3 +125,8 @@ module UserFacing : sig
(** This combines the user-facing value printer and the generic expression (** This combines the user-facing value printer and the generic expression
printer to handle all AST nodes *) printer to handle all AST nodes *)
end end
(**/*)
val skip_wrappers : ('a, 'm) gexpr -> ('a, 'm) gexpr
(** This is exported from [Expr], but first defined here for dependency reasons *)

131
compiler/shared_ast/typing.ml
View File

@ -327,7 +327,6 @@ let resolve_overload_ret_type
Operator.overload_type ctx Operator.overload_type ctx
(Mark.add (Expr.pos e) op) (Mark.add (Expr.pos e) op)
(List.map (typ_to_ast ~leave_unresolved) tys) (List.map (typ_to_ast ~leave_unresolved) tys)
(* We use [unsafe] because the error is caught below *)
in in
ast_to_typ (Type.arrow_return op_ty) ast_to_typ (Type.arrow_return op_ty)
@ -750,7 +749,7 @@ and typecheck_expr_top_down :
(unionfind ~pos:e1 tuple_ty) (unionfind ~pos:e1 tuple_ty)
e1 e1
in in
Expr.etupleaccess e1' index size context_mark Expr.etupleaccess ~e:e1' ~index ~size context_mark
| A.EAbs { binder; tys = t_args } -> | A.EAbs { binder; tys = t_args } ->
if Bindlib.mbinder_arity binder <> List.length t_args then if Bindlib.mbinder_arity binder <> List.length t_args then
Message.raise_spanned_error (Expr.pos e) Message.raise_spanned_error (Expr.pos e)
@ -774,98 +773,72 @@ and typecheck_expr_top_down :
in in
let binder' = Bindlib.bind_mvar xs' (Expr.Box.lift body') 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 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_args = List.map ast_to_typ tys in
let t_func = unionfind (TArrow (t_args, tau)) in let t_func = unionfind (TArrow (t_args, tau)) in
let e1', args' = let args =
Operator.kind_dispatch op Operator.kind_dispatch op
~polymorphic:(fun _ -> ~polymorphic:(fun op ->
(* Type the operator first, then right-to-left: polymorphic operators (* Type the operator first, then right-to-left: polymorphic operators
are required to allow the resolution of all type variables this are required to allow the resolution of all type variables this
way *) way *)
let e1' = unify ctx e (polymorphic_op_type (Mark.add pos_e op)) t_func;
typecheck_expr_top_down ~leave_unresolved ctx env t_func e1 List.rev_map2
in (typecheck_expr_top_down ~leave_unresolved ctx env)
let args' = (List.rev t_args) (List.rev args))
List.rev_map2 ~overloaded:(fun op ->
(typecheck_expr_top_down ~leave_unresolved ctx env)
(List.rev t_args) (List.rev args)
in
e1', args')
~overloaded:(fun _ ->
(* Typing the arguments first is required to resolve the operator *) (* Typing the arguments first is required to resolve the operator *)
let args' = let args' =
List.map2 List.map2
(typecheck_expr_top_down ~leave_unresolved ctx env) (typecheck_expr_top_down ~leave_unresolved ctx env)
t_args args t_args args
in in
let e1' = unify ctx e tau
typecheck_expr_top_down ~leave_unresolved ctx env t_func e1 (resolve_overload_ret_type ~leave_unresolved ctx e op t_args);
in args')
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)))
~monomorphic:(fun op -> ~monomorphic:(fun op ->
let mark = (* Here it doesn't matter but may affect the error messages *)
mark_with_tau_and_unify unify ctx e
(ast_to_typ (Operator.monomorphic_type (Mark.add pos_e op))) (ast_to_typ (Operator.monomorphic_type (Mark.add pos_e op)))
in t_func;
List.map (typ_to_ast ~leave_unresolved) tys', mark) List.map2
~overloaded:(fun op -> (typecheck_expr_top_down ~leave_unresolved ctx env)
unify ctx e t_ret t_args args)
(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 } ))
~resolved:(fun op -> ~resolved:(fun op ->
let mark = (* This case should not fail *)
mark_with_tau_and_unify unify ctx e
(ast_to_typ (Operator.resolved_type (Mark.add pos_e op))) (ast_to_typ (Operator.resolved_type (Mark.add pos_e op)))
in t_func;
List.map (typ_to_ast ~leave_unresolved) tys', mark) List.map2
(typecheck_expr_top_down ~leave_unresolved ctx env)
t_args args)
in 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 } -> | A.EDefault { excepts; just; cons } ->
let cons' = typecheck_expr_top_down ~leave_unresolved ctx env tau cons in let cons' = typecheck_expr_top_down ~leave_unresolved ctx env tau cons in
let just' = let just' =

9
compiler/shared_ast/typing.mli
View File

@ -61,9 +61,12 @@ val expr :
filling the gaps ([TAny]) if any. Use [Expr.untype] first if this is not filling the gaps ([TAny]) if any. Use [Expr.untype] first if this is not
what you want. what you want.
Note that typing also transparently performs disambiguation of constructors: Note that typing also transparently performs
[EDStructAccess] nodes are translated into [EStructAccess] with the suitable - disambiguation of constructors: [EDStructAccess] nodes are translated into
structure and field idents (this only concerns [desugared] expressions). *) [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 : val check_expr :
leave_unresolved:bool -> leave_unresolved:bool ->

48
compiler/verification/conditions.ml
View File

@ -38,15 +38,10 @@ let rec conjunction_exprs (exprs : typed expr list) (mark : typed mark) :
match exprs with match exprs with
| [] -> ELit (LBool true), mark | [] -> ELit (LBool true), mark
| hd :: tl -> | hd :: tl ->
( EApp ( EAppOp
{ {
f = op = And;
( EOp tys = [TLit TBool, Expr.pos hd; TLit TBool, Expr.pos hd];
{
op = And;
tys = [TLit TBool, Expr.pos hd; TLit TBool, Expr.pos hd];
},
mark );
args = [hd; conjunction_exprs tl mark]; args = [hd; conjunction_exprs tl mark];
}, },
mark ) mark )
@ -57,27 +52,17 @@ let conjunction (args : vc_return list) (mark : typed mark) : vc_return =
in in
List.fold_left List.fold_left
(fun acc arg -> (fun acc arg ->
( EApp ( EAppOp
{ {
f = op = And;
( EOp tys = [TLit TBool, Expr.pos acc; TLit TBool, Expr.pos arg];
{
op = And;
tys = [TLit TBool, Expr.pos acc; TLit TBool, Expr.pos arg];
},
mark );
args = [arg; acc]; args = [arg; acc];
}, },
mark )) mark ))
acc list acc list
let negation (arg : vc_return) (mark : typed mark) : vc_return = let negation (arg : vc_return) (mark : typed mark) : vc_return =
( EApp EAppOp { op = Not; tys = [TLit TBool, Expr.pos arg]; args = [arg] }, mark
{
f = EOp { op = Not; tys = [TLit TBool, Expr.pos arg] }, mark;
args = [arg];
},
mark )
let disjunction (args : vc_return list) (mark : typed mark) : vc_return = let disjunction (args : vc_return list) (mark : typed mark) : vc_return =
let acc, list = let acc, list =
@ -85,15 +70,10 @@ let disjunction (args : vc_return list) (mark : typed mark) : vc_return =
in in
List.fold_left List.fold_left
(fun (acc : vc_return) arg -> (fun (acc : vc_return) arg ->
( EApp ( EAppOp
{ {
f = op = Or;
( EOp tys = [TLit TBool, Expr.pos acc; TLit TBool, Expr.pos arg];
{
op = Or;
tys = [TLit TBool, Expr.pos acc; TLit TBool, Expr.pos arg];
},
mark );
args = [arg; acc]; args = [arg; acc];
}, },
mark )) mark ))
@ -117,7 +97,7 @@ let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : typed expr) :
| EErrorOnEmpty | EErrorOnEmpty
( EDefault ( EDefault
{ {
excepts = [(EApp { f = EVar x, _; args = [(ELit LUnit, _)] }, _)]; excepts = [(EApp { f = EVar x, _; args = [(ELit LUnit, _)]; _ }, _)];
just = ELit (LBool true), _; just = ELit (LBool true), _;
cons; 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 (* Per default calculus semantics, you cannot call a function with an argument
that evaluates to the empty error. Thus, all variable evaluate to that evaluates to the empty error. Thus, all variable evaluate to
non-empty-error terms. *) non-empty-error terms. *)
| ELit _ | EOp _ -> | ELit _ ->
Mark.copy e (ELit (LBool true)) Mark.copy e (ELit (LBool true))
| EApp { f; args } -> | EApp { f; args; _ } ->
(* Invariant: For the [EApp] case, we assume here that function calls never (* Invariant: For the [EApp] case, we assume here that function calls never
return empty error, which implies all functions have been checked never return empty error, which implies all functions have been checked never
to return empty errors. *) to return empty errors. *)
@ -250,7 +230,7 @@ let rec generate_vc_must_not_return_conflict (ctx : ctx) (e : typed expr) :
| EAbs { binder; _ } -> | EAbs { binder; _ } ->
let _vars, body = Bindlib.unmbind binder in let _vars, body = Bindlib.unmbind binder in
(generate_vc_must_not_return_conflict ctx) body (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 } -> | EDefault { excepts; just; cons } ->
(* <e1 ... en | ejust :- econs > never returns conflict if and only if: - (* <e1 ... en | ejust :- econs > never returns conflict if and only if: -
neither e1 nor ... nor en nor ejust nor econs return conflict - there is neither e1 nor ... nor en nor ejust nor econs return conflict - there is

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

@ -437,9 +437,9 @@ let rec translate_op :
let ill_formed () = let ill_formed () =
Format.kasprintf failwith Format.kasprintf failwith
"[Z3 encoding] Ill-formed operator application: %a" Shared_ast.Expr.format "[Z3 encoding] Ill-formed operator application: %a" Shared_ast.Expr.format
(Shared_ast.Expr.eapp (Shared_ast.Expr.eappop ~op
(Shared_ast.Expr.eop op [] (Untyped { pos = Pos.no_pos })) ~args:(List.map Shared_ast.Expr.untype args)
(List.map Shared_ast.Expr.untype args) ~tys:[]
(Untyped { pos = Pos.no_pos }) (Untyped { pos = Pos.no_pos })
|> Shared_ast.Expr.unbox) |> Shared_ast.Expr.unbox)
in in
@ -458,10 +458,7 @@ let rec translate_op :
failwith "[Z3 encoding] ternary operator application not supported" failwith "[Z3 encoding] ternary operator application not supported"
(* Special case for GetYear comparisons *) (* Special case for GetYear comparisons *)
| ( Lt_int_int, | ( Lt_int_int,
[ [(EAppOp { op = GetYear; args = [e1]; _ }, _); (ELit (LInt n), _)] ) ->
(EApp { f = EOp { op = GetYear; _ }, _; args = [e1] }, _);
(ELit (LInt n), _);
] ) ->
let n = Runtime.integer_to_int n in let n = Runtime.integer_to_int n in
let ctx, e1 = translate_expr ctx e1 in let ctx, e1 = translate_expr ctx e1 in
let e2 = let e2 =
@ -472,10 +469,7 @@ let rec translate_op :
days *) days *)
ctx, Arithmetic.mk_lt ctx.ctx_z3 e1 e2 ctx, Arithmetic.mk_lt ctx.ctx_z3 e1 e2
| ( Lte_int_int, | ( Lte_int_int,
[ [(EAppOp { op = GetYear; args = [e1]; _ }, _); (ELit (LInt n), _)] ) ->
(EApp { f = EOp { op = GetYear; _ }, _; args = [e1] }, _);
(ELit (LInt n), _);
] ) ->
let ctx, e1 = translate_expr ctx e1 in let ctx, e1 = translate_expr ctx e1 in
let nb_days = if is_leap_year n then 365 else 364 in let nb_days = if is_leap_year n then 365 else 364 in
let n = Runtime.integer_to_int n in let n = Runtime.integer_to_int n in
@ -489,10 +483,7 @@ let rec translate_op :
in in
ctx, Arithmetic.mk_le ctx.ctx_z3 e1 e2 ctx, Arithmetic.mk_le ctx.ctx_z3 e1 e2
| ( Gt_int_int, | ( Gt_int_int,
[ [(EAppOp { op = GetYear; args = [e1]; _ }, _); (ELit (LInt n), _)] ) ->
(EApp { f = EOp { op = GetYear; _ }, _; args = [e1] }, _);
(ELit (LInt n), _);
] ) ->
let ctx, e1 = translate_expr ctx e1 in let ctx, e1 = translate_expr ctx e1 in
let nb_days = if is_leap_year n then 365 else 364 in let nb_days = if is_leap_year n then 365 else 364 in
let n = Runtime.integer_to_int n in let n = Runtime.integer_to_int n in
@ -506,10 +497,7 @@ let rec translate_op :
in in
ctx, Arithmetic.mk_gt ctx.ctx_z3 e1 e2 ctx, Arithmetic.mk_gt ctx.ctx_z3 e1 e2
| ( Gte_int_int, | ( Gte_int_int,
[ [(EAppOp { op = GetYear; args = [e1]; _ }, _); (ELit (LInt n), _)] ) ->
(EApp { f = EOp { op = GetYear; _ }, _; args = [e1] }, _);
(ELit (LInt n), _);
] ) ->
let n = Runtime.integer_to_int n in let n = Runtime.integer_to_int n in
let ctx, e1 = translate_expr ctx e1 in let ctx, e1 = translate_expr ctx e1 in
let e2 = let e2 =
@ -519,11 +507,7 @@ let rec translate_op :
be directly translated as >= in the Z3 encoding using the number of be directly translated as >= in the Z3 encoding using the number of
days *) days *)
ctx, Arithmetic.mk_ge ctx.ctx_z3 e1 e2 ctx, Arithmetic.mk_ge ctx.ctx_z3 e1 e2
| ( Eq, | Eq, [(EAppOp { op = GetYear; args = [e1]; _ }, _); (ELit (LInt n), _)] ->
[
(EApp { f = EOp { op = GetYear; _ }, _; args = [e1] }, _);
(ELit (LInt n), _);
] ) ->
let n = Runtime.integer_to_int n in let n = Runtime.integer_to_int n in
let ctx, e1 = translate_expr ctx e1 in let ctx, e1 = translate_expr ctx e1 in
let min_date = let min_date =
@ -733,9 +717,9 @@ and translate_expr (ctx : context) (vc : typed expr) : context * Expr.expr =
| EArray _ -> failwith "[Z3 encoding] EArray unsupported" | EArray _ -> failwith "[Z3 encoding] EArray unsupported"
| ELit l -> ctx, translate_lit ctx l | ELit l -> ctx, translate_lit ctx l
| EAbs _ -> failwith "[Z3 encoding] EAbs unsupported" | 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 match Mark.remove head with
| EOp { op; _ } -> translate_op ctx op args
| EVar v -> | EVar v ->
let (Typed { ty = f_ty; _ }) = Mark.get head in let (Typed { ty = f_ty; _ }) = Mark.get head in
let ctx, fd = find_or_create_funcdecl ctx v f_ty 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 \ "[Z3 encoding] EApp node: Catala function calls should only include \
operators or function names") operators or function names")
| EAssert e -> translate_expr ctx e | EAssert e -> translate_expr ctx e
| EOp _ -> failwith "[Z3 encoding] EOp unsupported"
| EDefault _ -> failwith "[Z3 encoding] EDefault unsupported" | EDefault _ -> failwith "[Z3 encoding] EDefault unsupported"
| EPureDefault _ -> failwith "[Z3 encoding] EPureDefault unsupported" | EPureDefault _ -> failwith "[Z3 encoding] EPureDefault unsupported"
| EIfThenElse { cond = e_if; etrue = e_then; efalse = e_else } -> | EIfThenElse { cond = e_if; etrue = e_then; efalse = e_else } ->