Abstract Syntax

Require Import String.
Require Import List.
Require Import ErgoSpec.Backend.QLib.
Require Import ErgoSpec.Common.Provenance.
Require Import ErgoSpec.Common.Names.
Require Import ErgoSpec.Common.NamespaceContext.
Require Import ErgoSpec.Common.Result.
Require Import ErgoSpec.Common.Ast.
Require Import ErgoSpec.Types.CTO.
Require Import ErgoSpec.Types.ErgoType.
Require Import ErgoSpec.Ergo.Lang.Ergo.
Require Import ErgoSpec.Ergo.Lang.ErgoSugar.
Require Import ErgoSpec.Translation.CTOtoErgo.

Section ErgoNameResolution.

  Fixpoint namespace_ctxt_of_ergo_decls
           (ctxt:namespace_ctxt)
           (ns:namespace_name)
           (dls:list lrergo_declaration) : (namespace_name * namespace_ctxt) :=
    match dls with
    | nil => (ns, ctxt)
    | DNamespace _ ns' :: rest =>
      (ns', ctxt)
    | DImport _ _ :: rest =>
      namespace_ctxt_of_ergo_decls ctxt ns rest
    | DType prov td :: rest =>
      let ln := td.(type_declaration_name) in
      let an := absolute_name_of_local_name ns ln in
      let ef : enum_flag :=
          match type_declaration_is_enum td.(type_declaration_type) with
          | None => EnumNone
          | Some enum_list =>
            let proc_enum := globals_from_enum prov (an,enum_list) in
            EnumType (map (fun xyz => (fst (fst xyz), snd xyz)) proc_enum)
          end
      in
      let (ns, ctxt) := namespace_ctxt_of_ergo_decls ctxt ns rest in
      (ns, add_type_to_namespace_ctxt ctxt ns ln an ef)
    | DStmt _ _ :: rest =>
      let ctxt := namespace_ctxt_of_ergo_decls ctxt ns rest in
      ctxt
    | DConstant _ ln ta cd :: rest =>
      let an := absolute_name_of_local_name ns ln in
      let (ns, ctxt) := namespace_ctxt_of_ergo_decls ctxt ns rest in
      (ns, add_constant_to_namespace_ctxt ctxt ns ln EnumNone an)
    | DFunc _ ln fd :: rest =>
      let an := absolute_name_of_local_name ns ln in
      let (ns, ctxt) := namespace_ctxt_of_ergo_decls ctxt ns rest in
      (ns, add_function_to_namespace_ctxt ctxt ns ln an)
    | DContract _ ln _ :: rest =>
      let an := absolute_name_of_local_name ns ln in
      let (ns, ctxt) := namespace_ctxt_of_ergo_decls ctxt ns rest in
      (ns, add_contract_to_namespace_ctxt ctxt ns ln an)
    | DSetContract _ ln _ :: rest =>
      namespace_ctxt_of_ergo_decls ctxt ns rest
    end.

  Definition namespace_ctxt_of_ergo_module (ctxt:namespace_ctxt) (m:lrergo_module) : namespace_ctxt :=
    snd (namespace_ctxt_of_ergo_decls ctxt m.(module_namespace) m.(module_declarations)).

  Definition namespace_ctxt_of_ergo_modules (ctxt:namespace_ctxt) (ml:list lrergo_module) : namespace_ctxt :=
    fold_left namespace_ctxt_of_ergo_module ml ctxt.

  Definition namespace_ctxt_of_cto_packages (ctxt:namespace_ctxt) (ctos:list cto_package) : namespace_ctxt :=
    let mls := map cto_package_to_ergo_module ctos in
    fold_left namespace_ctxt_of_ergo_module mls ctxt.

  Section ResolveImports.
    Definition lookup_one_import
               (ctxt:namespace_ctxt)
               (ic:limport_decl) : eresult namespace_table :=
      match ic with
      | ImportAll prov ns =>
        match lookup string_dec ctxt.(namespace_ctxt_modules) ns with
        | Some tbl => esuccess tbl nil
        | None => import_not_found_error prov ns
        end
      | ImportSelf prov ns =>
        match lookup string_dec ctxt.(namespace_ctxt_modules) ns with
        | Some tbl => esuccess tbl nil
        | None => esuccess empty_namespace_table nil
        end
      | ImportName prov ns ln =>
        match lookup string_dec ctxt.(namespace_ctxt_modules) ns with
        | Some tbl =>
          match lookup string_dec tbl.(namespace_table_types) ln with
          | None =>
            match lookup string_dec tbl.(namespace_table_constants) ln with
            | Some an =>
              esuccess (import_one_constant_to_namespace_table ln (fst an)) nil
            | None =>
              import_name_not_found_error prov ns ln
            end
          | Some (an,EnumType l) =>
            esuccess (import_one_enum_type_to_namespace_table ln an l) nil
          | Some (an,_) =>
            esuccess (import_one_type_to_namespace_table ln an) nil
          end
        | None => import_not_found_error prov ns
        end
      end.

    Definition resolve_one_import
               (ctxt:namespace_ctxt)
               (ic:limport_decl) : eresult namespace_ctxt :=
      elift (fun tbl =>
               mkNamespaceCtxt
                 ctxt.(namespace_ctxt_modules)
                 ctxt.(namespace_ctxt_namespace)
                 ctxt.(namespace_ctxt_current_module)
                 (namespace_table_app ctxt.(namespace_ctxt_current_in_scope) tbl)
                 ctxt.(namespace_ctxt_abstract))
            (lookup_one_import ctxt ic).

    Definition builtin_imports :=
      accordproject_base_namespace
        :: accordproject_stdlib_namespace
        :: nil.
    Definition is_builtin_import (ns:namespace_name) : bool :=
      if in_dec string_dec ns builtin_imports
      then true
      else false.

    Definition stdlib_imports :=
      accordproject_base_namespace
        :: accordproject_stdlib_namespace
        :: accordproject_time_namespace
        :: accordproject_options_namespace
        :: accordproject_template_namespace
        :: nil.
    Definition is_stdlib_import (ns:namespace_name) : bool :=
      if in_dec string_dec ns stdlib_imports
      then true
      else false.

  End ResolveImports.

  Section NameResolution.
    Fixpoint resolve_ergo_type
             (nsctxt:namespace_ctxt)
             (t:lrergo_type) : eresult laergo_type :=
      match t with
      | ErgoTypeAny prov => esuccess (ErgoTypeAny prov) nil
      | ErgoTypeNothing prov => esuccess (ErgoTypeNothing prov) nil
      | ErgoTypeUnit prov => esuccess (ErgoTypeUnit prov) nil
      | ErgoTypeBoolean prov => esuccess (ErgoTypeBoolean prov) nil
      | ErgoTypeString prov => esuccess (ErgoTypeString prov) nil
      | ErgoTypeDouble prov => esuccess (ErgoTypeDouble prov) nil
      | ErgoTypeLong prov => esuccess (ErgoTypeLong prov) nil
      | ErgoTypeInteger prov => esuccess (ErgoTypeInteger prov) nil
      | ErgoTypeDateTime prov => esuccess (ErgoTypeDateTime prov) nil
      | ErgoTypeDateTimeFormat prov => esuccess (ErgoTypeDateTimeFormat prov) nil
      | ErgoTypeDuration prov => esuccess (ErgoTypeDuration prov) nil
      | ErgoTypePeriod prov => esuccess (ErgoTypePeriod prov) nil
      | ErgoTypeClassRef prov rn =>
        elift (ErgoTypeClassRef prov) (resolve_type_name prov nsctxt rn)
      | ErgoTypeOption prov t =>
        elift (ErgoTypeOption prov) (resolve_ergo_type nsctxt t)
      | ErgoTypeRecord prov r =>
        let initial_map := map (fun xy => (fst xy, resolve_ergo_type nsctxt (snd xy))) r in
        let lifted_map := emaplift (fun xy => elift (fun t => (fst xy, t)) (snd xy)) initial_map in
        elift (ErgoTypeRecord prov) lifted_map
      | ErgoTypeArray prov t =>
        elift (ErgoTypeArray prov) (resolve_ergo_type nsctxt t)
      | ErgoTypeSum prov t1 t2 =>
        elift2 (ErgoTypeSum prov)
               (resolve_ergo_type nsctxt t1)
               (resolve_ergo_type nsctxt t2)
      end.

    Definition resolve_ergo_type_struct
               (nsctxt:namespace_ctxt)
               (t:list (string * lrergo_type)) : eresult (list (string * laergo_type)) :=
      emaplift (fun xy =>
                  elift (fun t => (fst xy, t)) (resolve_ergo_type nsctxt (snd xy))) t.

    Definition resolve_type_annotation
               (prov:provenance)
               (nsctxt:namespace_ctxt)
               (en:option relative_name) : eresult (option absolute_name) :=
      match en with
      | None => esuccess None nil
      | Some rn => elift Some (resolve_type_name prov nsctxt rn)
      end.

    Definition resolve_extends
               (prov:provenance)
               (nsctxt:namespace_ctxt)
               (en:rextends) : eresult aextends :=
      resolve_type_annotation prov nsctxt en.

    Definition resolve_ergo_type_signature
               (prov:provenance)
               (nsctxt:namespace_ctxt)
               (fname:string)
               (sig:lrergo_type_signature) : eresult laergo_type_signature :=
      let params_types := resolve_ergo_type_struct nsctxt (sig.(type_signature_params)) in
      let params_types :=
          eolift (fun ps => (duplicate_function_params_check prov fname (map fst ps) ps)) params_types
      in
      let output_type : eresult (option laergo_type) :=
          match sig.(type_signature_output) with
          | None => esuccess None nil
          | Some out_ty =>
            elift Some (resolve_ergo_type nsctxt out_ty)
          end
      in
      let emits_type : eresult (option laergo_type) :=
          match sig.(type_signature_emits) with
          | None => esuccess None nil
          | Some emits_ty =>
            elift Some (resolve_ergo_type nsctxt emits_ty)
          end
      in
      elift3 (mkErgoTypeSignature
                sig.(type_signature_annot))
             params_types
             output_type
             emits_type.

    Definition resolve_ergo_type_clauses
               (prov:provenance)
               (nsctxt:namespace_ctxt)
               (cls:list (string * lrergo_type_signature)) : eresult (list (string * laergo_type_signature)) :=
      emaplift (fun xy => elift (fun r => (fst xy, r))
                                (resolve_ergo_type_signature prov nsctxt (fst xy) (snd xy))) cls.

    Definition resolve_ergo_type_declaration_desc
               (prov:provenance)
               (nsctxt:namespace_ctxt)
               (name:string)
               (d:lrergo_type_declaration_desc)
      : eresult laergo_type_declaration_desc :=
      match d with
      | ErgoTypeEnum l => esuccess (ErgoTypeEnum l) nil
      | ErgoTypeTransaction isabs extends_name ergo_type_struct =>
        elift2 (ErgoTypeTransaction isabs)
               (resolve_extends prov nsctxt extends_name)
               (resolve_ergo_type_struct nsctxt ergo_type_struct)
      | ErgoTypeConcept isabs extends_name ergo_type_struct =>
        elift2 (ErgoTypeConcept isabs)
               (resolve_extends prov nsctxt extends_name)
               (resolve_ergo_type_struct nsctxt ergo_type_struct)
      | ErgoTypeEvent isabs extends_name ergo_type_struct =>
        elift2 (ErgoTypeEvent isabs)
               (resolve_extends prov nsctxt extends_name)
               (resolve_ergo_type_struct nsctxt ergo_type_struct)
      | ErgoTypeAsset isabs extends_name ergo_type_struct =>
        elift2 (ErgoTypeAsset isabs)
               (resolve_extends prov nsctxt extends_name)
               (resolve_ergo_type_struct nsctxt ergo_type_struct)
      | ErgoTypeParticipant isabs extends_name ergo_type_struct =>
        elift2 (ErgoTypeParticipant isabs)
               (resolve_extends prov nsctxt extends_name)
               (resolve_ergo_type_struct nsctxt ergo_type_struct)
      | ErgoTypeGlobal ergo_type =>
        elift ErgoTypeGlobal (resolve_ergo_type nsctxt ergo_type)
      | ErgoTypeFunction ergo_type_signature =>
        elift ErgoTypeFunction
              (resolve_ergo_type_signature prov nsctxt name ergo_type_signature)
      | ErgoTypeContract template_type state_type clauses_sigs =>
        elift3 ErgoTypeContract
               (resolve_ergo_type nsctxt template_type)
               (resolve_ergo_type nsctxt state_type)
               (resolve_ergo_type_clauses prov nsctxt clauses_sigs)
      end.
 
    Definition resolve_ergo_type_declaration
               prov
               (module_ns:namespace_name)
               (nsctxt:namespace_ctxt)
               (decl: abstract_ctxt * lrergo_type_declaration)
      : eresult (abstract_ctxt * laergo_declaration * list (string * laergo_expr * data)) :=
      let '(actxt,decl) := decl in
      let name := absolute_name_of_local_name module_ns decl.(type_declaration_name) in
      let enumglobals : list (string * laergo_expr * data) :=
          match type_declaration_is_enum decl.(type_declaration_type) with
          | None => nil
          | Some enum_list => globals_from_enum prov (name,enum_list)
          end
      in
      let actxt :=
          if type_declaration_is_abstract decl.(type_declaration_type)
          then name :: actxt
          else actxt
      in
      let edecl_desc :=
          resolve_ergo_type_declaration_desc
            decl.(type_declaration_annot) nsctxt decl.(type_declaration_name) decl.(type_declaration_type)
      in
      elift (fun k => (actxt,
                       DType prov (mkErgoTypeDeclaration decl.(type_declaration_annot) name k), enumglobals))
            edecl_desc.

    Definition resolve_ergo_pattern
               (nsctxt:namespace_ctxt)
               (p:lrergo_pattern) : eresult (laergo_pattern) :=
      match p with
      | CaseData prov d => esuccess (CaseData prov d) nil
      | CaseEnum prov v =>
        let ename := resolve_econstant_name prov nsctxt v in
        elift (CaseData prov) (elift snd ename)
      | CaseWildcard prov ta => elift (CaseWildcard prov) (resolve_type_annotation prov nsctxt ta)
      | CaseLet prov v ta => elift (CaseLet prov v) (resolve_type_annotation prov nsctxt ta)
      | CaseLetOption prov v ta => elift (CaseLetOption prov v) (resolve_type_annotation prov nsctxt ta)
      end.

    Fixpoint resolve_ergo_expr
             (nsctxt:namespace_ctxt)
             (e:lrergo_expr) : eresult laergo_expr :=
      match e with
      | EThis prov => esuccess (EThis prov) nil
      | EThisContract prov => esuccess (EThisContract prov) nil
      | EThisClause prov => esuccess (EThisClause prov) nil
      | EThisState prov => esuccess (EThisState prov) nil
      | EVar prov (None,v) =>
        let cname := resolve_all_constant_name prov nsctxt (None,v) in
        elift_both
          (fun x => esuccess (EVar prov x) nil)
          (fun e => esuccess (EVar prov v) nil)
          cname
      | EVar prov (Some ns,v) =>
        let cname := resolve_all_constant_name prov nsctxt (Some ns,v) in
        elift
          (EVar prov)
          cname
      | EConst prov d => esuccess (EConst prov d) nil
      | ENone prov => esuccess (ENone prov) nil
      | EText prov el =>
        let init_el := esuccess nil nil in
        let proc_one (e:lrergo_expr) (acc:eresult (list laergo_expr)) : eresult (list laergo_expr) :=
            elift2
              cons
              (resolve_ergo_expr nsctxt e)
              acc
        in
        elift (EText prov) (fold_right proc_one init_el el)
      | ESome prov e =>
        elift (ESome prov)
              (resolve_ergo_expr nsctxt e)
      | EArray prov el =>
        let init_el := esuccess nil nil in
        let proc_one (e:lrergo_expr) (acc:eresult (list laergo_expr)) : eresult (list laergo_expr) :=
            elift2
              cons
              (resolve_ergo_expr nsctxt e)
              acc
        in
        elift (EArray prov) (fold_right proc_one init_el el)
      | EUnaryOperator prov u e =>
        elift (EUnaryOperator prov u)
              (resolve_ergo_expr nsctxt e)
      | EBinaryOperator prov b e1 e2 =>
        elift2 (EBinaryOperator prov b)
               (resolve_ergo_expr nsctxt e1)
               (resolve_ergo_expr nsctxt e2)
      | EUnaryBuiltin prov u e =>
        elift (EUnaryBuiltin prov u)
              (resolve_ergo_expr nsctxt e)
      | EBinaryBuiltin prov b e1 e2 =>
        elift2 (EBinaryBuiltin prov b)
               (resolve_ergo_expr nsctxt e1)
               (resolve_ergo_expr nsctxt e2)
      | EIf prov e1 e2 e3 =>
        elift3 (EIf prov)
               (resolve_ergo_expr nsctxt e1)
               (resolve_ergo_expr nsctxt e2)
               (resolve_ergo_expr nsctxt e3)
      | ELet prov v ta e1 e2 =>
        let rta :=
            match ta with
            | None => esuccess None nil
            | Some ta => elift Some (resolve_ergo_type nsctxt ta)
            end
        in
        elift3 (ELet prov v)
               rta
               (resolve_ergo_expr nsctxt e1)
               (resolve_ergo_expr (hide_constant_from_namespace_ctxt_current nsctxt v) e2)
      | EPrint prov e1 e2 =>
        elift2 (EPrint prov)
               (resolve_ergo_expr nsctxt e1)
               (resolve_ergo_expr nsctxt e2)
      | ENew prov cr el =>
        let rcr := resolve_type_name prov nsctxt cr in
        let init_rec := esuccess nil nil in
        let proc_one (att:string * lrergo_expr) (acc:eresult (list (string * laergo_expr))) :=
            let attname := fst att in
            let e := resolve_ergo_expr nsctxt (snd att) in
            elift2 (fun e => fun acc => (attname,e)::acc) e acc
        in
        elift2 (ENew prov) rcr (fold_right proc_one init_rec el)
      | ERecord prov el =>
        let init_rec := esuccess nil nil in
        let proc_one (att:string * lrergo_expr) (acc:eresult (list (string * laergo_expr))) :=
            let attname := fst att in
            let e := resolve_ergo_expr nsctxt (snd att) in
            elift2 (fun e => fun acc => (attname,e)::acc) e acc
        in
        elift (ERecord prov) (fold_right proc_one init_rec el)
      | ECallFun prov fname el =>
        let rfname := resolve_function_name prov nsctxt fname in
        let init_el := esuccess nil nil in
        let proc_one (e:lrergo_expr) (acc:eresult (list laergo_expr)) : eresult (list laergo_expr) :=
            elift2
              cons
              (resolve_ergo_expr nsctxt e)
              acc
        in
        elift2 (ECallFun prov) rfname (fold_right proc_one init_el el)
      | ECallFunInGroup prov gname fname el =>
        let rgname := resolve_contract_name prov nsctxt gname in
        let init_el := esuccess nil nil in
        let proc_one (e:lrergo_expr) (acc:eresult (list laergo_expr)) : eresult (list laergo_expr) :=
            elift2
              cons
              (resolve_ergo_expr nsctxt e)
              acc
        in
        elift3 (ECallFunInGroup prov) rgname (esuccess fname nil) (fold_right proc_one init_el el)
      | EMatch prov e0 ecases edefault =>
        let ec0 := resolve_ergo_expr nsctxt e0 in
        let eccases :=
            let proc_one acc (ecase : lrergo_pattern * lrergo_expr) :=
                let (pcase, pe) := ecase in
                let apcase := resolve_ergo_pattern nsctxt pcase in
                eolift (fun apcase =>
                          eolift
                            (fun acc =>
                               elift (fun x => (apcase, x)::acc)
                                     (resolve_ergo_expr nsctxt pe)) acc)
                       apcase
            in
            fold_left proc_one ecases (esuccess nil nil)
        in
        let ecdefault := resolve_ergo_expr nsctxt edefault in
        eolift
          (fun ec0 : laergo_expr =>
             eolift
               (fun eccases : list (laergo_pattern * laergo_expr) =>
                  elift
                    (fun ecdefault : laergo_expr =>
                    EMatch prov ec0 eccases ecdefault)
                    ecdefault) eccases) ec0
      | EForeach prov foreachs econd e2 =>
        let re2 := resolve_ergo_expr nsctxt e2 in
        let recond :=
            match econd with
            | None => esuccess None nil
            | Some econd => elift Some (resolve_ergo_expr nsctxt econd)
            end
        in
        let init_e := esuccess nil nil in
        let proc_one
              (foreach:string * lrergo_expr)
              (acc:eresult (list (string * laergo_expr)))
            : eresult (list (string * laergo_expr)) :=
            let v := fst foreach in
            let e := resolve_ergo_expr nsctxt (snd foreach) in
            elift2 (fun e => fun acc => (v,e)::acc)
                 e
                 acc
        in
        elift3 (EForeach prov)
               (fold_right proc_one init_e foreachs)
               recond
               re2
      end.

    Fixpoint resolve_ergo_stmt
             (nsctxt:namespace_ctxt)
             (e:lrergo_stmt) : eresult laergo_stmt :=
      match e with
      | SReturn prov e => elift (SReturn prov) (resolve_ergo_expr nsctxt e)
      | SFunReturn prov e => elift (SFunReturn prov) (resolve_ergo_expr nsctxt e)
      | SThrow prov e => elift (SThrow prov) (resolve_ergo_expr nsctxt e)
      | SCallClause prov e0 fname el =>
        let init_el := esuccess nil nil in
        let proc_one (e:lrergo_expr) (acc:eresult (list laergo_expr)) : eresult (list laergo_expr) :=
            elift2
              cons
              (resolve_ergo_expr nsctxt e)
              acc
        in
        elift3 (SCallClause prov)
               (resolve_ergo_expr nsctxt e0)
               (esuccess fname nil)
               (fold_right proc_one init_el el)
      | SCallContract prov e0 el =>
        let init_el := esuccess nil nil in
        let proc_one (e:lrergo_expr) (acc:eresult (list laergo_expr)) : eresult (list laergo_expr) :=
            elift2
              cons
              (resolve_ergo_expr nsctxt e)
              acc
        in
        elift2 (SCallContract prov)
               (resolve_ergo_expr nsctxt e0)
               (fold_right proc_one init_el el)
      | SSetState prov e1 s2 =>
        elift2 (SSetState prov)
               (resolve_ergo_expr nsctxt e1)
               (resolve_ergo_stmt nsctxt s2)
      | SSetStateDot prov a e1 s2 =>
        elift2 (SSetStateDot prov a)
               (resolve_ergo_expr nsctxt e1)
               (resolve_ergo_stmt nsctxt s2)
      | SEmit prov e1 s2 =>
        elift2 (SEmit prov)
               (resolve_ergo_expr nsctxt e1)
               (resolve_ergo_stmt nsctxt s2)
      | SLet prov v ta e1 s2 =>
        let rta :=
            match ta with
            | None => esuccess None nil
            | Some ta => elift Some (resolve_ergo_type nsctxt ta)
            end
        in
        elift3 (SLet prov v)
               rta
               (resolve_ergo_expr nsctxt e1)
               (resolve_ergo_stmt (hide_constant_from_namespace_ctxt_current nsctxt v) s2)
      | SPrint prov e1 s2 =>
        elift2 (SPrint prov)
               (resolve_ergo_expr nsctxt e1)
               (resolve_ergo_stmt nsctxt s2)
      | SIf prov e1 s2 s3 =>
        elift3 (SIf prov)
               (resolve_ergo_expr nsctxt e1)
               (resolve_ergo_stmt nsctxt s2)
               (resolve_ergo_stmt nsctxt s3)
      | SEnforce prov e1 os2 s3 =>
        let rs2 :=
            match os2 with
            | None => esuccess None nil
            | Some s2 => elift Some (resolve_ergo_stmt nsctxt s2)
            end
        in
        elift3 (SEnforce prov)
               (resolve_ergo_expr nsctxt e1)
               rs2
               (resolve_ergo_stmt nsctxt s3)
      | SMatch prov e0 scases sdefault =>
        let ec0 := resolve_ergo_expr nsctxt e0 in
        let sccases :=
            let proc_one acc (scase : lrergo_pattern * lrergo_stmt) :=
                let (pcase, pe) := scase in
                let apcase := resolve_ergo_pattern nsctxt pcase in
                eolift (fun apcase =>
                          eolift
                            (fun acc =>
                               elift (fun x => (apcase, x)::acc)
                                     (resolve_ergo_stmt nsctxt pe)) acc)
                       apcase
            in
            fold_left proc_one scases (esuccess nil nil)
        in
        let scdefault := resolve_ergo_stmt nsctxt sdefault in
        eolift
          (fun ec0 : laergo_expr =>
             eolift
               (fun sccases : list (laergo_pattern * laergo_stmt) =>
                  elift
                    (fun scdefault : laergo_stmt =>
                    SMatch prov ec0 sccases scdefault)
                    scdefault) sccases) ec0
      end.


    Definition resolve_ergo_function
               (module_ns:namespace_name)
               (nsctxt:namespace_ctxt)
               (name:string)
               (f:lrergo_function) : eresult laergo_function :=
      let prov := f.(function_annot) in
      let sig := f.(function_sig) in
      let params := List.map fst sig.(type_signature_params) in
      let nsctxt := hide_constants_from_namespace_ctxt_current nsctxt params in
      let rbody :=
          match f.(function_body) with
          | None => esuccess None nil
          | Some body => elift Some (resolve_ergo_expr nsctxt body)
          end
      in
      elift2 (mkFunc prov)
             (resolve_ergo_type_signature prov nsctxt name sig)
             rbody.
    
    Definition resolve_ergo_clause
               (module_ns:namespace_name)
               (nsctxt:namespace_ctxt)
               (c:ergo_clause) : eresult laergo_clause :=
      let prov := c.(clause_annot) in
      let rcname := c.(clause_name) in
      let rbody :=
          match c.(clause_body) with
          | None => esuccess None nil
          | Some body => elift Some (resolve_ergo_stmt nsctxt body)
          end
      in
      elift2 (mkClause prov rcname)
             (resolve_ergo_type_signature prov nsctxt rcname c.(clause_sig))
             rbody.

    Definition resolve_ergo_clauses
               (module_ns:namespace_name)
               (nsctxt:namespace_ctxt)
               (cl:list ergo_clause) : eresult (list laergo_clause) :=
      emaplift (resolve_ergo_clause module_ns nsctxt) cl.

    Definition resolve_ergo_contract
               (module_ns:namespace_name)
               (nsctxt:namespace_ctxt)
               (c:lrergo_contract) : eresult laergo_contract :=
      let prov := c.(contract_annot) in
      let rtemplate := resolve_ergo_type nsctxt c.(contract_template) in
      let rstate :=
          match c.(contract_state) with
          | None => esuccess None nil
          | Some state => elift Some (resolve_ergo_type nsctxt state)
          end
      in
      elift3 (mkContract prov)
             rtemplate
             rstate
             (resolve_ergo_clauses module_ns nsctxt c.(contract_clauses)).

    Definition resolve_ergo_declaration
               (nsctxt:namespace_ctxt)
               (decl:lrergo_declaration)
      : eresult (list laergo_declaration * namespace_ctxt) :=
      let module_ns : namespace_name := nsctxt.(namespace_ctxt_namespace) in
      let actxt := nsctxt.(namespace_ctxt_abstract) in
      match decl with
      | DNamespace prov ns =>
        esuccess (DNamespace prov ns :: nil, local_namespace_scope nsctxt ns) nil
      | DImport prov id =>
        elift (fun x => (DImport prov id :: nil, x)) (resolve_one_import nsctxt id)
      | DType prov td =>
        let ln := td.(type_declaration_name) in
        let an := absolute_name_of_local_name module_ns ln in
        let ef : enum_flag :=
            match type_declaration_is_enum td.(type_declaration_type) with
            | None => EnumNone
            | Some enum_list =>
              let proc_enum := globals_from_enum prov (an,enum_list) in
              EnumType (map (fun xyz => (fst (fst xyz), snd xyz)) proc_enum)
            end
        in
        let nsctxt := add_type_to_namespace_ctxt_current nsctxt ln an ef in
        elift (fun xy : abstract_ctxt * laergo_declaration * list (string * laergo_expr * data) =>
                 let '(actxt,x,globalenums) := xy in
                 let nsctxt := update_namespace_context_abstract nsctxt actxt in
                 let enum_ns := enum_namespace module_ns ln in
                 let (rglobalnames,rglobalenums) :=
                     split
                       (map (fun xyz : string * laergo_expr * data =>
                               let '(en, expr, d) := xyz in
                               let an := absolute_name_of_local_name enum_ns en in
                               ((en,(an,EnumValue d)), DConstant prov an None expr)
                               ) globalenums)
                 in
                 let nsctxt := add_econstants_to_namespace_ctxt_current nsctxt enum_ns rglobalnames in
                 (x::rglobalenums, nsctxt))
              (resolve_ergo_type_declaration prov module_ns nsctxt (actxt, td))
      | DStmt prov st =>
        elift (fun x => (DStmt prov x::nil, nsctxt)) (resolve_ergo_stmt nsctxt st)
      | DConstant prov ln ta e =>
        let an := absolute_name_of_local_name module_ns ln in
        let rta :=
            match ta with
            | None => esuccess None nil
            | Some ta => elift Some (resolve_ergo_type nsctxt ta)
            end
        in
        let nsctxt := add_constant_to_namespace_ctxt_current nsctxt ln an EnumNone in
        elift2 (fun ta x => (DConstant prov an ta x::nil, nsctxt))
               rta
               (resolve_ergo_expr nsctxt e)
      | DFunc prov ln fd =>
        let an := absolute_name_of_local_name module_ns ln in
        let nsctxt := add_function_to_namespace_ctxt_current nsctxt ln an in
        elift (fun x => (DFunc prov an x :: nil, nsctxt)) (resolve_ergo_function module_ns nsctxt an fd)
      | DContract prov ln c =>
        let an := absolute_name_of_local_name module_ns ln in
        let nsctxt := add_contract_to_namespace_ctxt_current nsctxt ln an in
        elift (fun x => (DContract prov an x :: nil, nsctxt)) (resolve_ergo_contract module_ns nsctxt c)
      | DSetContract prov rn e1 =>
        eolift (fun an =>
                  elift (fun x => (DSetContract prov an x :: nil, nsctxt))
                        (resolve_ergo_expr nsctxt e1))
               (resolve_contract_name prov nsctxt rn)
      end.

    Definition resolve_ergo_template_expr := resolve_ergo_expr.

    Definition resolve_ergo_declarations
               (ctxt:namespace_ctxt)
               (decls: list lrergo_declaration)
      : eresult (list ergo_declaration * namespace_ctxt) :=
      elift (fun xy => (concat (fst xy), snd xy))
            (elift_context_fold_left
               resolve_ergo_declaration
               decls
               ctxt).

    Definition silently_resolve_ergo_declarations
               (ctxt:namespace_ctxt)
               (decls: list lrergo_declaration)
      : eresult namespace_ctxt :=
      elift snd (resolve_ergo_declarations ctxt decls).

  End NameResolution.

  Section Top.
    Definition init_namespace_ctxt : namespace_ctxt :=
      empty_namespace_ctxt no_namespace.

    Definition patch_cto_imports
               (ctxt_ns:namespace_name)
               (decls: list lrergo_declaration) : list lrergo_declaration :=
      if is_builtin_import ctxt_ns
      then (DImport dummy_provenance (ImportSelf dummy_provenance ctxt_ns)) :: decls
      else
        (DImport dummy_provenance (ImportAll dummy_provenance accordproject_base_namespace))
          :: (DImport dummy_provenance (ImportSelf dummy_provenance ctxt_ns))
          :: decls.

    Definition patch_ergo_imports
               (ctxt_ns:namespace_name)
               (decls: list lrergo_declaration) : list lrergo_declaration :=
      if is_builtin_import ctxt_ns
      then app decls (DImport dummy_provenance (ImportSelf dummy_provenance ctxt_ns) :: nil)
      else
        (DImport dummy_provenance (ImportAll dummy_provenance accordproject_base_namespace))
          ::(DImport dummy_provenance (ImportAll dummy_provenance accordproject_stdlib_namespace))
          ::(DImport dummy_provenance (ImportSelf dummy_provenance ctxt_ns))
          :: decls.
      
    Definition new_cto_package_namespace
               (ctxt:namespace_ctxt)
               (ns:namespace_name)
               (m:lrergo_module)
      : eresult namespace_ctxt :=
      if is_builtin_import ns
      then esuccess ctxt nil
      else
        let builtin_cto_imports :=
            (DImport dummy_provenance (ImportAll dummy_provenance accordproject_base_namespace))
              :: (DImport dummy_provenance (ImportSelf dummy_provenance ns))
              :: nil
        in
        let ctxt := new_namespace_scope ctxt ns in
        let ctxt := namespace_ctxt_of_ergo_module ctxt m in
        silently_resolve_ergo_declarations ctxt builtin_cto_imports.

    Definition new_ergo_module_namespace
               (ctxt:namespace_ctxt)
               (ns:namespace_name)
      : eresult namespace_ctxt :=
      if is_builtin_import ns
      then esuccess ctxt nil
      else
        let builtin_cto_imports :=
            (DImport dummy_provenance (ImportAll dummy_provenance accordproject_base_namespace))
              ::(DImport dummy_provenance (ImportAll dummy_provenance accordproject_stdlib_namespace))
              ::(DImport dummy_provenance (ImportSelf dummy_provenance ns))
              :: nil
        in
        let ctxt := new_namespace_scope ctxt ns in
        silently_resolve_ergo_declarations ctxt builtin_cto_imports.

    Definition resolve_cto_package
               (ctxt:namespace_ctxt)
               (cto:lrcto_package) : eresult (laergo_module * namespace_ctxt) :=
      let m := cto_package_to_ergo_module cto in
      let module_ns := m.(module_namespace) in
      let ctxt := new_namespace_scope ctxt module_ns in
      let ctxt := namespace_ctxt_of_ergo_module ctxt m in
      let declarations := m.(module_declarations) in
      let ctxt_ns := ctxt.(namespace_ctxt_namespace) in
      elift
        (fun nc =>
           (mkModule
              m.(module_annot)
              m.(module_file)
              m.(module_prefix)
              module_ns
              (fst nc), snd nc))
        (resolve_ergo_declarations
           ctxt
           (patch_cto_imports module_ns declarations)).

    Definition resolve_ergo_module
               (ctxt:namespace_ctxt)
               (m:lrergo_module) : eresult (laergo_module * namespace_ctxt) :=
      let module_ns := m.(module_namespace) in
      let ctxt := new_namespace_scope ctxt module_ns in
      let declarations := m.(module_declarations) in
      let ctxt_ns := ctxt.(namespace_ctxt_namespace) in
      elift
        (fun nc =>
           (mkModule
              m.(module_annot)
              m.(module_file)
              m.(module_prefix)
              module_ns
              (fst nc), snd nc))
        (resolve_ergo_declarations
           ctxt
           (patch_ergo_imports module_ns declarations)).

    Definition resolve_ergo_template
               (ctxt:namespace_ctxt)
               (ftemplate:option (string * lrergo_expr)) : eresult (option (string * laergo_expr)) :=
      match ftemplate with
      | None => esuccess None nil
      | Some t =>
        let (fname, template) := t in
        elift
          (fun x =>
             Some (fname, x))
          (resolve_ergo_template_expr ctxt template)
      end.

    Definition resolve_ergo_modules
               (ctxt:namespace_ctxt)
               (ml:list lrergo_module) : eresult (list laergo_module * namespace_ctxt) :=
      elift_context_fold_left
        resolve_ergo_module
        ml
        ctxt.

    Definition resolve_cto_packages
               (ctxt:namespace_ctxt)
               (ctos:list lrcto_package) : eresult (list laergo_module * namespace_ctxt) :=
      let ctxt := namespace_ctxt_of_cto_packages ctxt ctos in
      elift_context_fold_left
        resolve_cto_package
        ctos
        ctxt.

    Fixpoint triage_ctos_and_ergos (inputs:list lrergo_input)
      : (list lrcto_package * list lrergo_module * option lrergo_module) :=
      match inputs with
      | nil => (nil, nil, None)
      | InputCTO cto :: rest =>
        let '(ctos', rest', p') := triage_ctos_and_ergos rest in
        (cto :: ctos', rest', p')
      | InputErgo ml :: rest =>
        let '(ctos', rest', p') := triage_ctos_and_ergos rest in
        match p' with
        | None =>
          if is_stdlib_import ml.(module_namespace)
          then (ctos', ml :: rest', None)
          else (ctos', rest', Some ml)
        | Some _ => (ctos', ml :: rest', p')
        end
      end.

  End Top.

  Section Examples.
    Local Open Scope string.
    Definition ergo_typed1 : lrergo_type_declaration :=
      mkErgoTypeDeclaration
        dummy_provenance
        "c1"
        (ErgoTypeConcept
           false
           None
           (("a", ErgoTypeBoolean dummy_provenance)
              ::("b", (ErgoTypeClassRef dummy_provenance (None, "c3")))::nil)).

    Definition ergo_typed2 : lrergo_type_declaration :=
      mkErgoTypeDeclaration
        dummy_provenance
        "c2"
        (ErgoTypeConcept
           false
           None
           (("c", ErgoTypeBoolean dummy_provenance)
              ::("d", (ErgoTypeClassRef dummy_provenance (None, "c1")))::nil)).

    Definition ergo_funcd1 : lrergo_function :=
      mkFunc
        dummy_provenance
        (mkErgoTypeSignature
           dummy_provenance
           nil
           (Some (ErgoTypeBoolean dummy_provenance))
           None)
        None.
    
    Definition ergo_funcd2 : lrergo_function :=
      mkFunc
        dummy_provenance
        (mkErgoTypeSignature
           dummy_provenance
           nil
           (Some (ErgoTypeBoolean dummy_provenance))
           None)
        (Some (ECallFun dummy_provenance (None,"addFee") nil)).

    Definition ergo_clause2 : lrergo_clause :=
      mkClause
        dummy_provenance
        "addFee2"
        (mkErgoTypeSignature
           dummy_provenance
           nil
           (Some (ErgoTypeBoolean dummy_provenance))
           None)
        (Some (SReturn dummy_provenance (ECallFun dummy_provenance (None,"addFee") nil))).

    Definition ergo_contractd1 : lrergo_contract :=
      mkContract
        dummy_provenance
        (ErgoTypeBoolean dummy_provenance)
        None
        (ergo_clause2::nil).
    
    Definition ergo_module1 : lrergo_module :=
      mkModule
        dummy_provenance
        ""
        ""
        "n1"
        (DImport dummy_provenance (ImportAll dummy_provenance "n2")
        ::DFunc dummy_provenance "addFee" ergo_funcd1
        ::DContract dummy_provenance "MyContract" ergo_contractd1
        ::DType dummy_provenance ergo_typed1
        ::DType dummy_provenance ergo_typed2::nil).
    
    Definition ergo_typed3 : lrergo_type_declaration :=
      mkErgoTypeDeclaration
        dummy_provenance
        "c3"
        (ErgoTypeConcept
           false
           None
           (("a", ErgoTypeBoolean dummy_provenance)
              ::("b", ErgoTypeString dummy_provenance)::nil)).

    Definition ergo_typed_top : lrergo_type_declaration :=
      mkErgoTypeDeclaration
        dummy_provenance
        "top"
        (ErgoTypeGlobal
           (ErgoTypeAny dummy_provenance)).

    Definition ergo_module2 : lrergo_module :=
      mkModule
        dummy_provenance "" "" "n2" (DType dummy_provenance ergo_typed3::nil).

    Definition ergo_hl : lrergo_module :=
      mkModule
        dummy_provenance "" "" accordproject_base_namespace (DType dummy_provenance ergo_typed_top::nil).

    Definition ergo_stdlib : lrergo_module :=
      mkModule
        dummy_provenance "" "" accordproject_stdlib_namespace (DType dummy_provenance ergo_typed_top::nil).

    Definition ml1 : list lrergo_module := ergo_hl :: ergo_stdlib :: ergo_module2 :: ergo_module1 :: nil.
    Definition aml1 := resolve_ergo_modules (empty_namespace_ctxt "TEST") ml1.

    Definition ml2 : list lrergo_module := ergo_hl :: ergo_stdlib :: ergo_module2 :: nil.
    Definition aml2 := resolve_ergo_modules (empty_namespace_ctxt "TEST") ml2.

    Definition aml3 := elift (fun mc => resolve_ergo_module (snd mc) ergo_module1) aml2.
  End Examples.
  
End ErgoNameResolution.