Vim syntax highlighting

vim-saw/syntax/saw.vim

@@ -1,10 +1,66 @@
-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
+" SAW syntax file
+" Language:     saw
+" Author:       Stanley Roberts
+
+if exists("b:current_syntax")
+      finish
+endif
+
+syn keyword sawInclude import include
+
+syn keyword sawConstant true false
+
+syn keyword sawType Int String Bool LLVMType Term CrucibleSetup JVMSetup JavaType SetupValue JVMValue LLVMModule CrucibleMethodSpec ProofScript SatResult TopLevel JavaClass JVMMethodSpec Theorem Simpset
+
+syn keyword sawKeyword do let and return as hiding rec in
+syn keyword sawConitional if then else
+
+syn keyword sawFunction abc list_term abstract_symbolic llvm_alias add_cryptol_defs llvm_alloc add_cryptol_eqs llvm_alloc_aligned add_prelude_defs llvm_alloc_global add_prelude_eqs llvm_alloc_readonly add_x86_preserved_reg llvm_alloc_readonly_aligned addsimp llvm_array addsimps llvm_array_value admit llvm_cfg approxmc llvm_conditional_points_to assume_unsat llvm_conditional_points_to_at_type assume_valid llvm_conditional_points_to_untyped auto_match llvm_declare_ghost_state basic_ss llvm_double beta_reduce_goal llvm_elem beta_reduce_term llvm_equal bitblast llvm_execute_func boolector llvm_extract caseProofResult llvm_field caseSatResult llvm_float check_convertible llvm_fresh_expanded_val check_goal llvm_fresh_pointer check_term llvm_fresh_var codegen llvm_ghost_value concat llvm_global core_axiom llvm_global_initializer core_thm llvm_int crucible_alloc llvm_load_module crucible_alloc_aligned llvm_null crucible_alloc_global llvm_packed_struct_type crucible_alloc_readonly llvm_packed_struct_value crucible_alloc_readonly_aligned llvm_pointer crucible_array llvm_points_to crucible_conditional_points_to llvm_points_to_at_type crucible_conditional_points_to_untyped llvm_points_to_untyped crucible_declare_ghost_state llvm_postcond crucible_elem llvm_precond crucible_equal llvm_return crucible_execute_func llvm_sizeof crucible_field llvm_spec_size crucible_fresh_expanded_val llvm_spec_solvers crucible_fresh_pointer llvm_struct crucible_fresh_var llvm_struct_type crucible_ghost_value llvm_struct_value crucible_global llvm_symbolic_alloc crucible_global_initializer llvm_term crucible_java_extract llvm_type crucible_llvm_extract llvm_unsafe_assume_spec crucible_llvm_unsafe_assume_spec llvm_verify crucible_llvm_verify load_aig crucible_null mathsat crucible_packed_struct nth crucible_points_to null crucible_points_to_untyped offline_aig crucible_postcond offline_aig_external crucible_precond offline_cnf crucible_return offline_cnf_external crucible_spec_size offline_extcore crucible_spec_solvers offline_smtlib2 crucible_struct offline_unint_smtlib2 crucible_symbolic_alloc offline_w4_unint_cvc4 crucible_term offline_w4_unint_yices cryptol_add_path offline_w4_unint_z3 cryptol_extract parse_core cryptol_load parser_printer_roundtrip cryptol_prims print cryptol_ss print_goal cvc4 print_goal_consts default_x86_preserved_reg print_goal_depth define print_goal_size disable_crucible_assert_then_assume print_term disable_crucible_profiling print_term_depth disable_debug_intrinsics print_type disable_lax_arithmetic prove disable_lax_pointer_ordering prove_core disable_smt_array_memory_model prove_print disable_what4_hash_consing qc_print disable_x86_what4_hash_consing quickcheck dsec_print read_aig dump_file_AST read_bytes empty_ss read_core enable_crucible_assert_then_assume replace enable_crucible_profiling enable_debug_intrinsics rewrite enable_deprecated rme enable_experimental run enable_lax_arithmetic sat enable_lax_pointer_ordering sat_print enable_smt_array_memory_model save_aig enable_what4_hash_consing save_aig_as_cnf env sbv_abc eval_bool sbv_boolector eval_int sbv_cvc4 eval_list sbv_mathsat eval_size sbv_unint_cvc4 exec sbv_unint_yices exit sbv_unint_z3 external_aig_solver sbv_yices external_cnf_solver sbv_z3 fails set_ascii false set_base for set_color fresh_symbolic set_min_sharing get_opt sharpSAT goal_eval show goal_eval_unint show_cfg head show_term hoist_ifs simplify str_concat java_array tail java_bool term_size java_byte term_tree_size java_char time java_class trivial java_double true java_float type java_int undefined java_load_class unfold_term java_long unfolding java_short unint_cvc4 jvm_alloc_array unint_yices jvm_alloc_object unint_z3 jvm_array_is w4 jvm_elem_is w4_abc_aiger jvm_execute_func w4_abc_smtlib2 jvm_extract w4_abc_verilog jvm_field_is w4_offline_smtlib2 jvm_fresh_var w4_unint_cvc4 jvm_modifies_array w4_unint_yices jvm_modifies_elem w4_unint_z3 jvm_modifies_field with_time jvm_modifies_static_field write_aig jvm_null write_aig_external jvm_postcond write_cnf jvm_precond write_cnf_external jvm_return write_core jvm_static_field_is write_saig jvm_term write_saig' jvm_unsafe_assume_spec write_smtlib2 jvm_verify write_smtlib2_w4 lambda yices lambdas z3 length
+
+syn match sawOperator "<-" "=" "=="
+
+syn match sawComment "\v//.*$"
+syn region sawComment start="/\*" end="\*/"
+
+syn match   sawEsc contained "\\\""
+syn match   sawEsc contained "\\'"
+syn match   sawEsc contained "\\\\"
+syn match   sawEsc contained "\\n"
+syn match   sawEsc contained "\\t"
+syn match   sawEsc contained "\\r"
+syn match   sawEsc contained "\\\d\+"
+syn match   sawEsc contained "\\\(x\|X\)\x\+"
+syn region  sawString start="\"" skip="\\\"" end="\"" contains=sawEsc
+syn region  sawByte   start="'"  skip="\\'"  end="'"  contains=sawEsc
+
+syn match sawParentheses "("
+syn match sawParentheses ")"
+
+syn match   sawNumber "\(0\(x\|X\|b\|B\|o\|O\)\x\+\)\|-\?\(\d\|_\)\+"
+syn match ddlIdent "\(\l\|\u\)\(\a\|\d\|_\|'\)*"
+
+" inline cryptol highlight
+if filereadable("syntax/cryptol.vim")
+      syn include @cry syntax/cryptol.vim
+endif
+syn region crySnip matchgroup=Snip start="{{" end="}}" contains=@cry
+
+hi def link Snip SpecialComment
+
+hi def link sawInclude        Include
+hi def link sawKeyword        Keyword
+hi def link sawConditional    Conditional
+hi def link sawConstant       Constant
+hi def link sawFunction       Function
+hi def link sawType           Type
+hi def link sawOperator       Operator
+hi def link sawParentheses    Delimiter
+hi def link sawComment        Comment
+
+hi def link sawEsc            Special
+hi def link sawString         String
+hi def link sawByte           Character
+
+hi def link sawNumber         Number
+
+let b:current_syntax = "saw"