Permalink
Browse files

Defined later as a new operator.

  • Loading branch information...
1 parent 941a60d commit 58e03eb56495162579c569c9d320c42140653004 @mattam82 committed Feb 20, 2012
Showing with 58 additions and 53 deletions.
  1. +27 −21 src/forcing.ml4
  2. +31 −32 test-suite/Basics.v
View
@@ -310,8 +310,6 @@ module Forcing(F : ForcingCond) = struct
[return (mkProd (Anonymous, mkApp (coq_subp, [| p |]), new_Type ()));
mk_appc coq_transport [return p]; a; b]
-
-
let rec trans (c : constr) : constr forcing_term =
let pn = next_p () in
let p = mk_var pn in
@@ -446,27 +444,32 @@ module Forcing(F : ForcingCond) = struct
| _ -> assert false)
| c -> Glob_term.map_glob_constr meta_to_holes c
- let translate c env sigma =
+ let interpretation c sigma =
+ let pn = next_p () in let p = mk_var pn in
+ let inter = interp (simpl (mk_app (trans c) [p]) sigma) p in
+ mk_cond_prod pn (return condition_type) inter sigma
+
+ let translate tr c env sigma =
clear_p (); clear_q (); clear_r (); clear_s (); clear_f (); clear_anon (); clear_ty ();
- let c' = trans c [] in
+ let c' = tr c [] in
let sigma, c' = named_to_nameless env sigma c' in
let dt = Detyping.detype true [] [] c' in
let dt = meta_to_holes dt in
sigma, dt
let tac i c = fun gs ->
let env = pf_env gs and sigma = Refiner.project gs in
- let evars, term' = translate c env sigma in
+ let evars, term' = translate trans c env sigma in
let evs = ref evars in
let term'', ty = Subtac_pretyping.interp env evs term' None in
tclTHEN (tclEVARS !evs)
(letin_tac None (Name i) term'' None onConcl) gs
(** Define [id] as the translation of [c] (with term and restriction map) *)
- let command id ?hook c =
+ let command id tr ?hook c =
let env = Global.env () and sigma = Evd.empty in
let c = Constrintern.interp_constr sigma env c in
- let evars, term' = translate c env sigma in
+ let evars, term' = translate tr c env sigma in
let evs = ref evars in
let term'', ty = Subtac_pretyping.interp env evs term' None in
let evm' = Subtac_utils.evars_of_term !evs Evd.empty term'' in
@@ -478,28 +481,31 @@ module Forcing(F : ForcingCond) = struct
open Decl_kinds
open Global
+ let reference_of_global g =
+ Qualid (dummy_loc, Nametab.shortest_qualid_of_global Idset.empty g)
+
let forcing_operator id c =
let hook ty _ gr =
+ let env = Global.env () in
let ax =
Declare.declare_constant id (ParameterEntry (None, ty, None), IsAssumption Logical)
in
+ let trty = constr_of_global gr in
+ let evars, ev = Evarutil.new_evar Evd.empty env trty in
let body, types =
Typeclasses.instance_constructor forcing_class
- [ty; mkConst ax; type_of_global gr; constr_of_global gr]
- in
- let ce =
- { const_entry_body = Option.get body;
- const_entry_secctx = None;
- const_entry_type = Some types;
- const_entry_opaque = false }
+ [ty; mkConst ax; trty; ev]
in
- let inst =
- Declare.declare_constant (add_suffix id "_inst")
- (DefinitionEntry ce, IsDefinition Instance)
+ let id' = add_suffix id "_inst" in
+ let evars, _, def, ty =
+ Eterm.eterm_obligations env id' evars evars 0 (Option.get body) types
in
- Typeclasses.add_instance
- (Typeclasses.new_instance forcing_class None false (ConstRef inst))
- in command (add_suffix id "_trans") c ~hook
+ ignore (Subtac_obligations.add_definition id' ~term:def
+ ~hook:(fun loc gr ->
+ Typeclasses.add_instance
+ (Typeclasses.new_instance forcing_class None false gr))
+ ty evars)
+ in command (add_suffix id "_trans") interpretation c ~hook
end
@@ -523,5 +529,5 @@ VERNAC COMMAND EXTEND Forcing_operator
END
VERNAC COMMAND EXTEND Force
-[ "Force" ident(i) ":=" constr(c) ] -> [ NatForcing.command i c ]
+[ "Force" ident(i) ":=" constr(c) ] -> [ NatForcing.command i NatForcing.trans c ]
END
View
@@ -31,31 +31,22 @@ Hint Extern 2 (_ <= _) => forcing_le : forcing.
Set Printing Existential Instances.
Print HintDb forcing.
-Forcing Operator later : (Type -> Type).
-
-Print later_trans.
-
-Program Definition embed (p : P) : subp p := p.
-
Program Definition later_sheaf_f {p : nat} (q : subp p) (T : sheaf q) : subp q -> Type :=
fun r =>
match r with
| 0 => unit
| S r' => sheaf_f T r'
end.
-Next Obligation. unfold le. destruct r. simpl in *. subst x. auto with arith. Qed.
-
-Program Definition later_def (p : nat) : projT1 (later_trans p) (embed p) :=
- λ q : subp p, λ T : sheaf q,
- let val : transport (later_sheaf_f q T) :=
- λ (r : subp q) (t : subp r) (M : later_sheaf_f q T r),
- let (tn, tprf) return later_sheaf_f q T (ι t) := t in
- match tn return forall prf : tn <= r, later_sheaf_f q T (ι (exist tn prf)) with
- | 0 => fun _ => tt
- | S t' => fun _ => Θ T (pred r) t' _
- end tprf
- in existT (later_sheaf_f q T) val.
-
+Next Obligation of later_sheaf_f. unfold le. destruct r. simpl in *. subst x. auto with arith. Qed.
+
+Program Definition later_transp {p} (q : subp p) (T : sheaf q) : transport (later_sheaf_f q T) :=
+ λ (r : subp q) (t : subp r) (M : later_sheaf_f q T r),
+ let (tn, tprf) return later_sheaf_f q T (ι t) := t in
+ match tn return forall prf : tn <= r, later_sheaf_f q T (ι (exist tn prf)) with
+ | 0 => fun _ => tt
+ | S t' => fun _ => Θ T (pred r) t' _
+ end tprf.
+
Next Obligation. intros. destruct r, t. simpl in *. unfold le in *. eauto with arith. Defined.
Next Obligation. intros. destruct r. simpl in *. unfold le in *. destruct x; eauto with arith. Defined.
Next Obligation. destruct r. simpl in *. unfold le in *. clear_subset_proofs. red in M.
@@ -66,25 +57,33 @@ Defined.
Next Obligation. unfold ι. simpl. pi. Defined.
-Next Obligation. split; red; intros.
-
- unfold ι, ι_refl, ι_ι_refl. simpl. destruct q0. simpl in *.
- rewrite eq_trans_eq_refl_l.
- rewrite eq_rect_f_equal.
- clear_subset_proofs.
- abstract_eq_proofs.
- simpl in M. destruct x; simpl in *. elimtype False. depelim H.
+Program Definition embed (p : P) : subp p := p.
- revert M; clear_subset_proofs. unfold le in *. clear_subset_proofs. trivial.
+Forcing Operator later : (Type -> Type).
+
+Next Obligation.
+ red. intros.
+ assert(forall p (q : subp p) (T : sheaf q), refl (later_transp q T) /\ trans (later_transp q T)). admit.
+ refine (exist (λ q : subp p, λ T : sheaf q,
+ existT (later_sheaf_f q T) (exist (later_transp q T) (H p q T))) _).
+ admit.
Defined.
- intros.
-
- red in M. destruct x; simpl in *. red in M. destruct T. simpl in *.
+Print later_trans.
+
+
+
+Next Obligation. admit. Defined.
+Next Obligation. clear_subset_proofs. admit. Defined.
+
+Program Definition later_def (p : nat) : projT1 (later_trans p) (embed p) :=
+ λ q : subp p, λ T : sheaf q,
+ existT (later_sheaf_f q T) (later_transp q T).
+Next Obligation. admit. Defined.
+Next Obligation. clear_subset_proofs. admit. Defined.
-red. simpl.
Time Force foo := (forall X : Set, X).

0 comments on commit 58e03eb

Please sign in to comment.