Skip to content

GitLab

Commit 5c1e10fe authored by POTTIER Francois's avatar POTTIER Francois
Browse files

Reimplement FixSolver using Fix.DataFlow. 

Also get rid of Boolean, which was redundant with Fix.Prop.Boolean.
parent b3528d40
Pipeline #188799 passed with stages
in 2 minutes
Hide whitespace changes
Inline Side-by-side
Showing with 103 additions and 153 deletions
src/Boolean.ml deleted 100644 → 0
View file @ b3528d40
(******************************************************************************)
(* *)
(* Menhir *)
(* *)
(* François Pottier, Inria Paris *)
(* Yann Régis-Gianas, PPS, Université Paris Diderot *)
(* *)
(* Copyright Inria. All rights reserved. This file is distributed under the *)
(* terms of the GNU General Public License version 2, as described in the *)
(* file LICENSE. *)
(* *)
(******************************************************************************)
(* The Boolean lattice. *)
type property =
bool
let bottom =
false
let equal (b1 : bool) (b2 : bool) =
b1 = b2
let is_maximal b =
b
let union (b1 : bool) (b2 : bool) =
b1 || b2
src/Boolean.mli deleted 100644 → 0
View file @ b3528d40
(******************************************************************************)
(* *)
(* Menhir *)
(* *)
(* François Pottier, Inria Paris *)
(* Yann Régis-Gianas, PPS, Université Paris Diderot *)
(* *)
(* Copyright Inria. All rights reserved. This file is distributed under the *)
(* terms of the GNU General Public License version 2, as described in the *)
(* file LICENSE. *)
(* *)
(******************************************************************************)
include Fix.PROPERTY with type property = bool
val union: property -> property -> property
src/FixSolver.ml
View file @ 5c1e10fe
......@@ -13,10 +13,7 @@
module Make
(M : Fix.IMPERATIVE_MAPS)
(P : sig
include Fix.PROPERTY
val union: property -> property -> property
end)
(P : Fix.MINIMAL_SEMI_LATTICE)
= struct
type variable =
......@@ -25,61 +22,47 @@ end)
type property =
P.property
(* A constraint is represented as a mapping of each variable to an
expression, which represents its lower bound. We could represent
an expression as a list of constants and variables; we can also
represent it as a binary tree, as follows. *)
type expression =
| EBottom
| ECon of property
| EVar of variable
| EJoin of expression * expression
type constraint_ =
expression M.t
(* Looking up a variable's lower bound. *)
let consult (m : constraint_) (x : variable) : expression =
try
M.find x m
with Not_found ->
EBottom
(* Evaluation of an expression in an environment. *)
let rec evaluate get e =
match e with
| EBottom ->
P.bottom
| ECon p ->
p
| EVar x ->
get x
| EJoin (e1, e2) ->
P.union (evaluate get e1) (evaluate get e2)
(* Solving a constraint. *)
let solve (m : constraint_) : variable -> property =
let module F = Fix.Make(M)(P) in
F.lfp (fun x get ->
evaluate get (consult m x)
)
(* The imperative interface. *)
let create () =
let m = M.create() in
let record_ConVar p y =
M.add y (EJoin (ECon p, consult m y)) m
and record_VarVar x y =
M.add y (EJoin (EVar x, consult m y)) m
in
record_ConVar,
record_VarVar,
fun () -> solve m
let join =
P.leq_join
end
(* A map of each variable to its upper bounds (its successors). *)
let upper : variable list M.t =
M.create()
let successors x =
try M.find x upper with Not_found -> []
let record_VarVar x y =
M.add x (y :: successors x) upper
(* A map of each variable to its lower bound (a constant). *)
let lower : property M.t =
M.create()
let record_ConVar p y =
match M.find y lower with
| exception Not_found ->
M.add y p lower
| q ->
M.add y (join p q) lower
(* Running the analysis. *)
module Solve () = struct
module G = struct
type nonrec variable = variable
type nonrec property = property
let foreach_root contribute =
M.iter contribute lower
let foreach_successor x p contribute =
List.iter (fun y -> contribute y p) (successors x)
end
include Fix.DataFlow.Run(M)(P)(G)
end
end
src/FixSolver.mli
View file @ 5c1e10fe
......@@ -11,32 +11,34 @@
(* *)
(******************************************************************************)
open Fix
module Make
(M : Fix.IMPERATIVE_MAPS)
(P : sig
include Fix.PROPERTY
val union: property -> property -> property
end)
(M : IMPERATIVE_MAPS)
(P : MINIMAL_SEMI_LATTICE)
: sig
(* Variables and constraints. A constraint is an inequality between
a constant or a variable, on the left-hand side, and a variable,
on the right-hand side. *)
type variable =
M.key
type property =
P.property
(* An imperative interface, where we create a new constraint system,
and are given three functions to add constraints and (once we are
done adding) to solve the system. *)
(* [record_ConVar x y] records an inequality between a constant and
a variable. *)
val create: unit ->
(property -> variable -> unit) *
(variable -> variable -> unit) *
(unit -> (variable -> property))
val record_ConVar: property -> variable -> unit
end
(* [record_VarVar x y] records an inequality between two variables. *)
val record_VarVar: variable -> variable -> unit
(* The functor [Solve] computes the least solution of the
constraints. The value [None] represents bottom. *)
module Solve () :
SOLUTION
with type variable = variable
and type property = property option
end
src/grammarFunctor.ml
View file @ 5c1e10fe
......@@ -429,6 +429,9 @@ module TerminalSet = struct
let is_maximal _ =
false
let leq_join =
union
end
(* Maps over terminals. *)
......@@ -561,8 +564,11 @@ module SymbolSet = struct
let bottom =
empty
let is_maximal _ =
false
let leq =
subset
let join =
union
end
......@@ -1094,7 +1100,7 @@ end
module NONEMPTY =
GenericAnalysis
(Boolean)
(Fix.Prop.Boolean)
(struct
(* A terminal symbol is nonempty. *)
let terminal _ = true
......@@ -1109,7 +1115,7 @@ module NONEMPTY =
module NULLABLE =
GenericAnalysis
(Boolean)
(Fix.Prop.Boolean)
(struct
(* A terminal symbol is not nullable. *)
let terminal _ = false
......@@ -1241,29 +1247,27 @@ let () =
intuitively represents a set of symbols. *)
module FOLLOW (P : sig
include Fix.PROPERTY
val union: property -> property -> property
include Fix.MINIMAL_SEMI_LATTICE
val bottom: property
val terminal: Terminal.t -> property
val first: Production.index -> int -> property
end) = struct
module M =
Fix.Glue.ArraysAsImperativeMaps(Nonterminal)
module S =
FixSolver.Make
(Fix.Glue.ArraysAsImperativeMaps(Nonterminal))
(P)
FixSolver.Make(M)(P)
(* Build a system of constraints. *)
let record_ConVar, record_VarVar, solve =
S.create()
(* Iterate over all start symbols. *)
let () =
let sharp = P.terminal Terminal.sharp in
for nt = 0 to Nonterminal.start - 1 do
assert (Nonterminal.is_start nt);
(* Add # to FOLLOW(nt). *)
record_ConVar sharp nt
S.record_ConVar sharp nt
done
(* We need to do this explicitly because our start productions are
of the form S' -> S, not S' -> S #, so # will not automatically
......@@ -1282,18 +1286,24 @@ end) = struct
and first = P.first prod (i+1) in
(* The FIRST set of the remainder of the right-hand side
contributes to the FOLLOW set of [nt2]. *)
record_ConVar first nt2;
S.record_ConVar first nt2;
(* If the remainder of the right-hand side is nullable,
FOLLOW(nt1) contributes to FOLLOW(nt2). *)
if nullable then
record_VarVar nt1 nt2
S.record_VarVar nt1 nt2
) rhs
) Production.table
(* Second pass. Solve the equations (on demand). *)
let follow : (Nonterminal.t -> P.property) Lazy.t =
lazy (
let module S = S.Solve() in
fun nt -> Option.value (S.solution nt) ~default:P.bottom
)
let follow : Nonterminal.t -> P.property =
solve()
fun nt -> (Lazy.force follow) nt
end
......@@ -1402,7 +1412,8 @@ let sfirst prod i =
let sfollow : Nonterminal.t -> SymbolSet.t =
let module F = FOLLOW(struct
include SymbolSet
let bottom = SymbolSet.bottom
include Fix.Glue.MinimalSemiLattice(SymbolSet)
let terminal t = SymbolSet.singleton (Symbol.T t)
let first = sfirst
end) in
......
src/invariant.ml
View file @ 5c1e10fe
......@@ -522,11 +522,8 @@ end
property -- in particular, I would like to keep track of no positions at all,
if the user doesn't use any position keyword. But I am suffering. *)
module S =
FixSolver.Make(M)(Boolean)
let record_ConVar, record_VarVar, solve =
S.create()
module F =
FixSolver.Make(M)(Fix.Prop.Boolean)
let () =
......@@ -544,10 +541,10 @@ let () =
if length > 0 then begin
(* If [nt] keeps track of its start position, then the first symbol
in the right-hand side must do so as well. *)
record_VarVar (Symbol.N nt, WhereStart) (rhs.(0), WhereStart);
F.record_VarVar (Symbol.N nt, WhereStart) (rhs.(0), WhereStart);
(* If [nt] keeps track of its end position, then the last symbol
in the right-hand side must do so as well. *)
record_VarVar (Symbol.N nt, WhereEnd) (rhs.(length - 1), WhereEnd)
F.record_VarVar (Symbol.N nt, WhereEnd) (rhs.(length - 1), WhereEnd)
end;
KeywordSet.iter (function
......@@ -572,7 +569,7 @@ let () =
its start position. Similarly for end positions. *)
Array.iteri (fun i id' ->
if id = id' then
record_ConVar true (rhs.(i), where)
F.record_ConVar true (rhs.(i), where)
) ids
) (Action.keywords action)
......@@ -591,8 +588,8 @@ let () =
let nt, rhs = Production.def prod in
let length = Array.length rhs in
if length = 0 then begin
record_VarVar (Symbol.N nt, WhereStart) (sym, WhereEnd);
record_VarVar (Symbol.N nt, WhereEnd) (sym, WhereEnd)
F.record_VarVar (Symbol.N nt, WhereStart) (sym, WhereEnd);
F.record_VarVar (Symbol.N nt, WhereEnd) (sym, WhereEnd)
end
) (Lr1.reductions s);
......@@ -600,12 +597,16 @@ let () =
can be reduced in state [s] and mentions [$endpos($0)], then [sym]
must keep track of its end position. *)
if Lr1.has_beforeend s then
record_ConVar true (sym, WhereEnd)
F.record_ConVar true (sym, WhereEnd)
)
let track : variable -> bool option =
let module S = F.Solve() in
S.solution
let track : variable -> bool =
solve()
fun x -> Option.value (track x) ~default:false
let startp symbol =
track (symbol, WhereStart)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment