Extraction of NbE

[HuStmpHrrr]

Closes #65

[HuStmpHrrr]

Current extraction looks like this:

(** val eval_exp_impl : exp -> (nat -> domain) -> domain **)

let rec eval_exp_impl m p =
  match m with
  | A_zero -> D_zero
  | A_succ e -> D_succ (eval_exp_impl e p)
  | A_natrec (e, e0, e1, e2) -> eval_natrec_impl e e0 e1 (eval_exp_impl e2 p) p
  | A_nat -> D_nat
  | A_typ n -> D_univ n
  | A_var n -> p n
  | A_fn (_, e) -> D_fn (p, e)
  | A_app (e, e0) -> eval_app_impl (eval_exp_impl e p) (eval_exp_impl e0 p)
  | A_pi (e, e0) -> D_pi ((eval_exp_impl e p), p, e0)
  | A_sub (e, s) -> eval_exp_impl e (eval_sub_impl s p)

(** val eval_natrec_impl : exp -> exp -> exp -> domain -> (nat -> domain) -> domain **)

and eval_natrec_impl a mZ mS m p =
  match m with
  | D_zero -> eval_exp_impl mZ p
  | D_succ d -> eval_exp_impl mS (extend_env (extend_env p d) (eval_natrec_impl a mZ mS d p))
  | D_neut (d, d0) ->
    (match d with
     | D_nat ->
       D_neut ((eval_exp_impl a (extend_env p (D_neut (D_nat, d0)))), (D_natrec (p, a, (eval_exp_impl mZ p), mS, d0)))
     | _ -> assert false (* absurd case *))
  | _ -> assert false (* absurd case *)

(** val eval_app_impl : domain -> domain -> domain **)

and eval_app_impl m n =
  match m with
  | D_fn (d, e) -> eval_exp_impl e (extend_env d n)
  | D_neut (d, d0) ->
    (match d with
     | D_pi (d1, d2, e) -> D_neut ((eval_exp_impl e (extend_env d2 n)), (D_app (d0, (D_dom (d1, n)))))
     | _ -> assert false (* absurd case *))
  | _ -> assert false (* absurd case *)

(** val eval_sub_impl : sub -> (nat -> domain) -> (nat -> domain) **)

and eval_sub_impl _UU03c3_ p =
  match _UU03c3_ with
  | A_id -> p
  | A_weaken -> drop_env p
  | A_compose (s, s0) -> eval_sub_impl s (eval_sub_impl s0 p)
  | A_extend (s, e) -> extend_env (eval_sub_impl s p) (eval_exp_impl e p)

[Ailrun]

That sigma unicode... it's sad that it emits that kind of "weird looking" variable name

[HuStmpHrrr]

That sigma unicode... it's sad that it emits that kind of "weird looking" variable name

That sigma unicode... it's sad that it emits that kind of "weird looking" variable name

this is easy to fix. just change the name in Equations to s.

[HuStmpHrrr]

readback functions:

(** val read_nf_impl : nat -> domain_nf -> nf **)

let rec read_nf_impl s = function
| D_dom (d0, d1) ->
  (match d0 with
   | D_nat ->
     (match d1 with
      | D_zero -> Nf_zero
      | D_succ d2 -> Nf_succ (read_nf_impl s (D_dom (D_nat, d2)))
      | D_neut (d2, d3) ->
        (match d2 with
         | D_nat -> Nf_neut (read_ne_impl s d3)
         | _ -> assert false (* absurd case *))
      | _ -> assert false (* absurd case *))
   | D_pi (d2, d3, e) ->
     Nf_fn ((read_typ_impl s d2),
       (read_nf_impl (S s) (D_dom
         ((eval_exp_impl e (extend_env d3 (D_neut (d2, (D_var s))))),
         (eval_app_impl d1 (D_neut (d2, (D_var s))))))))
   | D_univ _ -> read_typ_impl s d1
   | D_neut (_, _) ->
     (match d1 with
      | D_neut (_, d2) -> Nf_neut (read_ne_impl s d2)
      | _ -> assert false (* absurd case *))
   | _ -> assert false (* absurd case *))

(** val read_ne_impl : nat -> domain_ne -> ne **)

and read_ne_impl s = function
| D_var x -> Ne_var (sub (sub s x) (S O))
| D_app (d0, d1) ->
  Ne_app ((read_ne_impl s d0), (read_nf_impl s d1))
| D_natrec (d0, e, d1, e0, d2) ->
  let b =
    eval_exp_impl e (extend_env d0 (D_neut (D_nat, (D_var s))))
  in
  Ne_natrec ((read_typ_impl (S s) b),
  (read_nf_impl s (D_dom ((eval_exp_impl e (extend_env d0 D_zero)),
    d1))),
  (read_nf_impl (S (S s)) (D_dom
    ((eval_exp_impl e
       (extend_env d0 (D_succ (D_neut (D_nat, (D_var s)))))),
    (eval_exp_impl e0
      (extend_env (extend_env d0 (D_neut (D_nat, (D_var s))))
        (D_neut (b, (D_var (S s))))))))), (read_ne_impl s d2))

(** val read_typ_impl : nat -> domain -> nf **)

and read_typ_impl s = function
| D_nat -> Nf_nat
| D_pi (d0, d1, e) ->
  Nf_pi ((read_typ_impl s d0),
    (read_typ_impl (S s)
      (eval_exp_impl e (extend_env d1 (D_neut (d0, (D_var s)))))))
| D_univ n -> Nf_typ n
| D_neut (_, d0) -> Nf_neut (read_ne_impl s d0)
| _ -> assert false (* absurd case *)

[HuStmpHrrr]

We will need to remember to put

Require Import ExtrOcamlBasic ExtrOcamlIntConv ExtrOcamlZInt.

when we actually do the real extraction.

[Ailrun]

this is easy to fix. just change the name in Equations to s.

Yeah I mean the trade-off (either using a better name in Coq or a better name in OCaml) is sad. It's probably better to use s here.

[HuStmpHrrr]

This PR is ready for review.

[Ailrun]

Other than the repeat thing, LGTM