Permalink
Browse files

Fix extraction taking a type in the wrong environment.

Fix restriction of universe contexts to not forget about potentially useful
constraints.
  • Loading branch information...
1 parent af53364 commit ce11f55e27c8e4f98384aacd61ee67c593340195 @mattam82 mattam82 committed May 2, 2014
Showing with 23 additions and 8 deletions.
  1. +2 −0 kernel/sorts.ml
  2. +11 −2 library/universes.ml
  3. +8 −4 plugins/extraction/extraction.ml
  4. +2 −2 plugins/setoid_ring/Field_theory.v
View
@@ -47,10 +47,12 @@ let equal s1 s2 = Int.equal (compare s1 s2) 0
let is_prop = function
| Prop Null -> true
+ | Type u when Universe.equal Universe.type0m u -> true
| _ -> false
let is_set = function
| Prop Pos -> true
+ | Type u when Universe.equal Universe.type0 u -> true
| _ -> false
let is_small = function
View
@@ -691,13 +691,22 @@ let restrict_universe_context (univs,csts) s =
(* Universes that are not necessary to typecheck the term.
E.g. univs introduced by tactics and not used in the proof term. *)
let diff = LSet.diff univs s in
+ let is_useless l r =
+ let lmem = LSet.mem l diff
+ and rmem = LSet.mem r diff in
+ lmem && rmem
+ (* if lmem then *)
+ (* rmem || not (LSet.mem r univs) *)
+ (* else *)
+ (* rmem && not (LSet.mem l s) *)
+ in
let (univscstrs, csts) =
Constraint.fold
(fun (l,d,r as c) (univs, csts) ->
- if LSet.mem l diff && LSet.mem r diff then (univs, csts)
+ if is_useless l r then (univs, csts)
else (LSet.add l (LSet.add r univs), Constraint.add c csts))
csts (LSet.empty, Constraint.empty)
- in (LSet.union s (LSet.inter univs univscstrs), csts)
+ in (LSet.inter univs (LSet.union s univscstrs), csts)
let simplify_universe_context (univs,csts) =
let uf = UF.create () in
@@ -76,7 +76,7 @@ let rec flag_of_type env t : flag =
let t = whd_betadeltaiota env none t in
match kind_of_term t with
| Prod (x,t,c) -> flag_of_type (push_rel (x,None,t) env) c
- | Sort (Prop Null) -> (Logic,TypeScheme)
+ | Sort s when Sorts.is_prop s -> (Logic,TypeScheme)
| Sort _ -> (Info,TypeScheme)
| _ -> if (sort_of env t) == InProp then (Logic,Default) else (Info,Default)
@@ -206,7 +206,11 @@ let oib_equal o1 o2 =
match o1.mind_arity, o2.mind_arity with
| RegularArity {mind_user_arity=c1; mind_sort=s1}, RegularArity {mind_user_arity=c2; mind_sort=s2} ->
eq_constr c1 c2 && Sorts.equal s1 s2
- | _ -> false
+ | TemplateArity p1, TemplateArity p2 ->
+ let eq o1 o2 = Option.equal Univ.Universe.equal o1 o2 in
+ List.equal eq p1.template_param_levels p2.template_param_levels &&
+ Univ.Universe.equal p1.template_level p2.template_level
+ | _, _ -> false
end &&
Array.equal Id.equal o1.mind_consnames o2.mind_consnames
@@ -976,7 +980,7 @@ let extract_fixpoint env vkn (fi,ti,ci) =
let extract_constant env kn cb =
let r = ConstRef kn in
- let typ = Global.type_of_global_unsafe r in
+ let typ = Typeops.type_of_constant_type env cb.const_type in
let warn_info () = if not (is_custom r) then add_info_axiom r in
let warn_log () = if not (constant_has_body cb) then add_log_axiom r
in
@@ -1023,7 +1027,7 @@ let extract_constant env kn cb =
let extract_constant_spec env kn cb =
let r = ConstRef kn in
- let typ = Global.type_of_global_unsafe r in
+ let typ = Typeops.type_of_constant_type env cb.const_type in
match flag_of_type env typ with
| (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype))
| (Logic, Default) -> Sval (r, Tdummy Kother)
@@ -588,13 +588,13 @@ Qed.
(** Smart constructors for polynomial expression,
with reduction of constants *)
-Time Definition NPEadd e1 e2 :=
+Definition NPEadd e1 e2 :=
match e1, e2 with
| PEc c1, PEc c2 => PEc (c1 + c2)
| PEc c, _ => if (c =? 0)%coef then e2 else e1 + e2
| _, PEc c => if (c =? 0)%coef then e1 else e1 + e2
(* Peut t'on factoriser ici ??? *)
- | _, _ => (@PEadd C e1 e2)
+ | _, _ => (e1 + e2)
end%poly.
Infix "++" := NPEadd (at level 60, right associativity).

0 comments on commit ce11f55

Please sign in to comment.