> 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

temorary unparser - Flagged_Itrms to strings

> import Kernel

> import Type_defs

> import Core_datatype

> import Attributes


unparse functions ro allow editor to type check

> unparse_trm ( SG isg ) _ = unparse' isg

> unparse_Trm _ _ ( TM itm _ isg ) = unparse' isg itm

> unparse_sgn _ _ isg  = unparse_sg' isg

> unparse_Sgn _ _ ( SG isg )  = unparse_sg' isg


> unparse_dec ( SG isg ) _ idc = unparse_dc isg idc

> unparse_Dec _ _ ( DC idc isg ) = unparse_dc isg idc


> unparse_Thm _ _ ( TH itm isg ) = unparse' isg itm


> unparse_th ( TH tm sg )
>	= "Theorem: " ++ unparse' sg tm ++ "\n"

> unparse_th ( TH_Err mesg )
>	= "Invalid theorem: " ++ mesg ++ "\n"






> unparse_tm ( TM tm1 tm2 sg )
>	= "Term: " ++ unparse' sg tm1 ++ "\nType: " ++ unparse' sg tm2 ++ "\nSig: " ++ unparse_sg' sg ++ "\n"

> unparse_tm ( TM_Err mesg ) = "\nTerm formation error\n" ++ mesg ++ "\n"







> unparse sg ( Opnd ( Itrm tm ))
>	= unparse' sg tm 

> unparse sg ( Opnd ( Idec dc ))
>	= unparse_dc sg dc 

> unparse _ ( Prs_Err mess ) = mess ++ "\n"

other (debugging) unparses

> unparse sg ( Opr ( OpItrm tm ) tpe prc )
>	= unparse' sg tm ++ "{tpe" ++ show_tpe tpe ++ "prc" ++ show prc ++ "}\n"

> unparse _ ( Opr (Spl "") _ _ ) = "unparse operator"

> unparse sg ( Opnd ( TypApp tm )) = "Unparse TypApp: " ++ unparse sg tm 

> unparse sg ( Opr ( Spl "typed" ) _ _ ) = "Unparse 'typed'" 

> unparse sg oth = "unparse unknown"



> unparse' sg ( Sym n1 n2 _ att )
>	= case attval Symbol_Style att  of
>		Named   -> lookUp sg n1 n2 (-1)
>		Indexed -> "\168" ++ show n1 ++ "," ++ show n2 ++ "\169"

> unparse' sg ( Const i j k _ _ )
> 	= lookUp sg i j k

> unparse' sg ( App tm1 tm2 _ _ )
>	= "(" ++ unparse' sg tm1 ++ " " ++ unparse' sg tm2 ++ ")"

> unparse' sg ( Pair tm1 tm2 tm3 _ _ )
>	= "((" ++ unparse' sg tm1 ++ " , " ++ unparse' sg tm2 ++ ") : " ++ unparse' sg tm3 ++ ")"

> unparse' sg ( Binder Subtype dc tm _ _ )
>	= "{" ++ unparse_dc sg dc ++ " | " ++ unparse' sg2 tm ++ "}"
>	  where
>	  sg2 = Extend dc sg []

N.B. Implies needs extended sg 

> unparse' sg ( Binder Imp dc tm _ _ )
>	= " [" ++ unparse_dc sg dc ++ "] " ++ "\182" ++ " " ++ unparse' sg2 tm
>	  where
>	  sg2 = Extend dc sg []

> unparse' sg ( Binder con dc tm _ _ )
>	= "(" ++ unparse_bdr con ++ unparse_dc sg dc ++ ". " ++ unparse' sg2 tm ++ ")" 
>	  where
>	  sg2 = Extend dc sg []

> unparse' sg ( Constant con _ _ )
> 	= unparse_constant con 

> unparse' sg ( Unary con tm _ _ )
>	= " \181" ++ unparse' sg tm


> unparse' sg ( Binary' con tm1 tm2 _ _ )
>	= "(" ++ unparse' sg tm1 ++ " " ++ unparse_bcon con 
>			++ " " ++ unparse' sg tm2 ++ ")"

