Ferramentas de Utilizador

Ferramentas de Site


ocaml

Esta é uma versão antiga do documento!

Links

  • Página da distribuição de OCaml

Referências

Material

Sintaxe abstrata do IMP

(* categoria sintatica Num *)
type num = int;;

(* categoria sintatica Ident *)
type ident = string;;

(* categoria sintatica Bool: usamos bool *)

(* categoria sintatica AExpr *)
type aExpr =   Num of num | Ident of ident
             | Sum of aExpr * aExpr 
             | Diff of aExpr * aExpr
             | Prod of aExpr * aExpr;;

(* categoria sintatica BExpr *)
type bExpr =   Bool of bool
             | Eq of aExpr * aExpr | Lt of aExpr * aExpr
             | Not of bExpr
             | And of bExpr * bExpr
             | Or of bExpr * bExpr;;

(* categoria sintatica Com *)
type com =   Skip
             | Assign of ident * aExpr
             | Seq of com * com
             | Cond of bExpr * com * com
             | While of bExpr * com
;;

Estados

(* o estado: uma função das identificadores para números inteiros *)
type sigma = ident -> num;;

(* o estado inicial *)
let empty : sigma = function x -> 0;;

(* um estado modificado em um ponto: sigma[l -> n] *)
let mapsto f l n a = if a = l then n else f a;;

Avaliação de expressões aritméticas

(* avaliação das expressões aritméticas *)
let rec eval_aExpr (a,sigma) =
  match a with 
    Num n -> n
  | Ident x -> sigma x
  | Sum (a1,a2) -> (eval_aExpr (a1,sigma))+(eval_aExpr (a2,sigma))
  | Diff (a1,a2) -> (eval_aExpr (a1,sigma))-(eval_aExpr (a2,sigma))
  | Prod (a1,a2) -> (eval_aExpr (a1,sigma))*(eval_aExpr (a2,sigma))
;;

Exercício 4.2: SOE de IMP em OCaml

type estado = Final of sigma | Intermediario of com * sigma;;

exception SemSuccessor;;

(* avaliação dos comandos: semântica operacional estrutural *)
let rec eval_one_com_est = function
    Final s -> raise SemSuccessor
  | Intermediario (Skip,s) -> Final s
  | Intermediario (Assign(l,a),s) -> Intermediario (Skip,mapsto s l (eval_aExpr (a,s)))
  | Intermediario (Seq(c1,c2),s) -> let e = eval_one_com_est (Intermediario (c1,s)) in
    begin
      match e with
	Final s' -> Intermediario(c2,s')
      | Intermediario(c1',s') -> Intermediario(Seq(c1',c2),s')
    end
  | Intermediario (Cond(b,c1,c2),s) -> if eval_bExpr(b,s) then Intermediario(c1,s) else Intermediario(c2,s)
  | Intermediario (While (b,c1) as w,s) -> Intermediario(Cond(b,Seq(c1,w),Skip),s)
  | Intermediario (_,s) -> raise SemSuccessor
;;

let rec eval_com_est e = try e::(eval_com_est (eval_one_com_est e)) with SemSuccessor -> [e];;

(* Exemplo *)
let programa = Seq(Assign("n",Num 1),Seq(Assign("x",Num 1),While(Lt(Loc "n",Num 10),Seq(Assign("x",Prod(Loc "x",Loc "n")),Assign("n",Sum(Loc "n", Num 1))))));;

# eval_com_est (Intermediario(programa,empty));;
- : estado list =
[Intermediario
  (Seq (Assign ("n", Num 1),
    Seq (Assign ("x", Num 1),
     While (Lt (Loc "n", Num 10),
      Seq (Assign ("x", Prod (Loc "x", Loc "n")),
       Assign ("n", Sum (Loc "n", Num 1)))))),
  <fun>);
 Intermediario
  (Seq (Skip,
    Seq (Assign ("x", Num 1),
     While (Lt (Loc "n", Num 10),
      Seq (Assign ("x", Prod (Loc "x", Loc "n")),
       Assign ("n", Sum (Loc "n", Num 1)))))),
  <fun>);
 Intermediario
  (Seq (Assign ("x", Num 1),
    While (Lt (Loc "n", Num 10),
     Seq (Assign ("x", Prod (Loc "x", Loc "n")),
      Assign ("n", Sum (Loc "n", Num 1))))),
  <fun>);
 
  ...
ocaml.1156901736.txt.gz · Esta página foi modificada pela última vez em: 2010/01/18 15:45 (Edição externa)