should be ok, without handling the types

This commit is contained in:
Alain 2021-11-22 15:49:39 +01:00
parent 0f5fde2c5a
commit 53b40121ad

View File

@ -40,7 +40,7 @@ let rec translate_default (ctx : ctx) (exceptions : D.expr Pos.marked list)
(just : D.expr Pos.marked) (cons : D.expr Pos.marked) (pos_default : Pos.t) :
A.expr Pos.marked Bindlib.box =
let exceptions =
List.map (fun except -> thunk_expr (translate_expr ctx except) pos_default) exceptions
List.map (fun except -> translate_expr ctx except) exceptions
in
let exceptions =
A.make_app
@ -61,6 +61,8 @@ and translate_typ (t: D.typ Pos.marked) : D.typ Pos.marked =
let _ = t in assert false
and translate_expr (ctx : ctx) (e : D.expr Pos.marked) : A.expr Pos.marked Bindlib.box =
let same_pos e' = Pos.same_pos_as e' e in
match Pos.unmark e with
| D.EVar v -> D.VarMap.find (Pos.unmark v) ctx
| D.ETuple (args, s) ->
@ -72,47 +74,108 @@ and translate_expr (ctx : ctx) (e : D.expr Pos.marked) : A.expr Pos.marked Bindl
let pos = Pos.get_position(Bindlib.unbox e1) in
let x = A.Var.make ("e1", pos) in
let tau = assert false in
let tau = failwith "todo" in
let e2 =
let+ e1 = Bindlib.box (A.EVar (x, pos)) in
(A.ETupleAccess ((e1, pos), i, s, ts), pos) in
same_pos @@ A.ETupleAccess ((e1, pos), i, s, ts)
in
A.make_letopt_in x tau e1 e2
| D.EInj (e1, i, en, ts) ->
Bindlib.box_apply
(fun e1 -> Pos.same_pos_as (A.EInj (e1, i, en, ts)) e)
(translate_expr ctx e1)
let e1 = translate_expr ctx e1 in
let pos = Pos.get_position(Bindlib.unbox e1) in
let x = A.Var.make ("e1", pos) in
let tau = failwith "todo" in
let e2 =
let+ e1 = Bindlib.box (A.EVar (x, pos)) in
same_pos @@ A.EInj ((e1, pos), i, en, ts)
in
A.make_letopt_in x tau e1 e2
| D.EMatch (e1, cases, en) ->
Bindlib.box_apply2
(fun e1 cases -> Pos.same_pos_as (A.EMatch (e1, cases, en)) e)
(translate_expr ctx e1)
(Bindlib.box_list (List.map (translate_expr ctx) cases))
let e1 = translate_expr ctx e1 in
let pos = Pos.get_position(Bindlib.unbox e1) in
let x = A.Var.make ("e1", pos) in
let tau = failwith "todo" in
let e2 =
let+ e1 = Bindlib.box (A.EVar (x, pos))
and+ cases = Bindlib.box_list (List.map (translate_expr ctx) cases) in
same_pos @@ A.EMatch ((e1, pos), cases, en)
in
A.make_letopt_in x tau e1 e2
| D.EArray es ->
Bindlib.box_apply
(fun es -> Pos.same_pos_as (A.EArray es) e)
(fun es -> same_pos @@ A.ESome (same_pos @@ (A.EArray es) ))
(Bindlib.box_list (List.map (translate_expr ctx) es))
| D.ELit l -> Bindlib.box (Pos.same_pos_as (translate_lit l) e)
| D.EOp op -> Bindlib.box (Pos.same_pos_as (A.EOp op) e)
| D.ELit l -> Bindlib.box @@ same_pos @@ A.ESome (same_pos @@ translate_lit l)
| D.EOp op -> Bindlib.box @@ same_pos @@ A.ESome (same_pos @@ A.EOp op)
| D.EIfThenElse (e1, e2, e3) ->
Bindlib.box_apply3
(fun e1 e2 e3 -> Pos.same_pos_as (A.EIfThenElse (e1, e2, e3)) e)
(translate_expr ctx e1) (translate_expr ctx e2) (translate_expr ctx e3)
| D.EAssert e1 ->
Bindlib.box_apply (fun e1 -> Pos.same_pos_as (A.EAssert e1) e) (translate_expr ctx e1)
let e1 = translate_expr ctx e1 in
let pos = Pos.get_position (Bindlib.unbox e1) in
let x = A.Var.make ("e1", pos) in
(* we can say staticly what is the type of tau here. *)
let tau = failwith "todo" in
let e2 =
let+ e1 = Bindlib.box (A.EVar (x, pos))
and+ e2 = translate_expr ctx e2
and+ e3 = translate_expr ctx e3 in
same_pos @@ A.EIfThenElse ((e1, pos), e2, e3)
in
A.make_letopt_in x tau e1 e2
| D.EAssert _e1 ->
(* don't know the semantic of EAssert. *)
(* Bindlib.box_apply (fun e1 -> Pos.same_pos_as (A.EAssert e1) e) (translate_expr ctx e1) *)
failwith "todo"
| D.ErrorOnEmpty arg ->
Bindlib.box_apply
(fun arg ->
Pos.same_pos_as
(A.ECatch (arg, A.EmptyError, Pos.same_pos_as (A.ERaise A.NoValueProvided) e))
e)
(translate_expr ctx arg)
let pos = Pos.get_position arg in
let x = A.Var.make ("e1", pos) in
let arg = translate_expr ctx arg in
let tau = failwith "todo" in
let+ e2 = A.make_abs
(Array.of_list [ x ])
(Bindlib.box @@ same_pos @@ A.EVar (x, pos))
pos
[ tau ]
pos
and+ e1 = arg in
same_pos @@ A.EMatchopt (e1, same_pos @@ A.ERaise A.NoValueProvided , e2)
| D.EApp (e1, args) ->
Bindlib.box_apply2
(fun e1 args -> Pos.same_pos_as (A.EApp (e1, args)) e)
(translate_expr ctx e1)
(Bindlib.box_list (List.map (translate_expr ctx) args))
let e1 = translate_expr ctx e1 in
let pos = Pos.get_position(Bindlib.unbox e1) in
let x = A.Var.make ("e1", pos) in
let tau = failwith "todo" in
let e2 =
let+ e1 = Bindlib.box (A.EVar (x, pos))
and+ args = Bindlib.box_list (List.map (translate_expr ctx) args) in
same_pos @@ A.EApp ((e1, pos), args)
in
A.make_letopt_in x tau e1 e2
| D.EAbs ((binder, pos_binder), ts) ->
let vars, body = Bindlib.unmbind binder in
let ctx, lc_vars =
@ -125,22 +188,8 @@ and translate_expr (ctx : ctx) (e : D.expr Pos.marked) : A.expr Pos.marked Bindl
in
let lc_vars = Array.of_list lc_vars in
let new_body = translate_expr ctx body in
let new_binder = Bindlib.bind_mvar lc_vars new_body in
Bindlib.box_apply
(fun new_binder -> Pos.same_pos_as (A.EAbs ((new_binder, pos_binder), ts)) e)
new_binder
| D.EDefault ([ exn ], just, cons) when !Cli.optimize_flag ->
Bindlib.box_apply3
(fun exn just cons ->
Pos.same_pos_as
(A.ECatch
( exn,
A.EmptyError,
Pos.same_pos_as
(A.EIfThenElse (just, cons, Pos.same_pos_as (A.ERaise A.EmptyError) e))
e ))
e)
(translate_expr ctx exn) (translate_expr ctx just) (translate_expr ctx cons)
let+ new_binder = Bindlib.bind_mvar lc_vars new_body in
same_pos @@ A.ESome (same_pos @@ A.EAbs ((new_binder, pos_binder), List.map translate_typ ts))
| D.EDefault (exceptions, just, cons) ->
translate_default ctx exceptions just cons (Pos.get_position e)