+ (* 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)
+ ;;
+
+ let deoptionize_exp_named_subst =
+ function
+ None -> [], (function _ -> [])
+ | Some (dom,mk_exp_named_subst) -> dom,mk_exp_named_subst
+ ;;
+
+ let term_of_con_uri uri exp_named_subst =
+ Const (uri,exp_named_subst)
+ ;;
+
+ let term_of_var_uri uri exp_named_subst =
+ Var (uri,exp_named_subst)
+ ;;
+
+ let term_of_indty_uri (uri,tyno) exp_named_subst =
+ MutInd (uri, tyno, exp_named_subst)
+ ;;
+
+ let term_of_indcon_uri (uri,tyno,consno) exp_named_subst =
+ MutConstruct (uri, tyno, consno, exp_named_subst)
+ ;;
+
+ let term_of_uri uri =
+ match uri with
+ CicTextualParser0.ConUri uri ->
+ term_of_con_uri uri
+ | CicTextualParser0.VarUri uri ->
+ term_of_var_uri uri
+ | CicTextualParser0.IndTyUri (uri,tyno) ->
+ term_of_indty_uri (uri,tyno)
+ | CicTextualParser0.IndConUri (uri,tyno,consno) ->
+ term_of_indcon_uri (uri,tyno,consno)
+ ;;
+
+ let var_uri_of_id id interp =
+ let module CTP0 = CicTextualParser0 in
+ match interp (CicTextualParser0.Id id) with
+ None -> raise (UnknownIdentifier id)
+ | Some (CTP0.Uri (CTP0.VarUri uri)) -> uri
+ | Some _ -> raise TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable
+ ;;
+
+ let indty_uri_of_id id interp =
+ let module CTP0 = CicTextualParser0 in
+ match interp (CicTextualParser0.Id id) with
+ None -> raise (UnknownIdentifier id)
+ | Some (CTP0.Uri (CTP0.IndTyUri (uri,tyno))) -> (uri,tyno)
+ | Some _ -> raise InductiveTypeURIExpected
+ ;;
+
+ let mk_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 ;
+ [], function _ -> Meta (newmeta+2,irl)