Merge pull request #1011 from herd/asl-print-inferred-types

[asl] Add types to local/global storage elements when given --print-typed

asllib/Typing.ml

@@ -178,6 +178,7 @@ type strictness = [ `Silence | `Warn | `TypeCheck ]
 module type ANNOTATE_CONFIG = sig
   val check : strictness
   val output_format : Error.output_format
+  val print_typed : bool
 end
 
 module type S = sig
@@ -2392,7 +2393,15 @@ module Annotate (C : ANNOTATE_CONFIG) : S = struct
             let env1, ldi1 =
               annotate_local_decl_item loc env t_e ldk ~e:e' ldi
             in
-            let env2 =
+            let ldi1 =
+              if C.print_typed then
+                (* When [print_typed] is specified, wrap untyped items with their inferred type. *)
+                match ldi1 with
+                | LDI_Typed _ | LDI_Discard -> ldi1
+                | LDI_Var _ | LDI_Tuple _ -> LDI_Typed (ldi1, t_e)
+              else ldi1
+            in
+            let new_env =
               match ldk with
               | LDK_Let | LDK_Var -> env1
               | LDK_Constant -> (
@@ -2401,12 +2410,14 @@ module Annotate (C : ANNOTATE_CONFIG) : S = struct
                     declare_local_constant env1 v ldi1
                   with Error.(ASLException _) -> env1)
             in
-            (S_Decl (ldk, ldi1, Some e') |> here, env2) |: TypingRule.SDeclSome
+            (S_Decl (ldk, ldi1, Some e') |> here, new_env)
+            |: TypingRule.SDeclSome
         (* SDecl.Some) *)
         (* SDecl.None( *)
         | LDK_Var, None ->
-            let env', ldi' = annotate_local_decl_item_uninit loc env ldi in
-            (S_Decl (LDK_Var, ldi', None) |> here, env') |: TypingRule.SDeclNone
+            let new_env, ldi1 = annotate_local_decl_item_uninit loc env ldi in
+            (S_Decl (LDK_Var, ldi1, None) |> here, new_env)
+            |: TypingRule.SDeclNone
         | (LDK_Constant | LDK_Let), None ->
             fatal_from s UnrespectedParserInvariant)
     (* SDecl.None) *)
@@ -2995,6 +3006,8 @@ module Annotate (C : ANNOTATE_CONFIG) : S = struct
       (* UpdateGlobalStorage) *)
     in
     let () = assert (env2.local == empty_local) in
+    (* If C.print_typed is specified pass [declared_t] to make sure the storage element is type-annotated. *)
+    let ty_opt' = if C.print_typed then Some declared_t else ty_opt' in
     ({ gsd with ty = ty_opt'; initial_value = initial_value' }, env2.global)
     |: TypingRule.DeclareGlobalStorage
   (* End *)
@@ -3135,4 +3148,5 @@ end
 module TypeCheckDefault = Annotate (struct
   let check = `TypeCheck
   let output_format = Error.HumanReadable
+  let print_typed = false
 end)

asllib/Typing.mli

