mirror of
https://github.com/ProvableHQ/leo.git
synced 2024-11-27 02:24:15 +03:00
Refactor Proof/Theorem to Snapshots
This commit is contained in:
parent
2f000a971a
commit
add64ae11a
@ -18,11 +18,11 @@
|
||||
use crate::{
|
||||
constraints::{generate_constraints, generate_test_constraints},
|
||||
errors::CompilerError,
|
||||
AstSnapshotOptions,
|
||||
CompilerOptions,
|
||||
GroupType,
|
||||
Output,
|
||||
OutputFile,
|
||||
TheoremOptions,
|
||||
TypeInferencePhase,
|
||||
};
|
||||
pub use leo_asg::{new_context, AsgContext as Context, AsgContext};
|
||||
@ -67,7 +67,7 @@ pub struct Compiler<'a, F: PrimeField, G: GroupType<F>> {
|
||||
context: AsgContext<'a>,
|
||||
asg: Option<AsgProgram<'a>>,
|
||||
options: CompilerOptions,
|
||||
proof_options: TheoremOptions,
|
||||
ast_snapshot_options: AstSnapshotOptions,
|
||||
_engine: PhantomData<F>,
|
||||
_group: PhantomData<G>,
|
||||
}
|
||||
@ -82,7 +82,7 @@ impl<'a, F: PrimeField, G: GroupType<F>> Compiler<'a, F, G> {
|
||||
output_directory: PathBuf,
|
||||
context: AsgContext<'a>,
|
||||
options: Option<CompilerOptions>,
|
||||
proof_options: Option<TheoremOptions>,
|
||||
ast_snapshot_options: Option<AstSnapshotOptions>,
|
||||
) -> Self {
|
||||
Self {
|
||||
program_name: package_name.clone(),
|
||||
@ -93,7 +93,7 @@ impl<'a, F: PrimeField, G: GroupType<F>> Compiler<'a, F, G> {
|
||||
asg: None,
|
||||
context,
|
||||
options: options.unwrap_or_default(),
|
||||
proof_options: proof_options.unwrap_or_default(),
|
||||
ast_snapshot_options: ast_snapshot_options.unwrap_or_default(),
|
||||
_engine: PhantomData,
|
||||
_group: PhantomData,
|
||||
}
|
||||
@ -112,7 +112,7 @@ impl<'a, F: PrimeField, G: GroupType<F>> Compiler<'a, F, G> {
|
||||
output_directory: PathBuf,
|
||||
context: AsgContext<'a>,
|
||||
options: Option<CompilerOptions>,
|
||||
proof_options: Option<TheoremOptions>,
|
||||
ast_snapshot_options: Option<AstSnapshotOptions>,
|
||||
) -> Result<Self, CompilerError> {
|
||||
let mut compiler = Self::new(
|
||||
package_name,
|
||||
@ -120,7 +120,7 @@ impl<'a, F: PrimeField, G: GroupType<F>> Compiler<'a, F, G> {
|
||||
output_directory,
|
||||
context,
|
||||
options,
|
||||
proof_options,
|
||||
ast_snapshot_options,
|
||||
);
|
||||
|
||||
compiler.parse_program()?;
|
||||
@ -151,7 +151,7 @@ impl<'a, F: PrimeField, G: GroupType<F>> Compiler<'a, F, G> {
|
||||
state_path: &Path,
|
||||
context: AsgContext<'a>,
|
||||
options: Option<CompilerOptions>,
|
||||
proof_options: Option<TheoremOptions>,
|
||||
ast_snapshot_options: Option<AstSnapshotOptions>,
|
||||
) -> Result<Self, CompilerError> {
|
||||
let mut compiler = Self::new(
|
||||
package_name,
|
||||
@ -159,7 +159,7 @@ impl<'a, F: PrimeField, G: GroupType<F>> Compiler<'a, F, G> {
|
||||
output_directory,
|
||||
context,
|
||||
options,
|
||||
proof_options,
|
||||
ast_snapshot_options,
|
||||
);
|
||||
|
||||
compiler.parse_input(input_string, input_path, state_string, state_path)?;
|
||||
@ -240,7 +240,7 @@ impl<'a, F: PrimeField, G: GroupType<F>> Compiler<'a, F, G> {
|
||||
|
||||
let mut ast: leo_ast::Ast = parse_ast(self.main_file_path.to_str().unwrap_or_default(), program_string)?;
|
||||
|
||||
if self.proof_options.initial {
|
||||
if self.ast_snapshot_options.initial {
|
||||
ast.to_json_file(self.output_directory.clone(), "initial_ast.json")?;
|
||||
}
|
||||
|
||||
@ -248,7 +248,7 @@ impl<'a, F: PrimeField, G: GroupType<F>> Compiler<'a, F, G> {
|
||||
if self.options.canonicalization_enabled {
|
||||
ast.canonicalize()?;
|
||||
|
||||
if self.proof_options.canonicalized {
|
||||
if self.ast_snapshot_options.canonicalized {
|
||||
ast.to_json_file(self.output_directory.clone(), "canonicalization_ast.json")?;
|
||||
}
|
||||
}
|
||||
@ -266,7 +266,7 @@ impl<'a, F: PrimeField, G: GroupType<F>> Compiler<'a, F, G> {
|
||||
&mut leo_imports::ImportParser::new(self.main_file_path.clone()),
|
||||
)?;
|
||||
|
||||
if self.proof_options.type_inferenced {
|
||||
if self.ast_snapshot_options.type_inferenced {
|
||||
let new_ast = TypeInferencePhase::default()
|
||||
.phase_ast(&self.program, &asg.clone().into_repr())
|
||||
.expect("Failed to produce type inference ast.");
|
||||
|
@ -38,13 +38,13 @@ impl Default for CompilerOptions {
|
||||
}
|
||||
|
||||
#[derive(Clone)]
|
||||
pub struct TheoremOptions {
|
||||
pub struct AstSnapshotOptions {
|
||||
pub initial: bool,
|
||||
pub canonicalized: bool,
|
||||
pub type_inferenced: bool,
|
||||
}
|
||||
|
||||
impl Default for TheoremOptions {
|
||||
impl Default for AstSnapshotOptions {
|
||||
fn default() -> Self {
|
||||
Self {
|
||||
initial: false,
|
||||
|
@ -18,8 +18,8 @@ use crate::{commands::Command, context::Context};
|
||||
use leo_compiler::{
|
||||
compiler::{thread_leaked_context, Compiler},
|
||||
group::targets::edwards_bls12::EdwardsGroupType,
|
||||
AstSnapshotOptions,
|
||||
CompilerOptions,
|
||||
TheoremOptions,
|
||||
};
|
||||
use leo_package::{
|
||||
inputs::*,
|
||||
@ -44,14 +44,14 @@ pub struct BuildOptions {
|
||||
pub disable_code_elimination: bool,
|
||||
#[structopt(long, help = "Disable all compiler optimizations")]
|
||||
pub disable_all_optimizations: bool,
|
||||
#[structopt(long, help = "Writes all theorem input AST files.")]
|
||||
pub enable_all_theorems: bool,
|
||||
#[structopt(long, help = "Writes AST files needed for the initial theorem before any changes.")]
|
||||
pub enable_initial_theorem: bool,
|
||||
#[structopt(long, help = "Writes AST files needed for canonicalization theorem.")]
|
||||
pub enable_canonicalized_theorem: bool,
|
||||
#[structopt(long, help = "Writes AST files needed for type inference theorem.")]
|
||||
pub enable_type_inferenced_theorem: bool,
|
||||
#[structopt(long, help = "Writes all AST snapshots for the different compiler phases.")]
|
||||
pub enable_all_ast_snapshots: bool,
|
||||
#[structopt(long, help = "Writes AST snapshot of the initial parse.")]
|
||||
pub enable_initial_ast_snapshot: bool,
|
||||
#[structopt(long, help = "Writes AST snapshot after the canonicalization phase.")]
|
||||
pub enable_canonicalized_ast_snapshot: bool,
|
||||
#[structopt(long, help = "Writes AST snapshot after the type inference phase.")]
|
||||
pub enable_type_inferenced_ast_snapshot: bool,
|
||||
}
|
||||
|
||||
impl Default for BuildOptions {
|
||||
@ -60,10 +60,10 @@ impl Default for BuildOptions {
|
||||
disable_constant_folding: true,
|
||||
disable_code_elimination: true,
|
||||
disable_all_optimizations: true,
|
||||
enable_all_theorems: false,
|
||||
enable_initial_theorem: false,
|
||||
enable_canonicalized_theorem: false,
|
||||
enable_type_inferenced_theorem: false,
|
||||
enable_all_ast_snapshots: false,
|
||||
enable_initial_ast_snapshot: false,
|
||||
enable_canonicalized_ast_snapshot: false,
|
||||
enable_type_inferenced_ast_snapshot: false,
|
||||
}
|
||||
}
|
||||
}
|
||||
@ -86,19 +86,19 @@ impl From<BuildOptions> for CompilerOptions {
|
||||
}
|
||||
}
|
||||
|
||||
impl From<BuildOptions> for TheoremOptions {
|
||||
impl From<BuildOptions> for AstSnapshotOptions {
|
||||
fn from(options: BuildOptions) -> Self {
|
||||
if options.enable_all_theorems {
|
||||
TheoremOptions {
|
||||
if options.enable_all_ast_snapshots {
|
||||
AstSnapshotOptions {
|
||||
initial: true,
|
||||
canonicalized: true,
|
||||
type_inferenced: true,
|
||||
}
|
||||
} else {
|
||||
TheoremOptions {
|
||||
initial: options.enable_initial_theorem,
|
||||
canonicalized: options.enable_canonicalized_theorem,
|
||||
type_inferenced: options.enable_type_inferenced_theorem,
|
||||
AstSnapshotOptions {
|
||||
initial: options.enable_initial_ast_snapshot,
|
||||
canonicalized: options.enable_canonicalized_ast_snapshot,
|
||||
type_inferenced: options.enable_type_inferenced_ast_snapshot,
|
||||
}
|
||||
}
|
||||
}
|
||||
|
Loading…
Reference in New Issue
Block a user