extraction: support for range types

drivers/ocaml64.drv

@@ -205,12 +205,14 @@ module mach.int.Int
 end
 
 module mach.int.Int63
-  syntax val of_int "Z.to_int %1"
-  syntax converter of_int "%1"
+  syntax type     int63     "int"
 
-  syntax function to_int "Z.of_int %1"
+  syntax literal   int63    "%1"
+  syntax converter of_int   "%1"
+
+  syntax val      of_int    "Z.to_int %1"
+  syntax function to_int    "Z.of_int %1"
 
-  syntax type     int63     "int"
   syntax constant min_int63 "Z.of_int min_int"
   syntax constant max_int63 "Z.of_int max_int"
   syntax constant min_int   "min_int"

src/mlw/compile.ml

@@ -338,6 +338,8 @@ module Translate = struct
           Mltree.Tapp (its.its_ts.ts_name, args) in
     loop t
 
+  let ty_int = mlty_of_ity MaskVisible ity_int
+
   let pvty pv =
     if pv.pv_ghost then ML.mk_var (pv_name pv) ML.tunit true
     else let (vs, vs_ty) = vsty pv.pv_vs in
@@ -457,7 +459,6 @@ module Translate = struct
         ML.e_seq body_expr rec_call ML.ity_unit eff Slab.empty in
       ML.mk_expr (Mltree.Eif (test, seq_expr, ML.e_unit)) ML.ity_unit
         eff Slab.empty in
-    let ty_int = mlty_of_ity MaskVisible ity_int in
     let for_call_expr = let for_call = Mltree.Eapp (for_rs, [from_expr]) in
       ML.mk_expr for_call ML.ity_unit eff Slab.empty in
     let pv_name pv = pv.pv_vs.vs_name in
@@ -685,9 +686,12 @@ module Translate = struct
                 ML.mk_its_defn id args is_private (Some (Mltree.Drecord pjl))
           end
       | Alias t, _, _ ->
-          ML.mk_its_defn id args is_private (* FIXME ? is this a good mask ? *)
+          ML.mk_its_defn id args is_private (* FIXME? is this a good mask? *)
             (Some (Mltree.Dalias (mlty_of_ity MaskVisible t)))
-      | Range _, _, _ -> assert false (* TODO *)
+      | Range _, [], [] ->
+          assert (args = []); (* a range type is not polymorphic *)
+          ML.mk_its_defn id [] is_private (Some (Mltree.Dalias ty_int))
+      | Range _, _, _ -> assert false (* a range type has no field/constructor *)
       | Float _, _, _ -> assert false (* TODO *)
     end
 

src/mlw/ocaml_printer.ml

