From 9061313aad409b78f7d9917784529b92a02f2c36 Mon Sep 17 00:00:00 2001 From: Lasse Letager Hansen Date: Tue, 14 Nov 2023 14:44:38 +0100 Subject: [PATCH] Cleanup before pr --- engine/backends/coq/coq/coq_backend.ml | 15 --------------- engine/backends/coq/coq_ast.ml | 2 -- 2 files changed, 17 deletions(-) diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml index 1396ca571..6e56b1da8 100644 --- a/engine/backends/coq/coq/coq_backend.ml +++ b/engine/backends/coq/coq/coq_backend.ml @@ -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 diff --git a/engine/backends/coq/coq_ast.ml b/engine/backends/coq/coq_ast.ml index 676fb12e8..ee58a11dc 100644 --- a/engine/backends/coq/coq_ast.ml +++ b/engine/backends/coq/coq_ast.ml @@ -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