Remove the Sfacto constructor from Gramlib.

Used by rule factorisation in theory, but appears to be unused in Coq.

4 files changed, 0 insertions, 30 deletions

diff --git a/gramlib/gramext.ml b/gramlib/gramext.ml
index 3b2c3de760..de9b1e864c 100644
--- a/gramlib/gramext.ml
+++ b/gramlib/gramext.ml
@@ -27,7 +27,6 @@ and 'te g_level =
     lprefix : 'te g_tree }
 and g_assoc = NonA | RightA | LeftA
 and 'te g_symbol =
-    Sfacto of 'te g_symbol
   | Snterm of 'te g_entry
   | Snterml of 'te g_entry * string
   | Slist0 of 'te g_symbol
@@ -65,7 +64,6 @@ let rec derive_eps =
     Slist0 _ -> true
   | Slist0sep (_, _, _) -> true
   | Sopt _ | Sflag _ -> true
-  | Sfacto s -> derive_eps s
   | Stree t -> tree_derive_eps t
   | Slist1 _ | Slist1sep (_, _, _) | Snterm _ |
     Snterml (_, _) | Snext | Sself | Scut | Stoken _ ->
@@ -90,21 +88,6 @@ let rec eq_symbol s1 s2 =
   | Sflag s1, Sflag s2 -> eq_symbol s1 s2
   | Sopt s1, Sopt s2 -> eq_symbol s1 s2
   | Stree _, Stree _ -> false
-  | Sfacto (Stree t1), Sfacto (Stree t2) ->
-      (* The only goal of the node 'Sfacto' is to allow tree comparison
-         (therefore factorization) without looking at the semantic
-         actions; allow factorization of rules like "SV foo" which are
-         actually expanded into a tree. *)
-      let rec eq_tree t1 t2 =
-        match t1, t2 with
-          Node n1, Node n2 ->
-            eq_symbol n1.node n2.node && eq_tree n1.son n2.son &&
-            eq_tree n1.brother n2.brother
-        | LocAct (_, _), LocAct (_, _) -> true
-        | DeadEnd, DeadEnd -> true
-        | _ -> false
-      in
-      eq_tree t1 t2
   | _ -> s1 = s2
 
 let is_before s1 s2 =
@@ -189,7 +172,6 @@ and token_exists_in_tree f =
   | LocAct (_, _) | DeadEnd -> false
 and token_exists_in_symbol f =
   function
-    Sfacto sy -> token_exists_in_symbol f sy
   | Slist0 sy -> token_exists_in_symbol f sy
   | Slist0sep (sy, sep, _) ->
       token_exists_in_symbol f sy || token_exists_in_symbol f sep
@@ -325,7 +307,6 @@ Error: entries \"%s\" and \"%s\" do not belong to the same grammar.\n"
           flush stderr;
           failwith "Grammar.extend error"
         end
-  | Sfacto s -> check_gram entry s
   | Slist0sep (s, t, _) -> check_gram entry t; check_gram entry s
   | Slist1sep (s, t, _) -> check_gram entry t; check_gram entry s
   | Slist0 s -> check_gram entry s
@@ -353,7 +334,6 @@ let get_initial entry =
 let insert_tokens gram symbols =
   let rec insert =
     function
-      Sfacto s -> insert s
     | Slist0 s -> insert s
     | Slist1 s -> insert s
     | Slist0sep (s, t, _) -> insert s; insert t
@@ -487,7 +467,6 @@ let rec decr_keyw_use gram =
           Hashtbl.remove gram.gtokens tok;
           gram.glexer.Plexing.tok_removing tok
         end
-  | Sfacto s -> decr_keyw_use gram s
   | Slist0 s -> decr_keyw_use gram s
   | Slist1 s -> decr_keyw_use gram s
   | Slist0sep (s1, s2, _) -> decr_keyw_use gram s1; decr_keyw_use gram s2
diff --git a/gramlib/gramext.mli b/gramlib/gramext.mli
index eb2ea7576b..ff59bae578 100644
--- a/gramlib/gramext.mli
+++ b/gramlib/gramext.mli
@@ -25,7 +25,6 @@ and 'te g_level =
     lprefix : 'te g_tree }
 and g_assoc = NonA | RightA | LeftA
 and 'te g_symbol =
