signature.ml 12.2 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 Table
21 22 23 24 25 26 27 28
open Lambda
open Abstract_syntax

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
29
      
30 31


32
module Make(Symbols:TABLE with type key=String.t)(Id:TABLE with type key=int) =
33 34 35 36 37 38
struct


  exception Duplicate_type_definition
  exception Duplicate_term_definition

39 40 41 42
  exception Not_found

  exception Not_functional_type

POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
43 44
  exception Not_yet_implemented

45 46 47 48 49 50
  type entry = sig_entry

  type t = {name:string*Abstract_syntax.location;
	    size:int;
	    terms:entry Symbols.t;
	    types:entry Symbols.t;
51 52
	    ids:entry Id.t;
	    is_2nd_order:bool}
53 54 55 56

  type term = Lambda.term

  type stype = Lambda.stype
57 58 59 60 61 62 63 64 65 66 67 68
      
  let find_term sym {terms=syms} =
    try
      match Symbols.find sym syms with
	| Term_declaration (x,id,_,const_type) as t when sym=x-> Lambda.Const id,const_type
	| Term_declaration _ -> failwith "Bug in find_term"
	| Term_definition (x,id,_,const_type,_) as t when sym=x-> Lambda.DConst id,const_type
	| Term_definition _ -> failwith "Bug in find_term"
	| _ -> raise Not_found
    with
      | Symbols.Not_found -> raise Not_found

69 70 71 72 73 74 75 76 77

  let id_to_string {ids=ids} i =
    match Id.find i ids with
      | Type_declaration(s,_,_) -> Abstract_syntax.Default,s
      | Type_definition(s,_,_,_) -> Abstract_syntax.Default,s
      | Term_declaration(s,_,behavior,_) -> behavior,s
      | Term_definition(s,_,behavior,_,_) -> behavior,s


POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
78 79 80 81 82 83 84 85
  let type_to_string ty sg = Lambda.type_to_string ty (id_to_string sg)
    
  let term_to_string t sg = 
    Lambda.term_to_string
      t
      (id_to_string sg)


86
  let empty n = {name=n;size=0;terms=Symbols.empty;types=Symbols.empty;ids=Id.empty;is_2nd_order=true}
87 88 89 90 91 92 93

  let name {name=n} = n

  let find_atomic_type s ({types=syms} as sg) = 
    try
      match Symbols.find s syms with
	| Type_declaration (x,id,_) when x=s -> Lambda.Atom id
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
94
	| Type_declaration _ -> failwith "Bug in find_atomic_type"
95
	| Type_definition (x,id,_,_) when x=s -> Lambda.DAtom id
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
96 97 98
	| Type_definition _ -> failwith "Bug in find_atomic_type"
	| Term_declaration _ -> failwith "Bug in find_atomic_type"
	| Term_definition _ -> failwith "Bug in find_atomic_type"
99
    with
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
100
      | Not_found -> failwith "Bug in find_atomic_type"
101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139


  let rec convert_type ty ({types=syms} as sg) = 
    match ty with
      | Abstract_syntax.Type_atom (s,l,args) -> find_atomic_type s sg
      | Abstract_syntax.Linear_arrow (ty1,ty2,l) -> Lambda.LFun (convert_type ty1 sg,convert_type ty2 sg)
      | Abstract_syntax.Arrow (ty1,ty2,l) -> Lambda.Fun (convert_type ty1 sg,convert_type ty2 sg)

  let abstract_on_dependent_types lst sg=
    List.fold_right
      (fun x acc -> Lambda.Depend(convert_type x sg,acc))
      lst
      Lambda.Type

  let add_sig_type t e ({size=s;types=syms;ids=ids} as sg) =
    try
      (* First perform addition on the functional data structure *)
      let new_symbols = Symbols.add t e syms in
      {sg with size=s+1;types=new_symbols;ids=Id.add s e ids}
    with
      | Symbols.Conflict -> raise Duplicate_type_definition
      | Id.Conflict  -> raise Duplicate_type_definition

  let add_sig_term t e ({size=s;terms=syms;ids=ids} as sg) =
    try
      (* First perform addition on the functional data structure *)
      let new_symbols = Symbols.add t e syms in
      {sg with size=s+1;terms= new_symbols;ids=Id.add s e ids}
    with
      | Symbols.Conflict -> raise Duplicate_term_definition
      | Id.Conflict  -> raise Duplicate_term_definition


  let rec expand_type ty ({ids=ids} as sg) = 
    match ty with
      | Lambda.Atom _ -> ty
      | Lambda.DAtom i ->
	  (match Id.find i ids with
	     | Type_definition (_,_,_,ty1) -> expand_type ty1 sg
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
140
	     | _ -> failwith "Bug in expand type")
