aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrextern.ml31
-rw-r--r--interp/constrintern.ml12
-rw-r--r--interp/genarg.ml2
-rw-r--r--interp/notation.ml12
-rw-r--r--interp/reserve.ml8
-rw-r--r--interp/topconstr.ml46
6 files changed, 53 insertions, 58 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index ec88e6fe8..ec74c91b2 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -233,11 +233,6 @@ and check_same_fix_binder bl1 bl2 =
let same c d = try check_same_type c d; true with _ -> false
(* Idem for rawconstr *)
-let option_iter2 f o1 o2 =
- match o1, o2 with
- Some o1, Some o2 -> f o1 o2
- | None, None -> ()
- | _ -> failwith "option"
let array_iter2 f v1 v2 =
List.iter2 f (Array.to_list v1) (Array.to_list v2)
@@ -256,7 +251,7 @@ let rec same_raw c d =
| RVar(_,id1), RVar(_,id2) -> if id1<>id2 then failwith "RVar"
| REvar(_,e1,a1), REvar(_,e2,a2) ->
if e1 <> e2 then failwith "REvar";
- option_iter2(List.iter2 same_raw) a1 a2
+ Option.iter2(List.iter2 same_raw) a1 a2
| RPatVar(_,pv1), RPatVar(_,pv2) -> if pv1<>pv2 then failwith "RPatVar"
| RApp(_,f1,a1), RApp(_,f2,a2) ->
List.iter2 same_raw (f1::a1) (f2::a2)
@@ -274,7 +269,7 @@ let rec same_raw c d =
(fun (t1,(al1,oind1)) (t2,(al2,oind2)) ->
same_raw t1 t2;
if al1 <> al2 then failwith "RCases";
- option_iter2(fun (_,i1,_,nl1) (_,i2,_,nl2) ->
+ Option.iter2(fun (_,i1,_,nl1) (_,i2,_,nl2) ->
if i1<>i2 || nl1 <> nl2 then failwith "RCases") oind1 oind2) c1 c2;
List.iter2 (fun (_,_,pl1,b1) (_,_,pl2,b2) ->
List.iter2 same_patt pl1 pl2;
@@ -290,7 +285,7 @@ let rec same_raw c d =
array_iter2
(List.iter2 (fun (na1,bd1,ty1) (na2,bd2,ty2) ->
if na1<>na2 then failwith "RRec";
- option_iter2 same_raw bd1 bd2;
+ Option.iter2 same_raw bd1 bd2;
same_raw ty1 ty2)) bl1 bl2;
array_iter2 same_raw ty1 ty2;
array_iter2 same_raw def1 def2
@@ -659,7 +654,7 @@ let rec extern inctx scopes vars r =
| REvar (loc,n,None) when !print_meta_as_hole -> CHole loc
| REvar (loc,n,l) ->
- extern_evar loc n (option_map (List.map (extern false scopes vars)) l)
+ extern_evar loc n (Option.map (List.map (extern false scopes vars)) l)
| RPatVar (loc,n) ->
if !print_meta_as_hole then CHole loc else CPatVar (loc,n)
@@ -699,17 +694,17 @@ let rec extern inctx scopes vars r =
let vars' =
List.fold_right (name_fold Idset.add)
(cases_predicate_names tml) vars in
- let rtntypopt' = option_map (extern_typ scopes vars') rtntypopt in
+ let rtntypopt' = Option.map (extern_typ scopes vars') rtntypopt in
let tml = List.map (fun (tm,(na,x)) ->
let na' = match na,tm with
Anonymous, RVar (_,id) when
- rtntypopt<>None & occur_rawconstr id (out_some rtntypopt)
+ rtntypopt<>None & occur_rawconstr id (Option.get rtntypopt)
-> Some Anonymous
| Anonymous, _ -> None
| Name id, RVar (_,id') when id=id' -> None
| Name _, _ -> Some na in
(sub_extern false scopes vars tm,
- (na',option_map (fun (loc,ind,n,nal) ->
+ (na',Option.map (fun (loc,ind,n,nal) ->
let params = list_tabulate
(fun _ -> RHole (dummy_loc,Evd.InternalHole)) n in
let args = List.map (function
@@ -722,15 +717,15 @@ let rec extern inctx scopes vars r =
| RLetTuple (loc,nal,(na,typopt),tm,b) ->
CLetTuple (loc,nal,
- (option_map (fun _ -> na) typopt,
- option_map (extern_typ scopes (add_vname vars na)) typopt),
+ (Option.map (fun _ -> na) typopt,
+ Option.map (extern_typ scopes (add_vname vars na)) typopt),
sub_extern false scopes vars tm,
extern false scopes (List.fold_left add_vname vars nal) b)
| RIf (loc,c,(na,typopt),b1,b2) ->
CIf (loc,sub_extern false scopes vars c,
- (option_map (fun _ -> na) typopt,
- option_map (extern_typ scopes (add_vname vars na)) typopt),
+ (Option.map (fun _ -> na) typopt,
+ Option.map (extern_typ scopes (add_vname vars na)) typopt),
sub_extern false scopes vars b1, sub_extern false scopes vars b2)
| RRec (loc,fk,idv,blv,tyv,bv) ->
@@ -949,12 +944,12 @@ let rec raw_of_pat env = function
let brs = Array.to_list (Array.map (raw_of_pat env) bv) in
let brns = Array.to_list cstr_nargs in
(* ind is None only if no branch and no return type *)
- let ind = out_some indo in
+ let ind = Option.get indo in
let mat = simple_cases_matrix_of_branches ind brns brs in
let indnames,rtn =
if p = PMeta None then (Anonymous,None),None
else
- let nparams,n = out_some ind_nargs in
+ let nparams,n = Option.get ind_nargs in
return_type_of_predicate ind nparams n (raw_of_pat env p) in
RCases (loc,rtn,[raw_of_pat env tm,indnames],mat)
| PFix f -> Detyping.detype false [] env (mkFix f)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 0d9f95795..6fc7a7d31 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -226,7 +226,7 @@ let make_current_scope (tmp_scope,scopes) = option_cons tmp_scope scopes
let set_var_scope loc id (_,scopt,scopes) varscopes =
let idscopes = List.assoc id varscopes in
if !idscopes <> None &
- make_current_scope (out_some !idscopes)
+ make_current_scope (Option.get !idscopes)
<> make_current_scope (scopt,scopes) then
user_err_loc (loc,"set_var_scope",
pr_id id ++ str " already occurs in a different scope")
@@ -796,7 +796,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
let idl = Array.map
(fun (id,(n,order),bl,ty,bd) ->
let intern_ro_arg c f =
- let before, after = list_chop (succ (out_some n)) bl in
+ let before, after = list_chop (succ (Option.get n)) bl in
let ((ids',_,_),rafter) =
List.fold_left intern_local_binder (env,[]) after in
let ro = (intern (ids', tmp_scope, scopes) c) in
@@ -898,21 +898,21 @@ let internalise sigma globalenv env allow_patvar lvar c =
let (tm,ind),nal = intern_case_item env citm in
(tm,ind)::inds,List.fold_left (push_name_env lvar) env nal)
tms ([],env) in
- let rtnpo = option_map (intern_type env') rtnpo in
+ let rtnpo = Option.map (intern_type env') rtnpo in
let eqns' = List.map (intern_eqn (List.length tms) env) eqns in
RCases (loc, rtnpo, tms, List.flatten eqns')
| CLetTuple (loc, nal, (na,po), b, c) ->
let env' = reset_tmp_scope env in
let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in
let env'' = List.fold_left (push_name_env lvar) env ids in
- let p' = option_map (intern_type env'') po in
+ let p' = Option.map (intern_type env'') po in
RLetTuple (loc, nal, (na', p'), b',
intern (List.fold_left (push_name_env lvar) env nal) c)
| CIf (loc, c, (na,po), b1, b2) ->
let env' = reset_tmp_scope env in
let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in
let env'' = List.fold_left (push_name_env lvar) env ids in
- let p' = option_map (intern_type env'') po in
+ let p' = Option.map (intern_type env'') po in
RIf (loc, c', (na', p'), intern env b1, intern env b2)
| CHole loc ->
RHole (loc, Evd.QuestionMark true)
@@ -921,7 +921,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
| CPatVar (loc, _) ->
raise (InternalisationError (loc,NegativeMetavariable))
| CEvar (loc, n, l) ->
- REvar (loc, n, option_map (List.map (intern env)) l)
+ REvar (loc, n, Option.map (List.map (intern env)) l)
| CSort (loc, s) ->
RSort(loc,s)
| CCast (loc, c1, CastConv (k, c2)) ->
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 930cfe739..fc93f455a 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -223,7 +223,7 @@ let app_list1 f = function
let app_opt f = function
| (OptArgType t as u, l) ->
let o = Obj.magic l in
- (u, Obj.repr (option_map (fun x -> out_gen t (f (in_gen t x))) o))
+ (u, Obj.repr (Option.map (fun x -> out_gen t (f (in_gen t x))) o))
| _ -> failwith "Genarg: not an opt"
let app_pair f1 f2 = function
diff --git a/interp/notation.ml b/interp/notation.ml
index aaab6a933..d5de23bc5 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -133,7 +133,7 @@ let push_scopes = List.fold_right push_scope
type local_scopes = tmp_scope_name option * scope_name list
let make_current_scopes (tmp_scope,scopes) =
- option_fold_right push_scope tmp_scope (push_scopes scopes !scope_stack)
+ Option.fold_right push_scope tmp_scope (push_scopes scopes !scope_stack)
(**********************************************************************)
(* Delimiters *)
@@ -143,7 +143,7 @@ let delimiters_map = ref Gmap.empty
let declare_delimiters scope key =
let sc = find_scope scope in
if sc.delimiters <> None && Options.is_verbose () then begin
- let old = out_some sc.delimiters in
+ let old = Option.get sc.delimiters in
Options.if_verbose
warning ("Overwritting previous delimiting key "^old^" in scope "^scope)
end;
@@ -239,12 +239,12 @@ let delay dir int loc x = (dir, (fun () -> int loc x))
let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) =
declare_prim_token_interpreter sc
(fun cont loc -> function Numeral n-> delay dir interp loc n | p -> cont loc p)
- (patl, (fun r -> option_map mkNumeral (uninterp r)), inpat)
+ (patl, (fun r -> Option.map mkNumeral (uninterp r)), inpat)
let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
declare_prim_token_interpreter sc
(fun cont loc -> function String s -> delay dir interp loc s | p -> cont loc p)
- (patl, (fun r -> option_map mkString (uninterp r)), inpat)
+ (patl, (fun r -> Option.map mkString (uninterp r)), inpat)
let check_required_module loc sc (sp,d) =
try let _ = Nametab.absolute_reference sp in ()
@@ -396,7 +396,7 @@ let uninterp_prim_token_cases_pattern c =
let availability_of_prim_token printer_scope local_scopes =
let f scope = Hashtbl.mem prim_token_interpreter_tab scope in
let scopes = make_current_scopes local_scopes in
- option_map snd (find_without_delimiters f (Some printer_scope,None) scopes)
+ Option.map snd (find_without_delimiters f (Some printer_scope,None) scopes)
(* Miscellaneous *)
@@ -454,7 +454,7 @@ type arguments_scope_discharge_request =
| ArgsScopeNoDischarge
let load_arguments_scope _ (_,(_,r,scl)) =
- List.iter (option_iter check_scope) scl;
+ List.iter (Option.iter check_scope) scl;
arguments_scope := Refmap.add r scl !arguments_scope
let cache_arguments_scope o =
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 5a8eafff7..131ce2970 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -59,17 +59,17 @@ let rec unloc = function
| RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c)
| RCases (_,rtntypopt,tml,pl) ->
RCases (dummy_loc,
- (option_map unloc rtntypopt),
+ (Option.map unloc rtntypopt),
List.map (fun (tm,x) -> (unloc tm,x)) tml,
List.map (fun (_,idl,p,c) -> (dummy_loc,idl,p,unloc c)) pl)
| RLetTuple (_,nal,(na,po),b,c) ->
- RLetTuple (dummy_loc,nal,(na,option_map unloc po),unloc b,unloc c)
+ RLetTuple (dummy_loc,nal,(na,Option.map unloc po),unloc b,unloc c)
| RIf (_,c,(na,po),b1,b2) ->
- RIf (dummy_loc,unloc c,(na,option_map unloc po),unloc b1,unloc b2)
+ RIf (dummy_loc,unloc c,(na,Option.map unloc po),unloc b1,unloc b2)
| RRec (_,fk,idl,bl,tyl,bv) ->
RRec (dummy_loc,fk,idl,
Array.map (List.map
- (fun (na,obd,ty) -> (na,option_map unloc obd, unloc ty)))
+ (fun (na,obd,ty) -> (na,Option.map unloc obd, unloc ty)))
bl,
Array.map unloc tyl,
Array.map unloc bv)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index a44f0b6b4..fcf383937 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -94,14 +94,14 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
let ((idl,e),patl) =
list_fold_map (cases_pattern_fold_map loc fold) ([],e) patl in
(loc,idl,patl,f e rhs)) eqnl in
- RCases (loc,option_map (f e') rtntypopt,tml',eqnl')
+ RCases (loc,Option.map (f e') rtntypopt,tml',eqnl')
| ALetTuple (nal,(na,po),b,c) ->
let e,nal = list_fold_map (name_fold_map g) e nal in
let e,na = name_fold_map g e na in
- RLetTuple (loc,nal,(na,option_map (f e) po),f e b,f e c)
+ RLetTuple (loc,nal,(na,Option.map (f e) po),f e b,f e c)
| AIf (c,(na,po),b1,b2) ->
let e,na = name_fold_map g e na in
- RIf (loc,f e c,(na,option_map (f e) po),f e b1,f e b2)
+ RIf (loc,f e c,(na,Option.map (f e) po),f e b1,f e b2)
| ACast (c,k) -> RCast (loc,f e c,
match k with
| CastConv (k,t) -> CastConv (k,f e t)
@@ -185,20 +185,20 @@ let aconstr_and_vars_of_rawconstr a =
| RLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c)
| RCases (_,rtntypopt,tml,eqnl) ->
let f (_,idl,pat,rhs) = found := idl@(!found); (pat,aux rhs) in
- ACases (option_map aux rtntypopt,
+ ACases (Option.map aux rtntypopt,
List.map (fun (tm,(na,x)) ->
add_name found na;
- option_iter
+ Option.iter
(fun (_,_,_,nl) -> List.iter (add_name found) nl) x;
- (aux tm,(na,option_map (fun (_,ind,n,nal) -> (ind,n,nal)) x))) tml,
+ (aux tm,(na,Option.map (fun (_,ind,n,nal) -> (ind,n,nal)) x))) tml,
List.map f eqnl)
| RLetTuple (loc,nal,(na,po),b,c) ->
add_name found na;
List.iter (add_name found) nal;
- ALetTuple (nal,(na,option_map aux po),aux b,aux c)
+ ALetTuple (nal,(na,Option.map aux po),aux b,aux c)
| RIf (loc,c,(na,po),b1,b2) ->
add_name found na;
- AIf (aux c,(na,option_map aux po),aux b1,aux b2)
+ AIf (aux c,(na,Option.map aux po),aux b1,aux b2)
| RCast (_,c,k) -> ACast (aux c,
match k with CastConv (k,t) -> CastConv (k,aux t)
| CastCoerce -> CastCoerce)
@@ -305,11 +305,11 @@ let rec subst_aconstr subst bound raw =
ALetIn (n,r1',r2')
| ACases (rtntypopt,rl,branches) ->
- let rtntypopt' = option_smartmap (subst_aconstr subst bound) rtntypopt
+ let rtntypopt' = Option.smartmap (subst_aconstr subst bound) rtntypopt
and rl' = list_smartmap
(fun (a,(n,signopt) as x) ->
let a' = subst_aconstr subst bound a in
- let signopt' = option_map (fun ((indkn,i),n,nal as z) ->
+ let signopt' = Option.map (fun ((indkn,i),n,nal as z) ->
let indkn' = subst_kn subst indkn in
if indkn == indkn' then z else ((indkn',i),n,nal)) signopt in
if a' == a && signopt' == signopt then x else (a',(n,signopt')))
@@ -327,14 +327,14 @@ let rec subst_aconstr subst bound raw =
ACases (rtntypopt',rl',branches')
| ALetTuple (nal,(na,po),b,c) ->
- let po' = option_smartmap (subst_aconstr subst bound) po
+ let po' = Option.smartmap (subst_aconstr subst bound) po
and b' = subst_aconstr subst bound b
and c' = subst_aconstr subst bound c in
if po' == po && b' == b && c' == c then raw else
ALetTuple (nal,(na,po'),b',c')
| AIf (c,(na,po),b1,b2) ->
- let po' = option_smartmap (subst_aconstr subst bound) po
+ let po' = Option.smartmap (subst_aconstr subst bound) po
and b1' = subst_aconstr subst bound b1
and b2' = subst_aconstr subst bound b2
and c' = subst_aconstr subst bound c in
@@ -368,7 +368,7 @@ let encode_list_value l = RApp (dummy_loc,RVar (dummy_loc,ldots_var),l)
(* Pattern-matching rawconstr and aconstr *)
let abstract_return_type_context pi mklam tml rtno =
- option_map (fun rtn ->
+ Option.map (fun rtn ->
let nal =
List.flatten (List.map (fun (_,(na,t)) ->
match t with Some x -> (pi x)@[na] | None -> [na]) tml) in
@@ -663,8 +663,8 @@ let ids_of_cases_indtype =
let ids_of_cases_tomatch tms =
List.fold_right
(fun (_,(ona,indnal)) l ->
- option_fold_right (fun t -> (@) (ids_of_cases_indtype t))
- indnal (option_fold_right name_cons ona l))
+ Option.fold_right (fun t -> (@) (ids_of_cases_indtype t))
+ indnal (Option.fold_right name_cons ona l))
tms []
let is_constructor id =
@@ -715,17 +715,17 @@ let fold_constr_expr_with_binders g f n acc = function
acc
| CCases (loc,rtnpo,al,bl) ->
let ids = ids_of_cases_tomatch al in
- let acc = option_fold_left (f (List.fold_right g ids n)) acc rtnpo in
+ let acc = Option.fold_left (f (List.fold_right g ids n)) acc rtnpo in
let acc = List.fold_left (f n) acc (List.map fst al) in
List.fold_right (fun (loc,patl,rhs) acc ->
let ids = ids_of_pattern_list patl in
f (Idset.fold g ids n) acc rhs) bl acc
| CLetTuple (loc,nal,(ona,po),b,c) ->
let n' = List.fold_right (name_fold g) nal n in
- f (option_fold_right (name_fold g) ona n') (f n acc b) c
+ f (Option.fold_right (name_fold g) ona n') (f n acc b) c
| CIf (_,c,(ona,po),b1,b2) ->
let acc = f n (f n (f n acc b1) b2) c in
- option_fold_left (f (option_fold_right (name_fold g) ona n)) acc po
+ Option.fold_left (f (Option.fold_right (name_fold g) ona n)) acc po
| CFix (loc,_,l) ->
let n' = List.fold_right (fun (id,_,_,_,_) -> g id) l n in
List.fold_right (fun (_,(_,o),lb,t,c) acc ->
@@ -828,15 +828,15 @@ let map_constr_expr_with_binders g f e = function
(* TODO: apply g on the binding variables in pat... *)
let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in
let ids = ids_of_cases_tomatch a in
- let po = option_map (f (List.fold_right g ids e)) rtnpo in
+ let po = Option.map (f (List.fold_right g ids e)) rtnpo in
CCases (loc, po, List.map (fun (tm,x) -> (f e tm,x)) a,bl)
| CLetTuple (loc,nal,(ona,po),b,c) ->
let e' = List.fold_right (name_fold g) nal e in
- let e'' = option_fold_right (name_fold g) ona e in
- CLetTuple (loc,nal,(ona,option_map (f e'') po),f e b,f e' c)
+ let e'' = Option.fold_right (name_fold g) ona e in
+ CLetTuple (loc,nal,(ona,Option.map (f e'') po),f e b,f e' c)
| CIf (loc,c,(ona,po),b1,b2) ->
- let e' = option_fold_right (name_fold g) ona e in
- CIf (loc,f e c,(ona,option_map (f e') po),f e b1,f e b2)
+ let e' = Option.fold_right (name_fold g) ona e in
+ CIf (loc,f e c,(ona,Option.map (f e') po),f e b1,f e b2)
| CFix (loc,id,dl) ->
CFix (loc,id,List.map (fun (id,n,bl,t,d) ->
let (e',bl') = map_local_binders f g e bl in
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 21:00:03 +0000