-let coercion_moo_statement_of uri =
- GrafiteAst.Coercion (HExtlib.dummy_floc, uri, false)
-
-let refinement_toolkit = {
- RefinementTool.type_of_aux' =
- (fun ?localization_tbl e c t u ->
- let saved = !CicRefine.insert_coercions in
- CicRefine.insert_coercions:= false;
- let rc =
- try
- let t, ty, metasenv, ugraph =
- CicRefine.type_of_aux' ?localization_tbl e c t u in
- RefinementTool.Success (t, ty, metasenv, ugraph)
- with
- | CicRefine.RefineFailure s
- | CicRefine.Uncertain s
- | CicRefine.AssertFailure s -> RefinementTool.Exception s
- in
- CicRefine.insert_coercions := saved;
- rc);
- RefinementTool.ppsubst = CicMetaSubst.ppsubst;
- RefinementTool.apply_subst = CicMetaSubst.apply_subst;
- RefinementTool.ppmetasenv = CicMetaSubst.ppmetasenv;
- RefinementTool.pack_coercion_obj = CicRefine.pack_coercion_obj;
- }
-
-let eval_coercion status ~add_composites uri =
- let basedir = Helm_registry.get "matita.basedir" in
- let status,compounds =
- prerr_endline "evaluating a coercion command";
- GrafiteSync.add_coercion ~basedir ~add_composites refinement_toolkit status uri in
- let moo_content = coercion_moo_statement_of uri in
- let status = GrafiteTypes.add_moo_content [moo_content] status in
- {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof},
- compounds
-
-let eval_tactical ~disambiguate_tactic status tac =
- let apply_tactic = apply_tactic ~disambiguate_tactic in
- let module MatitaStatus =
- struct
- type input_status = GrafiteTypes.status * ProofEngineTypes.goal
-
- type output_status =
- GrafiteTypes.status * ProofEngineTypes.goal list * ProofEngineTypes.goal list
-
- type tactic = input_status -> output_status
-
- let id_tactic = apply_tactic (GrafiteAst.IdTac HExtlib.dummy_floc)
- let mk_tactic tac = tac
- let apply_tactic tac = tac
- let goals (_, opened, closed) = opened, closed
- let set_goals (opened, closed) (status, _, _) = (status, opened, closed)
- let get_stack (status, _) = GrafiteTypes.get_stack status
-
- let set_stack stack (status, opened, closed) =
- GrafiteTypes.set_stack stack status, opened, closed
-
- let inject (status, _) = (status, [], [])
- let focus goal (status, _, _) = (status, goal)
- end
- in
- let module MatitaTacticals = Tacticals.Make (MatitaStatus) in
- let rec tactical_of_ast l tac =
- match tac with
- | GrafiteAst.Tactic (loc, tactic) ->
- MatitaTacticals.tactic (MatitaStatus.mk_tactic (apply_tactic tactic))
- | GrafiteAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
- assert (l > 0);
- MatitaTacticals.seq ~tactics:(List.map (tactical_of_ast (l+1)) tacticals)
- | GrafiteAst.Do (loc, n, tactical) ->
- MatitaTacticals.do_tactic ~n ~tactic:(tactical_of_ast (l+1) tactical)
- | GrafiteAst.Repeat (loc, tactical) ->
- MatitaTacticals.repeat_tactic ~tactic:(tactical_of_ast (l+1) tactical)
- | GrafiteAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
- assert (l > 0);
- MatitaTacticals.thens ~start:(tactical_of_ast (l+1) tactical)
- ~continuations:(List.map (tactical_of_ast (l+1)) tacticals)
- | GrafiteAst.First (loc, tacticals) ->
- MatitaTacticals.first
- ~tactics:(List.map (fun t -> "", tactical_of_ast (l+1) t) tacticals)
- | GrafiteAst.Try (loc, tactical) ->
- MatitaTacticals.try_tactic ~tactic:(tactical_of_ast (l+1) tactical)
- | GrafiteAst.Solve (loc, tacticals) ->
- MatitaTacticals.solve_tactics
- ~tactics:(List.map (fun t -> "", tactical_of_ast (l+1) t) tacticals)
-
- | GrafiteAst.Skip loc -> MatitaTacticals.skip
- | GrafiteAst.Dot loc -> MatitaTacticals.dot
- | GrafiteAst.Semicolon loc -> MatitaTacticals.semicolon
- | GrafiteAst.Branch loc -> MatitaTacticals.branch
- | GrafiteAst.Shift loc -> MatitaTacticals.shift
- | GrafiteAst.Pos (loc, i) -> MatitaTacticals.pos i
- | GrafiteAst.Merge loc -> MatitaTacticals.merge
- | GrafiteAst.Focus (loc, goals) -> MatitaTacticals.focus goals
- | GrafiteAst.Unfocus loc -> MatitaTacticals.unfocus