X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=b065040523bc2d46d3fa2b4f3db89d91a9611ca9;hb=28ac70d3f475442cda4ef30e0e9c0e6d012b2527;hp=19944417f048e440b7c5ac0ace0967fcef6cad7b;hpb=aa6153d8e480abfe52b00e1bc6bd48ef84c48988;p=helm.git diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 19944417f..b06504052 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -24,6 +24,7 @@ *) open Printf + open MatitaTypes exception Drop;; @@ -161,14 +162,15 @@ 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) ~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 - let status = MatitaSync.set_proof_aliases status aliases in + let status = MatitaSync.set_proof_aliases status diff in status_ref := status; cic @@ -180,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 ~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 + let status = MatitaSync.set_proof_aliases status diff in status_ref := status; cic, metasenv, ugraph) @@ -327,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) }, @@ -353,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 @@ -448,34 +580,36 @@ 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 = - 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 = - try - let uri,obj = CicElim.elim_of ~sort uri 0 in - MatitaSync.add_obj uri obj status - with CicElim.Can_t_eliminate -> status - in - List.fold_left (fun status sort -> elim sort status) status - [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ] + let status' = ref status in + let elim sort = + try + let uri,obj = CicElim.elim_of ~sort uri 0 in + status' := MatitaSync.add_obj uri obj !status' + with CicElim.Can_t_eliminate -> () + in + try + List.iter elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ]; + !status' + with exn -> + MatitaSync.time_travel ~present:!status' ~past:status; + raise exn let generate_projections uri fields status = let projections = CicRecord.projections_of uri fields in @@ -500,7 +634,7 @@ let generate_projections uri fields status = ) status projections (* to avoid a long list of recursive functions *) -let eval_from_stream_ref = ref (fun _ _ _ -> assert false);; +let eval_from_moo_ref = ref (fun _ _ _ -> assert false);; let disambiguate_obj status obj = let uri = @@ -510,10 +644,10 @@ 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) ~uri obj) + ~aliases:status.aliases ~universe:(Some status.multi_aliases) ~uri obj) in let proof_status = match status.proof_status with @@ -523,7 +657,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 @@ -571,19 +705,15 @@ 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 - let ic = - try open_in moopath with Sys_error _ -> - raise (IncludedFileNotCompiled moopath) in - let stream = Stream.of_channel ic in let status = ref status in - !eval_from_stream_ref status stream (fun _ _ -> ()); - close_in ic; - !status + if not (Sys.file_exists moopath) then + raise (IncludedFileNotCompiled moopath); + !eval_from_moo_ref status moopath (fun _ _ -> ()); + !status | GrafiteAst.Set (loc, name, value) -> let value = if name = "baseuri" then @@ -623,47 +753,33 @@ let eval_command opts status cmd = let name = UriManager.name_of_uri uri in let obj = Cic.Constant (name,Some bo,ty,[],[]) in MatitaSync.add_obj uri obj status - | GrafiteAst.Coercion (loc, coercion) -> - eval_coercion status coercion + | 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.cons - (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.cons - (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.cons - (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' = - { status with - moo_content_rev = - (GrafiteAstPp.pp_command stm ^ "\n") :: status.moo_content_rev } + let status' = add_moo_content [stm] status in + let diff = + [DisambiguateTypes.Symbol (symbol, 0), + DisambiguateChoices.lookup_symbol_by_dsc symbol dsc] in - let aliases' = - DisambiguateTypes.Environment.cons - (DisambiguateTypes.Symbol (symbol, 0)) - (DisambiguateChoices.lookup_symbol_by_dsc symbol dsc) - status.aliases - in - MatitaSync.set_proof_aliases status' aliases' - | GrafiteAst.Notation _ as stm -> - { status with moo_content_rev = - (GrafiteAstPp.pp_command stm ^ "\n") :: status.moo_content_rev } + MatitaSync.set_proof_aliases status' diff + | GrafiteAst.Notation _ as stm -> add_moo_content [stm] status | GrafiteAst.Obj (loc,obj) -> let ext,name = match obj with @@ -720,23 +836,30 @@ let eval_command opts status cmd = if metasenv <> [] then command_error ( "metasenv not empty while giving a definition with body: " ^ - CicMetaSubst.ppmetasenv metasenv []); - let status = MatitaSync.add_obj uri obj status in - match obj with - Cic.Constant _ -> status + CicMetaSubst.ppmetasenv [] metasenv); + let status' = ref status in + (try + status' := MatitaSync.add_obj uri obj !status'; + (match obj with + | Cic.Constant _ -> () | Cic.InductiveDefinition (_,_,_,attrs) -> - let status = generate_elimination_principles uri status in - let rec get_record_attrs = - function - [] -> None - | (`Class (`Record fields))::_ -> Some fields - | _::tl -> get_record_attrs tl - in + status' := generate_elimination_principles uri !status'; + let rec get_record_attrs = + function + | [] -> None + | (`Class (`Record fields))::_ -> Some fields + | _::tl -> get_record_attrs tl + in (match get_record_attrs attrs with - None -> status (* not a record *) - | Some fields -> generate_projections uri fields status) + | None -> () (* not a record *) + | Some fields -> + status' := generate_projections uri fields !status') | Cic.CurrentProof _ - | Cic.Variable _ -> assert false + | Cic.Variable _ -> assert false); + !status' + with exn -> + MatitaSync.time_travel ~present:!status' ~past:status; + raise exn) let eval_executable opts status ex = match ex with @@ -761,6 +884,22 @@ let eval_ast | GrafiteAst.Executable (_,ex) -> eval_executable opts status ex | GrafiteAst.Comment (_,c) -> eval_comment status c +let eval_from_moo ?do_heavy_checks ?include_paths ?clean_baseuri status fname + cb += + let moo = MatitaMoo.load_moo fname in + List.iter + (fun ast -> + let ast = + GrafiteAst.Executable (DisambiguateTypes.dummy_floc, + GrafiteAst.Command (DisambiguateTypes.dummy_floc, + (GrafiteAst.reash_cmd_uris ast))) + in + cb !status ast; + status := + eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast) + moo + let eval_from_stream ?do_heavy_checks ?include_paths ?clean_baseuri status str cb = @@ -768,12 +907,13 @@ let eval_from_stream while true do let ast = GrafiteParser.parse_statement str in cb !status ast; - status := eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast + status := + eval_ast ?do_heavy_checks ?include_paths ?clean_baseuri !status ast done with End_of_file -> () (* to avoid a long list of recursive functions *) -let _ = eval_from_stream_ref := eval_from_stream +let _ = eval_from_moo_ref := eval_from_moo let eval_from_stream_greedy ?do_heavy_checks ?include_paths ?clean_baseuri status str cb @@ -789,7 +929,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 () = (* @@ -809,7 +950,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 ();