Module ErgoSpec.Common.Names

Require Import String.

Require Import ErgoSpec.Backend.Component.LogComponent.
Require Import EquivDec.

Section Debug.
  Definition DEBUG_aux {A} s (d1 d2 : A) : A
    := match LOG_string s with
       | y => if unit_eqdec y tt then d1 else d2
       end.
  Definition DEBUG {A} s (d:A) : A :=
    DEBUG_aux s d d.
                                   
End Debug.

Section Names.
  Local Open Scope string.

  Section ScopedNames.
    Definition local_name : Set := string.
    Definition namespace_name : Set := string.
    Definition enum_name : Set := string.
    Definition namespace_prefix : Set := option namespace_name.

    Definition relative_name : Set := namespace_prefix * local_name.
    Definition absolute_name : Set := string.

    Definition absolute_name_of_local_name (ns:namespace_name) (ln:local_name) : absolute_name :=
      ns ++ "." ++ ln.

    Definition enum_namespace (ns:namespace_name) (en:enum_name) : namespace_name :=
      ns ++ "." ++ en.
      
    Definition absolute_name_of_relative_name (local_ns: namespace_name) (rn: relative_name) : absolute_name :=
      match rn with
      | (None,ln) => absolute_name_of_local_name local_ns ln
      | (Some ns,ln) => absolute_name_of_local_name ns ln
      end.

  End ScopedNames.

  Section ReservedNames.
    Definition clause_main_name : local_name := "main".
    Definition clause_init_name : local_name := "init".

    Definition this_this := "__this".
    Definition this_contract := "__contract".
    Definition this_state := "__state".
    Definition this_emit := "__emit".
    Definition this_request := "__request".
    Definition this_response := "__response".
    Definition local_state := "__lstate".
    Definition local_emit := "__lemit".
    Definition current_time := "__now".
    Definition options := "__options".

  End ReservedNames.
  
  Section TypeNames.
    Definition accordproject_base_namespace : string := "org.accordproject.base"%string.
    Definition accordproject_runtime_namespace : string := "org.accordproject.cicero.runtime"%string.
    Definition accordproject_contract_namespace : string := "org.accordproject.cicero.contract"%string.
    Definition accordproject_stdlib_namespace : string := "org.accordproject.ergo.stdlib"%string.
    Definition accordproject_time_namespace : string := "org.accordproject.time"%string.
    Definition accordproject_top_namespace : string := "org.accordproject.ergo.top"%string.
    Definition accordproject_options_namespace : string := "org.accordproject.ergo.options"%string.
    Definition accordproject_template_namespace : string := "org.accordproject.ergo.template"%string.

    Definition default_enum_absolute_name : string :=
      absolute_name_of_local_name accordproject_base_namespace "Enum".
    Definition default_event_absolute_name : string :=
      absolute_name_of_local_name accordproject_base_namespace "Event".
    Definition default_transaction_absolute_name : string :=
      absolute_name_of_local_name accordproject_base_namespace "Transaction".
    Definition default_asset_absolute_name : string :=
      absolute_name_of_local_name accordproject_base_namespace "Asset".
    Definition default_participant_absolute_name : string :=
      absolute_name_of_local_name accordproject_base_namespace "Participant".

    Definition default_request_absolute_name : string :=
      absolute_name_of_local_name accordproject_runtime_namespace "Request".
    Definition default_response_absolute_name : string :=
      absolute_name_of_local_name accordproject_runtime_namespace "Response".
    Definition default_state_absolute_name : string :=
      absolute_name_of_local_name accordproject_contract_namespace "AccordContractState".
    Definition default_contract_absolute_name : string :=
      absolute_name_of_local_name accordproject_contract_namespace "AccordContract".
    Definition default_clause_absolute_name : string :=
      absolute_name_of_local_name accordproject_contract_namespace "AccordClause".

    Definition default_error_absolute_name : string :=
      absolute_name_of_local_name accordproject_stdlib_namespace "ErgoErrorResponse".
    Definition default_options : string :=
      absolute_name_of_local_name accordproject_options_namespace "Options".

  End TypeNames.

  Section Misc.
    Definition function_name_in_table (tname:option string) (fname:string) : string :=
      match tname with
      | None => fname
      | Some tname => tname ++ "_" ++ fname
      end.
  End Misc.

  Section Namespaces.
    Definition no_namespace : string := "".
  End Namespaces.

End Names.