X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=707e31d988fff576c60795d8a257b6f1ec380179;hb=5b32b7905bc78c11e353efd68137b8eb7b6ac73b;hp=577e243a6744879152b0706965c3dde1ff8afddd;hpb=8ecc9fb74f80c2f5b3e3c70f0a625e63a48292fb;p=helm.git diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 577e243a6..707e31d98 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -162,7 +162,7 @@ let singleton = function let disambiguate_term status_ref term = let status = !status_ref in - let (aliases, metasenv, cic, _) = + let (diff, metasenv, cic, _) = singleton (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ()) ~aliases:status.aliases ~universe:(Some status.multi_aliases) @@ -170,7 +170,7 @@ let disambiguate_term status_ref term = ~metasenv:(MatitaMisc.get_proof_metasenv status) term) in let status = MatitaTypes.set_metasenv metasenv status in - let status = MatitaSync.set_proof_aliases status aliases in + let status = MatitaSync.set_proof_aliases status diff in status_ref := status; cic @@ -182,14 +182,14 @@ let disambiguate_term status_ref term = let disambiguate_lazy_term status_ref term = (fun context metasenv ugraph -> let status = !status_ref in - let (aliases, metasenv, cic, ugraph) = + let (diff, metasenv, cic, ugraph) = singleton (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ()) ~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 + let status = MatitaSync.set_proof_aliases status diff in status_ref := status; cic, metasenv, ugraph) @@ -329,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) }, @@ -450,7 +580,7 @@ let eval_coercion status coercion = (* also adds them to the Db *) CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri in let status = - List.fold_left (fun s (uri,o,ugraph) -> MatitaSync.add_obj uri o status) + List.fold_left (fun s (uri,o,_) -> MatitaSync.add_obj uri o status) status new_coercions in let statement_of name = GrafiteAst.Coercion (DisambiguateTypes.dummy_floc, @@ -509,7 +639,7 @@ let disambiguate_obj status obj = Some (UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".ind")) | GrafiteAst.Inductive _ -> assert false | GrafiteAst.Theorem _ -> None in - let (aliases, metasenv, cic, _) = + let (diff, metasenv, cic, _) = singleton (MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ()) ~aliases:status.aliases ~universe:(Some status.multi_aliases) ~uri obj) @@ -522,7 +652,7 @@ let disambiguate_obj status obj = | Intermediate _ -> assert false in let status = { status with proof_status = proof_status } in - let status = MatitaSync.set_proof_aliases status aliases in + let status = MatitaSync.set_proof_aliases status diff in status, cic let disambiguate_command status = function @@ -561,6 +691,8 @@ let make_absolute paths path = with Unix.Unix_error _ as exc -> raise (UnableToInclude path) ;; +let profiler_include = CicUtil.profile "include" + let eval_command opts status cmd = let status,cmd = disambiguate_command status cmd in let cmd,notation_ids' = CicNotation.process_notation cmd in @@ -577,9 +709,10 @@ let eval_command opts status cmd = let ic = try open_in moopath with Sys_error _ -> raise (IncludedFileNotCompiled moopath) in - let stream = Stream.of_channel ic in + let stream = Ulexing.from_utf8_channel ic in let status = ref status in - !eval_from_stream_ref status stream (fun _ _ -> ()); + profiler_include.CicUtil.profile + (!eval_from_stream_ref status stream) (fun _ _ -> ()); close_in ic; !status | GrafiteAst.Set (loc, name, value) -> @@ -624,37 +757,30 @@ let eval_command opts status cmd = | GrafiteAst.Coercion (loc, coercion) -> eval_coercion status coercion | GrafiteAst.Alias (loc, spec) -> - let aliases = + let diff = (*CSC: Warning: this code should be factorized with the corresponding code in DisambiguatePp *) match spec with | GrafiteAst.Ident_alias (id,uri) -> - DisambiguateTypes.Environment.add - (DisambiguateTypes.Id id) - (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri))) - status.aliases + [DisambiguateTypes.Id id, + (uri,(fun _ _ _-> CicUtil.term_of_uri(UriManager.uri_of_string uri)))] | GrafiteAst.Symbol_alias (symb, instance, desc) -> - DisambiguateTypes.Environment.add - (DisambiguateTypes.Symbol (symb,instance)) - (DisambiguateChoices.lookup_symbol_by_dsc symb desc) - status.aliases + [DisambiguateTypes.Symbol (symb,instance), + DisambiguateChoices.lookup_symbol_by_dsc symb desc] | GrafiteAst.Number_alias (instance,desc) -> - DisambiguateTypes.Environment.add - (DisambiguateTypes.Num instance) - (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases + [DisambiguateTypes.Num instance, + DisambiguateChoices.lookup_num_by_dsc desc] in - MatitaSync.set_proof_aliases status aliases + MatitaSync.set_proof_aliases status diff | GrafiteAst.Render _ -> assert false (* ZACK: to be removed *) | GrafiteAst.Dump _ -> assert false (* ZACK: to be removed *) | GrafiteAst.Interpretation (_, dsc, (symbol, _), _) as stm -> let status' = add_moo_content [stm] status in - let aliases' = - DisambiguateTypes.Environment.add - (DisambiguateTypes.Symbol (symbol, 0)) - (DisambiguateChoices.lookup_symbol_by_dsc symbol dsc) - status.aliases + let diff = + [DisambiguateTypes.Symbol (symbol, 0), + DisambiguateChoices.lookup_symbol_by_dsc symbol dsc] in - MatitaSync.set_proof_aliases status' aliases' + MatitaSync.set_proof_aliases status' diff | GrafiteAst.Notation _ as stm -> add_moo_content [stm] status | GrafiteAst.Obj (loc,obj) -> let ext,name = @@ -781,7 +907,8 @@ let eval_from_stream_greedy let eval_string ?do_heavy_checks ?include_paths ?clean_baseuri status str = eval_from_stream - ?do_heavy_checks ?include_paths ?clean_baseuri status (Stream.of_string str) (fun _ _ ->()) + ?do_heavy_checks ?include_paths ?clean_baseuri status + (Ulexing.from_utf8_string str) (fun _ _ ->()) let default_options () = (*