> unparse' sg ( Cond dc tm1 tm2 _ _ )
>	= " if [" ++ unparse_dc sg dc ++ "] then " ++ unparse' sg2 tm1 ++
>			" else " ++ unparse' sg2 tm2
>	  where
>	  sg2 = Extend dc sg []


> unparse' sg ( Recurse tml srt _ _ )
>	= "\nrecurse\n\t" ++ concat ( map unparse_cls tml ) ++
>			"\nend typed " ++ unparse' sg srt
>	  where
>	  unparse_cls tm = unparse' sg tm ++ "\n\t"


> unparse' sg ( Tagid ( nm , _ , _ ) argL )
>	= "( " ++ nm ++ concat' " " ( map argl argL ) ++ " )"
>	  where
>	  concat' sep ( a:x ) = sep ++ a ++ concat' sep x
>	  concat' _ []        = ""
>	  argl ( Tg_Trm tm ) = unparse_tm tm
>	  argl ( Tg_Thm th ) = unparse_th th
>	  argl ( Tg_Int iL ) = "\168" ++ concat' "," ( map show iL ) ++ "\169"

> unparse' sg ( ITrm_Err mesg ) = mesg





> unparse_bdr Lambda = "\236"

> unparse_bdr Forall = "\177"

> unparse_bdr Exists = "\178"

> unparse_bdr Pi = "\208"

> unparse_bdr Sigma = "\211"

> unparse_bdr Choose = "\229"

> unparse_bdr Delta = "\196"



> unparse_dc sg ( Symbol_dec tm attL ) 
>	= unparse_nm nm ++ " : " ++ unparse' sg tm
>	  where
>	  nm = case attval Name_Style attL of
>		   Symbol_Name nm'   -> nm'
>		   Datatype_Name nmL -> Name " Unexpected Datatype "

> unparse_dc sg ( Axiom_dec tm attL ) 
>	= unparse_nm nm ++ " :a: " ++ unparse' sg tm
>	  where
>	  nm = case attval Name_Style attL of
>		   Symbol_Name nm'   -> nm'
>		   Datatype_Name nmL -> Name " Unexpected Datatype "

> unparse_dc sg ( Decpair dc1 dc2 _ )
>	= " ( " ++ unparse_dc sg dc1 ++ " ; " ++ unparse_dc sg2 dc2 ++ " ) "
>	  where
>	  sg2 = Extend dc1 sg [] 

> unparse_dc sg ( Data dcl ctrs attL )
>	= "datatype " ++ unparse_nm nm ++ " " ++ unparse_fmls sg dcl ++ " = " ++ unparse_ctrs sg2 nmL ctrs
>	  where
>	  sg2 = Extend tp_dcl ( extend_sg sg ( reverse dcl )) []
>	  tp_dcl = Symbol_dec u0 [ sym_nm nm ] 
>	  u0 = Constant ( Univ 0 ) [] []
>	  extend_sg sg' ( dc : dcl ) = extend_sg ( Extend dc sg' []) dcl
>	  extend_sg sg' [] = sg'
>	  nm : nmL = case attval Name_Style attL of
>		  	 Symbol_Name nm'    -> [ Name " Unexpected Symbol " ]
>		   	 Datatype_Name nmL' -> nmL'

> unparse_dc sg ( Def tm srt attL )
>	= unparse_nm nm ++ " \189 " ++ unparse' sg tm
>	  where
>	  nm = case attval Name_Style attL of
>		   Symbol_Name nm'   -> nm'
>		   Datatype_Name nmL -> Name " Unexpected Datatype "

> unparse_dc sg _
>	= " dc not implemented "



> unparse_fmls sg ( dc : dcl )
>	= "(" ++ unparse_dc sg dc ++ ") " ++ unparse_fmls sg dcl 

> unparse_fmls _ [] = ""


> unparse_ctrs sg ( nm : nml ) ( ctr : ctrl )
>	= unparse_nm nm ++ " " ++ unparse_ctr sg ctr ++ " | " ++ unparse_ctrs sg nml ctrl

> unparse_ctrs _ [] [] = ""


> unparse_ctr sg ( arg : argl )
>	= unparse' sg arg ++ " " ++ unparse_ctr sg argl

> unparse_ctr _ [] = ""







