+type equality =
+ int * (* weight *)
+ proof *
+ (Cic.term * (* type *)
+ Cic.term * (* left side *)
+ Cic.term * (* right side *)
+ Utils.comparison) * (* ordering *)
+ Cic.metasenv * (* environment for metas *)
+ Cic.term list (* arguments *)
+
+and proof =
+ | NoProof
+ | BasicProof of Cic.term
+ | ProofBlock of
+ Cic.substitution * UriManager.uri *
+ (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * proof
+ | ProofGoalBlock of proof * proof
+ | ProofSymBlock of Cic.term list * proof
+ | SubProof of Cic.term * int * proof
+;;
+
+
+let string_of_equality ?env =
+ match env with
+ | None -> (
+ function
+ | w, _, (ty, left, right, o), _, _ ->
+ Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.ppterm ty)
+ (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right)
+ )
+ | Some (_, context, _) -> (
+ let names = names_of_context context in
+ function
+ | w, _, (ty, left, right, o), _, _ ->
+ Printf.sprintf "Weight: %d, {%s}: %s =(%s) %s" w (CicPp.pp ty names)
+ (CicPp.pp left names) (string_of_comparison o)
+ (CicPp.pp right names)
+ )
+;;
+
+
+let rec string_of_proof = function
+ | NoProof -> "NoProof"
+ | BasicProof t -> "BasicProof " ^ (CicPp.ppterm t)
+ | SubProof (t, i, p) ->
+ Printf.sprintf "SubProof(%s, %s, %s)"
+ (CicPp.ppterm t) (string_of_int i) (string_of_proof p)
+ | ProofSymBlock _ -> "ProofSymBlock"
+ | ProofBlock _ -> "ProofBlock"
+ | ProofGoalBlock (p1, p2) ->
+ Printf.sprintf "ProofGoalBlock(%s, %s)"
+ (string_of_proof p1) (string_of_proof p2)
+;;
+
+
+(* 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
+ match obj with
+ | Cic.Constant (_, _, _, uris, _) ->
+ assert (List.length uris <= List.length termlist);
+ let rec aux = function
+ | [], tl -> [], tl
+ | (uri::uris), (term::tl) ->
+ let ens, args = aux (uris, tl) in
+ (uri, term)::ens, args
+ | _, _ -> assert false
+ in
+ aux (uris, termlist)
+ | _ -> assert false
+;;
+
+
+let build_proof_term proof =
+ let rec do_build_proof proof =
+ match proof with
+ | NoProof ->
+ Printf.fprintf stderr "WARNING: no proof!\n";
+ Cic.Implicit None
+ | BasicProof term -> 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' =
+ let _, proof', _, _, _ = eq in
+ do_build_proof proof'
+ in
+ let eqproof = do_build_proof eqproof in
+ let _, _, (ty, what, other, _), menv', args' = eq in
+ let what, other =
+ if pos = Utils.Left then what, other else other, what
+ in
+ CicMetaSubst.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 rec metas_of_term = function
+ | Cic.Meta (i, c) -> [i]
+ | Cic.Var (_, ens)
+ | Cic.Const (_, ens)
+ | Cic.MutInd (_, _, ens)
+ | Cic.MutConstruct (_, _, _, ens) ->
+ List.flatten (List.map (fun (u, t) -> metas_of_term t) ens)
+ | Cic.Cast (s, t)
+ | Cic.Prod (_, s, t)
+ | Cic.Lambda (_, s, t)
+ | Cic.LetIn (_, s, t) -> (metas_of_term s) @ (metas_of_term t)
+ | Cic.Appl l -> List.flatten (List.map metas_of_term l)
+ | Cic.MutCase (uri, i, s, t, l) ->
+ (metas_of_term s) @ (metas_of_term t) @
+ (List.flatten (List.map metas_of_term l))
+ | Cic.Fix (i, il) ->
+ List.flatten
+ (List.map (fun (s, i, t1, t2) ->
+ (metas_of_term t1) @ (metas_of_term t2)) il)
+ | Cic.CoFix (i, il) ->
+ List.flatten
+ (List.map (fun (s, t1, t2) ->
+ (metas_of_term t1) @ (metas_of_term t2)) il)
+ | _ -> []
+;;
+
+