X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=3658b0c20ab93d2990a9a73717faaf35c87bf463;hb=6e9833ff8664143f8916caf98f0818322e7ff9a1;hp=a9b46267f98c9ba1a032ce6a9315aac3d04cadfe;hpb=d1126c6b78a3333bbf415daf027004496b77c2f4;p=helm.git diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index a9b46267f..3658b0c20 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -24,6 +24,7 @@ *) open Printf + open MatitaTypes exception Drop;; @@ -156,7 +157,7 @@ let tactic_of_ast ast = | GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term let singleton = function - | [x] -> x + | [x], _ -> x | _ -> assert false let disambiguate_term status_ref term = @@ -164,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 @@ -183,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 @@ -192,9 +194,7 @@ let disambiguate_lazy_term status_ref term = cic, metasenv, ugraph) let disambiguate_pattern status_ref (wanted, hyp_paths, goal_path) = - let interp path = - Disambiguate.interpretate_path [] !status_ref.aliases path - in + let interp path = Disambiguate.interpretate_path [] path in let goal_path = interp goal_path in let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in let wanted = @@ -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) }, @@ -355,7 +485,7 @@ module MatitaStatus = let set_goals (status,_) goals = status,goals let id_tac status = - apply_tactic (GrafiteAst.IdTac Disambiguate.dummy_floc) status + apply_tactic (GrafiteAst.IdTac DisambiguateTypes.dummy_floc) status let mk_tactic tac = tac @@ -453,21 +583,18 @@ let eval_coercion status coercion = List.fold_left (fun s (uri,o,ugraph) -> MatitaSync.add_obj uri o status) status new_coercions in let statement_of name = - GrafiteAstPp.pp_statement - (GrafiteAst.Executable (Disambiguate.dummy_floc, - (GrafiteAst.Command (Disambiguate.dummy_floc, - (GrafiteAst.Coercion (Disambiguate.dummy_floc, - (CicNotationPt.Ident (name, None)))))))) ^ "\n" + GrafiteAst.Coercion (DisambiguateTypes.dummy_floc, + (CicNotationPt.Ident (name, None))) in - let moo_content_rev = - [statement_of (UriManager.name_of_uri coer_uri)] @ + let moo_content = + statement_of (UriManager.name_of_uri coer_uri) :: (List.map (fun (uri, _, _) -> statement_of (UriManager.name_of_uri uri)) - new_coercions) @ status.moo_content_rev + new_coercions) in - let status = {status with moo_content_rev = moo_content_rev} in - {status with proof_status = No_proof} + let status = add_moo_content moo_content status in + { status with proof_status = No_proof } let generate_elimination_principles uri status = let elim sort status = @@ -513,12 +640,9 @@ let disambiguate_obj status obj = | GrafiteAst.Inductive _ -> assert false | GrafiteAst.Theorem _ -> None in let (aliases, metasenv, cic, _) = - match - MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ()) - ~aliases:(status.aliases) ~uri obj - with - | [x] -> x - | _ -> assert false + singleton + (MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ()) + ~aliases:status.aliases ~universe:(Some status.multi_aliases) ~uri obj) in let proof_status = match status.proof_status with @@ -567,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 @@ -576,8 +702,7 @@ let eval_command opts status cmd = match cmd with | GrafiteAst.Default (loc, what, uris) as cmd -> LibraryObjects.set_default what uris; - {status with moo_content_rev = - (GrafiteAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev} + add_moo_content [cmd] status | GrafiteAst.Include (loc, path) -> let absolute_path = make_absolute opts.include_paths path in let moopath = MatitaMisc.obj_file_of_script absolute_path in @@ -586,7 +711,8 @@ let eval_command opts status cmd = raise (IncludedFileNotCompiled moopath) in let stream = Stream.of_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) -> @@ -612,7 +738,7 @@ let eval_command opts status cmd = set_option status name value | GrafiteAst.Drop loc -> raise Drop | GrafiteAst.Qed loc -> - let uri, metasenv, bo, ty = + let uri, metasenv, bo, ty = match status.proof_status with | Proof (Some uri, metasenv, body, ty) -> uri, metasenv, body, ty @@ -636,7 +762,7 @@ let eval_command opts status cmd = code in DisambiguatePp *) match spec with | GrafiteAst.Ident_alias (id,uri) -> - DisambiguateTypes.Environment.add + DisambiguateTypes.Environment.add (DisambiguateTypes.Id id) (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri))) status.aliases @@ -653,10 +779,16 @@ let eval_command opts status cmd = MatitaSync.set_proof_aliases status aliases | GrafiteAst.Render _ -> assert false (* ZACK: to be removed *) | GrafiteAst.Dump _ -> assert false (* ZACK: to be removed *) - | GrafiteAst.Interpretation _ - | GrafiteAst.Notation _ as stm -> - { status with moo_content_rev = - (GrafiteAstPp.pp_command stm ^ "\n") :: status.moo_content_rev } + | 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 + in + MatitaSync.set_proof_aliases status' aliases' + | GrafiteAst.Notation _ as stm -> add_moo_content [stm] status | GrafiteAst.Obj (loc,obj) -> let ext,name = match obj with @@ -713,7 +845,7 @@ let eval_command opts status cmd = if metasenv <> [] then command_error ( "metasenv not empty while giving a definition with body: " ^ - CicMetaSubst.ppmetasenv metasenv []); + CicMetaSubst.ppmetasenv [] metasenv); let status = MatitaSync.add_obj uri obj status in match obj with Cic.Constant _ -> status @@ -802,7 +934,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 ();