1 module Unparse(unparse_tm , unparse_th , unparse , unparse' , disp_tk , unparse_sg , unparse_sg' , unparse_nm , unparse_trm , unparse_Trm , unparse_sgn , unparse_Sgn , unparse_Dec , unparse_dec , unparse_Thm ) where 2 3 4 5 import Kernel 6 7 import Type_defs 8 9 import Core_datatype 10 11 import Attributes 12 13 14 15 16 unparse_trm ( SG isg ) _ = unparse' isg 17 18 unparse_Trm _ _ ( TM itm _ isg ) = unparse' isg itm 19 20 unparse_sgn _ _ isg = unparse_sg' isg 21 22 unparse_Sgn _ _ ( SG isg ) = unparse_sg' isg 23 24 25 unparse_dec ( SG isg ) _ idc = unparse_dc isg idc 26 27 unparse_Dec _ _ ( DC idc isg ) = unparse_dc isg idc 28 29 30 unparse_Thm _ _ ( TH itm isg ) = unparse' isg itm 31 32 33 unparse_th ( TH tm sg ) 34 = "Theorem: " ++ unparse' sg tm ++ "\n" 35 36 unparse_th ( TH_Err mesg ) 37 = "Invalid theorem: " ++ mesg ++ "\n" 38 39 40 41 42 43 44 unparse_tm ( TM tm1 tm2 sg ) 45 = "Term: " ++ unparse' sg tm1 ++ "\nType: " ++ unparse' sg tm2 ++ "\nSig: " ++ unparse_sg' sg ++ "\n" 46 47 unparse_tm ( TM_Err mesg ) = "\nTerm formation error\n" ++ mesg ++ "\n" 48 49 50 51 52 53 54 55 unparse sg ( Opnd ( Itrm tm )) 56 = unparse' sg tm 57 58 unparse sg ( Opnd ( Idec dc )) 59 = unparse_dc sg dc 60 61 unparse _ ( Prs_Err mess ) = mess ++ "\n" 62 63 64 65 unparse sg ( Opr ( OpItrm tm ) tpe prc ) 66 = unparse' sg tm ++ "{tpe" ++ show_tpe tpe ++ "prc" ++ show prc ++ "}\n" 67 68 unparse _ ( Opr (Spl "") _ _ ) = "unparse operator" 69 70 unparse sg ( Opnd ( TypApp tm )) = "Unparse TypApp: " ++ unparse sg tm 71 72 unparse sg ( Opr ( Spl "typed" ) _ _ ) = "Unparse 'typed'" 73 74 unparse sg oth = "unparse unknown" 75 76 77 78 unparse' sg ( Sym n1 n2 _ att ) 79 = case attval Symbol_Style att of 80 Named -> lookUp sg n1 n2 (-1) 81 Indexed -> "\168" ++ show n1 ++ "," ++ show n2 ++ "\169" 82 83 unparse' sg ( Const i j k _ _ ) 84 = lookUp sg i j k 85 86 unparse' sg ( App tm1 tm2 _ _ ) 87 = "(" ++ unparse' sg tm1 ++ " " ++ unparse' sg tm2 ++ ")" 88 89 unparse' sg ( Pair tm1 tm2 tm3 _ _ ) 90 = "((" ++ unparse' sg tm1 ++ " , " ++ unparse' sg tm2 ++ ") : " ++ unparse' sg tm3 ++ ")" 91 92 unparse' sg ( Binder Subtype dc tm _ _ ) 93 = "{" ++ unparse_dc sg dc ++ " | " ++ unparse' sg2 tm ++ "}" 94 where 95 sg2 = Extend dc sg [] 96 97 98 99 unparse' sg ( Binder Imp dc tm _ _ ) 100 = " [" ++ unparse_dc sg dc ++ "] " ++ "\182" ++ " " ++ unparse' sg2 tm 101 where 102 sg2 = Extend dc sg [] 103 104 unparse' sg ( Binder con dc tm _ _ ) 105 = "(" ++ unparse_bdr con ++ unparse_dc sg dc ++ ". " ++ unparse' sg2 tm ++ ")" 106 where 107 sg2 = Extend dc sg [] 108 109 unparse' sg ( Constant con _ _ ) 110 = unparse_constant con 111 112 unparse' sg ( Unary con tm _ _ ) 113 = " \181" ++ unparse' sg tm 114 115 116 unparse' sg ( Binary' con tm1 tm2 _ _ ) 117 = "(" ++ unparse' sg tm1 ++ " " ++ unparse_bcon con 118 ++ " " ++ unparse' sg tm2 ++ ")" 119 120 unparse' sg ( Cond dc tm1 tm2 _ _ ) 121 = " if [" ++ unparse_dc sg dc ++ "] then " ++ unparse' sg2 tm1 ++ 122 " else " ++ unparse' sg2 tm2 123 where 124 sg2 = Extend dc sg [] 125 126 127 unparse' sg ( Recurse tml srt _ _ ) 128 = "\nrecurse\n\t" ++ concat ( map unparse_cls tml ) ++ 129 "\nend typed " ++ unparse' sg srt 130 where 131 unparse_cls tm = unparse' sg tm ++ "\n\t" 132 133 134 unparse' sg ( Tagid ( nm , _ , _ ) argL ) 135 = "( " ++ nm ++ concat' " " ( map argl argL ) ++ " )" 136 where 137 concat' sep ( a:x ) = sep ++ a ++ concat' sep x 138 concat' _ [] = "" 139 argl ( Tg_Trm tm ) = unparse_tm tm 140 argl ( Tg_Thm th ) = unparse_th th 141 argl ( Tg_Int iL ) = "\168" ++ concat' "," ( map show iL ) ++ "\169" 142 143 unparse' sg ( ITrm_Err mesg ) = mesg 144 145 146 147 148 149 unparse_bdr Lambda = "\236" 150 151 unparse_bdr Forall = "\177" 152 153 unparse_bdr Exists = "\178" 154 155 unparse_bdr Pi = "\208" 156 157 unparse_bdr Sigma = "\211" 158 159 unparse_bdr Choose = "\229" 160 161 unparse_bdr Delta = "\196" 162 163 164 165 unparse_dc sg ( Symbol_dec tm attL ) 166 = unparse_nm nm ++ " : " ++ unparse' sg tm 167 where 168 nm = case attval Name_Style attL of 169 Symbol_Name nm' -> nm' 170 Datatype_Name nmL -> Name " Unexpected Datatype " 171 172 unparse_dc sg ( Axiom_dec tm attL ) 173 = unparse_nm nm ++ " :a: " ++ unparse' sg tm 174 where 175 nm = case attval Name_Style attL of 176 Symbol_Name nm' -> nm' 177 Datatype_Name nmL -> Name " Unexpected Datatype " 178 179 unparse_dc sg ( Decpair dc1 dc2 _ ) 180 = " ( " ++ unparse_dc sg dc1 ++ " ; " ++ unparse_dc sg2 dc2 ++ " ) " 181 where 182 sg2 = Extend dc1 sg [] 183 184 unparse_dc sg ( Data dcl ctrs attL ) 185 = "datatype " ++ unparse_nm nm ++ " " ++ unparse_fmls sg dcl ++ " = " ++ unparse_ctrs sg2 nmL ctrs 186 where 187 sg2 = Extend tp_dcl ( extend_sg sg ( reverse dcl )) [] 188 tp_dcl = Symbol_dec u0 [ sym_nm nm ] 189 u0 = Constant ( Univ 0 ) [] [] 190 extend_sg sg' ( dc : dcl ) = extend_sg ( Extend dc sg' []) dcl 191 extend_sg sg' [] = sg' 192 nm : nmL = case attval Name_Style attL of 193 Symbol_Name nm' -> [ Name " Unexpected Symbol " ] 194 Datatype_Name nmL' -> nmL' 195 196 unparse_dc sg ( Def tm srt attL ) 197 = unparse_nm nm ++ " \189 " ++ unparse' sg tm 198 where 199 nm = case attval Name_Style attL of 200 Symbol_Name nm' -> nm' 201 Datatype_Name nmL -> Name " Unexpected Datatype " 202 203 unparse_dc sg _ 204 = " dc not implemented " 205 206 207 208 unparse_fmls sg ( dc : dcl ) 209 = "(" ++ unparse_dc sg dc ++ ") " ++ unparse_fmls sg dcl 210 211 unparse_fmls _ [] = "" 212 213 214 unparse_ctrs sg ( nm : nml ) ( ctr : ctrl ) 215 = unparse_nm nm ++ " " ++ unparse_ctr sg ctr ++ " | " ++ unparse_ctrs sg nml ctrl 216 217 unparse_ctrs _ [] [] = "" 218 219 220 unparse_ctr sg ( arg : argl ) 221 = unparse' sg arg ++ " " ++ unparse_ctr sg argl 222 223 unparse_ctr _ [] = "" 224 225 226 227 228 229 230 231 unparse_nm ( Name nm ) 232 = nm 233 234 unparse_nm ( Operator' op prc tpe ) 235 = "{" ++ op ++ " " ++ show_tpe tpe ++ " " ++ show prc ++ "}" 236 237 238 239 240 show_tpe Pre = "Pre" 241 242 show_tpe BinL = "BinL" 243 244 show_tpe BinR = "BinR" 245 246 show_tpe Post = "Post" 247 248 249 250 251 252 unparse_bcon :: Binary_conn -> String 253 254 unparse_bcon Or = "\180" 255 256 unparse_bcon And = "\179" 257 258 -- unparse_bcon Imp = "\182" 259 260 unparse_bcon Eq' = "=" 261 262 unparse_bcon Issubtype = "\172" 263 264 265 266 unparse_constant T = "True" 267 268 unparse_constant F = "False" 269 270 unparse_constant Bool' = "Bool" 271 272 unparse_constant ( Univ i ) = "U" ++ show i 273 274 275 276 277 278 lookUp ( Extend dc sg _ ) 0 i2 i3 279 = lookup_dc dc [] i2 i3 280 281 lookUp ( Extend dc sg _ ) i1 i2 i3 | i1 > 0 282 = lookUp sg (i1-1) i2 i3 283 284 lookUp _ _ _ _ = "symbol not found " 285 286 287 288 289 lookup_dc ( Symbol_dec tm attL ) _ 0 _ 290 = case nm of 291 Name inm -> inm 292 Operator' op _ _ -> op 293 where 294 nm = case attval Name_Style attL of 295 Symbol_Name nm' -> nm' 296 Datatype_Name nmL -> Name " Unexpected Datatype " 297 298 lookup_dc ( Axiom_dec tm attL ) _ 0 _ 299 = case nm of 300 Name inm -> inm 301 Operator' op _ _ -> op 302 where 303 nm = case attval Name_Style attL of 304 Symbol_Name nm' -> nm' 305 Datatype_Name nmL -> Name " Unexpected Datatype " 306 307 308 lookup_dc ( Decpair dc1 dc2 attL ) dcl i k | i > 0 309 = case attval Dec_Style attL of 310 -- Grouped -> --HERE 311 Grouped -> lookup_dc dc1 ( dc2 : dcl ) (i-1) k 312 Ungrouped -> lookup_dc dc1 ( dc2 : dcl ) (i-1) k 313 314 lookup_dc ( Data _ _ attL ) _ 0 k 315 = lookup_ctr nmL k 316 where 317 nmL = case attval Name_Style attL of 318 Symbol_Name nm' -> [ nm' ] -- error cond (change?) 319 Datatype_Name nmL' -> nmL' 320 321 lookup_dc ( Def _ _ attL ) _ 0 _ 322 = case nm of 323 Name inm -> inm 324 Operator' op _ _ -> op 325 where 326 nm = case attval Name_Style attL of 327 Symbol_Name nm' -> nm' 328 Datatype_Name nmL -> Name " Unexpected Datatype " 329 330 lookup_dc _ ( dc : dcl ) i k | i > 0 331 = lookup_dc dc dcl (i-1) k 332 333 lookup_dc _ _ _ _ = " symbol not found " 334 335 336 337 338 339 340 341 lookup_ctr ( nm : nml ) k | k > 0 342 = lookup_ctr nml (k-1) 343 344 lookup_ctr ( nm : nml ) 0 345 = case nm of 346 Name inm -> inm 347 Operator' op _ _ -> op 348 349 lookup_ctr [] _ 350 = " Constructor not found " 351 352 353 354 355 356 357 358 359 360 disp_tk :: Token -> String 361 362 disp_tk ( Rvd str ) = str 363 364 disp_tk ( Clr str ) = str 365 366 disp_tk ( Bdr bdr ) = unparse_bdr bdr 367 368 disp_tk ( IfxBdr str ) = str 369 370 disp_tk ( IfxOp str ) = str 371 372 disp_tk ( Scan_Err str ) = "Invalid token: " ++ str -- have to change this? 373 374 375 376 377 378 unparse_sg :: Flagged_ITrm -> String 379 380 unparse_sg ( Opnd ( Isgn sg )) = unparse_sg' sg 381 382 unparse_sg ( Prs_Err mesg ) = mesg 383 384 385 386 387 388 unparse_sg' ( Empty _ ) = "" 389 390 unparse_sg' ( Extend dc sg _ ) 391 = unparse_dc ( Empty [] ) dc ++ " ;\n" ++ unparse_sg' sg 392