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 -}