found a bug inside the match translation.

This commit is contained in:
Alain 2021-11-22 15:49:02 +01:00
parent f75341c44f
commit 08b38472e2
3 changed files with 15 additions and 2 deletions

View File

@ -26,6 +26,7 @@ type lit =
type except = ConflictError | EmptyError | NoValueProvided | Crash type except = ConflictError | EmptyError | NoValueProvided | Crash
type expr = type expr =
| EVar of expr Bindlib.var Pos.marked | EVar of expr Bindlib.var Pos.marked
| ETuple of expr Pos.marked list * D.StructName.t option | ETuple of expr Pos.marked list * D.StructName.t option
@ -118,6 +119,8 @@ let make_letopt_in
(e2: expr Pos.marked Bindlib.box) (e2: expr Pos.marked Bindlib.box)
: expr Pos.marked Bindlib.box = : expr Pos.marked Bindlib.box =
(* let%opt x: tau = e1 in e2 == matchopt e1 with | None -> None | Some x -> e2 *)
let pos = Pos.get_position (Bindlib.unbox e2) in let pos = Pos.get_position (Bindlib.unbox e2) in
let+ e2 = make_abs let+ e2 = make_abs

View File

@ -106,7 +106,16 @@ and translate_expr (ctx : ctx) (e : D.expr Pos.marked) : A.expr Pos.marked Bindl
let e2 = let e2 =
let+ e1 = Bindlib.box (A.EVar (x, pos)) let+ e1 = Bindlib.box (A.EVar (x, pos))
and+ cases = Bindlib.box_list (List.map (translate_expr ctx) cases) in (* there is an issue here. *)
and+ cases = cases
|> List.map (fun e' -> translate_expr ctx e')
|> List.map (function
| A.ESome e'' -> e''
| _ -> assert false
)
|> assert false
|> Bindlib.box_list
in
same_pos @@ A.EMatch ((e1, pos), cases, en) same_pos @@ A.EMatch ((e1, pos), cases, en)
in in

View File

@ -108,6 +108,7 @@ let avoid_keywords (s : string) : string =
| "object" | "of" | "open" | "or" | "private" | "rec" | "sig" | "struct" | "then" | "to" | "object" | "of" | "open" | "or" | "private" | "rec" | "sig" | "struct" | "then" | "to"
| "true" | "try" | "type" | "val" | "virtual" | "when" | "while" | "with" -> | "true" | "try" | "type" | "val" | "virtual" | "when" | "while" | "with" ->
true true
| "x" -> true (* i need a variable to make the translation *)
| _ -> false | _ -> false
then s ^ "_" then s ^ "_"
else s else s
@ -331,7 +332,7 @@ let rec format_expr (ctx : Dcalc.Ast.decl_ctx) (fmt : Format.formatter) (e : exp
Format.fprintf fmt "@[<hov 2> Some@ %a@ @]" format_with_parens e1 Format.fprintf fmt "@[<hov 2> Some@ %a@ @]" format_with_parens e1
| ENone -> Format.fprintf fmt "None@" | ENone -> Format.fprintf fmt "None@"
| EMatchopt (e1, e2, e3) -> | EMatchopt (e1, e2, e3) ->
let x = assert false in let x = Ast.Var.make ("x", Pos.no_pos) in
Format.fprintf fmt "@[<hov 2>match@ %a@]@ with@\n| None ->@[<hov 2>@ %a@]@\n| Some %a ->@[<hov 2>@ %a@ %a@]" format_expr e1 format_with_parens e2 format_var x format_with_parens e3 format_var x Format.fprintf fmt "@[<hov 2>match@ %a@]@ with@\n| None ->@[<hov 2>@ %a@]@\n| Some %a ->@[<hov 2>@ %a@ %a@]" format_expr e1 format_with_parens e2 format_var x format_with_parens e3 format_var x
let format_struct_embedding (fmt : Format.formatter) let format_struct_embedding (fmt : Format.formatter)