Formatting

This commit is contained in:
Denis Merigoux 2021-03-19 16:27:23 +01:00
parent c4fc0ff622
commit 71085ba3da
6 changed files with 258 additions and 254 deletions

View File

@ -36,9 +36,9 @@ let rec type_eq (t1 : A.typ Pos.marked) (t2 : A.typ Pos.marked) : bool =
match (Pos.unmark t1, Pos.unmark t2) with
| A.TLit tl1, A.TLit tl2 -> tl1 = tl2
| A.TTuple (ts1, s1), A.TTuple (ts2, s2) -> (
try s1 == s2 && List.for_all2 type_eq ts1 ts2 with Invalid_argument _ -> false)
try s1 == s2 && List.for_all2 type_eq ts1 ts2 with Invalid_argument _ -> false )
| A.TEnum (ts1, e1), A.TEnum (ts2, e2) -> (
try e1 == e2 && List.for_all2 type_eq ts1 ts2 with Invalid_argument _ -> false)
try e1 == e2 && List.for_all2 type_eq ts1 ts2 with Invalid_argument _ -> false )
| A.TArray t1, A.TArray t2 -> type_eq t1 t2
| A.TArrow (t11, t12), A.TArrow (t21, t22) -> type_eq t11 t12 && type_eq t21 t22
| _, _ -> false
@ -50,7 +50,7 @@ let log_indent = ref 0
let rec evaluate_operator (ctx : Ast.decl_ctx) (op : A.operator Pos.marked)
(args : A.expr Pos.marked list) : A.expr Pos.marked =
Pos.same_pos_as
(match (Pos.unmark op, List.map Pos.unmark args) with
( match (Pos.unmark op, List.map Pos.unmark args) with
| A.Ternop A.Fold, [ _f; _init; EArray es ] ->
Pos.unmark
(List.fold_left
@ -81,7 +81,7 @@ let rec evaluate_operator (ctx : Ast.decl_ctx) (op : A.operator Pos.marked)
[
(Some "The division operator:", Pos.get_position op);
(Some "The null denominator:", Pos.get_position (List.nth args 2));
])
] )
| A.Binop (A.Add KMoney), [ ELit (LMoney i1); ELit (LMoney i2) ] ->
A.ELit (LMoney Runtime.(i1 +$ i2))
| A.Binop (A.Sub KMoney), [ ELit (LMoney i1); ELit (LMoney i2) ] ->
@ -95,7 +95,7 @@ let rec evaluate_operator (ctx : Ast.decl_ctx) (op : A.operator Pos.marked)
[
(Some "The division operator:", Pos.get_position op);
(Some "The null denominator:", Pos.get_position (List.nth args 2));
])
] )
| A.Binop (A.Add KDuration), [ ELit (LDuration i1); ELit (LDuration i2) ] ->
A.ELit (LDuration Runtime.(i1 +^ i2))
| A.Binop (A.Sub KDuration), [ ELit (LDuration i1); ELit (LDuration i2) ] ->
@ -127,7 +127,7 @@ let rec evaluate_operator (ctx : Ast.decl_ctx) (op : A.operator Pos.marked)
"Cannot compare together durations that cannot be converted to a precise number of days"
[
(None, Pos.get_position (List.nth args 0)); (None, Pos.get_position (List.nth args 1));
])
] )
| A.Binop (A.Lte KDuration), [ ELit (LDuration i1); ELit (LDuration i2) ] -> (
try A.ELit (LBool Runtime.(i1 <=^ i2))
with _ ->
@ -135,7 +135,7 @@ let rec evaluate_operator (ctx : Ast.decl_ctx) (op : A.operator Pos.marked)
"Cannot compare together durations that cannot be converted to a precise number of days"
[
(None, Pos.get_position (List.nth args 0)); (None, Pos.get_position (List.nth args 1));
])
] )
| A.Binop (A.Gt KDuration), [ ELit (LDuration i1); ELit (LDuration i2) ] -> (
try A.ELit (LBool Runtime.(i1 >^ i2))
with _ ->
@ -143,7 +143,7 @@ let rec evaluate_operator (ctx : Ast.decl_ctx) (op : A.operator Pos.marked)
"Cannot compare together durations that cannot be converted to a precise number of days"
[
(None, Pos.get_position (List.nth args 0)); (None, Pos.get_position (List.nth args 1));
])
] )
| A.Binop (A.Gte KDuration), [ ELit (LDuration i1); ELit (LDuration i2) ] -> (
try A.ELit (LBool Runtime.(i1 >=^ i2))
with _ ->
@ -151,7 +151,7 @@ let rec evaluate_operator (ctx : Ast.decl_ctx) (op : A.operator Pos.marked)
"Cannot compare together durations that cannot be converted to a precise number of days"
[
(None, Pos.get_position (List.nth args 0)); (None, Pos.get_position (List.nth args 1));
])
] )
| A.Binop (A.Lt KDate), [ ELit (LDate i1); ELit (LDate i2) ] ->
A.ELit (LBool Runtime.(i1 <@ i2))
| A.Binop (A.Lte KDate), [ ELit (LDate i1); ELit (LDate i2) ] ->
@ -171,44 +171,44 @@ let rec evaluate_operator (ctx : Ast.decl_ctx) (op : A.operator Pos.marked)
| A.Binop A.Eq, [ EArray es1; EArray es2 ] ->
A.ELit
(LBool
(try
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 *))
es1 es2
with Invalid_argument _ -> false))
( try
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 *))
es1 es2
with Invalid_argument _ -> false ))
| A.Binop A.Eq, [ ETuple (es1, s1); ETuple (es2, s2) ] ->
A.ELit
(LBool
(try
s1 = s2
&& 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 *))
es1 es2
with Invalid_argument _ -> false))
( try
s1 = s2
&& 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 *))
es1 es2
with Invalid_argument _ -> false ))
| A.Binop A.Eq, [ EInj (e1, i1, en1, ts1); EInj (e2, i2, en2, ts2) ] ->
A.ELit
(LBool
(try
en1 = en2 && List.for_all2 type_eq ts1 ts2 && i1 = i2
&&
match Pos.unmark (evaluate_operator ctx op [ e1; e2 ]) with
| A.ELit (LBool b) -> b
| _ -> assert false
(* should not happen *)
with Invalid_argument _ -> false))
( try
en1 = en2 && List.for_all2 type_eq ts1 ts2 && i1 = i2
&&
match Pos.unmark (evaluate_operator ctx op [ e1; e2 ]) with
| A.ELit (LBool b) -> b
| _ -> assert false
(* should not happen *)
with Invalid_argument _ -> false ))
| A.Binop A.Eq, [ _; _ ] -> A.ELit (LBool false) (* comparing anything else return false *)
| A.Binop A.Neq, [ _; _ ] -> (
match Pos.unmark (evaluate_operator ctx (Pos.same_pos_as (A.Binop A.Eq) op) args) with
| A.ELit (A.LBool b) -> A.ELit (A.LBool (not b))
| _ -> assert false (*should not happen *))
| _ -> assert false (*should not happen *) )
| A.Binop A.Map, [ _; A.EArray es ] ->
A.EArray
(List.map
@ -252,7 +252,7 @@ let rec evaluate_operator (ctx : Ast.decl_ctx) (op : A.operator Pos.marked)
Cli.log_print
(Format.asprintf "%*s%a %a: %s" (!log_indent * 2) "" Print.format_log_entry entry
Print.format_uid_list infos
(match e' with
( match e' with
| Ast.EAbs _ -> Cli.print_with_style [ ANSITerminal.green ] "<function>"
| _ ->
let expr_str =
@ -263,7 +263,7 @@ let rec evaluate_operator (ctx : Ast.decl_ctx) (op : A.operator Pos.marked)
~subst:(fun _ -> " ")
expr_str
in
Cli.print_with_style [ ANSITerminal.green ] "%s" expr_str))
Cli.print_with_style [ ANSITerminal.green ] "%s" expr_str ))
| PosRecordIfTrueBool -> (
let pos = Pos.get_position op in
match (pos <> Pos.no_pos, e') with
@ -274,7 +274,7 @@ let rec evaluate_operator (ctx : Ast.decl_ctx) (op : A.operator Pos.marked)
(Cli.print_with_style [ ANSITerminal.green ] "Definition applied")
(Cli.add_prefix_to_each_line (Pos.retrieve_loc_text pos) (fun _ ->
Format.asprintf "%*s" (!log_indent * 2) "")))
| _ -> ())
| _ -> () )
| BeginCall ->
Cli.log_print
(Format.asprintf "%*s%a %a" (!log_indent * 2) "" Print.format_log_entry entry
@ -284,20 +284,20 @@ let rec evaluate_operator (ctx : Ast.decl_ctx) (op : A.operator Pos.marked)
log_indent := !log_indent - 1;
Cli.log_print
(Format.asprintf "%*s%a %a" (!log_indent * 2) "" Print.format_log_entry entry
Print.format_uid_list infos))
Print.format_uid_list infos) )
else ();
e'
| A.Unop _, [ ELit LEmptyError ] -> A.ELit LEmptyError
| _ ->
Errors.raise_multispanned_error
"Operator applied to the wrong arguments\n(should nothappen if the term was well-typed)"
([ (Some "Operator:", Pos.get_position op) ]
( [ (Some "Operator:", Pos.get_position op) ]
@ List.mapi
(fun i arg ->
( Some
(Format.asprintf "Argument n°%d, value %a" (i + 1) (Print.format_expr ctx) arg),
Pos.get_position arg ))
args))
args ) )
op
and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) : A.expr Pos.marked =
@ -325,21 +325,21 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) : A.expr Pos.mark
Errors.raise_spanned_error
"function has not been reduced to a lambda at evaluation (should not happen if the \
term was well-typed"
(Pos.get_position e))
(Pos.get_position e) )
| EAbs _ | ELit _ | EOp _ -> e (* thse are values *)
| ETuple (es, s) -> Pos.same_pos_as (A.ETuple (List.map (evaluate_expr ctx) es, s)) e
| ETupleAccess (e1, n, s, _) -> (
let e1 = evaluate_expr ctx e1 in
match Pos.unmark e1 with
| ETuple (es, s') -> (
(match (s, s') with
( match (s, s') with
| None, None -> ()
| Some s, Some s' when s = s' -> ()
| _ ->
Errors.raise_multispanned_error
"Error during tuple access: not the same structs (should not happen if the term \
was well-typed)"
[ (None, Pos.get_position e); (None, Pos.get_position e1) ]);
[ (None, Pos.get_position e); (None, Pos.get_position e1) ] );
match List.nth_opt es n with
| Some e' -> e'
| None ->
@ -348,14 +348,14 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) : A.expr Pos.mark
"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)
(Pos.get_position e1))
(Pos.get_position e1) )
| _ ->
Errors.raise_spanned_error
(Format.asprintf
"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) e n)
(Pos.get_position e1))
(Pos.get_position e1) )
| EInj (e1, n, en, ts) ->
let e1' = evaluate_expr ctx e1 in
Pos.same_pos_as (A.EInj (e1', n, en, ts)) e
@ -383,7 +383,7 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) : A.expr Pos.mark
Errors.raise_spanned_error
"Expected a term having a sum type as an argument to a match (should not happend if \
the term was well-typed"
(Pos.get_position e1))
(Pos.get_position e1) )
| EDefault (exceptions, just, cons) -> (
let exceptions_orig = exceptions in
let exceptions = List.map (evaluate_expr ctx) exceptions in
@ -399,7 +399,7 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) : A.expr Pos.mark
Errors.raise_spanned_error
"Default justification has not been reduced to a boolean at evaluation (should not \
happen if the term was well-typed"
(Pos.get_position e))
(Pos.get_position e) )
| 1 -> List.find (fun sub -> not (is_empty_error sub)) exceptions
| _ ->
Errors.raise_multispanned_error
@ -408,7 +408,7 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) : A.expr Pos.mark
(fun (_, except) -> (Some "This justification is true:", Pos.get_position except))
(List.filter
(fun (sub, _) -> not (is_empty_error sub))
(List.map2 (fun x y -> (x, y)) exceptions exceptions_orig))))
(List.map2 (fun x y -> (x, y)) exceptions exceptions_orig))) )
| EIfThenElse (cond, et, ef) -> (
match Pos.unmark (evaluate_expr ctx cond) with
| ELit (LBool true) -> evaluate_expr ctx et
@ -417,7 +417,7 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) : A.expr Pos.mark
Errors.raise_spanned_error
"Expected a boolean literal for the result of this condition (should not happen if the \
term was well-typed)"
(Pos.get_position cond))
(Pos.get_position cond) )
| EArray es -> Pos.same_pos_as (A.EArray (List.map (evaluate_expr ctx) es)) e
| EAssert e' -> (
match Pos.unmark (evaluate_expr ctx e') with
@ -430,12 +430,13 @@ and evaluate_expr (ctx : Ast.decl_ctx) (e : A.expr Pos.marked) : A.expr Pos.mark
Print.format_binop (op, pos_op) (Print.format_expr ctx) e2)
(Pos.get_position e')
| _ ->
Errors.raise_spanned_error (Format.asprintf "Assertion failed") (Pos.get_position e'))
Errors.raise_spanned_error (Format.asprintf "Assertion failed") (Pos.get_position e')
)
| _ ->
Errors.raise_spanned_error
"Expected a boolean literal for the result of this assertion (should not happen if the \
term was well-typed)"
(Pos.get_position e'))
(Pos.get_position e') )
(** {1 API} *)
@ -459,7 +460,7 @@ let interpret_program (ctx : Ast.decl_ctx) (e : Ast.expr Pos.marked) :
Errors.raise_spanned_error
"The interpretation of a program should always yield a struct corresponding to the \
scope variables"
(Pos.get_position e))
(Pos.get_position e) )
| _ ->
Errors.raise_spanned_error
"The interpreter can only interpret terms starting with functions having thunked arguments"

View File

@ -98,7 +98,7 @@ let format_lit (fmt : Format.formatter) (l : lit Pos.marked) : unit =
| LMoney e -> (
match !Utils.Cli.locale_lang with
| `En -> Format.fprintf fmt "$%s" (Runtime.money_to_string e)
| `Fr -> Format.fprintf fmt "%s €" (Runtime.money_to_string e))
| `Fr -> Format.fprintf fmt "%s €" (Runtime.money_to_string e) )
| LDate d -> Format.fprintf fmt "%s" (Runtime.date_to_string d)
| LDuration d -> Format.fprintf fmt "%s" (Runtime.duration_to_string d)
@ -137,7 +137,7 @@ let format_log_entry (fmt : Format.formatter) (entry : log_entry) : unit =
let format_unop (fmt : Format.formatter) (op : unop Pos.marked) : unit =
Format.fprintf fmt "%s"
(match Pos.unmark op with
( match Pos.unmark op with
| Minus _ -> "-"
| Not -> "~"
| ErrorOnEmpty -> "error_empty"
@ -151,7 +151,7 @@ let format_unop (fmt : Format.formatter) (op : unop Pos.marked) : unit =
| IntToRat -> "int_to_rat"
| GetDay -> "get_day"
| GetMonth -> "get_month"
| GetYear -> "get_year")
| GetYear -> "get_year" )
let needs_parens (e : expr Pos.marked) : bool =
match Pos.unmark e with EAbs _ | ETuple (_, Some _) -> true | _ -> false
@ -197,7 +197,7 @@ let rec format_expr (ctx : Ast.decl_ctx) (fmt : Format.formatter) (e : expr Pos.
Format.fprintf fmt "%a%a%a%a%a" format_expr e1 format_punctuation "." format_punctuation
"\"" Ast.StructFieldName.format_t
(fst (List.nth (Ast.StructMap.find s ctx.ctx_structs) n))
format_punctuation "\"")
format_punctuation "\"" )
| EInj (e, n, en, _ts) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" Ast.EnumConstructor.format_t
(fst (List.nth (Ast.EnumMap.find en ctx.ctx_enums) n))

View File

@ -222,7 +222,7 @@ let rec typecheck_expr_bottom_up (ctx : Ast.decl_ctx) (env : env) (e : A.expr Po
| Some t -> t
| None ->
Errors.raise_spanned_error "Variable not found in the current context"
(Pos.get_position e))
(Pos.get_position e) )
| ELit (LBool _) -> UnionFind.make (Pos.same_pos_as (TLit TBool) e)
| ELit (LInt _) -> UnionFind.make (Pos.same_pos_as (TLit TInt) e)
| ELit (LRat _) -> UnionFind.make (Pos.same_pos_as (TLit TRat) e)
@ -246,7 +246,7 @@ let rec typecheck_expr_bottom_up (ctx : Ast.decl_ctx) (env : env) (e : A.expr Po
(Format.asprintf
"Expression should have a tuple type with at least %d elements but only has %d" n
(List.length typs))
(Pos.get_position e1))
(Pos.get_position e1) )
| EInj (e1, n, e_name, ts) ->
let ts = List.map (fun t -> UnionFind.make (Pos.map_under_mark ast_to_typ t)) ts in
let ts_n =
@ -350,7 +350,7 @@ and typecheck_expr_top_down (ctx : Ast.decl_ctx) (env : env) (e : A.expr Pos.mar
| Some tau' -> ignore (unify ctx tau tau')
| None ->
Errors.raise_spanned_error "Variable not found in the current context"
(Pos.get_position e))
(Pos.get_position e) )
| ELit (LBool _) -> unify ctx tau (UnionFind.make (Pos.same_pos_as (TLit TBool) e))
| ELit (LInt _) -> unify ctx tau (UnionFind.make (Pos.same_pos_as (TLit TInt) e))
| ELit (LRat _) -> unify ctx tau (UnionFind.make (Pos.same_pos_as (TLit TRat) e))
@ -375,7 +375,7 @@ and typecheck_expr_top_down (ctx : Ast.decl_ctx) (env : env) (e : A.expr Pos.mar
(Format.asprintf
"Expression should have a tuple type with at least %d elements but only has %d" n
(List.length typs))
(Pos.get_position e1))
(Pos.get_position e1) )
| EInj (e1, n, e_name, ts) ->
let ts = List.map (fun t -> UnionFind.make (Pos.map_under_mark ast_to_typ t)) ts in
let ts_n =

View File

@ -245,7 +245,7 @@ let rec format_expr (ctx : Dcalc.Ast.decl_ctx) (fmt : Format.formatter) (e : exp
format_with_parens e1
| Some s ->
Format.fprintf fmt "%a.%a" format_with_parens e1 format_struct_field_name
(fst (List.nth (Dcalc.Ast.StructMap.find s ctx.ctx_structs) n)))
(fst (List.nth (Dcalc.Ast.StructMap.find s ctx.ctx_structs) n)) )
| EInj (e, n, en, _ts) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" format_enum_cons_name
(fst (List.nth (Dcalc.Ast.EnumMap.find en ctx.ctx_enums) n))

View File

@ -102,7 +102,7 @@ let disambiguate_constructor (ctxt : Name_resolution.context)
with Not_found ->
Errors.raise_spanned_error
(Format.asprintf "Enum %s has not been defined before" (Pos.unmark enum))
(Pos.get_position enum))
(Pos.get_position enum) )
(** Usage: [translate_expr scope ctxt expr]
@ -180,9 +180,9 @@ let rec translate_expr (scope : Scopelang.Ast.ScopeName.t) (ctxt : Name_resoluti
Scopelang.Ast.ELit
(Dcalc.Ast.LRat
Runtime.(
(decimal_of_integer i
( decimal_of_integer i
+& decimal_of_integer f
/& decimal_of_integer (integer_exponentiation (integer_of_int 10) digits_f))
/& decimal_of_integer (integer_exponentiation (integer_of_int 10) digits_f) )
/& decimal_of_string "100"))
| LBool b -> Scopelang.Ast.ELit (Dcalc.Ast.LBool b)
| LMoneyAmount i ->
@ -212,12 +212,12 @@ let rec translate_expr (scope : Scopelang.Ast.ScopeName.t) (ctxt : Name_resoluti
(Pos.get_position date.literal_date_day);
Scopelang.Ast.ELit
(Dcalc.Ast.LDate
(try
Runtime.date_of_numbers
(Pos.unmark date.literal_date_year)
(Pos.unmark date.literal_date_month)
(Pos.unmark date.literal_date_day)
with Runtime.ImpossibleDate -> Errors.raise_spanned_error "Invalid date" pos))
( try
Runtime.date_of_numbers
(Pos.unmark date.literal_date_year)
(Pos.unmark date.literal_date_month)
(Pos.unmark date.literal_date_day)
with Runtime.ImpossibleDate -> Errors.raise_spanned_error "Invalid date" pos ))
in
Bindlib.box (untyped_term, pos)
| Ident x -> (
@ -289,7 +289,7 @@ let rec translate_expr (scope : Scopelang.Ast.ScopeName.t) (ctxt : Name_resoluti
with Not_found ->
Errors.raise_spanned_error
(Format.asprintf "Struct %s has not been defined before" (Pos.unmark c_name))
(Pos.get_position c_name))))
(Pos.get_position c_name) ) ) )
| FunCall (f, arg) ->
Bindlib.box_apply2
(fun f arg -> (Scopelang.Ast.EApp (f, [ arg ]), pos))
@ -314,13 +314,14 @@ let rec translate_expr (scope : Scopelang.Ast.ScopeName.t) (ctxt : Name_resoluti
(Pos.unmark s_name))
(Pos.get_position f_name)
in
(match Scopelang.Ast.StructFieldMap.find_opt f_uid s_fields with
( match Scopelang.Ast.StructFieldMap.find_opt f_uid s_fields with
| None -> ()
| Some e_field ->
Errors.raise_multispanned_error
(Format.asprintf "The field %a has been defined twice:"
Scopelang.Ast.StructFieldName.format_t f_uid)
[ (None, Pos.get_position f_e); (None, Pos.get_position (Bindlib.unbox e_field)) ]);
[ (None, Pos.get_position f_e); (None, Pos.get_position (Bindlib.unbox e_field)) ]
);
let f_e = translate_expr scope ctxt f_e in
Scopelang.Ast.StructFieldMap.add f_uid f_e s_fields)
Scopelang.Ast.StructFieldMap.empty fields
@ -358,9 +359,10 @@ let rec translate_expr (scope : Scopelang.Ast.ScopeName.t) (ctxt : Name_resoluti
Bindlib.box_apply
(fun payload ->
( Scopelang.Ast.EEnumInj
( (match payload with
( ( match payload with
| Some e' -> e'
| None -> (Scopelang.Ast.ELit Dcalc.Ast.LUnit, Pos.get_position constructor)),
| None -> (Scopelang.Ast.ELit Dcalc.Ast.LUnit, Pos.get_position constructor)
),
c_uid,
e_uid ),
pos ))
@ -375,9 +377,10 @@ let rec translate_expr (scope : Scopelang.Ast.ScopeName.t) (ctxt : Name_resoluti
Bindlib.box_apply
(fun payload ->
( Scopelang.Ast.EEnumInj
( (match payload with
( ( match payload with
| Some e' -> e'
| None -> (Scopelang.Ast.ELit Dcalc.Ast.LUnit, Pos.get_position constructor)),
| None -> (Scopelang.Ast.ELit Dcalc.Ast.LUnit, Pos.get_position constructor)
),
c_uid,
e_uid ),
pos ))
@ -390,7 +393,7 @@ let rec translate_expr (scope : Scopelang.Ast.ScopeName.t) (ctxt : Name_resoluti
with Not_found ->
Errors.raise_spanned_error
(Format.asprintf "Enum %s has not been defined before" (Pos.unmark enum))
(Pos.get_position enum)))
(Pos.get_position enum) ) )
| MatchWith (e1, (cases, _cases_pos)) ->
let e1 = translate_expr scope ctxt e1 in
let cases_d, e_uid = disambiguate_match_and_build_expression scope ctxt cases in
@ -399,12 +402,12 @@ let rec translate_expr (scope : Scopelang.Ast.ScopeName.t) (ctxt : Name_resoluti
e1
(LiftEnumConstructorMap.lift_box cases_d)
| TestMatchCase (e1, pattern) ->
(match snd (Pos.unmark pattern) with
( match snd (Pos.unmark pattern) with
| None -> ()
| Some binding ->
Errors.print_spanned_warning
"This binding will be ignored (remove it to suppress warning)"
(Pos.get_position binding));
(Pos.get_position binding) );
let enum_uid, c_uid =
disambiguate_constructor ctxt (fst (Pos.unmark pattern)) (Pos.get_position pattern)
in
@ -440,10 +443,10 @@ let rec translate_expr (scope : Scopelang.Ast.ScopeName.t) (ctxt : Name_resoluti
(fun f_pred collection ->
( Scopelang.Ast.EApp
( ( Scopelang.Ast.EOp
(match op' with
( match op' with
| Ast.Map -> Dcalc.Ast.Binop Dcalc.Ast.Map
| Ast.Filter -> Dcalc.Ast.Binop Dcalc.Ast.Filter
| _ -> assert false (* should not happen *)),
| _ -> assert false (* should not happen *) ),
pos ),
[ f_pred; collection ] ),
pos ))
@ -739,7 +742,7 @@ and disambiguate_match_and_build_expression (scope : Scopelang.Ast.ScopeName.t)
Scopelang.Ast.EnumName.format_t e_uid Scopelang.Ast.EnumName.format_t e_uid')
(Pos.get_position case.Ast.match_case_pattern)
in
(match Scopelang.Ast.EnumConstructorMap.find_opt c_uid cases_d with
( match Scopelang.Ast.EnumConstructorMap.find_opt c_uid cases_d with
| None -> ()
| Some e_case ->
Errors.raise_multispanned_error
@ -748,7 +751,7 @@ and disambiguate_match_and_build_expression (scope : Scopelang.Ast.ScopeName.t)
[
(None, Pos.get_position case.match_case_expr);
(None, Pos.get_position (Bindlib.unbox e_case));
]);
] );
let ctxt, (param_var, param_pos) =
match binding with
| None -> (ctxt, (Scopelang.Ast.Var.make ("_", Pos.no_pos), Pos.no_pos))
@ -865,12 +868,12 @@ let process_def (precond : Scopelang.Ast.expr Pos.marked Bindlib.box option)
| Some x -> x
| None ->
Desugared.Ast.RuleName.fresh
(match def.definition_label with
( match def.definition_label with
| None ->
Pos.map_under_mark
(fun qident -> String.concat "." (List.map (fun i -> Pos.unmark i) qident))
def.definition_name
| Some label -> label)
| Some label -> label )
in
let is_exception (def : Ast.definition) =
match def.Ast.definition_exception_to with NotAnException -> false | _ -> true
@ -889,20 +892,20 @@ let process_def (precond : Scopelang.Ast.expr Pos.marked Bindlib.box option)
| NotAnException -> None
| UnlabeledException ->
Some
(match Desugared.Ast.ScopeDefMap.find_opt def_key scope_ctxt.default_rulemap with
( match Desugared.Ast.ScopeDefMap.find_opt def_key scope_ctxt.default_rulemap with
(* This should have been caught previously by check_unlabeled_exception *)
| None | Some Name_resolution.Ambiguous -> assert false
| Some (Name_resolution.Unique name) -> Pos.same_pos_as name def.Ast.definition_name)
| Some (Name_resolution.Unique name) -> Pos.same_pos_as name def.Ast.definition_name )
| ExceptionToLabel label ->
Some
(try
Pos.same_pos_as
(Desugared.Ast.IdentMap.find (Pos.unmark label) scope_ctxt.label_idmap)
label
with Not_found ->
Errors.raise_spanned_error
(Format.asprintf "Unknown label: \"%s\"" (Pos.unmark label))
(Pos.get_position label))
( try
Pos.same_pos_as
(Desugared.Ast.IdentMap.find (Pos.unmark label) scope_ctxt.label_idmap)
label
with Not_found ->
Errors.raise_spanned_error
(Format.asprintf "Unknown label: \"%s\"" (Pos.unmark label))
(Pos.get_position label) )
in
let x_def =
Desugared.Ast.RuleMap.add rule_name
@ -947,12 +950,12 @@ let process_assert (precond : Scopelang.Ast.expr Pos.marked Bindlib.box option)
let scope : Desugared.Ast.scope = Scopelang.Ast.ScopeMap.find scope_uid prgm.program_scopes in
let ass =
translate_expr scope_uid ctxt
(match ass.Ast.assertion_condition with
( match ass.Ast.assertion_condition with
| None -> ass.Ast.assertion_content
| Some cond ->
( Ast.IfThenElse
(cond, ass.Ast.assertion_content, Pos.same_pos_as (Ast.Literal (Ast.LBool true)) cond),
Pos.get_position cond ))
Pos.get_position cond ) )
in
let ass =
match precond with
@ -1003,7 +1006,7 @@ let check_unlabeled_exception (scope : Scopelang.Ast.ScopeName.t) (ctxt : Name_r
Errors.raise_spanned_error
"This exception can refer to several definitions. Try using labels to disambiguate"
(Pos.get_position item)
| Some (Unique _) -> ()))
| Some (Unique _) -> () ) )
| Ast.Definition def -> (
match def.definition_exception_to with
| Ast.NotAnException | Ast.ExceptionToLabel _ -> ()
@ -1021,7 +1024,7 @@ let check_unlabeled_exception (scope : Scopelang.Ast.ScopeName.t) (ctxt : Name_r
Errors.raise_spanned_error
"This exception can refer to several definitions. Try using labels to disambiguate"
(Pos.get_position item)
| Some (Unique _) -> ()))
| Some (Unique _) -> () ) )
| _ -> ()
(** Translates a surface scope use, which is a bunch of definitions *)

File diff suppressed because it is too large Load Diff