{-
* 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_Core3 where
import Vtslib
import Core_datatype
import Sub_Core2
import Sub_Core1
select_sm_ty f sg i j
= case extract_dc j dc of
Symbol_dec tm _ | f -> uncurry_trm dc j tm
Axiom_dec tm _ | not f -> uncurry_trm dc j tm
Def _ tm _ | f -> uncurry_trm dc j tm
Def tm _ _ | not f -> Binary' Eq' (Sym 0 j [] [])
(uncurry_trm dc j tm) [] []
_ -> error ("select: " ++ show f ++ show i ++ show j ++ "|\n")
where
dc = nth_dec i sg
select_cn_ty :: ISgn -> Int -> Int -> Int -> ITrm
select_cn_ty sg i j k
= Sym 0 0 [] []
{-
= case extract_dc j dc of
Data dcL tmL _
-> if k == 0 then uncurry_trm dc j ty
else remake_ty ty4 dcL
(foldr make_app sms_base (reverse sms))
where
ty = foldr mk_pi (Constant (Univ 0) [] [])
( reverse dcL )
sms = mk_smsl dcL 0 []
ty1 = foldr make_app (Sym 0 0 [] []) ( reverse sms )
ty2 = foldr mk_fnspace (Sym 0 0 [] []) (tmL!!k-1)
d1 = Symbol_dec (Constant (Univ 0) [] [] ) []
ty3 = foldr mk_pi (Binder Pi d1 ty2 [] [])
( reverse dcL )
ty4 = uncurry_trm dc j ty3
sms_base = Const (length dcL) j 0 [] []
-- _ -> error "BadIndex" -- ** exn
where
dc = nth_dec i sg
-}
make_app tm1 tm2 = App tm1 tm2 [] []
{- return the type of a symbol -}
typ_of_sm sg i j
= shift_trm (get_share_map sg) i ty1
where
ty1 = select_sm_ty True sg i j -- partain: was true
{- return the type of a constructor -}
typ_of_cn sg i j k
= shift_trm (get_share_map sg) i ty1
where
ty1 = select_cn_ty sg i j k
{- return the type of an axiom -}
typ_of_axm sg i j
= shift_trm (get_share_map sg) i ty1
where
ty1 = select_sm_ty False sg i j -- partain: was false
{- extract the alternative types for a term -}
other_typ (Sym _ _ tmL _) = tmL
other_typ (App _ _ tmL _) = tmL
other_typ (Pair _ _ _ tmL _) = tmL
other_typ (Const _ _ _ tmL _) = tmL
other_typ (Binder _ _ _ tmL _) = tmL
other_typ (Unary _ _ tmL _) = tmL
other_typ (Binary' _ _ _ tmL _) = tmL
other_typ (Cond _ _ _ tmL _) = tmL
other_typ (Constant _ tmL _) = tmL
other_typ (Recurse _ _ tmL _) = tmL
{-
* return the type of a term. If a term has alternative type other
* than its natural type return that that.
*
-}
-- typ_of_trm :: ISgn -> ITrm -> ITrm
typ_of_trm sg tm
= case other_typ tm of
[] -> typ_of_trm' sg tm
(tm:_) -> tm
typ_of_trm' sg (Sym i j _ _)
= typ_of_sm sg i j
typ_of_trm' sg (Const i j k _ _)
= typ_of_cn sg i j k
typ_of_trm' sg (App tm1 tm2 _ _)
= case typ_of_trm sg tm1 of
Binder Pi dc tm3 _ _
-> subst_trm dc tm3 tm2
_ -> case typ_of_trm' sg tm1 of
Binder Pi dc tm3 _ _
-> subst_trm dc tm3 tm2
-- _ -> error "TypeOfTerm" -- ** exn
typ_of_trm' sg (Pair tm1 tm2 tm3 _ _)
= tm3
typ_of_trm' sg (Binder q dc tm _ _)
= typ_of_bnd sg q dc tm
typ_of_trm' sg (Constant c _ _)
= typ_of_cnt c
typ_of_trm' sg (Recurse _ tm _ _)
= tm
typ_of_trm' _ _
= Constant Bool' [] []
typ_of_bnd sg Forall dc tm
= Constant Bool' [] []
typ_of_bnd sg Exists dc tm
= Constant Bool' [] []
typ_of_bnd sg Imp dc tm
= Constant Bool' [] []
typ_of_bnd sg Pi dc tm
= Constant (Univ (max i j)) [] []
where
sg1 = Extend dc sg []
(Constant (Univ i) _ _) = typ_of_trm sg1 tm
(Constant (Univ j) _ _) = typ_of_trm sg (typ_of_dec dc)
typ_of_bnd sg Sigma dc tm
= Constant (Univ (max i j)) [] []
where
sg1 = Extend dc sg []
(Constant (Univ i) _ _) = typ_of_trm sg1 tm
(Constant (Univ j) _ _) = typ_of_trm sg (typ_of_dec dc)
typ_of_bnd sg Subtype dc tm
= Constant (Univ 0) [] []
typ_of_bnd sg Lambda dc tm
= Binder Pi dc (typ_of_trm (Extend dc sg []) tm) [] []
typ_of_bnd sg Choose dc tm
= Binder Subtype dc tm [] []
--typ_of_bnd _ _ _ _ = error "System_Error" -- ** exn
typ_of_cnt T = Constant Bool' [] []
typ_of_cnt F = Constant Bool' [] []
typ_of_cnt Bool' = Constant (Univ 0) [] []
typ_of_cnt (Univ i) = Constant (Univ (i+1)) [] []
{-
* evaluate a propositional term.
* A propositional term consists of:
* T, F, #fo d.t, #ex d.t, t1 #an t1, t1 #or t2, t1 #im t2, t1 = t2, #no t
* and locally bound symbols of type bool.
*
-}
-- eval :: ITrm -> Bool
eval (Constant T _ _) = True
eval (Constant F _ _) = False
--eval (Constant _ _ _) = error "EvalError" -- ** exn
eval (Binder Forall dc tm _ _)
= eval_quant forall dc tm
eval (Binder Exists dc tm _ _)
= eval_quant exists dc tm
eval (Binder Imp dc tm _ _)
= not (eval ( typ_of_dec dc)) || eval tm
--eval (Binder _ _ _ _ _)
-- = error "EvalError"
eval (Binary' And tm1 tm2 _ _)
= eval tm1 && eval tm2
eval (Binary' Or tm1 tm2 _ _)
= eval tm1 || eval tm2
eval (Binary' Eq' tm1 tm2 _ _)
= eval tm1 == eval tm2
eval (Unary Not tm _ _)
= not (eval tm)
eval (Cond dc tm1 tm2 _ _)
= eval (subst_trm dc tm1 (Constant T [] [])) &&
eval (subst_trm dc tm1 (Constant F [] []))
--eval _ = error "EvalError" -- ** exn
eval_quant f dc tm
= f (eval . subst_trm dc tm) (truth_table dc)
truth_table (Symbol_dec (Constant Bool' _ _ ) _)
= [ Constant T [] [] , Constant F [] [] ]
truth_table (Decpair dc1 dc2 _)
= make_pair (truth_table dc1) (truth_table dc2)
--truth_table _ = error "EvalError" -- ** exn
make_pair [] _ = []
make_pair (tm:tmL) l
= map (\ x -> Pair tm x (Constant Bool' [] []) [] []) l
++ make_pair tmL l
{-
* check to see if any symbols are defined at particular level
-}
occurs n (Sym i _ _ _)
= n == i
occurs n (App tm1 tm2 _ _)
= occurs n tm1 || occurs n tm2
occurs n (Pair tm1 tm2 tm3 _ _)
= occurs n tm1 || occurs n tm2 || occurs n tm3
occurs n (Binder _ dc tm _ _)
= occurs' n dc || occurs (n+1) tm
occurs n (Unary _ tm _ _)
= occurs n tm
occurs n (Binary' _ tm1 tm2 _ _)
= occurs n tm1 || occurs n tm2
occurs n (Cond dc tm1 tm2 _ _)
= occurs' n dc || occurs (n+1) tm1 || occurs (n+1) tm2
occurs n (Recurse tmL tm _ _)
= exists (occurs n) tmL || occurs n tm
occurs _ _ = False
occurs' n (Symbol_dec tm _)
= occurs n tm
occurs' n (Axiom_dec tm _)
= occurs n tm
occurs' n (Decpair dc1 dc2 _)
= occurs' n dc1 || occurs' (n+1) dc2
--occurs' _ _ = error "VTS_ERROR" -- ** exn
{-
* functions for retrieving and setting the information fields of
* term, decs and sigs.
-}
get_trm_att tm iL
= case subtm of
(Sym _ _ _ att) -> att
(App _ _ _ att) -> att
(Pair _ _ _ _ att) -> att
(Constant _ _ att) -> att
(Binder _ _ _ _ att) -> att
(Unary _ _ _ att) -> att
(Binary' _ _ _ _ att) -> att
(Cond _ _ _ _ att) -> att
(Const _ _ _ _ att) -> att
(Recurse _ _ _ att) -> att
where
(subtm,_) = select_trm tm iL
set_trm_att tm iL att
= replace_trm tm (set subtm) iL
where
set (Sym i j tmL _) = Sym i j tmL att
set (App tm1 tm2 tmL _) = App tm1 tm2 tmL att
set (Pair tm1 tm2 tm3 tmL _) = Pair tm1 tm2 tm3 tmL att
set (Constant c tmL _) = Constant c tmL att
set (Binder c tm1 tm2 tmL _) = Binder c tm1 tm2 tmL att
set (Unary c tm tmL _) = Unary c tm tmL att
set (Binary' c dc tm tmL _) = Binary' c dc tm tmL att
set (Cond dc tm1 tm2 tmL _) = Cond dc tm1 tm2 tmL att
set (Const i j k tmL _) = Const i j k tmL att
set (Recurse tmL tm tyL _) = Recurse tmL tm tyL att
(subtm,_) = select_trm tm iL
|