inprogress

TODO

@@ -3,54 +3,20 @@
 
 
 
-URGENT
-
-- record generation breaks circularity through use of "loc" systematically for records
-
-SANITY 
-
-- reject programs with constructor names ending with "_"
-  (e.g. "A_" is already used for type variables *)
-
-- reject variable names and type definition that belongs to the list
-  builtin_type_constructors
-
-- rename on the fly coq keyword such as exists, forall, etc..
-  => requires a list of all coq keywords: see
-      else if name = "exists" then "exists__"
-      else if name = "forall" then "forall__"
-
-- prevent rebinding of List
-
-- restriction on not binding "min" and "max" might be a bit restrictive..
-
-
-COMPILATION
-
-
-- In the makefile.Coq, when building the .vq and obtaining
-	 "Error: /home/charguer/tlc/src/LibPer.vio: premature end of file. Try to rebuild it."
-  => then delete the .vio file
-    (useful for compilations interrupted using CTRL+C)
-  => even better, wrap "coqc -quick" with an atomic commit of its result.
-  
-
 MAJOR TODAY
 
-
-- record
-
-- array
-
-- notations for primitive ops
-
 - loops
 
 - mutual type defs
+   record generation breaks circularity through use of "loc" systematically for records
 
 
 MAJOR NEXT
 
+- record single field and array single cell notation
+	Notation "x `. f '~>' S" := 
+	Notation "x `[ i ] '~>' S" := 
+
 - partial application
 
 - xabstract => rename as xgen
@@ -76,18 +42,7 @@ MAJOR POSTPONED
   => how to shared typed/untyped AST
 
 
-
-
-LATER
-
-- semantics for records|arrays  passed by value / passed by reference
-
-
-
-
-
-TODO
-
+SANITY 
 
 - discuss the naming scheme
   => type t -->  t_ || x'
@@ -97,37 +52,51 @@ TODO
   => PB: plus_plus_infix' !
   => var x_ --> forbidden
 
+- reject programs with constructor names ending with "_"
+  (e.g. "A_" is already used for type variables *)
 
+- reject variable names and type definition that belongs to the list
+  builtin_type_constructors
 
-- in print_tast and print_past, protect with parenth the infix names being bound
+- rename on the fly coq keyword such as exists, forall, etc..
+  => requires a list of all coq keywords: see
+      else if name = "exists" then "exists__"
+      else if name = "forall" then "forall__"
 
-- make sure that check_var is called where needed 
+- prevent rebinding of List
+
+- restriction on not binding "min" and "max" might be a bit restrictive..
 
 - need to prevent double-underscore in the names? 
 
-- unify the source code in main.ml and makecmj.ml
 
-- check that there are no uses of labels in source files
+OTHER LANGUAGES
 
+- semantics for records|arrays  passed by value / passed by reference
 
-- make systematic use of    || (rm -f $@; exit 1)   in cfml calls
+- support null pointers
 
-- Ltac xcf_core tt   should be able to test whether Spec is a top val, and then do rewrite.
 
+CODE BEAUTIFY
 
-DEPRECATED?
+- make sure that check_var is called where needed 
 
-- no longer rely on myocamldep
+- unify the source code in main.ml and makecmj.ml
 
-- incorrect CF generation for "let n = null"
+- check that there are no uses of labels in input source files
 
+- Ltac xcf_core tt  
+  should be able to test whether Spec is a top val, and then do rewrite.
 
-(*
 
-(** Auxiliary function for the special case of compiling pervasives *)
+MAKEFILE BEAUTIFY
 
-let add_pervasives_prefix_if_needed p =
-  if !Clflags.nopervasives then "Pervasives." ^ p else p 
-   let p = add_pervasives_prefix_if_needed p in
+- no longer rely on myocamldep
+
+- make systematic use of    || (rm -f $@; exit 1)   in cfml calls
 
-*)
\ No newline at end of file
+- In the makefile.Coq, when building the .vq and obtaining
+	 "Error: /home/charguer/tlc/src/LibPer.vio: premature end of file. Try to rebuild it."
+  => then delete the .vio file
+    (useful for compilations interrupted using CTRL+C)
+  => even better, wrap "coqc -quick" with an atomic commit of its result.

examples/BasicDemos/Demo_proof.v

@@ -7,6 +7,60 @@ Require Import Stdlib.
 
 
 
