search

FStarLang / FStar

A Proof-oriented Programming Language
https://fstar-lang.org
Apache License 2.0
2.68k stars 231 forks source link

Verification not supported for match with when clause #64

Open catalin-hritcu opened 9 years ago

catalin-hritcu commented 9 years ago

The following simple program:

  let f = function
  | 0 -> 0
  | n when (n>1) -> 1

produces the following error trace:

../../bin/fstar.exe --fstar_home ../.. bug64.fst --trace_error
Bound term variable not found: n
  at Microsoft.FStar.ToSMT.Encode.lookup_term_var[syntax`2,syntax`2] (Microsoft.FStar.ToSMT.env_t env, Microsoft.FStar.Absyn.withinfo_t`2 a) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_exp (Microsoft.FStar.Absyn.syntax`2 e, Microsoft.FStar.ToSMT.env_t env) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode+encode_args@771-1.Invoke (System.Tuple`2 tupledArg) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Core.OptimizedClosures+Adapt@3006[System.Tuple`3[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.Util+either`2[Microsoft.FStar.ToSMT.Term+term,Microsoft.FStar.ToSMT.Term+term]],Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[System.Tuple`2[System.String,Microsoft.FStar.ToSMT.Term+sort],Microsoft.FStar.ToSMT.Term+term]],Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+decl]],System.Tuple`2[Microsoft.FStar.Util+either`2[Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]],Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+exp',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]]]],System.Boolean],System.Tuple`3[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.Util+either`2[Microsoft.FStar.ToSMT.Term+term,Microsoft.FStar.ToSMT.Term+term]],Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[System.Tuple`2[System.String,Microsoft.FStar.ToSMT.Term+sort],Microsoft.FStar.ToSMT.Term+term]],Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+decl]]].Invoke (System.Tuple`3 , System.Tuple`2 ) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.loop@144-20[Tuple`2,Tuple`3] (Microsoft.FSharp.Core.FSharpFunc`3 f, System.Tuple`3 s, Microsoft.FSharp.Collections.FSharpList`1 xs) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.Fold[Tuple`2,Tuple`3] (Microsoft.FSharp.Core.FSharpFunc`2 folder, System.Tuple`3 state, Microsoft.FSharp.Collections.FSharpList`1 list) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_args (Microsoft.FSharp.Collections.FSharpList`1 l, Microsoft.FStar.ToSMT.env_t env) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_exp (Microsoft.FStar.Absyn.syntax`2 e, Microsoft.FStar.ToSMT.env_t env) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode+enc@827-2.Invoke (System.Tuple`2 x) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Core.FSharpFunc`2[System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[System.Tuple`2[System.String,Microsoft.FStar.ToSMT.Term+sort],Microsoft.FStar.ToSMT.Term+term]],Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+decl]],System.Tuple`2[Microsoft.FStar.Util+either`2[Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]],Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+exp',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]]]],System.Boolean]].InvokeFast[Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`2 func, System.Tuple`2 arg1, System.Tuple`2 arg2) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Util+fold@385-1[System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[System.Tuple`2[System.String,Microsoft.FStar.ToSMT.Term+sort],Microsoft.FStar.ToSMT.Term+term]],Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+decl]],System.Tuple`2[Microsoft.FStar.Util+either`2[Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]],Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+exp',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]]]],System.Boolean],Microsoft.FStar.ToSMT.Term+term].Invoke (System.Tuple`2 x) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Core.OptimizedClosures+Adapt@3006[System.Tuple`2[System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[System.Tuple`2[System.String,Microsoft.FStar.ToSMT.Term+sort],Microsoft.FStar.ToSMT.Term+term]],Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+decl]],Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+term]],System.Tuple`2[Microsoft.FStar.Util+either`2[Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]],Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+exp',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]]]],System.Boolean],System.Tuple`2[System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[System.Tuple`2[System.String,Microsoft.FStar.ToSMT.Term+sort],Microsoft.FStar.ToSMT.Term+term]],Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+decl]],Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+term]]].Invoke (System.Tuple`2 , System.Tuple`2 ) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.loop@144-20[Tuple`2,Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`3 f, System.Tuple`2 s, Microsoft.FSharp.Collections.FSharpList`1 xs) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.Fold[Tuple`2,Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`2 folder, System.Tuple`2 state, Microsoft.FSharp.Collections.FSharpList`1 list) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Util.fold_map[Tuple`2,Tuple`2,term] (Microsoft.FSharp.Core.FSharpFunc`2 f, System.Tuple`2 state, Microsoft.FSharp.Collections.FSharpList`1 s) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.enc@826 (Microsoft.FStar.ToSMT.env_t env, Microsoft.FSharp.Core.FSharpFunc`2 f, Microsoft.FSharp.Collections.FSharpList`1 l) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode+eq_op@849.Invoke (Microsoft.FSharp.Collections.FSharpList`1 _arg8) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_formula_with_labels (Microsoft.FStar.Absyn.syntax`2 phi, Microsoft.FStar.ToSMT.env_t env) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Primitives.Basics.List.map2ToFreshConsTail[Tuple`3,Boolean,Tuple`2] (Microsoft.FSharp.Collections.FSharpList`1 cons, Microsoft.FSharp.Core.FSharpFunc`3 f, Microsoft.FSharp.Collections.FSharpList`1 xs1, Microsoft.FSharp.Collections.FSharpList`1 xs2) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Primitives.Basics.List.map2[Boolean,Tuple`2,Tuple`3] (Microsoft.FSharp.Core.FSharpFunc`2 mapping, Microsoft.FSharp.Collections.FSharpList`1 xs1, Microsoft.FSharp.Collections.FSharpList`1 xs2) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.Map2[Boolean,Tuple`2,Tuple`3] (Microsoft.FSharp.Core.FSharpFunc`2 mapping, Microsoft.FSharp.Collections.FSharpList`1 list1, Microsoft.FSharp.Collections.FSharpList`1 list2) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode+enc_prop_c@833-1.Invoke (Microsoft.FSharp.Core.FSharpFunc`2 f, Microsoft.FSharp.Collections.FSharpList`1 l) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Core.OptimizedClosures+Invoke@3000[Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[Microsoft.FStar.Util+either`2[Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]],Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+exp',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]]]],System.Boolean]],System.Tuple`3[Microsoft.FStar.ToSMT.Term+term,Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[System.Tuple`2[System.String,Microsoft.FStar.ToSMT.Term+sort],System.String]],Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+decl]],Microsoft.FSharp.Core.FSharpFunc`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+term],Microsoft.FStar.ToSMT.Term+term]].Invoke (Microsoft.FSharp.Collections.FSharpList`1 u) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_formula_with_labels (Microsoft.FStar.Absyn.syntax`2 phi, Microsoft.FStar.ToSMT.env_t env) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Primitives.Basics.List.map2[Boolean,Tuple`2,Tuple`3] (Microsoft.FSharp.Core.FSharpFunc`2 mapping, Microsoft.FSharp.Collections.FSharpList`1 xs1, Microsoft.FSharp.Collections.FSharpList`1 xs2) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.Map2[Boolean,Tuple`2,Tuple`3] (Microsoft.FSharp.Core.FSharpFunc`2 mapping, Microsoft.FSharp.Collections.FSharpList`1 list1, Microsoft.FSharp.Collections.FSharpList`1 list2) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode+enc_prop_c@833-1.Invoke (Microsoft.FSharp.Core.FSharpFunc`2 f, Microsoft.FSharp.Collections.FSharpList`1 l) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Core.OptimizedClosures+Invoke@3000[Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[Microsoft.FStar.Util+either`2[Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]],Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+exp',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]]]],System.Boolean]],System.Tuple`3[Microsoft.FStar.ToSMT.Term+term,Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[System.Tuple`2[System.String,Microsoft.FStar.ToSMT.Term+sort],System.String]],Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+decl]],Microsoft.FSharp.Core.FSharpFunc`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+term],Microsoft.FStar.ToSMT.Term+term]].Invoke (Microsoft.FSharp.Collections.FSharpList`1 u) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_formula_with_labels (Microsoft.FStar.Absyn.syntax`2 phi, Microsoft.FStar.ToSMT.env_t env) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Primitives.Basics.List.map2ToFreshConsTail[Tuple`3,Boolean,Tuple`2] (Microsoft.FSharp.Collections.FSharpList`1 cons, Microsoft.FSharp.Core.FSharpFunc`3 f, Microsoft.FSharp.Collections.FSharpList`1 xs1, Microsoft.FSharp.Collections.FSharpList`1 xs2) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Primitives.Basics.List.map2[Boolean,Tuple`2,Tuple`3] (Microsoft.FSharp.Core.FSharpFunc`2 mapping, Microsoft.FSharp.Collections.FSharpList`1 xs1, Microsoft.FSharp.Collections.FSharpList`1 xs2) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.Map2[Boolean,Tuple`2,Tuple`3] (Microsoft.FSharp.Core.FSharpFunc`2 mapping, Microsoft.FSharp.Collections.FSharpList`1 list1, Microsoft.FSharp.Collections.FSharpList`1 list2) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode+enc_prop_c@833-1.Invoke (Microsoft.FSharp.Core.FSharpFunc`2 f, Microsoft.FSharp.Collections.FSharpList`1 l) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Core.OptimizedClosures+Invoke@3000[Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[Microsoft.FStar.Util+either`2[Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]],Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+exp',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]]]],System.Boolean]],System.Tuple`3[Microsoft.FStar.ToSMT.Term+term,Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[System.Tuple`2[System.String,Microsoft.FStar.ToSMT.Term+sort],System.String]],Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+decl]],Microsoft.FSharp.Core.FSharpFunc`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+term],Microsoft.FStar.ToSMT.Term+term]].Invoke (Microsoft.FSharp.Collections.FSharpList`1 u) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_formula_with_labels (Microsoft.FStar.Absyn.syntax`2 phi, Microsoft.FStar.ToSMT.env_t env) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Primitives.Basics.List.map2[Boolean,Tuple`2,Tuple`3] (Microsoft.FSharp.Core.FSharpFunc`2 mapping, Microsoft.FSharp.Collections.FSharpList`1 xs1, Microsoft.FSharp.Collections.FSharpList`1 xs2) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.Map2[Boolean,Tuple`2,Tuple`3] (Microsoft.FSharp.Core.FSharpFunc`2 mapping, Microsoft.FSharp.Collections.FSharpList`1 list1, Microsoft.FSharp.Collections.FSharpList`1 list2) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode+enc_prop_c@833-1.Invoke (Microsoft.FSharp.Core.FSharpFunc`2 f, Microsoft.FSharp.Collections.FSharpList`1 l) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Core.OptimizedClosures+Invoke@3000[Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[Microsoft.FStar.Util+either`2[Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]],Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+exp',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]]]],System.Boolean]],System.Tuple`3[Microsoft.FStar.ToSMT.Term+term,Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[System.Tuple`2[System.String,Microsoft.FStar.ToSMT.Term+sort],System.String]],Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+decl]],Microsoft.FSharp.Core.FSharpFunc`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+term],Microsoft.FStar.ToSMT.Term+term]].Invoke (Microsoft.FSharp.Collections.FSharpList`1 u) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_formula_with_labels (Microsoft.FStar.Absyn.syntax`2 phi, Microsoft.FStar.ToSMT.env_t env) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_q_body@908 (Microsoft.FStar.ToSMT.env_t env, Microsoft.FSharp.Collections.FSharpList`1 bs, Microsoft.FSharp.Collections.FSharpList`1 ps, Microsoft.FStar.Absyn.syntax`2 body) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_formula_with_labels (Microsoft.FStar.Absyn.syntax`2 phi, Microsoft.FStar.ToSMT.env_t env) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Primitives.Basics.List.map2[Boolean,Tuple`2,Tuple`3] (Microsoft.FSharp.Core.FSharpFunc`2 mapping, Microsoft.FSharp.Collections.FSharpList`1 xs1, Microsoft.FSharp.Collections.FSharpList`1 xs2) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.Map2[Boolean,Tuple`2,Tuple`3] (Microsoft.FSharp.Core.FSharpFunc`2 mapping, Microsoft.FSharp.Collections.FSharpList`1 list1, Microsoft.FSharp.Collections.FSharpList`1 list2) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode+enc_prop_c@833-1.Invoke (Microsoft.FSharp.Core.FSharpFunc`2 f, Microsoft.FSharp.Collections.FSharpList`1 l) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Core.OptimizedClosures+Invoke@3000[Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[Microsoft.FStar.Util+either`2[Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]],Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+exp',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]]]],System.Boolean]],System.Tuple`3[Microsoft.FStar.ToSMT.Term+term,Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[System.Tuple`2[System.String,Microsoft.FStar.ToSMT.Term+sort],System.String]],Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+decl]],Microsoft.FSharp.Core.FSharpFunc`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+term],Microsoft.FStar.ToSMT.Term+term]].Invoke (Microsoft.FSharp.Collections.FSharpList`1 u) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_formula_with_labels (Microsoft.FStar.Absyn.syntax`2 phi, Microsoft.FStar.ToSMT.env_t env) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.solve (Microsoft.FStar.Tc.env tcenv, Microsoft.FStar.Absyn.syntax`2 q) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode+solver@1566-5.Invoke (Microsoft.FStar.Tc.env tcenv, Microsoft.FStar.Absyn.syntax`2 q) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Core.FSharpFunc`2[Microsoft.FStar.Tc.Env+env,Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]]].InvokeFast[Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`2 func, Microsoft.FStar.Tc.env arg1, Microsoft.FStar.Absyn.syntax`2 arg2) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Util.try_discharge_guard (Microsoft.FStar.Tc.env env, Microsoft.FStar.Tc.guard_t g) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Util.discharge_guard (Microsoft.FStar.Tc.env env, Microsoft.FStar.Tc.guard_t g) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.tc_value (Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.syntax`2 e) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.tc_exp (Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.syntax`2 e) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.tc_exp (Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.syntax`2 e) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.tc_decl (Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.sigelt se, Boolean deserialized) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc+tc_decls@1426-1.Invoke (Microsoft.FStar.Absyn.sigelt se) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Core.OptimizedClosures+Adapt@3006[System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.Absyn.Syntax+sigelt],Microsoft.FStar.Tc.Env+env],Microsoft.FStar.Absyn.Syntax+sigelt,System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.Absyn.Syntax+sigelt],Microsoft.FStar.Tc.Env+env]].Invoke (System.Tuple`2 , Microsoft.FStar.Absyn.sigelt ) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.loop@144-20[sigelt,Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`3 f, System.Tuple`2 s, Microsoft.FSharp.Collections.FSharpList`1 xs) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.Fold[sigelt,Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`2 folder, System.Tuple`2 state, Microsoft.FSharp.Collections.FSharpList`1 list) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.tc_decls (Microsoft.FStar.Tc.env env, Microsoft.FSharp.Collections.FSharpList`1 ses, Boolean deserialized) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.tc_modul (Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.modul modul) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc+check_modules@1471-1.Invoke (Microsoft.FStar.Absyn.modul m) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Core.OptimizedClosures+Adapt@3006[System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.Absyn.Syntax+modul],Microsoft.FStar.Tc.Env+env],Microsoft.FStar.Absyn.Syntax+modul,System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.Absyn.Syntax+modul],Microsoft.FStar.Tc.Env+env]].Invoke (System.Tuple`2 , Microsoft.FStar.Absyn.modul ) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.loop@144-20[modul,Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`3 f, System.Tuple`2 s, Microsoft.FSharp.Collections.FSharpList`1 xs) [0x00000] in <filename unknown>:0 
  at Microsoft.FSharp.Collections.ListModule.Fold[modul,Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`2 folder, System.Tuple`2 state, Microsoft.FSharp.Collections.FSharpList`1 list) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.check_modules (Microsoft.FStar.Tc.solver_t s, Microsoft.FStar.Tc.solver_t ds, Microsoft.FSharp.Collections.FSharpList`1 mods) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.FStar.go$cont@55 (Microsoft.FSharp.Collections.FSharpList`1 filenames, Microsoft.FSharp.Core.Unit unitVar) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.FStar.go[Unit] (Microsoft.FSharp.Core.Unit _arg1) [0x00000] in <filename unknown>:0 
  at <StartupCode$fstar>.$Microsoft.FStar.FStar.main@ () [0x00000] in <filename unknown>:0
nikswamy commented 9 years ago

Rather than fixing this issue now, I have disabled when clauses for the moment, when --verify is set. Will resurrect them after the POPL tutorial.

catalin-hritcu commented 7 years ago

This feature is still missing, but the error message is much better:

When clauses are not yet supported in --verify mode; they will be some day