Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Ability to declare definition forced at specific object #7

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

Ability to declare definition forced at specific object #7

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 8 additions & 2 deletions src/fPlugin.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -306,7 +306,7 @@ let force_translate (obj, hom) gr ids =

(** Implementation in the forcing layer *)

let force_implement (obj, hom) id typ idopt =
let force_implement (obj, hom) id typ idopt fromopt =
let env = Global.env () in
let obj = Universes.constr_of_global (Nametab.global obj) in
let hom = Universes.constr_of_global (Nametab.global hom) in
Expand All @@ -322,7 +322,13 @@ let force_implement (obj, hom) id typ idopt =
let sigma = Evd.from_env env in
let (typ, uctx) = Constrintern.interp_type env sigma typ in
let sigma = Evd.from_ctx uctx in
let (sigma, typ_) = FTranslate.translate_type !translator cat env sigma typ in
let (sigma, typ_) = match fromopt with
| None -> FTranslate.translate_type !translator cat env sigma typ
| Some from -> let (from, uctx) = Constrintern.interp_casted_constr env sigma from obj in
let sigma = Evd.from_ctx uctx in
let (sigma, typ_) = FTranslate.translate_type ~toplevel:false !translator cat env sigma typ in
sigma, Vars.subst1 from typ_
in
let (sigma, _) = Typing.type_of env sigma typ_ in
let hook _ dst =
(** Declare the original term as an axiom *)
Expand Down
2 changes: 1 addition & 1 deletion src/fPlugin.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,4 +6,4 @@ val force_tac : FTranslate.category -> Constr.t -> unit tactic

val force_translate : (reference * reference) -> reference -> Id.t list option -> unit

val force_implement : (reference * reference) -> Id.t -> Constrexpr.constr_expr -> Id.t option -> unit
val force_implement : (reference * reference) -> Id.t -> Constrexpr.constr_expr -> Id.t option -> Constrexpr.constr_expr option -> unit
10 changes: 7 additions & 3 deletions src/g_forcing.ml4
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,11 @@ let classify_impl _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacit

VERNAC COMMAND EXTEND ForcingImplementation CLASSIFIED BY classify_impl
| [ "Forcing" "Definition" ident(id) ":" lconstr(typ) "using" global(obj) global(hom) ] ->
[ FPlugin.force_implement (obj, hom) id typ None ]
| [ "Forcing" "Definition" ident(id) ":" lconstr(typ) "as" ident(id') "using" global(obj) global(hom) ] ->
[ FPlugin.force_implement (obj, hom) id typ (Some id') ]
[ FPlugin.force_implement (obj, hom) id typ None None ]
| [ "Forcing" "Definition" ident(id) ":" lconstr(typ) "as" ident(id') "using" global(obj) global(hom)] ->
[ FPlugin.force_implement (obj, hom) id typ (Some id') None ]
| [ "Forcing" "Definition" ident(id) ":" lconstr(typ) "using" global(obj) global(hom) "from" constr(c)] ->
[ FPlugin.force_implement (obj, hom) id typ None (Some c) ]
| [ "Forcing" "Definition" ident(id) ":" lconstr(typ) "as" ident(id') "using" global(obj) global(hom) "from" constr(c)] ->
[ FPlugin.force_implement (obj, hom) id typ (Some id') (Some c) ]
END