cp

TODO

 
-(* todo: warning if not the right nb of args on xapp *)
 
 
--> corriger  let n = null  qui ne génère pas ce qu'il faut
 
 
-unifier main.ml et makecmj.ml
+LATER
 
-se débarrasser de myocamldep serait agréable
+- unify the source code in main.ml and makecmj.ml
 
-NullPointers et StrongPointers sont spéciaux puisque l'utilisateur
-va devoir lier son code OCaml avec eux; ils ne devraient pas être
-installés avec la lib standard?
+- check that there are no uses of labels in source files
 
+- support float
 
 
+DEPRECATED?
+
+- no longer rely on myocamldep
+
+- incorrect CF generation for "let n = null"
\ No newline at end of file

bin/Old_CFTactics.v

@@ -2674,3 +2674,15 @@ Tactic Notation "xapp_4" constr(args) := xapp_3 args; xapp4.
 Tactic Notation "xapp_4_spec" constr(H) := xapp_spec H; xapp4.
 Tactic Notation "xapp_4_spec" constr(H) constr(args) := xapp_3_spec H args; xapp4.
 *)
+
+
+
+
+    
+    Hint: call [xgc] prior to [xapply] if you also need a
+    step of garbage collection. 
+    // LATER: make [xapply] support the gc rule, and introduce
+    // [xapply_no_gc E] is like [xapply] but does not allow 
+    // for the garbage collection rule to be applied.
+    // In that case, change [xapp_prepare] to not do [xgc];
+    // but check first that introduce evars later is not an issue.

examples/BasicDemos/Demo.ml

@@ -122,10 +122,14 @@ let test_partial_app_arities () =
    let f3 = func4 1 2 3 in
    f1 2 3 4 + f2 3 4 + f3 4
 
-let app_partial_builtin () =
+let app_partial_builtin_add () =
   let f = (+) 1 in
   f 2
 
+let app_partial_builtin_and () =
+  let f = (&&) true in
+  f false
+
 
 (********************************************************************)
 (* ** Over applications *)
@@ -145,6 +149,37 @@ let infix_aux x y = x +++ y
 let (---) = infix_aux
 
 
+(********************************************************************)
+(* ** Lazy binary operators *)
+
+let lazyop_val () =
+  if true && (false || true) then 1 else 0
+
+let lazyop_term () =
+  let f x = (x = 0) in
+  if f 1 || f 0 then 1 else 0
+
+let lazyop_mixed () =
+  let f x = (x = 0) in
+  if true && (f 1 || (f 0 && true)) then 1 else 0
+
+
+(********************************************************************)
+(* ** Comparison operators *)
+
+let compare_int () =
+  (1 <> 0 && 1 <= 2) || (0 = 1 && 1 >= 2 && 1 < 2 && 2 > 1)
+
+let compare_min () =
+  (min 0 1)
+
+(*
+let compare_float () =
+  (1. <> 0. && 1. <= 2.) || (0. = 1. && 1. >= 2. && 1. < 2. && 2. > 1.)
+*)
+
+
+
 (********************************************************************)
 (* ** Inlined total functions *)
 
@@ -157,7 +192,6 @@ let inlined_fun_others n =
 
 
 
-
 (********************************************************************)
 (* ** Polymorphic functions *)
 
@@ -297,6 +331,49 @@ let sitems_push x r =
   r.items <- x :: r.items
 
 
+
+(********************************************************************)
+(* ** Evaluation order *)
+
+let order_app () =
+  let r = ref 0 in
+  let h () = assert (!r = 2); (fun a b -> a + b) in
+  let f () = incr r; 1 in
+  let g () = assert (!r = 1); incr r; 1 in
+  (h()) (g()) (f())
+
+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() |]
+
+let order_list () =
+  let r = ref 0 in
+  let f () = incr r; 1 in
+  let g () = assert (!r = 1); 1 in
+  [ g() ; f() ]
+
+let order_tuple () =
+  let r = ref 0 in
+  let f () = incr r; 1 in
+  let g () = assert (!r = 1); 1 in
+  (g(), f())
+
+let order_record () =
+  let r = ref 0 in
+  let g () = incr r; [] in
+  let f () = assert (!r = 1); 1 in
+  { nb = f(); items = g() }
+
+
+
 (********************************************************************)
 (* ** Arrays *)
 
@@ -346,6 +423,11 @@ let rec rec_partial_half x =
   else if x = 1 then assert false
   else 1 + rec_partial_half(x-2)
 