> unparse_nm ( Name nm )
>	= nm

> unparse_nm ( Operator' op prc tpe )
>	= "{" ++ op ++ " " ++ show_tpe tpe ++ " " ++ show prc ++ "}"




> show_tpe Pre = "Pre"

> show_tpe BinL = "BinL"

> show_tpe BinR = "BinR"

> show_tpe Post = "Post"





> unparse_bcon :: Binary_conn -> String

> unparse_bcon Or = "\180"

> unparse_bcon And = "\179"

>-- unparse_bcon Imp = "\182"

> unparse_bcon Eq' = "="

> unparse_bcon Issubtype = "\172"



> unparse_constant T = "True"

> unparse_constant F = "False"

> unparse_constant Bool' = "Bool"

> unparse_constant ( Univ i ) = "U" ++ show i





> lookUp ( Extend dc sg _ ) 0 i2 i3
>	= lookup_dc dc [] i2 i3

> lookUp ( Extend dc sg _ ) i1 i2 i3 | i1 > 0
>	= lookUp sg (i1-1) i2 i3

> lookUp _ _ _ _ = "symbol not found "




> lookup_dc ( Symbol_dec tm attL ) _ 0 _
>	= case nm of
>	 	Name inm         -> inm
>		Operator' op _ _ -> op
>	  where
>	  nm = case attval Name_Style attL of
>		   Symbol_Name nm'   -> nm'
>		   Datatype_Name nmL -> Name " Unexpected Datatype "

> lookup_dc ( Axiom_dec tm attL ) _ 0 _
>	= case nm of
>	 	Name inm         -> inm
>		Operator' op _ _ -> op
>	  where
>	  nm = case attval Name_Style attL of
>		   Symbol_Name nm'   -> nm'
>		   Datatype_Name nmL -> Name " Unexpected Datatype "


> lookup_dc ( Decpair dc1 dc2 attL ) dcl i k | i > 0
>	= case attval Dec_Style attL of
>--		Grouped   -> --HERE
>		Grouped   ->  lookup_dc dc1 ( dc2 : dcl ) (i-1) k
>		Ungrouped -> lookup_dc dc1 ( dc2 : dcl ) (i-1) k

> lookup_dc ( Data _ _ attL ) _ 0 k
>	= lookup_ctr nmL k
>	  where
>	  nmL = case attval Name_Style attL of
>		   Symbol_Name nm'    -> [ nm' ] -- error cond (change?)
>		   Datatype_Name nmL' -> nmL'

> lookup_dc ( Def _ _ attL ) _ 0 _ 
>	= case nm of
>	 	Name inm         -> inm
>		Operator' op _ _ -> op
>	  where
>	  nm = case attval Name_Style attL of
>		   Symbol_Name nm'   -> nm'
>		   Datatype_Name nmL -> Name " Unexpected Datatype "

> lookup_dc _ ( dc : dcl ) i k | i > 0
>	= lookup_dc dc dcl (i-1) k

> lookup_dc _ _ _ _ = " symbol not found "







> lookup_ctr ( nm : nml ) k | k > 0
>	= lookup_ctr nml (k-1)

> lookup_ctr ( nm : nml ) 0
>	= case nm of
>	 	Name inm         -> inm
>		Operator' op _ _ -> op

> lookup_ctr [] _
>	= " Constructor not found "







token display function used in debugging messages

> disp_tk :: Token -> String

> disp_tk ( Rvd str ) = str

> disp_tk ( Clr str ) = str

> disp_tk ( Bdr bdr ) = unparse_bdr bdr

> disp_tk ( IfxBdr str ) = str

> disp_tk ( IfxOp str ) = str

> disp_tk ( Scan_Err str ) = "Invalid token: " ++ str -- have to change this?



unparse signature

> unparse_sg :: Flagged_ITrm -> String

> unparse_sg ( Opnd ( Isgn sg )) = unparse_sg' sg

> unparse_sg ( Prs_Err mesg ) = mesg





> unparse_sg' ( Empty _ ) = ""

> unparse_sg' ( Extend dc sg _ )
>	= unparse_dc ( Empty [] ) dc ++ " ;\n" ++ unparse_sg' sg