(*
Copyright (C) 2016- National Institute of Advanced Industrial Science and Technology (AIST)

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 2.1 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public
License along with this library; if not, write to the Free Software
Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301  USA
*)

DECLARE PLUGIN "coq-codegen.plugin"

{

let () = Mltop.add_init_function "coq-codegen.plugin"
  (fun () ->
    Feedback.msg_info Pp.(str"coq-codegen 0.1"))

open Cgenutil
open State
open Specialize
open Linear
open Genc
open Snippet
open Indimp
open Induc
open Filegen

open Stdarg (* for wit_string *)

(* for lconstr(...). lconstr accepts "Command 1 + 1" addition to "Command (1 + 1)"
  which is used for "CodeGen Linear", etc. *)
open Ltac_plugin
open Extraargs

open Pcoq.Prim (* for reference(id) in VERNAC ARGUMENT EXTEND *)
open Pcoq.Constr (* for constr(term) in VERNAC ARGUMENT EXTEND *)
}

(*
  CodeGen IndType COQ_TYPE =>
    ["C_TYPE_LEFT" ["C_TYPE_RIGHT"]]
    [swfunc "C_SWFUNC"]
    [ with ( | CONSTRUCTOR =>
      [case "C_CASELABEL"]
      [accessor "C_ACCESSOR"*]
      [deallocator "C_DEALLOCATOR"] )* ].

  CodeGen Primitive CONSTRUCTOR ARG_OR_HOLE* => "C_CONSTRUCTOR".
  CodeGen Constant CONSTRUCTOR ARG* => "C_CONSTANT".

  An empty C_CASELABEL, "", means "default:" in C switch statement.
  A non-empty C_CASELABEL, "foo", means "case foo:" in C switch statement.
  (If no default label, the first constructor is choosen to use default label.)

  Print CodeGen Inductive.              show all inductive types for codegen.
  Print CodeGen Inductive COQ_TYPE*     show the specified inductive types for codegen.

  Example:

  CodeGen IndType bool => "bool" swfunc "" with true => case "" | false => case "0".
  CodeGen Constant true => "true".
  CodeGen Constant false => "false".
  Print CodeGen Inductive bool.

  CodeGen IndType nat => "uint64_t" swfunc "" with
  | O => case "0"
  | S => case "" accessor "pred".
  CodeGen Constant O => "0".
  CodeGen Primitive S => "succ".
  Print CodeGen Inductive nat.

  CodeGen IndType option bool => "int" swfunc "" with
  | None => case "-1"
  | Some => case "" accessor "".
  CodeGen Constant @None bool => "(-1)".
  CodeGen Primitive @Some bool => "(int)".
  Print CodeGen Inductive (option bool).

  Print CodeGen Inductive.
*)

(*
  CodeGen StaticArgs FUNCTION SorD*.
  CodeGen AutoArgs FUNCTION*.
  CodeGen Func FUNCTION ARG_OR_HOLE* => "C_FUNCNAME" PRESIMP_NAME SIMPLIFIED_NAME ( ( where | and ) OPTION_KEY OPTION_VALUE )* .
  CodeGen Primitive FUNCTION ARG_OR_HOLE* => "C_FUNCNAME" PRESIMP_NAME.
  CodeGen Constant FUNCTION ARG* => "C_CONSTANT" PRESIMP_NAME.
  CodeGen NoFunc FUNCTION ARG_OR_HOLE*.

  CodeGen Snippet "SECTION" "CODE".                (* append the string into the source file *)
  CodeGen RawSnippet "SECTION" "CODE".             (* same as CodeGen Snippet but it does not strip indent *)
  CodeGen HeaderSnippet "SECTION" "CODE".          (* append the string into the header file *)
  CodeGen HeaderRawSnippet "SECTION" "CODE".       (* same as CodeGen Header Snippet but it does not strip indent *)

  CodeGen IndImp COQ_TYPE ( ( where | and ) OPTION_KEY OPTION_VALUE )* .

  CodeGen GenerateFile "FILENAME".
  CodeGen GenerateTest.
  CodeGen Gen FUNCTION_OR_C_FUNCNAME+.

  CodeGen GlobalInline QUALID...
  CodeGen LocalInline QUALID : QUALID...

  CodeGen SimplifyFunction C_FUNCNAME*.
  CodeGen SimplifyDependencies C_FUNCNAME*.

  CodeGen Linear COQ_TYPE.
  CodeGen LinearCheck FUNCTION*.

  Print CodeGen Specialization.
  Print CodeGen Specialization FUNCTION+.

  "CodeGen Func" and "CodeGen Primitive"
  declares C function name for a Gallina function.
  "CodeGen GenerateFile" generates functions declared by "CodeGen Func".
  The actual C definition of functions declared by "CodeGen Primitive"
  should be provided by a user.

  Example:

  CodeGen StaticArgs id s d.
  CodeGen Func id nat.
  CodeGen Func id nat => id_nat.
  CodeGen Func id nat => id_nat id_nat_specialized.
  CodeGen Func id nat => "id_nat".
  CodeGen Func id nat => "id_nat" id_nat.
  CodeGen Func id nat => "id_nat" id_nat id_nat_specialized.

  CodeGen SimplifyFunction id nat

  Print CodeGen Specialization id.

*)

