Commit b5ff7fcf authored by Andrei Paskevich's avatar Andrei Paskevich

properly format the transformation descriptions

parent 5e93e6d7
...@@ -406,9 +406,6 @@ let list_transforms () = ...@@ -406,9 +406,6 @@ let list_transforms () =
let list_transforms_l () = let list_transforms_l () =
Hstr.fold (fun k (desc,_) acc -> (k, desc)::acc) transforms_l [] Hstr.fold (fun k (desc,_) acc -> (k, desc)::acc) transforms_l []
(** transformations with arguments *) (** transformations with arguments *)
type naming_table = { type naming_table = {
......
...@@ -124,8 +124,8 @@ let () = try ...@@ -124,8 +124,8 @@ let () = try
(Pp.print_list Pp.newline2 print_trans_desc) (Pp.print_list Pp.newline2 print_trans_desc)
(List.sort sort_pair (Trans.list_transforms_l ())); (List.sort sort_pair (Trans.list_transforms_l ()));
let list_transform_with_arg = let list_transform_with_arg =
Trans.list_transforms_with_args () @ Trans.list_transforms_with_args_l () Trans.list_transforms_with_args () @
in Trans.list_transforms_with_args_l () in
printf "@[<hov 2>Known transformations with arguments:@\n%a@]@\n@." printf "@[<hov 2>Known transformations with arguments:@\n%a@]@\n@."
(Pp.print_list Pp.newline2 print_trans_desc) (Pp.print_list Pp.newline2 print_trans_desc)
(List.sort sort_pair list_transform_with_arg) (List.sort sort_pair list_transform_with_arg)
......
...@@ -34,4 +34,5 @@ let elim_less (d:decl) = ...@@ -34,4 +34,5 @@ let elim_less (d:decl) =
let () = let () =
Trans.register_transform "abstract_quantifiers" (Trans.decl elim_less None) Trans.register_transform "abstract_quantifiers" (Trans.decl elim_less None)
~desc:"abstract@ quantifiers@ in@ the@ axioms@ of@ the@ context and the goals@." ~desc:"Abstract@ quantifiers@ in@ the@ axioms@ of@ the@ context \
and@ the@ goals."
...@@ -518,29 +518,51 @@ let unfold unf hl = ...@@ -518,29 +518,51 @@ let unfold unf hl =
| _ -> [d]) None | _ -> [d]) None
let () = wrap_and_register ~desc:"sort declarations" let () = wrap_and_register ~desc:"Sort@ declarations." "sort" Ttrans sort
"sort"
(Ttrans) sort
let () = wrap_and_register ~desc:"unfold ls [in] pr: unfold logic symbol ls in list of hypothesis pr. The argument in is optional: by default unfold in the goal." (* TODO *)
"unfold"
(Tlsymbol (Topt ("in", Tprlist Ttrans))) unfold
let () = wrap_and_register
~desc:"unfold <ls> [in] <name list>@ \
unfolds@ logical@ symbol@ <ls> in@ the@ given@ \
list@ of@ premises.@ If@ no@ list@ is@ given,@ \
unfold@ in@ the@ goal."
"unfold"
(Tlsymbol (Topt ("in", Tprlist Ttrans)))
unfold
let () = wrap_and_register let () = wrap_and_register
~desc:"replace <term1> <term2> [in] <name list> replaces occcurences of term1 by term2 in prop name. If no list is given, replace in the goal." ~desc:"replace <term1> <term2> [in] <name list>@ \
"replace" replaces@ occcurences@ of@ <term1>@ by@ <term2>@ in@ \
(Tterm (Tterm (Topt ("in", Tprlist Ttrans_l)))) replace the@ given@ list@ of@ premises.@ If@ no@ list@ is@ given,@ \
replace@ in@ the@ goal."
"replace"
(Tterm (Tterm (Topt ("in", Tprlist Ttrans_l))))
replace
let _ = wrap_and_register let _ = wrap_and_register
~desc:"rewrite [<-] <name> [in] <name2> [with] <list term> rewrites equality defined in name into name2 using exactly all terms of the list as instance for what cannot be deduced directly" "rewrite" ~desc:"rewrite [<-] <name> [in] <name2> [with] <term list>@ \
(Toptbool ("<-",(Tprsymbol (Topt ("in", Tprsymbol (Topt ("with", Ttermlist Ttrans_l))))))) (fun rev h h1opt term_list -> rewrite term_list rev h h1opt) rewrites@ equality@ defined@ in@ <name>@ into@ <name2>@ \
using@ exactly@ all@ terms@ in@ the@ list@ as@ instances@ \
for@ what@ cannot@ be@ deduced@ directly."
"rewrite"
(Toptbool ("<-",(Tprsymbol (Topt ("in",
Tprsymbol (Topt ("with", Ttermlist Ttrans_l)))))))
(fun rev h h1opt term_list -> rewrite term_list rev h h1opt)
let _ = wrap_and_register let _ = wrap_and_register
~desc:"rewrite_list [<-] <list name> [?] [in] <name2> rewrites equalities defined in <list name> into name2. If [?] is set, each of the rewrites is optional." "rewrite_list" ~desc:"rewrite_list [<-] <name list> [?] [in] <name2>@ \
(Toptbool ("<-", (Tprlist (Toptbool ("?", Topt ("in", Tprsymbol Ttrans_l)))))) (fun rev hl opt h1opt -> rewrite_list rev opt hl h1opt) rewrites@ equalities@ defined@ in@ the@ given@ list@ \
of@ premises@ into@ <name2>.@ If@ [?]@ is@ set,@ each@ \
of@ the@ rewrites@ is@ optional."
"rewrite_list"
(Toptbool ("<-", (Tprlist (Toptbool ("?",
Topt ("in", Tprsymbol Ttrans_l))))))
(fun rev hl opt h1opt -> rewrite_list rev opt hl h1opt)
let () = wrap_and_register let () = wrap_and_register
~desc:"apply <prop> [with] <list term> applies prop to the goal and \ ~desc:"apply <prop> [with] <term list>@ \
uses the list of terms to instantiate the variables that are not found." "apply" applies@ premise@ <prop>@ to@ the@ goal@ and@ uses@ the@ \
(Tprsymbol (Topt ("with", Ttermlist Ttrans_l))) (fun x y -> apply x y) list@ of@ terms@ to@ instantiate@ the@ variables@ that@ \
are@ not@ found."
"apply"
(Tprsymbol (Topt ("with", Ttermlist Ttrans_l)))
apply
...@@ -152,27 +152,36 @@ let introduce_premises n = Trans.goal (intros (create_list n)) ...@@ -152,27 +152,36 @@ let introduce_premises n = Trans.goal (intros (create_list n))
let intros_list l = Trans.goal (intros l) let intros_list l = Trans.goal (intros l)
let () = wrap_and_register let () = wrap_and_register
~desc:"case <term> [name] generates hypothesis 'name: term' in a first goal and 'name: ~ term' in a second one." ~desc:"case <term> [name]@ generates@ hypothesis@ 'name: term'@ \
in@ a@ first@ goal@ and@ 'name: ~ term'@ in@ a@ second@ one."
"case" "case"
(Tformula (Topt ("as",Tstring Ttrans_l))) case (Tformula (Topt ("as",Tstring Ttrans_l))) case
let () = wrap_and_register ~desc:"left transform a disjunctive goal A \\/ B into A" let () = wrap_and_register
~desc:"left@ transforms@ a@ disjunctive@ goal@ A \\/ B@ into@ A."
"left" "left"
(Ttrans) (or_intro true) (Ttrans) (or_intro true)
let () = wrap_and_register ~desc:"right transform a disjunctive goal A \\/ B into B" let () = wrap_and_register
~desc:"right@ transforms@ a@ disjunctive@ goal@ A \\/ B@ into@ B."
"right" "right"
(Ttrans) (or_intro false) (Ttrans) (or_intro false)
let () = wrap_and_register let () = wrap_and_register
~desc:"exists <term> substitutes the existentially quantified variable with the given term" ~desc:"exists <term>@ substitutes@ the@ top-most@ existentially@ \
quantified@ variable@ with@ the@ given@ term."
"exists" "exists"
(Tterm Ttrans) exists (Tterm Ttrans) exists
let () = wrap_and_register ~desc:"intros n introduces the first n quantified variables and hypotheses" let () = wrap_and_register
~desc:"intros <n>@ introduces@ the@ first@ <n>@ quantified@ \
variables@ and@ hypotheses."
"intros_n" "intros_n"
(Tint Ttrans) introduce_premises (Tint Ttrans) introduce_premises
let () = wrap_and_register ~desc:"intros id1,id2,...,idk introduces quantified variables and hypotheses using the given identifiers names" let () = wrap_and_register
~desc:"intros <id1>,<id2>,...,<idk>@ \
introduces@ quantified@ variables@ and@ hypotheses@ under@ \
the\ given@ names."
"intros" "intros"
(Tidentlist Ttrans) intros_list (Tidentlist Ttrans) intros_list
...@@ -22,7 +22,7 @@ let meta_rewrite_def = Theory.register_meta "rewrite_def" [Theory.MTlsymbol] ...@@ -22,7 +22,7 @@ let meta_rewrite_def = Theory.register_meta "rewrite_def" [Theory.MTlsymbol]
let meta_compute_max_steps = Theory.register_meta_excl "compute_max_steps" let meta_compute_max_steps = Theory.register_meta_excl "compute_max_steps"
[Theory.MTint] [Theory.MTint]
~desc:"Maximal@ number@ of@ reduction@ steps@ done@ by@ compute@ \ ~desc:"Maximal@ number@ of@ reduction@ steps@ done@ by@ the@ 'compute'@ \
transformation" transformation"
let compute_max_steps = ref 1024 let compute_max_steps = ref 1024
...@@ -116,12 +116,13 @@ let normalize_goal_transf_few env = ...@@ -116,12 +116,13 @@ let normalize_goal_transf_few env =
let () = let () =
Trans.register_env_transform_l "compute_in_goal" normalize_goal_transf_all Trans.register_env_transform_l "compute_in_goal" normalize_goal_transf_all
~desc:"Performs@ possible@ computations@ in@ goal, including@ by@ \ ~desc:"Perform@ computations@ in@ the@ goal,@ also@ using@ \
declared@ rewrite@ rules" the@ automatically@ derived@ rules)."
let () = let () =
Trans.register_env_transform_l "compute_specified" normalize_goal_transf_few Trans.register_env_transform_l "compute_specified" normalize_goal_transf_few
~desc:"Rewrite@ goal@ using@ specified@ rules" ~desc:"Perform@ computations@ in@ the@ goal,@ only@ using@ \
the@ user-specified@ rules)."
let normalize_hyp step_limit pr_norm env = let normalize_hyp step_limit pr_norm env =
let p = { compute_defs = true; let p = { compute_defs = true;
...@@ -130,19 +131,24 @@ let normalize_hyp step_limit pr_norm env = ...@@ -130,19 +131,24 @@ let normalize_hyp step_limit pr_norm env =
} in } in
normalize_goal_transf ?pr_norm ?step_limit p env normalize_goal_transf ?pr_norm ?step_limit p env
let () = wrap_and_register ~desc:"experimental: Takes a prsymbol and reduce \ let () = wrap_and_register
one \"elementary\" step." ~desc:"step [in] <name>@ performs@ one@ \"elementary\"@ \
reduction@ step@ in@ the@ given@ premise@ (experimental)."
"step" "step"
(Topt ("in", Tprsymbol Tenvtrans_l)) (normalize_hyp (Some 1)) (Topt ("in", Tprsymbol Tenvtrans_l))
(normalize_hyp (Some 1))
let () = wrap_and_register ~desc:"experimental: Same as step except that it \ let () = wrap_and_register
reduces the given number of steps." ~desc:"steps <n> [in] <name>@ performs@ <n>@ \"elementary\"@ \
reduction@ steps@ in@ the@ given@ premise@ (experimental)."
"steps" "steps"
(Tint (Topt ("in", Tprsymbol Tenvtrans_l))) (fun n -> normalize_hyp (Some n)) (Tint (Topt ("in", Tprsymbol Tenvtrans_l)))
(fun n -> normalize_hyp (Some n))
let () = wrap_and_register
let () = wrap_and_register ~desc:"Performs@ possible@ computations@ in@ given \ ~desc:"compute_hyp [in] <name>@ performs@ computations@ \
hypothesis@ including@ by@ declared@ rewrite@ rules" in@ the@ given@ premise, also@ using@ the@ automatically@ \
derived@ rules."
"compute_hyp" "compute_hyp"
(Topt ("in", Tprsymbol Tenvtrans_l)) (normalize_hyp None) (Topt ("in", Tprsymbol Tenvtrans_l)) (normalize_hyp None)
...@@ -153,8 +159,9 @@ let normalize_hyp_few step_limit pr_norm env = ...@@ -153,8 +159,9 @@ let normalize_hyp_few step_limit pr_norm env =
} in } in
normalize_goal_transf ?pr_norm ?step_limit p env normalize_goal_transf ?pr_norm ?step_limit p env
let () = wrap_and_register ~desc:"Performs@ possible@ computations@ in@ given \ let () = wrap_and_register
hypothesis@ using@ specified@ rules" ~desc:"compute_hyp_specified [in] <name>@ performs@ computations@ \
in@ the@ given@ premise, only@ using@ the@ user-specified@ rules."
"compute_hyp_specified" "compute_hyp_specified"
(Topt ("in", Tprsymbol Tenvtrans_l)) (normalize_hyp_few None) (Topt ("in", Tprsymbol Tenvtrans_l)) (normalize_hyp_few None)
......
...@@ -178,43 +178,53 @@ let hide (clear: bool) (name: string) (t: term) = ...@@ -178,43 +178,53 @@ let hide (clear: bool) (name: string) (t: term) =
Trans.bind_comp (pose clear name t) Trans.bind_comp (pose clear name t)
(fun (hyp,new_constant,ls_term) -> replace_all hyp new_constant ls_term) (fun (hyp,new_constant,ls_term) -> replace_all hyp new_constant ls_term)
let () = wrap_and_register ~desc:"clear all axioms but the hypothesis argument" let () = wrap_and_register
~desc:"clear_but <name list>@ \
clears@ all@ premises@ except@ the@ listed@ ones."
"clear_but" "clear_but"
(Tprlist Ttrans) clear_but (Tprlist Ttrans) clear_but
let () = wrap_and_register let () = wrap_and_register
~desc:"cut <term> [name] makes a cut with hypothesis 'name: term'" ~desc:"cut <term> [name]@ \
makes@ a@ cut@ with@ a@ hypothesis@ 'name: term'."
"cut" "cut"
(Tformula (Topt ("as",Tstring Ttrans_l))) cut (Tformula (Topt ("as",Tstring Ttrans_l))) cut
let () = wrap_and_register let () = wrap_and_register
~desc:"cut <term> [name] makes an assert with hypothesis 'name: term'" ~desc:"assert <term> [name]@ \
makes@ an@ assertion@ with@ a@ hypothesis@ 'name: term'."
"assert" "assert"
(Tformula (Topt ("as",Tstring Ttrans_l))) assert_tac (Tformula (Topt ("as",Tstring Ttrans_l))) assert_tac
let () = wrap_and_register let () = wrap_and_register
~desc:"remove <prop list>: removes a list of hypothesis given by their names separated with ','. Example: remove_list a,b,c " ~desc:"remove <name list>@ removes@ the@ listed@ premises."
"remove" "remove"
(Tlist Ttrans) (fun l -> remove_list l) (Tlist Ttrans) (fun l -> remove_list l)
let () = wrap_and_register let () = wrap_and_register
~desc:"use_th <theory> imports the theory" "use_th" ~desc:"use_th <theory>@ imports@ the@ given@ theory."
"use_th"
(Ttheory Ttrans) use_th (Ttheory Ttrans) use_th
let pose (name: string) (t: term) = let pose (name: string) (t: term) =
Trans.bind (pose false name t) (fun (_, task) -> Trans.store (fun _ -> task)) Trans.bind (pose false name t) (fun (_, task) -> Trans.store (fun _ -> task))
let () = wrap_and_register let () = wrap_and_register
~desc:"pose <name> <term> adds a new constant <name> equal to <term>" ~desc:"pose <name> <term>@ \
adds@ a@ new@ constant@ <name>@ equal@ to@ <term>."
"pose" "pose"
(Tstring (Tterm Ttrans)) pose (Tstring (Tterm Ttrans)) pose
let () = wrap_and_register let () = wrap_and_register
~desc:"hide <name> <term> adds a new constant <name> equal to <term> and replace everywhere the term with the new constant." ~desc:"hide <name> <term>@ \
adds@ a@ new@ constant@ <name>@ equal@ to@ <term>@ \
and@ replaces@ everywhere@ the@ term@ with@ the@ new@ constant."
"hide" "hide"
(Tstring (Tterm Ttrans)) (hide false) (Tstring (Tterm Ttrans)) (hide false)
let () = wrap_and_register let () = wrap_and_register
~desc:"hide and clear <name> <term> adds a new constant <name> which replaces all occurences of <term>." ~desc:"hide_and_clear <name> <term>@ \
adds@ a@ new constant@ <name>@ which@ replaces@ all@ \
occurences@ of@ <term>."
"hide_and_clear" "hide_and_clear"
(Tstring (Tterm Ttrans)) (hide true) (Tstring (Tterm Ttrans)) (hide true)
...@@ -414,25 +414,50 @@ let instantiate ~rem (pr: Decl.prsymbol) lt = ...@@ -414,25 +414,50 @@ let instantiate ~rem (pr: Decl.prsymbol) lt =
| _ -> [d]) None | _ -> [d]) None
let () = wrap_and_register let () = wrap_and_register
~desc:"instantiate <prop> <term list> generates a new hypothesis with quantified variables of prop replaced with terms" ~desc:"instantiate <prop> <term list>@ \
generates@ a@ new@ hypothesis@ with@ quantified@ variables@ \
of@ <prop>@ replaced@ with@ the@ given@ terms."
"instantiate" "instantiate"
(Tprsymbol (Ttermlist Ttrans)) (instantiate ~rem:false) (Tprsymbol (Ttermlist Ttrans)) (instantiate ~rem:false)
let () = wrap_and_register let () = wrap_and_register
~desc:"instantiate <prop> <term list> generates a new hypothesis with quantified variables of prop replaced with terms. Also remove the old hypothesis." ~desc:"instantiate <prop> <term list>@ \
generates@ a@ new@ hypothesis@ with@ quantified@ variables@ \
of@ <prop>@ replaced@ with@ then@ given@ terms.@ \
Also@ removes@ the@ old@ hypothesis."
"inst_rem" "inst_rem"
(Tprsymbol (Ttermlist Ttrans)) (instantiate ~rem:true) (Tprsymbol (Ttermlist Ttrans)) (instantiate ~rem:true)
let () = wrap_and_register ~desc:"destruct <name> destructs the head logic constructor of hypothesis name (/\\, \\/, -> or <->).\nTo destruct a literal of algebraic type, use destruct_term." let () = wrap_and_register
~desc:"destruct <name>@ \
destructs@ the@ top-most@ propositional@ connector@ \
(/\\,@ \\/,@ ->@ or@ <->)@ of@ the@ given@ hypothesis.@ \
To@ destruct@ a@ literal@ of@ an@ algebraic@ type,@ \
use@ 'destruct_term'."
"destruct" (Tprsymbol Ttrans_l) (destruct ~recursive:false) "destruct" (Tprsymbol Ttrans_l) (destruct ~recursive:false)
let () = wrap_and_register ~desc:"destruct <name> recursively destructs the head logic constructor of hypothesis name (/\\, \\/, -> or <->).\nTo destruct a literal of algebraic type, use destruct_term." let () = wrap_and_register
~desc:"destruct_rec <name>@ \
recursively@ destructs@ the@ top@ propositional@ connectors@ \
(/\\,@ \\/,@ ->@ or@ <->)@ of@ the@ given@ hypothesis.@ \
To@ destruct@ a@ literal@ of@ an@ algebraic@ type,@ \
use@ 'destruct_term'."
"destruct_rec" (Tprsymbol Ttrans_l) (destruct ~recursive:true) "destruct_rec" (Tprsymbol Ttrans_l) (destruct ~recursive:true)
let () = wrap_and_register ~desc:"destruct <name> as an algebraic type. Option using can be used to name elements created by destruct_term" let () = wrap_and_register
~desc:"destruct_term <term> [using] <id list>@ \
destructs@ the@ given@ term@ of@ an@ algebraic@ type.@ \
Option@ 'using'@ can@ be@ used@ to@ name@ the@ elements@ \
created@ by@ 'destruct_term'."
"destruct_term" (Tterm (Topt ("using", Tidentlist Ttrans_l))) "destruct_term" (Tterm (Topt ("using", Tidentlist Ttrans_l)))
(fun t names -> destruct_term ?names false t) (fun t names -> destruct_term ?names false t)
let () = wrap_and_register ~desc:"destruct <name> as an algebraic type and substitute the definition if an lsymbol was provided. Option using can be used to name elements created by destruct_term_subst" let () = wrap_and_register
~desc:"destruct_term_subst <term> [using] <id list>@ \
destructs@ the@ given@ term@ of@ an@ algebraic@ type@ \
and@ substitutes@ the@ definition@ if@ the@ term@ is@ \
a@ constant@ function@ symbol.@ \
Option@ 'using'@ can@ be@ used@ to@ name@ the@ elements@ \
created@ by@ 'destruct_term_subst'."
"destruct_term_subst" (Tterm (Topt ("using", Tidentlist Ttrans_l))) "destruct_term_subst" (Tterm (Topt ("using", Tidentlist Ttrans_l)))
(fun t names -> destruct_term ?names true t) (fun t names -> destruct_term ?names true t)
...@@ -141,7 +141,7 @@ let eliminate_if = Trans.compose eliminate_if_term eliminate_if_fmla ...@@ -141,7 +141,7 @@ let eliminate_if = Trans.compose eliminate_if_term eliminate_if_fmla
let () = let () =
Trans.register_transform "eliminate_if_term" eliminate_if_term Trans.register_transform "eliminate_if_term" eliminate_if_term
~desc:"Replaces@ terms@ of@ the@ form@ [if f1 then t2 else t3]@ by@ \ ~desc:"Replace@ terms@ of@ the@ form@ [if f1 then t2 else t3]@ by@ \
lifting@ them@ at@ the@ level@ of@ formulas."; lifting@ them@ at@ the@ level@ of@ formulas.";
Trans.register_transform "eliminate_if_fmla" eliminate_if_fmla Trans.register_transform "eliminate_if_fmla" eliminate_if_fmla
~desc:"Eliminate@ formulas@ of@ the@ form@ [if f1 then f2 else f3]."; ~desc:"Eliminate@ formulas@ of@ the@ form@ [if f1 then f2 else f3].";
......
...@@ -96,4 +96,4 @@ let remove_types = ...@@ -96,4 +96,4 @@ let remove_types =
let () = let () =
Trans.register_transform "eliminate_unknown_types" remove_types Trans.register_transform "eliminate_unknown_types" remove_types
~desc:"Remove@ types@ unknown@ to@ the@ prover@ and@ terms@ referring@ to@ them@." ~desc:"Remove@ types@ unknown@ to@ the@ prover@ and@ terms@ referring@ to@ them."
...@@ -74,7 +74,8 @@ let encoding_smt env = Trans.seq [ ...@@ -74,7 +74,8 @@ let encoding_smt env = Trans.seq [
Libencoding.monomorphise_goal; Libencoding.monomorphise_goal;
select_kept def_enco_select_smt env; select_kept def_enco_select_smt env;
Trans.print_meta Libencoding.debug Libencoding.meta_kept; Trans.print_meta Libencoding.debug Libencoding.meta_kept;
Trans.trace_goal "meta_enco_kept" (Trans.on_flag meta_enco_kept ft_enco_kept def_enco_kept_smt env); Trans.trace_goal "meta_enco_kept"
(Trans.on_flag meta_enco_kept ft_enco_kept def_enco_kept_smt env);
Trans.on_flag meta_enco_poly ft_enco_poly def_enco_poly_smt env] Trans.on_flag meta_enco_poly ft_enco_poly def_enco_poly_smt env]
let encoding_tptp env = Trans.seq [ let encoding_tptp env = Trans.seq [
...@@ -100,7 +101,7 @@ let encoding_smt_if_poly env = ...@@ -100,7 +101,7 @@ let encoding_smt_if_poly env =
let () = let () =
Trans.register_env_transform "encoding_smt_if_poly" Trans.register_env_transform "encoding_smt_if_poly"
encoding_smt_if_poly encoding_smt_if_poly
~desc:"Same@ as@ encoding_smt@ but@ only@ if@ polymorphism@ appear." ~desc:"Same@ as@ encoding_smt@ but@ only@ in@ presence@ of@ polymorphism."
let encoding_tptp_if_poly env = let encoding_tptp_if_poly env =
Trans.on_meta Detect_polymorphism.meta_monomorphic_types_only Trans.on_meta Detect_polymorphism.meta_monomorphic_types_only
...@@ -111,4 +112,4 @@ let encoding_tptp_if_poly env = ...@@ -111,4 +112,4 @@ let encoding_tptp_if_poly env =
let () = let () =
Trans.register_env_transform "encoding_tptp_if_poly" Trans.register_env_transform "encoding_tptp_if_poly"
encoding_tptp_if_poly encoding_tptp_if_poly
~desc:"Same@ as@ encoding_tptp@ but@ only@ if@ polymorphism@ appear." ~desc:"Same@ as@ encoding_tptp@ but@ only@ in@ presence@ of@ polymorphism."
...@@ -301,11 +301,15 @@ let induction x bound env = ...@@ -301,11 +301,15 @@ let induction x bound env =
Trans.par [init_trans; rec_trans] Trans.par [init_trans; rec_trans]
let () = wrap_and_register let () = wrap_and_register
~desc:"induction <term1> [from] <term2> performs a strong induction on int term1 from int term2. term2 is optional and default to 0." ~desc:"induction <term1> [from] <term2>@ \
performs@ a@ strong@ induction@ on@ the@ integer@ <term1>@ \
starting@ from@ the@ integer@ <term2>.@ <term2>@ is@ optional@ \
and@ defaults@ to@ 0."
"induction" "induction"
(Tterm (Topt ("from", Tterm Tenvtrans_l))) induction (Tterm (Topt ("from", Tterm Tenvtrans_l))) induction
let () = wrap_and_register let () = wrap_and_register
~desc:"revert <list> puts list back in the goal." ~desc:"revert <id list>@ \
puts@ the@ given@ identifiers@ back@ in@ the@ goal."
"revert" "revert"
(Tlist Ttrans) revert_tr_symbol (Tlist Ttrans) revert_tr_symbol
...@@ -352,7 +352,8 @@ let induction_on_hyp ls = ...@@ -352,7 +352,8 @@ let induction_on_hyp ls =
(Trans.store induction_ty_lex) (Trans.store induction_ty_lex)
let () = wrap_and_register let () = wrap_and_register
~desc:"induction_arg_ty_lex <ls> performs induction_ty_lex on ls." ~desc:"induction_arg_ty_lex <id>@ \
performs@ 'induction_ty_lex'@ on@ the@ given@ logical@ symbol."
"induction_arg_ty_lex" "induction_arg_ty_lex"
(Tlsymbol Ttrans_l) induction_on_hyp (Tlsymbol Ttrans_l) induction_on_hyp
......
...@@ -219,7 +219,8 @@ let induction_l attr induct task = match task with ...@@ -219,7 +219,8 @@ let induction_l attr induct task = match task with
| Some { task_decl ={ td_node = Decl { d_node = Dprop (Pgoal, pr, f) } }; | Some { task_decl ={ td_node = Decl { d_node = Dprop (Pgoal, pr, f) } };
task_prev = prev; task_prev = prev;
task_known = kn } -> task_known = kn } ->
begin try List.map (add_prop_decl prev Pgoal pr) (induction_l attr induct kn f) begin try List.map (add_prop_decl prev Pgoal pr)
(induction_l attr induct kn f)
with Ind_not_found -> [task] end with Ind_not_found -> [task] end
| _ -> assert false | _ -> assert false
...@@ -228,26 +229,24 @@ let induction_on_hyp attr b h = ...@@ -228,26 +229,24 @@ let induction_on_hyp attr b h =
(Trans.store (induction_l attr b)) (Trans.store (induction_l attr b))
let () = wrap_and_register let () = wrap_and_register
~desc:"induction_arg_pr <pr> performs induction_pr on pr." ~desc:"induction_arg_pr <name>@ \
performs@ 'induction_pr'@ on@ the@ given@ premise."
"induction_arg_pr" "induction_arg_pr"
(Tprsymbol Ttrans_l) (induction_on_hyp attr_ind true) (Tprsymbol Ttrans_l) (induction_on_hyp attr_ind true)
let () = wrap_and_register let () = wrap_and_register
~desc:"induction_arg_pr <pr> performs inversion_pr on pr." ~desc:"inversion_arg_pr <name>@ \
performs@ 'inversion_pr'@ on@ the@ given@ premise."
"inversion_arg_pr" "inversion_arg_pr"
(Tprsymbol Ttrans_l) (induction_on_hyp attr_inv false) (Tprsymbol Ttrans_l) (induction_on_hyp attr_inv false)
let () = let () =
Trans.register_transform_l "induction_pr" (Trans.store (induction_l attr_ind true)) Trans.register_transform_l "induction_pr"
~desc:"Generate@ induction@ hypotheses@ for@ goals@ over@ inductive@ predicates." (Trans.store (induction_l attr_ind true))
~desc:"Generate@ induction@ hypotheses@ \
for@ goals@ over@ inductive@ predicates."
let () = let () =
Trans.register_transform_l "inversion_pr" (Trans.store (induction_l attr_inv false)) Trans.register_transform_l "inversion_pr"
(Trans.store (induction_l attr_inv false))
~desc:"Invert@ inductive@ predicate." ~desc:"Invert@ inductive@ predicate."
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. bin/why3.byte"
End:
*)
...@@ -150,4 +150,4 @@ let () = ...@@ -150,4 +150,4 @@ let () =
~desc:"Same@ as@ 'inline_all', but@ only@ inline in@ goals."; ~desc:"Same@ as@ 'inline_all', but@ only@ inline in@ goals.";
Trans.register_transform "inline_trivial" trivial Trans.register_transform "inline_trivial" trivial
~desc:"Inline@ trivial@ definitions@ like@ @[f(x,y) = g(y,x,0)@]. \ ~desc:"Inline@ trivial@ definitions@ like@ @[f(x,y) = g(y,x,0)@]. \
Add@ the@ \"inline:trivial\"@ attribute@ to@ force@ inlining." Add@ the@ [@@inline:trivial]@ attribute@ to@ force@ inlining."
...@@ -231,5 +231,5 @@ let () = Trans.register_env_transform "intro_projections_counterexmp" ...@@ -231,5 +231,5 @@ let () = Trans.register_env_transform "intro_projections_counterexmp"
intro_projections_counterexmp intro_projections_counterexmp
~desc:"For@ each@ declared@ abstract@ function@ and@ predicate@ p@ \ ~desc:"For@ each@ declared@ abstract@ function@ and@ predicate@ p@ \
with@ attribute@ [%@model_projected]@ and@ projecting@ f@ \ with@ attribute@ [%@model_projected]@ and@ projecting@ f@ \
for@ p@ creates@ declaration@ of@ new@ constant@ c@ with@ \ for@ p,@ create@ declaration@ of@ new@ constant@ c@ with@ \
attribute@ [%@model]@ and@ an@ axiom@ c = f p." attribute@ [%@model]@ and@ an@ axiom@ c = f p."
...@@ -34,6 +34,6 @@ let prepare_for_counterexmp env = Trans.store (prepare_for_counterexmp2 env) ...@@ -34,6 +34,6 @@ let prepare_for_counterexmp env = Trans.store (prepare_for_counterexmp2 env)
let () = Trans.register_env_transform "prepare_for_counterexmp" let () = Trans.register_env_transform "prepare_for_counterexmp"
prepare_for_counterexmp prepare_for_counterexmp
~desc:"Transformation@ that@ prepares@ the@ task@ for@ querying@ for@ \ ~desc:"Prepare@ the@ task@ for@ querying@ for@ \
the@ counter-example@ model.@ This@ transformation@ does@ so@ only@ \ the@ counter-example@ model.@ This@ transformation@ does@ so@ only@ \
when@ the@ solver@ will@ be@ asked@ for@ the@ counter-example." when@ the@ solver@ w