Skip to content

why3
why3
Commit 18a0e0b0 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

reworking tags and transformations, stage 1: 

- introduce a new Theory.tdecl "Meta" to be used for tags
- simplify cloning procedure, get rid of the th_clone field
- when a goal proposition is discarded during cloning, 
  it's still keeped in the theory as a "skip proposition",
  this is needed to preserve/clone every local identifier.
  Skip propositions are eliminated during task formation.
- get rid of a separate Task.tdecl type
- reorganize the Task.task_hd record:
  * use/clone history is cached in a theory-keyed map;
  * meta-properties are cached in a tagname-keyed map.
  This is done to simplify the fine-grained configuration
  of transformations.
parent f288825a
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 718 additions and 546 deletions
src/core/decl.ml
View file @ 18a0e0b0
......@@ -90,18 +90,15 @@ let pr_equal pr1 pr2 = id_equal pr1.pr_name pr2.pr_name
let create_prsymbol n = { pr_name = id_register n }
type prop = prsymbol * fmla
let prop_equal (pr1,f1) (pr2,f2) = pr_equal pr1 pr2 && f_equal f1 f2
type ind_decl = lsymbol * prop list
type ind_decl = lsymbol * (prsymbol * fmla) list
(** Proposition declaration *)
type prop_kind =
| Paxiom
| Plemma
| Pgoal
| Plemma (* prove, use as a premise *)
| Paxiom (* do not prove, use as a premise *)
| Pgoal (* prove, do not use as a premise *)
| Pskip (* do not prove, do not use as a premise *)
type prop_decl = prop_kind * prsymbol * fmla
......@@ -164,14 +161,12 @@ module Hsdecl = Hashcons.Make (struct
let hs_ind (ps,al) = Hashcons.combine_list hs_prop ps.ls_name.id_tag al
let hs_kind = function
| Paxiom -> 7
| Plemma -> 11
| Pgoal -> 13
| Plemma -> 11 | Paxiom -> 13 | Pgoal -> 17 | Pskip -> 19
let hash d = match d.d_node with
| 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
| Dtype l -> Hashcons.combine_list hs_td 3 l
| Dlogic l -> Hashcons.combine_list hs_ld 5 l
| Dind l -> Hashcons.combine_list hs_ind 7 l
| Dprop (k,pr,f) -> Hashcons.combine (hs_kind k) (hs_prop (pr,f))
let tag n d = { d with d_tag = n }
......@@ -191,18 +186,13 @@ let d_equal = (==)
(** Declaration constructors *)
let mk_decl node syms news = {
let mk_decl node syms news = Hsdecl.hashcons {
d_node = node;
d_syms = syms;
d_news = news;
d_tag = -1;
}
let create_ty_decl tdl s n = Hsdecl.hashcons (mk_decl (Dtype tdl) s n)
let create_logic_decl ldl s n = Hsdecl.hashcons (mk_decl (Dlogic ldl) s n)
let create_ind_decl idl s n = Hsdecl.hashcons (mk_decl (Dind idl) s n)
let create_prop_decl k p f s n = Hsdecl.hashcons (mk_decl (Dprop (k,p,f)) s n)
exception IllegalTypeAlias of tysymbol
exception ClashIdent of ident
exception BadLogicDecl of ident * ident
......@@ -252,7 +242,7 @@ let create_ty_decl tdl =
List.fold_left (check_constr ty) (syms,news) cl
in
let (syms,news) = List.fold_left check_decl (Sid.empty,Sid.empty) tdl in
create_ty_decl tdl syms news
mk_decl (Dtype tdl) syms news
let create_logic_decl ldl =
if ldl = [] then raise EmptyDecl;
......@@ -267,7 +257,7 @@ let create_logic_decl ldl =
syms, news_id news ls.ls_name
in
let (syms,news) = List.fold_left check_decl (Sid.empty,Sid.empty) ldl in
create_logic_decl ldl syms news
mk_decl (Dlogic ldl) syms news
exception InvalidIndDecl of lsymbol * prsymbol
exception TooSpecificIndDecl of lsymbol * prsymbol * term
......@@ -320,12 +310,12 @@ let create_ind_decl idl =
List.fold_left (check_ax ps) (syms,news) al
in
let (syms,news) = List.fold_left check_decl (Sid.empty,Sid.empty) idl in
create_ind_decl idl syms news
mk_decl (Dind idl) syms news
let create_prop_decl k p f =
let syms = syms_fmla Sid.empty f in
let news = news_id Sid.empty p.pr_name in
create_prop_decl k p (check_fvs f) syms news
mk_decl (Dprop (k,p,check_fvs f)) syms news
(** Split declarations *)
......@@ -460,14 +450,14 @@ let merge_known kn1 kn2 =
in
Mid.fold add_known kn1 kn2
let known_add_decl kn decl =
let known_add_decl kn0 decl =
let add_known id kn =
try
if not (d_equal (Mid.find id kn) decl) then raise (RedeclaredIdent id);
if not (d_equal (Mid.find id kn0) decl) then raise (RedeclaredIdent id);
raise (KnownIdent id)
with Not_found -> Mid.add id decl kn
in
let kn = Sid.fold add_known decl.d_news kn in
let kn = Sid.fold add_known decl.d_news kn0 in
let check_known id =
if not (Mid.mem id kn) then raise (UnknownIdent id)
in
......
src/core/decl.mli
View file @ 18a0e0b0
......@@ -59,20 +59,17 @@ module Hpr : Hashtbl.S with type key = prsymbol
val create_prsymbol : preid -> prsymbol
type prop = prsymbol * fmla
type ind_decl = lsymbol * prop list
val pr_equal : prsymbol -> prsymbol -> bool
val prop_equal : prop -> prop -> bool
type ind_decl = lsymbol * (prsymbol * fmla) list
(* Proposition declaration *)
type prop_kind =
| Paxiom
| Plemma
| Pgoal
| Plemma (* prove, use as a premise *)
| Paxiom (* do not prove, use as a premise *)
| Pgoal (* prove, do not use as a premise *)
| Pskip (* do not prove, do not use as a premise *)
type prop_decl = prop_kind * prsymbol * fmla
......@@ -135,6 +132,7 @@ val decl_fold : ('a -> term -> 'a) -> ('a -> fmla -> 'a) -> 'a -> decl -> 'a
type known_map = decl Mid.t
val known_id : known_map -> ident -> unit
val known_add_decl : known_map -> decl -> known_map
val merge_known : known_map -> known_map -> known_map
......@@ -144,6 +142,6 @@ exception RedeclaredIdent of ident
exception NonExhaustiveExpr of (pattern list * expr)
val find_constructors : known_map -> tysymbol -> lsymbol list
val find_inductive_cases : known_map -> lsymbol -> prop list
val find_inductive_cases : known_map -> lsymbol -> (prsymbol * fmla) list
val find_prop : known_map -> prsymbol -> fmla
src/core/pretty.ml
View file @ 18a0e0b0
......@@ -313,12 +313,19 @@ let print_pkind fmt = function
| Paxiom -> fprintf fmt "axiom"
| Plemma -> fprintf fmt "lemma"
| Pgoal -> fprintf fmt "goal"
| Pskip -> fprintf fmt "skip"
let print_prop_decl fmt (k,pr,f) =
fprintf fmt "@[<hov 2>%a %a : %a@]" print_pkind k
print_pr pr print_fmla f;
forget_tvs ()
let print_decl fmt d = match d.d_node with
| Dtype tl -> print_list newline print_type_decl fmt tl
| Dlogic ll -> print_list newline print_logic_decl fmt ll
| Dind il -> print_list newline print_ind_decl fmt il
| Dprop p -> print_prop_decl fmt p
let print_inst fmt (id1,id2) =
if Hid.mem thash id2 then
let n = id_unique tprinter id1 in
......@@ -332,20 +339,42 @@ let print_inst fmt (id1,id2) =
else
fprintf fmt "ident %s = %s" id1.id_string id2.id_string
let print_decl fmt d = match d.d_node with
| Dtype tl -> print_list newline print_type_decl fmt tl
| Dlogic ll -> print_list newline print_logic_decl fmt ll
| Dind il -> print_list newline print_ind_decl fmt il
| Dprop p -> print_prop_decl fmt p
let print_task_tdecl fmt = function
| Task.Decl d ->
let print_meta_arg_type fmt = function
| MTtysymbol -> fprintf fmt "type_symbol"
| MTlsymbol -> fprintf fmt "logic_symbol"
| MTprsymbol -> fprintf fmt "proposition"
| MTstring -> fprintf fmt "string"
| MTint -> fprintf fmt "int"
let print_meta_arg fmt = function
| MARid id ->
if Hid.mem thash id then
fprintf fmt "type %a" print_ts (Hid.find thash id)
else if Hid.mem lhash id then
fprintf fmt "logic %a" print_ls (Hid.find lhash id)
else if Hid.mem phash id then
fprintf fmt "prop %a" print_pr (Hid.find phash id)
else
fprintf fmt "ident %s" id.id_string
| MARstr s -> fprintf fmt "\"%s\"" s
| MARint i -> fprintf fmt "%d" i
let print_tdecl fmt td = match td.td_node with
| Decl d ->
print_decl fmt d
| Task.Use th ->
| Use th ->
fprintf fmt "@[<hov 2>(* use %a *)@]" print_th th
| Task.Clone (th,inst) ->
| Clone (th,inst) ->
let inst = Mid.fold (fun x y a -> (x,y)::a) inst [] in
fprintf fmt "@[<hov 2>(* clone %a with %a *)@]"
print_th th (print_list comma print_inst) inst
| Meta (t,al) ->
fprintf fmt "@[<hov 2>(* meta %s %a *)@]"
t (print_list space print_meta_arg) al
let print_theory fmt th =
fprintf fmt "@[<hov 2>theory %a@\n%a@]@\nend@."
print_th th (print_list newline2 print_tdecl) th.th_decls
let print_task fmt task =
fprintf fmt "@[<hov>%a@]@."
......@@ -353,20 +382,7 @@ let print_task fmt task =
let print_named_task fmt name task =
fprintf fmt "@[<hov 2>task %s@\n%a@]@\nend@."
name (print_list newline2 print_task_tdecl) (task_tdecls task)
let print_theory_tdecl fmt = function
| Theory.Decl d ->
print_decl fmt d
| Theory.Use th ->
fprintf fmt "@[<hov 2>(* use %a *)@]" print_th th
| Theory.Clone (th,inst) ->
fprintf fmt "@[<hov 2>(* clone %a with %a *)@]"
print_th th (print_list comma print_inst) inst
let print_theory fmt th =
fprintf fmt "@[<hov 2>theory %a@\n%a@]@\nend@."
print_th th (print_list newline2 print_theory_tdecl) th.th_decls
name (print_list newline2 print_tdecl) (task_tdecls task)
module NsTree = struct
type t =
......
src/core/pretty.mli
View file @ 18a0e0b0
......@@ -47,15 +47,15 @@ val print_fmla : formatter -> fmla -> unit (* formula *)
val print_expr : formatter -> expr -> unit (* term or formula *)
val print_pkind : formatter -> prop_kind -> unit
val print_meta_arg : formatter -> meta_arg_real -> unit
val print_meta_arg_type : formatter -> meta_arg_type -> unit
val print_type_decl : formatter -> ty_decl -> unit
val print_logic_decl : formatter -> logic_decl -> unit
val print_ind_decl : formatter -> ind_decl -> unit
val print_prop_decl : formatter -> prop_decl -> unit
val print_decl : formatter -> decl -> unit
val print_task_tdecl : formatter -> Task.tdecl -> unit
val print_theory_tdecl : formatter -> Theory.tdecl -> unit
val print_tdecl : formatter -> tdecl -> unit
val print_task : formatter -> task -> unit
val print_theory : formatter -> theory -> unit
......
src/core/task.ml
View file @ 18a0e0b0
......@@ -26,6 +26,9 @@ open Theory
(** Task *)
type clone_map = Stdecl.t Mid.t
type meta_map = Stdecl.t Mstr.t
type task = task_hd option
and task_hd = {
......@@ -33,19 +36,10 @@ and task_hd = {
task_prev : task; (* context *)
task_known : known_map; (* known identifiers *)
task_clone : clone_map; (* cloning history *)
task_used : use_map; (* referenced theories *)
task_meta : meta_map; (* meta properties *)
task_tag : int; (* unique task tag *)
}
and tdecl =
| Decl of decl
| Use of theory
| Clone of theory * (ident * ident) list
let task_known = option_apply Mid.empty (fun t -> t.task_known)
let task_clone = option_apply Mid.empty (fun t -> t.task_clone)
let task_used = option_apply Mid.empty (fun t -> t.task_used)
let task_hd_equal = (==)
let task_equal t1 t2 = match t1, t2 with
......@@ -53,77 +47,81 @@ let task_equal t1 t2 = match t1, t2 with
| None, None -> true
| _ -> false
module Task = struct
module Hstask = Hashcons.Make (struct
type t = task_hd
let equal_pair (il1,ir1) (il2,ir2) =
id_equal il1 il2 && id_equal ir1 ir2
let equal_tdecl td1 td2 = match td1,td2 with
| Decl d1, Decl d2 -> d_equal d1 d2
| Use th1, Use th2 -> id_equal th1.th_name th2.th_name
| Clone (th1,sl1), Clone (th2,sl2) ->
id_equal th1.th_name th2.th_name && list_all2 equal_pair sl1 sl2
| _,_ -> false
let equal a b = equal_tdecl a.task_decl b.task_decl &&
task_equal a.task_prev b.task_prev
let hash_pair (il,ir) = Hashcons.combine il.id_tag ir.id_tag
let hash_tdecl = function
| Decl d -> Hashcons.combine 3 d.d_tag
| Use th -> Hashcons.combine 5 th.th_name.id_tag
| Clone (th,i) ->
Hashcons.combine_list hash_pair th.th_name.id_tag i
let equal t1 t2 = td_equal t1.task_decl t2.task_decl &&
task_equal t1.task_prev t2.task_prev
let hash task =
let decl = hash_tdecl task.task_decl in
let prev = match task.task_prev with
| Some task -> 1 + task.task_tag
| None -> 0
in
let decl = task.task_decl.td_tag in
let prev = option_apply 0 (fun t -> t.task_tag + 1) task.task_prev in
Hashcons.combine decl prev
let tag i task = { task with task_tag = i }
end
module Htask = Hashcons.Make(Task)
end)
let mk_task decl prev known clone used = Some (Htask.hashcons {
let mk_task decl prev known clone meta = Some (Hstask.hashcons {
task_decl = decl;
task_prev = prev;
task_known = known;
task_clone = clone;
task_used = used;
task_meta = meta;
task_tag = -1;
})
let task_known = option_apply Mid.empty (fun t -> t.task_known)
let task_clone = option_apply Mid.empty (fun t -> t.task_clone)
let task_meta = option_apply Mstr.empty (fun t -> t.task_meta)
let find_clone task th =
try Mid.find th.th_name (task_clone task) with Not_found -> Stdecl.empty
let find_meta task t =
try Mstr.find t (task_meta task) with Not_found -> Stdecl.empty
let add_decl task d td =
let kn = known_add_decl (task_known task) d in
mk_task td task kn (task_clone task) (task_meta task)
let add_clone task th td =
let st = Stdecl.add td (find_clone task th) in
let cl = Mid.add th.th_name st (task_clone task) in
mk_task td task (task_known task) cl (task_meta task)
let add_meta task t td =
let st = Stdecl.add td (find_meta task t) in
let mt = Mstr.add t st (task_meta task) in
mk_task td task (task_known task) (task_clone task) mt
(* add_decl with checks *)
exception LemmaFound
exception SkipFound
exception GoalFound
exception GoalNotFound
let add_tdecl task td =
let kn,cl,us = match task with
| Some {task_decl=Decl{d_node=Dprop(Pgoal,_,_)}} -> raise GoalFound
| Some task -> task.task_known, task.task_clone, task.task_used
| None -> Mid.empty, Mid.empty, Mid.empty
in
match td with
| Decl { d_node = Dprop (Plemma,_,_) } -> raise LemmaFound
| Decl d ->
begin try mk_task td task (known_add_decl kn d) cl us
with KnownIdent _ -> task end
| Use th ->
if Mid.mem th.th_name us then task else
mk_task td task kn cl (merge_used us th)
| Clone (th,sl) ->
mk_task td task kn (merge_clone cl th sl) us
let add_decl task d = add_tdecl task (Decl d)
let create_decl d = Decl d
let rec task_goal = function
| Some task ->
begin match task.task_decl.td_node with
| Decl { d_node = Dprop (Pgoal,pr,_) } -> pr
| Decl _ -> raise GoalNotFound
| _ -> task_goal task.task_prev
end
| None -> raise GoalNotFound
let new_decl task d td = match d.d_node with
| Dprop (Plemma,_,_) -> raise LemmaFound
| Dprop (Pskip,_,_) -> raise SkipFound
| _ ->
try ignore (task_goal task); raise GoalFound
with GoalNotFound -> try add_decl task d td
with KnownIdent _ -> task
(* declaration constructors + add_decl *)
let add_decl task d = new_decl task d (create_decl d)
let add_ty_decl tk dl = add_decl tk (create_ty_decl dl)
let add_logic_decl tk dl = add_decl tk (create_logic_decl dl)
let add_ind_decl tk dl = add_decl tk (create_ind_decl dl)
......@@ -133,38 +131,38 @@ let add_ty_decls tk dl = List.fold_left add_decl tk (create_ty_decls dl)
let add_logic_decls tk dl = List.fold_left add_decl tk (create_logic_decls dl)
let add_ind_decls tk dl = List.fold_left add_decl tk (create_ind_decls dl)
(* use, clone and split_theory *)
(* task constructors *)
let rec add_tdecl task td = match td.td_node with
| Decl d -> new_decl task d td
| Use th -> use_export task th
| Clone (th,_) -> add_clone task th td
| Meta (t,_) -> add_meta task t td
let rec use_export task th = match task with
| Some task_hd when Mid.mem th.th_name task_hd.task_used -> task
| _ -> add_tdecl (List.fold_left flat_tdecl task th.th_decls) (Use th)
and flat_tdecl task td = match td.td_node with
| Decl { d_node = Dprop (Plemma,pr,f) } -> add_prop_decl task Paxiom pr f
| Decl { d_node = Dprop ((Pgoal|Pskip),_,_) } -> task
| _ -> add_tdecl task td
and flat_tdecl task = function
| Theory.Decl { d_node = Dprop (Pgoal,_,_) } ->
task
| Theory.Decl { d_node = Dprop (Plemma,pr,f) } ->
add_prop_decl task Paxiom pr f
| Theory.Decl d -> add_tdecl task (Decl d)
| Theory.Clone (th,sl) -> add_tdecl task (Clone (th,sl))
| Theory.Use th -> use_export task th
and use_export task th =
let td = create_null_clone th in
if Stdecl.mem td (find_clone task th) then task else
let task = List.fold_left flat_tdecl task th.th_decls in
add_clone task th td
let clone_export = clone_theory flat_tdecl
let split_tdecl names (res,task) = function
| Theory.Decl { d_node = Dprop (Pgoal,pr,f) }
when option_apply true (Spr.mem pr) names ->
add_prop_decl task Pgoal pr f :: res, task
| Theory.Decl { d_node = Dprop (Pgoal,_,_) } ->
res, task
| Theory.Decl { d_node = Dprop (Plemma,pr,f) }
let add_meta task t al = add_meta task t (create_meta t al)
(* split theory *)
let split_tdecl names (res,task) td = match td.td_node with
| Decl { d_node = Dprop ((Pgoal|Plemma),pr,f) }
when option_apply true (Spr.mem pr) names ->
add_prop_decl task Pgoal pr f :: res,
add_prop_decl task Paxiom pr f
| Theory.Decl { d_node = Dprop (Plemma,pr,f) } ->
res, add_prop_decl task Paxiom pr f
| Theory.Decl d -> res, add_tdecl task (Decl d)
| Theory.Clone (th,sl) -> res, add_tdecl task (Clone (th,sl))
| Theory.Use th -> res, use_export task th
let res = add_prop_decl task Pgoal pr f :: res in
res, flat_tdecl task td
| _ ->
res, flat_tdecl task td
let split_theory th names =
fst (List.fold_left (split_tdecl names) ([],None) th.th_decls)
......@@ -179,32 +177,43 @@ let rec task_iter fn = function
| Some task -> fn task.task_decl; task_iter fn task.task_prev
| None -> ()
let task_tdecls = task_fold (fun acc d -> d::acc) []
let task_tdecls = task_fold (fun acc td -> td::acc) []
let task_decls = task_fold (fun acc td ->
match td.td_node with Decl d -> d::acc | _ -> acc) []
(* TO BE REMOVED *)
let old_task_clone task =
Mid.fold (fun _ -> Stdecl.fold (function
| { td_node = Clone (_,cl) } ->
Mid.fold (fun id id' m ->
let s = try Mid.find id' m with Not_found -> Sid.empty in
Mid.add id' (Sid.add id s) m) cl
| _ -> assert false)) (task_clone task) Mid.empty
let task_decls =
task_fold (fun acc -> function Decl d -> d::acc | _ -> acc) []
let old_task_use task =
Mid.fold (fun _ -> Stdecl.fold (function
| { td_node = Clone (th,cl) } -> (fun m ->
if Mid.is_empty cl then Mid.add th.th_name th m else m)
| _ -> assert false)) (task_clone task) Mid.empty
let rec last_use task = match task with
| Some { task_decl = Use _ } -> task
| Some { task_prev = task } -> last_use task
| Some {task_decl={td_node=Clone(_,cl)}} when Mid.is_empty cl -> task
| Some {task_prev=task} -> last_use task
| None -> None
let rec last_clone task = match task with
| Some { task_decl = Clone _ } -> task
| Some { task_prev = task } -> last_clone task
| Some {task_decl={td_node=Clone _}} -> task
| Some {task_prev=task} -> last_clone task
| None -> None
exception GoalNotFound
let task_goal = function
| Some { task_decl = Decl { d_node = Dprop (Pgoal,pr,_) }} -> pr
| _ -> raise GoalNotFound
(* Exception reporting *)
let () = Exn_printer.register
begin fun fmt exn -> match exn with
| LemmaFound -> Format.fprintf fmt "Task cannot contain a lemma"
| SkipFound -> Format.fprintf fmt "Task cannot contain a skip"
| GoalFound -> Format.fprintf fmt "The task already ends with a goal"
| GoalNotFound -> Format.fprintf fmt "The task does not end with a goal"
| _ -> raise exn
......
src/core/task.mli
View file @ 18a0e0b0
......@@ -17,6 +17,7 @@
(* *)
(**************************************************************************)
open Util
open Ident
open Ty
open Term
......@@ -25,6 +26,9 @@ open Theory
(** Task *)
type clone_map = Stdecl.t Mid.t
type meta_map = Stdecl.t Mstr.t
type task = task_hd option
and task_hd = private {
......@@ -32,31 +36,25 @@ and task_hd = private {
task_prev : task; (* context *)
task_known : known_map; (* known identifiers *)
task_clone : clone_map; (* cloning history *)
task_used : use_map; (* referenced theories *)
task_meta : meta_map; (* meta properties *)
task_tag : int; (* unique task tag *)
}
and tdecl = private
| Decl of decl
| Use of theory
| Clone of theory * (ident * ident) list
val task_equal : task -> task -> bool
val task_hd_equal : task_hd -> task_hd -> bool
val task_known : task -> known_map
val task_clone : task -> clone_map
val task_used : task -> use_map
val task_meta : task -> meta_map
(** {2 constructors} *)
val create_decl : decl -> tdecl
val add_decl : task -> decl -> task
val add_tdecl : task -> tdecl -> task
val use_export : task -> theory -> task
val clone_export : task -> theory -> th_inst -> task
val add_meta : task -> string -> meta_arg list -> task
(** {2 declaration constructors + add_decl} *)
......@@ -79,17 +77,23 @@ val split_theory : theory -> Spr.t option -> task list
val task_fold : ('a -> tdecl -> 'a) -> 'a -> task -> 'a
val task_iter : (tdecl -> unit) -> task -> unit
val task_tdecls : task -> tdecl list
val task_decls : task -> decl list
val task_decls : task -> decl list
val task_goal : task -> prsymbol
val last_clone : task -> task
val last_use : task -> task
(* TO BE REMOVED *)
val old_task_clone : task -> Sid.t Mid.t
val old_task_use : task -> theory Mid.t
val last_clone : task -> task
val last_use : task -> task
(* exceptions *)
exception GoalNotFound
exception GoalFound
exception SkipFound
exception LemmaFound
src/core/theory.ml
View file @ 18a0e0b0
This diff is collapsed.
src/core/theory.mli
View file @ 18a0e0b0
......@@ -30,41 +30,69 @@ 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 Mnm.t; (* propositions *)
ns_pr : prsymbol 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 -> prsymbol
val ns_find_ts : namespace -> string list -> tysymbol
val ns_find_ls : namespace -> string list -> lsymbol
val ns_find_pr : namespace -> string list -> prsymbol
val ns_find_prop : namespace -> string list -> prop
val ns_find_fmla : namespace -> string list -> fmla
(** Meta properties *)
type meta_arg_type =
| MTtysymbol
| MTlsymbol
| MTprsymbol
| MTstring
| MTint
type meta_arg =
| MAts of tysymbol
| MAls of lsymbol
| MApr of prsymbol
| MAstr of string
| MAint of int
type meta_arg_real =
| MARid of ident
| MARstr of string
| MARint of int
val register_meta : string -> meta_arg_type list -> unit
val lookup_meta : string -> meta_arg_type list
val list_meta : unit -> string list
(** Theory *)
type theory = private {
th_name : ident; (* theory name *)
th_decls : tdecl list; (* theory declarations *)
th_export : namespace; (* exported namespace *)
th_known : known_map; (* known identifiers *)
th_clone : clone_map; (* cloning history *)
th_used : use_map; (* referenced theories *)
th_local : Sid.t; (* locally declared idents *)
th_name : ident; (* theory name *)
th_decls : tdecl list; (* theory declarations *)
th_export : namespace; (* exported namespace *)
th_known : known_map; (* known identifiers *)
th_local : Sid.t; (* locally declared idents *)
th_used : Sid.t; (* used theories *)
}
and tdecl = private {
td_node : tdecl_node;
td_tag : int;
}
and tdecl = private
and tdecl_node = private
| Decl of decl
| Use of theory
| Clone of theory * (ident * ident) list
and use_map = theory Mid.t
| Clone of theory * ident Mid.t
| Meta of string * meta_arg_real list