(* grafite ast constructors *************************************************)
+(*
let floc = H.dummy_floc
let mk_note str = G.Comment (floc, G.Note (floc, str))
render_steps sep (render_step (Some mk_dot) a p) ps
let render_steps a = render_steps None a
+*)
+let render_steps sep a = assert false
(* counting *****************************************************************)
| `Whd ]
type ('term, 'lazy_term, 'reduction, 'ident) tactic =
+ (* Higher order tactics (i.e. tacticals) *)
+ | Do of loc * int * ('term, 'lazy_term, 'reduction, 'ident) tactic
+ | Repeat of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic
+ | Seq of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic list
+ (* sequential composition *)
+ | Then of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic *
+ ('term, 'lazy_term, 'reduction, 'ident) tactic list
+ | First of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic list
+ (* try a sequence of loc * tactic until one succeeds, fail otherwise *)
+ | Try of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic
+ (* try a tactic and mask failures *)
+ | Solve of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic list
+ | Progress of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic
+ (* Real tactics *)
| Absurd of loc * 'term
| Apply of loc * 'term
| ApplyS of loc * 'term * (string * string) list
| Fourier of loc
| FwdSimpl of loc * string * 'ident list
| Generalize of loc * ('term, 'lazy_term, 'ident) pattern * 'ident option
- | Goal of loc * int (* change current goal, argument is goal number 1-based *)
| IdTac of loc
| Intros of loc * int option * 'ident list
| Inversion of loc * 'term
| Print of loc * string
| Qed of loc
-type ('term, 'lazy_term, 'reduction, 'ident) tactical =
- | Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic
- | Do of loc * int * ('term, 'lazy_term, 'reduction, 'ident) tactical
- | Repeat of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical
- | Seq of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical list
- (* sequential composition *)
- | Then of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical *
- ('term, 'lazy_term, 'reduction, 'ident) tactical list
- | First of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical list
- (* try a sequence of loc * tactical until one succeeds, fail otherwise *)
- | Try of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical
- (* try a tactical and mask failures *)
- | Solve of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical list
- | Progress of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical
-
+type ('term, 'lazy_term, 'reduction, 'ident) punctuation_tactical =
| Dot of loc
| Semicolon of loc
| Branch of loc
| Pos of loc * int list
| Wildcard of loc
| Merge of loc
+
+type ('term,'lazy_term,'reduction,'ident) non_punctuation_tactical =
| Focus of loc * int list
| Unfocus of loc
| Skip of loc
-let is_punctuation =
- function
- | Dot _ | Semicolon _ | Branch _ | Shift _ | Merge _ | Pos _ -> true
- | _ -> false
-
type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code =
| Command of loc * ('term, 'obj) command
| Macro of loc * 'term macro
- | Tactical of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical
- * ('term, 'lazy_term, 'reduction, 'ident) tactical option(* punctuation *)
+ | Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic option
+ * ('term, 'lazy_term, 'reduction, 'ident) punctuation_tactical
+ | NonPunctuationTactical of loc
+ * ('term, 'lazy_term, 'reduction, 'ident) non_punctuation_tactical
+ * ('term, 'lazy_term, 'reduction, 'ident) punctuation_tactical
type ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment =
| Note of loc * string
let pp_reduction_kind = pp_reduction_kind ~term_pp in
let pp_tactic_pattern = pp_tactic_pattern ~lazy_term_pp ~term_pp in
function
+ (* Higher order tactics *)
+ | Do (_, count, tac) ->
+ sprintf "do %d %s" count (pp_tactic ~term_pp ~lazy_term_pp tac)
+ | Repeat (_, tac) -> "repeat " ^ pp_tactic ~term_pp ~lazy_term_pp tac
+ | Seq (_, tacs) -> pp_tactics ~term_pp ~lazy_term_pp ~sep:"; " tacs
+ | Then (_, tac, tacs) ->
+ sprintf "%s; [%s]" (pp_tactic ~term_pp ~lazy_term_pp tac)
+ (pp_tactics ~term_pp ~lazy_term_pp ~sep:" | " tacs)
+ | First (_, tacs) ->
+ sprintf "tries [%s]" (pp_tactics ~term_pp ~lazy_term_pp ~sep:" | " tacs)
+ | Try (_, tac) -> "try " ^ pp_tactic ~term_pp ~lazy_term_pp tac
+ | Solve (_, tac) ->
+ sprintf "solve [%s]" (pp_tactics ~term_pp ~lazy_term_pp ~sep:" | " tac)
+ | Progress (_, tac) -> "progress " ^ pp_tactic ~term_pp ~lazy_term_pp tac
+ (* First order tactics *)
| Absurd (_, term) -> "absurd" ^ term_pp term
| Apply (_, term) -> "apply " ^ term_pp term
| ApplyS (_, term, params) ->
| Generalize (_, pattern, ident) ->
sprintf "generalize %s%s" (pp_tactic_pattern pattern)
(match ident with None -> "" | Some id -> " as " ^ id)
- | Goal (_, n) -> "goal " ^ string_of_int n
| Fail _ -> "fail"
| Fourier _ -> "fourier"
| IdTac _ -> "id"
(List.map (function (id,term) -> "(" ^ id ^ ": " ^ term_pp term ^ ")")
args)
+and pp_tactics ~term_pp ~lazy_term_pp ~sep tacs =
+ String.concat sep (List.map (pp_tactic ~lazy_term_pp ~term_pp) tacs)
+
let pp_search_kind = function
| `Locate -> "locate"
| `Hint -> "hint"
| Print (_,s) -> "print " ^ s
| Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value
-let rec pp_tactical ~term_pp ~lazy_term_pp =
- let pp_tactic = pp_tactic ~lazy_term_pp ~term_pp in
- let pp_tacticals = pp_tacticals ~lazy_term_pp ~term_pp in
+let pp_punctuation_tactical ~term_pp ~lazy_term_pp =
function
- | Tactic (_, tac) -> pp_tactic tac
- | Do (_, count, tac) ->
- sprintf "do %d %s" count (pp_tactical ~term_pp ~lazy_term_pp tac)
- | Repeat (_, tac) -> "repeat " ^ pp_tactical ~term_pp ~lazy_term_pp tac
- | Seq (_, tacs) -> pp_tacticals ~sep:"; " tacs
- | Then (_, tac, tacs) ->
- sprintf "%s; [%s]" (pp_tactical ~term_pp ~lazy_term_pp tac)
- (pp_tacticals ~sep:" | " tacs)
- | First (_, tacs) -> sprintf "tries [%s]" (pp_tacticals ~sep:" | " tacs)
- | Try (_, tac) -> "try " ^ pp_tactical ~term_pp ~lazy_term_pp tac
- | Solve (_, tac) -> sprintf "solve [%s]" (pp_tacticals ~sep:" | " tac)
- | Progress (_, tac) -> "progress " ^ pp_tactical ~term_pp ~lazy_term_pp tac
-
| Dot _ -> "."
| Semicolon _ -> ";"
| Branch _ -> "["
| Pos (_, i) -> sprintf "%s:" (String.concat "," (List.map string_of_int i))
| Wildcard _ -> "*:"
| Merge _ -> "]"
+
+let pp_non_punctuation_tactical ~term_pp ~lazy_term_pp =
+ function
| Focus (_, goals) ->
sprintf "focus %s" (String.concat " " (List.map string_of_int goals))
| Unfocus _ -> "unfocus"
| Skip _ -> "skip"
-and pp_tacticals ~term_pp ~lazy_term_pp ~sep tacs =
- String.concat sep (List.map (pp_tactical~lazy_term_pp ~term_pp) tacs)
-
let pp_executable ~term_pp ~lazy_term_pp ~obj_pp =
function
| Macro (_, macro) -> pp_macro ~term_pp macro ^ "."
- | Tactical (_, tac, Some punct) ->
- pp_tactical ~lazy_term_pp ~term_pp tac
- ^ pp_tactical ~lazy_term_pp ~term_pp punct
- | Tactical (_, tac, None) -> pp_tactical ~lazy_term_pp ~term_pp tac
+ | Tactic (_, Some tac, punct) ->
+ pp_tactic ~lazy_term_pp ~term_pp tac
+ ^ pp_punctuation_tactical ~lazy_term_pp ~term_pp punct
+ | Tactic (_, None, punct) ->
+ pp_punctuation_tactical ~lazy_term_pp ~term_pp punct
+ | NonPunctuationTactical (_, tac, punct) ->
+ pp_non_punctuation_tactical ~lazy_term_pp ~term_pp tac
+ ^ pp_punctuation_tactical ~lazy_term_pp ~term_pp punct
| Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ ".\n"
let pp_comment ~term_pp ~lazy_term_pp ~obj_pp =
GrafiteAst.statement ->
string
-val pp_tactical:
+val pp_punctuation_tactical:
term_pp:('term -> string) ->
lazy_term_pp:('lazy_term -> string) ->
('term, 'lazy_term, 'term GrafiteAst.reduction, string)
- GrafiteAst.tactical ->
+ GrafiteAst.punctuation_tactical ->
string
end else
FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
-let tactic_of_ast status ast =
+let rec tactic_of_ast status ast =
let module PET = ProofEngineTypes in
match ast with
+ (* Higher order tactics *)
+ | GrafiteAst.Do (loc, n, tactic) ->
+ Tacticals.do_tactic n (tactic_of_ast status tactic)
+ | GrafiteAst.Seq (loc, tactics) -> (* tac1; tac2; ... *)
+ Tacticals.seq (List.map (tactic_of_ast status) tactics)
+ | GrafiteAst.Repeat (loc, tactic) ->
+ Tacticals.repeat_tactic (tactic_of_ast status tactic)
+ | GrafiteAst.Then (loc, tactic, tactics) -> (* tac; [ tac1 | ... ] *)
+ Tacticals.thens
+ (tactic_of_ast status tactic)
+ (List.map (tactic_of_ast status) tactics)
+ | GrafiteAst.First (loc, tactics) ->
+ Tacticals.first (List.map (tactic_of_ast status) tactics)
+ | GrafiteAst.Try (loc, tactic) ->
+ Tacticals.try_tactic (tactic_of_ast status tactic)
+ | GrafiteAst.Solve (loc, tactics) ->
+ Tacticals.solve_tactics (List.map (tactic_of_ast status) tactics)
+ | GrafiteAst.Progress (loc, tactic) ->
+ Tacticals.progress_tactic (tactic_of_ast status tactic)
+ (* First order tactics *)
| GrafiteAst.Absurd (_, term) -> Tactics.absurd term
| GrafiteAst.Apply (_, term) -> Tactics.apply term
| GrafiteAst.ApplyS (_, term, params) ->
| GrafiteAst.Generalize (_,pattern,ident) ->
let names = match ident with None -> [] | Some id -> [id] in
Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern
- | GrafiteAst.Goal (_, n) -> Tactics.set_goal n
| GrafiteAst.IdTac _ -> Tactics.id
| GrafiteAst.Intros (_, None, names) ->
PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
| GrafiteAst.Generalize _
| GrafiteAst.Elim _
| GrafiteAst.Cut _
- | GrafiteAst.Decompose _ -> true, true
- (* tactics we don't want to reorder goals. I think only Goal needs this. *)
- | GrafiteAst.Goal _ -> false, true
+ | GrafiteAst.Decompose _ -> true
(* tactics like apply *)
- | _ -> true, false
+ | _ -> false
let reorder_metasenv start refine tactic goals current_goal always_opens_a_goal=
let module PEH = ProofEngineHelpers in
let metasenv_after_refinement = GrafiteTypes.get_proof_metasenv status in
let proof = GrafiteTypes.get_current_proof status in
let proof_status = proof, goal in
- let needs_reordering, always_opens_a_goal = classify_tactic tactic in
+ let always_opens_a_goal = classify_tactic tactic in
let tactic = tactic_of_ast status tactic in
let (proof, opened) = ProofEngineTypes.apply_tactic tactic proof_status in
let after = ProofEngineTypes.goals_of_proof proof in
let opened_goals, closed_goals = Tacticals.goals_diff ~before ~after ~opened in
let proof, opened_goals =
- if needs_reordering then begin
- let uri, metasenv_after_tactic, t, ty, attrs = proof in
- let reordered_metasenv, opened_goals =
- reorder_metasenv
- starting_metasenv
- metasenv_after_refinement metasenv_after_tactic
- opened goal always_opens_a_goal
- in
- let proof' = uri, reordered_metasenv, t, ty, attrs in
- proof', opened_goals
- end
- else
- proof, opened_goals
+ let uri, metasenv_after_tactic, t, ty, attrs = proof in
+ let reordered_metasenv, opened_goals =
+ reorder_metasenv
+ starting_metasenv
+ metasenv_after_refinement metasenv_after_tactic
+ opened goal always_opens_a_goal
+ in
+ let proof' = uri, reordered_metasenv, t, ty, attrs in
+ proof', opened_goals
in
let incomplete_proof =
match status.GrafiteTypes.proof_status with
let metasenv_after_refinement = GrafiteTypes.get_proof_metasenv status in
let proof = GrafiteTypes.get_current_proof status in
let proof_status = proof, goal in
- let needs_reordering, always_opens_a_goal = classify_tactic tactic in
+ let always_opens_a_goal = classify_tactic tactic in
let tactic = tactic_of_ast status tactic in
let tactic = patch tactic in
let (proof, opened) = ProofEngineTypes.apply_tactic tactic proof_status in
let after = ProofEngineTypes.goals_of_proof proof in
let opened_goals, closed_goals = Tacticals.goals_diff ~before ~after ~opened in
let proof, opened_goals =
- if needs_reordering then begin
- let uri, metasenv_after_tactic, t, ty, attrs = proof in
- let reordered_metasenv, opened_goals =
- reorder_metasenv
- starting_metasenv
- metasenv_after_refinement metasenv_after_tactic
- opened goal always_opens_a_goal
- in
- let proof' = uri, reordered_metasenv, t, ty, attrs in
- proof', opened_goals
- end
- else
- proof, opened_goals
+ let uri, metasenv_after_tactic, t, ty, attrs = proof in
+ let reordered_metasenv, opened_goals =
+ reorder_metasenv
+ starting_metasenv
+ metasenv_after_refinement metasenv_after_tactic
+ opened goal always_opens_a_goal
+ in
+ let proof' = uri, reordered_metasenv, t, ty, attrs in
+ proof', opened_goals
in
let incomplete_proof =
match status.GrafiteTypes.proof_status with
{status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
List.map fst compounds
-let eval_tactical ~disambiguate_tactic status tac =
- let apply_tactic = apply_tactic ~disambiguate_tactic in
- let module MatitaStatus =
- struct
- type input_status = GrafiteTypes.status * ProofEngineTypes.goal
-
- type output_status =
- GrafiteTypes.status * ProofEngineTypes.goal list * ProofEngineTypes.goal list
-
- type tactic = input_status -> output_status
-
- let mk_tactic tac = tac
- let apply_tactic tac = tac
- let goals (_, opened, closed) = opened, closed
- let get_stack (status, _) = GrafiteTypes.get_stack status
-
- let set_stack stack (status, opened, closed) =
- GrafiteTypes.set_stack stack status, opened, closed
-
- let inject (status, _) = (status, [], [])
- let focus goal (status, _, _) = (status, goal)
- end
- in
-(*
- let rec atomic_tactical_of_ast (text,prefix_len,tac) =
- match tac with
- | GrafiteAst.Tactic (loc, tactic) ->
- cic_tactic_of_ast ~disambiguate_tactic (text,prefix_len,tactic)
- (status,~-1)
- | GrafiteAst.Seq (loc,tacticals) ->
- Tacticals.seq
- (List.map atomic_tactical_of_ast
- (List.map (fun x -> text,prefix_len,x) tacticals))
- | _ -> assert false
- in
-*)
- let module MatitaTacticals = Continuationals.Make(MatitaStatus) in
- let tactical_of_ast l (text,prefix_len,tac) =
- let apply_tactic t = apply_tactic (text, prefix_len, t) in
- match tac with
- | GrafiteAst.Tactic (loc, tactic) ->
- MatitaTacticals.eval
- (MatitaTacticals.Tactical
- (MatitaTacticals.Tactic
- (MatitaStatus.mk_tactic (apply_tactic tactic))))
-(*
- | GrafiteAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
- assert (l > 0);
- MatitaTacticals.seq ~tactics:(List.map (tactical_of_ast (l+1)) tacticals)
- | GrafiteAst.Do (loc, n, tactical) ->
- MatitaTacticals.do_tactic ~n ~tactic:(tactical_of_ast (l+1) tactical)
-*)
- | GrafiteAst.Repeat (loc, GrafiteAst.Tactic (_,tactical)) ->
- MatitaTacticals.eval
- (MatitaTacticals.Tactical
- (MatitaTacticals.Tactic
- (MatitaStatus.mk_tactic
- (apply_atomic_tactical ~disambiguate_tactic
- ~patch:(fun tactic -> Tacticals.repeat_tactic ~tactic)
- (text,prefix_len,tactical)))))
-(*
- | GrafiteAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
- assert (l > 0);
- MatitaTacticals.thens ~start:(tactical_of_ast (l+1) tactical)
- ~continuations:(List.map (tactical_of_ast (l+1)) tacticals)
-*)
- | GrafiteAst.First (loc, [GrafiteAst.Tactic (_,tacticals)]) ->
- MatitaTacticals.eval
- (MatitaTacticals.Tactical
- (MatitaTacticals.Tactic
- (MatitaStatus.mk_tactic
- (apply_atomic_tactical ~disambiguate_tactic
- ~patch:(fun tactic ->Tacticals.first ~tactics:["",tactic])
- (text,prefix_len,tacticals)))))
- | GrafiteAst.Try (loc, GrafiteAst.Tactic (_,tactical)) ->
- MatitaTacticals.eval
- (MatitaTacticals.Tactical
- (MatitaTacticals.Tactic
- (MatitaStatus.mk_tactic
- (apply_atomic_tactical ~disambiguate_tactic
- ~patch:(fun tactic -> Tacticals.try_tactic ~tactic)
- (text,prefix_len,tactical)))))
- | GrafiteAst.Solve (loc, [GrafiteAst.Tactic (_,tacticals)]) ->
- MatitaTacticals.eval
- (MatitaTacticals.Tactical
- (MatitaTacticals.Tactic
- (MatitaStatus.mk_tactic
- (apply_atomic_tactical ~disambiguate_tactic
- ~patch:(fun tactic ->Tacticals.solve_tactics ~tactics:["",tactic])
- (text,prefix_len,tacticals)))))
- | GrafiteAst.Progress (loc, GrafiteAst.Tactic (_,tactical)) ->
- MatitaTacticals.eval
- (MatitaTacticals.Tactical
- (MatitaTacticals.Tactic
- (MatitaStatus.mk_tactic
- (apply_atomic_tactical ~disambiguate_tactic
- ~patch:(fun tactic -> Tacticals.progress_tactic ~tactic)
- (text,prefix_len,tactical)))))
- | GrafiteAst.Skip _loc ->
- MatitaTacticals.eval (MatitaTacticals.Tactical MatitaTacticals.Skip)
- | GrafiteAst.Dot _loc ->
- MatitaTacticals.eval (MatitaTacticals.Dot)
- | GrafiteAst.Semicolon _loc ->
- MatitaTacticals.eval (MatitaTacticals.Semicolon)
- | GrafiteAst.Branch _loc ->
- MatitaTacticals.eval MatitaTacticals.Branch
- | GrafiteAst.Shift _loc ->
- MatitaTacticals.eval MatitaTacticals.Shift
- | GrafiteAst.Pos (_loc, i) ->
- MatitaTacticals.eval (MatitaTacticals.Pos i)
- | GrafiteAst.Merge _loc ->
- MatitaTacticals.eval MatitaTacticals.Merge
- | GrafiteAst.Focus (_loc, goals) ->
- MatitaTacticals.eval (MatitaTacticals.Focus goals)
- | GrafiteAst.Unfocus _loc ->
- MatitaTacticals.eval MatitaTacticals.Unfocus
- | GrafiteAst.Wildcard _loc ->
- MatitaTacticals.eval MatitaTacticals.Wildcard
- in
- let status, _, _ = tactical_of_ast 0 tac (status, ~-1) in
+module MatitaStatus =
+ struct
+ type input_status = GrafiteTypes.status * ProofEngineTypes.goal
+
+ type output_status =
+ GrafiteTypes.status * ProofEngineTypes.goal list * ProofEngineTypes.goal list
+
+ type tactic = input_status -> output_status
+
+ let mk_tactic tac = tac
+ let apply_tactic tac = tac
+ let goals (_, opened, closed) = opened, closed
+ let get_stack (status, _) = GrafiteTypes.get_stack status
+
+ let set_stack stack (status, opened, closed) =
+ GrafiteTypes.set_stack stack status, opened, closed
+
+ let inject (status, _) = (status, [], [])
+ let focus goal (status, _, _) = (status, goal)
+ end
+
+module MatitaTacticals = Continuationals.Make(MatitaStatus)
+
+let tactic_of_ast' tac =
+ MatitaTacticals.Tactical (MatitaTacticals.Tactic (MatitaStatus.mk_tactic tac))
+
+let punctuation_tactical_of_ast (text,prefix_len,punct) =
+ match punct with
+ | 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.Wildcard _loc -> MatitaTacticals.Wildcard
+
+let non_punctuation_tactical_of_ast (text,prefix_len,punct) =
+ match punct with
+ | GrafiteAst.Focus (_loc,goals) -> MatitaTacticals.Focus goals
+ | GrafiteAst.Unfocus _loc -> MatitaTacticals.Unfocus
+ | GrafiteAst.Skip _loc -> MatitaTacticals.Tactical MatitaTacticals.Skip
+
+let eval_tactical status tac =
+ let status, _, _ = MatitaTacticals.eval tac (status, ~-1) in
let status = (* is proof completed? *)
match status.GrafiteTypes.proof_status with
| GrafiteTypes.Incomplete_proof
} and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command
~disambiguate_macro opts status (text,prefix_len,ex) ->
match ex with
- | GrafiteAst.Tactical (_, tac, None) ->
- eval_tactical ~disambiguate_tactic status (text,prefix_len,tac),[]
- | GrafiteAst.Tactical (_, tac, Some punct) ->
+ | GrafiteAst.Tactic (_, Some tac, punct) ->
+ let tac = apply_tactic ~disambiguate_tactic (text,prefix_len,tac) in
+ let status = eval_tactical status (tactic_of_ast' tac) in
+ eval_tactical status
+ (punctuation_tactical_of_ast (text,prefix_len,punct)),[]
+ | GrafiteAst.Tactic (_, None, punct) ->
+ eval_tactical status
+ (punctuation_tactical_of_ast (text,prefix_len,punct)),[]
+ | GrafiteAst.NonPunctuationTactical (_, tac, punct) ->
let status =
- eval_tactical ~disambiguate_tactic status (text,prefix_len,tac) in
- eval_tactical ~disambiguate_tactic status (text,prefix_len,punct),[]
+ eval_tactical status
+ (non_punctuation_tactical_of_ast (text,prefix_len,tac))
+ in
+ eval_tactical status
+ (punctuation_tactical_of_ast (text,prefix_len,punct)),[]
| GrafiteAst.Command (_, cmd) ->
eval_command.ec_go ~disambiguate_command opts status (text,prefix_len,cmd)
| GrafiteAst.Macro (loc, macro) ->
| `Whd as kind -> kind
;;
-let disambiguate_tactic
+let rec disambiguate_tactic
lexicon_status_ref context metasenv (text,prefix_len,tactic)
=
let disambiguate_term =
disambiguate_reduction_kind text prefix_len lexicon_status_ref in
let disambiguate_lazy_term =
disambiguate_lazy_term text prefix_len lexicon_status_ref in
+ let disambiguate_tactic metasenv tac =
+ disambiguate_tactic lexicon_status_ref context metasenv (text,prefix_len,tac)
+ in
match tactic with
+ (* Higher order tactics *)
+ | GrafiteAst.Progress (loc,tac) ->
+ let metasenv,tac = disambiguate_tactic metasenv tac in
+ metasenv,GrafiteAst.Progress (loc,tac)
+ | GrafiteAst.Solve (loc,tacl) ->
+ let metasenv,tacl =
+ List.fold_right
+ (fun tac (metasenv,tacl) ->
+ let metasenv,tac = disambiguate_tactic metasenv tac in
+ metasenv,tac::tacl
+ ) tacl (metasenv,[])
+ in
+ metasenv,GrafiteAst.Solve (loc,tacl)
+ | GrafiteAst.Try (loc,tac) ->
+ let metasenv,tac = disambiguate_tactic metasenv tac in
+ metasenv,GrafiteAst.Try (loc,tac)
+ | GrafiteAst.First (loc,tacl) ->
+ let metasenv,tacl =
+ List.fold_right
+ (fun tac (metasenv,tacl) ->
+ let metasenv,tac = disambiguate_tactic metasenv tac in
+ metasenv,tac::tacl
+ ) tacl (metasenv,[])
+ in
+ metasenv,GrafiteAst.First (loc,tacl)
+ | GrafiteAst.Seq (loc,tacl) ->
+ let metasenv,tacl =
+ List.fold_right
+ (fun tac (metasenv,tacl) ->
+ let metasenv,tac = disambiguate_tactic metasenv tac in
+ metasenv,tac::tacl
+ ) tacl (metasenv,[])
+ in
+ metasenv,GrafiteAst.Seq (loc,tacl)
+ | GrafiteAst.Repeat (loc,tac) ->
+ let metasenv,tac = disambiguate_tactic metasenv tac in
+ metasenv,GrafiteAst.Repeat (loc,tac)
+ | GrafiteAst.Do (loc,n,tac) ->
+ let metasenv,tac = disambiguate_tactic metasenv tac in
+ metasenv,GrafiteAst.Do (loc,n,tac)
+ | GrafiteAst.Then (loc,tac,tacl) ->
+ let metasenv,tac = disambiguate_tactic metasenv tac in
+ let metasenv,tacl =
+ List.fold_right
+ (fun tac (metasenv,tacl) ->
+ let metasenv,tac = disambiguate_tactic metasenv tac in
+ metasenv,tac::tacl
+ ) tacl (metasenv,[])
+ in
+ metasenv,GrafiteAst.Then (loc,tac,tacl)
+ (* First order tactics *)
| GrafiteAst.Absurd (loc, term) ->
let metasenv,cic = disambiguate_term context metasenv term in
metasenv,GrafiteAst.Absurd (loc, cic)
| GrafiteAst.Generalize (loc,pattern,ident) ->
let pattern = disambiguate_pattern pattern in
metasenv,GrafiteAst.Generalize (loc,pattern,ident)
- | GrafiteAst.Goal (loc, g) ->
- metasenv,GrafiteAst.Goal (loc, g)
| GrafiteAst.IdTac loc ->
metasenv,GrafiteAst.IdTac loc
| GrafiteAst.Intros (loc, num, names) ->
GrafiteAst.FwdSimpl (loc, hyp, idents)
| IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] ->
GrafiteAst.Generalize (loc,p,id)
- | IDENT "goal"; n = int ->
- GrafiteAst.Goal (loc, n)
| IDENT "id" -> GrafiteAst.IdTac loc
| IDENT "intro"; ident = OPT IDENT ->
let idents = match ident with None -> [] | Some id -> [id] in
(GrafiteAst.Then (loc, tac, tacs))
]
| "loops" RIGHTA
- [ IDENT "do"; count = int; tac = SELF; IDENT "end" ->
+ [ IDENT "do"; count = int; tac = SELF ->
GrafiteAst.Do (loc, count, tac)
- | IDENT "repeat"; tac = SELF; IDENT "end" -> GrafiteAst.Repeat (loc, tac)
+ | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac)
]
| "simple" NONA
[ IDENT "first";
GrafiteAst.Solve (loc, tacs)
| IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
| LPAREN; tac = SELF; RPAREN -> tac
- | tac = tactic -> GrafiteAst.Tactic (loc, tac)
+ | tac = tactic -> tac
]
];
punctuation_tactical:
| SYMBOL "." -> GrafiteAst.Dot loc
]
];
- tactical:
+ non_punctuation_tactical:
[ "simple" NONA
[ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals)
| IDENT "unfocus" -> GrafiteAst.Unfocus loc
| IDENT "skip" -> GrafiteAst.Skip loc
- | tac = atomic_tactical LEVEL "loops" -> tac
]
];
theorem_flavour: [
]];
executable: [
[ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd)
- | tac = tactical; punct = punctuation_tactical ->
- GrafiteAst.Tactical (loc, tac, Some punct)
- | punct = punctuation_tactical -> GrafiteAst.Tactical (loc, punct, None)
+ | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
+ GrafiteAst.Tactic (loc, Some tac, punct)
+ | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct)
+ | tac = non_punctuation_tactical; punct = punctuation_tactical ->
+ GrafiteAst.NonPunctuationTactical (loc, tac, punct)
| mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac)
]
];
~continuations:
[PrimitiveTactics.apply_tac ~term:_Rinv_R1;
Tacticals.first
- ~tactics:[ "ring",Ring.ring_tac; "id", Tacticals.id_tac]
+ ~tactics:[Ring.ring_tac; Tacticals.id_tac]
])
;(*Tacticals.id_tac*)
Tacticals.then_
(curi, metasenv, pbo, pty, attrs), [goal]
in
PET.mk_tactic rename
-
-let set_goal n =
- PET.mk_tactic
- (fun (proof, goal) ->
- let (_, metasenv, _, _, _) = proof in
- if CicUtil.exists_meta n metasenv then
- (proof, [n])
- else
- raise (PET.Fail (lazy ("no such meta: " ^ string_of_int n))))
(* Warning: this tactic has no effect on the proof term.
It just changes the name of an hypothesis in the current sequent *)
val rename: froms:string list -> tos:string list -> ProofEngineTypes.tactic
-
- (* change the current goal to those referred by the given meta number *)
-val set_goal: int -> ProofEngineTypes.tactic
ProofEngineTypes.apply_tactic
(Tacticals.first
~tactics:[
- "reflexivity", EqualityTactics.reflexivity_tac ;
- "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ;
- "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'' ;
- "exact sym_eqt su t1 ...", exact_tac
+ EqualityTactics.reflexivity_tac ;
+ exact_tac ~term:t1'_eq_t1'' ;
+ exact_tac ~term:t2'_eq_t2'' ;
+ exact_tac
~term:(
Cic.Appl
[mkConst HelmLibraryObjects.Logic.sym_eq_URI
] ;
t1'_eq_t1''
]) ;
- "elim_type eqt su t1 ...", ProofEngineTypes.mk_tactic (fun status ->
+ ProofEngineTypes.mk_tactic (fun status ->
let status' = (* status after 1st elim_type use *)
let context = context_of_status status in
let b,_ = (*TASSI : FIXME*)
ProofEngineTypes.apply_tactic
(Tacticals.first (* try to solve 1st subgoal *)
~tactics:[
- "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'';
- "exact sym_eqt su t2 ...",
- exact_tac
+ exact_tac ~term:t2'_eq_t2'';
+ exact_tac
~term:(
Cic.Appl
[mkConst HelmLibraryObjects.Logic.sym_eq_URI
] ;
t2'_eq_t2''
]) ;
- "elim_type eqt su t2 ...",
ProofEngineTypes.mk_tactic (fun status ->
let status' =
let context = context_of_status status in
(* Tacticals that cannot be implemented on top of tynycals *)
let first ~tactics =
- let rec first ~(tactics: (string * tactic) list) status =
+ let rec first ~(tactics: tactic list) status =
info (lazy "in Tacticals.first");
match tactics with
[] -> raise (PET.Fail (lazy "first: no tactics left"))
- | (descr, tac)::tactics ->
- info (lazy ("Tacticals.first IS TRYING " ^ descr));
+ | tac::tactics ->
try
let res = PET.apply_tactic tac status in
- info (lazy ("Tacticals.first: " ^ descr ^ " succedeed!!!"));
+ info (lazy ("Tacticals.first: succedeed!!!"));
res
with
PET.Fail _ -> first ~tactics status
(* This tries tactics until one of them solves the goal *)
let solve_tactics ~tactics =
- let rec solve_tactics ~(tactics: (string * tactic) list) status =
+ let rec solve_tactics ~(tactics: tactic list) status =
info (lazy "in Tacticals.solve_tactics");
match tactics with
- | (descr, currenttactic)::moretactics ->
- info (lazy ("Tacticals.solve_tactics is trying " ^ descr));
+ | currenttactic::moretactics ->
(try
let (proof, opened) as output_status =
PET.apply_tactic currenttactic status
in
match opened with
- | [] -> info (lazy ("Tacticals.solve_tactics: " ^ descr ^
- " solved the goal!!!"));
+ | [] -> info (lazy ("Tacticals.solve_tactics: solved the goal!!!"));
output_status
| _ -> info (lazy ("Tacticals.solve_tactics: try the next tactic"));
raise (PET.Fail (lazy "Goal not solved"))
val id_tac : tactic
val fail_tac: tactic
-val first: tactics: (string * tactic) list -> tactic
+val first: tactics: tactic list -> tactic
val thens: start: tactic -> continuations: tactic list -> tactic
val then_: start: tactic -> continuation: tactic -> tactic
val seq: tactics: tactic list -> tactic (** "folding" of then_ *)
val repeat_tactic: tactic: tactic -> tactic
val do_tactic: n: int -> tactic: tactic -> tactic
val try_tactic: tactic: tactic -> tactic
-val solve_tactics: tactics: (string * tactic) list -> tactic
+val solve_tactics: tactics: tactic list -> tactic
val progress_tactic: tactic: tactic -> tactic
(* TODO temporary *)
let rewrite_simpl = EqualityTactics.rewrite_simpl_tac
let right = IntroductionTactics.right_tac
let ring = Ring.ring_tac
-let set_goal = ProofEngineStructuralRules.set_goal
let simpl = ReductionTactics.simpl_tac
let split = IntroductionTactics.split_tac
let subst = SubstTactic.subst_tac
-(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Apr 16 17:26:20 CEST 2007 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Apr 20 15:46:14 CEST 2007 *)
val absurd : term:Cic.term -> ProofEngineTypes.tactic
val apply : term:Cic.term -> ProofEngineTypes.tactic
val applyS :
?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic
val exact : term:Cic.term -> ProofEngineTypes.tactic
val exists : ProofEngineTypes.tactic
-val fail : ProofEngineTypes.tactic
+val fail : Tacticals.tactic
val fold :
reduction:ProofEngineTypes.lazy_reduction ->
term:Cic.lazy_term ->
val generalize :
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
-val id : ProofEngineTypes.tactic
+val id : Tacticals.tactic
val intros :
?howmany:int ->
?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
Cic.term -> string list -> ProofEngineTypes.tactic
val right : ProofEngineTypes.tactic
val ring : ProofEngineTypes.tactic
-val set_goal : int -> ProofEngineTypes.tactic
val simpl : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic
val split : ProofEngineTypes.tactic
val subst : ProofEngineTypes.tactic
let o = PT.Theorem (`Theorem,name,f,None) in
statements @ [
GA.Executable(floc,GA.Command(floc,GA.Obj(floc,o)));
- GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
- GA.Intros (floc,None,[])),Some (GA.Dot(floc))))] @
+ GA.Executable(floc,GA.Tactic(floc, Some
+ (GA.Intros (floc,None,[])),GA.Dot(floc)))] @
(if fv <> [] then
(List.flatten
(List.map
(fun _ ->
- [GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
- GA.Exists floc),Some (GA.Branch floc)));
- GA.Executable(floc,GA.Tactical(floc,
- GA.Pos (floc,[2]),None))])
+ [GA.Executable(floc,GA.Tactic(floc, Some
+ (GA.Exists floc),GA.Branch floc));
+ GA.Executable(floc,GA.Tactic(floc, None,
+ (GA.Pos (floc,[2]))))])
fv))
else [])@
- [GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc,
+ [GA.Executable(floc,GA.Tactic(floc, Some (
if ueq_case then
GA.Auto (floc,["paramodulation","";
"timeout",string_of_int !paramod_timeout])
else
GA.Auto (floc,["depth",string_of_int !depth])
),
- Some (GA.Dot(floc))));
- GA.Executable(floc,GA.Tactical(floc, GA.Try(floc,
- GA.Tactic (floc, GA.Assumption floc)), Some (GA.Dot(floc))))
+ GA.Dot(floc)));
+ GA.Executable(floc,GA.Tactic(floc, Some (GA.Try(floc,
+ GA.Assumption floc)), GA.Dot(floc)))
]@
(if fv <> [] then
(List.flatten
(List.map
(fun _ ->
- [GA.Executable(floc,GA.Tactical(floc, GA.Shift floc, None));
- GA.Executable(floc,GA.Tactical(floc, GA.Skip floc,Some
+ [GA.Executable(floc,GA.Tactic(floc, None, GA.Shift floc));
+ GA.Executable(floc,GA.NonPunctuationTactical(floc, GA.Skip floc,
(GA.Merge floc)))])
fv))
else [])@
<entry/>
<entry>|</entry>
<entry><emphasis role="bold">do</emphasis> &nat;
- &LCFtactical; <emphasis role="bold">end</emphasis>
+ &LCFtactical;
</entry>
<entry>&TODO;</entry>
</row>
<entry/>
<entry>|</entry>
<entry><emphasis role="bold">repeat</emphasis>
- &LCFtactical; <emphasis role="bold">end</emphasis>
+ &LCFtactical;
</entry>
<entry>&TODO;</entry>
</row>
(* some properties of div and mod *)
theorem div_times: \forall n,m:nat. ((S n)*m) / (S n) = m.
intros.
-apply (div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O).
-goal 15. (* ?11 is closed with the following tactics *)
-apply div_mod_spec_div_mod.
-unfold lt.apply le_S_S.apply le_O_n.
-apply div_mod_spec_times.
+apply (div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O);
+[2: apply div_mod_spec_div_mod.
+ unfold lt.apply le_S_S.apply le_O_n.
+| skip
+| apply div_mod_spec_times
+]
qed.
theorem div_n_n: \forall n:nat. O < n \to n / n = S O.
rewrite > Hcut.rewrite < H1.rewrite < times_n_O.reflexivity.
apply le_to_or_lt_eq.apply le_O_n.
(* prova del cut *)
-goal 20.
apply (p_ord_aux_to_exp (S(S m1))).
apply lt_O_nth_prime_n.
assumption.
apply (nat_elim2 (\lambda n,m.n \leq m \to n-m = O)).
intros.simplify.reflexivity.
intros.apply False_ind.
-apply not_le_Sn_O.
-goal 13.apply H.
+apply not_le_Sn_O;
+[2: apply H | skip].
intros.
simplify.apply H.apply le_S_S_to_le. apply H1.
qed.
theorem le_n_O_to_eq : \forall n:nat. n \leq O \to O=n.
intro.elim n.reflexivity.
apply False_ind.
-apply not_le_Sn_O.
-goal 17. apply H1.
+apply not_le_Sn_O;
+[2: apply H1 | skip].
qed.
theorem le_n_O_elim: \forall n:nat.n \leq O \to \forall P: nat \to Prop.
if (MatitaScript.current ())#onGoingProof () then
(MatitaScript.current ())#advance
~statement:("\n"
- ^ GrafiteAstPp.pp_tactical ~term_pp:CicNotationPp.pp_term
- ~lazy_term_pp:CicNotationPp.pp_term (A.Tactic (loc, ast)))
+ ^ GrafiteAstPp.pp_tactic ~term_pp:CicNotationPp.pp_term
+ ~lazy_term_pp:CicNotationPp.pp_term ast)
()
in
let tac_w_term ast _ =
"\n" ^
GrafiteAstPp.pp_executable ~term_pp:(fun s -> s)
~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false)
- (GrafiteAst.Tactical (loc,
- GrafiteAst.Tactic (loc, GrafiteAst.Reduce (loc, kind, pat)),
- Some (GrafiteAst.Semicolon loc))) in
+ (GrafiteAst.Tactic (loc,
+ Some (GrafiteAst.Reduce (loc, kind, pat)),
+ GrafiteAst.Semicolon loc)) in
(MatitaScript.current ())#advance ~statement () in
connect_menu_item copy gui#copy;
connect_menu_item normalize (reduction_action `Normalize);
String.sub s 0 nl_pos
with Not_found -> s
- (** creates a statement AST for the Goal tactic, e.g. "goal 7" *)
-let goal_ast n =
- let module A = GrafiteAst in
- let loc = HExtlib.dummy_floc in
- A.Executable (loc, A.Tactical (loc,
- A.Tactic (loc, A.Goal (loc, n)),
- Some (A.Dot loc)))
-
type guistuff = {
mathviewer:MatitaTypes.mathViewer;
urichooser: UriManager.uri list -> UriManager.uri list;
| [uri] ->
let suri = UriManager.string_of_uri uri in
let ast loc =
- TA.Executable (loc, (TA.Tactical (loc,
- TA.Tactic (loc,
- TA.Apply (loc, CicNotationPt.Uri (suri, None))),
- Some (TA.Dot loc)))) in
+ TA.Executable (loc, (TA.Tactic (loc,
+ Some (TA.Apply (loc, CicNotationPt.Uri (suri, None))),
+ TA.Dot loc))) in
let text =
comment parsed_text ^ "\n" ^
pp_eager_statement_ast (ast HExtlib.dummy_floc) in
projects / helm.git / commitdiff