Skip to content

Commit

Permalink
Cleanup before pr
Browse files Browse the repository at this point in the history
  • Loading branch information
cmester0 committed Nov 15, 2023
1 parent b47b423 commit 9061313
Show file tree
Hide file tree
Showing 2 changed files with 0 additions and 17 deletions.
15 changes: 0 additions & 15 deletions engine/backends/coq/coq/coq_backend.ml
Original file line number Diff line number Diff line change
Expand Up @@ -70,27 +70,12 @@ open AST

module CoqLibrary : Library = struct
module Notation = struct
let additional_identifier : string = ""

let int_repr (x : string) (i : string) : string =
"(@repr" ^ " " ^ "WORDSIZE" ^ x ^ " " ^ i ^ ")"

let let_stmt (var : string) (expr : string) (typ : string) (body : string)
(depth : int) : string =
"let" ^ " " ^ var ^ " " ^ ":=" ^ " (" ^ expr ^ ") " ^ ":" ^ " " ^ typ
^ " " ^ "in" ^ newline_indent depth ^ body

let let_mut_stmt = let_stmt
let let_bind_stmt = let_stmt (* TODO *)
let let_bind_mut_stmt = let_stmt
let type_str : string = "Type"
let bool_str : string = "bool"
let unit_str : string = "unit"

let if_stmt (cond : string) (then_e : string) (else_e : string)
(depth : int) : string =
"if" ^ " " ^ cond ^ newline_indent depth ^ "then" ^ " " ^ then_e
^ newline_indent depth ^ "else" ^ " " ^ else_e
end
end

Expand Down
2 changes: 0 additions & 2 deletions engine/backends/coq/coq_ast.ml
Original file line number Diff line number Diff line change
Expand Up @@ -4,12 +4,10 @@ open Base

module type Library = sig
module Notation : sig
val additional_identifier : string
val int_repr : string -> string -> string
val type_str : string
val bool_str : string
val unit_str : string
val if_stmt : string -> string -> string -> int -> string
end
end

Expand Down

0 comments on commit 9061313

Please sign in to comment.