Commits

Thomas Tuerk  committed c7ef1b4

improved whitespacing and parentheses for inlining and target-reps

moreover, removed infix_swap (as it turned out tricky
to implement correctly) and changed syntax of undefined target-reps to
avoid using "undefined" as an extra keyword

  • Participants
  • Parent commits 8483cdf

Comments (0)

Files changed (20)

File language/lem.ott

 target_rep_rhs :: 'Target_rep_rhs_' ::=
   {{ com right hand side of a target representation declaration }}
   | infix fixity_decl backtick_string :: :: infix
-  | infix_swap fixity_decl backtick_string :: :: infix_swap
   | exp                          :: :: term_replacement
   | typ                          :: :: type_replacement
   | special string exp1 ... expn :: :: special
-  | undefined                    :: :: undefined
+  |                              :: :: undefined
 
 target_rep_lhs  :: 'Target_rep_lhs_' ::=
   {{ com left hand side of a target representation declaration }}

File library/basic_classes.lem

 type ordering = LT | EQ | GT
 
 declare ocaml target_rep type ordering = `int`
-declare ocaml target_rep function LT = `-1`
+declare ocaml target_rep function LT = `(-1)`
 declare ocaml target_rep function EQ = `0`
 declare ocaml target_rep function GT = `1`
 
 val defaultGreaterEq : forall 'a. 'a -> 'a -> bool
 
 declare ocaml    target_rep function defaultCompare = `compare`
-declare hol      target_rep function defaultCompare = undefined
-declare isabelle target_rep function defaultCompare = undefined
+declare hol      target_rep function defaultCompare = 
+declare isabelle target_rep function defaultCompare = 
 declare coq      target_rep function defaultCompare x y = EQ
 
 declare ocaml    target_rep function defaultLess = infix `<`
-declare hol      target_rep function defaultLess = undefined
-declare isabelle target_rep function defaultLess = undefined
-declare coq      target_rep function defaultLess = undefined
+declare hol      target_rep function defaultLess = 
+declare isabelle target_rep function defaultLess = 
+declare coq      target_rep function defaultLess = 
 
 declare ocaml    target_rep function defaultLessEq = infix `<=`
-declare hol      target_rep function defaultLessEq = undefined
-declare isabelle target_rep function defaultLessEq = undefined
-declare coq      target_rep function defaultLessEq = undefined
+declare hol      target_rep function defaultLessEq = 
+declare isabelle target_rep function defaultLessEq = 
+declare coq      target_rep function defaultLessEq = 
 
 declare ocaml    target_rep function defaultGreater = infix `>`
-declare hol      target_rep function defaultGreater = undefined
-declare isabelle target_rep function defaultGreater = undefined
-declare coq      target_rep function defaultGreater = undefined
+declare hol      target_rep function defaultGreater = 
+declare isabelle target_rep function defaultGreater = 
+declare coq      target_rep function defaultGreater = 
 
 declare ocaml    target_rep function defaultGreaterEq = infix `>=`
-declare hol      target_rep function defaultGreaterEq = undefined
-declare isabelle target_rep function defaultGreaterEq = undefined
-declare coq      target_rep function defaultGreaterEq = undefined
+declare hol      target_rep function defaultGreaterEq = 
+declare isabelle target_rep function defaultGreaterEq = 
+declare coq      target_rep function defaultGreaterEq = 
 
 (*
 (* compare should really be a total order *)
 type 
 target_rep_rhs =  (* right hand side of a target representation declaration *)
    Target_rep_rhs_infix of terminal * fixity_decl * terminal * Ulib.UTF8.t
- | Target_rep_rhs_infix_swap of terminal * fixity_decl * terminal * Ulib.UTF8.t
  | Target_rep_rhs_term_replacement of exp
  | Target_rep_rhs_type_replacement of typ
  | Target_rep_rhs_special of terminal * terminal * Ulib.UTF8.t * (exp) list
- | Target_rep_rhs_undefined of terminal
+ | Target_rep_rhs_undefined
 
 
 type 

File src/backend.ml

   let reln_clause_add_paren = false
   let reln_clause_start = emp
 
-  let backend_quote i = i
+  let backend_quote i = (meta "`") ^ i ^ (meta "`")
 end
 
 module Lem : Target = struct
   include Identity 
   let target = Target_no_ident Target_lem
 
-  let backend_quote i = i
+  let backend_quote i = (meta "`") ^ i ^ (meta "`")
 end
 
 module Tex : Target = struct
   let target = Target_no_ident Target_ocaml
 
   let path_sep = kwd "."
-  let backend_quote i = i
+  let backend_quote i = (meta "`") ^ i ^ (meta "`")
 
   let typ_rec_start = kwd "{"
   let typ_rec_end = kwd "}"
 
   let path_sep = kwd "."
   let list_sep = kwd ","
-  let backend_quote i = i
+  let backend_quote i = (meta "`") ^ i ^ (meta "`")
 
   let ctor_typ_end _ _ = emp
   let ctor_typ_end' _ _ _ = emp
 
   let path_sep = meta "$"
   let list_sep = kwd ";"
-  let backend_quote i = i
+  let backend_quote i = (meta "`") ^ i ^ (meta "`")
 
   let ctor_typ_end _ _ = emp
   let ctor_typ_end' _ _ _ = emp
           | Typ_app _ -> B.type_app_to_output typ p ts
           | Typ_backend _ -> (ts, 
 	      let i = Path.to_ident (ident_get_lskip p) p.descr in
+              let i_out = (Ident.to_output Type_ctor T.path_sep (Ident.replace_lskip i None)) in
               ws (Ident.get_lskip i) ^
-              T.backend_quote (Ident.to_output Type_ctor T.path_sep (Ident.replace_lskip i None)))
+              if (T.target = Target.Target_ident) then
+                T.backend_quote i_out
+              else i_out)
           | _ -> raise (Reporting_basic.err_unreachable (Ast.Trans (false, "Backend.typ", None)) "can't be reached because of previous match")
       end in
       if (T.type_params_pre) then
               (sep (texspace ^ kwd "|" ^ texspace))
               constrs))
 
