Commit d96ec44b authored by Andrei Paskevich's avatar Andrei Paskevich

faire joli

parent 0e46a420
......@@ -372,3 +372,88 @@ let create_ind_decls idl =
| [_] -> [create_ind_decl idl]
| _ -> List.rev_map create_ind_decl (build idl)
(** Known identifiers *)
exception KnownIdent of ident
exception UnknownIdent of ident
exception RedeclaredIdent of ident
type known = decl Mid.t
let known_id kn id =
if not (Mid.mem id kn) then raise (UnknownIdent id)
let known_ts kn () ts = known_id kn ts.ts_name
let known_ls kn () ls = known_id kn ls.ls_name
let known_ty kn ty = ty_s_fold (known_ts kn) () ty
let known_term kn t = t_s_fold (known_ts kn) (known_ls kn) () t
let known_fmla kn f = f_s_fold (known_ts kn) (known_ls kn) () f
let merge_known kn1 kn2 =
let add_known id decl kn =
try
if Mid.find id kn2 != decl then raise (RedeclaredIdent id);
kn
with Not_found -> Mid.add id decl kn
in
Mid.fold add_known kn1 kn2
let add_known id decl kn =
try
if Mid.find id kn != decl then raise (RedeclaredIdent id);
raise (KnownIdent id)
with Not_found -> Mid.add id decl kn
let add_constr d kn fs = add_known fs.ls_name d kn
let add_type d kn (ts,def) =
let kn = add_known ts.ts_name d kn in
match def with
| Tabstract -> kn
| Talgebraic lfs -> List.fold_left (add_constr d) kn lfs
let check_type kn (ts,def) =
let check_constr fs = List.iter (known_ty kn) fs.ls_args in
match def with
| Tabstract -> option_iter (known_ty kn) ts.ts_def
| Talgebraic lfs -> List.iter check_constr lfs
let add_logic d kn (ls,_) = add_known ls.ls_name d kn
let check_ls_defn kn ld =
let _,e = open_ls_defn ld in
e_apply (known_term kn) (known_fmla kn) e
let check_logic kn (ls,ld) =
List.iter (known_ty kn) ls.ls_args;
option_iter (known_ty kn) ls.ls_value;
option_iter (check_ls_defn kn) 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.pr_name d kn in
List.fold_left add kn la
let check_ind kn (ps,la) =
List.iter (known_ty kn) ps.ls_args;
let check (_,f) = known_fmla kn f in
List.iter check la
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.pr_name d kn
let check_decl kn d = match d.d_node with
| Dtype dl -> List.iter (check_type kn) dl
| Dlogic dl -> List.iter (check_logic kn) dl
| Dind dl -> List.iter (check_ind kn) dl
| Dprop (_,_,f) -> known_fmla kn f
let kn_add_decl kn d =
let kn = add_decl kn d in
ignore (check_decl kn d);
kn
......@@ -112,3 +112,13 @@ exception UnboundVars of Svs.t
exception ClashIdent of ident
exception EmptyDecl
(** Known identifiers *)
type known = decl Mid.t
val kn_add_decl : known -> decl -> known
exception KnownIdent of ident
exception UnknownIdent of ident
exception RedeclaredIdent of ident
......@@ -47,7 +47,7 @@ let create_env =
exception TheoryNotFound of string list * string
let find_theory env sl s =
try
try
let m =
try
Hashtbl.find env.env_memo sl
......@@ -58,7 +58,7 @@ let find_theory env sl s =
m
in
Mnm.find s m
with Not_found ->
with Not_found ->
raise (TheoryNotFound (sl, s))
let env_tag env = env.env_tag
......
......@@ -16,102 +16,81 @@
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Env
open Task
open Trans
type 'a value = env option -> clone option -> 'a
type 'a registered = {mutable value : 'a value;
generate : unit -> 'a value;
tag : int}
type 'a registered = {
mutable value : 'a value;
generate : unit -> 'a value;
}
type 'a trans_reg = 'a trans registered
type 'a tlist_reg = 'a tlist registered
(*
module HSreg =
struct
type t = 'a registered
let equal a b = a.tag = b.tag
let hash a = a.tag
end
module WeakReg = Weak.Make(HSreg)
let registers = WeakReg.create 17
*)
let c = ref (-1)
let create gen =
let reg = {value = gen ();
generate = gen;
tag = (incr c; !c)} in
(* WeakRef.add registers reg;*)
reg
let cl_tag cl = cl.cl_tag
let create gen = {
value = gen ();
generate = gen;
}
exception ArgumentNeeded
let memo f tag h = function
let memo f tag h = function
| None -> raise ArgumentNeeded
| Some x ->
let t = tag x in
try
Hashtbl.find h t
try Hashtbl.find h t
with Not_found ->
let r = f x in
Hashtbl.add h t r;
r
let memo0 tag f =
let memo_t = Hashtbl.create 7 in
memo f tag memo_t
let memo0 tag f = memo f tag (Hashtbl.create 7)
let unused0 f = fun _ -> f
let cl_tag cl = cl.cl_tag
let store0 memo_env memo_cl f =
let gen () =
let gen () =
let f2 = memo_env (f ()) in
fun env -> memo_cl (f2 env) in
fun env -> memo_cl (f2 env)
in
create gen
let store f = store0 unused0 unused0 f
let store_env f = store0 (memo0 env_tag) unused0 f
let store f = store0 unused0 unused0 f
let store_env f = store0 (memo0 env_tag) unused0 f
let store_clone f = store0 (memo0 env_tag) (memo0 cl_tag) f
let apply0 reg env clone = Trans.apply (reg.value env clone)
let apply_clone reg env clone = apply0 reg (Some env) (Some clone)
let apply_env reg env = apply0 reg (Some env) None
let apply reg = apply0 reg None None
let apply_clone reg env clone = apply0 reg (Some env) (Some clone)
let apply_env reg env = apply0 reg (Some env) None
let apply reg = apply0 reg None None
let clear reg = reg.value<-reg.generate ()
(*
(* We change reg here but that doesnt change the hash and equality*)
let clear_all () = WeakReg.iter clear registers
*)
let clear_all () = assert false
let clear reg = reg.value <- reg.generate ()
let compose0 comp reg1 reg2 =
let combine comb reg1 reg2 =
let gen () =
let reg1 = reg1.generate () in
let reg2 = reg2.generate () in
fun env cl -> comp (reg1 env cl) (reg2 env cl) in
fun env cl -> comb (reg1 env cl) (reg2 env cl) in
create gen
let compose reg1 reg2 = compose0 (fun f g -> Trans.compose f g) reg1 reg2
let compose_l reg1 reg2 = compose0 (fun f g -> Trans.compose_l f g)
reg1 reg2
let conv_res conv reg1 =
let compose r1 r2 = combine (fun t1 t2 -> Trans.compose t1 t2) r1 r2
let compose_l r1 r2 = combine (fun t1 t2 -> Trans.compose_l t1 t2) r1 r2
let conv_res conv reg1 =
let gen () =
let reg1 = reg1.generate () in
fun env cl -> conv (reg1 env cl) in
create gen
let singleton reg = conv_res singleton reg
let singleton reg = conv_res Trans.singleton reg
let identity = store (fun () -> Trans.identity)
let identity_l = store (fun () -> Trans.identity_l)
let identity_trans = store (fun () -> identity)
let identity_trans_l = store (fun () -> identity_l)
......@@ -16,6 +16,7 @@
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Env
open Task
open Trans
......@@ -23,27 +24,26 @@ open Trans
type 'a trans_reg
type 'a tlist_reg = 'a list trans_reg
val store : (unit -> 'a trans) -> 'a trans_reg
val store_env : (unit -> env -> 'a trans) -> 'a trans_reg
val store : (unit -> 'a trans) -> 'a trans_reg
val store_env : (unit -> env -> 'a trans) -> 'a trans_reg
val store_clone : (unit -> env -> clone -> 'a trans) -> 'a trans_reg
exception ArgumentNeeded
val apply_clone : 'a trans_reg -> env -> clone -> task -> 'a
val apply_env : 'a trans_reg -> env -> task -> 'a
val apply : 'a trans_reg -> task -> 'a
val apply_env : 'a trans_reg -> env -> task -> 'a
val apply : 'a trans_reg -> task -> 'a
val compose : task trans_reg -> 'a trans_reg -> 'a trans_reg
val compose_l : task tlist_reg -> 'a tlist_reg -> 'a tlist_reg
val compose : task trans_reg -> 'a trans_reg -> 'a trans_reg
val compose_l : task tlist_reg -> 'a tlist_reg -> 'a tlist_reg
(*val conv_res : ('a -> 'b) -> 'a registered -> 'b registered
(* Sould be used only with function working in constant time*)
*)
(* Should be only used with functions working in constant time *)
(* val conv_res : ('a -> 'b) -> 'a trans_reg -> 'b trans_reg *)
val singleton : 'a trans_reg -> 'a tlist_reg
val clear_all : unit -> unit
val clear : 'a trans_reg -> unit
val identity_trans : task trans_reg
val identity_trans_l : task tlist_reg
val identity : task trans_reg
val identity_l : task tlist_reg
......@@ -47,90 +47,6 @@ let add_clone =
{ cl_map = merge_clone cl.cl_map th sl; cl_tag = !r }
(** Known identifiers *)
exception UnknownIdent of ident
exception RedeclaredIdent of ident
let known_id kn id =
if not (Mid.mem id kn) then raise (UnknownIdent id)
let known_ts kn () ts = known_id kn ts.ts_name
let known_ls kn () ls = known_id kn ls.ls_name
let known_ty kn ty = ty_s_fold (known_ts kn) () ty
let known_term kn t = t_s_fold (known_ts kn) (known_ls kn) () t
let known_fmla kn f = f_s_fold (known_ts kn) (known_ls kn) () f
let merge_known kn1 kn2 =
let add_known id decl kn =
try
if Mid.find id kn2 != decl then raise (RedeclaredIdent id);
kn
with Not_found -> Mid.add id decl kn
in
Mid.fold add_known kn1 kn2
exception DejaVu
let add_known id decl kn =
try
if Mid.find id kn != decl then raise (RedeclaredIdent id);
raise DejaVu
with Not_found -> Mid.add id decl kn
let add_constr d kn fs = add_known fs.ls_name d kn
let add_type d kn (ts,def) =
let kn = add_known ts.ts_name d kn in
match def with
| Tabstract -> kn
| Talgebraic lfs -> List.fold_left (add_constr d) kn lfs
let check_type kn (ts,def) =
let check_constr fs = List.iter (known_ty kn) fs.ls_args in
match def with
| Tabstract -> option_iter (known_ty kn) ts.ts_def
| Talgebraic lfs -> List.iter check_constr lfs
let add_logic d kn (ls,_) = add_known ls.ls_name d kn
let check_ls_defn kn ld =
let _,e = open_ls_defn ld in
e_apply (known_term kn) (known_fmla kn) e
let check_logic kn (ls,ld) =
List.iter (known_ty kn) ls.ls_args;
option_iter (known_ty kn) ls.ls_value;
option_iter (check_ls_defn kn) 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.pr_name d kn in
List.fold_left add kn la
let check_ind kn (ps,la) =
List.iter (known_ty kn) ps.ls_args;
let check (_,f) = known_fmla kn f in
List.iter check la
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.pr_name d kn
let check_decl kn d = match d.d_node with
| Dtype dl -> List.iter (check_type kn) dl
| Dlogic dl -> List.iter (check_logic kn) dl
| Dind dl -> List.iter (check_ind kn) dl
| Dprop (_,_,f) -> known_fmla kn f
let add_decl kn d =
let kn = add_decl kn d in
ignore (check_decl kn d);
kn
(** Task *)
type task = task_hd option
......@@ -138,7 +54,7 @@ type task = task_hd option
and task_hd = {
task_decl : decl;
task_prev : task;
task_known : decl Mid.t;
task_known : known;
task_tag : int;
}
......@@ -178,12 +94,12 @@ let push_decl task d =
| Dprop (Pgoal,_,_) -> raise GoalFound
| _ -> ()
end;
try mk_task d (Some task) (add_decl task.task_known d)
with DejaVu -> task
try mk_task d (Some task) (kn_add_decl task.task_known d)
with KnownIdent _ -> task
let init_decl d =
try mk_task d None (add_decl Mid.empty d)
with DejaVu -> assert false
try mk_task d None (kn_add_decl Mid.empty d)
with KnownIdent _ -> assert false
let add_decl opt d =
begin match d.d_node with
......
......@@ -39,7 +39,7 @@ type task = task_hd option
and task_hd = private {
task_decl : decl;
task_prev : task;
task_known : decl Mid.t;
task_known : known;
task_tag : int;
}
......@@ -63,8 +63,6 @@ val task_goal : task -> prsymbol
(* exceptions *)
exception UnknownIdent of ident
exception RedeclaredIdent of ident
exception GoalNotFound
exception GoalFound
exception LemmaFound
......
......@@ -43,7 +43,7 @@ type lsymbol = private {
}
val create_lsymbol : preid -> ty list -> ty option -> bool -> lsymbol
(* create_lsymbols preid tyargs tyres is_constr *)
val create_fsymbol : preid -> ty list -> ty -> lsymbol
val create_fconstr : preid -> ty list -> ty -> lsymbol
val create_psymbol : preid -> ty list -> lsymbol
......
......@@ -245,22 +245,18 @@ let empty_inst = {
}
let create_inst ~ts ~ls ~lemma ~goal =
let ts =
let ts =
List.fold_left (fun acc (tso,tsn) -> Mts.add tso tsn acc) Mts.empty ts in
let ls =
let ls =
List.fold_left (fun acc (lso,lsn) -> Mls.add lso lsn acc) Mls.empty ls in
let make_list = List.fold_left (fun acc lem -> Spr.add lem acc) Spr.empty in
let lemma = make_list lemma in
let goal = make_list goal in
{
inst_ts = ts;
inst_ls = ls;
inst_lemma = lemma;
inst_goal = goal;
inst_lemma = make_list lemma;
inst_goal = make_list goal;
}
exception CannotInstantiate of ident
type clones = {
......
......@@ -68,13 +68,14 @@ val create_theory : preid -> theory_uc
val close_theory : theory_uc -> theory
val add_decl : theory_uc -> decl -> theory_uc
val use_export : theory_uc -> theory -> theory_uc
val open_namespace : theory_uc -> theory_uc
val close_namespace : theory_uc -> bool -> string option -> theory_uc
val get_namespace : theory_uc -> namespace
(** Use and clone *)
(** Clone *)
type th_inst = {
inst_ts : tysymbol Mts.t; (* old to new *)
......@@ -84,12 +85,13 @@ type th_inst = {
}
val empty_inst : th_inst
val create_inst :
ts:(tysymbol * tysymbol) list ->
ls:(lsymbol * lsymbol) list ->
lemma:prsymbol list -> goal:prsymbol list -> th_inst
val use_export : theory_uc -> theory -> theory_uc
val create_inst :
ts : (tysymbol * tysymbol) list ->
ls : (lsymbol * lsymbol) list ->
lemma : prsymbol list ->
goal : prsymbol list -> th_inst
val clone_export : theory_uc -> theory -> th_inst -> theory_uc
val merge_clone : clone_map -> theory -> (ident * ident) list -> clone_map
......
......@@ -32,7 +32,7 @@ type 'a tlist = 'a list trans
let identity x = x
let identity_l x = [x]
let conv_res f c x = c (f x)
let conv_res c f x = c (f x)
let singleton f x = [f x]
......@@ -96,8 +96,8 @@ let fold_l fn v =
let rewind = List.fold_left rewind in
accum memo_t rewind [v] []
let fold_map fn v t = conv_res (fold fn (v, t)) snd
let fold_map_l fn v t = conv_res (fold_l fn (v, t)) (List.rev_map snd)
let fold_map fn v t = conv_res snd (fold fn (v, t))
let fold_map_l fn v t = conv_res (List.rev_map snd) (fold_l fn (v, t))
let map fn = fold (fun t1 t2 -> fn t1 t2)
let map_l fn = fold_l (fun t1 t2 -> fn t1 t2)
......
......@@ -37,7 +37,8 @@ val singleton : 'a trans -> 'a tlist
val compose : task trans -> 'a trans -> 'a trans
val compose_l : task tlist -> 'a tlist -> 'a tlist
(* val conv_res : 'a trans -> ('a -> 'b) -> 'b trans *)
(* Should be only used with functions working in constant time *)
(* val conv_res : ('a -> 'b) -> 'a trans -> 'b trans *)
val fold : (task_hd -> 'a -> 'a ) -> 'a -> 'a trans
val fold_l : (task_hd -> 'a -> 'a list) -> 'a -> 'a tlist
......
......@@ -56,9 +56,9 @@ and ty_node =
| Tyvar of tvsymbol
| Tyapp of tysymbol * ty list
module Structts = Util.StructMake(struct
type t = tysymbol
let tag x = x.ts_name.id_tag
module Structts = Util.StructMake(struct
type t = tysymbol
let tag x = x.ts_name.id_tag
end)
module Sts = Structts.S
module Mts = Structts.M
......@@ -190,9 +190,9 @@ let ts_real = create_tysymbol (id_fresh "real") [] None
let ty_int = ty_app ts_int []
let ty_real = ty_app ts_real []
module Structty = Util.StructMake(struct
type t = ty
let tag x = x.ty_tag
module Structty = Util.StructMake(struct
type t = ty
let tag x = x.ty_tag
end)
module Sty = Structty.S
module Mty = Structty.M
......
......@@ -331,7 +331,7 @@ let load_driver file env =
with Not_found -> errorm ~loc "unknown transformation %s" s in
compose_l acc t
)
identity_trans_l transformations in
identity_l transformations in
let transforms = trans ltransforms in
{ drv_printer = !printer;
drv_task = None;
......
......@@ -127,8 +127,8 @@ let rec report fmt = function
Denv.report fmt e
| Typing.Error e ->
Typing.report fmt e
| UnknownIdent i ->
fprintf fmt "anomaly: unknownident %s" i.Ident.id_short
| Decl.UnknownIdent i ->
fprintf fmt "anomaly: unknown ident %s" i.Ident.id_short
| Driver.Error e ->
Driver.report fmt e
| Dynlink_compat.Dynlink.Error e ->
......
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