{-
* kernel for vts90
*
* Tue Nov 6 14:35:39 GMT 1990
*
* For information about the typing rules for the construction of
* term, signatures, declarations an signatures see the file
* doc/abstract_logic/rules3.tex
*
-}
module Kernel where
import Core_database
import Dcore
import Sub_Core1
import Sub_Core2
import Sub_Core3
import Sub_Core4
import Vtslib
import Core_datatype
{- for tags -- terms and theorems now defined in core_datatype -}
--data Trm = TM ITrm ITrm ISgn | {- the term, its type, and signature -}
-- TM_Err String
data Sgn = SG ISgn |
SG_Err String
data Dec = DC IDec ISgn | {- the declaration, and its signature -}
DC_Err String
--data Thm = TH ITrm ISgn | {- the theorem, and its signature -}
-- TH_Err String
{-
(*and Mph = MP of mapping list*)
-}
{- Symbol formation -}
symbol (SG sg) i j
= if share_map !! i == i
then TM (Sym i j [] []) (typ_of_sm sg i j) sg
else TM_Err "Malformed symbol"
where
share_map = get_share_map sg
{- Universe formation -}
universe (SG sg) i
| i>=0 = TM (Constant (Univ i) [] []) (Constant (Univ (i+1)) [] []) sg
| i<0 = TM_Err "Malformed Universe"
{- Pi formation -}
pi' (TM tm (Constant (Univ i) _ _) (Extend dc sg _))
= case typ_of_trm sg (typ_of_dec dc) of
Constant (Univ j) _ _
-> TM tm1 tm2 sg
where
tm1 = Binder Pi dc tm [] []
tm2 = Constant (Univ (max i j)) [] []
_ -> TM_Err "Malformed pi expression"
pi' _ = TM_Err "Sort of pi exression is not a universe"
{- Pi introduction -}
lambda (TM tm1 tm2 (Extend dc sg _))
= if is_sym_dec dc
then
TM (Binder Lambda dc tm1 [] []) (Binder Pi dc tm2 [] []) sg
else
TM_Err "lambda: invalid declaration"
lambda (TM_Err mesg ) = TM_Err mesg
lambda _ = TM_Err "Malformed lambda expression"
{- PI elimination -}
appl (TM tm1 (Binder Pi dc tm2 _ _) sg1) (TM tm3 tm4 sg2)
= if eq_sgn sg1 sg2 && eq_trm (typ_of_dec dc) tm4
then
TM (App tm1 tm3 [] []) (subst_trm dc tm2 tm3) sg1
else
TM_Err "Malformed application"
appl _ _
= TM_Err "Malformed application (2)"
{- Sigma formation -}
sigma (TM tm (Constant (Univ i) _ _) (Extend dc sg _))
= case typ_of_trm sg (typ_of_dec dc) of
Constant (Univ j) _ _
-> TM tm1 tm2 sg
where
tm1 = Binder Sigma dc tm [] []
tm2 = Constant (Univ (max i j)) [] []
_ -> TM_Err "Malformed sigma"
sigma _ = TM_Err "Malformed sigma (2)"
{- Sigma introduction -}
pair (TM tm1 tm2 sg1) (TM tm3 tm4 sg2) (TM tm7@(Binder Sigma dc tm5 _ _) tm6 sg3)
= if eq_sgn sg1 sg2 && eq_sgn sg2 sg3 &&
eq_trm tm2 (typ_of_dec dc) && eq_trm tm4 (subst_trm dc tm5 tm1)
then
TM (Pair tm1 tm3 tm7 [] []) tm7 sg1
else
TM_Err "Malformed pair"
pair _ _ _ = TM_Err "Malformed pair (2)"
{- Subtype formation -}
subtype (TM tm (Constant Bool' _ _) (Extend dc sg _))
= if eq_trm (typ_of_trm sg (typ_of_dec dc)) (Constant (Univ 0) [] [])
then
TM (Binder Subtype dc tm [] []) (Constant (Univ 0) [] []) sg
else
TM_Err "Malformed subtype"
subtype _ = TM_Err "Malformed subtype (2)"
{- Subtype introduction -}
into (TM tm1 tm2 sg1) (TM tm3@(Binder Subtype dc tm4 _ _) _ sg2) (TH tm5 sg3)
= if eq_sgn sg1 sg2 && eq_sgn sg2 sg3 &&
eq_trm (typ_of_trm sg2 (typ_of_dec dc)) (Constant (Univ 0) [] []) &&
eq_trm tm2 (typ_of_dec dc) && eq_trm tm5 (subst_trm dc tm4 tm1)
then
TM (add_type tm1 tm3) tm3 sg1
else
TM_Err "Malformed subtype introduction "
into _ _ _ = TM_Err "Malformed subtype introduction (2)"
{- Subtype elimination -}
outof (TM tm1 (Binder Subtype dc _ _ _) sg)
= TM (add_type tm1 tm2) tm2 sg
where
tm2 = typ_of_dec dc
outof _ = TM_Err " outof: argument invalid"
{- Bool formation -}
bool_sm (SG sg)
= TM (Constant Bool' [] []) (Constant (Univ 0) [] []) sg
{- Bool introduction -}
{- true formation -}
true_sm (SG sg) = TM (Constant T [] []) (Constant Bool' [] []) sg
{- false formation -}
false_sm (SG sg) = TM (Constant F [] []) (Constant Bool' [] []) sg
{- Universal quantification formation -}
universal (TM tm (Constant Bool' _ _) (Extend dc sg _))
= if is_sym_dec dc
then
TM (Binder Forall dc tm [] []) (Constant Bool' [] []) sg
else
TM_Err "Malformed universal quantification"
universal _ = TM_Err "Malformed universal quantification (2)"
{- Existential quantification formation -}
existential (TM tm (Constant Bool' _ _) (Extend dc sg _))
= if is_sym_dec dc
then
TM (Binder Exists dc tm [] []) (Constant Bool' [] []) sg
else
TM_Err "Malformed existential quantification"
existential _ = TM_Err "Malformed existential quantification (2)"
{- Implication formation -}
implication (TM tm (Constant Bool' _ _) (Extend dc sg _))
= if is_axm_dec dc
then
TM (Binder Imp dc tm [] []) (Constant Bool' [] []) sg
else
TM_Err "Malformed Implication"
implication _ = TM_Err "Malformed Implication (2)"
{- And formation -}
conjunction (TM tm1 (Constant Bool' _ _) sg1) (TM tm2 (Constant Bool' _ _) sg2)
= if eq_sgn sg1 sg2
then
TM (Binary' And tm1 tm2 [] []) (Constant Bool' [] []) sg1
else
TM_Err "Malformed conjunction"
conjunction _ _ = TM_Err "Malformed conjunction (2)"
{- Or formation -}
disjunction (TM tm1 (Constant Bool' _ _) sg1) (TM tm2 (Constant Bool' _ _) sg2)
= if eq_sgn sg1 sg2
then
TM (Binary' Or tm1 tm2 [] []) (Constant Bool' [] []) sg1
else
TM_Err "Malformed disjunction "
disjunction _ _ = TM_Err "Malformed disjunction (2)"
{- Not formation -}
negation (TM tm (Constant Bool' _ _) sg)
= TM (Unary Not tm [] []) (Constant Bool' [] []) sg
negation _ = TM_Err "Malformed negation"
{- Eq formation -}
equal (TM tm1 _ sg1) (TM tm2 _ sg2)
= if eq_sgn sg1 sg2
then
TM (Binary' Eq' tm1 tm2 [] []) (Constant Bool' [] []) sg1
else
TM_Err "Malformed equality"
{- Issustype formation -}
issubtype (TM tm1 (Constant (Univ 0) _ _) sg1)
(TM tm2 (Constant (Univ 0) _ _) sg2)
= if eq_sgn sg1 sg2
then
TM (Binary' Issubtype tm1 tm2 [] []) (Constant Bool' [] []) sg1
else
TM_Err "Malformed subtype"
issubtype _ _ = TM_Err "Malformed subtype (2)"
{- Bool elimination (ie Conditionals) -}
conditional (TM tm1 tm2 (Extend dc1 sg1 _)) (TM tm3 tm4 (Extend dc2 sg2 _))
= if eq_sgn sg1 sg2 &&
eq_trm tm2 tm4 &&
eq_trm (Unary Not (typ_of_dec dc1) [] []) (typ_of_dec dc2)
then
TM (Cond dc1 tm1 tm3 [] []) tm2 sg1
else
TM_Err "Malformed conditional"
conditional _ _ = TM_Err "Malformed conditional (2)"
{- Hilbert epsilon operator introduction -}
choose (TH (Binder Exists dc tm _ _) sg)
= if eq_trm (typ_of_trm sg (typ_of_dec dc)) (Constant (Univ 0) [] [])
then
TM (Binder Choose dc tm [] []) (Binder Subtype dc tm [] []) sg
else
TM_Err "epsilon operator error"
choose _ = TM_Err "epsilon operator error (2)"
{- Datatype constructor formation and introduction -}
constructor (SG sg) i j k
= if share_map !! i == i
then
TM (Const i j k [] []) (typ_of_cn sg i j k) sg
else
TM_Err "Malformed constructor"
where
share_map = get_share_map sg
{- Datatype elimination -}
recurse tmL (TM (tm @ (Binder Pi (Symbol_dec tm1 _) _ _ _)) _ sg)
= if forall ok (zip tmL tyL)
then
TM (Recurse (map fst tmL) tm [] []) tm sg
else
TM_Err "recurse error"
where
(tyL,_) = clause_types sg tm1 tm
ok (TM _ tm1 sg1 , tm2) = eq_sgn sg sg1 && eq_trm tm1 tm2
fst (TM tm _ _) = tm
recurse _ _ = TM_Err "recurse error (2)"
{- Widen type -}
widen (TM tm1 tm2 sg1) (TH (Binary' Issubtype tm3 tm4 _ _) sg2)
= if eq_sgn sg1 sg2 && eq_trm tm2 tm3
then
TM (add_type tm1 tm4) tm4 sg1
else
TM_Err "widen: error"
widen _ _ = TM_Err "widen: error (2)"
{- Set the attributes of a term -}
set_Trm_att (TM tm1 tm2 sg) iL att
= TM (set_trm_att tm1 iL att) tm2 sg
set_Trm_att (TM_Err mesg) _ _ = TM_Err mesg
{- Get the attributes of a term -}
get_Trm_att (TM tm _ _) iL
= get_trm_att tm iL
{- return the internal representation of a term -}
internal_Trm (TM tm1 tm2 sg) = (tm1,tm2,sg)
{- Read a term in from the database -}
restore_Trm s = TM_Err "restore_Trm unimplemented"
{- The empty signature -}
empty = SG (Empty [])
{- Extend a signature with a declaration -}
extend (DC dc sg1) (SG sg2)
= if eq_sgn sg1 sg2
then
SG (Extend dc sg2 [])
else
SG_Err "Malformed signature extension"
extend _ _ = SG_Err "Invalid declaration in signature"
{- Combine two signatures -}
combine (SG sg1) (SG sg2)
= SG (Combine sg1 sg2 (len_sgn sg2) (sm2 ++ map update sm1) [])
where
sm1 = get_share_map sg1
sm2 = get_share_map sg2
offset = length sm2
update i = i + offset
{- Share two sub-sigantures within a signature -}
share (SG sg) i j
= if eq_sgn sg1 sg2
then
SG (Share sg i j (len_sgn sg2)
(addequivL i j (len_sgn sg2) sm) [])
else
SG_Err "sg: Share"
where
sg1 = nth_sgn i sg
sg2 = nth_sgn j sg
sm = get_share_map sg
{- Return the attributes of a signature -}
get_Sgn_att (SG sg) = get_sgn_att sg
{- Set the attributes of a signature -}
set_Sgn_att (SG sg) att = (SG (set_sgn_att sg att))
{- Return the internal representation of a signature -}
internal_Sgn (SG sg) = sg
{- Restore a signature from the database -}
restore_Sgn s = SG_Err "restore_Sgn unimplemented"
{- declare a new symbol -}
symbol_dec (TM tm1 tm2 sg)
= case typ_of_trm sg tm2 of
Constant (Univ _) _ _ -> DC (Symbol_dec tm1 []) sg
_ -> DC_Err "Malformed symbol declaration"
{- declare a new axiom -}
axiom_dec (TM tm (Constant Bool' _ _) sg)
= DC (Axiom_dec tm []) sg
axiom_dec _ = DC_Err "Malformed axiom declaration"
{- Define a new symbol -}
def (TM tm1 tm2 sg)
= DC (Def tm1 tm2 []) sg
make_data tmLL (TH tm sg)
= if forall (forall (wf_param sg1)) tmLL
then
if exists (eq_trm tm) non_empty_thms
then
DC (Data [] (map (map fst) tmLL) []) sg
else
DC_Err "Malformed datatype"
else
DC_Err "Malformed datatype (2)"
where
non_empty_thms = map gen_proof (filter is_base tmLL)
wf_param sg1 (TM tm1 (Constant (Univ _) _ _) sg2)
= eq_trm tm1 (Sym 0 0 [] []) || not (occurs 0 tm1)
wf_param _ _ = False
mk_exists tm1 tm2
= Binder Exists (Symbol_dec tm3 []) tm4 [] []
where
tm3 = shift_trm [] (-1) tm1
tm4 = shift_trm [] 1 tm2
fst (TM tm _ _) = tm
is_base tmL = not (exists (eq_trm (Sym 0 0 [] [])) (map fst tmL))
gen_proof tmL = foldr mk_exists (Constant T [] [])
( reverse (map fst tmL))
sg1 = Extend (Symbol_dec (Constant (Univ 0) [] []) []) sg []
polydata (DC (Data dcL tmLL _) (Extend dc sg _))
= if is_sym_dec dc
then
DC (Data (dc:dcL) tmLL []) sg
else
DC_Err "Malformed datatype (polydata)"
polydata _ = DC_Err "Malformed datatype (polydata 2)"
{- Declaration pair formation -}
decpair (DC dc1 (Extend dc2 sg _))
= DC (Decpair dc2 dc1 []) sg
decpair _ = DC_Err "Malformed declaation pair"
{- Get the attributes of a declaration -}
get_Dec_att (DC dc _)
= get_dec_att dc
{- Set the attributes of a declaration -}
set_Dec_att (DC dc sg) att
= DC (set_dec_att dc att) sg
{- Return the internal representation of a declaration -}
internal_Dec (DC dc sg) = (dc,sg)
{- Restore a declaration from the database -}
restore_Dec s = error "BadDeclaration" -- ** exn NOT IMPLEMENTED YET
{- Axiom formation -}
axiom (SG sg) i j
= if share_map !! i == i
then
TH (typ_of_axm sg i j) sg
else
TH_Err "Malformed Axiom"
where
share_map = get_share_map sg
{- Forall introduction -}
generalise (TH tm (Extend dc sg _))
= if is_sym_dec dc
then
TH (Binder Forall dc tm [] []) sg
else
TH_Err "Malformed generalisation"
generalise _ = TH_Err "Malformed generalisation (2)"
{- Forall elimination -}
specialise (TH (Binder Forall dc tm1 _ _) sg1) (TM tm2 tm3 sg2)
= if eq_sgn sg1 sg2 && eq_trm (typ_of_dec dc) tm3
then
TH (subst_trm dc tm1 tm2) sg1
else
TH_Err "Malformed specialisation"
specialise _ _
= TH_Err "Malformed specialisation (2)"
{- Exists introduction -}
exists_intro (TH tm1 sg1)
(TM tm5@(Binder Exists dc tm2 _ _) _ sg2)
(TM tm3 tm4 sg3)
= if eq_sgn sg1 sg2 && eq_sgn sg2 sg3 &&
eq_trm (typ_of_dec dc) tm4 && eq_trm (subst_trm dc tm2 tm3) tm1
then
TH tm5 sg2
else
TH_Err "Malformed existential introduction"
exists_intro _ _ _ = TH_Err "Malformed existential introduction (2)"
{- Exists elimination -}
exists_elim (TH (Binder Forall dc1 (Binder Imp dc tm2 _ _) _ _) sg1)
(TH (Binder Exists dc2 tm3 _ _) sg2)
= if eq_sgn sg1 sg2 && eq_dec dc1 dc2 &&
eq_trm ( typ_of_dec dc ) tm3 && not (occurs 0 tm2)
then
TH tm2 sg1
else
TH_Err "Invalid existential elimination"
exists_elim _ _ = TH_Err "Invalid existential elimination"
{- => introduction -}
discharge (TH tm (Extend dc sg _))
= if is_axm_dec dc
then
TH (Binder Imp dc tm [] [] ) sg
else
TH_Err "Invalid implication introduction"
discharge _ = TH_Err "Invalid implication introduction (2)"
{- => elimination -}
modus_ponens (TH (Binder Imp dc tm2 _ _) sg1) (TH tm3 sg2)
= if eq_sgn sg1 sg2 && eq_trm ( typ_of_dec dc ) tm3
then
TH tm2 sg1
else
TH_Err "Invalid implication elimination"
modus_ponens _ _ = TH_Err "Invalid implication elimination"
{- Propositional tautologies -}
taut (TM tm (Constant Bool' _ _) sg)
= if eval tm
then
TH tm sg
else
TH_Err "term is not a tautology"
taut _ = TH_Err "argument must be a term of sort `bool'"
{- Reflexivity of equality -}
reflex (TM tm _ sg)
= TH (Binary' Eq' tm tm [] []) sg
{- Symmetry of equality -}
symmetry (TH (Binary' Eq' tm1 tm2 _ _) sg)
= TH (Binary' Eq' tm2 tm1 [] []) sg
symmetry _ = TH_Err "symmetry: argument must be an equality term"
{- Beta reduce a subterm of a theorem -}
beta_rw (TH tm sg) i
= case select_trm tm i of
(App (Binder Lambda dc tm1 _ _) tm2 _ _ ,_)
-> TH (replace_trm tm (subst_trm dc tm1 tm2) i) sg
_ -> TH_Err "Invalid beta reduction"
{- Eta reduce a subterm of a theorem -}
eta_rw (TH tm sg) i
= case select_trm tm i of
(Binder Lambda dc (App tm1 tm2 _ _) _ _ ,_)
-> if not (occurs 0 tm1) && eta_match dc tm2 1
then
TH (replace_trm tm (shift_trm [] (-1) tm1) i) sg
else
TH_Err "Invalid eta reduction"
_ -> TH_Err "Invlaid eta reduction (2)"
{- Rewrite conditional (condition is true) -}
cond_true_rw (TH tm1 sg1) (TH tm2 sg2) i
= case select_trm tm2 i of
(Cond dc tm3 tm4 _ _ ,dcL)
-> if eq_sgn sg1 sg3 && eq_trm tm1 (typ_of_dec dc)
then
TH (replace_trm tm2 (shift_trm [] (-1) tm3) i) sg1
else
TH_Err "cond_true_rw: error"
where
sg3 = foldr (\ dc -> \ sg -> Extend dc sg []) sg2 dcL
_ -> TH_Err "cond_true_rw: error 2"
{- Rewrite conditional (condition is false) -}
cond_false_rw (TH tm1 sg1) (TH tm2 sg2) i
= case select_trm tm2 i of
(Cond dc tm3 tm4 _ _ ,dcL)
-> if eq_sgn sg1 sg3 &&
eq_trm tm1 (Unary Not (typ_of_dec dc) [] [])
then
TH (replace_trm tm2 (shift_trm [] (-1) tm4) i) sg1
else
TH_Err "cond_false_rw: error"
where
sg3 = foldr (\ dc -> \ sg -> Extend dc sg []) sg2 dcL
_ -> TH_Err "cond_false_rw: error 2"
{- Substutution of equal terms -}
subterm_rw (TH tm1 sg1) (TH (Binary' Eq' tm2 tm3 _ _) sg2) i
= if eq_sgn sg3 sg3 && eq_trm tm2 tm4
then
TH (replace_trm tm1 tm3 i) sg1
else
TH_Err "subterm_rw: terms or sigs unequal"
where
(tm4,dcL) = select_trm tm1 i
sg3 = foldr (\ dc -> \ sg -> Extend dc sg []) sg1 dcL
subterm_rw _ _ _ = TH_Err "subterm_rw: Invalid argument"
{- Injectivity of datatypes -}
injection (TH (Binary' Eq' tm1 tm2 _ _) sg)
= case (reduce_app tm1 [], reduce_app tm2 []) of
(c1@(Const i j k _ _):tmL1 , c2@(Const _ _ _ _ _):tmL2)
-> case extract_dc j (nth_dec i sg) of
Data dcL _ _
-> if length dcL < length tmL1 &&
eq_trm c1 c2 &&
length tmL1 == length tmL2
then
TH (foldr1 mk_and
(map mk_eq (zip tmL11 tmL21))) sg
else
TH_Err "Invalid injection"
where
tmL11 = drop (length dcL) tmL1
tmL21 = drop (length dcL) tmL2
_ -> TH_Err "Invalid injection: not a datatype"
_ -> TH_Err "Invalid injection (3)"
where
reduce_app (App tm1 tm2 _ _) tmL
= reduce_app tm1 (tm2:tmL)
reduce_app tm tmL = tm:tmL
mk_eq (tm1,tm2) = Binary' Eq' tm1 tm2 [] []
mk_and tm1 tm2 = Binary' And tm1 tm2 [] []
injection _ = TH_Err "Invalid injection (4)"
{- Induction over datatypes -}
induction (TM tm@(Const i j 0 _ _) _ sg)
= TH ind_axm sg
where
ind_axm = induction_trm sg tm
induction _ = TH_Err "Invalid induction"
{- Issubtype introduction -}
issubstype_intro (TH (Binder Forall dc1 tm1 _ _) sg)
= case tm1 of
Binder Exists dc2 (Binary' Eq' tm2 tm3 _ _) _ _
-> case (tm2,tm3) of
(Sym 1 0 _ _ , Sym 0 0 _ _)
-> TH (Binary' Issubtype tm4 tm5 [] []) sg
where
tm4 = typ_of_dec dc1
tm5 = shift_trm [] (-1) (typ_of_dec dc2)
_ -> TH_Err "issubtype_intro error (1)"
_ -> TH_Err "issubtype_intro error (2)"
issubstype_intro _ = TH_Err "issubtype_intro error (3)"
{- Issubtype elimination -}
issubstype_elim (TH (Binary' Issubtype tm1 tm2 _ _) sg)
= TH (Binder Forall dc1 tm5 [] []) sg
where
dc1 = Symbol_dec tm1 []
dc2 = Symbol_dec (shift_trm [] 1 tm2) []
tm3 = Sym 1 0 [] []
tm4 = Sym 0 0 [] []
tm5 = Binder Exists dc2 (Binary' Eq' tm3 tm4 [] []) [] []
issubstype_elim _ = TH_Err "issubtype_elim error"
{- Equality of types -}
eq_of_ty (TH (Binary' Issubtype tm1 tm2 [] []) sg1)
(TH (Binary' Issubtype tm3 tm4 [] []) sg2)
= if eq_sgn sg1 sg2 && eq_trm tm1 tm4 && eq_trm tm2 tm3
then
TH (Binary' Eq' tm1 tm2 [] []) sg1
else
TH_Err "eq_of_ty error"
eq_of_ty _ _ = TH_Err "eq_of_ty error (2)"
{- project the theorem out of a terms subtype -}
from (TM tm1 (Binder Subtype dc tm2 _ _) sg)
= TH (subst_trm dc tm2 tm1) sg
from _ = TH_Err "from: argument must be term of subtype sort"
{- definition elimination -}
def_elim_thm (TH tm (Extend dc sg _))
= if is_def_dec dc
then
TH (subst_trm dc1 tm tm1) sg
else
TH_Err "Definition elimination error"
where
(dc1,tm1,_) = split_def dc
def_elim_thm _ = TH_Err "Definition elimination error (2)"
{- weaken a theorem -}
weaken (SG sg1) (TH tm sg2)
= case is_sub_sgn sg2 sg1 of
SOME i
-> TH (shift_trm share_map i tm) sg1
where
share_map = get_share_map sg1
NONE -> TH_Err "Weaken error"
set_Thm_att (TH tm sg) iL att
= TH (set_trm_att tm iL att) sg
get_Thm_att (TH tm sg) iL
= get_trm_att tm iL
{- Restore a theorem from the database -}
restore_Thm s = error "BadTheorem" -- ** exn
{- return the internal representation of a theorem -}
internal_Thm (TH tm sg) = (tm,sg)
internal_Thm (TH_Err mesg ) = error "add feed to itm via extra itrm ctr"
{-
database_magic_trm_str = "VTSTRM\^H\^H\^H\^H\^H\^H\^X\^Y"
database_magic_sgn_str = "VTSSGN\^H\^H\^H\^H\^H\^H\^X\^Y"
database_magic_dec_str = "VTSDEC\^H\^H\^H\^H\^H\^H\^X\^Y"
database_magic_thm_str = "VTSTHM\^H\^H\^H\^H\^H\^H\^X\^Y"
magic_str_len = length database_magic_trm_str
dbase_str = "vts90/lib/dbase/"
trm_str = "Term"
sgn_str = "Signature"
dec_str = "Declaration"
thm_str = "Theorem"
write_obj magic_str type_str obj file
= if test_file full_file_name "f"
then
False
else
let val ostr = open_out full_file_name
in output (ostr, magic_str);
output (ostr, obj);
close_out ostr;
true
end
end
let val home = get_env_var "HOME"
val full_file_name = home ^ "/" ^ dbase_str ^ type_str ^ "/" ^ file
fun read_obj exn magic_str type_str file =
let val home = get_env_var "HOME"
val vtshome = get_env_var "VTS_LIB_DIR"
val first_choice = home ^ "/" ^ dbase_str ^ type_str ^ "/" ^ file
val second_choice = vtshome ^ "/" ^ dbase_str ^ type_str ^ "/" ^ file
val file_name =
if test_file first_choice "fr" then
first_choice
else if test_file second_choice "fr" then
second_choice
else
raise exn
val istr = open_in file_name
val obj_magic_str = input (istr, magic_str_len)
val obj_str = input_to_eof istr
in close_in istr;
if magic_str = obj_magic_str then
obj_str
else
raise exn
end
and input_to_eof istr =
if end_of_stream istr then
""
else
let val str1 = input (istr,1024)
val str2 = input_to_eof istr
in (str1 ^ str2) end
val anon_sgn_name_header = "%"
fun read file =
let val instr = open_in file
val str = input_to_eof instr
in close_in instr;
str
end
handle Io _ => ""
fun write file str =
let val outstr = open_out file
in output (outstr, str);
close_out outstr
end
fun already_there str dir ("." :: files) = (* skip over . and .. *)
already_there str dir files
| already_there str dir (".." :: files) =
already_there str dir files
| already_there str dir (file :: files) =
if read (dir ^ file) = str then
SOME file
else
already_there str dir files
| already_there str dir [] =
NONE
fun save_sgn name sgn_rep =
let val home = get_env_var "HOME"
val sgn_dir = home ^ "/" ^ dbase_str ^ sgn_str ^ "/"
val sgs = System.Directory.listDir sgn_dir
in case already_there sgn_rep sgn_dir sgs
of SOME nm => nm
| NONE => (write (sgn_dir ^ anon_sgn_name_header ^ name) sgn_rep;
anon_sgn_name_header ^ name)
end
val a_chr = fromEnum "a"
and z_chr = fromEnum "z"
and A_chr = fromEnum "A"
and Z_chr = fromEnum "Z"
and zero_chr = fromEnum "0"
and nine_chr = fromEnum "9"
and minus_chr = fromEnum "-"
and underline_chr = fromEnum "_"
and dot_cht = fromEnum "."
(* database names must be either: *)
(* lower-case alphas a-z *)
(* upper-case alphas A-Z *)
(* numbers 0-9 *)
(* or _ - . *)
fun ok_name name =
let fun ok_ch ch =
(a_chr <= ch andalso ch <= z_chr) orelse
(A_chr <= ch andalso ch <= Z_chr) orelse
(zero_chr <= ch andalso ch <= nine_chr) orelse
(ch = minus_chr) orelse
(ch = underline_chr) orelse
(ch = dot_cht)
in forall ok_ch (map fromEnum (explode name)) end
in (* local *)
(* STILL TO BE DONE *)
(* SORT OUT SIGNATURE SHARING *)
fun save_Trm name (TM (tm1,tm2,sg)) =
if ok_name name then
let val tm1_str = trm_to_str tm1
val tm2_str = trm_to_str tm2
val sg_str = database_magic_sgn_str ^ sgn_to_str sg
val sg_nm = save_sgn name sg_str
in write_obj database_magic_trm_str trm_str (tm1_str ^ tm2_str ^ sg_nm) name end
else
false
fun save_Sgn name (SG sg) =
if ok_name name then
let val sg_str = database_magic_sgn_str ^ sgn_to_str sg
val sg_nm = save_sgn name sg_str
in write_obj database_magic_sgn_str sgn_str sg_nm name end
else
false
fun save_Dec name (DC (dc,sg)) =
if ok_name name then
let val dc_str = dec_to_str dc
val sg_str = database_magic_sgn_str ^ sgn_to_str sg
val sg_nm = save_sgn name sg_str
in write_obj database_magic_dec_str dec_str (dc_str ^ sg_nm) name end
else
false
fun save_Thm name (TH (tm,sg)) =
if ok_name name then
let val tm_str = trm_to_str tm
val sg_str = database_magic_sgn_str ^ sgn_to_str sg
val sg_nm = save_sgn name sg_str
in write_obj database_magic_thm_str thm_str (tm_str ^ sg_nm) name end
else
false
fun restore_Trm file =
let val obj_str = read_obj BadTerm database_magic_trm_str trm_str file
val (tm1, is1) = str_to_trm (mkistring obj_str)
val (tm2, is2) = str_to_trm is1
val sg_nm = rest_istring is2
val sgn_rep = read_obj BadSignature database_magic_sgn_str sgn_str sg_nm
val (sg, is3) = str_to_sgn (mkistring sgn_rep)
in (TM (tm1,tm2,sg)) end
fun restore_Sgn file =
if ok_name file then
let val sg_nm = read_obj BadSignature database_magic_sgn_str sgn_str file
val obj_str = read_obj BadSignature database_magic_sgn_str sgn_str sg_nm
val (sg, is3) = str_to_sgn (mkistring obj_str)
in (SG sg) end
else
raise BadSignature
fun restore_Dec file =
let val obj_str = read_obj BadDeclaration database_magic_dec_str dec_str file
val (dc, is1) = str_to_dec (mkistring obj_str)
val sg_nm = rest_istring is1
val sgn_rep = read_obj BadSignature database_magic_sgn_str sgn_str sg_nm
val (sg, is2) = str_to_sgn (mkistring sgn_rep)
in (DC (dc,sg)) end
fun restore_Thm file =
let val obj_str = read_obj BadTheorem database_magic_thm_str thm_str file
val (tm, is1) = str_to_trm (mkistring obj_str)
val sg_nm = rest_istring is1
val sgn_rep = read_obj BadSignature database_magic_sgn_str sgn_str sg_nm
val (sg, is2) = str_to_sgn (mkistring sgn_rep)
in (TH (tm,sg)) end
end (* local *)
-}
eq_Trm (TM tm1 _ sg1 ) (TM tm2 _ sg2 )
= eq_trm tm1 tm2 && eq_sgn sg1 sg2
eq_Sgn (SG sg1) (SG sg2)
= eq_sgn sg1 sg2
eq_Dec (DC dc1 sg1 ) (DC dc2 sg2 )
= eq_dec dc1 dc2 && eq_sgn sg1 sg2
eq_Thm (TH tm1 sg1) (TH tm2 sg2)
= eq_trm tm1 tm2 && eq_sgn sg1 sg2
typ_of_Trm (TM _ tm sg)
= TM tm ( typ_of_trm sg tm ) sg
typ_of_Dec ( DC dc sg )
= TM tm1 tm2 sg
where
tm1 = typ_of_dec dc
tm2 = typ_of_trm sg tm1
typ_of_Thm ( TH tm sg )
= TM tm ( Constant Bool' [] [] ) sg
shift_Trm i (SG sg1) (TM tm1 tm2 sg2)
= if eq_sgn sg2 sg3
then TM (shift_trm sm i tm1) (shift_trm sm i tm2) sg1
else TM_Err "shift_Trm: signatures unequal"
where
sg3 = nth_sgn i sg1
sm = get_share_map sg2
subst_Trm (TM tm1 tm2 (Extend dc sg1 _)) (TM tm3 tm4 sg2)
= if eq_sgn sg1 sg2 && eq_trm (typ_of_dec dc) tm4
then TM (subst_trm dc tm1 tm2) (subst_trm dc tm2 tm3) sg1
else TM_Err "subst_Trm: signatures unequal or type of dc unequal to type of second argument"
subst_Trm _ _ = TM_Err "subst_Trm: Invalid arguments"
sgn_of_Trm (TM _ _ sg) = SG sg
sgn_of_Trm (TM_Err mesg ) = SG_Err mesg
sgn_of_Dec (DC _ sg) = SG sg
sgn_of_Dec (DC_Err mesg ) = SG_Err mesg
sgn_of_Thm (TH _ sg) = SG sg
sgn_of_Thm (TH_Err mesg ) = SG_Err mesg
is_valid_Thm ( TH _ _ ) = True
is_valid_Thm _ = False
is_valid_Trm ( TM _ _ _ ) = True
is_valid_Trm _ = False
is_valid_Sgn ( SG _ ) = True
is_valid_Sgn _ = False
|
