anchor.diff:  open Microsoft.FStar.Absyn.Util
   open Microsoft.FStar.Util
   
  -let constructors = Util.smap_create 100
  +let constructors = Util.smap_create 1000
   
   let nothing = 
  -    Util.smap_add constructors "Prims.op_Minus" (1, Some(function x::[] -> JSE_Minus(x) | _ -> failwith ""));
  -    Util.smap_add constructors "Prims.op_Negation" (1, Some(function x::[] -> JSE_Lnot(x) | _ -> failwith ""));
  -    Util.smap_add constructors "Prims.op_Addition" (2, Some(function x::y::[] -> JSE_Add(x,y) | _ -> failwith ""));
  -    Util.smap_add constructors "Prims.op_Subtraction" (2, Some(function x::y::[] -> JSE_Sub(x,y) | _ -> failwith ""));
  -    Util.smap_add constructors "Prims.op_Division" (2, Some(function x::y::[] -> JSE_Divide(x,y) | _ -> failwith ""));
  -    Util.smap_add constructors "Prims.op_Multiply" (2, Some(function x::y::[] -> JSE_Multiply(x,y) | _ -> failwith ""));
  -    Util.smap_add constructors "Prims.op_Modulus" (2, Some(function x::y::[] -> JSE_Mod(x,y) | _ -> failwith ""));
  -    Util.smap_add constructors "Prims.op_BarBar" (2, Some(function x::y::[] -> JSE_Lor(x,y) | _ -> failwith ""));
  -    Util.smap_add constructors "Prims.op_AmpAmp" (2, Some(function x::y::[] -> JSE_Land(x,y) | _ -> failwith ""));
  -    Util.smap_add constructors "Prims.op_GreaterThan" (2, Some(function x::y::[] -> JSE_Gt(x,y) | _ -> failwith ""));
  -    Util.smap_add constructors "Prims.op_LessThanOrEqual" (2, Some(function x::y::[] -> JSE_Le(x,y) | _ -> failwith ""));
  -    Util.smap_add constructors "Prims.op_LessThan" (2, Some(function x::y::[] -> JSE_Lt(x,y) | _ -> failwith ""));
  -    Util.smap_add constructors "Prims.op_GreaterThanOrEqual" (2, Some(function x::y::[] -> JSE_Ge(x,y) | _ -> failwith ""));
  -    Util.smap_add constructors "Prims.op_Equality" (2, Some(function x::y::[] -> JSE_Equal(JSE_Add(x,JSE_String("")),y) | _ -> failwith ""));
  -    Util.smap_add constructors "Prims.op_disEquality" (2, Some(function x::y::[] -> JSE_Lnot(JSE_Equal(JSE_Add(x,JSE_String("")),y)) | _ -> failwith ""));
  -    Util.smap_add constructors "String.strcat" (2, Some(function x::y::[] -> JSE_Add(x,y) | _ -> failwith ""));
  -    Util.smap_add constructors "Prims.fst" (1, Some(function x::[] -> JSE_Dot(x, "v[0]") | _ -> failwith ""));
  -    Util.smap_add constructors "Prims.snd" (1, Some(function x::[] -> JSE_Dot(x, "v[1]") | _ -> failwith ""));
  -    Util.smap_add constructors "Prims.op_ColonEquals" (2, Some(function x::y::[] -> JSE_Assign(x,y) | _ -> failwith ""));
  -    Util.smap_add constructors "Prims.MkTuple2" (2, None);
  -    Util.smap_add constructors "Prims.MkTuple3" (3, None);
  -    Util.smap_add constructors "Prims.MkTuple4" (4, None);
  -    Util.smap_add constructors "Prims.MkTuple5" (5, None);
  -    Util.smap_add constructors "Prims.MkTuple6" (6, None);
  -    Util.smap_add constructors "Prims.MkTuple7" (7, None);
  -    Util.smap_add constructors "Prims.MkTuple8" (8, None);
  -    Util.smap_add constructors "Prims.failwith" (1, Some(function x::[] -> JSE_Call(
  +    Util.smap_add constructors "Prims.op_Minus" (Some 1, Some(function x::[] -> JSE_Minus(x) | _ -> failwith ""));
  +    Util.smap_add constructors "Prims.op_Negation" (Some 1, Some(function x::[] -> JSE_Lnot(x) | _ -> failwith ""));
  +    Util.smap_add constructors "Prims.op_Addition" (Some 2, Some(function x::y::[] -> JSE_Add(x,y) | _ -> failwith ""));
  +    Util.smap_add constructors "Prims.op_Subtraction" (Some 2, Some(function x::y::[] -> JSE_Sub(x,y) | _ -> failwith ""));
  +    Util.smap_add constructors "Prims.op_Division" (Some 2, Some(function x::y::[] -> JSE_Divide(x,y) | _ -> failwith ""));
  +    Util.smap_add constructors "Prims.op_Multiply" (Some 2, Some(function x::y::[] -> JSE_Multiply(x,y) | _ -> failwith ""));
  +    Util.smap_add constructors "Prims.op_Modulus" (Some 2, Some(function x::y::[] -> JSE_Mod(x,y) | _ -> failwith ""));
  +    Util.smap_add constructors "Prims.op_BarBar" (Some 2, Some(function x::y::[] -> JSE_Lor(x,y) | _ -> failwith ""));
  +    Util.smap_add constructors "Prims.op_AmpAmp" (Some 2, Some(function x::y::[] -> JSE_Land(x,y) | _ -> failwith ""));
  +    Util.smap_add constructors "Prims.op_GreaterThan" (Some 2, Some(function x::y::[] -> JSE_Gt(x,y) | _ -> failwith ""));
  +    Util.smap_add constructors "Prims.op_LessThanOrEqual" (Some 2, Some(function x::y::[] -> JSE_Le(x,y) | _ -> failwith ""));
  +    Util.smap_add constructors "Prims.op_LessThan" (Some 2, Some(function x::y::[] -> JSE_Lt(x,y) | _ -> failwith ""));
  +    Util.smap_add constructors "Prims.op_GreaterThanOrEqual" (Some 2, Some(function x::y::[] -> JSE_Ge(x,y) | _ -> failwith ""));
  +    Util.smap_add constructors "Prims.op_Equality" (Some 2, Some(function x::y::[] -> JSE_Equal(JSE_Add(x,JSE_String("")),JSE_Add(y,JSE_String(""))) | _ -> failwith ""));
  +    Util.smap_add constructors "Prims.op_disEquality" (Some 2, Some(function x::y::[] -> JSE_Lnot(JSE_Equal(JSE_Add(x,JSE_String("")),JSE_Add(y,JSE_String("")))) | _ -> failwith ""));
  +    Util.smap_add constructors "String.strcat" (Some 2, Some(function x::y::[] -> JSE_Add(x,y) | _ -> failwith ""));
  +    Util.smap_add constructors "String.length" (Some 1, Some(function x::[] -> JSE_Dot(x,"length") | _ -> failwith ""));
  +    Util.smap_add constructors "Prims.fst" (Some 1, Some(function x::[] -> JSE_Dot(x, "v[0]") | _ -> failwith ""));
  +    Util.smap_add constructors "Prims.snd" (Some 1, Some(function x::[] -> JSE_Dot(x, "v[1]") | _ -> failwith ""));
  +    Util.smap_add constructors "Prims.op_ColonEquals" (Some 2, Some(function x::y::[] -> JSE_Assign(x,y) | _ -> failwith ""));
  +    Util.smap_add constructors "Prims.Nil" (None, None);
  +    Util.smap_add constructors "Prims.Cons" (None, None);
  +    Util.smap_add constructors "Prims.None" (None, None);
  +    Util.smap_add constructors "Prims.Some" (None, None);
  +    Util.smap_add constructors "Prims.MkTuple2" (None, None);
  +    Util.smap_add constructors "Prims.MkTuple3" (None, None);
  +    Util.smap_add constructors "Prims.MkTuple4" (None, None);
  +    Util.smap_add constructors "Prims.MkTuple5" (None, None);
  +    Util.smap_add constructors "Prims.MkTuple6" (None, None);
  +    Util.smap_add constructors "Prims.MkTuple7" (None, None);
  +    Util.smap_add constructors "Prims.MkTuple8" (None, None);
  +    Util.smap_add constructors "Prims.failwith" (Some 1, Some(function x::[] -> JSE_Call(
           JSE_Function(None,[],[JS_Statement(JSS_Throw(x))]),[]) | _ -> failwith ""));
       ()
   
  
positive.code:             ]))))]
          ))])))::fmods
      ), [])))]
  
  
  
  
negative.code:     | _ -> []
  
  let js_of_fstar (m:modul) : Ast.t =
      (JS_Statement(JSS_If(JSE_Lnot(JSE_Dot(JSE_This, m.name.str)), JSS_Expression(JSE_Assign(JSE_Identifier(m.name.str),JSE_Object([]))),None)))
          :: (List.map js_of_singl m.exports |> List.concat)
  
  let js_of_fstars (fmods : list<modul>) : Ast.t =
      let fmods = List.concat (List.map js_of_fstar fmods) in
      [JS_Statement(JSS_Expression(JSE_Call(JSE_Function(None, [],
          (JS_Statement(JSS_Declaration(["$C", Some(JSE_Function(None, ["t";"v"],
              [JS_Statement(JSS_Return(Some(JSE_Object([
                  JSP_Property("t", JSE_Identifier("t"));
  