(* $Id: inference.ml 6245 2006-04-05 12:07:51Z tassi $ *)
-
-(******* CIC substitution ***************************************************)
-
-type cic_substitution = Cic.substitution
-let cic_apply_subst = CicMetaSubst.apply_subst
-let cic_apply_subst_metasenv = CicMetaSubst.apply_subst_metasenv
-let cic_ppsubst = CicMetaSubst.ppsubst
-let cic_buildsubst n context t ty tail = (n,(context,t,ty)) :: tail
-let cic_flatten_subst subst =
- List.map
- (fun (i, (context, term, ty)) ->
- let context = (* cic_apply_subst_context subst*) context in
- let term = cic_apply_subst subst term in
- let ty = cic_apply_subst subst ty in
- (i, (context, term, ty))) subst
-let rec cic_lookup_subst meta subst =
- match meta with
- | Cic.Meta (i, _) -> (
- try let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst
- in cic_lookup_subst t subst
- with Not_found -> meta
- )
- | _ -> meta
-;;
-
-let cic_merge_subst_if_possible s1 s2 =
- let already_in = Hashtbl.create 13 in
- let rec aux acc = function
- | ((i,_,x) as s)::tl ->
- (try
- let x' = Hashtbl.find already_in i in
- if x = x' then aux acc tl else None
- with
- | Not_found ->
- Hashtbl.add already_in i x;
- aux (s::acc) tl)
- | [] -> Some acc
- in
- aux [] (s1@s2)
-;;
-
-(******** NAIF substitution **************************************************)
-(*
- * naif version of apply subst; the local context of metas is ignored;
- * we assume the substituted term must be lifted according to the nesting
- * depth of the meta.
- * Alternatively, we could used implicit instead of metas
- *)
-
-type naif_substitution = (int * Cic.term) list
-
-let naif_apply_subst subst term =
- let rec aux k t =
- match t with
- Cic.Rel _ -> t
- | Cic.Var (uri,exp_named_subst) ->
- let exp_named_subst' =
- List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
- in
- Cic.Var (uri, exp_named_subst')
- | Cic.Meta (i, l) ->
- (try
- aux k (CicSubstitution.lift k (List.assoc i subst))
- with Not_found -> t)
- | Cic.Sort _
- | Cic.Implicit _ -> t
- | Cic.Cast (te,ty) -> Cic.Cast (aux k te, aux k ty)
- | Cic.Prod (n,s,t) -> Cic.Prod (n, aux k s, aux (k+1) t)
- | Cic.Lambda (n,s,t) -> Cic.Lambda (n, aux k s, aux (k+1) t)
- | Cic.LetIn (n,s,t) -> Cic.LetIn (n, aux k s, aux (k+1) t)
- | Cic.Appl [] -> assert false
- | Cic.Appl l -> Cic.Appl (List.map (aux k) l)
- | Cic.Const (uri,exp_named_subst) ->
- let exp_named_subst' =
- List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
- in
- if exp_named_subst' != exp_named_subst then
- Cic.Const (uri, exp_named_subst')
- else
- t (* TODO: provare a mantenere il piu' possibile sharing *)
- | Cic.MutInd (uri,typeno,exp_named_subst) ->
- let exp_named_subst' =
- List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
- in
- Cic.MutInd (uri,typeno,exp_named_subst')
- | Cic.MutConstruct (uri,typeno,consno,exp_named_subst) ->
- let exp_named_subst' =
- List.map (fun (uri, t) -> (uri, aux k t)) exp_named_subst
- in
- Cic.MutConstruct (uri,typeno,consno,exp_named_subst')
- | Cic.MutCase (sp,i,outty,t,pl) ->
- let pl' = List.map (aux k) pl in
- Cic.MutCase (sp, i, aux k outty, aux k t, pl')
- | Cic.Fix (i, fl) ->
- let len = List.length fl in
- let fl' =
- List.map
- (fun (name, i, ty, bo) -> (name, i, aux k ty, aux (k+len) bo)) fl
- in
- Cic.Fix (i, fl')
- | Cic.CoFix (i, fl) ->
- let len = List.length fl in
- let fl' =
- List.map (fun (name, ty, bo) -> (name, aux k ty, aux (k+len) bo)) fl
- in
- Cic.CoFix (i, fl')
-in
- aux 0 term
-;;
-
-(* naif version of apply_subst_metasenv: we do not apply the
-substitution to the context *)
-
-let naif_apply_subst_metasenv subst metasenv =
- List.map
- (fun (n, context, ty) ->
- (n, context, naif_apply_subst subst ty))
- (List.filter
- (fun (i, _, _) -> not (List.mem_assoc i subst))
- metasenv)
-
-let naif_ppsubst names subst =
- "{" ^ String.concat "; "
- (List.map
- (fun (idx, t) ->
- Printf.sprintf "%d:= %s" idx (CicPp.pp t names))
- subst) ^ "}"
-;;
-
-let naif_buildsubst n context t ty tail = (n,t) :: tail ;;
-
-let naif_flatten_subst subst =
- List.map (fun (i,t) -> i, naif_apply_subst subst t ) subst
-;;
-
-let rec naif_lookup_subst meta subst =
- match meta with
- | Cic.Meta (i, _) ->
- (try
- naif_lookup_subst (List.assoc i subst) subst
- with
- Not_found -> meta)
- | _ -> meta
-;;
-
-let naif_merge_subst_if_possible s1 s2 =
- let already_in = Hashtbl.create 13 in
- let rec aux acc = function
- | ((i,x) as s)::tl ->
- (try
- let x' = Hashtbl.find already_in i in
- if x = x' then aux acc tl else None
- with
- | Not_found ->
- Hashtbl.add already_in i x;
- aux (s::acc) tl)
- | [] -> Some acc
- in
- aux [] (s1@s2)
-;;
-
-(********** ACTUAL SUBSTITUTION IMPLEMENTATION *******************************)
-
-type substitution = naif_substitution
-let apply_subst = naif_apply_subst
-let apply_subst_metasenv = naif_apply_subst_metasenv
-let ppsubst ~names l = naif_ppsubst (names:(Cic.name option)list) l
-let buildsubst = naif_buildsubst
-let flatten_subst = naif_flatten_subst
-let lookup_subst = naif_lookup_subst
-
-(* filter out from metasenv the variables in substs *)
-let filter subst metasenv =
- List.filter
- (fun (m, _, _) ->
- try let _ = List.find (fun (i, _) -> m = i) subst in false
- with Not_found -> true)
- metasenv
-;;
-
-let is_in_subst i subst = List.mem_assoc i subst;;
-
-let merge_subst_if_possible = naif_merge_subst_if_possible;;
-
-let empty_subst = [];;
-
-(********* EQUALITY **********************************************************)
-
type rule = SuperpositionRight | SuperpositionLeft | Demodulation
type uncomparable = int -> int
type equality =
Utils.comparison) * (* ordering *)
Cic.metasenv * (* environment for metas *)
int (* id *)
-and proof = new_proof * old_proof
-
-and new_proof =
+and proof =
| Exact of Cic.term
- | Step of substitution * (rule * int*(Utils.pos*int)* Cic.term) (* eq1, eq2,predicate *)
-and old_proof =
- | NoProof (* term is the goal missing a proof *)
- | BasicProof of substitution * Cic.term
- | ProofBlock of
- substitution * UriManager.uri *
- (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * old_proof
- | ProofGoalBlock of old_proof * old_proof
- | ProofSymBlock of Cic.term list * old_proof
- | SubProof of Cic.term * int * old_proof
-and goal_proof = (Utils.pos * int * substitution * Cic.term) list
+ | Step of Subst.substitution * (rule * int*(Utils.pos*int)* Cic.term)
+ (* subst, (rule,eq1, eq2,predicate) *)
+and goal_proof = (Utils.pos * int * Subst.substitution * Cic.term) list
;;
(* globals *)
let uncomparable = fun _ -> 0
-let mk_equality (weight,(newp,oldp),(ty,l,r,o),m) =
+let mk_equality (weight,p,(ty,l,r,o),m) =
let id = freshid () in
- let eq = (uncomparable,weight,(newp,oldp),(ty,l,r,o),m,id) in
+ let eq = (uncomparable,weight,p,(ty,l,r,o),m,id) in
Hashtbl.add id_to_eq id eq;
eq
;;
+let mk_tmp_equality (weight,(ty,l,r,o),m) =
+ let id = -1 in
+ uncomparable,weight,Exact (Cic.Implicit None),(ty,l,r,o),m,id
+;;
+
+
let open_equality (_,weight,proof,(ty,l,r,o),m,id) =
(weight,proof,(ty,l,r,o),m,id)
Pervasives.compare s1 s2
;;
-let rec string_of_proof_old ?(names=[]) = function
- | NoProof -> "NoProof "
- | BasicProof (s, t) -> "BasicProof(" ^
- ppsubst ~names s ^ ", " ^ (CicPp.pp t names) ^ ")"
- | SubProof (t, i, p) ->
- Printf.sprintf "SubProof(%s, %s, %s)"
- (CicPp.pp t names) (string_of_int i) (string_of_proof_old p)
- | ProofSymBlock (_,p) ->
- Printf.sprintf "ProofSymBlock(%s)" (string_of_proof_old p)
- | ProofBlock (subst, _, _, _ ,(_,eq),old) ->
- let _,(_,p),_,_,_ = open_equality eq in
- "ProofBlock(" ^ (ppsubst ~names subst) ^ "," ^ (string_of_proof_old old) ^ "," ^
- string_of_proof_old p ^ ")"
- | ProofGoalBlock (p1, p2) ->
- Printf.sprintf "ProofGoalBlock(%s, %s)"
- (string_of_proof_old p1) (string_of_proof_old p2)
-;;
-
-
let proof_of_id id =
try
- let (_,(p,_),(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
+ let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
p,l,r
with
Not_found -> assert false
-let string_of_proof_new ?(names=[]) p gp =
+let string_of_proof ?(names=[]) p gp =
let str_of_rule = function
| SuperpositionRight -> "SupR"
| SuperpositionLeft -> "SupL"
prefix (CicPp.pp t names)
| Step (subst,(rule,eq1,(pos,eq2),pred)) ->
Printf.sprintf "%s%s(%s|%d with %d dir %s pred %s))\n"
- prefix (str_of_rule rule) (ppsubst ~names subst) eq1 eq2 (str_of_pos pos)
+ prefix (str_of_rule rule) (Subst.ppsubst ~names subst) eq1 eq2 (str_of_pos pos)
(CicPp.pp pred names)^
aux (margin+1) (Printf.sprintf "%d" eq1) (fst3 (proof_of_id eq1)) ^
aux (margin+1) (Printf.sprintf "%d" eq2) (fst3 (proof_of_id eq2))
(fun (pos,i,s,t) ->
(Printf.sprintf
"GOAL: %s %d %s %s\n"
- (str_of_pos pos) i (ppsubst ~names s) (CicPp.pp t names)) ^
+ (str_of_pos pos) i (Subst.ppsubst ~names s) (CicPp.pp t names)) ^
aux 1 (Printf.sprintf "%d " i) (fst3 (proof_of_id i)))
gp)
;;
-let ppsubst = ppsubst ~names:[]
+let rec depend eq id =
+ let (_,p,(_,_,_,_),_,ideq) = open_equality eq in
+ if id = ideq then true else
+ match p with
+ Exact _ -> false
+ | Step (_,(_,id1,(_,id2),_)) ->
+ let eq1 = Hashtbl.find id_to_eq id1 in
+ let eq2 = Hashtbl.find id_to_eq id2 in
+ depend eq1 id || depend eq2 id
+;;
+
+let ppsubst = Subst.ppsubst ~names:[];;
(* returns an explicit named subst and a list of arguments for sym_eq_URI *)
let build_ens uri termlist =
| _ -> assert false
;;
-let build_proof_term_old ?(noproof=Cic.Implicit None) proof =
- let rec do_build_proof proof =
- match proof with
- | NoProof ->
- Printf.fprintf stderr "WARNING: no proof!\n";
- noproof
- | BasicProof (s,term) -> apply_subst s term
- | ProofGoalBlock (proofbit, proof) ->
- print_endline "found ProofGoalBlock, going up...";
- do_build_goal_proof proofbit proof
- | ProofSymBlock (termlist, proof) ->
- let proof = do_build_proof proof in
- let ens, args = build_ens (Utils.sym_eq_URI ()) termlist in
- Cic.Appl ([Cic.Const (Utils.sym_eq_URI (), ens)] @ args @ [proof])
- | ProofBlock (subst, eq_URI, (name, ty), bo, (pos, eq), eqproof) ->
- let t' = Cic.Lambda (name, ty, bo) in
- let _, (_,proof), (ty, what, other, _), menv',_ = open_equality eq in
- let proof' = do_build_proof proof in
- let eqproof = do_build_proof eqproof in
- let what, other =
- if pos = Utils.Left then what, other else other, what
- in
- apply_subst subst
- (Cic.Appl [Cic.Const (eq_URI, []); ty;
- what; t'; eqproof; other; proof'])
- | SubProof (term, meta_index, proof) ->
- let proof = do_build_proof proof in
- let eq i = function
- | Cic.Meta (j, _) -> i = j
- | _ -> false
- in
- ProofEngineReduction.replace
- ~equality:eq ~what:[meta_index] ~with_what:[proof] ~where:term
-
- and do_build_goal_proof proofbit proof =
- match proof with
- | ProofGoalBlock (pb, p) ->
- do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p))
- | _ -> do_build_proof (replace_proof proofbit proof)
-
- and replace_proof newproof = function
- | ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof) ->
- let eqproof' = replace_proof newproof eqproof in
- ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof')
- | ProofGoalBlock (pb, p) ->
- let pb' = replace_proof newproof pb in
- ProofGoalBlock (pb', p)
- | BasicProof _ -> newproof
- | SubProof (term, meta_index, p) ->
- SubProof (term, meta_index, replace_proof newproof p)
- | p -> p
- in
- do_build_proof proof
-;;
-
let mk_sym uri ty t1 t2 p =
let ens, args = build_ens uri [ty;t1;t2;p] in
Cic.Appl (Cic.Const(uri, ens) :: args)
| _ -> assert false
;;
+let open_eq_ind args =
+ match args with
+ | [ty;l;pred;pl;r;pleqr] -> ty,l,pred,pl,r,pleqr
+ | _ -> assert false
+;;
+
+let open_pred pred =
+ match pred with
+ | Cic.Lambda (_,ty,(Cic.Appl [Cic.MutInd (uri, 0,_);_;l;r]))
+ when LibraryObjects.is_eq_URI uri -> ty,uri,l,r
+ | _ -> prerr_endline (CicPp.ppterm pred); assert false
+;;
+
+let is_not_fixed t =
+ CicSubstitution.subst (Cic.Implicit None) t <>
+ CicSubstitution.subst (Cic.Rel 1) t
+;;
+
+
let canonical t =
let rec remove_refl t =
match t with
| Cic.Appl l -> Cic.Appl (List.map canonical l)
| _ -> t
in
- remove_refl (canonical t)
+ remove_refl (canonical t)
+;;
+
+let ty_of_lambda = function
+ | Cic.Lambda (_,ty,_) -> ty
+ | _ -> assert false
;;
+let compose_contexts ctx1 ctx2 =
+ ProofEngineReduction.replace_lifting
+ ~equality:(=) ~what:[Cic.Rel 1] ~with_what:[ctx2] ~where:ctx1
+;;
+
+let put_in_ctx ctx t =
+ ProofEngineReduction.replace_lifting
+ ~equality:(=) ~what:[Cic.Rel 1] ~with_what:[t] ~where:ctx
+;;
+
+let mk_eq uri ty l r =
+ Cic.Appl [Cic.MutInd(uri,0,[]);ty;l;r]
+;;
+
+let mk_refl uri ty t =
+ Cic.Appl [Cic.MutConstruct(uri,0,1,[]);ty;t]
+;;
+
+let open_eq = function
+ | Cic.Appl [Cic.MutInd(uri,0,[]);ty;l;r] when LibraryObjects.is_eq_URI uri ->
+ uri, ty, l ,r
+ | _ -> assert false
+;;
+
+let contextualize uri ty left right t =
+ (* aux [uri] [ty] [left] [right] [ctx] [t]
+ *
+ * the parameters validate this invariant
+ * t: eq(uri) ty left right
+ * that is used only by the base case
+ *
+ * ctx is a term with an open (Rel 1). (Rel 1) is the empty context
+ *)
+ let rec aux uri ty left right ctx_d = function
+ | Cic.Appl ((Cic.Const(uri_ind,ens))::tl)
+ when LibraryObjects.is_eq_ind_URI uri_ind ||
+ LibraryObjects.is_eq_ind_r_URI uri_ind ->
+ let ty1,what,pred,p1,other,p2 = open_eq_ind tl in
+ let ty2,eq,lp,rp = open_pred pred in
+ let uri_trans = LibraryObjects.trans_eq_URI ~eq:uri in
+ let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in
+ let is_not_fixed_lp = is_not_fixed lp in
+ let avoid_eq_ind = LibraryObjects.is_eq_ind_URI uri_ind in
+ (* extract the context and the fixed term from the predicate *)
+ let m, ctx_c =
+ let m, ctx_c = if is_not_fixed_lp then rp,lp else lp,rp in
+ (* they were under a lambda *)
+ let m = CicSubstitution.subst (Cic.Implicit None) m in
+ let ctx_c = CicSubstitution.subst (Cic.Rel 1) ctx_c in
+ m, ctx_c
+ in
+ (* create the compound context and put the terms under it *)
+ let ctx_dc = compose_contexts ctx_d ctx_c in
+ let dc_what = put_in_ctx ctx_dc what in
+ let dc_other = put_in_ctx ctx_dc other in
+ (* m is already in ctx_c so it is put in ctx_d only *)
+ let d_m = put_in_ctx ctx_d m in
+ (* we also need what in ctx_c *)
+ let c_what = put_in_ctx ctx_c what in
+ (* now put the proofs in the compound context *)
+ let p1 = (* p1: dc_what = d_m *)
+ if is_not_fixed_lp then
+ aux uri ty1 c_what m ctx_d p1
+ else
+ mk_sym uri_sym ty d_m dc_what
+ (aux uri ty1 m c_what ctx_d p1)
+ in
+ let p2 = (* p2: dc_other = dc_what *)
+ if avoid_eq_ind then
+ mk_sym uri_sym ty dc_what dc_other
+ (aux uri ty1 what other ctx_dc p2)
+ else
+ aux uri ty1 other what ctx_dc p2
+ in
+ (* if pred = \x.C[x]=m --> t : C[other]=m --> trans other what m
+ if pred = \x.m=C[x] --> t : m=C[other] --> trans m what other *)
+ let a,b,c,paeqb,pbeqc =
+ if is_not_fixed_lp then
+ dc_other,dc_what,d_m,p2,p1
+ else
+ d_m,dc_what,dc_other,
+ (mk_sym uri_sym ty dc_what d_m p1),
+ (mk_sym uri_sym ty dc_other dc_what p2)
+ in
+ mk_trans uri_trans ty a b c paeqb pbeqc
+ | t ->
+ let uri_sym = LibraryObjects.sym_eq_URI ~eq:uri in
+ let uri_ind = LibraryObjects.eq_ind_URI ~eq:uri in
+ let pred =
+ (* ctx_d will go under a lambda, but put_in_ctx substitutes Rel 1 *)
+ let ctx_d = CicSubstitution.lift_from 2 1 ctx_d in (* bleah *)
+ let r = put_in_ctx ctx_d (CicSubstitution.lift 1 left) in
+ let l = ctx_d in
+ let lty = CicSubstitution.lift 1 ty in
+ Cic.Lambda (Cic.Name "foo",ty,(mk_eq uri lty l r))
+ in
+ let d_left = put_in_ctx ctx_d left in
+ let d_right = put_in_ctx ctx_d right in
+ let refl_eq = mk_refl uri ty d_left in
+ mk_sym uri_sym ty d_right d_left
+ (mk_eq_ind uri_ind ty left pred refl_eq right t)
+ in
+ let empty_context = Cic.Rel 1 in
+ aux uri ty left right empty_context t
+;;
+
+let contextualize_rewrites t ty =
+ let eq,ty,l,r = open_eq ty in
+ contextualize eq ty l r t
+;;
+
let build_proof_step subst p1 p2 pos l r pred =
- let p1 = apply_subst subst p1 in
- let p2 = apply_subst subst p2 in
- let l = apply_subst subst l in
- let r = apply_subst subst r in
- let pred = apply_subst subst pred in
- let ty,body = (* Cic.Implicit None *)
+ let p1 = Subst.apply_subst subst p1 in
+ let p2 = Subst.apply_subst subst p2 in
+ let l = Subst.apply_subst subst l in
+ let r = Subst.apply_subst subst r in
+ let pred = Subst.apply_subst subst pred in
+ let ty,body =
match pred with
| Cic.Lambda (_,ty,body) -> ty,body
| _ -> assert false
in
- let what, other = (* Cic.Implicit None, Cic.Implicit None *)
+ let what, other =
if pos = Utils.Left then l,r else r,l
in
- let is_not_fixed t =
- CicSubstitution.subst (Cic.Implicit None) t <>
- CicSubstitution.subst (Cic.Rel 1) t
- in
- match body,pos with
- |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Left ->
- let third = CicSubstitution.subst (Cic.Implicit None) third in
- let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- let uri_sym = LibraryObjects.sym_eq_URI ~eq in
- mk_trans uri_trans ty other what third
- (mk_sym uri_sym ty what other p2) p1
- |Cic.Appl [Cic.MutInd(eq,_,_);_;Cic.Rel 1;third],Utils.Right ->
- let third = CicSubstitution.subst (Cic.Implicit None) third in
- let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- mk_trans uri_trans ty other what third p2 p1
- |Cic.Appl [Cic.MutInd(eq,_,_);_;third;Cic.Rel 1],Utils.Left ->
- let third = CicSubstitution.subst (Cic.Implicit None) third in
- let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- mk_trans uri_trans ty third what other p1 p2
- |Cic.Appl [Cic.MutInd(eq,_,_);_;third;Cic.Rel 1],Utils.Right ->
- let third = CicSubstitution.subst (Cic.Implicit None) third in
- let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- let uri_sym = LibraryObjects.sym_eq_URI ~eq in
- mk_trans uri_trans ty third what other p1
- (mk_sym uri_sym ty other what p2)
- | Cic.Appl [Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed lhs
- ->
- let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in
- let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- let pred_of t = CicSubstitution.subst t lhs in
- let pred_of_what = pred_of what in
- let pred_of_other = pred_of other in
- (* p2 : what = other
- * ====================================
- * inject p2: P(what) = P(other)
- *)
- let rec inject ty lhs what other p2 =
- match p2 with
- | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
- when LibraryObjects.is_trans_eq_URI uri_trans ->
- let ty,l,m,r,plm,pmr = open_trans ens tl in
- mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l)
- (inject ty lhs m r pmr) (inject ty lhs l m plm)
- | _ ->
- let liftedty = CicSubstitution.lift 1 ty in
- let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
- let refl_eq_part =
- Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
- in
- (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
- (Cic.Lambda (Cic.Name "foo",ty,
- (Cic.Appl
- [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
- refl_eq_part what p2)
- in
- mk_trans uri_trans ty pred_of_other pred_of_what rhs
- (inject ty lhs what other p2) p1
- | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed lhs
- ->
- let rhs = CicSubstitution.subst (Cic.Implicit None) rhs in
- let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- let pred_of t = CicSubstitution.subst t lhs in
- let pred_of_what = pred_of what in
- let pred_of_other = pred_of other in
- (* p2 : what = other
- * ====================================
- * inject p2: P(what) = P(other)
- *)
- let rec inject ty lhs what other p2 =
- match p2 with
- | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
- when LibraryObjects.is_trans_eq_URI uri_trans ->
- let ty,l,m,r,plm,pmr = open_trans ens tl in
- mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r)
- (inject ty lhs m l plm)
- (inject ty lhs r m pmr)
- | _ ->
- let liftedty = CicSubstitution.lift 1 ty in
- let lifted_pred_of_other =
- CicSubstitution.lift 1 (pred_of other) in
- let refl_eq_part =
- Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
- in
- mk_eq_ind (Utils.eq_ind_URI ()) ty other
- (Cic.Lambda (Cic.Name "foo",ty,
- (Cic.Appl
- [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
- refl_eq_part what p2
- in
- mk_trans uri_trans ty pred_of_other pred_of_what rhs
- (inject ty lhs what other p2) p1
- | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Right when is_not_fixed rhs
- ->
- let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in
- let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- let pred_of t = CicSubstitution.subst t rhs in
- let pred_of_what = pred_of what in
- let pred_of_other = pred_of other in
- (* p2 : what = other
- * ====================================
- * inject p2: P(what) = P(other)
- *)
- let rec inject ty lhs what other p2 =
- match p2 with
- | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
- when LibraryObjects.is_trans_eq_URI uri_trans ->
- let ty,l,m,r,plm,pmr = open_trans ens tl in
- mk_trans uri_trans ty (pred_of r) (pred_of m) (pred_of l)
- (inject ty lhs m r pmr)
- (inject ty lhs l m plm)
- | _ ->
- let liftedty = CicSubstitution.lift 1 ty in
- let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
- let refl_eq_part =
- Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
- in
- (mk_eq_ind (Utils.eq_ind_r_URI ()) ty other
- (Cic.Lambda (Cic.Name "foo",ty,
- (Cic.Appl
- [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
- refl_eq_part what p2)
- in
- mk_trans uri_trans ty lhs pred_of_what pred_of_other
- p1 (inject ty rhs other what p2)
- | Cic.Appl[Cic.MutInd(eq,_,_);_;lhs;rhs],Utils.Left when is_not_fixed rhs
- ->
- let lhs = CicSubstitution.subst (Cic.Implicit None) lhs in
- let uri_trans = LibraryObjects.trans_eq_URI ~eq in
- let pred_of t = CicSubstitution.subst t rhs in
- let pred_of_what = pred_of what in
- let pred_of_other = pred_of other in
- (* p2 : what = other
- * ====================================
- * inject p2: P(what) = P(other)
- *)
- let rec inject ty lhs what other p2 =
- match p2 with
- | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
- when LibraryObjects.is_trans_eq_URI uri_trans ->
- let ty,l,m,r,plm,pmr = open_trans ens tl in
- (mk_trans uri_trans ty (pred_of l) (pred_of m) (pred_of r)
- (inject ty lhs m l plm)
- (inject ty lhs r m pmr))
- | _ ->
- let liftedty = CicSubstitution.lift 1 ty in
- let lifted_pred_of_other = CicSubstitution.lift 1 (pred_of other) in
- let refl_eq_part =
- Cic.Appl [Cic.MutConstruct(eq,0,1,[]);ty;pred_of other]
- in
- mk_eq_ind (Utils.eq_ind_URI ()) ty other
- (Cic.Lambda (Cic.Name "foo",ty,
- (Cic.Appl
- [Cic.MutInd(eq,0,[]);liftedty;lifted_pred_of_other;lhs])))
- refl_eq_part what p2
- in
- mk_trans uri_trans ty lhs pred_of_what pred_of_other
- p1 (inject ty rhs other what p2)
- | _, Utils.Left ->
+ match pos with
+ | Utils.Left ->
mk_eq_ind (Utils.eq_ind_URI ()) ty what pred p1 other p2
- | _, Utils.Right ->
+ | Utils.Right ->
mk_eq_ind (Utils.eq_ind_r_URI ()) ty what pred p1 other p2
;;
-let build_proof_term_new proof =
+let build_proof_term proof =
let rec aux = function
| Exact term -> term
| Step (subst,(_, id1, (pos,id2), pred)) ->
aux proof
;;
-let wfo goalproof =
+let wfo goalproof proof =
let rec aux acc id =
let p,_,_ = proof_of_id id in
match p with
- | Exact _ -> id :: acc
+ | Exact _ -> if (List.mem id acc) then acc else id :: acc
| Step (_,(_,id1, (_,id2), _)) ->
let acc = if not (List.mem id1 acc) then aux acc id1 else acc in
let acc = if not (List.mem id2 acc) then aux acc id2 else acc in
id :: acc
in
- List.fold_left (fun acc (_,id,_,_) -> aux acc id) [] goalproof
+ let acc =
+ match proof with
+ | Exact _ -> []
+ | Step (_,(_,id1, (_,id2), _)) -> aux (aux [] id1) id2
+ in
+ List.fold_left (fun acc (_,id,_,_) -> aux acc id) acc goalproof
;;
let string_of_id names id =
try
- let (_,(p,_),(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
+ let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
match p with
| Exact t ->
Printf.sprintf "%d = %s: %s = %s" id
(CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names)
| Step (_,(step,id1, (_,id2), _) ) ->
- Printf.sprintf "%5d: %s %4d %4d %s = %s" id
+ Printf.sprintf "%6d: %s %6d %6d %s = %s" id
(if step = SuperpositionRight then "SupR" else "Demo")
id1 id2 (CicPp.pp l names) (CicPp.pp r names)
with
Not_found -> assert false
-let pp_proof names goalproof =
- String.concat "\n" (List.map (string_of_id names) (wfo goalproof))
-
-let build_goal_proof l initial =
- let proof =
- List.fold_left
- (fun current_proof (pos,id,subst,pred) ->
- let p,l,r = proof_of_id id in
- let p = build_proof_term_new p in
- let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
- build_proof_step subst current_proof p pos l r pred)
- initial l
+let pp_proof names goalproof proof =
+ String.concat "\n" (List.map (string_of_id names) (wfo goalproof proof)) ^
+ "\ngoal is demodulated with " ^
+ (String.concat " "
+ ((List.map (fun (_,i,_,_) -> string_of_int i) goalproof)))
+;;
+
+let build_goal_proof l initial ty se =
+ let se = List.map (fun i -> Cic.Meta (i,[])) se in
+ let proof,se =
+ let rec aux se current_proof = function
+ | [] -> current_proof,se
+ | (pos,id,subst,pred)::tl ->
+ let p,l,r = proof_of_id id in
+ let p = build_proof_term p in
+ let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
+ let proof = build_proof_step subst current_proof p pos l r pred in
+ let proof,se = aux se proof tl in
+ Subst.apply_subst subst proof,
+ List.map (fun x -> Subst.apply_subst subst x) se
+ in
+ aux se initial l
in
- canonical proof
+ canonical (contextualize_rewrites proof ty), se
;;
let refl_proof ty term =
ty; term]
;;
-let metas_of_proof p = Utils.metas_of_term (build_proof_term_old (snd p)) ;;
+let metas_of_proof p =
+ let p = build_proof_term p in
+ Utils.metas_of_term p
+;;
let relocate newmeta menv =
let subst, metasenv, newmeta =
let irl = [] (*
CicMkImplicit.identity_relocation_list_for_metavariable context *)
in
- let newsubst = buildsubst i context (Cic.Meta(maxmeta,irl)) ty subst in
+ let newsubst = Subst.buildsubst i context (Cic.Meta(maxmeta,irl)) ty subst in
let newmeta = maxmeta, context, ty in
newsubst, newmeta::menv, maxmeta+1)
- menv ([], [], newmeta+1)
+ menv (Subst.empty_subst, [], newmeta+1)
in
- let metasenv = apply_subst_metasenv subst metasenv in
- let subst = flatten_subst subst in
+ let metasenv = Subst.apply_subst_metasenv subst metasenv in
+ let subst = Subst.flatten_subst subst in
subst, metasenv, newmeta
let fix_metas newmeta eq =
- let w, (p1,p2), (ty, left, right, o), menv,_ = open_equality eq in
+ let w, p, (ty, left, right, o), menv,_ = open_equality eq in
(* debug
let _ , eq =
fix_metas_old newmeta (w, p, (ty, left, right, o), menv, args) in
prerr_endline (string_of_equality eq); *)
let subst, metasenv, newmeta = relocate newmeta menv in
- let ty = apply_subst subst ty in
- let left = apply_subst subst left in
- let right = apply_subst subst right in
+ let ty = Subst.apply_subst subst ty in
+ let left = Subst.apply_subst subst left in
+ let right = Subst.apply_subst subst right in
let fix_proof = function
- | NoProof -> NoProof
- | BasicProof (subst',term) -> BasicProof (subst@subst',term)
- | ProofBlock (subst', eq_URI, namety, bo, (pos, eq), p) ->
- (*
- let newsubst =
- List.map
- (fun (i, (context, term, ty)) ->
- let context = apply_subst_context subst context in
- let term = apply_subst subst term in
- let ty = apply_subst subst ty in
- (i, (context, term, ty))) subst' in *)
- ProofBlock (subst@subst', eq_URI, namety, bo, (pos, eq), p)
- | p -> assert false
- in
- let fix_new_proof = function
- | Exact p -> Exact (apply_subst subst p)
+ | Exact p -> Exact (Subst.apply_subst subst p)
| Step (s,(r,id1,(pos,id2),pred)) ->
- Step (s@subst,(r,id1,(pos,id2),(*apply_subst subst*) pred))
+ Step (Subst.concat s subst,(r,id1,(pos,id2), pred))
in
- let new_p = fix_new_proof p1 in
- let old_p = fix_proof p2 in
- let eq = mk_equality (w, (new_p,old_p), (ty, left, right, o), metasenv) in
+ let p = fix_proof p in
+ let eq = mk_equality (w, p, (ty, left, right, o), metasenv) in
(* debug prerr_endline (string_of_equality eq); *)
newmeta+1, eq
let o = !Utils.compare_terms t1 t2 in
let stat = (ty,t1,t2,o) in
let w = Utils.compute_equality_weight stat in
- let e = mk_equality (w, (Exact proof, BasicProof ([],proof)),stat,[]) in
+ let e = mk_equality (w, Exact proof, stat,[]) in
e
| _ ->
raise TermIsNotAnEquality
projects / helm.git / blobdiff