From 4ded065368b2f6dcc182b882a1b3bff84491e8c9 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Tue, 16 Jan 2024 21:01:42 +0100 Subject: [PATCH] initial incompletely specified reduction relation for expressions --- Makefile.coq.local | 3 +- docs/report/abs_defs.tex | 89 ++++++++++++++++++++++++++++++---------- docs/report/main.mng | 12 ++++-- src/abs.ott | 23 ++++++----- theories/abs_defs.v | 3 +- 5 files changed, 91 insertions(+), 39 deletions(-) diff --git a/Makefile.coq.local b/Makefile.coq.local index 1627316..7a83e83 100644 --- a/Makefile.coq.local +++ b/Makefile.coq.local @@ -20,6 +20,7 @@ docs/report/main.tex: docs/report/main.mng src/abs.ott docs/report/main.pdf: docs/report/abs_defs.tex docs/report/main.tex pdflatex -output-directory=docs/report docs/report/main.tex pdflatex -output-directory=docs/report docs/report/main.tex + pdflatex -output-directory=docs/report docs/report/main.tex coqdoc: $(GLOBFILES) $(VFILES) $(CSSFILES) $(JSFILES) $(HTMLFILES) $(SHOW)'COQDOC -d $(COQDOCDIR)' @@ -33,6 +34,6 @@ resources/index.html: resources/index.md pandoc -s -o $@ $< clean:: - $(HIDE)rm -f theories/abs_defs.v docs/abs_defs.tex \ + $(HIDE)rm -f docs/abs_defs.tex \ docs/report/main.tex docs/report/main.log docs/report/main.out \ docs/report/main.toc docs/report/main.pdf docs/report/main.aux diff --git a/docs/report/abs_defs.tex b/docs/report/abs_defs.tex index e143564..d8634c2 100644 --- a/docs/report/abs_defs.tex +++ b/docs/report/abs_defs.tex @@ -30,14 +30,12 @@ $ \ottmv{i} ,\, \ottmv{j} ,\, \ottmv{n} $ & \ottcom{index variables (subscripts)} \\ $ \ottmv{fn} $ & \ottcom{function name} \\ $ \ottmv{x} ,\, \ottmv{y} $ & \ottcom{variable} \\ + $ \ottmv{b} $ & \ottcom{boolean} \\ + $ \ottmv{z} $ & \ottcom{integer} \\ }} \newcommand{\ottT}{ \ottrulehead{\ottnt{T}}{::=}{\ottcom{ground type}}\ottprodnewline -\ottfirstprodline{|}{\ottnt{B}}{}{}{}{}} - -\newcommand{\ottB}{ -\ottrulehead{\ottnt{B}}{::=}{\ottcom{basic type}}\ottprodnewline \ottfirstprodline{|}{\mathsf{Bool}}{}{}{}{}\ottprodnewline \ottprodline{|}{\mathsf{Int}}{}{}{}{}} @@ -45,16 +43,17 @@ \ottrulehead{\ottnt{F}}{::=}{\ottcom{function definition}}\ottprodnewline \ottfirstprodline{|}{\ottkw{def} \, \ottnt{T} \, \ottmv{fn} \ottsym{(} \ottnt{T_{{\mathrm{1}}}} \, \ottmv{x_{{\mathrm{1}}}} \ottsym{,} \, ... \, \ottsym{,} \ottnt{T_{\ottmv{n}}} \, \ottmv{x_{\ottmv{n}}} \ottsym{)} \ottsym{=} \ottnt{e} \ottsym{;}}{}{}{}{}} -\newcommand{\ottb}{ -\ottrulehead{\ottnt{b}}{::=}{\ottcom{boolean}}\ottprodnewline -\ottfirstprodline{|}{\mathrm{True}} {\textsf{M}}{}{}{}\ottprodnewline -\ottprodline{|}{\mathrm{False}} {\textsf{M}}{}{}{}} +\newcommand{\ottt}{ +\ottrulehead{\ottnt{t}}{::=}{\ottcom{ground term}}\ottprodnewline +\ottfirstprodline{|}{\ottmv{b}}{}{}{}{\ottcom{boolean}}\ottprodnewline +\ottprodline{|}{\ottmv{z}}{}{}{}{\ottcom{integer}}} \newcommand{\otte}{ \ottrulehead{\ottnt{e}}{::=}{\ottcom{expression}}\ottprodnewline -\ottfirstprodline{|}{\ottnt{b}}{}{}{}{\ottcom{boolean expression}}\ottprodnewline +\ottfirstprodline{|}{\ottnt{t}}{}{}{}{\ottcom{term}}\ottprodnewline \ottprodline{|}{\ottmv{x}}{}{}{}{\ottcom{variable}}\ottprodnewline -\ottprodline{|}{\ottmv{fn} \ottsym{(} \ottnt{e_{{\mathrm{1}}}} \ottsym{,} \, ... \, \ottsym{,} \ottnt{e_{\ottmv{n}}} \ottsym{)}}{}{}{}{\ottcom{function call}}} +\ottprodline{|}{\ottmv{fn} \ottsym{(} \ottnt{e_{{\mathrm{1}}}} \ottsym{,} \, ... \, \ottsym{,} \ottnt{e_{\ottmv{n}}} \ottsym{)}}{}{}{}{\ottcom{function call}}\ottprodnewline +\ottprodline{|}{\ottnt{e} \ottsym{[} \ottmv{x_{{\mathrm{1}}}} \mapsto \ottmv{y_{{\mathrm{1}}}} \ottsym{,} \, ... \, \ottsym{,} \ottmv{x_{\ottmv{n}}} \mapsto \ottmv{y_{\ottmv{n}}} \ottsym{]}} {\textsf{M}}{}{}{}} \newcommand{\ottsig}{ \ottrulehead{\ottnt{sig}}{::=}{}\ottprodnewline @@ -69,14 +68,14 @@ \ottrulehead{\Gamma}{::=}{}\ottprodnewline \ottfirstprodline{|}{\Gamma \ottsym{[} \ottmv{x_{{\mathrm{1}}}} \mapsto \ottnt{T_{{\mathrm{1}}}} \ottsym{,} \, ... \, \ottsym{,} \ottmv{x_{\ottmv{n}}} \mapsto \ottnt{T_{\ottmv{n}}} \ottsym{]}} {\textsf{M}}{}{}{}} +\newcommand{\otts}{ +\ottrulehead{\sigma}{::=}{}\ottprodnewline +\ottfirstprodline{|}{\sigma \ottsym{[} \ottmv{x_{{\mathrm{1}}}} \mapsto \ottnt{t_{{\mathrm{1}}}} \ottsym{,} \, ... \, \ottsym{,} \ottmv{x_{\ottmv{n}}} \mapsto \ottnt{t_{\ottmv{n}}} \ottsym{]}} {\textsf{M}}{}{}{}} + \newcommand{\ottterminals}{ \ottrulehead{\ottnt{terminals}}{::=}{}\ottprodnewline -\ottfirstprodline{|}{ \{ }{}{}{}{}\ottprodnewline -\ottprodline{|}{ \} }{}{}{}{}\ottprodnewline -\ottprodline{|}{ \mathsf{Bool} }{}{}{}{}\ottprodnewline +\ottfirstprodline{|}{ \mathsf{Bool} }{}{}{}{}\ottprodnewline \ottprodline{|}{ \mathsf{Int} }{}{}{}{}\ottprodnewline -\ottprodline{|}{ \mathrm{True} }{}{}{}{}\ottprodnewline -\ottprodline{|}{ \mathrm{False} }{}{}{}{}\ottprodnewline \ottprodline{|}{ \leadsto }{}{}{}{}\ottprodnewline \ottprodline{|}{ \vdash }{}{}{}{}\ottprodnewline \ottprodline{|}{ \mapsto }{}{}{}{}\ottprodnewline @@ -87,45 +86,55 @@ \ottfirstprodline{|}{\ottnt{judgement}}{}{}{}{\ottcom{judgment}}\ottprodnewline \ottprodline{|}{\ottnt{formula_{{\mathrm{1}}}} \quad ... \quad \ottnt{formula_{\ottmv{n}}}}{}{}{}{\ottcom{conjunction of formulas}}\ottprodnewline \ottprodline{|}{\Gamma \ottsym{(} \ottmv{x} \ottsym{)} \ottsym{=} \ottnt{T}} {\textsf{M}}{}{}{}\ottprodnewline -\ottprodline{|}{\Gamma \ottsym{(} \ottmv{fn} \ottsym{)} \ottsym{=} \ottnt{sig}} {\textsf{M}}{}{}{}} +\ottprodline{|}{\sigma \ottsym{(} \ottmv{x} \ottsym{)} \ottsym{=} \ottnt{t}} {\textsf{M}}{}{}{}\ottprodnewline +\ottprodline{|}{\Gamma \ottsym{(} \ottmv{fn} \ottsym{)} \ottsym{=} \ottnt{sig}} {\textsf{M}}{}{}{}\ottprodnewline +\ottprodline{|}{\ottkw{fresh} \, \ottsym{(} \ottmv{x_{{\mathrm{1}}}} \ottsym{,} \, ... \, \ottsym{,} \ottmv{x_{\ottmv{n}}} \ottsym{,} \ottnt{e} \ottsym{)}} {\textsf{M}}{}{}{}} \newcommand{\ottfunctionalXXwellXXtyping}{ \ottrulehead{\ottnt{functional\_well\_typing}}{::=}{}\ottprodnewline \ottfirstprodline{|}{\Gamma \vdash \ottnt{e} \ottsym{:} \ottnt{T}}{}{}{}{\ottcom{well-typed expression}}\ottprodnewline \ottprodline{|}{\Gamma \vdash \ottnt{F}}{}{}{}{\ottcom{well-typed function declaration}}} +\newcommand{\ottfunctionalXXevaluation}{ +\ottrulehead{\ottnt{functional\_evaluation}}{::=}{}\ottprodnewline +\ottfirstprodline{|}{\ottnt{F_{{\mathrm{1}}}} \, ... \, \ottnt{F_{\ottmv{n}}} \ottsym{,} \sigma \vdash \ottnt{e} \leadsto \sigma' \vdash \ottnt{e'}}{}{}{}{\ottcom{expression evaluation}}} + \newcommand{\ottjudgement}{ \ottrulehead{\ottnt{judgement}}{::=}{}\ottprodnewline -\ottfirstprodline{|}{\ottnt{functional\_well\_typing}}{}{}{}{}} +\ottfirstprodline{|}{\ottnt{functional\_well\_typing}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottnt{functional\_evaluation}}{}{}{}{}} \newcommand{\ottuserXXsyntax}{ \ottrulehead{\ottnt{user\_syntax}}{::=}{}\ottprodnewline \ottfirstprodline{|}{\ottmv{i}}{}{}{}{}\ottprodnewline \ottprodline{|}{\ottmv{fn}}{}{}{}{}\ottprodnewline \ottprodline{|}{\ottmv{x}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottmv{b}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottmv{z}}{}{}{}{}\ottprodnewline \ottprodline{|}{\ottnt{T}}{}{}{}{}\ottprodnewline -\ottprodline{|}{\ottnt{B}}{}{}{}{}\ottprodnewline \ottprodline{|}{\ottnt{F}}{}{}{}{}\ottprodnewline -\ottprodline{|}{\ottnt{b}}{}{}{}{}\ottprodnewline +\ottprodline{|}{\ottnt{t}}{}{}{}{}\ottprodnewline \ottprodline{|}{\ottnt{e}}{}{}{}{}\ottprodnewline \ottprodline{|}{\ottnt{sig}}{}{}{}{}\ottprodnewline \ottprodline{|}{\ottnt{ctxv}}{}{}{}{}\ottprodnewline \ottprodline{|}{\Gamma}{}{}{}{}\ottprodnewline +\ottprodline{|}{\sigma}{}{}{}{}\ottprodnewline \ottprodline{|}{\ottnt{terminals}}{}{}{}{}\ottprodnewline \ottprodline{|}{\ottnt{formula}}{}{}{}{}} \newcommand{\ottgrammar}{\ottgrammartabular{ \ottT\ottinterrule -\ottB\ottinterrule \ottF\ottinterrule -\ottb\ottinterrule +\ottt\ottinterrule \otte\ottinterrule \ottsig\ottinterrule \ottctxv\ottinterrule \ottG\ottinterrule +\otts\ottinterrule \ottterminals\ottinterrule \ottformula\ottinterrule \ottfunctionalXXwellXXtyping\ottinterrule +\ottfunctionalXXevaluation\ottinterrule \ottjudgement\ottinterrule \ottuserXXsyntax\ottafterlastrule }} @@ -135,7 +144,7 @@ %% defn e \newcommand{\ottdruletXXbool}[1]{\ottdrule[#1]{% }{ -\Gamma \vdash \ottnt{b} \ottsym{:} \mathsf{Bool}}{% +\Gamma \vdash \ottmv{b} \ottsym{:} \mathsf{Bool}}{% {\ottdrulename{t\_bool}}{}% }} @@ -179,8 +188,44 @@ \newcommand{\ottdefnsfunctionalXXwellXXtyping}{ \ottdefntXXe{}\ottdefntXXF{}} +% defns functional_evaluation +%% defn e +\newcommand{\ottdruleredXXvar}[1]{\ottdrule[#1]{% +\ottpremise{\sigma \ottsym{(} \ottmv{x} \ottsym{)} \ottsym{=} \ottnt{t}}% +}{ +\ottnt{F_{{\mathrm{1}}}} \, ... \, \ottnt{F_{\ottmv{n}}} \ottsym{,} \sigma \vdash \ottmv{x} \leadsto \sigma \vdash \ottnt{t}}{% +{\ottdrulename{red\_var}}{}% +}} + + +\newcommand{\ottdruleredXXfunXXexp}[1]{\ottdrule[#1]{% +\ottpremise{\ottnt{F_{{\mathrm{1}}}} \, ... \, \ottnt{F_{\ottmv{n}}} \ottsym{,} \sigma \vdash \ottnt{e} \leadsto \sigma' \vdash \ottnt{e'}}% +}{ +\ottnt{F_{{\mathrm{1}}}} \, ... \, \ottnt{F_{\ottmv{n}}} \ottsym{,} \sigma \vdash \ottmv{fn} \ottsym{(} \ottnt{e_{{\mathrm{1}}}} \ottsym{,} \, ... \, \ottsym{,} \ottnt{e_{\ottmv{i}}} \ottsym{,} \ottnt{e} \ottsym{,} \ottnt{e'_{{\mathrm{1}}}} \ottsym{,} \, ... \, \ottsym{,} \ottnt{e'_{\ottmv{j}}} \ottsym{)} \leadsto \sigma' \vdash \ottmv{fn} \ottsym{(} \ottnt{e_{{\mathrm{1}}}} \ottsym{,} \, ... \, \ottsym{,} \ottnt{e_{\ottmv{i}}} \ottsym{,} \ottnt{e'} \ottsym{,} \ottnt{e'_{{\mathrm{1}}}} \ottsym{,} \, ... \, \ottsym{,} \ottnt{e'_{\ottmv{j}}} \ottsym{)}}{% +{\ottdrulename{red\_fun\_exp}}{}% +}} + + +\newcommand{\ottdruleredXXfunXXground}[1]{\ottdrule[#1]{% +\ottpremise{\ottkw{fresh} \, \ottsym{(} \ottmv{y_{{\mathrm{1}}}} \ottsym{,} \, ... \, \ottsym{,} \ottmv{y_{\ottmv{n}}} \ottsym{,} \ottnt{e} \ottsym{)}}% +}{ +\ottnt{F_{{\mathrm{1}}}} \, ... \, \ottnt{F_{\ottmv{i}}} \, \ottkw{def} \, \ottnt{T} \, \ottmv{fn} \ottsym{(} \ottnt{T_{{\mathrm{1}}}} \, \ottmv{x_{{\mathrm{1}}}} \ottsym{,} \, ... \, \ottsym{,} \ottnt{T_{\ottmv{n}}} \, \ottmv{x_{\ottmv{n}}} \ottsym{)} \ottsym{=} \ottnt{e} \ottsym{;} \, \ottnt{F'_{{\mathrm{1}}}} \, ... \, \ottnt{F'_{\ottmv{j}}} \ottsym{,} \sigma \vdash \ottmv{fn} \ottsym{(} \ottnt{t_{{\mathrm{1}}}} \ottsym{,} \, ... \, \ottsym{,} \ottnt{t_{\ottmv{n}}} \ottsym{)} \leadsto \sigma \ottsym{[} \ottmv{y_{{\mathrm{1}}}} \mapsto \ottnt{t_{{\mathrm{1}}}} \ottsym{,} \, ... \, \ottsym{,} \ottmv{y_{\ottmv{n}}} \mapsto \ottnt{t_{\ottmv{n}}} \ottsym{]} \vdash \ottnt{e} \ottsym{[} \ottmv{x_{{\mathrm{1}}}} \mapsto \ottmv{y_{{\mathrm{1}}}} \ottsym{,} \, ... \, \ottsym{,} \ottmv{x_{\ottmv{n}}} \mapsto \ottmv{y_{\ottmv{n}}} \ottsym{]}}{% +{\ottdrulename{red\_fun\_ground}}{}% +}} + +\newcommand{\ottdefnredXXe}[1]{\begin{ottdefnblock}[#1]{$\ottnt{F_{{\mathrm{1}}}} \, ... \, \ottnt{F_{\ottmv{n}}} \ottsym{,} \sigma \vdash \ottnt{e} \leadsto \sigma' \vdash \ottnt{e'}$}{\ottcom{expression evaluation}} +\ottusedrule{\ottdruleredXXvar{}} +\ottusedrule{\ottdruleredXXfunXXexp{}} +\ottusedrule{\ottdruleredXXfunXXground{}} +\end{ottdefnblock}} + + +\newcommand{\ottdefnsfunctionalXXevaluation}{ +\ottdefnredXXe{}} + \newcommand{\ottdefnss}{ \ottdefnsfunctionalXXwellXXtyping +\ottdefnsfunctionalXXevaluation } \newcommand{\ottall}{\ottmetavars\\[0pt] diff --git a/docs/report/main.mng b/docs/report/main.mng index 317370f..d435f27 100644 --- a/docs/report/main.mng +++ b/docs/report/main.mng @@ -41,6 +41,8 @@ We define ABS and describe its metatheory. \tableofcontents +\newpage + \section{Introduction} \label{sec:intro} Introduction goes here. @@ -52,10 +54,10 @@ In this section, we define the abstract syntax of ABS. \ottgrammartabular{\ottT\ottinterrule} -\ottgrammartabular{\ottB\ottinterrule} - \ottgrammartabular{\ottF\ottinterrule} +\ottgrammartabular{\ottt\ottinterrule} + \ottgrammartabular{\otte\ottinterrule} \section{Semantics} @@ -68,14 +70,16 @@ In this section, we define the semantics of ABS. \ottgrammartabular{\ottctxv\ottinterrule} -\ottgrammartabular{\ottG\ottinterrule} - \subsection{Typing} \ottdefntXXe{} \ottdefntXXF{} +\subsection{Reduction} + +\ottdefnredXXe{} + \section{Metatheory} \label{sec:metatheory} diff --git a/src/abs.ott b/src/abs.ott index 2fb1762..4aab52a 100644 --- a/src/abs.ott +++ b/src/abs.ott @@ -63,8 +63,8 @@ e :: e_ ::= {{ com variable }} | fn ( e1 , ... , en ) :: :: fn_call {{ com function call }} -% | e [ x1 |-> y1 , ... , xn |-> yn ] :: M :: xsubst -% {{ coq (xsubst_e [[e]] [[xsubst]]) }} + | e [ x1 |-> y1 , ... , xn |-> yn ] :: M :: subst_var + {{ coq ([[e]]) }} % FIXME sig :: sig_ ::= | T1 , ... , Tn -> T :: :: sig @@ -86,12 +86,12 @@ s {{ tex \sigma }} :: s_ ::= {{ coq (fold_right (fun (xt : x * t) (s5 : s) => Map.add (fst xt) (snd xt) s5) [[s]] [[x1 |-> t1 ... xn |-> tn]]) }} terminals :: terminals_ ::= - | Bool :: :: bool {{ tex \mathsf{Bool} }} - | Int :: :: int {{ tex \mathsf{Int} }} - | ~> :: :: trans {{ tex \leadsto }} - | |- :: :: turnstile {{ tex \vdash }} - | |-> :: :: mapsto {{ tex \mapsto }} - | -> :: :: arrow {{ tex \rightarrow }} + | Bool :: :: bool {{ tex \mathsf{Bool} }} + | Int :: :: int {{ tex \mathsf{Int} }} + | ~> :: :: trans {{ tex \leadsto }} + | |- :: :: turnstile {{ tex \vdash }} + | |-> :: :: mapsto {{ tex \mapsto }} + | -> :: :: arrow {{ tex \rightarrow }} formula :: formula_ ::= {{ com formulas }} @@ -105,6 +105,8 @@ formula :: formula_ ::= {{ coq (Map.find [[x]] [[s]] = Some ([[t]])) }} | G ( fn ) = sig :: M :: G_fn_eq_sig {{ coq (Map.find [[fn]] [[G]] = Some (ctxv_sig [[sig]])) }} + | fresh ( x1 , ... , xn , e ) :: M :: fresh + {{ coq True }} % FIXME defns functional_well_typing :: t_ ::= @@ -149,7 +151,6 @@ defn ------------------------------------------------------------------------------------------------------------- :: fun_exp F1 ... Fn , s |- fn ( e1 , ... , ei , e , e'1 , ... , e'j ) ~> s' |- fn ( e1 , ... , ei , e' , e'1 , ... , e'j ) - %fresh ( y1 , ... , yn , e ) + fresh ( y1 , ... , yn , e ) ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------- :: fun_ground - F1 ... Fi def T fn ( T1 x1 , ... , Tn xn ) = e ; F'1 ... F'j , s |- fn ( t1 , ... , tn ) ~> s [ y1 |-> t1 , ... , yn |-> tn ] |- e - %[ x1 |-> y1 , ... , xn |-> yn ] + F1 ... Fi def T fn ( T1 x1 , ... , Tn xn ) = e ; F'1 ... F'j , s |- fn ( t1 , ... , tn ) ~> s [ y1 |-> t1 , ... , yn |-> tn ] |- e [ x1 |-> y1 , ... , xn |-> yn ] diff --git a/theories/abs_defs.v b/theories/abs_defs.v index d387b34..770f73b 100644 --- a/theories/abs_defs.v +++ b/theories/abs_defs.v @@ -127,6 +127,7 @@ Inductive red_e : list F -> s -> e -> s -> e -> Prop := (* defn e *) red_e F_list s5 e_5 s' e' -> red_e F_list s5 (e_fn_call fn5 ((app e_list (app (cons e_5 nil) (app e'_list nil))))) s' (e_fn_call fn5 ((app e_list (app (cons e' nil) (app e'_list nil))))) | red_fun_ground : forall (T_x_t_y_list:list (T*x*t*x)) (F'_list F_list:list F) (T_5:T) (fn5:fn) (e5:e) (s5:s), - red_e ((app F_list (app (cons (F_fn T_5 fn5 (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (T_,x_) end ) T_x_t_y_list) e5) nil) (app F'_list nil)))) s5 (e_fn_call fn5 (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (e_t t_) end ) T_x_t_y_list)) (fold_right (fun (xt : x * t) (s5 : s) => Map.add (fst xt) (snd xt) s5) s5 (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (y_,t_) end ) T_x_t_y_list) ) e5. + True -> + red_e ((app F_list (app (cons (F_fn T_5 fn5 (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (T_,x_) end ) T_x_t_y_list) e5) nil) (app F'_list nil)))) s5 (e_fn_call fn5 (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (e_t t_) end ) T_x_t_y_list)) (fold_right (fun (xt : x * t) (s5 : s) => Map.add (fst xt) (snd xt) s5) s5 (map (fun (pat_:(T*x*t*x)) => match pat_ with (T_,x_,t_,y_) => (y_,t_) end ) T_x_t_y_list) ) ( e5 ) .