+(*
+open Disambiguate_struct
+open ProofEngineHelpers
+
+exception UnknownIdentifier of string
+exception InductiveTypeExpected
+
+let list_of_domain dom = Domain.fold (fun s acc -> s :: acc) dom []
+let apply_interp (interp: interpretation) item = snd (interp item)
+
+let pre_disambiguate ~context ast =
+ let rec aux loc context = function
+ | Ast.LocatedTerm (loc, term) -> aux loc context term
+ | Ast.Appl terms ->
+ let (dom, funs) =
+ List.fold_left
+ (fun (dom, funs) term ->
+ let (dom', f) = aux loc context term in
+ (Domain.union dom dom', f :: funs))
+ (Domain.empty, [])
+ terms
+ in
+ let f interp =
+ Cic.Appl (List.map (fun f -> f interp) (List.rev funs))
+ in
+ (dom, f)
+ | Ast.Appl_symbol (symb, args) ->
+ let (dom, funs) =
+ List.fold_left
+ (fun (dom, funs) term ->
+ let (dom', f) = aux loc context term in
+ (Domain.union dom dom', f :: funs))
+ (Domain.empty, [])
+ args
+ in
+ (Domain.add (Symbol (symb, 0)) dom,
+ (fun interp ->
+ apply_interp interp (Symbol (symb, 0)) interp
+ (List.map (fun f -> f interp) funs)))
+ | Ast.Binder (binder_kind, var, typ, body) ->
+ let (type_dom, type_f) =
+ match typ with
+ | Some t -> aux loc context t
+ | None -> (Domain.empty, (fun _ -> Cic.Implicit))
+ in
+ let (dom', body_f) = aux loc (Some var :: context) body in
+ let dom'' = Domain.union dom' type_dom in
+ (dom'',
+ match binder_kind with
+ | `Lambda ->
+ (fun interp ->
+ Cic.Lambda (var, type_f interp, body_f interp))
+ | `Pi | `Forall ->
+ (fun interp ->
+ Cic.Prod (var, type_f interp, body_f interp))
+ | `Exists ->
+ (fun interp ->
+ let typ = type_f interp in
+ Cic.Appl
+ [ apply_interp interp (Id "ex") interp [];
+ typ;
+ (Cic.Lambda (var, typ, body_f interp)) ]))
+ | Ast.Case (term, indty_ident, outtype, branches) ->
+ let (term_dom, term_f) = aux loc context term in
+ let (outtype_dom, outtype_f) =
+ match outtype with
+ | Some typ -> aux loc context typ
+ | None -> (Domain.empty, (fun _ -> Cic.Implicit))
+ in
+ let do_branch (pat, term) =
+ let rec do_branch' context = function
+ | [] -> aux loc context term
+ | hd :: tl ->
+ let (dom, f) = do_branch' (Some (Cic.Name hd) :: context) tl in
+ (dom,
+ (fun interp ->
+ Cic.Lambda (Cic.Name hd, Cic.Implicit, f interp)))
+ in
+ match pat with
+ | _ :: tl -> (* ignoring constructor *)
+ do_branch' context tl
+ | [] -> assert false
+ in
+ let (branches_dom, branches_f) =
+ List.fold_right
+ (fun branch (dom, f) ->
+ let (dom', f') = do_branch branch in
+ Domain.union dom dom', (fun interp -> f' interp :: f interp))
+ branches
+ (Domain.empty, (fun _ -> []))
+ in
+ (Domain.union outtype_dom (Domain.union term_dom branches_dom),
+ (fun interp ->
+ let (indtype_uri, indtype_no) =
+ match apply_interp interp (Id indty_ident) interp [] with
+ | Cic.MutInd (uri, tyno, _) -> uri, tyno
+ | _ -> assert false
+ in
+ Cic.MutCase (indtype_uri, indtype_no, outtype_f interp,
+ term_f interp, branches_f interp)))
+ | Ast.LetIn (var, body, where) ->
+ let (body_dom, body_f) = aux loc context body in
+ let (where_dom, where_f) = aux loc context where in
+ (Domain.union body_dom where_dom,
+ fun interp -> Cic.LetIn (Cic.Name var, body_f interp, where_f interp))
+ | Ast.LetRec (kind, defs, where) ->
+ let context' =
+ List.fold_left (fun acc (var, _, _, _) -> Some (Cic.Name var) :: acc)
+ context defs
+ in
+ let (where_dom, where_f) = aux loc context' where in
+ let inductiveFuns =
+ List.map
+ (fun (var, body, typ, decr_idx) ->
+ let body_dom, body_f = aux loc context' body in
+ let typ_dom, typ_f =
+ match typ with
+ | None -> (Domain.empty, (fun _ -> Cic.Implicit))
+ | Some typ -> aux loc context' typ
+ in
+ (Domain.union body_dom typ_dom,
+ (fun interp ->
+ (var, decr_idx, typ_f interp, body_f interp))))
+ defs
+ in
+ let dom =
+ List.fold_left (fun acc (dom, _) -> Domain.union acc dom)
+ where_dom inductiveFuns
+ in
+ let inductiveFuns interp =
+ List.map (fun (_, g) -> g interp) inductiveFuns
+ in
+ let build_term counter funs =
+ (* this is the body of the fold_right function below. Rationale: Fix
+ * and CoFix cases differs only in an additional index in the
+ * indcutiveFun list, see Cic.term *)
+ match kind with
+ | `Inductive ->
+ (fun (var, _, _, _) cic ->
+ incr counter;
+ Cic.LetIn (Cic.Name var, Cic.Fix (!counter, funs), cic))
+ | `CoInductive ->
+ let funs =
+ List.map (fun (name, _, typ, body) -> (name, typ, body)) funs
+ in
+ (fun (var, _, _, _) cic ->
+ Cic.LetIn (Cic.Name var, Cic.CoFix (!counter, funs), cic))
+ in
+ (dom,
+ (fun interp ->
+ let counter = ref 0 in
+ let funs = inductiveFuns interp in
+ List.fold_right (build_term counter funs) funs (where_f interp)))
+ | Ast.Ident (name, subst) ->
+ (* TODO hanlde explicit substitutions *)
+ let rec find acc e = function
+ | [] -> raise Not_found
+ | Some (Cic.Name hd) :: tl when e = hd -> acc
+ | _ :: tl -> find (acc + 1) e tl
+ in
+ (try
+ let index = find 1 name context in
+ if subst <> [] then
+ fail loc "Explicit substitutions not allowed here";
+ (Domain.empty, fun _ -> Cic.Rel index)
+ with Not_found ->
+ (Domain.singleton (Id name),
+ (fun interp -> apply_interp interp (Id name) interp [])))
+ | Ast.Num num ->
+ (* TODO check to see if num can be removed from the domain *)
+ (Domain.singleton (Num (num, 0)),
+ (fun interp -> apply_interp interp (Num (num, 0)) interp []))
+ | Ast.Meta (index, subst) ->
+ let (dom, funs) =
+ List.fold_left
+ (fun (dom, funs) term ->
+ match term with
+ | None -> (dom, (fun _ -> None) :: funs)
+ | Some term ->
+ let (dom', f) = aux loc context term in
+ (Domain.union dom dom',
+ (fun interp -> Some (f interp)) :: funs))
+ (Domain.empty, [])
+ subst
+ in
+ let f interp =
+ Cic.Meta (index, List.map (fun f -> f interp) (List.rev funs))
+ in
+ (dom, f)
+ | Ast.Sort `Prop -> Domain.empty, fun _ -> Cic.Sort Cic.Prop
+ | Ast.Sort `Set -> Domain.empty, fun _ -> Cic.Sort Cic.Set
+ | Ast.Sort `Type -> Domain.empty, fun _ -> Cic.Sort Cic.Type
+ | Ast.Sort `CProp -> Domain.empty, fun _ -> Cic.Sort Cic.CProp
+ in
+ match ast with
+ | Ast.LocatedTerm (loc, term) ->
+ let (dom, f) = aux loc context term in
+ dom, f
+ | _ -> assert false
+
+let main ~context char_stream =
+ let term_ast = parse_term char_stream in
+ debug_print (Pp.pp_term term_ast);
+ pre_disambiguate ~context term_ast
+*)
+