Commit 259be340 authored by Andrei Paskevich's avatar Andrei Paskevich

replace abstract types tvsymbol and prop with one-field records.

Interface consistency is god.
parent 2854bc40
......@@ -82,14 +82,22 @@ let ls_defn_axiom (_,_,_,f) = f
(** Inductive predicate declaration *)
type prop = ident
type prop = {
pr_name : ident;
}
module Spr = Sid
module Mpr = Mid
module Hpr = Hid
module Prop = struct
type t = prop
let equal = (==)
let hash pr = pr.pr_name.id_tag
let compare pr1 pr2 =
Pervasives.compare pr1.pr_name.id_tag pr2.pr_name.id_tag
end
module Spr = Set.Make(Prop)
module Mpr = Map.Make(Prop)
module Hpr = Hashtbl.Make(Prop)
let create_prop = id_register
let pr_name x = x
let create_prop n = { pr_name = id_register n }
type prop_fmla = prop * fmla
......@@ -157,9 +165,9 @@ module Decl = struct
let hs_ld (ls,ld) = Hashcons.combine ls.ls_name.id_tag
(Hashcons.combine_option (fun (_,_,_,f) -> f.f_tag) ld)
let hs_ind (ps,al) =
let hs_pair (pr,f) = Hashcons.combine pr.id_tag f.f_tag in
Hashcons.combine_list hs_pair ps.ls_name.id_tag al
let hs_prop (pr,f) = Hashcons.combine pr.pr_name.id_tag f.f_tag
let hs_ind (ps,al) = Hashcons.combine_list hs_prop ps.ls_name.id_tag al
let hs_kind = function
| Paxiom -> 7
......@@ -170,7 +178,7 @@ module Decl = struct
| Dtype l -> Hashcons.combine_list hs_td 0 l
| Dlogic l -> Hashcons.combine_list hs_ld 3 l
| Dind l -> Hashcons.combine_list hs_ind 5 l
| Dprop (k,pr,f) -> Hashcons.combine2 (hs_kind k) pr.id_tag f.f_tag
| Dprop (k,pr,f) -> Hashcons.combine (hs_kind k) (hs_prop (pr,f))
let tag n d = { d with d_tag = n }
......@@ -280,7 +288,7 @@ let create_ind_decl idl =
(try ignore (List.for_all (f_pos_ps sps (Some true)) cls)
with Found ls ->
raise (NonPositiveIndDecl (ps, pr, ls)));
add_id acc (pr_name pr)
add_id acc pr.pr_name
| _ -> raise (InvalidIndDecl (ps, pr))
in
let check_decl acc (ps,al) =
......
......@@ -47,14 +47,15 @@ val ls_defn_axiom : ls_defn -> fmla
(** Inductive predicate declaration *)
type prop
type prop = 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
val create_prop : preid -> prop
val pr_name : prop -> ident
type prop_fmla = prop * fmla
......
......@@ -60,9 +60,9 @@ let tv_set = ref Sid.empty
(* type variables always start with a quote *)
let print_tv fmt tv =
tv_set := Sid.add (tv_name tv) !tv_set;
tv_set := Sid.add tv.tv_name !tv_set;
let sanitize n = "'" ^ n in
let n = id_unique iprinter ~sanitizer:sanitize (tv_name tv) in
let n = id_unique iprinter ~sanitizer:sanitize tv.tv_name in
fprintf fmt "%s" n
let forget_tvs () =
......@@ -96,8 +96,8 @@ let print_ls fmt ls =
fprintf fmt "%s" n
let print_pr fmt pr =
Hid.replace phash (pr_name pr) pr;
fprintf fmt "%s" (id_unique pprinter (pr_name pr))
Hid.replace phash pr.pr_name pr;
fprintf fmt "%s" (id_unique pprinter pr.pr_name)
(** Types *)
......
......@@ -106,7 +106,7 @@ let check_logic kn (ls,ld) =
let add_ind d kn (ps,la) =
let kn = add_known ps.ls_name d kn in
let add kn (pr,_) = add_known (pr_name pr) d kn in
let add kn (pr,_) = add_known pr.pr_name d kn in
List.fold_left add kn la
let check_ind kn (ps,la) =
......@@ -118,7 +118,7 @@ let add_decl kn d = match d.d_node with
| Dtype dl -> List.fold_left (add_type d) kn dl
| Dlogic dl -> List.fold_left (add_logic d) kn dl
| Dind dl -> List.fold_left (add_ind d) kn dl
| Dprop (_,pr,_) -> add_known (pr_name pr) d kn
| Dprop (_,pr,_) -> add_known pr.pr_name d kn
let check_decl kn d = match d.d_node with
| Dtype dl -> List.iter (check_type kn) dl
......
......@@ -201,10 +201,10 @@ let add_logic uc (ls,_) = add_symbol add_ls ls.ls_name ls uc
let add_ind uc (ps,la) =
let uc = add_symbol add_ls ps.ls_name ps uc in
let add uc (pr,f) = add_symbol add_pr (pr_name pr) (pr,f) uc in
let add uc (pr,f) = add_symbol add_pr pr.pr_name (pr,f) uc in
List.fold_left add uc la
let add_prop uc (_,pr,f) = add_symbol add_pr (pr_name pr) (pr,f) uc
let add_prop uc (_,pr,f) = add_symbol add_pr pr.pr_name (pr,f) uc
let add_decl uc d =
let uc = match d.d_node with
......@@ -298,9 +298,9 @@ 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_name pr)) in
let pr' = create_prop (id_dup pr.pr_name) in
let f' = cl_trans_fmla cl f in
Hid.add cl.id_table (pr_name pr) (pr_name pr');
Hid.add cl.id_table pr.pr_name pr'.pr_name;
Hpr.add cl.pr_table pr (pr',f');
pr', f'
......@@ -333,8 +333,7 @@ let cl_init_ls cl ls ls' =
cl_add_ls cl ls ls'
let cl_init_pr cl pr =
let id = pr_name pr in
if not (Sid.mem id cl.id_local) then raise (NonLocal id)
if not (Sid.mem pr.pr_name cl.id_local) then raise (NonLocal pr.pr_name)
let cl_init th inst =
let cl = empty_clones th.th_local in
......@@ -358,7 +357,7 @@ let cl_new_ls cl ls =
let cl_new_prop cl pf =
let pf' = cl_trans_prop cl pf in
Hid.add cl.nw_local (pr_name (fst pf')) ();
Hid.add cl.nw_local (fst pf').pr_name ();
pf'
let cl_add_type cl inst_ts acc (ts, def) =
......@@ -464,7 +463,7 @@ let clone_export uc th inst =
then Hls.find cl.ls_table ls else ls in
let find_pr (pr,f) =
if Sid.mem (pr_name pr) th.th_local
if Sid.mem pr.pr_name th.th_local
then Hpr.find cl.pr_table pr else (pr,f) in
let f_ts n ts ns = add_ts true n (find_ts ts) ns in
......
......@@ -22,14 +22,22 @@ open Ident
(** Types *)
type tvsymbol = ident
type tvsymbol = {
tv_name : ident;
}
module Stv = Sid
module Mtv = Mid
module Htv = Hid
module Tvar = struct
type t = tvsymbol
let equal = (==)
let hash tv = tv.tv_name.id_tag
let compare tv1 tv2 =
Pervasives.compare tv1.tv_name.id_tag tv2.tv_name.id_tag
end
module Stv = Set.Make(Tvar)
module Mtv = Map.Make(Tvar)
module Htv = Hashtbl.Make(Tvar)
let create_tvsymbol = id_register
let tv_name v = v
let create_tvsymbol n = { tv_name = id_register n }
(* type symbols and types *)
......@@ -79,7 +87,7 @@ module Ty = struct
let hash_ty ty = ty.ty_tag
let hash ty = match ty.ty_node with
| Tyvar v -> v.id_tag
| Tyvar v -> v.tv_name.id_tag
| Tyapp (s, tl) -> Hashcons.combine_list hash_ty s.ts_name.id_tag tl
let tag n ty = { ty with ty_tag = n }
......
......@@ -21,14 +21,15 @@ open Ident
(** Types *)
type tvsymbol
type tvsymbol = private {
tv_name : ident;
}
module Stv : Set.S with type elt = tvsymbol
module Mtv : Map.S with type key = tvsymbol
module Htv : Hashtbl.S with type key = tvsymbol
val create_tvsymbol : preid -> tvsymbol
val tv_name : tvsymbol -> ident
(* type symbols and types *)
......
......@@ -231,7 +231,7 @@ let load_rules env clone driver {thr_name = loc,qualid; thr_rules = trl} =
begin
try
add_htheory c
(pr_name (ns_find_prop th.th_export q)) Remove
(ns_find_prop 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 (pr_name (ns_find_prop th.th_export q))
add_htheory c (ns_find_prop th.th_export q).pr_name
(Tag (Sstr.singleton s))
with Not_found -> errorm ~loc "Unknown proposition %s"
(string_of_qualid qualid q)
......@@ -386,7 +386,7 @@ let filename_of_goal drv ident_printer filename theory_name task =
match drv.drv_filename with
| None -> errorm "no filename syntax given"
| Some f ->
let pr_name = pr_name (task_goal task) in
let pr_name = (task_goal task).pr_name in
let repl_fun s =
let i = matched_group 1 s in
match i with
......
......@@ -260,7 +260,7 @@ let do_file env drv filename_printer file =
let res = Driver.call_prover ~debug:!debug ?timeout env cl drv task in
printf "%s %s %s : %a@."
file th.th_name.Ident.id_short
(Decl.pr_name (task_goal task)).Ident.id_long
((task_goal task).Decl.pr_name).Ident.id_long
Call_provers.print_prover_result res in
List.iter call goals
end
......
......@@ -154,7 +154,7 @@ let rec print_dty fmt = function
| Tyvar { type_val = Some t } ->
print_dty fmt t
| Tyvar { type_val = None; tvsymbol = v } ->
fprintf fmt "'%s" (tv_name v).id_short
fprintf fmt "'%s" v.tv_name.id_short
| Tyapp (s, []) ->
fprintf fmt "%s" s.ts_name.id_short
| Tyapp (s, [t]) ->
......@@ -795,7 +795,7 @@ let add_types dl th =
let vars = th'.utyvars in
List.iter
(fun v ->
Hashtbl.add vars (tv_name v).id_short
Hashtbl.add vars v.tv_name.id_short
(create_ty_decl_var ~user:true v))
ts.ts_args;
ts, th'
......@@ -1018,11 +1018,11 @@ let add_inductives dl th =
try
List.fold_left add_decl th (create_ind_decls dl)
with
| InvalidIndDecl (_,pr) -> errorm ~loc:(loc_of_id (pr_name pr))
| InvalidIndDecl (_,pr) -> errorm ~loc:(loc_of_id pr.pr_name)
"not a clausal form"
| NonPositiveIndDecl (_,pr,s) -> errorm ~loc:(loc_of_id (pr_name pr))
| NonPositiveIndDecl (_,pr,s) -> errorm ~loc:(loc_of_id pr.pr_name)
"non-positive occurrence of %a" Pretty.print_ls s
| TooSpecificIndDecl (_,pr,t) -> errorm ~loc:(loc_of_id (pr_name pr))
| TooSpecificIndDecl (_,pr,t) -> errorm ~loc:(loc_of_id pr.pr_name)
"term @[%a@] is too specific" Pretty.print_term t
(* parse file and store all theories into parsed_theories *)
......@@ -1098,12 +1098,12 @@ and add_decl env lenv th = function
| CSlemma p ->
let pr,_ = find_prop_ns p t.th_export in
if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
then error ~loc (Clash (pr_name pr).id_short);
then error ~loc (Clash pr.pr_name.id_short);
{ s with inst_lemma = Spr.add pr s.inst_lemma }
| CSgoal p ->
let pr,_ = find_prop_ns p t.th_export in
if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
then error ~loc (Clash (pr_name pr).id_short);
then error ~loc (Clash pr.pr_name.id_short);
{ s with inst_goal = Spr.add pr s.inst_goal }
in
let s = List.fold_left add_inst empty_inst s in
......
......@@ -34,7 +34,7 @@ let print_ident fmt id =
fprintf fmt "%s" (id_unique ident_printer id)
let print_tvsymbols fmt id =
fprintf fmt "'%s" (id_unique ident_printer (tv_name id))
fprintf fmt "'%s" (id_unique ident_printer id.tv_name)
let forget_var v = forget_id ident_printer v.vs_name
......@@ -195,13 +195,13 @@ let print_decl drv task fmt d = match d.d_node with
print_list_opt newline (print_logic_decl drv task) fmt dl
| Dind _ -> assert false (* TODO *)
| Dprop (Paxiom, pr, _) when
Driver.query_ident drv (pr_name pr) = Driver.Remove -> false
Driver.query_ident drv pr.pr_name = Driver.Remove -> false
| Dprop (Paxiom, pr, f) ->
fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n"
print_ident (pr_name pr) (print_fmla drv) f; true
print_ident pr.pr_name (print_fmla drv) f; true
| Dprop (Pgoal, pr, f) ->
fprintf fmt "@[<hov 2>goal %a :@ %a@]@\n"
print_ident (pr_name pr) (print_fmla drv) f; true
print_ident pr.pr_name (print_fmla drv) f; true
| Dprop (Plemma, _, _) ->
assert false
......
......@@ -52,9 +52,9 @@ let tv_set = ref Sid.empty
(* type variables always start with a quote *)
let print_tv fmt tv =
tv_set := Sid.add (tv_name tv) !tv_set;
tv_set := Sid.add tv.tv_name !tv_set;
let sanitize n = "'" ^ n in
let n = id_unique iprinter ~sanitizer:sanitize (tv_name tv) in
let n = id_unique iprinter ~sanitizer:sanitize tv.tv_name in
fprintf fmt "%s" n
let forget_tvs () =
......@@ -80,7 +80,7 @@ let print_ls fmt ls =
fprintf fmt "%s" n
let print_pr fmt pr =
fprintf fmt "%s" (id_unique pprinter (pr_name pr))
fprintf fmt "%s" (id_unique pprinter pr.pr_name)
(** Types *)
......@@ -316,7 +316,7 @@ let print_prop_decl drv fmt (k,pr,f) =
print_pr pr (print_fmla drv) f
let print_prop_decl drv fmt (k,pr,f) =
match k, query_ident drv (pr_name pr) with
match k, query_ident drv pr.pr_name with
| Paxiom, Remove -> ()
| _ -> print_prop_decl drv fmt (k,pr,f); forget_tvs ()
......
......@@ -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_name pr))) p]) l
(create_prop (id_clone pr.pr_name)) p]) l
| _ -> [[d]]
let t fsp = Register.store (fun () -> Trans.decl_l (elt fsp) None)
......
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