interfaces part 1

generator/characteristic.ml

@@ -149,9 +149,8 @@ let lift_typ_exp ty =
 (** Translates a Caml type scheme into a Coq type *)
 
 let lift_typ_sch ty =
-   mark_loops ty;
-   let t = btree_of_typexp true ty in
-   let fv = fv_btyp~through_arrow:false t in
+   let t = btyp_of_typ_sch_simple ty in
+   let fv = fv_btyp ~through_arrow:false t in
    fv, lift_btyp t
 
 (** Translates the type of a Caml expression into a Coq type *)
@@ -770,7 +769,7 @@ let rec cfg_structure_item s : cftops =
       end else if (List.length pat_expr_list = 1) then begin (* later: check it is not a function *)
         let (pat,bod) = List.hd pat_expr_list in
         let x = pattern_name pat in
-        if (skip_cf_for x) then [] else begin
+        if (hack_recognize_okasaki_lazy x) then [] else begin
         let fvs_typ, typ = lift_typ_sch pat.pat_type in
         let fvs = List.map name_of_type fvs in
         let fvs_strict = list_intersect fvs fvs_typ in
@@ -905,7 +904,7 @@ and cfg_type_record (name,dec) =
    [ Coqtop_record top ] 
    @ (implicit_decl)
    @ [ Coqtop_hint_constructors ([record_name], "typeclass_instances") ]
-   @ record_functions record_name (record_name ^ "_of") (make_upper x) params fields_names fields_types
+   @ record_functions record_name (record_name ^ "_of") (str_capitalize_1 x) params fields_names fields_types
   (*  todo: move le "_of" *)
 
 (** Auxiliary function to generate stuff for records *)
@@ -924,7 +923,7 @@ and record_functions record_name record_constr repr_name params fields_names fie
       [ Coqtop_param (nth i get_names, val_type); 
         Coqtop_param (nth i set_names, val_type) ] in
    
-   let logicals = List.map make_upper_2 fields_names (* for_indices (fun i -> sprintf "A%d" (i+1)) *) in
+   let logicals = List.map str_capitalize_1 fields_names (* for_indices (fun i -> sprintf "A%d" (i+1)) *) in
    let reprs = for_indices (fun i -> sprintf "_T%d" (i+1)) in
    let abstracts = for_indices (fun i -> sprintf "_X%d" (i+1)) in
    let concretes = for_indices (fun i -> sprintf "x%d" (i+1)) in

generator/mytools.ml

-(** This file contains some helper functions *)
 
 
 (**************************************************************)
@@ -16,7 +15,7 @@ let unsome = function
   | None -> assert false
   | Some v -> v
 
-let option_to_list = function (* todo: rename as [list_of_option] *)
+let list_of_option = function
   | None -> []
   | Some v -> [v]
 
@@ -128,13 +127,13 @@ let str_replace char1 char2 s =
    done;
    s2
 
-let make_upper s =
+let str_capitalize_1 s =
    if String.length s <= 0 then s else
    let s' = String.copy s in
    s'.[0] <- Char.uppercase s.[0];
    s'
 
-let make_upper_2 s =
+let str_capitalize_2 s =
    if String.length s < 2 then s else
    let s' = String.copy s in
    s'.[1] <- Char.uppercase s.[1];
@@ -156,7 +155,6 @@ let file_put_contents filename text =
 (**************************************************************)
 (** Try-with manipulation functions *)
 
-(** Tests whether a function throws [Not_found] *)
 let gives_not_found f =
    try ignore (f()); false 
    with Not_found -> true
@@ -185,12 +183,12 @@ let show_option f ox =
    | None -> ""
    | Some x -> f x
 
-let show_str s =
-  s
-
 let show_par required s =
   if required then "(" ^ s ^ ")" else s
 
+let show_str s =
+  s
+
 
 (**************************************************************)
 (** Error messages *)

generator/mytools.mli

