merge branches/sylvain-2011_05 from r311 to r319 into trunk

src/Makefile.in

@@ -19,7 +19,8 @@
 
 .PHONY: byte opt clean superclean
 
-SUBDIRS= utils logic grammars acg-data scripting lambda datalog
+#SUBDIRS= utils logic grammars acg-data scripting lambda datalog
+SUBDIRS= utils logic grammars acg-data scripting datalog
 
 byte:
 	$(foreach dir,$(SUBDIRS),$(MAKE) -r -S -C $(dir) byte;)

src/acg-data/Makefile.in

@@ -38,7 +38,7 @@ PREVIOUS_DIRS = ../utils ../logic ../grammars
 
 # Source files in the right order of dependance
 
-ML = signature.ml acg_lexicon.ml
+ML = type_system.ml signature.ml acg_lexicon.ml
 
 EXE_SOURCES = acgc.ml
 

src/acg-data/acg_lexicon.ml

@@ -19,7 +19,7 @@
 
 open Abstract_syntax
 open Lambda
-open Signature
+open Signature 
 
 module Make (Sg:Interface.Signature_sig with type  term = Lambda.term and type stype = Lambda.stype) =
 struct
@@ -40,10 +40,10 @@ struct
 
 
   let interpretation_to_string abstract_type_or_cst_id fun_type_from_id i sg = match i with
-    | Type (_,t) -> Printf.sprintf "\t%s" (Lambda.type_to_string t (Sg.id_to_string sg))
+    | Type (_,t) -> Printf.sprintf "\t%s" (Signature.type_to_string t sg)
     | Constant (_,c) -> 
 	let eta_long = Sg.eta_long_form c (fun_type_from_id abstract_type_or_cst_id) sg  in
