diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/glob_ops.ml | 16 | ||||
| -rw-r--r-- | pretyping/glob_term.ml | 19 | ||||
| -rw-r--r-- | pretyping/patternops.ml | 24 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 4 |
5 files changed, 26 insertions, 39 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index eaa5736336..062e3ca8b2 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -653,7 +653,7 @@ let detype_fix detype flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) = let v = Array.map3 (fun c t i -> share_names detype flags (i+1) [] def_avoid def_env sigma c (lift n t)) bodies tys vn in - GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi), + GRec(GFix (Array.map (fun i -> Some i) (fst nvn), snd nvn),Array.of_list (List.rev lfi), Array.map (fun (bl,_,_) -> bl) v, Array.map (fun (_,_,ty) -> ty) v, Array.map (fun (_,bd,_) -> bd) v) diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 6da168711c..85b9faac77 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -106,19 +106,9 @@ let glob_decl_eq f (na1, bk1, c1, t1) (na2, bk2, c2, t2) = Name.equal na1 na2 && binding_kind_eq bk1 bk2 && Option.equal f c1 c2 && f t1 t2 -let fix_recursion_order_eq f o1 o2 = match o1, o2 with - | GStructRec, GStructRec -> true - | GWfRec c1, GWfRec c2 -> f c1 c2 - | GMeasureRec (c1, o1), GMeasureRec (c2, o2) -> - f c1 c2 && Option.equal f o1 o2 - | (GStructRec | GWfRec _ | GMeasureRec _), _ -> false - -let fix_kind_eq f k1 k2 = match k1, k2 with +let fix_kind_eq k1 k2 = match k1, k2 with | GFix (a1, i1), GFix (a2, i2) -> - let eq (i1, o1) (i2, o2) = - Option.equal Int.equal i1 i2 && fix_recursion_order_eq f o1 o2 - in - Int.equal i1 i2 && Array.equal eq a1 a2 + Int.equal i1 i2 && Array.equal (Option.equal Int.equal) a1 a2 | GCoFix i1, GCoFix i2 -> Int.equal i1 i2 | (GFix _ | GCoFix _), _ -> false @@ -150,7 +140,7 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with f m1 m2 && Name.equal pat1 pat2 && Option.equal f p1 p2 && f c1 c2 && f t1 t2 | GRec (kn1, id1, decl1, t1, c1), GRec (kn2, id2, decl2, t2, c2) -> - fix_kind_eq f kn1 kn2 && Array.equal Id.equal id1 id2 && + fix_kind_eq kn1 kn2 && Array.equal Id.equal id1 id2 && Array.equal (fun l1 l2 -> List.equal (glob_decl_eq f) l1 l2) decl1 decl2 && Array.equal f c1 c2 && Array.equal f t1 t2 | GSort s1, GSort s2 -> glob_sort_eq s1 s2 diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index c57cf88cc6..02cb294f6d 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -41,6 +41,12 @@ type glob_constraint = glob_level * Univ.constraint_type * glob_level type sort_info = (Libnames.qualid * int) option list type glob_sort = sort_info glob_sort_gen +type glob_recarg = int option + +and glob_fix_kind = + | GFix of (glob_recarg array * int) + | GCoFix of int + (** Casts *) type 'a cast_type = @@ -78,7 +84,7 @@ type 'a glob_constr_r = (** [GCases(style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *) | GLetTuple of Name.t list * (Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g | GIf of 'a glob_constr_g * (Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g - | GRec of 'a fix_kind_g * Id.t array * 'a glob_decl_g list array * + | GRec of glob_fix_kind * Id.t array * 'a glob_decl_g list array * 'a glob_constr_g array * 'a glob_constr_g array | GSort of glob_sort | GHole of Evar_kinds.t * Namegen.intro_pattern_naming_expr * Genarg.glob_generic_argument option @@ -88,15 +94,6 @@ and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t and 'a glob_decl_g = Name.t * binding_kind * 'a glob_constr_g option * 'a glob_constr_g -and 'a fix_recursion_order_g = - | GStructRec - | GWfRec of 'a glob_constr_g - | GMeasureRec of 'a glob_constr_g * 'a glob_constr_g option - -and 'a fix_kind_g = - | GFix of ((int option * 'a fix_recursion_order_g) array * int) - | GCoFix of int - and 'a predicate_pattern_g = Name.t * (inductive * Name.t list) CAst.t option (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)]. *) @@ -117,9 +114,7 @@ type tomatch_tuples = [ `any ] tomatch_tuples_g type cases_clause = [ `any ] cases_clause_g type cases_clauses = [ `any ] cases_clauses_g type glob_decl = [ `any ] glob_decl_g -type fix_kind = [ `any ] fix_kind_g type predicate_pattern = [ `any ] predicate_pattern_g -type fix_recursion_order = [ `any ] fix_recursion_order_g type any_glob_constr = AnyGlobConstr : 'r glob_constr_g -> any_glob_constr diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index b29afd1fd2..c788efda48 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -470,17 +470,19 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function PCase (info, pred, pat_of_raw metas vars c, brs) | GRec (GFix (ln,n), ids, decls, tl, cl) -> - if Array.exists (function (Some n, GStructRec) -> false | _ -> true) ln then - err ?loc (Pp.str "\"struct\" annotation is expected.") - else - let ln = Array.map (fst %> Option.get) ln in - let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in - let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in - let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in - let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in - let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in - let names = Array.map (fun id -> Name id) ids in - PFix ((ln,n), (names, tl, cl)) + let get_struct_arg = function + | Some n -> n + | None -> err ?loc (Pp.str "\"struct\" annotation is expected.") + (* TODO why can't the annotation be omitted? *) + in + let ln = Array.map get_struct_arg ln in + let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in + let tl = Array.map (fun (ctx,tl) -> it_mkPProd_or_LetIn tl ctx) ctxtl in + let vars = Array.fold_left (fun vars na -> Name na::vars) vars ids in + let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls cl in + let cl = Array.map (fun (ctx,cl) -> it_mkPLambda_or_LetIn cl ctx) ctxtl in + let names = Array.map (fun id -> Name id) ids in + PFix ((ln,n), (names, tl, cl)) | GRec (GCoFix n, ids, decls, tl, cl) -> let ctxtl = Array.map2 (pat_of_glob_in_context metas vars) decls tl in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 0f7676cd19..48d981082c 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -607,10 +607,10 @@ let rec pretype ~program_mode ~poly k0 resolve_tc (tycon : type_constraint) (env fixpoints ?) *) let possible_indexes = Array.to_list (Array.mapi - (fun i (n,_) -> match n with + (fun i annot -> match annot with | Some n -> [n] | None -> List.map_i (fun i _ -> i) 0 ctxtv.(i)) - vn) + vn) in let fixdecls = (names,ftys,fdefs) in let indexes = esearch_guard ?loc !!env sigma possible_indexes fixdecls in |