1 (* Copyright (C) 2005, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
26 (* $Id: termAcicContent.ml 9304 2008-12-05 23:12:39Z sacerdot $ *)
30 module Ast = CicNotationPt
33 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
38 type interpretation_id = int
41 { sort: (Cic.id, Ast.sort_kind) Hashtbl.t;
42 uri: (Cic.id, UriManager.uri) Hashtbl.t;
46 let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
48 | Cic.InductiveDefinition (l,_,leftno,_) -> l, leftno
52 let idref register_ref =
56 let id = "i" ^ string_of_int !id in
57 (match reference with None -> () | Some r -> register_ref id r);
58 Ast.AttributedTerm (`IdRef id, t)
62 let name = NUri.name_of_uri u in
63 assert(String.length name > String.length "Type");
64 String.sub name 4 (String.length name - 4)
68 let is_nat_URI = NUri.eq (NUri.uri_of_string
69 "cic:/matita/ng/arithmetics/nat/nat.ind") in
70 let is_zero = function
71 | NCic.Const (NReference.Ref (uri, NReference.Con (0, 1, 0))) when
72 is_nat_URI uri -> true
75 let is_succ = function
76 | NCic.Const (NReference.Ref (uri, NReference.Con (0, 2, 0))) when
77 is_nat_URI uri -> true
80 let rec aux acc = function
81 | NCic.Appl [he ; tl] when is_succ he -> aux (acc + 1) tl
82 | t when is_zero t -> Some acc
87 (* CODICE c&p da NCicPp *)
88 let nast_of_cic0 status
90 ?reference:NReference.reference -> CicNotationPt.term -> CicNotationPt.term)
91 ~output_type ~metasenv ~subst k ~context =
95 let name,_ = List.nth context (n-1) in
96 let name = if name = "_" then "__"^string_of_int n else name in
97 idref (Ast.Ident (name,None))
98 with Failure "nth" | Invalid_argument "List.nth" ->
99 idref (Ast.Ident ("-" ^ string_of_int (n - List.length context),None)))
100 | NCic.Const r -> idref ~reference:r (Ast.Ident (NCicPp.r2s true r, None))
101 | NCic.Meta (n,lc) when List.mem_assoc n subst ->
102 let _,_,t,_ = List.assoc n subst in
103 k ~context (NCicSubstitution.subst_meta lc t)
104 | NCic.Meta (n,(s,l)) ->
105 (* CSC: qua non dovremmo espandere *)
106 let l = NCicUtils.expand_local_context l in
108 (n, List.map (fun x -> Some (k ~context (NCicSubstitution.lift s x))) l))
109 | NCic.Sort NCic.Prop -> idref (Ast.Sort `Prop)
110 | NCic.Sort NCic.Type [] -> idref (Ast.Sort `Set)
111 | NCic.Sort NCic.Type ((`Type,u)::_) ->
112 idref(Ast.Sort (`NType (level_of_uri u)))
113 | NCic.Sort NCic.Type ((`CProp,u)::_) ->
114 idref(Ast.Sort (`NCProp (level_of_uri u)))
115 | NCic.Sort NCic.Type ((`Succ,u)::_) ->
116 idref(Ast.Sort (`NType (level_of_uri u ^ "+1")))
117 | NCic.Implicit `Hole -> idref (Ast.UserInput)
118 | NCic.Implicit `Vector -> idref (Ast.Implicit `Vector)
119 | NCic.Implicit _ -> idref (Ast.Implicit `JustOne)
120 | NCic.Prod (n,s,t) ->
121 let n = if n.[0] = '_' then "_" else n in
122 let binder_kind = `Forall in
123 idref (Ast.Binder (binder_kind, (Ast.Ident (n,None), Some (k ~context s)),
124 k ~context:((n,NCic.Decl s)::context) t))
125 | NCic.Lambda (n,s,t) ->
126 idref (Ast.Binder (`Lambda,(Ast.Ident (n,None), Some (k ~context s)),
127 k ~context:((n,NCic.Decl s)::context) t))
128 | NCic.LetIn (n,s,ty,NCic.Rel 1) ->
129 idref (Ast.Cast (k ~context ty, k ~context s))
130 | NCic.LetIn (n,s,ty,t) ->
131 idref (Ast.LetIn ((Ast.Ident (n,None), Some (k ~context s)), k ~context
132 ty, k ~context:((n,NCic.Decl s)::context) t))
133 | NCic.Appl (NCic.Meta (n,lc) :: args) when List.mem_assoc n subst ->
134 let _,_,t,_ = List.assoc n subst in
135 let hd = NCicSubstitution.subst_meta lc t in
137 (NCicReduction.head_beta_reduce ~upto:(List.length args)
139 | NCic.Appl l -> NCic.Appl (l@args)
140 | _ -> NCic.Appl (hd :: args)))
141 | NCic.Appl args as t ->
142 (match destroy_nat t with
143 | Some n -> idref (Ast.Num (string_of_int n, -1))
146 if not !Acic2content.hide_coercions then args
149 NCicCoercion.match_coercion status ~metasenv ~context ~subst t
152 | Some (_,sats,cpos) ->
153 (* CSC: sats e' il numero di pi, ma non so cosa farmene! voglio il numero di
154 argomenti da saltare, come prima! *)
155 if cpos < List.length args - 1 then
156 List.nth args (cpos + 1) ::
157 try snd (HExtlib.split_nth (cpos+sats+2) args)
163 [arg] -> idref (k ~context arg)
164 | _ -> idref (Ast.Appl (List.map (k ~context) args))))
165 | NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) ->
166 let name = NUri.name_of_uri uri in
168 let uri_str = UriManager.string_of_uri uri in
169 let puri_str = sprintf "%s#xpointer(1/%d)" uri_str (typeno+1) in
171 UriManager.uri_of_string
172 (sprintf "%s#xpointer(1/%d/%d)" uri_str (typeno+1) j)
176 name, None(*CSC Some (UriManager.uri_of_string puri_str)*) in
177 let constructors, leftno =
178 let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys r in
179 let _,_,_,cl = List.nth tys n in
182 let rec eat_branch n ctx ty pat =
184 | NCic.Prod (name, s, t), _ when n > 0 ->
185 eat_branch (pred n) ctx t pat
186 | NCic.Prod (_, _, t), NCic.Lambda (name, s, t') ->
187 let cv, rhs = eat_branch 0 ((name,NCic.Decl s)::ctx) t t' in
188 (Ast.Ident (name,None), Some (k ~context:ctx s)) :: cv, rhs
189 | _, _ -> [], k ~context:ctx pat
195 (fun (_, name, ty) pat ->
197 let name,(capture_variables,rhs) =
198 match output_type with
199 `Term -> name, eat_branch leftno context ty pat
200 | `Pattern -> "_", ([], k ~context pat)
202 Ast.Pattern (name, None(*CSC Some (ctor_puri !j)*), capture_variables), rhs
203 ) constructors patterns
204 with Invalid_argument _ -> assert false
207 match output_type with
209 | `Term -> Some case_indty
211 idref (Ast.Case (k ~context te, indty, Some (k ~context outty), patterns))
214 (* persistent state *)
217 let initial_level2_patterns32 () = Hashtbl.create 211
218 let initial_interpretations () = Hashtbl.create 211
220 let level2_patterns32 = ref (initial_level2_patterns32 ())
221 (* symb -> id list ref *)
222 let interpretations = ref (initial_interpretations ())
224 let compiled32 = ref None
226 let pattern32_matrix = ref []
227 let counter = ref ~-1
232 stack := (!counter,!level2_patterns32,!interpretations,!compiled32,!pattern32_matrix)::!stack;
234 level2_patterns32 := initial_level2_patterns32 ();
235 interpretations := initial_interpretations ();
237 pattern32_matrix := []
243 | (ocounter,olevel2_patterns32,ointerpretations,ocompiled32,opattern32_matrix)::old ->
246 level2_patterns32 := olevel2_patterns32;
247 interpretations := ointerpretations;
248 compiled32 := ocompiled32;
249 pattern32_matrix := opattern32_matrix
253 let get_compiled32 () =
254 match !compiled32 with
255 | None -> assert false
256 | Some f -> Lazy.force f
258 let set_compiled32 f = compiled32 := Some f
261 List.fold_right (fun idref t -> Ast.AttributedTerm (`IdRef idref, t))
263 let instantiate32 idrefs env symbol args =
264 let rec instantiate_arg = function
265 | Ast.IdentArg (n, name) ->
267 try List.assoc name env
268 with Not_found -> prerr_endline ("name not found in env: "^name);
271 let rec count_lambda = function
272 | Ast.AttributedTerm (_, t) -> count_lambda t
273 | Ast.Binder (`Lambda, _, body) -> 1 + count_lambda body
276 let rec add_lambda t n =
278 let name = CicNotationUtil.fresh_name () in
279 Ast.Binder (`Lambda, (Ast.Ident (name, None), None),
280 Ast.Appl [add_lambda t (n - 1); Ast.Ident (name, None)])
284 add_lambda t (n - count_lambda t)
287 let symbol = Ast.Symbol (symbol, 0) in
288 add_idrefs idrefs symbol
290 if args = [] then head
291 else Ast.Appl (head :: List.map instantiate_arg args)
293 let rec nast_of_cic1 status ~idref ~output_type ~metasenv ~subst ~context term =
294 match (get_compiled32 ()) term with
296 nast_of_cic0 status ~idref ~output_type ~metasenv ~subst
297 (nast_of_cic1 status ~idref ~output_type ~metasenv ~subst) ~context term
298 | Some (env, ctors, pid) ->
305 (match term with NCic.Const nref -> nref | _ -> assert false)
306 (CicNotationPt.Ident ("dummy",None))
309 Ast.AttributedTerm (`IdRef id, _) -> id
317 nast_of_cic1 status ~idref ~output_type ~subst ~metasenv ~context
321 let _, symbol, args, _ =
323 TermAcicContent.find_level2_patterns32 pid
324 with Not_found -> assert false
326 let ast = instantiate32 idrefs env symbol args in
327 idref ast (*Ast.AttributedTerm (`IdRef (idref term), ast)*)
330 let load_patterns32 t =
332 HExtlib.filter_map (function (true, ap, id) -> Some (ap, id) | _ -> None) t
334 set_compiled32 (lazy (Ncic2astMatcher.Matcher32.compiler t))
336 TermAcicContent.add_load_patterns32 load_patterns32;
337 TermAcicContent.init ()
341 let ast_of_acic ~output_type id_to_sort annterm =
342 debug_print (lazy ("ast_of_acic <- "
343 ^ CicPp.ppterm (Deannotate.deannotate_term annterm)));
344 let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in
345 let ast = ast_of_acic1 ~output_type term_info annterm in
346 debug_print (lazy ("ast_of_acic -> " ^ CicNotationPp.pp_term ast));
354 let add_interpretation dsc (symbol, args) appl_pattern =
355 let id = fresh_id () in
356 Hashtbl.add !level2_patterns32 id (dsc, symbol, args, appl_pattern);
357 pattern32_matrix := (true, appl_pattern, id) :: !pattern32_matrix;
358 load_patterns32 !pattern32_matrix;
360 let ids = Hashtbl.find !interpretations symbol in
362 with Not_found -> Hashtbl.add !interpretations symbol (ref [id]));
365 let get_all_interpretations () =
367 (function (_, _, id) ->
370 Hashtbl.find !level2_patterns32 id
371 with Not_found -> assert false
376 let get_active_interpretations () =
377 HExtlib.filter_map (function (true, _, id) -> Some id | _ -> None)
380 let set_active_interpretations ids =
381 let pattern32_matrix' =
384 | (_, ap, id) when List.mem id ids -> (true, ap, id)
385 | (_, ap, id) -> (false, ap, id))
388 pattern32_matrix := pattern32_matrix';
389 load_patterns32 !pattern32_matrix
391 exception Interpretation_not_found
393 let lookup_interpretations symbol =
396 (List.sort Pervasives.compare
399 let (dsc, _, args, appl_pattern) =
401 Hashtbl.find !level2_patterns32 id
402 with Not_found -> assert false
404 dsc, args, appl_pattern)
405 !(Hashtbl.find !interpretations symbol)))
406 with Not_found -> raise Interpretation_not_found
408 let remove_interpretation id =
410 let dsc, symbol, _, _ = Hashtbl.find !level2_patterns32 id in
411 let ids = Hashtbl.find !interpretations symbol in
412 ids := List.filter ((<>) id) !ids;
413 Hashtbl.remove !level2_patterns32 id;
414 with Not_found -> raise Interpretation_not_found);
416 List.filter (fun (_, _, id') -> id <> id') !pattern32_matrix;
417 load_patterns32 !pattern32_matrix
419 let _ = load_patterns32 []
421 let instantiate_appl_pattern
422 ~mk_appl ~mk_implicit ~term_of_uri env appl_pattern
425 try List.assoc name env
427 prerr_endline (sprintf "Name %s not found" name);
430 let rec aux = function
431 | Ast.UriPattern uri -> term_of_uri uri
432 | Ast.ImplicitPattern -> mk_implicit false
433 | Ast.VarPattern name -> lookup name
434 | Ast.ApplPattern terms -> mk_appl (List.map aux terms)
439 let nmap_sequent0 status ~idref ~metasenv ~subst (i,(n,context,ty)) =
440 let module K = Content in
442 nast_of_cic1 status ~idref ~output_type:`Term ~metasenv ~subst in
445 (fun item (res,context) ->
447 | name,NCic.Decl t ->
449 (* We should call build_decl_item, but we have not computed *)
450 (* the inner-types ==> we always produce a declaration *)
452 { K.dec_name = (Some name);
454 K.dec_inductive = false;
456 K.dec_type = nast_of_cic ~context t
457 })::res,item::context
458 | name,NCic.Def (t,ty) ->
460 (* We should call build_def_item, but we have not computed *)
461 (* the inner-types ==> we always produce a declaration *)
463 { K.def_name = (Some name);
466 K.def_term = nast_of_cic ~context t;
467 K.def_type = nast_of_cic ~context ty
468 })::res,item::context
471 ("-1",i,context',nast_of_cic ~context ty)
474 let nmap_sequent status ~metasenv ~subst conjecture =
475 let module K = Content in
476 let ids_to_refs = Hashtbl.create 211 in
477 let register_ref = Hashtbl.add ids_to_refs in
478 nmap_sequent0 status ~idref:(idref register_ref) ~metasenv ~subst conjecture,
482 let object_prefix = "obj:";;
483 let declaration_prefix = "decl:";;
484 let definition_prefix = "def:";;
485 let inductive_prefix = "ind:";;
486 let joint_prefix = "joint:";;
490 Ast.AttributedTerm (`IdRef id, _) -> id
494 let gen_id prefix seed =
495 let res = prefix ^ string_of_int !seed in
500 let build_def_item seed context metasenv id n t ty =
501 let module K = Content in
504 let sort = Hashtbl.find ids_to_inner_sorts id in
507 (acic2content seed context metasenv ?name:(name_of n) ~ids_to_inner_sorts ~ids_to_inner_types t)
513 { K.def_name = Some n;
514 K.def_id = gen_id definition_prefix seed;
521 Not_found -> assert false
524 let build_decl_item seed id n s =
525 let module K = Content in
529 Some (Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id))
530 with Not_found -> None
535 { K.dec_name = name_of n;
536 K.dec_id = gen_id declaration_prefix seed;
537 K.dec_inductive = false;
544 { K.dec_name = Some n;
545 K.dec_id = gen_id declaration_prefix seed;
546 K.dec_inductive = false;
552 let nmap_obj status (uri,_,metasenv,subst,kind) =
553 let module K = Content in
554 let ids_to_refs = Hashtbl.create 211 in
555 let register_ref = Hashtbl.add ids_to_refs in
556 let idref = idref register_ref in
558 nast_of_cic1 status ~idref ~output_type:`Term ~metasenv ~subst in
563 | _ -> (*Some (List.map (map_conjectures seed) metasenv)*)
564 (*CSC: used to be the previous line, that uses seed *)
565 Some (List.map (nmap_sequent0 status ~idref ~metasenv ~subst) metasenv)
567 let build_constructors seed l =
570 let ty = nast_of_cic ~context:[] ty in
571 { K.dec_name = Some n;
572 K.dec_id = gen_id declaration_prefix seed;
573 K.dec_inductive = false;
578 let build_inductive b seed =
580 let ty = nast_of_cic ~context:[] ty in
582 { K.inductive_id = gen_id inductive_prefix seed;
583 K.inductive_name = n;
584 K.inductive_kind = b;
585 K.inductive_type = ty;
586 K.inductive_constructors = build_constructors seed cl
589 let build_fixpoint b seed =
591 let t = nast_of_cic ~context:[] t in
592 let ty = nast_of_cic ~context:[] ty in
594 { K.def_id = gen_id inductive_prefix seed;
603 | NCic.Fixpoint (is_rec, ifl, _) ->
604 (gen_id object_prefix seed, [], conjectures,
606 { K.joint_id = gen_id joint_prefix seed;
609 `Recursive (List.map (fun (_,_,i,_,_) -> i) ifl)
611 K.joint_defs = List.map (build_fixpoint is_rec seed) ifl
613 | NCic.Inductive (is_ind, lno, itl, _) ->
614 (gen_id object_prefix seed, [], conjectures,
616 { K.joint_id = gen_id joint_prefix seed;
618 if is_ind then `Inductive lno else `CoInductive lno;
619 K.joint_defs = List.map (build_inductive is_ind seed) itl
621 | NCic.Constant (_,_,Some bo,ty,_) ->
622 let ty = nast_of_cic ~context:[] ty in
623 let bo = nast_of_cic ~context:[] bo in
624 (gen_id object_prefix seed, [], conjectures,
626 build_def_item seed [] [] (get_id bo) (NUri.name_of_uri uri) bo ty))
627 | NCic.Constant (_,_,None,ty,_) ->
628 let ty = nast_of_cic ~context:[] ty in
629 (gen_id object_prefix seed, [], conjectures,
631 (*CSC: ??? get_id ty here used to be the id of the axiom! *)
632 build_decl_item seed (get_id ty) (NUri.name_of_uri uri) ty))