-type options = {
- do_heavy_checks: bool ;
- include_paths: string list ;
- clean_baseuri: bool
-}
-
-(** 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,full) ->
- AutoTactic.auto_tac ?depth ?width ?paramodulation ?full
- ~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
-
- (** @param term not meaningful when context is given *)
-let disambiguate_term ?context status_ref goal term =
- let status = !status_ref in
- let context =
- match context with
- | Some c -> c
- | None -> MatitaTypes.get_proof_context status goal
- in
- let (diff, metasenv, cic, _) =
- singleton
- (MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
- ~aliases:status.aliases ~universe:(Some status.multi_aliases)
- ~context ~metasenv:(MatitaTypes.get_proof_metasenv status) term)
- in
- let status = MatitaTypes.set_metasenv metasenv status in
- let status = MatitaSync.set_proof_aliases status diff 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 (diff, 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.set_proof_aliases status diff 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 goal tactic =
- let status_ref = ref status in
- let tactic =
- match tactic with
- | GrafiteAst.Absurd (loc, term) ->
- let cic = disambiguate_term status_ref goal term in
- GrafiteAst.Absurd (loc, cic)
- | GrafiteAst.Apply (loc, term) ->
- let cic = disambiguate_term status_ref goal term in
- GrafiteAst.Apply (loc, cic)
- | GrafiteAst.Assumption loc -> GrafiteAst.Assumption loc
- | GrafiteAst.Auto (loc,depth,width,paramodulation,full) ->
- GrafiteAst.Auto (loc,depth,width,paramodulation,full)
- | 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 goal 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 goal 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 goal
- (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 goal term in
- GrafiteAst.Discriminate(loc,term)
- | GrafiteAst.Exact (loc, term) ->
- let cic = disambiguate_term status_ref goal term in
- GrafiteAst.Exact (loc, cic)
- | GrafiteAst.Elim (loc, what, Some using, depth, idents) ->
- let what = disambiguate_term status_ref goal what in
- let using = disambiguate_term status_ref goal using in
- GrafiteAst.Elim (loc, what, Some using, depth, idents)
- | GrafiteAst.Elim (loc, what, None, depth, idents) ->
- let what = disambiguate_term status_ref goal what in
- GrafiteAst.Elim (loc, what, None, depth, idents)
- | GrafiteAst.ElimType (loc, what, Some using, depth, idents) ->
- let what = disambiguate_term status_ref goal what in
- let using = disambiguate_term status_ref goal using in
- GrafiteAst.ElimType (loc, what, Some using, depth, idents)
- | GrafiteAst.ElimType (loc, what, None, depth, idents) ->
- let what = disambiguate_term status_ref goal 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 goal 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 goal term in
- term :: to_what
- in
- let to_what = List.fold_right f to_what [] in
- let what = disambiguate_term status_ref goal 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 goal 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 goal 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 goal term in
- GrafiteAst.Transitivity (loc, cic)
- in
- status_ref, tactic