(**************************************************************************
* Proving functional programs through a deep embedding                    *
* Syntax of the embedded language                                         *
***************************************************************************)

Set Implicit Arguments.
Require Export LibCore LibEnv LibVars.
Open Scope int_scope.


(************************************************************)
(* ** Representation of the embedded language *)

(** Representation of primitive operators *)

Inductive builtin : Set :=
  | builtin_throw
  | builtin_add 
  | builtin_sub 
  | builtin_mul 
  | builtin_div 
  | builtin_equ
  | builtin_leq.

(** Representation of constructors *)

Definition con := var.
Canonical Structure Con := 
  @make_obj con var_0 LibVars.beq LibVars.req.

(** Grammar of terms, values and patterns. *)

Inductive trm : Type := 
  | trm_val : val -> trm
  | trm_exn : val -> trm
  | trm_var : var -> trm
  | trm_app : trm -> trm -> trm
  | trm_con : con -> list trm -> trm
  | trm_fix : var -> pat -> trm -> trm -> trm
  | trm_try : trm -> trm -> trm

with val : Type :=
  | val_int : int -> val
  | val_builtin : builtin -> val
  | val_con : con -> list val -> val
  | val_fix : var -> pat -> trm -> trm -> val
 
with pat : Type :=
  | pat_var : var -> pat
  | pat_int : int -> pat
  | pat_con : con -> list pat -> pat
  | pat_wildcard : pat
  | pat_alias : var -> pat -> pat.


(** [novar] is to be given as first argument to [trm_fix]
    and [val_fix] for building non-recursive functions. *)

Definition novar : var := `0.


(************************************************************)
(* ** Builtin data constructors : booleans, tuples,
      options, lists, and primitive exceptions. Each 
      constructor is represented using a unique constant. *)

Definition con_false : con := `1`0.
Definition con_true : con := `2`0.

Definition con_tuple : con := `1`1`0.

Definition con_none : con := `2`1`0.
Definition con_some : con := `2`2`0.

Definition con_nil : con := `1`1`1`0.
Definition con_cons : con := `1`1`2`0.

Definition con_match_failure : con := `2`1`1`0.
Definition con_div_by_zero : con := `2`1`2`0.
Definition con_not_found : con := `2`2`1`0.
Definition con_user_failure : con := `2`2`2`0.


(************************************************************)
(* ** Builtin encoders *)

(** [code A] is the type of encoders for the type [A]. *)

Definition code (A:Type) := A -> val.  

(** Encoders for values, integers, unit, booleans, 
    options, lists and tuples. *)

Definition _Val (t:val) := t.

Definition _Int n := val_int n.

Definition _Unit (_:unit) := val_con con_tuple nil.

Definition _Bool b := 
  match b with
  | true =>  val_con con_true  nil
  | false => val_con con_false nil
  end.

Definition _Option (A : Type) _A (x : option A) := 
  match x with
  | Some v => val_con con_some ((_A v)::nil)
  | None => val_con con_none nil
  end.

Definition _List (A : Type) (_A:code A) : (list A)->val :=
  (fix f (x:list A) {struct x} :=
  match x with 
  | nil => val_con con_nil nil
  | cons h t => val_con con_cons ((_A h)::(f t)::nil)
  end).

Section Tuples.

Variables (A1 A2 A3 A4 : Type).
Variables (_A1 : code A1) (_A2 : code A2)
          (_A3 : code A3) (_A4 : code A4).

Definition _Tup2 x := 
  match x with (x1,x2) => 
    val_con con_tuple ((_A1 x1)::(_A2 x2)::nil)
  end.

Definition _Tup3 x := 
  match x with (x1,x2,x3) => 
    val_con con_tuple ((_A1 x1)::(_A2 x2)::(_A3 x3)::nil)
  end.

Definition _Tup4 x := 
  match x with (x1,x2,x3,x4) => 
    val_con con_tuple ((_A1 x1)::(_A2 x2)::(_A3 x3)::(_A4 x4)::nil)
  end.

End Tuples.

(** The notation [#N _A1 .. _AN] stands for the encoder for
    an [N]-ary tuple whose components are encoded with encoders [Ai].
    Notation [_A1 _x _A2] is also available for pairs. *)

Notation "'#2' _A1 _A2" := 
  (@_Tup2 _ _ _A1 _A2)
  (at level 38, _A1 at level 0, _A2 at level 0)
  : encoder_scope.
Notation "'#3' _A1 _A2 _A3" := 
  (@_Tup3 _ _ _ _A1 _A2 _A3) 
  (at level 38, _A1 at level 0, _A2 at level 0, _A3 at level 0)
  : encoder_scope.
Notation "'#4' _A1 _A2 _A3 _A4" := 
  (@_Tup4 _ _ _ _ _A1 _A2 _A3 _A4) 
  (at level 38, _A1 at level 0, _A2 at level 0, _A3 at level 0,
   _A4 at level 0)
  : encoder_scope.
Notation "_A1 '_x' _A2" := 
  (@_Tup2 _ _ _A1 _A2)
  (at level 38, no associativity, _A2 at next level)
  : encoder_scope.

Open Scope encoder_scope.