Library DIStack

Require Import Showable String Decidable List DepEquiv HODepEquiv HoTT.
Local Open Scope string_scope.

Notation "{ x : A & P }" := (sigT (A:=A) (fun x ⇒ P)) : type_scope.
Notation "x .1" := (projT1 x) (at level 3).
Notation "x .2" := (projT2 x) (at level 3).
Notation " ( x ; p ) " := (existT _ x p).

Dependent Stack/Instr

A dstack is a bunch of nested pairs of depth n

Fixpoint dstack (n : nat) : Type :=
  match n with
    | O ⇒ unit
    | S n' ⇒ nat × dstack n'
  end%type.

The dependent instructions dinstr are explicit about their effect on the depth of the dstack

Inductive dinstr : nat → nat → Type :=
| IConst : ∀ (k:nat) {n}, dinstr n (S n)
| IPlus : ∀ {n}, dinstr (S (S n)) (S n).

The stach machine satisfies those depth invariants

Definition exec n n' (i : dinstr n n') : dstack n → dstack n' :=
  match i with
    | IConst n ⇒ fun s ⇒ (n , s )
    | IPlus ⇒ fun s ⇒
                  let '(arg1, (arg2, s')) := s in
                  (arg1 + arg2, s')
  end.

Eval compute in exec 1 _ (IConst 1) (2,tt ).
Eval compute in exec 2 _ IPlus (2, (1, tt )).

Plain stack & instr

There is no need to define plain dstacks: we just use lists of nats, with a condition on their length.

Plain instructions are another inductive, with its Show instance, and the condition is expressed with the valid_instr predicate below (which is decidable).

Inductive instr@{i} : Type@{i} :=
| NConst : nat → instr
| NPlus : instr.

Instance show_instr : Show instr :=
  {| show s :=
       match s with
         | NConst n ⇒ "NConst " ++ show n
         | NPlus ⇒ "NPlus"
       end
  |}.

Definition instr_index n (i:instr) : Cast nat :=
  match i with
    | NConst _ ⇒ creturn (S n)
    | NPlus ⇒ match n with
                 | S (S n) ⇒ creturn (S n)
                 | _ ⇒ Fail _ (Cast_info_wrap "invalid instruction")
               end
  end.

Equivalences

dstack is equivalent to lists through

  {n:nat & dstack n} ~ {l : list nat & length l = n}

Definition dstack_to_list {n} : dstack n → {l : list nat & clift (info := Cast_info) (length (A:=nat)) l = Some n }.
Defined.

Definition list_to_dstack {n} : {l : list nat & clift (info := Cast_info) (length (A:=nat)) l = Some n } → dstack n.
Defined.

Instance DepEquiv_dstack :
dstack ≈ (list nat ) :=
@DepEquiv_eq _ _ (list nat) _ _ _ (clift (length (A:=nat))) (@dstack_to_list) (@list_to_dstack) _ _ _.

dinstr is equivalent to instr through

 {n n': nat & dinstr n n'} ~ {i: instr & valid_instr n i n'}

Definition valid_instr i n n' := instr_index n i = Some n'.

Definition dinstr_to_instr n n' :
  dinstr n n' → {i: instr & valid_instr i n n'} := fun i ⇒
  match i with
    IConst k ⇒ (NConst k; eq_refl )
  | IPlus ⇒ (NPlus ; eq_refl ) end.

Definition Fail_is_not_Some {A info i R} {x:A} :
  @Fail A info i = Some x → R.
Defined.

Definition instr_to_dinstr n n' :
  {i: instr & valid_instr i n n'} → dinstr n n' := fun x ⇒
match x with (i;v) ⇒ match i return valid_instr i n n' → dinstr n n' with

  | NConst k ⇒ fun v ⇒ transport (fun X ⇒ dinstr _ X) (Some_inj v) (IConst k)
  | NPlus ⇒ match n return valid_instr NPlus n n' → dinstr n n'
     with

       0 ⇒ fun v ⇒ Fail_is_not_Some v

     | S 0 ⇒ fun v ⇒ Fail_is_not_Some v

     | S (S n) ⇒ fun v ⇒ transport (fun X ⇒ dinstr _ X) (Some_inj v) (IPlus) end end v end.

Instance DecidablePaths_instr : DecidablePaths instr.
Defined.

Definition transport_instr_Const (n m n0 : nat) (e : S n = m) :
   dinstr_to_instr _ _
     (transport (λ X : nat , dinstr n X) e (IConst n0)) =
   (NConst n0 ; ap Some e ).
Defined.

Definition transport_instr_Plus (n m : nat) (e : S n = m) :
   dinstr_to_instr _ _
     (transport (λ X : nat , dinstr (S (S n)) X) e IPlus) =
   (NPlus ; ap Some e ).
Defined.

Definition DepEquiv_instr_retr n m (x:{i:instr & instr_index n i = Some m }) :
  (dinstr_to_instr _ _) ° (instr_to_dinstr _ _) x = x :=
  match x with (i;v) ⇒
          match i return ∀ v :valid_instr i n m,
              (dinstr_to_instr _ _) ° (instr_to_dinstr _ _) (i ; v ) = id (i ; v ) with

   NConst n0 ⇒ fun v ⇒ transport_instr_Const _ _ _ _ @
                        path_sigma _ (NConst n0; ap (Some (A:=nat)) (Some_inj v))
                                     (NConst n0; v ) eq_refl (is_hprop _ _)
| NPlus ⇒ match n return ∀ v : valid_instr NPlus n m ,
                (dinstr_to_instr _ _) ° (instr_to_dinstr _ _) (NPlus ; v ) = (NPlus ; v )
            with

              0 ⇒ fun v ⇒ Fail_is_not_Some v

            | S 0 ⇒ fun v ⇒ Fail_is_not_Some v

            | S (S n) ⇒ fun v ⇒ transport_instr_Plus _ _ _ @
                               path_sigma _ (NPlus ; ap (Some (A:=nat)) (Some_inj v))
                               (NPlus ; v ) eq_refl (is_hprop _ _) end
            end v end.

Instance DepEquiv_instr n :
  (dinstr n ) ≈ instr
  :=
    @DepEquiv_eq _ _ instr _ _ _
                 (instr_index n)
                 (dinstr_to_instr n)
                 (instr_to_dinstr n) _ _ _.

Lifting

Lifting exec to safely accept instr and list nat

Definition simple_exec : instr → list nat ⇀ list nat := lift2 exec.

Print simple_exec.

Eval compute in simple_exec NPlus (1 :: 2 :: nil).
Eval compute in simple_exec NPlus (1 :: nil).

Print Assumptions simple_exec.

Extraction

Require Import ExtrOcamlString ExtrOcamlNatInt.
Extract Inductive list ⇒ "list" [ "[]" "(::)" ].

Extraction "distack" cast_erasure exec simple_exec.

$ ocaml -init didstack.ml
# (exec 0 0 (IPlus 0) [1;2] : int list);;
- : int list = [3]
# exec 0 0 (IPlus 0) [];;
Segmentation fault: 11

$ ocamlc didstack.mli didstack.ml
# #load "didstack.cmo";;
# open Didstack;;
# simple_exec NPlus [1;2];;
- : int list = [3]                                                                              
# simple_exec NPlus [];;
Exception: (Failure "Cast failure: invalid instruction").