-	  Printf.sprintf "\t%s [eta-long form: %s {%s}]" (Lambda.term_to_string c (Sg.id_to_string sg)) (Lambda.term_to_string eta_long (Sg.id_to_string sg) ) (Lambda.raw_to_string eta_long)
+	  Printf.sprintf "\t%s [eta-long form: %s {%s}]" (Sg.term_to_string c sg) (Sg.term_to_string eta_long sg ) (Lambda.raw_to_string eta_long)
 
   type t = {name:string*Abstract_syntax.location;
 	    dico:interpretation Dico.t;
@@ -65,7 +65,7 @@ struct
   let rec interpret_type abs_ty ({abstract_sig=abs_sg;dico=dico} as lex) =
     match abs_ty with
       | Lambda.Atom i -> 
-	  (let _,abs_ty_as_str = Sg.id_to_string abs_sg i in
+	  (let abs_ty_as_str = Sg.type_to_string abs_ty abs_sg in
 	     try
 	       match Dico.find abs_ty_as_str dico with
 		 | Type (_,obj_ty) -> obj_ty
@@ -81,7 +81,7 @@ struct
     match abs_t with
       | (Lambda.Var i| Lambda.LVar i) -> abs_t
       | Lambda.Const i -> 
-	  (let _,abs_term_as_str = Sg.id_to_string abs_sg i in
+	  (let abs_term_as_str = Sg.term_to_string abs_t abs_sg in
 	     try
 	       match Dico.find abs_term_as_str dico with
 		 | Constant (_,obj_t) -> obj_t

src/acg-data/signature.mli

@@ -20,16 +20,15 @@
 open Abstract_syntax
 open Lambda
 
-
 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 Sylvains_signature  : Interface.Signature_sig 
   with
     type term = Lambda.term
   and type stype = Lambda.stype 
-  and type entry = sig_entry
+(*  and type entry = Interfacesig_entry *)

src/grammars/syntactic_data_structures.mli → src/acg-data/type_system.mli

@@ -18,9 +18,25 @@
 (**************************************************************************)
 
 open Abstract_syntax
+open Lambda
 
-(** This modules implements the abstract syntax and the build function for the signatures *)
+module type SIG_ACCESS =
+sig
+  exception Not_found
+  type t
 
-module Abstract_sig : Interface.Signature_sig with type entry = Abstract_syntax.sig_entry
+  val expand_type :  Lambda.stype -> t -> Lambda.stype 
+  val find_term : string -> t -> Lambda.term *Lambda.stype
+  val type_to_string : Lambda.stype -> t -> string
+(*  val id_to_string : t -> int -> Abstract_syntax.syntactic_behavior*string*)
+end
 
-module Abstract_lex : Interface.Lexicon_sig with type Signature.t = Abstract_sig.t
+module Type_System :
+sig
+  module Make(Signature:SIG_ACCESS) : 
+  sig
+    val typecheck : Abstract_syntax.term -> Lambda.stype -> Signature.t -> Lambda.term
+  end
+end
+
+      

src/acg-data/typing.ml

-(**************************************************************************)
-(*                                                                        *)
-(*                 ACG development toolkit                                *)
-(*                                                                        *)
-(*                  Copyright 2008 INRIA                                  *)
-(*                                                                        *)
-(*  More information on "http://acg.gforge.loria.fr/"                     *)
-(*  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           *)
-(*                                                                        *)
-(**************************************************************************)
-

src/data/tag.acg

@@ -42,7 +42,7 @@ signature derived_trees =
 	N2,S2,VP2:tree -> tree -> tree;
 	every,dog,chases,a,cat,sleeps,slowly,new,big,black,seems,john,mary,bill,paul,
 	claims,loves,to_love,who,said,liked,does,think:tree;
-	n = lambda  . lambda d a.d (a(N1 n)) : tree -> (tree -> tree) -> (tree -> tree) -> tree;
+	n = lambda n. lambda d a.d (a(N1 n)) : tree -> (tree -> tree) -> (tree -> tree) -> tree;
 	iv = lambda v . lambda s a np0 .s (S2 np0 (a (VP1 v))) : tree -> (tree -> tree)  -> (tree -> tree) -> tree -> tree ;
 	tv = lambda v . lambda s a np0 np1 .s (S2 np0 (a (VP2 v np1))) : tree -> (tree -> tree) -> (tree -> tree) -> tree -> tree -> tree ;
 	ph_arg_v = lambda v . lambda s_root a np0 s_foot .s_root (S2 np0 (a (VP2 v s_foot))) : tree -> (tree -> tree) -> (tree -> tree) -> tree -> tree -> tree ;

src/grammars/Makefile.in

@@ -37,8 +37,8 @@ LIBDIR += @DYPGEN_INCLUDE@
 PREVIOUS_DIRS = ../utils ../logic
 
 # Source files in the right order of dependance
-#ML = error.ml abstract_syntax.ml interface.ml environment.ml entry.ml data_parser.ml data_lexer.ml data_parsing.ml
-ML = error.ml interface.ml environment.ml entry.ml syntactic_data_structures.ml acg_token.ml data_lexer.ml data_parser.ml  interactive.ml 
+#ML = error.ml interface.ml environment.ml entry.ml syntactic_data_structures.ml acg_token.ml data_lexer.ml data_parser.ml  interactive.ml 
+ML = error.ml interface.ml environment.ml entry.ml acg_token.ml data_lexer.ml data_parser.ml  interactive.ml 
 
 EXE_SOURCES =  
 
@@ -68,17 +68,17 @@ include ../Makefile.common
 # data_lexer.ml : data_lexer.mll
 # 	@OCAMLLEX@ $<
 
-data_parser.ml: ../utils/utils.cmi acg_token.cmi syntactic_data_structures.cmi \
+data_parser.ml: ../utils/utils.cmi acg_token.cmi \
     data_lexer.cmi error.cmi environment.cmi entry.cmi \
     ../logic/abstract_syntax.cmi
 
-data_parser.cmo: ../utils/utils.cmi acg_token.cmi syntactic_data_structures.cmi \
+data_parser.cmo: ../utils/utils.cmi acg_token.cmi \
      data_lexer.cmo error.cmi environment.cmi entry.cmi \
      ../logic/abstract_syntax.cmi data_parser.cmi
-data_parser.cmx: ../utils/utils.cmx acg_token.cmx syntactic_data_structures.cmx \
+data_parser.cmx: ../utils/utils.cmx acg_token.cmx \
      data_lexer.cmx error.cmx environment.cmx entry.cmx \
      ../logic/abstract_syntax.cmx data_parser.cmi
-data_parser.ml: ../utils/utils.cmi acg_token.cmi syntactic_data_structures.cmi \
+data_parser.ml: ../utils/utils.cmi acg_token.cmi \
 
 
 example_dispatch.ml : example.aut

src/grammars/data_parser.dyp

@@ -20,7 +20,7 @@
  %mltop {
 
   open Abstract_syntax
-  open Syntactic_data_structures
+(*  open Syntactic_data_structures*)
   open Dyp
 
   module Env = Utils.StringSet

src/grammars/environment.ml

@@ -20,74 +20,6 @@
 open Interface
 open Abstract_syntax
 
-(*module type Signature_sig =
-sig
-  (** Exceptions raised when definitions of types or constants are
-      duplicated *)
-  
-  exception Duplicate_type_definition
-  exception Duplicate_term_definition
-
-  (** The type of the signature as abstract object *)
-  type t
-
-  (** The (ocaml) type for the terms of the signature *)
-  type term
-
-  (** The (ocaml) type for the types of the signature *)
-  type stype
-
-    
-  (** [empty name] returns the empty signature of name [name] *)
-  val empty : (string*Abstract_syntax.location) -> t
-    
-  (** [name s] returns the name of the signature [s] and the location of its definition *)
-  val name : t -> (string*Abstract_syntax.location)
-    
-  (** [add_entry e s] returns a signature where the entry [e] has been
-      added *)
-  val add_entry : Abstract_syntax.sig_entry -> t -> t
-    
-  (** [is_atomic_ype id s ] returns [true] if [id] is the name of an
-      atomic type in [s] and [false] oterwise *)
-  val is_type : string -> t -> bool
-    
-  (** [is_constant id s ] returns [(true,Some b)] together with its
-      syntactic behaviour [b] if [id] is the name of a constant in [s]
-      and [false,None] oterwise *)
-  val is_constant : string -> t -> bool * Abstract_syntax.syntactic_behavior option
-
-  (** [add_warnings w s ] resturns a signature where the warning [w] have been added *)
-  val add_warnings : Error.warning list -> t -> t
-
-  (** [get_warnings sg] returns the warnigs emitted while parsing [sg]. *)
-  val get_warnings : t -> Error.warning list
-
-  (** [to_string sg] returns a string describing the signature
-      [sg]. Should be parsable *)
-  val to_string : t -> string
-
-  (** [term_to_string t sg] returns a string describing the term [t]
-      wrt the signature [sg]. *)
-  val term_to_string : term -> t -> string
-
-  (** [type_to_string t sg] returns a string describing the term [t]
-      wrt the signature [sg]. *)
-  val type_to_string : stype -> t -> string
-    
-  (** [convert_term t ty sg] returns a the term corresponding to the
-      parsed term [t] with parsed type [ty] wrt to the signature [sg]
-  *)
-  val convert_term : Abstract_syntax.term -> Abstract_syntax.type_def -> t -> term * stype
-
-  (** [convert_type ty sg] returns a type to the parsed type [ty] wrt
-      to the signature [sg] *)
-  val convert_type : Abstract_syntax.type_def -> t -> stype
-  val get_binder_argument_functional_type : string -> t -> Abstract_syntax.abstraction option
-
-
-end
-  *)
 
 
 module type Environment_sig =

src/grammars/environment.mli

@@ -21,78 +21,6 @@ open Interface
 
 open Abstract_syntax
 
-(* A simple interface for environmnent *)
-(*module type Signature_sig =
-sig
-  (** Exceptions raised when definitions of types or constants are
-      duplicated *)
-  
-  exception Duplicate_type_definition
-  exception Duplicate_term_definition
-
-  (** The type of the signature as abstract object *)
-  type t
-
-  (** The (ocaml) type for the terms of the signature *)
-  type term
-
-  (** The (ocaml) type for the types of the signature *)
-  type stype
-
-    
-  (** [empty name] returns the empty signature of name [name] *)
-  val empty : (string*Abstract_syntax.location) -> t
-    
-  (** [name s] returns the name of the signature [s] and the location of its definition *)
-  val name : t -> (string*Abstract_syntax.location)
-    
-  (** [add_entry e s] returns a signature where the entry [e] has been
-      added *)
-  val add_entry : Abstract_syntax.sig_entry -> t -> t
-    
-  (** [is_atomic_ype id s ] returns [true] if [id] is the name of an
-      atomic type in [s] and [false] oterwise *)
-  val is_type : string -> t -> bool
-    
-  (** [is_constant id s ] returns [(true,Some b)] together with its
-      syntactic behaviour [b] if [id] is the name of a constant in [s]
-      and [false,None] oterwise *)
-  val is_constant : string -> t -> bool * Abstract_syntax.syntactic_behavior option
-
-  (** [add_warnings w s ] resturns a signature where the warning [w] have been added *)
-  val add_warnings : Error.warning list -> t -> t
-
-  (** [get_warnings sg] returns the warnigs emitted while parsing [sg]. *)
-  val get_warnings : t -> Error.warning list
-
-  (** [to_string sg] returns a string describing the signature
-      [sg]. Should be parsable *)
-  val to_string : t -> string
-
-  (** [term_to_string t sg] returns a string describing the term [t]
-      wrt the signature [sg]. *)
-  val term_to_string : term -> t -> string
-
-  (** [type_to_string t sg] returns a string describing the term [t]
-      wrt the signature [sg]. *)
-  val type_to_string : stype -> t -> string
-    
-  (** [convert_term t ty sg] returns a the term corresponding to the
-      parsed term [t] with parsed type [ty] wrt to the signature [sg]
-  *)
-  val convert_term : Abstract_syntax.term -> Abstract_syntax.type_def -> t -> term * stype
-
-  (** [convert_type ty sg] returns a type to the parsed type [ty] wrt
-      to the signature [sg] *)
-  val convert_type : Abstract_syntax.type_def -> t -> stype
-  val get_binder_argument_functional_type : string -> t -> Abstract_syntax.abstraction option
-
-
-end
-*)
-
-
-  
 (** This modules implements a functor that build an environment
     containing signatures and lexicons when provided with to actual
     implementations of a signature and a lexicon *)

src/grammars/interface.ml

@@ -20,29 +20,34 @@
 open Abstract_syntax
 open Lambda
 
+
 module type Signature_sig =
 sig
   exception Duplicate_type_definition
   exception Duplicate_term_definition
+  exception Not_found
 
   type t
   type entry
+
   type term
   type stype
   val empty : (string*Abstract_syntax.location) -> t
   val name : t -> (string*Abstract_syntax.location)
   val add_entry : Abstract_syntax.sig_entry -> t -> t
+  val find_term : string -> t -> term * stype
   val is_type : string -> t -> bool
   val is_constant : string -> t -> bool*Abstract_syntax.syntactic_behavior option
-  val id_to_string : t -> int -> Abstract_syntax.syntactic_behavior*string
-  val unfold_type_definition : int -> t -> Lambda.stype
-  val unfold_term_definition : int -> t -> Lambda.term
+  val type_to_string : stype -> t -> string
+  val term_to_string : term -> t -> string
+(*  val type_to_string : stype -> t -> string*)
+  val unfold_type_definition : int -> t -> Lambda.stype 
+  val unfold_term_definition : int -> t -> Lambda.term 
   val add_warnings : Error.warning list -> t -> t
   val get_warnings : t -> Error.warning list
   val to_string : t -> string
-  val term_to_string : term -> t -> string
+(*  val term_to_string : term -> t -> string *)
 (*  val raw_to_string : term -> string*)
-  val type_to_string : stype -> t -> string
   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

src/grammars/interface.mli

@@ -21,6 +21,7 @@ open Abstract_syntax
 open Lambda
 
 (** This module signature describes the interface for modules implementing signatures *)
+
 module type Signature_sig =
 sig
   (** Exceptions raised when definitions of types or constants are
@@ -29,6 +30,12 @@ sig
   exception Duplicate_type_definition
   exception Duplicate_term_definition
 
+  (** Exception raised when no entry associated to a given symbol
+      exists in a signature *)
+
+  exception Not_found
+
+
   (** The type of the signature as abstract object *)
   type t
 
@@ -51,6 +58,12 @@ sig
   (** [add_entry e s] returns a signature where the entry [e] has been
       added *)
   val add_entry : Abstract_syntax.sig_entry -> t -> t
+
+  (** [find_term id s] returns the term together with its type, as
+      declared or defined in the signature [s], corresponding to the
+      symbol [id] in [s] if it exists. Raise [Not_found] otherwise*)
+  val find_term : string -> t -> term * stype
+
     
   (** [is_atomic_ype id s ] returns [true] if [id] is the name of an
       atomic type in [s] and [false] oterwise *)
@@ -61,24 +74,27 @@ sig
       and [false,None] oterwise *)
   val is_constant : string -> t -> bool * Abstract_syntax.syntactic_behavior option
 
-  (** [id_to_string id sg] returns the a syntactic behaviour together
-      with a string describing the term or the type of [sg] whose
-      identifier in (as [i] in [Lambda.Atom i] of type
-      {!Lambda.Lambda.stype}) is [id]. If [id] corresponds to a type,
-      the syntactic behaviour is meaningless and should not be relied on *)
-  val id_to_string : t -> int -> Abstract_syntax.syntactic_behavior*string
+  (** [type_to_string ty sg] returns the string corresponding to a
+      type [ty] of type {!Lambda.Lambda.stype}) with respect to the
+      signature [sg] *)
+    val type_to_string : stype -> t -> string 
+
+  (** [term_to_string t sg] returns the string corresponding to a
+      term [t] of type {!Lambda.Lambda.term}) with respect to the
+      signature [sg] *)
+    val term_to_string : term -> t -> string 
 
   (** [unfold_type_definition id t] returns the actual type for the
       type defined by [Lambda.DAtom id]. Fails with "Bug" if [id] does
       not correspond to a type definition *)
 
-  val unfold_type_definition : int -> t -> Lambda.stype
+  val unfold_type_definition : int -> t -> Lambda.stype 
 
   (** [unfold_term_definition id t] returns the actual term for the
       term defined by [Lambda.DConst id]. Fails with "Bug" if [id]
       does not correspond to a term definition *)
 
-  val unfold_term_definition : int -> t -> Lambda.term
+  val unfold_term_definition : int -> t -> Lambda.term 
     
   (** [add_warnings w s ] resturns a signature where the warning [w] have been added *)
   val add_warnings : Error.warning list -> t -> t
@@ -92,12 +108,12 @@ sig
 
   (** [term_to_string t sg] returns a string describing the term [t]
       wrt the signature [sg]. *)
-  val term_to_string : term -> t -> string
+(*  val term_to_string : term -> t -> string *)
 (*  val raw_to_string : term -> string*)
 
   (** [type_to_string t sg] returns a string describing the term [t]
       wrt the signature [sg]. *)
-  val type_to_string : stype -> t -> string
+(*  val type_to_string : stype -> t -> string *)
     
   (** [convert_term t ty sg] returns a the term corresponding to the
       parsed term [t] with parsed type [ty] wrt to the signature [sg]