X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaTypes.ml;h=8bd32bb23eac45b32f53f8f88f818bc391222f02;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=580f022f59baa8d0337718c9281ebcaf1331775e;hpb=a7b90d2494f7d580faa54ecd2835bd4649129763;p=helm.git diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml index 580f022f5..8bd32bb23 100644 --- a/helm/matita/matitaTypes.ml +++ b/helm/matita/matitaTypes.ml @@ -41,9 +41,14 @@ exception Option_error of string * string exception Unbound_identifier of string +type incomplete_proof = { + proof: ProofEngineTypes.proof; + stack: Continuationals.Stack.t; +} + type proof_status = | No_proof - | Incomplete_proof of ProofEngineTypes.status + | Incomplete_proof of incomplete_proof | Proof of ProofEngineTypes.proof | Intermediate of Cic.metasenv (* Status in which the proof could be while it is being processed by the @@ -57,18 +62,34 @@ type option_value = 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; (** disambiguation aliases *) + aliases: DisambiguateTypes.environment; + multi_aliases: DisambiguateTypes.multiple_environment; + moo_content_rev: moo; proof_status: proof_status; options: options; objects: (UriManager.uri * string) list; - (** in-scope objects, with their paths *) + coercions: UriManager.uri list; + notation_ids: CicNotation.notation_id list; } +let set_metasenv metasenv status = + let proof_status = + match status.proof_status with + | No_proof -> Intermediate metasenv + | Incomplete_proof ({ proof = (uri, _, proof, ty) } as incomplete_proof) -> + Incomplete_proof + { incomplete_proof with proof = (uri, metasenv, proof, ty) } + | Intermediate _ -> Intermediate metasenv + | Proof _ -> assert false + in + { status with proof_status = proof_status } + let dump_status status = MatitaLog.message "status.aliases:\n"; - MatitaLog.message - (CicTextualParser2.EnvironmentP3.to_string status.aliases ^ "\n"); MatitaLog.message "status.proof_status:"; MatitaLog.message (match status.proof_status with @@ -90,7 +111,6 @@ let dump_status status = (fun (u,_) -> MatitaLog.message (UriManager.string_of_uri u)) status.objects - let get_option status name = try StringMap.find name status.options @@ -126,7 +146,51 @@ let set_option status name value = with Failure _ -> command_error (sprintf "Not an integer value \"%s\"" value)) in - { status with options = StringMap.add name value status.options } + if StringMap.mem name status.options && name = "baseuri" then + command_error "Redefinition of 'baseuri' is forbidden." + 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 = @@ -181,3 +245,47 @@ class type mathViewer = ?reuse:bool -> entry:mathViewer_entry -> UriManager.uri list -> unit end +let qualify status name = get_string_option status "baseuri" ^ "/" ^ name + +let get_current_proof status = + match status.proof_status with + | Incomplete_proof { proof = p } -> p + | _ -> statement_error "no ongoing proof" + +let get_proof_metasenv status = + match status.proof_status with + | No_proof -> [] + | Proof (_, metasenv, _, _) + | Incomplete_proof { proof = (_, metasenv, _, _) } + | Intermediate metasenv -> + metasenv + +let get_proof_context status goal = + match status.proof_status with + | Incomplete_proof { proof = (_, metasenv, _, _) } -> + let (_, context, _) = CicUtil.lookup_meta goal metasenv in + context + | _ -> [] + +let get_proof_conclusion status goal = + match status.proof_status with + | Incomplete_proof { proof = (_, metasenv, _, _) } -> + let (_, _, conclusion) = CicUtil.lookup_meta goal metasenv in + conclusion + | _ -> statement_error "no ongoing proof" + +let get_stack status = + match status.proof_status with + | Incomplete_proof p -> p.stack + | Proof _ -> Continuationals.Stack.empty + | _ -> assert false + +let set_stack stack status = + match status.proof_status with + | Incomplete_proof p -> + { status with proof_status = Incomplete_proof { p with stack = stack } } + | Proof _ -> + assert (Continuationals.Stack.is_empty stack); + status + | _ -> assert false +