|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2024type-inferences.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2024type-inferences.tex" :end))
% (defun C () (interactive) (find-LATEXsh "lualatex 2024type-inferences.tex" "Success!!!"))
% (defun D () (interactive) (find-pdf-page "~/LATEX/2024type-inferences.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2024type-inferences.pdf"))
% (defun e () (interactive) (find-LATEX "2024type-inferences.tex"))
% (defun o () (interactive) (find-LATEX "2024type-inferences.tex"))
% (defun u () (interactive) (find-latex-upload-links "2024type-inferences"))
% (defun v () (interactive) (find-2a '(e) '(d)))
% (defun d0 () (interactive) (find-ebuffer "2024type-inferences.pdf"))
% (defun cv () (interactive) (C) (ee-kill-this-buffer) (v) (g))
% (code-eec-LATEX "2024type-inferences")
% (find-pdf-page "~/LATEX/2024type-inferences.pdf")
% (find-sh0 "cp -v ~/LATEX/2024type-inferences.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2024type-inferences.pdf /tmp/pen/")
% (find-xournalpp "/tmp/2024type-inferences.pdf")
% file:///home/edrx/LATEX/2024type-inferences.pdf
% file:///tmp/2024type-inferences.pdf
% file:///tmp/pen/2024type-inferences.pdf
% http://anggtwu.net/LATEX/2024type-inferences.pdf
% (find-LATEX "2019.mk")
% (find-Deps1-links "Caepro5 Piecewise2 Maxima2 Verbatim3")
% (find-Deps1-cps "Caepro5 Piecewise2 Maxima2 Verbatim3")
% (find-Deps1-anggs "Caepro5 Piecewise2 Maxima2 Verbatim3")
% (find-MM-aula-links "2024type-inferences" "2" "2024tins" "tins")
% «.defs» (to "defs")
% «.defs-T-and-B» (to "defs-T-and-B")
% «.defs-caepro» (to "defs-caepro")
% «.defs-pict2e» (to "defs-pict2e")
% «.defs-Und2D2» (to "defs-Und2D2")
% «.title» (to "title")
% «.links» (to "links")
% «.instance-Monad-List» (to "instance-Monad-List")
% «.fun-proj-eq» (to "fun-proj-eq")
% «.p123456» (to "p123456")
% «.ST-S-app» (to "ST-S-app")
\documentclass[oneside,12pt]{article}
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
\usepackage{colorweb} % (find-es "tex" "colorweb")
%\usepackage{tikz}
%
% (find-dn6 "preamble6.lua" "preamble0")
%\usepackage{proof} % For derivation trees ("%:" lines)
%\input diagxy % For 2D diagrams ("%D" lines)
%\xyoption{curve} % For the ".curve=" feature in 2D diagrams
%
\usepackage{edrx21} % (find-LATEX "edrx21.sty")
\input edrxaccents.tex % (find-LATEX "edrxaccents.tex")
\input edrx21chars.tex % (find-LATEX "edrx21chars.tex")
\input edrxheadfoot.tex % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex % (find-LATEX "edrxgac2.tex")
%
% (find-es "tex" "geometry")
\usepackage[a6paper, landscape,
top=1.5cm, bottom=.25cm, left=1cm, right=1cm, includefoot
]{geometry}
%
\begin{document}
% «defs» (to ".defs")
% (find-LATEX "edrx21defs.tex" "colors")
% (find-LATEX "edrx21.sty")
\def\drafturl{http://anggtwu.net/LATEX/2024-1-C2.pdf}
\def\drafturl{http://anggtwu.net/2024.1-C2.html}
\def\draftfooter{\tiny \href{\drafturl}{\jobname{}} \ColorBrown{\shorttoday{} \hours}}
% (find-LATEX "2024-1-C2-carro.tex" "defs-caepro")
% (find-LATEX "2024-1-C2-carro.tex" "defs-pict2e")
\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua")
% «defs-T-and-B» (to ".defs-T-and-B")
\long\def\ColorDarkOrange#1{{\color{orange!90!black}#1}}
\def\T(Total: #1 pts){{\bf(Total: #1)}}
\def\T(Total: #1 pts){{\bf(Total: #1 pts)}}
\def\T(Total: #1 pts){\ColorRed{\bf(Total: #1 pts)}}
\def\B (#1 pts){\ColorDarkOrange{\bf(#1 pts)}}
% «defs-caepro» (to ".defs-caepro")
%L -- dofile "Caepro5.lua" -- (find-angg "LUA/Caepro5.lua" "LaTeX")
\def\Caurl #1{\expr{Caurl("#1")}}
\def\Cahref#1#2{\href{\Caurl{#1}}{#2}}
\def\Ca #1{\Cahref{#1}{#1}}
% «defs-pict2e» (to ".defs-pict2e")
%L -- dofile "Piecewise2.lua" -- (find-LATEX "Piecewise2.lua")
%L --dofile "Escadas1.lua" -- (find-LATEX "Escadas1.lua")
\def\pictgridstyle{\color{GrayPale}\linethickness{0.3pt}}
\def\pictaxesstyle{\linethickness{0.5pt}}
\def\pictnaxesstyle{\color{GrayPale}\linethickness{0.5pt}}
\celllower=2.5pt
% «defs-Und2D2» (to ".defs-Und2D2")
% (tinp 1 "defs-Und2D2")
% (tina "defs-Und2D2")
%L dofile "Und2D2.lua" -- (find-angg "LUA/Und2D2.lua")
\pu
%L dofile "Co1.lua" -- (find-angg "LUA/Co1.lua")
%L dofile "Verbatim3.lua" -- (find-angg "LUA/Verbatim3.lua")
\pu
\def\und#1#2{\underbrace{#1}_{#2}}
% _____ _ _ _
% |_ _(_) |_| | ___ _ __ __ _ __ _ ___
% | | | | __| |/ _ \ | '_ \ / _` |/ _` |/ _ \
% | | | | |_| | __/ | |_) | (_| | (_| | __/
% |_| |_|\__|_|\___| | .__/ \__,_|\__, |\___|
% |_| |___/
%
% «title» (to ".title")
% (2024tinsp 1 "title")
% (2024tinsa "title")
\thispagestyle{empty}
\begin{center}
\vspace*{1.2cm}
{\bf \Large
Some type inferences
and parsing diagrams
}
\bsk
%Some type inferences
%\bsk
Eduardo Ochs - RCN/PURO/UFF
\url{http://anggtwu.net/eev-lean4.html}
\end{center}
\newpage
% «links» (to ".links")
% (2024tinsp 2 "links")
% (2024tinsa "links")
% {\bf Links}
%
% \scalebox{0.6}{\def\colwidth{9cm}\firstcol{
% }\anothercol{
% }}
\newpage
% «instance-Monad-List» (to ".instance-Monad-List")
% (2024tinsp 2 "instance-Monad-List")
% (2024tinsa "instance-Monad-List")
% (find-es "lean" "instance-Monad-List")
%L bigstr = [=[
%L bind [a1,a2] fun a => bind [b1,b2] fun b => pure (a ,b )
%L -------- --- -------- --- --- ---
%L : List A : A : List B : B : A : B
%L ---------
%L : A×B
%L --------------
%L : List A×B
%L --------------------------
%L : B → List A×B
%L ----------------------------------------
%L : List A×B
%L ---------------------------------------------------
%L : A → List A×B
%L ----------------------------------------------------------------
%L : List A×B
%L ]=]
%L ut = GrUD.from(bigstr):addallbars():totex_textsf()
%L -- ut = GrUD.from(bigstr):addallbars():totex()
%L print(ut)
%L ut2 = format("\\sa{fig1}{%s}", ut)
%L output(ut2)
\pu
$$\scalebox{0.9}{$
\ga{fig1}
$}
$$
\newpage
% «fun-proj-eq» (to ".fun-proj-eq")
% (2024tinsp 3 "fun-proj-eq")
% (2024tinsa "fun-proj-eq")
% (find-angg "LEAN/parsediagram1.lean")
\def\Textsf#1{\mathstrut\textsf{#1}}
%L textsfco = Co.new("#$", " %&<>[\\]^_{}~"):add("\n", "\\\\\n")
%L textsfco = Co.new("#$", "%&<>[\\]^_{}~"):add("\n", "\\\\\n")
%L
%L GrUD.__index.textsfstr = function (grud,str)
%L --str = str:gsub("[%{%}_%^]", "\\%1")
%L str = textsfco:translate(str)
%L return format("\\Textsf{%s}", str)
%L --return format("\\textsf{%s}", str)
%L end
%L bigstr = [=[
%L fun {α β} [BEq α] (ab : α×β) => let (a,_) := ab; a==a
%L ----- -------------- ---------- -------------- ---- ---------------------
%L implicitBinder instBinder typeAscription "=>" let
%L -------------- ---------- -------------- ---------------------
%L funBinder funBinder funBinder termParser
%L ------------------------------------------ -------
%L (many1 funBinder) optType
%L ----- -----------------------------------------------------------------------------
%L "fun" basicFun
%L ------------------------------------------------------------------------------------
%L fun
%L ]=]
%L ut = GrUD.from(bigstr):addallbars():totex_textsf()
%L ut2 = format("\\sa{fig-fun}{%s}", ut)
%L output(ut2)
\pu
%L bigstr = [=[
%L { α β }
%L --- ----------- ----------- ---
%L "{" ident ident "}"
%L ----------- -----------
%L binderIdent binderIdent
%L ------------------------ ---------
%L (many1 binderIdent) (opttype)
%L ------------------------------------------
%L implicitBinder
%L ]=]
%L ut = GrUD.from(bigstr):addallbars():totex_textsf()
%L ut2 = format("\\sa{fig-implicitBinder}{%s}", ut)
%L output(ut2)
\pu
%L bigstr = [=[
%L [ BEq α ]
%L --- ----- ----- ---
%L "[" ident ident "]"
%L -----------
%L app
%L -------- -----------
%L optIdent termParser
%L ----------------------------
%L instBinder
%L ]=]
%L ut = GrUD.from(bigstr):addallbars():totex_textsf()
%L ut2 = format("\\sa{fig-instBinder}{%s}", ut)
%L output(ut2)
\pu
%L bigstr = [=[
%L ( ab : α × β )
%L --- ---------- --- ----- --- ----- ---
%L "(" ident ":" ident "×" ident ")"
%L ---------- ---------------
%L termParser term_×_
%L ---------------
%L termParser
%L --------------------------------------
%L typeAscription
%L ]=]
%L ut = GrUD.from(bigstr):addallbars():totex_textsf()
%L ut2 = format("\\sa{fig-typeAscription}{%s}", ut)
%L output(ut2)
\pu
%L bigstr = [=[
%L ( a , _ ) := ab
%L --- ---------- --- ---------- --- ------- ---- ----------
%L "(" ident "," "_" ")" optType ":=" ident
%L --- ---------- ---------- ----------
%L termParser hole termParser
%L ----------
%L termParser
%L ---------------------------------
%L tuple
%L ---------------------------------
%L termParser
%L -----------------------------------------------
%L letPatDecl
%L -----------------------------------------------------------
%L letDecl
%L ]=]
%L ut = GrUD.from(bigstr):addallbars():totex_textsf()
%L ut2 = format("\\sa{fig-letDecl}{%s}", ut)
%L output(ut2)
\pu
%L bigstr = [=[
%L let (a,_) := ab ; a == a
%L ----- ----------- ------------ ---------- ---- ----------
%L "let" letDecl ";" ident "==" ident
%L ------------ ---------- ----------
%L optSemicolon termParser termParser
%L --------------------------
%L term_==_
%L --------------------------
%L termParser
%L -----------------------------------------------------------
%L let
%L ]=]
%L ut = GrUD.from(bigstr):addallbars():totex_textsf()
%L ut2 = format("\\sa{fig-let}{%s}", ut)
%L output(ut2)
\pu
\vspace*{-0.4cm}
$$\scalebox{0.55}{$
\begin{array}{l}
\ga{fig-fun}
\\\\[7pt]
\ga{fig-implicitBinder}
\qquad
\ga{fig-instBinder}
\qquad
\ga{fig-typeAscription}
\\\\[7pt]
\ga{fig-letDecl}
\qquad
\ga{fig-let}
\end{array}
$}
$$
\newpage
% «p123456» (to ".p123456")
% (2024tinsp 4 "p123456")
% (2024tinsa "p123456")
% (find-luatreelean "Test1.lean")
%
% syntax num : catA
% syntax:50 catA:50 " - " catA:51 : catA
% syntax:70 catA:71 " ^ " catA:70 : catA
% syntax "[: " catA " :]" : term
%
% #eval paren [: 1 - 2 - 3 - 4 ^ 5 ^ 6 :] --> "(((1-2)-3)-(4^(5^6)))"
%L bigstr = [=[
%L 1 - 2 - 3 - 4 ^ 5 ^ 6
%L ------- ------- ------- ------- ------- -------
%L num num num num num num
%L ------- ------- ------- ------- ------- -------
%L catA catA catA catA catA catA
%L ------- ------- ------- ------- ------- -------
%L catA:50 catA:51 catA:51 catA:71 catA:71 catA:70
%L ----------------- -----------------
%L catA:50 catA:70
%L --------------------------- ---------------------------
%L catA:50 catA:70
%L ---------------------------
%L catA:51
%L ---------------------------------------------------------
%L catA:50
%L ]=]
%L ut = GrUD.from(bigstr):addallbars():totex_textsf()
%L ut2 = format("\\sa{fig-123456}{%s}", ut)
%L output(ut2)
\pu
\vspace*{-0.4cm}
$$\scalebox{1.0}{$
\begin{array}{l}
\ga{fig-123456}
\end{array}
$}
$$
\newpage
% (find-huttonbookpage 201 "Relabelling trees")
% (find-huttonbooktext 201 "Relabelling trees")
% «ST-S-app» (to ".ST-S-app")
% (2024tinsp 5 "ST-S-app")
% (2024tinsa "ST-S-app")
% (find-es "pandoc" "epub-to-html")
%L bigstr = [=[
%L app (S st ) x = st x
%L ------------------- ------- ------------------ -------
%L ::State->(a,State) ::State ::State->(a,State) ::State
%L --------------------- --------------------------
%L ::S(State->(a,State)) ::(a,State)
%L ---------------------
%L ::ST a
%L -----------------------------------
%L ::(a,State)
%L ]=]
%L ut = GrUD.from(bigstr):addallbars():totex_textsf()
%L ut2 = format("\\sa{fig-ST-S-app}{%s}", ut)
%L output(ut2)
\pu
%L bigstr = [=[
%L fmap g st = S (\s -> let (x ,s' ) = app st s in (g x , s' ))
%L ------ ------ ------- --- ------- ------ ------- ------ --- -------
%L ::a->b ::ST a ::State ::a ::State ::St a ::State ::a->b ::a ::State
%L ------------------ ------------- ------------------ ----------
%L ::ST b ::(a,State) ::(a,State) ::b
%L ---------------------
%L ::(b,State)
%L ---------------------------------------------------------------
%L ::(b,State)
%L --------------------------------------------------------------------------
%L ::State->(b,State)
%L ------------------------------------------------------------------------------
%L ::ST b
%L ]=]
%L ut = GrUD.from(bigstr):addallbars():totex_textsf()
%L ut2 = format("\\sa{fig-St-S-fmap}{%s}", ut)
%L output(ut2)
\pu
%V newtype ST a = S (State -> (a,State))
%V app :: ST a -> State -> (a,State)
%V app (S st) x = st x
%L
%L defvbt "ST-S"
\pu
%V newtype ST a = S (State -> (a,State))
%V app :: ST a -> State -> (a,State)
%V app (S st) x = st x
%V instance Functor ST where
%V -- fmap :: (a -> b) -> ST a -> ST b
%V fmap g st = S (\s -> let (x,s') = app st s in (g x, s'))
%L
%L defvbt "ST-S-fmap"
\pu
%V _________ __________
%V | | | |
%V | | x :: a | g :: | g x :: b
%V | | --------> | a -> b | ---------->
%V | st :: | | |
%V | ST a | |__________|
%V | |
%V | |
%V --------> | | --------------------------------->
%V s :: |_________| s' ::
%V State State
%L
%L defvbt "my-fig-00090"
\pu
\newpage
$$\scalebox{1.25}{$
\begin{array}{l}
\scalebox{1.1}{\vbt{ST-S}} \\
\\[-5pt]
\ga{fig-ST-S-app} \\
\end{array}
$}
$$
\newpage
% (find-fline "~/LATEX/2024type-inferences/" "00090.pdf")
% (find-pdf-page "~/LATEX/2024type-inferences/00090.pdf")
\vspace*{-0.5cm}
$$\scalebox{0.7}{$
\begin{array}{l}
\scalebox{1.1}{\vbt{ST-S-fmap}} \\
\\[-5pt]
\myvcenter{\includegraphics[width=5cm]{2024type-inferences/00090.pdf}}
\quad
\myvcenter{\scalebox{0.7}{\vbt{my-fig-00090}}} \\
\\[-5pt]
\ga{fig-St-S-fmap} \\
\end{array}
$}
$$
\GenericWarning{Success:}{Success!!!} % Used by `M-x cv'
\end{document}
% Local Variables:
% coding: utf-8-unix
% ee-tla: "tins"
% ee-tla: "2024tins"
% End: