{- * 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 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