Qcert.Compiler.Driver.CompConfig

Section CompConfig.


  Context {ft:foreign_type}.
  Context {fr:foreign_runtime}.
  Context {bm:brand_model}.


  Section optim.


    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.


    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_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
         nil
         EmptyString
         nil
         EmptyString
         nil.


  Definition default_dv_config :=
    mkDvConfig
       "query"
       "query"
       nil
       init_vinit
       nil
       ""
       nil.

End CompConfig.