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

Author: nikswamy

src/ml/FStarC_Parser_LexFStar.ml

@@ -54,7 +54,6 @@ let () =
   Hashtbl.add keywords "by"            BY          ;
   Hashtbl.add keywords "calc"          CALC        ;
   Hashtbl.add keywords "class"         CLASS       ;
-  Hashtbl.add keywords "default"       DEFAULT     ;
   Hashtbl.add keywords "decreases"     DECREASES   ;
   Hashtbl.add keywords "effect"        EFFECT      ;
   Hashtbl.add keywords "eliminate"     ELIM;

src/ml/FStarC_Parser_Parse.mly

@@ -115,7 +115,7 @@ type tc_constraint = {
 %token PRAGMA_SHOW_OPTIONS PRAGMA_SET_OPTIONS PRAGMA_RESET_OPTIONS PRAGMA_PUSH_OPTIONS PRAGMA_POP_OPTIONS PRAGMA_RESTART_SOLVER PRAGMA_PRINT_EFFECTS_GRAPH PRAGMA_CHECK
 %token TYP_APP_LESS TYP_APP_GREATER SUBTYPE EQUALTYPE SUBKIND BY
 %token AND ASSERT SYNTH BEGIN ELSE END
-%token EXCEPTION FALSE FUN FUNCTION IF IN MODULE DEFAULT
+%token EXCEPTION FALSE FUN FUNCTION IF IN MODULE
 %token MATCH OF
 %token FRIEND OPEN REC THEN TRUE TRY TYPE CALC CLASS INSTANCE EFFECT VAL
 %token INTRO ELIM
@@ -640,7 +640,6 @@ qualifier:
   }
   | IRREDUCIBLE   { Irreducible }
   | NOEXTRACT     { NoExtract }
-  | DEFAULT       { DefaultEffect }
   | TOTAL         { TotalEffect }
   | PRIVATE       { Private }
 

src/ml/FStarC_Parser_ParseIt.ml

@@ -358,7 +358,6 @@ let string_of_token =
   | IF -> "IF"
   | IN -> "IN"
   | MODULE -> "MODULE"
-  | DEFAULT -> "DEFAULT"
   | MATCH -> "MATCH"
   | OF -> "OF"
   | FRIEND -> "FRIEND"

src/parser/FStarC.Parser.AST.Diff.fst

@@ -465,7 +465,6 @@ let eq_qualifier (t1 t2: qualifier) =
   | Noeq, Noeq -> true
   | Unopteq, Unopteq -> true
   | Assumption, Assumption -> true
-  | DefaultEffect, DefaultEffect -> true
   | TotalEffect, TotalEffect -> true
   | Effect_qual, Effect_qual -> true
   | New, New -> true

src/parser/FStarC.Parser.AST.fsti

@@ -192,7 +192,6 @@ type qualifier =
   | Noeq
   | Unopteq
   | Assumption
-  | DefaultEffect
   | TotalEffect
   | Effect_qual
   | New

src/parser/FStarC.Parser.ToDocument.fst

@@ -1046,7 +1046,6 @@ and p_qualifier = function
   | Noeq -> str "noeq"
   | Unopteq -> str "unopteq"
   | Assumption -> str "assume"
-  | DefaultEffect -> str "default"
   | TotalEffect -> str "total"
   | Effect_qual -> empty
   | New -> str "new"

src/tosyntax/FStarC.ToSyntax.ToSyntax.fst

@@ -166,7 +166,6 @@ let trans_qual (r:Range.t) maybe_effect_id = function
   | AST.Reifiable ->     S.Reifiable
   | AST.Noeq ->          S.Noeq
   | AST.Unopteq ->       S.Unopteq
-  | AST.DefaultEffect -> raise_error r Errors.Fatal_DefaultQualifierNotAllowedOnEffects "The 'default' qualifier on effects is no longer supported"
   | AST.Inline
   | AST.Visible ->
     raise_error r Errors.Fatal_UnsupportedQualifier "Unsupported qualifier"