This commit is contained in:
Louis Gesbert 2022-10-04 14:25:15 +02:00
parent ea114bada2
commit 14f1ebfd0a
6 changed files with 36 additions and 35 deletions

View File

@ -479,7 +479,7 @@ let interpret_program :
fun (ctx : decl_ctx) (e : 'm Ast.expr) :
(Uid.MarkedString.info * 'm Ast.expr) list ->
match evaluate_expr ctx e with
| EAbs (_, [((TStruct s_in, _) as _targs)]), mark_e as e -> begin
| (EAbs (_, [((TStruct s_in, _) as _targs)]), mark_e) as e -> begin
(* At this point, the interpreter seeks to execute the scope but does not
have a way to retrieve input values from the command line. [taus] contain
the types of the scope arguments. For [context] arguments, we can provide
@ -503,7 +503,7 @@ let interpret_program :
in
let to_interpret =
Expr.make_app (Bindlib.box e)
[ Expr.make_tuple application_term (Some s_in) mark_e ]
[Expr.make_tuple application_term (Some s_in) mark_e]
(Expr.pos e)
in
match Marked.unmark (evaluate_expr ctx (Bindlib.unbox to_interpret)) with

View File

@ -41,8 +41,9 @@ let rec translate_default
let pos = Expr.mark_pos mark_default in
let exceptions =
Expr.make_app
(Expr.make_var (Var.translate A.handle_default,
(Expr.with_ty mark_default (Utils.Marked.mark pos TAny))))
(Expr.make_var
( Var.translate A.handle_default,
Expr.with_ty mark_default (Utils.Marked.mark pos TAny) ))
[
Expr.earray exceptions mark_default;
thunk_expr (translate_expr ctx just);

View File

@ -61,20 +61,16 @@ let empty_ctx
local_vars = Var.Map.empty;
}
let mark_tany m pos =
Expr.with_ty m (Marked.mark pos TAny) ~pos
let mark_tany m pos = Expr.with_ty m (Marked.mark pos TAny) ~pos
(* Expression argument is used as a type witness, its type and positions aren't
used *)
let pos_mark_mk (type a m) (e : (a, m mark) gexpr):
(Pos.t -> m mark) *
((_, Pos.t) Marked.t -> m mark) =
let pos_mark_mk (type a m) (e : (a, m mark) gexpr) :
(Pos.t -> m mark) * ((_, Pos.t) Marked.t -> m mark) =
let pos_mark pos =
Expr.map_mark (fun _ -> pos) (fun _ -> TAny, pos) (Marked.get_mark e)
in
let pos_mark_as e =
pos_mark (Marked.get_mark e)
in
let pos_mark_as e = pos_mark (Marked.get_mark e) in
pos_mark, pos_mark_as
let merge_defaults
@ -92,7 +88,8 @@ let merge_defaults
(fun caller callee ->
let m = Marked.get_mark callee in
let ltrue =
Marked.mark (Expr.with_ty m (Marked.mark (Expr.mark_pos m) (TLit TBool)))
Marked.mark
(Expr.with_ty m (Marked.mark (Expr.mark_pos m) (TLit TBool)))
(ELit (LBool true))
in
Marked.mark m (EDefault ([caller], ltrue, callee)))
@ -108,8 +105,7 @@ let tag_with_log_entry
Bindlib.box_apply
(fun e ->
let m = mark_tany (Marked.get_mark e) (Expr.pos e) in
Marked.mark m
(EApp (Marked.mark m (EOp (Unop (Log (l, markings)))), [e])))
Marked.mark m (EApp (Marked.mark m (EOp (Unop (Log (l, markings)))), [e])))
e
(* In a list of exceptions, it is normally an error if more than a single one
@ -555,8 +551,7 @@ let translate_rule
in
let subscope_func =
tag_with_log_entry
(Expr.make_var
(scope_dcalc_var, mark_tany m pos_call))
(Expr.make_var (scope_dcalc_var, mark_tany m pos_call))
BeginCall
[
sigma_name, pos_sigma;
@ -650,8 +645,7 @@ let translate_rule
defined, we add an check "ErrorOnEmpty" here. *)
Marked.mark
(Expr.map_ty (fun _ -> scope_let_typ) (Marked.get_mark e))
(EAssert (Marked.same_mark_as (ErrorOnEmpty new_e) e))
;
(EAssert (Marked.same_mark_as (ErrorOnEmpty new_e) e));
scope_let_kind = Assertion;
})
(Bindlib.bind_var (Var.make "_") next)
@ -662,7 +656,7 @@ let translate_rules
(ctx : 'm ctx)
(rules : 'm Ast.rule list)
((sigma_name, pos_sigma) : Utils.Uid.MarkedString.info)
(mark: 'm mark)
(mark : 'm mark)
(sigma_return_struct_name : StructName.t) :
'm Dcalc.Ast.expr scope_body_expr Bindlib.box * 'm ctx =
let scope_lets, new_ctx =
@ -684,8 +678,7 @@ let translate_rules
let return_exp =
Bindlib.box_apply
(fun args ->
ETuple (args, Some sigma_return_struct_name),
mark_tany mark pos_sigma)
ETuple (args, Some sigma_return_struct_name), mark_tany mark pos_sigma)
(Bindlib.box_list
(List.map
(fun (_, (dcalc_var, _, _)) ->
@ -790,7 +783,8 @@ let translate_scope_decl
mark_tany sigma.scope_mark pos_sigma );
})
(Bindlib.bind_var v next)
(Expr.make_var (scope_input_var, mark_tany sigma.scope_mark pos_sigma)),
(Expr.make_var
(scope_input_var, mark_tany sigma.scope_mark pos_sigma)),
i - 1 ))
scope_input_variables
(next, List.length scope_input_variables - 1))

View File

@ -256,8 +256,7 @@ let rec unifiable ty1 ty2 =
| TOption t1, TOption t2 -> unifiable t1 t2
| TArrow (t1, t1'), TArrow (t2, t2') -> unifiable t1 t2 && unifiable t1' t2'
| TArray t1, TArray t2 -> unifiable t1 t2
| ( ( TLit _ | TTuple _ | TStruct _ | TEnum _ | TOption _ | TArrow _
| TArray _ ),
| ( (TLit _ | TTuple _ | TStruct _ | TEnum _ | TOption _ | TArrow _ | TArray _),
_ ) ->
false
@ -755,8 +754,12 @@ let make_app e u pos =
tr
| TAny -> tf
| _ ->
Format.eprintf "Attempt to construct application of non-arrow type %a:@\n%a"
Print.typ_debug tf (Print.expr_debug ~debug:false) e;
Format.eprintf
"Attempt to construct application of non-arrow type %a:@\n\
%a"
Print.typ_debug tf
(Print.expr_debug ~debug:false)
e;
assert false)
fty.ty argtys)
(List.map Marked.get_mark (e :: u))
@ -799,9 +802,10 @@ let make_tuple el structname m0 =
match el with
| [] ->
etuple [] structname
(with_ty m0 (match structname with
| Some n -> TStruct n, mark_pos m0
| None -> TTuple [], mark_pos m0))
(with_ty m0
(match structname with
| Some n -> TStruct n, mark_pos m0
| None -> TTuple [], mark_pos m0))
| el ->
let m =
fold_marks

