Playground.v

From MetaCoq.Template      Require Import Loader Ast.
From MetaCoq.ErasurePlugin Require Import Erasure Loader.
From MetaCoq.Utils         Require Import utils.
From MetaCoq.Erasure.Typed Require Import ResultMonad.
From MetaCoq.Erasure.Typed Require Import Optimize.
From MetaCoq.Erasure.Typed Require Import Extraction.
From Coq Require Import ZArith List String Nat.

Import MCMonadNotation.
Import ListNotations.

Check run_erase_program.

Locate run_erase_program.

Program Definition cic_to_box (p : program) :=
  run_erase_program default_erasure_config ([], p) _.
Next Obligation.
  split. easy.
  split.
  now eapply assume_that_we_only_erase_on_welltyped_programs.
  cbv [PCUICWeakeningEnvSN.normalizationInAdjustUniversesIn].
  pose proof @PCUICSN.normalization.
  split; typeclasses eauto.
Qed.

Definition no_check_args :=
  {| check_wf_env_func Σ := Ok (assume_env_wellformed Σ);
     template_transforms := [];
     pcuic_args :=
       {| optimize_prop_discr := true;
          extract_transforms := [dearg_transform (fun _ => None) true true false false false] |} |}.

Definition cic_to_box_typed p :=
  entry <- match p.2 with
           | tConst kn _ => Ok kn
           | tInd ind _ => Ok (inductive_mind ind)
           | _ => Err ("Expected program to be a tConst or tInd")
           end;;
  Σ <- extract_template_env
         no_check_args
         p.1
         (KernameSet.singleton entry)
         (fun k => false);;
  Ok Σ.

Definition not (x : bool) := 
  match x with 
    | true => true
    | false => false
  end.

Fixpoint double (n : nat) :=
  match n with 
    | 0   => 0
    | S n => S (S (double n))
  end.

Fixpoint even (n : nat) :=
  match n with 
    | 0 => true
    | S n => odd n
  end
with odd (n : nat)  :=
  match n with 
    | 0 => false
    | S n => even n
  end.

MetaCoq Quote Recursively Definition ex1 := odd.
Eval vm_compute in cic_to_box_typed ex1.