@@ -31,6 +31,7 @@ type strictness = [ `Silence | `Warn | `TypeCheck ]
 module type ANNOTATE_CONFIG = sig
   val check : strictness
   val output_format : Error.output_format
+  val print_typed : bool
 end
 
 module type S = sig

asllib/aslref.ml

@@ -208,6 +208,7 @@ let () =
     let module C = struct
       let output_format = args.output_format
       let check = args.strictness
+      let print_typed = args.print_typed
     end in
     let module T = Typing.Annotate (C) in
     or_exit @@ fun () -> T.type_check_ast ast

asllib/doc/Statements.tex

@@ -343,23 +343,21 @@ \subsubsection{Prose}
     \item annotating the right-hand-side expression $\ve$ in $\tenv$ yields $(\vte,\vep)$\ProseOrTypeError;
     \item annotating the local declaration item $\ldi$ with local declaration keyword $\ldk$, the type $\vte$,
           and the initializing expression $\vep$, in $\tenv$
-          yields $(\tenvone, \ldip)$;
+          yields $(\tenvone, \ldione)$;
     \item One of the following applies:
     \begin{itemize}
       \item All of the following apply (\textsc{constant}):
       \begin{itemize}
         \item $\ldk$ indicates a local constant declaration, that is, $\LDKConstant$;
         \item symbolically simplifying $\ve$ in $\tenvone$ yields the literal $\vv$\ProseOrTypeError;
-        \item declaring a local constant of type $\vte$, literal $\vv$ and identifier $\ldi$ in $\tenvone$ yields $(\newtenv, \ldip)$;
-        \item $\news$ is a declaration with $\ldk$, $\ldip$ and an expression $\vep$.
+        \item declaring a local constant of type $\vte$, literal $\vv$ and local declaration item $\ldione$ in $\tenvone$ yields $\newtenv$;
+        \item $\news$ is a declaration with $\ldk$, $\ldione$ and an expression $\vep$.
       \end{itemize}
 
       \item All of the following apply (\textsc{non\_constant}):
       \begin{itemize}
         \item $\ldk$ indicates that this is not a local constant declaration, that is, $\ldk\neq\LDKConstant$;
-        \item declaring the local identifiers $\ldi$ of type $\vte$ with local declaration keyword $\ldk$ in $\tenv$
-              yields $(\newtenv, \ldip)$;
-        \item $\news$ is a declaration with $\ldk$, $\ldip$ and an expression $\vep$;
+        \item $\news$ is a declaration with $\ldk$, $\ldione$ and an expression $\vep$;
         \item $\newtenv$ is $\tenvone$.
       \end{itemize}
     \end{itemize}
@@ -371,21 +369,21 @@ \subsubsection{Prose}
         that is, $\SDecl(\LDKVar, \ldi, \None)$ (local declarations of \texttt{let} variables and constants require
         an initializing expression, otherwise they are rejected by an ASL parser);
   \item annotating the uninitialised local declarations $\ldi$ in $\tenv$ yields \\
-        $(\newtenv, \ldip)$;
-  \item $\news$ is a local declaration statement with variable keyword, local identifiers $\ldip$, and no initial expression,
-        that is, $\SDecl(\LDKVar, \ldip, \None)$.
+        $(\newtenv, \ldione)$;
+  \item $\news$ is a local declaration statement with variable keyword, local identifiers $\ldione$, and no initial expression,
+        that is, $\SDecl(\LDKVar, \ldione, \None)$.
   \end{itemize}
 \end{itemize}
 \subsubsection{Formally}
 \begin{mathpar}
 \inferrule[constant]{
   \annotateexpr{\tenv, \ve} \typearrow (\vte, \vep) \OrTypeError\\\\
-  \annotatelocaldeclitem{\tenv, \vte, \ldk, \vep, \ldi} \typearrow (\tenvone, \ldip)\\\\
+  \annotatelocaldeclitem{\tenv, \vte, \ldk, \langle\vep\rangle, \ldi} \typearrow (\tenvone, \ldione)\\\\
   \commonprefixline\\\\
   \ldk = \LDKConstant\\
   \reduceconstants(\tenvone, \ve) \typearrow \vv \OrTypeError\\\\
-  \declarelocalconstant(\tenvone, \vv, \ldi) \typearrow \newtenv\\
-  \news \eqdef \SDecl(\LDKConstant, \ldip, \langle\vep\rangle)
+  \declarelocalconstant(\tenvone, \vv, \ldione) \typearrow \newtenv\\
+  \news \eqdef \SDecl(\LDKConstant, \ldione, \langle\vep\rangle)
 }{
   \annotatestmt(\tenv, \overname{\SDecl(\ldk, \ldi, \langle\ve\rangle)}{\vs}) \typearrow (\news, \newtenv)
 }
@@ -394,10 +392,10 @@ \subsubsection{Formally}
 \begin{mathpar}
 \inferrule[non\_constant]{
   \annotateexpr{\tenv, \ve} \typearrow (\vte, \vep) \OrTypeError\\\\
-  \annotatelocaldeclitem{\tenv, \vte, \ldk, \vep, \ldi} \typearrow (\tenvone, \ldip)\\\\
+  \annotatelocaldeclitem{\tenv, \vte, \ldk, \langle\vep\rangle, \ldi} \typearrow (\tenvone, \ldione)\\\\
   \commonprefixline\\\\
   \ldk \neq \LDKConstant\\
-  \news \eqdef \SDecl(\ldk, \ldip, \langle\vep\rangle)
+  \news \eqdef \SDecl(\ldk, \ldione, \langle\vep\rangle)
 }{
   \annotatestmt(\tenv, \overname{\SDecl(\ldk, \ldi, \langle\ve\rangle)}{\vs}) \typearrow (\news, \overname{\tenvone}{\newtenv})
 }
@@ -406,8 +404,8 @@ \subsubsection{Formally}
 
 \begin{mathpar}
 \inferrule[none]{
-  \annotatelocaldeclitemuninit(\tenv, \ldi) \typearrow (\newtenv, \ldip) \OrTypeError\\\\
-  \news \eqdef \SDecl(\LDKVar, \ldip, \None)
+  \annotatelocaldeclitemuninit(\tenv, \ldi) \typearrow (\newtenv, \ldione) \OrTypeError\\\\
+  \news \eqdef \SDecl(\LDKVar, \ldione, \None)
 }{
   \annotatestmt(\tenv, \overname{\SDecl(\LDKVar, \ldi, \None)}{\vs}) \typearrow (\news, \newtenv)
 }

herd/ASLSem.ml

@@ -110,6 +110,7 @@ module Make (C : Config) = struct
       else `Silence
 
     let output_format = Asllib.Error.Silence
+    let print_typed = false
   end)
 
   module ASLInterpreterConfig = struct