-let backend sk i =
+let backend inlined sk i =
   ws sk ^
-  T.backend_quote (Ident.to_output Term_const T.path_sep i) 
+  if inlined then
+    Ident.to_output Term_const T.path_sep i
+  else
+    T.backend_quote (Ident.to_output Term_const T.path_sep i) 
 
 let rec pat p = match p.term with
   | P_wild(s) ->
   | P_const(cd,ps) ->
       let oL = B.pattern_application_to_output p.locn pat cd ps (use_ascii_rep_for_const cd) in
       concat texspace oL
-  | P_backend(sk,i,_,ps) ->
-      backend sk i ^
+  | P_backend(inlined, sk,i,_,ps) ->
+      backend inlined sk i ^
       concat texspace (List.map pat ps)
   | P_record(s1,fields,s2) ->
       ws s1 ^
 match C.exp_to_term e with
   | Var(n) ->
       Name.to_output Term_var n
-  | Backend(sk, i) ->
-      backend sk i
+  | Backend(inlined, sk, i) ->
+      backend inlined sk i
   | Nvar_e(s,n) ->
       ws s ^ id Nexpr_var (Ulib.Text.(^^^) T.nexp_var (Nvar.to_rope n))
   | Constant(cd) ->
       Output.concat emp (B.function_application_to_output (exp_to_locn e) exp false e cd [] (use_ascii_rep_for_const cd))
-
   | Fun(s1,ps,s2,e) ->
       ws s1 ^
       T.fun_start ^
   | Ast.Ascii_opt_some (sk1, sk2, q, sk3) -> 
      if (is_human_target T.target) then begin
         let i = Ident.mk_ident_strings [] q in
-        ws sk1 ^ kwd "[" ^ backend sk2 i ^ ws sk3 ^ kwd "]" 
+        ws sk1 ^ kwd "[" ^ backend false sk2 i ^ ws sk3 ^ kwd "]" 
      end else emp
 
 let infix_decl = function
         kwd "=" ^
         (match rhs with
           | Target_rep_rhs_term_replacement e -> exp e
-          | Target_rep_rhs_undefined sk -> ws sk ^ kwd "undefined"
-          | Target_rep_rhs_infix (sk1, swap, decl, sk2, i) -> begin
+          | Target_rep_rhs_undefined -> emp
+          | Target_rep_rhs_infix (sk1, decl, sk2, i) -> begin
                ws sk1 ^
-               (if swap then kwd "infix_swap" else kwd "infix") ^
+               kwd "infix" ^
                infix_decl decl ^
-               backend sk2 i
+               backend false sk2 i
             end
           | _ -> raise (Reporting_basic.err_todo true Ast.Unknown "declaration")
         ) 
       let n' = Name.strip_lskip n in 
       [(Name.to_rope n', Name.to_rope_tex Term_ctor n', p.locn)] @
       List.flatten (List.map names_of_pat ps)
-  | P_backend(sk,i,_,ps) ->
+  | P_backend(_,_,i,_,ps) ->
       let n = Name.strip_lskip (Ident.get_name i) in
       [(Name.to_rope n, Name.to_rope_tex Term_ctor n, p.locn)] @
       List.flatten (List.map names_of_pat ps)

File src/backend_common.ml

 let r = Ulib.Text.of_latin1
 let marker_lex_skip : Ast.lex_skips = (Some [Ast.Ws (Ulib.Text.of_latin1 "***marker***")])
 
+let mark_backend_exp_for_inline _ e = 
+  let old_l = exp_to_locn e in
+  let old_t = exp_to_typ e in
+  let module C = Exps_in_context(struct let env_opt = None;; let avoid = None end) in
+  match (C.exp_to_term e) with
+    | Backend(false, sk, i) ->
+        Some (C.mk_backend old_l true sk i old_t)
+    | _ -> None
+
+
+let cleanup_for_inline env e : exp = begin 
+   let module Ctxt = struct let avoid = None let env_opt = (Some env) end in
+   let module M = Macro_expander.Expander(Ctxt) in
+   M.expand_exp Macro_expander.Ctxt_other 
+                (Macro_expander.list_to_mac [mark_backend_exp_for_inline],
+                (fun ty -> ty),
+                (fun ty -> ty),
+                Macro_expander.list_to_bool_mac []) e
+ end
+
+
 (* Resolve a const identifier stored inside a id, with a full one in case of Id_none *)
 let resolve_constant_id_ident l env targ id : Ident.t =
   resolve_const_ref l env targ id.id_path id.descr
     | (params, []) -> (Nfmap.empty, params, [])
     | (p::params, a::args) ->
         let (subst, x, y) = build_subst params args in
