helm/software/components/ng_paramodulation/nCicProof.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
  13
  14 let reference_of_oxuri = ref (fun _ -> assert false);;
  15 let set_reference_of_oxuri f = reference_of_oxuri := f;;
  16
  17
  18   let eqP () =
  19     let r =
  20       !reference_of_oxuri
  21        (UriManager.uri_of_string
  22          "cic:/matita/logic/equality/eq.ind#xpointer(1/1)")
  23     in
  24     NCic.Const r
  25   ;;
  26
  27   let eq_ind () =
  28     let r =
  29       !reference_of_oxuri
  30        (UriManager.uri_of_string
  31          "cic:/matita/logic/equality/eq_ind.con")
  32     in
  33     NCic.Const r
  34   ;;
  35
  36   let eq_ind_r () =
  37     let r =
  38       !reference_of_oxuri
  39        (UriManager.uri_of_string
  40          "cic:/matita/logic/equality/eq_elim_r.con")
  41     in
  42     NCic.Const r
  43   ;;
  44
  45   let eq_refl () =
  46     let r =
  47       !reference_of_oxuri
  48        (UriManager.uri_of_string
  49          "cic:/matita/logic/equality/eq.ind#xpointer(1/1/1)")
  50     in
  51     NCic.Const r
  52   ;;
  53
  54   let extract lift vl t =
  55     let rec pos i = function
  56       | [] -> raise Not_found
  57       | j :: tl when j <> i -> 1+ pos i tl
  58       | _ -> 1
  59     in
  60     let vl_len = List.length vl in
  61     let rec extract = function
  62       | Terms.Leaf x -> NCicSubstitution.lift (vl_len+lift) x
  63       | Terms.Var j ->
  64            (try NCic.Rel (pos j vl) with Not_found -> NCic.Implicit `Term)
  65       | Terms.Node l -> NCic.Appl (List.map extract l)
  66     in
  67       extract t
  68   ;;
  69
  70    let mk_predicate hole_type amount ft p1 vl =
  71     let rec aux t p =
  72       match p with
  73       | [] -> NCic.Rel 1
  74       | n::tl ->
  75           match t with
  76           | Terms.Leaf _
  77           | Terms.Var _ ->
  78               let module Pp =
  79                 Pp.Pp(NCicBlob.NCicBlob(
  80                         struct
  81                           let metasenv = [] let subst = [] let context = []
  82                         end))
  83               in
  84                prerr_endline ("term: " ^ Pp.pp_foterm ft);
  85                prerr_endline ("path: " ^ String.concat ","
  86                  (List.map string_of_int p1));
  87                prerr_endline ("leading to: " ^ Pp.pp_foterm t);
  88                assert false
  89           | Terms.Node l ->
  90               let l =
  91                 HExtlib.list_mapi
  92                   (fun t i ->
  93                     if i = n then aux t tl
  94                     else extract amount (0::vl) t)
  95                   l
  96               in
  97               NCic.Appl l
  98     in
  99       NCic.Lambda("x", hole_type, aux ft (List.rev p1))
 100     ;;
 101
 102   let mk_proof (bag : NCic.term Terms.bag) mp steps =
 103     let module Subst = FoSubst in
 104     let position i l =
 105       let rec aux = function
 106        | [] -> assert false
 107        | (j,_) :: tl when i = j -> 1
 108        | _ :: tl -> 1 + aux tl
 109       in
 110         aux l
 111     in
 112     let vars_of i l = fst (List.assoc i l) in
 113     let ty_of i l = snd (List.assoc i l) in
 114     let close_with_lambdas vl t =
 115       List.fold_left
 116        (fun t i ->
 117           NCic.Lambda ("x"^string_of_int i, NCic.Implicit `Type, t))
 118        t vl
 119     in
 120     let close_with_forall vl t =
 121       List.fold_left
 122        (fun t i ->
 123           NCic.Prod ("x"^string_of_int i, NCic.Implicit `Type, t))
 124        t vl
 125     in
 126     let get_literal id =
 127       let (_, lit, vl, proof),_,_ = Terms.get_from_bag id bag in
 128       let lit =match lit with
 129           | Terms.Predicate t -> assert false
 130           | Terms.Equation (l,r,ty,_) ->
 131               Terms.Node [ Terms.Leaf eqP(); ty; l; r]
 132       in
 133         lit, vl, proof
 134     in
 135     let rec aux ongoal seen = function
 136       | [] -> NCic.Rel 1
 137       | id :: tl ->
 138           let amount = List.length seen in
 139           let lit,vl,proof = get_literal id in
 140           if not ongoal && id = mp then
 141             ((*prerr_endline ("Reached m point, id=" ^ (string_of_int id));*)
 142              NCic.LetIn ("clause_" ^ string_of_int id,
 143                 extract amount [] lit,
 144                 (NCic.Appl [eq_refl();NCic.Implicit `Type;NCic.Implicit `Term]),
 145                 aux true ((id,([],lit))::seen) (id::tl)))
 146           else
 147           match proof with
 148           | Terms.Exact _ when tl=[] ->
 149               (* prerr_endline ("Exact (tl=[]) for " ^ (string_of_int id));*)
 150               aux ongoal seen tl
 151           | Terms.Step _ when tl=[] -> assert false
 152           | Terms.Exact ft ->
 153               (* prerr_endline ("Exact for " ^ (string_of_int id));*)
 154                NCic.LetIn ("clause_" ^ string_of_int id,
 155                  close_with_forall vl (extract amount vl lit),
 156                  close_with_lambdas vl (extract amount vl ft),
 157                  aux ongoal
 158                    ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
 159           | Terms.Step (_, id1, id2, dir, pos, subst) ->
 160               let id, id1,(lit,vl,proof) =
 161                 if ongoal then id1,id,get_literal id1
 162                 else id,id1,(lit,vl,proof)
 163               in
 164               let vl = if ongoal then [](*Subst.filter subst vl*) else vl in
 165               let proof_of_id id =
 166                 let vars = List.rev (vars_of id seen) in
 167                 let args = List.map (Subst.apply_subst subst) vars in
 168                 let args = List.map (extract amount vl) args in
 169                 let rel_for_id = NCic.Rel (List.length vl + position id seen) in
 170                   if args = [] then rel_for_id
 171                   else NCic.Appl (rel_for_id::args)
 172               in
 173               let p_id1 = proof_of_id id1 in
 174               let p_id2 = proof_of_id id2 in
 175               let pred, hole_type, l, r =
 176                 let id1_ty = ty_of id1 seen in
 177                 let id2_ty,l,r =
 178                   match ty_of id2 seen with
 179                   | Terms.Node [ _; t; l; r ] ->
 180                       extract amount vl (Subst.apply_subst subst t),
 181                       extract amount vl (Subst.apply_subst subst l),
 182                       extract amount vl (Subst.apply_subst subst r)
 183                   | _ -> assert false
 184                 in
 185                   (*prerr_endline "mk_predicate :";
 186                   if ongoal then prerr_endline "ongoal=true"
 187                   else prerr_endline "ongoal=false";
 188                   prerr_endline ("id=" ^ string_of_int id);
 189                   prerr_endline ("id1=" ^ string_of_int id1);
 190                   prerr_endline ("id2=" ^ string_of_int id2);
 191                   prerr_endline ("Positions :" ^
 192                                    (String.concat ", "
 193                                       (List.map string_of_int pos)));*)
 194                 mk_predicate
 195                   id2_ty amount (Subst.apply_subst subst id1_ty) pos vl,
 196                 id2_ty,
 197                 l,r
 198               in
 199               let l, r, eq_ind =
 200                 if (ongoal=true) = (dir=Terms.Left2Right) then
 201                   r,l,eq_ind_r ()
 202                 else
 203                   l,r,eq_ind ()
 204               in
 205                NCic.LetIn ("clause_" ^ string_of_int id,
 206                  close_with_forall vl (extract amount vl lit),
 207                            (* NCic.Implicit `Type, *)
 208                  close_with_lambdas vl
 209                    (NCic.Appl [ eq_ind ; hole_type; l; pred; p_id1; r; p_id2 ]),
 210                  aux ongoal
 211                    ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl)
 212     in
 213       aux false [] steps
 214   ;;
 215