%---|----1----|----2----|----3----|----4----|----5----|----6----|----7----|----8

%% natded package version 0.1
%% Copyright 2014 Mohammad M. Ajallooeian
%
% This work may be distributed and/or modified under the
% conditions of the LaTeX Project Public License, either version 1.3
% of this license or (at your option) any later version.
% The latest version of this license is in
%   http://www.latex-project.org/lppl.txt
% and version 1.3 or later is part of all distributions of LaTeX
% version 2005/12/01 or later.
%
% This work has the LPPL maintenance status `maintained'.
% 
% The Current Maintainer of this work is Mohammad M. Ajallooeian, m.ajallooeian@gmail.com.
%
% This work consists of the files natded.sty, natded.tex and extended_doc.tex
% and complied files natded.pdf and extended_doc.pdf.

\makeatletter

%%%%% LEVEL A

\usepackage{calc}

% lengths

\newlength{\negdepth@jaska}			% negative depth
\newlength{\posdepth@jaska}			% positive depth
\newlength{\lineheight@jaska}		% line height
\newlength{\hmargin@jaska}			% horizontal margin
\newlength{\vmargin@jaska}			% vertical margin
\newlength{\vextra@jaska}			% line extra height
\newlength{\cmargin@jaska}			% comments margin
\newlength{\borderwidth@jaska}		% border width
\newlength{\nowidth@jaska}			% no border width
\newlength{\hhrulebase@jaska}		% half of horizontal rule base length
\newlength{\stdepth@jaska}			% depth of strikethrough mark
\newlength{\stwidth@jaska}			% width of strikethrough mark
\newlength{\arrayrowheight@jaska}	% array environment row height
\newlength{\guardspace@jaska}		% length of guards
\newlength{\jguard@jaska}			% length of guards - Jáskowski style
\newlength{\kmguard@jaska}			% length of guards - Kalish and Montague style

\newlength{\templength@jaska}		% temporary length variable

% initialization

%%% independent
\setlength{\hmargin@jaska}		{ 10pt}
\setlength{\vmargin@jaska}		{  5pt}
\setlength{\vextra@jaska}		{  0pt}
\setlength{\cmargin@jaska}		{ 20pt}
\setlength{\borderwidth@jaska}	{  1pt}
\setlength{\nowidth@jaska}		{  0pt}


%%% dependent
\setlength{\hhrulebase@jaska}{\hmargin@jaska}		% 
\addtolength{\hhrulebase@jaska}{\borderwidth@jaska}

%%% boxes

\newsavebox\tempbox@jaska

% utilities

\newcommand\hcancel@jaska[2][0.5pt]{
	\ifmmode
		\sbox\tempbox@jaska{$#2$}
	\else
		\sbox\tempbox@jaska{#2}
	\fi
	\makebox[0pt][l]{\usebox\tempbox@jaska}
	\rule[0.5\ht\tempbox@jaska-#1/2]{\wd\tempbox@jaska}{#1}
}

\newcommand{\showmark@jaska}{
	\hcancel@jaska{Show}\;
}

% context dependent initializations

\sbox\tempbox@jaska{$\showmark@jaska$}
\setlength{\kmguard@jaska}{\wd\tempbox@jaska}
\setlength{\jguard@jaska}{\vmargin@jaska}

\setlength{\guardspace@jaska}{\jguard@jaska}

%low-level commands

\newcommand{\frml@jaska}[1]{
	\sbox\tempbox@jaska{$#1$, \the\ht\tempbox@jaska, \the\dp\tempbox@jaska}
	
	\setlength{\lineheight@jaska}{\ht\tempbox@jaska}
	\addtolength{\lineheight@jaska}{\dp\tempbox@jaska}
	\addtolength{\lineheight@jaska}{2\vmargin@jaska}	
	\addtolength{\lineheight@jaska}{\vextra@jaska}
	
	\begin{minipage}[c][\lineheight@jaska][c]{\wd\tempbox@jaska}
		$#1$
	\end{minipage}
}

\newcommand{\boxtop@jaska}[3][\,]{
	\makebox[\guardspace@jaska][r]{$#1$}
	
	\sbox\tempbox@jaska{$#2$}
	
	\setlength{\templength@jaska}{#3}
	\addtolength{\templength@jaska}{2\hhrulebase@jaska}
	
	\setlength{\negdepth@jaska}{-\dp\tempbox@jaska}

	\setlength{\lineheight@jaska}{\ht\tempbox@jaska}
	\addtolength{\lineheight@jaska}{\dp\tempbox@jaska}
	\addtolength{\lineheight@jaska}{\vextra@jaska}
	\addtolength{\lineheight@jaska}{-0.25\vmargin@jaska}
	
	
	\setlength{\posdepth@jaska}{\lineheight@jaska}
	\addtolength{\posdepth@jaska}{\negdepth@jaska}	

	\rule[\negdepth@jaska]{\borderwidth@jaska}{\lineheight@jaska}
	\hspace{-\borderwidth@jaska}
	\rule[\posdepth@jaska]{\templength@jaska}{\borderwidth@jaska}
	\hspace{-\borderwidth@jaska}
	\rule[\negdepth@jaska]{\borderwidth@jaska}{\lineheight@jaska}
	\setlength{\templength@jaska}{-#3}
	\addtolength{\templength@jaska}{-\hhrulebase@jaska}
	\hspace{\templength@jaska}
	\addtolength{\lineheight@jaska}{0.25\vmargin@jaska}
	\raisebox{0pt}[\lineheight@jaska][0pt]{$#2$}
	\hspace{\cmargin@jaska}
}

\newcommand{\boxmid@jaska}[3][\,]{
	\makebox[\guardspace@jaska][r]{$#1$}
	
	\sbox\tempbox@jaska{$#2$}
	
	\setlength{\negdepth@jaska}{-\dp\tempbox@jaska}
	
	\setlength{\lineheight@jaska}{\ht\tempbox@jaska}
	\addtolength{\lineheight@jaska}{\dp\tempbox@jaska}
	\addtolength{\lineheight@jaska}{\vextra@jaska}	

	\rule[\negdepth@jaska]{\borderwidth@jaska}{\lineheight@jaska}
	\hspace{\hmargin@jaska}
	\hspace{#3}
	\hspace{\hmargin@jaska}
	\rule[\negdepth@jaska]{\borderwidth@jaska}{\lineheight@jaska}
	\setlength{\templength@jaska}{-#3}
	\addtolength{\templength@jaska}{-\hhrulebase@jaska}
	\hspace{\templength@jaska}
	\makebox[#3][l]{$#2$}
	\hspace{\cmargin@jaska}
}

\newcommand{\boxbot@jaska}[3][\,]{
	\makebox[\guardspace@jaska][r]{$#1$}

	\sbox\tempbox@jaska{$#2$}
	
	\setlength{\negdepth@jaska}{-\dp\tempbox@jaska}
	\addtolength{\negdepth@jaska}{0.25\vmargin@jaska}
	
	\setlength{\lineheight@jaska}{\ht\tempbox@jaska}
	\addtolength{\lineheight@jaska}{\dp\tempbox@jaska}
	\addtolength{\lineheight@jaska}{\vextra@jaska}
	\addtolength{\lineheight@jaska}{-0.25\vmargin@jaska}
	
	\setlength{\templength@jaska}{#3}
	\addtolength{\templength@jaska}{2\hhrulebase@jaska}
	
	\rule[\negdepth@jaska]{\borderwidth@jaska}{\lineheight@jaska}
	\hspace{-\borderwidth@jaska}
	\rule[\negdepth@jaska]{\templength@jaska}{\borderwidth@jaska}
	\hspace{-\borderwidth@jaska}
	\rule[\negdepth@jaska]{\borderwidth@jaska}{\lineheight@jaska}
	\setlength{\templength@jaska}{-#3}
	\addtolength{\templength@jaska}{-\hhrulebase@jaska}
	\hspace{\templength@jaska}
	\addtolength{\lineheight@jaska}{0.0\vmargin@jaska}
	\raisebox{0pt}[0pt][\lineheight@jaska]{$#2$}
	\hspace{\cmargin@jaska}
}

\newcommand{\boxdbl@jaska}[3][\,]{
	\makebox[\guardspace@jaska][r]{$#1$}

	\sbox\tempbox@jaska{$#2$}
	
	\setlength{\negdepth@jaska}{-\dp\tempbox@jaska}
	\addtolength{\negdepth@jaska}{0.25\vmargin@jaska}
	
	\setlength{\lineheight@jaska}{\ht\tempbox@jaska}
	\addtolength{\lineheight@jaska}{\dp\tempbox@jaska}
	\addtolength{\lineheight@jaska}{\vextra@jaska}
	\addtolength{\lineheight@jaska}{-0.5\vmargin@jaska}
	
	\setlength{\posdepth@jaska}{\lineheight@jaska}
	\addtolength{\posdepth@jaska}{\negdepth@jaska}	
	
	\setlength{\templength@jaska}{#3}
	\addtolength{\templength@jaska}{2\hhrulebase@jaska}
	
	\rule[\negdepth@jaska]{\borderwidth@jaska}{\lineheight@jaska}
	\hspace{-\borderwidth@jaska}
	\rule[\negdepth@jaska]{\templength@jaska}{\borderwidth@jaska}
	\hspace{-\templength@jaska}
	\rule[\posdepth@jaska]{\templength@jaska}{\borderwidth@jaska}
	\hspace{-\borderwidth@jaska}	
	\rule[\negdepth@jaska]{\borderwidth@jaska}{\lineheight@jaska}
	\setlength{\templength@jaska}{-#3}
	\addtolength{\templength@jaska}{-\hhrulebase@jaska}
	\hspace{\templength@jaska}
	\addtolength{\lineheight@jaska}{0.0\vmargin@jaska}
	\raisebox{0pt}[0pt][\lineheight@jaska]{$#2$}
	\hspace{\cmargin@jaska}
}


\newcommand{\boxnot@jaska}[3][\,]{
	\hspace{-\guardspace@jaska}
	\hspace{-\hmargin@jaska}
	\hspace{-\borderwidth@jaska}
	\makebox[\guardspace@jaska][r]{$#1$}
	
	\sbox\tempbox@jaska{$#2$}
	
	\setlength{\negdepth@jaska}{-\dp\tempbox@jaska}
	
	\setlength{\lineheight@jaska}{\ht\tempbox@jaska}
	\addtolength{\lineheight@jaska}{\dp\tempbox@jaska}
	\addtolength{\lineheight@jaska}{\vextra@jaska}
	
	\setlength{\posdepth@jaska}{\lineheight@jaska}
	\addtolength{\posdepth@jaska}{\negdepth@jaska}	

	\rule[\negdepth@jaska]{0pt}{\lineheight@jaska}
	\hspace{\borderwidth@jaska}
	\hspace{\hmargin@jaska}
	\hspace{#3}
	\hspace{\hmargin@jaska}
	\rule[\negdepth@jaska]{0pt}{\lineheight@jaska}
	\hspace{\borderwidth@jaska}
	\setlength{\templength@jaska}{-#3}
	\addtolength{\templength@jaska}{-\hhrulebase@jaska}
	\hspace{\templength@jaska}
	\makebox[#3][l]{$#2$}
	\hspace{\cmargin@jaska}
}

\newcommand{\setstylej@jaska}{
	\setlength{\guardspace@jaska}{\jguard@jaska}
}

\newcommand{\setstylekm@jaska}{
	\setlength{\guardspace@jaska}{\kmguard@jaska}
}

%%%%% LEVEL B

\newcounter{depth@jaskb}
\newcounter{jdepth@jaskb}
\newcounter{linecount@jaskb}

\newlength{\templength@jaskb}
\newlength{\extrawin@jaskb}
\newlength{\extrawout@jaskb}

\setlength{\extrawin@jaskb}{2pt}
\setlength{\extrawout@jaskb}{\dimexpr\guardspace@jaska+\hmargin@jaska+25pt+\hmargin@jaska\relax}

\newsavebox\tempbox@jaskb

\def\makcl@jaskb#1#2{%
  \ifcsname	#1#2@jaskb\endcsname%
  \else%
    \ifnum#2>0\relax%
      \makcl@jaskb{#1}{\number\numexpr#2-1\relax}%
    \fi%
    \global\expandafter\newcount\csname #1#2@jaskb\endcsname%
  \fi%
}

\def\setcl@jaskb#1#2#3{%
  \global\expandafter\csname #1#2@jaskb\endcsname #3\relax%
}

\def\inccl@jaskb#1#2{%
  \global\expandafter\advance\csname #1#2@jaskb\endcsname by 1\relax%
}%

\def\stpcl@jaskb#1#2{%
  \ifnum#2>0\relax%
    \stpcl@jaskb{#1}{\number\numexpr#2-1\relax}%
  \fi%
  \inccl@jaskb{#1}{#2}%
}%

\def\getcl@jaskb#1#2{% 
  \the\expandafter\csname #1#2@jaskb\endcsname%
}%

\def\makdl@jaskb#1#2{%
  \ifcsname	#1#2@jaskb\endcsname%
  \else%
    \ifnum#2>0\relax%
      \makdl@jaskb{#1}{\number\numexpr#2-1\relax}%
    \fi%
    \global\expandafter\newdimen\csname #1#2@jaskb\endcsname%
  \fi%
}

\def\setdl@jaskb#1#2#3{%
  \global\expandafter\csname #1#2@jaskb\endcsname=\dimexpr#3\relax%
}

\def\adddl@jaskb#1#2#3{%
  \global\expandafter\advance\csname #1#2@jaskb\endcsname \dimexpr#3\relax%
}%

\def\getdl@jaskb#1#2{%
  \the\expandafter\csname #1#2@jaskb\endcsname%
}%

\def\upddl@jaskb#1#2#3{%
  \ifdim#3>\expandafter\csname #1#2@jaskb\endcsname\relax%
    \setdl@jaskb{#1}{#2}{#3}%
  \fi%
}%

\def\ruddl@jaskb#1#2#3#4{%
  \upddl@jaskb{#1}{#2}{#3}%
  \ifnum#2>0\relax%
    \ruddl@jaskb{#1}{\number\numexpr#2-1\relax}{\dimexpr#3+#4\relax}{#4}%
  \fi%
}%

\def\pshlsymb@jaskb#1#2#3{%
  \global\expandafter\def\csname #1#2@jaskb\endcsname{#3}%
}%

\def\poplsymb@jaskb#1#2{%
  \csname #1#2@jaskb\endcsname%
%  \texttt{G}#2
%  \pshlsymb@jaskb{#1}{#2}{}%
}%


\def\measurewidth@jaskb#1{%
	\inccl@jaskb{mlevel}{\thedepth@jaskb}
	\sbox\tempbox@jaskb{$#1$}%
	\makdl@jaskb{blockwidth}{\thedepth@jaskb}
	\ruddl@jaskb{blockwidth}{\thedepth@jaskb}{\dimexpr\wd\tempbox@jaskb+\extrawin@jaskb\relax}{\extrawout@jaskb}
}

\def\jmeasurewidth@jaskb#1{%
	\inccl@jaskb{mlevel}{\thedepth@jaskb}
	\sbox\tempbox@jaskb{$#1$}%
	\makdl@jaskb{blockwidth}{\thejdepth@jaskb}
	\ruddl@jaskb{blockwidth}{\thejdepth@jaskb}{\dimexpr\wd\tempbox@jaskb+\extrawin@jaskb\relax}{\extrawout@jaskb}
}

\def\setle@jaskb#1#2#3{%
	\global\expandafter\def\csname #1#2@jaskb\endcsname{#3}%	
}

\def\getle@jaskb#1#2{%
	\csname #1#2@jaskb\endcsname%
}

\def\genlevexpr@jaskb#1#2{%
	\ifnum\getcl@jaskb{plevel}{#1}=1\relax%
		\ifnum\getcl@jaskb{plevel}{#1}=\getcl@jaskb{mlevel}{#1}\relax%
			\setle@jaskb{levexpr}{#1}{\boxdbl@jaska[#2\poplsymb@jaskb{guardsym}{#1}]{\getle@jaskb{levexpr}{\number\numexpr#1+1\relax}}{\getdl@jaskb{blockwidth}{#1}}}%
		\else%
			\setle@jaskb{levexpr}{#1}{\boxtop@jaska[#2\poplsymb@jaskb{guardsym}{#1}]{\getle@jaskb{levexpr}{\number\numexpr#1+1\relax}}{\getdl@jaskb{blockwidth}{#1}}}%
		\fi%
	\else%
		\ifnum\getcl@jaskb{plevel}{#1}=\getcl@jaskb{mlevel}{#1}\relax%
			\setle@jaskb{levexpr}{#1}{\boxbot@jaska[#2]{\getle@jaskb{levexpr}{\number\numexpr#1+1\relax}}{\getdl@jaskb{blockwidth}{#1}}}%
		\else%
			\setle@jaskb{levexpr}{#1}{\boxmid@jaska[#2]{\getle@jaskb{levexpr}{\number\numexpr#1+1\relax}}{\getdl@jaskb{blockwidth}{#1}}}%
		\fi%
	\fi%
	\ifnum#1>1\relax%
		\genlevexpr@jaskb{\number\numexpr#1-1\relax}{}%
	\fi%
}

\def\statement@jaskb#1#2#3#4#5#6{%
	\stpcl@jaskb{plevel}{\thedepth@jaskb}%
	\ifnum#1>0\relax%
		\setle@jaskb{levexpr}{\number\numexpr#1+1\relax}{\frml@jaska{#5}}		\genlevexpr@jaskb{#1}{#4#2}%
		\setle@jaskb{levexpr}{0}{\getle@jaskb{levexpr}{1}}%
	\else%
		\setle@jaskb{levexpr}{0}{\boxnot@jaska[#4#2]{\frml@jaska{#5}}{\getdl@jaskb{blockwidth}{#1}}}%
 	\fi%
	%#3&...
	\stepcounter{linecount@jaskb}%
	\thelinecount@jaskb.&\getle@jaskb{levexpr}{0}&\mbox{#6}\\%
}

\def\cblockmeasure@jaskb#1{%
	\stepcounter{jdepth@jaskb}%
	\gdef\hypo@jaskb##1##2##3##4{\jmeasurewidth@jaskb{##3}}%
	\gdef\have@jaskb##1##2##3##4{\jmeasurewidth@jaskb{##3}}%
	\makdl@jaskb{blockwidth}{\thejdepth@jaskb}%
	\setdl@jaskb{blockwidth}{\thejdepth@jaskb}{\extrawin@jaskb}%
	#1%
	\gdef\hypo@jaskb##1##2##3##4{\measurewidth@jaskb{##3}}%
	\gdef\have@jaskb##1##2##3##4{\measurewidth@jaskb{##3}}%
	\addtocounter{jdepth@jaskb}{-1}%	
}

\def\cblockprint@jaskb#1#2{%
	\stepcounter{depth@jaskb}%
	\stepcounter{jdepth@jaskb}%
	\pshlsymb@jaskb{guardsym}{\thedepth@jaskb}{#2}%
	\makcl@jaskb{mlevel}{\thedepth@jaskb}%
	\setcl@jaskb{mlevel}{\thedepth@jaskb}{0}%
	\makcl@jaskb{plevel}{\thedepth@jaskb}%
	\setcl@jaskb{plevel}{\thedepth@jaskb}{0}%
	\makdl@jaskb{blockwidth}{\thedepth@jaskb}%
	\setdl@jaskb{blockwidth}{\thedepth@jaskb}{\extrawin@jaskb}%
	\gdef\hypo@jaskb##1##2##3##4{\measurewidth@jaskb{##3}}%
	\gdef\have@jaskb##1##2##3##4{\measurewidth@jaskb{##3}}%
	\gdef\cblock@jaskb##1##2{\cblockmeasure@jaskb{##1}}%
	#1%
	\gdef\hypo@jaskb##1##2##3##4{\statement@jaskb{\thedepth@jaskb}{}{##1}{##2}{\showmark@jaska##3}{##4}}%
	\gdef\have@jaskb##1##2##3##4{\statement@jaskb{\thedepth@jaskb}{}{##1}{##2}{##3}{##4}}%
	\gdef\cblock@jaskb##1##2{\cblockprint@jaskb{##1}{##2}}%
	#1%
	\addtocounter{depth@jaskb}{-1}%
	\addtocounter{jdepth@jaskb}{-1}%
}

\def\hypo@jaskb#1#2#3#4{}
\def\have@jaskb#1#2#3#4{}

\def\cblock@jaskb#1#2{\cblockprint@jaskb{#1}{#2}}

\def\outer@jaskb#1{%
	\setcounter{depth@jaskb}{0}%
	\setcounter{jdepth@jaskb}{0}%
	\setcounter{linecount@jaskb}{0}
	\makcl@jaskb{mlevel}{\thedepth@jaskb}
	\setcl@jaskb{mlevel}{\thedepth@jaskb}{0}
	\makcl@jaskb{plevel}{\thedepth@jaskb}
	\setcl@jaskb{plevel}{\thedepth@jaskb}{0}
	\begin{array}{lll}%
		\gdef\hypo@jaskb##1##2##3##4{\jmeasurewidth@jaskb{##3}\statement@jaskb{\thedepth@jaskb}{}{##1}{##2}{\showmark@jaska##3}{##4}}%
		\gdef\have@jaskb##1##2##3##4{\jmeasurewidth@jaskb{##3}\statement@jaskb{\thedepth@jaskb}{}{##1}{##2}{##3}{##4}}%
		#1%
	\end{array}%
}

%%%%% OUTPUT LEVEL
\gdef\setvstate@jaskc{%
	\gdef\ndline##1##2##3{%
		\have@jaskb{##1.}{}{##2}{##3}%
	}%
}

\gdef\setystate@jaskc{%
	\gdef\ndline##1##2##3{%
		\hypo@jaskb{##1.}{}{##2}{##3}%
	}%
}
	
\gdef\setJcondblock@jaskc{%
	\gdef\condblock##1##2##3{%
		\cblock@jaskb{##3}{##1\;}%
		##2%
	}%
}%

\gdef\setJblockcond@jaskc{%
	\gdef\blockcond##1##2##3{%
		\cblock@jaskb{##2}{##1\;}%
		##3%
	}%
}%

\gdef\setKMcondblock@jaskc{%
	\gdef\condblock##1##2##3{%
		\setystate@jaskc
		##2%
		\setvstate@jaskc%
		\cblock@jaskb{##3}{##1\;}%
	}%
}%

\gdef\setKMblockcond@jaskc{%
	\gdef\blockcond##1##2##3{%
		\setystate@jaskc
		##3%
		\setvstate@jaskc%
		\cblock@jaskb{##2}{##1\;}%
	}%
}%			

\gdef\condblock#1#2#3{}
\gdef\blockcond#1#2#3{}
\gdef\ndline#1#2#3{}

\newcommand{\Jproof}[1]{
	\setstylej@jaska%
	\setvstate@jaskc
	\setJcondblock@jaskc
	\setJblockcond@jaskc
	\outer@jaskb{#1}%
}

\newcommand{\KMproof}[1]{
	\setstylekm@jaska%
	\setvstate@jaskc%
	\setKMcondblock@jaskc
	\setKMblockcond@jaskc
	\outer@jaskb{#1}%
}

\newcommand{\proofline}[2]{
	\ndline{}{#1}{#2}
}

\newcommand{\cablk}[3][]{
	\blockcond{#1}{#2}{#3}
}

\newcommand{\cbblk}[3][]{
	\condblock{#1}{#2}{#3}
}


\makeatother