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