View File

@ -225,12 +225,13 @@ val make_default :
exceptions, is collapsed into [<ex | def>]
- [<ex | false :- _>], when [ex] is a single exception, is rewritten as [ex] *)
(** Builds a tuple; the mark argument is only used as witness and for position when building 0-uples *)
val make_tuple:
([< dcalc | lcalc] as 'a, 'm mark) gexpr box list ->
val make_tuple :
(([< dcalc | lcalc ] as 'a), 'm mark) gexpr box list ->
StructName.t option ->
'm mark ->
('a, 'm mark) gexpr box
(** Builds a tuple; the mark argument is only used as witness and for position
when building 0-uples *)
(** {2 Transformations} *)

View File

@ -92,14 +92,15 @@ let map_exprs ~f ~varf scopes =
new_body_expr new_next)
~init:(Bindlib.box Nil) scopes
(* TODO: compute the expected body expr arrow type manually instead of [TAny] for double-checking types ? *)
(* TODO: compute the expected body expr arrow type manually instead of [TAny]
for double-checking types ? *)
let rec get_body_expr_mark = function
| ScopeLet sl ->
let _, e = Bindlib.unbind sl.scope_let_next in
get_body_expr_mark e
| Result e ->
let m = Marked.get_mark e in
(Expr.with_ty m (Utils.Marked.mark (Expr.mark_pos m) TAny))
Expr.with_ty m (Utils.Marked.mark (Expr.mark_pos m) TAny)
let get_body_mark scope_body =
let _, e = Bindlib.unbind scope_body.scope_body_expr in