Set Implicit Arguments.
Require Export LibCore LibEnv LibVars.
Open Scope int_scope.
Inductive builtin : Set :=
| builtin_throw
| builtin_add
| builtin_sub
| builtin_mul
| builtin_div
| builtin_equ
| builtin_leq.
Definition con := var.
Canonical Structure Con :=
@make_obj con var_0 LibVars.beq LibVars.req.
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.
Definition novar : var := `0.
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.
Definition code (A:Type) := A -> val.
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.
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.