Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Splitting tuple types into separate modules for each #3204

Open
wants to merge 6 commits into
base: master
Choose a base branch
from
Open

Splitting tuple types into separate modules for each #3204

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
77df44f
Splitting tuples
mtzguido Feb 5, 2024
067f87d
Fixing compiler for new tuples
mtzguido Feb 6, 2024
357b0c3
Fix library
mtzguido Feb 6, 2024
100e490
Fix tests/examples for new tuples
mtzguido Feb 6, 2024
6937c86
Parser.Const: fix tuple arities, fix extraction
mtzguido Feb 6, 2024
168732e
FStar.AllTuples: add a way to include all tuples
mtzguido Feb 7, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions examples/rel/UnionFind.Functions.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
10 changes: 10 additions & 0 deletions ocaml/fstar-lib/FStar_DTuple3.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
16 changes: 16 additions & 0 deletions ocaml/fstar-lib/FStar_DTuple4.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
25 changes: 25 additions & 0 deletions ocaml/fstar-lib/FStar_DTuple5.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
21 changes: 9 additions & 12 deletions ocaml/fstar-lib/FStar_Extraction_ML_PrintML.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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", []))
Expand Down
264 changes: 0 additions & 264 deletions ocaml/fstar-lib/FStar_Pervasives_Native.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
24 changes: 24 additions & 0 deletions ocaml/fstar-lib/FStar_Tuple10.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Loading
Loading