@@ -28,6 +28,7 @@ open Printer
 type info = {
   info_syn          : syntax_map;
   info_convert      : syntax_map;
+  info_literal      : syntax_map;
   info_current_th   : Theory.theory;
   info_current_mo   : Pmodule.pmodule option;
   info_th_known_map : Decl.known_map;
@@ -281,6 +282,13 @@ module Print = struct
         Loc.errorm ?loc "Function %a cannot be extracted" Expr.print_rs rs
     | _ -> ()
 
+  let print_constant fmt e = begin match e.e_node with
+    | Econst c ->
+        let s = BigInt.to_string (Number.compute_int_constant c) in
+        if c.Number.ic_negative then fprintf fmt "(%s)" s
+        else fprintf fmt "%s" s
+    | _ -> assert false end
+
   let rec print_apply_args info fmt = function
     | expr :: exprl, pv :: pvl ->
         if is_optional ~labels:(pv_name pv).id_label then
@@ -311,12 +319,6 @@ module Print = struct
     match query_syntax info.info_convert rs.rs_name,
           query_syntax info.info_syn rs.rs_name, pvl with
     | Some s, _, [{e_node = Econst _}] ->
-        let print_constant fmt e = match e.e_node with
-          | Econst c ->
-              let s = BigInt.to_string (Number.compute_int_constant c) in
-              if c.Number.ic_negative then fprintf fmt "(%s)" s
-              else fprintf fmt "%s" s
-          | _ -> assert false in
         syntax_arguments s print_constant fmt pvl
     | _, Some s, _ (* when is_local_id info rs.rs_name  *)->
         syntax_arguments s (print_expr ~paren:true info) fmt pvl;
@@ -409,10 +411,16 @@ module Print = struct
         forget_vars args
     | Lany (rs, _, _) -> check_val_in_drv info rs
 
-  and print_enode ?(paren=false) info fmt = function
+  and print_expr ?(paren=false) info fmt e = match e.e_node with
     | Econst c ->
         let n = Number.compute_int_constant c in
-        fprintf fmt "(Z.of_string \"%s\")" (BigInt.to_string n)
+        let n = BigInt.to_string n in
+        let id = match e.e_ity with
+          | I { ity_node = Ityapp ({its_ts = ts},_,_) } -> ts.ts_name
+          | _ -> assert false in
+        (match query_syntax info.info_literal id with
+         | Some s -> syntax_arguments s print_constant fmt [e]
+         | None   -> fprintf fmt "(Z.of_string \"%s\")" n)
     | Evar pvs ->
         (print_lident info) fmt (pv_name pvs)
     | Elet (let_def, e) ->
@@ -432,12 +440,6 @@ module Print = struct
     | Eapp (rs, pvl) ->
         begin match query_syntax info.info_convert rs.rs_name, pvl with
           | Some s, [{e_node = Econst _}] ->
-              let print_constant fmt e = begin match e.e_node with
-                | Econst c ->
-                    let s = BigInt.to_string (Number.compute_int_constant c) in
-                    if c.Number.ic_negative then fprintf fmt "(%s)" s
-                    else fprintf fmt "%s" s
-                | _ -> assert false end in
               syntax_arguments s print_constant fmt pvl
           | _ ->
               fprintf fmt (protect_on paren "%a")
@@ -546,9 +548,6 @@ module Print = struct
         fprintf fmt "@[<hov 4>| %a %a ->@ %a@]" (print_uident info) (xs.xs_name)
           (print_list nothing print_var) pvl (print_expr info) e
 
-  and print_expr ?(paren=false) info fmt e =
-    print_enode ~paren info fmt e.e_node
-
   let print_type_decl info fst fmt its =
     let print_constr fmt (id, cs_args) =
       match cs_args with
@@ -641,6 +640,7 @@ let print_decl =
     let info = {
       info_syn          = pargs.Pdriver.syntax;
       info_convert      = pargs.Pdriver.converter;
+      info_literal      = pargs.Pdriver.literal;
       info_current_th   = th;
       info_current_mo   = Some m;
       info_th_known_map = th.th_known;

src/mlw/pdriver.ml

@@ -27,6 +27,7 @@ type driver = {
   drv_blacklist   : Printer.blacklist;
   drv_syntax      : Printer.syntax_map;
   drv_converter   : Printer.syntax_map;
+  drv_literal     : Printer.syntax_map;
 }
 
 type printer_args = {
@@ -36,6 +37,7 @@ type printer_args = {
   blacklist   : Printer.blacklist;
   syntax      : Printer.syntax_map;
   converter   : Printer.syntax_map;
+  literal     : Printer.syntax_map;
 }
 
 let load_file file =
@@ -85,6 +87,7 @@ let load_driver env file extra_files =
   let thprelude = ref Mid.empty in
   let syntax_map = ref Mid.empty in
   let converter_map = ref Mid.empty in
+  let literal_map = ref Mid.empty in
   let qualid    = ref [] in
 
   let find_pr th (loc,q) = try Theory.ns_find_pr th.th_export q
@@ -106,6 +109,8 @@ let load_driver env file extra_files =
     syntax_map := Mid.add id (s,if b then 1 else 0) !syntax_map in
   let add_converter id s b =
     converter_map := Mid.add id (s,if b then 1 else 0) !converter_map in
+  let add_literal id s b =
+    literal_map := Mid.add id (s,if b then 1 else 0) !literal_map in
   let add_local th = function
     | Rprelude s ->
         let l = Mid.find_def [] th.th_name !thprelude in
@@ -124,6 +129,9 @@ let load_driver env file extra_files =
         add_syntax ps.ls_name s b
     | Rconverter _ ->
         Loc.errorm "Syntax converter cannot be used in pure theories"
+    | Rliteral (q,s,b) ->
+        let ts = find_ts th q in
+        add_literal ts.ts_name s b
     | Rremovepr (q) ->
       ignore (find_pr th q)
     | Rremoveall ->
@@ -156,7 +164,6 @@ let load_driver env file extra_files =
         in
         let m = lookup_meta s in
         ignore (create_meta m (List.map convert al))
-    | Rliteral _ -> assert false (* TODO *)
   in
   let add_local th (loc,rule) = Loc.try2 ~loc add_local th rule in
   let open Pmodule in
@@ -214,6 +221,7 @@ let load_driver env file extra_files =
     drv_blacklist   = Queue.fold (fun l s -> s :: l) [] blacklist;
     drv_syntax      = !syntax_map;
     drv_converter   = !converter_map;
+    drv_literal     = !literal_map;
   }
 
 (* registering printers for programs *)
@@ -250,6 +258,7 @@ let lookup_printer drv =
       blacklist   = drv.drv_blacklist;
       syntax      = drv.drv_syntax;
       converter   = drv.drv_converter;
+      literal     = drv.drv_literal;
     }
   in
   try
@@ -259,12 +268,6 @@ let lookup_printer drv =
 let list_printers () =
   Hstr.fold (fun k (desc,_,_) acc -> (k,desc)::acc) printers []
 
-(*
-let extract_module ?old drv fmt m =
-  let printer = lookup_printer p printer_args in
-  Format.fprintf fmt "@[%a@]@?" (printer ?old) m
- *)
-
 (* exception report *)
 
 let string_of_qualid thl idl =
@@ -289,6 +292,8 @@ let () = Exn_printer.register (fun fmt exn ->
       "%a is not a function symbol" Pretty.print_ls ls
   | PSymExpected ls -> fprintf fmt
       "%a is not a predicate symbol" Pretty.print_ls ls
+  | NoPrinter ->
+      fprintf fmt "Missing printer in driver"
   | KnownPrinter s ->
       fprintf fmt "Program printer '%s' is already registered" s
   | UnknownPrinter s ->

src/mlw/pdriver.mli

@@ -19,6 +19,7 @@ type driver = private {
   drv_blacklist   : Printer.blacklist;
   drv_syntax      : Printer.syntax_map;
   drv_converter   : Printer.syntax_map;
+  drv_literal     : Printer.syntax_map;
 }
 
 
@@ -29,6 +30,7 @@ type printer_args = private {
   blacklist   : Printer.blacklist;
   syntax      : Printer.syntax_map;
   converter   : Printer.syntax_map;
+  literal     : Printer.syntax_map;
 }
 
 val load_driver : Env.env -> string -> string list -> driver