coq output

drivers/coq.drv

@@ -88,3 +88,9 @@ theory real.Abs
 
 end
 
+theory real.FromInt
+
+  syntax logic from_int "(IZR %1)"
+
+end
+

src/core/ident.mli

@@ -69,28 +69,29 @@ val id_from_user : ident -> Loc.position option
 
 type ident_printer
 
-(* start a new printer with a sanitizing function and a blacklist *)
 val create_ident_printer :
   ?sanitizer : (string -> string) -> string list -> ident_printer
+(** start a new printer with a sanitizing function and a blacklist *)
 
-(* use ident_printer to generate a unique name for ident *)
-(* an optional sanitizer is applied over the printer's sanitizer *)
 val id_unique :
   ident_printer -> ?sanitizer : (string -> string) -> ident -> string
+(** use ident_printer to generate a unique name for ident 
+    an optional sanitizer is applied over the printer's sanitizer *)
 
-(* Uniquify string *)
 val string_unique : ident_printer -> string -> string
+(** Uniquify string *)
 
-(* forget an ident *)
 val forget_id : ident_printer -> ident -> unit
+(** forget an ident *)
 
-(* forget all idents *)
 val forget_all : ident_printer -> unit
+(** forget all idents *)
 
-(* generic sanitizer taking a separate encoder for the first letter *)
 val sanitizer : (char -> string) -> (char -> string) -> string -> string
+(** generic sanitizer taking a separate encoder for the first letter *)
+
+(** various character encoders *)
 
-(* various character encoders *)
 val char_to_alpha : char -> string
 val char_to_lalpha : char -> string
 val char_to_ualpha : char -> string

src/printer/coq.ml

@@ -49,8 +49,7 @@ let tv_set = ref Sid.empty
 (* type variables *)
 let print_tv fmt tv =
   tv_set := Sid.add tv.tv_name !tv_set;
-  let sanitize n = n in
-  let n = id_unique iprinter ~sanitizer:sanitize tv.tv_name in
+  let n = id_unique iprinter tv.tv_name in
   fprintf fmt "%s" n
 
 let forget_tvs () =
@@ -59,8 +58,7 @@ let forget_tvs () =
 
 (* logic variables *)
 let print_vs fmt vs =
-  let sanitize n = n in
-  let n = id_unique iprinter ~sanitizer:sanitize vs.vs_name in
+  let n = id_unique iprinter vs.vs_name in
   fprintf fmt "%s" n
 
 let forget_var vs = forget_id iprinter vs.vs_name
@@ -69,10 +67,9 @@ let print_ts fmt ts =
   fprintf fmt "%s" (id_unique tprinter ts.ts_name)
 
 let print_ls fmt ls =
-  let n = if ls.ls_constr
-    then id_unique lprinter ~sanitizer:String.capitalize ls.ls_name
-    else id_unique lprinter ls.ls_name
-  in
+  let n = id_unique lprinter ls.ls_name in
+(*  if ls.ls_name = "mod" then *)
+    eprintf "Coq.print_ls: %s -> %s@." ls.ls_name.id_long n;
   fprintf fmt "%s" n
 
 let print_pr fmt pr =
@@ -80,8 +77,6 @@ let print_pr fmt pr =
 
 (** Types *)
 
-let rec ns_comma fmt () = fprintf fmt ",@,"
-
 let rec print_ty drv fmt ty = match ty.ty_node with
   | Tyvar v -> print_tv fmt v
   | Tyapp (ts, tl) ->
@@ -257,23 +252,19 @@ let print_constr drv fmt cs =
   fprintf fmt "@[<hov 4>| %a%a@]" print_ls cs
     (print_paren_l (print_ty drv)) cs.ls_args
 
-let print_ty_args fmt = function
-  | [] -> ()
-  | [tv] -> fprintf fmt " %a" print_tv tv
-  | l -> fprintf fmt " (%a)" (print_list ns_comma print_tv) l
-
 let print_type_decl drv fmt (ts,def) = match def with
   | Tabstract -> begin match ts.ts_def with
       | None ->
-          fprintf fmt "@[<hov 2>Parameter %a : %a -> Type.@]@\n@\n"
-            print_ts ts print_ty_args ts.ts_args 
+          fprintf fmt "@[<hov 2>Parameter %a : %aType.@]@\n@\n"
+            print_ts ts (print_arrow_list print_tv) ts.ts_args 
       | Some ty ->
           fprintf fmt "@[<hov 2>Definition %a %a :=@ %a@]@\n@\n"
-            print_ts ts print_ty_args ts.ts_args (print_ty drv) ty
+            print_ts ts (print_arrow_list print_tv) ts.ts_args 
+	    (print_ty drv) ty
       end
   | Talgebraic csl ->
-      fprintf fmt "@[<hov 2>Inductive %a %a :=@\n@[<hov>%a@]@]@\n@\n"
-        print_ts ts print_ty_args ts.ts_args 
+      fprintf fmt "@[<hov 2>Inductive %a %a :=@\n@[<hov>%a@].@]@\n@\n"
+        print_ts ts (print_arrow_list print_tv) ts.ts_args 
         (print_list newline (print_constr drv)) csl
 
 let print_type_decl drv fmt d =
@@ -321,9 +312,13 @@ let print_pkind fmt = function
   | Plemma -> fprintf fmt "Lemma"
   | Pgoal  -> fprintf fmt "Theorem"
 
+let print_proof fmt = function
+  | Paxiom -> ()
+  | Plemma | Pgoal  -> fprintf fmt "Admitted.@\n"
+
 let print_prop_decl drv fmt (k,pr,f) =
-  fprintf fmt "@[<hov 2>%a %a : %a.@]@\n@\n" print_pkind k
-    print_pr pr (print_fmla drv) f
+  fprintf fmt "@[<hov 2>%a %a : %a.@]@\n%a@\n" print_pkind k
+    print_pr pr (print_fmla drv) f print_proof k
 
 let print_prop_decl drv fmt (k,pr,f) =
   match k, query_ident drv pr.pr_name with

theories/floating_point.why

@@ -3,7 +3,7 @@
 (* definition of IEEE-754 rounding modes *)
 theory Rounding
 
-  type mode = Near | Zero | Up | Down | NearTiesToAway
+  type mode = NearestTiesToEven | ToZero | Up | Down | NearTiesToAway
     (** nearest ties to even, to zero, upward, downward, nearest ties to away *)
 
 end
@@ -120,7 +120,7 @@ theory Test
   use import Rounding
   use import Single
 
-  lemma Round_01: round(Near,0.1) = 0x0.199999Ap0
+  lemma Round_01: round(NearestTiesToEven,0.1) = 0x0.199999Ap0
 
 end