aboutsummaryrefslogtreecommitdiff
path: root/contrib/funind
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/funind')
-rw-r--r--contrib/funind/functional_principles_proofs.ml8
-rw-r--r--contrib/funind/functional_principles_types.ml6
-rw-r--r--contrib/funind/indfun.ml14
-rw-r--r--contrib/funind/indfun_common.ml36
-rw-r--r--contrib/funind/invfun.ml18
-rw-r--r--contrib/funind/rawterm_to_relation.ml8
-rw-r--r--contrib/funind/rawtermops.ml24
7 files changed, 57 insertions, 57 deletions
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index b10aa782c8..45976d6e5b 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -882,7 +882,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
let f_def = Global.lookup_constant (destConst f) in
let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in
let f_body =
- force (out_some f_def.const_body)
+ force (Option.get f_def.const_body)
in
let params,f_body_with_params = decompose_lam_n nb_params f_body in
let (_,num),(_,_,bodies) = destFix f_body_with_params in
@@ -933,8 +933,8 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
let equation_lemma =
try
let finfos = find_Function_infos (destConst f) in
- mkConst (out_some finfos.equation_lemma)
- with (Not_found | Failure "out_some" as e) ->
+ mkConst (Option.get finfos.equation_lemma)
+ with (Not_found | Option.IsNone as e) ->
let f_id = id_of_label (con_label (destConst f)) in
(*i The next call to mk_equation_id is valid since we will construct the lemma
Ensures by: obvious
@@ -943,7 +943,7 @@ let do_replace params rec_arg_num rev_args_id f fun_num all_funs g =
generate_equation_lemma all_funs f fun_num (List.length params) (List.length rev_args_id) rec_arg_num;
let _ =
match e with
- | Failure "out_some" ->
+ | Option.IsNone ->
let finfos = find_Function_infos (destConst f) in
update_Function
{finfos with
diff --git a/contrib/funind/functional_principles_types.ml b/contrib/funind/functional_principles_types.ml
index cb804f6f2b..72f930b0a6 100644
--- a/contrib/funind/functional_principles_types.ml
+++ b/contrib/funind/functional_principles_types.ml
@@ -115,7 +115,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
it_mkProd_or_LetIn
~init:
(it_mkProd_or_LetIn
- ~init:(option_fold_right
+ ~init:(Option.fold_right
mkProd_or_LetIn
princ_type_info.indarg
princ_type_info.concl
@@ -564,9 +564,9 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent
let opacity =
let finfos = find_Function_infos this_block_funs.(0) in
try
- let equation = out_some finfos.equation_lemma in
+ let equation = Option.get finfos.equation_lemma in
(Global.lookup_constant equation).Declarations.const_opaque
- with Failure "out_some" -> (* non recursive definition *)
+ with Option.IsNone -> (* non recursive definition *)
false
in
let const = {const with const_entry_opaque = opacity } in
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index 199e01525b..3102f1b5d7 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -48,8 +48,8 @@ let functional_induction with_clean c princl pat =
| InType -> finfo.rect_lemma
in
let princ = (* then we get the principle *)
- try mkConst (out_some princ_option )
- with Failure "out_some" ->
+ try mkConst (Option.get princ_option )
+ with Option.IsNone ->
(*i If there is not default lemma defined then,
we cross our finger and try to find a lemma named f_ind
(or f_rec, f_rect) i*)
@@ -589,21 +589,21 @@ let rec add_args id new_args b =
CApp(loc,(pf,add_args id new_args b),
List.map (fun (e,o) -> add_args id new_args e,o) bl)
| CCases(loc,b_option,cel,cal) ->
- CCases(loc,option_map (add_args id new_args) b_option,
+ CCases(loc,Option.map (add_args id new_args) b_option,
List.map (fun (b,(na,b_option)) ->
add_args id new_args b,
- (na,option_map (add_args id new_args) b_option)) cel,
+ (na,Option.map (add_args id new_args) b_option)) cel,
List.map (fun (loc,cpl,e) -> (loc,cpl,add_args id new_args e)) cal
)
| CLetTuple(loc,nal,(na,b_option),b1,b2) ->
- CLetTuple(loc,nal,(na,option_map (add_args id new_args) b_option),
+ CLetTuple(loc,nal,(na,Option.map (add_args id new_args) b_option),
add_args id new_args b1,
add_args id new_args b2
)
| CIf(loc,b1,(na,b_option),b2,b3) ->
CIf(loc,add_args id new_args b1,
- (na,option_map (add_args id new_args) b_option),
+ (na,Option.map (add_args id new_args) b_option),
add_args id new_args b2,
add_args id new_args b3
)
@@ -722,7 +722,7 @@ let make_graph (f_ref:global_reference) =
)
in
let rec_id =
- match List.nth bl' (out_some n) with
+ match List.nth bl' (Option.get n) with
|(_,Name id) -> id | _ -> anomaly ""
in
let new_args =
diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml
index 609504ba5a..c2372d3ed0 100644
--- a/contrib/funind/indfun_common.ml
+++ b/contrib/funind/indfun_common.ml
@@ -319,12 +319,12 @@ let subst_Function (_,subst,finfos) =
in
let function_constant' = do_subst_con finfos.function_constant in
let graph_ind' = do_subst_ind finfos.graph_ind in
- let equation_lemma' = Util.option_smartmap do_subst_con finfos.equation_lemma in
- let correctness_lemma' = Util.option_smartmap do_subst_con finfos.correctness_lemma in
- let completeness_lemma' = Util.option_smartmap do_subst_con finfos.completeness_lemma in
- let rect_lemma' = Util.option_smartmap do_subst_con finfos.rect_lemma in
- let rec_lemma' = Util.option_smartmap do_subst_con finfos.rec_lemma in
- let prop_lemma' = Util.option_smartmap do_subst_con finfos.prop_lemma in
+ let equation_lemma' = Option.smartmap do_subst_con finfos.equation_lemma in
+ let correctness_lemma' = Option.smartmap do_subst_con finfos.correctness_lemma in
+ let completeness_lemma' = Option.smartmap do_subst_con finfos.completeness_lemma in
+ let rect_lemma' = Option.smartmap do_subst_con finfos.rect_lemma in
+ let rec_lemma' = Option.smartmap do_subst_con finfos.rec_lemma in
+ let prop_lemma' = Option.smartmap do_subst_con finfos.prop_lemma in
if function_constant' == finfos.function_constant &&
graph_ind' == finfos.graph_ind &&
equation_lemma' == finfos.equation_lemma &&
@@ -354,12 +354,12 @@ let export_Function infos = Some infos
let discharge_Function (_,finfos) =
let function_constant' = Lib.discharge_con finfos.function_constant
and graph_ind' = Lib.discharge_inductive finfos.graph_ind
- and equation_lemma' = Util.option_smartmap Lib.discharge_con finfos.equation_lemma
- and correctness_lemma' = Util.option_smartmap Lib.discharge_con finfos.correctness_lemma
- and completeness_lemma' = Util.option_smartmap Lib.discharge_con finfos.completeness_lemma
- and rect_lemma' = Util.option_smartmap Lib.discharge_con finfos.rect_lemma
- and rec_lemma' = Util.option_smartmap Lib.discharge_con finfos.rec_lemma
- and prop_lemma' = Util.option_smartmap Lib.discharge_con finfos.prop_lemma
+ and equation_lemma' = Option.smartmap Lib.discharge_con finfos.equation_lemma
+ and correctness_lemma' = Option.smartmap Lib.discharge_con finfos.correctness_lemma
+ and completeness_lemma' = Option.smartmap Lib.discharge_con finfos.completeness_lemma
+ and rect_lemma' = Option.smartmap Lib.discharge_con finfos.rect_lemma
+ and rec_lemma' = Option.smartmap Lib.discharge_con finfos.rec_lemma
+ and prop_lemma' = Option.smartmap Lib.discharge_con finfos.prop_lemma
in
if function_constant' == finfos.function_constant &&
graph_ind' == finfos.graph_ind &&
@@ -387,12 +387,12 @@ let pr_info f_info =
str "function_constant := " ++ Printer.pr_lconstr (mkConst f_info.function_constant)++ fnl () ++
str "function_constant_type := " ++
(try Printer.pr_lconstr (Global.type_of_global (ConstRef f_info.function_constant)) with _ -> mt ()) ++ fnl () ++
- str "equation_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.equation_lemma (mt ()) ) ++ fnl () ++
- str "completeness_lemma :=" ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.completeness_lemma (mt ()) ) ++ fnl () ++
- str "correctness_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.correctness_lemma (mt ()) ) ++ fnl () ++
- str "rect_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rect_lemma (mt ()) ) ++ fnl () ++
- str "rec_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rec_lemma (mt ()) ) ++ fnl () ++
- str "prop_lemma := " ++ (Util.option_fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.prop_lemma (mt ()) ) ++ fnl () ++
+ str "equation_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.equation_lemma (mt ()) ) ++ fnl () ++
+ str "completeness_lemma :=" ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.completeness_lemma (mt ()) ) ++ fnl () ++
+ str "correctness_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.correctness_lemma (mt ()) ) ++ fnl () ++
+ str "rect_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rect_lemma (mt ()) ) ++ fnl () ++
+ str "rec_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.rec_lemma (mt ()) ) ++ fnl () ++
+ str "prop_lemma := " ++ (Option.fold_right (fun v acc -> Printer.pr_lconstr (mkConst v)) f_info.prop_lemma (mt ()) ) ++ fnl () ++
str "graph_ind := " ++ Printer.pr_lconstr (mkInd f_info.graph_ind) ++ fnl ()
let pr_table tb =
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 6171e81948..dcbefe4a40 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -665,8 +665,8 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
if infos.is_general || Rtree.is_infinite graph_def.mind_recargs
then
let eq_lemma =
- try out_some (infos).equation_lemma
- with Failure "out_some" -> anomaly "Cannot find equation lemma"
+ try Option.get (infos).equation_lemma
+ with Option.IsNone -> anomaly "Cannot find equation lemma"
in
tclTHENSEQ[
tclMAP h_intro ids;
@@ -769,7 +769,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
Array.of_list
(List.map
(fun entry ->
- (entry.Entries.const_entry_body, out_some entry.Entries.const_entry_type )
+ (entry.Entries.const_entry_body, Option.get entry.Entries.const_entry_type )
)
(make_scheme (array_map_to_list (fun const -> const,Rawterm.RType None) funs))
)
@@ -960,13 +960,13 @@ let invfun qhyp f =
in
try
let finfos = find_Function_infos f in
- let f_correct = mkConst(out_some finfos.correctness_lemma)
+ let f_correct = mkConst(Option.get finfos.correctness_lemma)
and kn = fst finfos.graph_ind
in
Tactics.try_intros_until (fun hid -> functional_inversion kn hid (mkConst f) f_correct) qhyp
with
| Not_found -> error "No graph found"
- | Failure "out_some" -> error "Cannot use equivalence with graph!"
+ | Option.IsNone -> error "Cannot use equivalence with graph!"
let invfun qhyp f g =
@@ -983,23 +983,23 @@ let invfun qhyp f g =
try
if not (isConst f1) then failwith "";
let finfos = find_Function_infos (destConst f1) in
- let f_correct = mkConst(out_some finfos.correctness_lemma)
+ let f_correct = mkConst(Option.get finfos.correctness_lemma)
and kn = fst finfos.graph_ind
in
functional_inversion kn hid f1 f_correct g
- with | Failure "" | Failure "out_some" | Not_found ->
+ with | Failure "" | Option.IsNone | Not_found ->
try
let f2,_ = decompose_app args.(2) in
if not (isConst f2) then failwith "";
let finfos = find_Function_infos (destConst f2) in
- let f_correct = mkConst(out_some finfos.correctness_lemma)
+ let f_correct = mkConst(Option.get finfos.correctness_lemma)
and kn = fst finfos.graph_ind
in
functional_inversion kn hid f2 f_correct g
with
| Failure "" ->
errorlabstrm "" (str "Hypothesis" ++ Ppconstr.pr_id hid ++ str " must contain at leat one Function")
- | Failure "out_some" ->
+ | Option.IsNone ->
if do_observe ()
then
error "Cannot use equivalence with graph for any side of the equality"
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index b34a1097a3..af0a2addc8 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -368,7 +368,7 @@ let raw_push_named (na,raw_value,raw_typ) env =
match na with
| Anonymous -> env
| Name id ->
- let value = Util.option_map (Pretyping.Default.understand Evd.empty env) raw_value in
+ let value = Option.map (Pretyping.Default.understand Evd.empty env) raw_value in
let typ = Pretyping.Default.understand_type Evd.empty env raw_typ in
Environ.push_named (id,value,typ) env
@@ -398,12 +398,12 @@ let add_pat_variables pat typ env : Environ.env =
| Anonymous -> assert false
| Name id ->
let new_t = substl ctxt t in
- let new_v = option_map (substl ctxt) v in
+ let new_v = Option.map (substl ctxt) v in
observe (str "for variable " ++ Ppconstr.pr_id id ++ fnl () ++
str "old type := " ++ Printer.pr_lconstr t ++ fnl () ++
str "new type := " ++ Printer.pr_lconstr new_t ++ fnl () ++
- option_fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++
- option_fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ())
+ Option.fold_right (fun v _ -> str "old value := " ++ Printer.pr_lconstr v ++ fnl ()) v (mt ()) ++
+ Option.fold_right (fun v _ -> str "new value := " ++ Printer.pr_lconstr v ++ fnl ()) new_v (mt ())
);
(Environ.push_named (id,new_v,new_t) env,mkVar id::ctxt)
)
diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml
index f9e188dacf..e8cce47adb 100644
--- a/contrib/funind/rawtermops.ml
+++ b/contrib/funind/rawtermops.ml
@@ -157,7 +157,7 @@ let change_vars =
let new_mapping = List.fold_left remove_name_from_mapping mapping nal in
RLetTuple(loc,
nal,
- (na, option_map (change_vars mapping) rto),
+ (na, Option.map (change_vars mapping) rto),
change_vars mapping b,
change_vars new_mapping e
)
@@ -170,7 +170,7 @@ let change_vars =
| RIf(loc,b,(na,e_option),lhs,rhs) ->
RIf(loc,
change_vars mapping b,
- (na,option_map (change_vars mapping) e_option),
+ (na,Option.map (change_vars mapping) e_option),
change_vars mapping lhs,
change_vars mapping rhs
)
@@ -338,11 +338,11 @@ let rec alpha_rt excluded rt =
if idmap_is_empty mapping
then rto,t,b
else let replace = change_vars mapping in
- (option_map replace rto, t,replace b)
+ (Option.map replace rto, t,replace b)
in
let new_t = alpha_rt new_excluded new_t in
let new_b = alpha_rt new_excluded new_b in
- let new_rto = option_map (alpha_rt new_excluded) new_rto in
+ let new_rto = Option.map (alpha_rt new_excluded) new_rto in
RLetTuple(loc,new_nal,(na,new_rto),new_t,new_b)
| RCases(loc,infos,el,brl) ->
let new_el =
@@ -351,7 +351,7 @@ let rec alpha_rt excluded rt =
RCases(loc,infos,new_el,List.map (alpha_br excluded) brl)
| RIf(loc,b,(na,e_o),lhs,rhs) ->
RIf(loc,alpha_rt excluded b,
- (na,option_map (alpha_rt excluded) e_o),
+ (na,Option.map (alpha_rt excluded) e_o),
alpha_rt excluded lhs,
alpha_rt excluded rhs
)
@@ -487,7 +487,7 @@ let replace_var_by_term x_id term =
| RLetTuple(loc,nal,(na,rto),def,b) ->
RLetTuple(loc,
nal,
- (na,option_map replace_var_by_pattern rto),
+ (na,Option.map replace_var_by_pattern rto),
replace_var_by_pattern def,
replace_var_by_pattern b
)
@@ -499,7 +499,7 @@ let replace_var_by_term x_id term =
)
| RIf(loc,b,(na,e_option),lhs,rhs) ->
RIf(loc, replace_var_by_pattern b,
- (na,option_map replace_var_by_pattern e_option),
+ (na,Option.map replace_var_by_pattern e_option),
replace_var_by_pattern lhs,
replace_var_by_pattern rhs
)
@@ -640,7 +640,7 @@ let zeta_normalize =
| RLetTuple(loc,nal,(na,rto),def,b) ->
RLetTuple(loc,
nal,
- (na,option_map zeta_normalize_term rto),
+ (na,Option.map zeta_normalize_term rto),
zeta_normalize_term def,
zeta_normalize_term b
)
@@ -652,7 +652,7 @@ let zeta_normalize =
)
| RIf(loc,b,(na,e_option),lhs,rhs) ->
RIf(loc, zeta_normalize_term b,
- (na,option_map zeta_normalize_term e_option),
+ (na,Option.map zeta_normalize_term e_option),
zeta_normalize_term lhs,
zeta_normalize_term rhs
)
@@ -695,17 +695,17 @@ let expand_as =
| RProd(loc,na,t,b) -> RProd(loc,na,expand_as map t, expand_as map b)
| RLetIn(loc,na,v,b) -> RLetIn(loc,na, expand_as map v,expand_as map b)
| RLetTuple(loc,nal,(na,po),v,b) ->
- RLetTuple(loc,nal,(na,option_map (expand_as map) po),
+ RLetTuple(loc,nal,(na,Option.map (expand_as map) po),
expand_as map v, expand_as map b)
| RIf(loc,e,(na,po),br1,br2) ->
- RIf(loc,expand_as map e,(na,option_map (expand_as map) po),
+ RIf(loc,expand_as map e,(na,Option.map (expand_as map) po),
expand_as map br1, expand_as map br2)
| RRec _ -> error "Not handled RRec"
| RDynamic _ -> error "Not handled RDynamic"
| RCast(loc,b,CastConv(kind,t)) -> RCast(loc,expand_as map b,CastConv(kind,expand_as map t))
| RCast(loc,b,CastCoerce) -> RCast(loc,expand_as map b,CastCoerce)
| RCases(loc,po,el,brl) ->
- RCases(loc, option_map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
+ RCases(loc, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el,
List.map (expand_as_br map) brl)
and expand_as_br map (loc,idl,cpl,rt) =
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-25 20:26:55 +0000