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