*)
exception Drop
-exception UnableToInclude of string
-exception IncludedFileNotCompiled of string
+exception IncludedFileNotCompiled of string (* file name *)
+exception MetadataNotFound of string (* file name *)
type options = {
do_heavy_checks: bool ;
- include_paths: string list ;
clean_baseuri: bool
}
type eval_ast =
{ea_go:
'term 'lazy_term 'reduction 'obj 'ident.
+ baseuri_of_script:(string -> string) ->
disambiguate_tactic:
(GrafiteTypes.status ->
ProofEngineTypes.goal ->
disambiguate_command:
(GrafiteTypes.status ->
- ('term, 'obj) GrafiteAst.command ->
- GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command) ->
+ 'obj GrafiteAst.command ->
+ GrafiteTypes.status * Cic.obj GrafiteAst.command) ->
?do_heavy_checks:bool ->
- ?include_paths:string list ->
?clean_baseuri:bool ->
GrafiteTypes.status ->
('term, 'lazy_term, 'reduction, 'obj, 'ident) GrafiteAst.statement ->
type 'a eval_command =
{ec_go: 'term 'obj.
+ baseuri_of_script:(string -> string) ->
disambiguate_command:
(GrafiteTypes.status ->
- ('term,'obj) GrafiteAst.command ->
- GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command) ->
- options -> GrafiteTypes.status -> ('term,'obj) GrafiteAst.command ->
+ 'obj GrafiteAst.command ->
+ GrafiteTypes.status * Cic.obj GrafiteAst.command) ->
+ options -> GrafiteTypes.status -> 'obj GrafiteAst.command ->
GrafiteTypes.status
}
type 'a eval_executable =
{ee_go: 'term 'lazy_term 'reduction 'obj 'ident.
+ baseuri_of_script:(string -> string) ->
disambiguate_tactic:
(GrafiteTypes.status ->
ProofEngineTypes.goal ->
disambiguate_command:
(GrafiteTypes.status ->
- ('term, 'obj) GrafiteAst.command ->
- GrafiteTypes.status * (Cic.term, Cic.obj) GrafiteAst.command) ->
+ 'obj GrafiteAst.command ->
+ GrafiteTypes.status * Cic.obj GrafiteAst.command) ->
options ->
GrafiteTypes.status ->
}
type 'a eval_from_moo = { efm_go: GrafiteTypes.status ref -> string -> unit }
+
+let coercion_moo_statement_of uri =
+ GrafiteAst.Coercion (DisambiguateTypes.dummy_floc, uri, false)
-let eval_coercion status ~add_composites coercion =
- let uri = CicUtil.uri_of_term coercion in
- let status = MatitaSync.add_coercion status ~add_composites uri in
+let eval_coercion status ~add_composites uri =
+ let basedir = Helm_registry.get "matita.basedir" in
+ let compounds = LibrarySync.add_coercion ~add_composites ~basedir uri in
+ let moo_content = coercion_moo_statement_of uri in
+ let status = GrafiteTypes.add_moo_content [moo_content] status in
+ let status = MatitaSync.add_coercion status uri compounds in
{status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}
let eval_tactical ~disambiguate_tactic status tac =
in
status
-let make_absolute paths path =
- let rec aux = function
- | [] -> ignore (Unix.stat path); path
- | p :: tl ->
- let path = p ^ "/" ^ path in
- try
- ignore (Unix.stat path); path
- with Unix.Unix_error _ -> aux tl
- in
- try
- aux paths
- with Unix.Unix_error _ -> raise (UnableToInclude path)
-;;
-
let eval_comment status c = status
-let rec eval_command = {ec_go = fun ~disambiguate_command opts status cmd ->
+(* since the record syntax allows to declare coercions, we have to put this
+ * information inside the moo *)
+let add_coercions_of_record_to_moo obj lemmas status =
+ let attributes = CicUtil.attributes_of_obj obj in
+ let is_record = function `Class (`Record att) -> Some att | _-> None in
+ match HExtlib.list_findopt is_record attributes with
+ | None -> status
+ | Some fields ->
+ let is_a_coercion uri =
+ try
+ let obj,_ =
+ CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri in
+ let attrs = CicUtil.attributes_of_obj obj in
+ List.mem (`Class `Projection) attrs
+ with Not_found -> assert false
+ in
+ (* looking at the fields we can know the 'wanted' coercions, but not the
+ * actually generated ones. So, only the intersection between the wanted
+ * and the actual should be in the moo as coercion, while everithing in
+ * lemmas should go as aliases *)
+ let wanted_coercions =
+ HExtlib.filter_map
+ (function
+ | (name,true) ->
+ Some
+ (UriManager.uri_of_string
+ (GrafiteTypes.qualify status name ^ ".con"))
+ | _ -> None)
+ fields
+ in
+ prerr_endline "wanted coercions:";
+ List.iter
+ (fun u -> prerr_endline (UriManager.string_of_uri u))
+ wanted_coercions;
+ let coercions, moo_content =
+ List.split
+ (HExtlib.filter_map
+ (fun uri ->
+ let is_a_wanted_coercion =
+ List.exists (UriManager.eq uri) wanted_coercions in
+ if is_a_coercion uri && is_a_wanted_coercion then
+ Some (uri, coercion_moo_statement_of uri)
+ else
+ None)
+ lemmas)
+ in
+ List.iter
+ (fun u -> prerr_endline (UriManager.string_of_uri u))
+ coercions;
+ let status = GrafiteTypes.add_moo_content moo_content status in
+ List.fold_left
+ (fun status uri ->
+ MatitaSync.add_coercion status uri [])
+ status coercions
+
+let add_obj uri obj status =
+ let basedir = Helm_registry.get "matita.basedir" in
+ let lemmas = LibrarySync.add_obj uri obj basedir in
+ let status =
+ {status with GrafiteTypes.objects = uri::status.GrafiteTypes.objects} in
+ let status = MatitaSync.add_obj uri obj lemmas status in
+ status, lemmas
+
+let rec eval_command = {ec_go = fun ~baseuri_of_script ~disambiguate_command opts status cmd ->
let status,cmd = disambiguate_command status cmd in
let cmd,notation_ids' = CicNotation.process_notation cmd in
let status =
LibraryObjects.set_default what uris;
GrafiteTypes.add_moo_content [cmd] status
| GrafiteAst.Include (loc, path) ->
- let absolute_path = make_absolute opts.include_paths path in
- let moopath = GrafiteMisc.obj_file_of_script ~basedir absolute_path in
- let status = ref status in
+ let baseuri = baseuri_of_script path in
+ let moopath = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
+ let metadatapath= LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in
if not (Sys.file_exists moopath) then
raise (IncludedFileNotCompiled moopath);
+ let status =
+ if Helm_registry.get_bool "db.nodb" then
+ if not (Sys.file_exists metadatapath) then
+ raise (MetadataNotFound metadatapath)
+ else
+ GrafiteTypes.add_metadata
+ (LibraryNoDb.load_metadata ~fname:metadatapath) status
+ else
+ status
+ in
+ let status = ref status in
eval_from_moo.efm_go status moopath;
!status
- | GrafiteAst.Metadata (loc, m) ->
- (match m with
- | GrafiteAst.Dependency uri -> GrafiteTypes.add_moo_metadata [m] status
- | GrafiteAst.Baseuri _ -> status)
| GrafiteAst.Set (loc, name, value) ->
let status =
if name = "baseuri" then begin
HLog.message ("cleaning baseuri " ^ value);
LibraryClean.clean_baseuris ~basedir [value]
end;
- GrafiteTypes.add_moo_metadata [GrafiteAst.Baseuri value] status
+ GrafiteTypes.add_metadata [LibraryNoDb.Baseuri value] status
end else
status
in
"Proof not completed! metasenv is not empty!");
let name = UriManager.name_of_uri uri in
let obj = Cic.Constant (name,Some bo,ty,[],[]) in
- MatitaSync.add_obj uri obj
+ let status, _lemmas = add_obj uri obj status in
+ (* should we assert lemmas = [] ? *)
{status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}
- | GrafiteAst.Coercion (loc, coercion, add_composites) ->
- eval_coercion status ~add_composites coercion
+ | GrafiteAst.Coercion (loc, uri, add_composites) ->
+ eval_coercion status ~add_composites uri
| GrafiteAst.Alias (loc, spec) ->
let diff =
(*CSC: Warning: this code should be factorized with the corresponding
let status = GrafiteTypes.add_moo_content [stm] status in
let uris =
List.map
- (fun uri -> GrafiteAst.Dependency (UriManager.buri_of_uri uri))
+ (fun uri -> LibraryNoDb.Dependency (UriManager.buri_of_uri uri))
(CicNotationUtil.find_appl_pattern_uris cic_appl_pattern)
in
let diff =
DisambiguateChoices.lookup_symbol_by_dsc symbol dsc]
in
let status = MatitaSync.set_proof_aliases status diff in
- let status = GrafiteTypes.add_moo_metadata uris status in
+ let status = GrafiteTypes.add_metadata uris status in
status
| GrafiteAst.Notation _ as stm -> GrafiteTypes.add_moo_content [stm] status
| GrafiteAst.Obj (loc,obj) ->
raise (GrafiteTypes.Command_error (
"metasenv not empty while giving a definition with body: " ^
CicMetaSubst.ppmetasenv [] metasenv));
- MatitaSync.add_obj uri obj
+ let status, lemmas = add_obj uri obj status in
+ let status = add_coercions_of_record_to_moo obj lemmas status in
{status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}
-} and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command opts status ex ->
+} and eval_executable = {ee_go = fun ~baseuri_of_script ~disambiguate_tactic ~disambiguate_command opts status ex ->
match ex with
| GrafiteAst.Tactical (_, tac, None) ->
eval_tactical ~disambiguate_tactic status tac
let status = eval_tactical ~disambiguate_tactic status tac in
eval_tactical ~disambiguate_tactic status punct
| GrafiteAst.Command (_, cmd) ->
- eval_command.ec_go ~disambiguate_command opts status cmd
+ eval_command.ec_go ~baseuri_of_script ~disambiguate_command
+ opts status cmd
| GrafiteAst.Macro (_, mac) ->
(*CSC: DA RIPRISTINARE CON UN TIPO DIVERSO
raise (Command_error
let ast_of_cmd cmd =
GrafiteAst.Executable (DisambiguateTypes.dummy_floc,
GrafiteAst.Command (DisambiguateTypes.dummy_floc,
- (GrafiteAst.reash_cmd_uris cmd)))
+ cmd))
in
- let moo, metadata = GrafiteMarshal.load_moo fname in
+ let moo = GrafiteMarshal.load_moo fname in
List.iter
(fun ast ->
let ast = ast_of_cmd ast in
status :=
eval_ast.ea_go
+ ~baseuri_of_script:(fun _ -> assert false)
~disambiguate_tactic:(fun status _ tactic -> ref status,tactic)
~disambiguate_command:(fun status cmd -> status,cmd)
!status ast)
- moo;
- List.iter
- (fun m ->
- let ast =
- ast_of_cmd (GrafiteAst.Metadata (DisambiguateTypes.dummy_floc, m))
- in
- status :=
- eval_ast.ea_go
- ~disambiguate_tactic:(fun status _ tactic -> ref status,tactic)
- ~disambiguate_command:(fun status cmd -> status,cmd)
- !status ast)
- metadata
-
-} and eval_ast = {ea_go = fun ~disambiguate_tactic ~disambiguate_command
- ?(do_heavy_checks=false) ?(include_paths=[]) ?(clean_baseuri=true) status st
+ moo
+} and eval_ast = {ea_go = fun ~baseuri_of_script ~disambiguate_tactic
+ ~disambiguate_command ?(do_heavy_checks=false) ?(clean_baseuri=true) status
+ st
->
let opts = {
do_heavy_checks = do_heavy_checks ;
- include_paths = include_paths;
clean_baseuri = clean_baseuri }
in
match st with
| GrafiteAst.Executable (_,ex) ->
- eval_executable.ee_go ~disambiguate_tactic ~disambiguate_command opts status ex
+ eval_executable.ee_go ~baseuri_of_script ~disambiguate_tactic
+ ~disambiguate_command opts status ex
| GrafiteAst.Comment (_,c) -> eval_comment status c
}
projects / helm.git / blobdiff