From b95be966e385957a25f26a41f45e0116955264ae Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 13 Apr 2006 14:24:03 +0000 Subject: [PATCH] added include' to include everything but preferences (aka aliases) --- .../grafite_parser/dependenciesParser.ml | 2 +- .../grafite_parser/grafiteParser.ml | 9 ++- .../software/components/lexicon/lexiconAst.ml | 4 +- .../components/lexicon/lexiconAstPp.ml | 6 +- .../components/lexicon/lexiconEngine.ml | 78 +++++++++++-------- 5 files changed, 59 insertions(+), 40 deletions(-) diff --git a/helm/software/components/grafite_parser/dependenciesParser.ml b/helm/software/components/grafite_parser/dependenciesParser.ml index fc49de600..dee951118 100644 --- a/helm/software/components/grafite_parser/dependenciesParser.ml +++ b/helm/software/components/grafite_parser/dependenciesParser.ml @@ -84,7 +84,7 @@ let baseuri_of_script ~include_paths file = if String.length uri < 5 || String.sub uri 0 5 <> "cic:/" then HLog.error (file ^ " sets an incorrect baseuri: " ^ buri); (try - ignore(Http_getter.resolve uri) + ignore(Http_getter.resolve ~writable:false uri) with | Http_getter_types.Unresolvable_URI _ -> HLog.error (file ^ " sets an unresolvable baseuri: " ^ buri) diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 8848efad6..e83152226 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -449,7 +449,10 @@ EXTEND ]; include_command: [ [ - IDENT "include" ; path = QSTRING -> loc,path + IDENT "include" ; path = QSTRING -> + loc,path,LexiconAst.WithPreferences + | IDENT "include'" ; path = QSTRING -> + loc,path,LexiconAst.WithoutPreferences ]]; grafite_command: [ [ @@ -528,11 +531,11 @@ EXTEND fun ~include_paths status -> status,LSome(GrafiteAst.Executable (loc,ex)) | com = comment -> fun ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com)) - | (iloc,fname) = include_command ; SYMBOL "." -> + | (iloc,fname,mode) = include_command ; SYMBOL "." -> fun ~include_paths status -> let path = DependenciesParser.baseuri_of_script ~include_paths fname in let status = - LexiconEngine.eval_command status (LexiconAst.Include (iloc,path)) + LexiconEngine.eval_command status (LexiconAst.Include (iloc,path,mode)) in status, LSome diff --git a/helm/software/components/lexicon/lexiconAst.ml b/helm/software/components/lexicon/lexiconAst.ml index aed4b0b15..50f0061ee 100644 --- a/helm/software/components/lexicon/lexiconAst.ml +++ b/helm/software/components/lexicon/lexiconAst.ml @@ -38,8 +38,10 @@ type alias_spec = * marshalling *) let magic = 5 +type inclusion_mode = WithPreferences | WithoutPreferences (* aka aliases *) + type command = - | Include of loc * string + | Include of loc * string * inclusion_mode | Alias of loc * alias_spec (** parameters, name, type, fields *) | Notation of loc * direction option * CicNotationPt.term * Gramext.g_assoc * diff --git a/helm/software/components/lexicon/lexiconAstPp.ml b/helm/software/components/lexicon/lexiconAstPp.ml index e49a66f60..4b20958aa 100644 --- a/helm/software/components/lexicon/lexiconAstPp.ml +++ b/helm/software/components/lexicon/lexiconAstPp.ml @@ -75,7 +75,11 @@ let pp_notation dir_opt l1_pattern assoc prec l2_pattern = (pp_l2_pattern l2_pattern) let pp_command = function - | Include (_,path) -> "include " ^ path + | Include (_,path,mode) -> + if mode = WithPreferences then + "include " ^ path + else + "include' " ^ path | Alias (_,s) -> pp_alias s | Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) -> pp_interpretation dsc symbol arg_patterns cic_appl_pattern diff --git a/helm/software/components/lexicon/lexiconEngine.ml b/helm/software/components/lexicon/lexiconEngine.ml index d3a8954ff..34e314edc 100644 --- a/helm/software/components/lexicon/lexiconEngine.ml +++ b/helm/software/components/lexicon/lexiconEngine.ml @@ -72,44 +72,50 @@ let add_metadata new_metadata status = else status -let set_proof_aliases status new_aliases = - let commands_of_aliases = - List.map - (fun alias -> LexiconAst.Alias (HExtlib.dummy_floc, alias)) - in - let deps_of_aliases = - HExtlib.filter_map - (function - | LexiconAst.Ident_alias (_, suri) -> - let buri = UriManager.buri_of_uri (UriManager.uri_of_string suri) in - Some (LibraryNoDb.Dependency buri) - | _ -> None) - in - let aliases = - List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc) - status.aliases new_aliases in - let multi_aliases = - List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.cons d c acc) - status.multi_aliases new_aliases in - let new_status = - { status with multi_aliases = multi_aliases ; aliases = aliases} - in - if new_aliases = [] then - new_status +let set_proof_aliases mode status new_aliases = + if mode = LexiconAst.WithoutPreferences then + status else - let aliases = - DisambiguatePp.aliases_of_domain_and_codomain_items_list new_aliases + let commands_of_aliases = + List.map + (fun alias -> LexiconAst.Alias (HExtlib.dummy_floc, alias)) in - let status = add_lexicon_content (commands_of_aliases aliases) new_status in - let status = add_metadata (deps_of_aliases aliases) status in - status + let deps_of_aliases = + HExtlib.filter_map + (function + | LexiconAst.Ident_alias (_, suri) -> + let buri = UriManager.buri_of_uri (UriManager.uri_of_string suri) in + Some (LibraryNoDb.Dependency buri) + | _ -> None) + in + let aliases = + List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.add d c acc) + status.aliases new_aliases in + let multi_aliases = + List.fold_left (fun acc (d,c) -> DisambiguateTypes.Environment.cons d c acc) + status.multi_aliases new_aliases in + let new_status = + { status with multi_aliases = multi_aliases ; aliases = aliases} + in + if new_aliases = [] then + new_status + else + let aliases = + DisambiguatePp.aliases_of_domain_and_codomain_items_list new_aliases + in + let status = + add_lexicon_content (commands_of_aliases aliases) new_status + in + let status = add_metadata (deps_of_aliases aliases) status in + status + -let rec eval_command status cmd = +let rec eval_command ?(mode=LexiconAst.WithPreferences) status cmd = let notation_ids' = CicNotation.process_notation cmd in let status = { status with notation_ids = notation_ids' @ status.notation_ids } in match cmd with - | LexiconAst.Include (loc, baseuri) -> + | LexiconAst.Include (loc, baseuri, mode) -> let lexiconpath_rw, lexiconpath_r = LibraryMisc.lexicon_file_of_baseuri ~must_exist:false ~writable:true ~baseuri, @@ -122,7 +128,7 @@ let rec eval_command status cmd = raise (IncludedFileNotCompiled lexiconpath_rw) in let lexicon = LexiconMarshal.load_lexicon lexiconpath in - let status = List.fold_left eval_command status lexicon in + let status = List.fold_left (eval_command ~mode) status lexicon in if Helm_registry.get_bool "db.nodb" then let metadatapath_rw, metadatapath_r = LibraryMisc.metadata_file_of_baseuri @@ -153,7 +159,7 @@ let rec eval_command status cmd = [DisambiguateTypes.Num instance, DisambiguateChoices.lookup_num_by_dsc desc] in - set_proof_aliases status diff + set_proof_aliases mode status diff | LexiconAst.Interpretation (_, dsc, (symbol, _), cic_appl_pattern) as stm -> let status = add_lexicon_content [stm] status in let uris = @@ -165,8 +171,12 @@ let rec eval_command status cmd = [DisambiguateTypes.Symbol (symbol, 0), DisambiguateChoices.lookup_symbol_by_dsc symbol dsc] in - let status = set_proof_aliases status diff in + let status = set_proof_aliases mode status diff in let status = add_metadata uris status in status | LexiconAst.Notation _ as stm -> add_lexicon_content [stm] status +let eval_command = eval_command ?mode:None + +let set_proof_aliases = set_proof_aliases LexiconAst.WithPreferences + -- 2.39.2