Commit c58baa5d authored by Clément Fumex's avatar Clément Fumex

remove Tenv in Ttrans_typ and add Tenvtrans and Tenvtrans_l

parent 75adb70d
......@@ -221,19 +221,20 @@ let build_name_tables task : name_tables =
(************* wrapper *************)
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
| Tstring : ('a, 'b) trans_typ -> ((string -> '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
| Tenv : ('a, 'b) trans_typ -> ((Env.env -> 'a), 'b) trans_typ
| Topt : string * ('a -> 'c, 'b) trans_typ -> (('a option -> 'c), 'b) trans_typ
| Toptbool : string * ('a, 'b) trans_typ -> (bool -> 'a, 'b) trans_typ
| Ttrans : ((task trans), task) trans_typ
| Ttrans_l : ((task tlist), task list) trans_typ
| Tenvtrans : (Env.env -> (task trans), task) trans_typ
| Tenvtrans_l : (Env.env -> (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
| Tstring : ('a, 'b) trans_typ -> ((string -> '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
| Topt : string * ('a -> 'c, 'b) trans_typ -> (('a option -> 'c), 'b) trans_typ
| Toptbool : string * ('a, 'b) trans_typ -> (bool -> 'a, 'b) trans_typ
let find_pr s task =
let tables = build_name_tables task in
......@@ -291,7 +292,9 @@ type _ trans_typ_is_l = Yes : (task list) trans_typ_is_l | No : task trans_typ_i
let rec is_trans_typ_l: type a b. (a, b) trans_typ -> b trans_typ_is_l =
fun t -> match t with
| Tenvtrans -> No
| Ttrans -> No
| Tenvtrans_l -> Yes
| Ttrans_l -> Yes
| Tint t -> is_trans_typ_l t
| Tty t -> is_trans_typ_l t
......@@ -301,7 +304,6 @@ let rec is_trans_typ_l: type a b. (a, b) trans_typ -> b trans_typ_is_l =
| 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
......@@ -310,6 +312,8 @@ let string_of_trans_typ : type a b. (a, b) trans_typ -> string =
match t with
| Ttrans -> "trans"
| Ttrans_l -> "transl"
| Tenvtrans -> "env trans"
| Tenvtrans_l -> "env transl"
| Tint _ -> "integer"
| Tty _ -> "type"
| Ttysymbol _ -> "type symbol"
......@@ -318,7 +322,6 @@ let string_of_trans_typ : type a b. (a, b) trans_typ -> string =
| Tstring _ -> "string"
| Tformula _ -> "formula"
| Ttheory _ -> "theory"
| Tenv _ -> "environment"
| Topt (s,_) -> "opt [" ^ s ^ "]"
| Toptbool (s,_) -> "boolean opt [" ^ s ^ "]"
......@@ -327,6 +330,8 @@ let rec print_type : type a b. (a, b) trans_typ -> string =
match t with
| Ttrans -> "()"
| Ttrans_l -> "()"
| Tenvtrans -> "()"
| Tenvtrans_l -> "()"
| Tint t -> "integer -> " ^ print_type t
| Tty t -> "type -> " ^ print_type t
| Ttysymbol t -> "type_symbol -> " ^ print_type t
......@@ -335,7 +340,6 @@ let rec print_type : type a b. (a, b) trans_typ -> string =
| 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
......@@ -344,6 +348,8 @@ let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.en
match t, l with
| Ttrans, _-> apply f task
| Ttrans_l, _ -> apply f task
| Tenvtrans, _ -> apply (f env) task
| Tenvtrans_l, _ -> apply (f env) task
| Tint t', s :: tail ->
let arg = parse_int s in wrap_to_store t' (f arg) tail env task
| Tformula t', s :: tail ->
......@@ -366,7 +372,6 @@ let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.en
wrap_to_store t' (f th) tail env task
| Tstring t', s :: tail ->
wrap_to_store t' (f s) tail env task
| Tenv t', _ -> wrap_to_store t' (f env) l env task
| Topt (optname, t'), s :: s' :: tail when s = optname ->
begin match t' with
| Tint t' ->
......
......@@ -24,6 +24,8 @@ val build_name_tables : Task.task -> name_tables
type (_, _) trans_typ =
| Ttrans : (task Trans.trans, task) trans_typ
| Ttrans_l : (task Trans.tlist, task list) trans_typ
| Tenvtrans : (Env.env -> (task Trans.trans), task) trans_typ
| Tenvtrans_l : (Env.env -> (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
......@@ -32,7 +34,6 @@ type (_, _) trans_typ =
| Tstring : ('a, 'b) trans_typ -> ((string -> '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
| Tenv : ('a, 'b) trans_typ -> ((Env.env -> 'a), 'b) trans_typ
| Topt : string * ('a -> 'c, 'b) trans_typ -> (('a option -> 'c), 'b) trans_typ
| Toptbool : string * ('a, 'b) trans_typ -> (bool -> 'a, 'b) trans_typ
......
......@@ -328,7 +328,7 @@ let is_good_type t ty =
try (Term.t_ty_check t (Some ty); true) with
| _ -> false
let induction env x bound =
let induction x bound env =
let th = Env.read_theory env ["int"] "Int" in
let le_int = Theory.ns_find_ls th.Theory.th_export ["infix <="] in
let plus_int = Theory.ns_find_ls th.Theory.th_export ["infix +"] in
......@@ -474,7 +474,7 @@ let () = wrap_and_register
let () = wrap_and_register
~desc:"induction <term1> <term2> performs induction on int term1 from int term2"
"induction"
(Tenv (Tterm (Tterm Ttrans_l))) induction
(Tterm (Tterm Tenvtrans_l)) induction
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