1 files changed, 115 insertions, 84 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index b7d89ba7b..f698f8151 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -15,6 +15,9 @@ open Term
 open Vars
 open Environ
 
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
 (* Sorts and sort family *)
 
 let print_sort = function
@@ -98,26 +101,28 @@ let print_constr_env t = !term_printer t
 let print_constr t = !term_printer (Global.env()) t
 let set_print_constr f = term_printer := f
 
-let pr_var_decl env (id,c,typ) =
-  let pbody = match c with
-    | None ->  (mt ())
-    | Some c ->
+let pr_var_decl env decl =
+  let open NamedDecl in
+  let pbody = match decl with
+    | LocalAssum _ ->  mt ()
+    | LocalDef (_,c,_) ->
 	(* Force evaluation *)
 	let pb = print_constr_env env c in
 	  (str" := " ++ pb ++ cut () ) in
-  let pt = print_constr_env env typ in
+  let pt = print_constr_env env (get_type decl) in
   let ptyp = (str" : " ++ pt) in
-    (pr_id id ++ hov 0 (pbody ++ ptyp))
+    (pr_id (get_id decl) ++ hov 0 (pbody ++ ptyp))
 
-let pr_rel_decl env (na,c,typ) =
-  let pbody = match c with
-    | None -> mt ()
-    | Some c ->
+let pr_rel_decl env decl =
+  let open RelDecl in
+  let pbody = match decl with
+    | LocalAssum _ -> mt ()
+    | LocalDef (_,c,_) ->
 	(* Force evaluation *)
 	let pb = print_constr_env env c in
 	  (str":=" ++ spc () ++ pb ++ spc ()) in
-  let ptyp = print_constr_env env typ in
-    match na with
+  let ptyp = print_constr_env env (get_type decl) in
+    match get_name decl with
       | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
       | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
 
@@ -157,42 +162,53 @@ let rel_list n m =
   in
   reln [] 1
 
-let push_rel_assum (x,t) env = push_rel (x,None,t) env
+let push_rel_assum (x,t) env =
+  let open RelDecl in
+  push_rel (LocalAssum (x,t)) env
 
 let push_rels_assum assums =
-  push_rel_context (List.map (fun (x,t) -> (x,None,t)) assums)
+  let open RelDecl in
+  push_rel_context (List.map (fun (x,t) -> LocalAssum (x,t)) assums)
 
 let push_named_rec_types (lna,typarray,_) env =
+  let open NamedDecl in
   let ctxt =
     Array.map2_i
       (fun i na t ->
 	 match na with
-	   | Name id -> (id, None, lift i t)
+	   | Name id -> LocalAssum (id, lift i t)
 	   | Anonymous -> anomaly (Pp.str "Fix declarations must be named"))
       lna typarray in
   Array.fold_left
     (fun e assum -> push_named assum e) env ctxt
 
 let lookup_rel_id id sign =
+  let open RelDecl in
   let rec lookrec n = function
