Skip to content

Commit

Permalink
snapshot
Browse files Browse the repository at this point in the history
  • Loading branch information
@cmester0
cmester0 committed Nov 25, 2024
1 parent eeedd11 commit 5832f3f
Show file tree
Hide file tree
Showing 11 changed files with 69 additions and 295 deletions.
14 changes: 7 additions & 7 deletions .github/workflows/extract_and_run_coq.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,20 +21,20 @@ jobs:
run: |
nix run . into coq
- name: install annotated core for coq
working-directory: hax/proof-libs/coq/coq/generated-core
run: |
nix-shell --packages coq coqPackages.coq-record-update --run "coq_makefile -f _CoqProject -o Makefile" && \
nix-shell --packages coq coqPackages.coq-record-update --run "make"
nix-shell --packages coq coqPackages.coq-record-update --run "make install"
- name: run coq - coverage
working-directory: hax/examples/coverage/proofs/coq/extraction
run: |
sed 's/_impl_f_/_f_/' < Coverage_Test_instance.v > Coverage_Test_instance.v # TODO: this is a hotfix, should be solved in backend and removed from here.
nix-shell --packages coq coqPackages.coq-record-update --run "coq_makefile -f _CoqProject -o Makefile"
nix-shell --packages coq coqPackages.coq-record-update --run "make"
- name: build and run coq on tests
working-directory: hax/proof-libs/coq/coq/generated-core
run: |
nix-shell --packages coq coqPackages.coq-record-update --run "coq_makefile -f _CoqProject -o Makefile" && \
nix-shell --packages coq coqPackages.coq-record-update --run "make"
nix-shell --packages coq coqPackages.coq-record-update --run "make install"
- name: build and run coq on tests
env:
FILES: assert attribute-opaque constructor-as-closure enum-repr enum-struct-variant even
Expand Down
7 changes: 3 additions & 4 deletions engine/backends/coq/coq/coq_backend.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -366,7 +366,8 @@ struct
string "let" ^^ space ^^ lhs#p ^^ space ^^ string ":=" ^^ space ^^ rhs#p
^^ space ^^ string "in" ^^ break 1 ^^ body#p

method expr'_Literal ~super:_ x2 = x2#p
method expr'_Literal ~super x2 =
parens(x2#p ^^ space ^^ colon ^^ space ^^ (self#_do_not_override_lazy_of_ty AstPos_expr'_Literal_x0 super.typ)#p)
method expr'_LocalVar ~super:_ x2 = x2#p

method expr'_Loop ~super:_ ~body ~kind ~state ~control_flow ~label:_
Expand Down Expand Up @@ -781,10 +782,8 @@ struct
^^ string "%float"

method literal_Int ~value ~negative ~kind =
parens
((if negative then !^"-" else empty)
^^ string value ^^ colon ^^ space ^^ !^"t_"
^^ string (show_int_kind kind))
^^ string value)

method literal_String x1 = string "\"" ^^ string x1 ^^ string "\"%string"

Expand Down
35 changes: 5 additions & 30 deletions test-harness/src/snapshots/toolchain__assert into-coq.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,45 +38,20 @@ Require Import String.
Require Import Coq.Floats.Floats.
From RecordUpdate Require Import RecordSet.
Import RecordSetNotations.

(* From Core Require Import Core. *)

(* TODO: Replace this dummy lib with core lib *)
Class t_Sized (T : Type) := { }.
Definition t_u8 := Z.
Definition t_u16 := Z.
Definition t_u32 := Z.
Definition t_u64 := Z.
Definition t_u128 := Z.
Definition t_usize := Z.
Definition t_i8 := Z.
Definition t_i16 := Z.
Definition t_i32 := Z.
Definition t_i64 := Z.
Definition t_i128 := Z.
Definition t_isize := Z.
Definition t_Array T (x : t_usize) := list T.
Definition t_String := string.
Definition ToString_f_to_string (x : string) := x.
Instance Sized_any : forall {t_A}, t_Sized t_A := {}.
Class t_Clone (T : Type) := { Clone_f_clone : T -> T }.
Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x => x}.
Definition t_Slice (T : Type) := list T.
Definition unsize {T : Type} : list T -> t_Slice T := id.
(* / dummy lib *)
From Core Require Import Core.



(* NotImplementedYet *)

Definition asserts '(_ : unit) : unit :=
let _ := assert (true) in
let _ := assert (t_PartialEq_f_eq (1) (1)) in
let _ := match (2,2) with
let _ := assert ((true : bool)) in
let _ := assert (t_PartialEq_f_eq ((1 : t_i32)) ((1 : t_i32))) in
let _ := match ((2 : t_i32),(2 : t_i32)) with
| (left_val,right_val) =>
assert (t_PartialEq_f_eq (left_val) (right_val))
end in
let _ := match (1,2) with
let _ := match ((1 : t_i32),(2 : t_i32)) with
| (left_val,right_val) =>
assert (negb (t_PartialEq_f_eq (left_val) (right_val)))
end in
Expand Down
39 changes: 7 additions & 32 deletions test-harness/src/snapshots/toolchain__enum-repr into-coq.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -39,40 +39,15 @@ Require Import String.
Require Import Coq.Floats.Floats.
From RecordUpdate Require Import RecordSet.
Import RecordSetNotations.

