open Printf
-open Disambiguate_types
+open DisambiguateTypes
open UriManager
exception Invalid_choice
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) =
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) =