From a42795cc1c2a8ed3efa9960af920ff7b16d928f0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 1 Sep 2016 17:52:44 +0200
Subject: Introducing a new EConstr.t type to perform the nf_evar operation on
 demand.

---
 engine/eConstr.ml | 614 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 614 insertions(+)
 create mode 100644 engine/eConstr.ml

(limited to 'engine/eConstr.ml')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
new file mode 100644
index 0000000000..0a5f1ba685
--- /dev/null
+++ b/engine/eConstr.ml
@@ -0,0 +1,614 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open CSig
+open CErrors
+open Util
+open Names
+open Term
+open Context
+open Evd
+
+module API :
+sig
+type t
+val kind : Evd.evar_map -> t -> (t, t) Constr.kind_of_term
+val kind_upto : Evd.evar_map -> constr -> (constr, types) Constr.kind_of_term
+val of_kind : (t, t) Constr.kind_of_term -> t
+val of_constr : Constr.t -> t
+val unsafe_to_constr : t -> Constr.t
+val unsafe_eq : (t, Constr.t) eq
+end =
+struct
+
+type t = Constr.t
+
+let safe_evar_value sigma ev =
+  try Some (Evd.existential_value sigma ev)
+  with NotInstantiatedEvar | Not_found -> None
+
+let rec kind sigma c =
+  let c0 = Constr.kind c in
+  match c0 with
+  | Evar (evk, args) ->
+    (match safe_evar_value sigma (evk, args) with
+        Some c -> kind sigma c
+      | None -> c0)
+  | Sort (Type u) ->
+    let u' = Evd.normalize_universe sigma u in
+    if u' == u then c0 else Sort (Type u')
+  | Const (c', u) when not (Univ.Instance.is_empty u) ->
+    let u' = Evd.normalize_universe_instance sigma u in
+    if u' == u then c0 else Const (c', u')
+  | Ind (i, u) when not (Univ.Instance.is_empty u) ->
+    let u' = Evd.normalize_universe_instance sigma u in
+    if u' == u then c0 else Ind (i, u')
+  | Construct (co, u) when not (Univ.Instance.is_empty u) ->
+    let u' = Evd.normalize_universe_instance sigma u in
+    if u' == u then c0 else Construct (co, u')
+  | App (c, args) when isEvar c ->
+    (** Enforce smart constructor invariant on applications *)
+    let ev = destEvar c in
+    begin match safe_evar_value sigma ev with
+    | None -> c0
+    | Some c -> kind sigma (mkApp (c, args))
+    end
+  | _ -> c0
+
+let kind_upto = kind
+let of_kind = Constr.of_kind
+let of_constr c = c
+let unsafe_to_constr c = c
+let unsafe_eq = Refl
+
+end
+
+include API
+
+type types = t
+type constr = t
+type existential = t pexistential
+type fixpoint = (t, t) pfixpoint
+type cofixpoint = (t, t) pcofixpoint
+
+let mkProp = of_kind (Sort Sorts.prop)
+let mkSet = of_kind (Sort Sorts.set)
+let mkType u = of_kind (Sort (Sorts.Type u))
+let mkRel n = of_kind (Rel n)
+let mkVar id = of_kind (Var id)
+let mkMeta n = of_kind (Meta n)
+let mkEvar e = of_kind (Evar e)
+let mkSort s = of_kind (Sort s)
+let mkCast (b, k, t) = of_kind (Cast (b, k, t))
+let mkProd (na, t, u) = of_kind (Prod (na, t, u))
+let mkLambda (na, t, c) = of_kind (Lambda (na, t, c))
+let mkLetIn (na, b, t, c) = of_kind (LetIn (na, b, t, c))
+let mkApp (f, arg) = of_kind (App (f, arg))
+let mkConstU pc = of_kind (Const pc)
+let mkIndU pi = of_kind (Ind pi)
+let mkConstructU pc = of_kind (Construct pc)
+let mkCase (ci, c, r, p) = of_kind (Case (ci, c, r, p))
+let mkFix f = of_kind (Fix f)
+let mkCoFix f = of_kind (CoFix f)
+let mkProj (p, c) = of_kind (Proj (p, c))
+
+let applist (f, arg) = mkApp (f, Array.of_list arg)
+
+let isRel sigma c = match kind sigma c with Rel _ -> true | _ -> false
+let isVar sigma c = match kind sigma c with Var _ -> true | _ -> false
+let isInd sigma c = match kind sigma c with Ind _ -> true | _ -> false
+let isEvar sigma c = match kind sigma c with Evar _ -> true | _ -> false
+let isMeta sigma c = match kind sigma c with Meta _ -> true | _ -> false
+let isSort sigma c = match kind sigma c with Sort _ -> true | _ -> false
+let isCast sigma c = match kind sigma c with Cast _ -> true | _ -> false
+let isApp sigma c = match kind sigma c with App _ -> true | _ -> false
+let isLambda sigma c = match kind sigma c with Lambda _ -> true | _ -> false
+let isLetIn sigma c = match kind sigma c with LetIn _ -> true | _ -> false
+let isProd sigma c = match kind sigma c with Prod _ -> true | _ -> false
+let isConst sigma c = match kind sigma c with Const _ -> true | _ -> false
+let isConstruct sigma c = match kind sigma c with Construct _ -> true | _ -> false
+let isFix sigma c = match kind sigma c with Fix _ -> true | _ -> false
+let isCoFix sigma c = match kind sigma c with CoFix _ -> true | _ -> false
+let isCase sigma c = match kind sigma c with Case _ -> true | _ -> false
+let isProj sigma c = match kind sigma c with Proj _ -> true | _ -> false
+let isVarId sigma id c =
+  match kind sigma c with Var id' -> Id.equal id id' | _ -> false
+
+let destRel sigma c = match kind sigma c with
+| Rel p -> p
+| _ -> raise DestKO
+
+let destVar sigma c = match kind sigma c with
+| Var p -> p
+| _ -> raise DestKO
+
+let destInd sigma c = match kind sigma c with
+| Ind p -> p
+| _ -> raise DestKO
+
+let destEvar sigma c = match kind sigma c with
+| Evar p -> p
+| _ -> raise DestKO
+
+let destMeta sigma c = match kind sigma c with
+| Meta p -> p
+| _ -> raise DestKO
+
+let destSort sigma c = match kind sigma c with
+| Sort p -> p
+| _ -> raise DestKO
+
+let destCast sigma c = match kind sigma c with
+| Cast (c, k, t) -> (c, k, t)
+| _ -> raise DestKO
+
+let destApp sigma c = match kind sigma c with
+| App (f, a) -> (f, a)
+| _ -> raise DestKO
+
+let destLambda sigma c = match kind sigma c with
+| Lambda (na, t, c) -> (na, t, c)
+| _ -> raise DestKO
+
+let destLetIn sigma c = match kind sigma c with
+| LetIn (na, b, t, c) -> (na, b, t, c)
+| _ -> raise DestKO
+
+let destProd sigma c = match kind sigma c with
+| Prod (na, t, c) -> (na, t, c)
+| _ -> raise DestKO
+
+let destConst sigma c = match kind sigma c with
+| Const p -> p
+| _ -> raise DestKO
+
+let destConstruct sigma c = match kind sigma c with
+| Construct p -> p
+| _ -> raise DestKO
+
+let destFix sigma c = match kind sigma c with
+| Fix p -> p
+| _ -> raise DestKO
+
+let destCoFix sigma c = match kind sigma c with
+| CoFix p -> p
+| _ -> raise DestKO
+
+let destCase sigma c = match kind sigma c with
+| Case (ci, t, c, p) -> (ci, t, c, p)
+| _ -> raise DestKO
+
+let destProj sigma c = match kind sigma c with
+| Proj (p, c) -> (p, c)
+| _ -> raise DestKO
+
+let decompose_app sigma c =
+  match kind sigma c with
+    | App (f,cl) -> (f, Array.to_list cl)
+    | _ -> (c,[])
+
+let local_assum (na, t) =
+  let open Rel.Declaration in
+  LocalAssum (na, unsafe_to_constr t)
+
+let local_def (na, b, t) =
+  let open Rel.Declaration in
+  LocalDef (na, unsafe_to_constr b, unsafe_to_constr t)
+
+let decompose_lam sigma c =
+  let rec lamdec_rec l c = match kind sigma c with
+    | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) c
+    | Cast (c,_,_)     -> lamdec_rec l c
+    | _                -> l,c
+  in
+  lamdec_rec [] c
+
+let decompose_lam_assum sigma c =
+  let rec lamdec_rec l c =
+    match kind sigma c with
+    | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (local_assum (x,t)) l) c
+    | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (local_def (x,b,t)) l) c
+    | Cast (c,_,_)      -> lamdec_rec l c
+    | _               -> l,c
+  in
+  lamdec_rec Context.Rel.empty c
+
+let decompose_lam_n_assum sigma n c =
+  if n < 0 then
+    error "decompose_lam_n_assum: integer parameter must be positive";
+  let rec lamdec_rec l n c =
+    if Int.equal n 0 then l,c
+    else
+      match kind sigma c with
+      | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (local_assum (x,t)) l) (n-1) c
+      | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (local_def (x,b,t)) l) n c
+      | Cast (c,_,_)      -> lamdec_rec l n c
+      | c -> error "decompose_lam_n_assum: not enough abstractions"
+  in
+  lamdec_rec Context.Rel.empty n c
+
+let decompose_lam_n_decls sigma n =
+  if n < 0 then
+    error "decompose_lam_n_decls: integer parameter must be positive";
+  let rec lamdec_rec l n c =
+    if Int.equal n 0 then l,c
+    else
+      match kind sigma c with
+      | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (local_assum (x,t)) l) (n-1) c
+      | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (local_def (x,b,t)) l) (n-1) c
+      | Cast (c,_,_)      -> lamdec_rec l n c
+      | c -> error "decompose_lam_n_decls: not enough abstractions"
+  in
+  lamdec_rec Context.Rel.empty n
+
+let decompose_prod sigma c =
+  let rec proddec_rec l c = match kind sigma c with
+    | Prod (x,t,c) -> proddec_rec ((x,t)::l) c
+    | Cast (c,_,_)     -> proddec_rec l c
+    | _                -> l,c
+  in
+  proddec_rec [] c
+
+let decompose_prod_assum sigma c =
+  let rec proddec_rec l c =
+    match kind sigma c with
+    | Prod (x,t,c)  -> proddec_rec (Context.Rel.add (local_assum (x,t)) l) c
+    | LetIn (x,b,t,c) -> proddec_rec (Context.Rel.add (local_def (x,b,t)) l) c
+    | Cast (c,_,_)      -> proddec_rec l c
+    | _               -> l,c
+  in
+  proddec_rec Context.Rel.empty c
+
+let decompose_prod_n_assum sigma n c =
+  if n < 0 then
+    error "decompose_prod_n_assum: integer parameter must be positive";
+  let rec prodec_rec l n c =
+    if Int.equal n 0 then l,c
+    else
+      match kind sigma c with
+      | Prod (x,t,c)    -> prodec_rec (Context.Rel.add (local_assum (x,t)) l) (n-1) c
+      | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (local_def (x,b,t)) l) (n-1) c
+      | Cast (c,_,_)      -> prodec_rec l n c
+      | c -> error "decompose_prod_n_assum: not enough assumptions"
+  in
+  prodec_rec Context.Rel.empty n c
+
+let existential_type sigma (evk, args) =
+  of_constr (existential_type sigma (evk, Array.map unsafe_to_constr args))
+
+let map sigma f c = match kind sigma c with
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+    | Construct _) -> c
+  | Cast (b,k,t) ->
+      let b' = f b in
+      let t' = f t in
+      if b'==b && t' == t then c
+      else mkCast (b', k, t')
+  | Prod (na,t,b) ->
+      let b' = f b in
+      let t' = f t in
+      if b'==b && t' == t then c
+      else mkProd (na, t', b')
+  | Lambda (na,t,b) ->
+      let b' = f b in
+      let t' = f t in
+      if b'==b && t' == t then c
+      else mkLambda (na, t', b')
+  | LetIn (na,b,t,k) ->
+      let b' = f b in
+      let t' = f t in
+      let k' = f k in
+      if b'==b && t' == t && k'==k then c
+      else mkLetIn (na, b', t', k')
+  | App (b,l) ->
+      let b' = f b in
+      let l' = Array.smartmap f l in
+      if b'==b && l'==l then c
+      else mkApp (b', l')
+  | Proj (p,t) ->
+      let t' = f t in
+      if t' == t then c
+      else mkProj (p, t')
+  | Evar (e,l) ->
+      let l' = Array.smartmap f l in
+      if l'==l then c
+      else mkEvar (e, l')
+  | Case (ci,p,b,bl) ->
+      let b' = f b in
+      let p' = f p in
+      let bl' = Array.smartmap f bl in
+      if b'==b && p'==p && bl'==bl then c
+      else mkCase (ci, p', b', bl')
+  | Fix (ln,(lna,tl,bl)) ->
+      let tl' = Array.smartmap f tl in
+      let bl' = Array.smartmap f bl in
+      if tl'==tl && bl'==bl then c
+      else mkFix (ln,(lna,tl',bl'))
+  | CoFix(ln,(lna,tl,bl)) ->
+      let tl' = Array.smartmap f tl in
+      let bl' = Array.smartmap f bl in
+      if tl'==tl && bl'==bl then c
+      else mkCoFix (ln,(lna,tl',bl'))
+
+let map_with_binders sigma g f l c0 = match kind sigma c0 with
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+    | Construct _) -> c0
+  | Cast (c, k, t) ->
+    let c' = f l c in
+    let t' = f l t in
+    if c' == c && t' == t then c0
+    else mkCast (c', k, t')
+  | Prod (na, t, c) ->
+    let t' = f l t in
+    let c' = f (g l) c in
+    if t' == t && c' == c then c0
+    else mkProd (na, t', c')
+  | Lambda (na, t, c) ->
+    let t' = f l t in
+    let c' = f (g l) c in
+    if t' == t && c' == c then c0
+    else mkLambda (na, t', c')
+  | LetIn (na, b, t, c) ->
+    let b' = f l b in
+    let t' = f l t in
+    let c' = f (g l) c in
+    if b' == b && t' == t && c' == c then c0
+    else mkLetIn (na, b', t', c')
+  | App (c, al) ->
+    let c' = f l c in
+    let al' = CArray.Fun1.smartmap f l al in
+    if c' == c && al' == al then c0
+    else mkApp (c', al')
+  | Proj (p, t) ->
+    let t' = f l t in
+    if t' == t then c0
+    else mkProj (p, t')
+  | Evar (e, al) ->
+    let al' = CArray.Fun1.smartmap f l al in
+    if al' == al then c0
+    else mkEvar (e, al')
+  | Case (ci, p, c, bl) ->
+    let p' = f l p in
+    let c' = f l c in
+    let bl' = CArray.Fun1.smartmap f l bl in
+    if p' == p && c' == c && bl' == bl then c0
+    else mkCase (ci, p', c', bl')
+  | Fix (ln, (lna, tl, bl)) ->
+    let tl' = CArray.Fun1.smartmap f l tl in
+    let l' = iterate g (Array.length tl) l in
+    let bl' = CArray.Fun1.smartmap f l' bl in
+    if tl' == tl && bl' == bl then c0
+    else mkFix (ln,(lna,tl',bl'))
+  | CoFix(ln,(lna,tl,bl)) ->
+    let tl' = CArray.Fun1.smartmap f l tl in
+    let l' = iterate g (Array.length tl) l in
+    let bl' = CArray.Fun1.smartmap f l' bl in
+    mkCoFix (ln,(lna,tl',bl'))
+
+let iter sigma f c = match kind sigma c with
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+    | Construct _) -> ()
+  | Cast (c,_,t) -> f c; f t
+  | Prod (_,t,c) -> f t; f c
+  | Lambda (_,t,c) -> f t; f c
+  | LetIn (_,b,t,c) -> f b; f t; f c
+  | App (c,l) -> f c; Array.iter f l
+  | Proj (p,c) -> f c
+  | Evar (_,l) -> Array.iter f l
+  | Case (_,p,c,bl) -> f p; f c; Array.iter f bl
+  | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
+  | CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
+
+let iter_with_full_binders sigma g f n c = match kind sigma c with
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+    | Construct _) -> ()
+  | Cast (c,_,t) -> f n c; f n t
+  | Prod (na,t,c) -> f n t; f (g (local_assum (na, t)) n) c
+  | Lambda (na,t,c) -> f n t; f (g (local_assum (na, t)) n) c
+  | LetIn (na,b,t,c) -> f n b; f n t; f (g (local_def (na, b, t)) n) c
+  | App (c,l) -> f n c; CArray.Fun1.iter f n l
+  | Evar (_,l) -> CArray.Fun1.iter f n l
+  | Case (_,p,c,bl) -> f n p; f n c; CArray.Fun1.iter f n bl
+  | Proj (p,c) -> f n c
+  | Fix (_,(lna,tl,bl)) ->
+    Array.iter (f n) tl;
+    let n' = Array.fold_left2 (fun n na t -> g (local_assum (na,t)) n) n lna tl in
+    Array.iter (f n') bl
+  | CoFix (_,(lna,tl,bl)) ->
+    Array.iter (f n) tl;
+    let n' = Array.fold_left2 (fun n na t -> g (local_assum (na,t)) n) n lna tl in
+    Array.iter (f n') bl
+
+let iter_with_binders sigma g f n c =
+  iter_with_full_binders sigma (fun _ acc -> g acc) f n c
+
+let fold sigma f acc c = match kind sigma c with
+  | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
+    | Construct _) -> acc
+  | Cast (c,_,t) -> f (f acc c) t
+  | Prod (_,t,c) -> f (f acc t) c
+  | Lambda (_,t,c) -> f (f acc t) c
+  | LetIn (_,b,t,c) -> f (f (f acc b) t) c
+  | App (c,l) -> Array.fold_left f (f acc c) l
+  | Proj (p,c) -> f acc c
+  | Evar (_,l) -> Array.fold_left f acc l
+  | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl
+  | Fix (_,(lna,tl,bl)) ->
+    Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
+  | CoFix (_,(lna,tl,bl)) ->
+    Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
+
+let to_constr sigma t =
+  let rec map c = Constr.map map (Constr.of_kind (kind_upto sigma c)) in
+  map (unsafe_to_constr t)
+
+let compare_gen k eq_inst eq_sort eq_constr c1 c2 =
+  (c1 == c2) || Constr.compare_head_gen_with k k eq_inst eq_sort eq_constr c1 c2
+
+let eq_constr sigma c1 c2 =
+  let kind c = kind_upto sigma c in
+  let rec eq_constr c1 c2 =
+    compare_gen kind (fun _ -> Univ.Instance.equal) Sorts.equal eq_constr c1 c2
+  in
+  eq_constr (unsafe_to_constr c1) (unsafe_to_constr c2)
+
+let eq_constr_nounivs sigma c1 c2 =
+  let kind c = kind_upto sigma c in
+  let rec eq_constr c1 c2 =
+    compare_gen kind (fun _ _ _ -> true) (fun _ _ -> true) eq_constr c1 c2
+  in
+  eq_constr (unsafe_to_constr c1) (unsafe_to_constr c2)
+
+(** TODO: factorize with universes.ml *)
+let test_constr_universes sigma leq m n =
+  let open Universes in
+  let kind c = kind_upto sigma c in
+  if m == n then Some Constraints.empty
+  else 
+    let cstrs = ref Constraints.empty in
+    let eq_universes strict l l' = 
+      cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in
+    let eq_sorts s1 s2 = 
+      if Sorts.equal s1 s2 then true
+      else (cstrs := Constraints.add 
+	      (Sorts.univ_of_sort s1,UEq,Sorts.univ_of_sort s2) !cstrs; 
+	    true)
+    in
+    let leq_sorts s1 s2 = 
+      if Sorts.equal s1 s2 then true
+      else 
+	(cstrs := Constraints.add 
+	   (Sorts.univ_of_sort s1,ULe,Sorts.univ_of_sort s2) !cstrs; 
+	 true)
+    in
+    let rec eq_constr' m n = compare_gen kind eq_universes eq_sorts eq_constr' m n in
+    let res =
+      if leq then
+        let rec compare_leq m n =
+          Constr.compare_head_gen_leq_with kind kind eq_universes leq_sorts eq_constr' leq_constr' m n
+        and leq_constr' m n = m == n || compare_leq m n in
+        compare_leq m n
+      else
+        Constr.compare_head_gen_with kind kind eq_universes eq_sorts eq_constr' m n
+    in
+    if res then Some !cstrs else None
+
+let eq_constr_universes sigma m n =
+  test_constr_universes sigma false (unsafe_to_constr m) (unsafe_to_constr n)
+let leq_constr_universes sigma m n =
+  test_constr_universes sigma true (unsafe_to_constr m) (unsafe_to_constr n)
+
+let compare_head_gen_proj env sigma equ eqs eqc' m n =
+  let kind c = kind_upto sigma c in
+  match kind_upto sigma m, kind_upto sigma n with
+  | Proj (p, c), App (f, args)
+  | App (f, args), Proj (p, c) -> 
+      (match kind_upto sigma f with
+      | Const (p', u) when Constant.equal (Projection.constant p) p' -> 
+          let pb = Environ.lookup_projection p env in
+          let npars = pb.Declarations.proj_npars in
+	  if Array.length args == npars + 1 then
+	    eqc' c args.(npars)
+	  else false
+      | _ -> false)
+  | _ -> Constr.compare_head_gen_with kind kind equ eqs eqc' m n
+
+let eq_constr_universes_proj env sigma m n =
+  let open Universes in
+  if m == n then Some Constraints.empty
+  else 
+    let cstrs = ref Constraints.empty in
+    let eq_universes strict l l' = 
+      cstrs := enforce_eq_instances_univs strict l l' !cstrs; true in
+    let eq_sorts s1 s2 = 
+      if Sorts.equal s1 s2 then true
+      else
+	(cstrs := Constraints.add 
+	   (Sorts.univ_of_sort s1, UEq, Sorts.univ_of_sort s2) !cstrs;
+	 true)
+    in
+    let rec eq_constr' m n = 
+      m == n ||	compare_head_gen_proj env sigma eq_universes eq_sorts eq_constr' m n
+    in
+    let res = eq_constr' (unsafe_to_constr m) (unsafe_to_constr n) in
+    if res then Some !cstrs else None
+
+module Vars =
+struct
+exception LocalOccur
+let to_constr = unsafe_to_constr
+
+(** Operations that commute with evar-normalization *)
+let lift n c = of_constr (Vars.lift n (to_constr c))
+let liftn n m c = of_constr (Vars.liftn n m (to_constr c))
+
+let substnl subst n c = of_constr (Vars.substnl (List.map to_constr subst) n (to_constr c))
+let substl subst c = of_constr (Vars.substl (List.map to_constr subst) (to_constr c))
+let subst1 c r = of_constr (Vars.subst1 (to_constr c) (to_constr r))
+
+let replace_vars subst c =
+  let map (id, c) = (id, to_constr c) in
+  of_constr (Vars.replace_vars (List.map map subst) (to_constr c))
+let substn_vars n subst c = of_constr (Vars.substn_vars n subst (to_constr c))
+let subst_vars subst c = of_constr (Vars.subst_vars subst (to_constr c))
+let subst_var subst c = of_constr (Vars.subst_var subst (to_constr c))
+
+(** Operations that dot NOT commute with evar-normalization *)
+let noccurn sigma n term =
+  let rec occur_rec n c = match kind sigma c with
+    | Rel m -> if Int.equal m n then raise LocalOccur
+    | _ -> iter_with_binders sigma succ occur_rec n c
+  in
+  try occur_rec n term; true with LocalOccur -> false
+
+let noccur_between sigma n m term =
+  let rec occur_rec n c = match kind sigma c with
+    | Rel p -> if n<=p && p<n+m then raise LocalOccur
+    | _        -> iter_with_binders sigma succ occur_rec n c
+  in
+  try occur_rec n term; true with LocalOccur -> false
+
+let closedn sigma n c =
+  let rec closed_rec n c = match kind sigma c with
+    | Rel m -> if m>n then raise LocalOccur
+    | _ -> iter_with_binders sigma succ closed_rec n c
+  in
+  try closed_rec n c; true with LocalOccur -> false
+
+let closed0 sigma c = closedn sigma 0 c
+
+end
+
+let rec isArity sigma c =
+  match kind sigma c with
+  | Prod (_,_,c)    -> isArity sigma c
+  | LetIn (_,b,_,c) -> isArity sigma (Vars.subst1 b c)
+  | Cast (c,_,_)      -> isArity sigma c
+  | Sort _          -> true
+  | _               -> false
+
+let mkProd_or_LetIn decl c =
+  let open Context.Rel.Declaration in
+  match decl with
+  | LocalAssum (na,t) -> mkProd (na, of_constr t, c)
+  | LocalDef (na,b,t) -> mkLetIn (na, of_constr b, of_constr t, c)
+
+let mkLambda_or_LetIn decl c =
+  let open Context.Rel.Declaration in
+  match decl with
+  | LocalAssum (na,t) -> mkLambda (na, of_constr t, c)
+  | LocalDef (na,b,t) -> mkLetIn (na, of_constr b, of_constr t, c)
+
+let it_mkProd_or_LetIn t ctx = List.fold_left (fun c d -> mkProd_or_LetIn d c) t ctx
+let it_mkLambda_or_LetIn t ctx = List.fold_left (fun c d -> mkLambda_or_LetIn d c) t ctx
+
+module Unsafe =
+struct
+let to_constr = unsafe_to_constr
+let eq = unsafe_eq
+end
-- 
cgit v1.2.3


From ca993b9e7765ac58f70740818758457c9367b0da Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 11 Nov 2016 00:29:02 +0100
Subject: Making judgment type generic over the type of inner constrs.

This allows to factorize code and prevents the unnecessary use of back and
forth conversions between the various types of terms.

Note that functions from typing may now raise errors as PretypeError rather
than TypeError, because they call the proper wrapper. I think that they were
wrongly calling the kernel because of an overlook of open modules.
---
 engine/eConstr.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'engine/eConstr.ml')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 0a5f1ba685..095521e252 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -75,6 +75,8 @@ type constr = t
 type existential = t pexistential
 type fixpoint = (t, t) pfixpoint
 type cofixpoint = (t, t) pcofixpoint
+type unsafe_judgment = (constr, types) Environ.punsafe_judgment
+type unsafe_type_judgment = types Environ.punsafe_type_judgment
 
 let mkProp = of_kind (Sort Sorts.prop)
 let mkSet = of_kind (Sort Sorts.set)
-- 
cgit v1.2.3


From 0489e8b56d7e10f7111c0171960e25d32201b963 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 11 Nov 2016 21:55:33 +0100
Subject: Clenv API using EConstr.

---
 engine/eConstr.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'engine/eConstr.ml')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 095521e252..7bd708e316 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -560,6 +560,8 @@ let substn_vars n subst c = of_constr (Vars.substn_vars n subst (to_constr c))
 let subst_vars subst c = of_constr (Vars.subst_vars subst (to_constr c))
 let subst_var subst c = of_constr (Vars.subst_var subst (to_constr c))
 
+let subst_univs_level_constr subst c =
+  of_constr (Vars.subst_univs_level_constr subst (to_constr c))
 (** Operations that dot NOT commute with evar-normalization *)
 let noccurn sigma n term =
   let rec occur_rec n c = match kind sigma c with
-- 
cgit v1.2.3


From 485bbfbed4ae4a28119c4e42c5e40fd77abf4f8a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 13 Nov 2016 20:38:41 +0100
Subject: Tactics API using EConstr.

---
 engine/eConstr.ml | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

(limited to 'engine/eConstr.ml')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 7bd708e316..9e0a55a0df 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -98,6 +98,7 @@ let mkCase (ci, c, r, p) = of_kind (Case (ci, c, r, p))
 let mkFix f = of_kind (Fix f)
 let mkCoFix f = of_kind (CoFix f)
 let mkProj (p, c) = of_kind (Proj (p, c))
+let mkArrow t1 t2 = of_kind (Prod (Anonymous, t1, t2))
 
 let applist (f, arg) = mkApp (f, Array.of_list arg)
 
@@ -466,6 +467,11 @@ let eq_constr_nounivs sigma c1 c2 =
   in
   eq_constr (unsafe_to_constr c1) (unsafe_to_constr c2)
 
+let compare_constr sigma cmp c1 c2 =
+  let kind c = kind_upto sigma c in
+  let cmp c1 c2 = cmp (of_constr c1) (of_constr c2) in
+  compare_gen kind (fun _ -> Univ.Instance.equal) Sorts.equal cmp (unsafe_to_constr c1) (unsafe_to_constr c2)
+
 (** TODO: factorize with universes.ml *)
 let test_constr_universes sigma leq m n =
   let open Universes in
@@ -608,6 +614,22 @@ let mkLambda_or_LetIn decl c =
   | LocalAssum (na,t) -> mkLambda (na, of_constr t, c)
   | LocalDef (na,b,t) -> mkLetIn (na, of_constr b, of_constr t, c)
 
+let mkNamedProd id typ c = mkProd (Name id, typ, Vars.subst_var id c)
+let mkNamedLambda id typ c = mkLambda (Name id, typ, Vars.subst_var id c)
+let mkNamedLetIn id c1 t c2 = mkLetIn (Name id, c1, t, Vars.subst_var id c2)
+
+let mkNamedProd_or_LetIn decl c =
+  let open Context.Named.Declaration in
+  match decl with
+    | LocalAssum (id,t) -> mkNamedProd id (of_constr t) c
+    | LocalDef (id,b,t) -> mkNamedLetIn id (of_constr b) (of_constr t) c
+
+let mkNamedLambda_or_LetIn decl c =
+  let open Context.Named.Declaration in
+  match decl with
+    | LocalAssum (id,t) -> mkNamedLambda id (of_constr t) c
+    | LocalDef (id,b,t) -> mkNamedLetIn id (of_constr b) (of_constr t) c
+
 let it_mkProd_or_LetIn t ctx = List.fold_left (fun c d -> mkProd_or_LetIn d c) t ctx
 let it_mkLambda_or_LetIn t ctx = List.fold_left (fun c d -> mkLambda_or_LetIn d c) t ctx
 
-- 
cgit v1.2.3


From 3f9e56fcbf479999325a86bbdaeefd6a0be13c65 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 18 Nov 2016 20:35:01 +0100
Subject: Equality API using EConstr.

---
 engine/eConstr.ml | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'engine/eConstr.ml')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 9e0a55a0df..1dd9d0c005 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -78,6 +78,8 @@ type cofixpoint = (t, t) pcofixpoint
 type unsafe_judgment = (constr, types) Environ.punsafe_judgment
 type unsafe_type_judgment = types Environ.punsafe_type_judgment
 
+let in_punivs a = (a, Univ.Instance.empty)
+
 let mkProp = of_kind (Sort Sorts.prop)
 let mkSet = of_kind (Sort Sorts.set)
 let mkType u = of_kind (Sort (Sorts.Type u))
@@ -92,8 +94,11 @@ let mkLambda (na, t, c) = of_kind (Lambda (na, t, c))
 let mkLetIn (na, b, t, c) = of_kind (LetIn (na, b, t, c))
 let mkApp (f, arg) = of_kind (App (f, arg))
 let mkConstU pc = of_kind (Const pc)
+let mkConst c = of_kind (Const (in_punivs c))
 let mkIndU pi = of_kind (Ind pi)
+let mkInd i = of_kind (Ind (in_punivs i))
 let mkConstructU pc = of_kind (Construct pc)
+let mkConstruct c = of_kind (Construct (in_punivs c))
 let mkCase (ci, c, r, p) = of_kind (Case (ci, c, r, p))
 let mkFix f = of_kind (Fix f)
 let mkCoFix f = of_kind (CoFix f)
-- 
cgit v1.2.3


From 118ae18590dbc7d01cf34e0cd6133b1e34ef9090 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 19 Nov 2016 00:20:30 +0100
Subject: Contradiction API using EConstr.

---
 engine/eConstr.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'engine/eConstr.ml')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 1dd9d0c005..629be8e4b5 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -99,6 +99,7 @@ let mkIndU pi = of_kind (Ind pi)
 let mkInd i = of_kind (Ind (in_punivs i))
 let mkConstructU pc = of_kind (Construct pc)
 let mkConstruct c = of_kind (Construct (in_punivs c))
+let mkConstructUi ((ind,u),i) = of_kind (Construct ((ind,i),u))
 let mkCase (ci, c, r, p) = of_kind (Case (ci, c, r, p))
 let mkFix f = of_kind (Fix f)
 let mkCoFix f = of_kind (CoFix f)
-- 
cgit v1.2.3


From b4b90c5d2e8c413e1981c456c933f35679386f09 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Nov 2016 16:18:47 +0100
Subject: Definining EConstr-based contexts.

This removes quite a few unsafe casts. Unluckily, I had to reintroduce
the old non-module based names for these data structures, because I could
not reproduce easily the same hierarchy in EConstr.
---
 engine/eConstr.ml | 105 +++++++++++++++++++++++++++++++++++++-----------------
 1 file changed, 73 insertions(+), 32 deletions(-)

(limited to 'engine/eConstr.ml')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 629be8e4b5..657285de2d 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -77,6 +77,10 @@ type fixpoint = (t, t) pfixpoint
 type cofixpoint = (t, t) pcofixpoint
 type unsafe_judgment = (constr, types) Environ.punsafe_judgment
 type unsafe_type_judgment = types Environ.punsafe_type_judgment
+type named_declaration = (constr, types) Context.Named.Declaration.pt
+type rel_declaration = (constr, types) Context.Rel.Declaration.pt
+type named_context = (constr, types) Context.Named.pt
+type rel_context = (constr, types) Context.Rel.pt
 
 let in_punivs a = (a, Univ.Instance.empty)
 
@@ -201,14 +205,6 @@ let decompose_app sigma c =
     | App (f,cl) -> (f, Array.to_list cl)
     | _ -> (c,[])
 
-let local_assum (na, t) =
-  let open Rel.Declaration in
-  LocalAssum (na, unsafe_to_constr t)
-
-let local_def (na, b, t) =
-  let open Rel.Declaration in
-  LocalDef (na, unsafe_to_constr b, unsafe_to_constr t)
-
 let decompose_lam sigma c =
   let rec lamdec_rec l c = match kind sigma c with
     | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) c
@@ -218,38 +214,41 @@ let decompose_lam sigma c =
   lamdec_rec [] c
 
 let decompose_lam_assum sigma c =
+  let open Rel.Declaration in
   let rec lamdec_rec l c =
     match kind sigma c with
-    | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (local_assum (x,t)) l) c
-    | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (local_def (x,b,t)) l) c
+    | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) c
+    | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) c
     | Cast (c,_,_)      -> lamdec_rec l c
     | _               -> l,c
   in
   lamdec_rec Context.Rel.empty c
 
 let decompose_lam_n_assum sigma n c =
