JasonGross

type nat =
| O
| S of nat

(** val fst : ('a1 * 'a2) -> 'a1 **)

let fst = function
| (x, _) -> x

JasonGross

(* -*- coq-prog-args: ("-indices-matter") -*- *)
(** Initial setup stuff to print sigma types with projections rather than as matches *)
Set Primitive Projections.
Set Universe Polymorphism.
Record sigT {A:Type} (P:A -> Type) : Type :=
  existT { pr1 : A ; pr2 : P pr1 }.
Arguments sigT (A P)%type.
Arguments pr1 {A P} _.
Arguments pr2 {A P} _.
Arguments existT {_} _ _ _.

JasonGross

Require Import Coq.ZArith.ZArith.
Require Import Coq.Lists.List.
Set Implicit Arguments.
Reserved Notation "'dlet' x .. y := v 'in' f"
         (at level 200, x binder, y binder, f at level 200, format "'dlet'  x .. y  :=  v  'in' '//' f").
Reserved Notation "'nllet' x .. y := v 'in' f"
         (at level 200, x binder, y binder, f at level 200, format "'nllet'  x .. y  :=  v  'in' '//' f").
Reserved Notation "'elet' x := v 'in' f"
         (at level 200, f at level 200, format "'elet'  x  :=  v  'in' '//' f").
Definition Let_In {A P} (v : A) (f : forall x : A, P x) : P v

JasonGross

Global Set Implicit Arguments.
Reserved Notation "'dlet' x .. y := v 'in' f"
         (at level 200, x binder, y binder, f at level 200, format "'dlet'  x .. y  :=  v  'in' '//' f").
Reserved Notation "'elet' x := v 'in' f"
         (at level 200, f at level 200, format "'elet'  x  :=  v  'in' '//' f").
Definition Let_In {A P} (v : A) (f : forall x : A, P x) : P v
  := let x := v in f x.
Notation "'dlet' x .. y := v 'in' f" := (Let_In v (fun x => .. (fun y => f) .. )).

Inductive expr {var : Type} : Type :=

JasonGross

(** * Expression trees in PHOAS *)
Require Import Coq.ZArith.ZArith.
Global Set Implicit Arguments.
Reserved Notation "'dlet' x .. y := v 'in' f"
         (at level 200, x binder, y binder, f at level 200, format "'dlet'  x .. y  :=  v  'in' '//' f").
Reserved Notation "'elet' x := v 'in' f"
         (at level 200, f at level 200, format "'elet'  x  :=  v  'in' '//' f").
Definition Let_In {A P} (v : A) (f : forall x : A, P x) : P v
  := let x := v in f x.
Notation "'dlet' x .. y := v 'in' f" := (Let_In v (fun x => .. (fun y => f) .. )).

JasonGross

-R . ReifyByPattern
-I .
comparison.v
reify.v
reify.ml4
reify.mllib

JasonGross

Require Import Coq.ZArith.ZArith.
Set Implicit Arguments.
Reserved Notation "'dlet' x .. y := v 'in' f"
         (at level 200, x binder, y binder, f at level 200, format "'dlet'  x .. y  :=  v  'in' '//' f").
Reserved Notation "'nlet' x .. y := v 'in' f"
         (at level 200, x binder, y binder, f at level 200, format "'nlet'  x .. y  :=  v  'in' '//' f").
Reserved Notation "'zlet' x .. y := v 'in' f"
         (at level 200, x binder, y binder, f at level 200, format "'zlet'  x .. y  :=  v  'in' '//' f").
Reserved Notation "'elet' x := v 'in' f"
         (at level 200, f at level 200, format "'elet'  x  :=  v  'in' '//' f").

JasonGross

JasonGross

Require Import Clightdefs.

Delimit Scope None_scope with None.
Delimit Scope C_scope with C.
Delimit Scope Z_scope with Z.
Delimit Scope camlfloat_of_coqfloat_scope with camlfloat_of_coqfloat.
Delimit Scope camlfloat_of_coqfloat32_scope with camlfloat_of_coqfloat32.
Delimit Scope camlint64_of_coqint_scope with camlint64_of_coqint.
Delimit Scope camlint_of_coqint_scope with camlint_of_coqint.
Delimit Scope expr_scope with expr.

JasonGross

Inductive TYPE' : Type -> Type :=
| UNIT' : TYPE' unit
| EMPTY' : TYPE' Empty_set
| SIGMA' {a} (A : TYPE' a) {p} (P : forall v : a, TYPE' (p v)) : TYPE' (@sigT a p)
| PI' {a} (A : TYPE' a) {b} (B : forall v : a, TYPE' (b v)) : TYPE' (forall v : a, b v).
Definition TYPE := { T : _ & TYPE' T }.
Definition interp_TYPE : TYPE -> Type := @projT1 _ _.
Definition UNIT : TYPE := existT _ _ UNIT'.
Definition EMPTY : TYPE := existT _ _ EMPTY'.
Definition SIGMA (A : TYPE) (P : interp_TYPE A -> TYPE) : TYPE