(* howmany = -1 means Intros, howmany > 0 means Intros n *)
let lambda_abstract ?(howmany=(-1)) metasenv context newmeta ty mk_fresh_name =
let module C = Cic in
- let rec collect_context context howmany ty =
+ let rec collect_context context howmany do_whd ty =
match howmany with
| 0 ->
let irl =
context, ty, (C.Meta (newmeta,irl))
| _ ->
match ty with
- C.Cast (te,_) -> collect_context context howmany te
+ C.Cast (te,_) -> collect_context context howmany do_whd te
| C.Prod (n,s,t) ->
let n' = mk_fresh_name metasenv context n ~typ:s in
let (context',ty,bo) =
- collect_context ((Some (n',(C.Decl s)))::context) (howmany - 1) t
+ collect_context ((Some (n',(C.Decl s)))::context) (howmany - 1) do_whd t
in
(context',ty,C.Lambda(n',s,bo))
| C.LetIn (n,s,t) ->
let (context',ty,bo) =
- collect_context ((Some (n,(C.Def (s,None))))::context) (howmany - 1) t
+ collect_context ((Some (n,(C.Def (s,None))))::context) (howmany - 1) do_whd t
in
(context',ty,C.LetIn(n,s,bo))
| _ as t ->
CicMkImplicit.identity_relocation_list_for_metavariable context
in
context, t, (C.Meta (newmeta,irl))
- else
+ else if do_whd then
+ let t = CicReduction.whd ~delta:true context t in
+ collect_context context howmany false t
+ else
raise (Fail (lazy "intro(s): not enough products or let-ins"))
in
- collect_context context howmany ty
+ collect_context context howmany true ty
let eta_expand metasenv context t arg =
let module T = CicTypeChecker in
let module T = CicTypeChecker in
let module R = CicReduction in
let module C = Cic in
- let (_,metasenv,_,_) = proof in
+ let (_,metasenv,_,_, _) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let newmeta = max (CicMkImplicit.new_meta metasenv subst) maxmeta in
let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
=
let module C = Cic in
let module R = CicReduction in
- let (_,metasenv,_,_) = proof in
+ let (_,metasenv,_,_, _) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
let (context',ty',bo') =
term (proof, goal)
=
let module C = Cic in
- let curi,metasenv,pbo,pty = proof in
+ let curi,metasenv,pbo,pty, attrs = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let newmeta1 = ProofEngineHelpers.new_meta_of_proof ~proof in
let newmeta2 = newmeta1 + 1 in
term (proof, goal)
=
let module C = Cic in
- let curi,metasenv,pbo,pty = proof in
+ let curi,metasenv,pbo,pty, attrs = proof in
(* occur check *)
let occur i t =
let m = CicUtil.metas_of_term t in
let exact_tac ~term =
let exact_tac ~term (proof, goal) =
(* Assumption: the term bo must be closed in the current context *)
- let (_,metasenv,_,_) = proof in
+ let (_,metasenv,_,_, _) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let module T = CicTypeChecker in
let module R = CicReduction in
mk_tactic (exact_tac ~term)
(* not really "primitive" tactics .... *)
-let elim_tac ~term =
- let elim_tac ~term (proof, goal) =
+let elim_tac ?using ~term =
+ let elim_tac (proof, goal) =
let module T = CicTypeChecker in
let module U = UriManager in
let module R = CicReduction in
let module C = Cic in
- let (curi,metasenv,proofbo,proofty) = proof in
+ let (curi,metasenv,proofbo,proofty, attrs) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
let termty = CicReduction.whd context termty in
in
U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con")
in
- let eliminator_ref = C.Const (eliminator_uri,exp_named_subst) in
+ let eliminator_ref = match using with
+ | None -> C.Const (eliminator_uri,exp_named_subst)
+ | Some t -> t
+ in
let ety,_ =
T.type_of_aux' metasenv' context eliminator_ref CicUniv.empty_ugraph in
let rec find_args_no =
ProofEngineHelpers.compare_metasenvs
~oldmetasenv:metasenv ~newmetasenv:metasenv''
in
- let proof' = curi,metasenv'',proofbo,proofty in
+ let proof' = curi,metasenv'',proofbo,proofty, attrs in
let proof'', new_goals' =
apply_tactic (apply_tac ~term:refined_term) (proof',goal)
in
(* The apply_tactic can have closed some of the new_goals *)
let patched_new_goals =
- let (_,metasenv''',_,_) = proof'' in
+ let (_,metasenv''',_,_, _) = proof'' in
List.filter
(function i -> List.exists (function (j,_,_) -> j=i) metasenv'''
) new_goals @ new_goals'
in
proof'', patched_new_goals
in
- mk_tactic (elim_tac ~term)
+ mk_tactic elim_tac
;;
let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
let module U = UriManager in
let module R = CicReduction in
let module C = Cic in
- let (curi,metasenv,proofbo,proofty) = proof in
+ let (curi,metasenv,proofbo,proofty, attrs) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
let termty = CicReduction.whd context termty in
(uri,exp_named_subst,typeno,args)
| _ -> raise NotAnInductiveTypeToEliminate
in
- let paramsno,patterns =
+ let paramsno,itty,patterns =
match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
C.InductiveDefinition (tys,_,paramsno,_),_ ->
- let _,_,_,cl = List.nth tys typeno in
+ let _,_,itty,cl = List.nth tys typeno in
let rec aux n context t =
match n,CicReduction.whd context t with
0,C.Prod (name,source,target) ->
| 0,_ -> C.Implicit None
| _,_ -> assert false
in
- paramsno,
+ paramsno,itty,
List.map (function (_,cty) -> aux paramsno context cty) cl
| _ -> assert false
in
0 -> target
| n -> C.Lambda (C.Name "fixme",C.Implicit None,add_lambdas (n-1))
in
- add_lambdas paramsno
+ add_lambdas (count_prods context itty - paramsno)
in
let term_to_refine =
C.MutCase (uri,typeno,outtype,term,patterns)
in
-prerr_endline (CicMetaSubst.ppterm_in_context ~metasenv:metasenv' [] term_to_refine context);
let refined_term,_,metasenv'',_ =
CicRefine.type_of_aux' metasenv' context term_to_refine
CicUniv.empty_ugraph
ProofEngineHelpers.compare_metasenvs
~oldmetasenv:metasenv ~newmetasenv:metasenv''
in
- let proof' = curi,metasenv'',proofbo,proofty in
+ let proof' = curi,metasenv'',proofbo,proofty, attrs in
let proof'', new_goals' =
apply_tactic (apply_tac ~term:refined_term) (proof',goal)
in
(* The apply_tactic can have closed some of the new_goals *)
let patched_new_goals =
- let (_,metasenv''',_,_) = proof'' in
+ let (_,metasenv''',_,_,_) = proof'' in
List.filter
(function i -> List.exists (function (j,_,_) -> j=i) metasenv'''
) new_goals @ new_goals'
let elim_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
?depth ?using what =
- Tacticals.then_ ~start:(elim_tac ~term:what)
+ Tacticals.then_ ~start:(elim_tac ?using ~term:what)
~continuation:(intros_tac ~mk_fresh_name_callback ?howmany:depth ())
;;
(* The simplification is performed only on the conclusion *)
let elim_intros_simpl_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
?depth ?using what =
- Tacticals.then_ ~start:(elim_tac ~term:what)
+ Tacticals.then_ ~start:(elim_tac ?using ~term:what)
~continuation:
(Tacticals.thens
~start:(intros_tac ~mk_fresh_name_callback ?howmany:depth ())
let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in
let term = C.Sort C.Set in
let letout_tac (proof, goal) =
- let curi, metasenv, pbo, pty = proof in
+ let curi, metasenv, pbo, pty, attrs = proof in
let metano, context, ty = CicUtil.lookup_meta goal metasenv in
let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "hole") ~typ:term in
projects / helm.git / blobdiff