type options = option_value StringMap.t
let no_options = StringMap.empty
+type ast_command = (CicNotationPt.term, GrafiteAst.obj) GrafiteAst.command
+type moo = ast_command list * GrafiteAst.metadata list
+
type status = {
- aliases : DisambiguateTypes.environment;
- moo_content_rev : string list;
- proof_status : proof_status;
- options : options;
- objects : (UriManager.uri * string) list;
+ aliases: DisambiguateTypes.environment;
+ multi_aliases: DisambiguateTypes.multiple_environment;
+ moo_content_rev: moo;
+ proof_status: proof_status;
+ options: options;
+ objects: (UriManager.uri * string) list;
notation_ids: CicNotation.notation_id list;
}
(fun (u,_) ->
MatitaLog.message (UriManager.string_of_uri u)) status.objects
-
let get_option status name =
try
StringMap.find name status.options
else
{ status with options = StringMap.add name value status.options }
+let add_moo_content cmds status =
+ let content, metadata = status.moo_content_rev in
+ let content' =
+ List.fold_right
+ (fun cmd acc ->
+(* prerr_endline ("adding to moo command: " ^ GrafiteAstPp.pp_command cmd); *)
+ match cmd with
+ | GrafiteAst.Interpretation _
+ | GrafiteAst.Default _ ->
+ if List.mem cmd content then acc
+ else cmd :: acc
+ | GrafiteAst.Alias _ -> (* move Alias as the last inserted one *)
+ cmd :: (List.filter ((<>) cmd) acc)
+ | _ -> cmd :: acc)
+ cmds content
+ in
+(* prerr_endline ("new moo content: " ^ String.concat " " (List.map
+ GrafiteAstPp.pp_command content')); *)
+ { status with moo_content_rev = content', metadata }
+
+let add_moo_metadata new_metadata status =
+ let content, metadata = status.moo_content_rev in
+ let metadata' =
+ List.fold_left
+ (fun acc m ->
+ match m with
+ | GrafiteAst.Dependency buri ->
+ let is_self = (* self dependency *)
+ try
+ get_string_option status "baseuri" = buri
+ with Option_error _ -> false (* baseuri not yet set *)
+ in
+ if is_self
+ || List.exists (GrafiteAst.eq_metadata m) metadata (* duplicate *)
+ then acc
+ else m :: acc
+ | _ -> m :: acc)
+ metadata new_metadata
+ in
+ { status with moo_content_rev = content, metadata' }
+
(* subset of MatitaConsole.console methods needed by MatitaInterpreter *)
class type console =
object