compiles

TODO

@@ -37,6 +37,7 @@ LATER
 
 - support float
 
+- make systematic use of    || (rm -f $@; exit 1)   in cfml calls
 
 DEPRECATED?
 

examples/BasicDemos/Demo.ml

@@ -346,13 +346,7 @@ let order_constr () =
   let r = ref 0 in
   let f () = incr r; 1 in
   let g () = assert (!r = 1); 1 in
-  (g() :: f() :: nil)
-
-let order_array () =
-  let r = ref 0 in
-  let f () = incr r; 1 in
-  let g () = assert (!r = 1); 1 in
-  [| g() ; f() |]
+  (g() :: f() :: [])
 
 let order_list () =
   let r = ref 0 in
@@ -366,12 +360,31 @@ let order_tuple () =
   let g () = assert (!r = 1); 1 in
   (g(), f())
 
+let order_record () : 'a sitems =
+  let r = ref 0 in
+  let g () : 'a list = incr r; [] in
+  let f () = assert (!r = 1); 1 in
+  { nb = f(); items = g() }
+
+(* not yet supported : relaxed value restriction;
+   (below, the call to g() results in a fresh type variable).
+   The work around is to annotate a bit more, as done above;
+   this avoids having a type for [g] that is too general.
+
 let order_record () =
   let r = ref 0 in
   let g () = incr r; [] in
   let f () = assert (!r = 1); 1 in
   { nb = f(); items = g() }
+*)
 
+(* not yet supported : array initializers 
+let order_array () =
+  let r = ref 0 in
+  let f () = incr r; 1 in
+  let g () = assert (!r = 1); 1 in
+  [| g() ; f() |]
+*)
 
 
 (********************************************************************)
@@ -392,7 +405,7 @@ let array_ops () =
 let while_decr () =
    let n = ref 3 in
    let c = ref 0 in
-   while !n > 0 do 
+   while !n > 0 do  
       incr c;
       decr n;
    done;
@@ -425,7 +438,7 @@ let rec rec_partial_half x =
 
 let rec rec_mutual_f x =
   if x <= 0 then x else 1 + rec_mutual_g (x-2)
-and rec rec_mutual g x =
+and rec_mutual_g x =
   rec_mutual_f (x+1)
 
 

examples/Makefile.example

@@ -97,7 +97,7 @@ cf: $(ML)
 	@$(MAKE) -C $(CFML)/lib/tlc --no-print-directory quick
 #	@$(MAKE) -C $(CFML) --no-print-directory tools coqlib_quick_cf 
 	@$(MAKE) -C $(CFML) --no-print-directory tools coqlib_quick 
-	@$(MAKE) -C $(CFML)/lib/stdlib --no-print-directory quick
+#	@$(MAKE) -C $(CFML)/lib/stdlib --no-print-directory quick
 	@$(MAKE) CFML=$(CFML) OCAML_FLAGS=$(OCAML_FLAGS) COQINCLUDE="$(COQINCLUDE)" ML="$(ML)" --no-print-directory -f $(CFML)/lib/make/Makefile.cf all
 
 proof:cf

generator/characteristic.ml

@@ -598,8 +598,8 @@ let rec cfg_exp env e =
    let aux = cfg_exp env in
    let lift e = lift_val env e in
    let ret e = Cf_ret (lift e) in
-   let not_normal () =
-      not_in_normal_form loc (Print_tast.string_of_expression false e) in
+   let not_normal ?s:(s="") () =
+      not_in_normal_form loc (s ^ Print_tast.string_of_expression false e) in
    match e.exp_desc with
    | Texp_ident (x,d) -> ret e
    | Texp_open (p, {exp_desc = Texp_ident _}) -> assert false
@@ -624,8 +624,7 @@ let rec cfg_exp env e =
 
    | Texp_apply (funct, oargs) when exp_is_inlined_primitive funct oargs -> ret e
 
-   | Texp_function (_, pat_expr_list, partial) -> assert false; (*not_normal ()   todo:better message*)
-       
+   | Texp_function (_, pat_expr_list, partial) -> not_normal ~s:"The function involved has not been lifted properly during normalization;\n check the normalized file in _output folder.\n" ()
 
    | Texp_let(rf, fvs, pat_expr_list, body) ->
       
@@ -687,8 +686,9 @@ let rec cfg_exp env e =
         end else begin
             
            if fvs_strict <> [] || fvs_others <> [] 
