{-
 * Mon Nov  5 09:54:24 GMT 1990
 *
 * Implementation of untyped terms, signatures and declarations
 *
 * Each constructors last argument (of the tuple) is a list of
 * information attributes that the parser, unparsers, tactics etc use.
 *	
 * Each terms' next to last argument is a list of alternative types the the
 * term can have to its natutal type.
 *
-}

module Sub_Core1 where

import Vtslib

import Core_datatype


{-
 * Equality on trms, decs and sgns is just on the important parts, ie ignore
 * extra types and information
 *
-}


{-
 * Pairwise compare values of two lists 
 * ie, eq_pair_wise cmp [a1,...,an] [b1,...,bn] = cmp a1 b1 andalso ... cmp an bn 
-}

eq_pair_wise cmp [] [] = True

eq_pair_wise cmp ( x1 : l1 ) ( x2 : l2 ) 
	= cmp x1 x2 && eq_pair_wise cmp l1 l2

eq_pair_wise cmp _ _ = False





eq_trm (Sym i1 j1 _ _) (Sym i2 j2 _ _) 
	= i1 == i2 && j1 == j2

eq_trm (App tm1 tm2 _ _) (App tm3 tm4 _ _) 
	= eq_trm tm1 tm3 && eq_trm tm2 tm4

eq_trm (Pair tm1 tm2 tm3 _ _) (Pair tm4 tm5 tm6 _ _) 
	= eq_trm tm1 tm4 && eq_trm tm2 tm5 && eq_trm tm3 tm6

eq_trm (Binder b1 dc1 tm1 _ _) (Binder b2 dc2 tm2 _ _) 
	= b1 == b2 && eq_dec dc1 dc2 && eq_trm tm1 tm2 

eq_trm (Constant c1 _ _) (Constant c2 _ _) 
	= c1 == c2 

eq_trm (Unary c1 tm1 _ _) (Unary c2 tm2 _ _) 
	= c1 == c2 && eq_trm tm1 tm2 

eq_trm (Binary' c1 tm1 tm2 _ _) (Binary' c2 tm3 tm4 _ _) 
	= c1 == c2 && eq_trm tm1 tm3 && eq_trm tm2 tm4 

eq_trm (Cond dc1 tm1 tm2 _ _) (Cond dc2 tm3 tm4 _ _) 
	= eq_dec dc1 dc2 && eq_trm tm1 tm3 && eq_trm tm2 tm4

eq_trm (Const i1 j1 k1 _ _) (Const i2 j2 k2 _ _) 
	= i1 == i2 && j1 == j2 && k1 == k2 

eq_trm (Recurse tmL1 tm1 _ _) (Recurse tmL2 tm2 _ _) 
	= eq_pair_wise eq_trm tmL1 tmL2 && eq_trm tm1 tm2

eq_trm _ _ = False






eq_dec (Symbol_dec tm1 _) (Symbol_dec tm2 _) 
	= eq_trm tm1 tm2

eq_dec (Axiom_dec tm1 _) (Axiom_dec tm2 _) 
	= eq_trm tm1 tm2

eq_dec (Def tm1 tm2 _) (Def tm3 tm4 _) 
	= eq_trm tm1 tm3 && eq_trm tm2 tm4

eq_dec (Data dcL1 tmLL1 _) (Data dcL2 tmLL2 _) 
	= eq_pair_wise eq_dec dcL1 dcL2 && 
	  eq_pair_wise (eq_pair_wise eq_trm) tmLL1 tmLL2 

eq_dec (Decpair dc1 dc2 _) (Decpair dc3 dc4 _) 
	= eq_dec dc1 dc3 && eq_dec dc2 dc4

eq_dec _ _ = False



      
eq_sgn (Empty _) (Empty _) = True 

eq_sgn (Extend dc1 sg1 _) (Extend dc2 sg2 _) 
	= eq_dec dc1 dc2 && eq_sgn sg1 sg2
	
eq_sgn (Combine sg1 sg2 i1 _ _) (Combine sg3 sg4 i2 _ _) 
	= i1 == i2 && eq_sgn sg1 sg3 && eq_sgn sg2 sg4

eq_sgn (Share sg1 i1 j1 k1 _ _) (Share sg2 i2 j2 k2 _ _) 
	= i1 == i2 && j1 == j2 && j1 == j2 && eq_sgn sg1 sg2

eq_sgn _ _ = False





{-
 * Extract a subterm from a term along with a list of all the 
 * declarations encounted on the spine down to the subterm.
 * generate an exception if the index does not point at a valid subterm
 * 
-}

-- select_trm :: ITrm -> [ Int ] -> ( ITrm , [ IDec ] )


