Parsing evar instances.

13 files changed, 64 insertions, 31 deletions

diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 2bce95f1e..f59a4af32 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -176,7 +176,10 @@ let rec mlexpr_of_constr = function
                $mlexpr_of_list (mlexpr_of_list mlexpr_of_constr) substl$,[]) >>
   | Constrexpr.CPatVar (loc,n) ->
       let loc = of_coqloc loc in
-      <:expr< Constrexpr.CPatVar $dloc$ $mlexpr_of_pair mlexpr_of_bool mlexpr_of_ident n$ >>
+      <:expr< Constrexpr.CPatVar $dloc$ $mlexpr_of_ident n$ >>
+  | Constrexpr.CEvar (loc,n,[]) ->
+      let loc = of_coqloc loc in
+      <:expr< Constrexpr.CEvar $dloc$ $mlexpr_of_ident n$ [] >>
   | _ -> failwith "mlexpr_of_constr: TODO"
 
 let mlexpr_of_occ_constr =
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index ca36f4c9f..01efef940 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -149,10 +149,10 @@ let rec constr_expr_eq e1 e2 =
     constr_expr_eq t1 t2 &&
     constr_expr_eq f1 f2
   | CHole _, CHole _ -> true
-  | CPatVar(_,(b1, i1)), CPatVar(_,(b2, i2)) ->
-    (b1 : bool) == b2 && Id.equal i1 i2
+  | CPatVar(_,i1), CPatVar(_,i2) ->
+    Id.equal i1 i2
   | CEvar (_, id1, c1), CEvar (_, id2, c2) ->
-    Id.equal id1 id2 && Option.equal (List.equal instance_eq) c1 c2
+    Id.equal id1 id2 && List.equal instance_eq c1 c2
   | CSort(_,s1), CSort(_,s2) ->
     Miscops.glob_sort_eq s1 s2
   | CCast(_,a1,(CastConv b1|CastVM b1)), CCast(_,a2,(CastConv b2|CastVM b2)) ->
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 9a6f8b22c..f71cf5a65 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -671,13 +671,14 @@ let rec extern inctx scopes vars r =
 
   | GVar (loc,id) -> CRef (Ident (loc,id),None)
 
-  | GEvar (loc,n,None) when !print_meta_as_hole -> CHole (loc, None, None)
+  | GEvar (loc,n,[]) when !print_meta_as_hole -> CHole (loc, None, None)
 
   | GEvar (loc,n,l) ->
-      extern_evar loc n (Option.map (List.map (on_snd (extern false scopes vars))) l)
+      extern_evar loc n (List.map (on_snd (extern false scopes vars)) l)
 
