(feature) Calculate extends relation between types; Expose subtyping,…

mechanization/Backend/Lib/ECType.v

@@ -33,53 +33,62 @@ Module ECType(ergomodel:ErgoBackendModel).
   Definition closed_kind : record_kind
     := RType.Closed.
 
-  Definition ectype_struct {m:brand_relation} : Set
+  Definition ectype_struct {br:brand_relation} : Set
     := RType.rtype₀.
-  Definition ectype {m:brand_relation} : Set
+  Definition ectype {br:brand_relation} : Set
     := RType.rtype.
-  Definition t {m:brand_relation} : Set
+  Definition t {br:brand_relation} : Set
     := ectype.
 
-  Definition sorted_pf_type {m:brand_relation} srl
+  Definition sorted_pf_type {br:brand_relation} srl
       := SortingAdd.is_list_sorted Bindings.ODT_lt_dec (@Assoc.domain String.string ectype srl) = true.
 
-  Definition tbottom {m:brand_relation} : ectype
+  Definition tbottom {br:brand_relation} : ectype
     := RType.Bottom.  
-  Definition ttop {m:brand_relation} : ectype
+  Definition ttop {br:brand_relation} : ectype
     := RType.Top.
-  Definition tunit {m:brand_relation} : ectype
+  Definition tunit {br:brand_relation} : ectype
     := RType.Unit.
-  Definition tfloat {m:brand_relation} : ectype
+  Definition tfloat {br:brand_relation} : ectype
     := RType.Float.
-  Definition tnat {m:brand_relation} : ectype
+  Definition tnat {br:brand_relation} : ectype
     := RType.Nat.
-  Definition tbool {m:brand_relation} : ectype
+  Definition tbool {br:brand_relation} : ectype
     := RType.Bool.
-  Definition tstring {m:brand_relation} : ectype
+  Definition tstring {br:brand_relation} : ectype
     := RType.String.
-  Definition tcoll {m:brand_relation} : ectype -> ectype
+  Definition tcoll {br:brand_relation} : ectype -> ectype
     := RType.Coll.
-  Definition trec {m:brand_relation} : record_kind -> forall (r:list (String.string*ectype)), sorted_pf_type r -> ectype
+  Definition trec {br:brand_relation} : record_kind -> forall (r:list (String.string*ectype)), sorted_pf_type r -> ectype
     := RType.Rec.
-  Definition teither {m:brand_relation} : ectype -> ectype -> ectype
+  Definition teither {br:brand_relation} : ectype -> ectype -> ectype
     := RType.Either.
-  Definition tarrow {m:brand_relation} : ectype -> ectype -> ectype
+  Definition tarrow {br:brand_relation} : ectype -> ectype -> ectype
     := RType.Arrow.
-  Definition tbrand {m:brand_relation} : list String.string -> ectype 
+  Definition tbrand {br:brand_relation} : list String.string -> ectype 
     := RType.Brand.
 
-  Definition toption {m:brand_relation} : ectype -> ectype
+  Definition toption {br:brand_relation} : ectype -> ectype
     := RType.Option.
 
-  (* Additional support for brand models extraction -- will have to be tested/consolidated *)
+  (* Support for type checking *)
+  Definition tmeet {br:brand_relation} : ectype -> ectype -> ectype := rtype_meet.
+  Definition tjoin {br:brand_relation} : ectype -> ectype -> ectype := rtype_meet.
 
-  Definition brand_context_type {m:brand_relation} : Set := (String.string*ectype).
-
-  Definition brand_relation : Set := brand_relation.
-  Definition make_brand_relation := Schema.mk_brand_relation.
-  Definition brand_model : Set := brand_model.
-  Definition make_brand_model := Schema.make_brand_model_from_decls_fails.
-  Definition typing_runtime : Set := typing_runtime.
+  Definition tsubtype {br:brand_relation} : ectype -> ectype -> Prop := subtype.
+  Theorem tsubtype_dec {m:brand_model}  (t1 t2:ectype) :
+    {tsubtype t1 t2} + {~ tsubtype t1 t2}.
+  Proof.
+    apply subtype_dec.
+  Defined.
+
+  Definition untcoll {m:brand_model} : ectype -> option ectype := tuncoll.
+  Definition unteither {m:brand_model} : ectype -> option (ectype * ectype) := tuneither.
+  Definition untrec {m:brand_model} : ectype -> option (record_kind * (list (string * ectype))) := tunrec.
+
+  Definition tinfer_data {m:brand_model} : data -> Datatypes.option ectype := infer_data_type.
+  Definition tinfer_binary_op {m:brand_model} : binary_op -> ectype -> ectype -> option (ectype * ectype * ectype) := infer_binary_op_type_sub.
+  Definition tinfer_unary_op {m:brand_model} : unary_op -> ectype -> option (ectype * ectype) := infer_unary_op_type_sub.
 
 End ECType.
 

mechanization/Common/Types/ErgoType.v

@@ -150,4 +150,37 @@ Section ErgoType.
       end
     end.
 
