let eqP = assert false;;
let saturate = assert false;;
+
+ let mk_proof = assert false;;
end
\ / This software is distributed as is, NO WARRANTY.
V_______________________________________________________________ *)
-module Subst (B : Terms.Blob) = struct
+(* module Subst (B : Terms.Blob) = struct *)
let id_subst = [];;
let concat x y = x @ y;;
-end
+(* end *)
(* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
+(*
module Subst (B : Terms.Blob) :
sig
- val id_subst : B.t Terms.substitution
+*)
+ val id_subst : 'a Terms.substitution
val build_subst :
- int -> B.t Terms.foterm -> B.t Terms.substitution ->
- B.t Terms.substitution
+ int -> 'a Terms.foterm -> 'a Terms.substitution ->
+ 'a Terms.substitution
val lookup_subst :
- int -> B.t Terms.substitution -> B.t Terms.foterm
- val filter : B.t Terms.substitution -> Terms.varlist -> Terms.varlist
+ int -> 'a Terms.substitution -> 'a Terms.foterm
+ val filter : 'a Terms.substitution -> Terms.varlist -> Terms.varlist
val apply_subst :
- B.t Terms.substitution -> B.t Terms.foterm -> B.t Terms.foterm
+ 'a Terms.substitution -> 'a Terms.foterm -> 'a Terms.foterm
val concat:
- B.t Terms.substitution -> B.t Terms.substitution ->
- B.t Terms.substitution
- end
+ 'a Terms.substitution -> 'a Terms.substitution ->
+ 'a Terms.substitution
+(* end *)
exception UnificationFailure of string Lazy.t;;
module Founif (B : Terms.Blob) = struct
- module Subst = FoSubst.Subst(B)
+ module Subst = FoSubst (*.Subst(B)*)
module U = FoUtils.Utils(B)
let unification vars locked_vars t1 t2 =
;;
module Utils (B : Terms.Blob) = struct
- module Subst = FoSubst.Subst(B) ;;
+ module Subst = FoSubst;; (*.Subst(B) ;;*)
module Order = Orderings.Orderings(B) ;;
let rec eq_foterm x y =
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
(* prerr_endline s *)
;;
-let nparamod metasenv subst context t table =
+let nparamod rdb metasenv subst context t table =
let nb_iter = ref 100 in
prerr_endline "========================================";
let module C = struct
in
let actives = [], IDX.DT.empty in
try given_clause bag maxvar actives passives g_actives g_passives
- with Sup.Success (bag, _, mp) ->
- prerr_endline "YES!";
- prerr_endline "Meeting point :"; prerr_endline (Pp.pp_unit_clause mp)
- (* prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag) *)
- | Failure _ -> prerr_endline "FAILURE"
+ with
+ | Sup.Success (bag, _, (i,_,_,_)) ->
+ let l =
+ let module S =
+ HTopoSort.Make(struct type t=int let compare=Pervasives.compare end)
+ in
+ let module C : Set.S with type elt = int =
+ Set.Make(struct type t=int let compare=Pervasives.compare end)
+ in
+ let all id =
+ let rec traverse acc i =
+ match Terms.M.find i bag with
+ | (_,_,_,Terms.Exact _) -> acc
+ | (_,_,_,Terms.Step (_,i1,i2,_,_,_)) ->
+ traverse (traverse (C.add i1 (C.add i2 acc)) i1) i2
+ in
+ C.elements (traverse C.empty id)
+ in
+ S.topological_sort (all i) all
+ in
+ prerr_endline "YES!";
+ prerr_endline "Proof:";
+ List.iter (fun x ->
+ prerr_endline (Pp.pp_unit_clause (Terms.M.find x bag))) l;
+ let proofterm = B.mk_proof bag l in
+ prerr_endline
+ (NCicPp.ppterm ~metasenv:C.metasenv ~subst:C.subst ~context:C.context
+ proofterm);
+ let _metasenv, _subst, _proofterm, _prooftype =
+ NCicRefiner.typeof rdb C.metasenv C.subst C.context proofterm None
+ in
+ ()
+ | Failure _ -> prerr_endline "FAILURE";
;;
val nparamod :
+ NRstatus.refiner_status ->
NCic.metasenv -> NCic.substitution -> NCic.context ->
(NCic.term * NCic.term) -> (NCic.term * NCic.term) list ->
unit
let pp_unit_clause ~formatter:f c =
let (id, l, vars, proof) = c in
- Format.fprintf f "Id : %d, " id ;
+ Format.fprintf f "Id : %3d, " id ;
match l with
| Terms.Predicate t ->
pp_foterm f t
| Terms.Equation (lhs, rhs, ty, comp) ->
- Format.fprintf f "{";
+ Format.fprintf f "@[<hv>{";
pp_foterm f ty;
- Format.fprintf f "}: ";
+ Format.fprintf f "}:@;@[<hv>";
pp_foterm f lhs;
- Format.fprintf f " %s " (string_of_comparison comp);
+ Format.fprintf f "@;%s@;" (string_of_comparison comp);
pp_foterm f rhs;
- Format.fprintf f " [%s] by %s"
+ Format.fprintf f "@]@;[%s] by %s@]"
(String.concat ", " (List.map string_of_int vars))
(match proof with
| Terms.Exact _ -> "axiom"
struct
module IDX = Index.Index(B)
module Unif = FoUnif.Founif(B)
- module Subst = FoSubst.Subst(B)
+ module Subst = FoSubst (*.Subst(B)*)
module Order = Orderings.Orderings(B)
module Utils = FoUtils.Utils(B)
module Pp = Pp.Pp(B)
val pp : t -> string
val embed : t -> t foterm
val saturate : t -> t -> t foterm * t foterm
+ val mk_proof : t bag -> int list -> t
end
val embed : t -> t foterm
(* saturate [proof] [type] -> [proof] * [type] *)
val saturate : t -> t -> t foterm * t foterm
+
+ val mk_proof : t bag -> int list -> t
+
end
(status, (t,ty) :: l))
(status,[]) l
in
- Paramod.nparamod metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l;
+ let rdb = status.estatus.NEstatus.rstatus.NRstatus.refiner_status in
+ Paramod.nparamod rdb metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l;
status
;;
projects / helm.git / commitdiff