From 66b139294edf89b6e207455a925f45dafe4f1cd2 Mon Sep 17 00:00:00 2001 From: Arnaud Spiwack Date: Sun, 21 Jul 2019 00:56:49 +0200 Subject: [PATCH] refactor: pull the various types in their own modules With pp, and hash, and equal, and all that. Also removed some dead code. --- .gitignore | 1 + src/main.ml | 177 +++++++++++++-------------------------------------- src/types.ml | 130 +++++++++++++++++++++++++++++++++++++ 3 files changed, 175 insertions(+), 133 deletions(-) create mode 100644 src/types.ml diff --git a/.gitignore b/.gitignore index 655e32b..ad9c0fd 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1,3 @@ _build .merlin +*.install \ No newline at end of file diff --git a/src/main.ml b/src/main.ml index 9c5c5e3..fd333f1 100644 --- a/src/main.ml +++ b/src/main.ml @@ -16,100 +16,19 @@ Steps: - Implement example sampler - Parse programs *) -type variable = string - -type location = variable -type item = variable -type indexed_item = item * int -(* Future plan for item: there can be more than one of an item in the - pool. In which case it will be translated to n variables (where n - is the number of occurrences of that item in the pool), the - corresponding range_constraints will be translated to formulas - which ensure that the n variables are ordered (to avoid generating - many semantically equal shuffles) *) -type range_constraint = { - scrutinee: item; - range: location list } - -type 'i atom = - | Reach of location - | Have of 'i * int - | Assign of location * 'i - (* Assign doesn't come from parsing as it is equivalent to a - singleton range_constraint. It appears in translations.*) -let map_atom f = function - | Reach l -> Reach l - | Have (i, n) -> Have (f i, n) - | Assign (l, i) -> Assign (l, f i) -type clause = { - goal: item atom; - requires: item atom list -} - -module StringMap = Map.Make(CCString) - -type program = { - locations: location list; - pool: item list; - range_constraints: range_constraint list; - range_definitions: location list StringMap.t; - logic: clause list; - goal: item atom -} - -let hash_location = CCHash.string -let hash_item = CCHash.string -let hash_indexed_item (i,n) = CCHash.(combine2 (string i) (int n)) -let hash_atom hash_item = function - | Reach l -> CCHash.(combine2 (int 0) (hash_location l)) - | Have (i, n) -> CCHash.(combine3 (int 1) (hash_item i) (int n)) - | Assign (l,i) -> CCHash.(combine3 (int 2) (hash_location l) (hash_item i)) - -let print_item i = i -let print_indexed_item (i, n) = i ^ "_" ^ (string_of_int n) -let print_atom print_item = function - | Reach l -> "reach: " ^ l - | Have (i,1) -> "have: " ^ print_item i - | Have (i,n) -> "have: " ^ print_item i ^ " *" ^ (string_of_int n) - | Assign(l,i) -> print_item i ^ " ∈ " ^ l -let print_timed_atom print_item = let open Provable in function - | Selection a -> print_atom print_item a - | At(a,i) -> print_atom print_item a ^ " @ " ^ string_of_int i - | Action (n, i) -> n ^ " @ " ^ string_of_int i - -let pp_clause fmt {goal;requires} = - let pp_atom fmt a = CCString.pp fmt (print_atom print_item a) in - Format.fprintf fmt "%a :- @[%a@]" pp_atom goal (CCList.pp ~sep:"," pp_atom) requires -let pp_range fmt {scrutinee;range} = - Format.fprintf fmt "%s ∈ {%a}" scrutinee (CCList.pp CCString.pp) range -let pp_program fmt prog = - (* XXX: I'm not printing range_definitions *) - let pp_locations = CCList.pp (fun fmt l -> Format.fprintf fmt "@[%s@]" l) in - let pp_pool = CCList.pp (fun fmt i -> Format.fprintf fmt "@[%s@]" i) in - let pp_ranges = CCList.pp pp_range in - let pp_logic = CCList.pp pp_clause in - let pp_goal fmt g = Format.fprintf fmt "%s." (print_atom print_item g) in - Format.fprintf fmt "@[@[[Locations]@,%a@]@,@[[Pool]@,%a@]@,@[[Ranges]@,%a@]@,@[[Logic]@,%a@]@,@[[Goal]@,%a@]@]@." pp_locations prog.locations pp_pool prog.pool pp_ranges prog.range_constraints pp_logic prog.logic pp_goal prog.goal - - +open Types let (&&&) = MLBDD.dand let (|||) = MLBDD.dor let anot = MLBDD.dnot let (-->) = MLBDD.imply -(* XXX: do I still need the AtomSet? *) -module AtomSet = Set.Make (struct type t = item atom let compare = compare end) -module TimedAtomSet = Set.Make (struct type t = item atom Provable.timed let compare = compare end) -module TimedAtomMap = Map.Make (struct type t = item atom Provable.timed let compare = compare end) -(* XXX: remove?*) -module AtomMap = Map.Make (struct type t = item atom let compare = compare end) +type formula = Item.t Atom.t Provable.timed Formula.t -type formula = item atom Provable.timed Formula.t - -module TimedLiteral = Sat.Literal(struct type t = item atom Provable.timed let equal = (=) let hash = Provable.hash (hash_atom hash_item) let pp fmt a = Format.fprintf fmt "%s" (print_timed_atom print_item a) end) -module TimedIndexedLiteral = Sat.Literal(struct type t = indexed_item atom Provable.timed let equal = (=) let hash = Provable.hash (hash_atom hash_indexed_item) let pp fmt a = Format.fprintf fmt "%s" (print_timed_atom print_indexed_item a) end) +module TimedLiteral = Sat.Literal(struct type t = Item.t Atom.t Provable.timed let equal = (=) let hash = Provable.hash (Atom.hash Item.hash) let pp = pp_timed_atom Item.pp end) +module TimedIndexedLiteral = Sat.Literal(struct type t = IndexedItem.t Atom.t Provable.timed let equal = (=) let hash = Provable.hash (Atom.hash IndexedItem.hash) let pp = pp_timed_atom IndexedItem.pp end) (* XXX: Literal, should provide its comparison function *) module TimedLiteralMap = Map.Make(struct type t = TimedLiteral.t let compare = compare end) + module LiteralsWithMults = struct include TimedIndexedLiteral type u = TimedLiteral.t @@ -118,7 +37,7 @@ module LiteralsWithMults = struct let norm_u = TimedLiteral.norm let decomp (n,l) = - ([n,Provable.map_timed (map_atom (fun i -> (i,0))) l], 1) + ([n,Provable.map_timed (Atom.map (fun i -> (i,0))) l], 1) end module Mult = Multiplicity.Make(LiteralsWithMults) @@ -146,11 +65,11 @@ let compile_formula man var_index (f : Mult.L.t Formula.t) : MLBDD.t = compile f let collect_program_atoms (p : program) : AtomSet.t = - let atoms : item atom Seq.t = + let atoms : Item.t Atom.t Seq.t = List.to_seq p.pool |> Seq.flat_map (fun i -> List.to_seq p.locations |> - Seq.flat_map (fun l -> List.to_seq [Assign(l,i)])) + Seq.flat_map (fun l -> List.to_seq [Atom.Assign(l,i)])) in AtomSet.of_seq atoms @@ -168,20 +87,19 @@ module Solver = Sat.Solver(Mult.L)(Mult.L.Map) do! If I use the function twice, it will destroy the previous bdd. *) let compile_to_bdd (p : program) : (MLBDD.t * Mult.L.t array) = - let bdd_vars = - collect_program_atoms p |> AtomSet.to_seq |> Array.of_seq - in - let assign (i : item) (l : location) : formula = - Formula.var (Provable.Selection (Assign(l,i))) + let assign (i : Item.t) (l : Location.t) : formula = + Formula.var (Provable.Selection (Atom.Assign(l,i))) in - let clause (c : clause) : item atom Provable.clause = - let open Provable in { + let clause (c : Clause.t) : Item.t Atom.t Provable.clause = + let open Provable in + let open Clause in + { hyps=c.requires; concl=c.goal; name=gen_rule_name () } in - let range (p : program) (r : range_constraint) : formula = + let range (p : program) (r : RangeConstraint.t) : formula = let at_least = Formula.disj_map (fun l -> assign r.scrutinee l) r.range in (* XXX: consider generating at_most/only constraint independently from the range, on _all_ locations. *) @@ -205,7 +123,7 @@ let compile_to_bdd (p : program) : (MLBDD.t * Mult.L.t array) = Formula.(at_least && at_most && only) in let ranges_formula = Seq.map (range p) (List.to_seq p.range_constraints) in - let capacity (p : program) (l : location) : formula = + let capacity (p : program) (l : Location.t) : formula = let distinct_pairs = List.to_seq p.pool |> Seq.flat_map (fun i -> Seq.map (fun i' -> (i, i')) (List.to_seq p.pool)) |> @@ -224,8 +142,8 @@ let compile_to_bdd (p : program) : (MLBDD.t * Mult.L.t array) = List.to_seq p.locations |> Seq.map begin fun l -> let open Provable in { - hyps = [ Reach l; Assign(l,i) ]; - concl = Have (i, 1); + hyps = [ Atom.Reach l; Atom.Assign(l,i) ]; + concl = Atom.Have (i, 1); name = gen_rule_name () } end @@ -254,7 +172,7 @@ let compile_to_bdd (p : program) : (MLBDD.t * Mult.L.t array) = in let observable = CCArray.filter (fun a -> match a with Provable.Selection _ -> true | _ -> false) atoms - |> Array.map (Provable.map_timed (map_atom (fun i -> (i, 0)))) + |> Array.map (Provable.map_timed (Atom.map (fun i -> (i, 0)))) |> Array.map TimedLiteral.of_atom |> Array.map (fun a -> Mult.Individual a) in @@ -269,6 +187,7 @@ let compile_to_bdd (p : program) : (MLBDD.t * Mult.L.t array) = , observable let femto_example = + let open Clause in (* A bit of early Alltp logic *) (* items *) let sword = "Sword" @@ -278,9 +197,9 @@ let femto_example = in let pool = [sword] in let locations = [well; eastern_boss; ] in - let goal = Reach eastern_boss in + let goal = Atom.Reach eastern_boss in let range_constraints = [ - {scrutinee=sword; range=locations}; + {RangeConstraint.scrutinee=sword; range=locations}; ] in let logic = [ {goal=Reach eastern_boss; requires=[Have (sword, 1)]}; @@ -289,6 +208,7 @@ let femto_example = { locations; pool; range_constraints; range_definitions=StringMap.empty; logic; goal } let micro_example = + let open Clause in (* A bit of early Alltp logic *) (* items *) let sword = "Sword" @@ -301,10 +221,10 @@ let micro_example = in let pool = [sword; bow] in let locations = [well; hideout; eastern_chest; eastern_boss; ] in - let goal = Reach eastern_boss in + let goal = Atom.Reach eastern_boss in let range_constraints = [ - {scrutinee=sword; range=locations}; - {scrutinee=bow; range=locations}; + {RangeConstraint.scrutinee=sword; range=locations}; + {RangeConstraint.scrutinee=bow; range=locations}; ] in let logic = [ {goal=Reach eastern_boss; requires=[Have (bow, 1); Have (sword, 1)]}; @@ -315,6 +235,7 @@ let micro_example = { locations; pool; range_constraints; range_definitions=StringMap.empty; logic; goal } let mini_example = + let open Clause in (* A bit of early Alltp logic *) (* items *) let sword = "Sword" @@ -330,11 +251,11 @@ let mini_example = let pool = [sword; bow; eastern_big] in let locations = [well; hideout; eastern_chest; eastern_big_chest; eastern_boss; ] in let eastern_palace = [eastern_chest; eastern_big_chest; eastern_boss] in - let goal = Reach eastern_boss in + let goal = Atom.Reach eastern_boss in let range_constraints = [ - {scrutinee=sword; range=locations}; - {scrutinee=bow; range=locations}; - {scrutinee=eastern_big; range=eastern_palace}; + {RangeConstraint.scrutinee=sword; range=locations}; + {RangeConstraint.scrutinee=bow; range=locations}; + {RangeConstraint.scrutinee=eastern_big; range=eastern_palace}; ] in let logic = [ {goal=Reach eastern_boss; requires=[Have (bow, 1); Have (sword, 1); Have (eastern_big, 1)]}; @@ -346,6 +267,7 @@ let mini_example = { locations; pool; range_constraints; range_definitions=StringMap.empty; logic; goal } let example = + let open Clause in (* A bit of early Alltp logic *) (* items *) let sword = "Sword" @@ -368,14 +290,14 @@ let example = let locations = [well; hideout; eastern_chest; eastern_big_chest; eastern_boss; desert_torch; desert_big_chest; desert_boss] in let eastern_palace = [eastern_chest; eastern_big_chest; eastern_boss] in let desert_palace = [desert_torch; desert_big_chest; desert_boss] in - let goal = Reach desert_boss in + let goal = Atom.Reach desert_boss in let range_constraints = [ - {scrutinee=sword; range=locations}; - {scrutinee=bow; range=locations}; - {scrutinee=boots; range=locations}; - {scrutinee=glove; range=locations}; - {scrutinee=eastern_big; range=eastern_palace}; - {scrutinee=desert_big; range=desert_palace}; + {RangeConstraint.scrutinee=sword; range=locations}; + {RangeConstraint.scrutinee=bow; range=locations}; + {RangeConstraint.scrutinee=boots; range=locations}; + {RangeConstraint.scrutinee=glove; range=locations}; + {RangeConstraint.scrutinee=eastern_big; range=eastern_palace}; + {RangeConstraint.scrutinee=desert_big; range=desert_palace}; ] in let logic = [ {goal=Reach eastern_boss; requires=[Have (bow, 1); Have (sword, 1); Have (eastern_big, 1)]}; @@ -396,11 +318,6 @@ let print_to_dot legend b ~file = let c = open_out file in let fmt = formatter_of_out_channel c in fprintf fmt "digraph bdd {@\n"; - (* let ranks = Hashtbl.create 17 in (\* var -> set of nodes *\) - * let add_rank v b = - * try Hashtbl.replace ranks v (S.add b (Hashtbl.find ranks v)) - * with Not_found -> Hashtbl.add ranks v (S.singleton b) - * in *) let visited = H1.create 1024 in let rec visit b = if not (H1.mem visited b) then begin @@ -412,19 +329,12 @@ let print_to_dot legend b ~file = fprintf fmt "%d [shape=box label=\"1\"];" (MLBDD.id b) | BIf (l, v, h) -> (* add_rank v b; *) - fprintf fmt "%d [label=\"x%s\"];" (MLBDD.id b) (print_timed_atom print_item (legend.(v-1))); + fprintf fmt "%d [label=\"x%a\"];" (MLBDD.id b) (pp_timed_atom Item.pp) (legend.(v-1)); fprintf fmt "%d -> %d;@\n" (MLBDD.id b) (MLBDD.id h); fprintf fmt "%d -> %d [style=\"dashed\"];@\n" (MLBDD.id b) (MLBDD.id l); visit h; visit l end in - (* Hashtbl.iter - * (fun v s -> - * fprintf fmt "{rank=same; "; - * S.iter (fun x -> fprintf fmt "%d " x.tag) s; - * fprintf fmt ";}@\n" - * ) - * ranks; *) visit b; fprintf fmt "}@."; close_out c @@ -445,7 +355,7 @@ let parse_file (filename : String.t) = let accumulate_range prog = function | Grammar.RangeDecl (item, range_expr) -> let locs = interp_range_expression prog range_expr in - let range = {scrutinee=item; range=locs} in + let range = {RangeConstraint.scrutinee=item; range=locs} in { prog with pool = item :: prog.pool; locations = locs @ prog.locations; @@ -458,11 +368,12 @@ let parse_file (filename : String.t) = } in let convert_atom = function - | Grammar.Have item -> Have(item, 1) - | Grammar.Reach loc -> Reach loc + | Grammar.Have item -> Atom.Have(item, 1) + | Grammar.Reach loc -> Atom.Reach loc in let accumulate_rule prog (goal, requires) = let clause = + let open Clause in { goal = convert_atom goal; requires = List.map convert_atom requires; } diff --git a/src/types.ml b/src/types.ml new file mode 100644 index 0000000..bca861e --- /dev/null +++ b/src/types.ml @@ -0,0 +1,130 @@ +module Variable = struct + + include CCString + + let pp fmt s = Format.fprintf fmt "%s" s + + module Set = Set.Make(CCString) + module Map = Map.Make(CCString) +end + +module Location = Variable + +module Item = Variable + +module IndexedItem = struct + + (* Stands for a specific copy of an item which may have several copies. *) + + type t = Item.t * int + + let compare = CCPair.compare Item.compare CCInt.compare + let equal = CCPair.equal Item.equal CCInt.equal + + let hash (item,k) = CCHash.(combine2 (Item.hash item) (int k)) + + let pp fmt (item,k) = Format.fprintf fmt "%a_%i" Item.pp item k +end + +module RangeConstraint = struct + type t = { + scrutinee: Item.t; + range: Location.t list; + } + + let pp fmt {scrutinee;range} = + Format.fprintf fmt "%s ∈ {%a}" scrutinee (CCList.pp CCString.pp) range + +end + +module Atom = struct + + type 'i t = + | Reach of Location.t + | Have of 'i * int + | Assign of Location.t * 'i + (* Assign doesn't come from parsing: it appears in translations.*) + + let compare item_compare al ar = match al, ar with + | Assign(locl,iteml), Assign(locr, itemr) -> + CCPair.compare Location.compare item_compare (locl,iteml) (locr,itemr) + | Assign _, _ -> -1 + | _, Assign _ -> 1 + | Reach locl, Reach locr -> + Location.compare locl locr + | Reach _, _ -> -1 + | _, Reach _ -> 1 + | Have(iteml, kl), Have(itemr, kr) -> + CCPair.compare item_compare CCInt.compare (iteml, kl) (itemr, kr) + let equal item_equal al ar = match al, ar with + | Assign(locl,iteml), Assign(locr, itemr) -> + Location.equal locl locr && item_equal iteml itemr + | Reach locl, Reach locr -> + Location.equal locl locr + | Have(iteml,kl), Have(itemr,kr) -> + item_equal iteml itemr && CCInt.equal kl kr + | _ -> false + + let hash hash_item = function + | Reach l -> CCHash.(combine2 (int 0) (Location.hash l)) + | Have (i, n) -> CCHash.(combine3 (int 1) (hash_item i) (int n)) + | Assign (l,i) -> CCHash.(combine3 (int 2) (Location.hash l) (hash_item i)) + + let map f = function + | Reach l -> Reach l + | Have (i, n) -> Have (f i, n) + | Assign (l, i) -> Assign (l, f i) + + let pp pp_item fmt = function + | Reach l -> Format.fprintf fmt "reach: %a" Location.pp l + | Have (i,1) -> Format.fprintf fmt "have: %a" pp_item i + | Have (i,n) -> Format.fprintf fmt "have: %a * %i" pp_item i n + | Assign(l,i) -> Format.fprintf fmt "%a ∈ %a" pp_item i Location.pp l + +end + +module Clause = struct + + type t = { + goal: Item.t Atom.t; + requires: Item.t Atom.t list + } + +end + +module StringMap = Map.Make(CCString) + +type program = { + locations: Location.t list; + (* Future plan for item: there can be more than one of an item in + the pool. In which case it will be translated to n variables + (where n is the number of occurrences of that item in the pool), + the corresponding range_constraints will be translated to + formulas which ensure that the n variables are ordered (to avoid + generating many semantically equal shuffles) *) + pool: Item.t list; + range_constraints: RangeConstraint.t list; + range_definitions: Location.t list StringMap.t; + logic: Clause.t list; + goal: Item.t Atom.t +} +let pp_timed_atom pp_item fmt = let open Provable in function + | Selection a -> Atom.pp pp_item fmt a + | At(a,i) -> Format.fprintf fmt "%a @ %i" (Atom.pp pp_item) a i + | Action (n, i) -> Format.fprintf fmt "%s @ %i" n i + +let pp_clause fmt {Clause.goal;requires} = + Format.fprintf fmt "%a :- @[%a@]" (Atom.pp Item.pp) goal (CCList.pp ~sep:"," (Atom.pp Item.pp)) requires +let pp_program fmt prog = + (* XXX: I'm not printing range_definitions *) + let pp_locations = CCList.pp (fun fmt l -> Format.fprintf fmt "@[%s@]" l) in + let pp_pool = CCList.pp (fun fmt i -> Format.fprintf fmt "@[%s@]" i) in + let pp_ranges = CCList.pp RangeConstraint.pp in + let pp_logic = CCList.pp pp_clause in + let pp_goal fmt g = Format.fprintf fmt "%a." (Atom.pp Item.pp) g in + Format.fprintf fmt "@[@[[Locations]@,%a@]@,@[[Pool]@,%a@]@,@[[Ranges]@,%a@]@,@[[Logic]@,%a@]@,@[[Goal]@,%a@]@]@." pp_locations prog.locations pp_pool prog.pool pp_ranges prog.range_constraints pp_logic prog.logic pp_goal prog.goal + +module AtomSet = Set.Make (struct type t = Item.t Atom.t let compare = Atom.compare Item.compare end) +module AtomMap = Map.Make (struct type t = Item.t Atom.t let compare = Atom.compare Item.compare end) +module TimedAtomSet = Set.Make (struct type t = Item.t Atom.t Provable.timed let compare = compare end) +module TimedAtomMap = Map.Make (struct type t = Item.t Atom.t Provable.timed let compare = compare end)