Merge remote-tracking branch 'origin/master' into guido_refine

examples/bug-reports/Makefile

@@ -31,7 +31,8 @@ SHOULD_VERIFY_CLOSED=bug022.fst bug024.fst bug025.fst bug026.fst bug026b.fst bug
   Bug1502.fst \
   Bug1488.fst bug607.fst bug466.fst bug400.fst bug1470.fst bug1481.fst Bug1506.fst bug606.fst bug543.fst bug1521.fst \
   Bug1533.fst bug1535a.fst bug1535b.fst Bug1536.fst bug1370a.fst bug1370b.fst bug1534.fst bug575.fst \
-  bug1443a.fst bug1443b.fst bug1443c.fst bug1443d.fst bug1443e.fst bug1523.fst bug1141a.fst bug1141b.fst bug1141c.fst bug1141d.fst
+  bug1443a.fst bug1443b.fst bug1443c.fst bug1443d.fst bug1443e.fst bug1523.fst bug1141a.fst bug1141b.fst bug1141c.fst bug1141d.fst \
+  bug1561a.fst bug1561b.fst bug1065a.fst bug1065b.fst bug1065c.fst
 
 SHOULD_VERIFY_INTERFACE_CLOSED=bug771.fsti bug771b.fsti
 SHOULD_VERIFY_AND_WARN_CLOSED=bug016.fst

examples/bug-reports/bug1065a.fst

@@ -0,0 +1,10 @@
+module Bug1065a
+
+assume type mem
+
+let st_pre = st_pre_h mem
+let st_post' (a:Type) (pre:Type) = st_post_h' mem a pre
+
+assume val myStack : (a:Type) -> (pre:st_pre) -> (post: (m0:mem -> Tot (st_post' a (pre m0)))) -> Type0
+
+assume val gg : #a:Type -> #pre:(st_pre_h mem) -> #post:(mem -> Tot (st_post_h' mem a True)) -> myStack a pre post

examples/bug-reports/bug1065b.fst

@@ -0,0 +1,5 @@
+module Bug1065b
+
+assume val f : list (x:int{x>=0}) -> unit
+
+let test (x:list nat) = f x

examples/bug-reports/bug1065c.fst

@@ -0,0 +1,14 @@
+module Bug1065c
+
+assume val t : Type
+
+assume val proof : squash t
+
+#set-options "--no_smt"
+
+val ref : _:unit{t}
+let ref  = proof
+
+let id1 (x : (_:unit{t})) : squash t = x
+
+let id2 (x : squash t) : (_:unit{t}) = x

examples/bug-reports/bug1561a.fst

@@ -0,0 +1,9 @@
+module Bug1561a
+
+class validator_cls = {  bidon: nat  }
+
+type validator' (v : validator_cls) (k: nat) : Type0 = | C
+
+let validator [| cls: validator_cls |] k = validator' cls k
+
+let validate_nat [| d : validator_cls |] (p: bool) : Tot (validator 18) = C

examples/bug-reports/bug1561b.fst

@@ -0,0 +1,22 @@
+module Bug1561b
+
+class a = {x : bool}
+
+let t [| a |] : Tot Type = if x then ℤ else unit
+
+type u = | A | B
+
+let f_t [| _ : a |]  :  Tot Type = u → t → Tot t
+
+instance ii : a = { x = true }
+
+let f0 : f_t = fun l y → y
+
+(* used to explode with an assertion failure *)
+val test : unit -> unit
+let test () : unit =
+    let f : f_t = fun l y → y
+    in ()
+
+val f1 : f_t
+let f1 = fun l y → y

examples/typeclasses/EnumEq.fst

@@ -6,14 +6,7 @@ open FStar.Tactics.Typeclasses
 
 (* Trying out a "class morphism", a post-facto relation between two existing classes. *)
 instance enum_eq (#a:Type) (d : enum a) : deq a = {
-    (* Why the #d annotation? A tricky dependency causes the meta-arg
-     * annotation to vanish. First we solve that the type where this
-     * comparison occurs is (Enum.bounded (Mkenum?.max #a ?u)), then
-     * we solve both of the dictionaries here with ?u. So they *ARE*
-     * solved, and the meta-arg annotation is lost. What should happen,
-     * is that when we solve a meta-implicit with a uvar, the meta-annotation
-     * should be copied. (But what about the environment?) *)
-    eq    = (fun (x y : a) -> toInt #_ #d x = toInt y);
+    eq    = (fun (x y : a) -> toInt x = toInt y);
     eq_ok = (fun (x y : a) -> inv1 x; inv1 y);
 }
 

src/ocaml-output/FStar_Extraction_Kremlin.ml

@@ -804,8 +804,8 @@ let thd3 :
       -> 'Auu____4074
   = fun uu____4085  -> match uu____4085 with | (uu____4092,uu____4093,x) -> x 
 let (mk_width : Prims.string -> width FStar_Pervasives_Native.option) =
-  fun uu___281_4103  ->
-    match uu___281_4103 with
+  fun uu___280_4103  ->
+    match uu___280_4103 with
     | "UInt8" -> FStar_Pervasives_Native.Some UInt8
     | "UInt16" -> FStar_Pervasives_Native.Some UInt16
     | "UInt32" -> FStar_Pervasives_Native.Some UInt32
@@ -817,8 +817,8 @@ let (mk_width : Prims.string -> width FStar_Pervasives_Native.option) =
     | uu____4115 -> FStar_Pervasives_Native.None
 
 let (mk_bool_op : Prims.string -> op FStar_Pervasives_Native.option) =
-  fun uu___282_4125  ->
-    match uu___282_4125 with
+  fun uu___281_4125  ->
+    match uu___281_4125 with
     | "op_Negation" -> FStar_Pervasives_Native.Some Not
     | "op_AmpAmp" -> FStar_Pervasives_Native.Some And
     | "op_BarBar" -> FStar_Pervasives_Native.Some Or
@@ -829,8 +829,8 @@ let (mk_bool_op : Prims.string -> op FStar_Pervasives_Native.option) =
 let (is_bool_op : Prims.string -> Prims.bool) =
   fun op  -> (mk_bool_op op) <> FStar_Pervasives_Native.None 
 let (mk_op : Prims.string -> op FStar_Pervasives_Native.option) =
-  fun uu___283_4155  ->
-    match uu___283_4155 with
+  fun uu___282_4155  ->
+    match uu___282_4155 with
     | "add" -> FStar_Pervasives_Native.Some Add
     | "op_Plus_Hat" -> FStar_Pervasives_Native.Some Add
     | "add_underspec" -> FStar_Pervasives_Native.Some Add
@@ -904,21 +904,21 @@ let (empty : Prims.string Prims.list -> env) =
 let (extend : env -> Prims.string -> env) =
   fun env  ->
     fun x  ->
-      let uu___289_4356 = env  in
+      let uu___288_4356 = env  in
       {
         names = ({ pretty = x } :: (env.names));
-        names_t = (uu___289_4356.names_t);
-        module_name = (uu___289_4356.module_name)
+        names_t = (uu___288_4356.names_t);
+        module_name = (uu___288_4356.module_name)
       }
 
 let (extend_t : env -> Prims.string -> env) =
   fun env  ->
     fun x  ->
-      let uu___290_4370 = env  in
+      let uu___289_4370 = env  in
       {
-        names = (uu___290_4370.names);
+        names = (uu___289_4370.names);
         names_t = (x :: (env.names_t));
-        module_name = (uu___290_4370.module_name)
+        module_name = (uu___289_4370.module_name)
       }
 
 let (find_name : env -> Prims.string -> name) =
@@ -935,12 +935,12 @@ let (find : env -> Prims.string -> Prims.int) =
   fun env  ->
     fun x  ->
       try
-        (fun uu___292_4409  ->
+        (fun uu___291_4409  ->
            match () with
            | () -> FStar_List.index (fun name  -> name.pretty = x) env.names)
           ()
       with
-      | uu___291_4416 ->
+      | uu___290_4416 ->
           let uu____4418 =
             FStar_Util.format1 "Internal error: name not found %s\n" x  in
           failwith uu____4418
@@ -949,11 +949,11 @@ let (find_t : env -> Prims.string -> Prims.int) =
   fun env  ->
     fun x  ->
       try
-        (fun uu___294_4438  ->
+        (fun uu___293_4438  ->
            match () with
            | () -> FStar_List.index (fun name  -> name = x) env.names_t) ()
       with
-      | uu___293_4447 ->
+      | uu___292_4447 ->
           let uu____4449 =
             FStar_Util.format1 "Internal error: name not found %s\n" x  in
           failwith uu____4449
@@ -1002,7 +1002,7 @@ let rec (translate : FStar_Extraction_ML_Syntax.mllib -> file Prims.list) =
                    FStar_Extraction_ML_Syntax.string_of_mlpath path
                 in
              try
-               (fun uu___296_4856  ->
+               (fun uu___295_4856  ->
                   match () with
                   | () ->
                       (FStar_Util.print1
@@ -1045,8 +1045,8 @@ and (translate_flags :
   FStar_Extraction_ML_Syntax.meta Prims.list -> flag Prims.list) =
   fun flags1  ->
     FStar_List.choose
-      (fun uu___284_4937  ->
-         match uu___284_4937 with
+      (fun uu___283_4937  ->
+         match uu___283_4937 with
          | FStar_Extraction_ML_Syntax.Private  ->
              FStar_Pervasives_Native.Some Private
          | FStar_Extraction_ML_Syntax.NoExtract  ->
@@ -1078,8 +1078,8 @@ and (translate_cc :
   fun flags1  ->
     let uu____4952 =
       FStar_List.choose
-        (fun uu___285_4959  ->
-           match uu___285_4959 with
+        (fun uu___284_4959  ->
+           match uu___284_4959 with
            | FStar_Extraction_ML_Syntax.CCConv s ->
                FStar_Pervasives_Native.Some s
            | uu____4966 -> FStar_Pervasives_Native.None) flags1
@@ -1125,8 +1125,8 @@ and (translate_let :
             FStar_Extraction_ML_Syntax.mllb_meta = meta;
             FStar_Extraction_ML_Syntax.print_typ = uu____5030;_} when
             FStar_Util.for_some
-              (fun uu___286_5035  ->
-                 match uu___286_5035 with
+              (fun uu___285_5035  ->
+                 match uu___285_5035 with
                  | FStar_Extraction_ML_Syntax.Assumed  -> true
                  | uu____5038 -> false) meta
             ->
@@ -1172,8 +1172,8 @@ and (translate_let :
                    (fun env2  -> fun name1  -> extend_t env2 name1) env1
                    tvars
                   in
-               let rec find_return_type eff i uu___287_5172 =
-                 match uu___287_5172 with
+               let rec find_return_type eff i uu___286_5172 =
+                 match uu___286_5172 with
                  | FStar_Extraction_ML_Syntax.MLTY_Fun (uu____5181,eff1,t)
                      when i > (Prims.parse_int "0") ->
                      find_return_type eff1 (i - (Prims.parse_int "1")) t
@@ -1210,7 +1210,7 @@ and (translate_let :
                            MustDisappear :: uu____5249
                        | uu____5252 -> translate_flags meta  in
                      try
-                       (fun uu___298_5261  ->
+                       (fun uu___297_5261  ->
                           match () with
                           | () ->
                               let body1 = translate_expr env3 body  in
@@ -1262,7 +1262,7 @@ and (translate_let :
                let t1 = translate_type env1 t  in
                let name1 = ((env1.module_name), name)  in
                try
-                 (fun uu___300_5367  ->
+                 (fun uu___299_5367  ->
                     match () with
                     | () ->
                         let expr1 = translate_expr env1 expr  in
@@ -2685,8 +2685,8 @@ and (translate_width :
   (FStar_Const.signedness,FStar_Const.width) FStar_Pervasives_Native.tuple2
     FStar_Pervasives_Native.option -> width)
   =
-  fun uu___288_8222  ->
-    match uu___288_8222 with
+  fun uu___287_8222  ->
+    match uu___287_8222 with
     | FStar_Pervasives_Native.None  -> CInt
     | FStar_Pervasives_Native.Some (FStar_Const.Signed ,FStar_Const.Int8 ) ->
         Int8

src/ocaml-output/FStar_Extraction_ML_Code.ml

@@ -345,40 +345,40 @@ let (escape_or :
     FStar_BaseTypes.char -> Prims.string)
   =
   fun fallback  ->
-    fun uu___273_1710  ->
-      if uu___273_1710 = 92
+    fun uu___272_1710  ->
+      if uu___272_1710 = 92
       then "\\\\"
       else
-        if uu___273_1710 = 32
+        if uu___272_1710 = 32
         then " "
         else
-          if uu___273_1710 = 8
+          if uu___272_1710 = 8
           then "\\b"
           else
-            if uu___273_1710 = 9
+            if uu___272_1710 = 9
             then "\\t"
             else
-              if uu___273_1710 = 13
+              if uu___272_1710 = 13
               then "\\r"
               else
-                if uu___273_1710 = 10
+                if uu___272_1710 = 10
                 then "\\n"
                 else
-                  if uu___273_1710 = 39
+                  if uu___272_1710 = 39
                   then "\\'"
                   else
-                    if uu___273_1710 = 34
+                    if uu___272_1710 = 34
                     then "\\\""
                     else
-                      if FStar_Util.is_letter_or_digit uu___273_1710
-                      then FStar_Util.string_of_char uu___273_1710
+                      if FStar_Util.is_letter_or_digit uu___272_1710
+                      then FStar_Util.string_of_char uu___272_1710
                       else
-                        if FStar_Util.is_punctuation uu___273_1710
-                        then FStar_Util.string_of_char uu___273_1710
+                        if FStar_Util.is_punctuation uu___272_1710
+                        then FStar_Util.string_of_char uu___272_1710
                         else
-                          if FStar_Util.is_symbol uu___273_1710
-                          then FStar_Util.string_of_char uu___273_1710
-                          else fallback uu___273_1710
+                          if FStar_Util.is_symbol uu___272_1710
+                          then FStar_Util.string_of_char uu___272_1710
+                          else fallback uu___272_1710
 
 let (string_of_mlconstant :
   FStar_Extraction_ML_Syntax.mlconstant -> Prims.string) =