anchor.diff:  
   let filter_imp a = a |> List.filter (function (_, Some (S.Implicit _)) -> false | _ -> true)
   
  -let resugar_arg_qual (q:option<S.arg_qualifier>) : option<A.arg_qualifier> =
  +(* If resugar_arg_qual returns None, the corresponding binder should *not* be resugared *)
  +let resugar_arg_qual (q:option<S.arg_qualifier>) : option<(option<A.arg_qualifier>)> =
     match q with
  -    | None -> None
  -    | Some (S.Implicit b) -> Some A.Implicit  //TODO: how should we map this flag back to the surface?
  -    | Some S.Equality -> Some A.Equality
  +  | None -> Some None
  +  | Some (S.Implicit b) ->
  +    (* TODO : set an option to print these inaccessible patterns *)
  +    if b then None
  +    else Some (Some A.Implicit)
  +  | Some S.Equality -> Some (Some A.Equality)
   
   let rec universe_to_int n u =
     match u with
  -    | U_succ u -> universe_to_int (n+1) u
  -    | _ -> (n, u)
  +  | U_succ u -> universe_to_int (n+1) u
  +  | _ -> (n, u)
   
   let rec resugar_universe (u:S.universe) r: A.term =
     let mk (a:A.term') r: A.term =
  -      //augment `a` an Unknown level (the level is unimportant ... we should maybe remove it altogether)
  -      A.mk_term a r A.Un
  +    //augment `a` an Unknown level (the level is unimportant ... we should maybe remove it altogether)
  +    A.mk_term a r A.Un
     in
     begin match u with
       | U_zero ->
  
positive.code: module D = FStar.Parser.ToDocument
  
  let bv_as_unique_ident (x:S.bv) : I.ident =
    let unique_name =  
      if starts_with reserved_prefix x.ppname.idText then
        x.ppname.idText ^ (string_of_int x.index)
      else
  
negative.code:       else None
    in
    match (SS.compress t).n with
    | Tm_fvar fv ->
      let length = String.length(fv.fv_name.v.nsstr) in
      let s = if length=0 then fv.fv_name.v.str
              else BU.substring_from fv.fv_name.v.str (length+1) in
      begin match string_to_op s with
        | Some t -> Some t
        | _ -> fallback fv
      end
    | Tm_uinst(e, us) -> resugar_term_as_op e
    | _ -> None
  
  let is_true_pat (p:S.pat) : bool = match p.v with
    | Pat_constant (Const_bool true) -> true
    | _ -> false
  
  let is_wild_pat (p:S.pat) : bool = match p.v with
    | Pat_wild _ -> true
    | _ -> false
  
  let rec resugar_term (t : S.term) : A.term =
    (* Cannot resugar term back to NamedTyp or Paren *)
    let mk (a:A.term') : A.term =
      //augment `a` with its source position
      //and an Unknown level (the level is unimportant ... we should maybe remove it altogether)
      A.mk_term a t.pos A.Un
    in
    let name a r =
      // make a Name term'
      A.Name (lid_of_path [a] r)
    in
    let var a r =
      // make a Var term'
      A.Var (lid_of_path [a] r)
    in
    match (SS.compress t).n with //always call compress before case-analyzing a S.term
    | Tm_delayed _ ->
      failwith "Tm_delayed is impossible after compress"
  
    | Tm_bvar x ->
      (* this case can happen when printing a subterm of a term that is not opened *)
      let l = FStar.Ident.lid_of_ids [bv_as_unique_ident x] in
      mk (A.Var l)
  
    | Tm_name x -> //a lower-case identifier
      //this is is too simplistic
      //the resulting unique_name is very ugly
      //it would be better to try to use x.ppname alone, unless the suffix is deemed semantically necessary
      let l = FStar.Ident.lid_of_ids [bv_as_unique_ident x] in
      mk (A.Var l)
  
    | Tm_fvar fv -> //a top-level identifier, may be lowercase or upper case
      //should be A.Var if lowercase
      //and A.Name if uppercase
      let a = fv.fv_name.v in
      let length = String.length(fv.fv_name.v.nsstr) in
      let s = if length=0 then a.str
          else BU.substring_from a.str (length+1) in
      let is_prefix = I.reserved_prefix ^ "is_" in
      if BU.starts_with s is_prefix then
        let rest = BU.substring_from s (String.length is_prefix) in
        mk (A.Discrim(lid_of_path [rest] t.pos))
      else if BU.starts_with s U.field_projector_prefix then
        let rest = BU.substring_from s (String.length U.field_projector_prefix) in
        let r = BU.split rest U.field_projector_sep in
        begin match r with
          | [fst; snd] ->
            let l = lid_of_path [fst] t.pos in
            let r = I.mk_ident (snd, t.pos) in
            mk (A.Projector(l, r ))
          | _ ->
            failwith "wrong projector format"
        end
        else if (lid_equals a C.assert_lid
            || lid_equals a C.assume_lid
            || Char.uppercase (String.get s 0) <> String.get s 0) then
              mk (var s t.pos)
          else
              mk (name s t.pos)
    | Tm_uinst(e, universes) ->
      if (Options.print_universes()) then
        let e = resugar_term e in
        List.fold_left(fun acc x -> mk (A.App(acc, resugar_universe x t.pos, A.UnivApp))) e universes
      else
        resugar_term e
  
    | Tm_constant c ->
      if is_teff t
      then mk (name "Effect" t.pos)
      else mk (A.Const c)
  
    | Tm_type u ->
        begin match u with
        | U_zero ->  mk (name "Type0" t.pos)
        | U_unknown -> mk (name "Type" t.pos)
        | _ ->
          if (Options.print_universes()) then
            let u = resugar_universe u t.pos in
            let l = lid_of_path ["Type"] t.pos in
            mk (A.Construct (l, [(u, UnivApp)]))
          else
            mk (name "Type" t.pos)
        end
  
    | Tm_abs(xs, body, _) -> //fun x1 .. xn -> body
      //before inspecting any syntactic form that has binding structure
      //you must call SS.open_* to replace de Bruijn indexes with names
      let xs, body = SS.open_term xs body in
      let xs = if (Options.print_implicits()) then xs else filter_imp xs in
      let patterns = xs |> List.choose (fun (x, qual) ->
        //x.sort contains a type annotation for the bound variable
        //the pattern `p` below only contains the variable, not the annotation
        //but, if the user wrote the annotation, then we should record that and print it back
        //additionally, if we're in verbose mode, e.g., if --print_bound_var_types is set
        //    then we should print the annotation too
        resugar_bv_as_pat x qual)
      in
      let body = resugar_term body in
      mk (A.Abs(patterns, body))
  
    | Tm_arrow(xs, body) ->
      let xs, body = SS.open_comp xs body in
      let xs = if (Options.print_implicits()) then xs else filter_imp xs in
      let body = resugar_comp body in
      let xs = xs |> List.map (fun (b, qual) -> resugar_bv_as_binder b t.pos) |> List.rev in
      let rec aux body = function
        | [] -> body
        | hd::tl ->
          let body = mk (A.Product([hd], body)) in
          aux body tl in
      aux body xs
  
    | Tm_refine(x, phi) ->
      (* bv * term -> binder * term *)
      let x, phi = SS.open_term [S.mk_binder x] phi in
      let (b, _) = List.hd x in
      let b = resugar_bv_as_binder b t.pos in
      mk (A.Refine(b, resugar_term phi))
  
    | Tm_app(e, args) ->
      (* Op("=!=", args) is desugared into Op("~", Op("==") and not resugared back as "=!=" *)
      let rec last = function
            | hd :: [] -> [hd]
            | hd :: tl -> last tl
            | _ -> failwith "last of an empty list"
      in
      let rec last_two = function
            | [] | [_] -> failwith "last two elements of a list with less than two elements "
            | [a1;a2] -> [a1;a2]
            | _::t -> last_two t
      in
      let rec last_three = function
            | [] | [_] | [_;_] -> failwith "last three elements of a list with less than three elements "
            | [a1;a2;a3] -> [a1;a2;a3]
            | _::t -> last_three t
      in
      let resugar_as_app e args =
        let args = args |> List.map (fun (e, qual) ->
              resugar_term e) in
        let e = resugar_term e in
        List.fold_left(fun acc x -> mk (A.App(acc, x, A.Nothing))) e args
      in
      let args = if (Options.print_implicits()) then args else filter_imp args
      in
      begin match resugar_term_as_op e with
        | None->
          resugar_as_app e args
  
        | Some "tuple" ->
          begin match args with
            | (fst, _)::(snd, _)::rest ->
              let e = mk(A.Op(Ident.id_of_text "*", [(resugar_term fst); (resugar_term snd)])) in
              List.fold_left(fun acc (x,_) -> mk (A.Op(Ident.id_of_text "*", [e; resugar_term x]))) e rest
            | _ -> resugar_as_app e args
          end
  
        | Some "dtuple" when List.length args > 0 ->
          (* this is desugared from Sum(binders*term) *)
          let args = last args in
          let body = match args with
            | [(b, _)] -> b
            | _ -> failwith "wrong arguments to dtuple"
          in
          begin match (SS.compress body).n with
            | Tm_abs(xs, body, _) ->
                let xs, body = SS.open_term xs body in
                let xs = if (Options.print_implicits()) then xs else filter_imp xs in
                let xs = xs |> List.map (fun (b, qual) -> resugar_bv_as_binder b t.pos) in
                let body = resugar_term body in
                mk (A.Sum(xs, body))
  
            | _ ->
              let args = args |> List.map (fun (e, qual) ->
                resugar_term e) in
              let e = resugar_term e in
              List.fold_left(fun acc x -> mk (A.App(acc, x, A.Nothing))) e args
          end
  
        | Some "dtuple" ->
          resugar_as_app e args
  
        | Some ref_read when (ref_read = C.sread_lid.str) ->
          let (t, _) = List.hd args in
          begin match (SS.compress t).n with
            | Tm_fvar fv when (U.field_projector_contains_constructor fv.fv_name.v.str) ->
              let f = lid_of_path [fv.fv_name.v.str] t.pos in
              mk (A.Project(resugar_term t, f))
            | _ -> resugar_term t
          end
  
        | Some "try_with" when List.length args > 1 ->
          (* only the last two args are from original AST terms, others are added by typechecker *)
          (* TODO: we need a place to store the information in the args added by the typechecker *)
          let new_args = last_two args in
          let body, handler = match new_args with
            | [(a1, _);(a2, _)] -> a1, a2 (* where a1 and a1 is Tm_abs(Tm_match)) *)
            | _ ->
              failwith("wrong arguments to try_with")
          in
          let decomp term = match (SS.compress term).n with
            | Tm_abs(x, e, _) ->
              let x, e = SS.open_term x e in
              e
            | _ -> failwith("wrong argument format to try_with") in
          let body = resugar_term (decomp body) in
          let handler = resugar_term (decomp handler) in
          let rec resugar_body t = match (t.tm) with
            | A.Match(e, [(_,_,b)]) -> b
            | A.Ascribed(t1, t2, t3) ->
              (* this case happens when the match is wrapped in Meta_Monadic which is resugared to Ascribe*)
              mk (A.Ascribed(resugar_body t1, t2, t3))
            | _ -> failwith("unexpected body format to try_with") in
          let e = resugar_body body in
          let rec resugar_branches t = match (t.tm) with
            | A.Match(e, branches) -> branches
            | A.Ascribed(t1, t2, t3) ->
              (* this case happens when the match is wrapped in Meta_Monadic which is resugared to Ascribe*)
              (* TODO: where should we keep the information stored in Ascribed? *)
              resugar_branches t1
            | _ ->
              (* TODO: forall created by close_forall doesn't follow the normal forall format, not sure how to resugar back *)
              []
          in
          let branches = resugar_branches handler in
          mk (A.TryWith(e, branches))
  
        | Some "try_with" ->
          resugar_as_app e args
  
        | Some op when op = "forall" || op = "exists" ->
          (* desugared from QForall(binders * patterns * body) to Tm_app(forall, Tm_abs(binders, Tm_meta(body, meta_pattern(list<args>)*)
          let rec uncurry xs pat (t:A.term) = match t.tm with
            | A.QExists(x, p , body)
            | A.QForall(x, p, body)
              -> uncurry (x@xs) (p@pat) body
            | _ -> xs, pat, t
          in
          let resugar body = match (SS.compress body).n with
            | Tm_abs(xs, body, _) ->
                let xs, body = SS.open_term xs body in
                let xs = if (Options.print_implicits()) then xs else filter_imp xs in
                let xs = xs |> List.map (fun (b, qual) -> resugar_bv_as_binder b t.pos) in
                let pats, body = match (SS.compress body).n with
                  | Tm_meta(e, m) ->
                    let body = resugar_term e in
                    let resugar_pats pats = List.map (fun es -> es |> List.map (fun (e, _) -> resugar_term e)) pats in
                    let pats = match m with
                      | Meta_pattern pats -> resugar_pats pats
                      | Meta_labeled (s, r, _) ->
                        // this case can occur in typechecker when a failure is wrapped in meta_labeled
                        [[mk (name s r)]]
                      | _ -> failwith "wrong pattern format for QForall/QExists"
                    in
                    pats, body
                  | _ -> [], resugar_term body
                in
                let xs, pats, body = uncurry xs pats body in
                let xs = xs |> List.rev in
                if op = "forall" then mk (A.QForall(xs, pats, body)) else mk (A.QExists(xs, pats, body))
  
            | _ ->
            (*forall added by typechecker.normalize doesn't not have Tm_abs as body*)
            (*TODO:  should we resugar them back as forall/exists or just as the term of the body *)
            if op = "forall" then mk (A.QForall([], [[]], resugar_term body))
            else mk (A.QExists([], [[]], resugar_term body))
          in
          (* only the last arg is from original AST terms, others are added by typechecker *)
          (* TODO: we need a place to store the information in the args added by the typechecker *)
          if List.length args > 0 then
            let args = last args in
            begin match args with
              | [(b, _)] -> resugar b
              | _ -> failwith "wrong args format to QForall"
            end
          else
            resugar_as_app e args
  
        | Some "alloc" ->
          let (e, _ ) = List.hd args in
          resugar_term e
  
        | Some op ->
          let op = Ident.id_of_text op in
          let resugar args = args |> List.map (fun (e, qual) ->
              resugar_term e)
          in
          (* ignore the arguments added by typechecker *)
          (* TODO: we need a place to store the information in the args added by the typechecker *)
          (* KM : I don't think that '-' is resugared correctly here *)
          //NS: this seems to produce the wrong output on things like
          begin match D.handleable_args_length op with
            | 1 when List.length args > 0 -> mk (A.Op(op, resugar (last args)))
            | 2 when List.length args > 1 -> mk (A.Op(op, resugar (last_two args)))
            | 3 when List.length args > 2 -> mk (A.Op(op, resugar (last_three args)))
            | _ -> resugar_as_app e args
          end
    end
    | Tm_match(e, [(pat1, _, t1); (pat2, _, t2)]) when is_true_pat pat1 && is_wild_pat pat2 ->
      mk (A.If(resugar_term e, resugar_term t1, resugar_term t2))
  
    | Tm_match(e, branches) ->
      let resugar_branch (pat, wopt,b) =
        let pat = resugar_match_pat pat in
        let wopt = match wopt with
          | None -> None
          | Some e -> Some (resugar_term e) in
        let b = resugar_term b in
        (pat, wopt, b) in
        mk (A.Match(resugar_term e, List.map resugar_branch branches))
  
    | Tm_ascribed(e, (asc, tac_opt), _) ->
      let term = match asc with
          | Inl n -> (* term *)
            resugar_term n
          | Inr n -> (* comp *)
            resugar_comp n in
      let tac_opt = Option.map resugar_term tac_opt in
      mk (A.Ascribed(resugar_term e, term, tac_opt))
  
    | Tm_let((is_rec, bnds), body) ->
      let mk_pat a = A.mk_pattern a t.pos in
      let bnd, body = SS.open_let_rec bnds body in
      let resugar_one_binding bnd =
        let univs, td = SS.open_univ_vars bnd.lbunivs (U.mk_conj bnd.lbtyp bnd.lbdef) in
        let typ, def = match (SS.compress td).n with
          | Tm_app(_, [(t, _); (d, _)]) -> t, d
          | _ -> failwith "wrong let binding format"
        in
        let binders, term, is_pat_app = match (SS.compress def).n with
          | Tm_abs(b, t, _) ->
            let b, t = SS.open_term b t in
            let b = if (Options.print_implicits()) then b else filter_imp b in
            b, t, true
          | _ -> [], def, false
        in
        let universe_to_string univs =
          if (Options.print_universes()) then
            List.map (fun x -> x.idText) univs |> String.concat  ", "
          else ""
        in
        let pat, term = match bnd.lbname with
          | Inr fv -> mk_pat (A.PatName fv.fv_name.v), term
          | Inl bv ->
            let x, term = SS.open_term [S.mk_binder bv] term in
            let (bv, _) = List.hd x in
            mk_pat (A.PatVar (bv_as_unique_ident bv, None)), term
        in
        if is_pat_app then
          let args = binders |> List.map (fun (bv, _) -> mk_pat(A.PatVar (bv_as_unique_ident bv, None))) in
          ((mk_pat (A.PatApp (pat, args)), resugar_term term), (universe_to_string univs))
        else
          ((pat, resugar_term term), (universe_to_string univs))
      in
      let r = List.map (resugar_one_binding) bnds in
      let bnds = List.map fst r in
      let comments = List.map snd r in
      let body = resugar_term body in
      mk (A.Let((if is_rec then A.Rec else A.NoLetQualifier), bnds, body))
  
    | Tm_uvar (u, _) ->
      let s = "uu___unification_ " ^ (FStar.Unionfind.uvar_id u |> string_of_int) in
      mk (var s t.pos)
  
    | Tm_meta(e, m) ->
        let resugar_meta_desugared = function
          | Data_app ->
              begin match (SS.compress e).n with
                | Tm_app(head, args) ->
                    let rec aux h = match ((SS.compress h).n) with
                      | Tm_fvar fv -> lid_of_fv fv, []
                      | Tm_uinst(h, u) ->
                        let h, l = aux h in
                        h, l@u
                      | _ -> failwith "wrong Data_app head format"
                    in
                    let head, universes = aux head in
                    let universes = List.map (fun u -> (resugar_universe u t.pos, A.UnivApp)) universes in
                    let args = List.map (fun (t, _) -> (resugar_term t, A.Nothing)) args in
                    if (U.is_tuple_data_lid' head) then
                      // ToDocument doesn't expect uvar that is added by the
                      // typechecker in tuple constructor
                      // TODO: where should be store the universe information?
                      mk (A.Construct(head, args))
                    else
                      if (Options.print_universes()) then
                        mk (A.Construct(head, args@universes))
                      else
                        mk (A.Construct(head, args))
                | Tm_meta(_, m) ->
                  // the Tm_app for Data_app could be wrapped inside Tm_meta(_, Meta_monadic) after TypeChecker
                  // applies monadic_application
                  begin match m with
                    | Meta_monadic (_, _) -> resugar_term e
                    | _ -> failwith "wrong Tm_meta format in Meta_desugared"
                  end
                | _ ->
                  failwith "wrong Data_app format"
              end
          | Sequence ->
              let term = resugar_term e in
              let rec resugar_seq t = match t.tm with
                | A.Let(_, [p, t1], t2) ->
                    mk (A.Seq(t1, t2))
                | A.Ascribed(t1, t2, t3) ->
                    (* this case happens when the let is wrapped in Meta_Monadic which is resugared to Ascribe*)
                    mk (A.Ascribed(resugar_seq t1, t2, t3))
                | _ ->
                    (* this case happens in typechecker.normalize when Tm_let is_pure_effect, then
                      only the body of Tm_let is used. *)
                    (* TODO: How should it be resugared *)
                    t
              in
              resugar_seq term
          | Primop (* doesn't seem to be generated by desugar *)
          | Masked_effect (* doesn't seem to be generated by desugar *)
          | Meta_smt_pat -> (* nothing special, just resugar the term *)
              resugar_term e
          | Mutable_alloc ->
              let term = resugar_term e in
              begin match term.tm with
                | A.Let(A.NoLetQualifier,l,t) -> mk (A.Let(A.Mutable, l, t))
                | _ -> failwith "mutable_alloc should have let term with no qualifier"
              end
          | Mutable_rval ->
              let fv = S.lid_as_fv C.sread_lid Delta_constant None in
              begin match (SS.compress e).n with
                | Tm_app({n=Tm_fvar fv}, [(term, _)])-> resugar_term term
                | _ -> failwith "mutable_rval should have app term"
              end
      in
      begin match m with
      | Meta_pattern pats ->
        // This case is possible in TypeChecker when creating "haseq" for Sig_inductive_typ whose Sig_datacon has no binders.
        let pats = List.flatten pats |> List.map (fun (x, _) -> resugar_term x) in
        // Is it correct to resugar it to Attributes.
        mk (A.Attributes pats)
  
      | Meta_labeled (l, _, p) ->
          mk (A.Labeled(resugar_term e, l, p))
      | Meta_desugared i ->
          resugar_meta_desugared i
      | Meta_named t ->
          mk (A.Name t)
      | Meta_monadic (name, t)
      | Meta_monadic_lift (name, _, t) ->
        mk (A.Ascribed(resugar_term e,
                        mk (A.Construct(name,[resugar_term t, A.Nothing])),
                        None))
      end
  
    | Tm_unknown -> mk A.Wild
  
  and resugar_comp (c:S.comp) : A.term =
    let mk (a:A.term') : A.term =
  