Commit e04c208a authored by charguer's avatar charguer

polymorphic_eq_constructors

parent 78e95944
......@@ -315,7 +315,7 @@ let lazyop_mixed () =
(********************************************************************)
(* ** Comparison operators *)
(* ** Comparison operators and polymorphic equality *)
let compare_int () =
(1 <> 0 && 1 <= 2) || (0 = 1 && 1 >= 2 && 1 < 2 && 2 > 1)
......@@ -338,6 +338,19 @@ let compare_poly () =
let f () = 4 in
let _r5 = ((Some f, None) = (None, Some f)) in *)
type 'a compare_poly_type =
| CompCst
| CompPoly of 'a
| CompTuple of 'a * bool
| CompFunc of ('a -> 'a)
let compare_poly_custom (x : 'a compare_poly_type) (y : int compare_poly_type) =
let _r1 = (x = CompCst) in
let _r2 = (y = CompPoly 3) in
let _r3 = (y = CompPoly 3) in
let _r4 = (y = CompTuple (3, true)) in
()
let compare_physical_loc_func () =
let r1a = ref 1 in
let r1b = ref 1 in
......
......@@ -3,12 +3,7 @@ Set Implicit Arguments.
Require Import CFLib.
Require Import Demo_ml.
Require Import Stdlib.
Open Scope tag_scope. (**)
Ltac xcur :=
cfml_get_precondition tt.
Open Scope tag_scope.
......@@ -644,6 +639,18 @@ Proof using.
xrets~.
Qed.
Lemma compare_poly_custom_spec : forall (A:Type),
forall (x:compare_poly_type_ A) (y : compare_poly_type_ int),
app compare_poly_custom [x y] \[] \[=tt].
Proof using.
xcf.
xapp. xpolymorphic_eq. intro_subst.
xapp. xpolymorphic_eq. intro_subst.
xapp. xpolymorphic_eq. intro_subst.
xapp. xpolymorphic_eq. intro_subst.
xrets~.
Qed.
Lemma compare_physical_loc_func_spec :
app compare_physical_loc_func [tt] \[] \[= tt].
Proof using.
......
type 'a vector = {
mutable default : 'a;
mutable size : int;
mutable data : 'a array;
}
let length t =
t.size
let default t =
t.default
let make size def =
(* assert (size >= 0); *)
{ default = def;
size;
data = Array.make size def;
}
let init size default f =
(* assert (size >= 0); *)
{ default;
size;
data = Array.init size f;
}
let get t i =
(* assert (i >= 0 && i < t.size); *)
t.data.(i)
let set t i v =
(* assert (i >= 0 && i < t.size); *)
t.data.(i) <- v
let transfer src dst nb =
for i = 0 to nb - 1 do
dst.(i) <- src.(i);
done
(* Distinguer le resize_extacly & resize_at_least *)
(* Option de remplir avec default quand on shrink *)
(* set_physical_size *)
(* get_physical_size *)
let resize t new_capa =
(* assert (new_capa >= 0); *)
let old_data = t.data in
t.data <- Array.make new_capa t.default;
transfer old_data t.data t.size
let push t x =
let capa = Array.length t.data in
if t.size = capa then
resize t (2 * (capa + 1));
t.data.(t.size) <- x;
t.size <- t.size + 1
(* TODO: Return option *)
let pop t =
(* assert (t.size > 0); *)
t.size <- t.size - 1;
let x = t.data.(t.size) in
let capa = Array.length t.data in
if (capa > 4) && (t.size <= capa / 4) then
resize t (capa / 2);
x
let is_empty t =
t.size = 0
let copy t =
{ default = t.default;
size = t.size;
data = Array.copy t.data;
}
let to_array t =
let s = length t in
Array.init s (fun i -> get t i)
let of_array default a =
{ default;
size = Array.length a;
data = Array.copy a;
}
type 'a compare_poly_type =
| CompCst
| CompPoly of 'a
| CompTuple of 'a * bool
| CompFunc of ('a -> 'a)
let compare_poly_custom (x : 'a compare_poly_type) (y : int compare_poly_type) =
let _r1 = (x = CompCst) in
let _r2 = (y = CompPoly 3) in
let _r3 = (y = CompPoly 3) in
let _r4 = (y = CompTuple (3, true)) in
()
......@@ -1363,13 +1363,36 @@ and cfg_algebraics decls =
| [] -> []
| _ -> List.map (fun (cname,_) -> Coqtop_implicit (cname, List.map (fun p -> p,Coqi_maximal) params)) branches
in
(coqind_decl, implicit_decl)
let build_polyeq_axioms (c,ts) =
let axiom_name = polymorphic_eq_arg_name c in
let axiom_type =
let pred = Coq_var "CFML.CFBuiltin.polymorphic_eq_arg" in
let arg_names_typs = list_mapi (fun i t ->
(variable_generated_name i, lift_typ_exp loc t)) ts in
let arg_names = List.map fst arg_names_typs in
let hyps = List.map (fun x -> Coq_app(pred, Coq_var x)) arg_names in
let conc_value = coq_app_var_at c ((List.map coq_var params) @ (List.map coq_var arg_names)) in
(* let conc_value = Coq_annot(coq_apps (Coq_var c) (List.map coq_var arg_names) , ret_typ) *)
let conc = Coq_app (pred, conc_value) in
coq_forall_types params (coq_foralls arg_names_typs (coq_impls hyps conc))
in
let inds,maxiss = List.split (List.map trans_ind decls) in
[ Coqtop_param (axiom_name, axiom_type);
Coqtop_hint_resolve ([axiom_name], "polymorphic_eq"); ] in
(* Example for "Some":
Axiom polymorphic_eq_arg_some : forall A (v:A),
polymorphic_eq_arg v ->
polymorphic_eq_arg (Some v).
Hint Resolve polymorphic_eq_arg_some : polymorphic_eq.
*)
let polyeq_axioms = List.map build_polyeq_axioms branches in
(coqind_decl, (implicit_decl @ List.concat polyeq_axioms))
in
let inds,tops = List.split (List.map trans_ind decls) in
[ Coqtop_ind inds ]
@ (List.concat maxiss)
@ (List.concat tops)
@ [ Coqtop_hint_constructors (List.map (fun i -> i.coqind_name) inds, "typeclass_instances") ]
(** Generate the top-level Coq declarations associated with
a type definition. *)
......
......@@ -54,7 +54,9 @@ type coqtop =
| Coqtop_label of var * int
| Coqtop_implicit of var * (var * implicit) list
| Coqtop_register of string * var * var
(* todo: factorize the 3 type of hints into a single constructor *)
| Coqtop_hint_constructors of vars * var
| Coqtop_hint_resolve of vars * var
| Coqtop_hint_unfold of vars * var
| Coqtop_require of vars
| Coqtop_import of vars
......@@ -177,6 +179,11 @@ let coq_app_wilds c n =
let coq_app_var_wilds x n =
if n = 0 then Coq_var x else coq_app_wilds (coq_var_at x) n
(** Applications of an at-identifier to arguments *)
let coq_app_var_at x args =
if args = [] then Coq_var x else coq_apps (coq_var_at x) args
(** Function [fun (x1:T1) .. (xn:Tn) => c] *)
let coq_funs args c =
......@@ -187,11 +194,13 @@ let coq_funs args c =
let coq_fun_types names c =
coq_funs (coq_types names) c
(** Let binding [let (x:T) := t1 in t2] *)
(** Let binding [let (x:T) := t1 in t2]
TODO
let coq_foralls args c =
List.fold_right (fun ci acc -> Coq_forall (ci, acc)) args c
*)
(** Universal [forall (x1:T1) .. (xn:Tn), c] *)
let coq_foralls args c =
......
......@@ -98,12 +98,12 @@ let rec coqtops_of_imp_cf cf =
| Cf_let_poly (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 p1_on_tvars = coq_app_var_at "P1" tvars in
let p1_on_arg = Coq_app (p1_on_tvars, Coq_var "_r") in
let h1 = Coq_var "H1" in
let q1 = Coq_fun (("_r",typ), heap_star (heap_pred p1_on_arg) h1) in
let c1 = coq_forall_types (fvs_strict @ fvs_other) (coq_apps (coq_of_cf cf1) [h;q1]) in
let x_on_tvars = if tvars = [] then Coq_var x else coq_apps (coq_var_at x) tvars in
let x_on_tvars = coq_app_var_at x tvars in
let hyp_on_x = coq_forall_types fvs_strict (coq_apps (coq_var_at "P1") (tvars @ [ x_on_tvars ])) in
let c2 = coq_foralls [x,type_of_x] (Coq_impl (hyp_on_x, coq_apps (coq_of_cf cf2) [h1;q])) in
let type_of_p1 = coq_forall_types fvs_strict (coq_pred typ) in
......@@ -339,8 +339,8 @@ let coqtops_of_cftop coq_of_cf cft =
| Cftop_pure_cf (x,fvs_strict,fvs_other,cf) ->
let type_of_p = coq_forall_types fvs_strict wild_to_prop in
let p_applied = if fvs_strict = [] then Coq_var "P" else coq_apps (Coq_var "@P") (coq_vars fvs_strict) in
let x_applied = if fvs_strict = [] then Coq_var x else coq_apps (Coq_var ("@" ^ x)) (coq_vars fvs_strict) in
let p_applied = coq_app_var_at "P" (coq_vars fvs_strict) in
let x_applied = coq_app_var_at x (coq_vars fvs_strict) in
let cf_body = coq_foralls ["P", type_of_p] (Coq_impl (Coq_app (coq_of_cf cf, p_applied), Coq_app (p_applied, x_applied))) in
let hyp = coq_forall_types (fvs_strict @ fvs_other) cf_body in
let t = coq_tag "tag_top_val" hyp in
......
......@@ -409,6 +409,12 @@ let top = function
spacecolon ^/^
string base
^^ dot
| Coqtop_hint_resolve (xs, base) ->
string "Hint Resolve " ^^
flow_map space string xs ^^
spacecolon ^/^
string base
^^ dot
| Coqtop_hint_unfold (xs, base) ->
string "Hint Unfold " ^^
flow_map space string xs ^^
......
......@@ -496,6 +496,12 @@ let module_name name =
let record_type_name name =
type_constr_name name (* TODO: inline *)
(** Convention for naming the axiom for polymorphic equality
on constructors *)
let polymorphic_eq_arg_name name =
"polymorphic_eq_arg_" ^ name ^ "__"
(** Convention for naming the coq record structure
used to describe a record in the heap *)
......
......@@ -148,6 +148,18 @@ Ltac cfml_show_app_type_concl S :=
(********************************************************************)
(* ** Simplification, Automation, and Cleaning *)
(*--------------------------------------------------------*)
(* ** [xcur] *)
(** [xcur] is a convenient way to obtain the current precondition.
Syntax is: [let H := xcur in ...].
Example: [let H := xcur in xif (\[= 3] \*+ H) ].
*)
Ltac xcur :=
cfml_get_precondition tt.
(*--------------------------------------------------------*)
(* ** [xclean] *)
......
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