(* Coq function name mangling.
   Copyright (C) 2003, 2008 Jean Goubault-Larrecq and LSV, CNRS UMR 8643 & ENS Cachan.

   This file is part of h1.

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

   h1 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 General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with h1; see the file COPYING.  If not, write to
   the Free Software Foundation, 675 Mass Ave, Cambridge, MA 02139, USA.
*)

open "coq_fun_h";
open "coq_kw_h";
open "ne_h";

local val nfa = re_make_nfa [ (re_parse "^_*[0-9]",
			       fn (f, _) => "_" ^ f),
			     (re_parse "^#false\\(([a-zA-Z0-9'_]*)\\)",
			      fn (f,a) => "__star__" ^ re_subst(f,a,1)),
			     (re_parse "^#(.*)$",
			      fn (f,a) => "__tuple__" ^ re_subst(f,a,1)),
			     (re_parse "^\\*$",
			      fn _ => "__star__")]
in
      fun coq_fun_name prefix f =
	  prefix ^ (case nfa_run (nfa, f) of
			SOME s => s
		      | _ => f)
end;

local val nfa = re_make_nfa [ (re_parse "^#false\\(([a-zA-Z0-9'_]*)\\)",
			      fn _ => 1),
			     (re_parse "^#(.*)$",
			      fn _ => 2)]
in
      fun false_fun_matches P =
	  case nfa_run (nfa, P) of
	      SOME 1 => true
	    | _ => false
      fun tuple_matches P =
	  case nfa_run (nfa, P) of
	      SOME 2 => true
	    | _ => false
      fun false_fun_or_tuple_matches P =
	  case nfa_run (nfa, P) of
	      SOME _ => true
	    | _ => false
end;

local
    val nfa = re_make_nfa [(re_parse "^#", fn _ => ())]
in
    fun percent_matches P =
	case nfa_run (nfa, P) of
	    SOME _ => true
	  | _ => false
end;

local
    val nfa = re_make_nfa [(re_parse "^#false\\(([a-zA-Z0-9'_]*)\\)",
			    fn (s,a) => re_subst(s,a,1))]
in
    fun match_false P =
	nfa_run (nfa, P)
    fun matches_false P =
	case match_false P of
	    SOME _ => true
	  | _ => false
end;

fun coq_pred_name (ver, prefix, term_type) P =
    if percent_matches P
	then let val blk = ne_of P
		 val |[exists_prolog, exists_midlog, exists_epilog, ...]| =
		     coq_keywords ver
	     in let val f as |[put, convert, ...]| =
			outstring exists_prolog
		    val delimr = ref ""
		in
		    put "X:";
		    put term_type;
		    put exists_midlog;
		    case blk of
			{} => put "True"
		      | _ =>
			iterate
			  (put (!delimr); delimr := " /\\ ";
			   put "("; put prefix; put Q; put " X)")
			| Q in set blk
			end;
		    put exists_epilog;
		    convert ()
		end
	     end handle NeOfEvt =>
	     (case match_false P of
		  SOME s => prefix ^ "__query__" ^ s
		| _ => prefix ^ substr (P, 1, size P))
    else prefix ^ P;