select_trm tm iL  
	= sel_trm iL tm [] 
	  where
	  sel_trm :: [ Int] -> ITrm -> [ IDec ] -> ( ITrm , [ IDec ] )

	  sel_trm (i:iL) (App tm1 tm2 _ _) dcL 
		= sel_trm iL ([tm1,tm2]!!i) dcL

	  sel_trm (i:iL) (Pair tm1 tm2 _ _ _) dcL 
		= sel_trm iL ([tm1,tm2]!!i) dcL

	  sel_trm (i:iL) (Binder _ dc tm _ _) dcL 
		| i==0 = sel_dec iL dc dcL 
		| i==1 = sel_trm iL tm (dc:dcL)

	  sel_trm (0:iL) (Unary _ tm _ _) dcL 
		= sel_trm iL tm dcL

	  sel_trm (i:iL) (Binary' _ tm1 tm2 _ _) dcL 
		= sel_trm iL ([tm1,tm2]!!i) dcL

	  sel_trm (i:iL) (Cond (dc @ (Axiom_dec tm inf)) tm1 tm2 _ _) dcL 
		| i==0 = sel_dec iL dc dcL
		| i/=0 = sel_trm iL ([tm1,tm2]!!(i-1)) (dc1:dcL) 
	          	 where
		 	 dc1 = if i==1 
				then dc
				else if i==2
				       then Axiom_dec (Unary Not tm [] inf) []
				       else error "sel_trm"

	  sel_trm (i:iL) (Recurse tmL _ _ _) dcL 
		= sel_trm iL (tmL!!i) dcL

	  sel_trm [] tm dcL = (tm,dcL)

--          sel_trm _ _ _ = error "Subterm"  -- ** exn


	  sel_dec :: [ Int ] -> IDec -> [ IDec ] -> ( ITrm , [ IDec ] )

	  sel_dec (0:iL) (Symbol_dec tm _) dcL 
		= sel_trm iL tm dcL

	  sel_dec (0:iL) (Axiom_dec tm _) dcL 
		= sel_trm iL tm dcL

	  sel_dec (i:iL) (Decpair dc1 dc2 _) dcL 
		| i==0 = sel_dec iL dc1 dcL 
	        | i==1 = sel_dec iL dc2 (dc1:dcL)

--	  sel_dec _ _ _ = error "Subterm" -- ** exn







{-
 * replace a subterm of a term. this function assumes that the replacement
 * subterm is of an appropriate type and defined on the right signature.
 *
-} 

-- replace_trm :: ITrm -> ITrm -> [ Int ] -> ITrm

replace_trm tm1 tm2 iL 
	= rep_trm iL tm1 
	  where
	  swap 0 (_:xL) y 
		= y : xL

	  swap i (x:xL) y 
		= x : swap (i-1) xL y

--	  swap _ _ _ = error "Subterm" -- ** exn

	  rep_trm :: [Int] -> ITrm -> ITrm

	  rep_trm (i:iL) (App tm1 tm2 tyL inf) 
		| i==0 = App (rep_trm iL tm1) tm2 tyL inf 
		| i==1 = App tm1 (rep_trm iL tm2) tyL inf

	  rep_trm (i:iL) (Pair tm1 tm2 tm3 tyL inf) 
		| i==0 = Pair (rep_trm iL tm1) tm2 tm3 tyL inf
		| i==1 = Pair tm1 (rep_trm iL tm2) tm3 tyL inf

	  rep_trm (i:iL) (Binder q dc tm tyL inf) 
		| i==0 = Binder q (rep_dec iL dc) tm tyL inf
		| i==1 = Binder q dc (rep_trm iL tm) tyL inf

	  rep_trm (i:iL) (Unary c tm tyL inf) 
		| i==0 = Unary c (rep_trm iL tm) tyL inf

	  rep_trm (i:iL) (Binary' c tm1 tm2 tyL inf) 
		| i==0 = Binary' c (rep_trm iL tm1) tm2 tyL inf
		| i==1 = Binary' c tm1 (rep_trm iL tm2) tyL inf

	  rep_trm (i:iL) (Cond dc tm1 tm2 tyL inf) 
		| i==0 = Cond (rep_dec iL dc) tm1 tm2 tyL inf
		| i==1 = Cond dc (rep_trm iL tm1) tm2 tyL inf
		| i==2 = Cond dc tm1 (rep_trm iL tm2) tyL inf

	  rep_trm (i:iL) (Recurse tmL tm tyL inf) 
		= Recurse tmL1 tm tyL inf 
		  where
		  tmL1 = swap i tmL (rep_trm iL (tmL!!i))

	  rep_trm [] _ = tm2

	  rep_trm iL _ = error ( "iL(len):" ++ show ( length iL) ++ "\niL:" ++  concat ( map show iL ) ++ "|" ) --"Subterm" -- ** exn



	  rep_dec (0:iL) (Symbol_dec tm inf) 
		= Symbol_dec (rep_trm iL tm) inf
		 
 	  rep_dec (0:iL) (Axiom_dec tm inf) 
		= Axiom_dec (rep_trm iL tm) inf

	  rep_dec (i:iL) (Decpair dc1 dc2 inf) 
		| i==0 = Decpair (rep_dec iL dc1) dc2 inf
		| i==1 = Decpair dc1 (rep_dec iL dc2) inf

--	  rep_dec _ _ = error "Subterm" -- ** exn






{-
 * map two functions (one for symbol and one for constructors) over
 * a term, applying then to all the non localally bound symbols and
 * constructors in the term. Return two functions: the first applies to
 * terms; the second to declarations
 *
-}

type Sym_map = Int -> Int -> Int -> [ ITrm ] -> [ Attribute ] -> ITrm
	
type Const_map = Int -> Int -> Int -> Int -> [ ITrm ] -> [ Attribute ] -> ITrm


-- map_fn :: Sym_map -> Const_map -> (( ITrm -> ITrm ) , ( IDec -> IDec ))

map_fn map_symbol map_const
	= (map_trm 0, map_dec 0) 
	  where
	  map_trm n (Sym i j tyL inf) 
		= if i < n then Sym i j tyL1 inf
			   else map_symbol n i j tyL1 inf
		  where
		  tyL1 = map (map_trm n) tyL 

	  map_trm n (Const i j k tyL inf) 
		= if i < n then Const i j k tyL1 inf
			   else map_const n i j k tyL1 inf
		  where
		  tyL1 = map (map_trm n) tyL 

	  map_trm n (Constant c tyL inf) 
		= Constant c (map (map_trm n) tyL) inf

	  map_trm n (App tm1 tm2 tyL inf) 
		= App (map_trm n tm1) (map_trm n tm2) (map (map_trm n) tyL) inf

	  map_trm n (Pair tm1 tm2 tm3 tyL inf) 
		= Pair (map_trm n tm1) (map_trm n tm2) (map_trm n tm3)
			(map (map_trm n) tyL) inf

	  map_trm n (Binder q dc tm tyL inf) 
		= Binder q (map_dec n dc) (map_trm (n+1) tm)
			  (map (map_trm n) tyL) inf

	  map_trm n (Unary c tm tyL inf) 
		= Unary c (map_trm n tm) (map (map_trm n) tyL) inf

	  map_trm n (Binary' c tm1 tm2 tyL inf) 
		= Binary' c (map_trm n tm1) (map_trm n tm2) 
			(map (map_trm n) tyL) inf

	  map_trm n (Cond dc tm1 tm2 tyL inf) 
		= Cond dc1 tm3 tm4 tyL1 inf 
		  where
		  dc1 = map_dec n dc
		  tm3 = map_trm (n+1) tm1
		  tm4 = map_trm (n+1) tm2
		  tyL1 = map (map_trm n) tyL

	  map_trm n (Recurse tmL tm tyL inf) 
		= Recurse tmL1 tm1 tyL1 inf 
		  where
		  tmL1 = map (map_trm n) tmL
		  tm1  = map_trm n tm
		  tyL1 = map (map_trm n) tyL

	  map_trm n (Tagid tg tg_argL)
		= Tagid tg tg_argL  -- need to shift tg_argL

	  map_trm n (ITrm_Err mesg )
		= ITrm_Err mesg



	  map_dec n (Symbol_dec tm inf) 
		= Symbol_dec (map_trm n tm) inf

	  map_dec n (Axiom_dec tm inf) 
		= Axiom_dec (map_trm n tm) inf
	
	  map_dec n (Decpair dc1 dc2 inf) 
		= Decpair (map_dec n dc1) (map_dec (n+1) dc2) inf

	  map_dec n (Def tm1 tm2 inf) 
		= Def (map_trm n tm1) (map_trm n tm2) inf

	  map_dec n (Data dcL tmLL inf) 
		= Data dcl' tmLL' inf'
		  where
		  (dcl', tmLL', inf') = (map_data n dcL tmLL inf)


	  map_data n [] tmLL inf 
		= ([], map (map (map_trm (n+1))) tmLL,inf)

	  map_data n (dc:dcL) tmLL inf 
		= (map_dec n dc:dcL,tmLL1,inf1) 
		  where
		  (dcL1,tmLL1,inf1) = map_data (n+1) dcL tmLL inf





{- return the nth sub-signature of a signature. -}

nth_sgn 0 sg = sg

nth_sgn i (Extend _ sg _) 
	= nth_sgn (i-1) sg

nth_sgn i (Combine sg1 sg2 k _ _) 
	= if i<k then nth_sgn (i-1) sg2 
		 else nth_sgn (i-k-1) sg1

nth_sgn i (Share sg _ _ _ _ _) 
	= nth_sgn (i-1) sg

--nth_sgn i (Empty _) 
--	= error	"Nth_Sgn" -- ** exn







{- return the ith declaration of a signature -}

nth_dec i sg 
	= case nth_sgn i sg of
	      Extend dc _ _ -> dc
--	      _ 	    -> error "NthDec" -- ** exn





{- Compute the length of a signature -}

-- len_sgn :: ISgn -> Int

len_sgn (Empty _) = 0

len_sgn (Extend _ sg _) = 1 + len_sgn sg

len_sgn (Combine sg _ k _ _) = 1+ k + len_sgn sg

len_sgn (Share sg _ _ _ _ _) = 1 + len_sgn sg