diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-11 20:00:27 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-09-12 10:39:32 +0200 |
commit | ca300977724a6b065a98c025d400c71f41b9df4b (patch) | |
tree | 59a2fd3327b3d0eb9cd1e11cbb31605f2a08ea27 | |
parent | 012fe1a96ba81ab0a7fa210610e3f25187baaf1d (diff) |
Parsing evar instances.
-rw-r--r-- | grammar/q_coqast.ml4 | 5 | ||||
-rw-r--r-- | interp/constrexpr_ops.ml | 6 | ||||
-rw-r--r-- | interp/constrextern.ml | 11 | ||||
-rw-r--r-- | interp/constrintern.ml | 14 | ||||
-rw-r--r-- | intf/constrexpr.mli | 4 | ||||
-rw-r--r-- | intf/glob_term.mli | 2 | ||||
-rw-r--r-- | parsing/g_constr.ml4 | 11 | ||||
-rw-r--r-- | pretyping/detyping.ml | 8 | ||||
-rw-r--r-- | pretyping/evd.ml | 16 | ||||
-rw-r--r-- | pretyping/evd.mli | 2 | ||||
-rw-r--r-- | pretyping/glob_ops.ml | 2 | ||||
-rw-r--r-- | pretyping/pretyping.ml | 8 | ||||
-rw-r--r-- | printing/ppconstr.ml | 6 |
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 () ++ |