Commit 90673664 authored by POTTIER Francois's avatar POTTIER Francois

Some of the position keywords are now expanded away early on,

that is, before %inlining.
parent f6577c1f
......@@ -37,6 +37,15 @@ let from_stretch s =
keywords = pkeywords_to_keywords pkeywords;
}
(* Defining a keyword in terms of other keywords. *)
let define keyword keywords f action =
assert (KeywordSet.mem keyword action.keywords);
{ action with
expr = f action.expr;
keywords = KeywordSet.union keywords (KeywordSet.remove keyword action.keywords)
}
(* Composition, used during inlining. *)
let compose x a1 a2 =
......@@ -153,34 +162,6 @@ let print f action =
let has_syntaxerror action =
KeywordSet.mem SyntaxError (keywords action)
let has_left action =
KeywordSet.exists (function
| Position (Left, _, _) ->
true
| _ ->
false
) (keywords action)
let has_leftstart action =
KeywordSet.exists (function
| Position (Left, WhereStart, _) ->
true
| _ ->
false
) (keywords action)
let has_leftend action =
KeywordSet.exists (function
| Position (Left, WhereEnd, _) ->
true
| _ ->
false
) (keywords action)
let has_beforeend action =
KeywordSet.exists (function
| Position (Before, WhereEnd, _) ->
true
| _ ->
false
) (keywords action)
KeywordSet.mem (Position (Before, WhereEnd, FlavorPosition)) action.keywords
open Keyword
(** Semantic action's type. *)
type t
......@@ -5,13 +7,24 @@ type t
feature is used during the processing of the %inline keyword. *)
val compose : string -> t -> t -> t
(* TEMPORARY document this: *)
(* [define keyword keywords f action] defines away the keyword [keyword].
It is removed from the set of keywords of this semantic action; the
set [keywords] is added in its place. The body of the semantic action
is transformed by the function [f], which typically wraps it in some
new [let] bindings. *)
val define: keyword -> KeywordSet.t -> (IL.expr -> IL.expr) -> t -> t
(* Variable-to-variable substitutions, used by [rename], below. *)
type subst =
(string * string) list
(* [Subject/where] pairs, as defined in [Keyword], encode a position
keyword. *)
type sw =
Keyword.subject * Keyword.where
subject * where
(** [rename f phi a] applies to the semantic action [a] the renaming [phi] as
well as the transformations decided by the function [f]. The function [f] is
......@@ -35,10 +48,10 @@ val to_il_expr: t -> IL.expr
val filenames: t -> string list
(** [pkeywords a] returns a list of all keyword occurrences in [a]. *)
val pkeywords: t -> Keyword.keyword Positions.located list
val pkeywords: t -> keyword Positions.located list
(** [keywords a] is the set of keywords used in the semantic action [a]. *)
val keywords: t -> Keyword.KeywordSet.t
val keywords: t -> KeywordSet.t
(** [print f a] prints [a] to channel [f]. *)
val print: out_channel -> t -> unit
......@@ -46,17 +59,8 @@ val print: out_channel -> t -> unit
(** [from_stretch s] builds an action out of a textual piece of code. *)
val from_stretch: Stretch.t -> t
(** Check whether the keyword $syntaxerror is used in the action. *)
(** Test whether the keyword [$syntaxerror] is used in the action. *)
val has_syntaxerror: t -> bool
(** Check whether the keyword $start is used in the action. *)
val has_leftstart: t -> bool
(** Check whether the keyword $end is used in the action. *)
val has_leftend: t -> bool
(** Check whether the keyword $start or $end is used in the action. *)
val has_left: t -> bool
(** Check whether the keyword $endpos($0) is used in the action. *)
(** Test whether the keyword [$endpos($0)] is used in the action. *)
val has_beforeend: t -> bool
......@@ -1181,22 +1181,13 @@ let reducebody prod =
exists and has an [endp] field at offset 1. Yes, we live
dangerously. You only live once. *)
(* Note that [Action.has_leftstart action] does not imply
[Invariant.startp symbol], and similarly for end positions. *)
let symbol =
Symbol.N nt
in
let posbindings action =
let bind_beforeendp =
Action.has_beforeend action
and bind_startp =
Action.has_leftstart action || Invariant.startp symbol
and bind_endp =
Action.has_leftend action || Invariant.endp symbol
in
elementif bind_beforeendp
let bind_startp = Invariant.startp symbol in
elementif (Action.has_beforeend action)
( (* Extract the field at offset 1 in the top stack cell. *)
PTuple [ PWildcard; PVar beforeendp ],
EVar stack
......@@ -1210,7 +1201,7 @@ let reducebody prod =
PTuple [ PWildcard; PVar startp ],
EVar stack
) @
elementif bind_endp
elementif (Invariant.endp symbol)
( if length > 0 then
PVar endp,
EVar (Printf.sprintf "_endpos_%s_" ids.(length - 1))
......@@ -1253,8 +1244,7 @@ let reducebody prod =
(blet (
(pat, EVar stack) ::
unitbindings @
posbindings action @
extrabindings action,
posbindings action,
(* If the semantic action is susceptible of raising [Error],
use a [let/unless] construct, otherwise use [let]. *)
......
......@@ -195,30 +195,6 @@ let destructuretokendef name codomain bindsemv branch = {
(* ------------------------------------------------------------------------ *)
(* Bindings for exotic keywords. *)
(* [extrabindings action] provides definitions for the [$startofs] and
[$endofs] keywords, if required by a semantic action. The parameter
[action] is the semantic action within which these keywords might be
used. *)
(* The [ofs] keyword family is defined in terms of the [pos] family by
accessing the [pos_cnum] field. *)
let extrabindings action =
let open Keyword in
KeywordSet.fold (fun keyword bindings ->
match keyword with
| Position (_, _, FlavorPosition)
| SyntaxError ->
bindings
| Position (s, w, (FlavorOffset as f)) ->
(PVar (posvar s w f),
ERecordAccess (EVar (posvar s w FlavorPosition), "Lexing.pos_cnum")) :: bindings
) (Action.keywords action) []
(* ------------------------------------------------------------------------ *)
(* A global variable holds the exception [Error]. *)
(* We preallocate the [Error] exception and store it into a global
......
......@@ -107,16 +107,6 @@ val destructuretokendef: string -> typ -> bool -> (Terminal.t -> expr) -> valdef
(* ------------------------------------------------------------------------ *)
(* Bindings for exotic keywords. *)
(* This provides definitions for the [$startofs] and [$endofs] keywords, if
required by a semantic action. The [ofs] keyword family is defined in terms
of the [pos] family by accessing the [pos_cnum] field. *)
val extrabindings: Action.t -> (pattern * expr) list
(* ------------------------------------------------------------------------ *)
(* A global variable holds the exception [Error]. *)
(* The definition of this global variable. *)
......
......@@ -68,9 +68,8 @@ module Run (T: sig end) = struct
(Nonterminal.print false nonterminal)
| Some _ -> ());
Production.iterx (fun prod ->
let act = Production.action prod in
if Action.(has_syntaxerror act || has_leftstart act || has_leftend act) then
Error.error [] "$syntaxerror, $start, $end are not supported by the Coq back-end."
if not (Keyword.KeywordSet.is_empty (Action.keywords (Production.action prod))) then
Error.error [] "The Coq back-end supports none of the $ keywords."
)
end;
......
......@@ -127,6 +127,13 @@ let grammar =
(* ------------------------------------------------------------------------- *)
(* Expand away some of the position keywords. *)
let grammar =
KeywordExpansion.expand_grammar grammar
(* ------------------------------------------------------------------------- *)
(* If [--no-inline] was specified on the command line, skip the
inlining of non terminal definitions marked with %inline. *)
......
open UnparameterizedSyntax
open Keyword
open IL
open CodeBits
(* [posvar_ keyword] constructs the conventional name of the variable
that stands for the position keyword [keyword]. *)
let posvar_ = function
| Position (subject, where, flavor) ->
posvar subject where flavor
| _ ->
assert false (* [posvar_] should be applied to a position keyword *)
(* [define keyword1 f keyword2] macro-expands [keyword1] as [f(keyword2)],
where [f] is a function of expressions to expressions. *)
let define keyword1 f keyword2 =
Action.define
keyword1
(KeywordSet.singleton keyword2)
(mlet
[ PVar (posvar_ keyword1) ]
[ f (EVar (posvar_ keyword2)) ])
(* [expand_action producers action] macro-expands certain keywords away
in the semantic action [action]. The list [producers] tells us how
many elements appear in this production. *)
let expand_action producers action =
let n = List.length producers in
KeywordSet.fold (fun keyword action ->
match keyword with
| Position (subject, where, FlavorOffset) ->
(* The [ofs] keyword family is defined in terms of the [pos] family by
accessing the [pos_cnum] field. *)
define keyword
(fun e -> ERecordAccess (e, "Lexing.pos_cnum"))
(Position (subject, where, FlavorPosition))
action
| Position (Left, WhereStart, flavor) ->
(* [$startpos] is defined as [$startpos($1)] if this production has
nonzero length and [$endpos($0)] otherwise. *)
define keyword (fun e -> e) (
if n > 0 then
let _, x = List.hd producers in
Position (RightNamed x, WhereStart, flavor)
else
Position (Before, WhereEnd, flavor)
) action
| Position (Left, WhereEnd, flavor) ->
(* [$endpos] is defined as [$endpos($n)] if this production has
nonzero length and [$endpos($0)] otherwise. *)
define keyword (fun e -> e) (
if n > 0 then
let _, x = List.hd (List.rev producers) in
Position (RightNamed x, WhereEnd, flavor)
else
Position (Before, WhereEnd, flavor)
) action
| Position (Before, _, _)
| Position (RightNamed _, _, _)
| SyntaxError ->
action
) (Action.keywords action) action
let expand_branch branch =
{ branch with action = expand_action branch.producers branch.action }
let expand_rule rule =
{ rule with branches = List.map expand_branch rule.branches }
let expand_grammar grammar =
{ grammar with rules = StringMap.map expand_rule grammar.rules }
open UnparameterizedSyntax
(* [expand_grammar] expands away the keywords [$startpos] and [$endpos], as well
the entire [ofs] family of keywords. Doing this early simplifies some aspects
later on, in particular %inlining. *)
val expand_grammar: grammar -> grammar
......@@ -842,9 +842,10 @@ let invert reductions : TerminalSet.t ProductionMap.t =
position of the cell that is at the top of the stack after popping and
before pushing. *)
(* This is the case if [s] can reduce an epsilon production whose semantic
action uses [$startpos] or [$endpos]. This is also the case if [s] can
reduce a production whose semantic action uses [$endpos($0)]. *)
(* This is also the case if [s] can reduce a production whose semantic
action uses [$endpos($0)]. Note that [$startpos] and [$endpos] have
been expanded away, so we need not worry about the fact that they
can be used in an epsilon production. *)
let has_beforeend node =
TerminalMap.fold (fun _ prods accu ->
......@@ -852,8 +853,7 @@ let has_beforeend node =
let prod = Misc.single prods in
not (Production.is_start prod) &&
let action = Production.action prod in
Production.length prod = 0 && Action.has_left action
|| Action.has_beforeend action
Action.has_beforeend action
) (reductions node) false
(* ------------------------------------------------------------------------ *)
......
......@@ -22,19 +22,12 @@ let index2id producers i =
(* [rename_sw_outer] transforms the keywords in the outer production (the
caller) during inlining. It replaces [$startpos(x)] and [$endpos(x)], where
[x] is the name of the callee, with [startpx] and [endpx], respectively. It
also replaces [$startpos] with [startp]. Although in most cases [startp]
will be [$startpos] -- so [$startpos] is not affected -- in the special
case where we are inlining an epsilon production in front of the outer
production, we must replace [$startpos] with [$endpos($0)]. *)
[x] is the name of the callee, with [startpx] and [endpx], respectively. *)
let rename_sw_outer (x, startpx, endpx, startp) (subject, where) : (subject * where) option =
let rename_sw_outer (x, startpx, endpx) (subject, where) : (subject * where) option =
match subject, where with
| Before, _
| Left, WhereEnd ->
| Before, _ ->
None
| Left, WhereStart ->
Some startp
| RightNamed x', _ ->
if x' = x then
match where with
......@@ -42,24 +35,25 @@ let rename_sw_outer (x, startpx, endpx, startp) (subject, where) : (subject * wh
| WhereEnd -> Some endpx
else
None
| Left, _ ->
(* [$startpos] and [$endpos] have been expanded away earlier; see
[KeywordExpansion]. *)
assert false
(* [rename_sw_inner] transforms the keywords in the inner production (the callee)
during inlining. It looks for [$endpos($0)], [$startpos], and [$endpos], and
replaces them with [beforeendp], [startp], and [endp], respectively. *)
(* It does not modify any [$startpos(x)], of course. *)
during inlining. It replaces [$endpos($0)] with [beforeendp]. *)
let rename_sw_inner (beforeendp, startp, endp) (subject, where) : (subject * where) option =
let rename_sw_inner beforeendp (subject, where) : (subject * where) option =
match subject, where with
| Before, _ ->
assert (where = WhereEnd);
Some beforeendp
| Left, WhereStart ->
Some startp
| Left, WhereEnd ->
Some endp
| RightNamed _, _ ->
None
| Left, _ ->
(* [$startpos] and [$endpos] have been expanded away earlier; see
[KeywordExpansion]. *)
assert false
(* Inline a grammar. The resulting grammar does not contain any definitions
that can be inlined. *)
......@@ -230,26 +224,11 @@ let inline grammar =
Before, WhereEnd
in
(* In the special case where the inner production is epsilon and
the prefix is empty, [$startpos] in the outer production must
be changed to [$endpos($0)] in order to preserve the semantics.
Indeed, if we do not do anything special, inlining causes the
inner production to disappear, so [$startpos] will be computed
based on the next element of the outer production, whereas in
the absence of inlining, it was computed by the epsilon production. *)
let outer_startp =
if inlined_producers = 0 && prefix = 0 then
Before, WhereEnd
else
Left, WhereStart
in
(* Rename the outer and inner semantic action. *)
let outer_action =
Action.rename (rename_sw_outer (c, startp, endp, outer_startp)) [] b.action
Action.rename (rename_sw_outer (c, startp, endp)) [] b.action
and action' =
Action.rename (rename_sw_inner (beforeendp, startp, endp)) phi pb.action
Action.rename (rename_sw_inner beforeendp) phi pb.action
in
{ b with
......
......@@ -247,7 +247,6 @@ let reducebody prod =
(pat, EVar stack) :: (* destructure the stack *)
casts @ (* perform type casts *)
posbindings @ (* bind [startp] and [endp] *)
extrabindings action @ (* add bindings for the weird keywords *)
[ PVar semv, act ], (* run the user's code and bind [semv] *)
(* Return a new stack, onto which we have pushed a new stack cell. *)
......
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