helm/matita/matitaEngine.ml

   1
   2 open Printf
   3
   4 open MatitaTypes
   5
   6
   7 (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
   8   * names as long as they are available, then it fallbacks to name generation
   9   * using FreshNamesGenerator module *)
  10 let namer_of names =
  11   let len = List.length names in
  12   let count = ref 0 in
  13   fun metasenv context name ~typ ->
  14     if !count < len then begin
  15       let name = Cic.Name (List.nth names !count) in
  16       incr count;
  17       name
  18     end else
  19       FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
  20
  21 let tactic_of_ast = function
  22   | TacticAst.Intros (_, _, names) ->
  23       (* TODO Zack implement intros length *)
  24       PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
  25   | TacticAst.Reflexivity _ -> Tactics.reflexivity
  26   | TacticAst.Assumption _ -> Tactics.assumption
  27   | TacticAst.Contradiction _ -> Tactics.contradiction
  28   | TacticAst.Exists _ -> Tactics.exists
  29   | TacticAst.Fourier _ -> Tactics.fourier
  30   | TacticAst.Goal (_, n) -> Tactics.set_goal n
  31   | TacticAst.Left _ -> Tactics.left
  32   | TacticAst.Right _ -> Tactics.right
  33   | TacticAst.Ring _ -> Tactics.ring
  34   | TacticAst.Split _ -> Tactics.split
  35   | TacticAst.Symmetry _ -> Tactics.symmetry
  36   | TacticAst.Transitivity (_, term) -> Tactics.transitivity term
  37   | TacticAst.Apply (_, term) -> Tactics.apply term
  38   | TacticAst.Absurd (_, term) -> Tactics.absurd term
  39   | TacticAst.Exact (_, term) -> Tactics.exact term
  40   | TacticAst.Cut (_, term) -> Tactics.cut term
  41   | TacticAst.Elim (_, term, _) ->
  42       (* TODO Zack implement "using" argument *)
  43       Tactics.elim_intros_simpl term
  44   | TacticAst.ElimType (_, term) -> Tactics.elim_type term
  45   | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what
  46 (*   | TacticAst.Auto _ -> Tactics.auto_new ~dbd *)
  47   | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what
  48 (*
  49   (* TODO Zack a lot more of tactics to be implemented here ... *)
  50   | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
  51   | TacticAst.Change of 'term * 'term * 'ident option
  52   | TacticAst.Decompose of 'ident * 'ident list
  53   | TacticAst.Discriminate of 'ident
  54   | TacticAst.Fold of reduction_kind * 'term
  55   | TacticAst.Injection of 'ident
  56   | TacticAst.LetIn of 'term * 'ident
  57   | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option
  58   | TacticAst.Replace_pattern of 'term pattern * 'term
  59   | TacticAst.Rewrite of direction * 'term * 'ident option
  60 *)
  61   | _ -> assert false
  62
  63 let eval_tactical status tac =
  64   let apply_tactic tactic =
  65     let (proof, goals) =
  66       ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status)
  67     in
  68     let new_status =
  69       match goals with
  70       | [] ->
  71           let (_,metasenv,_,_) = proof in
  72           (match metasenv with
  73           | [] -> Proof proof
  74           | (ng,_,_)::_ -> Incomplete_proof (proof,ng))
  75       | ng::_ -> Incomplete_proof (proof, ng)
  76     in
  77     { status with proof_status = new_status }
  78   in
  79   let rec tactical_of_ast = function
  80     | TacticAst.Tactic (loc, tactic) -> tactic_of_ast tactic
  81     | TacticAst.Fail loc -> Tacticals.fail
  82     | TacticAst.Do (loc, num, tactical) ->
  83         Tacticals.do_tactic num (tactical_of_ast tactical)
  84     | TacticAst.IdTac loc -> Tacticals.id_tac
  85     | TacticAst.Repeat (loc, tactical) ->
  86         Tacticals.repeat_tactic (tactical_of_ast tactical)
  87     | TacticAst.Seq (loc, tacticals) ->  (* tac1; tac2; ... *)
  88         Tacticals.seq (List.map tactical_of_ast tacticals)
  89     | TacticAst.Then (loc, tactical, tacticals) ->  (* tac; [ tac1 | ... ] *)
  90         Tacticals.thens (tactical_of_ast tactical)
  91           (List.map tactical_of_ast tacticals)
  92     | TacticAst.Tries (loc, tacticals) ->
  93         Tacticals.try_tactics
  94           (List.map (fun t -> "", tactical_of_ast t) tacticals)
  95     | TacticAst.Try (loc, tactical) ->
  96         Tacticals.try_tactic (tactical_of_ast tactical)
  97   in
  98   apply_tactic (tactical_of_ast tac)
  99
 100 let eval_command status cmd =
 101   match cmd with
 102   | TacticAst.Set (loc, name, value) -> set_option status name value
 103   | TacticAst.Qed loc ->
 104       let uri, metasenv, bo, ty =
 105         match status.proof_status with
 106         | Proof (Some uri, metasenv, body, ty) ->
 107             uri, metasenv, body, ty
 108         | Proof (None, metasenv, body, ty) ->
 109             command_error
 110               ("Someone allows to start a thm without giving the "^
 111                "name/uri. This should be fixed!")
 112         | _-> command_error "You can't qed an uncomplete theorem"
 113       in
 114       let suri = UriManager.string_of_uri uri in
 115       if metasenv <> [] then
 116         command_error "Proof not completed! metasenv is not empty!";
 117       let proved_ty,ugraph =
 118         CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph
 119       in
 120       let b,ugraph =
 121         CicReduction.are_convertible [] proved_ty ty ugraph
 122       in
 123       if not b then
 124         command_error
 125           ("The type of your proof is not convertible with the "^
 126           "type you've declared!");
 127       MatitaLog.message (sprintf "%s defined" suri);
 128       let status = MatitaSync.add_constant ~uri ~body:bo ~ty ~ugraph status in
 129       {status with proof_status = No_proof }
 130   | TacticAst.Inductive (loc, dummy_params, types) ->
 131       (* dummy_params are not real params, it is a list of nothing, and the only
 132        * semantic content is the len, that is leftno (note: leftno and pamaters
 133        * have nothing in common).
 134        *)
 135       let suri =
 136         match types with
 137         | (name, _, _, _) :: tl -> MatitaMisc.qualify status name ^ ".ind"
 138         | _ -> assert false
 139       in
 140       let uri = UriManager.uri_of_string suri in
 141       let leftno = List.length dummy_params in
 142       let obj = Cic.InductiveDefinition (types, [], leftno, []) in
 143       let ugraph =
 144         CicTypeChecker.typecheck_mutual_inductive_defs uri
 145           (types, [], leftno) CicUniv.empty_ugraph
 146       in
 147         MatitaSync.add_inductive_def
 148           ~uri ~types ~params:[] ~leftno ~ugraph status;
 149   | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) ->
 150       let uri =
 151         UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
 152       in
 153       let goalno = 1 in
 154       let metasenv, body =
 155         match status.proof_status with
 156         | Intermediate metasenv ->
 157             ((goalno, [], ty) :: metasenv) , Cic.Meta (goalno,[])
 158         | _-> assert false
 159       in
 160       let initial_proof = (Some uri, metasenv, body, ty) in
 161       { status with proof_status = Incomplete_proof (initial_proof,goalno)}
 162   | TacticAst.Theorem (loc, thm_flavour, Some name, ty, Some body) ->
 163       let uri =
 164         UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
 165       in
 166       let metasenv = MatitaMisc.get_proof_metasenv status in
 167       let (body_type, ugraph) =
 168         CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph
 169       in
 170       let (subst, metasenv, ugraph) =
 171         CicUnification.fo_unif metasenv [] body_type ty ugraph
 172       in
 173       if metasenv <> [] then
 174         command_error
 175           "metasenv not empty while giving a definition with body";
 176       let body = CicMetaSubst.apply_subst subst body in
 177       let ty = CicMetaSubst.apply_subst subst ty in
 178       MatitaSync.add_constant ~uri ~body ~ty ~ugraph status
 179   | TacticAst.Theorem (_, _, None, _, _) ->
 180       command_error "The grammas should avoid having unnamed theorems!"
 181   | TacticAst.Coercion (loc, term) -> assert false  (** TODO *)
 182   | TacticAst.Alias (loc, spec) ->
 183       match spec with
 184       | TacticAst.Ident_alias (id,uri) ->
 185           {status with aliases =
 186             DisambiguateTypes.Environment.add
 187               (DisambiguateTypes.Id id)
 188               ("boh?",(fun _ _ _ -> CicUtil.term_of_uri uri))
 189               status.aliases }
 190       | TacticAst.Symbol_alias (symb, instance, desc) ->
 191           {status with aliases =
 192             DisambiguateTypes.Environment.add
 193               (DisambiguateTypes.Symbol (symb,instance))
 194               (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
 195               status.aliases }
 196       | TacticAst.Number_alias (instance,desc) ->
 197           {status with aliases =
 198             DisambiguateTypes.Environment.add
 199               (DisambiguateTypes.Num instance)
 200               (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases }
 201
 202 let eval status st =
 203   match st with
 204   | TacticAst.Tactical (_, tac) -> eval_tactical status tac
 205   | TacticAst.Command (_, cmd) -> eval_command status cmd
 206   | TacticAst.Macro (_, mac) ->
 207       command_error (sprintf "The macro %s can't be in a script"
 208         (TacticAstPp.pp_macro_cic mac))
 209
 210 let disambiguate_term status term =
 211   let (aliases, metasenv, cic, _) =
 212     match
 213       MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
 214         ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
 215         ~metasenv:(MatitaMisc.get_proof_metasenv status) term
 216     with
 217     | [x] -> x
 218     | _ -> assert false
 219   in
 220   let proof_status =
 221     match status.proof_status with
 222     | No_proof -> Intermediate metasenv
 223     | Incomplete_proof ((uri, _, proof, ty), goal) ->
 224         Incomplete_proof ((uri, metasenv, proof, ty), goal)
 225     | Intermediate _ -> Intermediate metasenv
 226     | Proof _ -> assert false
 227   in
 228   let status =
 229     { status with
 230         aliases = aliases;
 231         proof_status = proof_status }
 232   in
 233   status, cic
 234
 235 let disambiguate_terms status terms =
 236   let term = CicAst.pack terms in
 237   let status, term = disambiguate_term status term in
 238   status, CicUtil.unpack term
 239
 240 let disambiguate_tactic status = function
 241   | TacticAst.Transitivity (loc, term) ->
 242       let status, cic = disambiguate_term status term in
 243       status, TacticAst.Transitivity (loc, cic)
 244   | TacticAst.Apply (loc, term) ->
 245       let status, cic = disambiguate_term status term in
 246       status, TacticAst.Apply (loc, cic)
 247   | TacticAst.Absurd (loc, term) ->
 248       let status, cic = disambiguate_term status term in
 249       status, TacticAst.Absurd (loc, cic)
 250   | TacticAst.Exact (loc, term) ->
 251       let status, cic = disambiguate_term status term in
 252       status, TacticAst.Exact (loc, cic)
 253   | TacticAst.Cut (loc, term) ->
 254       let status, cic = disambiguate_term status term in
 255       status, TacticAst.Cut (loc, cic)
 256   | TacticAst.Elim (loc, term, Some term') ->
 257       let status, cic1 = disambiguate_term status term in
 258       let status, cic2 = disambiguate_term status term' in
 259       status, TacticAst.Elim (loc, cic1, Some cic2)
 260   | TacticAst.Elim (loc, term, None) ->
 261       let status, cic = disambiguate_term status term in
 262       status, TacticAst.Elim (loc, cic, None)
 263   | TacticAst.ElimType (loc, term) ->
 264       let status, cic = disambiguate_term status term in
 265       status, TacticAst.ElimType (loc, cic)
 266   | TacticAst.Replace (loc, what, with_what) ->
 267       let status, cic1 = disambiguate_term status what in
 268       let status, cic2 = disambiguate_term status with_what in
 269       status, TacticAst.Replace (loc, cic1, cic2)
 270   | TacticAst.Change (loc, what, with_what, ident) ->
 271       let status, cic1 = disambiguate_term status what in
 272       let status, cic2 = disambiguate_term status with_what in
 273       status, TacticAst.Change (loc, cic1, cic2, ident)
 274 (*
 275   (* TODO Zack a lot more of tactics to be implemented here ... *)
 276   | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
 277   | TacticAst.Change of 'term * 'term * 'ident option
 278   | TacticAst.Decompose of 'ident * 'ident list
 279   | TacticAst.Discriminate of 'ident
 280   | TacticAst.Fold of reduction_kind * 'term
 281   | TacticAst.Injection of 'ident
 282   | TacticAst.LetIn of 'term * 'ident
 283   | TacticAst.Reduce of reduction_kind * 'term pattern * 'ident option
 284   | TacticAst.Replace_pattern of 'term pattern * 'term
 285   | TacticAst.Rewrite of direction * 'term * 'ident option
 286 *)
 287   | TacticAst.Intros (loc, num, names) ->
 288       status, TacticAst.Intros (loc, num, names)
 289   | TacticAst.Auto loc -> status, TacticAst.Auto loc
 290   | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc
 291   | TacticAst.Assumption loc -> status, TacticAst.Assumption loc
 292   | TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc
 293   | TacticAst.Exists loc -> status, TacticAst.Exists loc
 294   | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
 295   | TacticAst.Left loc -> status, TacticAst.Left loc
 296   | TacticAst.Right loc -> status, TacticAst.Right loc
 297   | TacticAst.Ring loc -> status, TacticAst.Ring loc
 298   | TacticAst.Split loc -> status, TacticAst.Split loc
 299   | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
 300   | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
 301   | x ->
 302       print_endline ("Not yet implemented:" ^ TacticAstPp.pp_tactic x);
 303       assert false
 304
 305 let rec disambiguate_tactical status = function
 306   | TacticAst.Tactic (loc, tactic) ->
 307       let status, tac = disambiguate_tactic status tactic in
 308       status, TacticAst.Tactic (loc, tac)
 309   | TacticAst.Do (loc, num, tactical) ->
 310       let status, tac = disambiguate_tactical status tactical in
 311       status, TacticAst.Do (loc, num, tac)
 312   | TacticAst.Repeat (loc, tactical) ->
 313       let status, tac = disambiguate_tactical status tactical in
 314       status, TacticAst.Repeat (loc, tac)
 315   | TacticAst.Seq (loc, tacticals) ->  (* tac1; tac2; ... *)
 316       let status, tacticals = disambiguate_tacticals status tacticals in
 317       let tacticals = List.rev tacticals in
 318       status, TacticAst.Seq (loc, tacticals)
 319   | TacticAst.Then (loc, tactical, tacticals) ->  (* tac; [ tac1 | ... ] *)
 320       let status, tactical = disambiguate_tactical status tactical in
 321       let status, tacticals = disambiguate_tacticals status tacticals in
 322       status, TacticAst.Then (loc, tactical, tacticals)
 323   | TacticAst.Tries (loc, tacticals) ->
 324       let status, tacticals = disambiguate_tacticals status tacticals in
 325       status, TacticAst.Tries (loc, tacticals)
 326   | TacticAst.Try (loc, tactical) ->
 327       let status, tactical = disambiguate_tactical status tactical in
 328       status, TacticAst.Try (loc, tactical)
 329   | (TacticAst.IdTac _ | TacticAst.Fail _) as tac ->
 330       status, tac
 331
 332 and disambiguate_tacticals status tacticals =
 333   let status, tacticals =
 334     List.fold_left
 335       (fun (status, tacticals) tactical ->
 336         let status, tac = disambiguate_tactical status tactical in
 337         status, tac :: tacticals)
 338       (status, [])
 339       tacticals
 340   in
 341   let tacticals = List.rev tacticals in
 342   status, tacticals
 343
 344 let disambiguate_inddef status params indTypes =
 345   let add_pi binders t =
 346     List.fold_right
 347       (fun (name, ast) acc ->
 348         CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc))
 349       binders t
 350   in
 351   let ind_binders =
 352     List.map (fun (name, _, typ, _) -> (name, add_pi params typ)) indTypes
 353   in
 354   let binders = ind_binders @ params in
 355   let asts = ref [] in
 356   let add_ast ast = asts := ast :: !asts in
 357   let paramsno = List.length params in
 358   let indbindersno = List.length ind_binders in
 359   List.iter
 360     (fun (name, _, typ, constructors) ->
 361       add_ast (add_pi params typ);
 362       List.iter (fun (_, ast) -> add_ast (add_pi binders ast)) constructors)
 363     indTypes;
 364   let status, terms = disambiguate_terms status !asts in
 365   let terms = ref (List.rev terms) in
 366   let get_term () =
 367     match !terms with [] -> assert false | hd :: tl -> terms := tl; hd
 368   in
 369   let uri =
 370     match indTypes with
 371     | (name, _, _, _) :: _ -> MatitaMisc.qualify status name ^ ".ind"
 372     | _ -> assert false
 373   in
 374   let mutinds =
 375     let counter = ref 0 in
 376     List.map
 377       (fun _ ->
 378         incr counter;
 379         CicUtil.term_of_uri (sprintf "%s#xpointer(1/%d)" uri !counter))
 380       indTypes
 381   in
 382   let subst_mutinds = List.fold_right CicSubstitution.subst mutinds in
 383   let cicIndTypes =
 384     List.fold_left
 385       (fun acc (name, inductive, typ, constructors) ->
 386         let cicTyp = get_term () in
 387         let cicConstructors =
 388           List.fold_left
 389             (fun acc (name, _) ->
 390               let typ =
 391                 subst_mutinds (CicUtil.strip_prods indbindersno (get_term ()))
 392               in
 393               (name, typ) :: acc)
 394             [] constructors
 395         in
 396         (name, inductive, cicTyp, List.rev cicConstructors) :: acc)
 397       [] indTypes
 398   in
 399   let cicIndTypes = List.rev cicIndTypes in
 400   status, (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno))
 401
 402 let disambiguate_command status = function
 403   | TacticAst.Inductive (loc, params, types) ->
 404       let (status, (uri, (ind_types, vars, paramsno))) =
 405         disambiguate_inddef status params types
 406       in
 407       let rec mk_list = function
 408         | 0 -> []
 409         | n -> ("", Cic.Rel ~-117) :: mk_list (n-1)
 410       in
 411       (* once we've built the cic inductive types we no longer need terms
 412          corresponding to parameters, but we need the leftno, and we encode
 413          it as the length of dummy_params
 414       *)
 415       let dummy_params = mk_list paramsno in
 416       status, TacticAst.Inductive (loc, dummy_params, ind_types)
 417   | TacticAst.Theorem (loc, thm_flavour, name, ty, body) ->
 418       let status, ty = disambiguate_term status ty in
 419       let status, body =
 420         match body with
 421         | None -> status, None
 422         | Some body ->
 423             let status, body = disambiguate_term status body in
 424             status, Some body
 425       in
 426       status, TacticAst.Theorem (loc, thm_flavour, name, ty, body)
 427   | TacticAst.Coercion (loc, term) -> assert false  (** TODO *)
 428   | (TacticAst.Set _ | TacticAst.Qed _) as cmd ->
 429       status, cmd
 430   | TacticAst.Alias _ as x -> status, x
 431
 432 let disambiguate_statement status statement =
 433   match statement with
 434   | TacticAst.Tactical (loc, tac) ->
 435       let status, tac = disambiguate_tactical status tac in
 436       status, (TacticAst.Tactical (loc, tac))
 437   | TacticAst.Command (loc, cmd) ->
 438       let status, cmd = disambiguate_command status cmd in
 439       status, (TacticAst.Command (loc, cmd))
 440   | TacticAst.Macro (_, mac) ->
 441       command_error
 442         (sprintf ("The engine is not allowed to disambiguate any macro, "^^
 443                  "in particular %s") (TacticAstPp.pp_macro_ast mac))
 444
 445 let eval_ast status ast =
 446   let status,st = disambiguate_statement status ast in
 447   (* this disambiguation step should be deferred to support tacticals *)
 448   eval status st
 449
 450 let eval_from_stream status str =
 451   let st = CicTextualParser2.parse_statement str in
 452   eval_ast status st
 453
 454 let eval_string status str =
 455   eval_from_stream status (Stream.of_string str)
 456
 457 let default_options () =
 458   let options =
 459     StringMap.add "baseuri"
 460       (String
 461         (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner"))
 462       no_options
 463   in
 464   let options =
 465     StringMap.add "basedir"
 466       (String (Helm_registry.get "matita.basedir" ))
 467       options
 468   in
 469   options
 470
 471 let initial_status =
 472   lazy {
 473     aliases = DisambiguateTypes.empty_environment;
 474     proof_status = No_proof;
 475     options = default_options ();
 476     coercions = [];
 477     objects = [];
 478   }
 479