#!/bin/bash

function get_deps () {
    grep "^Require" $1.v \
    | sed 's/Require Import \(.*\)\..*$/\1/' \
    | sed 's/Require Export \(.*\)\..*$/\1/' \
    | sed 's/Require \(.*\)\..*$/\1/'
}

containsElement () {
    local e
    for e in "${@:2}"; do
	[[ "$e" == "$1" ]] && return 0;
    done
    return 1
}

declare -A aa
declare -a remfiles
declare -a allfiles
#declare -a temp

remfiles=("all")
allfiles=("all")

echo "`date`" > debug

while true
do
    #printf '%s\n' "==+== ${remfiles[@]} ==+=="
    if [[ ${#remfiles[@]} -eq 0 ]]
    then
	echo "++++++ no more files" >> debug
	break
    else
	file=${remfiles[0]}
	remfiles=("${remfiles[@]:1}")
	#printf '%s\n' "++=++ ${remfiles[@]} ++=++"
	echo "===============================" >> debug
	echo "++++++ file: ${file}" >> debug

	temp=`get_deps $file`
	deps=()
	for f in $temp
	do
	    if [ -e "${f}.v" ]
	    then deps+=("$f")
	    else
		if [ -e "model/${f}.v" ]
		then deps+=("model/$f")
		else
		    if [ -e "PBFT/${f}.v" ]
		    then deps+=("PBFT/$f")
		    else
			if [ -e "MinBFT/${f}.v" ]
			then deps+=("MinBFT/$f")
			else
			    if [ -e "SM/${f}.v" ]
			    then deps+=("SM/$f")
			    else
			        if [ -e "SM2/${f}.v" ]
			        then deps+=("SM2/$f")
			        else
				    if [ -e "PrimaryBackup/${f}.v" ]
				    then deps+=("PrimaryBackup/$f")
				    else
					if [ -e "runtime/${f}.v" ]
					then deps+=("runtime/$f")
					else
					    if [ -e "coq-tools/${f}.v" ]
					    then deps+=("coq-tools/$f")
					    else echo "${f} doesn't exist" >> debug
					    fi
					fi
				    fi
				fi
			    fi
			fi
		    fi
		fi
	    fi	    
	done
	#printf '%s\n' "++=++ ${deps[@]} ++=++"
	#deps=("${temp[@]}")

	aa[$file]=${deps[@]}
   
	for i in "${deps[@]}"
	do
	    #echo "checking $i"
	    containsElement "$i" "${allfiles[@]}"
	    n=$?
	    if [[ $n -eq 1 ]]
	    then
		echo "++ new dependency: ${i}" >> debug
		remfiles=("${remfiles[@]}" "$i")
		allfiles=("${allfiles[@]}" "$i")
	    else echo "++ not new dependency: ${i}" >> debug
	    fi
	done
    fi
done

echo "# Makefile generated by create_makefile.sh" > Makefile
echo "" >> Makefile
echo "default : all.vo" >> Makefile

echo "" >> Makefile
echo "clean :" >> Makefile

echo "	rm -f model/.*.aux         model/*.glob         model/*.vo"         >> Makefile
echo "	rm -f PBFT/.*.aux          PBFT/*.glob          PBFT/*.vo"          >> Makefile
echo "	rm -f MinBFT/.*.aux        MinBFT/*.glob        MinBFT/*.vo"        >> Makefile
echo "	rm -f SM/.*.aux            SM/*.glob            SM/*.vo"            >> Makefile
echo "	rm -f SM2/.*.aux           SM2/*.glob           SM2/*.vo"           >> Makefile
echo "	rm -f PrimaryBackup/.*.aux PrimaryBackup/*.glob PrimaryBackup/*.vo" >> Makefile
echo "	rm -f runtime/.*.aux       runtime/*.glob       runtime/*.vo"       >> Makefile
echo "	rm -f coq-tools/.*.aux     coq-tools/*.glob     coq-tools/*.vo"     >> Makefile

for i in "${!aa[@]}"
do
    #echo "-------------------"
    #echo "++ ${i}"

    echo "" >> Makefile
    echo -n "${i}.vo : ${i}.v" >> Makefile

    if [[ ${#aa[$i]} -eq 0 ]]
    then
	echo "${i} doesn't have dependencies"
    else
	#echo "${aa[$i]}"
	IFS=' ' read -a vals <<< "${aa[$i]}"
	for f in "${vals[@]}"
	do
	    #echo "---- ${f}"
	    echo -n " ${f}.vo" >> Makefile
	done
    fi

    echo "" >> Makefile
    echo "	coqc -R coq-tools util -R model model -R PBFT PBFT -R MinBFT MinBFT -R SM SM -R SM2 SM2 -R PrimaryBackup PrimaryBackup -R runtime runtime ${i}.v" >> Makefile
done
