source: extracted/untrusted/compute_fixpoints.ml @ 2773

Last change on this file since 2773 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 987 bytes
Line 
1module Label_ImperativeMap = struct
2
3  type key = Graphs.label
4
5  type 'data t = 'data Graphs.graph ref
6
7  let create () = ref (Identifiers.empty_map PreIdentifiers.LabelTag)
8
9  let clear t =
10    t := Identifiers.empty_map PreIdentifiers.LabelTag
11
12  let add k d t =
13    t := Identifiers.add PreIdentifiers.LabelTag !t k d
14
15  let find k t =
16   match Identifiers.lookup PreIdentifiers.LabelTag !t k with
17      Types.Some res -> res
18    | Types.None -> raise Not_found
19
20  let iter f t =
21   Identifiers.foldi PreIdentifiers.LabelTag (fun k v () -> f k v) !t ()
22
23end
24
25(** val compute_fixpoint : Fixpoints.fixpoint_computer **)
26let compute_fixpoint latt =
27 let module L : Fix.PROPERTY with type property = Preamble.__ =
28  struct
29   type property = Preamble.__
30   let bottom = Fixpoints.l_bottom latt
31   let equal x y = Fixpoints.l_equal latt x y = Bool.True
32   let is_maximal x = Fixpoints.l_is_maximal latt x = Bool.True
33  end in
34 let module F = Fix.Make (Label_ImperativeMap) (L) in
35  F.lfp
Note: See TracBrowser for help on using the repository browser.