gistfile1.txt

(* Construit un enregistrement à partir d'une liste de paires clé/valeur. *)
(* En cas de doublons, la première valeur associée au champ prime. *)

Fixpoint build_rec (l: list (rec_field*option val)): option (rec_field -> option val) := 
  match l with
    | nil => Some (fun _ => None)
    | (f,v)::l => match (v, build_rec l) with
                    | (Some v', Some r) => Some (update_rec r f v')
                    | _ => None
                  end
  end.

(* Evaluation d'une expression (peut échouer => type option). *)
Fixpoint eval_expr (s: state) (e: exp) {struct e}: option val :=
  match e with
    | Econst v => Some v
    | Erec l =>
      match build_rec (map (fun p => match p with (f,e) => (f, eval_expr s e) end) l) with
        | Some r => Some (Vrec r)
        | _ => None
      end
    | Evar x => s x
    | Eplus e1 e2 => 
      match (eval_expr s e1, eval_expr s e2) with
        | (Some (Vint x1), Some (Vint x2)) => Some (Vint (x1 + x2))
        | _ => None
      end
    | Eminus e1 e2 => 
      match (eval_expr s e1, eval_expr s e2) with
        | (Some (Vint x1), Some (Vint x2)) => Some (Vint (x1 - x2))
        | _ => None
      end
    | Elookup e f =>
      match (eval_expr s e) with
        | Some (Vrec rec) => rec f
        | _ => None
      end
    | Esubst e f new =>
      match (eval_expr s e, eval_expr s new) with
        | (Some (Vrec rec), Some v) =>  
          Some (Vrec (update_rec rec f v))
        | _ => None
      end
  end.