1   module Type_defs where
    2 
    3   import Core_datatype
    4 
    5   import Kernel
    6 
    7   data MayBe a b = Ok a | Bad b deriving ( Eq )
    8 
    9   data Token = Rvd String | Clr String | Bdr Binder_conn |
   10                IfxBdr String | IfxOp String | Scan_Err String
   11                  deriving ( Eq )
   12     -- partain:
   13   instance Show Token
   14 
   15 
   16  -- data Oprtype = Pre | Post | BinL | BinR deriving ( Eq )
   17 
   18 
   19 
   20 
   21 
   22  {-
   23   data Flagged_ITrm = Opr Operator Oprtype Int |
   24                       Opnd Operand         | 
   25                       Prs_Err String
   26                         deriving ( Eq )
   27 
   28   data Operand = Itrm ITrm | Idec IDec | Isgn ISgn   -- normal operands
   29                  | PApp Binder_conn IDec Bool        -- special partial apps, bool indicates anonymous declaration 
   30                  | PairApp ITrm 
   31                  | ParIfx Binary_conn ITrm
   32                  | TypApp Flagged_ITrm
   33                    deriving ( Eq )
   34 
   35   data Operator = OpItrm ITrm | OpBdr Binder_conn 
   36                   | OpIfx Binary_conn | Spl String deriving ( Eq )
   37 
   38 
   39 
   40   type Itrm_fn = Flagged_ITrm -> ITrm
   41 
   42   type Trm_fn = Flagged_ITrm -> Trm
   43 
   44   type Deriv_fn = Flagged_ITrm -> Thm
   45 
   46   type Tag = ( String , [Tag_Arg_type] , Itrm_fn , Trm_fn , Deriv_fn )
   47 
   48   data Tag_Arg_type = Term_Arg | Deriv_Arg | Int_Arg deriving ( Eq )
   49   -}