Source file signature.ml

(**************************************************************************)
(*                                                                        *)
(*                 ACG development toolkit                                *)
(*                                                                        *)
(*                  Copyright 2008-2023 INRIA                             *)
(*                                                                        *)
(*  More information on "https://acg.loria.fr/"                     *)
(*  License: CeCILL, see the LICENSE file or "http://www.cecill.info"     *)
(*  Authors: see the AUTHORS file                                         *)
(*                                                                        *)
(*                                                                        *)
(*                                                                        *)
(*                                                                        *)
(*                                                                        *)
(**************************************************************************)

open UtilsLib
open Table
open Logic.Lambda
open Logic.Abstract_syntax

type sig_entry =
  | Type_declaration of string * int * Lambda.kind
  | Type_definition of string * int * Lambda.kind * Lambda.stype
  | Term_declaration of
      string * int * Abstract_syntax.syntactic_behavior * Lambda.stype
  | Term_definition of
      string
      * int
      * Abstract_syntax.syntactic_behavior
      * Lambda.stype
      * Lambda.term

module Log = Xlog.Make (struct
  let name = "Signature"
end)

module Make
    (Symbols : TABLE with type key = String.t)
    (Id : TABLE with type key = int) =
struct
  exception Duplicate_type_definition
  exception Duplicate_term_definition
  exception Not_found
  exception Not_functional_type

  (* exception Not_yet_implemented *)

  type entry = sig_entry
  type id = int

  [@@@warning "-69"]
  type t = {
    name : string * id ;
    loc : string * Abstract_syntax.location; (* name of the file where
                                                the signature is
                                                defined and its
                                                location *)
    size : int;
    terms : entry Symbols.t;
    types : entry Symbols.t;
    precedence : (float * string option) Symbols.t;
    (* indicates the precedence and a link to the previous one *)
    max_pred : float * string option;
    (* indicates the greatest precedence and a link to the previous one *)
    ids : entry Id.t;
    is_2nd_order : bool;
    extension_timestamp : float;
    definition_timestamp : float;
  }
  [@@@warning "+69"]

  type term = Lambda.term
  type stype = Lambda.stype
  type data = Type of stype | Term of (term * stype)

  let find_term sym { terms = syms; _ } =
    match Symbols.find sym syms with
    | Term_declaration (x, id, _, const_type) when sym = x ->
        (Lambda.Const id, const_type)
    | Term_declaration _ ->
        failwith "Bug in find_term" (* x should match the symbol *)
    | Term_definition (x, id, _, const_type, _) when sym = x ->
        (Lambda.DConst id, const_type)
    | Term_definition _ ->
        failwith "Bug in find_term" (* x should match the symbol *)
    | _ -> failwith "Bug in find_term" (* x should return a Term, not a type *)
    | exception Symbols.Not_found -> raise Not_found

  let id_to_string { ids; _ } i =
    match Id.find i ids with
    | Type_declaration (s, _, _) -> (Abstract_syntax.Default, s)
    | Type_definition (s, _, _, _) -> (Abstract_syntax.Default, s)
    | Term_declaration (s, _, behavior, _) -> (behavior, s)
    | Term_definition (s, _, behavior, _, _) -> (behavior, s)

  let pp_type sg ppf ty = Lambda.pp_type (id_to_string sg) ppf ty
  let pp_term sg ppf t = Lambda.pp_term (id_to_string sg) ppf t

  let empty ~filename (n, l) =
    let timestamp = Unix.time () in
    {
      name = (n, Random.(let () = self_init () in bits ())) ;
      loc = filename , l ;
      size = 0;
      terms = Symbols.empty;
      types = Symbols.empty;
      ids = Id.empty;
      is_2nd_order = true;
      precedence = Symbols.empty;
      max_pred = (0., None);
      definition_timestamp = timestamp;
      extension_timestamp = timestamp;
    }

  let name { name = n, _ ; loc = _, l; _ } = n, l
  let full_name { name = n ; loc = filename, _; _ } = n, filename

  let find_atomic_type s { types = syms; _ } =
    (* TODO : Replace by an assert within IFDEFDEBUG *)
    match Symbols.find s syms with
    | Type_declaration (x, id, _) when x = s -> Lambda.Atom id
    | Type_declaration _ ->
        failwith "Bug in find_atomic_type"
        (* x and s should match if something is returned *)
    | Type_definition (x, id, _, _) when x = s -> Lambda.DAtom id
    | Type_definition _ ->
        failwith "Bug in find_atomic_type"
        (* x and s should match if something is returned *)
    | _ ->
        failwith "Bug in find_atomic_type"
        (* A type, not a term should be returned *)
    | exception Symbols.Not_found -> failwith "Bug in find_atomic_type"

  let find_type s sg =
    (* TODO : Replace by an assert within IFDEFDEBUG *)
    match Symbols.find s sg.types with
    | Type_declaration (x, id, _) when x = s -> Lambda.Atom id
    | Type_definition (x, id, _, _) when x = s -> Lambda.DAtom id
    | _ ->
        failwith "Bug in find_type"
        (* A type, not a term should be returned and x and s should match  *)
    | exception Symbols.Not_found -> raise Not_found
    [@@warning "-32"]

  let rec convert_type ty sg =
    match ty with
    | Abstract_syntax.Type_atom (s, _, _) -> find_atomic_type s sg
    | Abstract_syntax.Linear_arrow (ty1, ty2, _) ->
        Lambda.LFun (convert_type ty1 sg, convert_type ty2 sg)
    | Abstract_syntax.Arrow (ty1, ty2, _) ->
        Lambda.Fun (convert_type ty1 sg, convert_type ty2 sg)

  let abstract_on_dependent_types lst sg =
    List.fold_right
      (fun x acc -> Lambda.Depend (convert_type x sg, acc))
      lst Lambda.Type

  let add_sig_type t e ({ size = s; types = syms; ids; _ } as sg) =
    try
      (* First perform addition on the functional data structure *)
      let new_symbols = Symbols.add t e syms in
      (* timestamps modified at add_entry function *)
      { sg with size = s + 1; types = new_symbols; ids = Id.add s e ids }
    with
    | Symbols.Conflict -> raise Duplicate_type_definition
    | Id.Conflict -> raise Duplicate_type_definition

  let add_sig_term t e ({ size = s; terms = syms; ids; _ } as sg) =
    try
      (* First perform addition on the functional data structure *)
      let new_symbols = Symbols.add t e syms in
      (* timestamps modified at add_entry function *)
      { sg with size = s + 1; terms = new_symbols; ids = Id.add s e ids }
    with
    | Symbols.Conflict -> raise Duplicate_term_definition
    | Id.Conflict -> raise Duplicate_term_definition

  let rec expand_type ty ({ ids; _ } as sg) =
    match ty with
    | Lambda.Atom _ -> ty
    | Lambda.DAtom i -> (
        match Id.find i ids with
        | Type_definition (_, _, _, ty1) -> expand_type ty1 sg
        | _ -> failwith "Bug in expand type")
    | Lambda.LFun (ty1, ty2) ->
        Lambda.LFun (expand_type ty1 sg, expand_type ty2 sg)
    | Lambda.Fun (ty1, ty2) ->
        Lambda.Fun (expand_type ty1 sg, expand_type ty2 sg)
    | _ -> failwith "Not yet implemented"

  let rec expand_term t ({ ids; _ } as sg) =
    match t with
    | Lambda.Var _ | Lambda.LVar _ | Lambda.Const _ -> t
    | Lambda.DConst i -> (
        match Id.find i ids with
        | Term_definition (_, _, _, _, u) -> expand_term u sg
        | _ -> failwith "Bug in expand term")
    | Lambda.Abs (x, u) -> Lambda.Abs (x, expand_term u sg)
    | Lambda.LAbs (x, u) -> Lambda.LAbs (x, expand_term u sg)
    | Lambda.App (u, v) -> Lambda.App (expand_term u sg, expand_term v sg)
    | _ -> failwith "Not yet implemented"

  let unfold_type_definition i ({ ids; _ } as sg) =
    match Id.find i ids with
    | Type_definition (_, _, _, ty1) -> expand_type ty1 sg
    | _ -> failwith "Bug in unfold_type_definition"

  let unfold_term_definition i ({ ids; _ } as sg) =
    match Id.find i ids with
    | Term_definition (_, _, _, _, t) -> expand_term t sg
    | _ -> failwith "Bug in unfold_term_definition"

  let get_type_of_const_id i ({ ids; _ } as sg) =
    match Id.find i ids with
    | Term_declaration (_, _, _, ty) -> expand_type ty sg
    | Term_definition (_, _, _, ty, _) -> expand_type ty sg
    | _ -> failwith "Should be applied only on constants"
    | exception Id.Not_found -> failwith "Bug in get_type_of_const_id"

  let rec decompose_functional_type ty ({ ids; _ } as sg) =
    match ty with
    | Lambda.LFun (ty1, ty2) -> (ty1, ty2, Abstract_syntax.Linear)
    | Lambda.Fun (ty1, ty2) -> (ty1, ty2, Abstract_syntax.Non_linear)
    | Lambda.DAtom i -> (
        match Id.find i ids with
        | Type_definition (_, _, _, ty1) -> decompose_functional_type ty1 sg
        | _ -> failwith "Bug in decompose_functional_type")
    | _ -> raise Not_functional_type

  let get_binder_argument_functional_type x ({ terms; _ } as sg) =
    let ty =
      match Symbols.find x terms with
      | Term_declaration (_, _, _, ty) -> ty
      | Term_definition (_, _, _, ty, _) -> ty
      | _ ->
          failwith
            (Printf.sprintf
               "Bug: Request of the type of the non constant \"%s\"" x)
    in
    try
      let ty1, _, _ = decompose_functional_type ty sg in
      let _, _, lin = decompose_functional_type ty1 sg in
      Some lin
    with Not_functional_type -> None

  (* We assume here that [term] is well typed and in beta-normal form
     and that types and terms definitions have been unfolded*)

  let eta_long_form term stype sg =
    let expanded_type = expand_type stype sg in
    let expanded_term = expand_term term sg in
    let res =
      Lambda.eta_long_form expanded_term expanded_type (fun id ->
          get_type_of_const_id id sg)
    in
    let f1 = pp_term sg in
    let f2 = pp_type sg in
    Log.debug (fun m -> m "term: %a:%a" f1 term f2 stype);
    Log.debug (fun m -> m "eta_long_form: %a:%a" f1 res f2 expanded_type);
    res

  let unfold t sg = Lambda.normalize (expand_term t sg)
  let is_atomic t sg = Lambda.is_atomic t (fun i -> unfold_type_definition i sg)

  type temp_t = t
  (* type temp_entry=entry *)

  module Type_System = Type_system.Type_System.Make (struct
    exception Not_found

    type t = temp_t

    let unfold_type_definition = unfold_type_definition
    let expand_type = expand_type
    let find_term = find_term
    let pp_type = pp_type
    let pp_term = pp_term
  end)

  let typecheck = Type_System.typecheck
  let stamp_declaration sg = { sg with extension_timestamp = Unix.time () }
  let stamp_definition sg = { sg with definition_timestamp = Unix.time () }

  let add_entry e ({ size = s; _ } as sg) =
    match e with
    | Abstract_syntax.Type_decl (t, _, Abstract_syntax.K k) ->
        stamp_declaration
          (add_sig_type t
             (Type_declaration (t, s, abstract_on_dependent_types k sg))
             sg)
    | Abstract_syntax.Type_def (t, _, ty, Abstract_syntax.K k) ->
        stamp_definition
          (add_sig_type t
             (Type_definition
                (t, s, abstract_on_dependent_types k sg, convert_type ty sg))
             sg)
    | Abstract_syntax.Term_decl (t, behavior, _, ty) ->
        let t_type = convert_type ty sg in
        let sg_is_2nd_order =
          sg.is_2nd_order
          && Lambda.is_2nd_order t_type (fun i -> unfold_type_definition i sg)
        in
        stamp_declaration
          (add_sig_term t
             (Term_declaration (t, s, behavior, convert_type ty sg))
             { sg with is_2nd_order = sg_is_2nd_order })
    | Abstract_syntax.Term_def (t, behavior, _, term, ty) ->
        let t_type = convert_type ty sg in
        let t_term, _ = typecheck term t_type sg in
        stamp_definition
          (add_sig_term t (Term_definition (t, s, behavior, t_type, t_term)) sg)

  let is_type ?(atomic = false) s { types = syms; _ } =
    match Symbols.find s syms with
    | Type_declaration _ -> true
    | Type_definition _ when not atomic -> true
    | _ -> false
    | exception Symbols.Not_found -> false

  let is_constant s ({ terms = syms; _ } as sg) =
    match Symbols.find s syms with
    | Term_declaration (_, _, behavior, ty) -> (true, Some (behavior, false, is_atomic (expand_type ty sg) sg))
    | Term_definition (_, _, behavior, ty, _) -> (true, Some (behavior, true, is_atomic (expand_type ty sg) sg))
    | _ -> (false, None)
    | exception Symbols.Not_found -> (false, None)

  (*
     let precedence s {precedence;_} =
       match Symbols.find s precedence with
       | f,_ -> Some f
       | exception Symbols.Not_found -> None
  *)

  let new_precedence ?before id sg =
    match (before, sg.max_pred) with
    | None, (f, None) ->
        let p = f +. 1. in
        ( p,
          {
            sg with
            max_pred = (p, Some id);
            precedence = Symbols.add id (p, None) sg.precedence;
          } )
    | None, (f, (Some _ as max)) ->
        let p = f +. 1. in
        ( p,
          {
            sg with
            max_pred = (p, Some id);
            precedence = Symbols.add id (p, max) sg.precedence;
          } )
    | Some _, (f, None) ->
        (* Strange to give an upper bound when there is no max. Behaves
           like introducing the first element *)
        let p = f +. 1. in
        ( p,
          {
            sg with
            max_pred = (p, Some id);
            precedence = Symbols.add id (p, None) sg.precedence;
          } )
    | Some upper_bound, _ -> (
        match Symbols.find upper_bound sg.precedence with
        | f_up, None ->
            let f_down = 0. in
            let p = (f_up +. f_down) /. 2. in
            let new_pred =
              Symbols.add ~overwrite:true upper_bound (f_up, Some id)
                (Symbols.add id (p, None) sg.precedence)
            in
            (p, { sg with precedence = new_pred })
        | f_up, Some lower_bound ->
            let f_down, _ = Symbols.find lower_bound sg.precedence in
            let p = (f_up +. f_down) /. 2. in
            let new_pred =
              Symbols.add upper_bound (f_up, Some id)
                (Symbols.add id (p, Some lower_bound) sg.precedence)
            in
            (p, { sg with precedence = new_pred })
        | exception Not_found -> failwith "Bug: Shouldn't happen")

  let raw_to_string t = Lambda.raw_to_string t [@@warning "-32"]

  let behavior_to_string = function
    | Abstract_syntax.Default -> ""
    | Abstract_syntax.Prefix -> "prefix "
    | Abstract_syntax.Infix _ -> "infix "
    | Abstract_syntax.Binder -> "binder "

  let pp_entry f fmt decl =
    let pp_kind = Lambda.pp_kind f in
    let pp_type = Lambda.pp_type f in
    let pp_term = Lambda.pp_term f in
    match decl with
    | Type_declaration (s, _, k) ->
        Format.fprintf fmt "@[<hov 4>%s :@ @[%a@];@]" s pp_kind k
    | Type_definition (s, _, k, ty) ->
        Format.fprintf fmt "@[<hov 4>%s =@ @[%a :@ @[%a@];@]@]" s pp_type ty
          pp_kind k
    | Term_declaration (s, _, behavior, ty) ->
        Format.fprintf fmt "@[<hov 4>%s%s :@ @[%a@];@]"
          (behavior_to_string behavior)
          s pp_type ty
    | Term_definition (s, _, behavior, ty, t) ->
        Format.fprintf fmt "@[<hov 4>%s%s =@ @[%a :@ @[%a@];@]@]"
          (behavior_to_string behavior)
          s pp_term t pp_type ty

  let pp fmt ({ name = n, _ ; ids; _ } as sg) =
    Format.fprintf fmt "signature %s =@,@[<v 2>@[%a@]@]@,end@." n
      (Id.pp (fun fmt _ entry -> pp_entry (id_to_string sg) fmt entry))
      ids

  let convert_term t ty sg =
    let t_type = convert_type ty sg in
    let t, _ = typecheck t t_type sg in
    (t, t_type)

  let type_of_constant x { terms = syms; _ } =
    match Symbols.find x syms with
    | Term_declaration (s, _, _, ty) when x = s -> ty
    | Term_definition (s, _, _, ty, _) when x = s -> ty
    | _ -> failwith "Bug in type_of_constant"
    | exception Symbols.Not_found -> failwith "Bug in type_of_constant"

  let fold f a { ids; _ } = Id.fold (fun _ att acc -> f att acc) a ids

  let is_declared e _ =
    match e with
    | Type_declaration (s, _, _) -> Some s
    | Term_declaration (s, _, _, _) -> Some s
    | _ -> None

  let is_2nd_order { is_2nd_order; _ } = is_2nd_order

  let entry_to_data e =
    match e with
    | Type_declaration (_,id,_) -> Type(Lambda.Atom id)
    | Type_definition (_,_,_,stype) -> Type stype
    | Term_declaration (_,id,_,stype) -> Term(Lambda.Const id,stype)
    | Term_definition (_,_,_,stype,term) -> Term (term,stype)

  let gen_term_list sg ty min_depth max_depth shuffle =
    let incr_vars vars =
      List.map (fun e -> let (args, t, tc) = e in
        match tc with
        | Lambda.Var n -> (args, t, Lambda.Var (n + 1))
        | Lambda.LVar n -> (args, t, Lambda.LVar (n + 1))
        | _ -> e) vars in

    (* This function decrements the indexes of all linear variables in the list
       "vars". We use it when the term of a linear abstraction has been built,
       because we need to return the linear variables list (which contains those
       which don't appear in the term) to the caller. At the same time, we check
       that we don't have a linear variable with an index of 0 in the list,
       because this would mean that it has not been used in the term, so it is
       invalid. *)
    let rec decr_vars vars =
      match vars with
      | (args, t, tc)::t_vars -> (match tc with
        | Lambda.LVar n -> if n = 0 then None
          else Option.map
            (fun vars -> (args, t, Lambda.LVar (n - 1))::vars) (decr_vars t_vars)
        | _ -> Option.map
          (fun vars -> (args, t, tc)::vars) (decr_vars t_vars))
      | [] -> Some [] in

    let shuffle_rules rules =
      let pairs = List.map (fun r -> (Random.bits (), r)) rules in
      let sorted_pairs =
        List.sort (fun p1 p2 -> compare (fst p1) (fst p2)) pairs in
      List.map snd sorted_pairs in

    let get_letter i =
      String.make 1 (Char.chr (97 + (i mod 26))) in

    let type_to_rule ty term =
      let ty = expand_type ty sg in
      let rec gen_arg_list ty acc =
        match ty with
        | Lambda.Atom _ -> (acc, ty)
        | Lambda.Fun (ty1, ty2) ->
          gen_arg_list ty2 ((ty1, false)::acc)
        | Lambda.LFun (ty1, ty2) ->
          gen_arg_list ty2 ((ty1, true)::acc)
        | _ -> failwith "Not implemented" in
      let (arg_list, ty_f) = gen_arg_list ty [] in
        (arg_list, ty_f, term) in

    (* This builds a rule list from all term declarations in the signature. A
       rule is of type "((stype, bool) list, stype, term)" and if
       "(arg_list, ty, te)" is a rule, it says "to build a term of type "ty"",
       one needs to compute a term of each type in the list "arg_list", add
       apply all theses terms to "te". The type "ty" is always an atom. The
       boolean associated to each type in the list "arg_list" is true iff free
       linear variables are allowed in the corresponding term to build. In
       other words, the rule "([(A, true), (B, true), (A, false)], C, build_c)"
       corresponds to this signature entry : "build_c : A -> B -> A => C". *)
    let env =
      fold (fun e l -> match e with
        | Term_declaration (_, i, _, t) ->
          (type_to_rule t (Lambda.Const i))::l
        | _ -> l)
      [] sg in

    let term_depth t =
      let rec term_depth_rec t add =
        match t with
        | Lambda.Abs (_, t) -> term_depth_rec t 1
        | Lambda.LAbs (_, t) -> term_depth_rec t 1
        | Lambda.App (t1, t2) -> add + max (term_depth_rec t1 0) (term_depth_rec t2 1)
        | _ -> 1 in
      term_depth_rec t 1 in

    let rec compute_arg (ty, lin) vars lvars_l letter fuel =
      LazyList.join_mix
        (LazyList.map
          (fun lvars_b -> (LazyList.map
            (fun (lvars_a, term) -> ((if lin then lvars_a else lvars_b), term))
            (gen_term_rec ty vars (if lin then lvars_b else []) letter (fuel - 1))))
          lvars_l)

    and apply_rule args term vars lvars letter fuel =
      match args with
      | arg::args -> LazyList.bind_mix
        (fun (lvars, arg_term) -> LazyList.map
          (fun (lvars, term) -> (lvars, Lambda.App (term, arg_term)))
          (apply_rule args term vars lvars letter fuel))
        (compute_arg arg vars (LazyList.one lvars) letter fuel)
      | [] -> LazyList.one (lvars, term)

    (* This function builds all possible terms using the rules in the list
       "rules". The rules are tried one by one (by calling the function
       "apply_rule"). When a rule corresponds to a linear variable (when it is
       of the form "(_, _, Lvar _)"), we need to remove its corresponding rule
       from the current context. *)
    and apply_rules rules vars lvars letter fuel =
      match rules with
      | (args, _, tc)::rules ->
        let lvars_f = (match tc with
          | Lambda.LVar i -> List.filter
            (fun (_, _, term) ->
              match term with | Lambda.LVar j -> not (i = j) | _ -> false) lvars
          | _ -> lvars) in
        LazyList.append_mix
          (apply_rule args tc vars lvars_f letter fuel)
          (fun () -> apply_rules rules vars lvars letter fuel)
      | [] -> LazyList.Nil

    (* To generate the terms of type "t" with the rules in the list "env", the
       variables in the list "vars" and the linear variables in the list
       "l_vars", we have three cases :
         - The type "t" is an atom, so we select all the rules which give a
           term of type "t" from the environment "env" and the list of linear
           variables "l_vars", shuffle them in a random order, and try all of
           them to build all possible terms.
         - The type is a normal arrow, "A -> B", so we add a new rule
           corresponding to A in the variables list, and try to build all
           possible terms of type B with this new environment. We apply an
           abstraction to all generated terms.
         - The type is a linear arrow, "A => B", so we add a new rule
           corresponding to A in the linear variables list, and try to build all
           possible terms of type B. We then return all generated terms in which
           this linear variable has been used, with a linear abstraction. *)
    and gen_term_rec ty vars lvars letter fuel =
      let ty = expand_type ty sg in
      if fuel = 0 then LazyList.Nil else
        match ty with
        | Lambda.Atom _ ->
          let rules = List.filter
            (fun (_, ty_rule, _) -> ty = ty_rule)
            (env @ vars @ lvars) in
          let res =
            if shuffle then
              apply_rules (shuffle_rules rules) vars lvars letter fuel
            else
              apply_rules rules vars lvars letter fuel in
          res
        | Lambda.Fun (ty1, ty2) ->
          LazyList.map
          (fun (lvars, term) -> (lvars, Lambda.Abs (get_letter letter, term)))
          (gen_term_rec ty2
            ((type_to_rule ty1 (Lambda.Var 0))::(incr_vars vars))
            lvars (letter + 1) fuel)
        | Lambda.LFun (ty1, ty2) ->
          LazyList.filter_map
          (fun (lvars, term) -> Option.map
            (fun lvars -> (lvars, Lambda.LAbs (get_letter letter, term)))
            (decr_vars lvars))
          (gen_term_rec ty2 vars
            ((type_to_rule ty1 (Lambda.LVar 0))::(incr_vars lvars))
            (letter + 1) fuel)
        | _ -> LazyList.Nil in

    LazyList.filter_map
      (fun (_, t) -> if term_depth t >= min_depth then Some t else None)
      (gen_term_rec ty [] [] 0 max_depth)
end

module Table = Table.Make_table (struct
  let b = 10
end)
(*module Table =
  struct
  module IntMap = Map.Make(struct type t=int let compare i j = i-j end)
  type 'a t = 'a IntMap.t
  type key = int

  exception Conflict
  let empty = IntMap.empty
  let add ?(overwrite=false) k v t =
  try
  let _ = IntMap.find k t in
  if overwrite then IntMap.add k v t else raise Conflict
  with
  | Not_found -> IntMap.add k v t


  exception Not_found

  let find k t =
  try
  IntMap.find k t
  with
  | Not_found -> raise Not_found
  let fold f acc t = IntMap.fold f t acc
  end
*)

module Data_Signature = Make (Tries.Tries) (Table)