From c8a04147a79c98218508e5500ce52c48aa9a216c Mon Sep 17 00:00:00 2001 From: Sylvain Pogodalla Date: Thu, 2 Jul 2009 15:28:40 +0000 Subject: [PATCH] eta expansion added --- src/acg-data/acg_lexicon.ml | 12 +- src/acg-data/signature.ml | 158 ++++++++++++---------- src/grammars/interface.ml | 1 + src/grammars/interface.mli | 4 + src/grammars/syntactic_data_structures.ml | 2 + src/logic/lambda.ml | 86 +++++++++++- src/logic/lambda.mli | 9 ++ 7 files changed, 195 insertions(+), 77 deletions(-) diff --git a/src/acg-data/acg_lexicon.ml b/src/acg-data/acg_lexicon.ml index a792bfe..5805cc7 100644 --- a/src/acg-data/acg_lexicon.ml +++ b/src/acg-data/acg_lexicon.ml @@ -39,9 +39,11 @@ struct | Constant of (Abstract_syntax.location * Lambda.term ) - let interpretation_to_string i sg = match i with + 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)) - | Constant (_,c) -> Printf.sprintf "\t%s" (Lambda.term_to_string c (Sg.id_to_string 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) type t = {name:string*Abstract_syntax.location; dico:interpretation Dico.t; @@ -103,7 +105,7 @@ struct | Abstract_syntax.Type (id,loc,ty) -> {lex with dico=Dico.add id (Type (loc,Sg.convert_type ty lex.object_sig)) d} | Abstract_syntax.Constant (id,loc,t) -> {lex with dico=Dico.add id (Constant (loc,Sg.typecheck t (interpret_type (Sg.type_of_constant id lex.abstract_sig) lex) lex.object_sig)) d} - let to_string {name=n,_;dico=d;abstract_sig=abs_sg;object_sig=obj_sg} = + let to_string ({name=n,_;dico=d;abstract_sig=abs_sg;object_sig=obj_sg} as lex) = Printf.sprintf "lexicon %s(%s): %s =\n%send" n @@ -112,8 +114,8 @@ struct (match Dico.fold (fun k i -> function - | None -> Some (Printf.sprintf "\t%s := %s;" k (interpretation_to_string i obj_sg)) - | Some a -> Some (Printf.sprintf "%s\n\t%s := %s;" a k (interpretation_to_string i obj_sg))) + | None -> Some (Printf.sprintf "\t%s := %s;" k (interpretation_to_string k (fun id -> interpret_type (Sg.type_of_constant id abs_sg) lex) i obj_sg)) + | Some a -> Some (Printf.sprintf "%s\n\t%s := %s;" a k (interpretation_to_string k (fun id -> interpret_type (Sg.type_of_constant id abs_sg) lex) i obj_sg))) d None with | None -> "" diff --git a/src/acg-data/signature.ml b/src/acg-data/signature.ml index f63aff8..f752d7b 100644 --- a/src/acg-data/signature.ml +++ b/src/acg-data/signature.ml @@ -62,6 +62,8 @@ struct exception Duplicate_type_definition exception Duplicate_term_definition + exception Not_yet_implemented + type entry = sig_entry type t = {name:string*Abstract_syntax.location; @@ -82,6 +84,21 @@ struct | Term_definition(s,_,behavior,_,_) -> behavior,s + 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) + (* (fun i -> match Id.find i ids with | + Term_declaration(s,_,_) -> + Abstract_syntax.Default,s | + Term_definition(s,_,_,_) -> + Abstract_syntax.Default,s | _ -> + failwith "Call a term on a + type")*) + + let empty n = {name=n;size=0;terms=Symbols.empty;types=Symbols.empty;ids=Id.empty} let name {name=n} = n @@ -90,13 +107,13 @@ struct try match Symbols.find s syms with | Type_declaration (x,id,_) when x=s -> Lambda.Atom id - | Type_declaration _ -> failwith "Bug" + | Type_declaration _ -> failwith "Bug in find_atomic_type" | Type_definition (x,id,_,_) when x=s -> Lambda.DAtom id - | Type_definition _ -> failwith "Bug" - | Term_declaration _ -> failwith "Bug" - | Term_definition _ -> failwith "Bug" + | Type_definition _ -> failwith "Bug in find_atomic_type" + | Term_declaration _ -> failwith "Bug in find_atomic_type" + | Term_definition _ -> failwith "Bug in find_atomic_type" with - | Not_found -> failwith "Bug" + | Not_found -> failwith "Bug in find_atomic_type" let rec convert_type ty ({types=syms} as sg) = @@ -136,7 +153,7 @@ struct | Lambda.DAtom i -> (match Id.find i ids with | Type_definition (_,_,_,ty1) -> expand_type ty1 sg - | _ -> failwith "Bug") + | _ -> failwith "Bug in expand type") | 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" @@ -144,7 +161,7 @@ struct let unfold_type_definition i ({ids=ids} as sg) = match Id.find i ids with | Type_definition (_,_,_,ty1) -> expand_type ty1 sg - | _ -> failwith "Bug" + | _ -> failwith "Bug in unfold_type_definition" let rec expand_term t ({ids=ids} as sg) = @@ -153,7 +170,7 @@ struct | Lambda.DConst i -> (match Id.find i ids with | Term_definition (_,_,_,_,u) -> expand_term u sg - | _ -> failwith "Bug") + | _ -> failwith "Bug in expand term") | 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) @@ -162,10 +179,19 @@ struct let unfold_term_definition i ({ids=ids} as sg) = match Id.find i ids with | Term_definition (_,_,_,_,t) -> expand_term t sg - | _ -> failwith "Bug" + | _ -> failwith "Bug in unfold_term_definition" + 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" + let rec decompose_functional_type ty ({ids=ids} as sg) = match ty with | Lambda.LFun (ty1,ty2) -> ty1,ty2,Abstract_syntax.Linear @@ -173,7 +199,7 @@ struct | Lambda.DAtom i -> (match Id.find i ids with | Type_definition (_,_,_,ty1) -> decompose_functional_type ty1 sg - | _ -> failwith "Bug") + | _ -> failwith "Bug in decompose_functional_type") | _ -> raise Not_functional_type @@ -196,13 +222,13 @@ struct (* [get_typing x loc typing_env] returns [l,t,e] where [l] is the level of [x] and [t] its type in the typing environment [typing_env] when [x] is a variable located at [loc]. [e] is the - new environment where [x] as been marcked as used at location - [l]. If [x] has been used alread once (this is marked by the [Some - l], 3rd projection in the association list), the function raises - [Not_linear l] where [l] is the location of the former usage of - [x]. If [x] is not in the typing environment [typing_env], it - raises Not_found *) - + new environment where [x] as been marked as used at location + [l]. If [x] has been used alread once (this is marked by the + [Some l], 3rd projection in the association list), the function + raises [Not_linear l] where [l] is the location of the former + usage of [x]. If [x] is not in the typing environment + [typing_env], it raises Not_found *) + let get_typing x loc lst = let rec get_typing_aux lst k = match lst with @@ -232,7 +258,7 @@ struct let () = Printf.printf "Linear environment:\n%s\n" (Utils.string_of_list "\n" (fun (x,(l,ty,u)) -> Printf.sprintf "%s (%d): %s (%s)" x l (Lambda.type_to_string ty f) (match u with | None -> "Not used" | Some _ -> "Used")) l_env) in let () = Printf.printf "Non linear environment:\n%s\n" (Utils.string_of_list "\n" (fun (x,(l,ty)) -> Printf.sprintf "%s (%d): %s" x l (Lambda.type_to_string ty f) ) env) in Printf.printf "Next usage:\n%s\n" (Utils.string_of_list "\n" (fun (x,ab) -> Printf.sprintf "%s : %s" x (match ab with | Abstract_syntax.Linear -> "Linear" | _ -> "Non Linear")) lin) - + type typing_env_content = | Delay of (int -> int -> Abstract_syntax.location -> Lambda.term) | Eval of (int -> int -> Abstract_syntax.location -> (Lambda.term * typing_env_content)) @@ -419,8 +445,15 @@ struct | Not_linear ((s1,e1),(s2,e2)) -> raise (Error.Error (Error.Type_error (Error.Two_occurrences_of_linear_variable (s2,e2),(s1,s1)))) | Vacuous_abstraction (x,l1,l2) -> raise (Error.Error (Error.Type_error (Error.Vacuous_abstraction (x,l2),l1))) + (* We assume here that [term] is well typed and in beta-normal form + and that types and terms definitions have been unfolded*) - + let eta_long_form term stype sg = + Lambda.eta_long_form (Lambda.normalize (expand_term term sg)) (expand_type stype sg) (fun id -> get_type_of_const_id id sg) + + + + let add_entry e ({size=s} as sg) = match e with | Abstract_syntax.Type_decl (t,_,Abstract_syntax.K k) -> @@ -434,7 +467,7 @@ struct 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 - + let is_type s {types=syms} = try match Symbols.find s syms with @@ -443,7 +476,7 @@ struct | _ -> false with | Symbols.Not_found -> false - + let is_constant s {terms=syms} = try match Symbols.find s syms with @@ -452,47 +485,36 @@ struct | _ -> false,None with | Symbols.Not_found -> false,None - + let add_warnings _ sg = sg - + let get_warnings _ = [] - - 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) - (* (fun i -> - match Id.find i ids with - | Term_declaration(s,_,_) -> Abstract_syntax.Default,s - | Term_definition(s,_,_,_) -> Abstract_syntax.Default,s - | _ -> failwith "Call a term on a type")*) - + + let raw_to_string t = Lambda.raw_to_string t - + let behavior_to_string = function | Abstract_syntax.Default -> "" | Abstract_syntax.Prefix -> "prefix " | Abstract_syntax.Infix -> "infix " | Abstract_syntax.Binder -> "binder " - + 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) - + let to_string ({name=n;ids=ids} as sg) = Printf.sprintf "signature %s = \n%send\n" (fst n) (fst (Id.fold - (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)) + (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)) let convert_term t ty sg = let t_type = convert_type ty sg in @@ -501,11 +523,11 @@ struct let type_of_constant x ({terms=syms} as sg) = try match Symbols.find x syms with - | Term_declaration (s,_,_,ty) when x = s -> ty - | Term_definition (s,_,_,ty,_) when x = s -> ty - | _ -> failwith "Bug" + | Term_declaration (s,_,_,ty) when x = s -> ty + | Term_definition (s,_,_,ty,_) when x = s -> ty + | _ -> failwith "Bug in type_of_constant" with - | Symbols.Not_found -> failwith "Bug" + | Symbols.Not_found -> failwith "Bug in type_of_constant" let fold f a {ids=ids} = Id.fold @@ -522,32 +544,32 @@ struct end module Table = Table.Make_table(struct let b = 10 end) -(*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 = + (*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 = try - let _ = IntMap.find k t in - if override then IntMap.add k v t else raise Conflict + let _ = IntMap.find k t in + if override then IntMap.add k v t else raise Conflict with - | Not_found -> IntMap.add k v t + | Not_found -> IntMap.add k v t - exception Not_found + exception Not_found - let find k t = + let find k t = try - IntMap.find k t + IntMap.find k t with - | Not_found -> raise Not_found - let fold f acc t = IntMap.fold f t acc -end -*) + | Not_found -> raise Not_found + let fold f acc t = IntMap.fold f t acc + end + *) module Sylvains_signature = Make(Tries.Tries)(Table) diff --git a/src/grammars/interface.ml b/src/grammars/interface.ml index e98da5c..4c8e724 100644 --- a/src/grammars/interface.ml +++ b/src/grammars/interface.ml @@ -50,6 +50,7 @@ sig val fold : (entry -> 'a -> 'a) -> 'a -> t -> 'a val get_binder_argument_functional_type : string -> t -> Abstract_syntax.abstraction option val is_declared : entry -> t -> string option + val eta_long_form : term -> stype -> t -> term end module type Lexicon_sig = diff --git a/src/grammars/interface.mli b/src/grammars/interface.mli index 28baa11..87b09cc 100644 --- a/src/grammars/interface.mli +++ b/src/grammars/interface.mli @@ -135,6 +135,10 @@ sig [None] otherwise *) val is_declared : entry -> t -> string option + (** [eta_long_form t ty sg] returns the eta-long form of [t] with + respect to the type [ty] and signature [sg]*) + val eta_long_form : term -> stype -> t -> term + end (** This module signature describes the interface for modules implementing lexicons *) diff --git a/src/grammars/syntactic_data_structures.ml b/src/grammars/syntactic_data_structures.ml index f5a83ce..452e040 100644 --- a/src/grammars/syntactic_data_structures.ml +++ b/src/grammars/syntactic_data_structures.ml @@ -295,6 +295,8 @@ struct let get_binder_argument_functional_type _ _ = Some Abstract_syntax.Linear let is_declared _ _ = None + + let eta_long_form _ _ _ = failwith "Not implemented: useless" let raw_to_string _ = failwith "TUTUTUT" diff --git a/src/logic/lambda.ml b/src/logic/lambda.ml index 58d563d..ff20519 100644 --- a/src/logic/lambda.ml +++ b/src/logic/lambda.ml @@ -82,13 +82,13 @@ module Lambda = let rec unfold_labs acc level env = function | LAbs (x,t) -> let x' = generate_var_name x env in - unfold_labs ((level,x')::acc) (level+1) env t + unfold_labs ((level,x')::acc) (level+1) ((level,x')::env) t | t -> acc,level,t let rec unfold_abs acc level env = function | Abs (x,t) -> let x' = generate_var_name x env in - unfold_abs ((level,x')::acc) (level+1) env t + unfold_abs ((level,x')::acc) (level+1) ((level,x')::env) t | t -> acc,level,t let rec unfold_app acc = function @@ -163,7 +163,7 @@ module Lambda = | DConst i -> let _,x = id_to_sym i in x,true | Abs (x,t) -> let x' = generate_var_name x env in - let vars,l,u=unfold_abs [level,x'] (level+1) env t in + let vars,l,u=unfold_abs [level,x'] (level+1) ((level,x')::env) t in Printf.sprintf "Lambda %s. %s" (Utils.string_of_list " " (fun (_,x) -> x) (List.rev vars)) @@ -171,7 +171,7 @@ module Lambda = false | LAbs (x,t) -> let x' = generate_var_name x l_env in - let vars,l,u=unfold_labs [l_level,x'] (l_level+1) l_env t in + let vars,l,u=unfold_labs [l_level,x'] (l_level+1) ((l_level,x')::l_env) t in Printf.sprintf "lambda %s. %s" (Utils.string_of_list " " (fun (_,x) -> x) (List.rev vars)) @@ -492,5 +492,83 @@ module Lambda = in convert (type_normalize ty1) (type_normalize ty2) + let eta_expand t ty = + let wrap t abstraction l_level nl_level = + let f,l_length,nl_length,abs'= + List.fold_left + (fun (f,l_depth,nl_depth,acc) abs -> + match abs with + | LVar _ -> (fun x -> App(f x,LVar (l_level-l_depth))),l_depth+1,nl_depth,abs::acc + | Var _ -> (fun x -> App(f x,Var (nl_level-nl_depth))),l_depth,nl_depth+1,abs::acc + | _ -> failwith "eta_expand should not be called here") + ((fun x -> x),1,1,[]) + abstraction in + List.fold_left + (fun t abs -> + match abs with + | Var _ -> Abs("x",t) + | LVar _ -> LAbs("x",t) + | _ -> failwith "eta_expand should not be called here") + (f (lift (l_length-1) (nl_length-1) t)) + abs' in + let rec eta_expand_rec ty l_level nl_level acc = + match ty with + | Atom _ -> wrap t acc l_level nl_level + | DAtom _ -> failwith "type definitions should have been unfolded" + | LFun (a,b) -> eta_expand_rec b (l_level+1) nl_level ((LVar 0)::acc) + | Fun (a,b) -> eta_expand_rec b l_level (nl_level+1) ((Var 0)::acc) + | _ -> failwith "Not yet implemented" in + let t' = eta_expand_rec ty 0 0 [] in + t' + + + (* We assume here that [term] is well typed and in beta-normal form + and that types and terms definitions have been unfolded*) + let eta_long_form term stype f_get_type_of_constant = + let rec eta_long_form_rec term stype linear_typing_env non_linear_typing_env = + match term,stype with + | LVar i , Some ty when ty = List.nth linear_typing_env i -> eta_expand term ty,ty + | LVar i , Some _ -> failwith "Term should be well typed" + | LVar i , None -> + let ty = List.nth linear_typing_env i in + eta_expand term ty,ty + | Var i , Some ty when ty = List.nth non_linear_typing_env i -> eta_expand term ty,ty + | Var i , Some _ -> failwith "Term should be well typed" + | Var i , None -> + let ty = List.nth non_linear_typing_env i in + eta_expand term ty,ty + | Const i , Some ty -> eta_expand term ty,ty + | Const i , None -> + let ty = f_get_type_of_constant i in + eta_expand term ty,ty + | DConst _ ,_ -> failwith "All the definitions should have been unfolded" + | Abs (x,t),Some (Fun(a,b) as ty) -> + let t',_ = eta_long_form_rec t (Some b) linear_typing_env (a::non_linear_typing_env) in + Abs(x,t'),ty + | Abs (x,t), None -> failwith "Should be in beta normal form" + | LAbs (x,t),Some (LFun(a,b) as ty) -> + let t',_ = eta_long_form_rec t (Some b) (a::linear_typing_env) non_linear_typing_env in + LAbs(x,t'),ty + | LAbs (x,t), None -> failwith "Should be in beta normal form" + | App (u,v) , None -> + let u',u_type = eta_long_form_rec u None linear_typing_env non_linear_typing_env in + (match u_type with + | (Fun (a,b)|LFun(a,b)) -> + let v',v_type =eta_long_form_rec v (Some a) linear_typing_env non_linear_typing_env in + eta_expand (normalize (App (u',v'))) b, b + | _ -> failwith "Should be well typed") + | App (u,v) , Some ty -> + let u',u_type = eta_long_form_rec u None linear_typing_env non_linear_typing_env in + (match u_type with + | (Fun (a,b)|LFun(a,b)) when ty=b -> + let v',v_type =eta_long_form_rec v (Some a) linear_typing_env non_linear_typing_env in + eta_expand (normalize (App (u',v'))) b, b + | _ -> failwith "Should be well typed") + | _ -> raise Not_yet_implemented in + let t',_ = eta_long_form_rec term (Some stype) [] [] in + normalize t' + + + end diff --git a/src/logic/lambda.mli b/src/logic/lambda.mli index a213a35..51c6f36 100644 --- a/src/logic/lambda.mli +++ b/src/logic/lambda.mli @@ -70,5 +70,14 @@ sig val term_to_string : term -> (int -> Abstract_syntax.syntactic_behavior * string) -> string val raw_to_string : term -> string val normalize : ?id_to_term:(int -> term) -> term -> term + + + (** [eta_long_form t ty type_of_cst] returns the eta-long form of + [t] with respect of type [ty]. [t] is supposed to be in + beta-normal form and all the definitions of [t] and [ty] should + have been unfolded. [type_of_cst i] is a function that returns + the type (with unfolded definitions) of the constant whose id is + [i]. [i] is supposed to be an actual id of a constant.*) + val eta_long_form : term -> stype -> (int -> stype) -> term end -- 2.24.1