Library programming_machine

Require Import listaux.
Require Import Omega.

Inductive value:Type:=
|value_none: value
|value_nat: nat->value
|value_listnat: list nat -> value
.

Inductive variable:Type:=
|var_argument : nat->variable
|var_scope : nat->variable
.

Inductive unioperation:Type:=
|unioperation_len : unioperation
.

Inductive binoperation:Type:=
|binoperation_plus : binoperation
|binoperation_minus : binoperation
|binoperation_lt : binoperation
|binoperation_and : binoperation
|binoperation_get : binoperation
.

Inductive expression:Type:=
|exp_variable: variable->expression
|exp_constant: value->expression
|exp_unioperation: unioperation->expression->expression
|exp_binoperation: binoperation->expression->expression->expression
.

Inductive statement:Type:=
|statement_assignment : variable->expression ->statement
|statement_listset : variable -> expression -> expression -> statement
.

Inductive program:Type:=
|program_nil : program
|program_cons : statement -> program -> program
|program_loop : loop -> program -> program
with loop:Type:=
|loop_intro : expression -> program -> loop
.

Definition memory:= ((list value)*(list value))%type.

Definition variable_value (m:memory) (var:variable) : value :=
let (argument,scope):=m in
match var with
|var_argument n => nth n argument value_none
|var_scope n => nth n scope value_none
end.

Definition cast_value_bool (v:value):bool:=
match v with
|value_none => false
|value_nat n => match n with O=>false|S p=>true end
|value_listnat l => match l with nil=>false|cons _ _=>true end
end.

Fixpoint expression_value (m:memory) (e:expression) {struct e} : value :=
match e with
|exp_variable var => variable_value m var
|exp_constant val => val
|exp_unioperation op e =>
  let v:=expression_value m e in
  match op with
  | unioperation_len =>
   match v with
   |value_none => value_none
   |value_nat _ => value_none
   |value_listnat l => value_nat (length l)
   end
  end
|exp_binoperation op e1 e2 =>
  let v1:=expression_value m e1 in
  let v2:=expression_value m e2 in
  match op with
  |binoperation_plus =>
   match v1 with
   |value_nat n1 =>
    match v2 with
    |value_nat n2 => value_nat (n1+n2)
    |_ => value_none
    end
   |_ => value_none
   end
  |binoperation_minus =>
   match v1 with
   |value_nat n1 =>
    match v2 with
    |value_nat n2 => value_nat (n1-n2)
    |_ => value_none
    end
   |_ => value_none
   end
  |binoperation_lt =>
   match v1 with
   |value_nat n1 =>
    match v2 with
    |value_nat n2 =>
     match le_lt_dec n2 n1 with
     |left _ => value_nat 0
     |right _ => value_nat 1
     end
    |_ => value_none
    end
   |_ => value_none
   end
  |binoperation_and =>
      if (andb (cast_value_bool v1) (cast_value_bool v2))
      then value_nat 1
      else value_nat 0
  |binoperation_get =>
   match v1 with
   |value_listnat l =>
    match v2 with
    |value_nat n => value_nat (nth n l 0)
    |_ => value_none
    end
   |_ => value_none
   end
  end
end.

Definition statement_execute (ST:statement) (mem:memory):memory:=
let (argument,scope):=mem in
   match ST with
   |statement_assignment var exp =>
     match var with
     |var_scope p => (argument,setandraise p scope (expression_value mem exp) value_none)
     |var_argument p => (setandraise p argument (expression_value mem exp) value_none,scope)
     end
   |statement_listset var exppos exp =>
     match var with
     |var_scope p => match nth p scope value_none with
       |value_none => mem
       |value_nat _ => mem
       |value_listnat l =>
        match (expression_value mem exp) with
        |value_none => mem
        |value_nat vn => match expression_value mem exppos with
         |value_none => mem
         |value_nat pos =>
               (argument,
               setandraise p scope (value_listnat(setandraise pos l vn O)) value_none
               )
         |value_listnat _ => mem
         end
        |value_listnat _ => mem
        end
       end
     |var_argument p => mem
     end
   end.


Fixpoint execute (P:program) (mem:memory) (limit:nat) {struct limit}: (nat*memory):=
match limit with
|O=> (O,mem)
|S plimit=>
 match P with
 |program_nil => (1,mem)
 |program_cons ST P' =>
  let m:=statement_execute ST mem
  in let (n',m'):=execute P' m plimit in
      (match n' with O=>0|S _=> S n' end,m')
 |program_loop L P' =>
    let (n,m):= loop_execute L mem plimit in
    match n with
    |O=>(0,m)
    |S _ => let (n',m'):=(execute P' m plimit) in
      (match n' with O=>0|S _=>n'+n end,m')
    end
end
end
with loop_execute (L:loop) (mem:memory) (limit:nat) {struct limit}: (nat*memory):=
match limit with
|O => (O,mem)
|S plimit=>
 match L with
 loop_intro e P =>
  let val:=expression_value mem e in
  match cast_value_bool(val) with
  |true => let (n1,m1):=execute P mem plimit in
        match n1 with
        |O=>(0,m1)
        |S_=>
           let (n2,m2):=loop_execute L m1 plimit in
           match n2 with
           |O=>(0,m2)
           |S_=> (n1+n2,m2)
           end
        end
  |false => (1,mem)
  end
 end
end
.

Eval compute in
 execute
 (program_cons
  (statement_assignment (var_scope 3) (exp_constant (value_nat 5)))
  program_nil
 )
 (nil, nil)
 1000.

Theorem infinity: exists P:program, forall (mem:memory) (limit:nat),
 let (n,m):=execute P mem limit in n=0.
Proof.
exists (program_loop
 (loop_intro (exp_constant (value_nat 1)) program_nil) program_nil).
intros.
destruct limit. simpl. auto.
revert mem. simpl.
induction limit. simpl. auto.
intros.
simpl.
destruct (execute program_nil mem limit) as [n1 m1].
specialize(IHlimit m1).
destruct limit. simpl. destruct n1;auto.
set(X:=loop_execute _ _ _) in IHlimit|-*.
simpl in X.
destruct X.
destruct n. destruct n1;auto.
simpl in IHlimit. inversion IHlimit.
Qed.

Theorem loop_nil: forall (E:expression) (mem:memory) (limit:nat),
 loop_execute (loop_intro E program_nil) mem limit=
 match limit with
 |O=>(0,mem)
 |S _=>
  match cast_value_bool(expression_value mem E) with
  |true => (0,mem)
  |false => (1,mem)
  end
 end.
Proof.
intros. induction limit. simpl. auto.
simpl.
destruct(cast_value_bool (expression_value mem E));auto.
set(X:=execute program_nil mem limit).
destruct limit. simpl in *|-*. auto.
simpl in X. unfold X. rewrite IHlimit. auto.
Qed.

Scheme program_loop_rect := Induction for program Sort Type
with loop_program_rect := Induction for loop Sort Type.

Theorem program_rect_expanded: forall (P : program -> Type)
    (IHnil:P program_nil)
    (IHcons: forall (ST : statement) (p : program), P p ->
           P (program_cons ST p))
    (IHloop:forall (Le:expression) (Lp : program) (p : program),
           P p -> P Lp ->
           P (program_loop (loop_intro Le Lp) p) ),
       forall p : program, P p.
Proof.
intros.
set(PL:=fun L:loop=> match L with loop_intro Le Lp =>P Lp end).
assert(R:=program_loop_rect P PL). apply R;clear R.
+ exact IHnil.
+ intros. apply IHcons. exact X.
+ intros. destruct l. apply IHloop;auto.
+ simpl. auto.
Qed.