| GrafiteAst.Split _ -> Tactics.split
| GrafiteAst.Symmetry _ -> Tactics.symmetry
| GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term
+ (* Implementazioni Aggiunte *)
+ | GrafiteAst.Assume (_, id, t) -> Declarative.assume id t
+ | GrafiteAst.Suppose (_, t, id) -> Declarative.suppose t id
+ | GrafiteAst.By_term_we_proved (_, t, ty, id) ->
+ Declarative.by_term_we_proved t ty id
+ | GrafiteAst.We_need_to_prove (_, t, id) -> Declarative.we_need_to_prove t id
+ | GrafiteAst.Bydone (_, t) -> Declarative.bydone t
(* maybe we only need special cases for apply and goal *)
let classify_tactic tactic =
let eval_coercion status ~add_composites uri =
let status,compounds =
GrafiteSync.add_coercion ~add_composites refinement_toolkit status uri in
- let moo_content = coercion_moo_statement_of uri in
- let status = GrafiteTypes.add_moo_content [moo_content] status in
+ let moo_content =
+ List.map coercion_moo_statement_of (uri::compounds)
+ in
+ let status = GrafiteTypes.add_moo_content moo_content status in
{status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
compounds
let obj,_ =
CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in
let attrs = CicUtil.attributes_of_obj obj in
- List.mem (`Class `Projection) attrs
+ List.mem (`Class `Coercion) attrs
with Not_found -> assert false
in
(* looking at the fields we can know the 'wanted' coercions, but not the
| _ -> None)
fields
in
- (*
- prerr_endline "wanted coercions:";
+ (*prerr_endline "wanted coercions:";
List.iter
(fun u -> prerr_endline (UriManager.string_of_uri u))
wanted_coercions; *)
(HExtlib.filter_map
(fun uri ->
let is_a_wanted_coercion =
- List.exists (UriManager.eq uri) wanted_coercions in
- if is_a_coercion uri && is_a_wanted_coercion then
+ List.exists (UriManager.eq uri) wanted_coercions
+ in
+ if is_a_coercion uri || is_a_wanted_coercion then
Some (uri, coercion_moo_statement_of uri)
else
None)
lemmas)
in
- (* prerr_endline "actual coercions:";
+ (*prerr_endline "actual coercions:";
+ List.iter
+ (fun u -> prerr_endline (UriManager.string_of_uri u))
+ coercions;
+ prerr_endline "lemmas was:";
List.iter
(fun u -> prerr_endline (UriManager.string_of_uri u))
- coercions; *)
+ lemmas; *)
let status = GrafiteTypes.add_moo_content moo_content status in
{status with
GrafiteTypes.coercions = coercions @ status.GrafiteTypes.coercions},