(* From Core Require Import Core. *)

(* TODO: Replace this dummy lib with core lib *)
Class t_Sized (T : Type) := { }.
Definition t_u8 := Z.
Definition t_u16 := Z.
Definition t_u32 := Z.
Definition t_u64 := Z.
Definition t_u128 := Z.
Definition t_usize := Z.
Definition t_i8 := Z.
Definition t_i16 := Z.
Definition t_i32 := Z.
Definition t_i64 := Z.
Definition t_i128 := Z.
Definition t_isize := Z.
Definition t_Array T (x : t_usize) := list T.
Definition t_String := string.
Definition ToString_f_to_string (x : string) := x.
Instance Sized_any : forall {t_A}, t_Sized t_A := {}.
Class t_Clone (T : Type) := { Clone_f_clone : T -> T }.
Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x => x}.
Definition t_Slice (T : Type) := list T.
Definition unsize {T : Type} : list T -> t_Slice T := id.
(* / dummy lib *)
From Core Require Import Core.



Definition discriminant_EnumWithRepr_ExplicitDiscr1 : t_u16 :=
1.
(1 : t_u16).

Definition discriminant_EnumWithRepr_ExplicitDiscr2 : t_u16 :=
5.
(5 : t_u16).

Inductive t_EnumWithRepr : Type :=
| EnumWithRepr_ExplicitDiscr1
Expand All @@ -91,19 +66,19 @@ Definition t_EnumWithRepr_cast_to_repr (x : t_EnumWithRepr) : t_u16 :=
| EnumWithRepr_ExplicitDiscr2 =>
discriminant_EnumWithRepr_ExplicitDiscr2
| EnumWithRepr_ImplicitDiscrEmptyTuple =>
t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) (1)
t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) ((1 : t_u16))
| EnumWithRepr_ImplicitDiscrEmptyStruct =>
t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) (2)
t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) ((2 : t_u16))
end.

(* NotImplementedYet *)

Definition f '(_ : unit) : t_u32 :=
let v__x := cast (t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) (0)) in
let v__x := cast (t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr2) ((0 : t_u16))) in
t_Add_f_add (cast (t_EnumWithRepr_cast_to_repr (EnumWithRepr_ImplicitDiscrEmptyTuple))) (cast (t_EnumWithRepr_cast_to_repr (EnumWithRepr_ImplicitDiscrEmptyStruct))).

Definition ff__CONST : t_u16 :=
cast (t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr1) (0)).
cast (t_Add_f_add (discriminant_EnumWithRepr_ExplicitDiscr1) ((0 : t_u16))).

Definition get_casted_repr (x : t_EnumWithRepr) : t_u64 :=
cast (t_EnumWithRepr_cast_to_repr (x)).
Expand Down
47 changes: 11 additions & 36 deletions test-harness/src/snapshots/toolchain__guards into-coq.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,32 +38,7 @@ Require Import String.
Require Import Coq.Floats.Floats.
From RecordUpdate Require Import RecordSet.
Import RecordSetNotations.

(* From Core Require Import Core. *)

(* TODO: Replace this dummy lib with core lib *)
Class t_Sized (T : Type) := { }.
Definition t_u8 := Z.
Definition t_u16 := Z.
Definition t_u32 := Z.
Definition t_u64 := Z.
Definition t_u128 := Z.
Definition t_usize := Z.
Definition t_i8 := Z.
Definition t_i16 := Z.
Definition t_i32 := Z.
Definition t_i64 := Z.
Definition t_i128 := Z.
Definition t_isize := Z.
Definition t_Array T (x : t_usize) := list T.
Definition t_String := string.
Definition ToString_f_to_string (x : string) := x.
Instance Sized_any : forall {t_A}, t_Sized t_A := {}.
Class t_Clone (T : Type) := { Clone_f_clone : T -> T }.
Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x => x}.
Definition t_Slice (T : Type) := list T.
Definition unsize {T : Type} : list T -> t_Slice T := id.
(* / dummy lib *)
From Core Require Import Core.