-    Sfacto of 'te g_symbol
   | Snterm of 'te g_entry
   | Snterml of 'te g_entry * string
   | Slist0 of 'te g_symbol
diff --git a/gramlib/grammar.ml b/gramlib/grammar.ml
index cdc3945323..6e99861423 100644
--- a/gramlib/grammar.ml
+++ b/gramlib/grammar.ml
@@ -41,7 +41,6 @@ let print_str ppf s = fprintf ppf "\"%s\"" (string_escaped s)
 
 let rec print_symbol ppf =
   function
-    Sfacto s -> print_symbol ppf s
   | Slist0 s -> fprintf ppf "LIST0 %a" print_symbol1 s
   | Slist0sep (s, t, osep) ->
       fprintf ppf "LIST0 %a SEP %a%s" print_symbol1 s print_symbol1 t
@@ -61,7 +60,6 @@ let rec print_symbol ppf =
       print_symbol1 ppf s
 and print_symbol1 ppf =
   function
-    Sfacto s -> print_symbol1 ppf s
   | Snterm e -> fprintf ppf "%s%s" e.ename (if e.elocal then "*" else "")
   | Sself -> pp_print_string ppf "SELF"
   | Snext -> pp_print_string ppf "NEXT"
@@ -150,7 +148,6 @@ let rec get_token_list entry rev_tokl last_tok tree =
 
 let rec name_of_symbol_failed entry =
   function
-    Sfacto s -> name_of_symbol_failed entry s
   | Slist0 s -> name_of_symbol_failed entry s
   | Slist0sep (s, _, _) -> name_of_symbol_failed entry s
   | Slist1 s -> name_of_symbol_failed entry s
@@ -538,7 +535,6 @@ and parser_of_token_list entry s son p1 p2 rev_tokl last_tok =
         let a = ps strm__ in let act = p1 strm__ in app act a
 and parser_of_symbol entry nlevn =
   function
-    Sfacto s -> parser_of_symbol entry nlevn s
   | Slist0 s ->
       let ps = call_and_push (parser_of_symbol entry nlevn s) in
       let rec loop al (strm__ : _ Stream.t) =
@@ -873,7 +869,6 @@ let find_entry e s =
         | x -> x
   and find_symbol =
     function
-      Sfacto s -> find_symbol s
     | Snterm e -> if e.ename = s then Some e else None
     | Snterml (e, _) -> if e.ename = s then Some e else None
     | Slist0 s -> find_symbol s
@@ -991,7 +986,6 @@ module type S =
     type ('self, 'a) ty_symbol
     type ('self, 'f, 'r) ty_rule
     type 'a ty_production
-    val s_facto : ('self, 'a) ty_symbol -> ('self, 'a) ty_symbol
     val s_nterm : 'a Entry.e -> ('self, 'a) ty_symbol
     val s_nterml : 'a Entry.e -> string -> ('self, 'a) ty_symbol
     val s_list0 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol
@@ -1081,7 +1075,6 @@ module GMake (L : GLexerType) =
     type ('self, 'a) ty_symbol = te Gramext.g_symbol
     type ('self, 'f, 'r) ty_rule = ('self, Obj.t) ty_symbol list
     type 'a ty_production = ('a, Obj.t, Obj.t) ty_rule * Gramext.g_action
-    let s_facto s = Sfacto s
     let s_nterm e = Snterm e
     let s_nterml e l = Snterml (e, l)
     let s_list0 s = Slist0 s
diff --git a/gramlib/grammar.mli b/gramlib/grammar.mli
index 7bbf799938..e115b9df43 100644
--- a/gramlib/grammar.mli
+++ b/gramlib/grammar.mli
@@ -112,7 +112,6 @@ module type S =
     type ('self, 'a) ty_symbol
     type ('self, 'f, 'r) ty_rule
     type 'a ty_production
-    val s_facto : ('self, 'a) ty_symbol -> ('self, 'a) ty_symbol
     val s_nterm : 'a Entry.e -> ('self, 'a) ty_symbol
     val s_nterml : 'a Entry.e -> string -> ('self, 'a) ty_symbol
     val s_list0 : ('self, 'a) ty_symbol -> ('self, 'a list) ty_symbol