progress

examples/BasicDemos/Test.ml

 
 
+(* ---CFML not supported : requires value restriction  *)
+
+
+let p0 () =
+   let x = (None = None) in ()
+
+let p1 () =
+   let f x = x in
+   let _r = f None in
+   ()
+
+let p2 () =
+   let f x = x in
+   let _r = 
+      let _s = f None in ()
+      in
+   ()
+
+(*
+
+let compare_poly () =
+   let _r1 = (None = None) in
+   let _r2 = (Some 3 = None) in
+   let _r3 = ((Some 3, None) = (Some 3, None)) in
+   let _r4 = (true = false) in
+   ()
+*)
+
+
 
 let f0 () =
   let r = ref [] in
   !r
 
+
 let f1 () : 'a list =
   let r = ref ([] : 'a list) in
   !r
@@ -36,19 +66,22 @@ let m0 () =
    let r = ref [] in
    r
 
+
 let h0 () =
   let g =
      let f () = ref [] in
      f in
   g
 
-(* not allowed because produces a ['_a list ref] at top level;
+
+(* ---Code not allowed because produces a ['_a list ref] at top level;
    i.e. rejected when using OCaml "-strict_value_restriction" flag 
 let h1 =
   let f () : 'a list ref = ref [] in
   f
 *)
 
+
 let h2 () =
   let f () : 'a list ref = ref [] in
   f
@@ -64,14 +97,14 @@ let k1 () =
 let k2 () =
   ref []
 
-(* CF does not typecheck because the type cannot be resolved 
+(* ---CF does not typecheck because the type cannot be resolved 
 
 let r1 () =
    let _x = ref [] in
    ()
 *)   
 
-(* CF does not typecheck because the type cannot be resolved 
+(* ---CF does not typecheck because the type cannot be resolved 
 
 let r2 () =
    let _x = ref [] in
@@ -80,12 +113,25 @@ let r2 () =
 
 *)
 
+(* ---CFML does not yet support: relaxed value restriction 
+
+let r3 () =
+   let r = 
+      let x = ref [] in
+      [] in
+   r
+*)
+
+
+
+
+
 type 'a sitems = {
   mutable nb : int;
   mutable items : 'a list; }
 
 let sitems_build n =
-  { nb = n; items = [] }
+  { nb = n; items = [7] }
 
 let sitems_incr_nb_let r =
   let x = r.nb in
@@ -95,6 +141,6 @@ let sitems_length_items_let r =
   let x = r.items in
   List.length x
  
+ (*----------------------
 
-
-
+--------------------*)
\ No newline at end of file

examples/Makefile.example

@@ -97,8 +97,8 @@ cf: $(ML)
 # Make sure TLC and CFML itself are up-to-date.
 # Needed only when developing TLC and CFML. Ideally, should be removed.
 	@$(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) --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) CFML=$(CFML) OCAML_FLAGS=$(OCAML_FLAGS) COQINCLUDE="$(COQINCLUDE)" ML="$(ML)" --no-print-directory -f $(CFML)/lib/make/Makefile.cf all
 
@@ -106,13 +106,13 @@ else
 
 #----------------FOR DIRECT TEST----------------------
 
-#-strict_value_restriction
-EXTRA= -only_normalize -debug
+# -only_normalize -strict_value_restriction
+EXTRA=-debug 
 
 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) --no-print-directory tools coqlib_quick_cf 
+	@$(MAKE) -C $(CFML) --no-print-directory tools coqlib_quick 
 	@$(MAKE) -C $(CFML)/lib/stdlib CFDEBUG=$(CFDEBUG) --no-print-directory cmj
 	@$(MAKE) CFML=$(CFML) EXTRA="$(EXTRA)" OCAML_FLAGS="$(OCAML_FLAGS)" COQINCLUDE="$(COQINCLUDE)" ML="$(ML)" --no-print-directory -f $(CFML)/lib/make/Makefile.cf all
 

generator/characteristic.ml

@@ -13,8 +13,14 @@ open Renaming
 open Printf
 
 
+(*#########################################################################*)
+(* ** Aux *)
+
+(** [list_is_included l1 l2] returns true if any item in [l1] also belongs to [l2] *)
+
+let list_is_included l1 l2 =
+   List.for_all (fun x -> List.mem x l2) l1
 
-let debug_generic = false
 
 (*#########################################################################*)
 (* ** Error messages *)
@@ -237,7 +243,9 @@ let coq_of_constructor loc p c ty =
       | None -> x, (typ_arity_constr c)
       | Some (coq_name,arity) -> coq_name, arity
       in
-    coq_apps (coq_var_at coq_name) typs
+    if typs = [] 
+      then coq_var coq_name
+      else coq_apps (coq_var_at coq_name) typs
    (* DEPRECATED: coq_app_var_wilds coq_name arity *)
     
 (* TODO: we might have some issue if type abbreviation
@@ -285,7 +293,7 @@ let rec lift_pat ?(through_aliases=true) p : coq =
       | TPat_alias id -> 
           if through_aliases then aux p else Coq_var (var_name (Ident.name id))
       | TPat_constraint ty -> 
-          let typ = lift_typ_sch_as_forall loc ty.ctyp_type in
+          let typ = lift_typ_exp loc ty.ctyp_type in 
           Coq_annot (aux p, typ)
       | TPat_type pp -> aux p 
       end
@@ -508,7 +516,7 @@ let rec lift_val env e =
    | Texp_lazy e -> 
       aux e
    | Texp_constraint (e, Some ty, None) -> 
-      let typ = lift_typ_sch_as_forall loc ty.ctyp_type in
+      let typ = lift_typ_exp loc ty.ctyp_type in
       Coq_annot (aux e, typ)
 
    (* --uncomment for debugging 
@@ -615,6 +623,36 @@ let rec extract_label_names_simple env ty =
   | _ -> assert false
 
 
+(*#########################################################################*)
+(* ** Helper functions for fvs (type variables) *)
+
+
+let show_fvs title fvs =
+   Format.fprintf Format.err_formatter "%s = %s\n" title (show_list show_str " , " fvs)
+
+(* needs to be called only after typing the body of the definition
+   associated with the pattern, so as to know which names are actually used. *)
+
+let get_fvs_typ loc fvs typ = 
+  let typ = lift_typ_exp loc typ in
+  let fvs = List.map name_of_type (List.filter typvar_is_used fvs) in
+  (fvs, [], typ)
+
+  (* DEPRECATED
+  let fvs_typ, typ = lift_typ_sch loc typ in
+  let fvs = List.map name_of_type (List.filter typvar_is_used fvs) in
+  if Settings.debug_generic then begin
+     show_fvs "fvs_typ" fvs_typ;
+     show_fvs "fvs" fvs;
+  end;
+  if not (list_is_included fvs_typ fvs)  
+    then failwith "fvs_typ not included in fvs for let binding";
+  let fvs_strict = fvs_typ in  
+  let fvs_others = list_minus fvs fvs_strict in
+  (fvs_strict, fvs_others, typ)
+  *)
+
+
 (*#########################################################################*)
 (* ** Characteristic formulae for expressions *)
 
@@ -689,17 +727,7 @@ let rec cfg_exp env e =
         if (List.length pat_expr_list <> 1) then not_normal();
         let (pat,bod) = List.hd pat_expr_list in
         let x = pattern_name_protect_infix pat in
-   
-        let get_fvs_typ () = (* needs to be called after typing the body! *)
-           let fvs_typ, typ = lift_typ_sch loc pat.pat_type in
-           let fvs = List.map name_of_type (List.filter typvar_is_used fvs) in
-           if debug_generic 
-              then Printf.printf "fvs exp_let = %s\n" (show_list show_str " , " fvs);
-           let fvs_strict = (* list_intersect fvs *) fvs_typ in
-           let fvs_others = list_minus fvs fvs_strict in
-           (fvs_strict, fvs_others, typ)
-           in
-
+        
         (* deprecated: pure-mode let-binding
         if !pure_mode then begin 
        
@@ -707,7 +735,7 @@ let rec cfg_exp env e =
            let env' = Ident.add (pattern_ident pat) (List.length fvs_strict) env in
            let cf2 = cfg_exp env' body in
            add_used_label x;
-           Cf_letpure (x, fvs_strict, fvs_others, typ, cf1, cf2)
+           Cf_let_poly (x, fvs_strict, fvs_others, typ, cf1, cf2)
          end else *)
 
         (* value let-binding *)
@@ -718,7 +746,7 @@ let rec cfg_exp env e =
              with Not_in_normal_form (loc2, s) -> 
                 raise (Not_in_normal_form (loc2, s ^ " (only value can satisfy the value restriction)"))
              in
-           let (fvs_strict, fvs_others, typ) = get_fvs_typ() in
+           let (fvs_strict, fvs_others, typ) = get_fvs_typ loc fvs pat.pat_type in
            let env' = Ident.add (pattern_ident pat) (List.length fvs_strict) env in
            let cf = cfg_exp env' body in
            add_used_label x;
@@ -726,7 +754,7 @@ let rec cfg_exp env e =
 
         (* term let-binding *)
         end else begin
-           let (fvs_strict, fvs_others, typ) = get_fvs_typ() in
+           let (fvs_strict, fvs_others, typ) = get_fvs_typ loc fvs pat.pat_type in
            if fvs_strict <> [] (* || fvs_others <> [] 
             TODO: if this is not empty, it'd better get bind elsewhere
            *) then begin
@@ -869,22 +897,11 @@ and cfg_func env fvs pat bod =
    let loc = pat.pat_loc in
    let f = pattern_name_protect_infix pat in
    let targs, body = get_typed_args [] bod in
-   let fv_body, typ = lift_typ_sch loc body.exp_type in
+   let typ = lift_typ_exp loc body.exp_type in
    let cf_body = cfg_exp env body in
    let cf_body = if !Mytools.use_credits then Cf_pay cf_body else cf_body in
    (* fvs computation must come after cf_body *)
    let fvs = List.map name_of_type (List.filter typvar_is_used fvs) in
-   if debug_generic then begin
-      Printf.printf "fvs cfg_func = %s\n" (show_list show_str " , " fvs);
-      Printf.printf "fvs_body cfg_func = %s\n" (show_list show_str " , " fv_body);
-   end;
-(*
-              let fvs_typ, typ = lift_typ_sch loc pat.pat_type in
-           let fvs = List.map name_of_type (List.filter typvar_is_used fvs) in
-           let fvs_strict = (*list_intersect fvs*) fvs_typ in
-           let fvs_others = list_minus fvs fvs_strict in
-           (fvs_strict, fvs_others, typ)
-*)
    Cf_body (f, fvs, targs, typ, cf_body) 
    (* --todo: check if the set of type variables quantified is not too
       conservative. Indeed, some type variables may no longer occur. *)
@@ -939,17 +956,6 @@ let rec cfg_structure_item s : cftops =
         let x = pattern_name_protect_infix pat in
         (* DEPRECATED if (hack_recognize_okasaki_lazy x) then [] else *)
         begin
-        
-        let get_fvs_typ () = (* need to be called after translating body *)
-           (* TODO: factorize with similar code for let bindings *)
-           let fvs_typ, typ = lift_typ_sch loc pat.pat_type in
-           let fvs = List.map name_of_type (List.filter typvar_is_used fvs) in
-           if debug_generic 
-              then Printf.printf "fvs str_value = %s\n" (show_list show_str " , " fvs);
-           let fvs_strict = (*list_intersect fvs*) fvs_typ in
-           let fvs_others = list_minus fvs fvs_strict in
-           (fvs_strict, fvs_others, typ)
-           in
 
         (* deprecated: pure-mode let-binding 
         if !pure_mode then begin 
@@ -975,10 +981,15 @@ let rec cfg_structure_item s : cftops =
                 (* TODO: here and elsewhere, use a wrapper for extending the errors *)
                 raise (Not_in_normal_form (loc2, s ^ " (only value can satisfy the value restriction)"))
             in
-           
-           let (fvs_strict, fvs_others, typ) = get_fvs_typ() in
-           let v_typed = coq_annot v typ in
+              
+           let fvs_typ, typ = lift_typ_sch loc pat.pat_type in
+           let fvs = List.map name_of_type (List.filter typvar_is_used fvs) in
+           if not (list_is_included fvs_typ fvs)  
+             then failwith "fvs_typ not included in fvs for let binding";
+           let fvs_strict = fvs_typ in
+           let fvs_others = list_minus fvs fvs_strict in
 
+           let v_typed = coq_annot v typ in
            let implicits = 
               match fvs_strict with
               | [] -> []
@@ -993,6 +1004,7 @@ let rec cfg_structure_item s : cftops =
         end else begin
             
            unsupported loc "top-level binding of terms that are not values";
+           (* let (fvs_strict, fvs_others, typ) = get_fvs_typ loc fvs pat.pat_type in*)
 
            (* if fvs_strict <> [] || fvs_others <> [] 
                then not_in_normal_form loc ("(unsatisfied value restriction) "
@@ -1560,6 +1572,7 @@ and cfg_module id m =
     a Caml file. *)
 
 let cfg_file str =
+   Print_type.type_rename := Renaming.type_variable_name;
    [ Cftop_coqs ([ 
       Coqtop_set_implicit_args; 
       Coqtop_require [ "Coq.ZArith.BinInt"; "TLC.LibLogic"; "TLC.LibRelation"; "TLC.LibInt"; "TLC.LibListZ"; "CFML.Shared"; "CFML.CFHeaps"; "CFML.CFApp"; "CFML.CFPrint"; "CFML.CFBuiltin" ];

generator/formula.ml

@@ -16,7 +16,7 @@ type cf =
   | Cf_app of coqs * coq * coq * coqs
   | Cf_body of var * vars * typed_vars * coq * cf
   | Cf_let of typed_var * cf * cf
-  | Cf_letpure of var * vars * vars * coq * cf * cf
+  | Cf_let_poly of var * vars * vars * coq * cf * cf
   | Cf_val of var * vars * vars * coq * coq * cf
   | Cf_fun of (var * cf) list * cf
   | Cf_caseif of coq * cf * cf

generator/formula.mli

@@ -30,7 +30,7 @@ type cf =
     (* Body f Ai xi => Q *)
   | Cf_let of typed_var * cf * cf 
     (* Let x := Q1 in Q2 *)
-  | Cf_letpure of var * vars * vars * coq * cf * cf 
+  | Cf_let_poly of var * vars * vars * coq * cf * cf 
     (* Let x [Ai,Bi] := Q1 in Q2  // where x : forall Ai.T *)
   | Cf_val of var * vars * vars * coq * coq * cf 
     (* Let x [Ai,Bi] := v in Q2  // where x : forall Ai.T *)

generator/formula_to_coq.ml

@@ -285,6 +285,22 @@ let rec coqtops_of_imp_cf cf =
 
   | Cf_letpure _ -> unsupported_noloc "letpure-expression in imperative mode"
 
+   (*
+  | Cf_letpure (x, fvs_strict, fvs_other, typ, cf1, cf2) ->
+      let type_of_x = coq_forall_types fvs_strict typ in
+      let tvars = coq_vars fvs_strict in
+      let p1_on_tvars = if tvars = [] then Coq_var "P1" else coq_apps (coq_var_at "P1") tvars in
+      let c1 = coq_forall_types (fvs_strict @ fvs_other) (Coq_app (coq_of_cf cf1, p1_on_tvars)) in
+      let x_on_tvars = if tvars = [] then Coq_var x else coq_apps (coq_var_at x) tvars in 
+      let hyp_on_x = coq_forall_types fvs_strict (coq_apps (Coq_var "@P1") (tvars @ [ x_on_tvars ])) in
+      let c2 = coq_foralls [x,type_of_x] (Coq_impl (hyp_on_x, Coq_app (coq_of_cf cf2, p))) in
+      let type_of_p1 = coq_forall_types fvs_strict (coq_pred typ) in
+      funp "tag_let" ~label:x (coq_exist "P1" type_of_p1 (coq_conj c1 c2))
+      (*(!L a: (fun P => exists (P1:forall A1, T -> Prop), (forall A1 B1, Q1 (P1 A1))
+                             /\ forall (x1:forall A1,T), ((forall A1, P1 A1 (x1 A1)) -> Q2 P)) *)
+    
+   *)
+
   (* --todo: scope of type variables should be different than that of program variables: prefix them! *)
 
 

generator/main.ml

@@ -38,11 +38,13 @@ let spec =
     ("-o", Arg.String (fun s -> outputfile := Some s), " set the output file name");
     ("-only_cmj", Arg.Set only_cmj, " only generate the .cmj file, not the .v file");
     ("-only_normalize", Arg.Set only_normalize, " only generate the .cmj file, and attempt normalization, not the .v file");
-    ("-strict_value_restriction", Arg.Set Clflags.strict_value_restriction, " enforce the strict value restriction (relaxed value restriction is the default)");
     ("-debug", Arg.Set is_tracing, " trace the various steps");
     ("-width", Arg.Set_int Print_coq.width, " set pretty-printing width for the .v file");
   ]
 
+(*
+    ("-strict_value_restriction", Arg.Set Clflags.strict_value_restriction, " enforce the strict value restriction (relaxed value restriction is the default)");
+*)
 
 
 let _ =

generator/print_tast.ml

@@ -11,9 +11,6 @@ open Print_type
 (** Printing facility for typed abstract syntax trees produced by the 
     type-checker*)
 
-let _ = 
-   Print_type.type_rename := (fun s -> s)
-
 
 (*#########################################################################*)
 (* ** Printing of items *)

generator/print_type.ml

@@ -12,14 +12,13 @@ open Asttypes
 open Btype
 open Printtyp
 open Outcometree
-open Renaming
 
 (** This file contains a data structure for representing types in an
     explicit form, as well as an algorithm for extracting such types
     from the representation used by OCaml's compiler. *)
 
 
-let type_rename = ref type_variable_name
+let type_rename = ref (fun s -> s) 
 
 
 (*#########################################################################*)

generator/print_type.mli

@@ -48,6 +48,9 @@ val string_of_type_exp : Types.type_expr -> string
 
 val string_of_type_sch : Types.type_expr list -> Types.type_expr -> string
 
-(** Customization of the type renaming function *)
+
+(** Customization of the type renaming function;
+    The identity function by default. 
+    (Reference set by Characteristic.cfg_file.) *)
 
 val type_rename : (string -> string) ref

generator/settings.ml

 
 let configure () =
    Config.interface_suffix := "____mli_files_are_ignored____";
-   (* Clflags.strict_value_restriction := true; *)
+   Clflags.strict_value_restriction := true;  
    Clflags.no_std_include := true
 
+(* strict_value_restriction is needed to avoid problematic over-generalization
+   on e.g. the code "let x = r.nb in ()", where nb is a record field *)
\ No newline at end of file

generator/typing/ctype.ml

@@ -148,7 +148,7 @@ let proper_abbrevs path tl abbrev =
                   (**********************************)
 
 (* CFML *)
-let debug_generic = false
+let debug_generic = true
 let hook_generic : (((type_expr list) ref) list) ref = ref []
 let open_hook () = 
    if debug_generic 
@@ -808,7 +808,9 @@ let close_hook ?(showtyp=(fun t -> ())) ~gen_nonexpansive () =
             if debug_generic then begin
                Format.fprintf Format.err_formatter "-->was at level %d\n" t.level;
             end;
-            generalize_structure t;
+            generalize t;
+            (* does not seem to generalize what it should
+               generalize_structure t; *)
             if gen_nonexpansive && t.level = !nongen_level then begin
                Format.fprintf Format.err_formatter "-->>> generalized non-expansive\n";
                set_level t generic_level;