Used shared_ast for scopelang expressions

This commit is contained in:
Louis Gesbert 2022-08-25 12:09:51 +02:00
parent a6702808ef
commit 01cc957b3b
31 changed files with 683 additions and 924 deletions

View File

@ -533,7 +533,7 @@ let interpret_program :
Errors.raise_spanned_error bad_pos
"@[<hv 2>(bug) Result of interpretation doesn't have the \
expected type:@ @[%a@]@]"
(Print.typ ctx) (fst @@ ty))
(Print.typ ctx) ty)
mark_e )
in
match Marked.unmark (evaluate_expr ctx to_interpret) with

View File

@ -27,6 +27,8 @@ module Any =
let to_string _ = "any"
let format_info fmt () = Format.fprintf fmt "any"
let equal _ _ = true
let compare _ _ = 0
end)
()

View File

@ -34,13 +34,6 @@ module LabelName : Uid.Id with type info = Uid.MarkedString.info =
module LabelMap : Map.S with type key = LabelName.t = Map.Make (LabelName)
module LabelSet : Set.S with type elt = LabelName.t = Set.Make (LabelName)
module StateName : Uid.Id with type info = Uid.MarkedString.info =
Uid.Make (Uid.MarkedString) ()
module ScopeVar : Uid.Id with type info = Uid.MarkedString.info =
Uid.Make (Uid.MarkedString) ()
module ScopeVarSet : Set.S with type elt = ScopeVar.t = Set.Make (ScopeVar)
module ScopeVarMap : Map.S with type key = ScopeVar.t = Map.Make (ScopeVar)
@ -132,8 +125,7 @@ and expr =
| EEnumInj of marked_expr * EnumConstructor.t * EnumName.t
| EMatch of marked_expr * EnumName.t * marked_expr EnumConstructorMap.t
| ELit of Dcalc.Ast.lit
| EAbs of
(expr, marked_expr) Bindlib.mbinder * Scopelang.Ast.typ Marked.pos list
| EAbs of (expr, marked_expr) Bindlib.mbinder * typ Marked.pos list
| EApp of marked_expr * marked_expr list
| EOp of operator
| EDefault of marked_expr list * marked_expr * marked_expr
@ -188,9 +180,7 @@ module Expr = struct
| n -> n)
| ELit l1, ELit l2 -> Stdlib.compare l1 l2
| EAbs (binder1, typs1), EAbs (binder2, typs2) -> (
match
list_compare (Marked.compare Scopelang.Ast.Typ.compare) typs1 typs2
with
match list_compare Expr.compare_typ typs1 typs2 with
| 0 ->
let _, (e1, _), (e2, _) = Bindlib.unmbind2 binder1 binder2 in
compare e1 e2
@ -268,7 +258,7 @@ type rule = {
rule_id : RuleName.t;
rule_just : expr Marked.pos Bindlib.box;
rule_cons : expr Marked.pos Bindlib.box;
rule_parameter : (Var.t * Scopelang.Ast.typ Marked.pos) option;
rule_parameter : (Var.t * typ Marked.pos) option;
rule_exception : exception_situation;
rule_label : label_situation;
}
@ -289,8 +279,8 @@ module Rule = struct
let c2, _ = Bindlib.unbox r2.rule_cons in
Expr.compare c1 c2
| n -> n)
| Some (v1, (t1, _)), Some (v2, (t2, _)) -> (
match Scopelang.Ast.Typ.compare t1 t2 with
| Some (v1, t1), Some (v2, t2) -> (
match Shared_ast.Expr.compare_typ t1 t2 with
| 0 -> (
let open Bindlib in
let b1 = unbox (bind_var v1 r1.rule_just) in
@ -308,9 +298,7 @@ module Rule = struct
| Some _, None -> 1
end
let empty_rule
(pos : Pos.t)
(have_parameter : Scopelang.Ast.typ Marked.pos option) : rule =
let empty_rule (pos : Pos.t) (have_parameter : typ Marked.pos option) : rule =
{
rule_just = Bindlib.box (ELit (LBool false), pos);
rule_cons = Bindlib.box (ELit LEmptyError, pos);
@ -323,9 +311,8 @@ let empty_rule
rule_label = Unlabeled;
}
let always_false_rule
(pos : Pos.t)
(have_parameter : Scopelang.Ast.typ Marked.pos option) : rule =
let always_false_rule (pos : Pos.t) (have_parameter : typ Marked.pos option) :
rule =
{
rule_just = Bindlib.box (ELit (LBool true), pos);
rule_cons = Bindlib.box (ELit (LBool false), pos);
@ -348,7 +335,7 @@ type meta_assertion =
type scope_def = {
scope_def_rules : rule RuleMap.t;
scope_def_typ : Scopelang.Ast.typ Marked.pos;
scope_def_typ : typ Marked.pos;
scope_def_is_condition : bool;
scope_def_io : Scopelang.Ast.io;
}
@ -366,8 +353,8 @@ type scope = {
type program = {
program_scopes : scope Scopelang.Ast.ScopeMap.t;
program_enums : Scopelang.Ast.enum_ctx;
program_structs : Scopelang.Ast.struct_ctx;
program_enums : enum_ctx;
program_structs : struct_ctx;
}
let rec locations_used (e : expr Marked.pos) : LocationSet.t =
@ -434,7 +421,7 @@ let make_var ((x, pos) : Var.t Marked.pos) : expr Marked.pos Bindlib.box =
let make_abs
(xs : vars)
(e : expr Marked.pos Bindlib.box)
(taus : Scopelang.Ast.typ Marked.pos list)
(taus : typ Marked.pos list)
(pos : Pos.t) : expr Marked.pos Bindlib.box =
Bindlib.box_apply (fun b -> EAbs (b, taus), pos) (Bindlib.bind_mvar xs e)
@ -446,7 +433,7 @@ let make_app
let make_let_in
(x : Var.t)
(tau : Scopelang.Ast.typ Marked.pos)
(tau : typ Marked.pos)
(e1 : expr Marked.pos Bindlib.box)
(e2 : expr Marked.pos Bindlib.box) : expr Marked.pos Bindlib.box =
Bindlib.box_apply2

View File

@ -28,8 +28,6 @@ module RuleSet : Set.S with type elt = RuleName.t
module LabelName : Uid.Id with type info = Uid.MarkedString.info
module LabelMap : Map.S with type key = LabelName.t
module LabelSet : Set.S with type elt = LabelName.t
module StateName : Uid.Id with type info = Uid.MarkedString.info
module ScopeVar : Uid.Id with type info = Uid.MarkedString.info
module ScopeVarSet : Set.S with type elt = ScopeVar.t
module ScopeVarMap : Map.S with type key = ScopeVar.t
@ -71,8 +69,7 @@ and expr =
| EEnumInj of marked_expr * EnumConstructor.t * EnumName.t
| EMatch of marked_expr * EnumName.t * marked_expr EnumConstructorMap.t
| ELit of Dcalc.Ast.lit
| EAbs of
(expr, marked_expr) Bindlib.mbinder * Scopelang.Ast.typ Marked.pos list
| EAbs of (expr, marked_expr) Bindlib.mbinder * marked_typ list
| EApp of marked_expr * marked_expr list
| EOp of operator
| EDefault of marked_expr list * marked_expr * marked_expr
@ -100,7 +97,7 @@ val make_var : Var.t Marked.pos -> expr Marked.pos Bindlib.box
val make_abs :
vars ->
expr Marked.pos Bindlib.box ->
Scopelang.Ast.typ Marked.pos list ->
typ Marked.pos list ->
Pos.t ->
expr Marked.pos Bindlib.box
@ -112,7 +109,7 @@ val make_app :
val make_let_in :
Var.t ->
Scopelang.Ast.typ Marked.pos ->
typ Marked.pos ->
expr Marked.pos Bindlib.box ->
expr Marked.pos Bindlib.box ->
expr Marked.pos Bindlib.box
@ -130,15 +127,15 @@ type rule = {
rule_id : RuleName.t;
rule_just : expr Marked.pos Bindlib.box;
rule_cons : expr Marked.pos Bindlib.box;
rule_parameter : (Var.t * Scopelang.Ast.typ Marked.pos) option;
rule_parameter : (Var.t * typ Marked.pos) option;
rule_exception : exception_situation;
rule_label : label_situation;
}
module Rule : Set.OrderedType with type t = rule
val empty_rule : Pos.t -> Scopelang.Ast.typ Marked.pos option -> rule
val always_false_rule : Pos.t -> Scopelang.Ast.typ Marked.pos option -> rule
val empty_rule : Pos.t -> typ Marked.pos option -> rule
val always_false_rule : Pos.t -> typ Marked.pos option -> rule
type assertion = expr Marked.pos Bindlib.box
type variation_typ = Increasing | Decreasing
@ -150,7 +147,7 @@ type meta_assertion =
type scope_def = {
scope_def_rules : rule RuleMap.t;
scope_def_typ : Scopelang.Ast.typ Marked.pos;
scope_def_typ : typ Marked.pos;
scope_def_is_condition : bool;
scope_def_io : Scopelang.Ast.io;
}
@ -168,8 +165,8 @@ type scope = {
type program = {
program_scopes : scope Scopelang.Ast.ScopeMap.t;
program_enums : Scopelang.Ast.enum_ctx;
program_structs : Scopelang.Ast.struct_ctx;
program_enums : enum_ctx;
program_structs : struct_ctx;
}
(** {1 Helpers} *)

View File

@ -33,33 +33,29 @@ open Shared_ast
Indeed, during interpretation, subscopes are executed atomically. *)
module Vertex = struct
type t =
| Var of Ast.ScopeVar.t * Ast.StateName.t option
| SubScope of SubScopeName.t
type t = Var of ScopeVar.t * StateName.t option | SubScope of SubScopeName.t
let hash x =
match x with
| Var (x, None) -> Ast.ScopeVar.hash x
| Var (x, Some sx) ->
Int.logxor (Ast.ScopeVar.hash x) (Ast.StateName.hash sx)
| Var (x, None) -> ScopeVar.hash x
| Var (x, Some sx) -> Int.logxor (ScopeVar.hash x) (StateName.hash sx)
| SubScope x -> SubScopeName.hash x
let compare = compare
let equal x y =
match x, y with
| Var (x, None), Var (y, None) -> Ast.ScopeVar.compare x y = 0
| Var (x, None), Var (y, None) -> ScopeVar.compare x y = 0
| Var (x, Some sx), Var (y, Some sy) ->
Ast.ScopeVar.compare x y = 0 && Ast.StateName.compare sx sy = 0
ScopeVar.compare x y = 0 && StateName.compare sx sy = 0
| SubScope x, SubScope y -> SubScopeName.compare x y = 0
| _ -> false
let format_t (fmt : Format.formatter) (x : t) : unit =
match x with
| Var (v, None) -> Ast.ScopeVar.format_t fmt v
| Var (v, None) -> ScopeVar.format_t fmt v
| Var (v, Some sv) ->
Format.fprintf fmt "%a.%a" Ast.ScopeVar.format_t v Ast.StateName.format_t
sv
Format.fprintf fmt "%a.%a" ScopeVar.format_t v StateName.format_t sv
| SubScope v -> SubScopeName.format_t fmt v
end
@ -104,12 +100,11 @@ let check_for_cycle (scope : Ast.scope) (g : ScopeDependencies.t) : unit =
let var_str, var_info =
match v with
| Vertex.Var (v, None) ->
( Format.asprintf "%a" Ast.ScopeVar.format_t v,
Ast.ScopeVar.get_info v )
Format.asprintf "%a" ScopeVar.format_t v, ScopeVar.get_info v
| Vertex.Var (v, Some sv) ->
( Format.asprintf "%a.%a" Ast.ScopeVar.format_t v
Ast.StateName.format_t sv,
Ast.StateName.get_info sv )
( Format.asprintf "%a.%a" ScopeVar.format_t v
StateName.format_t sv,
StateName.get_info sv )
| Vertex.SubScope v ->
( Format.asprintf "%a" SubScopeName.format_t v,
SubScopeName.get_info v )
@ -121,10 +116,10 @@ let check_for_cycle (scope : Ast.scope) (g : ScopeDependencies.t) : unit =
let succ_str =
match succ with
| Vertex.Var (v, None) ->
Format.asprintf "%a" Ast.ScopeVar.format_t v
Format.asprintf "%a" ScopeVar.format_t v
| Vertex.Var (v, Some sv) ->
Format.asprintf "%a.%a" Ast.ScopeVar.format_t v
Ast.StateName.format_t sv
Format.asprintf "%a.%a" ScopeVar.format_t v StateName.format_t
sv
| Vertex.SubScope v ->
Format.asprintf "%a" SubScopeName.format_t v
in
@ -149,7 +144,7 @@ let build_scope_dependencies (scope : Ast.scope) : ScopeDependencies.t =
(* Add all the vertices to the graph *)
let g =
Ast.ScopeVarMap.fold
(fun (v : Ast.ScopeVar.t) var_or_state g ->
(fun (v : ScopeVar.t) var_or_state g ->
match var_or_state with
| Ast.WholeVar -> ScopeDependencies.add_vertex g (Vertex.Var (v, None))
| Ast.States states ->

View File

@ -34,7 +34,7 @@ open Utils
module Vertex : sig
type t =
| Var of Ast.ScopeVar.t * Ast.StateName.t option
| Var of Shared_ast.ScopeVar.t * Shared_ast.StateName.t option
| SubScope of Shared_ast.SubScopeName.t
val format_t : Format.formatter -> t -> unit

View File

@ -23,7 +23,7 @@ computation order. All the graph computations are done using the
The other important piece of work performed by
{!module: Desugared.Desugared_to_scope} is the construction of the default trees
(see {!Dcalc.Ast.EDefault}) from the list of prioritized rules.
(see {!Shared_ast.EDefault}) from the list of prioritized rules.
Related modules:

View File

@ -23,11 +23,11 @@ open Shared_ast
type target_scope_vars =
| WholeVar of ScopeVar.t
| States of (Ast.StateName.t * ScopeVar.t) list
| States of (StateName.t * ScopeVar.t) list
type ctx = {
scope_var_mapping : target_scope_vars Ast.ScopeVarMap.t;
var_mapping : Scopelang.Ast.Var.t Ast.VarMap.t;
var_mapping : Scopelang.Ast.expr Var.t Ast.VarMap.t;
}
let tag_with_log_entry
@ -35,8 +35,7 @@ let tag_with_log_entry
(l : log_entry)
(markings : Utils.Uid.MarkedString.info list) :
Scopelang.Ast.expr Marked.pos =
( Scopelang.Ast.EApp
((Scopelang.Ast.EOp (Unop (Log (l, markings))), Marked.get_mark e), [e]),
( EApp ((EOp (Unop (Log (l, markings))), Marked.get_mark e), [e]),
Marked.get_mark e )
let rec translate_expr (ctx : ctx) (e : Ast.expr Marked.pos) :
@ -54,22 +53,21 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Marked.pos) :
| States states ->
Marked.same_mark_as (snd (List.hd (List.rev states))) s_var
in
Bindlib.box (ELocation (SubScopeVar (s_name, ss_name, new_s_var)), m)
| Ast.ELocation (Ast.ScopeVar (s_var, None)) ->
Bindlib.box
(Scopelang.Ast.ELocation (SubScopeVar (s_name, ss_name, new_s_var)), m)
| Ast.ELocation (ScopeVar (s_var, None)) ->
Bindlib.box
( Scopelang.Ast.ELocation
(ScopeVar
( ELocation
(ScopelangScopeVar
(match
Ast.ScopeVarMap.find (Marked.unmark s_var) ctx.scope_var_mapping
with
| WholeVar new_s_var -> Marked.same_mark_as new_s_var s_var
| States _ -> failwith "should not happen")),
m )
| Ast.ELocation (ScopeVar (s_var, Some state)) ->
| Ast.ELocation (Ast.ScopeVar (s_var, Some state)) ->
Bindlib.box
( Scopelang.Ast.ELocation
(ScopeVar
( ELocation
(ScopelangScopeVar
(match
Ast.ScopeVarMap.find (Marked.unmark s_var) ctx.scope_var_mapping
with
@ -83,30 +81,30 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Marked.pos) :
(Bindlib.box_var (Ast.VarMap.find v ctx.var_mapping))
| EStruct (s_name, fields) ->
Bindlib.box_apply
(fun new_fields -> Scopelang.Ast.EStruct (s_name, new_fields), m)
(fun new_fields -> EStruct (s_name, new_fields), m)
(Scopelang.Ast.StructFieldMapLift.lift_box
(StructFieldMap.map (translate_expr ctx) fields))
| EStructAccess (e1, s_name, f_name) ->
Bindlib.box_apply
(fun new_e1 -> Scopelang.Ast.EStructAccess (new_e1, s_name, f_name), m)
(fun new_e1 -> EStructAccess (new_e1, s_name, f_name), m)
(translate_expr ctx e1)
| EEnumInj (e1, cons, e_name) ->
Bindlib.box_apply
(fun new_e1 -> Scopelang.Ast.EEnumInj (new_e1, cons, e_name), m)
(fun new_e1 -> EEnumInj (new_e1, cons, e_name), m)
(translate_expr ctx e1)
| EMatch (e1, e_name, arms) ->
Bindlib.box_apply2
(fun new_e1 new_arms ->
Scopelang.Ast.EMatch (new_e1, e_name, new_arms), m)
(fun new_e1 new_arms -> EMatchS (new_e1, e_name, new_arms), m)
(translate_expr ctx e1)
(Scopelang.Ast.EnumConstructorMapLift.lift_box
(EnumConstructorMap.map (translate_expr ctx) arms))
| ELit l -> Bindlib.box (Scopelang.Ast.ELit l, m)
| ELit
(( LBool _ | LEmptyError | LInt _ | LRat _ | LMoney _ | LUnit | LDate _
| LDuration _ ) as l) ->
Bindlib.box (ELit l, m)
| EAbs (binder, typs) ->
let vars, body = Bindlib.unmbind binder in
let new_vars =
Array.map (fun var -> Scopelang.Ast.Var.make (Bindlib.name_of var)) vars
in
let new_vars = Array.map (fun var -> Var.make (Bindlib.name_of var)) vars in
let ctx =
List.fold_left2
(fun ctx var new_var ->
@ -114,32 +112,31 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Marked.pos) :
ctx (Array.to_list vars) (Array.to_list new_vars)
in
Bindlib.box_apply
(fun new_binder -> Scopelang.Ast.EAbs (new_binder, typs), m)
(fun new_binder -> EAbs (new_binder, typs), m)
(Bindlib.bind_mvar new_vars (translate_expr ctx body))
| EApp (e1, args) ->
Bindlib.box_apply2
(fun new_e1 new_args -> Scopelang.Ast.EApp (new_e1, new_args), m)
(fun new_e1 new_args -> EApp (new_e1, new_args), m)
(translate_expr ctx e1)
(Bindlib.box_list (List.map (translate_expr ctx) args))
| EOp op -> Bindlib.box (Scopelang.Ast.EOp op, m)
| EOp op -> Bindlib.box (EOp op, m)
| EDefault (excepts, just, cons) ->
Bindlib.box_apply3
(fun new_excepts new_just new_cons ->
Scopelang.Ast.make_default ~pos:m new_excepts new_just new_cons)
Expr.make_default new_excepts new_just new_cons m)
(Bindlib.box_list (List.map (translate_expr ctx) excepts))
(translate_expr ctx just) (translate_expr ctx cons)
| EIfThenElse (e1, e2, e3) ->
Bindlib.box_apply3
(fun new_e1 new_e2 new_e3 ->
Scopelang.Ast.EIfThenElse (new_e1, new_e2, new_e3), m)
(fun new_e1 new_e2 new_e3 -> EIfThenElse (new_e1, new_e2, new_e3), m)
(translate_expr ctx e1) (translate_expr ctx e2) (translate_expr ctx e3)
| EArray args ->
Bindlib.box_apply
(fun new_args -> Scopelang.Ast.EArray new_args, m)
(fun new_args -> EArray new_args, m)
(Bindlib.box_list (List.map (translate_expr ctx) args))
| ErrorOnEmpty e1 ->
Bindlib.box_apply
(fun new_e1 -> Scopelang.Ast.ErrorOnEmpty new_e1, m)
(fun new_e1 -> ErrorOnEmpty new_e1, m)
(translate_expr ctx e1)
(** {1 Rule tree construction} *)
@ -219,9 +216,7 @@ let rec rule_tree_to_expr
| Some new_param -> (
match Ast.VarMap.find_opt new_param ctx.var_mapping with
| None ->
let new_param_scope =
Scopelang.Ast.Var.make (Bindlib.name_of new_param)
in
let new_param_scope = Var.make (Bindlib.name_of new_param) in
{
ctx with
var_mapping = Ast.VarMap.add new_param new_param_scope ctx.var_mapping;
@ -256,17 +251,18 @@ let rec rule_tree_to_expr
let default_containing_base_cases =
Bindlib.box_apply2
(fun base_just_list base_cons_list ->
Scopelang.Ast.make_default
Expr.make_default
(List.map2
(fun base_just base_cons ->
Scopelang.Ast.make_default ~pos:def_pos []
Expr.make_default []
(* Here we insert the logging command that records when a
decision is taken for the value of a variable. *)
(tag_with_log_entry base_just PosRecordIfTrueBool [])
base_cons)
base_cons def_pos)
base_just_list base_cons_list)
(Scopelang.Ast.ELit (LBool false), def_pos)
(Scopelang.Ast.ELit LEmptyError, def_pos))
(ELit (LBool false), def_pos)
(ELit LEmptyError, def_pos)
def_pos)
(Bindlib.box_list (translate_and_unbox_list base_just_list))
(Bindlib.box_list (translate_and_unbox_list base_cons_list))
in
@ -279,9 +275,9 @@ let rec rule_tree_to_expr
let default =
Bindlib.box_apply2
(fun exceptions default_containing_base_cases ->
Scopelang.Ast.make_default exceptions
(Scopelang.Ast.ELit (LBool true), def_pos)
default_containing_base_cases)
Expr.make_default exceptions
(ELit (LBool true), def_pos)
default_containing_base_cases def_pos)
exceptions default_containing_base_cases
in
match is_func, (List.hd base_rules).Ast.rule_parameter with
@ -293,10 +289,10 @@ let rec rule_tree_to_expr
let default =
Bindlib.box_apply
(fun (default : Scopelang.Ast.expr * Pos.t) ->
Scopelang.Ast.ErrorOnEmpty default, def_pos)
ErrorOnEmpty default, def_pos)
default
in
Scopelang.Ast.make_abs
Expr.make_abs
[| Ast.VarMap.find new_param ctx.var_mapping |]
default [typ] def_pos
else default
@ -310,15 +306,13 @@ let translate_def
(ctx : ctx)
(def_info : Ast.ScopeDef.t)
(def : Ast.rule Ast.RuleMap.t)
(typ : Scopelang.Ast.typ Marked.pos)
(typ : typ Marked.pos)
(io : Scopelang.Ast.io)
~(is_cond : bool)
~(is_subscope_var : bool) : Scopelang.Ast.expr Marked.pos =
(* Here, we have to transform this list of rules into a default tree. *)
let is_def_func =
match Marked.unmark typ with
| Scopelang.Ast.TArrow (_, _) -> true
| _ -> false
match Marked.unmark typ with TArrow (_, _) -> true | _ -> false
in
let is_rule_func _ (r : Ast.rule) : bool =
Option.is_some r.Ast.rule_parameter
@ -327,15 +321,15 @@ let translate_def
let all_rules_not_func =
Ast.RuleMap.for_all (fun n r -> not (is_rule_func n r)) def
in
let is_def_func_param_typ : Scopelang.Ast.typ Marked.pos option =
let is_def_func_param_typ : typ Marked.pos option =
if is_def_func && all_rules_func then
match Marked.unmark typ with
| Scopelang.Ast.TArrow (t_param, _) -> Some t_param
| TArrow (t_param, _) -> Some t_param
| _ ->
Errors.raise_spanned_error (Marked.get_mark typ)
"The definitions of %a are function but its type, %a, is not a \
function type"
Ast.ScopeDef.format_t def_info Scopelang.Print.format_typ typ
"The definitions of %a are function but it doesn't have a function \
type"
Ast.ScopeDef.format_t def_info
else if (not is_def_func) && all_rules_not_func then None
else
let spans =
@ -449,7 +443,7 @@ let translate_scope (ctx : ctx) (scope : Ast.scope) : Scopelang.Ast.scope_decl =
redefined. *)
Errors.raise_multispanned_error
(( Some "Incriminated variable:",
Marked.get_mark (Ast.ScopeVar.get_info var) )
Marked.get_mark (ScopeVar.get_info var) )
:: List.map
(fun (rule, _) ->
( Some "Incriminated variable definition:",
@ -477,7 +471,7 @@ let translate_scope (ctx : ctx) (scope : Ast.scope) : Scopelang.Ast.scope_decl =
in
[
Scopelang.Ast.Definition
( ( Scopelang.Ast.ScopeVar
( ( ScopelangScopeVar
( scope_var,
Marked.get_mark (ScopeVar.get_info scope_var) ),
Marked.get_mark (ScopeVar.get_info scope_var) ),
@ -531,8 +525,8 @@ let translate_scope (ctx : ctx) (scope : Ast.scope) : Scopelang.Ast.scope_decl =
(( Some "Incriminated subscope:",
Ast.ScopeDef.get_position def_key )
:: ( Some "Incriminated variable:",
Marked.get_mark
(Ast.ScopeVar.get_info sub_scope_var) )
Marked.get_mark (ScopeVar.get_info sub_scope_var)
)
:: List.map
(fun (rule, _) ->
( Some
@ -549,8 +543,7 @@ let translate_scope (ctx : ctx) (scope : Ast.scope) : Scopelang.Ast.scope_decl =
( Some "Incriminated subscope:",
Ast.ScopeDef.get_position def_key );
( Some "Incriminated variable:",
Marked.get_mark
(Ast.ScopeVar.get_info sub_scope_var) );
Marked.get_mark (ScopeVar.get_info sub_scope_var) );
]
"This subscope variable is a mandatory input but no \
definition was provided."
@ -567,10 +560,10 @@ let translate_scope (ctx : ctx) (scope : Ast.scope) : Scopelang.Ast.scope_decl =
scope.scope_sub_scopes
in
let var_pos =
Marked.get_mark (Ast.ScopeVar.get_info sub_scope_var)
Marked.get_mark (ScopeVar.get_info sub_scope_var)
in
Scopelang.Ast.Definition
( ( Scopelang.Ast.SubScopeVar
( ( SubScopeVar
( subscop_real_name,
(sub_scope_index, var_pos),
match
@ -630,7 +623,7 @@ let translate_scope (ctx : ctx) (scope : Ast.scope) : Scopelang.Ast.scope_decl =
interesting. We need to create as many Scopelang.Var entries in the
scope signature as there are states. *)
List.fold_left
(fun acc (state : Ast.StateName.t) ->
(fun acc (state : StateName.t) ->
let scope_def =
Ast.ScopeDefMap.find
(Ast.ScopeDef.Var (var, Some state))
@ -668,7 +661,7 @@ let translate_program (pgrm : Ast.program) : Scopelang.Ast.program =
ctx with
scope_var_mapping =
Ast.ScopeVarMap.add scope_var
(WholeVar (ScopeVar.fresh (Ast.ScopeVar.get_info scope_var)))
(WholeVar (ScopeVar.fresh (ScopeVar.get_info scope_var)))
ctx.scope_var_mapping;
}
| States states ->
@ -682,10 +675,9 @@ let translate_program (pgrm : Ast.program) : Scopelang.Ast.program =
( state,
ScopeVar.fresh
(let state_name, state_pos =
Ast.StateName.get_info state
StateName.get_info state
in
( Marked.unmark
(Ast.ScopeVar.get_info scope_var)
( Marked.unmark (ScopeVar.get_info scope_var)
^ "_"
^ state_name,
state_pos )) ))
@ -702,6 +694,6 @@ let translate_program (pgrm : Ast.program) : Scopelang.Ast.program =
{
Scopelang.Ast.program_scopes =
Scopelang.Ast.ScopeMap.map (translate_scope ctx) pgrm.program_scopes;
Scopelang.Ast.program_structs = pgrm.program_structs;
Scopelang.Ast.program_enums = pgrm.program_enums;
Scopelang.Ast.program_ctx =
{ ctx_structs = pgrm.program_structs; ctx_enums = pgrm.program_enums };
}

View File

@ -170,12 +170,12 @@ let driver source_file (options : Cli.options) : int =
@@ fun fmt ->
if Option.is_some options.ex_scope then
Format.fprintf fmt "%a\n"
(Scopelang.Print.format_scope ~debug:options.debug)
(Scopelang.Print.scope prgm.program_ctx ~debug:options.debug)
( scope_uid,
Scopelang.Ast.ScopeMap.find scope_uid prgm.program_scopes )
else
Format.fprintf fmt "%a\n"
(Scopelang.Print.format_program ~debug:options.debug)
(Scopelang.Print.program ~debug:options.debug)
prgm
| ( `Interpret | `Typecheck | `OCaml | `Python | `Scalc | `Lcalc | `Dcalc
| `Proof | `Plugin _ ) as backend -> (

View File

@ -23,17 +23,6 @@ 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. *)
let translate_lit (l : D.lit) : 'm A.expr =
match l with
| LBool l -> ELit (LBool l)
| LInt i -> ELit (LInt i)
| LRat r -> ELit (LRat r)
| LMoney m -> ELit (LMoney m)
| LUnit -> ELit LUnit
| LDate d -> ELit (LDate d)
| LDuration d -> ELit (LDuration d)
| LEmptyError -> ERaise EmptyError
let thunk_expr (e : 'm A.marked_expr Bindlib.box) (mark : 'm mark) :
'm A.marked_expr Bindlib.box =
let dummy_var = Var.make "_" in
@ -78,7 +67,11 @@ and translate_expr (ctx : 'm ctx) (e : 'm D.marked_expr) :
en (Marked.get_mark e)
| EArray es ->
Expr.earray (List.map (translate_expr ctx) es) (Marked.get_mark e)
| ELit l -> Bindlib.box (Marked.same_mark_as (translate_lit l) e)
| ELit
((LBool _ | LInt _ | LRat _ | LMoney _ | LUnit | LDate _ | LDuration _) as
l) ->
Bindlib.box (Marked.same_mark_as (ELit l) e)
| ELit LEmptyError -> Bindlib.box (Marked.same_mark_as (ERaise EmptyError) e)
| EOp op -> Expr.eop op (Marked.get_mark e)
| EIfThenElse (e1, e2, e3) ->
Expr.eifthenelse (translate_expr ctx e1) (translate_expr ctx e2)

View File

@ -137,20 +137,6 @@ let rec translate_typ (tau : typ Marked.pos) : typ Marked.pos =
| TArrow (t1, t2) -> TArrow (translate_typ t1, translate_typ t2)
end
let translate_lit (l : D.lit) (pos : Pos.t) : A.lit =
match l with
| LBool l -> LBool l
| LInt i -> LInt i
| LRat r -> LRat r
| LMoney m -> LMoney m
| LUnit -> LUnit
| LDate d -> LDate d
| LDuration d -> LDuration d
| LEmptyError ->
Errors.raise_spanned_error pos
"Internal Error: An empty error was found in a place that shouldn't be \
possible."
(** [c = disjoint_union_maps cs] Compute the disjoint union of multiple maps.
Raises an internal error if there is two identicals keys in differnts parts. *)
let disjoint_union_maps (pos : Pos.t) (cs : ('e, 'a) Var.Map.t list) :
@ -219,7 +205,10 @@ let rec translate_and_hoist (ctx : 'm ctx) (e : 'm D.marked_expr) :
(Expr.make_abs [| x |] (Expr.make_var (x, pos)) [TAny, Expr.pos e] pos),
Var.Map.empty )
(* pure terms *)
| ELit l -> Expr.elit (translate_lit l (Expr.pos e)) pos, Var.Map.empty
| ELit
((LBool _ | LInt _ | LRat _ | LMoney _ | LUnit | LDate _ | LDuration _) as
l) ->
Expr.elit l pos, Var.Map.empty
| EIfThenElse (e1, e2, e3) ->
let e1', h1 = translate_and_hoist ctx e1 in
let e2', h2 = translate_and_hoist ctx e2 in

View File

@ -107,14 +107,14 @@ let rec format_statement
(fun fmt ((name, _), typ) ->
Format.fprintf fmt "%a%a %a@ %a%a" Print.punctuation "("
LocalName.format_t name Print.punctuation ":" (Print.typ decl_ctx)
(Marked.unmark typ) Print.punctuation ")"))
typ Print.punctuation ")"))
func.func_params Print.punctuation "="
(format_block decl_ctx ~debug)
func.func_body
| SLocalDecl (name, typ) ->
Format.fprintf fmt "@[<hov 2>%a %a %a@ %a@]" Print.keyword "decl"
LocalName.format_t (Marked.unmark name) Print.punctuation ":"
(Print.typ decl_ctx) (Marked.unmark typ)
(Print.typ decl_ctx) typ
| SLocalDef (name, expr) ->
Format.fprintf fmt "@[<hov 2>%a %a@ %a@]" LocalName.format_t
(Marked.unmark name) Print.punctuation "="
@ -184,7 +184,7 @@ let format_scope
(fun fmt ((name, _), typ) ->
Format.fprintf fmt "%a%a %a@ %a%a" Print.punctuation "("
LocalName.format_t name Print.punctuation ":" (Print.typ decl_ctx)
(Marked.unmark typ) Print.punctuation ")"))
typ Print.punctuation ")"))
body.scope_body_func.func_params Print.punctuation "="
(format_block decl_ctx ~debug)
body.scope_body_func.func_body

View File

@ -29,10 +29,7 @@ module ScopeVarMap : Map.S with type key = ScopeVar.t = Map.Make (ScopeVar)
module StructFieldMapLift = Bindlib.Lift (StructFieldMap)
module EnumConstructorMapLift = Bindlib.Lift (EnumConstructorMap)
type location =
| ScopeVar of ScopeVar.t Marked.pos
| SubScopeVar of
ScopeName.t * SubScopeName.t Marked.pos * ScopeVar.t Marked.pos
type location = scopelang glocation
module LocationSet : Set.S with type elt = location Marked.pos =
Set.Make (struct
@ -40,166 +37,24 @@ Set.Make (struct
let compare x y =
match Marked.unmark x, Marked.unmark y with
| ScopeVar (vx, _), ScopeVar (vy, _) -> ScopeVar.compare vx vy
| ScopelangScopeVar (vx, _), ScopelangScopeVar (vy, _) ->
ScopeVar.compare vx vy
| ( SubScopeVar (_, (xsubindex, _), (xsubvar, _)),
SubScopeVar (_, (ysubindex, _), (ysubvar, _)) ) ->
let c = SubScopeName.compare xsubindex ysubindex in
if c = 0 then ScopeVar.compare xsubvar ysubvar else c
| ScopeVar _, SubScopeVar _ -> -1
| SubScopeVar _, ScopeVar _ -> 1
| ScopelangScopeVar _, SubScopeVar _ -> -1
| SubScopeVar _, ScopelangScopeVar _ -> 1
end)
type typ =
| TLit of typ_lit
| TStruct of StructName.t
| TEnum of EnumName.t
| TArrow of typ Marked.pos * typ Marked.pos
| TArray of typ
| TAny
module Typ = struct
type t = typ
let rec compare ty1 ty2 =
match ty1, ty2 with
| TLit l1, TLit l2 -> Stdlib.compare l1 l2
| TStruct n1, TStruct n2 -> StructName.compare n1 n2
| TEnum en1, TEnum en2 -> EnumName.compare en1 en2
| TArrow ((a1, _), (b1, _)), TArrow ((a2, _), (b2, _)) -> (
match compare a1 a2 with 0 -> compare b1 b2 | n -> n)
| TArray t1, TArray t2 -> compare t1 t2
| TAny, TAny -> 0
| TLit _, _ -> -1
| _, TLit _ -> 1
| TStruct _, _ -> -1
| _, TStruct _ -> 1
| TEnum _, _ -> -1
| _, TEnum _ -> 1
| TArrow _, _ -> -1
| _, TArrow _ -> 1
| TArray _, _ -> -1
| _, TArray _ -> 1
end
type expr = (scopelang, Pos.t) gexpr
type marked_expr = expr Marked.pos
and expr =
| ELocation of location
| EVar of expr Bindlib.var
| EStruct of StructName.t * marked_expr StructFieldMap.t
| EStructAccess of marked_expr * StructFieldName.t * StructName.t
| EEnumInj of marked_expr * EnumConstructor.t * EnumName.t
| EMatch of marked_expr * EnumName.t * marked_expr EnumConstructorMap.t
| ELit of Dcalc.Ast.lit
| EAbs of (expr, marked_expr) Bindlib.mbinder * typ Marked.pos list
| EApp of marked_expr * marked_expr list
| EOp of operator
| EDefault of marked_expr list * marked_expr * marked_expr
| EIfThenElse of marked_expr * marked_expr * marked_expr
| EArray of marked_expr list
| ErrorOnEmpty of marked_expr
module ExprMap = Map.Make (struct
type t = marked_expr
module Expr = struct
type t = expr
let rec compare e1 e2 =
let rec list_compare cmp l1 l2 =
(* List.compare is available from OCaml 4.12 on *)
match l1, l2 with
| [], [] -> 0
| [], _ :: _ -> -1
| _ :: _, [] -> 1
| a1 :: l1, a2 :: l2 ->
let c = cmp a1 a2 in
if c <> 0 then c else list_compare cmp l1 l2
in
match e1, e2 with
| ELocation _, ELocation _ -> 0
| EVar v1, EVar v2 -> Bindlib.compare_vars v1 v2
| EStruct (name1, field_map1), EStruct (name2, field_map2) -> (
match StructName.compare name1 name2 with
| 0 ->
StructFieldMap.compare (Marked.compare compare) field_map1 field_map2
| n -> n)
| ( EStructAccess ((e1, _), field_name1, struct_name1),
EStructAccess ((e2, _), field_name2, struct_name2) ) -> (
match compare e1 e2 with
| 0 -> (
match StructFieldName.compare field_name1 field_name2 with
| 0 -> StructName.compare struct_name1 struct_name2
| n -> n)
| n -> n)
| EEnumInj ((e1, _), cstr1, name1), EEnumInj ((e2, _), cstr2, name2) -> (
match compare e1 e2 with
| 0 -> (
match EnumName.compare name1 name2 with
| 0 -> EnumConstructor.compare cstr1 cstr2
| n -> n)
| n -> n)
| EMatch ((e1, _), name1, emap1), EMatch ((e2, _), name2, emap2) -> (
match compare e1 e2 with
| 0 -> (
match EnumName.compare name1 name2 with
| 0 -> EnumConstructorMap.compare (Marked.compare compare) emap1 emap2
| n -> n)
| n -> n)
| ELit l1, ELit l2 -> Stdlib.compare l1 l2
| EAbs (binder1, typs1), EAbs (binder2, typs2) -> (
match list_compare (Marked.compare Typ.compare) typs1 typs2 with
| 0 ->
let _, (e1, _), (e2, _) = Bindlib.unmbind2 binder1 binder2 in
compare e1 e2
| n -> n)
| EApp ((f1, _), args1), EApp ((f2, _), args2) -> (
match compare f1 f2 with
| 0 -> list_compare (fun (x1, _) (x2, _) -> compare x1 x2) args1 args2
| n -> n)
| EOp op1, EOp op2 -> Stdlib.compare op1 op2
| ( EDefault (exs1, (just1, _), (cons1, _)),
EDefault (exs2, (just2, _), (cons2, _)) ) -> (
match compare just1 just2 with
| 0 -> (
match compare cons1 cons2 with
| 0 -> list_compare (Marked.compare compare) exs1 exs2
| n -> n)
| n -> n)
| ( EIfThenElse ((i1, _), (t1, _), (e1, _)),
EIfThenElse ((i2, _), (t2, _), (e2, _)) ) -> (
match compare i1 i2 with
| 0 -> ( match compare t1 t2 with 0 -> compare e1 e2 | n -> n)
| n -> n)
| EArray a1, EArray a2 ->
list_compare (fun (e1, _) (e2, _) -> compare e1 e2) a1 a2
| ErrorOnEmpty (e1, _), ErrorOnEmpty (e2, _) -> compare e1 e2
| ELocation _, _ -> -1
| _, ELocation _ -> 1
| EVar _, _ -> -1
| _, EVar _ -> 1
| EStruct _, _ -> -1
| _, EStruct _ -> 1
| EStructAccess _, _ -> -1
| _, EStructAccess _ -> 1
| EEnumInj _, _ -> -1
| _, EEnumInj _ -> 1
| EMatch _, _ -> -1
| _, EMatch _ -> 1
| ELit _, _ -> -1
| _, ELit _ -> 1
| EAbs _, _ -> -1
| _, EAbs _ -> 1
| EApp _, _ -> -1
| _, EApp _ -> 1
| EOp _, _ -> -1
| _, EOp _ -> 1
| EDefault _, _ -> -1
| _, EDefault _ -> 1
| EIfThenElse _, _ -> -1
| _, EIfThenElse _ -> 1
| EArray _, _ -> -1
| _, EArray _ -> 1
end
module ExprMap = Map.Make (Expr)
let compare = Expr.compare
end)
let rec locations_used (e : expr Marked.pos) : LocationSet.t =
match Marked.unmark e with
@ -214,7 +69,7 @@ let rec locations_used (e : expr Marked.pos) : LocationSet.t =
es LocationSet.empty
| EStructAccess (e1, _, _) -> locations_used e1
| EEnumInj (e1, _, _) -> locations_used e1
| EMatch (e1, _, es) ->
| EMatchS (e1, _, es) ->
EnumConstructorMap.fold
(fun _ e' acc -> LocationSet.union acc (locations_used e'))
es (locations_used e1)
@ -240,79 +95,17 @@ type io_input = NoInput | OnlyInput | Reentrant
type io = { io_output : bool Marked.pos; io_input : io_input Marked.pos }
type rule =
| Definition of location Marked.pos * typ Marked.pos * io * expr Marked.pos
| Definition of location Marked.pos * marked_typ * io * expr Marked.pos
| Assertion of expr Marked.pos
| Call of ScopeName.t * SubScopeName.t
type scope_decl = {
scope_decl_name : ScopeName.t;
scope_sig : (typ Marked.pos * io) ScopeVarMap.t;
scope_sig : (marked_typ * io) ScopeVarMap.t;
scope_decl_rules : rule list;
}
type struct_ctx = (StructFieldName.t * typ Marked.pos) list StructMap.t
type enum_ctx = (EnumConstructor.t * typ Marked.pos) list EnumMap.t
type program = {
program_scopes : scope_decl ScopeMap.t;
program_enums : enum_ctx;
program_structs : struct_ctx;
program_ctx : decl_ctx;
}
module Var = struct
type t = expr Bindlib.var
let make (s : string) : t =
Bindlib.new_var (fun (x : expr Bindlib.var) : expr -> EVar x) s
let compare x y = Bindlib.compare_vars x y
end
type vars = expr Bindlib.mvar
let make_var ((x, pos) : Var.t Marked.pos) : expr Marked.pos Bindlib.box =
Bindlib.box_apply (fun v -> v, pos) (Bindlib.box_var x)
let make_abs
(xs : vars)
(e : expr Marked.pos Bindlib.box)
(taus : typ Marked.pos list)
(pos : Pos.t) : expr Marked.pos Bindlib.box =
Bindlib.box_apply (fun b -> EAbs (b, taus), pos) (Bindlib.bind_mvar xs e)
let make_app
(e : expr Marked.pos Bindlib.box)
(u : expr Marked.pos Bindlib.box list)
(pos : Pos.t) : expr Marked.pos Bindlib.box =
Bindlib.box_apply2 (fun e u -> EApp (e, u), pos) e (Bindlib.box_list u)
let make_let_in
(x : Var.t)
(tau : typ Marked.pos)
(e1 : expr Marked.pos Bindlib.box)
(e2 : expr Marked.pos Bindlib.box) : expr Marked.pos Bindlib.box =
Bindlib.box_apply2
(fun e u -> EApp (e, u), Marked.get_mark (Bindlib.unbox e2))
(make_abs [| x |] e2 [tau] (Marked.get_mark (Bindlib.unbox e2)))
(Bindlib.box_list [e1])
let make_default ?(pos = Pos.no_pos) exceptions just cons =
let rec bool_value = function
| ELit (LBool b), _ -> Some b
| EApp ((EOp (Unop (Log (l, _))), _), [e]), _
when l <> PosRecordIfTrueBool
(* we don't remove the log calls corresponding to source code
definitions !*) ->
bool_value e
| _ -> None
in
match exceptions, bool_value just, cons with
| [], Some true, cons -> cons
| exceptions, Some true, (EDefault ([], just, cons), pos) ->
EDefault (exceptions, just, cons), pos
| [except], Some false, _ -> except
| exceptions, _, cons ->
let pos = if pos <> Pos.no_pos then pos else Marked.get_mark just in
EDefault (exceptions, just, cons), pos
module VarMap = Map.Make (Var)

View File

@ -37,49 +37,18 @@ module EnumConstructorMapLift : sig
'a Bindlib.box EnumConstructorMap.t -> 'a EnumConstructorMap.t Bindlib.box
end
type location =
| ScopeVar of ScopeVar.t Marked.pos
| SubScopeVar of
ScopeName.t * SubScopeName.t Marked.pos * ScopeVar.t Marked.pos
type location = scopelang glocation
module LocationSet : Set.S with type elt = location Marked.pos
(** {1 Abstract syntax tree} *)
type typ =
| TLit of typ_lit
| TStruct of StructName.t
| TEnum of EnumName.t
| TArrow of typ Marked.pos * typ Marked.pos
| TArray of typ
| TAny
type expr = (scopelang, Pos.t) gexpr
type marked_expr = (scopelang, Pos.t) marked_gexpr
module Typ : Set.OrderedType with type t = typ
module ExprMap : Map.S with type key = marked_expr
type marked_expr = expr Marked.pos
(** The expressions use the {{:https://lepigre.fr/ocaml-bindlib/} Bindlib}
library, based on higher-order abstract syntax*)
and expr =
| ELocation of location
| EVar of expr Bindlib.var
| EStruct of StructName.t * marked_expr StructFieldMap.t
| EStructAccess of marked_expr * StructFieldName.t * StructName.t
| EEnumInj of marked_expr * EnumConstructor.t * EnumName.t
| EMatch of marked_expr * EnumName.t * marked_expr EnumConstructorMap.t
| ELit of Dcalc.Ast.lit
| EAbs of (expr, marked_expr) Bindlib.mbinder * typ Marked.pos list
| EApp of marked_expr * marked_expr list
| EOp of operator
| EDefault of marked_expr list * marked_expr * marked_expr
| EIfThenElse of marked_expr * marked_expr * marked_expr
| EArray of marked_expr list
| ErrorOnEmpty of marked_expr
module Expr : Set.OrderedType with type t = expr
module ExprMap : Map.S with type key = expr
val locations_used : expr Marked.pos -> LocationSet.t
val locations_used : marked_expr -> LocationSet.t
(** This type characterizes the three levels of visibility for a given scope
variable with regards to the scope's input and possible redefinitions inside
@ -103,75 +72,17 @@ type io = {
(** Characterization of the input/output status of a scope variable. *)
type rule =
| Definition of location Marked.pos * typ Marked.pos * io * expr Marked.pos
| Definition of location Marked.pos * marked_typ * io * expr Marked.pos
| Assertion of expr Marked.pos
| Call of ScopeName.t * SubScopeName.t
type scope_decl = {
scope_decl_name : ScopeName.t;
scope_sig : (typ Marked.pos * io) ScopeVarMap.t;
scope_sig : (marked_typ * io) ScopeVarMap.t;
scope_decl_rules : rule list;
}
type struct_ctx = (StructFieldName.t * typ Marked.pos) list StructMap.t
type enum_ctx = (EnumConstructor.t * typ Marked.pos) list EnumMap.t
type program = {
program_scopes : scope_decl ScopeMap.t;
program_enums : enum_ctx;
program_structs : struct_ctx;
program_ctx : decl_ctx;
}
(** {1 Variable helpers} *)
module Var : sig
type t = expr Bindlib.var
val make : string -> t
val compare : t -> t -> int
end
module VarMap : Map.S with type key = Var.t
type vars = expr Bindlib.mvar
val make_var : Var.t Marked.pos -> expr Marked.pos Bindlib.box
val make_abs :
vars ->
expr Marked.pos Bindlib.box ->
typ Marked.pos list ->
Pos.t ->
expr Marked.pos Bindlib.box
val make_app :
expr Marked.pos Bindlib.box ->
expr Marked.pos Bindlib.box list ->
Pos.t ->
expr Marked.pos Bindlib.box
val make_let_in :
Var.t ->
typ Marked.pos ->
expr Marked.pos Bindlib.box ->
expr Marked.pos Bindlib.box ->
expr Marked.pos Bindlib.box
val make_default :
?pos:Pos.t ->
expr Marked.pos list ->
expr Marked.pos ->
expr Marked.pos ->
expr Marked.pos
(** [make_default ?pos exceptions just cons] builds a term semantically
equivalent to [<exceptions | just :- cons>] (the [EDefault] constructor)
while avoiding redundant nested constructions. The position is extracted
from [just] by default.
Note that, due to the simplifications taking place, the result might not be
of the form [EDefault]:
- [<true :- x>] is rewritten as [x]
- [<ex | true :- def>], when [def] is a default term [<j :- c>] without
exceptions, is collapsed into [<ex | def>]
- [<ex | false :- _>], when [ex] is a single exception, is rewritten as [ex] *)

View File

@ -164,19 +164,23 @@ module TTopologicalTraversal = Graph.Topological.Make (TDependencies)
module TSCC = Graph.Components.Make (TDependencies)
(** Tarjan's stongly connected components algorithm, provided by OCamlGraph *)
let rec get_structs_or_enums_in_type (t : Ast.typ Marked.pos) : TVertexSet.t =
let rec get_structs_or_enums_in_type (t : typ Marked.pos) : TVertexSet.t =
match Marked.unmark t with
| Ast.TStruct s -> TVertexSet.singleton (TVertex.Struct s)
| Ast.TEnum e -> TVertexSet.singleton (TVertex.Enum e)
| Ast.TArrow (t1, t2) ->
| TStruct s -> TVertexSet.singleton (TVertex.Struct s)
| TEnum e -> TVertexSet.singleton (TVertex.Enum e)
| TArrow (t1, t2) ->
TVertexSet.union
(get_structs_or_enums_in_type t1)
(get_structs_or_enums_in_type t2)
| Ast.TLit _ | Ast.TAny -> TVertexSet.empty
| Ast.TArray t1 -> get_structs_or_enums_in_type (Marked.same_mark_as t1 t)
| TLit _ | TAny -> TVertexSet.empty
| TOption t1 | TArray t1 -> get_structs_or_enums_in_type t1
| TTuple ts ->
List.fold_left
(fun acc t -> TVertexSet.union acc (get_structs_or_enums_in_type t))
TVertexSet.empty ts
let build_type_graph (structs : Ast.struct_ctx) (enums : Ast.enum_ctx) :
TDependencies.t =
let build_type_graph (structs : struct_ctx) (enums : enum_ctx) : TDependencies.t
=
let g = TDependencies.empty in
let g =
StructMap.fold
@ -228,8 +232,8 @@ let build_type_graph (structs : Ast.struct_ctx) (enums : Ast.enum_ctx) :
in
g
let check_type_cycles (structs : Ast.struct_ctx) (enums : Ast.enum_ctx) :
TVertex.t list =
let check_type_cycles (structs : struct_ctx) (enums : enum_ctx) : TVertex.t list
=
let g = build_type_graph structs enums in
(* if there is a cycle, there will be an strongly connected component of
cardinality > 1 *)

View File

@ -49,6 +49,6 @@ module TVertexSet : Set.S with type elt = TVertex.t
module TDependencies :
Graph.Sig.P with type V.t = TVertex.t and type E.label = Pos.t
val get_structs_or_enums_in_type : Ast.typ Marked.pos -> TVertexSet.t
val build_type_graph : Ast.struct_ctx -> Ast.enum_ctx -> TDependencies.t
val check_type_cycles : Ast.struct_ctx -> Ast.enum_ctx -> TVertex.t list
val get_structs_or_enums_in_type : typ Marked.pos -> TVertexSet.t
val build_type_graph : struct_ctx -> enum_ctx -> TDependencies.t
val check_type_cycles : struct_ctx -> enum_ctx -> TVertex.t list

View File

@ -18,147 +18,8 @@ open Utils
open Shared_ast
open Ast
let needs_parens (e : expr Marked.pos) : bool =
match Marked.unmark e with EAbs _ -> true | _ -> false
let format_var (fmt : Format.formatter) (v : Var.t) : unit =
Format.fprintf fmt "%s_%d" (Bindlib.name_of v) (Bindlib.uid_of v)
let format_location (fmt : Format.formatter) (l : location) : unit =
match l with
| ScopeVar v -> Format.fprintf fmt "%a" ScopeVar.format_t (Marked.unmark v)
| SubScopeVar (_, subindex, subvar) ->
Format.fprintf fmt "%a.%a" SubScopeName.format_t (Marked.unmark subindex)
ScopeVar.format_t (Marked.unmark subvar)
let typ_needs_parens (e : typ Marked.pos) : bool =
match Marked.unmark e with TArrow _ -> true | _ -> false
let rec format_typ (fmt : Format.formatter) (typ : typ Marked.pos) : unit =
let format_typ_with_parens (fmt : Format.formatter) (t : typ Marked.pos) =
if typ_needs_parens t then
Format.fprintf fmt "%a%a%a" Print.punctuation "(" format_typ t
Print.punctuation ")"
else Format.fprintf fmt "%a" format_typ t
in
match Marked.unmark typ with
| TLit l -> Print.tlit fmt l
| TStruct s -> Format.fprintf fmt "%a" StructName.format_t s
| TEnum e -> Format.fprintf fmt "%a" EnumName.format_t e
| TArrow (t1, t2) ->
Format.fprintf fmt "@[<hov 2>%a %a@ %a@]" format_typ_with_parens t1
Print.operator "" format_typ t2
| TArray t1 ->
Format.fprintf fmt "@[%a@ %a@]" format_typ
(Marked.same_mark_as t1 typ)
Print.base_type "array"
| TAny -> Format.fprintf fmt "any"
let rec format_expr
?(debug : bool = false)
(fmt : Format.formatter)
(e : expr Marked.pos) : unit =
let format_expr = format_expr ~debug in
let format_with_parens (fmt : Format.formatter) (e : expr Marked.pos) =
if needs_parens e then Format.fprintf fmt "(%a)" format_expr e
else Format.fprintf fmt "%a" format_expr e
in
match Marked.unmark e with
| ELocation l -> Format.fprintf fmt "%a" format_location l
| EVar v -> Format.fprintf fmt "%a" format_var v
| ELit l -> Format.fprintf fmt "%a" Print.lit l
| EStruct (name, fields) ->
Format.fprintf fmt " @[<hov 2>%a@ %a@ %a@ %a@]" StructName.format_t name
Print.punctuation "{"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "%a@ " Print.punctuation ";")
(fun fmt (field_name, field_expr) ->
Format.fprintf fmt "%a%a%a%a@ %a" Print.punctuation "\""
StructFieldName.format_t field_name Print.punctuation "\""
Print.punctuation "=" format_expr field_expr))
(StructFieldMap.bindings fields)
Print.punctuation "}"
| EStructAccess (e1, field, _) ->
Format.fprintf fmt "%a%a%a%a%a" format_expr e1 Print.punctuation "."
Print.punctuation "\"" StructFieldName.format_t field Print.punctuation
"\""
| EEnumInj (e1, cons, _) ->
Format.fprintf fmt "%a@ %a" EnumConstructor.format_t cons format_expr e1
| EMatch (e1, _, cases) ->
Format.fprintf fmt "@[<hov 0>%a@ @[<hov 2>%a@]@ %a@ %a@]" Print.keyword
"match" format_expr e1 Print.keyword "with"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n")
(fun fmt (cons_name, case_expr) ->
Format.fprintf fmt "@[<hov 2>%a %a@ %a@ %a@]" Print.punctuation "|"
Print.enum_constructor cons_name Print.punctuation "" format_expr
case_expr))
(EnumConstructorMap.bindings cases)
| EApp ((EAbs (binder, taus), _), args) ->
let xs, body = Bindlib.unmbind binder in
let xs_tau = List.map2 (fun x tau -> x, tau) (Array.to_list xs) taus in
let xs_tau_arg = List.map2 (fun (x, tau) arg -> x, tau, arg) xs_tau args in
Format.fprintf fmt "@[%a%a@]"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt " ")
(fun fmt (x, tau, arg) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@ %a@ %a@ %a@ %a@\n@]"
Print.keyword "let" format_var x Print.punctuation ":" format_typ
tau Print.punctuation "=" format_expr arg Print.keyword "in"))
xs_tau_arg format_expr body
| EAbs (binder, taus) ->
let xs, body = Bindlib.unmbind binder in
let xs_tau = List.map2 (fun x tau -> x, tau) (Array.to_list xs) taus in
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@ %a@]" Print.punctuation "λ"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt " ")
(fun fmt (x, tau) ->
Format.fprintf fmt "@[%a%a%a@ %a%a@]" Print.punctuation "("
format_var x Print.punctuation ":" format_typ tau Print.punctuation
")"))
xs_tau Print.punctuation "" format_expr body
| EApp ((EOp (Binop op), _), [arg1; arg2]) ->
Format.fprintf fmt "@[%a@ %a@ %a@]" format_with_parens arg1 Print.binop op
format_with_parens arg2
| EApp ((EOp (Unop (Log _)), _), [arg1]) when not debug ->
format_expr fmt arg1
| EApp ((EOp (Unop op), _), [arg1]) ->
Format.fprintf fmt "@[%a@ %a@]" Print.unop op format_with_parens arg1
| EApp (f, args) ->
Format.fprintf fmt "@[%a@ %a@]" format_expr f
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")
format_with_parens)
args
| EIfThenElse (e1, e2, e3) ->
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@ %a@ %a@ %a@]" Print.keyword "if"
format_expr e1 Print.keyword "then" format_expr e2 Print.keyword "else"
format_expr e3
| EOp (Ternop op) -> Format.fprintf fmt "%a" Print.ternop op
| EOp (Binop op) -> Format.fprintf fmt "%a" Print.binop op
| EOp (Unop op) -> Format.fprintf fmt "%a" Print.unop op
| EDefault (excepts, just, cons) ->
if List.length excepts = 0 then
Format.fprintf fmt "@[%a%a %a@ %a%a@]" Print.punctuation "" format_expr
just Print.punctuation "" format_expr cons Print.punctuation ""
else
Format.fprintf fmt "@[<hov 2>%a%a@ %a@ %a %a@ %a%a@]" Print.punctuation
""
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt ",@ ")
format_expr)
excepts Print.punctuation "|" format_expr just Print.punctuation ""
format_expr cons Print.punctuation ""
| ErrorOnEmpty e' ->
Format.fprintf fmt "error_empty@ %a" format_with_parens e'
| EArray es ->
Format.fprintf fmt "%a%a%a" Print.punctuation "["
(Format.pp_print_list
~pp_sep:(fun fmt () -> Print.punctuation fmt ";")
(fun fmt e -> Format.fprintf fmt "@[%a@]" format_expr e))
es Print.punctuation "]"
let format_struct
let struc
ctx
(fmt : Format.formatter)
((name, fields) : StructName.t * (StructFieldName.t * typ Marked.pos) list)
: unit =
@ -168,10 +29,11 @@ let format_struct
~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n")
(fun fmt (field_name, typ) ->
Format.fprintf fmt "%a%a %a" StructFieldName.format_t field_name
Print.punctuation ":" format_typ typ))
Print.punctuation ":" (Print.typ ctx) typ))
fields Print.punctuation "}"
let format_enum
let enum
ctx
(fmt : Format.formatter)
((name, cases) : EnumName.t * (EnumConstructor.t * typ Marked.pos) list) :
unit =
@ -181,21 +43,17 @@ let format_enum
~pp_sep:(fun fmt () -> Format.fprintf fmt "@\n")
(fun fmt (field_name, typ) ->
Format.fprintf fmt "%a %a%a %a" Print.punctuation "|"
EnumConstructor.format_t field_name Print.punctuation ":" format_typ
typ))
EnumConstructor.format_t field_name Print.punctuation ":"
(Print.typ ctx) typ))
cases
let format_scope
?(debug : bool = false)
(fmt : Format.formatter)
((name, decl) : ScopeName.t * scope_decl) : unit =
let scope ?(debug = false) ctx fmt (name, decl) =
Format.fprintf fmt "@[<hov 2>%a@ %a@ %a@ %a@ %a@]@\n@[<v 2> %a@]"
Print.keyword "let" Print.keyword "scope" ScopeName.format_t name
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")
(Format.pp_print_list ~pp_sep:Format.pp_print_space
(fun fmt (scope_var, (typ, vis)) ->
Format.fprintf fmt "%a%a%a %a%a%a%a%a" Print.punctuation "("
ScopeVar.format_t scope_var Print.punctuation ":" format_typ typ
ScopeVar.format_t scope_var Print.punctuation ":" (Print.typ ctx) typ
Print.punctuation "|" Print.keyword
(match Marked.unmark vis.io_input with
| NoInput -> "internal"
@ -214,12 +72,12 @@ let format_scope
match rule with
| Definition (loc, typ, _, e) ->
Format.fprintf fmt "@[<hov 2>%a %a %a %a %a@ %a@]" Print.keyword
"let" format_location (Marked.unmark loc) Print.punctuation ":"
format_typ typ Print.punctuation "="
"let" Print.location (Marked.unmark loc) Print.punctuation ":"
(Print.typ ctx) typ Print.punctuation "="
(fun fmt e ->
match Marked.unmark loc with
| SubScopeVar _ -> format_expr fmt e
| ScopeVar v -> (
| SubScopeVar _ -> Print.expr ctx fmt e
| ScopelangScopeVar v -> (
match
Marked.unmark
(snd (ScopeVarMap.find (Marked.unmark v) decl.scope_sig))
@ -227,40 +85,33 @@ let format_scope
with
| Reentrant ->
Format.fprintf fmt "%a@ %a" Print.operator
"reentrant or by default" (format_expr ~debug) e
| _ -> Format.fprintf fmt "%a" (format_expr ~debug) e))
"reentrant or by default" (Print.expr ~debug ctx) e
| _ -> Format.fprintf fmt "%a" (Print.expr ~debug ctx) e))
e
| Assertion e ->
Format.fprintf fmt "%a %a" Print.keyword "assert"
(format_expr ~debug) e
(Print.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 "["
SubScopeName.format_t subscope_name Print.punctuation "]"))
decl.scope_decl_rules
let format_program
?(debug : bool = false)
(fmt : Format.formatter)
(p : program) : unit =
Format.fprintf fmt "%a%a%a%a%a"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "\n\n")
format_struct)
(StructMap.bindings p.program_structs)
(fun fmt () ->
if StructMap.is_empty p.program_structs then Format.fprintf fmt ""
else Format.fprintf fmt "\n\n")
let program ?(debug : bool = false) (fmt : Format.formatter) (p : program) :
unit =
let ctx = p.program_ctx in
let pp_sep fmt () =
Format.pp_print_cut fmt ();
Format.pp_print_cut fmt ()
in
Format.fprintf fmt "@[<v>%a%a%a%a%a@]"
(Format.pp_print_list ~pp_sep (struc ctx))
(StructMap.bindings ctx.ctx_structs)
(if StructMap.is_empty ctx.ctx_structs then fun _ _ -> () else pp_sep)
()
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "\n\n")
format_enum)
(EnumMap.bindings p.program_enums)
(fun fmt () ->
if EnumMap.is_empty p.program_enums then Format.fprintf fmt ""
else Format.fprintf fmt "\n\n")
(Format.pp_print_list ~pp_sep (enum ctx))
(EnumMap.bindings ctx.ctx_enums)
(if EnumMap.is_empty ctx.ctx_enums then fun _ _ -> () else pp_sep)
()
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "\n\n")
(format_scope ~debug))
(Format.pp_print_list ~pp_sep (scope ~debug ctx))
(ScopeMap.bindings p.program_scopes)

View File

@ -14,25 +14,14 @@
License for the specific language governing permissions and limitations under
the License. *)
open Utils
val format_var : Format.formatter -> Ast.Var.t -> unit
val format_location : Format.formatter -> Ast.location -> unit
val format_typ : Format.formatter -> Ast.typ Marked.pos -> unit
val format_expr :
?debug:bool (** [true] for debug printing *) ->
Format.formatter ->
Ast.expr Marked.pos ->
unit
val format_scope :
val scope :
?debug:bool (** [true] for debug printing *) ->
Shared_ast.decl_ctx ->
Format.formatter ->
Shared_ast.ScopeName.t * Ast.scope_decl ->
unit
val format_program :
val program :
?debug:bool (** [true] for debug printing *) ->
Format.formatter ->
Ast.program ->

View File

@ -36,20 +36,20 @@ type scope_sig_ctx = {
type scope_sigs_ctx = scope_sig_ctx Ast.ScopeMap.t
type ctx = {
structs : Ast.struct_ctx;
enums : Ast.enum_ctx;
structs : struct_ctx;
enums : enum_ctx;
scope_name : ScopeName.t;
scopes_parameters : scope_sigs_ctx;
scope_vars : (untyped Dcalc.Ast.expr Var.t * typ * Ast.io) Ast.ScopeVarMap.t;
subscope_vars :
(untyped Dcalc.Ast.expr Var.t * typ * Ast.io) Ast.ScopeVarMap.t
Ast.SubScopeMap.t;
local_vars : untyped Dcalc.Ast.expr Var.t Ast.VarMap.t;
local_vars : (Ast.expr, untyped Dcalc.Ast.expr Var.t) Var.Map.t;
}
let empty_ctx
(struct_ctx : Ast.struct_ctx)
(enum_ctx : Ast.enum_ctx)
(struct_ctx : struct_ctx)
(enum_ctx : enum_ctx)
(scopes_ctx : scope_sigs_ctx)
(scope_name : ScopeName.t) =
{
@ -59,21 +59,9 @@ let empty_ctx
scopes_parameters = scopes_ctx;
scope_vars = Ast.ScopeVarMap.empty;
subscope_vars = Ast.SubScopeMap.empty;
local_vars = Ast.VarMap.empty;
local_vars = Var.Map.empty;
}
let rec translate_typ (_ctx : ctx) (t : Ast.typ Marked.pos) : typ Marked.pos =
Marked.same_mark_as
(match Marked.unmark t with
| Ast.TLit l -> TLit l
| Ast.TArrow (t1, t2) ->
TArrow (translate_typ _ctx t1, translate_typ _ctx t2)
| Ast.TStruct s_uid -> TStruct s_uid
| Ast.TEnum e_uid -> TEnum e_uid
| Ast.TArray t1 -> TArray (translate_typ _ctx (Marked.same_mark_as t1 t))
| Ast.TAny -> TAny)
t
let pos_mark (pos : Pos.t) : untyped mark = Untyped { pos }
let pos_mark_as e = pos_mark (Marked.get_mark e)
@ -118,7 +106,7 @@ let collapse_similar_outcomes (excepts : Ast.expr Marked.pos list) :
let cons_map =
List.fold_left
(fun map -> function
| (Ast.EDefault ([], _, (cons, _)), _) as e ->
| (EDefault ([], _, cons), _) as e ->
Ast.ExprMap.update cons
(fun prev -> Some (e :: Option.value ~default:[] prev))
map
@ -129,12 +117,12 @@ let collapse_similar_outcomes (excepts : Ast.expr Marked.pos list) :
List.fold_right
(fun e (cons_map, excepts) ->
match e with
| Ast.EDefault ([], _, (cons, _)), _ ->
| EDefault ([], _, cons), _ ->
let collapsed_exc =
List.fold_left
(fun acc -> function
| Ast.EDefault ([], just, cons), pos ->
[Ast.EDefault (acc, just, cons), pos]
| EDefault ([], just, cons), pos ->
[EDefault (acc, just, cons), pos]
| _ -> assert false)
[]
(Ast.ExprMap.find cons cons_map)
@ -151,8 +139,11 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Marked.pos) :
Marked.mark (pos_mark_as e) x)
@@
match Marked.unmark e with
| EVar v -> Bindlib.box_var (Ast.VarMap.find v ctx.local_vars)
| ELit l -> Bindlib.box (ELit l)
| EVar v -> Bindlib.box_var (Var.Map.find v ctx.local_vars)
| ELit
(( LBool _ | LEmptyError | LInt _ | LRat _ | LMoney _ | LUnit | LDate _
| LDuration _ ) as l) ->
Bindlib.box (ELit l)
| EStruct (struct_name, e_fields) ->
let struct_sig = StructMap.find struct_name ctx.structs in
let d_fields, remaining_e_fields =
@ -189,11 +180,7 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Marked.pos) :
let e1 = translate_expr ctx e1 in
Bindlib.box_apply
(fun e1 ->
ETupleAccess
( e1,
field_index,
Some struct_name,
List.map (fun (_, t) -> translate_typ ctx t) struct_sig ))
ETupleAccess (e1, field_index, Some struct_name, List.map snd struct_sig))
e1
| EEnumInj (e1, constructor, enum_name) ->
let enum_sig = EnumMap.find enum_name ctx.enums in
@ -207,14 +194,9 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Marked.pos) :
in
let e1 = translate_expr ctx e1 in
Bindlib.box_apply
(fun e1 ->
EInj
( e1,
constructor_index,
enum_name,
List.map (fun (_, t) -> translate_typ ctx t) enum_sig ))
(fun e1 -> EInj (e1, constructor_index, enum_name, List.map snd enum_sig))
e1
| EMatch (e1, enum_name, cases) ->
| EMatchS (e1, enum_name, cases) ->
let enum_sig = EnumMap.find enum_name ctx.enums in
let d_cases, remaining_e_cases =
List.fold_right
@ -251,9 +233,9 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Marked.pos) :
let e1_func = translate_expr ctx e1 in
let markings l =
match l with
| Ast.ScopeVar (v, _) ->
| ScopelangScopeVar (v, _) ->
[ScopeName.get_info ctx.scope_name; ScopeVar.get_info v]
| Ast.SubScopeVar (s, _, (v, _)) ->
| SubScopeVar (s, _, (v, _)) ->
[ScopeName.get_info s; ScopeVar.get_info v]
in
let e1_func =
@ -275,7 +257,7 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Marked.pos) :
| _ -> TAny, TAny
in
match Marked.unmark e1 with
| ELocation (ScopeVar var) ->
| ELocation (ScopelangScopeVar var) ->
retrieve_in_and_out_typ_or_any var ctx.scope_vars
| ELocation (SubScopeVar (_, sname, var)) ->
ctx.subscope_vars
@ -318,22 +300,20 @@ let rec translate_expr (ctx : ctx) (e : Ast.expr Marked.pos) :
ctx with
local_vars =
Array.fold_left
(fun local_vars (x, new_x) -> Ast.VarMap.add x new_x local_vars)
(fun local_vars (x, new_x) -> Var.Map.add x new_x local_vars)
ctx.local_vars both_xs;
}
body
in
let binder = Bindlib.bind_mvar new_xs body in
Bindlib.box_apply
(fun b -> EAbs (b, List.map (translate_typ ctx) typ))
binder
Bindlib.box_apply (fun b -> EAbs (b, typ)) binder
| EDefault (excepts, just, cons) ->
let excepts = collapse_similar_outcomes excepts in
Bindlib.box_apply3
(fun e j c -> EDefault (e, j, c))
(Bindlib.box_list (List.map (translate_expr ctx) excepts))
(translate_expr ctx just) (translate_expr ctx cons)
| ELocation (ScopeVar a) ->
| ELocation (ScopelangScopeVar a) ->
let v, _, _ = Ast.ScopeVarMap.find (Marked.unmark a) ctx.scope_vars in
Bindlib.box_var v
| ELocation (SubScopeVar (_, s, a)) -> (
@ -381,10 +361,9 @@ let translate_rule
untyped Dcalc.Ast.expr scope_body_expr Bindlib.box)
* ctx =
match rule with
| Definition ((ScopeVar a, var_def_pos), tau, a_io, e) ->
| Definition ((ScopelangScopeVar a, var_def_pos), tau, a_io, e) ->
let a_name = ScopeVar.get_info (Marked.unmark a) in
let a_var = Var.make (Marked.unmark a_name) in
let tau = translate_typ ctx tau in
let new_e = translate_expr ctx e in
let a_expr = Expr.make_var (a_var, pos_mark var_def_pos) in
let merged_expr =
@ -435,7 +414,6 @@ let translate_rule
(SubScopeName.get_info (Marked.unmark subs_index))
in
let a_var = Var.make (Marked.unmark a_name) in
let tau = translate_typ ctx tau in
let new_e =
tag_with_log_entry (translate_expr ctx e)
(VarDef (Marked.unmark tau))
@ -690,8 +668,8 @@ let translate_rules
new_ctx )
let translate_scope_decl
(struct_ctx : Ast.struct_ctx)
(enum_ctx : Ast.enum_ctx)
(struct_ctx : struct_ctx)
(enum_ctx : enum_ctx)
(sctx : scope_sigs_ctx)
(scope_name : ScopeName.t)
(sigma : Ast.scope_decl) :
@ -826,29 +804,11 @@ let translate_program (prgm : Ast.program) :
let scope_dependencies = Dependency.build_program_dep_graph prgm in
Dependency.check_for_cycle_in_scope scope_dependencies;
let types_ordering =
Dependency.check_type_cycles prgm.program_structs prgm.program_enums
Dependency.check_type_cycles prgm.program_ctx.ctx_structs
prgm.program_ctx.ctx_enums
in
let scope_ordering = Dependency.get_scope_ordering scope_dependencies in
let struct_ctx = prgm.program_structs in
let enum_ctx = prgm.program_enums in
let ctx_for_typ_translation scope_name =
empty_ctx struct_ctx enum_ctx Ast.ScopeMap.empty scope_name
in
let dummy_scope = ScopeName.fresh ("dummy", Pos.no_pos) in
let decl_ctx =
{
ctx_structs =
StructMap.map
(List.map (fun (x, y) ->
x, translate_typ (ctx_for_typ_translation dummy_scope) y))
struct_ctx;
ctx_enums =
EnumMap.map
(List.map (fun (x, y) ->
x, (translate_typ (ctx_for_typ_translation dummy_scope)) y))
enum_ctx;
}
in
let decl_ctx = prgm.program_ctx in
let sctx : scope_sigs_ctx =
Ast.ScopeMap.mapi
(fun scope_name scope ->
@ -875,9 +835,6 @@ let translate_program (prgm : Ast.program) :
scope_sig_local_vars =
List.map
(fun (scope_var, (tau, vis)) ->
let tau =
translate_typ (ctx_for_typ_translation scope_name) tau
in
{
scope_var_name = scope_var;
scope_var_typ = Marked.unmark tau;
@ -898,7 +855,8 @@ let translate_program (prgm : Ast.program) :
(fun scope_name (scopes, decl_ctx) ->
let scope = Ast.ScopeMap.find scope_name prgm.program_scopes in
let scope_body, scope_out_struct =
translate_scope_decl struct_ctx enum_ctx sctx scope_name scope
translate_scope_decl decl_ctx.ctx_structs decl_ctx.ctx_enums sctx
scope_name scope
in
let dvar = (Ast.ScopeMap.find scope_name sctx).scope_sig_scope_var in
let decl_ctx =

View File

@ -56,6 +56,9 @@ module StructFieldMap : Map.S with type key = StructFieldName.t =
module EnumConstructorMap : Map.S with type key = EnumConstructor.t =
Map.Make (EnumConstructor)
module StateName : Uid.Id with type info = Uid.MarkedString.info =
Uid.Make (Uid.MarkedString) ()
(** {1 Abstract syntax tree} *)
(** {2 Types} *)
@ -131,12 +134,6 @@ type unop =
| RoundDecimal
type operator = Ternop of ternop | Binop of binop | Unop of unop
type location =
| ScopeVar of ScopeVar.t Marked.pos
| SubScopeVar of
ScopeName.t * SubScopeName.t Marked.pos * ScopeVar.t Marked.pos
type except = ConflictError | EmptyError | NoValueProvided | Crash
(** {2 Generic expressions} *)
@ -164,11 +161,28 @@ type 'a glit =
| LDate : date -> 'a glit
| LDuration : duration -> 'a glit
(** Locations are handled differently in [desugared] and [scopelang] *)
type 'a glocation =
| DesugaredScopeVar :
ScopeVar.t Marked.pos * StateName.t option
-> desugared glocation
| ScopelangScopeVar : ScopeVar.t Marked.pos -> scopelang glocation
| SubScopeVar :
ScopeName.t * SubScopeName.t Marked.pos * ScopeVar.t Marked.pos
-> [< desugared | scopelang ] glocation
type ('a, 't) marked_gexpr = (('a, 't) 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 expr = dcalc gexpr] plus the annotations. *)
are then defined with [type expr = dcalc gexpr] plus the annotations.
A few tips on using this GADT:
- To write a function that handles cases from different ASTs, explicit the
type variables: [fun (type a) (x: a gexpr) -> ...]
- For recursive functions, you may need to additionally explicit the
generalisation of the variable: [let rec f: type a . a gexpr -> ...] *)
(** The expressions use the {{:https://lepigre.fr/ocaml-bindlib/} Bindlib}
library, based on higher-order abstract syntax *)
@ -185,14 +199,13 @@ and ('a, 't) gexpr =
('a, 't) gexpr Bindlib.var
-> (([< desugared | scopelang | dcalc | lcalc ] as 'a), 't) gexpr
| EAbs :
(('a, 't) gexpr, ('a, 't) marked_gexpr) Bindlib.mbinder
* typ Marked.pos list
(('a, 't) gexpr, ('a, 't) marked_gexpr) Bindlib.mbinder * marked_typ list
-> (([< desugared | scopelang | dcalc | lcalc ] as 'a), 't) gexpr
| EIfThenElse :
('a, 't) marked_gexpr * ('a, 't) marked_gexpr * ('a, 't) marked_gexpr
-> (([< desugared | scopelang | dcalc | lcalc ] as 'a), 't) gexpr
(* Early stages *)
| ELocation : location -> (([< desugared | scopelang ] as 'a), 't) gexpr
| ELocation : 'a glocation -> (([< desugared | scopelang ] as 'a), 't) gexpr
| EStruct :
StructName.t * ('a, 't) marked_gexpr StructFieldMap.t
-> (([< desugared | scopelang ] as 'a), 't) gexpr
@ -212,10 +225,10 @@ and ('a, 't) gexpr =
('a, 't) marked_gexpr list * StructName.t option
-> (([< dcalc | lcalc ] as 'a), 't) gexpr
| ETupleAccess :
('a, 't) marked_gexpr * int * StructName.t option * typ Marked.pos list
('a, 't) marked_gexpr * int * StructName.t option * marked_typ list
-> (([< dcalc | lcalc ] as 'a), 't) gexpr
| EInj :
('a, 't) marked_gexpr * int * EnumName.t * typ Marked.pos list
('a, 't) marked_gexpr * int * EnumName.t * marked_typ list
-> (([< dcalc | lcalc ] as 'a), 't) gexpr
| EMatch :
('a, 't) marked_gexpr * ('a, 't) marked_gexpr list * EnumName.t
@ -330,10 +343,6 @@ and 'e scopes =
constraint 'e = ('a, 'm mark) gexpr
type struct_ctx = (StructFieldName.t * marked_typ) list StructMap.t
type decl_ctx = {
ctx_enums : (EnumConstructor.t * marked_typ) list EnumMap.t;
ctx_structs : struct_ctx;
}
type enum_ctx = (EnumConstructor.t * marked_typ) list EnumMap.t
type decl_ctx = { ctx_enums : enum_ctx; ctx_structs : struct_ctx }
type 'e program = { decl_ctx : decl_ctx; scopes : 'e scopes }

View File

@ -259,6 +259,23 @@ let make_multiple_let_in xs taus e1s e2 pos =
in
make_app (make_abs xs e2 taus m_abs) e1s m_e2
let make_default exceptions just cons mark =
let rec bool_value = function
| ELit (LBool b), _ -> Some b
| EApp ((EOp (Unop (Log (l, _))), _), [e]), _
when l <> PosRecordIfTrueBool
(* we don't remove the log calls corresponding to source code
definitions !*) ->
bool_value e
| _ -> None
in
match exceptions, bool_value just, cons with
| [], Some true, cons -> cons
| exceptions, Some true, (EDefault ([], just, cons), mark) ->
EDefault (exceptions, just, cons), mark
| [except], Some false, _ -> except
| exceptions, _, cons -> EDefault (exceptions, just, cons), mark
(* Tests *)
let is_value (type a) (e : (a, 'm mark) gexpr marked) =
@ -266,34 +283,137 @@ let is_value (type a) (e : (a, 'm mark) gexpr marked) =
| ELit _ | EAbs _ | EOp _ | ERaise _ -> true
| _ -> false
let rec equal_typs ty1 ty2 =
let equal_tlit l1 l2 = l1 = l2
let compare_tlit l1 l2 = Stdlib.compare l1 l2
let rec equal_typ ty1 ty2 =
match Marked.unmark ty1, Marked.unmark ty2 with
| TLit l1, TLit l2 -> l1 = l2
| TTuple tys1, TTuple tys2 -> equal_typs_list tys1 tys2
| TLit l1, TLit l2 -> equal_tlit l1 l2
| TTuple tys1, TTuple tys2 -> equal_typ_list tys1 tys2
| TStruct n1, TStruct n2 -> StructName.equal n1 n2
| TEnum n1, TEnum n2 -> EnumName.equal n1 n2
| TOption t1, TOption t2 -> equal_typs t1 t2
| TArrow (t1, t1'), TArrow (t2, t2') -> equal_typs t1 t2 && equal_typs t1' t2'
| TArray t1, TArray t2 -> equal_typs t1 t2
| TOption t1, TOption t2 -> equal_typ t1 t2
| TArrow (t1, t1'), TArrow (t2, t2') -> equal_typ t1 t2 && equal_typ t1' t2'
| TArray t1, TArray t2 -> equal_typ t1 t2
| TAny, TAny -> true
| ( ( TLit _ | TTuple _ | TStruct _ | TEnum _ | TOption _ | TArrow _
| TArray _ | TAny ),
_ ) ->
false
and equal_typs_list tys1 tys2 =
try List.for_all2 equal_typs tys1 tys2 with Invalid_argument _ -> false
and equal_typ_list tys1 tys2 =
try List.for_all2 equal_typ tys1 tys2 with Invalid_argument _ -> false
let rec compare_typ ty1 ty2 =
match Marked.unmark ty1, Marked.unmark ty2 with
| TLit l1, TLit l2 -> compare_tlit l1 l2
| TTuple tys1, TTuple tys2 -> List.compare compare_typ tys1 tys2
| TStruct n1, TStruct n2 -> StructName.compare n1 n2
| TEnum en1, TEnum en2 -> EnumName.compare en1 en2
| TOption t1, TOption t2 -> compare_typ t1 t2
| TArrow (a1, b1), TArrow (a2, b2) -> (
match compare_typ a1 a2 with 0 -> compare_typ b1 b2 | n -> n)
| TArray t1, TArray t2 -> compare_typ t1 t2
| TAny, TAny -> 0
| TLit _, _ -> -1
| _, TLit _ -> 1
| TTuple _, _ -> -1
| _, TTuple _ -> 1
| TStruct _, _ -> -1
| _, TStruct _ -> 1
| TEnum _, _ -> -1
| _, TEnum _ -> 1
| TOption _, _ -> -1
| _, TOption _ -> 1
| TArrow _, _ -> -1
| _, TArrow _ -> 1
| TArray _, _ -> -1
| _, TArray _ -> 1
let equal_lit (type a) (l1 : a glit) (l2 : a glit) =
match l1, l2 with
| LBool b1, LBool b2 -> Bool.equal b1 b2
| LEmptyError, LEmptyError -> true
| LInt n1, LInt n2 -> Runtime.( =! ) n1 n2
| LRat r1, LRat r2 -> Runtime.( =& ) r1 r2
| LMoney m1, LMoney m2 -> Runtime.( =$ ) m1 m2
| LUnit, LUnit -> true
| LDate d1, LDate d2 -> Runtime.( =@ ) d1 d2
| LDuration d1, LDuration d2 -> Runtime.( =^ ) d1 d2
| ( ( LBool _ | LEmptyError | LInt _ | LRat _ | LMoney _ | LUnit | LDate _
| LDuration _ ),
_ ) ->
false
let compare_lit (type a) (l1 : a glit) (l2 : a glit) =
match l1, l2 with
| LBool b1, LBool b2 -> Bool.compare b1 b2
| LEmptyError, LEmptyError -> 0
| LInt n1, LInt n2 ->
if Runtime.( <! ) n1 n2 then -1 else if Runtime.( =! ) n1 n2 then 0 else 1
| LRat r1, LRat r2 ->
if Runtime.( <& ) r1 r2 then -1 else if Runtime.( =& ) r1 r2 then 0 else 1
| LMoney m1, LMoney m2 ->
if Runtime.( <$ ) m1 m2 then -1 else if Runtime.( =$ ) m1 m2 then 0 else 1
| LUnit, LUnit -> 0
| LDate d1, LDate d2 ->
if Runtime.( <@ ) d1 d2 then -1 else if Runtime.( =@ ) d1 d2 then 0 else 1
| LDuration d1, LDuration d2 -> (
(* Duration comparison in the runtime may fail, so rely on a basic
lexicographic comparison instead *)
let y1, m1, d1 = Runtime.duration_to_years_months_days d1 in
let y2, m2, d2 = Runtime.duration_to_years_months_days d2 in
match compare y1 y2 with
| 0 -> ( match compare m1 m2 with 0 -> compare d1 d2 | n -> n)
| n -> n)
| LBool _, _ -> -1
| _, LBool _ -> 1
| LEmptyError, _ -> -1
| _, LEmptyError -> 1
| LInt _, _ -> -1
| _, LInt _ -> 1
| LRat _, _ -> -1
| _, LRat _ -> 1
| LMoney _, _ -> -1
| _, LMoney _ -> 1
| LUnit, _ -> -1
| _, LUnit -> 1
| LDate _, _ -> -1
| _, LDate _ -> 1
| LDuration _, _ -> .
| _, LDuration _ -> .
let equal_log_entries l1 l2 =
match l1, l2 with
| VarDef t1, VarDef t2 -> equal_typs (t1, Pos.no_pos) (t2, Pos.no_pos)
| VarDef t1, VarDef t2 -> equal_typ (t1, Pos.no_pos) (t2, Pos.no_pos)
| x, y -> x = y
let compare_log_entries l1 l2 =
match l1, l2 with
| VarDef t1, VarDef t2 -> compare_typ (t1, Pos.no_pos) (t2, Pos.no_pos)
| BeginCall, BeginCall
| EndCall, EndCall
| PosRecordIfTrueBool, PosRecordIfTrueBool ->
0
| VarDef _, _ -> -1
| _, VarDef _ -> 1
| BeginCall, _ -> -1
| _, BeginCall -> 1
| EndCall, _ -> -1
| _, EndCall -> 1
| PosRecordIfTrueBool, _ -> .
| _, PosRecordIfTrueBool -> .
(* let equal_op_kind = Stdlib.(=) *)
let compare_op_kind = Stdlib.compare
let equal_unops op1 op2 =
match op1, op2 with
(* Log entries contain a typ which contain position information, we thus need
to descend into them *)
| Log (l1, info1), Log (l2, info2) -> equal_log_entries l1 l2 && info1 = info2
| Log (l1, info1), Log (l2, info2) ->
equal_log_entries l1 l2 && List.equal Uid.MarkedString.equal info1 info2
| Log _, _ | _, Log _ -> false
(* All the other cases can be discharged through equality *)
| ( ( Not | Minus _ | Length | IntToRat | MoneyToRat | RatToMoney | GetDay
@ -302,37 +422,104 @@ let equal_unops op1 op2 =
_ ) ->
op1 = op2
let compare_unops op1 op2 =
match op1, op2 with
| Not, Not -> 0
| Minus k1, Minus k2 -> compare_op_kind k1 k2
| Log (l1, info1), Log (l2, info2) -> (
match compare_log_entries l1 l2 with
| 0 -> List.compare Uid.MarkedString.compare info1 info2
| n -> n)
| Length, Length
| IntToRat, IntToRat
| MoneyToRat, MoneyToRat
| RatToMoney, RatToMoney
| GetDay, GetDay
| GetMonth, GetMonth
| GetYear, GetYear
| FirstDayOfMonth, FirstDayOfMonth
| LastDayOfMonth, LastDayOfMonth
| RoundMoney, RoundMoney
| RoundDecimal, RoundDecimal ->
0
| Not, _ -> -1
| _, Not -> 1
| Minus _, _ -> -1
| _, Minus _ -> 1
| Log _, _ -> -1
| _, Log _ -> 1
| Length, _ -> -1
| _, Length -> 1
| IntToRat, _ -> -1
| _, IntToRat -> 1
| MoneyToRat, _ -> -1
| _, MoneyToRat -> 1
| RatToMoney, _ -> -1
| _, RatToMoney -> 1
| GetDay, _ -> -1
| _, GetDay -> 1
| GetMonth, _ -> -1
| _, GetMonth -> 1
| GetYear, _ -> -1
| _, GetYear -> 1
| FirstDayOfMonth, _ -> -1
| _, FirstDayOfMonth -> 1
| LastDayOfMonth, _ -> -1
| _, LastDayOfMonth -> 1
| RoundMoney, _ -> -1
| _, RoundMoney -> 1
| RoundDecimal, _ -> .
| _, RoundDecimal -> .
let equal_binop = Stdlib.( = )
let compare_binop = Stdlib.compare
let equal_ternop = Stdlib.( = )
let compare_ternop = Stdlib.compare
let equal_ops op1 op2 =
match op1, op2 with
| Ternop op1, Ternop op2 -> op1 = op2
| Binop op1, Binop op2 -> op1 = op2
| Ternop op1, Ternop op2 -> equal_ternop op1 op2
| Binop op1, Binop op2 -> equal_binop op1 op2
| Unop op1, Unop op2 -> equal_unops op1 op2
| _, _ -> false
let compare_op op1 op2 =
match op1, op2 with
| Ternop op1, Ternop op2 -> compare_ternop op1 op2
| Binop op1, Binop op2 -> compare_binop op1 op2
| Unop op1, Unop op2 -> compare_unops op1 op2
| Ternop _, _ -> -1
| _, Ternop _ -> 1
| Binop _, _ -> -1
| _, Binop _ -> 1
| Unop _, _ -> .
| _, Unop _ -> .
let equal_except ex1 ex2 = ex1 = ex2
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 marked list -> ('a, 't) gexpr marked list -> bool =
'a. ('a, 't) marked_gexpr list -> ('a, 't) marked_gexpr list -> bool =
fun es1 es2 ->
try List.for_all2 equal es1 es2 with Invalid_argument _ -> false
and equal : type a. (a, 't) gexpr marked -> (a, 't) gexpr marked -> bool =
and equal : type a. (a, 't) marked_gexpr -> (a, 't) marked_gexpr -> bool =
fun e1 e2 ->
match Marked.unmark e1, Marked.unmark e2 with
| EVar v1, EVar v2 -> Bindlib.eq_vars v1 v2
| ETuple (es1, n1), ETuple (es2, n2) -> n1 = n2 && equal_list es1 es2
| ETupleAccess (e1, id1, n1, tys1), ETupleAccess (e2, id2, n2, tys2) ->
equal e1 e2 && id1 = id2 && n1 = n2 && equal_typs_list tys1 tys2
equal e1 e2 && id1 = id2 && n1 = n2 && equal_typ_list tys1 tys2
| EInj (e1, id1, n1, tys1), EInj (e2, id2, n2, tys2) ->
equal e1 e2 && id1 = id2 && n1 = n2 && equal_typs_list tys1 tys2
equal e1 e2 && id1 = id2 && n1 = n2 && equal_typ_list tys1 tys2
| EMatch (e1, cases1, n1), EMatch (e2, cases2, n2) ->
n1 = n2 && equal e1 e2 && equal_list cases1 cases2
| EArray es1, EArray es2 -> equal_list es1 es2
| ELit l1, ELit l2 -> l1 = l2
| EAbs (b1, tys1), EAbs (b2, tys2) ->
equal_typs_list tys1 tys2
equal_typ_list tys1 tys2
&&
let vars1, body1 = Bindlib.unmbind b1 in
let body2 = Bindlib.msubst b2 (Array.map (fun x -> EVar x) vars1) in
@ -366,6 +553,103 @@ and equal : type a. (a, 't) gexpr marked -> (a, 't) gexpr marked -> bool =
_ ) ->
false
let rec compare : type a. (a, _) marked_gexpr -> (a, _) marked_gexpr -> int =
fun e1 e2 ->
(* Infix operator to chain comparisons lexicographically. *)
let ( @@< ) cmp1 cmpf = match cmp1 with 0 -> cmpf () | n -> n in
(* OCamlformat doesn't know to keep consistency in match cases so disabled
locally for readability *)
match[@ocamlformat "disable"] Marked.unmark e1, Marked.unmark e2 with
| ELit l1, ELit l2 ->
compare_lit l1 l2
| EApp (f1, args1), EApp (f2, args2) ->
compare f1 f2 @@< fun () ->
List.compare compare args1 args2
| EOp op1, EOp op2 ->
compare_op op1 op2
| EArray a1, EArray a2 ->
List.compare compare a1 a2
| EVar v1, EVar v2 ->
Bindlib.compare_vars v1 v2
| EAbs (binder1, typs1), EAbs (binder2, typs2) ->
List.compare compare_typ typs1 typs2 @@< fun () ->
let _, e1, e2 = Bindlib.unmbind2 binder1 binder2 in
compare e1 e2
| EIfThenElse (i1, t1, e1), EIfThenElse (i2, t2, e2) ->
compare i1 i2 @@< fun () ->
compare t1 t2 @@< fun () ->
compare e1 e2
| ELocation _, ELocation _ ->
0
| EStruct (name1, field_map1), EStruct (name2, field_map2) ->
StructName.compare name1 name2 @@< fun () ->
StructFieldMap.compare compare field_map1 field_map2
| EStructAccess (e1, field_name1, struct_name1),
EStructAccess (e2, field_name2, struct_name2) ->
compare e1 e2 @@< fun () ->
StructFieldName.compare field_name1 field_name2 @@< fun () ->
StructName.compare struct_name1 struct_name2
| EEnumInj (e1, cstr1, name1), EEnumInj (e2, cstr2, name2) ->
compare e1 e2 @@< fun () ->
EnumName.compare name1 name2 @@< fun () ->
EnumConstructor.compare cstr1 cstr2
| EMatchS (e1, name1, emap1), EMatchS (e2, name2, emap2) ->
compare e1 e2 @@< fun () ->
EnumName.compare name1 name2 @@< fun () ->
EnumConstructorMap.compare compare emap1 emap2
| ETuple (es1, s1), ETuple (es2, s2) ->
Option.compare StructName.compare s1 s2 @@< fun () ->
List.compare compare es1 es2
| ETupleAccess (e1, n1, s1, tys1), ETupleAccess (e2, n2, s2, tys2) ->
Option.compare StructName.compare s1 s2 @@< fun () ->
Int.compare n1 n2 @@< fun () ->
List.compare compare_typ tys1 tys2 @@< fun () ->
compare e1 e2
| EInj (e1, n1, name1, ts1), EInj (e2, n2, name2, ts2) ->
EnumName.compare name1 name2 @@< fun () ->
Int.compare n1 n2 @@< fun () ->
List.compare compare_typ ts1 ts2 @@< fun () ->
compare e1 e2
| EMatch (e1, cases1, n1), EMatch (e2, cases2, n2) ->
EnumName.compare n1 n2 @@< fun () ->
compare e1 e2 @@< fun () ->
List.compare compare cases1 cases2
| EAssert e1, EAssert e2 ->
compare e1 e2
| EDefault (exs1, just1, cons1), EDefault (exs2, just2, cons2) ->
compare just1 just2 @@< fun () ->
compare cons1 cons2 @@< fun () ->
List.compare compare exs1 exs2
| ErrorOnEmpty e1, ErrorOnEmpty e2 ->
compare e1 e2
| ERaise ex1, ERaise ex2 ->
compare_except ex1 ex2
| ECatch (etry1, ex1, ewith1), ECatch (etry2, ex2, ewith2) ->
compare_except ex1 ex2 @@< fun () ->
compare etry1 etry2 @@< fun () ->
compare ewith1 ewith2
| ELit _, _ -> -1 | _, ELit _ -> 1
| EApp _, _ -> -1 | _, EApp _ -> 1
| EOp _, _ -> -1 | _, EOp _ -> 1
| EArray _, _ -> -1 | _, EArray _ -> 1
| EVar _, _ -> -1 | _, EVar _ -> 1
| EAbs _, _ -> -1 | _, EAbs _ -> 1
| EIfThenElse _, _ -> -1 | _, EIfThenElse _ -> 1
| ELocation _, _ -> -1 | _, ELocation _ -> 1
| EStruct _, _ -> -1 | _, EStruct _ -> 1
| EStructAccess _, _ -> -1 | _, EStructAccess _ -> 1
| EEnumInj _, _ -> -1 | _, EEnumInj _ -> 1
| EMatchS _, _ -> -1 | _, EMatchS _ -> 1
| ETuple _, _ -> -1 | _, ETuple _ -> 1
| ETupleAccess _, _ -> -1 | _, ETupleAccess _ -> 1
| EInj _, _ -> -1 | _, EInj _ -> 1
| EMatch _, _ -> -1 | _, EMatch _ -> 1
| EAssert _, _ -> -1 | _, EAssert _ -> 1
| EDefault _, _ -> -1 | _, EDefault _ -> 1
| ErrorOnEmpty _, _ -> . | _, ErrorOnEmpty _ -> .
| ERaise _, _ -> -1 | _, ERaise _ -> 1
| ECatch _, _ -> . | _, ECatch _ -> .
let rec free_vars : type a. (a, 't) gexpr marked -> (a, 't) gexpr Var.Set.t =
fun e ->
match Marked.unmark e with

View File

@ -174,11 +174,11 @@ val map_marks :
val make_var : 'a Bindlib.var * 'b -> ('a * 'b) Bindlib.box
val make_abs :
'e Var.vars ->
(('a, 'm mark) gexpr as 'e) marked Bindlib.box ->
('a, 't) gexpr Var.vars ->
('a, 't) marked_gexpr Bindlib.box ->
typ Marked.pos list ->
'm mark ->
'e marked Bindlib.box
't ->
('a, 't) marked_gexpr Bindlib.box
val make_app :
((_ any, 'm mark) gexpr as 'e) marked Bindlib.box ->
@ -205,6 +205,25 @@ val make_multiple_let_in :
Pos.t ->
'e marked Bindlib.box
val make_default :
(([< desugared | scopelang | dcalc ] as 'a), 't) marked_gexpr list ->
('a, 't) marked_gexpr ->
('a, 't) marked_gexpr ->
't ->
('a, 't) marked_gexpr
(** [make_default ?pos exceptions just cons] builds a term semantically
equivalent to [<exceptions | just :- cons>] (the [EDefault] constructor)
while avoiding redundant nested constructions. The position is extracted
from [just] by default.
Note that, due to the simplifications taking place, the result might not be
of the form [EDefault]:
- [<true :- x>] is rewritten as [x]
- [<ex | true :- def>], when [def] is a default term [<j :- c>] without
exceptions, is collapsed into [<ex | def>]
- [<ex | false :- _>], when [ex] is a single exception, is rewritten as [ex] *)
(** {2 Transformations} *)
val remove_logging_calls :
@ -221,11 +240,18 @@ val format :
(** {2 Analysis and tests} *)
val is_value : (_ any, 'm mark) gexpr marked -> bool
val equal_lit : 'a glit -> 'a glit -> bool
val compare_lit : 'a glit -> 'a glit -> int
val equal : ('a, 'm mark) gexpr marked -> ('a, 'm mark) gexpr marked -> bool
val equal : ('a, 't) marked_gexpr -> ('a, 't) marked_gexpr -> bool
(** Determines if two expressions are equal, omitting their position information *)
val compare : ('a, 't) marked_gexpr -> ('a, 't) marked_gexpr -> int
(** Standard comparison function, suitable for e.g. [Set.Make]. Ignores position
information *)
val compare_typ : marked_typ -> marked_typ -> int
val is_value : (_ any, 'm mark) gexpr marked -> bool
val free_vars : 'e marked -> 'e Var.Set.t
val size : (_ any, 't) gexpr marked -> int

View File

@ -18,8 +18,8 @@ open Utils
open String_common
open Definitions
let typ_needs_parens (e : typ) : bool =
match e with TArrow _ | TArray _ -> true | _ -> false
let typ_needs_parens (ty : marked_typ) : bool =
match Marked.unmark ty with TArrow _ | TArray _ -> true | _ -> false
let uid_list (fmt : Format.formatter) (infos : Uid.MarkedString.info list) :
unit =
@ -59,9 +59,12 @@ let tlit (fmt : Format.formatter) (l : typ_lit) : unit =
| TDuration -> "duration"
| TDate -> "date")
let location (fmt : Format.formatter) (l : location) : unit =
let location (type a) (fmt : Format.formatter) (l : a glocation) : unit =
match l with
| ScopeVar v -> Format.fprintf fmt "%a" ScopeVar.format_t (Marked.unmark v)
| DesugaredScopeVar (v, _st) ->
Format.fprintf fmt "%a" ScopeVar.format_t (Marked.unmark v)
| ScopelangScopeVar v ->
Format.fprintf fmt "%a" ScopeVar.format_t (Marked.unmark v)
| SubScopeVar (_, subindex, subvar) ->
Format.fprintf fmt "%a.%a" SubScopeName.format_t (Marked.unmark subindex)
ScopeVar.format_t (Marked.unmark subvar)
@ -71,20 +74,20 @@ let enum_constructor (fmt : Format.formatter) (c : EnumConstructor.t) : unit =
(Utils.Cli.format_with_style [ANSITerminal.magenta])
(Format.asprintf "%a" EnumConstructor.format_t c)
let rec typ (ctx : decl_ctx) (fmt : Format.formatter) (ty : typ) : unit =
let rec typ (ctx : decl_ctx) (fmt : Format.formatter) (ty : marked_typ) : unit =
let typ = typ ctx in
let typ_with_parens (fmt : Format.formatter) (t : typ) =
let typ_with_parens (fmt : Format.formatter) (t : marked_typ) =
if typ_needs_parens t then Format.fprintf fmt "(%a)" typ t
else Format.fprintf fmt "%a" typ t
in
match ty with
match Marked.unmark ty with
| TLit l -> tlit fmt l
| TTuple ts ->
Format.fprintf fmt "@[<hov 2>(%a)@]"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ %a@ " operator "*")
(fun fmt t -> Format.fprintf fmt "%a" typ t))
(List.map Marked.unmark ts)
ts
| TStruct s ->
Format.fprintf fmt "@[<hov 2>%a%a%a%a@]" StructName.format_t s punctuation
"{"
@ -93,7 +96,7 @@ let rec typ (ctx : decl_ctx) (fmt : Format.formatter) (ty : typ) : unit =
(fun fmt (field, mty) ->
Format.fprintf fmt "%a%a%a%a@ %a" punctuation "\""
StructFieldName.format_t field punctuation "\"" punctuation ":" typ
(Marked.unmark mty)))
mty))
(StructMap.find s ctx.ctx_structs)
punctuation "}"
| TEnum e ->
@ -102,18 +105,14 @@ let rec typ (ctx : decl_ctx) (fmt : Format.formatter) (ty : typ) : unit =
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ %a@ " punctuation "|")
(fun fmt (case, mty) ->
Format.fprintf fmt "%a%a@ %a" enum_constructor case punctuation ":"
typ (Marked.unmark mty)))
typ mty))
(EnumMap.find e ctx.ctx_enums)
punctuation "]"
| TOption t ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" base_type "option" typ
(Marked.unmark t)
| TOption t -> Format.fprintf fmt "@[<hov 2>%a@ %a@]" base_type "option" typ t
| TArrow (t1, t2) ->
Format.fprintf fmt "@[<hov 2>%a %a@ %a@]" typ_with_parens (Marked.unmark t1)
operator "" typ (Marked.unmark t2)
| TArray t1 ->
Format.fprintf fmt "@[<hov 2>%a@ %a@]" base_type "array" typ
(Marked.unmark t1)
Format.fprintf fmt "@[<hov 2>%a %a@ %a@]" typ_with_parens t1 operator ""
typ t2
| TArray t1 -> Format.fprintf fmt "@[<hov 2>%a@ %a@]" base_type "array" typ t1
| TAny -> base_type fmt "any"
let lit (type a) (fmt : Format.formatter) (l : a glit) : unit =
@ -206,21 +205,21 @@ let except (fmt : Format.formatter) (exn : except) : unit =
| Crash -> "Crash"
| NoValueProvided -> "NoValueProvided")
let needs_parens (type a) (e : (a, _) gexpr marked) : bool =
match Marked.unmark e with EAbs _ | ETuple (_, Some _) -> true | _ -> false
let var fmt v =
Format.fprintf fmt "%s_%d" (Bindlib.name_of v) (Bindlib.uid_of v)
let needs_parens (type a) (e : (a, _) marked_gexpr) : bool =
match Marked.unmark e with EAbs _ | ETuple (_, Some _) -> true | _ -> false
let rec expr :
'a.
?debug:bool ->
decl_ctx ->
Format.formatter ->
('a, 't) gexpr marked ->
('a, 't) marked_gexpr ->
unit =
fun (type a) ?(debug : bool = false) (ctx : decl_ctx) (fmt : Format.formatter)
(e : (a, 't) gexpr marked) ->
(e : (a, 't) marked_gexpr) ->
let expr e = expr ~debug ctx e in
let with_parens fmt e =
if needs_parens e then (
@ -278,9 +277,7 @@ let rec expr :
| ELit l -> lit fmt l
| EApp ((EAbs (binder, taus), _), args) ->
let xs, body = Bindlib.unmbind binder in
let xs_tau =
List.map2 (fun x tau -> x, Marked.unmark tau) (Array.to_list xs) taus
in
let xs_tau = List.mapi (fun i tau -> xs.(i), tau) taus in
let xs_tau_arg = List.map2 (fun (x, tau) arg -> x, tau, arg) xs_tau args in
Format.fprintf fmt "%a%a"
(Format.pp_print_list
@ -292,9 +289,7 @@ let rec expr :
xs_tau_arg expr body
| EAbs (binder, taus) ->
let xs, body = Bindlib.unmbind binder in
let xs_tau =
List.map2 (fun x tau -> x, Marked.unmark tau) (Array.to_list xs) taus
in
let xs_tau = List.mapi (fun i tau -> xs.(i), tau) taus in
Format.fprintf fmt "@[<hov 2>%a @[<hov 2>%a@] %a@ %a@]" punctuation "λ"
(Format.pp_print_list
~pp_sep:(fun fmt () -> Format.fprintf fmt "@ ")

View File

@ -32,7 +32,8 @@ val lit_style : Format.formatter -> string -> unit
val uid_list : Format.formatter -> Uid.MarkedString.info list -> unit
val enum_constructor : Format.formatter -> EnumConstructor.t -> unit
val tlit : Format.formatter -> typ_lit -> unit
val typ : decl_ctx -> Format.formatter -> typ -> unit
val location : Format.formatter -> 'a glocation -> unit
val typ : decl_ctx -> Format.formatter -> marked_typ -> unit
val lit : Format.formatter -> 'a glit -> unit
val op_kind : Format.formatter -> op_kind -> unit
val binop : Format.formatter -> binop -> unit
@ -46,5 +47,5 @@ val expr :
?debug:bool (** [true] for debug printing *) ->
decl_ctx ->
Format.formatter ->
'e marked ->
('a, 't) marked_gexpr ->
unit

View File

@ -253,19 +253,15 @@ let rec translate_expr
| [] -> None
| states -> (
match inside_definition_of with
| Some (Desugared.Ast.ScopeDef.Var (x'_uid, sx'), _)
when Desugared.Ast.ScopeVar.compare uid x'_uid = 0 -> (
| Some (Var (x'_uid, sx'), _) when ScopeVar.compare uid x'_uid = 0
-> (
match sx' with
| None ->
failwith
"inconsistent state: inside a definition of a variable with \
no state but variable has states"
| Some inside_def_state ->
if
Desugared.Ast.StateName.compare inside_def_state
(List.hd states)
= 0
then
if StateName.compare inside_def_state (List.hd states) = 0 then
Errors.raise_spanned_error pos
"It is impossible to refer to the variable you are \
defining when defining its first state."
@ -276,11 +272,8 @@ let rec translate_expr
ignore
(List.fold_left
(fun previous_state state ->
if
Desugared.Ast.StateName.compare inside_def_state
state
= 0
then correct_state := previous_state;
if StateName.equal inside_def_state state then
correct_state := previous_state;
Some state)
None states);
!correct_state)
@ -362,7 +355,7 @@ let rec translate_expr
(rec_helper f) (rec_helper arg)
| LetIn (x, e1, e2) ->
let ctxt, v = Name_resolution.add_def_local_var ctxt (Marked.unmark x) in
let tau = Scopelang.Ast.TAny, Marked.get_mark x in
let tau = TAny, Marked.get_mark x in
let fn =
Desugared.Ast.make_abs [| v |]
(translate_expr scope inside_definition_of ctxt e2)
@ -544,7 +537,7 @@ let rec translate_expr
let f_pred =
Desugared.Ast.make_abs [| param |]
(translate_expr scope inside_definition_of ctxt predicate)
[Scopelang.Ast.TAny, pos]
[TAny, pos]
pos
in
Bindlib.box_apply2
@ -587,7 +580,7 @@ let rec translate_expr
let f_pred =
Desugared.Ast.make_abs [| param |]
(translate_expr scope inside_definition_of ctxt predicate)
[Scopelang.Ast.TAny, pos]
[TAny, pos]
pos
in
let f_pred_var = Desugared.Ast.Var.make "predicate" in
@ -619,7 +612,7 @@ let rec translate_expr
in
let fold_f =
Desugared.Ast.make_abs [| acc_var; item_var |] fold_body
[Scopelang.Ast.TAny, pos; Scopelang.Ast.TAny, pos]
[TAny, pos; TAny, pos]
pos
in
let fold =
@ -631,7 +624,7 @@ let rec translate_expr
pos ))
fold_f collection init
in
Desugared.Ast.make_let_in f_pred_var (Scopelang.Ast.TAny, pos) f_pred fold
Desugared.Ast.make_let_in f_pred_var (TAny, pos) f_pred fold
| CollectionOp (op', param', collection, predicate) ->
let ctxt, param =
Name_resolution.add_def_local_var ctxt (Marked.unmark param')
@ -686,7 +679,7 @@ let rec translate_expr
(translate_expr scope inside_definition_of ctxt predicate)
acc
in
let make_extr_body (cmp_op : binop) (t : Scopelang.Ast.typ Marked.pos) =
let make_extr_body (cmp_op : binop) (t : typ Marked.pos) =
let tmp_var = Desugared.Ast.Var.make "tmp" in
let tmp = Desugared.Ast.make_var (tmp_var, Marked.get_mark param') in
Desugared.Ast.make_let_in tmp_var t
@ -719,11 +712,11 @@ let rec translate_expr
| Ast.Aggregate (Ast.AggregateExtremum (max_or_min, t, _)) ->
let op_kind, typ =
match t with
| Ast.Integer -> KInt, (Scopelang.Ast.TLit TInt, pos)
| Ast.Decimal -> KRat, (Scopelang.Ast.TLit TRat, pos)
| Ast.Money -> KMoney, (Scopelang.Ast.TLit TMoney, pos)
| Ast.Duration -> KDuration, (Scopelang.Ast.TLit TDuration, pos)
| Ast.Date -> KDate, (Scopelang.Ast.TLit TDate, pos)
| Ast.Integer -> KInt, (TLit TInt, pos)
| Ast.Decimal -> KRat, (TLit TRat, pos)
| Ast.Money -> KMoney, (TLit TMoney, pos)
| Ast.Duration -> KDuration, (TLit TDuration, pos)
| Ast.Date -> KDate, (TLit TDate, pos)
| _ ->
Errors.raise_spanned_error pos
"ssible to compute the %s of two values of type %a"
@ -758,8 +751,8 @@ let rec translate_expr
( Desugared.Ast.EAbs
( binder,
[
Scopelang.Ast.TLit t, Marked.get_mark op';
Scopelang.Ast.TAny, pos
TLit t, Marked.get_mark op';
TAny, pos
(* we put any here because the type of the elements of the
arrays is not always the type of the accumulator; for
instance in AggregateCount. *);
@ -820,9 +813,7 @@ let rec translate_expr
let f =
Bindlib.box_apply
(fun binder ->
( Desugared.Ast.EAbs
(binder, [Scopelang.Ast.TLit TBool, pos; Scopelang.Ast.TAny, pos]),
pos ))
Desugared.Ast.EAbs (binder, [TLit TBool, pos; TAny, pos]), pos)
(Bindlib.bind_mvar [| acc_var; param_var |] f_body)
in
Bindlib.box_apply3
@ -1037,9 +1028,8 @@ let process_default
Name_resolution.get_def_typ ctxt (Marked.unmark def_key)
in
match Marked.unmark def_key_typ, param_uid with
| Scopelang.Ast.TArrow (t_in, _), Some param_uid ->
Some (Marked.unmark param_uid, t_in)
| Scopelang.Ast.TArrow _, None ->
| TArrow (t_in, _), Some param_uid -> Some (Marked.unmark param_uid, t_in)
| TArrow _, None ->
Errors.raise_spanned_error
(Marked.get_mark (Bindlib.unbox cons))
"This definition has a function type but the parameter is missing"
@ -1375,8 +1365,7 @@ let desugar_program (ctxt : Name_resolution.context) (prgm : Ast.program) :
else
( Scopelang.Ast.NoInput,
Marked.get_mark
(Desugared.Ast.StateName
.get_info state) )
(StateName.get_info state) )
in
let io_output =
if i = List.length states - 1 then
@ -1384,8 +1373,7 @@ let desugar_program (ctxt : Name_resolution.context) (prgm : Ast.program) :
else
( false,
Marked.get_mark
(Desugared.Ast.StateName
.get_info state) )
(StateName.get_info state) )
in
{ io_input; io_output });
}

View File

@ -24,7 +24,6 @@ open Shared_ast
(** {1 Name resolution context} *)
type ident = string
type typ = Scopelang.Ast.typ
type unique_rulename =
| Ambiguous of Pos.t list
@ -36,8 +35,7 @@ type scope_def_context = {
}
type scope_context = {
var_idmap : Desugared.Ast.ScopeVar.t Desugared.Ast.IdentMap.t;
(** Scope variables *)
var_idmap : ScopeVar.t Desugared.Ast.IdentMap.t; (** Scope variables *)
scope_defs_contexts : scope_def_context Desugared.Ast.ScopeDefMap.t;
(** What is the default rule to refer to for unnamed exceptions, if any *)
sub_scopes_idmap : SubScopeName.t Desugared.Ast.IdentMap.t;
@ -57,8 +55,8 @@ type var_sig = {
var_sig_typ : typ Marked.pos;
var_sig_is_condition : bool;
var_sig_io : Ast.scope_decl_context_io;
var_sig_states_idmap : Desugared.Ast.StateName.t Desugared.Ast.IdentMap.t;
var_sig_states_list : Desugared.Ast.StateName.t list;
var_sig_states_idmap : StateName.t Desugared.Ast.IdentMap.t;
var_sig_states_list : StateName.t list;
}
type context = {
@ -102,22 +100,20 @@ let raise_unknown_identifier (msg : string) (ident : ident Marked.pos) =
msg
(** Gets the type associated to an uid *)
let get_var_typ (ctxt : context) (uid : Desugared.Ast.ScopeVar.t) :
typ Marked.pos =
let get_var_typ (ctxt : context) (uid : ScopeVar.t) : typ Marked.pos =
(Desugared.Ast.ScopeVarMap.find uid ctxt.var_typs).var_sig_typ
let is_var_cond (ctxt : context) (uid : Desugared.Ast.ScopeVar.t) : bool =
let is_var_cond (ctxt : context) (uid : ScopeVar.t) : bool =
(Desugared.Ast.ScopeVarMap.find uid ctxt.var_typs).var_sig_is_condition
let get_var_io (ctxt : context) (uid : Desugared.Ast.ScopeVar.t) :
Ast.scope_decl_context_io =
let get_var_io (ctxt : context) (uid : ScopeVar.t) : Ast.scope_decl_context_io =
(Desugared.Ast.ScopeVarMap.find uid ctxt.var_typs).var_sig_io
(** Get the variable uid inside the scope given in argument *)
let get_var_uid
(scope_uid : ScopeName.t)
(ctxt : context)
((x, pos) : ident Marked.pos) : Desugared.Ast.ScopeVar.t =
((x, pos) : ident Marked.pos) : ScopeVar.t =
let scope = Scopelang.Ast.ScopeMap.find scope_uid ctxt.scopes in
match Desugared.Ast.IdentMap.find_opt x scope.var_idmap with
| None ->
@ -144,13 +140,11 @@ let is_subscope_uid (scope_uid : ScopeName.t) (ctxt : context) (y : ident) :
Desugared.Ast.IdentMap.mem y scope.sub_scopes_idmap
(** Checks if the var_uid belongs to the scope scope_uid *)
let belongs_to
(ctxt : context)
(uid : Desugared.Ast.ScopeVar.t)
(scope_uid : ScopeName.t) : bool =
let belongs_to (ctxt : context) (uid : ScopeVar.t) (scope_uid : ScopeName.t) :
bool =
let scope = Scopelang.Ast.ScopeMap.find scope_uid ctxt.scopes in
Desugared.Ast.IdentMap.exists
(fun _ var_uid -> Desugared.Ast.ScopeVar.compare uid var_uid = 0)
(fun _ var_uid -> ScopeVar.compare uid var_uid = 0)
scope.var_idmap
(** Retrieves the type of a scope definition from the context *)
@ -226,30 +220,28 @@ let is_type_cond ((typ, _) : Ast.typ Marked.pos) =
(** Process a basic type (all types except function types) *)
let rec process_base_typ
(ctxt : context)
((typ, typ_pos) : Ast.base_typ Marked.pos) : Scopelang.Ast.typ Marked.pos =
((typ, typ_pos) : Ast.base_typ Marked.pos) : typ Marked.pos =
match typ with
| Ast.Condition -> Scopelang.Ast.TLit TBool, typ_pos
| Ast.Condition -> TLit TBool, typ_pos
| Ast.Data (Ast.Collection t) ->
( Scopelang.Ast.TArray
(Marked.unmark
(process_base_typ ctxt
(Ast.Data (Marked.unmark t), Marked.get_mark t))),
( TArray
(process_base_typ ctxt (Ast.Data (Marked.unmark t), Marked.get_mark t)),
typ_pos )
| Ast.Data (Ast.Primitive prim) -> (
match prim with
| Ast.Integer -> Scopelang.Ast.TLit TInt, typ_pos
| Ast.Decimal -> Scopelang.Ast.TLit TRat, typ_pos
| Ast.Money -> Scopelang.Ast.TLit TMoney, typ_pos
| Ast.Duration -> Scopelang.Ast.TLit TDuration, typ_pos
| Ast.Date -> Scopelang.Ast.TLit TDate, typ_pos
| Ast.Boolean -> Scopelang.Ast.TLit TBool, typ_pos
| Ast.Integer -> TLit TInt, typ_pos
| Ast.Decimal -> TLit TRat, typ_pos
| Ast.Money -> TLit TMoney, typ_pos
| Ast.Duration -> TLit TDuration, typ_pos
| Ast.Date -> TLit TDate, typ_pos
| Ast.Boolean -> TLit TBool, typ_pos
| Ast.Text -> raise_unsupported_feature "text type" typ_pos
| Ast.Named ident -> (
match Desugared.Ast.IdentMap.find_opt ident ctxt.struct_idmap with
| Some s_uid -> Scopelang.Ast.TStruct s_uid, typ_pos
| Some s_uid -> TStruct s_uid, typ_pos
| None -> (
match Desugared.Ast.IdentMap.find_opt ident ctxt.enum_idmap with
| Some e_uid -> Scopelang.Ast.TEnum e_uid, typ_pos
| Some e_uid -> TEnum e_uid, typ_pos
| None ->
Errors.raise_spanned_error typ_pos
"Unknown type \"%a\", not a struct or enum previously declared"
@ -258,12 +250,11 @@ let rec process_base_typ
(** Process a type (function or not) *)
let process_type (ctxt : context) ((typ, typ_pos) : Ast.typ Marked.pos) :
Scopelang.Ast.typ Marked.pos =
typ Marked.pos =
match typ with
| Ast.Base base_typ -> process_base_typ ctxt (base_typ, typ_pos)
| Ast.Func { arg_typ; return_typ } ->
( Scopelang.Ast.TArrow
(process_base_typ ctxt arg_typ, process_base_typ ctxt return_typ),
( TArrow (process_base_typ ctxt arg_typ, process_base_typ ctxt return_typ),
typ_pos )
(** Process data declaration *)
@ -280,14 +271,14 @@ let process_data_decl
| Some use ->
Errors.raise_multispanned_error
[
Some "First use:", Marked.get_mark (Desugared.Ast.ScopeVar.get_info use);
Some "First use:", Marked.get_mark (ScopeVar.get_info use);
Some "Second use:", pos;
]
"Variable name \"%a\" already used"
(Utils.Cli.format_with_style [ANSITerminal.yellow])
name
| None ->
let uid = Desugared.Ast.ScopeVar.fresh (name, pos) in
let uid = ScopeVar.fresh (name, pos) in
let scope_ctxt =
{
scope_ctxt with
@ -297,7 +288,7 @@ let process_data_decl
let states_idmap, states_list =
List.fold_right
(fun state_id (states_idmap, states_list) ->
let state_uid = Desugared.Ast.StateName.fresh state_id in
let state_uid = StateName.fresh state_id in
( Desugared.Ast.IdentMap.add (Marked.unmark state_id) state_uid
states_idmap,
state_uid :: states_list ))
@ -429,7 +420,7 @@ let process_enum_decl (ctxt : context) (edecl : Ast.enum_decl) : context =
(fun cases ->
let typ =
match cdecl.Ast.enum_decl_case_typ with
| None -> Scopelang.Ast.TLit TUnit, cdecl_pos
| None -> TLit TUnit, cdecl_pos
| Some typ -> process_type ctxt typ
in
match cases with
@ -560,10 +551,10 @@ let get_def_key
[
None, Marked.get_mark state;
( Some "Variable declaration:",
Marked.get_mark (Desugared.Ast.ScopeVar.get_info x_uid) );
Marked.get_mark (ScopeVar.get_info x_uid) );
]
"This identifier is not a state declared for variable %a."
Desugared.Ast.ScopeVar.format_t x_uid)
ScopeVar.format_t x_uid)
| None ->
if not (Desugared.Ast.IdentMap.is_empty var_sig.var_sig_states_idmap)
then
@ -571,11 +562,11 @@ let get_def_key
[
None, Marked.get_mark x;
( Some "Variable declaration:",
Marked.get_mark (Desugared.Ast.ScopeVar.get_info x_uid) );
Marked.get_mark (ScopeVar.get_info x_uid) );
]
"This definition does not indicate which state has to be \
considered for variable %a."
Desugared.Ast.ScopeVar.format_t x_uid
ScopeVar.format_t x_uid
else None )
| [y; x] ->
let subscope_uid : SubScopeName.t = get_subscope_uid scope_uid ctxt y in

View File

@ -24,7 +24,6 @@ open Shared_ast
(** {1 Name resolution context} *)
type ident = string
type typ = Scopelang.Ast.typ
type unique_rulename =
| Ambiguous of Pos.t list
@ -36,8 +35,7 @@ type scope_def_context = {
}
type scope_context = {
var_idmap : Desugared.Ast.ScopeVar.t Desugared.Ast.IdentMap.t;
(** Scope variables *)
var_idmap : ScopeVar.t Desugared.Ast.IdentMap.t; (** Scope variables *)
scope_defs_contexts : scope_def_context Desugared.Ast.ScopeDefMap.t;
(** What is the default rule to refer to for unnamed exceptions, if any *)
sub_scopes_idmap : SubScopeName.t Desugared.Ast.IdentMap.t;
@ -57,8 +55,8 @@ type var_sig = {
var_sig_typ : typ Marked.pos;
var_sig_is_condition : bool;
var_sig_io : Ast.scope_decl_context_io;
var_sig_states_idmap : Desugared.Ast.StateName.t Desugared.Ast.IdentMap.t;
var_sig_states_list : Desugared.Ast.StateName.t list;
var_sig_states_idmap : StateName.t Desugared.Ast.IdentMap.t;
var_sig_states_list : StateName.t list;
}
type context = {
@ -96,16 +94,13 @@ val raise_unknown_identifier : string -> ident Marked.pos -> 'a
(** Function to call whenever an identifier used somewhere has not been declared
in the program previously *)
val get_var_typ : context -> Desugared.Ast.ScopeVar.t -> typ Marked.pos
val get_var_typ : context -> ScopeVar.t -> typ Marked.pos
(** Gets the type associated to an uid *)
val is_var_cond : context -> Desugared.Ast.ScopeVar.t -> bool
val is_var_cond : context -> ScopeVar.t -> bool
val get_var_io : context -> ScopeVar.t -> Ast.scope_decl_context_io
val get_var_io :
context -> Desugared.Ast.ScopeVar.t -> Ast.scope_decl_context_io
val get_var_uid :
ScopeName.t -> context -> ident Marked.pos -> Desugared.Ast.ScopeVar.t
val get_var_uid : ScopeName.t -> context -> ident Marked.pos -> ScopeVar.t
(** Get the variable uid inside the scope given in argument *)
val get_subscope_uid :
@ -116,7 +111,7 @@ val is_subscope_uid : ScopeName.t -> context -> ident -> bool
(** [is_subscope_uid scope_uid ctxt y] returns true if [y] belongs to the
subscopes of [scope_uid]. *)
val belongs_to : context -> Desugared.Ast.ScopeVar.t -> ScopeName.t -> bool
val belongs_to : context -> ScopeVar.t -> ScopeName.t -> bool
(** Checks if the var_uid belongs to the scope scope_uid *)
val get_def_typ : context -> Desugared.Ast.ScopeDef.t -> typ Marked.pos

View File

@ -19,6 +19,8 @@ module type Info = sig
val to_string : info -> string
val format_info : Format.formatter -> info -> unit
val equal : info -> info -> bool
val compare : info -> info -> int
end
module type Id = sig
@ -58,4 +60,6 @@ module MarkedString = struct
let to_string (s, _) = s
let format_info fmt i = Format.pp_print_string fmt (to_string i)
let equal i1 i2 = String.equal (Marked.unmark i1) (Marked.unmark i2)
let compare i1 i2 = String.compare (Marked.unmark i1) (Marked.unmark i2)
end

View File

@ -22,6 +22,12 @@ module type Info = sig
val to_string : info -> string
val format_info : Format.formatter -> info -> unit
val equal : info -> info -> bool
(** Equality disregards position *)
val compare : info -> info -> int
(** Comparison disregards position *)
end
module MarkedString : Info with type info = string Marked.pos

View File

@ -20,5 +20,5 @@ Type integer coming from expression:
--> tests/test_array/bad/fold_error.catala_en
|
5 | context list content collection integer
| ^^^^^^^^^^^^^^^^^^
| ^^^^^^^
+ Article

View File

@ -1,6 +1,5 @@
let scope Foo (y: integer|input) (x: integer|internal|output) =
let x : integer =
⟨⟨⟨⟨y = 4 ⊢ 4⟩, ⟨y = 5 ⊢ 5⟩ | false ⊢ ∅ ⟩ |
true ⊢
⟨⟨y = 2 ⊢ 2⟩, ⟨y = 3 ⊢ 3⟩ | false ⊢ ∅ ⟩⟩ |
⟨⟨⟨⟨y = 4 ⊢ 4⟩, ⟨y = 5 ⊢ 5⟩ | false ⊢ ∅ ⟩ | true
⊢ ⟨⟨y = 2 ⊢ 2⟩, ⟨y = 3 ⊢ 3⟩ | false ⊢ ∅ ⟩⟩ |
true ⊢ ⟨⟨y = 0 ⊢ 0⟩, ⟨y = 1 ⊢ 1⟩ | false ⊢ ∅ ⟩⟩