(*
    ||M||  This file is part of HELM, an Hypertextual, Electronic        
    ||A||  Library of Mathematics, developed at the Computer Science     
    ||T||  Department, University of Bologna, Italy.                     
    ||I||                                                                
    ||T||  HELM is free software; you can redistribute it and/or         
    ||A||  modify it under the terms of the GNU General Public License   
    \   /  version 2 or (at your option) any later version.      
     \ /   This software is distributed as is, NO WARRANTY.     
      V_______________________________________________________________ *)

(* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)

  let eqP () = 
    let r = 
      OCic2NCic.reference_of_oxuri 
       (UriManager.uri_of_string 
         "cic:/matita/logic/equality/eq.ind#xpointer(1/1)")
    in
    NCic.Const r
  ;;

  let eq_ind () = 
    let r = 
      OCic2NCic.reference_of_oxuri 
       (UriManager.uri_of_string 
         "cic:/matita/logic/equality/eq_ind.con")
    in
    NCic.Const r
  ;;

  let eq_ind_r () = 
    let r = 
      OCic2NCic.reference_of_oxuri 
       (UriManager.uri_of_string 
         "cic:/matita/logic/equality/eq_elim_r.con")
    in
    NCic.Const r
  ;;

  let eq_refl () = 
    let r = 
      OCic2NCic.reference_of_oxuri 
       (UriManager.uri_of_string 
         "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)")
    in
    NCic.Const r
  ;;

  let extract lift vl t =
    let rec pos i = function 
      | [] -> raise Not_found 
      | j :: tl when j <> i -> 1+ pos i tl
      | _ -> 1
    in
    let vl_len = List.length vl in
    let rec extract = function
      | Terms.Leaf x -> NCicSubstitution.lift (vl_len+lift) x
      | Terms.Var j -> 
           (try NCic.Rel (pos j vl) with Not_found -> NCic.Implicit `Term) 
      | Terms.Node l -> NCic.Appl (List.map extract l)
    in
      extract t
  ;;

   let mk_predicate hole_type amount ft p1 vl =
    let rec aux t p = 
      match p with
      | [] -> NCic.Rel 1
      | n::tl ->
          match t with
          | Terms.Leaf _ 
          | Terms.Var _ -> 
	      let module Pp = 
		Pp.Pp(NCicBlob.NCicBlob(
			struct
			  let metasenv = [] let subst = [] let context = []
			end))
	      in  
               prerr_endline ("term: " ^ Pp.pp_foterm ft);
               prerr_endline ("path: " ^ String.concat "," 
                 (List.map string_of_int p1));
	       prerr_endline ("leading to: " ^ Pp.pp_foterm t);
               assert false
          | Terms.Node l -> 
              let l = 
                HExtlib.list_mapi
                  (fun t i -> 
                    if i = n then aux t tl 
                    else extract amount (0::vl) t)
                  l
              in            
              NCic.Appl l
    in
      NCic.Lambda("x", hole_type, aux ft (List.rev p1))
    ;;

  let mk_proof (bag : NCic.term Terms.bag) mp steps =
    let module Subst = FoSubst in
    let position i l = 
      let rec aux = function
       | [] -> assert false
       | (j,_) :: tl when i = j -> 1
       | _ :: tl -> 1 + aux tl
      in
        aux l
    in
    let vars_of i l = fst (List.assoc i l) in
    let ty_of i l = snd (List.assoc i l) in
    let close_with_lambdas vl t = 
      List.fold_left 
       (fun t i -> 
          NCic.Lambda ("x"^string_of_int i, NCic.Implicit `Type, t))
       t vl  
    in
    let close_with_forall vl t = 
      List.fold_left 
       (fun t i -> 
          NCic.Prod ("x"^string_of_int i, NCic.Implicit `Type, t))
       t vl  
    in
    let get_literal id =
      let (_, lit, vl, proof),_ = Terms.M.find id bag in
      let lit =match lit with 
          | Terms.Predicate t -> assert false 
          | Terms.Equation (l,r,ty,_) -> 
              Terms.Node [ Terms.Leaf eqP(); ty; l; r]
      in
	lit, vl, proof
    in
    let rec aux ongoal seen = function
      | [] -> NCic.Rel 1
      | id :: tl ->
          let amount = List.length seen in
          let lit,vl,proof = get_literal id in
          if not ongoal && id = mp then
            ((*prerr_endline ("Reached m point, id=" ^ (string_of_int id));*)
             NCic.LetIn ("clause_" ^ string_of_int id, 
                extract amount [] lit, 
                (NCic.Appl [eq_refl();NCic.Implicit `Type;NCic.Implicit `Term]),
                aux true ((id,([],lit))::seen) (id::tl)))
          else
          match proof with
          | Terms.Exact _ when tl=[] ->
	      (* prerr_endline ("Exact (tl=[]) for " ^ (string_of_int id));*)
	      aux ongoal seen tl
          | Terms.Step _ when tl=[] -> assert false
          | Terms.Exact ft ->
	      (* prerr_endline ("Exact for " ^ (string_of_int id));*)
               NCic.LetIn ("clause_" ^ string_of_int id, 
                 close_with_forall vl (extract amount vl lit),
                 close_with_lambdas vl (extract amount vl ft),
                 aux ongoal 
                   ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
          | Terms.Step (_, id1, id2, dir, pos, subst) ->
              let id, id1,(lit,vl,proof) =
		if ongoal then id1,id,get_literal id1
		else id,id1,(lit,vl,proof)
	      in
	      let vl = if ongoal then [](*Subst.filter subst vl*) else vl in
              let proof_of_id id = 
                let vars = List.rev (vars_of id seen) in
                let args = List.map (Subst.apply_subst subst) vars in
                let args = List.map (extract amount vl) args in
		let rel_for_id = NCic.Rel (List.length vl + position id seen) in
		  if args = [] then rel_for_id		    
                  else NCic.Appl (rel_for_id::args)
              in
              let p_id1 = proof_of_id id1 in
              let p_id2 = proof_of_id id2 in
              let pred, hole_type, l, r = 
                let id1_ty = ty_of id1 seen in
                let id2_ty,l,r = 
                  match ty_of id2 seen with
                  | Terms.Node [ _; t; l; r ] -> 
                      extract amount vl (Subst.apply_subst subst t),
                      extract amount vl (Subst.apply_subst subst l),
                      extract amount vl (Subst.apply_subst subst r)
                  | _ -> assert false
                in
		  (*prerr_endline "mk_predicate :";
		  if ongoal then prerr_endline "ongoal=true"
		  else prerr_endline "ongoal=false";
		  prerr_endline ("id=" ^ string_of_int id);
		  prerr_endline ("id1=" ^ string_of_int id1);
		  prerr_endline ("id2=" ^ string_of_int id2);
		  prerr_endline ("Positions :" ^
				   (String.concat ", "
				      (List.map string_of_int pos)));*)
                mk_predicate 
                  id2_ty amount (Subst.apply_subst subst id1_ty) pos vl,
                id2_ty,
                l,r
              in
              let l, r, eq_ind = 
                if (ongoal=true) = (dir=Terms.Left2Right) then
                  r,l,eq_ind_r ()
                else
                  l,r,eq_ind ()
              in
               NCic.LetIn ("clause_" ^ string_of_int id, 
                 close_with_forall vl (extract amount vl lit),
			   (* NCic.Implicit `Type, *)
                 close_with_lambdas vl 
                   (NCic.Appl [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]),
                 aux ongoal 
                   ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
    in 
      aux false [] steps
  ;;