beautifHOL 0.1 → 0.10
raw patch · 12 files changed
+2674/−2 lines, 12 filesbinary-added
Files
- AbsHOL.hs +40/−0
- ConfigHOL.hs +93/−0
- DOCHOL.pdf binary
- DocHOL.tex +160/−0
- ErrM.hs +26/−0
- HOL.cf +35/−0
- LexHOL.hs +346/−0
- ParHOL.hs +922/−0
- PrintHOL.hs +808/−0
- SkelHOL.hs +65/−0
- beautifHOL.cabal +2/−2
- examples.txt +177/−0
+ AbsHOL.hs view
@@ -0,0 +1,40 @@+module AbsHOL where++-- Haskell module generated by the BNF converter++newtype Idents = Idents String deriving (Eq,Ord,Show)+newtype PredId = PredId String deriving (Eq,Ord,Show)+newtype FunctId = FunctId String deriving (Eq,Ord,Show)+data PROGRAM =+ PROGRAM [SENT]+ deriving (Eq,Ord,Show)++data DEF =+ DefSent Idents SENT+ deriving (Eq,Ord,Show)++data SENT =+ ASentPred PredId [TERMS]+ | TrueSent+ | FalseSent+ | IdentSent Idents+ | ASentEq TERM TERM+ | NegSent SENT+ | IfSent SENT SENT SENT+ | AndSent SENT SENT+ | OrSent SENT SENT+ | ImpSent SENT SENT+ | LetSent [DEF] SENT+ | ForallSent [TERM] SENT+ | ExistsSent [TERM] SENT+ deriving (Eq,Ord,Show)++data TERM =+ FunctTerm FunctId [TERMS]+ | ConstVarTerm Idents+ deriving (Eq,Ord,Show)++data TERMS =+ Terms [TERM]+ deriving (Eq,Ord,Show)+
+ ConfigHOL.hs view
@@ -0,0 +1,93 @@+{-+# ConfigHOL for beautifHOL, a HOL prettyprinter+# Based on the paper found at http://www.cs.indiana.edu/~lepike/pub_pages/pphol.html+# Lee Pike <lee-pike-@-gma-il-.com> (remove dashes)+# Jan 5, 2009+# Copyright 2008++# This file is part of beautifHOL.+# BSD3.+-}++module ConfigHOL where++-- Maximum lenght of a term before splitting it across lines.+maxArgLen :: Int+maxArgLen = 10++-- Output strings. Listed here as a list of strings for easy manipulation. DO+-- NOT CHANGE THE ORDER OF THE LIST! Most of the operators are obvious; ones+-- that are not are commented.+opStr :: [String]+opStr = + [ "true", "false", "=", "and", "or", "not", "implies", "forall", "exists"+ , " " -- the space separator (" " for ASCII pretty-printing)+ , "\n" -- the line-break operator+ , "." -- the separator between variables after a quantifier and the sentence+ , "," -- the separator between arguments to a function or predicate or let definitions+ , "\n" -- prelude+ , "\n" -- postlude+ , "|" -- String to separate labels from the formula+ , "if", "then", "else"+ , "let", "in " -- complete HACK because the prter inserts spcs and these+ -- are 1 spc apart. Okay for two.+ ] +------------+-- +-- Below, the only thing to edit is to manually set some of the tab lengths for+-- the above operators if your output strings are to be comiled (e.g., for LaTeX+-- output, you might want to set the tab for forall to be 1 (rather than the+-- length of '\forall').+--+------------+ +trueStr, falseStr, eqStr, andStr, orStr, negStr, impStr, forallStr, existsStr :: String+spaceStr, brkStr, quantVarsMark, argSepStr, preStr, postStr, labelSepStr :: String+ifStr, thenStr, elseStr, letStr, inStr :: String++eqTab, andTab, orTab, negTab, impTab, forallTab, existsTab, ifTab, letTab :: Int++trueStr = opStr !! 0 --"true"+falseStr = opStr !! 1 --"false"+eqStr = opStr !! 2 --"="+andStr = opStr !! 3 --"and"+orStr = opStr !! 4 --"or"+negStr = opStr !! 5 --"not"+impStr = opStr !! 6 --"implies"+forallStr = opStr !! 7 --"forall"+existsStr = opStr !! 8 --"exists"+spaceStr = opStr !! 9 --" "++brkChar :: Char+brkChar = head $ opStr !! 10 --'\n'+brkStr = [brkChar]++quantVarsMark = opStr !! 11 --"."+argSepStr = opStr !! 12 --","+preStr = opStr !! 13+postStr = opStr !! 14+labelSepStr = opStr !! 15++ifStr = opStr !! 16+thenStr = opStr !! 17+elseStr = opStr !! 18+letStr = opStr !! 19+inStr = opStr !! 20++eqTab = length eqStr+andTab = length andStr+orTab = length orStr+negTab = length negStr+impTab = length impStr+forallTab = length forallStr+existsTab = length existsStr+ifTab = max (length ifStr) $ max (length thenStr) (length elseStr)+letTab = max (length letStr) (length inStr)++-- get filepath+-- check that the dir and file exist+-- open the file+-- parse it+-- return errors on bad parsing+-- set the constants+-- close the file
+ DOCHOL.pdf view
binary file changed (absent → 47372 bytes)
+ DocHOL.tex view
@@ -0,0 +1,160 @@+\batchmode+%This Latex file is machine-generated by the BNF-converter++\documentclass[a4paper,11pt]{article}+\author{BNF-converter}+\title{The Language HOL}+\setlength{\parindent}{0mm}+\setlength{\parskip}{1mm}+\begin{document}++\maketitle++\newcommand{\emptyP}{\mbox{$\epsilon$}}+\newcommand{\terminal}[1]{\mbox{{\texttt {#1}}}}+\newcommand{\nonterminal}[1]{\mbox{$\langle \mbox{{\sl #1 }} \! \rangle$}}+\newcommand{\arrow}{\mbox{::=}}+\newcommand{\delimit}{\mbox{$|$}}+\newcommand{\reserved}[1]{\mbox{{\texttt {#1}}}}+\newcommand{\literal}[1]{\mbox{{\texttt {#1}}}}+\newcommand{\symb}[1]{\mbox{{\texttt {#1}}}}++This document was automatically generated by the {\em BNF-Converter}. It was generated together with the lexer, the parser, and the abstract syntax module, which guarantees that the document matches with the implementation of the language (provided no hand-hacking has taken place).++\section*{The lexical structure of HOL}++\subsection*{Literals}+++++Idents literals are recognized by the regular expression+\({\nonterminal{letter}}+ {\nonterminal{digit}}* \mid {\nonterminal{digit}}+\)++PredId literals are recognized by the regular expression+\({\nonterminal{upper}} {\nonterminal{letter}}* \mbox{`('}\)++FunctId literals are recognized by the regular expression+\({\nonterminal{lower}} {\nonterminal{letter}}* \mbox{`('}\)+++\subsection*{Reserved words and symbols}+The set of reserved words is the set of terminals appearing in the grammar. Those reserved words that consist of non-letter characters are called symbols, and they are treated in a different way from those that are similar to identifiers. The lexer follows rules familiar from languages like Haskell, C, and Java, including longest match and spacing conventions.++The reserved words used in HOL are the following: \\++\begin{tabular}{lll}+{\reserved{and}} &{\reserved{else}} &{\reserved{exists}} \\+{\reserved{false}} &{\reserved{forall}} &{\reserved{if}} \\+{\reserved{implies}} &{\reserved{in}} &{\reserved{let}} \\+{\reserved{not}} &{\reserved{or}} &{\reserved{then}} \\+{\reserved{true}} & & \\+\end{tabular}\\++The symbols used in HOL are the following: \\++\begin{tabular}{lll}+{\symb{)}} &{\symb{{$=$}}} &{\symb{.}} \\+{\symb{)(}} &{\symb{,}} &{\symb{;}} \\+{\symb{(}} & & \\+\end{tabular}\\++\subsection*{Comments}+Single-line comments begin with {\symb{{$-$}{$-$}}}. \\There are no multiple-line comments in the grammar.++\section*{The syntactic structure of HOL}+Non-terminals are enclosed between $\langle$ and $\rangle$. +The symbols {\arrow} (production), {\delimit} (union) +and {\emptyP} (empty rule) belong to the BNF notation. +All other symbols are terminals.\\++\begin{tabular}{lll}+{\nonterminal{PROGRAM}} & {\arrow} &{\nonterminal{ListSENT}} \\+\end{tabular}\\++\begin{tabular}{lll}+{\nonterminal{SENT6}} & {\arrow} &{\nonterminal{PredId}} {\nonterminal{ListTERMS}} {\terminal{)}} \\+ & {\delimit} &{\terminal{true}} \\+ & {\delimit} &{\terminal{false}} \\+ & {\delimit} &{\nonterminal{Idents}} \\+ & {\delimit} &{\nonterminal{TERM}} {\terminal{{$=$}}} {\nonterminal{TERM}} \\+ & {\delimit} &{\terminal{(}} {\nonterminal{SENT}} {\terminal{)}} \\+\end{tabular}\\++\begin{tabular}{lll}+{\nonterminal{SENT5}} & {\arrow} &{\terminal{not}} {\nonterminal{SENT5}} \\+ & {\delimit} &{\nonterminal{SENT6}} \\+\end{tabular}\\++\begin{tabular}{lll}+{\nonterminal{SENT4}} & {\arrow} &{\terminal{if}} {\nonterminal{SENT3}} {\terminal{then}} {\nonterminal{SENT3}} {\terminal{else}} {\nonterminal{SENT3}} \\+ & {\delimit} &{\terminal{let}} {\nonterminal{ListDEF}} {\terminal{in}} {\nonterminal{SENT2}} \\+ & {\delimit} &{\nonterminal{SENT5}} \\+\end{tabular}\\++\begin{tabular}{lll}+{\nonterminal{SENT3}} & {\arrow} &{\nonterminal{SENT3}} {\terminal{and}} {\nonterminal{SENT4}} \\+ & {\delimit} &{\nonterminal{SENT3}} {\terminal{or}} {\nonterminal{SENT4}} \\+ & {\delimit} &{\nonterminal{SENT4}} \\+\end{tabular}\\++\begin{tabular}{lll}+{\nonterminal{SENT2}} & {\arrow} &{\nonterminal{SENT2}} {\terminal{implies}} {\nonterminal{SENT3}} \\+ & {\delimit} &{\nonterminal{SENT3}} \\+\end{tabular}\\++\begin{tabular}{lll}+{\nonterminal{DEF}} & {\arrow} &{\nonterminal{Idents}} {\terminal{{$=$}}} {\nonterminal{SENT}} \\+\end{tabular}\\++\begin{tabular}{lll}+{\nonterminal{SENT}} & {\arrow} &{\terminal{forall}} {\nonterminal{ListTERM}} {\terminal{.}} {\nonterminal{SENT}} \\+ & {\delimit} &{\terminal{exists}} {\nonterminal{ListTERM}} {\terminal{.}} {\nonterminal{SENT}} \\+ & {\delimit} &{\nonterminal{SENT1}} \\+\end{tabular}\\++\begin{tabular}{lll}+{\nonterminal{TERM}} & {\arrow} &{\nonterminal{FunctId}} {\nonterminal{ListTERMS}} {\terminal{)}} \\+ & {\delimit} &{\nonterminal{TERM1}} \\+\end{tabular}\\++\begin{tabular}{lll}+{\nonterminal{TERM1}} & {\arrow} &{\nonterminal{Idents}} \\+ & {\delimit} &{\terminal{(}} {\nonterminal{TERM}} {\terminal{)}} \\+\end{tabular}\\++\begin{tabular}{lll}+{\nonterminal{TERMS}} & {\arrow} &{\nonterminal{ListTERM}} \\+\end{tabular}\\++\begin{tabular}{lll}+{\nonterminal{ListTERMS}} & {\arrow} &{\emptyP} \\+ & {\delimit} &{\nonterminal{TERMS}} \\+ & {\delimit} &{\nonterminal{TERMS}} {\terminal{)(}} {\nonterminal{ListTERMS}} \\+\end{tabular}\\++\begin{tabular}{lll}+{\nonterminal{ListDEF}} & {\arrow} &{\emptyP} \\+ & {\delimit} &{\nonterminal{DEF}} \\+ & {\delimit} &{\nonterminal{DEF}} {\terminal{,}} {\nonterminal{ListDEF}} \\+\end{tabular}\\++\begin{tabular}{lll}+{\nonterminal{ListSENT}} & {\arrow} &{\emptyP} \\+ & {\delimit} &{\nonterminal{SENT}} {\terminal{;}} {\nonterminal{ListSENT}} \\+\end{tabular}\\++\begin{tabular}{lll}+{\nonterminal{SENT1}} & {\arrow} &{\nonterminal{SENT2}} \\+\end{tabular}\\++\begin{tabular}{lll}+{\nonterminal{ListTERM}} & {\arrow} &{\emptyP} \\+ & {\delimit} &{\nonterminal{TERM}} \\+ & {\delimit} &{\nonterminal{TERM}} {\terminal{,}} {\nonterminal{ListTERM}} \\+\end{tabular}\\++++\end{document}+
+ ErrM.hs view
@@ -0,0 +1,26 @@+-- BNF Converter: Error Monad+-- Copyright (C) 2004 Author: Aarne Ranta++-- This file comes with NO WARRANTY and may be used FOR ANY PURPOSE.+module ErrM where++-- the Error monad: like Maybe type with error msgs++import Control.Monad (MonadPlus(..), liftM)++data Err a = Ok a | Bad String+ deriving (Read, Show, Eq, Ord)++instance Monad Err where+ return = Ok+ fail = Bad+ Ok a >>= f = f a+ Bad s >>= f = Bad s++instance Functor Err where+ fmap = liftM++instance MonadPlus Err where+ mzero = Bad "Err.mzero"+ mplus (Bad _) y = y+ mplus x _ = x
+ HOL.cf view
@@ -0,0 +1,35 @@++PROGRAM. PROGRAM ::= [SENT] ;+ASentPred. SENT6 ::= PredId [TERMS] ")";+TrueSent. SENT6 ::= "true" ;+FalseSent. SENT6 ::= "false" ;+IdentSent. SENT6 ::= Idents ;+ASentEq. SENT6 ::= TERM "=" TERM ;+NegSent. SENT5 ::= "not" SENT5 ;+IfSent. SENT4 ::= "if" SENT3 "then" SENT3 "else" SENT3 ;+AndSent. SENT3 ::= SENT3 "and" SENT4 ;+OrSent. SENT3 ::= SENT3 "or" SENT4 ;+ImpSent. SENT2 ::= SENT2 "implies" SENT3 ;+LetSent. SENT4 ::= "let" [DEF] "in" SENT2 ;+DefSent. DEF ::= Idents "=" SENT ;+ForallSent. SENT ::= "forall" [TERM] "." SENT ;+ExistsSent. SENT ::= "exists" [TERM] "." SENT ;+FunctTerm. TERM ::= FunctId [TERMS] ")" ;+ConstVarTerm. TERM1 ::= Idents ;+Terms. TERMS ::= [TERM] ;+++--separator Idents "," ;+separator TERMS ")(" ;+separator DEF "," ;+terminator SENT ";" ;+coercions SENT 6 ;+coercions TERM 1 ;+separator TERM "," ;+token Idents ((letter)+ (digit)* | (digit)+) ;++-- Note: parents must start right after pred and funct names.+token PredId (upper (letter)* '(' );+token FunctId (lower (letter)* '(');+comment "--" ;+
+ LexHOL.hs view
@@ -0,0 +1,346 @@+{-# OPTIONS -fglasgow-exts -cpp #-}+{-# LINE 3 "LexHOL.x" #-}++{-# OPTIONS -fno-warn-incomplete-patterns #-}+module LexHOL where++++#if __GLASGOW_HASKELL__ >= 603+#include "ghcconfig.h"+#elif defined(__GLASGOW_HASKELL__)+#include "config.h"+#endif+#if __GLASGOW_HASKELL__ >= 503+import Data.Array+import Data.Char (ord)+import Data.Array.Base (unsafeAt)+#else+import Array+import Char (ord)+#endif+#if __GLASGOW_HASKELL__ >= 503+import GHC.Exts+#else+import GlaExts+#endif+alex_base :: AlexAddr+alex_base = AlexA# "\xf8\xff\xff\xff\xd9\xff\xff\xff\xfd\xff\xff\xff\xfe\xff\xff\xff\xdc\xff\xff\xff\x02\x00\x00\x00\x00\x00\x00\x00\xe2\xff\xff\xff\xd1\x00\x00\x00\xaa\x01\x00\x00\x83\x02\x00\x00\x5c\x03\x00\x00\x2c\x04\x00\x00\x43\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xfc\x04\x00\x00"#++alex_table :: AlexAddr+alex_table = AlexA# "\x00\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x04\x00\xff\xff\xff\xff\x02\x00\x06\x00\x05\x00\x05\x00\x05\x00\x05\x00\x05\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x05\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x06\x00\x07\x00\x05\x00\x00\x00\x06\x00\x04\x00\x06\x00\x00\x00\x0d\x00\x0d\x00\x0d\x00\x0d\x00\x0d\x00\x0d\x00\x0d\x00\x0d\x00\x0d\x00\x0d\x00\x00\x00\x06\x00\x00\x00\x06\x00\x00\x00\x00\x00\x00\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0d\x00\x0d\x00\x0d\x00\x0d\x00\x0d\x00\x0d\x00\x0d\x00\x0d\x00\x0d\x00\x0d\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x00\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x08\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x00\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x0a\x00\x10\x00\x0e\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x00\x00\x00\x00\x00\x00\x00\x00\x10\x00\x00\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x00\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x00\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x10\x00\x0e\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x00\x00\x00\x00\x00\x00\x00\x00\x10\x00\x00\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x00\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x00\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x09\x00\x10\x00\x0f\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x00\x00\x00\x00\x00\x00\x00\x00\x10\x00\x00\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x00\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x00\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x10\x00\x0f\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x00\x00\x00\x00\x00\x00\x00\x00\x10\x00\x00\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x00\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x10\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0b\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x0c\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x00\x00\x00\x00\x00\x00\x00\x00\x10\x00\x00\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x00\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x00\x00\x00\x00\x00\x00\x00\x00\x10\x00\x00\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x00\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x00\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00\x10\x00"#++alex_check :: AlexAddr+alex_check = AlexA# "\xff\xff\x09\x00\x0a\x00\x0b\x00\x0c\x00\x0d\x00\x2d\x00\x0a\x00\x0a\x00\x2d\x00\x28\x00\x09\x00\x0a\x00\x0b\x00\x0c\x00\x0d\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x20\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x28\x00\x29\x00\x20\x00\xff\xff\x2c\x00\x2d\x00\x2e\x00\xff\xff\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\x3b\x00\xff\xff\x3d\x00\xff\xff\xff\xff\xff\xff\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xc0\x00\xc1\x00\xc2\x00\xc3\x00\xc4\x00\xc5\x00\xc6\x00\xc7\x00\xc8\x00\xc9\x00\xca\x00\xcb\x00\xcc\x00\xcd\x00\xce\x00\xcf\x00\xd0\x00\xd1\x00\xd2\x00\xd3\x00\xd4\x00\xd5\x00\xd6\x00\xff\xff\xd8\x00\xd9\x00\xda\x00\xdb\x00\xdc\x00\xdd\x00\xde\x00\xdf\x00\xe0\x00\xe1\x00\xe2\x00\xe3\x00\xe4\x00\xe5\x00\xe6\x00\xe7\x00\xe8\x00\xe9\x00\xea\x00\xeb\x00\xec\x00\xed\x00\xee\x00\xef\x00\xf0\x00\xf1\x00\xf2\x00\xf3\x00\xf4\x00\xf5\x00\xf6\x00\xff\xff\xf8\x00\xf9\x00\xfa\x00\xfb\x00\xfc\x00\xfd\x00\xfe\x00\xff\x00\x27\x00\x28\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xc0\x00\xc1\x00\xc2\x00\xc3\x00\xc4\x00\xc5\x00\xc6\x00\xc7\x00\xc8\x00\xc9\x00\xca\x00\xcb\x00\xcc\x00\xcd\x00\xce\x00\xcf\x00\xd0\x00\xd1\x00\xd2\x00\xd3\x00\xd4\x00\xd5\x00\xd6\x00\xff\xff\xd8\x00\xd9\x00\xda\x00\xdb\x00\xdc\x00\xdd\x00\xde\x00\xdf\x00\xe0\x00\xe1\x00\xe2\x00\xe3\x00\xe4\x00\xe5\x00\xe6\x00\xe7\x00\xe8\x00\xe9\x00\xea\x00\xeb\x00\xec\x00\xed\x00\xee\x00\xef\x00\xf0\x00\xf1\x00\xf2\x00\xf3\x00\xf4\x00\xf5\x00\xf6\x00\xff\xff\xf8\x00\xf9\x00\xfa\x00\xfb\x00\xfc\x00\xfd\x00\xfe\x00\xff\x00\x27\x00\x28\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xc0\x00\xc1\x00\xc2\x00\xc3\x00\xc4\x00\xc5\x00\xc6\x00\xc7\x00\xc8\x00\xc9\x00\xca\x00\xcb\x00\xcc\x00\xcd\x00\xce\x00\xcf\x00\xd0\x00\xd1\x00\xd2\x00\xd3\x00\xd4\x00\xd5\x00\xd6\x00\xff\xff\xd8\x00\xd9\x00\xda\x00\xdb\x00\xdc\x00\xdd\x00\xde\x00\xdf\x00\xe0\x00\xe1\x00\xe2\x00\xe3\x00\xe4\x00\xe5\x00\xe6\x00\xe7\x00\xe8\x00\xe9\x00\xea\x00\xeb\x00\xec\x00\xed\x00\xee\x00\xef\x00\xf0\x00\xf1\x00\xf2\x00\xf3\x00\xf4\x00\xf5\x00\xf6\x00\xff\xff\xf8\x00\xf9\x00\xfa\x00\xfb\x00\xfc\x00\xfd\x00\xfe\x00\xff\x00\x27\x00\x28\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xc0\x00\xc1\x00\xc2\x00\xc3\x00\xc4\x00\xc5\x00\xc6\x00\xc7\x00\xc8\x00\xc9\x00\xca\x00\xcb\x00\xcc\x00\xcd\x00\xce\x00\xcf\x00\xd0\x00\xd1\x00\xd2\x00\xd3\x00\xd4\x00\xd5\x00\xd6\x00\xff\xff\xd8\x00\xd9\x00\xda\x00\xdb\x00\xdc\x00\xdd\x00\xde\x00\xdf\x00\xe0\x00\xe1\x00\xe2\x00\xe3\x00\xe4\x00\xe5\x00\xe6\x00\xe7\x00\xe8\x00\xe9\x00\xea\x00\xeb\x00\xec\x00\xed\x00\xee\x00\xef\x00\xf0\x00\xf1\x00\xf2\x00\xf3\x00\xf4\x00\xf5\x00\xf6\x00\xff\xff\xf8\x00\xf9\x00\xfa\x00\xfb\x00\xfc\x00\xfd\x00\xfe\x00\xff\x00\x27\x00\x28\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xc0\x00\xc1\x00\xc2\x00\xc3\x00\xc4\x00\xc5\x00\xc6\x00\xc7\x00\xc8\x00\xc9\x00\xca\x00\xcb\x00\xcc\x00\xcd\x00\xce\x00\xcf\x00\xd0\x00\xd1\x00\xd2\x00\xd3\x00\xd4\x00\xd5\x00\xd6\x00\xff\xff\xd8\x00\xd9\x00\xda\x00\xdb\x00\xdc\x00\xdd\x00\xde\x00\xdf\x00\xe0\x00\xe1\x00\xe2\x00\xe3\x00\xe4\x00\xe5\x00\xe6\x00\xe7\x00\xe8\x00\xe9\x00\xea\x00\xeb\x00\xec\x00\xed\x00\xee\x00\xef\x00\xf0\x00\xf1\x00\xf2\x00\xf3\x00\xf4\x00\xf5\x00\xf6\x00\x27\x00\xf8\x00\xf9\x00\xfa\x00\xfb\x00\xfc\x00\xfd\x00\xfe\x00\xff\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xc0\x00\xc1\x00\xc2\x00\xc3\x00\xc4\x00\xc5\x00\xc6\x00\xc7\x00\xc8\x00\xc9\x00\xca\x00\xcb\x00\xcc\x00\xcd\x00\xce\x00\xcf\x00\xd0\x00\xd1\x00\xd2\x00\xd3\x00\xd4\x00\xd5\x00\xd6\x00\xff\xff\xd8\x00\xd9\x00\xda\x00\xdb\x00\xdc\x00\xdd\x00\xde\x00\xdf\x00\xe0\x00\xe1\x00\xe2\x00\xe3\x00\xe4\x00\xe5\x00\xe6\x00\xe7\x00\xe8\x00\xe9\x00\xea\x00\xeb\x00\xec\x00\xed\x00\xee\x00\xef\x00\xf0\x00\xf1\x00\xf2\x00\xf3\x00\xf4\x00\xf5\x00\xf6\x00\x27\x00\xf8\x00\xf9\x00\xfa\x00\xfb\x00\xfc\x00\xfd\x00\xfe\x00\xff\x00\x30\x00\x31\x00\x32\x00\x33\x00\x34\x00\x35\x00\x36\x00\x37\x00\x38\x00\x39\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x41\x00\x42\x00\x43\x00\x44\x00\x45\x00\x46\x00\x47\x00\x48\x00\x49\x00\x4a\x00\x4b\x00\x4c\x00\x4d\x00\x4e\x00\x4f\x00\x50\x00\x51\x00\x52\x00\x53\x00\x54\x00\x55\x00\x56\x00\x57\x00\x58\x00\x59\x00\x5a\x00\xff\xff\xff\xff\xff\xff\xff\xff\x5f\x00\xff\xff\x61\x00\x62\x00\x63\x00\x64\x00\x65\x00\x66\x00\x67\x00\x68\x00\x69\x00\x6a\x00\x6b\x00\x6c\x00\x6d\x00\x6e\x00\x6f\x00\x70\x00\x71\x00\x72\x00\x73\x00\x74\x00\x75\x00\x76\x00\x77\x00\x78\x00\x79\x00\x7a\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xc0\x00\xc1\x00\xc2\x00\xc3\x00\xc4\x00\xc5\x00\xc6\x00\xc7\x00\xc8\x00\xc9\x00\xca\x00\xcb\x00\xcc\x00\xcd\x00\xce\x00\xcf\x00\xd0\x00\xd1\x00\xd2\x00\xd3\x00\xd4\x00\xd5\x00\xd6\x00\xff\xff\xd8\x00\xd9\x00\xda\x00\xdb\x00\xdc\x00\xdd\x00\xde\x00\xdf\x00\xe0\x00\xe1\x00\xe2\x00\xe3\x00\xe4\x00\xe5\x00\xe6\x00\xe7\x00\xe8\x00\xe9\x00\xea\x00\xeb\x00\xec\x00\xed\x00\xee\x00\xef\x00\xf0\x00\xf1\x00\xf2\x00\xf3\x00\xf4\x00\xf5\x00\xf6\x00\xff\xff\xf8\x00\xf9\x00\xfa\x00\xfb\x00\xfc\x00\xfd\x00\xfe\x00\xff\x00"#++alex_deflt :: AlexAddr+alex_deflt = AlexA# "\xff\xff\xff\xff\x03\x00\x03\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff"#++alex_accept = listArray (0::Int,16) [[],[],[(AlexAccSkip)],[(AlexAccSkip)],[],[(AlexAccSkip)],[(AlexAcc (alex_action_2))],[(AlexAcc (alex_action_2))],[(AlexAcc (alex_action_3))],[(AlexAcc (alex_action_3))],[(AlexAcc (alex_action_3))],[(AlexAcc (alex_action_3))],[(AlexAcc (alex_action_3))],[(AlexAcc (alex_action_3))],[(AlexAcc (alex_action_4))],[(AlexAcc (alex_action_5))],[(AlexAcc (alex_action_6))]]+{-# LINE 36 "LexHOL.x" #-}+++tok f p s = f p s++share :: String -> String+share = id++data Tok =+ TS !String -- reserved words and symbols+ | TL !String -- string literals+ | TI !String -- integer literals+ | TV !String -- identifiers+ | TD !String -- double precision float literals+ | TC !String -- character literals+ | T_Idents !String+ | T_PredId !String+ | T_FunctId !String++ deriving (Eq,Show,Ord)++data Token = + PT Posn Tok+ | Err Posn+ deriving (Eq,Show,Ord)++tokenPos (PT (Pn _ l _) _ :_) = "line " ++ show l+tokenPos (Err (Pn _ l _) :_) = "line " ++ show l+tokenPos _ = "end of file"++posLineCol (Pn _ l c) = (l,c)+mkPosToken t@(PT p _) = (posLineCol p, prToken t)++prToken t = case t of+ PT _ (TS s) -> s+ PT _ (TI s) -> s+ PT _ (TV s) -> s+ PT _ (TD s) -> s+ PT _ (TC s) -> s+ PT _ (T_Idents s) -> s+ PT _ (T_PredId s) -> s+ PT _ (T_FunctId s) -> s++ _ -> show t++data BTree = N | B String Tok BTree BTree deriving (Show)++eitherResIdent :: (String -> Tok) -> String -> Tok+eitherResIdent tv s = treeFind resWords+ where+ treeFind N = tv s+ treeFind (B a t left right) | s < a = treeFind left+ | s > a = treeFind right+ | s == a = t++resWords = b "implies" (b "false" (b "else" (b "and" N N) (b "exists" N N)) (b "if" (b "forall" N N) N)) (b "or" (b "let" (b "in" N N) (b "not" N N)) (b "true" (b "then" N N) N))+ where b s = B s (TS s)++unescapeInitTail :: String -> String+unescapeInitTail = unesc . tail where+ unesc s = case s of+ '\\':c:cs | elem c ['\"', '\\', '\''] -> c : unesc cs+ '\\':'n':cs -> '\n' : unesc cs+ '\\':'t':cs -> '\t' : unesc cs+ '"':[] -> []+ c:cs -> c : unesc cs+ _ -> []++-------------------------------------------------------------------+-- Alex wrapper code.+-- A modified "posn" wrapper.+-------------------------------------------------------------------++data Posn = Pn !Int !Int !Int+ deriving (Eq, Show,Ord)++alexStartPos :: Posn+alexStartPos = Pn 0 1 1++alexMove :: Posn -> Char -> Posn+alexMove (Pn a l c) '\t' = Pn (a+1) l (((c+7) `div` 8)*8+1)+alexMove (Pn a l c) '\n' = Pn (a+1) (l+1) 1+alexMove (Pn a l c) _ = Pn (a+1) l (c+1)++type AlexInput = (Posn, -- current position,+ Char, -- previous char+ String) -- current input string++tokens :: String -> [Token]+tokens str = go (alexStartPos, '\n', str)+ where+ go :: (Posn, Char, String) -> [Token]+ go inp@(pos, _, str) =+ case alexScan inp 0 of+ AlexEOF -> []+ AlexError (pos, _, _) -> [Err pos]+ AlexSkip inp' len -> go inp'+ AlexToken inp' len act -> act pos (take len str) : (go inp')++alexGetChar :: AlexInput -> Maybe (Char,AlexInput)+alexGetChar (p, c, []) = Nothing+alexGetChar (p, _, (c:s)) =+ let p' = alexMove p c+ in p' `seq` Just (c, (p', c, s))++alexInputPrevChar :: AlexInput -> Char+alexInputPrevChar (p, c, s) = c++alex_action_2 = tok (\p s -> PT p (TS $ share s)) +alex_action_3 = tok (\p s -> PT p (eitherResIdent (T_Idents . share) s)) +alex_action_4 = tok (\p s -> PT p (eitherResIdent (T_PredId . share) s)) +alex_action_5 = tok (\p s -> PT p (eitherResIdent (T_FunctId . share) s)) +alex_action_6 = tok (\p s -> PT p (eitherResIdent (TV . share) s)) +{-# LINE 1 "templates/GenericTemplate.hs" #-}+{-# LINE 1 "templates/GenericTemplate.hs" #-}+{-# LINE 1 "<built-in>" #-}+{-# LINE 1 "<command line>" #-}+{-# LINE 1 "templates/GenericTemplate.hs" #-}+-- -----------------------------------------------------------------------------+-- ALEX TEMPLATE+--+-- This code is in the PUBLIC DOMAIN; you may copy it freely and use+-- it for any purpose whatsoever.++-- -----------------------------------------------------------------------------+-- INTERNALS and main scanner engine++{-# LINE 35 "templates/GenericTemplate.hs" #-}++{-# LINE 45 "templates/GenericTemplate.hs" #-}+++data AlexAddr = AlexA# Addr#++#if __GLASGOW_HASKELL__ < 503+uncheckedShiftL# = shiftL#+#endif++{-# INLINE alexIndexInt16OffAddr #-}+alexIndexInt16OffAddr (AlexA# arr) off =+#ifdef WORDS_BIGENDIAN+ narrow16Int# i+ where+ i = word2Int# ((high `uncheckedShiftL#` 8#) `or#` low)+ high = int2Word# (ord# (indexCharOffAddr# arr (off' +# 1#)))+ low = int2Word# (ord# (indexCharOffAddr# arr off'))+ off' = off *# 2#+#else+ indexInt16OffAddr# arr off+#endif++++++{-# INLINE alexIndexInt32OffAddr #-}+alexIndexInt32OffAddr (AlexA# arr) off = +#ifdef WORDS_BIGENDIAN+ narrow32Int# i+ where+ i = word2Int# ((b3 `uncheckedShiftL#` 24#) `or#`+ (b2 `uncheckedShiftL#` 16#) `or#`+ (b1 `uncheckedShiftL#` 8#) `or#` b0)+ b3 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 3#)))+ b2 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 2#)))+ b1 = int2Word# (ord# (indexCharOffAddr# arr (off' +# 1#)))+ b0 = int2Word# (ord# (indexCharOffAddr# arr off'))+ off' = off *# 4#+#else+ indexInt32OffAddr# arr off+#endif++++++#if __GLASGOW_HASKELL__ < 503+quickIndex arr i = arr ! i+#else+-- GHC >= 503, unsafeAt is available from Data.Array.Base.+quickIndex = unsafeAt+#endif+++++-- -----------------------------------------------------------------------------+-- Main lexing routines++data AlexReturn a+ = AlexEOF+ | AlexError !AlexInput+ | AlexSkip !AlexInput !Int+ | AlexToken !AlexInput !Int a++-- alexScan :: AlexInput -> StartCode -> AlexReturn a+alexScan input (I# (sc))+ = alexScanUser undefined input (I# (sc))++alexScanUser user input (I# (sc))+ = case alex_scan_tkn user input 0# input sc AlexNone of+ (AlexNone, input') ->+ case alexGetChar input of+ Nothing -> ++++ AlexEOF+ Just _ ->++++ AlexError input'++ (AlexLastSkip input len, _) ->++++ AlexSkip input len++ (AlexLastAcc k input len, _) ->++++ AlexToken input len k+++-- Push the input through the DFA, remembering the most recent accepting+-- state it encountered.++alex_scan_tkn user orig_input len input s last_acc =+ input `seq` -- strict in the input+ let + new_acc = check_accs (alex_accept `quickIndex` (I# (s)))+ in+ new_acc `seq`+ case alexGetChar input of+ Nothing -> (new_acc, input)+ Just (c, new_input) -> ++++ let+ base = alexIndexInt32OffAddr alex_base s+ (I# (ord_c)) = ord c+ offset = (base +# ord_c)+ check = alexIndexInt16OffAddr alex_check offset+ + new_s = if (offset >=# 0#) && (check ==# ord_c)+ then alexIndexInt16OffAddr alex_table offset+ else alexIndexInt16OffAddr alex_deflt s+ in+ case new_s of + -1# -> (new_acc, input)+ -- on an error, we want to keep the input *before* the+ -- character that failed, not after.+ _ -> alex_scan_tkn user orig_input (len +# 1#) + new_input new_s new_acc++ where+ check_accs [] = last_acc+ check_accs (AlexAcc a : _) = AlexLastAcc a input (I# (len))+ check_accs (AlexAccSkip : _) = AlexLastSkip input (I# (len))+ check_accs (AlexAccPred a pred : rest)+ | pred user orig_input (I# (len)) input+ = AlexLastAcc a input (I# (len))+ check_accs (AlexAccSkipPred pred : rest)+ | pred user orig_input (I# (len)) input+ = AlexLastSkip input (I# (len))+ check_accs (_ : rest) = check_accs rest++data AlexLastAcc a+ = AlexNone+ | AlexLastAcc a !AlexInput !Int+ | AlexLastSkip !AlexInput !Int++data AlexAcc a user+ = AlexAcc a+ | AlexAccSkip+ | AlexAccPred a (AlexAccPred user)+ | AlexAccSkipPred (AlexAccPred user)++type AlexAccPred user = user -> AlexInput -> Int -> AlexInput -> Bool++-- -----------------------------------------------------------------------------+-- Predicates on a rule++alexAndPred p1 p2 user in1 len in2+ = p1 user in1 len in2 && p2 user in1 len in2++--alexPrevCharIsPred :: Char -> AlexAccPred _ +alexPrevCharIs c _ input _ _ = c == alexInputPrevChar input++--alexPrevCharIsOneOfPred :: Array Char Bool -> AlexAccPred _ +alexPrevCharIsOneOf arr _ input _ _ = arr ! alexInputPrevChar input++--alexRightContext :: Int -> AlexAccPred _+alexRightContext (I# (sc)) user _ _ input = + case alex_scan_tkn user input 0# input sc AlexNone of+ (AlexNone, _) -> False+ _ -> True+ -- TODO: there's no need to find the longest+ -- match when checking the right context, just+ -- the first match will do.++-- used by wrappers+iUnbox (I# (i)) = i
+ ParHOL.hs view
@@ -0,0 +1,922 @@+{-# OPTIONS -fglasgow-exts -cpp #-}+{-# OPTIONS -fno-warn-incomplete-patterns -fno-warn-overlapping-patterns #-}+module ParHOL where+import AbsHOL+import LexHOL+import ErrM+#if __GLASGOW_HASKELL__ >= 503+import Data.Array+#else+import Array+#endif+#if __GLASGOW_HASKELL__ >= 503+import GHC.Exts+#else+import GlaExts+#endif++-- parser produced by Happy Version 1.17++newtype HappyAbsSyn = HappyAbsSyn HappyAny+#if __GLASGOW_HASKELL__ >= 607+type HappyAny = GHC.Exts.Any+#else+type HappyAny = forall a . a+#endif+happyIn19 :: (Idents) -> (HappyAbsSyn )+happyIn19 x = unsafeCoerce# x+{-# INLINE happyIn19 #-}+happyOut19 :: (HappyAbsSyn ) -> (Idents)+happyOut19 x = unsafeCoerce# x+{-# INLINE happyOut19 #-}+happyIn20 :: (PredId) -> (HappyAbsSyn )+happyIn20 x = unsafeCoerce# x+{-# INLINE happyIn20 #-}+happyOut20 :: (HappyAbsSyn ) -> (PredId)+happyOut20 x = unsafeCoerce# x+{-# INLINE happyOut20 #-}+happyIn21 :: (FunctId) -> (HappyAbsSyn )+happyIn21 x = unsafeCoerce# x+{-# INLINE happyIn21 #-}+happyOut21 :: (HappyAbsSyn ) -> (FunctId)+happyOut21 x = unsafeCoerce# x+{-# INLINE happyOut21 #-}+happyIn22 :: (PROGRAM) -> (HappyAbsSyn )+happyIn22 x = unsafeCoerce# x+{-# INLINE happyIn22 #-}+happyOut22 :: (HappyAbsSyn ) -> (PROGRAM)+happyOut22 x = unsafeCoerce# x+{-# INLINE happyOut22 #-}+happyIn23 :: (SENT) -> (HappyAbsSyn )+happyIn23 x = unsafeCoerce# x+{-# INLINE happyIn23 #-}+happyOut23 :: (HappyAbsSyn ) -> (SENT)+happyOut23 x = unsafeCoerce# x+{-# INLINE happyOut23 #-}+happyIn24 :: (SENT) -> (HappyAbsSyn )+happyIn24 x = unsafeCoerce# x+{-# INLINE happyIn24 #-}+happyOut24 :: (HappyAbsSyn ) -> (SENT)+happyOut24 x = unsafeCoerce# x+{-# INLINE happyOut24 #-}+happyIn25 :: (SENT) -> (HappyAbsSyn )+happyIn25 x = unsafeCoerce# x+{-# INLINE happyIn25 #-}+happyOut25 :: (HappyAbsSyn ) -> (SENT)+happyOut25 x = unsafeCoerce# x+{-# INLINE happyOut25 #-}+happyIn26 :: (SENT) -> (HappyAbsSyn )+happyIn26 x = unsafeCoerce# x+{-# INLINE happyIn26 #-}+happyOut26 :: (HappyAbsSyn ) -> (SENT)+happyOut26 x = unsafeCoerce# x+{-# INLINE happyOut26 #-}+happyIn27 :: (SENT) -> (HappyAbsSyn )+happyIn27 x = unsafeCoerce# x+{-# INLINE happyIn27 #-}+happyOut27 :: (HappyAbsSyn ) -> (SENT)+happyOut27 x = unsafeCoerce# x+{-# INLINE happyOut27 #-}+happyIn28 :: (DEF) -> (HappyAbsSyn )+happyIn28 x = unsafeCoerce# x+{-# INLINE happyIn28 #-}+happyOut28 :: (HappyAbsSyn ) -> (DEF)+happyOut28 x = unsafeCoerce# x+{-# INLINE happyOut28 #-}+happyIn29 :: (SENT) -> (HappyAbsSyn )+happyIn29 x = unsafeCoerce# x+{-# INLINE happyIn29 #-}+happyOut29 :: (HappyAbsSyn ) -> (SENT)+happyOut29 x = unsafeCoerce# x+{-# INLINE happyOut29 #-}+happyIn30 :: (TERM) -> (HappyAbsSyn )+happyIn30 x = unsafeCoerce# x+{-# INLINE happyIn30 #-}+happyOut30 :: (HappyAbsSyn ) -> (TERM)+happyOut30 x = unsafeCoerce# x+{-# INLINE happyOut30 #-}+happyIn31 :: (TERM) -> (HappyAbsSyn )+happyIn31 x = unsafeCoerce# x+{-# INLINE happyIn31 #-}+happyOut31 :: (HappyAbsSyn ) -> (TERM)+happyOut31 x = unsafeCoerce# x+{-# INLINE happyOut31 #-}+happyIn32 :: (TERMS) -> (HappyAbsSyn )+happyIn32 x = unsafeCoerce# x+{-# INLINE happyIn32 #-}+happyOut32 :: (HappyAbsSyn ) -> (TERMS)+happyOut32 x = unsafeCoerce# x+{-# INLINE happyOut32 #-}+happyIn33 :: ([TERMS]) -> (HappyAbsSyn )+happyIn33 x = unsafeCoerce# x+{-# INLINE happyIn33 #-}+happyOut33 :: (HappyAbsSyn ) -> ([TERMS])+happyOut33 x = unsafeCoerce# x+{-# INLINE happyOut33 #-}+happyIn34 :: ([DEF]) -> (HappyAbsSyn )+happyIn34 x = unsafeCoerce# x+{-# INLINE happyIn34 #-}+happyOut34 :: (HappyAbsSyn ) -> ([DEF])+happyOut34 x = unsafeCoerce# x+{-# INLINE happyOut34 #-}+happyIn35 :: ([SENT]) -> (HappyAbsSyn )+happyIn35 x = unsafeCoerce# x+{-# INLINE happyIn35 #-}+happyOut35 :: (HappyAbsSyn ) -> ([SENT])+happyOut35 x = unsafeCoerce# x+{-# INLINE happyOut35 #-}+happyIn36 :: (SENT) -> (HappyAbsSyn )+happyIn36 x = unsafeCoerce# x+{-# INLINE happyIn36 #-}+happyOut36 :: (HappyAbsSyn ) -> (SENT)+happyOut36 x = unsafeCoerce# x+{-# INLINE happyOut36 #-}+happyIn37 :: ([TERM]) -> (HappyAbsSyn )+happyIn37 x = unsafeCoerce# x+{-# INLINE happyIn37 #-}+happyOut37 :: (HappyAbsSyn ) -> ([TERM])+happyOut37 x = unsafeCoerce# x+{-# INLINE happyOut37 #-}+happyInTok :: Token -> (HappyAbsSyn )+happyInTok x = unsafeCoerce# x+{-# INLINE happyInTok #-}+happyOutTok :: (HappyAbsSyn ) -> Token+happyOutTok x = unsafeCoerce# x+{-# INLINE happyOutTok #-}+++happyActOffsets :: HappyAddr+happyActOffsets = HappyA# "\x00\x00\x1f\x00\xf8\x00\xf1\x00\xf1\x00\xf1\x00\xd1\x00\xe0\x00\x39\x00\x24\x00\x39\x00\x6f\x00\xd1\x00\x00\x00\xf1\x00\x39\x00\xd1\x00\x00\x00\x00\x00\x07\x00\xd7\x00\x00\x00\xbf\x00\x39\x00\x00\x00\x01\x00\x07\x00\x00\x00\x00\x00\x00\x00\x75\x00\xc0\x00\xbe\x00\xb1\x00\xe0\x00\x00\x00\xf1\x00\xa7\x00\xf8\x00\x00\x00\x00\x00\x18\x00\xb0\x00\xa9\x00\x8b\x00\x9c\x00\x7d\x00\x00\x00\x7d\x00\x7d\x00\x7d\x00\x7d\x00\x00\x00\x39\x00\x39\x00\x7d\x00\xff\xff\x2f\x00\x7d\x00\x7d\x00\x7d\x00\x7d\x00\xe0\x00\x7c\x00\xf1\x00\xf1\x00\xf1\x00\x7e\x00\x13\x00\x04\x00\x6b\x00\xe0\x00\x00\x00\x58\x00\x67\x00\x76\x00\x7a\x00\x39\x00\x57\x00\x4c\x00\x39\x00\x10\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf1\x00\xf1\x00\x00\x00\x00\x00\x00\x00\xe0\x00\xe0\x00\x75\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf6\xff\xf2\x00\xf1\x00\x75\x00\x00\x00"#++happyGotoOffsets :: HappyAddr+happyGotoOffsets = HappyA# "\x3c\x00\xa5\x01\x9f\x01\x85\x01\x5e\x01\x1d\x01\x63\x00\xcf\x00\xb2\x01\x4b\x00\x5e\x00\x4f\x00\x83\x00\xf1\xff\xdd\x00\x73\x00\x00\x00\x00\x00\x00\x00\x47\x00\x00\x00\x00\x00\x00\x00\xac\x01\x00\x00\x00\x00\x38\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xc1\x00\x00\x00\x51\x01\x56\x00\x92\x01\x00\x00\x00\x00\xb3\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x66\x00\x62\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xb3\x00\x00\x00\x78\x01\x6b\x01\x44\x01\x00\x00\x00\x00\x30\x00\x03\x00\xa5\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x8d\x01\x00\x00\x00\x00\x15\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x37\x01\x10\x01\x00\x00\x00\x00\x00\x00\x97\x00\x89\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x2a\x01\x00\x00\x00\x00"#++happyDefActions :: HappyAddr+happyDefActions = HappyA# "\xcc\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xc9\xff\xc9\xff\xcf\xff\xcc\xff\x00\x00\xc9\xff\x00\x00\xef\xff\xd5\xff\xc9\xff\xc8\xff\xd6\xff\x00\x00\x00\x00\xed\xff\xd5\xff\xc9\xff\xe4\xff\xe1\xff\xde\xff\xdc\xff\xca\xff\x00\x00\x00\x00\x00\x00\xe9\xff\x00\x00\xcf\xff\x00\x00\xea\xff\xee\xff\x00\x00\x00\x00\xce\xff\x00\x00\xd1\xff\x00\x00\xd3\xff\x00\x00\x00\x00\x00\x00\x00\x00\xd8\xff\xc9\xff\xc9\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xec\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xc9\xff\xcf\xff\x00\x00\xe5\xff\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xc9\xff\x00\x00\xd7\xff\xc7\xff\xd4\xff\xeb\xff\xe7\xff\xe6\xff\x00\x00\x00\x00\xdb\xff\xcd\xff\xd0\xff\x00\x00\x00\x00\xdd\xff\xdf\xff\xe0\xff\xcb\xff\xda\xff\xd9\xff\xe2\xff\x00\x00\x00\x00\xe3\xff"#++happyCheck :: HappyAddr+happyCheck = HappyA# "\xff\xff\x10\x00\x01\x00\x00\x00\x0e\x00\x01\x00\x05\x00\x06\x00\x01\x00\x08\x00\x09\x00\x07\x00\x09\x00\x0e\x00\x07\x00\x0e\x00\x0f\x00\x01\x00\x0f\x00\x12\x00\x13\x00\x00\x00\x03\x00\x02\x00\x19\x00\x15\x00\x19\x00\x17\x00\x15\x00\x19\x00\x17\x00\x07\x00\x0b\x00\x0c\x00\x0a\x00\x0b\x00\x0c\x00\x0d\x00\x07\x00\x12\x00\x10\x00\x11\x00\x0b\x00\x07\x00\x14\x00\x15\x00\x16\x00\x17\x00\x00\x00\x19\x00\x02\x00\x14\x00\x15\x00\x16\x00\x17\x00\x08\x00\x00\x00\x15\x00\x02\x00\x0b\x00\x0c\x00\x0d\x00\x0e\x00\x03\x00\x07\x00\x12\x00\x12\x00\x0b\x00\x0c\x00\x0d\x00\x0e\x00\x00\x00\x19\x00\x02\x00\x12\x00\x00\x00\x10\x00\x01\x00\x15\x00\x00\x00\x17\x00\x02\x00\x0b\x00\x0c\x00\x0d\x00\x0e\x00\x00\x00\x0c\x00\x01\x00\x12\x00\x0b\x00\x0c\x00\x0d\x00\x0e\x00\x00\x00\x09\x00\x02\x00\x12\x00\x00\x00\x00\x00\x02\x00\x0f\x00\x00\x00\x0f\x00\x02\x00\x0b\x00\x0c\x00\x0d\x00\x09\x00\x0b\x00\x0c\x00\x08\x00\x12\x00\x0b\x00\x0c\x00\x00\x00\x12\x00\x02\x00\x07\x00\x01\x00\x12\x00\x12\x00\x13\x00\x01\x00\x02\x00\x08\x00\x0b\x00\x0c\x00\x15\x00\x03\x00\x06\x00\x00\x00\x15\x00\x12\x00\x17\x00\x12\x00\x19\x00\x00\x00\x01\x00\x02\x00\x09\x00\x04\x00\x05\x00\x06\x00\x07\x00\x08\x00\x0f\x00\x0a\x00\x0b\x00\x0c\x00\x19\x00\x00\x00\x01\x00\x02\x00\x11\x00\x04\x00\x05\x00\x06\x00\x07\x00\x08\x00\x04\x00\x0a\x00\x0b\x00\x0c\x00\x19\x00\x00\x00\x01\x00\x02\x00\x11\x00\x04\x00\x05\x00\x06\x00\x07\x00\x08\x00\x05\x00\x0a\x00\x0b\x00\x0c\x00\x02\x00\x00\x00\x01\x00\x02\x00\x11\x00\x04\x00\x05\x00\x06\x00\x07\x00\x08\x00\x15\x00\x0a\x00\x0b\x00\x0c\x00\x02\x00\x00\x00\x01\x00\x02\x00\x11\x00\x04\x00\x05\x00\x06\x00\x07\x00\x08\x00\x19\x00\x0a\x00\x0b\x00\x0c\x00\x0e\x00\x00\x00\x01\x00\x02\x00\x11\x00\x04\x00\x05\x00\x06\x00\x07\x00\x08\x00\x19\x00\x0a\x00\x0b\x00\x0c\x00\x05\x00\x00\x00\x01\x00\x02\x00\x11\x00\x04\x00\x05\x00\x06\x00\x07\x00\x08\x00\x15\x00\x07\x00\x0b\x00\x0c\x00\x0a\x00\x0b\x00\x0c\x00\x0d\x00\x11\x00\xff\xff\x10\x00\x11\x00\xff\xff\xff\xff\x14\x00\x15\x00\x16\x00\x17\x00\x07\x00\xff\xff\x08\x00\x09\x00\x0b\x00\xff\xff\x0d\x00\x07\x00\xff\xff\x10\x00\x11\x00\x0b\x00\x12\x00\x14\x00\x15\x00\x16\x00\x17\x00\x11\x00\xff\xff\xff\xff\x14\x00\x15\x00\x16\x00\x17\x00\x00\x00\x01\x00\x02\x00\xff\xff\x04\x00\x05\x00\x06\x00\x07\x00\x08\x00\xff\xff\xff\xff\x0b\x00\x0c\x00\x00\x00\x01\x00\x02\x00\xff\xff\x04\x00\x05\x00\x06\x00\x07\x00\x08\x00\xff\xff\xff\xff\x0b\x00\x0c\x00\x00\x00\x01\x00\x02\x00\xff\xff\x04\x00\x05\x00\x06\x00\x07\x00\xff\xff\xff\xff\xff\xff\x0b\x00\x0c\x00\x00\x00\x01\x00\x02\x00\xff\xff\x04\x00\x05\x00\x06\x00\x07\x00\xff\xff\xff\xff\xff\xff\x0b\x00\x0c\x00\x00\x00\x01\x00\x02\x00\xff\xff\x04\x00\x05\x00\x06\x00\x07\x00\xff\xff\xff\xff\xff\xff\x0b\x00\x0c\x00\x00\x00\x01\x00\x02\x00\xff\xff\x04\x00\x05\x00\x06\x00\x07\x00\xff\xff\xff\xff\xff\xff\x0b\x00\x0c\x00\x00\x00\x01\x00\x02\x00\xff\xff\x04\x00\x05\x00\x06\x00\x07\x00\xff\xff\xff\xff\xff\xff\x0b\x00\x0c\x00\x00\x00\x01\x00\x02\x00\xff\xff\x04\x00\x05\x00\x06\x00\xff\xff\xff\xff\xff\xff\xff\xff\x0b\x00\x0c\x00\x00\x00\x01\x00\x02\x00\xff\xff\x04\x00\x05\x00\x06\x00\xff\xff\xff\xff\xff\xff\xff\xff\x0b\x00\x0c\x00\x00\x00\x01\x00\x02\x00\xff\xff\x04\x00\x05\x00\x06\x00\xff\xff\x00\x00\xff\xff\x02\x00\x0b\x00\x0c\x00\x00\x00\x01\x00\x02\x00\xff\xff\x04\x00\x05\x00\x0b\x00\x0c\x00\xff\xff\xff\xff\xff\xff\x0b\x00\x0c\x00\x00\x00\x01\x00\x02\x00\xff\xff\x04\x00\x05\x00\x00\x00\x01\x00\x02\x00\xff\xff\x04\x00\x0b\x00\x0c\x00\x00\x00\xff\xff\x02\x00\xff\xff\x0b\x00\x0c\x00\x00\x00\xff\xff\x02\x00\xff\xff\xff\xff\x0b\x00\x0c\x00\xff\xff\xff\xff\xff\xff\xff\xff\x0b\x00\x0c\x00\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff"#++happyTable :: HappyAddr+happyTable = HappyA# "\x00\x00\x29\x00\xd5\xff\x2a\x00\x43\x00\xc9\xff\xe8\xff\xe8\xff\xc9\xff\xe8\xff\xe8\xff\x18\x00\x2b\x00\x43\x00\x18\x00\xe8\xff\xe8\xff\x53\x00\x5b\x00\xe8\xff\xe8\xff\x12\x00\x5e\x00\x13\x00\xff\xff\x12\x00\xe8\xff\x19\x00\x12\x00\xc9\xff\x19\x00\x23\x00\x14\x00\x15\x00\x36\x00\x24\x00\x37\x00\x25\x00\x23\x00\x53\x00\x26\x00\x27\x00\x24\x00\x18\x00\x28\x00\x12\x00\x29\x00\x19\x00\x12\x00\xff\xff\x13\x00\x28\x00\x12\x00\x29\x00\x19\x00\x41\x00\x12\x00\x12\x00\x13\x00\x14\x00\x15\x00\x2d\x00\x5c\x00\x3d\x00\x18\x00\x42\x00\x2f\x00\x14\x00\x15\x00\x2d\x00\x4e\x00\x12\x00\xff\xff\x13\x00\x2f\x00\x12\x00\x3e\x00\x55\x00\x12\x00\x12\x00\x19\x00\x13\x00\x14\x00\x15\x00\x2d\x00\x51\x00\x2a\x00\x31\x00\x56\x00\x2f\x00\x14\x00\x15\x00\x2d\x00\x2e\x00\x12\x00\x2b\x00\x13\x00\x2f\x00\x12\x00\x2a\x00\x13\x00\x49\x00\x12\x00\x5a\x00\x13\x00\x14\x00\x15\x00\x30\x00\x37\x00\x14\x00\x15\x00\x41\x00\x2f\x00\x14\x00\x15\x00\x12\x00\x43\x00\x13\x00\x18\x00\x58\x00\x44\x00\x42\x00\x59\x00\x55\x00\x4e\x00\x41\x00\x14\x00\x15\x00\x12\x00\x5f\x00\x63\x00\x2a\x00\x12\x00\x16\x00\x19\x00\x42\x00\xc9\xff\x19\x00\x1a\x00\x13\x00\x2b\x00\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\x2c\x00\x63\x00\x20\x00\x15\x00\xff\xff\x19\x00\x1a\x00\x13\x00\x34\x00\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\x46\x00\x64\x00\x20\x00\x15\x00\xff\xff\x19\x00\x1a\x00\x13\x00\x34\x00\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\x47\x00\x5a\x00\x20\x00\x15\x00\x48\x00\x19\x00\x1a\x00\x13\x00\x34\x00\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\x12\x00\x3f\x00\x20\x00\x15\x00\x4e\x00\x19\x00\x1a\x00\x13\x00\x34\x00\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\xff\xff\x4b\x00\x4c\x00\x15\x00\x43\x00\x19\x00\x1a\x00\x13\x00\x34\x00\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\xff\xff\x33\x00\x20\x00\x15\x00\x51\x00\x19\x00\x1a\x00\x13\x00\x34\x00\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x1f\x00\x12\x00\x23\x00\x20\x00\x15\x00\x36\x00\x24\x00\x37\x00\x25\x00\x21\x00\x00\x00\x26\x00\x27\x00\x00\x00\x00\x00\x28\x00\x12\x00\x29\x00\x19\x00\x23\x00\x00\x00\x41\x00\x68\x00\x24\x00\x00\x00\x25\x00\x23\x00\x00\x00\x26\x00\x27\x00\x24\x00\x42\x00\x28\x00\x12\x00\x29\x00\x19\x00\x27\x00\x00\x00\x00\x00\x28\x00\x12\x00\x29\x00\x19\x00\x19\x00\x1a\x00\x13\x00\x00\x00\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x65\x00\x00\x00\x00\x00\x20\x00\x15\x00\x19\x00\x1a\x00\x13\x00\x00\x00\x1b\x00\x1c\x00\x1d\x00\x1e\x00\x38\x00\x00\x00\x00\x00\x20\x00\x15\x00\x19\x00\x1a\x00\x13\x00\x00\x00\x1b\x00\x1c\x00\x1d\x00\x68\x00\x00\x00\x00\x00\x00\x00\x20\x00\x15\x00\x19\x00\x1a\x00\x13\x00\x00\x00\x1b\x00\x1c\x00\x1d\x00\x66\x00\x00\x00\x00\x00\x00\x00\x20\x00\x15\x00\x19\x00\x1a\x00\x13\x00\x00\x00\x1b\x00\x1c\x00\x1d\x00\x5f\x00\x00\x00\x00\x00\x00\x00\x20\x00\x15\x00\x19\x00\x1a\x00\x13\x00\x00\x00\x1b\x00\x1c\x00\x1d\x00\x4a\x00\x00\x00\x00\x00\x00\x00\x20\x00\x15\x00\x19\x00\x1a\x00\x13\x00\x00\x00\x1b\x00\x1c\x00\x1d\x00\x39\x00\x00\x00\x00\x00\x00\x00\x20\x00\x15\x00\x19\x00\x1a\x00\x13\x00\x00\x00\x1b\x00\x1c\x00\x60\x00\x00\x00\x00\x00\x00\x00\x00\x00\x20\x00\x15\x00\x19\x00\x1a\x00\x13\x00\x00\x00\x1b\x00\x1c\x00\x61\x00\x00\x00\x00\x00\x00\x00\x00\x00\x20\x00\x15\x00\x19\x00\x1a\x00\x13\x00\x00\x00\x1b\x00\x1c\x00\x3a\x00\x00\x00\x12\x00\x00\x00\x13\x00\x20\x00\x15\x00\x19\x00\x1a\x00\x13\x00\x00\x00\x1b\x00\x48\x00\x56\x00\x15\x00\x00\x00\x00\x00\x00\x00\x20\x00\x15\x00\x19\x00\x1a\x00\x13\x00\x00\x00\x1b\x00\x3b\x00\x19\x00\x1a\x00\x13\x00\x00\x00\x3c\x00\x20\x00\x15\x00\x12\x00\x00\x00\x13\x00\x00\x00\x20\x00\x15\x00\x12\x00\x00\x00\x13\x00\x00\x00\x00\x00\x4f\x00\x15\x00\x00\x00\x00\x00\x00\x00\x00\x00\x32\x00\x15\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00"#++happyReduceArr = array (16, 56) [+ (16 , happyReduce_16),+ (17 , happyReduce_17),+ (18 , happyReduce_18),+ (19 , happyReduce_19),+ (20 , happyReduce_20),+ (21 , happyReduce_21),+ (22 , happyReduce_22),+ (23 , happyReduce_23),+ (24 , happyReduce_24),+ (25 , happyReduce_25),+ (26 , happyReduce_26),+ (27 , happyReduce_27),+ (28 , happyReduce_28),+ (29 , happyReduce_29),+ (30 , happyReduce_30),+ (31 , happyReduce_31),+ (32 , happyReduce_32),+ (33 , happyReduce_33),+ (34 , happyReduce_34),+ (35 , happyReduce_35),+ (36 , happyReduce_36),+ (37 , happyReduce_37),+ (38 , happyReduce_38),+ (39 , happyReduce_39),+ (40 , happyReduce_40),+ (41 , happyReduce_41),+ (42 , happyReduce_42),+ (43 , happyReduce_43),+ (44 , happyReduce_44),+ (45 , happyReduce_45),+ (46 , happyReduce_46),+ (47 , happyReduce_47),+ (48 , happyReduce_48),+ (49 , happyReduce_49),+ (50 , happyReduce_50),+ (51 , happyReduce_51),+ (52 , happyReduce_52),+ (53 , happyReduce_53),+ (54 , happyReduce_54),+ (55 , happyReduce_55),+ (56 , happyReduce_56)+ ]++happy_n_terms = 26 :: Int+happy_n_nonterms = 19 :: Int++happyReduce_16 = happySpecReduce_1 0# happyReduction_16+happyReduction_16 happy_x_1+ = case happyOutTok happy_x_1 of { (PT _ (T_Idents happy_var_1)) -> + happyIn19+ (Idents (happy_var_1)+ )}++happyReduce_17 = happySpecReduce_1 1# happyReduction_17+happyReduction_17 happy_x_1+ = case happyOutTok happy_x_1 of { (PT _ (T_PredId happy_var_1)) -> + happyIn20+ (PredId (happy_var_1)+ )}++happyReduce_18 = happySpecReduce_1 2# happyReduction_18+happyReduction_18 happy_x_1+ = case happyOutTok happy_x_1 of { (PT _ (T_FunctId happy_var_1)) -> + happyIn21+ (FunctId (happy_var_1)+ )}++happyReduce_19 = happySpecReduce_1 3# happyReduction_19+happyReduction_19 happy_x_1+ = case happyOut35 happy_x_1 of { happy_var_1 -> + happyIn22+ (PROGRAM (reverse happy_var_1)+ )}++happyReduce_20 = happySpecReduce_3 4# happyReduction_20+happyReduction_20 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut20 happy_x_1 of { happy_var_1 -> + case happyOut33 happy_x_2 of { happy_var_2 -> + happyIn23+ (ASentPred happy_var_1 happy_var_2+ )}}++happyReduce_21 = happySpecReduce_1 4# happyReduction_21+happyReduction_21 happy_x_1+ = happyIn23+ (TrueSent+ )++happyReduce_22 = happySpecReduce_1 4# happyReduction_22+happyReduction_22 happy_x_1+ = happyIn23+ (FalseSent+ )++happyReduce_23 = happySpecReduce_1 4# happyReduction_23+happyReduction_23 happy_x_1+ = case happyOut19 happy_x_1 of { happy_var_1 -> + happyIn23+ (IdentSent happy_var_1+ )}++happyReduce_24 = happySpecReduce_3 4# happyReduction_24+happyReduction_24 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut30 happy_x_1 of { happy_var_1 -> + case happyOut30 happy_x_3 of { happy_var_3 -> + happyIn23+ (ASentEq happy_var_1 happy_var_3+ )}}++happyReduce_25 = happySpecReduce_3 4# happyReduction_25+happyReduction_25 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut29 happy_x_2 of { happy_var_2 -> + happyIn23+ (happy_var_2+ )}++happyReduce_26 = happySpecReduce_2 5# happyReduction_26+happyReduction_26 happy_x_2+ happy_x_1+ = case happyOut24 happy_x_2 of { happy_var_2 -> + happyIn24+ (NegSent happy_var_2+ )}++happyReduce_27 = happySpecReduce_1 5# happyReduction_27+happyReduction_27 happy_x_1+ = case happyOut23 happy_x_1 of { happy_var_1 -> + happyIn24+ (happy_var_1+ )}++happyReduce_28 = happyReduce 6# 6# happyReduction_28+happyReduction_28 (happy_x_6 `HappyStk`+ happy_x_5 `HappyStk`+ happy_x_4 `HappyStk`+ happy_x_3 `HappyStk`+ happy_x_2 `HappyStk`+ happy_x_1 `HappyStk`+ happyRest)+ = case happyOut26 happy_x_2 of { happy_var_2 -> + case happyOut26 happy_x_4 of { happy_var_4 -> + case happyOut26 happy_x_6 of { happy_var_6 -> + happyIn25+ (IfSent happy_var_2 happy_var_4 happy_var_6+ ) `HappyStk` happyRest}}}++happyReduce_29 = happyReduce 4# 6# happyReduction_29+happyReduction_29 (happy_x_4 `HappyStk`+ happy_x_3 `HappyStk`+ happy_x_2 `HappyStk`+ happy_x_1 `HappyStk`+ happyRest)+ = case happyOut34 happy_x_2 of { happy_var_2 -> + case happyOut27 happy_x_4 of { happy_var_4 -> + happyIn25+ (LetSent happy_var_2 happy_var_4+ ) `HappyStk` happyRest}}++happyReduce_30 = happySpecReduce_1 6# happyReduction_30+happyReduction_30 happy_x_1+ = case happyOut24 happy_x_1 of { happy_var_1 -> + happyIn25+ (happy_var_1+ )}++happyReduce_31 = happySpecReduce_3 7# happyReduction_31+happyReduction_31 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut26 happy_x_1 of { happy_var_1 -> + case happyOut25 happy_x_3 of { happy_var_3 -> + happyIn26+ (AndSent happy_var_1 happy_var_3+ )}}++happyReduce_32 = happySpecReduce_3 7# happyReduction_32+happyReduction_32 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut26 happy_x_1 of { happy_var_1 -> + case happyOut25 happy_x_3 of { happy_var_3 -> + happyIn26+ (OrSent happy_var_1 happy_var_3+ )}}++happyReduce_33 = happySpecReduce_1 7# happyReduction_33+happyReduction_33 happy_x_1+ = case happyOut25 happy_x_1 of { happy_var_1 -> + happyIn26+ (happy_var_1+ )}++happyReduce_34 = happySpecReduce_3 8# happyReduction_34+happyReduction_34 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut27 happy_x_1 of { happy_var_1 -> + case happyOut26 happy_x_3 of { happy_var_3 -> + happyIn27+ (ImpSent happy_var_1 happy_var_3+ )}}++happyReduce_35 = happySpecReduce_1 8# happyReduction_35+happyReduction_35 happy_x_1+ = case happyOut26 happy_x_1 of { happy_var_1 -> + happyIn27+ (happy_var_1+ )}++happyReduce_36 = happySpecReduce_3 9# happyReduction_36+happyReduction_36 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut19 happy_x_1 of { happy_var_1 -> + case happyOut29 happy_x_3 of { happy_var_3 -> + happyIn28+ (DefSent happy_var_1 happy_var_3+ )}}++happyReduce_37 = happyReduce 4# 10# happyReduction_37+happyReduction_37 (happy_x_4 `HappyStk`+ happy_x_3 `HappyStk`+ happy_x_2 `HappyStk`+ happy_x_1 `HappyStk`+ happyRest)+ = case happyOut37 happy_x_2 of { happy_var_2 -> + case happyOut29 happy_x_4 of { happy_var_4 -> + happyIn29+ (ForallSent happy_var_2 happy_var_4+ ) `HappyStk` happyRest}}++happyReduce_38 = happyReduce 4# 10# happyReduction_38+happyReduction_38 (happy_x_4 `HappyStk`+ happy_x_3 `HappyStk`+ happy_x_2 `HappyStk`+ happy_x_1 `HappyStk`+ happyRest)+ = case happyOut37 happy_x_2 of { happy_var_2 -> + case happyOut29 happy_x_4 of { happy_var_4 -> + happyIn29+ (ExistsSent happy_var_2 happy_var_4+ ) `HappyStk` happyRest}}++happyReduce_39 = happySpecReduce_1 10# happyReduction_39+happyReduction_39 happy_x_1+ = case happyOut36 happy_x_1 of { happy_var_1 -> + happyIn29+ (happy_var_1+ )}++happyReduce_40 = happySpecReduce_3 11# happyReduction_40+happyReduction_40 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut21 happy_x_1 of { happy_var_1 -> + case happyOut33 happy_x_2 of { happy_var_2 -> + happyIn30+ (FunctTerm happy_var_1 happy_var_2+ )}}++happyReduce_41 = happySpecReduce_1 11# happyReduction_41+happyReduction_41 happy_x_1+ = case happyOut31 happy_x_1 of { happy_var_1 -> + happyIn30+ (happy_var_1+ )}++happyReduce_42 = happySpecReduce_1 12# happyReduction_42+happyReduction_42 happy_x_1+ = case happyOut19 happy_x_1 of { happy_var_1 -> + happyIn31+ (ConstVarTerm happy_var_1+ )}++happyReduce_43 = happySpecReduce_3 12# happyReduction_43+happyReduction_43 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut30 happy_x_2 of { happy_var_2 -> + happyIn31+ (happy_var_2+ )}++happyReduce_44 = happySpecReduce_1 13# happyReduction_44+happyReduction_44 happy_x_1+ = case happyOut37 happy_x_1 of { happy_var_1 -> + happyIn32+ (Terms happy_var_1+ )}++happyReduce_45 = happySpecReduce_0 14# happyReduction_45+happyReduction_45 = happyIn33+ ([]+ )++happyReduce_46 = happySpecReduce_1 14# happyReduction_46+happyReduction_46 happy_x_1+ = case happyOut32 happy_x_1 of { happy_var_1 -> + happyIn33+ ((:[]) happy_var_1+ )}++happyReduce_47 = happySpecReduce_3 14# happyReduction_47+happyReduction_47 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut32 happy_x_1 of { happy_var_1 -> + case happyOut33 happy_x_3 of { happy_var_3 -> + happyIn33+ ((:) happy_var_1 happy_var_3+ )}}++happyReduce_48 = happySpecReduce_0 15# happyReduction_48+happyReduction_48 = happyIn34+ ([]+ )++happyReduce_49 = happySpecReduce_1 15# happyReduction_49+happyReduction_49 happy_x_1+ = case happyOut28 happy_x_1 of { happy_var_1 -> + happyIn34+ ((:[]) happy_var_1+ )}++happyReduce_50 = happySpecReduce_3 15# happyReduction_50+happyReduction_50 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut28 happy_x_1 of { happy_var_1 -> + case happyOut34 happy_x_3 of { happy_var_3 -> + happyIn34+ ((:) happy_var_1 happy_var_3+ )}}++happyReduce_51 = happySpecReduce_0 16# happyReduction_51+happyReduction_51 = happyIn35+ ([]+ )++happyReduce_52 = happySpecReduce_3 16# happyReduction_52+happyReduction_52 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut35 happy_x_1 of { happy_var_1 -> + case happyOut29 happy_x_2 of { happy_var_2 -> + happyIn35+ (flip (:) happy_var_1 happy_var_2+ )}}++happyReduce_53 = happySpecReduce_1 17# happyReduction_53+happyReduction_53 happy_x_1+ = case happyOut27 happy_x_1 of { happy_var_1 -> + happyIn36+ (happy_var_1+ )}++happyReduce_54 = happySpecReduce_0 18# happyReduction_54+happyReduction_54 = happyIn37+ ([]+ )++happyReduce_55 = happySpecReduce_1 18# happyReduction_55+happyReduction_55 happy_x_1+ = case happyOut30 happy_x_1 of { happy_var_1 -> + happyIn37+ ((:[]) happy_var_1+ )}++happyReduce_56 = happySpecReduce_3 18# happyReduction_56+happyReduction_56 happy_x_3+ happy_x_2+ happy_x_1+ = case happyOut30 happy_x_1 of { happy_var_1 -> + case happyOut37 happy_x_3 of { happy_var_3 -> + happyIn37+ ((:) happy_var_1 happy_var_3+ )}}++happyNewToken action sts stk [] =+ happyDoAction 25# notHappyAtAll action sts stk []++happyNewToken action sts stk (tk:tks) =+ let cont i = happyDoAction i tk action sts stk tks in+ case tk of {+ PT _ (TS ")") -> cont 1#;+ PT _ (TS "=") -> cont 2#;+ PT _ (TS ".") -> cont 3#;+ PT _ (TS ")(") -> cont 4#;+ PT _ (TS ",") -> cont 5#;+ PT _ (TS ";") -> cont 6#;+ PT _ (TS "(") -> cont 7#;+ PT _ (TS "and") -> cont 8#;+ PT _ (TS "else") -> cont 9#;+ PT _ (TS "exists") -> cont 10#;+ PT _ (TS "false") -> cont 11#;+ PT _ (TS "forall") -> cont 12#;+ PT _ (TS "if") -> cont 13#;+ PT _ (TS "implies") -> cont 14#;+ PT _ (TS "in") -> cont 15#;+ PT _ (TS "let") -> cont 16#;+ PT _ (TS "not") -> cont 17#;+ PT _ (TS "or") -> cont 18#;+ PT _ (TS "then") -> cont 19#;+ PT _ (TS "true") -> cont 20#;+ PT _ (T_Idents happy_dollar_dollar) -> cont 21#;+ PT _ (T_PredId happy_dollar_dollar) -> cont 22#;+ PT _ (T_FunctId happy_dollar_dollar) -> cont 23#;+ _ -> cont 24#;+ _ -> happyError' (tk:tks)+ }++happyError_ tk tks = happyError' (tk:tks)++happyThen :: () => Err a -> (a -> Err b) -> Err b+happyThen = (thenM)+happyReturn :: () => a -> Err a+happyReturn = (returnM)+happyThen1 m k tks = (thenM) m (\a -> k a tks)+happyReturn1 :: () => a -> b -> Err a+happyReturn1 = \a tks -> (returnM) a+happyError' :: () => [Token] -> Err a+happyError' = happyError++pPROGRAM tks = happySomeParser where+ happySomeParser = happyThen (happyParse 0# tks) (\x -> happyReturn (happyOut22 x))++pSENT6 tks = happySomeParser where+ happySomeParser = happyThen (happyParse 1# tks) (\x -> happyReturn (happyOut23 x))++pSENT5 tks = happySomeParser where+ happySomeParser = happyThen (happyParse 2# tks) (\x -> happyReturn (happyOut24 x))++pSENT4 tks = happySomeParser where+ happySomeParser = happyThen (happyParse 3# tks) (\x -> happyReturn (happyOut25 x))++pSENT3 tks = happySomeParser where+ happySomeParser = happyThen (happyParse 4# tks) (\x -> happyReturn (happyOut26 x))++pSENT2 tks = happySomeParser where+ happySomeParser = happyThen (happyParse 5# tks) (\x -> happyReturn (happyOut27 x))++pDEF tks = happySomeParser where+ happySomeParser = happyThen (happyParse 6# tks) (\x -> happyReturn (happyOut28 x))++pSENT tks = happySomeParser where+ happySomeParser = happyThen (happyParse 7# tks) (\x -> happyReturn (happyOut29 x))++pTERM tks = happySomeParser where+ happySomeParser = happyThen (happyParse 8# tks) (\x -> happyReturn (happyOut30 x))++pTERM1 tks = happySomeParser where+ happySomeParser = happyThen (happyParse 9# tks) (\x -> happyReturn (happyOut31 x))++pTERMS tks = happySomeParser where+ happySomeParser = happyThen (happyParse 10# tks) (\x -> happyReturn (happyOut32 x))++pListTERMS tks = happySomeParser where+ happySomeParser = happyThen (happyParse 11# tks) (\x -> happyReturn (happyOut33 x))++pListDEF tks = happySomeParser where+ happySomeParser = happyThen (happyParse 12# tks) (\x -> happyReturn (happyOut34 x))++pListSENT tks = happySomeParser where+ happySomeParser = happyThen (happyParse 13# tks) (\x -> happyReturn (happyOut35 x))++pSENT1 tks = happySomeParser where+ happySomeParser = happyThen (happyParse 14# tks) (\x -> happyReturn (happyOut36 x))++pListTERM tks = happySomeParser where+ happySomeParser = happyThen (happyParse 15# tks) (\x -> happyReturn (happyOut37 x))++happySeq = happyDontSeq+++returnM :: a -> Err a+returnM = return++thenM :: Err a -> (a -> Err b) -> Err b+thenM = (>>=)++happyError :: [Token] -> Err a+happyError ts =+ Bad $ "syntax error at " ++ tokenPos ts ++ + case ts of+ [] -> []+ [Err _] -> " due to lexer error"+ _ -> " before " ++ unwords (map prToken (take 4 ts))++myLexer = tokens+{-# LINE 1 "templates/GenericTemplate.hs" #-}+{-# LINE 1 "templates/GenericTemplate.hs" #-}+{-# LINE 1 "<built-in>" #-}+{-# LINE 1 "<command line>" #-}+{-# LINE 1 "templates/GenericTemplate.hs" #-}+-- Id: GenericTemplate.hs,v 1.26 2005/01/14 14:47:22 simonmar Exp ++{-# LINE 28 "templates/GenericTemplate.hs" #-}+++data Happy_IntList = HappyCons Int# Happy_IntList++++++{-# LINE 49 "templates/GenericTemplate.hs" #-}++{-# LINE 59 "templates/GenericTemplate.hs" #-}++{-# LINE 68 "templates/GenericTemplate.hs" #-}++infixr 9 `HappyStk`+data HappyStk a = HappyStk a (HappyStk a)++-----------------------------------------------------------------------------+-- starting the parse++happyParse start_state = happyNewToken start_state notHappyAtAll notHappyAtAll++-----------------------------------------------------------------------------+-- Accepting the parse++-- If the current token is 0#, it means we've just accepted a partial+-- parse (a %partial parser). We must ignore the saved token on the top of+-- the stack in this case.+happyAccept 0# tk st sts (_ `HappyStk` ans `HappyStk` _) =+ happyReturn1 ans+happyAccept j tk st sts (HappyStk ans _) = + (happyTcHack j (happyTcHack st)) (happyReturn1 ans)++-----------------------------------------------------------------------------+-- Arrays only: do the next action++++happyDoAction i tk st+ = {- nothing -}+++ case action of+ 0# -> {- nothing -}+ happyFail i tk st+ -1# -> {- nothing -}+ happyAccept i tk st+ n | (n <# (0# :: Int#)) -> {- nothing -}++ (happyReduceArr ! rule) i tk st+ where rule = (I# ((negateInt# ((n +# (1# :: Int#))))))+ n -> {- nothing -}+++ happyShift new_state i tk st+ where new_state = (n -# (1# :: Int#))+ where off = indexShortOffAddr happyActOffsets st+ off_i = (off +# i)+ check = if (off_i >=# (0# :: Int#))+ then (indexShortOffAddr happyCheck off_i ==# i)+ else False+ action | check = indexShortOffAddr happyTable off_i+ | otherwise = indexShortOffAddr happyDefActions st++{-# LINE 127 "templates/GenericTemplate.hs" #-}+++indexShortOffAddr (HappyA# arr) off =+#if __GLASGOW_HASKELL__ > 500+ narrow16Int# i+#elif __GLASGOW_HASKELL__ == 500+ intToInt16# i+#else+ (i `iShiftL#` 16#) `iShiftRA#` 16#+#endif+ where+#if __GLASGOW_HASKELL__ >= 503+ i = word2Int# ((high `uncheckedShiftL#` 8#) `or#` low)+#else+ i = word2Int# ((high `shiftL#` 8#) `or#` low)+#endif+ high = int2Word# (ord# (indexCharOffAddr# arr (off' +# 1#)))+ low = int2Word# (ord# (indexCharOffAddr# arr off'))+ off' = off *# 2#++++++data HappyAddr = HappyA# Addr#+++++-----------------------------------------------------------------------------+-- HappyState data type (not arrays)++{-# LINE 170 "templates/GenericTemplate.hs" #-}++-----------------------------------------------------------------------------+-- Shifting a token++happyShift new_state 0# tk st sts stk@(x `HappyStk` _) =+ let i = (case unsafeCoerce# x of { (I# (i)) -> i }) in+-- trace "shifting the error token" $+ happyDoAction i tk new_state (HappyCons (st) (sts)) (stk)++happyShift new_state i tk st sts stk =+ happyNewToken new_state (HappyCons (st) (sts)) ((happyInTok (tk))`HappyStk`stk)++-- happyReduce is specialised for the common cases.++happySpecReduce_0 i fn 0# tk st sts stk+ = happyFail 0# tk st sts stk+happySpecReduce_0 nt fn j tk st@((action)) sts stk+ = happyGoto nt j tk st (HappyCons (st) (sts)) (fn `HappyStk` stk)++happySpecReduce_1 i fn 0# tk st sts stk+ = happyFail 0# tk st sts stk+happySpecReduce_1 nt fn j tk _ sts@((HappyCons (st@(action)) (_))) (v1`HappyStk`stk')+ = let r = fn v1 in+ happySeq r (happyGoto nt j tk st sts (r `HappyStk` stk'))++happySpecReduce_2 i fn 0# tk st sts stk+ = happyFail 0# tk st sts stk+happySpecReduce_2 nt fn j tk _ (HappyCons (_) (sts@((HappyCons (st@(action)) (_))))) (v1`HappyStk`v2`HappyStk`stk')+ = let r = fn v1 v2 in+ happySeq r (happyGoto nt j tk st sts (r `HappyStk` stk'))++happySpecReduce_3 i fn 0# tk st sts stk+ = happyFail 0# tk st sts stk+happySpecReduce_3 nt fn j tk _ (HappyCons (_) ((HappyCons (_) (sts@((HappyCons (st@(action)) (_))))))) (v1`HappyStk`v2`HappyStk`v3`HappyStk`stk')+ = let r = fn v1 v2 v3 in+ happySeq r (happyGoto nt j tk st sts (r `HappyStk` stk'))++happyReduce k i fn 0# tk st sts stk+ = happyFail 0# tk st sts stk+happyReduce k nt fn j tk st sts stk+ = case happyDrop (k -# (1# :: Int#)) sts of+ sts1@((HappyCons (st1@(action)) (_))) ->+ let r = fn stk in -- it doesn't hurt to always seq here...+ happyDoSeq r (happyGoto nt j tk st1 sts1 r)++happyMonadReduce k nt fn 0# tk st sts stk+ = happyFail 0# tk st sts stk+happyMonadReduce k nt fn j tk st sts stk =+ happyThen1 (fn stk tk) (\r -> happyGoto nt j tk st1 sts1 (r `HappyStk` drop_stk))+ where sts1@((HappyCons (st1@(action)) (_))) = happyDrop k (HappyCons (st) (sts))+ drop_stk = happyDropStk k stk++happyMonad2Reduce k nt fn 0# tk st sts stk+ = happyFail 0# tk st sts stk+happyMonad2Reduce k nt fn j tk st sts stk =+ happyThen1 (fn stk tk) (\r -> happyNewToken new_state sts1 (r `HappyStk` drop_stk))+ where sts1@((HappyCons (st1@(action)) (_))) = happyDrop k (HappyCons (st) (sts))+ drop_stk = happyDropStk k stk++ off = indexShortOffAddr happyGotoOffsets st1+ off_i = (off +# nt)+ new_state = indexShortOffAddr happyTable off_i+++++happyDrop 0# l = l+happyDrop n (HappyCons (_) (t)) = happyDrop (n -# (1# :: Int#)) t++happyDropStk 0# l = l+happyDropStk n (x `HappyStk` xs) = happyDropStk (n -# (1#::Int#)) xs++-----------------------------------------------------------------------------+-- Moving to a new state after a reduction+++happyGoto nt j tk st = + {- nothing -}+ happyDoAction j tk new_state+ where off = indexShortOffAddr happyGotoOffsets st+ off_i = (off +# nt)+ new_state = indexShortOffAddr happyTable off_i+++++-----------------------------------------------------------------------------+-- Error recovery (0# is the error token)++-- parse error if we are in recovery and we fail again+happyFail 0# tk old_st _ stk =+-- trace "failing" $ + happyError_ tk++{- We don't need state discarding for our restricted implementation of+ "error". In fact, it can cause some bogus parses, so I've disabled it+ for now --SDM++-- discard a state+happyFail 0# tk old_st (HappyCons ((action)) (sts)) + (saved_tok `HappyStk` _ `HappyStk` stk) =+-- trace ("discarding state, depth " ++ show (length stk)) $+ happyDoAction 0# tk action sts ((saved_tok`HappyStk`stk))+-}++-- Enter error recovery: generate an error token,+-- save the old token and carry on.+happyFail i tk (action) sts stk =+-- trace "entering error recovery" $+ happyDoAction 0# tk action sts ( (unsafeCoerce# (I# (i))) `HappyStk` stk)++-- Internal happy errors:++notHappyAtAll = error "Internal Happy error\n"++-----------------------------------------------------------------------------+-- Hack to get the typechecker to accept our action functions+++happyTcHack :: Int# -> a -> a+happyTcHack x y = y+{-# INLINE happyTcHack #-}+++-----------------------------------------------------------------------------+-- Seq-ing. If the --strict flag is given, then Happy emits +-- happySeq = happyDoSeq+-- otherwise it emits+-- happySeq = happyDontSeq++happyDoSeq, happyDontSeq :: a -> b -> b+happyDoSeq a b = a `seq` b+happyDontSeq a b = b++-----------------------------------------------------------------------------+-- Don't inline any functions from the template. GHC has a nasty habit+-- of deciding to inline happyGoto everywhere, which increases the size of+-- the generated parser quite a bit.+++{-# NOINLINE happyDoAction #-}+{-# NOINLINE happyTable #-}+{-# NOINLINE happyCheck #-}+{-# NOINLINE happyActOffsets #-}+{-# NOINLINE happyGotoOffsets #-}+{-# NOINLINE happyDefActions #-}++{-# NOINLINE happyShift #-}+{-# NOINLINE happySpecReduce_0 #-}+{-# NOINLINE happySpecReduce_1 #-}+{-# NOINLINE happySpecReduce_2 #-}+{-# NOINLINE happySpecReduce_3 #-}+{-# NOINLINE happyReduce #-}+{-# NOINLINE happyMonadReduce #-}+{-# NOINLINE happyGoto #-}+{-# NOINLINE happyFail #-}++-- end of Happy Template.
+ PrintHOL.hs view
@@ -0,0 +1,808 @@+{-+# Prettyprinter for beautifHOL, a HOL prettyprinter+# Based on the paper found at http://www.cs.indiana.edu/~lepike/pub_pages/pphol.html+# Lee Pike <lee-pike-@-gma-il-.com> (remove dashes)+# Copyright 2008++# This file is part of beautifHOL.+# BSD3.+-}++-- | Module handles the actual pretty-printing.+module PrintHOL where++-- Library imports --+-- We use the reader monad to pass the pretty-print environment around.+import Control.Monad.Reader+import Data.List++-- Program imports.+import AbsHOL+import Char+import ConfigHOL -- Constants are defined here++-- |Possible flags to the program.+type Flags = [String]++-- |List of possible arguments. Do not modify the ordering of this list (add new+-- flags to the end).+arglst :: Flags+arglst = ["--silent", "--notree", "--showinput", "--nolabels", "--help", "--f"]++-- |Defne flags here so they can be easily renamed.+silentArg, notreeArg, showinputArg :: String+silentArg = arglst !! 0+notreeArg = arglst !! 1+showinputArg = arglst !! 2+nolabelsArg = arglst !! 3+helpArg = arglst !! 4+fileArg = arglst !! 5++-- |The major datatype passed around holding the pretty-printing state.+data Env = + EnvDT { label :: Int -- ^ Line label+ , newLn :: Bool -- ^ If true, then we're on a new line. Note: binary+ -- operators are always on a new line; this tells us+ -- whether some other sentence or term is on its own+ -- line.+ , unOp :: Int -- ^ How many negations we've seen+ , absInd :: Int -- ^ Indentation after label stuff. Where the line begins.+ , relInd :: Int -- ^ Relative indentation (from last operator)+ , defaultInd :: Int -- ^ Default indendtation (up to the longest label of a+ -- formula)+ , prevSameBinOp :: Bool -- ^ Was this binary operator the argument to the+ -- same binary operator? (If so, we don't indent.)+ , splitArgs :: Bool -- ^ True: put args to functions & predicates on their+ -- own line. The number is the length of the+ -- identifier, plus other args and identifiers, up to+ -- this term.+ , innerTerm :: Bool -- ^ Is this term inside another term? (The only case+ -- in which it is not is if it is an argument to = .)+ , showLabels :: Bool -- ^ Show labels? This is only for whether labels+ -- should currently be suppressed (e.g., in let+ -- defs). For no labels at all, we set a global+ -- flag.+ , noLabels :: Bool -- ^ Are we showing labels at all (or are they globally suppressed)?++ }+++-- |The initial environment.+mkinitEnv :: Flags -> Env+mkinitEnv fs = EnvDT 1 True 0 0 0 0 False False False True getLabelFlag+ where getLabelFlag = not $ elem nolabelsArg fs++-- |"Resets" the environment except for the default indentation (from the length of+-- the longest label).+resetEnv :: Env -> Env+resetEnv env = EnvDT 1 True 0 0 0 (defaultInd env) False False False (showLabels env) (noLabels env)++printTree :: Print a => a -> Flags -> String+printTree t fs = render $ runReader (prt t) (mkinitEnv fs)++type Doc = [ShowS] -> [ShowS]++doc :: ShowS -> Doc+doc = (:)++-- |Takes the final Doc and returns the output. Ideally, the Doc should be considered+-- the logical structure of the pretty-printed formula and the render assigns+-- concrete syntax.+render :: Doc -> String+render d = rend 0 (map ($ "") $ d []) "" + where rend i ss = + case ss of+ -- For curried args.+ "( " : ts -> showChar '(' . spaces 1 . rend i ts+ t : "(" :ts -> showString t . showChar '(' . rend i ts+ ";" :ts -> + showString preStr . new . showString postStr . rend i ts+ -- Another hack for curried preds where the pred is one char long.+ -- If there's a space, a 2nd gets added by rend; if there's no+ -- space, nothing gets added. So I can only have 0 or 2 spaces.+ "\n" : "( " :ts -> new . spaces 1 . showChar '(' . spaces 1 . rend i ts+ -- I need this: I don't want a space after \n because it'll carry+ -- to the next line.+ "\n" :ts -> new . rend i ts+ t : "." :ts -> showString t . space quantVarsMark . rend i ts+ -- Hack: The comma wasn't picked up in the case of odd number of+ -- parens in a row. e.g., Foo(h(g(f(a))), 4 );+ t : ")" :"," :ts -> + showString t . spaces 1 . showChar ')' . space argSepStr . rend i ts+ t : ")" :ts -> + showString t . spaces 1 . showChar ')' . spaces 1 . rend i ts+ t : "," :ts -> showString t . space argSepStr . rend i ts+ "" :ts -> rend i ts + t :ts -> showString t . spaces 1 . rend i ts + _ -> id+ new = showChar brkChar + space t = showString t . (\s -> if null s then "" else (' ':s))++concatS :: [ShowS] -> ShowS+concatS = foldr (.) id++concatD :: [Doc] -> Doc+concatD = foldr (.) id++replicateS :: Int -> ShowS -> ShowS+replicateS n f = concatS (replicate n f)++spaces :: Int -> ShowS+spaces n = replicateS n (showString spaceStr)++type EnvT = Reader Env Doc++prtList :: Print a => [a] -> [Env] -> [Doc]+prtList [] _ = []+prtList ls envs = + let zp = zip envs ls + in map (\(env,a) -> runReader (prt a) env) zp+++-- |The Print class. Each constructor of the grammar instantiates this. The prt+-- function tells how to pretty-print each construct.+class Print a + where prt :: a -> EnvT++instance Print Char + where prt s = return $ doc (showChar '\'' . mkEsc '\'' s . showChar '\'')++-- |Escape characters for rendering.+mkEsc :: Char -> Char -> ShowS+mkEsc q s = case s of+ _ | s == q -> showChar '\\' . showChar s+ '\\'-> showString "\\\\"+ '\n' -> showString "\\n"+ '\t' -> showString "\\t"+ _ -> showChar s++instance Print Integer where+ prt x = return $ doc (shows x)++instance Print Double where+ prt x = return $ doc (shows x)++instance Print Int where+ prt x = return $ doc (shows x)++instance Print Idents where+ prt (Idents i) = return $ doc (showString i)++instance Print PredId where+ prt (PredId i) = return $ doc (showString i)++instance Print FunctId where+ prt (FunctId i) = return $ doc (showString i)++maxLabels :: [SENT] -> Env -> [Env]+maxLabels sents env = + if (noLabels env) --getLabelFlag env --(showLabels env) + then map (\x -> env {defaultInd = x + 1}) $ map countBins sents + else map (\_ -> env ) sents+ where+ -- Sets up how far to indent the formula, to give space for labels.+ countBins s = + case s of+ AndSent s0 s1 -> binCnt s0 s1+ OrSent s0 s1 -> binCnt s0 s1+ ImpSent s0 s1 -> binCnt s0 s1+ ASentEq _ _ -> 1+ ForallSent _ s0 -> unCnt s0+ ExistsSent _ s0 -> unCnt s0+ IfSent s0 s1 s2 -> triCnt s0 s1 s2+ LetSent _ s0 -> countBins s0+ NegSent s0 -> if negCnt s0 then unCnt s0 else countBins s0+ _ -> 0+ where triCnt s0 s1 s2 = 1 + (max (countBins s0) $ max (countBins s1) (countBins s2))+ binCnt s0 s1 = 1 + max (countBins s0) (countBins s1)+ unCnt s0 = 1 + countBins s0+ -- See if there's ever another label to be applied. If so, we+ -- count the not label; o/w, we don't. (E.g., not forall+ -- x. P()) shouldn't count forall label.)+ negCnt s = case s of+ AndSent _ _ -> True+ OrSent _ _ -> True+ ImpSent _ _ -> True+ ASentEq _ _ -> True+ IfSent _ _ _ -> True+ LetSent _ _ -> True+ ForallSent _ s0 -> negCnt' s0+ ExistsSent _ s0 -> negCnt' s0+ NegSent s0 -> negCnt' s0+ _ -> False+ negCnt' s = case s of+ AndSent _ _ -> True+ OrSent _ _ -> True+ ImpSent _ _ -> True+ ASentEq _ _ -> True+ IfSent _ _ _ -> True+ LetSent _ _ -> True+ ForallSent _ _ -> True+ ExistsSent _ _ -> True+ NegSent s0 -> negCnt s0+ _ -> False+++-- |Takes the list of sentences in the program and returns a corresponding list of+-- initial environments in which the defaultInd (i.e., the length of the longest+-- label for that sentence) is set.+instance Print PROGRAM where+ prt e = + case e of+ PROGRAM sents -> + do + env <- ask+ return $ + concatD $ + intersperse + (doc $ showString ";") $+ (doc $ showString preStr):(prtList sents (maxLabels sents env))++instance Print TERM where+ prt e = do+ env <- ask+ let initInd = if innerTerm env then doc $ spaces 0 else simpInd env+ in return $ case e of+ FunctTerm functid ((Terms terms):termsLst) -> + concatD $ initInd:+ (runReader (prt functid) env):+ (intersperseTerms env' terms) ++ + (prtList termsLst (repeat env''))+ where env' = env { splitArgs = newSplit terms + , absInd = absIndUp + env + (functIdLen functid) + , innerTerm = True+ }+ i = if (innerTerm env) then 1+ else 2+ env'' = env {absInd = + (absInd env) + + (functIdLen functid) - i}+ ConstVarTerm idents -> concatD [ initInd+ , runReader (prt idents) env]+ _ -> concatD [] -- Should be unreachable.+++instance Print TERMS where+ prt e = do+ env <- ask+ return $ case e of+ Terms terms -> + concatD $ (nextLnArgs env):+ (doc $ showString "( "):+ (intersperseTerms env' terms)+ where a = absInd env+ env' = env { splitArgs = newSplit terms + , innerTerm = True+ , absInd = a + 2+ }++-- |For a list of terms, we intersperse the argument separator string.+intersperseTerms :: Env -> [TERM] -> [Doc]+intersperseTerms env terms = + intersperse + (argSeparators env) + (prtList terms $ repeat env)+++ [doc $ showString ")"]++instance Print DEF where+ prt def = do+ env <- ask+ return $ + case def of + DefSent ids sent ->+ concatD $ [ runReader (prt ids) env+ , doc $ showString eqStr+ , runReader (prt sent) $ letEnv env varEqsLn 0 False+ ]+ where varEqsLn = + (length $ render $ runReader (prt ids) env) + (length eqStr)++instance Print SENT where+ prt e = do + env <- ask+ return $ + case e of+ IdentSent idents -> let initInd = if innerTerm env then doc $ spaces 0 else simpInd env+ in concatD [ initInd+ , runReader (prt idents) env]+ ASentPred predid ((Terms terms):termsLst) -> + concatD $ (simpInd env):+ (runReader (prt predid) env):+ (intersperseTerms env' terms) +++ (prtList termsLst (repeat env''))+ where predLen = predIdLen predid+ newAbs = absIndUp env predLen + env' = env { splitArgs = newSplit terms+ , absInd = newAbs+ , innerTerm = True}+ env'' = env {absInd = (absInd env) + predLen - 2}++ TrueSent -> concatD [ simpInd env + , doc (showString trueStr)+ ]+ FalseSent -> concatD [ simpInd env + , doc (showString falseStr)+ ]+ ASentEq term0 term -> + concatD [runReader (prt term0) env1+ , binaryOpInd env eqStr+ , runReader (prt term) env2+ ]+ where env1 = binEnv1 env eqTab False 0 -- arbitrary label (suppressed for eq)+ env2 = binEnv2 env eqTab False 1 -- arbitrary label (suppressed for eq)++ ForallSent vars sent -> + quantDoc env vars sent forallStr forallTab forallSent++ ExistsSent vars sent -> + quantDoc env vars sent existsStr existsTab existsSent++ NegSent sent -> + concatD [ quantOpInd env negStr + , runReader (prt sent) e+ ]+ where e = notEnv env negTab True++ AndSent sent0 sent -> + binOpDoc env sent0 sent andStr andTab andSent + OrSent sent0 sent -> + binOpDoc env sent0 sent orStr orTab orSent + ImpSent sent0 sent -> + binOpDoc env sent0 sent impStr impTab impSent + IfSent sent0 sent1 sent2 ->+ ifDoc env sent0 sent1 sent2+ LetSent defs sent ->+ letDoc env defs sent+ _ -> concatD [] -- Should be unreachable.+++-------------------------------------------------------------+-- Helper functions+-------------------------------------------------------------++-- |Returns the String to bring for binary operator sentences.+binOpDoc :: Env -> SENT -> SENT -> String -> Int -> (SENT -> Bool) -> Doc+binOpDoc env sent0 sent binOpStr binOpTab binOpTest =+ concatD [runReader (prt sent0) env1 + , binaryOpInd env binOpStr+ , runReader (prt sent) env2+ ]+ where env1 = binEnv1 env binOpTab (binOpTest sent0) binOpLabel1+ env2 = binEnv2 env binOpTab (binOpTest sent) binOpLabel2+ -- what are the labels?+ binOpLabel1 = case binOpStr of+ _ | binOpStr == andStr -> 1+ | binOpStr == orStr || binOpStr == impStr -> 3+ | otherwise -> 0 -- should be unreachableb+ binOpLabel2 = case binOpStr of+ _ | binOpStr == andStr -> 2+ | binOpStr == orStr || binOpStr == impStr -> 4+ | otherwise -> 0 -- should be unreachableb++-- |Returns the String to print for a forall/exists sentence.+quantDoc :: Env -> [TERM] -> SENT -> String -> Int -> (SENT -> Bool) -> Doc+quantDoc env vars sent quantStr quantTab quantTest =+ concatD $ [ quantOpInd env quantStr+ , concatD $ + intersperse + (argSeparators env)+ (prtList vars (repeat ((resetEnv env) {innerTerm = True})))+ , doc (showString quantVarsMark)+ , doc (showString brkStr)+ , runReader (prt sent) env1+ ]+ where env1 = quantEnv1 env quantTab (quantTest sent) quantLabel+ quantLabel = case quantStr of + _ | quantStr == forallStr -> 8+ | quantStr == existsStr -> 9+ | otherwise -> 0 --should be unreachable++-- |Returns the string to print for if-then-else sentences.+ifDoc :: Env -> SENT -> SENT -> SENT -> Doc+ifDoc env sent0 sent1 sent2 =+ concatD $ [ quantOpInd env ifStr+ , runReader (prt sent0) e1+ , doc (showString brkStr)+ , quantOpInd e2 thenStr + , runReader (prt sent1) e3+ , doc (showString brkStr)+ , quantOpInd e2 elseStr+ , runReader (prt sent2) e4+ ]+ where l = ifTab+ e1 = ifEnv env l (l - (length ifStr)) 5+ e3 = ifEnv env l (l - (length thenStr)) 6+ e4 = ifEnv env l (l - (length elseStr)) 7+ e2 = env {newLn = True}++-- |New environment for the second argument to a binary operator.+ifEnv :: Env + -> Int -- ^ length of ifTab + -> Int -- ^ extra space needed because "if" is shorter than "then" and "else"+ -> Int -- ^ operand label+ -> Env+ifEnv env tab n i = EnvDT + (numApp (showLabels env) (label env) i)+ False+ newUnOp+ newAbsInd+ (n-1)+ (defaultInd env)+ False+ False+ False+ (showLabels env)+ (noLabels env)+ where newUnOp = 0+ newAbsInd = upIndUnOp env tab++-- |Returns the doc for let [defs] in SENT. [DEF] should be nonempty.+letDoc :: Env -> [DEF] -> SENT -> Doc+letDoc env defs sent = + concatD $ (quantOpInd env letStr):+ letdefs+ ++ [ doc $ showString brkStr+ , quantOpInd e1 inStr + , runReader (prt sent) e2+ ]+ where n = nextLnArgs e4+ m = letTab - (length inStr)+ letdefs = intersperse n (prtList defs $ repeat e3)+ e2 = letEnv env letTab m True+ e1 = env {newLn = True}+ e3 = letEnv env letTab m False+ e4 = env { absInd = (absInd env) + letTab }++letEnv :: Env + -> Int -- ^ length of letTab+ -> Int -- ^ extra space needed because "let" is longer than "in"+ -> Bool -- ^ whether labels should be shown or suppressed+ -> Env+letEnv env tab n l = EnvDT + --(numApp (showLabels env) (label env) 1)+ (label env)+ False+ 0+ newAbsInd+ (n-1)+ (defaultInd env)+ False+ False+ False+ l+ (noLabels env)+ where newAbsInd = upIndUnOp env tab+++notEnv :: Env -> Int -> Bool -> Env+notEnv env tab l = EnvDT + (numApp (showLabels env) (label env) 0)+ False+ ((unOp env) + 1)+ newAbsInd+ 0+ (defaultInd env)+ False+ False+ False+ l+ (noLabels env)+ where newAbsInd = upIndUnOp env tab++-- |Takes an environment and returns separators (default is commas) for between+-- lists of variables, terms, etc. and if necessary, it inserts linebreak+-- commands. The Doc returned is interspersed into the list of of variables or+-- terms.+argSeparators :: Env -> Doc+argSeparators env =+ concatD [ doc $ showString argSepStr+ , sepStr]+ where sepStr = if splitArgs env + then nextLnArgs env+ else doc $ spaces 0++-- |Puts either args or curried arguments on the next line with the right indenting.+nextLnArgs :: Env -> Doc+nextLnArgs env =+ doc $ concatS [ showString brkStr+ , computeSpcs + (noLabels env) --(showLabels env) + (defaultInd env - 1) + (absInd env)+ ]+++-------------------------------------------------------------+-- Term Helper functions+-------------------------------------------------------------++-- |Are the args long enough that we have to split+-- them, or is there a curried function that is a+-- term?+newSplit :: [TERM] -> Bool+newSplit terms = (maxArgLen <= (maxArg terms))+ || (curriedTerm terms)+ +curriedTerm :: [TERM] -> Bool+curriedTerm terms = + case terms of+ [] -> False+ t:ts -> case t of+ FunctTerm _ ((Terms _):termsLst) ->+ if null termsLst+ then curriedTerm ts+ else True+ ConstVarTerm _ -> curriedTerm ts++maxArg :: [TERM] -> Int+maxArg terms = + let mlst = map + (\_ -> foldl max 0 (map (\x -> termStrLens x) terms))+ terms+ in maximum mlst+ +termStrLens :: TERM -> Int+termStrLens term = + case term of+ FunctTerm functid termsLst -> sumFunctTerms functid (maxTerm functid termsLst)+ ConstVarTerm (Idents i) -> length i + where maxTerm id ts = + maximumBy + (\x y -> compare + (sumFunctTerms id x)+ (sumFunctTerms id y))+ ts ++ sumFunctTerms :: FunctId -> TERMS -> Int+ sumFunctTerms functid termsLst = functIdLen + termsSum + where functIdLen = case functid of FunctId i -> length i+ terms = case termsLst of Terms ts -> ts+ termsSum = foldl (+) 0 (map (\x -> termStrLens x) terms) + sepLens+ sepLens = 0+-------------------------------------------------------------++-------------------------------------------------------------+-- Labeling Helper functions+-------------------------------------------------------------++numApp :: Bool -- ^ are labels currently suppressed (e.g., in let...in statements). + -> Int -- ^ depth+ -> Int -- ^ which operand+ -> Int +numApp b n m = if b+ then n * 10 + m + else n++showLabel :: Env -> ShowS+showLabel env = if noLabels env+ then if showLabels env+ then showString $ show $ label env+ else spaces $ (defaultInd env) - 1 + else spaces 0++predIdLen :: PredId -> Int+predIdLen (PredId i) = length i++functIdLen :: FunctId -> Int+functIdLen (FunctId i) = length i++-- |Absolute indentation (for splitting across lines and not splitting).+absIndUp :: Env -> Int -> Int+absIndUp env predlen = + -- indentation when a predicate is split across lines.+-- if split then predlen + initAbs else initAbs+ predlen + initAbs + where initAbs = if innerTerm env then (absInd env) + 1 else absInd env++andSent :: SENT -> Bool+andSent s = case s of+ AndSent _ _ -> True+ _ -> False++orSent :: SENT -> Bool+orSent s = case s of+ OrSent _ _ -> True+ _ -> False++impSent :: SENT -> Bool+impSent s = case s of+ ImpSent _ _ -> True+ _ -> False++forallSent :: SENT -> Bool+forallSent s = case s of+ ForallSent _ _ -> True+ _ -> False++existsSent :: SENT -> Bool+existsSent s = case s of+ ExistsSent _ _ -> True+ _ -> False+-------------------------------------------------------------++-------------------------------------------------------------+-- Binary operator helper functions+-------------------------------------------------------------++-- |Returns the new environment for the first argument to a binary operator.+binEnv1 :: Env + -> Int+ -> Bool -- ^ is the same operator as we've just seen, so no indentation+ -> Int -- ^ label+ -> Env+binEnv1 env tab b l = EnvDT + (numApp (showLabels env) (label env) l)+ (newLn env)+ 0 --newunOp+ newabsInd+ newRelind+ (defaultInd env)+ b+ False+ False+ (showLabels env)+ (noLabels env)+ where newabsInd = if b then absInd env else upIndUnOp env tab+ newRelind = relPrevOp --if b then relInd env else relPrevOp + -- redundant code?+ relPrevOp = if prevSameBinOp env+ then relInd env+ else relUpdate (relInd env) tab++-- |Returns the new environment for second argument to a binary operator (see documentation for binEnv1).+binEnv2 :: Env -> Int -> Bool -> Int -> Env+binEnv2 env tab b l = EnvDT + (numApp (showLabels env) (label env) l)+ False+ 0 --newUnOp+ newAbsInd+ 0+ (defaultInd env)+ b+ False+ False+ (showLabels env)+ (noLabels env)+ where newAbsInd = if b then absInd env else upIndUnOp env tab+-------------------------------------------------------------++ ++-------------------------------------------------------------+-- Sentence Helper functions+-------------------------------------------------------------++-- |If the next sentence to parse is a binary operator sentence, then don't do anything+-- the "not" will printed with the next sentence. Otherwise, just do the indenting.+checkUnOpArg :: SENT -> String -> Doc+checkUnOpArg e s = if checkBinOp e then doc $ spaces 0+ else if checkQuant e then doc $ spaces 0+ else doc $ showString s++-- |True if there is a sequence of "not sentences" followed by a quantified+-- sentence.+checkQuant :: SENT -> Bool+checkQuant e = case e of + NegSent e1 -> checkQuant e1+ ExistsSent _ _ -> True+ ForallSent _ _ -> True+ _ -> False+ +-- |True if there is a sequence of negated sentences followed by a "binary operator+-- sentence".+checkBinOp :: SENT -> Bool+checkBinOp e = case e of+ NegSent e1 -> checkBinOp e1+ AndSent _ _ -> True+ OrSent _ _ -> True+ ImpSent _ _ -> True+ _ -> False++negInd :: Env -> SENT -> Doc+negInd env e = if checkBinOp e then doc $ spaces 0 + else if checkQuant e then doc $ spaces 0 + else simpInd env+-------------------------------------------------------------+++-- |New environment for an argument to a quantifier.+quantEnv1 :: Env -> Int -> Bool -> Int -> Env+quantEnv1 env tab b l = EnvDT + (numApp (showLabels env) (label env) l) + True+ 0+ newAbsInd+ newRelInd+ (defaultInd env)+ b+ False+ False+ (showLabels env)+ (noLabels env)+ where newAbsInd = if b then absInd env else upIndUnOp env tab+ newRelInd = if b then relInd env else relUpdate (relInd env) tab+ +-- |If the env has not been indented yet (i==0), then just update according to the+-- operator's tab width (j); otherwise add the old relative indent, the new tab, and+-- an extra space between the strings.+relUpdate :: Int + -> Int -- ^ i==0 menas the environment hasn't been indented yet.+ -> Int -- ^ +relUpdate i j = if i==0 then j else i+j+1++-- |Indentation for binary operator sentences.+simpInd :: Env -> Doc+simpInd env = doc $ concatS [indent (env {absInd=((absInd env)-1)})] where+ indent env = if (unOp env > 0) then spaces 0 -- just saw a "not"+ else if newLn env + -- binary operator, on new line+ then computeSpcs+ (noLabels env) --(showLabels env) + (defaultInd env - 1) + (absInd env)+ -- after binary operator, either right after or arbitrarily after + else spaces (relInd env) +++-- |Returns an absolute indentation depending on the operator size and whether+-- there is a preceding unary operator. Does not indent for operators of the same+-- kind (so there's no precedence to record).+upIndUnOp :: Env + -> Int -- ^ operator size+ -> Int +upIndUnOp env t = 1 + (absInd env) + t -- + (unOp env) -- + negTab * (unOp env)++-- If we're inside a "not" sentence, then put this sentence right after the not;+-- otherwise indent it by ind+quantOpInd :: Env -> String -> Doc+quantOpInd env op = + doc $ concatS [ putLabel + , quantIndent +-- , makeNots (unOp env) (prevSameBinOp env)+ , showString op+ ] + where putLabel = if newLn env + then showLabel env + else spaces 0+ quantIndent = if newLn env -- If there's a label, I know newLn=True.+ then labelInd env+ -- Subtract out all the neg tabs: NegSent adds to + -- relInd, but those should count for sentences on the+ -- same line as the neg.+ else spaces $ rel - ((negTab + 1) * unOp env)+ rel = let r = relInd env+ in if r == 0 then r else r + 1++-- |If we're inside a "not" sentence, then put this sentence right after the "not"s.+binaryOpInd :: Env -> String -> Doc+binaryOpInd env op = + doc $ concatS [ showString brkStr+ , showLabel env+ , labelInd env+ , showString op+ ]++-- |Compute spaces from beginning of line. +computeSpcs :: Bool -- ^ are there labels+ -> Int -- ^ spaces before separator+ -> Int -- ^ spaces after separator+ -> ShowS+computeSpcs b i j = + showString (concat $ (replicate i spaceStr)+ ++ sep ++ + (replicate k spaceStr))+ where sep = if b then [labelSepStr] else []+ k = if b then j + 1 + else j ++-- |Returns the indentation for directly after a label.+labelInd :: Env -> ShowS+labelInd env = + computeSpcs (noLabels env) --(showLabels env) + ((defaultInd env) - labelLen - 1) (absInd env)+ where labelLen = if (noLabels env) --showLabels env+ then length $ show $ label env+ else 0+
+ SkelHOL.hs view
@@ -0,0 +1,65 @@+module SkelHOL where++-- Haskell module generated by the BNF converter++import AbsHOL+import ErrM+type Result = Err String++failure :: Show a => a -> Result+failure x = Bad $ "Undefined case: " ++ show x++transIdents :: Idents -> Result+transIdents x = case x of+ Idents str -> failure x+++transPredId :: PredId -> Result+transPredId x = case x of+ PredId str -> failure x+++transFunctId :: FunctId -> Result+transFunctId x = case x of+ FunctId str -> failure x+++transPROGRAM :: PROGRAM -> Result+transPROGRAM x = case x of+ PROGRAM sents -> failure x+++transDEF :: DEF -> Result+transDEF x = case x of+ DefSent idents sent -> failure x+++transSENT :: SENT -> Result+transSENT x = case x of+ ASentPred predid termss -> failure x+ TrueSent -> failure x+ FalseSent -> failure x+ IdentSent idents -> failure x+ ASentEq term0 term -> failure x+ NegSent sent -> failure x+ IfSent sent0 sent1 sent -> failure x+ AndSent sent0 sent -> failure x+ OrSent sent0 sent -> failure x+ ImpSent sent0 sent -> failure x+ LetSent defs sent -> failure x+ ForallSent terms sent -> failure x+ ExistsSent terms sent -> failure x+++transTERM :: TERM -> Result+transTERM x = case x of+ FunctTerm functid termss -> failure x+ ConstVarTerm idents -> failure x+++transTERMS :: TERMS -> Result+transTERMS x = case x of+ Terms terms -> failure x+++
beautifHOL.cabal view
@@ -1,5 +1,5 @@ Name: beautifHOL-Version: 0.1+Version: 0.10 Cabal-Version: >= 1.2 License: GPL License-file: LICENSE@@ -15,7 +15,7 @@ Maintainer: Lee Pike <leepike@gmail.com> Category: Text Homepage: http://www.cs.indiana.edu/~lepike/pub_pages/holpp.html-extra-source-files: README+extra-source-files: README AbsHOL.hs ConfigHOL.hs DocHOL.tex DOCHOL.pdf ErrM.hs HOL.cf LexHOL.hs ParHOL.hs PrintHOL.hs SkelHOL.hs examples.txt Executable beautifHOL Main-is: TestHOL.hs Build-Depends: haskell98, mtl, array, base
+ examples.txt view
@@ -0,0 +1,177 @@++-- Not a valid sentence-- True can't be an arg to equals.+-- foo(bar, bar)(bar) = true; +++(true and (not false and (true or false))) and (true and (false and (true or false)))+;+++(true and (not false implies (true or false))) or (true implies (false and (true or false))) ;++P(g) ;++ Pred(g );++ PRED(1);++-- Pred4 (g,a, 4 ); fails+ -- Foo (g a); fails+ -- Foo (g, a, ); fails++-- -- f(a) ; fails -- a function is a term, not a sentence!++a = 4 ;++bb = e ;++not P(1);++ forall a. exists b. a=b and (P(g) and true) or false;+++P(1) and G(2);+++ forall b,a . true;++not (forall a . true);+-- not forall a . true; won't parse -- "not" binds tighter than quantifiers++not not not (true or false);+++((forall d , b, c . a = b and (exists b ,f. P(b, c, g) or f(g)=b)) or not not (forall e. exists b. a=b and (P(g)(f,g(a, foo(bar, bar, bar), a)) and (not (not true )))) or false);++not true;++true or (not (P() and Q()) or false);++true or (P() and Q() or false);++true or (not not Z() or (not not (forall x. P(x)) and Q() or false));+true or (Z() or ((forall x. P(x)) and Q() or false));++true or (Z() or ((forall x. P(x) and Q(x)) and Q() or false));++true or (Z() or ((forall x. x = z) and Q() or false));++true or (Z() or ((P(x)) and Q() or false));++true or ((forall a. true) or (not not P() and Q() or false));++not not (P(1) and G(2));+++not not (forall a,b. not not not (forall c. not true));+++not (true and (Pred(foobarfoobarfoobarfoobar, bar, zoo) and false));++Foo(g(f(foobarfoobarfoo, a, b,c)), 4 );++P(asdflkasjdflkjsdf, asdlfkjasdf);+++true or P(f(g(3,4)),e(2,f(g(asdflksadfajsdfasdlfk,y(asldkfjasldkfjsasdfadasf,asdlfkjasdlfkjdfdf,+ u(askdfjhasldkfjhasdkjfh)))),t(3,f)));++forall x. forall y. exists x. exists y. true;++f(1, f(1,2,3,4,5,6,7,8,9), 3) = g(asdlkfjas, 4);++f(1, 2, f(1,2,3,4,5,6,7,8,9)) = 2;++true or f(asdflkasjdflkjsdf, asdlfkjasdf) = g(asdlkfjas, 4);++231234 = gdd(asdsdfsdlkfjas, 4);++sdfsdg(1) = fdkfj(123, dfdff(1,2,3,4,5,6,7,8,9), 3) ;++sdfsdg(1,2) = fdkfj(123, dfdff(1,2,3,4,5,6,7,8,9), 3) ;++sdfsdg() = fdkfj(123, dfdff(1,2,3,4,5,6,7,8,9), 3) ;++true or 231234 = gdd(asdsdfsdlkfjas, 4);++true or f(f(2,3)) = gdd(asdsdfsdlkfjas, 4);++sdfsdg(g(f(2,3))) = fdkfj(123, dfdff(1,2,3,4,5,6,7,8,9), 3) ;+++sdfsdg(f(2,3)) = fdkfj(123, dfdff(1,2,3,4,5,6,7,8,9), 3) ;+++forall x. + P(f)(g)(h);++Q(f(g(3 )), efgasdfasdaa , 12345612345 ) or Foo(i(h(g(f(foobarfoobarfoo, a, b,c)))), 4 );++not (forall x. exists y. true);++Foo(f(foobarfoobarfoo, a, b,c), 4 );++true or Foo(f(foobarfoobarfoo, a, b,c), 4 );++forall x. forall x, y, y. Ppppp( bar, foo(bar))(foo, bar);+forall x. forall x, y, y. exists z. Ppppp( bar, foo(bar))(foo, bar);++not (forall x. exists y. Pppp( bar, foo(bar,foo()(bar(bar,baradflkjsdflkj))))(foo, bar)());++forall x. exists y. P( bar, foo(bar)(foo(twerkljweklrjwe,aslkdjfldkjfd,bar())))(foo, bar);++forall x. Pppp( bar, foo(bar)()(foo,bar))(foo, bar);++ foo( bar, bar)( bar) = 4;++P(a)(b);++Pasdfasdxb(a)(b);++P(asdf, asdfasdfasdfs, c)(b);++Foo(foobarfoobarfoo, a, b,c);++f(g(f(2,3)(123456789, 1)(4,5,6)(7,8)))(1) = functName(123, anotherfunctName(1,2,3,4,5,6,7,8,9), foo(h()(1,2,f(1,2))(3)),987654, bar()(1)) ;++f(g(f(2,3))(4,5,6)(7,8)) = f(g(f(2,3))(4,5,6)(7,8));++f(g(f(2,3)(4,5))(4,5,6)(7,8)) = 3;++feeee(geeeeeee(fee(2,gg(1)(2))(4,5))(4,5,6)(7,8))(3,4) = 3;++Feeee(geeeeee(fee(2,gg(1)(2))(4,5))(4,5,6)(7,8))(3,4);++Feeee(3, geeee(2222, 1, fee(2,gg(1)(2))(4,5))(4,5,6)(7,8))(3,4);++Feeee(geeee(2222, 1, fee(2,gg(1)(2))(4,5))(4,5,6)(7,8))(3,4);++true and feeee(geeeeee(fee(2,gg(1)(2))(4,5))(4,5,6)(7,8))(3,4) = 3;++P(2, f(a)(b), 3, f(a)(b));++if (true and false) then (true and false) else (true and false);++if true then false else true;++if (if true then false else true) then (if true then false else true) else (if true then false else true);++true and (if P() then (F()) else false);++let a = true in false;+let a = true in P();++let a = true, b = false in false; +++-- bad numbering: don't number let defs; also bad indentation+let a = if true then false else P(), b = P() in true and false;++let bbb = forall c. P(), d = true and false, cc = forall c. P(), aaa = if true then false else P() in true and false;+++let a = if P(a) then f() = g(a) else P(b), b = forall a. Q(a) in R(a, b);++not not not (not not (not not true and not not (false or true) and (true or not false)));++not ((true and false) and false);