Module Qcert.Utils.Closure

Require Import String.
Require Import List.

Section Closure.
  Context {C:Set}.
  Context {T:Set}.

  Context {free_vars : C -> list string}.

  Definition code_closed_for_params (params:list string) (c:C) : Prop :=
    forall v, In v (free_vars c) -> In v params.
  
  Record closure :=
    mkClosure
      { closure_params: list (string * option T);
        closure_output : option T;
        closure_body : C; }.

  Definition closure_is_closed (f:closure) : Prop :=
    code_closed_for_params (map fst f.(closure_params)) f.(closure_body).

  Definition closed_closure :=
    { c : closure | closure_is_closed c }.
  
End Closure.