+  Section Extends.
+    Definition extends_rel
+               (to:absolute_name)
+               (e:@extends absolute_name) : list (absolute_name * absolute_name) :=
+      match e with
+      | None => (to,to) :: nil
+      | Some from => (to,from) :: (to,to) :: nil
+      end.
+
+    Definition type_declaration_desc_extend_rel
+               (to:absolute_name)
+               (decl_desc:laergo_type_declaration_desc) : list (absolute_name * absolute_name) :=
+      match decl_desc with
+      | ErgoTypeEnum _ => extends_rel to None
+      | ErgoTypeTransaction e _ => extends_rel to e
+      | ErgoTypeConcept e _ => extends_rel to e
+      | ErgoTypeEvent e _ => extends_rel to e
+      | ErgoTypeAsset e _ => extends_rel to e
+      | ErgoTypeParticipant e _ => extends_rel to e
+      | ErgoTypeGlobal _ => nil
+      | ErgoTypeFunction _ => nil
+      | ErgoTypeContract _ _ _ => extends_rel to None
+      end.
+
+    Definition type_declaration_extend_rel
+               (decl:laergo_type_declaration) : list (absolute_name * absolute_name) :=
+      type_declaration_desc_extend_rel decl.(type_declaration_name) decl.(type_declaration_type).
+
+    Definition type_declarations_extend_rel
+               (decls:list laergo_type_declaration) : list (absolute_name * absolute_name) :=
+      List.concat (List.map type_declaration_extend_rel decls).
+  End Extends.
+
 End ErgoType.

mechanization/Common/Utils/EUtil.v

@@ -48,4 +48,12 @@ Section EUtil.
       None
       l.
 
+  (*
+  Section TopoSort.
+    Context {A:Set}.
+    (* function from node to string -> graph edges -> visited nodes -> starting node -> ordered nodes *)
+    (* This assumes no two nodes have the same string *)
+    Parameter dfs : (A -> string) -> list (string * string) -> list A -> A -> list A.
+  End TopoSort.
+*)
 End EUtil.

mechanization/Compiler/ErgoDriver.v

@@ -171,7 +171,7 @@ Section ErgoDriver.
           repl_context_eval_ctxt : eval_context;
           repl_context_comp_ctxt : compilation_context
         }.
-    
+
     Definition init_repl_context
                (ctos : list lrcto_package)
                (mls : list lrergo_module) : eresult repl_context :=

mechanization/ErgoC/Lang/ErgoCType.v

@@ -27,25 +27,19 @@ Require Import Basics.
 Require Import ErgoSpec.Backend.ErgoBackend.
 Require Import ErgoSpec.Common.Utils.EUtil.
 Require Import ErgoSpec.Common.Utils.EResult.
+Require Import ErgoSpec.Common.Utils.EProvenance.
 Require Import ErgoSpec.Common.Pattern.EPattern.
 
 Require Import ErgoSpec.ErgoC.Lang.ErgoC.
 Require Import ErgoSpec.ErgoC.Lang.ErgoCTypeContext.
 
 Require Import ErgoSpec.Ergo.Lang.Ergo.
 
-
 Section ErgoCType.
+  Context {m : brand_model}.
 
-  (*
-  Definition ergo_unary_eval := ErgoOps.Unary.eval.
-  Definition ergo_binary_eval := ErgoOps.Binary.eval.
-*)
-
-  Context {br : brand_relation}.
   Import ErgoCTypes.
 
-  (*
   Fixpoint ergo_type_expr (ctxt : type_context) (expr : ergoc_expr) : eresult ergoc_type :=
     match expr with
     | EThisContract prov => efailure (SystemError prov "No `this' in ergoc")
@@ -55,21 +49,23 @@ Section ErgoCType.
       let opt := lookup String.string_dec (ctxt.(type_context_local_env)++ctxt.(type_context_global_env)) name in
       eresult_of_option opt (RuntimeError prov ("Variable not found: " ++ name)%string)
     | EConst prov d =>
-      eresult_of_option (infer_data_type d) (TypeError prov "Baaad constant.")
+      eresult_of_option
+        (infer_data_type d)
+        (TypeError prov "Bad constant.")
     | EArray prov es =>
       fold_left
-        (fun ls new =>
-           match ls with
-           | Success _ _ (ErgoCTypes.tcoll ls') =>
-             match ergo_type_expr ctxt new with
-             | Success _ _ new' => esuccess (tcoll (ls' ++ (new'::nil)))
-             | Failure _ _ f => efailure f
-             end
-           | Success _ _ _ => efailure (RuntimeError prov "This should never happen.")
-           | Failure _ _ f => efailure f
-           end)
+        (fun T new =>
+           eolift
+             (fun T' =>
+                elift
+                  (fun new' => tmeet T' new')
+                  (ergo_type_expr ctxt new))
+             T)
         es (esuccess (tcoll ttop))
-    | EUnaryOp prov o e => TODO
+    | _ => TODO dummy_provenance "No `this' in ergoc"
+    end.
+
+(*
     (*
       match ergo_type_expr ctxt e with
       | Success _ _ e' =>
@@ -245,6 +241,5 @@ Section ErgoCType.
       esuccess (dctxt, None)
     end.
 *)
-*)
-
-End ErgoCType.
+ *)
+End ErgoCType.