+  let open Rel.Declaration in
   if n < 0 then
     error "decompose_lam_n_assum: integer parameter must be positive";
   let rec lamdec_rec l n c =
     if Int.equal n 0 then l,c
     else
       match kind sigma c with
-      | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (local_assum (x,t)) l) (n-1) c
-      | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (local_def (x,b,t)) l) n c
+      | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c
+      | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) n c
       | Cast (c,_,_)      -> lamdec_rec l n c
       | c -> error "decompose_lam_n_assum: not enough abstractions"
   in
   lamdec_rec Context.Rel.empty n c
 
 let decompose_lam_n_decls sigma n =
+  let open Rel.Declaration in
   if n < 0 then
     error "decompose_lam_n_decls: integer parameter must be positive";
   let rec lamdec_rec l n c =
     if Int.equal n 0 then l,c
     else
       match kind sigma c with
-      | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (local_assum (x,t)) l) (n-1) c
-      | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (local_def (x,b,t)) l) (n-1) c
+      | Lambda (x,t,c)  -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c
+      | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c
       | Cast (c,_,_)      -> lamdec_rec l n c
       | c -> error "decompose_lam_n_decls: not enough abstractions"
   in
@@ -264,24 +263,26 @@ let decompose_prod sigma c =
   proddec_rec [] c
 
 let decompose_prod_assum sigma c =
