-let rec rational_of_constr c =
- match kind_of_term c with
- | Cast (c,t) -> (rational_of_constr c)
- | App (c,args) ->
- (match kind_of_term c with
- Const c ->
- (match (string_of_path c) with
- "Coq.Reals.Rdefinitions.Ropp" ->
- rop (rational_of_constr args.(0))
- |"Coq.Reals.Rdefinitions.Rinv" ->
- rinv (rational_of_constr args.(0))
- |"Coq.Reals.Rdefinitions.Rmult" ->
- rmult (rational_of_constr args.(0))
- (rational_of_constr args.(1))
- |"Coq.Reals.Rdefinitions.Rdiv" ->
- rdiv (rational_of_constr args.(0))
- (rational_of_constr args.(1))
- |"Coq.Reals.Rdefinitions.Rplus" ->
- rplus (rational_of_constr args.(0))
- (rational_of_constr args.(1))
- |"Coq.Reals.Rdefinitions.Rminus" ->
- rminus (rational_of_constr args.(0))
- (rational_of_constr args.(1))
+(* coq wrapper
+let string_of_constr = string_of_term
+;;
+*)
+
+(**
+ @param t a term
+ @raise Failure if conversion is impossible
+ @return rational proiection of t
+*)
+let rec rational_of_term t =
+ (* fun to apply f to the first and second rational-term of l *)
+ let rat_of_binop f l =
+ let a = List.hd l and
+ b = List.hd(List.tl l) in
+ f (rational_of_term a) (rational_of_term b)
+ in
+ (* as before, but f is unary *)
+ let rat_of_unop f l =
+ f (rational_of_term (List.hd l))
+ in
+ match t with
+ | Cic.Cast (t1,t2) -> (rational_of_term t1)
+ | Cic.Appl (t1::next) ->
+ (match t1 with
+ Cic.Const (u,boh) ->
+ (match (UriManager.string_of_uri u) with
+ "cic:/Coq/Reals/Rdefinitions/Ropp" ->
+ rat_of_unop rop next
+ |"cic:/Coq/Reals/Rdefinitions/Rinv" ->
+ rat_of_unop rinv next
+ |"cic:/Coq/Reals/Rdefinitions/Rmult" ->
+ rat_of_binop rmult next
+ |"cic:/Coq/Reals/Rdefinitions/Rdiv" ->
+ rat_of_binop rdiv next
+ |"cic:/Coq/Reals/Rdefinitions/Rplus" ->
+ rat_of_binop rplus next
+ |"cic:/Coq/Reals/Rdefinitions/Rminus" ->
+ rat_of_binop rminus next