diff options
Diffstat (limited to 'plugins/xml/unshare.ml')
| -rw-r--r-- | plugins/xml/unshare.ml | 52 |
1 files changed, 52 insertions, 0 deletions
diff --git a/plugins/xml/unshare.ml b/plugins/xml/unshare.ml new file mode 100644 index 00000000..f30f8230 --- /dev/null +++ b/plugins/xml/unshare.ml @@ -0,0 +1,52 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * The HELM Project / The EU MoWGLI Project *) +(* * University of Bologna *) +(************************************************************************) +(* This file is distributed under the terms of the *) +(* GNU Lesser General Public License Version 2.1 *) +(* *) +(* Copyright (C) 2000-2004, HELM Team. *) +(* http://helm.cs.unibo.it *) +(************************************************************************) + +exception CanNotUnshare;; + +(* [unshare t] gives back a copy of t where all sharing has been removed *) +(* Physical equality becomes meaningful on unshared terms. Hashtables that *) +(* use physical equality can now be used to associate information to evey *) +(* node of the term. *) +let unshare ?(already_unshared = function _ -> false) t = + let obj = Obj.repr t in + let rec aux obj = + if already_unshared (Obj.obj obj) then + obj + else + (if Obj.is_int obj then + obj + else if Obj.is_block obj then + begin + let tag = Obj.tag obj in + if tag < Obj.no_scan_tag then + begin + let size = Obj.size obj in + let new_obj = Obj.new_block 0 size in + Obj.set_tag new_obj tag ; + for i = 0 to size - 1 do + Obj.set_field new_obj i (aux (Obj.field obj i)) + done ; + new_obj + end + else if tag = Obj.string_tag then + obj + else + raise CanNotUnshare + end + else + raise CanNotUnshare + ) + in + Obj.obj (aux obj) +;; |