initial incompletely specified reduction relation for expressions

kth-step · Jan 16, 2024 · 4ded065 · 4ded065
1 parent 6632ab7
commit 4ded065
Show file tree

Hide file tree

Showing 5 changed files with 91 additions and 39 deletions.
diff --git 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
@@ -30,31 +30,30 @@
  $ \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}}{}{}{}{}}
 
 \newcommand{\ottF}{
 \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
@@ -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
@@ -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
@@ -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 ) .