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