let proof = ref (None : proof option)
let goal = ref (None : goal option)
+let get_proof () = !proof;;
+let set_proof p = proof := p;;
+
let get_current_status_as_xml () =
- match !proof with
+ match get_proof () with
None -> assert false
| Some (uri, metasenv, bo, ty) ->
+ let uri = match uri with Some uri -> uri | None -> assert false in
let currentproof =
(*CSC: Wrong: [] is just plainly wrong *)
Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
in
let (acurrentproof,_,_,ids_to_inner_sorts,_,_,_) =
- Cic2acic.acic_object_of_cic_object currentproof
+ Cic2acic.acic_object_of_cic_object ~eta_fix:false currentproof
in
let xml, bodyxml =
match
;;
let apply_tactic ~tactic =
- match !proof,!goal with
+ match get_proof (),!goal with
| None,_
| _,None -> assert false
| Some proof', Some goal' ->
- let (newproof, newgoals) = tactic ~status:(proof', goal') in
- proof := Some newproof;
+ let (newproof, newgoals) = tactic (proof', goal') in
+ set_proof (Some newproof);
goal :=
(match newgoals, newproof with
goal::_, _ -> Some goal
C.Rel _ -> []
| C.Meta (n,_) -> [n]
| C.Sort _
- | C.Implicit -> []
+ | C.Implicit _ -> []
| C.Cast (te,ty) -> (aux te) @ (aux ty)
| C.Prod (_,s,t) -> (aux s) @ (aux t)
| C.Lambda (_,s,t) -> (aux s) @ (aux t)
(* are efficiency reasons. *)
let perforate context term ty =
let module C = Cic in
- match !proof with
+ match get_proof () with
None -> assert false
| Some (uri,metasenv,bo,gty as proof') ->
- let newmeta = new_meta proof' in
+ let newmeta = new_meta_of_proof proof' in
(* We push the new meta at the end of the list for pretty-printing *)
(* purposes: in this way metas are ordered. *)
let metasenv' = metasenv@[newmeta,context,ty] in
- let irl = identity_relocation_list_for_metavariable context in
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context
+ in
(*CSC: Bug: se ci sono due term uguali nella prova dovrei bucarne uno solo!!!*)
let bo' =
ProofEngineReduction.replace (==) [term] [C.Meta (newmeta,irl)] bo
let metasenv'' =
List.filter (function (n,_,_) -> List.mem n newmetas) metasenv'
in
- proof := Some (uri,metasenv'',bo',gty) ;
+ set_proof (Some (uri,metasenv'',bo',gty)) ;
goal := Some newmeta
(* Reduces [term] using [reduction_function] in the current scratch goal [ty] *)
let reduction_tactic_in_scratch reduction_function terms ty =
let metasenv =
- match !proof with
+ match get_proof () with
None -> []
| Some (_,metasenv,_,_) -> metasenv
in
let elim_type term = apply_tactic (EliminationTactics.elim_type_tac ~term)
let ring () = apply_tactic Ring.ring_tac
let fourier () = apply_tactic FourierR.fourier_tac
+let auto mqi_handle () = apply_tactic (VariousTactics.auto_tac mqi_handle)
let rewrite_simpl term = apply_tactic (EqualityTactics.rewrite_simpl_tac ~term)
let rewrite_back_simpl term = apply_tactic (EqualityTactics.rewrite_back_simpl_tac ~term)