Source file acg_lexicon.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 Containers
open Logic
open Abstract_syntax
open Lambda
open Signature

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

module MagicLog = Xlog.Make (struct
  let name = "Acg_lexicon/Magic"
end)

module ParsingLog = Xlog.Make (struct
  let name = "Acg_lexicon/Parsing_check"
end)


module Data_Lexicon = struct
  exception Duplicate_type_interpretation
  exception Duplicate_constant_interpretation
  exception Not_almost_linear

  module Pair = struct
    type kind = Type | Cst
    type t = string * kind

    let compare (s, k) (s', k') =
      match (k, k') with
      | Type, Cst -> -1
      | Cst, Type -> 1
      | _, _ -> String.compare s s'
  end

  module Dico = Map.Make (Pair)

  type resumptions = int SharedForest.SharedForest.Resumptions.resumptions * int SharedForest.SharedForest.forest * (Data_Signature.term * Data_Signature.stype)

  type interpretation =
    | Type of (Abstract_syntax.location * Lambda.stype)
    | Constant of (Abstract_syntax.location * Lambda.term)

  let pp_interpretation fun_type_from_id i sg fmt abstract_type_or_cst_id =
    let pp_term = Data_Signature.pp_term sg in
    let pp_type = Data_Signature.pp_type sg in
    match i with
    | Type (_, t) -> pp_type fmt t
    | Constant (_, c) ->
        let eta_long =
          Data_Signature.eta_long_form c
            (fun_type_from_id abstract_type_or_cst_id)
            sg
        in
        Format.fprintf fmt "%a [eta-long form: %a {%s}]" pp_term c pp_term
          eta_long
          (Lambda.raw_to_string eta_long)

  module Datalog = DatalogLib.Datalog.Datalog
  module DatalogRule = Datalog.Rule
  module DatalogPredMap = Datalog.Predicate.PredMap
  module DatalogAbstractSyntax = DatalogLib.Datalog_AbstractSyntax.AbstractSyntax
  module ASPred = DatalogAbstractSyntax.Predicate
  module ASProg = DatalogAbstractSyntax.Program
  module ASRule = DatalogAbstractSyntax.Rule
  module RuleToCstMap = Utils.IntMap

  type datalog_correspondance = {
    prog : Datalog.Program.program;
    magic_programs :
      (Datalog.Program.program * MagicRewriting.Rewriting.magic_context)
      MagicRewriting.Rewriting.QueryMap.t
      option;
    rule_to_cst : Lambda.term RuleToCstMap.t;
    cst_to_rule : int Utils.IntMap.t;
    generated_symbols : string Utils.IntMap.t * Utils.StringSet.t;
        (* These maps and sets record map from ids of object constants to
           symbols that where generated for extensional predicates to
           avoid a name clash when an object constant has the same name as
           an abstract atomic type *)
  }

  type 'a build =
    | Interpret of (string * string)
    | Compose of ('a list)

  [@@@warning "-69"]

  type t = {
    name : string * Abstract_syntax.location;
    dico : interpretation Dico.t;
    syntax_dico : Abstract_syntax.lex_entry Dico.t option;
    non_linear_interpretation : bool;
    abstract_sig : Data_Signature.t;
    object_sig : Data_Signature.t;
    datalog_prog : datalog_correspondance option;
    build : string build;
    timestamp : float;
    is_almost_linear : bool;
  }

  type dumped_t = {
    dumped_name : string * Abstract_syntax.location;
    dumped_dico : interpretation Dico.t;
    dumped_syntax_dico : Abstract_syntax.lex_entry Dico.t option;
    dumped_non_linear_interpretation : bool;
    dumped_abstract_sig : (string * Data_Signature.id) * string;
    dumped_object_sig : (string * Data_Signature.id) * string;
    dumped_datalog_prog : datalog_correspondance option;
    dumped_build : string build;
    dumped_timestamp : float;
    dumped_is_almost_linear : bool;
  }

  let name_of_dumped l = fst (l.dumped_name)
  
  let prepare_dump (l:t) =
    { 
    dumped_name = l.name;
    dumped_dico = l.dico;
    dumped_syntax_dico = l.syntax_dico;
    dumped_non_linear_interpretation = l.non_linear_interpretation;
    dumped_abstract_sig = Data_Signature.full_name l.abstract_sig;
    dumped_object_sig = Data_Signature.full_name l.object_sig;
    dumped_datalog_prog= l.datalog_prog;
    dumped_build = l.build;
    dumped_timestamp = l.timestamp;
    dumped_is_almost_linear = l.is_almost_linear;
  }

  let recover_from_dump ~filename ~get_sig l =
    let check_and_get_sig ((sg_name, sg_id), _) =
      let sg = (get_sig sg_name) in
      let sg_name_id, sg_filename = (Data_Signature.full_name sg) in
      if sg_name_id = (sg_name, sg_id) then
        sg
      else
        Errors.(LexiconErrors.emit (Lexicon_l.NotCompatibleSignature (fst l.dumped_name, filename, sg_name, sg_filename)))        in
    { 
    name = l.dumped_name;
    dico = l.dumped_dico;
    syntax_dico = l.dumped_syntax_dico;
    non_linear_interpretation = l.dumped_non_linear_interpretation;
    abstract_sig = check_and_get_sig l.dumped_abstract_sig;
    object_sig = check_and_get_sig l.dumped_object_sig;
    datalog_prog= l.dumped_datalog_prog;
    build = l.dumped_build;
    timestamp = l.dumped_timestamp;
    is_almost_linear = l.dumped_is_almost_linear;
  }
  
  [@@@warning "+69"]

  type dependency =
    | Signatures of (string * string)
    | Lexicons of string list

  type parsing = Unavailable | Available_with_magic | Available_wo_magic

  let get_dependencies lex =
    match lex.build with
    | Interpret s -> Signatures s
    | Compose l -> Lexicons l

  let pp_lex fmt lex =
    let name, _ = lex.name in
    Utils.lex_pp fmt name
  
  let short_pp fmt
      ({ abstract_sig = abs_sg; object_sig = obj_sg; _ } as lex) =
    Format.fprintf fmt "lexicon@ %a(%a):@ %a" pp_lex lex
      Utils.sig_pp (fst (Data_Signature.name abs_sg))
      Utils.sig_pp (fst (Data_Signature.name obj_sg))


  let name { name = n; _ } = n
  let get_sig { abstract_sig = abs; object_sig = obj; _ } = (abs, obj)

  let empty ?(non_linear = false) ~abs ~obj name =
    let prog =
      (*      if (Data_Signature.is_2nd_order abs) && (not non_linear) then *)
      if Data_Signature.is_2nd_order abs then
        (*	Some (Datalog.Program.empty,RuleToCstMap.empty)  *)
        Some
          {
            prog = Datalog.Program.empty;
            magic_programs = None;
            rule_to_cst = RuleToCstMap.empty;
            cst_to_rule = Utils.IntMap.empty;
            generated_symbols = (Utils.IntMap.empty, Utils.StringSet.empty);
          }
      else None
    in
    {
      name;
      dico = Dico.empty;
      syntax_dico = Some Dico.empty;
      abstract_sig = abs;
      object_sig = obj;
      datalog_prog = prog;
      non_linear_interpretation = non_linear;
      build = Data_Signature.(Interpret (fst (name abs), fst (name obj)));
      timestamp = Unix.time ();
      is_almost_linear = true;
    }

  let is_linear { non_linear_interpretation; _ } = not non_linear_interpretation

  let emit_missing_inter lex lst =
    let lex_name, loc = name lex in
    let abs_name, _ = Data_Signature.name lex.abstract_sig in
    Errors.(LexiconErrors.emit (Lexicon_l.MissingInterpretations (lex_name, abs_name, lst)) ~loc)

  let rec interpret_type abs_ty ({ abstract_sig = abs_sg; dico; _ } as lex) =                         
    match abs_ty with
    | Lambda.Atom i -> (
        let () =
          assert (
            snd (Data_Signature.id_to_string abs_sg i)
            = Format.asprintf "%a" (Data_Signature.pp_type abs_sg) abs_ty)
        in
        let abs_ty_as_str = snd (Data_Signature.id_to_string abs_sg i) in
        match Dico.find (abs_ty_as_str, Pair.Type) dico with
        | Type (_, obj_ty) -> Data_Signature.expand_type obj_ty lex.object_sig
        | Constant _ -> failwith "Bug"
        | exception Not_found -> emit_missing_inter lex [ abs_ty_as_str ])
    | Lambda.DAtom i ->
        interpret_type (Data_Signature.unfold_type_definition i abs_sg) lex
    | Lambda.LFun (ty1, ty2) ->
        if lex.non_linear_interpretation then
          Lambda.Fun (interpret_type ty1 lex, interpret_type ty2 lex)
        else Lambda.LFun (interpret_type ty1 lex, interpret_type ty2 lex)
    | Lambda.Fun (ty1, ty2) ->
        Lambda.Fun (interpret_type ty1 lex, interpret_type ty2 lex)
    | _ -> failwith "Not yet implemented"

  let rec interpret_term abs_t ({ abstract_sig = abs_sg; dico; _ } as lex) =
    match abs_t with
    | Lambda.Var _ -> abs_t
    | Lambda.LVar i ->
        if lex.non_linear_interpretation then Lambda.Var i else abs_t
    | Lambda.Const _ -> (
        let abs_term_as_str =
          Format.asprintf "%a" (Data_Signature.pp_term abs_sg) abs_t
        in
        match Dico.find (abs_term_as_str, Pair.Cst) dico with
        | Constant (_, obj_t) -> obj_t
        | Type _ -> failwith "Bug"
        | exception Not_found -> emit_missing_inter lex [ abs_term_as_str ])
    | Lambda.DConst i ->
        interpret_term (Data_Signature.unfold_term_definition i abs_sg) lex
    | Lambda.Abs (x, t) -> Lambda.Abs (x, interpret_term t lex)
    | Lambda.LAbs (x, t) ->
        if lex.non_linear_interpretation then
          Lambda.Abs (x, interpret_term t lex)
        else Lambda.LAbs (x, interpret_term t lex)
    | Lambda.App (t, u) ->
        Lambda.App (interpret_term t lex, interpret_term u lex)
    | _ -> failwith "Not yet implemented"

  let interpret t ty lex =
    let t_interpretation = interpret_term t lex in
    let t_interpretation =
      Lambda.normalize
        ~id_to_term:(fun i ->
          Data_Signature.unfold_term_definition i lex.object_sig)
        t_interpretation
    in
    let ty_interpretation = interpret_type ty lex in
    (t_interpretation, ty_interpretation)

  let pp fmt
      ({ dico = d; abstract_sig = abs_sg; object_sig = obj_sg; _ }
      as lex) =
    let pp_dico fmt dico =
      Dico.iter
        (fun (id, _) i ->
          Format.fprintf fmt "@[<hv 2>%s :=@ %a;@]@;" id
            (pp_interpretation
               (fun id ->
                 interpret_type (Data_Signature.type_of_constant id abs_sg) lex)
               i obj_sg)
            id)
        dico
    in
    let () = Format.fprintf fmt "@[<hv 2>@[" in
    let () = short_pp fmt lex in
    let () =
      Format.fprintf fmt " =@]@,@[<v>%a@]@," pp_dico d
    in
    let () = Format.fprintf fmt "-----------------------------------@," in
    match lex.datalog_prog with
    | None ->
        Format.fprintf fmt
          "@[This@ lexicon@ was@ not@ recognized@ as@ having@ a@ 2nd-order@ \
           abstract@ signature@]@]"
    | Some { prog = p; _ } ->
        Format.fprintf fmt
          "@[This@ lexicon@ is@ recognized@ as@ having@ a@ 2nd-order@ abstract@ \
           signature.@ The@ associated@ datalog@ program@ is:@,\
           @[<v> @[%a@]@]" (DatalogAbstractSyntax.Program.pp ~with_position:false ~with_id:true)
          (Datalog.Program.to_abstract p)



  module Reduction = Reduction.Make (Data_Signature)

  (* This functions generates a new symbol for an extensional datalog
     predicate that corresponds to an object constant in case the
     symbol [s] being processed is already an atomic type, i.e., gave
     rise to an intensional predicate.

     It is ensured that the newly generated symbol does not conflict
     neither with another atomic type, another object constant, nor
     with an already generated symbol.

     The functions returns the new symbol (unchanged if not necessary)
     and the new set of generated symbols (unchanged if not
     necessary). *)
  let generate_unambiguous_obj_sym lex cst (map, syms) =
    let rec disambiguate id l_s =
      let () = Log.debug (fun m -> m "Testing \"%s\"" l_s) in
      if
        Data_Signature.is_type ~atomic:true l_s lex.abstract_sig
        || Utils.StringSet.mem l_s syms
        ||
        match Data_Signature.is_constant l_s lex.object_sig with
        | true, Some (_, false, _) -> true
        | _, _ -> false
      then disambiguate id (Printf.sprintf "%s__" l_s)
      else
        let () = Log.debug (fun m -> m "Succeeded!") in
        (l_s, (Utils.IntMap.add id l_s map, Utils.StringSet.add l_s syms))
    in
    let cst_name =
      Format.asprintf "%a" (Data_Signature.pp_term lex.object_sig) cst
    in
    (* Check if the object constant corresponds to an atomic type *)
    if Data_Signature.is_type ~atomic:true cst_name lex.abstract_sig then
      (* It does *)
      let () =
        Log.debug (fun m ->
            m "Needs to define a new symbol instead of \"%s\"" cst_name)
      in
      let new_sym =
        Printf.sprintf "%s__%s__" cst_name
          (fst (Data_Signature.name lex.object_sig))
      in
      (* Get the id of the constant *)
      let cst_id =
        match cst with
        | Lambda.Const i -> i
        | _ ->
            failwith
              "Bug: Predicates should be build only for declared constants"
      in
      disambiguate cst_id new_sym
    else (* It does not: do nothing*)
      (cst_name, (map, syms))

  let add_rule_for_cst_in_prog name duplicated abs_type interpreted_term lex
      { prog; magic_programs; rule_to_cst; cst_to_rule; generated_symbols } =
    let interpreted_type = interpret_type abs_type lex in
    let eta_long_term =
      Data_Signature.eta_long_form interpreted_term interpreted_type
        lex.object_sig
    in
    let pp_obj_term = Data_Signature.pp_term lex.object_sig in
    let pp_obj_type = Data_Signature.pp_type lex.object_sig in
    Log.info (fun m ->
        m "term: %a: %a" pp_obj_term interpreted_term pp_obj_type
          interpreted_type);
    Log.info (fun m -> m "eta-long form: %a" pp_obj_term eta_long_term);
    Log.info (fun m ->
        m "eta-long form (as caml term): %s" (Lambda.raw_to_caml eta_long_term));
    Log.info (fun m ->
        m "Datalog rule addition: lexicon \"%s\", constant \"%s: %a\""
          (fst lex.name) name
          (Data_Signature.pp_type lex.abstract_sig)
          abs_type);
    Log.info (fun m ->
        m "mapped to \"%a: %a\"" pp_obj_term eta_long_term pp_obj_type
          interpreted_type);
    let obj_princ_type, obj_typing_env =
      TypeInference.Type.inference eta_long_term
    in
    Log.info (fun m ->
        m "Interpreting \"%s\" as \"%a=%s\" with principle type: \"%s\"" name
          (Data_Signature.pp_term lex.object_sig)
          eta_long_term
          (Lambda.raw_to_caml eta_long_term)
          (Lambda.raw_type_to_string obj_princ_type));
    Log.info (fun m ->
        let pp_typing_env fmt env =
          Utils.IntMap.iter
            (fun k (t, ty) ->
              Format.fprintf fmt "@[%d --> %s : %s@]" k (Lambda.raw_to_string t)
                (Lambda.raw_type_to_string ty))
            env
        in
        m "In the context of:@,@[<v>  @[%a@]@]" pp_typing_env obj_typing_env);
    let rule, new_prog, new_generated_symbols =
      Reduction.generate_and_add_rule ~abs_cst:(name, abs_type) ~obj_princ_type
        ~obj_typing_env ~abs_sig:lex.abstract_sig ~obj_sig:lex.object_sig
        ~update_fct:(generate_unambiguous_obj_sym lex)
        ~syms:generated_symbols prog
    in
    let cst_id, _ = Data_Signature.find_term name lex.abstract_sig in
    let cst_id_as_int =
      match cst_id with
      | Lambda.Const i -> i
      | _ ->
          failwith
            "Bug: Trying to add a rule that does not correspond to a constant"
    in
    let new_prog' =
      if duplicated then
        Datalog.Program.remove_rule
          (Utils.IntMap.find cst_id_as_int cst_to_rule)
          rule.DatalogAbstractSyntax.Rule.lhs
            .DatalogAbstractSyntax.Predicate.p_id new_prog
      else new_prog
    in
    (*    new_prog,RuleToCstMap.add rule.DatalogAbstractSyntax.Rule.id cst_id rule_to_cst *)
    {
      prog = new_prog';
      magic_programs;
      rule_to_cst =
        RuleToCstMap.add rule.DatalogAbstractSyntax.Rule.id cst_id rule_to_cst;
      cst_to_rule =
        Utils.IntMap.add cst_id_as_int rule.DatalogAbstractSyntax.Rule.id
          cst_to_rule;
      (* HERE: TODO: New value*)
      generated_symbols = new_generated_symbols;
    }

  let insert e ({ dico = d; _ } as lex) =
    match e with
    | Abstract_syntax.Type (id, loc, ty) ->
        let interpreted_type = Data_Signature.convert_type ty lex.object_sig in
        {
          lex with
          dico = Dico.add (id, Pair.Type) (Type (loc, interpreted_type)) d;
        }
    | Abstract_syntax.Constant (id, loc, t) ->
        let abs_type =
          Data_Signature.expand_type
            (Data_Signature.type_of_constant id lex.abstract_sig)
            lex.abstract_sig
        in
        let interpreted_type = interpret_type abs_type lex in
        let unfold i = Data_Signature.unfold_term_definition i lex.object_sig in
        let interpretation, is_almost_linear =
          Data_Signature.typecheck t interpreted_type lex.object_sig
        in
        let () =
          if not is_almost_linear then
            Logs.warn (fun m ->
                m
                  "Because@ of@ \"%s :=@ %a :@ %a\",@ the@ lexicon@ \"%a\"@ \
                   is@ not@ almost@ linear."
                  id
                  (Data_Signature.pp_term lex.object_sig)
                  interpretation
                  (Data_Signature.pp_type lex.object_sig)
                  interpreted_type
                  Utils.lex_pp
                  (let name, _ = lex.name in
                   name))
        in
        let interpreted_term =
          Lambda.normalize ~id_to_term:unfold interpretation
        in
        let prog =
          match (lex.datalog_prog, is_almost_linear) with
          | None, _ -> None
          | _, false -> None
          | Some p, true ->
              let duplicated_entry = Dico.mem (id, Pair.Cst) d in
              let new_prog =
                add_rule_for_cst_in_prog id duplicated_entry abs_type
                  (Data_Signature.expand_term interpreted_term lex.object_sig)
                  lex p
              in
              (* When a new constant has been added, it is necessary to regenerate the magic programs *)
              Some { new_prog with magic_programs = None }
        in
        {
          lex with
          dico = Dico.add (id, Pair.Cst) (Constant (loc, interpreted_term)) d;
          datalog_prog = prog;
          is_almost_linear = lex.is_almost_linear && is_almost_linear;
        }

  let rebuild_prog lex =
    match lex.datalog_prog with
    | None -> lex
    | Some _ -> (
        try
          let new_prog =
            Dico.fold
              (fun (id, _) inter acc ->
                match inter with
                | Type (_, _) -> acc
                | Constant (_, t) ->
                    add_rule_for_cst_in_prog id false
                      (* When rebuilding, no risk of dublicated interpretations *)
                      (Data_Signature.expand_type
                         (Data_Signature.type_of_constant id lex.abstract_sig)
                         lex.abstract_sig)
                      t lex acc)
              lex.dico
              {
                prog = Datalog.Program.empty;
                magic_programs = None;
                rule_to_cst = RuleToCstMap.empty;
                cst_to_rule = Utils.IntMap.empty;
                generated_symbols = Utils.IntMap.empty, Utils.StringSet.empty;
              }
          in
          { lex with datalog_prog = Some new_prog }
        with Not_almost_linear -> { lex with is_almost_linear = false })

  let parse ~alt_max ?(magic = true) (term, term_type) dist_type lex =
    let dist_type = Data_Signature.expand_type dist_type lex.abstract_sig in
    let term_type = Data_Signature.expand_type term_type lex.object_sig in
    let term =
      Lambda.normalize
        ~id_to_term:(fun i ->
            Data_Signature.unfold_term_definition i lex.object_sig)
        (Data_Signature.expand_term term lex.object_sig)
    in
    match
      (lex.datalog_prog, dist_type)
    with
    | None, _ ->
      let () =
        Logs.warn (fun m ->
            m "Parsing@ is@ not@ implemented@ for@ non@ 2nd-order@ ACG.")
      in
      SharedForest.SharedForest.Resumptions.empty ~alt_max, [], ( term, dist_type)
    | ( Some { prog; magic_programs = Some q_to_prog_map; generated_symbols; _ },
        (* A magic program is available and the --no-magic option is not set *)
        (Lambda.Atom _ as dist_type) )
      when magic = true ->
      Log.info (fun m -> m "Before parsing. Program is currently:@,@[<v>  @[%a@]@]" (DatalogAbstractSyntax.Program.pp ~with_position:false ~with_id:true) (Datalog.Program.to_abstract prog));
      let dist_type_image = interpret_type dist_type lex in
      if dist_type_image <> term_type then
        let obj_term_type_s = Format.dprintf "%a" (Data_Signature.pp_type lex.object_sig) term_type in
        let abs_dist_type_s = Format.dprintf "%a" (Data_Signature.pp_type lex.abstract_sig) dist_type in
        let interpreted_abs_dist_type_s = Format.dprintf "%a" (Data_Signature.pp_type lex.object_sig) dist_type_image in
        let lex_name = Format.dprintf "%a" pp_lex lex in
        Errors.(CmdErrors.emit (Cmd_l.TypeMismatch (obj_term_type_s, abs_dist_type_s, interpreted_abs_dist_type_s, lex_name)))
      else
        let () = Log.info (fun m ->
            m "Term for the query: %a"
              (Data_Signature.pp_term lex.object_sig)
              term) in
        let obj_term =
          Data_Signature.eta_long_form term dist_type_image lex.object_sig
        in
        let obj_princ_type, obj_typing_env =
          TypeInference.Type.inference obj_term
        in
        Log.debug (fun m ->
            m "Going to set a query for the distinguised type \"%a(%s)\""
              (Data_Signature.pp_type lex.abstract_sig)
              dist_type
              (Lambda.raw_type_to_string dist_type));
        Log.debug (fun m ->
            m "whose image is \"%a(%s)\""
              (Data_Signature.pp_type lex.object_sig)
              dist_type_image
              (Lambda.raw_type_to_string dist_type_image));
        Log.debug (fun m ->
            m "resulting int the principle type \"%s\""
              (Lambda.raw_type_to_string obj_princ_type));
        (* original_query is the datalog query (compute from the
           distinguished type) original_queried_program is the
           unchanged datalog program (no facts from the edb resulting
           from the term to parse are added), and _facts_as_preds is a
           list of facts to be added *)
        (* let original_query, _facts_as_preds,
           original_queried_program = Reduction.only_edb_and_query
           ~obj_term ~obj_type:obj_princ_type ~obj_typing_env
           ~dist_type prog ~abs_sig:lex.abstract_sig
           ~obj_sig:lex.object_sig *)
        let original_query, original_queried_program =
          Reduction.edb_and_query ~obj_term ~obj_type:obj_princ_type
            ~obj_typing_env ~dist_type prog ~abs_sig:lex.abstract_sig
            ~obj_sig:lex.object_sig ~syms:generated_symbols
        in
        let () = Log.debug (fun m -> m "Done (query)") in
        let bfs, _ =
          MagicRewriting.Adornment.adornment ~bound_variables:ASPred.TermSet.empty original_query in
        let () = Log.debug (fun m -> m "Done (adornment of the query)") in
        let magic_program, magic_context =
          match
            MagicRewriting.Rewriting.QueryMap.find_opt
              (original_query.ASPred.p_id, bfs)
              q_to_prog_map
          with
          | None -> failwith "Bug: no magic rewritten program"
          | Some (p, c) ->
            (* the abstract magic program has been retrieved *)
            let abstract_program = Datalog.Program.to_abstract p in
            let () =
              Log.debug (fun m ->
                  m "Found the following magic program for the query '%s':@,@[<v>  @[%a@]@]"
                    (MagicRewriting.Adornment.adorned_predicate_to_string ~pred_table:prog.Datalog.Program.pred_table (original_query, bfs))
                    (ASProg.pp ~with_position:false ~with_id:true)
                    abstract_program)
            in
            let () =
              Log.debug (fun m ->
                  m "It was built from the following unique binding program:@,@[<v>  @[%a@]@]"
                    (ASProg.pp ~with_position:false ~with_id:true)
                    c.MagicRewriting.Rewriting.unique_binding_program)
            in
            ( Datalog.Program.
                { p with const_table = original_queried_program.const_table },
              c )
        in
        (* Add the facts to the magic program *)
        (* CHECK which facts have to be added !!! *)
        (* CHECK it is an adorned query *)
        let query, temp_magic_prog =
          Reduction.edb_and_query ~obj_term ~obj_type:obj_princ_type
            ~obj_typing_env ~dist_type ~adornment:bfs magic_program
            ~abs_sig:lex.abstract_sig ~obj_sig:lex.object_sig ~syms:generated_symbols
        in
        (* CHECK: je ne comprends pas pourquoi la règle seed est ajoutée
           au programme. Ne faudrrait-il pas que ce soit un prédicat
           magic ? Vérifié : c'est bien un prédicat magic qui est ajouté
           au programme magique. *)
        let temp_magic_prog' =
          MagicRewriting.Magic.query_to_seed_concrete query temp_magic_prog
        in
        let () =
          Log.info (fun m ->
              m "Going to solve the query: \"%a\" with the program:@,@[<v>  @[%a@]@]"
                (DatalogAbstractSyntax.Predicate.pp
                   temp_magic_prog'.Datalog.Program.pred_table
                   temp_magic_prog'.Datalog.Program.const_table)  query
                (DatalogAbstractSyntax.Program.pp ~with_position:false ~with_id:true)
                (Datalog.Program.to_abstract temp_magic_prog'))
        in
        let parse_time_start = Timer.top () in
        let _derived_facts, magic_derivations =
          Datalog.Program.seminaive temp_magic_prog'
        in
        let parse_time_end = Timer.top () in
        let () =
          Log.debug (fun m ->
              m "I could derive the following facts:@,@[  @[<v>%a@]@]"
                (Datalog.Predicate.pp_facts
                   temp_magic_prog'.Datalog.Program.pred_table
                   temp_magic_prog'.Datalog.Program.const_table) _derived_facts)
        in
        let () =
          Log.debug (fun m ->
              m "With the following derivations:@,@[<v>  @[%a@]@]"
                (Datalog.Predicate.pp_facts_from_premises ~with_id:true
                   temp_magic_prog'.Datalog.Program.pred_table
                   temp_magic_prog'.Datalog.Program.const_table)
                magic_derivations)
        in
        let () =
          Log.debug (fun m ->
              m "Mapping of unique binding predicates to original program predicates:@[  @[<v>%a@]@]@]"
                (fun fmt unadorned_predicats ->
                   ASPred.PredIdMap.iter
                     (fun p_id_ub p_id_orig ->
                        Format.fprintf
                          fmt
                          "@[%a ---> %a@]@,"
                          (ASPred.pp
                             ~with_id:true
                             magic_context.MagicRewriting.Rewriting.unique_binding_program.ASProg.pred_table
                             DatalogLib.Datalog_AbstractSyntax.ConstGen.Table.empty)
                          ASPred.{ p_id = p_id_ub; arity = 0; arguments = [] }
                          (ASPred.pp
                             ~with_id:true
                             original_queried_program.Datalog.Program.pred_table
                             DatalogLib.Datalog_AbstractSyntax.ConstGen.Table.empty)
                          ASPred.{ p_id = p_id_orig; arity = 0; arguments = [] })
                     unadorned_predicats)
                magic_context.MagicRewriting.Rewriting.adorn_to_unadorm_pred_ids_map)
        in
        let derivations, prog_for_building_forest =
          let rewritten_derivations =
            MagicRewriting.Rewriting.rewrite_derivations magic_derivations
              magic_context
          in
          let () =
            Log.debug (fun m ->
                m "Rewritten derivations:@,@[<v>@[%a@]@]"
                  (Datalog.Predicate.pp_facts_from_premises ~with_id:true
                     original_queried_program.Datalog.Program.pred_table
                     original_queried_program.Datalog.Program.const_table)
                  rewritten_derivations)
          in
          (rewritten_derivations, original_queried_program)
        in
        let () =
          Log.debug (fun m ->
              m "Original query (original program): %a"
                (ASPred.pp ~with_id:true
                   original_queried_program.Datalog.Program.pred_table
                   original_queried_program.Datalog.Program.const_table) original_query)
        in
        let () =
          Log.debug (fun m ->
              m "Magic query: %a"
                (ASPred.pp ~with_id:true
                   temp_magic_prog'.Datalog.Program.pred_table
                   temp_magic_prog'.Datalog.Program.const_table) query)
        in
        let build_forest_start = Timer.top () in
        let parse_forest =
          Datalog.Program.build_forest ~query:original_query derivations
            prog_for_building_forest
        in
        let build_forest_end = Timer.top () in
        let () =
          Logs.app
            (fun m -> m "Parsing time:               %a"
                Timer.diff
                (parse_time_end, parse_time_start)) in
        let () =
          Logs.app
            (fun m -> m "Parse forest building time: %a"
                Timer.diff
                (build_forest_end, build_forest_start)) in
        let resumptions =
          match parse_forest with
          | [] ->
            let () = Log.debug (fun m -> m "The shared forest is empty") in
            SharedForest.SharedForest.Resumptions.empty ~alt_max, [], (term, dist_type)
          | [ f ] ->
            let () =
              Log.debug (fun m -> m "The shared forest is not empty") in
            let forest = f in
            let () =
              Log.debug (fun m ->
                  m
                    "The shared forest is: @[%a@]"
                    (SharedForest.SharedForest.pp_forest Format.pp_print_int)
                    forest)
            in
            SharedForest.SharedForest.init ~alt_max (Format.pp_print_int) f, f, (term, dist_type)
          (*	| a::b::tl -> NewSharedForest.SharedForest.init a *)
          | _ -> failwith "Bug: not fully specified query"
        in
        resumptions
    | Some { prog; magic_programs = None; generated_symbols; _ }, (Lambda.Atom _ as dist_type)
    | Some { prog; magic_programs = _; generated_symbols; _ }, (Lambda.Atom _ as dist_type) ->
      let dist_type_image = interpret_type dist_type lex in
      if dist_type_image <> term_type then
        let obj_term_type_s = Format.dprintf "%a" (Data_Signature.pp_type lex.object_sig) term_type in
        let abs_dist_type_s = Format.dprintf "%a" (Data_Signature.pp_type lex.abstract_sig) dist_type in
        let interpreted_abs_dist_type_s = Format.dprintf "%a" (Data_Signature.pp_type lex.object_sig) dist_type_image in
        let lex_name = Format.dprintf "%a" pp_lex lex in
        Errors.(CmdErrors.emit (Cmd_l.TypeMismatch (obj_term_type_s, abs_dist_type_s, interpreted_abs_dist_type_s, lex_name)))
      else
      let term =
        Lambda.normalize
          ~id_to_term:(fun i ->
              Data_Signature.unfold_term_definition i lex.object_sig)
          (Data_Signature.expand_term term lex.object_sig)
      in
      Log.info (fun m ->
          m "Term for the query: %a"
            (Data_Signature.pp_term lex.object_sig) term);
      let obj_term =
        Data_Signature.eta_long_form term dist_type_image lex.object_sig
      in
      let obj_princ_type, obj_typing_env =
        TypeInference.Type.inference obj_term
      in
      Log.debug (fun m ->
          m "Going to set a query for the distinguised type \"%a(%s)\""
            (Data_Signature.pp_type lex.abstract_sig)  dist_type
            (Lambda.raw_type_to_string dist_type));
      Log.debug (fun m ->
          m "whose image is \"%a(%s)\""
            (Data_Signature.pp_type lex.object_sig)  dist_type_image
            (Lambda.raw_type_to_string dist_type_image));
      Log.debug (fun m ->
          m "resulting in the principle type \"%s\""
            (Lambda.raw_type_to_string obj_princ_type));
      (* query is the datalog query (compute from the distinguished
         type) and temp_prog is the program augmented with the
         extensional database resulting from the term to parse *)
      let query, temp_prog =
        Reduction.edb_and_query ~obj_term ~obj_type:obj_princ_type
          ~obj_typing_env ~dist_type prog ~abs_sig:lex.abstract_sig
          ~obj_sig:lex.object_sig ~syms:generated_symbols
      in
      let parse_time_start = Timer.top () in
      let _, derivations = Datalog.Program.seminaive temp_prog in
      let parse_time_end = Timer.top () in
      let () =
        Log.debug (fun m ->
            m "Derivations:@,@[<v>@[%a@]@]"
              (Datalog.Predicate.pp_facts_from_premises ~with_id:true
                 temp_prog.Datalog.Program.pred_table
                 temp_prog.Datalog.Program.const_table)
              derivations)
      in      
      let build_forest_start = Timer.top () in
      let parse_forest =
        Datalog.Program.build_forest ~query derivations temp_prog
      in
      let build_forest_end = Timer.top () in
      let () =
        Logs.app
          (fun m -> m "Parsing time:               %a"
              Timer.diff
              (parse_time_end, parse_time_start)) in
      let () =
        Logs.app
          (fun m -> m "Parse forest building time: %a"
              Timer.diff
              (build_forest_end, build_forest_start)) in
      let resumptions =
        match parse_forest with
        | [] ->
          let () = Log.debug (fun m -> m "The shared forest is empty") in
          SharedForest.SharedForest.Resumptions.empty ~alt_max, [], (term, dist_type)
        | [ f ] ->
          let () =
            Log.debug (fun m -> m "The shared forest is not empty") in
          let forest = f in
          let () =
            Log.debug (fun m ->
                m
                  "The shared forest is:@[%a@]"
                  (SharedForest.SharedForest.pp_forest Format.pp_print_int)
                  forest)
          in
          SharedForest.SharedForest.init ~alt_max (Format.pp_print_int) f, f, (term, dist_type)
        (*	| a::b::tl -> NewSharedForest.SharedForest.init a *)
        | _ -> failwith "Bug: not fully specified query"
      in
      resumptions
    | Some _, _ ->
      let () =
        Logs.warn (fun m ->
            m
              "Parsing@ is@ not@ yet@ implemented@ for@ non-atomic@ \
               distinguished@ type.")
      in
      SharedForest.SharedForest.Resumptions.empty ~alt_max, [], (term, dist_type)

  let get_analysis (resumptions, initial_forest, object_term) lex =
    Log.debug (fun m -> m "Trying to get some analysis");
    match lex.datalog_prog with
    | None ->
        let () =
          Logs.warn (fun m ->
              m
                "Parsing@ is@ not@ yet@ implemented@ for@ non-atomic@ \
                 distinguished@ type.")
        in
        (None, (resumptions, initial_forest, object_term))
    | Some { rule_to_cst = rule_id_to_cst; _ } -> (
        match SharedForest.SharedForest.resume resumptions with
        | None, resumptions -> (None, (resumptions, initial_forest, object_term))
        | Some (t, weight), resumptions ->
          let res = Containers.TreeContext.Tree.fold_depth_first
              ( (fun rule_id -> RuleToCstMap.find rule_id rule_id_to_cst),
                fun x y -> Lambda.App (x, y) )
              t in          
          let () =
            ParsingLog.info
              (fun m ->
                 let test = 
                   let obj_term, dist_type = object_term in
                   let interpreted_type = Data_Signature.expand_type (interpret_type dist_type lex) lex.object_sig in
                   (* Check that the interpretation of the later is the former *)
                   Lambda.equal
                     ~id_to_term:(fun i -> Data_Signature.unfold_term_definition i lex.object_sig)
                     ~type_of_const:(fun i -> Data_Signature.(expand_type (type_of_constant (snd (id_to_string lex.object_sig i)) lex.object_sig) lex.object_sig))
                     (obj_term, interpreted_type)
                     (interpret res (Data_Signature.expand_type dist_type lex.abstract_sig) lex) in
                 let () = m "Checking@ that@ the@ interpretation@ of@ the@ parsing@ result@ and@ the@ term@ to@ parse@ are@ the@ same: %B" test in
                 assert test) in  
          ( Some(res, weight ),
            (resumptions, initial_forest, object_term) ))
      
  let is_empty (resumptions, _, _) = SharedForest.SharedForest.Resumptions.is_empty resumptions

  let get_program lex =
    match lex.datalog_prog with None -> None | Some { prog = p; _ } -> Some p

  let check_intentional_predicates lex =
    if Data_Signature.is_2nd_order lex.abstract_sig then
      match lex.datalog_prog with
      | None -> () (*lex *)
      | Some ({ prog; magic_programs = _; rule_to_cst = _; cst_to_rule = _ ; generated_symbols = _} as _correspondance) ->
        let _new_ids_to_rules_map =
          List.fold_left
            (fun ids_to_rules p_id ->
               match DatalogPredMap.find_opt p_id ids_to_rules with
               | Some rules when not (DatalogRule.Rules.is_empty rules) -> ids_to_rules
               | _ ->
                 let () =
                   Logs.warn (fun m ->
                       m
                         "The@ ACG@ defined@ by@ lexicon@ \"%a\"@ is@ \
                          second-order,@ but@ the@ abstract@ type@ \"%s\"@ is@ \
                          never@ the@ resulting@ type@ of@ an@ abstract@ \
                          constant,@ although@ it@ is@ used@ as@ argument@ \
                          type@ for@ some@ constant."
                         Utils.lex_pp
                         (let name, _ = lex.name in
                          name)
                         (ASPred.PredIdTable.find_sym_from_id p_id
                            prog.Datalog.Program.pred_table)) in
                 DatalogPredMap.add p_id DatalogRule.Rules.empty ids_to_rules)
            prog.Datalog.Program.rules
            prog.Datalog.Program.idb in
        ()
    else ()

  let check ({ dico = d; abstract_sig = abs; _ } as lex) =
    let missing_interpretations =
      Data_Signature.fold
        (fun e acc ->
          match Data_Signature.is_declared e abs with
          | Some s -> (
              match Data_Signature.entry_to_data e with
              | Data_Signature.Type _ ->
                  if Dico.mem (s, Pair.Type) d then acc else s :: acc
              | Data_Signature.Term _ ->
                  if Dico.mem (s, Pair.Cst) d then acc else s :: acc)
          | None -> acc)
        [] abs
    in
    match missing_interpretations with
    | [] -> check_intentional_predicates lex
    | lst -> emit_missing_inter lex lst

  let rebuild_interpetation lex =
    match lex.syntax_dico with
    | None ->
        failwith
          "bug: a rebuild of a lexicon defined as composition was triggered"
    | Some syntax_dico ->
        let prog =
          (*	 if (Data_Signature.is_2nd_order lex.abstract_sig) && (not lex.non_linear_interpretation) then *)
          if Data_Signature.is_2nd_order lex.abstract_sig then
            (*	   Some (Datalog.Program.empty,RuleToCstMap.empty)  *)
            Some
              {
                prog = Datalog.Program.empty;
                magic_programs = None;
                rule_to_cst = RuleToCstMap.empty;
                cst_to_rule = Utils.IntMap.empty;
                generated_symbols = (Utils.IntMap.empty, Utils.StringSet.empty);
              }
          else None
        in
        let new_lex =
          Dico.fold
            (fun _ abs_syntax_tree lex -> insert abs_syntax_tree lex)
            syntax_dico
            { lex with dico = Dico.empty; datalog_prog = prog }
        in
        { new_lex with timestamp = Unix.time () }
    [@@warning "-32"]

  
  
  let compose lex1 lex2 n =
    let temp_lex =
      {
        name = n;
        dico =
          Dico.fold
            (fun key inter acc ->
              match inter with
              | Type (l, stype) ->
                  Dico.add key (Type (l, interpret_type stype lex1)) acc
              | Constant (l, t) ->
                  Dico.add key
                    (Constant
                       ( l,
                         Lambda.normalize
                           ~id_to_term:(fun i ->
                             Data_Signature.unfold_term_definition i
                               lex1.object_sig)
                           (interpret_term t lex1) ))
                    acc)
            lex2.dico Dico.empty;
        syntax_dico = None;
        abstract_sig = lex2.abstract_sig;
        object_sig = lex1.object_sig;
        datalog_prog = lex2.datalog_prog;
        non_linear_interpretation =
          lex1.non_linear_interpretation || lex2.non_linear_interpretation;
        build = Compose [fst (name lex1); fst(name lex2)];
        timestamp = Unix.time ();
        is_almost_linear = true;
      }
    in
    rebuild_prog temp_lex

  let rec interpret_by_lexicons ~interpretation term_or_type lexicons =
    match lexicons with
    | [] -> term_or_type
    | (l,_) :: tl ->
        interpret_by_lexicons ~interpretation (interpretation term_or_type l) tl


  let term_interpretation_and_normalization t l =
    let  interpreted_term = interpret_term t l in
    Lambda.normalize
      ~id_to_term:(fun i ->
          Data_Signature.unfold_term_definition i
            l.object_sig)
      interpreted_term
  
  let compose_lexicons lexicons n =
    (* lexicons are supposed to be in the interpretation order,
       i.e. [l1; l2; l3; … ; ln] for ln∘….∘l3∘l2∘l1 *)
    match lexicons with
    | [] -> failwith "Bug: composing an empty sequence of lexicons"
    | (lex,pos) :: tl ->
      let (last_lex, _), non_linear_interpretation =
        List.fold_left
          (fun ((previous_lex,pos1), non_linear_interpretation) (l_lex,pos2) ->
             match Data_Signature.name previous_lex.object_sig, Data_Signature.name l_lex.abstract_sig with
             | (l1_name,_), (l2_name, _) when l1_name <> l2_name ->
               let new_loc = fst pos2, snd pos1 in
               Errors.(LexiconErrors.emit (Lexicon_l.NotComposable (fst n, fst previous_lex.name, fst l_lex.name)) ~loc:new_loc)
             | _ ->
               (l_lex, pos2),
               non_linear_interpretation || l_lex.non_linear_interpretation)
          ((lex,pos), lex.non_linear_interpretation)
          tl in
      let temp_lex =
        {
          name = n;
          dico =
            Dico.fold
              (fun key inter acc ->
                 match inter with
                 | Type (l, stype) ->
                   Dico.add key (Type (l, interpret_by_lexicons
                                         ~interpretation:(fun stype l_lex ->
                                             interpret_type stype l_lex)
                                         stype
                                         tl)) acc
                 | Constant (l, t) ->
                   Dico.add key
                     (Constant
                        ( l,
                          (interpret_by_lexicons ~interpretation:term_interpretation_and_normalization t tl) ))
                     acc)
              lex.dico Dico.empty;
          syntax_dico = None;
          abstract_sig = lex.abstract_sig;
          object_sig = last_lex.object_sig;
          datalog_prog = lex.datalog_prog;
          non_linear_interpretation = non_linear_interpretation;
          build = Compose ((fst (name lex) :: (List.map (fun (l, _) -> fst (name l)) tl))) ;
          timestamp = Unix.time ();
          is_almost_linear = true;
        }
      in
      rebuild_prog temp_lex
        
  let pp_query lex fmt (term, dist_type) =
    match
      (lex.datalog_prog, Data_Signature.expand_type dist_type lex.abstract_sig)
    with
    | None, _ ->
        Logs.warn (fun m ->
            m "Parsing is not implemented for non 2nd order ACG")
    | Some { prog; generated_symbols; _ }, (Lambda.Atom _ as dist_type) ->
        let dist_type_image = interpret_type dist_type lex in
        let obj_term =
          Data_Signature.eta_long_form
            (Lambda.normalize
               ~id_to_term:(fun i ->
                 Data_Signature.unfold_term_definition i lex.object_sig)
               (Data_Signature.expand_term term lex.object_sig))
            dist_type_image lex.object_sig
        in
        let obj_princ_type, obj_typing_env =
          TypeInference.Type.inference obj_term
        in
        let query, temp_prog =
          Reduction.edb_and_query ~obj_term ~obj_type:obj_princ_type
            ~obj_typing_env ~dist_type prog ~abs_sig:lex.abstract_sig
            ~obj_sig:lex.object_sig ~syms:generated_symbols
        in
        Format.fprintf fmt
          "@[Facts:@,@[<v>  @[<v>%a@]@]@]@,@[Query:@,@[<v>  @[%a?@]@]@]"
          Datalog.Program.pp_edb temp_prog
          (DatalogAbstractSyntax.Predicate.pp
             temp_prog.Datalog.Program.pred_table
             temp_prog.Datalog.Program.const_table)
          query
    | Some _, _ ->
        Logs.warn (fun m -> m 
          "Parsing is not yet implemented for non atomic distinguished type")

  let magic lex =
    match lex.datalog_prog with
    | None -> lex
    | Some prog
      when prog.magic_programs = None
        && Data_Signature.is_2nd_order lex.abstract_sig ->
      let rules = prog.prog.Datalog.Program.abstract_rules in
      let t = Timer.top () in
      let abs_prog =
        ASProg.
          {
            rules;
            pred_table = prog.prog.Datalog.Program.pred_table;
            const_table = prog.prog.Datalog.Program.const_table;
            i_preds = ASPred.PredIds.of_list prog.prog.Datalog.Program.idb;
            rule_id_gen = prog.prog.Datalog.Program.rule_id_gen;
            head_to_rules =
              ASRule.Rules.fold
                (fun r acc ->
                   match
                     ASPred.PredIdMap.find_opt r.ASRule.lhs.ASPred.p_id acc
                   with
                   | None ->
                     ASPred.PredIdMap.add r.ASRule.lhs.ASPred.p_id
                       (ASRule.Rules.singleton r) acc
                   | Some ruls ->
                     ASPred.PredIdMap.add r.ASRule.lhs.ASPred.p_id
                       (ASRule.Rules.add r ruls) acc)
                rules ASPred.PredIdMap.empty;
            e_pred_to_rules = ASPred.PredIdMap.empty;
          }
      in
      let () = Timer.debug (fun m ->
          m "@[Converting@ Datalog@ program@ for@ %a@ to@ abstract@ \
             progam@ before@ magic@ rewritting@ took: %a@]"
            pp_lex lex UtilsLib.Timer.elapsed t) in
      let starting_magic_computation = Timer.top () in
      let progs =
        MagicRewriting.Rewriting.rewrite_programs
          ~msg:(Printf.sprintf "Lexicon '%s'" (fst lex.name))
          abs_prog
      in
      let ending_magic_computation = Timer.top () in
      let magic_programs =
        MagicRewriting.Rewriting.QueryMap.mapi
          (fun (p_id, bfs) (as_prog, ctx) ->
             let () = 
               MagicLog.info (fun m ->
                   m "Making magic program for lexicon %s and query %s_%s \
                      (%d rules)@?"
                     (fst lex.name)
                     (ASPred.PredIdTable.find_sym_from_id p_id
                        prog.prog.Datalog.Program.pred_table)
                     (MagicRewriting.Adornment.to_string bfs)
                     (ASRule.Rules.cardinal as_prog.ASProg.rules)) in
             let () =
               MagicLog.debug (fun m ->
                   m "Abstract program (%s) for %s_%s is:@,@[<v>@[%a@]@]" (fst lex.name)
                     (ASPred.PredIdTable.find_sym_from_id p_id
                        prog.prog.Datalog.Program.pred_table)
                     (MagicRewriting.Adornment.to_string bfs)
                     (ASProg.pp ~with_position:false ~with_id:true)
                     as_prog)
             in
             (Datalog.Program.make_program as_prog, ctx))
          progs
      in
      let ending_compile_all_programs = Timer.top () in
      let () =
        Timer.debug (fun m ->
            m "@[<v2>Magic programs for lexicon %a:@,@[<hv>Build time:   %a@]@,@[Compile time: %a@]@]"
              pp_lex
              lex
              Timer.diff
              (ending_magic_computation, starting_magic_computation)
              Timer.diff
              (ending_compile_all_programs, ending_magic_computation)) in
      let prog' = { prog with magic_programs = Some magic_programs } in
      { lex with datalog_prog = Some prog' }
    | Some _prog -> lex
  (* Don't need to rebuild magic programs for a lexicon whose magic
     program is not set to [None]. A magic programs is set to None
     whenever the lexicon has been modified through [insert],
     [compose] or [update] *)

  let has_magic lex =
    match lex.datalog_prog with
    | None -> Unavailable
    | Some prog when prog.magic_programs = None -> Available_wo_magic
    | Some _ -> Available_with_magic
end