(* $Id$ *)
-let debug_print = fun _ -> ()
+let debug = false
+let debug_print =
+ if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ())
+;;
(* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori
diversi *)
in
let discriminate'_tac ~term status =
let (proof, goal) = status in
- let _,metasenv,_,_, _ = proof in
+ let _,metasenv,_subst,_,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let termty,_ =
CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
let exn_noneqind =
ProofEngineTypes.Fail (lazy "Injection: not an equality over elements of an inductive type");;
+let pp ctx t =
+ let names = List.map (function Some (n,_) -> Some n | None -> None) ctx in
+ CicPp.pp t names
+;;
+
let rec injection_tac ~first_time ~term ~liftno ~continuation =
let module C = Cic in
let module CR = CicReduction in
let module T = Tacticals in
let module PST = ProofEngineStructuralRules in
let module PET = ProofEngineTypes in
- let prerr_endline s = prerr_endline (String.make liftno ' ' ^ s) in
let are_convertible hd1 hd2 metasenv context =
fst (CR.are_convertible ~metasenv context hd1 hd2 CicUniv.empty_ugraph)
in
let injection_tac ~term status =
let (proof, goal) = status in
- let _,metasenv,_,_, _ = proof in
+ let _,metasenv,_subst, _,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let term = CicSubstitution.lift liftno term in
let termty,_ =
CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
in
- prerr_endline ("injection su: " ^ CicPp.ppterm termty);
+ debug_print (lazy ("\ninjection su: " ^ pp context termty));
let tac =
match termty with
| C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]
let module P = PrimitiveTactics in
let module PET = ProofEngineTypes in
let module T = Tacticals in
- let prerr_endline s = prerr_endline (String.make liftno ' ' ^ s) in
let give_name seed = function
| C.Name _ as name -> name
| C.Anonymous -> C.Name (incr seed; "y" ^ string_of_int !seed)
* differiscono (o potrebbero differire?) nell'i-esimo parametro
* del costruttore *)
let term = CicSubstitution.lift liftno term in
- let _,metasenv,_,_, _ = proof in
+ let _,metasenv,_subst,_,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let termty,_ =
CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
in
- prerr_endline ("injection1 su : " ^ CicPp.ppterm termty);
+ debug_print (lazy ("\ninjection1 su : " ^ pp context termty));
match termty with (* an equality *)
| C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]
when LibraryObjects.is_eq_URI equri ->
let binder' = give_name seed binder in
C.Lambda (binder',source,(aux (k+1) target))
| _ ->
- let nr_param_constr = k - paramsno in
+ let nr_param_constr = k - paramsno - 1 in
if id = i_constr_id then C.Rel (k - i)
else S.lift nr_param_constr t1'
(* + 1 per liftare anche il lambda aggiunto
* esternamente al case *)
- in aux 1 reduced_cty)
+ in CicSubstitution.lift 1 (aux 1 reduced_cty))
constructor_list
in
+ (* this code should be taken from cases_tac *)
let outtype =
let seed = ref 0 in
let rec to_lambdas te head =
| _, _ -> assert false
in
let abstracted_tty =
- match CicSubstitution.lift (paramsno(* + 1*)) tty with
+ let tty =
+ List.fold_left (fun x y -> CicSubstitution.subst y x) tty left_params
+ in
+ (* non lift, ma subst coi left! *)
+ match S.lift 1 tty with
| C.MutInd _ as tty' -> tty'
| C.Appl l ->
let keep,abstract = HExtlib.split_nth (paramsno +1) l in
+ let keep = List.map (S.lift paramsno) keep in
C.Appl (keep@mk_rels (List.length abstract))
| _ -> assert false
in
match ind_type_list with
| [] -> assert false
| (_,_,ty,_)::_ ->
+ (* this is in general wrong, do as in cases_tac *)
to_lambdas (skip_prods left_params ty)
(C.Lambda
- (C.Name "x", abstracted_tty, S.lift 1 tty'))
+ (C.Name "cased", abstracted_tty,
+ (* here we should capture right parameters *)
+ (* 1 for his Lambda, one for the Lambda outside the match
+ * and then one for each to_lambda *)
+ S.lift (2+List.length right_params) tty'))
in
patterns,outtype
| _ -> raise exn_discrnonind
in
let cutted = C.Appl [C.MutInd (equri,0,[]) ; tty' ; t1' ; t2'] in
- prerr_endline ("CUT: " ^ CicPp.ppterm cutted);
+ let changed =
+ C.Appl [ C.Lambda (C.Name "x", tty,
+ C.MutCase (turi,typeno,outtype,C.Rel 1,patterns)) ; t1]
+ in
+ (* check if cutted and changed are well typed and if t1' ~ changed *)
+ let go_on =
+ try
+ let _,g = CicTypeChecker.type_of_aux' metasenv context cutted
+ CicUniv.empty_ugraph
+ in
+ let _,g = CicTypeChecker.type_of_aux' metasenv context changed g in
+ fst (CicReduction.are_convertible ~metasenv context t1' changed g)
+ with
+ | CicTypeChecker.TypeCheckerFailure _ -> false
+ in
+ if not go_on then
+ PET.apply_tactic Tacticals.id_tac status
+ else
+ (debug_print (lazy ("CUT: " ^ pp context cutted));
PET.apply_tactic
(T.thens ~start: (P.cut_tac cutted)
~continuations:
;T.then_
~start:(PET.mk_tactic
(fun status ->
- prerr_endline "riempo il cut";
+ debug_print (lazy "riempo il cut");
let (proof, goal) = status in
- let _,metasenv,_,_, _ = proof in
+ let _,metasenv,_subst,_,_, _ = proof in
let _,context,gty =CicUtil.lookup_meta goal metasenv in
let gty = Unshare.unshare gty in
let new_t1' =
| (C.Appl (C.MutInd (_,_,_)::_::t::_)) -> t
| _ -> raise exn_injwronggoal
in
- let changed =
- C.Appl [
- C.Lambda (C.Name "x", tty,
- C.MutCase (turi,typeno,outtype,C.Rel 1,patterns))
- ; t1]
- in
- prerr_endline
- ("metto questo: " ^ CicPp.ppterm changed);
- prerr_endline
- ("al posto di questo: " ^ CicPp.ppterm new_t1');
- prerr_endline
- ("nel goal: " ^ CicPp.ppterm gty);
- prerr_endline
- ("nel contesto:\n" ^ CicPp.ppcontext context);
- let rc =
+ debug_print
+ (lazy ("metto questo: " ^ pp context changed));
+ debug_print
+ (lazy ("al posto di questo: " ^ pp context new_t1'));
+ debug_print
+ (lazy ("nel goal: " ^ pp context gty));
+ debug_print
+ (lazy ("nel contesto:\n" ^ CicPp.ppcontext context));
+ debug_print
+ (lazy ("e poi rewrite con: "^pp context term));
+ let rc =
PET.apply_tactic
(ReductionTactics.change_tac
~pattern:(None, [],
~term:gty [new_t1']))
(fun _ m u -> changed,m,u))
status
- in prerr_endline "fine";rc
+ in rc
))
~continuation:
(T.then_
term [])
~continuation:EqualityTactics.reflexivity_tac)
])
- status
+ status)
| _ -> raise exn_noneq
in
PET.mk_tactic (injection1_tac ~term ~i)
projects / helm.git / blobdiff