Skip to content
Browse files

format+gadts: make format types "relational" to fix %(...%) typing

See the long comment in pervasives.ml for an explanation of the
change. The short summary is that we need to prove more elaborate
properties between the format types involved in the typing of %(...%),
and that proving things by writing GADT functions in OCaml reveals
that Coq's Ltac is a miracle of usability.

Proofs on OCaml GADTs are runtime functions that do have a runtime
semantics: it is legitimate to hope that those proof computations are
as simple as possible, but the current implementation was optimized
for feasability, not simplicity. François Bobot has some interesting
suggestions to simplify the reasoning part (with more equality
reasoning where I used transitivity and symmetry of the
relation profusely), which may make the code simpler in the future
(and possibly more efficient: the hope is that only %(...%) users will
pay a proof-related cost).

git-svn-id: http://caml.inria.fr/svn/ocaml/trunk@14897 f963ae5c-01c2-4b8c-9fe0-0dff7051ff02
  • Loading branch information...
1 parent 34fb0d4 commit e0b000527be1c6e2a93a7b859499378db85b915c @gasche gasche committed May 21, 2014
View
BIN boot/ocamlc
Binary file not shown.
View
BIN boot/ocamldep
Binary file not shown.
View
BIN boot/ocamllex
Binary file not shown.
View
177 otherlibs/threads/pervasives.ml
@@ -646,75 +646,97 @@ type prec_option = int option
(***)
-(* Type used in Format_subst_ty and Format_subst constructors as "a proof"
- of '->' number equality between two ('d, 'e) relations. *)
-(* See the scanf implementation of "%(...%)". *)
-(* Not meaningful for Printf and Format since "%r" is Scanf specific. *)
-type ('d1, 'e1, 'd2, 'e2) reader_nb_unifier =
- | Zero_reader :
- ('d1, 'd1, 'd2, 'd2) reader_nb_unifier
- | Succ_reader :
- ('d1, 'e1, 'd2, 'e2) reader_nb_unifier ->
- ('x -> 'd1, 'e1, 'x -> 'd2, 'e2) reader_nb_unifier
-
-(***)
-
(* List of format type elements. *)
(* In particular used to represent %(...%) and %{...%} contents. *)
type ('a, 'b, 'c, 'd, 'e, 'f) fmtty =
+ ('a, 'b, 'c, 'd, 'e, 'f,
+ 'a, 'b, 'c, 'd, 'e, 'f) fmtty_rel
+and ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel =
| Char_ty : (* %c *)
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (char -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (char -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ char -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
| String_ty : (* %s *)
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (string -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (string -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ string -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
| Int_ty : (* %d *)
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (int -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (int -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ int -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
| Int32_ty : (* %ld *)
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (int32 -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (int32 -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ int32 -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
| Nativeint_ty : (* %nd *)
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (nativeint -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (nativeint -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ nativeint -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
| Int64_ty : (* %Ld *)
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (int64 -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (int64 -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ int64 -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
| Float_ty : (* %f *)
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (float -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (float -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ float -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
| Bool_ty : (* %B *)
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (bool -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (bool -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ bool -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
| Format_arg_ty : (* %{...%} *)
('g, 'h, 'i, 'j, 'k, 'l) fmtty *
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (('g, 'h, 'i, 'j, 'k, 'l) format6 -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (('g, 'h, 'i, 'j, 'k, 'l) format6 -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ ('g, 'h, 'i, 'j, 'k, 'l) format6 -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
| Format_subst_ty : (* %(...%) *)
- ('d1, 'q1, 'd2, 'q2) reader_nb_unifier *
- ('x, 'b, 'c, 'd1, 'q1, 'u) fmtty *
- ('u, 'b, 'c, 'q1, 'e1, 'f) fmtty ->
- (('x, 'b, 'c, 'd2, 'q2, 'u) format6 -> 'x, 'b, 'c, 'd1, 'e1, 'f) fmtty
+ ('g, 'h, 'i, 'j, 'k, 'l,
+ 'g1, 'b1, 'c1, 'j1, 'd1, 'a1) fmtty_rel *
+ ('g, 'h, 'i, 'j, 'k, 'l,
+ 'g2, 'b2, 'c2, 'j2, 'd2, 'a2) fmtty_rel *
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (('g, 'h, 'i, 'j, 'k, 'l) format6 -> 'g1, 'b1, 'c1, 'j1, 'e1, 'f1,
+ ('g, 'h, 'i, 'j, 'k, 'l) format6 -> 'g2, 'b2, 'c2, 'j2, 'e2, 'f2) fmtty_rel
(* Printf and Format specific constructors. *)
| Alpha_ty : (* %a *)
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (('b -> 'x -> 'c) -> 'x -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (('b1 -> 'x -> 'c1) -> 'x -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ ('b2 -> 'x -> 'c2) -> 'x -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
| Theta_ty : (* %t *)
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (('b -> 'c) -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (('b1 -> 'c1) -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ ('b2 -> 'c2) -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
(* Scanf specific constructor. *)
| Reader_ty : (* %r *)
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- ('x -> 'a, 'b, 'c, ('b -> 'x) -> 'd, 'e, 'f) fmtty
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ ('x -> 'a1, 'b1, 'c1, ('b1 -> 'x) -> 'd1, 'e1, 'f1,
+ 'x -> 'a2, 'b2, 'c2, ('b2 -> 'x) -> 'd2, 'e2, 'f2) fmtty_rel
| Ignored_reader_ty : (* %_r *)
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- ('a, 'b, 'c, ('b -> 'x) -> 'd, 'e, 'f) fmtty
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ ('a1, 'b1, 'c1, ('b1 -> 'x) -> 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, ('b2 -> 'x) -> 'd2, 'e2, 'f2) fmtty_rel
| End_of_fmtty :
- ('f, 'b, 'c, 'd, 'd, 'f) fmtty
+ ('f1, 'b1, 'c1, 'd1, 'd1, 'f1,
+ 'f2, 'b2, 'c2, 'd2, 'd2, 'f2) fmtty_rel
(***)
@@ -771,10 +793,11 @@ and ('a, 'b, 'c, 'd, 'e, 'f) fmt =
('a, 'b, 'c, 'd, 'e, 'f) fmt ->
(('g, 'h, 'i, 'j, 'k, 'l) format6 -> 'a, 'b, 'c, 'd, 'e, 'f) fmt
| Format_subst : (* %(...%) *)
- pad_option * ('d1, 'q1, 'd2, 'q2) reader_nb_unifier *
- ('x, 'b, 'c, 'd1, 'q1, 'u) fmtty *
- ('u, 'b, 'c, 'q1, 'e1, 'f) fmt ->
- (('x, 'b, 'c, 'd2, 'q2, 'u) format6 -> 'x, 'b, 'c, 'd1, 'e1, 'f) fmt
+ pad_option *
+ ('g, 'h, 'i, 'j, 'k, 'l,
+ 'g2, 'b, 'c, 'j2, 'd, 'a) fmtty_rel *
+ ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
+ (('g, 'h, 'i, 'j, 'k, 'l) format6 -> 'g2, 'b, 'c, 'j2, 'e, 'f) fmt
(* Printf and Format specific constructor. *)
| Alpha : (* %a *)
@@ -831,7 +854,7 @@ and ('a, 'b, 'c, 'd, 'e, 'f) ignored =
| Ignored_bool : (* %_B *)
('a, 'b, 'c, 'd, 'd, 'a) ignored
| Ignored_format_arg : (* %_{...%} *)
- pad_option * ('x, 'b, 'c, 'y, 'z, 't) fmtty ->
+ pad_option * ('g, 'h, 'i, 'j, 'k, 'l) fmtty ->
('a, 'b, 'c, 'd, 'd, 'a) ignored
| Ignored_format_subst : (* %_(...%) *)
pad_option * ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
@@ -846,6 +869,40 @@ and ('a, 'b, 'c, 'd, 'e, 'f) ignored =
and ('a, 'b, 'c, 'd, 'e, 'f) format6 =
Format of ('a, 'b, 'c, 'd, 'e, 'f) fmt * string
+let rec erase_rel : type a b c d e f g h i j k l .
+ (a, b, c, d, e, f,
+ g, h, i, j, k, l) fmtty_rel -> (a, b, c, d, e, f) fmtty
+= function
+ | Char_ty rest ->
+ Char_ty (erase_rel rest)
+ | String_ty rest ->
+ String_ty (erase_rel rest)
+ | Int_ty rest ->
+ Int_ty (erase_rel rest)
+ | Int32_ty rest ->
+ Int32_ty (erase_rel rest)
+ | Int64_ty rest ->
+ Int64_ty (erase_rel rest)
+ | Nativeint_ty rest ->
+ Nativeint_ty (erase_rel rest)
+ | Float_ty rest ->
+ Float_ty (erase_rel rest)
+ | Bool_ty rest ->
+ Bool_ty (erase_rel rest)
+ | Format_arg_ty (ty, rest) ->
+ Format_arg_ty (ty, erase_rel rest)
+ | Format_subst_ty (ty1, ty2, rest) ->
+ Format_subst_ty (ty1, ty1, erase_rel rest)
+ | Alpha_ty rest ->
+ Alpha_ty (erase_rel rest)
+ | Theta_ty rest ->
+ Theta_ty (erase_rel rest)
+ | Reader_ty rest ->
+ Reader_ty (erase_rel rest)
+ | Ignored_reader_ty rest ->
+ Ignored_reader_ty (erase_rel rest)
+ | End_of_fmtty -> End_of_fmtty
+
(******************************************************************************)
(* Format type concatenation *)
@@ -854,10 +911,24 @@ and ('a, 'b, 'c, 'd, 'e, 'f) format6 =
* reader_nb_unifier_of_fmtty to count readers in an fmtty,
* Scanf.take_fmtty_format_readers to extract readers inside %(...%),
* CamlinternalFormat.fmtty_of_ignored_format to extract format type. *)
+
+(*
let rec concat_fmtty : type a b c d e f g h .
(a, b, c, d, e, f) fmtty ->
(f, b, c, e, g, h) fmtty ->
(a, b, c, d, g, h) fmtty =
+*)
+let rec concat_fmtty :
+ type a1 b1 c1 d1 e1 f1
+ a2 b2 c2 d2 e2 f2
+ g1 j1 g2 j2
+ .
+ (g1, b1, c1, j1, d1, a1,
+ g2, b2, c2, j2, d2, a2) fmtty_rel ->
+ (a1, b1, c1, d1, e1, f1,
+ a2, b2, c2, d2, e2, f2) fmtty_rel ->
+ (g1, b1, c1, j1, e1, f1,
+ g2, b2, c2, j2, e2, f2) fmtty_rel =
fun fmtty1 fmtty2 -> match fmtty1 with
| Char_ty rest ->
Char_ty (concat_fmtty rest fmtty2)
@@ -885,8 +956,8 @@ fun fmtty1 fmtty2 -> match fmtty1 with
Ignored_reader_ty (concat_fmtty rest fmtty2)
| Format_arg_ty (ty, rest) ->
Format_arg_ty (ty, concat_fmtty rest fmtty2)
- | Format_subst_ty (rnu, ty, rest) ->
- Format_subst_ty (rnu, ty, concat_fmtty rest fmtty2)
+ | Format_subst_ty (ty1, ty2, rest) ->
+ Format_subst_ty (ty1, ty2, concat_fmtty rest fmtty2)
| End_of_fmtty -> fmtty2
(******************************************************************************)
@@ -936,8 +1007,8 @@ fun fmt1 fmt2 -> match fmt1 with
| Format_arg (pad, fmtty, rest) ->
Format_arg (pad, fmtty, concat_fmt rest fmt2)
- | Format_subst (pad, rnu, fmtty, rest) ->
- Format_subst (pad, rnu, fmtty, concat_fmt rest fmt2)
+ | Format_subst (pad, fmtty, rest) ->
+ Format_subst (pad, fmtty, concat_fmt rest fmt2)
| Scan_char_set (width_opt, char_set, rest) ->
Scan_char_set (width_opt, char_set, concat_fmt rest fmt2)
View
337 stdlib/camlinternalFormat.ml
@@ -47,30 +47,6 @@ let is_in_char_set char_set c =
let str_ind = ind lsr 3 and mask = 1 lsl (ind land 0b111) in
(int_of_char (String.get char_set str_ind) land mask) <> 0
-(******************************************************************************)
- (* Reader count *)
-
-(* Count the number of "%r" (Reader_ty) and "%_r" (Ignored_reader_ty)
- in an fmtty. *)
-let rec reader_nb_unifier_of_fmtty : type a b c d e f .
- (a, b, c, d, e, f) fmtty -> (d, e, d, e) reader_nb_unifier =
-fun fmtty -> match fmtty with
- | Char_ty rest -> reader_nb_unifier_of_fmtty rest
- | String_ty rest -> reader_nb_unifier_of_fmtty rest
- | Int_ty rest -> reader_nb_unifier_of_fmtty rest
- | Int32_ty rest -> reader_nb_unifier_of_fmtty rest
- | Nativeint_ty rest -> reader_nb_unifier_of_fmtty rest
- | Int64_ty rest -> reader_nb_unifier_of_fmtty rest
- | Float_ty rest -> reader_nb_unifier_of_fmtty rest
- | Bool_ty rest -> reader_nb_unifier_of_fmtty rest
- | Alpha_ty rest -> reader_nb_unifier_of_fmtty rest
- | Theta_ty rest -> reader_nb_unifier_of_fmtty rest
- | Reader_ty rest -> Succ_reader (reader_nb_unifier_of_fmtty rest)
- | Ignored_reader_ty rest -> Succ_reader (reader_nb_unifier_of_fmtty rest)
- | Format_arg_ty (_, rest) -> reader_nb_unifier_of_fmtty rest
- | Format_subst_ty(_,sub_fmtty,rest) ->
- reader_nb_unifier_of_fmtty (concat_fmtty sub_fmtty rest)
- | End_of_fmtty -> Zero_reader
(******************************************************************************)
(* Ignored param conversion *)
@@ -125,7 +101,7 @@ fun ign fmt -> match ign with
Param_format_EBB (Format_arg (pad_opt, fmtty, fmt))
| Ignored_format_subst (pad_opt, fmtty) ->
Param_format_EBB
- (Format_subst (pad_opt, reader_nb_unifier_of_fmtty fmtty, fmtty, fmt))
+ (Format_subst (pad_opt, fmtty, fmt))
| Ignored_reader ->
Param_format_EBB (Reader fmt)
| Ignored_scan_char_set (width_opt, char_set) ->
@@ -478,8 +454,8 @@ let bprint_string_literal buf str =
(* Format pretty-printing *)
(* Print a complete format type (an fmtty) in a buffer. *)
-let rec bprint_fmtty : type a b c d e f .
- buffer -> (a, b, c, d, e, f) fmtty -> unit =
+let rec bprint_fmtty : type a b c d e f g h i j k l .
+ buffer -> (a, b, c, d, e, f, g, h, i, j, k, l) fmtty_rel -> unit =
fun buf fmtty -> match fmtty with
| Char_ty rest -> buffer_add_string buf "%c"; bprint_fmtty buf rest;
| String_ty rest -> buffer_add_string buf "%s"; bprint_fmtty buf rest;
@@ -500,7 +476,7 @@ fun buf fmtty -> match fmtty with
| Format_arg_ty (sub_fmtty, rest) ->
buffer_add_string buf "%{"; bprint_fmtty buf sub_fmtty;
buffer_add_string buf "%}"; bprint_fmtty buf rest;
- | Format_subst_ty (_, sub_fmtty, rest) ->
+ | Format_subst_ty (sub_fmtty, _, rest) ->
buffer_add_string buf "%("; bprint_fmtty buf sub_fmtty;
buffer_add_string buf "%)"; bprint_fmtty buf rest;
@@ -572,7 +548,7 @@ let bprint_fmt buf fmt =
bprint_pad_opt buf pad_opt; buffer_add_char buf '{';
bprint_fmtty buf fmtty; buffer_add_char buf '%'; buffer_add_char buf '}';
fmtiter rest false;
- | Format_subst (pad_opt, _, fmtty, rest) ->
+ | Format_subst (pad_opt, fmtty, rest) ->
buffer_add_char buf '%'; bprint_ignored_flag buf ign_flag;
bprint_pad_opt buf pad_opt; buffer_add_char buf '(';
bprint_fmtty buf fmtty; buffer_add_char buf '%'; buffer_add_char buf ')';
@@ -609,6 +585,199 @@ let string_of_fmt fmt =
(******************************************************************************)
(* Type extraction *)
+type (_, _) eq = Refl : ('a, 'a) eq
+
+(* Invariant: this function is the identity on values.
+
+ In particular, if (ty1, ty2) have equal values, then
+ (trans (symm ty1) ty2) respects the 'trans' precondition. *)
+let rec symm : type a1 b1 c1 d1 e1 f1 a2 b2 c2 d2 e2 f2 .
+ (a1, b1, c1, d1, e1, f1,
+ a2, b2, c2, d2, e2, f2) fmtty_rel
+-> (a2, b2, c2, d2, e2, f2,
+ a1, b1, c1, d1, e1, f1) fmtty_rel
+= function
+ | Char_ty rest -> Char_ty (symm rest)
+ | Int_ty rest -> Int_ty (symm rest)
+ | Int32_ty rest -> Int32_ty (symm rest)
+ | Int64_ty rest -> Int64_ty (symm rest)
+ | Nativeint_ty rest -> Nativeint_ty (symm rest)
+ | Float_ty rest -> Float_ty (symm rest)
+ | Bool_ty rest -> Bool_ty (symm rest)
+ | String_ty rest -> String_ty (symm rest)
+ | Theta_ty rest -> Theta_ty (symm rest)
+ | Alpha_ty rest -> Alpha_ty (symm rest)
+ | Reader_ty rest -> Reader_ty (symm rest)
+ | Ignored_reader_ty rest -> Ignored_reader_ty (symm rest)
+ | Format_arg_ty (ty, rest) ->
+ Format_arg_ty (ty, symm rest)
+ | Format_subst_ty (ty1, ty2, rest) ->
+ Format_subst_ty (ty2, ty1, symm rest)
+ | End_of_fmtty -> End_of_fmtty
+
+let rec fmtty_rel_det : type a1 b c d1 e1 f1 a2 d2 e2 f2 .
+ (a1, b, c, d1, e1, f1,
+ a2, b, c, d2, e2, f2) fmtty_rel ->
+ ((f1, f2) eq -> (a1, a2) eq)
+ * ((a1, a2) eq -> (f1, f2) eq)
+ * ((e1, e2) eq -> (d1, d2) eq)
+ * ((d1, d2) eq -> (e1, e2) eq)
+= function
+ | End_of_fmtty ->
+ (fun Refl -> Refl),
+ (fun Refl -> Refl),
+ (fun Refl -> Refl),
+ (fun Refl -> Refl)
+ | Char_ty rest ->
+ let fa, af, ed, de = fmtty_rel_det rest in
+ (fun Refl -> let Refl = fa Refl in Refl),
+ (fun Refl -> let Refl = af Refl in Refl),
+ ed, de
+ | String_ty rest ->
+ let fa, af, ed, de = fmtty_rel_det rest in
+ (fun Refl -> let Refl = fa Refl in Refl),
+ (fun Refl -> let Refl = af Refl in Refl),
+ ed, de
+ | Int_ty rest ->
+ let fa, af, ed, de = fmtty_rel_det rest in
+ (fun Refl -> let Refl = fa Refl in Refl),
+ (fun Refl -> let Refl = af Refl in Refl),
+ ed, de
+ | Int32_ty rest ->
+ let fa, af, ed, de = fmtty_rel_det rest in
+ (fun Refl -> let Refl = fa Refl in Refl),
+ (fun Refl -> let Refl = af Refl in Refl),
+ ed, de
+ | Int64_ty rest ->
+ let fa, af, ed, de = fmtty_rel_det rest in
+ (fun Refl -> let Refl = fa Refl in Refl),
+ (fun Refl -> let Refl = af Refl in Refl),
+ ed, de
+ | Nativeint_ty rest ->
+ let fa, af, ed, de = fmtty_rel_det rest in
+ (fun Refl -> let Refl = fa Refl in Refl),
+ (fun Refl -> let Refl = af Refl in Refl),
+ ed, de
+ | Float_ty rest ->
+ let fa, af, ed, de = fmtty_rel_det rest in
+ (fun Refl -> let Refl = fa Refl in Refl),
+ (fun Refl -> let Refl = af Refl in Refl),
+ ed, de
+ | Bool_ty rest ->
+ let fa, af, ed, de = fmtty_rel_det rest in
+ (fun Refl -> let Refl = fa Refl in Refl),
+ (fun Refl -> let Refl = af Refl in Refl),
+ ed, de
+
+ | Theta_ty rest ->
+ let fa, af, ed, de = fmtty_rel_det rest in
+ (fun Refl -> let Refl = fa Refl in Refl),
+ (fun Refl -> let Refl = af Refl in Refl),
+ ed, de
+ | Alpha_ty rest ->
+ let fa, af, ed, de = fmtty_rel_det rest in
+ (fun Refl -> let Refl = fa Refl in Refl),
+ (fun Refl -> let Refl = af Refl in Refl),
+ ed, de
+ | Reader_ty rest ->
+ let fa, af, ed, de = fmtty_rel_det rest in
+ (fun Refl -> let Refl = fa Refl in Refl),
+ (fun Refl -> let Refl = af Refl in Refl),
+ (fun Refl -> let Refl = ed Refl in Refl),
+ (fun Refl -> let Refl = de Refl in Refl)
+ | Ignored_reader_ty rest ->
+ let fa, af, ed, de = fmtty_rel_det rest in
+ (fun Refl -> let Refl = fa Refl in Refl),
+ (fun Refl -> let Refl = af Refl in Refl),
+ (fun Refl -> let Refl = ed Refl in Refl),
+ (fun Refl -> let Refl = de Refl in Refl)
+ | Format_arg_ty (_ty, rest) ->
+ let fa, af, ed, de = fmtty_rel_det rest in
+ (fun Refl -> let Refl = fa Refl in Refl),
+ (fun Refl -> let Refl = af Refl in Refl),
+ ed, de
+ | Format_subst_ty (ty1, ty2, rest) ->
+ let fa, af, ed, de = fmtty_rel_det rest in
+ let ty = trans (symm ty1) ty2 in
+ let ag, ga, dj, jd = fmtty_rel_det ty in
+ (fun Refl -> let Refl = fa Refl in let Refl = ag Refl in Refl),
+ (fun Refl -> let Refl = ga Refl in let Refl = af Refl in Refl),
+ (fun Refl -> let Refl = ed Refl in let Refl = dj Refl in Refl),
+ (fun Refl -> let Refl = jd Refl in let Refl = de Refl in Refl)
+
+(* Precondition: we assume that the two fmtty_rel arguments have equal
+ values (at possibly distinct types); this invariant comes from the way
+ fmtty_rel witnesses are produced by the type-checker
+
+ The code below uses (assert false) when this assumption is broken. The
+ code pattern is the following:
+
+ | Foo x, Foo y ->
+ (* case where indeed both values
+ start with constructor Foo *)
+ | Foo _, _
+ | _, Foo _ ->
+ (* different head constructors: broken precondition *)
+ assert false
+*)
+and trans : type
+ a1 b1 c1 d1 e1 f1
+ a2 b2 c2 d2 e2 f2
+ a3 b3 c3 d3 e3 f3
+.
+ (a1, b1, c1, d1, e1, f1,
+ a2, b2, c2, d2, e2, f2) fmtty_rel
+-> (a2, b2, c2, d2, e2, f2,
+ a3, b3, c3, d3, e3, f3) fmtty_rel
+-> (a1, b1, c1, d1, e1, f1,
+ a3, b3, c3, d3, e3, f3) fmtty_rel
+= fun ty1 ty2 -> match ty1, ty2 with
+ | Char_ty rest1, Char_ty rest2 -> Char_ty (trans rest1 rest2)
+ | String_ty rest1, String_ty rest2 -> String_ty (trans rest1 rest2)
+ | Bool_ty rest1, Bool_ty rest2 -> Bool_ty (trans rest1 rest2)
+ | Int_ty rest1, Int_ty rest2 -> Int_ty (trans rest1 rest2)
+ | Int32_ty rest1, Int32_ty rest2 -> Int32_ty (trans rest1 rest2)
+ | Int64_ty rest1, Int64_ty rest2 -> Int64_ty (trans rest1 rest2)
+ | Nativeint_ty rest1, Nativeint_ty rest2 -> Nativeint_ty (trans rest1 rest2)
+ | Float_ty rest1, Float_ty rest2 -> Float_ty (trans rest1 rest2)
+
+ | Alpha_ty rest1, Alpha_ty rest2 -> Alpha_ty (trans rest1 rest2)
+ | Alpha_ty _, _ -> assert false
+ | _, Alpha_ty _ -> assert false
+
+ | Theta_ty rest1, Theta_ty rest2 -> Theta_ty (trans rest1 rest2)
+ | Theta_ty _, _ -> assert false
+ | _, Theta_ty _ -> assert false
+
+ | Reader_ty rest1, Reader_ty rest2 -> Reader_ty (trans rest1 rest2)
+ | Reader_ty _, _ -> assert false
+ | _, Reader_ty _ -> assert false
+
+ | Ignored_reader_ty rest1, Ignored_reader_ty rest2 ->
+ Ignored_reader_ty (trans rest1 rest2)
+ | Ignored_reader_ty _, _ -> assert false
+ | _, Ignored_reader_ty _ -> assert false
+
+ | Format_arg_ty (ty1, rest1), Format_arg_ty (ty2, rest2) ->
+ Format_arg_ty (trans ty1 ty2, trans rest1 rest2)
+ | Format_arg_ty _, _ -> assert false
+ | _, Format_arg_ty _ -> assert false
+
+ | Format_subst_ty (ty11, ty12, rest1),
+ Format_subst_ty (ty21, ty22, rest2) ->
+ let ty = trans (symm ty12) ty21 in
+ let _, f2, _, f4 = fmtty_rel_det ty in
+ let Refl = f2 Refl in
+ let Refl = f4 Refl in
+ Format_subst_ty (ty11, ty22, trans rest1 rest2)
+ | Format_subst_ty _, _ -> assert false
+ | _, Format_subst_ty _ -> assert false
+
+ | End_of_fmtty, End_of_fmtty -> End_of_fmtty
+ | End_of_fmtty, _ -> assert false
+ | _, End_of_fmtty -> assert false
+
+
(* Extract the type representation (an fmtty) of a format. *)
let rec fmtty_of_fmt : type a b c d e f .
(a, b, c, d, e, f) CamlinternalFormatBasics.fmt -> (a, b, c, d, e, f) fmtty =
@@ -648,8 +817,8 @@ fun fmtty -> match fmtty with
| Format_arg (_, ty, rest) ->
Format_arg_ty (ty, fmtty_of_fmt rest)
- | Format_subst (_, rnu, ty, rest) ->
- Format_subst_ty (rnu, ty, fmtty_of_fmt rest)
+ | Format_subst (_, ty, rest) ->
+ Format_subst_ty (ty, ty, fmtty_of_fmt rest)
| Flush rest -> fmtty_of_fmt rest
| String_literal (_, rest) -> fmtty_of_fmt rest
@@ -704,7 +873,7 @@ and fmtty_of_precision_fmtty : type x a b c d e f .
(******************************************************************************)
(* Format typing *)
-(* Exception raised by type_XXX when a typing error occurs. *)
+(* Exception raised when a format does not match a given format type. *)
exception Type_mismatch
(* Type a padding. *)
@@ -738,11 +907,14 @@ fun pad prec fmtty -> match prec, type_padding pad fmtty with
(* If typing succeed, generate a copy of the format with the same
type parameters as the fmtty. *)
(* Raise a Failure with an error message in case of type mismatch. *)
-let rec type_format : type x t u v a b c d e f .
- (x, b, c, t, u, v) CamlinternalFormatBasics.fmt ->
- (a, b, c, d, e, f) fmtty ->
- (a, b, c, d, e, f) CamlinternalFormatBasics.fmt =
-fun fmt fmtty -> match fmt, fmtty with
+
+let rec type_format :
+ type a1 b1 c1 d1 e1 f1
+ a2 b2 c2 d2 e2 f2 .
+ (a1, b1, c1, d1, e1, f1) fmt
+ -> (a2, b2, c2, d2, e2, f2) fmtty
+ -> (a2, b2, c2, d2, e2, f2) fmt
+= fun fmt fmtty -> match fmt, fmtty with
| Char fmt_rest, Char_ty fmtty_rest ->
Char (type_format fmt_rest fmtty_rest)
| Caml_char fmt_rest, Char_ty fmtty_rest ->
@@ -803,11 +975,11 @@ fun fmt fmtty -> match fmt, fmtty with
Format_arg_ty (sub_fmtty', fmtty_rest) ->
if Fmtty_EBB sub_fmtty <> Fmtty_EBB sub_fmtty' then raise Type_mismatch;
Format_arg (pad_opt, sub_fmtty', type_format fmt_rest fmtty_rest)
- | Format_subst (pad_opt, _, sub_fmtty, fmt_rest),
- Format_subst_ty (rnu', sub_fmtty', fmtty_rest) ->
- if Fmtty_EBB sub_fmtty <> Fmtty_EBB sub_fmtty' then raise Type_mismatch;
- Format_subst (pad_opt, rnu', sub_fmtty', type_format fmt_rest fmtty_rest)
-
+ | Format_subst (pad_opt, sub_fmtty, fmt_rest),
+ Format_subst_ty (sub_fmtty1, _sub_fmtty2, fmtty_rest) ->
+ if Fmtty_EBB (erase_rel sub_fmtty) <> Fmtty_EBB (erase_rel sub_fmtty1) then
+ raise Type_mismatch;
+ Format_subst (pad_opt, sub_fmtty1, type_format fmt_rest (erase_rel fmtty_rest))
(* Printf and Format specific constructors: *)
| Alpha fmt_rest, Alpha_ty fmtty_rest ->
Alpha (type_format fmt_rest fmtty_rest)
@@ -833,10 +1005,10 @@ fun fmt fmtty -> match fmt, fmtty with
| _ -> raise Type_mismatch
-(* Type and Ignored_param node according to an fmtty. *)
-and type_ignored_param : type p q x t u v a b c d e f .
- (x, b, c, t, q, p) ignored ->
- (p, b, c, q, u, v) CamlinternalFormatBasics.fmt ->
+(* Type an Ignored_param node according to an fmtty. *)
+and type_ignored_param : type p q x y z t u v a b c d e f .
+ (x, y, z, t, q, p) ignored ->
+ (p, y, z, q, u, v) CamlinternalFormatBasics.fmt ->
(a, b, c, d, e, f) fmtty ->
(a, b, c, d, e, f) CamlinternalFormatBasics.fmt =
fun ign fmt fmtty -> match ign with
@@ -857,7 +1029,7 @@ fun ign fmt fmtty -> match ign with
| Ignored_format_subst (pad_opt, sub_fmtty) ->
let Fmtty_fmt_EBB (sub_fmtty', fmt') =
type_ignored_format_substitution sub_fmtty fmt fmtty in
- Ignored_param (Ignored_format_subst (pad_opt, sub_fmtty'), fmt')
+ Ignored_param (Ignored_format_subst (pad_opt, erase_rel (symm sub_fmtty')), fmt')
| Ignored_reader ->
begin match fmtty with
| Ignored_reader_ty fmtty_rest ->
@@ -868,9 +1040,9 @@ fun ign fmt fmtty -> match ign with
Ignored_param (ign', type_format fmt fmtty)
(* Typing of the complex case: "%_(...%)". *)
-and type_ignored_format_substitution : type w z p s t u a b c d e f .
- (w, b, c, z, s, p) fmtty ->
- (p, b, c, s, t, u) CamlinternalFormatBasics.fmt ->
+and type_ignored_format_substitution : type w x y z p s t u a b c d e f .
+ (w, x, y, z, s, p) fmtty ->
+ (p, x, y, s, t, u) CamlinternalFormatBasics.fmt ->
(a, b, c, d, e, f) fmtty -> (a, b, c, d, e, f) fmtty_fmt_ebb =
fun sub_fmtty fmt fmtty -> match sub_fmtty, fmtty with
| Char_ty sub_fmtty_rest, Char_ty fmtty_rest ->
@@ -928,18 +1100,59 @@ fun sub_fmtty fmt fmtty -> match sub_fmtty, fmtty with
let Fmtty_fmt_EBB (sub_fmtty_rest', fmt') =
type_ignored_format_substitution sub_fmtty_rest fmt fmtty_rest in
Fmtty_fmt_EBB (Format_arg_ty (sub2_fmtty', sub_fmtty_rest'), fmt')
- | Format_subst_ty (_, sub2_fmtty, sub_fmtty_rest),
- Format_subst_ty (rnu', sub2_fmtty', fmtty_rest) ->
- if Fmtty_EBB sub2_fmtty <> Fmtty_EBB sub2_fmtty' then raise Type_mismatch;
+ | Format_subst_ty (sub1_fmtty, sub2_fmtty, sub_fmtty_rest),
+ Format_subst_ty (sub1_fmtty', sub2_fmtty', fmtty_rest) ->
+ (* TODO define Fmtty_rel_EBB to remove those erase_rel *)
+ if Fmtty_EBB (erase_rel sub1_fmtty) <> Fmtty_EBB (erase_rel sub1_fmtty') then raise Type_mismatch;
+ if Fmtty_EBB (erase_rel sub2_fmtty) <> Fmtty_EBB (erase_rel sub2_fmtty') then raise Type_mismatch;
+ let sub_fmtty' = trans (symm sub1_fmtty') sub2_fmtty' in
+ let _, f2, _, f4 = fmtty_rel_det sub_fmtty' in
+ let Refl = f2 Refl in
+ let Refl = f4 Refl in
let Fmtty_fmt_EBB (sub_fmtty_rest', fmt') =
- type_ignored_format_substitution sub_fmtty_rest fmt fmtty_rest in
- Fmtty_fmt_EBB (Format_subst_ty (rnu', sub2_fmtty', sub_fmtty_rest'),fmt')
-
+ type_ignored_format_substitution (erase_rel sub_fmtty_rest) fmt fmtty_rest in
+ Fmtty_fmt_EBB (Format_subst_ty (sub1_fmtty', sub2_fmtty', symm sub_fmtty_rest'), fmt')
| End_of_fmtty, fmtty ->
Fmtty_fmt_EBB (End_of_fmtty, type_format fmt fmtty)
| _ -> raise Type_mismatch
+
+(* This implementation of `recast` is a bit disappointing. The
+ invariant provided by the type are very strong: the input format's
+ type is in relation to the output type's as witnessed by the
+ fmtty_rel argument. One would at first expect this function to be
+ total, and implementable by exhaustive pattern matching. Instead,
+ we reuse the highly partial and much less well-defined function
+ `type_format` that has lost all knowledge of the correspondence
+ between the argument's types.
+
+ Besides the fact that this function reuses a lot of the
+ `type_format` logic (eg.: seeing Int_ty in the fmtty parameter does
+ not let you match on Int only, as you may in fact have Float
+ (Arg_padding, ...) ("%.*d") beginning with an Int_ty), it is also
+ a partial function, because the typing information in a format is
+ not quite enough to reconstruct it unambiguously. For example, the
+ format types of "%d%_r" and "%_r%d" have the same format6
+ parameters, but they are not at all exchangeable, and putting one
+ in place of the other must result in a dynamic failure.
+
+ Given that:
+ - we'd have to duplicate a lot of non-trivial typing logic from type_format
+ - this wouldn't even eliminate (all) the dynamic failures
+ we decided to just reuse type_format directly for now.
+*)
+let recast :
+ type a1 b1 c1 d1 e1 f1
+ a2 b2 c2 d2 e2 f2
+ .
+ (a1, b1, c1, d1, e1, f1) fmt
+ -> (a1, b1, c1, d1, e1, f1,
+ a2, b2, c2, d2, e2, f2) fmtty_rel
+ -> (a2, b2, c2, d2, e2, f2) fmt
+= fun fmt fmtty ->
+ type_format fmt (erase_rel (symm fmtty))
+
(******************************************************************************)
(* Printing tools *)
@@ -1117,10 +1330,9 @@ fun k o acc fmt -> match fmt with
(fun str ->
ignore str;
make_printf k o (Acc_string (acc, ty)) rest)
- | Format_subst (_, _, fmtty, rest) ->
- (* Call to type_format can't fail (raise Type_mismatch). *)
+ | Format_subst (_, fmtty, rest) ->
fun (Format (fmt, _)) -> make_printf k o acc
- (concat_fmt (type_format fmt fmtty) rest)
+ (concat_fmt (recast fmt fmtty) rest)
| Scan_char_set (_, _, rest) ->
let new_acc = Acc_invalid_arg (acc, "Printf: bad conversion %[") in
@@ -1185,7 +1397,8 @@ fun k o acc fmtty fmt -> match fmtty with
| Ignored_reader_ty _ -> assert false
| Format_arg_ty (_, rest) -> fun _ -> make_from_fmtty k o acc rest fmt
| End_of_fmtty -> make_invalid_arg k o acc fmt
- | Format_subst_ty (_, ty, rest) ->
+ | Format_subst_ty (ty1, ty2, rest) ->
+ let ty = trans (symm ty1) ty2 in
fun _ -> make_from_fmtty k o acc (concat_fmtty ty rest) fmt
(* Insert an Acc_invalid_arg in the accumulator and continue to generate
@@ -1792,8 +2005,8 @@ let fmt_ebb_of_string str =
Fmt_EBB (Ignored_param (ignored, fmt_rest))
else
Fmt_EBB (Format_subst (get_pad_opt '(',
- reader_nb_unifier_of_fmtty sub_fmtty,
- sub_fmtty, fmt_rest))
+ sub_fmtty,
+ fmt_rest))
| '[' ->
let next_ind, char_set = parse_char_set str_ind end_ind in
let Fmt_EBB fmt_rest = parse next_ind end_ind in
View
23 stdlib/camlinternalFormat.mli
@@ -10,9 +10,6 @@ val create_char_set : unit -> mutable_char_set
val add_in_char_set : mutable_char_set -> char -> unit
val freeze_char_set : mutable_char_set -> char_set
-val reader_nb_unifier_of_fmtty :
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty -> ('d, 'e, 'd, 'e) reader_nb_unifier
-
type ('a, 'b, 'c, 'd, 'e, 'f) param_format_ebb = Param_format_EBB :
('x -> 'a, 'b, 'c, 'd, 'e, 'f) fmt ->
('a, 'b, 'c, 'd, 'e, 'f) param_format_ebb
@@ -70,3 +67,23 @@ val string_of_fmtty :
('a, 'b, 'c, 'd, 'e, 'f) CamlinternalFormatBasics.fmtty -> string
val string_of_fmt :
('a, 'b, 'c, 'd, 'e, 'f) CamlinternalFormatBasics.fmt -> string
+
+val symm :
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
+-> ('a2, 'b2, 'c2, 'd2, 'e2, 'f2,
+ 'a1, 'b1, 'c1, 'd1, 'e1, 'f1) fmtty_rel
+
+val trans :
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
+-> ('a2, 'b2, 'c2, 'd2, 'e2, 'f2,
+ 'a3, 'b3, 'c3, 'd3, 'e3, 'f3) fmtty_rel
+-> ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a3, 'b3, 'c3, 'd3, 'e3, 'f3) fmtty_rel
+
+val recast :
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1) fmt
+-> ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
+-> ('a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmt
View
304 stdlib/pervasives.ml
@@ -548,75 +548,226 @@ type prec_option = int option
(***)
-(* Type used in Format_subst_ty and Format_subst constructors as "a proof"
- of '->' number equality between two ('d, 'e) relations. *)
-(* See the scanf implementation of "%(...%)". *)
-(* Not meaningful for Printf and Format since "%r" is Scanf specific. *)
-type ('d1, 'e1, 'd2, 'e2) reader_nb_unifier =
- | Zero_reader :
- ('d1, 'd1, 'd2, 'd2) reader_nb_unifier
- | Succ_reader :
- ('d1, 'e1, 'd2, 'e2) reader_nb_unifier ->
- ('x -> 'd1, 'e1, 'x -> 'd2, 'e2) reader_nb_unifier
-
-(***)
+(* Relational format types
+
+In the first format+gadts implementation, the type for %(..%) in the
+fmt GADT was as follows:
+
+| Format_subst : (* %(...%) *)
+ pad_option * ('d1, 'q1, 'd2, 'q2) reader_nb_unifier *
+ ('x, 'b, 'c, 'd1, 'q1, 'u) fmtty *
+ ('u, 'b, 'c, 'q1, 'e1, 'f) fmt ->
+ (('x, 'b, 'c, 'd2, 'q2, 'u) format6 -> 'x, 'b, 'c, 'd1, 'e1, 'f) fmt
+
+Notice that the 'u parameter in 'f position in the format argument
+(('x, .., 'u) format6 -> ..) is equal to the 'u parameter in 'a
+position in the format tail (('u, .., 'f) fmt). This means that the
+type of the expected format parameter depends of where the %(...%)
+are in the format string:
+
+ # Printf.printf "%(%)";;
+ - : (unit, out_channel, unit, '_a, '_a, unit)
+ CamlinternalFormatBasics.format6 -> unit
+ = <fun>
+ # Printf.printf "%(%)%d";;
+ - : (int -> unit, out_channel, unit, '_a, '_a, int -> unit)
+ CamlinternalFormatBasics.format6 -> int -> unit
+ = <fun>
+
+On the contrary, the legacy typer gives a clever type that does not
+depend on the position of %(..%) in the format string. For example,
+%(%) will have the polymorphic type ('a, 'b, 'c, 'd, 'd, 'a): it can
+be concatenated to any format type, and only enforces the constraint
+that its 'a and 'f parameters are equal (no format arguments) and 'd
+and 'e are equal (no reader argument).
+
+The weakening of this parameter type in the GADT version broke user
+code (in fact it essentially made %(...%) unusable except at the last
+position of a format). In particular, the following would not work
+anymore:
+
+ fun sep ->
+ Format.printf "foo%(%)bar%(%)baz" sep sep
+
+As the type-checker would require two *incompatible* types for the %(%)
+in different positions.
+
+The solution to regain a general type for %(..%) is to generalize this
+technique, not only on the 'd, 'e parameters, but on all six
+parameters of a format: we introduce a "relational" type
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
+whose values are proofs that ('a1, .., 'f1) and ('a2, .., 'f2) morally
+correspond to the same format type: 'a1 is obtained from 'f1,'b1,'c1
+in the exact same way that 'a2 is obtained from 'f2,'b2,'c2, etc.
+
+For example, the relation between two format types beginning with a Char
+parameter is as follows:
+
+| Char_ty : (* %c *)
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (char -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ char -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
+
+In the general case, the term structure of fmtty_rel is (almost¹)
+isomorphic to the fmtty of the previous implementation: every
+constructor is re-read with a binary, relational type, instead of the
+previous unary typing. fmtty can then be re-defined as the diagonal of
+fmtty_rel:
+
+ type ('a, 'b, 'c, 'd, 'e, 'f) fmtty =
+ ('a, 'b, 'c, 'd, 'e, 'f,
+ 'a, 'b, 'c, 'd, 'e, 'f) fmtty_rel
+
+Once we have this fmtty_rel type in place, we can give the more
+general type to %(...%):
+
+| Format_subst : (* %(...%) *)
+ pad_option *
+ ('g, 'h, 'i, 'j, 'k, 'l,
+ 'g2, 'b, 'c, 'j2, 'd, 'a) fmtty_rel *
+ ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
+ (('g, 'h, 'i, 'j, 'k, 'l) format6 -> 'g2, 'b, 'c, 'j2, 'e, 'f) fmt
+
+We accept any format (('g, 'h, 'i, 'j, 'k, 'l) format6) (this is
+completely unrelated to the type of the current format), but also
+require a proof that this format is in relation to another format that
+is concatenable to the format tail. When executing a %(...%) format
+(in camlinternalFormat.ml:make_printf or scanf.ml:make_scanf), we
+transtype the format along this relation using the 'recast' function
+to transpose between related format types.
+
+ val recast :
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1) fmt
+ -> ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
+ -> ('a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmt
+
+NOTE ¹: the typing of Format_subst_ty requires not one format type, but
+two, one to establish the link between the format argument and the
+first six parameters, and the other for the link between the format
+argumant and the last six parameters.
+
+| Format_subst_ty : (* %(...%) *)
+ ('g, 'h, 'i, 'j, 'k, 'l,
+ 'g1, 'b1, 'c1, 'j1, 'd1, 'a1) fmtty_rel *
+ ('g, 'h, 'i, 'j, 'k, 'l,
+ 'g2, 'b2, 'c2, 'j2, 'd2, 'a2) fmtty_rel *
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (('g, 'h, 'i, 'j, 'k, 'l) format6 -> 'g1, 'b1, 'c1, 'j1, 'e1, 'f1,
+ ('g, 'h, 'i, 'j, 'k, 'l) format6 -> 'g2, 'b2, 'c2, 'j2, 'e2, 'f2) fmtty_rel
+
+When we generate a format AST, we generate exactly the same witness
+for both relations, and the witness-conversion functions in
+camlinternalFormat do rely on this invariant. For example, the
+function that proves that the relation is transitive
+
+ val trans :
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
+ -> ('a2, 'b2, 'c2, 'd2, 'e2, 'f2,
+ 'a3, 'b3, 'c3, 'd3, 'e3, 'f3) fmtty_rel
+ -> ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a3, 'b3, 'c3, 'd3, 'e3, 'f3) fmtty_rel
+
+does assume that the two input have exactly the same term structure
+(and is only every used for argument witnesses of the
+Format_subst_ty constructor).
+*)
(* List of format type elements. *)
(* In particular used to represent %(...%) and %{...%} contents. *)
type ('a, 'b, 'c, 'd, 'e, 'f) fmtty =
+ ('a, 'b, 'c, 'd, 'e, 'f,
+ 'a, 'b, 'c, 'd, 'e, 'f) fmtty_rel
+and ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel =
| Char_ty : (* %c *)
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (char -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (char -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ char -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
| String_ty : (* %s *)
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (string -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (string -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ string -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
| Int_ty : (* %d *)
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (int -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (int -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ int -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
| Int32_ty : (* %ld *)
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (int32 -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (int32 -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ int32 -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
| Nativeint_ty : (* %nd *)
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (nativeint -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (nativeint -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ nativeint -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
| Int64_ty : (* %Ld *)
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (int64 -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (int64 -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ int64 -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
| Float_ty : (* %f *)
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (float -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (float -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ float -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
| Bool_ty : (* %B *)
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (bool -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (bool -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ bool -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
| Format_arg_ty : (* %{...%} *)
('g, 'h, 'i, 'j, 'k, 'l) fmtty *
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (('g, 'h, 'i, 'j, 'k, 'l) format6 -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (('g, 'h, 'i, 'j, 'k, 'l) format6 -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ ('g, 'h, 'i, 'j, 'k, 'l) format6 -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
| Format_subst_ty : (* %(...%) *)
- ('d1, 'q1, 'd2, 'q2) reader_nb_unifier *
- ('x, 'b, 'c, 'd1, 'q1, 'u) fmtty *
- ('u, 'b, 'c, 'q1, 'e1, 'f) fmtty ->
- (('x, 'b, 'c, 'd2, 'q2, 'u) format6 -> 'x, 'b, 'c, 'd1, 'e1, 'f) fmtty
+ ('g, 'h, 'i, 'j, 'k, 'l,
+ 'g1, 'b1, 'c1, 'j1, 'd1, 'a1) fmtty_rel *
+ ('g, 'h, 'i, 'j, 'k, 'l,
+ 'g2, 'b2, 'c2, 'j2, 'd2, 'a2) fmtty_rel *
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (('g, 'h, 'i, 'j, 'k, 'l) format6 -> 'g1, 'b1, 'c1, 'j1, 'e1, 'f1,
+ ('g, 'h, 'i, 'j, 'k, 'l) format6 -> 'g2, 'b2, 'c2, 'j2, 'e2, 'f2) fmtty_rel
(* Printf and Format specific constructors. *)
| Alpha_ty : (* %a *)
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (('b -> 'x -> 'c) -> 'x -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (('b1 -> 'x -> 'c1) -> 'x -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ ('b2 -> 'x -> 'c2) -> 'x -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
| Theta_ty : (* %t *)
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (('b -> 'c) -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (('b1 -> 'c1) -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ ('b2 -> 'c2) -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
(* Scanf specific constructor. *)
| Reader_ty : (* %r *)
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- ('x -> 'a, 'b, 'c, ('b -> 'x) -> 'd, 'e, 'f) fmtty
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ ('x -> 'a1, 'b1, 'c1, ('b1 -> 'x) -> 'd1, 'e1, 'f1,
+ 'x -> 'a2, 'b2, 'c2, ('b2 -> 'x) -> 'd2, 'e2, 'f2) fmtty_rel
| Ignored_reader_ty : (* %_r *)
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- ('a, 'b, 'c, ('b -> 'x) -> 'd, 'e, 'f) fmtty
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ ('a1, 'b1, 'c1, ('b1 -> 'x) -> 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, ('b2 -> 'x) -> 'd2, 'e2, 'f2) fmtty_rel
| End_of_fmtty :
- ('f, 'b, 'c, 'd, 'd, 'f) fmtty
+ ('f1, 'b1, 'c1, 'd1, 'd1, 'f1,
+ 'f2, 'b2, 'c2, 'd2, 'd2, 'f2) fmtty_rel
(***)
@@ -673,10 +824,11 @@ and ('a, 'b, 'c, 'd, 'e, 'f) fmt =
('a, 'b, 'c, 'd, 'e, 'f) fmt ->
(('g, 'h, 'i, 'j, 'k, 'l) format6 -> 'a, 'b, 'c, 'd, 'e, 'f) fmt
| Format_subst : (* %(...%) *)
- pad_option * ('d1, 'q1, 'd2, 'q2) reader_nb_unifier *
- ('x, 'b, 'c, 'd1, 'q1, 'u) fmtty *
- ('u, 'b, 'c, 'q1, 'e1, 'f) fmt ->
- (('x, 'b, 'c, 'd2, 'q2, 'u) format6 -> 'x, 'b, 'c, 'd1, 'e1, 'f) fmt
+ pad_option *
+ ('g, 'h, 'i, 'j, 'k, 'l,
+ 'g2, 'b, 'c, 'j2, 'd, 'a) fmtty_rel *
+ ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
+ (('g, 'h, 'i, 'j, 'k, 'l) format6 -> 'g2, 'b, 'c, 'j2, 'e, 'f) fmt
(* Printf and Format specific constructor. *)
| Alpha : (* %a *)
@@ -733,7 +885,7 @@ and ('a, 'b, 'c, 'd, 'e, 'f) ignored =
| Ignored_bool : (* %_B *)
('a, 'b, 'c, 'd, 'd, 'a) ignored
| Ignored_format_arg : (* %_{...%} *)
- pad_option * ('x, 'b, 'c, 'y, 'z, 't) fmtty ->
+ pad_option * ('g, 'h, 'i, 'j, 'k, 'l) fmtty ->
('a, 'b, 'c, 'd, 'd, 'a) ignored
| Ignored_format_subst : (* %_(...%) *)
pad_option * ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
@@ -748,6 +900,40 @@ and ('a, 'b, 'c, 'd, 'e, 'f) ignored =
and ('a, 'b, 'c, 'd, 'e, 'f) format6 =
Format of ('a, 'b, 'c, 'd, 'e, 'f) fmt * string
+let rec erase_rel : type a b c d e f g h i j k l .
+ (a, b, c, d, e, f,
+ g, h, i, j, k, l) fmtty_rel -> (a, b, c, d, e, f) fmtty
+= function
+ | Char_ty rest ->
+ Char_ty (erase_rel rest)
+ | String_ty rest ->
+ String_ty (erase_rel rest)
+ | Int_ty rest ->
+ Int_ty (erase_rel rest)
+ | Int32_ty rest ->
+ Int32_ty (erase_rel rest)
+ | Int64_ty rest ->
+ Int64_ty (erase_rel rest)
+ | Nativeint_ty rest ->
+ Nativeint_ty (erase_rel rest)
+ | Float_ty rest ->
+ Float_ty (erase_rel rest)
+ | Bool_ty rest ->
+ Bool_ty (erase_rel rest)
+ | Format_arg_ty (ty, rest) ->
+ Format_arg_ty (ty, erase_rel rest)
+ | Format_subst_ty (ty1, ty2, rest) ->
+ Format_subst_ty (ty1, ty1, erase_rel rest)
+ | Alpha_ty rest ->
+ Alpha_ty (erase_rel rest)
+ | Theta_ty rest ->
+ Theta_ty (erase_rel rest)
+ | Reader_ty rest ->
+ Reader_ty (erase_rel rest)
+ | Ignored_reader_ty rest ->
+ Ignored_reader_ty (erase_rel rest)
+ | End_of_fmtty -> End_of_fmtty
+
(******************************************************************************)
(* Format type concatenation *)
@@ -756,10 +942,24 @@ and ('a, 'b, 'c, 'd, 'e, 'f) format6 =
* reader_nb_unifier_of_fmtty to count readers in an fmtty,
* Scanf.take_fmtty_format_readers to extract readers inside %(...%),
* CamlinternalFormat.fmtty_of_ignored_format to extract format type. *)
+
+(*
let rec concat_fmtty : type a b c d e f g h .
(a, b, c, d, e, f) fmtty ->
(f, b, c, e, g, h) fmtty ->
(a, b, c, d, g, h) fmtty =
+*)
+let rec concat_fmtty :
+ type a1 b1 c1 d1 e1 f1
+ a2 b2 c2 d2 e2 f2
+ g1 j1 g2 j2
+ .
+ (g1, b1, c1, j1, d1, a1,
+ g2, b2, c2, j2, d2, a2) fmtty_rel ->
+ (a1, b1, c1, d1, e1, f1,
+ a2, b2, c2, d2, e2, f2) fmtty_rel ->
+ (g1, b1, c1, j1, e1, f1,
+ g2, b2, c2, j2, e2, f2) fmtty_rel =
fun fmtty1 fmtty2 -> match fmtty1 with
| Char_ty rest ->
Char_ty (concat_fmtty rest fmtty2)
@@ -787,8 +987,8 @@ fun fmtty1 fmtty2 -> match fmtty1 with
Ignored_reader_ty (concat_fmtty rest fmtty2)
| Format_arg_ty (ty, rest) ->
Format_arg_ty (ty, concat_fmtty rest fmtty2)
- | Format_subst_ty (rnu, ty, rest) ->
- Format_subst_ty (rnu, ty, concat_fmtty rest fmtty2)
+ | Format_subst_ty (ty1, ty2, rest) ->
+ Format_subst_ty (ty1, ty2, concat_fmtty rest fmtty2)
| End_of_fmtty -> fmtty2
(******************************************************************************)
@@ -838,8 +1038,8 @@ fun fmt1 fmt2 -> match fmt1 with
| Format_arg (pad, fmtty, rest) ->
Format_arg (pad, fmtty, concat_fmt rest fmt2)
- | Format_subst (pad, rnu, fmtty, rest) ->
- Format_subst (pad, rnu, fmtty, concat_fmt rest fmt2)
+ | Format_subst (pad, fmtty, rest) ->
+ Format_subst (pad, fmtty, concat_fmt rest fmt2)
| Scan_char_set (width_opt, char_set, rest) ->
Scan_char_set (width_opt, char_set, concat_fmt rest fmt2)
View
326 stdlib/pervasives.mli
@@ -1014,138 +1014,185 @@ module CamlinternalFormatBasics : sig
type prec_option = int option
- type ('d1, 'e1, 'd2, 'e2) reader_nb_unifier =
- | Zero_reader :
- ('d1, 'd1, 'd2, 'd2) reader_nb_unifier
- | Succ_reader :
- ('d1, 'e1, 'd2, 'e2) reader_nb_unifier ->
- ('x -> 'd1, 'e1, 'x -> 'd2, 'e2) reader_nb_unifier
-
- type ('a, 'b, 'c, 'd, 'e, 'f) fmtty =
- | Char_ty :
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (char -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
- | String_ty :
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (string -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
- | Int_ty :
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (int -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
- | Int32_ty :
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (int32 -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
- | Nativeint_ty :
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (nativeint -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
- | Int64_ty :
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (int64 -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
- | Float_ty :
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (float -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
- | Bool_ty :
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (bool -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
- | Format_arg_ty :
- ('g, 'h, 'i, 'j, 'k, 'l) fmtty * ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (('g, 'h, 'i, 'j, 'k, 'l) format6 -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
- | Format_subst_ty :
- ('d1, 'q1, 'd2, 'q2) reader_nb_unifier *
- ('x, 'b, 'c, 'd1, 'q1, 'u) fmtty *
- ('u, 'b, 'c, 'q1, 'e1, 'f) fmtty ->
- (('x, 'b, 'c, 'd2, 'q2, 'u) format6 -> 'x, 'b, 'c, 'd1, 'e1, 'f) fmtty
- | Alpha_ty :
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (('b -> 'x -> 'c) -> 'x -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
- | Theta_ty :
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- (('b -> 'c) -> 'a, 'b, 'c, 'd, 'e, 'f) fmtty
- | Reader_ty :
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- ('x -> 'a, 'b, 'c, ('b -> 'x) -> 'd, 'e, 'f) fmtty
- | Ignored_reader_ty :
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- ('a, 'b, 'c, ('b -> 'x) -> 'd, 'e, 'f) fmtty
- | End_of_fmtty :
- ('f, 'b, 'c, 'd, 'd, 'f) fmtty
-
- and ('a, 'b, 'c, 'd, 'e, 'f) fmt =
- | Char :
- ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
- (char -> 'a, 'b, 'c, 'd, 'e, 'f) fmt
- | Caml_char :
- ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
- (char -> 'a, 'b, 'c, 'd, 'e, 'f) fmt
- | String :
- ('x, string -> 'a) padding * ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
- ('x, 'b, 'c, 'd, 'e, 'f) fmt
- | Caml_string :
- ('x, string -> 'a) padding * ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
- ('x, 'b, 'c, 'd, 'e, 'f) fmt
- | Int :
- int_conv * ('x, 'y) padding * ('y, int -> 'a) precision *
- ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
- ('x, 'b, 'c, 'd, 'e, 'f) fmt
- | Int32 :
- int_conv * ('x, 'y) padding * ('y, int32 -> 'a) precision *
- ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
- ('x, 'b, 'c, 'd, 'e, 'f) fmt
- | Nativeint :
- int_conv * ('x, 'y) padding * ('y, nativeint -> 'a) precision *
- ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
- ('x, 'b, 'c, 'd, 'e, 'f) fmt
- | Int64 :
- int_conv * ('x, 'y) padding * ('y, int64 -> 'a) precision *
- ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
- ('x, 'b, 'c, 'd, 'e, 'f) fmt
- | Float :
- float_conv * ('x, 'y) padding * ('y, float -> 'a) precision *
- ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
- ('x, 'b, 'c, 'd, 'e, 'f) fmt
- | Bool :
- ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
- (bool -> 'a, 'b, 'c, 'd, 'e, 'f) fmt
- | Flush :
- ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
- ('a, 'b, 'c, 'd, 'e, 'f) fmt
- | String_literal :
- string * ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
- ('a, 'b, 'c, 'd, 'e, 'f) fmt
- | Char_literal :
- char * ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
- ('a, 'b, 'c, 'd, 'e, 'f) fmt
- | Format_arg :
- pad_option * ('g, 'h, 'i, 'j, 'k, 'l) fmtty *
- ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
- (('g, 'h, 'i, 'j, 'k, 'l) format6 -> 'a, 'b, 'c, 'd, 'e, 'f) fmt
- | Format_subst :
- pad_option * ('d1, 'q1, 'd2, 'q2) reader_nb_unifier *
- ('x, 'b, 'c, 'd1, 'q1, 'u) fmtty *
- ('u, 'b, 'c, 'q1, 'e1, 'f) fmt ->
- (('x,'b,'c,'d2, 'q2, 'u) format6 -> 'x, 'b, 'c, 'd1, 'e1, 'f) fmt
- | Alpha :
- ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
- (('b -> 'x -> 'c) -> 'x -> 'a, 'b, 'c, 'd, 'e, 'f) fmt
- | Theta :
- ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
- (('b -> 'c) -> 'a, 'b, 'c, 'd, 'e, 'f) fmt
- | Formatting :
- formatting * ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
- ('a, 'b, 'c, 'd, 'e, 'f) fmt
- | Reader :
- ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
- ('x -> 'a, 'b, 'c, ('b -> 'x) -> 'd, 'e, 'f) fmt
- | Scan_char_set :
- pad_option * char_set * ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
- (string -> 'a, 'b, 'c, 'd, 'e, 'f) fmt
- | Scan_get_counter :
- counter * ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
- (int -> 'a, 'b, 'c, 'd, 'e, 'f) fmt
- | Ignored_param :
- ('a, 'b, 'c, 'd, 'y, 'x) ignored * ('x, 'b, 'c, 'y, 'e, 'f) fmt ->
- ('a, 'b, 'c, 'd, 'e, 'f) fmt
- | End_of_format :
- ('f, 'b, 'c, 'e, 'e, 'f) fmt
+type ('a, 'b, 'c, 'd, 'e, 'f) fmtty =
+ ('a, 'b, 'c, 'd, 'e, 'f,
+ 'a, 'b, 'c, 'd, 'e, 'f) fmtty_rel
+and ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel =
+ | Char_ty : (* %c *)
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (char -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ char -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
+ | String_ty : (* %s *)
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (string -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ string -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
+ | Int_ty : (* %d *)
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (int -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ int -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
+ | Int32_ty : (* %ld *)
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (int32 -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ int32 -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
+ | Nativeint_ty : (* %nd *)
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (nativeint -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ nativeint -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
+ | Int64_ty : (* %Ld *)
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (int64 -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ int64 -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
+ | Float_ty : (* %f *)
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (float -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ float -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
+ | Bool_ty : (* %B *)
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (bool -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ bool -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
+ | Format_arg_ty : (* %{...%} *)
+ ('g, 'h, 'i, 'j, 'k, 'l) fmtty *
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (('g, 'h, 'i, 'j, 'k, 'l) format6 -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ ('g, 'h, 'i, 'j, 'k, 'l) format6 -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
+ | Format_subst_ty : (* %(...%) *)
+ ('g, 'h, 'i, 'j, 'k, 'l,
+ 'g1, 'b1, 'c1, 'j1, 'd1, 'a1) fmtty_rel *
+ ('g, 'h, 'i, 'j, 'k, 'l,
+ 'g2, 'b2, 'c2, 'j2, 'd2, 'a2) fmtty_rel *
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (('g, 'h, 'i, 'j, 'k, 'l) format6 -> 'g1, 'b1, 'c1, 'j1, 'e1, 'f1,
+ ('g, 'h, 'i, 'j, 'k, 'l) format6 -> 'g2, 'b2, 'c2, 'j2, 'e2, 'f2) fmtty_rel
+
+ (* Printf and Format specific constructors. *)
+ | Alpha_ty : (* %a *)
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (('b1 -> 'x -> 'c1) -> 'x -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ ('b2 -> 'x -> 'c2) -> 'x -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
+ | Theta_ty : (* %t *)
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ (('b1 -> 'c1) -> 'a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ ('b2 -> 'c2) -> 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel
+
+ (* Scanf specific constructor. *)
+ | Reader_ty : (* %r *)
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ ('x -> 'a1, 'b1, 'c1, ('b1 -> 'x) -> 'd1, 'e1, 'f1,
+ 'x -> 'a2, 'b2, 'c2, ('b2 -> 'x) -> 'd2, 'e2, 'f2) fmtty_rel
+ | Ignored_reader_ty : (* %_r *)
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ ('a1, 'b1, 'c1, ('b1 -> 'x) -> 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, ('b2 -> 'x) -> 'd2, 'e2, 'f2) fmtty_rel
+
+ | End_of_fmtty :
+ ('f1, 'b1, 'c1, 'd1, 'd1, 'f1,
+ 'f2, 'b2, 'c2, 'd2, 'd2, 'f2) fmtty_rel
+
+(***)
+
+(* List of format elements. *)
+and ('a, 'b, 'c, 'd, 'e, 'f) fmt =
+ | Char : (* %c *)
+ ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
+ (char -> 'a, 'b, 'c, 'd, 'e, 'f) fmt
+ | Caml_char : (* %C *)
+ ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
+ (char -> 'a, 'b, 'c, 'd, 'e, 'f) fmt
+ | String : (* %s *)
+ ('x, string -> 'a) padding * ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
+ ('x, 'b, 'c, 'd, 'e, 'f) fmt
+ | Caml_string : (* %S *)
+ ('x, string -> 'a) padding * ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
+ ('x, 'b, 'c, 'd, 'e, 'f) fmt
+ | Int : (* %[dixXuo] *)
+ int_conv * ('x, 'y) padding * ('y, int -> 'a) precision *
+ ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
+ ('x, 'b, 'c, 'd, 'e, 'f) fmt
+ | Int32 : (* %l[dixXuo] *)
+ int_conv * ('x, 'y) padding * ('y, int32 -> 'a) precision *
+ ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
+ ('x, 'b, 'c, 'd, 'e, 'f) fmt
+ | Nativeint : (* %n[dixXuo] *)
+ int_conv * ('x, 'y) padding * ('y, nativeint -> 'a) precision *
+ ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
+ ('x, 'b, 'c, 'd, 'e, 'f) fmt
+ | Int64 : (* %L[dixXuo] *)
+ int_conv * ('x, 'y) padding * ('y, int64 -> 'a) precision *
+ ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
+ ('x, 'b, 'c, 'd, 'e, 'f) fmt
+ | Float : (* %[feEgGF] *)
+ float_conv * ('x, 'y) padding * ('y, float -> 'a) precision *
+ ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
+ ('x, 'b, 'c, 'd, 'e, 'f) fmt
+ | Bool : (* %[bB] *)
+ ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
+ (bool -> 'a, 'b, 'c, 'd, 'e, 'f) fmt
+ | Flush : (* %! *)
+ ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
+ ('a, 'b, 'c, 'd, 'e, 'f) fmt
+
+ | String_literal : (* abc *)
+ string * ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
+ ('a, 'b, 'c, 'd, 'e, 'f) fmt
+ | Char_literal : (* x *)
+ char * ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
+ ('a, 'b, 'c, 'd, 'e, 'f) fmt
+
+ | Format_arg : (* %{...%} *)
+ pad_option * ('g, 'h, 'i, 'j, 'k, 'l) fmtty *
+ ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
+ (('g, 'h, 'i, 'j, 'k, 'l) format6 -> 'a, 'b, 'c, 'd, 'e, 'f) fmt
+ | Format_subst : (* %(...%) *)
+ pad_option *
+ ('g, 'h, 'i, 'j, 'k, 'l,
+ 'g2, 'b, 'c, 'j2, 'd, 'a) fmtty_rel *
+ ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
+ (('g, 'h, 'i, 'j, 'k, 'l) format6 -> 'g2, 'b, 'c, 'j2, 'e, 'f) fmt
+
+ (* Printf and Format specific constructor. *)
+ | Alpha : (* %a *)
+ ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
+ (('b -> 'x -> 'c) -> 'x -> 'a, 'b, 'c, 'd, 'e, 'f) fmt
+ | Theta : (* %t *)
+ ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
+ (('b -> 'c) -> 'a, 'b, 'c, 'd, 'e, 'f) fmt
+
+ (* Format specific constructor: *)
+ | Formatting : (* @_ *)
+ formatting * ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
+ ('a, 'b, 'c, 'd, 'e, 'f) fmt
+
+ (* Scanf specific constructors: *)
+ | Reader : (* %r *)
+ ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
+ ('x -> 'a, 'b, 'c, ('b -> 'x) -> 'd, 'e, 'f) fmt
+ | Scan_char_set : (* %[...] *)
+ pad_option * char_set * ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
+ (string -> 'a, 'b, 'c, 'd, 'e, 'f) fmt
+ | Scan_get_counter : (* %[nlNL] *)
+ counter * ('a, 'b, 'c, 'd, 'e, 'f) fmt ->
+ (int -> 'a, 'b, 'c, 'd, 'e, 'f) fmt
+ | Ignored_param : (* %_ *)
+ ('a, 'b, 'c, 'd, 'y, 'x) ignored * ('x, 'b, 'c, 'y, 'e, 'f) fmt ->
+ ('a, 'b, 'c, 'd, 'e, 'f) fmt
+
+ | End_of_format :
+ ('f, 'b, 'c, 'e, 'e, 'f) fmt
and ('a, 'b, 'c, 'd, 'e, 'f) ignored =
| Ignored_char :
@@ -1169,7 +1216,7 @@ module CamlinternalFormatBasics : sig
| Ignored_bool :
('a, 'b, 'c, 'd, 'd, 'a) ignored
| Ignored_format_arg :
- pad_option * ('x, 'b, 'c, 'y, 'z, 't) fmtty ->
+ pad_option * ('g, 'h, 'i, 'j, 'k, 'l) fmtty ->
('a, 'b, 'c, 'd, 'd, 'a) ignored
| Ignored_format_subst :
pad_option * ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
@@ -1185,9 +1232,16 @@ module CamlinternalFormatBasics : sig
Format of ('a, 'b, 'c, 'd, 'e, 'f) fmt * string
val concat_fmtty :
- ('a, 'b, 'c, 'd, 'e, 'f) fmtty ->
- ('f, 'b, 'c, 'e, 'g, 'h) fmtty ->
- ('a, 'b, 'c, 'd, 'g, 'h) fmtty
+ ('g1, 'b1, 'c1, 'j1, 'd1, 'a1,
+ 'g2, 'b2, 'c2, 'j2, 'd2, 'a2) fmtty_rel ->
+ ('a1, 'b1, 'c1, 'd1, 'e1, 'f1,
+ 'a2, 'b2, 'c2, 'd2, 'e2, 'f2) fmtty_rel ->
+ ('g1, 'b1, 'c1, 'j1, 'e1, 'f1,
+ 'g2, 'b2, 'c2, 'j2, 'e2, 'f2) fmtty_rel
+
+ val erase_rel :
+ ('a, 'b, 'c, 'd, 'e, 'f,
+ 'g, 'h, 'i, 'j, 'k, 'l) fmtty_rel -> ('a, 'b, 'c, 'd, 'e, 'f) fmtty
val concat_fmt :
('a, 'b, 'c, 'd, 'e, 'f) fmt ->
View
99 stdlib/scanf.ml
@@ -1036,7 +1036,7 @@ fun k fmt -> match fmt with
| Formatting (_, rest) -> take_format_readers k rest
| Format_arg (_, _, rest) -> take_format_readers k rest
- | Format_subst (_, _, fmtty, rest) -> take_fmtty_format_readers k fmtty rest
+ | Format_subst (_, fmtty, rest) -> take_fmtty_format_readers k (erase_rel (symm fmtty)) rest
| Ignored_param (ign, rest) -> take_ignored_format_readers k ign rest
| End_of_format -> k Nil
@@ -1066,7 +1066,8 @@ fun k fmtty fmt -> match fmtty with
| Theta_ty rest -> take_fmtty_format_readers k rest fmt
| Format_arg_ty (_, rest) -> take_fmtty_format_readers k rest fmt
| End_of_fmtty -> take_format_readers k fmt
- | Format_subst_ty (_, ty, rest) ->
+ | Format_subst_ty (ty1, ty2, rest) ->
+ let ty = trans (symm ty1) ty2 in
take_fmtty_format_readers k (concat_fmtty ty rest) fmt
(* Take readers associated to an ignored parameter. *)
@@ -1094,77 +1095,6 @@ fun k ign fmt -> match ign with
| Ignored_scan_get_counter _ -> take_format_readers k fmt
(******************************************************************************)
- (* Scanf "%(...%)" tools *)
-
-(* Type used to cross and substract reader_nb_unifer. *)
-(* Used to interface make_format_subst_rnus and convert_fmtty_on_reader_nb. *)
-type (_, _, _, _, _, _, _) format_subst_rnus = Format_subst_rnus :
- ('d3, 'q3, 'd2, 'q2) reader_nb_unifier *
- ('d1, 'q1, 'd3, 'q3) reader_nb_unifier *
- ('q1, 'e1, 'q3, 'e3) reader_nb_unifier ->
- ('d1, 'q1, 'e1, 'd2, 'q2, 'd3, 'e3) format_subst_rnus
-
-(* Cross and substract reader_nb_unifers. *)
-(* Used when formats contains encapsulated "%(...%)" like "%(..%(..%)..%)". *)
-(* See (convert_fmtty_on_reader_nb _ "%(...%)"). *)
-let rec make_format_subst_rnus : type d1 q1 e1 d2 q2 d3 e3 .
- (d1, e1, d3, e3) reader_nb_unifier -> (d1, q1, d2, q2) reader_nb_unifier ->
- (d1, q1, e1, d2, q2, d3, e3) format_subst_rnus =
-fun rnu sub_rnu -> match rnu, sub_rnu with
- | Succ_reader rnu_rest, Succ_reader sub_rnu_rest ->
- let Format_subst_rnus (sub_rnu', sub_fmtty_rnu, rest_rnu) =
- make_format_subst_rnus rnu_rest sub_rnu_rest in
- Format_subst_rnus(Succ_reader sub_rnu', Succ_reader sub_fmtty_rnu, rest_rnu)
- | _, Zero_reader ->
- Format_subst_rnus (Zero_reader, Zero_reader, rnu)
- | Zero_reader, Succ_reader _ ->
- (* Impossible! By hypothesis: rnu > sub_rnu. *)
- assert false
-
-(* Use a reader_nb_unifier to transform 'd and 'e parameters of an fmtty. *)
-(* See make_scanf "%(...%)". *)
-let rec convert_fmtty_on_reader_nb : type a b c d1 d2 e1 e2 f .
- (d1, e1, d2, e2) reader_nb_unifier -> (a, b, c, d1, e1, f) fmtty ->
- (a, b, c, d2, e2, f) fmtty =
-fun rnu fmtty -> match rnu, fmtty with
- | _, Char_ty rest -> Char_ty (convert_fmtty_on_reader_nb rnu rest)
- | _, String_ty rest -> String_ty (convert_fmtty_on_reader_nb rnu rest)
- | _, Int_ty rest -> Int_ty (convert_fmtty_on_reader_nb rnu rest)
- | _, Int32_ty rest -> Int32_ty (convert_fmtty_on_reader_nb rnu rest)
- | _, Nativeint_ty rest -> Nativeint_ty (convert_fmtty_on_reader_nb rnu rest)
- | _, Int64_ty rest -> Int64_ty (convert_fmtty_on_reader_nb rnu rest)
- | _, Float_ty rest -> Float_ty (convert_fmtty_on_reader_nb rnu rest)
- | _, Bool_ty rest -> Bool_ty (convert_fmtty_on_reader_nb rnu rest)
- | _, Alpha_ty rest -> Alpha_ty (convert_fmtty_on_reader_nb rnu rest)
- | _, Theta_ty rest -> Theta_ty (convert_fmtty_on_reader_nb rnu rest)
-
- | Succ_reader rnu_rest, Reader_ty fmtty_rest ->
- Reader_ty (convert_fmtty_on_reader_nb rnu_rest fmtty_rest)
- | Succ_reader rnu_rest, Ignored_reader_ty fmtty_rest ->
- Ignored_reader_ty (convert_fmtty_on_reader_nb rnu_rest fmtty_rest)
-
- | _, Format_arg_ty (sub_fmtty, rest) ->
- Format_arg_ty (sub_fmtty, convert_fmtty_on_reader_nb rnu rest)
- | _, Format_subst_ty (sub_rnu, sub_fmtty, rest) ->
- let Format_subst_rnus (sub_rnu', sub_fmtty_rnu, rest_rnu) =
- make_format_subst_rnus rnu sub_rnu in
- let sub_fmtty' = convert_fmtty_on_reader_nb sub_fmtty_rnu sub_fmtty in
- let rest' = convert_fmtty_on_reader_nb rest_rnu rest in
- Format_subst_ty (sub_rnu', sub_fmtty', rest')
-
- | Zero_reader, End_of_fmtty -> End_of_fmtty
-
- | Zero_reader, Reader_ty _ ->
- (* Impossible, by typing constraints on fmtty and rnu constructors: *)
- (* rnu = Zero_reader => d1 == e1 *)
- (* fmtty = Reader_ty _ => d1 <> e1 *)
- assert false
- | Zero_reader, Ignored_reader_ty _ ->
- assert false (* Similar. *)
- | Succ_reader _, End_of_fmtty ->
- assert false (* Similar. *)
-
-(******************************************************************************)
(* Generic scanning *)
(* Make a generic scanning function. *)
@@ -1251,18 +1181,31 @@ fun ib fmt readers -> match fmt with
with Failure msg -> bad_input msg
in
Cons (fmt, make_scanf ib rest readers)
- | Format_subst (pad_opt, rnu, fmtty, rest) ->
- let fmtty' = convert_fmtty_on_reader_nb rnu fmtty in
+ | Format_subst (pad_opt, fmtty, rest) ->
let _ = scan_caml_string (width_of_pad_opt pad_opt) ib in
let s = token_string ib in
let fmt, fmt' =
try
let Fmt_EBB fmt = fmt_ebb_of_string s in
- type_format fmt fmtty, type_format fmt fmtty'
+ let Fmt_EBB fmt' = fmt_ebb_of_string s in
+ (* TODO: find a way to avoid reparsing twice *)
+
+ (* TODO: these type-checks below *can* fail because of type
+ ambiguity in presence of ignored-readers: "%_r%d" and "%d%_r"
+ are typed in the same way.
+
+ # Scanf.sscanf "\"%_r%d\"3" "%(%d%_r%)" ignore
+ (fun fmt n -> string_of_format fmt, n);;
+ Exception: CamlinternalFormat.Type_mismatch.
+
+ We should properly catch this exception.
+ *)
+ type_format fmt (erase_rel fmtty),
+ type_format fmt' (erase_rel (symm fmtty))
with Failure msg -> bad_input msg
in
- Cons (Format (fmt', s),
- make_scanf ib (concat_fmt fmt rest) readers)
+ Cons (Format (fmt, s),
+ make_scanf ib (concat_fmt fmt' rest) readers)
| Scan_char_set (width_opt, char_set, Formatting (fmting, rest)) ->
let stp, str = stopper_of_formatting fmting in
View
20 typing/typecore.ml
@@ -2840,15 +2840,8 @@ and type_format loc str env =
| Some n ->
let lid_loc = mk_lid_loc (Longident.Lident "Some") in
mk_exp_loc (Pexp_construct (lid_loc, Some (mk_int n))) in
- let rec mk_reader_nb_unifier : type d1 e1 d2 e2 .
- (d1, e1, d2, e2) reader_nb_unifier -> Parsetree.expression =
- fun rnu -> match rnu with
- | Succ_reader rest ->
- mk_constr "Succ_reader" [ mk_reader_nb_unifier rest ]
- | Zero_reader ->
- mk_constr "Zero_reader" [] in
- let rec mk_fmtty : type a b c d e f .
- (a, b, c, d, e, f) fmtty -> Parsetree.expression =
+ let rec mk_fmtty : type a b c d e f g h i j k l .
+ (a, b, c, d, e, f, g, h, i, j, k, l) fmtty_rel -> Parsetree.expression =
fun fmtty -> match fmtty with
| Char_ty rest -> mk_constr "Char_ty" [ mk_fmtty rest ]
| String_ty rest -> mk_constr "String_ty" [ mk_fmtty rest ]
@@ -2865,9 +2858,9 @@ and type_format loc str env =
mk_constr "Ignored_reader_ty" [ mk_fmtty rest ]
| Format_arg_ty (sub_fmtty, rest) ->
mk_constr "Format_arg_ty" [ mk_fmtty sub_fmtty; mk_fmtty rest ]
- | Format_subst_ty (rnu, sub_fmtty, rest) ->
+ | Format_subst_ty (sub_fmtty1, sub_fmtty2, rest) ->
mk_constr "Format_subst_ty"
- [ mk_reader_nb_unifier rnu; mk_fmtty sub_fmtty; mk_fmtty rest ]
+ [ mk_fmtty sub_fmtty1; mk_fmtty sub_fmtty2; mk_fmtty rest ]
| End_of_fmtty -> mk_constr "End_of_fmtty" []
in
let mk_ignored : type a b c d e f .
@@ -2955,10 +2948,9 @@ and type_format loc str env =
| Format_arg (pad_opt, fmtty, rest) ->
mk_constr "Format_arg" [
mk_int_opt pad_opt; mk_fmtty fmtty; mk_fmt rest ]
- | Format_subst (pad_opt, rnu, fmtty, rest) ->
+ | Format_subst (pad_opt, fmtty, rest) ->
mk_constr "Format_subst" [
- mk_int_opt pad_opt; mk_reader_nb_unifier rnu; mk_fmtty fmtty;
- mk_fmt rest ]
+ mk_int_opt pad_opt; mk_fmtty fmtty; mk_fmt rest ]
| Alpha rest ->
mk_constr "Alpha" [ mk_fmt rest ]
| Theta rest ->

0 comments on commit e0b0005

Please sign in to comment.
Something went wrong with that request. Please try again.