#!/bin/sh

# This script should be invoked from cert
# It expects "$PROGRAMATICA", "$SERVERDIR" and "$certsDir" to be set

[ -n "$PROGRAMATICA" ] || { echo >&2 'Bug: $PROGRAMATICA is not set'; exit 1;}
. "$PROGRAMATICA/functions.sh"
[ -n "$certsDir" ] || abort 'Bug: $certsDir is not set'

type=QuickCheck

usage() { abort "Usage: cert new $type <module/cert> <conc>"; } # [<hyp>]

createcert() {
  mkdir -p "$1"
  cat >"$1/cert.attr" <<EOF
type: $type
version: `getserverattr version`
conc: $2
hyp: $3
who: $USER
date: `LANG=C date`
EOF
}

[ -n "$1" ] || usage
cert="$1"

[ -n "$2" ] || usage
conc="$2"
shift;shift;
[ -n "$*" ] && usage # Hypotheses are not supported (yet).
#hyp="$*"
hyp=".."

checkproject

module="${cert%/*}"
certname="${cert##*/}"
#checkcertannot "$module" "$certname"
certpath="$module/$certname"
[ -d "$certsDir$certpath" ] && abort "$cert already exists"
pfe assertions "$module" | grep -qw "$conc" ||
  abort "Error: $conc is not a named assertion in module $module"

createcert "$certsDir$certpath" "$conc" "$hyp"