Commit c8a04147 authored by POGODALLA Sylvain's avatar POGODALLA Sylvain

eta expansion added

parent 6ff347dc
......@@ -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 -> ""
......
......@@ -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,12 +222,12 @@ 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 =
......@@ -419,6 +445,13 @@ 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) =
......@@ -457,17 +490,6 @@ struct
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
......@@ -503,9 +525,9 @@ struct
match Symbols.find x syms with
| Term_declaration (s,_,_,ty) when x = s -> ty
| Term_definition (s,_,_,ty,_) when x = s -> ty
| _ -> failwith "Bug"
| _ -> 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,8 +544,8 @@ struct
end
module Table = Table.Make_table(struct let b = 10 end)
(*module Table =
struct
(*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
......@@ -546,8 +568,8 @@ struct
with
| Not_found -> raise Not_found
let fold f acc t = IntMap.fold f t acc
end
*)
end
*)
module Sylvains_signature = Make(Tries.Tries)(Table)
......
......@@ -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 =
......
......@@ -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 *)
......
......@@ -296,6 +296,8 @@ struct
let is_declared _ _ = None
let eta_long_form _ _ _ = failwith "Not implemented: useless"
let raw_to_string _ = failwith "TUTUTUT"
......
......@@ -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
......@@ -71,4 +71,13 @@ sig
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
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment