• Página da distribuição de OCaml

• Didier Rémy. Using, understanding, and unraveling the OCaml language. In G. Barthe, P. Dybjer, L. Pinto, and J. Saraiva, editors,Applied Semantics, number 2395 in Lecture Notes in Computer Science, pages 413–536. Springer, 2002. INF: 681.32.06(063) I61as.

Uma introdução a OCaml de um dos autores.

• Emmanuel Chailloux, Pascal Manoury, and Bruno Pagano. Developing applications with Objective Caml. O'Reilly, 2000.
• Jason Hickey. Introduction to the objective caml language, 2002.
• Xavier Leroy. An introduction to the objective caml language and its type system.

(* 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
;;

(* o estado: uma função das locais para números inteiros *)
type sigma = loc -> 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 das expressões aritméticas *)
let rec eval_aExpr (a,sigma) =
  match a with 
    Num n -> n
  | Loc l -> sigma l
  | 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))
;;

(* avaliação das expressões booleanas *)
let rec eval_bExpr (b,sigma) =
  match b with
    Bool b -> b
  | Eq (a1,a2) -> (eval_aExpr (a1,sigma)) = (eval_aExpr (a2,sigma))
  | Lt (a1,a2) -> (eval_aExpr (a1,sigma)) < (eval_aExpr (a2,sigma))
  | Not b -> not (eval_bExpr (b,sigma))
  | And (b1,b2) -> eval_bExpr(b1,sigma) && eval_bExpr(b2,sigma)
  | Or (b1,b2) -> eval_bExpr(b1,sigma) || eval_bExpr(b2,sigma)
;;

(* avaliação das comandos: semântica operacional natural *)
let rec eval_com_nat = function
    (Skip,sigma) -> sigma
  | (Assign (l,a),sigma) -> mapsto sigma l (eval_aExpr (a,sigma))
  | (Seq (c1,c2),sigma) -> eval_com_nat(c2,eval_com_nat(c1,sigma))
  | (Cond(b,c1,c2),sigma) -> if ( eval_bExpr (b,sigma)) then eval_com_nat(c1,sigma) else eval_com_nat(c2,sigma)
  | (While(b,c1) as w, sigma) -> if (eval_bExpr(b,sigma)) then eval_com_nat(Seq(c1,w),sigma) else sigma
  | (_, sigma) -> raise SemValor;
;;

(* 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))))));;

let estado_final = eval_com_nat(programa,empty);;

# estado_final "x";;
- : num = 362880
# estado_final "n";;
- : num = 10

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>);
 
  ...