+let rec rec_mutual_f x =
+  if x <= 0 then x else 1 + rec_mutual_g (x-2)
+and rec rec_mutual g x =
+  rec_mutual_f (x+1)
+
 
 (********************************************************************)
 (* ** External *)

examples/BasicDemos/Demo_proof.v

@@ -10,6 +10,14 @@ Require Import Pervasives_ml. (* optional, improves display of, e.g. [incr] *)
 
 
 
+
+
+
+
+
+
+
+
 Lemma if_true_spec : 
   app if_true [tt] \[] \[= 1].
 Proof using.
@@ -474,6 +482,13 @@ Proof using.
 Qed.
 
 
+let app_partial_builtin_and () =
+  let f = (&&) true in
+  f false
+
+
+
+
 (********************************************************************)
 (* ** Over applications *)
 
@@ -717,14 +732,73 @@ Qed.
 
 
 
-
+let rec rec_mutual_f x =
+  if x <= 0 then x else 1 + rec_mutual_g (x-2)
+and rec rec_mutual g x =
+  rec_mutual_f (x+1)
 *)
 
 
+(********************************************************************)
+(* ** Lazy binary operators 
+
+let lazyop_val () =
+  if true && (false || true) then 1 else 0
+
+let lazyop_term () =
+  let f x = (x = 0) in
+  if f 1 || f 0 then 1 else 0
+
+let lazyop_mixed () =
+  let f x = (x = 0) in
+  if true && (f 1 || (f 0 && true)) then 1 else 0
+
+*)
+
 
 (* TODO: include demo of  xpost (fun r =>\[r = 3]). *)
 
 
+(********************************************************************)
+(* ** Evaluation order 
+
+let order_app () =
+  let r = ref 0 in
+  let f () = incr r; 1 in
+  let g () = assert (!r = 1); 1 in
+  g() + f()
+
+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() |]
+
+let order_list () =
+  let r = ref 0 in
+  let f () = incr r; 1 in
+  let g () = assert (!r = 1); 1 in
+  [ g() ; f() ]
+
+let order_tuple () =
+  let r = ref 0 in
+  let f () = incr r; 1 in
+  let g () = assert (!r = 1); 1 in
+  (g(), f())
+
+let order_record () =
+  let r = ref 0 in
+  let g () = incr r; [] in
+  let f () = assert (!r = 1); 1 in
+  { nb = f(); items = g() }
+*)
+
 
 
 (*************************************************************************)
@@ -780,6 +854,3 @@ Proof using. intros. xcf. xval as p Hp. subst p. xrets. auto. Qed.
 
 
 
-
-
-

generator/characteristic.ml

@@ -12,10 +12,6 @@ open Path
 open Renaming
 open Printf
 
