111 lines
4.8 KiB
OCaml
111 lines
4.8 KiB
OCaml
open List
|
|
|
|
(* définition des différents types : tout est à reprendre et étendre *)
|
|
type expr =
|
|
Const of int
|
|
| BConst of bool
|
|
| Add of expr*expr
|
|
| Mul of expr*expr
|
|
| Min of expr*expr
|
|
| Eq of expr*expr
|
|
| Gt of expr*expr
|
|
| Lt of expr*expr
|
|
| Gte of expr*expr
|
|
| Lte of expr*expr
|
|
| Band of expr*expr
|
|
| Bor of expr*expr
|
|
| ITE of expr*expr*expr
|
|
| PrInt of expr
|
|
| Var of string
|
|
| LetIn of string*expr*expr
|
|
| Fun of string*expr
|
|
| App of expr*expr
|
|
|
|
type valeur = VInt of int | VBool of bool | VFunc of string*expr
|
|
|
|
type env = (string*valeur) list
|
|
|
|
let empty_env = []
|
|
|
|
exception InvalidTypeException of (string*valeur) (** expected, given **)
|
|
exception UnknownVariableException of (string*env) (** query, env **)
|
|
|
|
|
|
let valToConstExpr v = match v with
|
|
| VInt(k) -> Const(k)
|
|
| VBool(b) -> BConst(b)
|
|
| VFunc(var,e) -> Fun(var,e)
|
|
|
|
let rec readVar env v0 e = match env with
|
|
| [] -> raise e
|
|
| (v,x)::t -> if (v0 = v) then x else readVar t v0 e
|
|
|
|
let rec decontextifier e env = match e with
|
|
| Const(_) | BConst(_)-> e
|
|
| Fun(v,e) -> Fun(v,decontextifier e (filter (fun (var,x)->not (v=var)) env)) (* On enlève de l'environnement toutes les occurences de v *)
|
|
| Add(e1,e2) -> Add(decontextifier e1 env, decontextifier e2 env)
|
|
| Mul(e1,e2) -> Mul(decontextifier e1 env, decontextifier e2 env)
|
|
| Min(e1,e2) -> Min(decontextifier e1 env, decontextifier e2 env)
|
|
| Gt(e1,e2) -> Gt(decontextifier e1 env, decontextifier e2 env)
|
|
| Lt(e1,e2) -> Lt(decontextifier e1 env, decontextifier e2 env)
|
|
| Gte(e1,e2) -> Gte(decontextifier e1 env, decontextifier e2 env)
|
|
| Lte(e1,e2) -> Lte(decontextifier e1 env, decontextifier e2 env)
|
|
| Eq(e1,e2) -> Eq(decontextifier e1 env, decontextifier e2 env)
|
|
| Band(e1,e2) -> Band(decontextifier e1 env, decontextifier e2 env)
|
|
| Bor(e1,e2) -> Bor(decontextifier e1 env, decontextifier e2 env)
|
|
| ITE(ec,e1,e2) -> ITE(decontextifier ec env, decontextifier e1 env, decontextifier e2 env)
|
|
| PrInt e1 -> PrInt(decontextifier e1 env)
|
|
| Var(v) ->
|
|
begin
|
|
try
|
|
valToConstExpr (readVar env v (UnknownVariableException (v,env)))
|
|
with UnknownVariableException(_,_) -> Var(v) (* Si ce n'est pas dans le contexte, on ne décontextualise pas *)
|
|
end
|
|
| LetIn(v,e0,e1) -> LetIn(v,decontextifier e0 env, decontextifier e1 (filter (fun (var,x)->not (v=var)) env))
|
|
| App(e0,e1) -> App(decontextifier e0 env, decontextifier e1 env)
|
|
|
|
let rec intIntOp op e1 e2 env = match (eval e1 env, eval e2 env) with
|
|
| VInt k1,VInt k2 -> VInt(op k1 k2)
|
|
| x,VInt k2 -> raise (InvalidTypeException ("Int",x))
|
|
| _,y -> raise (InvalidTypeException ("Int",y))
|
|
and intBoolOp op e1 e2 env = match (eval e1 env, eval e2 env) with
|
|
| VInt k1,VInt k2 -> VBool(op k1 k2)
|
|
| x,VInt k2 -> raise (InvalidTypeException ("Int",x))
|
|
| _,y -> raise (InvalidTypeException ("Int",y))
|
|
(* sémantique opérationnelle à grands pas *)
|
|
and eval e env = match e with
|
|
| Const(k) -> VInt k
|
|
| BConst(b) -> VBool b
|
|
| Fun(v,e) -> VFunc(v,decontextifier e (filter (fun (var,_)->not (v=var)) env)) (* On enlève de l'environnement toutes les occurences de v *)
|
|
| Add(e1,e2) -> intIntOp ( + ) e1 e2 env
|
|
| Mul(e1,e2) -> intIntOp ( * ) e1 e2 env
|
|
| Min(e1,e2) -> intIntOp ( - ) e1 e2 env
|
|
| Gt(e1,e2) -> intBoolOp ( > ) e1 e2 env
|
|
| Lt(e1,e2) -> intBoolOp ( < ) e1 e2 env
|
|
| Gte(e1,e2) -> intBoolOp ( >= ) e1 e2 env
|
|
| Lte(e1,e2) -> intBoolOp ( <= ) e1 e2 env
|
|
| Eq(e1,e2) -> (match (eval e1 env, eval e2 env) with
|
|
| VInt k1,VInt k2 -> VBool (k1=k2)
|
|
| VBool k1,VBool k2 -> VBool (k1=k2)
|
|
| (x,y) -> raise (InvalidTypeException ("mismatch",x)))
|
|
| Band(e1,e2) -> (match (eval e1 env, eval e2 env) with
|
|
| VBool b1,VBool b2 -> VBool (b1 && b2)
|
|
| x,VBool k2 -> raise (InvalidTypeException ("Bool",x))
|
|
| _,y -> raise (InvalidTypeException ("Bool",y)))
|
|
| Bor(e1,e2) -> (match (eval e1 env, eval e2 env) with
|
|
| VBool b1,VBool b2 -> VBool (b1 || b2)
|
|
| x,VBool k2 -> (raise (InvalidTypeException ("Bool",x)))
|
|
| _,y -> raise (InvalidTypeException ("Bool",y)))
|
|
| ITE(ec,e1,e2) -> (match (eval ec env) with
|
|
| VBool bc -> eval (if bc then e1 else e2) env
|
|
| x -> raise (InvalidTypeException ("Bool",x)))
|
|
| PrInt e1 -> (match (eval e1 env) with
|
|
| VInt k -> VInt k
|
|
| x -> raise (InvalidTypeException ("Int",x)))
|
|
| Var(v) -> readVar env v (UnknownVariableException (v,env))
|
|
| LetIn(v,e0,e1) -> eval e1 (let x=(eval e0 env) in if v="_" then env else (v,x)::env) (* Le let est là pour forcer l'évaluation *)
|
|
| App(e0,e1) -> (match (eval e0 env) with
|
|
| VFunc(v,e) -> eval (LetIn(v,e1,e)) env (* On utilise l'équivalence (fun x->e) y <=> let x=y in e *)
|
|
| x -> raise (InvalidTypeException ("Func",x)))
|
|
|