X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_paramodulation%2FnCicBlob.ml;h=5aded532907f4d9acd6e373b60633314f86d044f;hb=8bc5bc0e8375a85736f6a5df317d129d5efa8de4;hp=e01edfae309e30053ea336e3aeee2d35ba658536;hpb=b97a7976503b2d2e5cbc9199f848135a324775a8;p=helm.git diff --git a/helm/software/components/ng_paramodulation/nCicBlob.ml b/helm/software/components/ng_paramodulation/nCicBlob.ml index e01edfae3..5aded5329 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;; @@ -46,6 +58,155 @@ module NCicBlob(C : NCicContext) : Terms.Blob with type t = NCic.term = struct (fun (r,v) t -> let r1,v1 = embed t in (r1::r),aux [] v v1) ([],[]) l in (Terms.Node (List.rev res)), vars | t -> Terms.Leaf t, [] -;; + ;; + + let embed t = fst (embed t) ;; + + let saturate t ty = + let sty, _, args = + NCicMetaSubst.saturate ~delta:max_int C.metasenv C.subst C.context + ty 0 + in + let proof = + if args = [] then Terms.Leaf t + else Terms.Node (Terms.Leaf t :: List.map embed args) + in + let sty = embed sty in + proof, sty + ;; + + 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 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 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", NCic.Implicit `Type, aux ft (List.rev p)) + ;; + + let mk_proof (bag : NCic.term Terms.bag) 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 rec aux seen = function + | [] -> NCic.Rel 1 + | id :: tl -> +(* prerr_endline ("Let4 : " ^string_of_int id); *) + 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 +(* prerr_endline ("X" ^ ppfot lit); *) + match proof with + | Terms.Exact ft -> + NCic.LetIn ("clause_" ^ string_of_int id, NCic.Implicit `Type, + close_with_lambdas vl (extract amount vl ft), + aux ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl) + | Terms.Step (_, id1, id2, dir, pos, subst) -> + let proof_of_id id = + let vars = 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 = + let id1_ty = ty_of id1 seen in + mk_predicate amount (Subst.apply_subst subst id1_ty) pos vl + in + let eq_ind = if dir=Terms.Left2Right then eq_ind else eq_ind_r in + NCic.LetIn ("clause_" ^ string_of_int id, NCic.Implicit `Type, + close_with_lambdas vl + (NCic.Appl [ eq_ind ; NCic.Implicit `Type; + pred; NCic.Implicit `Term; p_id1; + NCic.Implicit `Term; p_id2 ]), + aux ((id,(List.map (fun x -> Terms.Var x) vl,lit))::seen) tl) + in + aux [] steps + ;; end