-    | []                     -> raise Not_found
-    | (Anonymous, _, _) :: l -> lookrec (n + 1) l
-    | (Name id', b, t) :: l  ->
-      if Names.Id.equal id' id then (n, b, t) else lookrec (n + 1) l
+    | [] ->
+        raise Not_found
+    | (LocalAssum (Anonymous, _) | LocalDef (Anonymous,_,_)) :: l ->
+        lookrec (n + 1) l
+    | LocalAssum (Name id', t) :: l  ->
+        if Names.Id.equal id' id then (n,None,t)  else lookrec (n + 1) l
+    | LocalDef (Name id', b, t) :: l  ->
+        if Names.Id.equal id' id then (n,Some b,t) else lookrec (n + 1) l
   in
   lookrec 1 sign
 
 (* Constructs either [forall x:t, c] or [let x:=b:t in c] *)
-let mkProd_or_LetIn (na,body,t) c =
-  match body with
-    | None -> mkProd (na, t, c)
-    | Some b -> mkLetIn (na, b, t, c)
+let mkProd_or_LetIn decl c =
+  let open RelDecl in
+  match decl with
+    | LocalAssum (na,t) -> mkProd (na, t, c)
+    | LocalDef (na,b,t) -> mkLetIn (na, b, t, c)
 
 (* Constructs either [forall x:t, c] or [c] in which [x] is replaced by [b] *)
-let mkProd_wo_LetIn (na,body,t) c =
-  match body with
-    | None -> mkProd (na,  t, c)
-    | Some b -> subst1 b c
+let mkProd_wo_LetIn decl c =
+  let open RelDecl in
+  match decl with
+    | LocalAssum (na,t) -> mkProd (na, t, c)
+    | LocalDef (_,b,_) -> subst1 b c
 
 let it_mkProd init = List.fold_left (fun c (n,t)  -> mkProd (n, t, c)) init
 let it_mkLambda init = List.fold_left (fun c (n,t)  -> mkLambda (n, t, c)) init
@@ -208,10 +224,11 @@ let it_mkNamedProd_wo_LetIn init = it_named_context_quantifier mkNamedProd_wo_Le
 let it_mkNamedLambda_or_LetIn init = it_named_context_quantifier mkNamedLambda_or_LetIn ~init
 
 let it_mkLambda_or_LetIn_from_no_LetIn c decls =
+  let open RelDecl in
   let rec aux k decls c = match decls with
   | [] -> c
-  | (na,Some b,t)::decls -> mkLetIn (na,b,t,aux (k-1) decls (liftn 1 k c))
-  | (na,None,t)::decls -> mkLambda (na,t,aux (k-1) decls c)
+  | LocalDef (na,b,t) :: decls -> mkLetIn (na,b,t,aux (k-1) decls (liftn 1 k c))
+  | LocalAssum (na,t) :: decls -> mkLambda (na,t,aux (k-1) decls c)
   in aux (List.length decls) (List.rev decls) c
 
 (* *)
@@ -302,7 +319,7 @@ let map_constr_with_named_binders g f l c = match kind_of_term c with
    (co-)fixpoint) *)
 
 let fold_rec_types g (lna,typarray,_) e =
-  let ctxt = Array.map2_i (fun i na t -> (na, None, lift i t)) lna typarray in
+  let ctxt = Array.map2_i (fun i na t -> RelDecl.LocalAssum (na, lift i t)) lna typarray in
   Array.fold_left (fun e assum -> g assum e) e ctxt
 
 let map_left2 f a g b =
@@ -317,7 +334,9 @@ let map_left2 f a g b =
     r, s
   end
 
-let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
+let map_constr_with_binders_left_to_right g f l c =
+  let open RelDecl in
+  match kind_of_term c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> c
   | Cast (b,k,t) -> 
@@ -327,18 +346,18 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
       else mkCast (b',k,t')
   | Prod (na,t,b) ->
       let t' = f l t in
-      let b' = f (g (na,None,t) l) b in
+      let b' = f (g (LocalAssum (na,t)) l) b in
 	if t' == t && b' == b then c
 	else mkProd (na, t', b')
   | Lambda (na,t,b) ->
       let t' = f l t in
-      let b' = f (g (na,None,t) l) b in
+      let b' = f (g (LocalAssum (na,t)) l) b in
 	if t' == t && b' == b then c
 	else mkLambda (na, t', b')
   | LetIn (na,bo,t,b) ->
       let bo' = f l bo in
       let t' = f l t in
-      let b' = f (g (na,Some bo,t) l) b in
+      let b' = f (g (LocalDef (na,bo,t)) l) b in
 	if bo' == bo && t' == t && b' == b then c
 	else mkLetIn (na, bo', t', b')	    
   | App (c,[||]) -> assert false
@@ -379,7 +398,9 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
 	else mkCoFix (ln,(lna,tl',bl'))
 
 (* strong *)
-let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with
+let map_constr_with_full_binders g f l cstr =
+  let open RelDecl in
+  match kind_of_term cstr with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> cstr
   | Cast (c,k, t) ->
@@ -388,16 +409,16 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with
       if c==c' && t==t' then cstr else mkCast (c', k, t')
   | Prod (na,t,c) ->
       let t' = f l t in
-      let c' = f (g (na,None,t) l) c in
+      let c' = f (g (LocalAssum (na,t)) l) c in
       if t==t' && c==c' then cstr else mkProd (na, t', c')
   | Lambda (na,t,c) ->
       let t' = f l t in
-      let c' = f (g (na,None,t) l) c in
+      let c' = f (g (LocalAssum (na,t)) l) c in
       if t==t' && c==c' then cstr 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 (na,Some b,t) l) c in
+      let c' = f (g (LocalDef (na,b,t)) l) c in
       if b==b' && t==t' && c==c' then cstr else mkLetIn (na, b', t', c')
   | App (c,al) ->
       let c' = f l c in
