From 278b2e5bc53906f11647a3abd6d2d2e3d089413d Mon Sep 17 00:00:00 2001 From: Francois Bobot Date: Thu, 4 Mar 2010 12:43:18 +0000 Subject: [PATCH] decl_or_use devient decl --- src/core/context.ml | 121 ++++++++++++++++++ src/core/theory.ml | 71 +++++----- src/core/theory.mli | 49 ++++--- src/pretty.ml | 12 +- src/pretty.mli | 4 - src/transform/flatten.ml | 12 +- src/transform/flatten.mli | 2 +- src/transform/inlining.ml | 8 +- src/transform/inlining.mli | 2 - .../simplify_recursive_definition.ml | 6 +- .../simplify_recursive_definition.mli | 2 - src/transform/transform.ml | 10 -- src/transform/transform.mli | 3 - src/util/pp.ml | 1 + src/util/pp.mli | 1 + 15 files changed, 197 insertions(+), 107 deletions(-) create mode 100644 src/core/context.ml diff --git a/src/core/context.ml b/src/core/context.ml new file mode 100644 index 000000000..bb18901ae --- /dev/null +++ b/src/core/context.ml @@ -0,0 +1,121 @@ +open Ident +open Theory + +type puc_def = + | Ktype of type_decl + | Klogic of logic_decl + | Kprop of prop + +type puc = { puc_next : (puc * Theory.decl) option; + puc_tag : int; + puc_known : decl Mid.t; + puc_def : puc_def Mid.t; + } + + +module S = + struct + type t = puc + let hash puc = match puc.puc_next with + | None -> 0 + | Some (n,d) -> 1 + (Hashcons.combine n.puc_tag d.d_tag) + + let equal a b = + match a.puc_next,b.puc_next with + | None, None -> true + | Some (na,da), Some (nb,db) -> na.puc_next == nb.puc_next && da.d_tag == db.d_tag + | _ -> false + + let tag i puc = {puc with puc_tag = i} + end + +module Hsh = Hashcons.Make(S) + +let nil = Hsh.hashcons {puc_next = None; puc_known = Mid.empty; puc_tag = -1} +(* +(* Manage new declaration *) + +exception RedeclaredIdent of ident +exception UnknownIdent of ident + +let add_known decl (id,def) puc = + try + if (Mid.find id uc.puc_known) != decl then raise (RedeclaredIdent id) + with Not_found -> (); + { puc with + puc_known = Mid.add id decl puc.puc_known; + puc_def = Mid.add id def puc.puc_def } + +let add_type uc decl (ts,def) = + let uc = add_known decl ts.ts_name uc in + match def with + | Tabstract -> uc + | Talgebraic lfs -> + let add_constr uc fs = add_known decl (fs.fs_name, uc in + List.fold_left add_constr uc lfs + +let check_type kn (ts,def) = match def with + | Tabstract -> + begin match ts.ts_def with + | Some ty -> known_ty kn ty + | None -> () + end + | Talgebraic lfs -> + let check fs = List.iter (known_ty kn) (fst fs.fs_scheme) in + List.iter check lfs + +let add_logic uc = function + | Lfunction (fs, df) -> + let uc = add_symbol add_fs fs.fs_name fs uc in + if df == None then add_param fs.fs_name uc else uc + | Lpredicate (ps, dp) -> + let uc = add_symbol add_ps ps.ps_name ps uc in + if dp == None then add_param ps.ps_name uc else uc + | Linductive (ps, la) -> + let uc = add_symbol add_ps ps.ps_name ps uc in + let add uc (id,f) = add_symbol add_pr id f uc in + List.fold_left add uc la + +let check_logic kn = function + | Lfunction (fs, df) -> + known_ty kn (snd fs.fs_scheme); + List.iter (known_ty kn) (fst fs.fs_scheme); + begin match df with + | Some (_,_,_,f) -> known_fmla kn f + | None -> () + end + | Lpredicate (ps, dp) -> + List.iter (known_ty kn) ps.ps_scheme; + begin match dp with + | Some (_,_,_,f) -> known_fmla kn f + | None -> () + end + | Linductive (ps, la) -> + List.iter (known_ty kn) ps.ps_scheme; + let check (_,f) = known_fmla kn f in + List.iter check la + + +let add_decl uc d = + let uc = match d.d_node with + | Dtype dl -> + let uc = List.fold_left (add_type d) uc dl in + List.iter (check_type uc.uc_known) dl; + uc + | Dlogic dl -> + let uc = List.fold_left (add_logic uc dl in + List.iter (check_logic uc.uc_known) dl; + uc + | Dprop (k, id, f) -> + known_fmla uc.uc_known f; + add_symbol add_pr id f uc + | Dclone _ | Duse _ -> assert false + in + { uc with uc_decls = d :: uc.uc_decls } + + +let cons n d = + + Hsh.hashcons {puc_next = None;known = Mid.empty; puc_tag = -1} + +*) diff --git a/src/core/theory.ml b/src/core/theory.ml index b8b6fc150..280eba674 100644 --- a/src/core/theory.ml +++ b/src/core/theory.ml @@ -55,12 +55,35 @@ type prop_decl = prop_kind * ident * fmla (* declaration *) -type decl_node = +(** Theory *) + +module Snm = Set.Make(String) +module Mnm = Map.Make(String) + +type theory = { + th_name : ident; + th_param : Sid.t; (* locally declared abstract symbols *) + th_known : ident Mid.t; (* imported and locally declared symbols *) + th_export : namespace; + th_decls : decl list; +} + +and namespace = { + ns_ts : tysymbol Mnm.t; (* type symbols *) + ns_ls : lsymbol Mnm.t; (* logic symbols *) + ns_ns : namespace Mnm.t; (* inner namespaces *) + ns_pr : fmla Mnm.t; (* propositions *) +} + +and decl_node = | Dtype of ty_decl list | Dlogic of logic_decl list | Dprop of prop_decl + | Duse of theory + | Dclone of (ident * ident) list -type decl = { + +and decl = { d_node : decl_node; d_tag : int; } @@ -112,11 +135,14 @@ module D = struct let hash d = match d.d_node with | Dtype l -> Hashcons.combine_list hs_td 0 l - | Dlogic l -> Hashcons.combine_list hs_ld 1 l - | Dprop (Paxiom,i,f) -> Hashcons.combine2 0 i.id_tag f.f_tag - | Dprop (Plemma,i,f) -> Hashcons.combine2 1 i.id_tag f.f_tag - | Dprop (Pgoal, i,f) -> Hashcons.combine2 2 i.id_tag f.f_tag - + | Dlogic l -> Hashcons.combine_list hs_ld 3 l + | Dprop (Paxiom,i,f) -> Hashcons.combine2 7 i.id_tag f.f_tag + | Dprop (Plemma,i,f) -> Hashcons.combine2 11 i.id_tag f.f_tag + | Dprop (Pgoal, i,f) -> Hashcons.combine2 13 i.id_tag f.f_tag + | Duse th -> 17 * th.th_name.id_tag + | Dclone sl -> Hashcons.combine_list + (fun (i1,i2) -> Hashcons.combine i1.id_tag i2.id_tag) + 19 sl let tag n d = { d with d_tag = n } let compare d1 d2 = Pervasives.compare d1.d_tag d2.d_tag @@ -214,30 +240,6 @@ let create_prop k i f = create_prop k i f -(** Theory *) - -module Snm = Set.Make(String) -module Mnm = Map.Make(String) - -type theory = { - th_name : ident; - th_param : Sid.t; (* locally declared abstract symbols *) - th_known : ident Mid.t; (* imported and locally declared symbols *) - th_export : namespace; - th_decls : decl_or_use list; -} - -and namespace = { - ns_ts : tysymbol Mnm.t; (* type symbols *) - ns_ls : lsymbol Mnm.t; (* logic symbols *) - ns_ns : namespace Mnm.t; (* inner namespaces *) - ns_pr : fmla Mnm.t; (* propositions *) -} - -and decl_or_use = - | Decl of decl - | Use of theory - (** Theory under construction *) @@ -247,7 +249,7 @@ type theory_uc = { uc_known : ident Mid.t; uc_import : namespace list; uc_export : namespace list; - uc_decls : decl_or_use list; + uc_decls : decl list; } @@ -398,7 +400,7 @@ let use_export uc th = uc_import = merge_ns th.th_export i0 :: sti; uc_export = merge_ns th.th_export e0 :: ste; uc_known = merge_known uc.uc_known th.th_known; - uc_decls = Use th :: uc.uc_decls; + uc_decls = mk_decl (Duse th) :: uc.uc_decls; } | _ -> assert false @@ -471,8 +473,9 @@ let add_decl uc d = | Dprop (k, id, f) -> known_fmla uc.uc_known f; add_symbol add_pr id f uc + | Dclone _ | Duse _ -> assert false in - { uc with uc_decls = Decl d :: uc.uc_decls } + { uc with uc_decls = d :: uc.uc_decls } (** Clone theories *) diff --git a/src/core/theory.mli b/src/core/theory.mli index c4bcf2258..42c859361 100644 --- a/src/core/theory.mli +++ b/src/core/theory.mli @@ -51,13 +51,34 @@ type prop_kind = type prop_decl = prop_kind * ident * fmla (* declaration *) +(** Theory *) -type decl_node = +module Snm : Set.S with type elt = string +module Mnm : Map.S with type key = string + +type theory = private { + th_name : ident; + th_param : Sid.t; (* locally declared abstract symbols *) + th_known : ident Mid.t; (* imported and locally declared symbols *) + th_export : namespace; + th_decls : decl list; +} + +and namespace = private { + ns_ts : tysymbol Mnm.t; (* type symbols *) + ns_ls : lsymbol Mnm.t; (* logic symbols *) + ns_ns : namespace Mnm.t; (* inner namespaces *) + ns_pr : fmla Mnm.t; (* propositions *) +} + +and decl_node = | Dtype of ty_decl list | Dlogic of logic_decl list | Dprop of prop_decl + | Duse of theory + | Dclone of (ident * ident) list -type decl = private { +and decl = private { d_node : decl_node; d_tag : int; } @@ -87,30 +108,6 @@ exception IllegalConstructor of lsymbol exception UnboundVars of Svs.t exception BadDecl of ident -(** Theory *) - -module Snm : Set.S with type elt = string -module Mnm : Map.S with type key = string - -type theory = private { - th_name : ident; - th_param : Sid.t; (* locally declared abstract symbols *) - th_known : ident Mid.t; (* imported and locally declared symbols *) - th_export : namespace; - th_decls : decl_or_use list; -} - -and namespace = private { - ns_ts : tysymbol Mnm.t; (* type symbols *) - ns_ls : lsymbol Mnm.t; (* logic symbols *) - ns_ns : namespace Mnm.t; (* inner namespaces *) - ns_pr : fmla Mnm.t; (* propositions *) -} - -and decl_or_use = - | Decl of decl - | Use of theory - (* theory construction *) type theory_uc (* a theory under construction *) diff --git a/src/pretty.ml b/src/pretty.ml index 5aa4b4bcb..1bed77865 100644 --- a/src/pretty.ml +++ b/src/pretty.ml @@ -164,19 +164,15 @@ let print_decl fmt d = match d.d_node with (match k with Paxiom -> "axiom" | Pgoal -> "goal" | Plemma -> "lemma") print_ident id print_fmla fmla + | Duse u -> fprintf fmt "use export %a@\n" print_ident u.th_name + | Dclone il -> fprintf fmt "(*@[clone export _ with %a@]@\n" + (print_list comma (print_pair_delim nothing nothing equal print_ident print_ident)) il let print_decl_list fmt de = fprintf fmt "@[%a@]" (print_list newline print_decl) de -let print_decl_or_use fmt = function - | Decl d -> fprintf fmt "%a" print_decl d - | Use u -> fprintf fmt "use export %a@\n" print_ident u.th_name - -let print_decl_or_use_list fmt de = - fprintf fmt "@[%a@]" (print_list newline print_decl_or_use) de - let print_theory fmt t = fprintf fmt "@[@[theory %a@\n%a@]@\nend@]@\n@\n" print_ident t.th_name - print_decl_or_use_list t.th_decls; + print_decl_list t.th_decls; fprintf fmt "@?" diff --git a/src/pretty.mli b/src/pretty.mli index 3b8beadc4..0f2a19218 100644 --- a/src/pretty.mli +++ b/src/pretty.mli @@ -39,8 +39,4 @@ val print_decl : formatter -> decl -> unit val print_decl_list : formatter -> decl list -> unit -val print_decl_or_use : formatter -> decl_or_use -> unit - -val print_decl_or_use_list : formatter -> decl_or_use list -> unit - val print_theory : formatter -> theory -> unit diff --git a/src/transform/flatten.ml b/src/transform/flatten.ml index a709a722d..df8f6d09c 100644 --- a/src/transform/flatten.ml +++ b/src/transform/flatten.ml @@ -1,10 +1,12 @@ open Theory +(* Il faut supprimer les goals et transformer les lemmes en axioms *) + let elt a = - let rec aux acc = function - | Decl a -> a::acc - | Use t -> List.fold_left aux acc t.th_decls in - List.rev (aux [] a) + let rec aux acc d = match d.d_node with + | Duse t -> List.fold_left aux (d::acc) t.th_decls + | _ -> d::acc + in List.rev (aux [] a) -let t = Transform.TDecl_or_Use_Decl.elt elt +let t = Transform.TDecl.elt elt diff --git a/src/transform/flatten.mli b/src/transform/flatten.mli index ce854d07f..8167c3e93 100644 --- a/src/transform/flatten.mli +++ b/src/transform/flatten.mli @@ -1,3 +1,3 @@ (* a list of decl_or_use to a list of decl *) -val t : (Theory.decl_or_use,Theory.decl) Transform.t +val t : (Theory.decl,Theory.decl) Transform.t diff --git a/src/transform/inlining.ml b/src/transform/inlining.ml index 86e870fd9..18818fa70 100644 --- a/src/transform/inlining.ml +++ b/src/transform/inlining.ml @@ -89,12 +89,6 @@ let fold env d = ) dl)] | Dtype dl -> env,[d] | Dprop (k,i,fmla) -> env,[create_prop k (id_dup i) (replacep env fmla)] + | Duse _ | Dclone _ -> env,[d] let t = Transform.TDecl.fold_map_left fold empty_env - -let t_use = Transform.TDecl_or_Use.fold_map_left - (fun env d -> match d with - | Decl d -> let env,l = (fold env d) in - env,List.map (fun d -> Decl d) l - | Use _ as u -> env,[u]) empty_env - diff --git a/src/transform/inlining.mli b/src/transform/inlining.mli index b520b3ffe..586ebb04d 100644 --- a/src/transform/inlining.mli +++ b/src/transform/inlining.mli @@ -1,5 +1,3 @@ (* Inline the definition not recursive *) val t : (Theory.decl,Theory.decl) Transform.t - -val t_use : (Theory.decl_or_use,Theory.decl_or_use) Transform.t diff --git a/src/transform/simplify_recursive_definition.ml b/src/transform/simplify_recursive_definition.ml index 71418c55d..9f9494917 100644 --- a/src/transform/simplify_recursive_definition.ml +++ b/src/transform/simplify_recursive_definition.ml @@ -144,10 +144,6 @@ let elt d = Mid.add ts.ts_name s acc) Mid.empty l in let l = connexe m in List.map (fun e -> create_type (List.map (Hid.find mem) e)) l + | Dclone _ | Duse _ -> [d] let t = Transform.TDecl.elt elt - -let t_use = Transform.TDecl_or_Use.elt - (function - | Decl d -> List.map (fun d -> Decl d) (elt d) - | Use _ as u -> [u]) diff --git a/src/transform/simplify_recursive_definition.mli b/src/transform/simplify_recursive_definition.mli index 013787f96..2b239422b 100644 --- a/src/transform/simplify_recursive_definition.mli +++ b/src/transform/simplify_recursive_definition.mli @@ -21,5 +21,3 @@ (* Simplify the recursive type and logic definition *) val t : (Theory.decl,Theory.decl) Transform.t - -val t_use : (Theory.decl_or_use,Theory.decl_or_use) Transform.t diff --git a/src/transform/transform.ml b/src/transform/transform.ml index 422dc9359..b14ef8835 100644 --- a/src/transform/transform.ml +++ b/src/transform/transform.ml @@ -192,14 +192,6 @@ module SDecl = let tag x = x.d_tag end -module SDecl_or_Use = - struct - type t = decl_or_use - let tag = function - | Decl d -> -d.d_tag - | Use t -> 1+t.th_name.Ident.id_tag - end - module STheory = struct type t = theory @@ -219,7 +211,5 @@ module SFmla = end module TDecl = Make(SDecl)(SDecl) -module TDecl_or_Use = Make(SDecl_or_Use)(SDecl_or_Use) -module TDecl_or_Use_Decl = Make(SDecl_or_Use)(SDecl) module TTheory = Make(STheory)(STheory) module TTheory_Decl = Make(STheory)(SDecl) diff --git a/src/transform/transform.mli b/src/transform/transform.mli index 4b6182610..f53d4e011 100644 --- a/src/transform/transform.mli +++ b/src/transform/transform.mli @@ -74,7 +74,6 @@ open Term module STerm : Sig with type t = term module SFmla : Sig with type t = fmla module SDecl : Sig with type t = decl -module SDecl_or_Use : Sig with type t = decl_or_use module STheory : Sig with type t = theory (* The functor to construct transformation from one S.t to another *) @@ -82,7 +81,5 @@ module Make (X1 : Sig)(X2 : Sig) : S with type t1 = X1.t with type t2 = X2.t (* Predefined transformation *) module TDecl : S with type t1 = decl and type t2 = decl -module TDecl_or_Use : S with type t1 = decl_or_use and type t2 = decl_or_use -module TDecl_or_Use_Decl : S with type t1 = decl_or_use and type t2 = decl module TTheory : S with type t1 = theory and type t2 = theory module TTheory_Decl : S with type t1 = theory and type t2 = decl diff --git a/src/util/pp.ml b/src/util/pp.ml index 82a8a0d36..45096147d 100644 --- a/src/util/pp.ml +++ b/src/util/pp.ml @@ -71,6 +71,7 @@ let underscore fmt () = fprintf fmt "_" let semi fmt () = fprintf fmt ";@ " let space fmt () = fprintf fmt " " let alt fmt () = fprintf fmt "|@ " +let equal fmt () = fprintf fmt "@ =@ " let newline fmt () = fprintf fmt "@\n" let newline2 fmt () = fprintf fmt "@\n@\n" let arrow fmt () = fprintf fmt "@ -> " diff --git a/src/util/pp.mli b/src/util/pp.mli index 5dccda21a..44bfa771c 100644 --- a/src/util/pp.mli +++ b/src/util/pp.mli @@ -68,6 +68,7 @@ val comma : formatter -> unit -> unit val simple_comma : formatter -> unit -> unit val semi : formatter -> unit -> unit val underscore : formatter -> unit -> unit +val equal : formatter -> unit -> unit val arrow : formatter -> unit -> unit val lbrace : formatter -> unit -> unit val rbrace : formatter -> unit -> unit -- GitLab