-  | GPatVar (loc,n) ->
-      if !print_meta_as_hole then CHole (loc, None, None) else CPatVar (loc,n)
+  | GPatVar (loc,(b,n)) ->
+      if !print_meta_as_hole then CHole (loc, None, None) else
+        if b then CPatVar (loc,n) else CEvar (loc,n,[])
 
   | GApp (loc,f,args) ->
       (match f with
@@ -1030,7 +1031,7 @@ let rec glob_of_pat env sigma = function
       let test id = function PVar id' -> Id.equal id id' | _ -> false in
       let l = Evd.evar_instance_array test (Evd.find sigma evk) l in
       let id = Evd.evar_ident evk sigma in
-      GEvar (loc,id,Some (List.map (on_snd (glob_of_pat env sigma)) l))
+      GEvar (loc,id,List.map (on_snd (glob_of_pat env sigma)) l)
   | PRel n ->
       let id = try match lookup_name_of_rel n env with
 	| Name id   -> id
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ff96340cd..d020a5153 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1579,14 +1579,18 @@ let internalize globalenv env allow_patvar lvar c =
           Some glb
         in
 	GHole (loc, k, solve)
+    (* Parsing pattern variables *)
     | CPatVar (loc, n) when allow_patvar ->
-	GPatVar (loc, n)
-    | CPatVar (loc, (false,n)) ->
-	GEvar (loc, n, None)
+	GPatVar (loc, (true,n))
+    | CEvar (loc, n, []) when allow_patvar ->
+	GPatVar (loc, (false,n))
+    (* end *)
+    (* Parsing existential variables *)
+    | CEvar (loc, n, l) ->
+	GEvar (loc, n, List.map (on_snd (intern env)) l)
     | CPatVar (loc, _) ->
         raise (InternalizationError (loc,IllegalMetavariable))
-    | CEvar (loc, n, l) ->
-	GEvar (loc, n, Option.map (List.map (on_snd (intern env))) l)
+    (* end *)
     | CSort (loc, s) ->
 	GSort(loc,s)
     | CCast (loc, c1, c2) ->
diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli
index bc2f7df24..f6660ff69 100644
--- a/intf/constrexpr.mli
+++ b/intf/constrexpr.mli
@@ -81,8 +81,8 @@ type constr_expr =
   | CIf of Loc.t * constr_expr * (Name.t located option * constr_expr option)
       * constr_expr * constr_expr
   | CHole of Loc.t * Evar_kinds.t option * Genarg.raw_generic_argument option
-  | CPatVar of Loc.t * (bool * patvar)
-  | CEvar of Loc.t * Glob_term.existential_name * (Id.t * constr_expr) list option
+  | CPatVar of Loc.t * patvar
+  | CEvar of Loc.t * Glob_term.existential_name * (Id.t * constr_expr) list
   | CSort of Loc.t * glob_sort
   | CCast of Loc.t * constr_expr * constr_expr cast_type
   | CNotation of Loc.t * notation * constr_notation_substitution
diff --git a/intf/glob_term.mli b/intf/glob_term.mli
index 9aca2306a..237d03366 100644
--- a/intf/glob_term.mli
+++ b/intf/glob_term.mli
@@ -32,7 +32,7 @@ type cases_pattern =
 type glob_constr =
   | GRef of (Loc.t * global_reference * glob_level list option)
   | GVar of (Loc.t * Id.t)
-  | GEvar of Loc.t * existential_name * (Id.t * glob_constr) list option
+  | GEvar of Loc.t * existential_name * (Id.t * glob_constr) list
   | GPatVar of Loc.t * (bool * patvar) (** Used for patterns only *)
   | GApp of Loc.t * glob_constr * glob_constr list
   | GLambda of Loc.t * Name.t * binding_kind *  glob_constr * glob_constr
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 272a18c3e..18012f8a1 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -193,7 +193,7 @@ GEXTEND Gram
       | "@"; f=global; i = instance; args=LIST0 NEXT -> CAppExpl(!@loc,(None,f,i),args)
       | "@"; (locid,id) = pattern_identref; args=LIST1 identref ->
           let args = List.map (fun x -> CRef (Ident x,None), None) args in
-          CApp(!@loc,(None,CPatVar(locid,(true,id))),args) ]
+          CApp(!@loc,(None,CPatVar(locid,id)),args) ]
     | "9"
         [ ".."; c = operconstr LEVEL "0"; ".." ->
           CAppExpl (!@loc,(None,Ident (!@loc,ldots_var),None),[c]) ]
@@ -289,7 +289,14 @@ GEXTEND Gram
       | n=INT -> CPrim (!@loc, Numeral (Bigint.of_string n))
       | s=string -> CPrim (!@loc, String s)
       | "_" -> CHole (!@loc, None, None)
