Module Qcert.NNRC.Lang.NNRCSanitizer

Require Import String.
Require Import List.
Require Import Ascii.
Require Import Utils.
Require Import cNNRCShadow.
Require Import NNRC.
Require Import NNRCShadow.
Require Import DataRuntime.

Local Open Scope string_scope.

Section NNRCSanitizer.
  Context {fruntime:foreign_runtime}.

  Definition unshadow_js {fruntime:foreign_runtime} (avoid:list var) (e:nnrc) : nnrc
    := unshadow jsSafeSeparator jsIdentifierSanitize (avoid++jsAvoidList) e.

  Definition jsSanitizeNNRC {fruntime:foreign_runtime} (e:nnrc) : nnrc
    := unshadow_js nil e.

End NNRCSanitizer.