Commit ef3b2492 authored by charguer's avatar charguer

cp

parent c4743ffc
......@@ -39,6 +39,8 @@ LATER
- make systematic use of || (rm -f $@; exit 1) in cfml calls
DEPRECATED?
- no longer rely on myocamldep
......
......@@ -94,6 +94,10 @@ let let_fun_poly_pair_homogeneous () =
let let_fun_on_the_fly () =
(fun x f -> f x) 3 (fun x -> x+1)
let let_fun_in_let () =
let f = (assert (true); fun x -> x) in
f
(********************************************************************)
(* ** Partial applications *)
......
......@@ -309,6 +309,11 @@ Proof using.
xsimpl~.
Qed.
let let_fun_in_let () =
let f = (assert (true); fun x -> x) in
f
(********************************************************************)
(* ** Let-term *)
......
......@@ -219,12 +219,13 @@ let get_assign_fct loc already_named new_name : expression -> bindings -> expres
let e' = { pexp_loc = loc; pexp_desc = Pexp_ident (Lident x) } in
e', b @ [ p, e ]
(* argument [named] indicates whether the context in which appear
is already a [let x = ... in ..]. This is useful to know whether
it is needed to introduce a fresh name in case the expression [e]
is of the form [fun .. -> ..]. *)
(* argument [is_named] indicates whether the context in which appear
is already a [let x = ... in ..]. If this is the case and we
encounter a function, then we don't need to introduce a fresh name
for it. Otherwise, any occurence of [fun .. -> ..] will be turned
into [let f = fun .. -> .. in f], for a fresh name f. *)
let normalize_expression named e =
let normalize_expression is_named e =
let loc = e.pexp_loc in
let i = ref (-1) in (* TODO: use a gensym function *)
let next_var () =
......@@ -240,8 +241,7 @@ let normalize_expression named e =
let svalue = if bvalue then "true" else "false" in
let explicit_arity = false in (* todo: what does it mean? *)
return (Pexp_construct (Lident svalue, None, explicit_arity)) in
let assign_fct pick_var =
get_assign_fct loc named pick_var in
(* [assign_var e' b] takes a a transformed expression and a list
of bindings; and it returns a transformed expression and a list
of bindings. If the parameter [named] is true, then this returns
......@@ -249,15 +249,17 @@ let normalize_expression named e =
where [b'] extends [b] with the binding from [x] to [e'].
This function should be called any time the translation
produces a term that may not be a value. *)
let assign_var =
assign_fct next_var in
let assign_var e b =
get_assign_fct loc is_named next_var e b in
(* DEPRECATED *)
match e.pexp_desc with
| Pexp_ident li -> return (Pexp_ident li), []
| Pexp_constant c -> return (Pexp_constant c), []
| Pexp_let (Recursive, l, b) ->
| Pexp_let (Recursive, l, eb) ->
let l' = List.map protect_branch l in
let b' = protect true b in
let e' = Pexp_let (Recursive, l', b') in
let eb' = protect true eb in
let e' = Pexp_let (Recursive, l', eb') in
assign_var (return e') []
| Pexp_let (rf, [], e2) -> unsupported loc "let without any binding"
| Pexp_let (rf, [p1,e1], e2) ->
......@@ -288,6 +290,7 @@ let normalize_expression named e =
aux true (List.fold_right (fun (pi,ei) eacc -> create_let loc [pi,ei] eacc) l e)
*)
| Pexp_function (lab, None, [_]) ->
(* function with a single pattern *)
let rec protect_func (ms : (expression * pattern) list) (e : expression) =
match e.pexp_desc with
| Pexp_function (lab, None, [p, e']) ->
......@@ -313,15 +316,15 @@ let normalize_expression named e =
return (Pexp_match (vi, [pi,eacc])) in
List.fold_left addmatch (protect true e) ms
in
let assign = assign_fct next_func in
assign (protect_func [] e) []
get_assign_fct loc is_named next_func (protect_func [] e) []
| Pexp_function (lab, None, l) ->
let x = next_var() in (* todo: factorize next three lines of code *)
(* [function p1 -> e1 | p2 -> e2] encoded as the translation of
[function x_ match x_ with p1 -> e1 | p2 -> e2] *)
let x = next_var() in (* todo: factorize next three lines of code *)
let px = { ppat_loc = Location.none (* hack to pass check-var *); ppat_desc = Ppat_var x } in (* todo: better hack to remember created var *)
let vx = { pexp_loc = Location.none (* hack to pass check-var *); pexp_desc = Pexp_ident (Lident x) } in
let e' = return (Pexp_match (vx, l)) in
aux named (return (Pexp_function (lab, None, [px,e'])))
(* [function /branches/] becomes [fun x => match x with /branches/] *)
| Pexp_function (p, Some _, l) ->
unsupported loc "function with optional expression"
| Pexp_apply (e0, l) when is_failwith_function e0 ->
......@@ -416,14 +419,14 @@ let normalize_expression named e =
assign_var (return (Pexp_ifthenelse (e1', protect named e2, Some (return (Pexp_construct (Lident "()", None, false)))))) b
*)
let e1', b = aux false e1 in
assign_var (return (Pexp_ifthenelse (e1', protect named e2, Some (return (Pexp_construct (Lident "()", None, false)))))) b
assign_var (return (Pexp_ifthenelse (e1', protect false e2, Some (return (Pexp_construct (Lident "()", None, false)))))) b
| Pexp_ifthenelse (e1, e2, Some e3) ->
(* old
let e1', b = aux true e1 in
assign_var (return (Pexp_ifthenelse (e1', protect named e2, Some (protect named e3)))) b
*)
let e1', b = aux false e1 in
assign_var (return (Pexp_ifthenelse (e1', protect named e2, Some (protect named e3)))) b
assign_var (return (Pexp_ifthenelse (e1', protect false e2, Some (protect false e3)))) b
(* todo: tester: if then else fun x -> x *)
| Pexp_sequence (e1,e2) ->
let e1', b = aux true e1 in
......@@ -431,11 +434,11 @@ let normalize_expression named e =
let e1'' = return (Pexp_constraint (e1', tunit, None)) in
assign_var (return (Pexp_sequence (e1'', protect false e2))) b
| Pexp_while (e1,e2) ->
assign_var (return (Pexp_while (protect named e1, protect named e2))) []
assign_var (return (Pexp_while (protect false e1, protect false e2))) []
| Pexp_for (s,e1,e2,d,e3) ->
let e1', b1 = aux false e1 in
let e2', b2 = aux false e2 in
assign_var (return (Pexp_for (s, e1', e2', d, protect named e3))) (b1 @ b2)
assign_var (return (Pexp_for (s, e1', e2', d, protect false e3))) (b1 @ b2)
| Pexp_constraint (e,to1,to2) ->
let e',b = aux named e in
return (Pexp_constraint (e',to1,to2)), b
......
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