interface.ml 5.01 KB
Newer Older
1 2 3 4
(**************************************************************************)
(*                                                                        *)
(*                 ACG development toolkit                                *)
(*                                                                        *)
5
(*                  Copyright 2008-2018 INRIA                             *)
6
(*                                                                        *)
7
(*  More information on "http://acg.gforge.inria.fr/"                     *)
8 9 10 11 12 13 14 15 16 17 18 19
(*  License: CeCILL, see the LICENSE file or "http://www.cecill.info"     *)
(*  Authors: see the AUTHORS file                                         *)
(*                                                                        *)
(*                                                                        *)
(*                                                                        *)
(*                                                                        *)
(*  $Rev::                              $:  Revision of last commit       *)
(*  $Author::                           $:  Author of last commit         *)
(*  $Date::                             $:  Date of last commit           *)
(*                                                                        *)
(**************************************************************************)

20 21
open Logic.Abstract_syntax
open Logic.Lambda
22

23

24 25 26 27
module type Signature_sig =
sig
  exception Duplicate_type_definition
  exception Duplicate_term_definition
28
  exception Not_found
29 30

  type t
31
  type entry
32

33
  type term
34
  type stype
35 36 37 38
  type data =
    | Type of stype
    | Term of (term*stype)

39 40 41
  val empty : (string*Abstract_syntax.location) -> t
  val name : t -> (string*Abstract_syntax.location)
  val add_entry : Abstract_syntax.sig_entry -> t -> t
42 43
  (* REVIEW: Commented out because of still missing impl. *)
  (* val find_type : string -> t -> stype *)
44
  val find_term : string -> t -> term * stype
45
  val is_type : string -> t -> bool
46
  val is_constant : string -> t -> bool*Abstract_syntax.syntactic_behavior option
47 48
  val precedence : string -> t -> (float*Abstract_syntax.associativity) option
  val new_precedence : t -> (float * t)
49 50
  val type_to_string : stype -> t -> string
  val term_to_string : term -> t -> string
51
  val id_to_string : t -> int -> Abstract_syntax.syntactic_behavior*string
52 53
  val type_to_formatted_string : Format.formatter -> stype -> t -> unit
  val term_to_formatted_string : Format.formatter -> term -> t -> unit
54 55 56
(*  val type_to_string : stype -> t -> string*)
  val unfold_type_definition : int -> t -> Lambda.stype 
  val unfold_term_definition : int -> t -> Lambda.term 
57 58 59
  val expand_type : Lambda.stype -> t -> Lambda.stype
  val expand_term : Lambda.term -> t -> Lambda.term

60
  val add_warnings : Error.warning list -> t -> t
61
  (*  val get_warnings : t -> Error.warning list *)
62
  val to_string : t -> string
63
(*  val term_to_string : term -> t -> string *)
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
64
(*  val raw_to_string : term -> string*)
65 66 67 68 69
  val convert_term : Abstract_syntax.term  -> Abstract_syntax.type_def -> t -> term*stype
  val convert_type : Abstract_syntax.type_def -> t -> stype
  val type_of_constant : string -> t -> stype
  val typecheck : Abstract_syntax.term -> stype -> t -> term
  val fold : (entry -> 'a -> 'a) -> 'a -> t -> 'a
70
  val entry_to_data : entry -> data 
71
  val get_binder_argument_functional_type : string -> t -> Abstract_syntax.abstraction option
72
  val is_declared : entry -> t -> string option
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
73
  val eta_long_form : term -> stype -> t -> term
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
74
  val unfold : term -> t -> term
75 76
  val is_2nd_order : t -> bool

77 78 79 80 81 82 83 84
end

module type Lexicon_sig =
sig
  exception Duplicate_type_interpretation
  exception Duplicate_constant_interpretation

  type t
85
  module Signature:Signature_sig  with type term=Lambda.term
86
  type signature = Signature.t
87
  type resume
88 89 90 91
  type dependency =
    | Signatures of (signature*signature)
    | Lexicons of (t*t)

92 93 94 95
  type data =
    | Signature of signature
    | Lexicon of t

96
  val get_dependencies : t -> dependency
97
  val empty : (string*Abstract_syntax.location) -> ?non_linear:bool -> abs:signature -> obj:signature -> t
98 99 100
  val name : t -> (string*Abstract_syntax.location)
  val insert : Abstract_syntax.lex_entry -> t -> t
  val to_string : t -> string
101 102
  val interpret_type : Signature.stype -> t -> Signature.stype
(*  val interpret_type : Lambda.stype -> t -> Lambda.stype *)
103
  val interpret_term : Lambda.term -> t -> Lambda.term
104 105
  val interpret : Signature.term -> Signature.stype -> t -> (Signature.term*Signature.stype)
  val get_sig : t -> (signature*signature)
106
  val check : t -> unit
107 108
  val parse : Signature.term -> Signature.stype -> t -> resume
  val get_analysis : resume -> t -> Lambda.term option * resume
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
109
  val compose: t -> t -> (string*Abstract_syntax.location) -> t
110
  val program_to_buffer : t -> Buffer.t
111
  val program_to_log : Logs.src -> Logs.level -> t -> unit
112
  val query_to_buffer : Signature.term -> Signature.stype -> t -> Buffer.t
113
  val query_to_log : Logs.src -> Logs.level -> Signature.term -> Signature.stype -> t -> unit
114
  val update : t -> (string -> data) -> t
115
end