remove the printing of weird notations for substitutions as functions

Author: MevenBertrand

lib/automationGen.ml

@@ -141,10 +141,8 @@ module NotationGen = struct
          | Up
          | UpInst of string
          | SubstApply of string list
-         | Subst of string list
          | RenApply of string list
-         | Ren of string list
-
+        
   let subst_scope = "subst_scope"
   let fscope = "fscope"
 
@@ -167,13 +165,9 @@ module NotationGen = struct
       sprintf "↑__%s" sort
     | SubstApply substSorts ->
       sprintf "s [ %s ]" (concat_substs (to_substs "sigma" substSorts))
-    | Subst substSorts ->
-      sprintf "[ %s ]" (concat_substs (to_substs "sigma" substSorts))
     | RenApply substSorts ->
       sprintf "s ⟨ %s ⟩" (concat_substs (to_substs "xi" substSorts))
-    | Ren substSorts ->
-      sprintf "⟨ %s ⟩" (concat_substs (to_substs "xi" substSorts))
-
+    
   let notation_modifiers sort n =
     let open Printf in
     match n with
@@ -189,16 +183,12 @@ module NotationGen = struct
       [ only_print_ ]
     | SubstApply _ | RenApply _ ->
       [ level_ 7; assoc_ LeftA; only_print_ ]
-    | Subst _ | Ren _ ->
-      [ level_ 1; assoc_ LeftA; only_print_ ]
-
+    
   let notation_scope = function
     | VarConstr | VarInst | Var | Up | UpInst _
     | SubstApply _ | RenApply _ ->
       subst_scope
-    | Subst _ | Ren _ ->
-      fscope
-
+    
   (* DONE hardcoded strings ersetzen durch die korrekten functionen in CoqNames *)
   let notation_body sort = function
     | VarConstr -> app_ref (var_ sort) [ ref_ "x" ]
@@ -208,9 +198,7 @@ module NotationGen = struct
     | Up -> ref_ (up_class_ sort)
     | UpInst bsort -> ref_ (up_inst_ bsort sort)
     | SubstApply substSorts -> app_ref (subst_ sort) ((List.map ref_ (to_substs "sigma" substSorts)) @ [ ref_ "s" ])
-    | Subst substSorts -> app_ref (subst_ sort) (List.map ref_ (to_substs "sigma" substSorts))
     | RenApply substSorts -> app_ref (ren_ sort) ((List.map ref_ (to_substs "xi" substSorts)) @ [ ref_ "s" ])
-    | Ren substSorts -> app_ref (ren_ sort) (List.map ref_ (to_substs "xi" substSorts))
 end
 
 

lib/automationGen.mli

@@ -52,9 +52,7 @@ module NotationGen : sig
          | Up
          | UpInst of string
          | SubstApply of string list
-         | Subst of string list
          | RenApply of string list
-         | Ren of string list
 
   val fscope : scope_name
   val subst_scope : scope_name

lib/codeGenerator.ml

@@ -250,7 +250,6 @@ module Renamings : COMPONENT_GENERATOR = FixGen(struct
       let* () = tell_instance (ClassGen.Ren (List.length substSorts), sort, ss_names ms @ ss_names ns) in
       let* () = tell_cbn_function (ren_ sort) in
       let* () = tell_notation (NotationGen.RenApply substSorts, sort) in
-      let* () = tell_notation (NotationGen.Ren substSorts, sort) in
       let* () = tell_proper_instance (sort, ren_ sort, extRen_ sort) in
       (* DONE what is the result of to_var here?\
        * when I call it with sort=tm, xi=[xity;xivl] I get this weird error term that to_var constructs. This is then probably ignored by some similar logic in the traversal. Seems brittle.
@@ -330,7 +329,6 @@ module Substitutions : COMPONENT_GENERATOR = FixGen(struct
       let* () = tell_class (ClassGen.Up "", sort) in
       let* () = tell_notation (NotationGen.Up, sort) in
       let* () = tell_notation (NotationGen.SubstApply substSorts, sort) in
-      let* () = tell_notation (NotationGen.Subst substSorts, sort) in
       let* () = tell_proper_instance (sort, subst_ sort, ext_ sort) in
       (** type *)
       let (s, bs) = genMatchVar sort ms in