-          (Nfmap.insert subst (Name.strip_lskip p.term, Sub(a)), x, y)
+        let (a', _) = alter_init_lskips remove_init_ws a in
+          (Nfmap.insert subst (Name.strip_lskip p.term, Sub(a')), x, y)
 
-let inline_exp l (target : Target.target) env was_infix params body tsubst (args : exp list) =
+let inline_exp l (target : Target.target) env was_infix params body_sk body tsubst (args : exp list) =
   let module C = Exps_in_context(struct let env_opt = Some env;; let avoid = None end) in
   let loc = Ast.Trans(false, "inline_exp", Some l) in
   let (vsubst, leftover_params, leftover_args) = build_subst params args in
-  let b = C.exp_subst (tsubst,vsubst) body in
+
+  (* adapt whitespace before body *)
+  let b = cleanup_for_inline env body in
+  let b = (fst (alter_init_lskips (fun _ -> (body_sk, None)) b)) in
+  let b = C.exp_subst (tsubst,vsubst) b in
   let stays_infix = Precedence.is_infix (Precedence.get_prec_exp target env b) in
   if params = [] && was_infix && stays_infix then
   begin
           let cd = c_env_lookup l_unk env.c_env c_id.descr in
           let do_it (params, body) : exp =
             let tsubst = Types.TNfmap.from_list2 cd.const_tparams c_id.instantiation in
-   
-            (* adapt whitespace before body *)
-            let b = (fst (alter_init_lskips (fun _ -> (ident_get_lskip c_id, None)) body)) in
-            inline_exp l_unk target env was_infix params b tsubst args
+            inline_exp l_unk target env was_infix params (ident_get_lskip c_id) body tsubst args
           in
 
           let subst_opt = begin            
             
    match (params, C.exp_to_term b) with
      | ([], Constant c_id') -> Some (C.mk_pconst l_unk c_id' ps None)
-     | ([], Backend (sk, i)) -> 
+     | ([], Backend (_, sk, i)) -> 
           let ty = Types.type_subst tsubst cd.const_type in
-          Some (C.mk_pbackend l_unk sk i ty ps None)
+          Some (C.mk_pbackend l_unk true sk i ty ps None)
      | _ -> None
 
 
 
 let const_id_to_ident c_id ascii_alternative = snd (const_id_to_ident_aux c_id ascii_alternative None)
 
-let constant_application_to_output_simple is_infix_pos arg_f args c_id ascii_alternative given_id_opt = begin
+let constant_application_to_output_simple is_infix_pos arg_f alter_sk_f args c_id ascii_alternative given_id_opt = begin
   let (ascii_used, i) = const_id_to_ident_aux c_id ascii_alternative given_id_opt in 
   let const_is_infix = not (ascii_used) && Precedence.is_infix (Precedence.get_prec A.target A.env c_id.descr) in 
   let const_is_infix_input = Precedence.is_infix (Precedence.get_prec Target.Target_ident A.env c_id.descr) in
-(* old check: things might become prefix, but only original infix positions might become infix 
-  let is_infix = (is_infix_pos && const_is_infix && (Ident.has_empty_path_prefix i)) in *)
-
   let is_infix = (const_is_infix && (Ident.has_empty_path_prefix i) && (List.length args = 2) &&
                   (is_infix_pos || not const_is_infix_input)) in           
   let use_infix_notation = ((not is_infix) && const_is_infix) in
+
+  (* adapt whitespace *)
+  let (i, args) = if (is_infix && not is_infix_pos) || (not is_infix && is_infix_pos) then
+      begin (* print "f arg1 arg2" as "arg1 f arg2" or vise versa, so swap space of arg1 and f *)
+        match args with
+          | [arg1; arg2] -> 
+              let (arg1', arg1_sk) = alter_sk_f (fun sk -> (Ident.get_lskip i, sk)) arg1 in
+              let i' = Ident.replace_lskip i arg1_sk in
+              (i', [arg1'; arg2])
+          | _ -> (i, args)
+      end
+    else (i, args)
+  in
   let name = ident_to_output use_infix_notation i in
   let args_out = List.map (arg_f use_infix_notation) args in
+
   if (not is_infix) then
      (name :: args_out) 
   else 
             end
      | Some (CR_simple (_, _, params,body)) when not ascii_alternative -> begin
          let tsubst = Types.TNfmap.from_list2 c_descr.const_tparams c_id.instantiation in
-         let b = (fst (alter_init_lskips (fun _ -> (ident_get_lskip c_id, None)) body)) in
-         let new_exp = inline_exp l A.target A.env is_infix_pos params b tsubst args in
+         let new_exp = inline_exp l A.target A.env is_infix_pos params (ident_get_lskip c_id) body tsubst args in
          [arg_f true new_exp]
        end
-     | Some (CR_infix (_, _, _, _, i)) -> constant_application_to_output_simple is_infix_pos arg_f args c_id ascii_alternative (Some i)
+     | Some (CR_infix (_, _, _, i)) -> constant_application_to_output_simple is_infix_pos arg_f alter_init_lskips args c_id ascii_alternative (Some i)
      | Some (CR_undefined (l', _)) -> 
        begin 
          let (^) = Pervasives.(^) in
          raise (Reporting_basic.Fatal_error (Reporting_basic.Err_type (l, 
            (m0 ^ loc_s))))
        end
-     | _ -> constant_application_to_output_simple is_infix_pos arg_f args c_id ascii_alternative None
+     | _ -> constant_application_to_output_simple is_infix_pos arg_f alter_init_lskips args c_id ascii_alternative None
 
 let pattern_application_to_output l (arg_f0 : pat -> Output.t) (c_id : const_descr_ref id) (args : pat list) (ascii_alternative : bool) : Output.t list =
   let arg_f b p = if b then arg_f0 (Pattern_syntax.mk_opt_paren_pat p) else arg_f0 p in
          raise (Reporting_basic.Fatal_error (Reporting_basic.Err_type (l, 
            (m0 ^ loc_s))))
        end
-     | _ -> constant_application_to_output_simple false arg_f args c_id ascii_alternative None
+     | _ -> constant_application_to_output_simple false arg_f pat_alter_init_lskips args c_id ascii_alternative None
 
 let type_path_to_name n0 (p : Path.t) : Name.lskips_t =
   let l = Ast.Trans (false, "type_path_to_name", None) in

File src/coq_backend.ml

         match C.exp_to_term e with
           | Var v ->
               Name.to_output Term_var v
-          | Backend (sk, i) ->
+          | Backend (_, sk, i) ->
               ws sk ^
               Ident.to_output Term_const path_sep i
           | Lit l -> literal l
         | P_const(cd, ps) ->
             let oL = B.pattern_application_to_output p.locn fun_pattern cd ps (use_ascii_rep_for_const cd.descr) in
             concat emp oL
-        | P_backend(sk, i, _, ps) ->
+        | P_backend(_, sk, i, _, ps) ->
             ws sk ^
             Ident.to_output Term_const path_sep i ^
             concat texspace (List.map fun_pattern ps)
         | P_const(cd, ps) ->
             let oL = B.pattern_application_to_output p.locn def_pattern cd ps (use_ascii_rep_for_const cd.descr) in
             concat emp oL
-        | P_backend(sk, i, _, ps) ->
+        | P_backend(_, sk, i, _, ps) ->
             ws sk ^
             Ident.to_output Term_const path_sep i ^
             concat texspace (List.map def_pattern ps)

File src/lexer.mll

      ("MEM",                     (fun x -> MEM(x,r"MEM")));
      ("declare",                 (fun x -> Declare(x)));
      ("infix",                   (fun x -> Infix(x)));
-     ("infix_swap",              (fun x -> Infix_swap(x)));
-     ("undefined",               (fun x -> Undefined(x)));
      ("field"),                  (fun x -> Field(x));
      ("automatic"),              (fun x -> Automatic(x));
      ("manual"),                 (fun x -> Manual(x));

File src/macro_expander.ml

                   c 
                   (List.map (fun p -> (trans p)) ps)
                   (Some new_t)
-            | P_backend(sk,i,ty,ps) -> 
-                C.mk_pbackend old_l sk i
+            | P_backend(b,sk,i,ty,ps) -> 
+                C.mk_pbackend old_l b sk i
                   (typ_r ty)
                   (List.map (fun p -> (trans p)) ps)
                   (Some new_t)
                   C.mk_const old_l c (Some new_t)
               | Var(n) ->
                   C.mk_var old_l n new_t
-              | Backend(sk, i) ->
-                  C.mk_backend old_l sk i new_t
+              | Backend(b, sk, i) ->
+                  C.mk_backend old_l b sk i new_t
               | Nvar_e(s,n) -> C.mk_nvar_e old_l s n new_t
               | Lit li  ->
                   C.mk_lit old_l  {li with typ = new_t} (Some new_t)

File src/parser.mly

 %token <Ast.terminal> Class_ Do LeftArrow
 %token <Ast.terminal> Inst Inst_default
 %token <Ast.terminal> Module CompileMessage Field Type Automatic Manual Exhaustive Inexhaustive AsciiRep SetFlag TerminationArgument PatternMatch
-%token <Ast.terminal> RightAssoc LeftAssoc NonAssoc Infix Infix_swap Undefined Special TargetRep
+%token <Ast.terminal> RightAssoc LeftAssoc NonAssoc Infix Special TargetRep
 
 %start file
 %type <Ast.defs> defs
     { Fixity_default_assoc }
 
 target_rep_rhs_term :
+  | 
+    { Target_rep_rhs_undefined }
   | Infix fixity_decl BacktickString 
     { Target_rep_rhs_infix($1, $2, fst $3, snd $3) }
-  | Infix_swap fixity_decl BacktickString 
-    { Target_rep_rhs_infix_swap($1, $2, fst $3, snd $3) }
   | exp
     { Target_rep_rhs_term_replacement($1) }
   | Special String exps
     { Target_rep_rhs_special($1, fst $2, snd $2, $3) }
-  | Undefined
-    { Target_rep_rhs_undefined($1) }
 
 target_rep_rhs_type :
   | typ

File src/pattern_syntax.ml

       | P_tup _ -> false
       | P_lit _ -> false
       | P_const (_, pL) -> not (pL = [])
+      | P_backend (_, _, _, _, pL) -> not (pL = [])
       | _ -> true
   in 
   if (needs_parens) then 
     | P_typ (_,p,_,_,_) -> [p] 
     | P_paren(_,p,_) -> [p]
     | P_const(_,ps) -> ps
-    | P_backend(_,_,_,ps) -> ps
+    | P_backend(_,_,_,_,ps) -> ps
     | P_as (_, p, _, _, _) -> [p]
     | P_cons(p1,_,p2) -> [p1;p2]
     | P_tup(_,ps,_) -> Seplist.to_list ps
           (fun e p -> C.mk_app l_unk e (pat_to_exp env p) None)
           (C.mk_const p.locn c None)
           ps
-    | P_backend(sk,i,ty,ps) ->
+    | P_backend(b,sk,i,ty,ps) ->
         List.fold_left
           (fun e p -> C.mk_app l_unk e (pat_to_exp env p) None)
-          (C.mk_backend p.locn sk i ty)
+          (C.mk_backend p.locn b sk i ty)
           ps
     | P_record(_,fieldpats,_) ->
         raise (Pat_to_exp_unsupported(p.locn, "record pattern"))

File src/patterns.ml

         | P_as (s1,p,s2,(n,l),s3) -> ([], (fun pL -> C.mk_pas l s1 (List.hd pL) s2 (n, l) s3 (Some p_ty)), [Name.strip_lskip n])
         | P_typ (s1,p,s2,src_t,s3) -> ([p], (fun pL -> C.mk_ptyp l s1 (List.hd pL) s2 src_t s3 (Some p_ty)), [])
         | P_const (id, pL) -> (pL, (fun pL' -> C.mk_pconst l id pL' (Some p_ty)), [])
-        | P_backend (sk, i, ty, pL) -> (pL, (fun pL' -> C.mk_pbackend l sk i ty pL' (Some p_ty)), [])
+        | P_backend (b,sk, i, ty, pL) -> (pL, (fun pL' -> C.mk_pbackend l b sk i ty pL' (Some p_ty)), [])
         | P_tup (s1,ps,s2) -> (Seplist.to_list ps, (fun pL -> C.mk_ptup l' s1 (Seplist.from_list_default None pL) s2 (Some p_ty)), [])
         | P_list (s1,ps,s2) -> (Seplist.to_list ps, (fun pL -> C.mk_plist l' s1 (Seplist.from_list_default None pL) s2 p_ty), [])
         | P_paren (s1, p, s2) -> ([p], (fun pL -> C.mk_pparen l s1 (List.hd pL) s2 (Some p_ty)), [])

File src/precedence.ml

   | P_infix_left i -> i
   | P_infix_right i -> i
   
-let ast_fixity_decl_to_t swap = function
- | Ast.Fixity_right_assoc   (_, i) -> if swap then P_infix_left i else P_infix_right i
- | Ast.Fixity_left_assoc    (_, i) -> if swap then P_infix_right i else P_infix_left i
+let ast_fixity_decl_to_t = function
+ | Ast.Fixity_right_assoc   (_, i) -> P_infix_right i
+ | Ast.Fixity_left_assoc    (_, i) -> P_infix_left i
  | Ast.Fixity_non_assoc     (_, i) -> P_infix i
  | Ast.Fixity_default_assoc        -> P_infix 0
 
     | Target.Target_no_ident targ' -> (* precedences for real targets are stored in the constant description *)
       begin
         match Target.Targetmap.apply c_descr.target_rep targ' with
-         | Some (CR_infix (_, _, swap, fixity, _)) -> ast_fixity_decl_to_t swap fixity
+         | Some (CR_infix (_, _, fixity, _)) -> ast_fixity_decl_to_t fixity
          | Some (CR_special _) -> P_special (* TODO: Thomas T.: uncertain, whether P_prefix would be better here, but it should not matter much I hope *)
          | Some (CR_inline (_, _, [], e)) -> get_prec_exp targ env e
          | Some (CR_simple (_, _, [], e)) -> get_prec_exp targ env e

File src/seplist.ml

       (None,l,e)
   | _ -> raise (Failure "Seplist.tl_sep")
 
+let replace_all_seps ns (so, l, e) = 
+  (Util.option_map ns so, List.map (fun (x, s) -> (x, ns s)) l, e)
+
 let append d l1 l2 = match (l1, l2) with
   | ((o11, l1, None), (_, l2, o22)) ->
     (o11, l1 @ l2, o22)

File src/seplist.mli

 
 val pp : (Format.formatter -> 'a -> unit) -> (Format.formatter -> 'b -> unit) -> Format.formatter -> ('a,'b) t -> unit
                                                                            
+val replace_all_seps : ('s -> 's) -> ('a, 's) t -> ('a, 's) t

File src/target_syntax.ml

     | _ -> assert false
 
 let delimit_exp get_prec (c : P.context) (e : exp) : exp =
-  let k = match C.exp_to_term e with
-    | App _ -> P.App
+  let rec get_context e = match C.exp_to_term e with
+    | App (e2, e3) -> if Typed_ast_syntax.is_empty_backend_exp e2 then get_context e3 else P.App
     | Infix(_,e2,_) -> P.Infix(exp_to_prec get_prec e2)
     | Fun _ | Let _ | If _ | Quant _ -> P.Let
     | _ -> P.Atomic
   in
-    if P.needs_parens c k then Typed_ast_syntax.mk_paren_exp e else e
+    if P.needs_parens c (get_context e) then Typed_ast_syntax.mk_paren_exp e else e
 
 let delimit_pat (c : P.pat_context) (p : pat) : pat =
   let k = match p.term with
                   (fun p -> delimit_pat P.Plist (trans p)) 
                   ps)
                old_t)
-      | P_backend(sk,i,ty,ps) -> 
-            (C.mk_pbackend old_l sk i ty 
+      | P_backend(b,sk,i,ty,ps) -> 
+            (C.mk_pbackend old_l b sk i ty 
                (List.map 
                   (fun p -> delimit_pat P.Plist (trans p)) 
                   ps)
           C.mk_const old_l c old_t
       | Var(n) ->
           C.mk_var old_l n (exp_to_typ e) 
-      | Backend(sk,i) ->
-          C.mk_backend old_l sk i (exp_to_typ e) 
+      | Backend(b,sk,i) ->
+          C.mk_backend old_l b sk i (exp_to_typ e) 
       | Lit _  | Nvar_e _ ->
           e
 

File src/typecheck.ml

               exp
         | Ast.Backend(sk,s) ->
             let id = check_backend_quote l s in
-              A.mk_backend l sk id ret_type
+              A.mk_backend l false sk id ret_type
         | Ast.Nvar((sk,n)) -> 
             let nv = Nvar.from_rope(n) in
             C.add_nvar nv;
        let _ = if (List.length args = 0) then () else
                  raise (Reporting_basic.err_type l "infix target declaration with arguments") in
        let i = check_backend_quote l id in
-       (Target_rep_rhs_infix (sk1, false, infix_decl, sk2, i), CR_infix(l, false, false, infix_decl, i))
-   | Ast.Target_rep_rhs_infix_swap (sk1, infix_decl, sk2, id) ->
-       let _ = if (List.length args = 0) then () else
-                 raise (Reporting_basic.err_type l "infix target declaration with arguments") in
-       let i = check_backend_quote l id in
-       (Target_rep_rhs_infix (sk1, true, infix_decl, sk2, i), CR_infix(l, false, true, infix_decl, i))
-   | Ast.Target_rep_rhs_undefined sk ->
-       (Target_rep_rhs_undefined sk, CR_undefined (l, false))
+       (Target_rep_rhs_infix (sk1, infix_decl, sk2, i), CR_infix(l, false, infix_decl, i))
+   | Ast.Target_rep_rhs_undefined ->
+       (Target_rep_rhs_undefined, CR_undefined (l, false))
    | Ast.Target_rep_rhs_special (sk1, sk2, sp, args) ->
        raise (Reporting_basic.err_todo true l "unsupported rhs of term target special representation declaration") in
   let (ctxt', _) = ctxt_c_env_set_target_rep l ctxt c targ new_rep in

File src/typed_ast.ml

   | P_typ of lskips * pat * lskips * src_t * lskips
   | P_var of Name.lskips_t
   | P_const of const_descr_ref id * pat list
-  | P_backend of lskips * Ident.t * Types.t * pat list
+  | P_backend of bool * lskips * Ident.t * Types.t * pat list
   | P_record of lskips * (const_descr_ref id * lskips * pat) lskips_seplist * lskips
   | P_vector of lskips * pat lskips_seplist * lskips
   | P_vectorC of lskips * pat list * lskips
 
 and const_target_rep =
   | CR_inline of Ast.l * bool * name_lskips_annot list * exp
-  | CR_infix of Ast.l * bool * bool * Ast.fixity_decl * Ident.t
+  | CR_infix of Ast.l * bool * Ast.fixity_decl * Ident.t
   | CR_undefined of Ast.l * bool 
   | CR_simple of Ast.l * bool * name_lskips_annot list * exp
   | CR_special of Ast.l * bool * cr_special_fun * Name.t list
 
 and exp_aux =
   | Var of Name.lskips_t
-  | Backend of lskips * Ident.t
+  | Backend of bool * lskips * Ident.t
   | Nvar_e of lskips * Nvar.t
   | Constant of const_descr_ref id
   | Fun of lskips * pat list * lskips * exp
 
 type 
 target_rep_rhs =  (* right hand side of a target representation declaration *)
-   Target_rep_rhs_infix of lskips * bool * Ast.fixity_decl * lskips * Ident.t
+   Target_rep_rhs_infix of lskips * Ast.fixity_decl * lskips * Ident.t
  | Target_rep_rhs_term_replacement of exp
  | Target_rep_rhs_type_replacement of src_t
  | Target_rep_rhs_special of lskips * lskips * string * exp list
- | Target_rep_rhs_undefined of lskips 
+ | Target_rep_rhs_undefined  
 
 
 type declare_def =  (* declarations *)
       | P_const(c,ps) -> 
           let (id_new, s_ret) = id_alter_init_lskips lskips_f c in
             res (P_const(id_new,ps)) s_ret
-      | P_backend(sk,i,ty,ps) -> 
+      | P_backend(b,sk,i,ty,ps) -> 
           let (s_new, s_ret) = lskips_f sk in
-            res (P_backend(s_new, i, ty, ps)) s_ret
+            res (P_backend(b, s_new, i, ty, ps)) s_ret
       | P_record(s1,fieldpats,s2) -> 
           let (s_new, s_ret) = lskips_f s1 in
             res (P_record(s_new, fieldpats, s2)) s_ret
       | Var(n) ->
           let (s_new, s_ret) = lskips_f (Name.get_lskip n) in
             res (Var(Name.replace_lskip n s_new)) s_ret
-      | Backend(sk, i) ->
+      | Backend(b, sk, i) ->
           let (s_new, s_ret) = lskips_f sk in
-            res (Backend(s_new, i)) s_ret
+            res (Backend(b, s_new, i)) s_ret
       | Nvar_e(s,n) ->
           let (s_new, s_ret) = lskips_f s in
             res (Nvar_e(s_new,n)) s_ret 
       typ = t;
       rest = { pvars = merge_free_env true l (List.map (fun p -> p.rest.pvars) ps); }; }
 
-  let mk_pbackend l sk i ty ps t =
+  let mk_pbackend l b sk i ty ps t =
     (* only perform checks, if environment is provided *)
     let c_base_ty_opt = Util.option_map (fun env -> begin
       let new_c_ty = ty in
     let t = 
       check_typ l "mk_pconst" t (fun d -> c_base_ty_opt)
     in
-    { term = P_backend(sk,i,ty,ps);
+    { term = P_backend(b,sk,i,ty,ps);
       locn = l;
       typ = t;
       rest = { pvars = merge_free_env true l (List.map (fun p -> p.rest.pvars) ps); }; }
                 List.map (type_subst tsubst) c.instantiation }
           in
             mk_pconst l c (List.map (pat_subst sub) ps) (Some new_typ)
-      | P_backend(sk,i,ty,ps) -> 
-          mk_pbackend l sk i (type_subst tsubst ty) (List.map (pat_subst sub) ps) (Some new_typ)
+      | P_backend(b,sk,i,ty,ps) -> 
+          mk_pbackend l b sk i (type_subst tsubst ty) (List.map (pat_subst sub) ps) (Some new_typ)
       | P_record(s1,fieldpats,s2) ->
           mk_precord l
             s1 
                 | Some(Sub(e')) -> 
                     exp_to_term (append_lskips (Name.get_lskip n) e')
             end
-        | Backend (s,i) -> Backend (s,i)
+        | Backend (b,s,i) -> Backend (b,s,i)
         | Nvar_e(s,v) -> Nvar_e(s,v)
         | Constant(c) -> 
             Constant(id_subst c)
         { free = sing_free_env (Name.strip_lskip n) t;
           subst = empty_sub; } }
 
-  let mk_backend l sk i t : exp =
-    { term = Backend(sk, i);
+  let mk_backend l b sk i t : exp =
+    { term = Backend(b, sk, i);
       locn = l;
       typ = t;
       rest =

File src/typed_ast.mli

   | P_typ of lskips * pat * lskips * src_t * lskips
   | P_var of Name.lskips_t
   | P_const of const_descr_ref id * pat list
-  | P_backend of lskips * Ident.t * Types.t * pat list
+  | P_backend of bool * lskips * Ident.t * Types.t * pat list
   | P_record of lskips * (const_descr_ref id * lskips * pat) lskips_seplist * lskips
   | P_vector of lskips * pat lskips_seplist * lskips
   | P_vectorC of lskips * pat list * lskips
         replacing the variable [vars] inside [e] with the arguments of the constant. The flag [allow_override] signals whether
         the declaration might be safely overriden. Automatically generated target-representations (e.g. for ocaml constructors) should
         be changeable by the user, whereas multiple user-defined ones should cause a type error. *)
-  | CR_infix of Ast.l * bool * bool * Ast.fixity_decl * Ident.t
-    (** [CR_infix (loc, allow_override, do_swap, fixity, i)] declares infix notation for the constant with the giving identifier. *)
+  | CR_infix of Ast.l * bool * Ast.fixity_decl * Ident.t
+    (** [CR_infix (loc, allow_override, fixity, i)] declares infix notation for the constant with the giving identifier. *)
   | CR_undefined of Ast.l * bool 
     (** [CR_undefined (loc, allow_override)] declares undefined constant. *)
   | CR_simple of Ast.l * bool * name_lskips_annot list * exp
 
 and exp_aux = private
   | Var of Name.lskips_t
-  | Backend of lskips * Ident.t (** An identifier that should be used literally by a backend. The identifier does not contain whitespace. Initial whitespace is represented explicitly. *)
+  | Backend of bool * lskips * Ident.t (** An identifier that should be used literally by a backend. The identifier does not contain whitespace. Initial whitespace is represented explicitly. *)
   | Nvar_e of lskips * Nvar.t
   | Constant of const_descr_ref id
   | Fun of lskips * pat list * lskips * exp
                              (indreln_indfn list) option * lskips
 
 type target_rep_rhs =  (** right hand side of a target representation declaration *)
-   Target_rep_rhs_infix of lskips * bool * Ast.fixity_decl * lskips * Ident.t (** Declaration of an infix constant *)
+   Target_rep_rhs_infix of lskips * Ast.fixity_decl * lskips * Ident.t (** Declaration of an infix constant *)
  | Target_rep_rhs_term_replacement of exp (** the standard term replacement, replace with the exp for the given backend *)
  | Target_rep_rhs_type_replacement of src_t (** the standard term replacement, replace with the type for the given backend *)
  | Target_rep_rhs_special of lskips * lskips * string * exp list (** fancy represenation of terms *)
- | Target_rep_rhs_undefined of lskips (** undefined, don't throw a problem during typeching, but during output *)
+ | Target_rep_rhs_undefined (** undefined, don't throw a problem during typeching, but during output *)
 
 type declare_def =  (** Declarations *)
  | Decl_compile_message of lskips * targets_opt * lskips * const_descr_ref id * lskips * lskips * string 
   val mk_ptyp : Ast.l -> lskips -> pat -> lskips -> src_t -> lskips -> Types.t option -> pat
   val mk_pvar : Ast.l -> Name.lskips_t -> Types.t -> pat
   val mk_pconst : Ast.l -> const_descr_ref id -> pat list -> Types.t option -> pat
-  val mk_pbackend : Ast.l -> lskips -> Ident.t -> Types.t -> pat list -> Types.t option -> pat
+  val mk_pbackend : Ast.l -> bool -> lskips -> Ident.t -> Types.t -> pat list -> Types.t option -> pat
   val mk_precord : Ast.l -> lskips -> (const_descr_ref id * lskips * pat) lskips_seplist -> lskips -> Types.t option -> pat
   val mk_ptup : Ast.l -> lskips -> pat lskips_seplist -> lskips -> Types.t option -> pat
   val mk_plist : Ast.l -> lskips -> pat lskips_seplist -> lskips -> Types.t -> pat
 
   val mk_var : Ast.l -> Name.lskips_t -> Types.t -> exp
   val mk_nvar_e : Ast.l -> lskips -> Nvar.t -> Types.t -> exp
-  val mk_backend : Ast.l -> lskips -> Ident.t -> Types.t -> exp
+  val mk_backend : Ast.l -> bool -> lskips -> Ident.t -> Types.t -> exp
   val mk_const : Ast.l -> const_descr_ref id -> Types.t option -> exp
   val mk_fun : Ast.l -> lskips -> pat list -> lskips -> exp -> Types.t option -> exp
   val mk_function : Ast.l -> lskips -> (pat * lskips * exp * Ast.l) lskips_seplist -> lskips -> Types.t option -> exp

File src/typed_ast_syntax.ml

 
 let const_target_rep_to_loc= function
   | CR_inline (l, _, _, _) -> l
-  | CR_infix (l, _, _, _, _) -> l
+  | CR_infix (l, _, _, _) -> l
   | CR_simple (l, _, _, _) -> l
   | CR_special (l, _, _, _) -> l
   | CR_undefined (l, _) -> l
 
 let const_target_rep_allow_override = function
   | CR_inline (_, f, _, _) -> f
-  | CR_infix (_, f, _, _, _) -> f
+  | CR_infix (_, f, _, _) -> f
   | CR_simple (_, f, _, _) -> f
   | CR_special (_, f, _, _) -> f
   | CR_undefined (_, f) -> f
      let (e', ws) = alter_init_lskips remove_init_ws e in
      C.mk_paren (exp_to_locn e) ws e' None (Some (exp_to_typ e))
 
-let mk_opt_paren_exp (e :exp) : exp =
+
+let is_empty_backend_exp e =
+  match C.exp_to_term e with
+   | Backend(_,_,i) -> (Ident.to_string i = "") 
+   | _ -> false
+
+
+let rec mk_opt_paren_exp (e :exp) : exp = 
   match C.exp_to_term e with
     | Var _ -> e
     | Constant _ -> e
+    | Backend _ -> e
     | Tup _ -> e
     | Paren _ -> e
     | Lit _ -> e
-    | _ -> mk_paren_exp e
+    | App (e1, e2) -> 
+      if is_empty_backend_exp e1 then
+        C.mk_app (exp_to_locn e) e1 (mk_opt_paren_exp e2) (Some (exp_to_typ e)) 
+      else
+        mk_paren_exp e
+    | _ -> mk_paren_exp e 
 
 
 let dest_const_exp (e : exp) : const_descr_ref id option =
     | P_const(c,ps) -> 
         let ue = used_entities_add_const ue c.descr in
         List.fold_left add_pat_entities ue ps
-    | P_backend(_,_,_,ps) -> 
+    | P_backend(_,_,_,_,ps) -> 
         List.fold_left add_pat_entities ue ps
     | P_record(_,fieldpats,_) -> Seplist.fold_left (fun (id, _, p) ue -> 
          add_pat_entities (used_entities_add_const ue id.descr)  p) ue fieldpats

File src/typed_ast_syntax.mli

 (** [mk_num_exp] creates a number literal expression. *)
 val mk_num_exp : int -> exp
 
+(** [is_empty_backend_exp] checks whether the expression is [``] *)
+val is_empty_backend_exp : exp -> bool
+
 (** [mk_eq_exp env e1 e2] constructs the expression [e1 = e2]. The environment [env] is needed
     to lookup the equality constant. *)
 val mk_eq_exp : env -> exp -> exp -> exp