open Printf
exception Drop
-exception IncludedFileNotCompiled of string (* file name *)
+(* mo file name, ma file name *)
+exception IncludedFileNotCompiled of string * string
exception Macro of
GrafiteAst.loc *
(Cic.context -> GrafiteTypes.status * Cic.term GrafiteAst.macro)
match ast with
| GrafiteAst.Absurd (_, term) -> Tactics.absurd term
| GrafiteAst.Apply (_, term) -> Tactics.apply term
+ | GrafiteAst.ApplyS (_, term) ->
+ Tactics.applyS ~term ~dbd:(LibraryDb.instance ())
| GrafiteAst.Assumption _ -> Tactics.assumption
- | GrafiteAst.Auto (_,depth,width,paramodulation,full) ->
- AutoTactic.auto_tac ?depth ?width ?paramodulation ?full
- ~dbd:(LibraryDb.instance ()) ()
+ | GrafiteAst.Auto (_,params) ->
+ AutoTactic.auto_tac ~params ~dbd:(LibraryDb.instance ())
| GrafiteAst.Change (_, pattern, with_what) ->
Tactics.change ~pattern with_what
| GrafiteAst.Clear (_,id) -> Tactics.clear id
let user_types = List.rev_map to_type types in
let dbd = LibraryDb.instance () in
let mk_fresh_name_callback = namer_of names in
- Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types what
+ Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types ?what
+ | GrafiteAst.Demodulate _ -> Tactics.demodulate ~dbd:(LibraryDb.instance ())
| GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term
| GrafiteAst.Elim (_, what, using, depth, names) ->
Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
| GrafiteAst.Fold (_, reduction_kind, term, pattern) ->
let reduction =
match reduction_kind with
- | `Demodulate ->
- GrafiteTypes.command_error "demodulation can't be folded"
| `Normalize ->
PET.const_lazy_reduction
(CicReduction.normalize ~delta:false ~subst:[])
~mk_fresh_name_callback:(namer_of names) ()
| GrafiteAst.Inversion (_, term) ->
Tactics.inversion term
- | GrafiteAst.LApply (_, how_many, to_what, what, ident) ->
+ | GrafiteAst.LApply (_, linear, how_many, to_what, what, ident) ->
let names = match ident with None -> [] | Some id -> [id] in
- Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many
- ~to_what what
+ Tactics.lapply ~mk_fresh_name_callback:(namer_of names)
+ ~linear ?how_many ~to_what what
| GrafiteAst.Left _ -> Tactics.left
| GrafiteAst.LetIn (loc,term,name) ->
Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
| GrafiteAst.Reduce (_, reduction_kind, pattern) ->
(match reduction_kind with
- | `Demodulate -> Tactics.demodulate ~dbd:(LibraryDb.instance ()) ~pattern
| `Normalize -> Tactics.normalize ~pattern
| `Reduce -> Tactics.reduce ~pattern
| `Simpl -> Tactics.simpl ~pattern
| 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
MatitaTacticals.solve_tactics
~tactics:(List.map (fun t -> "", tactical_of_ast (l+1) t) tacticals)
- | GrafiteAst.Skip loc -> MatitaTacticals.skip
- | GrafiteAst.Dot loc -> MatitaTacticals.dot
- | GrafiteAst.Semicolon loc -> MatitaTacticals.semicolon
- | GrafiteAst.Branch loc -> MatitaTacticals.branch
- | GrafiteAst.Shift loc -> MatitaTacticals.shift
- | GrafiteAst.Pos (loc, i) -> MatitaTacticals.pos i
- | GrafiteAst.Merge loc -> MatitaTacticals.merge
- | GrafiteAst.Focus (loc, goals) -> MatitaTacticals.focus goals
- | GrafiteAst.Unfocus loc -> MatitaTacticals.unfocus
+ | GrafiteAst.Skip _loc -> MatitaTacticals.skip
+ | GrafiteAst.Dot _loc -> MatitaTacticals.dot
+ | GrafiteAst.Semicolon _loc -> MatitaTacticals.semicolon
+ | GrafiteAst.Branch _loc -> MatitaTacticals.branch
+ | GrafiteAst.Shift _loc -> MatitaTacticals.shift
+ | GrafiteAst.Pos (_loc, i) -> MatitaTacticals.pos i
+ | GrafiteAst.Merge _loc -> MatitaTacticals.merge
+ | GrafiteAst.Focus (_loc, goals) -> MatitaTacticals.focus goals
+ | GrafiteAst.Unfocus _loc -> MatitaTacticals.unfocus
+ | GrafiteAst.Wildcard _loc -> MatitaTacticals.wildcard
in
let status, _, _ = tactical_of_ast 0 tac (status, ~-1) in
let status = (* is proof completed? *)
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},
let moopath =
if Sys.file_exists moopath_r then moopath_r else
if Sys.file_exists moopath_rw then moopath_rw else
- raise (IncludedFileNotCompiled moopath_rw)
+ raise (IncludedFileNotCompiled (moopath_rw,baseuri))
in
let status = eval_from_moo.efm_go status moopath in
status,[]