- CicTypeChecker.TypeCheckerFailure s ->
- MatitaLog.message
- ("Unable to create projection " ^ name ^ " cause: " ^ s);
- status
- | CicEnvironment.Object_not_found uri ->
- let depend = UriManager.name_of_uri uri in
- MatitaLog.message
- ("Unable to create projection " ^ name ^ " because it requires " ^ depend);
- status
- ) status projections
-
-(* to avoid a long list of recursive functions *)
-let eval_from_stream_ref = ref (fun _ _ _ -> assert false);;
-
-let eval_command status cmd =
- match cmd with
- | TacticAst.Default (loc, what, uris) as cmd ->
- LibraryObjects.set_default what uris;
- {status with moo_content_rev =
- (TacticAstPp.pp_command cmd ^ "\n") :: status.moo_content_rev}
- | TacticAst.Include (loc, path) ->
- let path = MatitaMisc.obj_file_of_script path in
- let stream = Stream.of_channel (open_in path) in
- let status = ref status in
- !eval_from_stream_ref status stream (fun _ _ -> ());
- !status
- | TacticAst.Set (loc, name, value) ->
- let value =
- if name = "baseuri" then
- MatitaMisc.strip_trailing_slash value
- else
- value
- in
- set_option status name value
- | TacticAst.Drop loc -> raise Drop
- | TacticAst.Qed loc ->
- let uri, metasenv, bo, ty =
- match status.proof_status with
- | Proof (Some uri, metasenv, body, ty) ->
- uri, metasenv, body, ty
- | Proof (None, metasenv, body, ty) ->
- command_error
- ("Someone allows to start a thm without giving the "^
- "name/uri. This should be fixed!")
- | _-> command_error "You can't qed an uncomplete theorem"
- in
- let suri = UriManager.string_of_uri uri in
- if metasenv <> [] then
- command_error "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 status
- | TacticAst.Coercion (loc, coercion) ->
- let status = eval_coercion status coercion in
- let moo_content_rev =
- (TacticAstPp.pp_cic_command
- (TacticAst.Coercion (CicAst.dummy_floc,coercion)) ^ ".\n") ::
- status.moo_content_rev in
- {status with moo_content_rev = moo_content_rev}
- | TacticAst.Alias (loc, spec) ->
- let aliases =
- match spec with
- | TacticAst.Ident_alias (id,uri) ->
- DisambiguateTypes.Environment.add
- (DisambiguateTypes.Id id)
- (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri)))
- status.aliases
- | TacticAst.Symbol_alias (symb, instance, desc) ->
- DisambiguateTypes.Environment.add
- (DisambiguateTypes.Symbol (symb,instance))
- (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
- status.aliases
- | TacticAst.Number_alias (instance,desc) ->
- DisambiguateTypes.Environment.add
- (DisambiguateTypes.Num instance)
- (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases
- in
- MatitaSync.set_proof_aliases status aliases
- | TacticAst.Obj (loc,obj) ->
- let ext,name =
- match obj with
- Cic.Constant (name,_,_,_,_)
- | Cic.CurrentProof (name,_,_,_,_,_) -> ".con",name
- | Cic.InductiveDefinition (types,_,_,_) ->
- ".ind",
- (match types with (name,_,_,_)::_ -> name | _ -> assert false)
- | _ -> assert false in
- let uri =
- UriManager.uri_of_string (MatitaMisc.qualify status name ^ ext)
- in
- let metasenv = MatitaMisc.get_proof_metasenv status in
- match obj with
- Cic.CurrentProof (_,metasenv',bo,ty,_,_) ->
- assert (metasenv = metasenv');
- let goalno =
- match metasenv' with (goalno,_,_)::_ -> goalno | _ -> assert false in
- let initial_proof = (Some uri, metasenv, bo, ty) in
- { status with proof_status = Incomplete_proof (initial_proof,goalno)}
- | _ ->
- if metasenv <> [] then
- command_error (
- "metasenv not empty while giving a definition with body: " ^
- CicMetaSubst.ppmetasenv metasenv []);
- let status = MatitaSync.add_obj uri obj status in
- match obj with
- Cic.Constant _ -> status
- | Cic.InductiveDefinition (_,_,_,attrs) ->
- let status = generate_elimination_principles uri status in
- let rec get_record_attrs =
- function
- [] -> None
- | (`Class (`Record fields))::_ -> Some fields
- | _::tl -> get_record_attrs tl
- in
- (match get_record_attrs attrs with
- None -> status (* not a record *)
- | Some fields -> generate_projections uri fields status)
- | Cic.CurrentProof _
- | Cic.Variable _ -> assert false
-
-let eval_executable status ex =
- match ex with
- | TacticAst.Tactical (_, tac) -> eval_tactical status tac
- | TacticAst.Command (_, cmd) -> eval_command status cmd
- | TacticAst.Macro (_, mac) ->
- command_error (sprintf "The macro %s can't be in a script"
- (TacticAstPp.pp_macro_cic mac))
-
-let eval_comment status c = status
-
-let eval status st =
- match st with
- | TacticAst.Executable (_,ex) -> eval_executable status ex
- | TacticAst.Comment (_,c) -> eval_comment status c
-
-let disambiguate_term status term =
- let (aliases, metasenv, cic, _) =
- match
- MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
- ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
- ~metasenv:(MatitaMisc.get_proof_metasenv status) term
- with
- | [x] -> x
- | _ -> assert false
- in
- let proof_status =
- match status.proof_status with
- | No_proof -> Intermediate metasenv
- | Incomplete_proof ((uri, _, proof, ty), goal) ->
- Incomplete_proof ((uri, metasenv, proof, ty), goal)
- | Intermediate _ -> Intermediate metasenv
- | Proof _ -> assert false
- in
- let status = { status with proof_status = proof_status } in
- let status = MatitaSync.set_proof_aliases status aliases in
- status, cic
-
-let disambiguate_obj status obj =
- let uri =
- match obj with
- TacticAst.Inductive (_,(name,_,_,_)::_)
- | TacticAst.Record (_,name,_,_) ->
- Some (UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".ind"))
- | TacticAst.Inductive _ -> assert false
- | _ -> None in
- let (aliases, metasenv, cic, _) =
- match
- MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())
- ~aliases:(status.aliases) ~uri obj
- with
- | [x] -> x
- | _ -> assert false
- in
- let proof_status =
- match status.proof_status with
- | No_proof -> Intermediate metasenv
- | Incomplete_proof _
- | Intermediate _
- | Proof _ -> assert false
- in
- let status = { status with proof_status = proof_status } in
- let status = MatitaSync.set_proof_aliases status aliases in
- status, cic
-
-let disambiguate_pattern status (wanted, hyp_paths, goal_path) =
- let interp path = Disambiguate.interpretate_path [] status.aliases path in
- let goal_path = interp goal_path in
- let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
- let status,wanted =
- match wanted with
- None -> status,None
- | Some wanted ->
- let status,wanted = disambiguate_term status wanted in
- status, Some wanted
- in
- status, (wanted, hyp_paths ,goal_path)
-
-let disambiguate_tactic status = function
- | TacticAst.Apply (loc, term) ->
- let status, cic = disambiguate_term status term in
- status, TacticAst.Apply (loc, cic)
- | TacticAst.Absurd (loc, term) ->
- let status, cic = disambiguate_term status term in
- status, TacticAst.Absurd (loc, cic)
- | TacticAst.Assumption loc -> status, TacticAst.Assumption loc
- | TacticAst.Auto (loc,depth,width) -> status, TacticAst.Auto (loc,depth,width)
- | TacticAst.Change (loc, pattern, with_what) ->
- let status, with_what = disambiguate_term status with_what in
- let status, pattern = disambiguate_pattern status pattern in
- status, TacticAst.Change (loc, pattern, with_what)
- | TacticAst.Clear (loc,id) -> status,TacticAst.Clear (loc,id)
- | TacticAst.ClearBody (loc,id) -> status,TacticAst.ClearBody (loc,id)
- | TacticAst.Compare (loc,term) ->
- let status, term = disambiguate_term status term in
- status, TacticAst.Compare (loc,term)
- | TacticAst.Constructor (loc,n) ->
- status, TacticAst.Constructor (loc,n)
- | TacticAst.Contradiction loc ->
- status, TacticAst.Contradiction loc
- | TacticAst.Cut (loc, ident, term) ->
- let status, cic = disambiguate_term status term in
- status, TacticAst.Cut (loc, ident, cic)
- | TacticAst.DecideEquality loc ->
- status, TacticAst.DecideEquality loc
- | TacticAst.Decompose (loc,term) ->
- let status,term = disambiguate_term status term in
- status, TacticAst.Decompose(loc,term)
- | TacticAst.Discriminate (loc,term) ->
- let status,term = disambiguate_term status term in
- status, TacticAst.Discriminate(loc,term)
- | TacticAst.Exact (loc, term) ->
- let status, cic = disambiguate_term status term in
- status, TacticAst.Exact (loc, cic)
- | TacticAst.Elim (loc, term, Some term') ->
- let status, cic1 = disambiguate_term status term in
- let status, cic2 = disambiguate_term status term' in
- status, TacticAst.Elim (loc, cic1, Some cic2)
- | TacticAst.Elim (loc, term, None) ->
- let status, cic = disambiguate_term status term in
- status, TacticAst.Elim (loc, cic, None)
- | TacticAst.ElimType (loc, term) ->
- let status, cic = disambiguate_term status term in
- status, TacticAst.ElimType (loc, cic)
- | TacticAst.Exists loc -> status, TacticAst.Exists loc
- | TacticAst.Fail loc -> status,TacticAst.Fail loc
- | TacticAst.Fold (loc,reduction_kind, term, pattern) ->
- let status, pattern = disambiguate_pattern status pattern in
- let status, term = disambiguate_term status term in
- status, TacticAst.Fold (loc,reduction_kind, term, pattern)
- | TacticAst.FwdSimpl (loc, hyp, names) ->
- status, TacticAst.FwdSimpl (loc, hyp, names)
- | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
- | TacticAst.Generalize (loc,pattern,ident) ->
- let status, pattern = disambiguate_pattern status pattern in
- status, TacticAst.Generalize(loc,pattern,ident)
- | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
- | TacticAst.IdTac loc -> status,TacticAst.IdTac loc
- | TacticAst.Injection (loc,term) ->
- let status, term = disambiguate_term status term in
- status, TacticAst.Injection (loc,term)
- | TacticAst.Intros (loc, num, names) ->
- status, TacticAst.Intros (loc, num, names)
- | TacticAst.LApply (loc, depth, to_what, what, ident) ->
- let f term (status, to_what) =
- let status, term = disambiguate_term status term in
- status, term :: to_what