Commit 38377bdd authored by charguer's avatar charguer
Browse files

interfaces

parent 642ef5d2
......@@ -13,3 +13,8 @@ clean:
rm -rf _build
rm -f *.native
rm -f *~
# Note: to generate mli files, run the following command from ./_build:
# ocamlc -I typing -I utils -I tools -I parsing -I lex -I /usr/local/lib/ocaml/4.01.0/pprint/ -i normalize.ml > ../normalize.mli
......@@ -15,8 +15,6 @@ open Printf
(*#########################################################################*)
(* ** Switch for generating formulae for purely-functional programs *)
let pure_mode = ref false
let use_credits = ref false
......@@ -580,7 +578,7 @@ let rec cfg_exp env e =
let fvs_strict = list_intersect fvs fvs_typ in
let fvs_others = list_minus fvs fvs_strict in
(* pure-mode let-binding *)
(* deprecated: pure-mode let-binding
if !pure_mode then begin
let cf1 = cfg_exp env bod in
......@@ -588,9 +586,10 @@ let rec cfg_exp env e =
let cf2 = cfg_exp env' body in
add_used_label x;
Cf_letpure (x, fvs_strict, fvs_others, typ, cf1, cf2)
end else *)
(* value let-binding *)
end else if Typecore.is_nonexpansive bod then begin
if Typecore.is_nonexpansive bod then begin
let v =
try lift_val env bod
......@@ -775,7 +774,7 @@ let rec cfg_structure_item s : cftops =
let fvs_strict = list_intersect fvs fvs_typ in
let fvs_others = list_minus fvs fvs_strict in
(* pure-mode let-binding *)
(* deprecated: pure-mode let-binding
if !pure_mode then begin
let cf_body = cfg_exp (Ident.empty) bod in
......@@ -788,9 +787,10 @@ let rec cfg_structure_item s : cftops =
Cftop_coqs implicits;
Cftop_pure_cf (x, fvs_strict, fvs_others, cf_body);
Cftop_coqs [register_cf x]; ]
end else*)
(* value let-binding *)
end else if Typecore.is_nonexpansive bod then begin
if Typecore.is_nonexpansive bod then begin
let v =
try lift_val (Ident.empty) bod
......@@ -1347,7 +1347,8 @@ and cfg_module id m =
let cfg_file str =
[ Cftop_coqs ([
Coqtop_set_implicit_args;
Coqtop_require_import (if !pure_mode then "FuncPrim" else "CFHeader") ]
Coqtop_require_import "CFHeader" ]
@ (external_modules_get_coqtop())) ]
@ cfg_structure str
(*deprecated: (if !pure_mode then "FuncPrim" else "CFHeader") *)
\ No newline at end of file
val use_credits : bool ref
(*
val external_modules : string list ref
val external_modules_add : string -> unit
val external_modules_get_coqtop : unit -> Coq.coqtop list
val external_modules_reset : unit -> unit
val lift_ident_name : Ident.t -> string
val lift_full_path : Path.t -> Path.t
val lift_path : Path.t -> Path.t
val lift_full_path_name : Path.t -> string
val lift_path_name : Path.t -> string
val record_type_name : string -> string
val record_constructor : string -> string
val fv_btyp : ?through_arrow:bool -> Print_type.btyp -> string list
val lift_btyp : Print_type.btyp -> Coq.coq
val lift_typ_exp : Types.type_expr -> Coq.coq
val lift_typ_sch : Types.type_expr -> string list * Coq.coq
val coq_typ : Typedtree.expression -> Coq.coq
val coq_typ_pat : Typedtree.pattern -> Coq.coq
val path_decompose : Path.t -> string * string
val get_record_decomposed_name_for_exp :
Typedtree.expression -> string * string
val typ_arity_var : int Ident.tbl -> Path.t -> int
val typ_arity_constr : Types.constructor_description -> int
val coq_of_constructor : Path.t -> Types.constructor_description -> Coq.coq
val pattern_variables : Typedtree.pattern -> Coq.typed_vars
val lift_pat : ?through_aliases:bool -> Typedtree.pattern -> Coq.coq
val pattern_aliases : Typedtree.pattern -> (Coq.typed_var * Coq.coq) list
val register_cf : Coq.var -> Coq.coqtop
val register_spec : Coq.var -> Coq.var -> Coq.coqtop
val prefix_for_label : Types.type_expr -> string
val string_of_label_with : string -> Types.label_description -> string
val name_for_record_new : string -> string
val name_for_record_get : Types.label_description -> string
val name_for_record_set : Types.label_description -> string
val string_of_label : Types.type_expr -> Types.label_description -> string
val simplify_apply_args :
('a * 'b option * Typedtree.optional) list -> 'b list
val exp_find_inlined_primitive :
Typedtree.expression ->
('a * Typedtree.expression option * Typedtree.optional) list ->
string option
val exp_is_inlined_primitive :
Typedtree.expression ->
('a * Typedtree.expression option * Typedtree.optional) list -> bool
val exp_get_inlined_primitive :
Typedtree.expression ->
('a * Typedtree.expression option * Typedtree.optional) list -> string
val lift_exp_path : int Ident.tbl -> Path.t -> Coq.coq
val lift_val : int Ident.tbl -> Typedtree.expression -> Coq.coq
val counter_local_label : int ref
val get_next_local_label : unit -> string
val reset_local_labels : unit -> unit
val used_labels : Coq.var list ref
val reset_used_labels : unit -> unit
val add_used_label : Coq.var -> unit
val cfg_extract_labels : unit -> Formula.cftop list
val pattern_ident : Typedtree.pattern -> Ident.t
val pattern_name : Typedtree.pattern -> string
val extract_label_names_simple : Env.t -> Types.type_expr -> string list
val cfg_exp : int Ident.tbl -> Typedtree.expression -> Formula.cf
val cfg_func :
int Ident.tbl ->
Typedtree.free_vars ->
Typedtree.pattern -> Typedtree.expression -> Formula.cf
val is_algebraic : 'a * Typedtree.type_declaration -> bool
val is_type_abbrev : 'a * Typedtree.type_declaration -> bool
val is_type_record : 'a * Typedtree.type_declaration -> bool
val cfg_structure_item : Typedtree.structure_item -> Formula.cftops
val cfg_type_abbrev :
Ident.t * Typedtree.type_declaration -> Coq.coqtop list * Coq.coqtop list
val cfg_type_record :
Ident.t * Typedtree.type_declaration -> Coq.coqtop list * Coq.coqtop list
val record_functions :
string ->
string ->
Coq.var -> Coq.var list -> string list -> Coq.coq list -> Coq.coqtop list
val cfg_algebraic :
(Ident.t * Typedtree.type_declaration) list ->
Coq.coqtop list * Coq.coqtop list
val cfg_type_decls :
(Ident.t * Typedtree.type_declaration) list -> Coq.coqtops
val cfg_structure : Typedtree.structure -> Formula.cftop list
val cfg_signature_item : Typedtree.signature_item -> Coq.coqtops
val cfg_signature : Typedtree.signature -> Coq.coqtop list
val cfg_modtype : Ident.t -> Typedtree.module_type -> Formula.cftops
val cfg_module : Ident.t -> Typedtree.module_expr -> Formula.cftops
*)
val cfg_file : Typedtree.structure -> Formula.cftop list
open Coq
open Mytools
(** This file contains a data structure for representing characteristic
formulae. Such data is constructed in file [characteristic.ml] from
the typed abstract syntax tree, and is converted into a Coq expression
(as described in [coq.ml]), using an algorithm contained in this file. *)
(*#########################################################################*)
(* ** Syntax of characteristic formulae *)
(** Characteristic formulae for terms *)
type cf =
| Cf_ret of coq
(* Ret v *)
Cf_ret of coq
| Cf_fail
(* Fail *)
| Cf_assert of cf
(* Assert Q *)
| Cf_done
(* Done *)
| Cf_app of coqs * coq * coqs
(* App f Ai xi *)
| Cf_app of coqs * coq * coqs
| Cf_body of var * vars * typed_vars * coq * 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
(* Let x [Ai,Bi] := Q1 in Q2 // where x : forall Ai.T *)
| Cf_letval of var * vars * vars * coq * coq * cf
(* Let x [Ai,Bi] := v in Q2 // where x : forall Ai.T *)
| Cf_letfunc of (var * cf) list * cf
(* Let fi := Qi in Q *)
(* old
| Cf_caseif of cf * cf * cf
(* If Q0 Then Q1 else Q2 *)
*)
| Cf_caseif of coq * cf * cf
(* If v Then Q1 else Q2 *)
| Cf_case of coq * typed_vars * coq * coq option * (typed_var*coq) list * cf * cf
(* Case v [xi] p [When c] Then (Alias yk = vk in Q1) else Q2 *)
| Cf_let of typed_var * cf * cf
| Cf_letpure of var * vars * vars * coq * cf * cf
| Cf_letval of var * vars * vars * coq * coq * cf
| Cf_letfunc of (var * cf) list * cf
| Cf_caseif of coq * cf * cf
| Cf_case of coq * typed_vars * coq * coq option *
(typed_var * coq) list * cf * cf
| Cf_match of var * int * cf
(* Match ?lab n Q *)
| Cf_seq of cf * cf
(* Q1 ;; Q2 *)
| Cf_for of var * coq * coq * cf
(* for i = v1 to v2 do Q done *)
| Cf_for of var * coq * coq * cf
| Cf_while of cf * cf
(* while Q1 do Q2 done *)
| Cf_manual of coq
(* Q *)
| Cf_manual of coq
| Cf_pay of cf
(* Pay; Q *)
(** Characteristic formulae for top-level declarations *)
type cftop =
| Cftop_val of typed_var
(* Lemma x_safe : Inhab t. Proof. typeclass. Qed.
Parameter x : t. *)
type cftop =
Cftop_val of typed_var
| Cftop_heap of var
(* Parameter h : heap. *)
| Cftop_pure_cf of var * vars * vars * cf
(* Parameter x_cf : forall Ai Bi P, F (P Ai) -> P Ai (x Ai) *)
| Cftop_val_cf of var * vars * vars * coq
(* Parameter x_cf: forall Ai, x = V *)
| Cftop_let_cf of var * var * var * cf
(* Parameter x_cf : forall H Q, H h -> F H Q -> Q x h' *)
| Cftop_pure_cf of var * vars * vars * cf
| Cftop_val_cf of var * vars * vars * coq
| Cftop_let_cf of var * var * var * cf
| Cftop_fun_cf of var * cf
(* Parameter f_cf : Val := H *)
| Cftop_coqs of coqtops
(* arbitrary coq top-level commands *)
and cftops = cftop list
(*#########################################################################*)
(* ** Shared functions *)
......@@ -194,123 +159,11 @@ let heap_pred c =
Coq_app (Coq_var "heap_is_empty_st", c)
(*#########################################################################*)
(* ** Conversion of PURE characteristic formulae to Coq *)
let rec coq_of_pure_cf cf =
let coq_of_cf = coq_of_pure_cf in
let p = Coq_var "P" in
let funp tag ?label c =
let f = coq_funs ["P", wild_to_prop] c in
match label with
| None -> coq_tag tag f
| Some x -> coq_tag tag ~label:x f
in (* todo improve *)
match cf with
| Cf_ret v -> funp "tag_ret" (Coq_app (p, v))
| Cf_assert cf -> coq_of_cf cf
| Cf_fail -> funp "tag_fail" coq_false
| Cf_done -> funp "tag_done" coq_true
| Cf_app (ts, f, vs) ->
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_body (f, fvs, targs, typ, cf) ->
let type_of_k = coq_impls ((List.map snd targs) @ [coq_pred wild_to_prop]) Coq_prop in (* TODO: wild_to_prop should be typ to prop *)
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
let sarity = string_of_int (List.length targs) in
let spec_n = Coq_var ("spec_" ^ sarity) in
let is_spec_k = Coq_app (Coq_var ("is_spec_" ^ sarity), var_k) in
let hyp_k = coq_foralls targs (coq_apps var_k args_of_k) in
let concl_k = coq_apps spec_n [var_k; coq_var f] in
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 Q) -> spec_2 K f)) *)
| 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)) *)
| Cf_letfunc (ncs, cf) ->
let ns, cs = List.split ncs in
let p_of n = "P" ^ n in
let fs = List.map (fun n -> (n, val_type)) ns in
let ps = List.map (fun n -> (p_of n, coq_pred val_type)) ns in
let c1hyps = List.map coq_of_cf cs in
let c1conc = coq_conjs (List.map (fun n -> Coq_app (Coq_var (p_of n), Coq_var n)) ns) in
let c1 = coq_impls c1hyps c1conc in
let c2hyps = List.map (fun n -> Coq_app (Coq_var (p_of n), Coq_var n)) ns in
let c2conc = Coq_app (coq_of_cf cf, p) in
let c2 = coq_impls c2hyps c2conc in
let x = List.hd ns in
funp "tag_letfun" ~label:x (coq_foralls fs (coq_exists ps (coq_conj c1 c2)))
(* (!F a: fun P => forall f1 f2, exists P1 P2,
(Q1 -> Q2 -> P1 f1 /\ P2 f2) /\ (P1 f1 -> P2 f2 -> Q P)) *)
| Cf_caseif (v,cf1,cf2) ->
(* todo: update with cf0
assert false
*)
let c1 = Coq_impl (coq_eq v (Coq_var "true"), Coq_app (coq_of_cf cf1, p)) in
let c2 = Coq_impl (coq_eq v (Coq_var "false"), Coq_app (coq_of_cf cf2, p)) in
funp "tag_if" (coq_conj c1 c2)
(* (!I a: (fun P => (x = true -> Q1 P) /\ (x = false -> Q2 P))) *)
| Cf_case (v,tps,pat,vwhenopt,aliases,cf1,cf2) ->
let add_alias ((name,typ),exp) cf : coq =
funp "tag_alias" (coq_foralls [name,typ] (coq_impls [coq_eq (Coq_var name) exp] (Coq_app (cf, p))))
(* !L a: (fun P => forall y, y = v -> Q P) *)
in
let cf1_aliased = List.fold_right add_alias aliases (coq_of_cf cf1) in
let same = coq_eq v pat in
let same_when = match vwhenopt with None -> [same] | Some w -> [same; w] in
let c1 = coq_foralls tps (coq_impls same_when (Coq_app (cf1_aliased, p))) in
let diff = coq_neq v pat in
let diff_when = match vwhenopt with None -> diff | Some w -> coq_disj diff (coq_neg w) in
let c2 = Coq_impl (coq_foralls tps diff_when, Coq_app (coq_of_cf cf2, p)) in
let tag = match vwhenopt with None -> "tag_case" | Some w -> "tag_casewhen" in
funp tag (coq_conj c1 c2)
(* (!C a: (fun P => (forall x1, x = p [-> trueb w] -> (!L a: y := v in Q1) P)
/\ ((forall x1, x <> p [\/ trueb !w]) -> Q2 P)))
where trueb are implicit by coercions *)
| Cf_match (label, n,cf1) ->
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"
| Cf_let _ -> unsupported "let-expression in pure mode"
| Cf_letval _ -> unsupported "letval-expression in pure mode"
(*#########################################################################*)
(* ** Conversion of IMPERATIVE characteristic formulae to Coq *)
let rec coq_of_imp_cf cf =
let coq_of_cf = coq_of_imp_cf in
let rec coqtops_of_imp_cf cf =
let coq_of_cf = coqtops_of_imp_cf in
let h = Coq_var "H" in
let q = Coq_var "Q" in
let funhq tag ?label ?rettype c =
......@@ -567,6 +420,134 @@ let coqtops_of_cftop coq_of_cf cft =
| Cftop_coqs cmds -> cmds
let coqtops_of_cftops coq_of_cf cfts =
list_concat_map (coqtops_of_cftop coq_of_cf) cfts
(*#########################################################################*)
(** Main entry point *)
let coqtops_of_cftops cfts =
list_concat_map (coqtops_of_cftop coqtops_of_imp_cf) cfts
(*#########################################################################*)
(* ** Conversion of PURE characteristic formulae to Coq *)
(* DEPRECATED *)
let rec coqtops_of_pure_cf cf =
let coq_of_cf = coqtops_of_pure_cf in
let p = Coq_var "P" in
let funp tag ?label c =
let f = coq_funs ["P", wild_to_prop] c in
match label with
| None -> coq_tag tag f
| Some x -> coq_tag tag ~label:x f
in (* todo improve *)
match cf with
| Cf_ret v -> funp "tag_ret" (Coq_app (p, v))
| Cf_assert cf -> coq_of_cf cf
| Cf_fail -> funp "tag_fail" coq_false
| Cf_done -> funp "tag_done" coq_true
| Cf_app (ts, f, vs) ->
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_body (f, fvs, targs, typ, cf) ->
let type_of_k = coq_impls ((List.map snd targs) @ [coq_pred wild_to_prop]) Coq_prop in (* TODO: wild_to_prop should be typ to prop *)
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
let sarity = string_of_int (List.length targs) in
let spec_n = Coq_var ("spec_" ^ sarity) in
let is_spec_k = Coq_app (Coq_var ("is_spec_" ^ sarity), var_k) in
let hyp_k = coq_foralls targs (coq_apps var_k args_of_k) in
let concl_k = coq_apps spec_n [var_k; coq_var f] in
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 Q) -> spec_2 K f)) *)
| 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)) *)
| Cf_letfunc (ncs, cf) ->
let ns, cs = List.split ncs in
let p_of n = "P" ^ n in
let fs = List.map (fun n -> (n, val_type)) ns in
let ps = List.map (fun n -> (p_of n, coq_pred val_type)) ns in
let c1hyps = List.map coq_of_cf cs in
let c1conc = coq_conjs (List.map (fun n -> Coq_app (Coq_var (p_of n), Coq_var n)) ns) in
let c1 = coq_impls c1hyps c1conc in
let c2hyps = List.map (fun n -> Coq_app (Coq_var (p_of n), Coq_var n)) ns in
let c2conc = Coq_app (coq_of_cf cf, p) in
let c2 = coq_impls c2hyps c2conc in
let x = List.hd ns in
funp "tag_letfun" ~label:x (coq_foralls fs (coq_exists ps (coq_conj c1 c2)))
(* (!F a: fun P => forall f1 f2, exists P1 P2,
(Q1 -> Q2 -> P1 f1 /\ P2 f2) /\ (P1 f1 -> P2 f2 -> Q P)) *)
| Cf_caseif (v,cf1,cf2) ->
(* todo: update with cf0
assert false
*)
let c1 = Coq_impl (coq_eq v (Coq_var "true"), Coq_app (coq_of_cf cf1, p)) in
let c2 = Coq_impl (coq_eq v (Coq_var "false"), Coq_app (coq_of_cf cf2, p)) in
funp "tag_if" (coq_conj c1 c2)
(* (!I a: (fun P => (x = true -> Q1 P) /\ (x = false -> Q2 P))) *)
| Cf_case (v,tps,pat,vwhenopt,aliases,cf1,cf2) ->
let add_alias ((name,typ),exp) cf : coq =
funp "tag_alias" (coq_foralls [name,typ] (coq_impls [coq_eq (Coq_var name) exp] (Coq_app (cf, p))))
(* !L a: (fun P => forall y, y = v -> Q P) *)
in
let cf1_aliased = List.fold_right add_alias aliases (coq_of_cf cf1) in
let same = coq_eq v pat in
let same_when = match vwhenopt with None -> [same] | Some w -> [same; w] in
let c1 = coq_foralls tps (coq_impls same_when (Coq_app (cf1_aliased, p))) in
let diff = coq_neq v pat in
let diff_when = match vwhenopt with None -> diff | Some w -> coq_disj diff (coq_neg w) in
let c2 = Coq_impl (coq_foralls tps diff_when, Coq_app (coq_of_cf cf2, p)) in
let tag = match vwhenopt with None -> "tag_case" | Some w -> "tag_casewhen" in
funp tag (coq_conj c1 c2)
(* (!C a: (fun P => (forall x1, x = p [-> trueb w] -> (!L a: y := v in Q1) P)
/\ ((forall x1, x <> p [\/ trueb !w]) -> Q2 P)))
where trueb are implicit by coercions *)
| Cf_match (label, n,cf1) ->
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"
| Cf_let _ -> unsupported "let-expression in pure mode"
| Cf_letval _ -> unsupported "letval-expression in pure mode"
open Coq
(** This module contains a data structure for representing characteristic
formulae. Such data is constructed in file [characteristic.ml] from
the typed abstract syntax tree, and is converted into a Coq expression
(as described in [coq.ml]), using an algorithm contained in this file. *)
(** Characteristic formulae for terms *)
type cf =
| Cf_ret of coq
(* Ret v *)
| Cf_fail
(* Fail *)
| Cf_assert of cf
(* Assert Q *)
| Cf_done
(* Done *)
| Cf_app of coqs * coq * coqs
(* App f Ai xi *)
| Cf_body of var * vars * typed_vars * coq * 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
(* Let x [Ai,Bi] := Q1 in Q2 // where x : forall Ai.T *)
| Cf_letval of var * vars * vars * coq * coq * cf
(* Let x [Ai,Bi] := v in Q2 // where x : forall Ai.T *)
| Cf_letfunc of (var * cf) list * cf
(* Let fi := Qi in Q *)
| Cf_caseif of coq * cf * cf
(* If v Then Q1 else Q2 *)
| Cf_case of coq * typed_vars * coq * coq option * (typed_var*coq) list * cf * cf
(* Case v [xi] p [When c] Then (Alias yk = vk in Q1) else Q2 *)
| Cf_match of var * int * cf
(* Match ?lab n Q *)
| Cf_seq of cf * cf
(* Q1 ;; Q2 *)
| Cf_for of var * coq * coq * cf
(* for i = v1 to v2 do Q done *)
| Cf_while of cf * cf
(* while Q1 do Q2 done *)
| Cf_manual of coq
(* Q *)
| Cf_pay of cf
(* Pay; Q *)
(* not currently used:
| Cf_caseif of cf * cf * cf
(* If Q0 Then Q1 else Q2 *)
*)
(** Characteristic formulae for top-level declarations *)
type cftop =
| Cftop_val of typed_var
(* Lemma x_safe : Inhab t. Proof. typeclass. Qed.
Parameter x : t. *)
| Cftop_heap of var
(* Parameter h : heap. *)
| Cftop_pure_cf of var * vars * vars * cf
(* Parameter x_cf : forall Ai Bi P, F (P Ai) -> P Ai (x Ai) *)
| Cftop_val_cf of var * vars * vars * coq
(* Parameter x_cf: forall Ai, x = V *)
| Cftop_let_cf of var * var * var * cf
(* Parameter x_cf : forall H Q, H h -> F H Q -> Q x h' *)
| Cftop_fun_cf of var * cf
(* Parameter f_cf : Val := H *)
| Cftop_coqs of coqtops
(* arbitrary coq top-level commands *)
and cftops = cftop list
(** Abstract datatype for functions (func) *)
val val_type : Coq.coq
(** Abstract data type for locations (loc) *)
val loc_type : Coq.coq
(** Abstract data type for heaps *)
val heap : Coq.coq