Source file miniml.ml

(************************************************************************)
(*         *      The Rocq Prover / The Rocq Development Team           *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(*s Target language for extraction: a core ML called MiniML. *)

open Names

module InfvInst =
struct
  type t = bool array (* true if informative *)
  let empty = [||]
  let compare i1 i2 = CArray.compare Bool.compare i1 i2
  let equal i1 i2 = Int.equal (compare i1 i2) 0

  let generate actx =
    let names = UVars.AbstractContext.names actx in
    let quals = Array.length names.UVars.quals in
    let init n =
      let ans = Array.make quals true in
      let n = ref n in
      for i = 0 to quals - 1 do
        let b = !n mod 2 = 0 in
        ans.(i) <- b;
        n := !n / 2
      done;
      ans
    in
    List.init (1 lsl quals) init

  let default actx =
    let names = UVars.AbstractContext.names actx in
    let quals = Array.length names.UVars.quals in
    Array.make quals true

  let ground inst =
    let qvars, _ = UVars.Instance.to_array inst in
    let map q = match q with
    | Sorts.Quality.QConstant (QProp | QSProp) -> false
    | Sorts.Quality.QConstant QType -> true
    | Sorts.Quality.QVar qv ->
      match Sorts.QVar.repr qv with
      | Var _ -> CErrors.anomaly (Pp.str "Non-ground instance")
      | Unif _ | Global _ -> true (* informative by default *)
    in
    Array.map map qvars

  let instantiate actx inst =
    let u = UVars.make_abstract_instance actx in
    let fl l = l in
    let fq q = match Sorts.QVar.var_index q with
    | None -> assert false
    | Some i ->
      if inst.(i) then Sorts.Quality.qtype
      else Sorts.Quality.qsprop
    in
    UVars.Instance.subst_fn (fq, fl) u

  let encode inst =
    if Array.for_all (fun b -> b) inst then None
    else
      let len = Array.length inst in
      Some (String.init len (fun i -> if inst.(i) then 'X' else 'O'))

end

type global = { glob : GlobRef.t; inst : InfvInst.t }

(* The [signature] type is used to know how many arguments a CIC
   object expects, and what these arguments will become in the ML
   object. *)

(* We eliminate from terms:
   1) types
   2) logical parts
   3) user-declared implicit arguments of a constant of constructor
*)

type kill_reason =
  | Ktype
  | Kprop
  | Kimplicit of global * int  (* n-th arg of a cst or construct *)

type sign = Keep | Kill of kill_reason

(* Convention: outmost lambda/product gives the head of the list. *)

type signature = sign list

(*s ML type expressions. *)

type ml_type =
  | Tarr    of ml_type * ml_type
  | Tglob   of global * ml_type list
  | Tvar    of int
  | Tvar'   of int (* same as Tvar, used to avoid clash *)
  | Tmeta   of ml_meta (* used during ML type reconstruction *)
  | Tdummy  of kill_reason
  | Tunknown
  | Taxiom

and ml_meta = { id : int; mutable contents : ml_type option }

(* ML type schema.
   The integer is the number of variable in the schema. *)

type ml_schema = int * ml_type

(*s ML inductive types. *)

type inductive_kind =
  | Singleton
  | Coinductive
  | Standard
  | Record of global option list (* None for anonymous field *)

(* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body].
   If the inductive is logical ([ip_logical = false]), then all other fields
   are unused. Otherwise,
   [ip_sign] is a signature concerning the arguments of the inductive,
   [ip_vars] contains the names of the type variables surviving in ML,
   [ip_types] contains the ML types of all constructors.
*)

type ml_ind_packet = {
  ip_typename : Id.t;
  ip_typename_ref : global;
  ip_consnames : Id.t array;
  ip_consnames_ref : global array;
  ip_logical : bool;
  ip_sign : signature;
  ip_vars : Id.t list;
  ip_types : (ml_type list) array
}

(* [ip_nparams] contains the number of parameters. *)

type equiv =
  | NoEquiv
  | Equiv of KerName.t
  | RenEquiv of string

type ml_ind = {
  ind_kind : inductive_kind;
  ind_nparams : int;
  ind_packets : ml_ind_packet array;
  ind_equiv : equiv
}

(*s ML terms. *)

type ml_ident =
  | Dummy
  | Id of Id.t
  | Tmp of Id.t

