(fix) Namespace resolution for qualified names accordproject#365

Signed-off-by: Jerome Simeon <[email protected]>

examples/promissory-note/money.ergo

@@ -14,7 +14,8 @@
 
 namespace org.accordproject.ergo.money
 
+define constant days_in_year = 365.0
 define function compoundInterestMultiple(annualInterest : Double, numberOfDays : Double) : Double {
-    return (1.0 + annualInterest) ^ (numberOfDays / 365.0)
+    return (1.0 + annualInterest) ^ (numberOfDays / days_in_year)
 }
 

mechanization/Common/Utils/Names.v

@@ -54,6 +54,7 @@ Section Names.
   Section TypeNames.
     Definition hyperledger_namespace : string := "org.hyperledger.composer.system"%string.
     Definition stdlib_namespace : string := "org.accordproject.ergo.stdlib"%string.
+    Definition ergotop_namespace : string := "org.accordproject.ergo.top"%string.
 
     Definition default_request_absolute_name : string := "org.accordproject.cicero.runtime.Request".
     Definition default_response_absolute_name : string := "org.accordproject.cicero.runtime.Response".

mechanization/Common/Utils/NamespaceContext.v

@@ -77,27 +77,6 @@ Section NamespaceContext.
       | Some an => esuccess an
       end.
 
-    Definition resolve_type_name (prov:provenance) (tbl:namespace_table) (rn:relative_name) :=
-      match fst rn with
-      | None => lookup_type_name prov tbl (snd rn)
-      | Some ns => esuccess (absolute_name_of_local_name ns (snd rn))
-      end.
-    Definition resolve_constant_name (prov:provenance) (tbl:namespace_table) (rn:relative_name) :=
-      match fst rn with
-      | None => lookup_constant_name prov tbl (snd rn)
-      | Some ns => esuccess (absolute_name_of_local_name ns (snd rn))
-      end.
-    Definition resolve_function_name (prov:provenance) (tbl:namespace_table) (rn:relative_name) :=
-      match fst rn with
-      | None => lookup_function_name prov tbl (snd rn)
-      | Some ns => esuccess (absolute_name_of_local_name ns (snd rn))
-      end.
-    Definition resolve_contract_name (prov:provenance) (tbl:namespace_table) (rn:relative_name) :=
-      match fst rn with
-      | None => lookup_contract_name prov tbl (snd rn)
-      | Some ns => esuccess (absolute_name_of_local_name ns (snd rn))
-      end.
-
     Definition add_type_to_namespace_table (ln:local_name) (an:absolute_name) (tbl:namespace_table) :=
       mkNamespaceTable
         ((ln,an)::tbl.(namespace_table_types))
@@ -292,5 +271,53 @@ Section NamespaceContext.
       prev_enums
       prev_abstract.
 
