Module CompConfig

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).
      
  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.

    Lemma vdbindings_of_constants_config_commutes x:
      vdbindings_of_constants_config (constants_config_of_tdbindings x)
      = vdbindings_of_tdbindings x.
    
    Lemma vdbindings_of_constants_config_prefixed_commutes x:
      vdbindings_of_constants_config_prefixed (constants_config_of_tdbindings x)
      = mkConstants (vdbindings_of_tdbindings x).
    
    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.
      
  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.