Implement type checker

[Ailrun]

The extracted code for type_check/type_infer (under ExtrOcamlBasic and ExtrOcamlNatBigInt) is

(** val type_check : exp list -> exp -> exp -> bool **)

let rec type_check g a m =
  match type_infer g m with
  | Some a0 -> subtyping_impl g (nf_to_exp a0) a
  | None -> false

(** val type_infer : exp list -> exp -> nf option **)

and type_infer g = function
| A_zero -> Some Nf_nat
| A_succ e -> if type_check g A_nat e then Some Nf_nat else None
| A_natrec (e, e0, e1, e2) ->
  if type_check g A_nat e2
  then (match type_infer (A_nat :: g) e with
        | Some a ->
          (match a with
           | Nf_typ _ ->
             if type_check g (A_sub (e, (A_extend (A_id, A_zero)))) e0
             then if type_check (e :: (A_nat :: g)) (A_sub (e, (A_extend ((A_compose (A_weaken, A_weaken)), (A_succ (A_var
                       (Big_int_Z.succ_big_int Big_int_Z.zero_big_int))))))) e1
                  then Some (nbe_ty_impl g (A_sub (e, (A_extend (A_id, e2)))))
                  else None
             else None
           | _ -> None)
        | None -> None)
  else None
| A_nat -> Some (Nf_typ Big_int_Z.zero_big_int)
| A_typ n -> Some (Nf_typ (Big_int_Z.succ_big_int n))
| A_var n -> (match lookup g n with
              | Some a -> Some (nbe_ty_impl g a)
              | None -> None)
| A_fn (e, e0) ->
  (match type_infer g e with
   | Some a ->
     (match a with
      | Nf_typ _ -> (match type_infer (e :: g) e0 with
                     | Some a0 -> Some (Nf_pi ((nbe_ty_impl g e), a0))
                     | None -> None)
      | _ -> None)
   | None -> None)
| A_app (e, e0) ->
  (match type_infer g e with
   | Some s ->
     (match s with
      | Nf_pi (n, n0) ->
        if type_check g (nf_to_exp n) e0 then Some (nbe_ty_impl g (A_sub ((nf_to_exp n0), (A_extend (A_id, e0))))) else None
      | _ -> None)
   | None -> None)
| A_pi (e, e0) ->
  (match type_infer g e with
   | Some a ->
     (match a with
      | Nf_typ n ->
        (match type_infer (e :: g) e0 with
         | Some a0 -> (match a0 with
                       | Nf_typ n0 -> Some (Nf_typ (max n n0))
                       | _ -> None)
         | None -> None)
      | _ -> None)
   | None -> None)
| A_sub (_, _) -> None

and for type_check_closed,

(** val type_check_closed : exp -> exp -> bool **)

let type_check_closed a m =
  match type_infer [] a with
  | Some a0 -> (match a0 with
                | Nf_typ _ -> type_check [] a m
                | _ -> false)
  | None -> false

[HuStmpHrrr]

     (match a with
      | Nf_pi (n, n0) ->
          let a0 = (n, n0) in

looks unnecessary. how is it generated?

[Ailrun]

@HuStmpHrrr
It seems like this gives that.

Equations get_subterms_of_pi_nf (A : nf) : { '(B, C) | A = n{{{ Π B C }}} } + { forall B C, A <> n{{{ Π B C }}} } :=
  | n{{{ Π B C }}} => pureo (exist _ (B, C) _)
  | _              => inright _

[Ailrun]

What do you mean by curry it? I mean, it is the returned value, not arguments.

[HuStmpHrrr]

instead of { '(B, C) | A = n{{{ Π B C }}} }, try { B & { C | A = n{{{ Π B C }}} } }

[Ailrun]

@HuStmpHrrr With that, it has

(match a with
      | Nf_pi (n, n0) ->
        let a0 = ExistT (n, n0) in
        let ExistT (a1, s) = a0 in

so I guess it doesn't help in terms of the extracted code. However, it gives a better in-coq implementation, so I pushed it.

[HuStmpHrrr]

@HuStmpHrrr With that, it has

(match a with
      | Nf_pi (n, n0) ->
        let a0 = ExistT (n, n0) in
        let ExistT (a1, s) = a0 in

so I guess it doesn't help in terms of the extracted code. However, it gives a better in-coq implementation, so I pushed it.

Wtf. This still sucks. I really wish something better can be done here.

[Ailrun]

I don't see an easy way to resolve that unless we just directly inline the function even in Coq.

[HuStmpHrrr]

if you are fine with it I think it's worth it to get rid of the glitch like this.

[Ailrun]

You mean inlining the function? I don't think that's very optimal in terms of development, but the function is used once anyway... Ok, let's inline that.

[HuStmpHrrr]

You mean inlining the function? I don't think that's very optimal in terms of development, but the function is used once anyway... Ok, let's inline that.

Yeah, I think that's fine for this. I'm surprised the extraction doesn't take care of it.

[Ailrun]

Updated.