let get_cookingno uri =
UriManager.relative_depth !CicTextualParser0.current_uri uri 0
;;
-
+
+ (* Returns the first meta whose number is above the *)
+ (* number of the higher meta. *)
+ (*CSC: cut&pasted from proofEngine.ml *)
+ let new_meta () =
+ let rec aux =
+ function
+ None,[] -> 1
+ | Some n,[] -> n
+ | None,(n,_,_)::tl -> aux (Some n,tl)
+ | Some m,(n,_,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
+ in
+ 1 + aux (None,!CicTextualParser0.metasenv)
+ ;;
+
+ (* identity_relocation_list_for_metavariable i canonical_context *)
+ (* returns the identity relocation list, which is the list [1 ; ... ; n] *)
+ (* where n = List.length [canonical_context] *)
+ (*CSC: ma mi basta la lunghezza del contesto canonico!!!*)
+ (*CSC: cut&pasted from proofEngine.ml *)
+ let identity_relocation_list_for_metavariable canonical_context =
+ let canonical_context_length = List.length canonical_context in
+ let rec aux =
+ function
+ (_,[]) -> []
+ | (n,None::tl) -> None::(aux ((n+1),tl))
+ | (n,_::tl) -> (Some (Cic.Rel n))::(aux ((n+1),tl))
+ in
+ aux (1,canonical_context)
+ ;;
+
%}
%token <string> ID
%token <int> META
done ;
CoFix (idx,cofixfuns)
}
- | IMPLICIT { Implicit }
+ | IMPLICIT
+ { let newmeta = new_meta () in
+ let new_canonical_context = [] in
+ let irl =
+ identity_relocation_list_for_metavariable new_canonical_context
+ in
+ CicTextualParser0.metasenv :=
+ [newmeta, new_canonical_context, Sort Type ;
+ newmeta+1, new_canonical_context, Meta (newmeta,irl);
+ newmeta+2, new_canonical_context, Meta (newmeta+1,irl)
+ ] @ !CicTextualParser0.metasenv ;
+ Meta (newmeta+2,irl)
+ }
| SET { Sort Set }
| PROP { Sort Prop }
| TYPE { Sort Type }
* http://cs.unibo.it/helm/.
*)
-let main ~current_uri ~context lexer lexbuf =
+let main ~current_uri ~context ~metasenv lexer lexbuf =
(* Warning: higly non-reentrant code!!! *)
CicTextualParser0.current_uri := current_uri ;
CicTextualParser0.binders := context ;
- let res = CicTextualParser.main lexer lexbuf in
- CicTextualParser0.binders := [] ;
- res
+ CicTextualParser0.metasenv := metasenv ;
+ match CicTextualParser.main lexer lexbuf with
+ None -> None
+ | Some res ->
+ CicTextualParser0.binders := [] ;
+ Some (!CicTextualParser0.metasenv,res)
;;