-type options = {
- do_heavy_checks: bool ;
- include_paths: string list ;
- clean_baseuri: bool
-}
-
-type statement =
- (CicNotationPt.term, CicNotationPt.term, GrafiteAst.reduction, GrafiteAst.obj,
- string)
- GrafiteAst.statement
-
-(** create a ProofEngineTypes.mk_fresh_name_type function which uses given
- * names as long as they are available, then it fallbacks to name generation
- * using FreshNamesGenerator module *)
-let namer_of names =
- let len = List.length names in
- let count = ref 0 in
- fun metasenv context name ~typ ->
- if !count < len then begin
- let name = Cic.Name (List.nth names !count) in
- incr count;
- name
- end else
- FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
-
-let tactic_of_ast ast =
- let module PET = ProofEngineTypes in
- match ast with
- | GrafiteAst.Absurd (_, term) -> Tactics.absurd term
- | GrafiteAst.Apply (_, term) -> Tactics.apply term
- | GrafiteAst.Assumption _ -> Tactics.assumption
- | GrafiteAst.Auto (_,depth,width,paramodulation) ->
- AutoTactic.auto_tac ?depth ?width ?paramodulation
- ~dbd:(MatitaDb.instance ()) ()
- | GrafiteAst.Change (_, pattern, with_what) ->
- Tactics.change ~pattern with_what
- | GrafiteAst.Clear (_,id) -> Tactics.clear id
- | GrafiteAst.ClearBody (_,id) -> Tactics.clearbody id
- | GrafiteAst.Contradiction _ -> Tactics.contradiction
- | GrafiteAst.Compare (_, term) -> Tactics.compare term
- | GrafiteAst.Constructor (_, n) -> Tactics.constructor n
- | GrafiteAst.Cut (_, ident, term) ->
- let names = match ident with None -> [] | Some id -> [id] in
- Tactics.cut ~mk_fresh_name_callback:(namer_of names) term
- | GrafiteAst.DecideEquality _ -> Tactics.decide_equality
- | GrafiteAst.Decompose (_, types, what, names) ->
- let to_type = function
- | GrafiteAst.Type (uri, typeno) -> uri, typeno
- | GrafiteAst.Ident _ -> assert false
- in
- let user_types = List.rev_map to_type types in
- let dbd = MatitaDb.instance () in
- let mk_fresh_name_callback = namer_of names in
- Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types what
- | GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term
- | GrafiteAst.Elim (_, what, using, depth, names) ->
- Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names)
- what
- | GrafiteAst.ElimType (_, what, using, depth, names) ->
- Tactics.elim_type ?using ?depth ~mk_fresh_name_callback:(namer_of names)
- what
- | GrafiteAst.Exact (_, term) -> Tactics.exact term
- | GrafiteAst.Exists _ -> Tactics.exists
- | GrafiteAst.Fail _ -> Tactics.fail
- | GrafiteAst.Fold (_, reduction_kind, term, pattern) ->
- let reduction =
- match reduction_kind with
- | `Normalize ->
- PET.const_lazy_reduction
- (CicReduction.normalize ~delta:false ~subst:[])
- | `Reduce -> PET.const_lazy_reduction ProofEngineReduction.reduce
- | `Simpl -> PET.const_lazy_reduction ProofEngineReduction.simpl
- | `Unfold None ->
- PET.const_lazy_reduction (ProofEngineReduction.unfold ?what:None)
- | `Unfold (Some lazy_term) ->
- (fun context metasenv ugraph ->
- let what, metasenv, ugraph = lazy_term context metasenv ugraph in
- ProofEngineReduction.unfold ~what, metasenv, ugraph)
- | `Whd ->
- PET.const_lazy_reduction (CicReduction.whd ~delta:false ~subst:[])
- in
- Tactics.fold ~reduction ~term ~pattern
- | GrafiteAst.Fourier _ -> Tactics.fourier
- | GrafiteAst.FwdSimpl (_, hyp, names) ->
- Tactics.fwd_simpl ~mk_fresh_name_callback:(namer_of names)
- ~dbd:(MatitaDb.instance ()) hyp
- | GrafiteAst.Generalize (_,pattern,ident) ->
- let names = match ident with None -> [] | Some id -> [id] in
- Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern
- | GrafiteAst.Goal (_, n) -> Tactics.set_goal n
- | GrafiteAst.IdTac _ -> Tactics.id
- | GrafiteAst.Injection (_,term) -> Tactics.injection term
- | GrafiteAst.Intros (_, None, names) ->
- PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
- | GrafiteAst.Intros (_, Some num, names) ->
- PrimitiveTactics.intros_tac ~howmany:num
- ~mk_fresh_name_callback:(namer_of names) ()
- | GrafiteAst.LApply (_, how_many, to_what, what, ident) ->
- let names = match ident with None -> [] | Some id -> [id] in
- Tactics.lapply ~mk_fresh_name_callback:(namer_of names) ?how_many
- ~to_what what
- | GrafiteAst.Left _ -> Tactics.left
- | GrafiteAst.LetIn (loc,term,name) ->
- Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
- | GrafiteAst.Reduce (_, reduction_kind, pattern) ->
- (match reduction_kind with
- | `Normalize -> Tactics.normalize ~pattern
- | `Reduce -> Tactics.reduce ~pattern
- | `Simpl -> Tactics.simpl ~pattern
- | `Unfold what -> Tactics.unfold ~pattern what
- | `Whd -> Tactics.whd ~pattern)
- | GrafiteAst.Reflexivity _ -> Tactics.reflexivity
- | GrafiteAst.Replace (_, pattern, with_what) ->
- Tactics.replace ~pattern ~with_what
- | GrafiteAst.Rewrite (_, direction, t, pattern) ->
- EqualityTactics.rewrite_tac ~direction ~pattern t
- | GrafiteAst.Right _ -> Tactics.right
- | GrafiteAst.Ring _ -> Tactics.ring
- | GrafiteAst.Split _ -> Tactics.split
- | GrafiteAst.Symmetry _ -> Tactics.symmetry
- | GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term
-
-let singleton = function
- | [x], _ -> x
- | _ -> assert false
-
-let disambiguate_term status_ref term =
- let status = !status_ref in
- let (aliases, metasenv, cic, _) =
- singleton
- (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
- ~aliases:status.aliases ~universe:(Some status.multi_aliases)
- ~context:(MatitaMisc.get_proof_context status)
- ~metasenv:(MatitaMisc.get_proof_metasenv status) term)
- in
- let status = MatitaTypes.set_metasenv metasenv status in
- let status = MatitaSync.compute_diff_and_set_proof_aliases status aliases in
- status_ref := status;
- cic
-
- (** disambiguate_lazy_term (circa): term -> (unit -> status) * lazy_term
- * rationale: lazy_term will be invoked in different context to obtain a term,
- * each invocation will disambiguate the term and can add aliases. Once all
- * disambiguations have been performed, the first returned function can be
- * used to obtain the resulting aliases *)
-let disambiguate_lazy_term status_ref term =
- (fun context metasenv ugraph ->
- let status = !status_ref in
- let (aliases, metasenv, cic, ugraph) =
- singleton
- (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
- ~initial_ugraph:ugraph ~aliases:status.aliases
- ~universe:(Some status.multi_aliases) ~context ~metasenv term)
- in
- let status = MatitaTypes.set_metasenv metasenv status in
- let status = MatitaSync.compute_diff_and_set_proof_aliases status aliases in
- status_ref := status;
- cic, metasenv, ugraph)
-
-let disambiguate_pattern status_ref (wanted, hyp_paths, goal_path) =
- let interp path = Disambiguate.interpretate_path [] path in
- let goal_path = interp goal_path in
- let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
- let wanted =
- match wanted with
- None -> None
- | Some wanted ->
- let wanted = disambiguate_lazy_term status_ref wanted in
- Some wanted
- in
- (wanted, hyp_paths ,goal_path)
-
-let disambiguate_reduction_kind aliases_ref = function
- | `Unfold (Some t) ->
- let t = disambiguate_lazy_term aliases_ref t in
- `Unfold (Some t)
- | `Normalize
- | `Reduce
- | `Simpl
- | `Unfold None
- | `Whd as kind -> kind
-
-let disambiguate_tactic status tactic =
- let status_ref = ref status in
- let tactic =
- match tactic with
- | GrafiteAst.Absurd (loc, term) ->
- let cic = disambiguate_term status_ref term in
- GrafiteAst.Absurd (loc, cic)
- | GrafiteAst.Apply (loc, term) ->
- let cic = disambiguate_term status_ref term in
- GrafiteAst.Apply (loc, cic)
- | GrafiteAst.Assumption loc -> GrafiteAst.Assumption loc
- | GrafiteAst.Auto (loc,depth,width,paramodulation) ->
- GrafiteAst.Auto (loc,depth,width,paramodulation)
- | GrafiteAst.Change (loc, pattern, with_what) ->
- let with_what = disambiguate_lazy_term status_ref with_what in
- let pattern = disambiguate_pattern status_ref pattern in
- GrafiteAst.Change (loc, pattern, with_what)
- | GrafiteAst.Clear (loc,id) -> GrafiteAst.Clear (loc,id)
- | GrafiteAst.ClearBody (loc,id) -> GrafiteAst.ClearBody (loc,id)
- | GrafiteAst.Compare (loc,term) ->
- let term = disambiguate_term status_ref term in
- GrafiteAst.Compare (loc,term)
- | GrafiteAst.Constructor (loc,n) -> GrafiteAst.Constructor (loc,n)
- | GrafiteAst.Contradiction loc -> GrafiteAst.Contradiction loc
- | GrafiteAst.Cut (loc, ident, term) ->
- let cic = disambiguate_term status_ref term in
- GrafiteAst.Cut (loc, ident, cic)
- | GrafiteAst.DecideEquality loc -> GrafiteAst.DecideEquality loc
- | GrafiteAst.Decompose (loc, types, what, names) ->
- let disambiguate types = function
- | GrafiteAst.Type _ -> assert false
- | GrafiteAst.Ident id ->
- (match disambiguate_term status_ref (CicNotationPt.Ident (id, None)) with
- | Cic.MutInd (uri, tyno, _) ->
- (GrafiteAst.Type (uri, tyno) :: types)
- | _ -> raise Disambiguate.NoWellTypedInterpretation)
- in
- let types = List.fold_left disambiguate [] types in
- GrafiteAst.Decompose (loc, types, what, names)
- | GrafiteAst.Discriminate (loc,term) ->
- let term = disambiguate_term status_ref term in
- GrafiteAst.Discriminate(loc,term)
- | GrafiteAst.Exact (loc, term) ->
- let cic = disambiguate_term status_ref term in
- GrafiteAst.Exact (loc, cic)
- | GrafiteAst.Elim (loc, what, Some using, depth, idents) ->
- let what = disambiguate_term status_ref what in
- let using = disambiguate_term status_ref using in
- GrafiteAst.Elim (loc, what, Some using, depth, idents)
- | GrafiteAst.Elim (loc, what, None, depth, idents) ->
- let what = disambiguate_term status_ref what in
- GrafiteAst.Elim (loc, what, None, depth, idents)
- | GrafiteAst.ElimType (loc, what, Some using, depth, idents) ->
- let what = disambiguate_term status_ref what in
- let using = disambiguate_term status_ref using in
- GrafiteAst.ElimType (loc, what, Some using, depth, idents)
- | GrafiteAst.ElimType (loc, what, None, depth, idents) ->
- let what = disambiguate_term status_ref what in
- GrafiteAst.ElimType (loc, what, None, depth, idents)
- | GrafiteAst.Exists loc -> GrafiteAst.Exists loc
- | GrafiteAst.Fail loc -> GrafiteAst.Fail loc
- | GrafiteAst.Fold (loc,red_kind, term, pattern) ->
- let pattern = disambiguate_pattern status_ref pattern in
- let term = disambiguate_lazy_term status_ref term in
- let red_kind = disambiguate_reduction_kind status_ref red_kind in
- GrafiteAst.Fold (loc, red_kind, term, pattern)
- | GrafiteAst.FwdSimpl (loc, hyp, names) ->
- GrafiteAst.FwdSimpl (loc, hyp, names)
- | GrafiteAst.Fourier loc -> GrafiteAst.Fourier loc
- | GrafiteAst.Generalize (loc,pattern,ident) ->
- let pattern = disambiguate_pattern status_ref pattern in
- GrafiteAst.Generalize (loc,pattern,ident)
- | GrafiteAst.Goal (loc, g) -> GrafiteAst.Goal (loc, g)
- | GrafiteAst.IdTac loc -> GrafiteAst.IdTac loc
- | GrafiteAst.Injection (loc, term) ->
- let term = disambiguate_term status_ref term in
- GrafiteAst.Injection (loc,term)
- | GrafiteAst.Intros (loc, num, names) -> GrafiteAst.Intros (loc, num, names)
- | GrafiteAst.LApply (loc, depth, to_what, what, ident) ->
- let f term to_what =
- let term = disambiguate_term status_ref term in
- term :: to_what
- in
- let to_what = List.fold_right f to_what [] in
- let what = disambiguate_term status_ref what in
- GrafiteAst.LApply (loc, depth, to_what, what, ident)
- | GrafiteAst.Left loc -> GrafiteAst.Left loc
- | GrafiteAst.LetIn (loc, term, name) ->
- let term = disambiguate_term status_ref term in
- GrafiteAst.LetIn (loc,term,name)
- | GrafiteAst.Reduce (loc, red_kind, pattern) ->
- let pattern = disambiguate_pattern status_ref pattern in
- let red_kind = disambiguate_reduction_kind status_ref red_kind in
- GrafiteAst.Reduce(loc, red_kind, pattern)
- | GrafiteAst.Reflexivity loc -> GrafiteAst.Reflexivity loc
- | GrafiteAst.Replace (loc, pattern, with_what) ->
- let pattern = disambiguate_pattern status_ref pattern in
- let with_what = disambiguate_lazy_term status_ref with_what in
- GrafiteAst.Replace (loc, pattern, with_what)
- | GrafiteAst.Rewrite (loc, dir, t, pattern) ->
- let term = disambiguate_term status_ref t in
- let pattern = disambiguate_pattern status_ref pattern in
- GrafiteAst.Rewrite (loc, dir, term, pattern)
- | GrafiteAst.Right loc -> GrafiteAst.Right loc
- | GrafiteAst.Ring loc -> GrafiteAst.Ring loc
- | GrafiteAst.Split loc -> GrafiteAst.Split loc
- | GrafiteAst.Symmetry loc -> GrafiteAst.Symmetry loc
- | GrafiteAst.Transitivity (loc, term) ->
- let cic = disambiguate_term status_ref term in
- GrafiteAst.Transitivity (loc, cic)
- in
- status_ref, tactic
-
-let reorder_metasenv start refine tactic goals current_goal always_opens_a_goal=
- let module PEH = ProofEngineHelpers in
- (* phase one calculates:
- * new_goals_from_refine: goals added by refine
- * head_goal: the first goal opened by ythe tactic
- * other_goals: other goals opened by the tactic
- *)
- let new_goals_from_refine = PEH.compare_metasenvs start refine in
- let new_goals_from_tactic = PEH.compare_metasenvs refine tactic in
- let head_goal, other_goals, goals =
- match goals with
- | [] -> None,[],goals
- | hd::tl ->
- (* assert (List.mem hd new_goals_from_tactic);
- * invalidato dalla goal_tac
- * *)
- Some hd, List.filter ((<>) hd) new_goals_from_tactic, List.filter ((<>)
- hd) goals
- in
- let produced_goals =
- match head_goal with
- | None -> new_goals_from_refine @ other_goals
- | Some x -> x :: new_goals_from_refine @ other_goals
- in
- (* extract the metas generated by refine and tactic *)
- let metas_for_tactic_head =
- match head_goal with
- | None -> []
- | Some head_goal -> List.filter (fun (n,_,_) -> n = head_goal) tactic in
- let metas_for_tactic_goals =
- List.map
- (fun x -> List.find (fun (metano,_,_) -> metano = x) tactic)
- goals
- in
- let metas_for_refine_goals =
- List.filter (fun (n,_,_) -> List.mem n new_goals_from_refine) tactic in
- let produced_metas, goals =
- let produced_metas =
- if always_opens_a_goal then
- metas_for_tactic_head @ metas_for_refine_goals @
- metas_for_tactic_goals
- else
- metas_for_refine_goals @ metas_for_tactic_head @
- metas_for_tactic_goals
- in
- let goals = List.map (fun (metano, _, _) -> metano) produced_metas in
- produced_metas, goals
- in
- (* residual metas, preserving the original order *)
- let before, after =
- let rec split e =
- function
- | [] -> [],[]
- | (metano, _, _) :: tl when metano = e ->
- [], List.map (fun (x,_,_) -> x) tl
- | (metano, _, _) :: tl -> let b, a = split e tl in metano :: b, a
- in
- let find n metasenv =
- try
- Some (List.find (fun (metano, _, _) -> metano = n) metasenv)
- with Not_found -> None
- in
- let extract l =
- List.fold_right
- (fun n acc ->
- match find n tactic with
- | Some x -> x::acc
- | None -> acc
- ) l [] in
- let before_l, after_l = split current_goal start in
- let before_l =
- List.filter (fun x -> not (List.mem x produced_goals)) before_l in
- let after_l =
- List.filter (fun x -> not (List.mem x produced_goals)) after_l in
- let before = extract before_l in
- let after = extract after_l in
- before, after
- in
- (* DEBUG CODE
- let print_m name metasenv =
- prerr_endline (">>>>> " ^ name);
- prerr_endline (CicMetaSubst.ppmetasenv metasenv [])
- in
- print_m "BEGIN" start;
- prerr_endline ("goal was: " ^ string_of_int current_goal);
- prerr_endline ("and metas from refine are:");
- List.iter
- (fun t -> prerr_string (" " ^ string_of_int t))
- new_goals_from_refine;
- prerr_endline "";
- print_m "before" before;
- print_m "metas_for_tactic_head" metas_for_tactic_head;
- print_m "metas_for_refine_goals" metas_for_refine_goals;
- print_m "metas_for_tactic_goals" metas_for_tactic_goals;
- print_m "after" after;
- FINE DEBUG CODE *)
- before @ produced_metas @ after, goals
-
-(* maybe we only need special cases for apply and goal *)
-let classify_tactic tactic =
- match tactic with
- (* tactics that can't close the goal (return a goal we want to "select") *)
- | GrafiteAst.Rewrite _
- | GrafiteAst.Split _
- | GrafiteAst.Replace _
- | GrafiteAst.Reduce _
- | GrafiteAst.Injection _
- | GrafiteAst.IdTac _
- | GrafiteAst.Generalize _
- | GrafiteAst.Elim _
- | GrafiteAst.Decompose _ -> true, true
- (* tactics we don't want to reorder goals. I think only Goal needs this. *)
- | GrafiteAst.Goal _ -> false, true
- (* tactics like apply *)
- | _ -> true, false
-
-let apply_tactic tactic status =
- let starting_metasenv = MatitaMisc.get_proof_metasenv status in
- let status_ref, tactic = disambiguate_tactic status tactic in
- let metasenv_after_refinement = MatitaMisc.get_proof_metasenv !status_ref in
- let proof_status = MatitaMisc.get_proof_status !status_ref in
- let needs_reordering, always_opens_a_goal = classify_tactic tactic in
- let tactic = tactic_of_ast tactic in
- (* apply tactic will change the status pointed by status_ref ... *)
- let current_goal = let _, g = proof_status in g in
- let (proof, goals) = ProofEngineTypes.apply_tactic tactic proof_status in
- let proof, goals =
- if needs_reordering then
- let uri, metasenv_after_tactic, t, ty = proof in
- let reordered_metasenv, goals =
- reorder_metasenv starting_metasenv metasenv_after_refinement
- metasenv_after_tactic goals current_goal always_opens_a_goal in
- (uri, reordered_metasenv, t, ty), goals
- else
- proof, goals