+ status, (wanted, hyp_paths ,goal_path)
+
+let disambiguate_tactic status = function
+ | GrafiteAst.Apply (loc, term) ->
+ let status, cic = disambiguate_term status term in
+ status, GrafiteAst.Apply (loc, cic)
+ | GrafiteAst.Absurd (loc, term) ->
+ let status, cic = disambiguate_term status term in
+ status, GrafiteAst.Absurd (loc, cic)
+ | GrafiteAst.Assumption loc -> status, GrafiteAst.Assumption loc
+ | GrafiteAst.Auto (loc,depth,width,paramodulation) -> status, GrafiteAst.Auto (loc,depth,width,paramodulation) (* ALB *)
+ | GrafiteAst.Change (loc, pattern, with_what) ->
+ let status, with_what = disambiguate_term status with_what in
+ let status, pattern = disambiguate_pattern status pattern in
+ status, GrafiteAst.Change (loc, pattern, with_what)
+ | GrafiteAst.Clear (loc,id) -> status,GrafiteAst.Clear (loc,id)
+ | GrafiteAst.ClearBody (loc,id) -> status,GrafiteAst.ClearBody (loc,id)
+ | GrafiteAst.Compare (loc,term) ->
+ let status, term = disambiguate_term status term in
+ status, GrafiteAst.Compare (loc,term)
+ | GrafiteAst.Constructor (loc,n) ->
+ status, GrafiteAst.Constructor (loc,n)
+ | GrafiteAst.Contradiction loc ->
+ status, GrafiteAst.Contradiction loc
+ | GrafiteAst.Cut (loc, ident, term) ->
+ let status, cic = disambiguate_term status term in
+ status, GrafiteAst.Cut (loc, ident, cic)
+ | GrafiteAst.DecideEquality loc ->
+ status, GrafiteAst.DecideEquality loc
+ | GrafiteAst.Decompose (loc, types, what, names) ->
+ let disambiguate (status, types) = function
+ | GrafiteAst.Type _ -> assert false
+ | GrafiteAst.Ident id ->
+ match disambiguate_term status (CicNotationPt.Ident (id, None)) with
+ | status, Cic.MutInd (uri, tyno, _) ->
+ status, (GrafiteAst.Type (uri, tyno) :: types)
+ | _ ->
+ raise Disambiguate.NoWellTypedInterpretation
+ in
+ let status, types = List.fold_left disambiguate (status, []) types in
+ status, GrafiteAst.Decompose(loc, types, what, names)
+ | GrafiteAst.Discriminate (loc,term) ->
+ let status,term = disambiguate_term status term in
+ status, GrafiteAst.Discriminate(loc,term)
+ | GrafiteAst.Exact (loc, term) ->
+ let status, cic = disambiguate_term status term in
+ status, GrafiteAst.Exact (loc, cic)
+ | GrafiteAst.Elim (loc, what, Some using, depth, idents) ->
+ let status, what = disambiguate_term status what in
+ let status, using = disambiguate_term status using in
+ status, GrafiteAst.Elim (loc, what, Some using, depth, idents)
+ | GrafiteAst.Elim (loc, what, None, depth, idents) ->
+ let status, what = disambiguate_term status what in
+ status, GrafiteAst.Elim (loc, what, None, depth, idents)
+ | GrafiteAst.ElimType (loc, what, Some using, depth, idents) ->
+ let status, what = disambiguate_term status what in
+ let status, using = disambiguate_term status using in
+ status, GrafiteAst.ElimType (loc, what, Some using, depth, idents)
+ | GrafiteAst.ElimType (loc, what, None, depth, idents) ->
+ let status, what = disambiguate_term status what in
+ status, GrafiteAst.ElimType (loc, what, None, depth, idents)
+ | GrafiteAst.Exists loc -> status, GrafiteAst.Exists loc
+ | GrafiteAst.Fail loc -> status,GrafiteAst.Fail loc
+ | GrafiteAst.Fold (loc,reduction_kind, term, pattern) ->
+ let status, pattern = disambiguate_pattern status pattern in
+ let status, term = disambiguate_term status term in
+ status, GrafiteAst.Fold (loc,reduction_kind, term, pattern)
+ | GrafiteAst.FwdSimpl (loc, hyp, names) ->
+ status, GrafiteAst.FwdSimpl (loc, hyp, names)
+ | GrafiteAst.Fourier loc -> status, GrafiteAst.Fourier loc
+ | GrafiteAst.Generalize (loc,pattern,ident) ->
+ let status, pattern = disambiguate_pattern status pattern in
+ status, GrafiteAst.Generalize(loc,pattern,ident)
+ | GrafiteAst.Goal (loc, g) -> status, GrafiteAst.Goal (loc, g)
+ | GrafiteAst.IdTac loc -> status,GrafiteAst.IdTac loc
+ | GrafiteAst.Injection (loc,term) ->
+ let status, term = disambiguate_term status term in
+ status, GrafiteAst.Injection (loc,term)
+ | GrafiteAst.Intros (loc, num, names) ->
+ status, GrafiteAst.Intros (loc, num, names)
+ | GrafiteAst.LApply (loc, depth, to_what, what, ident) ->
+ let f term (status, to_what) =
+ let status, term = disambiguate_term status term in
+ status, term :: to_what
+ in
+ let status, to_what = List.fold_right f to_what (status, []) in
+ let status, what = disambiguate_term status what in
+ status, GrafiteAst.LApply (loc, depth, to_what, what, ident)
+ | GrafiteAst.Left loc -> status, GrafiteAst.Left loc
+ | GrafiteAst.LetIn (loc, term, name) ->
+ let status, term = disambiguate_term status term in
+ status, GrafiteAst.LetIn (loc,term,name)
+ | GrafiteAst.Reduce (loc, reduction_kind, pattern) ->
+ let status, pattern = disambiguate_pattern status pattern in
+ status, GrafiteAst.Reduce(loc, reduction_kind, pattern)
+ | GrafiteAst.Reflexivity loc -> status, GrafiteAst.Reflexivity loc
+ | GrafiteAst.Replace (loc, pattern, with_what) ->
+ let status, pattern = disambiguate_pattern status pattern in
+ let status, with_what = disambiguate_term status with_what in
+ status, GrafiteAst.Replace (loc, pattern, with_what)
+ | GrafiteAst.Rewrite (loc, dir, t, pattern) ->
+ let status, term = disambiguate_term status t in
+ let status, pattern = disambiguate_pattern status pattern in
+ status, GrafiteAst.Rewrite (loc, dir, term, pattern)
+ | GrafiteAst.Right loc -> status, GrafiteAst.Right loc
+ | GrafiteAst.Ring loc -> status, GrafiteAst.Ring loc
+ | GrafiteAst.Split loc -> status, GrafiteAst.Split loc
+ | GrafiteAst.Symmetry loc -> status, GrafiteAst.Symmetry loc
+ | GrafiteAst.Transitivity (loc, term) ->
+ let status, cic = disambiguate_term status term in
+ status, GrafiteAst.Transitivity (loc, cic)
+
+let apply_tactic tactic status =
+ let status,tactic = disambiguate_tactic status tactic in
+ let tactic = tactic_of_ast tactic in
+ let (proof, goals) =
+ ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status) in
+ let dummy = -1 in
+ { status with
+ proof_status = MatitaTypes.Incomplete_proof (proof,dummy) }, goals
+
+module MatitaStatus =
+ struct
+ type input_status = MatitaTypes.status
+ type output_status = MatitaTypes.status * ProofEngineTypes.goal list
+ type tactic = input_status -> output_status
+
+ let focus (status,_) goal =
+ let proof,_ = MatitaMisc.get_proof_status status in
+ {status with proof_status = MatitaTypes.Incomplete_proof (proof,goal)}
+
+ let goals (_,goals) = goals
+
+ let set_goals (status,_) goals = status,goals
+
+ let id_tac status =
+ apply_tactic (GrafiteAst.IdTac Disambiguate.dummy_floc) status
+
+ let mk_tactic tac = tac
+
+ let apply_tactic tac = tac
+
+ end
+
+module MatitaTacticals = Tacticals.Make(MatitaStatus)
+
+let eval_tactical status tac =
+ let rec tactical_of_ast tac =
+ match tac with
+ | GrafiteAst.Tactic (loc, tactic) -> apply_tactic tactic
+ | GrafiteAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
+ MatitaTacticals.seq ~tactics:(List.map tactical_of_ast tacticals)
+ | GrafiteAst.Do (loc, num, tactical) ->
+ MatitaTacticals.do_tactic ~n:num ~tactic:(tactical_of_ast tactical)
+ | GrafiteAst.Repeat (loc, tactical) ->
+ MatitaTacticals.repeat_tactic ~tactic:(tactical_of_ast tactical)
+ | GrafiteAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
+ MatitaTacticals.thens ~start:(tactical_of_ast tactical)
+ ~continuations:(List.map tactical_of_ast tacticals)
+ | GrafiteAst.First (loc, tacticals) ->
+ MatitaTacticals.first
+ ~tactics:(List.map (fun t -> "", tactical_of_ast t) tacticals)
+ | GrafiteAst.Try (loc, tactical) ->
+ MatitaTacticals.try_tactic ~tactic:(tactical_of_ast tactical)
+ | GrafiteAst.Solve (loc, tacticals) ->
+ MatitaTacticals.solve_tactics
+ ~tactics:(List.map (fun t -> "",tactical_of_ast t) tacticals)
+ in
+ let status,goals = tactical_of_ast tac status in
+ let proof,_ = MatitaMisc.get_proof_status status in
+ let new_status =
+ match goals with
+ | [] ->
+ let (_,metasenv,_,_) = proof in
+ (match metasenv with
+ | [] -> Proof proof
+ | (ng,_,_)::_ -> Incomplete_proof (proof,ng))
+ | ng::_ -> Incomplete_proof (proof, ng)
+ in
+ { status with proof_status = new_status }