Skip to content

Commit

Permalink
[asl] Always add types to local/global storage elements
Browse files Browse the repository at this point in the history
  • Loading branch information
Roman-Manevich committed Oct 23, 2024
1 parent f71fc7e commit 530f24b
Show file tree
Hide file tree
Showing 5 changed files with 35 additions and 20 deletions.
22 changes: 18 additions & 4 deletions asllib/Typing.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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 -> (
Expand All @@ -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) *)
Expand Down Expand Up @@ -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 *)
Expand Down Expand Up @@ -3135,4 +3148,5 @@ end
module TypeCheckDefault = Annotate (struct
let check = `TypeCheck
let output_format = Error.HumanReadable
let print_typed = false
end)
1 change: 1 addition & 0 deletions asllib/Typing.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions asllib/aslref.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
30 changes: 14 additions & 16 deletions asllib/doc/Statements.tex
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand All @@ -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)
}
Expand All @@ -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})
}
Expand All @@ -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)
}
Expand Down
1 change: 1 addition & 0 deletions herd/ASLSem.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 530f24b

Please sign in to comment.