substaux 1 what where
;;
+(* replaces in a term a term with another one. *)
+(* Lifting are performed as usual. *)
+let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
+ let rec substaux k =
+ let module C = Cic in
+ let module S = CicSubstitution in
+ function
+ t when (equality t what) -> S.lift (k-1) with_what
+ | C.Rel n as t ->
+ if n < k then C.Rel n else C.Rel (n + nnn)
+ | C.Var (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
+ in
+ C.Var (uri,exp_named_subst')
+ | C.Meta (i, l) as t ->
+ let l' =
+ List.map
+ (function
+ None -> None
+ | Some t -> Some (substaux k t)
+ ) l
+ in
+ C.Meta(i,l')
+ | C.Sort _ as t -> t
+ | C.Implicit as t -> t
+ | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty)
+ | C.Prod (n,s,t) ->
+ C.Prod (n, substaux k s, substaux (k + 1) t)
+ | C.Lambda (n,s,t) ->
+ C.Lambda (n, substaux k s, substaux (k + 1) t)
+ | C.LetIn (n,s,t) ->
+ C.LetIn (n, substaux k s, substaux (k + 1) t)
+ | C.Appl (he::tl) ->
+ (* Invariant: no Appl applied to another Appl *)
+ let tl' = List.map (substaux k) tl in
+ begin
+ match substaux k he with
+ C.Appl l -> C.Appl (l@tl')
+ | _ as he' -> C.Appl (he'::tl')
+ end
+ | C.Appl _ -> assert false
+ | C.Const (uri,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
+ in
+ C.Const (uri,exp_named_subst')
+ | C.MutInd (uri,i,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
+ in
+ C.MutInd (uri,i,exp_named_subst')
+ | C.MutConstruct (uri,i,j,exp_named_subst) ->
+ let exp_named_subst' =
+ List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
+ in
+ C.MutConstruct (uri,i,j,exp_named_subst')
+ | C.MutCase (sp,i,outt,t,pl) ->
+ C.MutCase (sp,i,substaux k outt, substaux k t,
+ List.map (substaux k) pl)
+ | C.Fix (i,fl) ->
+ let len = List.length fl in
+ let substitutedfl =
+ List.map
+ (fun (name,i,ty,bo) ->
+ (name, i, substaux k ty, substaux (k+len) bo))
+ fl
+ in
+ C.Fix (i, substitutedfl)
+ | C.CoFix (i,fl) ->
+ let len = List.length fl in
+ let substitutedfl =
+ List.map
+ (fun (name,ty,bo) ->
+ (name, substaux k ty, substaux (k+len) bo))
+ fl
+ in
+ C.CoFix (i, substitutedfl)
+ in
+let res =
+ substaux 1 where
+in prerr_endline ("@@@@ risultato replace: " ^ (CicPp.ppterm res)); res
+;;
+
(* Takes a well-typed term and fully reduces it. *)
(*CSC: It does not perform reduction in a Case *)
let reduce context =
(* ANCORA DA DEBUGGARE *)
-
-(* IN FASE DI IMPLEMENTAZIONE *)
-
let generalize_tac ~term ~status:((proof,goal) as status) =
let module C = Cic in
let module P = PrimitiveTactics in
let module T = Tacticals in
let _,metasenv,_,_ = proof in
let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
-
-(*
-let uno = (C.Appl [
- C.MutConstruct (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind", 0, 2, []) ;
- C.MutConstruct (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind", 0, 1, [])]) in
- let tuno = CicTypeChecker.type_of_aux' metasenv context uno in
-prerr_endline ("#### uno: " ^ CicPp.ppterm uno);
-prerr_endline ("#### tuno: " ^ CicPp.ppterm tuno);
-*)
-prerr_endline ("#### dummy: " ^ (CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv context term)));
-prerr_endline ("#### with_what: " ^ CicPp.ppterm (C.Rel 1));
-prerr_endline ("#### term: " ^ CicPp.ppterm term);
-prerr_endline ("#### ty: " ^ CicPp.ppterm ty);
-
-
T.thens
~start:(P.cut_tac
~term:(
C.Prod (
- (C.Name "dummy_for_gen"),
- (CicTypeChecker.type_of_aux' metasenv context term),
- (ProofEngineReduction.replace_lifting
+ (C.Name "dummy_for_gen")),
+ (CicTypeChecker.type_of_aux' metasenv context term)),
+ (ProofEngineReduction.replace_lifting_csc 1
~equality:(==)
- ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *)
~what:term
- ~where:ty))))
- ~continuations:
- [T.id_tac ; (P.apply_tac ~term:(C.Appl [(C.Rel 1); term]))] (* in quest'ordine o viceversa? provare *)
-(* [(P.apply_tac ~term:(C.Appl [(C.Rel 1); term])) ; T.id_tac] (* in quest'ordine o viceversa? provare *)*)
+ ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *)
+ ~where:ty)
+ )
+ ~continuations: [(P.apply_tac ~term:(C.Rel 1)) ; T.id_tac]
~status
;;
-(*
-let generalize_tac ~term ~status:((proof,goal) as status) =
- let module C = Cic in
- let module H = ProofEngineHelpers in
- let module P = PrimitiveTactics in
- let module T = Tacticals in
- let _,metasenv,_,_ = proof in
- let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
-
- let add_decl_tac ~term ~status:(proof, goal) =
- let module C = Cic in
- let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
- let _ = CicTypeChecker.type_of_aux' metasenv context term in
- let newmeta = H.new_meta ~proof in
- let context_for_newmeta = (Some (C.Name "dummy_for_gen",C.Decl term))::context in
- let irl = H.identity_relocation_list_for_metavariable context_for_newmeta in
- let newmetaty = CicSubstitution.lift 1 ty in
- let bo' = C.LetIn (C.Name "dummy_for_gen" , term , C.Meta (newmeta,irl)) in
- let (newproof, _) = H.subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty]
- in
- (newproof, [newmeta])
-
- in
- T.then_
- ~start:(add_decl_tac ~term:(CicTypeChecker.type_of_aux' metasenv context term))
- ~continuation:(
-T.id_tac) (* T.thens
- ~start:(P.cut_tac ~term:(ProofEngineReduction.replace
- ~equality:(==)
- ~with_what:(C.Rel 1) (* dummy_for_gen *)
- ~what:term
- ~where:ty))
- ~continuations:
- [T.id_tac ; (P.apply_tac ~term:(C.Appl [term ; (C.Rel 1)]))]) (* in quest'ordine o viceversa? provare *)
-(* [(P.apply_tac ~term:(C.Appl [term ; (C.Rel 1)])) ; T.id_tac]) in quest'ordine o viceversa? provare *)
-*) ~status
-;;
-*)
-
+(* IN FASE DI IMPLEMENTAZIONE *)
let decide_equality_tac =
Tacticals.id_tac
(*** DOMANDE ***
-- come faccio clear di un ipotesi di cui non so il nome?
-- differenza tra elim e induction ...e inversion?
-- come passo a decompose la lista di termini?
-- ma la rewrite funzionava?
-- come implemento la generalize?
+- field, omega... come ring?
*)
projects / helm.git / commitdiff