-let debug = true ;;
-let debug_print = if debug then prerr_endline else ignore ;;
-
-(** create a ProofEngineTypes.mk_fresh_name_type function which uses given
- * names as long as they are available, then it fallbacks to name generation
- * using FreshNamesGenerator module *)
-let namer_of names =
- let len = List.length names in
- let count = ref 0 in
- fun metasenv context name ~typ ->
- if !count < len then begin
- let name = Cic.Name (List.nth names !count) in
- incr count;
- name
- end else
- FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
-
-let tactic_of_ast = function
- | TacticAst.Intros (_, None, names) ->
- (* TODO Zack implement intros length *)
- PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
- | TacticAst.Intros (_, Some num, names) ->
- (* TODO Zack implement intros length *)
- PrimitiveTactics.intros_tac ~howmany:num
- ~mk_fresh_name_callback:(namer_of names) ()
- | TacticAst.Reflexivity _ -> Tactics.reflexivity
- | TacticAst.Assumption _ -> Tactics.assumption
- | TacticAst.Contradiction _ -> Tactics.contradiction
- | TacticAst.Exists _ -> Tactics.exists
- | TacticAst.Fourier _ -> Tactics.fourier
- | TacticAst.Goal (_, n) -> Tactics.set_goal n
- | TacticAst.Left _ -> Tactics.left
- | TacticAst.Right _ -> Tactics.right
- | TacticAst.Ring _ -> Tactics.ring
- | TacticAst.Split _ -> Tactics.split
- | TacticAst.Symmetry _ -> Tactics.symmetry
- | TacticAst.Transitivity (_, term) -> Tactics.transitivity term
- | TacticAst.Apply (_, term) -> Tactics.apply term
- | TacticAst.Absurd (_, term) -> Tactics.absurd term
- | TacticAst.Exact (_, term) -> Tactics.exact term
- | TacticAst.Cut (_, term) -> Tactics.cut term
- | TacticAst.Elim (_, term, _) ->
- (* TODO Zack implement "using" argument *)
- (* old: Tactics.elim_intros_simpl term *)
- Tactics.elim_intros term
- | TacticAst.ElimType (_, term) -> Tactics.elim_type term
- | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what
- | TacticAst.Auto (_,num) ->
- AutoTactic.auto_tac ~num (MatitaDb.instance ())
- | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what
-(*
- (* TODO Zack a lot more of tactics to be implemented here ... *)
- | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
- | TacticAst.Change of 'term * 'term * 'ident option
- | TacticAst.Decompose of 'ident * 'ident list
- | TacticAst.Discriminate of 'ident
- | TacticAst.Fold of reduction_kind * 'term
- | TacticAst.Injection of 'ident
- | TacticAst.Replace_pattern of 'term pattern * 'term
-*)
- | TacticAst.LetIn (loc,term,name) ->
- Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
- | TacticAst.ReduceAt (_,reduction_kind,ident,path) ->
- ProofEngineTypes.mk_tactic
- (fun (((_,metasenv,_,_),goal) as status) ->
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let where, also_in_hypotheses =
- if ident = "goal" then
- ty, false
- else
- let hyp =
- try
- List.find (function
- | Some (Cic.Name name,entry) when name = ident -> true
- | _ -> false)
- context
- with
- Not_found -> raise (ProofEngineTypes.Fail (ident ^ " is not an hypothesis"))
- in
- (match hyp with
- | Some (_, Cic.Decl term) -> term
- | Some (_, Cic.Def (term,ty)) -> term
- | None -> assert false),true
- in
- let pointers = CicUtil.select ~term:where ~context:path in
- (match reduction_kind with
- | `Normalize ->
- ProofEngineTypes.apply_tactic
- (Tactics.normalize ~also_in_hypotheses ~terms:(Some pointers))
- status
- | `Reduce ->
- ProofEngineTypes.apply_tactic
- (Tactics.reduce ~also_in_hypotheses ~terms:(Some pointers))
- status
- | `Simpl ->
- ProofEngineTypes.apply_tactic
- (Tactics.simpl ~also_in_hypotheses ~terms:(Some pointers))
- status
- | `Whd ->
- ProofEngineTypes.apply_tactic
- (Tactics.whd ~also_in_hypotheses ~terms:(Some pointers))
- status))
- | TacticAst.Reduce (_,reduction_kind,opts) ->
- let terms, also_in_hypotheses =
- match opts with
- | Some (l,`Goal) -> Some l, false
- | Some (l,`Everywhere) -> Some l, true
- | None -> None, false
- in
- (match reduction_kind with
- | `Normalize -> Tactics.normalize ~also_in_hypotheses ~terms
- | `Reduce -> Tactics.reduce ~also_in_hypotheses ~terms
- | `Simpl -> Tactics.simpl ~also_in_hypotheses ~terms
- | `Whd -> Tactics.whd ~also_in_hypotheses ~terms)
- | TacticAst.Rewrite (_,dir,t,ident) ->
- if dir = `Left then
- EqualityTactics.rewrite_tac ~term:t
- else
- EqualityTactics.rewrite_back_tac ~term:t
- | _ -> assert false
-
-let eval_tactical status tac =
- let apply_tactic tactic =
- let (proof, goals) =
- ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status)
- in
- let new_status =
- match goals with
- | [] ->
- let (_,metasenv,_,_) = proof in
- (match metasenv with
- | [] -> Proof proof
- | (ng,_,_)::_ -> Incomplete_proof (proof,ng))
- | ng::_ -> Incomplete_proof (proof, ng)
- in
- { status with proof_status = new_status }
- in
- let rec tactical_of_ast = function
- | TacticAst.Tactic (loc, tactic) -> tactic_of_ast tactic
- | TacticAst.Fail loc -> Tacticals.fail
- | TacticAst.Do (loc, num, tactical) ->
- Tacticals.do_tactic num (tactical_of_ast tactical)
- | TacticAst.IdTac loc -> Tacticals.id_tac
- | TacticAst.Repeat (loc, tactical) ->
- Tacticals.repeat_tactic (tactical_of_ast tactical)
- | TacticAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *)
- Tacticals.seq (List.map tactical_of_ast tacticals)
- | TacticAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *)
- Tacticals.thens (tactical_of_ast tactical)
- (List.map tactical_of_ast tacticals)
- | TacticAst.Tries (loc, tacticals) ->
- Tacticals.try_tactics
- (List.map (fun t -> "", tactical_of_ast t) tacticals)
- | TacticAst.Try (loc, tactical) ->
- Tacticals.try_tactic (tactical_of_ast tactical)
- in
- apply_tactic (tactical_of_ast tac)
-
-(** given a uri and a type list (the contructors types) builds a list of pairs
- * (name,uri) that is used to generate authomatic aliases **)
-let extract_alias types uri =
- fst(List.fold_left (
- fun (acc,i) (name, _, _, cl) ->
- ((name, UriManager.string_of_uriref (uri,[i]))
- ::
- (fst(List.fold_left (
- fun (acc,j) (name,_) ->
- (((name,UriManager.string_of_uriref (uri,[i;j])) :: acc) , j+1)
- ) (acc,1) cl))),i+1
- ) ([],0) types)
-
-(** adds a (name,uri) list l to a disambiguation environment e **)
-let env_of_list l e =
- let module DT = DisambiguateTypes in
- let module DTE = DisambiguateTypes.Environment in
- List.fold_left (
- fun e (name,uri) ->
- DTE.add
- (DT.Id name)
- (uri,fun _ _ _ -> CicUtil.term_of_uri uri)
- e
- ) e l
-
-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 =
- let ty_src = CicReduction.whd context ty_src in
- UriManager.uri_of_string (CicUtil.uri_of_term ty_src)
- in
- let tgt_uri =
- let ty_tgt = CicReduction.whd context ty_tgt in
- UriManager.uri_of_string (CicUtil.uri_of_term ty_tgt)
- in
- let new_coercions =
- (* also adds them to the Db *)
- CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri
- in
- let status =
- List.fold_left (
- fun s (uri,o,ugraph) ->
- match o with
- | Cic.Constant (_,Some body, ty, params, attrs) ->
- MatitaSync.add_constant ~uri ~body ~ty ~ugraph ~params ~attrs status
- | _ -> assert false
- ) status new_coercions
- in
- {status with proof_status = No_proof}
-
-let eval_command status cmd =
- match cmd with
- | TacticAst.Set (loc, name, value) -> set_option status name value
- | 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 proved_ty,ugraph =
- CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph
- in
- let b,ugraph =
- CicReduction.are_convertible [] proved_ty ty ugraph
- in
- if not b then
- command_error
- ("The type of your proof is not convertible with the "^
- "type you've declared!");
- MatitaLog.message (sprintf "%s defined" suri);
- let status = MatitaSync.add_constant ~uri ~body:bo ~ty ~ugraph status in
- let status =
- let name = UriManager.name_of_uri uri in
- let new_env = env_of_list [(name,suri)] status.aliases in
- {status with aliases = new_env }
- in
- {status with proof_status = No_proof }
- | TacticAst.Inductive (loc, dummy_params, types) ->
- (* dummy_params are not real params, it is a list of nothing, and the only
- * semantic content is the len, that is leftno (note: leftno and pamaters
- * have nothing in common).
- *)
- let suri =
- match types with
- | (name, _, _, _) :: tl -> MatitaMisc.qualify status name ^ ".ind"
- | _ -> assert false
- in
- let uri = UriManager.uri_of_string suri in
- let leftno = List.length dummy_params in
- let obj = Cic.InductiveDefinition (types, [], leftno, []) in
- let ugraph =
- CicTypeChecker.typecheck_mutual_inductive_defs uri
- (types, [], leftno) CicUniv.empty_ugraph
- in
- let status =
- MatitaSync.add_inductive_def
- ~uri ~types ~params:[] ~leftno ~ugraph status
- in
- (* aliases for the constructors and types *)
- let aliases = env_of_list (extract_alias types uri) status.aliases in
- (* aliases for the eliminations principles *)
- let aliases =
- let base = String.sub suri 0 (String.length suri - 4) in
- env_of_list
- (List.fold_left (
- fun acc suffix ->
- if List.exists (
- fun (uri,_) -> UriManager.string_of_uri uri = base ^ suffix
- ) status.objects then
- let u = base ^ suffix in
- (UriManager.name_of_uri (UriManager.uri_of_string u),u)::acc
- else
- acc
- ) [] ["_ind.con";"_rec.con";"_rec_t.con"]) aliases
- in
- let status = {status with proof_status = No_proof } in
- { status with aliases = aliases}
- | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) ->
- let uri =
- UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
- in
- let goalno = 1 in
- let metasenv, body =
- match status.proof_status with
- | Intermediate metasenv ->
- ((goalno, [], ty) :: metasenv) , Cic.Meta (goalno,[])
- | _-> assert false
- in
- let initial_proof = (Some uri, metasenv, body, ty) in
- { status with proof_status = Incomplete_proof (initial_proof,goalno)}
- | TacticAst.Theorem (loc, thm_flavour, Some name, ty, Some body) ->
- let uri =
- UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
- in
- let metasenv = MatitaMisc.get_proof_metasenv status in
- let (body_type, ugraph) =
- CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph
- in
- let (subst, metasenv, ugraph) =
- CicUnification.fo_unif metasenv [] body_type ty ugraph
- in
- if metasenv <> [] then
- command_error (
- "metasenv not empty while giving a definition with body: " ^
- CicMetaSubst.ppmetasenv metasenv []) ;
- let body = CicMetaSubst.apply_subst subst body in
- let ty = CicMetaSubst.apply_subst subst ty in
- let status = MatitaSync.add_constant ~uri ~body ~ty ~ugraph status in
- let status =
- let suri = UriManager.string_of_uri uri in
- let new_env = env_of_list [(name,suri)] status.aliases in
- {status with aliases = new_env }
- in
- {status with proof_status = No_proof}
- | TacticAst.Theorem (_, _, None, _, _) ->
- command_error "The grammar should avoid having unnamed theorems!"
- | TacticAst.Coercion (loc, coercion) ->
- eval_coercion status coercion
- | TacticAst.Alias (loc, spec) ->
- match spec with
- | TacticAst.Ident_alias (id,uri) ->
- {status with aliases =
- DisambiguateTypes.Environment.add
- (DisambiguateTypes.Id id)
- ("boh?",(fun _ _ _ -> CicUtil.term_of_uri uri))
- status.aliases }
- | TacticAst.Symbol_alias (symb, instance, desc) ->
- {status with aliases =
- DisambiguateTypes.Environment.add
- (DisambiguateTypes.Symbol (symb,instance))
- (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
- status.aliases }
- | TacticAst.Number_alias (instance,desc) ->
- {status with aliases =
- DisambiguateTypes.Environment.add
- (DisambiguateTypes.Num instance)
- (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases }
-
-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))