diff --git a/vim-saw/doc/saw.txt b/vim-saw/doc/saw.txt new file mode 100644 index 0000000000..820f6291e5 --- /dev/null +++ b/vim-saw/doc/saw.txt @@ -0,0 +1,10 @@ +*saw.txt* functionality for developing sawscript scripts + +This plugin adds basic syntax highlighting and a vim-slime override. This +allows using vim-slime to send sawscript snippets from a sawscript file to a +running sawscript interpreter. See the official vim-slime documentation for how +to use vim-slime. The most basic command is , which sends the whole +paragraph the cursor is in. Note that the saw interpreter will correctly parse +single top-level statements, but not multpile top-level statements. + +Dependencies: vim-slime diff --git a/vim-saw/ftdetect/saw.vim b/vim-saw/ftdetect/saw.vim new file mode 100644 index 0000000000..121b01ba77 --- /dev/null +++ b/vim-saw/ftdetect/saw.vim @@ -0,0 +1 @@ +autocmd BufNewFile,BufRead *.saw set filetype=saw diff --git a/vim-saw/plugin/saw.vim b/vim-saw/plugin/saw.vim new file mode 100644 index 0000000000..75b6225b63 --- /dev/null +++ b/vim-saw/plugin/saw.vim @@ -0,0 +1,18 @@ +" a function that overrides vim-slime's default behavior: +function SlimeOverride_EscapeText_saw(text) + " create temp buffer + split __saw_slime_temp_buffer__ + setlocal buftype=nofile + " paste text in buffer + set paste + exe "normal! i" . a:text . "\" + set nopaste + " remove blank things: + silent! keepp g/^\s*\n/d + silent! keepp g/^\n/d + silent! keepp g/^\s*\/\/.*\n/d + silent! keepp %s/\/\/.*$//eg " remove end-of-line comments + let res = join(getline(1, '$'), "\\\n") " copy buffer contents into res, adding a backslash at the end of each line + bdelete __saw_slime_temp_buffer__ " delete temp buffer (the following didn't work reliably: setlocal bufhidden=delete) + return res . "\n" +endfunction diff --git a/vim-saw/syntax/saw.vim b/vim-saw/syntax/saw.vim new file mode 100644 index 0000000000..98455932ec --- /dev/null +++ b/vim-saw/syntax/saw.vim @@ -0,0 +1,10 @@ +hi link SAWKeyword Keyword +setlocal commentstring=//%s " is this useless? the doc says only used for folding +setlocal comments=s1:/*,mb:*,ex:*/,://" +syntax match SAWComment "\v//.*$" contains=@Spell +syntax region SAWComment start="/\*" end="\*/" contains=@Spell +highlight link SAWComment Comment +setlocal formatoptions=tcqr + +" all SAW builtins included: +syn keyword SAWKeyword do let import abc get_opt offline_cnf abstract_symbolic goal_apply offline_cnf_external add_cryptol_defs goal_assume offline_coq add_cryptol_eqs goal_eval offline_extcore add_prelude_defs goal_eval_unint offline_smtlib2 add_prelude_eqs goal_insert offline_unint_smtlib2 add_x86_preserved_reg goal_intro offline_verilog addsimp goal_num_ite offline_w4_unint_cvc4 addsimp' goal_num_when offline_w4_unint_yices addsimps goal_when offline_w4_unint_z3 addsimps' head parse_core admit hoist_ifs parser_printer_roundtrip approxmc include print assume_unsat java_array print_goal assume_valid java_bool print_goal_consts auto_match java_byte print_goal_depth basic_ss java_char print_goal_size beta_reduce_goal java_class print_term beta_reduce_term java_double print_term_depth boolector java_float print_type caseProofResult java_int prove caseSatResult java_load_class prove_core check_convertible java_long prove_print check_goal java_short qc_print check_term jvm_alloc_array quickcheck codegen jvm_alloc_object read_aig concat jvm_array_is read_bytes core_axiom jvm_elem_is read_core core_thm jvm_execute_func replace crucible_alloc jvm_extract return crucible_alloc_aligned jvm_field_is rewrite crucible_alloc_global jvm_fresh_var rme crucible_alloc_readonly jvm_modifies_elem run crucible_alloc_readonly_aligned jvm_modifies_field sat crucible_alloc_with_size jvm_modifies_static_field sat_print crucible_array jvm_null sbv_abc crucible_conditional_points_to jvm_postcond sbv_boolector crucible_conditional_points_to_untyped jvm_precond sbv_cvc4 crucible_declare_ghost_state jvm_return sbv_mathsat crucible_elem jvm_static_field_is sbv_unint_cvc4 crucible_equal jvm_term sbv_unint_yices crucible_execute_func jvm_unsafe_assume_spec sbv_unint_z3 crucible_field jvm_verify sbv_yices crucible_fresh_cryptol_var lambda sbv_z3 crucible_fresh_expanded_val lambdas set_ascii crucible_fresh_pointer length set_base crucible_fresh_var list_term set_color crucible_ghost_value llvm_alias set_timeout crucible_global llvm_alloc set_x86_stack_base_align crucible_global_initializer llvm_alloc_aligned sharpSAT crucible_java_extract llvm_alloc_global show crucible_llvm_array_size_profile llvm_alloc_readonly show_cfg crucible_llvm_compositional_extract llvm_alloc_readonly_aligned show_term crucible_llvm_extract llvm_alloc_with_size simplify crucible_llvm_unsafe_assume_spec llvm_array skeleton_arg crucible_llvm_verify llvm_array_size_profile skeleton_arg_index crucible_llvm_verify_x86 llvm_array_value skeleton_arg_index_pointer crucible_null llvm_boilerplate skeleton_arg_pointer crucible_packed_struct llvm_cfg skeleton_exec crucible_points_to llvm_compositional_extract skeleton_globals_post crucible_points_to_array_prefix llvm_conditional_points_to skeleton_globals_pre crucible_points_to_untyped llvm_conditional_points_to_at_type skeleton_guess_arg_sizes crucible_postcond llvm_conditional_points_to_untyped skeleton_poststate crucible_precond llvm_declare_ghost_state skeleton_prestate crucible_return llvm_double skeleton_resize_arg crucible_spec_size llvm_elem skeleton_resize_arg_index crucible_spec_solvers llvm_equal split_goal crucible_struct llvm_execute_func str_concat crucible_symbolic_alloc llvm_extract summarize_verification crucible_term llvm_field tail cryptol_add_path llvm_float term_size cryptol_extract llvm_fresh_cryptol_var term_tree_size cryptol_load llvm_fresh_expanded_val test_mr_solver cryptol_prims llvm_fresh_pointer time cryptol_ss llvm_fresh_var trivial cvc4 llvm_ghost_value true default_x86_preserved_reg llvm_global type default_x86_stack_base_align llvm_global_initializer undefined define llvm_int unfold_term disable_crucible_assert_then_assume llvm_load_module unfolding disable_crucible_profiling llvm_null unint_cvc4 disable_smt_array_memory_model llvm_packed_struct_type unint_yices disable_what4_hash_consing llvm_packed_struct_value unint_z3 disable_x86_what4_hash_consing llvm_pointer w4 dsec_print llvm_points_to w4_abc_smtlib2 dump_file_AST llvm_points_to_array_prefix w4_abc_verilog empty_ss llvm_points_to_at_type w4_offline_smtlib2 enable_crucible_assert_then_assume llvm_points_to_untyped w4_unint_cvc4 enable_crucible_profiling llvm_postcond w4_unint_yices enable_deprecated llvm_precond w4_unint_z3 enable_experimental llvm_return with_time enable_lax_arithmetic llvm_sizeof write_aig enable_smt_array_memory_model llvm_spec_size write_aig_external enable_what4_hash_consing llvm_spec_solvers write_cnf enable_x86_what4_hash_consing llvm_struct write_cnf_external env llvm_struct_type write_coq_cryptol_module eval_bool llvm_struct_value write_coq_cryptol_primitives_for_sawcore eval_int llvm_symbolic_alloc write_coq_sawcore_prelude eval_list llvm_term write_coq_term eval_size llvm_type write_core exec llvm_unsafe_assume_spec write_saig exit llvm_verify write_saig' external_aig_solver llvm_verify_x86 write_smtlib2 external_cnf_solver mathsat write_smtlib2_w4 fails module_skeleton write_verilog false nth yices for null z3 fresh_symbolic offline_aig function_skeleton offline_aig_external