[aslspec][asl reference] stronger subsumption test for functions and imported static_env_to_env to aslspec

Author: Roman-Manevich

asllib/aslspec/spec.ml

@@ -1237,20 +1237,21 @@ module Check = struct
                  (fun { term = sub_term; _ } { term = super_term; _ } ->
                    subsumed_rec spec expanded_types sub_term super_term)
                  sub_fields super_fields
-        | ( Function { from_type = _, sub_from_term; to_type = _, sub_to_term },
+        | ( Function
+              {
+                from_type = _, sub_from_term;
+                to_type = _, sub_to_term;
+                total = sub_total;
+              },
             Function
-              { from_type = _, super_from_term; to_type = _, super_to_term } )
-          ->
-            (* Functions can be partial or total, which require different subsumption tests.
-             To make this simple, we require equivalence of the from-terms and to-terms,
-             which is sufficient for our needs.
-          *)
-            let equivalence_test term term' =
-              subsumed_rec spec expanded_types term term'
-              && subsumed_rec spec expanded_types term' term
-            in
-            equivalence_test sub_from_term super_from_term
-            && equivalence_test sub_to_term super_to_term
+              {
+                from_type = _, super_from_term;
+                to_type = _, super_to_term;
+                total = super_total;
+              } ) ->
+            ((not sub_total) || super_total) (* sub_total implies super_total *)
+            && subsumed_rec spec expanded_types super_from_term sub_from_term
+            && subsumed_rec spec expanded_types sub_to_term super_to_term
         | ConstantsSet sub_names, ConstantsSet super_names ->
             List.for_all (fun name -> List.mem name super_names) sub_names
         | _ ->

asllib/doc/StaticEvaluation.tex

@@ -53,25 +53,4 @@ \chapter{Static Evaluation\label{chap:StaticEvaluation}}
 \{ \dynamicenvsG: \{\vHALFWORDSIZE \mapsto \nvint(32)\}, \dynamicenvsL: \emptyfunc \} \enspace.
 \]
 
-\ProseParagraph
-\AllApply
-\begin{itemize}
-  \item define the global dynamic environment $\vglobal$ as the map that binds
-        each $\id$ in the domain of $\tenv.\staticenvsG.\constantvalues$ to $\NVLiteral(\vl)$
-        if
-        $\tenv.\staticenvsG.\constantvalues(\id) = \vl$;
-  \item define the local dynamic environment $\vlocal$ as the empty map;
-  \item define the environment $\env$ to have the static component $\tenv$ and the dynamic
-        environment $\{\dynamicenvsG: \vglobal, \dynamicenvsL: \vlocal\}$;
-\end{itemize}
-\FormallyParagraph
-\begin{mathpar}
-\inferrule{
-  \vglobal \eqdef [\id \mapsto \NVLiteral(\vl) \;|\; \tenv.\staticenvsG.\constantvalues(\id) = \vl]\\
-  \vlocal \eqdef \emptyfunc
-}{
-  \staticenvtoenv(\tenv) \typearrow \overname{(\tenv, \{\dynamicenvsG: \vglobal, \dynamicenvsL: \vlocal\})}{\env}
-}
-\end{mathpar}
-% TODO: re-translate once empty_func has been introduced.
-% \RenderProseAndFormally{static_env_to_env}
+\RenderProseAndFormally{static_env_to_env}

asllib/doc/asl.spec

@@ -10266,8 +10266,18 @@ semantics function static_env_to_env(tenv: static_envs) ->
   \staticenvironmentterm{} {tenv} into an environment
   {env}.",
   prose_transition = "transforming the constants defined in {tenv} into an \environmentterm{} yields",
-};
-
+} =
+  constant_bindings := bindings(tenv.static_envs_G.constant_values);
+  constant_bindings =: list_combine(constant_ids, constant_literals);
+  constant_values := list_map(l, constant_literals, NV_Literal(l));
+  global_storage_bindings := list_combine(constant_ids, constant_values);
+  global_storage := bindings_to_map(global_storage_bindings);
+  empty_global := empty_denv.dynamic_envs_G;
+  new_global := empty_global(storage: global_storage);
+  new_denv := empty_denv(dynamic_envs_G: new_global);
+  --
+  (tenv, new_denv);
+;
 
 //////////////////////////////////////////////////
 // Relations for Subprogram Calls