https://github.com/xi-business/infsat
Tip revision: 31552cff3d6d4239fcf05c9c201e9c2fa3678b7a authored by Jan Wroblewski on 10 February 2022, 12:43:54 UTC
Removed unusable benchmark and renamed the other g45 one.
Removed unusable benchmark and renamed the other g45 one.
Tip revision: 31552cf
environment.ml
open Binding
open GrammarCommon
open HGrammar
open TypingCommon
open Type
open Utilities
(** Map from used nonterminal typings to whether they were used at least twice in the proof
tree. *)
type used_nts = bool NTTyMap.t
let empty_used_nts : used_nts = NTTyMap.empty
let nt_ty_used_once (nt : nt_id) (ty : ty) : used_nts =
NTTyMap.singleton (nt, ty) false
(** Map from used terminal typings to where they were used in proof's hterm. *)
type loc_types = int TyMap.t HlocMap.t
let empty_loc_types : loc_types = HlocMap.empty
let loc_with_single_type (loc : hloc) (ty : ty) : loc_types =
HlocMap.singleton loc @@ TyMap.singleton ty 1
(** Immutable typing environment for a term. Contains info on types of variables and various
metadata gathered from the derivation tree for that term. *)
type env = {
(** Mapping from variables to their intersection types. Logically, everything is connected with
AND. *)
vars : ity IntMap.t;
(** Information if duplication occured when computing this environment on the top of the
derivation tree. *)
dup : bool;
(** Information if productive actual argument was used on the top of the derivation tree. *)
pr_arg : bool;
(** Nonterminals used when computing this environment in the whole derivation tree.
This is redundant due to loc_types, but allows for quick search of relevant
for duplication graph info. loc_types is only used for pretty-printing proofs. *)
used_nts : used_nts;
(** Typings of terminals and nonterminals used in the derivation in different locations. *)
loc_types : loc_types;
(** Information if duplication or terminal a occured in the whole derivation tree. *)
positive : bool
}
(* --- construction --- *)
let mk_env (used_nts : used_nts) (loc_types : loc_types) (positive : bool)
(vars : ity IntMap.t) : env =
{
vars = vars;
dup = false;
pr_arg = false;
used_nts = used_nts;
loc_types = loc_types;
positive = positive
}
(** Make empty environment with given metadata, but with no duplications. *)
let mk_empty_env (used_nts : used_nts) (loc_types : loc_types) (positive : bool) : env =
mk_env used_nts loc_types positive IntMap.empty
(** Creates an environment with empty metadata. Careful with making sure that location types are
eventually added. *)
let mk_env_empty_meta (vars : ity IntMap.t) =
mk_env empty_used_nts empty_loc_types false vars
let singleton_env (used_nts : used_nts) (loc_types : loc_types) (positive : bool)
(_, i : var_id) (ity : ity) : env =
mk_env used_nts loc_types positive @@ IntMap.singleton i ity
(* --- access --- *)
let env2fun (arity : int) (env : env) (codomain : ty) : ty =
cons_fun (List.map (fun v ->
option_default ity_top @@ IntMap.find_opt v env.vars
) @@ range 0 arity) codomain
let env_has_pr_vars (env : env) : bool =
IntMap.exists (fun _ ity -> TyList.exists is_productive ity) env.vars
(* --- transformation --- *)
let with_dup (dup : bool) (env : env) : env =
{ env with dup = dup }
let with_positive (positive : bool) (env : env) : env =
{ env with positive = positive }
let with_used_nts (used_nts : used_nts) (env : env) : env =
{ env with used_nts = used_nts }
let with_single_loc_ty (loc : hloc) (ty : ty) (env : env) : env =
{ env with loc_types = loc_with_single_type loc ty }
(** Merging vars is intersection of itys of the same var (i.e., summation of restrictions, so
it is implemented as sum of sets). The result is a new, merged environment and information
whether duplication of a productive variable occured. *)
let intersect_vars (vars1 : ity IntMap.t) (vars2 : ity IntMap.t) : ity IntMap.t * bool =
let dup = ref false in
let vars = IntMap.union (fun _ ity1 ity2 ->
Some (TyList.merge_custom (fun ty _ ->
if is_productive ty then
dup := true;
ty) ity1 ity2)
) vars1 vars2
in
vars, !dup
(** Merges two environments together, setting the duplication and positive flag if needed. *)
let intersect_envs (env1 : env) (env2 : env) =
let vars, merged_dup = intersect_vars env1.vars env2.vars in
{
vars = vars;
dup = env1.dup || env2.dup || merged_dup;
pr_arg = env1.pr_arg || env2.pr_arg;
used_nts =
NTTyMap.union (fun _ _ _ -> Some true)
env1.used_nts env2.used_nts;
loc_types =
HlocMap.union (fun _ ty_counts1 ty_counts2 ->
Some (TyMap.union (fun _ count1 count2 ->
Some (count1 + count2)
) ty_counts1 ty_counts2)
) env1.loc_types env2.loc_types;
positive = env1.positive || env2.positive || merged_dup
}
(* --- comparison --- *)
(** Compares two environments with the same amount of variables. Ignores loc_types, which means
that locations and terminals are ignored and all used nonterminals in counts above 2 are
treated as if the count was 2. *)
let env_compare (env1 : env) (env2 : env) : int =
compare_pair
compare
(compare_pair (IntMap.compare TyList.compare) @@
NTTyMap.compare compare)
((env1.dup, env1.pr_arg, env1.positive), (env1.vars, env1.used_nts))
((env2.dup, env2.pr_arg, env2.positive), (env2.vars, env2.used_nts))
let env_eq (env1 : env) (env2 : env) =
env_compare env1 env2 = 0
(* --- printing --- *)
let string_of_env (env : env) : string =
let vars_str =
if IntMap.is_empty env.vars then
"()"
else
String.concat ", " @@ List.of_seq @@
Seq.map (fun (i, ity) -> string_of_int i ^ " : " ^ string_of_ity ity) @@
IntMap.to_seq env.vars
in
let dup_info = if env.dup then " DUP" else "" in
let pr_arg_info = if env.pr_arg then " PR_ARG" else "" in
let nts_info =
if NTTyMap.is_empty env.used_nts then
""
else
" NTS " ^ (NTTyMap.bindings env.used_nts |>
Utilities.string_of_list (fun (nt_ty, multi) ->
let multi_str =
if multi then
"+"
else
""
in
string_of_nt_ty nt_ty ^ multi_str
)
)
in
let loc_types_str =
" LOC " ^ (HlocMap.bindings env.loc_types |>
Utilities.string_of_list (fun (loc, ty_counts) ->
string_of_int loc ^ ": " ^
Utilities.string_of_list (fun (ty, count) ->
string_of_ty ty ^ " x" ^ string_of_int count
) (TyMap.bindings ty_counts)
)
)
in
let positive_info = if env.positive then " POS" else "" in
vars_str ^ dup_info ^ pr_arg_info ^ nts_info ^ loc_types_str ^ positive_info