+(********************************************************************)
+(* ** Records *)
+
+type 'a sitems = {
+  mutable nb : int;
+  mutable items : 'a list; }
+
+Lemma sitems_build n =
+  { nb = n; items = [] }
+Proof using.
+  xcf.
+Qed.
+
+Lemma sitems_get_nb r =
+  r.nb
+Proof using.
+  xcf.
+Qed.
+
+Lemma sitems_incr_nb r =
+  r.nb <- r.nb + 1 
+Proof using.
+  xcf.
+Qed.
+
+Lemma sitems_length_items r =
+  List.length r.items
+Proof using.
+  xcf.
+Qed.
+
+Lemma sitems_push x r =
+  r.nb <- r.nb + 1;
+  r.items <- x :: r.items
+Proof using.
+  xcf.
+Qed.
+
+
+(********************************************************************)
+(* ** Arrays *)
+
+Lemma array_ops () =
+  let t = Array.make 3 0 in
+  let _x = t.(1) in
+  t.(2) <- 4;
+  let _y = t.(2) in
+  let _z = t.(1) in
+  Array.length t
+Proof using.
+  xcf.
+Qed.
+
+
 
 (********************************************************************)
 (********************************************************************)
@@ -674,17 +728,6 @@ let order_record () =
 
 Require Import LibInt.
 
-Ltac xgo1_core tt :=
-  xgo_once tt.
-
-Tactic Notation "x" :=
-  xgo1_core tt.
-Tactic Notation "x" "~" := 
-  x; xauto~.
-Tactic Notation "x" "*" := 
-  x; xauto*.
-
-
 Lemma rec_partial_half_spec : forall k n,
   n = 2 * k ->
   app rec_partial_half [n] \[] \[= k].
@@ -825,60 +868,6 @@ Qed.
 
 
 
-(********************************************************************)
-(* ** Records *)
-
-type 'a sitems = {
-  mutable nb : int;
-  mutable items : 'a list; }
-
-Lemma sitems_build n =
-  { nb = n; items = [] }
-Proof using.
-  xcf.
-Qed.
-
-Lemma sitems_get_nb r =
-  r.nb
-Proof using.
-  xcf.
-Qed.
-
-Lemma sitems_incr_nb r =
-  r.nb <- r.nb + 1 
-Proof using.
-  xcf.
-Qed.
-
-Lemma sitems_length_items r =
-  List.length r.items
-Proof using.
-  xcf.
-Qed.
-
-Lemma sitems_push x r =
-  r.nb <- r.nb + 1;
-  r.items <- x :: r.items
-Proof using.
-  xcf.
-Qed.
-
-
-(********************************************************************)
-(* ** Arrays *)
-
-Lemma array_ops () =
-  let t = Array.make 3 0 in
-  let _x = t.(1) in
-  t.(2) <- 4;
-  let _y = t.(2) in
-  let _z = t.(1) in
-  Array.length t
-Proof using.
-  xcf.
-Qed.
-
-
 (********************************************************************)
 (* ** While loops *)
 

generator/characteristic.ml

@@ -611,18 +611,26 @@ let rec cfg_exp env e =
    (* TODO: only in purely function setting:   | Texp_record (lbl_expr_list, opt_init_expr) -> ret e*)
 
    | Texp_record (lbl_expr_list, opt_init_expr) ->
-      if opt_init_expr <> None then unsupported loc "record-with"; (* TODO *)
-      let (pathfront,pathend) = get_record_decomposed_name_for_exp e in
-      let func = Coq_var (pathfront ^ (record_make_name pathend)) in (* tood: move the underscore *)
+      if opt_init_expr <> None then unsupported loc "record-with"; 
       let named_args = List.map (fun (p,li,ei) -> (li.lbl_name,ei)) lbl_expr_list in
-      (* deprecated sorting: let args = List.map snd (list_ksort str_cmp named_args) in *)
-      let fields_names = extract_label_names_simple e.exp_env e.exp_type in
+      let build_arg (name, arg) =
+        let value = coq_apps coq_dyn_at [coq_typ arg; lift arg] in
+        Coq_tuple [Coq_var (record_field_name name); value]
+        in
+      let arg = coq_list (List.map build_arg named_args) in
+      Cf_record_new (arg)
+
+      (* DEPRECATED
+      let (pathfront,pathend) = get_record_decomposed_name_for_exp e in
+      let func = Coq_var (pathfront ^ (record_make_name pathend)) in 
+      let fields_names = extract_label_names_scimple e.exp_env e.exp_type in
       let args = 
          try List.map (fun name -> List.assoc name named_args) fields_names
          with Not_found -> failwith "some fields are missing in a record construction" 
          in
       let tprod = coq_prod (List.map coq_typ args) in
       Cf_app ([tprod], loc_type, func, [Coq_tuple (List.map lift args)]) 
+      *)
 
    | Texp_apply (funct, oargs) when exp_is_inlined_primitive funct oargs -> ret e
 
