# This script recreates all the certificates (and is invoked from setup.sh).

WARNSLOW=no # Avoid repeated warnings...
export WARNSLOW

new() {
  cert new "$@" &&
  case "$1" in
    Alfa)
      cert setattr "$2" SimplePatterns True
      cert setattr "$2" proof "${2%%/*}Proofs.proof$3"
  esac
}

new Alfa Nat/NatEq NatEq 
new Alfa Nat/CongSucc CongSucc 
new Alfa Nat/EqNatRefl EqNatRefl 
new Alfa Nat/NotLtZero NotLtZero 
new Alfa Nat/AddSucc AddSucc 
new Alfa Nat/Peano4b Peano4b 
new Alfa Nat/Peano4 Peano4 
new Alfa Nat/AddZero AddZero
new Alfa Nat/LeNatRefl LeNatRefl
new Alfa Nat/LtNatSucc LtNatSucc
new Alfa Nat/LeNatSucc LeNatSucc
new Alfa Nat/LtNatPlus LtNatPlus

new Alfa FunFM/LookupUpdate LookupUpdateFM
new Alfa FunFM/UpdateOther UpdateOtherFM
new Alfa FunFM/UpdateSame UpdateSameFM 

new Alfa Memories/StoreEqRange StoreEqRange 
new Alfa Memories/LookupUpdateM LookupUpdateM 
new Alfa Memories/UpdateOtherM UpdateOtherM 
new Alfa Memories/StoreList StoreList 
new Alfa Memories/UpdateSameM UpdateSameM 
new Alfa Memories/LookupInRange LookupInRange 
new Alfa Memories/LoadEqRange LoadEqRange 

new Alfa MemoryState/ReturnS_MSI ReturnS_MSI
new Alfa MemoryState/BindS_MSI BindS_MSI

new Alfa ChipModel/CondSeparation CondSeparation &&
 cert setattr ChipModel/CondSeparation file/proof SeparationProof.alfa &&
 cert setattr ChipModel/CondSeparation proof SeparationProof.proofCondSeparation
new Alfa ChipModel/Separation Separation 
new Alfa ChipModel/AllGoodAlg AllGoodAlg
new Alfa ChipModel/SameState SameState 

#new I_say_so ChipModel/ISayCondSeparation CondSeparation 
#new I_say_so ChipModel/ISaySeparation Separation 
new TestCase Examples/testcase1 testcase1