diff options
author | 2007-12-05 21:11:19 +0000 | |
---|---|---|
committer | 2007-12-05 21:11:19 +0000 | |
commit | fb75bd254df2eadfc8abd45a646dfe9b1c4a53b6 (patch) | |
tree | 4e1e289a56b97ec2a8fe9de2ac0e6418f7c48d2b /contrib/funind/indfun.ml | |
parent | c6d34ae80622b409733776c3cc4ecf5fce6a8378 (diff) |
Factorisation des opérations sur le type option de Util dans un module
lib/option.ml(i) . J'en profite pour rajouter des primitives de lifting
des fonctions (à un ou deux arguments tous ou partie de type option).
Il reste quelques opérations dans Util à propos desquelles je ne suis
pas trop sûr, ou simplement que j'ai oublié, mais qui attendront demain
car il est tard (comme some_in qui devrait devenir Option.make je
suppose) . Elles s'expriment souvent facilement en fonction des
autres, par exemple "option_compare x y" est égal à "Option.lift2 compare x y"
. Le option_cons devrait faire son chemin dans le module parce qu'il est
assez primitif et qu'il n'y a pas de fonction "cons" dans OCaml.
J'en ai profité aussi pour remplacer les trop nombreux "failwith" par
des erreurs locales au module, donc plus robustes.
J'ai trouvé aussi une fonction qui était définie deux fois, et une
définie dans un module particulier.
Mon seul bémol (mais facile à traiter) c'est la proximité entre le
nom de module Option et l'ancien Options. J'ai pas de meilleure idée de
nom à l'heure qu'il est, ni pour l'un, ni pour l'autre.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10346 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/funind/indfun.ml')
-rw-r--r-- | contrib/funind/indfun.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index 199e01525..3102f1b5d 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 = |