From ed7582c5d4463672e4964f15b49df80a0508f691 Mon Sep 17 00:00:00 2001 From: Andrei Paskevich Date: Thu, 18 Mar 2010 15:49:31 +0000 Subject: [PATCH] a bit of renaming around prsymbols and props --- src/core/decl.ml | 18 +++++++++--------- src/core/decl.mli | 24 ++++++++++++------------ src/core/pretty.mli | 2 +- src/core/task.mli | 2 +- src/core/theory.ml | 12 ++++++------ src/core/theory.mli | 4 ++-- src/driver/driver.ml | 4 ++-- src/main.ml | 2 +- src/parser/typing.ml | 4 ++-- src/transform/split_conjunction.ml | 2 +- 10 files changed, 37 insertions(+), 37 deletions(-) diff --git a/src/core/decl.ml b/src/core/decl.ml index 40785023f..37c61b896 100644 --- a/src/core/decl.ml +++ b/src/core/decl.ml @@ -82,12 +82,12 @@ let ls_defn_axiom (_,_,_,f) = f (** Inductive predicate declaration *) -type prop = { +type prsymbol = { pr_name : ident; } module Prop = struct - type t = prop + type t = prsymbol let equal = (==) let hash pr = pr.pr_name.id_tag let compare pr1 pr2 = @@ -97,11 +97,11 @@ module Spr = Set.Make(Prop) module Mpr = Map.Make(Prop) module Hpr = Hashtbl.Make(Prop) -let create_prop n = { pr_name = id_register n } +let create_prsymbol n = { pr_name = id_register n } -type prop_fmla = prop * fmla +type prop = prsymbol * fmla -type ind_decl = lsymbol * prop_fmla list +type ind_decl = lsymbol * prop list (** Proposition declaration *) @@ -110,7 +110,7 @@ type prop_kind = | Plemma | Pgoal -type prop_decl = prop_kind * prop * fmla +type prop_decl = prop_kind * prsymbol * fmla (** Declaration type *) @@ -246,9 +246,9 @@ let create_logic_decl ldl = ignore (List.fold_left check_decl Sid.empty ldl); create_logic_decl ldl -exception InvalidIndDecl of lsymbol * prop -exception TooSpecificIndDecl of lsymbol * prop * term -exception NonPositiveIndDecl of lsymbol * prop * lsymbol +exception InvalidIndDecl of lsymbol * prsymbol +exception TooSpecificIndDecl of lsymbol * prsymbol * term +exception NonPositiveIndDecl of lsymbol * prsymbol * lsymbol exception Found of lsymbol let ls_mem s sps = if Sls.mem s sps then raise (Found s) else false diff --git a/src/core/decl.mli b/src/core/decl.mli index 89f1d68ca..e5438889e 100644 --- a/src/core/decl.mli +++ b/src/core/decl.mli @@ -47,19 +47,19 @@ val ls_defn_axiom : ls_defn -> fmla (** Inductive predicate declaration *) -type prop = private { +type prsymbol = private { pr_name : ident; } -module Spr : Set.S with type elt = prop -module Mpr : Map.S with type key = prop -module Hpr : Hashtbl.S with type key = prop +module Spr : Set.S with type elt = prsymbol +module Mpr : Map.S with type key = prsymbol +module Hpr : Hashtbl.S with type key = prsymbol -val create_prop : preid -> prop +val create_prsymbol : preid -> prsymbol -type prop_fmla = prop * fmla +type prop = prsymbol * fmla -type ind_decl = lsymbol * prop_fmla list +type ind_decl = lsymbol * prop list (* Proposition declaration *) @@ -68,7 +68,7 @@ type prop_kind = | Plemma | Pgoal -type prop_decl = prop_kind * prop * fmla +type prop_decl = prop_kind * prsymbol * fmla (** Declaration type *) @@ -88,7 +88,7 @@ and decl_node = val create_ty_decl : ty_decl list -> decl val create_logic_decl : logic_decl list -> decl val create_ind_decl : ind_decl list -> decl -val create_prop_decl : prop_kind -> prop -> fmla -> decl +val create_prop_decl : prop_kind -> prsymbol -> fmla -> decl (* separate independent groups of declarations *) @@ -102,9 +102,9 @@ exception ConstructorExpected of lsymbol exception IllegalTypeAlias of tysymbol exception UnboundTypeVar of tvsymbol -exception InvalidIndDecl of lsymbol * prop -exception TooSpecificIndDecl of lsymbol * prop * term -exception NonPositiveIndDecl of lsymbol * prop * lsymbol +exception InvalidIndDecl of lsymbol * prsymbol +exception TooSpecificIndDecl of lsymbol * prsymbol * term +exception NonPositiveIndDecl of lsymbol * prsymbol * lsymbol exception IllegalConstructor of lsymbol exception BadLogicDecl of ident diff --git a/src/core/pretty.mli b/src/core/pretty.mli index 26c63bf7d..75d3022e5 100644 --- a/src/core/pretty.mli +++ b/src/core/pretty.mli @@ -34,7 +34,7 @@ val print_vs : formatter -> vsymbol -> unit (* variable *) val print_ts : formatter -> tysymbol -> unit (* type symbol *) val print_ls : formatter -> lsymbol -> unit (* logic symbol *) -val print_pr : formatter -> prop -> unit (* proposition name *) +val print_pr : formatter -> prsymbol -> unit (* proposition name *) val print_ty : formatter -> ty -> unit (* type *) val print_vsty : formatter -> vsymbol -> unit (* variable : type *) diff --git a/src/core/task.mli b/src/core/task.mli index 93641ac4f..8679119b9 100644 --- a/src/core/task.mli +++ b/src/core/task.mli @@ -57,7 +57,7 @@ val task_iter : (decl -> unit) -> task -> unit val task_decls : task -> decl list -val task_goal : task -> prop +val task_goal : task -> prsymbol (* exceptions *) diff --git a/src/core/theory.ml b/src/core/theory.ml index e2d2b2e93..0d4045709 100644 --- a/src/core/theory.ml +++ b/src/core/theory.ml @@ -32,7 +32,7 @@ module Mnm = Mstr type namespace = { ns_ts : tysymbol Mnm.t; (* type symbols *) ns_ls : lsymbol Mnm.t; (* logic symbols *) - ns_pr : prop_fmla Mnm.t; (* propositions *) + ns_pr : prop Mnm.t; (* propositions *) ns_ns : namespace Mnm.t; (* inner namespaces *) } @@ -70,10 +70,10 @@ let rec ns_find get_map ns = function let ns_find_ts = ns_find (fun ns -> ns.ns_ts) let ns_find_ls = ns_find (fun ns -> ns.ns_ls) -let ns_find_pr = ns_find (fun ns -> ns.ns_pr) -let ns_find_prop ns sl = fst (ns_find_pr ns sl) -let ns_find_fmla ns sl = snd (ns_find_pr ns sl) +let ns_find_prop = ns_find (fun ns -> ns.ns_pr) +let ns_find_pr ns sl = fst (ns_find_prop ns sl) +let ns_find_fmla ns sl = snd (ns_find_prop ns sl) (** Theory *) @@ -249,7 +249,7 @@ exception CannotInstantiate of ident type clones = { ts_table : tysymbol Hts.t; ls_table : lsymbol Hls.t; - pr_table : prop_fmla Hpr.t; + pr_table : prop Hpr.t; id_table : ident Hid.t; nw_local : unit Hid.t; id_local : Sid.t; @@ -298,7 +298,7 @@ let cl_find_ls cl ls = let cl_trans_fmla cl f = f_s_map (cl_find_ts cl) (cl_find_ls cl) f let cl_trans_prop cl (pr,f) = - let pr' = create_prop (id_dup pr.pr_name) in + let pr' = create_prsymbol (id_dup pr.pr_name) in let f' = cl_trans_fmla cl f in Hid.add cl.id_table pr.pr_name pr'.pr_name; Hpr.add cl.pr_table pr (pr',f'); diff --git a/src/core/theory.mli b/src/core/theory.mli index d09d30b45..aed18812f 100644 --- a/src/core/theory.mli +++ b/src/core/theory.mli @@ -30,13 +30,13 @@ module Mnm : Map.S with type key = string type namespace = private { ns_ts : tysymbol Mnm.t; (* type symbols *) ns_ls : lsymbol Mnm.t; (* logic symbols *) - ns_pr : prop_fmla Mnm.t; (* propositions *) + ns_pr : prop Mnm.t; (* propositions *) ns_ns : namespace Mnm.t; (* inner namespaces *) } val ns_find_ts : namespace -> string list -> tysymbol val ns_find_ls : namespace -> string list -> lsymbol -val ns_find_pr : namespace -> string list -> prop_fmla +val ns_find_pr : namespace -> string list -> prsymbol val ns_find_prop : namespace -> string list -> prop val ns_find_fmla : namespace -> string list -> fmla diff --git a/src/driver/driver.ml b/src/driver/driver.ml index 04b4a1e2d..36cccd152 100644 --- a/src/driver/driver.ml +++ b/src/driver/driver.ml @@ -231,7 +231,7 @@ let load_rules env clone driver {thr_name = loc,qualid; thr_rules = trl} = begin try add_htheory c - (ns_find_prop th.th_export q).pr_name Remove + (ns_find_pr th.th_export q).pr_name Remove with Not_found -> errorm ~loc "Unknown axioms %s" (string_of_qualid qualid q) end @@ -272,7 +272,7 @@ let load_rules env clone driver {thr_name = loc,qualid; thr_rules = trl} = | Rtagpr (c,(loc,q),s) -> begin try - add_htheory c (ns_find_prop th.th_export q).pr_name + add_htheory c (ns_find_pr th.th_export q).pr_name (Tag (Sstr.singleton s)) with Not_found -> errorm ~loc "Unknown proposition %s" (string_of_qualid qualid q) diff --git a/src/main.ml b/src/main.ml index 0760a4115..b8720a543 100644 --- a/src/main.ml +++ b/src/main.ml @@ -201,7 +201,7 @@ let do_file env drv filename_printer file = | Some s -> Some (Hashtbl.fold (fun s l acc -> - let pr = try fst (ns_find_pr th.th_export l) with Not_found -> + let pr = try ns_find_pr th.th_export l with Not_found -> eprintf "File %s : --goal : Unknown goal %s@." file s ; exit 1 in Decl.Spr.add pr acc ) s Decl.Spr.empty) in diff --git a/src/parser/typing.ml b/src/parser/typing.ml index 2c6413904..139101b00 100644 --- a/src/parser/typing.ml +++ b/src/parser/typing.ml @@ -911,7 +911,7 @@ let fmla env f = let add_prop k loc s f th = let f = fmla th f in try - add_decl th (create_prop_decl k (create_prop (id_user s.id loc)) f) + add_decl th (create_prop_decl k (create_prsymbol (id_user s.id loc)) f) with ClashSymbol _ -> error ~loc (Clash s.id) @@ -1010,7 +1010,7 @@ let add_inductives dl th = let id = d.in_ident.id in let ps = Hashtbl.find psymbols id in let clause (loc, id, f) = - create_prop (id_user id.id loc), fmla th' f + create_prsymbol (id_user id.id loc), fmla th' f in ps, List.map clause d.in_def in diff --git a/src/transform/split_conjunction.ml b/src/transform/split_conjunction.ml index 786c31721..64936926c 100644 --- a/src/transform/split_conjunction.ml +++ b/src/transform/split_conjunction.ml @@ -85,7 +85,7 @@ let elt split_pos d = | Dprop (Pgoal,pr,f) -> let l = split_pos [] f in List.map (fun p -> [create_prop_decl Pgoal - (create_prop (id_clone pr.pr_name)) p]) l + (create_prsymbol (id_clone pr.pr_name)) p]) l | _ -> [[d]] let t fsp = Register.store (fun () -> Trans.decl_l (elt fsp) None) -- GitLab