141 142 143 144 145 146 147 148 149 150 151
      | Lambda.LFun (ty1,ty2) -> Lambda.LFun(expand_type ty1 sg,expand_type ty2 sg)
      | Lambda.Fun (ty1,ty2) -> Lambda.Fun(expand_type ty1 sg,expand_type ty2 sg)
      | _ -> failwith "Not yet implemented"


  let rec expand_term t ({ids=ids} as sg) = 
    match t with
      | (Lambda.Var _| Lambda.LVar _ | Lambda.Const _) -> t
      | Lambda.DConst i ->
	  (match Id.find i ids with
	     | Term_definition (_,_,_,_,u) -> expand_term u sg
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
152
	     | _ -> failwith "Bug in expand term")
153 154 155 156 157
      | Lambda.Abs (x,u) -> Lambda.Abs (x,expand_term u sg)
      | Lambda.LAbs (x,u) -> Lambda.LAbs (x,expand_term u sg)
      | Lambda.App (u,v) -> Lambda.App (expand_term u sg,expand_term v sg)
      | _ -> failwith "Not yet implemented"

158 159 160 161 162 163
  let unfold_type_definition i ({ids=ids} as sg) = 
    match Id.find i ids with
      | Type_definition (_,_,_,ty1) -> expand_type ty1 sg
      | _ -> failwith "Bug in unfold_type_definition"


164 165 166
  let unfold_term_definition i ({ids=ids} as sg) = 
    match Id.find i ids with
      | Term_definition (_,_,_,_,t) -> expand_term t sg
167
      | _ -> failwith "Bug in unfold_term_definition" 
168 169 170
	  
	  

POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
171 172 173 174 175 176 177 178 179
  let get_type_of_const_id i ({ids=ids} as sg) =
    try
      match Id.find i ids with
	| Term_declaration (_,_,_,ty) -> expand_type ty sg
	| Term_definition (_,_,_,ty,_) -> expand_type ty sg
	| _ -> failwith "Should be applied only on constants"
    with
      | Id.Not_found -> failwith "Bug in get_type_of_const_id"

180 181 182 183 184 185 186
  let rec decompose_functional_type ty ({ids=ids} as sg) =
    match ty with
      | Lambda.LFun (ty1,ty2) -> ty1,ty2,Abstract_syntax.Linear
      | Lambda.Fun (ty1,ty2) -> ty1,ty2,Abstract_syntax.Non_linear
      | Lambda.DAtom i ->
	  (match Id.find i ids with
	     | Type_definition (_,_,_,ty1) -> decompose_functional_type ty1 sg
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
187
	     | _ -> failwith "Bug in decompose_functional_type")
188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207
      | _ -> raise Not_functional_type


  let rec get_binder_argument_functional_type x ({terms=terms} as sg) =
    let ty = 
      match Symbols.find x terms with
	| Term_declaration (_,_,_,ty) -> ty
	| Term_definition (_,_,_,ty,_) -> ty
	| _ -> failwith (Printf.sprintf "Bug: Request of the type of the non constant \"%s\"" x) in
      try
	let ty1,ty2,_ = decompose_functional_type ty sg in
	let _,_,lin = decompose_functional_type ty1 sg in
	  Some lin
      with
	| Not_functional_type -> None


	  
	  
	    
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
208 209
  (* We assume here that [term] is well typed and in beta-normal form
     and that types and terms definitions have been unfolded*)
210
	    
211
  let eta_long_form term stype sg =
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
212 213
    Lambda.eta_long_form (Lambda.normalize (expand_term term sg)) (expand_type stype sg) (fun id -> get_type_of_const_id id sg)
			   
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
214 215 216

  let unfold t sg = Lambda.normalize (expand_term t sg)
 
217 218 219 220 221 222 223 224 225 226 227 228
  type temp_t=t
  type temp_entry=entry

  module Type_System=Type_system.Type_System.Make(
    struct
      exception Not_found
      type t=temp_t
      type entry=temp_entry
      type stype=Lambda.stype
      let expand_type = expand_type
      let find_term = find_term
      let type_to_string = type_to_string
229
      let term_to_string = term_to_string
230 231 232 233
    end)

  let typecheck=Type_System.typecheck
	  
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
234
			   
235 236 237 238 239 240 241 242
  let add_entry e ({size=s} as sg) =
    match e with
      | Abstract_syntax.Type_decl (t,_,Abstract_syntax.K k) -> 
	  add_sig_type t (Type_declaration (t,s,abstract_on_dependent_types k sg)) sg
      | Abstract_syntax.Type_def (t,_,ty,Abstract_syntax.K k) ->
	  add_sig_type t (Type_definition (t,s,abstract_on_dependent_types k sg,convert_type ty sg)) sg
      | Abstract_syntax.Term_decl (t,behavior,_,ty) ->
	  let t_type = convert_type ty sg in
243 244
	  let sg_is_2nd_order = sg.is_2nd_order && (Lambda.is_2nd_order t_type (fun i -> unfold_type_definition i sg)) in
	  add_sig_term t (Term_declaration (t,s,behavior,convert_type ty sg)) {sg with is_2nd_order=sg_is_2nd_order}
