-
Notifications
You must be signed in to change notification settings - Fork 22
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #568 from hacspec/fix-bad-break-constructor
fix(engine/phase/cf-into-monads): use `call_Constructor`, not `call`
- Loading branch information
Showing
8 changed files
with
255 additions
and
38 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
53 changes: 53 additions & 0 deletions
53
test-harness/src/snapshots/toolchain__enum-repr into-coq.snap
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,53 @@ | ||
| --- | ||
| source: test-harness/src/harness.rs | ||
| expression: snapshot | ||
| info: | ||
| kind: | ||
| Translate: | ||
| backend: coq | ||
| info: | ||
| name: enum-repr | ||
| manifest: enum-repr/Cargo.toml | ||
| description: ~ | ||
| spec: | ||
| optional: false | ||
| broken: false | ||
| issue_id: ~ | ||
| positive: true | ||
| snapshot: | ||
| stderr: true | ||
| stdout: true | ||
| include_flag: ~ | ||
| backend_options: ~ | ||
| --- | ||
| exit = 0 | ||
| stderr = ''' | ||
| Compiling enum-repr v0.1.0 (WORKSPACE_ROOT/enum-repr) | ||
| Finished dev [unoptimized + debuginfo] target(s) in XXs''' | ||
| [stdout] | ||
| diagnostics = [] | ||
|
|
||
| [stdout.files] | ||
| "Enum_repr.v" = ''' | ||
| (* File automatically generated by Hacspec *) | ||
| From Hacspec Require Import Hacspec_Lib MachineIntegers. | ||
| From Coq Require Import ZArith. | ||
| Import List.ListNotations. | ||
| Open Scope Z_scope. | ||
| Open Scope bool_scope. | ||
|
|
||
| Inductive t_Foo : Type := | ||
| | Foo_A : t_Foo | ||
| | Foo_B : t_Foo | ||
| | Foo_C : t_Foo. | ||
|
|
||
| (*Not implemented yet? todo(item)*) | ||
|
|
||
| Definition f (_ : unit) : int16 := | ||
| let _x := cast ((@repr WORDSIZE16 5).+(@repr WORDSIZE16 0)) : int16 in | ||
| cast ((@repr WORDSIZE16 9).+(@repr WORDSIZE16 0)). | ||
|
|
||
| Definition ff__CONST : int16 := | ||
| cast ((@repr WORDSIZE16 1).+(@repr WORDSIZE16 0)). | ||
| ''' |
48 changes: 48 additions & 0 deletions
48
test-harness/src/snapshots/toolchain__enum-repr into-fstar.snap
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,48 @@ | ||
| --- | ||
| source: test-harness/src/harness.rs | ||
| expression: snapshot | ||
| info: | ||
| kind: | ||
| Translate: | ||
| backend: fstar | ||
| info: | ||
| name: enum-repr | ||
| manifest: enum-repr/Cargo.toml | ||
| description: ~ | ||
| spec: | ||
| optional: false | ||
| broken: false | ||
| issue_id: ~ | ||
| positive: true | ||
| snapshot: | ||
| stderr: true | ||
| stdout: true | ||
| include_flag: ~ | ||
| backend_options: ~ | ||
| --- | ||
| exit = 0 | ||
| stderr = ''' | ||
| Compiling enum-repr v0.1.0 (WORKSPACE_ROOT/enum-repr) | ||
| Finished dev [unoptimized + debuginfo] target(s) in XXs''' | ||
| [stdout] | ||
| diagnostics = [] | ||
|
|
||
| [stdout.files] | ||
| "Enum_repr.fst" = ''' | ||
| module Enum_repr | ||
| #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" | ||
| open Core | ||
| open FStar.Mul | ||
|
|
||
| type t_Foo = | ||
| | Foo_A : t_Foo | ||
| | Foo_B : t_Foo | ||
| | Foo_C : t_Foo | ||
|
|
||
| let f (_: Prims.unit) : u16 = | ||
| let v__x:u16 = cast (5us +! 0us <: u16) <: u16 in | ||
| cast (9us +! 0us <: u16) <: u16 | ||
|
|
||
| let ff__CONST: u16 = cast (1us +! 0us <: u16) <: u16 | ||
| ''' |
89 changes: 89 additions & 0 deletions
89
test-harness/src/snapshots/toolchain__enum-repr into-ssprove.snap
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,89 @@ | ||
| --- | ||
| source: test-harness/src/harness.rs | ||
| expression: snapshot | ||
| info: | ||
| kind: | ||
| Translate: | ||
| backend: ssprove | ||
| info: | ||
| name: enum-repr | ||
| manifest: enum-repr/Cargo.toml | ||
| description: ~ | ||
| spec: | ||
| optional: false | ||
| broken: false | ||
| issue_id: ~ | ||
| positive: true | ||
| snapshot: | ||
| stderr: true | ||
| stdout: true | ||
| include_flag: ~ | ||
| backend_options: ~ | ||
| --- | ||
| exit = 0 | ||
| stderr = ''' | ||
| Compiling enum-repr v0.1.0 (WORKSPACE_ROOT/enum-repr) | ||
| Finished dev [unoptimized + debuginfo] target(s) in XXs''' | ||
| [stdout] | ||
| diagnostics = [] | ||
|
|
||
| [stdout.files] | ||
| "Enum_repr.v" = ''' | ||
| (* File automatically generated by Hacspec *) | ||
| Set Warnings "-notation-overridden,-ambiguous-paths". | ||
| From Crypt Require Import choice_type Package Prelude. | ||
| Import PackageNotation. | ||
| From extructures Require Import ord fset. | ||
| From mathcomp Require Import word_ssrZ word. | ||
| From Jasmin Require Import word. | ||
|
|
||
| From Coq Require Import ZArith. | ||
| From Coq Require Import Strings.String. | ||
| Import List.ListNotations. | ||
| Open Scope list_scope. | ||
| Open Scope Z_scope. | ||
| Open Scope bool_scope. | ||
|
|
||
| From Hacspec Require Import ChoiceEquality. | ||
| From Hacspec Require Import LocationUtility. | ||
| From Hacspec Require Import Hacspec_Lib_Comparable. | ||
| From Hacspec Require Import Hacspec_Lib_Pre. | ||
| From Hacspec Require Import Hacspec_Lib. | ||
|
|
||
| Open Scope hacspec_scope. | ||
| Import choice.Choice.Exports. | ||
|
|
||
| Obligation Tactic := (* try timeout 8 *) solve_ssprove_obligations. | ||
|
|
||
| Definition t_Foo : choice_type := | ||
| ('unit ∐ 'unit ∐ 'unit). | ||
| Notation "'Foo_A_case'" := (inl (inl tt)) (at level 100). | ||
| Equations Foo_A {L : {fset Location}} {I : Interface} : both L I t_Foo := | ||
| Foo_A := | ||
| solve_lift (ret_both (inl (inl (tt : 'unit)) : t_Foo)) : both L I t_Foo. | ||
| Fail Next Obligation. | ||
| Notation "'Foo_B_case'" := (inl (inr tt)) (at level 100). | ||
| Equations Foo_B {L : {fset Location}} {I : Interface} : both L I t_Foo := | ||
| Foo_B := | ||
| solve_lift (ret_both (inl (inr (tt : 'unit)) : t_Foo)) : both L I t_Foo. | ||
| Fail Next Obligation. | ||
| Notation "'Foo_C_case'" := (inr tt) (at level 100). | ||
| Equations Foo_C {L : {fset Location}} {I : Interface} : both L I t_Foo := | ||
| Foo_C := | ||
| solve_lift (ret_both (inr (tt : 'unit) : t_Foo)) : both L I t_Foo. | ||
| Fail Next Obligation. | ||
|
|
||
| (*Not implemented yet? todo(item)*) | ||
|
|
||
| Equations f {L1 : {fset Location}} {I1 : Interface} (_ : both L1 I1 'unit) : both L1 I1 int16 := | ||
| f _ := | ||
| letb v__x := cast_int (WS2 := _) ((ret_both (5 : int16)) .+ (ret_both (0 : int16))) in | ||
| solve_lift (cast_int (WS2 := _) ((ret_both (9 : int16)) .+ (ret_both (0 : int16)))) : both L1 I1 int16. | ||
| Fail Next Obligation. | ||
|
|
||
| Equations ff__CONST {L : {fset Location}} {I : Interface} : both L I int16 := | ||
| ff__CONST := | ||
| solve_lift (cast_int (WS2 := _) ((ret_both (1 : int16)) .+ (ret_both (0 : int16)))) : both L I int16. | ||
| Fail Next Obligation. | ||
| ''' |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.