Commit 22ef0535 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

Adding formula into trans type. We need to know if a term is a formula

or not before parsing with wrap. So we give a Tformula instead of Tterm
constructor for those transformations.
parent f3e6c74a
......@@ -10,6 +10,7 @@ type _ trans_typ =
| Tty : 'a trans_typ -> (ty -> 'a) trans_typ
| Ttysymbol : 'a trans_typ -> (tysymbol -> 'a) trans_typ
| Tterm : 'a trans_typ -> (term -> 'a) trans_typ
| Tformula : 'a trans_typ -> (term -> 'a) trans_typ
(*** term argument parsed in the context of the task ***)
let type_ptree ~as_fmla t task =
......@@ -33,17 +34,13 @@ let type_ptree ~as_fmla t task =
then Typing.type_fmla th_uc (fun _ -> None) t
else Typing.type_term th_uc (fun _ -> None) t
let parse_and_type s task =
let parse_and_type ~as_fmla s task =
let lb = Lexing.from_string s in
let t =
Lexer.parse_term lb
in
let t =
(* TODO I need both as_fmla = true and as_fmla = false in some transformations. How to tell which one to use ?
For example, cut needs a formula and simple_apply needs a term *)
try
type_ptree ~as_fmla:false t task
with _ -> type_ptree ~as_fmla:true t task
type_ptree ~as_fmla:as_fmla t task
in
t
......@@ -67,17 +64,19 @@ let rec wrap : type a. a trans_typ -> a -> trans_with_args =
| s :: tail -> wrap t' (f s) tail task
| _ -> failwith "Missing argument: expecting a string."
end
(* | Tformula t' ->
| Tformula t' ->
begin
end (* TODO *)
*)
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 s task in
let te = parse_and_type ~as_fmla:false s task in
wrap t' (f te) tail task
| _ -> failwith "Missing argument: expecting a term."
end
......
......@@ -8,5 +8,6 @@ type _ trans_typ =
| Tty : 'a trans_typ -> (Ty.ty -> 'a) trans_typ
| Ttysymbol : 'a trans_typ -> (Ty.tysymbol -> 'a) trans_typ
| Tterm : 'a trans_typ -> (Term.term -> 'a) trans_typ
| Tformula : 'a trans_typ -> (Term.term -> 'a) trans_typ
val wrap : 'a trans_typ -> 'a -> Trans.trans_with_args
......@@ -224,43 +224,8 @@ let apply name task =
| Tbinop (Timplies, _ta, _tb) -> failwith "Not implemented yet" (* TODO to be done later *)
| _ -> failwith "Not of the form forall x. A -> B"
(*
let case' =
(*
args task =
match args with
| [TAterm t] -> case t task
| _ -> failwith "wrong arguments for case"
*)
let cut' args task =
match args with
| [TAterm t] -> cut t task
| _ -> failwith "wrong arguments for cut"
let exists' args task =
match args with
| [TAterm t] -> exists t task
| _ -> failwith "wrong arguments for exists"
let remove' args task =
match args with
| [TAstring name] -> remove name task
| _ -> failwith "wrong argument for remove"
let simple_apply' args task =
match args with
| [TAstring name; TAterm t] -> simple_apply name t task
| _ -> failwith "wrong arguments of simple_apply"
let apply' args task =
match args with
| [TAstring name] -> apply name task
| _ -> failwith "wrong arguments of simple_apply"
*)
let () = register_transform_with_args ~desc:"test case" "case" (wrap (Tterm Ttrans) case)
let () = register_transform_with_args ~desc:"test cut" "cut" (wrap (Tterm Ttrans) cut)
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 () = register_transform_with_args ~desc:"test remove" "remove" (wrap (Tstring Ttrans) remove)
let () = register_transform_with_args ~desc:"test simple_apply" "simple_apply"
......
......@@ -453,122 +453,30 @@ let test_transformation_with_args fmt args =
in
C.schedule_transformation cont id "duplicate" args ~callback
(* Do not use this. TODO
Claude: indeed type_fmla and type_term should never be used like this
*)
let typing_terms t th =
try (Typing.type_fmla th (fun _ -> None) t) with
| _ -> Typing.type_term th (fun _ -> None) t
(*
let parse_transformation_arg args : Term.term option =
(* temporary : parses the term *)
match args with
| [s] ->
printf "parsing string '%s'@." s;
begin try
let lb = Lexing.from_string s in
let t = Lexer.parse_term lb in
printf "parsing OK@.";
let env = cont.controller_env in
let th = Theory.create_theory (Ident.id_fresh "dummy") in
let int_theory = Env.read_theory env ["int"] "Int" in
let th = Theory.use_export th int_theory in
let t = typing_terms t th in
let _ = printf "typing OK: %a@." Pretty.print_term t in
Some t
with e ->
let _ = printf "Error while parsing/typing: %a@." Exn_printer.exn_printer e in
None
end
| _ -> let _ = printf "term argument expected@." in None
*)
(*
let parse_transformation_string args : string option =
(* temporary : parses a string *)
match args with
| [s] ->
let s =
let l = String.length s in
if l >= 2 && s.[0] = '"' && s.[l - 1] = '"' then
String.sub s 1 (l - 2)
else s
in
printf "parsing string \"%s\"@." s;
Some s
| _ -> let _ = printf "term argument expected@." in None
*)
let test_simple_apply fmt args =
(* temporary : parses a string *)
(*
match args with
| [s';s] ->
let s =
let l = String.length s in
if l >= 2 && s.[0] = '"' && s.[l - 1] = '"' then
String.sub s 1 (l - 2)
else s
in
let s' =
let l = String.length s' in
if l >= 2 && s'.[0] = '"' && s'.[l - 1] = '"' then
String.sub s' 1 (l - 2)
else s'
in
printf "parsing string \"%s\"@." s;
begin try
let lb = Lexing.from_string s in
let t = Lexer.parse_term lb in
printf "parsing OK@.";
let env = cont.controller_env in
let th = Theory.create_theory (Ident.id_fresh "dummy") in
let int_theory = Env.read_theory env ["int"] "Int" in
let th = Theory.use_export th int_theory in
let t = typing_terms t th in
let _ = printf "typing OK: %a@." Pretty.print_term t in
*)
let id = nearest_goal () in
let callback status =
fprintf fmt "transformation status: %a@."
Controller_itp.print_trans_status status
in
C.schedule_transformation cont id "simple_apply" args ~callback
(*
with e ->
let _ = printf "Error while parsing/typing: %a@." Exn_printer.exn_printer e in
()
end
| _ -> let _ = printf "term argument expected@." in ()
*)
let id = nearest_goal () in
let callback status =
fprintf fmt "transformation status: %a@."
Controller_itp.print_trans_status status
in
C.schedule_transformation cont id "simple_apply" args ~callback
let test_apply_with_string_args fmt args =
(*
match (parse_transformation_string args) with
| None -> ()
| Some s ->
*)
let id = nearest_goal () in
let callback status =
fprintf fmt "transformation status: %a@."
Controller_itp.print_trans_status status
in
C.schedule_transformation cont id "apply" args ~callback
let id = nearest_goal () in
let callback status =
fprintf fmt "transformation status: %a@."
Controller_itp.print_trans_status status
in
C.schedule_transformation cont id "apply" args ~callback
let test_remove_with_string_args fmt args =
(*
match (parse_transformation_string args) with
| None -> ()
| Some s ->
*)
let id = nearest_goal () in
let callback status =
fprintf fmt "transformation status: %a@."
Controller_itp.print_trans_status status
in
C.schedule_transformation cont id "remove" args ~callback
let id = nearest_goal () in
let callback status =
fprintf fmt "transformation status: %a@."
Controller_itp.print_trans_status status
in
C.schedule_transformation cont id "remove" args ~callback
let type_ptree ~as_fmla t task =
let used_ths = Task.used_theories task in
......@@ -593,14 +501,10 @@ let type_ptree ~as_fmla t task =
let parse_arg_only s task =
let lb = Lexing.from_string s in
let t =
(* try *)
Lexer.parse_term lb
(* with _ -> failwith "parsing error" *)
Lexer.parse_term lb
in
let t =
(* try *)
type_ptree ~as_fmla:false t task
(* with *)
type_ptree ~as_fmla:false t task
in
eprintf "transformation parse_arg_only succeeds: %a@." Pretty.print_term t;
[task]
......@@ -610,20 +514,12 @@ let () = Trans.(register_transform_with_args
~desc:"Just parse and type the string argument")
let test_transformation_with_string_parsed_later fmt args =
(*
match args with
| [s] ->
*)
let id = nearest_goal () in
let callback status =
fprintf fmt "transformation status: %a@."
Controller_itp.print_trans_status status
in
C.schedule_transformation cont id "parse_arg_only" args ~callback
(*
| _ -> printf "string argument expected@."
*)
let id = nearest_goal () in
let callback status =
fprintf fmt "transformation status: %a@."
Controller_itp.print_trans_status status
in
C.schedule_transformation cont id "parse_arg_only" args ~callback
(*******)
......@@ -635,19 +531,13 @@ let test_transformation_with_term_arg _fmt args =
*)
let test_case_with_term_args fmt args =
(*
match (parse_transformation_arg args) with
| None -> ()
| Some t ->
*)
let id = nearest_goal () in
let callback status =
fprintf fmt "transformation status: %a@."
Controller_itp.print_trans_status status
Controller_itp.print_trans_status status
in
C.schedule_transformation cont id "case" args ~callback
(* TODO rewrite this. Only for testing *)
let test_transformation_one_arg_term fmt args =
match args with
......@@ -658,12 +548,7 @@ let test_transformation_one_arg_term fmt args =
fprintf fmt "transformation %s status: %a@."
tr Controller_itp.print_trans_status status
in
(*
match (parse_transformation_arg tl) with
| None -> ()
| Some t ->
*)
C.schedule_transformation cont id tr tl ~callback
C.schedule_transformation cont id tr tl ~callback
let task_driver =
......
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