pub fn run(options: Options) -> Result<(), Box<dyn Error>> {
    let mut editor = {
        let config = Config::builder()
            .history_ignore_space(true)
            .history_ignore_dups(true)
            .build();

        Editor::<()>::with_config(config)
    };

    if editor.load_history(&options.history_file).is_err() {
        // No previous REPL history!
    }

    let mut files = Files::new();
    let context = mltt_elaborate::Context::default();

    let writer = StandardStream::stdout(ColorChoice::Always);

    loop {
        let line = editor.readline(&options.prompt);
        match line {
            Ok(line) => {
                let file_id = files.add("repl", line);

                editor.add_history_entry(files[file_id].contents());

                let lexer = Lexer::new(&files[file_id]);
                let concrete_term = match parser::parse_term(lexer) {
                    Ok(concrete_term) => concrete_term,
                    Err(diagnostic) => {
                        let config = language_reporting::DefaultConfig;
                        language_reporting::emit(&mut writer.lock(), &files, &diagnostic, &config)?;
                        continue;
                    },
                };

                let (core_term, ty) = match mltt_elaborate::synth_term(&context, &concrete_term) {
                    Ok((core_term, ty)) => (core_term, ty),
                    Err(diagnostic) => {
                        let config = language_reporting::DefaultConfig;
                        language_reporting::emit(&mut writer.lock(), &files, &diagnostic, &config)?;
                        continue;
                    },
                };

                let term_span = concrete_term.span();
                let term = context.normalize(term_span, &core_term).unwrap();
                let ty = context.read_back(None, &ty).unwrap();

                println!("{} : {}", term, ty);
            },
            Err(ReadlineError::Interrupted) => println!("Interrupted!"),
            Err(ReadlineError::Eof) => break,
            Err(error) => return Err(error.into()),
        }
    }

    editor.save_history(&options.history_file)?;

    println!("Bye bye");

    Ok(())
}
/// Run the REPL with the given options
Run the REPL with the given options
Run the REPL with the given options
pub fn run(options: Options) -> Result<(), Box<dyn Error>> {
    let mut editor = {
        let config = Config::builder()
            .history_ignore_space(true)
            .history_ignore_dups(true)
            .build();
        Editor::<()>::with_config(config)
    };
    if editor.load_history(&options.history_file).is_err() {
        // No previous REPL history!
    }
    let mut files = Files::new();
    let context = mltt_elaborate::Context::default();
    let writer = StandardStream::stdout(ColorChoice::Always);
    loop {
        let line = editor.readline(&options.prompt);
        match line {
            Ok(line) => {
                let file_id = files.add("repl", line);
                editor.add_history_entry(files[file_id].contents());
                let lexer = Lexer::new(&files[file_id]);
                let concrete_term = match parser::parse_term(lexer) {
                    Ok(concrete_term) => concrete_term,
                    Err(diagnostic) => {
                        let config = language_reporting::DefaultConfig;
                        language_reporting::emit(&mut writer.lock(), &files, &diagnostic, &config)?;
                        continue;
                    },
                };
                let (core_term, ty) = match mltt_elaborate::synth_term(&context, &concrete_term) {
                    Ok((core_term, ty)) => (core_term, ty),
                    Err(diagnostic) => {
                        let config = language_reporting::DefaultConfig;
                        language_reporting::emit(&mut writer.lock(), &files, &diagnostic, &config)?;
                        continue;
                    },
                };
                let term_span = concrete_term.span();
                let term = context.normalize(term_span, &core_term).unwrap();
                let ty = context.read_back(None, &ty).unwrap();
                println!("{} : {}", term, ty);
            },
            Err(ReadlineError::Interrupted) => println!("Interrupted!"),
            Err(ReadlineError::Eof) => break,
            Err(error) => return Err(error.into()),
        }
    }
    editor.save_history(&options.history_file)?;
    println!("Bye bye");
    Ok(())
}
pub fn run ( options : Options ) -> Result < ( ) , Box < dyn Error > > { let mut editor = { let config = Config :: builder ( ) . history_ignore_space ( true ) . history_ignore_dups ( true ) . build ( ) ; Editor :: < ( ) > :: with_config ( config ) } ; if editor . load_history ( & options . history_file ) . is_err ( ) { // No previous REPL history! } let mut files = Files :: new ( ) ; let context = mltt_elaborate :: Context :: default ( ) ; let writer = StandardStream :: stdout ( ColorChoice :: Always ) ; loop { let line = editor . readline ( & options . prompt ) ; match line { Ok ( line ) => { let file_id = files . add ( " " , line ) ; editor . add_history_entry ( files [ file_id ] . contents ( ) ) ; let lexer = Lexer :: new ( & files [ file_id ] ) ; let concrete_term = match parser :: parse_term ( lexer ) { Ok ( concrete_term ) => concrete_term , Err ( diagnostic ) => { let config = language_reporting :: DefaultConfig ; language_reporting :: emit ( & mut writer . lock ( ) , & files , & diagnostic , & config ) ? ; continue ; } , } ; let ( core_term , ty ) = match mltt_elaborate :: synth_term ( & context , & concrete_term ) { Ok ( ( core_term , ty ) ) => ( core_term , ty ) , Err ( diagnostic ) => { let config = language_reporting :: DefaultConfig ; language_reporting :: emit ( & mut writer . lock ( ) , & files , & diagnostic , & config ) ? ; continue ; } , } ; let term_span = concrete_term . span ( ) ; let term = context . normalize ( term_span , & core_term ) . unwrap ( ) ; let ty = context . read_back ( None , & ty ) . unwrap ( ) ; println ! ( " " term ty ) ; } , Err ( ReadlineError :: Interrupted ) => println ! ( " " ) , Err ( ReadlineError :: Eof ) => break , Err ( error ) => return Err ( error . into ( ) ) , } } editor . save_history ( & options . history_file ) ? ; println ! ( " " ) ; Ok ( ( ) ) }
Run the REPL with the given options
Run the REPL with the given options
options
Options