diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 09:26:08 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 09:26:08 +0000 |
commit | 9330bf650ca602884c5c4c69c2fb3e94ee32838b (patch) | |
tree | 5947d599c9c408680236995b11a47ab93703b701 | |
parent | 02077f5b5e132e135be778c201e74a5eb87b97ae (diff) |
Implemented a full-fledged equality on [constr_expr]. By the way,
some cleaning of the interface and moving of code.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16066 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | grammar/grammar.mllib | 3 | ||||
-rw-r--r-- | interp/constrexpr_ops.ml | 181 | ||||
-rw-r--r-- | interp/constrexpr_ops.mli | 54 | ||||
-rw-r--r-- | interp/constrextern.ml | 116 | ||||
-rw-r--r-- | interp/constrextern.mli | 2 | ||||
-rw-r--r-- | interp/constrintern.ml | 7 | ||||
-rw-r--r-- | interp/constrintern.mli | 5 | ||||
-rw-r--r-- | intf/constrexpr.mli | 16 | ||||
-rw-r--r-- | toplevel/command.ml | 12 |
9 files changed, 240 insertions, 156 deletions
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 757df76a6..50eac6e76 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -34,7 +34,10 @@ Argextend Tacextend Vernacextend +Nameops Redops +Miscops +Glob_ops Constrexpr_ops Locusops G_prim diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index b9469bdf3..d49219114 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -12,6 +12,7 @@ open Names open Libnames open Glob_term open Constrexpr +open Misctypes open Decl_kinds (***********************) @@ -22,6 +23,11 @@ let binding_kind_eq bk1 bk2 = match bk1, bk2 with | Implicit, Implicit -> true | _ -> false +let abstraction_kind_eq ak1 ak2 = match ak1, ak2 with +| AbsLambda, AbsLambda -> true +| AbsPi, AbsPi -> true +| _ -> false + let binder_kind_eq b1 b2 = match b1, b2 with | Default bk1, Default bk2 -> binding_kind_eq bk1 bk2 | Generalized (bk1, ck1, b1), Generalized (bk2, ck2, b2) -> @@ -40,6 +46,181 @@ let names_of_local_binders bl = (**********************************************************************) (* Functions on constr_expr *) +let prim_token_eq t1 t2 = match t1, t2 with +| Numeral i1, Numeral i2 -> Bigint.equal i1 i2 +| String s1, String s2 -> String.equal s1 s2 +| _ -> false + +let explicitation_eq ex1 ex2 = match ex1, ex2 with +| ExplByPos (i1, id1), ExplByPos (i2, id2) -> + Int.equal i1 i2 && Option.equal id_eq id1 id2 +| ExplByName id1, ExplByName id2 -> + id_eq id1 id2 +| _ -> false + +let eq_located f (_, x) (_, y) = f x y + +let rec cases_pattern_expr_eq p1 p2 = + if p1 == p2 then true + else match p1, p2 with + | CPatAlias(_,a1,i1), CPatAlias(_,a2,i2) -> + id_eq i1 i2 && cases_pattern_expr_eq a1 a2 + | CPatCstr(_,c1,a1,b1), CPatCstr(_,c2,a2,b2) -> + eq_reference c1 c2 && + List.equal cases_pattern_expr_eq a1 a2 && + List.equal cases_pattern_expr_eq b1 b2 + | CPatAtom(_,r1), CPatAtom(_,r2) -> + Option.equal eq_reference r1 r2 + | CPatOr (_, a1), CPatOr (_, a2) -> + List.equal cases_pattern_expr_eq a1 a2 + | CPatNotation (_, n1, s1, l1), CPatNotation (_, n2, s2, l2) -> + String.equal n1 n2 && + cases_pattern_notation_substitution_eq s1 s2 && + List.equal cases_pattern_expr_eq l1 l2 + | CPatPrim(_,i1), CPatPrim(_,i2) -> + prim_token_eq i1 i2 + | CPatRecord (_, l1), CPatRecord (_, l2) -> + let equal (r1, e1) (r2, e2) = + eq_reference r1 r2 && cases_pattern_expr_eq e1 e2 + in + List.equal equal l1 l2 + | CPatDelimiters(_,s1,e1), CPatDelimiters(_,s2,e2) -> + String.equal s1 s2 && cases_pattern_expr_eq e1 e2 + | _ -> false + +and cases_pattern_notation_substitution_eq (s1, n1) (s2, n2) = + List.equal cases_pattern_expr_eq s1 s2 && + List.equal (List.equal cases_pattern_expr_eq) n1 n2 + +let rec constr_expr_eq e1 e2 = + if e1 == e2 then true + else match e1, e2 with + | CRef r1, CRef r2 -> eq_reference r1 r2 + | CFix(_,id1,fl1), CFix(_,id2,fl2) -> + eq_located id_eq id1 id2 && + List.equal fix_expr_eq fl1 fl2 + | CCoFix(_,id1,fl1), CCoFix(_,id2,fl2) -> + eq_located id_eq id1 id2 && + List.equal cofix_expr_eq fl1 fl2 + | CProdN(_,bl1,a1), CProdN(_,bl2,a2) -> + List.equal binder_expr_eq bl1 bl2 && + constr_expr_eq a1 a2 + | CLambdaN(_,bl1,a1), CLambdaN(_,bl2,a2) -> + List.equal binder_expr_eq bl1 bl2 && + constr_expr_eq a1 a2 + | CLetIn(_,(_,na1),a1,b1), CLetIn(_,(_,na2),a2,b2) -> + name_eq na1 na2 && + constr_expr_eq a1 a2 && + constr_expr_eq b1 b2 + | CAppExpl(_,(proj1,r1),al1), CAppExpl(_,(proj2,r2),al2) -> + Option.equal Int.equal proj1 proj2 && + eq_reference r1 r2 && + List.equal constr_expr_eq al1 al2 + | CApp(_,(proj1,e1),al1), CApp(_,(proj2,e2),al2) -> + Option.equal Int.equal proj1 proj2 && + constr_expr_eq e1 e2 && + List.equal args_eq al1 al2 + | CRecord (_, e1, l1), CRecord (_, e2, l2) -> + let field_eq (r1, e1) (r2, e2) = + eq_reference r1 r2 && constr_expr_eq e1 e2 + in + Option.equal constr_expr_eq e1 e2 && + List.equal field_eq l1 l2 + | CCases(_,_,r1,a1,brl1), CCases(_,_,r2,a2,brl2) -> + (** Don't care about the case_style *) + Option.equal constr_expr_eq r1 r2 && + List.equal case_expr_eq a1 a2 && + List.equal branch_expr_eq brl1 brl2 + | CLetTuple (_, n1, (m1, e1), t1, b1), CLetTuple (_, n2, (m2, e2), t2, b2) -> + List.equal (eq_located name_eq) n1 n2 && + Option.equal (eq_located name_eq) m1 m2 && + Option.equal constr_expr_eq e1 e2 && + constr_expr_eq t1 t2 && + constr_expr_eq b1 b2 + | CIf (_, e1, (n1, r1), t1, f1), CIf (_, e2, (n2, r2), t2, f2) -> + constr_expr_eq e1 e2 && + Option.equal (eq_located name_eq) n1 n2 && + Option.equal constr_expr_eq r1 r2 && + constr_expr_eq t1 t2 && + constr_expr_eq f1 f2 + | CHole _, CHole _ -> true + | CPatVar(_,(b1, i1)), CPatVar(_,(b2, i2)) -> + (b1 : bool) == b2 && id_eq i1 i2 + | CEvar (_, ev1, c1), CEvar (_, ev2, c2) -> + Int.equal ev1 ev2 && + Option.equal (List.equal constr_expr_eq) c1 c2 + | CSort(_,s1), CSort(_,s2) -> + Glob_ops.glob_sort_eq s1 s2 + | CCast(_,a1,(CastConv b1|CastVM b1)), CCast(_,a2,(CastConv b2|CastVM b2)) -> + constr_expr_eq a1 a2 && + constr_expr_eq b1 b2 + | CCast(_,a1,CastCoerce), CCast(_,a2, CastCoerce) -> + constr_expr_eq a1 a2 + | CNotation(_, n1, s1), CNotation(_, n2, s2) -> + String.equal n1 n2 && + constr_notation_substitution_eq s1 s2 + | CPrim(_,i1), CPrim(_,i2) -> + prim_token_eq i1 i2 + | CGeneralization (_, bk1, ak1, e1), CGeneralization (_, bk2, ak2, e2) -> + binding_kind_eq bk1 bk2 && + Option.equal abstraction_kind_eq ak1 ak2 && + constr_expr_eq e1 e2 + | CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) -> + String.equal s1 s2 && + constr_expr_eq e1 e2 + | _ -> false + +and args_eq (a1,e1) (a2,e2) = + Option.equal (eq_located explicitation_eq) e1 e2 && + constr_expr_eq a1 a2 + +and case_expr_eq (e1, (n1, p1)) (e2, (n2, p2)) = + constr_expr_eq e1 e2 && + Option.equal (eq_located name_eq) n1 n2 && + Option.equal cases_pattern_expr_eq p1 p2 + +and branch_expr_eq (_, p1, e1) (_, p2, e2) = + List.equal (eq_located (List.equal cases_pattern_expr_eq)) p1 p2 && + constr_expr_eq e1 e2 + +and binder_expr_eq ((n1, _, e1) : binder_expr) (n2, _, e2) = + (** Don't care about the [binder_kind] *) + List.equal (eq_located name_eq) n1 n2 && constr_expr_eq e1 e2 + +and fix_expr_eq (id1,(j1, r1),bl1,a1,b1) (id2,(j2, r2),bl2,a2,b2) = + (eq_located id_eq id1 id2) && + Option.equal (eq_located id_eq) j1 j2 && + recursion_order_expr_eq r1 r2 && + List.equal local_binder_eq bl1 bl2 && + constr_expr_eq a1 a2 && + constr_expr_eq b1 b2 + +and cofix_expr_eq (id1,bl1,a1,b1) (id2,bl2,a2,b2) = + (eq_located id_eq id1 id2) && + List.equal local_binder_eq bl1 bl2 && + constr_expr_eq a1 a2 && + constr_expr_eq b1 b2 + +and recursion_order_expr_eq r1 r2 = match r1, r2 with +| CStructRec, CStructRec -> true +| CWfRec e1, CWfRec e2 -> constr_expr_eq e1 e2 +| CMeasureRec (e1, o1), CMeasureRec (e2, o2) -> + constr_expr_eq e1 e2 && Option.equal constr_expr_eq o1 o2 +| _ -> false + +and local_binder_eq l1 l2 = match l1, l2 with +| LocalRawDef (n1, e1), LocalRawDef (n2, e2) -> + eq_located name_eq n1 n2 && constr_expr_eq e1 e2 +| LocalRawAssum (n1, _, e1), LocalRawAssum (n2, _, e2) -> + (** Don't care about the [binder_kind] *) + List.equal (eq_located name_eq) n1 n2 && constr_expr_eq e1 e2 +| _ -> false + +and constr_notation_substitution_eq (e1, el1, bl1) (e2, el2, bl2) = + List.equal constr_expr_eq e1 e2 && + List.equal (List.equal constr_expr_eq) el1 el2 && + List.equal (List.equal local_binder_eq) bl1 bl2 + let constr_loc = function | CRef (Ident (loc,_)) -> loc | CRef (Qualid (loc,_)) -> loc diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index bd118bbce..8eb88f70d 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -17,18 +17,32 @@ open Constrexpr (** Constrexpr_ops: utilities on [constr_expr] *) -val constr_loc : constr_expr -> Loc.t +(** {6 Equalities on [constr_expr] related types} *) -val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t -val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t +val explicitation_eq : explicitation -> explicitation -> bool +(** Equality on [explicitation]. *) -val local_binders_loc : local_binder list -> Loc.t +val constr_expr_eq : constr_expr -> constr_expr -> bool +(** Equality on [constr_expr]. This is a syntactical one, which is oblivious to + some parsing details, including locations. *) + +val local_binder_eq : local_binder -> local_binder -> bool +(** Equality on [local_binder]. Same properties as [constr_expr_eq]. *) val binding_kind_eq : Decl_kinds.binding_kind -> Decl_kinds.binding_kind -> bool +(** Equality on [binding_kind] *) val binder_kind_eq : binder_kind -> binder_kind -> bool +(** Equality on [binder_kind] *) -val default_binder_kind : binder_kind +(** {6 Retrieving locations} *) + +val constr_loc : constr_expr -> Loc.t +val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t +val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t +val local_binders_loc : local_binder list -> Loc.t + +(** {6 Constructors}*) val mkIdentC : identifier -> constr_expr val mkRefC : reference -> constr_expr @@ -38,24 +52,36 @@ val mkLambdaC : name located list * binder_kind * constr_expr * constr_expr -> c val mkLetInC : name located * constr_expr * constr_expr -> constr_expr val mkProdC : name located list * binder_kind * constr_expr * constr_expr -> constr_expr -val coerce_reference_to_id : reference -> identifier -val coerce_to_id : constr_expr -> identifier located -val coerce_to_name : constr_expr -> name located - val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr val prod_constr_expr : constr_expr -> local_binder list -> constr_expr -(** Same as [abstract_constr_expr] and [prod_constr_expr], with location *) val mkCLambdaN : Loc.t -> local_binder list -> constr_expr -> constr_expr +(** Same as [abstract_constr_expr], with location *) + val mkCProdN : Loc.t -> local_binder list -> constr_expr -> constr_expr +(** Same as [prod_constr_expr], with location *) -(** For binders parsing *) +(** {6 Destructors}*) -(** With let binders *) -val names_of_local_assums : local_binder list -> name located list +val coerce_reference_to_id : reference -> identifier +(** FIXME: nothing to do here *) + +val coerce_to_id : constr_expr -> identifier located +(** Destruct terms of the form [CRef (Ident _)]. *) + +val coerce_to_name : constr_expr -> name located +(** Destruct terms of the form [CRef (Ident _)] or [CHole _]. *) + +(** {6 Binder manipulation} *) + +val default_binder_kind : binder_kind -(** Does not take let binders into account *) val names_of_local_binders : local_binder list -> name located list +(** Retrieve a list of binding names from a list of binders. *) + +val names_of_local_assums : local_binder list -> name located list +(** Same as [names_of_local_binders], but does not take the [let] bindings into + account. *) val raw_cases_pattern_expr_of_glob_constr : (Globnames.global_reference -> unit) -> Glob_term.glob_constr -> raw_cases_pattern_expr diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 72577d866..d0be33031 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -155,116 +155,6 @@ let extern_reference loc vars r = else Qualid (loc,shortest_qualid_of_global vars r) - -(************************************************************************) -(* Equality up to location (useful for translator v8) *) - -let prim_token_eq t1 t2 = match t1, t2 with -| Numeral i1, Numeral i2 -> Bigint.equal i1 i2 -| String s1, String s2 -> String.equal s1 s2 -| _ -> false - -(** ppedrot: FIXME, EVERYTHING IS WRONG HERE! *) - -let rec check_same_pattern p1 p2 = - match p1, p2 with - | CPatAlias(_,a1,i1), CPatAlias(_,a2,i2) when id_eq i1 i2 -> - check_same_pattern a1 a2 - | CPatCstr(_,c1,a1,b1), CPatCstr(_,c2,a2,b2) when eq_reference c1 c2 -> - let () = List.iter2 check_same_pattern a1 a2 in - List.iter2 check_same_pattern b1 b2 - | CPatAtom(_,r1), CPatAtom(_,r2) when Option.equal eq_reference r1 r2 -> () - | CPatPrim(_,i1), CPatPrim(_,i2) when prim_token_eq i1 i2 -> () - | CPatDelimiters(_,s1,e1), CPatDelimiters(_,s2,e2) when String.equal s1 s2 -> - check_same_pattern e1 e2 - | _ -> failwith "not same pattern" - -let check_same_ref r1 r2 = - if not (eq_reference r1 r2) then failwith "not same ref" - -let eq_located f (_, x) (_, y) = f x y - -let same_id (id1, c1) (id2, c2) = - Option.equal (eq_located id_eq) id1 id2 && Pervasives.(=) c1 c2 - -let rec check_same_type ty1 ty2 = - match ty1, ty2 with - | CRef r1, CRef r2 -> check_same_ref r1 r2 - | CFix(_,id1,fl1), CFix(_,id2,fl2) when eq_located id_eq id1 id2 -> - List.iter2 (fun ((_, id1),i1,bl1,a1,b1) ((_, id2),i2,bl2,a2,b2) -> - if not (id_eq id1 id2) || not (same_id i1 i2) then failwith "not same fix"; - check_same_fix_binder bl1 bl2; - check_same_type a1 a2; - check_same_type b1 b2) - fl1 fl2 - | CCoFix(_,id1,fl1), CCoFix(_,id2,fl2) when eq_located id_eq id1 id2 -> - List.iter2 (fun (id1,bl1,a1,b1) (id2,bl2,a2,b2) -> - if not (eq_located id_eq id1 id2) then failwith "not same fix"; - check_same_fix_binder bl1 bl2; - check_same_type a1 a2; - check_same_type b1 b2) - fl1 fl2 - | CProdN(_,bl1,a1), CProdN(_,bl2,a2) -> - List.iter2 check_same_binder bl1 bl2; - check_same_type a1 a2 - | CLambdaN(_,bl1,a1), CLambdaN(_,bl2,a2) -> - List.iter2 check_same_binder bl1 bl2; - check_same_type a1 a2 - | CLetIn(_,(_,na1),a1,b1), CLetIn(_,(_,na2),a2,b2) when name_eq na1 na2 -> - check_same_type a1 a2; - check_same_type b1 b2 - | CAppExpl(_,(proj1,r1),al1), CAppExpl(_,(proj2,r2),al2) when Option.equal Int.equal proj1 proj2 -> - check_same_ref r1 r2; - List.iter2 check_same_type al1 al2 - | CApp(_,(_,e1),al1), CApp(_,(_,e2),al2) -> - check_same_type e1 e2; - let check_args (a1,e1) (a2,e2) = - let eq_expl = eq_located Constrintern.explicitation_eq in - if not (Option.equal eq_expl e1 e2) then failwith "not same expl"; - check_same_type a1 a2 - in - List.iter2 check_args al1 al2 - | CCases(_,_,_,a1,brl1), CCases(_,_,_,a2,brl2) -> - List.iter2 (fun (tm1,_) (tm2,_) -> check_same_type tm1 tm2) a1 a2; - List.iter2 (fun (_,pl1,r1) (_,pl2,r2) -> - List.iter2 (Loc.located_iter2 (List.iter2 check_same_pattern)) pl1 pl2; - check_same_type r1 r2) brl1 brl2 - | CHole _, CHole _ -> () - | CPatVar(_,(b1, i1)), CPatVar(_,(b2, i2)) when (b1 : bool) == b2 && id_eq i1 i2 -> () - | CSort(_,s1), CSort(_,s2) when glob_sort_eq s1 s2 -> () - | CCast(_,a1,(CastConv b1|CastVM b1)), CCast(_,a2,(CastConv b2|CastVM b2)) -> - check_same_type a1 a2; - check_same_type b1 b2 - | CCast(_,a1,CastCoerce), CCast(_,a2, CastCoerce) -> - check_same_type a1 a2 - | CNotation(_,n1,(e1,el1,bl1)), CNotation(_,n2,(e2,el2,bl2)) when String.equal n1 n2 -> - List.iter2 check_same_type e1 e2; - List.iter2 (List.iter2 check_same_type) el1 el2; - List.iter2 check_same_fix_binder bl1 bl2 - | CPrim(_,i1), CPrim(_,i2) when prim_token_eq i1 i2 -> () - | CDelimiters(_,s1,e1), CDelimiters(_,s2,e2) when String.equal s1 s2 -> - check_same_type e1 e2 - | _ when Pervasives.(=) ty1 ty2 -> () (** FIXME *) - | _ -> failwith "not same type" - -and check_same_binder (nal1,_,e1) (nal2,_,e2) = - List.iter2 (fun (_,na1) (_,na2) -> - if not (name_eq na1 na2) then failwith "not same name") nal1 nal2; - check_same_type e1 e2 - -and check_same_fix_binder bl1 bl2 = - List.iter2 (fun b1 b2 -> - match b1,b2 with - LocalRawAssum(nal1,k,ty1), LocalRawAssum(nal2,k',ty2) -> - check_same_binder (nal1,k,ty1) (nal2,k',ty2) - | LocalRawDef(na1,def1), LocalRawDef(na2,def2) -> - check_same_binder ([na1],default_binder_kind,def1) ([na2],default_binder_kind,def2) - | _ -> failwith "not same binder") bl1 bl2 - -let is_same_type c d = - try let () = check_same_type c d in true - with Failure _ | Invalid_argument _ -> false - (**********************************************************************) (* mapping patterns to cases_pattern_expr *) @@ -865,7 +755,7 @@ and factorize_prod scopes vars na bk aty c = let c = extern_typ scopes vars c in match na, c with | Name id, CProdN (loc,[nal,Default bk',ty],c) - when binding_kind_eq bk bk' && is_same_type aty ty + when binding_kind_eq bk bk' && constr_expr_eq aty ty & not (occur_var_constr_expr id ty) (* avoid na in ty escapes scope *) -> nal,c | _ -> @@ -875,7 +765,7 @@ and factorize_lambda inctx scopes vars na bk aty c = let c = sub_extern inctx scopes vars c in match c with | CLambdaN (loc,[nal,Default bk',ty],c) - when binding_kind_eq bk bk' && is_same_type aty ty + when binding_kind_eq bk bk' && constr_expr_eq aty ty & not (occur_name na ty) (* avoid na in ty escapes scope *) -> nal,c | _ -> @@ -893,7 +783,7 @@ and extern_local_binder scopes vars = function let ty = extern_typ scopes vars (anonymize_if_reserved na ty) in (match extern_local_binder scopes (name_fold Idset.add na vars) l with (assums,ids,LocalRawAssum(nal,k,ty')::l) - when is_same_type ty ty' & + when constr_expr_eq ty ty' & match na with Name id -> not (occur_var_constr_expr id ty') | _ -> true -> (na::assums,na::ids, diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 91ad86381..0ca25656f 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -22,8 +22,6 @@ open Notation_term open Notation open Misctypes -val is_same_type : constr_expr -> constr_expr -> bool - (** Translation of pattern, cases pattern, glob_constr and term into syntax trees for printing *) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index f1316bbfa..e4df61c47 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1188,13 +1188,6 @@ let intern_ind_pattern genv env pat = (**********************************************************************) (* Utilities for application *) -let explicitation_eq ex1 ex2 = match ex1, ex2 with -| ExplByPos (i1, id1), ExplByPos (i2, id2) -> - Int.equal i1 i2 && Option.equal id_eq id1 id2 -| ExplByName id1, ExplByName id2 -> - id_eq id1 id2 -| _ -> false - let merge_impargs l args = let test x = function | (_, Some (_, y)) -> explicitation_eq x y diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 6e2c9e883..28e7e2985 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -188,8 +188,3 @@ val parsing_explicit : bool ref (** Globalization leak for Grammar *) val for_grammar : ('a -> 'b) -> 'a -> 'b - -(** Nothing to do here *) - -val explicitation_eq : explicitation -> explicitation -> bool - diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index 322528479..01380b8d5 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -65,16 +65,15 @@ type constr_expr = | CRef of reference | CFix of Loc.t * identifier located * fix_expr list | CCoFix of Loc.t * identifier located * cofix_expr list - | CProdN of Loc.t * (name located list * binder_kind * constr_expr) list * constr_expr - | CLambdaN of Loc.t * (name located list * binder_kind * constr_expr) list * constr_expr + | CProdN of Loc.t * binder_expr list * constr_expr + | CLambdaN of Loc.t * binder_expr list * constr_expr | CLetIn of Loc.t * name located * constr_expr * constr_expr | CAppExpl of Loc.t * (proj_flag * reference) * constr_expr list | CApp of Loc.t * (proj_flag * constr_expr) * (constr_expr * explicitation located option) list | CRecord of Loc.t * constr_expr option * (reference * constr_expr) list | CCases of Loc.t * case_style * constr_expr option * - (constr_expr * (name located option * cases_pattern_expr option)) list * - (Loc.t * cases_pattern_expr list located list * constr_expr) list + case_expr list * branch_expr list | CLetTuple of Loc.t * name located list * (name located option * constr_expr option) * constr_expr * constr_expr | CIf of Loc.t * constr_expr * (name located option * constr_expr option) @@ -89,6 +88,15 @@ type constr_expr = | CPrim of Loc.t * prim_token | CDelimiters of Loc.t * string * constr_expr +and case_expr = + constr_expr * (name located option * cases_pattern_expr option) + +and branch_expr = + Loc.t * cases_pattern_expr list located list * constr_expr + +and binder_expr = + name located list * binder_kind * constr_expr + and fix_expr = identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr diff --git a/toplevel/command.ml b/toplevel/command.ml index 5967b435a..69918b2b0 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -328,18 +328,8 @@ let interp_mutual_inductive (paramsl,indl) notations finite = impls (* Very syntactical equality *) -let eq_local_binder d1 d2 = match d1,d2 with - | LocalRawAssum (nal1,k1,c1), LocalRawAssum (nal2,k2,c2) -> - Int.equal (List.length nal1) (List.length nal2) && binder_kind_eq k1 k2 && - List.for_all2 (fun (_,na1) (_,na2) -> name_eq na1 na2) nal1 nal2 && - Constrextern.is_same_type c1 c2 - | LocalRawDef ((_,id1),c1), LocalRawDef ((_,id2),c2) -> - name_eq id1 id2 && Constrextern.is_same_type c1 c2 - | _ -> - false - let eq_local_binders bl1 bl2 = - Int.equal (List.length bl1) (List.length bl2) && List.for_all2 eq_local_binder bl1 bl2 + List.equal local_binder_eq bl1 bl2 let extract_coercions indl = let mkqid (_,((_,id),_)) = qualid_of_ident id in |