From: Enrico Tassi Date: Wed, 1 Dec 2004 09:43:44 +0000 (+0000) Subject: Added universes handling. Tag PRE_UNIVERSES may help ;) X-Git-Tag: V_0_1_0~174 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=cf8abaf99bf9065c82d8f668d441bc4c0a2a13df;p=helm.git Added universes handling. Tag PRE_UNIVERSES may help ;) --- diff --git a/helm/gTopLevel/batchParser.ml b/helm/gTopLevel/batchParser.ml index b19797df8..8eb800b84 100644 --- a/helm/gTopLevel/batchParser.ml +++ b/helm/gTopLevel/batchParser.ml @@ -79,11 +79,12 @@ let parse dbd ?(uri_pred = constants_only ~prefix:"") = 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 ) diff --git a/helm/gTopLevel/batchParser.mli b/helm/gTopLevel/batchParser.mli index edfaa6927..6d2900304 100644 --- a/helm/gTopLevel/batchParser.mli +++ b/helm/gTopLevel/batchParser.mli @@ -39,11 +39,16 @@ val uri_pred_of_conf: * 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 diff --git a/helm/gTopLevel/chosenTermEditor.mli b/helm/gTopLevel/chosenTermEditor.mli index d88932c70..8a5402449 100644 --- a/helm/gTopLevel/chosenTermEditor.mli +++ b/helm/gTopLevel/chosenTermEditor.mli @@ -4,7 +4,7 @@ class type term_editor = 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 diff --git a/helm/gTopLevel/disambiguatingParser.mli b/helm/gTopLevel/disambiguatingParser.mli index a8afd0e65..3d2c91f25 100644 --- a/helm/gTopLevel/disambiguatingParser.mli +++ b/helm/gTopLevel/disambiguatingParser.mli @@ -41,8 +41,10 @@ module Make (C : DisambiguateTypes.Callbacks) : 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 diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 7ba0650ce..2276fdac4 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -23,15 +23,15 @@ * http://helm.cs.unibo.it/ *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 06/01/2002 *) -(* *) -(* *) -(******************************************************************************) +(*****************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 06/01/2002 *) +(* *) +(* *) +(*****************************************************************************) let debug_level = ref 1 let debug_print ?(level = 1) s = if !debug_level >= level then prerr_endline s @@ -150,7 +150,8 @@ let check_window uris = ~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) @@ -436,42 +437,52 @@ let save_obj uri obj = ;; 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 *) @@ -493,11 +504,11 @@ let typecheck_loaded_proof metasenv bo ty = 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 = @@ -869,7 +880,7 @@ let (`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),_,_,_) = @@ -1222,7 +1233,7 @@ let new_inductive () = (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 @@ -1324,7 +1335,7 @@ let new_inductive () = 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 @@ -1368,22 +1379,29 @@ let new_inductive () = 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 -> @@ -1462,7 +1480,7 @@ let new_proof () = (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 @@ -1514,7 +1532,9 @@ let new_proof () = 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 ; @@ -1544,8 +1564,10 @@ let check scratch_window () = 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 @@ -1568,10 +1590,10 @@ let open_ () = 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 _ @@ -1833,7 +1855,8 @@ let refine_constraints (must_obj,must_rel,must_sort) = 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 = diff --git a/helm/gTopLevel/invokeTactics.ml b/helm/gTopLevel/invokeTactics.ml index cbe25219c..13dc83f1d 100644 --- a/helm/gTopLevel/invokeTactics.ml +++ b/helm/gTopLevel/invokeTactics.ml @@ -169,7 +169,7 @@ module Make (C: Callbacks) : Tactics = 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); @@ -235,7 +235,7 @@ module Make (C: Callbacks) : Tactics = 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 diff --git a/helm/gTopLevel/logicalOperations.ml b/helm/gTopLevel/logicalOperations.ml index 93c511f13..3fab938a0 100644 --- a/helm/gTopLevel/logicalOperations.ml +++ b/helm/gTopLevel/logicalOperations.ml @@ -94,8 +94,10 @@ let to_sequent id ids_to_terms ids_to_father_ids = 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;; @@ -110,8 +112,10 @@ let focus id ids_to_terms ids_to_father_ids = 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 ;; diff --git a/helm/gTopLevel/oldDisambiguate.ml b/helm/gTopLevel/oldDisambiguate.ml index b760b3b8c..24dd30f91 100644 --- a/helm/gTopLevel/oldDisambiguate.ml +++ b/helm/gTopLevel/oldDisambiguate.ml @@ -160,10 +160,10 @@ module Make(C:Callbacks) = 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) ; diff --git a/helm/gTopLevel/regtest.ml b/helm/gTopLevel/regtest.ml index 7836fae47..bee1c2816 100644 --- a/helm/gTopLevel/regtest.ml +++ b/helm/gTopLevel/regtest.ml @@ -227,11 +227,13 @@ let as_expected report_fname expected found = 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 = @@ -246,7 +248,7 @@ let test_this mqi_handle uri_pred raw_term = 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 diff --git a/helm/gTopLevel/termEditor.ml b/helm/gTopLevel/termEditor.ml index f74e45077..4cca70221 100644 --- a/helm/gTopLevel/termEditor.ml +++ b/helm/gTopLevel/termEditor.ml @@ -23,15 +23,15 @@ * http://cs.unibo.it/helm/. *) -(******************************************************************************) -(* *) -(* PROJECT HELM *) -(* *) -(* Claudio Sacerdoti Coen *) -(* 06/01/2002 *) -(* *) -(* *) -(******************************************************************************) +(*****************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 06/01/2002 *) +(* *) +(* *) +(*****************************************************************************) open Printf @@ -44,7 +44,8 @@ class type term_editor = 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 @@ -61,7 +62,7 @@ module Make(C:DisambiguateTypes.Callbacks) = = 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 @@ -98,16 +99,18 @@ module Make(C:DisambiguateTypes.Callbacks) = | 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 diff --git a/helm/gTopLevel/termEditor.mli b/helm/gTopLevel/termEditor.mli index 9ae451e4b..2817f812a 100644 --- a/helm/gTopLevel/termEditor.mli +++ b/helm/gTopLevel/termEditor.mli @@ -30,7 +30,8 @@ class type term_editor = 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 diff --git a/helm/gTopLevel/testlibrary.ml b/helm/gTopLevel/testlibrary.ml index fccdc19c6..f35ee096a 100644 --- a/helm/gTopLevel/testlibrary.ml +++ b/helm/gTopLevel/testlibrary.ml @@ -38,7 +38,12 @@ module Disambiguate' = Disambiguate.Make (DisambiguateCallbacks) 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 @@ -103,10 +108,10 @@ ignore ;; -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 *) @@ -133,10 +138,10 @@ let report (ok,nok,maybe,timeout) = 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 "[ OK ]"; ok := uri_str :: !ok @@ -148,9 +153,12 @@ let do_uri (ok, nok, maybe, timeout) uri = maybe := uri_str :: !maybe | `TimeOut -> print_endline "[TIMEOUT!]"; - 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 @@ -158,7 +166,7 @@ let do_file status fname = 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 @@ -175,6 +183,7 @@ let _ = (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 @@ -186,7 +195,8 @@ let _ = "-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; @@ -199,10 +209,10 @@ let _ = (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 ; diff --git a/helm/gTopLevel/texTermEditor.ml b/helm/gTopLevel/texTermEditor.ml index d0fefdee3..a59fb3489 100644 --- a/helm/gTopLevel/texTermEditor.ml +++ b/helm/gTopLevel/texTermEditor.ml @@ -45,7 +45,8 @@ class type term_editor = 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 @@ -217,16 +218,17 @@ module Make(C:DisambiguateTypes.Callbacks) = ) 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 diff --git a/helm/gTopLevel/texTermEditor.mli b/helm/gTopLevel/texTermEditor.mli index fa2dbb95b..ece0bd8d9 100644 --- a/helm/gTopLevel/texTermEditor.mli +++ b/helm/gTopLevel/texTermEditor.mli @@ -30,7 +30,8 @@ class type term_editor = 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