+  Definition verify_name
+             (f_lookup: provenance -> namespace_table -> local_name -> eresult absolute_name)
+             (prov:provenance)
+             (ctxt:namespace_ctxt)
+             (ns:namespace_name)
+             (ln:local_name) : eresult absolute_name :=
+    let current_ns := ctxt.(namespace_ctxt_namespace) in
+    let current_tbl : namespace_table := ctxt.(namespace_ctxt_current_in_scope) in
+    let all_modules := (current_ns, current_tbl) :: ctxt.(namespace_ctxt_modules) in
+    match lookup string_dec all_modules ns with
+    | None => namespace_not_found_error prov ns
+    | Some tbl => f_lookup prov tbl ln
+    end.
+
+  Definition verify_type_name (prov:provenance) (ctxt:namespace_ctxt) (ns:namespace_name) (ln:local_name) :=
+    verify_name lookup_type_name prov ctxt ns ln.
+  Definition verify_constant_name (prov:provenance) (ctxt:namespace_ctxt) (ns:namespace_name) (ln:local_name) :=
+    verify_name lookup_constant_name prov ctxt ns ln.
+  Definition verify_function_name (prov:provenance) (ctxt:namespace_ctxt) (ns:namespace_name) (ln:local_name) :=
+    verify_name lookup_function_name prov ctxt ns ln.
+  Definition verify_contract_name (prov:provenance) (ctxt:namespace_ctxt) (ns:namespace_name) (ln:local_name) :=
+    verify_name lookup_contract_name prov ctxt ns ln.
+
+  Definition resolve_type_name (prov:provenance) (ctxt:namespace_ctxt) (rn:relative_name) :=
+    let tbl : namespace_table := ctxt.(namespace_ctxt_current_in_scope) in
+    match fst rn with
+    | None => lookup_type_name prov tbl (snd rn)
+    | Some ns => verify_type_name prov ctxt ns (snd rn)
+    end.
+  Definition resolve_constant_name (prov:provenance) (ctxt:namespace_ctxt) (rn:relative_name) :=
+    let tbl : namespace_table := ctxt.(namespace_ctxt_current_in_scope) in
+    match fst rn with
+    | None => lookup_constant_name prov tbl (snd rn)
+    | Some ns => verify_constant_name prov ctxt ns (snd rn)
+    end.
+  Definition resolve_function_name (prov:provenance) (ctxt:namespace_ctxt) (rn:relative_name) :=
+    let tbl : namespace_table := ctxt.(namespace_ctxt_current_in_scope) in
+    match fst rn with
+    | None => lookup_function_name prov tbl (snd rn)
+    | Some ns => verify_function_name prov ctxt ns (snd rn)
+    end.
+  Definition resolve_contract_name (prov:provenance) (ctxt:namespace_ctxt) (rn:relative_name) :=
+    let tbl : namespace_table := ctxt.(namespace_ctxt_current_in_scope) in
+    match fst rn with
+    | None => lookup_contract_name prov tbl (snd rn)
+    | Some ns => verify_contract_name prov ctxt ns (snd rn)
+    end.
+
 End NamespaceContext.
 

mechanization/Common/Utils/PrintTypedData.v

@@ -31,7 +31,7 @@ Section PrintTypedData.
     match get_local_part b with
     | None => "~" ++ b
     | Some local_name =>
-      match resolve_type_name dummy_provenance nsctxt.(namespace_ctxt_current_in_scope) (None,local_name) with
+      match resolve_type_name dummy_provenance nsctxt (None,local_name) with
       | Success _ _ resolved_b =>
         if string_dec resolved_b b
         then

mechanization/Common/Utils/Result.v

@@ -159,6 +159,8 @@ Section Result.
       efailure (ECompilationError prov ("Import not found: " ++ import)).
     Definition type_name_not_found_error {A} prov (ln:string) : eresult A :=
       efailure (ECompilationError prov ("Cannot find type with name '" ++ ln ++ "'")).
+    Definition namespace_not_found_error {A} prov (ns:string) : eresult A :=
+      efailure (ECompilationError prov ("Cannot find namespace '" ++ ns ++ "'")).
     Definition variable_name_not_found_error {A} prov (ln:string) : eresult A :=
       efailure (ECompilationError prov ("Cannot find variable with name '" ++ ln ++ "'")).
     Definition function_name_not_found_error {A} prov (ln:string) : eresult A :=

mechanization/Compiler/ErgoDriver.v

@@ -294,8 +294,7 @@ Section ErgoDriver.
     Definition init_repl_context
                (inputs : list lrergo_input) : eresult repl_context :=
       elift (mkREPLCtxt ErgoCEvalContext.empty_eval_context)
-            (eolift (set_namespace_in_compilation_context
-                       "org.accordproject.ergotop"%string)
+            (eolift (set_namespace_in_compilation_context ergotop_namespace)
                     (compilation_context_from_inputs_no_main inputs)).
 
     Definition update_repl_ctxt_comp_ctxt