(* $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 = (rule * 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)
+let string_of_rule = function
+ | SuperpositionRight -> "SupR"
+ | SuperpositionLeft -> "SupL"
+ | Demodulation -> "Demod"
+;;
+
let string_of_equality ?env eq =
match env with
| None ->
- let w, _, (ty, left, right, o), _ , id = open_equality eq in
- Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s"
+ let w, _, (ty, left, right, o), m , id = open_equality eq in
+ Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s [%s]"
id w (CicPp.ppterm ty)
(CicPp.ppterm left)
(Utils.string_of_comparison o) (CicPp.ppterm right)
+ (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
| Some (_, context, _) ->
let names = Utils.names_of_context context in
- let w, _, (ty, left, right, o), _ , id = open_equality eq in
- Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s"
+ let w, _, (ty, left, right, o), m , id = open_equality eq in
+ Printf.sprintf "Id: %d, Weight: %d, {%s}: %s =(%s) %s [%s]"
id w (CicPp.pp ty names)
(CicPp.pp left names) (Utils.string_of_comparison o)
(CicPp.pp right names)
+ (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
;;
let compare (_,_,_,s1,_,_) (_,_,_,s2,_,_) =
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,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in
- p,m,l,r
+ 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 str_of_rule = function
- | SuperpositionRight -> "SupR"
- | SuperpositionLeft -> "SupL"
- | Demodulation -> "Demod"
- in
+let string_of_proof ?(names=[]) p gp =
let str_of_pos = function
| Utils.Left -> "left"
| Utils.Right -> "right"
in
- let fst4 (x,_,_,_) = x in
+ let fst3 (x,_,_) = x in
let rec aux margin name =
let prefix = String.make margin ' ' ^ name ^ ": " in function
| Exact t ->
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 (string_of_rule rule) (Subst.ppsubst ~names subst) eq1 eq2 (str_of_pos pos)
(CicPp.pp pred names)^
- aux (margin+1) (Printf.sprintf "%d" eq1) (fst4 (proof_of_id eq1)) ^
- aux (margin+1) (Printf.sprintf "%d" eq2) (fst4 (proof_of_id eq2))
+ aux (margin+1) (Printf.sprintf "%d" eq1) (fst3 (proof_of_id eq1)) ^
+ aux (margin+1) (Printf.sprintf "%d" eq2) (fst3 (proof_of_id eq2))
in
aux 0 "" p ^
String.concat "\n"
(List.map
- (fun (pos,i,s,t) ->
+ (fun (r,pos,i,s,t) ->
(Printf.sprintf
- "GOAL: %s %d %s %s\n"
- (str_of_pos pos) i (ppsubst ~names s) (CicPp.pp t names)) ^
- aux 1 (Printf.sprintf "%d " i) (fst4 (proof_of_id i)))
+ "GOAL: %s %s %d %s %s\n" (string_of_rule r)
+ (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 seen =
+ let (_,p,(_,_,_,_),_,ideq) = open_equality eq in
+ if List.mem ideq seen then
+ false,seen
+ else
+ if id = ideq then
+ true,seen
+ else
+ match p with
+ | Exact _ -> false,seen
+ | Step (_,(_,id1,(_,id2),_)) ->
+ let seen = ideq::seen in
+ let eq1 = Hashtbl.find id_to_eq id1 in
+ let eq2 = Hashtbl.find id_to_eq id2 in
+ let b1,seen = depend eq1 id seen in
+ if b1 then b1,seen else depend eq2 id seen
+;;
+
+let depend eq id = fst (depend eq id []);;
+
+let ppsubst = Subst.ppsubst ~names:[];;
(* returns an explicit named subst and a list of arguments for sym_eq_URI *)
-let build_ens_for_sym_eq sym_eq_URI termlist =
- let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph sym_eq_URI in
+let build_ens uri termlist =
+ let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
match obj with
| Cic.Constant (_, _, _, uris, _) ->
assert (List.length uris <= List.length 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_for_sym_eq (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
+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)
+;;
+
+let mk_trans uri ty t1 t2 t3 p12 p23 =
+ let ens, args = build_ens uri [ty;t1;t2;t3;p12;p23] in
+ Cic.Appl (Cic.Const (uri, ens) :: args)
+;;
+
+let mk_eq_ind uri ty what pred p1 other p2 =
+ Cic.Appl [Cic.Const (uri, []); ty; what; pred; p1; other; p2]
+;;
+
+let p_of_sym ens tl =
+ let args = List.map snd ens @ tl in
+ match args with
+ | [_;_;_;p] -> p
+ | _ -> assert false
+;;
+
+let open_trans ens tl =
+ let args = List.map snd ens @ tl in
+ match args with
+ | [ty;l;m;r;p1;p2] -> ty,l,m,r,p1,p2
+ | _ -> assert false
+;;
+
+let open_sym ens tl =
+ let args = List.map snd ens @ tl in
+ match args with
+ | [ty;l;r;p] -> ty,l,r,p
+ | _ -> 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 (((Cic.Const(uri_trans,ens))::tl) as args)
+ when LibraryObjects.is_trans_eq_URI uri_trans ->
+ let ty,l,m,r,p1,p2 = open_trans ens tl in
+ (match p1,p2 with
+ | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_],p2 ->
+ remove_refl p2
+ | p1,Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] ->
+ remove_refl p1
+ | _ -> Cic.Appl (List.map remove_refl args))
+ | Cic.Appl l -> Cic.Appl (List.map remove_refl l)
+ | Cic.LetIn (name,bo,rest) ->
+ Cic.LetIn (name,remove_refl bo,remove_refl rest)
+ | _ -> t
+ in
+ let rec canonical t =
+ match t with
+ | Cic.LetIn(name,bo,rest) -> Cic.LetIn(name,canonical bo,canonical rest)
+ | Cic.Appl (((Cic.Const(uri_sym,ens))::tl) as args)
+ when LibraryObjects.is_sym_eq_URI uri_sym ->
+ (match p_of_sym ens tl with
+ | Cic.Appl ((Cic.Const(uri,ens))::tl)
+ when LibraryObjects.is_sym_eq_URI uri ->
+ canonical (p_of_sym ens tl)
+ | Cic.Appl ((Cic.Const(uri_trans,ens))::tl)
+ when LibraryObjects.is_trans_eq_URI uri_trans ->
+ let ty,l,m,r,p1,p2 = open_trans ens tl in
+ mk_trans uri_trans ty r m l
+ (canonical (mk_sym uri_sym ty m r p2))
+ (canonical (mk_sym uri_sym ty l m p1))
+ | Cic.Appl (((Cic.Const(uri_ind,ens)) as he)::tl)
+ when LibraryObjects.is_eq_ind_URI uri_ind ||
+ LibraryObjects.is_eq_ind_r_URI uri_ind ->
+ let ty, what, pred, p1, other, p2 =
+ match tl with
+ | [ty;what;pred;p1;other;p2] -> ty, what, pred, p1, other, p2
+ | _ -> assert false
+ in
+ let pred,l,r =
+ match pred with
+ | Cic.Lambda (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;l;r])
+ when LibraryObjects.is_eq_URI uri ->
+ Cic.Lambda
+ (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;r;l]),l,r
+ | _ ->
+ prerr_endline (CicPp.ppterm pred);
+ assert false
+ in
+ let l = CicSubstitution.subst what l in
+ let r = CicSubstitution.subst what r in
+ Cic.Appl
+ [he;ty;what;pred;
+ canonical (mk_sym uri_sym ty l r p1);other;canonical p2]
+ | Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] as t
+ when LibraryObjects.is_eq_URI uri -> t
+ | _ -> Cic.Appl (List.map canonical args))
+ | Cic.Appl l -> Cic.Appl (List.map canonical l)
+ | _ -> t
+ in
+ 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.Implicit(Some `Hole)] ~with_what:[ctx2] ~where:ctx1
+;;
+
+let put_in_ctx ctx t =
+ ProofEngineReduction.replace_lifting
+ ~equality:(=) ~what:[Cic.Implicit (Some `Hole)] ~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 =
+ let hole = Cic.Implicit (Some `Hole) in
+ (* 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 hole. Cic.Implicit(Some `Hole) is the empty context
+ *)
+ let rec aux uri ty left right ctx_d = function
+ | Cic.Appl ((Cic.Const(uri_sym,ens))::tl)
+ when LibraryObjects.is_sym_eq_URI uri_sym ->
+ let ty,l,r,p = open_sym ens tl in
+ mk_sym uri_sym ty l r (aux uri ty l r ctx_d p)
+ | Cic.LetIn (name,body,rest) ->
+ (* we should go in body *)
+ Cic.LetIn (name,body,aux uri ty left right ctx_d rest)
+ | 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 hole 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 r = CicSubstitution.lift 1 (put_in_ctx ctx_d left) in
+ let l =
+ let ctx_d = CicSubstitution.lift 1 ctx_d in
+ put_in_ctx ctx_d (Cic.Rel 1)
+ in
+ let lty = CicSubstitution.lift 1 ty in
+ Cic.Lambda (Cic.Name "foo",ty,(mk_eq uri lty l r))
in
- ProofEngineReduction.replace
- ~equality:eq ~what:[meta_index] ~with_what:[proof] ~where:term
+ 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
+ aux uri ty left right hole t
+;;
+
+let contextualize_rewrites t ty =
+ let eq,ty,l,r = open_eq ty in
+ contextualize eq ty l r t
+;;
+
+let add_subst subst =
+ function
+ | Exact t -> Exact (Subst.apply_subst subst t)
+ | Step (s,(rule, id1, (pos,id2), pred)) ->
+ Step (Subst.concat subst s,(rule, id1, (pos,id2), pred))
+;;
+
+let build_proof_step ?(sym=false) lift subst p1 p2 pos l r pred =
+ let p1 = Subst.apply_subst_lift lift subst p1 in
+ let p2 = Subst.apply_subst_lift lift subst p2 in
+ let l = CicSubstitution.lift lift l in
+ let l = Subst.apply_subst_lift lift subst l in
+ let r = CicSubstitution.lift lift r in
+ let r = Subst.apply_subst_lift lift subst r in
+ let pred = CicSubstitution.lift lift pred in
+ let pred = Subst.apply_subst_lift lift subst pred in
+ let ty,body =
+ match pred with
+ | Cic.Lambda (_,ty,body) -> ty,body
+ | _ -> assert false
+ in
+ let what, other =
+ if pos = Utils.Left then l,r else r,l
+ in
+ let p =
+ match pos with
+ | Utils.Left ->
+ mk_eq_ind (Utils.eq_ind_URI ()) ty what pred p1 other p2
+ | Utils.Right ->
+ mk_eq_ind (Utils.eq_ind_r_URI ()) ty what pred p1 other p2
+ in
+ if sym then
+ let uri,pl,pr =
+ let eq,_,pl,pr = open_eq body in
+ LibraryObjects.sym_eq_URI ~eq, pl, pr
+ in
+ let l = CicSubstitution.subst other pl in
+ let r = CicSubstitution.subst other pr in
+ mk_sym uri ty l r p
+ else
+ p
+;;
+
+let parametrize_proof p l r ty =
+ let parameters = CicUtil.metas_of_term p
+@ CicUtil.metas_of_term l
+@ CicUtil.metas_of_term r
+in (* ?if they are under a lambda? *)
+ let parameters =
+ HExtlib.list_uniq (List.sort Pervasives.compare parameters)
+ in
+ let what = List.map (fun (i,l) -> Cic.Meta (i,l)) parameters in
+ let with_what, lift_no =
+ List.fold_right (fun _ (acc,n) -> ((Cic.Rel n)::acc),n+1) what ([],1)
+ in
+ let p = CicSubstitution.lift (lift_no-1) p in
+ let p =
+ ProofEngineReduction.replace_lifting
+ ~equality:(fun t1 t2 ->
+ match t1,t2 with Cic.Meta (i,_),Cic.Meta(j,_) -> i=j | _ -> false)
+ ~what ~with_what ~where:p
+ in
+ let ty_of_m _ = ty (*function
+ | Cic.Meta (i,_) -> List.assoc i menv
+ | _ -> assert false *)
+ in
+ let args, proof,_ =
+ List.fold_left
+ (fun (instance,p,n) m ->
+ (instance@[m],
+ Cic.Lambda
+ (Cic.Name ("x"^string_of_int n),
+ CicSubstitution.lift (lift_no - n - 1) (ty_of_m m),
+ p),
+ n+1))
+ ([Cic.Rel 1],p,1)
+ what
+ in
+ let instance = match args with | [x] -> x | _ -> Cic.Appl args in
+ proof, instance
+;;
- and do_build_goal_proof proofbit proof =
+let wfo goalproof proof id =
+ let rec aux acc id =
+ let p,_,_ = proof_of_id id in
+ match p with
+ | 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
+ let acc =
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 build_proof_term_new proof =
- let rec aux extra = function
- | Exact term -> term
- | Step (subst,(_, id1, (pos,id2), pred)) ->
- let p,m1,_,_ = proof_of_id id1 in
- let p1 = aux [] p in
- let p,m3,l,r = proof_of_id id2 in
- let p2 = aux [] p in
- 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 = (* Cic.Implicit None *)
+ | Exact _ -> [id]
+ | Step (_,(_,id1, (_,id2), _)) -> aux (aux [id] id1) id2
+ in
+ List.fold_left (fun acc (_,_,id,_,_) -> aux acc id) acc goalproof
+;;
+
+let string_of_id names id =
+ if id = 0 then "" else
+ try
+ let (_,p,(_,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in
+ match p with
+ | Exact t ->
+ Printf.sprintf "%d = %s: %s = %s [%s]" id
+ (CicPp.pp t names) (CicPp.pp l names) (CicPp.pp r names)
+ (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
+ | Step (_,(step,id1, (_,id2), _) ) ->
+ Printf.sprintf "%6d: %s %6d %6d %s = %s [%s]" id
+ (string_of_rule step)
+ id1 id2 (CicPp.pp l names) (CicPp.pp r names)
+ (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
+ with
+ Not_found -> assert false
+
+let pp_proof names goalproof proof subst id initial_goal =
+ String.concat "\n" (List.map (string_of_id names) (wfo goalproof proof id)) ^
+ "\ngoal:\n " ^
+ (String.concat "\n "
+ (fst (List.fold_right
+ (fun (r,pos,i,s,pred) (acc,g) ->
+ let _,_,left,right = open_eq g in
+ let ty =
+ match pos with
+ | Utils.Left -> CicReduction.head_beta_reduce (Cic.Appl[pred;right])
+ | Utils.Right -> CicReduction.head_beta_reduce (Cic.Appl[pred;left])
+ in
+ let ty = Subst.apply_subst s ty in
+ ("("^ string_of_rule r ^ " " ^ string_of_int i^") -> "
+ ^ CicPp.pp ty names) :: acc,ty) goalproof ([],initial_goal)))) ^
+ "\nand then subsumed by " ^ string_of_int id ^ " when " ^ Subst.ppsubst subst
+;;
+
+module OT =
+ struct
+ type t = int
+ let compare = Pervasives.compare
+ end
+
+module M = Map.Make(OT)
+
+let rec find_deps m i =
+ if M.mem i m then m
+ else
+ let p,_,_ = proof_of_id i in
+ match p with
+ | Exact _ -> M.add i [] m
+ | Step (_,(_,id1,(_,id2),_)) ->
+ let m = find_deps m id1 in
+ let m = find_deps m id2 in
+ M.add i (M.find id1 m @ M.find id2 m @ [id1;id2]) m
+;;
+
+let topological_sort l =
+ (* build the partial order relation *)
+ let m =
+ List.fold_left (fun m i -> find_deps m i)
+ M.empty l
+ in
+ let m = M.map (fun x -> Some x) m in
+ (* utils *)
+ let keys m = M.fold (fun i _ acc -> i::acc) m [] in
+ let split l m = List.filter (fun i -> M.find i m = Some []) l in
+ let purge l m =
+ M.mapi
+ (fun k v -> if List.mem k l then None else
+ match v with
+ | None -> None
+ | Some ll -> Some (List.filter (fun i -> not (List.mem i l)) ll))
+ m
+ in
+ let rec aux m =
+ let keys = keys m in
+ let ok = split keys m in
+ let m = purge ok m in
+ ok @ (if ok = [] then [] else aux m)
+ in
+ aux m
+;;
+
+
+(* returns the list of ids that should be factorized *)
+let get_duplicate_step_in_wfo l p =
+ let ol = List.rev l in
+ let h = Hashtbl.create 13 in
+ (* NOTE: here the n parameter is an approximation of the dependency
+ between equations. To do things seriously we should maintain a
+ dependency graph. This approximation is not perfect. *)
+ let add i =
+ let p,_,_ = proof_of_id i in
+ match p with
+ | Exact _ -> true
+ | _ ->
+ try
+ let no = Hashtbl.find h i in
+ Hashtbl.replace h i (no+1);
+ false
+ with Not_found -> Hashtbl.add h i 1;true
+ in
+ let rec aux = function
+ | Exact _ -> ()
+ | Step (_,(_,i1,(_,i2),_)) ->
+ let go_on_1 = add i1 in
+ let go_on_2 = add i2 in
+ if go_on_1 then aux (let p,_,_ = proof_of_id i1 in p);
+ if go_on_2 then aux (let p,_,_ = proof_of_id i2 in p)
+ in
+ aux p;
+ List.iter
+ (fun (_,_,id,_,_) -> aux (let p,_,_ = proof_of_id id in p))
+ ol;
+ (* now h is complete *)
+ let proofs = Hashtbl.fold (fun k count acc-> (k,count)::acc) h [] in
+ let proofs = List.filter (fun (_,c) -> c > 1) proofs in
+ topological_sort (List.map (fun (i,_) -> i) proofs)
+;;
+
+let build_proof_term h lift proof =
+ let proof_of_id aux id =
+ let p,l,r = proof_of_id id in
+ try List.assoc id h,l,r with Not_found -> aux p, l, r
+ in
+ let rec aux = function
+ | Exact term -> CicSubstitution.lift lift term
+ | Step (subst,(rule, id1, (pos,id2), pred)) ->
+ let p1,_,_ = proof_of_id aux id1 in
+ let p2,l,r = proof_of_id aux id2 in
+ let varname =
+ match rule with
+ | SuperpositionRight -> Cic.Name ("SupR" ^ Utils.string_of_pos pos)
+ | Demodulation -> Cic.Name ("DemEq"^ Utils.string_of_pos pos)
+ | _ -> assert false
+ in
+ let pred =
match pred with
- | Cic.Lambda (_,ty,_) -> ty
+ | Cic.Lambda (_,a,b) -> Cic.Lambda (varname,a,b)
| _ -> assert false
in
- let what, other = (* Cic.Implicit None, Cic.Implicit None *)
- if pos = Utils.Left then l,r else r,l
+ let p = build_proof_step lift subst p1 p2 pos l r pred in
+(* let cond = (not (List.mem 302 (Utils.metas_of_term p)) || id1 = 8 || id1 = 132) in
+ if not cond then
+ prerr_endline ("ERROR " ^ string_of_int id1 ^ " " ^ string_of_int id2);
+ assert cond;*)
+ p
+ in
+ aux proof
+;;
+
+let build_goal_proof l initial ty se =
+ let se = List.map (fun i -> Cic.Meta (i,[])) se in
+ let lets = get_duplicate_step_in_wfo l initial in
+ let letsno = List.length lets in
+ let _,mty,_,_ = open_eq ty in
+ let lift_list l = List.map (fun (i,t) -> i,CicSubstitution.lift 1 t) l
+ in
+ let lets,_,h =
+ List.fold_left
+ (fun (acc,n,h) id ->
+ let p,l,r = proof_of_id id in
+ let cic = build_proof_term h n p in
+ let real_cic,instance =
+ parametrize_proof cic l r (CicSubstitution.lift n mty)
+ in
+ let h = (id, instance)::lift_list h in
+ acc@[id,real_cic],n+1,h)
+ ([],0,[]) lets
+ in
+ let proof,se =
+ let rec aux se current_proof = function
+ | [] -> current_proof,se
+ | (rule,pos,id,subst,pred)::tl ->
+ let p,l,r = proof_of_id id in
+ let p = build_proof_term h letsno p in
+ let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
+ let varname =
+ match rule with
+ | SuperpositionLeft -> Cic.Name ("SupL" ^ Utils.string_of_pos pos)
+ | Demodulation -> Cic.Name ("DemG"^ Utils.string_of_pos pos)
+ | _ -> assert false
in
- let eq_URI =
- match pos with
- | Utils.Left -> Utils.eq_ind_URI ()
- | Utils.Right -> Utils.eq_ind_r_URI ()
- in
- (Cic.Appl [
- Cic.Const (eq_URI, []);
- ty; what; pred; p1; other; p2])
- in
- aux [] proof
-
-let build_goal_proof l refl=
- let proof, subst =
- List.fold_left
- (fun (current_proof,current_subst) (pos,id,subst,pred) ->
- let p,m,l,r = proof_of_id id in
- let p = build_proof_term_new p in
- let p = apply_subst subst p in
- let l = apply_subst subst l in
- let r = apply_subst subst r in
- let pred = apply_subst subst pred in
- let ty = (* Cic.Implicit None *)
- match pred with
- | Cic.Lambda (_,ty,_) -> ty
- | _ -> assert false
- in
- let what, other = (* Cic.Implicit None, Cic.Implicit None *)
- if pos = Utils.Right then l,r else r,l
- in
- let eq_URI =
- match pos with
- | Utils.Left -> Utils.eq_ind_r_URI ()
- | Utils.Right -> Utils.eq_ind_URI ()
- in
- ((Cic.Appl [Cic.Const (eq_URI, []);
- ty; what; pred; current_proof; other; p]), subst @ current_subst))
- (refl,[]) l
+ let pred =
+ match pred with
+ | Cic.Lambda (_,a,b) -> Cic.Lambda (varname,a,b)
+ | _ -> assert false
+ in
+ let proof =
+ build_proof_step letsno subst current_proof p pos l r pred
+ in
+ let proof,se = aux se proof tl in
+ Subst.apply_subst_lift letsno subst proof,
+ List.map (fun x -> Subst.apply_subst_lift letsno subst x) se
+ in
+ aux se (build_proof_term h letsno initial) l
+ in
+ let n,proof =
+ let initial = proof in
+ List.fold_right
+ (fun (id,cic) (n,p) ->
+ n-1,
+ Cic.LetIn (
+ Cic.Name ("H"^string_of_int id),
+ cic, p))
+ lets (letsno-1,initial)
in
- proof
+ (proof,se)
+ (* canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)),
+ se *)
;;
let refl_proof ty term =
Cic.Appl
[Cic.MutConstruct
- (LibraryObjects.eq_URI (), 0, 1, []);
+ (Utils.eq_URI (), 0, 1, []);
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 [] 0 p in
+ Utils.metas_of_term p
+;;
-let relocate newmeta menv =
- let subst, metasenv, newmeta =
+let relocate newmeta menv to_be_relocated =
+ let subst, newmetasenv, newmeta =
List.fold_right
- (fun (i, context, ty) (subst, menv, maxmeta) ->
- let irl = [] (*
- CicMkImplicit.identity_relocation_list_for_metavariable context *)
- in
- let newsubst = buildsubst i context (Cic.Meta(maxmeta,irl)) ty subst in
- let newmeta = maxmeta, context, ty in
- newsubst, newmeta::menv, maxmeta+1)
- menv ([], [], newmeta+1)
+ (fun i (subst, metasenv, maxmeta) ->
+ let _,context,ty = CicUtil.lookup_meta i menv in
+ let irl = [] in
+ let newmeta = Cic.Meta(maxmeta,irl) in
+ let newsubst = Subst.buildsubst i context newmeta ty subst in
+ newsubst, (maxmeta,context,ty)::metasenv, maxmeta+1)
+ to_be_relocated (Subst.empty_subst, [], newmeta+1)
in
- let metasenv = apply_subst_metasenv subst metasenv in
- let subst = flatten_subst subst in
- subst, metasenv, newmeta
+ let menv = Subst.apply_subst_metasenv subst menv @ newmetasenv in
+ subst, menv, newmeta
let fix_metas newmeta eq =
- let w, (p1,p2), (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 w, p, (ty, left, right, o), menv,_ = open_equality eq in
+ let to_be_relocated =
+(* List.map (fun i ,_,_ -> i) menv *)
+ HExtlib.list_uniq
+ (List.sort Pervasives.compare
+ (Utils.metas_of_term left @ Utils.metas_of_term right))
+ in
+ let subst, metasenv, newmeta = relocate newmeta menv to_be_relocated 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
- (* debug prerr_endline (string_of_equality eq); *)
- newmeta+1, eq
+ let p = fix_proof p in
+ let eq' = mk_equality (w, p, (ty, left, right, o), metasenv) in
+ newmeta+1, eq'
exception NotMetaConvertible;;
exception TermIsNotAnEquality;;
let term_is_equality term =
- let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
+ let iseq uri = UriManager.eq uri (Utils.eq_URI ()) in
match term with
| Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
| _ -> false
;;
let equality_of_term proof term =
- let eq_uri = LibraryObjects.eq_URI () in
+ let eq_uri = Utils.eq_URI () in
let iseq uri = UriManager.eq uri eq_uri in
match term with
| Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
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
let argsno = List.length menv in
let t =
CicSubstitution.lift argsno
- (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
+ (Cic.Appl [Cic.MutInd (Utils.eq_URI (), 0, []); ty; left; right])
in
snd (
List.fold_right
menv (argsno, t))
;;
+let symmetric eq_ty l id uri m =
+ let eq = Cic.MutInd(uri,0,[]) in
+ let pred =
+ Cic.Lambda (Cic.Name "Sym",eq_ty,
+ Cic.Appl [CicSubstitution.lift 1 eq ;
+ CicSubstitution.lift 1 eq_ty;
+ Cic.Rel 1;CicSubstitution.lift 1 l])
+ in
+ let prefl =
+ Exact (Cic.Appl
+ [Cic.MutConstruct(uri,0,1,[]);eq_ty;l])
+ in
+ let id1 =
+ let eq = mk_equality (0,prefl,(eq_ty,l,l,Utils.Eq),m) in
+ let (_,_,_,_,id) = open_equality eq in
+ id
+ in
+ Step(Subst.empty_subst,
+ (Demodulation,id1,(Utils.Left,id),pred))
+;;
+
projects / helm.git / blobdiff