+  let open Rel.Declaration in
   let rec proddec_rec l c =
     match kind sigma c with
-    | Prod (x,t,c)  -> proddec_rec (Context.Rel.add (local_assum (x,t)) l) c
-    | LetIn (x,b,t,c) -> proddec_rec (Context.Rel.add (local_def (x,b,t)) l) c
+    | Prod (x,t,c)  -> proddec_rec (Context.Rel.add (LocalAssum (x,t)) l) c
+    | LetIn (x,b,t,c) -> proddec_rec (Context.Rel.add (LocalDef (x,b,t)) l) c
     | Cast (c,_,_)      -> proddec_rec l c
     | _               -> l,c
   in
   proddec_rec Context.Rel.empty c
 
 let decompose_prod_n_assum sigma n c =
+  let open Rel.Declaration in
   if n < 0 then
     error "decompose_prod_n_assum: integer parameter must be positive";
   let rec prodec_rec l n c =
     if Int.equal n 0 then l,c
     else
       match kind sigma c with
-      | Prod (x,t,c)    -> prodec_rec (Context.Rel.add (local_assum (x,t)) l) (n-1) c
-      | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (local_def (x,b,t)) l) (n-1) c
+      | Prod (x,t,c)    -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c
+      | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c
       | Cast (c,_,_)      -> prodec_rec l n c
       | c -> error "decompose_prod_n_assum: not enough assumptions"
   in
