#!/bin/bash

cloc --by-file ./theories --include-ext=v --json | jq -r '
	def categories: {
		"./theories/lambda/operational.v": {
			component: "(2) LambdaLang",
			category1: "(1) Operational semantics",
			category2: "General",
		},
		"./theories/lambda/operational_props.v": {
			component: "(2) LambdaLang",
			category1: "(1) Operational semantics",
			category2: "Properties",
		},
		"./theories/lambda/interp.v": {
			component: "(2) LambdaLang",
			category1: "(2) Interpreter",
			category2: "General",
		},
		"./theories/lambda/interp_proofs.v": {
			component: "(2) LambdaLang",
			category1: "(2) Interpreter",
			category2: "Theorem + proofs",
		},
		"./theories/dynlang/operational.v": {
			component: "(3) DynLang",
			category1: "(1) Operational semantics",
			category2: "General",
		},
		"./theories/dynlang/operational_props.v": {
			component: "(3) DynLang",
			category1: "(1) Operational semantics",
			category2: "Properties",
		},
		"./theories/dynlang/interp.v": {
			component: "(3) DynLang",
			category1: "(2) Interpreter",
			category2: "General",
		},
		"./theories/dynlang/interp_proofs.v": {
			component: "(3) DynLang",
			category1: "(2) Interpreter",
			category2: "Theorem + proofs",
		},
		"./theories/dynlang/equiv.v": {
			component: "(3) DynLang",
			category1: "(4) Extra",
			category2: "Equivalence with LambdaLang",
		},
		"./theories/evallang/operational.v": {
			component: "(4) EvalLang",
			category1: "(1) Operational semantics",
			category2: "General",
		},
		"./theories/evallang/operational_props.v": {
			component: "(4) EvalLang",
			category1: "(1) Operational semantics",
			category2: "Properties",
		},
		"./theories/evallang/interp.v": {
			component: "(4) EvalLang",
			category1: "(2) Interpreter",
			category2: "General",
		},
		"./theories/evallang/interp_proofs.v": {
			component: "(4) EvalLang",
			category1: "(2) Interpreter",
			category2: "Theorem + proofs",
		},
		"./theories/evallang/tests.v": {
			component: "(4) EvalLang",
			category1: "(3) Tests",
			category2: "General",
		},
		"./theories/nix/floats.v": {
			component: "(5) NixLang",
			category1: "(4) Extra",
			category2: "General",
		},
		"./theories/nix/operational.v": {
			component: "(5) NixLang",
			category1: "(1) Operational semantics",
			category2: "General",
		},
		"./theories/nix/operational_props.v": {
			component: "(5) NixLang",
			category1: "(1) Operational semantics",
			category2: "Properties",
		},
		"./theories/nix/notations.v": {
			component: "(5) NixLang",
			category1: "(4) Extra",
			category2: "General",
		},
		"./theories/nix/interp.v": {
			component: "(5) NixLang",
			category1: "(2) Interpreter",
			category2: "General",
		},
		"./theories/nix/interp_proofs.v": {
			component: "(5) NixLang",
			category1: "(2) Interpreter",
			category2: "Theorem + proofs",
		},
		"./theories/nix/tests.v": {
			component: "(5) NixLang",
			category1: "(3) Tests",
			category2: "General",
		},
		"./theories/nix/wp.v": {
			component: "(5) NixLang",
			category1: "(4) Extra",
			category2: "General",
		},
		"./theories/nix/wp_examples.v": {
			component: "(5) NixLang",
			category1: "(4) Extra",
			category2: "General",
		},
		"./theories/utils.v": {
			component: "(1) Shared",
			category1: "General",
			category2: "General",
		},
		"./theories/res.v": {
			component: "(1) Shared",
			category1: "General",
			category2: "General",
		},
	};
	def add_cat_data:
		{ key, value: ({loc: .value.code} + categories[.key]) };
	def categorize_by(key):
		group_by(.value[key]) | map({ key: .[0].value[key], value: . }) | from_entries;
	def spaces: if . == 0 then "" else " " + (. - 1 | spaces) end;
	def pretty(ind):
		if (. | type) == "number" then
			. | tostring
		else
			to_entries | reduce .[] as $item (""; . + "\n" + (ind | spaces) + $item.key + ": " + ($item.value | pretty(ind + 2)))
		end;
	.SUM.code as $sum | del(.header, .SUM) | with_entries(add_cat_data) | to_entries
	| categorize_by("component") | map_values(categorize_by("category1"))
	| map_values(map_values(categorize_by("category2") | map_values(map(.value.loc) | add)))
	| map_values(map_values(. + { TOTAL: to_entries | map(.value) | add }))
	| map_values(. + { TOTAL: to_entries | map(.value.TOTAL) | add })
	| . + { TOTAL: to_entries | map(.value.TOTAL) | add }
	| if .TOTAL == $sum then . else error("internal error: calculated total \(.TOTAL) does not match provided sum \($sum)") end
	| "Lines of code for the different parts of the Rocq development:" + pretty(0)
'