X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaEngine.ml;h=4e48df8072d13a027ea5dac975936fa884d91d1f;hb=86af949158e013178557c7fec7662ac06fae753c;hp=577e243a6744879152b0706965c3dde1ff8afddd;hpb=8ecc9fb74f80c2f5b3e3c70f0a625e63a48292fb;p=helm.git diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml index 577e243a6..4e48df807 100644 --- a/helm/matita/matitaEngine.ml +++ b/helm/matita/matitaEngine.ml @@ -65,8 +65,8 @@ let tactic_of_ast ast = | GrafiteAst.Absurd (_, term) -> Tactics.absurd term | GrafiteAst.Apply (_, term) -> Tactics.apply term | GrafiteAst.Assumption _ -> Tactics.assumption - | GrafiteAst.Auto (_,depth,width,paramodulation) -> - AutoTactic.auto_tac ?depth ?width ?paramodulation + | GrafiteAst.Auto (_,depth,width,paramodulation,full) -> + AutoTactic.auto_tac ?depth ?width ?paramodulation ?full ~dbd:(MatitaDb.instance ()) () | GrafiteAst.Change (_, pattern, with_what) -> Tactics.change ~pattern with_what @@ -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) @@ -227,8 +227,8 @@ let disambiguate_tactic status tactic = let cic = disambiguate_term status_ref term in GrafiteAst.Apply (loc, cic) | GrafiteAst.Assumption loc -> GrafiteAst.Assumption loc - | GrafiteAst.Auto (loc,depth,width,paramodulation) -> - GrafiteAst.Auto (loc,depth,width,paramodulation) + | 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 @@ -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, @@ -467,14 +597,19 @@ let eval_coercion status coercion = { 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 @@ -499,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 = @@ -509,7 +644,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 +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 @@ -574,14 +709,11 @@ let eval_command opts status cmd = | 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 @@ -621,40 +753,32 @@ 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.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 = @@ -713,22 +837,29 @@ let eval_command opts status cmd = 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 + 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 @@ -753,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 = @@ -760,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 @@ -781,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 () = (*