itrm building functions used by parser

> module Build_itrm where

> import Char(isDigit)--1.3
> import Core_datatype

> import Type_defs

> import Attributes

> import Unparse  -- for debugging purposes only

> import Kernel

> import Sub_Core1

> import Sub_Core2

> import Sub_Core3

> import Sub_Core4

> import Vtslib

rewrite for continuation based version of read?

> sym' :: String -> String -> Flagged_ITrm

> sym' str1 str2
>	= if isint str1 && isint str2
>		then Opnd ( Itrm  ( Sym no1 no2 [] [sym_ind] ))
>		else Prs_Err ( errstr ++ " is not an integer " )
>	  where
>	  no1 = read str1
>	  no2 = read str2
>	  isint = and . ( map isDigit )
>	  errstr = if isint str1 then str2 else str1




const' needs to be similar to above

> const' :: String -> String -> String -> Flagged_ITrm

> const' str1 str2 str3
>	= Opnd ( Itrm ( Const no1 no2 no3 [] [sym_ind]))
>	  where
>	  no1 = read str1
>	  no2 = read str2
>	  no3 = read str3





> binder' bnd_con ( Opnd ( Idec dc )) ( Opnd ( Itrm tm ))
>	= ( Opnd . Itrm ) ( Binder bnd_con dc tm [] [pre_bdr] )

improve err mess

> binder' _ ( Prs_Err x ) _ = Prs_Err x

> binder' _ _ ( Prs_Err x ) = Prs_Err x





> cond' :: Flagged_ITrm -> Flagged_ITrm -> Flagged_ITrm -> Flagged_ITrm

> cond' ( Prs_Err x ) _ _ = Prs_Err x

> cond' _ ( Prs_Err x ) _ = Prs_Err x

> cond' _ _ ( Prs_Err x ) = Prs_Err x

> cond' ( Opnd ( Idec dc ) ) ( Opnd ( Itrm tm1 ) ) ( Opnd ( Itrm tm2 )) 
>	= Opnd ( Itrm ( Cond dc tm1 tm2 [] [] ))




> let' ( Prs_Err x ) _ _ = Prs_Err x

> let' _ ( Prs_Err x ) _ = Prs_Err x

> let' _ _ ( Prs_Err x ) = Prs_Err x

> let' ( Opnd ( Idec dc)) ( Opnd ( Itrm tm1)) ( Opnd ( Itrm tm2 )) 
>	= opnd ( App ( Binder Lambda dc tm2 [] [] ) tm1 [] [let_stl] )

> let' ( Opr _ _ _ ) _ _ = error "1"
> let' _ ( Opr _ _ _ ) _ = error "2"
> let' _ _ ( Opr _ _ _ ) = error "3"
> let' _ ( Opnd ( PApp _ _ _ )) _ = error "4.1"
> let' _ ( Opnd ( PairApp _ ) ) _ = error "4.2"
> let' _ ( Opnd ( ParIfx _ _) ) _ = error "4.3"
> let' _ ( Opnd ( TypApp _ ) ) _ = error "4.4"
> let' _ ( Opnd ( Itrm _ ) ) _ = error "4.5"
> let' _ ( Opnd ( Idec _ ) ) _ = error "4.6"
> let' _ ( Opnd _ ) _ = error "5"
> let' _ _ ( Opnd _ ) = error "6"







remove dummy application operators

> app' ( Opr ( Spl "" ) _ _ ) x = x

> app' x ( Opr ( Spl "" ) _ _ ) = x

