* http://helm.cs.unibo.it/
*)
-(******************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
-(* 06/01/2002 *)
-(* *)
-(* *)
-(******************************************************************************)
+(*****************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* 06/01/2002 *)
+(* *)
+(* *)
+(*****************************************************************************)
let debug_level = ref 1
let debug_print ?(level = 1) s = if !debug_level >= level then prerr_endline s
~database:(Helm_registry.get "db.database")
()
-let xlinkns = Gdome.domString "http://www.w3.org/1999/xlink";;
-
let restore_environment_on_boot = true ;;
let notify_hbugs_on_goal_change = false ;;
lazy
(let mmlwidget =
TermViewer.sequent_viewer
- ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent
+ ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent
~packing:scrolled_window#add ~width:400 ~height:280 () in
let expr =
let term = CicUtil.term_of_uri uri in
- (Cic.Cast (term, CicTypeChecker.type_of_aux' [] [] term))
+ (Cic.Cast (term, fst(CicTypeChecker.type_of_aux' [] [] term
+ CicUniv.empty_ugraph )))
in
try
mmlwidget#load_sequent [] (111,[],expr)
in
(* innertypes *)
let innertypesuri = UriManager.innertypesuri_of_uri uri in
- Xml.pp ~quiet:true xmlinnertypes (Some (path ^ ".types.xml")) ;
+ Xml.pp ~gzip:false xmlinnertypes (Some (path ^ ".types.xml")) ;
Http_getter.register' innertypesuri
(Helm_registry.get "local_library.url" ^
Str.replace_first (Str.regexp "^cic:") ""
(UriManager.string_of_uri innertypesuri) ^ ".xml"
) ;
(* constant type / variable / mutual inductive types definition *)
- Xml.pp ~quiet:true xml (Some (path ^ ".xml")) ;
+ Xml.pp ~gzip:false xml (Some (path ^ ".xml")) ;
Http_getter.register' uri
(Helm_registry.get "local_library.url" ^
Str.replace_first (Str.regexp "^cic:") ""
None -> assert false
| Some bodyuri -> bodyuri
in
- Xml.pp ~quiet:true bodyxml' (Some (path ^ ".body.xml")) ;
+ Xml.pp ~gzip:false bodyxml' (Some (path ^ ".body.xml")) ;
Http_getter.register' bodyuri
(Helm_registry.get "local_library.url" ^
Str.replace_first (Str.regexp "^cic:") ""
;;
let qed () =
- 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 () ;
- if
- CicReduction.are_convertible []
- (CicTypeChecker.type_of_aux' [] [] bo) ty
- then
- begin
- (*CSC: Wrong: [] is just plainly wrong *)
- let proof = Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[]) in
- let (acic,ids_to_inner_types,ids_to_inner_sorts) =
- (rendering_window ())#output#load_proof uri proof
- in
- !qed_set_sensitive false ;
- (* let's save the theorem and register it to the getter *)
- 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;
- (* 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 ();
- end
- else
- raise WrongProof
- | _ -> raise OpenConjecturesStillThere
+ 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 *)
+ prerr_endline "-------------> QED";
+ let ty_bo,u =
+ CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
+ let b,u1 = CicReduction.are_convertible [] ty_bo ty u in
+ if b then
+ begin
+ (*CSC: Wrong: [] is just plainly wrong *)
+ let proof =
+ Cic.Constant (UriManager.name_of_uri uri,Some bo,ty,[],[])
+ in
+ let (acic,ids_to_inner_types,ids_to_inner_sorts) =
+ (rendering_window ())#output#load_proof proof
+ in
+ !qed_set_sensitive false ;
+ (* let's save the theorem and register it to the getter *)
+ let pathname =
+ pathname_of_annuri (UriManager.buri_of_uri uri)
+ in
+ let list_of_universes =
+ CicUnivUtils.universes_of_obj uri
+ (Cic.Constant ("",None,ty,[],[]))
+ in
+ let u1_clean = CicUniv.clean_ugraph u1 list_of_universes in
+ let u2 = CicUniv.fill_empty_nodes_with_uri u1_clean uri in
+ (**********************************************
+ TASSI: to uncomment whe universes will be ON
+ ***********************************************)
+ (*
+ make_dirs pathname ;
+ save_object_to_disk uri acic ids_to_inner_sorts
+ ids_to_inner_types pathname;
+ *)
+ (* save the universe graph u2 *)
+ (* add the object to the env *)
+ CicEnvironment.add_type_checked_term uri ((
+ Cic.Constant ((UriManager.name_of_uri uri),
+ (Some bo),ty,[],[])),u2);
+ (* FIXME: the variable list!! *)
+ prerr_endline "-------------> FINE";
+ end
+ else
+ raise WrongProof
+ | _ -> raise OpenConjecturesStillThere
;;
(** save an unfinished proof on the filesystem *)
let (xml, bodyxml) = ProofEngine.get_current_status_as_xml () in
let proof_file_type = Helm_registry.get "gtoplevel.proof_file_type" in
let proof_file = Helm_registry.get "gtoplevel.proof_file" in
- Xml.pp ~quiet:true xml (Some proof_file_type) ;
+ Xml.pp ~gzip:false xml (Some proof_file_type) ;
HelmLogger.log
(`Msg (`T ("Current proof type saved to " ^ proof_file_type))) ;
- Xml.pp ~quiet:true bodyxml (Some proof_file) ;
+ Xml.pp ~gzip:false bodyxml (Some proof_file) ;
HelmLogger.log
(`Msg (`T ("Current proof body saved to " ^ proof_file)))
;;
ignore (
List.fold_left
(fun metasenv ((_,context,ty) as conj) ->
- ignore (T.type_of_aux' metasenv context ty) ;
+ ignore (T.type_of_aux' metasenv context ty CicUniv.empty_ugraph) ;
metasenv @ [conj]
) [] metasenv) ;
- ignore (T.type_of_aux' metasenv [] ty) ;
- ignore (T.type_of_aux' metasenv [] bo)
+ ignore (T.type_of_aux' metasenv [] ty CicUniv.empty_ugraph) ;
+ ignore (T.type_of_aux' metasenv [] bo CicUniv.empty_ugraph)
;;
let decompose_uris_choice_callback uris =
(*CSC: Wrong: [] is just plainly wrong *)
let uri = match uri with Some uri -> uri | _ -> assert false in
(uri,
- Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
+ Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[],[]))
in
- ignore (output#load_proof uri currentproof)
+ ignore (output#load_proof currentproof)
with
e ->
match ProofEngine.get_proof () with
None -> assert false
| Some (uri,metasenv,bo,ty) ->
- debug_print ("Offending proof: " ^ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[])));
+ debug_print ("Offending proof: " ^
+ CicPp.ppobj (Cic.CurrentProof ("questa",metasenv,bo,ty,[],[])));
raise (InvokeTactics.RefreshProofException e)
let set_proof_engine_goal g =
let proof_file_type = Helm_registry.get "gtoplevel.proof_file_type" in
let proof_file = Helm_registry.get "gtoplevel.proof_file" in
match CicParser.obj_of_xml proof_file_type (Some proof_file) with
- Cic.CurrentProof (_,metasenv,bo,ty,_) ->
+ Cic.CurrentProof (_,metasenv,bo,ty,_,_) ->
typecheck_loaded_proof metasenv bo ty ;
ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty));
refresh_proof output ;
let href = Gdome.domString "href" in
let show_in_show_window_obj uri obj =
try
- let
- (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,
- ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses)
- =
- Cic2acic.acic_object_of_cic_object obj
- in
- let mml =
- ChosenTransformer.mml_of_cic_object
- ~explode_all:false uri acic ids_to_inner_sorts ids_to_inner_types
+ let mml,(_,(ids_to_terms,ids_to_father_ids,ids_to_conjectures,
+ ids_to_hypotheses,_,_)) =
+ ApplyTransformation.mml_of_cic_object obj
in
window#set_title (UriManager.string_of_uri uri) ;
window#misc#hide () ; window#show () ;
(`Error (`T (Printexc.to_string e)))
in
let show_in_show_window_uri uri =
- let obj = CicEnvironment.get_obj uri in
+ let obj,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
show_in_show_window_obj uri obj
in
let show_in_show_window_callback mmlwidget ((n : Gdome.element option),_,_,_) =
match n with
None -> ()
| Some n' ->
- if n'#hasAttributeNS ~namespaceURI:xlinkns ~localName:href then
+ if n'#hasAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href then
let uri =
- (n'#getAttributeNS ~namespaceURI:xlinkns ~localName:href)#to_string
+ (n'#getAttributeNS ~namespaceURI:Misc.xlink_ns ~localName:href)#to_string
in
show_in_show_window_uri (UriManager.uri_of_string uri)
else
(fun name (newinputt,cons_names_entry) ->
let consnamesstr = cons_names_entry#text in
let cons_names = Str.split (Str.regexp " +") consnamesstr in
- let metasenv,expr =
+ let metasenv,expr,ugraph =
newinputt#get_metasenv_and_term ~context:[] ~metasenv:[]
in
match metasenv with
let cons_types =
List.map2
(fun name inputt ->
- let metasenv,expr =
+ let metasenv,expr,ugraph =
inputt#get_metasenv_and_term ~context ~metasenv:[]
in
match metasenv with
(*CSC: Da finire *)
let params = [] in
let tys = !get_types_and_cons () in
- let obj = Cic.InductiveDefinition(tys,params,!paramsno) in
- begin
- try
- debug_print (CicPp.ppobj obj);
- CicTypeChecker.typecheck_mutual_inductive_defs uri
- (tys,params,!paramsno) ;
- with
- e ->
- debug_print "Offending mutual (co)inductive type declaration:" ;
- debug_print (CicPp.ppobj obj) ;
- end ;
+ let obj = Cic.InductiveDefinition(tys,params,!paramsno,[]) in
+ let u =
+ begin
+ try
+ debug_print (CicPp.ppobj obj);
+ CicTypeChecker.typecheck_mutual_inductive_defs uri
+ (tys,params,!paramsno) CicUniv.empty_ugraph
+ with
+ e ->
+ debug_print "Offending mutual (co)inductive type declaration:" ;
+ debug_print (CicPp.ppobj obj) ;
+ (* I think we should fail here! *)
+ CicUniv.empty_ugraph
+ end
+ in
(* We already know that obj is well-typed. We need to add it to the *)
(* environment in order to compute the inner-types without having to *)
(* debrujin it or having to modify lots of other functions to avoid *)
(* asking the environment for the MUTINDs we are defining now. *)
- CicEnvironment.put_inductive_definition uri obj ;
+
+ (* u should be cleaned before adding it to the env *)
+ CicEnvironment.put_inductive_definition uri (obj,u) ;
save_obj uri obj ;
+ (* TASSI: FIXME we should save the cleaned u here *)
show_in_show_window_obj uri obj
with
e ->
(function () ->
chosen := true ;
try
- let metasenv,parsed = newinputt#get_metasenv_and_term [] [] in
+ let metasenv,parsed,ugraph = newinputt#get_metasenv_and_term [] [] in
let uristr = "cic:" ^ uri_entry#text in
let uri = UriManager.uri_of_string uristr in
if String.sub uristr (String.length uristr - 4) 4 <> ".con" then
let check_term_in_scratch scratch_window metasenv context expr =
try
- let ty = CicTypeChecker.type_of_aux' metasenv context expr in
+ let ty,ugraph =
+ CicTypeChecker.type_of_aux' metasenv context expr CicUniv.empty_ugraph
+ in
let expr = Cic.Cast (expr,ty) in
scratch_window#show () ;
scratch_window#set_term expr ;
canonical_context
in
try
- let metasenv',expr = inputt#get_metasenv_and_term context metasenv in
- check_term_in_scratch scratch_window metasenv' context expr
+ let metasenv',expr,ugraph =
+ inputt#get_metasenv_and_term context metasenv
+ in
+ check_term_in_scratch scratch_window metasenv' context expr
with
e ->
HelmLogger.log
let notebook = (rendering_window ())#notebook in
try
let uri = input_or_locate_uri ~title:"Open" in
- ignore(CicTypeChecker.typecheck uri);
+ ignore(CicTypeChecker.typecheck uri CicUniv.empty_ugraph);
(* 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.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
+ match fst(CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri ) with
+ Cic.Constant (_,Some bo,ty,_,_) -> [],bo,ty
+ | Cic.CurrentProof (_,metasenv,bo,ty,_,_) -> metasenv,bo,ty
| Cic.Constant _
| Cic.Variable _
| Cic.InductiveDefinition _ -> raise NotADefinition
let completeSearchPattern () =
let inputt = ((rendering_window ())#inputt : TermEditor.term_editor) in
try
- let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
+ let metasenv,expr,ugraph =
+ inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
let must = CGSearchPattern.get_constraints expr in
let must',only = refine_constraints must in
let query =
let module G = Gdome in
let rec aux element =
if element#hasAttributeNS
- ~namespaceURI:Misc.helmns
+ ~namespaceURI:Misc.helm_ns
~localName:(G.domString "xref")
then
mmlwidget#set_selection (Some element)
~packing:(vbox#pack ~expand:true ~padding:5) () in
let sequent_viewer =
TermViewer.sequent_viewer
- ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent
+ ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent
~packing:(scrolled_window#add) ~width:400 ~height:280 () in
object(self)
val mutable term = Cic.Rel 1 (* dummy value *)
~packing:(vbox1#pack ~expand:true ~padding:5) () in
let proofw =
TermViewer.sequent_viewer
- ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent
+ ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent
~width:400 ~height:275 ~packing:(scrolled_window1#add) () in
let _ = proofw_ref <- Some proofw in
let hbox3 =
~packing:(vbox1#pack ~expand:true ~padding:5) () in
let proofw =
TermViewer.sequent_viewer
- ~mml_of_cic_sequent:ChosenTransformer.mml_of_cic_sequent
+ ~mml_of_cic_sequent:ApplyTransformation.mml_of_cic_sequent
~width:400 ~height:275 ~packing:(scrolled_window1#add) () in
object(self)
method proofw = (assert false : TermViewer.sequent_viewer)
factory3#add_item "Reload Stylesheets"
~callback:
(function _ ->
- ChosenTransformer.reload_stylesheets () ;
if ProofEngine.get_proof () <> None then
try
refresh_goals notebook ;
let initialize_everything () =
let output =
TermViewer.proof_viewer
- ~mml_of_cic_object:ChosenTransformer.mml_of_cic_object
+ ~mml_of_cic_object:ApplyTransformation.mml_of_cic_object
~width:350 ~height:280 ()
in
let notebook = new notebook in
projects / helm.git / blobdiff