(*
  CodeGen IndImp COQ_TYPE.
*)

VERNAC ARGUMENT EXTEND onoff
| [ "on" ] -> { true }
| [ "off" ] -> { false }
END

VERNAC ARGUMENT EXTEND where_or_and
| [ "where" ] -> { () }
| [ "and" ] -> { () }
END

VERNAC ARGUMENT EXTEND ind_cstr_mod_elt
| [ "primitive" string(cfunc) ] -> { { cm_interface = Some (CiPrimitive cfunc); cm_caselabel = None; cm_accessors = [||]; cm_deallocator = None } }
| [ "constant" string(cvalue) ] -> { { cm_interface = Some (CiConstant cvalue); cm_caselabel = None; cm_accessors = [||]; cm_deallocator = None } }
| [ "nofunc" ] -> { { cm_interface = Some CiNoFunc; cm_caselabel = None; cm_accessors = [||]; cm_deallocator = None } }
| [ "case" string(caselabel) ] -> { { cm_interface = None; cm_caselabel = Some caselabel; cm_accessors = [||]; cm_deallocator = None } }
| [ "accessor" string_list(accessors) ] -> { { cm_interface = None; cm_caselabel = None; cm_accessors = Array.map (fun accessor -> Some accessor) (Array.of_list accessors); cm_deallocator = None } }
| [ "deallocator" string(deallocator) ] -> { { cm_interface = None; cm_caselabel = None; cm_accessors = [||]; cm_deallocator = Some deallocator } }
END

VERNAC ARGUMENT EXTEND ind_cstr_mod
| [ ident(cstr_id) "=>" ind_cstr_mod_elt_list(s) ] ->
  { let cstr_mod = List.fold_left merge_cstr_mod cstr_mod_empty s in
    (cstr_id, cstr_mod) }
END

VERNAC ARGUMENT EXTEND dealloc_cstr_deallocator
| [ ident(dealloc_cstr_id) "=>" string(dealloc_cstr_deallocator) ] ->
  { { dealloc_cstr_id; dealloc_cstr_deallocator } }
END

VERNAC ARGUMENT EXTEND s_or_d
| [ "s" ] -> { SorD_S }
| [ "d" ] -> { SorD_D }
END

VERNAC ARGUMENT EXTEND id_or_underscore
| [ ident(id) ] -> { Some id }
| [ "_" ] -> { None }
END

VERNAC ARGUMENT EXTEND string_or_qualid
| [ string(s) ] -> { StrOrQid_Str s }
| [ reference(qid) ] -> { StrOrQid_Qid qid }
END

VERNAC ARGUMENT EXTEND sp_instance_names3
| [ "=>" string_opt(cfunc) id_or_underscore(presimp_id) id_or_underscore(simplified_id) ] -> { { spi_cfunc_name = cfunc; spi_presimp_id = presimp_id; spi_simplified_id = simplified_id } }
| [ "=>" string_opt(cfunc) id_or_underscore(presimp_id) ] -> { { spi_cfunc_name = cfunc; spi_presimp_id = presimp_id; spi_simplified_id = None } }
| [ "=>" string_opt(cfunc) ] -> { { spi_cfunc_name = cfunc; spi_presimp_id = None; spi_simplified_id = None } }
| [ ] -> { { spi_cfunc_name = None; spi_presimp_id = None; spi_simplified_id = None } }
END

VERNAC ARGUMENT EXTEND sp_instance_names2
| [ "=>" string_opt(cfunc) id_or_underscore(presimp_id) ] -> { { spi_cfunc_name = cfunc; spi_presimp_id = presimp_id; spi_simplified_id = None } }
| [ "=>" string_opt(cfunc) ] -> { { spi_cfunc_name = cfunc; spi_presimp_id = None; spi_simplified_id = None } }
| [ ] -> { { spi_cfunc_name = None; spi_presimp_id = None; spi_simplified_id = None } }
END

