Section CompConfig.
Require Import List.
Require Import String.
Require Import BasicSystem.
Require Import TypingRuntime.
Require Import ForeignReduceOps.
Context {
ft:
foreign_type}.
Context {
fr:
foreign_runtime}.
Context {
bm:
brand_model}.
Require Import OptimizerLogger.
Require Import CompLang CompEnv.
Section optim.
Require Import NNRCOptimizer.
Require Import NRAEnvOptimizer.
Require Import OptimizerStep.
Definition optim_type_of_language (
l:
language) :
Set :=
match l with
|
L_nra =>
nraenv
|
L_nraenv_core =>
nraenv
|
L_nraenv =>
nraenv
|
L_nnrc_core =>
nnrc
|
L_nnrc =>
nnrc
|
_ =>
Empty_set
end.
Definition optim_config_list_type :=
list {
l:
language & (
string *
list (
OptimizerStep (
optim_type_of_language l)))}%
type.
Definition optim_config_list :
optim_config_list_type
:=
existT _ L_nra ("
NRAEnv.Optim.NRAEnvOptimizer"%
string,
tnraenv_optim_list)
::
existT _ L_nraenv_core ("
NRAEnv.Optim.NRAEnvOptimizer"%
string,
tnraenv_optim_list)
::
existT _ L_nraenv ("
NRAEnv.Optim.NRAEnvOptimizer"%
string,
tnraenv_optim_list)
::
existT _ L_nnrc_core ("
NNRC.Optim.TNNRCOptimizer"%
string,
tnnrc_optim_list)
::
existT _ L_nnrc ("
NNRC.Optim.TNNRCOptimizer"%
string,
tnnrc_optim_list)
::
nil.
Definition optim_config :
Set :=
list (
language *
optim_phases_config).
Definition optim_config_default :
optim_config :=
(
L_nra,
default_nraenv_optim_phases)
:: (
L_nraenv_core,
default_nraenv_optim_phases)
:: (
L_nraenv,
default_nraenv_optim_phases)
:: (
L_nnrc_core,
default_nnrc_optim_phases)
:: (
L_nnrc,
default_nnrc_optim_phases)
::
nil.
Definition get_default_optim_config (
l:
language) :
optim_phases_config :=
match lookup language_eq_dec optim_config_default l with
|
Some x =>
x
|
None =>
nil
end.
Definition get_optim_config (
l:
language) (
oc:
optim_config) :
optim_phases_config :=
match lookup language_eq_dec oc l with
|
Some opc =>
opc
|
None =>
get_default_optim_config l
end.
Require Import Permutation.
Remark optim_config_list_default_in_sync :
Permutation
(
map (@
projT1 _ _)
optim_config_list)
(
map fst optim_config_default).
Proof.
End optim.
Section constants.
Record constant_config :=
mkConstantConfig {
constant_localization :
dlocalization;
constant_type :
rtype; }.
Definition constants_config :=
list (
string *
constant_config).
Definition vdbindings_of_constants_config (
cconf:
constants_config) :=
map (
fun xy => (
fst xy, (
snd xy).(
constant_localization)))
cconf.
Definition vdbindings_of_constants_config_prefixed (
cconf:
constants_config) :=
mkConstants (
map (
fun xy => (
fst xy, (
snd xy).(
constant_localization)))
cconf).
Definition tbindings_of_constants_config (
cconf:
constants_config) :=
map (
fun xy => (
fst xy, (
snd xy).(
constant_type)))
cconf.
Definition tdbinding_of_constant_config (
gc:
string *
constant_config) :=
let (
s,
cc) :=
gc in
(
s,
v_and_t_to_dt cc.(
constant_localization)
cc.(
constant_type)).
Definition tdbindings_of_constants_config (
gc:
constants_config) :=
map tdbinding_of_constant_config gc.
Definition constant_config_of_tdbinding_opt (
td:
string *
drtype) :
string *
constant_config :=
match td with
| (
s,
Tlocal t) => (
s,
mkConstantConfig Vlocal t)
| (
s,
Tdistr t) => (
s,
mkConstantConfig Vdistr (
Coll t))
end.
Definition constant_config_of_tdbinding (
td:
string *
drtype) :
string *
constant_config :=
match td with
| (
s,
Tlocal t) => (
s,
mkConstantConfig Vlocal t)
| (
s,
Tdistr t) => (
s,
mkConstantConfig Vdistr t)
end.
Definition constants_config_of_tdbindings (
tds:
tdbindings) :
constants_config :=
map constant_config_of_tdbinding tds.
Lemma constants_config_of_tdbindings_merges (
tds:
tdbindings) :
tdbindings_of_constants_config (
constants_config_of_tdbindings tds)
=
tds.
Proof.
induction tds;
simpl.
-
reflexivity.
-
unfold tdbindings_of_constants_config in *;
simpl.
rewrite IHtds;
clear IHtds.
destruct a;
simpl in *.
destruct d;
simpl in *;
reflexivity.
Qed.
Lemma vdbindings_of_constants_config_commutes x:
vdbindings_of_constants_config (
constants_config_of_tdbindings x)
=
vdbindings_of_tdbindings x.
Proof.
induction x; simpl.
- reflexivity.
- rewrite IHx.
destruct a; simpl.
destruct d; simpl; reflexivity.
Qed.
Lemma vdbindings_of_constants_config_prefixed_commutes x:
vdbindings_of_constants_config_prefixed (
constants_config_of_tdbindings x)
=
mkConstants (
vdbindings_of_tdbindings x).
Proof.
Definition one_tdbindings_of_avoid_list (
avoid:
list string) :
tdbindings :=
map (
fun x => (
x,
Tlocal Unit))
avoid.
Definition one_constant_config_of_avoid_list (
avoid:
list string) :
constants_config :=
constants_config_of_tdbindings (
one_tdbindings_of_avoid_list avoid).
Lemma one_constant_config_of_avoid_list_extracts (
avoid:
list string) :
map fst (
vdbindings_of_constants_config (
one_constant_config_of_avoid_list avoid)) =
avoid.
Proof.
End constants.
Record driver_config :=
mkDvConfig
{
comp_qname :
string;
comp_qname_lowercase :
string;
comp_class_name :
string;
comp_brand_rel :
list (
string *
string) ;
comp_mr_vinit :
string;
comp_constants :
constants_config;
comp_java_imports :
string;
comp_optim_config :
optim_config; }.
Definition trivial_driver_config :
driver_config
:=
mkDvConfig
EmptyString
EmptyString
EmptyString
nil
EmptyString
nil
EmptyString
nil.
Definition default_dv_config :=
mkDvConfig
"
query"
"
query"
"
query"
nil
init_vinit
nil
""
nil.
End CompConfig.