Guillaume ALLAIS 1d4c84171d [ refactor ] suggested during SPLV ... Main change =========== The main change is to the type of function dealing with an untouched segment of the local scope. e.g. ``` weak : {outer, vars : _} -> (ns : List Name) -> tm (outer ++ inner) -> tm (outer ++ ns ++ inner) ``` Instead we now write ``` weak : SizeOf ns -> tm (outer ++ inner) -> tm (outer ++ ns ++ inner) ``` meaning that we do not need the values of `outer`, `inner` and `ns` at runtime. Instead we only demand a `SizeOf ns` which is a `Nat` together with an (erased) proof that `ns` is of that length. Other modifications =================== Quadratic behaviour ------------------- A side effect of this refactor is the removal of two sources of quadratic behaviour. They typically arise in a situation where work is done on a scope of the form ``` outer ++ done ++ ns ++ inner ``` When `ns` is non-empty, some work is performed and then the variable is moved to the pile of things we are `done` with. This leads to recursive calls of the form `f done` -> `f (done ++ [v])` leading to a cost quadratic in the size of `ns`. Now that we only care about `SizeOf done`, the recursive call is (once all the runtime irrelevant content is erased) for the form `f n` -> `f (S n)`! More runtime irrelevance ------------------------ In some places we used to rely on a list of names `vars` being available. However once we only care about the length of `vars`, the fact it is not available is not a limitation. For instance a `SizeOf vars` can be reconstructed from an environment assigning values to `vars` even if `vars` is irrelevant. Indeed the size of the environment is the same as that of `vars`.		2020-08-27 10:14:55 +01:00
..
base	[ refactor ] suggested during SPLV	2020-08-27 10:14:55 +01:00
contrib	implement HVect (#563)	2020-08-26 15:48:19 +01:00
network	Use the same naming convention for foreign primitives	2020-08-19 14:05:28 +01:00
prelude	Add supporting code	2020-08-25 14:30:57 +03:00