@@ -418,7 +439,7 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with
   | Fix (ln,(lna,tl,bl)) ->
       let tl' = Array.map (f l) tl in
       let l' =
-        Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+        Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in
       let bl' = Array.map (f l') bl in
       if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
       then cstr
@@ -426,7 +447,7 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with
   | CoFix(ln,(lna,tl,bl)) ->
       let tl' = Array.map (f l) tl in
       let l' =
-        Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+        Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in
       let bl' = Array.map (f l') bl in
       if Array.for_all2 (==) tl tl' && Array.for_all2 (==) bl bl'
       then cstr
@@ -439,23 +460,25 @@ let map_constr_with_full_binders g f l cstr = match kind_of_term cstr with
    index) which is processed by [g] (which typically add 1 to [n]) at
    each binder traversal; it is not recursive *)
 
-let fold_constr_with_full_binders g f n acc c = match kind_of_term c with
+let fold_constr_with_full_binders g f n acc c =
+  let open RelDecl in
+  match kind_of_term 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 (na,None,t) n) (f n acc t) c
-  | Lambda (na,t,c) -> f (g (na,None,t) n) (f n acc t) c
-  | LetIn (na,b,t,c) -> f (g (na,Some b,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 (n,None,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 (n,None,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
 
@@ -467,23 +490,25 @@ let fold_constr_with_binders g f n acc c =
    each binder traversal; it is not recursive and the order with which
    subterms are processed is not specified *)
 
-let iter_constr_with_full_binders g f l c = match kind_of_term c with
+let iter_constr_with_full_binders g f l c =
+  let open RelDecl in
+  match kind_of_term c with
   | (Rel _ | Meta _ | Var _   | Sort _ | Const _ | Ind _
     | Construct _) -> ()
   | Cast (c,_, t) -> f l c; f l t
-  | Prod (na,t,c) -> f l t; f (g (na,None,t) l) c
-  | Lambda (na,t,c) -> f l t; f (g (na,None,t) l) c
-  | LetIn (na,b,t,c) -> f l b; f l t; f (g (na,Some b,t) l) c
+  | Prod (na,t,c) -> f l t; f (g (LocalAssum (na,t)) l) c
+  | Lambda (na,t,c) -> f l t; f (g (LocalAssum (na,t)) l) c
+  | LetIn (na,b,t,c) -> f l b; f l t; f (g (LocalDef (na,b,t)) l) c
   | App (c,args) -> f l c; Array.iter (f l) args
   | Proj (p,c) -> f l c
   | Evar (_,args) -> Array.iter (f l) args
   | Case (_,p,c,bl) -> f l p; f l c; Array.iter (f l) bl
   | Fix (_,(lna,tl,bl)) ->
-      let l' = Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+      let l' = Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in
       Array.iter (f l) tl;
       Array.iter (f l') bl
   | CoFix (_,(lna,tl,bl)) ->
-      let l' = Array.fold_left2 (fun l na t -> g (na,None,t) l) l lna tl in
+      let l' = Array.fold_left2 (fun l na t -> g (LocalAssum (na,t)) l) l lna tl in
       Array.iter (f l) tl;
       Array.iter (f l') bl
 
@@ -531,10 +556,11 @@ let occur_var env id c =
   in
   try occur_rec c; false with Occur -> true
 
-let occur_var_in_decl env hyp (_,c,typ) =
-  match c with
-    | None -> occur_var env hyp typ
-    | Some body ->
+let occur_var_in_decl env hyp decl =
+  let open NamedDecl in
+  match decl with
+    | LocalAssum (_,typ) -> occur_var env hyp typ
+    | LocalDef (_, body, typ) ->
         occur_var env hyp typ ||
         occur_var env hyp body
 
@@ -593,10 +619,11 @@ let dependent_no_evar = dependent_main true false
 let dependent_univs = dependent_main false true
 let dependent_univs_no_evar = dependent_main true true
 
-let dependent_in_decl a (_,c,t) =
-  match c with
-    | None -> dependent a t
-    | Some body -> dependent a body || dependent a t
+let dependent_in_decl a decl =
+  let open NamedDecl in
+  match decl with
+    | LocalAssum (_,t) -> dependent a t
+    | LocalDef (_, body, t) -> dependent a body || dependent a t
 
 let count_occurrences m t =
   let n = ref 0 in
@@ -699,10 +726,10 @@ let replace_term = replace_term_gen eq_constr
 
 let vars_of_env env =
   let s =
-    Context.Named.fold_outside (fun (id,_,_) s -> Id.Set.add id s)
+    Context.Named.fold_outside (fun decl s -> Id.Set.add (NamedDecl.get_id decl) s)
       (named_context env) ~init:Id.Set.empty in
   Context.Rel.fold_outside
-    (fun (na,_,_) s -> match na with Name id -> Id.Set.add id s | _ -> s)
+    (fun decl s -> match RelDecl.get_name decl with Name id -> Id.Set.add id s | _ -> s)
     (rel_context env) ~init:s
 
 let add_vname vars = function
@@ -728,11 +755,11 @@ let empty_names_context = []
 
 let ids_of_rel_context sign =
   Context.Rel.fold_outside
-    (fun (na,_,_) l -> match na with Name id -> id::l | Anonymous -> l)
+    (fun decl l -> match RelDecl.get_name decl with Name id -> id::l | Anonymous -> l)
     sign ~init:[]
 
 let ids_of_named_context sign =
-  Context.Named.fold_outside (fun (id,_,_) idl -> id::idl) sign ~init:[]
+  Context.Named.fold_outside (fun decl idl -> NamedDecl.get_id decl :: idl) sign ~init:[]
 
 let ids_of_context env =
   (ids_of_rel_context (rel_context env))
@@ -740,7 +767,7 @@ let ids_of_context env =
 
 
 let names_of_rel_context env =
-  List.map (fun (na,_,_) -> na) (rel_context env)
+  List.map RelDecl.get_name (rel_context env)
 
 let is_section_variable id =
   try let _ = Global.lookup_named id in true
@@ -813,7 +840,7 @@ let filtering env cv_pb c1 c2 =
         end
       | Prod (n,t1,c1), Prod (_,t2,c2) ->
 	  aux env cv_pb t1 t2;
-	  aux ((n,None,t1)::env) cv_pb c1 c2
+	  aux (RelDecl.LocalAssum (n,t1) :: env) cv_pb c1 c2
       | _, Evar (ev,_) -> define cv_pb env ev c1
       | Evar (ev,_), _ -> define cv_pb env ev c2
       | _ ->
@@ -826,8 +853,8 @@ let filtering env cv_pb c1 c2 =
 
 let decompose_prod_letin : constr -> int * Context.Rel.t * constr =
   let rec prodec_rec i l c = match kind_of_term c with
-    | Prod (n,t,c)    -> prodec_rec (succ i) ((n,None,t)::l) c
-    | LetIn (n,d,t,c) -> prodec_rec (succ i) ((n,Some d,t)::l) c
+    | Prod (n,t,c)    -> prodec_rec (succ i) (RelDecl.LocalAssum (n,t)::l) c
+    | LetIn (n,d,t,c) -> prodec_rec (succ i) (RelDecl.LocalDef (n,d,t)::l) c
     | Cast (c,_,_)    -> prodec_rec i l c
     | _               -> i,l,c in
   prodec_rec 0 []
@@ -902,16 +929,16 @@ let process_rel_context f env =
 
 let assums_of_rel_context sign =
   Context.Rel.fold_outside
-    (fun (na,c,t) l ->
-      match c with
-          Some _ -> l
-        | None -> (na, t)::l)
+    (fun decl l ->
+      match decl with
+      | RelDecl.LocalDef _ -> l
+      | RelDecl.LocalAssum (na,t) -> (na, t)::l)
     sign ~init:[]
 
 let map_rel_context_in_env f env sign =
   let rec aux env acc = function
     | d::sign ->
-	aux (push_rel d env) (Context.Rel.Declaration.map (f env) d :: acc) sign
+	aux (push_rel d env) (RelDecl.map_constr (f env) d :: acc) sign
     | [] ->
 	acc
   in
@@ -919,7 +946,7 @@ let map_rel_context_in_env f env sign =
 
 let map_rel_context_with_binders f sign =
   let rec aux k = function
-    | d::sign -> Context.Rel.Declaration.map (f k) d :: aux (k-1) sign
+    | d::sign -> RelDecl.map_constr (f k) d :: aux (k-1) sign
     | [] -> []
   in
   aux (Context.Rel.length sign) sign
@@ -933,21 +960,23 @@ let lift_rel_context n =
 let smash_rel_context sign =
   let rec aux acc = function
   | [] -> acc
-  | (_,None,_ as d) :: l -> aux (d::acc) l
-  | (_,Some b,_) :: l ->
+  | (RelDecl.LocalAssum _ as d) :: l -> aux (d::acc) l
+  | RelDecl.LocalDef (_,b,_) :: l ->
       (* Quadratic in the number of let but there are probably a few of them *)
       aux (List.rev (substl_rel_context [b] (List.rev acc))) l
   in List.rev (aux [] sign)
 
 let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init
 
-let rec mem_named_context id = function
-  | (id',_,_) :: _ when Id.equal id id' -> true
+let rec mem_named_context id ctxt =
+  match ctxt with
+  | decl :: _ when Id.equal id (NamedDecl.get_id decl) -> true
   | _ :: sign -> mem_named_context id sign
   | [] -> false
 
 let compact_named_context_reverse sign =
-  let compact l (i1,c1,t1) =
+  let compact l decl =
+    let (i1,c1,t1) = NamedDecl.to_tuple decl in
     match l with
     | [] -> [[i1],c1,t1]
     | (l2,c2,t2)::q ->
@@ -959,16 +988,17 @@ let compact_named_context_reverse sign =
 let compact_named_context sign = List.rev (compact_named_context_reverse sign)
 
 let clear_named_body id env =
+  let open NamedDecl in
   let aux _ = function
-  | (id',Some c,t) when Id.equal id id' -> push_named (id,None,t)
+  | LocalDef (id',c,t) when Id.equal id id' -> push_named (LocalAssum (id,t))
   | d -> push_named d in
   fold_named_context aux env ~init:(reset_context env)
 
 let global_vars env ids = Id.Set.elements (global_vars_set env ids)
 
 let global_vars_set_of_decl env = function
-  | (_,None,t) -> global_vars_set env t
-  | (_,Some c,t) ->
+  | NamedDecl.LocalAssum (_,t) -> global_vars_set env t
+  | NamedDecl.LocalDef (_,c,t) ->
       Id.Set.union (global_vars_set env t)
         (global_vars_set env c)
 
@@ -976,7 +1006,8 @@ let dependency_closure env sign hyps =
   if Id.Set.is_empty hyps then [] else
     let (_,lh) =
       Context.Named.fold_inside
-        (fun (hs,hl) (x,_,_ as d) ->
+        (fun (hs,hl) d ->
+          let x = NamedDecl.get_id d in
           if Id.Set.mem x hs then
             (Id.Set.union (global_vars_set_of_decl env d) (Id.Set.remove x hs),
             x::hl)
@@ -996,7 +1027,7 @@ let on_judgment_type f j = { j with uj_type = f j.uj_type }
 let context_chop k ctx =
   let rec chop_aux acc = function
     | (0, l2) -> (List.rev acc, l2)
-    | (n, ((_,Some _,_ as h)::t)) -> chop_aux (h::acc) (n, t)
+    | (n, (RelDecl.LocalDef _ as h)::t) -> chop_aux (h::acc) (n, t)
     | (n, (h::t)) -> chop_aux (h::acc) (pred n, t)
     | (_, []) -> anomaly (Pp.str "context_chop")
   in chop_aux [] (k,ctx)