1 files changed, 62 insertions, 39 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index 3dfb0c34..a343ad3c 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -22,11 +22,13 @@ module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 module CompactedDecl = Context.Compacted.Declaration
 
+module Internal = struct
+
 (* Sorts and sort family *)
 
 let print_sort = function
-  | Prop Pos -> (str "Set")
-  | Prop Null -> (str "Prop")
+  | Set -> (str "Set")
+  | Prop -> (str "Prop")
   | Type u -> (str "Type(" ++ Univ.Universe.pr u ++ str ")")
 
 let pr_sort_family = function
@@ -47,7 +49,9 @@ let pr_fix pr_constr ((t,i),(lna,tl,bl)) =
 
 let pr_puniverses p u = 
   if Univ.Instance.is_empty u then p 
-  else p ++ str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)"
+  else p ++ str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)"
+
+(* Minimalistic constr printer, typically for debugging *)
 
 let rec pr_constr c = match kind c with
   | Rel n -> str "#"++int n
@@ -96,9 +100,16 @@ let rec pr_constr c = match kind c with
            cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++
          str"}")
 
-let term_printer = ref (fun _env _sigma c -> pr_constr (EConstr.Unsafe.to_constr c))
+let debug_print_constr c = pr_constr EConstr.Unsafe.(to_constr c)
+let debug_print_constr_env env sigma c = pr_constr EConstr.(to_constr sigma c)
+let term_printer = ref debug_print_constr_env
+
 let print_constr_env env sigma t = !term_printer env sigma t
-let print_constr t = !term_printer (Global.env()) Evd.empty t
+let print_constr t =
+  let env = Global.env () in
+  let evd = Evd.from_env env in
+  !term_printer env evd t
+
 let set_print_constr f = term_printer := f
 
 module EvMap = Evar.Map
@@ -111,11 +122,11 @@ let pr_evar_suggested_name evk sigma =
   | None -> match evi.evar_source with
   | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id
   | _,Evar_kinds.VarInstance id -> id
-  | _,Evar_kinds.QuestionMark (_,Name id) -> id
+  | _,Evar_kinds.QuestionMark {Evar_kinds.qm_name = Name id} -> id
   | _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
   | _ ->
       let env = reset_with_named_context evi.evar_hyps (Global.env()) in
-      Namegen.id_of_name_using_hdchar env sigma (EConstr.of_constr evi.evar_concl) Anonymous
+      Namegen.id_of_name_using_hdchar env sigma evi.evar_concl Anonymous
   in
   let names = EvMap.mapi base_id (undefined_map sigma) in
   let id = EvMap.find evk names in
@@ -154,7 +165,7 @@ let protect f x =
   with e -> str "EXCEPTION: " ++ str (Printexc.to_string e)
 
 let print_kconstr a =
-  protect (fun c -> print_constr (EConstr.of_constr c)) a
+  protect (fun c -> print_constr c) a
 
 let pr_meta_map evd =
   let open Evd in
@@ -197,17 +208,21 @@ let pr_evar_source = function
       let print_constr = print_kconstr in
       let id = Option.get ido in
       str "parameter " ++ Id.print id ++ spc () ++ str "of" ++
-      spc () ++ print_constr (printable_constr_of_global c)
+      spc () ++ print_constr (EConstr.of_constr @@ printable_constr_of_global c)
   | Evar_kinds.InternalHole -> str "internal placeholder"
   | Evar_kinds.TomatchTypeParameter (ind,n) ->
       let print_constr = print_kconstr in
-      pr_nth n ++ str " argument of type " ++ print_constr (mkInd ind)
+      pr_nth n ++ str " argument of type " ++ print_constr (EConstr.mkInd ind)
   | Evar_kinds.GoalEvar -> str "goal evar"
   | Evar_kinds.ImpossibleCase -> str "type of impossible pattern-matching clause"
   | Evar_kinds.MatchingVar _ -> str "matching variable"
   | Evar_kinds.VarInstance id -> str "instance of " ++ Id.print id
-  | Evar_kinds.SubEvar evk ->
-    str "subterm of " ++ Evar.print evk
+  | Evar_kinds.SubEvar (where,evk) ->
+     (match where with
+     | None -> str "subterm of "
+     | Some Evar_kinds.Body -> str "body of "
+     | Some Evar_kinds.Domain -> str "domain of "
+     | Some Evar_kinds.Codomain -> str "codomain of ") ++ Evar.print evk
 
 let pr_evar_info evi =
   let open Evd in
@@ -252,7 +267,7 @@ let compute_evar_dependency_graph sigma =
     in
     match evar_body evi with
     | Evar_empty -> acc
-    | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term c) acc
+    | Evar_defined c -> Evar.Set.fold fold_ev (evars_of_term (EConstr.Unsafe.to_constr c)) acc
   in
   Evd.fold fold sigma EvMap.empty
 
