in
let empty_context = [] in
let empty_metasenv = [] in
- fun input ->
+ fun input ugraph ->
(Disambiguate'.disambiguate_term
- dbd empty_context empty_metasenv input empty_environment)
+ ~dbd empty_context empty_metasenv input empty_environment
+ ~initial_ugraph:ugraph)
-let parse_pp dbd ?uri_pred input =
- List.map (fun (_,_,t) -> CicPp.ppterm t)
- (parse dbd ?uri_pred input)
+let parse_pp dbd ?uri_pred input ugraph =
+ List.map (fun (_,_,t,_) -> CicPp.ppterm t)
+ (parse dbd ?uri_pred input ugraph )
* uri_pred is the predicate used to select which uris are tried. Per default
* only constant URIs are accepted *)
val parse:
- Mysql.dbd -> ?uri_pred:(string -> bool) -> string ->
- (DisambiguatingParser.EnvironmentP3.t * Cic.metasenv * Cic.term) list
+ Mysql.dbd -> ?uri_pred:(string -> bool) -> string ->
+ CicUniv.universe_graph ->
+ (DisambiguatingParser.EnvironmentP3.t *
+ Cic.metasenv *
+ Cic.term *
+ CicUniv.universe_graph) list
(** as above, but instead of returning the parsed cic term, pretty prints it
* (ignoring returned metasenv)
*)
-val parse_pp: Mysql.dbd -> ?uri_pred:(string -> bool) -> string -> string list
+val parse_pp: Mysql.dbd -> ?uri_pred:(string -> bool) ->
+ string -> CicUniv.universe_graph -> string list
method get_as_string : string
method get_metasenv_and_term :
context:Cic.context ->
- metasenv:Cic.metasenv -> Cic.metasenv * Cic.term
+ metasenv:Cic.metasenv -> Cic.metasenv * Cic.term * CicUniv.universe_graph
method environment : DisambiguatingParser.EnvironmentP3.t ref
method reset : unit
method set_term : string -> unit
Cic.metasenv ->
string ->
EnvironmentP3.t -> (* previous interpretation status *)
- (EnvironmentP3.t * (* new interpretation status *)
- Cic.metasenv * (* new metasenv *)
- Cic.term) list (* disambiguated term *)
+ ?initial_ugraph:CicUniv.universe_graph ->
+ (EnvironmentP3.t * (* new interpretation status *)
+ Cic.metasenv * (* new metasenv *)
+ Cic.term *
+ CicUniv.universe_graph) list (* disambiguated term *)
end
* 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
~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)
;;
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 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
+ let list_of_universes =
+ CicUnivUtils.universes_of_obj (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 *)
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 =
(`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 uri CicUniv.empty_ugraph in
show_in_show_window_obj uri obj
in
let show_in_show_window_callback mmlwidget ((n : Gdome.element option),_,_,_) =
(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
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 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
+ match fst(CicEnvironment.get_cooked_obj uri CicUniv.empty_ugraph) with
Cic.Constant (_,Some bo,ty,_) -> [],bo,ty
| Cic.CurrentProof (_,metasenv,bo,ty,_) -> metasenv,bo,ty
| Cic.Constant _
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 =
in
handle_refresh_exception
(fun () ->
- let metasenv',expr =
+ let metasenv',expr,ugraph = (*TASSI: FIX THIS*)
(match term with
| None -> ()
| Some t -> (C.term_editor ())#set_term t);
List.find (function (m,_,_) -> m=metano) metasenv
in
canonical_context in
- let (metasenv',expr) =
+ let (metasenv',expr,ugraph) =(* FIX THIS AND *)
(C.term_editor ())#get_metasenv_and_term
canonical_context metasenv
in
None -> assert false
| Some (_,metasenv,_,_) -> metasenv
in
- let ty = CicTypeChecker.type_of_aux' metasenv context term in
- P.perforate context term ty (* P.perforate also sets the goal *)
+ let ty,_ = (* TASSI: FIXME ehhmmmm *)
+ CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
+ in
+ P.perforate context term ty (* P.perforate also sets the goal *)
;;
exception FocusOnlyOnMeta;;
None -> assert false
| Some (_,metasenv,_,_) -> metasenv
in
- let ty = CicTypeChecker.type_of_aux' metasenv context term in
- match term with
- Cic.Meta (n,_) -> P.goal := Some n
- | _ -> raise FocusOnlyOnMeta
+ let ty,_ =
+ CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
+ in
+ match term with
+ Cic.Meta (n,_) -> P.goal := Some n
+ | _ -> raise FocusOnlyOnMeta
;;
let metasenv',expr = mk_metasenv_and_expr resolve_id' in
(*CSC: Bug here: we do not try to typecheck also the metasenv' *)
try
- let term,_,metasenv'' =
- CicRefine.type_of_aux' metasenv' context expr
+ let term,_,metasenv'',_ = (* TASSI: FIXME what are we doning here?*)
+ CicRefine.type_of_aux' metasenv' context expr CicUniv.empty_ugraph
in
- Ok (term,metasenv'')
+ Ok (term,metasenv'') (* TASSI: whould we pass back the ugraph? *)
with
CicRefine.Uncertain _ ->
prerr_endline ("%%% UNCERTAIN!!! " ^ CicPp.ppterm expr) ;
let test_this mqi_handle uri_pred raw_term =
let empty_context = [] in
List.map
- (function (env, metasenv, cic_term) ->
+ (function (env, metasenv, cic_term,ugraph ) ->
let etype =
try
- CicPp.ppterm
- (CicTypeChecker.type_of_aux' metasenv empty_context cic_term)
+ let ty, _ =
+ (CicTypeChecker.type_of_aux' metasenv empty_context cic_term ugraph)
+ in
+ CicPp.ppterm ty
with _ -> "MALFORMED"
in
let ereduced =
etype = etype ^ "\n";
ereduced = ereduced ^ "\n";
}
- ) (BatchParser.parse mqi_handle ~uri_pred raw_term)
+ ) (BatchParser.parse mqi_handle ~uri_pred raw_term CicUniv.empty_ugraph)
let dump_environment filename =
try
* http://cs.unibo.it/helm/.
*)
-(******************************************************************************)
-(* *)
-(* PROJECT HELM *)
-(* *)
-(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
-(* 06/01/2002 *)
-(* *)
-(* *)
-(******************************************************************************)
+(*****************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* 06/01/2002 *)
+(* *)
+(* *)
+(*****************************************************************************)
open Printf
method get_as_string : string
method get_metasenv_and_term :
context:Cic.context ->
- metasenv:Cic.metasenv -> Cic.metasenv * Cic.term
+ metasenv:Cic.metasenv ->
+ Cic.metasenv * Cic.term * CicUniv.universe_graph
method reset : unit
(* The input of set_term is unquoted *)
method set_term : string -> unit
=
let environment =
match share_environment_with with
- None -> ref
+ None -> ref (*DisambiguateTypes.empty_environment*)
(DisambiguatingParser.EnvironmentP3.of_string
DisambiguatingParser.EnvironmentP3.empty)
| Some obj -> obj#environment
| None -> None
) context
in
- let environment',metasenv,expr =
+ let environment',metasenv,expr,ugraph =
match
Disambiguate'.disambiguate_term ~dbd context metasenv
- (input#buffer#get_text ()) !environment
+ (input#buffer#get_text ()) ~initial_ugraph:CicUniv.empty_ugraph
+ !environment
with
- [environment',metasenv,expr] -> environment',metasenv,expr
+ [environment',metasenv,expr,u] -> environment',metasenv,expr,u
| _ -> assert false
in
environment := environment';
- (metasenv, expr)
+ (metasenv, expr,ugraph)
+ (* TASSI: FIXME ?are we sure we have to keep this? *)
method environment = environment
end
method get_as_string : string
method get_metasenv_and_term :
context:Cic.context ->
- metasenv:Cic.metasenv -> Cic.metasenv * Cic.term
+ metasenv:Cic.metasenv ->
+ Cic.metasenv * Cic.term * CicUniv.universe_graph
method reset : unit
method set_term : string -> unit
method environment : DisambiguatingParser.EnvironmentP3.t ref
let debug_print s = prerr_endline ("^^^^^^ " ^ s)
-let test_uri uri =
+let test_uri typecheck uri =
+ if typecheck then
+ try ignore(CicTypeChecker.typecheck uri);1
+ with CicTypeChecker.TypeCheckerFailure s |
+ CicTypeChecker.AssertFailure s -> 0
+ else
let obj = CicEnvironment.get_obj uri in
let (annobj, _, _, ids_to_inner_sorts, _, _, _) =
Cic2acic.acic_object_of_cic_object ~eta_fix:false obj
;;
-let test_uri uri =
+let test_uri typecheck uri =
try
ignore (Unix.alarm !time_out) ;
- if test_uri uri = 1 then `Ok else `Maybe
+ if test_uri typecheck uri = 1 then `Ok else `Maybe
with
| TimeOut ->
(* We do this to clear the alarm set by the signal handler *)
List.iter (fun s -> print_endline ("\t" ^ s)) (List.rev !timeout);
print_newline ()
-let do_uri (ok, nok, maybe, timeout) uri =
+let do_uri typecheck (ok, nok, maybe, timeout) uri =
let uri_str = UriManager.string_of_uri uri in
printf "Testing URI: %-55s %!" (uri_str ^ " ...");
- match test_uri uri with
+ (match test_uri typecheck uri with
| `Ok ->
print_endline "\e[01;32m[ OK ]\e[00m";
ok := uri_str :: !ok
maybe := uri_str :: !maybe
| `TimeOut ->
print_endline "\e[01;34m[TIMEOUT!]\e[00m";
- timeout := uri_str :: !timeout
+ timeout := uri_str :: !timeout);
+ print_endline "--";
+ print_endline (CicUniv.print_stats ());
+ print_endline "--"
-let do_file status fname =
+let do_file typecheck status fname =
try
let ic = open_in fname in
(try
let line = input_line ic in
try
let uri = UriManager.uri_of_string line in
- do_uri status uri
+ do_uri typecheck status uri
with UriManager.IllFormedUri _ ->
printf "Error parsing URI '%s', ignoring it" line
done
(HelmLogger.string_of_html_msg msg));
let names = ref [] in
let tryvars = ref false in
+ let typecheck = ref false in
let prefix = ref "" in
let varsprefix = ref "####" in
let usage = "testlibrary [OPTION] ... (uri1 | file1) (uri2 | file2) ..." in
"-varsprefix", Arg.Set_string varsprefix,
"limit variable choices to URIs beginning with prefix; overrides -prefix" ;
"-timeout", Arg.Set_int time_out,
- "number of seconds before a timeout; 0 means no timeout"
+ "number of seconds before a timeout; 0 means no timeout";
+ "-typecheck", Arg.Set typecheck, "simply typechek the uri"
]
in
Arg.parse spec (fun name -> names := name :: !names) usage;
(fun name ->
try
let uri = UriManager.uri_of_string name in
- do_uri status uri
+ do_uri !typecheck status uri
with UriManager.IllFormedUri _ ->
if Sys.file_exists name then
- do_file status name
+ do_file !typecheck status name
else
printf "Don't know what to do with '%s', ignoring it\n%!" name)
names ;
method get_as_string : string
method get_metasenv_and_term :
context:Cic.context ->
- metasenv:Cic.metasenv -> Cic.metasenv * Cic.term
+ metasenv:Cic.metasenv ->
+ Cic.metasenv * Cic.term * CicUniv.universe_graph
method reset : unit
(* The input of set_term is unquoted *)
method set_term : string -> unit
) context
in
debug_print ("TexTermEditor: Raw Tex: " ^ (Mathml_editor.get_tex tex_editor)) ;
- let environment',metasenv,expr =
+ let environment',metasenv,expr,ugraph =
match
Disambiguate'.disambiguate_term ~dbd
- context metasenv (Mathml_editor.get_tex tex_editor) !environment
+ context metasenv (Mathml_editor.get_tex tex_editor)
+ ~initial_ugraph:CicUniv.empty_ugraph !environment
with
- [environment',metasenv,expr] -> environment',metasenv,expr
+ [environment',metasenv,expr,u] -> environment',metasenv,expr,u
| _ -> assert false
in
environment := environment' ;
- metasenv,expr
+ metasenv,expr,ugraph
method environment = environment
end
method get_as_string : string
method get_metasenv_and_term :
context:Cic.context ->
- metasenv:Cic.metasenv -> Cic.metasenv * Cic.term
+ metasenv:Cic.metasenv ->
+ Cic.metasenv * Cic.term * CicUniv.universe_graph
method reset : unit
(* The input of set_term is unquoted *)
method set_term : string -> unit
projects / helm.git / commitdiff