@@ -413,24 +414,26 @@ let iter sigma f c = match kind sigma c with
   | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
   | CoFix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl
 
-let iter_with_full_binders sigma g f n c = match kind sigma c with
+let iter_with_full_binders sigma g f n c =
+  let open Context.Rel.Declaration in
+  match kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> ()
   | Cast (c,_,t) -> f n c; f n t
-  | Prod (na,t,c) -> f n t; f (g (local_assum (na, t)) n) c
-  | Lambda (na,t,c) -> f n t; f (g (local_assum (na, t)) n) c
-  | LetIn (na,b,t,c) -> f n b; f n t; f (g (local_def (na, b, t)) n) c
+  | Prod (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
+  | Lambda (na,t,c) -> f n t; f (g (LocalAssum (na, t)) n) c
+  | LetIn (na,b,t,c) -> f n b; f n t; f (g (LocalDef (na, b, t)) n) c
   | App (c,l) -> f n c; CArray.Fun1.iter f n l
   | Evar (_,l) -> CArray.Fun1.iter f n l
   | Case (_,p,c,bl) -> f n p; f n c; CArray.Fun1.iter f n bl
   | Proj (p,c) -> f n c
   | Fix (_,(lna,tl,bl)) ->
     Array.iter (f n) tl;
-    let n' = Array.fold_left2 (fun n na t -> g (local_assum (na,t)) n) n lna tl in
+    let n' = Array.fold_left2 (fun n na t -> g (LocalAssum (na,t)) n) n lna tl in
     Array.iter (f n') bl
   | CoFix (_,(lna,tl,bl)) ->
     Array.iter (f n) tl;
-    let n' = Array.fold_left2 (fun n na t -> g (local_assum (na,t)) n) n lna tl in
+    let n' = Array.fold_left2 (fun n na t -> g (LocalAssum (na,t)) n) n lna tl in
     Array.iter (f n') bl
 
 let iter_with_binders sigma g f n c =
@@ -611,14 +614,14 @@ let rec isArity sigma c =
 let mkProd_or_LetIn decl c =
   let open Context.Rel.Declaration in
   match decl with
-  | LocalAssum (na,t) -> mkProd (na, of_constr t, c)
-  | LocalDef (na,b,t) -> mkLetIn (na, of_constr b, of_constr t, c)
+  | LocalAssum (na,t) -> mkProd (na, t, c)
+  | LocalDef (na,b,t) -> mkLetIn (na, b, t, c)
 
 let mkLambda_or_LetIn decl c =
   let open Context.Rel.Declaration in
   match decl with
-  | LocalAssum (na,t) -> mkLambda (na, of_constr t, c)
-  | LocalDef (na,b,t) -> mkLetIn (na, of_constr b, of_constr t, c)
+  | LocalAssum (na,t) -> mkLambda (na, t, c)
+  | LocalDef (na,b,t) -> mkLetIn (na, b, t, c)
 
 let mkNamedProd id typ c = mkProd (Name id, typ, Vars.subst_var id c)
 let mkNamedLambda id typ c = mkLambda (Name id, typ, Vars.subst_var id c)
@@ -627,18 +630,56 @@ let mkNamedLetIn id c1 t c2 = mkLetIn (Name id, c1, t, Vars.subst_var id c2)
 let mkNamedProd_or_LetIn decl c =
   let open Context.Named.Declaration in
   match decl with
-    | LocalAssum (id,t) -> mkNamedProd id (of_constr t) c
-    | LocalDef (id,b,t) -> mkNamedLetIn id (of_constr b) (of_constr t) c
+    | LocalAssum (id,t) -> mkNamedProd id t c
+    | LocalDef (id,b,t) -> mkNamedLetIn id b t c
 
 let mkNamedLambda_or_LetIn decl c =
   let open Context.Named.Declaration in
   match decl with
-    | LocalAssum (id,t) -> mkNamedLambda id (of_constr t) c
-    | LocalDef (id,b,t) -> mkNamedLetIn id (of_constr b) (of_constr t) c
+    | LocalAssum (id,t) -> mkNamedLambda id t c
+    | LocalDef (id,b,t) -> mkNamedLetIn id b t c
 
 let it_mkProd_or_LetIn t ctx = List.fold_left (fun c d -> mkProd_or_LetIn d c) t ctx
 let it_mkLambda_or_LetIn t ctx = List.fold_left (fun c d -> mkLambda_or_LetIn d c) t ctx
 
+open Context
+open Environ
+
+let sym : type a b. (a, b) eq -> (b, a) eq = fun Refl -> Refl
+
+let cast_rel_decl :
+  type a b. (a,b) eq -> (a, a) Rel.Declaration.pt -> (b, b) Rel.Declaration.pt =
+  fun Refl x -> x
+
+let cast_rel_context :
+  type a b. (a,b) eq -> (a, a) Rel.pt -> (b, b) Rel.pt =
+  fun Refl x -> x
+
+let cast_named_decl :
+  type a b. (a,b) eq -> (a, a) Named.Declaration.pt -> (b, b) Named.Declaration.pt =
+  fun Refl x -> x
+
+let cast_named_context :
+  type a b. (a,b) eq -> (a, a) Named.pt -> (b, b) Named.pt =
+  fun Refl x -> x
+
+let push_rel d e = push_rel (cast_rel_decl unsafe_eq d) e
+let push_rel_context d e = push_rel_context (cast_rel_context unsafe_eq d) e
+let push_named d e = push_named (cast_named_decl unsafe_eq d) e
+let push_named_context d e = push_named_context (cast_named_context unsafe_eq d) e
+let push_named_context_val d e = push_named_context_val (cast_named_decl unsafe_eq d) e
+
+let rel_context e = cast_rel_context (sym unsafe_eq) (rel_context e)
+let named_context e = cast_named_context (sym unsafe_eq) (named_context e)
+
+let val_of_named_context e = val_of_named_context (cast_named_context unsafe_eq e)
+let named_context_of_val e = cast_named_context (sym unsafe_eq) (named_context_of_val e)
+
+let lookup_rel i e = cast_rel_decl (sym unsafe_eq) (lookup_rel i e)
+let lookup_named n e = cast_named_decl (sym unsafe_eq) (lookup_named n e)
+let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_val n e)
+
+
 module Unsafe =
 struct
 let to_constr = unsafe_to_constr
-- 
cgit v1.2.3


From be51c33a6bf91a00fdd5f3638ddb5b3cc3a2c626 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 30 Nov 2016 00:41:31 +0100
Subject: Namegen primitives now apply on evar constrs.

Incidentally, this fixes a printing bug in output/inference.v where the
displayed name of an evar was the wrong one because its type was not
evar-expanded enough.
---
 engine/eConstr.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'engine/eConstr.ml')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 657285de2d..7d4d17c630 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -131,6 +131,8 @@ let isCase sigma c = match kind sigma c with Case _ -> true | _ -> false
 let isProj sigma c = match kind sigma c with Proj _ -> true | _ -> false
 let isVarId sigma id c =
   match kind sigma c with Var id' -> Id.equal id id' | _ -> false
+let isRelN sigma n c =
+  match kind sigma c with Rel n' -> Int.equal n n' | _ -> false
 
 let destRel sigma c = match kind sigma c with
 | Rel p -> p
-- 
cgit v1.2.3


From 4f66c854956bd05a24fd55c3d52fb669dbbb65e6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 30 Nov 2016 15:06:42 +0100
Subject: Moving evar-normalization functions to EConstr.

This removes code duplication between Evarutil and EConstr.
---
 engine/eConstr.ml | 37 +++++++++++++++++++------------------
 1 file changed, 19 insertions(+), 18 deletions(-)

(limited to 'engine/eConstr.ml')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 7d4d17c630..2de6d7ae4a 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -19,8 +19,10 @@ sig
 type t
 val kind : Evd.evar_map -> t -> (t, t) Constr.kind_of_term
 val kind_upto : Evd.evar_map -> constr -> (constr, types) Constr.kind_of_term
+val whd_evar : Evd.evar_map -> t -> t
 val of_kind : (t, t) Constr.kind_of_term -> t
 val of_constr : Constr.t -> t
+val to_constr : evar_map -> t -> Constr.t
 val unsafe_to_constr : t -> Constr.t
 val unsafe_eq : (t, Constr.t) eq
 end =
@@ -32,40 +34,43 @@ let safe_evar_value sigma ev =
   try Some (Evd.existential_value sigma ev)
   with NotInstantiatedEvar | Not_found -> None
 
-let rec kind sigma c =
-  let c0 = Constr.kind c in
-  match c0 with
+let rec whd_evar sigma c =
+  match Constr.kind c with
   | Evar (evk, args) ->
     (match safe_evar_value sigma (evk, args) with
-        Some c -> kind sigma c
-      | None -> c0)
+        Some c -> whd_evar sigma c
+      | None -> c)
   | Sort (Type u) ->
     let u' = Evd.normalize_universe sigma u in
