anchor.diff:      reduce_primops ({cfg with steps = { default_steps with primops = true };
                                 primitive_steps=equality_ops}) tm
   
  +(********************************************************************************************************************)
  +(* Main normalization function of the abstract machine                                                              *)
  +(********************************************************************************************************************)
  +let is_norm_request hd args =
  +    match (U.un_uinst hd).n, args with
  +    | Tm_fvar fv, [_; _] ->
  +      S.fv_eq_lid fv PC.normalize_term
  +
  +    | Tm_fvar fv, [_] ->
  +      S.fv_eq_lid fv PC.normalize
  +
  +    | Tm_fvar fv, [steps; _; _] ->
  +      S.fv_eq_lid fv PC.norm
  +
  +    | _ -> false
  +
  +let tr_norm_step = function
  +    | EMB.Zeta ->    [Zeta]
  +    | EMB.Iota ->    [Iota]
  +    | EMB.Delta ->   [UnfoldUntil Delta_constant]
  +    | EMB.Simpl ->   [Simplify]
  +    | EMB.Weak ->    [Weak]
  +    | EMB.HNF  ->    [HNF]
  +    | EMB.Primops -> [Primops]
  +    | EMB.UnfoldOnly names ->
  +        [UnfoldUntil Delta_constant; UnfoldOnly (List.map I.lid_of_str names)]
  +    | EMB.UnfoldAttr t ->
  +        [UnfoldUntil Delta_constant; UnfoldAttr t]
  +
  +let tr_norm_steps s =
  +    List.concatMap tr_norm_step s
  +
  +let get_norm_request (full_norm:term -> term) args =
  +    let parse_steps s =
  +      try
  +        Some (EMB.unembed_list_safe EMB.unembed_norm_step s |> BU.must |> tr_norm_steps)
  +      with | _ -> None
  +    in
  +    match args with
  +    | [_; (tm, _)]
  +    | [(tm, _)] ->
  +      let s = [Beta; Zeta; Iota; Primops; UnfoldUntil Delta_constant; Reify] in
  +      Some (s, tm)
  +    | [(steps, _); _; (tm, _)] ->
  +      let add_exclude s z = if List.contains z s then s else Exclude z :: s in
  +      begin
  +      match parse_steps (full_norm steps) with
  +      | None -> None
  +      | Some s ->
  +        let s = Beta::s in
  +        let s = add_exclude s Zeta in
  +        let s = add_exclude s Iota in
  +        Some (s, tm)
  +      end
  +    | _ ->
  +      None
  +
  +let is_reify_head = function
  +    | App(_, {n=Tm_constant FC.Const_reify}, _, _)::_ ->
  +      true
  +    | _ ->
  +      false
  +
  +let firstn k l = if List.length l < k then l,[] else first_N k l
  +let should_reify cfg stack = match stack with
  +    // TODO: we should likely ignore the meta-level stack elements, such as Memo
  +    | App (_, {n=Tm_constant FC.Const_reify}, _, _) :: _ ->
  +        // BU.print1 "Found a reify on the stack. %s" "" ;
  +        cfg.steps.reify_
  +    | _ -> false
  +
  +let rec norm : cfg -> env -> stack -> term -> term =
  +    fun cfg env stack t ->
  +        let t =
  +            if cfg.debug.norm_delayed
  +            then (match t.n with
  +                  | Tm_delayed _ ->
  +                    BU.print1 "NORM delayed: %s\n" (Print.term_to_string t)
  +                  | _ -> ());
  +            compress t
  +        in
  +        log cfg  (fun () ->
  +          BU.print4 ">>> %s\nNorm %s with with %s env elements top of the stack %s \n"
  +                                        (Print.tag_of_term t)
  +                                        (Print.term_to_string t)
  +                                        (BU.string_of_int (List.length env))
  +                                        (stack_to_string (fst <| firstn 4 stack)));
  +        match t.n with
  +          | Tm_unknown
  +          | Tm_constant _
  +          | Tm_name _
  +
  +          | Tm_lazy _
  +
  +          | Tm_fvar( {fv_delta=Delta_constant} )
  +          | Tm_fvar( {fv_qual=Some Data_ctor } )
  +          | Tm_fvar( {fv_qual=Some (Record_ctor _)} ) -> //these last three are just constructors; no delta steps can apply
  +            //log cfg (fun () -> BU.print "Tm_fvar case 0\n" []) ;
  +            rebuild cfg env stack t
  +
  +          | Tm_meta (t0, Meta_quoted (t1, qi)) ->
  +            let t0 = closure_as_term cfg env t0 in
  +            let t1 = if qi.qopen
  +                     then closure_as_term cfg env t1
  +                     else t1
  +            in
  +            let t = { t with n = Tm_meta (t0, Meta_quoted (t1, qi)) } in
  +            rebuild cfg env stack t
  +
  +          | Tm_app(hd, args)
  +            when not (cfg.steps.no_full_norm)
  +              && is_norm_request hd args
  +              && not (Ident.lid_equals cfg.tcenv.curmodule PC.prims_lid) ->
  +            let cfg' = { cfg with steps = { cfg.steps with unfold_only = None
  +                                                         ; no_delta_steps = false };
  +                                  delta_level=[Unfold Delta_constant];
  +                                  normalize_pure_lets=true} in
  +            begin
  +            match get_norm_request (norm cfg' env []) args with
  +            | None -> //just normalize it as a normal application
  +              let stack =
  +                stack |>
  +                List.fold_right
  +                  (fun (a, aq) stack -> Arg (Clos(env, a, BU.mk_ref None, false),aq,t.pos)::stack)
  +                  args
  +              in
  +              log cfg  (fun () -> BU.print1 "\tPushed %s arguments\n" (string_of_int <| List.length args));
  +              norm cfg env stack hd
  +
  +            | Some (s, tm) ->
  +              let delta_level =
  +                if s |> BU.for_some (function UnfoldUntil _ | UnfoldOnly _ -> true | _ -> false)
  +                then [Unfold Delta_constant]
  +                else [NoDelta] in
  +              let cfg' = {cfg with steps = to_fsteps s
  +                               ; delta_level = delta_level
  +                               ; normalize_pure_lets = true } in
  +              let stack' =
  +                let tail = (Cfg cfg)::stack in
  +                if cfg.debug.print_normalized
  +                then Debug(t, BU.now())::tail
  +                else tail in
  +              norm cfg' env stack' tm
  +            end
  +
  +          | Tm_type u ->
  +            let u = norm_universe cfg env u in
  +            rebuild cfg env stack (mk (Tm_type u) t.pos)
  +
  +          | Tm_uinst(t', us) ->
  +            if cfg.steps.erase_universes
  +            then norm cfg env stack t'
  +            else let us = UnivArgs(List.map (norm_universe cfg env) us, t.pos) in
  +                 let stack = us::stack in
  +                 norm cfg env stack t'
  +
  +          | Tm_fvar fv ->
  +            let qninfo = Env.lookup_qname cfg.tcenv (S.lid_of_fv fv) in
  +            if Env.qninfo_is_action qninfo
  +            // we don't unfold dm4f actions unless reifying
  +            then let b = should_reify cfg stack in
  +                 log cfg (fun () -> BU.print2 ">>> For DM4F action %s, should_reify = %s\n"
  +                                          (Print.term_to_string t)
  +                                          (string_of_bool b));
  +                 if b
  +                 then do_unfold_fv cfg env (List.tl stack) t qninfo fv
  +                 else rebuild cfg env stack t
  +            else // not an action, common case
  +                 let should_delta =
  +                     Option.isNone (find_prim_step cfg fv) //if it is handled primitively, then don't unfold
  +                     && cfg.delta_level |> BU.for_some (function
  +                         | Env.UnfoldTac
  +                         | NoDelta -> false
  +                         | Env.Inlining
  +                         | Eager_unfolding_only -> true
  +                         | Unfold l -> Common.delta_depth_greater_than fv.fv_delta l)
  +                 in
  +                 let should_delta = should_delta && (
  +                          let attrs = Env.attrs_of_qninfo qninfo in
  +                           // never unfold something marked tac_opaque when reducing tactics
  +                          (not cfg.steps.unfold_tac ||
  +                           not (cases (BU.for_some (U.attr_eq U.tac_opaque_attr)) false attrs)) &&
  +                          //otherwise, unfold fv if it appears in "Delta_only" or if one of the Delta_attr matches
  +                          ( //delta_only l
  +                            (match cfg.steps.unfold_only with
  +                             | None -> true
  +                             | Some lids -> BU.for_some (fv_eq_lid fv) lids) ||
  +                           ( //delta_attrs a
  +                             match attrs, cfg.steps.unfold_attr with
  +                             | None, Some _ -> false
  +                             | Some ats, Some ats' -> BU.for_some (fun at -> BU.for_some (U.attr_eq at) ats') ats
  +                             | _, _ -> false)))
  +                 in
  +                 log cfg (fun () -> BU.print3 ">>> For %s (%s), should_delta = %s\n"
  +                                 (Print.term_to_string t)
  +                                 (Range.string_of_range t.pos)
  +                                 (string_of_bool should_delta));
  +                 if should_delta
  +                 then do_unfold_fv cfg env stack t qninfo fv
  +                 else rebuild cfg env stack t
  +
  +          | Tm_bvar x ->
  +            begin match lookup_bvar env x with
  +                | Univ _ -> failwith "Impossible: term variable is bound to a universe"
  +                | Dummy -> failwith "Term variable not found"
  +                | Clos(env, t0, r, fix) ->
  +                   if not fix || cfg.steps.zeta
  +                   then match !r with
  +                        | Some (env, t') ->
  +                            log cfg  (fun () -> BU.print2 "Lazy hit: %s cached to %s\n" (Print.term_to_string t) (Print.term_to_string t'));
  +                            begin match (compress t').n with
  +                                | Tm_abs _  ->
  +                                    norm cfg env stack t'
  +                                | _ ->
  +                                    rebuild cfg env stack t'
  +                            end
  +                        | None -> norm cfg env (MemoLazy r::stack) t0
  +                   else norm cfg env stack t0 //Fixpoint steps are excluded; so don't take the recursive knot
  +            end
  +
  +          | Tm_abs(bs, body, lopt) ->
  +            begin match stack with
  +                | UnivArgs _::_ ->
  +                  failwith "Ill-typed term: universes cannot be applied to term abstraction"
  +
  +                | Match _::_ ->
  +                  failwith "Ill-typed term: cannot pattern match an abstraction"
  +
  +                | Arg(c, _, _)::stack_rest ->
  +                  begin match c with
  +                    | Univ _ -> //universe variables do not have explicit binders
  +                      norm cfg ((None,c)::env) stack_rest t
  +
  +                    | _ ->
  +                     (* Note: we peel off one application at a time.
  +                              An optimization to attempt would be to push n-args are once,
  +                              and try to pop all of them at once, in the common case of a full application.
  +                      *)
  +                      begin match bs with
  +                        | [] -> failwith "Impossible"
  +                        | [b] ->
  +                          log cfg  (fun () -> BU.print1 "\tShifted %s\n" (closure_to_string c));
  +                          norm cfg ((Some b, c) :: env) stack_rest body
  +                        | b::tl ->
  +                          log cfg  (fun () -> BU.print1 "\tShifted %s\n" (closure_to_string c));
  +                          let body = mk (Tm_abs(tl, body, lopt)) t.pos in
  +                          norm cfg ((Some b, c) :: env) stack_rest body
  +                      end
  +                  end
  +
  +                | Cfg cfg :: stack ->
  +                  norm cfg env stack t
  +
  +                | MemoLazy r :: stack ->
  +                  set_memo cfg r (env, t); //We intentionally do not memoize the strong normal form; only the WHNF
  +                  log cfg  (fun () -> BU.print1 "\tSet memo %s\n" (Print.term_to_string t));
  +                  norm cfg env stack t
  +
  +                | Debug _::_
  +                | Meta _::_
  +                | Let _ :: _
  +                | App _ :: _
  +                | Abs _ :: _
  +                | [] ->
  +                  if cfg.steps.weak //don't descend beneath a lambda if we're just doing weak reduction
  +                  then rebuild cfg env stack (closure_as_term cfg env t) //But, if the environment is non-empty, we need to substitute within the term
  +                  else let bs, body, opening = open_term' bs body in
  +                       let env' = bs |> List.fold_left (fun env _ -> dummy::env) env in
  +                       let lopt = match lopt with
  +                        | Some rc ->
  +                          let rct =
  +                            if cfg.steps.check_no_uvars
  +                            then BU.map_opt rc.residual_typ (fun t -> norm cfg env' [] (SS.subst opening t))
  +                            else BU.map_opt rc.residual_typ (SS.subst opening) in
  +                          Some ({rc with residual_typ=rct})
  +                        | _ -> lopt in
  +                       log cfg  (fun () -> BU.print1 "\tShifted %s dummies\n" (string_of_int <| List.length bs));
  +                       let stack = (Cfg cfg)::stack in
  +                       let cfg = { cfg with strong = true } in
  +                       norm cfg env' (Abs(env, bs, env', lopt, t.pos)::stack) body
  +            end
  +
  +          | Tm_app(head, args) ->
  +            let stack = stack |> List.fold_right (fun (a, aq) stack -> Arg (Clos(env, a, BU.mk_ref None, false),aq,t.pos)::stack) args in
  +            log cfg  (fun () -> BU.print1 "\tPushed %s arguments\n" (string_of_int <| List.length args));
  +            norm cfg env stack head
  +
  +          | Tm_refine(x, f) -> //non tail-recursive; the alternative is to keep marks on the stack to rebuild the term ... but that's very heavy
  +            if cfg.steps.weak
  +            then match env, stack with
  +                    | [], [] -> //TODO: Make this work in general!
  +                      let t_x = norm cfg env [] x.sort in
  +                      let t = mk (Tm_refine({x with sort=t_x}, f)) t.pos in
  +                      rebuild cfg env stack t
  +                    | _ -> rebuild cfg env stack (closure_as_term cfg env t)
  +            else let t_x = norm cfg env [] x.sort in
  +                 let closing, f = open_term [(x, None)] f in
  +                 let f = norm cfg (dummy::env) [] f in
  +                 let t = mk (Tm_refine({x with sort=t_x}, close closing f)) t.pos in
  +                 rebuild cfg env stack t
  +
  +          | Tm_arrow(bs, c) ->
  +            if cfg.steps.weak
  +            then rebuild cfg env stack (closure_as_term cfg env t)
  +            else let bs, c = open_comp bs c in
  +                 let c = norm_comp cfg (bs |> List.fold_left (fun env _ -> dummy::env) env) c in
  +                 let t = arrow (norm_binders cfg env bs) c in
  +                 rebuild cfg env stack t
  +
  +          | Tm_ascribed(t1, (tc, tacopt), l) when cfg.steps.unascribe ->
  +            norm cfg env stack t1
  +
  +          | Tm_ascribed(t1, (tc, tacopt), l) ->
  +            begin match stack with
  +              | Match _ :: _
  +              | Arg _ :: _
  +              | App (_, {n=Tm_constant FC.Const_reify}, _, _) :: _
  +              | MemoLazy _ :: _ ->
  +                log cfg  (fun () -> BU.print_string "+++ Dropping ascription \n");
  +                norm cfg env stack t1 //ascriptions should not block reduction
  +              | _ ->
  +                (* Drops stack *)
  +                log cfg  (fun () -> BU.print_string "+++ Keeping ascription \n");
  +                let t1 = norm cfg env [] t1 in
  +                log cfg  (fun () -> BU.print_string "+++ Normalizing ascription \n");
  +                let tc = match tc with
  +                    | Inl t -> Inl (norm cfg env [] t)
  +                    | Inr c -> Inr (norm_comp cfg env c) in
  +                let tacopt = BU.map_opt tacopt (norm cfg env []) in
  +                match stack with
  +                | Cfg cfg :: stack ->
  +                  let t = mk (Tm_ascribed(U.unascribe t1, (tc, tacopt), l)) t.pos in
  +                  norm cfg env stack t
  +                | _ ->
  +                  rebuild cfg env stack (mk (Tm_ascribed(U.unascribe t1, (tc, tacopt), l)) t.pos)
  +            end
  +
  +          | Tm_match(head, branches) ->
  +            let stack = Match(env, branches, t.pos)::stack in
  +            norm cfg env stack head
  +
  +          | Tm_let((b, lbs), lbody) when is_top_level lbs && cfg.steps.compress_uvars ->
  +            let lbs = lbs |> List.map (fun lb ->
  +              let openings, lbunivs = Subst.univ_var_opening lb.lbunivs in
  +              let cfg = { cfg with tcenv = Env.push_univ_vars cfg.tcenv lbunivs } in
  +              let norm t = Subst.close_univ_vars lbunivs (norm cfg env [] (Subst.subst openings t)) in
  +              let lbtyp = norm lb.lbtyp in
  +              let lbdef = norm lb.lbdef in
  +              { lb with lbunivs = lbunivs; lbtyp = lbtyp; lbdef = lbdef }
  +            ) in
  +
  +            rebuild cfg env stack (mk (Tm_let ((b, lbs), lbody)) t.pos)
  +
  +          | Tm_let((_, {lbname=Inr _}::_), _) -> //this is a top-level let binding; nothing to normalize
  +            rebuild cfg env stack t
  +
  +          | Tm_let((false, [lb]), body) ->
  +            let n = TypeChecker.Env.norm_eff_name cfg.tcenv lb.lbeff in
  +            if not (cfg.steps.no_delta_steps) //we're allowed to do some delta steps, and ..
  +            && ((cfg.steps.pure_subterms_within_computations &&
  +                 U.has_attribute lb.lbattrs PC.inline_let_attr)        //1. we're extracting, and it's marked @inline_let
  +             || (U.is_pure_effect n && (cfg.normalize_pure_lets        //Or, 2. it's pure and we either not extracting, or
  +                                        || U.has_attribute lb.lbattrs PC.inline_let_attr)) //it's marked @inline_let
  +             || (U.is_ghost_effect n &&                                //Or, 3. it's ghost and we're not extracting
  +                    not (cfg.steps.pure_subterms_within_computations)))
  +            then let binder = S.mk_binder (BU.left lb.lbname) in
  +                 let env = (Some binder, Clos(env, lb.lbdef, BU.mk_ref None, false))::env in
  +                 log cfg (fun () -> BU.print_string "+++ Reducing Tm_let\n");
  +                 norm cfg env stack body
  +            else if cfg.steps.weak
  +            then (log cfg (fun () -> BU.print_string "+++ Not touching Tm_let\n");
  +                  rebuild cfg env stack (closure_as_term cfg env t))
  +            else let bs, body = Subst.open_term [lb.lbname |> BU.left |> S.mk_binder] body in
  +                 log cfg (fun () -> BU.print_string "+++ Normalizing Tm_let -- type");
  +                 let ty = norm cfg env [] lb.lbtyp in
  +                 let lbname =
  +                    let x = fst (List.hd bs) in
  +                    Inl ({x with sort=ty}) in
  +                 log cfg (fun () -> BU.print_string "+++ Normalizing Tm_let -- definiens\n");
  +                 let lb = {lb with lbname=lbname;
  +                                   lbtyp=ty;
  +                                   lbdef=norm cfg env [] lb.lbdef} in
  +                 let env' = bs |> List.fold_left (fun env _ -> dummy::env) env in
  +                 let stack = (Cfg cfg)::stack in
  +                 let cfg = { cfg with strong = true } in
  +                 log cfg (fun () -> BU.print_string "+++ Normalizing Tm_let -- body\n");
  +                 norm cfg env' (Let(env, bs, lb, t.pos)::stack) body
  +
  +          | Tm_let((true, lbs), body)
  +                when cfg.steps.compress_uvars
  +                  || ((not cfg.steps.zeta) &&
  +                      cfg.steps.pure_subterms_within_computations) -> //no fixpoint reduction allowed
  +            let lbs, body = Subst.open_let_rec lbs body in
  +            let lbs = List.map (fun lb ->
  +                let ty = norm cfg env [] lb.lbtyp in
  +                let lbname = Inl ({BU.left lb.lbname with sort=ty}) in
  +                let xs, def_body, lopt = U.abs_formals lb.lbdef in
  +                let xs = norm_binders cfg env xs in
  +                let env = List.map (fun _ -> dummy) lbs
  +                        @ List.map (fun _ -> dummy) xs
  +                        @ env in
  +                let def_body = norm cfg env [] def_body in
  +                let lopt =
  +                  match lopt with
  +                  | Some rc -> Some ({rc with residual_typ=BU.map_opt rc.residual_typ (norm cfg env [])})
  +                  | _ -> lopt in
  +                let def = U.abs xs def_body lopt in
  +                { lb with lbname = lbname;
  +                          lbtyp = ty;
  +                          lbdef = def}) lbs in
  +            let env' = List.map (fun _ -> dummy) lbs @ env in
  +            let body = norm cfg env' [] body in
  +            let lbs, body = Subst.close_let_rec lbs body in
  +            let t = {t with n=Tm_let((true, lbs), body)} in
  +            rebuild cfg env stack t
  +
  +          | Tm_let(lbs, body) when not cfg.steps.zeta -> //no fixpoint reduction allowed
  +            rebuild cfg env stack (closure_as_term cfg env t)
  +
  +          | Tm_let(lbs, body) ->
  +            //let rec: The basic idea is to reduce the body in an environment that includes recursive bindings for the lbs
  +            //Consider reducing (let rec f x = f x in f 0) in initial environment env
  +            //We build two environments, rec_env and body_env and reduce (f 0) in body_env
  +            //rec_env = Clos(env, let rec f x = f x in f, memo)::env
  +            //body_env = Clos(rec_env, \x. f x, _)::env
  +            //i.e., in body, the bound variable is bound to definition, \x. f x
  +            //Within the definition \x.f x, f is bound to the recursive binding (let rec f x = f x in f), aka, fix f. \x. f x
  +            //Finally, we add one optimization for laziness by tying a knot in rec_env
  +            //i.e., we set memo := Some (rec_env, \x. f x)
  +
  +            let rec_env, memos, _ = List.fold_right (fun lb (rec_env, memos, i) ->
  +                    let bv = {left lb.lbname with index=i} in
  +                    let f_i = Syntax.bv_to_tm bv in
  +                    let fix_f_i = mk (Tm_let(lbs, f_i)) t.pos in
  +                    let memo = BU.mk_ref None in
  +                    let rec_env = (None, Clos(env, fix_f_i, memo, true))::rec_env in
  +                    rec_env, memo::memos, i + 1) (snd lbs) (env, [], 0) in
  +            let _ = List.map2 (fun lb memo -> memo := Some (rec_env, lb.lbdef)) (snd lbs) memos in //tying the knot
  +            let body_env = List.fold_right (fun lb env -> (None, Clos(rec_env, lb.lbdef, BU.mk_ref None, false))::env)
  +                               (snd lbs) env in
  +            norm cfg body_env stack body
  +
  +          | Tm_meta (head, m) ->
  +            log cfg (fun () -> BU.print1 ">> metadata = %s\n" (Print.metadata_to_string m));
  +            begin match m with
  +              | Meta_monadic (m, t) ->
  +                reduce_impure_comp cfg env stack head (Inl m) t
  +
  +              | Meta_monadic_lift (m, m', t) ->
  +                reduce_impure_comp cfg env stack head (Inr (m, m')) t
  +
  +              | Meta_quoted (qt, inf) ->
  +                rebuild cfg env stack t
  +
  +              | _ ->
  +                if cfg.steps.unmeta
  +                then norm cfg env stack head
  +                else begin match stack with
  +                  | _::_ ->
  +                    begin match m with
  +                      | Meta_labeled(l, r, _) ->
  +                        (* meta doesn't block reduction, but we need to put the label back *)
  +                        norm cfg env (Meta(m,r)::stack) head
  +
  +                      | Meta_pattern args ->
  +                          let args = norm_pattern_args cfg env args in
  +                          norm cfg env (Meta(Meta_pattern args, t.pos)::stack) head //meta doesn't block reduction, but we need to put the label back
  +
  +                      | _ ->
  +                          norm cfg env stack head //meta doesn't block reduction
  +                    end
  +                  | [] ->
  +                    let head = norm cfg env [] head in
  +                    let m = match m with
  +                        | Meta_pattern args ->
  +                            Meta_pattern (norm_pattern_args cfg env args)
  +                        | _ -> m in
  +                    let t = mk (Tm_meta(head, m)) t.pos in
  +                    rebuild cfg env stack t
  +                end
  +        end //Tm_meta
  +
  +        | Tm_delayed _ ->
  +          let t = SS.compress t in
  +          norm cfg env stack t
  +
  +        | Tm_uvar _ ->
  +          let t = SS.compress t in
  +          match t.n with
  +          | Tm_uvar _ ->
  +            if cfg.steps.check_no_uvars
  +            then failwith (BU.format2 "(%s) CheckNoUvars: Unexpected unification variable remains: %s"
  +                                    (Range.string_of_range t.pos)
  +                                    (Print.term_to_string t))
  +            else rebuild cfg env stack t
  +
  +          | _ ->
  +            norm cfg env stack t
  +
  +
  +
  +and do_unfold_fv cfg env stack (t0:term) (qninfo : qninfo) (f:fv) : term =
  +    //preserve the range info on the returned def
  +    let r_env = Env.set_range cfg.tcenv (S.range_of_fv f) in
  +    match Env.lookup_definition_qninfo cfg.delta_level f.fv_name.v qninfo with
  +       | None ->
  +         log cfg (fun () -> BU.print "Tm_fvar case 2\n" []) ;
  +         rebuild cfg env stack t0
  +
  +       | Some (us, t) ->
  +         log cfg (fun () -> BU.print2 ">>> Unfolded %s to %s\n"
  +                       (Print.term_to_string t0) (Print.term_to_string t));
  +         let t =
  +           if cfg.steps.unfold_until = Some Delta_constant
  +            && not cfg.steps.unfold_tac
  +           //we're really trying to compute here; no point propagating range information
  +           //which can be expensive (except for tactics: it matters for tracing!)
  +           then t
  +           else Subst.set_use_range (Ident.range_of_lid f.fv_name.v) t
  +         in
  +         let n = List.length us in
  +         if n > 0
  +         then match stack with //universe beta reduction
  +                | UnivArgs(us', _)::stack ->
  +                  let env = us' |> List.fold_left (fun env u -> (None, Univ u)::env) env in
  +                  norm cfg env stack t
  +                | _ when cfg.steps.erase_universes || cfg.steps.allow_unbound_universes ->
  +                  norm cfg env stack t
  +                | _ -> failwith (BU.format1 "Impossible: missing universe instantiation on %s" (Print.lid_to_string f.fv_name.v))
  +         else norm cfg env stack t
  +
  +and reduce_impure_comp cfg env stack (head : term) // monadic term
  +                                     (m : either<monad_name,(monad_name * monad_name)>)
  +                                        // relevant monads.
  +                                        // Inl m - this is a Meta_monadic with monad m
  +                                        // Inr (m, m') - this is a Meta_monadic_lift with monad m
  +                                     (t : typ) // annotated type in the Meta
  +                                     : term =
  +    (* We have an impure computation, and we aim to perform any pure      *)
  +    (* steps within that computation.                                     *)
  +
  +    (* This scenario arises primarily as we extract (impure) programs and *)
  +    (* partially evaluate them before extraction, as an optimization.     *)
  +
  +    (* First, we reduce **the type annotation** t with an empty stack (as *)
  +    (* it's not applied to anything)                                      *)
  +
  +    (* Then, we reduce the monadic computation `head`, in a stack marked  *)
  +    (* with a Meta_monadic, indicating that this reduction should         *)
  +    (* not consume any arguments on the stack. `rebuild` will notice      *)
  +    (* the Meta_monadic marker and reconstruct the computation after      *)
  +    (* normalization.                                                     *)
  +    let t = norm cfg env [] t in
  +    let stack = (Cfg cfg)::stack in
  +    let cfg =
  +      if cfg.steps.pure_subterms_within_computations
  +      then
  +        let new_steps = [PureSubtermsWithinComputations;
  +                         Primops;
  +                         AllowUnboundUniverses;
  +                         EraseUniverses;
  +                         Exclude Zeta;
  +                         Inlining]
  +        in { cfg with
  +               steps = List.fold_right fstep_add_one new_steps cfg.steps;
  +               delta_level = [Env.Inlining; Env.Eager_unfolding_only]
  +           }
  +      else
  +        { cfg with steps = { cfg.steps with zeta = false } }
  +    in
  +    (* monadic annotations don't block reduction, but we need to put the label back *)
  +    let metadata = match m with
  +                   | Inl m -> Meta_monadic (m, t)
  +                   | Inr (m, m') -> Meta_monadic_lift (m, m', t)
  +    in
  +    norm cfg env (Meta(metadata, head.pos)::stack) head
  +
  +and do_reify_monadic fallback cfg env stack (head : term) (m : monad_name) (t : typ) : term =
  +    (* Precondition: the stack head is an App (reify, ...) *)
  +    let head0 = head in
  +    let head = U.unascribe head in
  +    log cfg (fun () -> BU.print2 "Reifying: (%s) %s\n" (Print.tag_of_term head) (Print.term_to_string head));
  +    let head = U.unmeta_safe head in
  +    match (SS.compress head).n with
  +    | Tm_let ((false, [lb]), body) ->
  +      (* ****************************************************************************)
  +      (* Monadic binding                                                            *)
  +      (*                                                                            *)
  +      (* This is reify (M.bind e1 (fun x -> e2)) which is elaborated to             *)
  +      (*                                                                            *)
  +      (*        M.bind_repr (reify e1) (fun x -> reify e2)                          *)
  +      (*                                                                            *)
  +      (* ****************************************************************************)
  +      let ed = Env.get_effect_decl cfg.tcenv (Env.norm_eff_name cfg.tcenv m) in
  +      let _, bind_repr = ed.bind_repr in
  +      begin match lb.lbname with
  +        | Inr _ -> failwith "Cannot reify a top-level let binding"
  +        | Inl x ->
  +
  +          (* [is_return e] returns [Some e'] if [e] is a lift from Pure of [e'], [None] otherwise *)
  +          let is_return e =
  +            match (SS.compress e).n with
  +            | Tm_meta(e, Meta_monadic(_, _)) ->
  +              begin match (SS.compress e).n with
  +                | Tm_meta(e, Meta_monadic_lift(_, msrc, _)) when U.is_pure_effect msrc ->
  +                    Some (SS.compress e)
  +                | _ -> None
  +              end
  +           | _ -> None
  +          in
  +
  +          match is_return lb.lbdef with
  +          (* We are in the case where [head] = [bind (return e) (fun x -> body)] *)
  +          (* which can be optimised to a non-monadic let-binding [let x = e in body] *)
  +          | Some e ->
  +            let lb = {lb with lbeff=PC.effect_PURE_lid; lbdef=e} in
  +            norm cfg env (List.tl stack) (S.mk (Tm_let((false, [lb]), U.mk_reify body)) None head.pos)
  +          | None ->
  +            if (match is_return body with Some ({n=Tm_bvar y}) -> S.bv_eq x y | _ -> false)
  +            then
  +              (* We are in the case where [head] = [bind e (fun x -> return x)] *)
  +              (* which can be optimised to just keeping normalizing [e] with a reify on the stack *)
  +              norm cfg env stack lb.lbdef
  +            else (
  +              (* TODO : optimize [bind (bind e1 e2) e3] into [bind e1 (bind e2 e3)] *)
  +              (* Rewriting binds in that direction would be better for exception-like monad *)
  +              (* since we wouldn't rematch on an already raised exception *)
  +              let rng = head.pos in
  +
  +              let head = U.mk_reify <| lb.lbdef in
  +              let body = U.mk_reify <| body in
  +              (* TODO : Check that there is no sensible cflags to pass in the residual_comp *)
  +              let body_rc = {
  +                residual_effect=m;
  +                residual_flags=[];
  +                residual_typ=Some t
  +              } in
  +              let body = S.mk (Tm_abs([S.mk_binder x], body, Some body_rc)) None body.pos in
  +              let close = closure_as_term cfg env in
  +              let bind_inst = match (SS.compress bind_repr).n with
  +                | Tm_uinst (bind, [_ ; _]) ->
  +                    S.mk (Tm_uinst (bind, [ cfg.tcenv.universe_of cfg.tcenv (close lb.lbtyp)
  +                                          ; cfg.tcenv.universe_of cfg.tcenv (close t)]))
  +                    None rng
  +                | _ -> failwith "NIY : Reification of indexed effects"
  +              in
  +              let maybe_range_arg =
  +                if BU.for_some (U.attr_eq U.dm4f_bind_range_attr) ed.eff_attrs
  +                then [as_arg (EMB.embed_range lb.lbpos lb.lbpos);
  +                      as_arg (EMB.embed_range body.pos body.pos)]
  +                else []
  +              in
  +              let reified = S.mk (Tm_app(bind_inst, [
  +                  (* a, b *)
  +                  as_arg lb.lbtyp; as_arg t] @
  +                  maybe_range_arg @ [
  +                  (* wp_head, head--the term shouldn't depend on wp_head *)
  +                  as_arg S.tun; as_arg head;
  +                  (* wp_body, body--the term shouldn't depend on wp_body *)
  +                  as_arg S.tun; as_arg body]))
  +                None rng
  +              in
  +              log cfg (fun () -> BU.print2 "Reified (1) <%s> to %s\n" (Print.term_to_string head0) (Print.term_to_string reified));
  +              norm cfg env (List.tl stack) reified
  +            )
  +      end
  +    | Tm_app (head_app, args) ->
  +        (* ****************************************************************************)
  +        (* Monadic application                                                        *)
  +        (*                                                                            *)
  +        (* The typechecker should have turned any monadic application into a serie of *)
  +        (* let-bindings (binding explicitly any monadic term)                         *)
  +        (*    let x0 = head in let x1 = arg0 in ... let xn = argn in x0 x1 ... xn     *)
  +        (*                                                                            *)
  +        (* which wil be ultimately reified to                                         *)
  +        (*     bind (reify head) (fun x0 ->                                           *)
  +        (*            bind (reify arg0) (fun x1 -> ... (fun xn -> x0 x1 .. xn) ))     *)
  +        (*                                                                            *)
  +        (* If head is an action then it is unfolded otherwise the                     *)
  +        (* resulting application is reified again                                     *)
  +        (* ****************************************************************************)
  +
  +
  +        let ed = Env.get_effect_decl cfg.tcenv (Env.norm_eff_name cfg.tcenv m) in
  +        let _, bind_repr = ed.bind_repr in
  +
  +        (* [maybe_unfold_action head] test whether [head] is an action and tries to unfold it if it is *)
  +        let maybe_unfold_action head : term * option<bool> =
  +          let maybe_extract_fv t =
  +            let t = match (SS.compress t).n with
  +              | Tm_uinst (t, _) -> t
  +              | _ -> head
  +            in match (SS.compress t).n with
  +              | Tm_fvar x -> Some x
  +              | _ -> None
  +          in
  +          match maybe_extract_fv head with
  +          | Some x when Env.is_action cfg.tcenv (S.lid_of_fv x) ->
  +            (* Note that this is not a tail call, but it's a bounded (small) number of recursive steps *)
  +            let head = norm cfg env [] head in
  +            let action_unfolded = match maybe_extract_fv head with | Some _ -> Some true | _ -> Some false in
  +            head, action_unfolded
  +          | _ ->
  +            head, None
  +        in
  +
  +        (* Checking that the typechecker did its job correctly and hoisted all impure *)
  +        (* terms to explicit let-bindings (see TcTerm, monadic_application) *)
  +        let _ =
  +          let is_arg_impure (e,q) =
  +            match (SS.compress e).n with
  +            | Tm_meta (e0, Meta_monadic_lift(m1, m2, t')) -> not (U.is_pure_effect m1)
  +            | _ -> false
  +          in
  +          if BU.for_some is_arg_impure ((as_arg head_app)::args)
  +          then failwith (BU.format1 "Incompability between typechecker and normalizer; \
  +                                     this monadic application contains impure terms %s\n"
  +                                    (Print.term_to_string head))
  +        in
  +
  +        let head_app, found_action = maybe_unfold_action head_app in
  +        let mk tm = S.mk tm None head.pos in
  +        let body = mk (Tm_app(head_app, args)) in
  +        let body = match found_action with
  +          (* This is not an action let's just keep the reify marker *)
  +          | None -> U.mk_reify body
  +
  +          (* The action was found but not unfolded (maybe abstract ?) *)
  +          | Some false -> mk (Tm_meta (body, Meta_monadic(m, t)))
  +
  +          (* An action was found and successfully unfolded *)
  +          | Some true -> body
  +        in
  +        log cfg (fun () -> BU.print2 "Reified (2) <%s> to %s\n" (Print.term_to_string head0) (Print.term_to_string body));
  +        norm cfg env (List.tl stack) body
  +
  +    // Doubly-annotated effect.. just take the outmost one. (unsure..)
  +    | Tm_meta(e, Meta_monadic _) ->
  +        do_reify_monadic fallback cfg env stack e m t
  +
  +    | Tm_meta(e, Meta_monadic_lift (msrc, mtgt, t')) ->
  +        let lifted = reify_lift cfg e msrc mtgt (closure_as_term cfg env t') in
  +        log cfg (fun () -> BU.print1 "Reified lift to (2): %s\n" (Print.term_to_string lifted));
  +        norm cfg env (List.tl stack) lifted
  +
  +    | Tm_match(e, branches) ->
  +      (* Commutation of reify with match, note that the scrutinee should never be effectful    *)
  +      (* (should be checked at typechecking and elaborated with an explicit binding if needed) *)
  +      (* reify (match e with p -> e') ~> match e with p -> reify e' *)
  +      let branches = branches |> List.map (fun (pat, wopt, tm) -> pat, wopt, U.mk_reify tm) in
  +      let tm = mk (Tm_match(e, branches)) head.pos in
  +      norm cfg env (List.tl stack) tm
  +
  +    | _ ->
  +      fallback ()
  +
  +(* Reifies the lifting of the term [e] of type [t] from computational  *)
  +(* effect [m] to computational effect [m'] using lifting data in [env] *)
  +and reify_lift cfg e msrc mtgt t : term =
  +  let env = cfg.tcenv in
  +  log cfg (fun () -> BU.print3 "Reifying lift %s -> %s: %s\n"
  +        (Ident.string_of_lid msrc) (Ident.string_of_lid mtgt) (Print.term_to_string e));
  +  (* check if the lift is concrete, if so replace by its definition on terms *)
  +  (* if msrc is PURE or Tot we can use mtgt.return *)
  +  if U.is_pure_effect msrc || U.is_div_effect msrc
  +  then
  +    let ed = Env.get_effect_decl env (Env.norm_eff_name cfg.tcenv mtgt) in
  +    let _, return_repr = ed.return_repr in
  +    let return_inst = match (SS.compress return_repr).n with
  +        | Tm_uinst(return_tm, [_]) ->
  +            S.mk (Tm_uinst (return_tm, [env.universe_of env t])) None e.pos
  +        | _ -> failwith "NIY : Reification of indexed effects"
  +    in
  +    S.mk (Tm_app(return_inst, [as_arg t ; as_arg e])) None e.pos
  +  else
  +    match Env.monad_leq env msrc mtgt with
  +    | None ->
  +      failwith (BU.format2 "Impossible : trying to reify a lift between unrelated effects (%s and %s)"
  +                            (Ident.text_of_lid msrc)
  +                            (Ident.text_of_lid mtgt))
  +    | Some {mlift={mlift_term=None}} ->
  +      failwith (BU.format2 "Impossible : trying to reify a non-reifiable lift (from %s to %s)"
  +                            (Ident.text_of_lid msrc)
  +                            (Ident.text_of_lid mtgt))
  +    | Some {mlift={mlift_term=Some lift}} ->
  +      (* We don't have any reasonable wp to provide so we just pass unknow *)
  +      (* Usually the wp is only necessary to typecheck, so this should not *)
  +      (* create a big issue. *)
  +      lift (env.universe_of env t) t S.tun (U.mk_reify e)
  +      (* We still eagerly unfold the lift to make sure that the Unknown is not kept stuck on a folded application *)
  +      (* let cfg = *)
  +      (*   { steps=[Exclude Iota ; Exclude Zeta; Inlining ; Eager_unfolding ; UnfoldUntil Delta_constant]; *)
  +      (*     tcenv=env; *)
  +      (*     delta_level=[Env.Unfold Delta_constant ; Env.Eager_unfolding_only ; Env.Inlining ] } *)
  +      (* in *)
  +      (* norm cfg [] [] (lift t S.tun (U.mk_reify e)) *)
  +
  +and norm_pattern_args cfg env args =
  +    (* Drops stack *)
  +    args |> List.map (List.map (fun (a, imp) -> norm cfg env [] a, imp))
  +
  +and norm_comp : cfg -> env -> comp -> comp =
  +    fun cfg env comp ->
  +        match comp.n with
  +            | Total (t, uopt) ->
  +              {comp with n=Total (norm cfg env [] t, Option.map (norm_universe cfg env) uopt)}
  +
  +            | GTotal (t, uopt) ->
  +              {comp with n=GTotal (norm cfg env [] t, Option.map (norm_universe cfg env) uopt)}
  +
  +            | Comp ct ->
  +              let norm_args args = args |> List.map (fun (a, i) -> (norm cfg env [] a, i)) in
  +              let flags = ct.flags |> List.map (function DECREASES t -> DECREASES (norm cfg env [] t) | f -> f) in
  +              {comp with n=Comp ({ct with comp_univs=List.map (norm_universe cfg env) ct.comp_univs;
  +                                          result_typ=norm cfg env [] ct.result_typ;
  +                                          effect_args=norm_args ct.effect_args;
  +                                          flags=flags})}
  +
  +and norm_binder : cfg -> env -> binder -> binder =
  +    fun cfg env (x, imp) -> {x with sort=norm cfg env [] x.sort}, imp
  +
  +and norm_binders : cfg -> env -> binders -> binders =
  +    fun cfg env bs ->
  +        let nbs, _ = List.fold_left (fun (nbs', env) b ->
  +            let b = norm_binder cfg env b in
  +            (b::nbs', dummy::env) (* crossing a binder, so shift environment *))
  +            ([], env)
  +            bs in
  +        List.rev nbs
  +
  +and norm_lcomp_opt : cfg -> env -> option<residual_comp> -> option<residual_comp> =
  +    fun cfg env lopt ->
  +        match lopt with
  +        | Some rc ->
  +          let flags = filter_out_lcomp_cflags rc.residual_flags in
  +          Some ({rc with residual_typ=BU.map_opt rc.residual_typ (norm cfg env [])})
  +       | _ -> lopt
  +
  +and maybe_simplify cfg env stack tm =
  +    let tm' = maybe_simplify_aux cfg env stack tm in
  +    if cfg.debug.b380
  +    then BU.print3 "%sSimplified\n\t%s to\n\t%s\n"
  +                   (if cfg.steps.simplify then "" else "NOT ")
  +                   (Print.term_to_string tm) (Print.term_to_string tm');
  +    tm'
  +
   (*******************************************************************)
   (* Simplification steps are not part of definitional equality      *)
   (* simplifies True /\ t, t /\ True, t /\ False, False /\ t etc.    *)
   (*******************************************************************)
  -let rec maybe_simplify_aux cfg env stack tm =
  +and maybe_simplify_aux cfg env stack tm =
       let tm = reduce_primops cfg env stack tm in
       if not <| cfg.steps.simplify then tm
       else
  
positive.code:         end
      | _ -> tm
  
  let maybe_simplify cfg env stack tm =
      let tm' = maybe_simplify_aux cfg env stack tm in
      if cfg.debug.b380
      then BU.print3 "%sSimplified\n\t%s to\n\t%s\n"
                     (if cfg.steps.simplify then "" else "NOT ")
                     (Print.term_to_string tm) (Print.term_to_string tm');
      tm'
  
  (********************************************************************************************************************)
  (* Main normalization function of the abstract machine                                                              *)
  (********************************************************************************************************************)
  let is_norm_request hd args =
      match (U.un_uinst hd).n, args with
      | Tm_fvar fv, [_; _] ->
        S.fv_eq_lid fv PC.normalize_term
  
      | Tm_fvar fv, [_] ->
        S.fv_eq_lid fv PC.normalize
  
      | Tm_fvar fv, [steps; _; _] ->
        S.fv_eq_lid fv PC.norm
  
      | _ -> false
  
  let tr_norm_step = function
      | EMB.Zeta ->    [Zeta]
      | EMB.Iota ->    [Iota]
      | EMB.Delta ->   [UnfoldUntil Delta_constant]
      | EMB.Simpl ->   [Simplify]
      | EMB.Weak ->    [Weak]
      | EMB.HNF  ->    [HNF]
      | EMB.Primops -> [Primops]
      | EMB.UnfoldOnly names ->
          [UnfoldUntil Delta_constant; UnfoldOnly (List.map I.lid_of_str names)]
      | EMB.UnfoldAttr t ->
          [UnfoldUntil Delta_constant; UnfoldAttr t]
  
  let tr_norm_steps s =
      List.concatMap tr_norm_step s
  
  let get_norm_request (full_norm:term -> term) args =
      let parse_steps s =
        try
          Some (EMB.unembed_list_safe EMB.unembed_norm_step s |> BU.must |> tr_norm_steps)
        with | _ -> None
      in
      match args with
      | [_; (tm, _)]
      | [(tm, _)] ->
        let s = [Beta; Zeta; Iota; Primops; UnfoldUntil Delta_constant; Reify] in
        Some (s, tm)
      | [(steps, _); _; (tm, _)] ->
        let add_exclude s z = if List.contains z s then s else Exclude z :: s in
        begin
        match parse_steps (full_norm steps) with
        | None -> None
        | Some s ->
          let s = Beta::s in
          let s = add_exclude s Zeta in
          let s = add_exclude s Iota in
          Some (s, tm)
        end
      | _ ->
        None
  
  let is_reify_head = function
      | App(_, {n=Tm_constant FC.Const_reify}, _, _)::_ ->
        true
      | _ ->
        false
  
  let firstn k l = if List.length l < k then l,[] else first_N k l
  let should_reify cfg stack = match stack with
      // TODO: we should likely ignore the meta-level stack elements, such as Memo
      | App (_, {n=Tm_constant FC.Const_reify}, _, _) :: _ ->
          // BU.print1 "Found a reify on the stack. %s" "" ;
          cfg.steps.reify_
      | _ -> false
  
  let rec norm : cfg -> env -> stack -> term -> term =
      fun cfg env stack t ->
          let t =
              if cfg.debug.norm_delayed
              then (match t.n with
                    | Tm_delayed _ ->
                      BU.print1 "NORM delayed: %s\n" (Print.term_to_string t)
                    | _ -> ());
              compress t
          in
          log cfg  (fun () ->
            BU.print4 ">>> %s\nNorm %s with with %s env elements top of the stack %s \n"
                                          (Print.tag_of_term t)
                                          (Print.term_to_string t)
                                          (BU.string_of_int (List.length env))
                                          (stack_to_string (fst <| firstn 4 stack)));
          match t.n with
            | Tm_unknown
            | Tm_constant _
            | Tm_name _
  
            | Tm_lazy _
  
            | Tm_fvar( {fv_delta=Delta_constant} )
            | Tm_fvar( {fv_qual=Some Data_ctor } )
            | Tm_fvar( {fv_qual=Some (Record_ctor _)} ) -> //these last three are just constructors; no delta steps can apply
              //log cfg (fun () -> BU.print "Tm_fvar case 0\n" []) ;
              rebuild cfg env stack t
  
            | Tm_meta (t0, Meta_quoted (t1, qi)) ->
              let t0 = closure_as_term cfg env t0 in
              let t1 = if qi.qopen
                       then closure_as_term cfg env t1
                       else t1
              in
              let t = { t with n = Tm_meta (t0, Meta_quoted (t1, qi)) } in
              rebuild cfg env stack t
  
            | Tm_app(hd, args)
              when not (cfg.steps.no_full_norm)
                && is_norm_request hd args
                && not (Ident.lid_equals cfg.tcenv.curmodule PC.prims_lid) ->
              let cfg' = { cfg with steps = { cfg.steps with unfold_only = None
                                                           ; no_delta_steps = false };
                                    delta_level=[Unfold Delta_constant];
                                    normalize_pure_lets=true} in
              begin
              match get_norm_request (norm cfg' env []) args with
              | None -> //just normalize it as a normal application
                let stack =
                  stack |>
                  List.fold_right
                    (fun (a, aq) stack -> Arg (Clos(env, a, BU.mk_ref None, false),aq,t.pos)::stack)
                    args
                in
                log cfg  (fun () -> BU.print1 "\tPushed %s arguments\n" (string_of_int <| List.length args));
                norm cfg env stack hd
  
              | Some (s, tm) ->
                let delta_level =
                  if s |> BU.for_some (function UnfoldUntil _ | UnfoldOnly _ -> true | _ -> false)
                  then [Unfold Delta_constant]
                  else [NoDelta] in
                let cfg' = {cfg with steps = to_fsteps s
                                 ; delta_level = delta_level
                                 ; normalize_pure_lets = true } in
                let stack' =
                  let tail = (Cfg cfg)::stack in
                  if cfg.debug.print_normalized
                  then Debug(t, BU.now())::tail
                  else tail in
                norm cfg' env stack' tm
              end
  
            | Tm_type u ->
              let u = norm_universe cfg env u in
              rebuild cfg env stack (mk (Tm_type u) t.pos)
  
            | Tm_uinst(t', us) ->
              if cfg.steps.erase_universes
              then norm cfg env stack t'
              else let us = UnivArgs(List.map (norm_universe cfg env) us, t.pos) in
                   let stack = us::stack in
                   norm cfg env stack t'
  
            | Tm_fvar fv ->
              let qninfo = Env.lookup_qname cfg.tcenv (S.lid_of_fv fv) in
              if Env.qninfo_is_action qninfo
              // we don't unfold dm4f actions unless reifying
              then let b = should_reify cfg stack in
                   log cfg (fun () -> BU.print2 ">>> For DM4F action %s, should_reify = %s\n"
                                            (Print.term_to_string t)
                                            (string_of_bool b));
                   if b
                   then do_unfold_fv cfg env (List.tl stack) t qninfo fv
                   else rebuild cfg env stack t
              else // not an action, common case
                   let should_delta =
                       Option.isNone (find_prim_step cfg fv) //if it is handled primitively, then don't unfold
                       && cfg.delta_level |> BU.for_some (function
                           | Env.UnfoldTac
                           | NoDelta -> false
                           | Env.Inlining
                           | Eager_unfolding_only -> true
                           | Unfold l -> Common.delta_depth_greater_than fv.fv_delta l)
                   in
                   let should_delta = should_delta && (
                            let attrs = Env.attrs_of_qninfo qninfo in
                             // never unfold something marked tac_opaque when reducing tactics
                            (not cfg.steps.unfold_tac ||
                             not (cases (BU.for_some (U.attr_eq U.tac_opaque_attr)) false attrs)) &&
                            //otherwise, unfold fv if it appears in "Delta_only" or if one of the Delta_attr matches
                            ( //delta_only l
                              (match cfg.steps.unfold_only with
                               | None -> true
                               | Some lids -> BU.for_some (fv_eq_lid fv) lids) ||
                             ( //delta_attrs a
                               match attrs, cfg.steps.unfold_attr with
                               | None, Some _ -> false
                               | Some ats, Some ats' -> BU.for_some (fun at -> BU.for_some (U.attr_eq at) ats') ats
                               | _, _ -> false)))
                   in
                   log cfg (fun () -> BU.print3 ">>> For %s (%s), should_delta = %s\n"
                                   (Print.term_to_string t)
                                   (Range.string_of_range t.pos)
                                   (string_of_bool should_delta));
                   if should_delta
                   then do_unfold_fv cfg env stack t qninfo fv
                   else rebuild cfg env stack t
  
            | Tm_bvar x ->
              begin match lookup_bvar env x with
                  | Univ _ -> failwith "Impossible: term variable is bound to a universe"
                  | Dummy -> failwith "Term variable not found"
                  | Clos(env, t0, r, fix) ->
                     if not fix || cfg.steps.zeta
                     then match !r with
                          | Some (env, t') ->
                              log cfg  (fun () -> BU.print2 "Lazy hit: %s cached to %s\n" (Print.term_to_string t) (Print.term_to_string t'));
                              begin match (compress t').n with
                                  | Tm_abs _  ->
                                      norm cfg env stack t'
                                  | _ ->
                                      rebuild cfg env stack t'
                              end
                          | None -> norm cfg env (MemoLazy r::stack) t0
                     else norm cfg env stack t0 //Fixpoint steps are excluded; so don't take the recursive knot
              end
  
            | Tm_abs(bs, body, lopt) ->
              begin match stack with
                  | UnivArgs _::_ ->
                    failwith "Ill-typed term: universes cannot be applied to term abstraction"
  
                  | Match _::_ ->
                    failwith "Ill-typed term: cannot pattern match an abstraction"
  
                  | Arg(c, _, _)::stack_rest ->
                    begin match c with
                      | Univ _ -> //universe variables do not have explicit binders
                        norm cfg ((None,c)::env) stack_rest t
  
                      | _ ->
                       (* Note: we peel off one application at a time.
                                An optimization to attempt would be to push n-args are once,
                                and try to pop all of them at once, in the common case of a full application.
                        *)
                        begin match bs with
                          | [] -> failwith "Impossible"
                          | [b] ->
                            log cfg  (fun () -> BU.print1 "\tShifted %s\n" (closure_to_string c));
                            norm cfg ((Some b, c) :: env) stack_rest body
                          | b::tl ->
                            log cfg  (fun () -> BU.print1 "\tShifted %s\n" (closure_to_string c));
                            let body = mk (Tm_abs(tl, body, lopt)) t.pos in
                            norm cfg ((Some b, c) :: env) stack_rest body
                        end
                    end
  
                  | Cfg cfg :: stack ->
                    norm cfg env stack t
  
                  | MemoLazy r :: stack ->
                    set_memo cfg r (env, t); //We intentionally do not memoize the strong normal form; only the WHNF
                    log cfg  (fun () -> BU.print1 "\tSet memo %s\n" (Print.term_to_string t));
                    norm cfg env stack t
  
                  | Debug _::_
                  | Meta _::_
                  | Let _ :: _
                  | App _ :: _
                  | Abs _ :: _
                  | [] ->
                    if cfg.steps.weak //don't descend beneath a lambda if we're just doing weak reduction
                    then rebuild cfg env stack (closure_as_term cfg env t) //But, if the environment is non-empty, we need to substitute within the term
                    else let bs, body, opening = open_term' bs body in
                         let env' = bs |> List.fold_left (fun env _ -> dummy::env) env in
                         let lopt = match lopt with
                          | Some rc ->
                            let rct =
                              if cfg.steps.check_no_uvars
                              then BU.map_opt rc.residual_typ (fun t -> norm cfg env' [] (SS.subst opening t))
                              else BU.map_opt rc.residual_typ (SS.subst opening) in
                            Some ({rc with residual_typ=rct})
                          | _ -> lopt in
                         log cfg  (fun () -> BU.print1 "\tShifted %s dummies\n" (string_of_int <| List.length bs));
                         let stack = (Cfg cfg)::stack in
                         let cfg = { cfg with strong = true } in
                         norm cfg env' (Abs(env, bs, env', lopt, t.pos)::stack) body
              end
  
            | Tm_app(head, args) ->
              let stack = stack |> List.fold_right (fun (a, aq) stack -> Arg (Clos(env, a, BU.mk_ref None, false),aq,t.pos)::stack) args in
              log cfg  (fun () -> BU.print1 "\tPushed %s arguments\n" (string_of_int <| List.length args));
              norm cfg env stack head
  
            | Tm_refine(x, f) -> //non tail-recursive; the alternative is to keep marks on the stack to rebuild the term ... but that's very heavy
              if cfg.steps.weak
              then match env, stack with
                      | [], [] -> //TODO: Make this work in general!
                        let t_x = norm cfg env [] x.sort in
                        let t = mk (Tm_refine({x with sort=t_x}, f)) t.pos in
                        rebuild cfg env stack t
                      | _ -> rebuild cfg env stack (closure_as_term cfg env t)
              else let t_x = norm cfg env [] x.sort in
                   let closing, f = open_term [(x, None)] f in
                   let f = norm cfg (dummy::env) [] f in
                   let t = mk (Tm_refine({x with sort=t_x}, close closing f)) t.pos in
                   rebuild cfg env stack t
  
            | Tm_arrow(bs, c) ->
              if cfg.steps.weak
              then rebuild cfg env stack (closure_as_term cfg env t)
              else let bs, c = open_comp bs c in
                   let c = norm_comp cfg (bs |> List.fold_left (fun env _ -> dummy::env) env) c in
                   let t = arrow (norm_binders cfg env bs) c in
                   rebuild cfg env stack t
  
            | Tm_ascribed(t1, (tc, tacopt), l) when cfg.steps.unascribe ->
              norm cfg env stack t1
  
            | Tm_ascribed(t1, (tc, tacopt), l) ->
              begin match stack with
                | Match _ :: _
                | Arg _ :: _
                | App (_, {n=Tm_constant FC.Const_reify}, _, _) :: _
                | MemoLazy _ :: _ ->
                  log cfg  (fun () -> BU.print_string "+++ Dropping ascription \n");
                  norm cfg env stack t1 //ascriptions should not block reduction
                | _ ->
                  (* Drops stack *)
                  log cfg  (fun () -> BU.print_string "+++ Keeping ascription \n");
                  let t1 = norm cfg env [] t1 in
                  log cfg  (fun () -> BU.print_string "+++ Normalizing ascription \n");
                  let tc = match tc with
                      | Inl t -> Inl (norm cfg env [] t)
                      | Inr c -> Inr (norm_comp cfg env c) in
                  let tacopt = BU.map_opt tacopt (norm cfg env []) in
                  match stack with
                  | Cfg cfg :: stack ->
                    let t = mk (Tm_ascribed(U.unascribe t1, (tc, tacopt), l)) t.pos in
                    norm cfg env stack t
                  | _ ->
                    rebuild cfg env stack (mk (Tm_ascribed(U.unascribe t1, (tc, tacopt), l)) t.pos)
              end
  
            | Tm_match(head, branches) ->
              let stack = Match(env, branches, t.pos)::stack in
              norm cfg env stack head
  
            | Tm_let((b, lbs), lbody) when is_top_level lbs && cfg.steps.compress_uvars ->
              let lbs = lbs |> List.map (fun lb ->
                let openings, lbunivs = Subst.univ_var_opening lb.lbunivs in
                let cfg = { cfg with tcenv = Env.push_univ_vars cfg.tcenv lbunivs } in
                let norm t = Subst.close_univ_vars lbunivs (norm cfg env [] (Subst.subst openings t)) in
                let lbtyp = norm lb.lbtyp in
                let lbdef = norm lb.lbdef in
                { lb with lbunivs = lbunivs; lbtyp = lbtyp; lbdef = lbdef }
              ) in
  
              rebuild cfg env stack (mk (Tm_let ((b, lbs), lbody)) t.pos)
  
            | Tm_let((_, {lbname=Inr _}::_), _) -> //this is a top-level let binding; nothing to normalize
              rebuild cfg env stack t
  
            | Tm_let((false, [lb]), body) ->
              let n = TypeChecker.Env.norm_eff_name cfg.tcenv lb.lbeff in
              if not (cfg.steps.no_delta_steps) //we're allowed to do some delta steps, and ..
              && ((cfg.steps.pure_subterms_within_computations &&
                   U.has_attribute lb.lbattrs PC.inline_let_attr)        //1. we're extracting, and it's marked @inline_let
               || (U.is_pure_effect n && (cfg.normalize_pure_lets        //Or, 2. it's pure and we either not extracting, or
                                          || U.has_attribute lb.lbattrs PC.inline_let_attr)) //it's marked @inline_let
               || (U.is_ghost_effect n &&                                //Or, 3. it's ghost and we're not extracting
                      not (cfg.steps.pure_subterms_within_computations)))
              then let binder = S.mk_binder (BU.left lb.lbname) in
                   let env = (Some binder, Clos(env, lb.lbdef, BU.mk_ref None, false))::env in
                   log cfg (fun () -> BU.print_string "+++ Reducing Tm_let\n");
                   norm cfg env stack body
              else if cfg.steps.weak
              then (log cfg (fun () -> BU.print_string "+++ Not touching Tm_let\n");
                    rebuild cfg env stack (closure_as_term cfg env t))
              else let bs, body = Subst.open_term [lb.lbname |> BU.left |> S.mk_binder] body in
                   log cfg (fun () -> BU.print_string "+++ Normalizing Tm_let -- type");
                   let ty = norm cfg env [] lb.lbtyp in
                   let lbname =
                      let x = fst (List.hd bs) in
                      Inl ({x with sort=ty}) in
                   log cfg (fun () -> BU.print_string "+++ Normalizing Tm_let -- definiens\n");
                   let lb = {lb with lbname=lbname;
                                     lbtyp=ty;
                                     lbdef=norm cfg env [] lb.lbdef} in
                   let env' = bs |> List.fold_left (fun env _ -> dummy::env) env in
                   let stack = (Cfg cfg)::stack in
                   let cfg = { cfg with strong = true } in
                   log cfg (fun () -> BU.print_string "+++ Normalizing Tm_let -- body\n");
                   norm cfg env' (Let(env, bs, lb, t.pos)::stack) body
  
            | Tm_let((true, lbs), body)
                  when cfg.steps.compress_uvars
                    || ((not cfg.steps.zeta) &&
                        cfg.steps.pure_subterms_within_computations) -> //no fixpoint reduction allowed
              let lbs, body = Subst.open_let_rec lbs body in
              let lbs = List.map (fun lb ->
                  let ty = norm cfg env [] lb.lbtyp in
                  let lbname = Inl ({BU.left lb.lbname with sort=ty}) in
                  let xs, def_body, lopt = U.abs_formals lb.lbdef in
                  let xs = norm_binders cfg env xs in
                  let env = List.map (fun _ -> dummy) lbs
                          @ List.map (fun _ -> dummy) xs
                          @ env in
                  let def_body = norm cfg env [] def_body in
                  let lopt =
                    match lopt with
                    | Some rc -> Some ({rc with residual_typ=BU.map_opt rc.residual_typ (norm cfg env [])})
                    | _ -> lopt in
                  let def = U.abs xs def_body lopt in
                  { lb with lbname = lbname;
                            lbtyp = ty;
                            lbdef = def}) lbs in
              let env' = List.map (fun _ -> dummy) lbs @ env in
              let body = norm cfg env' [] body in
              let lbs, body = Subst.close_let_rec lbs body in
              let t = {t with n=Tm_let((true, lbs), body)} in
              rebuild cfg env stack t
  
            | Tm_let(lbs, body) when not cfg.steps.zeta -> //no fixpoint reduction allowed
              rebuild cfg env stack (closure_as_term cfg env t)
  
            | Tm_let(lbs, body) ->
              //let rec: The basic idea is to reduce the body in an environment that includes recursive bindings for the lbs
              //Consider reducing (let rec f x = f x in f 0) in initial environment env
              //We build two environments, rec_env and body_env and reduce (f 0) in body_env
              //rec_env = Clos(env, let rec f x = f x in f, memo)::env
              //body_env = Clos(rec_env, \x. f x, _)::env
              //i.e., in body, the bound variable is bound to definition, \x. f x
              //Within the definition \x.f x, f is bound to the recursive binding (let rec f x = f x in f), aka, fix f. \x. f x
              //Finally, we add one optimization for laziness by tying a knot in rec_env
              //i.e., we set memo := Some (rec_env, \x. f x)
  
              let rec_env, memos, _ = List.fold_right (fun lb (rec_env, memos, i) ->
                      let bv = {left lb.lbname with index=i} in
                      let f_i = Syntax.bv_to_tm bv in
                      let fix_f_i = mk (Tm_let(lbs, f_i)) t.pos in
                      let memo = BU.mk_ref None in
                      let rec_env = (None, Clos(env, fix_f_i, memo, true))::rec_env in
                      rec_env, memo::memos, i + 1) (snd lbs) (env, [], 0) in
              let _ = List.map2 (fun lb memo -> memo := Some (rec_env, lb.lbdef)) (snd lbs) memos in //tying the knot
              let body_env = List.fold_right (fun lb env -> (None, Clos(rec_env, lb.lbdef, BU.mk_ref None, false))::env)
                                 (snd lbs) env in
              norm cfg body_env stack body
  
            | Tm_meta (head, m) ->
              log cfg (fun () -> BU.print1 ">> metadata = %s\n" (Print.metadata_to_string m));
              begin match m with
                | Meta_monadic (m, t) ->
                  reduce_impure_comp cfg env stack head (Inl m) t
  
                | Meta_monadic_lift (m, m', t) ->
                  reduce_impure_comp cfg env stack head (Inr (m, m')) t
  
                | Meta_quoted (qt, inf) ->
                  rebuild cfg env stack t
  
                | _ ->
                  if cfg.steps.unmeta
                  then norm cfg env stack head
                  else begin match stack with
                    | _::_ ->
                      begin match m with
                        | Meta_labeled(l, r, _) ->
                          (* meta doesn't block reduction, but we need to put the label back *)
                          norm cfg env (Meta(m,r)::stack) head
  
                        | Meta_pattern args ->
                            let args = norm_pattern_args cfg env args in
                            norm cfg env (Meta(Meta_pattern args, t.pos)::stack) head //meta doesn't block reduction, but we need to put the label back
  
                        | _ ->
                            norm cfg env stack head //meta doesn't block reduction
                      end
                    | [] ->
                      let head = norm cfg env [] head in
                      let m = match m with
                          | Meta_pattern args ->
                              Meta_pattern (norm_pattern_args cfg env args)
                          | _ -> m in
                      let t = mk (Tm_meta(head, m)) t.pos in
                      rebuild cfg env stack t
                  end
          end //Tm_meta
  
          | Tm_delayed _ ->
            let t = SS.compress t in
            norm cfg env stack t
  
          | Tm_uvar _ ->
            let t = SS.compress t in
            match t.n with
            | Tm_uvar _ ->
              if cfg.steps.check_no_uvars
              then failwith (BU.format2 "(%s) CheckNoUvars: Unexpected unification variable remains: %s"
                                      (Range.string_of_range t.pos)
                                      (Print.term_to_string t))
              else rebuild cfg env stack t
  
            | _ ->
              norm cfg env stack t
  
  
  
  and do_unfold_fv cfg env stack (t0:term) (qninfo : qninfo) (f:fv) : term =
      //preserve the range info on the returned def
      let r_env = Env.set_range cfg.tcenv (S.range_of_fv f) in
      match Env.lookup_definition_qninfo cfg.delta_level f.fv_name.v qninfo with
         | None ->
           log cfg (fun () -> BU.print "Tm_fvar case 2\n" []) ;
           rebuild cfg env stack t0
  
         | Some (us, t) ->
           log cfg (fun () -> BU.print2 ">>> Unfolded %s to %s\n"
                         (Print.term_to_string t0) (Print.term_to_string t));
           let t =
             if cfg.steps.unfold_until = Some Delta_constant
              && not cfg.steps.unfold_tac
             //we're really trying to compute here; no point propagating range information
             //which can be expensive (except for tactics: it matters for tracing!)
             then t
             else Subst.set_use_range (Ident.range_of_lid f.fv_name.v) t
           in
           let n = List.length us in
           if n > 0
           then match stack with //universe beta reduction
                  | UnivArgs(us', _)::stack ->
                    let env = us' |> List.fold_left (fun env u -> (None, Univ u)::env) env in
                    norm cfg env stack t
                  | _ when cfg.steps.erase_universes || cfg.steps.allow_unbound_universes ->
                    norm cfg env stack t
                  | _ -> failwith (BU.format1 "Impossible: missing universe instantiation on %s" (Print.lid_to_string f.fv_name.v))
           else norm cfg env stack t
  
  and reduce_impure_comp cfg env stack (head : term) // monadic term
                                       (m : either<monad_name,(monad_name * monad_name)>)
                                          // relevant monads.
                                          // Inl m - this is a Meta_monadic with monad m
                                          // Inr (m, m') - this is a Meta_monadic_lift with monad m
                                       (t : typ) // annotated type in the Meta
                                       : term =
      (* We have an impure computation, and we aim to perform any pure      *)
      (* steps within that computation.                                     *)
  
      (* This scenario arises primarily as we extract (impure) programs and *)
      (* partially evaluate them before extraction, as an optimization.     *)
  
      (* First, we reduce **the type annotation** t with an empty stack (as *)
      (* it's not applied to anything)                                      *)
  
      (* Then, we reduce the monadic computation `head`, in a stack marked  *)
      (* with a Meta_monadic, indicating that this reduction should         *)
      (* not consume any arguments on the stack. `rebuild` will notice      *)
      (* the Meta_monadic marker and reconstruct the computation after      *)
      (* normalization.                                                     *)
      let t = norm cfg env [] t in
      let stack = (Cfg cfg)::stack in
      let cfg =
        if cfg.steps.pure_subterms_within_computations
        then
          let new_steps = [PureSubtermsWithinComputations;
                           Primops;
                           AllowUnboundUniverses;
                           EraseUniverses;
                           Exclude Zeta;
                           Inlining]
          in { cfg with
                 steps = List.fold_right fstep_add_one new_steps cfg.steps;
                 delta_level = [Env.Inlining; Env.Eager_unfolding_only]
             }
        else
          { cfg with steps = { cfg.steps with zeta = false } }
      in
      (* monadic annotations don't block reduction, but we need to put the label back *)
      let metadata = match m with
                     | Inl m -> Meta_monadic (m, t)
                     | Inr (m, m') -> Meta_monadic_lift (m, m', t)
      in
      norm cfg env (Meta(metadata, head.pos)::stack) head
  
  and do_reify_monadic fallback cfg env stack (head : term) (m : monad_name) (t : typ) : term =
      (* Precondition: the stack head is an App (reify, ...) *)
      let head0 = head in
      let head = U.unascribe head in
      log cfg (fun () -> BU.print2 "Reifying: (%s) %s\n" (Print.tag_of_term head) (Print.term_to_string head));
      let head = U.unmeta_safe head in
      match (SS.compress head).n with
      | Tm_let ((false, [lb]), body) ->
        (* ****************************************************************************)
        (* Monadic binding                                                            *)
        (*                                                                            *)
        (* This is reify (M.bind e1 (fun x -> e2)) which is elaborated to             *)
        (*                                                                            *)
        (*        M.bind_repr (reify e1) (fun x -> reify e2)                          *)
        (*                                                                            *)
        (* ****************************************************************************)
        let ed = Env.get_effect_decl cfg.tcenv (Env.norm_eff_name cfg.tcenv m) in
        let _, bind_repr = ed.bind_repr in
        begin match lb.lbname with
          | Inr _ -> failwith "Cannot reify a top-level let binding"
          | Inl x ->
  
            (* [is_return e] returns [Some e'] if [e] is a lift from Pure of [e'], [None] otherwise *)
            let is_return e =
              match (SS.compress e).n with
              | Tm_meta(e, Meta_monadic(_, _)) ->
                begin match (SS.compress e).n with
                  | Tm_meta(e, Meta_monadic_lift(_, msrc, _)) when U.is_pure_effect msrc ->
                      Some (SS.compress e)
                  | _ -> None
                end
             | _ -> None
            in
  
            match is_return lb.lbdef with
            (* We are in the case where [head] = [bind (return e) (fun x -> body)] *)
            (* which can be optimised to a non-monadic let-binding [let x = e in body] *)
            | Some e ->
              let lb = {lb with lbeff=PC.effect_PURE_lid; lbdef=e} in
              norm cfg env (List.tl stack) (S.mk (Tm_let((false, [lb]), U.mk_reify body)) None head.pos)
            | None ->
              if (match is_return body with Some ({n=Tm_bvar y}) -> S.bv_eq x y | _ -> false)
              then
                (* We are in the case where [head] = [bind e (fun x -> return x)] *)
                (* which can be optimised to just keeping normalizing [e] with a reify on the stack *)
                norm cfg env stack lb.lbdef
              else (
                (* TODO : optimize [bind (bind e1 e2) e3] into [bind e1 (bind e2 e3)] *)
                (* Rewriting binds in that direction would be better for exception-like monad *)
                (* since we wouldn't rematch on an already raised exception *)
                let rng = head.pos in
  
                let head = U.mk_reify <| lb.lbdef in
                let body = U.mk_reify <| body in
                (* TODO : Check that there is no sensible cflags to pass in the residual_comp *)
                let body_rc = {
                  residual_effect=m;
                  residual_flags=[];
                  residual_typ=Some t
                } in
                let body = S.mk (Tm_abs([S.mk_binder x], body, Some body_rc)) None body.pos in
                let close = closure_as_term cfg env in
                let bind_inst = match (SS.compress bind_repr).n with
                  | Tm_uinst (bind, [_ ; _]) ->
                      S.mk (Tm_uinst (bind, [ cfg.tcenv.universe_of cfg.tcenv (close lb.lbtyp)
                                            ; cfg.tcenv.universe_of cfg.tcenv (close t)]))
                      None rng
                  | _ -> failwith "NIY : Reification of indexed effects"
                in
                let maybe_range_arg =
                  if BU.for_some (U.attr_eq U.dm4f_bind_range_attr) ed.eff_attrs
                  then [as_arg (EMB.embed_range lb.lbpos lb.lbpos);
                        as_arg (EMB.embed_range body.pos body.pos)]
                  else []
                in
                let reified = S.mk (Tm_app(bind_inst, [
                    (* a, b *)
                    as_arg lb.lbtyp; as_arg t] @
                    maybe_range_arg @ [
                    (* wp_head, head--the term shouldn't depend on wp_head *)
                    as_arg S.tun; as_arg head;
                    (* wp_body, body--the term shouldn't depend on wp_body *)
                    as_arg S.tun; as_arg body]))
                  None rng
                in
                log cfg (fun () -> BU.print2 "Reified (1) <%s> to %s\n" (Print.term_to_string head0) (Print.term_to_string reified));
                norm cfg env (List.tl stack) reified
              )
        end
      | Tm_app (head_app, args) ->
          (* ****************************************************************************)
          (* Monadic application                                                        *)
          (*                                                                            *)
          (* The typechecker should have turned any monadic application into a serie of *)
          (* let-bindings (binding explicitly any monadic term)                         *)
          (*    let x0 = head in let x1 = arg0 in ... let xn = argn in x0 x1 ... xn     *)
          (*                                                                            *)
          (* which wil be ultimately reified to                                         *)
          (*     bind (reify head) (fun x0 ->                                           *)
          (*            bind (reify arg0) (fun x1 -> ... (fun xn -> x0 x1 .. xn) ))     *)
          (*                                                                            *)
          (* If head is an action then it is unfolded otherwise the                     *)
          (* resulting application is reified again                                     *)
          (* ****************************************************************************)
  
  
          let ed = Env.get_effect_decl cfg.tcenv (Env.norm_eff_name cfg.tcenv m) in
          let _, bind_repr = ed.bind_repr in
  
          (* [maybe_unfold_action head] test whether [head] is an action and tries to unfold it if it is *)
          let maybe_unfold_action head : term * option<bool> =
            let maybe_extract_fv t =
              let t = match (SS.compress t).n with
                | Tm_uinst (t, _) -> t
                | _ -> head
              in match (SS.compress t).n with
                | Tm_fvar x -> Some x
                | _ -> None
            in
            match maybe_extract_fv head with
            | Some x when Env.is_action cfg.tcenv (S.lid_of_fv x) ->
              (* Note that this is not a tail call, but it's a bounded (small) number of recursive steps *)
              let head = norm cfg env [] head in
              let action_unfolded = match maybe_extract_fv head with | Some _ -> Some true | _ -> Some false in
              head, action_unfolded
            | _ ->
              head, None
          in
  
          (* Checking that the typechecker did its job correctly and hoisted all impure *)
          (* terms to explicit let-bindings (see TcTerm, monadic_application) *)
          let _ =
            let is_arg_impure (e,q) =
              match (SS.compress e).n with
              | Tm_meta (e0, Meta_monadic_lift(m1, m2, t')) -> not (U.is_pure_effect m1)
              | _ -> false
            in
            if BU.for_some is_arg_impure ((as_arg head_app)::args)
            then failwith (BU.format1 "Incompability between typechecker and normalizer; \
                                       this monadic application contains impure terms %s\n"
                                      (Print.term_to_string head))
          in
  
          let head_app, found_action = maybe_unfold_action head_app in
          let mk tm = S.mk tm None head.pos in
          let body = mk (Tm_app(head_app, args)) in
          let body = match found_action with
            (* This is not an action let's just keep the reify marker *)
            | None -> U.mk_reify body
  
            (* The action was found but not unfolded (maybe abstract ?) *)
            | Some false -> mk (Tm_meta (body, Meta_monadic(m, t)))
  
            (* An action was found and successfully unfolded *)
            | Some true -> body
          in
          log cfg (fun () -> BU.print2 "Reified (2) <%s> to %s\n" (Print.term_to_string head0) (Print.term_to_string body));
          norm cfg env (List.tl stack) body
  
      // Doubly-annotated effect.. just take the outmost one. (unsure..)
      | Tm_meta(e, Meta_monadic _) ->
          do_reify_monadic fallback cfg env stack e m t
  
      | Tm_meta(e, Meta_monadic_lift (msrc, mtgt, t')) ->
          let lifted = reify_lift cfg e msrc mtgt (closure_as_term cfg env t') in
          log cfg (fun () -> BU.print1 "Reified lift to (2): %s\n" (Print.term_to_string lifted));
          norm cfg env (List.tl stack) lifted
  
      | Tm_match(e, branches) ->
        (* Commutation of reify with match, note that the scrutinee should never be effectful    *)
        (* (should be checked at typechecking and elaborated with an explicit binding if needed) *)
        (* reify (match e with p -> e') ~> match e with p -> reify e' *)
        let branches = branches |> List.map (fun (pat, wopt, tm) -> pat, wopt, U.mk_reify tm) in
        let tm = mk (Tm_match(e, branches)) head.pos in
        norm cfg env (List.tl stack) tm
  
      | _ ->
        fallback ()
  
  (* Reifies the lifting of the term [e] of type [t] from computational  *)
  (* effect [m] to computational effect [m'] using lifting data in [env] *)
  and reify_lift cfg e msrc mtgt t : term =
    let env = cfg.tcenv in
    log cfg (fun () -> BU.print3 "Reifying lift %s -> %s: %s\n"
          (Ident.string_of_lid msrc) (Ident.string_of_lid mtgt) (Print.term_to_string e));
    (* check if the lift is concrete, if so replace by its definition on terms *)
    (* if msrc is PURE or Tot we can use mtgt.return *)
    if U.is_pure_effect msrc || U.is_div_effect msrc
    then
      let ed = Env.get_effect_decl env (Env.norm_eff_name cfg.tcenv mtgt) in
      let _, return_repr = ed.return_repr in
      let return_inst = match (SS.compress return_repr).n with
          | Tm_uinst(return_tm, [_]) ->
              S.mk (Tm_uinst (return_tm, [env.universe_of env t])) None e.pos
          | _ -> failwith "NIY : Reification of indexed effects"
      in
      S.mk (Tm_app(return_inst, [as_arg t ; as_arg e])) None e.pos
    else
      match Env.monad_leq env msrc mtgt with
      | None ->
        failwith (BU.format2 "Impossible : trying to reify a lift between unrelated effects (%s and %s)"
                              (Ident.text_of_lid msrc)
                              (Ident.text_of_lid mtgt))
      | Some {mlift={mlift_term=None}} ->
        failwith (BU.format2 "Impossible : trying to reify a non-reifiable lift (from %s to %s)"
                              (Ident.text_of_lid msrc)
                              (Ident.text_of_lid mtgt))
      | Some {mlift={mlift_term=Some lift}} ->
        (* We don't have any reasonable wp to provide so we just pass unknow *)
        (* Usually the wp is only necessary to typecheck, so this should not *)
        (* create a big issue. *)
        lift (env.universe_of env t) t S.tun (U.mk_reify e)
        (* We still eagerly unfold the lift to make sure that the Unknown is not kept stuck on a folded application *)
        (* let cfg = *)
        (*   { steps=[Exclude Iota ; Exclude Zeta; Inlining ; Eager_unfolding ; UnfoldUntil Delta_constant]; *)
        (*     tcenv=env; *)
        (*     delta_level=[Env.Unfold Delta_constant ; Env.Eager_unfolding_only ; Env.Inlining ] } *)
        (* in *)
        (* norm cfg [] [] (lift t S.tun (U.mk_reify e)) *)
  
  and norm_pattern_args cfg env args =
      (* Drops stack *)
      args |> List.map (List.map (fun (a, imp) -> norm cfg env [] a, imp))
  
  and norm_comp : cfg -> env -> comp -> comp =
      fun cfg env comp ->
          match comp.n with
              | Total (t, uopt) ->
                {comp with n=Total (norm cfg env [] t, Option.map (norm_universe cfg env) uopt)}
  
              | GTotal (t, uopt) ->
                {comp with n=GTotal (norm cfg env [] t, Option.map (norm_universe cfg env) uopt)}
  
              | Comp ct ->
                let norm_args args = args |> List.map (fun (a, i) -> (norm cfg env [] a, i)) in
                let flags = ct.flags |> List.map (function DECREASES t -> DECREASES (norm cfg env [] t) | f -> f) in
                {comp with n=Comp ({ct with comp_univs=List.map (norm_universe cfg env) ct.comp_univs;
                                            result_typ=norm cfg env [] ct.result_typ;
                                            effect_args=norm_args ct.effect_args;
                                            flags=flags})}
  
  and norm_binder : cfg -> env -> binder -> binder =
      fun cfg env (x, imp) -> {x with sort=norm cfg env [] x.sort}, imp
  
  and norm_binders : cfg -> env -> binders -> binders =
      fun cfg env bs ->
          let nbs, _ = List.fold_left (fun (nbs', env) b ->
              let b = norm_binder cfg env b in
              (b::nbs', dummy::env) (* crossing a binder, so shift environment *))
              ([], env)
              bs in
          List.rev nbs
  
  and norm_lcomp_opt : cfg -> env -> option<residual_comp> -> option<residual_comp> =
      fun cfg env lopt ->
          match lopt with
          | Some rc ->
            let flags = filter_out_lcomp_cflags rc.residual_flags in
            Some ({rc with residual_typ=BU.map_opt rc.residual_typ (norm cfg env [])})
         | _ -> lopt
  
  and rebuild (cfg:cfg) (env:env) (stack:stack) (t:term) : term =
    (* Pre-condition: t is in either weak or strong normal form w.r.t env, depending on *)
  
negative.code:         | _ -> false
      in
      let simplify arg = (simp_t (fst arg), arg) in
      match is_quantified_true tm with
      (* We need to recurse, and maybe reduce further! *)
      | Some tm -> maybe_simplify_aux cfg env stack (norm cfg env [] tm)
      (* Otherwise try to simplify this point *)
      | None ->
      match (SS.compress tm).n with
      | Tm_app({n=Tm_uinst({n=Tm_fvar fv}, _)}, args)
      | Tm_app({n=Tm_fvar fv}, args) ->
  