aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrexpr.ml8
-rw-r--r--interp/constrexpr_ops.ml15
-rw-r--r--interp/constrextern.ml22
-rw-r--r--interp/constrintern.ml67
-rw-r--r--interp/notation_ops.ml2
-rw-r--r--interp/notation_term.ml2
6 files changed, 51 insertions, 65 deletions
diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index 7a14a4e708..653bb68f30 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -134,16 +134,16 @@ and branch_expr =
(cases_pattern_expr list list * constr_expr) CAst.t
and fix_expr =
- lident * (lident option * recursion_order_expr) *
+ lident * (recursion_order_expr CAst.t) option *
local_binder_expr list * constr_expr * constr_expr
and cofix_expr =
lident * local_binder_expr list * constr_expr * constr_expr
and recursion_order_expr =
- | CStructRec
- | CWfRec of constr_expr
- | CMeasureRec of constr_expr * constr_expr option (** measure, relation *)
+ | CStructRec of lident
+ | CWfRec of lident * constr_expr
+ | CMeasureRec of lident option * constr_expr * constr_expr option (** argument, measure, relation *)
(* Anonymous defs allowed ?? *)
and local_binder_expr =
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 60610b92b8..db860e0c3b 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -196,10 +196,9 @@ and branch_expr_eq {CAst.v=(p1, e1)} {CAst.v=(p2, e2)} =
List.equal (List.equal cases_pattern_expr_eq) p1 p2 &&
constr_expr_eq e1 e2
-and fix_expr_eq (id1,(j1, r1),bl1,a1,b1) (id2,(j2, r2),bl2,a2,b2) =
+and fix_expr_eq (id1,r1,bl1,a1,b1) (id2,r2,bl2,a2,b2) =
(eq_ast Id.equal id1 id2) &&
- Option.equal (eq_ast Id.equal) j1 j2 &&
- recursion_order_expr_eq r1 r2 &&
+ Option.equal (eq_ast recursion_order_expr_eq) r1 r2 &&
List.equal local_binder_eq bl1 bl2 &&
constr_expr_eq a1 a2 &&
constr_expr_eq b1 b2
@@ -211,9 +210,11 @@ and cofix_expr_eq (id1,bl1,a1,b1) (id2,bl2,a2,b2) =
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) ->
+ | CStructRec i1, CStructRec i2 -> eq_ast Id.equal i1 i2
+ | CWfRec (i1,e1), CWfRec (i2,e2) ->
+ constr_expr_eq e1 e2
+ | CMeasureRec (i1, e1, o1), CMeasureRec (i2, e2, o2) ->
+ Option.equal (eq_ast Id.equal) i1 i2 &&
constr_expr_eq e1 e2 && Option.equal constr_expr_eq o1 o2
| _ -> false
@@ -349,7 +350,7 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
(f (Option.fold_right (CAst.with_val (Name.fold_right g)) ona n)) acc po
| CFix (_,l) ->
let n' = List.fold_right (fun ( { CAst.v = id },_,_,_,_) -> g id) l n in
- List.fold_right (fun (_,(_,o),lb,t,c) acc ->
+ List.fold_right (fun (_,ro,lb,t,c) acc ->
fold_local_binders g f n'
(fold_local_binders g f n acc t lb) c lb) l acc
| CCoFix (_,_) ->
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index b89b6b5765..3b169edaab 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -938,13 +938,12 @@ let rec extern inctx (custom,scopes as allscopes) vars r =
let (assums,ids,bl) = extern_local_binder scopes vars bl in
let vars0 = List.fold_right (Name.fold_right Id.Set.add) ids vars in
let vars1 = List.fold_right (Name.fold_right Id.Set.add) ids vars' in
- let n =
- match fst nv.(i) with
- | None -> None
- | Some x -> Some (CAst.make @@ Name.get_id (List.nth assums x))
- in
- let ro = extern_recursion_order scopes vars (snd nv.(i)) in
- ((CAst.make fi), (n, ro), bl, extern_typ scopes vars0 ty,
+ let n =
+ match nv.(i) with
+ | None -> None
+ | Some x -> Some (CAst.make @@ CStructRec (CAst.make @@ Name.get_id (List.nth assums x)))
+ in
+ ((CAst.make fi), n, bl, extern_typ scopes vars0 ty,
extern false scopes vars1 def)) idv
in
CFix (CAst.(make ?loc idv.(n)), Array.to_list listdecl)
@@ -1159,13 +1158,6 @@ and extern_notation (custom,scopes as allscopes) lonely_seen vars t = function
let lonely_seen = add_lonely keyrule lonely_seen in
extern_notation allscopes lonely_seen vars t rules
-and extern_recursion_order scopes vars = function
- GStructRec -> CStructRec
- | GWfRec c -> CWfRec (extern true scopes vars c)
- | GMeasureRec (m,r) -> CMeasureRec (extern true scopes vars m,
- Option.map (extern true scopes vars) r)
-
-
let extern_glob_constr vars c =
extern false (InConstrEntrySomeLevel,(None,[])) vars c
@@ -1294,7 +1286,7 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
let v = Array.map3
(fun c t i -> Detyping.share_pattern_names glob_of_pat (i+1) [] def_avoid def_env sigma c (Patternops.lift_pattern n t))
bl tl ln in
- GRec(GFix (Array.map (fun i -> Some i, GStructRec) ln,i),Array.of_list (List.rev lfi),
+ GRec(GFix (Array.map (fun i -> Some i) ln,i),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/interp/constrintern.ml b/interp/constrintern.ml
index 3329ba2047..c0801067ce 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1845,51 +1845,44 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
in
apply_impargs c env imp subscopes l loc
- | CFix ({ CAst.loc = locid; v = iddef}, dl) ->
+ | CFix ({ CAst.loc = locid; v = iddef}, dl) ->
let lf = List.map (fun ({CAst.v = id},_,_,_,_) -> id) dl in
let dl = Array.of_list dl in
- let n =
- try List.index0 Id.equal iddef lf
+ let n =
+ try List.index0 Id.equal iddef lf
with Not_found ->
- raise (InternalizationError (locid,UnboundFixName (false,iddef)))
- in
- let idl_temp = Array.map
- (fun (id,(n,order),bl,ty,_) ->
- let intern_ro_arg f =
- let before, after = split_at_annot bl n in
- let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in
- let ro = f (intern env') in
- let n' = Option.map (fun _ -> List.count (fun c -> match DAst.get c with
- | GLocalAssum _ -> true
- | _ -> false (* remove let-ins *))
- rbefore) n in
- n', ro, List.fold_left intern_local_binder (env',rbefore) after
- in
- let n, ro, (env',rbl) =
- match order with
- | CStructRec ->
- intern_ro_arg (fun _ -> GStructRec)
- | CWfRec c ->
- intern_ro_arg (fun f -> GWfRec (f c))
- | CMeasureRec (m,r) ->
- intern_ro_arg (fun f -> GMeasureRec (f m, Option.map f r))
- in
- let bl = List.rev (List.map glob_local_binder_of_extended rbl) in
- ((n, ro), bl, intern_type env' ty, env')) dl in
+ raise (InternalizationError (locid,UnboundFixName (false,iddef)))
+ in
+ let idl_temp = Array.map
+ (fun (id,recarg,bl,ty,_) ->
+ let recarg = Option.map (function { CAst.v = v } -> match v with
+ | CStructRec i -> i
+ | _ -> anomaly Pp.(str "Non-structural recursive argument in non-program fixpoint")) recarg
+ in
+ let before, after = split_at_annot bl recarg in
+ let (env',rbefore) = List.fold_left intern_local_binder (env,[]) before in
+ let n = Option.map (fun _ -> List.count (fun c -> match DAst.get c with
+ | GLocalAssum _ -> true
+ | _ -> false (* remove let-ins *))
+ rbefore) recarg in
+ let (env',rbl) = List.fold_left intern_local_binder (env',rbefore) after in
+ let bl = List.rev (List.map glob_local_binder_of_extended rbl) in
+ (n, bl, intern_type env' ty, env')) dl in
let idl = Array.map2 (fun (_,_,_,_,bd) (a,b,c,env') ->
- let env'' = List.fold_left_i (fun i en name ->
- let (_,bli,tyi,_) = idl_temp.(i) in
- let fix_args = (List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli) in
- push_name_env ntnvars (impls_type_list ~args:fix_args tyi)
- en (CAst.make @@ Name name)) 0 env' lf in
- (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in
- DAst.make ?loc @@
- GRec (GFix
- (Array.map (fun (ro,_,_,_) -> ro) idl,n),
+ let env'' = List.fold_left_i (fun i en name ->
+ let (_,bli,tyi,_) = idl_temp.(i) in
+ let fix_args = (List.map (fun (na, bk, _, _) -> (build_impls bk na)) bli) in
+ push_name_env ntnvars (impls_type_list ~args:fix_args tyi)
+ en (CAst.make @@ Name name)) 0 env' lf in
+ (a,b,c,intern {env'' with tmp_scope = None} bd)) dl idl_temp in
+ DAst.make ?loc @@
+ GRec (GFix
+ (Array.map (fun (ro,_,_,_) -> ro) idl,n),
Array.of_list lf,
Array.map (fun (_,bl,_,_) -> bl) idl,
Array.map (fun (_,_,ty,_) -> ty) idl,
Array.map (fun (_,_,_,bd) -> bd) idl)
+
| CCoFix ({ CAst.loc = locid; v = iddef }, dl) ->
let lf = List.map (fun ({CAst.v = id},_,_,_) -> id) dl in
let dl = Array.of_list dl in
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 9801e56ca1..7f084fffdd 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -957,7 +957,7 @@ let match_fix_kind fk1 fk2 =
match (fk1,fk2) with
| GCoFix n1, GCoFix n2 -> Int.equal n1 n2
| GFix (nl1,n1), GFix (nl2,n2) ->
- let test (n1, _) (n2, _) = match n1, n2 with
+ let test n1 n2 = match n1, n2 with
| _, None -> true
| Some id1, Some id2 -> Int.equal id1 id2
| _ -> false
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 6fe20486dc..5024f5c26f 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -38,7 +38,7 @@ type notation_constr =
notation_constr * notation_constr
| NIf of notation_constr * (Name.t * notation_constr option) *
notation_constr * notation_constr
- | NRec of fix_kind * Id.t array *
+ | NRec of glob_fix_kind * Id.t array *
(Name.t * notation_constr option * notation_constr) list array *
notation_constr array * notation_constr array
| NSort of glob_sort
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:04:35 +0000