Commit db256998 authored by charguer's avatar charguer
Browse files

credits

parent bb3bad34
......@@ -71,7 +71,7 @@ $(CFML)/lib/tools/cfml_dep:
###############################################################################
# Clean
clean_gen:ls
clean_gen:
make -C generator clean
clean_ocamllib:
......
......@@ -17,6 +17,9 @@ open Printf
let pure_mode = ref false
let use_credits = ref false
(*#########################################################################*)
(* ** Error messages *)
......@@ -103,7 +106,7 @@ let rec lift_btyp t =
| Btyp_constr (id,[t]) when Path.name id = "heap" || Path.name id = "Heap.heap" -> (* todo generalize *)
loc_type
| Btyp_constr (id,[t]) when Path.same id Predef.path_lazy_t || Path.name id = "Lazy.t" ->
aux t (* todo: les Lazy provenant des patterns ne sont pas identique Predef.path_lazy_t *)
aux t (* todo: les Lazy provenant des patterns ne sont pas identique Predef.path_lazy_t *)
| Btyp_constr (id,[t]) when Path.name id = "Stream.stream" || Path.name id = "stream" ->
Coq_app (Coq_var "list", aux t)
| Btyp_constr (id,[t]) when Path.name id = "Stream.stream_cell" || Path.name id = "stream_cell" ->
......@@ -557,7 +560,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 pat in
(* todo: une diffrence entre pattern_name et pattern_ident utils plus bas? *)
(* todo: une diffrence entre pattern_name et pattern_ident utils plus bas? *)
let fvs_typ, typ = lift_typ_sch pat.pat_type in
let fvs = List.map name_of_type fvs in
let fvs_strict = list_intersect fvs fvs_typ in
......@@ -699,6 +702,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 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
......
......@@ -50,6 +50,8 @@ type cf =
(* while Q1 do Q2 done *)
| Cf_manual of coq
(* Q *)
| Cf_pay of cf
(* Pay; Q *)
(** Characteristic formulae for top-level declarations *)
......@@ -296,6 +298,7 @@ let rec coq_of_pure_cf cf =
coq_tag (Printf.sprintf "(tag_match %d%snat)" n "%") ~label:label (coq_of_cf cf1)
| Cf_manual c -> c
| Cf_pay _ -> unsupported "seq-expression in pure mode"
| Cf_seq _ -> unsupported "seq-expression in pure mode"
| Cf_for _ -> unsupported "for-expression in pure mode"
| Cf_while _ -> unsupported "while-expression in pure mode"
......@@ -432,7 +435,7 @@ let rec coq_of_imp_cf cf =
funhq "tag_seq" (coq_exist "Q'" wild_to_hprop (coq_conj c1 c2))
(* (!S: fun H Q => exists Q', F1 H Q /\ F2 (Q' tt) Q *)
| Cf_for (i_name,v1,v2,cf) ->
| Cf_for (i_name,v1,v2,cf) ->
let s = Coq_var "S" in
let i = Coq_var i_name in
let typs = Coq_impl (coq_int,formula_type) in
......@@ -471,6 +474,13 @@ let rec coq_of_imp_cf cf =
-> R H Q)
-> R H Q). *)
| Cf_pay (cf1) ->
let h' = Coq_var "H'" in
let c1 = coq_apps (Coq_var "pay_one") [h;h'] in
let c2 = coq_apps (coq_of_cf cf1) [h'; Coq_var "Q"] in
funhq "tag_pay" (coq_exist "H'" hprop (coq_conj c1 c2))
(* (!Pay: fun H Q => exists H', pay_one H H' /\ F1 H' Q *)
(* old:
let r = Coq_var "R" in
let typr = formula_type in
......
......@@ -35,6 +35,7 @@ let _ =
"includes a directory where to look for interface files");
("-pure", Arg.Set Characteristic.pure_mode, "generate formulae for purely-functional code");
("-rectypes", Arg.Set Clflags.recursive_types, "activates recursive types");
("-credits", Arg.Set Characteristic.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");
......
......@@ -2,6 +2,18 @@ Set Implicit Arguments.
Require Import CFSpec.
(* TEMPORARY : move to CFHeaps later *)
Axiom credits : nat -> hprop.
Notation "'\$' n" := (credits n) (at level 40, format "\$ n") : charac.
Definition pay_one H H' :=
H ==> credits 1 \* H'.
(********************************************************************)
(* ** Notation for specifications *)
......@@ -155,7 +167,8 @@ Inductive tag_type : Type :=
| tag_match (n : nat)
| tag_seq
| tag_for
| tag_while.
| tag_while
| tag_pay.
Definition tag (t:tag_type) `{x:Label} (A:Type) (P:A) := P.
......@@ -191,6 +204,8 @@ Notation "'!Seq' P" := (tag tag_seq _ (local P))
(at level 95).
Notation "'!For' P" := (tag tag_for _ (local P))
(at level 95).
Notation "'!Pay' P" := (tag tag_pay _ (local P))
(at level 95).
Notation "'!While' P" := (tag tag_while _ (local P))
(at level 95).
Notation "'!TV' P" := (tag tag_top_val _ (local P))
......@@ -264,7 +279,7 @@ Notation "'App' f x1 x2 x3 x4 ;" :=
Notation "'AppReturns'" := (@app_1 _ _).
(** Let / Seq *)
(** Let / Seq / Pay *)
Notation "'LetVal' x ':=' V 'in' F" :=
(!V (fun H Q => forall x, x = V -> F H Q))
......@@ -291,6 +306,11 @@ Notation "Q1 ;; Q2" :=
(at level 68, right associativity, only parsing,
format "'[v' '[' Q1 ']' ;; '/' '[' Q2 ']' ']'") : charac.
Notation "'Pay_' ;; Q1" :=
(!Seq (fun H Q => exists H', pay_one H H' /\ Q1 H' Q))
(at level 68, right associativity,
format "'[v' 'Pay_' ;; '[' Q1 ']' ']'") : charac.
(** LetApp *)
Notation "'LetApp' x ':=' f x1 'in' F2" :=
......
......@@ -64,6 +64,7 @@ endif
###############################################################################
# Definitions
CMJ := $(patsubst %.ml,%.cmj,$(ML))
MLV := $(patsubst %.ml,%_ml.v,$(ML))
MLVIO := $(patsubst %.ml,%_ml.vio,$(ML))
MLVQ := $(patsubst %.ml,%_ml.vq,$(ML))
......@@ -83,7 +84,7 @@ OCAMLPOST := $(CFML)/lib/make/ocamldep.post
###############################################################################
# Targets
all: $(MLVQ)
all: $(CMJ) $(MLVQ)
###############################################################################
......
# TODO ?
\ No newline at end of file
# todo: put a basic rule to use ocamlc to compile %.ml files into %.out, and to generate %.ml.d using ocamldep, using ocamlinclude variable for dependencies.
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment