Commit 84dc2aa6 authored by Clément Fumex's avatar Clément Fumex
Browse files

+ change type trans_with_args to use task trans type

+ add type trans_with_args_l + wrap_l + register_..._l
+ add use_th transformation that will use import a theory in the current goal
parent 723f80a8
......@@ -42,6 +42,8 @@ let compose_l f g x = Lists.apply g (f x)
let seq l x = List.fold_left (fun x f -> f x) x l
let seq_l l x = List.fold_left (fun x f -> Lists.apply f x) [x] l
let par (l:task trans list) x = List.map (fun f -> f x) l
module Wtask = Weakhtbl.Make (struct
type t = task_hd
let tag t = t.task_tag
......@@ -333,22 +335,33 @@ let list_transforms_l () =
(** transformations with arguments *)
type trans_with_args = string list -> task -> task list
type trans_with_args = string list -> Env.env -> task trans
type trans_with_args_l = string list -> Env.env -> task tlist
let transforms_with_args = Hstr.create 17
let transforms_with_args_l = Hstr.create 17
let lookup_transform_with_args s =
try snd (Hstr.find transforms_with_args s)
with Not_found -> raise (UnknownTrans s)
let lookup_transform_with_args_l s =
try snd (Hstr.find transforms_with_args_l s)
with Not_found -> raise (UnknownTrans s)
let register_transform_with_args ~desc s p =
if Hstr.mem transforms_with_args s then raise (KnownTrans s);
Hstr.replace transforms_with_args s (desc, fun _ -> p)
let register_transform_with_args_l ~desc s p =
if Hstr.mem transforms_with_args_l s then raise (KnownTrans s);
Hstr.replace transforms_with_args_l s (desc, fun _ -> p)
type gentrans =
| Trans_one of Task.task trans
| Trans_list of Task.task tlist
| Trans_with_args of trans_with_args
| Trans_with_args_l of trans_with_args_l
let lookup_trans env name =
try
......@@ -359,21 +372,26 @@ let lookup_trans env name =
let t = lookup_transform_l name env in
Trans_list t
with UnknownTrans _ ->
let t = lookup_transform_with_args name env in
Trans_with_args t
try
let t = lookup_transform_with_args name env in
Trans_with_args t
with UnknownTrans _ ->
let t = lookup_transform_with_args_l name env in
Trans_with_args_l t
let apply_transform tr_name env task =
match lookup_trans env tr_name with
| Trans_one t -> [apply t task]
| Trans_list t -> apply t task
| Trans_with_args t -> t [] task
| Trans_with_args _ (* [apply (t []) task] *)
| Trans_with_args_l _ -> assert false (* apply (t []) task *)
let apply_transform_args tr_name env args task =
match lookup_trans env tr_name with
| Trans_one t -> [apply t task]
| Trans_list t -> apply t task
| Trans_with_args t -> t args task
| Trans_with_args t -> [apply (t args) env task]
| Trans_with_args_l t -> apply (t args) env task
(** Flag-dependent transformations *)
......
......@@ -40,6 +40,11 @@ val compose_l : task tlist -> 'a tlist -> 'a tlist
val seq : task trans list -> task trans
val seq_l : task tlist list -> task tlist
(** parallelize transformations: [par l] will duplicate the current
task in [n] new tasks, with [n] the length of [l], and apply to each of
this new task the corresponding transformation in [l] *)
val par : task trans list -> task tlist
(** Create Transformation *)
val fold : (task_hd -> 'a -> 'a ) -> 'a -> 'a trans
val fold_l : (task_hd -> 'a -> 'a list) -> 'a -> 'a tlist
......@@ -145,9 +150,12 @@ val apply_transform : string -> Env.env -> task -> task list
*)
type trans_with_args = string list -> task -> task list
type trans_with_args = string list -> Env.env -> task trans
type trans_with_args_l = string list -> Env.env -> task tlist
val register_transform_with_args : desc:Pp.formatted -> string -> trans_with_args -> unit
val register_transform_with_args_l : desc:Pp.formatted -> string -> trans_with_args_l -> unit
val apply_transform_args : string -> Env.env -> string list -> task -> task list
(** apply a registered 1-to-1 or a 1-to-n or a trans with args, directly *)
......@@ -162,17 +162,16 @@ let build_name_tables task : name_tables =
(************* wrapper *************)
type _ trans_typ =
| Ttrans : (task -> task list) trans_typ
| Tint : 'a trans_typ -> (int -> 'a) trans_typ
(*
| Tstring : 'a trans_typ -> (string -> 'a) trans_typ
*)
| Tty : 'a trans_typ -> (ty -> 'a) trans_typ
| Ttysymbol : 'a trans_typ -> (tysymbol -> 'a) trans_typ
| Tprsymbol : 'a trans_typ -> (Decl.prsymbol -> 'a) trans_typ
| Tterm : 'a trans_typ -> (term -> 'a) trans_typ
| Tformula : 'a trans_typ -> (term -> 'a) trans_typ
type (_, _) trans_typ =
| Ttrans : ((task trans), task) trans_typ
| Ttrans_l : ((task tlist), task list) trans_typ
| Tint : ('a, 'b) trans_typ -> ((int -> 'a), 'b) trans_typ
| Tty : ('a, 'b) trans_typ -> ((ty -> 'a), 'b) trans_typ
| Ttysymbol : ('a, 'b) trans_typ -> ((tysymbol -> 'a), 'b) trans_typ
| Tprsymbol : ('a, 'b) trans_typ -> ((Decl.prsymbol -> 'a), 'b) trans_typ
| Tterm : ('a, 'b) trans_typ -> ((term -> 'a), 'b) trans_typ
| Tformula : ('a, 'b) trans_typ -> ((term -> 'a), 'b) trans_typ
| Ttheory : ('a, 'b) trans_typ -> ((Theory.theory -> 'a), 'b) trans_typ
let find_pr s task =
let tables = build_name_tables task in
......@@ -186,45 +185,6 @@ let type_ptree ~as_fmla t task =
then Typing.type_fmla_in_namespace ns km (fun _ -> None) t
else Typing.type_term_in_namespace ns km (fun _ -> None) t
(*
(*** term argument parsed in the context of the task ***)
let type_ptree ~as_fmla t task =
let used_ths = Task.used_theories task in
let used_symbs = Task.used_symbols used_ths in
let local_decls = Task.local_decls task used_symbs in
(* rebuild a theory_uc *)
let th_uc = Theory.create_theory (Ident.id_fresh "dummy") in
let th_uc =
Ident.Mid.fold
(fun _id th acc ->
let name = th.Theory.th_name in
(**)
Format.eprintf "[Args_wrapper.type_ptree] use theory %s (%s)@."
_id.Ident.id_string
name.Ident.id_string;
(**)
Theory.close_namespace
(Theory.use_export
(Theory.open_namespace acc name.Ident.id_string)
th)
true)
used_ths th_uc
in
let th_uc =
List.fold_left
(fun acc d ->
(**)
Format.eprintf "[Args_wrapper.type_ptree] add decl %a@."
Pretty.print_decl d;
(**)
Theory.add_decl ~warn:false acc d)
th_uc local_decls
in
if as_fmla
then Typing.type_fmla th_uc (fun _ -> None) t
else Typing.type_term th_uc (fun _ -> None) t
*)
let parse_and_type ~as_fmla s task =
let lb = Lexing.from_string s in
let t =
......@@ -235,65 +195,82 @@ let parse_and_type ~as_fmla s task =
in
t
let rec wrap : type a. a trans_typ -> a -> trans_with_args =
fun t f l task ->
match t with
| Ttrans -> f task
| Tint t' ->
begin
match l with
| s :: tail ->
(try
let n = int_of_string s in
wrap t' (f n) tail task
with Failure _ -> raise (Failure "Parsing error: expecting an integer."))
| _ -> failwith "Missing argument: expecting an integer."
end
(*
| Tstring t' ->
begin
match l with
| s :: tail -> wrap t' (f s) tail task
| _ -> failwith "Missing argument: expecting a string."
end
*)
| Tformula t' ->
begin
match l with
| s :: tail ->
let te = parse_and_type ~as_fmla:true s task in
wrap t' (f te) tail task
| _ -> failwith "Missing argument: expecting a formula."
end
| Tterm t' ->
begin
match l with
| s :: tail ->
let te = parse_and_type ~as_fmla:false s task in
wrap t' (f te) tail task
| _ -> failwith "Missing argument: expecting a term."
end
| Tty t' ->
begin
match l with
| _s :: tail ->
let ty = Ty.ty_int in (* TODO: parsing + typing of s *)
wrap t' (f ty) tail task
| _ -> failwith "Missing argument: expecting a type."
end
| Ttysymbol t' ->
begin
match l with
| _s :: tail ->
let tys = Ty.ts_int in (* TODO: parsing + typing of s *)
wrap t' (f tys) tail task
| _ -> failwith "Missing argument: expecting a type symbol."
end
| Tprsymbol t' ->
begin
match l with
let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.env -> task -> b =
fun t f l env task ->
match t with
| Ttrans -> apply f task
| Ttrans_l -> apply f task
| Tint t' ->
begin
match l with
| s :: tail ->
(try
let n = int_of_string s in
wrap_to_store t' (f n) tail env task
with Failure _ -> raise (Failure "Parsing error: expecting an integer."))
| _ -> failwith "Missing argument: expecting an integer."
end
| Tformula t' ->
begin
match l with
| s :: tail ->
let te = parse_and_type ~as_fmla:true s task in
wrap_to_store t' (f te) tail env task
| _ -> failwith "Missing argument: expecting a formula."
end
| Tterm t' ->
begin
match l with
| s :: tail ->
let te = parse_and_type ~as_fmla:false s task in
wrap_to_store t' (f te) tail env task
| _ -> failwith "Missing argument: expecting a term."
end
| Tty t' ->
begin
match l with
| _s :: tail ->
let ty = Ty.ty_int in (* TODO: parsing + typing of s *)
wrap_to_store t' (f ty) tail env task
| _ -> failwith "Missing argument: expecting a type."
end
| Ttysymbol t' ->
begin
match l with
| _s :: tail ->
let tys = Ty.ts_int in (* TODO: parsing + typing of s *)
wrap_to_store t' (f tys) tail env task
| _ -> failwith "Missing argument: expecting a type symbol."
end
| Tprsymbol t' ->
begin
match l with
| s :: tail ->
let pr = find_pr s task in
wrap t' (f pr) tail task
| _ -> failwith "Missing argument: expecting a prop symbol."
end
wrap_to_store t' (f pr) tail env task
| _ -> failwith "Missing argument: expecting a prop symbol."
end
| Ttheory t' ->
begin
match l with
| s :: tail ->
(try
let path, name = match Str.split (Str.regexp "\.") s with
| [name] -> [],name
| path::[name] ->
let path = Str.split (Str.regexp "/") path in
path, name
| _ -> failwith "Ill-formed theory name"
in
let th = Env.read_theory env path name in
wrap_to_store t' (f th) tail env task
with
_ -> failwith "Theory not found.")
| _ -> failwith "Missing argument: expecting a theory."
end
let wrap_l : type a. (a, task list) trans_typ -> a -> trans_with_args_l =
fun t f l env -> Trans.store (wrap_to_store t f l env)
let wrap : type a. (a, task) trans_typ -> a -> trans_with_args =
fun t f l env -> Trans.store (wrap_to_store t f l env)
......@@ -13,20 +13,21 @@ type name_tables = {
val build_name_tables : Task.task -> name_tables
type _ trans_typ =
| Ttrans : (task -> task list) trans_typ
| Tint : 'a trans_typ -> (int -> 'a) trans_typ
(*
| Tstring : 'a trans_typ -> (string -> 'a) trans_typ
*)
| Tty : 'a trans_typ -> (Ty.ty -> 'a) trans_typ
| Ttysymbol : 'a trans_typ -> (Ty.tysymbol -> 'a) trans_typ
| Tprsymbol : 'a trans_typ -> (Decl.prsymbol -> 'a) trans_typ
| Tterm : 'a trans_typ -> (Term.term -> 'a) trans_typ
| Tformula : 'a trans_typ -> (Term.term -> 'a) trans_typ
type (_, _) trans_typ =
| Ttrans : (task Trans.trans, task) trans_typ
| Ttrans_l : (task Trans.tlist, task list) trans_typ
| Tint : ('a, 'b) trans_typ -> ((int -> 'a), 'b) trans_typ
| Tty : ('a, 'b) trans_typ -> ((Ty.ty -> 'a), 'b) trans_typ
| Ttysymbol : ('a, 'b) trans_typ -> ((Ty.tysymbol -> 'a), 'b) trans_typ
| Tprsymbol : ('a, 'b) trans_typ -> ((Decl.prsymbol -> 'a), 'b) trans_typ
| Tterm : ('a, 'b) trans_typ -> ((Term.term -> 'a), 'b) trans_typ
| Tformula : ('a, 'b) trans_typ -> ((Term.term -> 'a), 'b) trans_typ
| Ttheory : ('a, 'b) trans_typ -> ((Theory.theory -> 'a), 'b) trans_typ
(** wrap arguments of transformations, turning string arguments into
arguments of proper types. arguments of type term of formula are
parsed and typed, name resolution using the given name_tables. *)
val wrap : (* name_tables -> *) 'a trans_typ -> 'a -> Trans.trans_with_args
val wrap_l : ('a, task list) trans_typ -> 'a -> Trans.trans_with_args_l
val wrap : ('a, task) trans_typ -> 'a -> Trans.trans_with_args
......@@ -20,26 +20,22 @@ let gen_ident = Ident.id_fresh
(* From task [delta |- G] and term t, build the tasks:
[delta, t] |- G] and [delta, not t | - G] *)
let case t task =
(*
clean_environment task;
*)
let case t =
let h = Decl.create_prsymbol (gen_ident "h") in
let hnot = Decl.create_prsymbol (gen_ident "hnot") in
let t_not_decl = Decl.create_prop_decl Decl.Paxiom hnot (Term.t_not t) in
let t_decl = Decl.create_prop_decl Decl.Paxiom h t in
List.map (fun f -> Trans.apply f task) [Trans.add_decls [t_decl]; Trans.add_decls [t_not_decl]]
Trans.par [Trans.add_decls [t_decl]; Trans.add_decls [t_not_decl]]
(* From task [delta |- G] , build the tasks [delta, t | - G] and [delta] |- t] *)
let cut t task =
clean_environment task;
let g, task = Task.task_separate_goal task in
let cut t =
(* let g, task = Task.task_separate_goal task in *)
let h = Decl.create_prsymbol (gen_ident "h") in
let g_t = Decl.create_prop_decl Decl.Pgoal h t in
let h_t = Decl.create_prop_decl Decl.Paxiom h t in
let goal_cut = Task.add_decl task g_t in
let goal = Task.add_tdecl (Task.add_decl task h_t) g in
[goal; goal_cut]
let goal_cut = Trans.goal (fun _ _ -> [g_t]) in
let goal = Trans.add_decls [h_t] in
Trans.par [goal; goal_cut]
let subst_quant c tq x : term =
let (vsl, tr, te) = t_open_quant tq in
......@@ -77,7 +73,7 @@ let exists x task =
let t = subst_exist t x in
let pr_goal = create_prsymbol (gen_ident "G") in
let new_goal = Decl.create_prop_decl Decl.Pgoal pr_goal t in
[Task.add_decl task new_goal]
Task.add_decl task new_goal
| _ -> failwith "No goal"
(* Return a new task with hypothesis name removed *)
......@@ -94,10 +90,8 @@ let remove_task_decl (name: Ident.ident) : task trans =
are extracted from same name. Seemed not to work before
adding "print_task". To be resolved in a better way. *)
(* from task [delta, name:A |- G] build the task [delta |- G] *)
let remove name task =
clean_environment task;
[Trans.apply (remove_task_decl name.pr_name) task]
let remove name =
remove_task_decl name.pr_name
let pr_prsymbol pr =
match pr with
......@@ -122,15 +116,15 @@ let instantiate (pr:Decl.prsymbol) t task =
let ndecl = find_hypothesis name task in
match ndecl with
| None -> Format.printf "Hypothesis %s not found@." name.Ident.id_string;
[Task.add_tdecl task g]
Task.add_tdecl task g
| Some decl -> (match decl.td_node with
| Decl {d_node = Dprop (pk, _pr, ht)} ->
let t_subst = subst_forall ht t in
let new_pr = create_prsymbol (Ident.id_clone name) in
let new_decl = create_prop_decl pk new_pr t_subst in
let task = add_decl task new_decl in
[Task.add_tdecl task g]
| _ -> Format.printf "Not an hypothesis@."; [Task.add_tdecl task g])
Task.add_tdecl task g
| _ -> Format.printf "Not an hypothesis@."; Task.add_tdecl task g)
(* TODO find correct librrary *)
let choose_option a b =
......@@ -212,10 +206,12 @@ let apply pr task =
let new_tb = t_subst_single v x tb in
(* TODO t_equal is probably too strong *)
if (Term.t_equal new_tb tg) then
[Task.add_decl task (create_prop_decl Pgoal
(create_prsymbol (gen_ident "G")) new_goal)]
Task.add_decl task (create_prop_decl Pgoal
(create_prsymbol (gen_ident "G")) new_goal)
else
(Format.printf "Term substituted was %a. Should be goal was %a. Goal was %a @." Pretty.print_term x Pretty.print_term new_tb Pretty.print_term tg;
(Format.printf
"Term substituted was %a. Should be goal was %a. Goal was %a @."
Pretty.print_term x Pretty.print_term new_tb Pretty.print_term tg;
failwith "After substitution, terms are not exactly identical")
end
| _ -> failwith "Not of the form forall immediately followed by implies"
......@@ -223,11 +219,15 @@ let apply pr task =
| Tbinop (Timplies, _ta, _tb) -> failwith "Not implemented yet" (* TODO to be done later *)
| _ -> failwith "Not of the form forall x. A -> B"
let () = register_transform_with_args ~desc:"test case" "case" (wrap (Tformula Ttrans) case)
let () = register_transform_with_args ~desc:"test cut" "cut" (wrap (Tformula Ttrans) cut)
let () = register_transform_with_args ~desc:"test exists" "exists" (wrap (Tterm Ttrans) exists)
let use_th th =
Trans.add_tdecls [Theory.create_use th]
let () = register_transform_with_args_l ~desc:"test case" "case" (wrap_l (Tformula Ttrans_l) case)
let () = register_transform_with_args_l ~desc:"test cut" "cut" (wrap_l (Tformula Ttrans_l) cut)
(* let () = register_transform_with_args ~desc:"test exists" "exists" (wrap (Tterm Ttrans) exists) *)
let () = register_transform_with_args ~desc:"test remove" "remove" (wrap (Tprsymbol Ttrans) remove)
let () = register_transform_with_args ~desc:"test instantiate" "instantiate"
(*let () = register_transform_with_args ~desc:"test instantiate" "instantiate"
(wrap (Tprsymbol (Tterm Ttrans)) instantiate)
let () = register_transform_with_args ~desc:"test apply" "apply" (wrap (Tprsymbol Ttrans) apply)
let () = register_transform_with_args ~desc:"test duplicate" "duplicate" (wrap (Tint Ttrans) dup)
let () = register_transform_with_args_l ~desc:"test duplicate" "duplicate" (wrap_l (Tint Ttrans_l) dup) *)
let () = register_transform_with_args ~desc:"use theory" "use_th" (wrap (Ttheory Ttrans) (use_th))
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