@@ -290,7 +305,7 @@ let has_no_evar sigma =
   with Exit -> false
 
 let pr_evd_level evd = UState.pr_uctx_level (Evd.evar_universe_context evd)
-let reference_of_level evd l = UState.reference_of_level (Evd.evar_universe_context evd) l
+let reference_of_level evd l = UState.qualid_of_level (Evd.evar_universe_context evd) l
 
 let pr_evar_universe_context ctx =
   let open UState in
@@ -302,7 +317,7 @@ let pr_evar_universe_context ctx =
      str"ALGEBRAIC UNIVERSES:"++brk(0,1)++
      h 0 (Univ.LSet.pr prl (UState.algebraics ctx)) ++ fnl() ++
      str"UNDEFINED UNIVERSES:"++brk(0,1)++
-     h 0 (Universes.pr_universe_opt_subst (UState.subst ctx)) ++ fnl() ++
+     h 0 (UnivSubst.pr_universe_opt_subst (UState.subst ctx)) ++ fnl() ++
      str "WEAK CONSTRAINTS:"++brk(0,1)++
      h 0 (UState.pr_weak prl ctx) ++ fnl ())
 
@@ -310,7 +325,8 @@ let print_env_short env =
   let print_constr = print_kconstr in
   let pr_rel_decl = function
     | RelDecl.LocalAssum (n,_) -> Name.print n
-    | RelDecl.LocalDef (n,b,_) -> str "(" ++ Name.print n ++ str " := " ++ print_constr b ++ str ")"
+    | RelDecl.LocalDef (n,b,_) -> str "(" ++ Name.print n ++ str " := "
+                                  ++ print_constr (EConstr.of_constr b) ++ str ")"
   in
   let pr_named_decl = NamedDecl.to_rel_decl %> pr_rel_decl in
   let nc = List.rev (named_context env) in
@@ -331,11 +347,11 @@ let pr_evar_constraints sigma pbs =
       Namegen.make_all_name_different env sigma
     in
     print_env_short env ++ spc () ++ str "|-" ++ spc () ++
-      protect (print_constr_env env sigma) (EConstr.of_constr t1) ++ spc () ++
+      protect (print_constr_env env sigma) t1 ++ spc () ++
       str (match pbty with
             | Reduction.CONV -> "=="
             | Reduction.CUMUL -> "<=") ++
-      spc () ++ protect (print_constr_env env Evd.empty) (EConstr.of_constr t2)
+      spc () ++ protect (print_constr_env env @@ Evd.from_env env) t2
   in
   prlist_with_sep fnl pr_evconstr pbs
 
@@ -429,27 +445,29 @@ let pr_metaset metas =
 
 let pr_var_decl env decl =
   let open NamedDecl in
+  let evd = Evd.from_env env in
   let pbody = match decl with
     | LocalAssum _ ->  mt ()
     | LocalDef (_,c,_) ->
 	(* Force evaluation *)
 	let c = EConstr.of_constr c in
-	let pb = print_constr_env env Evd.empty c in
+        let pb = print_constr_env env evd c in
 	  (str" := " ++ pb ++ cut () ) in
-  let pt = print_constr_env env Evd.empty (EConstr.of_constr (get_type decl)) in
+  let pt = print_constr_env env evd (EConstr.of_constr (get_type decl)) in
   let ptyp = (str" : " ++ pt) in
     (Id.print (get_id decl) ++ hov 0 (pbody ++ ptyp))
 
 let pr_rel_decl env decl =
   let open RelDecl in
+  let evd = Evd.from_env env in
   let pbody = match decl with
     | LocalAssum _ -> mt ()
     | LocalDef (_,c,_) ->
 	(* Force evaluation *)
 	let c = EConstr.of_constr c in
-	let pb = print_constr_env env Evd.empty c in
+        let pb = print_constr_env env evd c in
 	  (str":=" ++ spc () ++ pb ++ spc ()) in
