let nargs it nleft consno =
pp (lazy (Printf.sprintf "nargs %d %d" nleft consno));
- let _,indname,_,cl = it in
+ let _,_indname,_,cl = it in
let _,_,t_k = List.nth cl consno in
List.length (arg_list nleft t_k) ;;
let default_pattern = "",0,(None,[],Some NotationPt.UserInput);;
let prod_pattern =
- "",0,(None,[],Some NotationPt.Binder
+ "",0,(None,[],Some (NotationPt.Binder
(`Pi, (mk_id "_",Some (NotationPt.Appl
[ NotationPt.Implicit `JustOne
; NotationPt.Implicit `JustOne
; NotationPt.UserInput
; NotationPt.Implicit `JustOne ])),
- NotationPt.Implicit `JustOne));;
+ NotationPt.Implicit `JustOne)));;
let prod_pattern_jm =
- "",0,(None,[],Some NotationPt.Binder
+ "",0,(None,[],Some (NotationPt.Binder
(`Pi, (mk_id "_",Some (NotationPt.Appl
[ NotationPt.Implicit `JustOne
; NotationPt.Implicit `JustOne
; NotationPt.UserInput
; NotationPt.Implicit `JustOne
; NotationPt.Implicit `JustOne ])),
- NotationPt.Implicit `JustOne));;
+ NotationPt.Implicit `JustOne)));;
let hp_pattern n =
"",0,(None,[n, NotationPt.Appl
(* 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 _uri,_height,nmenv,_nsubst,_nobj = theorem in
let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
let status = status#set_obj theorem in
let status = status#set_stack ninitial_stack in
let status = subst_metasenv_and_fix_names status in
(* PHASE 3: we finally prove the discrimination principle *)
- let dbranch it ~use_jmeq leftno consno =
+ let dbranch it ~use_jmeq:__ leftno consno =
let refl_id = mk_sym "refl" in
pp (lazy (Printf.sprintf "dbranch %d %d" leftno consno));
let nlist = HExtlib.list_seq 0 (nargs it leftno consno) in
;;
let subst_tac ~context ~dir skip cur_eq =
- fun status as oldstatus ->
+ fun (status as oldstatus) ->
let eq_name,(NCic.Decl s | NCic.Def (s,_)) = List.nth context (cur_eq-1) in
let _,ctx' = HExtlib.split_nth cur_eq context in
let status, s = NTacStatus.whd status ctx' (mk_cic_term ctx' s) 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
else
let gen_tac x =
(fun s ->
- let x' = String.concat " " x in
+ (*let x' = String.concat " " x in*)
let x = List.map mk_id x in
(* let s = NTactics.print_tac false ("@generalize " ^ x') s in *)
generalize0_tac x s) in
~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
;;
| _ -> status, `NonEq
in match kind with
| `Identity ->
- let status, goalty = term_of_cic_term status (get_goalty status goal) ctx in
+ let status, _goalty = term_of_cic_term status (get_goalty status goal) ctx in
status, Some (List.length ctx - i), kind
| `Cycle | `Blob | `NonEq -> aux (i+1) (* XXX: skip cyclic/blob equations for now *)
| _ ->
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
projects / helm.git / blobdiff