let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
res,newmetasenv,arguments,newmeta,lastmeta
-let apply_tac ~status:(proof, goal) ~term =
+let apply_tac ~term ~status:(proof, goal) =
(* Assumption: The term "term" must be closed in the current context *)
let module T = CicTypeChecker in
let module R = CicReduction in
let module C = Cic in
- let metasenv =
- match proof with
- None -> assert false
- | Some (_,metasenv,_,_) -> metasenv
- in
- let metano,context,ty =
- match goal with
- None -> assert false
- | Some metano ->
- List.find (function (m,_,_) -> m=metano) metasenv
- in
+ let (_,metasenv,_,_) = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
let termty = CicTypeChecker.type_of_aux' metasenv context term in
(* newmeta is the lowest index of the new metas introduced *)
let (consthead,newmetas,arguments,newmeta,_) =
subst_meta_and_metasenv_in_proof
proof metano subst_in newmetasenv''
in
- (newproof,
- (match newmetasenv''' with
- | [] -> None
- | (i,_,_)::_ -> Some i))
+ (newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas)
(* TODO per implementare i tatticali e' necessario che tutte le tattiche
sollevino _solamente_ Fail *)
-let apply_tac ~status ~term =
+let apply_tac ~term ~status =
try
- apply_tac ~status ~term
+ apply_tac ~term ~status
(* TODO cacciare anche altre eccezioni? *)
with CicUnification.UnificationFailed as e ->
raise (Fail (Printexc.to_string e))
-let intros_tac ~status:(proof, goal) ~name =
+let intros_tac ~name ~status:(proof, goal) =
let module C = Cic in
let module R = CicReduction in
- let metasenv =
- match proof with
- None -> assert false
- | Some (_,metasenv,_,_) -> metasenv
- in
- let metano,context,ty =
- match goal with
- None -> assert false
- | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
- in
+ let (_,metasenv,_,_) = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
let newmeta = new_meta ~proof in
let (context',ty',bo') = lambda_abstract context newmeta ty name in
let (newproof, _) =
subst_meta_in_proof proof metano bo' [newmeta,context',ty']
in
- let newgoal = Some newmeta in
- (newproof, newgoal)
+ (newproof, [newmeta])
-let cut_tac ~status:(proof, goal) ~term =
+let cut_tac ~term ~status:(proof, goal) =
let module C = Cic in
- let curi,metasenv,pbo,pty =
- match proof with
- None -> assert false
- | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
- in
- let metano,context,ty =
- match goal with
- None -> assert false
- | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
- in
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
let newmeta1 = new_meta ~proof in
let newmeta2 = newmeta1 + 1 in
let context_for_newmeta1 =
subst_meta_in_proof proof metano bo'
[newmeta2,context,term; newmeta1,context_for_newmeta1,newmeta1ty];
in
- let newgoal = Some newmeta1 in
- (newproof, newgoal)
+ (newproof, [newmeta1 ; newmeta2])
-let letin_tac ~status:(proof, goal) ~term =
+let letin_tac ~term ~status:(proof, goal) =
let module C = Cic in
- let curi,metasenv,pbo,pty =
- match proof with
- None -> assert false
- | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
- in
- let metano,context,ty =
- match goal with
- None -> assert false
- | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
- 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 = new_meta ~proof in
let context_for_newmeta =
subst_meta_in_proof
proof metano bo'[newmeta,context_for_newmeta,newmetaty]
in
- let newgoal = Some newmeta in
- (newproof, newgoal)
+ (newproof, [newmeta])
(** functional part of the "exact" tactic *)
-let exact_tac ~status:(proof, goal) ~term =
+let exact_tac ~term ~status:(proof, goal) =
(* Assumption: the term bo must be closed in the current context *)
- let metasenv =
- match proof with
- None -> assert false
- | Some (_,metasenv,_,_) -> metasenv
- in
- let metano,context,ty =
- match goal with
- None -> assert false
- | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
- in
+ let (_,metasenv,_,_) = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
let module T = CicTypeChecker in
let module R = CicReduction in
if R.are_convertible context (T.type_of_aux' metasenv context term) ty then
begin
let (newproof, metasenv') =
subst_meta_in_proof proof metano term [] in
- let newgoal =
- (match metasenv' with
- [] -> None
- | (n,_,_)::_ -> Some n)
- in
- (newproof, newgoal)
+ (newproof, [])
end
else
raise (Fail "The type of the provided term is not the one expected.")
(* not really "primite" tactics .... *)
-let elim_intros_simpl_tac ~status:(proof, goal) ~term =
+let elim_intros_simpl_tac ~term ~status:(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 =
- match proof with
- None -> assert false
- | Some (curi,metasenv,_,_) -> curi,metasenv
- in
- let metano,context,ty =
- match goal with
- None -> assert false
- | Some metano ->
- List.find (function (m,_,_) -> m=metano) metasenv
- in
+ let (curi,metasenv,_,_) = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
let termty = T.type_of_aux' metasenv context term in
let uri,cookingno,typeno,args =
match termty with
proof metano apply_subst' newmetasenv'''
in
(newproof,
- (match newmetasenv'''' with
- | [] -> None
- | (i,_,_)::_ -> Some i))
+ List.map (function (i,_,_) -> i) new_uninstantiatedmetas)
+
+exception NotConvertible
+
+(*CSC: Bug (or feature?). [with_what] is parsed in the context of the goal, *)
+(*CSC: while [what] can have a richer context (because of binders) *)
+(*CSC: So it is _NOT_ possible to use those binders in the [with_what] term. *)
+(*CSC: Is that evident? Is that right? Or should it be changed? *)
+let change_tac ~what ~with_what ~status:(proof, goal) =
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ (* are_convertible works only on well-typed terms *)
+ ignore (CicTypeChecker.type_of_aux' metasenv context with_what) ;
+ if CicReduction.are_convertible context what with_what then
+ begin
+ let replace =
+ ProofEngineReduction.replace ~equality:(==) ~what ~with_what
+ in
+ let ty' = replace ty in
+ let context' =
+ List.map
+ (function
+ Some (name,Cic.Def t) -> Some (name,Cic.Def (replace t))
+ | Some (name,Cic.Decl t) -> Some (name,Cic.Decl (replace t))
+ | None -> None
+ ) context
+ in
+ let metasenv' =
+ List.map
+ (function
+ (n,_,_) when n = metano -> (metano,context',ty')
+ | _ as t -> t
+ ) metasenv
+ in
+ (curi,metasenv',pbo,pty), [metano]
+ end
+ else
+ raise (ProofEngineTypes.Fail "Not convertible")
projects / helm.git / blobdiff