Skip to content

Commit

Permalink
refactor(engine/fstar-ast): get rid of zarith and GMP
Browse files Browse the repository at this point in the history
  • Loading branch information
Lucas Franceschino authored and W95Psp committed Jun 26, 2024
1 parent 18e21e2 commit 6013d42
Show file tree
Hide file tree
Showing 38 changed files with 217 additions and 5,890 deletions.
18 changes: 9 additions & 9 deletions engine/backends/fstar/fstar-surface-ast/FStar_BaseTypes.ml
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
type char = FStar_Char.char[@@deriving yojson,show]
type float = FStar_Float.float[@@deriving yojson,show]
type double = FStar_Float.double[@@deriving yojson,show]
type byte = FStar_UInt8.byte[@@deriving yojson,show]
type int8 = FStar_Int8.int8
type uint8 = FStar_UInt8.uint8
type int16 = FStar_Int16.int16
type uint16 = FStar_UInt16.uint16
type int32 = FStar_Int32.int32
type int64 = FStar_Int64.int64
type float = Base.Float.t
type double = Base.Float.t
type byte = Base.Int.t
type int8 = Stdint.Int8.t
type uint8 = Stdint.Uint8.t
type int16 = Stdint.Int16.t
type uint16 = Stdint.Uint16.t
type int32 = Stdint.Int32.t
type int64 = Stdint.Int64.t
44 changes: 0 additions & 44 deletions engine/backends/fstar/fstar-surface-ast/FStar_BigInt.ml

This file was deleted.

19 changes: 0 additions & 19 deletions engine/backends/fstar/fstar-surface-ast/FStar_Char.ml
Original file line number Diff line number Diff line change
@@ -1,21 +1,2 @@
module UChar = BatUChar

module U32 = FStar_UInt32

type char = int[@@deriving yojson,show]
type char_code = U32.t

(* FIXME(adl) UChar.lowercase/uppercase removed from recent Batteries. Use Camomile? *)
let lowercase (x:char) : char =
try Char.code (Char.lowercase_ascii (Char.chr x))
with _ -> x

let uppercase (x:char) : char =
try Char.code (Char.uppercase_ascii (Char.chr x))
with _ -> x

let int_of_char (x:char) : Z.t= Z.of_int x
let char_of_int (i:Z.t) : char = Z.to_int i

let u32_of_char (x:char) : char_code = U32.of_native_int x
let char_of_u32 (x:char_code) : char = U32.to_native_int x
177 changes: 0 additions & 177 deletions engine/backends/fstar/fstar-surface-ast/FStar_Common.ml

This file was deleted.

19 changes: 0 additions & 19 deletions engine/backends/fstar/fstar-surface-ast/FStar_CommonST.ml

This file was deleted.

37 changes: 0 additions & 37 deletions engine/backends/fstar/fstar-surface-ast/FStar_Compiler_Option.ml

This file was deleted.

Loading

0 comments on commit 6013d42

Please sign in to comment.