-    if u' == u then c0 else Sort (Type u')
+    if u' == u then c else mkSort (Sorts.sort_of_univ u')
   | Const (c', u) when not (Univ.Instance.is_empty u) ->
     let u' = Evd.normalize_universe_instance sigma u in
-    if u' == u then c0 else Const (c', u')
+    if u' == u then c else mkConstU (c', u')
   | Ind (i, u) when not (Univ.Instance.is_empty u) ->
     let u' = Evd.normalize_universe_instance sigma u in
-    if u' == u then c0 else Ind (i, u')
+    if u' == u then c else mkIndU (i, u')
   | Construct (co, u) when not (Univ.Instance.is_empty u) ->
     let u' = Evd.normalize_universe_instance sigma u in
-    if u' == u then c0 else Construct (co, u')
-  | App (c, args) when isEvar c ->
+    if u' == u then c else mkConstructU (co, u')
+  | App (f, args) when isEvar f ->
     (** Enforce smart constructor invariant on applications *)
-    let ev = destEvar c in
+    let ev = destEvar f in
     begin match safe_evar_value sigma ev with
-    | None -> c0
-    | Some c -> kind sigma (mkApp (c, args))
+    | None -> c
+    | Some f -> whd_evar sigma (mkApp (f, args))
     end
-  | _ -> c0
+  | _ -> c
 
