| Cic.AConst (id,uri,substs) ->
register_uri id uri;
idref id (Ast.Ident (UriManager.name_of_uri uri, aux_substs substs))
- | Cic.AMutInd (id,uri,i,substs) as t ->
+ | Cic.AMutInd (id,uri,i,substs) ->
let name = name_of_inductive_type uri i in
let uri_str = UriManager.string_of_uri uri in
let puri_str = sprintf "%s#xpointer(1/%d)" uri_str (i+1) in
let fill_empty_set s =
SOF.fold (fun e s -> SOF.add (fill_empty_universe e) s) s SOF.empty
in
- let fill_empty_entry e = { e with
+ let fill_empty_entry e = {
eq_closure = (fill_empty_set e.eq_closure) ;
ge_closure = (fill_empty_set e.ge_closure) ;
gt_closure = (fill_empty_set e.gt_closure) ;
C.MutCase (sp, i, unshare outty, unshare t,
List.map unshare pl)
| C.Fix (i, fl) ->
- let len = List.length fl in
let liftedfl =
List.map
(fun (name, i, ty, bo) -> (name, i, unshare ty, unshare bo))
in
C.Fix (i, liftedfl)
| C.CoFix (i, fl) ->
- let len = List.length fl in
let liftedfl =
List.map
(fun (name, ty, bo) -> (name, unshare ty, unshare bo))
let exp_named_subst' =
List.map (function (i,t) -> i, beta_reduce t) exp_named_subst
in
- C.Var (uri,exp_named_subst)
+ C.Var (uri,exp_named_subst')
| C.Meta (n,l) ->
C.Meta (n,
List.map
| C.LetIn (n,s,t) ->
C.LetIn
(n,eta_fix' context s,eta_fix' ((Some (n,(C.Def (s,None))))::context) t)
- | C.Appl l as appl ->
+ | C.Appl l ->
let l' = List.map (eta_fix' context) l
in
(match l' with
| C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
let exp_named_subst' = fix_exp_named_subst context exp_named_subst in
C.MutConstruct (uri, tyno, consno, exp_named_subst')
- | C.MutCase (uri, tyno, outty, term, patterns) as prima ->
+ | C.MutCase (uri, tyno, outty, term, patterns) ->
let outty' = eta_fix' context outty in
let term' = eta_fix' context term in
let patterns' = List.map (eta_fix' context) patterns in
| _ -> prerr_endline ("QUA"); assert false) in
let patterns2 =
List.map2 fix_lambdas_wrt_type
- constructor_types patterns in
+ constructor_types patterns' in
C.MutCase (uri, tyno, outty',term',patterns2)
| C.Fix (funno, funs) ->
let fun_types =
let todo_dom = domain_diff thing_dom current_dom in
(* (2) lookup function for any item (Id/Symbol/Num) *)
let lookup_choices =
- let id_choices = Hashtbl.create 1023 in
fun item ->
let choices =
let lookup_in_library () =
*)
let _ =
- let const s = Cic.Const (s, []) in
- let mutind s = Cic.MutInd (s, 0, []) in
-
DisambiguateChoices.add_num_choice
("natural number",
(fun _ num _ -> HelmLibraryObjects.build_nat (int_of_string num)));
C.MutCase (recons uri, i, restore_in_term outty, restore_in_term t,
List.map restore_in_term pl)
| C.Fix (i, fl) ->
- let len = List.length fl in
let liftedfl =
List.map
(fun (name, i, ty, bo) ->
in
C.Fix (i, liftedfl)
| C.CoFix (i, fl) ->
- let len = List.length fl in
let liftedfl =
List.map
(fun (name, ty, bo) -> (name, restore_in_term ty, restore_in_term bo))
* return the object,ugraph
*)
let add_trusted_uri_to_cache uri =
- let o,u,_ = find_or_add_to_unchecked uri in
+ let _ = find_or_add_to_unchecked uri in
Cache.unchecked_to_frozen uri;
set_type_checking_info uri;
try
let module S = CicSubstitution in
let rec reduce =
function
- (k, e, _, (C.Rel n as t), s) ->
+ (k, e, _, C.Rel n, s) ->
let d =
try
Some (RS.from_env (List.nth e (n-1)))
if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s)))
| (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *)
| (k, e, _, (C.Implicit _ as t), s) -> t (* s should be empty *)
- | (k, e, ens, (C.Cast (te,ty) as t), s) ->
+ | (k, e, ens, C.Cast (te,ty), s) ->
reduce (k, e, ens, te, s) (* s should be empty *)
| (k, e, ens, (C.Prod _ as t), s) ->
unwind k e ens t (* s should be empty *)
| (k, e, ens, (C.Lambda (_,_,t) as t'), []) -> unwind k e ens t'
| (k, e, ens, C.Lambda (_,_,t), p::s) ->
reduce (k+1, (RS.stack_to_env ~reduce ~unwind p)::e, ens, t,s)
- | (k, e, ens, (C.LetIn (_,m,t) as t'), s) ->
+ | (k, e, ens, C.LetIn (_,m,t), s) ->
let m' = RS.compute_to_env ~reduce ~unwind k e ens m in
reduce (k+1, m'::e, ens, t, s)
| (_, _, _, C.Appl [], _) -> assert false
| (k, e, ens, (C.MutCase (mutind,i,_,term,pl) as t),s) ->
let decofix =
function
- C.CoFix (i,fl) as t ->
+ C.CoFix (i,fl) ->
let (_,_,body) = List.nth fl i in
let body' =
let counter = ref (List.length fl) in
let t = whd ~delta ~subst ctx term in
let aux = normalize ~delta ~subst in
let decl name t = Some (name, C.Decl t) in
- let def name t = Some (name, C.Def (t,None)) in
+ let def name t = Some (name, C.Def (t,None)) in
match t with
| C.Rel n -> t
| C.Var (uri,exp_named_subst) ->
List.map (function (uri,t) -> (uri,substaux k t)) exp_named_subst
in
C.Var (uri,exp_named_subst')
- | C.Meta (i, l) as t ->
+ | C.Meta (i, l) ->
let l' =
List.map
(function
*)
C.Var (uri,exp_named_subst'')
)
- | C.Meta (i, l) as t ->
+ | C.Meta (i, l) ->
let l' =
List.map
(function
C.Var (uri,exp_named_subst')
| C.Meta (i,l) ->
let l' = List.map (function None -> None | Some t -> Some (aux k t)) l in
- C.Meta (i,l)
+ C.Meta (i,l')
| C.Sort _
| C.Implicit _ as t -> t
| C.Cast (te,ty) -> C.Cast (aux k te, aux k ty)
ugraph'
) ugraph cl in
(i + 1),ugraph''
- ) itl (1,ugraph)
+ ) itl (1,ugrap1)
in
ugraph2
| C.Lambda _
| C.LetIn _ ->
raise (AssertFailure (lazy "25"))(* due to type-checking *)
- | C.Appl ((C.MutInd (uri,_,_))::_) as ty
- when uri == coInductiveTypeURI ->
+ | C.Appl ((C.MutInd (uri,_,_))::_) when uri == coInductiveTypeURI ->
guarded_by_constructors ~subst context n nn true te []
coInductiveTypeURI
- | C.Appl ((C.MutInd (uri,_,_))::_) as ty ->
+ | C.Appl ((C.MutInd (uri,_,_))::_) ->
guarded_by_constructors ~subst context n nn true te tl
coInductiveTypeURI
| C.Appl _ ->
(lazy (sprintf
("Case analysys: analysed term type is %s (%s#1/%d{_}), but is expected to be (an application of) %s#1/%d{_}")
(CicPp.ppterm typ) (U.string_of_uri uri') i' (U.string_of_uri uri) i)))
- | C.Appl
- ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) as typ' ->
+ | C.Appl ((C.MutInd (uri',i',exp_named_subst) as typ):: tl) ->
if U.eq uri uri' && i = i' then
let params,args =
split tl (List.length tl - k)
(*CSC: this is a very rough approximation; to be finished *)
let are_all_occurrences_positive metasenv ugraph uri tys leftno =
- let number_of_types = List.length tys in
let subst,metasenv,ugraph,tys =
List.fold_right
(fun (name,ind,arity,cl) (subst,metasenv,ugraph,acc) ->
let tl_renderings =
List.map
(fun f ->
- let indent_header = if indent then string_indent else "" in
+(* let indent_header = if indent then string_indent else "" in *)
snd (indent_children (f children_size)))
tl_fs
in
remove_left_quote (Ulexing.utf8_lexeme lexbuf))
| meta_anonymous -> return lexbuf ("UNPARSED_META", "anonymous")
| beginnote ->
- let comment = comment_token (Ulexing.utf8_lexeme lexbuf) 0 lexbuf in
+ let _comment = comment_token (Ulexing.utf8_lexeme lexbuf) 0 lexbuf in
(* let comment =
Ulexing.utf8_sub_lexeme lexbuf 2 (Ulexing.lexeme_length lexbuf - 4)
in
if lexeme.[0] = '\\'
then [ Utf8Macro.expand (String.sub lexeme 1 (String.length lexeme - 1)) ]
else List.rev (Hashtbl.find_all ligatures lexeme)
- with Invalid_argument _ | Utf8Macro.Macro_not_found _ as exn -> []
+ with Invalid_argument _ | Utf8Macro.Macro_not_found _ -> []
List.split (extract_term_production level1_pattern)
in
let level = level_of precedence associativity in
- let p_names = flatten_opt p_bindings in
+(* let p_names = flatten_opt p_bindings in *)
let _ =
Grammar.extend
[ Grammar.Entry.obj (term: 'a Grammar.Entry.e),
let render ids_to_uris =
let module A = Ast in
let module P = Mpresentation in
- let use_unicode = true in
+(* let use_unicode = true in *)
let lookup_uri id =
(try
let uri = Hashtbl.find ids_to_uris id in
let new_xref = ref [] in
let new_xmlattrs = ref [] in
let new_pos = ref pos in
- let reinit = ref false in
+(* let reinit = ref false in *)
let rec aux_attribute =
function
| A.AttributedTerm (attr, t) ->
| Ast.Variable _ -> PatternMatcher.Variable
| Ast.Magic _
| Ast.Layout _
- | Ast.Literal _ as t -> assert false
+ | Ast.Literal _ -> assert false
| _ -> PatternMatcher.Constructor
let tag_of_pattern = get_tag
let tag_of_term t = get_tag t
Ast.AttributedTerm (attr, subst_singleton pos env t)
| t -> CicNotationUtil.group (subst pos env t)
and subst pos env = function
- | Ast.AttributedTerm (attr, t) as term ->
+ | Ast.AttributedTerm (attr, t) ->
(* prerr_endline ("loosing attribute " ^ CicNotationPp.pp_attribute attr); *)
subst pos env t
| Ast.Variable var ->
exception NoOtherChoices;;
-let is_in_metasenv goal metasenv =
- try
- let (_, ey ,ty) =
- CicUtil.lookup_meta goal metasenv in
- true
- with CicUtil.Meta_not_found _ -> false
-
let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
universe
=
let _,metasenv,p,_ = proof in
(* first of all we check if the goal has been already
inspected *)
- assert (is_in_metasenv goal metasenv);
+ assert (CicUtil.exists_meta goal metasenv);
let exitus =
try Hashtbl.find inspected_goals ty
with Not_found -> NotYetInspected in
| [] -> []
| (subst,(proof, goals, sign))::tl ->
let _,metasenv,_,_ = proof in
- let is_in_metasenv (goal, _) =
- try
- let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
- true
- with CicUtil.Meta_not_found _ -> false
+ let goals'=
+ List.filter (fun (goal, _) -> CicUtil.exists_meta goal metasenv) goals
in
- let goals'= List.filter is_in_metasenv goals in
auto_new_aux dbd
width already_seen_goals universe ((subst,(proof, goals', sign))::tl)
T.then_
~start:(injection1_tac ~i ~term)
~continuation:(traverse_list (i+1) tl1 tl2)
- | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: i 2 termini hanno in testa lo stesso costruttore, ma applicato a un numero diverso di termini. possibile???")) ; T.id_tac
+ | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: i 2 termini hanno in testa lo stesso costruttore, ma applicato a un numero diverso di termini. possibile???"))
in traverse_list 1 applist1 applist2
| ((C.MutConstruct (uri1,typeno1,consno1,exp_named_subst1)),
(C.MutConstruct (uri2,typeno2,consno2,exp_named_subst2)))
assert (wanted = None); (* this should be checked syntactically *)
let proof,goal = status in
let curi, metasenv, pbo, pty = proof in
- let (metano,context,gty) as conjecture = CicUtil.lookup_meta goal metasenv in
+ let (metano,context,gty) = CicUtil.lookup_meta goal metasenv in
match hyps_pat with
he::(_::_ as tl) ->
PET.apply_tactic
debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto:\n");
debug_pcontext s_context;
- let fhyp = String.copy "new_hyp_for_fourier" in
-
(* here we need to negate the thesis, but to do this we need to apply the
right theoreme,so let's parse our thesis *)
let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose
let cmatch' = Constr.cmatch'
-let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as status) =
+let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
let (_, metasenv, _, _) = proof in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let main, sig_constants = Constr.signature_of ty in
let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
uris
-let equations_for_goal ~(dbd:HMysql.dbd) ((proof, goal) as status) =
- let to_string set =
+let equations_for_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
+(* let to_string set =
"{ " ^
(String.concat ", "
(Constr.UriManagerSet.fold
(fun u l -> (UriManager.string_of_uri u)::l) set []))
^ " }"
- in
+ in *)
let (_, metasenv, _, _) = proof in
let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
let main, sig_constants = Constr.signature_of ty in
List.concat (map2 "wrong number of arguments in application"
(fun t1 t2 -> aux context t1 t2) terms1 terms2)
in
- let context_len = List.length context in
let roots = aux context where term in
match wanted with
None -> [],metasenv,ugraph,roots
let subst,metasenv,ugraph,ty_terms =
select_in_term ~metasenv ~context ~ugraph ~term:ty
~pattern:(what,goal_pattern) in
- let context_len = List.length context in
let subst,metasenv,ugraph,context_terms =
let subst,metasenv,ugraph,res,_ =
(List.fold_right
List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
in
C.Var (uri,exp_named_subst')
- | C.Meta (i, l) as t ->
+ | C.Meta (i, l) ->
let l' =
List.map
(function
S.lift (k-1) (find_image t)
with Not_found ->
match t with
- C.Rel n as t ->
+ C.Rel n ->
if n < k then C.Rel n else C.Rel (n + nnn)
| C.Var (uri,exp_named_subst) ->
let exp_named_subst' =
List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
in
C.Var (uri,exp_named_subst')
- | C.Meta (i, l) as t ->
+ | C.Meta (i, l) ->
let l' =
List.map
(function
in
let t' = C.MutInd (uri,i,exp_named_subst') in
if l = [] then t' else C.Appl (t'::l)
- | C.MutConstruct (uri,i,j,exp_named_subst) as t ->
+ | C.MutConstruct (uri,i,j,exp_named_subst) ->
let exp_named_subst' =
reduceaux_exp_named_subst context l exp_named_subst
in
| C.MutCase (mutind,i,outtype,term,pl) ->
let decofix =
function
- C.CoFix (i,fl) as t ->
- let tys =
- List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
- in
+ C.CoFix (i,fl) ->
let (_,_,body) = List.nth fl i in
let body' =
let counter = ref (List.length fl) in
in
reduceaux context [] body'
| C.Appl (C.CoFix (i,fl) :: tl) ->
- let tys =
- List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
- in
let (_,_,body) = List.nth fl i in
let body' =
let counter = ref (List.length fl) in
(*CSC: It does not perform simplification in a Case *)
let simpl context =
- let mk_appl t l =
- if l = [] then
- t
- else
- match t with
- | Cic.Appl l' -> Cic.Appl (l'@l)
- | _ -> Cic.Appl (t::l)
- in
(* reduceaux is equal to the reduceaux locally defined inside *)
(* reduce, but for the const case. *)
(**** Step 1 ****)
| C.MutCase (mutind,i,outtype,term,pl) ->
let decofix =
function
- C.CoFix (i,fl) as t ->
- let tys =
- List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl in
+ C.CoFix (i,fl) ->
let (_,_,body) = List.nth fl i in
let body' =
let counter = ref (List.length fl) in
body
in
let tl' = List.map (reduceaux context []) tl in
- reduceaux context tl body'
+ reduceaux context tl' body'
| t -> t
in
(match decofix (CicReduction.whd context term) with
let res,constant_args =
let rec aux rev_constant_args l =
function
- C.Lambda (name,s,t) as t' ->
+ C.Lambda (name,s,t) ->
begin
match l with
[] -> raise WrongShape
end
| C.LetIn (_,s,t) ->
aux rev_constant_args l (S.subst s t)
- | C.Fix (i,fl) as t ->
- let tys =
- List.map (function (name,_,ty,_) ->
- Some (C.Name name, C.Decl ty)) fl
- in
+ | C.Fix (i,fl) ->
let (_,recindex,_,body) = List.nth fl i in
let recparam =
try
projects / helm.git / commitdiff