From 77df44f9c97b7dd4097c2c86dfc73641fb4a1cec Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 5 Feb 2024 15:38:41 -0800 Subject: [PATCH 1/6] Splitting tuples --- ocaml/fstar-lib/FStar_DTuple3.ml | 10 + ocaml/fstar-lib/FStar_DTuple4.ml | 16 ++ ocaml/fstar-lib/FStar_DTuple5.ml | 25 ++ ocaml/fstar-lib/FStar_Pervasives_Native.ml | 264 --------------------- ocaml/fstar-lib/FStar_Tuple10.ml | 24 ++ ocaml/fstar-lib/FStar_Tuple11.ml | 26 ++ ocaml/fstar-lib/FStar_Tuple12.ml | 28 +++ ocaml/fstar-lib/FStar_Tuple13.ml | 30 +++ ocaml/fstar-lib/FStar_Tuple14.ml | 32 +++ ocaml/fstar-lib/FStar_Tuple3.ml | 10 + ocaml/fstar-lib/FStar_Tuple4.ml | 12 + ocaml/fstar-lib/FStar_Tuple5.ml | 14 ++ ocaml/fstar-lib/FStar_Tuple6.ml | 16 ++ ocaml/fstar-lib/FStar_Tuple7.ml | 18 ++ ocaml/fstar-lib/FStar_Tuple8.ml | 20 ++ ocaml/fstar-lib/FStar_Tuple9.ml | 22 ++ ulib/FStar.DTuple3.fsti | 6 + ulib/FStar.DTuple4.fsti | 8 + ulib/FStar.DTuple5.fsti | 9 + ulib/FStar.Pervasives.Native.fst | 112 --------- ulib/FStar.Pervasives.fsti | 20 -- ulib/FStar.Tuple10.fsti | 30 +++ ulib/FStar.Tuple11.fsti | 31 +++ ulib/FStar.Tuple12.fsti | 32 +++ ulib/FStar.Tuple13.fsti | 33 +++ ulib/FStar.Tuple14.fsti | 34 +++ ulib/FStar.Tuple3.fsti | 19 ++ ulib/FStar.Tuple4.fsti | 19 ++ ulib/FStar.Tuple5.fsti | 19 ++ ulib/FStar.Tuple6.fsti | 19 ++ ulib/FStar.Tuple7.fsti | 20 ++ ulib/FStar.Tuple8.fsti | 20 ++ ulib/FStar.Tuple9.fsti | 29 +++ 33 files changed, 631 insertions(+), 396 deletions(-) create mode 100644 ocaml/fstar-lib/FStar_DTuple3.ml create mode 100644 ocaml/fstar-lib/FStar_DTuple4.ml create mode 100644 ocaml/fstar-lib/FStar_DTuple5.ml create mode 100644 ocaml/fstar-lib/FStar_Tuple10.ml create mode 100644 ocaml/fstar-lib/FStar_Tuple11.ml create mode 100644 ocaml/fstar-lib/FStar_Tuple12.ml create mode 100644 ocaml/fstar-lib/FStar_Tuple13.ml create mode 100644 ocaml/fstar-lib/FStar_Tuple14.ml create mode 100644 ocaml/fstar-lib/FStar_Tuple3.ml create mode 100644 ocaml/fstar-lib/FStar_Tuple4.ml create mode 100644 ocaml/fstar-lib/FStar_Tuple5.ml create mode 100644 ocaml/fstar-lib/FStar_Tuple6.ml create mode 100644 ocaml/fstar-lib/FStar_Tuple7.ml create mode 100644 ocaml/fstar-lib/FStar_Tuple8.ml create mode 100644 ocaml/fstar-lib/FStar_Tuple9.ml create mode 100644 ulib/FStar.DTuple3.fsti create mode 100644 ulib/FStar.DTuple4.fsti create mode 100644 ulib/FStar.DTuple5.fsti create mode 100644 ulib/FStar.Tuple10.fsti create mode 100644 ulib/FStar.Tuple11.fsti create mode 100644 ulib/FStar.Tuple12.fsti create mode 100644 ulib/FStar.Tuple13.fsti create mode 100644 ulib/FStar.Tuple14.fsti create mode 100644 ulib/FStar.Tuple3.fsti create mode 100644 ulib/FStar.Tuple4.fsti create mode 100644 ulib/FStar.Tuple5.fsti create mode 100644 ulib/FStar.Tuple6.fsti create mode 100644 ulib/FStar.Tuple7.fsti create mode 100644 ulib/FStar.Tuple8.fsti create mode 100644 ulib/FStar.Tuple9.fsti diff --git a/ocaml/fstar-lib/FStar_DTuple3.ml b/ocaml/fstar-lib/FStar_DTuple3.ml new file mode 100644 index 00000000000..6cee1a8fb43 --- /dev/null +++ b/ocaml/fstar-lib/FStar_DTuple3.ml @@ -0,0 +1,10 @@ +type ('a, 'b, 'c) dtuple3 = + | Mkdtuple3 of 'a * 'b * 'c +let uu___is_Mkdtuple3 : 'a 'b 'c . ('a, 'b, 'c) dtuple3 -> Prims.bool = + fun projectee -> true +let __proj__Mkdtuple3__item___1 : 'a 'b 'c . ('a, 'b, 'c) dtuple3 -> 'a = + fun projectee -> match projectee with | Mkdtuple3 (_1, _2, _3) -> _1 +let __proj__Mkdtuple3__item___2 : 'a 'b 'c . ('a, 'b, 'c) dtuple3 -> 'b = + fun projectee -> match projectee with | Mkdtuple3 (_1, _2, _3) -> _2 +let __proj__Mkdtuple3__item___3 : 'a 'b 'c . ('a, 'b, 'c) dtuple3 -> 'c = + fun projectee -> match projectee with | Mkdtuple3 (_1, _2, _3) -> _3 diff --git a/ocaml/fstar-lib/FStar_DTuple4.ml b/ocaml/fstar-lib/FStar_DTuple4.ml new file mode 100644 index 00000000000..306a9b5deb9 --- /dev/null +++ b/ocaml/fstar-lib/FStar_DTuple4.ml @@ -0,0 +1,16 @@ +type ('a, 'b, 'c, 'd) dtuple4 = + | Mkdtuple4 of 'a * 'b * 'c * 'd +let uu___is_Mkdtuple4 : 'a 'b 'c 'd . ('a, 'b, 'c, 'd) dtuple4 -> Prims.bool + = fun projectee -> true +let __proj__Mkdtuple4__item___1 : + 'a 'b 'c 'd . ('a, 'b, 'c, 'd) dtuple4 -> 'a = + fun projectee -> match projectee with | Mkdtuple4 (_1, _2, _3, _4) -> _1 +let __proj__Mkdtuple4__item___2 : + 'a 'b 'c 'd . ('a, 'b, 'c, 'd) dtuple4 -> 'b = + fun projectee -> match projectee with | Mkdtuple4 (_1, _2, _3, _4) -> _2 +let __proj__Mkdtuple4__item___3 : + 'a 'b 'c 'd . ('a, 'b, 'c, 'd) dtuple4 -> 'c = + fun projectee -> match projectee with | Mkdtuple4 (_1, _2, _3, _4) -> _3 +let __proj__Mkdtuple4__item___4 : + 'a 'b 'c 'd . ('a, 'b, 'c, 'd) dtuple4 -> 'd = + fun projectee -> match projectee with | Mkdtuple4 (_1, _2, _3, _4) -> _4 diff --git a/ocaml/fstar-lib/FStar_DTuple5.ml b/ocaml/fstar-lib/FStar_DTuple5.ml new file mode 100644 index 00000000000..13541e514b2 --- /dev/null +++ b/ocaml/fstar-lib/FStar_DTuple5.ml @@ -0,0 +1,25 @@ +type ('a, 'b, 'c, 'd, 'e) dtuple5 = + | Mkdtuple5 of 'a * 'b * 'c * 'd * 'e +let uu___is_Mkdtuple5 : + 'a 'b 'c 'd 'e . ('a, 'b, 'c, 'd, 'e) dtuple5 -> Prims.bool = + fun projectee -> true +let __proj__Mkdtuple5__item___1 : + 'a 'b 'c 'd 'e . ('a, 'b, 'c, 'd, 'e) dtuple5 -> 'a = + fun projectee -> + match projectee with | Mkdtuple5 (_1, _2, _3, _4, _5) -> _1 +let __proj__Mkdtuple5__item___2 : + 'a 'b 'c 'd 'e . ('a, 'b, 'c, 'd, 'e) dtuple5 -> 'b = + fun projectee -> + match projectee with | Mkdtuple5 (_1, _2, _3, _4, _5) -> _2 +let __proj__Mkdtuple5__item___3 : + 'a 'b 'c 'd 'e . ('a, 'b, 'c, 'd, 'e) dtuple5 -> 'c = + fun projectee -> + match projectee with | Mkdtuple5 (_1, _2, _3, _4, _5) -> _3 +let __proj__Mkdtuple5__item___4 : + 'a 'b 'c 'd 'e . ('a, 'b, 'c, 'd, 'e) dtuple5 -> 'd = + fun projectee -> + match projectee with | Mkdtuple5 (_1, _2, _3, _4, _5) -> _4 +let __proj__Mkdtuple5__item___5 : + 'a 'b 'c 'd 'e . ('a, 'b, 'c, 'd, 'e) dtuple5 -> 'e = + fun projectee -> + match projectee with | Mkdtuple5 (_1, _2, _3, _4, _5) -> _5 diff --git a/ocaml/fstar-lib/FStar_Pervasives_Native.ml b/ocaml/fstar-lib/FStar_Pervasives_Native.ml index 0027fcb263a..8daa93b4aa1 100644 --- a/ocaml/fstar-lib/FStar_Pervasives_Native.ml +++ b/ocaml/fstar-lib/FStar_Pervasives_Native.ml @@ -19,267 +19,3 @@ let snd = Stdlib.snd let __proj__Mktuple2__item___1 = fst let __proj__Mktuple2__item___2 = snd - -type ('a,'b,'c) tuple3 = - 'a* 'b* 'c -[@@deriving yojson,show] -let uu___is_Mktuple3 projectee = true -let __proj__Mktuple3__item___1 projectee = - match projectee with | (_1,_2,_3) -> _1 -let __proj__Mktuple3__item___2 projectee = - match projectee with | (_1,_2,_3) -> _2 -let __proj__Mktuple3__item___3 projectee = - match projectee with | (_1,_2,_3) -> _3 - -type ('a,'b,'c,'d) tuple4 = - 'a* 'b* 'c* 'd -[@@deriving yojson,show] -let uu___is_Mktuple4 projectee = true -let __proj__Mktuple4__item___1 projectee = - match projectee with | (_1,_2,_3,_4) -> _1 -let __proj__Mktuple4__item___2 projectee = - match projectee with | (_1,_2,_3,_4) -> _2 -let __proj__Mktuple4__item___3 projectee = - match projectee with | (_1,_2,_3,_4) -> _3 -let __proj__Mktuple4__item___4 projectee = - match projectee with | (_1,_2,_3,_4) -> _4 - -type ('a,'b,'c,'d,'e) tuple5 = - 'a* 'b* 'c* 'd* 'e -[@@deriving yojson,show] -let uu___is_Mktuple5 projectee = true -let __proj__Mktuple5__item___1 projectee = - match projectee with | (_1,_2,_3,_4,_5) -> _1 -let __proj__Mktuple5__item___2 projectee = - match projectee with | (_1,_2,_3,_4,_5) -> _2 -let __proj__Mktuple5__item___3 projectee = - match projectee with | (_1,_2,_3,_4,_5) -> _3 -let __proj__Mktuple5__item___4 projectee = - match projectee with | (_1,_2,_3,_4,_5) -> _4 -let __proj__Mktuple5__item___5 projectee = - match projectee with | (_1,_2,_3,_4,_5) -> _5 - -type ('a,'b,'c,'d,'e,'f) tuple6 = - 'a* 'b* 'c* 'd* 'e* 'f -[@@deriving yojson,show] -let uu___is_Mktuple6 projectee = true -let __proj__Mktuple6__item___1 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6) -> _1 -let __proj__Mktuple6__item___2 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6) -> _2 -let __proj__Mktuple6__item___3 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6) -> _3 -let __proj__Mktuple6__item___4 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6) -> _4 -let __proj__Mktuple6__item___5 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6) -> _5 -let __proj__Mktuple6__item___6 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6) -> _6 - -type ('a,'b,'c,'d,'e,'f,'g) tuple7 = - 'a* 'b* 'c* 'd* 'e* 'f* 'g -[@@deriving yojson,show] -let uu___is_Mktuple7 projectee = true -let __proj__Mktuple7__item___1 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7) -> _1 -let __proj__Mktuple7__item___2 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7) -> _2 -let __proj__Mktuple7__item___3 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7) -> _3 -let __proj__Mktuple7__item___4 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7) -> _4 -let __proj__Mktuple7__item___5 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7) -> _5 -let __proj__Mktuple7__item___6 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7) -> _6 -let __proj__Mktuple7__item___7 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7) -> _7 - -type ('a,'b,'c,'d,'e,'f,'g,'h) tuple8 = - 'a* 'b* 'c* 'd* 'e* 'f* 'g* 'h -[@@deriving yojson,show] -let uu___is_Mktuple8 projectee = true -let __proj__Mktuple8__item___1 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8) -> _1 -let __proj__Mktuple8__item___2 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8) -> _2 -let __proj__Mktuple8__item___3 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8) -> _3 -let __proj__Mktuple8__item___4 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8) -> _4 -let __proj__Mktuple8__item___5 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8) -> _5 -let __proj__Mktuple8__item___6 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8) -> _6 -let __proj__Mktuple8__item___7 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8) -> _7 -let __proj__Mktuple8__item___8 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8) -> _8 - -type ('a,'b,'c,'d,'e,'f,'g,'h,'i) tuple9 = - 'a *'b *'c *'d *'e *'f *'g *'h *'i -[@@deriving yojson,show] -let uu___is_Mktuple9 projectee = true -let __proj__Mktuple9__item___1 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9) -> _1 -let __proj__Mktuple9__item___2 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9) -> _2 -let __proj__Mktuple9__item___3 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9) -> _3 -let __proj__Mktuple9__item___4 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9) -> _4 -let __proj__Mktuple9__item___5 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9) -> _5 -let __proj__Mktuple9__item___6 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9) -> _6 -let __proj__Mktuple9__item___7 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9) -> _7 -let __proj__Mktuple9__item___8 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9) -> _8 -let __proj__Mktuple9__item___9 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9) -> _9 - -type ('a,'b,'c,'d,'e,'f,'g,'h,'i,'j) tuple10 = - 'a *'b *'c *'d *'e *'f *'g *'h *'i *'j -[@@deriving yojson,show] -let uu___is_Mktuple10 projectee = true -let __proj__Mktuple10__item___1 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10) -> _1 -let __proj__Mktuple10__item___2 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10) -> _2 -let __proj__Mktuple10__item___3 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10) -> _3 -let __proj__Mktuple10__item___4 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10) -> _4 -let __proj__Mktuple10__item___5 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10) -> _5 -let __proj__Mktuple10__item___6 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10) -> _6 -let __proj__Mktuple10__item___7 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10) -> _7 -let __proj__Mktuple10__item___8 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10) -> _8 -let __proj__Mktuple10__item___9 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10) -> _9 -let __proj__Mktuple10__item___10 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10) -> _10 - -type ('a,'b,'c,'d,'e,'f,'g,'h,'i,'j,'k) tuple11 = - 'a *'b *'c *'d *'e *'f *'g *'h *'i *'j *'k -[@@deriving yojson,show] -let uu___is_Mktuple11 projectee = true -let __proj__Mktuple11__item___1 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11) -> _1 -let __proj__Mktuple11__item___2 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11) -> _2 -let __proj__Mktuple11__item___3 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11) -> _3 -let __proj__Mktuple11__item___4 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11) -> _4 -let __proj__Mktuple11__item___5 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11) -> _5 -let __proj__Mktuple11__item___6 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11) -> _6 -let __proj__Mktuple11__item___7 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11) -> _7 -let __proj__Mktuple11__item___8 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11) -> _8 -let __proj__Mktuple11__item___9 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11) -> _9 -let __proj__Mktuple11__item___10 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11) -> _10 -let __proj__Mktuple11__item___11 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11) -> _11 - -type ('a,'b,'c,'d,'e,'f,'g,'h,'i,'j,'k,'l) tuple12 = - 'a *'b *'c *'d *'e *'f *'g *'h *'i *'j *'k *'l -[@@deriving yojson,show] -let uu___is_Mktuple12 projectee = true -let __proj__Mktuple12__item___1 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12) -> _1 -let __proj__Mktuple12__item___2 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12) -> _2 -let __proj__Mktuple12__item___3 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12) -> _3 -let __proj__Mktuple12__item___4 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12) -> _4 -let __proj__Mktuple12__item___5 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12) -> _5 -let __proj__Mktuple12__item___6 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12) -> _6 -let __proj__Mktuple12__item___7 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12) -> _7 -let __proj__Mktuple12__item___8 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12) -> _8 -let __proj__Mktuple12__item___9 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12) -> _9 -let __proj__Mktuple12__item___10 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12) -> _10 -let __proj__Mktuple12__item___11 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12) -> _11 -let __proj__Mktuple12__item___12 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12) -> _12 - -type ('a,'b,'c,'d,'e,'f,'g,'h,'i,'j,'k,'l,'m) tuple13 = - 'a *'b *'c *'d *'e *'f *'g *'h *'i *'j *'k *'l *'m -[@@deriving yojson,show] -let uu___is_Mktuple13 projectee = true -let __proj__Mktuple13__item___1 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13) -> _1 -let __proj__Mktuple13__item___2 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13) -> _2 -let __proj__Mktuple13__item___3 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13) -> _3 -let __proj__Mktuple13__item___4 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13) -> _4 -let __proj__Mktuple13__item___5 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13) -> _5 -let __proj__Mktuple13__item___6 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13) -> _6 -let __proj__Mktuple13__item___7 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13) -> _7 -let __proj__Mktuple13__item___8 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13) -> _8 -let __proj__Mktuple13__item___9 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13) -> _9 -let __proj__Mktuple13__item___10 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13) -> _10 -let __proj__Mktuple13__item___11 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13) -> _11 -let __proj__Mktuple13__item___12 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13) -> _12 -let __proj__Mktuple13__item___13 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13) -> _13 - -type ('a,'b,'c,'d,'e,'f,'g,'h,'i,'j,'k,'l,'m,'n) tuple14 = - 'a *'b *'c *'d *'e *'f *'g *'h *'i *'j *'k *'l *'m *'n -[@@deriving yojson,show] -let uu___is_Mktuple14 projectee = true -let __proj__Mktuple14__item___1 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _1 -let __proj__Mktuple14__item___2 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _2 -let __proj__Mktuple14__item___3 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _3 -let __proj__Mktuple14__item___4 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _4 -let __proj__Mktuple14__item___5 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _5 -let __proj__Mktuple14__item___6 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _6 -let __proj__Mktuple14__item___7 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _7 -let __proj__Mktuple14__item___8 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _8 -let __proj__Mktuple14__item___9 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _9 -let __proj__Mktuple14__item___10 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _10 -let __proj__Mktuple14__item___11 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _11 -let __proj__Mktuple14__item___12 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _12 -let __proj__Mktuple14__item___13 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _13 -let __proj__Mktuple14__item___14 projectee = - match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _14 diff --git a/ocaml/fstar-lib/FStar_Tuple10.ml b/ocaml/fstar-lib/FStar_Tuple10.ml new file mode 100644 index 00000000000..faa7547aee3 --- /dev/null +++ b/ocaml/fstar-lib/FStar_Tuple10.ml @@ -0,0 +1,24 @@ +type ('a,'b,'c,'d,'e,'f,'g,'h,'i,'j) tuple10 = + 'a *'b *'c *'d *'e *'f *'g *'h *'i *'j +[@@deriving yojson,show] +let uu___is_Mktuple10 projectee = true +let __proj__Mktuple10__item___1 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10) -> _1 +let __proj__Mktuple10__item___2 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10) -> _2 +let __proj__Mktuple10__item___3 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10) -> _3 +let __proj__Mktuple10__item___4 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10) -> _4 +let __proj__Mktuple10__item___5 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10) -> _5 +let __proj__Mktuple10__item___6 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10) -> _6 +let __proj__Mktuple10__item___7 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10) -> _7 +let __proj__Mktuple10__item___8 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10) -> _8 +let __proj__Mktuple10__item___9 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10) -> _9 +let __proj__Mktuple10__item___10 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10) -> _10 diff --git a/ocaml/fstar-lib/FStar_Tuple11.ml b/ocaml/fstar-lib/FStar_Tuple11.ml new file mode 100644 index 00000000000..95769a4e717 --- /dev/null +++ b/ocaml/fstar-lib/FStar_Tuple11.ml @@ -0,0 +1,26 @@ +type ('a,'b,'c,'d,'e,'f,'g,'h,'i,'j,'k) tuple11 = + 'a *'b *'c *'d *'e *'f *'g *'h *'i *'j *'k +[@@deriving yojson,show] +let uu___is_Mktuple11 projectee = true +let __proj__Mktuple11__item___1 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11) -> _1 +let __proj__Mktuple11__item___2 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11) -> _2 +let __proj__Mktuple11__item___3 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11) -> _3 +let __proj__Mktuple11__item___4 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11) -> _4 +let __proj__Mktuple11__item___5 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11) -> _5 +let __proj__Mktuple11__item___6 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11) -> _6 +let __proj__Mktuple11__item___7 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11) -> _7 +let __proj__Mktuple11__item___8 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11) -> _8 +let __proj__Mktuple11__item___9 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11) -> _9 +let __proj__Mktuple11__item___10 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11) -> _10 +let __proj__Mktuple11__item___11 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11) -> _11 diff --git a/ocaml/fstar-lib/FStar_Tuple12.ml b/ocaml/fstar-lib/FStar_Tuple12.ml new file mode 100644 index 00000000000..3574e0d2dee --- /dev/null +++ b/ocaml/fstar-lib/FStar_Tuple12.ml @@ -0,0 +1,28 @@ +type ('a,'b,'c,'d,'e,'f,'g,'h,'i,'j,'k,'l) tuple12 = + 'a *'b *'c *'d *'e *'f *'g *'h *'i *'j *'k *'l +[@@deriving yojson,show] +let uu___is_Mktuple12 projectee = true +let __proj__Mktuple12__item___1 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12) -> _1 +let __proj__Mktuple12__item___2 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12) -> _2 +let __proj__Mktuple12__item___3 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12) -> _3 +let __proj__Mktuple12__item___4 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12) -> _4 +let __proj__Mktuple12__item___5 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12) -> _5 +let __proj__Mktuple12__item___6 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12) -> _6 +let __proj__Mktuple12__item___7 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12) -> _7 +let __proj__Mktuple12__item___8 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12) -> _8 +let __proj__Mktuple12__item___9 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12) -> _9 +let __proj__Mktuple12__item___10 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12) -> _10 +let __proj__Mktuple12__item___11 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12) -> _11 +let __proj__Mktuple12__item___12 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12) -> _12 diff --git a/ocaml/fstar-lib/FStar_Tuple13.ml b/ocaml/fstar-lib/FStar_Tuple13.ml new file mode 100644 index 00000000000..27ccdf54963 --- /dev/null +++ b/ocaml/fstar-lib/FStar_Tuple13.ml @@ -0,0 +1,30 @@ +type ('a,'b,'c,'d,'e,'f,'g,'h,'i,'j,'k,'l,'m) tuple13 = + 'a *'b *'c *'d *'e *'f *'g *'h *'i *'j *'k *'l *'m +[@@deriving yojson,show] +let uu___is_Mktuple13 projectee = true +let __proj__Mktuple13__item___1 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13) -> _1 +let __proj__Mktuple13__item___2 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13) -> _2 +let __proj__Mktuple13__item___3 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13) -> _3 +let __proj__Mktuple13__item___4 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13) -> _4 +let __proj__Mktuple13__item___5 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13) -> _5 +let __proj__Mktuple13__item___6 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13) -> _6 +let __proj__Mktuple13__item___7 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13) -> _7 +let __proj__Mktuple13__item___8 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13) -> _8 +let __proj__Mktuple13__item___9 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13) -> _9 +let __proj__Mktuple13__item___10 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13) -> _10 +let __proj__Mktuple13__item___11 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13) -> _11 +let __proj__Mktuple13__item___12 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13) -> _12 +let __proj__Mktuple13__item___13 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13) -> _13 diff --git a/ocaml/fstar-lib/FStar_Tuple14.ml b/ocaml/fstar-lib/FStar_Tuple14.ml new file mode 100644 index 00000000000..b352cadf63c --- /dev/null +++ b/ocaml/fstar-lib/FStar_Tuple14.ml @@ -0,0 +1,32 @@ +type ('a,'b,'c,'d,'e,'f,'g,'h,'i,'j,'k,'l,'m,'n) tuple14 = + 'a *'b *'c *'d *'e *'f *'g *'h *'i *'j *'k *'l *'m *'n +[@@deriving yojson,show] +let uu___is_Mktuple14 projectee = true +let __proj__Mktuple14__item___1 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _1 +let __proj__Mktuple14__item___2 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _2 +let __proj__Mktuple14__item___3 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _3 +let __proj__Mktuple14__item___4 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _4 +let __proj__Mktuple14__item___5 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _5 +let __proj__Mktuple14__item___6 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _6 +let __proj__Mktuple14__item___7 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _7 +let __proj__Mktuple14__item___8 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _8 +let __proj__Mktuple14__item___9 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _9 +let __proj__Mktuple14__item___10 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _10 +let __proj__Mktuple14__item___11 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _11 +let __proj__Mktuple14__item___12 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _12 +let __proj__Mktuple14__item___13 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _13 +let __proj__Mktuple14__item___14 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9,_10,_11,_12,_13,_14) -> _14 diff --git a/ocaml/fstar-lib/FStar_Tuple3.ml b/ocaml/fstar-lib/FStar_Tuple3.ml new file mode 100644 index 00000000000..dad7732be6b --- /dev/null +++ b/ocaml/fstar-lib/FStar_Tuple3.ml @@ -0,0 +1,10 @@ +type ('a,'b,'c) tuple3 = + 'a* 'b* 'c +[@@deriving yojson,show] +let uu___is_Mktuple3 projectee = true +let __proj__Mktuple3__item___1 projectee = + match projectee with | (_1,_2,_3) -> _1 +let __proj__Mktuple3__item___2 projectee = + match projectee with | (_1,_2,_3) -> _2 +let __proj__Mktuple3__item___3 projectee = + match projectee with | (_1,_2,_3) -> _3 diff --git a/ocaml/fstar-lib/FStar_Tuple4.ml b/ocaml/fstar-lib/FStar_Tuple4.ml new file mode 100644 index 00000000000..1c43762d2c4 --- /dev/null +++ b/ocaml/fstar-lib/FStar_Tuple4.ml @@ -0,0 +1,12 @@ +type ('a,'b,'c,'d) tuple4 = + 'a* 'b* 'c* 'd +[@@deriving yojson,show] +let uu___is_Mktuple4 projectee = true +let __proj__Mktuple4__item___1 projectee = + match projectee with | (_1,_2,_3,_4) -> _1 +let __proj__Mktuple4__item___2 projectee = + match projectee with | (_1,_2,_3,_4) -> _2 +let __proj__Mktuple4__item___3 projectee = + match projectee with | (_1,_2,_3,_4) -> _3 +let __proj__Mktuple4__item___4 projectee = + match projectee with | (_1,_2,_3,_4) -> _4 diff --git a/ocaml/fstar-lib/FStar_Tuple5.ml b/ocaml/fstar-lib/FStar_Tuple5.ml new file mode 100644 index 00000000000..209b31ee4c1 --- /dev/null +++ b/ocaml/fstar-lib/FStar_Tuple5.ml @@ -0,0 +1,14 @@ +type ('a,'b,'c,'d,'e) tuple5 = + 'a* 'b* 'c* 'd* 'e +[@@deriving yojson,show] +let uu___is_Mktuple5 projectee = true +let __proj__Mktuple5__item___1 projectee = + match projectee with | (_1,_2,_3,_4,_5) -> _1 +let __proj__Mktuple5__item___2 projectee = + match projectee with | (_1,_2,_3,_4,_5) -> _2 +let __proj__Mktuple5__item___3 projectee = + match projectee with | (_1,_2,_3,_4,_5) -> _3 +let __proj__Mktuple5__item___4 projectee = + match projectee with | (_1,_2,_3,_4,_5) -> _4 +let __proj__Mktuple5__item___5 projectee = + match projectee with | (_1,_2,_3,_4,_5) -> _5 diff --git a/ocaml/fstar-lib/FStar_Tuple6.ml b/ocaml/fstar-lib/FStar_Tuple6.ml new file mode 100644 index 00000000000..bbbfae2e249 --- /dev/null +++ b/ocaml/fstar-lib/FStar_Tuple6.ml @@ -0,0 +1,16 @@ +type ('a,'b,'c,'d,'e,'f) tuple6 = + 'a* 'b* 'c* 'd* 'e* 'f +[@@deriving yojson,show] +let uu___is_Mktuple6 projectee = true +let __proj__Mktuple6__item___1 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6) -> _1 +let __proj__Mktuple6__item___2 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6) -> _2 +let __proj__Mktuple6__item___3 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6) -> _3 +let __proj__Mktuple6__item___4 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6) -> _4 +let __proj__Mktuple6__item___5 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6) -> _5 +let __proj__Mktuple6__item___6 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6) -> _6 diff --git a/ocaml/fstar-lib/FStar_Tuple7.ml b/ocaml/fstar-lib/FStar_Tuple7.ml new file mode 100644 index 00000000000..47941e1a2da --- /dev/null +++ b/ocaml/fstar-lib/FStar_Tuple7.ml @@ -0,0 +1,18 @@ +type ('a,'b,'c,'d,'e,'f,'g) tuple7 = + 'a* 'b* 'c* 'd* 'e* 'f* 'g +[@@deriving yojson,show] +let uu___is_Mktuple7 projectee = true +let __proj__Mktuple7__item___1 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7) -> _1 +let __proj__Mktuple7__item___2 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7) -> _2 +let __proj__Mktuple7__item___3 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7) -> _3 +let __proj__Mktuple7__item___4 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7) -> _4 +let __proj__Mktuple7__item___5 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7) -> _5 +let __proj__Mktuple7__item___6 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7) -> _6 +let __proj__Mktuple7__item___7 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7) -> _7 diff --git a/ocaml/fstar-lib/FStar_Tuple8.ml b/ocaml/fstar-lib/FStar_Tuple8.ml new file mode 100644 index 00000000000..5a8127fde30 --- /dev/null +++ b/ocaml/fstar-lib/FStar_Tuple8.ml @@ -0,0 +1,20 @@ +type ('a,'b,'c,'d,'e,'f,'g,'h) tuple8 = + 'a* 'b* 'c* 'd* 'e* 'f* 'g* 'h +[@@deriving yojson,show] +let uu___is_Mktuple8 projectee = true +let __proj__Mktuple8__item___1 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8) -> _1 +let __proj__Mktuple8__item___2 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8) -> _2 +let __proj__Mktuple8__item___3 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8) -> _3 +let __proj__Mktuple8__item___4 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8) -> _4 +let __proj__Mktuple8__item___5 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8) -> _5 +let __proj__Mktuple8__item___6 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8) -> _6 +let __proj__Mktuple8__item___7 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8) -> _7 +let __proj__Mktuple8__item___8 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8) -> _8 diff --git a/ocaml/fstar-lib/FStar_Tuple9.ml b/ocaml/fstar-lib/FStar_Tuple9.ml new file mode 100644 index 00000000000..c25b13d1260 --- /dev/null +++ b/ocaml/fstar-lib/FStar_Tuple9.ml @@ -0,0 +1,22 @@ +type ('a,'b,'c,'d,'e,'f,'g,'h,'i) tuple9 = + 'a *'b *'c *'d *'e *'f *'g *'h *'i +[@@deriving yojson,show] +let uu___is_Mktuple9 projectee = true +let __proj__Mktuple9__item___1 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9) -> _1 +let __proj__Mktuple9__item___2 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9) -> _2 +let __proj__Mktuple9__item___3 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9) -> _3 +let __proj__Mktuple9__item___4 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9) -> _4 +let __proj__Mktuple9__item___5 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9) -> _5 +let __proj__Mktuple9__item___6 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9) -> _6 +let __proj__Mktuple9__item___7 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9) -> _7 +let __proj__Mktuple9__item___8 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9) -> _8 +let __proj__Mktuple9__item___9 projectee = + match projectee with | (_1,_2,_3,_4,_5,_6,_7,_8,_9) -> _9 diff --git a/ulib/FStar.DTuple3.fsti b/ulib/FStar.DTuple3.fsti new file mode 100644 index 00000000000..4fad54c4440 --- /dev/null +++ b/ulib/FStar.DTuple3.fsti @@ -0,0 +1,6 @@ +module FStar.DTuple3 + +(** Dependent triples, with sugar [x:a & y:b x & c x y] *) +unopteq +type dtuple3 (a: Type) (b: (a -> GTot Type)) (c: (x: a -> b x -> GTot Type)) = + | Mkdtuple3 : _1: a -> _2: b _1 -> _3: c _1 _2 -> dtuple3 a b c diff --git a/ulib/FStar.DTuple4.fsti b/ulib/FStar.DTuple4.fsti new file mode 100644 index 00000000000..696eae5f5cc --- /dev/null +++ b/ulib/FStar.DTuple4.fsti @@ -0,0 +1,8 @@ +module FStar.DTuple4 + +(** Dependent quadruples, with sugar [x:a & y:b x & z:c x y & d x y z] *) +unopteq +type dtuple4 + (a: Type) (b: (x: a -> GTot Type)) (c: (x: a -> b x -> GTot Type)) + (d: (x: a -> y: b x -> z: c x y -> GTot Type)) + = | Mkdtuple4 : _1: a -> _2: b _1 -> _3: c _1 _2 -> _4: d _1 _2 _3 -> dtuple4 a b c d diff --git a/ulib/FStar.DTuple5.fsti b/ulib/FStar.DTuple5.fsti new file mode 100644 index 00000000000..01a82a8107e --- /dev/null +++ b/ulib/FStar.DTuple5.fsti @@ -0,0 +1,9 @@ +module FStar.DTuple5 + +(** Dependent quadruples, with sugar [x:a & y:b x & z:c x y & d x y z] *) +unopteq +type dtuple5 + (a: Type) (b: (x: a -> GTot Type)) (c: (x: a -> b x -> GTot Type)) + (d: (x: a -> y: b x -> z: c x y -> GTot Type)) + (e: (x: a -> y: b x -> z: c x y -> w: d x y z -> GTot Type)) + = | Mkdtuple5 : _1: a -> _2: b _1 -> _3: c _1 _2 -> _4: d _1 _2 _3 -> _5: e _1 _2 _3 _4 -> dtuple5 a b c d e diff --git a/ulib/FStar.Pervasives.Native.fst b/ulib/FStar.Pervasives.Native.fst index f6db654977b..2caa33c739d 100644 --- a/ulib/FStar.Pervasives.Native.fst +++ b/ulib/FStar.Pervasives.Native.fst @@ -61,115 +61,3 @@ type tuple2 'a 'b = | Mktuple2 : _1: 'a -> _2: 'b -> tuple2 'a 'b (** The fst and snd projections on pairs are very common *) let fst (x: tuple2 'a 'b) : 'a = Mktuple2?._1 x let snd (x: tuple2 'a 'b) : 'b = Mktuple2?._2 x - -type tuple3 'a 'b 'c = | Mktuple3 : _1: 'a -> _2: 'b -> _3: 'c -> tuple3 'a 'b 'c - -type tuple4 'a 'b 'c 'd = | Mktuple4 : _1: 'a -> _2: 'b -> _3: 'c -> _4: 'd -> tuple4 'a 'b 'c 'd - -type tuple5 'a 'b 'c 'd 'e = - | Mktuple5 : _1: 'a -> _2: 'b -> _3: 'c -> _4: 'd -> _5: 'e -> tuple5 'a 'b 'c 'd 'e - -type tuple6 'a 'b 'c 'd 'e 'f = - | Mktuple6 : _1: 'a -> _2: 'b -> _3: 'c -> _4: 'd -> _5: 'e -> _6: 'f -> tuple6 'a 'b 'c 'd 'e 'f - -type tuple7 'a 'b 'c 'd 'e 'f 'g = - | Mktuple7 : _1: 'a -> _2: 'b -> _3: 'c -> _4: 'd -> _5: 'e -> _6: 'f -> _7: 'g - -> tuple7 'a 'b 'c 'd 'e 'f 'g - -type tuple8 'a 'b 'c 'd 'e 'f 'g 'h = - | Mktuple8 : _1: 'a -> _2: 'b -> _3: 'c -> _4: 'd -> _5: 'e -> _6: 'f -> _7: 'g -> _8: 'h - -> tuple8 'a 'b 'c 'd 'e 'f 'g 'h - -type tuple9 'a 'b 'c 'd 'e 'f 'g 'h 'i = - | Mktuple9 : - _1: 'a -> - _2: 'b -> - _3: 'c -> - _4: 'd -> - _5: 'e -> - _6: 'f -> - _7: 'g -> - _8: 'h -> - _9: 'i - -> tuple9 'a 'b 'c 'd 'e 'f 'g 'h 'i - -type tuple10 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j = - | Mktuple10 : - _1: 'a -> - _2: 'b -> - _3: 'c -> - _4: 'd -> - _5: 'e -> - _6: 'f -> - _7: 'g -> - _8: 'h -> - _9: 'i -> - _10: 'j - -> tuple10 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j - -type tuple11 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k = - | Mktuple11 : - _1: 'a -> - _2: 'b -> - _3: 'c -> - _4: 'd -> - _5: 'e -> - _6: 'f -> - _7: 'g -> - _8: 'h -> - _9: 'i -> - _10: 'j -> - _11: 'k - -> tuple11 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k - -type tuple12 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k 'l = - | Mktuple12 : - _1: 'a -> - _2: 'b -> - _3: 'c -> - _4: 'd -> - _5: 'e -> - _6: 'f -> - _7: 'g -> - _8: 'h -> - _9: 'i -> - _10: 'j -> - _11: 'k -> - _12: 'l - -> tuple12 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k 'l - -type tuple13 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k 'l 'm = - | Mktuple13 : - _1: 'a -> - _2: 'b -> - _3: 'c -> - _4: 'd -> - _5: 'e -> - _6: 'f -> - _7: 'g -> - _8: 'h -> - _9: 'i -> - _10: 'j -> - _11: 'k -> - _12: 'l -> - _13: 'm - -> tuple13 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k 'l 'm - -type tuple14 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k 'l 'm 'n = - | Mktuple14 : - _1: 'a -> - _2: 'b -> - _3: 'c -> - _4: 'd -> - _5: 'e -> - _6: 'f -> - _7: 'g -> - _8: 'h -> - _9: 'i -> - _10: 'j -> - _11: 'k -> - _12: 'l -> - _13: 'm -> - _14: 'n - -> tuple14 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k 'l 'm 'n - diff --git a/ulib/FStar.Pervasives.fsti b/ulib/FStar.Pervasives.fsti index 6bb8b1076a3..bf43b175152 100644 --- a/ulib/FStar.Pervasives.fsti +++ b/ulib/FStar.Pervasives.fsti @@ -739,26 +739,6 @@ let dsnd (#a: Type) (#b: a -> GTot Type) (t: dtuple2 a b) : Tot (b (Mkdtuple2?._1 t)) = Mkdtuple2?._2 t -(** Dependent triples, with sugar [x:a & y:b x & c x y] *) -unopteq -type dtuple3 (a: Type) (b: (a -> GTot Type)) (c: (x: a -> b x -> GTot Type)) = - | Mkdtuple3 : _1: a -> _2: b _1 -> _3: c _1 _2 -> dtuple3 a b c - -(** Dependent quadruples, with sugar [x:a & y:b x & z:c x y & d x y z] *) -unopteq -type dtuple4 - (a: Type) (b: (x: a -> GTot Type)) (c: (x: a -> b x -> GTot Type)) - (d: (x: a -> y: b x -> z: c x y -> GTot Type)) - = | Mkdtuple4 : _1: a -> _2: b _1 -> _3: c _1 _2 -> _4: d _1 _2 _3 -> dtuple4 a b c d - -(** Dependent quadruples, with sugar [x:a & y:b x & z:c x y & d x y z] *) -unopteq -type dtuple5 - (a: Type) (b: (x: a -> GTot Type)) (c: (x: a -> b x -> GTot Type)) - (d: (x: a -> y: b x -> z: c x y -> GTot Type)) - (e: (x: a -> y: b x -> z: c x y -> w: d x y z -> GTot Type)) - = | Mkdtuple5 : _1: a -> _2: b _1 -> _3: c _1 _2 -> _4: d _1 _2 _3 -> _5: e _1 _2 _3 _4 -> dtuple5 a b c d e - (** Explicitly discarding a value *) let ignore (#a: Type) (x: a) : Tot unit = () diff --git a/ulib/FStar.Tuple10.fsti b/ulib/FStar.Tuple10.fsti new file mode 100644 index 00000000000..594d5a33f67 --- /dev/null +++ b/ulib/FStar.Tuple10.fsti @@ -0,0 +1,30 @@ +(* + Copyright 2008-2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) +module FStar.Tuple10 + +type tuple10 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j = + | Mktuple10 : + _1: 'a -> + _2: 'b -> + _3: 'c -> + _4: 'd -> + _5: 'e -> + _6: 'f -> + _7: 'g -> + _8: 'h -> + _9: 'i -> + _10: 'j + -> tuple10 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j diff --git a/ulib/FStar.Tuple11.fsti b/ulib/FStar.Tuple11.fsti new file mode 100644 index 00000000000..a8f0e323bfb --- /dev/null +++ b/ulib/FStar.Tuple11.fsti @@ -0,0 +1,31 @@ +(* + Copyright 2008-2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) +module FStar.Tuple11 + +type tuple11 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k = + | Mktuple11 : + _1: 'a -> + _2: 'b -> + _3: 'c -> + _4: 'd -> + _5: 'e -> + _6: 'f -> + _7: 'g -> + _8: 'h -> + _9: 'i -> + _10: 'j -> + _11: 'k + -> tuple11 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k diff --git a/ulib/FStar.Tuple12.fsti b/ulib/FStar.Tuple12.fsti new file mode 100644 index 00000000000..6e63e3ac72c --- /dev/null +++ b/ulib/FStar.Tuple12.fsti @@ -0,0 +1,32 @@ +(* + Copyright 2008-2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) +module FStar.Tuple12 + +type tuple12 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k 'l = + | Mktuple12 : + _1: 'a -> + _2: 'b -> + _3: 'c -> + _4: 'd -> + _5: 'e -> + _6: 'f -> + _7: 'g -> + _8: 'h -> + _9: 'i -> + _10: 'j -> + _11: 'k -> + _12: 'l + -> tuple12 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k 'l diff --git a/ulib/FStar.Tuple13.fsti b/ulib/FStar.Tuple13.fsti new file mode 100644 index 00000000000..72d0d223c22 --- /dev/null +++ b/ulib/FStar.Tuple13.fsti @@ -0,0 +1,33 @@ +(* + Copyright 2008-2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) +module FStar.Tuple13 + +type tuple13 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k 'l 'm = + | Mktuple13 : + _1: 'a -> + _2: 'b -> + _3: 'c -> + _4: 'd -> + _5: 'e -> + _6: 'f -> + _7: 'g -> + _8: 'h -> + _9: 'i -> + _10: 'j -> + _11: 'k -> + _12: 'l -> + _13: 'm + -> tuple13 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k 'l 'm diff --git a/ulib/FStar.Tuple14.fsti b/ulib/FStar.Tuple14.fsti new file mode 100644 index 00000000000..0b734d4da89 --- /dev/null +++ b/ulib/FStar.Tuple14.fsti @@ -0,0 +1,34 @@ +(* + Copyright 2008-2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) +module FStar.Tuple14 + +type tuple14 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k 'l 'm 'n = + | Mktuple14 : + _1: 'a -> + _2: 'b -> + _3: 'c -> + _4: 'd -> + _5: 'e -> + _6: 'f -> + _7: 'g -> + _8: 'h -> + _9: 'i -> + _10: 'j -> + _11: 'k -> + _12: 'l -> + _13: 'm -> + _14: 'n + -> tuple14 'a 'b 'c 'd 'e 'f 'g 'h 'i 'j 'k 'l 'm 'n diff --git a/ulib/FStar.Tuple3.fsti b/ulib/FStar.Tuple3.fsti new file mode 100644 index 00000000000..0c4b37dad42 --- /dev/null +++ b/ulib/FStar.Tuple3.fsti @@ -0,0 +1,19 @@ +(* + Copyright 2008-2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) +module FStar.Tuple3 + +type tuple3 'a 'b 'c = + | Mktuple3 : _1: 'a -> _2: 'b -> _3: 'c -> tuple3 'a 'b 'c diff --git a/ulib/FStar.Tuple4.fsti b/ulib/FStar.Tuple4.fsti new file mode 100644 index 00000000000..83c32990213 --- /dev/null +++ b/ulib/FStar.Tuple4.fsti @@ -0,0 +1,19 @@ +(* + Copyright 2008-2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) +module FStar.Tuple4 + +type tuple4 'a 'b 'c 'd = + | Mktuple4 : _1: 'a -> _2: 'b -> _3: 'c -> _4: 'd -> tuple4 'a 'b 'c 'd diff --git a/ulib/FStar.Tuple5.fsti b/ulib/FStar.Tuple5.fsti new file mode 100644 index 00000000000..1d5e4c4f125 --- /dev/null +++ b/ulib/FStar.Tuple5.fsti @@ -0,0 +1,19 @@ +(* + Copyright 2008-2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) +module FStar.Tuple5 + +type tuple5 'a 'b 'c 'd 'e = + | Mktuple5 : _1: 'a -> _2: 'b -> _3: 'c -> _4: 'd -> _5: 'e -> tuple5 'a 'b 'c 'd 'e diff --git a/ulib/FStar.Tuple6.fsti b/ulib/FStar.Tuple6.fsti new file mode 100644 index 00000000000..aca3c3349ad --- /dev/null +++ b/ulib/FStar.Tuple6.fsti @@ -0,0 +1,19 @@ +(* + Copyright 2008-2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) +module FStar.Tuple6 + +type tuple6 'a 'b 'c 'd 'e 'f = + | Mktuple6 : _1: 'a -> _2: 'b -> _3: 'c -> _4: 'd -> _5: 'e -> _6: 'f -> tuple6 'a 'b 'c 'd 'e 'f diff --git a/ulib/FStar.Tuple7.fsti b/ulib/FStar.Tuple7.fsti new file mode 100644 index 00000000000..20d2cc463e2 --- /dev/null +++ b/ulib/FStar.Tuple7.fsti @@ -0,0 +1,20 @@ +(* + Copyright 2008-2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) +module FStar.Tuple7 + +type tuple7 'a 'b 'c 'd 'e 'f 'g = + | Mktuple7 : _1: 'a -> _2: 'b -> _3: 'c -> _4: 'd -> _5: 'e -> _6: 'f -> _7: 'g + -> tuple7 'a 'b 'c 'd 'e 'f 'g diff --git a/ulib/FStar.Tuple8.fsti b/ulib/FStar.Tuple8.fsti new file mode 100644 index 00000000000..2c2cabc641f --- /dev/null +++ b/ulib/FStar.Tuple8.fsti @@ -0,0 +1,20 @@ +(* + Copyright 2008-2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) +module FStar.Tuple8 + +type tuple8 'a 'b 'c 'd 'e 'f 'g 'h = + | Mktuple8 : _1: 'a -> _2: 'b -> _3: 'c -> _4: 'd -> _5: 'e -> _6: 'f -> _7: 'g -> _8: 'h + -> tuple8 'a 'b 'c 'd 'e 'f 'g 'h diff --git a/ulib/FStar.Tuple9.fsti b/ulib/FStar.Tuple9.fsti new file mode 100644 index 00000000000..f1f6ce7a9c1 --- /dev/null +++ b/ulib/FStar.Tuple9.fsti @@ -0,0 +1,29 @@ +(* + Copyright 2008-2024 Microsoft Research + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. +*) +module FStar.Tuple9 + +type tuple9 'a 'b 'c 'd 'e 'f 'g 'h 'i = + | Mktuple9 : + _1: 'a -> + _2: 'b -> + _3: 'c -> + _4: 'd -> + _5: 'e -> + _6: 'f -> + _7: 'g -> + _8: 'h -> + _9: 'i + -> tuple9 'a 'b 'c 'd 'e 'f 'g 'h 'i From 067f87dc47c0fd4dbb0ed1768a4d108d5b1522fb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 5 Feb 2024 16:34:42 -0800 Subject: [PATCH 2/6] Fixing compiler for new tuples --- src/basic/FStar.Compiler.List.fsti | 2 + src/basic/FStar.Compiler.Util.fsti | 1 + src/basic/FStar.Errors.Codes.fsti | 2 + src/basic/FStar.Getopt.fsti | 2 + src/basic/FStar.Options.fsti | 2 + src/class/FStar.Class.Deq.fsti | 5 ++ src/class/FStar.Class.PP.fsti | 5 ++ src/parser/FStar.Parser.Const.fst | 65 ++++++++++++++++--- src/parser/FStar.Parser.Dep.fst | 58 ++++++++++++----- src/syntax/FStar.Syntax.Util.fst | 1 + src/syntax/FStar.Syntax.VisitM.fst | 1 + src/tosyntax/FStar.ToSyntax.ToSyntax.fst | 31 ++++----- .../FStar.TypeChecker.Normalize.fst | 2 +- src/typechecker/FStar.TypeChecker.TcTerm.fsti | 2 + 14 files changed, 135 insertions(+), 44 deletions(-) diff --git a/src/basic/FStar.Compiler.List.fsti b/src/basic/FStar.Compiler.List.fsti index 957872d8690..d1b95156bf8 100644 --- a/src/basic/FStar.Compiler.List.fsti +++ b/src/basic/FStar.Compiler.List.fsti @@ -17,6 +17,8 @@ module FStar.Compiler.List open FStar.Compiler.Effect open Prims +open FStar.Tuple3 + val isEmpty : (list 'a) -> Tot bool val singleton : 'a -> list 'a val hd : (list 'a) -> 'a diff --git a/src/basic/FStar.Compiler.Util.fsti b/src/basic/FStar.Compiler.Util.fsti index 3221954c332..0b0108e1132 100644 --- a/src/basic/FStar.Compiler.Util.fsti +++ b/src/basic/FStar.Compiler.Util.fsti @@ -20,6 +20,7 @@ open FStar.Compiler.Effect open FStar.Json open FStar.BaseTypes +open FStar.Tuple3 exception Impos val max_int: int diff --git a/src/basic/FStar.Errors.Codes.fsti b/src/basic/FStar.Errors.Codes.fsti index f78128c5c07..daeba694707 100644 --- a/src/basic/FStar.Errors.Codes.fsti +++ b/src/basic/FStar.Errors.Codes.fsti @@ -393,3 +393,5 @@ type error_code = type error_setting = error_code & error_flag & int val default_settings : list error_setting + +module X = FStar.Tuple3 // stupid hack diff --git a/src/basic/FStar.Getopt.fsti b/src/basic/FStar.Getopt.fsti index a3a2310547a..6d1cc50f0e2 100644 --- a/src/basic/FStar.Getopt.fsti +++ b/src/basic/FStar.Getopt.fsti @@ -17,6 +17,8 @@ module FStar.Getopt open FStar.Compiler.Effect open FStar.BaseTypes +open FStar.Tuple3 + val noshort : char val nolong : string type opt_variant 'a = diff --git a/src/basic/FStar.Options.fsti b/src/basic/FStar.Options.fsti index b7ca1a60a36..5523430d8e9 100644 --- a/src/basic/FStar.Options.fsti +++ b/src/basic/FStar.Options.fsti @@ -24,6 +24,8 @@ open FStar.Compiler type codegen_t = | OCaml | FSharp | Krml | Plugin | Extension +open FStar.Tuple4 + //let __test_norm_all = Util.mk_ref false type split_queries_t = | No | OnFailure | Always diff --git a/src/class/FStar.Class.Deq.fsti b/src/class/FStar.Class.Deq.fsti index ae28930caac..4ef01c943a6 100644 --- a/src/class/FStar.Class.Deq.fsti +++ b/src/class/FStar.Class.Deq.fsti @@ -2,6 +2,11 @@ module FStar.Class.Deq open FStar.Compiler.Effect +open FStar.Tuple3 +open FStar.Tuple4 +open FStar.Tuple5 +open FStar.Tuple6 + class deq (a:Type) = { (=?) : a -> a -> bool; } diff --git a/src/class/FStar.Class.PP.fsti b/src/class/FStar.Class.PP.fsti index cbeccc496e9..bd620ffa524 100644 --- a/src/class/FStar.Class.PP.fsti +++ b/src/class/FStar.Class.PP.fsti @@ -3,6 +3,11 @@ module FStar.Class.PP open FStar.Compiler.Effect open FStar.Pprint +open FStar.Tuple3 +open FStar.Tuple4 +open FStar.Tuple5 +open FStar.Tuple6 + class pretty (a:Type) = { pp : a -> ML document; } diff --git a/src/parser/FStar.Parser.Const.fst b/src/parser/FStar.Parser.Const.fst index 78b759519c3..43613a656f9 100644 --- a/src/parser/FStar.Parser.Const.fst +++ b/src/parser/FStar.Parser.Const.fst @@ -429,8 +429,14 @@ let const_to_string x = match x with (* Tuples *) let mk_tuple_lid n r = - let t = U.format1 "tuple%s" (U.string_of_int n) in - set_lid_range (psnconst t) r + let l = + if n = 2 then + Ident.lid_of_str "FStar.Pervasives.Native.tuple2" + else + let s = U.format2 "FStar.Tuple%s.tuple%s" (U.string_of_int n) (U.string_of_int n) in + Ident.lid_of_str s + in + set_lid_range l r let lid_tuple2 = mk_tuple_lid 2 dummyRange let lid_tuple3 = mk_tuple_lid 3 dummyRange @@ -438,14 +444,32 @@ let lid_tuple4 = mk_tuple_lid 4 dummyRange let lid_tuple5 = mk_tuple_lid 5 dummyRange let is_tuple_constructor_string (s:string) :bool = - U.starts_with s "FStar.Pervasives.Native.tuple" + s = "FStar.Pervasives.Native.tuple2" || + s = "FStar.Tuple3.tuple3" || + s = "FStar.Tuple4.tuple4" || + s = "FStar.Tuple5.tuple5" || + s = "FStar.Tuple6.tuple6" || + s = "FStar.Tuple7.tuple7" || + s = "FStar.Tuple8.tuple8" || + s = "FStar.Tuple9.tuple9" || + s = "FStar.Tuple10.tuple10" || + s = "FStar.Tuple11.tuple11" || + s = "FStar.Tuple12.tuple12" || + s = "FStar.Tuple13.tuple13" || + s = "FStar.Tuple14.tuple14" let is_tuple_constructor_id id = is_tuple_constructor_string (string_of_id id) let is_tuple_constructor_lid lid = is_tuple_constructor_string (string_of_lid lid) let mk_tuple_data_lid n r = - let t = U.format1 "Mktuple%s" (U.string_of_int n) in - set_lid_range (psnconst t) r + let l = + if n = 2 then + Ident.lid_of_str "FStar.Pervasives.Native.Mktuple2" + else + let s = U.format2 "FStar.Tuple%s.Mktuple%s" (U.string_of_int n) (U.string_of_int n) in + Ident.lid_of_str s + in + set_lid_range l r let lid_Mktuple2 = mk_tuple_data_lid 2 dummyRange let lid_Mktuple3 = mk_tuple_data_lid 3 dummyRange @@ -453,7 +477,19 @@ let lid_Mktuple4 = mk_tuple_data_lid 4 dummyRange let lid_Mktuple5 = mk_tuple_data_lid 5 dummyRange let is_tuple_datacon_string (s:string) :bool = - U.starts_with s "FStar.Pervasives.Native.Mktuple" + s = "FStar.Pervasives.Native.Mktuple2" || + s = "FStar.Tuple3.Mktuple3" || + s = "FStar.Tuple4.Mktuple4" || + s = "FStar.Tuple5.Mktuple5" || + s = "FStar.Tuple6.Mktuple6" || + s = "FStar.Tuple7.Mktuple7" || + s = "FStar.Tuple8.Mktuple8" || + s = "FStar.Tuple9.Mktuple9" || + s = "FStar.Tuple10.Mktuple10" || + s = "FStar.Tuple11.Mktuple11" || + s = "FStar.Tuple12.Mktuple12" || + s = "FStar.Tuple13.Mktuple13" || + s = "FStar.Tuple14.Mktuple14" let is_tuple_datacon_id id = is_tuple_datacon_string (string_of_id id) let is_tuple_datacon_lid lid = is_tuple_datacon_string (string_of_lid lid) @@ -467,15 +503,21 @@ let is_tuple_data_lid' f = is_tuple_datacon_string (string_of_lid f) (* Dtuples *) (* dtuple is defined in prims if n = 2, in pervasives otherwise *) -let mod_prefix_dtuple (n:int) :(string -> lident) = - if n = 2 then pconst else psconst +let mod_prefix_dtuple (n:int) : (string -> lident) = + fun s -> + if n = 2 + then pconst s + else lid_of_path ["FStar"; "DTuple" ^ string_of_int n; s] dummyRange let mk_dtuple_lid n r = let t = U.format1 "dtuple%s" (U.string_of_int n) in set_lid_range ((mod_prefix_dtuple n) t) r let is_dtuple_constructor_string (s:string) :bool = - s = "Prims.dtuple2" || U.starts_with s "FStar.Pervasives.dtuple" + s = "Prims.dtuple2" || + s = "FStar.DTuple3.dtuple3" || + s = "FStar.DTuple4.dtuple4" || + s = "FStar.DTuple5.dtuple5" let is_dtuple_constructor_lid lid = is_dtuple_constructor_string (string_of_lid lid) @@ -484,7 +526,10 @@ let mk_dtuple_data_lid n r = set_lid_range ((mod_prefix_dtuple n) t) r let is_dtuple_datacon_string (s:string) :bool = - s = "Prims.Mkdtuple2" || U.starts_with s "FStar.Pervasives.Mkdtuple" + s = "Prims.Mkdtuple2" || + s = "FStar.DTuple3.Mkdtuple3" || + s = "FStar.DTuple4.Mkdtuple4" || + s = "FStar.DTuple5.Mkdtuple5" let is_dtuple_data_lid f n = lid_equals f (mk_dtuple_data_lid n dummyRange) diff --git a/src/parser/FStar.Parser.Dep.fst b/src/parser/FStar.Parser.Dep.fst index f1735a0b45d..35b9e6d0293 100644 --- a/src/parser/FStar.Parser.Dep.fst +++ b/src/parser/FStar.Parser.Dep.fst @@ -806,6 +806,10 @@ let collect_one then pd := elt::!pd in + let add_module m = + add_to_parsing_data (P_dep (false, (Ident.lid_of_str m))) + in + let rec collect_module = function | Module (lid, decls) | Interface (lid, decls, _) -> @@ -896,7 +900,7 @@ let collect_one | VpOfNotation t | VpArbitrary t -> collect_term t | VpRecord (record, t) -> collect_tycon_record record; iter_opt t collect_term - ) (List.filter_map Mktuple3?._2 identterms) + ) (List.filter_map Tuple3.Mktuple3?._2 identterms) and collect_tycon_record r = List.iter (fun (_, aq, attrs, t) -> @@ -931,6 +935,15 @@ let collect_one | _ -> () and collect_term t = + let rec tdepth (t:term) : int = + match t.tm with + | Op (id, [_; r]) when string_of_id id = "*" || string_of_id id = "&" -> + 1 + tdepth r + | _ -> 1 + in + let d = tdepth t in + if tdepth t > 1 then + add_module ("FStar.Tuple" ^ string_of_int d); collect_term' t.tm and collect_constant = function @@ -955,7 +968,7 @@ let collect_one () | Const c -> collect_constant c - | Op (_, ts) -> + | Op (op, ts) -> List.iter collect_term ts | Tvar _ | AST.Uvar _ -> @@ -1039,6 +1052,13 @@ let collect_one collect_binders binders; collect_term t | Sum (binders, t) -> + let sn = string_of_int (1 + List.length binders) in + let is_dep = + not <| List.for_all (function | Inr _ -> true | _ -> false) binders + in + if is_dep + then add_module ("FStar.DTuple" ^ sn) + else add_module ("FStar.Tuple" ^ sn); List.iter (function | Inl b -> collect_binder b | Inr t -> collect_term t) @@ -1063,7 +1083,7 @@ let collect_one collect_term t | LexList l -> List.iter collect_term l | WFOrder (t1, t2) -> - add_to_parsing_data (P_dep (false, (Ident.lid_of_str "FStar.WellFounded"))); + add_module "FStar.WellFounded"; begin collect_term t1; collect_term t2 end @@ -1075,7 +1095,7 @@ let collect_one | Attributes cattributes -> List.iter collect_term cattributes | CalcProof (rel, init, steps) -> - add_to_parsing_data (P_dep (false, (Ident.lid_of_str "FStar.Calc"))); + add_module "FStar.Calc"; begin collect_term rel; collect_term init; @@ -1086,46 +1106,46 @@ let collect_one end | IntroForall (bs, p, e) -> - add_to_parsing_data (P_dep (false, (Ident.lid_of_str "FStar.Classical.Sugar"))); + add_module "FStar.Classical.Sugar"; collect_binders bs; collect_term p; collect_term e | IntroExists(bs, t, vs, e) -> - add_to_parsing_data (P_dep (false, (Ident.lid_of_str "FStar.Classical.Sugar"))); + add_module "FStar.Classical.Sugar"; collect_binders bs; collect_term t; List.iter collect_term vs; collect_term e | IntroImplies(p, q, x, e) -> - add_to_parsing_data (P_dep (false, (Ident.lid_of_str "FStar.Classical.Sugar"))); + add_module "FStar.Classical.Sugar"; collect_term p; collect_term q; collect_binder x; collect_term e | IntroOr(b, p, q, r) -> - add_to_parsing_data (P_dep (false, (Ident.lid_of_str "FStar.Classical.Sugar"))); + add_module "FStar.Classical.Sugar"; collect_term p; collect_term q; collect_term r | IntroAnd(p, q, r, e) -> - add_to_parsing_data (P_dep (false, (Ident.lid_of_str "FStar.Classical.Sugar"))); + add_module "FStar.Classical.Sugar"; collect_term p; collect_term q; collect_term r; collect_term e | ElimForall(bs, p, vs) -> - add_to_parsing_data (P_dep (false, (Ident.lid_of_str "FStar.Classical.Sugar"))); + add_module "FStar.Classical.Sugar"; collect_binders bs; collect_term p; List.iter collect_term vs | ElimExists(bs, p, q, b, e) -> - add_to_parsing_data (P_dep (false, (Ident.lid_of_str "FStar.Classical.Sugar"))); + add_module "FStar.Classical.Sugar"; collect_binders bs; collect_term p; collect_term q; @@ -1133,13 +1153,13 @@ let collect_one collect_term e | ElimImplies(p, q, e) -> - add_to_parsing_data (P_dep (false, (Ident.lid_of_str "FStar.Classical.Sugar"))); + add_module "FStar.Classical.Sugar"; collect_term p; collect_term q; collect_term e | ElimAnd(p, q, r, x, y, e) -> - add_to_parsing_data (P_dep (false, (Ident.lid_of_str "FStar.Classical.Sugar"))); + add_module "FStar.Classical.Sugar"; collect_term p; collect_term q; collect_term r; @@ -1148,7 +1168,7 @@ let collect_one collect_term e | ElimOr(p, q, r, x, e, y, e') -> - add_to_parsing_data (P_dep (false, (Ident.lid_of_str "FStar.Classical.Sugar"))); + add_module "FStar.Classical.Sugar"; collect_term p; collect_term q; collect_term r; @@ -1188,8 +1208,14 @@ let collect_one | PatName _ -> () | PatList ps - | PatOr ps - | PatTuple (ps, _) -> + | PatOr ps -> + collect_patterns ps + + | PatTuple (ps, is_dep) -> + let sn = string_of_int (List.length ps) in + if is_dep + then add_module ("FStar.DTuple" ^ sn) + else add_module ("FStar.Tuple" ^ sn); collect_patterns ps | PatRecord lidpats -> List.iter (fun (_, p) -> collect_pattern p) lidpats diff --git a/src/syntax/FStar.Syntax.Util.fst b/src/syntax/FStar.Syntax.Util.fst index 85c56cda831..8c2ea19d530 100644 --- a/src/syntax/FStar.Syntax.Util.fst +++ b/src/syntax/FStar.Syntax.Util.fst @@ -31,6 +31,7 @@ open FStar.Dyn module U = FStar.Compiler.Util module List = FStar.Compiler.List module PC = FStar.Parser.Const +open FStar.Tuple3 open FStar.Class.Show open FStar.Class.Monad diff --git a/src/syntax/FStar.Syntax.VisitM.fst b/src/syntax/FStar.Syntax.VisitM.fst index ab125b3234d..5eae09742c7 100644 --- a/src/syntax/FStar.Syntax.VisitM.fst +++ b/src/syntax/FStar.Syntax.VisitM.fst @@ -8,6 +8,7 @@ open FStar.Class.Monad open FStar.Syntax open FStar.Syntax.Syntax +open FStar.Tuple3 type endo (m:Type -> Type) a = a -> m a diff --git a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst index 3eea02ba793..5771573715e 100644 --- a/src/tosyntax/FStar.ToSyntax.ToSyntax.fst +++ b/src/tosyntax/FStar.ToSyntax.ToSyntax.fst @@ -1190,7 +1190,7 @@ and desugar_term_maybe_top (top_level:bool) (env:env_t) (top:term) : S.term & an | Op(op_star, [lhs;rhs]) when (Ident.string_of_id op_star = "*" && op_as_term env 2 op_star |> Option.isNone) -> - (* See the comment in parse.mly to understand why this implicitly relies + (* See the comment in FStar_Parser_Parse.mly to understand why this implicitly relies * on the presence of a Paren node in the AST. *) let rec flatten t = match t.tm with // * is left-associative @@ -1445,8 +1445,14 @@ and desugar_term_maybe_top (top_level:bool) (env:env_t) (top:term) : S.term & an is desugared to - fun y1 y2 y3 -> match (y1, y2, y3) with - | (P1 x1, P2 x2, P3 x3) -> [[e]] + fun y1 y2 y3 -> + match y1 with P1 x1 -> + match y2 with P2 x2 -> + match y3 with P3 x3 -> + [[e]] + + The nested matches allow us to not use any tuples, which + must be loaded from FStar.TupleX. (FIXME: not true, nested pairs now) *) let rec aux aqs env bs sc_pat_opt pats : S.term & antiquotations_temp = match pats with @@ -1480,20 +1486,11 @@ and desugar_term_maybe_top (top_level:bool) (env:env_t) (top:term) : S.term & an | None, _ -> sc_pat_opt | Some p, None -> Some (S.bv_to_name x, p) | Some p, Some (sc, p') -> begin - match sc.n, p'.v with - | Tm_name _, _ -> - let tup2 = S.lid_and_dd_as_fv (C.mk_tuple_data_lid 2 top.range) (Some Data_ctor) in - let sc = S.mk (Tm_app {hd=mk (Tm_fvar tup2); - args=[as_arg sc; as_arg <| S.bv_to_name x]}) top.range in - let p = withinfo (Pat_cons(tup2, None, [(p', false);(p, false)])) (Range.union_ranges p'.p p.p) in - Some(sc, p) - | Tm_app {args}, Pat_cons(_, _, pats) -> - let tupn = S.lid_and_dd_as_fv (C.mk_tuple_data_lid (1 + List.length args) top.range) (Some Data_ctor) in - let sc = mk (Tm_app {hd=mk (Tm_fvar tupn); - args=args@[as_arg <| S.bv_to_name x]}) in - let p = withinfo (Pat_cons(tupn, None, pats@[(p, false)])) (Range.union_ranges p'.p p.p) in - Some(sc, p) - | _ -> failwith "Impossible" + let tup2 = S.lid_and_dd_as_fv (C.mk_tuple_data_lid 2 top.range) (Some Data_ctor) in + let sc = S.mk (Tm_app {hd=mk (Tm_fvar tup2); + args=[as_arg sc; as_arg <| S.bv_to_name x]}) top.range in + let p = withinfo (Pat_cons(tup2, None, [(p', false);(p, false)])) (Range.union_ranges p'.p p.p) in + Some(sc, p) end in (mk_binder_with_attrs x aq attrs), sc_pat_opt diff --git a/src/typechecker/FStar.TypeChecker.Normalize.fst b/src/typechecker/FStar.TypeChecker.Normalize.fst index b277bffa941..a3b37f7ca10 100644 --- a/src/typechecker/FStar.TypeChecker.Normalize.fst +++ b/src/typechecker/FStar.TypeChecker.Normalize.fst @@ -3033,7 +3033,7 @@ let elim_uvars_aux_c env univ_names binders c = univ_names, binders, BU.right tc let rec elim_uvars (env:Env.env) (s:sigelt) = - let sigattrs = List.map Mktuple3?._3 <| List.map (elim_uvars_aux_t env [] []) s.sigattrs in + let sigattrs = List.map Tuple3.Mktuple3?._3 <| List.map (elim_uvars_aux_t env [] []) s.sigattrs in let s = { s with sigattrs } in match s.sigel with | Sig_inductive_typ {lid; us=univ_names; params=binders; diff --git a/src/typechecker/FStar.TypeChecker.TcTerm.fsti b/src/typechecker/FStar.TypeChecker.TcTerm.fsti index 9145f8380f6..b1720c6bb9a 100644 --- a/src/typechecker/FStar.TypeChecker.TcTerm.fsti +++ b/src/typechecker/FStar.TypeChecker.TcTerm.fsti @@ -31,6 +31,8 @@ open FStar.Const open FStar.TypeChecker.Rel open FStar.TypeChecker.Common +open FStar.Tuple8 + val level_of_type: env -> term -> typ -> universe //the term argument is for error reporting only val tc_constant: env -> FStar.Compiler.Range.range -> sconst -> typ val tc_binders: env -> binders -> binders & env & guard_t & universes From 357b0c35cd02a0e87c1c3a863a0d22f569674cd8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 5 Feb 2024 16:35:15 -0800 Subject: [PATCH 3/6] Fix library --- ulib/FStar.Class.Printable.fst | 10 +++++----- ulib/FStar.Stubs.Reflection.Types.fsti | 2 ++ ulib/FStar.UInt128.fst | 4 ++-- ulib/LowStar.BufferView.Down.fsti | 2 ++ ulib/LowStar.BufferView.fsti | 2 ++ ulib/LowStar.Printf.fst | 2 +- 6 files changed, 14 insertions(+), 8 deletions(-) diff --git a/ulib/FStar.Class.Printable.fst b/ulib/FStar.Class.Printable.fst index 8f781012915..8d7aba6a483 100644 --- a/ulib/FStar.Class.Printable.fst +++ b/ulib/FStar.Class.Printable.fst @@ -164,7 +164,7 @@ instance printable_tuple2 #a #b {| printable a |} {| printable b |} : printable instance printable_tuple3 #t0 #t1 #t2 {| printable t0 |} {| printable t1 |} {| printable t2 |} -: printable (tuple3 t0 t1 t2) = +: printable (Tuple3.tuple3 t0 t1 t2) = { to_string = (fun (v0,v1,v2) -> @@ -177,7 +177,7 @@ instance printable_tuple3 instance printable_tuple4 #t0 #t1 #t2 #t3 {| printable t0 |} {| printable t1 |} {| printable t2 |} {| printable t3 |} -: printable (tuple4 t0 t1 t2 t3) = +: printable (Tuple4.tuple4 t0 t1 t2 t3) = { to_string = (fun (v0,v1,v2,v3) -> @@ -192,7 +192,7 @@ instance printable_tuple5 #t0 #t1 #t2 #t3 #t4 {| printable t0 |} {| printable t1 |} {| printable t2 |} {| printable t3 |} {| printable t4 |} -: printable (tuple5 t0 t1 t2 t3 t4) = +: printable (Tuple5.tuple5 t0 t1 t2 t3 t4) = { to_string = (fun (v0,v1,v2,v3,v4) -> @@ -208,7 +208,7 @@ instance printable_tuple6 #t0 #t1 #t2 #t3 #t4 #t5 {| printable t0 |} {| printable t1 |} {| printable t2 |} {| printable t3 |} {| printable t4 |} {| printable t5 |} -: printable (tuple6 t0 t1 t2 t3 t4 t5) = +: printable (Tuple6.tuple6 t0 t1 t2 t3 t4 t5) = { to_string = (fun (v0,v1,v2,v3,v4,v5) -> @@ -226,7 +226,7 @@ instance printable_tuple7 #t0 #t1 #t2 #t3 #t4 #t5 #t6 {| printable t0 |} {| printable t1 |} {| printable t2 |} {| printable t3 |} {| printable t4 |} {| printable t5 |} {| printable t6 |} -: printable (tuple7 t0 t1 t2 t3 t4 t5 t6) = +: printable (Tuple7.tuple7 t0 t1 t2 t3 t4 t5 t6) = { to_string = (fun (v0,v1,v2,v3,v4,v5,v6) -> diff --git a/ulib/FStar.Stubs.Reflection.Types.fsti b/ulib/FStar.Stubs.Reflection.Types.fsti index adb473243d5..64dbb33564e 100644 --- a/ulib/FStar.Stubs.Reflection.Types.fsti +++ b/ulib/FStar.Stubs.Reflection.Types.fsti @@ -40,6 +40,8 @@ type univ_name = ident type typ = term type binders = list binder +open FStar.Tuple3 + (* * match e as binder returns t|C * diff --git a/ulib/FStar.UInt128.fst b/ulib/FStar.UInt128.fst index 444ce8b0882..05f84e7efe0 100644 --- a/ulib/FStar.UInt128.fst +++ b/ulib/FStar.UInt128.fst @@ -1008,7 +1008,7 @@ let mul_wide_high (x y: U64.t) = (plh x y + (phl x y + pll_h x y) % pow2 32) / pow2 32 inline_for_extraction noextract -let mul_wide_impl_t' (x y: U64.t) : Pure (tuple4 U64.t U64.t U64.t U64.t) +let mul_wide_impl_t' (x y: U64.t) : Pure (Tuple4.tuple4 U64.t U64.t U64.t U64.t) (requires True) (ensures (fun r -> let (u1, w3, x', t') = r in U64.v u1 == U64.v x % pow2 32 /\ @@ -1120,7 +1120,7 @@ let mul_wide_low_ok (x y: U64.t) : val product_high32 : x:U64.t -> y:U64.t -> Lemma ((U64.v x * U64.v y) / pow2 32 == phh x y * pow2 32 + plh x y + phl x y + pll_h x y) -#push-options "--z3rlimit 20" +#push-options "--z3rlimit 40" let product_high32 x y = Math.pow2_plus 32 32; product_expand x y; diff --git a/ulib/LowStar.BufferView.Down.fsti b/ulib/LowStar.BufferView.Down.fsti index 7862da54982..9d8392f4417 100644 --- a/ulib/LowStar.BufferView.Down.fsti +++ b/ulib/LowStar.BufferView.Down.fsti @@ -15,6 +15,8 @@ *) module LowStar.BufferView.Down +open FStar.DTuple4 + (** * A "down view" on a buffer allows treating a * `Buffer.buffer a` as a diff --git a/ulib/LowStar.BufferView.fsti b/ulib/LowStar.BufferView.fsti index e076f63502e..b0ed37848c0 100644 --- a/ulib/LowStar.BufferView.fsti +++ b/ulib/LowStar.BufferView.fsti @@ -30,6 +30,8 @@ module LowStar.BufferView **) open LowStar.Monotonic.Buffer +open FStar.DTuple4 + module HS=FStar.HyperStack module B=LowStar.Monotonic.Buffer diff --git a/ulib/LowStar.Printf.fst b/ulib/LowStar.Printf.fst index 76c1feab457..502880bbe55 100644 --- a/ulib/LowStar.Printf.fst +++ b/ulib/LowStar.Printf.fst @@ -254,7 +254,7 @@ let rec arg_t (a:arg) : Type u#1 = match a with | Base t -> lift (base_typ_as_type t) | Array t -> (l:UInt32.t & r:_ & s:_ & lmbuffer (base_typ_as_type t) r s l) - | Any -> (a:Type0 & (a -> StTrivial unit) & a) + | Any -> (a:Type0 & _:(a -> StTrivial unit) & a) /// `frag_t`: a fragment is either a string literal or a argument to be interpolated noextract From 100e490a42d76f9a97d91f3afbb8adf51dbde1d3 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 5 Feb 2024 18:16:38 -0800 Subject: [PATCH 4/6] Fix tests/examples for new tuples --- examples/rel/UnionFind.Functions.fst | 6 +++--- tests/bug-reports/Bug1866.fst | 4 ++-- tests/bug-reports/Bug2684c.fst | 2 +- tests/bug-reports/Bug2684d.fst | 2 +- tests/micro-benchmarks/TestPrintable.fst | 2 +- 5 files changed, 8 insertions(+), 8 deletions(-) diff --git a/examples/rel/UnionFind.Functions.fst b/examples/rel/UnionFind.Functions.fst index 2fe0c2f4cae..1666bc39d78 100644 --- a/examples/rel/UnionFind.Functions.fst +++ b/examples/rel/UnionFind.Functions.fst @@ -26,9 +26,9 @@ open UnionFind.Forest module ST = FStar.DM4F.Heap.ST (* helpers for getting the parent, height, and the subtree *) -unfold let parent (#n:nat) (uf:uf_forest n) (i:id n) (h:heap) :GTot (id n) = Mktuple3?._1 (sel h (index uf i)) -unfold let height (#n:nat) (uf:uf_forest n) (i:id n) (h:heap) :GTot nat = Mktuple3?._2 (sel h (index uf i)) -unfold let subtree (#n:nat) (uf:uf_forest n) (i:id n) (h:heap) :GTot subtree_t = reveal (Mktuple3?._3 (sel h (index uf i))) +unfold let parent (#n:nat) (uf:uf_forest n) (i:id n) (h:heap) :GTot (id n) = Tuple3.Mktuple3?._1 (sel h (index uf i)) +unfold let height (#n:nat) (uf:uf_forest n) (i:id n) (h:heap) :GTot nat = Tuple3.Mktuple3?._2 (sel h (index uf i)) +unfold let subtree (#n:nat) (uf:uf_forest n) (i:id n) (h:heap) :GTot subtree_t = reveal (Tuple3.Mktuple3?._3 (sel h (index uf i))) (* * well-formed conditions on the forest, essentially the invariants needed for proving the termination of operations diff --git a/tests/bug-reports/Bug1866.fst b/tests/bug-reports/Bug1866.fst index 8891b34e350..a180c0be9df 100644 --- a/tests/bug-reports/Bug1866.fst +++ b/tests/bug-reports/Bug1866.fst @@ -57,11 +57,11 @@ let base0 = x let base1 = - let Mktuple3 x y z = (1,2,3) in + let Tuple3.Mktuple3 x y z = (1,2,3) in x let base2 = - let Mktuple3 #_ #_ #_ x y z = (1,2,3) in + let Tuple3.Mktuple3 #_ #_ #_ x y z = (1,2,3) in x val base3 : #a:Type -> #b:Type -> a & b -> a diff --git a/tests/bug-reports/Bug2684c.fst b/tests/bug-reports/Bug2684c.fst index ad5a4cf1fef..0e9a3d8b861 100644 --- a/tests/bug-reports/Bug2684c.fst +++ b/tests/bug-reports/Bug2684c.fst @@ -15,4 +15,4 @@ val a_lemma: #ty:Type0 -> (#[exact (`())] _ : unit) -> #x:nat -> #y:nat_dep x -> let rec a_lemma #ty #tc #x #y z = let r = a_function z in match r with - | Mkdtuple3 _ _ _ -> () + | DTuple3.Mkdtuple3 _ _ _ -> () diff --git a/tests/bug-reports/Bug2684d.fst b/tests/bug-reports/Bug2684d.fst index 80b46d3900a..1d3ddfd625e 100644 --- a/tests/bug-reports/Bug2684d.fst +++ b/tests/bug-reports/Bug2684d.fst @@ -7,4 +7,4 @@ let f #_ = unit let elim (d : (y:f & z:unit{y == z} & w:unit{w == z})) : unit = match d with - | Mkdtuple3 #_ #_ #_ x y z -> () + | DTuple3.Mkdtuple3 #_ #_ #_ x y z -> () diff --git a/tests/micro-benchmarks/TestPrintable.fst b/tests/micro-benchmarks/TestPrintable.fst index 4aa5f2f64aa..0d7bd856d6e 100644 --- a/tests/micro-benchmarks/TestPrintable.fst +++ b/tests/micro-benchmarks/TestPrintable.fst @@ -61,7 +61,7 @@ let printable_either_test_r = assert(to_string ((fun (i : either int int) -> i) let printable_char_test = assert(to_string '?' = "?") by compute() -let printable_tuple3_test = assert(to_string (Mktuple3 0 1 2) = "(0, 1, 2)") by compute() +let printable_tuple3_test = assert(to_string (Tuple3.Mktuple3 0 1 2) = "(0, 1, 2)") by compute() (* From 6937c86d69e49aa5894459395c1843c851cc7325 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Mon, 5 Feb 2024 21:30:44 -0800 Subject: [PATCH 5/6] Parser.Const: fix tuple arities, fix extraction --- .../fstar-lib/FStar_Extraction_ML_PrintML.ml | 21 +-- src/extraction/FStar.Extraction.ML.Code.fst | 6 +- src/extraction/FStar.Extraction.ML.Util.fst | 14 +- src/parser/FStar.Parser.Const.fst | 167 +++++++++--------- src/parser/FStar.Parser.ToDocument.fst | 4 +- src/syntax/FStar.Syntax.Resugar.fst | 6 +- 6 files changed, 100 insertions(+), 118 deletions(-) diff --git a/ocaml/fstar-lib/FStar_Extraction_ML_PrintML.ml b/ocaml/fstar-lib/FStar_Extraction_ML_PrintML.ml index 100564959f6..57b070eb591 100644 --- a/ocaml/fstar-lib/FStar_Extraction_ML_PrintML.ml +++ b/ocaml/fstar-lib/FStar_Extraction_ML_PrintML.ml @@ -212,18 +212,15 @@ let rec build_core_type ?(annots = []) (ty: mlty): core_type = let c_tys = map build_core_type tys in let p = path_to_ident (path, sym) in let ty = Typ.mk (Ptyp_constr (p, c_tys)) in - (match path with - | ["FStar"; "Pervasives"; "Native"] -> - (* A special case for tuples, so they are displayed as - * ('a * 'b) instead of ('a,'b) FStar_Pervasives_Native.tuple2 - * VD: Should other types named "tupleXX" where XX does not represent - * the arity of the tuple be added to FStar.Pervasives.Native, - * the condition below might need to be more specific. *) - if BatString.starts_with sym "tuple" then - Typ.mk (Ptyp_tuple (map build_core_type tys)) - else - ty - | _ -> ty) + if FStar_Parser_Const.is_tuple_constructor_string (String.concat "." (path@[sym])) then + (* A special case for tuples, so they are displayed as + * ('a * 'b) instead of ('a,'b) FStar_Pervasives_Native.tuple2 + * VD: Should other types named "tupleXX" where XX does not represent + * the arity of the tuple be added to FStar.Pervasives.Native, + * the condition below might need to be more specific. *) + Typ.mk (Ptyp_tuple (map build_core_type tys)) + else + ty | MLTY_Tuple tys -> Typ.mk (Ptyp_tuple (map build_core_type tys)) | MLTY_Top -> Typ.mk (Ptyp_constr (mk_lident "Obj.t", [])) | MLTY_Erased -> Typ.mk (Ptyp_constr (mk_lident "unit", [])) diff --git a/src/extraction/FStar.Extraction.ML.Code.fst b/src/extraction/FStar.Extraction.ML.Code.fst index 5b879ad77d4..bbd6ef4c957 100644 --- a/src/extraction/FStar.Extraction.ML.Code.fst +++ b/src/extraction/FStar.Extraction.ML.Code.fst @@ -27,8 +27,10 @@ open FStar.Const open FStar.BaseTypes module BU = FStar.Compiler.Util -(* This is the old printer used exclusively for the F# build of F*. It will not - * evolve in the future. *) +(* NOTE!!!!!!!!!!!!!!!!!!!! + * This is the old printer used exclusively for the F# build of F*. It will not + * evolve in the future. For the actual printer used for extracting OCaml code, + * see ocaml/fstar-lib/FStar_Extraction_ML_PrintML.ml *) (* -------------------------------------------------------------------- *) type assoc = | ILeft | IRight | Left | Right | NonAssoc diff --git a/src/extraction/FStar.Extraction.ML.Util.fst b/src/extraction/FStar.Extraction.ML.Util.fst index 45dc81e1a07..91f37e0b337 100644 --- a/src/extraction/FStar.Extraction.ML.Util.fst +++ b/src/extraction/FStar.Extraction.ML.Util.fst @@ -275,10 +275,9 @@ let is_type_abstraction = function | _ -> false let is_xtuple (ns, n) = - if FStar.Parser.Const.is_tuple_datacon_string (BU.concat_l "." (ns@[n])) - (* Returns the integer k in "Mktuplek" *) - then Some (BU.int_of_char (BU.char_at n 7)) - else None + Parser.Const.get_tuple_datacon_arity (BU.concat_l "." (ns@[n])) +let is_xtuple_ty (ns, n) = + Parser.Const.get_tuple_tycon_arity (BU.concat_l "." (ns@[n])) let resugar_exp e = match e.expr with | MLE_CTor(mlp, args) -> @@ -309,13 +308,6 @@ let record_fields fs vs = List.map2 (fun (f:lident) e -> (string_of_id (ident_of // end // | _ -> p - -let is_xtuple_ty (ns, n) = - if FStar.Parser.Const.is_tuple_constructor_string (BU.concat_l "." (ns@[n])) - (* Returns the integer k in "tuplek" *) - then Some (BU.int_of_char (BU.char_at n 5)) - else None - let resugar_mlty t = match t with | MLTY_Named (args, mlp) -> begin match is_xtuple_ty mlp with diff --git a/src/parser/FStar.Parser.Const.fst b/src/parser/FStar.Parser.Const.fst index 43613a656f9..f90abf425c1 100644 --- a/src/parser/FStar.Parser.Const.fst +++ b/src/parser/FStar.Parser.Const.fst @@ -428,113 +428,104 @@ let const_to_string x = match x with (* Tuples *) +// Arity, type constructor, and data constructor for tuples +private +let tuple_table : list (int & string & string) = [ + (2, "FStar.Pervasives.Native.tuple2", "FStar.Pervasives.Native.Mktuple2"); + (3, "FStar.Tuple3.tuple3", "FStar.Tuple3.Mktuple3"); + (4, "FStar.Tuple4.tuple4", "FStar.Tuple4.Mktuple4"); + (5, "FStar.Tuple5.tuple5", "FStar.Tuple5.Mktuple5"); + (6, "FStar.Tuple6.tuple6", "FStar.Tuple6.Mktuple6"); + (7, "FStar.Tuple7.tuple7", "FStar.Tuple7.Mktuple7"); + (8, "FStar.Tuple8.tuple8", "FStar.Tuple8.Mktuple8"); + (9, "FStar.Tuple9.tuple9", "FStar.Tuple9.Mktuple9"); + (10, "FStar.Tuple10.tuple10", "FStar.Tuple10.Mktuple10"); + (11, "FStar.Tuple11.tuple11", "FStar.Tuple11.Mktuple11"); + (12, "FStar.Tuple12.tuple12", "FStar.Tuple12.Mktuple12"); + (13, "FStar.Tuple13.tuple13", "FStar.Tuple13.Mktuple13"); + (14, "FStar.Tuple14.tuple14", "FStar.Tuple14.Mktuple14"); +] + let mk_tuple_lid n r = - let l = - if n = 2 then - Ident.lid_of_str "FStar.Pervasives.Native.tuple2" - else - let s = U.format2 "FStar.Tuple%s.tuple%s" (U.string_of_int n) (U.string_of_int n) in - Ident.lid_of_str s - in - set_lid_range l r + match List.tryFind (fun (n', _, _) -> n = n') tuple_table with + | Some (_, s, _) -> + let l = Ident.lid_of_str s in + set_lid_range l r + | None -> + failwith "Tuple too large" -let lid_tuple2 = mk_tuple_lid 2 dummyRange -let lid_tuple3 = mk_tuple_lid 3 dummyRange -let lid_tuple4 = mk_tuple_lid 4 dummyRange -let lid_tuple5 = mk_tuple_lid 5 dummyRange - -let is_tuple_constructor_string (s:string) :bool = - s = "FStar.Pervasives.Native.tuple2" || - s = "FStar.Tuple3.tuple3" || - s = "FStar.Tuple4.tuple4" || - s = "FStar.Tuple5.tuple5" || - s = "FStar.Tuple6.tuple6" || - s = "FStar.Tuple7.tuple7" || - s = "FStar.Tuple8.tuple8" || - s = "FStar.Tuple9.tuple9" || - s = "FStar.Tuple10.tuple10" || - s = "FStar.Tuple11.tuple11" || - s = "FStar.Tuple12.tuple12" || - s = "FStar.Tuple13.tuple13" || - s = "FStar.Tuple14.tuple14" +let mk_tuple_data_lid n r = + match List.tryFind (fun (n', _, _) -> n = n') tuple_table with + | Some (_, _, s) -> + let l = Ident.lid_of_str s in + set_lid_range l r + | None -> + failwith "Tuple too large" + +let get_tuple_datacon_arity (s:string) : option int = + match List.tryFind (fun (_, _, s') -> s = s') tuple_table with + | Some (n, _, _) -> Some n + | None -> None +let get_tuple_tycon_arity (s:string) : option int = + match List.tryFind (fun (_, s', _) -> s = s') tuple_table with + | Some (n, _, _) -> Some n + | None -> None + +let is_tuple_constructor_string (s:string) : bool = + List.existsb (fun (_, s', _) -> s = s') tuple_table + +let is_tuple_datacon_string (s:string) : bool = + List.existsb (fun (n, _, s') -> s = s') tuple_table let is_tuple_constructor_id id = is_tuple_constructor_string (string_of_id id) let is_tuple_constructor_lid lid = is_tuple_constructor_string (string_of_lid lid) -let mk_tuple_data_lid n r = - let l = - if n = 2 then - Ident.lid_of_str "FStar.Pervasives.Native.Mktuple2" - else - let s = U.format2 "FStar.Tuple%s.Mktuple%s" (U.string_of_int n) (U.string_of_int n) in - Ident.lid_of_str s - in - set_lid_range l r +let is_tuple_datacon_id id = is_tuple_datacon_string (string_of_id id) +let is_tuple_datacon_lid lid = is_tuple_datacon_string (string_of_lid lid) +let is_tuple_data_lid f n = lid_equals f (mk_tuple_data_lid n dummyRange) +let lid_tuple2 = mk_tuple_lid 2 dummyRange +let lid_tuple3 = mk_tuple_lid 3 dummyRange let lid_Mktuple2 = mk_tuple_data_lid 2 dummyRange let lid_Mktuple3 = mk_tuple_data_lid 3 dummyRange let lid_Mktuple4 = mk_tuple_data_lid 4 dummyRange let lid_Mktuple5 = mk_tuple_data_lid 5 dummyRange -let is_tuple_datacon_string (s:string) :bool = - s = "FStar.Pervasives.Native.Mktuple2" || - s = "FStar.Tuple3.Mktuple3" || - s = "FStar.Tuple4.Mktuple4" || - s = "FStar.Tuple5.Mktuple5" || - s = "FStar.Tuple6.Mktuple6" || - s = "FStar.Tuple7.Mktuple7" || - s = "FStar.Tuple8.Mktuple8" || - s = "FStar.Tuple9.Mktuple9" || - s = "FStar.Tuple10.Mktuple10" || - s = "FStar.Tuple11.Mktuple11" || - s = "FStar.Tuple12.Mktuple12" || - s = "FStar.Tuple13.Mktuple13" || - s = "FStar.Tuple14.Mktuple14" - -let is_tuple_datacon_id id = is_tuple_datacon_string (string_of_id id) -let is_tuple_datacon_lid lid = is_tuple_datacon_string (string_of_lid lid) - -let is_tuple_data_lid f n = - lid_equals f (mk_tuple_data_lid n dummyRange) - -let is_tuple_data_lid' f = is_tuple_datacon_string (string_of_lid f) - - (* Dtuples *) -(* dtuple is defined in prims if n = 2, in pervasives otherwise *) -let mod_prefix_dtuple (n:int) : (string -> lident) = - fun s -> - if n = 2 - then pconst s - else lid_of_path ["FStar"; "DTuple" ^ string_of_int n; s] dummyRange +// Arity, type constructor, and data constructor for dependent tuples +private +let dtuple_table : list (int & string & string) = [ + (2, "Prims.dtuple2", "Prims.Mkdtuple2"); + (3, "FStar.DTuple3.dtuple3", "FStar.DTuple3.Mkdtuple3"); + (4, "FStar.DTuple4.dtuple4", "FStar.DTuple4.Mkdtuple4"); + (5, "FStar.DTuple5.dtuple5", "FStar.DTuple5.Mkdtuple5"); +] let mk_dtuple_lid n r = - let t = U.format1 "dtuple%s" (U.string_of_int n) in - set_lid_range ((mod_prefix_dtuple n) t) r - -let is_dtuple_constructor_string (s:string) :bool = - s = "Prims.dtuple2" || - s = "FStar.DTuple3.dtuple3" || - s = "FStar.DTuple4.dtuple4" || - s = "FStar.DTuple5.dtuple5" - -let is_dtuple_constructor_lid lid = is_dtuple_constructor_string (string_of_lid lid) + match List.tryFind (fun (n', _, _) -> n = n') dtuple_table with + | Some (_, s, _) -> + let l = Ident.lid_of_str s in + set_lid_range l r + | None -> + failwith "Dependent Tuple too large" let mk_dtuple_data_lid n r = - let t = U.format1 "Mkdtuple%s" (U.string_of_int n) in - set_lid_range ((mod_prefix_dtuple n) t) r - -let is_dtuple_datacon_string (s:string) :bool = - s = "Prims.Mkdtuple2" || - s = "FStar.DTuple3.Mkdtuple3" || - s = "FStar.DTuple4.Mkdtuple4" || - s = "FStar.DTuple5.Mkdtuple5" + match List.tryFind (fun (n', _, _) -> n = n') dtuple_table with + | Some (_, _, s) -> + let l = Ident.lid_of_str s in + set_lid_range l r + | None -> + failwith "Dependent Tuple too large" + +let is_dtuple_constructor_string (s:string) : bool = + List.existsb (fun (_, s', _) -> s = s') dtuple_table +let is_dtuple_datacon_string (s:string) : bool = + List.existsb (fun (_, _, s') -> s = s') dtuple_table -let is_dtuple_data_lid f n = - lid_equals f (mk_dtuple_data_lid n dummyRange) - -let is_dtuple_data_lid' f = is_dtuple_datacon_string (string_of_lid f) +let is_dtuple_constructor_lid lid = is_dtuple_constructor_string (string_of_lid lid) +let is_dtuple_data_lid f n = lid_equals f (mk_dtuple_data_lid n dummyRange) +let is_dtuple_datacon_lid f = is_dtuple_datacon_string (string_of_lid f) let is_name (lid:lident) = let c = U.char_at (string_of_id (ident_of_lid lid)) 0 in diff --git a/src/parser/FStar.Parser.ToDocument.fst b/src/parser/FStar.Parser.ToDocument.fst index f9aa3646505..40a6dfee8f7 100644 --- a/src/parser/FStar.Parser.ToDocument.fst +++ b/src/parser/FStar.Parser.ToDocument.fst @@ -234,8 +234,8 @@ let matches_var t x = | Var y -> (string_of_id x) = string_of_lid y | _ -> false -let is_tuple_constructor = C.is_tuple_data_lid' -let is_dtuple_constructor = C.is_dtuple_data_lid' +let is_tuple_constructor = C.is_tuple_datacon_lid +let is_dtuple_constructor = C.is_dtuple_datacon_lid let is_array e = match e.tm with (* TODO check that there is no implicit parameters *) diff --git a/src/syntax/FStar.Syntax.Resugar.fst b/src/syntax/FStar.Syntax.Resugar.fst index 38efb13ca00..03632c9612b 100644 --- a/src/syntax/FStar.Syntax.Resugar.fst +++ b/src/syntax/FStar.Syntax.Resugar.fst @@ -225,8 +225,8 @@ let is_true_pat (p:S.pat) : bool = match p.v with | _ -> false let is_tuple_constructor_lid lid = - C.is_tuple_data_lid' lid - || C.is_dtuple_data_lid' lid + C.is_tuple_datacon_lid lid + || C.is_dtuple_datacon_lid lid let may_shorten lid = if Options.print_real_names () then false @@ -1234,7 +1234,7 @@ and resugar_pat' env (p:S.pat) (branch_bv: FlatSet.t bv) : A.pattern = args |> List.filter_map (fun (p, is_implicit) -> if is_implicit then None else Some (aux p (Some false))) in - let is_dependent_tuple = C.is_dtuple_data_lid' fv.fv_name.v in + let is_dependent_tuple = C.is_dtuple_datacon_lid fv.fv_name.v in mk (A.PatTuple (args, is_dependent_tuple)) | Pat_cons({fv_qual=Some (Record_ctor(name, fields))}, _, args) -> From 168732e29cb2bb09e65ca99a1c80e6655d250e28 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= Date: Wed, 7 Feb 2024 09:39:12 -0800 Subject: [PATCH 6/6] FStar.AllTuples: add a way to include all tuples --- ulib/FStar.AllTuples.fsti | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 ulib/FStar.AllTuples.fsti diff --git a/ulib/FStar.AllTuples.fsti b/ulib/FStar.AllTuples.fsti new file mode 100644 index 00000000000..e0db76a1f58 --- /dev/null +++ b/ulib/FStar.AllTuples.fsti @@ -0,0 +1,18 @@ +module FStar.AllTuples + +include FStar.Tuple3 +include FStar.Tuple4 +include FStar.Tuple5 +include FStar.Tuple6 +include FStar.Tuple7 +include FStar.Tuple8 +include FStar.Tuple9 +include FStar.Tuple10 +include FStar.Tuple11 +include FStar.Tuple12 +include FStar.Tuple13 +include FStar.Tuple14 + +include FStar.DTuple3 +include FStar.DTuple4 +include FStar.DTuple5