mirror of
https://github.com/CatalaLang/catala.git
synced 2024-11-08 07:51:43 +03:00
Reformat
This commit is contained in:
parent
0ec04c4925
commit
75bf768264
@ -16,7 +16,6 @@
|
||||
|
||||
open Catala_utils
|
||||
open Shared_ast
|
||||
|
||||
module S = Scopelang.Ast
|
||||
|
||||
type scope_var_ctx = {
|
||||
@ -150,8 +149,8 @@ let tag_with_log_entry
|
||||
|
||||
NOTE: the choice of the exception that will be triggered and show in the
|
||||
trace is arbitrary (but deterministic). *)
|
||||
let collapse_similar_outcomes (type m) (excepts : m S.expr list) :
|
||||
m S.expr list =
|
||||
let collapse_similar_outcomes (type m) (excepts : m S.expr list) : m S.expr list
|
||||
=
|
||||
let module ExprMap = Map.Make (struct
|
||||
type t = m S.expr
|
||||
|
||||
@ -213,8 +212,7 @@ let thunk_scope_arg var_ctx e =
|
||||
Expr.make_abs [| Var.make "_" |] e [TLit TUnit, pos] pos
|
||||
| _ -> assert false
|
||||
|
||||
let rec translate_expr (ctx : 'm ctx) (e : 'm S.expr) :
|
||||
'm Ast.expr boxed =
|
||||
let rec translate_expr (ctx : 'm ctx) (e : 'm S.expr) : 'm Ast.expr boxed =
|
||||
let m = Mark.get e in
|
||||
match Mark.remove e with
|
||||
| EMatch { e = e1; name; cases = e_cases } ->
|
||||
@ -575,9 +573,9 @@ let rec translate_expr (ctx : 'm ctx) (e : 'm S.expr) :
|
||||
| EIfThenElse _ | EAppOp _ ) as e ->
|
||||
Expr.map ~f:(translate_expr ctx) ~op:Operator.translate (e, m)
|
||||
|
||||
(** The result of a rule translation is a list of assignments, with variables and
|
||||
expressions. We also return the new translation context available after the
|
||||
assignment to use in later rule translations. The list is actually a
|
||||
(** The result of a rule translation is a list of assignments, with variables
|
||||
and expressions. We also return the new translation context available after
|
||||
the assignment to use in later rule translations. The list is actually a
|
||||
continuation yielding a [Dcalc.scope_body_expr] by giving it what should
|
||||
come later in the chain of let-bindings. *)
|
||||
let translate_rule
|
||||
@ -591,12 +589,13 @@ let translate_rule
|
||||
| S.ScopeVarDefinition { var; typ; e; _ }
|
||||
| S.SubScopeVarDefinition { var; typ; e; _ } ->
|
||||
let pos_mark, _ = pos_mark_mk e in
|
||||
let scope_let_kind, io = match rule with
|
||||
| S.ScopeVarDefinition {io; _} -> ScopeVarDefinition, io
|
||||
let scope_let_kind, io =
|
||||
match rule with
|
||||
| S.ScopeVarDefinition { io; _ } -> ScopeVarDefinition, io
|
||||
| S.SubScopeVarDefinition _ ->
|
||||
let pos = Mark.get var in
|
||||
SubScopeVarDefinition,
|
||||
{ io_input = (NoInput, pos); io_output = (false, pos) }
|
||||
( SubScopeVarDefinition,
|
||||
{ io_input = NoInput, pos; io_output = false, pos } )
|
||||
| S.Assertion _ -> assert false
|
||||
in
|
||||
let a_name = ScopeVar.get_info (Mark.remove var) in
|
||||
@ -763,9 +762,11 @@ let translate_scope_decl
|
||||
or not ? *)
|
||||
Message.raise_spanned_error pos_sigma "Scope %a has no content"
|
||||
ScopeName.format scope_name
|
||||
| (S.ScopeVarDefinition { e; _ }
|
||||
| ( S.ScopeVarDefinition { e; _ }
|
||||
| S.SubScopeVarDefinition { e; _ }
|
||||
| S.Assertion e) :: _ -> Mark.get e
|
||||
| S.Assertion e )
|
||||
:: _ ->
|
||||
Mark.get e
|
||||
in
|
||||
let rules_with_return_expr, ctx =
|
||||
translate_rules ctx scope_name sigma.scope_decl_rules sigma_info scope_mark
|
||||
|
@ -27,25 +27,29 @@ module ScopeDef = struct
|
||||
module Base = struct
|
||||
type kind =
|
||||
| Var of StateName.t option
|
||||
| SubScope of { name: ScopeName.t; var_within_origin_scope: ScopeVar.t }
|
||||
| SubScope of { name : ScopeName.t; var_within_origin_scope : ScopeVar.t }
|
||||
|
||||
type t = ScopeVar.t Mark.pos * kind
|
||||
|
||||
let equal_kind k1 k2 = match k1, k2 with
|
||||
let equal_kind k1 k2 =
|
||||
match k1, k2 with
|
||||
| Var s1, Var s2 -> Option.equal StateName.equal s1 s2
|
||||
| SubScope { var_within_origin_scope = v1; _ }, SubScope { var_within_origin_scope = v2; _ } -> ScopeVar.equal v1 v2
|
||||
| ( SubScope { var_within_origin_scope = v1; _ },
|
||||
SubScope { var_within_origin_scope = v2; _ } ) ->
|
||||
ScopeVar.equal v1 v2
|
||||
| (Var _ | SubScope _), _ -> false
|
||||
|
||||
let equal (v1, k1) (v2, k2) =
|
||||
ScopeVar.equal (Mark.remove v1) (Mark.remove v2) &&
|
||||
equal_kind k1 k2
|
||||
ScopeVar.equal (Mark.remove v1) (Mark.remove v2) && equal_kind k1 k2
|
||||
|
||||
let compare_kind k1 k2 = match k1, k2 with
|
||||
| Var st1, Var st2 -> Option.compare StateName.compare st1 st2
|
||||
| SubScope { var_within_origin_scope = v1; _ }, SubScope { var_within_origin_scope = v2; _ } ->
|
||||
ScopeVar.compare v1 v2
|
||||
| Var _, SubScope _ -> -1
|
||||
| SubScope _, Var _ -> 1
|
||||
let compare_kind k1 k2 =
|
||||
match k1, k2 with
|
||||
| Var st1, Var st2 -> Option.compare StateName.compare st1 st2
|
||||
| ( SubScope { var_within_origin_scope = v1; _ },
|
||||
SubScope { var_within_origin_scope = v2; _ } ) ->
|
||||
ScopeVar.compare v1 v2
|
||||
| Var _, SubScope _ -> -1
|
||||
| SubScope _, Var _ -> 1
|
||||
|
||||
let compare (v1, k1) (v2, k2) =
|
||||
match Mark.compare ScopeVar.compare v1 v2 with
|
||||
@ -57,19 +61,19 @@ module ScopeDef = struct
|
||||
let format_kind ppf = function
|
||||
| Var None -> ()
|
||||
| Var (Some st) -> Format.fprintf ppf "@%a" StateName.format st
|
||||
| SubScope { var_within_origin_scope = v; _ } -> Format.fprintf ppf ".%a" ScopeVar.format v
|
||||
| SubScope { var_within_origin_scope = v; _ } ->
|
||||
Format.fprintf ppf ".%a" ScopeVar.format v
|
||||
|
||||
let format ppf (v, k) =
|
||||
ScopeVar.format ppf (Mark.remove v);
|
||||
format_kind ppf k
|
||||
|
||||
let hash_kind = function
|
||||
| Var (None) -> 0
|
||||
| Var None -> 0
|
||||
| Var (Some st) -> StateName.hash st
|
||||
| SubScope { var_within_origin_scope = v; _ } -> ScopeVar.hash v
|
||||
|
||||
let hash (v, k) =
|
||||
Int.logxor (ScopeVar.hash (Mark.remove v)) (hash_kind k)
|
||||
let hash (v, k) = Int.logxor (ScopeVar.hash (Mark.remove v)) (hash_kind k)
|
||||
end
|
||||
|
||||
include Base
|
||||
@ -249,8 +253,7 @@ type program = {
|
||||
|
||||
let rec locations_used e : LocationSet.t =
|
||||
match e with
|
||||
| ELocation l, m ->
|
||||
LocationSet.singleton (l, Expr.mark_pos m)
|
||||
| ELocation l, m -> LocationSet.singleton (l, Expr.mark_pos m)
|
||||
| e ->
|
||||
Expr.shallow_fold
|
||||
(fun e -> LocationSet.union (locations_used e))
|
||||
@ -263,8 +266,7 @@ let free_variables (def : rule RuleName.Map.t) : Pos.t ScopeDef.Map.t =
|
||||
(fun (loc, loc_pos) acc ->
|
||||
let usage =
|
||||
match loc with
|
||||
| DesugaredScopeVar { name; state } ->
|
||||
Some (name, ScopeDef.Var state)
|
||||
| DesugaredScopeVar { name; state } -> Some (name, ScopeDef.Var state)
|
||||
| ToplevelVar _ -> None
|
||||
in
|
||||
match usage with
|
||||
|
@ -19,11 +19,12 @@
|
||||
open Catala_utils
|
||||
open Shared_ast
|
||||
|
||||
(** Inside a scope, a definition can refer to a variable (possibly an intermediate state thereof) or an input of a subscope. *)
|
||||
(** Inside a scope, a definition can refer to a variable (possibly an
|
||||
intermediate state thereof) or an input of a subscope. *)
|
||||
module ScopeDef : sig
|
||||
type kind =
|
||||
| Var of StateName.t option
|
||||
| SubScope of { name: ScopeName.t; var_within_origin_scope: ScopeVar.t }
|
||||
| SubScope of { name : ScopeName.t; var_within_origin_scope : ScopeVar.t }
|
||||
|
||||
val equal_kind : kind -> kind -> bool
|
||||
val compare_kind : kind -> kind -> int
|
||||
|
@ -179,7 +179,8 @@ let build_scope_dependencies (scope : Ast.scope) : ScopeDependencies.t =
|
||||
in
|
||||
(* then add the edges *)
|
||||
let g =
|
||||
let to_vertex (var, kind) = match kind with
|
||||
let to_vertex (var, kind) =
|
||||
match kind with
|
||||
| Ast.ScopeDef.Var st -> Vertex.Var (Mark.remove var, st)
|
||||
| Ast.ScopeDef.SubScope _ -> Vertex.Var (Mark.remove var, None)
|
||||
in
|
||||
@ -190,14 +191,14 @@ let build_scope_dependencies (scope : Ast.scope) : ScopeDependencies.t =
|
||||
let fv = Ast.free_variables def in
|
||||
Ast.ScopeDef.Map.fold
|
||||
(fun fv_def fv_def_pos g ->
|
||||
let v_used = to_vertex fv_def in
|
||||
if Vertex.equal v_used v_defined then
|
||||
Message.raise_spanned_error fv_def_pos
|
||||
"The variable %a is used in one of its definitions, but \
|
||||
recursion is forbidden in Catala"
|
||||
Ast.ScopeDef.format def_key;
|
||||
ScopeDependencies.add_edge_e g
|
||||
(ScopeDependencies.E.create v_used fv_def_pos v_defined))
|
||||
let v_used = to_vertex fv_def in
|
||||
if Vertex.equal v_used v_defined then
|
||||
Message.raise_spanned_error fv_def_pos
|
||||
"The variable %a is used in one of its definitions, but \
|
||||
recursion is forbidden in Catala"
|
||||
Ast.ScopeDef.format def_key;
|
||||
ScopeDependencies.add_edge_e g
|
||||
(ScopeDependencies.E.create v_used fv_def_pos v_defined))
|
||||
fv g)
|
||||
scope.scope_defs g
|
||||
in
|
||||
|
@ -84,10 +84,10 @@ let program prg =
|
||||
let vars =
|
||||
ScopeDef.Map.fold
|
||||
(fun (v, kind) def vars ->
|
||||
match kind with
|
||||
| ScopeDef.Var _ -> ScopeVar.Map.add (Mark.remove v) def.scope_def_typ vars
|
||||
| ScopeDef.SubScope _ -> vars
|
||||
)
|
||||
match kind with
|
||||
| ScopeDef.Var _ ->
|
||||
ScopeVar.Map.add (Mark.remove v) def.scope_def_typ vars
|
||||
| ScopeDef.SubScope _ -> vars)
|
||||
scope.scope_defs ScopeVar.Map.empty
|
||||
in
|
||||
(* at this stage, rule resolution and the corresponding encapsulation
|
||||
|
@ -482,8 +482,8 @@ let rec translate_expr
|
||||
| mod_id :: path ->
|
||||
get_str (Name_resolution.get_module_ctx ctxt mod_id) path
|
||||
in
|
||||
Expr.edstructaccess ~e ~field:(Mark.remove x)
|
||||
~name_opt:(get_str ctxt path) emark
|
||||
Expr.edstructaccess ~e ~field:(Mark.remove x) ~name_opt:(get_str ctxt path)
|
||||
emark
|
||||
| FunCall ((Builtin b, _), [arg]) ->
|
||||
let op, ty =
|
||||
match b with
|
||||
@ -1510,20 +1510,25 @@ let init_scope_defs
|
||||
(* Initializing the definitions of all scopes and subscope vars, with no rules
|
||||
yet inside *)
|
||||
let add_def _ v scope_def_map =
|
||||
let pos = match v with ScopeVar v | SubScope (v, _, _) -> Mark.get (ScopeVar.get_info v) in
|
||||
let new_def v_sig io = {
|
||||
Ast.scope_def_rules = RuleName.Map.empty;
|
||||
Ast.scope_def_typ = v_sig.Name_resolution.var_sig_typ;
|
||||
Ast.scope_def_is_condition = v_sig.var_sig_is_condition;
|
||||
Ast.scope_def_parameters = v_sig.var_sig_parameters;
|
||||
Ast.scope_def_io = io;
|
||||
} in
|
||||
let pos =
|
||||
match v with
|
||||
| ScopeVar v | SubScope (v, _, _) -> Mark.get (ScopeVar.get_info v)
|
||||
in
|
||||
let new_def v_sig io =
|
||||
{
|
||||
Ast.scope_def_rules = RuleName.Map.empty;
|
||||
Ast.scope_def_typ = v_sig.Name_resolution.var_sig_typ;
|
||||
Ast.scope_def_is_condition = v_sig.var_sig_is_condition;
|
||||
Ast.scope_def_parameters = v_sig.var_sig_parameters;
|
||||
Ast.scope_def_io = io;
|
||||
}
|
||||
in
|
||||
match v with
|
||||
| ScopeVar v -> (
|
||||
let v_sig = ScopeVar.Map.find v ctxt.Name_resolution.var_typs in
|
||||
match v_sig.var_sig_states_list with
|
||||
| [] ->
|
||||
let def_key = ((v, pos), Ast.ScopeDef.Var None) in
|
||||
let def_key = (v, pos), Ast.ScopeDef.Var None in
|
||||
Ast.ScopeDef.Map.add def_key
|
||||
(new_def v_sig (attribute_to_io v_sig.var_sig_io))
|
||||
scope_def_map
|
||||
@ -1535,9 +1540,9 @@ let init_scope_defs
|
||||
let def_key = (v, pos), Ast.ScopeDef.Var (Some state) in
|
||||
let original_io = attribute_to_io v_sig.var_sig_io in
|
||||
(* The first state should have the input I/O of the original
|
||||
variable, and the last state should have the output I/O
|
||||
of the original variable. All intermediate states shall
|
||||
have "internal" I/O.*)
|
||||
variable, and the last state should have the output I/O of the
|
||||
original variable. All intermediate states shall have
|
||||
"internal" I/O.*)
|
||||
let io_input =
|
||||
if i = 0 then original_io.io_input
|
||||
else NoInput, Mark.get (StateName.get_info state)
|
||||
@ -1563,32 +1568,41 @@ let init_scope_defs
|
||||
ctxt
|
||||
(ScopeName.path subscope_uid)
|
||||
in
|
||||
let var_def = {
|
||||
Ast.scope_def_rules = RuleName.Map.empty;
|
||||
Ast.scope_def_typ = TStruct sub_scope_def.scope_out_struct, Mark.get (ScopeVar.get_info v0);
|
||||
Ast.scope_def_is_condition = false;
|
||||
Ast.scope_def_parameters = None;
|
||||
Ast.scope_def_io = { io_input = NoInput, Mark.get forward_out; io_output = forward_out };
|
||||
} in
|
||||
let var_def =
|
||||
{
|
||||
Ast.scope_def_rules = RuleName.Map.empty;
|
||||
Ast.scope_def_typ =
|
||||
( TStruct sub_scope_def.scope_out_struct,
|
||||
Mark.get (ScopeVar.get_info v0) );
|
||||
Ast.scope_def_is_condition = false;
|
||||
Ast.scope_def_parameters = None;
|
||||
Ast.scope_def_io =
|
||||
{
|
||||
io_input = NoInput, Mark.get forward_out;
|
||||
io_output = forward_out;
|
||||
};
|
||||
}
|
||||
in
|
||||
let scope_def_map =
|
||||
Ast.ScopeDef.Map.add ((v0, pos), Ast.ScopeDef.Var None) var_def scope_def_map
|
||||
Ast.ScopeDef.Map.add
|
||||
((v0, pos), Ast.ScopeDef.Var None)
|
||||
var_def scope_def_map
|
||||
in
|
||||
Ident.Map.fold
|
||||
(fun _ v scope_def_map ->
|
||||
match v with
|
||||
| SubScope _ ->
|
||||
(* TODO: if we consider "input subscopes" at some point their inputs will need to be forwarded here *)
|
||||
(* TODO: if we consider "input subscopes" at some point their inputs
|
||||
will need to be forwarded here *)
|
||||
scope_def_map
|
||||
| ScopeVar v ->
|
||||
(* TODO: shouldn't we ignore internal variables too at this point
|
||||
? *)
|
||||
let v_sig = ScopeVar.Map.find v ctxt.Name_resolution.var_typs in
|
||||
let def_key =
|
||||
(v0, Mark.get (ScopeVar.get_info v)),
|
||||
Ast.ScopeDef.SubScope {
|
||||
name = subscope_uid;
|
||||
var_within_origin_scope = v;
|
||||
}
|
||||
( (v0, Mark.get (ScopeVar.get_info v)),
|
||||
Ast.ScopeDef.SubScope
|
||||
{ name = subscope_uid; var_within_origin_scope = v } )
|
||||
in
|
||||
Ast.ScopeDef.Map.add def_key
|
||||
{
|
||||
|
@ -27,8 +27,11 @@ let detect_empty_definitions (p : program) : unit =
|
||||
if
|
||||
(match scope_def_key with _, ScopeDef.Var _ -> true | _ -> false)
|
||||
&& RuleName.Map.is_empty scope_def.scope_def_rules
|
||||
&& not scope_def.scope_def_is_condition
|
||||
&& not (ScopeVar.Map.mem (Mark.remove (fst scope_def_key)) scope.scope_sub_scopes)
|
||||
&& (not scope_def.scope_def_is_condition)
|
||||
&& (not
|
||||
(ScopeVar.Map.mem
|
||||
(Mark.remove (fst scope_def_key))
|
||||
scope.scope_sub_scopes))
|
||||
&&
|
||||
match Mark.remove scope_def.scope_def_io.io_input with
|
||||
| NoInput -> true
|
||||
@ -254,7 +257,9 @@ let detect_dead_code (p : program) : unit =
|
||||
| Assertion _ -> true
|
||||
| Var (var, state) ->
|
||||
let scope_def =
|
||||
ScopeDef.Map.find ((var, Pos.no_pos), ScopeDef.Var state) scope.scope_defs
|
||||
ScopeDef.Map.find
|
||||
((var, Pos.no_pos), ScopeDef.Var state)
|
||||
scope.scope_defs
|
||||
in
|
||||
Mark.remove scope_def.scope_def_io.io_output
|
||||
(* A variable is initially alive if it is an output*)
|
||||
@ -263,14 +268,15 @@ let detect_dead_code (p : program) : unit =
|
||||
let emit_unused_warning vx =
|
||||
Message.emit_spanned_warning
|
||||
(Mark.get (Dependency.Vertex.info vx))
|
||||
"Unused varible: %a does not contribute to computing \
|
||||
any of scope %a outputs. Did you forget something?"
|
||||
Dependency.Vertex.format vx
|
||||
ScopeName.format scope_name
|
||||
"Unused varible: %a does not contribute to computing any of scope %a \
|
||||
outputs. Did you forget something?"
|
||||
Dependency.Vertex.format vx ScopeName.format scope_name
|
||||
in
|
||||
Dependency.ScopeDependencies.iter_vertex (fun vx ->
|
||||
if not (is_alive vx) &&
|
||||
Dependency.ScopeDependencies.succ scope_dependencies vx = []
|
||||
Dependency.ScopeDependencies.iter_vertex
|
||||
(fun vx ->
|
||||
if
|
||||
(not (is_alive vx))
|
||||
&& Dependency.ScopeDependencies.succ scope_dependencies vx = []
|
||||
then emit_unused_warning vx)
|
||||
scope_dependencies)
|
||||
p.program_root.module_scopes
|
||||
|
@ -163,10 +163,11 @@ let belongs_to (ctxt : context) (uid : ScopeVar.t) (scope_uid : ScopeName.t) :
|
||||
| _ -> false)
|
||||
scope.var_idmap
|
||||
|
||||
let get_var_def (def: Ast.ScopeDef.t) : ScopeVar.t =
|
||||
let get_var_def (def : Ast.ScopeDef.t) : ScopeVar.t =
|
||||
match def with
|
||||
| ((v, _), Ast.ScopeDef.Var _)
|
||||
| (_, Ast.ScopeDef.SubScope { var_within_origin_scope = v; _ }) -> v
|
||||
| (v, _), Ast.ScopeDef.Var _
|
||||
| _, Ast.ScopeDef.SubScope { var_within_origin_scope = v; _ } ->
|
||||
v
|
||||
|
||||
(** Retrieves the type of a scope definition from the context *)
|
||||
let get_params (ctxt : context) (def : Ast.ScopeDef.t) :
|
||||
@ -255,7 +256,10 @@ let process_subscope_decl
|
||||
(ctxt : context)
|
||||
(decl : Surface.Ast.scope_decl_context_scope) : context =
|
||||
let name, name_pos = decl.scope_decl_context_scope_name in
|
||||
let forward_output = decl.Surface.Ast.scope_decl_context_scope_attribute.scope_decl_context_io_output in
|
||||
let forward_output =
|
||||
decl.Surface.Ast.scope_decl_context_scope_attribute
|
||||
.scope_decl_context_io_output
|
||||
in
|
||||
let (path, subscope), s_pos = decl.scope_decl_context_scope_sub_scope in
|
||||
let scope_ctxt = get_scope_context ctxt scope in
|
||||
match Ident.Map.find_opt (Mark.remove subscope) scope_ctxt.var_idmap with
|
||||
@ -567,16 +571,18 @@ let process_scope_decl (ctxt : context) (decl : Surface.Ast.scope_decl) :
|
||||
data.scope_decl_context_item_typ;
|
||||
}
|
||||
:: acc
|
||||
| Surface.Ast.ContextScope {
|
||||
scope_decl_context_scope_name = var;
|
||||
scope_decl_context_scope_sub_scope = ((path, scope), pos);
|
||||
scope_decl_context_scope_attribute = { scope_decl_context_io_output = true, _; _ };
|
||||
} ->
|
||||
| Surface.Ast.ContextScope
|
||||
{
|
||||
scope_decl_context_scope_name = var;
|
||||
scope_decl_context_scope_sub_scope = (path, scope), pos;
|
||||
scope_decl_context_scope_attribute =
|
||||
{ scope_decl_context_io_output = true, _; _ };
|
||||
} ->
|
||||
Mark.add (Mark.get item)
|
||||
{
|
||||
Surface.Ast.struct_decl_field_name = var;
|
||||
Surface.Ast.struct_decl_field_typ =
|
||||
(Base (Data (Primitive (Named (path, scope))))), pos;
|
||||
Base (Data (Primitive (Named (path, scope)))), pos;
|
||||
}
|
||||
:: acc
|
||||
| _ -> acc)
|
||||
@ -765,9 +771,9 @@ let get_def_key
|
||||
| [x] ->
|
||||
let x_uid = get_var_uid scope_uid ctxt x in
|
||||
let var_sig = ScopeVar.Map.find x_uid ctxt.var_typs in
|
||||
(x_uid, pos),
|
||||
Ast.ScopeDef.Var
|
||||
( match state with
|
||||
( (x_uid, pos),
|
||||
Ast.ScopeDef.Var
|
||||
(match state with
|
||||
| Some state -> (
|
||||
try
|
||||
Some
|
||||
@ -790,22 +796,21 @@ let get_def_key
|
||||
"This definition does not indicate which state has to be \
|
||||
considered for variable %a."
|
||||
ScopeVar.format x_uid
|
||||
else None )
|
||||
else None) )
|
||||
| [y; x] ->
|
||||
let (subscope_var, name) : ScopeVar.t * ScopeName.t =
|
||||
match Ident.Map.find_opt (Mark.remove y) scope_ctxt.var_idmap with
|
||||
| Some (SubScope (v, u, _)) -> v, u
|
||||
| Some _ ->
|
||||
Message.raise_spanned_error pos
|
||||
"Invalid definition, %a is not a subscope"
|
||||
Print.lit_style (Mark.remove y)
|
||||
"Invalid definition, %a is not a subscope" Print.lit_style
|
||||
(Mark.remove y)
|
||||
| None ->
|
||||
Message.raise_spanned_error pos "No definition found for subscope %a"
|
||||
Print.lit_style (Mark.remove y)
|
||||
in
|
||||
let var_within_origin_scope = get_var_uid name ctxt x in
|
||||
(subscope_var, pos),
|
||||
Ast.ScopeDef.SubScope { name; var_within_origin_scope }
|
||||
(subscope_var, pos), Ast.ScopeDef.SubScope { name; var_within_origin_scope }
|
||||
| _ ->
|
||||
Message.raise_spanned_error pos
|
||||
"This line is defining a quantity that is neither a scope variable nor a \
|
||||
|
@ -132,8 +132,7 @@ val get_scope_context : context -> ScopeName.t -> scope_context
|
||||
val get_var_uid : ScopeName.t -> context -> Ident.t Mark.pos -> ScopeVar.t
|
||||
(** Get the variable uid inside the scope given in argument *)
|
||||
|
||||
val get_subscope_uid :
|
||||
ScopeName.t -> context -> Ident.t Mark.pos -> ScopeVar.t
|
||||
val get_subscope_uid : ScopeName.t -> context -> Ident.t Mark.pos -> ScopeVar.t
|
||||
(** Get the subscope uid inside the scope given in argument *)
|
||||
|
||||
val is_subscope_uid : ScopeName.t -> context -> Ident.t -> bool
|
||||
|
@ -339,7 +339,7 @@ module Commands = struct
|
||||
let get_variable_uid
|
||||
(ctxt : Desugared.Name_resolution.context)
|
||||
(scope_uid : ScopeName.t)
|
||||
(variable : string): Desugared.Ast.ScopeDef.t =
|
||||
(variable : string) : Desugared.Ast.ScopeDef.t =
|
||||
(* Sometimes the variable selected is of the form [a.b] *)
|
||||
let first_part, second_part =
|
||||
match String.index_opt variable '.' with
|
||||
@ -358,18 +358,19 @@ module Commands = struct
|
||||
variable ScopeName.format scope_uid
|
||||
| Some (ScopeVar v | SubScope (v, _, _)) ->
|
||||
let state =
|
||||
second_part |> Option.map @@ fun id ->
|
||||
let var_sig = ScopeVar.Map.find v ctxt.var_typs in
|
||||
match Ident.Map.find_opt id var_sig.var_sig_states_idmap with
|
||||
| Some state -> state
|
||||
| None ->
|
||||
Message.raise_error
|
||||
"State @{<yellow>\"%s\"@} is not found for variable \
|
||||
@{<yellow>\"%s\"@} of scope @{<yellow>\"%a\"@}"
|
||||
id first_part ScopeName.format scope_uid
|
||||
second_part
|
||||
|> Option.map
|
||||
@@ fun id ->
|
||||
let var_sig = ScopeVar.Map.find v ctxt.var_typs in
|
||||
match Ident.Map.find_opt id var_sig.var_sig_states_idmap with
|
||||
| Some state -> state
|
||||
| None ->
|
||||
Message.raise_error
|
||||
"State @{<yellow>\"%s\"@} is not found for variable \
|
||||
@{<yellow>\"%s\"@} of scope @{<yellow>\"%a\"@}"
|
||||
id first_part ScopeName.format scope_uid
|
||||
in
|
||||
( (v, Pos.no_pos),
|
||||
Desugared.Ast.ScopeDef.Var state )
|
||||
(v, Pos.no_pos), Desugared.Ast.ScopeDef.Var state
|
||||
|
||||
let get_output ?ext options output_file =
|
||||
let output_file = Option.map options.Global.path_rewrite output_file in
|
||||
|
@ -40,16 +40,16 @@ let rec locations_used (e : 'm expr) : LocationSet.t =
|
||||
|
||||
type 'm rule =
|
||||
| ScopeVarDefinition of {
|
||||
var: ScopeVar.t Mark.pos;
|
||||
typ: typ;
|
||||
io: Desugared.Ast.io;
|
||||
e: 'm expr
|
||||
var : ScopeVar.t Mark.pos;
|
||||
typ : typ;
|
||||
io : Desugared.Ast.io;
|
||||
e : 'm expr;
|
||||
}
|
||||
| SubScopeVarDefinition of {
|
||||
var: ScopeVar.t Mark.pos;
|
||||
var_within_origin_scope: ScopeVar.t;
|
||||
typ: typ;
|
||||
e: 'm expr
|
||||
var : ScopeVar.t Mark.pos;
|
||||
var_within_origin_scope : ScopeVar.t;
|
||||
typ : typ;
|
||||
e : 'm expr;
|
||||
}
|
||||
| Assertion of 'm expr
|
||||
|
||||
@ -78,7 +78,7 @@ type 'm program = {
|
||||
let type_rule decl_ctx env = function
|
||||
| ScopeVarDefinition ({ typ; e; _ } as def) ->
|
||||
let e = Typing.expr decl_ctx ~env ~typ e in
|
||||
ScopeVarDefinition {def with e = Expr.unbox e}
|
||||
ScopeVarDefinition { def with e = Expr.unbox e }
|
||||
| SubScopeVarDefinition ({ typ; e; _ } as def) ->
|
||||
let e = Typing.expr decl_ctx ~env ~typ e in
|
||||
SubScopeVarDefinition { def with e = Expr.unbox e }
|
||||
|
@ -33,19 +33,19 @@ val locations_used : 'm expr -> LocationSet.t
|
||||
|
||||
type 'm rule =
|
||||
| ScopeVarDefinition of {
|
||||
var: ScopeVar.t Mark.pos;
|
||||
typ: typ;
|
||||
io: Desugared.Ast.io;
|
||||
e: 'm expr
|
||||
var : ScopeVar.t Mark.pos;
|
||||
typ : typ;
|
||||
io : Desugared.Ast.io;
|
||||
e : 'm expr;
|
||||
}
|
||||
| SubScopeVarDefinition of {
|
||||
var: ScopeVar.t Mark.pos; (** Variable within the current scope *)
|
||||
var : ScopeVar.t Mark.pos; (** Variable within the current scope *)
|
||||
(* scope: ScopeVar.t Mark.pos; (\** Variable pointing to the *\) *)
|
||||
(* origin_var: ScopeVar.t Mark.pos;
|
||||
* reentrant: bool; *)
|
||||
var_within_origin_scope: ScopeVar.t;
|
||||
typ: typ; (* non-thunked at this point for reentrant vars *)
|
||||
e: 'm expr
|
||||
var_within_origin_scope : ScopeVar.t;
|
||||
typ : typ; (* non-thunked at this point for reentrant vars *)
|
||||
e : 'm expr;
|
||||
}
|
||||
| Assertion of 'm expr
|
||||
|
||||
|
@ -94,7 +94,9 @@ let rec expr_used_defs e =
|
||||
| e -> recurse_subterms e
|
||||
|
||||
let rule_used_defs = function
|
||||
| Ast.Assertion e | Ast.ScopeVarDefinition { e; _} | Ast.SubScopeVarDefinition { e; _ } ->
|
||||
| Ast.Assertion e
|
||||
| Ast.ScopeVarDefinition { e; _ }
|
||||
| Ast.SubScopeVarDefinition { e; _ } ->
|
||||
(* TODO: maybe this info could be passed on from previous passes without
|
||||
walking through all exprs again *)
|
||||
expr_used_defs e
|
||||
|
@ -195,80 +195,77 @@ let rule_to_exception_graph (scope : D.scope) = function
|
||||
(* Before calling the sub_scope, we need to include all the re-definitions
|
||||
of subscope parameters*)
|
||||
D.ScopeDef.Map.fold
|
||||
(fun (sscope, kind as def_key) scope_def exc_graphs ->
|
||||
match kind with
|
||||
| D.ScopeDef.Var _ -> exc_graphs
|
||||
| D.ScopeDef.SubScope _
|
||||
when
|
||||
not (ScopeVar.equal var (Mark.remove sscope))
|
||||
||
|
||||
Mark.remove scope_def.D.scope_def_io.io_input = NoInput
|
||||
&& RuleName.Map.is_empty scope_def.scope_def_rules
|
||||
->
|
||||
(* We exclude subscope variables that have 0 re-definitions and are
|
||||
not visible in the input of the subscope *)
|
||||
exc_graphs
|
||||
| D.ScopeDef.SubScope { var_within_origin_scope; _ } ->
|
||||
(* This definition redefines a variable of the correct subscope. But
|
||||
we have to check that this redefinition is allowed with respect
|
||||
to the io parameters of that subscope variable. *)
|
||||
let def = scope_def.D.scope_def_rules in
|
||||
let is_cond = scope_def.scope_def_is_condition in
|
||||
let () = match Mark.remove scope_def.D.scope_def_io.io_input with
|
||||
| NoInput ->
|
||||
Message.raise_multispanned_error
|
||||
(( Some "Incriminated subscope:",
|
||||
Mark.get (ScopeVar.get_info (Mark.remove sscope)) )
|
||||
:: ( Some "Incriminated variable:",
|
||||
Mark.get (ScopeVar.get_info var_within_origin_scope) )
|
||||
:: List.map
|
||||
(fun rule ->
|
||||
(fun ((sscope, kind) as def_key) scope_def exc_graphs ->
|
||||
match kind with
|
||||
| D.ScopeDef.Var _ -> exc_graphs
|
||||
| D.ScopeDef.SubScope _
|
||||
when (not (ScopeVar.equal var (Mark.remove sscope)))
|
||||
|| Mark.remove scope_def.D.scope_def_io.io_input = NoInput
|
||||
&& RuleName.Map.is_empty scope_def.scope_def_rules ->
|
||||
(* We exclude subscope variables that have 0 re-definitions and are
|
||||
not visible in the input of the subscope *)
|
||||
exc_graphs
|
||||
| D.ScopeDef.SubScope { var_within_origin_scope; _ } ->
|
||||
(* This definition redefines a variable of the correct subscope. But
|
||||
we have to check that this redefinition is allowed with respect to
|
||||
the io parameters of that subscope variable. *)
|
||||
let def = scope_def.D.scope_def_rules in
|
||||
let is_cond = scope_def.scope_def_is_condition in
|
||||
let () =
|
||||
match Mark.remove scope_def.D.scope_def_io.io_input with
|
||||
| NoInput ->
|
||||
Message.raise_multispanned_error
|
||||
(( Some "Incriminated subscope:",
|
||||
Mark.get (ScopeVar.get_info (Mark.remove sscope)) )
|
||||
:: ( Some "Incriminated variable:",
|
||||
Mark.get (ScopeVar.get_info var_within_origin_scope) )
|
||||
:: List.map
|
||||
(fun rule ->
|
||||
( Some "Incriminated subscope variable definition:",
|
||||
Mark.get (RuleName.get_info rule) ))
|
||||
(RuleName.Map.keys def))
|
||||
"Invalid assignment to a subscope variable that is \
|
||||
not tagged as input or context."
|
||||
| OnlyInput when RuleName.Map.is_empty def && not is_cond ->
|
||||
(* If the subscope variable is tagged as input, then it shall be
|
||||
defined. *)
|
||||
Message.raise_multispanned_error
|
||||
[
|
||||
( Some "Incriminated subscope:",
|
||||
Mark.get (ScopeVar.get_info (Mark.remove sscope)) );
|
||||
Some "Incriminated variable:", Mark.get sscope;
|
||||
]
|
||||
"This subscope variable is a mandatory input but no definition \
|
||||
was provided."
|
||||
| _ -> ()
|
||||
in
|
||||
let new_exc_graph = def_to_exception_graph def_key def in
|
||||
D.ScopeDef.Map.add def_key new_exc_graph exc_graphs)
|
||||
scope.scope_defs
|
||||
D.ScopeDef.Map.empty
|
||||
| Desugared.Dependency.Vertex.Var (var, state) ->
|
||||
(let pos = Mark.get (ScopeVar.get_info var) in
|
||||
let scope_def =
|
||||
D.ScopeDef.Map.find ((var, pos), D.ScopeDef.Var state) scope.scope_defs
|
||||
in
|
||||
let var_def = scope_def.D.scope_def_rules in
|
||||
match Mark.remove scope_def.D.scope_def_io.io_input with
|
||||
| OnlyInput when not (RuleName.Map.is_empty var_def) ->
|
||||
(* If the variable is tagged as input, then it shall not be redefined. *)
|
||||
Message.raise_multispanned_error
|
||||
((Some "Incriminated variable:", Mark.get (ScopeVar.get_info var))
|
||||
:: List.map
|
||||
(fun rule ->
|
||||
( Some "Incriminated variable definition:",
|
||||
Mark.get (RuleName.get_info rule) ))
|
||||
(RuleName.Map.keys var_def))
|
||||
"It is impossible to give a definition to a scope variable tagged as \
|
||||
input."
|
||||
| OnlyInput -> D.ScopeDef.Map.empty
|
||||
(* we do not provide any definition for an input-only variable *)
|
||||
| _ ->
|
||||
D.ScopeDef.Map.singleton
|
||||
((var, pos), (D.ScopeDef.Var state))
|
||||
(def_to_exception_graph ((var, pos), D.ScopeDef.Var state) var_def))
|
||||
(RuleName.Map.keys def))
|
||||
"Invalid assignment to a subscope variable that is not tagged \
|
||||
as input or context."
|
||||
| OnlyInput when RuleName.Map.is_empty def && not is_cond ->
|
||||
(* If the subscope variable is tagged as input, then it shall be
|
||||
defined. *)
|
||||
Message.raise_multispanned_error
|
||||
[
|
||||
( Some "Incriminated subscope:",
|
||||
Mark.get (ScopeVar.get_info (Mark.remove sscope)) );
|
||||
Some "Incriminated variable:", Mark.get sscope;
|
||||
]
|
||||
"This subscope variable is a mandatory input but no definition \
|
||||
was provided."
|
||||
| _ -> ()
|
||||
in
|
||||
let new_exc_graph = def_to_exception_graph def_key def in
|
||||
D.ScopeDef.Map.add def_key new_exc_graph exc_graphs)
|
||||
scope.scope_defs D.ScopeDef.Map.empty
|
||||
| Desugared.Dependency.Vertex.Var (var, state) -> (
|
||||
let pos = Mark.get (ScopeVar.get_info var) in
|
||||
let scope_def =
|
||||
D.ScopeDef.Map.find ((var, pos), D.ScopeDef.Var state) scope.scope_defs
|
||||
in
|
||||
let var_def = scope_def.D.scope_def_rules in
|
||||
match Mark.remove scope_def.D.scope_def_io.io_input with
|
||||
| OnlyInput when not (RuleName.Map.is_empty var_def) ->
|
||||
(* If the variable is tagged as input, then it shall not be redefined. *)
|
||||
Message.raise_multispanned_error
|
||||
((Some "Incriminated variable:", Mark.get (ScopeVar.get_info var))
|
||||
:: List.map
|
||||
(fun rule ->
|
||||
( Some "Incriminated variable definition:",
|
||||
Mark.get (RuleName.get_info rule) ))
|
||||
(RuleName.Map.keys var_def))
|
||||
"It is impossible to give a definition to a scope variable tagged as \
|
||||
input."
|
||||
| OnlyInput -> D.ScopeDef.Map.empty
|
||||
(* we do not provide any definition for an input-only variable *)
|
||||
| _ ->
|
||||
D.ScopeDef.Map.singleton
|
||||
((var, pos), D.ScopeDef.Var state)
|
||||
(def_to_exception_graph ((var, pos), D.ScopeDef.Var state) var_def))
|
||||
| Assertion _ -> D.ScopeDef.Map.empty (* no exceptions for assertions *)
|
||||
|
||||
let scope_to_exception_graphs (scope : D.scope) :
|
||||
@ -553,17 +550,18 @@ let translate_rule
|
||||
ctx
|
||||
(scope : D.scope)
|
||||
(exc_graphs :
|
||||
Desugared.Dependency.ExceptionsDependencies.t D.ScopeDef.Map.t)
|
||||
= function
|
||||
| Desugared.Dependency.Vertex.Var (var, state) ->
|
||||
Desugared.Dependency.ExceptionsDependencies.t D.ScopeDef.Map.t) = function
|
||||
| Desugared.Dependency.Vertex.Var (var, state) -> (
|
||||
let pos = Mark.get (ScopeVar.get_info var) in
|
||||
(* TODO: this may point to the place where the variable was declared instead of the binding in the definition being explored. Needs double-checking and maybe adding more position information *)
|
||||
(* TODO: this may point to the place where the variable was declared instead
|
||||
of the binding in the definition being explored. Needs double-checking
|
||||
and maybe adding more position information *)
|
||||
let scope_def =
|
||||
D.ScopeDef.Map.find ((var, pos), D.ScopeDef.Var state) scope.scope_defs
|
||||
in
|
||||
(match ScopeVar.Map.find_opt var scope.scope_sub_scopes with
|
||||
| None ->
|
||||
(let var_def = scope_def.D.scope_def_rules in
|
||||
match ScopeVar.Map.find_opt var scope.scope_sub_scopes with
|
||||
| None -> (
|
||||
let var_def = scope_def.D.scope_def_rules in
|
||||
let var_params = scope_def.D.scope_def_parameters in
|
||||
let var_typ = scope_def.D.scope_def_typ in
|
||||
let is_cond = scope_def.D.scope_def_is_condition in
|
||||
@ -587,86 +585,98 @@ let translate_rule
|
||||
| _ -> assert false
|
||||
in
|
||||
[
|
||||
Ast.ScopeVarDefinition {
|
||||
var = scope_var, pos;
|
||||
typ = var_typ;
|
||||
io = scope_def.D.scope_def_io;
|
||||
e = Expr.unbox expr_def;
|
||||
}
|
||||
Ast.ScopeVarDefinition
|
||||
{
|
||||
var = scope_var, pos;
|
||||
typ = var_typ;
|
||||
io = scope_def.D.scope_def_io;
|
||||
e = Expr.unbox expr_def;
|
||||
};
|
||||
])
|
||||
| Some subscope ->
|
||||
(* Before calling the subscope, we need to include all the re-definitions
|
||||
of subscope parameters *)
|
||||
let subscope_params =
|
||||
D.ScopeDef.Map.fold (fun def_key scope_def acc ->
|
||||
match def_key with
|
||||
| _, D.ScopeDef.Var _ -> acc
|
||||
| (v, _), D.ScopeDef.SubScope _
|
||||
when
|
||||
not (ScopeVar.equal var v)
|
||||
||
|
||||
Mark.remove scope_def.D.scope_def_io.io_input = NoInput
|
||||
&& RuleName.Map.is_empty scope_def.scope_def_rules
|
||||
-> acc
|
||||
| v, D.ScopeDef.SubScope { var_within_origin_scope; _ } ->
|
||||
let pos = Mark.get v in
|
||||
let def = scope_def.D.scope_def_rules in
|
||||
let def_typ = scope_def.scope_def_typ in
|
||||
let is_cond = scope_def.scope_def_is_condition in
|
||||
assert (* an error should have been already raised *)
|
||||
(match scope_def.D.scope_def_io.io_input with
|
||||
| NoInput, _ -> false
|
||||
| OnlyInput, _ -> is_cond || not (RuleName.Map.is_empty def)
|
||||
| _ -> true);
|
||||
let var_within_origin_scope =
|
||||
match ScopeVar.Map.find var_within_origin_scope ctx.scope_var_mapping with
|
||||
| WholeVar v -> v
|
||||
| States ((_, v) :: _) -> v
|
||||
| States [] -> assert false
|
||||
in
|
||||
let def_var =
|
||||
Var.make
|
||||
(String.concat "."
|
||||
[Mark.remove (ScopeVar.get_info (Mark.remove v));
|
||||
Mark.remove (ScopeVar.get_info var_within_origin_scope)])
|
||||
in
|
||||
let typ =
|
||||
Scope.input_type def_typ scope_def.D.scope_def_io.D.io_input
|
||||
in
|
||||
let expr_def =
|
||||
translate_def ctx def_key def scope_def.D.scope_def_parameters
|
||||
def_typ scope_def.D.scope_def_io
|
||||
(D.ScopeDef.Map.find def_key exc_graphs)
|
||||
~is_cond ~is_subscope_var:true
|
||||
in
|
||||
ScopeVar.Map.add var_within_origin_scope (def_var, pos, typ, expr_def) acc)
|
||||
scope.scope_defs ScopeVar.Map.empty
|
||||
in
|
||||
let subscope_param_map =
|
||||
ScopeVar.Map.map (fun (_, _, _, expr) -> expr)
|
||||
subscope_params
|
||||
in
|
||||
let subscope_call_expr =
|
||||
Expr.escopecall ~scope:subscope ~args:subscope_param_map (Untyped { pos })
|
||||
in
|
||||
let subscope_expr = subscope_call_expr in
|
||||
assert (RuleName.Map.is_empty scope_def.D.scope_def_rules);
|
||||
(* The subscope will be defined by its inputs, it's not supposed to have direct rules yet *)
|
||||
let scope_info = ScopeName.Map.find subscope ctx.decl_ctx.ctx_scopes in
|
||||
let subscope_var_dcalc =
|
||||
match ScopeVar.Map.find var ctx.scope_var_mapping with
|
||||
| WholeVar v -> v
|
||||
| _ -> assert false
|
||||
in
|
||||
let subscope_def =
|
||||
Ast.ScopeVarDefinition {
|
||||
var = subscope_var_dcalc, pos;
|
||||
typ = TStruct scope_info.out_struct_name, Mark.get (ScopeVar.get_info var);
|
||||
io = scope_def.D.scope_def_io;
|
||||
e = Expr.unbox_closed subscope_expr;
|
||||
}
|
||||
in
|
||||
[ subscope_def ])
|
||||
| Some subscope ->
|
||||
(* Before calling the subscope, we need to include all the re-definitions
|
||||
of subscope parameters *)
|
||||
let subscope_params =
|
||||
D.ScopeDef.Map.fold
|
||||
(fun def_key scope_def acc ->
|
||||
match def_key with
|
||||
| _, D.ScopeDef.Var _ -> acc
|
||||
| (v, _), D.ScopeDef.SubScope _
|
||||
when (not (ScopeVar.equal var v))
|
||||
|| Mark.remove scope_def.D.scope_def_io.io_input = NoInput
|
||||
&& RuleName.Map.is_empty scope_def.scope_def_rules ->
|
||||
acc
|
||||
| v, D.ScopeDef.SubScope { var_within_origin_scope; _ } ->
|
||||
let pos = Mark.get v in
|
||||
let def = scope_def.D.scope_def_rules in
|
||||
let def_typ = scope_def.scope_def_typ in
|
||||
let is_cond = scope_def.scope_def_is_condition in
|
||||
assert (
|
||||
(* an error should have been already raised *)
|
||||
match scope_def.D.scope_def_io.io_input with
|
||||
| NoInput, _ -> false
|
||||
| OnlyInput, _ -> is_cond || not (RuleName.Map.is_empty def)
|
||||
| _ -> true);
|
||||
let var_within_origin_scope =
|
||||
match
|
||||
ScopeVar.Map.find var_within_origin_scope
|
||||
ctx.scope_var_mapping
|
||||
with
|
||||
| WholeVar v -> v
|
||||
| States ((_, v) :: _) -> v
|
||||
| States [] -> assert false
|
||||
in
|
||||
let def_var =
|
||||
Var.make
|
||||
(String.concat "."
|
||||
[
|
||||
Mark.remove (ScopeVar.get_info (Mark.remove v));
|
||||
Mark.remove (ScopeVar.get_info var_within_origin_scope);
|
||||
])
|
||||
in
|
||||
let typ =
|
||||
Scope.input_type def_typ scope_def.D.scope_def_io.D.io_input
|
||||
in
|
||||
let expr_def =
|
||||
translate_def ctx def_key def scope_def.D.scope_def_parameters
|
||||
def_typ scope_def.D.scope_def_io
|
||||
(D.ScopeDef.Map.find def_key exc_graphs)
|
||||
~is_cond ~is_subscope_var:true
|
||||
in
|
||||
ScopeVar.Map.add var_within_origin_scope
|
||||
(def_var, pos, typ, expr_def)
|
||||
acc)
|
||||
scope.scope_defs ScopeVar.Map.empty
|
||||
in
|
||||
let subscope_param_map =
|
||||
ScopeVar.Map.map (fun (_, _, _, expr) -> expr) subscope_params
|
||||
in
|
||||
let subscope_call_expr =
|
||||
Expr.escopecall ~scope:subscope ~args:subscope_param_map
|
||||
(Untyped { pos })
|
||||
in
|
||||
let subscope_expr = subscope_call_expr in
|
||||
assert (RuleName.Map.is_empty scope_def.D.scope_def_rules);
|
||||
(* The subscope will be defined by its inputs, it's not supposed to have
|
||||
direct rules yet *)
|
||||
let scope_info = ScopeName.Map.find subscope ctx.decl_ctx.ctx_scopes in
|
||||
let subscope_var_dcalc =
|
||||
match ScopeVar.Map.find var ctx.scope_var_mapping with
|
||||
| WholeVar v -> v
|
||||
| _ -> assert false
|
||||
in
|
||||
let subscope_def =
|
||||
Ast.ScopeVarDefinition
|
||||
{
|
||||
var = subscope_var_dcalc, pos;
|
||||
typ =
|
||||
( TStruct scope_info.out_struct_name,
|
||||
Mark.get (ScopeVar.get_info var) );
|
||||
io = scope_def.D.scope_def_io;
|
||||
e = Expr.unbox_closed subscope_expr;
|
||||
}
|
||||
in
|
||||
[subscope_def])
|
||||
| Assertion a_name ->
|
||||
let assertion_expr =
|
||||
D.AssertionName.Map.find a_name scope.scope_assertions
|
||||
@ -688,13 +698,16 @@ let translate_scope_interface ctx scope =
|
||||
svar_io = scope_def.scope_def_io;
|
||||
}
|
||||
in
|
||||
let scope_sig = (* Add the definitions of standard scope vars *)
|
||||
let scope_sig =
|
||||
(* Add the definitions of standard scope vars *)
|
||||
ScopeVar.Map.fold
|
||||
(fun var (states : D.var_or_states) acc ->
|
||||
match states with
|
||||
| WholeVar ->
|
||||
let scope_def =
|
||||
D.ScopeDef.Map.find ((var, Pos.no_pos), D.ScopeDef.Var None) scope.D.scope_defs
|
||||
D.ScopeDef.Map.find
|
||||
((var, Pos.no_pos), D.ScopeDef.Var None)
|
||||
scope.D.scope_defs
|
||||
in
|
||||
ScopeVar.Map.add
|
||||
(match ScopeVar.Map.find var ctx.scope_var_mapping with
|
||||
@ -720,15 +733,20 @@ let translate_scope_interface ctx scope =
|
||||
acc states)
|
||||
scope.scope_vars ScopeVar.Map.empty
|
||||
in
|
||||
let scope_sig = (* Add the definition of vars corresponding to subscope calls, and their parameters (subscope vars) *)
|
||||
ScopeVar.Map.fold (fun var _scope_name acc ->
|
||||
let scope_sig =
|
||||
(* Add the definition of vars corresponding to subscope calls, and their
|
||||
parameters (subscope vars) *)
|
||||
ScopeVar.Map.fold
|
||||
(fun var _scope_name acc ->
|
||||
let scope_def =
|
||||
D.ScopeDef.Map.find ((var, Pos.no_pos), D.ScopeDef.Var None) scope.D.scope_defs
|
||||
D.ScopeDef.Map.find
|
||||
((var, Pos.no_pos), D.ScopeDef.Var None)
|
||||
scope.D.scope_defs
|
||||
in
|
||||
ScopeVar.Map.add
|
||||
(match ScopeVar.Map.find var ctx.scope_var_mapping with
|
||||
| WholeVar v -> v
|
||||
| States _ -> assert false)
|
||||
| WholeVar v -> v
|
||||
| States _ -> assert false)
|
||||
(get_svar scope_def) acc)
|
||||
scope.D.scope_sub_scopes scope_sig
|
||||
in
|
||||
@ -786,69 +804,71 @@ let translate_program
|
||||
let add_scope_mappings modul ctx =
|
||||
ScopeName.Map.fold
|
||||
(fun _ scdef ctx ->
|
||||
let ctx =
|
||||
(* Add normal scope vars to the env *)
|
||||
ScopeVar.Map.fold
|
||||
(fun scope_var (states : D.var_or_states) ctx ->
|
||||
let var_name, var_pos = ScopeVar.get_info scope_var in
|
||||
let new_var =
|
||||
match states with
|
||||
| D.WholeVar -> WholeVar (ScopeVar.fresh (var_name, var_pos))
|
||||
| States states ->
|
||||
let var_prefix = var_name ^ "_" in
|
||||
let state_var state =
|
||||
ScopeVar.fresh
|
||||
(Mark.map (( ^ ) var_prefix) (StateName.get_info state))
|
||||
in
|
||||
States (List.map (fun state -> state, state_var state) states)
|
||||
in
|
||||
let reentrant =
|
||||
let state =
|
||||
match states with
|
||||
| D.WholeVar -> None
|
||||
| States (s :: _) -> Some s
|
||||
| States [] -> assert false
|
||||
let ctx =
|
||||
(* Add normal scope vars to the env *)
|
||||
ScopeVar.Map.fold
|
||||
(fun scope_var (states : D.var_or_states) ctx ->
|
||||
let var_name, var_pos = ScopeVar.get_info scope_var in
|
||||
let new_var =
|
||||
match states with
|
||||
| D.WholeVar -> WholeVar (ScopeVar.fresh (var_name, var_pos))
|
||||
| States states ->
|
||||
let var_prefix = var_name ^ "_" in
|
||||
let state_var state =
|
||||
ScopeVar.fresh
|
||||
(Mark.map (( ^ ) var_prefix) (StateName.get_info state))
|
||||
in
|
||||
match
|
||||
D.ScopeDef.Map.find_opt
|
||||
((scope_var, Pos.no_pos), Var state)
|
||||
scdef.D.scope_defs
|
||||
with
|
||||
| Some
|
||||
{
|
||||
scope_def_io = { io_input = Runtime.Reentrant, _; _ };
|
||||
scope_def_typ;
|
||||
_;
|
||||
} ->
|
||||
Some scope_def_typ
|
||||
| _ -> None
|
||||
States
|
||||
(List.map (fun state -> state, state_var state) states)
|
||||
in
|
||||
let reentrant =
|
||||
let state =
|
||||
match states with
|
||||
| D.WholeVar -> None
|
||||
| States (s :: _) -> Some s
|
||||
| States [] -> assert false
|
||||
in
|
||||
{
|
||||
ctx with
|
||||
scope_var_mapping =
|
||||
ScopeVar.Map.add scope_var new_var ctx.scope_var_mapping;
|
||||
reentrant_vars =
|
||||
Option.fold reentrant
|
||||
~some:(fun ty ->
|
||||
ScopeVar.Map.add scope_var ty ctx.reentrant_vars)
|
||||
~none:ctx.reentrant_vars;
|
||||
})
|
||||
scdef.D.scope_vars ctx
|
||||
in
|
||||
let ctx =
|
||||
(* Add scope vars pointing to subscope executions to the env
|
||||
(their definitions are introduced during the processing of the rules above) *)
|
||||
ScopeVar.Map.fold (fun var _ ctx ->
|
||||
let var_name, var_pos = ScopeVar.get_info var in
|
||||
let scope_var_mapping =
|
||||
let new_var = WholeVar (ScopeVar.fresh (var_name, var_pos)) in
|
||||
ScopeVar.Map.add var new_var ctx.scope_var_mapping
|
||||
in
|
||||
{ ctx with scope_var_mapping }
|
||||
)
|
||||
scdef.D.scope_sub_scopes ctx
|
||||
in
|
||||
ctx)
|
||||
match
|
||||
D.ScopeDef.Map.find_opt
|
||||
((scope_var, Pos.no_pos), Var state)
|
||||
scdef.D.scope_defs
|
||||
with
|
||||
| Some
|
||||
{
|
||||
scope_def_io = { io_input = Runtime.Reentrant, _; _ };
|
||||
scope_def_typ;
|
||||
_;
|
||||
} ->
|
||||
Some scope_def_typ
|
||||
| _ -> None
|
||||
in
|
||||
{
|
||||
ctx with
|
||||
scope_var_mapping =
|
||||
ScopeVar.Map.add scope_var new_var ctx.scope_var_mapping;
|
||||
reentrant_vars =
|
||||
Option.fold reentrant
|
||||
~some:(fun ty ->
|
||||
ScopeVar.Map.add scope_var ty ctx.reentrant_vars)
|
||||
~none:ctx.reentrant_vars;
|
||||
})
|
||||
scdef.D.scope_vars ctx
|
||||
in
|
||||
let ctx =
|
||||
(* Add scope vars pointing to subscope executions to the env (their
|
||||
definitions are introduced during the processing of the rules
|
||||
above) *)
|
||||
ScopeVar.Map.fold
|
||||
(fun var _ ctx ->
|
||||
let var_name, var_pos = ScopeVar.get_info var in
|
||||
let scope_var_mapping =
|
||||
let new_var = WholeVar (ScopeVar.fresh (var_name, var_pos)) in
|
||||
ScopeVar.Map.add var new_var ctx.scope_var_mapping
|
||||
in
|
||||
{ ctx with scope_var_mapping })
|
||||
scdef.D.scope_sub_scopes ctx
|
||||
in
|
||||
ctx)
|
||||
modul.D.module_scopes ctx
|
||||
in
|
||||
(* Todo: since we rename all scope vars at this point, it would be better to
|
||||
|
@ -72,26 +72,21 @@ let scope ?debug ctx fmt (name, (decl, _pos)) =
|
||||
~pp_sep:(fun fmt () -> Format.fprintf fmt "%a@ " Print.punctuation ";")
|
||||
(fun fmt rule ->
|
||||
match rule with
|
||||
| ScopeVarDefinition { var; typ; io; e; } ->
|
||||
Format.fprintf fmt "@[<hov 2>%a %a %a %a %a@ %t%a@]"
|
||||
Print.keyword "let"
|
||||
ScopeVar.format (Mark.remove var)
|
||||
Print.punctuation ":"
|
||||
| ScopeVarDefinition { var; typ; io; e } ->
|
||||
Format.fprintf fmt "@[<hov 2>%a %a %a %a %a@ %t%a@]" Print.keyword
|
||||
"let" ScopeVar.format (Mark.remove var) Print.punctuation ":"
|
||||
(Print.typ ctx) typ Print.punctuation "="
|
||||
(fun fmt -> match Mark.remove io.io_input with
|
||||
| Reentrant ->
|
||||
Print.op_style fmt "reentrant or by default";
|
||||
Format.pp_print_space fmt ()
|
||||
| _ -> ())
|
||||
(fun fmt ->
|
||||
match Mark.remove io.io_input with
|
||||
| Reentrant ->
|
||||
Print.op_style fmt "reentrant or by default";
|
||||
Format.pp_print_space fmt ()
|
||||
| _ -> ())
|
||||
(Print.expr ?debug ()) e
|
||||
| SubScopeVarDefinition { var; typ; e; _ } ->
|
||||
Format.fprintf fmt "@[<hov 2>%a %a %a %a %a@ %a@]"
|
||||
Print.keyword "let"
|
||||
ScopeVar.format (Mark.remove var)
|
||||
Print.punctuation ":"
|
||||
(Print.typ ctx) typ
|
||||
Print.punctuation "="
|
||||
(Print.expr ?debug ()) e
|
||||
Format.fprintf fmt "@[<hov 2>%a %a %a %a %a@ %a@]" Print.keyword
|
||||
"let" ScopeVar.format (Mark.remove var) Print.punctuation ":"
|
||||
(Print.typ ctx) typ Print.punctuation "=" (Print.expr ?debug ()) e
|
||||
| Assertion e ->
|
||||
Format.fprintf fmt "%a %a" Print.keyword "assert"
|
||||
(Print.expr ?debug ()) e))
|
||||
|
@ -98,7 +98,7 @@ module ScopeVar =
|
||||
type scope_var_or_subscope =
|
||||
| ScopeVar of ScopeVar.t
|
||||
| SubScope of ScopeVar.t * ScopeName.t * bool Mark.pos
|
||||
(* The bool is true if the output of the subscope is to be forwarded *)
|
||||
(* The bool is true if the output of the subscope is to be forwarded *)
|
||||
|
||||
module StateName =
|
||||
Uid.Gen
|
||||
|
@ -538,10 +538,10 @@ let compare_location
|
||||
(y : a glocation Mark.pos) =
|
||||
match Mark.remove x, Mark.remove y with
|
||||
| ( DesugaredScopeVar { name = vx; state = sx },
|
||||
DesugaredScopeVar { name = vy; state = sy } ) ->
|
||||
(match Mark.compare ScopeVar.compare vx vy with
|
||||
| 0 -> Option.compare StateName.compare sx sy
|
||||
| n -> n)
|
||||
DesugaredScopeVar { name = vy; state = sy } ) -> (
|
||||
match Mark.compare ScopeVar.compare vx vy with
|
||||
| 0 -> Option.compare StateName.compare sx sy
|
||||
| n -> n)
|
||||
| ScopelangScopeVar { name = vx, _ }, ScopelangScopeVar { name = vy, _ } ->
|
||||
ScopeVar.compare vx vy
|
||||
| ToplevelVar { name = vx, _ }, ToplevelVar { name = vy, _ } ->
|
||||
|
@ -405,7 +405,6 @@ module Env = struct
|
||||
let get t v = Var.Map.find_opt v t.vars
|
||||
let get_scope_var t sv = A.ScopeVar.Map.find_opt sv t.scope_vars
|
||||
let get_toplevel_var t v = A.TopdefName.Map.find_opt v t.toplevel_vars
|
||||
|
||||
let add v tau t = { t with vars = Var.Map.add v tau t.vars }
|
||||
let add_var v typ t = add v (ast_to_typ typ) t
|
||||
|
||||
@ -558,9 +557,7 @@ and typecheck_expr_top_down :
|
||||
| Some name -> unionfind (TStruct name)
|
||||
| None -> unionfind (TAny (Any.fresh ()))
|
||||
in
|
||||
let e_struct' =
|
||||
typecheck_expr_top_down ctx env t_struct e_struct
|
||||
in
|
||||
let e_struct' = typecheck_expr_top_down ctx env t_struct e_struct in
|
||||
let name =
|
||||
match UnionFind.get (ty e_struct') with
|
||||
| TStruct name, _ -> name
|
||||
@ -569,8 +566,8 @@ and typecheck_expr_top_down :
|
||||
"Disambiguation failed before reaching field %s" field
|
||||
| _ ->
|
||||
Message.raise_spanned_error (Expr.pos e)
|
||||
"This is not a structure, cannot access field %s (found type: %a)" field
|
||||
(format_typ ctx) (ty e_struct')
|
||||
"This is not a structure, cannot access field %s (found type: %a)"
|
||||
field (format_typ ctx) (ty e_struct')
|
||||
in
|
||||
let str =
|
||||
try A.StructName.Map.find name env.structs
|
||||
@ -581,30 +578,43 @@ and typecheck_expr_top_down :
|
||||
let field =
|
||||
let candidate_structs =
|
||||
try A.Ident.Map.find field ctx.ctx_struct_fields
|
||||
with A.Ident.Map.Not_found _ ->
|
||||
with A.Ident.Map.Not_found _ -> (
|
||||
match
|
||||
A.ScopeName.Map.choose_opt @@
|
||||
A.ScopeName.Map.filter
|
||||
(fun _ { A.out_struct_name; _ } -> A.StructName.equal out_struct_name name)
|
||||
ctx.ctx_scopes
|
||||
A.ScopeName.Map.choose_opt
|
||||
@@ A.ScopeName.Map.filter
|
||||
(fun _ { A.out_struct_name; _ } ->
|
||||
A.StructName.equal out_struct_name name)
|
||||
ctx.ctx_scopes
|
||||
with
|
||||
| Some (scope_out, _) ->
|
||||
Message.raise_multispanned_error_full
|
||||
[Some (fun ppf -> Format.fprintf ppf "@{<yellow>%s@} is used here as an output" field),
|
||||
Expr.mark_pos context_mark;
|
||||
Some (fun ppf -> Format.fprintf ppf "Scope %a is declared here" A.ScopeName.format scope_out),
|
||||
Mark.get (A.StructName.get_info name)]
|
||||
[
|
||||
( Some
|
||||
(fun ppf ->
|
||||
Format.fprintf ppf
|
||||
"@{<yellow>%s@} is used here as an output" field),
|
||||
Expr.mark_pos context_mark );
|
||||
( Some
|
||||
(fun ppf ->
|
||||
Format.fprintf ppf "Scope %a is declared here"
|
||||
A.ScopeName.format scope_out),
|
||||
Mark.get (A.StructName.get_info name) );
|
||||
]
|
||||
"Variable @{<yellow>%s@} is not a declared output of scope %a."
|
||||
field A.ScopeName.format scope_out
|
||||
~suggestion:(List.map A.StructField.to_string (A.StructField.Map.keys str))
|
||||
~suggestion:
|
||||
(List.map A.StructField.to_string (A.StructField.Map.keys str))
|
||||
| None ->
|
||||
Message.raise_multispanned_error
|
||||
[None, Expr.mark_pos context_mark;
|
||||
Some "Structure definition", Mark.get (A.StructName.get_info name)]
|
||||
[
|
||||
None, Expr.mark_pos context_mark;
|
||||
( Some "Structure definition",
|
||||
Mark.get (A.StructName.get_info name) );
|
||||
]
|
||||
"Field @{<yellow>\"%s\"@} does not belong to structure \
|
||||
@{<yellow>\"%a\"@}."
|
||||
field A.StructName.format name
|
||||
~suggestion:(A.Ident.Map.keys ctx.ctx_struct_fields)
|
||||
~suggestion:(A.Ident.Map.keys ctx.ctx_struct_fields))
|
||||
in
|
||||
try A.StructName.Map.find name candidate_structs
|
||||
with A.StructName.Map.Not_found _ ->
|
||||
|
Loading…
Reference in New Issue
Block a user