+let kind sigma c = Constr.kind (whd_evar sigma c)
 let kind_upto = kind
 let of_kind = Constr.of_kind
 let of_constr c = c
 let unsafe_to_constr c = c
 let unsafe_eq = Refl
 
+let rec to_constr sigma t =
+  Constr.map (fun t -> to_constr sigma t) (whd_evar sigma t)
+
 end
 
 include API
@@ -457,10 +462,6 @@ let fold sigma f acc c = match kind sigma c with
   | CoFix (_,(lna,tl,bl)) ->
     Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
 
-let to_constr sigma t =
-  let rec map c = Constr.map map (Constr.of_kind (kind_upto sigma c)) in
-  map (unsafe_to_constr t)
-
 let compare_gen k eq_inst eq_sort eq_constr c1 c2 =
   (c1 == c2) || Constr.compare_head_gen_with k k eq_inst eq_sort eq_constr c1 c2
 
-- 
cgit v1.2.3


From 1523276aedcde1c79aff899ec87f05f3a708d13b Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 9 Feb 2017 18:53:53 +0100
Subject: Missing API in EConstr.

---
 engine/eConstr.ml | 36 ++++++++++++++++++++++++++++++++++++
 1 file changed, 36 insertions(+)

(limited to 'engine/eConstr.ml')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 2de6d7ae4a..b6b202cd95 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -19,12 +19,17 @@ sig
 type t
 val kind : Evd.evar_map -> t -> (t, t) Constr.kind_of_term
 val kind_upto : Evd.evar_map -> constr -> (constr, types) Constr.kind_of_term
+val kind_of_type : Evd.evar_map -> t -> (t, t) kind_of_type
 val whd_evar : Evd.evar_map -> t -> t
 val of_kind : (t, t) Constr.kind_of_term -> t
 val of_constr : Constr.t -> t
 val to_constr : evar_map -> t -> Constr.t
 val unsafe_to_constr : t -> Constr.t
 val unsafe_eq : (t, Constr.t) eq
+val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, t) Context.Named.Declaration.pt
+val unsafe_to_named_decl : (t, t) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt
+val unsafe_to_rel_decl : (t, t) Context.Rel.Declaration.pt -> (Constr.t, Constr.types) Context.Rel.Declaration.pt
+val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, t) Context.Rel.Declaration.pt
 end =
 struct
 
@@ -63,6 +68,7 @@ let rec whd_evar sigma c =
 
 let kind sigma c = Constr.kind (whd_evar sigma c)
 let kind_upto = kind
+let kind_of_type sigma c = Term.kind_of_type (whd_evar sigma c)
 let of_kind = Constr.of_kind
 let of_constr c = c
 let unsafe_to_constr c = c
@@ -71,6 +77,11 @@ let unsafe_eq = Refl
 let rec to_constr sigma t =
   Constr.map (fun t -> to_constr sigma t) (whd_evar sigma t)
 
+let of_named_decl d = d
+let unsafe_to_named_decl d = d
+let of_rel_decl d = d
+let unsafe_to_rel_decl d = d
+
 end
 
 include API
@@ -261,6 +272,25 @@ let decompose_lam_n_decls sigma n =
   in
   lamdec_rec Context.Rel.empty n
 
+let lamn n env b =
+  let rec lamrec = function
+    | (0, env, b)        -> b
+    | (n, ((v,t)::l), b) -> lamrec (n-1,  l, mkLambda (v,t,b))
+    | _ -> assert false
+  in
+  lamrec (n,env,b)
+
+let compose_lam l b = lamn (List.length l) l b
+
+let rec to_lambda sigma n prod =
+  if Int.equal n 0 then
+    prod
+  else
+    match kind sigma prod with
+      | Prod (na,ty,bd) -> mkLambda (na,ty,to_lambda sigma (n-1) bd)
+      | Cast (c,_,_) -> to_lambda sigma n c
+      | _   -> user_err ~hdr:"to_lambda" (Pp.mt ())
+
 let decompose_prod sigma c =
   let rec proddec_rec l c = match kind sigma c with
     | Prod (x,t,c) -> proddec_rec ((x,t)::l) c
@@ -682,9 +712,15 @@ let lookup_rel i e = cast_rel_decl (sym unsafe_eq) (lookup_rel i e)
 let lookup_named n e = cast_named_decl (sym unsafe_eq) (lookup_named n e)
 let lookup_named_val n e = cast_named_decl (sym unsafe_eq) (lookup_named_val n e)
 
+let fresh_global ?loc ?rigid ?names env sigma reference =
+  let Sigma.Sigma (t,sigma,p) =
+    Sigma.fresh_global ?loc ?rigid ?names env sigma reference in
+  Sigma.Sigma (of_constr t,sigma,p)
 
 module Unsafe =
 struct
 let to_constr = unsafe_to_constr
+let to_rel_decl = unsafe_to_rel_decl
+let to_named_decl = unsafe_to_named_decl
 let eq = unsafe_eq
 end
-- 
cgit v1.2.3


From b5f07be9fdcd41fdaf73503e5214e766bf6a303b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 30 Mar 2017 16:22:33 +0200
Subject: Specially crafted EConstr.kind to be more efficient.

We do one step of loop unrolling, limit the number of allocations and
mark the function as inline.
---
 engine/eConstr.ml | 56 ++++++++++++++++++++++++++++++++++++++++++++++++-------
 1 file changed, 49 insertions(+), 7 deletions(-)

(limited to 'engine/eConstr.ml')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index f50a8b8501..68ef372263 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -41,8 +41,8 @@ let safe_evar_value sigma ev =
 
 let rec whd_evar sigma c =
   match Constr.kind c with
-  | Evar (evk, args) ->
-    (match safe_evar_value sigma (evk, args) with
+  | Evar ev ->
+    (match safe_evar_value sigma ev with
         Some c -> whd_evar sigma c
       | None -> c)
   | Sort (Type u) ->
@@ -57,16 +57,58 @@ let rec whd_evar sigma c =
   | Construct (co, u) when not (Univ.Instance.is_empty u) ->
     let u' = Evd.normalize_universe_instance sigma u in
     if u' == u then c else mkConstructU (co, u')
-  | App (f, args) when isEvar f ->
+  | App (f, args) ->
     (** Enforce smart constructor invariant on applications *)
-    let ev = destEvar f in
+    begin match Constr.kind f with
+    | Evar ev ->
+      begin match safe_evar_value sigma ev with
+      | None -> c
+      | Some f -> whd_evar sigma (mkApp (f, args))
+      end
+    | _ -> c
+    end
+  | _ -> c
+
+(** Loop unrolling to ensure efficiency *)
+let kind sigma c =
+  let c = Constr.kind c in
+  match c with
+  | Evar ev ->
     begin match safe_evar_value sigma ev with
