* http://helm.cs.unibo.it/
*)
-open Disambiguate_types
+open Printf
+
+open DisambiguateTypes
+open UriManager
exception Invalid_choice
exception No_choices of domain_item
let refine metasenv context term =
let metasenv, term = CicMkImplicit.expand_implicits metasenv context term in
+ debug_print (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm term));
try
let term', _, _, metasenv' = CicRefine.type_of_aux' metasenv context term in
Ok (term', metasenv')
debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ;
Ko
-open Printf
-
-open UriManager
-
-let indtyuri_of_uri uri =
- let index_sharp = String.index uri '#' in
- let index_num = index_sharp + 3 in
- (UriManager.uri_of_string (String.sub uri 0 index_sharp),
- int_of_string(String.sub uri index_num (String.length uri - index_num)) - 1)
-
-let indconuri_of_uri uri =
- let index_sharp = String.index uri '#' in
- let index_div = String.rindex uri '/' in
- let index_con = index_div + 1 in
- (UriManager.uri_of_string (String.sub uri 0 index_sharp),
- int_of_string
- (String.sub uri (index_sharp + 3) (index_div - index_sharp - 3)) - 1,
- int_of_string
- (String.sub uri index_con (String.length uri - index_con)))
-
- (* TODO move it to Cic *)
-let term_of_uri uri =
- try
- (* Constant *)
- (* TODO explicit substitutions? *)
- let len = String.length uri in
- if String.sub uri (len - 4) 4 = ".con" then
- Cic.Const (uri_of_string uri, [])
- else if String.sub uri (len - 4) 4 = ".var" then
- Cic.Var (uri_of_string uri, [])
- else
- (try
- (* Inductive Type *)
- let uri',typeno = indtyuri_of_uri uri in
- Cic.MutInd (uri', typeno, [])
- with
- | UriManager.IllFormedUri _ | Failure _ | Invalid_argument _ ->
- (* Constructor of an Inductive Type *)
- let uri',typeno,consno = indconuri_of_uri uri in
- Cic.MutConstruct (uri', typeno, consno, []))
- with
- | Invalid_argument _ -> raise (UriManager.IllFormedUri uri)
-
let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
snd (Environment.find item env) env num args
+ (* TODO move it to Cic *)
let find_in_environment name context =
let rec aux acc = function
| [] -> raise Not_found
let interpretate ~context ~env ast =
let rec aux loc context = function
- | Ast.LocatedTerm (loc, term) -> aux loc context term
- | Ast.Appl terms -> Cic.Appl (List.map (aux loc context) terms)
- | Ast.Appl_symbol (symb, i, args) ->
+ | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term
+ | CicTextualParser2Ast.Appl terms -> Cic.Appl (List.map (aux loc context) terms)
+ | CicTextualParser2Ast.Appl_symbol (symb, i, args) ->
let cic_args = List.map (aux loc context) args in
resolve env (Symbol (symb, i)) ~args:cic_args ()
- | Ast.Binder (binder_kind, var, typ, body) ->
+ | CicTextualParser2Ast.Binder (binder_kind, var, typ, body) ->
let cic_type = aux_option loc context typ in
let cic_body = aux loc (var :: context) body in
(match binder_kind with
| `Exists ->
resolve env (Symbol ("exists", 0))
~args:[ cic_type; Cic.Lambda (var, cic_type, cic_body) ] ())
- | Ast.Case (term, indty_ident, outtype, branches) ->
+ | CicTextualParser2Ast.Case (term, indty_ident, outtype, branches) ->
let cic_term = aux loc context term in
let cic_outtype = aux_option loc context outtype in
let do_branch (pat, term) =
match resolve env (Id indty_ident) () with
| Cic.MutInd (uri, tyno, _) -> uri, tyno
| Cic.Implicit -> raise Try_again
- | _ -> Parser.fail loc ("Not an inductive type: " ^ indty_ident)
+ | _ -> raise Invalid_choice
in
Cic.MutCase (indtype_uri, indtype_no, cic_outtype, cic_term,
(List.map do_branch branches))
- | Ast.LetIn (var, def, body) ->
+ | CicTextualParser2Ast.LetIn (var, def, body) ->
let cic_def = aux loc context def in
let name = Cic.Name var in
let cic_body = aux loc (name :: context) body in
Cic.LetIn (name, cic_def, cic_body)
- | Ast.LetRec (kind, defs, body) ->
+ | CicTextualParser2Ast.LetRec (kind, defs, body) ->
let context' =
List.fold_left (fun acc (var, _, _, _) -> Cic.Name var :: acc)
context defs
Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic))
in
List.fold_right (build_term inductiveFuns) inductiveFuns cic_body
- | Ast.Ident (name, subst) ->
+ | CicTextualParser2Ast.Ident (name, subst) ->
(* TODO hanlde explicit substitutions *)
(try
let index = find_in_environment name context in
if subst <> [] then
- Parser.fail loc "Explicit substitutions not allowed here";
+ CicTextualParser2.fail loc "Explicit substitutions not allowed here";
Cic.Rel index
with Not_found -> resolve env (Id name) ())
- | Ast.Num (num, i) -> resolve env (Num i) ~num ()
- | Ast.Meta (index, subst) ->
+ | CicTextualParser2Ast.Num (num, i) -> resolve env (Num i) ~num ()
+ | CicTextualParser2Ast.Meta (index, subst) ->
let cic_subst =
List.map
(function None -> None | Some term -> Some (aux loc context term))
subst
in
Cic.Meta (index, cic_subst)
- | Ast.Sort `Prop -> Cic.Sort Cic.Prop
- | Ast.Sort `Set -> Cic.Sort Cic.Set
- | Ast.Sort `Type -> Cic.Sort Cic.Type
- | Ast.Sort `CProp -> Cic.Sort Cic.CProp
+ | CicTextualParser2Ast.Sort `Prop -> Cic.Sort Cic.Prop
+ | CicTextualParser2Ast.Sort `Set -> Cic.Sort Cic.Set
+ | CicTextualParser2Ast.Sort `Type -> Cic.Sort Cic.Type
+ | CicTextualParser2Ast.Sort `CProp -> Cic.Sort Cic.CProp
and aux_option loc context = function
| None -> Cic.Implicit
| Some term -> aux loc context term
in
match ast with
- | Ast.LocatedTerm (loc, term) -> aux loc context term
+ | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term
| _ -> assert false
let domain_of_term ~context ast =
let rec aux loc context = function
- | Ast.LocatedTerm (_, term) -> aux loc context term
- | Ast.Appl terms ->
+ | CicTextualParser2Ast.LocatedTerm (_, term) -> aux loc context term
+ | CicTextualParser2Ast.Appl terms ->
List.fold_left (fun dom term -> Domain.union dom (aux loc context term))
Domain.empty terms
- | Ast.Appl_symbol (symb, i, args) ->
+ | CicTextualParser2Ast.Appl_symbol (symb, i, args) ->
List.fold_left (fun dom term -> Domain.union dom (aux loc context term))
(Domain.singleton (Symbol (symb, i))) args
- | Ast.Binder (_, var, typ, body) ->
+ | CicTextualParser2Ast.Binder (_, var, typ, body) ->
let type_dom = aux_option loc context typ in
let body_dom = aux loc (var :: context) body in
Domain.union type_dom body_dom
- | Ast.Case (term, indty_ident, outtype, branches) ->
+ | CicTextualParser2Ast.Case (term, indty_ident, outtype, branches) ->
let term_dom = aux loc context term in
let outtype_dom = aux_option loc context outtype in
let do_branch (pat, term) =
in
Domain.add (Id indty_ident)
(Domain.union outtype_dom (Domain.union term_dom branches_dom))
- | Ast.LetIn (var, body, where) ->
+ | CicTextualParser2Ast.LetIn (var, body, where) ->
let body_dom = aux loc context body in
let where_dom = aux loc (Cic.Name var :: context) where in
Domain.union body_dom where_dom
- | Ast.LetRec (kind, defs, where) ->
+ | CicTextualParser2Ast.LetRec (kind, defs, where) ->
let context' =
List.fold_left (fun acc (var, _, _, _) -> Cic.Name var :: acc)
context defs
Domain.empty defs
in
Domain.union where_dom defs_dom
- | Ast.Ident (name, subst) ->
+ | CicTextualParser2Ast.Ident (name, subst) ->
(* TODO hanlde explicit substitutions *)
(try
let index = find_in_environment name context in
if subst <> [] then
- Parser.fail loc "Explicit substitutions not allowed here";
+ CicTextualParser2.fail loc "Explicit substitutions not allowed here";
Domain.empty
with Not_found -> Domain.singleton (Id name))
- | Ast.Num (num, i) -> Domain.singleton (Num i)
- | Ast.Meta (index, local_context) ->
+ | CicTextualParser2Ast.Num (num, i) -> Domain.singleton (Num i)
+ | CicTextualParser2Ast.Meta (index, local_context) ->
List.fold_left
(fun dom term -> Domain.union dom (aux_option loc context term))
Domain.empty local_context
- | Ast.Sort _ -> Domain.empty
+ | CicTextualParser2Ast.Sort _ -> Domain.empty
and aux_option loc context = function
| None -> Domain.empty
| Some t -> aux loc context t
in
match ast with
- | Ast.LocatedTerm (loc, term) -> aux loc context term
+ | CicTextualParser2Ast.LocatedTerm (loc, term) -> aux loc context term
| _ -> assert false
module Make (C: Callbacks) =
uris
in
List.map
- (fun uri -> (uri, let term = term_of_uri uri in fun _ _ _ -> term))
+ (fun uri ->
+ (uri,
+ let term =
+ try
+ HelmLibraryObjects.term_of_uri (UriManager.uri_of_string uri)
+ with _ -> assert false
+ in
+ fun _ _ _ -> term))
uris'
let disambiguate_term mqi_handle context metasenv term ~aliases:current_env
let cic_term =
interpretate ~context:disambiguate_context ~env:filled_env term
in
- debug_print
- (sprintf "TEST_INTERPRETATION: %s" (CicPp.ppterm cic_term));
refine metasenv context cic_term
with
| Try_again -> Uncertain
projects / helm.git / blobdiff