CatalaLang/catala
1
1
Fork 0
mirror of https://github.com/CatalaLang/catala.git synced 2024-09-19 16:28:12 +03:00
Code Issues Projects Releases Wiki Activity

Make all supertypes use ('a, 't) gexpr as parameter instead of naked_gexpr

Browse Source
This commit is contained in:
Louis Gesbert 2022-08-25 19:46:13 +02:00 committed by Denis Merigoux
parent 5e9c3d630e
commit 7e0d24efd2
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
44 changed files with 268 additions and 351 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
compiler/dcalc/ast.ml
View File

@ -22,4 +22,4 @@ type lit = dcalc glit
type 'm naked_expr = (dcalc, 'm mark) naked_gexpr
and 'm expr = (dcalc, 'm mark) gexpr
type 'm program = 'm naked_expr Shared_ast.program
type 'm program = 'm expr Shared_ast.program

2
compiler/dcalc/ast.mli
View File

@ -24,4 +24,4 @@ type lit = dcalc glit
type 'm naked_expr = (dcalc, 'm mark) naked_gexpr
and 'm expr = (dcalc, 'm mark) gexpr
type 'm program = 'm naked_expr Shared_ast.program
type 'm program = 'm expr Shared_ast.program

12
compiler/dcalc/interpreter.ml
View File

