anchor.diff:                    norm cfg (c :: env) stack body 
   
                   | MemoLazy r :: stack -> 
  -                  set_memo r (env, t);
  +                  set_memo r (env, t); //TODO: fix! this doesn't always memoize the strong normal form
                     log (fun () -> Printf.printf "\tSet memo\n");
                     norm cfg env stack t
   
  
positive.code:               let t = mk (Tm_app(t, [(a,aq)])) r in 
                rebuild cfg env stack t
  
              | Match(env, branches) :: stack -> 
                failwith "NYI"
  
negative.code:         match t.n with 
            | Tm_delayed _ -> 
              failwith "Impossible"
  
            | Tm_name _ 
            | Tm_uinst _
            | Tm_constant _
            | Tm_type _
            | Tm_uvar _ 
            | Tm_unknown _ ->
              rebuild cfg env stack t
  
            | Tm_fvar(_, Some Data_ctor)
            | Tm_fvar(_, Some (Record_ctor _)) -> //these are just constructors; no delta steps can apply
              rebuild cfg env stack t
       
            | Tm_fvar (f, _) -> 
              if List.contains DeltaHard cfg.steps
              || (List.contains Delta cfg.steps && not (is_empty stack)) //delta only if reduction is blocked
              then match Env.lookup_definition cfg.tcenv f.v with 
                      | None -> rebuild cfg env stack t
                      | Some t -> norm cfg env stack t 
              else rebuild cfg env stack t     
  
            | Tm_bvar x -> 
              let c = try List.nth env x.index
  