X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=4bb40797527a38bb03cbec392cb0e82df5675aae;hb=5a702cea95883f7095c16b450e065ccb1714fc5a;hp=8c891b04355759f28ff7a8522329fed6dcb54293;hpb=51ce243d63b02d6ad690a5d2e1d79e34d548f86b;p=helm.git diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 8c891b043..4bb407975 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -165,7 +165,8 @@ let disambiguate_term status_ref term = let (aliases, metasenv, cic, _) = singleton (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ()) - ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status) + ~aliases:status.aliases ~universe:(Some status.multi_aliases) + ~context:(MatitaMisc.get_proof_context status) ~metasenv:(MatitaMisc.get_proof_metasenv status) term) in let status = MatitaTypes.set_metasenv metasenv status in @@ -184,8 +185,8 @@ let disambiguate_lazy_term status_ref term = let (aliases, metasenv, cic, ugraph) = singleton (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ()) - ~initial_ugraph:ugraph ~aliases:status.aliases ~context ~metasenv - term) + ~initial_ugraph:ugraph ~aliases:status.aliases + ~universe:(Some status.multi_aliases) ~context ~metasenv term) in let status = MatitaTypes.set_metasenv metasenv status in let status = MatitaSync.set_proof_aliases status aliases in @@ -328,12 +329,142 @@ let disambiguate_tactic status tactic = in status_ref, tactic +let reorder_metasenv start refine tactic goals current_goal always_opens_a_goal= + let module PEH = ProofEngineHelpers 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 + metas_for_refine_goals @ metas_for_tactic_head @ + metas_for_tactic_goals + 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 + let print_m name metasenv = + prerr_endline (">>>>> " ^ name); + prerr_endline (CicMetaSubst.ppmetasenv metasenv []) + in + 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 "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.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 = + let starting_metasenv = MatitaMisc.get_proof_metasenv status in let status_ref, tactic = disambiguate_tactic status tactic in + let metasenv_after_refinement = MatitaMisc.get_proof_metasenv !status_ref in let proof_status = MatitaMisc.get_proof_status !status_ref in + let needs_reordering, always_opens_a_goal = classify_tactic tactic in let tactic = tactic_of_ast tactic in (* apply tactic will change the status pointed by status_ref ... *) + let current_goal = let _, g = proof_status in g in let (proof, goals) = ProofEngineTypes.apply_tactic tactic proof_status in + let proof, goals = + if needs_reordering then + let uri, metasenv_after_tactic, t, ty = proof in + let reordered_metasenv, goals = + reorder_metasenv starting_metasenv metasenv_after_refinement + metasenv_after_tactic goals current_goal always_opens_a_goal in + (uri, reordered_metasenv, t, ty), goals + else + proof, goals + in let dummy = -1 in { !status_ref with proof_status = MatitaTypes.Incomplete_proof (proof,dummy) }, @@ -511,7 +642,7 @@ let disambiguate_obj status obj = let (aliases, metasenv, cic, _) = singleton (MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ()) - ~aliases:(status.aliases) ~uri obj) + ~aliases:status.aliases ~universe:(Some status.multi_aliases) ~uri obj) in let proof_status = match status.proof_status with @@ -628,17 +759,17 @@ let eval_command opts status cmd = code in DisambiguatePp *) match spec with | GrafiteAst.Ident_alias (id,uri) -> - DisambiguateTypes.Environment.cons + DisambiguateTypes.Environment.add (DisambiguateTypes.Id id) (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri))) status.aliases | GrafiteAst.Symbol_alias (symb, instance, desc) -> - DisambiguateTypes.Environment.cons + DisambiguateTypes.Environment.add (DisambiguateTypes.Symbol (symb,instance)) (DisambiguateChoices.lookup_symbol_by_dsc symb desc) status.aliases | GrafiteAst.Number_alias (instance,desc) -> - DisambiguateTypes.Environment.cons + DisambiguateTypes.Environment.add (DisambiguateTypes.Num instance) (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases in @@ -648,7 +779,7 @@ let eval_command opts status cmd = | GrafiteAst.Interpretation (_, dsc, (symbol, _), _) as stm -> let status' = add_moo_content [stm] status in let aliases' = - DisambiguateTypes.Environment.cons + DisambiguateTypes.Environment.add (DisambiguateTypes.Symbol (symbol, 0)) (DisambiguateChoices.lookup_symbol_by_dsc symbol dsc) status.aliases @@ -800,7 +931,8 @@ let default_options () = let initial_status = lazy { - aliases = DisambiguateTypes.empty_environment; + aliases = DisambiguateTypes.Environment.empty; + multi_aliases = DisambiguateTypes.Environment.empty; moo_content_rev = []; proof_status = No_proof; options = default_options ();