helm/matita/matitaEngine.ml

   1
   2 open Printf
   3 open MatitaTypes
   4
   5 let debug = true ;;
   6 let debug_print = if debug then prerr_endline else ignore ;;
   7
   8 (** create a ProofEngineTypes.mk_fresh_name_type function which uses given
   9   * names as long as they are available, then it fallbacks to name generation
  10   * using FreshNamesGenerator module *)
  11 let namer_of names =
  12   let len = List.length names in
  13   let count = ref 0 in
  14   fun metasenv context name ~typ ->
  15     if !count < len then begin
  16       let name = Cic.Name (List.nth names !count) in
  17       incr count;
  18       name
  19     end else
  20       FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ
  21
  22 let tactic_of_ast = function
  23   | TacticAst.Intros (_, None, names) ->
  24       (* TODO Zack implement intros length *)
  25       PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) ()
  26   | TacticAst.Intros (_, Some num, names) ->
  27       (* TODO Zack implement intros length *)
  28       PrimitiveTactics.intros_tac ~howmany:num ~mk_fresh_name_callback:(namer_of names) ()
  29   | TacticAst.Reflexivity _ -> Tactics.reflexivity
  30   | TacticAst.Assumption _ -> Tactics.assumption
  31   | TacticAst.Contradiction _ -> Tactics.contradiction
  32   | TacticAst.Exists _ -> Tactics.exists
  33   | TacticAst.Fourier _ -> Tactics.fourier
  34   | TacticAst.Goal (_, n) -> Tactics.set_goal n
  35   | TacticAst.Left _ -> Tactics.left
  36   | TacticAst.Right _ -> Tactics.right
  37   | TacticAst.Ring _ -> Tactics.ring
  38   | TacticAst.Split _ -> Tactics.split
  39   | TacticAst.Symmetry _ -> Tactics.symmetry
  40   | TacticAst.Transitivity (_, term) -> Tactics.transitivity term
  41   | TacticAst.Apply (_, term) -> Tactics.apply term
  42   | TacticAst.Absurd (_, term) -> Tactics.absurd term
  43   | TacticAst.Exact (_, term) -> Tactics.exact term
  44   | TacticAst.Cut (_, term) -> Tactics.cut term
  45   | TacticAst.Elim (_, term, _) ->
  46       (* TODO Zack implement "using" argument *)
  47       (* old: Tactics.elim_intros_simpl term *)
  48       Tactics.elim_intros term
  49   | TacticAst.ElimType (_, term) -> Tactics.elim_type term
  50   | TacticAst.Replace (_, what, with_what) -> Tactics.replace ~what ~with_what
  51   | TacticAst.Auto (_,num) ->
  52       AutoTactic.auto_tac ~num ~dbd:(MatitaDb.instance ())
  53   | TacticAst.Change (_, what, with_what, _) -> Tactics.change ~what ~with_what
  54 (*
  55   (* TODO Zack a lot more of tactics to be implemented here ... *)
  56   | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
  57   | TacticAst.Change of 'term * 'term * 'ident option
  58   | TacticAst.Decompose of 'ident * 'ident list
  59   | TacticAst.Discriminate of 'ident
  60   | TacticAst.Fold of reduction_kind * 'term
  61   | TacticAst.Injection of 'ident
  62   | TacticAst.Replace_pattern of 'term pattern * 'term
  63 *)
  64   | TacticAst.LetIn (loc,term,name) ->
  65       Tactics.letin ~term ~mk_fresh_name_callback:(namer_of [name])
  66   | TacticAst.ReduceAt (_,reduction_kind,ident,path) ->
  67       ProofEngineTypes.mk_tactic
  68       (fun (((_,metasenv,_,_),goal) as status) ->
  69          let metano,context,ty = CicUtil.lookup_meta goal metasenv in
  70          let where, also_in_hypotheses =
  71            if ident = "goal" then
  72              ty, false
  73            else
  74              let hyp =
  75                try
  76                  List.find (function
  77                    | Some (Cic.Name name,entry) when name = ident -> true
  78                    | _ -> false)
  79                  context
  80                with
  81                  Not_found -> raise (ProofEngineTypes.Fail (ident ^ " is not an hypothesis"))
  82              in
  83              (match hyp with
  84              | Some (_, Cic.Decl term) -> term
  85              | Some (_, Cic.Def (term,ty)) -> term
  86              | None -> assert false),true
  87          in
  88          let pointers = CicUtil.select ~term:where ~context:path in
  89           (match reduction_kind with
  90           | `Normalize ->
  91               ProofEngineTypes.apply_tactic
  92                 (Tactics.normalize ~also_in_hypotheses ~terms:(Some pointers))
  93                 status
  94           | `Reduce ->
  95               ProofEngineTypes.apply_tactic
  96                 (Tactics.reduce ~also_in_hypotheses ~terms:(Some pointers))
  97                 status
  98           | `Simpl ->
  99               ProofEngineTypes.apply_tactic
 100                 (Tactics.simpl ~also_in_hypotheses ~terms:(Some pointers))
 101                 status
 102           | `Whd ->
 103               ProofEngineTypes.apply_tactic
 104                 (Tactics.whd ~also_in_hypotheses ~terms:(Some pointers))
 105                 status))
 106   | TacticAst.Reduce (_,reduction_kind,opts) ->
 107       let terms, also_in_hypotheses =
 108         match opts with
 109         | Some (l,`Goal) -> Some l, false
 110         | Some (l,`Everywhere) -> Some l, true
 111         | None -> None, false
 112       in
 113       (match reduction_kind with
 114       | `Normalize -> Tactics.normalize ~also_in_hypotheses ~terms
 115       | `Reduce -> Tactics.reduce ~also_in_hypotheses ~terms
 116       | `Simpl -> Tactics.simpl ~also_in_hypotheses ~terms
 117       | `Whd -> Tactics.whd ~also_in_hypotheses ~terms)
 118   | TacticAst.Rewrite (_,dir,t,ident) ->
 119       if dir = `Left then
 120         EqualityTactics.rewrite_tac ~term:t
 121       else
 122         EqualityTactics.rewrite_back_tac ~term:t
 123   | _ -> assert false
 124
 125 let eval_tactical status tac =
 126   let apply_tactic tactic =
 127     let (proof, goals) =
 128       ProofEngineTypes.apply_tactic tactic (MatitaMisc.get_proof_status status)
 129     in
 130     let new_status =
 131       match goals with
 132       | [] ->
 133           let (_,metasenv,_,_) = proof in
 134           (match metasenv with
 135           | [] -> Proof proof
 136           | (ng,_,_)::_ -> Incomplete_proof (proof,ng))
 137       | ng::_ -> Incomplete_proof (proof, ng)
 138     in
 139     { status with proof_status = new_status }
 140   in
 141   let rec tactical_of_ast = function
 142     | TacticAst.Tactic (loc, tactic) -> tactic_of_ast tactic
 143     | TacticAst.Fail loc -> Tacticals.fail
 144     | TacticAst.Do (loc, num, tactical) ->
 145         Tacticals.do_tactic num (tactical_of_ast tactical)
 146     | TacticAst.IdTac loc -> Tacticals.id_tac
 147     | TacticAst.Repeat (loc, tactical) ->
 148         Tacticals.repeat_tactic (tactical_of_ast tactical)
 149     | TacticAst.Seq (loc, tacticals) ->  (* tac1; tac2; ... *)
 150         Tacticals.seq (List.map tactical_of_ast tacticals)
 151     | TacticAst.Then (loc, tactical, tacticals) ->  (* tac; [ tac1 | ... ] *)
 152         Tacticals.thens (tactical_of_ast tactical)
 153           (List.map tactical_of_ast tacticals)
 154     | TacticAst.Tries (loc, tacticals) ->
 155         Tacticals.try_tactics
 156           (List.map (fun t -> "", tactical_of_ast t) tacticals)
 157     | TacticAst.Try (loc, tactical) ->
 158         Tacticals.try_tactic (tactical_of_ast tactical)
 159   in
 160   apply_tactic (tactical_of_ast tac)
 161
 162 (** given a uri and a type list (the contructors types) builds a list of pairs
 163  *  (name,uri) that is used to generate authomatic aliases **)
 164 let extract_alias types uri =
 165   fst(List.fold_left (
 166     fun (acc,i) (name, _, _, cl) ->
 167       ((name, UriManager.string_of_uriref (uri,[i]))
 168       ::
 169       (fst(List.fold_left (
 170         fun (acc,j) (name,_) ->
 171           (((name,UriManager.string_of_uriref (uri,[i;j])) :: acc) , j+1)
 172         ) (acc,1) cl))),i+1
 173   ) ([],0) types)
 174
 175 (** adds a (name,uri) list l to a disambiguation environment e **)
 176 let env_of_list l e =
 177   let module DT = DisambiguateTypes in
 178   let module DTE = DisambiguateTypes.Environment in
 179   List.fold_left (
 180     fun e (name,uri) ->
 181       DTE.add
 182        (DT.Id name)
 183        (uri,fun _ _ _ -> CicUtil.term_of_uri uri)
 184        e
 185   ) e l
 186
 187 let eval_coercion status coercion =
 188   let coer_uri,coer_ty =
 189     match coercion with
 190     | Cic.Const (uri,_)
 191     | Cic.Var (uri,_) ->
 192         let o,_ =
 193           CicEnvironment.get_obj CicUniv.empty_ugraph uri
 194         in
 195         (match o with
 196         | Cic.Constant (_,_,ty,_,_)
 197         | Cic.Variable (_,_,ty,_,_) ->
 198             uri,ty
 199         | _ -> assert false)
 200     | Cic.MutConstruct (uri,t,c,_) ->
 201         let o,_ =
 202           CicEnvironment.get_obj CicUniv.empty_ugraph uri
 203         in
 204         (match o with
 205         | Cic.InductiveDefinition (l,_,_,_) ->
 206             let (_,_,_,cl) = List.nth l t in
 207             let (_,cty) = List.nth cl c in
 208               uri,cty
 209         | _ -> assert false)
 210     | _ -> assert false
 211   in
 212   (* we have to get the source and the tgt type uri
 213    * in Coq syntax we have already their names, but
 214    * since we don't support Funclass and similar I think
 215    * all the coercion should be of the form
 216    * (A:?)(B:?)T1->T2
 217    * So we should be able to extract them from the coercion type
 218    *)
 219   let extract_last_two_p ty =
 220     let rec aux = function
 221       | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) -> aux (Cic.Prod(n,t1,t2))
 222       | Cic.Prod( _, src, tgt) -> src, tgt
 223       | _ -> assert false
 224     in
 225     aux ty
 226   in
 227   let ty_src,ty_tgt = extract_last_two_p coer_ty in
 228   let src_uri = UriManager.uri_of_string (CicUtil.uri_of_term ty_src) in
 229   let tgt_uri = UriManager.uri_of_string (CicUtil.uri_of_term ty_tgt) in
 230   let new_coercions =
 231     (* also adds them to the Db *)
 232     CoercGraph.close_coercion_graph src_uri tgt_uri coer_uri
 233   in
 234   let status =
 235     List.fold_left (
 236       fun s (uri,o,ugraph) ->
 237         match o with
 238         | Cic.Constant (_,Some body, ty, params, attrs) ->
 239             MatitaSync.add_constant ~uri ~body ~ty ~ugraph ~params ~attrs status
 240         | _ -> assert false
 241     ) status new_coercions
 242   in
 243   {status with proof_status = No_proof}
 244
 245 let eval_command status cmd =
 246   match cmd with
 247   | TacticAst.Set (loc, name, value) -> set_option status name value
 248   | TacticAst.Qed loc ->
 249       let uri, metasenv, bo, ty =
 250         match status.proof_status with
 251         | Proof (Some uri, metasenv, body, ty) ->
 252             uri, metasenv, body, ty
 253         | Proof (None, metasenv, body, ty) ->
 254             command_error
 255               ("Someone allows to start a thm without giving the "^
 256                "name/uri. This should be fixed!")
 257         | _-> command_error "You can't qed an uncomplete theorem"
 258       in
 259       let suri = UriManager.string_of_uri uri in
 260       if metasenv <> [] then
 261         command_error "Proof not completed! metasenv is not empty!";
 262       let proved_ty,ugraph =
 263         CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph
 264       in
 265       let b,ugraph =
 266         CicReduction.are_convertible [] proved_ty ty ugraph
 267       in
 268       if not b then
 269         command_error
 270           ("The type of your proof is not convertible with the "^
 271           "type you've declared!");
 272       MatitaLog.message (sprintf "%s defined" suri);
 273       let status = MatitaSync.add_constant ~uri ~body:bo ~ty ~ugraph status in
 274       let status =
 275         let name = UriManager.name_of_uri uri in
 276         let new_env = env_of_list [(name,suri)] status.aliases in
 277         {status with aliases = new_env }
 278       in
 279       {status with proof_status = No_proof }
 280   | TacticAst.Inductive (loc, dummy_params, types) ->
 281       (* dummy_params are not real params, it is a list of nothing, and the only
 282        * semantic content is the len, that is leftno (note: leftno and pamaters
 283        * have nothing in common).
 284        *)
 285       let suri =
 286         match types with
 287         | (name, _, _, _) :: tl -> MatitaMisc.qualify status name ^ ".ind"
 288         | _ -> assert false
 289       in
 290       let uri = UriManager.uri_of_string suri in
 291       let leftno = List.length dummy_params in
 292       let obj = Cic.InductiveDefinition (types, [], leftno, []) in
 293       let ugraph =
 294         CicTypeChecker.typecheck_mutual_inductive_defs uri
 295           (types, [], leftno) CicUniv.empty_ugraph
 296       in
 297       let status =
 298         MatitaSync.add_inductive_def
 299           ~uri ~types ~params:[] ~leftno ~ugraph status
 300       in
 301       (* aliases for the constructors and types *)
 302       let aliases = env_of_list (extract_alias types uri) status.aliases in
 303       (* aliases for the eliminations principles *)
 304       let aliases =
 305         let base = String.sub suri 0 (String.length suri - 4)  in
 306         env_of_list
 307         (List.fold_left (
 308           fun acc suffix ->
 309             if List.exists (
 310               fun (uri,_) -> UriManager.string_of_uri uri = base ^ suffix
 311             ) status.objects then
 312               let u = base ^ suffix in
 313               (UriManager.name_of_uri (UriManager.uri_of_string u),u)::acc
 314             else
 315               acc
 316         ) [] ["_ind.con";"_rec.con";"_rec_t.con"]) aliases
 317       in
 318       let status = {status with proof_status = No_proof } in
 319       { status with aliases = aliases}
 320   | TacticAst.Theorem (loc, thm_flavour, Some name, ty, None) ->
 321       let uri =
 322         UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
 323       in
 324       let goalno = 1 in
 325       let metasenv, body =
 326         match status.proof_status with
 327         | Intermediate metasenv ->
 328             ((goalno, [], ty) :: metasenv) , Cic.Meta (goalno,[])
 329         | _-> assert false
 330       in
 331       let initial_proof = (Some uri, metasenv, body, ty) in
 332       { status with proof_status = Incomplete_proof (initial_proof,goalno)}
 333   | TacticAst.Theorem (loc, thm_flavour, Some name, ty, Some body) ->
 334       let uri =
 335         UriManager.uri_of_string (MatitaMisc.qualify status name ^ ".con")
 336       in
 337       let metasenv = MatitaMisc.get_proof_metasenv status in
 338       debug_print ("XXXXXXXXXX" ^ CicPp.ppterm body);
 339       let (body_type, ugraph) =
 340         CicTypeChecker.type_of_aux' metasenv [] body CicUniv.empty_ugraph
 341       in
 342       let (subst, metasenv, ugraph) =
 343         CicUnification.fo_unif metasenv [] body_type ty ugraph
 344       in
 345       if metasenv <> [] then
 346         command_error (
 347           "metasenv not empty while giving a definition with body: " ^
 348           CicMetaSubst.ppmetasenv metasenv []) ;
 349       let body = CicMetaSubst.apply_subst subst body in
 350       let ty = CicMetaSubst.apply_subst subst ty in
 351       let status = MatitaSync.add_constant ~uri ~body ~ty ~ugraph status in
 352       let status =
 353         let suri = UriManager.string_of_uri uri in
 354         let new_env = env_of_list [(name,suri)] status.aliases in
 355         {status with aliases = new_env }
 356       in
 357       {status with proof_status = No_proof}
 358   | TacticAst.Theorem (_, _, None, _, _) ->
 359       command_error "The grammar should avoid having unnamed theorems!"
 360   | TacticAst.Coercion (loc, coercion) ->
 361       eval_coercion status coercion
 362   | TacticAst.Alias (loc, spec) ->
 363       match spec with
 364       | TacticAst.Ident_alias (id,uri) ->
 365           {status with aliases =
 366             DisambiguateTypes.Environment.add
 367               (DisambiguateTypes.Id id)
 368               ("boh?",(fun _ _ _ -> CicUtil.term_of_uri uri))
 369               status.aliases }
 370       | TacticAst.Symbol_alias (symb, instance, desc) ->
 371           {status with aliases =
 372             DisambiguateTypes.Environment.add
 373               (DisambiguateTypes.Symbol (symb,instance))
 374               (DisambiguateChoices.lookup_symbol_by_dsc symb desc)
 375               status.aliases }
 376       | TacticAst.Number_alias (instance,desc) ->
 377           {status with aliases =
 378             DisambiguateTypes.Environment.add
 379               (DisambiguateTypes.Num instance)
 380               (DisambiguateChoices.lookup_num_by_dsc desc) status.aliases }
 381
 382 let eval_executable status ex =
 383   match ex with
 384   | TacticAst.Tactical (_, tac) -> eval_tactical status tac
 385   | TacticAst.Command (_, cmd) -> eval_command status cmd
 386   | TacticAst.Macro (_, mac) ->
 387       command_error (sprintf "The macro %s can't be in a script"
 388         (TacticAstPp.pp_macro_cic mac))
 389
 390 let eval_comment status c = status
 391
 392 let eval status st =
 393   match st with
 394   | TacticAst.Executable (_,ex) -> eval_executable status ex
 395   | TacticAst.Comment (_,c) -> eval_comment status c
 396
 397 let disambiguate_term status term =
 398   let (aliases, metasenv, cic, _) =
 399     match
 400       MatitaDisambiguator.disambiguate_term ~dbd:(MatitaDb.instance ())
 401         ~aliases:(status.aliases) ~context:(MatitaMisc.get_proof_context status)
 402         ~metasenv:(MatitaMisc.get_proof_metasenv status) term
 403     with
 404     | [x] -> x
 405     | _ -> assert false
 406   in
 407   let proof_status =
 408     match status.proof_status with
 409     | No_proof -> Intermediate metasenv
 410     | Incomplete_proof ((uri, _, proof, ty), goal) ->
 411         Incomplete_proof ((uri, metasenv, proof, ty), goal)
 412     | Intermediate _ -> Intermediate metasenv
 413     | Proof _ -> assert false
 414   in
 415   let status =
 416     { status with
 417         aliases = aliases;
 418         proof_status = proof_status }
 419   in
 420   status, cic
 421
 422 let disambiguate_terms status terms =
 423   let term = CicAst.pack terms in
 424   let status, term = disambiguate_term status term in
 425   status, CicUtil.unpack term
 426
 427 let disambiguate_tactic status = function
 428   | TacticAst.Transitivity (loc, term) ->
 429       let status, cic = disambiguate_term status term in
 430       status, TacticAst.Transitivity (loc, cic)
 431   | TacticAst.Apply (loc, term) ->
 432       let status, cic = disambiguate_term status term in
 433       status, TacticAst.Apply (loc, cic)
 434   | TacticAst.Absurd (loc, term) ->
 435       let status, cic = disambiguate_term status term in
 436       status, TacticAst.Absurd (loc, cic)
 437   | TacticAst.Exact (loc, term) ->
 438       let status, cic = disambiguate_term status term in
 439       status, TacticAst.Exact (loc, cic)
 440   | TacticAst.Cut (loc, term) ->
 441       let status, cic = disambiguate_term status term in
 442       status, TacticAst.Cut (loc, cic)
 443   | TacticAst.Elim (loc, term, Some term') ->
 444       let status, cic1 = disambiguate_term status term in
 445       let status, cic2 = disambiguate_term status term' in
 446       status, TacticAst.Elim (loc, cic1, Some cic2)
 447   | TacticAst.Elim (loc, term, None) ->
 448       let status, cic = disambiguate_term status term in
 449       status, TacticAst.Elim (loc, cic, None)
 450   | TacticAst.ElimType (loc, term) ->
 451       let status, cic = disambiguate_term status term in
 452       status, TacticAst.ElimType (loc, cic)
 453   | TacticAst.Replace (loc, what, with_what) ->
 454       let status, cic1 = disambiguate_term status what in
 455       let status, cic2 = disambiguate_term status with_what in
 456       status, TacticAst.Replace (loc, cic1, cic2)
 457   | TacticAst.Change (loc, what, with_what, ident) ->
 458       let status, cic1 = disambiguate_term status what in
 459       let status, cic2 = disambiguate_term status with_what in
 460       status, TacticAst.Change (loc, cic1, cic2, ident)
 461 (*
 462   (* TODO Zack a lot more of tactics to be implemented here ... *)
 463   | TacticAst.Change_pattern of 'term pattern * 'term * 'ident option
 464   | TacticAst.Change of 'term * 'term * 'ident option
 465   | TacticAst.Decompose of 'ident * 'ident list
 466   | TacticAst.Discriminate of 'ident
 467   | TacticAst.Fold of reduction_kind * 'term
 468   | TacticAst.Injection of 'ident
 469   | TacticAst.Replace_pattern of 'term pattern * 'term
 470 *)
 471   | TacticAst.LetIn (loc,term,name) ->
 472       let status, term = disambiguate_term status term in
 473       status, TacticAst.LetIn (loc,term,name)
 474   | TacticAst.ReduceAt (loc, reduction_kind, ident, path) ->
 475       let path = Disambiguate.interpretate [] status.aliases path in
 476       status, TacticAst.ReduceAt(loc, reduction_kind, ident, path)
 477   | TacticAst.Reduce (loc, reduction_kind, opts) ->
 478       let status, opts =
 479         match opts with
 480         | None -> status, None
 481         | Some (l,pat) ->
 482             let status, l =
 483               List.fold_right (fun t (status,acc) ->
 484                 let status',t' = disambiguate_term status t in
 485                 status', t'::acc)
 486               l (status,[])
 487             in
 488             status, Some (l, pat)
 489       in
 490       status, TacticAst.Reduce (loc, reduction_kind, opts)
 491   | TacticAst.Rewrite (loc,dir,t,ident) ->
 492       let status, term = disambiguate_term status t in
 493       status, TacticAst.Rewrite (loc,dir,term,ident)
 494   | TacticAst.Intros (loc, num, names) ->
 495       status, TacticAst.Intros (loc, num, names)
 496   | TacticAst.Auto (loc,num) -> status, TacticAst.Auto (loc,num)
 497   | TacticAst.Reflexivity loc -> status, TacticAst.Reflexivity loc
 498   | TacticAst.Assumption loc -> status, TacticAst.Assumption loc
 499   | TacticAst.Contradiction loc -> status, TacticAst.Contradiction loc
 500   | TacticAst.Exists loc -> status, TacticAst.Exists loc
 501   | TacticAst.Fourier loc -> status, TacticAst.Fourier loc
 502   | TacticAst.Left loc -> status, TacticAst.Left loc
 503   | TacticAst.Right loc -> status, TacticAst.Right loc
 504   | TacticAst.Ring loc -> status, TacticAst.Ring loc
 505   | TacticAst.Split loc -> status, TacticAst.Split loc
 506   | TacticAst.Symmetry loc -> status, TacticAst.Symmetry loc
 507   | TacticAst.Goal (loc, g) -> status, TacticAst.Goal (loc, g)
 508   | x ->
 509       print_endline ("Not yet implemented:" ^ TacticAstPp.pp_tactic x);
 510       assert false
 511
 512 let rec disambiguate_tactical status = function
 513   | TacticAst.Tactic (loc, tactic) ->
 514       let status, tac = disambiguate_tactic status tactic in
 515       status, TacticAst.Tactic (loc, tac)
 516   | TacticAst.Do (loc, num, tactical) ->
 517       let status, tac = disambiguate_tactical status tactical in
 518       status, TacticAst.Do (loc, num, tac)
 519   | TacticAst.Repeat (loc, tactical) ->
 520       let status, tac = disambiguate_tactical status tactical in
 521       status, TacticAst.Repeat (loc, tac)
 522   | TacticAst.Seq (loc, tacticals) ->  (* tac1; tac2; ... *)
 523       let status, tacticals = disambiguate_tacticals status tacticals in
 524       let tacticals = List.rev tacticals in
 525       status, TacticAst.Seq (loc, tacticals)
 526   | TacticAst.Then (loc, tactical, tacticals) ->  (* tac; [ tac1 | ... ] *)
 527       let status, tactical = disambiguate_tactical status tactical in
 528       let status, tacticals = disambiguate_tacticals status tacticals in
 529       status, TacticAst.Then (loc, tactical, tacticals)
 530   | TacticAst.Tries (loc, tacticals) ->
 531       let status, tacticals = disambiguate_tacticals status tacticals in
 532       status, TacticAst.Tries (loc, tacticals)
 533   | TacticAst.Try (loc, tactical) ->
 534       let status, tactical = disambiguate_tactical status tactical in
 535       status, TacticAst.Try (loc, tactical)
 536   | (TacticAst.IdTac _ | TacticAst.Fail _) as tac ->
 537       status, tac
 538
 539 and disambiguate_tacticals status tacticals =
 540   let status, tacticals =
 541     List.fold_left
 542       (fun (status, tacticals) tactical ->
 543         let status, tac = disambiguate_tactical status tactical in
 544         status, tac :: tacticals)
 545       (status, [])
 546       tacticals
 547   in
 548   let tacticals = List.rev tacticals in
 549   status, tacticals
 550
 551 let disambiguate_inddef status params indTypes =
 552   let add_pi binders t =
 553     List.fold_right
 554       (fun (name, ast) acc ->
 555         CicAst.Binder (`Forall, (Cic.Name name, Some ast), acc))
 556       binders t
 557   in
 558   let ind_binders =
 559     List.map (fun (name, _, typ, _) -> (name, add_pi params typ)) indTypes
 560   in
 561   let binders = ind_binders @ params in
 562   let asts = ref [] in
 563   let add_ast ast = asts := ast :: !asts in
 564   let paramsno = List.length params in
 565   let indbindersno = List.length ind_binders in
 566   List.iter
 567     (fun (name, _, typ, constructors) ->
 568       add_ast (add_pi params typ);
 569       List.iter (fun (_, ast) -> add_ast (add_pi binders ast)) constructors)
 570     indTypes;
 571   let status, terms = disambiguate_terms status !asts in
 572   let terms = ref (List.rev terms) in
 573   let get_term () =
 574     match !terms with [] -> assert false | hd :: tl -> terms := tl; hd
 575   in
 576   let uri =
 577     match indTypes with
 578     | (name, _, _, _) :: _ -> MatitaMisc.qualify status name ^ ".ind"
 579     | _ -> assert false
 580   in
 581   let mutinds =
 582     let counter = ref 0 in
 583     List.map
 584       (fun _ ->
 585         incr counter;
 586         CicUtil.term_of_uri (sprintf "%s#xpointer(1/%d)" uri !counter))
 587       indTypes
 588   in
 589   let subst_mutinds = List.fold_right CicSubstitution.subst mutinds in
 590   let cicIndTypes =
 591     List.fold_left
 592       (fun acc (name, inductive, typ, constructors) ->
 593         let cicTyp = get_term () in
 594         let cicConstructors =
 595           List.fold_left
 596             (fun acc (name, _) ->
 597               let typ =
 598                 subst_mutinds (CicUtil.strip_prods indbindersno (get_term ()))
 599               in
 600               (name, typ) :: acc)
 601             [] constructors
 602         in
 603         (name, inductive, cicTyp, List.rev cicConstructors) :: acc)
 604       [] indTypes
 605   in
 606   let cicIndTypes = List.rev cicIndTypes in
 607   status, (UriManager.uri_of_string uri, (cicIndTypes, [], paramsno))
 608
 609 let disambiguate_command status = function
 610   | TacticAst.Inductive (loc, params, types) ->
 611       let (status, (uri, (ind_types, vars, paramsno))) =
 612         disambiguate_inddef status params types
 613       in
 614       let rec mk_list = function
 615         | 0 -> []
 616         | n -> ("", Cic.Rel ~-117) :: mk_list (n-1)
 617       in
 618       (* once we've built the cic inductive types we no longer need terms
 619          corresponding to parameters, but we need the leftno, and we encode
 620          it as the length of dummy_params
 621       *)
 622       let dummy_params = mk_list paramsno in
 623       status, TacticAst.Inductive (loc, dummy_params, ind_types)
 624   | TacticAst.Theorem (loc, thm_flavour, name, ty, body) ->
 625       let status, ty = disambiguate_term status ty in
 626       let status, body =
 627         match body with
 628         | None -> status, None
 629         | Some body ->
 630             let status, body = disambiguate_term status body in
 631             status, Some body
 632       in
 633       status, TacticAst.Theorem (loc, thm_flavour, name, ty, body)
 634   | TacticAst.Coercion (loc, term) ->
 635       let status, term = disambiguate_term status term in
 636       status, TacticAst.Coercion (loc,term)
 637   | (TacticAst.Set _ | TacticAst.Qed _) as cmd ->
 638       status, cmd
 639   | TacticAst.Alias _ as x -> status, x
 640
 641 let disambiguate_executable status ex =
 642   match ex with
 643   | TacticAst.Tactical (loc, tac) ->
 644       let status, tac = disambiguate_tactical status tac in
 645       status, (TacticAst.Tactical (loc, tac))
 646   | TacticAst.Command (loc, cmd) ->
 647       let status, cmd = disambiguate_command status cmd in
 648       status, (TacticAst.Command (loc, cmd))
 649   | TacticAst.Macro (_, mac) ->
 650       command_error
 651         (sprintf ("The engine is not allowed to disambiguate any macro, "^^
 652                  "in particular %s") (TacticAstPp.pp_macro_ast mac))
 653
 654 let disambiguate_comment status c =
 655   match c with
 656   | TacticAst.Note (loc,n) -> status, TacticAst.Note (loc,n)
 657   | TacticAst.Code (loc,ex) ->
 658         let status, ex = disambiguate_executable status ex in
 659         status, TacticAst.Code (loc,ex)
 660
 661 let disambiguate_statement status statement =
 662   match statement with
 663   | TacticAst.Comment (loc,c) ->
 664         let status, c = disambiguate_comment status c in
 665         status, TacticAst.Comment (loc,c)
 666   | TacticAst.Executable (loc,ex) ->
 667         let status, ex = disambiguate_executable status ex in
 668         status, TacticAst.Executable (loc,ex)
 669
 670 let eval_ast status ast =
 671   let status,st = disambiguate_statement status ast in
 672   (* this disambiguation step should be deferred to support tacticals *)
 673   eval status st
 674
 675 let eval_from_stream status str cb =
 676   let stl = CicTextualParser2.parse_statements str in
 677   List.fold_left
 678     (fun status ast -> cb status ast;eval_ast status ast) status
 679   stl
 680
 681 let eval_string status str =
 682   eval_from_stream status (Stream.of_string str) (fun _ _ -> ())
 683
 684 let default_options () =
 685   let options =
 686     StringMap.add "baseuri"
 687       (String
 688         (Helm_registry.get "matita.baseuri" ^ Helm_registry.get "matita.owner"))
 689       no_options
 690   in
 691   let options =
 692     StringMap.add "basedir"
 693       (String (Helm_registry.get "matita.basedir" ))
 694       options
 695   in
 696   options
 697
 698 let initial_status =
 699   lazy {
 700     aliases = DisambiguateTypes.empty_environment;
 701     proof_status = No_proof;
 702     options = default_options ();
 703     objects = [];
 704   }
 705