(** We now store some typing information on constructors
    and cases to avoid type-unsafe optimisations. This will be
    either the type of the applied constructor or the type
    of the head of the match.
*)

(** Nota : the constructor [MLtuple] and the extension of [MLcase]
    to general patterns have been proposed by P.N. Tollitte for
    his Relation Extraction plugin. [MLtuple] is currently not
    used by the main extraction, as well as deep patterns. *)

type ml_branch = ml_ident list * ml_pattern * ml_ast

and ml_ast =
  | MLrel    of int
  | MLapp    of ml_ast * ml_ast list
  | MLlam    of ml_ident * ml_ast
  | MLletin  of ml_ident * ml_ast * ml_ast
  | MLglob   of global
  | MLcons   of ml_type * global * ml_ast list
  | MLtuple  of ml_ast list
  | MLcase   of ml_type * ml_ast * ml_branch array
  | MLfix    of int * Id.t array * ml_ast array
  | MLexn    of string
  | MLdummy  of kill_reason
  | MLaxiom  of string
  | MLmagic  of ml_ast
  | MLuint   of Uint63.t
  | MLfloat  of Float64.t
  | MLstring of Pstring.t
  | MLparray of ml_ast array * ml_ast

and ml_pattern =
  | Pcons   of global * ml_pattern list
  | Ptuple  of ml_pattern list
  | Prel    of int (** Cf. the idents in the branch. [Prel 1] is the last one. *)
  | Pwild
  | Pusual  of global (** Shortcut for Pcons (r,[Prel n;...;Prel 1]) **)

(*s ML declarations. *)

type ml_decl =
  | Dind  of ml_ind
  | Dtype of global * Id.t list * ml_type
  | Dterm of global * ml_ast * ml_type
  | Dfix  of global array * ml_ast array * ml_type array

type ml_spec =
  | Sind  of ml_ind
  | Stype of global * Id.t list * ml_type option
  | Sval  of global * ml_type

type ml_specif =
  | Spec of ml_spec
  | Smodule of ml_module_type
  | Smodtype of ml_module_type

and ml_module_type =
  | MTident of ModPath.t
  | MTfunsig of MBId.t * ml_module_type * ml_module_type
  | MTsig of ModPath.t * ml_module_sig
  | MTwith of ml_module_type * ml_with_declaration

and ml_with_declaration =
  | ML_With_type of InfvInst.t * Id.t list * Id.t list * ml_type
  | ML_With_module of Id.t list * ModPath.t

and ml_module_sig = (Label.t * ml_specif) list

type ml_structure_elem =
  | SEdecl of ml_decl
  | SEmodule of ml_module
  | SEmodtype of ml_module_type

and ml_module_expr =
  | MEident of ModPath.t
  | MEfunctor of MBId.t * ml_module_type * ml_module_expr
  | MEstruct of ModPath.t * ml_module_structure
  | MEapply of ml_module_expr * ml_module_expr

and ml_module_structure = (Label.t * ml_structure_elem) list

and ml_module =
    { ml_mod_expr : ml_module_expr;
      ml_mod_type : ml_module_type }

(* NB: we do not translate the [mod_equiv] field, since [mod_equiv = mp]
   implies that [mod_expr = MEBident mp]. Same with [msb_equiv]. *)

type ml_structure = (ModPath.t * ml_module_structure) list

type ml_signature = (ModPath.t * ml_module_sig) list

type unsafe_needs = {
  mldummy : bool;
  tdummy : bool;
  tunknown : bool;
  magic : bool
}

type 's language_descr = {
  keywords : Id.Set.t;

  (* Concerning the source file *)
  file_suffix : string;
  file_naming : 's -> ModPath.t -> string;
  (* the second argument is a comment to add to the preamble *)
  preamble :
    's -> Id.t -> Pp.t option -> ModPath.t list -> unsafe_needs ->
    Pp.t;
  pp_struct : 's -> ml_structure -> Pp.t;

  (* Concerning a possible interface file *)
  sig_suffix : string option;
  (* the second argument is a comment to add to the preamble *)
  sig_preamble :
    's -> Id.t -> Pp.t option -> ModPath.t list -> unsafe_needs ->
    Pp.t;
  pp_sig : 's -> ml_signature -> Pp.t;

  (* for an isolated declaration print *)
  pp_decl : 's -> ml_decl -> Pp.t;

}