+    | Some c -> Constr.kind (whd_evar sigma c)
     | None -> c
-    | Some f -> whd_evar sigma (mkApp (f, args))
     end
-  | _ -> c
+  | Sort (Type u) ->
+    let u' = Evd.normalize_universe sigma u in
+    if u' == u then c else Sort (Sorts.sort_of_univ u')
+  | Const (c', u) ->
+    if Univ.Instance.is_empty u then c
+    else
+      let u' = Evd.normalize_universe_instance sigma u in
+      if u' == u then c else Const (c', u')
+  | Ind (i, u) ->
+    if Univ.Instance.is_empty u then c
+    else
+      let u' = Evd.normalize_universe_instance sigma u in
+      if u' == u then c else Ind (i, u')
+  | Construct (co, u) ->
+    if Univ.Instance.is_empty u then c
+    else
+      let u' = Evd.normalize_universe_instance sigma u in
+      if u' == u then c else Construct (co, u')
+  | App (f, args) ->
+    (** Enforce smart constructor invariant on applications *)
+    begin match Constr.kind f with
+    | Evar ev ->
+      begin match safe_evar_value sigma ev with
+      | None -> c
+      | Some f -> Constr.kind (whd_evar sigma (mkApp (f, args)))
+      end
+    | _ -> c
+    end
+  | c -> c
+[@@ocaml.inline]
 
-let kind sigma c = Constr.kind (whd_evar sigma c)
 let kind_upto = kind
 let kind_of_type sigma c = Term.kind_of_type (whd_evar sigma c)
 let of_kind = Constr.of_kind
-- 
cgit v1.2.3


From a20494163815e4b8275c4d0412d6c857c95263f4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 31 Mar 2017 22:39:36 +0200
Subject: Revert "Specially crafted EConstr.kind to be more efficient."

This reverts commit b5f07be9fdcd41fdaf73503e5214e766bf6a303b. The performance
difference was not conclusive enough to pay for the code ugliness.
---
 engine/eConstr.ml | 56 +++++++------------------------------------------------
 1 file changed, 7 insertions(+), 49 deletions(-)

(limited to 'engine/eConstr.ml')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 68ef372263..f50a8b8501 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -41,8 +41,8 @@ let safe_evar_value sigma ev =
 
 let rec whd_evar sigma c =
   match Constr.kind c with
-  | Evar ev ->
-    (match safe_evar_value sigma ev with
+  | Evar (evk, args) ->
+    (match safe_evar_value sigma (evk, args) with
         Some c -> whd_evar sigma c
       | None -> c)
   | Sort (Type u) ->
@@ -57,58 +57,16 @@ let rec whd_evar sigma c =
   | Construct (co, u) when not (Univ.Instance.is_empty u) ->
     let u' = Evd.normalize_universe_instance sigma u in
     if u' == u then c else mkConstructU (co, u')
-  | App (f, args) ->
+  | App (f, args) when isEvar f ->
     (** Enforce smart constructor invariant on applications *)
-    begin match Constr.kind f with
-    | Evar ev ->
-      begin match safe_evar_value sigma ev with
-      | None -> c
-      | Some f -> whd_evar sigma (mkApp (f, args))
-      end
-    | _ -> c
-    end
-  | _ -> c
-
-(** Loop unrolling to ensure efficiency *)
-let kind sigma c =
-  let c = Constr.kind c in
-  match c with
-  | Evar ev ->
+    let ev = destEvar f in
     begin match safe_evar_value sigma ev with
-    | Some c -> Constr.kind (whd_evar sigma c)
     | None -> c
+    | Some f -> whd_evar sigma (mkApp (f, args))
     end
-  | Sort (Type u) ->
-    let u' = Evd.normalize_universe sigma u in
-    if u' == u then c else Sort (Sorts.sort_of_univ u')
-  | Const (c', u) ->
-    if Univ.Instance.is_empty u then c
-    else
-      let u' = Evd.normalize_universe_instance sigma u in
-      if u' == u then c else Const (c', u')
-  | Ind (i, u) ->
-    if Univ.Instance.is_empty u then c
-    else
-      let u' = Evd.normalize_universe_instance sigma u in
-      if u' == u then c else Ind (i, u')
-  | Construct (co, u) ->
-    if Univ.Instance.is_empty u then c
-    else
-      let u' = Evd.normalize_universe_instance sigma u in
-      if u' == u then c else Construct (co, u')
-  | App (f, args) ->
-    (** Enforce smart constructor invariant on applications *)
-    begin match Constr.kind f with
-    | Evar ev ->
-      begin match safe_evar_value sigma ev with
-      | None -> c
-      | Some f -> Constr.kind (whd_evar sigma (mkApp (f, args)))
-      end
-    | _ -> c
-    end
-  | c -> c
-[@@ocaml.inline]
+  | _ -> c
 
+let kind sigma c = Constr.kind (whd_evar sigma c)
 let kind_upto = kind
 let kind_of_type sigma c = Term.kind_of_type (whd_evar sigma c)
 let of_kind = Constr.of_kind
-- 
cgit v1.2.3


From 6add354ad9ca0f68d3ef311c4e53ee96d9fdb4d7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 31 Mar 2017 22:46:05 +0200
Subject: Ensuring proper cast invariants in EConstr.kind.

The kernel does fishy things with casts, such that ensuring there are no
two consecutive VMcast or NATIVEcast in terms. We enforce this in EConstr
view as well.
---
 engine/eConstr.ml | 16 ++++++++++++----
 1 file changed, 12 insertions(+), 4 deletions(-)

(limited to 'engine/eConstr.ml')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index f50a8b8501..9026800f2b 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -41,10 +41,11 @@ let safe_evar_value sigma ev =
 
 let rec whd_evar sigma c =
   match Constr.kind c with
-  | Evar (evk, args) ->
-    (match safe_evar_value sigma (evk, args) with
-        Some c -> whd_evar sigma c
-      | None -> c)
+  | Evar ev ->
+    begin match safe_evar_value sigma ev with
+    | Some c -> whd_evar sigma c
+    | None -> c
+    end
   | Sort (Type u) ->
     let u' = Evd.normalize_universe sigma u in
     if u' == u then c else mkSort (Sorts.sort_of_univ u')
@@ -64,6 +65,13 @@ let rec whd_evar sigma c =
     | None -> c
     | Some f -> whd_evar sigma (mkApp (f, args))
     end
+  | Cast (c0, k, t) when isEvar c0 ->
+    (** Enforce smart constructor invariant on casts. *)
+    let ev = destEvar c0 in
+    begin match safe_evar_value sigma ev with
+    | None -> c
+    | Some c -> whd_evar sigma (mkCast (c, k, t))
+    end
   | _ -> c
 
 let kind sigma c = Constr.kind (whd_evar sigma c)
-- 
cgit v1.2.3


From ce029533a1f0fc6ac9e28d162350a64446522246 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 31 Mar 2017 23:05:17 +0200
Subject: Make the Constr.kind_of_term type parametric in sorts and universes.

---
 engine/eConstr.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'engine/eConstr.ml')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 9026800f2b..094841d69d 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -17,11 +17,11 @@ open Evd
 module API :
 sig
 type t
-val kind : Evd.evar_map -> t -> (t, t) Constr.kind_of_term
-val kind_upto : Evd.evar_map -> constr -> (constr, types) Constr.kind_of_term
+val kind : Evd.evar_map -> t -> (t, t, Sorts.t, Univ.Instance.t) Constr.kind_of_term
+val kind_upto : Evd.evar_map -> constr -> (constr, types, Sorts.t, Univ.Instance.t) Constr.kind_of_term
 val kind_of_type : Evd.evar_map -> t -> (t, t) kind_of_type
 val whd_evar : Evd.evar_map -> t -> t
-val of_kind : (t, t) Constr.kind_of_term -> t
+val of_kind : (t, t, Sorts.t, Univ.Instance.t) Constr.kind_of_term -> t
 val of_constr : Constr.t -> t
 val to_constr : evar_map -> t -> Constr.t
 val unsafe_to_constr : t -> Constr.t
-- 
cgit v1.2.3


From 3df2431a80f9817ce051334cb9c3b1f465bffb60 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 31 Mar 2017 23:20:25 +0200
Subject: Actually exporting delayed universes in the EConstr implementation.

For now we only normalize sorts, and we leave instances for the next
commit.
---
 engine/eConstr.ml | 54 +++++++++++++++++++++++++++++++++++++++++++-----------
 1 file changed, 43 insertions(+), 11 deletions(-)

(limited to 'engine/eConstr.ml')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 094841d69d..166340b412 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -16,12 +16,19 @@ open Evd
 
 module API :
 sig
+module ESorts :
+sig
+type t
+val make : Sorts.t -> t
+val kind : Evd.evar_map -> t -> Sorts.t
+val unsafe_to_sorts : t -> Sorts.t
+end
 type t
