X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FnCicBlob.ml;h=621b22559a1e75a7338b1898414a73a98c008c9f;hb=a9e037fe189335607ab5d10523c836d8c7717245;hp=a0fa80adab1bbff4f949c37b69d3734a79ba52e1;hpb=6b0a195b180e3526af7b55771b2df7b10acd7c30;p=helm.git diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml index a0fa80ada..621b22559 100644 --- a/helm/software/components/ng_paramodulation/nCicBlob.ml +++ b/helm/software/components/ng_paramodulation/nCicBlob.ml @@ -27,10 +27,22 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct let rec compare x y = match x,y with | NCic.Rel i, NCic.Rel j -> i-j + | NCic.Meta (i,_), NCic.Meta (j,_) -> i-j | NCic.Const r1, NCic.Const r2 -> NReference.compare r1 r2 - | NCic.Appl l1, NCic.Appl l2 -> assert false (* TODO *) + | NCic.Appl l1, NCic.Appl l2 -> FoUtils.lexicograph compare l1 l2 + | NCic.Rel _, ( NCic.Meta _ | NCic.Const _ | NCic.Appl _ ) -> ~-1 + | ( NCic.Meta _ | NCic.Const _ | NCic.Appl _ ), NCic.Rel _ -> 1 + | NCic.Const _, ( NCic.Meta _ | NCic.Appl _ ) -> ~-1 + | ( NCic.Meta _ | NCic.Appl _ ), NCic.Const _ -> 1 + | NCic.Appl _, NCic.Meta _ -> ~-1 + | NCic.Meta _, NCic.Appl _ -> 1 | _ -> assert false ;; + + let compare x y = + if NCicReduction.alpha_eq C.metasenv C.subst C.context x y then 0 + else compare x y + ;; let pp t = NCicPp.ppterm ~context:C.context ~metasenv:C.metasenv ~subst:C.subst t;; @@ -63,7 +75,179 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct proof, sty ;; - let is_eq_predicate t = assert false;; + 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 rec ppfot = function + | Terms.Leaf _ -> "." + | Terms.Var i -> "?" ^ string_of_int i + | Terms.Node l -> "(" ^ String.concat " " (List.map ppfot l) ^ ")" + ;; + + let mk_predicate hole_type amount ft p vl = + let rec aux t p = + match p with + | [] -> NCic.Rel 1 + | n::tl -> + match t with + | Terms.Leaf _ + | Terms.Var _ -> + prerr_endline ("term: " ^ ppfot ft); + prerr_endline ("path: " ^ String.concat "," + (List.map string_of_int p)); + 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 p)) + ;; + + 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 rec aux ongoal seen = function + | [] -> NCic.Rel 1 + | id :: tl -> + let amount = List.length seen in + 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 + if not ongoal && id = mp then + (assert (vl = []); + NCic.LetIn ("clause_" ^ string_of_int id, + extract amount vl 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=[] -> aux ongoal seen tl + | Terms.Step _ when tl=[] -> assert false + | Terms.Exact ft -> + 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 = if ongoal then id1,id else id,id1 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 + NCic.Appl (NCic.Rel (List.length vl + position id seen) :: 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 + 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), + 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 + ;; end