-  let ptyp = print_constr_env env Evd.empty (EConstr.of_constr (get_type decl)) in
+  let ptyp = print_constr_env env evd (EConstr.of_constr (get_type decl)) in
     match get_name decl with
       | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
       | Name id -> hov 0 (Id.print id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
@@ -771,24 +789,23 @@ let map_constr_with_full_binders sigma g f l cstr =
 
 let fold_constr_with_full_binders sigma g f n acc c =
   let open RelDecl in
-  let inj c = EConstr.Unsafe.to_constr c in
   match EConstr.kind sigma c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> acc
   | Cast (c,_, t) -> f n (f n acc c) t
-  | Prod (na,t,c) -> f (g (LocalAssum (na, inj t)) n) (f n acc t) c
-  | Lambda (na,t,c) -> f (g (LocalAssum (na, inj t)) n) (f n acc t) c
-  | LetIn (na,b,t,c) -> f (g (LocalDef (na, inj b, inj t)) n) (f n (f n acc b) t) c
+  | Prod (na,t,c) -> f (g (LocalAssum (na, t)) n) (f n acc t) c
+  | Lambda (na,t,c) -> f (g (LocalAssum (na, t)) n) (f n acc t) c
+  | LetIn (na,b,t,c) -> f (g (LocalDef (na, b, t)) n) (f n (f n acc b) t) c
   | App (c,l) -> Array.fold_left (f n) (f n acc c) l
   | Proj (p,c) -> f n acc c
   | Evar (_,l) -> Array.fold_left (f n) acc l
   | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
   | Fix (_,(lna,tl,bl)) ->
-      let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, inj t)) c) n lna tl in
+      let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, t)) c) n lna tl in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
       Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
   | CoFix (_,(lna,tl,bl)) ->
-      let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, inj t)) c) n lna tl in
+      let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n, t)) c) n lna tl in
       let fd = Array.map2 (fun t b -> (t,b)) tl bl in
       Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
 
@@ -847,6 +864,13 @@ let occur_meta_or_existential sigma c =
     | _ -> EConstr.iter sigma occrec c
   in try occrec c; false with Occur -> true
 
+let occur_metavariable sigma m c =
+  let rec occrec c = match EConstr.kind sigma c with
+  | Meta m' -> if Int.equal m m' then raise Occur
+  | _ -> EConstr.iter sigma occrec c
+  in
+  try occrec c; false with Occur -> true
+
 let occur_evar sigma n c =
   let rec occur_rec c = match EConstr.kind sigma c with
     | Evar (sp,_) when Evar.equal sp n -> raise Occur
@@ -926,7 +950,7 @@ let dependent_main noevar sigma m t =
       match EConstr.kind sigma m, EConstr.kind sigma t with
 	| App (fm,lm), App (ft,lt) when Array.length lm < Array.length lt ->
 	    deprec m (mkApp (ft,Array.sub lt 0 (Array.length lm)));
-	    CArray.Fun1.iter deprec m
+            Array.Fun1.iter deprec m
 	      (Array.sub lt
 		(Array.length lm) ((Array.length lt) - (Array.length lm)))
 	| _, Cast (c,_,_) when noevar && isMeta sigma c -> ()
@@ -964,9 +988,6 @@ let count_occurrences sigma m t =
   countrec m t;
   !n
 
-(* Synonymous *)
-let occur_term = dependent
-
 let pop t = EConstr.Vars.lift (-1) t
 
 (***************************)
@@ -1149,15 +1170,14 @@ let is_template_polymorphic env sigma f =
 
 let base_sort_cmp pb s0 s1 =
   match (s0,s1) with
-    | (Prop c1, Prop c2) -> c1 == Null || c2 == Pos  (* Prop <= Set *)
-    | (Prop c1, Type u)  -> pb == Reduction.CUMUL
-    | (Type u1, Type u2) -> true
-    | _ -> false
+  | Prop, Prop | Set, Set | Type _, Type _ -> true
+  | Prop, Set | Prop, Type _ | Set, Type _ -> pb == Reduction.CUMUL
+  | Set, Prop | Type _, Prop | Type _, Set -> false
 
 let rec is_Prop sigma c = match EConstr.kind sigma c with
   | Sort u ->
     begin match EConstr.ESorts.kind sigma u with
-    | Prop Null -> true
+    | Prop -> true
     | _ -> false
     end
   | Cast (c,_,_) -> is_Prop sigma c
@@ -1166,7 +1186,7 @@ let rec is_Prop sigma c = match EConstr.kind sigma c with
 let rec is_Set sigma c = match EConstr.kind sigma c with
   | Sort u ->
     begin match EConstr.ESorts.kind sigma u with
-    | Prop Pos -> true
+    | Set -> true
     | _ -> false
     end
   | Cast (c,_,_) -> is_Set sigma c
@@ -1369,7 +1389,7 @@ let smash_rel_context sign =
 let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init
 
 let mem_named_context_val id ctxt =
-  try ignore(Environ.lookup_named_val id ctxt); true with Not_found -> false
+  try ignore(Environ.lookup_named_ctxt id ctxt); true with Not_found -> false
 
 let map_rel_decl f = function
 | RelDecl.LocalAssum (id, t) -> RelDecl.LocalAssum (id, f t)
@@ -1495,3 +1515,6 @@ let env_rel_context_chop k env =
   let ctx1,ctx2 = List.chop k rels in
   push_rel_context ctx2 (reset_with_named_context (named_context_val env) env),
   ctx1
+end
+
+include Internal