VERNAC ARGUMENT EXTEND ind_constructor
| [ "|" ident(coq_cstr) "=>" string(c_cstr) ] -> { { ic_coq_cstr = coq_cstr; ic_c_cstr = c_cstr } }
END

VERNAC ARGUMENT EXTEND genflag
| [ "DisableDependencyResolver" ] -> { DisableDependencyResolver }
| [ "DisableMutualRecursionDetection" ] -> { DisableMutualRecursionDetection }
END

VERNAC COMMAND EXTEND CodeGenQuery CLASSIFIED AS QUERY
    | [ "Print" "CodeGen" "Inductive" constr_list(coq_type_list)] ->
      { command_print_inductive coq_type_list }
    | [ "Print" "CodeGen" "Specialization" ref_list(funcs)] ->
      { command_print_specialization funcs }
    | [ "Print" "CodeGen" "GenerationList"] ->
      { command_print_generation_map () }
END

VERNAC ARGUMENT EXTEND func_mod
| [ "static" onoff(onoff) ] -> { { (* func_mods_empty with *) func_mods_static = Some onoff } }
END

VERNAC ARGUMENT EXTEND func_mods
| [ where_or_and func_mod(func_mod) func_mods(func_mods) ] -> { merge_func_mods func_mod func_mods }
| [] -> { func_mods_empty }
END

VERNAC ARGUMENT EXTEND indtype_cstrs
| [ "with" ne_ind_cstr_mod_list_sep(cstr_id_mod_list, "|") ] -> { cstr_id_mod_list }
| [ "with" "|" ne_ind_cstr_mod_list_sep(cstr_id_mod_list, "|") ] -> { cstr_id_mod_list }
| [ "with" ] -> { [] }
| [ ] -> { [] }
END

VERNAC ARGUMENT EXTEND indimp_cstrs
| [ "with" ne_dealloc_cstr_deallocator_list_sep(dealloc_cstr_deallocator_list, "|") ] -> { dealloc_cstr_deallocator_list }
| [ "with" "|" ne_dealloc_cstr_deallocator_list_sep(dealloc_cstr_deallocator_list, "|") ] -> { dealloc_cstr_deallocator_list }
| [ "with" ] -> { [] }
| [] -> { [] }
END

VERNAC ARGUMENT EXTEND filename_and_sectionopt
| [ string(filename) ":" string(section) ] -> { (filename, Some section) }
| [ "current_source" ":" string(section) ] -> { (!current_source_filename, Some section) }
| [ "current_header" ":" string(section) ] -> { (!current_header_filename, Some section) }
| [ string(filename) ] -> { (filename, None) }
| [ "current_source" ] -> { (!current_source_filename, None) }
| [ "current_header" ] -> { (!current_header_filename, None) }
END

VERNAC ARGUMENT EXTEND indimp_mod
| [ "heap" onoff(onoff) ] -> { { indimp_mods_empty with indimp_mods_heap = Some onoff } }
| [ "output_type_decls" filename_and_sectionopt(fn_and_secopt) ] -> { { indimp_mods_empty with indimp_mods_output_type_decls = Some (fst fn_and_secopt, Stdlib.Option.value ~default:"type_decls" (snd fn_and_secopt)) } }
| [ "output_type_impls" filename_and_sectionopt(fn_and_secopt) ] -> { { indimp_mods_empty with indimp_mods_output_type_impls = Some (fst fn_and_secopt, Stdlib.Option.value ~default:"type_impls" (snd fn_and_secopt)) } }
| [ "output_func_decls" filename_and_sectionopt(fn_and_secopt) ] -> { { indimp_mods_empty with indimp_mods_output_func_decls = Some (fst fn_and_secopt, Stdlib.Option.value ~default:"func_decls" (snd fn_and_secopt)) } }
| [ "output_func_impls" filename_and_sectionopt(fn_and_secopt) ] -> { { indimp_mods_empty with indimp_mods_output_func_impls = Some (fst fn_and_secopt, Stdlib.Option.value ~default:"func_impls" (snd fn_and_secopt)) } }
| [ "prefix" string(prefix) ] -> { { indimp_mods_empty with indimp_mods_prefix = Some prefix } }
| [ "static" onoff(onoff) ] -> { { indimp_mods_empty with indimp_mods_static = Some onoff } }
END

VERNAC ARGUMENT EXTEND where_indimp_mod
| [ where_or_and indimp_mod(indimp_mod) ] -> { indimp_mod }
END

VERNAC ARGUMENT EXTEND indimp_mods
| [ where_indimp_mod(indimp_mod) indimp_mods(indimp_mods) ] -> { merge_indimp_mods indimp_mod indimp_mods }
| [] -> { indimp_mods_empty }
END

