interface.ml 4.85 KB
Newer Older
1 2 3 4 5 6
(**************************************************************************)
(*                                                                        *)
(*                 ACG development toolkit                                *)
(*                                                                        *)
(*                  Copyright 2008 INRIA                                  *)
(*                                                                        *)
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
open Abstract_syntax
21
open 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 type_to_string : stype -> t -> string
  val term_to_string : term -> t -> string
49
  val id_to_string : t -> int -> Abstract_syntax.syntactic_behavior*string
50 51
  val type_to_formatted_string : Format.formatter -> stype -> t -> unit
  val term_to_formatted_string : Format.formatter -> term -> t -> unit
52 53 54
(*  val type_to_string : stype -> t -> string*)
  val unfold_type_definition : int -> t -> Lambda.stype 
  val unfold_term_definition : int -> t -> Lambda.term 
55 56 57
  val expand_type : Lambda.stype -> t -> Lambda.stype
  val expand_term : Lambda.term -> t -> Lambda.term

58 59 60
  val add_warnings : Error.warning list -> t -> t
  val get_warnings : t -> Error.warning list
  val to_string : t -> string
61
(*  val term_to_string : term -> t -> string *)
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
62
(*  val raw_to_string : term -> string*)
63 64 65 66 67
  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
68 69
  (* REVIEW: Commented out because of still missing impl. *)
  (*  val extract : entry -> t -> data *)
70
  val get_binder_argument_functional_type : string -> t -> Abstract_syntax.abstraction option
71
  val is_declared : entry -> t -> string option
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
72
  val eta_long_form : term -> stype -> t -> term
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
73
  val unfold : term -> t -> term
74 75
  val is_2nd_order : t -> bool

76 77 78 79 80 81 82 83
end

module type Lexicon_sig =
sig
  exception Duplicate_type_interpretation
  exception Duplicate_constant_interpretation

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

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

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