-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) -> status, GrafiteAst.Auto (loc,depth,width)
- | 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 disambiguate_tactic status goal tactic =
+ let status_ref = ref status in
+ let tactic =
+ match tactic with
+ | GrafiteAst.Absurd (loc, term) ->
+ let cic = disambiguate_term status_ref goal term in
+ GrafiteAst.Absurd (loc, cic)
+ | GrafiteAst.Apply (loc, term) ->
+ let cic = disambiguate_term status_ref goal term in
+ GrafiteAst.Apply (loc, cic)
+ | GrafiteAst.Assumption loc -> GrafiteAst.Assumption loc
+ | GrafiteAst.Auto (loc,depth,width,paramodulation,full) ->
+ GrafiteAst.Auto (loc,depth,width,paramodulation,full)
+ | GrafiteAst.Change (loc, pattern, with_what) ->
+ let with_what = disambiguate_lazy_term status_ref with_what in
+ let pattern = disambiguate_pattern status_ref pattern in
+ GrafiteAst.Change (loc, pattern, with_what)
+ | GrafiteAst.Clear (loc,id) -> GrafiteAst.Clear (loc,id)
+ | GrafiteAst.ClearBody (loc,id) -> GrafiteAst.ClearBody (loc,id)
+ | GrafiteAst.Compare (loc,term) ->
+ let term = disambiguate_term status_ref goal term in
+ GrafiteAst.Compare (loc,term)
+ | GrafiteAst.Constructor (loc,n) -> GrafiteAst.Constructor (loc,n)
+ | GrafiteAst.Contradiction loc -> GrafiteAst.Contradiction loc
+ | GrafiteAst.Cut (loc, ident, term) ->
+ let cic = disambiguate_term status_ref goal term in
+ GrafiteAst.Cut (loc, ident, cic)
+ | GrafiteAst.DecideEquality loc -> GrafiteAst.DecideEquality loc
+ | GrafiteAst.Decompose (loc, types, what, names) ->
+ let disambiguate types = function
+ | GrafiteAst.Type _ -> assert false
+ | GrafiteAst.Ident id ->
+ (match disambiguate_term status_ref goal
+ (CicNotationPt.Ident (id, None))
+ with
+ | Cic.MutInd (uri, tyno, _) ->
+ (GrafiteAst.Type (uri, tyno) :: types)
+ | _ -> raise (MatitaDisambiguator.DisambiguationError [[lazy "Decompose works only on inductive types"]]))
+ in
+ let types = List.fold_left disambiguate [] types in
+ GrafiteAst.Decompose (loc, types, what, names)
+ | GrafiteAst.Discriminate (loc,term) ->
+ let term = disambiguate_term status_ref goal term in
+ GrafiteAst.Discriminate(loc,term)
+ | GrafiteAst.Exact (loc, term) ->
+ let cic = disambiguate_term status_ref goal term in
+ GrafiteAst.Exact (loc, cic)
+ | GrafiteAst.Elim (loc, what, Some using, depth, idents) ->
+ let what = disambiguate_term status_ref goal what in
+ let using = disambiguate_term status_ref goal using in
+ GrafiteAst.Elim (loc, what, Some using, depth, idents)
+ | GrafiteAst.Elim (loc, what, None, depth, idents) ->
+ let what = disambiguate_term status_ref goal what in
+ GrafiteAst.Elim (loc, what, None, depth, idents)
+ | GrafiteAst.ElimType (loc, what, Some using, depth, idents) ->
+ let what = disambiguate_term status_ref goal what in
+ let using = disambiguate_term status_ref goal using in
+ GrafiteAst.ElimType (loc, what, Some using, depth, idents)
+ | GrafiteAst.ElimType (loc, what, None, depth, idents) ->
+ let what = disambiguate_term status_ref goal what in
+ GrafiteAst.ElimType (loc, what, None, depth, idents)
+ | GrafiteAst.Exists loc -> GrafiteAst.Exists loc
+ | GrafiteAst.Fail loc -> GrafiteAst.Fail loc
+ | GrafiteAst.Fold (loc,red_kind, term, pattern) ->
+ let pattern = disambiguate_pattern status_ref pattern in
+ let term = disambiguate_lazy_term status_ref term in
+ let red_kind = disambiguate_reduction_kind status_ref red_kind in
+ GrafiteAst.Fold (loc, red_kind, term, pattern)
+ | GrafiteAst.FwdSimpl (loc, hyp, names) ->
+ GrafiteAst.FwdSimpl (loc, hyp, names)
+ | GrafiteAst.Fourier loc -> GrafiteAst.Fourier loc
+ | GrafiteAst.Generalize (loc,pattern,ident) ->
+ let pattern = disambiguate_pattern status_ref pattern in
+ GrafiteAst.Generalize (loc,pattern,ident)
+ | GrafiteAst.Goal (loc, g) -> GrafiteAst.Goal (loc, g)
+ | GrafiteAst.IdTac loc -> GrafiteAst.IdTac loc
+ | GrafiteAst.Injection (loc, term) ->
+ let term = disambiguate_term status_ref goal term in
+ GrafiteAst.Injection (loc,term)
+ | GrafiteAst.Intros (loc, num, names) -> GrafiteAst.Intros (loc, num, names)
+ | GrafiteAst.LApply (loc, depth, to_what, what, ident) ->
+ let f term to_what =
+ let term = disambiguate_term status_ref goal term in
+ term :: to_what
+ in
+ let to_what = List.fold_right f to_what [] in
+ let what = disambiguate_term status_ref goal what in
+ GrafiteAst.LApply (loc, depth, to_what, what, ident)
+ | GrafiteAst.Left loc -> GrafiteAst.Left loc
+ | GrafiteAst.LetIn (loc, term, name) ->
+ let term = disambiguate_term status_ref goal term in
+ GrafiteAst.LetIn (loc,term,name)
+ | GrafiteAst.Reduce (loc, red_kind, pattern) ->
+ let pattern = disambiguate_pattern status_ref pattern in
+ let red_kind = disambiguate_reduction_kind status_ref red_kind in
+ GrafiteAst.Reduce(loc, red_kind, pattern)
+ | GrafiteAst.Reflexivity loc -> GrafiteAst.Reflexivity loc
+ | GrafiteAst.Replace (loc, pattern, with_what) ->
+ let pattern = disambiguate_pattern status_ref pattern in
+ let with_what = disambiguate_lazy_term status_ref with_what in
+ GrafiteAst.Replace (loc, pattern, with_what)
+ | GrafiteAst.Rewrite (loc, dir, t, pattern) ->
+ let term = disambiguate_term status_ref goal t in
+ let pattern = disambiguate_pattern status_ref pattern in
+ GrafiteAst.Rewrite (loc, dir, term, pattern)
+ | GrafiteAst.Right loc -> GrafiteAst.Right loc
+ | GrafiteAst.Ring loc -> GrafiteAst.Ring loc
+ | GrafiteAst.Split loc -> GrafiteAst.Split loc
+ | GrafiteAst.Symmetry loc -> GrafiteAst.Symmetry loc
+ | GrafiteAst.Transitivity (loc, term) ->
+ let cic = disambiguate_term status_ref goal term in
+ GrafiteAst.Transitivity (loc, cic)
+ in
+ status_ref, tactic
+
+let reorder_metasenv start refine tactic goals current_goal always_opens_a_goal=
+ let module PEH = ProofEngineHelpers in
+(* let print_m name metasenv =
+ prerr_endline (">>>>> " ^ name);
+ prerr_endline (CicMetaSubst.ppmetasenv [] metasenv)
+ in *)
+ (* phase one calculates:
+ * new_goals_from_refine: goals added by refine
+ * head_goal: the first goal opened by ythe tactic
+ * other_goals: other goals opened by the tactic
+ *)
+ let new_goals_from_refine = PEH.compare_metasenvs start refine in
+ let new_goals_from_tactic = PEH.compare_metasenvs refine tactic in
+ let head_goal, other_goals, goals =
+ match goals with
+ | [] -> None,[],goals
+ | hd::tl ->
+ (* assert (List.mem hd new_goals_from_tactic);
+ * invalidato dalla goal_tac
+ * *)
+ Some hd, List.filter ((<>) hd) new_goals_from_tactic, List.filter ((<>)
+ hd) goals
+ in
+ let produced_goals =
+ match head_goal with
+ | None -> new_goals_from_refine @ other_goals
+ | Some x -> x :: new_goals_from_refine @ other_goals
+ in
+ (* extract the metas generated by refine and tactic *)
+ let metas_for_tactic_head =
+ match head_goal with
+ | None -> []
+ | Some head_goal -> List.filter (fun (n,_,_) -> n = head_goal) tactic in
+ let metas_for_tactic_goals =
+ List.map
+ (fun x -> List.find (fun (metano,_,_) -> metano = x) tactic)
+ goals
+ in
+ let metas_for_refine_goals =
+ List.filter (fun (n,_,_) -> List.mem n new_goals_from_refine) tactic in
+ let produced_metas, goals =
+ let produced_metas =
+ if always_opens_a_goal then
+ metas_for_tactic_head @ metas_for_refine_goals @
+ metas_for_tactic_goals
+ else begin
+(* print_m "metas_for_refine_goals" metas_for_refine_goals;
+ print_m "metas_for_tactic_head" metas_for_tactic_head;
+ print_m "metas_for_tactic_goals" metas_for_tactic_goals; *)
+ metas_for_refine_goals @ metas_for_tactic_head @
+ metas_for_tactic_goals
+ end
+ in
+ let goals = List.map (fun (metano, _, _) -> metano) produced_metas in
+ produced_metas, goals
+ in
+ (* residual metas, preserving the original order *)
+ let before, after =
+ let rec split e =
+ function
+ | [] -> [],[]
+ | (metano, _, _) :: tl when metano = e ->
+ [], List.map (fun (x,_,_) -> x) tl
+ | (metano, _, _) :: tl -> let b, a = split e tl in metano :: b, a
+ in
+ let find n metasenv =
+ try
+ Some (List.find (fun (metano, _, _) -> metano = n) metasenv)
+ with Not_found -> None
+ in
+ let extract l =
+ List.fold_right
+ (fun n acc ->
+ match find n tactic with
+ | Some x -> x::acc
+ | None -> acc
+ ) l [] in
+ let before_l, after_l = split current_goal start in
+ let before_l =
+ List.filter (fun x -> not (List.mem x produced_goals)) before_l in
+ let after_l =
+ List.filter (fun x -> not (List.mem x produced_goals)) after_l in
+ let before = extract before_l in
+ let after = extract after_l in
+ before, after
+ in
+(* |+ DEBUG CODE +|
+ print_m "BEGIN" start;
+ prerr_endline ("goal was: " ^ string_of_int current_goal);
+ prerr_endline ("and metas from refine are:");
+ List.iter
+ (fun t -> prerr_string (" " ^ string_of_int t))
+ new_goals_from_refine;
+ prerr_endline "";
+ print_m "before" before;
+ print_m "metas_for_tactic_head" metas_for_tactic_head;
+ print_m "metas_for_refine_goals" metas_for_refine_goals;
+ print_m "metas_for_tactic_goals" metas_for_tactic_goals;
+ print_m "produced_metas" produced_metas;
+ print_m "after" after;
+|+ FINE DEBUG CODE +| *)
+ before @ produced_metas @ after, goals
+
+(* maybe we only need special cases for apply and goal *)
+let classify_tactic tactic =
+ match tactic with
+ (* tactics that can't close the goal (return a goal we want to "select") *)
+ | GrafiteAst.Rewrite _
+ | GrafiteAst.Split _
+ | GrafiteAst.Replace _
+ | GrafiteAst.Reduce _
+ | GrafiteAst.Injection _
+ | GrafiteAst.IdTac _
+ | 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
+ (* tactics like apply *)
+ | _ -> true, false
+
+let apply_tactic tactic (status, goal) =
+(* prerr_endline "apply_tactic"; *)
+(* prerr_endline (Continuationals.Stack.pp (MatitaTypes.get_stack status)); *)
+ let starting_metasenv = MatitaTypes.get_proof_metasenv status in
+ let before = List.map (fun g, _, _ -> g) starting_metasenv in
+(* prerr_endline "disambiguate"; *)
+ let status_ref, tactic = disambiguate_tactic status goal tactic in
+ let metasenv_after_refinement = MatitaTypes.get_proof_metasenv !status_ref in
+ let proof = MatitaTypes.get_current_proof !status_ref in
+ let proof_status = proof, goal in
+ let needs_reordering, always_opens_a_goal = classify_tactic tactic in