(* creates the discrimination = injection+contradiction principle *)
exception ConstructorTooBig of string;;
-let mk_discriminator ~use_jmeq name it leftno status baseuri =
+let mk_discriminator ~use_jmeq ?(force=false) name it leftno status baseuri =
let itnargs =
let _,_,arity,_ = it in
List.length (arg_list 0 arity) in
List.map
(fun i ->
let nargs_kty = nargs it leftno i in
- if (nargs_kty > 5 && not use_jmeq) then raise (ConstructorTooBig (kname i));
+ if (nargs_kty > 5 && not use_jmeq && not force) then raise (ConstructorTooBig (kname i));
let ts = iter (fun m acc -> mk_id ("t" ^ (string_of_int m))::acc)
(nargs_kty - 1) [] in
let nones =
(* PHASE 2: create the object for the proof of the principle: we'll name it
* "theorem" *)
let status, theorem =
- GrafiteDisambiguate.disambiguate_nobj status ~baseuri
+ let attrs = `Generated, `Theorem, `DiscriminationPrinciple in
+ GrafiteDisambiguate.disambiguate_nobj status ~baseuri
(baseuri ^ name ^ ".def",0,
NotationPt.Theorem
- (`Theorem,name,principle,
- Some (NotationPt.Implicit (`Tagged "inv")),`DiscriminationPrinciple))
+ (name, principle, Some (NotationPt.Implicit (`Tagged "inv")), attrs))
in
let uri,height,nmenv,nsubst,nobj = theorem in
let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
| NCic.Rel var ->
cascade_select_in_ctx status ~subst:(get_subst status) context skip (var+cur_eq)
| _ -> cascade_select_in_ctx status ~subst:(get_subst status) context skip cur_eq in
+ let varname = match var with
+ | NCic.Rel var ->
+ let name,_ = List.nth context (var+cur_eq-1) in
+ HLog.warn (Printf.sprintf "destruct: trying to remove variable: %s" name);
+ [name]
+ | _ -> []
+ in
let names_to_gen = List.filter (fun n -> n <> eq_name) names_to_gen in
if (List.exists (fun x -> List.mem x skip) names_to_gen)
then oldstatus
~what:("",0,mk_id eq_name) ~where:default_pattern;
(* NTactics.reduce_tac ~reduction:(`Normalize true)
~where:default_pattern;*)
+ (* XXX: temo che la clear multipla funzioni bene soltanto se
+ * gli identificatori sono nell'ordine giusto.
+ * Per non saper né leggere né scrivere, usiamo due clear
+ * invece di una *)
NTactics.try_tac (NTactics.clear_tac [eq_name]);
+ NTactics.try_tac (NTactics.clear_tac varname);
]@
(List.map NTactics.intro_tac (List.rev names_to_gen))) status
;;
let has_cleared =
try
let _ = NTactics.find_in_context eq_name (get_ctx status' newgoal) in false
- with _ -> true in
+ with
+ | Sys.Break as e -> raise e
+ |_ -> true in
let rm_eq b l = if b then List.filter (fun x -> x <> eq_name) l else l in
let acc = rm_eq has_cleared acc in
let skip = rm_eq has_cleared skip in
let has_cleared =
try
let _ = NTactics.find_in_context eq_name (get_ctx status' newgoal) in false
- with _ -> true in
+ with
+ | Sys.Break as e -> raise e
+ | _ -> true in
let rm_eq b l = if b then List.filter (fun x -> x <> eq_name) l else l in
let acc = rm_eq has_cleared acc in
let skip = rm_eq has_cleared skip in