2020-11-23 12:44:06 +03:00
|
|
|
(* This file is part of the Catala compiler, a specification language for tax
|
|
|
|
and social benefits computation rules. Copyright (C) 2020 Inria, contributor:
|
2021-05-29 19:56:20 +03:00
|
|
|
Denis Merigoux <denis.merigoux@inria.fr>, Emile Rolley <emile.rolley@tuta.io>
|
2020-11-23 12:44:06 +03:00
|
|
|
|
|
|
|
Licensed under the Apache License, Version 2.0 (the "License"); you may not
|
|
|
|
use this file except in compliance with the License. You may obtain a copy of
|
|
|
|
the License at
|
|
|
|
|
|
|
|
http://www.apache.org/licenses/LICENSE-2.0
|
|
|
|
|
|
|
|
Unless required by applicable law or agreed to in writing, software
|
|
|
|
distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
|
|
|
|
WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
|
|
|
|
License for the specific language governing permissions and limitations under
|
|
|
|
the License. *)
|
|
|
|
|
2020-12-14 20:09:38 +03:00
|
|
|
(** Reference interpreter for the default calculus *)
|
|
|
|
|
2021-01-21 23:33:04 +03:00
|
|
|
open Utils
|
2020-11-23 12:44:06 +03:00
|
|
|
module A = Ast
|
|
|
|
|
2020-12-14 20:09:38 +03:00
|
|
|
(** {1 Helpers} *)
|
|
|
|
|
2020-11-23 12:44:06 +03:00
|
|
|
let is_empty_error (e : A.expr Pos.marked) : bool =
|
|
|
|
match Pos.unmark e with ELit LEmptyError -> true | _ -> false
|
|
|
|
|
2021-01-09 19:44:45 +03:00
|
|
|
let log_indent = ref 0
|
|
|
|
|
2020-12-14 20:09:38 +03:00
|
|
|
(** {1 Evaluation} *)
|
|
|
|
|
2021-01-14 02:17:24 +03:00
|
|
|
let rec evaluate_operator
|
|
|
|
(ctx : Ast.decl_ctx)
|
|
|
|
(op : A.operator Pos.marked)
|
|
|
|
(args : A.expr Pos.marked list) : A.expr Pos.marked =
|
2021-05-31 11:42:20 +03:00
|
|
|
(* Try to apply [div] and if a [Division_by_zero] exceptions is catched, use
|
|
|
|
[op] to raise multispanned errors. *)
|
2021-05-29 21:17:22 +03:00
|
|
|
let apply_div_or_raise_err (div : unit -> A.expr) (op : A.operator Pos.marked)
|
|
|
|
: A.expr =
|
2021-05-29 19:56:20 +03:00
|
|
|
try div ()
|
|
|
|
with Division_by_zero ->
|
2022-03-08 15:04:27 +03:00
|
|
|
Errors.raise_multispanned_error
|
2021-05-29 19:56:20 +03:00
|
|
|
[
|
|
|
|
Some "The division operator:", Pos.get_position op;
|
|
|
|
Some "The null denominator:", Pos.get_position (List.nth args 1);
|
|
|
|
]
|
2022-03-08 15:04:27 +03:00
|
|
|
"division by zero at runtime"
|
2021-05-29 19:56:20 +03:00
|
|
|
in
|
2021-05-31 11:56:13 +03:00
|
|
|
let get_binop_args_pos (args : (A.expr * Pos.t) list) :
|
|
|
|
(string option * Pos.t) list =
|
|
|
|
[
|
|
|
|
None, Pos.get_position (List.nth args 0);
|
|
|
|
None, Pos.get_position (List.nth args 1);
|
|
|
|
]
|
|
|
|
in
|
2021-05-31 11:42:20 +03:00
|
|
|
(* Try to apply [cmp] and if a [UncomparableDurations] exceptions is catched,
|
|
|
|
use [args] to raise multispanned errors. *)
|
2021-05-29 21:17:22 +03:00
|
|
|
let apply_cmp_or_raise_err
|
|
|
|
(cmp : unit -> A.expr)
|
|
|
|
(args : (A.expr * Pos.t) list) : A.expr =
|
|
|
|
try cmp ()
|
|
|
|
with Runtime.UncomparableDurations ->
|
2022-03-08 15:04:27 +03:00
|
|
|
Errors.raise_multispanned_error (get_binop_args_pos args)
|
2021-05-29 21:17:22 +03:00
|
|
|
"Cannot compare together durations that cannot be converted to a \
|
|
|
|
precise number of days"
|
|
|
|
in
|
2020-11-24 13:27:23 +03:00
|
|
|
Pos.same_pos_as
|
2021-03-16 22:34:03 +03:00
|
|
|
(match Pos.unmark op, List.map Pos.unmark args with
|
2020-12-30 00:26:10 +03:00
|
|
|
| A.Ternop A.Fold, [_f; _init; EArray es] ->
|
2020-12-28 01:53:02 +03:00
|
|
|
Pos.unmark
|
|
|
|
(List.fold_left
|
|
|
|
(fun acc e' ->
|
2021-01-14 02:17:24 +03:00
|
|
|
evaluate_expr ctx
|
|
|
|
(Pos.same_pos_as (A.EApp (List.nth args 0, [acc; e'])) e'))
|
2020-12-28 01:53:02 +03:00
|
|
|
(List.nth args 1) es)
|
2020-11-24 13:27:23 +03:00
|
|
|
| A.Binop A.And, [ELit (LBool b1); ELit (LBool b2)] ->
|
|
|
|
A.ELit (LBool (b1 && b2))
|
|
|
|
| A.Binop A.Or, [ELit (LBool b1); ELit (LBool b2)] ->
|
|
|
|
A.ELit (LBool (b1 || b2))
|
2021-03-16 22:34:03 +03:00
|
|
|
| A.Binop A.Xor, [ELit (LBool b1); ELit (LBool b2)] ->
|
|
|
|
A.ELit (LBool (b1 <> b2))
|
2021-03-05 21:16:56 +03:00
|
|
|
| A.Binop (A.Add KInt), [ELit (LInt i1); ELit (LInt i2)] ->
|
|
|
|
A.ELit (LInt Runtime.(i1 +! i2))
|
|
|
|
| A.Binop (A.Sub KInt), [ELit (LInt i1); ELit (LInt i2)] ->
|
|
|
|
A.ELit (LInt Runtime.(i1 -! i2))
|
|
|
|
| A.Binop (A.Mult KInt), [ELit (LInt i1); ELit (LInt i2)] ->
|
|
|
|
A.ELit (LInt Runtime.(i1 *! i2))
|
2020-12-09 16:51:22 +03:00
|
|
|
| A.Binop (A.Div KInt), [ELit (LInt i1); ELit (LInt i2)] ->
|
2021-05-29 21:17:22 +03:00
|
|
|
apply_div_or_raise_err (fun _ -> A.ELit (LInt Runtime.(i1 /! i2))) op
|
2021-03-05 21:16:56 +03:00
|
|
|
| A.Binop (A.Add KRat), [ELit (LRat i1); ELit (LRat i2)] ->
|
|
|
|
A.ELit (LRat Runtime.(i1 +& i2))
|
|
|
|
| A.Binop (A.Sub KRat), [ELit (LRat i1); ELit (LRat i2)] ->
|
|
|
|
A.ELit (LRat Runtime.(i1 -& i2))
|
|
|
|
| A.Binop (A.Mult KRat), [ELit (LRat i1); ELit (LRat i2)] ->
|
|
|
|
A.ELit (LRat Runtime.(i1 *& i2))
|
2021-05-29 19:56:20 +03:00
|
|
|
| A.Binop (A.Div KRat), [ELit (LRat i1); ELit (LRat i2)] ->
|
2021-05-29 21:17:22 +03:00
|
|
|
apply_div_or_raise_err (fun _ -> A.ELit (LRat Runtime.(i1 /& i2))) op
|
2021-05-31 11:56:13 +03:00
|
|
|
| A.Binop (A.Add KMoney), [ELit (LMoney m1); ELit (LMoney m2)] ->
|
|
|
|
A.ELit (LMoney Runtime.(m1 +$ m2))
|
|
|
|
| A.Binop (A.Sub KMoney), [ELit (LMoney m1); ELit (LMoney m2)] ->
|
|
|
|
A.ELit (LMoney Runtime.(m1 -$ m2))
|
|
|
|
| A.Binop (A.Mult KMoney), [ELit (LMoney m1); ELit (LRat m2)] ->
|
|
|
|
A.ELit (LMoney Runtime.(m1 *$ m2))
|
|
|
|
| A.Binop (A.Div KMoney), [ELit (LMoney m1); ELit (LMoney m2)] ->
|
|
|
|
apply_div_or_raise_err (fun _ -> A.ELit (LRat Runtime.(m1 /$ m2))) op
|
|
|
|
| A.Binop (A.Add KDuration), [ELit (LDuration d1); ELit (LDuration d2)] ->
|
|
|
|
A.ELit (LDuration Runtime.(d1 +^ d2))
|
|
|
|
| A.Binop (A.Sub KDuration), [ELit (LDuration d1); ELit (LDuration d2)] ->
|
|
|
|
A.ELit (LDuration Runtime.(d1 -^ d2))
|
|
|
|
| A.Binop (A.Sub KDate), [ELit (LDate d1); ELit (LDate d2)] ->
|
|
|
|
A.ELit (LDuration Runtime.(d1 -@ d2))
|
|
|
|
| A.Binop (A.Add KDate), [ELit (LDate d1); ELit (LDuration d2)] ->
|
|
|
|
A.ELit (LDate Runtime.(d1 +@ d2))
|
|
|
|
| A.Binop (A.Div KDuration), [ELit (LDuration d1); ELit (LDuration d2)] ->
|
2021-05-31 11:42:20 +03:00
|
|
|
apply_div_or_raise_err
|
|
|
|
(fun _ ->
|
2021-05-31 11:56:13 +03:00
|
|
|
try A.ELit (LRat Runtime.(d1 /^ d2))
|
2021-05-31 11:42:20 +03:00
|
|
|
with Runtime.IndivisableDurations ->
|
2022-03-08 15:04:27 +03:00
|
|
|
Errors.raise_multispanned_error (get_binop_args_pos args)
|
|
|
|
"Cannot divide durations that cannot be converted to a precise \
|
|
|
|
number of days")
|
2022-05-12 16:10:55 +03:00
|
|
|
op
|
2022-05-31 21:00:52 +03:00
|
|
|
| A.Binop (A.Mult KDuration), [ELit (LDuration d1); ELit (LInt i1)] ->
|
|
|
|
A.ELit (LDuration Runtime.(d1 *^ i1))
|
2021-03-05 21:16:56 +03:00
|
|
|
| A.Binop (A.Lt KInt), [ELit (LInt i1); ELit (LInt i2)] ->
|
|
|
|
A.ELit (LBool Runtime.(i1 <! i2))
|
|
|
|
| A.Binop (A.Lte KInt), [ELit (LInt i1); ELit (LInt i2)] ->
|
|
|
|
A.ELit (LBool Runtime.(i1 <=! i2))
|
|
|
|
| A.Binop (A.Gt KInt), [ELit (LInt i1); ELit (LInt i2)] ->
|
|
|
|
A.ELit (LBool Runtime.(i1 >! i2))
|
|
|
|
| A.Binop (A.Gte KInt), [ELit (LInt i1); ELit (LInt i2)] ->
|
|
|
|
A.ELit (LBool Runtime.(i1 >=! i2))
|
|
|
|
| A.Binop (A.Lt KRat), [ELit (LRat i1); ELit (LRat i2)] ->
|
|
|
|
A.ELit (LBool Runtime.(i1 <& i2))
|
|
|
|
| A.Binop (A.Lte KRat), [ELit (LRat i1); ELit (LRat i2)] ->
|
|
|
|
A.ELit (LBool Runtime.(i1 <=& i2))
|
|
|
|
| A.Binop (A.Gt KRat), [ELit (LRat i1); ELit (LRat i2)] ->
|
|
|
|
A.ELit (LBool Runtime.(i1 >& i2))
|
|
|
|
| A.Binop (A.Gte KRat), [ELit (LRat i1); ELit (LRat i2)] ->
|
|
|
|
A.ELit (LBool Runtime.(i1 >=& i2))
|
2021-05-31 11:56:13 +03:00
|
|
|
| A.Binop (A.Lt KMoney), [ELit (LMoney m1); ELit (LMoney m2)] ->
|
|
|
|
A.ELit (LBool Runtime.(m1 <$ m2))
|
|
|
|
| A.Binop (A.Lte KMoney), [ELit (LMoney m1); ELit (LMoney m2)] ->
|
|
|
|
A.ELit (LBool Runtime.(m1 <=$ m2))
|
|
|
|
| A.Binop (A.Gt KMoney), [ELit (LMoney m1); ELit (LMoney m2)] ->
|
|
|
|
A.ELit (LBool Runtime.(m1 >$ m2))
|
|
|
|
| A.Binop (A.Gte KMoney), [ELit (LMoney m1); ELit (LMoney m2)] ->
|
|
|
|
A.ELit (LBool Runtime.(m1 >=$ m2))
|
|
|
|
| A.Binop (A.Lt KDuration), [ELit (LDuration d1); ELit (LDuration d2)] ->
|
2020-12-30 00:26:10 +03:00
|
|
|
apply_cmp_or_raise_err (fun _ -> A.ELit (LBool Runtime.(d1 <^ d2))) args
|
2021-05-31 11:56:13 +03:00
|
|
|
| A.Binop (A.Lte KDuration), [ELit (LDuration d1); ELit (LDuration d2)] ->
|
|
|
|
apply_cmp_or_raise_err (fun _ -> A.ELit (LBool Runtime.(d1 <=^ d2))) args
|
|
|
|
| A.Binop (A.Gt KDuration), [ELit (LDuration d1); ELit (LDuration d2)] ->
|
|
|
|
apply_cmp_or_raise_err (fun _ -> A.ELit (LBool Runtime.(d1 >^ d2))) args
|
|
|
|
| A.Binop (A.Gte KDuration), [ELit (LDuration d1); ELit (LDuration d2)] ->
|
|
|
|
apply_cmp_or_raise_err (fun _ -> A.ELit (LBool Runtime.(d1 >=^ d2))) args
|
|
|
|
| A.Binop (A.Lt KDate), [ELit (LDate d1); ELit (LDate d2)] ->
|
|
|
|
A.ELit (LBool Runtime.(d1 <@ d2))
|
|
|
|
| A.Binop (A.Lte KDate), [ELit (LDate d1); ELit (LDate d2)] ->
|
|
|
|
A.ELit (LBool Runtime.(d1 <=@ d2))
|
|
|
|
| A.Binop (A.Gt KDate), [ELit (LDate d1); ELit (LDate d2)] ->
|
|
|
|
A.ELit (LBool Runtime.(d1 >@ d2))
|
|
|
|
| A.Binop (A.Gte KDate), [ELit (LDate d1); ELit (LDate d2)] ->
|
|
|
|
A.ELit (LBool Runtime.(d1 >=@ d2))
|
2020-12-31 02:28:26 +03:00
|
|
|
| A.Binop A.Eq, [ELit LUnit; ELit LUnit] -> A.ELit (LBool true)
|
2021-05-31 11:56:13 +03:00
|
|
|
| A.Binop A.Eq, [ELit (LDuration d1); ELit (LDuration d2)] ->
|
|
|
|
A.ELit (LBool Runtime.(d1 =^ d2))
|
|
|
|
| A.Binop A.Eq, [ELit (LDate d1); ELit (LDate d2)] ->
|
|
|
|
A.ELit (LBool Runtime.(d1 =@ d2))
|
|
|
|
| A.Binop A.Eq, [ELit (LMoney m1); ELit (LMoney m2)] ->
|
|
|
|
A.ELit (LBool Runtime.(m1 =$ m2))
|
2021-03-05 21:16:56 +03:00
|
|
|
| A.Binop A.Eq, [ELit (LRat i1); ELit (LRat i2)] ->
|
|
|
|
A.ELit (LBool Runtime.(i1 =& i2))
|
|
|
|
| A.Binop A.Eq, [ELit (LInt i1); ELit (LInt i2)] ->
|
|
|
|
A.ELit (LBool Runtime.(i1 =! i2))
|
2020-11-24 13:27:23 +03:00
|
|
|
| A.Binop A.Eq, [ELit (LBool b1); ELit (LBool b2)] ->
|
|
|
|
A.ELit (LBool (b1 = b2))
|
2020-12-30 00:26:10 +03:00
|
|
|
| A.Binop A.Eq, [EArray es1; EArray es2] ->
|
2022-05-12 16:10:55 +03:00
|
|
|
A.ELit
|
|
|
|
(LBool
|
|
|
|
(try
|
2021-03-16 22:34:03 +03:00
|
|
|
List.for_all2
|
|
|
|
(fun e1 e2 ->
|
|
|
|
match Pos.unmark (evaluate_operator ctx op [e1; e2]) with
|
|
|
|
| A.ELit (LBool b) -> b
|
|
|
|
| _ -> assert false
|
|
|
|
(* should not happen *))
|
2022-05-12 16:10:55 +03:00
|
|
|
es1 es2
|
2021-03-16 22:34:03 +03:00
|
|
|
with Invalid_argument _ -> false))
|
2021-01-14 02:17:24 +03:00
|
|
|
| A.Binop A.Eq, [ETuple (es1, s1); ETuple (es2, s2)] ->
|
2022-05-12 16:10:55 +03:00
|
|
|
A.ELit
|
|
|
|
(LBool
|
|
|
|
(try
|
|
|
|
s1 = s2
|
2021-03-16 22:34:03 +03:00
|
|
|
&& List.for_all2
|
|
|
|
(fun e1 e2 ->
|
|
|
|
match Pos.unmark (evaluate_operator ctx op [e1; e2]) with
|
|
|
|
| A.ELit (LBool b) -> b
|
|
|
|
| _ -> assert false
|
|
|
|
(* should not happen *))
|
2022-05-12 16:10:55 +03:00
|
|
|
es1 es2
|
2021-03-16 22:34:03 +03:00
|
|
|
with Invalid_argument _ -> false))
|
2021-04-07 22:17:13 +03:00
|
|
|
| A.Binop A.Eq, [EInj (e1, i1, en1, _ts1); EInj (e2, i2, en2, _ts2)] ->
|
2022-05-12 16:10:55 +03:00
|
|
|
A.ELit
|
|
|
|
(LBool
|
|
|
|
(try
|
2021-04-07 22:17:13 +03:00
|
|
|
en1 = en2 && i1 = i2
|
2022-05-12 16:10:55 +03:00
|
|
|
&&
|
2021-03-16 22:34:03 +03:00
|
|
|
match Pos.unmark (evaluate_operator ctx op [e1; e2]) with
|
|
|
|
| A.ELit (LBool b) -> b
|
|
|
|
| _ -> assert false
|
|
|
|
(* should not happen *)
|
|
|
|
with Invalid_argument _ -> false))
|
2020-12-30 00:26:10 +03:00
|
|
|
| A.Binop A.Eq, [_; _] ->
|
|
|
|
A.ELit (LBool false) (* comparing anything else return false *)
|
|
|
|
| A.Binop A.Neq, [_; _] -> (
|
2022-05-12 16:10:55 +03:00
|
|
|
match
|
2020-12-28 01:53:02 +03:00
|
|
|
Pos.unmark
|
2021-01-14 02:17:24 +03:00
|
|
|
(evaluate_operator ctx (Pos.same_pos_as (A.Binop A.Eq) op) args)
|
2022-05-12 16:10:55 +03:00
|
|
|
with
|
2020-12-28 01:53:02 +03:00
|
|
|
| A.ELit (A.LBool b) -> A.ELit (A.LBool (not b))
|
|
|
|
| _ -> assert false (*should not happen *))
|
2021-07-09 20:44:55 +03:00
|
|
|
| A.Binop A.Concat, [A.EArray es1; A.EArray es2] -> A.EArray (es1 @ es2)
|
2020-12-28 01:53:02 +03:00
|
|
|
| A.Binop A.Map, [_; A.EArray es] ->
|
2022-05-12 16:10:55 +03:00
|
|
|
A.EArray
|
2020-12-28 01:53:02 +03:00
|
|
|
(List.map
|
|
|
|
(fun e' ->
|
2021-01-14 02:17:24 +03:00
|
|
|
evaluate_expr ctx
|
2020-12-28 01:53:02 +03:00
|
|
|
(Pos.same_pos_as (A.EApp (List.nth args 0, [e'])) e'))
|
2022-05-12 16:10:55 +03:00
|
|
|
es)
|
2021-01-10 20:11:46 +03:00
|
|
|
| A.Binop A.Filter, [_; A.EArray es] ->
|
2022-05-12 16:10:55 +03:00
|
|
|
A.EArray
|
2021-01-10 20:11:46 +03:00
|
|
|
(List.filter
|
2021-01-14 02:17:24 +03:00
|
|
|
(fun e' ->
|
2022-05-12 16:10:55 +03:00
|
|
|
match
|
2021-01-14 02:17:24 +03:00
|
|
|
evaluate_expr ctx
|
|
|
|
(Pos.same_pos_as (A.EApp (List.nth args 0, [e'])) e')
|
2020-12-28 01:53:02 +03:00
|
|
|
with
|
2021-03-16 22:34:03 +03:00
|
|
|
| A.ELit (A.LBool b), _ -> b
|
2021-03-05 21:16:56 +03:00
|
|
|
| _ ->
|
2021-05-29 21:17:22 +03:00
|
|
|
Errors.raise_spanned_error
|
|
|
|
(Pos.get_position (List.nth args 0))
|
2021-05-29 19:56:20 +03:00
|
|
|
"This predicate evaluated to something else than a boolean \
|
2021-05-29 21:17:22 +03:00
|
|
|
(should not happen if the term was well-typed)")
|
2021-05-31 11:56:13 +03:00
|
|
|
es)
|
|
|
|
| A.Binop _, ([ELit LEmptyError; _] | [_; ELit LEmptyError]) ->
|
|
|
|
A.ELit LEmptyError
|
|
|
|
| A.Unop (A.Minus KInt), [ELit (LInt i)] ->
|
|
|
|
A.ELit (LInt Runtime.(integer_of_int 0 -! i))
|
|
|
|
| A.Unop (A.Minus KRat), [ELit (LRat i)] ->
|
|
|
|
A.ELit (LRat Runtime.(decimal_of_string "0" -& i))
|
2021-03-05 21:16:56 +03:00
|
|
|
| A.Unop (A.Minus KMoney), [ELit (LMoney i)] ->
|
|
|
|
A.ELit (LMoney Runtime.(money_of_units_int 0 -$ i))
|
|
|
|
| A.Unop (A.Minus KDuration), [ELit (LDuration i)] ->
|
|
|
|
A.ELit (LDuration Runtime.(~-^i))
|
|
|
|
| A.Unop A.Not, [ELit (LBool b)] -> A.ELit (LBool (not b))
|
|
|
|
| A.Unop A.Length, [EArray es] ->
|
2021-05-31 11:56:13 +03:00
|
|
|
A.ELit (LInt (Runtime.integer_of_int (List.length es)))
|
|
|
|
| A.Unop A.GetDay, [ELit (LDate d)] ->
|
|
|
|
A.ELit (LInt Runtime.(day_of_month_of_date d))
|
|
|
|
| A.Unop A.GetMonth, [ELit (LDate d)] ->
|
|
|
|
A.ELit (LInt Runtime.(month_number_of_date d))
|
|
|
|
| A.Unop A.GetYear, [ELit (LDate d)] ->
|
|
|
|
A.ELit (LInt Runtime.(year_of_date d))
|
|
|
|
| A.Unop A.IntToRat, [ELit (LInt i)] ->
|
|
|
|
A.ELit (LRat Runtime.(decimal_of_integer i))
|
|
|
|
| A.Unop A.RoundMoney, [ELit (LMoney m)] ->
|
|
|
|
A.ELit (LMoney Runtime.(money_round m))
|
2021-03-05 21:16:56 +03:00
|
|
|
| A.Unop A.RoundDecimal, [ELit (LRat m)] ->
|
|
|
|
A.ELit (LRat Runtime.(decimal_round m))
|
|
|
|
| A.Unop (A.Log (entry, infos)), [e'] ->
|
2021-03-16 22:34:03 +03:00
|
|
|
if !Cli.trace_flag then (
|
|
|
|
match entry with
|
|
|
|
| VarDef _ ->
|
|
|
|
(* TODO: this usage of Format is broken, Formatting requires that all
|
|
|
|
is formatted in one pass, without going through intermediate
|
|
|
|
"%s" *)
|
|
|
|
Cli.log_format "%*s%a %a: %s" (!log_indent * 2) ""
|
|
|
|
Print.format_log_entry entry Print.format_uid_list infos
|
|
|
|
(match e' with
|
2022-07-13 18:27:08 +03:00
|
|
|
| Ast.EAbs _ -> Cli.with_style [ANSITerminal.green] "<function>"
|
2020-12-30 00:26:10 +03:00
|
|
|
| _ ->
|
2022-03-08 15:04:27 +03:00
|
|
|
let expr_str =
|
2021-01-14 02:17:24 +03:00
|
|
|
Format.asprintf "%a"
|
|
|
|
(Print.format_expr ctx ~debug:false)
|
|
|
|
(e', Pos.no_pos)
|
2022-05-12 16:10:55 +03:00
|
|
|
in
|
2021-01-14 02:17:24 +03:00
|
|
|
let expr_str =
|
|
|
|
Re.Pcre.substitute ~rex:(Re.Pcre.regexp "\n\\s*")
|
2021-01-10 20:11:46 +03:00
|
|
|
~subst:(fun _ -> " ")
|
2021-01-14 02:17:24 +03:00
|
|
|
expr_str
|
2022-03-08 15:04:27 +03:00
|
|
|
in
|
2020-12-09 13:23:03 +03:00
|
|
|
Cli.with_style [ANSITerminal.green] "%s" expr_str)
|
|
|
|
| PosRecordIfTrueBool -> (
|
2021-03-05 21:16:56 +03:00
|
|
|
let pos = Pos.get_position op in
|
|
|
|
match pos <> Pos.no_pos, e' with
|
2020-11-24 13:27:23 +03:00
|
|
|
| true, ELit (LBool true) ->
|
2021-03-05 21:16:56 +03:00
|
|
|
Cli.log_format "%*s%a%s:\n%s" (!log_indent * 2) ""
|
|
|
|
Print.format_log_entry entry
|
|
|
|
(Cli.with_style [ANSITerminal.green] "Definition applied")
|
|
|
|
(Cli.add_prefix_to_each_line (Pos.retrieve_loc_text pos) (fun _ ->
|
2022-03-08 16:55:48 +03:00
|
|
|
Format.asprintf "%*s" (!log_indent * 2) ""))
|
2021-03-16 22:34:03 +03:00
|
|
|
| _ -> ())
|
2022-03-08 15:04:27 +03:00
|
|
|
| BeginCall ->
|
|
|
|
Cli.log_format "%*s%a %a" (!log_indent * 2) "" Print.format_log_entry
|
|
|
|
entry Print.format_uid_list infos;
|
|
|
|
log_indent := !log_indent + 1
|
|
|
|
| EndCall ->
|
|
|
|
log_indent := !log_indent - 1;
|
|
|
|
Cli.log_format "%*s%a %a" (!log_indent * 2) "" Print.format_log_entry
|
|
|
|
entry Print.format_uid_list infos)
|
2020-12-11 12:51:46 +03:00
|
|
|
else ();
|
|
|
|
e'
|
2020-12-09 13:23:03 +03:00
|
|
|
| A.Unop _, [ELit LEmptyError] -> A.ELit LEmptyError
|
2020-11-24 13:27:23 +03:00
|
|
|
| _ ->
|
|
|
|
Errors.raise_multispanned_error
|
2021-03-16 22:34:03 +03:00
|
|
|
([Some "Operator:", Pos.get_position op]
|
2020-12-10 13:35:56 +03:00
|
|
|
@ List.mapi
|
2020-12-10 18:58:32 +03:00
|
|
|
(fun i arg ->
|
2021-01-14 02:17:24 +03:00
|
|
|
( Some
|
2022-01-10 16:19:04 +03:00
|
|
|
(Format.asprintf "Argument n°%d, value %a" (i + 1)
|
|
|
|
(Print.format_expr ctx ~debug:true)
|
|
|
|
arg),
|
2020-12-10 18:58:32 +03:00
|
|
|
Pos.get_position arg ))
|
2022-03-08 15:04:27 +03:00
|
|
|
args)
|
|
|
|
"Operator applied to the wrong arguments\n\
|
|
|
|
(should not happen if the term was well-typed)")
|
2020-11-24 13:27:23 +03:00
|
|
|
op
|
|
|
|
|
2021-01-14 02:17:24 +03:00
|
|
|
and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) :
|
|
|
|
A.expr Pos.marked =
|
2020-11-23 18:12:45 +03:00
|
|
|
match Pos.unmark e with
|
|
|
|
| EVar _ ->
|
2022-03-08 15:04:27 +03:00
|
|
|
Errors.raise_spanned_error (Pos.get_position e)
|
2020-11-23 18:12:45 +03:00
|
|
|
"free variable found at evaluation (should not happen if term was \
|
|
|
|
well-typed"
|
2020-11-24 12:28:39 +03:00
|
|
|
| EApp (e1, args) -> (
|
2021-01-14 02:17:24 +03:00
|
|
|
let e1 = evaluate_expr ctx e1 in
|
|
|
|
let args = List.map (evaluate_expr ctx) args in
|
2020-11-23 18:12:45 +03:00
|
|
|
match Pos.unmark e1 with
|
2021-04-03 12:49:13 +03:00
|
|
|
| EAbs ((binder, _), _) ->
|
2020-11-24 12:28:39 +03:00
|
|
|
if Bindlib.mbinder_arity binder = List.length args then
|
2021-01-14 02:17:24 +03:00
|
|
|
evaluate_expr ctx
|
|
|
|
(Bindlib.msubst binder (Array.of_list (List.map Pos.unmark args)))
|
2020-11-24 12:28:39 +03:00
|
|
|
else
|
2022-03-08 15:04:27 +03:00
|
|
|
Errors.raise_spanned_error (Pos.get_position e)
|
|
|
|
"wrong function call, expected %d arguments, got %d"
|
|
|
|
(Bindlib.mbinder_arity binder)
|
|
|
|
(List.length args)
|
2021-01-14 02:17:24 +03:00
|
|
|
| EOp op ->
|
|
|
|
Pos.same_pos_as
|
|
|
|
(Pos.unmark (evaluate_operator ctx (Pos.same_pos_as op e1) args))
|
|
|
|
e
|
2020-11-23 18:12:45 +03:00
|
|
|
| ELit LEmptyError -> Pos.same_pos_as (A.ELit LEmptyError) e
|
|
|
|
| _ ->
|
2022-03-08 15:04:27 +03:00
|
|
|
Errors.raise_spanned_error (Pos.get_position e)
|
2020-11-23 18:12:45 +03:00
|
|
|
"function has not been reduced to a lambda at evaluation (should not \
|
2022-03-08 15:04:27 +03:00
|
|
|
happen if the term was well-typed")
|
2022-02-02 12:30:39 +03:00
|
|
|
| EAbs _ | ELit _ | EOp _ -> e (* these are values *)
|
2021-04-03 16:07:49 +03:00
|
|
|
| ETuple (es, s) ->
|
|
|
|
let new_es = List.map (evaluate_expr ctx) es in
|
|
|
|
if List.exists is_empty_error new_es then
|
|
|
|
Pos.same_pos_as (A.ELit LEmptyError) e
|
|
|
|
else Pos.same_pos_as (A.ETuple (new_es, s)) e
|
2021-01-14 02:17:24 +03:00
|
|
|
| ETupleAccess (e1, n, s, _) -> (
|
|
|
|
let e1 = evaluate_expr ctx e1 in
|
2020-11-23 18:12:45 +03:00
|
|
|
match Pos.unmark e1 with
|
2021-01-14 02:17:24 +03:00
|
|
|
| ETuple (es, s') -> (
|
2021-03-16 22:34:03 +03:00
|
|
|
(match s, s' with
|
2021-01-14 02:17:24 +03:00
|
|
|
| None, None -> ()
|
|
|
|
| Some s, Some s' when s = s' -> ()
|
2020-11-23 18:12:45 +03:00
|
|
|
| _ ->
|
2021-01-14 02:17:24 +03:00
|
|
|
Errors.raise_multispanned_error
|
2022-03-08 15:04:27 +03:00
|
|
|
[None, Pos.get_position e; None, Pos.get_position e1]
|
2021-01-14 02:17:24 +03:00
|
|
|
"Error during tuple access: not the same structs (should not happen \
|
2022-03-08 15:04:27 +03:00
|
|
|
if the term was well-typed)");
|
2020-11-23 18:12:45 +03:00
|
|
|
match List.nth_opt es n with
|
2021-01-14 02:17:24 +03:00
|
|
|
| Some e' -> e'
|
2020-11-23 18:12:45 +03:00
|
|
|
| None ->
|
2022-03-08 15:04:27 +03:00
|
|
|
Errors.raise_spanned_error (Pos.get_position e1)
|
|
|
|
"The tuple has %d components but the %i-th element was requested \
|
|
|
|
(should not happen if the term was well-type)"
|
|
|
|
(List.length es) n)
|
2021-04-03 16:07:49 +03:00
|
|
|
| ELit LEmptyError -> Pos.same_pos_as (A.ELit LEmptyError) e
|
2022-05-12 16:10:55 +03:00
|
|
|
| _ ->
|
2022-03-08 15:04:27 +03:00
|
|
|
Errors.raise_spanned_error (Pos.get_position e1)
|
|
|
|
"The expression %a should be a tuple with %d components but is not \
|
|
|
|
(should not happen if the term was well-typed)"
|
|
|
|
(Print.format_expr ctx ~debug:true)
|
|
|
|
e n)
|
2021-01-14 02:17:24 +03:00
|
|
|
| EInj (e1, n, en, ts) ->
|
|
|
|
let e1' = evaluate_expr ctx e1 in
|
2021-04-03 16:07:49 +03:00
|
|
|
if is_empty_error e1' then Pos.same_pos_as (A.ELit LEmptyError) e
|
|
|
|
else Pos.same_pos_as (A.EInj (e1', n, en, ts)) e
|
2021-01-14 02:17:24 +03:00
|
|
|
| EMatch (e1, es, e_name) -> (
|
|
|
|
let e1 = evaluate_expr ctx e1 in
|
2020-12-03 22:11:41 +03:00
|
|
|
match Pos.unmark e1 with
|
2021-01-14 02:17:24 +03:00
|
|
|
| A.EInj (e1, n, e_name', _) ->
|
|
|
|
if e_name <> e_name' then
|
|
|
|
Errors.raise_multispanned_error
|
2022-03-08 15:04:27 +03:00
|
|
|
[None, Pos.get_position e; None, Pos.get_position e1]
|
2021-01-14 02:17:24 +03:00
|
|
|
"Error during match: two different enums found (should not happend \
|
|
|
|
if the term was well-typed)";
|
|
|
|
let es_n =
|
2020-12-03 22:11:41 +03:00
|
|
|
match List.nth_opt es n with
|
|
|
|
| Some es_n -> es_n
|
|
|
|
| None ->
|
2022-03-08 15:04:27 +03:00
|
|
|
Errors.raise_spanned_error (Pos.get_position e)
|
2020-12-03 22:11:41 +03:00
|
|
|
"sum type index error (should not happend if the term was \
|
|
|
|
well-typed)"
|
|
|
|
in
|
|
|
|
let new_e = Pos.same_pos_as (A.EApp (es_n, [e1])) e in
|
2021-01-14 02:17:24 +03:00
|
|
|
evaluate_expr ctx new_e
|
2020-12-09 12:36:09 +03:00
|
|
|
| A.ELit A.LEmptyError -> Pos.same_pos_as (A.ELit A.LEmptyError) e
|
2020-12-03 22:11:41 +03:00
|
|
|
| _ ->
|
2022-03-08 15:04:27 +03:00
|
|
|
Errors.raise_spanned_error (Pos.get_position e1)
|
2020-12-03 22:11:41 +03:00
|
|
|
"Expected a term having a sum type as an argument to a match (should \
|
2022-03-08 15:04:27 +03:00
|
|
|
not happend if the term was well-typed")
|
2020-12-18 17:59:15 +03:00
|
|
|
| EDefault (exceptions, just, cons) -> (
|
2021-01-14 02:17:24 +03:00
|
|
|
let exceptions = List.map (evaluate_expr ctx) exceptions in
|
2020-12-18 17:59:15 +03:00
|
|
|
let empty_count = List.length (List.filter is_empty_error exceptions) in
|
|
|
|
match List.length exceptions - empty_count with
|
2020-11-24 00:26:26 +03:00
|
|
|
| 0 -> (
|
2021-01-14 02:17:24 +03:00
|
|
|
let just = evaluate_expr ctx just in
|
|
|
|
match Pos.unmark just with
|
2021-04-03 16:07:49 +03:00
|
|
|
| ELit LEmptyError -> Pos.same_pos_as (A.ELit LEmptyError) e
|
2021-01-14 02:17:24 +03:00
|
|
|
| ELit (LBool true) -> evaluate_expr ctx cons
|
2020-12-18 17:59:15 +03:00
|
|
|
| ELit (LBool false) -> Pos.same_pos_as (A.ELit LEmptyError) e
|
2020-11-24 00:26:26 +03:00
|
|
|
| _ ->
|
2022-03-08 15:04:27 +03:00
|
|
|
Errors.raise_spanned_error (Pos.get_position e)
|
2020-12-18 17:59:15 +03:00
|
|
|
"Default justification has not been reduced to a boolean at \
|
2022-03-08 15:04:27 +03:00
|
|
|
evaluation (should not happen if the term was well-typed")
|
2020-12-18 17:59:15 +03:00
|
|
|
| 1 -> List.find (fun sub -> not (is_empty_error sub)) exceptions
|
2022-05-12 16:10:55 +03:00
|
|
|
| _ ->
|
2020-12-18 17:59:15 +03:00
|
|
|
Errors.raise_multispanned_error
|
|
|
|
(List.map
|
|
|
|
(fun except ->
|
2022-01-05 12:42:46 +03:00
|
|
|
( Some "This consequence has a valid justification:",
|
|
|
|
Pos.get_position except ))
|
2022-03-08 15:04:27 +03:00
|
|
|
(List.filter (fun sub -> not (is_empty_error sub)) exceptions))
|
2022-04-07 23:43:05 +03:00
|
|
|
"There is a conflict between multiple valid consequences for assigning \
|
2022-03-08 15:04:27 +03:00
|
|
|
the same variable.")
|
2020-11-24 00:26:26 +03:00
|
|
|
| EIfThenElse (cond, et, ef) -> (
|
2021-01-14 02:17:24 +03:00
|
|
|
match Pos.unmark (evaluate_expr ctx cond) with
|
|
|
|
| ELit (LBool true) -> evaluate_expr ctx et
|
|
|
|
| ELit (LBool false) -> evaluate_expr ctx ef
|
2021-04-03 16:07:49 +03:00
|
|
|
| ELit LEmptyError -> Pos.same_pos_as (A.ELit LEmptyError) e
|
2022-05-12 16:10:55 +03:00
|
|
|
| _ ->
|
2022-03-08 15:04:27 +03:00
|
|
|
Errors.raise_spanned_error (Pos.get_position cond)
|
2020-11-26 18:32:52 +03:00
|
|
|
"Expected a boolean literal for the result of this condition (should \
|
|
|
|
not happen if the term was well-typed)")
|
2021-04-03 16:07:49 +03:00
|
|
|
| EArray es ->
|
|
|
|
let new_es = List.map (evaluate_expr ctx) es in
|
|
|
|
if List.exists is_empty_error new_es then
|
|
|
|
Pos.same_pos_as (A.ELit LEmptyError) e
|
|
|
|
else Pos.same_pos_as (A.EArray new_es) e
|
|
|
|
| ErrorOnEmpty e' ->
|
|
|
|
let e' = evaluate_expr ctx e' in
|
|
|
|
if Pos.unmark e' = A.ELit LEmptyError then
|
2022-04-04 16:56:45 +03:00
|
|
|
Errors.raise_spanned_error (Pos.get_position e')
|
2021-04-03 16:07:49 +03:00
|
|
|
"This variable evaluated to an empty term (no rule that defined it \
|
|
|
|
applied in this situation)"
|
|
|
|
else e'
|
2020-12-10 20:11:43 +03:00
|
|
|
| EAssert e' -> (
|
2021-01-14 02:17:24 +03:00
|
|
|
match Pos.unmark (evaluate_expr ctx e') with
|
2020-12-10 20:11:43 +03:00
|
|
|
| ELit (LBool true) -> Pos.same_pos_as (Ast.ELit LUnit) e'
|
2020-12-17 22:54:38 +03:00
|
|
|
| ELit (LBool false) -> (
|
|
|
|
match Pos.unmark e' with
|
2022-05-05 15:34:29 +03:00
|
|
|
| Ast.ErrorOnEmpty
|
|
|
|
( EApp
|
2020-12-31 02:28:26 +03:00
|
|
|
( (Ast.EOp (Binop op), pos_op),
|
|
|
|
[((ELit _, _) as e1); ((ELit _, _) as e2)] ),
|
2022-05-12 16:10:55 +03:00
|
|
|
_ )
|
|
|
|
| EApp
|
2022-05-05 15:34:29 +03:00
|
|
|
( (Ast.EOp (Ast.Unop (Ast.Log _)), _),
|
2020-12-31 02:28:26 +03:00
|
|
|
[
|
2021-02-01 17:57:19 +03:00
|
|
|
( Ast.EApp
|
2022-05-05 15:34:29 +03:00
|
|
|
( (Ast.EOp (Binop op), pos_op),
|
|
|
|
[((ELit _, _) as e1); ((ELit _, _) as e2)] ),
|
2022-05-12 16:10:55 +03:00
|
|
|
_ );
|
2020-12-31 02:28:26 +03:00
|
|
|
] )
|
2022-05-12 16:10:55 +03:00
|
|
|
| EApp
|
2022-05-05 15:34:29 +03:00
|
|
|
( (Ast.EOp (Binop op), pos_op),
|
2020-12-31 02:28:26 +03:00
|
|
|
[((ELit _, _) as e1); ((ELit _, _) as e2)] ) ->
|
2022-03-08 15:04:27 +03:00
|
|
|
Errors.raise_spanned_error (Pos.get_position e')
|
|
|
|
"Assertion failed: %a %a %a"
|
|
|
|
(Print.format_expr ctx ~debug:false)
|
|
|
|
e1 Print.format_binop (op, pos_op)
|
|
|
|
(Print.format_expr ctx ~debug:false)
|
|
|
|
e2
|
2020-12-10 20:11:43 +03:00
|
|
|
| _ ->
|
2022-05-05 15:34:29 +03:00
|
|
|
Cli.debug_format "%a" (Print.format_expr ctx) e';
|
2022-03-08 15:04:27 +03:00
|
|
|
Errors.raise_spanned_error (Pos.get_position e') "Assertion failed")
|
2021-04-03 16:07:49 +03:00
|
|
|
| ELit LEmptyError -> Pos.same_pos_as (A.ELit LEmptyError) e
|
2022-05-12 16:10:55 +03:00
|
|
|
| _ ->
|
2022-03-08 15:04:27 +03:00
|
|
|
Errors.raise_spanned_error (Pos.get_position e')
|
2020-12-10 20:11:43 +03:00
|
|
|
"Expected a boolean literal for the result of this assertion (should \
|
|
|
|
not happen if the term was well-typed)")
|
2020-11-26 18:22:08 +03:00
|
|
|
|
2020-12-14 20:09:38 +03:00
|
|
|
(** {1 API} *)
|
2020-11-26 18:22:08 +03:00
|
|
|
|
2021-01-14 02:17:24 +03:00
|
|
|
let interpret_program (ctx : Ast.decl_ctx) (e : Ast.expr Pos.marked) :
|
2021-02-01 17:57:19 +03:00
|
|
|
(Uid.MarkedString.info * Ast.expr Pos.marked) list =
|
2021-01-14 02:17:24 +03:00
|
|
|
match Pos.unmark (evaluate_expr ctx e) with
|
2021-04-03 12:49:13 +03:00
|
|
|
| Ast.EAbs (_, [(Ast.TTuple (taus, Some s_in), _)]) -> (
|
2022-01-28 19:31:31 +03:00
|
|
|
let application_term = List.map (fun _ -> Ast.empty_thunked_term) taus in
|
2021-02-01 17:57:19 +03:00
|
|
|
let to_interpret =
|
|
|
|
( Ast.EApp (e, [Ast.ETuple (application_term, Some s_in), Pos.no_pos]),
|
|
|
|
Pos.no_pos )
|
2022-05-12 16:10:55 +03:00
|
|
|
in
|
2021-01-14 02:17:24 +03:00
|
|
|
match Pos.unmark (evaluate_expr ctx to_interpret) with
|
2021-02-01 17:57:19 +03:00
|
|
|
| Ast.ETuple (args, Some s_out) ->
|
|
|
|
let s_out_fields =
|
2022-05-12 16:10:55 +03:00
|
|
|
List.map
|
2021-02-01 17:57:19 +03:00
|
|
|
(fun (f, _) -> Ast.StructFieldName.get_info f)
|
|
|
|
(Ast.StructMap.find s_out ctx.ctx_structs)
|
|
|
|
in
|
|
|
|
List.map2 (fun arg var -> var, arg) args s_out_fields
|
2020-11-26 18:22:08 +03:00
|
|
|
| _ ->
|
2022-03-08 15:04:27 +03:00
|
|
|
Errors.raise_spanned_error (Pos.get_position e)
|
2021-01-29 18:32:04 +03:00
|
|
|
"The interpretation of a program should always yield a struct \
|
|
|
|
corresponding to the scope variables")
|
2022-05-12 16:10:55 +03:00
|
|
|
| _ ->
|
2022-03-08 15:04:27 +03:00
|
|
|
Errors.raise_spanned_error (Pos.get_position e)
|
2020-11-26 18:22:08 +03:00
|
|
|
"The interpreter can only interpret terms starting with functions having \
|
|
|
|
thunked arguments"
|