Commit de5927c1 authored by Sylvain Dailler's avatar Sylvain Dailler

Added list of terms for instantiate.

parent 594f552d
......@@ -245,6 +245,8 @@ rule token = parse
let parse_term lb = Loc.with_location (Parser.term_eof token) lb
let parse_term_list lb = Loc.with_location (Parser.term_comma_list_eof token) lb
let parse_qualid lb = Loc.with_location (Parser.qualid_eof token) lb
let parse_list_ident lb = Loc.with_location (Parser.ident_comma_list_eof token) lb
......
......@@ -222,6 +222,7 @@ end
%start <Ptree.term> term_eof
%start <Ptree.qualid> qualid_eof
%start <Ptree.qualid list> qualid_comma_list_eof
%start <Ptree.term list> term_comma_list_eof
%start <Ptree.ident list> ident_comma_list_eof
%%
......@@ -1106,3 +1107,7 @@ qualid_comma_list_eof:
ident_comma_list_eof:
| comma_list1(ident) EOF { $1 }
(* TODO: Weird to not have any parser conflicts here *)
term_comma_list_eof:
| comma_list1(term) EOF { $1 }
......@@ -246,6 +246,10 @@ let get_exception_message ses id e =
| Args_wrapper.Unnecessary_arguments l ->
Pp.sprintf "First arguments were parsed and typed correcly but the last following are useless:\n%a"
(Pp.print_list Pp.newline (fun fmt s -> Format.fprintf fmt "%s" s)) l, Loc.dummy_position, ""
| Generic_arg_trans_utils.Unnecessary_terms l ->
Pp.sprintf "First arguments were parsed and typed correcly but the last following are useless:\n%a"
(Pp.print_list Pp.newline
(fun fmt s -> Format.fprintf fmt "%a" (print_term ses id) s)) l, Loc.dummy_position, ""
| Args_wrapper.Arg_expected_none s ->
Pp.sprintf "An argument was expected of type %s, none were given" s, Loc.dummy_position, ""
......
......@@ -188,7 +188,8 @@ type (_, _) trans_typ =
| Tlsymbol : ('a, 'b) trans_typ -> ((Term.lsymbol -> 'a), 'b) trans_typ
| Tsymbol : ('a, 'b) trans_typ -> ((symbol -> 'a), 'b) trans_typ
| Tlist : ('a, 'b) trans_typ -> ((symbol list -> 'a), 'b) trans_typ
| Tidentlist : ('a, 'b) trans_typ -> ((string list -> 'a), 'b) trans_typ
| Tidentlist : ('a, 'b) trans_typ -> ((string list -> 'a), 'b) trans_typ
| Ttermlist : ('a, 'b) trans_typ -> ((term list -> '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
......@@ -235,6 +236,19 @@ let parse_and_type ~as_fmla s task =
with
| Loc.Located (loc, e) -> raise (Arg_parse_type_error (loc, s, e))
let parse_and_type_list ~as_fmla s task =
try
let lb = Lexing.from_string s in
let t_list =
Lexer.parse_term_list lb
in
let t_list =
List.map (fun t -> type_ptree ~as_fmla:as_fmla t task) t_list
in
t_list
with
| Loc.Located (loc, e) -> raise (Arg_parse_type_error (loc, s, e))
let parse_qualid s =
try
let lb = Lexing.from_string s in
......@@ -316,6 +330,7 @@ let rec is_trans_typ_l: type a b. (a, b) trans_typ -> b trans_typ_is_l =
| Tlist t -> is_trans_typ_l t
| Tterm t -> is_trans_typ_l t
| Tidentlist t -> is_trans_typ_l t
| Ttermlist t -> is_trans_typ_l t
| Tformula t -> is_trans_typ_l t
| Ttheory t -> is_trans_typ_l t
| Topt (_,t) -> is_trans_typ_l t
......@@ -340,6 +355,7 @@ let rec string_of_trans_typ : type a b. (a, b) trans_typ -> string =
| Tterm _ -> "term"
| Tformula _ -> "formula"
| Tidentlist _ -> "list ident"
| Ttermlist _ -> "list term"
| Ttheory _ -> "theory"
| Topt (s,t) -> "?" ^ s ^ (string_of_trans_typ t)
| Toptbool (s,_) -> "?" ^ s ^ ":bool"
......@@ -362,7 +378,8 @@ let rec print_type : type a b. (a, b) trans_typ -> string =
| Tlist t -> "list symbol -> " ^ print_type t
| Tterm t -> "term -> " ^ print_type t
| Tformula t -> "formula -> " ^ print_type t
| Tidentlist t -> "list ident -> " ^ print_type t
| Tidentlist t -> "list ident -> " ^ print_type t
| Ttermlist t -> "list term -> " ^ print_type t
| Ttheory t -> "theory -> " ^ print_type t
| Topt (s,t) -> "?" ^ s ^ ":" ^ print_type t
| Toptbool (s,t) -> "?" ^ s ^ ":bool -> " ^ print_type t
......@@ -429,6 +446,9 @@ let rec wrap_to_store : type a b. (a, b) trans_typ -> a -> string list -> Env.en
| Tidentlist t', s :: tail ->
let list = List.map (fun id -> id.Ptree.id_str) (parse_list_ident s) in
wrap_to_store t' (f list) tail env tables task
| Ttermlist t', s :: tail ->
let term_list = parse_and_type_list ~as_fmla:false s tables in
wrap_to_store t' (f term_list) tail env tables task
| Topt (optname, t'), s :: s' :: tail when s = optname ->
begin match t' with
| Tint t' ->
......
......@@ -81,6 +81,8 @@ type (_, _) trans_typ =
| Tidentlist : ('a, 'b) trans_typ -> ((string list -> 'a), 'b) trans_typ
(** transformation with a list of identifiers as argument. The identifiers do not need
to exist in the task, typically they could be fresh symbols *)
| Ttermlist : ('a, 'b) trans_typ -> ((Term.term list -> 'a), 'b) trans_typ
(** transformation with a list of terms as argument. *)
| Tterm : ('a, 'b) trans_typ -> ((Term.term -> 'a), 'b) trans_typ
(** transformation with a Why3 term as argument *)
| Tformula : ('a, 'b) trans_typ -> ((Term.term -> 'a), 'b) trans_typ
......
......@@ -155,13 +155,13 @@ let destruct pr : Task.task Trans.tlist =
(* from task [delta, name:forall x.A |- G,
build the task [delta,name:forall x.A,name':A[x -> t]] |- G] *)
let instantiate (pr: Decl.prsymbol) t =
let instantiate (pr: Decl.prsymbol) lt =
let r = ref [] in
Trans.decl
(fun d ->
match d.d_node with
| Dprop (pk, dpr, ht) when Ident.id_equal dpr.pr_name pr.pr_name ->
let t_subst = subst_forall ht t in
let t_subst = subst_forall_list ht lt in
let new_pr = create_prsymbol (Ident.id_clone dpr.pr_name) in
let new_decl = create_prop_decl pk new_pr t_subst in
r := [new_decl];
......@@ -169,11 +169,10 @@ let instantiate (pr: Decl.prsymbol) t =
| Dprop (Pgoal, _, _) -> !r @ [d]
| _ -> [d]) None
let () = wrap_and_register
~desc:"instantiate <prop> <term> generates a new hypothesis with first quantified variables of prop replaced with term "
~desc:"instantiate <prop> <term list> generates a new hypothesis with quantified variables of prop replaced with terms"
"instantiate"
(Tprsymbol (Tterm Ttrans)) instantiate
(Tprsymbol (Ttermlist Ttrans)) instantiate
let () = wrap_and_register ~desc:"destruct <name> destructs the head constructor of hypothesis name"
"destruct" (Tprsymbol Ttrans_l) destruct
......
......@@ -17,6 +17,7 @@ exception Arg_trans_pattern of (string * pattern * pattern)
exception Arg_trans_type of (string * Ty.ty * Ty.ty)
exception Arg_bad_hypothesis of (string * term)
exception Cannot_infer_type of string
exception Unnecessary_terms of term list
let gen_ident = Ident.id_fresh
......@@ -29,13 +30,31 @@ let subst_quant c tq x : term =
(match vsl with
| hdv :: tl ->
(try
(let new_t = t_subst_single hdv x te in
t_quant_close c tl tr new_t)
let new_t = t_subst_single hdv x te in
t_quant_close c tl tr new_t
with
| Ty.TypeMismatch (ty1, ty2) ->
raise (Arg_trans_type ("subst_quant", ty1, ty2)))
| [] -> failwith "subst_quant: Should not happen, please report")
let subst_quant_list quant term_quant list_term : term =
let (vsl, triggers, te) = t_open_quant term_quant in
let rec create_mvs list_term vsl acc =
match list_term, vsl with
| t :: lt_tl, v :: vsl_tl ->
create_mvs lt_tl vsl_tl (Mvs.add v t acc)
| _ :: _, [] -> raise (Unnecessary_terms list_term)
| [], vsl_remaining -> acc, vsl_remaining
in
let m_subst, variables_remaining = create_mvs list_term vsl Mvs.empty in
try
let new_t = t_subst m_subst te in
t_quant_close quant variables_remaining triggers new_t
with
| Ty.TypeMismatch (ty1, ty2) ->
raise (Arg_trans_type ("subst_quant_list", ty1, ty2))
(* Transform the term (exists v, f) into f[x/v] *)
let subst_exist t x =
match t.t_node with
......@@ -49,3 +68,11 @@ let subst_forall t x =
| Tquant (Tforall, tq) ->
subst_quant Tforall tq x
| _ -> raise (Arg_trans "subst_forall")
(* Same as subst_forall but l is a list of term *)
let subst_forall_list t l =
match t.t_node with
| Tquant (Tforall, tq) ->
subst_quant_list Tforall tq l
| _ -> raise (Arg_trans "subst_forall_list")
......@@ -17,6 +17,7 @@ exception Arg_trans_pattern of (string * pattern * pattern)
exception Arg_trans_type of (string * Ty.ty * Ty.ty)
exception Arg_bad_hypothesis of (string * term)
exception Cannot_infer_type of string
exception Unnecessary_terms of term list
val gen_ident : ?label:Ident.Slab.t -> ?loc:Loc.position -> string -> Ident.preid
......@@ -29,3 +30,7 @@ val subst_exist: term -> term -> term
(* Transform the term (forall v, f) into f[x/v] *)
val subst_forall: term -> term -> term
(* TODO remove subst_forall and subst_exist *)
(* Same as subst_forall with a list of term *)
val subst_forall_list: term -> term list -> term
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