-      | id=pattern_ident -> CPatVar(!@loc,(false,id)) ] ]
+      | id=pattern_ident; inst = evar_instance -> CEvar(!@loc,id,inst) ] ]
+  ;
+  inst:
+    [ [ id = ident; ":="; c = lconstr -> (id,c) ] ]
+  ;
+  evar_instance:
+    [ [ "@{"; l = LIST1 inst SEP ","; "}" -> l
+      | -> [] ] ]
   ;
   instance:
     [ [ "@{"; l = LIST1 level; "}" -> Some l
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 3bd23a802..b59f67bc3 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -405,7 +405,7 @@ let rec detype isgoal avoid env sigma t =
     | Meta n ->
 	(* Meta in constr are not user-parsable and are mapped to Evar *)
         (* using numbers to be unparsable *)
-	GEvar (dl, Id.of_string (string_of_int n), None)
+	GEvar (dl, Id.of_string (string_of_int n), [])
     | Var id ->
 	(try let _ = Global.lookup_named id in GRef (dl, VarRef id, None)
 	 with Not_found -> GVar (dl, id))
@@ -439,10 +439,10 @@ let rec detype isgoal avoid env sigma t =
     | Evar (evk,cl) ->
       let id,l =
         try Evd.evar_ident evk sigma,
-            Some (Evd.evar_instance_array isVarId (Evd.find sigma evk) cl)
-        with Not_found -> Id.of_string ("X" ^ string_of_int (Evar.repr evk)), None in
+            Evd.evar_instance_array isVarId (Evd.find sigma evk) cl
+        with Not_found -> Id.of_string ("X" ^ string_of_int (Evar.repr evk)), [] in
         GEvar (dl,id,
-               Option.map (List.map (on_snd (detype isgoal avoid env sigma))) l)
+               List.map (on_snd (detype isgoal avoid env sigma)) l)
     | Ind (ind_sp,u) ->
 	GRef (dl, IndRef ind_sp, detype_instance u)
     | Construct (cstr_sp,u) ->
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 17928f26e..4dc3672a4 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -279,6 +279,22 @@ let instantiate_evar_array info c args =
   | [] -> c
   | _ -> replace_vars inst c
 
+let complete_instance hyps update =
+  let oldinst = List.map (fun (id,_,_) -> mkVar id) hyps in
+  let rec aux seen newinst = function
+    | [] -> newinst
+    | (id,c) :: l ->
+        if List.mem id seen then
+          user_err_loc (Loc.ghost,"",pr_id id ++ str "appears more than once.")
+        else
+          let l1,l2 = List.split_when (fun c -> isVarId id c) newinst in
+          match l2 with
+          | [] ->
+              user_err_loc (Loc.ghost,"",str "No such variable in the signature of the existential variable: " ++ pr_id id)
+          | _::tl ->
+              aux (id::seen) (l1 @ c :: tl) l in
+  Array.of_list (aux [] oldinst update)
+
 module StringOrd = struct type t = string let compare = String.compare end
 module UNameMap = struct
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 0d88415e2..2cea0eaa2 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -229,6 +229,8 @@ val evar_instance_array : (Id.t -> 'a -> bool) -> evar_info ->
 
 val instantiate_evar_array : evar_info -> constr -> constr array -> constr
 
+val complete_instance : named_context -> (Id.t * constr) list -> constr array
+
 val subst_evar_defs_light : substitution -> evar_map -> evar_map
 (** Assume empty universe constraints in [evar_map] and [conv_pbs] *)
 
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 8a4fd65a1..fb52a0481 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -65,7 +65,7 @@ let rec glob_constr_eq c1 c2 = match c1, c2 with
 | GVar (_, id1), GVar (_, id2) -> Id.equal id1 id2
 | GEvar (_, id1, arg1), GEvar (_, id2, arg2) ->
   Id.equal id1 id2 &&
-  Option.equal (fun l1 l2 -> List.equal instance_eq l1 l2) arg1 arg2
+  List.equal instance_eq arg1 arg2
 | GPatVar (_, (b1, pat1)), GPatVar (_, (b2, pat2)) ->
   (b1 : bool) == b2 && Id.equal pat1 pat2
 | GApp (_, f1, arg1), GApp (_, f2, arg2) ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f26d2d638..a21548d57 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -407,7 +407,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
       (pretype_id (fun e r l t -> pretype tycon e r l t) loc env evdref lvar id)
       tycon
 
-  | GEvar (loc, id, instopt) ->
+  | GEvar (loc, id, inst) ->
       (* Ne faudrait-il pas s'assurer que hyps est bien un
 	 sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *)
       let evk =
@@ -415,9 +415,9 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
         with Not_found ->
           user_err_loc (loc,"",str "Unknown existential variable.") in
       let hyps = evar_filtered_context (Evd.find !evdref evk) in
-      let args = match instopt with
-        | None -> Array.of_list (instance_from_named_context hyps)
-        | Some inst -> error "Non-identity subtitutions of existential variables not implemented" in
+      let f c = (pretype empty_tycon env evdref lvar c).uj_val in
+      let inst = List.map (on_snd f) inst in
+      let args = complete_instance hyps inst in
       let c = mkEvar (evk, args) in
       let j = (Retyping.get_judgment_of env !evdref c) in
 	inh_conv_coerce_to_tycon loc env evdref j tycon
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 6956ec448..baafbc04f 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -177,8 +177,8 @@ let pr_prim_token = function
 let pr_evar pr id l =
   hov 0 (str "?" ++ pr_id id ++
   (match l with
-   | None | Some [] -> mt()
-   | Some l ->
+   | [] -> mt()
+   | l ->
        let f (id,c) = pr_id id ++ str ":=" ++ pr ltop c in
        str"@{" ++ hov 0 (prlist_with_sep pr_comma f l) ++ str"}"))
 
@@ -554,7 +554,7 @@ let pr pr sep inherited a =
 
   | CHole _ -> str "_", latom
   | CEvar (_,n,l) -> pr_evar (pr mt) n l, latom
-  | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom
+  | CPatVar (_,p) -> str "?" ++ pr_patvar p, latom
   | CSort (_,s) -> pr_glob_sort s, latom
   | CCast (_,a,b) ->
       hv 0 (pr mt (lcast,L) a ++ cut () ++