nonTerminalDefinitionInlining.ml 6.17 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17
(* $Id: nonTerminalDefinitionInlining.ml,v 1.17 2006/06/26 09:41:33 regisgia Exp $ *)
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 = 
18
    List.fold_left (fun s (_, x) -> StringSet.add x s) 
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 66
      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
67
		if r.inline_flag then 
68 69
		    (* We have to inline the rule [r] into [b] between
		       [prefix] and [xs]. *)
70 71 72
		  List.rev prefix, nt, r, id, xs
		else 
		  chop_inline (i + 1) (x :: prefix, xs) 
73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89
	      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' =
90 91 92 93 94 95 96
      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
97 98 99 100 101 102
    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 =
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 132
    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
133
	  in
134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157
	  (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
	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 167 168 169 170 171 172 173 174
  (* Expand a rule if necessary. *)
  and expand_rule k r = 
    try 
      (match expanded_state k with
	 | BeingExpanded ->
    	     Error.error
	       r.positions
	       (Printf.sprintf "there is a cycle in the definition of %s." k)
	 | 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 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201
  let _ =
    if Settings.coq then
      StringMap.iter 
        (fun _ r -> 
	   if r.inline_flag then
             Error.error r.positions
               (Printf.sprintf "%%inline is not supported by the coq back-end"))
        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