Module ErgoSpec.Common.Types.ErgoTypetoErgoCType

Require Import String.
Require Import List.

Require Import ErgoSpec.Backend.ErgoBackend.
Require Import ErgoSpec.Common.Utils.Misc.
Require Import ErgoSpec.Common.Utils.Names.
Require Import ErgoSpec.Common.Utils.Result.
Require Import ErgoSpec.Common.Utils.Provenance.
Require Import ErgoSpec.Common.Utils.Ast.
Require Import ErgoSpec.Common.Types.ErgoType.

Section ErgoTypetoErgoCType.
  Definition expand_hierarchy : Set := list string.
  Definition expanded_type : Set := list (string * laergo_type).
  Definition expand_ctxt : Set := list (string * (expand_hierarchy * expanded_type)).

  Section ErgoTypeExpansion.
    Definition ergo_expand_extends
               (ctxt:expand_ctxt)
               (this:absolute_name)
               (super:absolute_name)
               (localtype:list (string * laergo_type)) : expand_ctxt :=
      match lookup string_dec ctxt super with
      | None => ctxt
      | Some (hierarchy, etype) =>
        (this, (super::hierarchy,etype ++ localtype)) :: ctxt
      end.

    Definition ergo_decl_expand_extends (ctxt:expand_ctxt)
               (this:absolute_name)
               (decl_desc:laergo_type_declaration_desc) : expand_ctxt :=
      match decl_desc with
      | ErgoTypeEnum _ => ctxt
      | ErgoTypeTransaction _ None rtl =>
        if string_dec this "org.hyperledger.composer.system.Transaction"%string
        then (this, (nil, rtl)) :: ctxt
        else ergo_expand_extends ctxt this "org.hyperledger.composer.system.Transaction"%string rtl
      | ErgoTypeTransaction _ (Some super) rtl =>
        ergo_expand_extends ctxt this super rtl
      | ErgoTypeConcept _ None rtl =>
        (this, (nil, rtl)) :: ctxt
      | ErgoTypeConcept _ (Some super) rtl =>
        ergo_expand_extends ctxt this super rtl
      | ErgoTypeEvent _ None rtl =>
        if string_dec this "org.hyperledger.composer.system.Event"%string
        then (this, (nil, rtl)) :: ctxt
        else ergo_expand_extends ctxt this "org.hyperledger.composer.system.Event"%string rtl
      | ErgoTypeEvent _ (Some super) rtl =>
        ergo_expand_extends ctxt this super rtl
      | ErgoTypeAsset _ None rtl =>
        if string_dec this "org.hyperledger.composer.system.Asset"%string
        then (this, (nil, rtl)) :: ctxt
        else ergo_expand_extends ctxt this "org.hyperledger.composer.system.Asset"%string rtl
      | ErgoTypeAsset _ (Some super) rtl =>
        ergo_expand_extends ctxt this super rtl
      | ErgoTypeParticipant _ None rtl =>
        if string_dec this "org.hyperledger.composer.system.Participant"%string
        then (this, (nil, rtl)) :: ctxt
        else ergo_expand_extends ctxt this "org.hyperledger.composer.system.Participant"%string rtl
      | ErgoTypeParticipant _ (Some super) rtl =>
        ergo_expand_extends ctxt this super rtl
      | ErgoTypeGlobal _ => ctxt
      | ErgoTypeFunction _ => ctxt
      | ErgoTypeContract _ _ _ => ctxt
      end.

    Fixpoint ergo_expand_extends_in_declarations (decls:list laergo_type_declaration) : expand_ctxt :=
      List.fold_left
        (fun ctxt decl =>
           ergo_decl_expand_extends
             ctxt
             decl.(type_declaration_name)
                    decl.(type_declaration_type))
        decls nil.

    Definition ergo_hierarchy_from_expand (ctxt : expand_ctxt) :=
      List.concat
        (List.map (fun xyz =>
                     List.map (fun x => (fst xyz, x)) (fst (snd xyz)))
                  ctxt).

  End ErgoTypeExpansion.

  Section ErgoTypetoErgoCType.
    Context {m:brand_relation}.
    Import ErgoCTypes.
    Definition enums_ctxt : Set := list string.

    Fixpoint ergo_type_to_ergoc_type (t:laergo_type) : ergoc_type :=
      match t with
      | ErgoTypeAny _ => ttop
      | ErgoTypeNothing _ => tbottom
      | ErgoTypeUnit _ => tunit
      | ErgoTypeBoolean _ => tbool
      | ErgoTypeString _ => tstring
      | ErgoTypeDouble _ => tfloat
      | ErgoTypeLong _ => tfloat
      | ErgoTypeInteger _ => tnat
      | ErgoTypeDateTime _ => tdateTime
      | ErgoTypeClassRef _ cr => tbrand (cr::nil)
      | ErgoTypeOption _ t => teither (ergo_type_to_ergoc_type t) tunit
      | ErgoTypeRecord _ rtl =>
        trec
          open_kind
          (rec_sort (List.map (fun xy => (fst xy, ergo_type_to_ergoc_type (snd xy))) rtl))
          (rec_sort_sorted
             (List.map (fun xy => (fst xy, ergo_type_to_ergoc_type (snd xy))) rtl)
             (rec_sort (List.map (fun xy => (fst xy, ergo_type_to_ergoc_type (snd xy))) rtl))
             eq_refl)
      | ErgoTypeArray _ t => tcoll (ergo_type_to_ergoc_type t)
      | ErgoTypeSum _ t1 t2 => teither (ergo_type_to_ergoc_type t1) (ergo_type_to_ergoc_type t2)
      end.

    Definition ergo_ctype_decl_from_expand (ctxt : expand_ctxt) : tbrand_context_decls :=
      List.map (fun xyz =>
                  (fst xyz,
                   let rtl := snd (snd xyz) in
                   trec
                     open_kind
                     (rec_sort
                        (List.map (fun xy => (fst xy, ergo_type_to_ergoc_type (snd xy))) rtl))
                     (rec_sort_sorted
                        (List.map (fun xy => (fst xy, ergo_type_to_ergoc_type (snd xy))) rtl)
                        (rec_sort (List.map (fun xy => (fst xy, ergo_type_to_ergoc_type (snd xy))) rtl))
                        eq_refl))) ctxt.

  End ErgoTypetoErgoCType.

  Section Translate.
    Local Open Scope string.
    Import ErgoCTypes.

    Definition brand_relation_maybe hierarchy : eresult tbrand_relation
      := eresult_of_qresult dummy_provenance (mk_tbrand_relation hierarchy).


    Definition mk_model_type_decls
               {br:brand_relation}
               (ctxt : expand_ctxt) : tbrand_context_decls :=
      @ergo_ctype_decl_from_expand br ctxt.

    Definition label_of_decl (decl:laergo_type_declaration) : string :=
      decl.(type_declaration_name).
    Definition name_of_decl : laergo_type_declaration -> string := label_of_decl.
    Definition decls_table (decls:list laergo_type_declaration) : list (string * laergo_type_declaration) :=
      List.map (fun d => (d.(type_declaration_name), d)) decls.
    Definition edge_of_decl (dt:list (string * laergo_type_declaration)) (decl:laergo_type_declaration) : laergo_type_declaration * list laergo_type_declaration :=
      let outedges := type_declaration_extend_rel decl in
      (decl, List.concat (List.map (fun xy => match lookup string_dec dt (snd xy) with | None => nil | Some x => x :: nil end) outedges)).
    Definition graph_of_decls (decls:list laergo_type_declaration)
      : list (laergo_type_declaration * list (laergo_type_declaration)) :=
      let dt := decls_table decls in
      map (edge_of_decl dt) decls.
    
    Definition sort_decls (decls:list laergo_type_declaration) : list laergo_type_declaration :=
      coq_toposort label_of_decl name_of_decl (graph_of_decls decls).

    Definition brand_model_of_declarations
               (decls:list laergo_type_declaration)
      : eresult ErgoCTypes.tbrand_model :=
      let decls := sort_decls decls in
      let ctxt := ergo_expand_extends_in_declarations decls in
      let hierarchy := ergo_hierarchy_from_expand ctxt in
      eolift (fun br =>
                eresult_of_qresult dummy_provenance
                                   (mk_tbrand_model (@mk_model_type_decls br ctxt)))
             (brand_relation_maybe hierarchy).

    Definition force_brand_model_of_declarations
               (decls:list laergo_type_declaration)
      : ErgoCTypes.tbrand_model :=
      match brand_model_of_declarations decls with
      | Success _ _ s => s
      | Failure _ _ e => tempty_brand_model
      end.

  End Translate.

End ErgoTypetoErgoCType.