case analysis on special operators
First case is for infix binders X -> etc ( prefix binders are dealt with
by term' in parser )

infix binders x , -> etc

> app' ( Opr ( OpBdr bdr ) _ _ )  ( Opnd ( Idec dc ))  
> 	= Opnd ( PApp bdr dc False )

> app' ( Opr ( OpBdr bdr ) _ _ )  ( Opnd ( Itrm srt ))  
> 	= Opnd ( PApp bdr dc True )
>	  where
>	  dc = Symbol_dec srt [ sym_nm ( Name "_" ) ]

> app' (Opnd ( PApp bdr dc anon )) ( Opnd ( Itrm tm ))
> 	= opnd ( Binder bdr dc shft_tm [] [ifx_bdr] ) 
>	  where
>	  shft_tm | anon     = shift_trm [] 1 tm
>		  | not anon = tm 

infix operators , /\. \/ etc

> app' ( Opr ( OpIfx op ) _ _ ) ( Opnd ( Itrm tm ))
>	= Opnd ( ParIfx op tm )

> app' ( Opnd ( ParIfx op tm1 ) ) ( Opnd ( Itrm tm2 )) 
> 	= opnd ( Binary' op tm1 tm2 [] [] )


PairApp is , applied to first argument only

> app' ( Opr ( Spl "," ) _ _ )  ( Opnd ( Itrm tm1 )) 
>	= Opnd ( PairApp tm1 )

form pair when second argument found
type set to U-1 to indicate it has not yet been defined. Will be defined
explicitely by "typed" (see following clause) or will be deduced by
`build_trm'' when proper term is constructed.

> app' ( Opnd ( PairApp tm1 )) ( Opnd ( Itrm tm2 )) 
>	= Opnd ( Itrm pairtm ) 
> 	  where
>	  pairtm = Pair tm1 tm2 pdt [] [pr_untyped]
>	  pdt = Constant ( Univ (-1) ) [] [] 

TypApp is 'typed' applied to its first argument
(does it need flagged_itrm as an argument in general?)

> app' ( Opr ( Spl "typed" ) _ _ ) opnd1
>	= Opnd ( TypApp opnd1 )

add other TypApp cases for other types (recurse )
(Note that pr_typed will replaced pr_untyped in attribute list)

> app' ( Opnd ( TypApp ( Opnd ( Itrm ( Pair tm1 tm2 _ a b )))))
>							( Opnd ( Itrm srt ))
>	= Opnd ( Itrm ( Pair tm1 tm2 srt a [pr_typed] ))

prefix not

> app' ( Opr ( Spl "Not" ) _ _ ) ( Opnd ( Itrm tm ))
>	= opnd ( Unary Not tm [] [] )

":" operator

> app' ( Opr ( Spl ":" ) _ _ ) ( Opnd ( Itrm tm ))
>	= Opnd ( ParColon tm )

> app' ( Opnd ( ParColon tm1 )) ( Opnd ( Itrm tm2 ))
>	= opnd ( add_type tm1 tm2 )

four permutations for operators and operands

> app' ( Opnd ( Itrm tm1 )) ( Opnd ( Itrm tm2 )) 
>	= opnd ( App tm1 tm2 [] [] ) 

> app' ( Opr ( OpItrm op ) stl _ ) ( Opnd ( Itrm tm )) 
>	= opnd ( App op tm [] [ op_stl stl ] )

> app' ( Opnd ( Itrm tm )) ( Opr ( OpItrm op ) _ _ ) -- happen?
>	= opnd ( App tm op [] [] ) 

?what happens to style for second operator here?

> app' ( Opr ( OpItrm op1 ) stl _ ) ( Opr ( OpItrm op2 ) _ _ ) 
>	= opnd ( App op1 op2 [] [ op_stl stl ] )

> app' ( Prs_Err mess ) _ = Prs_Err mess

> app' _ ( Prs_Err mess ) = Prs_Err mess

> app' x y = error ( "app' y: " ++ unparse ( Empty []) y ++ "\nx: " ++ unparse (Empty [] ) x )






> opnd :: ITrm -> Flagged_ITrm

> opnd = Opnd . Itrm


include following as optimisation?

> fetch_arg :: Flagged_ITrm -> ITrm

> fetch_arg ( Opnd ( Itrm tm )) = tm

> fetch_arg ( Opr ( OpItrm op ) _ _ ) = op



> decpair' _ ( Prs_Err x ) _ = Prs_Err x

> decpair' _ _ ( Prs_Err x ) = Prs_Err x

> decpair' att ( Opnd ( Idec dc1 )) ( Opnd ( Idec dc2 ))
>	= ( Opnd . Idec ) ( Decpair dc1 dc2 att )



> symbol_dec' ( Opnd ( Itrm tm )) nm attL
>	= ( Opnd . Idec ) ( Symbol_dec tm ( sym_nm nm : attL ) )

> symbol_dec' ( Prs_Err mess ) nm _ = Prs_Err mess





> data' ( _ , [ Prs_Err mesg ] ) _
>	= Prs_Err mesg

> data' ( type_nm , dcl ) ctr_defs
>	= case ctrs of
>		Ok ( ctr_nml , ctr_srtl ) 
>			 -> ( Opnd . Idec ) ( Data ( clear dcl ) ctr_srtl att )
>			    where
>         		    att = [ dat_nm ( type_nm : ctr_nml ) ]	
>		Bad mesg -> Prs_Err mesg
>	  where
>	  ctrs = ctr' [] [] ctr_defs
>	  clear ( Opnd ( Idec dc ) : dcl ) = dc : clear dcl
>	  clear [] = []




> ctr' nml argll (( nm , argl ) : ctrl )
>	= case checked_args of
>		Ok iargl -> ctr' ( nm : nml ) ( iargl : argll ) ctrl 
>	 	Bad mesg -> Bad mesg
>	  where
>	  checked_args = check_arg [] argl

> ctr' nml argll []
>	= Ok ( reverse nml , reverse argll )



> check_arg tml ( Opnd ( Itrm tm ) : argl )
>	= check_arg ( tm : tml ) argl

> check_arg tml []
>	= Ok ( reverse tml )

> check_arg _ ( Prs_Err mesg : argl )
>	= Bad mesg



> extend' ( Opnd ( Idec dc )) ( Opnd ( Isgn sg ))
>	= Opnd ( Isgn ( Extend dc sg [] ))	

> extend' _ ( Prs_Err mesg )
>	= Prs_Err mesg

> extend' ( Prs_Err mesg ) _
>	= Prs_Err mesg




> def' ( _ , [ Prs_Err mesg ] ) _ _
>	= Prs_Err mesg

> def' _ ( Prs_Err mesg ) _
>	= Prs_Err mesg

> def' ( nm , fmls ) ( Opnd ( Itrm rhs )) att
>	= ( Opnd . Idec ) ( Def tm srt [ sym_nm nm , att ] )
>	  where
>	  tm = make_tm fmls rhs
>	  srt = Constant ( Univ 0 ) [] [] -- temporary - need sort fn


> make_tm ( Opnd ( Idec dc ) : dcl ) rhs
>	= Binder Lambda dc ( make_tm dcl rhs ) [] []

> make_tm [] rhs
>	= rhs


> add_sg_att ( Prs_Err mesg ) _ = Prs_Err mesg

> add_sg_att ( Opnd ( Isgn ( Empty attl ))) att 
>	= Opnd ( Isgn ( Empty ( att : attl )))

> add_sg_att ( Opnd ( Isgn ( Extend  dc sg attl ))) att 
>	= Opnd ( Isgn ( Extend dc sg ( att : attl )))






> recurse' _ ( Prs_Err mesg ) = Prs_Err mesg

> recurse' tml ( Opnd ( Itrm srt ))
>	= case clr [] tml of
>		Ok itml  -> Opnd ( Itrm ( Recurse itml srt [] [rcrs_stl] ))
>	        Bad mesg -> Prs_Err mesg 
>	  where
>	  clr itml (( Opnd ( Itrm tm )) : tml ) = clr ( tm : itml ) tml
>	  clr itml [] = Ok itml 
>	  clr _ ( Prs_Err mesg : _ ) = Bad mesg





> tag' tg tgL
>	= case check tgL of
>		Ok _     -> Opnd ( Itrm ( Tagid tg tgL ))
>	 	Bad mesg -> Prs_Err mesg
>	  where
>	  check ( Tg_Trm ( TM _ _ _ ) : oth )    = check oth
>	  check ( Tg_Trm ( TM_Err mesg ) :oth )  = Bad mesg
>	  check ( Tg_Thm ( TH _ _ ) : oth )      = check oth
>	  check ( Tg_Thm ( TH_Err mesg ) : oth ) = Bad mesg
>	  check ( Tg_Int iL : oth )              = check oth
>	  check []                               = Ok [] -- list is given in tgL