% (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:
