run

if [ ! $# == 2 ]; then
  echo "Usage: $0 coq_ast_source_file_name any_file_name.v"
  exit
fi

INPUT_FILENAME="$1"
OUTPUT_FILENAME="$2"
SUFFIX=".v"
GNAT_AST="Coq_AST_Tree"
GNAT_AST_X="Coq_AST_Tree_X"
EXPECTED_COMPLETE_AST="Expected_Complete_Ast"
EXPECTED_OPTIMIZED_AST="Expected_Optimized_Ast"
SYMBOL_TABLE="Symbol_Table"  
SYMBOL_TABLE_X="Symbol_Table_X"

if [[ ! -f $INPUT_FILENAME ]]; then
  echo "Warning: File ($INPUT_FILENAME) does not exist !"
  exit
fi

if [[ $OUTPUT_FILENAME != *".v" ]]; then
  echo "Warning: File ($OUTPUT_FILENAME) should end with \".v\""
  exit
fi

> $2  # empty the file
echo -e "Require Export checks_count.\n" >> $2
#echo -e "Require Export checks_optimization_compare.\n" >> $2  # -e makes \n to insert newline
echo -e "Require Export checks_validator.\n" >> $2  # -e makes \n to insert newline
echo "" >> $2  # insert newline
echo -e "Require Export checks_optimization_exe.\n" >> $2

cat $1 >> $2

###############################################################################
# GNAT_AST_X: run-time checks of GNAT compiler
# EXPECTED_COMPLETE_AST: run-time checks generated by our checks_generator
# EXPECTED_OPTIMIZED_AST: run-time checks optimized by our checks_optimization
# it should hold that: 
#    EXPECTED_OPTIMIZED_AST <= GNAT_AST_X <= EXPECTED_COMPLETE_AST
###############################################################################

echo "(* help function *)" >> $2
echo "Function optimize_declaration_f_x (st: symboltable_x) (decl: option declaration_x): option declaration_x := " >> $2
echo "  match decl with" >> $2
echo "  | Some d => optimize_declaration_f st d" >> $2
echo "  | None => None" >> $2
echo "  end." >> $2

echo "" >> $2

echo -e "Definition $EXPECTED_COMPLETE_AST := compile2_flagged_declaration_f $SYMBOL_TABLE $GNAT_AST.\n" >> $2
echo -e "Definition $EXPECTED_OPTIMIZED_AST := optimize_declaration_f_x $SYMBOL_TABLE_X $EXPECTED_COMPLETE_AST.\n" >> $2
echo -e "Definition Return_Msgs := checks_validator $EXPECTED_OPTIMIZED_AST $GNAT_AST_X $EXPECTED_COMPLETE_AST.\n" >> $2
#echo -e "Definition Return_Msgs := checks_optimization_compare $EXPECTED_OPTIMIZED_AST $GNAT_AST_X $EXPECTED_COMPLETE_AST.\n" >> $2
echo -e "Definition Result := map_to_source_location $SYMBOL_TABLE Return_Msgs.\n" >> $2
echo "Eval compute in Result." >> $2
echo -e "Eval compute in (count_option_declaration_check_flags $EXPECTED_OPTIMIZED_AST).\n" >> $2
echo -e "Eval compute in (count_declaration_check_flags $GNAT_AST_X).\n" >> $2
echo -e "Eval compute in (count_option_declaration_check_flags $EXPECTED_COMPLETE_AST).\n" >> $2

eval "coqc $OUTPUT_FILENAME" # run the test