VERNAC ARGUMENT EXTEND indtype_c_type
| [ string(c_type_left) string(c_type_right) ] -> { { c_type_left; c_type_right } }
| [ string(c_type) ] -> { { c_type_left=c_type; c_type_right="" } }
END

VERNAC ARGUMENT EXTEND indtype_swfunc
| [ "swfunc" string(swfunc) ] -> { swfunc }
END

VERNAC ARGUMENT EXTEND indtype_ind_args
| [ "=>" indtype_c_type_opt(c_type_opt) indtype_swfunc_opt(swfunc_opt) ] -> { (c_type_opt, swfunc_opt) }
| [] -> { (None, None) }
END

VERNAC COMMAND EXTEND CodeGen CLASSIFIED AS SIDEFF
    | [ "CodeGen" "IndType" lconstr(coq_type) indtype_ind_args(indtype_ind_args) indtype_cstrs(cstr_config_list) ] ->
      { command_ind_type coq_type indtype_ind_args cstr_config_list }

    | [ "CodeGen" "StaticArgs" ref(func) s_or_d_list(sd_list) ] ->
      { command_arguments func sd_list }
    | [ "CodeGen" "AutoArgs" ref_list(func_list) ] ->
      { command_auto_arguments func_list }
    | [ "CodeGen" "TestArgs" ref(func) s_or_d_list(sd_list) ] -> { command_test_args func sd_list }

    | [ "CodeGen" "Func" lconstr(func_args) sp_instance_names3(names) func_mods(func_mods) ] ->
      { command_function func_args names func_mods }
    | [ "CodeGen" "Primitive" lconstr(func_args) sp_instance_names2(names) ] ->
      { command_primitive func_args names }
    | [ "CodeGen" "Constant" lconstr(func_args) sp_instance_names2(names) ] ->
      { command_constant func_args names }
    | [ "CodeGen" "NoFunc" lconstr(func_args) ] ->
      { command_nofunc func_args }

    | [ "CodeGen" "Snippet" string(section) string(str) ] -> { command_snippet section str }
    | [ "CodeGen" "HeaderSnippet" string(section) string(str) ] -> { command_header_snippet section str }
    | [ "CodeGen" "RawSnippet" string(section) string(str) ] -> { command_rawsnippet section str }
    | [ "CodeGen" "HeaderRawSnippet" string(section) string(str) ] -> { command_header_rawsnippet section str }

    | [ "CodeGen" "IndImp" lconstr(coq_type) indimp_mods(indimp_mods) ] -> { command_indimp coq_type indimp_mods }

    | [ "CodeGen" "Gen" ne_string_or_qualid_list(cfunc_list) ] -> { command_gen cfunc_list }

    | [ "CodeGen" "HeaderFile" string(fn) ] -> { codegen_set_headerfile fn }
    | [ "CodeGen" "SourceFile" string(fn) ] -> { codegen_set_sourcefile fn }

    | [ "CodeGen" "GenerateFile" genflag_list(gflist) ] -> { command_generate_file gflist }
    | [ "CodeGen" "GenerateTest" genflag_list(gflist) ] -> { command_generate_test gflist }

    | [ "CodeGen" "GlobalInline" ref_list(funcs) ] ->
      { command_global_inline funcs }
    | [ "CodeGen" "LocalInline" ref(func) ":" ref_list(funcs) ] ->
      { command_local_inline func funcs }

    | [ "CodeGen" "SimplifyFunction" string_list(cfuncs) ] ->
      { command_simplify_function cfuncs }
    | [ "CodeGen" "SimplifyDependencies" string_list(cfuncs) ] ->
      { command_simplify_dependencies cfuncs }

    | [ "CodeGen" "ResolveDependencies" ] ->
      { command_resolve_dependencies () }

    | [ "CodeGen" "Linear" lconstr(ty) ] ->
      { command_linear ty }
    | [ "CodeGen" "TestLinearType" lconstr(t) ] ->
      { command_test_linear t }
    | [ "CodeGen" "TestUnrestrictedType" lconstr(t) ] ->
      { command_test_unrestricted t }

    | [ "CodeGen" "Downward" lconstr(ty) ] -> { command_downward ty }
    | [ "CodeGen" "BorrowFunc" ref(f) ] -> { command_borrow_function f }
    | [ "CodeGen" "BorrowType" lconstr(ty) ] -> { command_borrow_type ty }
    | [ "CodeGen" "TestBorrowCheck" lconstr(t) ] -> { command_test_borrowcheck t }

    (*| [ "CodeGen" "ShowLocalGensymID" ] -> { command_show_local_gensym_id () }*)
END
