nonTerminalDefinitionInlining.ml 6.11 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
open UnparameterizedSyntax
open ListMonad

(* This exception will be raised when a branch does not need inlining. *)
exception NoInlining

(* Color are used to detect cycles. *)
type 'a color = 
  | BeingExpanded
  | Expanded of 'a

(* Inline a grammar. The resulting grammar does not contain any definitions
   that can be inlined. *)
let inline grammar = 

  let names producers = 
17
    List.fold_left (fun s (_, x) -> StringSet.add x s) 
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
      StringSet.empty producers 
  in

  (* This function returns a fresh name beginning with [prefix] and 
     that is not in the set of names [names]. *)
  let rec fresh ?(c=0) names prefix =
    let name = prefix^string_of_int c in
      if StringSet.mem name names then
	fresh ~c:(c+1) names prefix
      else 
	name
  in

  let use_inline = ref false in

  (* This table associates a color to each non terminal that can be expanded. *)
  let expanded_non_terminals = 
    Hashtbl.create 13 
  in

  let expanded_state k = 
    Hashtbl.find expanded_non_terminals k 
  in
      
  let mark_as_being_expanded k = 
    Hashtbl.add expanded_non_terminals k BeingExpanded
  in

  let mark_as_expanded k r =
    Hashtbl.replace expanded_non_terminals  k (Expanded r);
    r
  in

  (* This function traverses the producers of the branch [b] and find
     the first non terminal that can be inlined. If it finds one, it
     inlines its branches into [b], that's why this function can return
     several branches. If it does not find one non terminal to be 
     inlined, it raises [NoInlining]. *)
  let rec find_inline_producer b = 
    let prefix, nt, p, psym, suffix = 
      let rec chop_inline i (prefix, suffix) =
	match suffix with
	  | [] -> 
	      raise NoInlining

	  | ((nt, id) as x) :: xs ->
	      try
		let r = StringMap.find nt grammar.rules in
66
		if r.inline_flag then 
67
68
		    (* We have to inline the rule [r] into [b] between
		       [prefix] and [xs]. *)
69
70
71
		  List.rev prefix, nt, r, id, xs
		else 
		  chop_inline (i + 1) (x :: prefix, xs) 
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
	      with Not_found -> 
		chop_inline (i + 1) (x :: prefix, xs) 
      in
	chop_inline 1 ([], b.producers)
    in
      prefix, expand_rule nt p, nt, psym, suffix

  (* We have to rename producers' names of the inlined production 
     if they clashes with the producers' names of the branch into 
     which we do the inlining. *)
  and rename_if_necessary b producers =

    (* First we compute the set of names already in use. *)
    let producers_names = names (b.producers @ producers) in

    (* Compute a renaming and the new inlined producers' names. *)
    let phi, producers' =
89
90
91
92
93
94
95
      List.fold_left (fun (phi, producers) (p, x) -> 
	if StringSet.mem x producers_names then
	  let x' = fresh producers_names x in
	  ((x, x') :: phi, (p, x') :: producers)
	else 
	  (phi, (p, x) :: producers)
      ) ([], []) producers
96
97
98
99
100
101
    in
      phi, List.rev producers'
	
  (* Inline the non terminals that can be inlined in [b]. We use the 
     ListMonad to combine the results. *)
  and expand_branch (b : branch) : branch ListMonad.m =
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
    try
      let prefix, p, _nt, psym, suffix = find_inline_producer b in
      use_inline := true;
      (* Inline a branch of [nt] at position [prefix] ... [suffix] in
	 the branch [b]. *)
      let inline_branch pb =
	(* Rename the producers of this branch is they conflict with
	   the name of the host's producers. *)
	let phi, inlined_producers = rename_if_necessary b pb.producers in

	(* Define the renaming environment given the shape of the branch. *)
	let renaming_env, prefix', suffix' =

	  let start_position, prefix' =
	    match List.rev prefix with

	      (* If the prefix is empty, the start position is the rule
		 start position. *)
	      | [] -> (Keyword.Left, Keyword.WhereStart), prefix

	      (* The last producer of prefix is named [x],
		 $startpos in the inlined rule will be changed to $endpos(x). *)
	      | (_, x) :: _ -> (Keyword.RightNamed x, Keyword.WhereEnd), prefix

	  in
	  (* Same thing for the suffix. *)
	  let end_position, suffix' =
	    match suffix with
	      | [] -> (Keyword.Left, Keyword.WhereEnd), suffix
	      | (_, x) :: _ -> (Keyword.RightNamed x, Keyword.WhereStart), suffix
132
	  in
133
134
135
136
137
138
139
140
141
142
143
144
145
	  (psym, start_position, end_position), prefix', suffix'
	in
	(* Rename the host semantic action.
	   Each reference of the inlined non terminal [psym] must be taken into
	   account. $startpos(psym) is changed to $startpos(x) where [x] is
	   the first producer of the inlined branch if it is not empty or
	   the preceding producer found in the prefix. *)
	let outer_action, (used1, used2) =
	  Action.rename_inlined_psym renaming_env [] b.action
	in
	let action', (used1', used2') =
	  Action.rename renaming_env phi pb.action
	in
146
        assert (prefix == prefix' && suffix == suffix');
147
148
149
150
151
152
153
154
155
156
157
	let prefix = if used1 || used1' then prefix' else prefix in
	let suffix = if used2 || used2' then suffix' else suffix in

	{ b with
	  producers = prefix @ inlined_producers @ suffix;
	  action = Action.compose psym action' outer_action
	}
      in
      List.map inline_branch p.branches >>= expand_branch

    with NoInlining ->
158
      return b
159

160
161
162
163
164
165
166
  (* Expand a rule if necessary. *)
  and expand_rule k r = 
    try 
      (match expanded_state k with
	 | BeingExpanded ->
    	     Error.error
	       r.positions
167
	       "there is a cycle in the definition of %s." k
168
169
170
171
172
173
174
	 | Expanded r ->
	     r)
    with Not_found ->
      mark_as_being_expanded k;
      mark_as_expanded k { r with branches = r.branches >>= expand_branch }
  in

175
  (* If we are in Coq mode, %inline is forbidden. *)
176
177
178
179
180
181
  let _ =
    if Settings.coq then
      StringMap.iter 
        (fun _ r -> 
	   if r.inline_flag then
             Error.error r.positions
182
               "%%inline is not supported by the Coq back-end.")
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
        grammar.rules
  in

    (* To expand a grammar, we expand all its rules and remove 
       the %inline rules. *)
  let expanded_rules = 
    StringMap.mapi expand_rule grammar.rules
  and useful_types = 
      StringMap.filter 
	(fun k _ -> try not (StringMap.find k grammar.rules).inline_flag
	 with Not_found -> true)
	grammar.types
  in

    { grammar with 
	rules = StringMap.filter (fun _ r -> not r.inline_flag) expanded_rules;
	types = useful_types
    }, !use_inline