X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Flambda-delta%2Fcommon%2Fhierarchy.ml;h=23c8109bf728e8003845153265cc79cd59e7f4f8;hb=689118326fbe47231865b26c66ae89144459be6a;hp=f916e1e4316671761f0218d76f11b84ee40bd30f;hpb=c8011c7ad75be5d03c4d4bb2e6900af32ad65c07;p=helm.git diff --git a/helm/software/lambda-delta/common/hierarchy.ml b/helm/software/lambda-delta/common/hierarchy.ml index f916e1e43..23c8109bf 100644 --- a/helm/software/lambda-delta/common/hierarchy.ml +++ b/helm/software/lambda-delta/common/hierarchy.ml @@ -15,35 +15,47 @@ module C = Cps type graph = string * (int -> int) -let sorts = 2 -let sort = H.create sorts -let index = ref 0 +let sorts = 3 +let sort = H.create sorts + +let default_graph = "Z1" (* Internal functions *******************************************************) -let set_sort f (h:int) (s:string) = - H.add sort h s; f (succ h) +let set_sort h s = + H.add sort h s; succ h + +let graph_of_string err f s = + try + let x = S.sscanf s "Z%u" C.start in + if x > 0 then f (s, fun h -> x + h) else err () + with + S.Scan_failure _ | Failure _ | End_of_file -> err () + +let graph = ref (graph_of_string C.err C.start default_graph) (* Interface functions ******************************************************) -let set_new_sorts f ss = - let f i = index := i; f i in - C.list_fold_left f set_sort !index ss +let set_sorts i ss = + List.fold_left set_sort i ss -let get_sort f h = - try f (Some (H.find sort h)) - with Not_found -> f None +let string_of_sort err f h = + try f (H.find sort h) with Not_found -> err () -let string_of_graph f (s, _) = f s +let sort_of_string err f s = + let map h n = function + | None when n = s -> Some h + | xh -> xh + in + match H.fold map sort None with + | None -> err () + | Some h -> f h -let apply f (_, g) h = f (g h) +let string_of_graph () = fst !graph -let graph_of_string f s = - try - let x = S.sscanf s "Z%u" C.start in - if x > 0 then f (Some (s, fun h -> x + h)) else f None - with - S.Scan_failure _ | Failure _ | End_of_file -> f None +let apply h = snd !graph h -let graph = - ref (graph_of_string (function Some g -> g | None -> assert false) "Z2") +let set_graph s = + let err () = false in + let f g = graph := g; true in + graph_of_string err f s