coq_of_prf.ml

(******************************************************************************
Rainbow, a termination proof certification tool
See the COPYRIGHTS and LICENSE files.

- Frederic Blanqui, 2006-05-31
- Adam Koprowski, 2007-04-20, adding matrix interpretations

from the internal representation of termination proofs to color
******************************************************************************)

open Proof;;
open Printf;;
open Util;;
open Require;;
open Coq_of_pb;;
open Problem;;
open Error;;

(*REMOVE: code used for debugging *)

(*let bprint_amap b s =
  bprintf b "(* arity map %d : " s;
  SymbMap.iter (bprintf b "%a: %d, " (symbol_sig s)) (get_amap s);
  bprintf b "*)\n";;

let print_amap = print bprint_amap stdout;;

let comment b s = bprintf b "(* %s *)\n" s;;

let coq_warning b s = comment b (sprintf "WARNING: %s" s);;*)

let hack f x s =
  if get_hack() then
    let x' = f x in
      if x' <> x then warning s;
      x', sprintf "(* WARNING: %s *)\n" s
  else x, "";;

(*****************************************************************************)
(* map completion *)
(*****************************************************************************)

let case_assoc f =
  let rec aux acc = function
    | [] -> None
    | (g,p) :: l when f=g -> Some (p, acc @ l)
    | x :: l -> aux (x::acc) l
  in aux [];;

