+ let metasenv' =
+ List.map
+ (function
+ (n,_,_) when n = metano -> (metano,context',ty')
+ | _ as t -> t
+ ) metasenv
+ in
+ proof := Some (curi,metasenv',pbo,pty) ;
+ goal := Some metano
+
+(* Reduces [term] using [reduction_function] in the current scratch goal [ty] *)
+let reduction_tactic_in_scratch reduction_function term ty =
+ let metasenv =
+ match !proof with
+ None -> []
+ | Some (_,metasenv,_,_) -> metasenv
+ in
+ let metano,context,_ =
+ match !goal with
+ None -> assert false
+ | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
+ in
+ let term' = reduction_function context term in
+ ProofEngineReduction.replace
+ ~equality:(==) ~what:term ~with_what:term' ~where:ty
+
+let whd = reduction_tactic CicReduction.whd
+let reduce = reduction_tactic ProofEngineReduction.reduce
+let simpl = reduction_tactic ProofEngineReduction.simpl
+
+let whd_in_scratch = reduction_tactic_in_scratch CicReduction.whd
+let reduce_in_scratch =
+ reduction_tactic_in_scratch ProofEngineReduction.reduce
+let simpl_in_scratch =
+ reduction_tactic_in_scratch ProofEngineReduction.simpl
+
+(* It is just the opposite of whd. The code should probably be merged. *)
+let fold term =
+ 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 term' = CicReduction.whd context term in
+ (* We don't know if [term] is a subterm of [ty] or a subterm of *)
+ (* the type of one metavariable. So we replace it everywhere. *)
+ (*CSC: ma si potrebbe ovviare al problema. Ma non credo *)
+ (*CSC: che si guadagni nulla in fatto di efficienza. *)
+ let replace =
+ ProofEngineReduction.replace
+ ~equality:(ProofEngineReduction.syntactic_equality)
+ ~what:term' ~with_what:term
+ in
+ let ty' = replace ty in
+ let context' =
+ List.map
+ (function
+ Some (n,Cic.Decl t) -> Some (n,Cic.Decl (replace t))
+ | Some (n,Cic.Def t) -> Some (n,Cic.Def (replace t))
+ | None -> None
+ ) context
+ in
+ let metasenv' =
+ List.map
+ (function
+ (n,_,_) when n = metano -> (metano,context',ty')
+ | _ as t -> t
+ ) metasenv
+ in
+ proof := Some (curi,metasenv',pbo,pty) ;
+ goal := Some metano
+
+exception NotConvertible
+
+(*CSC: Bug (or feature?). [input] is parsed in the context of the goal, *)
+(*CSC: while [goal_input] can have a richer context (because of binders) *)
+(*CSC: So it is _NOT_ possible to use those binders in the [input] term. *)
+(*CSC: Is that evident? Is that right? Or should it be changed? *)
+let change ~goal_input ~input =
+ 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
+ (* are_convertible works only on well-typed terms *)
+ ignore (CicTypeChecker.type_of_aux' metasenv context input) ;
+ if CicReduction.are_convertible context goal_input input then
+ begin
+ let replace =
+ ProofEngineReduction.replace
+ ~equality:(==) ~what:goal_input ~with_what:input
+ 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
+ proof := Some (curi,metasenv',pbo,pty) ;
+ goal := Some metano
+ end
+ else
+ raise NotConvertible
+
+(************************************************************)
+(* Tactics defined elsewhere *)
+(************************************************************)
+
+ (* primitive tactics *)
+
+let apply term = apply_tactic (PrimitiveTactics.apply_tac ~term)
+let intros () =
+ apply_tactic (PrimitiveTactics.intros_tac ~name:(fresh_name ()))
+let cut term = apply_tactic (PrimitiveTactics.cut_tac ~term)
+let letin term = apply_tactic (PrimitiveTactics.letin_tac ~term)
+let exact term = apply_tactic (PrimitiveTactics.exact_tac ~term)
+let elim_intros_simpl term =
+ apply_tactic (PrimitiveTactics.elim_intros_simpl_tac ~term)
+
+ (* structural tactics *)
+
+let clearbody hyp = apply_tactic (ProofEngineStructuralRules.clearbody ~hyp)
+let clear hyp = apply_tactic (ProofEngineStructuralRules.clear ~hyp)
+
+ (* other tactics *)
+
+let elim_type term = apply_tactic (Ring.elim_type_tac ~term)
+let ring () = apply_tactic Ring.ring_tac
+let fourier () = apply_tactic FourierR.fourier_tac