let left_params_no_of_inductive_type uri =
snd (get_types uri)
-let ast_of_acic0 term_info acic k =
+let ast_of_acic0 ~output_type term_info acic k =
let k = k term_info in
let id_to_uris = term_info.uri in
let register_uri id uri = Hashtbl.add id_to_uris id uri in
List.map2
(fun (name, ty) pat ->
incr j;
- let (capture_variables, rhs) = eat_branch lpsno ty pat in
- Ast.Pattern (name, Some (ctor_puri !j), capture_variables), rhs
+ let name,(capture_variables,rhs) =
+ match output_type with
+ `Term -> name, eat_branch lpsno ty pat
+ | `Pattern -> "_", ([], k pat)
+ in
+ Ast.Pattern (name, Some (ctor_puri !j), capture_variables), rhs
) constructors patterns
with Invalid_argument _ -> assert false
in
- idref id (Ast.Case (k te, Some case_indty, Some (k ty), patterns))
+ let indty =
+ match output_type with
+ `Pattern -> None
+ | `Term -> Some case_indty
+ in
+ idref id (Ast.Case (k te, indty, Some (k ty), patterns))
| Cic.AFix (id, no, funs) ->
let defs =
List.map
if args = [] then head
else Ast.Appl (head :: List.map instantiate_arg args)
-let rec ast_of_acic1 term_info annterm =
+let rec ast_of_acic1 ~output_type term_info annterm =
let id_to_uris = term_info.uri in
let register_uri id uri = Hashtbl.add id_to_uris id uri in
match (get_compiled32 ()) annterm with
- | None -> ast_of_acic0 term_info annterm ast_of_acic1
+ | None ->
+ ast_of_acic0 ~output_type term_info annterm (ast_of_acic1 ~output_type)
| Some (env, ctors, pid) ->
let idrefs =
List.map
ctors
in
let env' =
- List.map (fun (name, term) -> (name, ast_of_acic1 term_info term)) env
+ List.map
+ (fun (name, term) -> name, ast_of_acic1 ~output_type term_info term) env
in
let _, symbol, args, _ =
try
in
set_compiled32 (lazy (Acic2astMatcher.Matcher32.compiler t))
-let ast_of_acic id_to_sort annterm =
+let ast_of_acic ~output_type id_to_sort annterm =
debug_print (lazy ("ast_of_acic <- "
^ CicPp.ppterm (Deannotate.deannotate_term annterm)));
let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in
- let ast = ast_of_acic1 term_info annterm in
+ let ast = ast_of_acic1 ~output_type term_info annterm in
debug_print (lazy ("ast_of_acic -> " ^ CicNotationPp.pp_term ast));
ast, term_info.uri
(** {2 acic -> content} *)
val ast_of_acic:
+ output_type:[`Pattern|`Term] ->
(Cic.id, CicNotationPt.sort_kind) Hashtbl.t -> (* id -> sort *)
Cic.annterm -> (* acic *)
CicNotationPt.term (* ast *)
content2pres ?skip_initial_lambdas ?skip_thm_and_qed
(fun ?(prec=90) annterm ->
let ast, ids_to_uris =
- TermAcicContent.ast_of_acic ids_to_inner_sorts annterm
+ TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm
in
CicNotationPres.box_of_mpres
(CicNotationPres.render ids_to_uris ~prec
sequent2pres
(fun annterm ->
let ast, ids_to_uris =
- TermAcicContent.ast_of_acic ids_to_inner_sorts annterm
+ TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm
in
CicNotationPres.box_of_mpres
(CicNotationPres.render ids_to_uris
ids_to_inner_sorts:(Cic.id, Cic2acic.sort_kind) Hashtbl.t ->
Cic.annterm Content.conjecture ->
CicNotationPres.boxml_markup
-
if b1||b2 then true,Cic.Cast (te, ty)
else
not_found
- | Cic.Prod (name, s, t) ->
+ | Cic.Prod (_, s, t) ->
let b1,s = aux s in
let b2,t = aux t in
if b1||b2 then
- true, Cic.Prod (name, s, t)
+ true, Cic.Prod (Cic.Anonymous, s, t)
else
not_found
- | Cic.Lambda (name, s, t) ->
+ | Cic.Lambda (_, s, t) ->
let b1,s = aux s in
let b2,t = aux t in
if b1||b2 then
- true, Cic.Lambda (name, s, t)
+ true, Cic.Lambda (Cic.Anonymous, s, t)
else
not_found
- | Cic.LetIn (name, s, t) ->
+ | Cic.LetIn (_, s, t) ->
let b1,s = aux s in
let b2,t = aux t in
if b1||b2 then
- true, Cic.LetIn (name, s, t)
+ true, Cic.LetIn (Cic.Anonymous, s, t)
else
not_found
| Cic.Appl terms ->
in
let content_sequent = Acic2content.map_sequent asequent in
let pres_sequent =
- (Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent)
- in
+ Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent in
let xmlpres = mpres_document pres_sequent in
(Xml2Gdome.document_of_xml DomMisc.domImpl xmlpres,
unsh_sequent,
BoxPp.render_to_string ~map_unicode_to_tex
(function x::_ -> x | _ -> assert false) size pres_sequent
-let txt_of_cic_sequent_conclusion ~map_unicode_to_tex size metasenv sequent =
+let txt_of_cic_sequent_conclusion ~map_unicode_to_tex ~output_type size
+ metasenv sequent =
let _,(asequent,_,_,ids_to_inner_sorts,_) =
Cic2acic.asequent_of_sequent metasenv sequent
in
let _,_,_,t = Acic2content.map_sequent asequent in
- let t, ids_to_uris = TermAcicContent.ast_of_acic ids_to_inner_sorts t in
+ let t, ids_to_uris =
+ TermAcicContent.ast_of_acic ~output_type ids_to_inner_sorts t in
let t = TermContentPres.pp_ast t in
let t = CicNotationPres.render ids_to_uris t in
BoxPp.render_to_string ~map_unicode_to_tex
(function x::_ -> x | _ -> assert false) size t
let txt_of_cic_term ~map_unicode_to_tex size metasenv context t =
- let fake_sequent = (-1,context,t) in
- txt_of_cic_sequent_conclusion ~map_unicode_to_tex size metasenv fake_sequent
+ let fake_sequent = (-1,context,t) in
+ txt_of_cic_sequent_conclusion ~map_unicode_to_tex ~output_type:`Term size
+ metasenv fake_sequent
;;
ignore (
let term2pres ~map_unicode_to_tex n ids_to_inner_sorts annterm =
let ast, ids_to_uris =
- TermAcicContent.ast_of_acic ids_to_inner_sorts annterm
- in
+ TermAcicContent.ast_of_acic ~output_type:`Term ids_to_inner_sorts annterm in
let bobj =
CicNotationPres.box_of_mpres (
CicNotationPres.render ~prec:90 ids_to_uris
- (TermContentPres.pp_ast ast)
- )
- in
+ (TermContentPres.pp_ast ast)) in
let render = function _::x::_ -> x | _ -> assert false in
let mpres = CicNotationPres.mpres_of_box bobj in
let s = BoxPp.render_to_string ~map_unicode_to_tex render n mpres in
val txt_of_cic_term:
map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.context -> Cic.term ->
- string
+ string
val txt_of_cic_sequent:
- map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.conjecture ->
- string
+ map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.conjecture -> string
val txt_of_cic_sequent_conclusion:
- map_unicode_to_tex:bool -> int -> Cic.metasenv -> Cic.conjecture ->
- string
+ map_unicode_to_tex:bool -> output_type:[`Pattern | `Term] -> int ->
+ Cic.metasenv -> Cic.conjecture -> string
(* columns, rendering style, name prefix, object *)
val txt_of_cic_object:
match self#get_term_by_id cic_info id with
| SelTerm (t, father_hyp) ->
let sequent = self#sequent_of_id ~paste_kind:`Pattern id in
- let text = self#string_of_cic_sequent sequent in
+ let text = self#string_of_cic_sequent ~output_type:`Pattern sequent in
(match father_hyp with
| None -> None, [], Some text
| Some hyp_name -> None, [ hyp_name, text ], None)
match self#get_term_by_id cic_info id with
| SelTerm (t, father_hyp) ->
let sequent = self#sequent_of_id ~paste_kind:`Term id in
- let text = self#string_of_cic_sequent sequent in
+ let text = self#string_of_cic_sequent ~output_type:`Term sequent in
text
| SelHyp (hyp_name, _ctxt) -> hyp_name
| `Term -> self#tactic_text_of_node node
else string_of_dom_node node
- method private string_of_cic_sequent cic_sequent =
+ method private string_of_cic_sequent ~output_type cic_sequent =
let script = MatitaScript.current () in
let metasenv =
if script#onGoingProof () then script#proofMetasenv else [] in
- (*
- let _, (acic_sequent, _, _, ids_to_inner_sorts, _) =
- Cic2acic.asequent_of_sequent metasenv cic_sequent in
- let _, _, _, annterm = acic_sequent in
- let ast, ids_to_uris =
- TermAcicContent.ast_of_acic ids_to_inner_sorts annterm in
- let pped_ast = TermContentPres.pp_ast ast in
- let markup = CicNotationPres.render ids_to_uris pped_ast in
- BoxPp.render_to_string text_width markup
- *)
let map_unicode_to_tex =
Helm_registry.get_bool "matita.paste_unicode_as_tex" in
ApplyTransformation.txt_of_cic_sequent_conclusion ~map_unicode_to_tex
- text_width metasenv cic_sequent
+ ~output_type text_width metasenv cic_sequent
method private pattern_of term context unsh_sequent =
let context_len = List.length context in
projects / helm.git / commitdiff