(* 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
| _ -> 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 in [name]
+ 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
(* 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 *)
+ * invece di una *)
NTactics.try_tac (NTactics.clear_tac [eq_name]);
NTactics.try_tac (NTactics.clear_tac varname);
]@
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