The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi, Agnès

If I undestand well your program, your evaluation function is 
parameterized by some
list of expressions (the list_exp parameter) , and the problem comes 
from you
use this parameter in recursive calls.

May I suggest to consider a main function eval_list whose 
structural_argument is
a list of expr, and having eval_exp as an auxiliary function ?
Something like that (perhaps does not fit your exact wish, but may be 
it's worth to
try this way ?)

Cheers,
Pierre
Require Import List.


Inductive exp : Set :=
|Espace : exp
|Emot : nat -> exp
|Eop : operation -> list exp -> exp.

Parameter env_extern : list nat.
Parameter list_exp : list exp.
Parameter Et : exp -> exp -> exp.
Parameter in_bool: (nat -> nat -> bool) -> nat -> list nat -> bool.

Require Import Coq.Arith.EqNat.

Fixpoint eval_list (l:list exp)(e:exp) {struct l}: option exp  :=
let eval_exp :=
(fix eval_exp (e:exp) : option exp :=
    match e with
| Espace => Some Espace
| Emot id => Some (Emot id)
| Eop OP2pt (e1::e2::nil) =>
    (match (eval_exp e1) with
    |Some(Emot id1) => (match (eval_exp e2) with
               |Some (Emot id2) => if in_bool beq_nat id2 env_extern
             then Some Espace
             else None
   |_ => None
                       end)
     |_ => None
  end)
  |Eop Opany (e1::e2::nil) => eval_list l e1

  | _ => None
  end)
 in
  match l with | nil => None
               | e'1::l1 => eval_list l1 (Et e'1 e)
          end.








agnes gonnet wrote:

> Hi,
>
> could anyone explain me what is wrong with the following mutually 
> recursive functions :
>
>
> Inductive operation : Set :=
> |OP2pt : operation
> |OPany : operation.
>
> Inductive exp : Set :=
> |Espace : exp
> |Emot : nat -> exp
> |Eop : operation -> list exp -> exp.
>
> Parameter env_extern : list nat.
> Parameter list_exp : list exp.
> Parameter Et : exp -> exp -> exp.
> Parameter in_bool: (nat -> nat -> bool) -> nat -> list nat -> bool.
>
>
> Fixpoint eval_exp  (e:exp) {struct e}: option exp  :=
> match e with
>  | Espace => Some Espace
>  | Emot id => Some (Emot id)
>  | Eop OP2pt (e1::e2::nil) =>
>      match (eval_exp e1) with
>      |Some(Emot id1) => match (eval_exp e2) with
>                 |Some (Emot id2) => if in_bool beq_nat id2 env_extern
>               then Some Espace
>               else None
>     |_ => None
>     end
>       |_ => None
>       end
>
>  |Eop Opany (e1::e2::nil) =>  eval_op list_exp e2
>  |_ => None
> end
> with eval_op  (l:list exp) (e:exp) {struct l} : option exp :=
>   match l with
>   |nil => Some (Espace)
>   |e1::l1 => match (eval_exp (Eop OP2pt (e1::e::nil))) with
>     |Some res => match (eval_op l1 e) with
>            |Some res1 => Some (Et res res1)
>            |None => None
>            end
>     |None => None
>     end
>    end.
>
>
> Thanks.
>
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club