From 70aa6dc959dc1d49f751c183367c3b73393c938b Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 4 Nov 2010 13:36:47 +0000 Subject: [PATCH] - Print/Set commands removed - stupid bug fixed in interpretations: we did not add the new id to the id list, so that only the first interpretation was considered - added a new field to the interpretations status to record the recently added aliases that need to be made explicit in the script; much better than what we did before (alias diffing) --- matita/components/content/interpretations.ml | 2 +- matita/components/grafite/grafiteAst.ml | 9 +-- matita/components/grafite/grafiteAstPp.ml | 5 -- matita/components/grafite/grafiteAstPp.mli | 1 - .../grafite_engine/grafiteEngine.ml | 70 +++++++++---------- .../grafite_engine/grafiteEngine.mli | 9 +-- .../grafite_parser/grafiteDisambiguate.ml | 9 ++- matita/components/lexicon/lexiconEngine.ml | 8 ++- matita/components/lexicon/lexiconEngine.mli | 1 + matita/components/lexicon/lexiconSync.ml | 23 +----- matita/components/lexicon/lexiconSync.mli | 8 --- matita/components/lexicon/lexiconTypes.ml | 6 +- matita/components/lexicon/lexiconTypes.mli | 3 +- matita/components/library/libraryClean.ml | 2 +- .../ng_cic_content/nTermCicContent.mli | 60 ---------------- matita/matita/matitaEngine.ml | 24 +++---- 16 files changed, 69 insertions(+), 171 deletions(-) diff --git a/matita/components/content/interpretations.ml b/matita/components/content/interpretations.ml index aaa87d083..28957074f 100644 --- a/matita/components/content/interpretations.ml +++ b/matita/components/content/interpretations.ml @@ -122,7 +122,7 @@ let add_interpretation (status : #status) dsc (symbol, args) appl_pattern = let status,id = fresh_id status in let ids = try - StringMap.find symbol status#interp_db.interpretations + id::StringMap.find symbol status#interp_db.interpretations with Not_found -> [id] in let status = status#set_interp_db { status#interp_db with diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml index 173912e1f..e251ae557 100644 --- a/matita/components/grafite/grafiteAst.ml +++ b/matita/components/grafite/grafiteAst.ml @@ -86,10 +86,6 @@ let magic = 35 (* composed magic: term + command magics. No need to change this value *) let magic = magic + 10000 * NotationPt.magic -type command = - | Set of loc * string * string - | Print of loc * string - type alias_spec = | Ident_alias of string * string (* identifier, uri *) | Symbol_alias of string * int * string (* name, instance no, description *) @@ -97,7 +93,7 @@ type alias_spec = type inclusion_mode = WithPreferences | WithoutPreferences (* aka aliases *) -type ncommand = +type command = | Include of loc * inclusion_mode * string (* _,buri,_,path *) | UnificationHint of loc * NotationPt.term * int (* term, precedence *) | NObj of loc * NotationPt.term NotationPt.obj @@ -121,8 +117,7 @@ type ncommand = (* description (i.e. id), symbol, arg pattern, appl pattern *) type code = - | Command of loc * command - | NCommand of loc * ncommand + | NCommand of loc * command | NMacro of loc * nmacro | NTactic of loc * ntactic list diff --git a/matita/components/grafite/grafiteAstPp.ml b/matita/components/grafite/grafiteAstPp.ml index 4ea07a54f..bd846248b 100644 --- a/matita/components/grafite/grafiteAstPp.ml +++ b/matita/components/grafite/grafiteAstPp.ml @@ -187,16 +187,11 @@ let pp_ncommand = function pp_notation dir_opt l1_pattern assoc prec l2_pattern ;; -let pp_command = function - | Print (_,s) -> "print " ^ s - | Set (_, name, value) -> Printf.sprintf "set \"%s\" \"%s\"" name value - let pp_executable ~map_unicode_to_tex = function | NMacro (_, macro) -> pp_nmacro macro ^ "." | NTactic (_,tacl) -> String.concat " " (List.map (pp_ntactic ~map_unicode_to_tex) tacl) - | Command (_, cmd) -> pp_command cmd ^ "." | NCommand (_, cmd) -> pp_ncommand cmd ^ "." let pp_comment ~map_unicode_to_tex = diff --git a/matita/components/grafite/grafiteAstPp.mli b/matita/components/grafite/grafiteAstPp.mli index 19de8bc8c..a695b20d2 100644 --- a/matita/components/grafite/grafiteAstPp.mli +++ b/matita/components/grafite/grafiteAstPp.mli @@ -23,7 +23,6 @@ * http://helm.cs.unibo.it/ *) -val pp_command: GrafiteAst.command -> string val pp_comment: map_unicode_to_tex:bool -> GrafiteAst.comment -> string val pp_executable: map_unicode_to_tex:bool -> GrafiteAst.code -> string diff --git a/matita/components/grafite_engine/grafiteEngine.ml b/matita/components/grafite_engine/grafiteEngine.ml index a70e78855..b471bece3 100644 --- a/matita/components/grafite_engine/grafiteEngine.ml +++ b/matita/components/grafite_engine/grafiteEngine.ml @@ -57,7 +57,7 @@ let eval_unification_hint status t n = let status = basic_eval_unification_hint (t,n) status in let dump = inject_unification_hint (t,n)::status#dump in let status = status#set_dump dump in - status,[] + status ;; let basic_index_obj l status = @@ -197,7 +197,7 @@ let eval_add_constraint status u1 u2 = let status = basic_eval_add_constraint (u1,u2) status in let dump = inject_constraint (u1,u2)::status#dump in let status = status#set_dump dump in - status,[] + status ;; let eval_ng_tac tac = @@ -300,12 +300,15 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = GrafiteTypes.Serializer.require ~baseuri:(NUri.uri_of_string baseuri) status in let status = status#set_dump (obj::status#dump) in - assert false (* mode must be passed to GrafiteTypes.Serializer.require + assert false; (* mode must be passed to GrafiteTypes.Serializer.require somehow *) - status,[] + status | GrafiteAst.UnificationHint (loc, t, n) -> eval_unification_hint status t n | GrafiteAst.NCoercion (loc, name, t, ty, source, target) -> + let status, composites = NCicCoercDeclaration.eval_ncoercion status name t ty source target + in + LexiconSync.add_aliases_for_objs status composites | GrafiteAst.NQed loc -> if status#ng_mode <> `ProofMode then raise (GrafiteTypes.Command_error "Not in proof mode") @@ -376,11 +379,11 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = *) let status = status#set_ng_mode `CommandMode in let status = LexiconSync.add_aliases_for_objs status [uri] in - let status,uris = + let status = List.fold_left - (fun (status,uris) boxml -> + (fun status boxml -> try - let nstatus,nuris = + let nstatus = eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NObj (HExtlib.dummy_floc,boxml)) in @@ -388,16 +391,16 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = begin (*HLog.warn "error in generating projection/eliminator";*) assert(status#ng_mode = `CommandMode); - status, uris + status end else - nstatus, uris@nuris + nstatus with | MultiPassDisambiguator.DisambiguationError _ | NCicTypeChecker.TypeCheckerFailure _ -> (*HLog.warn "error in generating projection/eliminator";*) - status,uris - ) (status,[] (* uris *)) boxml in + status + ) status boxml in let _,_,_,_,nobj = obj in let status = match nobj with NCic.Inductive (is_ind,leftno,[it],_) -> @@ -412,10 +415,10 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = (snd (NCicElim.ast_of_sort outsort))) is_ind it leftno outsort status status#baseuri in let _,_,menv,_,_ = invobj in - fst (match menv with + (match menv with [] -> eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) - | _ -> status,[])) + | _ -> status)) (* XXX *) with _ -> (*HLog.warn "error in generating inversion principle"; *) let status = status#set_ng_mode `CommandMode in status) @@ -433,9 +436,9 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = (fun (name,is_coercion,arity) -> if is_coercion then Some(name,leftno,arity) else None) fields | _ -> [] in - let status,uris = + let status = List.fold_left - (fun (status,uris) (name,cpos,arity) -> + (fun status (name,cpos,arity) -> try let metasenv,subst,status,t = GrafiteDisambiguate.disambiguate_nterm None status [] [] [] @@ -446,14 +449,13 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = basic_eval_and_record_ncoercion_from_t_cpos_arity status (name,t,cpos,arity) in - let uris = nuris@uris in - status, uris + LexiconSync.add_aliases_for_objs status nuris with MultiPassDisambiguator.DisambiguationError _-> HLog.warn ("error in generating coercion: "^name); - status, uris) - (status,uris) coercions + status) + status coercions in - status,uris + status with exn -> NCicLibrary.time_travel old_status; @@ -505,7 +507,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = (match nmenv with [] -> eval_ncommand ~include_paths opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) - | _ -> status,[]) + | _ -> status) | GrafiteAst.NDiscriminator (_,_) -> assert false (*(loc, indty) -> if status#ng_mode <> `CommandMode then raise (GrafiteTypes.Command_error "Not in command mode") @@ -593,8 +595,10 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = let diff = [DisambiguateTypes.Symbol (symbol, 0), GrafiteAst.Symbol_alias (symbol,0,dsc)] in - let status = LexiconEngine.set_proof_aliases status mode diff in - status, [] + let status = + LexiconEngine.set_proof_aliases status ~implicit_aliases:false mode diff + in + status (*assert false*) (* MANCA SALVATAGGIO SU DISCO CHE DEVE TENERE IN CONTO IL MODE WithPreference/WithOutPreferences*) | GrafiteAst.Notation (loc, dir, l1, associativity, precedence, l2) -> @@ -618,7 +622,7 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = status in (* assert false (* MANCA SALVATAGGIO SU DISCO *) *) - status, [] (* capire [] XX *) + status (* capire [] XX *) | GrafiteAst.Alias (loc, spec) -> let diff = (*CSC: Warning: this code should be factorized with the corresponding @@ -632,21 +636,13 @@ let rec eval_ncommand ~include_paths opts status (text,prefix_len,cmd) = [DisambiguateTypes.Num instance,spec] in let mode = assert false in (* VEDI SOPRA *) - LexiconEngine.set_proof_aliases status mode diff; + LexiconEngine.set_proof_aliases status ~implicit_aliases:false mode diff; assert false (* MANCA SALVATAGGIO SU DISCO *) ;; -let eval_comment opts status (text,prefix_len,c) = status, [] - -let rec eval_command opts status (text,prefix_len,cmd) = - let status,uris = - match cmd with - | GrafiteAst.Print (_,_) -> status,[] - | GrafiteAst.Set (loc, name, value) -> status, [] - in - status,uris +let eval_comment opts status (text,prefix_len,c) = status -and eval_executable ~include_paths opts status (text,prefix_len,ex) = +let rec eval_executable ~include_paths opts status (text,prefix_len,ex) = match ex with | GrafiteAst.NTactic (_(*loc*), tacl) -> if status#ng_mode <> `ProofMode then @@ -659,9 +655,7 @@ and eval_executable ~include_paths opts status (text,prefix_len,ex) = subst_metasenv_and_fix_names status) status tacl in - status,[] - | GrafiteAst.Command (_, cmd) -> - eval_command opts status (text,prefix_len,cmd) + status | GrafiteAst.NCommand (_, cmd) -> eval_ncommand ~include_paths opts status (text,prefix_len,cmd) | GrafiteAst.NMacro (loc, macro) -> diff --git a/matita/components/grafite_engine/grafiteEngine.mli b/matita/components/grafite_engine/grafiteEngine.mli index 9b1979970..ae2c9e814 100644 --- a/matita/components/grafite_engine/grafiteEngine.mli +++ b/matita/components/grafite_engine/grafiteEngine.mli @@ -28,9 +28,6 @@ exception NMacro of GrafiteAst.loc * GrafiteAst.nmacro type 'a disambiguator_input = string * int * 'a val eval_ast : - include_paths:string list -> - ?do_heavy_checks:bool -> - GrafiteTypes.status -> - GrafiteAst.statement disambiguator_input -> - (* the new status and generated objects, if any *) - GrafiteTypes.status * NUri.uri list + include_paths:string list -> ?do_heavy_checks:bool -> + GrafiteTypes.status -> GrafiteAst.statement disambiguator_input -> + GrafiteTypes.status diff --git a/matita/components/grafite_parser/grafiteDisambiguate.ml b/matita/components/grafite_parser/grafiteDisambiguate.ml index f82759195..58a241e3f 100644 --- a/matita/components/grafite_parser/grafiteDisambiguate.ml +++ b/matita/components/grafite_parser/grafiteDisambiguate.ml @@ -138,7 +138,8 @@ let disambiguate_nterm expty estatus context metasenv subst thing ~context ~metasenv ~subst thing) in let estatus = - LexiconEngine.set_proof_aliases estatus GrafiteAst.WithPreferences diff + LexiconEngine.set_proof_aliases estatus ~implicit_aliases:true + GrafiteAst.WithPreferences diff in metasenv, subst, estatus, cic ;; @@ -219,7 +220,9 @@ let disambiguate_nobj estatus ?baseuri (text,prefix_len,obj) = ~aliases:estatus#lstatus.LexiconTypes.aliases ~universe:(Some estatus#lstatus.LexiconTypes.multi_aliases) (text,prefix_len,obj)) in - let estatus = LexiconEngine.set_proof_aliases estatus - GrafiteAst.WithPreferences diff in + let estatus = + LexiconEngine.set_proof_aliases estatus ~implicit_aliases:true + GrafiteAst.WithPreferences diff + in estatus, cic ;; diff --git a/matita/components/lexicon/lexiconEngine.ml b/matita/components/lexicon/lexiconEngine.ml index ce7e4e2aa..64f91ad25 100644 --- a/matita/components/lexicon/lexiconEngine.ml +++ b/matita/components/lexicon/lexiconEngine.ml @@ -31,7 +31,7 @@ let dump_aliases out msg status = (fun _ x -> out (GrafiteAstPp.pp_alias x)) status#lstatus.LexiconTypes.aliases -let set_proof_aliases status mode new_aliases = +let set_proof_aliases status ~implicit_aliases mode new_aliases = if mode = GrafiteAst.WithoutPreferences then status else @@ -50,6 +50,10 @@ let set_proof_aliases status mode new_aliases = status#lstatus.LexiconTypes.multi_aliases new_aliases in let new_status = - {LexiconTypes.multi_aliases = multi_aliases ; aliases = aliases} + {LexiconTypes.multi_aliases = multi_aliases ; + aliases = aliases; + new_aliases = + (if implicit_aliases then new_aliases else []) @ + status#lstatus.LexiconTypes.new_aliases} in status#set_lstatus new_status diff --git a/matita/components/lexicon/lexiconEngine.mli b/matita/components/lexicon/lexiconEngine.mli index 6209ce40d..c09fc9806 100644 --- a/matita/components/lexicon/lexiconEngine.mli +++ b/matita/components/lexicon/lexiconEngine.mli @@ -25,6 +25,7 @@ val set_proof_aliases: #LexiconTypes.status as 'status -> + implicit_aliases:bool -> (* implicit ones are made explicit *) GrafiteAst.inclusion_mode -> (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list -> 'status diff --git a/matita/components/lexicon/lexiconSync.ml b/matita/components/lexicon/lexiconSync.ml index 322279769..9a5ff7633 100644 --- a/matita/components/lexicon/lexiconSync.ml +++ b/matita/components/lexicon/lexiconSync.ml @@ -25,26 +25,6 @@ (* $Id$ *) -let alias_diff ~from status = - let module Map = DisambiguateTypes.Environment in - Map.fold - (fun domain_item codomain_item acc -> - let description1 = GrafiteAst.description_of_alias codomain_item in - try - let description2 = - GrafiteAst.description_of_alias - (Map.find domain_item from#lstatus.LexiconTypes.aliases) - in - if description1 <> description2 then - (domain_item,codomain_item)::acc - else - acc - with - Not_found -> - (domain_item,codomain_item)::acc) - status#lstatus.LexiconTypes.aliases [] -;; - let add_aliases_for_objs status = List.fold_left (fun status nref -> @@ -57,5 +37,6 @@ let add_aliases_for_objs status = GrafiteAst.Ident_alias (name,NReference.string_of_reference u) ) references in - LexiconEngine.set_proof_aliases status GrafiteAst.WithPreferences new_env + LexiconEngine.set_proof_aliases status ~implicit_aliases:false + GrafiteAst.WithPreferences new_env ) status diff --git a/matita/components/lexicon/lexiconSync.mli b/matita/components/lexicon/lexiconSync.mli index f19906528..f9ed52406 100644 --- a/matita/components/lexicon/lexiconSync.mli +++ b/matita/components/lexicon/lexiconSync.mli @@ -25,11 +25,3 @@ val add_aliases_for_objs: #LexiconTypes.status as 'status -> NUri.uri list -> 'status - - (** perform a diff between the aliases contained in two statuses, assuming - * that the second one can only have more aliases than the first one - * @return the list of aliases that should be added to aliases of from in - * order to be equal to aliases of the second argument *) -val alias_diff: - from:#LexiconTypes.status -> #LexiconTypes.status -> - (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list diff --git a/matita/components/lexicon/lexiconTypes.ml b/matita/components/lexicon/lexiconTypes.ml index 5e6a0a326..3aa2dadab 100644 --- a/matita/components/lexicon/lexiconTypes.ml +++ b/matita/components/lexicon/lexiconTypes.ml @@ -27,12 +27,14 @@ type lexicon_status = { aliases: GrafiteAst.alias_spec DisambiguateTypes.Environment.t; - multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t + multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t; + new_aliases: (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list } let initial_status = { aliases = DisambiguateTypes.Environment.empty; - multi_aliases = DisambiguateTypes.Environment.empty + multi_aliases = DisambiguateTypes.Environment.empty; + new_aliases = [] } class type g_status = diff --git a/matita/components/lexicon/lexiconTypes.mli b/matita/components/lexicon/lexiconTypes.mli index 813b9955b..b94aa076f 100644 --- a/matita/components/lexicon/lexiconTypes.mli +++ b/matita/components/lexicon/lexiconTypes.mli @@ -25,7 +25,8 @@ type lexicon_status = { aliases: GrafiteAst.alias_spec DisambiguateTypes.Environment.t; - multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t + multi_aliases: GrafiteAst.alias_spec list DisambiguateTypes.Environment.t; + new_aliases: (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list } class type g_status = diff --git a/matita/components/library/libraryClean.ml b/matita/components/library/libraryClean.ml index 6f58bb54e..e59b42227 100644 --- a/matita/components/library/libraryClean.ml +++ b/matita/components/library/libraryClean.ml @@ -220,7 +220,7 @@ let moo_root_dir = lazy ( *) let rec close_db cache_of_processed_baseuri uris next = - prerr_endline "CLOSE_DB "; uris (* MATITA 1.0 *) + uris (* MATITA 1.0 *) ;; let clean_baseuris ?(verbose=true) buris = diff --git a/matita/components/ng_cic_content/nTermCicContent.mli b/matita/components/ng_cic_content/nTermCicContent.mli index f06ea2e91..4a13a8956 100644 --- a/matita/components/ng_cic_content/nTermCicContent.mli +++ b/matita/components/ng_cic_content/nTermCicContent.mli @@ -23,66 +23,6 @@ * http://helm.cs.unibo.it/ *) - -(* - (** {2 Persistant state handling} *) - -type interpretation_id - -val add_interpretation: - string -> (* id / description *) - string * NotationPt.argument_pattern list -> (* symbol, level 2 pattern *) - NotationPt.cic_appl_pattern -> (* level 3 pattern *) - interpretation_id - - (** @raise Interpretation_not_found *) -val lookup_interpretations: - string -> (* symbol *) - (string * NotationPt.argument_pattern list * - NotationPt.cic_appl_pattern) list - -exception Interpretation_not_found - - (** @raise Interpretation_not_found *) -val remove_interpretation: interpretation_id -> unit - - (** {3 Interpretations toggling} *) - -val get_all_interpretations: unit -> (interpretation_id * string) list -val get_active_interpretations: unit -> interpretation_id list -val set_active_interpretations: interpretation_id list -> unit - - (** {2 acic -> content} *) - -val ast_of_acic: - output_type:[`Pattern|`Term] -> - (Cic.id, NotationPt.sort_kind) Hashtbl.t -> (* id -> sort *) - Cic.annterm -> (* acic *) - NotationPt.term (* ast *) - * (Cic.id, UriManager.uri) Hashtbl.t (* id -> uri *) - - (** {2 content -> acic} *) - - (** @param env environment from argument_pattern to cic terms - * @param pat cic_appl_pattern *) -val instantiate_appl_pattern: - mk_appl:('term list -> 'term) -> - mk_implicit:(bool -> 'term) -> - term_of_uri : (UriManager.uri -> 'term) -> - (string * 'term) list -> NotationPt.cic_appl_pattern -> - 'term - -val push: unit -> unit -val pop: unit -> unit -*) - -(* -val nast_of_cic : - output_type:[`Pattern | `Term ] -> - subst:NCic.substitution -> context:NCic.context -> NCic.term -> - NotationPt.term -*) - type id = string val hide_coercions: bool ref diff --git a/matita/matita/matitaEngine.ml b/matita/matita/matitaEngine.ml index 0c389d66f..b87c8523b 100644 --- a/matita/matita/matitaEngine.ml +++ b/matita/matita/matitaEngine.ml @@ -52,19 +52,13 @@ let eval_macro_screenshot (status : GrafiteTypes.status) name = ;; let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) = - let lexicon_status_ref = ref (status :> LexiconTypes.status) in let baseuri = status#baseuri in - let new_status,new_objs = + let status = + status#set_lstatus { status#lstatus with LexiconTypes.new_aliases = [] } in + let status = GrafiteEngine.eval_ast ~include_paths ?do_heavy_checks status - (text,prefix_len,ast) - in - let new_status = - if !lexicon_status_ref#lstatus != status#lstatus then - new_status#set_lstatus (!lexicon_status_ref#lstatus) - else - new_status in - let new_status = LexiconSync.add_aliases_for_objs new_status new_objs in - let new_aliases = LexiconSync.alias_diff ~from:status new_status in + (text,prefix_len,ast) in + let new_aliases = status#lstatus.LexiconTypes.new_aliases in let _,intermediate_states = List.fold_left (fun (status,acc) (k,value) -> @@ -80,14 +74,14 @@ let eval_ast ~include_paths ?do_heavy_checks status (text,prefix_len,ast) = if b then status,acc else - let new_status = - LexiconEngine.set_proof_aliases status + let status = + LexiconEngine.set_proof_aliases status ~implicit_aliases:false GrafiteAst.WithPreferences [k,value] in - new_status, (new_status ,Some (k,value))::acc + status, (status ,Some (k,value))::acc ) (status,[]) new_aliases in - ((new_status),None)::intermediate_states + (status,None)::intermediate_states ;; exception TryingToAdd of string -- 2.39.2