1 {- 2 * Mon Nov 5 09:54:24 GMT 1990 3 * 4 * Implementation of untyped terms, signatures and declarations 5 * 6 * Each constructors last argument (of the tuple) is a list of 7 * information attributes that the parser, unparsers, tactics etc use. 8 * 9 * Each terms' next to last argument is a list of alternative types that the 10 * term can have to its natutal type. 11 * 12 -} 13 14 module Core_datatype where 15 16 17 18 type Share_map = [ Int ] 19 20 data ITrm = Sym Int Int [ ITrm ] [ Attribute ] 21 | App ITrm ITrm [ ITrm ] [ Attribute ] 22 | Pair ITrm ITrm ITrm [ ITrm ] [ Attribute ] 23 | Binder Binder_conn IDec ITrm [ ITrm ] [ Attribute ] 24 | Constant Constant_conn [ ITrm ] [ Attribute ] 25 | Unary Unary_conn ITrm [ ITrm ] [ Attribute ] 26 | Binary' Binary_conn ITrm ITrm [ ITrm ] [ Attribute ] 27 | Cond IDec ITrm ITrm [ ITrm ] [ Attribute ] 28 | Const Int Int Int [ ITrm ] [ Attribute ] 29 | Recurse [ ITrm ] ITrm [ ITrm ] [ Attribute ] 30 | Tagid Tag [ Tag_Arg ] 31 | ITrm_Err String 32 -- deriving (Eq) 33 34 data IDec = Symbol_dec ITrm [ Attribute ] 35 | Axiom_dec ITrm [ Attribute ] 36 | Def ITrm ITrm [ Attribute ] 37 | Data [ IDec ] [[ ITrm ]] [ Attribute ] 38 | Decpair IDec IDec [ Attribute ] 39 -- deriving (Eq) 40 41 data ISgn = Empty [ Attribute ] 42 | Extend IDec ISgn [ Attribute ] 43 | Combine ISgn ISgn Int [ Int ] [ Attribute ] 44 | Share ISgn Int Int Int [ Int ] [ Attribute ] 45 -- deriving (Eq) 46 47 data Binder_conn = Lambda | Forall | Exists | Pi | Sigma | 48 Imp | Subtype | Delta | Choose 49 deriving (Eq) 50 51 data Unary_conn = Not deriving (Eq) 52 53 data Binary_conn = Or | And | Eq' | Issubtype deriving (Eq) 54 55 data Constant_conn = T | F | Bool' | Univ Int deriving (Eq) 56 57 58 59 60 61 62 63 64 -- types associated with tags 65 66 type Tag = ( String , [Tag_Arg_type] , [Cnv_Fn] ) 67 68 69 -- type indicator and resulting types for args 70 71 data Tag_Arg_type = Term_Arg | Deriv_Arg | Int_Arg deriving ( Eq ) 72 73 data Tag_Arg = Tg_Trm Trm | Tg_Thm Thm | Tg_Int [Int] -- deriving ( Eq ) 74 75 76 -- convertion function ( tags to related objects ) 77 78 data Cnv_Fn = Trm_Fn ( [Tag_Arg] -> Trm ) | 79 Thm_Fn ( [Tag_Arg] -> Thm ) 80 81 -- need terms and theorems in tags ( leave here permanently? ) 82 83 data Trm = TM ITrm ITrm ISgn | {- the term, its type, and signature -} 84 TM_Err String 85 86 data Thm = TH ITrm ISgn | {- the theorem, and its signature -} 87 TH_Err String 88 89 90 91 92 93 94 -- working types for parser 95 96 type Attribute = ( Attribute_Tag , Attribute_Value ) 97 98 99 data Flagged_ITrm = Opr Operator Oprtype Int | 100 Opnd Operand | 101 Prs_Err String 102 -- deriving ( Eq ) 103 104 data Operand = Itrm ITrm | Idec IDec | Isgn ISgn -- normal operands 105 | PApp Binder_conn IDec Bool -- special partial apps, bool indicates anonymous declaration 106 | PairApp ITrm 107 | ParIfx Binary_conn ITrm 108 | TypApp Flagged_ITrm 109 | ParColon ITrm 110 -- deriving ( Eq ) 111 112 data Operator = OpItrm ITrm | OpBdr Binder_conn 113 | OpIfx Binary_conn | Spl String --deriving ( Eq ) 114 115 116 data Attribute_Tag = Name_Style 117 | Symbol_Style 118 | Pair_Style 119 | Let_Style 120 | Case_Style 121 | Opr_Style 122 | Fun_Style 123 | Binder_Style 124 | Constant_Style 125 | Unary_Style 126 | Binary_Style 127 | Cond_Style 128 | Recurse_Style 129 | Hyp_Style 130 | Dec_Style 131 | Def_Style 132 | Comment 133 deriving (Eq) 134 135 136 data Attribute_Value = Symbol_Name Name' 137 | Datatype_Name [ Name' ] 138 | Named | Indexed 139 | Typed | Untyped 140 | Let 141 | Case 142 | Prefixed | Linfixed | Rinfixed | Postfixed 143 | Functional | Subscripted 144 | Prefix_Binder | Infix_Binder 145 | Recursive | Fn 146 | NonDependent 147 | Grouped | Ungrouped 148 | Parameter | NonParameter 149 | String' String 150 deriving (Eq) 151 152 data Name' = Name String | Operator' String Int Oprtype 153 deriving ( Eq ) 154 155 data Oprtype = Pre | Post | BinL | BinR deriving ( Eq ) 156 157 -- att_to_str (Name' s) = s 158