#!/bin/sh

# Script to validate Cut certificates.
# This script should be invoked from cert.
# It expects "$PROGRAMATICA", "$SERVERDIR" and "$certsDir" to be set.

type=Cut

[ -n "$PROGRAMATICA" ] || { echo >&2 'Bug: $PROGRAMATICA is not set'; exit 1;}
. "$PROGRAMATICA/validation.sh" # Sets assertion, attr, conc, deps, module
[ -n "$SERVERDIR" ] || abort 'Bug: $SERVERDIR is not set'
. $SERVERDIR/functions.sh  # cut()


### Auxiliary functions ########################################################

checkcut() {
  conc2=`getattr conc $attr`
  hyp2=`getattr hyp $attr`
  cut "$1" "$2"
  err=0
  if [ -n "$conc2" ] ; then
    [ "$conc" = "$conc2" ] || { echo "Conclusion doesn't match, should be $conc"; err=1; }
  else
    setattr conc "$conc" "$attr"
  fi
  if [ -n "$hyp2" ] ; then
    [ "$hyp" = "$hyp2" ] || { echo "Hypothesis doesn't match, should be $hyp"; err=1; }
  else
    #echo "setting hyp to $hyp"
    setattr hyp "$hyp" "$attr"
  fi
  return $err
}

checkcerts() {
  err=0
  for cert in $* ; do
    (checkcert "$cert")
    valid="`cd $certsDir && quickvalidate $cert`"
    case "$valid" in
      Valid) ;;
      *) err=1
    esac
  done
  return $err
}

validate() {
  left=`getattr left $attr`
  right=`getattr right $attr`
  if checkcerts "$left $right" >"$output"; then
      if checkcut "$left" "$right" >>"$output"; then
        trivialmarkvalid
      else
	markinvalid
      fi
  else
      { echo "Bad/missing names for certificate to cut (should be <Module/certname>):"
        echo "left certificates: $left"
        echo "right certificate: $right"
      } | tee -a "$output"
      markinvalid
  fi
}

### Here we go... ##############################################################

validate