let add_mapping default f n (old_map, new_map) =
  match case_assoc f old_map with
    | Some (p, old_map') -> old_map', (f,p) :: new_map
    | None -> old_map, (f, default n) :: new_map;;

let complete s default l =
  match SymbMap.fold (add_mapping default) (get_amap s) (l, []) with
    | [], new_map -> new_map
    | _, _ -> failwith "error in map completion";;

(*****************************************************************************)
(* trivial termination proof (empty relation) *)
(*****************************************************************************)

let trivial b = bprintf b "termination_trivial.\n";;

(*****************************************************************************)
(* to create a new reduction ordering id *)
(*****************************************************************************)

let new_ro_id, cur_ro_id =
  let n = ref 0 in
    (fun () -> n:= succ !n; !n),
    (fun () -> !n);;

let ro_module_prefix fn b wp cc =
  require ["ARedPair"];
  let n = new_ro_id() in
    bprintf b "(* reduction ordering %d *)\n\n" n;
    fn b;
    bprintf b "Module WP%d := %s.\n\n\
      Module WPR%d.\n  \
        Module P := WeakRedPairProps WP%d.\n  \
        Ltac prove_cc := %a.\n  \
        Ltac prove_termin := P.prove_termination prove_cc.\n\
      End WPR%d.\n\n" n wp n n cc n n;;

let ro_module = ro_module_prefix (fun _ -> ());;

let ro_mon_alg s b ma =
  ro_module b (sprintf "WP_MonAlg %s.MonotoneAlgebra" ma)
    (fun b _k -> bprintf b "%s.prove_cc_succ S%d.Fs_ok" ma s);;

let ro_proof b = bprintf b "WPR%d.prove_termin.\n" (cur_ro_id());;

(*****************************************************************************)
(* polynomial interpretations *)
(*****************************************************************************)

(* polynomials *)

let rec monom b = function
  | [] -> bprintf b "Vnil"
  | [i] -> bprintf b "Vcons %i Vnil" i
  | i :: is -> bprintf b "Vcons %i (%a)" i monom is;;

let coef b c = if c < 0 then bprintf b "(%i)%%Z" c else bprintf b "%i%%Z" c;;

let rec polynom b = function
  | [] -> bprintf b "nil"
  | (c, m) :: p ->
      bprintf b "(%a, %a)\n        :: %a" coef c monom m polynom p;;

(* default interpretation *)

(*REMOVE: defined in CoLoR
let default_polynom n =
  let rec aux acc k =
    if k <= 0 then acc else aux (poly_sum (poly_xi n k) acc) (k-1)
  in aux (poly_const n 0) n;;*)

(* interpretation definition with labelled symbols *)

let pi_lab_map =
  let add k x m =
    try let r = SymbMap.find k m in r := x :: !r; m
    with Not_found -> SymbMap.add k (ref [x]) m
  in List.fold_left
       (fun m -> function
	  | Label (f, l), p -> add f (l,p) m
	  | (Ident _ | Hd _ | Int _), _ -> error_fmt
	    "polynomial interpretation mixing labelled and unlabelled symbols")
       SymbMap.empty;;

let list_of_map_ref m = SymbMap.fold (fun f x l -> (f, !x) :: l) m [];;

let pi_assoc pi =
  (*WARNING: sorting is necessary to be in the same order as the one
    generated by "destruct f" *)
  List.sort (fun (f,_) (g,_) -> Pervasives.compare f g)
    (list_of_map_ref (pi_lab_map pi));;

let pi_def_label b n =
  let rec aux b k = if k > n then () else
      bprintf b ", x%d%a" k aux (k+1) in
    if n < 1 then () else bprintf b "x1%a" aux 2;;

let pi_def_cases s b (l,p) =
  bprintf b "    | %a =>\n         %a\n"
    (list ", " (symbol_pat s)) l polynom p;;

let pi_inversion b n =
  let rec aux b k =
    if k >= n then ()
    else let l = k+1 in
      bprintf b "inversion v%d as [|x%d n%d v%d h%d]%a. " k l l l l aux l
  in aux b 0;;

let pi_def_lab_case s b (f,lps) =
  let n = arity s f in
    bprintf b "%a\nexact (match %a with%aend).\n"
      pi_inversion n pi_def_label n (list "" (pi_def_cases s)) lps;;

let pi_def_lab s b pi = bprintf b
  "Definition trsInt : forall f, poly (@ASignature.arity sig f).\n\n\
  Proof.\nintros [f v0]. revert v0. destruct f; intro v0.\n%aDefined."
  (list "" (pi_def_lab_case (parent_sig s))) (pi_assoc pi);;

(* polynomial interpretation *)

let new_pi_id = counter();;

let pi_def s b pi =
  match pi with
    | (Label _, _) :: _ -> pi_def_lab s b pi
    | [] | ((Ident _|Hd _|Int _),_) :: _ ->
	fun_def_symb "trsInt" "" "as f return poly (@ASignature.arity sig f)"
	  polynom s (sprintf "default_pi S%d.Sig f" s) b pi;;

let pi_module s b pi n =
  require ["Polynom";"APolyInt";"APolyInt_MA"];
  bprintf b "(* polynomial interpretation %d *)\n\n\
  Module PIS%d.\n  \
    Definition sig := S%d.Sig.\n  \
    %a\n  \
    Lemma trsInt_wm : PolyWeakMonotone trsInt.\n  \
    Proof. PolyWeakMonotone S%d.Fs_ok. Qed.\n\
  End PIS%d.\n\n\
  Module PI%d := PolyInt PIS%d.\n\n" n n s (pi_def s) pi s n n n;;

let poly_int s b pi =
  let n = new_pi_id() in
    pi_module s b (*REMOVE:complete s default_polynom*) pi n;
    ro_mon_alg s b (sprintf "PI%d" n);;

(*****************************************************************************)
(* matrix/arctic interpretations *)
(*****************************************************************************)

(* vectors and matrices *)

let arctic b = function
  | Fin p -> bprintf b "Pos %d" p
  | MinusInf -> bprintf b "MinusInf";;

let arcticBZ b = function
  | Fin p when p > 0 -> bprintf b "Fin %d" p
  | Fin p -> bprintf b "Fin (%d)" p
  | MinusInf -> bprintf b "MinusInfBZ";;

let tropical b = function
  | TroFin p -> bprintf b "TPos %d" p
  | PlusInf -> bprintf b "PlusInf";;

let vec_of_list elt b = bprintf b "(vec_of_list (%a))" (coq_list elt);;

let matrix elt = vector (vec_of_list elt);;

(* default interpretations *)

(*FIXME: define in CoLoR*)
let vector_xi z o d i = clist z (i-1) @ o :: clist z (d-i);;

let default_vector z o d = vector_xi z o d 1;;

let default_matrix z o d =
  let rec aux i = if i > d then [] else vector_xi z o d i :: aux (i+1)
  in aux 1;;

let default_mi_fun z o d n =
  { mi_const = default_vector z o d;
    mi_args = clist (default_matrix z o d) n };;

(* generic matrix interpretation *)

let new_mi_id = counter();;

let mi_case elt b fi =
  bprintf b "mkMatrixInt (vec_of_list (%a))\n        (vec_of_list (%a))"
    (coq_list elt) fi.mi_const (coq_list (par (matrix elt))) fi.mi_args;;

let mi_fun_def elt s mo = fun_def_symb "trsInt" ""
  (sprintf "as f return %s.matrixInt dim (@ASignature.arity sig f)" mo)
  (mi_case elt) s "default_mi f";; (*FIXME: default_mi undefined in CoLoR*)

let mi_module z o elt postfix m s b mi n =
  let mo = sprintf "A%sInt" m in
  require [mo; "NatUtil"];
  bprintf b
    "(* matrix interpretation %d *)\n\n\
    Module MIS%d.\n  \
      Definition sig := S%d.Sig.\n  \
      Definition dim := %d.\n  \
      Lemma dim_pos : dim > 0. Proof. check_gt. Qed.\n  \
      Notation mkMatrixInt := %s.mkMatrixInt.\n  \
      %a%s\n\
    End MIS%d.\n\n\
    Module MI%d := %s.%sInt MIS%d.\n\n"
    n n s mi.mi_dim mo (mi_fun_def elt s mo)
(*FIXME: define default interpretation in CoLoR*)
    (complete s (default_mi_fun z o mi.mi_dim) mi.mi_int)
    postfix n n mo m n;;

let matrix_based_int z o elt postfix m s b mi = 
  let n = new_mi_id() in
    mi_module z o elt postfix m s b mi n;
    ro_mon_alg s b (sprintf "MI%d" n);;

(* instanciation to int, arctic and arctic_bz *)
let matrix_int s b = matrix_based_int 0 1 int "" "Matrix" s b;;

let trsIntOk s m = Printf.sprintf
  "\n\n  Lemma trsIntOk : forall f : sig, %s dim_pos (trsInt f).\n  \
  Proof. %s S%d.Fs_ok. Qed.\n" m m s;;

let arctic_int s b mi =
  require ["SemiRing"]; import ["ArcticSemiRing"];
  matrix_based_int MinusInf (Fin 0) arctic
    (trsIntOk s "somewhere_finite") "Arctic" s b mi;;

let tropical_int s b mi =
  require ["SemiRing"]; import ["TropicalSemiRing"];
  matrix_based_int PlusInf (TroFin 0) tropical
    (trsIntOk s "somewhere_tfinite") "Tropical" s b mi;;

let arctic_bz_int s b mi =
  require ["SemiRing"]; import ["ArcticBZSemiRing"];
  matrix_based_int MinusInf (Fin 0) arcticBZ
    (trsIntOk s "absolute_finite") "ArcticBZ" s b mi;;

(*****************************************************************************)
(* dependency pair transformation *)
(*****************************************************************************)

let dp_trans b = require ["AGraph"]; bprintf b "dp_trans.\n";;

(*****************************************************************************)
(* non-permutative non-collapsing arguments filtering *)
(*****************************************************************************)

let new_ab_id = counter();;

let ab_arity =
  let rec aux k = function
    | [] -> k
    | true :: l -> aux (k+1) l
    | false :: l -> aux k l
  in aux 0;;

let ab_amap = List.fold_left
  (fun m (f,v) -> SymbMap.add f (ab_arity v) m) SymbMap.empty;;

let ab_module s b ab n =
  require ["AFilterBool"; "VecBool"];
  bprintf b "(* argument boolean filtering %d *)\n\n\
    Module AB%d.\n  \
      Definition Sig := S%d.Sig.\n  \
      %a\n\
    End AB%d.\n\n" n n s
    (fun_def_symb "pi" "" "as f return bools (@ASignature.arity Sig f)"
       (vector bool) s "Vconst true (@ASignature.arity Sig f)")
    ab n;;

let arg_bool s b ab =
  let n = new_ab_id() in
  (*REMOVE:let ab = complete s (clist true) ab in*)
  let amap = ab_amap (complete s (clist true) ab) in
  let s' = new_sig_id (parent_sig s) amap in
    ab_module s b ab n;
    sig_include b A s' (sprintf "AFilterBool.Make S%d AB%d" s n) amap;
    n, s';;

let ab_proof b n = bprintf b "AFilterBool.filter AB%d.pi.\n" n;;

let arg_bool_proof s bi bp ab =
  let n, s' = arg_bool s bi ab in
    ab_proof bp n;
    s';;

let wpab_module s n ro_id b = bprintf b
  "Module WPAB%d.\n\
     Definition Sig := S%d.Sig.\n  \
     Definition pi := AB%d.pi.\n  \
     Module WP := WP%d.\n\
   End WPAB%d.\n\n" n s n ro_id n;;

(*****************************************************************************)
(* permutative non-collapsing arguments filtering *)
(*****************************************************************************)

let new_am_id = counter();;

let am_amap = List.fold_left
  (fun m (f,v) -> SymbMap.add f (List.length v) m) SymbMap.empty;;

let am_module s b am n =
  require ["AFilterPerm"];
  bprintf b "(* argument filtering %d *)\n\n\
    Module AM%d.\n  \
      Definition Sig := S%d.Sig.\n  \
      %a\n  \
      Lemma raw_pi_ok : AFilterPerm.bvalid raw_pi S%d.Fs = true.\n  \
      Proof. check_eq. Qed.\n  \
      Definition pi := AFilterPerm.build_pi S%d.Fs_ok raw_pi_ok.\n  \
      Lemma pi_ok : non_dup pi.\n  \
      Proof. non_dup. Qed.\n\
    End AM%d.\n\n" n n s
    (fun_def_symb "raw_pi" "list nat" "" (coq_list int) s
       "nats_incr_lt (@ASignature.arity Sig f)") am
    s s n;;

let arg_perm s b am =
  let n = new_am_id() in
  (*REMOVE:let am = complete s nats_incr_lt am in*)
  let amap = am_amap (complete s nats_incr_lt am) in
  let s' = new_sig_id (parent_sig s) amap in
    am_module s b am n;
    sig_include b A s' (sprintf "AFilterPerm.Make S%d AM%d" s n) amap;
    n, s';;

let am_proof b n = bprintf b "AFilterPerm.filter AM%d.pi.\n" n;;

let arg_perm_proof s bi bp am =
  let n, s' = arg_perm s bi am in
    am_proof bp n;
    s';;

let wpam_module s n ro_id b = bprintf b
  "Module WPAM%d.\n  \
     Definition Sig := S%d.Sig.\n  \
     Definition pi := AM%d.pi.\n  \
     Definition pi_ok := AM%d.pi_ok.\n  \
     Module WP := WP%d.\n\
   End WPAM%d.\n\n" n s n n ro_id n;;

(*****************************************************************************)
(* collapsing arguments filtering *)
(*****************************************************************************)

let new_ap_id = counter();;

let ap_module s b ap n =
  require ["AProj"];
  bprintf b "(* argument projection %d *)\n\n\
    Module AP%d.\n  \
      %a\n  \
      Lemma raw_pi_ok : AProj.valid raw_pi.\n  \
      Proof. AProj.valid S%d.Fs_ok. Qed.\n  \
      Definition pi := AProj.build_pi raw_pi_ok.\n\
    End AP%d.\n\n" n n
    (fun_def_symb "raw_pi" "option nat" "" (option int) s "@None nat") ap
    s n;;

let arg_proj s b ap =
  let n = new_ap_id() in
  (*REMOVE:let ap = complete s (fun _ -> None) ap in*)
    ap_module s b ap n;
    n;;

let ap_proof b n = bprintf b "proj AP%d.pi.\n" n;;

let arg_proj_proof s bi bp ap =
  let n = arg_proj s bi ap in
    ap_proof bp n;
    s;;

let wpap_module s n ro_id b = bprintf b
  "Module WPAP%d.\n  \
     Definition Sig := S%d.Sig.\n  \
     Definition pi := AP%d.pi.\n  \
     Module WP := WP%d.\n\
   End WPAP%d.\n\n" n s n ro_id n;;

(*****************************************************************************)
(* general arguments filtering *)
(*****************************************************************************)

(* tell if a symbol is projected to one of its arguments *)
let is_proj = function
  | _, Some (Proj _) -> true
  | _, Some (Bool _|Perm _)
  | _, None -> false;;

(* tell if a symbol has its arguments filtered *)
let is_filter = function
  | _, Some (Bool _|Perm _) -> true
  | _, Some (Proj _)
  | _, None -> false;;

(* collapsing part of an AF *)
let proj_of_af = function
  | f, Some (Proj k) -> f, Some k
  | f, Some (Bool _|Perm _)
  | f, None -> f, None;;

(*UNUSED:
(* convert a non-permutative Perm AF into a Bool AF *)
let bool_of_perm n l =
  if l <> List.sort Pervasives.compare l then invalid_arg "bool_of_perm"
  else
    let rec aux bs k = function
      | [] -> bs @ clist false (n-k)
      | i :: l -> aux (bs @ clist false (i-k) @ [true]) (i+1) l
    in aux [] 0 l;;

(* convert the non-collapsing part of a non-permutative AF into a Bool AF *)
let bool_of_af s = function
  | f, Some (Bool l) -> f, l
  | f, Some (Perm l) -> f, bool_of_perm (arity s f) l
  | f, Some (Proj _)
  | f, None -> f, clist true (arity s f);;*)

(* convert a Bool AF into a non-permutative Perm AF *)
let perm_of_bool =
  let rec aux k = function
    | [] -> []
    | true :: l -> k :: aux (k+1) l
    | false :: l -> aux (k+1) l
  in aux 0;;

(* convert the non-collapsing part of an AF into a Perm AF *)
let perm_of_af s = function
  | f, Some (Perm l) -> f, l
  | f, Some (Bool l) -> f, perm_of_bool l
  | f, Some (Proj _)
  | f, None -> f, nats_incr_lt (arity s f);;

(* general argument filtering proof *)
let arg_filter_proof s bi bp af =
  match List.exists is_proj af, List.exists is_filter af with
    | true, true ->
	arg_perm_proof (arg_proj_proof s bi bp (List.map proj_of_af af))
	  bi bp (List.map (perm_of_af s) af)
    | false, true ->
	arg_perm_proof s bi bp (List.map (perm_of_af s) af)
    | true, false ->
	arg_proj_proof s bi bp (List.map proj_of_af af)
    | false, false -> s;;

(* tell if an AF preserves contect-closedness *)
let preserves_cc s = List.for_all
  (fun (f, l) -> List.sort Pervasives.compare l = nats_incr_lt (arity s f));;

(*****************************************************************************)
(* rpo *)
(*****************************************************************************)

let new_rpo_id = counter();;

let status b = function
  | Lex -> bprintf b "Lex"
  | Mul -> bprintf b "Mul";;

(* compute a map precedence -> status from user declarations

in case of incompatibility:
- if the symbol is of arity <= 1, then change its status and print a warning
- otherwise:
   . if the -hack option is set, then change its status to enforce compatibility
   . otherwise, raise an error *)

let prec_status_map s =
  let rec aux (m, w) = function
    | [] -> m, w
    | (f, (st, p)) :: l ->
	aux (try
	       if st = IntMap.find p m then m, w
	       else let k = arity s f in
		 if k <= 1 || get_hack() then
		   let w' = sprintf "WARNING: status of %s of arity %d was %s"
		     (sprint (symbol_pat s) f) k (sprint status st) in
		     (warning w'; m,
		      if w = "" then w' else sprintf "%s\n%s" w w')
		 else error_fmt (sprintf "two symbols of precedence %d \
                                          have incompatible statuses" p)
	     with Not_found -> IntMap.add p st m, w) l
  in aux (IntMap.empty, "");;

(* compute default status and modified user declarations
to avoid incompatibilities *)

let prec_status s l =
  let m, w = prec_status_map s l in
    ((try IntMap.find 0 m with Not_found -> Lex),
    List.map (fun (f, (_, p)) -> f, (IntMap.find p m, p)) l,
    if w = "" then "" else sprintf "(* %s *)\n  " w);;

let rpo_module s b l n w st =
  require ["Coccinelle"; "rpo"; "rpo_extension"];
  bprintf b "(* RPO %d *)\n\n\
    Module RPO%d.\n  \
      Definition Sig := S%d.Sig.\n  %s\
      %a\n  \
      %a\n  \
      Definition bb := 100.\n  \
      Lemma prec_eq_status : forall f g,\n    \
        prec_eq prec_nat f g -> status f = status g.\n  \
      Proof. prec_eq_status status prec_nat S%d.Fs_ok. Qed.\n\
    End RPO%d.\n\n" n n s w
    (fun_def_symb "status" "status_type" "" (first status) s st) l
    (fun_def_symb "prec_nat" "nat" "" (second int) s "0") l s n;;

let rpo s b l =
  let n = new_rpo_id() and st, l, w = prec_status s l in
    rpo_module s b l n w (sprint status st);
    ro_module b (sprintf "WP_RPO RPO%d" n)
      (fun b k -> bprintf b "apply WP%d.cc_succ" k);;

(*****************************************************************************)
(* usable rules *)
(*****************************************************************************)

let ur_module s b =
  let n = cur_ro_id() in
    bprintf b "Module WPUR%d := Usable WP%d S%d S%d.\n\n" n n s s;;

let ur_proof b = bprintf b "WPUR%d.prove_termin.\n" (cur_ro_id());;

let usable_rules s bi bp = require ["AUsable"];
  try ur_module s bi; ur_proof bp with Not_found -> ro_proof bp;;

(*****************************************************************************)
(* reduction ordering *)
(*****************************************************************************)

let rec red_ord_def s b = function
  | PolyInt pi -> poly_int s b pi
  | MatrixInt mi -> matrix_int s b mi
  | ArcticInt ai -> arctic_int s b ai
  | TropicalInt ai -> tropical_int s b ai
  | ArcticBZInt ai -> arctic_bz_int s b ai
  | ArgBoolOrd (af, ro) -> ro_bool s b af ro
  | ArgProjOrd (af, ro) -> ro_proj s b af ro
  | ArgPermOrd (af, ro) -> ro_perm s b af ro
  | ArgFilterOrd (af, ro) -> ro_filter s b af ro
  | Rpo l -> rpo s b l

and ro_bool s b af ro =
  let n, s' = arg_bool s b af in
  let _ = red_ord_def s' b ro in
    ro_module_prefix (wpab_module s n (cur_ro_id())) b
      (sprintf "WP_Filter WPAB%d" n)
      (fun b _k -> bprintf b
	 "fail 10 \"no tactic for proving closure by context\"")

and ro_proj s b af ro =
  let n = arg_proj s b af in
  let _ = red_ord_def s b ro in
    ro_module_prefix (wpap_module s n (cur_ro_id())) b
      (sprintf "WP_Proj WPAP%d" n)
      (fun b _k -> bprintf b
	 "fail 10 \"no tactic for proving closure by context\"")

and ro_perm s b af ro =
  let n, s' = arg_perm s b af in
  let _ = red_ord_def s' b ro in
  let k = cur_ro_id() in
    ro_module_prefix (wpam_module s n k) b
      (sprintf "WP_Perm WPAM%d" n)
      (fun b _k ->
	 if preserves_cc s af then
	   bprintf b "prove_cc_succ WPR%d.prove_cc" k
	 else bprintf b
	   "fail 10 \"no tactic for proving closure by context\"")

and ro_filter s b af ro = red_ord_def s b
  (match List.exists is_proj af, List.exists is_filter af with
     | true, true ->
	 ArgPermOrd (List.map (perm_of_af s) af,
		     ArgProjOrd (List.map proj_of_af af, ro))
     | false, true -> ArgPermOrd (List.map (perm_of_af s) af, ro)
     | true, false -> ArgProjOrd (List.map proj_of_af af, ro)
     | false, false -> ro);;

let red_ord ur s bi bp ro =
  red_ord_def s bi ro; if ur then usable_rules s bi bp else ro_proof bp;;

(*****************************************************************************)
(* conversion from SRS to TRS *)
(*****************************************************************************)

let as_trs_amap s =
  SymbMap.fold (fun f _ m -> SymbMap.add f 1 m) (get_amap s) SymbMap.empty;;

let as_trs_sig_def s = sprintf "ATerm_of_String.Make S%d" s;;

let as_trs_proof b = bprintf b "as_trs.\n";;

let as_trs s bi bp =
  require ["ATerm_of_String"; "ATrs"; "VecUtil"];
  let amap = as_trs_amap s in
  let s' = new_sig_id s amap in
    sig_include bi V s' (as_trs_sig_def s) amap;
    as_trs_proof bp;
    s';;

(*****************************************************************************)
(* conversion from TRS to SRS *)
(*****************************************************************************)

let as_srs_module b s s' =
  bprintf b "Module S%d := String_of_ATerm.Make S%d.\n\n" s' s;;

let as_srs_proof b s' = bprintf b "as_srs S%d.Fs_ok.\n" s';;

let as_srs s bi bp =
  require ["String_of_ATerm"; "Srs"];
  let s' = new_sig_id s (get_amap s) in
    as_srs_module bi s s';
    as_srs_proof bp s';
    s';;

(*****************************************************************************)
(* graph decomposition *)
(*****************************************************************************)

let new_decomp_id = counter();;

let component s = par (prefix "  " (list_nil "nil" "\n   :: " (rule A s)));;

let decomp_def s b n cs =
  bprintf b "(* graph decomposition %d *)\n\n\
    Definition cs%d : list (list (@ATrs.rule S%i.Sig)) :=\n\n   %a.\n\n"
    n n s (list_nil "nil" "\n\n:: " (component s)) cs;;

let component_proof proof s bi bp = function
  | None -> bprintf bp "left. co_scc.\n"
  | Some p -> bprintf bp "right. "; proof s bi bp p;;

let decomp s bi bp og l proof =
  require ["ADecomp"];
  let cs, ps = List.split l and n = new_decomp_id() in
  decomp_def s bi n cs;
  (match og with
    | HDE | HDE_Marked ->
	require ["AHDE"];
	bprintf bp "let D := fresh \"D\" in set_rules_to D;\n\
          graph_decomp S%d.Sig (hde_bool D) cs%d; subst D. \n\
          hde_bool_correct.\n" s n
    | Unif ->
	require ["ADPUnif"];
(*FIXME: the number of unification steps should be modifiable
by a command line argument *)
	bprintf bp "let D := fresh \"D\" in let R := fresh \"R\" in \
          set_rules_to D; set_mod_rules_to R;\n\
          graph_decomp S%d.Sig (dpg_unif_N 100 R D) cs%d; subst D; subst R.\n\
          dpg_unif_N_correct.\n" s n);
  List.iter (component_proof proof s bi bp) ps;;

(*****************************************************************************)
(* mark symbols *)
(*****************************************************************************)

let mark_amap s = SymbMap.fold
  (fun f k m -> SymbMap.add (Hd f) k (SymbMap.add (Int f) k m))
  (get_amap s) SymbMap.empty;;

let mark_sig_include s = sprintf "ADuplicateSymb.Make S%d" s;;

let mark_proof b = bprintf b "mark.\n";;
 
let mark s bi bp =
  require ["ADuplicateSymb"];
  let amap = mark_amap s in
  let s' = new_sig_id s amap in
    sig_include bi A s' (mark_sig_include s) amap;
    mark_proof bp;
    s';;

(*****************************************************************************)
(* SRS reversal *)
(*****************************************************************************)

let srs_rev b = require ["SReverse"]; bprintf b "SReverse.rev_tac.\n";;

(*****************************************************************************)
(* TRS reversal *)
(*****************************************************************************)

let trs_rev_sig_def s = sprintf "rev_Sig S%d.Sig" s;;

let trs_rev_proof s b = bprintf b "AReverse.rev_tac S%d.Fs_ok.\n" s;;

let trs_rev s bi bp =
  require ["AReverse"; "AUnary"];
  let amap = get_amap s in
  let s' = new_sig_id s amap in
    sig_module_of_amap bi A s' (trs_rev_sig_def s) amap;
    trs_rev_proof s bp;
    s';;

(*****************************************************************************)
(* flat context closure *)
(*****************************************************************************)

let new_flat_cc_id = counter();;

let flat_cc_module s b n = bprintf b
  "(* flat context closure %d *)\n\n\
   Module FC%d := FlatCCProps S%d.\n\n" n n s;;

let flat_cc_proof b n = bprintf b "FC%d.flat_cc.\n" n;;

let flat_cc s bi bp =
  require ["AFlatCont"];
  let n = new_flat_cc_id() in
  flat_cc_module s bi n;
  flat_cc_proof bp n;;

(*****************************************************************************)
(* root labelling *)
(*****************************************************************************)

let new_root_lab_id = counter();;

let root_lab_module s b n = bprintf b
  "(* root labelling %d *)\n\n\
   Module RLP%d := RootLabProps S%d.\n\n" n n s;;

(*FIXME: to be improved by using a cache *)
let enum_tuple fs =
  let rec aux n =
    if n <= 0 then [[]]
    else flat_map (fun ds -> List.map (fun d -> d :: ds) fs) (aux (n-1))
  in aux;;

let root_lab_amap s =
  let amap = get_amap s in
  let fs = symbols_of_map amap in
    SymbMap.fold
      (fun f k m ->
	 List.fold_left (fun m ds -> SymbMap.add (Label (f,ds)) k m)
	   m (enum_tuple fs k)) amap SymbMap.empty;;

let root_lab_sig_def n = sprintf "RLP%d.LabSig" n;;

let root_lab_proof b n = bprintf b "RLP%d.rootlab.\n" n;;

let root_lab s bi bp =
  require ["ARootLab"; "ASemLab"];
  let n = new_root_lab_id() in
  let amap = root_lab_amap s in
  let s' = new_sig_id s amap in
  root_lab_module s bi n;
  sig_include bi A s' (root_lab_sig_def n) amap;
  root_lab_proof bp n;
  s';;

(*****************************************************************************)
(* unlabelling *)
(*****************************************************************************)

let unlab s b = bprintf b "S%d.unlab.\n" s; parent_sig s;;

(*****************************************************************************)
(* subterm criterion *)
(*****************************************************************************)

let new_sc_id = counter();;

let sc_hack = "validity of simple projection enforced";;

let sc_enforce_valid s = List.map (fun (f, k) -> f, min k (arity s f - 1));;

let sc_module s b ap n w =
  require ["ASimpleProj"];
  bprintf b "(* simple projection %d *)\n\n\
    Module SC%d.\n  %s\
      %a\n  \
      Lemma pi_ok : ASimpleProj.valid pi.\n  \
      Proof. ASimpleProj.valid S%d.Fs_ok. Qed.\n\
    End SC%d.\n\n" n n w
    (fun_def_symb "pi" "nat" "" int s "0") ap
    s n;;

let sc_proof b n = bprintf b "subterm_crit SC%d.pi_ok.\n" n;;

let subterm_crit s bi bp ap =
  require ["ASubtermCrit"];
  let n = new_sc_id() and ap, w = hack (sc_enforce_valid s) ap sc_hack in
    sc_module s bi ap n w;
    sc_proof bp n;;

(*****************************************************************************)
(* termination proofs *)
(*****************************************************************************)

let rec proof s bi bp = function
  | Trivial -> trivial bp
  | MarkSymb p -> proof (mark s bi bp) bi bp p
  | MannaNess (ur, ro, p) -> red_ord ur s bi bp ro; proof s bi bp p
  | DP p -> dp_trans bp; proof s bi bp p
  | ArgBool (af, p) -> proof (arg_bool_proof s bi bp af) bi bp p
  | ArgProj (af, p) -> proof (arg_proj_proof s bi bp af) bi bp p
  | ArgPerm (af, p) -> proof (arg_perm_proof s bi bp af) bi bp p
  | ArgFilter (af, p) -> proof (arg_filter_proof s bi bp af) bi bp p
  | AsTrs p -> proof (as_trs s bi bp) bi bp p
  | AsSrs p -> proof (as_srs s bi bp) bi bp p
  | SrsRev p -> srs_rev bp; proof s bi bp p
  | TrsRev p -> proof (trs_rev s bi bp) bi bp p
  | Decomp (og, l) -> decomp s bi bp og l proof
  | FlatCC p -> flat_cc s bi bp; proof s bi bp p
  | RootLab p -> proof (root_lab s bi bp) bi bp p
  | Unlab p -> proof (unlab s bp) bi bp p
  | SubtermCrit (af, p) -> subterm_crit s bi bp af; proof s bi bp p;;

(*****************************************************************************)
(* trs loops *)
(*****************************************************************************)

let sig_kind_of_problem = function
  | Trs {trs_algebra = Varyadic; _} -> V
  | Trs {trs_algebra = Signature _; _} -> A
  | Srs _ -> error_fmt "SRS counter-example with TRS problem";;

let term pb = term (sig_kind_of_problem pb) 1;;
let rule pb = rule (sig_kind_of_problem pb) 1;;

let position = coq_list int;;

let trs_mod_step pb b s =
  bprintf b "(%a,\n   %a)" position s.cet_mod_step_pos
    (rule pb) s.cet_mod_step_rule;;

let trs_mod_steps pb = list_nil "nil" "\n  :: " (trs_mod_step pb);;

let trs_step pb b s =
  if has_relative_rules pb then
    bprintf b "(%a,\n   (%a,\n   %a))"
      (trs_mod_steps pb) s.cet_step_mod_steps position s.cet_step_pos
      (rule pb) s.cet_step_rule
  else
    bprintf b "(%a,\n   %a)" position s.cet_step_pos
      (rule pb) s.cet_step_rule;;

let trs_steps pb = list_nil "nil" "\n  :: " (trs_step pb);;

let if_mod pb s = if has_relative_rules pb then s else "";;

let data_prefix pb = if_mod pb "mod_";;

(*UNUSED:
let loop_module pb = if has_relative_rules pb then "ModLoop" else "Loop";;*)

let loop_modules k pb = (k ^ "Loop") ::
  (if has_relative_rules pb then [k ^ "ModLoop"] else []);;

let ce_mod pb f b x =
  if has_relative_rules pb then
    bprintf b "\nDefinition ds' : list (data S1.Sig) :=\n  %a.\n" f x;;

let cet_loop pb bi bp ce =
  let k = string_of_sig_kind (sig_kind_of_problem pb) in
    require ("APosition" :: loop_modules k pb);
    bprintf bi "(* counter-example *)\n\n\
      Definition t : term S1.Sig := %a.\n\
      Definition ds : list (%sdata S1.Sig) :=\n  %a.\n%a\n\
      Definition p : position := %a.\n\n"
      (term pb) ce.cet_start
      (data_prefix pb) (trs_steps pb) ce.cet_steps
      (ce_mod pb (trs_mod_steps pb)) ce.cet_mod
      position ce.cet_pos;
    bprintf bp "%s%sLoop.loop t ds%s p.\n" k
      (if_mod pb "Mod") (if_mod pb " ds'");;

(*****************************************************************************)
(* srs loops *)
(*****************************************************************************)

let srs_mod_step b s =
  bprintf b "(%a,%a)" int s.ces_mod_step_pos srs_rule s.ces_mod_step_rule;;

let srs_mod_steps = coq_list srs_mod_step;;

let srs_step pb b s =
  if has_relative_rules pb then
    bprintf b "(%a,(%a,%a))" srs_mod_steps s.ces_step_mod_steps
      int s.ces_step_pos srs_rule s.ces_step_rule
  else
    bprintf b "(%a,%a)" int s.ces_step_pos srs_rule s.ces_step_rule;;

let srs_steps pb = coq_list (srs_step pb);;

let ces_loop pb bi bp ce =
  require (loop_modules "S" pb);
  bprintf bi "(* counter-example *)\n\n\
    Definition t : list S1.Sig := %a.\n\n\
    Definition ds : list (%sdata S1.Sig) :=\n  %a.\n%a\n\
    Definition p : nat := %i.\n\n"
    word ce.ces_start
    (data_prefix pb) (srs_steps pb) ce.ces_steps
    (ce_mod pb srs_mod_steps) ce.ces_mod
    ce.ces_pos;
  bprintf bp "S%sLoop.loop t ds%s p.\n" (if_mod pb "Mod") (if_mod pb " ds'");;

(*****************************************************************************)
(* counter-examples *)
(*****************************************************************************)

let cet_var_cond pb b =
  let k = string_of_sig_kind (sig_kind_of_problem pb) in
    require [k ^ "VarCond"]; bprintf b "var_cond S1.Sig.\n";;

let cet pb bi bp = function
  | CET_var_cond -> cet_var_cond pb bp
  | CET_loop ce -> cet_loop pb bi bp ce;;

let ces pb bi bp = function
  | CES_loop ce -> ces_loop pb bi bp ce;;

let counter_example pb bi bp = function
  | CE_trs ce -> cet pb bi bp ce
  | CE_srs ce -> ces pb bi bp ce

(*****************************************************************************)
(* certificates *)
(*****************************************************************************)

let certif pb bi bp = function
  | Proof prf ->
      require ["SN"; "LogicUtil"; (*for debug only*)"RelUtil"; "BoolUtil"];
      bprintf bp
	"(* termination proof *)\n\n\
         Lemma termination : WF rel.\n\n\
         Proof.\n\
         unfold rel.\n";
      proof 1 bi bp prf
  | Counter_example ce -> (*FIXME: non_terminating changed name EIS*)
      require ["RelUtil"];
      bprintf bp
	"(* non-termination proof *)\n\n\
         Lemma non_termination : EIS rel.\n\n\
         Proof.\n\
         unfold rel.\n";
      (*bprintf bp
	"(* non-termination proof *)\n\n\
         Lemma non_termination : non_terminating rel.\n\n\
         Proof.\n\
         unfold rel.\n";*)  
      counter_example pb bi bp ce;;

let genr_certif pb bi bp c =
  certif pb bi bp c;
  bprintf bp "Qed.\n";;