match ProofEngine.get_proof () with
None -> assert false
| Some (uri,[],bo,ty) ->
+ let uri = match uri with Some uri -> uri | _ -> assert false in
+ (* we want to typecheck in the ENV *)
+ (*let old_working = CicUniv.get_working () in
+ CicUniv.set_working (CicUniv.get_global ());*)
+ CicUniv.directly_to_env_begin () ;
+ prerr_endline "-------------> QED";
if
CicReduction.are_convertible []
(CicTypeChecker.type_of_aux' [] [] bo) ty
let pathname = pathname_of_annuri (UriManager.buri_of_uri uri) in
make_dirs pathname ;
save_object_to_disk uri acic ids_to_inner_sorts ids_to_inner_types
- pathname
+ pathname;
+ (* add the object to the env *)
+ CicEnvironment.add_type_checked_term uri (
+ Cic.Constant ((UriManager.name_of_uri uri),(Some bo),ty,[]));
+ (* FIXME: the variable list!! *)
+ (*
+ CicUniv.qed (); (* now the env has the right constraints *)*)
+ CicUniv.directly_to_env_end();
+ CicUniv.reset_working ();
+ prerr_endline "-------------> FINE";
end
else
raise WrongProof
else
Hbugs.notify () ;
(*CSC: Wrong: [] is just plainly wrong *)
- uri,
- (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
+ let uri = match uri with Some uri -> uri | _ -> assert false in
+ (uri,
+ Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
in
ignore (output#load_proof uri currentproof)
with
match CicParser.obj_of_xml proof_file_type (Some proof_file) with
Cic.CurrentProof (_,metasenv,bo,ty,_) ->
typecheck_loaded_proof metasenv bo ty ;
- ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ;
+ ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty));
refresh_proof output ;
set_proof_engine_goal
(match metasenv with
interactive_user_uri_choice ~selection_mode ?ok
?enable_button_for_non_vars ~title ~msg
let interactive_interpretation_choice = interactive_interpretation_choice
- let input_or_locate_uri ~title ?id = input_or_locate_uri ~title
+ let input_or_locate_uri ~title ?id () = input_or_locate_uri ~title
end
;;
let metasenv,expr = !get_metasenv_and_term () in
let _ = CicTypeChecker.type_of_aux' metasenv [] expr in
ProofEngine.set_proof
- (Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)) ;
+ (Some (Some (!get_uri ()), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr));
set_proof_engine_goal (Some 1) ;
refresh_goals notebook ;
refresh_proof output ;
let notebook = (rendering_window ())#notebook in
try
let uri = input_or_locate_uri ~title:"Open" in
- CicTypeChecker.typecheck uri ;
+ ignore(CicTypeChecker.typecheck uri);
+ (* TASSI: typecheck mette la uri nell'env... cosa fa la open_ ?*)
let metasenv,bo,ty =
match CicEnvironment.get_cooked_obj uri with
Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
| Cic.Variable _
| Cic.InductiveDefinition _ -> raise NotADefinition
in
- ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ;
+ ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty)) ;
set_proof_engine_goal None ;
refresh_goals notebook ;
refresh_proof output ;