-val kind : Evd.evar_map -> t -> (t, t, Sorts.t, Univ.Instance.t) Constr.kind_of_term
+val kind : Evd.evar_map -> t -> (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term
 val kind_upto : Evd.evar_map -> constr -> (constr, types, Sorts.t, Univ.Instance.t) Constr.kind_of_term
 val kind_of_type : Evd.evar_map -> t -> (t, t) kind_of_type
 val whd_evar : Evd.evar_map -> t -> t
-val of_kind : (t, t, Sorts.t, Univ.Instance.t) Constr.kind_of_term -> t
+val of_kind : (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term -> t
 val of_constr : Constr.t -> t
 val to_constr : evar_map -> t -> Constr.t
 val unsafe_to_constr : t -> Constr.t
@@ -33,6 +40,16 @@ val of_rel_decl : (Constr.t, Constr.types) Context.Rel.Declaration.pt -> (t, t)
 end =
 struct
 
+module ESorts =
+struct
+  type t = Sorts.t
+  let make s = s
+  let kind sigma = function
+  | Type u -> sort_of_univ (Evd.normalize_universe sigma u)
+  | s -> s
+  let unsafe_to_sorts s = s
+end
+
 type t = Constr.t
 
 let safe_evar_value sigma ev =
@@ -46,9 +63,6 @@ let rec whd_evar sigma c =
     | Some c -> whd_evar sigma c
     | None -> c
     end
-  | Sort (Type u) ->
-    let u' = Evd.normalize_universe sigma u in
-    if u' == u then c else mkSort (Sorts.sort_of_univ u')
   | Const (c', u) when not (Univ.Instance.is_empty u) ->
     let u' = Evd.normalize_universe_instance sigma u in
     if u' == u then c else mkConstU (c', u')
@@ -82,8 +96,25 @@ let of_constr c = c
 let unsafe_to_constr c = c
 let unsafe_eq = Refl
 
-let rec to_constr sigma t =
-  Constr.map (fun t -> to_constr sigma t) (whd_evar sigma t)
+let rec to_constr sigma c = match Constr.kind c with
+| Evar ev ->
+  begin match safe_evar_value sigma ev with
+  | Some c -> to_constr sigma c
+  | None -> Constr.map (fun c -> to_constr sigma c) c
+  end
+| Sort (Type u) ->
+  let u' = Evd.normalize_universe sigma u in
+  if u' == u then c else mkSort (Sorts.sort_of_univ u')
+| Const (c', u) when not (Univ.Instance.is_empty u) ->
+  let u' = Evd.normalize_universe_instance sigma u in
+  if u' == u then c else mkConstU (c', u')
+| Ind (i, u) when not (Univ.Instance.is_empty u) ->
+  let u' = Evd.normalize_universe_instance sigma u in
+  if u' == u then c else mkIndU (i, u')
+| Construct (co, u) when not (Univ.Instance.is_empty u) ->
+  let u' = Evd.normalize_universe_instance sigma u in
+  if u' == u then c else mkConstructU (co, u')
+| _ -> Constr.map (fun c -> to_constr sigma c) c
 
 let of_named_decl d = d
 let unsafe_to_named_decl d = d
@@ -108,14 +139,14 @@ type rel_context = (constr, types) Context.Rel.pt
 
 let in_punivs a = (a, Univ.Instance.empty)
 
-let mkProp = of_kind (Sort Sorts.prop)
-let mkSet = of_kind (Sort Sorts.set)
-let mkType u = of_kind (Sort (Sorts.Type u))
+let mkProp = of_kind (Sort (ESorts.make Sorts.prop))
+let mkSet = of_kind (Sort (ESorts.make Sorts.set))
+let mkType u = of_kind (Sort (ESorts.make (Sorts.Type u)))
 let mkRel n = of_kind (Rel n)
 let mkVar id = of_kind (Var id)
 let mkMeta n = of_kind (Meta n)
 let mkEvar e = of_kind (Evar e)
-let mkSort s = of_kind (Sort s)
+let mkSort s = of_kind (Sort (ESorts.make s))
 let mkCast (b, k, t) = of_kind (Cast (b, k, t))
 let mkProd (na, t, u) = of_kind (Prod (na, t, u))
 let mkLambda (na, t, c) = of_kind (Lambda (na, t, c))
@@ -730,6 +761,7 @@ let fresh_global ?loc ?rigid ?names env sigma reference =
 
 module Unsafe =
 struct
+let to_sorts = ESorts.unsafe_to_sorts
 let to_constr = unsafe_to_constr
 let to_rel_decl = unsafe_to_rel_decl
 let to_named_decl = unsafe_to_named_decl
-- 
cgit v1.2.3


From 7babf0d42af11f5830bc157a671bd81b478a4f02 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 1 Apr 2017 02:36:16 +0200
Subject: Using delayed universe instances in EConstr.

The transition has been done a bit brutally. I think we can still save a
lot of useless normalizations here and there by providing the right API
in EConstr. Nonetheless, this is a first step.
---
 engine/eConstr.ml | 35 +++++++++++++++++++++++------------
 1 file changed, 23 insertions(+), 12 deletions(-)

(limited to 'engine/eConstr.ml')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 166340b412..28e9ffdb27 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -23,12 +23,21 @@ val make : Sorts.t -> t
 val kind : Evd.evar_map -> t -> Sorts.t
 val unsafe_to_sorts : t -> Sorts.t
 end
+module EInstance :
+sig
+type t
+val make : Univ.Instance.t -> t
+val kind : Evd.evar_map -> t -> Univ.Instance.t
+val empty : t
+val is_empty : t -> bool
+val unsafe_to_instance : t -> Univ.Instance.t
+end
 type t
-val kind : Evd.evar_map -> t -> (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term
+val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_term
 val kind_upto : Evd.evar_map -> constr -> (constr, types, Sorts.t, Univ.Instance.t) Constr.kind_of_term
 val kind_of_type : Evd.evar_map -> t -> (t, t) kind_of_type
 val whd_evar : Evd.evar_map -> t -> t
-val of_kind : (t, t, ESorts.t, Univ.Instance.t) Constr.kind_of_term -> t
+val of_kind : (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -> t
 val of_constr : Constr.t -> t
 val to_constr : evar_map -> t -> Constr.t
 val unsafe_to_constr : t -> Constr.t
@@ -50,6 +59,16 @@ struct
   let unsafe_to_sorts s = s
 end
 
+module EInstance =
+struct
+  type t = Univ.Instance.t
+  let make i = i
+  let kind sigma i = Evd.normalize_universe_instance sigma i
+  let empty = Univ.Instance.empty
+  let is_empty = Univ.Instance.is_empty
+  let unsafe_to_instance t = t
+end
+
 type t = Constr.t
 
 let safe_evar_value sigma ev =
@@ -63,15 +82,6 @@ let rec whd_evar sigma c =
     | Some c -> whd_evar sigma c
     | None -> c
     end
-  | Const (c', u) when not (Univ.Instance.is_empty u) ->
-    let u' = Evd.normalize_universe_instance sigma u in
-    if u' == u then c else mkConstU (c', u')
-  | Ind (i, u) when not (Univ.Instance.is_empty u) ->
-    let u' = Evd.normalize_universe_instance sigma u in
-    if u' == u then c else mkIndU (i, u')
-  | Construct (co, u) when not (Univ.Instance.is_empty u) ->
-    let u' = Evd.normalize_universe_instance sigma u in
-    if u' == u then c else mkConstructU (co, u')
   | App (f, args) when isEvar f ->
     (** Enforce smart constructor invariant on applications *)
     let ev = destEvar f in
@@ -137,7 +147,7 @@ type rel_declaration = (constr, types) Context.Rel.Declaration.pt
 type named_context = (constr, types) Context.Named.pt
 type rel_context = (constr, types) Context.Rel.pt
 
-let in_punivs a = (a, Univ.Instance.empty)
+let in_punivs a = (a, EInstance.empty)
 
 let mkProp = of_kind (Sort (ESorts.make Sorts.prop))
 let mkSet = of_kind (Sort (ESorts.make Sorts.set))
@@ -762,6 +772,7 @@ let fresh_global ?loc ?rigid ?names env sigma reference =
 module Unsafe =
 struct
 let to_sorts = ESorts.unsafe_to_sorts
+let to_instance = EInstance.unsafe_to_instance
 let to_constr = unsafe_to_constr
 let to_rel_decl = unsafe_to_rel_decl
 let to_named_decl = unsafe_to_named_decl
-- 
cgit v1.2.3


From b824d8ad00001f6c41d0fc8bbf528dccb937c887 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 1 Apr 2017 20:25:05 +0200
Subject: Restore a fast path in EConstr instance normalization.

---
 engine/eConstr.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'engine/eConstr.ml')

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index 28e9ffdb27..bb9075e74a 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -63,7 +63,9 @@ module EInstance =
 struct
   type t = Univ.Instance.t
   let make i = i
-  let kind sigma i = Evd.normalize_universe_instance sigma i
+  let kind sigma i =
+    if Univ.Instance.is_empty i then i
+    else Evd.normalize_universe_instance sigma i
   let empty = Univ.Instance.empty
   let is_empty = Univ.Instance.is_empty
   let unsafe_to_instance t = t
-- 
cgit v1.2.3