From: Claudio Sacerdoti Coen Date: Sat, 25 Apr 2009 23:11:35 +0000 (+0000) Subject: It is now possible for commands processed by grafiteEngine to either return X-Git-Tag: make_still_working~4046 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7233348f05485c2ee317df9c3407cf1ce7e56927;p=helm.git It is now possible for commands processed by grafiteEngine to either return uris for an old object or for a new one. This information is only used to generate preferences. --- diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index ebba1988d..6b341f77c 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -414,7 +414,7 @@ type eval_ast = GrafiteTypes.status -> (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement) disambiguator_input -> - GrafiteTypes.status * UriManager.uri list + GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list] } type 'a eval_command = @@ -424,7 +424,7 @@ type 'a eval_command = GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) -> options -> GrafiteTypes.status -> (('term,'obj) GrafiteAst.command) disambiguator_input -> - GrafiteTypes.status * UriManager.uri list + GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list] } type 'a eval_comment = @@ -434,7 +434,7 @@ type 'a eval_comment = GrafiteTypes.status * (Cic.term,Cic.obj) GrafiteAst.command) -> options -> GrafiteTypes.status -> (('term,'lazy_term,'reduction_kind,'obj,'ident) GrafiteAst.comment) disambiguator_input -> - GrafiteTypes.status * UriManager.uri list + GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list] } type 'a eval_executable = @@ -460,7 +460,7 @@ type 'a eval_executable = options -> GrafiteTypes.status -> (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.code) disambiguator_input -> - GrafiteTypes.status * UriManager.uri list + GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list] } type 'a eval_from_moo = @@ -473,7 +473,7 @@ let coercion_moo_statement_of (uri,arity, saturations,_) = let eval_unification_hint status t n = (* XXX no undo *) NCicUnifHint.add_user_provided_hint t n; - status,[] + status,`Old [] ;; let add_coercions_of_lemmas lemmas status = @@ -514,7 +514,7 @@ let eval_prefer_coercion status c = let status = GrafiteSync.prefer_coercion status uri in let moo_content = GrafiteAst.PreferCoercion (HExtlib.dummy_floc,c) in let status = GrafiteTypes.add_moo_content [moo_content] status in - status, [] + status, `Old [] module MatitaStatus = struct @@ -648,9 +648,9 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status prerr_endline msg; *) let status = GrafiteTypes.add_moo_content [cmd] status in - status,[] + status,`Old [] | GrafiteAst.Select (_,uri) as cmd -> - if List.mem cmd status.GrafiteTypes.moo_content_rev then status, [] + if List.mem cmd status.GrafiteTypes.moo_content_rev then status, `Old [] else let cache = AutomationCache.add_term_to_active status.GrafiteTypes.automation_cache @@ -658,31 +658,36 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status in let status = { status with GrafiteTypes.automation_cache = cache } in let status = GrafiteTypes.add_moo_content [cmd] status in - status, [] + status, `Old [] | GrafiteAst.Pump (_,steps) -> let cache = AutomationCache.pump status.GrafiteTypes.automation_cache steps in let status = { status with GrafiteTypes.automation_cache = cache } in - status, [] + status, `Old [] | GrafiteAst.PreferCoercion (loc, coercion) -> eval_prefer_coercion status coercion | GrafiteAst.Coercion (loc, uri, add_composites, arity, saturations) -> - eval_coercion status ~add_composites uri arity saturations + let res,uris = + eval_coercion status ~add_composites uri arity saturations + in + res,`Old uris | GrafiteAst.Inverter (loc, name, indty, params) -> let buri = GrafiteTypes.get_baseuri status in let uri = UriManager.uri_of_string (buri ^ "/" ^ name ^ ".con") in let indty_uri = try CicUtil.uri_of_term indty with Invalid_argument _ -> - raise (Invalid_argument "not an inductive type to invert") + raise (Invalid_argument "not an inductive type to invert") in + let res,uris = + Inversion_principle.build_inverter ~add_obj status uri indty_uri params in - Inversion_principle.build_inverter ~add_obj status uri indty_uri params + res,`Old uris | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n | GrafiteAst.Default (loc, what, uris) as cmd -> LibraryObjects.set_default what uris; - GrafiteTypes.add_moo_content [cmd] status,[] + GrafiteTypes.add_moo_content [cmd] status,`Old [] | GrafiteAst.Drop loc -> raise Drop | GrafiteAst.Include (loc, baseuri) -> let moopath_rw, moopath_r = @@ -711,12 +716,12 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status in prerr_endline msg; *) - status,[] + status,`Old [] | GrafiteAst.Print (_,"proofterm") -> let _,_,_,p,_, _ = GrafiteTypes.get_current_proof status in prerr_endline (Auto.pp_proofterm (Lazy.force p)); - status,[] - | GrafiteAst.Print (_,_) -> status,[] + status,`Old [] + | GrafiteAst.Print (_,_) -> status,`Old [] | GrafiteAst.Qed loc -> let uri, metasenv, _subst, bo, ty, attrs = match status.GrafiteTypes.proof_status with @@ -740,7 +745,7 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}, (*CSC: I throw away the arities *) - uri::lemmas + `Old (uri::lemmas) | GrafiteAst.NQed loc -> (match status.GrafiteTypes.ng_status with | GrafiteTypes.ProofMode @@ -758,12 +763,12 @@ prerr_endline "CSC: here we should fix the height!!!"; NCicLibrary.add_obj uri obj; {status with GrafiteTypes.ng_status = - GrafiteTypes.CommandMode lexicon_status },[] + GrafiteTypes.CommandMode lexicon_status },`Old [] | _ -> raise (GrafiteTypes.Command_error "Not in proof mode")) | GrafiteAst.Relation (loc, id, a, aeq, refl, sym, trans) -> Setoids.add_relation id a aeq refl sym trans; - status, [] (*CSC: TO BE FIXED *) - | GrafiteAst.Set (loc, name, value) -> status, [] + status, `Old [] (*CSC: TO BE FIXED *) + | GrafiteAst.Set (loc, name, value) -> status, `Old [] (* GrafiteTypes.set_option status name value,[] *) | GrafiteAst.NObj (loc,obj) -> let lexicon_status = @@ -783,7 +788,8 @@ prerr_endline "CSC: here we should fix the height!!!"; in NCicLibrary.add_obj uri obj; {status with - GrafiteTypes.ng_status=GrafiteTypes.CommandMode lexicon_status },[] + GrafiteTypes.ng_status=GrafiteTypes.CommandMode lexicon_status }, + `Old [] | _ -> let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in { status with @@ -791,7 +797,7 @@ prerr_endline "CSC: here we should fix the height!!!"; GrafiteTypes.ProofMode { NTacStatus.gstatus = ninitial_stack; istatus = { NTacStatus.pstatus = obj; lstatus = lexicon_status}} - },[]) + },`Old []) | GrafiteAst.Obj (loc,obj) -> let ext,name = match obj with @@ -845,18 +851,16 @@ prerr_endline "CSC: here we should fix the height!!!"; GrafiteTypes.Incomplete_proof { GrafiteTypes.proof = initial_proof; stack = initial_stack } ; }, - [] + `Old [] | _ -> if metasenv <> [] then raise (GrafiteTypes.Command_error ( "metasenv not empty while giving a definition with body: " ^ CicMetaSubst.ppmetasenv [] metasenv)); let status, lemmas = add_obj uri obj status in - let status,new_lemmas = - add_coercions_of_lemmas lemmas status - in + let status,new_lemmas = add_coercions_of_lemmas lemmas status in {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}, - uri::new_lemmas@lemmas + `Old (uri::new_lemmas@lemmas) in match status.GrafiteTypes.proof_status with GrafiteTypes.Intermediate _ -> @@ -879,10 +883,10 @@ prerr_endline "CSC: here we should fix the height!!!"; print_endline "GOOD"; () with ProofEngineTypes.Fail _ -> print_endline "BAD" | _ -> ());*) eval_tactical status - (punctuation_tactical_of_ast (text,prefix_len,punct)),[] + (punctuation_tactical_of_ast (text,prefix_len,punct)),`Old [] | GrafiteAst.Tactic (_, None, punct) -> eval_tactical status - (punctuation_tactical_of_ast (text,prefix_len,punct)),[] + (punctuation_tactical_of_ast (text,prefix_len,punct)),`Old [] | GrafiteAst.NTactic (_(*loc*), tac, punct) -> (match status.GrafiteTypes.ng_status with | GrafiteTypes.CommandMode _ -> assert false @@ -890,14 +894,14 @@ prerr_endline "CSC: here we should fix the height!!!"; let nstatus = eval_ng_tac (text,prefix_len,tac) nstatus in let nstatus = eval_ng_punct (text,prefix_len,punct) nstatus in NTacStatus.pp_tac_status nstatus; - { status with GrafiteTypes.ng_status = GrafiteTypes.ProofMode nstatus }, []) + { status with GrafiteTypes.ng_status = GrafiteTypes.ProofMode nstatus }, `Old []) | GrafiteAst.NonPunctuationTactical (_, tac, punct) -> let status = eval_tactical status (non_punctuation_tactical_of_ast (text,prefix_len,tac)) in eval_tactical status - (punctuation_tactical_of_ast (text,prefix_len,punct)),[] + (punctuation_tactical_of_ast (text,prefix_len,punct)),`Old [] | GrafiteAst.Command (_, cmd) -> eval_command.ec_go ~disambiguate_command opts status (text,prefix_len,cmd) | GrafiteAst.Macro (loc, macro) -> @@ -920,7 +924,7 @@ prerr_endline "CSC: here we should fix the height!!!"; ~disambiguate_macro:(fun _ _ -> assert false) status ast in - assert (lemmas=[]); + assert (lemmas=`Old []); status) status moo } and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command @@ -935,7 +939,7 @@ prerr_endline "CSC: here we should fix the height!!!"; | GrafiteAst.Comment (_,c) -> eval_comment.ecm_go ~disambiguate_command opts status (text,prefix_len,c) } and eval_comment = { ecm_go = fun ~disambiguate_command opts status (text,prefix_len,c) -> - status, [] + status, `Old [] } ;; diff --git a/helm/software/components/grafite_engine/grafiteEngine.mli b/helm/software/components/grafite_engine/grafiteEngine.mli index 993ccda71..de7fb2790 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.mli +++ b/helm/software/components/grafite_engine/grafiteEngine.mli @@ -55,5 +55,5 @@ val eval_ast : (('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement) disambiguator_input -> (* the new status and generated objects, if any *) - GrafiteTypes.status * UriManager.uri list + GrafiteTypes.status * [`Old of UriManager.uri list | `New of NUri.uri list] diff --git a/helm/software/components/lexicon/lexiconSync.ml b/helm/software/components/lexicon/lexiconSync.ml index a3a0d766e..f99535d19 100644 --- a/helm/software/components/lexicon/lexiconSync.ml +++ b/helm/software/components/lexicon/lexiconSync.ml @@ -85,11 +85,14 @@ let add_aliases_for_object status uri = | Cic.Variable _ | Cic.CurrentProof _ -> assert false -let add_aliases_for_objs = - List.fold_left - (fun status uri -> - let obj,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in - add_aliases_for_object status uri obj) +let add_aliases_for_objs status = + function + `Old uris -> + List.fold_left + (fun status uri -> + let obj,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in + add_aliases_for_object status uri obj) status uris + | `New nrefs -> assert false module OrderedId = struct diff --git a/helm/software/components/lexicon/lexiconSync.mli b/helm/software/components/lexicon/lexiconSync.mli index fd3892747..c2ff15c42 100644 --- a/helm/software/components/lexicon/lexiconSync.mli +++ b/helm/software/components/lexicon/lexiconSync.mli @@ -24,7 +24,8 @@ *) val add_aliases_for_objs: - LexiconEngine.status -> UriManager.uri list -> LexiconEngine.status + LexiconEngine.status -> [`Old of UriManager.uri list | `New of NUri.uri list]-> + LexiconEngine.status val time_travel: present:LexiconEngine.status -> past:LexiconEngine.status -> unit