generated

examples/BasicDemos/Demo.ml

+open Pervasives
+
 (** 
  *
  * This file contains unit tests for testing the generation of
@@ -176,18 +178,20 @@ let let_poly_nil_pair_heterogeneous () =
 let match_pair_as () =
    match (3,4) with (a, (b as c)) as p -> (c,p)
 
+let match_nested () =
+  let l = [ (1,1); (0,0); (2,2) ] in
+  match l with
+  | _::(0,0)::q -> q
+  | _ -> []
+
+(* not yet supported when clauses
 let match_term_when () =
    let f x = x + 1 in
    match f 3 with 
    | 0 -> 1
    | n when n > 0 -> 2
    | _ -> 3
-   
-let match_nested () =
-  let l = [ (1,1); (0,0); (2,2) ] in
-  match l with
-  | _::(0,0)::q -> q
-  | _ -> []
+*)
 
 
 (********************************************************************)

generator/characteristic.ml

@@ -47,11 +47,12 @@ let external_modules_reset () =
 
 let lift_ident_name id =
    let name = Ident.name id in
-   let coqname = name ^ "_" in
+   let coqname = name ^ "_ml" in
    if Ident.persistent id then external_modules_add coqname;
    coqname
+
    (* -- old:
-   if Ident.persistent id  
+     if Ident.persistent id  
       then (let result = name ^ "_ml" in external_modules_add result; result)
       else "ML" ^ name
    *)
@@ -542,7 +543,7 @@ let rec cfg_exp env e =
          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)]) 
+      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
 
@@ -629,7 +630,7 @@ let rec cfg_exp env e =
       let args = simplify_apply_args oargs in
       let tr = coq_typ e in
       let ts = List.map coq_typ args in
-      Cf_app (ts@[tr], lift funct, List.map lift args) 
+      Cf_app (ts, tr, lift funct, List.map lift args) 
 
    | Texp_match (arg, pat_expr_list, partial) ->
       let tested = lift arg in
@@ -678,13 +679,13 @@ let rec cfg_exp env e =
       let tr = coq_typ e in 
       let ts = coq_typ arg in (* todo: check it is always 'loc' *)
       let func = Coq_var (name_for_record_get lbl) in
-      Cf_app ([ts;tr], func, [lift arg]) 
+      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 (name_for_record_set lbl) 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 "try expression"
    | Texp_variant(l, arg) ->  unsupported "variant expression"

generator/coq.ml

@@ -23,7 +23,9 @@ and coq_path =
 
 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
@@ -132,6 +134,9 @@ let coq_unit =
 let coq_int =
   Coq_var "int" 
 
+let coq_list xs =
+  Coq_list xs
+
 let coq_bool =
   Coq_var "bool"
 

generator/formula.ml

@@ -10,7 +10,7 @@ type cf =
   | Cf_fail
   | Cf_assert of cf
   | Cf_done
-  | Cf_app of coqs * coq * coqs
+  | 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
@@ -162,6 +162,7 @@ let heap_pred c =
 (*#########################################################################*)
 (* ** Conversion of IMPERATIVE characteristic formulae to Coq *)
 
+
 let rec coqtops_of_imp_cf cf =
   let coq_of_cf = coqtops_of_imp_cf in
   let h = Coq_var "H" in
@@ -199,17 +200,17 @@ let rec coqtops_of_imp_cf cf =
   | Cf_done -> 
       funhq "tag_done" coq_true
 
-  | Cf_app (ts, f, vs) -> 
-      (* the following is the same as for pure *)
-      let arity = List.length vs in
-      assert (arity > 0);
-      let appn = coq_var_at ("app_" ^ (string_of_int arity)) in
-      coq_tag "tag_apply" (coq_apps appn (ts @ f::vs))
-      (* (!A: (app_2 f x1 x2)) *)
+  | 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);
+      let tvs = List.combine ts vs in
+      let args = List.map (fun (t,v) -> coq_apps (coq_var_at "dyn") [t;v]) tvs in
+      coq_tag "tag_apply" (coq_apps (coq_var_at "app_def") [f; coq_list args; tret])
+      (* (!Apply: (app_def f [(@dyn t1 v1) (@dyn t2 v2)])) *)
 
