scopes: objects and explicits

Scopes_objects_and_explicits.ml

(* we start by setting up a global scope.
   `setup` is a special function that handles all we need behind
   the scenes. `$global` is a macro that gets substituted with
   the scope ID from the meta-environment mapping (ID -> scope) *)
$global -> setup ()

(* `let` is an applicative statement that handles intro and
   substitution in the specified scope *)
let($global) n := 3

(* `function` is an applicative statement that handles what
   `let` does, but also sets up the necessary scope to access
   parameters *)
function($global) square (n : Nat) := n * n

(* Optionally, to specify which scope the identifier we are
   using is defined in, we can suffix it with `@scope` where
   `scope` is to be replaced with an actual scope ID. If you
   don't indicate it, the closest scope will be assumed. This
   means that if the identifier is not found in said scope, it
   will NOT try to look up in higher scopes, but throw a
   compilation error instead. *)

(* `function` introduces a `rec` identifier that allows the
   function to call itself recursively. *)
function($global) factorial (n : Nat) :=
  match n with
  | 0 -> 1
  | S n' -> n * rec@factorial n'
  end

(* function application is just substitution behind the scenes -
   `n` is not eliminated. *)
let($global) m := square n
let($global) p := factorial n

(* however, if we do want to eliminate `n`, here's how: *)
elim($global) n
(* this should be done with care especially if we did not
   explicitly `intro`ed `n` ourselves. *)

might craft a toy implementation in ocaml at some point