Commit 18e27a9a authored by Andrei Paskevich's avatar Andrei Paskevich

print preludes. And we really need to revise Driver.

parent 6fd622fe
...@@ -63,5 +63,5 @@ let find_theory env sl s = ...@@ -63,5 +63,5 @@ let find_theory env sl s =
let env_tag env = env.env_tag let env_tag env = env.env_tag
let print_theorynotfound fmt (l,s) = let print_theorynotfound fmt (l,s) =
Format.fprintf fmt "%s.%s" (String.concat "." l) s Format.fprintf fmt "%s.%s" (String.concat "." l) s
...@@ -111,8 +111,8 @@ let add_decl opt d = ...@@ -111,8 +111,8 @@ let add_decl opt d =
| None -> Some (init_decl d) | None -> Some (init_decl d)
let rec flat_theory used cl task th = let rec flat_theory used cl task th =
if Sid.mem th.th_name used then used,cl,task else if Mid.mem th.th_name used then used,cl,task else
let acc = Sid.add th.th_name used, cl, task in let acc = Mid.add th.th_name th used, cl, task in
List.fold_left flat_tdecl acc th.th_decls List.fold_left flat_tdecl acc th.th_decls
and flat_tdecl (used, cl, task) = function and flat_tdecl (used, cl, task) = function
...@@ -143,14 +143,14 @@ let split_tdecl names (res, used, cl, task) = function ...@@ -143,14 +143,14 @@ let split_tdecl names (res, used, cl, task) = function
begin match d.d_node with begin match d.d_node with
| Dprop (Pgoal,pr,_) | Dprop (Pgoal,pr,_)
when option_apply true (Spr.mem pr) names -> when option_apply true (Spr.mem pr) names ->
let t = add_decl task d, cl in let t = add_decl task d, cl, used in
t :: res, used, cl, task t :: res, used, cl, task
| Dprop (Pgoal,_,_) -> | Dprop (Pgoal,_,_) ->
res, used, cl, task res, used, cl, task
| Dprop (Plemma,pr,f) | Dprop (Plemma,pr,f)
when option_apply true (Spr.mem pr) names -> when option_apply true (Spr.mem pr) names ->
let d = create_prop_decl Pgoal pr f in let d = create_prop_decl Pgoal pr f in
let t = add_decl task d, cl in let t = add_decl task d, cl, used in
let d = create_prop_decl Paxiom pr f in let d = create_prop_decl Paxiom pr f in
t :: res, used, cl, add_decl task d t :: res, used, cl, add_decl task d
| Dprop (Plemma,pr,f) -> | Dprop (Plemma,pr,f) ->
...@@ -163,12 +163,12 @@ let split_tdecl names (res, used, cl, task) = function ...@@ -163,12 +163,12 @@ let split_tdecl names (res, used, cl, task) = function
end end
let split_theory th names = let split_theory th names =
let acc = [], Sid.empty, empty_clone, None in let acc = [], Mid.empty, empty_clone, None in
let res,_,_,_ = List.fold_left (split_tdecl names) acc th.th_decls in let res,_,_,_ = List.fold_left (split_tdecl names) acc th.th_decls in
res res
let flat_theory task th = let flat_theory task th =
let _,_,task = flat_theory Sid.empty empty_clone task th in let _,_,task = flat_theory Mid.empty empty_clone task th in
task task
(* Generic utilities *) (* Generic utilities *)
......
...@@ -47,7 +47,7 @@ and task_hd = private { ...@@ -47,7 +47,7 @@ and task_hd = private {
val add_decl : task -> decl -> task val add_decl : task -> decl -> task
val split_theory : theory -> Spr.t option -> (task * clone) list val split_theory : theory -> Spr.t option -> (task * clone * use_map) list
val flat_theory : task -> theory -> task val flat_theory : task -> theory -> task
......
...@@ -88,7 +88,7 @@ type theory = { ...@@ -88,7 +88,7 @@ type theory = {
th_export : namespace; (* exported namespace *) th_export : namespace; (* exported namespace *)
th_clone : clone_map; (* cloning history *) th_clone : clone_map; (* cloning history *)
th_known : known_map; (* known identifiers *) th_known : known_map; (* known identifiers *)
th_used : Sid.t; (* referenced theories *) th_used : use_map; (* referenced theories *)
th_local : Sid.t; (* locally declared idents *) th_local : Sid.t; (* locally declared idents *)
} }
...@@ -97,6 +97,8 @@ and tdecl = ...@@ -97,6 +97,8 @@ and tdecl =
| Use of theory | Use of theory
| Clone of theory * (ident * ident) list | Clone of theory * (ident * ident) list
and use_map = theory Mid.t
and clone_map = Sid.t Mid.t and clone_map = Sid.t Mid.t
let builtin_theory = let builtin_theory =
...@@ -126,7 +128,7 @@ let builtin_theory = ...@@ -126,7 +128,7 @@ let builtin_theory =
th_export = export; th_export = export;
th_clone = Mid.empty; th_clone = Mid.empty;
th_known = kn_neq; th_known = kn_neq;
th_used = Sid.empty; th_used = Mid.empty;
th_local = Sid.empty } th_local = Sid.empty }
...@@ -139,21 +141,21 @@ type theory_uc = { ...@@ -139,21 +141,21 @@ type theory_uc = {
uc_export : namespace list; uc_export : namespace list;
uc_clone : clone_map; uc_clone : clone_map;
uc_known : known_map; uc_known : known_map;
uc_used : Sid.t; uc_used : use_map;
uc_local : Sid.t; uc_local : Sid.t;
} }
exception CloseTheory exception CloseTheory
exception NoOpenedNamespace exception NoOpenedNamespace
let create_theory n = let empty_theory n =
{ uc_name = id_register n; { uc_name = id_register n;
uc_decls = [Use builtin_theory]; uc_decls = [];
uc_import = [builtin_theory.th_export]; uc_import = [empty_ns];
uc_export = [builtin_theory.th_export]; uc_export = [empty_ns];
uc_clone = Mid.empty; uc_clone = Mid.empty;
uc_known = builtin_theory.th_known; uc_known = Mid.empty;
uc_used = Sid.singleton builtin_theory.th_name; uc_used = Mid.empty;
uc_local = Sid.empty; } uc_local = Sid.empty; }
let close_theory uc = match uc.uc_export with let close_theory uc = match uc.uc_export with
...@@ -191,9 +193,13 @@ let close_namespace uc import s = ...@@ -191,9 +193,13 @@ let close_namespace uc import s =
| _ -> | _ ->
assert false assert false
let merge_used m th =
Mid.add th.th_name th (Mid.fold Mid.add th.th_used m)
let use_export uc th = let use_export uc th =
let uc = if Sid.mem th.th_name uc.uc_used then uc else { uc with let uc = if Mid.mem th.th_name uc.uc_used then uc else
uc_used = Sid.add th.th_name (Sid.union uc.uc_used th.th_used); { uc with
uc_used = merge_used uc.uc_used th;
uc_known = merge_known uc.uc_known th.th_known; uc_known = merge_known uc.uc_known th.th_known;
uc_decls = Use th :: uc.uc_decls } uc_decls = Use th :: uc.uc_decls }
in in
...@@ -204,6 +210,8 @@ let use_export uc th = ...@@ -204,6 +210,8 @@ let use_export uc th =
| _ -> | _ ->
assert false assert false
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
...@@ -474,8 +482,8 @@ let cl_add_tdecl cl inst uc td = match td with ...@@ -474,8 +482,8 @@ let cl_add_tdecl cl inst uc td = match td with
uc_known = known_add_decl uc.uc_known d } uc_known = known_add_decl uc.uc_known d }
| None -> uc | None -> uc
end end
| Use th -> if Sid.mem th.th_name uc.uc_used then uc else { uc with | Use th -> if Mid.mem th.th_name uc.uc_used then uc else { uc with
uc_used = Sid.add th.th_name (Sid.union uc.uc_used th.th_used); uc_used = merge_used uc.uc_used th;
uc_known = merge_known uc.uc_known th.th_known; uc_known = merge_known uc.uc_known th.th_known;
uc_decls = td :: uc.uc_decls } uc_decls = td :: uc.uc_decls }
| Clone (th,sl) -> | Clone (th,sl) ->
......
...@@ -49,7 +49,7 @@ type theory = private { ...@@ -49,7 +49,7 @@ type theory = private {
th_export : namespace; (* exported namespace *) th_export : namespace; (* exported namespace *)
th_clone : clone_map; (* cloning history *) th_clone : clone_map; (* cloning history *)
th_known : known_map; (* known identifiers *) th_known : known_map; (* known identifiers *)
th_used : Sid.t; (* referenced theories *) th_used : use_map; (* referenced theories *)
th_local : Sid.t; (* locally declared idents *) th_local : Sid.t; (* locally declared idents *)
} }
...@@ -58,6 +58,8 @@ and tdecl = private ...@@ -58,6 +58,8 @@ and tdecl = private
| Use of theory | Use of theory
| Clone of theory * (ident * ident) list | Clone of theory * (ident * ident) list
and use_map = theory Mid.t
and clone_map = Sid.t Mid.t and clone_map = Sid.t Mid.t
val builtin_theory : theory val builtin_theory : theory
......
...@@ -135,9 +135,10 @@ and raw_driver = { ...@@ -135,9 +135,10 @@ and raw_driver = {
} }
and driver = { and driver = {
drv_raw : raw_driver; drv_raw : raw_driver;
drv_clone : clone; drv_clone : clone;
drv_env : env; drv_used : theory Mid.t;
drv_env : env;
drv_thprelude : string list Hid.t; drv_thprelude : string list Hid.t;
(* the first is the translation only for this ident, the second is (* the first is the translation only for this ident, the second is
also for representant *) also for representant *)
...@@ -222,7 +223,7 @@ let check_syntax loc s len = ...@@ -222,7 +223,7 @@ let check_syntax loc s len =
i len) s i len) s
let load_rules env clone driver {thr_name = loc,qualid; thr_rules = trl} = let load_rules env driver {thr_name = loc,qualid; thr_rules = trl} =
let id,qfile = qualid_to_slist qualid in let id,qfile = qualid_to_slist qualid in
let th = try let th = try
find_theory env qfile id find_theory env qfile id
...@@ -382,20 +383,40 @@ let syntax_arguments s print fmt l = ...@@ -382,20 +383,40 @@ let syntax_arguments s print fmt l =
let apply_transforms drv = let apply_transforms drv =
apply_clone drv.drv_raw.drv_transforms drv.drv_env drv.drv_clone apply_clone drv.drv_raw.drv_transforms drv.drv_env drv.drv_clone
let cook_driver env clone drv = let cook_driver env clone used drv =
let drv = { drv_raw = drv; let drv = { drv_raw = drv;
drv_clone = clone; drv_clone = clone;
drv_env = env; drv_used = used;
drv_env = env;
drv_thprelude = Hid.create 17; drv_thprelude = Hid.create 17;
drv_theory = Hid.create 17; drv_theory = Hid.create 17;
drv_with_task = Hid.create 17} in drv_with_task = Hid.create 17} in
List.iter (load_rules env clone drv) drv.drv_raw.drv_rules; List.iter (load_rules env drv) drv.drv_raw.drv_rules;
drv drv
let print_prelude drv fmt =
let pr_pr s () = fprintf fmt "%s@\n" s in
List.fold_right pr_pr drv.drv_raw.drv_prelude ();
let seen = Hid.create 17 in
let rec print_prel th_name th =
if Hid.mem seen th_name then () else
Hid.add seen th_name ();
Mid.iter print_prel th.th_used;
let prel =
try Hid.find drv.drv_thprelude th_name
with Not_found -> []
in
List.fold_right pr_pr prel ()
in
Mid.iter print_prel drv.drv_used;
fprintf fmt "@."
let print_task drv fmt task = match drv.drv_raw.drv_printer with let print_task drv fmt task = match drv.drv_raw.drv_printer with
| None -> errorm "no printer" | None -> errorm "no printer"
| Some f -> f drv fmt task | Some f ->
print_prelude drv fmt;
f drv fmt task
let regexp_filename = Str.regexp "%\\([a-z]\\)" let regexp_filename = Str.regexp "%\\([a-z]\\)"
......
...@@ -32,7 +32,7 @@ val load_driver : string -> env -> raw_driver ...@@ -32,7 +32,7 @@ val load_driver : string -> env -> raw_driver
(** cooked driver *) (** cooked driver *)
type driver type driver
val cook_driver : env -> clone -> raw_driver -> driver val cook_driver : env -> clone -> Theory.use_map -> raw_driver -> driver
(** querying drivers *) (** querying drivers *)
......
...@@ -172,9 +172,9 @@ let transform env l = ...@@ -172,9 +172,9 @@ let transform env l =
let extract_goals ?filter = let extract_goals ?filter =
fun env drv acc th -> fun env drv acc th ->
let l = split_theory th filter in let l = split_theory th filter in
let l = List.rev_map (fun (task,cl) -> let l = List.rev_map (fun (task,cl,used) ->
let drv = Driver.cook_driver env cl drv in let drv = Driver.cook_driver env cl used drv in
(th,task,drv)) l in (th,task,drv)) l in
List.rev_append l acc List.rev_append l acc
let file_sanitizer = None (* We should remove which character? *) let file_sanitizer = None (* We should remove which character? *)
......
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