@ -36,7 +36,8 @@ let rec evaluate_operator
(args : 'm Ast.expr list) : 'm Ast.naked_expr =
(* Try to apply [div] and if a [Division_by_zero] exceptions is catched, use
[op] to raise multispanned errors. *)
let apply_div_or_raise_err (div : unit -> 'm Ast.naked_expr) : 'm Ast.naked_expr =
let apply_div_or_raise_err (div : unit -> 'm Ast.naked_expr) :
'm Ast.naked_expr =
try div ()
with Division_by_zero ->
Errors.raise_multispanned_error
@ -314,8 +315,7 @@ let rec evaluate_operator
"Operator applied to the wrong arguments\n\
(should not happen if the term was well-typed)"
and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr
=
and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr =
match Marked.unmark e with
| EVar _ ->
Errors.raise_spanned_error (Expr.pos e)
@ -481,10 +481,8 @@ and evaluate_expr (ctx : decl_ctx) (e : 'm Ast.expr) : 'm Ast.expr
(** {1 API} *)
let interpret_program :
'm.
decl_ctx ->
'm Ast.expr ->
(Uid.MarkedString.info * 'm Ast.expr) list =
'm. decl_ctx -> 'm Ast.expr -> (Uid.MarkedString.info * 'm Ast.expr) list
=
fun (ctx : decl_ctx) (e : 'm Ast.expr) :
(Uid.MarkedString.info * 'm Ast.expr) list ->
match evaluate_expr ctx e with

4
compiler/dcalc/interpreter.mli
View File

@ -23,9 +23,7 @@ val evaluate_expr : decl_ctx -> 'm Ast.expr -> 'm Ast.expr
(** Evaluates an expression according to the semantics of the default calculus. *)
val interpret_program :
decl_ctx ->
'm Ast.expr ->
(Uid.MarkedString.info * 'm Ast.expr) list
decl_ctx -> 'm Ast.expr -> (Uid.MarkedString.info * 'm Ast.expr) list
(** Interprets a program. This function expects an expression typed as a
function whose argument are all thunked. The function is executed by
providing for each argument a thunked empty default. Returns a list of all

8
compiler/dcalc/optimizations.ml
View File

@ -19,7 +19,7 @@ open Shared_ast
open Ast
type partial_evaluation_ctx = {
var_values : (typed naked_expr, typed expr) Var.Map.t;
var_values : (typed expr, typed expr) Var.Map.t;
decl_ctx : decl_ctx;
}
@ -190,8 +190,8 @@ let optimize_expr (decl_ctx : decl_ctx) (e : 'm expr) =
let rec scope_lets_map
(t : 'a -> 'm expr -> 'm expr Bindlib.box)
(ctx : 'a)
(scope_body_expr : 'm naked_expr scope_body_expr) :
'm naked_expr scope_body_expr Bindlib.box =
(scope_body_expr : 'm expr scope_body_expr) :
'm expr scope_body_expr Bindlib.box =
match scope_body_expr with
| Result e -> Bindlib.box_apply (fun e' -> Result e') (t ctx e)
| ScopeLet scope_let ->
@ -212,7 +212,7 @@ let rec scope_lets_map
let rec scopes_map
(t : 'a -> 'm expr -> 'm expr Bindlib.box)
(ctx : 'a)
(scopes : 'm naked_expr scopes) : 'm naked_expr scopes Bindlib.box =
(scopes : 'm expr scopes) : 'm expr scopes Bindlib.box =
match scopes with
| Nil -> Bindlib.box Nil
| ScopeDef scope_def ->

27
compiler/dcalc/typing.ml
View File

@ -33,8 +33,8 @@ module Any =
()
type unionfind_typ = naked_typ Marked.pos UnionFind.elem
(** We do not reuse {!type: Dcalc.Ast.naked_typ} because we have to include a new
[TAny] variant. Indeed, error terms can have any type and this has to be
(** We do not reuse {!type: Dcalc.Ast.naked_typ} because we have to include a
new [TAny] variant. Indeed, error terms can have any type and this has to be
captured by the type sytem. *)
and naked_typ =
@ -84,9 +84,7 @@ let rec format_typ
(fmt : Format.formatter)
(naked_typ : unionfind_typ) : unit =
let format_typ = format_typ ctx in
let format_typ_with_parens
(fmt : Format.formatter)
(t : unionfind_typ) =
let format_typ_with_parens (fmt : Format.formatter) (t : unionfind_typ) =
if typ_needs_parens t then Format.fprintf fmt "(%a)" format_typ t
else Format.fprintf fmt "%a" format_typ t
in
@ -109,11 +107,7 @@ let rec format_typ
| TArray t1 -> Format.fprintf fmt "@[%a@ array@]" format_typ t1
| TAny d -> Format.fprintf fmt "any[%d]" (Any.hash d)
exception
Type_error of
A.any_marked_expr
* unionfind_typ
* unionfind_typ
exception Type_error of A.any_marked_expr * unionfind_typ * unionfind_typ
type mark = { pos : Pos.t; uf : unionfind_typ }
@ -306,7 +300,7 @@ let box_ty e = Bindlib.unbox (Bindlib.box_apply ty e)
(** Infers the most permissive type from an expression *)
let rec typecheck_expr_bottom_up
(ctx : A.decl_ctx)
(env : 'm Ast.naked_expr env)
(env : 'm Ast.expr env)
(e : 'm Ast.expr) : (A.dcalc, mark) A.gexpr Bindlib.box =
(* Cli.debug_format "Looking for type of %a" (Expr.format ~debug:true ctx)
e; *)
@ -469,11 +463,11 @@ let rec typecheck_expr_bottom_up
(** Checks whether the expression can be typed with the provided type *)
and typecheck_expr_top_down
(ctx : A.decl_ctx)
(env : 'm Ast.naked_expr env)
(env : 'm Ast.expr env)
(tau : unionfind_typ)
(e : 'm Ast.expr) : (A.dcalc, mark) A.gexpr Bindlib.box =
(* Cli.debug_format "Propagating type %a for naked_expr %a" (format_typ ctx) tau
(Expr.format ctx) e; *)
(* Cli.debug_format "Propagating type %a for naked_expr %a" (format_typ ctx)
tau (Expr.format ctx) e; *)
let pos_e = A.Expr.pos e in
let mark e = Marked.mark { uf = tau; pos = pos_e } e in
let unify_and_mark (e' : (A.dcalc, mark) A.naked_gexpr) tau' =
@ -667,10 +661,7 @@ let infer_type (type m) ctx (e : m Ast.expr) =
| A.Untyped _ -> A.Expr.ty (Bindlib.unbox (infer_types ctx e))
(** Typechecks an expression given an expected type *)
let check_type
(ctx : A.decl_ctx)
(e : 'm Ast.expr)
(tau : A.typ) =
let check_type (ctx : A.decl_ctx) (e : 'm Ast.expr) (tau : A.typ) =
(* todo: consider using the already inferred type if ['m] = [typed] *)
ignore
@@ wrap ctx (typecheck_expr_top_down ctx A.Var.Map.empty (ast_to_typ tau)) e

3
compiler/dcalc/typing.mli
View File

@ -19,8 +19,7 @@
open Shared_ast
val infer_types :
decl_ctx -> untyped Ast.expr -> typed Ast.expr Bindlib.box
val infer_types : decl_ctx -> untyped Ast.expr -> typed Ast.expr Bindlib.box
(** Infers types everywhere on the given expression, and adds (or replaces) type
annotations on each node *)

5
compiler/desugared/ast.ml
View File

@ -114,7 +114,7 @@ type rule = {
rule_id : RuleName.t;
rule_just : expr Bindlib.box;
rule_cons : expr Bindlib.box;
rule_parameter : (naked_expr Var.t * typ) option;
rule_parameter : (expr Var.t * typ) option;
rule_exception : exception_situation;
rule_label : label_situation;
}
@ -167,8 +167,7 @@ let empty_rule (pos : Pos.t) (have_parameter : typ option) : rule =
rule_label = Unlabeled;
}
let always_false_rule (pos : Pos.t) (have_parameter : typ option) : rule
=
let always_false_rule (pos : Pos.t) (have_parameter : typ option) : rule =
{
rule_just = Bindlib.box (ELit (LBool true), pos);
rule_cons = Bindlib.box (ELit (LBool false), pos);

2
compiler/desugared/ast.mli
View File

@ -72,7 +72,7 @@ type rule = {
rule_id : RuleName.t;
rule_just : expr Bindlib.box;
rule_cons : expr Bindlib.box;
rule_parameter : (naked_expr Var.t * typ) option;
rule_parameter : (expr Var.t * typ) option;
rule_exception : exception_situation;
rule_label : label_situation;
}

12
compiler/desugared/desugared_to_scope.ml
View File

@ -27,14 +27,13 @@ type target_scope_vars =
type ctx = {
scope_var_mapping : target_scope_vars ScopeVarMap.t;
var_mapping : (Ast.naked_expr, Scopelang.Ast.naked_expr Var.t) Var.Map.t;
var_mapping : (Ast.expr, Scopelang.Ast.expr Var.t) Var.Map.t;
}
let tag_with_log_entry
(e : Scopelang.Ast.expr)
(l : log_entry)
(markings : Utils.Uid.MarkedString.info list) :
Scopelang.Ast.expr =
(markings : Utils.Uid.MarkedString.info list) : Scopelang.Ast.expr =
( EApp ((EOp (Unop (Log (l, markings))), Marked.get_mark e), [e]),
Marked.get_mark e )
@ -186,7 +185,7 @@ let rec rule_tree_to_expr
~(toplevel : bool)
(ctx : ctx)
(def_pos : Pos.t)
(is_func : Ast.naked_expr Var.t option)
(is_func : Ast.expr Var.t option)
(tree : rule_tree) : Scopelang.Ast.expr Bindlib.box =
let exceptions, base_rules =
match tree with Leaf r -> [], r | Node (exceptions, r) -> exceptions, r
@ -194,9 +193,8 @@ let rec rule_tree_to_expr
(* because each rule has its own variable parameter and we want to convert the
whole rule tree into a function, we need to perform some alpha-renaming of
all the expressions *)
let substitute_parameter
(e : Ast.expr Bindlib.box)
(rule : Ast.rule) : Ast.expr Bindlib.box =
let substitute_parameter (e : Ast.expr Bindlib.box) (rule : Ast.rule) :
Ast.expr Bindlib.box =
match is_func, rule.Ast.rule_parameter with
| Some new_param, Some (old_param, _) ->
let binder = Bindlib.bind_var old_param e in

2
compiler/lcalc/ast.ml
View File

@ -22,7 +22,7 @@ type lit = lcalc glit
type 'm naked_expr = (lcalc, 'm mark) naked_gexpr
and 'm expr = (lcalc, 'm mark) gexpr
type 'm program = 'm naked_expr Shared_ast.program
type 'm program = 'm expr Shared_ast.program
let option_enum : EnumName.t = EnumName.fresh ("eoption", Pos.no_pos)
let none_constr : EnumConstructor.t = EnumConstructor.fresh ("ENone", Pos.no_pos)

8
compiler/lcalc/ast.mli
View File

@ -25,7 +25,7 @@ type lit = lcalc glit
type 'm naked_expr = (lcalc, 'm mark) naked_gexpr
and 'm expr = (lcalc, 'm mark) gexpr
type 'm program = 'm naked_expr Shared_ast.program
type 'm program = 'm expr Shared_ast.program
(** {1 Language terms construction}*)
@ -44,7 +44,7 @@ val make_matchopt_with_abs_arms :
val make_matchopt :
'm mark ->
'm naked_expr Var.t ->
'm expr Var.t ->
typ ->
'm expr Bindlib.box ->
'm expr Bindlib.box ->
@ -55,5 +55,5 @@ val make_matchopt :
(** {1 Special symbols} *)
val handle_default : untyped naked_expr Var.t
val handle_default_opt : untyped naked_expr Var.t
val handle_default : untyped expr Var.t
val handle_default_opt : untyped expr Var.t

2
compiler/lcalc/closure_conversion.ml
View File

@ -22,7 +22,7 @@ module D = Dcalc.Ast
(** TODO: This version is not yet debugged and ought to be specialized when
Lcalc has more structure. *)
type 'm ctx = { name_context : string; globally_bound_vars : 'm naked_expr Var.Set.t }
type 'm ctx = { name_context : string; globally_bound_vars : 'm expr Var.Set.t }
(** Returns the expression with closed closures and the set of free variables
inside this new expression. Implementation guided by

13
compiler/lcalc/compile_with_exceptions.ml
View File

@ -19,7 +19,7 @@ open Shared_ast
module D = Dcalc.Ast
module A = Ast
type 'm ctx = ('m D.naked_expr, 'm A.naked_expr Var.t) Var.Map.t
type 'm ctx = ('m D.expr, 'm A.expr Var.t) Var.Map.t
(** This environment contains a mapping between the variables in Dcalc and their
correspondance in Lcalc. *)
@ -51,8 +51,7 @@ let rec translate_default
in
exceptions
and translate_expr (ctx : 'm ctx) (e : 'm D.expr) :
'm A.expr Bindlib.box =
and translate_expr (ctx : 'm ctx) (e : 'm D.expr) : 'm A.expr Bindlib.box =
match Marked.unmark e with
| EVar v -> Expr.make_var (Var.Map.find v ctx, Marked.get_mark e)
| ETuple (args, s) ->
@ -112,8 +111,8 @@ and translate_expr (ctx : 'm ctx) (e : 'm D.expr) :
let rec translate_scope_lets
(decl_ctx : decl_ctx)
(ctx : 'm ctx)
(scope_lets : 'm D.naked_expr scope_body_expr) :
'm A.naked_expr scope_body_expr Bindlib.box =
(scope_lets : 'm D.expr scope_body_expr) :
'm A.expr scope_body_expr Bindlib.box =
match scope_lets with
| Result e -> Bindlib.box_apply (fun e -> Result e) (translate_expr ctx e)
| ScopeLet scope_let ->
@ -140,7 +139,7 @@ let rec translate_scope_lets
let rec translate_scopes
(decl_ctx : decl_ctx)
(ctx : 'm ctx)
(scopes : 'm D.naked_expr scopes) : 'm A.naked_expr scopes Bindlib.box =
(scopes : 'm D.expr scopes) : 'm A.expr scopes Bindlib.box =
match scopes with
| Nil -> Bindlib.box Nil
| ScopeDef scope_def ->
@ -159,7 +158,7 @@ let rec translate_scopes
let new_scope_body_expr =
Bindlib.bind_var new_scope_input_var new_scope_body_expr
in
let new_scope : 'm A.naked_expr scope_body Bindlib.box =
let new_scope : 'm A.expr scope_body Bindlib.box =
Bindlib.box_apply
(fun new_scope_body_expr ->
{

29
compiler/lcalc/compile_without_exceptions.ml
View File

@ -42,12 +42,13 @@ module A = Ast
open Shared_ast
type 'm hoists = ('m A.naked_expr, 'm D.expr) Var.Map.t
(** Hoists definition. It represent bindings between [A.Var.t] and [D.naked_expr]. *)
type 'm hoists = ('m A.expr, 'm D.expr) Var.Map.t
(** Hoists definition. It represent bindings between [A.Var.t] and
[D.naked_expr]. *)
type 'm info = {
naked_expr : 'm A.expr Bindlib.box;
var : 'm A.naked_expr Bindlib.var;
var : 'm A.expr Var.t;
is_pure : bool;
}
(** Information about each encontered Dcalc variable is stored inside a context
@ -61,14 +62,14 @@ let pp_info (fmt : Format.formatter) (info : 'm info) =
type 'm ctx = {
decl_ctx : decl_ctx;
vars : ('m D.naked_expr, 'm info) Var.Map.t;
vars : ('m D.expr, 'm info) Var.Map.t;
(** information context about variables in the current scope *)
}
let _pp_ctx (fmt : Format.formatter) (ctx : 'm ctx) =
let pp_binding
(fmt : Format.formatter)
((v, info) : 'm D.naked_expr Var.t * 'm info) =
((v, info) : 'm D.expr Var.t * 'm info) =
Format.fprintf fmt "%a: %a" Print.var v pp_info info
in
@ -82,7 +83,7 @@ let _pp_ctx (fmt : Format.formatter) (ctx : 'm ctx) =
(** [find ~info n ctx] is a warpper to ocaml's Map.find that handle errors in a
slightly better way. *)
let find ?(info : string = "none") (n : 'm D.naked_expr Var.t) (ctx : 'm ctx) :
let find ?(info : string = "none") (n : 'm D.expr Var.t) (ctx : 'm ctx) :
'm info =
(* let _ = Format.asprintf "Searching for variable %a inside context %a"
Print.var n pp_ctx ctx |> Cli.debug_print in *)
@ -99,7 +100,7 @@ let find ?(info : string = "none") (n : 'm D.naked_expr Var.t) (ctx : 'm ctx) :
debuging purposes as it printing each of the Dcalc/Lcalc variable pairs. *)
let add_var
(mark : 'm mark)
(var : 'm D.naked_expr Var.t)
(var : 'm D.expr Var.t)
(is_pure : bool)
(ctx : 'm ctx) : 'm ctx =
let new_var = Var.make (Bindlib.name_of var) in
@ -288,8 +289,8 @@ let rec translate_and_hoist (ctx : 'm ctx) (e : 'm D.expr) :
Expr.earray es' pos, disjoint_union_maps (Expr.pos e) hoists
| EOp op -> Bindlib.box (EOp op, pos), Var.Map.empty
and translate_expr ?(append_esome = true) (ctx : 'm ctx) (e : 'm D.expr)
: 'm A.expr Bindlib.box =
and translate_expr ?(append_esome = true) (ctx : 'm ctx) (e : 'm D.expr) :
'm A.expr Bindlib.box =
let e', hoists = translate_and_hoist ctx e in
let hoists = Var.Map.bindings hoists in
@ -356,8 +357,8 @@ and translate_expr ?(append_esome = true) (ctx : 'm ctx) (e : 'm D.expr)
(TAny, Expr.mark_pos mark_hoist)
c' (A.make_none mark_hoist) acc)
let rec translate_scope_let (ctx : 'm ctx) (lets : 'm D.naked_expr scope_body_expr) :
'm A.naked_expr scope_body_expr Bindlib.box =
let rec translate_scope_let (ctx : 'm ctx) (lets : 'm D.expr scope_body_expr) :
'm A.expr scope_body_expr Bindlib.box =
match lets with
| Result e ->
Bindlib.box_apply
@ -478,7 +479,7 @@ let rec translate_scope_let (ctx : 'm ctx) (lets : 'm D.naked_expr scope_body_ex
let translate_scope_body
(scope_pos : Pos.t)
(ctx : 'm ctx)
(body : 'm D.naked_expr scope_body) : 'm A.naked_expr scope_body Bindlib.box =
(body : 'm D.expr scope_body) : 'm A.expr scope_body Bindlib.box =
match body with
| {
scope_body_expr = result;
@ -504,8 +505,8 @@ let translate_scope_body
})
(Bindlib.bind_var v' (translate_scope_let ctx' lets))
let rec translate_scopes (ctx : 'm ctx) (scopes : 'm D.naked_expr scopes) :
'm A.naked_expr scopes Bindlib.box =
let rec translate_scopes (ctx : 'm ctx) (scopes : 'm D.expr scopes) :
'm A.expr scopes Bindlib.box =
match scopes with
| Nil -> Bindlib.box Nil
| ScopeDef { scope_name; scope_body; scope_next } ->

3
compiler/lcalc/optimizations.ml
View File

@ -116,8 +116,7 @@ let _beta_optimizations (p : 'm program) : 'm program =
in
{ p with scopes = Bindlib.unbox new_scopes }
let rec peephole_expr (_ : unit) (e : 'm expr) :
'm expr Bindlib.box =
let rec peephole_expr (_ : unit) (e : 'm expr) : 'm expr Bindlib.box =
let default_mark e' = Marked.mark (Marked.get_mark e) e' in
match Marked.unmark e with

16
compiler/lcalc/to_ocaml.ml
View File

@ -183,8 +183,7 @@ let format_enum_cons_name (fmt : Format.formatter) (v : EnumConstructor.t) :
(avoid_keywords
(to_ascii (Format.asprintf "%a" EnumConstructor.format_t v)))
let rec typ_embedding_name (fmt : Format.formatter) (ty : typ) : unit
=
let rec typ_embedding_name (fmt : Format.formatter) (ty : typ) : unit =
match Marked.unmark ty with
| TLit TUnit -> Format.fprintf fmt "embed_unit"
| TLit TBool -> Format.fprintf fmt "embed_bool"
@ -271,10 +270,8 @@ let format_exception (fmt : Format.formatter) (exc : except Marked.pos) : unit =
(Pos.get_end_line pos) (Pos.get_end_column pos) format_string_list
(Pos.get_law_info pos)
let rec format_expr
(ctx : decl_ctx)
(fmt : Format.formatter)
(e : 'm expr) : unit =
let rec format_expr (ctx : decl_ctx) (fmt : Format.formatter) (e : 'm expr) :
unit =
let format_expr = format_expr ctx in
let format_with_parens (fmt : Format.formatter) (e : 'm expr) =
if needs_parens e then Format.fprintf fmt "(%a)" format_expr e
@ -472,8 +469,7 @@ let format_struct_embedding
let format_enum_embedding
(fmt : Format.formatter)
((enum_name, enum_cases) :
EnumName.t * (EnumConstructor.t * typ) list) =
((enum_name, enum_cases) : EnumName.t * (EnumConstructor.t * typ) list) =
if List.length enum_cases = 0 then
Format.fprintf fmt "let embed_%a (_: %a.t) : runtime_value = Unit@\n@\n"
format_to_module_name (`Ename enum_name) format_enum_name enum_name
@ -556,7 +552,7 @@ let format_ctx
let rec format_scope_body_expr
(ctx : decl_ctx)
(fmt : Format.formatter)
(scope_lets : 'm Ast.naked_expr scope_body_expr) : unit =
(scope_lets : 'm Ast.expr scope_body_expr) : unit =
match scope_lets with
| Result e -> format_expr ctx fmt e
| ScopeLet scope_let ->
@ -572,7 +568,7 @@ let rec format_scope_body_expr
let rec format_scopes
(ctx : decl_ctx)
(fmt : Format.formatter)
(scopes : 'm Ast.naked_expr scopes) : unit =
(scopes : 'm Ast.expr scopes) : unit =
match scopes with
| Nil -> ()
| ScopeDef scope_def ->

9
compiler/lcalc/to_ocaml.mli
View File

@ -21,13 +21,8 @@ open Ast
(** Formats a lambda calculus program into a valid OCaml program *)
val avoid_keywords : string -> string
val find_struct :
StructName.t -> decl_ctx -> (StructFieldName.t * typ) list
val find_enum :
EnumName.t -> decl_ctx -> (EnumConstructor.t * typ) list
val find_struct : StructName.t -> decl_ctx -> (StructFieldName.t * typ) list
val find_enum : EnumName.t -> decl_ctx -> (EnumConstructor.t * typ) list
val typ_needs_parens : typ -> bool
val needs_parens : 'm expr -> bool
val format_enum_name : Format.formatter -> EnumName.t -> unit

4
compiler/plugins/api_web.ml
View File

@ -328,10 +328,10 @@ module To_jsoo = struct
Format.fprintf fmt "%a@\n" format_enum_decl (e, find_enum e ctx))
(type_ordering @ scope_structs)
let fmt_input_struct_name fmt (scope_def : 'a naked_expr scope_def) =
let fmt_input_struct_name fmt (scope_def : 'a expr scope_def) =
format_struct_name fmt scope_def.scope_body.scope_body_input_struct
let fmt_output_struct_name fmt (scope_def : 'a naked_expr scope_def) =
let fmt_output_struct_name fmt (scope_def : 'a expr scope_def) =
format_struct_name fmt scope_def.scope_body.scope_body_output_struct
let rec format_scopes_to_fun

5
compiler/plugins/json_schema.ml
View File

@ -49,7 +49,7 @@ module To_json = struct
Format.fprintf fmt "%s" s
let rec find_scope_def (target_name : string) :
'm naked_expr scopes -> 'm naked_expr scope_def option = function
'm expr scopes -> 'm expr scope_def option = function
| Nil -> None
| ScopeDef scope_def ->
let name = Format.asprintf "%a" ScopeName.format_t scope_def.scope_name in
@ -111,8 +111,7 @@ module To_json = struct
in
let rec collect_required_type_defs_from_scope_input
(input_struct : StructName.t) : typ list =
let rec collect (acc : typ list) (t : typ) : typ list
=
let rec collect (acc : typ list) (t : typ) : typ list =
match Marked.unmark t with
| TStruct s ->
(* Scope's input is a struct. *)

1
compiler/scalc/ast.ml
View File

@ -26,6 +26,7 @@ let handle_default = TopLevelName.fresh ("handle_default", Pos.no_pos)
let handle_default_opt = TopLevelName.fresh ("handle_default_opt", Pos.no_pos)
type expr = naked_expr Marked.pos
and naked_expr =
| EVar of LocalName.t
| EFunc of TopLevelName.t

16
compiler/scalc/compile_from_lambda.ml
View File

@ -21,17 +21,16 @@ module L = Lcalc.Ast
module D = Dcalc.Ast
type 'm ctxt = {
func_dict : ('m L.naked_expr, A.TopLevelName.t) Var.Map.t;
func_dict : ('m L.expr, A.TopLevelName.t) Var.Map.t;
decl_ctx : decl_ctx;
var_dict : ('m L.naked_expr, A.LocalName.t) Var.Map.t;
var_dict : ('m L.expr, A.LocalName.t) Var.Map.t;
inside_definition_of : A.LocalName.t option;
context_name : string;
}
(* Expressions can spill out side effect, hence this function also returns a
list of statements to be prepended before the expression is evaluated *)
let rec translate_expr (ctxt : 'm ctxt) (expr : 'm L.expr) :
A.block * A.expr =
let rec translate_expr (ctxt : 'm ctxt) (expr : 'm L.expr) : A.block * A.expr =
match Marked.unmark expr with
| EVar v ->
let local_var =
@ -115,8 +114,7 @@ let rec translate_expr (ctxt : 'm ctxt) (expr : 'm L.expr) :
:: tmp_stmts,
(A.EVar tmp_var, Expr.pos expr) )
and translate_statements (ctxt : 'm ctxt) (block_expr : 'm L.expr) :
A.block =
and translate_statements (ctxt : 'm ctxt) (block_expr : 'm L.expr) : A.block =
match Marked.unmark block_expr with
| EAssert e ->
(* Assertions are always encapsulated in a unit-typed let binding *)
@ -273,9 +271,9 @@ and translate_statements (ctxt : 'm ctxt) (block_expr : 'm L.expr) :
let rec translate_scope_body_expr
(scope_name : ScopeName.t)
(decl_ctx : decl_ctx)
(var_dict : ('m L.naked_expr, A.LocalName.t) Var.Map.t)
(func_dict : ('m L.naked_expr, A.TopLevelName.t) Var.Map.t)
(scope_expr : 'm L.naked_expr scope_body_expr) : A.block =
(var_dict : ('m L.expr, A.LocalName.t) Var.Map.t)
(func_dict : ('m L.expr, A.TopLevelName.t) Var.Map.t)
(scope_expr : 'm L.expr scope_body_expr) : A.block =
match scope_expr with
| Result e ->
let block, new_e =

6
compiler/scalc/to_python.ml
View File

@ -259,10 +259,8 @@ let format_exception (fmt : Format.formatter) (exc : except Marked.pos) : unit =
(Pos.get_end_line pos) (Pos.get_end_column pos) format_string_list
(Pos.get_law_info pos)
let rec format_expression
(ctx : decl_ctx)
(fmt : Format.formatter)
(e : expr) : unit =
let rec format_expression (ctx : decl_ctx) (fmt : Format.formatter) (e : expr) :
unit =
match Marked.unmark e with
| EVar v -> format_var fmt v
| EFunc f -> format_toplevel_name fmt f

13
compiler/scopelang/print.ml
View File

@ -21,8 +21,7 @@ open Ast
let struc
ctx
(fmt : Format.formatter)
((name, fields) : StructName.t * (StructFieldName.t * typ) list)
: unit =
((name, fields) : StructName.t * (StructFieldName.t * typ) list) : unit =
Format.fprintf fmt "%a %a %a %a@\n@[<hov 2> %a@]@\n%a" Print.keyword "type"
StructName.format_t name Print.punctuation "=" Print.punctuation "{"
(Format.pp_print_list
@ -35,8 +34,7 @@ let struc
let enum
ctx
(fmt : Format.formatter)
((name, cases) : EnumName.t * (EnumConstructor.t * typ) list) :
unit =
((name, cases) : EnumName.t * (EnumConstructor.t * typ) list) : unit =
Format.fprintf fmt "%a %a %a @\n@[<hov 2> %a@]" Print.keyword "type"
EnumName.format_t name Print.punctuation "="
(Format.pp_print_list
@ -85,12 +83,15 @@ let scope ?(debug = false) ctx fmt (name, decl) =
with
| Reentrant ->
Format.fprintf fmt "%a@ %a" Print.operator
"reentrant or by default" (Print.naked_expr ~debug ctx) e
"reentrant or by default"
(Print.naked_expr ~debug ctx)
e
| _ -> Format.fprintf fmt "%a" (Print.naked_expr ~debug ctx) e))
e
| Assertion e ->
Format.fprintf fmt "%a %a" Print.keyword "assert"
(Print.naked_expr ~debug ctx) e
(Print.naked_expr ~debug ctx)
e
| Call (scope_name, subscope_name) ->
Format.fprintf fmt "%a %a%a%a%a" Print.keyword "call"
ScopeName.format_t scope_name Print.punctuation "["

27
compiler/scopelang/scope_to_dcalc.ml
View File

@ -25,9 +25,9 @@ type scope_var_ctx = {
type scope_sig_ctx = {
scope_sig_local_vars : scope_var_ctx list; (** List of scope variables *)
scope_sig_scope_var : untyped Dcalc.Ast.naked_expr Var.t;
scope_sig_scope_var : untyped Dcalc.Ast.expr Var.t;
(** Var representing the scope *)
scope_sig_input_var : untyped Dcalc.Ast.naked_expr Var.t;
scope_sig_input_var : untyped Dcalc.Ast.expr Var.t;
(** Var representing the scope input inside the scope func *)
scope_sig_input_struct : StructName.t; (** Scope input *)
scope_sig_output_struct : StructName.t; (** Scope output *)
@ -40,11 +40,12 @@ type ctx = {
enums : enum_ctx;
scope_name : ScopeName.t;
scopes_parameters : scope_sigs_ctx;
scope_vars : (untyped Dcalc.Ast.naked_expr Var.t * naked_typ * Ast.io) ScopeVarMap.t;
scope_vars :
(untyped Dcalc.Ast.expr Var.t * naked_typ * Ast.io) ScopeVarMap.t;
subscope_vars :
(untyped Dcalc.Ast.naked_expr Var.t * naked_typ * Ast.io) ScopeVarMap.t
(untyped Dcalc.Ast.expr Var.t * naked_typ * Ast.io) ScopeVarMap.t
Ast.SubScopeMap.t;
local_vars : (Ast.naked_expr, untyped Dcalc.Ast.naked_expr Var.t) Var.Map.t;
local_vars : (Ast.expr, untyped Dcalc.Ast.expr Var.t) Var.Map.t;
}
let empty_ctx
@ -101,8 +102,7 @@ let tag_with_log_entry
NOTE: the choice of the exception that will be triggered and show in the
trace is arbitrary (but deterministic). *)
let collapse_similar_outcomes (excepts : Ast.expr list) :
Ast.expr list =
let collapse_similar_outcomes (excepts : Ast.expr list) : Ast.expr list =
let cons_map =
List.fold_left
(fun map -> function
@ -135,8 +135,7 @@ let collapse_similar_outcomes (excepts : Ast.expr list) :
let rec translate_expr (ctx : ctx) (e : Ast.expr) :
untyped Dcalc.Ast.expr Bindlib.box =
Bindlib.box_apply (fun (x : untyped Dcalc.Ast.naked_expr) ->
Marked.mark (pos_mark_as e) x)
Bindlib.box_apply (fun x -> Marked.mark (pos_mark_as e) x)
@@
match Marked.unmark e with
| EVar v -> Bindlib.box_var (Var.Map.find v ctx.local_vars)
@ -357,8 +356,8 @@ let translate_rule
(ctx : ctx)
(rule : Ast.rule)
((sigma_name, pos_sigma) : Utils.Uid.MarkedString.info) :
(untyped Dcalc.Ast.naked_expr scope_body_expr Bindlib.box ->
untyped Dcalc.Ast.naked_expr scope_body_expr Bindlib.box)
(untyped Dcalc.Ast.expr scope_body_expr Bindlib.box ->
untyped Dcalc.Ast.expr scope_body_expr Bindlib.box)
* ctx =
match rule with
| Definition ((ScopelangScopeVar a, var_def_pos), tau, a_io, e) ->
@ -636,7 +635,7 @@ let translate_rules
(rules : Ast.rule list)
((sigma_name, pos_sigma) : Utils.Uid.MarkedString.info)
(sigma_return_struct_name : StructName.t) :
untyped Dcalc.Ast.naked_expr scope_body_expr Bindlib.box * ctx =
untyped Dcalc.Ast.expr scope_body_expr Bindlib.box * ctx =
let scope_lets, new_ctx =
List.fold_left
(fun (scope_lets, ctx) rule ->
@ -673,7 +672,7 @@ let translate_scope_decl
(sctx : scope_sigs_ctx)
(scope_name : ScopeName.t)
(sigma : Ast.scope_decl) :
untyped Dcalc.Ast.naked_expr scope_body Bindlib.box * struct_ctx =
untyped Dcalc.Ast.expr scope_body Bindlib.box * struct_ctx =
let sigma_info = ScopeName.get_info sigma.scope_decl_name in
let scope_sig = Ast.ScopeMap.find sigma.scope_decl_name sctx in
let scope_variables = scope_sig.scope_sig_local_vars in
@ -850,7 +849,7 @@ let translate_program (prgm : Ast.program) :
in
(* the resulting expression is the list of definitions of all the scopes,
ending with the top-level scope. *)
let (scopes, decl_ctx) : untyped Dcalc.Ast.naked_expr scopes Bindlib.box * _ =
let (scopes, decl_ctx) : untyped Dcalc.Ast.expr scopes Bindlib.box * _ =
List.fold_right
(fun scope_name (scopes, decl_ctx) ->
let scope = Ast.ScopeMap.find scope_name prgm.program_scopes in

66
compiler/shared_ast/definitions.ml
View File

@ -178,7 +178,8 @@ type ('a, 't) gexpr = (('a, 't) naked_gexpr, 't) Marked.t
(** General expressions: groups all expression cases of the different ASTs, and
uses a GADT to eliminate irrelevant cases for each one. The ['t] annotations
are also totally unconstrained at this point. The dcalc exprs, for example,
are then defined with [type naked_expr = dcalc naked_gexpr] plus the annotations.
are then defined with [type naked_expr = dcalc naked_gexpr] plus the
annotations.
A few tips on using this GADT:
@ -187,14 +188,10 @@ type ('a, 't) gexpr = (('a, 't) naked_gexpr, 't) Marked.t
- For recursive functions, you may need to additionally explicit the
generalisation of the variable: [let rec f: type a . a naked_gexpr -> ...] *)
(** The expressions use the {{:https://lepigre.fr/ocaml-bindlib/} Bindlib}
library, based on higher-order abstract syntax *)
and ('a, 't) naked_gexpr =
(* Constructors common to all ASTs *)
| ELit : 'a glit -> ('a any, 't) naked_gexpr
| EApp :
('a, 't) gexpr * ('a, 't) gexpr list
-> ('a any, 't) naked_gexpr
| EApp : ('a, 't) gexpr * ('a, 't) gexpr list -> ('a any, 't) naked_gexpr
| EOp : operator -> ('a any, 't) naked_gexpr
| EArray : ('a, 't) gexpr list -> ('a any, 't) naked_gexpr
(* All but statement calculus *)
@ -208,7 +205,9 @@ and ('a, 't) naked_gexpr =
('a, 't) gexpr * ('a, 't) gexpr * ('a, 't) gexpr
-> (([< desugared | scopelang | dcalc | lcalc ] as 'a), 't) naked_gexpr
(* Early stages *)
| ELocation : 'a glocation -> (([< desugared | scopelang ] as 'a), 't) naked_gexpr
| ELocation :
'a glocation
-> (([< desugared | scopelang ] as 'a), 't) naked_gexpr
| EStruct :
StructName.t * ('a, 't) gexpr StructFieldMap.t
-> (([< desugared | scopelang ] as 'a), 't) naked_gexpr
@ -219,9 +218,7 @@ and ('a, 't) naked_gexpr =
('a, 't) gexpr * EnumConstructor.t * EnumName.t
-> (([< desugared | scopelang ] as 'a), 't) naked_gexpr
| EMatchS :
('a, 't) gexpr
* EnumName.t
* ('a, 't) gexpr EnumConstructorMap.t
('a, 't) gexpr * EnumName.t * ('a, 't) gexpr EnumConstructorMap.t
-> (([< desugared | scopelang ] as 'a), 't) naked_gexpr
(* Lambda-like *)
| ETuple :
@ -250,6 +247,13 @@ and ('a, 't) naked_gexpr =
('a, 't) gexpr * except * ('a, 't) gexpr
-> ((lcalc as 'a), 't) naked_gexpr
type 'a box = 'a Bindlib.box
type ('e, 'b) binder = (('a, 't) naked_gexpr, 'b) Bindlib.binder
constraint 'e = ('a, 't) gexpr
(** The expressions use the {{:https://lepigre.fr/ocaml-bindlib/} Bindlib}
library, based on higher-order abstract syntax *)
(* (\* Statement calculus *\)
* | ESVar: LocalName.t -> (scalc as 'a, 't) naked_gexpr
* | ESStruct: ('a, 't) gexpr list * StructName.t -> (scalc as 'a, 't) naked_gexpr
@ -257,7 +261,7 @@ and ('a, 't) naked_gexpr =
* | ESInj: ('a, 't) gexpr * EnumConstructor.t * EnumName.t -> (scalc as 'a, 't) naked_gexpr
* | ESFunc: TopLevelName.t -> (scalc as 'a, 't) naked_gexpr *)
type 'e anyexpr = 'e constraint 'e = (_ any, _) naked_gexpr
type 'e anyexpr = 'e constraint 'e = (_ any, _) gexpr
(** Shorter alias for functions taking any kind of expression *)
(** {2 Markings} *)
@ -268,27 +272,21 @@ type typed = { pos : Pos.t; ty : typ }
(** The generic type of AST markings. Using a GADT allows functions to be
polymorphic in the marking, but still do transformations on types when
appropriate. Expected to fill the ['t] parameter of [naked_gexpr] and
[gexpr] (a ['t] annotation different from this type is used in the
middle of the typing processing, but all visible ASTs should otherwise use
this. *)
[gexpr] (a ['t] annotation different from this type is used in the middle of
the typing processing, but all visible ASTs should otherwise use this. *)
type _ mark = Untyped : untyped -> untyped mark | Typed : typed -> typed mark
type 'e marked = ('e, 'm mark) Marked.t constraint 'e = ('a, 'm mark) naked_gexpr
(** [('a, 't) naked_gexpr marked] is equivalent to [('a, 'm mark) gexpr] but
often more convenient to write since we generally use the type of
expressions ['e = (_, _ mark) naked_gexpr] as type parameter. *)
(** Useful for errors and printing, for example *)
type any_marked_expr =
| AnyExpr : (_ any, _ mark) gexpr -> any_marked_expr
type any_marked_expr = AnyExpr : (_ any, _ mark) gexpr -> any_marked_expr
(** {2 Higher-level program structure} *)
(** Constructs scopes and programs on top of expressions. The ['e] type
parameter throughout is expected to match instances of the [naked_gexpr] type
defined above. Markings are constrained to the [mark] GADT defined above.
Note that this structure is at the moment only relevant for [dcalc] and
[lcalc], as [scopelang] has its own scope structure, as the name implies. *)
parameter throughout is expected to match instances of the [naked_gexpr]
type defined above. Markings are constrained to the [mark] GADT defined
above. Note that this structure is at the moment only relevant for [dcalc]
and [lcalc], as [scopelang] has its own scope structure, as the name
implies. *)
(** This kind annotation signals that the let-binding respects a structural
invariant. These invariants concern the shape of the expression in the
@ -306,11 +304,11 @@ type scope_let_kind =
type 'e scope_let = {
scope_let_kind : scope_let_kind;
scope_let_typ : typ;
scope_let_expr : 'e marked;
scope_let_next : ('e, 'e scope_body_expr) Bindlib.binder;
scope_let_expr : 'e;
scope_let_next : ('e, 'e scope_body_expr) binder;
scope_let_pos : Pos.t;
}
constraint 'e = ('a, 'm mark) naked_gexpr
constraint 'e = ('a, 'm mark) gexpr
(** This type is parametrized by the expression type so it can be reused in
later intermediate representations. *)
@ -318,15 +316,16 @@ type 'e scope_let = {
let-binding expression, plus an annotation for the kind of the let-binding
that comes from the compilation of a {!module: Scopelang.Ast} statement. *)
and 'e scope_body_expr =
| Result of 'e marked
| Result of 'e
| ScopeLet of 'e scope_let
constraint 'e = ('a, 'm mark) naked_gexpr
constraint 'e = (_, _ mark) gexpr
type 'e scope_body = {
scope_body_input_struct : StructName.t;
scope_body_output_struct : StructName.t;
scope_body_expr : ('e, 'e scope_body_expr) Bindlib.binder;
scope_body_expr : ('e, 'e scope_body_expr) binder;
}
constraint 'e = (_, _ mark) gexpr
(** Instead of being a single expression, we give a little more ad-hoc structure
to the scope body by decomposing it in an ordered list of let-bindings, and
a result expression that uses the let-binded variables. The first binder is
@ -335,15 +334,16 @@ type 'e scope_body = {
type 'e scope_def = {
scope_name : ScopeName.t;
scope_body : 'e scope_body;
scope_next : ('e, 'e scopes) Bindlib.binder;
scope_next : ('e, 'e scopes) binder;
}
constraint 'e = (_, _ mark) gexpr
(** Finally, we do the same transformation for the whole program for the kinded
lets. This permit us to use bindlib variables for scopes names. *)
and 'e scopes =
| Nil
| ScopeDef of 'e scope_def
constraint 'e = ('a, 'm mark) naked_gexpr
constraint 'e = (_, _ mark) gexpr
type struct_ctx = (StructFieldName.t * typ) list StructMap.t
type enum_ctx = (EnumConstructor.t * typ) list EnumMap.t

18
compiler/shared_ast/expr.ml
View File

@ -18,8 +18,6 @@
open Utils
open Definitions
type 'a box = 'a Bindlib.box
(** Functions handling the types of [shared_ast] *)
(* Basic block constructors *)
@ -108,11 +106,8 @@ let with_ty (type m) (ty : typ) (x : ('a, m mark) Marked.t) :
| Typed m -> Typed { m with ty })
(Marked.unmark x)
let map_mark
(type m)
(pos_f : Pos.t -> Pos.t)
(ty_f : typ -> typ)
(m : m mark) : m mark =
let map_mark (type m) (pos_f : Pos.t -> Pos.t) (ty_f : typ -> typ) (m : m mark)
: m mark =
match m with
| Untyped { pos } -> Untyped { pos = pos_f pos }
| Typed { pos; ty } -> Typed { pos = pos_f pos; ty = ty_f ty }
@ -283,7 +278,7 @@ let make_default exceptions just cons mark =
(* Tests *)
let is_value (type a) (e : (a, 'm mark) naked_gexpr marked) =
let is_value (type a) (e : (a, _) gexpr) =
match Marked.unmark e with
| ELit _ | EAbs _ | EOp _ | ERaise _ -> true
| _ -> false
@ -532,8 +527,7 @@ let compare_except ex1 ex2 = Stdlib.compare ex1 ex2
(* weird indentation; see
https://github.com/ocaml-ppx/ocamlformat/issues/2143 *)
let rec equal_list :
'a. ('a, 't) gexpr list -> ('a, 't) gexpr list -> bool =
let rec equal_list : 'a. ('a, 't) gexpr list -> ('a, 't) gexpr list -> bool =
fun es1 es2 ->
try List.for_all2 equal es1 es2 with Invalid_argument _ -> false
@ -683,7 +677,7 @@ let rec compare : type a. (a, _) gexpr -> (a, _) gexpr -> int =
| ERaise _, _ -> -1 | _, ERaise _ -> 1
| ECatch _, _ -> . | _, ECatch _ -> .
let rec free_vars : type a. (a, 't) naked_gexpr marked -> (a, 't) naked_gexpr Var.Set.t =
let rec free_vars : type a. (a, 't) gexpr -> (a, 't) gexpr Var.Set.t =
fun e ->
match Marked.unmark e with
| EOp _ | ELit _ | ERaise _ -> Var.Set.empty
@ -733,7 +727,7 @@ let remove_logging_calls e =
let format ?debug decl_ctx ppf e = Print.naked_expr ?debug decl_ctx ppf e
let rec size : type a. (a, 't) naked_gexpr marked -> int =
let rec size : type a. (a, 't) gexpr -> int =
fun e ->
match Marked.unmark e with
| EVar _ | ELit _ | EOp _ -> 1

72
compiler/shared_ast/expr.mli
View File

@ -20,12 +20,10 @@
open Utils
open Definitions
type 'a box = 'a Bindlib.box
(** {2 Boxed constructors} *)
val box : ('a, 't) gexpr -> ('a, 't) gexpr box
val evar : ('a, 't) naked_gexpr Bindlib.var -> 't -> ('a, 't) gexpr box
val evar : ('a, 't) gexpr Var.t -> 't -> ('a, 't) gexpr box
val etuple :
(([< dcalc | lcalc ] as 'a), 't) gexpr box list ->
@ -56,11 +54,7 @@ val ematch :
't ->
('a, 't) gexpr box
val earray :
('a any, 't) gexpr box list ->
't ->
('a, 't) gexpr box
val earray : ('a any, 't) gexpr box list -> 't -> ('a, 't) gexpr box
val elit : 'a any glit -> 't -> ('a, 't) gexpr box
val eabs :
@ -70,15 +64,10 @@ val eabs :
('a, 't) gexpr box
val eapp :
('a any, 't) gexpr box ->
('a, 't) gexpr box list ->
't ->
('a, 't) gexpr box
('a any, 't) gexpr box -> ('a, 't) gexpr box list -> 't -> ('a, 't) gexpr box
val eassert :
(([< dcalc | lcalc ] as 'a), 't) gexpr box ->
't ->
('a, 't) gexpr box
(([< dcalc | lcalc ] as 'a), 't) gexpr box -> 't -> ('a, 't) gexpr box
val eop : operator -> 't -> (_ any, 't) gexpr box
@ -114,12 +103,10 @@ val eraise : except -> 't -> (lcalc, 't) gexpr box
val no_mark : 'm mark -> 'm mark
val mark_pos : 'm mark -> Pos.t
val pos : ('e, _) naked_gexpr marked -> Pos.t
val pos : ('e, _ mark) gexpr -> Pos.t
val ty : (_, typed mark) Marked.t -> typ
val with_ty : typ -> ('a, _ mark) Marked.t -> ('a, typed mark) Marked.t
val map_mark :
(Pos.t -> Pos.t) -> (typ -> typ) -> 'm mark -> 'm mark
val map_mark : (Pos.t -> Pos.t) -> (typ -> typ) -> 'm mark -> 'm mark
val map_mark2 :
(Pos.t -> Pos.t -> Pos.t) ->
@ -131,8 +118,7 @@ val map_mark2 :
val fold_marks :
(Pos.t list -> Pos.t) -> (typed list -> typ) -> 'm mark list -> 'm mark
val untype :
('a, 'm mark) gexpr -> ('a, untyped mark) gexpr box
val untype : ('a, 'm mark) gexpr -> ('a, untyped mark) gexpr box
(** {2 Traversal functions} *)
@ -168,39 +154,38 @@ val map_top_down :
returned by [f] is hybrid since the mark at top-level has been rewritten,
but not yet the marks in the subtrees. *)
val map_marks :
f:('t1 -> 't2) -> ('a, 't1) gexpr -> ('a, 't2) gexpr box
val map_marks : f:('t1 -> 't2) -> ('a, 't1) gexpr -> ('a, 't2) gexpr box
(** {2 Expression building helpers} *)
val make_var : 'a Bindlib.var * 'b -> ('a * 'b) box
val make_var : ('a, 't) gexpr Var.t * 'b -> (('a, 't) naked_gexpr * 'b) box
val make_abs :
('a, 't) naked_gexpr Var.vars ->
('a, 't) gexpr Var.vars ->
('a, 't) gexpr box ->
typ list ->
't ->
('a, 't) gexpr box
val make_app :
((_ any, 'm mark) naked_gexpr as 'e) marked box ->
'e marked box list ->
('a any, 'm mark) gexpr box ->
('a, 'm mark) gexpr box list ->
'm mark ->
'e marked box
('a, 'm mark) gexpr box
val empty_thunked_term :
'm mark -> ([< dcalc | desugared | scopelang ], 'm mark) naked_gexpr marked
'm mark -> ([< dcalc | desugared | scopelang ], 'm mark) gexpr
val make_let_in :
'e Bindlib.var ->
('a, 'm mark) gexpr Var.t ->
typ ->
'e anyexpr marked box ->
'e marked box ->
('a, 'm mark) gexpr box ->
('a, 'm mark) gexpr box ->
Utils.Pos.t ->
'e marked box
('a, 'm mark) gexpr box
val make_let_in_raw :
('a any, 't) naked_gexpr Bindlib.var ->
('a, 't) gexpr Var.t ->
typ ->
('a, 't) gexpr box ->
('a, 't) gexpr box ->
@ -209,12 +194,12 @@ val make_let_in_raw :
(** Version with any mark; to be removed once we use the [mark] type everywhere. *)
val make_multiple_let_in :
'e Var.vars ->
('a, 'm mark) gexpr Var.vars ->
typ list ->
'e marked box list ->
'e marked box ->
('a, 'm mark) gexpr box list ->
('a, 'm mark) gexpr box ->
Pos.t ->
'e marked box
('a, 'm mark) gexpr box
val make_default :
(([< desugared | scopelang | dcalc ] as 'a), 't) gexpr list ->
@ -237,8 +222,7 @@ val make_default :
(** {2 Transformations} *)
val remove_logging_calls :
((_ any, 't) naked_gexpr as 'e) marked -> 'e marked box
val remove_logging_calls : ('a any, 't) gexpr -> ('a, 't) gexpr box
(** Removes all calls to [Log] unary operators in the AST, replacing them by
their argument. *)
@ -246,7 +230,7 @@ val format :
?debug:bool (** [true] for debug printing *) ->
decl_ctx ->
Format.formatter ->
'e marked ->
(_, _ mark) gexpr ->
unit
(** {2 Analysis and tests} *)
@ -264,8 +248,8 @@ val compare : ('a, 't) gexpr -> ('a, 't) gexpr -> int
information *)
val compare_typ : typ -> typ -> int
val is_value : (_ any, 'm mark) naked_gexpr marked -> bool
val free_vars : 'e marked -> 'e Var.Set.t
val is_value : ('a any, 't) gexpr -> bool
val free_vars : ('a any, 't) gexpr -> ('a, 't) gexpr Var.Set.t
val size : (_ any, 't) naked_gexpr marked -> int
val size : ('a, 't) gexpr -> int
(** Used by the optimizer to know when to stop *)

30
compiler/shared_ast/print.ml
View File

@ -213,11 +213,8 @@ let needs_parens (type a) (e : (a, _) gexpr) : bool =
let rec naked_expr :
'a.
?debug:bool ->
decl_ctx ->
Format.formatter ->
('a, 't) gexpr ->
unit =
?debug:bool -> decl_ctx -> Format.formatter -> ('a, 't) gexpr -> unit
=
fun (type a) ?(debug : bool = false) (ctx : decl_ctx) (fmt : Format.formatter)
(e : (a, 't) gexpr) ->
let naked_expr e = naked_expr ~debug ctx e in
@ -257,8 +254,8 @@ let rec naked_expr :
match s with
| None -> Format.fprintf fmt "%a%a%d" naked_expr e1 punctuation "." n
| Some s ->
Format.fprintf fmt "%a%a%a%a%a" naked_expr e1 operator "." punctuation "\""
StructFieldName.format_t
Format.fprintf fmt "%a%a%a%a%a" naked_expr e1 operator "." punctuation
"\"" StructFieldName.format_t
(fst (List.nth (StructMap.find s ctx.ctx_structs) n))
punctuation "\"")
| EInj (e, n, en, _ts) ->
@ -303,7 +300,8 @@ let rec naked_expr :
| EApp ((EOp (Binop op), _), [arg1; arg2]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@]" with_parens arg1 binop op
with_parens arg2
| EApp ((EOp (Unop (Log _)), _), [arg1]) when not debug -> naked_expr fmt arg1
| EApp ((EOp (Unop (Log _)), _), [arg1]) when not debug ->
naked_expr fmt arg1
| EApp ((EOp (Unop op), _), [arg1]) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" unop op with_parens arg1
| EApp (f, args) ->
@ -313,22 +311,22 @@ let rec naked_expr :
with_parens)
args
| EIfThenElse (e1, e2, e3) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@ %a@ %a@ %a@]" keyword "if" naked_expr e1
keyword "then" naked_expr e2 keyword "else" naked_expr e3
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@ %a@ %a@ %a@]" keyword "if"
naked_expr e1 keyword "then" naked_expr e2 keyword "else" naked_expr e3
| EOp (Ternop op) -> Format.fprintf fmt "%a" ternop op
| EOp (Binop op) -> Format.fprintf fmt "%a" binop op
| EOp (Unop op) -> Format.fprintf fmt "%a" unop op
| EDefault (exceptions, just, cons) ->
if List.length exceptions = 0 then
Format.fprintf fmt "@[<hov 2>%a%a@ %a@ %a%a@]" punctuation "⟨" naked_expr just
punctuation "⊢" naked_expr cons punctuation "⟩"
Format.fprintf fmt "@[<hov 2>%a%a@ %a@ %a%a@]" punctuation "⟨" naked_expr
just punctuation "⊢" naked_expr cons punctuation "⟩"
else
Format.fprintf fmt "@[<hov 2>%a%a@ %a@ %a@ %a@ %a%a@]" punctuation "⟨"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "%a@ " punctuation ",")
naked_expr)
exceptions punctuation "|" naked_expr just punctuation "⊢" naked_expr cons
punctuation "⟩"
exceptions punctuation "|" naked_expr just punctuation "⊢" naked_expr
cons punctuation "⟩"
| ErrorOnEmpty e' ->
Format.fprintf fmt "%a@ %a" operator "error_empty" with_parens e'
| EAssert e' ->
@ -352,8 +350,8 @@ let rec naked_expr :
(StructFieldMap.bindings fields)
punctuation "}"
| EStructAccess (e1, field, _) ->
Format.fprintf fmt "%a%a%a%a%a" naked_expr e1 punctuation "." punctuation "\""
StructFieldName.format_t field punctuation "\""
Format.fprintf fmt "%a%a%a%a%a" naked_expr e1 punctuation "." punctuation
"\"" StructFieldName.format_t field punctuation "\""
| EEnumInj (e1, cons, _) ->
Format.fprintf fmt "%a@ %a" EnumConstructor.format_t cons naked_expr e1
| EMatchS (e1, _, cases) ->

5
compiler/shared_ast/program.ml
View File

@ -22,10 +22,9 @@ let map_exprs ~f ~varf { scopes; decl_ctx } =
(fun scopes -> { scopes; decl_ctx })
(Scope.map_exprs ~f ~varf scopes)
let untype : 'm. ('a, 'm mark) naked_gexpr program -> ('a, untyped mark) naked_gexpr program
let untype : 'm. ('a, 'm mark) gexpr program -> ('a, untyped mark) gexpr program
=
fun (prg : ('a, 'm mark) naked_gexpr program) ->
Bindlib.unbox (map_exprs ~f:Expr.untype ~varf:Var.translate prg)
fun prg -> Bindlib.unbox (map_exprs ~f:Expr.untype ~varf:Var.translate prg)
let rec find_scope name vars = function
| Nil -> raise Not_found

14
compiler/shared_ast/program.mli
View File

@ -20,19 +20,17 @@ open Definitions
(** {2 Transformations} *)
val map_exprs :
f:('expr1 marked -> 'expr2 marked Bindlib.box) ->
varf:('expr1 Bindlib.var -> 'expr2 Bindlib.var) ->
f:('expr1 -> 'expr2 box) ->
varf:('expr1 Var.t -> 'expr2 Var.t) ->
'expr1 program ->
'expr2 program Bindlib.box
'expr2 program box
val untype :
(([< dcalc | lcalc ] as 'a), 'm mark) naked_gexpr program ->
('a, untyped mark) naked_gexpr program
(([< dcalc | lcalc ] as 'a), 'm mark) gexpr program ->
('a, untyped mark) gexpr program
val to_expr :
(([< dcalc | lcalc ], _) naked_gexpr as 'e) program ->
ScopeName.t ->
'e marked Bindlib.box
(([< dcalc | lcalc ], _) gexpr as 'e) program -> ScopeName.t -> 'e box
(** Usage: [build_whole_program_expr program main_scope] builds an expression
corresponding to the main program and returning the main scope as a
function. *)

10
compiler/shared_ast/scope.ml
View File

@ -97,7 +97,7 @@ let get_body_mark scope_body =
| Result e | ScopeLet { scope_let_expr = e; _ } -> Marked.get_mark e
let rec unfold_body_expr (ctx : decl_ctx) (scope_let : 'e scope_body_expr) :
'e marked Bindlib.box =
'e box =
match scope_let with
| Result e -> Expr.box e
| ScopeLet
@ -122,12 +122,10 @@ let build_typ_from_sig
let result_typ = Marked.mark pos (TStruct scope_return_struct_name) in
Marked.mark pos (TArrow (input_typ, result_typ))
type 'e scope_name_or_var =
| ScopeName of ScopeName.t
| ScopeVar of 'e Bindlib.var
type 'e scope_name_or_var = ScopeName of ScopeName.t | ScopeVar of 'e Var.t
let to_expr (ctx : decl_ctx) (body : 'e scope_body) (mark_scope : 'm mark) :
'e marked Bindlib.box =
'e box =
let var, body_expr = Bindlib.unbind body.scope_body_expr in
let body_expr = unfold_body_expr ctx body_expr in
Expr.make_abs [| var |] body_expr
@ -152,7 +150,7 @@ let rec unfold
(ctx : decl_ctx)
(s : 'e scopes)
(mark : 'm mark)
(main_scope : 'naked_expr scope_name_or_var) : 'e marked Bindlib.box =
(main_scope : 'expr scope_name_or_var) : 'e Bindlib.box =
match s with
| Nil -> (
match main_scope with

41
compiler/shared_ast/scope.mli
View File

@ -23,7 +23,7 @@ open Definitions
(** {2 Traversal functions} *)
val fold_left_lets :
f:('a -> 'e scope_let -> 'e Bindlib.var -> 'a) ->
f:('a -> 'e scope_let -> 'e Var.t -> 'a) ->
init:'a ->
'e scope_body_expr ->
'a
@ -33,8 +33,8 @@ val fold_left_lets :
scope lets to be examined. *)
val fold_right_lets :
f:('expr1 scope_let -> 'expr1 Bindlib.var -> 'a -> 'a) ->
init:('expr1 marked -> 'a) ->
f:('expr1 scope_let -> 'expr1 Var.t -> 'a -> 'a) ->
init:('expr1 -> 'a) ->
'expr1 scope_body_expr ->
'a
(** Usage:
@ -43,13 +43,13 @@ val fold_right_lets :
scope lets to be examined (which are before in the program order). *)
val map_exprs_in_lets :
f:('expr1 marked -> 'expr2 marked Bindlib.box) ->
varf:('expr1 Bindlib.var -> 'expr2 Bindlib.var) ->
f:('expr1 -> 'expr2 box) ->
varf:('expr1 Var.t -> 'expr2 Var.t) ->
'expr1 scope_body_expr ->
'expr2 scope_body_expr Bindlib.box
'expr2 scope_body_expr box
val fold_left :
f:('a -> 'expr1 scope_def -> 'expr1 Bindlib.var -> 'a) ->
f:('a -> 'expr1 scope_def -> 'expr1 Var.t -> 'a) ->
init:'a ->
'expr1 scopes ->
'a
@ -58,7 +58,7 @@ val fold_left :
be examined. *)
val fold_right :
f:('expr1 scope_def -> 'expr1 Bindlib.var -> 'a -> 'a) ->
f:('expr1 scope_def -> 'expr1 Var.t -> 'a -> 'a) ->
init:'a ->
'expr1 scopes ->
'a
@ -67,20 +67,17 @@ val fold_right :
where [scope_var] is the variable bound to the scope in the next scopes to
be examined (which are before in the program order). *)
val map :
f:('e scope_def -> 'e scope_def Bindlib.box) ->
'e scopes ->
'e scopes Bindlib.box
val map : f:('e scope_def -> 'e scope_def box) -> 'e scopes -> 'e scopes box
val map_exprs :
f:('expr1 marked -> 'expr2 marked Bindlib.box) ->
varf:('expr1 Bindlib.var -> 'expr2 Bindlib.var) ->
f:('expr1 -> 'expr2 box) ->
varf:('expr1 Var.t -> 'expr2 Var.t) ->
'expr1 scopes ->
'expr2 scopes Bindlib.box
'expr2 scopes box
(** This is the main map visitor for all the expressions inside all the scopes
of the program. *)
val get_body_mark : (_, 'm mark) naked_gexpr scope_body -> 'm mark
val get_body_mark : (_, 'm mark) gexpr scope_body -> 'm mark
(** {2 Conversions} *)
@ -93,22 +90,20 @@ val format :
val to_expr :
decl_ctx ->
((_ any, 'm mark) naked_gexpr as 'e) scope_body ->
('a any, 'm mark) gexpr scope_body ->
'm mark ->
'e marked Bindlib.box
('a, 'm mark) gexpr box
(** Usage: [to_expr ctx body scope_position] where [scope_position] corresponds
to the line of the scope declaration for instance. *)
type 'e scope_name_or_var =
| ScopeName of ScopeName.t
| ScopeVar of 'e Bindlib.var
type 'e scope_name_or_var = ScopeName of ScopeName.t | ScopeVar of 'e Var.t
val unfold :
decl_ctx ->
((_ any, 'm mark) naked_gexpr as 'e) scopes ->
((_, 'm mark) gexpr as 'e) scopes ->
'm mark ->
'e scope_name_or_var ->
'e marked Bindlib.box
'e box
val build_typ_from_sig :
decl_ctx -> StructName.t -> StructName.t -> Pos.t -> typ

11
compiler/shared_ast/var.ml
View File

@ -18,12 +18,13 @@ open Definitions
(** {1 Variables and their collections} *)
(** This module provides types and helpers for Bindlib variables on the [naked_gexpr]
(** This module provides types and helpers for Bindlib variables on the [gexpr]
type *)
type 'e t = 'e anyexpr Bindlib.var
type 'e vars = 'e anyexpr Bindlib.mvar
type 'e binder = ('e, 'e marked) Bindlib.binder
type 'e t = ('a, 't) naked_gexpr Bindlib.var constraint 'e = ('a any, 't) gexpr
type 'e vars = ('a, 't) naked_gexpr Bindlib.mvar
constraint 'e = ('a any, 't) gexpr
let make (name : string) : 'e t = Bindlib.new_var (fun x -> EVar x) name
let compare = Bindlib.compare_vars
@ -36,7 +37,7 @@ type 'e var = 'e t
(* The purpose of this module is just to lift a type parameter outside of
[Set.S] and [Map.S], so that we can have ['e Var.Set.t] for sets of variables
bound to the ['e = ('a, 't) naked_gexpr] expression type. This is made possible by
bound to the ['e = ('a, 't) gexpr] expression type. This is made possible by
the fact that [Bindlib.compare_vars] is polymorphic in that parameter; we
first hide that parameter inside an existential, then re-add a phantom type
outside of the set to ensure consistency. Extracting the elements is then

9
compiler/shared_ast/var.mli
View File

@ -18,12 +18,13 @@ open Definitions
(** {1 Variables and their collections} *)
(** This module provides types and helpers for Bindlib variables on the [naked_gexpr]
(** This module provides types and helpers for Bindlib variables on the [gexpr]
type *)
type 'e t = 'e anyexpr Bindlib.var
type 'e vars = 'e anyexpr Bindlib.mvar
type 'e binder = ('e, 'e marked) Bindlib.binder
type 'e t = ('a, 't) naked_gexpr Bindlib.var constraint 'e = ('a any, 't) gexpr
type 'e vars = ('a, 't) naked_gexpr Bindlib.mvar
constraint 'e = ('a any, 't) gexpr
val make : string -> 'e t
val compare : 'e t -> 'e t -> int

1
compiler/surface/ast.ml
View File

@ -135,6 +135,7 @@ type func_typ = {
}]
type typ = naked_typ Marked.pos
and naked_typ = Base of base_typ | Func of func_typ
[@@deriving
visitors

9
compiler/surface/desugaring.ml
View File

@ -785,8 +785,7 @@ and disambiguate_match_and_build_expression
(inside_definition_of : Desugared.Ast.ScopeDef.t Marked.pos option)
(ctxt : Name_resolution.context)
(cases : Ast.match_case Marked.pos list) :
Desugared.Ast.expr Bindlib.box EnumConstructorMap.t * EnumName.t
=
Desugared.Ast.expr Bindlib.box EnumConstructorMap.t * EnumName.t =
let create_var = function
| None -> ctxt, Var.make "_"
| Some param ->
@ -799,7 +798,9 @@ and disambiguate_match_and_build_expression
(ctxt : Name_resolution.context)
(case_body : ('a * Pos.t) Bindlib.box)
(e_binder :
(Desugared.Ast.naked_expr, Desugared.Ast.naked_expr * Pos.t) Bindlib.mbinder
( Desugared.Ast.naked_expr,
Desugared.Ast.naked_expr * Pos.t )
Bindlib.mbinder
Bindlib.box) : 'c Bindlib.box =
Bindlib.box_apply2
(fun e_binder case_body ->
@ -948,7 +949,7 @@ let process_default
(scope : ScopeName.t)
(def_key : Desugared.Ast.ScopeDef.t Marked.pos)
(rule_id : Desugared.Ast.RuleName.t)
(param_uid : Desugared.Ast.naked_expr Var.t Marked.pos option)
(param_uid : Desugared.Ast.expr Var.t Marked.pos option)
(precond : Desugared.Ast.expr Bindlib.box option)
(exception_situation : Desugared.Ast.exception_situation)
(label_situation : Desugared.Ast.label_situation)

10
compiler/surface/name_resolution.ml
View File

@ -60,7 +60,7 @@ type var_sig = {
}
type context = {
local_var_idmap : Desugared.Ast.naked_expr Var.t Desugared.Ast.IdentMap.t;
local_var_idmap : Desugared.Ast.expr Var.t Desugared.Ast.IdentMap.t;
(** Inside a definition, local variables can be introduced by functions
arguments or pattern matching *)
scope_idmap : ScopeName.t Desugared.Ast.IdentMap.t;
@ -148,8 +148,7 @@ let belongs_to (ctxt : context) (uid : ScopeVar.t) (scope_uid : ScopeName.t) :
scope.var_idmap
(** Retrieves the type of a scope definition from the context *)
let get_def_typ (ctxt : context) (def : Desugared.Ast.ScopeDef.t) :
typ =
let get_def_typ (ctxt : context) (def : Desugared.Ast.ScopeDef.t) : typ =
match def with
| Desugared.Ast.ScopeDef.SubScopeVar (_, x)
(* we don't need to look at the subscope prefix because [x] is already the uid
@ -249,8 +248,7 @@ let rec process_base_typ
ident)))
(** Process a type (function or not) *)
let process_type (ctxt : context) ((naked_typ, typ_pos) : Ast.typ) :
typ =
let process_type (ctxt : context) ((naked_typ, typ_pos) : Ast.typ) : typ =
match naked_typ with
| Ast.Base base_typ -> process_base_typ ctxt (base_typ, typ_pos)
| Ast.Func { arg_typ; return_typ } ->
@ -321,7 +319,7 @@ let process_item_decl
(** Adds a binding to the context *)
let add_def_local_var (ctxt : context) (name : ident) :
context * Desugared.Ast.naked_expr Var.t =
context * Desugared.Ast.expr Var.t =
let local_var_uid = Var.make name in
let ctxt =
{

4
compiler/surface/name_resolution.mli
View File

@ -60,7 +60,7 @@ type var_sig = {
}
type context = {
local_var_idmap : Desugared.Ast.naked_expr Var.t Desugared.Ast.IdentMap.t;
local_var_idmap : Desugared.Ast.expr Var.t Desugared.Ast.IdentMap.t;
(** Inside a definition, local variables can be introduced by functions
arguments or pattern matching *)
scope_idmap : ScopeName.t Desugared.Ast.IdentMap.t;
@ -120,7 +120,7 @@ val get_def_typ : context -> Desugared.Ast.ScopeDef.t -> typ
val is_def_cond : context -> Desugared.Ast.ScopeDef.t -> bool
val is_type_cond : Ast.typ -> bool
val add_def_local_var : context -> ident -> context * Desugared.Ast.naked_expr Var.t
val add_def_local_var : context -> ident -> context * Desugared.Ast.expr Var.t
(** Adds a binding to the context *)
val get_def_key :

22
compiler/verification/conditions.ml
View File

@ -22,15 +22,15 @@ open Ast
(** {1 Helpers and type definitions}*)
type vc_return = typed expr * (typed naked_expr, typ) Var.Map.t
type vc_return = typed expr * (typed expr, typ) Var.Map.t
(** The return type of VC generators is the VC expression plus the types of any
locally free variable inside that expression. *)
type ctx = {
current_scope_name : ScopeName.t;
decl : decl_ctx;
input_vars : typed naked_expr Var.t list;
scope_variables_typs : (typed naked_expr, typ) Var.Map.t;
input_vars : typed expr Var.t list;
scope_variables_typs : (typed expr, typ) Var.Map.t;
}
let conjunction (args : vc_return list) (mark : typed mark) : vc_return =
@ -74,8 +74,8 @@ let half_product (l1 : 'a list) (l2 : 'b list) : ('a * 'b) list =
variables, or [fun () -> e1] for subscope variables. But what we really want
to analyze is only [e1], so we match this outermost structure explicitely
and have a clean verification condition generator that only runs on [e1] *)
let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : typed expr)
: typed expr =
let match_and_ignore_outer_reentrant_default (ctx : ctx) (e : typed expr) :
typed expr =
match Marked.unmark e with
| ErrorOnEmpty
( EDefault
@ -200,8 +200,8 @@ let rec generate_vc_must_not_return_empty (ctx : ctx) (e : typed expr) :
[b] such that if [b] is true, then [e] will never return a conflict error.
It also returns a map of all the types of locally free variables inside the
expression. *)
let rec generate_vs_must_not_return_confict (ctx : ctx) (e : typed expr)
: vc_return =
let rec generate_vs_must_not_return_confict (ctx : ctx) (e : typed expr) :
vc_return =
let out =
(* See the code of [generate_vc_must_not_return_empty] for a list of invariants on which this
function relies on. *)
@ -287,13 +287,13 @@ type verification_condition = {
(* should have type bool *)
vc_kind : verification_condition_kind;
vc_scope : ScopeName.t;
vc_variable : typed naked_expr Var.t Marked.pos;
vc_free_vars_typ : (typed naked_expr, typ) Var.Map.t;
vc_variable : typed expr Var.t Marked.pos;
vc_free_vars_typ : (typed expr, typ) Var.Map.t;
}
let rec generate_verification_conditions_scope_body_expr
(ctx : ctx)
(scope_body_expr : 'm naked_expr scope_body_expr) :
(scope_body_expr : 'm expr scope_body_expr) :
ctx * verification_condition list =
match scope_body_expr with
| Result _ -> ctx, []
@ -378,7 +378,7 @@ let rec generate_verification_conditions_scope_body_expr
let rec generate_verification_conditions_scopes
(decl_ctx : decl_ctx)
(scopes : 'm naked_expr scopes)
(scopes : 'm expr scopes)
(s : ScopeName.t option) : verification_condition list =
match scopes with
| Nil -> []

4
compiler/verification/conditions.mli
View File

@ -33,8 +33,8 @@ type verification_condition = {
(** This expression should have type [bool]*)
vc_kind : verification_condition_kind;
vc_scope : ScopeName.t;
vc_variable : typed Dcalc.Ast.naked_expr Var.t Marked.pos;
vc_free_vars_typ : (typed Dcalc.Ast.naked_expr, typ) Var.Map.t;
vc_variable : typed Dcalc.Ast.expr Var.t Marked.pos;
vc_free_vars_typ : (typed Dcalc.Ast.expr, typ) Var.Map.t;
(** Types of the locally free variables in [vc_guard]. The types of other
free variables linked to scope variables can be obtained with
[Dcalc.Ast.variable_types]. *)

14
compiler/verification/io.ml
View File

@ -24,8 +24,7 @@ module type Backend = sig
type backend_context
val make_context :
decl_ctx -> (typed naked_expr, typ) Var.Map.t -> backend_context
val make_context : decl_ctx -> (typed expr, typ) Var.Map.t -> backend_context
type vc_encoding
@ -39,9 +38,7 @@ module type Backend = sig
val is_model_empty : model -> bool
val translate_expr :
backend_context ->
typed Dcalc.Ast.expr ->
backend_context * vc_encoding
backend_context -> typed Dcalc.Ast.expr -> backend_context * vc_encoding
end
module type BackendIO = sig
@ -49,15 +46,12 @@ module type BackendIO = sig
type backend_context
val make_context :
decl_ctx -> (typed naked_expr, typ) Var.Map.t -> backend_context
val make_context : decl_ctx -> (typed expr, typ) Var.Map.t -> backend_context
type vc_encoding
val translate_expr :
backend_context ->
typed Dcalc.Ast.expr ->
backend_context * vc_encoding
backend_context -> typed Dcalc.Ast.expr -> backend_context * vc_encoding
type model

16
compiler/verification/io.mli
View File

@ -25,9 +25,7 @@ module type Backend = sig
type backend_context
val make_context :
decl_ctx ->
(typed Dcalc.Ast.naked_expr, typ) Var.Map.t ->
backend_context
decl_ctx -> (typed Dcalc.Ast.expr, typ) Var.Map.t -> backend_context
type vc_encoding
@ -41,9 +39,7 @@ module type Backend = sig
val is_model_empty : model -> bool
val translate_expr :
backend_context ->
typed Dcalc.Ast.expr ->
backend_context * vc_encoding
backend_context -> typed Dcalc.Ast.expr -> backend_context * vc_encoding
end
module type BackendIO = sig
@ -52,16 +48,12 @@ module type BackendIO = sig
type backend_context
val make_context :
decl_ctx ->
(typed Dcalc.Ast.naked_expr, typ) Var.Map.t ->
backend_context
decl_ctx -> (typed Dcalc.Ast.expr, typ) Var.Map.t -> backend_context
type vc_encoding
val translate_expr :
backend_context ->
typed Dcalc.Ast.expr ->
backend_context * vc_encoding
backend_context -> typed Dcalc.Ast.expr -> backend_context * vc_encoding
type model

32
compiler/verification/z3backend.real.ml
View File

@ -27,20 +27,20 @@ type context = {
ctx_decl : decl_ctx;
(* The declaration context from the Catala program, containing information to
precisely pretty print Catala expressions *)
ctx_var : (typed naked_expr, typ) Var.Map.t;
ctx_var : (typed expr, typ) Var.Map.t;
(* A map from Catala variables to their types, needed to create Z3 expressions
of the right sort *)
ctx_funcdecl : (typed naked_expr, FuncDecl.func_decl) Var.Map.t;
ctx_funcdecl : (typed expr, FuncDecl.func_decl) Var.Map.t;
(* A map from Catala function names (represented as variables) to Z3 function
declarations, used to only define once functions in Z3 queries *)
ctx_z3vars : typed naked_expr Var.t StringMap.t;
ctx_z3vars : typed expr Var.t StringMap.t;
(* A map from strings, corresponding to Z3 symbol names, to the Catala
variable they represent. Used when to pretty-print Z3 models when a
counterexample is generated *)
ctx_z3datatypes : Sort.sort EnumMap.t;
(* A map from Catala enumeration names to the corresponding Z3 sort, from
which we can retrieve constructors and accessors *)
ctx_z3matchsubsts : (typed naked_expr, Expr.expr) Var.Map.t;
ctx_z3matchsubsts : (typed expr, Expr.expr) Var.Map.t;
(* A map from Catala temporary variables, generated when translating a match,
to the corresponding enum accessor call as a Z3 expression *)
ctx_z3structs : Sort.sort StructMap.t;
@ -66,14 +66,14 @@ type context = {
(** [add_funcdecl] adds the mapping between the Catala variable [v] and the Z3
function declaration [fd] to the context **)
let add_funcdecl
(v : typed naked_expr Var.t)
(v : typed expr Var.t)
(fd : FuncDecl.func_decl)
(ctx : context) : context =
{ ctx with ctx_funcdecl = Var.Map.add v fd ctx.ctx_funcdecl }
(** [add_z3var] adds the mapping between [name] and the Catala variable [v] to
the context **)
let add_z3var (name : string) (v : typed naked_expr Var.t) (ctx : context) : context =
let add_z3var (name : string) (v : typed expr Var.t) (ctx : context) : context =
{ ctx with ctx_z3vars = StringMap.add name v ctx.ctx_z3vars }
(** [add_z3enum] adds the mapping between the Catala enumeration [enum] and the
@ -84,7 +84,7 @@ let add_z3enum (enum : EnumName.t) (sort : Sort.sort) (ctx : context) : context
(** [add_z3var] adds the mapping between temporary variable [v] and the Z3
expression [e] representing an accessor application to the context **)
let add_z3matchsubst (v : typed naked_expr Var.t) (e : Expr.expr) (ctx : context) :
let add_z3matchsubst (v : typed expr Var.t) (e : Expr.expr) (ctx : context) :
context =
{ ctx with ctx_z3matchsubsts = Var.Map.add v e ctx.ctx_z3matchsubsts }
@ -129,8 +129,7 @@ let nb_days_to_date (nb : int) : string =
(** [print_z3model_expr] pretty-prints the value [e] given by a Z3 model
according to the Catala type [ty], corresponding to [e] **)
let rec print_z3model_expr (ctx : context) (ty : typ) (e : Expr.expr)
: string =
let rec print_z3model_expr (ctx : context) (ty : typ) (e : Expr.expr) : string =
let print_lit (ty : typ_lit) =
match ty with
(* TODO: Print boolean according to current language *)
@ -284,9 +283,7 @@ let rec translate_typ (ctx : context) (t : naked_typ) : context * Sort.sort =
and find_or_create_enum (ctx : context) (enum : EnumName.t) :
context * Sort.sort =
(* Creates a Z3 constructor corresponding to the Catala constructor [c] *)
let create_constructor
(ctx : context)
(c : EnumConstructor.t * typ) :
let create_constructor (ctx : context) (c : EnumConstructor.t * typ) :
context * Datatype.Constructor.constructor =
let name, ty = c in
let name = Marked.unmark (EnumConstructor.get_info name) in
@ -390,7 +387,7 @@ let translate_lit (ctx : context) (l : lit) : Expr.expr =
corresponding to the variable [v]. If no such function declaration exists
yet, we construct it and add it to the context, thus requiring to return a
new context *)
let find_or_create_funcdecl (ctx : context) (v : typed naked_expr Var.t) :
let find_or_create_funcdecl (ctx : context) (v : typed expr Var.t) :
context * FuncDecl.func_decl =
match Var.Map.find_opt v ctx.ctx_funcdecl with
| Some fd -> ctx, fd
@ -417,10 +414,8 @@ let find_or_create_funcdecl (ctx : context) (v : typed naked_expr Var.t) :
(** [translate_op] returns the Z3 expression corresponding to the application of
[op] to the arguments [args] **)
let rec translate_op
(ctx : context)
(op : operator)
(args : 'm expr list) : context * Expr.expr =
let rec translate_op (ctx : context) (op : operator) (args : 'm expr list) :
context * Expr.expr =
match op with
| Ternop _top ->
let _e1, _e2, _e3 =
@ -810,8 +805,7 @@ module Backend = struct
let make_context
(decl_ctx : decl_ctx)
(free_vars_typ : (typed naked_expr, typ) Var.Map.t) : backend_context
=
(free_vars_typ : (typed expr, typ) Var.Map.t) : backend_context =
let cfg =
(if !Cli.disable_counterexamples then [] else ["model", "true"])
@ ["proof", "false"]