diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml b/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml index 113de7287c7..2c35af96712 100644 --- a/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml +++ b/ocaml/fstar-lib/generated/FStar_Extraction_Krml.ml @@ -1077,71 +1077,59 @@ let rec (translate_type_without_decay' : let uu___2 = translate_type_without_decay env1 arg in TBuf uu___2 | FStar_Extraction_ML_Syntax.MLTY_Named (arg::[], p) when (let uu___ = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___ = "LowStar.ConstBuffer.const_buffer") || - (let uu___ = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___ = "Steel.TLArray.t") + uu___ = "LowStar.ConstBuffer.const_buffer") || false -> let uu___ = translate_type_without_decay env1 arg in TConstBuf uu___ | FStar_Extraction_ML_Syntax.MLTY_Named (arg::[], p) when - ((((((((((((((((let uu___ = - FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___ = "FStar.Buffer.buffer") || - (let uu___ = - FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___ = "LowStar.Buffer.buffer")) - || - (let uu___ = - FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___ = "LowStar.ImmutableBuffer.ibuffer")) - || + ((((((((((((((let uu___ = + FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___ = "FStar.Buffer.buffer") || (let uu___ = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___ = "LowStar.UninitializedBuffer.ubuffer")) + uu___ = "LowStar.Buffer.buffer")) || (let uu___ = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___ = "FStar.HyperStack.reference")) + uu___ = "LowStar.ImmutableBuffer.ibuffer")) || (let uu___ = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___ = "FStar.HyperStack.stackref")) + uu___ = "LowStar.UninitializedBuffer.ubuffer")) || (let uu___ = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___ = "FStar.HyperStack.ref")) + uu___ = "FStar.HyperStack.reference")) || (let uu___ = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___ = "FStar.HyperStack.mmstackref")) + uu___ = "FStar.HyperStack.stackref")) || (let uu___ = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___ = "FStar.HyperStack.mmref")) + uu___ = "FStar.HyperStack.ref")) || (let uu___ = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___ = "FStar.HyperStack.ST.reference")) + uu___ = "FStar.HyperStack.mmstackref")) || (let uu___ = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___ = "FStar.HyperStack.ST.stackref")) + uu___ = "FStar.HyperStack.mmref")) || (let uu___ = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___ = "FStar.HyperStack.ST.ref")) + uu___ = "FStar.HyperStack.ST.reference")) || (let uu___ = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___ = "FStar.HyperStack.ST.mmstackref")) + uu___ = "FStar.HyperStack.ST.stackref")) || (let uu___ = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___ = "FStar.HyperStack.ST.mmref")) + uu___ = "FStar.HyperStack.ST.ref")) || (let uu___ = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___ = "Steel.Reference.ref")) + uu___ = "FStar.HyperStack.ST.mmstackref")) || (let uu___ = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___ = "Steel.ST.Reference.ref")) - || - (let uu___ = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___ = "Steel.ST.HigherArray.ptr") + uu___ = "FStar.HyperStack.ST.mmref")) + || false -> let uu___ = translate_type_without_decay env1 arg in TBuf uu___ | FStar_Extraction_ML_Syntax.MLTY_Named (uu___::arg::[], p) when (let uu___1 = FStar_Extraction_ML_Syntax.string_of_mlpath p in @@ -1244,42 +1232,6 @@ and (translate_expr' : env -> FStar_Extraction_ML_Syntax.mlexpr -> expr) = let uu___2 = translate_branches env1 branches1 in (uu___1, uu___2) in EMatch uu___ - | FStar_Extraction_ML_Syntax.MLE_App - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_TApp - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Name p; - FStar_Extraction_ML_Syntax.mlty = uu___; - FStar_Extraction_ML_Syntax.loc = uu___1;_}, - t::[]); - FStar_Extraction_ML_Syntax.mlty = uu___2; - FStar_Extraction_ML_Syntax.loc = uu___3;_}, - uu___4) - when - let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "Steel.ST.HigherArray.null_ptr" -> - let uu___5 = translate_type env1 t in EBufNull uu___5 - | FStar_Extraction_ML_Syntax.MLE_App - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_TApp - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Name p; - FStar_Extraction_ML_Syntax.mlty = uu___; - FStar_Extraction_ML_Syntax.loc = uu___1;_}, - t::[]); - FStar_Extraction_ML_Syntax.mlty = uu___2; - FStar_Extraction_ML_Syntax.loc = uu___3;_}, - arg::[]) - when - let uu___4 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___4 = "Steel.ST.HigherArray.is_null_ptr" -> - let uu___4 = translate_type env1 t in - let uu___5 = translate_expr env1 arg in - generate_is_null uu___4 uu___5 | FStar_Extraction_ML_Syntax.MLE_App ({ FStar_Extraction_ML_Syntax.expr = @@ -1398,26 +1350,6 @@ and (translate_expr' : env -> FStar_Extraction_ML_Syntax.mlexpr -> expr) = (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in uu___5 = "LowStar.ToFStarBuffer.old_to_new_st") -> translate_expr env1 e1 - | FStar_Extraction_ML_Syntax.MLE_App - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_TApp - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Name p; - FStar_Extraction_ML_Syntax.mlty = uu___; - FStar_Extraction_ML_Syntax.loc = uu___1;_}, - uu___2); - FStar_Extraction_ML_Syntax.mlty = uu___3; - FStar_Extraction_ML_Syntax.loc = uu___4;_}, - _perm0::_perm1::_seq0::_seq1::e0::_len0::e1::_len1::[]) - when - let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "Steel.ST.HigherArray.ptrdiff_ptr" -> - let uu___5 = - let uu___6 = translate_expr env1 e0 in - let uu___7 = translate_expr env1 e1 in (uu___6, uu___7) in - EBufDiff uu___5 | FStar_Extraction_ML_Syntax.MLE_App ({ FStar_Extraction_ML_Syntax.expr = @@ -1432,47 +1364,24 @@ and (translate_expr' : env -> FStar_Extraction_ML_Syntax.mlexpr -> expr) = FStar_Extraction_ML_Syntax.loc = uu___4;_}, e1::e2::[]) when - (((((let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "FStar.Buffer.index") || - (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "FStar.Buffer.op_Array_Access")) - || + ((((let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___5 = "FStar.Buffer.index") || (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "LowStar.Monotonic.Buffer.index")) + uu___5 = "FStar.Buffer.op_Array_Access")) || (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "LowStar.UninitializedBuffer.uindex")) + uu___5 = "LowStar.Monotonic.Buffer.index")) || (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "LowStar.ConstBuffer.index")) + uu___5 = "LowStar.UninitializedBuffer.uindex")) || (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "Steel.TLArray.get") + uu___5 = "LowStar.ConstBuffer.index") -> let uu___5 = let uu___6 = translate_expr env1 e1 in let uu___7 = translate_expr env1 e2 in (uu___6, uu___7) in EBufRead uu___5 - | FStar_Extraction_ML_Syntax.MLE_App - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_TApp - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Name p; - FStar_Extraction_ML_Syntax.mlty = uu___; - FStar_Extraction_ML_Syntax.loc = uu___1;_}, - uu___2); - FStar_Extraction_ML_Syntax.mlty = uu___3; - FStar_Extraction_ML_Syntax.loc = uu___4;_}, - _perm::e1::_len::_seq::e2::[]) - when - let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "Steel.ST.HigherArray.index_ptr" -> - let uu___5 = - let uu___6 = translate_expr env1 e1 in - let uu___7 = translate_expr env1 e2 in (uu___6, uu___7) in - EBufRead uu___5 | FStar_Extraction_ML_Syntax.MLE_App ({ FStar_Extraction_ML_Syntax.expr = @@ -1487,31 +1396,8 @@ and (translate_expr' : env -> FStar_Extraction_ML_Syntax.mlexpr -> expr) = FStar_Extraction_ML_Syntax.loc = uu___4;_}, e1::[]) when - (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "FStar.HyperStack.ST.op_Bang") || - (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "Steel.Reference.read") - -> - let uu___5 = - let uu___6 = translate_expr env1 e1 in - (uu___6, (EQualified (["C"], "_zero_for_deref"))) in - EBufRead uu___5 - | FStar_Extraction_ML_Syntax.MLE_App - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_TApp - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Name p; - FStar_Extraction_ML_Syntax.mlty = uu___; - FStar_Extraction_ML_Syntax.loc = uu___1;_}, - uu___2); - FStar_Extraction_ML_Syntax.mlty = uu___3; - FStar_Extraction_ML_Syntax.loc = uu___4;_}, - _perm::_v::e1::[]) - when let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "Steel.ST.Reference.read" -> + uu___5 = "FStar.HyperStack.ST.op_Bang" -> let uu___5 = let uu___6 = translate_expr env1 e1 in (uu___6, (EQualified (["C"], "_zero_for_deref"))) in @@ -1608,9 +1494,7 @@ and (translate_expr' : env -> FStar_Extraction_ML_Syntax.mlexpr -> expr) = init::[]) when (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "FStar.HyperStack.ST.salloc") || - (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "Steel.ST.Reference._alloca") + uu___5 = "FStar.HyperStack.ST.salloc") || false -> let uu___5 = let uu___6 = translate_expr env1 init in @@ -1793,29 +1677,6 @@ and (translate_expr' : env -> FStar_Extraction_ML_Syntax.mlexpr -> expr) = let uu___6 = translate_expr env1 init in (ManuallyManaged, uu___6, (EConstant (UInt32, "1"))) in EBufCreate uu___5 - | FStar_Extraction_ML_Syntax.MLE_App - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_TApp - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Name p; - FStar_Extraction_ML_Syntax.mlty = uu___; - FStar_Extraction_ML_Syntax.loc = uu___1;_}, - uu___2); - FStar_Extraction_ML_Syntax.mlty = uu___3; - FStar_Extraction_ML_Syntax.loc = uu___4;_}, - init::[]) - when - (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "Steel.Reference.malloc") || - (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "Steel.ST.Reference.alloc") - -> - let uu___5 = - let uu___6 = translate_expr env1 init in - (ManuallyManaged, uu___6, (EConstant (UInt32, "1"))) in - EBufCreate uu___5 | FStar_Extraction_ML_Syntax.MLE_App ({ FStar_Extraction_ML_Syntax.expr = @@ -1846,27 +1707,6 @@ and (translate_expr' : env -> FStar_Extraction_ML_Syntax.mlexpr -> expr) = let uu___7 = translate_expr env1 e2 in (ManuallyManaged, uu___6, uu___7) in EBufCreate uu___5 - | FStar_Extraction_ML_Syntax.MLE_App - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_TApp - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Name p; - FStar_Extraction_ML_Syntax.mlty = uu___; - FStar_Extraction_ML_Syntax.loc = uu___1;_}, - uu___2); - FStar_Extraction_ML_Syntax.mlty = uu___3; - FStar_Extraction_ML_Syntax.loc = uu___4;_}, - e0::e1::[]) - when - let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "Steel.ST.HigherArray.malloc_ptr" -> - let uu___5 = - let uu___6 = translate_expr env1 e0 in - let uu___7 = translate_expr env1 e1 in - (ManuallyManaged, uu___6, uu___7) in - EBufCreate uu___5 | FStar_Extraction_ML_Syntax.MLE_App ({ FStar_Extraction_ML_Syntax.expr = @@ -1902,28 +1742,7 @@ and (translate_expr' : env -> FStar_Extraction_ML_Syntax.mlexpr -> expr) = e2::[]) when (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "FStar.HyperStack.ST.rfree") || - (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "Steel.Reference.free") - -> let uu___5 = translate_expr env1 e2 in EBufFree uu___5 - | FStar_Extraction_ML_Syntax.MLE_App - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_TApp - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Name p; - FStar_Extraction_ML_Syntax.mlty = uu___; - FStar_Extraction_ML_Syntax.loc = uu___1;_}, - uu___2); - FStar_Extraction_ML_Syntax.mlty = uu___3; - FStar_Extraction_ML_Syntax.loc = uu___4;_}, - _v::e2::[]) - when - (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "Steel.ST.HigherArray.free_ptr") || - (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "Steel.ST.Reference.free") + uu___5 = "FStar.HyperStack.ST.rfree") || false -> let uu___5 = translate_expr env1 e2 in EBufFree uu___5 | FStar_Extraction_ML_Syntax.MLE_App ({ @@ -2017,11 +1836,8 @@ and (translate_expr' : env -> FStar_Extraction_ML_Syntax.mlexpr -> expr) = FStar_Extraction_ML_Syntax.loc = uu___4;_}, e1::e2::[]) when - (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "FStar.Buffer.offset") || - (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "Steel.ST.HigherArray.ptr_shift") - -> + let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___5 = "FStar.Buffer.offset" -> let uu___5 = let uu___6 = translate_expr env1 e1 in let uu___7 = translate_expr env1 e2 in (uu___6, uu___7) in @@ -2076,27 +1892,6 @@ and (translate_expr' : env -> FStar_Extraction_ML_Syntax.mlexpr -> expr) = let uu___7 = translate_expr env1 e2 in let uu___8 = translate_expr env1 e3 in (uu___6, uu___7, uu___8) in EBufWrite uu___5 - | FStar_Extraction_ML_Syntax.MLE_App - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_TApp - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Name p; - FStar_Extraction_ML_Syntax.mlty = uu___; - FStar_Extraction_ML_Syntax.loc = uu___1;_}, - uu___2); - FStar_Extraction_ML_Syntax.mlty = uu___3; - FStar_Extraction_ML_Syntax.loc = uu___4;_}, - e1::_len::_s::e2::e3::[]) - when - let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "Steel.ST.HigherArray.upd_ptr" -> - let uu___5 = - let uu___6 = translate_expr env1 e1 in - let uu___7 = translate_expr env1 e2 in - let uu___8 = translate_expr env1 e3 in (uu___6, uu___7, uu___8) in - EBufWrite uu___5 | FStar_Extraction_ML_Syntax.MLE_App ({ FStar_Extraction_ML_Syntax.expr = @@ -2111,32 +1906,8 @@ and (translate_expr' : env -> FStar_Extraction_ML_Syntax.mlexpr -> expr) = FStar_Extraction_ML_Syntax.loc = uu___4;_}, e1::e2::[]) when - (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "FStar.HyperStack.ST.op_Colon_Equals") || - (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "Steel.Reference.write") - -> - let uu___5 = - let uu___6 = translate_expr env1 e1 in - let uu___7 = translate_expr env1 e2 in - (uu___6, (EQualified (["C"], "_zero_for_deref")), uu___7) in - EBufWrite uu___5 - | FStar_Extraction_ML_Syntax.MLE_App - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_TApp - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Name p; - FStar_Extraction_ML_Syntax.mlty = uu___; - FStar_Extraction_ML_Syntax.loc = uu___1;_}, - uu___2); - FStar_Extraction_ML_Syntax.mlty = uu___3; - FStar_Extraction_ML_Syntax.loc = uu___4;_}, - _v::e1::e2::[]) - when let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "Steel.ST.Reference.write" -> + uu___5 = "FStar.HyperStack.ST.op_Colon_Equals" -> let uu___5 = let uu___6 = translate_expr env1 e1 in let uu___7 = translate_expr env1 e2 in @@ -2151,9 +1922,7 @@ and (translate_expr' : env -> FStar_Extraction_ML_Syntax.mlexpr -> expr) = uu___2::[]) when (let uu___3 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___3 = "FStar.HyperStack.ST.push_frame") || - (let uu___3 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___3 = "Steel.ST.Reference._push_frame") + uu___3 = "FStar.HyperStack.ST.push_frame") || false -> EPushFrame | FStar_Extraction_ML_Syntax.MLE_App ({ @@ -2165,22 +1934,6 @@ and (translate_expr' : env -> FStar_Extraction_ML_Syntax.mlexpr -> expr) = when let uu___3 = FStar_Extraction_ML_Syntax.string_of_mlpath p in uu___3 = "FStar.HyperStack.ST.pop_frame" -> EPopFrame - | FStar_Extraction_ML_Syntax.MLE_App - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_TApp - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Name p; - FStar_Extraction_ML_Syntax.mlty = uu___; - FStar_Extraction_ML_Syntax.loc = uu___1;_}, - uu___2); - FStar_Extraction_ML_Syntax.mlty = uu___3; - FStar_Extraction_ML_Syntax.loc = uu___4;_}, - uu___5::uu___6::[]) - when - let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___7 = "Steel.ST.Reference._free_and_pop_frame" -> EPopFrame | FStar_Extraction_ML_Syntax.MLE_App ({ FStar_Extraction_ML_Syntax.expr = @@ -2211,30 +1964,6 @@ and (translate_expr' : env -> FStar_Extraction_ML_Syntax.mlexpr -> expr) = let uu___10 = translate_expr env1 e5 in (uu___6, uu___7, uu___8, uu___9, uu___10) in EBufBlit uu___5 - | FStar_Extraction_ML_Syntax.MLE_App - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_TApp - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Name p; - FStar_Extraction_ML_Syntax.mlty = uu___; - FStar_Extraction_ML_Syntax.loc = uu___1;_}, - uu___2); - FStar_Extraction_ML_Syntax.mlty = uu___3; - FStar_Extraction_ML_Syntax.loc = uu___4;_}, - uu___5::uu___6::uu___7::e1::uu___8::e2::e3::uu___9::e4::e5::[]) - when - let uu___10 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___10 = "Steel.ST.HigherArray.blit_ptr" -> - let uu___10 = - let uu___11 = translate_expr env1 e1 in - let uu___12 = translate_expr env1 e2 in - let uu___13 = translate_expr env1 e3 in - let uu___14 = translate_expr env1 e4 in - let uu___15 = translate_expr env1 e5 in - (uu___11, uu___12, uu___13, uu___14, uu___15) in - EBufBlit uu___10 | FStar_Extraction_ML_Syntax.MLE_App ({ FStar_Extraction_ML_Syntax.expr = @@ -2669,22 +2398,6 @@ and (translate_expr' : env -> FStar_Extraction_ML_Syntax.mlexpr -> expr) = ((EQualified (["FStar"; "Int"; "Cast"], c)), uu___11) in EApp uu___10) - | FStar_Extraction_ML_Syntax.MLE_App - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_TApp - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Name p; - FStar_Extraction_ML_Syntax.mlty = uu___; - FStar_Extraction_ML_Syntax.loc = uu___1;_}, - uu___2); - FStar_Extraction_ML_Syntax.mlty = uu___3; - FStar_Extraction_ML_Syntax.loc = uu___4;_}, - uu___5::uu___6::e1::[]) - when - let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___7 = "Steel.Effect.Atomic.return" -> translate_expr env1 e1 | FStar_Extraction_ML_Syntax.MLE_App ({ FStar_Extraction_ML_Syntax.expr = @@ -2720,116 +2433,6 @@ and (translate_expr' : env -> FStar_Extraction_ML_Syntax.mlexpr -> expr) = let uu___2 = let uu___3 = translate_expr env1 arg in (uu___3, (TInt UInt32)) in ECast uu___2 - | FStar_Extraction_ML_Syntax.MLE_App - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Name p; - FStar_Extraction_ML_Syntax.mlty = uu___; - FStar_Extraction_ML_Syntax.loc = uu___1;_}, - _inv::test::body::[]) - when - let uu___2 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___2 = "Steel.ST.Loops.while_loop" -> - let uu___2 = - let uu___3 = - let uu___4 = - let uu___5 = translate_expr env1 test in - let uu___6 = - let uu___7 = translate_expr env1 body in [uu___7] in - uu___5 :: uu___6 in - EUnit :: uu___4 in - ((EQualified (["Steel"; "Loops"], "while_loop")), uu___3) in - EApp uu___2 - | FStar_Extraction_ML_Syntax.MLE_App - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Name - ("Steel"::"ST"::"Printf"::[], fn); - FStar_Extraction_ML_Syntax.mlty = uu___; - FStar_Extraction_ML_Syntax.loc = uu___1;_}, - args) - -> - let uu___2 = - let uu___3 = FStar_Compiler_List.map (translate_expr env1) args in - ((EQualified (["LowStar"; "Printf"], fn)), uu___3) in - EApp uu___2 - | FStar_Extraction_ML_Syntax.MLE_App - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_TApp - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Name p; - FStar_Extraction_ML_Syntax.mlty = uu___; - FStar_Extraction_ML_Syntax.loc = uu___1;_}, - uu___2); - FStar_Extraction_ML_Syntax.mlty = uu___3; - FStar_Extraction_ML_Syntax.loc = uu___4;_}, - uu___5::uu___6::e1::[]) - when - (let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___7 = "Steel.Effect.Atomic.return") || - (let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___7 = "Steel.ST.Util.return") - -> translate_expr env1 e1 - | FStar_Extraction_ML_Syntax.MLE_App - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_TApp - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Name p; - FStar_Extraction_ML_Syntax.mlty = uu___; - FStar_Extraction_ML_Syntax.loc = uu___1;_}, - uu___2); - FStar_Extraction_ML_Syntax.mlty = uu___3; - FStar_Extraction_ML_Syntax.loc = uu___4;_}, - _fp::_fp'::_opened::_p::_i::{ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Fun - (uu___5, body); - FStar_Extraction_ML_Syntax.mlty = - uu___6; - FStar_Extraction_ML_Syntax.loc = - uu___7;_}::[]) - when - (let uu___8 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___8 = "Steel.ST.Util.with_invariant") || - (let uu___8 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___8 = "Steel.Effect.Atomic.with_invariant") - -> translate_expr env1 body - | FStar_Extraction_ML_Syntax.MLE_App - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_TApp - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Name p; - FStar_Extraction_ML_Syntax.mlty = uu___; - FStar_Extraction_ML_Syntax.loc = uu___1;_}, - uu___2); - FStar_Extraction_ML_Syntax.mlty = uu___3; - FStar_Extraction_ML_Syntax.loc = uu___4;_}, - _fp::_fp'::_opened::_p::_i::e1::[]) - when - (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "Steel.ST.Util.with_invariant") || - (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___5 = "Steel.Effect.Atomic.with_invariant") - -> - let uu___5 = - let uu___6 = - let uu___7 = - FStar_Compiler_Util.string_of_int - (FStar_Pervasives_Native.fst - e1.FStar_Extraction_ML_Syntax.loc) in - FStar_Compiler_Util.format2 - "Extraction of with_invariant requires its argument to be a function literal at extraction time, try marking its argument inline_for_extraction (%s, %s)" - uu___7 - (FStar_Pervasives_Native.snd - e1.FStar_Extraction_ML_Syntax.loc) in - (FStar_Errors_Codes.Fatal_ExtractionUnsupported, uu___6) in - FStar_Errors.raise_error uu___5 FStar_Compiler_Range.dummyRange | FStar_Extraction_ML_Syntax.MLE_App (head, args) -> let uu___ = let uu___1 = translate_expr env1 head in @@ -3214,7 +2817,7 @@ let (translate_type_decl' : (FStar_Errors_Codes.Warning_DefinitionNotTranslated, uu___7) in FStar_Errors.log_issue FStar_Compiler_Range.dummyRange uu___6); FStar_Pervasives_Native.None) -let (translate_let : +let (translate_let' : env -> FStar_Extraction_ML_Syntax.mlletflavor -> FStar_Extraction_ML_Syntax.mllb -> decl FStar_Pervasives_Native.option) @@ -3350,74 +2953,6 @@ let (translate_let : (cc1, meta1, (FStar_Compiler_List.length tvars), t1, name2, binders, (EAbortS msg1)))))))) - | { FStar_Extraction_ML_Syntax.mllb_name = name1; - FStar_Extraction_ML_Syntax.mllb_tysc = - FStar_Pervasives_Native.Some (tvars, t); - FStar_Extraction_ML_Syntax.mllb_add_unit = uu___; - FStar_Extraction_ML_Syntax.mllb_def = - { - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_App - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_TApp - ({ - FStar_Extraction_ML_Syntax.expr = - FStar_Extraction_ML_Syntax.MLE_Name p; - FStar_Extraction_ML_Syntax.mlty = uu___1; - FStar_Extraction_ML_Syntax.loc = uu___2;_}, - uu___3); - FStar_Extraction_ML_Syntax.mlty = uu___4; - FStar_Extraction_ML_Syntax.loc = uu___5;_}, - l::[]); - FStar_Extraction_ML_Syntax.mlty = uu___6; - FStar_Extraction_ML_Syntax.loc = uu___7;_}; - FStar_Extraction_ML_Syntax.mllb_meta = meta; - FStar_Extraction_ML_Syntax.print_typ = uu___8;_} when - let uu___9 = FStar_Extraction_ML_Syntax.string_of_mlpath p in - uu___9 = "Steel.TLArray.create" -> - if - FStar_Compiler_List.mem FStar_Extraction_ML_Syntax.NoExtract - meta - then FStar_Pervasives_Native.None - else - (let meta1 = translate_flags meta in - let env2 = - FStar_Compiler_List.fold_left - (fun env3 -> fun name2 -> extend_t env3 name2) env1 tvars in - let t1 = translate_type env2 t in - let name2 = ((env2.module_name), name1) in - try - (fun uu___10 -> - match () with - | () -> - let expr1 = - let uu___11 = list_elements l in - FStar_Compiler_List.map (translate_expr env2) - uu___11 in - FStar_Pervasives_Native.Some - (DGlobal - (meta1, name2, - (FStar_Compiler_List.length tvars), t1, - (EBufCreateL (Eternal, expr1))))) () - with - | uu___10 -> - ((let uu___12 = - let uu___13 = - let uu___14 = - FStar_Extraction_ML_Syntax.string_of_mlpath name2 in - let uu___15 = FStar_Compiler_Util.print_exn uu___10 in - FStar_Compiler_Util.format2 - "Error extracting %s to KaRaMeL (%s)\n" uu___14 - uu___15 in - (FStar_Errors_Codes.Warning_DefinitionNotTranslated, - uu___13) in - FStar_Errors.log_issue FStar_Compiler_Range.dummyRange - uu___12); - FStar_Pervasives_Native.Some - (DGlobal - (meta1, name2, (FStar_Compiler_List.length tvars), - t1, EAny)))) | { FStar_Extraction_ML_Syntax.mllb_name = name1; FStar_Extraction_ML_Syntax.mllb_tysc = FStar_Pervasives_Native.Some (tvars, t); @@ -3485,6 +3020,29 @@ let (translate_let : (FStar_String.concat ", " idents) uu___6 | FStar_Pervasives_Native.None -> ()); FStar_Pervasives_Native.None) +type translate_let_t = + env -> + FStar_Extraction_ML_Syntax.mlletflavor -> + FStar_Extraction_ML_Syntax.mllb -> decl FStar_Pervasives_Native.option +let (ref_translate_let : translate_let_t FStar_Compiler_Effect.ref) = + FStar_Compiler_Util.mk_ref translate_let' +let (register_pre_translate_let : translate_let_t -> unit) = + fun f -> + let before = FStar_Compiler_Effect.op_Bang ref_translate_let in + let after e fl lb = + try (fun uu___ -> match () with | () -> f e fl lb) () + with | NotSupportedByKrmlExtension -> before e fl lb in + FStar_Compiler_Effect.op_Colon_Equals ref_translate_let after +let (translate_let : + env -> + FStar_Extraction_ML_Syntax.mlletflavor -> + FStar_Extraction_ML_Syntax.mllb -> decl FStar_Pervasives_Native.option) + = + fun env1 -> + fun flavor -> + fun lb -> + let uu___ = FStar_Compiler_Effect.op_Bang ref_translate_let in + uu___ env1 flavor lb let (translate_decl : env -> FStar_Extraction_ML_Syntax.mlmodule1 -> decl Prims.list) = fun env1 -> @@ -3554,7 +3112,7 @@ let (translate : FStar_Extraction_ML_Syntax.mllib -> file Prims.list) = "Unable to translate module: %s because:\n %s\n" m_name uu___3); FStar_Pervasives_Native.None)) modules -let (uu___1975 : unit) = +let (uu___1713 : unit) = register_post_translate_type_without_decay translate_type_without_decay'; register_post_translate_type translate_type'; register_post_translate_type_decl translate_type_decl'; diff --git a/ocaml/fstar-lib/generated/FStar_Extraction_Krml_Steel.ml b/ocaml/fstar-lib/generated/FStar_Extraction_Krml_Steel.ml new file mode 100644 index 00000000000..cb9afa780da --- /dev/null +++ b/ocaml/fstar-lib/generated/FStar_Extraction_Krml_Steel.ml @@ -0,0 +1,664 @@ +open Prims +let (steel_translate_type_without_decay : + FStar_Extraction_Krml.translate_type_without_decay_t) = + fun env -> + fun t -> + match t with + | FStar_Extraction_ML_Syntax.MLTY_Named (arg::[], p) when + let uu___ = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___ = "Steel.TLArray.t" -> + let uu___ = + FStar_Extraction_Krml.translate_type_without_decay env arg in + FStar_Extraction_Krml.TConstBuf uu___ + | FStar_Extraction_ML_Syntax.MLTY_Named (arg::[], p) when + ((let uu___ = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___ = "Steel.Reference.ref") || + (let uu___ = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___ = "Steel.ST.Reference.ref")) + || + (let uu___ = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___ = "Steel.ST.HigherArray.ptr") + -> + let uu___ = + FStar_Extraction_Krml.translate_type_without_decay env arg in + FStar_Extraction_Krml.TBuf uu___ + | uu___ -> + FStar_Compiler_Effect.raise + FStar_Extraction_Krml.NotSupportedByKrmlExtension +let (steel_translate_expr : FStar_Extraction_Krml.translate_expr_t) = + fun env -> + fun e -> + match e.FStar_Extraction_ML_Syntax.expr with + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + t::[]); + FStar_Extraction_ML_Syntax.mlty = uu___2; + FStar_Extraction_ML_Syntax.loc = uu___3;_}, + uu___4) + when + let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___5 = "Steel.ST.HigherArray.null_ptr" -> + let uu___5 = FStar_Extraction_Krml.translate_type env t in + FStar_Extraction_Krml.EBufNull uu___5 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + t::[]); + FStar_Extraction_ML_Syntax.mlty = uu___2; + FStar_Extraction_ML_Syntax.loc = uu___3;_}, + arg::[]) + when + let uu___4 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___4 = "Steel.ST.HigherArray.is_null_ptr" -> + let uu___4 = FStar_Extraction_Krml.translate_type env t in + let uu___5 = FStar_Extraction_Krml.translate_expr env arg in + FStar_Extraction_Krml.generate_is_null uu___4 uu___5 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2); + FStar_Extraction_ML_Syntax.mlty = uu___3; + FStar_Extraction_ML_Syntax.loc = uu___4;_}, + _perm0::_perm1::_seq0::_seq1::e0::_len0::e1::_len1::[]) + when + let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___5 = "Steel.ST.HigherArray.ptrdiff_ptr" -> + let uu___5 = + let uu___6 = FStar_Extraction_Krml.translate_expr env e0 in + let uu___7 = FStar_Extraction_Krml.translate_expr env e1 in + (uu___6, uu___7) in + FStar_Extraction_Krml.EBufDiff uu___5 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2); + FStar_Extraction_ML_Syntax.mlty = uu___3; + FStar_Extraction_ML_Syntax.loc = uu___4;_}, + e1::e2::[]) + when + let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___5 = "Steel.TLArray.get" -> + let uu___5 = + let uu___6 = FStar_Extraction_Krml.translate_expr env e1 in + let uu___7 = FStar_Extraction_Krml.translate_expr env e2 in + (uu___6, uu___7) in + FStar_Extraction_Krml.EBufRead uu___5 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2); + FStar_Extraction_ML_Syntax.mlty = uu___3; + FStar_Extraction_ML_Syntax.loc = uu___4;_}, + _perm::e1::_len::_seq::e2::[]) + when + let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___5 = "Steel.ST.HigherArray.index_ptr" -> + let uu___5 = + let uu___6 = FStar_Extraction_Krml.translate_expr env e1 in + let uu___7 = FStar_Extraction_Krml.translate_expr env e2 in + (uu___6, uu___7) in + FStar_Extraction_Krml.EBufRead uu___5 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2); + FStar_Extraction_ML_Syntax.mlty = uu___3; + FStar_Extraction_ML_Syntax.loc = uu___4;_}, + e1::[]) + when + let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___5 = "Steel.Reference.read" -> + let uu___5 = + let uu___6 = FStar_Extraction_Krml.translate_expr env e1 in + (uu___6, + (FStar_Extraction_Krml.EQualified (["C"], "_zero_for_deref"))) in + FStar_Extraction_Krml.EBufRead uu___5 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2); + FStar_Extraction_ML_Syntax.mlty = uu___3; + FStar_Extraction_ML_Syntax.loc = uu___4;_}, + _perm::_v::e1::[]) + when + let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___5 = "Steel.ST.Reference.read" -> + let uu___5 = + let uu___6 = FStar_Extraction_Krml.translate_expr env e1 in + (uu___6, + (FStar_Extraction_Krml.EQualified (["C"], "_zero_for_deref"))) in + FStar_Extraction_Krml.EBufRead uu___5 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2); + FStar_Extraction_ML_Syntax.mlty = uu___3; + FStar_Extraction_ML_Syntax.loc = uu___4;_}, + init::[]) + when + let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___5 = "Steel.ST.Reference._alloca" -> + let uu___5 = + let uu___6 = FStar_Extraction_Krml.translate_expr env init in + (FStar_Extraction_Krml.Stack, uu___6, + (FStar_Extraction_Krml.EConstant + (FStar_Extraction_Krml.UInt32, "1"))) in + FStar_Extraction_Krml.EBufCreate uu___5 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2); + FStar_Extraction_ML_Syntax.mlty = uu___3; + FStar_Extraction_ML_Syntax.loc = uu___4;_}, + init::[]) + when + (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___5 = "Steel.Reference.malloc") || + (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___5 = "Steel.ST.Reference.alloc") + -> + let uu___5 = + let uu___6 = FStar_Extraction_Krml.translate_expr env init in + (FStar_Extraction_Krml.ManuallyManaged, uu___6, + (FStar_Extraction_Krml.EConstant + (FStar_Extraction_Krml.UInt32, "1"))) in + FStar_Extraction_Krml.EBufCreate uu___5 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2); + FStar_Extraction_ML_Syntax.mlty = uu___3; + FStar_Extraction_ML_Syntax.loc = uu___4;_}, + e0::e1::[]) + when + let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___5 = "Steel.ST.HigherArray.malloc_ptr" -> + let uu___5 = + let uu___6 = FStar_Extraction_Krml.translate_expr env e0 in + let uu___7 = FStar_Extraction_Krml.translate_expr env e1 in + (FStar_Extraction_Krml.ManuallyManaged, uu___6, uu___7) in + FStar_Extraction_Krml.EBufCreate uu___5 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2); + FStar_Extraction_ML_Syntax.mlty = uu___3; + FStar_Extraction_ML_Syntax.loc = uu___4;_}, + e2::[]) + when + let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___5 = "Steel.Reference.free" -> + let uu___5 = FStar_Extraction_Krml.translate_expr env e2 in + FStar_Extraction_Krml.EBufFree uu___5 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2); + FStar_Extraction_ML_Syntax.mlty = uu___3; + FStar_Extraction_ML_Syntax.loc = uu___4;_}, + _v::e2::[]) + when + (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___5 = "Steel.ST.HigherArray.free_ptr") || + (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___5 = "Steel.ST.Reference.free") + -> + let uu___5 = FStar_Extraction_Krml.translate_expr env e2 in + FStar_Extraction_Krml.EBufFree uu___5 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2); + FStar_Extraction_ML_Syntax.mlty = uu___3; + FStar_Extraction_ML_Syntax.loc = uu___4;_}, + e1::e2::[]) + when + let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___5 = "Steel.ST.HigherArray.ptr_shift" -> + let uu___5 = + let uu___6 = FStar_Extraction_Krml.translate_expr env e1 in + let uu___7 = FStar_Extraction_Krml.translate_expr env e2 in + (uu___6, uu___7) in + FStar_Extraction_Krml.EBufSub uu___5 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2); + FStar_Extraction_ML_Syntax.mlty = uu___3; + FStar_Extraction_ML_Syntax.loc = uu___4;_}, + e1::_len::_s::e2::e3::[]) + when + let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___5 = "Steel.ST.HigherArray.upd_ptr" -> + let uu___5 = + let uu___6 = FStar_Extraction_Krml.translate_expr env e1 in + let uu___7 = FStar_Extraction_Krml.translate_expr env e2 in + let uu___8 = FStar_Extraction_Krml.translate_expr env e3 in + (uu___6, uu___7, uu___8) in + FStar_Extraction_Krml.EBufWrite uu___5 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2); + FStar_Extraction_ML_Syntax.mlty = uu___3; + FStar_Extraction_ML_Syntax.loc = uu___4;_}, + e1::_len::_s::e2::e3::[]) + when + let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___5 = "Steel.ST.HigherArray.upd_ptr" -> + let uu___5 = + let uu___6 = FStar_Extraction_Krml.translate_expr env e1 in + let uu___7 = FStar_Extraction_Krml.translate_expr env e2 in + let uu___8 = FStar_Extraction_Krml.translate_expr env e3 in + (uu___6, uu___7, uu___8) in + FStar_Extraction_Krml.EBufWrite uu___5 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2); + FStar_Extraction_ML_Syntax.mlty = uu___3; + FStar_Extraction_ML_Syntax.loc = uu___4;_}, + e1::e2::[]) + when + let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___5 = "Steel.Reference.write" -> + let uu___5 = + let uu___6 = FStar_Extraction_Krml.translate_expr env e1 in + let uu___7 = FStar_Extraction_Krml.translate_expr env e2 in + (uu___6, + (FStar_Extraction_Krml.EQualified (["C"], "_zero_for_deref")), + uu___7) in + FStar_Extraction_Krml.EBufWrite uu___5 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2); + FStar_Extraction_ML_Syntax.mlty = uu___3; + FStar_Extraction_ML_Syntax.loc = uu___4;_}, + _v::e1::e2::[]) + when + let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___5 = "Steel.ST.Reference.write" -> + let uu___5 = + let uu___6 = FStar_Extraction_Krml.translate_expr env e1 in + let uu___7 = FStar_Extraction_Krml.translate_expr env e2 in + (uu___6, + (FStar_Extraction_Krml.EQualified (["C"], "_zero_for_deref")), + uu___7) in + FStar_Extraction_Krml.EBufWrite uu___5 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2::[]) + when + let uu___3 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___3 = "Steel.ST.Reference._push_frame" -> + FStar_Extraction_Krml.EPushFrame + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2); + FStar_Extraction_ML_Syntax.mlty = uu___3; + FStar_Extraction_ML_Syntax.loc = uu___4;_}, + uu___5::uu___6::[]) + when + let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___7 = "Steel.ST.Reference._free_and_pop_frame" -> + FStar_Extraction_Krml.EPopFrame + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2); + FStar_Extraction_ML_Syntax.mlty = uu___3; + FStar_Extraction_ML_Syntax.loc = uu___4;_}, + uu___5::uu___6::uu___7::e1::uu___8::e2::e3::uu___9::e4::e5::[]) + when + let uu___10 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___10 = "Steel.ST.HigherArray.blit_ptr" -> + let uu___10 = + let uu___11 = FStar_Extraction_Krml.translate_expr env e1 in + let uu___12 = FStar_Extraction_Krml.translate_expr env e2 in + let uu___13 = FStar_Extraction_Krml.translate_expr env e3 in + let uu___14 = FStar_Extraction_Krml.translate_expr env e4 in + let uu___15 = FStar_Extraction_Krml.translate_expr env e5 in + (uu___11, uu___12, uu___13, uu___14, uu___15) in + FStar_Extraction_Krml.EBufBlit uu___10 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2); + FStar_Extraction_ML_Syntax.mlty = uu___3; + FStar_Extraction_ML_Syntax.loc = uu___4;_}, + uu___5::uu___6::e1::[]) + when + let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___7 = "Steel.Effect.Atomic.return" -> + FStar_Extraction_Krml.translate_expr env e1 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + _inv::test::body::[]) + when + let uu___2 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___2 = "Steel.ST.Loops.while_loop" -> + let uu___2 = + let uu___3 = + let uu___4 = + let uu___5 = FStar_Extraction_Krml.translate_expr env test in + let uu___6 = + let uu___7 = FStar_Extraction_Krml.translate_expr env body in + [uu___7] in + uu___5 :: uu___6 in + FStar_Extraction_Krml.EUnit :: uu___4 in + ((FStar_Extraction_Krml.EQualified + (["Steel"; "Loops"], "while_loop")), uu___3) in + FStar_Extraction_Krml.EApp uu___2 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name + ("Steel"::"ST"::"Printf"::[], fn); + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + args) + -> + let uu___2 = + let uu___3 = + FStar_Compiler_List.map + (FStar_Extraction_Krml.translate_expr env) args in + ((FStar_Extraction_Krml.EQualified (["LowStar"; "Printf"], fn)), + uu___3) in + FStar_Extraction_Krml.EApp uu___2 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2); + FStar_Extraction_ML_Syntax.mlty = uu___3; + FStar_Extraction_ML_Syntax.loc = uu___4;_}, + uu___5::uu___6::e1::[]) + when + (let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___7 = "Steel.Effect.Atomic.return") || + (let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___7 = "Steel.ST.Util.return") + -> FStar_Extraction_Krml.translate_expr env e1 + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2); + FStar_Extraction_ML_Syntax.mlty = uu___3; + FStar_Extraction_ML_Syntax.loc = uu___4;_}, + _fp::_fp'::_opened::_p::_i::{ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Fun + (uu___5, body); + FStar_Extraction_ML_Syntax.mlty = + uu___6; + FStar_Extraction_ML_Syntax.loc = + uu___7;_}::[]) + when + (let uu___8 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___8 = "Steel.ST.Util.with_invariant") || + (let uu___8 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___8 = "Steel.Effect.Atomic.with_invariant") + -> FStar_Extraction_Krml.translate_expr env body + | FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___; + FStar_Extraction_ML_Syntax.loc = uu___1;_}, + uu___2); + FStar_Extraction_ML_Syntax.mlty = uu___3; + FStar_Extraction_ML_Syntax.loc = uu___4;_}, + _fp::_fp'::_opened::_p::_i::e1::[]) + when + (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___5 = "Steel.ST.Util.with_invariant") || + (let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___5 = "Steel.Effect.Atomic.with_invariant") + -> + let uu___5 = + let uu___6 = + let uu___7 = + FStar_Compiler_Util.string_of_int + (FStar_Pervasives_Native.fst + e1.FStar_Extraction_ML_Syntax.loc) in + FStar_Compiler_Util.format2 + "Extraction of with_invariant requires its argument to be a function literal at extraction time, try marking its argument inline_for_extraction (%s, %s)" + uu___7 + (FStar_Pervasives_Native.snd + e1.FStar_Extraction_ML_Syntax.loc) in + (FStar_Errors_Codes.Fatal_ExtractionUnsupported, uu___6) in + FStar_Errors.raise_error uu___5 FStar_Compiler_Range.dummyRange + | uu___ -> + FStar_Compiler_Effect.raise + FStar_Extraction_Krml.NotSupportedByKrmlExtension +let (steel_translate_let : FStar_Extraction_Krml.translate_let_t) = + fun env -> + fun flavor -> + fun lb -> + match lb with + | { FStar_Extraction_ML_Syntax.mllb_name = name; + FStar_Extraction_ML_Syntax.mllb_tysc = + FStar_Pervasives_Native.Some (tvars, t); + FStar_Extraction_ML_Syntax.mllb_add_unit = uu___; + FStar_Extraction_ML_Syntax.mllb_def = + { + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_App + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_TApp + ({ + FStar_Extraction_ML_Syntax.expr = + FStar_Extraction_ML_Syntax.MLE_Name p; + FStar_Extraction_ML_Syntax.mlty = uu___1; + FStar_Extraction_ML_Syntax.loc = uu___2;_}, + uu___3); + FStar_Extraction_ML_Syntax.mlty = uu___4; + FStar_Extraction_ML_Syntax.loc = uu___5;_}, + l::[]); + FStar_Extraction_ML_Syntax.mlty = uu___6; + FStar_Extraction_ML_Syntax.loc = uu___7;_}; + FStar_Extraction_ML_Syntax.mllb_meta = meta; + FStar_Extraction_ML_Syntax.print_typ = uu___8;_} when + let uu___9 = FStar_Extraction_ML_Syntax.string_of_mlpath p in + uu___9 = "Steel.TLArray.create" -> + if + FStar_Compiler_List.mem FStar_Extraction_ML_Syntax.NoExtract + meta + then FStar_Pervasives_Native.None + else + (let meta1 = FStar_Extraction_Krml.translate_flags meta in + let env1 = + FStar_Compiler_List.fold_left + (fun env2 -> + fun name1 -> FStar_Extraction_Krml.extend_t env2 name1) + env tvars in + let t1 = FStar_Extraction_Krml.translate_type env1 t in + let name1 = ((env1.FStar_Extraction_Krml.module_name), name) in + try + (fun uu___10 -> + match () with + | () -> + let expr = + let uu___11 = FStar_Extraction_Krml.list_elements l in + FStar_Compiler_List.map + (FStar_Extraction_Krml.translate_expr env1) + uu___11 in + FStar_Pervasives_Native.Some + (FStar_Extraction_Krml.DGlobal + (meta1, name1, + (FStar_Compiler_List.length tvars), t1, + (FStar_Extraction_Krml.EBufCreateL + (FStar_Extraction_Krml.Eternal, expr))))) + () + with + | uu___10 -> + ((let uu___12 = + let uu___13 = + let uu___14 = + FStar_Extraction_ML_Syntax.string_of_mlpath name1 in + let uu___15 = FStar_Compiler_Util.print_exn uu___10 in + FStar_Compiler_Util.format2 + "Error extracting %s to KaRaMeL (%s)\n" uu___14 + uu___15 in + (FStar_Errors_Codes.Warning_DefinitionNotTranslated, + uu___13) in + FStar_Errors.log_issue FStar_Compiler_Range.dummyRange + uu___12); + FStar_Pervasives_Native.Some + (FStar_Extraction_Krml.DGlobal + (meta1, name1, (FStar_Compiler_List.length tvars), + t1, FStar_Extraction_Krml.EAny)))) + | uu___ -> + FStar_Compiler_Effect.raise + FStar_Extraction_Krml.NotSupportedByKrmlExtension +let (uu___391 : unit) = + FStar_Extraction_Krml.register_pre_translate_type_without_decay + steel_translate_type_without_decay; + FStar_Extraction_Krml.register_pre_translate_expr steel_translate_expr; + FStar_Extraction_Krml.register_pre_translate_let steel_translate_let \ No newline at end of file diff --git a/src/Makefile.boot b/src/Makefile.boot index e80aca1c630..5db72dc2920 100644 --- a/src/Makefile.boot +++ b/src/Makefile.boot @@ -91,6 +91,7 @@ EXTRACT = $(addprefix --extract_module , $(EXTRACT_MODULES)) \ $(Q)$(FSTAR_C) --dep full \ fstar/FStar.Main.fst \ boot/FStar.Tests.Test.fst \ + extraction/FStar.Extraction.Krml.Steel.fst \ --odir $(OUTPUT_DIRECTORY) \ $(EXTRACT) > ._depend @# We've generated deps for everything into fstar-lib/generated. diff --git a/src/extraction/FStar.Extraction.Krml.Steel.fst b/src/extraction/FStar.Extraction.Krml.Steel.fst new file mode 100644 index 00000000000..543d3edd6ef --- /dev/null +++ b/src/extraction/FStar.Extraction.Krml.Steel.fst @@ -0,0 +1,191 @@ +module FStar.Extraction.Krml.Steel +friend FStar.Extraction.Krml + +(* IMPORTANT: these `open` directives come from FStar.Extraction.Krml. + Without them, spurious dependencies on F* ulib will be introduced *) +open FStar.Compiler.Effect +open FStar.Compiler.List +open FStar +open FStar.Compiler +open FStar.Compiler.Util +open FStar.Extraction +open FStar.Extraction.ML +open FStar.Extraction.ML.Syntax +open FStar.Const +open FStar.BaseTypes + +module BU = FStar.Compiler.Util +module FC = FStar.Const + +open FStar.Extraction.Krml + +let steel_translate_type_without_decay : translate_type_without_decay_t = fun env t -> + match t with + | MLTY_Named ([arg], p) when + Syntax.string_of_mlpath p = "Steel.TLArray.t" -> + TConstBuf (translate_type_without_decay env arg) + + | MLTY_Named ([arg], p) when + Syntax.string_of_mlpath p = "Steel.Reference.ref" || + Syntax.string_of_mlpath p = "Steel.ST.Reference.ref" || + Syntax.string_of_mlpath p = "Steel.ST.HigherArray.ptr" + -> + TBuf (translate_type_without_decay env arg) + + | _ -> raise NotSupportedByKrmlExtension + +let steel_translate_expr : translate_expr_t = fun env e -> + match e.expr with + | MLE_App ({expr = MLE_TApp ({expr = MLE_Name p}, [t]) }, _) + when string_of_mlpath p = "Steel.ST.HigherArray.null_ptr" + -> + EBufNull (translate_type env t) + | MLE_App ({expr = MLE_TApp ({expr = MLE_Name p }, [t])}, [arg]) + when string_of_mlpath p = "Steel.ST.HigherArray.is_null_ptr" + -> + generate_is_null (translate_type env t) (translate_expr env arg) + + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p}, _) }, [ _perm0; _perm1; _seq0; _seq1; e0; _len0; e1; _len1]) + when string_of_mlpath p = "Steel.ST.HigherArray.ptrdiff_ptr" -> + EBufDiff (translate_expr env e0, translate_expr env e1) + + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; e2 ]) + when string_of_mlpath p = "Steel.TLArray.get" -> + EBufRead (translate_expr env e1, translate_expr env e2) + + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _perm; e1; _len; _seq; e2 ]) + when string_of_mlpath p = "Steel.ST.HigherArray.index_ptr" -> + EBufRead (translate_expr env e1, translate_expr env e2) + + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e ]) + when string_of_mlpath p = "Steel.Reference.read" -> + EBufRead (translate_expr env e, EQualified (["C"], "_zero_for_deref")) + + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _perm; _v; e ]) + when string_of_mlpath p = "Steel.ST.Reference.read" -> + EBufRead (translate_expr env e, EQualified (["C"], "_zero_for_deref")) + + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) } , [ init ]) + when ( + string_of_mlpath p = "Steel.ST.Reference._alloca" + ) -> + EBufCreate (Stack, translate_expr env init, EConstant (UInt32, "1")) + + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) } , [ init ]) + when (string_of_mlpath p = "Steel.Reference.malloc" || + string_of_mlpath p = "Steel.ST.Reference.alloc") -> + EBufCreate (ManuallyManaged, translate_expr env init, EConstant (UInt32, "1")) + + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e0; e1 ]) + when string_of_mlpath p = "Steel.ST.HigherArray.malloc_ptr" -> + EBufCreate (ManuallyManaged, translate_expr env e0, translate_expr env e1) + + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e2 ]) when + string_of_mlpath p = "Steel.Reference.free" -> + EBufFree (translate_expr env e2) + + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _v; e2 ]) when + string_of_mlpath p = "Steel.ST.HigherArray.free_ptr" || + string_of_mlpath p = "Steel.ST.Reference.free" -> + EBufFree (translate_expr env e2) + + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; e2 ]) + when string_of_mlpath p = "Steel.ST.HigherArray.ptr_shift" -> + EBufSub (translate_expr env e1, translate_expr env e2) + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; _len; _s; e2; e3 ]) + when string_of_mlpath p = "Steel.ST.HigherArray.upd_ptr" -> + EBufWrite (translate_expr env e1, translate_expr env e2, translate_expr env e3) + + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; _len; _s; e2; e3 ]) + when string_of_mlpath p = "Steel.ST.HigherArray.upd_ptr" -> + EBufWrite (translate_expr env e1, translate_expr env e2, translate_expr env e3) + + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; e2 ]) + when string_of_mlpath p = "Steel.Reference.write" -> + EBufWrite (translate_expr env e1, EQualified (["C"], "_zero_for_deref"), translate_expr env e2) + + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _v; e1; e2 ]) + when string_of_mlpath p = "Steel.ST.Reference.write" -> + EBufWrite (translate_expr env e1, EQualified (["C"], "_zero_for_deref"), translate_expr env e2) + + | MLE_App ({ expr = MLE_Name p }, [ _ ]) when ( + string_of_mlpath p = "Steel.ST.Reference._push_frame" + ) -> + EPushFrame + + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _; _ ]) when (string_of_mlpath p = "Steel.ST.Reference._free_and_pop_frame") -> + EPopFrame + + | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _; _; _; e1; _; e2; e3; _; e4; e5 ]) when ( + string_of_mlpath p = "Steel.ST.HigherArray.blit_ptr" + ) -> + EBufBlit (translate_expr env e1, translate_expr env e2, translate_expr env e3, translate_expr env e4, translate_expr env e5) + + (* Misc. Steel operations *) + | MLE_App ({expr=MLE_TApp ({expr=MLE_Name p}, _)}, [_; _; e]) + when string_of_mlpath p = "Steel.Effect.Atomic.return" -> + translate_expr env e + + | MLE_App ({expr=MLE_Name p}, [ _inv; test; body ]) + when (string_of_mlpath p = "Steel.ST.Loops.while_loop") -> + EApp (EQualified (["Steel"; "Loops"], "while_loop"), [ EUnit; translate_expr env test; translate_expr env body ]) + + (* Piggyback Steel.ST.Printf primitives to LowStar.Printf *) + | MLE_App ({ expr = MLE_Name (["Steel"; "ST"; "Printf"], fn) }, args) -> + EApp (EQualified ([ "LowStar"; "Printf" ], fn), List.map (translate_expr env) args) + + | MLE_App ({expr=MLE_TApp ({expr=MLE_Name p}, _)}, [_; _; e]) + when string_of_mlpath p = "Steel.Effect.Atomic.return" || + string_of_mlpath p = "Steel.ST.Util.return" -> + translate_expr env e + + | MLE_App ({expr=MLE_TApp ({expr=MLE_Name p}, _)}, [_fp; _fp'; _opened; _p; _i; {expr=MLE_Fun (_, body)}]) + when string_of_mlpath p = "Steel.ST.Util.with_invariant" || + string_of_mlpath p = "Steel.Effect.Atomic.with_invariant" -> + translate_expr env body + + | MLE_App ({expr=MLE_TApp ({expr=MLE_Name p}, _)}, [_fp; _fp'; _opened; _p; _i; e]) + when string_of_mlpath p = "Steel.ST.Util.with_invariant" || + string_of_mlpath p = "Steel.Effect.Atomic.with_invariant" -> + Errors.raise_error + (Errors.Fatal_ExtractionUnsupported, + BU.format2 + "Extraction of with_invariant requires its argument to be a function literal \ + at extraction time, try marking its argument inline_for_extraction (%s, %s)" + (string_of_int (fst e.loc)) + (snd e.loc)) + Range.dummyRange + + | _ -> raise NotSupportedByKrmlExtension + +let steel_translate_let : translate_let_t = fun env flavor lb -> + match lb with + | { + mllb_name = name; + mllb_tysc = Some (tvars, t); + mllb_def = { expr = MLE_App ({ + expr = MLE_TApp ({expr = MLE_Name p}, _)}, [ l ] ) }; + mllb_meta = meta + } + when string_of_mlpath p = "Steel.TLArray.create" -> + if List.mem Syntax.NoExtract meta then + None + else + // This is a global const array, defined using Steel.TLArray + let meta = translate_flags meta in + let env = List.fold_left (fun env name -> extend_t env name) env tvars in + let t = translate_type env t in + let name = env.module_name, name in + begin try + let expr = List.map (translate_expr env) (list_elements l) in + Some (DGlobal (meta, name, List.length tvars, t, EBufCreateL (Eternal, expr))) + with e -> + Errors. log_issue Range.dummyRange (Errors.Warning_DefinitionNotTranslated, (BU.format2 "Error extracting %s to KaRaMeL (%s)\n" (Syntax.string_of_mlpath name) (BU.print_exn e))); + Some (DGlobal (meta, name, List.length tvars, t, EAny)) + end + | _ -> raise NotSupportedByKrmlExtension + +let _ = + register_pre_translate_type_without_decay steel_translate_type_without_decay; + register_pre_translate_expr steel_translate_expr; + register_pre_translate_let steel_translate_let diff --git a/src/extraction/FStar.Extraction.Krml.Steel.fsti b/src/extraction/FStar.Extraction.Krml.Steel.fsti new file mode 100644 index 00000000000..b6477e00f20 --- /dev/null +++ b/src/extraction/FStar.Extraction.Krml.Steel.fsti @@ -0,0 +1,3 @@ +module FStar.Extraction.Krml.Steel + +// this fsti is necessary because we are `friend`ing FStar.Extraction.Krml diff --git a/src/extraction/FStar.Extraction.Krml.fst b/src/extraction/FStar.Extraction.Krml.fst index ccf706f1fb9..47d841aaa19 100644 --- a/src/extraction/FStar.Extraction.Krml.fst +++ b/src/extraction/FStar.Extraction.Krml.fst @@ -529,7 +529,8 @@ let rec translate_type_without_decay' env t: typ = | MLTY_Named ([arg], p) when Syntax.string_of_mlpath p = "LowStar.ConstBuffer.const_buffer" || - Syntax.string_of_mlpath p = "Steel.TLArray.t" -> TConstBuf (translate_type_without_decay env arg) + false + -> TConstBuf (translate_type_without_decay env arg) | MLTY_Named ([arg], p) when Syntax.string_of_mlpath p = "FStar.Buffer.buffer" || @@ -546,9 +547,7 @@ let rec translate_type_without_decay' env t: typ = Syntax.string_of_mlpath p = "FStar.HyperStack.ST.ref" || Syntax.string_of_mlpath p = "FStar.HyperStack.ST.mmstackref" || Syntax.string_of_mlpath p = "FStar.HyperStack.ST.mmref" || - Syntax.string_of_mlpath p = "Steel.Reference.ref" || - Syntax.string_of_mlpath p = "Steel.ST.Reference.ref" || - Syntax.string_of_mlpath p = "Steel.ST.HigherArray.ptr" + false -> TBuf (translate_type_without_decay env arg) @@ -634,14 +633,6 @@ and translate_expr' env e: expr = // We recognize certain distinguished names from [FStar.HST] and other // modules, and translate them into built-in Karamel constructs - | MLE_App ({expr = MLE_TApp ({expr = MLE_Name p}, [t]) }, _) - when string_of_mlpath p = "Steel.ST.HigherArray.null_ptr" - -> - EBufNull (translate_type env t) - | MLE_App ({expr = MLE_TApp ({expr = MLE_Name p }, [t])}, [arg]) - when string_of_mlpath p = "Steel.ST.HigherArray.is_null_ptr" - -> - generate_is_null (translate_type env t) (translate_expr env arg) | MLE_App({expr=MLE_TApp ({ expr = MLE_Name p }, [t])}, [arg]) when string_of_mlpath p = "FStar.Dyn.undyn" -> ECast (translate_expr env arg, translate_type env t) @@ -671,29 +662,17 @@ and translate_expr' env e: expr = -> translate_expr env e - | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p}, _) }, [ _perm0; _perm1; _seq0; _seq1; e0; _len0; e1; _len1]) - when string_of_mlpath p = "Steel.ST.HigherArray.ptrdiff_ptr" -> - EBufDiff (translate_expr env e0, translate_expr env e1) - | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; e2 ]) when string_of_mlpath p = "FStar.Buffer.index" || string_of_mlpath p = "FStar.Buffer.op_Array_Access" || string_of_mlpath p = "LowStar.Monotonic.Buffer.index" || string_of_mlpath p = "LowStar.UninitializedBuffer.uindex" || string_of_mlpath p = "LowStar.ConstBuffer.index" - || string_of_mlpath p = "Steel.TLArray.get" -> - EBufRead (translate_expr env e1, translate_expr env e2) - - | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _perm; e1; _len; _seq; e2 ]) - when string_of_mlpath p = "Steel.ST.HigherArray.index_ptr" -> + -> EBufRead (translate_expr env e1, translate_expr env e2) | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e ]) when string_of_mlpath p = "FStar.HyperStack.ST.op_Bang" - || string_of_mlpath p = "Steel.Reference.read" -> - EBufRead (translate_expr env e, EQualified (["C"], "_zero_for_deref")) - - | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _perm; _v; e ]) - when string_of_mlpath p = "Steel.ST.Reference.read" -> + -> EBufRead (translate_expr env e, EQualified (["C"], "_zero_for_deref")) (* Flatten all universes *) @@ -721,7 +700,7 @@ and translate_expr' env e: expr = | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) } , [ init ]) when ( string_of_mlpath p = "FStar.HyperStack.ST.salloc" || - string_of_mlpath p = "Steel.ST.Reference._alloca" + false ) -> EBufCreate (Stack, translate_expr env init, EConstant (UInt32, "1")) @@ -772,11 +751,6 @@ and translate_expr' env e: expr = (string_of_mlpath p = "FStar.HyperStack.ST.ralloc_drgn_mm") -> EBufCreate (ManuallyManaged, translate_expr env init, EConstant (UInt32, "1")) - | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) } , [ init ]) - when (string_of_mlpath p = "Steel.Reference.malloc" || - string_of_mlpath p = "Steel.ST.Reference.alloc") -> - EBufCreate (ManuallyManaged, translate_expr env init, EConstant (UInt32, "1")) - | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _e0; e1; e2 ]) when (string_of_mlpath p = "FStar.Buffer.rcreate_mm" || string_of_mlpath p = "LowStar.Monotonic.Buffer.mmalloc" || @@ -784,11 +758,6 @@ and translate_expr' env e: expr = string_of_mlpath p = "LowStar.ImmutableBuffer.imalloc") -> EBufCreate (ManuallyManaged, translate_expr env e1, translate_expr env e2) - | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e0; e1 ]) - when string_of_mlpath p = "Steel.ST.HigherArray.malloc_ptr" -> - EBufCreate (ManuallyManaged, translate_expr env e0, translate_expr env e1) - - | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _erid; elen ]) when string_of_mlpath p = "LowStar.UninitializedBuffer.umalloc" -> EBufCreateNoInit (ManuallyManaged, translate_expr env elen) @@ -796,12 +765,7 @@ and translate_expr' env e: expr = (* Only manually-managed references and buffers can be freed. *) | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e2 ]) when (string_of_mlpath p = "FStar.HyperStack.ST.rfree" || - string_of_mlpath p = "Steel.Reference.free") -> - EBufFree (translate_expr env e2) - - | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _v; e2 ]) when - string_of_mlpath p = "Steel.ST.HigherArray.free_ptr" || - string_of_mlpath p = "Steel.ST.Reference.free" -> + false) -> EBufFree (translate_expr env e2) | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e2 ]) @@ -823,7 +787,7 @@ and translate_expr' env e: expr = | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; e2 ]) when string_of_mlpath p = "FStar.Buffer.offset" - || string_of_mlpath p = "Steel.ST.HigherArray.ptr_shift" -> + -> EBufSub (translate_expr env e1, translate_expr env e2) | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; e2 ]) when string_of_mlpath p = "LowStar.Monotonic.Buffer.moffset" -> @@ -836,38 +800,24 @@ and translate_expr' env e: expr = -> EBufWrite (translate_expr env e1, translate_expr env e2, translate_expr env e3) - | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; _len; _s; e2; e3 ]) - when string_of_mlpath p = "Steel.ST.HigherArray.upd_ptr" -> - EBufWrite (translate_expr env e1, translate_expr env e2, translate_expr env e3) - | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; e2 ]) when string_of_mlpath p = "FStar.HyperStack.ST.op_Colon_Equals" - || string_of_mlpath p = "Steel.Reference.write" -> - EBufWrite (translate_expr env e1, EQualified (["C"], "_zero_for_deref"), translate_expr env e2) - - | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _v; e1; e2 ]) - when string_of_mlpath p = "Steel.ST.Reference.write" -> + -> EBufWrite (translate_expr env e1, EQualified (["C"], "_zero_for_deref"), translate_expr env e2) | MLE_App ({ expr = MLE_Name p }, [ _ ]) when ( string_of_mlpath p = "FStar.HyperStack.ST.push_frame" || - string_of_mlpath p = "Steel.ST.Reference._push_frame" + false ) -> EPushFrame | MLE_App ({ expr = MLE_Name p }, [ _ ]) when (string_of_mlpath p = "FStar.HyperStack.ST.pop_frame") -> EPopFrame - | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _; _ ]) when (string_of_mlpath p = "Steel.ST.Reference._free_and_pop_frame") -> - EPopFrame | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; e2; e3; e4; e5 ]) when ( string_of_mlpath p = "FStar.Buffer.blit" || string_of_mlpath p = "LowStar.Monotonic.Buffer.blit" || string_of_mlpath p = "LowStar.UninitializedBuffer.ublit" ) -> EBufBlit (translate_expr env e1, translate_expr env e2, translate_expr env e3, translate_expr env e4, translate_expr env e5) - | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _; _; _; e1; _; e2; e3; _; e4; e5 ]) when ( - string_of_mlpath p = "Steel.ST.HigherArray.blit_ptr" - ) -> - EBufBlit (translate_expr env e1, translate_expr env e2, translate_expr env e3, translate_expr env e4, translate_expr env e5) | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e1; e2; e3 ]) when (let s = string_of_mlpath p in (s = "FStar.Buffer.fill" || s = "LowStar.Monotonic.Buffer.fill" )) -> EBufFill (translate_expr env e1, translate_expr env e2, translate_expr env e3) @@ -1000,11 +950,6 @@ and translate_expr' env e: expr = else EApp (EQualified ([ "FStar"; "Int"; "Cast" ], c), [ translate_expr env arg ]) - (* Misc. Steel operations *) - | MLE_App ({expr=MLE_TApp ({expr=MLE_Name p}, _)}, [_; _; e]) - when string_of_mlpath p = "Steel.Effect.Atomic.return" -> - translate_expr env e - | MLE_App ({ expr = MLE_Name p }, [ arg ]) when string_of_mlpath p = "FStar.SizeT.uint16_to_sizet" || string_of_mlpath p = "FStar.SizeT.uint32_to_sizet" || @@ -1016,36 +961,6 @@ and translate_expr' env e: expr = when string_of_mlpath p = "FStar.SizeT.sizet_to_uint32" -> ECast (translate_expr env arg, TInt UInt32) - | MLE_App ({expr=MLE_Name p}, [ _inv; test; body ]) - when (string_of_mlpath p = "Steel.ST.Loops.while_loop") -> - EApp (EQualified (["Steel"; "Loops"], "while_loop"), [ EUnit; translate_expr env test; translate_expr env body ]) - - (* Piggyback Steel.ST.Printf primitives to LowStar.Printf *) - | MLE_App ({ expr = MLE_Name (["Steel"; "ST"; "Printf"], fn) }, args) -> - EApp (EQualified ([ "LowStar"; "Printf" ], fn), List.map (translate_expr env) args) - - | MLE_App ({expr=MLE_TApp ({expr=MLE_Name p}, _)}, [_; _; e]) - when string_of_mlpath p = "Steel.Effect.Atomic.return" || - string_of_mlpath p = "Steel.ST.Util.return" -> - translate_expr env e - - | MLE_App ({expr=MLE_TApp ({expr=MLE_Name p}, _)}, [_fp; _fp'; _opened; _p; _i; {expr=MLE_Fun (_, body)}]) - when string_of_mlpath p = "Steel.ST.Util.with_invariant" || - string_of_mlpath p = "Steel.Effect.Atomic.with_invariant" -> - translate_expr env body - - | MLE_App ({expr=MLE_TApp ({expr=MLE_Name p}, _)}, [_fp; _fp'; _opened; _p; _i; e]) - when string_of_mlpath p = "Steel.ST.Util.with_invariant" || - string_of_mlpath p = "Steel.Effect.Atomic.with_invariant" -> - Errors.raise_error - (Errors.Fatal_ExtractionUnsupported, - BU.format2 - "Extraction of with_invariant requires its argument to be a function literal \ - at extraction time, try marking its argument inline_for_extraction (%s, %s)" - (string_of_int (fst e.loc)) - (snd e.loc)) - Range.dummyRange - | MLE_App (head, args) -> EApp (translate_expr env head, List.map (translate_expr env) args) @@ -1241,7 +1156,7 @@ let translate_type_decl' env ty: option decl = Errors. log_issue Range.dummyRange (Errors.Warning_DefinitionNotTranslated, (BU.format1 "Error extracting type definition %s to KaRaMeL\n" name)); None -let translate_let env flavor lb: option decl = +let translate_let' env flavor lb: option decl = match lb with | { mllb_name = name; @@ -1308,29 +1223,6 @@ let translate_let env flavor lb: option decl = Some (DFunction (cc, meta, List.length tvars, t, name, binders, EAbortS msg)) end - | { - mllb_name = name; - mllb_tysc = Some (tvars, t); - mllb_def = { expr = MLE_App ({ - expr = MLE_TApp ({expr = MLE_Name p}, _)}, [ l ] ) }; - mllb_meta = meta - } - when string_of_mlpath p = "Steel.TLArray.create" -> - if List.mem Syntax.NoExtract meta then - None - else - // This is a global const array, defined using Steel.TLArray - let meta = translate_flags meta in - let env = List.fold_left (fun env name -> extend_t env name) env tvars in - let t = translate_type env t in - let name = env.module_name, name in - begin try - let expr = List.map (translate_expr env) (list_elements l) in - Some (DGlobal (meta, name, List.length tvars, t, EBufCreateL (Eternal, expr))) - with e -> - Errors. log_issue Range.dummyRange (Errors.Warning_DefinitionNotTranslated, (BU.format2 "Error extracting %s to KaRaMeL (%s)\n" (Syntax.string_of_mlpath name) (BU.print_exn e))); - Some (DGlobal (meta, name, List.length tvars, t, EAny)) - end | { mllb_name = name; mllb_tysc = Some (tvars, t); @@ -1366,6 +1258,22 @@ let translate_let env flavor lb: option decl = end; None +let translate_let_t = env -> mlletflavor -> mllb -> ML (option decl) +(* translate_let' is not recursive, so we can directly use it to initialize ref_translate_let *) +let ref_translate_let : ref translate_let_t = mk_ref translate_let' +let register_pre_translate_let + (f: translate_let_t) +: ML unit += let before : translate_let_t = !ref_translate_let in + let after : translate_let_t = fun e fl lb -> + try + f e fl lb + with NotSupportedByKrmlExtension -> before e fl lb + in + ref_translate_let := after +let translate_let env flavor lb: option decl = + !ref_translate_let env flavor lb + let translate_decl env d: list decl = match d with | MLM_Let (flavor, lbs) ->