Commit 9f6a9955 authored by Mário Pereira's avatar Mário Pereira

OCaml extraction:

proper extraction of named and optional arguments in functions
with polymorphic arguments.
parent 06c4cb7c
......@@ -93,14 +93,13 @@ module Impl
let unsafe_resize (a: t 'a) (n: int63) : unit
requires { 0 <= n <= max_array_length }
writes { a.data, a.size, a.data.elts, a.view }
ensures { n = a.size }
ensures { forall i. 0 <= i < MinMax.min ((old a).size) n ->
Seq.([]) a.view i = Seq.([]) (old a).view i }
= let n_old = A.length a.data in
if n <= a.size then
(* shrink *)
if n < n_old / (of_int 4) then begin (* reallocate into a smaller array *)
if n < n_old / 4 then begin (* reallocate into a smaller array *)
a.data <- A.sub a.data zero n;
a.view <- a.view[.. to_int n] end
else begin
......@@ -109,12 +108,12 @@ module Impl
else begin
(* grow *)
if n > n_old then begin (* reallocate into a larger array *)
let n_div2 = n / of_int 2 in
let n_div2 = n / 2 in
let n' =
if n_div2 >= n_old then
if max_array_length / of_int 2 >= n_div2 then n
if max_array_length / 2 >= n_div2 then n
else max_array_length
else if max_array_length / of_int 2 >= n_old then (of_int 2) * n_old
else if max_array_length / 2 >= n_old then 2 * n_old
else max_array_length in
let a' = A.make n' a.dummy in
A.blit a.data zero a' zero a.size;
......@@ -127,7 +126,6 @@ module Impl
a.size <- n
let resize (a: t 'a) (n: int63) : unit
writes { a.data, a.size, a.data.elts, a.view }
ensures { n = a.size }
ensures { forall i. 0 <= i < MinMax.min ((old a).size) n ->
Seq.([]) a.view i = Seq.([]) (old a).view i }
......@@ -138,7 +136,6 @@ module Impl
(** Array interface *)
let clear (a: t 'a) : unit
writes { a.data.elts, a.size, a.data, a.view }
ensures { a.size = 0 }
= unsafe_resize a zero
......
......@@ -36,7 +36,7 @@ type info = {
info_flat : bool;
info_prec : int list Mid.t;
info_current_ph : string list; (* current path *)
}
}
(* operator precedence, from http://caml.inria.fr/pub/docs/manual-ocaml/expr.html
! ? ~ ... | 1
......@@ -168,7 +168,8 @@ module Print = struct
let print_uident = print_qident ~sanitizer:Strings.capitalize
let print_tv ~use_quote fmt tv =
fprintf fmt (if use_quote then "'%s" else "%s") (id_unique aprinter tv.tv_name)
fprintf fmt (if use_quote then "'%s" else "%s")
(id_unique aprinter tv.tv_name)
let protect_on ?(boxed=false) ?(be=false) b s =
if b
......@@ -194,7 +195,7 @@ module Print = struct
let complex_syntax s =
String.contains s '%' || String.contains s ' ' || String.contains s '('
(** Types *)
let rec print_ty ~use_quote ?(paren=false) info fmt = function
......@@ -222,7 +223,8 @@ module Print = struct
(print_lident info) fmt ts
| [ty] ->
fprintf fmt (protect_on paren "%a@ %a")
(print_ty ~use_quote ~paren:true info) ty (print_lident info) ts
(print_ty ~use_quote ~paren:true info) ty (print_lident info)
ts
| tl ->
fprintf fmt (protect_on paren "(%a)@ %a")
(print_list comma (print_ty ~use_quote ~paren:false info)) tl
......@@ -232,22 +234,52 @@ module Print = struct
fprintf fmt "?%s:(%a:@ %a)" id.id_string (print_lident info) id
(print_ty ~use_quote:false ~paren:false info) ty
let print_vs_opt info fmt id =
fprintf fmt "?%s:%a" id.id_string (print_lident info) id
let print_vsty_named info fmt id ty =
fprintf fmt "~%s:(%a:@ %a)" id.id_string (print_lident info) id
(print_ty ~use_quote:false ~paren:false info) ty
let print_vs_named info fmt id =
fprintf fmt "~%s:%a" id.id_string (print_lident info) id
let print_vsty info fmt (id, ty, _) =
let attrs = id.id_attrs in
if is_optional ~attrs then print_vsty_opt info fmt id ty
else if is_named ~attrs then print_vsty_named info fmt id ty
else fprintf fmt "(%a:@ %a)" (print_lident info) id
(print_ty ~use_quote:false ~paren:false info) ty
(print_ty ~use_quote:false ~paren:false info) ty
let print_vsty_opt_fun info fmt id = function
| Tapp (id_ty, [arg]) ->
assert (query_syntax info.info_syn id_ty = Some "%1 option");
fprintf fmt "?%s:%a" id.id_string
(print_ty ~use_quote:false ~paren:false info) arg
| _ -> invalid_arg "print_vsty_opt_fun" (*FIXME : better error message *)
let print_vsty_named_fun info fmt id ty =
fprintf fmt "%s:%a" id.id_string
(print_ty ~use_quote:false ~paren:false info) ty
let print_vsty_fun info fmt (id, ty, _) =
let attrs = id.id_attrs in
if is_optional ~attrs then print_vsty_opt_fun info fmt id ty
else if is_named ~attrs then print_vsty_named_fun info fmt id ty
else fprintf fmt "%a" (print_ty ~use_quote:false ~paren:true info) ty
let print_vs_fun info fmt id =
let attrs = id.id_attrs in
if is_optional ~attrs then print_vs_opt info fmt id
else if is_named ~attrs then print_vs_named info fmt id
else print_lident info fmt id
let print_tv_arg = print_tv
let print_tv_args ~use_quote fmt = function
| [] -> ()
| [tv] -> fprintf fmt "%a@ " (print_tv_arg ~use_quote) tv
| tvl -> fprintf fmt "(%a)@ " (print_list comma (print_tv_arg ~use_quote)) tvl
| tvl ->
fprintf fmt "(%a)@ " (print_list comma (print_tv_arg ~use_quote)) tvl
let print_vs_arg info fmt vs =
fprintf fmt "@[%a@]" (print_vsty info) vs
......@@ -380,7 +412,8 @@ module Print = struct
| None, tl when is_rs_tuple rs ->
fprintf fmt "@[(%a)@]" (print_list comma (print_expr info 14)) tl
| None, [t1] when isfield ->
fprintf fmt "%a.%a" (print_expr info 2) t1 (print_lident info) rs.rs_name
fprintf fmt "%a.%a" (print_expr info 2) t1 (print_lident info)
rs.rs_name
| None, tl when isconstructor () ->
let pjl = get_record info rs in
begin match pjl, tl with
......@@ -413,16 +446,16 @@ module Print = struct
(print_ty ~use_quote:false info) res
(print_expr ~opr:false info 18) e
else
let ty_args = List.map (fun (_, ty, _) -> ty) args in
let id_args = List.map (fun (id, _, _) -> id) args in
let arrow fmt () = fprintf fmt " ->@ " in
let start fmt () = fprintf fmt "fun@ " in
fprintf fmt ":@ @[<h>type @[%a@]. @[%a@ %a@]@] =@ \
@[<hv 2>@[%a@]%a@]"
print_svar s
(print_list_suf arrow (print_ty ~use_quote:false ~paren:true info)) ty_args
(print_list_suf arrow (print_vsty_fun info)) args
(print_ty ~use_quote:false ~paren:true info) res
(print_list_delim ~start ~stop:arrow ~sep:space (print_lident info)) id_args
(print_list_delim ~start ~stop:arrow ~sep:space (print_vs_fun info))
id_args
(print_expr ~opr:false info 18) e
and print_let_def ?(functor_arg=false) info fmt = function
......
......@@ -239,6 +239,14 @@ module TestExtraction
match x with None -> y | Some x -> x + y end
let constant opt_c = opt_g (Some 40) 2
let opt_f_poly (x [@ocaml:optional]: option 'a) (y: int) : int =
match x with
| None -> y
| Some _ -> 89
end
let call_f_poly (x: 'a) = opt_f_poly (Some x) 42
(* FIXME: partial application with named arguments not yet supported *)
let constant opt_b = fun y -> opt_g y 42
let opt_h () = fun y -> opt_f 40 y
......
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