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
typing.ml
open Binding
open Context
open Environment
open GrammarCommon
open HGrammar
open HtyStore
open TargetEnvs
open Type
open TypingCommon
open Utilities
class typing (hg : hgrammar) = object(self)
(* --- registers --- *)
(** nt_ity[nt] has all typings of nonterminal nt. *)
val nt_ity : TySet.t array = Array.make hg#nt_count TySet.empty
(** htys[id] contains list of types derived under some environment for
corresponding terms in the list of terms identified by id. *)
val hty_store : hty_store = new hty_store hg
(* --- getting registered typings --- *)
method nt_ity (nt : nt_id) : TySet.t = nt_ity.(nt)
(* --- saving new typings --- *)
(** Adds nonterminal typing and returns whether it is a new one. *)
method add_nt_ty (nt : nt_id) (ty : ty) : bool =
if TySet.mem ty nt_ity.(nt) then
false
else
begin
nt_ity.(nt) <- TySet.add ty nt_ity.(nt);
true
end
method add_hterms_hty (id : hterms_id) (hty : hty) : bool =
hty_store#add_hty id hty
(* --- constructing contexts --- *)
(** Constructs product environment for hterms in the binding and a map from variable positions
(i.e., without nonterminal) to index of hterm in the product environment (ih). *)
method binding2ctx (hterm : hterm) (mask : vars option)
(fixed_hterms_hty : (hterms_id * hty) option)
(fixed_nt_ty : (nt_id * TySet.t) option)
(binding : hterms_id binding) : ctx =
let var_bix = var_bix binding in
let bix_data = IntMap.of_list @@ index_list binding in
let apply_mask =
match mask with
| None -> fun _ hty -> hty
| Some mask ->
let maskSet = IntSet.of_list @@ List.map snd @@ SortedVars.to_list mask in
fun i hty ->
Array.mapi (fun ix tys ->
if IntSet.mem (ix + i) maskSet then
tys
else
tys_top
) hty
in
let bix_htys =
IntMap.map (fun (i, _, id) ->
HtySet.map (apply_mask i) @@
hty_store#get_htys id
) bix_data
in
(* assuming that forced hty is present in bix_hty *)
let forced_hterms_hty =
match fixed_hterms_hty with
| Some (fid, fhty) ->
let fbix_htys =
BixMap.of_seq @@
Seq.filter_map (fun (bix, (i, _, id)) ->
if id = fid then
Some (bix, apply_mask i fhty)
else
None
) @@
BixMap.to_seq bix_data
in
assert (BixMap.for_all (fun bix hty ->
HtySet.mem hty @@ BixMap.find bix bix_htys
) fbix_htys);
Some fbix_htys
| None -> None
in
(* assuming that forced ty is in nt_ity *)
let forced_nt_ty =
match fixed_nt_ty with
| Some (nt, tys) ->
let locs =
List.map fst @@
List.filter (fun (l, (h, i)) -> h = HNT nt) @@
HlocMap.bindings @@
hg#loc2head_occurence hterm
in
assert (TySet.subset tys nt_ity.(nt));
Some (locs, tys)
| None -> None
in
mk_ctx var_bix bix_htys forced_hterms_hty forced_nt_ty
(* --- typing --- *)
method terminal_ity : terminal -> ity =
let a_ity = TyList.of_list [
mk_fun [ity_np] true;
mk_fun [ity_pr] true
]
in
let b_ity = TyList.of_list [
mk_fun [ity_np; ity_top] false;
mk_fun [ity_pr; ity_top] false;
mk_fun [ity_top; ity_np] false;
mk_fun [ity_top; ity_pr] false
]
in
let e_ity = ity_np in
let t_ity = TyList.of_list [
mk_fun [ity_np; ity_np] false;
mk_fun [ity_pr; ity_np] false;
mk_fun [ity_np; ity_pr] false;
mk_fun [ity_pr; ity_pr] false
]
in
function
| A -> a_ity
| B -> b_ity
| E -> e_ity
| T -> t_ity
(** Infer variable environments under which type checking of hterm : target succeeds. If target
is not specified, environments are inferred for all possible targets. Returns the result
in form of target -> possible environments map.
The typing is done in a prefix order on the term tree. Types of terminals are constant,
and types of nonterminals and variables are taken from the environment's context.
The environment's context takes care of enforcing a usage of a specific typing of a
nonterminal or a hterm. It is also used to keep possible variable typings as a product
of variable typings as long as possible, since in many cases these typings will be invalid.
Flag no_pr_vars prevents usage of productive variables. Flag force_pr_var ensures that
there is at least one productive variable. Only one of these flags may be true.
This method delegates the typing to type_check_hterm and later filters out results whose
contexts did not satisfy restrictions that given typing of a nonterminal or hterms must
be used at least once. It is necessary to do it here after traversing the whole term tree,
because a nonterminal or hterms may simply never be typed if one of nodes above has
type T. *)
method type_check (hterm : hterm) (target : ty option) (ctx : ctx)
(no_pr_vars : bool) (force_pr_var : bool) : te =
let te = self#type_check_hterm hterm target ctx 0 no_pr_vars force_pr_var in
print_verbose !Flags.verbose_proofs @@ lazy (
"TE size before filtering out contexts that do not satisfy restrictions: " ^
(string_of_int @@ TargetEnvs.size te) ^ "."
);
let res = te |> TargetEnvs.filter_satisfied_ctx in
print_verbose !Flags.verbose_proofs @@ lazy (
"TE size after filtering out contexts that do not satisfy restrictions: " ^
(string_of_int @@ TargetEnvs.size res) ^ "."
);
res
(** This method types leafs, i.e., terminals, nonterminals, and variables. Taking care of
application is delegated to another method. *)
method type_check_hterm (hterm : hterm) (target : ty option) (ctx : ctx) (loc : hloc)
(no_pr_vars : bool) (force_pr_var : bool) : te =
assert (not (no_pr_vars && force_pr_var));
print_verbose !Flags.verbose_proofs @@ lazy (
let vars_info = match no_pr_vars, force_pr_var with
| true, false -> " (no pr vars)"
| false, true -> " (force pr var)"
| _ -> ""
in
let target_info =
match target with
| Some target -> " : " ^ string_of_ty target;
| None -> ""
in
let ctx_info =
string_of_ctx ctx
in
"Inferring environment for " ^ hg#string_of_hterm true HlocMap.empty 0 hterm ^
target_info ^ vars_info ^ " under context " ^ ctx_info
);
let res = match hterm with
| HT a, [] ->
if not force_pr_var then
let ity = self#terminal_ity a in
let filtered =
match target with
| Some target ->
ity |> TyList.filter (Ty.equal target)
| None -> ity
in
TargetEnvs.of_list @@
TyList.map (fun ty -> (ty, [
(mk_empty_env empty_used_nts (loc_with_single_type loc ty) (is_productive ty),
ctx)
])) @@
filtered
else
TargetEnvs.empty
| HNT nt, [] ->
if not force_pr_var then
let compatible_ctx =
match target with
| Some target ->
list_of_option @@ ctx_enforce_nt ctx nt_ity nt loc target
| None ->
ctx_split_nt ctx nt_ity nt loc
in
TargetEnvs.of_list @@
List.map (fun (ty, ctx) -> (ty, [
(mk_empty_env (nt_ty_used_once nt ty) (loc_with_single_type loc ty) false,
ctx)
])) @@
compatible_ctx
else
TargetEnvs.empty
| HVar v, [] ->
begin
match target with
| Some target ->
if is_productive target then
(* variables are only NP *)
TargetEnvs.empty
else
begin
let compatible_ctx : (ty * ctx) list =
if no_pr_vars then
list_of_option @@ ctx_enforce_var ctx v target
else if force_pr_var then
let pr_target = with_productivity true target in
list_of_option @@ ctx_enforce_var ctx v pr_target
else
(* both NP and PR versions are possible *)
let pr_target = with_productivity true target in
list_of_option (ctx_enforce_var ctx v target) @
list_of_option (ctx_enforce_var ctx v pr_target)
in
(* selecting a typing for a variable fixes hty to occurence of hterms, so
for each variable type a context where that variable has that type is used
effectively splitting the context into one piece per used variable type *)
TargetEnvs.of_list @@
List.map (fun (ty, ctx) ->
let env =
singleton_env empty_used_nts (loc_with_single_type loc ty) false v @@ sty ty
in
(target, [(env, ctx)])
) @@
compatible_ctx
end
| None ->
(* If we're in this branch with None target then this must be a head variable,
since other variables will always have a target inferred from the head.
If the context is defined, we take the variables from it. If not, we deem this
term untypable in current conditions. This is not a problem, because to construct
the proof tree for application of this nonterminal, we'll have to get the proof
tree for arguments first. *)
TargetEnvs.of_list @@
List.map (fun (ty, ctx) ->
let env =
singleton_env empty_used_nts (loc_with_single_type loc ty) false v @@ sty ty
in
(with_productivity false ty, [(env, ctx)])
) @@
ctx_split_var ctx v
end
| _ -> (* application *)
let h, args = hg#decompose_hterm hterm in
self#type_check_app h args target ctx loc no_pr_vars force_pr_var
in
assert (target = None || TargetEnvs.targets_count res <= 1);
print_verbose !Flags.verbose_proofs @@ lazy (
let target_info =
match target with
| Some target -> " : " ^ string_of_ty target
| None -> ""
in
let check_info =
if TargetEnvs.is_empty res then
" does not type check"
else
" type checks with the following targets and environments: " ^
TargetEnvs.to_string res
in
hg#string_of_hterm true HlocMap.empty 0 hterm ^ target_info ^ check_info
);
res
(** This method is used to type check an application of head h to arguments args. *)
method type_check_app (h : head) (args : hterm list) (target : ty option) (ctx : ctx)
(loc : hloc) (no_pr_vars : bool) (force_pr_var : bool) : te =
(* Definitions:
* target is the type used in type checking hterm h : target and is either restricted to
type in argument or all possible targets are computed
* target argument's productivity is the productivity of an argument in target type
* actual argument's productivity is computed productivity of the type of an argument and
it does not have to be the same as productivity of the target argument
* head's type is the type of h, where h is a variable, terminal, or nonterminal *)
let h_arity = List.length args in
(* Get all head typings using type_check. Head typings are targets of this TE. Note that
types of variables may have different productivity from the variable itself. *)
let all_h_te = self#type_check_hterm (h, []) None ctx loc no_pr_vars false in
print_verbose !Flags.verbose_proofs @@ lazy (
"head_ity: " ^
string_of_ity (TyList.of_list @@ TargetEnvs.targets all_h_te)
);
(* Filtering compatible head types so that the type after application will be equal to
target type. *)
let h_data =
target |>
option_map_or_default all_h_te @@
self#filter_compatible_heads all_h_te h_arity
in
print_verbose !Flags.verbose_proofs @@ lazy (
"compatible head_ity: " ^
string_of_ity (TyList.of_list @@ TargetEnvs.targets h_data)
);
(* Iteration over each compatible with the target typing of the head. annotate_args
takes care of grouping target types of arguments with their respective terms in args.
h_target is the type of the head without arguments present in this application (the
effective productivity may still be different due to, e.g., duplications). *)
List.fold_left TargetEnvs.union TargetEnvs.empty @@
(self#annotate_args args (loc + 1) h_data |>
List.map (fun (args, h_target, env, ctx) ->
(* Computing target for current typing of head and categorizing it by productivity. *)
let head_pr = is_productive h_target in
let pr_target, np_target = match target with
| Some target ->
(* When target is given, it is used. *)
if is_productive target then
(Some target, None)
else
(None, Some target)
| None ->
(* When target is not given, it is inferred from head's type. There is one
possibility if head is productive and two if not. *)
if head_pr then
(Some h_target, None)
else
(Some (with_productivity true h_target), Some h_target)
in
(* Construction of a TE with starting variables for each target. *)
let pr_start_te =
pr_target |> option_map_or_default TargetEnvs.empty (fun target ->
TargetEnvs.of_list [(target, [(env, ctx)])]
)
in
let np_start_te =
np_target |> option_map_or_default TargetEnvs.empty (fun target ->
TargetEnvs.of_list [(target, [(env, ctx)])]
)
in
let initial_te = TargetEnvs.union pr_start_te np_start_te in
(* Delegating computation of TE with args of known types and known target to another
method. *)
self#type_check_targeted_app initial_te pr_target np_target args h_target env ctx
no_pr_vars force_pr_var
)
)
(** Assume that the target is
/\_i t_1i -> .. -> /\_i t_ki -> t
with t = pr or np. Typings of h that could make the application have the target type are
* -> .. -> * -> /\_i t_1i -> .. -> /\_i t_ki -> *
with some restrictions. If target = NP then t = np, but any * could be valid without
additional information about duplication. If t = PR then t = pr or at least one of * is
pr. *)
method filter_compatible_heads (h_te : te) (arity : int) (target : ty) : te =
let filter : ty -> bool =
if is_productive target then
let np_target = with_productivity false target in
(fun ty ->
let arg_itys, res_ty = split_ty ty arity in
Ty.equal res_ty target ||
Ty.equal res_ty np_target &&
List.fold_left (fun acc ity ->
TyList.fold_left (fun acc ty ->
if is_productive ty then
acc + 1
else
acc
) acc ity
) 0 arg_itys >= 1
)
else
(fun ty ->
let res_ty = remove_args ty arity in
Ty.equal res_ty target
)
in
h_te |> TargetEnvs.filter_targets filter
(** Annotates terms with their target types to split up the work easier. Preserves metadata. *)
method annotate_args (terms : hterm list) (loc : hloc)
(te : te) : ((hterm * (ity * hloc)) list * ty * env * ctx) list =
let len = List.length terms in
(* computing locations of leafs of arguments *)
let arg_locs =
List.rev @@ snd @@ List.fold_left (fun (arg_loc, arg_locs) arg_hterm ->
let arg_hterm_size = hg#hterm_size arg_hterm in
(arg_loc + arg_hterm_size, arg_loc :: arg_locs)
) (loc, []) terms
in
TargetEnvs.to_list te |>
List.fold_left (fun acc (ty, envs) ->
let arg_itys, codomain = split_ty ty len in
List.fold_left (fun acc (env, ctx) ->
(List.combine terms @@ List.combine arg_itys arg_locs, codomain, env, ctx) :: acc
) acc envs
) []
(** Computation of TE of an application where target type and types of each argument are
known. Targets differing only by productivity are grouped together because they have
some common typings of whole subtrees in some situations. *)
method type_check_targeted_app (initial_te : te) (pr_target : ty option) (np_target : ty option)
(args : ((hterm * (ity * hloc)) list)) (h_target : ty)
(env : env) (ctx : ctx) (no_pr_vars : bool) (force_pr_var : bool) : te =
let head_pr = is_productive h_target in
print_verbose !Flags.verbose_proofs @@ lazy (
let head_info =
if head_pr then
" -> ... -> pr"
else
" -> ... -> np";
in
"* Type checking " ^
String.concat " -> " (args |> List.map (fun (arg_term, (arg_ity, _)) ->
"(" ^ hg#string_of_hterm true HlocMap.empty 0 arg_term ^ " : " ^
string_of_ity arg_ity ^ ")"
)) ^
head_info
);
indent (+1);
(* The target is args = (arg_i: arg_ity_i)_i and the productivity of head is head_pr.
arg_ity_i are the target types of respective arguments. We already know the actual type
of head, so actual/target type terminology does not apply to head type.
We iterate over arguments while intersecting variable environments with short-circuit.
(PR) When the target is productive, there are three cases:
(1) head is productive and there are no restrictions on arguments, or
(2) head is not productive and at least one actual type of argument is productive, or
(3) head is not productive and all actual types of arguments are not productive and
there is a duplication (which also implies that at least two target types of
arguments are productive in head type assuming there are no head variables).
(NP) When the target is not productive, the head is not productive, actual types of
arguments are not productive, and there are no duplications.
Target types of arguments may still be productive as long as that does not imply
a duplication. *)
let te = fold_left_short_circuit initial_te args TargetEnvs.empty
(fun te (arg_term, (arg_ity, arg_loc)) ->
(* te contains not only variable environments, but also information whether
there was a duplication (for (3) and (NP)) and whether a productive argument
was used (for (3)). *)
TyList.fold_left_short_circuit te arg_ity TargetEnvs.empty
(fun te arg_ty ->
print_verbose !Flags.verbose_proofs @@ lazy (
"* Typing argument " ^
hg#string_of_hterm true HlocMap.empty 0 arg_term ^ " : " ^
string_of_ity arg_ity
);
indent (+1);
(* te are possible variable environments constructed so far from previous
arguments, only for the current target.
When target argument type is productive, the actual argument type can be
either productive or not productive, but with a productive variable. When
target argument is not productive, the actual argument must be not
productive and have no productive variables. *)
let arg_te =
self#type_check_arg arg_term arg_ty pr_target np_target ctx arg_loc no_pr_vars
in
let intersection = TargetEnvs.intersect te arg_te in
print_verbose !Flags.verbose_proofs @@ lazy (
"retargeted envs for the argument: " ^
TargetEnvs.to_string arg_te ^ "\n" ^
"intersected with envs: " ^
TargetEnvs.to_string te ^ "\n" ^
"env count for the argument: " ^
string_of_int (TargetEnvs.size arg_te) ^ "\n" ^
"env count after intersection: " ^
string_of_int (TargetEnvs.size intersection)
);
(* Productive target might require duplication in (3), but this requirement
is checked after all arguments are processed.
Target type being not productive implies there may be no duplication. *)
let res = TargetEnvs.filter_no_dup_for_np_targets intersection in
print_verbose !Flags.verbose_proofs @@ lazy (
"envs after no duplication filtering: " ^
TargetEnvs.to_string res ^ "\n" ^
"envs count: " ^
string_of_int (TargetEnvs.size res)
);
indent (-1);
res
)
)
in
print_verbose !Flags.verbose_proofs @@ lazy (
"* Intersected envs before duplication filtering:\n" ^
" " ^ TargetEnvs.to_string te
);
let te =
if not head_pr then
begin
(* A duplication or productive actual argument is required when head is not
productive and target type is productive. *)
let te = TargetEnvs.filter_dup_or_pr_arg_for_pr_targets te in
print_verbose !Flags.verbose_proofs @@ lazy (
"* env count after duplication or pr arg filtering: " ^
string_of_int (TargetEnvs.size te)
);
te
end
else
te
in
if force_pr_var then
let te = TargetEnvs.filter_pr_vars te in
print_verbose !Flags.verbose_proofs @@ lazy (
"* env count after pr var filtering: " ^
string_of_int (TargetEnvs.size te)
);
indent (-1);
te
else
begin
indent (-1);
te
end
(** Type checking argument of an application with known argument typing (but unknown actual
typing) for up to two versions of a target at once with common context. *)
method type_check_arg (hterm : hterm) (arg_target : ty)
(pr_target : ty option) (np_target : ty option)
(ctx : ctx) (loc : hloc)
(no_pr_vars : bool) : te =
if is_productive arg_target then
(* case when target argument is productive *)
(* subcase when actual argument is productive *)
let pr_arg_te =
(* productive actual argument implies productive target *)
(* TODO target is in keys of te, it can be extracted from there instead of passing it
as another argument *)
match pr_target with
| Some pr_target ->
(* Retarget also marks these environments with information that
productive actual argument was used and removes duplication
flags. Not passing the force_pr_var flag, since this is one of
many arguments. *)
TargetEnvs.retarget pr_target @@
self#type_check_hterm hterm (Some arg_target) ctx loc no_pr_vars false
| None -> TargetEnvs.empty
in
(* subcase when actual argument is nonproductive *)
let np_arg_te =
if no_pr_vars then
TargetEnvs.empty
else
(* productive target argument together with not productive actual
argument implies productive variable *)
let arg_te =
self#type_check_hterm hterm (Some (with_productivity false arg_target))
ctx loc false true
in
(* both target productivities are valid for nonproductive actual
argument *)
let pr_target_arg_te = match pr_target with
| Some pr_target -> TargetEnvs.retarget pr_target arg_te
| None -> TargetEnvs.empty
in
let np_target_arg_te = match np_target with
| Some np_target -> TargetEnvs.retarget np_target arg_te
| None -> TargetEnvs.empty
in
TargetEnvs.union pr_target_arg_te np_target_arg_te
in
TargetEnvs.union pr_arg_te np_arg_te
else
(* case when target argument is nonproductive *)
(* nonproductive target argument implies nonproductive actual argument
and no productive vars *)
let arg_te =
self#type_check_hterm hterm (Some arg_target) ctx loc true false
in
(* both target productivities are valid for nonproductive target
argument *)
let pr_target_arg_te = match pr_target with
| Some pr_target -> TargetEnvs.retarget pr_target arg_te
| None -> TargetEnvs.empty
in
let np_target_arg_te = match np_target with
| Some np_target -> TargetEnvs.retarget np_target arg_te
| None -> TargetEnvs.empty
in
TargetEnvs.union pr_target_arg_te np_target_arg_te
(* --- printing --- *)
method string_of_nt_ity : string =
"Types of nonterminals:\n" ^
String.concat "\n" @@ (range 0 hg#nt_count |> List.map (fun nt ->
hg#nt_name nt ^ ": " ^ string_of_ity (TySet.to_ity nt_ity.(nt))
))
method string_of_hterms_hty (should_be_printed : hterms_id -> bool) : string =
"Types of hterms:\n" ^
String.concat "\n" @@ List.filter (fun s -> s <> "")
(range 0 hg#hterms_count |> List.map (fun id ->
if should_be_printed id then
let htys = hty_store#get_htys id in
string_of_int id ^ ":\n" ^
concat_map "\n" string_of_hty @@ HtySet.elements htys
else
""
))
(* --- debugging --- *)
method get_hty_store = hty_store
end