Commit d770b304 authored by Martin Clochard's avatar Martin Clochard

BySo: prepare for integration

parent ae434627
......@@ -323,12 +323,12 @@ module TheClassicalSudokuGrid
ss[n72]<-n54; ss[n73]<-n54; ss[n74]<-n54; ss[n75]<-n57; ss[n76]<-n57;
ss[n77]<-n57; ss[n78]<-n60; ss[n79]<-n60; ss[n80]<-n60;
(* square offset *)
let so = Array31.make n9 n0 in
so[n00]<-n00; so[n01]<-n01; so[n02]<-n02; so[n03]<-n09; so[n04]<-n10;
so[n05]<-n11; so[n06]<-n18; so[n07]<-n19; so[n08]<-n20;
let sqo = Array31.make n9 n0 in
sqo[n00]<-n00; sqo[n01]<-n01; sqo[n02]<-n02; sqo[n03]<-n09; sqo[n04]<-n10;
sqo[n05]<-n11; sqo[n06]<-n18; sqo[n07]<-n19; sqo[n08]<-n20;
{ column_start = cs; column_offsets = co;
row_start = rs; row_offsets = ro;
square_start = ss; square_offsets = so; }
square_start = ss; square_offsets = sqo; }
end
......
......@@ -214,12 +214,12 @@ module TheClassicalSudokuGrid
ss[71]<-60; ss[72]<-54; ss[73]<-54; ss[74]<-54; ss[75]<-57;
ss[76]<-57; ss[77]<-57; ss[78]<-60; ss[79]<-60; ss[80]<-60;
(* square offset *)
let so = Array.make 9 0 in
so[ 0]<-0; so[ 1]<-1; so[ 2]<-2; so[ 3]<-9; so[ 4]<-10;
so[ 5]<-11; so[ 6]<-18; so[ 7]<-19; so[ 8]<-20;
let sqo = Array.make 9 0 in
sqo[ 0]<-0; sqo[ 1]<-1; sqo[ 2]<-2; sqo[ 3]<-9; sqo[ 4]<-10;
sqo[ 5]<-11; sqo[ 6]<-18; sqo[ 7]<-19; sqo[ 8]<-20;
{ column_start = cs; column_offsets = co;
row_start = rs; row_offsets = ro;
square_start = ss; square_offsets = so; }
square_start = ss; square_offsets = sqo; }
end
......
......@@ -28,7 +28,7 @@ let rec intros pr f = match f.t_node with
(* split f1 *)
(* f is going to be removed, preserve its labels and location in f2 *)
let f2 = t_label_copy f f2 in
let l = Split_goal.split_pos_intro f1 in
let l = Split_goal.split_intro_right f1 in
List.fold_right
(fun f acc ->
let id = create_prsymbol (id_fresh "H") in
......@@ -63,12 +63,15 @@ let intros pr f =
let subst = Mtv.map (fun ts -> ty_app ts []) tvm in
Mtv.values decls @ intros pr (t_ty_subst subst Mvs.empty f)
let () = Trans.register_transform "introduce_premises" (Trans.goal intros)
let introduce_premises = Trans.goal intros
let () = Trans.register_transform "introduce_premises" introduce_premises
~desc:"Introduce@ universal@ quantification@ and@ hypothesis@ in@ the@ \
goal@ into@ constant@ symbol@ and@ axioms."
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. byte"
End:
*)
let split_intro =
Trans.compose_l Split_goal.split_goal_wp (Trans.singleton introduce_premises)
let () = Trans.register_transform_l "split_intro" split_intro
~desc:"Same@ as@ split_goal_wp,@ but@ moves@ \
the@ implication@ antecedents@ to@ premises."
......@@ -30,3 +30,8 @@
val intros : Decl.prsymbol -> Term.term -> Decl.decl list
(** [intros G f] returns the declarations after introducing
premises of [goal G : f] *)
val introduce_premises : Task.task Trans.trans
val split_intro : Task.task Trans.tlist
(** [split_intro] is [split_goal_wp] followed by [introduce_premises] *)
......@@ -23,6 +23,18 @@ type split = {
comp_match : known_map option;
}
let stop_split = Ident.create_label "stop_split"
let compiled = Ident.create_label "split_goal: compiled match"
let case_label = Ident.create_label "case_split"
let stop f = Slab.mem stop_split f.t_label
let asym f = Slab.mem Term.asym_label f.t_label
let keep f = Slab.mem Term.keep_on_simp_label f.t_label
let case f = Slab.mem case_label f.t_label
let unstop f =
t_label ?loc:f.t_loc (Slab.remove stop_split f.t_label) f
(* Represent monoid of formula interpretation for conjonction and disjunction *)
module M = struct
......@@ -36,10 +48,28 @@ module M = struct
(* inject formula into monoid. *)
let (!+) a = Comb (Base a)
let rec filter c = match c with
| Base a when keep a -> Some c
| Base _ -> None
| Op (a,b) ->
match filter a, filter b with
| None, u | u, None -> u
| Some a, Some b -> Some (Op (a,b))
(* monoid law. *)
let (++) a b = match a, b with
| Zero _, _ | _, Unit -> a
| _, Zero _ | Unit, _ -> b
let (++) a b =
match a, b with
| _, Unit -> a
| Unit, _ -> b
| Zero ta, Comb b -> begin match filter b with
| None -> a
| Some b -> Comb (Op (Base ta,b))
end
| Comb a, Zero tb -> begin match filter a with
| None -> b
| Some a -> Comb (Op (a,Base tb))
end
| Zero _, Zero _ -> a
| Comb ca, Comb cb -> Comb (Op (ca, cb))
(* (base -> base) morphism application. *)
......@@ -102,19 +132,6 @@ type split_ret = {
side : M.monoid;
}
let stop_split = Ident.create_label "stop_split"
let compiled = Ident.create_label "split_goal: compiled match"
let case_label = Ident.create_label "case_split"
let stop f = Slab.mem stop_split f.t_label
let asym f = Slab.mem Term.asym_label f.t_label
let keep f = Slab.mem Term.keep_on_simp_label f.t_label
let case f = Slab.mem case_label f.t_label
let unstop f =
t_label ?loc:f.t_loc (Slab.remove stop_split f.t_label) f
let rec drop_byso f = match f.t_node with
| Tbinop (Timplies,{ t_node = Tbinop (Tor,_,{ t_node = Ttrue }) },f) ->
drop_byso f
......@@ -175,11 +192,11 @@ let rec split_core sp f =
let ret pos neg bwd fwd side = { pos; neg; bwd; fwd; side } in
let r = match f.t_node with
| _ when sp.stop_split && stop f ->
let f = unstop f in
let df = drop_byso f in
ret !+f !+df f df Unit
| Ttrue -> ret (if keep f then !+f else Unit) (Zero f) f f Unit
| Tfalse -> ret (Zero f) (if keep f then !+f else Unit) f f Unit
ret !+(unstop f) !+(unstop df) f df Unit
| (Ttrue | Tfalse) when keep f -> ret !+f !+f f f Unit
| Ttrue -> ret Unit (Zero f) f f Unit
| Tfalse -> ret (Zero f) Unit f f Unit
| Tapp _ -> let uf = !+f in ret uf uf f f Unit
(* f1 so f2 *)
| Tbinop (Tand,f1,{ t_node = Tbinop (Tor,f2,{ t_node = Ttrue }) }) ->
......@@ -370,27 +387,38 @@ let full_split kn = {
}
let right_split kn = { (full_split kn) with right_only = true }
let wp_split kn = { (right_split kn) with stop_split = true }
let intro_split kn = { (wp_split kn) with asym_split = false }
let proof_split kn = { (wp_split kn) with byso_split = true }
let total_split kn = { (proof_split kn) with right_only = false }
let full_proof kn = { (full_split kn) with stop_split = true;
byso_split = true }
let right_proof kn = { (full_proof kn) with right_only = true }
let full_intro kn = { (full_split kn) with asym_split = false;
stop_split = true }
let right_intro kn = { (full_intro kn) with right_only = true }
let split_pos sp f =
let core = split_core sp f in
assert (core.side = Unit);
to_list core.pos
let split_neg sp f =
let core = split_core sp f in
assert (core.side = Unit);
to_list core.neg
let split_pos sp f = M.to_list (split_core sp f).pos
let split_neg sp f = M.to_list (split_core sp f).neg
let split_proof sp f =
let core = split_core sp f in M.to_list (M.(++) core.pos core.side)
let split_pos_full ?known_map f = split_pos (full_split known_map) f
let split_neg_full ?known_map f = split_neg (full_split known_map) f
let core = split_core sp f in
to_list (core.pos ++ core.side)
let split_pos_full ?known_map f = split_pos (full_split known_map) f
let split_pos_right ?known_map f = split_pos (right_split known_map) f
let split_neg_full ?known_map f = split_neg (full_split known_map) f
let split_neg_right ?known_map f = split_neg (right_split known_map) f
let split_pos_wp ?known_map f = split_pos (wp_split known_map) f
let split_neg_wp ?known_map f = split_neg (wp_split known_map) f
let split_proof_full ?known_map f = split_proof (full_proof known_map) f
let split_proof_right ?known_map f = split_proof (right_proof known_map) f
let split_pos_intro ?known_map f = split_pos (intro_split known_map) f
let split_neg_intro ?known_map f = split_neg (intro_split known_map) f
let split_intro_full ?known_map f = split_pos (full_intro known_map) f
let split_intro_right ?known_map f = split_pos (right_intro known_map) f
let split_goal sp pr f =
let make_prop f = [create_prop_decl Pgoal pr f] in
......@@ -429,19 +457,17 @@ let prep_premise split = Trans.store (fun t ->
let trans = Trans.decl (split_premise split) None in
Trans.apply trans t)
let split_goal_full = prep_goal full_split
let split_goal_right = prep_goal right_split
let split_goal_wp = prep_goal wp_split
let split_proof = prep_goal proof_split
let split_proof_full = prep_goal total_split
let split_goal_full = prep_goal full_proof
let split_goal_right = prep_goal right_proof
let split_goal_wp = split_goal_right
let split_all_full = prep_all full_split
let split_all_right = prep_all right_split
let split_all_wp = prep_all wp_split
let split_all_full = prep_all full_proof
let split_all_right = prep_all right_proof
let split_all_wp = split_all_right
let split_premise_full = prep_premise full_split
let split_premise_right = prep_premise right_split
let split_premise_wp = prep_premise wp_split
let split_premise_full = prep_premise full_proof
let split_premise_right = prep_premise right_proof
let split_premise_wp = split_premise_right
let () = Trans.register_transform_l "split_goal_full" split_goal_full
~desc:"Put@ the@ goal@ in@ a@ conjunctive@ form,@ \
......@@ -462,63 +488,9 @@ let () = Trans.register_transform "split_premise_right" split_premise_right
~desc:"Same@ as@ split_all_right,@ but@ split@ only@ premises."
let () = Trans.register_transform_l "split_goal_wp" split_goal_wp
~desc:"Same@ as@ split_goal_right,@ but@ stops@ at@ \
the@ `stop_split'@ label@ and@ removes@ the@ label."
~desc:"Same@ as@ split_goal_right."
let () = Trans.register_transform_l "split_all_wp" split_all_wp
~desc:"Same@ as@ split_goal_wp,@ but@ also@ split@ premises."
let () = Trans.register_transform "split_premise_wp" split_premise_wp
~desc:"Same@ as@ split_all_wp,@ but@ split@ only@ premises."
let () = Trans.register_transform_l "split_goal_wp_old"
(Trans.goal_l (split_goal (wp_split None)))
~desc:"transitional, to be removed as soon as all sessions migrate"
let () = Trans.register_transform_l "split_proof" split_proof
~desc:"experimental"
let () = Trans.register_transform_l "split_proof_full" split_proof_full
~desc:"experimental"
let ls_of_var v =
create_fsymbol (id_fresh ("spl_" ^ v.vs_name.id_string)) [] v.vs_ty
let split_intro known_map pr f =
let rec split_intro dl acc f =
let rsp = split_intro dl in
match f.t_node with
| Ttrue when not (keep f) -> acc
| Tbinop (Tand,f1,f2) when asym f1 ->
rsp (rsp acc (t_implies f1 f2)) f1
| Tbinop (Tand,f1,f2) ->
rsp (rsp acc f2) f1
| Tbinop (Timplies,f1,f2) ->
let pp = create_prsymbol (id_fresh (pr.pr_name.id_string ^ "_spl")) in
let dl = create_prop_decl Paxiom pp f1 :: dl in
split_intro dl acc f2
| Tbinop (Tiff,f1,f2) ->
rsp (rsp acc (t_implies f2 f1)) (t_implies f1 f2)
| Tif (fif,fthen,felse) ->
rsp (rsp acc (t_implies (t_not fif) felse)) (t_implies fif fthen)
| Tlet (t,fb) -> let vs,f = t_open_bound fb in
let ls = ls_of_var vs in
let f = t_subst_single vs (fs_app ls [] vs.vs_ty) f in
let dl = create_logic_decl [make_ls_defn ls [] t] :: dl in
split_intro dl acc f
| Tquant (Tforall,fq) -> let vsl,_,f = t_open_quant fq in
let lls = List.map ls_of_var vsl in
let add s vs ls = Mvs.add vs (fs_app ls [] vs.vs_ty) s in
let f = t_subst (List.fold_left2 add Mvs.empty vsl lls) f in
let add dl ls = create_param_decl ls :: dl in
let dl = List.fold_left add dl lls in
split_intro dl acc f
| _ ->
let goal f = List.rev (create_prop_decl Pgoal pr f :: dl) in
List.rev_append (List.rev_map goal (split_pos_wp ~known_map f)) acc
in
split_intro [] [] f
let split_intro = Trans.store (fun t ->
Trans.apply (Trans.goal_l (split_intro (Task.task_known t))) t)
let () = Trans.register_transform_l "split_intro" split_intro
~desc:"Same@ as@ split_goal_wp,@ but@ moves@ \
the@ implication@ antecedents@ to@ premises."
......@@ -29,21 +29,25 @@ val split_neg_right : ?known_map:Decl.known_map -> Term.term -> Term.term list
(** [split_neg_right] works as [split_neg_full] but does not split
disjunctions and implications under conjunctions *)
val split_pos_wp : ?known_map:Decl.known_map -> Term.term -> Term.term list
(** [split_pos_wp] works as [split_pos_right] but stops at
the `[stop_split]' label and removes the label *)
val split_neg_wp : ?known_map:Decl.known_map -> Term.term -> Term.term list
(** [split_neg_wp] works as [split_neg_right] but stops at
the `[stop_split]' label and removes the label *)
val split_pos_intro : ?known_map:Decl.known_map -> Term.term -> Term.term list
(** [split_pos_intro] works as [split_pos_wp] but does not
respect the `asym_split' label *)
val split_neg_intro : ?known_map:Decl.known_map -> Term.term -> Term.term list
(** [split_neg_intro] works as [split_neg_wp] but does not
respect the `asym_split' label *)
val split_proof_full : ?known_map:Decl.known_map -> Term.term -> Term.term list
(** [split_proof_full f] returns a list of formulas whose conjunction implies f.
The reverse implication also holds when f does not contain the by/so
connectives. In this case, [split_pos_wp] works as [split_pos_full]
but stops at the [stop_split] label and removes it. *)
val split_proof_right : ?known_map:Decl.known_map -> Term.term -> Term.term list
(** [split_proof_right f] returns a list of formulas whose conjunction
implies f. The reverse implication also holds when f does not contain
the by/so connectives. In this case, [split_pos_wp] works as
[split_pos_right] but stops at the [stop_split] label and removes it. *)
val split_intro_full : ?known_map:Decl.known_map -> Term.term -> Term.term list
(** [split_intro_full] works as [split_pos_full] but does not respect
the [asym_split] label, stops at the [stop_split] label and removes it *)
val split_intro_right : ?known_map:Decl.known_map -> Term.term -> Term.term list
(** [split_intro_right] works as [split_pos_right] but does not respect
the [asym_split] label, stops at the [stop_split] label and removes it *)
val split_goal_full : Task.task Trans.tlist
val split_all_full : Task.task Trans.tlist
......@@ -57,5 +61,3 @@ val split_goal_wp : Task.task Trans.tlist
val split_all_wp : Task.task Trans.tlist
val split_premise_wp : Task.task Trans.trans
val split_intro : Task.task Trans.tlist
(** [split_intro] is [split_goal_wp] with skolemization and formula separation *)
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