X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_procedural%2FproceduralHelpers.mli;h=c021c7c69e8a768d09cc44c9c4524bb9001b5e92;hb=8ae1653eb75d2b57c50e077c49cb9d078313ea9d;hp=97b637d70b126cc21f0c1b80ec28e5faefcf6bbd;hpb=20c9d7116bdfefe8075dd04266836c183d66178e;p=helm.git diff --git a/helm/software/components/acic_procedural/proceduralHelpers.mli b/helm/software/components/acic_procedural/proceduralHelpers.mli index 97b637d70..c021c7c69 100644 --- a/helm/software/components/acic_procedural/proceduralHelpers.mli +++ b/helm/software/components/acic_procedural/proceduralHelpers.mli @@ -24,31 +24,80 @@ *) val mk_fresh_name: - Cic.context -> Cic.name -> Cic.name + bool -> Cic.context -> Cic.name -> Cic.name + +val list_fold_right_cps: + ('b -> 'c) -> (('b -> 'c) -> 'a -> 'b -> 'c) -> 'a list -> 'b -> 'c + +val list_fold_left_cps: + ('b -> 'c) -> (('b -> 'c) -> 'b -> 'a -> 'c) -> 'b -> 'a list -> 'c + val list_map_cps: - ('a list -> 'b) -> (('a -> 'b) -> 'c -> 'b) -> 'c list -> 'b + ('b list -> 'c) -> (('b -> 'c) -> 'a -> 'c) -> 'a list -> 'c + val identity: - 'a -> 'a + 'a -> 'a + val compose: ('a -> 'b) -> ('c -> 'a) -> 'c -> 'b + val fst3: 'a * 'b * 'c -> 'a + val refine: Cic.context -> Cic.term -> Cic.term + val get_type: - Cic.context -> Cic.term -> Cic.term + string -> Cic.context -> Cic.term -> Cic.term + +val is_prop: + Cic.context -> Cic.term -> bool + val is_proof: Cic.context -> Cic.term -> bool + +val is_sort: + Cic.term -> bool + val is_unsafe: int -> Cic.context * Cic.term -> bool + val is_not_atomic: Cic.term -> bool + val is_atomic: Cic.term -> bool + val get_ind_type: UriManager.uri -> int -> int * Cic.inductiveType + +val get_ind_names: + UriManager.uri -> int -> string list + val get_default_eliminator: Cic.context -> UriManager.uri -> int -> Cic.term -> Cic.term + val get_ind_parameters: Cic.context -> Cic.term -> Cic.term list * int -val cic: Cic.annterm -> Cic.term + +val cic: + Cic.annterm -> Cic.term + +val occurs: + Cic.context -> what:Cic.term -> where:Cic.term -> bool + +val name_of_uri: + UriManager.uri -> int option -> int option -> string + +val cic_bc: + Cic.context -> Cic.term -> Cic.term + +val acic_bc: + Cic.context -> Cic.annterm -> Cic.annterm + +val is_acic_proof: + (Cic.id, Cic2acic.sort_kind) Hashtbl.t -> Cic.context -> Cic.annterm -> + bool + +val alpha: + ?flatten:bool -> Cic.context -> Cic.term -> Cic.term -> bool