| NCic.Rel _
| NCic.Sort _ -> ()
| NCic.Implicit _ -> assert false
- | NCic.Const nref as t ->
+ | NCic.Const nref ->
(*
prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[]
~context:[] t ^ ":" ^ string_of_int (height_of_ref nref));
with
NCicRefiner.RefineFailure msg
| NCicRefiner.Uncertain msg ->
- print (lazy ("WARNING: refining in fast_eq_check failed\n" ^
+ debug_print (lazy ("WARNING: refining in fast_eq_check failed\n" ^
snd (Lazy.force msg) ^
"\n in the environment\n" ^
NCicPp.ppmetasenv subst metasenv)); None
| NCicRefiner.AssertFailure msg ->
- print (lazy ("WARNING: refining in fast_eq_check failed" ^
+ debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
Lazy.force msg ^
"\n in the environment\n" ^
NCicPp.ppmetasenv subst metasenv)); None
let open_goal = List.hd open_goals in
let ngty = get_goalty status open_goal in
let ctx = ctx_of ngty in
+ let ctx = apply_subst_context ~fix_projections:true status ctx in
let c = ref 0 in
List.fold_left
(fun eq_cache _ ->
let ty = NCicTypeChecker.typeof [] [] ctx t in
if is_a_fact status (mk_cic_term ctx ty) then
(debug_print(lazy("eq indexing " ^ (NCicPp.ppterm ctx [] [] ty)));
+ debug_print(lazy("riprovo " ^ (ppterm status (mk_cic_term ctx ty))));
NCicParamod.forward_infer_step eq_cache t ty)
else
(debug_print (lazy ("not a fact: " ^ (NCicPp.ppterm ctx [] [] ty)));
| NCic.Const(NReference.Ref (_,NReference.Def _) as nre)
when nre<>nref ->
let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def nre in
- aux metasenv ty (args@moreargs)
+ aux metasenv bo (args@moreargs)
| NCic.Appl(NCic.Const(NReference.Ref (_,NReference.Def _) as nre)::tl)
when nre<>nref ->
let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def nre in
type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
+(* cartesian: term set list -> term list set *)
+let rec cartesian =
+ function
+ [] -> NDiscriminationTree.TermListSet.empty
+ | [l] ->
+ NDiscriminationTree.TermSet.fold
+ (fun x acc -> NDiscriminationTree.TermListSet.add [x] acc) l NDiscriminationTree.TermListSet.empty
+ | he::tl ->
+ let rest = cartesian tl in
+ NDiscriminationTree.TermSet.fold
+ (fun x acc ->
+ NDiscriminationTree.TermListSet.fold (fun l acc' -> NDiscriminationTree.TermListSet.add (x::l) acc') rest acc
+ ) he NDiscriminationTree.TermListSet.empty
+;;
+
+(* all_keys_of_cic_type: term -> term set *)
+let all_keys_of_cic_type metasenv subst context ty =
+ let saturate ty =
+ (* Here we are dropping the metasenv, but this should not raise any
+ exception (hopefully...) *)
+ let ty,_,hyps =
+ NCicMetaSubst.saturate ~delta:max_int metasenv subst context ty 0
+ in
+ ty,List.length hyps
+ in
+ let rec aux ty =
+ match ty with
+ NCic.Appl (he::tl) ->
+ let tl' =
+ List.map (fun ty ->
+ let wty = NCicReduction.whd ~delta:0 ~subst context ty in
+ if ty = wty then
+ NDiscriminationTree.TermSet.add ty (aux ty)
+ else
+ NDiscriminationTree.TermSet.union
+ (NDiscriminationTree.TermSet.add ty (aux ty))
+ (NDiscriminationTree.TermSet.add wty (aux wty))
+ ) tl
+ in
+ NDiscriminationTree.TermListSet.fold
+ (fun l acc -> NDiscriminationTree.TermSet.add (NCic.Appl l) acc)
+ (cartesian ((NDiscriminationTree.TermSet.singleton he)::tl'))
+ NDiscriminationTree.TermSet.empty
+ | _ -> NDiscriminationTree.TermSet.empty
+ in
+ let ty,ity = saturate ty in
+ let wty,iwty = saturate (NCicReduction.whd ~delta:0 ~subst context ty) in
+ if ty = wty then
+ [ity, NDiscriminationTree.TermSet.add ty (aux ty)]
+ else
+ [ity, NDiscriminationTree.TermSet.add ty (aux ty) ;
+ iwty, NDiscriminationTree.TermSet.add wty (aux wty) ]
+;;
+
+let all_keys_of_type status t =
+ let _,_,metasenv,subst,_ = status#obj in
+ let context = ctx_of t in
+ let status, t = apply_subst status context t in
+ let keys =
+ all_keys_of_cic_type metasenv subst context
+ (snd (term_of_cic_term status t context))
+ in
+ status,
+ List.map
+ (fun (intros,keys) ->
+ intros,
+ NDiscriminationTree.TermSet.fold
+ (fun t acc -> Ncic_termSet.add (mk_cic_term context t) acc)
+ keys Ncic_termSet.empty
+ ) keys
+;;
+
+
let keys_of_type status orig_ty =
+ (* Here we are dropping the metasenv (in the status), but this should not
+ raise any exception (hopefully...) *)
let _, ty, _ = saturate ~delta:max_int status orig_ty in
- let keys = [ty] in
+ let _, ty = apply_subst status (ctx_of ty) ty in
+ let keys =
+(*
+ let orig_ty' = NCicTacReduction.normalize ~subst context orig_ty in
+ if orig_ty' <> orig_ty then
+ let ty',_,_= NCicMetaSubst.saturate ~delta:0 metasenv subst context orig_ty' 0 in
+ [ty;ty']
+ else
+ [ty]
+*)
+ [ty] in
+(*CSC: strange: we keep ty, ty normalized and ty ~delta:(h-1) *)
let keys =
let _, ty = term_of_cic_term status ty (ctx_of ty) in
match ty with
status, keys
;;
+let all_keys_of_term status t =
+ let status, orig_ty = typeof status (ctx_of t) t in
+ all_keys_of_type status orig_ty
+;;
+
let keys_of_term status t =
let status, orig_ty = typeof status (ctx_of t) t in
keys_of_type status orig_ty
| [] -> (* Ncic_termSet.elements *) acc
| (_::tl) as k ->
try
- let idx = List.assq k th in
+ let idx = List.assoc(*q*) k th in
let acc = Ncic_termSet.union acc
(InvRelDiscriminationTree.retrieve_unifiables idx gty)
in
else if smart = 1 then smart_apply_auto ("",0,t) eq_cache status
else (* smart = 2: both *)
try NTactics.apply_tac ("",0,t) status
- with Error _ as exc ->
+ with Error _ ->
smart_apply_auto ("",0,t) eq_cache status
in
(*
let c_ast = function
| NCic.Const r -> Ast.NRef r | _ -> assert false in
let _, raw_gty = term_of_cic_term status gty context in
- let cands =
- NDiscriminationTree.DiscriminationTree.retrieve_unifiables
- universe raw_gty
- in
+ let keys = all_keys_of_cic_term metasenv subst context raw_gty in
+ (* we only keep those keys that do not require any intros for now *)
+ let no_intros_keys = snd (List.hd keys) in
+ let cands =
+ NDiscriminationTree.TermSet.fold
+ (fun ty acc ->
+ NDiscriminationTree.TermSet.union acc
+ (NDiscriminationTree.DiscriminationTree.retrieve_unifiables
+ universe ty)
+ ) no_intros_keys NDiscriminationTree.TermSet.empty in
+(* old code:
+ let cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables
+ universe raw_gty in
+*)
+ let local_cands =
+ NDiscriminationTree.TermSet.fold
+ (fun ty acc ->
+ Ncic_termSet.union acc (search_in_th (mk_cic_term context ty) cache)
+ ) no_intros_keys Ncic_termSet.empty in
+(* old code:
let local_cands = search_in_th gty cache in
+*)
debug_print (lazy ("candidates for" ^ NTacStatus.ppterm status gty));
debug_print (lazy ("local cands = " ^ (string_of_int (List.length (Ncic_termSet.elements local_cands)))));
let together global local =
let is_prod status =
let _, ctx, gty = current_goal status in
+ let status, gty = apply_subst status ctx gty in
let _, raw_gty = term_of_cic_term status gty ctx in
match raw_gty with
- | NCic.Prod (name,_,_) -> Some (guess_name name ctx)
- | _ -> None
+ | NCic.Prod (name,src,_) ->
+ let status, src = whd status ~delta:0 ctx (mk_cic_term ctx src) in
+ (match snd (term_of_cic_term status src ctx) with
+ | NCic.Const(NReference.Ref (_,NReference.Ind _) as r)
+ | NCic.Appl (NCic.Const(NReference.Ref (_,NReference.Ind _) as r)::_) ->
+ let _,_,itys,_,_ = NCicEnvironment.get_checked_indtys r in
+ (match itys with
+ | [_,_,_,[_;_]]
+ | [_,_,_,[_]]
+ | [_,_,_,[]] -> `Inductive (guess_name name ctx)
+ | _ -> `Some (guess_name name ctx))
+ | _ -> `Some (guess_name name ctx))
+ | _ -> `None
let intro ~depth status facts name =
let status = NTactics.intro_tac name status in
;;
let rec intros_facts ~depth status facts =
+ if List.length (head_goals status#stack) <> 1 then status, facts else
match is_prod status with
- | Some(name) ->
+ | `Some(name) ->
let status,facts =
intro ~depth status facts name
in intros_facts ~depth status facts
+ | `Inductive name ->
+ let status = NTactics.case1_tac name status in
+ intros_facts ~depth status facts
| _ -> status, facts
;;
-let rec intros ~depth status cache =
+let intros ~depth status cache =
match is_prod status with
- | Some _ ->
+ | `Inductive _
+ | `Some _ ->
let trace = cache.trace in
let status,facts =
intros_facts ~depth status cache.facts
in
+ if head_goals status#stack = [] then
+ let status = NTactics.merge_tac status in
+ [(0,Ast.Ident("__intros",None)),status], cache
+ else
(* we reindex the equation from scratch *)
- let unit_eq =
- index_local_equations status#eq_cache status in
- status, init_cache ~facts ~unit_eq () ~trace
- | _ -> status, cache
+ let unit_eq = index_local_equations status#eq_cache status in
+ let status = NTactics.merge_tac status in
+ [(0,Ast.Ident("__intros",None)),status],
+ init_cache ~facts ~unit_eq () ~trace
+ | _ -> [],cache
;;
-let reduce ~depth status g =
+let reduce ~whd ~depth status g =
let n,h,metasenv,subst,o = status#obj in
let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
let ty = NCicUntrusted.apply_subst subst ctx ty in
- let ty' = NCicReduction.whd ~subst ctx ty in
+ let ty' =
+ (if whd then NCicReduction.whd else NCicTacReduction.normalize) ~subst ctx ty
+ in
if ty = ty' then []
else
(debug_print ~depth
;;
let do_something signature flags status g depth gty cache =
+ let l0, cache = intros ~depth status cache in
+ if l0 <> [] then l0, cache
+ else
(* whd *)
- let l = reduce ~depth status g in
+ let l = (*reduce ~whd:true ~depth status g @*) reduce ~whd:true ~depth status g in
(* if l <> [] then l,cache else *)
(* backward aplications *)
let l1 =
raise (Gaveup IntSet.empty)
else
let status = NTactics.branch_tac ~force:true status in
- let status, cache = intros ~depth status cache in
let g,gctx, gty = current_goal status in
let ctx,ty = close status g in
let closegty = mk_cic_term ctx ty in
debug_print (~depth:depth)
(lazy ("Case: " ^ CicNotationPp.pp_term t));
let depth,cache =
- if t=Ast.Ident("__whd",None) then depth, cache
+ if t=Ast.Ident("__whd",None) ||
+ t=Ast.Ident("__intros",None)
+ then depth, cache
else depth+1,loop_cache in
let cache = add_to_trace ~depth cache t in
try
debug_print (lazy ("proved at depth " ^ string_of_int x));
List.iter (toref incr_uses statistics) trace;
let trace = cleanup_trace s trace in
- let _ = print (pptrace trace) in
+ let _ = debug_print (pptrace trace) in
let stack =
match s#stack with
| (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
projects / helm.git / blobdiff