progress_gen

examples/BasicDemos/Demo.ml

@@ -33,6 +33,16 @@ let top_fun_poly_pair_homogeneous (x:'a) (y:'a) =
   (x,y)
 
 
+(********************************************************************)
+(* ** Infix functions *)
+
+let (+++) x y = x + y  
+
+let infix_aux x y = x + y
+
+let (---) = infix_aux
+
+
 (********************************************************************)
 (* ** Return *)
 

generator/characteristic.ml

@@ -42,12 +42,32 @@ let external_modules_reset () =
    external_modules := []
 
 
+(*#########################################################################*)
+(* ** Idenntifier name renaming conventions *)
+
+(** Convention for naming record types *)
+
+let record_type_name name =
+  name ^ "_record_"
+
+(** Convention for naming record constructors *)
+
+let record_constructor name =
+  name ^ "_record_of_"
+
+(** Convention for naming module names*)
+
+let module_name name =
+   name ^ "_ml"
+
+
 (*#########################################################################*)
 (* ** Lifting of paths *)
 
+
 let lift_ident_name id =
    let name = Ident.name id in
-   let coqname = name ^ "_ml" in
+   let coqname = module_name name in
    if Ident.persistent id then external_modules_add coqname;
    coqname
 
@@ -60,7 +80,7 @@ let lift_ident_name id =
 
 let rec lift_full_path = function
   | Pident id -> Pident (Ident.create (lift_ident_name id))
-  | Pdot(p, s, pos) -> Pdot(lift_full_path p, "ML" ^ s, pos) 
+  | Pdot(p, s, pos) -> Pdot(lift_full_path p, (module_name s), pos) 
   | Papply(p1, p2) -> assert false 
 
 let lift_path = function
@@ -81,16 +101,6 @@ let lift_full_path_name p =
 let lift_path_name p =
   Path.name (lift_path p)
 
-(** Convention for naming record types *)
-
-let record_type_name name =
-  "_" ^ name
-
-(** Convention for naming record constructors *)
-
-let record_constructor name =
-  "_" ^ name ^ "_of"
-
 
 (*#########################################################################*)
 (* ** Lifting of types *)
@@ -346,7 +356,10 @@ let exp_find_inlined_primitive e oargs =
         when m > 0 && let x = Path.name f in x = "Pervasives.mod" || x = "Pervasives./" -> 
         find_inlined_primitive (Path.name f) primitive_special
     | Texp_ident (f,d), _ -> 
-        find_inlined_primitive (Path.name f) (List.length args)
+        let r = find_inlined_primitive (Path.name f) (List.length args) in
+        (* debug: Printf.printf "exp_find_inlined_primitive: %s %d\n"  (Path.name f)  (List.length args);
+        if r = None then Printf.printf "failed\n"; *)
+        r
     | _ -> None
 
 let exp_is_inlined_primitive e oargs =
@@ -495,6 +508,47 @@ let rec pattern_ident p =
 let pattern_name p =
    Ident.name (pattern_ident p)
 
+(** Auxiliary function for encoding infix function names *)
+
+let infix_name_symbols =
+  ['!', 'a';
+   '$', 'b';
+   '%', 'c';
+   '&', 'd';
+   '*', 'e';
+   '+', 'f';
+   '-', 'g';
+   '.', 'h';
+   '/', 'i';
+   ':', 'j';
+   '<', 'k';
+   '=', 'l';
+   '>', 'm';
+   '?', 'n';
+   '@', 'o';
+   '^', 'p';
+   '|', 'q';
+   '~', 'r']
+
+let infix_name_encode name =
+  let gen = String.map (fun c ->
+     try List.assoc c infix_name_symbols
+     with Not_found -> failwith ("infix_name_encode: cannot encode name: " ^ name))
+    name in
+  "infix_" ^ gen ^ "_"
+
+(** Takes a function name and encodes its name in case of an infix operator *)
+
+let pattern_name_protect_infix p =
+   let name = pattern_name p in
+   let n = String.length name in
+   let r = if n > 0 && List.mem_assoc name.[0] infix_name_symbols
+      then infix_name_encode name 
+      else name in
+   (* debug: Printf.printf "protect %s as %s\n" name r;*)
+   r
+
+
 (** An alternative version of function extract_label_names, for obtaining record labels *)
 
 let rec extract_label_names_simple env ty =
@@ -567,7 +621,7 @@ let rec cfg_exp env e =
               List.fold_left (fun (pat,bod) acc -> Ident.add (pattern_ident pat) 0 acc) env pat_expr_list *)
            | Default -> unsupported "Default recursion mode"
            in
-        let ncs = List.map (fun (pat,bod) -> (pattern_name pat, cfg_func env' fvs pat bod)) pat_expr_list in
+        let ncs = List.map (fun (pat,bod) -> (pattern_name_protect_infix pat, cfg_func env' fvs pat bod)) pat_expr_list in
         let cf_body = cfg_exp env' body in 
         add_used_label (fst (List.hd ncs));
         Cf_letfunc (ncs, cf_body)
@@ -577,8 +631,7 @@ let rec cfg_exp env e =
       end else begin 
         if (List.length pat_expr_list <> 1) then not_normal();
         let (pat,bod) = List.hd pat_expr_list in
-        let x = pattern_name pat in
-           (* todo: une diffrence entre pattern_name et pattern_ident utils plus bas? *)
+        let x = pattern_name_protect_infix pat in
         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
@@ -714,7 +767,7 @@ and cfg_func env fvs pat bod =
          get_typed_args ((pattern_name p1, coq_typ_pat p1)::acc) e1
       | _ -> List.rev acc, e
       in  
-   let f = pattern_name pat in
+   let f = pattern_name_protect_infix pat in
    let targs, body = get_typed_args [] bod in
    let typ = coq_typ body in
    let cf_body = cfg_exp env body in
@@ -762,7 +815,7 @@ let rec cfg_structure_item s : cftops =
               List.fold_left (fun (pat,bod) acc -> Ident.add (pattern_ident pat) 0 acc) env pat_expr_list *)
            | Default -> unsupported "Default recursion mode"
            in
-        let ncs = List.map (fun (pat,bod) -> (pattern_name pat, cfg_func env' fvs pat bod)) pat_expr_list in
+        let ncs = List.map (fun (pat,bod) -> (pattern_name_protect_infix pat, cfg_func env' fvs pat bod)) pat_expr_list in
           (List.map (fun (name,_) -> Cftop_val (name, val_type)) ncs)
         @ (List.map (fun (name,cf_body) -> Cftop_fun_cf (name, cf_body)) ncs)
         @ [Cftop_coqs (List.map (fun (name,_) -> register_cf name) ncs)]
@@ -770,7 +823,7 @@ let rec cfg_structure_item s : cftops =
       (* let-binding of a single value *)
       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
+        let x = pattern_name_protect_infix pat in
         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
@@ -844,7 +897,7 @@ let rec cfg_structure_item s : cftops =
       [ Cftop_coqs [ Coqtop_require_import (lift_full_path_name path) ] ]
 
   | Tstr_primitive(id, descr) ->
-      let id = lift_ident_name id in
+      let id = Ident.name id in
       let fvs, typ = lift_typ_sch descr.val_desc.ctyp_type in
       let typ = coq_fun_types fvs typ in
       [ Cftop_val (id, typ) ]
@@ -1171,7 +1224,8 @@ and cfg_type_decls (decls : (Ident.t * Typedtree.type_declaration) list) =
 and cfg_structure s =
    reset_used_labels();
    let body = list_concat_map (fun si -> reset_names(); cfg_structure_item si) s.str_items in
-   cfg_extract_labels() @ body
+   (* cfg_extract_labels() @ *)
+   body
 
 (** Generate the top-level Coq declarations associated with 
     a Caml signature definition. *)

generator/main.ml

@@ -75,7 +75,7 @@ let _ =
      | Some f ->
          f
    in
-   let debugdir = Filename.concat dirname "output" in
+   let debugdir = Filename.concat dirname "_output" in
    let debugdirBase = Filename.concat debugdir (String.capitalize basename) in
    (*  FAILURE ON WINDOWS   *)
    let cmd = Printf.sprintf "mkdir -p %s" debugdir in
@@ -108,11 +108,14 @@ let _ =
       | None -> failwith "Could not typecheck the normalized source code\nCheck out the file output/_normalized.ml." 
       | Some typedtree2 -> typedtree2
       in
-   file_put_contents (debugdirBase ^ "_normalized_typed.ml") (Print_tast.string_of_structure typedtree2); 
-   ignore (typedtree2);
+ 
+   (*---------------------------------------------------*)
+   trace "5) dumping .cmj file";
+   file_put_contents (debugdirBase ^ "_normalized_typed.ml") (Print_tast.string_of_structure typedtree2);
+   (* ignore (typedtree2); *)
 
    if !onlycmj then begin
-      trace "5) exiting after cmj has been generated";
+      trace "6) exiting since -onlycmj";
       exit 0;
    end;
 
@@ -126,13 +129,16 @@ let _ =
    let coqtops = Formula.coqtops_of_cftops cftops in
 
    (*---------------------------------------------------*)
-   trace "7) printing coq ast";
+   trace "7) dumping debug formula file";
    let result = Print_coq.tops coqtops in
    file_put_contents (debugdirBase ^ "_formulae.v") result; 
+
+   (*---------------------------------------------------*)
+   trace "8) dumping .v file";
    file_put_contents outputfile result; 
 
    (*---------------------------------------------------*)
-   trace "8) characteristic formulae successfully generated\n"
+   trace "9) characteristic formulae successfully generated\n"
 
 
 (*########################################################

generator/primitives.ml

@@ -152,6 +152,7 @@ let builtin_constructors_table =
 (** Find the inlined primitive associated with [p] of arity [arity] *)
 
 let find_inlined_primitive p arity =
+   Printf.printf "find_inlined_primitive: %s %d\n" p arity;
    match list_assoc_option p inlined_primitives_table with
    | None -> None
    | Some (n,y) -> if n = arity then Some y else None

lib/make/Makefile.cf

@@ -151,7 +151,7 @@ include $(CFML)/lib/make/Makefile.coq
 
 clean::
 	rm -f *.cmj *_ml.v *.vio *.d *.v.d *.vo *.vq *.aux .*.aux *.glob
-	rm -rf output
+	rm -rf _output
 
 
 # ==> TODO: rename output into _output

examples/Stdlib/Array.ml → stdlib/Array.ml

 
-let make = Primitives.array_make
 
-let length = Primitives.array_length
+(* Temporary: because [||] is not supported. *)
+
+external make_empty : unit -> 'a array = "%array_make_empty"
+
+external make : int -> 'a -> 'a array = "%array_make"
+
+external length : 'a array -> int = "%array_length"
+
+external get : 'a array -> int -> 'a = "%array_get"
+
+external set : 'a array -> int -> 'a -> unit = "%array_set"
 
-let get = Primitives.array_get
 
-let set = Primitives.array_set
 
 let init n f =
   assert (n >= 0);
-  if n = 0 then [||] else begin
-    let res = create n (f 0) in
+  if n = 0 then make_empty() else begin
+    let res = make n (f 0) in
     for i = 1 to pred n do
-      unsafe_set res i (f i)
+      set res i (f i)
     done;
     res
   end
@@ -21,47 +28,48 @@ let init n f =
 let fill a start nb v =
   assert (not (start < 0 || nb < 0 || start > length a - nb));
   for i = start to pred (start + nb) do 
-    a.(i) <- v;
+    set a i v;
   done
 
 let blit a1 start1 a2 start2 nb =
   assert (not (nb < 0 || start1 < 0 || start1 > length a1 - nb
                       || start2 < 0 || start2 > length a2 - nb));
   for i = 0 to pred nb do
-    a2.(start2 + i) <- a1.(start1 + i);
+    set a2 (start2 + i) (get a1 (start1 + i));
   done
 
 let append a1 a2 =
   let n1 = length a1 in
   let n2 = length a2 in
-  if n1 = 0 && n2 = 0 then [||] else begin
-     let d = (if n1 <> 0 then a1.(0) else a2.(0)) in
+  if n1 = 0 && n2 = 0 then make_empty() else begin
+     let d = (if n1 <> 0 then get a1 0 else get a2 0) in
      let a = make (n1+n2) d in
      for i = 0 to pred n1 do
-        a.(i) <- a1.(i);
+        set a i (get a1 i);
      done;
      for i = 0 to pred n2 do
-        a.(n1+i) <- a2.(i)
+        set a (n1+i) (get a2 i);
      done;
+     a
    end
   (* Remark: might be optimized by using a sub-array to avoid initialization *)
 
 let iter f a =
   for i = 0 to pred (length a) do 
-    f a.(i)
+    f (get a i)
   done
 
 let iteri f a =
   for i = 0 to pred (length a) do 
-    f i a.(i)
+    f i (get a i)
   done
 
 let map f a =
   let n = length a in
-  if n = 0 then [||] else begin
-    let r = make n (f a.(0)) in
+  if n = 0 then make_empty() else begin
+    let r = make n (f (get a 0)) in
     for i = 1 to pred n do
-      r.(i) <- f a.(i);
+      set r i (f (get a i));
     done;
     r
   end
@@ -69,10 +77,10 @@ let map f a =
 
 let mapi f a =
   let n = length a in
-  if n = 0 then [||] else begin
-    let r = make n (f 0 a.(0)) in
+  if n = 0 then make_empty() else begin
+    let r = make n (f 0 (get a 0)) in
     for i = 1 to pred n do
-      r.(i) <- f i a.(i);
+      set r i (f i (get a i));
     done;
     r
   end
@@ -81,13 +89,17 @@ let mapi f a =
 let fold_left f x a =
   let r = ref x in
   for i = 0 to pred (length a) do
-    r := f !r a.(i)
+    r := f !r (get a i)
   done;
   !r
 
+(* TODO: add support for downto in CFML 
 let fold_right f a x =
   let r = ref x in
   for i = pred (length a) downto 0 do
-    r := f a.(i) !r
+    r := f (get a i) !r
   done;
   !r
+  
+  *)
+

examples/Stdlib/List.ml → stdlib/List.ml

@@ -15,7 +15,7 @@ let tl = function
 let length l = 
    let rec aux len = function
      | [] -> len
-     | a::l -> length_aux (len + 1) l
+     | a::l -> aux (len + 1) l
      in
   aux 0 l
 
@@ -48,7 +48,7 @@ let rev l =
 
 let rec concat = function
   | [] -> []
-  | l::r -> l @ flatten r
+  | l::r -> l @ concat r
 
 
 let rec iter f = function
@@ -76,7 +76,7 @@ let mapi f l =
         let r = f i a in
         r :: aux (i + 1) l
    in
-   mapi 0 f l
+   aux 0 l
 
 (* USEFUL?
 let rev_map f l =
@@ -115,7 +115,7 @@ let rec find p = function
 let filter p l =
   let rec aux acc = function
      | [] -> rev acc
-     | a::l -> if p a then aux (a::acc) l else find acc l
+     | a::l -> if p a then aux (a::acc) l else aux acc l
      in
   aux [] l
 
@@ -148,7 +148,7 @@ let take n l =
      if n = 0 then [] else begin
         match l with
         | [] -> assert false
-        | a::l -> a::(aux (n-1) l) in
+        | a::l -> a::(aux (n-1) l) 
      end
      in
   aux n l
@@ -159,7 +159,7 @@ let drop n l =
      if n = 0 then l else begin
         match l with
         | [] -> assert false
-        | a::l -> aux (n-1) l in
+        | a::l -> aux (n-1) l 
      end
      in
   aux n l

stdlib/Makefile

+
+
+
+
+##############################################################
+# Parameters
+
+READLINK = $(shell if hash greadlink 2>/dev/null ; then echo greadlink ; else echo readlink ; fi)
+
+# Path to CFML relative to immediate subfolders of $(CFML)/examples.
+CFML := ..
+
+# Absolute path to CFML.
+CFML := $(shell $(READLINK) -f $(CFML))
+
+# Include any local settings.
+-include $(CFML)/settings.sh
+
+
+ifeq ($(findstring $(MAKECMDGOALS),clean),)
+   include $(CFML)/lib/make/Makefile.tools
+endif
+
+ifndef COQINCLUDE
+	COQINCLUDE := -R $(CFML)/lib/coq/ CFML -R $(CFML)/lib/tlc/ TLC -R . EXAMPLE
+endif
+
+ifndef OCAML_FLAGS
+	OCAML_FLAGS := 
+	# e.g. -rectypes
+endif
+
+COQC      := $(COQBIN)coqc
+
+
+
+# TODO :needed?
+# OCAMLDEP  := $(OCAMLBIN)ocamldep
+# OCAMLPOST := $(CFML)/lib/make/ocamldep.post
+
+
+##############################################################
+# Files
+
+# ML := $(filter-out myocamlbuild.ml,$(shell ls *.ml))
+
+ML := $(shell ls *.ml)
+CMJ   := $(patsubst %.ml,%.cmj,$(ML))
+MLV   := $(patsubst %.ml,%_ml.v,$(ML))
+MLVIO := $(patsubst %.ml,%_ml.vio,$(ML))
+MLVO := $(patsubst %.ml,%_ml.vo,$(ML))
+D     := $(patsubst %.ml,%.d,$(ML))
+
+
+##############################################################
+# Targets
+
+all: cmj vo
+
+quick: cmj vio
+
+cmj: $(CMJ) 
+vo: $(MLVO)
+vio: $(MLVIO) 
+
+tools:
+	@$(MAKE) -C $(CFML) --no-print-directory tools
+
+
+##############################################################
+# CMJ/MLV generation rules
+
+# TODO: use per-file flags hack
+
+Pervasives.cmj: Pervasives.ml $(CFML_MLV) 
+# Make sure CFML tools are up-to-date.
+# Needed only when developing CFML. Ideally, should be removed.
+	@$(MAKE) -C $(CFML) --no-print-directory tools
+	$(CFML_MLV) $(OCAML_FLAGS) -nostdlib -nopervasives -I . $< || (rm -f $@; exit 1)
+
+# note: we need to delete the cmj file if mlv has failed
+
+%.cmj: %.ml Pervasives.cmj $(CFML_MLV)
+# Needed only when developing CFML. Ideally, should be removed.
+	@$(MAKE) -C $(CFML) --no-print-directory tools
+	$(CFML_MLV) $(OCAML_FLAGS) -nostdlib -I . $< || (rm -f $@; exit 1)
+
+
+##############################################################
+# Coq compilation rules
+
+# We use Coq to produce a .vio file out of a .v file.
+# We declare a dependency on the .cmj file, since %_ml.v is not known to "make".
+	
+Array_ml.vo List_ml.vo: Pervasives_ml.vo
+Array_ml.vio List_ml.vio: Pervasives_ml.vio
+
+%_ml.vo: %.cmj
+	$(COQC) $(COQINCLUDE) $*_ml.v
+
+%_ml.vio: %.cmj
+	$(COQC) -quick $(COQINCLUDE) $*_ml.v
+
+
+# V := $(MLV)
+# include $(CFML)/lib/make/Makefile.coq
+
+
+##############################################################
+# Cleanup
+
+# Do not delete intermediate files.
+.SECONDARY:
+.PRECIOUS: *.vio
+
+clean::
+	@make CFML=$(CFML) -f $(CFML)/lib/make/Makefile.cf clean
+
+
+

examples/Stdlib/Pervasives.ml → stdlib/Pervasives.ml

 
 
+
+(************************************************************)
+(** Exception *)
+
+external raise : exn -> 'a = "%raise"
+
+
 (************************************************************)
 (** Type conversion *)
 
 external magic : 'a -> 'b = "%magic"
 
 
+
+(************************************************************)
+(** Boolean *)
+
+let not x = 
+  if x then false else true
+
+
+
 (************************************************************)
 (** Physical equality *)
 
@@ -22,12 +38,12 @@ let ( !== ) = physical_neq
 (************************************************************)
 (** Comparison *)
 
-let compare_eq : 'a -> 'a -> bool = "%compare_eq"
-let compare_neq : 'a -> 'a -> bool = "%compare_neq"
-let compare_lt : 'a -> 'a -> bool = "%compare_lt"
-let compare_gt : 'a -> 'a -> bool = "%compare_gt"
-let compare_le : 'a -> 'a -> bool = "%compare_le"
-let compare_ge : 'a -> 'a -> bool = "%compare_ge"
+external compare_eq : 'a -> 'a -> bool = "%compare_eq"
+external compare_neq : 'a -> 'a -> bool = "%compare_neq"
+external compare_lt : 'a -> 'a -> bool = "%compare_lt"
+external compare_gt : 'a -> 'a -> bool = "%compare_gt"
+external compare_le : 'a -> 'a -> bool = "%compare_le"
+external compare_ge : 'a -> 'a -> bool = "%compare_ge"
 
 let ( = ) = compare_eq
 let ( <> ) = compare_neq
@@ -53,6 +69,34 @@ let ( && ) = bool_and
 let ( || ) = bool_or
 
 
+
+(************************************************************)
+(** Integer *)
+
+external int_neg : int -> int = "%int_neg"
+external int_add : int -> int -> int = "%int_add"
+external int_sub : int -> int -> int = "%int_sub"
+external int_mul : int -> int -> int = "%int_mul"
+external int_div : int -> int -> int = "%int_div"
+external int_mod : int -> int -> int = "%int_mod"
+
+let ( ~- ) = int_neg
+let ( + ) = int_add
+let ( - ) = int_sub
+let ( * ) = int_mul
+let ( / ) = int_div
+let ( mod ) = int_mod
+
+let succ n =
+  n + 1
+
+let pred n =
+  n - 1
+
+let abs x = 
+  if x >= 0 then x else -x
+
+
 (************************************************************)
 (** References *)
 
@@ -84,44 +128,10 @@ let ref_free r =
   ()
 
 (** [ref_unsafe_set r x] allows to modifies the contents of a reference *)
-
+(* unsupported currently, needs explicit types
 let ref_unsafe_set r x =
   r.contents <- (magic x)
-
-
-(************************************************************)
-(** Boolean *)
-
-let not x = 
-  if x then false else true
-
-
-(************************************************************)
-(** Integer *)
-
-external int_neg : int -> int = "%int_neg"
-external int_add : int -> int -> int = "%int_add"
-external int_sub : int -> int -> int = "%int_sub"
-external int_mul : int -> int -> int = "%int_mul"
-external int_div : int -> int -> int = "%int_div"
-external int_mod : int -> int -> int = "%int_mod"
-
-let ( ~- ) = int_neg
-let ( + ) = int_add
-let ( - ) = int_sub
-let ( * ) = int_mul
-let ( / ) = int_div
-let ( mod ) = int_mod
-
-let succ n =
-  n + 1
-
-let pred n =
-  n - 1
-
-let abs x = 
-  if x >= 0 then x else -x
-
+*)