Commit 8d8ef8c3 authored by charguer's avatar charguer
Browse files

normalization_doc

parent 90a9b46c
......@@ -26,12 +26,14 @@ let fresh_var =
type etrm =
| Evar of var
(* x *)
| Ecst of int
| Ebool of bool
(* b *)
| Eint of int
(* n *)
| Econstr of cstr * etrms
(* C(e1, ..., en) *)
| Eapp of etrm * etrm
(* (e1 e2) *)
| Eapp of etrm * etrms
(* (e0 e1 .. en) *)
| Elet of var * etrm * etrm
(* let(rec) x = e1 in e2 *)
| Eif of etrm * etrm * etrm
......@@ -40,6 +42,10 @@ type etrm =
(* match e1 with bes *)
| Efun of var * etrm
(* fun x -> e1 *)
| Elazyand of etrm * etrm
(* e1 && e2 *)
| Elazyor of etrm * etrm
(* e1 || e2 *)
and etrms = etrm list
......@@ -53,13 +59,21 @@ and ebranches = ebranch list
(*************************************************************)
(* Target language *)
type logic_fct =
| Logic_add (* + *)
| Logic_and (* && *)
| Logic_or (* || *)
type aval =
| Avar of var
(* x *)
| Acst of int
| Abool of bool
(* b *)
| Aint of int
(* n *)
| Aconstr of cstr * avals
(* C(v1, ..., vn) *)
| Alogic of logic_fct * avals
(* Note: at runtime, type aval also includes closures,
but there are no closures in the source code.
......@@ -70,8 +84,8 @@ and avals = aval list
type atrm =
| Aval of aval
(* v *)
| Aapp of aval * aval
(* (v1 v2) *)
| Aapp of aval * avals
(* (v0 v1 .. vn) *)
| Alet of var * atrm * atrm
(* let x = t1 in t2 *)
| Aletfun of var * var * atrm * atrm
......@@ -131,6 +145,29 @@ let apply_binding b t0 =
let apply_bindings bs t0 =
List.fold_right apply_binding bs t0
(** [apply_bindings_to_res (r,bs)] is like the above,
except that it converts the result [r] into a term [t0],
using [atrm_of_res]. *)
let apply_bindings_to_res (r,bs) =
let t0 = atrm_of_res r in
apply_bindings bs t0
(** [val_bindings_of_res_bindings (r,bs)] produces
a pair [(v,bs')]. When the result [r] is a term [t]
and not a value, it is replaced with a variable[x],
and [x] is bound to [t] is [bs']. *)
let val_bindings_of_res_bindings (r,bs) =
match r with
| ResVal v -> (v, bs)
| ResTrm t ->
let x = fresh_var() in
let v = Avar x in
let bs2 = bs @ [BindingTrm (x,t)] in
(v, bs2)
(*************************************************************)
(* Translation *)
......@@ -155,34 +192,31 @@ let apply_bindings bs t0 =
*)
let rec tr_val e =
let (r,bs) = tr_any e in
match r with
| ResVal v -> (v, bs)
| ResTrm t ->
let x = fresh_var() in
let v = Avar x in
let bs2 = bs @ [BindingTrm (x,t)] in
(v, bs2)
val_bindings_of_res_bindings (tr_any e)
and tr_trm e =
let (r,bs) = tr_any e in
let t0 = atrm_of_res r in
apply_bindings bs t0
apply_bindings_to_res (tr_any e)
and tr_any e =
match e with
| Evar x ->
(ResVal(Avar x), [])
| Ecst n ->
(ResVal(Acst n), [])
| Ebool b ->
(ResVal(Abool b), [])
| Eint n ->
(ResVal(Aint n), [])
| Econstr (c,es) ->
let (vs,bs) = tr_vals es in
(ResVal(Aconstr(c, vs)), bs)
| Eapp (e1,e2) ->
let (vs,bs) = tr_vals [e1;e2] in
begin match vs with
| [v1;v2] -> (ResTrm(Aapp(v1, v2)), bs)
| _ -> assert false
| Eapp (e0,es) ->
let (vs,bs) = tr_vals es in
begin match e0 with
| Evar "+" -> (* total function directly reflected in the logic *)
(ResVal(Alogic(Logic_add, vs)), bs)
| _ ->
let (v0,b0) = tr_val e0 in
(ResTrm(Aapp(v0, vs)), bs @ b0)
(* assuming right-to-left evaluation, else use [b0 @ bs] *)
end
| Elet (f,Efun(x,e1),e2) ->
let t1 = tr_trm e1 in
......@@ -207,6 +241,33 @@ and tr_any e =
let (v1,bs1) = tr_val e1 in
let bas = List.map (fun (p,e) -> (p, tr_trm e)) bes in
(ResTrm(Amatch(v1,bas)), bs1)
| Elazyand (e1,e2) ->
let (r1,bs1) = tr_any e1 in
let (r2,bs2) = tr_any e2 in
begin match r1, bs2, r2 with
| ResVal v1, [], ResVal v2 ->
(ResVal (Alogic (Logic_and, [v1;v2])), bs1)
(* let bs1 in Val(v1 && v2) *)
| _ ->
let (v1,bs1') = val_bindings_of_res_bindings (r1,bs1) in
let t2 = apply_bindings_to_res (r2,bs2) in
(ResTrm(Aif(v1,t2,Aval(Abool false))), bs1')
(* let bs1 in if v1 then t2 else false *)
end
| Elazyor (e1,e2) -> (* in practice, factorized with previous case *)
let (r1,bs1) = tr_any e1 in
let (r2,bs2) = tr_any e2 in
begin match r1, bs2, r2 with
| ResVal v1, [], ResVal v2 ->
(ResVal (Alogic (Logic_or, [v1;v2])), bs1)
(* let bs1 in Val(v1 || v2) *)
| _ ->
let (v1,bs1') = val_bindings_of_res_bindings (r1,bs1) in
let t2 = apply_bindings_to_res (r2,bs2) in
(ResTrm(Aif(v1,Aval(Abool true),t2)), bs1')
(* let bs1 in if v1 then true else t2 *)
end
and tr_anys es =
(* assume here right-to-left evaluation order, as in OCaml;
......@@ -223,3 +284,4 @@ and tr_vals es =
(v::vs, bs @ bs2)
) es ([],[])
......@@ -2648,7 +2648,7 @@ Tactic Notation "xcase_no_intros" :=
Several variants are available:
- [xmatch] investigates all the cases, doing inversions,
and introduceing all aliases as equalities.
and introducing all aliases as equalities.
- [xmatch_no_alias] is like [xmatch], but does not
introduce aliases.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment