Commit 278b2e5b authored by Francois Bobot's avatar Francois Bobot

decl_or_use devient decl

parent a9822e0b
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}
*)
......@@ -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 *)
......
......@@ -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 *)
......
......@@ -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 "(*@[<hov 2>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 "@[<hov>%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 "@[<hov>%a@]" (print_list newline print_decl_or_use) de
let print_theory fmt t =
fprintf fmt "@[@[<hov 2>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 "@?"
......@@ -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
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
(* 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
......@@ -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
(* 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
......@@ -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])
......@@ -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
......@@ -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)
......@@ -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
......@@ -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 "@ -> "
......
......@@ -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
......
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