-               then not_in_normal_form loc ("(unsatisfied value restriction) "
-                                        ^ (Print_tast.string_of_expression false e));
+               then unsupported loc "relaxed value restriction";
+               (* not_in_normal_form loc ("(un value restriction) "
+                                        ^ (Print_tast.string_of_expression false e));*)
            let cf1 = cfg_exp env bod in
            let env' = Ident.add (pattern_ident pat) (List.length fvs_strict) env in
            let cf2 = cfg_exp env' body in

generator/normalize.ml

@@ -267,15 +267,16 @@ let normalize_expression named e =
              let e1',b1 = aux true e1 in
              let e' = create_let loc b1 (
                       create_let loc [normalize_pattern p1, e1'] (
-                       protect named e2)) in
+                       protect false e2)) in
              assign_var e' []
          | _ ->  
              let e1',b1 = aux false e1 in
              let e' = create_let loc b1 (
-                      create_match_one loc e1' (normalize_pattern p1) (protect named e2)) in
+                      create_match_one loc e1' (normalize_pattern p1) (protect false e2)) in
              assign_var e' []
          end
-      | Pexp_let (rf, l, e) -> 
+      | Pexp_let (rf, l, e) -> unsupported loc "non-recursive let-and construct"
+          (* DEPRECATED --seems   buggous
           let check_is_named_pat p =
              match p.ppat_desc with
              | Ppat_var x 
@@ -285,6 +286,7 @@ let normalize_expression named e =
           if not (List.for_all check_is_named_pat (List.map fst l))
              then unsupported loc "let-rec with patterns not reduced to names";
           aux true (List.fold_right (fun (pi,ei) eacc -> create_let loc [pi,ei] eacc) l e)
+          *)
       | Pexp_function (lab, None, [_]) -> 
           let rec protect_func (ms : (expression * pattern) list) (e : expression) = 
              match e.pexp_desc with 
@@ -327,7 +329,10 @@ let normalize_expression named e =
       | Pexp_apply (e0, [(l1,e1); (l2,e2)]) when is_lazy_binary_op e0 ->
          (* TODO: assert that the labels are irrelevant here *)
          let e0',b0 = aux false e0 in
-         let name = match e0.pexp_desc with Pexp_ident f -> name_of_lident f in
+         let name = match e0.pexp_desc with
+            | Pexp_ident f -> name_of_lident f 
+            | _ -> assert false (* could not be a lazy op otherwise *) 
+            in
          assert (b0 = []); (* since e0 should be "&&" or "||" *)
          let e1',b1 = aux false e1 in
          let e2',b2 = aux false e2 in
@@ -424,7 +429,7 @@ let normalize_expression named e =
           let e1', b = aux true e1 in
           let tunit = Some { ptyp_desc = Ptyp_constr (Lident "unit", []); ptyp_loc = loc } in
           let e1'' = return (Pexp_constraint (e1', tunit, None)) in
-          assign_var (return (Pexp_sequence (e1'', protect named e2))) b     
+          assign_var (return (Pexp_sequence (e1'', protect false e2))) b     
       | Pexp_while (e1,e2) -> 
          assign_var (return (Pexp_while (protect named e1, protect named e2))) []      
       | Pexp_for (s,e1,e2,d,e3) -> 

generator/print_past.ml

@@ -12,7 +12,11 @@ open Format
 (* ** Printing of base values *)
 
 let parent_if_infix s =
-   if Renaming.is_infix_name s then sprintf "(%s)" s else s
+   if Renaming.is_infix_name s then begin
+      if s.[0] = '*' || s.[String.length s - 1] = '*'
+         then sprintf "( %s )" s 
+         else sprintf "(%s)" s 
+   end else s
 
 let string_of_ident s = 
    parent_if_infix (Ident.name s)

lib/make/Makefile.cf

@@ -129,7 +129,7 @@ endif
 # Only the %.cmj target is known to "make".
 
 %.cmj: %.ml $(CFML_MLV)
-	$(CFML_MLV) $(OCAML_FLAGS) -nostdlib -I $(CFML)/lib/stdlib -I . $<
+	$(CFML_MLV) $(OCAML_FLAGS) -nostdlib -I $(CFML)/lib/stdlib -I . $< || (rm -f $@; exit 1)
 
 
 # We use Coq to produce a .vio file out of a .v file.