let after = ProofEngineTypes.goals_of_proof proof in
let opened_goals, closed_goals = Tacticals.goals_diff ~before ~after ~opened in
let proof, opened_goals =
- let uri, metasenv_after_tactic, t, ty, attrs = proof in
+ let uri, metasenv_after_tactic, _subst, t, ty, attrs = proof in
let reordered_metasenv, opened_goals =
reorder_metasenv
starting_metasenv
metasenv_after_refinement metasenv_after_tactic
opened goal always_opens_a_goal
in
- let proof' = uri, reordered_metasenv, t, ty, attrs in
+ let proof' = uri, reordered_metasenv, _subst, t, ty, attrs in
proof', opened_goals
in
let incomplete_proof =
let after = ProofEngineTypes.goals_of_proof proof in
let opened_goals, closed_goals = Tacticals.goals_diff ~before ~after ~opened in
let proof, opened_goals =
- let uri, metasenv_after_tactic, t, ty, attrs = proof in
+ let uri, metasenv_after_tactic, _subst, t, ty, attrs = proof in
let reordered_metasenv, opened_goals =
reorder_metasenv
starting_metasenv
metasenv_after_refinement metasenv_after_tactic
opened goal always_opens_a_goal
in
- let proof' = uri, reordered_metasenv, t, ty, attrs in
+ let proof' = uri, reordered_metasenv, _subst, t, ty, attrs in
proof', opened_goals
in
let incomplete_proof =
*)
status,[]
| GrafiteAst.Print (_,"proofterm") ->
- let _,_,p,_, _ = GrafiteTypes.get_current_proof status in
+ let _,_,_,p,_, _ = GrafiteTypes.get_current_proof status in
print_endline (AutoTactic.pp_proofterm p);
status,[]
| GrafiteAst.Print (_,_) -> status,[]
| GrafiteAst.Qed loc ->
- let uri, metasenv, bo, ty, attrs =
+ let uri, metasenv, _subst, bo, ty, attrs =
match status.GrafiteTypes.proof_status with
- | GrafiteTypes.Proof (Some uri, metasenv, body, ty, attrs) ->
- uri, metasenv, body, ty, attrs
- | GrafiteTypes.Proof (None, metasenv, body, ty, attrs) ->
+ | GrafiteTypes.Proof (Some uri, metasenv, subst, body, ty, attrs) ->
+ uri, metasenv, subst, body, ty, attrs
+ | GrafiteTypes.Proof (None, metasenv, subst, body, ty, attrs) ->
raise (GrafiteTypes.Command_error
("Someone allows to start a theorem without giving the "^
"name/uri. This should be fixed!"))
("Theorem already proved: " ^ UriManager.string_of_uri x ^
"\nPlease use a variant."));
end;
- let initial_proof = (Some uri, metasenv', bo, ty, attrs) in
+ let _subst = [] in
+ let initial_proof = (Some uri, metasenv', _subst, bo, ty, attrs) in
let initial_stack = Continuationals.Stack.of_metasenv metasenv' in
{ status with GrafiteTypes.proof_status =
GrafiteTypes.Incomplete_proof
let get_proof_metasenv status =
match status.proof_status with
| No_proof -> []
- | Proof (_, metasenv, _, _, _)
- | Incomplete_proof { proof = (_, metasenv, _, _, _) }
+ | Proof (_, metasenv, _, _, _, _)
+ | Incomplete_proof { proof = (_, metasenv, _, _, _, _) }
| Intermediate metasenv ->
metasenv
let proof_status =
match status.proof_status with
| No_proof -> Intermediate metasenv
- | Incomplete_proof ({ proof = (uri, _, proof, ty, attrs) } as incomplete_proof) ->
+ | Incomplete_proof ({ proof = (uri, _, subst, proof, ty, attrs) } as incomplete_proof) ->
Incomplete_proof
- { incomplete_proof with proof = (uri, metasenv, proof, ty, attrs) }
+ { incomplete_proof with proof = (uri, metasenv, subst, proof, ty, attrs) }
| Intermediate _ -> Intermediate metasenv
- | Proof (_, metasenv', _, _, _) ->
+ | Proof (_, metasenv', _, _, _, _) ->
assert (metasenv = metasenv');
status.proof_status
in
let get_proof_context status goal =
match status.proof_status with
- | Incomplete_proof { proof = (_, metasenv, _, _, _) } ->
+ | Incomplete_proof { proof = (_, metasenv, _, _, _, _) } ->
let (_, context, _) = CicUtil.lookup_meta goal metasenv in
context
| _ -> []
let get_proof_conclusion status goal =
match status.proof_status with
- | Incomplete_proof { proof = (_, metasenv, _, _, _) } ->
+ | Incomplete_proof { proof = (_, metasenv, _, _, _, _) } ->
let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in
conclusion
| _ -> raise (Statement_error "no ongoing proof")
let init_cache_and_tables dbd use_library paramod universe (proof, goal) =
(* the local cache in initially empty *)
let cache = AutoCache.cache_empty in
- let _, metasenv, _, _, _ = proof in
+ let _, metasenv, _subst,_, _, _ = proof in
let signature = MetadataQuery.signature_of metasenv goal in
let newmeta = CicMkImplicit.new_meta metasenv [] in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let close_more tables maxmeta context status auto universe cache =
let (active,passive,bag) = tables in
let proof, goalno = status in
- let _, metasenv,_,_, _ = proof in
+ let _, metasenv,_subst,_,_, _ = proof in
let signature = MetadataQuery.signature_of metasenv goalno in
let equations = retrieve_equations signature universe cache context in
let eqs_and_types =
let module C = Cic in
let module S = CicSubstitution in
let module T = CicTypeChecker in
- let _,metasenv,_,_, _ = proof in
+ let _,metasenv,_subst,_,_, _ = proof in
let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
(* if use_auto is true, we try to close the hypothesis of equational
statements using auto; a naif, and probably wrong approach *)
match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments)
in
let proof',oldmetasenv =
- let (puri,metasenv,pbo,pty, attrs) = proof in
- (puri,newmetasenv,pbo,pty, attrs),metasenv
+ let (puri,metasenv,_subst,pbo,pty, attrs) = proof in
+ (puri,newmetasenv,_subst,pbo,pty, attrs),metasenv
in
let goal_for_paramod =
match LibraryObjects.eq_URI () with
in
let newmeta = CicMkImplicit.new_meta newmetasenv (*subst*) [] in
let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in
- let proof'' = let uri,_,p,ty, attrs = proof' in uri,metasenv_for_paramod,p,ty, attrs in
+ let proof'' =
+ let uri,_,_subst,p,ty, attrs = proof' in
+ uri,metasenv_for_paramod,_subst,p,ty, attrs
+ in
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
let proof''',goals =
ProofEngineTypes.apply_tactic
| Some (_,proof''''',_), active,passive,_ ->
subst,proof''''',
ProofEngineHelpers.compare_metasenvs ~oldmetasenv
- ~newmetasenv:(let _,m,_,_, _ = proof''''' in m), active, passive
+ ~newmetasenv:(let _,m,_subst,_,_, _ = proof''''' in m), active, passive
;;
let rec count_prods context ty =
let module T = CicTypeChecker in
let module R = CicReduction in
let module C = Cic in
- let (_,metasenv,_,_, _) = proof in
+ let (_,metasenv,_subst,_,_, _) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let newmeta = CicMkImplicit.new_meta metasenv subst in
let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
subst, metasenv
;;
let mk_fake_proof metasenv (goalno,_,_) goalty context =
- None,metasenv,Cic.Meta(goalno,mk_irl context),goalty, []
+ None,metasenv,[],Cic.Meta(goalno,mk_irl context),goalty, []
;;
let equational_case
tables maxm cache depth fake_proof goalno goalty subst context
with
| None, active, passive, maxmeta ->
[], (active,passive,bag), cache, maxmeta, flags
- | Some(subst',(_,metasenv,proof,_, _),open_goals),active,
+ | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
passive,maxmeta ->
assert_subst_are_disjoint subst subst';
let subst = subst@subst' in
assert (maxmeta >= maxm);
let res' =
List.map
- (fun subst',(_,metasenv,proof,_, _),open_goals ->
+ (fun subst',(_,metasenv,_subst,proof,_, _),open_goals ->
assert_subst_are_disjoint subst subst';
let subst = subst@subst' in
let open_goals =
=
let ppterm = ppterm context in
try
- let subst', ((_,metasenv,_,_, _), open_goals), maxmeta =
+ let subst', ((_,metasenv,_subst,_,_, _), open_goals), maxmeta =
PrimitiveTactics.apply_with_subst
~maxmeta:maxm ~term:cand ~subst (fake_proof,goalno)
in
let superposition_tac ~target ~table ~subterms_only ~demod_table status =
Saturation.reset_refs();
let proof,goalno = status in
- let curi,metasenv,pbo,pty, attrs = proof in
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
let eq_uri,tty = eq_and_ty_of_goal ty in
let env = (metasenv, context, CicUniv.empty_ugraph) in
~target ~table ~subterms_only ~demod_table (proof,goal)
| false ->
(* this is the real auto *)
- let _,metasenv,_,_, _ = proof in
+ let _,metasenv,_subst,_,_, _ = proof in
let _,context,goalty = CicUtil.lookup_meta goal metasenv in
let flags = flags_of_params params () in
(* just for testing *)
auto_all_solutions universe cache
else tables,cache,newmeta in
let initial_time = Unix.gettimeofday() in
- let (_,oldmetasenv,_,_, _) = proof in
+ let (_,oldmetasenv,_subst,_,_, _) = proof in
hint := None;
let elem =
metasenv,[],1,[D (goal,flags.maxdepth,P)],[]
*)
let proof,metasenv =
ProofEngineHelpers.subst_meta_and_metasenv_in_proof
- proof goal (CicMetaSubst.apply_subst subst) metasenv
+ proof goal subst metasenv
in
let opened =
ProofEngineHelpers.compare_metasenvs ~oldmetasenv
(* DEMODULATE *)
let demodulate_tac ~dbd ~universe (proof,goal)=
- let curi,metasenv,pbo,pty, attrs = proof in
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
let initgoal = [], [], ty in
in
let extended_metasenv = (maxm,context,newty)::metasenv in
let extended_status =
- (curi,extended_metasenv,pbo,pty, attrs),goal in
+ (curi,extended_metasenv,_subst,pbo,pty, attrs),goal in
let (status,newgoals) =
ProofEngineTypes.apply_tactic
(PrimitiveTactics.apply_tac ~term:proofterm)
let module S = CicSubstitution in
let module PET = ProofEngineTypes in
let module PT = PrimitiveTactics in
- let _,metasenv,_,_, _ = proof in
+ let _,metasenv,_subst,_,_, _ = proof in
let _,context,ty = CicUtil.lookup_meta goal metasenv in
let rec find n = function
| [] -> []
let compare_goals proof goal1 goal2 =
- let _,metasenv,_,_, _ = proof in
+ let _,metasenv,_subst,_,_, _ = proof in
let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in
let ty_sort1,_ = CicTypeChecker.type_of_aux' metasenv ey1 ty1
if List.mem ty already_seen_goals then [] else
let already_seen_goals = ty::already_seen_goals in
let facts = (depth = 1) in
- let _,metasenv,p,_, _ = proof in
+ let _,metasenv,_subst, p,_, _ = proof in
(* first of all we check if the goal has been already
inspected *)
assert (CicUtil.exists_meta goal metasenv);
(* if we just apply the subtitution, the type
is irrelevant: we may use Implicit, since it will
be dropped *)
- CicMetaSubst.apply_subst
- [(goal,(ey, bo, Cic.Implicit None))] in
+ [(goal,(ey, bo, Cic.Implicit None))]
+ in
+ let _ = assert false in
let (proof,_) =
ProofEngineHelpers.subst_meta_and_metasenv_in_proof
proof goal subst_in metasenv in
- [(subst_in,(proof,[],sign))]
+ [(CicMetaSubst.apply_subst subst_in,(proof,[],sign))]
| No d when (d >= depth) ->
(* debug_print (lazy "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); *)
[] (* the empty list means no choices, i.e. failure *)
and auto_new dbd width already_seen_goals universe = function
| [] -> []
| (subst,(proof, goals, sign))::tl ->
- let _,metasenv,_,_, _ = proof in
+ let _,metasenv, _subst, _,_, _ = proof in
let goals'=
List.filter (fun (goal, _) -> CicUtil.exists_meta goal metasenv) goals
in
(List.length goals) > width ->
auto_new dbd width already_seen_goals universe tl
| (subst,(proof, (goal,depth)::gtl, sign))::tl ->
- let _,metasenv,p,_, _ = proof in
+ let _,metasenv,_subst,p,_, _ = proof in
let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
match (auto_single dbd proof goal ey ty depth
(width - (List.length gtl)) sign already_seen_goals) universe
| (_,(proof,[],_))::_ ->
let t2 = Unix.gettimeofday () in
debug_print (lazy "AUTO_TAC HA FINITO");
- let _,_,p,_, _ = proof in
+ let _,_,_subst,p,_, _ = proof in
debug_print (lazy (CicPp.ppterm p));
debug_print (lazy (Printf.sprintf "tempo: %.9f\n" (t2 -. t1)));
(proof,[])
let existselim ~dbd ~universe t id1 t1 id2 t2 =
let aux (proof, goal) =
- let (n,metasenv,bo,ty,attrs) = proof in
+ let (n,metasenv,_subst,bo,ty,attrs) = proof in
let metano,context,_ = CicUtil.lookup_meta goal metasenv in
let t2, metasenv, _ = t2 (Some (Cic.Name id1, Cic.Decl t1) :: context) metasenv CicUniv.oblivion_ugraph in
- let proof' = (n,metasenv,bo,ty,attrs) in
+ let proof' = (n,metasenv,_subst,bo,ty,attrs) in
ProofEngineTypes.apply_tactic (
Tacticals.thens
~start:(Tactics.cut (Cic.Appl [Cic.MutInd (UriManager.uri_of_string "cic:/matita/logic/connectives/ex.ind", 0, []); t1 ; Cic.Lambda (Cic.Name id1, t1, t2)]))
let rewritingstep ~dbd ~universe lhs rhs just last_step =
let aux ((proof,goal) as status) =
- let (curi,metasenv,proofbo,proofty, attrs) = proof in
+ let (curi,metasenv,_subst,proofbo,proofty, attrs) = proof in
let _,context,gty = CicUtil.lookup_meta goal metasenv in
let eq,trans =
match LibraryObjects.eq_URI () with
FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context
(Cic.Name name) ~typ
in
- let proof = curi,metasenv,proofbo,proofty, attrs in
+ let proof = curi,metasenv,_subst,proofbo,proofty, attrs in
let proof,goals =
ProofEngineTypes.apply_tactic
(Tacticals.thens
in
let discriminate'_tac ~term status =
let (proof, goal) = status in
- let _,metasenv,_,_, _ = proof in
+ let _,metasenv,_subst,_,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let termty,_ =
CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
in
let injection_tac ~term status =
let (proof, goal) = status in
- let _,metasenv,_,_, _ = proof in
+ let _,metasenv,_subst, _,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let term = CicSubstitution.lift liftno term in
let termty,_ =
* differiscono (o potrebbero differire?) nell'i-esimo parametro
* del costruttore *)
let term = CicSubstitution.lift liftno term in
- let _,metasenv,_,_, _ = proof in
+ let _,metasenv,_subst,_,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let termty,_ =
CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
(fun status ->
debug_print (lazy "riempo il cut");
let (proof, goal) = status in
- let _,metasenv,_,_, _ = proof in
+ let _,metasenv,_subst,_,_, _ = proof in
let _,context,gty =CicUtil.lookup_meta goal metasenv in
let gty = Unshare.unshare gty in
let new_t1' =
let rec scan_tac ~old_context_length ~index ~tactic =
let scan_tac status =
let (proof, goal) = status in
- let _, metasenv, _, _, _ = proof in
+ let _, metasenv, _subst, _, _, _ = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let context_length = List.length context in
let rec aux index =
let elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback ~what =
let elim_clear_unfold_tac status =
let (proof, goal) = status in
- let _, metasenv, _, _, _ = proof in
+ let _, metasenv, _subst, _, _, _ = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let index, ty = PEH.lookup_type metasenv context what in
let tac =
?(mk_fresh_name_callback = F.mk_fresh_name ~subst:[]) () =
let decompose_tac status =
let (proof, goal) = status in
- let _, metasenv,_,_, _ = proof in
+ let _, metasenv, _subst, _,_, _ = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let tactic = elim_clear_unfold_tac ~sorts ~mk_fresh_name_callback in
let old_context_length = List.length context in
let _rewrite_tac status =
assert (wanted = None); (* this should be checked syntactically *)
let proof,goal = status in
- let curi, metasenv, pbo, pty, attrs = proof in
+ let curi, metasenv, _subst, pbo, pty, attrs = proof in
let (metano,context,gty) = CicUtil.lookup_meta goal metasenv in
let gsort,_ =
CicTypeChecker.type_of_aux' metasenv context gty CicUniv.oblivion_ugraph in
try
let (proof',goals) =
PET.apply_tactic
- (tac ~term:exact_proof newtyp) ((curi,metasenv',pbo,pty, attrs),goal)
+ (tac ~term:exact_proof newtyp) ((curi,metasenv',_subst,pbo,pty, attrs),goal)
in
let goals =
goals@(ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv
let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what status =
let _wanted, hyps_pat, concl_pat = pattern in
let (proof, goal) = status in
- let uri,metasenv,pbo,pty, attrs = proof in
+ let uri,metasenv,_subst,pbo,pty, attrs = proof in
let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
assert (hyps_pat = []); (*CSC: not implemented yet *)
let eq_URI =
let with_what = CicMetaSubst.apply_subst subst with_what in
let pbo = CicMetaSubst.apply_subst subst pbo in
let pty = CicMetaSubst.apply_subst subst pty in
- let status = (uri,metasenv,pbo,pty, attrs),goal in
+ let status = (uri,metasenv,_subst,pbo,pty, attrs),goal in
let ty_of_with_what,u =
CicTypeChecker.type_of_aux'
metasenv context with_what CicUniv.empty_ugraph in
(ProofEngineTypes.Fail
(lazy "Replace: one of the selected terms and the term to be replaced with have not convertible types"))
) l in
- let rec aux n whats status =
+ let rec aux n whats (status : ProofEngineTypes.status) =
match whats with
[] -> ProofEngineTypes.apply_tactic T.id_tac status
| (what,lazy_pattern)::tl ->
~start:(
ProofEngineTypes.mk_tactic
(function ((proof,goal) as status) ->
- let _,metasenv,_,_, _ = proof in
+ let _,metasenv,_subst,_,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let hyps =
try
T.id_tac])
status
and aux_tac n tl = ProofEngineTypes.mk_tactic (aux n tl) in
- aux 0 whats status
+ aux 0 whats (status : ProofEngineTypes.status)
in
ProofEngineTypes.mk_tactic (replace_tac ~pattern ~with_what)
;;
let symmetry_tac =
let symmetry_tac (proof, goal) =
- let (_,metasenv,_,_, _) = proof in
+ let (_,metasenv,_subst,_,_, _) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
match (R.whd context ty) with
(C.Appl [(C.MutInd (uri, 0, [])); _; _; _])
let transitivity_tac ~term =
let transitivity_tac ~term status =
let (proof, goal) = status in
- let (_,metasenv,_,_, _) = proof in
+ let (_,metasenv,_subst,_,_, _) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
match (R.whd context ty) with
(C.Appl [(C.MutInd (uri, 0, [])); _; _; _])
(*let cste = pf_parse_constr gl in*)
let pall str (proof,goal) t =
debug ("tac "^str^" :\n" );
- let curi,metasenv,pbo,pty, attrs = proof in
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
debug ("th = "^ CicPp.ppterm t ^"\n");
debug ("ty = "^ CicPp.ppterm ty^"\n");
let tac_zero_infeq_false gl (n,d) =
let tac_zero_infeq_false gl (n,d) status =
let (proof, goal) = status in
- let curi,metasenv,pbo,pty, attrs = proof in
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
debug("faccio fold di " ^ CicPp.ppterm
let apply_type_tac ~cast:t ~applist:al =
let apply_type_tac ~cast:t ~applist:al (proof,goal) =
- let curi,metasenv,pbo,pty, attrs = proof in
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable context in
let metasenv' = (fresh_meta,context,t)::metasenv in
- let proof' = curi,metasenv',pbo,pty, attrs in
+ let proof' = curi,metasenv',_subst,pbo,pty, attrs in
let proof'',goals =
apply_tactic
(PrimitiveTactics.apply_tac
let my_cut ~term:c =
let my_cut ~term:c (proof,goal) =
- let curi,metasenv,pbo,pty, attrs = proof in
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
let irl =
CicMkImplicit.identity_relocation_list_for_metavariable context in
let metasenv' = (fresh_meta,context,c)::metasenv in
- let proof' = curi,metasenv',pbo,pty, attrs in
+ let proof' = curi,metasenv',_subst,pbo,pty, attrs in
let proof'',goals =
apply_tactic
(apply_type_tac
let tac_use h status =
let (proof, goal) = status in
debug("Inizio TC_USE\n");
- let curi,metasenv,pbo,pty, attrs = proof in
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
debug ("hname = "^ CicPp.ppterm h.hname ^"\n");
debug ("ty = "^ CicPp.ppterm ty^"\n");
debug("inizio EQ\n");
let module C = Cic in
let proof,goal = status in
- let curi,metasenv,pbo,pty, attrs = proof in
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
~direction:`LeftToRight
~pattern:(ProofEngineTypes.conclusion_pattern None)
(C.Meta (fresh_meta,irl)) [])
- ((curi,metasenv',pbo,pty, attrs),goal)
+ ((curi,metasenv',_subst,pbo,pty, attrs),goal)
in
let new_goals = fresh_meta::goals in
debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = "
(* ********************* TATTICA ******************************** *)
let rec fourier (s_proof,s_goal)=
- let s_curi,s_metasenv,s_pbo,s_pty, attrs = s_proof in
+ let s_curi,s_metasenv,_subst,s_pbo,s_pty, attrs = s_proof in
let s_metano,s_context,s_ty = CicUtil.lookup_meta s_goal s_metasenv in
debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto:\n");
debug_pcontext s_context;
(* now we have all the right environment *)
- let curi,metasenv,pbo,pty, attrs = proof in
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
(* now we want to convert hp to inequations, but first we must lift
(Tacticals.thens
~start:(mk_tactic (fun status ->
debug ("inizio t1 strict\n");
- let curi,metasenv,pbo,pty, attrs = proof in
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n");
debug ("ty = "^ CicPp.ppterm ty^"\n");
tac1:=(Tacticals.thens
~start:(mk_tactic (fun status ->
debug("INIZIO TAC 1 2\n");
- let curi,metasenv,pbo,pty, attrs = proof in
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n");
debug ("ty = "^ CicPp.ppterm ty^"\n");
~continuations:[Tacticals.then_
~start:( mk_tactic (fun status ->
let (proof, goal) = status in
- let curi,metasenv,pbo,pty, attrs = proof in
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
apply_tactic
(ReductionTactics.change_tac
Tacticals.then_
~start:(mk_tactic (fun status ->
let (proof, goal) = status in
- let curi,metasenv,pbo,pty, attrs = proof in
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
(* check if ty is of type *)
let w1 =
let id_tac =
let id_tac (proof,goal) =
try
- let _, metasenv, _, _, _ = proof in
+ let _, metasenv, _subst, _, _, _ = proof in
let _, _, _ = CicUtil.lookup_meta goal metasenv in
(proof,[goal])
with CicUtil.Meta_not_found _ -> (proof, [])
in
let clearbody status =
let (proof, goal) = status in
- let _, metasenv, _, _, _ = proof in
+ let _, metasenv, _subst, _, _, _ = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
PET.apply_tactic (PESR.clearbody ~hyp:(find_name index context)) status
in
(* ?(substs = []) *) ?how_many ?(to_what = []) what =
let letin_tac term = PT.letin_tac ~mk_fresh_name_callback term in
let lapply_tac (proof, goal) =
- let xuri, metasenv, u, t, attrs = proof in
+ let xuri, metasenv, _subst, u, t, attrs = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let lemma, _ = TC.type_of_aux' metasenv context what U.empty_ugraph in
let lemma = FNG.clean_dummy_dependent_types lemma in
T.then_ ~start:(letin_tac conclusion)
~continuation:(clearbody ~index:1)
in
- let proof = (xuri, metasenv, u, t, attrs) in
+ let proof = (xuri, metasenv, _subst, u, t, attrs) in
let aux (proof, goals) (tac, goal) =
let proof, new_goals = PET.apply_tactic tac (proof, goal) in
proof, goals @ new_goals
(* ?(substs = []) *) ?(linear = false) ?how_many ?(to_what = []) what =
let lapply_tac status =
let proof, goal = status in
- let _, metasenv, _, _, _ = proof in
+ let _, metasenv, _subst, _, _, _ = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let lapply = lapply_tac_aux ~mk_fresh_name_callback ?how_many ~to_what what in
let tac =
in
let fwd_simpl_tac status =
let (proof, goal) = status in
- let _, metasenv, _, _, _ = proof in
+ let _, metasenv, _subst, _, _, _ = proof in
let _, context, ty = CicUtil.lookup_meta goal metasenv in
let index, major = PEH.lookup_type metasenv context hyp in
match FwdQueries.fwd_simpl ~dbd major with
let fake_constructor_tac ~n (proof, goal) =
let module C = Cic in
let module R = CicReduction in
- let (_,metasenv,_,_, _) = proof in
+ let (_,metasenv,_subst,_,_, _) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
match (R.whd context ty) with
(C.MutInd (uri, typeno, exp_named_subst))
let private_inversion_tac ~term (proof, goal) =
(*DEBUG*) debug_print (lazy ("private inversion begins"));
- let _,metasenv,_,_, _ = proof in
+ let _,metasenv,_subst,_,_, _ = proof in
let uri_of_eq =
match LibraryObjects.eq_URI () with
None -> raise EqualityNotDefinedYet
(*DEBUG*) debug_print (lazy ("after apply HCUT;reflexivity
in private inversion"));
(* apply (ledx_ind( lambda x. lambda y, ...)) *)
- let t1,metasenv,t3,t4, attrs = proof2 in
+ let t1,metasenv,_subst,t3,t4, attrs = proof2 in
let goal2 = List.hd (List.tl gl1) in
let (_,context,_) = CicUtil.lookup_meta goal2 metasenv in
(* rightparameters type list *)
in
(*DEBUG*) debug_print (lazy ("private inversion: termine after refinement: "
^ CicPp.ppterm ref_t));
- let proof2 = (t1,metasenv'',t3,t4, attrs) in
+ let proof2 = (t1,metasenv'',_subst,t3,t4, attrs) in
let my_apply_tac =
let my_apply_tac status =
let proof,goals =
ProofEngineTypes.apply_tactic (P.apply_tac ref_t) status in
let patched_new_goals =
- let (_,metasenv''',_,_, _) = proof in
+ let (_,metasenv''',_subst,_,_, _) = proof in
let new_goals = ProofEngineHelpers.compare_metasenvs
~oldmetasenv:metasenv ~newmetasenv:metasenv''
in
let module PET = ProofEngineTypes in
let inversion_tac ~term (proof, goal) =
(*DEBUG*) debug_print (lazy ("inversion begins"));
- let _,metasenv,_,_, _ = proof in
+ let _,metasenv,_subst,_,_, _ = proof in
let (_,context,goalty) = CicUtil.lookup_meta goal metasenv in
let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
let uri, typeno =
Cic.Appl ([Cic.Const(uri,[])] @ !a @ [Cic.Rel 1])
in
let t = appl_term (arity_length + (List.length cons_list)) inversor_uri in
- let (t1,metasenv,t3,t4, attrs) = proof in
+ let (t1,metasenv,_subst,t3,t4, attrs) = proof in
let (ref_t,_,metasenv'',_) = CicRefine.type_of_aux' metasenv context t
CicUniv.empty_ugraph
in
- let proof = (t1,metasenv'',t3,t4, attrs) in
+ let proof = (t1,metasenv'',_subst,t3,t4, attrs) in
let proof3,gl3 =
ProofEngineTypes.apply_tactic (P.apply_tac ref_t) (proof,goal) in
let patched_new_goals =
- let (_,metasenv''',_,_, _) = proof3 in
+ let (_,metasenv''',_subst,_,_, _) = proof3 in
let new_goals = ProofEngineHelpers.compare_metasenvs
~oldmetasenv:metasenv ~newmetasenv:metasenv''
in
let goal = CicMkImplicit.new_meta metasenv [] in
let metasenv' = (goal,[],ref_theorem)::metasenv in
let attrs = [`Class (`InversionPrinciple); `Generated] in
+ let _subst = [] in
let proof=
- (Some inversor_uri,metasenv',Cic.Meta(goal,[]),ref_theorem, attrs) in
+ (Some inversor_uri,metasenv',_subst,Cic.Meta(goal,[]),ref_theorem, attrs) in
let _,applies =
List.fold_right
(fun _ (i,applies) ->
(proof,goal)
in
let metasenv,bo,ty, attrs =
- match proof1 with (_,metasenv,bo,ty, attrs) -> metasenv,bo,ty, attrs
+ match proof1 with (_,metasenv,_subst,bo,ty, attrs) -> metasenv,bo,ty, attrs
in
assert (metasenv = []);
Some
intersect uris siguris
let compare_goal_list proof goal1 goal2 =
- let _,metasenv,_,_, _ = proof in
+ let _,metasenv, _subst, _,_, _ = proof in
let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in
let ty_sort1,_ =
(* used only by te old auto *)
let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
- let (_, metasenv, _, _, _) = proof in
+ let (_, metasenv, _subst, _, _, _) = proof in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let main, sig_constants = Constr.signature_of ty in
let set = signature_of_hypothesis context metasenv in
^ "\n}"
in
*)
- let (_, metasenv, _, _, _) = proof in
+ let (_, metasenv, _subst, _, _, _) = proof in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let main, sig_constants =
match signature with
let experimental_hint
~(dbd:HMysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
- let (_, metasenv, _, _, _) = proof in
+ let (_, metasenv, _subst, _, _, _) = proof in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let (uris, (main, sig_constants)) =
match signature with
~(dbd:HMysql.dbd) ?(facts=false) ?signature ~universe
((proof, goal) as status)
=
- let (_, metasenv, _, _, _) = proof in
+ let (_, metasenv, _subst, _, _, _) = proof in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let (uris, (main, sig_constants)) =
match signature with
let module C = Cic in
let module U = UriManager in
let module P = PrimitiveTactics in
- let _,metasenv,_,_, _ = proof in
+ let _,metasenv,_subst,_,_, _ = proof in
let _,context,ty = CicUtil.lookup_meta goal metasenv in
let absurd_URI =
match LibraryObjects.absurd_URI () with
if proof_menv = [] then prerr_endline "+++++++++++++++VUOTA"
else prerr_endline (CicMetaSubst.ppmetasenv [] proof_menv);
let proof, goalno = status in
- let uri, metasenv, meta_proof, term_to_prove, attrs = proof in
+ let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
let eq_uri = eq_of_goal type_of_goal in
let names = Utils.names_of_context context in
*)
let proof, real_metasenv =
ProofEngineHelpers.subst_meta_and_metasenv_in_proof
- proof goalno (CicMetaSubst.apply_subst final_subst)
+ proof goalno final_subst
(List.filter (fun i,_,_ -> i<>goalno ) real_menv)
in
let open_goals =
let all_subsumed bag maxm status active passive =
maxmeta := maxm;
let proof, goalno = status in
- let uri, metasenv, meta_proof, term_to_prove, attrs = proof in
+ let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
let env = metasenv,context,CicUniv.empty_ugraph in
let cleaned_goal = Utils.remove_local_context type_of_goal in
let mp = max_l passive_l in
*)
let proof, goalno = status in
- let uri, metasenv, meta_proof, term_to_prove, attrs = proof in
+ let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
let eq_uri = eq_of_goal type_of_goal in
let cleaned_goal = Utils.remove_local_context type_of_goal in
let module T = CicTypeChecker in
let module R = CicReduction in
let module C = Cic in
- let (_,metasenv,_,_, _) = proof in
+ let (_,metasenv,_subst,_,_, _) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let newmeta = max (CicMkImplicit.new_meta metasenv subst) maxmeta in
let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
let subst_in =
(* if we just apply the subtitution, the type is irrelevant:
we may use Implicit, since it will be dropped *)
- CicMetaSubst.apply_subst ((metano,(context,bo',Cic.Implicit None))::subst)
+ ((metano,(context,bo',Cic.Implicit None))::subst)
in
let (newproof, newmetasenv''') =
ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof metano subst_in
=
let module C = Cic in
let module R = CicReduction in
- let (_,metasenv,_,_, _) = proof in
+ let (_,metasenv,_subst,_,_, _) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
let (context',ty',bo') =
term (proof, goal)
=
let module C = Cic in
- let curi,metasenv,pbo,pty, attrs = proof in
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let newmeta1 = ProofEngineHelpers.new_meta_of_proof ~proof in
let newmeta2 = newmeta1 + 1 in
term (proof, goal)
=
let module C = Cic in
- let curi,metasenv,pbo,pty, attrs = proof in
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
(* occur check *)
let occur i t =
let m = CicUtil.metas_of_term t in
let exact_tac ~term =
let exact_tac ~term (proof, goal) =
(* Assumption: the term bo must be closed in the current context *)
- let (_,metasenv,_,_, _) = proof in
+ let (_,metasenv,_subst,_,_, _) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let module T = CicTypeChecker in
let module R = CicReduction in
let beta_after_elim_tac upto predicate =
let beta_after_elim_tac status =
let proof, goal = status in
- let _, metasenv, _, _, _ = proof in
+ let _, metasenv, _subst, _, _, _ = proof in
let _, _, ty = CicUtil.lookup_meta goal metasenv in
let mk_pattern ~equality ~upto ~predicate ty =
(* code adapted from ProceduralConversion.generalize *)
| _ -> raise (PET.Fail (lazy "not implemented"))
in
let ugraph = CicUniv.empty_ugraph in
- let curi, metasenv, proofbo, proofty, attrs = proof in
+ let curi, metasenv, _subst, proofbo, proofty, attrs = proof in
let conjecture = CicUtil.lookup_meta goal metasenv in
let metano, context, ty = conjecture in
let termty,_ugraph = TC.type_of_aux' metasenv context term ugraph in
ProofEngineHelpers.compare_metasenvs
~oldmetasenv:metasenv ~newmetasenv:metasenv''
in
- let proof' = curi,metasenv'',proofbo,proofty, attrs in
+ let proof' = curi,metasenv'',_subst,proofbo,proofty, attrs in
let proof'', new_goals' =
PET.apply_tactic (apply_tac ~term:refined_term) (proof',goal)
in
(* The apply_tactic can have closed some of the new_goals *)
let patched_new_goals =
- let (_,metasenv''',_,_, _) = proof'' in
+ let (_,metasenv''',_subst,_,_, _) = proof'' in
List.filter
(function i -> List.exists (function (j,_,_) -> j=i) metasenv''')
new_goals @ new_goals'
let module U = UriManager in
let module R = CicReduction in
let module C = Cic in
- let (curi,metasenv,proofbo,proofty, attrs) = proof in
+ let (curi,metasenv,_subst, proofbo,proofty, attrs) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let termty,_ = TC.type_of_aux' metasenv context term CicUniv.empty_ugraph in
let termty = CicReduction.whd context termty in
ProofEngineHelpers.compare_metasenvs
~oldmetasenv:metasenv ~newmetasenv:metasenv''
in
- let proof' = curi,metasenv'',proofbo,proofty, attrs in
+ let proof' = curi,metasenv'',_subst,proofbo,proofty, attrs in
let proof'', new_goals' =
PET.apply_tactic (apply_tac ~term:refined_term) (proof',goal)
in
(* The apply_tactic can have closed some of the new_goals *)
let patched_new_goals =
- let (_,metasenv''',_,_,_) = proof'' in
+ let (_,metasenv''',_subst,_,_,_) = proof'' in
List.filter
(function i -> List.exists (function (j,_,_) -> j=i) metasenv''')
new_goals @ new_goals'
let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in
let term = C.Sort C.Set in
let letout_tac (proof, goal) =
- let curi, metasenv, pbo, pty, attrs = proof in
+ let curi, metasenv, _subst, pbo, pty, attrs = proof in
let metano, context, ty = CicUtil.lookup_meta goal metasenv in
let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "hole") ~typ:term in
exception Bad_pattern of string Lazy.t
-let new_meta_of_proof ~proof:(_, metasenv, _, _, _) =
+let new_meta_of_proof ~proof:(_, metasenv, _, _, _, _) =
CicMkImplicit.new_meta metasenv []
let subst_meta_in_proof proof meta term newmetasenv =
- let uri,metasenv,bo,ty, attrs = proof in
+ let uri,metasenv,initial_subst,bo,ty, attrs = proof in
(* empty context is ok for term since it wont be used by apply_subst *)
(* hack: since we do not know the context and the type of term, we
create a substitution with cc =[] and type = Implicit; they will be
* since the parser does not reject as statements terms with
* metavariable therein *)
let ty' = subst_in ty in
- let newproof = uri,metasenv'',bo',ty', attrs in
+ let newproof = uri,metasenv'',initial_subst,bo',ty', attrs in
(newproof, metasenv'')
(*CSC: commento vecchio *)
(*CSC: ci ripasso sopra apply_subst!!! *)
(*CSC: Attenzione! Ora questa funzione applica anche [subst_in] a *)
(*CSC: [newmetasenv]. *)
-let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
- let (uri,_,bo,ty, attrs) = proof in
+let subst_meta_and_metasenv_in_proof proof meta subst newmetasenv =
+ let (uri,_,initial_subst,bo,ty, attrs) = proof in
+ let subst_in = CicMetaSubst.apply_subst subst in
let bo' = subst_in bo in
(* Metavariables can appear also in the *statement* of the theorem
* since the parser does not reject as statements terms with
| _ -> i
) newmetasenv []
in
- let newproof = uri,metasenv',bo',ty', attrs in
+ (* qui da capire se per la fase transitoria si fa initial_subst @ subst
+ * oppure subst *)
+ let newproof = uri,metasenv',subst,bo',ty', attrs in
(newproof, metasenv')
let compare_metasenvs ~oldmetasenv ~newmetasenv =
ProofEngineTypes.proof * Cic.metasenv
val subst_meta_and_metasenv_in_proof :
ProofEngineTypes.proof ->
- int -> (Cic.term -> Cic.term) -> Cic.metasenv ->
+ int -> Cic.substitution -> Cic.metasenv ->
ProofEngineTypes.proof * Cic.metasenv
(* returns the list of goals that are in newmetasenv and were not in
let clearbody ~hyp =
let clearbody (proof, goal) =
- let curi,metasenv,pbo,pty, attrs = proof in
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let metano,_,_ = CicUtil.lookup_meta goal metasenv in
let string_of_name =
function
| t -> t
) metasenv
in
- (curi,metasenv',pbo,pty, attrs), [goal]
+ (curi,metasenv',_subst,pbo,pty, attrs), [goal]
in
PET.mk_tactic clearbody
let clear_one ~hyp =
let clear_one (proof, goal) =
- let curi,metasenv,pbo,pty, attrs = proof in
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let metano,context,ty =
CicUtil.lookup_meta goal metasenv
in
| t -> t
) metasenv
in
- (curi,metasenv',pbo,pty, attrs), [goal]
+ (curi,metasenv',_subst,pbo,pty, attrs), [goal]
in
PET.mk_tactic clear_one
try List.combine froms tos
with Invalid_argument _ -> raise (PET.Fail (lazy error))
in
- let curi, metasenv, pbo, pty, attrs = proof in
+ let curi, metasenv, _subst, pbo, pty, attrs = proof in
let metano, _, _ = CicUtil.lookup_meta goal metasenv in
let rename_map = function
| Some (Cic.Name hyp, decl_or_def) as entry ->
| conjecture -> conjecture
in
let metasenv = List.map map metasenv in
- (curi, metasenv, pbo, pty, attrs), [goal]
+ (curi, metasenv, _subst, pbo, pty, attrs), [goal]
in
PET.mk_tactic rename
(**
current proof (proof uri * metas * (in)complete proof * term to be prooved)
*)
-type proof = UriManager.uri option * Cic.metasenv * Cic.term * Cic.term * Cic.attribute list
+type proof = UriManager.uri option * Cic.metasenv * Cic.substitution * Cic.term * Cic.term * Cic.attribute list
(** current goal, integer index *)
type goal = int
type status = proof * goal
aux max tl
in
let newmeta_idx = aux 0 metasenv in
+ let _subst = [] in
let proof =
- None, (newmeta_idx, [], ty) :: metasenv, Cic.Meta (newmeta_idx, []), ty, attrs
+ None, (newmeta_idx, [], ty) :: metasenv, _subst, Cic.Meta (newmeta_idx, []), ty, attrs
in
(proof, newmeta_idx)
calls the opaque tactic on the status
*)
let apply_tactic t status =
- let (uri,metasenv,bo,ty, attrs), gl = t status in
+ let (uri,metasenv,subst,bo,ty, attrs), gl = t status in
match
CicRefine.pack_coercion_obj
(Cic.CurrentProof ("",metasenv,Cic.Rel ~-1,ty,[],attrs))
with
| Cic.CurrentProof (_,metasenv,_,ty,_, attrs) ->
- (uri,metasenv,bo,ty, attrs), gl
+ (uri,metasenv,subst,bo,ty, attrs), gl
| _ -> assert false
;;
type mk_fresh_name_type =
Cic.metasenv -> Cic.context -> Cic.name -> typ:Cic.term -> Cic.name
-let goals_of_proof (_,metasenv,_,_,_) = List.map (fun (g,_,_) -> g) metasenv
+let goals_of_proof (_,metasenv,_subst,_,_,_) = List.map (fun (g,_,_) -> g) metasenv
current proof (proof uri * metas * (in)complete proof * term to be prooved)
*)
type proof =
- UriManager.uri option * Cic.metasenv * Cic.term * Cic.term * Cic.attribute list
+ UriManager.uri option * Cic.metasenv * Cic.substitution * Cic.term * Cic.term * Cic.attribute list
(** current goal, integer index *)
type goal = int
type status = proof * goal
(* Note: this code is almost identical to change_tac and
* it could be unified by making the change function a callback *)
let reduction_tac ~reduction ~pattern (proof,goal) =
- let curi,metasenv,pbo,pty, attrs = proof in
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
let change subst where terms metasenv ugraph =
if terms = [] then where, metasenv, ugraph
| _ as t -> t
) metasenv
in
- (curi,metasenv',pbo,pty, attrs), [metano]
+ (curi,metasenv',_subst,pbo,pty, attrs), [metano]
;;
let simpl_tac ~pattern =
term(s) to be replaced. *)
let change_tac ~pattern with_what =
let change_tac ~pattern ~with_what (proof, goal) =
- let curi,metasenv,pbo,pty, attrs = proof in
+ let curi,metasenv,_subst,pbo,pty, attrs = proof in
let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
let change subst where terms metasenv ugraph =
if terms = [] then where, metasenv, ugraph
| _ as t -> t)
metasenv
in
- (curi,metasenv',pbo,pty, attrs), [metano]
+ (curi,metasenv',_subst,pbo,pty, attrs), [metano]
in
mk_tactic (change_tac ~pattern ~with_what)
@param proof a proof
@return the uri of a given proof
*)
-let uri_of_proof ~proof:(uri, _, _, _, _) = uri
+let uri_of_proof ~proof:(uri, _, _, _, _, _) = uri
(**
@param status current proof engine status
@raise Failure if proof is None
@return current goal's metasenv
*)
-let metasenv_of_status ((_,m,_,_, _), _) = m
+let metasenv_of_status ((_,m,_,_,_, _), _) = m
(**
@param status a proof engine status
(ProofEngineTypes.apply_tactic (S.clear ~hyps:[name_of_hyp]) status))
| (_, []) -> failwith "Ring.purge_hyps_tac: no hypotheses left"
in
- let (_, metasenv, _, _, _) = proof in
+ let (_, metasenv, _subst, _, _, _) = proof in
let (_, context, _) = CicUtil.lookup_meta goal metasenv in
let proof',goal' = aux count context status in
assert (goal = goal') ;
let setoid_reflexivity_tac =
let tac ((proof,goal) as status) =
- let (_,metasenv,_,_, _) = proof in
+ let (_,metasenv,_subst,_,_, _) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
try
let relation_class =
incr next_id;
!next_id
in
- let initial_proof = ((uri: UriManager.uri option), metasenv, body, typ, attrs) in
+ let _subst = ([] : Cic.substitution) in
+ let initial_proof = ((uri: UriManager.uri option), metasenv, _subst, body, typ, attrs) in
let next_goal (goals, proof) =
match goals, proof with
| goal :: _, _ -> Some goal
- | [], (_, (goal, _, _) :: _, _, _, _) ->
+ | [], (_, (goal, _, _) :: _, _, _, _, _) ->
(* the tactic left no open goal: let's choose the first open goal *)
Some goal
| _, _ -> None
raise exn
*)
- method uri = let (uri, _, _, _, _) = _proof in uri
- method metasenv = let (_, metasenv, _, _, _) = _proof in metasenv
- method body = let (_, _, body, _, _) = _proof in body
- method typ = let (_, _, _, typ, _) = _proof in typ
- method attrs = let (_, _, _, _, attrs) = _proof in attrs
+ method uri = let (uri, _, _, _, _, _) = _proof in uri
+ method metasenv = let (_, metasenv, _, _, _, _) = _proof in metasenv
+ method body = let (_, _, _, body, _, _) = _proof in body
+ method typ = let (_, _, _, _, typ, _) = _proof in typ
+ method attrs = let (_, _, _, _, _, attrs) = _proof in attrs
method set_metasenv metasenv =
- let (uri, _, body, typ, attes) = _proof in
- _proof <- (uri, metasenv, body, typ, attrs)
+ let (uri, _, _subst,body, typ, attes) = _proof in
+ _proof <- (uri, metasenv, _subst,body, typ, attrs)
method set_uri uri =
- let (old_uri, metasenv, body, typ, attrs) = _proof in
+ let (old_uri, metasenv, _subst,body, typ, attrs) = _proof in
if old_uri <> None then
raise Uri_redefinition;
- _proof <- (Some uri, metasenv, body, typ, attrs)
+ _proof <- (Some uri, metasenv, _subst,body, typ, attrs)
method conjecture goal =
- let (_, metasenv, _, _, _) = _proof in
+ let (_, metasenv, _subst, _, _, _) = _proof in
CicUtil.lookup_meta goal metasenv
method apply_tactic tactic =
let lift_rewrite_tac ~context ~direction ~pattern equality =
let lift_rewrite_tac status =
let (proof, goal) = status in
- let (_, metasenv, _, _, _) = proof in
+ let (_, metasenv, _subst, _, _, _) = proof in
let _, new_context, _ = CicUtil.lookup_meta goal metasenv in
let n = List.length new_context - List.length context in
let equality = S.lift n equality in
let lift_destruct_tac ~context ~what =
let lift_destruct_tac status =
let (proof, goal) = status in
- let (_, metasenv, _, _, _) = proof in
+ let (_, metasenv, _subst, _, _, _) = proof in
let _, new_context, _ = CicUtil.lookup_meta goal metasenv in
let n = List.length new_context - List.length context in
let what = S.lift n what in
in
let subst_tac status =
let (proof, goal) = status in
- let (_, metasenv, _, _, _) = proof in
+ let (_, metasenv, _subst, _, _, _) = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let what = match PEH.get_rel context hyp with
| Some t -> t
| _ -> None
in
let (proof, goal) = status in
- let (_, metasenv, _, _, _) = proof in
+ let (_, metasenv, _subst, _, _, _) = proof in
let _, context, _ = CicUtil.lookup_meta goal metasenv in
let tactics = HEL.list_rev_map_filter map context in
let result = PET.apply_tactic (T.seq ~tactics) status in
let id_tac =
let id_tac (proof,goal) =
- let _, metasenv, _, _, _ = proof in
+ let _, metasenv, _subst, _, _, _ = proof in
let _, _, _ = CicUtil.lookup_meta goal metasenv in
(proof,[goal])
in
let fail_tac =
let fail_tac (proof,goal) =
- let _, metasenv, _, _, _ = proof in
+ let _, metasenv, _subst, _ , _, _ = proof in
let _, _, _ = CicUtil.lookup_meta goal metasenv in
raise (PET.Fail (lazy "fail tactical"))
in
let progress_tactic ~tactic =
let msg = lazy "Failed to progress" in
- let progress_tactic (((_,metasenv,_,_,_),_) as istatus) =
- let ((_,metasenv',_,_,_),_) as ostatus =
+ let progress_tactic (((_,metasenv,_subst,_,_,_),_) as istatus) =
+ let ((_,metasenv',_subst,_,_,_),_) as ostatus =
PET.apply_tactic tactic istatus
in
(*CSC: Warning
let module R = CicReduction in
let module S = CicSubstitution in
let module PT = PrimitiveTactics in
- let _,metasenv,_,_, _ = proof in
+ let _,metasenv,_subst,_,_, _ = proof in
let _,context,ty = CicUtil.lookup_meta goal metasenv in
let rec find n = function
hd::tl ->
let module C = Cic in
let module P = PrimitiveTactics in
let module T = Tacticals in
- let uri,metasenv,pbo,pty, attrs = proof in
+ let uri,metasenv,_subst,pbo,pty, attrs = proof in
let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
let subst,metasenv,u,selected_hyps,terms_with_context =
ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
else
u1
) u terms_with_context) ;
- let status = (uri,metasenv',pbo,pty, attrs),goal in
+ let status = (uri,metasenv',_subst,pbo,pty, attrs),goal in
let proof,goals =
PET.apply_tactic
(T.thens
T.id_tac])
status
in
- let _,metasenv'',_,_, _ = proof in
+ let _,metasenv'',_subst,_,_, _ = proof in
(* CSC: the following is just a bad approximation since a meta
can be closed and then re-opened! *)
(proof,
(MatitaScript.current ())#grafite_status.GrafiteTypes.proof_status
with
| GrafiteTypes.No_proof -> (Cic.Implicit None)
- | Incomplete_proof i -> let _,_,p,_, _ = i.GrafiteTypes.proof in p
- | Proof p -> let _,_,p,_, _ = p in p
+ | Incomplete_proof i -> let _,_,_subst,p,_, _ = i.GrafiteTypes.proof in p
+ | Proof p -> let _,_,_subst,p,_, _ = p in p
| Intermediate _ -> assert false)));
addDebugItem "Print current proof (natural language) to stderr"
(fun _ ->
with
| GrafiteTypes.No_proof -> assert false
| Incomplete_proof i ->
- let _,m,p,ty, attrs = i.GrafiteTypes.proof in
+ let _,m,_subst,p,ty, attrs = i.GrafiteTypes.proof in
Cic.CurrentProof ("current (incomplete) proof",m,p,ty,[],attrs)
- | Proof (_,m,p,ty, attrs) ->
+ | Proof (_,m,_subst,p,ty, attrs) ->
Cic.CurrentProof ("current proof",m,p,ty,[],attrs)
| Intermediate _ -> assert false)));
(* addDebugItem "ask record choice"
_metasenv <- [];
self#script#setGoal None
- method load_sequents { proof = (_,metasenv,_,_, _) as proof; stack = stack } =
+ method load_sequents
+ { proof = (_,metasenv,_subst,_,_, _) as proof; stack = stack }
+ =
_metasenv <- metasenv;
pages <- 0;
let win goal_switch =
method private home () =
self#_showMath;
match self#script#grafite_status.proof_status with
- | Proof (uri, metasenv, bo, ty, attrs) ->
+ | Proof (uri, metasenv, _subst, bo, ty, attrs) ->
let name = UriManager.name_of_uri (HExtlib.unopt uri) in
let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in
self#_loadObj obj
- | Incomplete_proof { proof = (uri, metasenv, bo, ty, attrs) } ->
+ | Incomplete_proof { proof = (uri, metasenv, _subst, bo, ty, attrs) } ->
let name = UriManager.name_of_uri (HExtlib.unopt uri) in
let obj = Cic.CurrentProof (name, metasenv, bo, ty, [], attrs) in
self#_loadObj obj
guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
[], "", parsed_text_length
| TA.WHint (loc, term) ->
- let s = ((None,[0,[],term], Cic.Meta (0,[]) ,term, []),0) in
+ let _subst = [] in
+ let s = ((None,[0,[],term], _subst, Cic.Meta (0,[]) ,term, []),0) in
let l = List.map fst (MQ.experimental_hint ~dbd s) in
let entry = `Whelp (pp_macro mac, l) in
guistuff.mathviewer#show_uri_list ~reuse:true ~entry l;
let watch_statuses lexicon_status grafite_status =
match grafite_status.GrafiteTypes.proof_status with
GrafiteTypes.Incomplete_proof
- {GrafiteTypes.proof = uri,metasenv,bo,ty,attrs ;
+ {GrafiteTypes.proof = uri,metasenv,_subst,bo,ty,attrs ;
GrafiteTypes.stack = stack } ->
let open_goals = Continuationals.Stack.open_goals stack in
print_endline
projects / helm.git / commitdiff