+
+
+let rec demodulation_goal newmeta env table goal =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ let module M = CicMetaSubst in
+ let module HL = HelmLibraryObjects in
+ let metasenv, context, ugraph = env in
+ let maxmeta = ref newmeta in
+ let proof, metas, term = goal in
+ let metasenv' = metasenv @ metas in
+
+ let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
+ let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
+ let what, other = if pos = Utils.Left then what, other else other, what in
+ let ty =
+ try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
+ with CicUtil.Meta_not_found _ -> ty
+ in
+ let newterm, newproof =
+ let bo = (* M. *)apply_subst subst (S.subst other t) in
+ let bo' = apply_subst subst t in
+ let name = C.Name ("x_DemodGoal_" ^ (string_of_int !demod_counter)) in
+ incr demod_counter;
+ let metaproof =
+ incr maxmeta;
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context in
+ Printf.printf "\nADDING META: %d\n" !maxmeta;
+ print_newline ();
+ C.Meta (!maxmeta, irl)
+ in
+ let eq_found =
+ let proof' =
+ let ens =
+ if pos = Utils.Left then build_ens_for_sym_eq ty what other
+ else build_ens_for_sym_eq ty other what
+ in
+ Inference.ProofSymBlock (ens, proof')
+ in
+ let what, other =
+ if pos = Utils.Left then what, other else other, what
+ in
+ pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args')
+ in
+ let goal_proof =
+ let pb =
+ Inference.ProofBlock (subst, eq_URI, (name, ty), bo',
+ eq_found, Inference.BasicProof metaproof)
+ in
+ let rec repl = function
+ | Inference.NoProof ->
+ debug_print (lazy "replacing a NoProof");
+ pb
+ | Inference.BasicProof _ ->
+ debug_print (lazy "replacing a BasicProof");
+ pb
+ | Inference.ProofGoalBlock (_, parent_proof) ->
+ debug_print (lazy "replacing another ProofGoalBlock");
+ Inference.ProofGoalBlock (pb, parent_proof)
+ | (Inference.SubProof (term, meta_index, p) as subproof) ->
+ debug_print
+ (lazy
+ (Printf.sprintf "replacing %s"
+ (Inference.string_of_proof subproof)));
+ Inference.SubProof (term, meta_index, repl p)
+ | _ -> assert false
+ in repl proof
+ in
+ bo, Inference.ProofGoalBlock (Inference.NoProof, goal_proof)
+ in
+ let m = Inference.metas_of_term newterm in
+ let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
+ !maxmeta, (newproof, newmetasenv, newterm)
+ in
+ let res = demodulation_aux metasenv' context ugraph table 0 term in
+ match res with
+ | Some t ->
+ let newmeta, newgoal = build_newgoal t in
+ let _, _, newg = newgoal in
+ if Inference.meta_convertibility term newg then
+ newmeta, newgoal
+ else
+ demodulation_goal newmeta env table newgoal
+ | None ->
+ newmeta, goal
+;;
+
+
+let rec demodulation_theorem newmeta env table theorem =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ let module M = CicMetaSubst in
+ let module HL = HelmLibraryObjects in
+ let metasenv, context, ugraph = env in
+ let maxmeta = ref newmeta in
+ let proof, metas, term = theorem in
+ let term, termty, metas = theorem in
+ let metasenv' = metasenv @ metas in
+
+ let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
+ let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in
+ let what, other = if pos = Utils.Left then what, other else other, what in
+ let newterm, newty =
+ let bo = apply_subst subst (S.subst other t) in
+ let bo' = apply_subst subst t in
+ let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in
+ incr demod_counter;
+ let newproof =
+ Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
+ Inference.BasicProof term)
+ in
+ (Inference.build_proof_term newproof, bo)
+ in
+ let m = Inference.metas_of_term newterm in
+ let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
+ !maxmeta, (newterm, newty, newmetasenv)
+ in
+ let res = demodulation_aux metasenv' context ugraph table 0 termty in
+ match res with
+ | Some t ->
+ let newmeta, newthm = build_newtheorem t in
+ let newt, newty, _ = newthm in
+ if Inference.meta_convertibility termty newty then
+ newmeta, newthm
+ else
+ demodulation_theorem newmeta env table newthm
+ | None ->
+ newmeta, theorem
+;;