Commit 9a77f4db authored by charguer's avatar charguer

generator_en_cours

parent 939de4c3
(*#########################################################################*)
(* ** 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"
......@@ -191,7 +191,7 @@ let match_nested () =
(********************************************************************)
(* ** Exceptions *)
(* ** Fatal Exceptions *)
let exn_assert_false () =
assert false
......@@ -205,6 +205,20 @@ let exn_raise () =
raise My_exn
(********************************************************************)
(* ** Assertions *)
let assert_true () =
assert true; 3
let assert_pos x =
assert (x > 0); 3
let assert_same (x:int) (y:int) =
assert (x = y); 3
(********************************************************************)
(* ** Conditionals *)
......@@ -299,5 +313,117 @@ let rec rec_partial_half x =
else 1 + rec_partial_half(x-2)
(********************************************************************)
(* ** External *)
external external_mono : int = "%external_mono"
external external_poly : 'a = "%external_poly"
external external_func : int -> 'a -> 'a array = "%external_func"
(********************************************************************)
(* ** Type abbreviation *)
type type_intpair = (int * int)
type 'a type_homo_pair = ('a * 'a)
type ('a,'b) type_poly_pair = (('a * 'b) * ('a * 'b))
(********************************************************************)
(* ** Type algebraic *)
type 'a alga_three =
| Alga_A
| Alga_B of int * int
| Alga_C of (int * int)
| Alga_D of 'a
| Alga_E of 'a * ('a -> 'a)
type ('a,'b) algb_erase =
| Algb_A of 'a
| Algb_B of int -> 'b
(********************************************************************)
(* ** Type record *)
type recorda = { recorda1 : int; recorda2 : int }
type ('a,'b) recordb = { recorda1 : 'a ; recorda2 : 'b -> 'b }
(********************************************************************)
(* ** Type mutual *)
type typereca1 = | Typereca_1 of typereca2
and typereca2 = | Typereca_2 of typereca1
type typerecb1 = | Typerecb_1 of typerecb2
and typerecb2 = { typerecb_2 : typerecb1 }
(* not supported: recursive definitions using abbreviation
type typerecb1 = | Typerecb_1 of typerecb2
and typerecb2 = typerecb1 list
work around by inlining, e.g.:
*)
type typerecb1 = | Typerecb_1 of typerecb1 list
type typerecb2 = typerecb1 list
(********************************************************************)
(* ** Local module *)
module ModFoo = struct
type t = int
val x : t = 3
end
(********************************************************************)
(* ** Local module signature *)
module type ModBarType = sig
type t
val x : t
end
module ModBar : ModBarType = struct
type t = int
val x : t = 3
end
(********************************************************************)
(* ** Functor *)
module ModFunctor (Bar : ModBarType) = struct
type u = Bar.t
val x : u = Bar.x
end
module ModFunctorTyped (Bar : ModBarType) : ModBarType = struct
type t = Bar.t
val x : t = Bar.x
end
(********************************************************************)
(* ** TODO: import of auxiliary files, like in examples/DemoMake *)
......@@ -646,11 +646,8 @@ let rec cfg_exp env e =
add_used_label label;
Cf_match (label, List.length pat_expr_list, List.fold_right cfg_case pat_expr_list conclu)
| Texp_assert e -> unsupported "general assert expressions"
(*
Printf.printf "Warning: assertions are ignored.\n";
| Texp_assert e ->
Cf_assert (aux e)
*)
| Texp_assertfalse ->
Cf_fail
......@@ -840,9 +837,12 @@ let rec cfg_structure_item s : cftops =
if is_primitive_module (Path.name path) then [] else
[ Cftop_coqs [ Coqtop_require_import (lift_full_path_name path) ] ]
(* -- todo: check no name clash occurs here *)
| Tstr_primitive(id, descr) ->
[]
let id = lift_ident_name id in
let fvs, typ = lift_typ_sch descr.val_desc.ctyp_type in
let typ = coq_fun_types fvs typ in
[ Cftop_val (id, typ) ]
| Tstr_exception(id, decl) ->
[] (* unsupported "exceptions" *)
| Tstr_exn_rebind(id, path) ->
......
......@@ -44,7 +44,7 @@ and cftops = cftop list
(** Abstract datatype for functions *)
let val_type = Coq_var "CFSpec.func"
let val_type = Coq_var "CFApp.func"
(** Abstract data type for locations *)
......@@ -181,14 +181,23 @@ let rec coqtops_of_imp_cf cf =
match cf with
| Cf_ret v -> funhq "tag_ret" (heap_impl h (Coq_app (q,v)))
(* (!R: fun H Q => H ==> Q v *)
| Cf_ret v ->
funhq "tag_ret" (heap_impl h (Coq_app (q,v)))
(* (!R: fun H Q => H ==> Q v *)
| Cf_assert cf -> coq_of_cf cf
| Cf_fail -> funhq "tag_fail" coq_false
| Cf_assert cf1 ->
let p = coq_eq (Coq_var "_b") coq_true in
let q' = Coq_fun (("_b",coq_bool), heap_star (heap_pred p) h) in
let c1 = coq_apps (coq_of_cf cf1) [h;q'] in
let c2 = heap_impl h (Coq_app (q,coq_tt)) in
funhq "tag_assert" (coq_conj c1 c2)
(* (!Assert (fun H Q => F1 H (fun (b:bool) => \[b = true] \* H) /\ H ==> Q tt)) *)
| Cf_fail ->
funhq "tag_fail" coq_false
| Cf_done -> funhq "tag_done" coq_true
| Cf_done ->
funhq "tag_done" coq_true
| Cf_app (ts, f, vs) ->
(* the following is the same as for pure *)
......@@ -431,123 +440,3 @@ let coqtops_of_cftops 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"
Require Export CFPrint.
Require Export LibCore LibListZ LibInt LibSet LibMap.
Require LibCore.
Require Export LibInt.
(* LibCore LibSet LibMap LibListZ *)
This diff is collapsed.
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