Replacing "cast surgery" in LetIn by a proper field (see PR #404).

This is a patch fulfilling the relevant remark of Maxime that an
explicit information at the ML type level would be better than "cast
surgery" to carry the optional type of a let-in.

There are a very few semantic changes.
- a "(x:t:=c)" in a block of binders is now written in the more
  standard way "(x:=c:t)"
- in notations, the type of a let-in is not displayed if not
  explicitly asked so.

See discussion at PR #417 for more information.

5 files changed, 59 insertions, 42 deletions

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 5ec44a68d..1cae8d16d 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -264,7 +264,11 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
 	  sorec ((na1,na2,c2)::ctx) (Environ.push_rel (LocalAssum (na2,c2)) env)
             (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
 
-      | PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) ->
+      | PLetIn (na1,c1,Some t1,d1), LetIn(na2,c2,t2,d2) ->
+	  sorec ((na1,na2,t2)::ctx) (Environ.push_rel (LocalDef (na2,c2,t2)) env)
+            (add_binders na1 na2 binding_vars (sorec ctx env (sorec ctx env subst c1 c2) t1 t2)) d1 d2
+
+      | PLetIn (na1,c1,None,d1), LetIn(na2,c2,t2,d2) ->
 	  sorec ((na1,na2,t2)::ctx) (Environ.push_rel (LocalDef (na2,c2,t2)) env)
             (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index cad5551c1..5a296de84 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -331,7 +331,7 @@ let extract_nondep_branches test c b l =
     match r,l with
       | r, [] -> r
       | GLambda (_,_,_,_,t), false::l -> strip l t
-      | GLetIn (_,_,_,t), true::l -> strip l t
+      | GLetIn (_,_,_,_,t), true::l -> strip l t
       (* FIXME: do we need adjustment? *)
       | _,_ -> assert false in
   if test c l then Some (strip l b) else None
@@ -341,7 +341,7 @@ let it_destRLambda_or_LetIn_names l c =
     match c, l with
       | _, [] -> (List.rev nal,c)
       | GLambda (_,na,_,_,c), false::l -> aux l (na::nal) c
-      | GLetIn (_,na,_,c), true::l -> aux l (na::nal) c
+      | GLetIn (_,na,_,_,c), true::l -> aux l (na::nal) c
       | _, true::l -> (* let-expansion *) aux l (Anonymous :: nal) c
       | _, false::l ->
           (* eta-expansion *)
@@ -690,9 +690,8 @@ and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c =
       let c = detype (lax,false) avoid env sigma (Option.get body) in
       (* Heuristic: we display the type if in Prop *)
       let s = try Retyping.get_sort_family_of (snd env) sigma ty with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in
-      let c = if s != InProp then c else
-          GCast (dl, c, CastConv (detype (lax,false) avoid env sigma ty)) in
-      GLetIn (dl, na', c, r)
+      let t = if s != InProp then None else Some (detype (lax,false) avoid env sigma ty) in
+      GLetIn (dl, na', c, t, r)
 
 let detype_rel_context ?(lax=false) where avoid env sigma sign =
   let where = Option.map (fun c -> it_mkLambda_or_LetIn c sign) where in
@@ -764,9 +763,9 @@ let detype_closed_glob ?lax isgoal avoid env sigma t =
     | GProd (loc,id,k,t,c) ->
         let id = convert_name cl id in
         GProd(loc,id,k,detype_closed_glob cl t, detype_closed_glob cl c)
-    | GLetIn (loc,id,b,e) ->
+    | GLetIn (loc,id,b,t,e) ->
         let id = convert_name cl id in
-        GLetIn(loc,id,detype_closed_glob cl b, detype_closed_glob cl e)
+        GLetIn(loc,id,detype_closed_glob cl b, Option.map (detype_closed_glob cl) t, detype_closed_glob cl e)
     | GLetTuple (loc,ids,(n,r),b,e) ->
         let ids = List.map (convert_name cl) ids in
         let n = convert_name cl n in
@@ -825,10 +824,12 @@ let rec subst_glob_constr subst raw =
 	if r1' == r1 && r2' == r2 then raw else
 	  GProd (loc,n,bk,r1',r2')
 
-  | GLetIn (loc,n,r1,r2) ->
-      let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in
-	if r1' == r1 && r2' == r2 then raw else
-	  GLetIn (loc,n,r1',r2')
+  | GLetIn (loc,n,r1,t,r2) ->
+      let r1' = subst_glob_constr subst r1 in
+      let t' = Option.smartmap (subst_glob_constr subst) t in
+      let r2' = subst_glob_constr subst r2 in
+	if r1' == r1 && t == t' && r2' == r2 then raw else
+	  GLetIn (loc,n,r1',t',r2')
 
   | GCases (loc,sty,rtno,rl,branches) ->
       let rtno' = Option.smartmap (subst_glob_constr subst) rtno
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 51660818f..ebbfa195f 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -77,8 +77,8 @@ let rec glob_constr_eq c1 c2 = match c1, c2 with
 | GProd (_, na1, bk1, t1, c1), GProd (_, na2, bk2, t2, c2) ->
   Name.equal na1 na2 && binding_kind_eq bk1 bk2 &&
   glob_constr_eq t1 t2 && glob_constr_eq c1 c2
-| GLetIn (_, na1, t1, c1), GLetIn (_, na2, t2, c2) ->
-  Name.equal na1 na2 && glob_constr_eq t1 t2 && glob_constr_eq c1 c2
+| GLetIn (_, na1, b1, t1, c1), GLetIn (_, na2, b2, t2, c2) ->
+  Name.equal na1 na2 && glob_constr_eq b1 b2 && Option.equal glob_constr_eq t1 t2 && glob_constr_eq c1 c2
 | GCases (_, st1, c1, tp1, cl1), GCases (_, st2, c2, tp2, cl2) ->
   case_style_eq st1 st2 && Option.equal glob_constr_eq c1 c2 &&
   List.equal tomatch_tuple_eq tp1 tp2 &&
@@ -152,10 +152,11 @@ let map_glob_constr_left_to_right f = function
       let comp1 = f ty in
       let comp2 = f c in
       GProd (loc,na,bk,comp1,comp2)
-  | GLetIn (loc,na,b,c) ->
+  | GLetIn (loc,na,b,t,c) ->
       let comp1 = f b in
+      let compt = Option.map f t in
       let comp2 = f c in
-      GLetIn (loc,na,comp1,comp2)
+      GLetIn (loc,na,comp1,compt,comp2)
   | GCases (loc,sty,rtntypopt,tml,pl) ->
       let comp1 = Option.map f rtntypopt in
       let comp2 = Util.List.map_left (fun (tm,x) -> (f tm,x)) tml in
@@ -189,8 +190,10 @@ let fold_return_type f acc (na,tyopt) = Option.fold_left f acc tyopt
 let fold_glob_constr f acc = function
   | GVar _ -> acc
   | GApp (_,c,args) -> List.fold_left f (f acc c) args
-  | GLambda (_,_,_,b,c) | GProd (_,_,_,b,c) | GLetIn (_,_,b,c) ->
+  | GLambda (_,_,_,b,c) | GProd (_,_,_,b,c) ->
     f (f acc b) c
+  | GLetIn (_,_,b,t,c) ->
+    f (Option.fold_left f (f acc b) t) c
   | GCases (_,_,rtntypopt,tml,pl) ->
     let fold_pattern acc (_,idl,p,c) = f acc c in
     List.fold_left fold_pattern
@@ -225,8 +228,8 @@ let occur_glob_constr id =
       (occur ty) || (not (same_id na id) && (occur c))
     | GProd (loc,na,bk,ty,c) ->
       (occur ty) || (not (same_id na id) && (occur c))
-    | GLetIn (loc,na,b,c) ->
-      (occur b) || (not (same_id na id) && (occur c))
+    | GLetIn (loc,na,b,t,c) ->
+      (Option.fold_left (fun b t -> occur t || b) (occur b) t) || (not (same_id na id) && (occur c))
     | GCases (loc,sty,rtntypopt,tml,pl) ->
 	(occur_option rtntypopt)
         || (List.exists (fun (tm,_) -> occur tm) tml)
@@ -270,10 +273,15 @@ let free_glob_vars =
   let rec vars bounded vs = function
     | GVar (loc,id') -> if Id.Set.mem id' bounded then vs else Id.Set.add id' vs
     | GApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args)
-    | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) | GLetIn (loc,na,ty,c) ->
+    | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) ->
 	let vs' = vars bounded vs ty in
 	let bounded' = add_name_to_ids bounded na in
        vars bounded' vs' c
+    | GLetIn (loc,na,b,ty,c) ->
+	let vs' = vars bounded vs b in
+	let vs'' = Option.fold_left (vars bounded) vs' ty in
+	let bounded' = add_name_to_ids bounded na in
+       vars bounded' vs'' c
     | GCases (loc,sty,rtntypopt,tml,pl) ->
 	let vs1 = vars_option bounded vs rtntypopt in
 	let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in
@@ -346,7 +354,7 @@ let add_and_check_ident id set =
 
 let bound_glob_vars =
   let rec vars bound = function
-    | GLambda (_,na,_,_,_) | GProd (_,na,_,_,_) | GLetIn (_,na,_,_) as c ->
+    | GLambda (_,na,_,_,_) | GProd (_,na,_,_,_) | GLetIn (_,na,_,_,_) as c ->
         let bound = name_fold add_and_check_ident na bound in
         fold_glob_constr vars bound c
     | GCases (loc,sty,rtntypopt,tml,pl) ->
@@ -460,7 +468,7 @@ let loc_of_glob_constr = function
   | GApp (loc,_,_) -> loc
   | GLambda (loc,_,_,_,_) -> loc
   | GProd (loc,_,_,_,_) -> loc
-  | GLetIn (loc,_,_,_) -> loc
+  | GLetIn (loc,_,_,_,_) -> loc
   | GCases (loc,_,_,_,_) -> loc
   | GLetTuple (loc,_,_,_,_) -> loc
   | GIf (loc,_,_,_,_) -> loc
@@ -512,9 +520,9 @@ let rec rename_glob_vars l = function
   | GLambda (loc,na,bk,t,c) ->
       let na',l' = update_subst na l in
       GLambda (loc,na',bk,rename_glob_vars l t,rename_glob_vars l' c)
-  | GLetIn (loc,na,b,c) ->
+  | GLetIn (loc,na,b,t,c) ->
       let na',l' = update_subst na l in
-      GLetIn (loc,na',rename_glob_vars l b,rename_glob_vars l' c)
+      GLetIn (loc,na',rename_glob_vars l b,Option.map (rename_glob_vars l) t,rename_glob_vars l' c)
   (* Lazy strategy: we fail if a collision with renaming occurs, rather than renaming further *)
   | GCases (loc,ci,po,tomatchl,cls) ->
       let test_pred_pat (na,ino) =
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 977d3dae1..79765a493 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -44,8 +44,9 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
   Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2
 | PProd (v1, t1, b1), PProd (v2, t2, b2) ->
   Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2
-| PLetIn (v1, t1, b1), PLetIn (v2, t2, b2) ->
-  Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2
+| PLetIn (v1, b1, t1, c1), PLetIn (v2, b2, t2, c2) ->
+  Name.equal v1 v2 && constr_pattern_eq b1 b2 &&
+  Option.equal constr_pattern_eq t1 t2 && constr_pattern_eq c1 c2
 | PSort s1, PSort s2 -> Miscops.glob_sort_eq s1 s2
 | PMeta m1, PMeta m2 -> Option.equal Id.equal m1 m2
 | PIf (t1, l1, r1), PIf (t2, l2, r2) ->
@@ -85,7 +86,8 @@ let rec occur_meta_pattern = function
   | PProj (_,arg) -> occur_meta_pattern arg
   | PLambda (na,t,c)  -> (occur_meta_pattern t) || (occur_meta_pattern c)
   | PProd (na,t,c)  -> (occur_meta_pattern t) || (occur_meta_pattern c)
-  | PLetIn (na,t,c)  -> (occur_meta_pattern t) || (occur_meta_pattern c)
+  | PLetIn (na,b,t,c)  ->
+     Option.fold_left (fun b t -> b || occur_meta_pattern t) (occur_meta_pattern b) t || (occur_meta_pattern c)
   | PIf (c,c1,c2)  ->
       (occur_meta_pattern c) ||
       (occur_meta_pattern c1) || (occur_meta_pattern c2)
@@ -101,7 +103,7 @@ exception BoundPattern;;
 let rec head_pattern_bound t =
   match t with
     | PProd (_,_,b)  -> head_pattern_bound b
-    | PLetIn (_,_,b) -> head_pattern_bound b
+    | PLetIn (_,_,_,b) -> head_pattern_bound b
     | PApp (c,args)  -> head_pattern_bound c
     | PIf (c,_,_)  -> head_pattern_bound c
     | PCase (_,p,c,br) -> head_pattern_bound c
@@ -132,7 +134,7 @@ let pattern_of_constr env sigma t =
     | Sort (Prop Pos) -> PSort GSet
     | Sort (Type _) -> PSort (GType [])
     | Cast (c,_,_)      -> pattern_of_constr env c
-    | LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c,
+    | LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c,Some (pattern_of_constr env t),
 				  pattern_of_constr (push_rel (LocalDef (na,c,t)) env) b)
     | Prod (na,c,b)   -> PProd (na,pattern_of_constr env c,
 				pattern_of_constr (push_rel (LocalAssum (na, c)) env) b)
@@ -189,7 +191,7 @@ let map_pattern_with_binders g f l = function
   | PSoApp (n,pl) -> PSoApp (n, List.map (f l) pl)
   | PLambda (n,a,b) -> PLambda (n,f l a,f (g n l) b)
   | PProd (n,a,b) -> PProd (n,f l a,f (g n l) b)
-  | PLetIn (n,a,b) -> PLetIn (n,f l a,f (g n l) b)
+  | PLetIn (n,a,t,b) -> PLetIn (n,f l a,Option.map (f l) t,f (g n l) b)
   | PIf (c,b1,b2) -> PIf (f l c,f l b1,f l b2)
   | PCase (ci,po,p,pl) ->
     PCase (ci,f l po,f l p, List.map (fun (i,n,c) -> (i,n,f l c)) pl)
@@ -274,11 +276,12 @@ let rec subst_pattern subst pat =
       let c2' = subst_pattern subst c2 in
 	if c1' == c1 && c2' == c2 then pat else
 	  PProd (name,c1',c2')
-  | PLetIn (name,c1,c2) ->
+  | PLetIn (name,c1,t,c2) ->
       let c1' = subst_pattern subst c1 in
+      let t' = Option.smartmap (subst_pattern subst) t in
       let c2' = subst_pattern subst c2 in
-	if c1' == c1 && c2' == c2 then pat else
-	  PLetIn (name,c1',c2')
+	if c1' == c1 && t' == t && c2' == c2 then pat else
+	  PLetIn (name,c1',t',c2')
   | PSort _
   | PMeta _ -> pat
   | PIf (c,c1,c2) ->
@@ -343,9 +346,10 @@ let rec pat_of_raw metas vars = function
       name_iter (fun n -> metas := n::!metas) na;
       PProd (na, pat_of_raw metas vars c1,
 	       pat_of_raw metas (na::vars) c2)
-  | GLetIn (_,na,c1,c2) ->
+  | GLetIn (_,na,c1,t,c2) ->
       name_iter (fun n -> metas := n::!metas) na;
       PLetIn (na, pat_of_raw metas vars c1,
+               Option.map (pat_of_raw metas vars) t,
 	       pat_of_raw metas (na::vars) c2)
   | GSort (_,s) ->
       PSort s
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f92110ea5..15a48a6a3 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -810,14 +810,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
         iraise (e, info) in
       inh_conv_coerce_to_tycon loc env evdref resj tycon
 
-  | GLetIn(loc,name,c1,c2)      ->
-    let j =
-      match c1 with
-      | GCast (loc, c, CastConv t) ->
-	let tj = pretype_type empty_valcon env evdref lvar t in
-	  pretype (mk_tycon tj.utj_val) env evdref lvar c
-      | _ -> pretype empty_tycon env evdref lvar c1
-    in
+  | GLetIn(loc,name,c1,t,c2)      ->
+    let tycon1 =
+      match t with
+      | Some t ->
+	 mk_tycon (pretype_type empty_valcon env evdref lvar t).utj_val
+      | None ->
+         empty_tycon in
+    let j = pretype tycon1 env evdref lvar c1 in
     let t = evd_comb1 (Evarsolve.refresh_universes
       ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env)
       evdref j.uj_type in