diff options
author | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-08 18:51:35 +0000 |
---|---|---|
committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-08 18:51:35 +0000 |
commit | b2f2727670853183bfbcbafb9dc19f0f71494a7b (patch) | |
tree | 8d9cea5ed2713ab2bfe3b142816a48c5ba615758 /library/library.ml | |
parent | 1f48326c7edf7f6e7062633494d25b254a6db82c (diff) |
State Transaction Machine
The process_transaction function adds a new edge to the Dag without
executing the transaction (when possible).
The observe id function runs the transactions necessary to reach to the
state id. Transaction being on a merged branch are not executed but
stored into a future.
The finish function calls observe on the tip of the current branch.
Imperative modifications to the environment made by some tactics are
now explicitly declared by the tactic and modeled as let-in/beta-redexes
at the root of the proof term. An example is the abstract tactic.
This is the work described in the Coq Workshop 2012 paper.
Coq is compile with thread support from now on.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16674 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/library.ml')
-rw-r--r-- | library/library.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/library/library.ml b/library/library.ml index 472b1fb1d..0766a62d7 100644 --- a/library/library.ml +++ b/library/library.ml @@ -44,17 +44,20 @@ module LibraryOrdered = DirPath module LibraryMap = Map.Make(LibraryOrdered) module LibraryFilenameMap = Map.Make(LibraryOrdered) +let join x = Safe_typing.join_compiled_library x.library_compiled (* This is a map from names to loaded libraries *) -let libraries_table = Summary.ref LibraryMap.empty ~name:"LIBRARY" +let freeze b l = if b then (LibraryMap.iter (fun _ x -> join x) l; l) else l +let libraries_table = Summary.ref LibraryMap.empty ~name:"LIBRARY" ~freeze (* This is the map of loaded libraries filename *) (* (not synchronized so as not to be caught in the states on disk) *) let libraries_filename_table = ref LibraryFilenameMap.empty (* These are the _ordered_ sets of loaded, imported and exported libraries *) -let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD" -let libraries_imports_list = Summary.ref [] ~name:"LIBRARY-IMPORT" -let libraries_exports_list = Summary.ref [] ~name:"LIBRARY-EXPORT" +let freeze b l = if b then (List.iter join l; l) else l +let libraries_loaded_list = Summary.ref [] ~name:"LIBRARY-LOAD" ~freeze +let libraries_imports_list = Summary.ref [] ~name:"LIBRARY-IMPORT" ~freeze +let libraries_exports_list = Summary.ref [] ~name:"LIBRARY-EXPORT" ~freeze (* various requests to the tables *) |