+ let find n metasenv =
+ try
+ Some (List.find (fun (metano, _, _) -> metano = n) metasenv)
+ with Not_found -> None
+ in
+ let extract l =
+ List.fold_right
+ (fun n acc ->
+ match find n tactic with
+ | Some x -> x::acc
+ | None -> acc
+ ) l [] in
+ let before_l, after_l = split current_goal start in
+ let before_l =
+ List.filter (fun x -> not (List.mem x produced_goals)) before_l in
+ let after_l =
+ List.filter (fun x -> not (List.mem x produced_goals)) after_l in
+ let before = extract before_l in
+ let after = extract after_l in
+ before, after
+ in
+(* |+ DEBUG CODE +|
+ print_m "BEGIN" start;
+ prerr_endline ("goal was: " ^ string_of_int current_goal);
+ prerr_endline ("and metas from refine are:");
+ List.iter
+ (fun t -> prerr_string (" " ^ string_of_int t))
+ new_goals_from_refine;
+ prerr_endline "";
+ print_m "before" before;
+ print_m "metas_for_tactic_head" metas_for_tactic_head;
+ print_m "metas_for_refine_goals" metas_for_refine_goals;
+ print_m "metas_for_tactic_goals" metas_for_tactic_goals;
+ print_m "produced_metas" produced_metas;
+ print_m "after" after;
+|+ FINE DEBUG CODE +| *)
+ before @ produced_metas @ after, goals
+
+(* maybe we only need special cases for apply and goal *)
+let classify_tactic tactic =
+ match tactic with
+ (* tactics that can't close the goal (return a goal we want to "select") *)
+ | GrafiteAst.Rewrite _
+ | GrafiteAst.Split _
+ | GrafiteAst.Replace _
+ | GrafiteAst.Reduce _
+ | GrafiteAst.Injection _
+ | GrafiteAst.IdTac _
+ | GrafiteAst.Generalize _
+ | GrafiteAst.Elim _
+ | GrafiteAst.Cut _
+ | GrafiteAst.Decompose _ -> true, true
+ (* tactics we don't want to reorder goals. I think only Goal needs this. *)
+ | GrafiteAst.Goal _ -> false, true
+ (* tactics like apply *)
+ | _ -> true, false
+
+let apply_tactic tactic (status, goal) =
+(* prerr_endline "apply_tactic"; *)
+(* prerr_endline (Continuationals.Stack.pp (MatitaMisc.get_stack status)); *)
+ let starting_metasenv = MatitaMisc.get_proof_metasenv status in
+ let before = List.map (fun g, _, _ -> g) starting_metasenv in
+(* prerr_endline "disambiguate"; *)
+ let status_ref, tactic = disambiguate_tactic status goal tactic in
+ let metasenv_after_refinement = MatitaMisc.get_proof_metasenv !status_ref in
+ let proof = MatitaMisc.get_current_proof !status_ref in
+ let proof_status = proof, goal in
+ let needs_reordering, always_opens_a_goal = classify_tactic tactic in
+ let tactic = tactic_of_ast tactic in
+ (* apply tactic will change the status pointed by status_ref ... *)
+(* prerr_endline "apply_tactic bassa"; *)
+ let (proof, opened) = ProofEngineTypes.apply_tactic tactic proof_status in
+ let after = ProofEngineTypes.goals_of_proof proof in
+ let opened_goals, closed_goals = Tacticals.goals_diff ~before ~after ~opened in
+(* prerr_endline("before: " ^ String.concat ", " (List.map string_of_int before));
+prerr_endline("after: " ^ String.concat ", " (List.map string_of_int after));
+prerr_endline("opened: " ^ String.concat ", " (List.map string_of_int opened)); *)
+(* prerr_endline("opened_goals: " ^ String.concat ", " (List.map string_of_int opened_goals));
+prerr_endline("closed_goals: " ^ String.concat ", " (List.map string_of_int closed_goals)); *)
+ let proof, opened_goals =
+ if needs_reordering then begin
+ let uri, metasenv_after_tactic, t, ty = proof in
+(* prerr_endline ("goal prima del riordino: " ^ String.concat " " (List.map string_of_int (ProofEngineTypes.goals_of_proof proof))); *)
+ let reordered_metasenv, opened_goals =
+ reorder_metasenv
+ starting_metasenv
+ metasenv_after_refinement metasenv_after_tactic
+ opened goal always_opens_a_goal
+ in
+ let proof' = uri, reordered_metasenv, t, ty in
+(* prerr_endline ("goal dopo il riordino: " ^ String.concat " " (List.map string_of_int (ProofEngineTypes.goals_of_proof proof'))); *)
+ proof', opened_goals
+ end
+ else
+ proof, opened_goals
+ in
+ let incomplete_proof =
+ match !status_ref.proof_status with
+ | Incomplete_proof p -> p
+ | _ -> assert false
+ in
+ { !status_ref with proof_status =
+ Incomplete_proof { incomplete_proof with proof = proof } },
+ opened_goals, closed_goals
+
+module MatitaStatus =
+struct
+ type input_status = MatitaTypes.status * ProofEngineTypes.goal
+
+ type output_status =
+ MatitaTypes.status * ProofEngineTypes.goal list * ProofEngineTypes.goal list
+
+ type tactic = input_status -> output_status
+
+ let id_tactic = apply_tactic (GrafiteAst.IdTac DisambiguateTypes.dummy_floc)
+ let mk_tactic tac = tac
+ let apply_tactic tac = tac
+ let goals (_, opened, closed) = opened, closed
+ let set_goals (opened, closed) (status, _, _) = (status, opened, closed)
+ let get_stack (status, _) = MatitaMisc.get_stack status
+
+ let set_stack stack (status, opened, closed) =
+ MatitaMisc.set_stack stack status, opened, closed
+
+ let inject (status, _) = (status, [], [])
+ let focus goal (status, _, _) = (status, goal)
+end
+
+module MatitaTacticals = Tacticals.Make (MatitaStatus)
+
+let eval_tactical status tac =
+ let rec tactical_of_ast l tac =
+ match tac with
+ | GrafiteAst.Tactic (loc, tactic) ->
+ MatitaTacticals.tactic (MatitaStatus.mk_tactic (apply_tactic tactic))
+ | GrafiteAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
+ assert (l > 0);
+ MatitaTacticals.seq ~tactics:(List.map (tactical_of_ast (l+1)) tacticals)
+ | GrafiteAst.Do (loc, n, tactical) ->
+ MatitaTacticals.do_tactic ~n ~tactic:(tactical_of_ast (l+1) tactical)
+ | GrafiteAst.Repeat (loc, tactical) ->
+ MatitaTacticals.repeat_tactic ~tactic:(tactical_of_ast (l+1) tactical)
+ | GrafiteAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
+ assert (l > 0);
+ MatitaTacticals.thens ~start:(tactical_of_ast (l+1) tactical)
+ ~continuations:(List.map (tactical_of_ast (l+1)) tacticals)
+ | GrafiteAst.First (loc, tacticals) ->
+ MatitaTacticals.first
+ ~tactics:(List.map (fun t -> "", tactical_of_ast (l+1) t) tacticals)
+ | GrafiteAst.Try (loc, tactical) ->
+ MatitaTacticals.try_tactic ~tactic:(tactical_of_ast (l+1) tactical)
+ | GrafiteAst.Solve (loc, tacticals) ->
+ MatitaTacticals.solve_tactics
+ ~tactics:(List.map (fun t -> "", tactical_of_ast (l+1) t) tacticals)
+
+ | GrafiteAst.Skip loc -> MatitaTacticals.skip
+ | GrafiteAst.Dot loc -> MatitaTacticals.dot
+ | GrafiteAst.Semicolon loc -> MatitaTacticals.semicolon
+ | GrafiteAst.Branch loc -> MatitaTacticals.branch
+ | GrafiteAst.Shift loc -> MatitaTacticals.shift
+ | GrafiteAst.Pos (loc, i) -> MatitaTacticals.pos i
+ | GrafiteAst.Merge loc -> MatitaTacticals.merge
+ | GrafiteAst.Focus (loc, goals) -> MatitaTacticals.focus goals
+ | GrafiteAst.Unfocus loc -> MatitaTacticals.unfocus
+ in
+ let status, _, _ = tactical_of_ast 0 tac (status, ~-1) in
+ let status = (* is proof completed? *)
+ match status.proof_status with
+ | Incomplete_proof { stack = stack; proof = proof }
+ when Continuationals.Stack.is_empty stack ->
+ { status with proof_status = Proof proof }
+ | _ -> status
+ in
+ status
+
+let eval_coercion status coercion =
+ let coer_uri,coer_ty =
+ match coercion with
+ | Cic.Const (uri,_)
+ | Cic.Var (uri,_) ->
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ (match o with
+ | Cic.Constant (_,_,ty,_,_)
+ | Cic.Variable (_,_,ty,_,_) ->
+ uri,ty
+ | _ -> assert false)
+ | Cic.MutConstruct (uri,t,c,_) ->
+ let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+ (match o with
+ | Cic.InductiveDefinition (l,_,_,_) ->
+ let (_,_,_,cl) = List.nth l t in
+ let (_,cty) = List.nth cl c in
+ uri,cty
+ | _ -> assert false)
+ | _ -> assert false
+ in
+ (* we have to get the source and the tgt type uri
+ * in Coq syntax we have already their names, but
+ * since we don't support Funclass and similar I think
+ * all the coercion should be of the form
+ * (A:?)(B:?)T1->T2
+ * So we should be able to extract them from the coercion type
+ *)
+ let extract_last_two_p ty =
+ let rec aux = function
+ | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) -> aux (Cic.Prod(n,t1,t2))
+ | Cic.Prod( _, src, tgt) -> src, tgt
+ | _ -> assert false
+ in
+ aux ty
+ in
+ let ty_src,ty_tgt = extract_last_two_p coer_ty in
+ let context = [] in
+ let src_uri = CoercDb.coerc_carr_of_term (CicReduction.whd context ty_src) in
+ let tgt_uri = CoercDb.coerc_carr_of_term (CicReduction.whd context ty_tgt) in
+ let new_coercions =
+ CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri in
+ let status =
+ List.fold_left (fun s (uri,o,_) -> MatitaSync.add_obj uri o status)
+ status new_coercions in
+ let statement_of name =
+ GrafiteAst.Coercion (DisambiguateTypes.dummy_floc,
+ (CicNotationPt.Ident (name, None)))
+ in
+ let moo_content =
+ statement_of (UriManager.name_of_uri coer_uri) ::
+ (List.map
+ (fun (uri, _, _) ->
+ statement_of (UriManager.name_of_uri uri))
+ new_coercions)
+ in
+ let status = add_moo_content moo_content status in
+ { status with proof_status = No_proof }
+
+let generate_elimination_principles uri status =
+ let status' = ref status in
+ let elim sort =
+ try
+ let uri,obj = CicElim.elim_of ~sort uri 0 in
+ status' := MatitaSync.add_obj uri obj !status'
+ with CicElim.Can_t_eliminate -> ()
+ in
+ try
+ List.iter elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ];
+ !status'
+ with exn ->
+ MatitaSync.time_travel ~present:!status' ~past:status;
+ raise exn
+
+let generate_projections uri fields status =
+ let projections = CicRecord.projections_of uri fields in
+ List.fold_left
+ (fun status (uri, name, bo) ->
+ try
+ let ty, ugraph =
+ CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
+ let attrs = [`Class `Projection; `Generated] in
+ let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
+ MatitaSync.add_obj uri obj status
+ with
+ CicTypeChecker.TypeCheckerFailure s ->
+ MatitaLog.message
+ ("Unable to create projection " ^ name ^ " cause: " ^ (Lazy.force 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_moo_ref = ref (fun _ _ _ -> assert false);;
+
+let disambiguate_obj status obj =
+ let uri =
+ match obj with
+ GrafiteAst.Inductive (_,(name,_,_,_)::_)
+ | GrafiteAst.Record (_,name,_,_) ->
+ Some (UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".ind"))
+ | GrafiteAst.Inductive _ -> assert false
+ | GrafiteAst.Theorem _ -> None in
+ let (diff, metasenv, cic, _) =
+ singleton
+ (MatitaDisambiguator.disambiguate_obj ~dbd:(MatitaDb.instance ())
+ ~aliases:status.aliases ~universe:(Some status.multi_aliases) ~uri obj)
+ in
+ let proof_status =
+ match status.proof_status with
+ | No_proof -> Intermediate metasenv
+ | Incomplete_proof _
+ | Proof _ -> command_error "imbricated proofs not allowed"
+ | Intermediate _ -> assert false