@@ -752,10 +760,7 @@ let rec cfg_exp env e =
       end
 
    | Texp_array args -> 
-      let ccons = Coq_var (get_builtin_constructor "::") in
-      let cnil = Coq_var (get_builtin_constructor "[]") in
-      let arg = List.fold_right (fun arg acc -> 
-         coq_apps ccons [lift arg; acc]) args cnil in
+      let arg = coq_list (List.map lift args) in
       let targ = (* ['a], obtained by extraction from ['a array]. *) 
          match btyp_of_typ_exp e.exp_type with
          | Btyp_constr (id,[t]) when Path.name id = "array" -> lift_btyp t
@@ -769,14 +774,24 @@ let rec cfg_exp env e =
    | Texp_field (arg, p, lbl) -> 
       let tr = coq_typ e in 
       let ts = coq_typ arg in (* todo: check it is always 'loc' *)
+      let func = Coq_var "CFML.CFApp.record_get" in
+      let field = Coq_var (record_field_name lbl.lbl_name) in
+      Cf_app ([ts; coq_nat], tr, func, [lift arg; field]) 
+      (* DEPRECATED
       let func = Coq_var (record_field_get_name lbl.lbl_name) in
       Cf_app ([ts], tr, func, [lift arg]) 
+      *)
 
    | Texp_setfield(arg, p, lbl, newval) -> 
       let ts1 = coq_typ arg in (* todo: check it is always 'loc' *)
       let ts2 = coq_typ newval in 
+      let func = Coq_var "CFML.CFApp.record_get" in
+      let field = Coq_var (record_field_name lbl.lbl_name) in
+      Cf_app ([ts1; coq_nat; ts2], coq_unit, func, [lift arg; field; lift newval]) 
+      (* DEPRECATED
       let func = Coq_var (record_field_set_name lbl.lbl_name) in
-      Cf_app ([ts1;ts2], coq_unit, func, [lift arg; lift newval]) 
+      Cf_app ([ts1;ts2], coq_unit, func, [lift arg; lift newval])
+      *)
 
    | Texp_try(body, pat_expr_list) -> unsupported loc "try expression"
    | Texp_variant(l, arg) ->  unsupported loc "variant expression"
@@ -1008,15 +1023,25 @@ and cfg_type_record (name,dec) =
       in
    let type_abbrev = Coqtop_def ((type_constr_name x, Coq_wild), coq_fun_types params loc_type) in
    [ type_abbrev ],
+   (* DEPRECATED BUT KEEP FOR FUTURE USE
    [ Coqtop_record top ] 
    @ (implicit_decl)
    @ [ Coqtop_hint_constructors ([record_structure_name x], "typeclass_instances") ]
-   @ record_functions x (record_constructor_name x) (record_repr_name x) params fields_names fields_types
+   @ 
+   *)
+   record_functions x (record_constructor_name x) (record_repr_name x) params fields_names fields_types
   (*  todo: move le "_of" *)
 
 (** Auxiliary function to generate stuff for records *)
 
-and record_functions name record_constr repr_name params fields_names fields_types =
+and record_functions name record_constr repr_name params fields_names fields_types =  
+   let build_field_name_def i field_name =
+      Coqtop_def ((field_name, coq_nat), Coq_nat i) 
+      in
+   let fields_names_def = list_mapi build_field_name_def fields_names in
+   fields_names_def
+
+   (* DEPRECATED BUT KEEP FOR FUTURE USE
    let nth i l = List.nth l i in
    let n = List.length fields_names in
    let indices = list_nat n in
@@ -1030,7 +1055,7 @@ and record_functions name record_constr repr_name params fields_names fields_typ
       [ Coqtop_param (nth i get_names, val_type); 
         Coqtop_param (nth i set_names, val_type) ] in
    
-   let logicals = List.map str_capitalize_1 fields_names (* for_indices (fun i -> sprintf "A%d" (i+1)) *) in
+   let logicals = List.map str_capitalize_1 fields_names 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
@@ -1050,6 +1075,7 @@ and record_functions name record_constr repr_name params fields_names fields_typ
    let tconcretes = List.map (fun i -> nth i concretes, nth i fields_types) indices in
    let tloc = (loc, loc_type) in
 
+
    let repr_args = tparams @ tlogicals @ treprs @ tabstracts @ [tloc] in
    let hcore = heap_is_single vloc (coq_apps (coq_var_at record_constr) (vparams @ vconcretes)) in
    let helems_items = for_indices (fun i -> hdata (nth i vconcretes) (Coq_app (nth i vreprs, nth i vabstracts))) in
@@ -1198,12 +1224,12 @@ and record_functions name record_constr repr_name params fields_names fields_typ
    @ [ repr_def ]
    @ repr_convert_focus_unfocus
    @ fields_convert_focus_unfocus
-   (* TODO: revive *)
-   (*
    @ new_spec
    @ (List.concat (List.map get_set_spec indices))
    @ (List.concat (List.map get_spec_focus indices))
-   @ (List.concat (List.map set_spec_unfocus indices)) *)
+   @ (List.concat (List.map set_spec_unfocus indices)) 
+
+   END DEPRECATED *)
   
 
 

generator/coq.ml

@@ -25,7 +25,6 @@ and coq =
   | Coq_var of var
   | Coq_nat of int
   | Coq_int of int
-  | Coq_list of coq list
   | Coq_app of coq * coq 
   | Coq_impl of coq * coq 
   | Coq_lettuple of coqs * coq * coq
@@ -38,6 +37,7 @@ and coq =
   | Coq_record of (var * coq) list 
   | Coq_tag of string * coq list * string option * coq
   | Coq_annot of coq * coq
+(* DEPRECATED ; maybe future ?  | Coq_list of coq list *)
 
 and coqs = coq list
 
@@ -136,8 +136,8 @@ let coq_unit =
 let coq_int =
   Coq_var "Coq.ZArith.BinInt.Z" 
 
-let coq_list xs =
-  Coq_list xs
+let coq_nat =
+  Coq_var "Coq.Init.Datatypes.nat"
 
 let coq_bool =
   Coq_var "Coq.Init.Datatypes.bool"
@@ -230,6 +230,24 @@ let coq_prod cs =
   | [c] -> c
   | c0::cs' -> List.fold_left (fun acc c -> coq_apps (Coq_var "Coq.Init.Datatypes.prod") [acc;c]) c0 cs'
 
+(** List [c1 :: c2 :: .. :: cN] *)
+
+let coq_list xs =
+   let ccons = Coq_var (Renaming.get_builtin_constructor "::") in
+   let cnil = Coq_var (Renaming.get_builtin_constructor "[]") in
+   List.fold_right (fun arg acc -> 
+      coq_apps ccons [arg; acc]) xs cnil
+   (* DEPRECATED ; maybe future ?
+   let coq_list xs =
+     Coq_list xs
+   *)
+   (* DEPRECATED
+   let ccons = get_builtin_constructor "::" in
+   let cnil = get_builtin_constructor "[]" in
+   let cnil = "Coq.Lists.List.nil" in
+   let ccons = "Coq.Lists.List.cons" in
+   *)
+
 (** Logic combinators *)
 
 let coq_eq c1 c2 =

generator/formula.ml

@@ -10,6 +10,7 @@ type cf =
   | Cf_fail
   | Cf_assert of cf
   | Cf_done
+  | Cf_record_new of coq
   | Cf_app of coqs * coq * coq * coqs
   | Cf_body of var * vars * typed_vars * coq * cf
   | Cf_let of typed_var * cf * cf

generator/formula.mli

@@ -19,6 +19,8 @@ type cf =
     (* Assert Q *)
   | Cf_done
     (* Done *)
+  | Cf_record_new of coq
+    (* AppNew [.. (fi, @dyn Ai xi) .. ] *)
   | Cf_app of coqs * coq * coq * coqs  
     (* App f [.. (@dyn Ai xi) .. ] (B:=B) *)
   | Cf_body of var * vars * typed_vars * coq * cf

generator/formula_to_coq.ml

@@ -46,6 +46,10 @@ let rec coqtops_of_imp_cf cf =
   | Cf_done -> 
       funhq "tag_done" coq_true
 
+  | Cf_record_new (arg) ->
+      (* AppNew [.. (fi, @dyn Ai xi) .. ] *)
+      coq_tag "tag_record_new" (coq_apps (Coq_var "CFML.CFApp.app_record_new") [arg])
+
   | Cf_app (ts, tret, f, vs) -> (* TODO: maybe make the return type explicit? *)
       (* old:  let arity = List.length vs in *)
       assert (List.length ts = List.length vs);

generator/print_coq.ml

@@ -134,10 +134,11 @@ let rec expr0 = function
       parens (string (string_of_int n)) ^^ string "%nat"
   | Coq_int n ->
       parens (string (string_of_int n)) ^^ string "%Z"
+   (* DEPRECATED ; maybe future ?
   | Coq_list cs ->
-      (* TODO: *)
-      if (cs = []) then string "nil" else 
+      if (cs = []) then string cnil else 
         parens ((separate_map (string "::" ^^ break 1) expr0 cs) ^^ string "::nil")
+     *)
   | Coq_wild ->
       string "_"
   | Coq_prop ->

generator/renaming.ml

@@ -318,10 +318,14 @@ let record_field_name name =
 
 (** Convention for naming record accessor function *)
 
-let record_field_get_name name =
+let record_field_name name =
+  name ^ "'"
+  (* TODO: avoid names ending with a quote in caml code *)
+
+let record_field_get_name name = (* DEPRECATED *)
   name ^ "__get"
 
-let record_field_set_name name =
+let record_field_set_name name = (* DEPRECATED *)
   name ^ "__set"
 
 (** Convention for naming record accessor function specifications *)

lib/coq/CFApp.v

@@ -8,36 +8,6 @@ Hint Extern 1 (_ ===> _) => apply rel_le_refl.
 
 
 
-(********************************************************************)
-(* ** Axioms of CFML *)
-
-(** Note: these axioms could in theory be realized by constructing
-    a deep embedding of the target programming language.  
-    See Arthur Chargueraud's PhD thesis for full details. *)
-
-(** The type Func, used to represent functions *)
-
-Axiom func : Type. 
-
-(** The type Func is inhabited *)
-
-Axiom func_inhab : Inhab func. 
-
-Existing Instance func_inhab.
-
-(** The evaluation predicate for functions: [eval f v h v' h'], 
-    asserts that the evaluation of the application of [f] to [v]
-    in a heap [h] terminates and produces a value [v'] in a heap [h']. *)
-
-Axiom eval : forall A B, func -> A -> heap -> B -> heap -> Prop.
-
-
-
-
-
-
-
-
 (********************************************************************)
 (* ** Overview *)
 
@@ -66,9 +36,35 @@ Axiom eval : forall A B, func -> A -> heap -> B -> heap -> Prop.
   These definitions are correct and sufficient to reasoning about all
   function calls, including partial and over applications.
 
+
+  This file also contains axiomatization of record operations.
+
 *)
 
 
+(********************************************************************)
+(* ** Axioms for applications *)
+
+(** Note: these axioms could in theory be realized by constructing
+    a deep embedding of the target programming language.  
+    See Arthur Chargueraud's PhD thesis for full details. *)
+
+(** The type Func, used to represent functions *)
+
+Axiom func : Type. 
+
+(** The type Func is inhabited *)
+
+Axiom func_inhab : Inhab func. 
+
+Existing Instance func_inhab.
+
+(** The evaluation predicate for functions: [eval f v h v' h'], 
+    asserts that the evaluation of the application of [f] to [v]
+    in a heap [h] terminates and produces a value [v'] in a heap [h']. *)
+
+Axiom eval : forall A B, func -> A -> heap -> B -> heap -> Prop.
+
 
 (********************************************************************)
 (* ** Definition and properties of the primitive app predicate *)
@@ -177,13 +173,6 @@ Notation "'app_keep' f xs H Q" :=
   (app f xs H%h (Q \*+ H))
   (at level 80, f at level 0, xs at level 0, H at level 0) : charac.
 
- 
-Definition demo_arglist := 
-  forall f (xs:list int) (x y:int) B H (Q:B->hprop),
-  app f [ x y ] H Q.
-(* Print demo_arglist. *)
-(* TODO: find a way that the parentheses are not printed around "app" *)
-
 
 (** Reformulation of the definition *)
 
@@ -399,7 +388,8 @@ Qed.
 
 
 (********************************************************************)
-(* ** Definition of [spec]  *)
+(* ** Packaging *)
+
 
 (** [spec f n P] asserts that [curried f n] is true and that  
     the proposition [P] is a valid specification for [f]. 
@@ -408,166 +398,18 @@ Qed.
 Definition spec (f:func) (n:nat) (P:Prop) :=
   curried n f /\ P.
 
-
-
-(********************************************************************)