Expand All @@ -72,7 +47,7 @@ Definition unsize {T : Type} : list T -> t_Slice T := id.
Definition equivalent (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 :=
match x with
| Option_None =>
0
(0 : t_i32)
| _ =>
match match x with
| Option_Some (v) =>
Expand All @@ -92,15 +67,15 @@ Definition equivalent (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 :=
| Option_Some (Result_Err (y)) =>
y
| _ =>
1
(1 : t_i32)
end
end
end.

Definition if_guard (x : t_Option ((t_i32))) : t_i32 :=
match match x with
| Option_Some (v) =>
match t_PartialOrd_f_gt (v) (0) with
match t_PartialOrd_f_gt (v) ((0 : t_i32)) with
| true =>
Option_Some (v)
| _ =>
Expand All @@ -112,13 +87,13 @@ Definition if_guard (x : t_Option ((t_i32))) : t_i32 :=
| Option_Some (x) =>
x
| Option_None =>
0
(0 : t_i32)
end.

Definition if_let_guard (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 :=
match x with
| Option_None =>
0
(0 : t_i32)
| _ =>
match match x with
| Option_Some (v) =>
Expand All @@ -138,21 +113,21 @@ Definition if_let_guard (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32
| Option_Some (Result_Err (y)) =>
y
| _ =>
1
(1 : t_i32)
end
end
end.

Definition multiple_guards (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i32 :=
match x with
| Option_None =>
0
(0 : t_i32)
| _ =>
match match x with
| Option_Some (Result_Ok (v)) =>
match Option_Some (t_Add_f_add (v) (1)) with
match Option_Some (t_Add_f_add (v) ((1 : t_i32))) with
| Option_Some (1) =>
Option_Some (0)
Option_Some ((0 : t_i32))
| _ =>
Option_None
end
Expand Down Expand Up @@ -180,7 +155,7 @@ Definition multiple_guards (x : t_Option ((t_Result ((t_i32)) ((t_i32))))) : t_i
| Option_Some (Result_Err (y)) =>
y
| _ =>
1
(1 : t_i32)
end
end
end
Expand Down
27 changes: 1 addition & 26 deletions test-harness/src/snapshots/toolchain__include-flag into-coq.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,32 +38,7 @@ Require Import String.
Require Import Coq.Floats.Floats.
From RecordUpdate Require Import RecordSet.
Import RecordSetNotations.

(* From Core Require Import Core. *)

(* TODO: Replace this dummy lib with core lib *)
Class t_Sized (T : Type) := { }.
Definition t_u8 := Z.
Definition t_u16 := Z.
Definition t_u32 := Z.
Definition t_u64 := Z.
Definition t_u128 := Z.
Definition t_usize := Z.
Definition t_i8 := Z.
Definition t_i16 := Z.
Definition t_i32 := Z.
Definition t_i64 := Z.
Definition t_i128 := Z.
Definition t_isize := Z.
Definition t_Array T (x : t_usize) := list T.
Definition t_String := string.
Definition ToString_f_to_string (x : string) := x.
Instance Sized_any : forall {t_A}, t_Sized t_A := {}.
Class t_Clone (T : Type) := { Clone_f_clone : T -> T }.
Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x => x}.
Definition t_Slice (T : Type) := list T.
Definition unsize {T : Type} : list T -> t_Slice T := id.
(* / dummy lib *)
From Core Require Import Core.



Expand Down
35 changes: 5 additions & 30 deletions test-harness/src/snapshots/toolchain__let-else into-coq.snap
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,32 +38,7 @@ Require Import String.
Require Import Coq.Floats.Floats.
From RecordUpdate Require Import RecordSet.
Import RecordSetNotations.

(* From Core Require Import Core. *)

(* TODO: Replace this dummy lib with core lib *)
Class t_Sized (T : Type) := { }.
Definition t_u8 := Z.
Definition t_u16 := Z.
Definition t_u32 := Z.
Definition t_u64 := Z.
Definition t_u128 := Z.
Definition t_usize := Z.
Definition t_i8 := Z.
Definition t_i16 := Z.
Definition t_i32 := Z.
Definition t_i64 := Z.
Definition t_i128 := Z.
Definition t_isize := Z.
Definition t_Array T (x : t_usize) := list T.
Definition t_String := string.
Definition ToString_f_to_string (x : string) := x.
Instance Sized_any : forall {t_A}, t_Sized t_A := {}.
Class t_Clone (T : Type) := { Clone_f_clone : T -> T }.
Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x => x}.
Definition t_Slice (T : Type) := list T.
Definition unsize {T : Type} : list T -> t_Slice T := id.
(* / dummy lib *)
From Core Require Import Core.



Expand All @@ -72,17 +47,17 @@ Definition unsize {T : Type} : list T -> t_Slice T := id.
Definition let_else (opt : t_Option ((t_u32))) : bool :=
run (match opt with
| Option_Some (x) =>
ControlFlow_Continue (true)
ControlFlow_Continue ((true : bool))
| _ =>
ControlFlow_Break (false)
ControlFlow_Break ((false : bool))
end).

Definition let_else_different_type (opt : t_Option ((t_u32))) : bool :=
run (let hoist1 := match opt with
| Option_Some (x) =>
ControlFlow_Continue (Option_Some (t_Add_f_add (x) (1)))
ControlFlow_Continue (Option_Some (t_Add_f_add (x) ((1 : t_u32))))
| _ =>
ControlFlow_Break (false)
ControlFlow_Break ((false : bool))
end in
ControlFlow_Continue (let_else (hoist1))).
'''
Expand Down
Loading

0 comments on commit 5832f3f

Please sign in to comment.