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

add a wrap_and_register that ... wraps and registers ! and also add the...

add a wrap_and_register that ... wraps and registers ! and also add the transformation type to its description
parent 8e278341
......@@ -266,19 +266,37 @@ let parse_theory env s =
with
_ -> raise (Arg_theory_not_found s)
let get_opt_type: type a b c. (a -> b, c) trans_typ -> (b, c) trans_typ =
let trans_typ_tail: type a b c. (a -> b, c) trans_typ -> (b, c) trans_typ =
fun t ->
match t with
| Tint t' -> t'
| Tty t' -> t'
| Ttysymbol t' -> t'
| Tprsymbol t' -> t'
| Tterm t' -> t'
| Tstring t' -> t'
| Tformula t' -> t'
| Ttheory t' -> t'
| Tint t -> t
| Tty t -> t
| Ttysymbol t -> t
| Tprsymbol t -> t
| Tterm t -> t
| Tstring t -> t
| Tformula t -> t
| Ttheory t -> t
| _ -> assert false
type _ trans_typ_is_l = Yes : (task list) trans_typ_is_l | No : task trans_typ_is_l
let rec is_trans_typ_l: type a b. (a, b) trans_typ -> b trans_typ_is_l =
fun t -> match t with
| Ttrans -> No
| Ttrans_l -> Yes
| Tint t -> is_trans_typ_l t
| Tty t -> is_trans_typ_l t
| Ttysymbol t -> is_trans_typ_l t
| Tprsymbol t -> is_trans_typ_l t
| Tterm t -> is_trans_typ_l t
| Tstring t -> is_trans_typ_l t
| Tformula t -> is_trans_typ_l t
| Ttheory t -> is_trans_typ_l t
| Tenv t -> is_trans_typ_l t
| Topt (_,t) -> is_trans_typ_l t
| Toptbool (_,t) -> is_trans_typ_l t
let string_of_trans_typ : type a b. (a, b) trans_typ -> string =
fun t ->
match t with
......@@ -296,6 +314,23 @@ let string_of_trans_typ : type a b. (a, b) trans_typ -> string =
| Topt (s,_) -> "opt [" ^ s ^ "]"
| Toptbool (s,_) -> "boolean opt [" ^ s ^ "]"
let rec print_type : type a b. (a, b) trans_typ -> string =
fun t ->
match t with
| Ttrans -> "()"
| Ttrans_l -> "()"
| Tint t -> "integer -> " ^ print_type t
| Tty t -> "type -> " ^ print_type t
| Ttysymbol t -> "type_symbol -> " ^ print_type t
| Tprsymbol t -> "prop_symbol -> " ^ print_type t
| Tterm t -> "term -> " ^ print_type t
| Tstring t -> "string -> " ^ print_type t
| Tformula t -> "formula -> " ^ print_type t
| Ttheory t -> "theory -> " ^ print_type t
| Tenv t -> "environment -> " ^ print_type t
| Topt (s,t) -> "opt [" ^ s ^ "] " ^ print_type t
| Toptbool (s,t) -> "opt [" ^ s ^ "] -> " ^ print_type t
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, l with
......@@ -347,7 +382,7 @@ let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.en
| _ -> assert false
end
| Topt (_, t'), _ ->
wrap_to_store (get_opt_type t') (f None) l env task
wrap_to_store (trans_typ_tail t') (f None) l env task
| Toptbool (optname, t'), s :: tail when s = optname ->
wrap_to_store t' (f true) tail env task
| Toptbool (_, t'), _ ->
......@@ -359,3 +394,16 @@ let wrap_l : type a. (a, task list) trans_typ -> a -> trans_with_args_l =
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)
let wrap_any : type a b. (a, b) trans_typ -> a -> string list -> Env.env -> b trans =
fun t f l env -> Trans.store (wrap_to_store t f l env)
let wrap_and_register : type a b. desc:Pp.formatted -> string -> (a, b) trans_typ -> a -> unit =
fun ~desc name t f ->
let type_desc = Scanf.format_from_string ("type : " ^ print_type t ^ "\n") Pp.empty_formatted in
let trans = wrap_any t f in
match is_trans_typ_l t with
| Yes ->
Trans.register_transform_with_args_l ~desc:(type_desc ^^ desc) name trans
| No ->
Trans.register_transform_with_args ~desc:(type_desc ^^ desc) name trans
......@@ -48,3 +48,5 @@ type (_, _) trans_typ =
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
val wrap_and_register : desc:Pp.formatted -> string -> ('a, 'b) trans_typ -> 'a -> unit
......@@ -404,59 +404,60 @@ let destruct pr : Task.task Trans.tlist =
let use_th th =
Trans.add_tdecls [Theory.create_use th]
let () = register_transform_with_args_l
let () = wrap_and_register
~desc:"case <term> [name] generates hypothesis 'name: term' in a first goal and 'name: ~ term' in a second one."
"case"
(wrap_l (Tformula (Topt ("as",Tstring Ttrans_l))) case)
(Tformula (Topt ("as",Tstring Ttrans_l))) case
let () = register_transform_with_args_l
let () = wrap_and_register
~desc:"cut <term> [name] makes a cut with hypothesis 'name: term'"
"cut"
(wrap_l (Tformula (Topt ("as",Tstring Ttrans_l))) cut)
(Tformula (Topt ("as",Tstring Ttrans_l))) cut
let () = register_transform_with_args
let () = wrap_and_register
~desc:"exists <term> substitutes the variable quantified by exists with term"
"exists"
(wrap (Tterm Ttrans) exists)
(Tterm Ttrans) exists
let () = register_transform_with_args
let () = wrap_and_register
~desc:"remove <prop> removes hypothesis named prop"
"remove"
(wrap (Tprsymbol Ttrans) remove)
(Tprsymbol Ttrans) remove
let () = register_transform_with_args
let () = wrap_and_register
~desc:"instantiate <prop> <term> generates a new hypothesis with first quantified variables of prop replaced with term "
"instantiate"
(wrap (Tprsymbol (Tterm Ttrans)) instantiate)
(Tprsymbol (Tterm Ttrans)) instantiate
let () = register_transform_with_args_l
let () = wrap_and_register
~desc:"apply <prop> applies prop to the goal" "apply"
(wrap_l (Tprsymbol Ttrans_l) apply)
(Tprsymbol Ttrans_l) apply
let () = register_transform_with_args_l
let () = wrap_and_register
~desc:"duplicate <int> duplicates the goal int times" "duplicate"
(wrap_l (Tint Ttrans_l) (fun x -> Trans.store (dup x)))
(Tint Ttrans_l) (fun x -> Trans.store (dup x))
let () = register_transform_with_args
let () = wrap_and_register
~desc:"use_th <theory> imports the theory" "use_th"
(wrap (Ttheory Ttrans) use_th)
(Ttheory Ttrans) use_th
let () = register_transform_with_args_l
~desc:"rewrite [<-] <name> [in] <name2> rewrites equality defined in name into name2"
"rewrite"
(wrap_l (Toptbool ("<-",(Tprsymbol (Topt ("in", Tprsymbol Ttrans_l))))) rewrite)
let _ = wrap_and_register
~desc:"rewrite [<-] <name> [in] <name2> rewrites equality defined in name into name2" "rewrite"
(Toptbool ("<-",(Tprsymbol (Topt ("in", Tprsymbol Ttrans_l))))) rewrite
(* register_transform_with_args_l *)
(* ~desc:"rewrite [<-] <name> [in] <name2> rewrites equality defined in name into name2" *)
(* "rewrite" *)
(* (wrap_l (Toptbool ("<-",(Tprsymbol (Topt ("in", Tprsymbol Ttrans_l))))) rewrite) *)
let () = register_transform_with_args_l
let () = wrap_and_register
~desc:"replace <term1> <term2> <name> replaces occcurences of term1 by term2 in prop name"
"replace"
(wrap_l (Tterm (Tterm (Tprsymbol Ttrans_l))) replace)
(Tterm (Tterm (Tprsymbol Ttrans_l))) replace
let () = register_transform_with_args_l
let () = wrap_and_register
~desc:"induction <term1> <term2> performs induction on int term1 from int term2"
"induction"
(wrap_l (Tenv (Tterm (Tterm Ttrans_l))) induction)
(Tenv (Tterm (Tterm Ttrans_l))) induction
let () = register_transform_with_args_l
~desc:"destruct <name> destructs the head constructor of hypothesis name"
"destruct"
(wrap_l (Tprsymbol Ttrans_l) destruct)
let () = wrap_and_register ~desc:"destruct <name> destructs the head constructor of hypothesis name"
"destruct" (Tprsymbol Ttrans_l) destruct
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