245 246 247 248
      | Abstract_syntax.Term_def (t,behavior,_,term,ty) ->
	  let t_type = convert_type ty sg in
	  let t_term = typecheck term t_type sg in
	    add_sig_term t (Term_definition (t,s,behavior,t_type,t_term)) sg
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
249
				     
250 251 252 253 254 255 256 257
  let is_type s {types=syms} =
    try
      match Symbols.find s syms with
	| Type_declaration _ -> true
	| Type_definition _ -> true
	| _ -> false
    with
      | Symbols.Not_found -> false
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
258
				 
259 260 261 262 263 264 265 266
  let is_constant s {terms=syms} =
    try
      match Symbols.find s syms with
	| Term_declaration (_,_,behavior,_) -> true,Some behavior
	| Term_definition (_,_,behavior,_,_) -> true,Some behavior
	| _ -> false,None
    with
      | Symbols.Not_found -> false,None
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
267
				 
268
  let add_warnings _ sg = sg
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
269
			   
270
  let get_warnings _  = []
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
271 272
    
      
273
  let raw_to_string t = Lambda.raw_to_string t
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
274
    
275 276 277 278 279
  let behavior_to_string = function
    | Abstract_syntax.Default -> ""
    | Abstract_syntax.Prefix -> "prefix "
    | Abstract_syntax.Infix -> "infix "
    | Abstract_syntax.Binder -> "binder "
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
280
	
281 282 283 284 285
  let entry_to_string f = function
    | Type_declaration(s,_,k) -> Printf.sprintf "\t%s : %s;" s (Lambda.kind_to_string k f)
    | Type_definition(s,_,k,ty) -> Printf.sprintf "\t%s = %s : %s;" s (Lambda.type_to_string ty f) (Lambda.kind_to_string k f)
    | Term_declaration(s,_,behavior,ty) -> Printf.sprintf "\t%s%s : %s;" (behavior_to_string behavior) s (Lambda.type_to_string ty f)
    | Term_definition(s,_,behavior,ty,t) -> Printf.sprintf "\t%s%s = %s : %s;" (behavior_to_string behavior) s (Lambda.term_to_string t f) (Lambda.type_to_string ty f)
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
286
	
287 288 289 290
  let to_string ({name=n;ids=ids} as sg) =
    Printf.sprintf "signature %s = \n%send\n"
      (fst n)
      (fst (Id.fold 
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
291 292 293 294 295 296
	      (fun _ e (acc,b) ->
		 match b with
		   | true -> Printf.sprintf "%s%s\n" acc (entry_to_string (id_to_string sg) e),true
		   | false -> Printf.sprintf "%s\n" (entry_to_string (id_to_string sg) e),true)
	      ("",false)
	      ids))
297 298 299

  let convert_term t ty sg =
    let t_type = convert_type ty sg in
300 301
    let t=typecheck t t_type sg in
      t,t_type
302 303 304 305

  let type_of_constant x ({terms=syms} as sg) =
    try
      match Symbols.find x syms with
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
306 307 308
	| Term_declaration (s,_,_,ty) when x = s -> ty
	| Term_definition (s,_,_,ty,_) when x = s -> ty
	| _ -> failwith "Bug in type_of_constant"
309
    with
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
310
      | Symbols.Not_found -> failwith "Bug in type_of_constant"
311 312 313 314 315 316 317 318 319 320 321 322 323

  let fold f a {ids=ids} =
    Id.fold
      (fun _ att acc -> f att acc)
      a
      ids

  let is_declared e _ =
    match e with
      | Type_declaration (s,_,_) -> Some s
      | Term_declaration (s,_,_,_) -> Some s
      | _ -> None

324
  let is_2nd_order {is_2nd_order} = is_2nd_order
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
325

326 327 328
end	  
  
module Table = Table.Make_table(struct let b = 10 end)
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
329 330 331 332 333 334 335 336 337
  (*module Table =
    struct
    module IntMap = Map.Make(struct type t=int let compare i j = i-j end)
    type 'a t = 'a IntMap.t
    type key = int

    exception Conflict
    let empty = IntMap.empty
    let add ?(override=false) k v t = 
338
    try 
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
339 340
    let _ = IntMap.find k t in
    if override then IntMap.add k v t else raise Conflict
341
    with
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
342
    | Not_found -> IntMap.add k v t
343 344


POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
345
    exception Not_found
346

POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
347
    let find k t = 
348
    try
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
349
    IntMap.find k t
350
    with
POGODALLA Sylvain's avatar
POGODALLA Sylvain committed
351 352 353 354
    | Not_found -> raise Not_found
    let fold f acc t = IntMap.fold f t acc
    end
  *)
355 356 357 358

module Sylvains_signature = Make(Tries.Tries)(Table)