| 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) do_whd t
+ let ctx = (Some (n',(C.Decl s)))::context in
+ collect_context ctx (howmany - 1) do_whd t
in
(context',ty,C.Lambda(n',s,bo))
| C.LetIn (n,s,t) ->
new_fresh_meta,newmetasenvfragment,exp_named_subst',exp_named_subst_diff
;;
-let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty goal_arity =
+let new_metasenv_and_unify_and_t newmeta' metasenv' subst context term' ty termty goal_arity =
let (consthead,newmetasenv,arguments,_) =
TermUtil.saturate_term newmeta' metasenv' context termty
goal_arity in
let subst,newmetasenv',_ =
- CicUnification.fo_unif newmetasenv context consthead ty CicUniv.empty_ugraph
+ CicUnification.fo_unif_subst
+ subst context newmetasenv consthead ty CicUniv.empty_ugraph
in
let t =
if List.length arguments = 0 then term' else Cic.Appl (term'::arguments)
let subst,newmetasenv',t =
let rec add_one_argument n =
try
- new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty
+ new_metasenv_and_unify_and_t newmeta' metasenv' subst context term' ty
termty n
with CicUnification.UnificationFailure _ when n > 0 ->
add_one_argument (n - 1)
ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof metano subst_in
newmetasenv''
in
- let subst = ((metano,(context,bo',Cic.Implicit None))::subst) in
+ let subst = ((metano,(context,bo',ty))::subst) in
subst,
(newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas),
max maxmeta (CicMkImplicit.new_meta newmetasenv''' subst)
TC.type_of_aux' metasenv' context eliminator_ref ugraph in
(* FG: ADDED PART ***********************************************************)
(* FG: we can not assume eliminator is the default eliminator ***************)
+(*
let add_lambdas n t =
let rec aux n t =
if n <= 0 then t
in
aux n (S.lift n t)
in
+*)
let rec args_init n f =
if n <= 0 then [] else f n :: args_init (pred n) f
in
| _, C.Appl (C.Rel i :: _) when i > 1 && i <= args_no -> i
| _ -> raise NotAnEliminator
in
+(*
let _, lambdas = PEH.split_with_whd (List.nth splits pred_pos) in
let termty_ty =
let termty_ty,_ugraph = TC.type_of_aux' metasenv' context termty ugraph in
CicReduction.whd context termty_ty
in
+*)
(*
let metasenv', term, pred, upto = match cpatt, termty_ty with
| C.Implicit (Some `Hole), _
let module U = UriManager in
let module R = CicReduction in
let module C = Cic in
- let (curi,metasenv,proofbo,proofty, attrs) = proof in
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let termty,_ = TC.type_of_aux' metasenv context term CicUniv.empty_ugraph in
- let termty = CicReduction.whd context termty in
- let (termty,metasenv',arguments,fresh_meta) =
- TermUtil.saturate_term
- (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in
- let term = if arguments = [] then term else Cic.Appl (term::arguments) in
- let uri,exp_named_subst,typeno,args =
- match termty with
- C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
- | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) ->
- (uri,exp_named_subst,typeno,args)
- | _ -> raise NotAnInductiveTypeToEliminate
- in
- let paramsno,itty,patterns =
- match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
- C.InductiveDefinition (tys,_,paramsno,_),_ ->
- 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) ->
- let fresh_name =
- mk_fresh_name_callback metasenv' context name
- (*CSC: WRONG TYPE HERE: I can get a "bad" name*)
- ~typ:source
- in
- C.Lambda (fresh_name,C.Implicit None,
- aux 0 (Some (fresh_name,C.Decl source)::context) target)
- | n,C.Prod (name,source,target) ->
- let fresh_name =
- mk_fresh_name_callback metasenv' context name
- (*CSC: WRONG TYPE HERE: I can get a "bad" name*)
- ~typ:source
- in
- aux (n-1) (Some (fresh_name,C.Decl source)::context) target
- | 0,_ -> C.Implicit None
- | _,_ -> assert false
- in
- paramsno,itty,
- List.map (function (_,cty) -> aux paramsno context cty) cl
- | _ -> assert false
- in
- let outtype =
- let target =
- C.Lambda (C.Name "fixme",C.Implicit None,
- ProofEngineReduction.replace_lifting
- ~equality:(ProofEngineReduction.alpha_equivalence)
- ~what:[CicSubstitution.lift (paramsno+1) term]
- ~with_what:[C.Rel (paramsno+1)]
- ~where:(CicSubstitution.lift (paramsno+1) ty))
+ let (curi,metasenv,proofbo,proofty, attrs) = proof in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+ let termty,_ = TC.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+ let termty = CicReduction.whd context termty in
+ let (termty,metasenv',arguments,fresh_meta) =
+ TermUtil.saturate_term
+ (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in
+ let term = if arguments = [] then term else Cic.Appl (term::arguments) in
+ let uri,exp_named_subst,typeno,args =
+ match termty with
+ | C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
+ | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) ->
+ (uri,exp_named_subst,typeno,args)
+ | _ -> raise NotAnInductiveTypeToEliminate
+ in
+ let paramsno,itty,patterns,right_args =
+ match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
+ | C.InductiveDefinition (tys,_,paramsno,_),_ ->
+ let _,left_parameters,right_args =
+ List.fold_right
+ (fun x (n,acc1,acc2) ->
+ if n > 0 then (n-1,acc1,x::acc2) else (n,x::acc1,acc2))
+ args (List.length args - paramsno, [],[])
in
- let rec add_lambdas =
- function
- 0 -> target
- | n -> C.Lambda (C.Name "fixme",C.Implicit None,add_lambdas (n-1))
- in
- add_lambdas (count_prods context itty - paramsno)
- in
- let term_to_refine =
- C.MutCase (uri,typeno,outtype,term,patterns)
+ let _,_,itty,cl = List.nth tys typeno in
+ let rec aux left_parameters context t =
+ match left_parameters,CicReduction.whd context t with
+ | [],C.Prod (name,source,target) ->
+ let fresh_name =
+ mk_fresh_name_callback metasenv' context name ~typ:source
+ in
+ C.Lambda (fresh_name,C.Implicit None,
+ aux [] (Some (fresh_name,C.Decl source)::context) target)
+ | hd::tl,C.Prod (name,source,target) ->
+ (* left parameters instantiation *)
+ aux tl context (CicSubstitution.subst hd target)
+ | [],_ -> C.Implicit None
+ | _ -> assert false
in
- let refined_term,_,metasenv'',_ =
- CicRefine.type_of_aux' metasenv' context term_to_refine
- CicUniv.empty_ugraph
+ paramsno,itty,
+ List.map (function (_,cty) -> aux left_parameters context cty) cl,
+ right_args
+ | _ -> assert false
+ in
+ let outtype =
+ let n_right_args = List.length right_args in
+ let n_lambdas = n_right_args + 1 in
+ let lifted_ty = CicSubstitution.lift n_lambdas ty in
+ let captured_ty =
+ let what =
+ List.map (CicSubstitution.lift n_lambdas) (right_args)
+ in
+ let with_what meta =
+ let rec mkargs = function
+ | 0 -> assert false
+ | 1 -> []
+ | n ->
+ (if meta then Cic.Implicit None else Cic.Rel n)::(mkargs (n-1))
in
- let new_goals =
- ProofEngineHelpers.compare_metasenvs
- ~oldmetasenv:metasenv ~newmetasenv:metasenv''
- 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
- List.filter
- (function i -> List.exists (function (j,_,_) -> j=i) metasenv'''
- ) new_goals @ new_goals'
- in
- proof'', patched_new_goals
- in
+ mkargs n_lambdas
+ in
+ let replaced = ref false in
+ let replace = ProofEngineReduction.replace_lifting
+ ~equality:(fun _ a b -> let rc = CicUtil.alpha_equivalence a b in
+ if rc then replaced := true; rc)
+ ~context:[]
+ in
+ let captured =
+ replace ~what:[CicSubstitution.lift n_lambdas term]
+ ~with_what:[Cic.Rel 1] ~where:lifted_ty
+ in
+ if not !replaced then
+ (* this means the matched term is not there,
+ * but maybe right params are: we user rels (to right args lambdas) *)
+ replace ~what ~with_what:(with_what false) ~where:captured
+ else
+ (* since the matched is there, rights should be inferrable *)
+ replace ~what ~with_what:(with_what true) ~where:captured
+ in
+ let captured_term_ty =
+ let term_ty = CicSubstitution.lift n_right_args termty in
+ let rec mkrels = function 0 -> []|n -> (Cic.Rel n)::(mkrels (n-1)) in
+ let rec fstn acc l n =
+ if n = 0 then acc else fstn (acc@[List.hd l]) (List.tl l) (n-1)
+ in
+ match term_ty with
+ | C.MutInd _ -> term_ty
+ | C.Appl ((C.MutInd (a,b,c))::args) ->
+ C.Appl ((C.MutInd (a,b,c))::
+ fstn [] args paramsno @ mkrels n_right_args)
+ | _ -> raise NotAnInductiveTypeToEliminate
+ in
+ let rec add_lambdas = function
+ | 0 -> captured_ty
+ | 1 ->
+ C.Lambda (C.Name "matched", captured_term_ty, (add_lambdas 0))
+ | n ->
+ C.Lambda (C.Name ("right_"^(string_of_int (n-1))),
+ C.Implicit None, (add_lambdas (n-1)))
+ in
+ add_lambdas n_lambdas
+ in
+ let term_to_refine = C.MutCase (uri,typeno,outtype,term,patterns) in
+ let refined_term,_,metasenv'',_ =
+ CicRefine.type_of_aux' metasenv' context term_to_refine
+ CicUniv.empty_ugraph
+ in
+ let new_goals =
+ ProofEngineHelpers.compare_metasenvs
+ ~oldmetasenv:metasenv ~newmetasenv:metasenv''
+ 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
+ List.filter
+ (function i -> List.exists (function (j,_,_) -> j=i) metasenv''')
+ new_goals @ new_goals'
+ in
+ proof'', patched_new_goals
+ in
mk_tactic (cases_tac ~term)
;;
projects / helm.git / blobdiff