+  (* DEPRECATED
   | Cf_body (f, fvs, targs, typ, cf) ->
       let type_of_k = coq_impls ((List.map snd targs) @ [formula_type_of typ]) Coq_prop in
-      (* the following is the same as for pure *)
       let args = List.map fst targs in
       let args_of_k = (List.map coq_var args) @ [ coq_of_cf cf ] in
       let var_k = Coq_var "K" in
@@ -221,6 +222,20 @@ let rec coqtops_of_imp_cf cf =
       coq_tag "tag_body" (coq_forall_types fvs (coq_foralls ["K", type_of_k] (coq_impls [is_spec_k;hyp_k] concl_k)))       
       (* (!B: (forall Ai K, is_spec_2 K -> 
                  (forall x1 x2, K x1 x2 F) -> spec_2 K f)) *)
+  *)
+
+  | Cf_body (f, fvs, targs, typ, cf1) ->
+      let narity = Coq_nat (List.length targs) in
+      let h_curried = coq_apps (Coq_var "curried") [narity; coq_var f] in 
+      let h_body_hyp = coq_apps (coq_of_cf cf1) [h; q] in
+      let args = List.map (fun (x,t) -> coq_apps (coq_var_at "dyn") [t; coq_var x]) targs in
+      let h_body_conc = coq_apps (Coq_var "app_def") [coq_var f; coq_list args; h; q]  in
+      let h_body_2 = Coq_impl (h_body_hyp, h_body_conc) in
+      let h_body_1 = coq_foralls [("H", hprop); ("Q", Coq_impl (typ, hprop))] h_body_2 in
+      let h_body = coq_forall_types fvs (coq_foralls targs h_body_1) in
+      coq_tag "tag_body" (coq_conj h_curried h_body)
+      (* (!B: curried 2 f /\ 
+              (forall Ai x1 x2 H Q, CF H Q -> app f [(dyn t1 x1) (dyn t2 x2)] H Q) *)
 
   | Cf_let ((x,typ), cf1, cf2) ->
       let q1 = Coq_var "Q1" in

generator/formula.mli

@@ -19,8 +19,8 @@ type cf =
     (* Assert Q *)
   | Cf_done
     (* Done *)
-  | Cf_app of coqs * coq * coqs  
-    (* App f 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
     (* Body f Ai xi => Q *)
   | Cf_let of typed_var * cf * cf 

generator/primitives.ml

@@ -31,32 +31,33 @@ let inlined_primitives_table =
    "Pervasives.~-", (1, "Coq.ZArith.BinInt.Zopp"); 
    "Pervasives.&&", (2, "LibBool.and");
    "Pervasives.||", (2, "LibBool.or");
-   (*
-   "Pervasives./", (primitive_special, "Coq.ZArith.Zdiv.Zdiv");
-   "Pervasives.mod", (primitive_special, "Coq.ZArith.Zdiv.Zmod");
-   *)
-   "Pervasives.=", (2, "(fun _y _z => isTrue (_y = _z))");
-   "Pervasives.<>", (2, "(fun _y _z => isTrue (_y <> _z))");
-   "Pervasives.<", (2, "(fun _y _z => isTrue (_y < _z))");
-   "Pervasives.<=", (2, "(fun _y _z => isTrue (_y <= _z))");
-   "Pervasives.>", (2, "(fun _y _z => isTrue (_y > _z))");
-   "Pervasives.>=", (2, "(fun _y _z => isTrue (_y >= _z))");
-   "Pervasives.max", (2, "(fun _y _z => Zmin (_y >= _z))");
-   "Pervasives.min", (2, "(fun _y _z => isTrue (_y >= _z))");
-   "Pervasives.not", (1, "LibBool.neg");
-   "Pervasives.fst", (1, "(@fst _ _)");
-   "Pervasives.snd", (1, "(@snd _ _)");
-   "Pervasives.@", (2, "LibList.append");
-   "List.rev", (1, "LibList.rev"); 
-   "List.length", (1, "LibList.length"); 
-   "List.append", (2, "LibList.append"); 
-   "OkaStream.++", (2, "LibList.append"); 
-   "OkaStream.reverse", (1, "LibList.rev");
-   "Lazy.force", (1, ""); (* i.e., @LibLogic.id _*)
-   "Okasaki.!$", (1, ""); (* i.e., @LibLogic.id _*)
-   "StrongPointers.cast", (1, "")
+      (*
+      "Pervasives./", (primitive_special, "Coq.ZArith.Zdiv.Zdiv");
+      "Pervasives.mod", (primitive_special, "Coq.ZArith.Zdiv.Zmod");
+      *)
+      (*
+      "Pervasives.=", (2, "(fun _y _z => isTrue (_y = _z))");
+      "Pervasives.<>", (2, "(fun _y _z => isTrue (_y <> _z))");
+      "Pervasives.<", (2, "(fun _y _z => isTrue (_y < _z))");
+      "Pervasives.<=", (2, "(fun _y _z => isTrue (_y <= _z))");
+      "Pervasives.>", (2, "(fun _y _z => isTrue (_y > _z))");
+      "Pervasives.>=", (2, "(fun _y _z => isTrue (_y >= _z))");
+      "Pervasives.max", (2, "(fun _y _z => Zmin (_y >= _z))");
+      "Pervasives.min", (2, "(fun _y _z => isTrue (_y >= _z))");
+      "Pervasives.not", (1, "LibBool.neg");
+      "Pervasives.fst", (1, "(@fst _ _)");
+      "Pervasives.snd", (1, "(@snd _ _)");
+      "Pervasives.@", (2, "LibList.append");
+      "List.rev", (1, "LibList.rev"); 
+      "List.length", (1, "LibList.length"); 
+      "List.append", (2, "LibList.append"); 
+      "OkaStream.++", (2, "LibList.append"); 
+      "OkaStream.reverse", (1, "LibList.rev");
+      "StrongPointers.cast", (1, "")
+      "Lazy.force", (1, "");
+      "Okasaki.!$", (1, ""); (* i.e., @LibLogic.id _*)
+      *)
    ]
-   (* --todo: add asr, etc.. *)
 
 (*#########################################################################*)
 (* ** List of all primitives *)
@@ -65,7 +66,8 @@ let inlined_primitives_table =
     Coq constants whose specification is axiomatized. *)
 
 let all_primitives_table =
-  [ "Pervasives.=", "ml_eqb";
+  [ 
+  (* "Pervasives.=", "ml_eqb";
     "Pervasives.<>", "ml_neq";
     "Pervasives.==", "ml_phy_eq";
     "Pervasives.!=", "ml_phy_neq";
@@ -121,7 +123,9 @@ let all_primitives_table =
     "NullPointers.free", "ml_free";
     "StrongPointers.sref", "ml_ref";    
     "StrongPointers.sget", "ml_get";
-    "StrongPointers.sset", "ml_sset"; ]
+    "StrongPointers.sset", "ml_sset";
+    *)
+   ]
     (* ---todo: add not, fst, snd *)
 
 

generator/print_coq.ml

@@ -130,8 +130,13 @@ let binding x t =
 let rec expr0 = function
   | Coq_var s ->
       string s
+  | Coq_nat n ->
+      parens (string (string_of_int n)) ^^ string "%nat"
   | Coq_int n ->
       parens (string (string_of_int n)) ^^ string "%Z"
+  | Coq_list cs ->
+      if (cs = []) then string "nil" else 
+        parens ((separate_map (string "::" ^^ break 1) expr0 cs) ^^ string "::nil")
   | Coq_wild ->
       string "_"
   | Coq_prop ->
@@ -390,7 +395,7 @@ let top = function
       brackets (flow_map space implicit xs)
       ^^ dot
   | Coqtop_register (db, x, v) ->
-      sprintf "Hint Extern 1 (Register %s %s) => Provide %s." db x v
+      sprintf "Hint Extern 1 (Register %s %s) => CFPrint_Provide %s." db x v
   | Coqtop_hint_constructors (xs, base) ->
       string "Hint Constructors " ^^
       flow_map space string xs ^^

lib/coq/CFPrint.v

 Set Implicit Arguments.
-Require Import CFHeaps CFApp.
+Require Import CFHeaps.
+Require Export CFApp.
 
 
 (** The idea is to tag nodes of the formulae with identity predicates