+(** This file contains some helper functions.
+    Ideally, many of these functions would come from a standard,
+    extensive Coq library. *)
+
+(**************************************************************)
+(** Option manipulation functions *)
+
+val option_map : ('a -> 'b) -> 'a option -> 'b option
+val option_iter : ('a -> unit) -> 'a option -> unit
+val unsome : 'a option -> 'a
+val list_of_option : 'a option -> 'a list
+val option_app : 'a -> ('b -> 'a) -> 'b option -> 'a
+val unsome_safe : 'a -> 'a option -> 'a
+val bool_of_option : bool option -> bool
+
+
+(**************************************************************)
+(** List manipulation functions *)
+
+val list_make : int -> 'a -> 'a list
+val list_mapi : (int -> 'a -> 'b) -> 'a list -> 'b list
+val list_nat : int -> int list
+val list_separ : 'a -> 'a list -> 'a list
+val filter_somes : 'a option list -> 'a list
+val list_unique : 'a list -> 'a list
+val list_intersect : 'a list -> 'a list -> 'a list
+val list_minus : 'a list -> 'a list -> 'a list
+val list_concat_map : ('a -> 'b list) -> 'a list -> 'b list
+val list_assoc_option : 'a -> ('a * 'b) list -> 'b option
+val assoc_list_map : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list
+val list_remove : int -> 'a list -> 'a list
+val list_replace : int -> 'a -> 'a list -> 'a list
+val list_replace_nth : int -> 'a list -> 'a list -> 'a list
+val list_ksort : ('a -> 'a -> int) -> ('a * 'b) list -> ('a * 'b) list
+val list_index : 'a -> 'a list -> int
+
+
+(**************************************************************)
+(** String manipulation functions *)
+
+val str_cmp : string -> string -> int
+val str_starts_with : string -> string -> bool
+val str_replace : char -> char -> string -> string
+
+(** Capitalize the first letter of a string (if any) *)
+
+val str_capitalize_1 : string -> string
+
+(** Capitalize the second letter of a string (if any) *)
+
+val str_capitalize_2 : string -> string
+
+
+(**************************************************************)
+(** File manipulation functions *)
+
+val file_put_contents : string -> string -> unit
+
+
+(**************************************************************)
+(** Try-with manipulation functions *)
+
+(** Tests whether a function throws [Not_found],
+    and returns the result in the form of a boolean value. *)
+
+val gives_not_found : (unit -> 'a) -> bool
+
+
+(**************************************************************)
+(** Pretty-printing functions *)
+
+val lin0 : string  (** The empty string *)
+val lin1 : string  (** The line-return string *)
+val lin2 : string  (** The double line-return string *)
+
+(** Display a list of values with a separator *)
+
+val show_list : ('a -> string) -> string -> 'a list -> string
+
+(** Display a list of values with a separator, including it at the front *)
+
+val show_listp : ('a -> string) -> string -> 'a list -> string
+
+(** Display a list of values with a separator, including it at the back *)
+
+val show_listq : ('a -> string) -> string -> 'a list -> string
+
+(** Dispaly the content of an option, else the empty string *)
+
+val show_option : ('a -> string) -> 'a option -> string
+
+(** Display a string, enclosed using parentheses if the first argument is true *)
+
+val show_par : bool -> string -> string
+
+(** Display *)
+
+val show_str : 'a -> 'a
+
+
+(**************************************************************)
+(** Error messages *)
+
+(** Display a string on stdout *)
+
+val output : string -> unit
+
+(** Display a string on stdout, preceeded by a "WARNING" string *)
+
+val warning : string -> unit
+
+(** Display a message explaining that a feature is not supported *)
+
+val unsupported : string -> 'a

generator/normalize.ml

@@ -318,7 +318,7 @@ let normalize_expression named e =
           *)
           let e1', b = aux false e1 in
           assign_var (return (Pexp_ifthenelse (e1', protect named e2, Some (protect named e3)))) b
-             (* todo:  tester: if then else fun x -> x *)
+             (* todo:  tester: if then else fun x -> x *)
       | Pexp_sequence (e1,e2) -> 
           let e1', b = aux true e1 in
           let tunit = Some { ptyp_desc = Ptyp_constr (Lident "unit", []); ptyp_loc = loc } in

generator/primitives.ml

 open Mytools
 
-(** This file contains information for properly handling 
-    Caml builtin functions and Coq builtin functions and
-    data types. *)
  
 
 (*#########################################################################*)
@@ -185,7 +182,7 @@ let find_builtin_constructor p =
     of [!$] as a keyword for forcing lazy expressions is one such
     exception. *)
 
-let skip_cf_for = function
+let hack_recognize_okasaki_lazy = function
   | "!$" -> true
   | _ -> false
 
@@ -193,5 +190,6 @@ let skip_cf_for = function
     generation of an [Require Import] statement. *)
 
 let is_primitive_module n =
-   List.mem n [ "NullPointers"; "StrongPointers"; "Okasaki"; "OkaStream" ]
+   List.mem n [ "NullPointers"; "StrongPointers" ]
+   (* ; "Okasaki"; "OkaStream" *)
 

generator/primitives.mli

+
+(** This module contains information for properly handling 
+    OCaml builtin functions and Coq builtin functions and
+    data types. *)
+
+
+
+
+(** [find_inlined_primitive] finds out, for a given function, 
+    applied to a given number of arguments, if it should be inlined 
+    during the normalization phase of the source program. 
+    For example, "Pervasives.+" applied to 2 arguments should
+    be inlined using "Coq.ZArith.BinInt.Zplus". *)
+
+val find_inlined_primitive : string -> int -> string option
+
+(** [is_inlined_primitive] returns true if 
+    [find_inlined_primitive] provides some result. *)
+
+val is_inlined_primitive : string -> int -> bool
+
+(* HACK! Same as above, but only checks base on the tail of the name,
+   e.g. considering only "+" instead of "Pervasives.+" 
+   This hack is only correct if we forbit the rebinding of
+   these special primitive names, however this check is not
+   yet implemented. *)
+
+val is_inlined_primitive_hack : string -> int -> bool
+
+(** [find_primitive] finds the primitive functions associated with the 
+    argument, and return an optional result.    
+    For example, given "Pervasives.ref" it gives "ml_ref" *)
+
+val find_primitive : string -> string option
+
+(** [find_builtin_constructor] finds the primitive data-constructor associated 
+    with the argument, and return an optional result.    
+    For example, given "::" it gives "Coq.Lists.List.cons" and 1,
+    where 1 is the number of type arguments to cons in Coq. *)
+
+val find_builtin_constructor : string -> (string * int) option
+
+(** Below is a HACK for the [!$] symbol used in Okasaki's code to mean "lazy" *)
+
+val hack_recognize_okasaki_lazy : string -> bool
+
+(** [is_primitive_module] Recognizes builtin modules that have a special treatment,
+    namely "NullPointers" and "StrongPointers" *)
+
+val is_primitive_module : string -> bool
+
+(** [primitive_special] is NOT CURRENTLY USED 
+    (optimized lifting of Zdiv and Zmod operations) *)
+
+val primitive_special : int
+

generator/print_coq.mli

+
+(* Width for printing
+   TODO: how to change it? *)
+
+val width : int ref
+
+(** Print a list of coqtop declaration into a string *)
+
+val tops : Coq.coqtops -> string

generator/print_past.mli

+
+(** Printing of the parse tree *)
+
+val string_of_ident : Ident.t -> string
+val string_of_lident : Longident.t -> string
+val string_of_constant : Asttypes.constant -> string
+val string_of_recflag : Asttypes.rec_flag -> string
+val string_of_pattern : 'a -> Parsetree.pattern -> string
+val string_of_expression : bool -> Parsetree.expression -> string
+val string_of_module : Parsetree.module_expr -> string
+val string_of_structure : Parsetree.structure -> string
+val string_of_structure_item : Parsetree.structure_item -> string
+val string_of_toplevel_phrase : Parsetree.toplevel_phrase -> string
+val string_of_source : Parsetree.toplevel_phrase list -> string

generator/print_tast.ml

@@ -20,9 +20,6 @@ let string_of_typed_var s t =
 let string_of_path p = 
    Path.name p
 
-let show_string s = 
-  s
-
 (*#########################################################################*)
 (* ** Printing of patterns *)
 

generator/print_tast.mli

+
+(** Printing of the typed tree *)
+
+val string_of_typed_var : string -> Types.type_expr -> string
+val string_of_path : Path.t -> string
+val string_of_pattern : 'a -> Typedtree.pattern -> string
+val string_of_let_pattern : 'a -> Types.type_expr list -> Typedtree.pattern -> string
+val string_of_expression : bool -> Typedtree.expression -> string
+val string_of_module : Typedtree.module_expr -> string
+val string_of_structure : Typedtree.structure -> string
+val string_of_structure_item : Typedtree.structure_item -> string

generator/print_type.ml

@@ -141,7 +141,7 @@ let rec btree_of_typexp sch ty =
   else pr_typ ()
 
 and btree_of_typlist sch tyl =
-  List.map (btree_of_typexp sch) tyl
+   List.map (btree_of_typexp sch) tyl
 
 
 (*#########################################################################*)
@@ -157,7 +157,7 @@ let btyp_of_typ_exp t =
    btree_of_typexp false t
 
 (** Translates of a type scheme [t] into a [btyp], including the call
-    to [mark_loops]. *)
+    to [mark_loops]. CURRENTLY NOT USED *)
 
 let btyp_of_typ_sch t =
    mark_loops t;
@@ -167,6 +167,15 @@ let btyp_of_typ_sch t =
    let fvta = list_concat_map (function Occ_alias x -> [x] | _ -> []) fvt in
    (fvtg, fvta, typ)
 
+(** Translates of a type scheme [t] into a [btyp], including the call
+    to [mark_loops]. Returns the tree with head quantification of
+    free type variables. *)
+
+let btyp_of_typ_sch_simple ty = 
+   mark_loops ty;  
+   btree_of_typexp true ty
+
+
 
 (*#########################################################################*)
 (* ** Printing of simple type representations *)

generator/print_type.mli

+
+(** Simple grammar of types *)
+
+type btyp =
+    Btyp_alias of btyp * string
+  | Btyp_arrow of btyp * btyp
+  | Btyp_constr of Path.t * btyp list
+  | Btyp_tuple of btyp list
+  | Btyp_var of bool * string
+  | Btyp_poly of string list * btyp
+  | Btyp_val
+
+(** Translates a type expression [t] into a [btyp]. *)
+
+val btyp_of_typ_exp : Types.type_expr -> btyp
+
+(** Translates of a type scheme [t] into a [btyp], *)
+
+val btyp_of_typ_sch_simple : Types.type_expr -> btyp
+
+(** Return the name of a type variable *) 
+
+val name_of_type : Types.type_expr -> string
+
+(** Function to reset the fresh name generator for type variables *)
+
+val reset_names : unit -> unit
+
+(** Pretty printer for a type *)
+
+val print_out_type : btyp -> string
+
+(** Convert a type into a string *)
+
+val string_of_type_exp : Types.type_expr -> string
+
+(** Convert a type scheme into a string *)
+
+val string_of_type_sch : Types.type_expr list -> Types.type_expr -> string

generator/settings.mli

+
+(** Configure the typechecker to 
+    - not include stdlib 
+    - use the value restriction 
+    - ignore "mli" files that might exist next to "ml" files
+  *)
+
+val configure : unit -> unit