Commit 292b6f43 authored by Andrei Paskevich's avatar Andrei Paskevich

fuse id_short and id_long into one id_string

parent 60a0f681
...@@ -373,7 +373,7 @@ and tr_global_ts dep env r = ...@@ -373,7 +373,7 @@ and tr_global_ts dep env r =
let (_,vars), env, t = decomp_type_quantifiers env ty in let (_,vars), env, t = decomp_type_quantifiers env ty in
let tvm = let tvm =
let add v1 v2 tvm = let add v1 v2 tvm =
Idmap.add (id_of_string v1.tv_name.Ident.id_short) v2 tvm Idmap.add (id_of_string v1.tv_name.Ident.id_string) v2 tvm
in in
List.fold_right2 add vars ts.Ty.ts_args Idmap.empty List.fold_right2 add vars ts.Ty.ts_args Idmap.empty
in in
......
...@@ -40,7 +40,7 @@ let create_env = ...@@ -40,7 +40,7 @@ let create_env =
env_tag = !r } env_tag = !r }
in in
let th = builtin_theory in let th = builtin_theory in
let m = Mnm.add th.th_name.id_short th Mnm.empty in let m = Mnm.add th.th_name.id_string th Mnm.empty in
Hashtbl.add env.env_memo [] m; Hashtbl.add env.env_memo [] m;
env env
......
...@@ -22,10 +22,9 @@ open Util ...@@ -22,10 +22,9 @@ open Util
(** Identifiers *) (** Identifiers *)
type ident = { type ident = {
id_short : string; (* non-unique name for string-based lookup *) id_string : string; (* non-unique name *)
id_long : string; (* non-unique name for pretty printing *)
id_origin : origin; (* origin of the ident *) id_origin : origin; (* origin of the ident *)
id_tag : int; (* unique numeric tag *) id_tag : int; (* unique numeric tag *)
} }
and origin = and origin =
...@@ -52,23 +51,16 @@ let gentag = let r = ref 0 in fun () -> incr r; !r ...@@ -52,23 +51,16 @@ let gentag = let r = ref 0 in fun () -> incr r; !r
let id_register id = { id with id_tag = gentag () } let id_register id = { id with id_tag = gentag () }
let create_ident short long origin = { let create_ident name origin = {
id_short = short; id_string = name;
id_long = long;
id_origin = origin; id_origin = origin;
id_tag = -1 id_tag = -1
} }
let id_fresh sh = create_ident sh sh Fresh let id_fresh nm = create_ident nm Fresh
let id_fresh_long sh ln = create_ident sh ln Fresh let id_user nm loc = create_ident nm (User loc)
let id_derive nm id = create_ident nm (Derived id)
let id_user sh loc = create_ident sh sh (User loc) let id_clone id = create_ident id.id_string (Derived id)
let id_user_long sh ln loc = create_ident sh ln (User loc)
let id_derive sh id = create_ident sh sh (Derived id)
let id_derive_long sh ln id = create_ident sh ln (Derived id)
let id_clone id = create_ident id.id_short id.id_long (Derived id)
let id_dup id = { id with id_tag = -1 } let id_dup id = { id with id_tag = -1 }
let rec id_derived_from i1 i2 = id_equal i1 i2 || let rec id_derived_from i1 i2 = id_equal i1 i2 ||
...@@ -121,7 +113,7 @@ let id_unique printer ?(sanitizer = same) id = ...@@ -121,7 +113,7 @@ let id_unique printer ?(sanitizer = same) id =
try try
Hashtbl.find printer.values id.id_tag Hashtbl.find printer.values id.id_tag
with Not_found -> with Not_found ->
let name = sanitizer (printer.sanitizer id.id_long) in let name = sanitizer (printer.sanitizer id.id_string) in
let name = find_unique printer.indices name in let name = find_unique printer.indices name in
Hashtbl.replace printer.values id.id_tag name; Hashtbl.replace printer.values id.id_tag name;
name name
......
...@@ -20,10 +20,9 @@ ...@@ -20,10 +20,9 @@
(** Identifiers *) (** Identifiers *)
type ident = private { type ident = private {
id_short : string; (* non-unique name for string-based lookup *) id_string : string; (* non-unique name *)
id_long : string; (* non-unique name for pretty printing *)
id_origin : origin; (* origin of the ident *) id_origin : origin; (* origin of the ident *)
id_tag : int; (* unique numeric tag *) id_tag : int; (* unique numeric tag *)
} }
and origin = and origin =
...@@ -45,15 +44,12 @@ val id_register : preid -> ident ...@@ -45,15 +44,12 @@ val id_register : preid -> ident
(* create a fresh pre-ident *) (* create a fresh pre-ident *)
val id_fresh : string -> preid val id_fresh : string -> preid
val id_fresh_long : string -> string -> preid
(* create a localized pre-ident *) (* create a localized pre-ident *)
val id_user : string -> Loc.position -> preid val id_user : string -> Loc.position -> preid
val id_user_long : string -> string -> Loc.position -> preid
(* create a derived pre-ident *) (* create a derived pre-ident *)
val id_derive : string -> ident -> preid val id_derive : string -> ident -> preid
val id_derive_long : string -> string -> ident -> preid
(* create a derived pre-ident with the same name *) (* create a derived pre-ident with the same name *)
val id_clone : ident -> preid val id_clone : ident -> preid
......
...@@ -330,7 +330,7 @@ let print_inst fmt (id1,id2) = ...@@ -330,7 +330,7 @@ let print_inst fmt (id1,id2) =
let n = id_unique pprinter id1 in let n = id_unique pprinter id1 in
fprintf fmt "prop %s = %a" n print_pr (Hid.find phash id2) fprintf fmt "prop %s = %a" n print_pr (Hid.find phash id2)
else else
fprintf fmt "ident %s = %s" id1.id_long id2.id_long fprintf fmt "ident %s = %s" id1.id_string id2.id_string
let print_decl fmt d = match d.d_node with let print_decl fmt d = match d.d_node with
| Dtype tl -> print_list newline print_type_decl fmt tl | Dtype tl -> print_list newline print_type_decl fmt tl
......
...@@ -115,10 +115,10 @@ let builtin_theory = ...@@ -115,10 +115,10 @@ let builtin_theory =
let kn_equ = known_add_decl kn_real decl_equ in let kn_equ = known_add_decl kn_real decl_equ in
let kn_neq = known_add_decl kn_equ decl_neq in let kn_neq = known_add_decl kn_equ decl_neq in
let ns_int = Mnm.add ts_int.ts_name.id_short ts_int Mnm.empty in let ns_int = Mnm.add ts_int.ts_name.id_string ts_int Mnm.empty in
let ns_real = Mnm.add ts_real.ts_name.id_short ts_real ns_int in let ns_real = Mnm.add ts_real.ts_name.id_string ts_real ns_int in
let ns_equ = Mnm.add ps_equ.ls_name.id_short ps_equ Mnm.empty in let ns_equ = Mnm.add ps_equ.ls_name.id_string ps_equ Mnm.empty in
let ns_neq = Mnm.add ps_neq.ls_name.id_short ps_neq ns_equ in let ns_neq = Mnm.add ps_neq.ls_name.id_string ps_neq ns_equ in
let export = { ns_ts = ns_real; ns_ls = ns_neq; let export = { ns_ts = ns_real; ns_ls = ns_neq;
ns_pr = Mnm.empty; ns_ns = Mnm.empty } in ns_pr = Mnm.empty; ns_ns = Mnm.empty } in
...@@ -215,8 +215,8 @@ let create_theory n = use_export (empty_theory n) builtin_theory ...@@ -215,8 +215,8 @@ let create_theory n = use_export (empty_theory n) builtin_theory
let add_symbol add id v uc = let add_symbol add id v uc =
match uc.uc_import, uc.uc_export with match uc.uc_import, uc.uc_export with
| i0 :: sti, e0 :: ste -> { uc with | i0 :: sti, e0 :: ste -> { uc with
uc_import = add false id.id_short v i0 :: sti; uc_import = add false id.id_string v i0 :: sti;
uc_export = add true id.id_short v e0 :: ste; uc_export = add true id.id_string v e0 :: ste;
uc_local = Sid.add id uc.uc_local } uc_local = Sid.add id uc.uc_local }
| _ -> | _ ->
assert false assert false
......
...@@ -375,7 +375,7 @@ let get_filename drv input_file theory_name goal_name = ...@@ -375,7 +375,7 @@ let get_filename drv input_file theory_name goal_name =
Str.global_substitute filename_regexp replace file Str.global_substitute filename_regexp replace file
let file_of_task drv input_file theory_name task = let file_of_task drv input_file theory_name task =
get_filename drv input_file theory_name (task_goal task).pr_name.id_short get_filename drv input_file theory_name (task_goal task).pr_name.id_string
let call_on_buffer ?debug ~command ?timelimit ?memlimit drv buffer = let call_on_buffer ?debug ~command ?timelimit ?memlimit drv buffer =
let regexps = drv.drv_regexps in let regexps = drv.drv_regexps in
......
...@@ -118,7 +118,7 @@ module Ide_namespace = struct ...@@ -118,7 +118,7 @@ module Ide_namespace = struct
Mnm.iter add_ns ns.ns_ns Mnm.iter add_ns ns.ns_ns
in in
let row = model#append () in let row = model#append () in
model#set ~row ~column (th.th_name.Ident.id_short : string); model#set ~row ~column (th.th_name.Ident.id_string : string);
fill row th.th_export fill row th.th_export
end end
......
...@@ -249,7 +249,7 @@ let rec report fmt = function ...@@ -249,7 +249,7 @@ let rec report fmt = function
| Typing.Error e -> | Typing.Error e ->
Typing.report fmt e Typing.report fmt e
| Decl.UnknownIdent i -> | Decl.UnknownIdent i ->
fprintf fmt "anomaly: unknown ident '%s'" i.Ident.id_short fprintf fmt "anomaly: unknown ident '%s'" i.Ident.id_string
| Driver.Error e -> | Driver.Error e ->
Driver.report fmt e Driver.report fmt e
| Config.Dynlink.Error e -> | Config.Dynlink.Error e ->
...@@ -263,7 +263,7 @@ let rec report fmt = function ...@@ -263,7 +263,7 @@ let rec report fmt = function
| e -> fprintf fmt "anomaly: %s" (Printexc.to_string e) | e -> fprintf fmt "anomaly: %s" (Printexc.to_string e)
let print_th_namespace fmt th = let print_th_namespace fmt th =
Pretty.print_namespace fmt th.th_name.Ident.id_short th.th_export Pretty.print_namespace fmt th.th_name.Ident.id_string th.th_export
let fname_printer = ref (Ident.create_ident_printer []) let fname_printer = ref (Ident.create_ident_printer [])
...@@ -274,7 +274,7 @@ let do_task _env drv fname tname (th : Why.Theory.theory) (task : Task.task) = ...@@ -274,7 +274,7 @@ let do_task _env drv fname tname (th : Why.Theory.theory) (task : Task.task) =
Prover.prove_task ~debug ~command ~timelimit ~memlimit drv task () Prover.prove_task ~debug ~command ~timelimit ~memlimit drv task ()
in in
printf "%s %s %s : %a@." fname tname printf "%s %s %s : %a@." fname tname
(task_goal task).Decl.pr_name.Ident.id_long (task_goal task).Decl.pr_name.Ident.id_string
Call_provers.print_prover_result res Call_provers.print_prover_result res
| None, None -> | None, None ->
Prover.print_task ~debug drv std_formatter task Prover.print_task ~debug drv std_formatter task
...@@ -283,7 +283,7 @@ let do_task _env drv fname tname (th : Why.Theory.theory) (task : Task.task) = ...@@ -283,7 +283,7 @@ let do_task _env drv fname tname (th : Why.Theory.theory) (task : Task.task) =
let fname = let fname =
try Filename.chop_extension fname with _ -> fname try Filename.chop_extension fname with _ -> fname
in in
let tname = th.th_name.Ident.id_short in let tname = th.th_name.Ident.id_string in
let dest = Driver.file_of_task drv fname tname task in let dest = Driver.file_of_task drv fname tname task in
(* Uniquify the filename before the extension if it exists*) (* Uniquify the filename before the extension if it exists*)
let i = try String.rindex dest '.' with _ -> String.length dest in let i = try String.rindex dest '.' with _ -> String.length dest in
......
...@@ -121,7 +121,7 @@ let rec report fmt = function ...@@ -121,7 +121,7 @@ let rec report fmt = function
| Typing.Error e -> | Typing.Error e ->
Typing.report fmt e Typing.report fmt e
| Decl.UnknownIdent i -> | Decl.UnknownIdent i ->
fprintf fmt "anomaly: unknown ident '%s'" i.Ident.id_short fprintf fmt "anomaly: unknown ident '%s'" i.Ident.id_string
| Driver.Error e -> | Driver.Error e ->
Driver.report fmt e Driver.report fmt e
| Config.Dynlink.Error e -> | Config.Dynlink.Error e ->
...@@ -146,7 +146,7 @@ let m : Why.Theory.theory Why.Theory.Mnm.t = ...@@ -146,7 +146,7 @@ let m : Why.Theory.theory Why.Theory.Mnm.t =
(***************************) (***************************)
let add_task (tname : string) (task : Why.Task.task) acc = let add_task (tname : string) (task : Why.Task.task) acc =
let name = (Why.Task.task_goal task).Why.Decl.pr_name.Why.Ident.id_long in let name = (Why.Task.task_goal task).Why.Decl.pr_name.Why.Ident.id_string in
eprintf "doing task: tname=%s, name=%s@." tname name; eprintf "doing task: tname=%s, name=%s@." tname name;
Db.add_or_replace_task ~tname ~name task :: acc Db.add_or_replace_task ~tname ~name task :: acc
...@@ -231,11 +231,11 @@ let main_loop goals = ...@@ -231,11 +231,11 @@ let main_loop goals =
let () = let () =
eprintf "looking for goals@."; eprintf "looking for goals@.";
let add_th t th mi = let add_th t th mi =
eprintf "adding theory %s, %s@." th.Why.Theory.th_name.Why.Ident.id_long t; eprintf "adding theory %s, %s@." th.Why.Theory.th_name.Why.Ident.id_string t;
Why.Ident.Mid.add th.Why.Theory.th_name (t,th) mi Why.Ident.Mid.add th.Why.Theory.th_name (t,th) mi
in in
let do_th _ (t,th) glist = let do_th _ (t,th) glist =
eprintf "doing theory %s, %s@." th.Why.Theory.th_name.Why.Ident.id_long t; eprintf "doing theory %s, %s@." th.Why.Theory.th_name.Why.Ident.id_string t;
do_theory t th glist do_theory t th glist
in in
let goals = let goals =
......
...@@ -58,14 +58,14 @@ let rec print_dty fmt = function ...@@ -58,14 +58,14 @@ let rec print_dty fmt = function
| Tyvar { type_val = Some t } -> | Tyvar { type_val = Some t } ->
print_dty fmt t print_dty fmt t
| Tyvar { type_val = None; tvsymbol = v } -> | Tyvar { type_val = None; tvsymbol = v } ->
fprintf fmt "'%s" v.tv_name.id_short fprintf fmt "'%s" v.tv_name.id_string
| Tyapp (s, []) -> | Tyapp (s, []) ->
fprintf fmt "%s" s.ts_name.id_short fprintf fmt "%s" s.ts_name.id_string
| Tyapp (s, [t]) -> | Tyapp (s, [t]) ->
fprintf fmt "%a %s" print_dty t s.ts_name.id_short fprintf fmt "%a %s" print_dty t s.ts_name.id_string
| Tyapp (s, l) -> | Tyapp (s, l) ->
fprintf fmt "(%a) %s" fprintf fmt "(%a) %s"
(print_list comma print_dty) l s.ts_name.id_short (print_list comma print_dty) l s.ts_name.id_string
let create_ty_decl_var = let create_ty_decl_var =
let t = ref 0 in let t = ref 0 in
......
...@@ -87,7 +87,7 @@ let report fmt = function ...@@ -87,7 +87,7 @@ let report fmt = function
| TermExpected -> | TermExpected ->
fprintf fmt "syntax error: term expected" fprintf fmt "syntax error: term expected"
| BadNumberOfArguments (s, n, m) -> | BadNumberOfArguments (s, n, m) ->
fprintf fmt "@[Symbol `%s' is applied to %d terms,@ " s.id_short n; fprintf fmt "@[Symbol `%s' is applied to %d terms,@ " s.id_string n;
fprintf fmt "but is expecting %d arguments@]" m fprintf fmt "but is expecting %d arguments@]" m
| ClashTheory s -> | ClashTheory s ->
fprintf fmt "clash with previous theory %s" s fprintf fmt "clash with previous theory %s" s
...@@ -709,7 +709,7 @@ let add_types dl th = ...@@ -709,7 +709,7 @@ let add_types dl th =
let vars = th'.utyvars in let vars = th'.utyvars in
List.iter List.iter
(fun v -> (fun v ->
Hashtbl.add vars v.tv_name.id_short Hashtbl.add vars v.tv_name.id_string
(create_ty_decl_var ~user:true v)) (create_ty_decl_var ~user:true v))
ts.ts_args; ts.ts_args;
ts, th' ts, th'
...@@ -733,7 +733,7 @@ let add_types dl th = ...@@ -733,7 +733,7 @@ let add_types dl th =
with ClashSymbol s -> error ~loc:(Hashtbl.find csymbols s) (Clash s) with ClashSymbol s -> error ~loc:(Hashtbl.find csymbols s) (Clash s)
let env_of_vsymbol_list vl = let env_of_vsymbol_list vl =
List.fold_left (fun env v -> Mstr.add v.vs_name.id_short v env) Mstr.empty vl List.fold_left (fun env v -> Mstr.add v.vs_name.id_string v env) Mstr.empty vl
let add_logics dl th = let add_logics dl th =
let fsymbols = Hashtbl.create 17 in let fsymbols = Hashtbl.create 17 in
...@@ -931,30 +931,30 @@ and add_decl env lenv th = function ...@@ -931,30 +931,30 @@ and add_decl env lenv th = function
let ts1 = find_tysymbol_ns p t.th_export in let ts1 = find_tysymbol_ns p t.th_export in
let ts2 = find_tysymbol q th in let ts2 = find_tysymbol q th in
if Mts.mem ts1 s.inst_ts if Mts.mem ts1 s.inst_ts
then error ~loc (Clash ts1.ts_name.id_short); then error ~loc (Clash ts1.ts_name.id_string);
{ s with inst_ts = Mts.add ts1 ts2 s.inst_ts } { s with inst_ts = Mts.add ts1 ts2 s.inst_ts }
| CSlsym (p,q) -> | CSlsym (p,q) ->
let ls1 = find_lsymbol_ns p t.th_export in let ls1 = find_lsymbol_ns p t.th_export in
let ls2 = find_lsymbol q th in let ls2 = find_lsymbol q th in
if Mls.mem ls1 s.inst_ls if Mls.mem ls1 s.inst_ls
then error ~loc (Clash ls1.ls_name.id_short); then error ~loc (Clash ls1.ls_name.id_string);
{ s with inst_ls = Mls.add ls1 ls2 s.inst_ls } { s with inst_ls = Mls.add ls1 ls2 s.inst_ls }
| CSlemma p -> | CSlemma p ->
let pr,_ = find_prop_ns p t.th_export in let pr,_ = find_prop_ns p t.th_export in
if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
then error ~loc (Clash pr.pr_name.id_short); then error ~loc (Clash pr.pr_name.id_string);
{ s with inst_lemma = Spr.add pr s.inst_lemma } { s with inst_lemma = Spr.add pr s.inst_lemma }
| CSgoal p -> | CSgoal p ->
let pr,_ = find_prop_ns p t.th_export in let pr,_ = find_prop_ns p t.th_export in
if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
then error ~loc (Clash pr.pr_name.id_short); then error ~loc (Clash pr.pr_name.id_string);
{ s with inst_goal = Spr.add pr s.inst_goal } { s with inst_goal = Spr.add pr s.inst_goal }
in in
let s = List.fold_left add_inst empty_inst s in let s = List.fold_left add_inst empty_inst s in
clone_export th t s clone_export th t s
in in
let n = match use.use_as with let n = match use.use_as with
| None -> Some t.th_name.id_short | None -> Some t.th_name.id_string
| Some (Some x) -> Some x.id | Some (Some x) -> Some x.id
| Some None -> None | Some None -> None
in in
...@@ -982,7 +982,7 @@ and add_decl env lenv th = function ...@@ -982,7 +982,7 @@ and add_decl env lenv th = function
and type_and_add_theory env lenv pt = and type_and_add_theory env lenv pt =
let id = pt.pt_name in let id = pt.pt_name in
if Mnm.mem id.id lenv || id.id = builtin_theory.th_name.id_short if Mnm.mem id.id lenv || id.id = builtin_theory.th_name.id_string
then error (ClashTheory id.id); then error (ClashTheory id.id);
let th = type_theory env lenv id pt in let th = type_theory env lenv id pt in
Mnm.add id.id th lenv Mnm.add id.id th lenv
......
...@@ -483,7 +483,7 @@ let add_decl uc ls = ...@@ -483,7 +483,7 @@ let add_decl uc ls =
| User loc -> Some loc | User loc -> Some loc
| _ -> None (* FIXME: loc for recursive functions *) | _ -> None (* FIXME: loc for recursive functions *)
in in
errorm ?loc "clash with previous symbol %s" ls.ls_name.id_short errorm ?loc "clash with previous symbol %s" ls.ls_name.id_string
let file env uc dl = let file env uc dl =
let uc, dl = let uc, dl =
...@@ -503,7 +503,7 @@ let file env uc dl = ...@@ -503,7 +503,7 @@ let file env uc dl =
let _, dl = letrec uc Mstr.empty dl in let _, dl = letrec uc Mstr.empty dl in
let one uc (v,_,_,_ as r) = let one uc (v,_,_,_ as r) =
let tyl, ty = uncurrying uc v.vs_ty in let tyl, ty = uncurrying uc v.vs_ty in
let id = id_fresh v.vs_name.id_short in let id = id_fresh v.vs_name.id_string in
let ls = create_lsymbol id tyl (Some ty) in let ls = create_lsymbol id tyl (Some ty) in
add_decl uc ls, (ls, r) add_decl uc ls, (ls, r)
in in
......
...@@ -158,7 +158,7 @@ let add_type (state, task) ts csl = ...@@ -158,7 +158,7 @@ let add_type (state, task) ts csl =
let cs_add tsk cs = add_decl tsk (create_logic_decl [cs, None]) in let cs_add tsk cs = add_decl tsk (create_logic_decl [cs, None]) in
let task = List.fold_left cs_add task csl in let task = List.fold_left cs_add task csl in
(* declare the selector function *) (* declare the selector function *)
let mt_id = id_derive ("match_" ^ ts.ts_name.id_long) ts.ts_name in let mt_id = id_derive ("match_" ^ ts.ts_name.id_string) ts.ts_name in
let mt_hd = ty_app ts (List.map ty_var ts.ts_args) in let mt_hd = ty_app ts (List.map ty_var ts.ts_args) in
let mt_ty = ty_var (create_tvsymbol (id_fresh "a")) in let mt_ty = ty_var (create_tvsymbol (id_fresh "a")) in
let mt_al = mt_hd :: List.rev_map (fun _ -> mt_ty) csl in let mt_al = mt_hd :: List.rev_map (fun _ -> mt_ty) csl in
...@@ -170,7 +170,7 @@ let add_type (state, task) ts csl = ...@@ -170,7 +170,7 @@ let add_type (state, task) ts csl =
let mt_vl = List.rev_map mt_vs csl in let mt_vl = List.rev_map mt_vs csl in
let mt_tl = List.rev_map t_var mt_vl in let mt_tl = List.rev_map t_var mt_vl in
let mt_add tsk cs t = let mt_add tsk cs t =
let id = mt_ls.ls_name.id_long ^ "_" ^ cs.ls_name.id_long in let id = mt_ls.ls_name.id_string ^ "_" ^ cs.ls_name.id_string in
let pr = create_prsymbol (id_derive id cs.ls_name) in let pr = create_prsymbol (id_derive id cs.ls_name) in
let vl = List.rev_map (create_vsymbol (id_fresh "u")) cs.ls_args in let vl = List.rev_map (create_vsymbol (id_fresh "u")) cs.ls_args in
let hd = t_app cs (List.rev_map t_var vl) (of_option cs.ls_value) in let hd = t_app cs (List.rev_map t_var vl) (of_option cs.ls_value) in
...@@ -182,7 +182,7 @@ let add_type (state, task) ts csl = ...@@ -182,7 +182,7 @@ let add_type (state, task) ts csl =
let task = List.fold_left2 mt_add task csl mt_tl in let task = List.fold_left2 mt_add task csl mt_tl in
(* declare and define the projection functions *) (* declare and define the projection functions *)
let pj_add (m,tsk) cs = let pj_add (m,tsk) cs =
let id = cs.ls_name.id_long ^ "_proj_" in let id = cs.ls_name.id_string ^ "_proj_" in
let vl = List.rev_map (create_vsymbol (id_fresh "u")) cs.ls_args in let vl = List.rev_map (create_vsymbol (id_fresh "u")) cs.ls_args in
let tl = List.rev_map t_var vl in let tl = List.rev_map t_var vl in
let hd = t_app cs tl (of_option cs.ls_value) in let hd = t_app cs tl (of_option cs.ls_value) in
...@@ -191,7 +191,7 @@ let add_type (state, task) ts csl = ...@@ -191,7 +191,7 @@ let add_type (state, task) ts csl =
let id = id_derive (id ^ (incr c; string_of_int !c)) cs.ls_name in let id = id_derive (id ^ (incr c; string_of_int !c)) cs.ls_name in
let ls = create_fsymbol id [of_option cs.ls_value] t.t_ty in let ls = create_fsymbol id [of_option cs.ls_value] t.t_ty in
let tsk = add_decl tsk (create_logic_decl [ls, None]) in let tsk = add_decl tsk (create_logic_decl [ls, None]) in
let id = id_derive (ls.ls_name.id_long ^ "_def") ls.ls_name in let id = id_derive (ls.ls_name.id_string ^ "_def") ls.ls_name in
let pr = create_prsymbol id in let pr = create_prsymbol id in
let hh = t_app ls [hd] t.t_ty in let hh = t_app ls [hd] t.t_ty in
let ax = f_forall (List.rev vl) [[Term hd]] (f_equ hh t) in let ax = f_forall (List.rev vl) [[Term hd]] (f_equ hh t) in
...@@ -202,7 +202,7 @@ let add_type (state, task) ts csl = ...@@ -202,7 +202,7 @@ let add_type (state, task) ts csl =
in in
let pjmap, task = List.fold_left pj_add (state.pj_map, task) csl in let pjmap, task = List.fold_left pj_add (state.pj_map, task) csl in
(* add the inversion axiom *) (* add the inversion axiom *)
let ax_id = ts.ts_name.id_long ^ "_inversion" in let ax_id = ts.ts_name.id_string ^ "_inversion" in
let ax_pr = create_prsymbol (id_derive ax_id ts.ts_name) in let ax_pr = create_prsymbol (id_derive ax_id ts.ts_name) in
let ax_vs = create_vsymbol (id_fresh "u") mt_hd in let ax_vs = create_vsymbol (id_fresh "u") mt_hd in
let ax_hd = t_var ax_vs in let ax_hd = t_var ax_vs in
......
...@@ -74,13 +74,13 @@ let add_ld func pred axl d = match d with ...@@ -74,13 +74,13 @@ let add_ld func pred axl d = match d with
| ls, Some ld -> | ls, Some ld ->
let vl,e = open_ls_defn ld in begin match e with let vl,e = open_ls_defn ld in begin match e with
| Term t when func -> | Term t when func ->
let nm = ls.ls_name.id_short ^ "_def" in let nm = ls.ls_name.id_string ^ "_def" in
let hd = t_app ls (List.map t_var vl) t.t_ty in let hd = t_app ls (List.map t_var vl) t.t_ty in
let ax = f_forall vl [[Term hd]] (t_insert hd t) in let ax = f_forall vl [[Term hd]] (t_insert hd t) in
let pr = create_prsymbol (id_derive nm ls.ls_name) in let pr = create_prsymbol (id_derive nm ls.ls_name) in
create_prop_decl Paxiom pr ax :: axl, (ls, None) create_prop_decl Paxiom pr ax :: axl, (ls, None)
| Fmla f when pred -> | Fmla f when pred ->
let nm = ls.ls_name.id_short ^ "_def" in let nm = ls.ls_name.id_string ^ "_def" in
let hd = f_app ls (List.map t_var vl) in let hd = f_app ls (List.map t_var vl) in
let ax = f_forall vl [[Fmla hd]] (f_insert hd f) in let ax = f_forall vl [[Fmla hd]] (f_insert hd f) in
let pr = create_prsymbol (id_derive nm ls.ls_name) in let pr = create_prsymbol (id_derive nm ls.ls_name) in
......
...@@ -69,7 +69,7 @@ let add_ld axl d = match d with ...@@ -69,7 +69,7 @@ let add_ld axl d = match d with
let vl,e = open_ls_defn ld in let vl,e = open_ls_defn ld in
begin match e with begin match e with
| Term t when has_if t -> | Term t when has_if t ->
let nm = ls.ls_name.id_short ^ "_def" in let nm = ls.ls_name.id_string ^ "_def" in
let pr = create_prsymbol (id_derive nm ls.ls_name) in let pr = create_prsymbol (id_derive nm ls.ls_name) in
let hd = t_app ls (List.map t_var vl) t.t_ty in let hd = t_app ls (List.map t_var vl) t.t_ty in
let f = f_forall vl [[Term hd]] (elim_f (f_equ hd t)) in let f = f_forall vl [[Term hd]] (elim_f (f_equ hd t)) in
......
...@@ -46,7 +46,7 @@ let inv acc (ps,al) = ...@@ -46,7 +46,7 @@ let inv acc (ps,al) =
let hd = f_app ps tl in let hd = f_app ps tl in
let dj = Util.map_join_left (exi tl) f_or al in let dj = Util.map_join_left (exi tl) f_or al in
let ax = f_forall vl [[Fmla hd]] (f_implies hd dj) in let ax = f_forall vl [[Fmla hd]] (f_implies hd dj) in
let nm = id_derive (ps.ls_name.id_long ^ "_inversion") ps.ls_name in let nm = id_derive (ps.ls_name.id_string ^ "_inversion") ps.ls_name in
create_prop_decl Paxiom (create_prsymbol nm) ax :: acc create_prop_decl Paxiom (create_prsymbol nm) ax :: acc
let elim d = match d.d_node with let elim d = match d.d_node with
......
...@@ -41,7 +41,7 @@ struct ...@@ -41,7 +41,7 @@ struct
(* let spec_conv ts = (* let spec_conv ts =
let name = ts.ts_name.id_short in let name = ts.ts_name.id_string in
let d2ty = create_fsymbol (id_fresh ("d2"^name)) [deco] (ty_app ts []) in let d2ty = create_fsymbol (id_fresh ("d2"^name)) [deco] (ty_app ts []) in
let ty2u = create_fsymbol (id_fresh (name^"2u")) [(ty_app ts [])] undeco in let ty2u = create_fsymbol (id_fresh (name^"2u")) [(ty_app ts [])] undeco in
let axiom = let axiom =
...@@ -85,7 +85,7 @@ let load_prelude query env = ...@@ -85,7 +85,7 @@ let load_prelude query env =
let logic_tty = Theory.ns_find_ls builtin.th_export ["tty"] in let logic_tty = Theory.ns_find_ls builtin.th_export ["tty"] in
let clone_builtin ts = let clone_builtin ts =
let task = None in let task = None in
let name = ts.ts_name.id_short in let name = ts.ts_name.id_string in
let th_uc = create_theory (id_fresh ("encoding_decorate_for_"^name)) in let th_uc = create_theory (id_fresh ("encoding_decorate_for_"^name)) in
let th_uc = Theory.use_export th_uc prelude in let th_uc = Theory.use_export th_uc prelude in
let th_uc = let th_uc =
...@@ -140,7 +140,7 @@ let rec term_of_ty tenv tvar ty = ...@@ -140,7 +140,7 @@ let rec term_of_ty tenv tvar ty =
| Tyvar tv -> | Tyvar tv ->
t_var (try Htv.find tvar tv t_var (try Htv.find tvar tv
with Not_found -> with Not_found ->
(let var = create_vsymbol (id_fresh ("tv"^tv.tv_name.id_short)) (let var = create_vsymbol (id_fresh ("tv"^tv.tv_name.id_string))
tenv.ty in tenv.ty in
Htv.add tvar tv var; Htv.add tvar tv var;
var)) var))
...