1 2 3 module Build_itrm where 4 5 import Char(isDigit)--1.3 6 import Core_datatype 7 8 import Type_defs 9 10 import Attributes 11 12 import Unparse -- for debugging purposes only 13 14 import Kernel 15 16 import Sub_Core1 17 18 import Sub_Core2 19 20 import Sub_Core3 21 22 import Sub_Core4 23 24 import Vtslib 25 26 27 28 sym' :: String -> String -> Flagged_ITrm 29 30 sym' str1 str2 31 = if isint str1 && isint str2 32 then Opnd ( Itrm ( Sym no1 no2 [] [sym_ind] )) 33 else Prs_Err ( errstr ++ " is not an integer " ) 34 where 35 no1 = read str1 36 no2 = read str2 37 isint = and . ( map isDigit ) 38 errstr = if isint str1 then str2 else str1 39 40 41 42 43 44 45 const' :: String -> String -> String -> Flagged_ITrm 46 47 const' str1 str2 str3 48 = Opnd ( Itrm ( Const no1 no2 no3 [] [sym_ind])) 49 where 50 no1 = read str1 51 no2 = read str2 52 no3 = read str3 53 54 55 56 57 58 binder' bnd_con ( Opnd ( Idec dc )) ( Opnd ( Itrm tm )) 59 = ( Opnd . Itrm ) ( Binder bnd_con dc tm [] [pre_bdr] ) 60 61 62 63 binder' _ ( Prs_Err x ) _ = Prs_Err x 64 65 binder' _ _ ( Prs_Err x ) = Prs_Err x 66 67 68 69 70 71 cond' :: Flagged_ITrm -> Flagged_ITrm -> Flagged_ITrm -> Flagged_ITrm 72 73 cond' ( Prs_Err x ) _ _ = Prs_Err x 74 75 cond' _ ( Prs_Err x ) _ = Prs_Err x 76 77 cond' _ _ ( Prs_Err x ) = Prs_Err x 78 79 cond' ( Opnd ( Idec dc ) ) ( Opnd ( Itrm tm1 ) ) ( Opnd ( Itrm tm2 )) 80 = Opnd ( Itrm ( Cond dc tm1 tm2 [] [] )) 81 82 83 84 85 let' ( Prs_Err x ) _ _ = Prs_Err x 86 87 let' _ ( Prs_Err x ) _ = Prs_Err x 88 89 let' _ _ ( Prs_Err x ) = Prs_Err x 90 91 let' ( Opnd ( Idec dc)) ( Opnd ( Itrm tm1)) ( Opnd ( Itrm tm2 )) 92 = opnd ( App ( Binder Lambda dc tm2 [] [] ) tm1 [] [let_stl] ) 93 94 let' ( Opr _ _ _ ) _ _ = error "1" 95 let' _ ( Opr _ _ _ ) _ = error "2" 96 let' _ _ ( Opr _ _ _ ) = error "3" 97 let' _ ( Opnd ( PApp _ _ _ )) _ = error "4.1" 98 let' _ ( Opnd ( PairApp _ ) ) _ = error "4.2" 99 let' _ ( Opnd ( ParIfx _ _) ) _ = error "4.3" 100 let' _ ( Opnd ( TypApp _ ) ) _ = error "4.4" 101 let' _ ( Opnd ( Itrm _ ) ) _ = error "4.5" 102 let' _ ( Opnd ( Idec _ ) ) _ = error "4.6" 103 let' _ ( Opnd _ ) _ = error "5" 104 let' _ _ ( Opnd _ ) = error "6" 105 106 107 108 109 110 111 112 113 114 app' ( Opr ( Spl "" ) _ _ ) x = x 115 116 app' x ( Opr ( Spl "" ) _ _ ) = x 117 118 119 120 121 122 123 124 app' ( Opr ( OpBdr bdr ) _ _ ) ( Opnd ( Idec dc )) 125 = Opnd ( PApp bdr dc False ) 126 127 app' ( Opr ( OpBdr bdr ) _ _ ) ( Opnd ( Itrm srt )) 128 = Opnd ( PApp bdr dc True ) 129 where 130 dc = Symbol_dec srt [ sym_nm ( Name "_" ) ] 131 132 app' (Opnd ( PApp bdr dc anon )) ( Opnd ( Itrm tm )) 133 = opnd ( Binder bdr dc shft_tm [] [ifx_bdr] ) 134 where 135 shft_tm | anon = shift_trm [] 1 tm 136 | not anon = tm 137 138 139 140 app' ( Opr ( OpIfx op ) _ _ ) ( Opnd ( Itrm tm )) 141 = Opnd ( ParIfx op tm ) 142 143 app' ( Opnd ( ParIfx op tm1 ) ) ( Opnd ( Itrm tm2 )) 144 = opnd ( Binary' op tm1 tm2 [] [] ) 145 146 147 148 149 app' ( Opr ( Spl "," ) _ _ ) ( Opnd ( Itrm tm1 )) 150 = Opnd ( PairApp tm1 ) 151 152 153 154 155 156 157 app' ( Opnd ( PairApp tm1 )) ( Opnd ( Itrm tm2 )) 158 = Opnd ( Itrm pairtm ) 159 where 160 pairtm = Pair tm1 tm2 pdt [] [pr_untyped] 161 pdt = Constant ( Univ (-1) ) [] [] 162 163 164 165 166 app' ( Opr ( Spl "typed" ) _ _ ) opnd1 167 = Opnd ( TypApp opnd1 ) 168 169 170 171 172 app' ( Opnd ( TypApp ( Opnd ( Itrm ( Pair tm1 tm2 _ a b ))))) 173 ( Opnd ( Itrm srt )) 174 = Opnd ( Itrm ( Pair tm1 tm2 srt a [pr_typed] )) 175 176 177 178 app' ( Opr ( Spl "Not" ) _ _ ) ( Opnd ( Itrm tm )) 179 = opnd ( Unary Not tm [] [] ) 180 181 182 183 app' ( Opr ( Spl ":" ) _ _ ) ( Opnd ( Itrm tm )) 184 = Opnd ( ParColon tm ) 185 186 app' ( Opnd ( ParColon tm1 )) ( Opnd ( Itrm tm2 )) 187 = opnd ( add_type tm1 tm2 ) 188 189 190 191 app' ( Opnd ( Itrm tm1 )) ( Opnd ( Itrm tm2 )) 192 = opnd ( App tm1 tm2 [] [] ) 193 194 app' ( Opr ( OpItrm op ) stl _ ) ( Opnd ( Itrm tm )) 195 = opnd ( App op tm [] [ op_stl stl ] ) 196 197 app' ( Opnd ( Itrm tm )) ( Opr ( OpItrm op ) _ _ ) -- happen? 198 = opnd ( App tm op [] [] ) 199 200 201 202 app' ( Opr ( OpItrm op1 ) stl _ ) ( Opr ( OpItrm op2 ) _ _ ) 203 = opnd ( App op1 op2 [] [ op_stl stl ] ) 204 205 app' ( Prs_Err mess ) _ = Prs_Err mess 206 207 app' _ ( Prs_Err mess ) = Prs_Err mess 208 209 app' x y = error ( "app' y: " ++ unparse ( Empty []) y ++ "\nx: " ++ unparse (Empty [] ) x ) 210 211 212 213 214 215 216 opnd :: ITrm -> Flagged_ITrm 217 218 opnd = Opnd . Itrm 219 220 221 222 223 fetch_arg :: Flagged_ITrm -> ITrm 224 225 fetch_arg ( Opnd ( Itrm tm )) = tm 226 227 fetch_arg ( Opr ( OpItrm op ) _ _ ) = op 228 229 230 231 decpair' _ ( Prs_Err x ) _ = Prs_Err x 232 233 decpair' _ _ ( Prs_Err x ) = Prs_Err x 234 235 decpair' att ( Opnd ( Idec dc1 )) ( Opnd ( Idec dc2 )) 236 = ( Opnd . Idec ) ( Decpair dc1 dc2 att ) 237 238 239 240 symbol_dec' ( Opnd ( Itrm tm )) nm attL 241 = ( Opnd . Idec ) ( Symbol_dec tm ( sym_nm nm : attL ) ) 242 243 symbol_dec' ( Prs_Err mess ) nm _ = Prs_Err mess 244 245 246 247 248 249 data' ( _ , [ Prs_Err mesg ] ) _ 250 = Prs_Err mesg 251 252 data' ( type_nm , dcl ) ctr_defs 253 = case ctrs of 254 Ok ( ctr_nml , ctr_srtl ) 255 -> ( Opnd . Idec ) ( Data ( clear dcl ) ctr_srtl att ) 256 where 257 att = [ dat_nm ( type_nm : ctr_nml ) ] 258 Bad mesg -> Prs_Err mesg 259 where 260 ctrs = ctr' [] [] ctr_defs 261 clear ( Opnd ( Idec dc ) : dcl ) = dc : clear dcl 262 clear [] = [] 263 264 265 266 267 ctr' nml argll (( nm , argl ) : ctrl ) 268 = case checked_args of 269 Ok iargl -> ctr' ( nm : nml ) ( iargl : argll ) ctrl 270 Bad mesg -> Bad mesg 271 where 272 checked_args = check_arg [] argl 273 274 ctr' nml argll [] 275 = Ok ( reverse nml , reverse argll ) 276 277 278 279 check_arg tml ( Opnd ( Itrm tm ) : argl ) 280 = check_arg ( tm : tml ) argl 281 282 check_arg tml [] 283 = Ok ( reverse tml ) 284 285 check_arg _ ( Prs_Err mesg : argl ) 286 = Bad mesg 287 288 289 290 extend' ( Opnd ( Idec dc )) ( Opnd ( Isgn sg )) 291 = Opnd ( Isgn ( Extend dc sg [] )) 292 293 extend' _ ( Prs_Err mesg ) 294 = Prs_Err mesg 295 296 extend' ( Prs_Err mesg ) _ 297 = Prs_Err mesg 298 299 300 301 302 def' ( _ , [ Prs_Err mesg ] ) _ _ 303 = Prs_Err mesg 304 305 def' _ ( Prs_Err mesg ) _ 306 = Prs_Err mesg 307 308 def' ( nm , fmls ) ( Opnd ( Itrm rhs )) att 309 = ( Opnd . Idec ) ( Def tm srt [ sym_nm nm , att ] ) 310 where 311 tm = make_tm fmls rhs 312 srt = Constant ( Univ 0 ) [] [] -- temporary - need sort fn 313 314 315 make_tm ( Opnd ( Idec dc ) : dcl ) rhs 316 = Binder Lambda dc ( make_tm dcl rhs ) [] [] 317 318 make_tm [] rhs 319 = rhs 320 321 322 add_sg_att ( Prs_Err mesg ) _ = Prs_Err mesg 323 324 add_sg_att ( Opnd ( Isgn ( Empty attl ))) att 325 = Opnd ( Isgn ( Empty ( att : attl ))) 326 327 add_sg_att ( Opnd ( Isgn ( Extend dc sg attl ))) att 328 = Opnd ( Isgn ( Extend dc sg ( att : attl ))) 329 330 331 332 333 334 335 recurse' _ ( Prs_Err mesg ) = Prs_Err mesg 336 337 recurse' tml ( Opnd ( Itrm srt )) 338 = case clr [] tml of 339 Ok itml -> Opnd ( Itrm ( Recurse itml srt [] [rcrs_stl] )) 340 Bad mesg -> Prs_Err mesg 341 where 342 clr itml (( Opnd ( Itrm tm )) : tml ) = clr ( tm : itml ) tml 343 clr itml [] = Ok itml 344 clr _ ( Prs_Err mesg : _ ) = Bad mesg 345 346 347 348 349 350 tag' tg tgL 351 = case check tgL of 352 Ok _ -> Opnd ( Itrm ( Tagid tg tgL )) 353 Bad mesg -> Prs_Err mesg 354 where 355 check ( Tg_Trm ( TM _ _ _ ) : oth ) = check oth 356 check ( Tg_Trm ( TM_Err mesg ) :oth ) = Bad mesg 357 check ( Tg_Thm ( TH _ _ ) : oth ) = check oth 358 check ( Tg_Thm ( TH_Err mesg ) : oth ) = Bad mesg 359 check ( Tg_Int iL : oth ) = check oth 360 check [] = Ok [] -- list is given in tgL 361 362