Merge branch 'master' of git+ssh://scm.gforge.inria.fr//gitroot/cfml/cfml

examples/BasicDemos/Demo.ml

 
+(*---------polymorphism -----------*)
+
+
+let test_poly () = let x = [] in x
+
+
 (*---------simple record------------*)
 
 type 'a myrec = {

examples/BasicDemos/Demo_proof.v

+Set Implicit Arguments.
 
+Require Import CFLib LibInt LibWf (*Facts*) Demo_ml.
+
+
+(*************************************************************************)
+
+(*
+let test_poly () = let x = [] in x
+*)
+
+Lemma test_poly_spec : forall A,
+  Spec test_poly () |B>>
+  B \[] (fun (x:list A) => \[x = @nil A]).
+Proof.
+  intros. xcf. 
+  apply local_erase. intros x Ex.
+  xret.
+  hsimpl.
+  subst x. auto.
+Qed.
 
 
-Set Implicit Arguments.
 
-Require Import CFLib LibInt LibWf (*Facts*) Demo_ml.
 
 
 (*************************************************************************)

generator/characteristic.ml

@@ -36,7 +36,7 @@ let lift_ident_name id =
    let name = Ident.name id in
    if name = "OkaStream" then "CFPrim" else (* TODO : improve *)
    if Ident.persistent id  
-      then name ^ "_ml" (* TODO: also emit a Require directive on name ^ "_ml" *)
+      then  (Printf.printf "require %s\n" name; name  ^ "_ml")
       else "ML" ^ name
 
 let rec lift_full_path = function
@@ -194,7 +194,7 @@ let coq_of_constructor p c =
    let x = string_of_path p in
    match find_builtin_constructor x with
    | None -> coq_app_var_wilds x (typ_arity_constr c) 
-   | Some y -> Coq_var y
+   | Some (y,arity) -> coq_app_var_wilds y arity
 
 
 (*#########################################################################*)

generator/formula.ml

@@ -370,10 +370,10 @@ let rec coq_of_imp_cf cf =
 
   | Cf_letval (x, fvs_strict, fvs_other, typ, v, cf) ->
       let type_of_x = coq_forall_types fvs_strict typ in
-      let equ = coq_eq (Coq_var x) v in
+      let equ = coq_eq (Coq_var x) (coq_fun_types fvs_strict v) in
       let conc = coq_apps (coq_of_cf cf) [h;q] in
       funhq "tag_let_val" (*~label:x*) (Coq_forall ((x, type_of_x), Coq_impl (equ, conc)))
-      (*(!!L x: (fun H Q => forall (x:forall Ai,T), x = v -> F H Q)) *)
+      (*(!!L x: (fun H Q => forall (x:forall Ai,T), x = (fun Ai => v) -> F H Q)) *)
  
   | Cf_letfunc (ncs, cf) ->
       let ns, cs = List.split ncs in

generator/primitives.ml

@@ -135,15 +135,15 @@ let all_primitives_table =
     inductive data constructors in Coq. *)
 
 let builtin_constructors_table =
-  [ "[]", "Coq.Lists.List.nil";
-    "::", "Coq.Lists.List.cons";
-    "()", "Coq.Init.Datatypes.tt";
-    "true", "Coq.Init.Datatypes.true";
-    "false", "Coq.Init.Datatypes.false";
-    "Nil", "Coq.Lists.List.nil";
-    "Cons", "Coq.Lists.List.cons";
-    "OkaStream.Nil", "Coq.Lists.List.nil";
-    "OkaStream.Cons", "Coq.Lists.List.cons";
+  [ "[]", ("Coq.Lists.List.nil", 1);
+    "::", ("Coq.Lists.List.cons", 1);
+    "()", ("Coq.Init.Datatypes.tt", 0);
+    "true", ("Coq.Init.Datatypes.true", 0);
+    "false", ("Coq.Init.Datatypes.false", 0);
+    "Nil", ("Coq.Lists.List.nil", 1);
+    "Cons", ("Coq.Lists.List.cons", 1);
+    "OkaStream.Nil", ("Coq.Lists.List.nil", 1);
+    "OkaStream.Cons", ("Coq.Lists.List.cons", 1);
     ]
     (* --todo: add [Pervasives] as prefix *)