From 35e59e49de3194449a3e89f6dd35678af4337357 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Franc=CC=A7ois=20Pottier?= Date: Wed, 6 Dec 2017 15:21:27 +0100 Subject: [PATCH] Front: implement selective expansion + safety test + full expansion. --- src/front.ml | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/src/front.ml b/src/front.ml index aea12016..7a6f4b7c 100644 --- a/src/front.ml +++ b/src/front.ml @@ -76,9 +76,21 @@ let sorts = to obtain a grammar without parameterized nonterminal symbols. *) let grammar : UnparameterizedSyntax.grammar = - (* TEMPORARY do selective expansion first *) - CheckSafeParameterizedGrammar.check grammar; - Drop.drop (SelectiveExpansion.expand SelectiveExpansion.ExpandAll sorts grammar) + let module S = SelectiveExpansion in + (* First, perform a selective expansion: expand away all parameters of + higher sort, keeping the parameters of sort [*]. This process always + terminates. *) + let grammar1 = S.expand S.ExpandHigherSort sorts grammar in + (* This "first-order parameterized grammar" can then be submitted to + the termination check. *) + CheckSafeParameterizedGrammar.check grammar1; + (* If it passes the check, then full expansion is safe. We drop [grammar1] + and start over from [grammar]. This is required in order to get correct + names. (Expanding [grammar1] would yield an equivalent grammar, with + more complicated names, reflecting the two steps of expansion.) *) + let grammar = S.expand S.ExpandAll sorts grammar in + (* This yields an unparameterized grammar. *) + Drop.drop grammar let () = Time.tick "Joining and expanding" -- GitLab