-(*#########################################################################*)
-(* ** Switch for generating formulae for purely-functional programs *)
-
-let use_credits = ref false
 
 
 (*#########################################################################*)
@@ -351,7 +347,7 @@ let exp_find_inlined_primitive e oargs =
     match e.exp_desc, args with 
     | Texp_ident (f,d), [n; {exp_desc = Texp_constant (Const_int m)}] 
         when m <> 0 && let x = Path.name f in x = "Pervasives.mod" || x = "Pervasives./" -> 
-        find_inlined_primitive (Path.name f) primitive_special
+        find_inlined_primitive (Path.name f) Primitive_binary_only_non_zero_second_arg
     | Texp_ident (f,d), _ -> 
         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);
@@ -737,7 +733,7 @@ and cfg_func env fvs pat bod =
    let targs, body = get_typed_args [] bod in
    let typ = coq_typ body in
    let cf_body = cfg_exp env body in
-   let cf_body = if !use_credits then Cf_pay cf_body else cf_body in
+   let cf_body = if !Mytools.use_credits then Cf_pay cf_body else cf_body in
    let fvs = List.map name_of_type fvs in
    Cf_body (f, fvs, targs, typ, cf_body) 
    (* --todo: check if the set of type variables quantified is not too

generator/characteristic.mli

-val use_credits : bool ref
-
 (*
 val external_modules : string list ref
 val external_modules_add : string -> unit

generator/main.ml

@@ -29,7 +29,8 @@ let spec =
     ("-I", Arg.String (fun i -> Clflags.include_dirs := i::!Clflags.include_dirs), 
                       " includes a directory where to look for interface files");
     ("-rectypes", Arg.Set Clflags.recursive_types, " activates recursive types");
-    ("-credits", Arg.Set Characteristic.use_credits, " generate 'pay' instructions");
+    ("-left2right", Arg.Set Mytools.use_left_to_right_order, " use the left-to-right evaluation order for sub-expressions, instead of OCaml order");
+    ("-credits", Arg.Set Mytools.use_credits, " generate 'pay' instructions");
     ("-nostdlib", Arg.Set no_mystd_include, " do not include standard library");
     ("-nopervasives", Arg.Set Clflags.nopervasives, " do not include standard pervasives file");
     ("-o", Arg.String (fun s -> outputfile := Some s), " set the output file name");
@@ -38,6 +39,8 @@ let spec =
     ("-width", Arg.Set_int Print_coq.width, " set pretty-printing width for the .v file");
   ]
 
+
+
 let _ =
    Settings.configure();
 
@@ -65,6 +68,12 @@ let _ =
    if List.length !files <> 1 then
       failwith "Expects one argument: the filename of the ML source file";
    let sourcefile = List.hd !files in
+   if !Clflags.nopervasives && sourcefile <> "Pervasives.ml" then
+      failwith "Option -nopervasives may only be used to compile file Pervasives";
+      (* this defensive check is needed for the correctness of normalization 
+         of special operators such as "mod" or "&&"; 
+         see also function [add_pervasives_prefix_if_needed] *)
+
    if not (Filename.check_suffix sourcefile ".ml") then
      failwith "The file name must be of the form *.ml";
    let basename = Filename.chop_suffix (Filename.basename sourcefile) ".ml" in

generator/mytools.ml

 
 
+(*#########################################################################*)
+(* ** Switch for controlling generation *)
+
+let use_credits = ref false
+
+let use_left_to_right_order = ref false
+
+
+
+
+
+
+(*#########################################################################*)
+
 (**************************************************************)
 (** Option manipulation functions *)
 

generator/mytools.mli

-(** This file contains some helper functions.
-    Ideally, many of these functions would come from a standard,
-    extensive Coq library. *)
+
+(**************************************************************)
+(** Parameters to control the normalization and generation *)
+
+val use_credits : bool ref
+
+val use_left_to_right_order : bool ref
+
+
+
+
+
+(**************************************************************)
+(**************************************************************)
+
+(** The rest of this file contains some helper functions. *)
 
 (**************************************************************)
 (** Option manipulation functions *)

generator/normalize.ml

@@ -27,23 +27,63 @@ let check_lident loc idt =
    check_var loc (name_of_lident idt)
 
 
+(*#########################################################################*)
+(* ** Control of evaluation order *)
+
+let reverse_if_right_to_left_order args =
+  if !Mytools.use_left_to_right_order then args else List.rev args
+
+
+
 (*#########################################################################*)
 (* ** Detection of primitive functions and exception-raising *)
 
-let is_inlined_primitive e largs =
+(** Obtain a full path for a variable expected to be bound only in Pervasives *)
+let get_qualified_pervasives_name lident = 
+   let name = name_of_lident lident in
+   if !Clflags.nopervasives 
+      then name  (* unqualified name when from inside Pervasives *)
+      else "Pervasives." ^ name  (* qualified name otherwise *)
+
+
+let exp_is_inlined_primitive e largs =
     let args = List.map snd largs in (* todo: check no labels*)
     match e.pexp_desc, args with 
+
     | Pexp_ident f, [n; {pexp_desc = Pexp_constant (Const_int m)}]  
-        (* URGENT: 
-          we could maybe reject programs that rebind these operators,
-          else it seems we need to have the typed tree in order to normalize...
-           -- TODO check that mod and "/" are actually coming from pervasives *)
-        when m <> 0 && let x = name_of_lident f in x = "mod" || x = "/" -> 
-        is_inlined_primitive ("Pervasives." ^ fullname_of_lident f) primitive_special
+        (* Remark: we impose elsewhere a check that the names "mod" and "/"
+           and "&&" and "||" are not bound outside of Pervasives *)
+          when m <> 0 && let x = name_of_lident f in List.mem x ["mod"; "/"] ->
+        let name = get_qualified_pervasives_name f in
+        begin match find_inlined_primitive name with
+        | Some (Primitive_binary_only_non_zero_second_arg, coq_name) -> true
+        | _ -> false
+       end
+
+    | Pexp_ident f, [e1; e2] 
+       when let x = name_of_lident f in List.mem x ["&&"; "||"] -> true
+       (* Remark: this check is not complete; it is only useful to ensure 
+          that values_variables won't fail *)
+
+    | Pexp_ident f, [e1; e2] 
+       when let x = name_of_lident f in List.mem x ["="; "<>"; "<="; ">="; "<"; ">"] ->  true
+       (* Remark: here we don't check that the types of the arguments are numbers;
+          we will catch this later in the characteristic formula generation *)
+
     | Pexp_ident f,_ -> 
-        is_inlined_primitive ("Pervasives." ^ fullname_of_lident f) (List.length args)
+        let arity = List.length args in
+        begin match find_inlined_primitive ("Pervasives." ^ fullname_of_lident f) with
+        | Some (Primitive_unary, coq_name) when arity = 1 -> true
+        | Some (Primitive_binary, coq_name) when arity = 2 -> true
+        (* remark: this case should have been caught earlier by [is_lazy_binary_op], so:
+           | Some (Primitive_binary_lazy, coq_name) when arity = 2 -> assert false
+        *)
+        | _ -> false
+        end
+
     | _ -> false
 
+
 let is_failwith_function e =
    match e.pexp_desc with
    | Pexp_ident li ->
@@ -54,6 +94,13 @@ let is_failwith_function e =
       end
    | _ -> false
 
+let is_lazy_binary_op e = 
+   match e.pexp_desc with 
+   | Pexp_ident f 
+     when let x = name_of_lident f in x = "&&" || x = "||" -> true
+   | _ -> false 
+
+
 
 (*#########################################################################*)
 (* ** Normalization of patterns *)
@@ -110,7 +157,7 @@ let rec values_variables e =
    | Pexp_ident (Lident x) -> [x]
    | Pexp_ident li -> []
    | Pexp_constant c -> []
-   | Pexp_apply (e0, l) when is_inlined_primitive e0 l -> 
+   | Pexp_apply (e0, l) when exp_is_inlined_primitive e0 l -> 
       list_concat_map aux (List.map snd l)
    | Pexp_tuple l -> 
       list_concat_map aux l
@@ -160,7 +207,11 @@ let get_assign_fct loc already_named new_name : expression -> bindings -> expres
               let e' = { pexp_loc = Location.none; pexp_desc = Pexp_ident (Lident x) } in
               e', b @ [ p, e ]
 
-(* -- todo: check evaluation order for tuples and records *)
+(* argument [named] indicates whether the context in which appear
+   is already a [let x = ... in ..]. This is useful to know whether
+   it is needed to introduce a fresh name in case the expression [e]
+   is of the form [fun .. -> ..]. *)
+
 let normalize_expression named e =
    let i = ref (-1) in (* TODO: use a gensym function *)
    let next_var () =
@@ -172,8 +223,19 @@ let normalize_expression named e =
      let loc = e.pexp_loc in
      let return edesc' = 
        { e with pexp_desc = edesc' } in
+     let mk_bool bvalue =
+       let svalue = if bvalue then "true" else "false" in
+       let explicit_arity = false in (* todo: what does it mean? *)
+       return (Pexp_construct (Lident svalue, None, explicit_arity)) in
      let assign_fct pick_var = 
          get_assign_fct loc named pick_var in
+     (* [assign_var e' b] takes a a transformed expression and a list 
+        of bindings; and it returns a transformed expression and a list
+        of bindings. If the parameter [named] is true, then this returns
+        simply [(e',b)]. Otherwise, it returns a pair [(var x, b')],
+        where [b'] extends [b] with the binding from [x] to [e']. 
+        This function should be called any time the translation 
+        produces a term that may not be a value. *)       
      let assign_var = 
          assign_fct next_var in      
      match e.pexp_desc with
@@ -249,12 +311,36 @@ let normalize_expression named e =
          unsupported "function with optional expression"
       | Pexp_apply (e0, l) when is_failwith_function e0 -> 
          return Pexp_assertfalse, []
+      | Pexp_apply (e0, [e1; e2]) when is_lazy_binary_op e0 ->
+         let e0',b0 = aux false e0 in
+         let name = match e0.pexp_desc with Pexp_ident f -> name_of_lident f in
+         assert (b0 = []); (* since e0 should be "&&" or "||" *)
+         let e1',b1 = aux false e1 in
+         let e2',b2 = aux false e2 in
+         if b2 = [] then begin 
+            let e' = return (Pexp_apply (e0', [e1'; e2'])) in
+            e', b1
+         end else if name = "&&" then begin 
+           (* produce: let <b1> in if <e1'> then (let <b2> in <e2'>) else false *)
+             assign_var (return (
+                Pexp_ifthenelse (
+                  e1', 
+                  create_let loc b2 e2', 
+                  Some (mk_bool false)))) b1 
+         end else if name = "||" then begin
+           (* produce: let <b1> in if <e1'> then true else (let <b2> in <e2'>) *)
+             assign_var (return (
+                Pexp_ifthenelse (
+                  e1', 
+                  mk_bool true, 
+                  Some (create_let loc b2 e2')))) b1 
+         end else assert false
       | Pexp_apply (e0, l) ->
          let e0',b0 = aux false e0 in
          let ei',bi = List.split (List.map (fun (lk,ek) -> let ek',bk = aux false ek in (lk, ek'), bk) l) in
          let e' = return (Pexp_apply (e0', ei')) in
-         let b' = (List.flatten bi) @ b0 in
-         if is_inlined_primitive e0 l
+         let b' = reverse_if_right_to_left_order (b0 @ (List.flatten bi)) in
+         if exp_is_inlined_primitive e0 l
             then e', b'
             else assign_var e' b'
       | Pexp_match (e0, l) -> 
@@ -281,7 +367,8 @@ let normalize_expression named e =
       | Pexp_try (e,l) -> unsupported "exceptions"
       | Pexp_tuple l -> 
          let l',bi = List.split (List.map (aux false) l) in
-         return (Pexp_tuple l'), List.flatten bi
+         let b = List.flatten (reverse_if_right_to_left_order bi) in
+         return (Pexp_tuple l'), b
       | Pexp_construct (li, None, b) -> 
          return (Pexp_construct (li, None, b)), []
       | Pexp_construct (li, Some e, bh) -> 
@@ -291,7 +378,8 @@ let normalize_expression named e =
       | Pexp_record (l,Some eo) -> unsupported "record-with"
       | Pexp_record (l,None) -> 
          let l',bi = List.split (List.map (fun (i,(e,b)) -> ((i,e),b)) (assoc_list_map (aux false) l)) in
-         assign_var (return (Pexp_record (l', None))) (List.flatten bi)
+         let b = List.flatten (reverse_if_right_to_left_order bi) in
+         assign_var (return (Pexp_record (l', None))) b
       | Pexp_field (e,i) -> 
           let e',b = aux false e in
           assign_var (return (Pexp_field (e', i))) b
@@ -301,7 +389,8 @@ let normalize_expression named e =
           assign_var (return (Pexp_setfield (e', i, e2'))) (b2 @ b)
       | Pexp_array l ->  (* todo: use assign *)
          let l',bi = List.split (List.map (aux false) l) in
-         return (Pexp_array l'), List.flatten bi
+         let b = List.flatten (reverse_if_right_to_left_order bi) in
+         return (Pexp_array l'), b 
       | Pexp_ifthenelse (e1, e2, None) ->
           (* old:
           let e1', b = aux true e1 in
@@ -355,6 +444,11 @@ let normalize_expression named e =
       | Pexp_pack _ -> unsupported "pack"
       | Pexp_open (id,e) -> unsupported "open local" (* Pexp_open (id,aux e), b *)
        
+
+   (* [protect named e] calls the translation function [aux named e],
+       obtaining a transformed term [e'] under a list of bindings [b],
+       and it returns the term [let x1 = v1 in .. let xn = vn in e'] 
+       where the [b] gives the list of the [(xi,vi)] pairs. *)
    and protect named e =
       let (e',b) = aux named e in
       create_let e.pexp_loc b e'

generator/renaming.ml

@@ -10,7 +10,12 @@ let check_var loc x =
       as we use such an underscore to disambiguate with type variables *)
    let n = String.length x in
    if n > 0 && x.[n-1] = '_' 
-      then unsupported ("variables names should not end with an underscore: " ^ x)
+      then unsupported ("variables names should not end with an underscore: " ^ x);
+   if   (not !Clflags.nopervasives)  
+     && (List.mem x ["mod"; "/"; "&&"; "||"; "="; "<>"; "<="; ">="; "<"; ">"])
+      then unsupported ("CFML requires -nopervasives to allow binding of operator: " ^ x)
+
+
    (* --is this line needed?    if loc.loc_ghost then () else *)
   (* TODO: also reject programs with variables that may clash with these! *)
   (* TODO: make sure that check_var is called where needed *)
@@ -75,19 +80,10 @@ let builtin_constructors_table =
     (* --todo: add [Pervasives] as prefix *)
 
 
-(* for the mli file:
-
-   (** [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